Module Smyth.Desugar

val lett : Lang.typ -> string -> Lang.exp -> Lang.exp -> Lang.exp

lett tau x binding body constructs the equivalent of the following let-binding expression:

let (x : tau) = binding in body
val func_params : Lang.param list -> Lang.exp -> Lang.exp

func_params [x0, ..., xN] body constructs the equivalent of the following nested lambda expression:

\x0 -> ... \xN -> body
val app : Lang.exp -> Lang.exp_arg list -> Lang.exp

app head [e0, ..., eN] body constructs the equivalent of the following application expression:

head e0 ... eN
val nat : int -> Lang.exp

nat n constructs the expression S (... S (Z ()) ...), where the S constructor is nested n times (i.e., Sn(Z ())).

Precondition: n >= 0.

val listt : Lang.exp list -> Lang.typ list -> Lang.exp

listt [e0, ..., eN] taus constructs the following polymorphic list expression:

Cons<taus> (e0, ... Cons<taus> (eN, Nil<taus>))
type program = {
datatypes : Lang.datatype_ctx;
definitions : (string * (Lang.typ * Lang.exp)) list;
assertions : (Lang.exp * Lang.exp) list;
main_opt : Lang.exp option;
}

Packages up datatypes, function definitions, assertions, and the main expression of a program into a single type.

val program : program -> Lang.exp * Lang.datatype_ctx

Desugars a program value into the corresponding Lang.exp value (along with its datatype context).