use less confusing Ott binary

5 files changed, 1506 insertions, 121 deletions

diff --git a/language/Makefile b/language/Makefile
index 750a5fbd..0c7563ce 100644
--- a/language/Makefile
+++ b/language/Makefile
@@ -1,4 +1,6 @@
-OTT=../../../rsem/ott/bin/ott
+#OTT=../../../rsem/ott/bin/ott
+# this is the binary that gets rebuilt by make in ott/src:
+OTT=../../../rsem/ott/src/ott
 OTTLIB=$(dir $(shell which ott))../hol
 
 .PHONY: all
@@ -36,3 +38,4 @@ clean:
 	rm -rf *~
 	-rm -rf *.uo *.ui *.sig *.sml .HOLMK
 	-rm -f *.tex *.aux *.log *.dvi *.ps *.pdf
+	rm -rf l2.pdf l2_parse.pdf l2.ml l2_parse.ml l2.lem
diff --git a/language/l2.lem b/language/l2.lem
index ea9e007d..5441587d 100644
--- a/language/l2.lem
+++ b/language/l2.lem
@@ -1,4 +1,4 @@
-(* generated by Ott 0.24 from: l2_typ.ott l2.ott *)
+(* generated by Ott 0.25 from: l2_typ.ott l2.ott *)
 open import Pervasives
 
 open import Map
diff --git a/language/l2.ml b/language/l2.ml
index d4423c54..c341a38a 100644
--- a/language/l2.ml
+++ b/language/l2.ml
@@ -1,4 +1,4 @@
-(* generated by Ott 0.24 from: l2.ott *)
+(* generated by Ott 0.25 from: l2.ott *)
 
 
 type text = string
@@ -108,6 +108,528 @@ type
 order = 
    Ord_aux of order_aux * l
 
+(** pretty printer *)
+let pp_x (y5:x) : string = y5
+
+let pp_kid_aux (kid_aux5:kid_aux) : string =
+  match kid_aux5 with
+  | (Var x) -> " ' " ^ (pp_x x)
+
+
+let pp_kid (kid5:kid) : string =
+  match kid5 with
+  | (Kid_aux (kid_aux,l)) -> (pp_kid_aux kid_aux) ^ " " ^ (pp_l l)
+
+
+let pp_effect_aux (effect_aux5:effect_aux) : string =
+  match effect_aux5 with
+  | (Effect_var kid) -> (pp_kid kid)
+  | (Effect_set (base_effect_list)) -> " { " ^ (String.concat "," (List.map (fun base_effect -> pp_base_effect base_effect) base_effect_list)) ^ " } "
+
+
+let pp_id_aux (id_aux5:id_aux) : string =
+  match id_aux5 with
+  | (Id x) -> (pp_x x)
+  | (DeIid x) -> " ( " ^ " deinfix " ^ (pp_x x) ^ " ) "
+
+
+let pp_typquant_aux (typquant_aux5:typquant_aux) : string =
+  match typquant_aux5 with
+  | (TypQ_tq (quant_item_list)) -> " forall " ^ (String.concat "," (List.map (fun quant_item -> pp_quant_item quant_item) quant_item_list)) ^ " . "
+  | TypQ_no_forall -> 
+
+
+let pp_effect (effect5:effect) : string =
+  match effect5 with
+  | (Effect_aux (effect_aux,l)) -> (pp_effect_aux effect_aux) ^ " " ^ (pp_l l)
+
+
+let pp_id (id5:id) : string =
+  match id5 with
+  | (Id_aux (id_aux,l)) -> (pp_id_aux id_aux) ^ " " ^ (pp_l l)
+
+
+let pp_typquant (typquant5:typquant) : string =
+  match typquant5 with
+  | (TypQ_aux (typquant_aux,l)) -> (pp_typquant_aux typquant_aux) ^ " " ^ (pp_l l)
+
+
+let rec pp_typ (typ5:typ) : string =
+  match typ5 with
+  | (Typ_aux (typ_aux,l)) -> (pp_typ_aux typ_aux) ^ " " ^ (pp_l l)
+and
+pp_typ_aux (typ_aux5:typ_aux) : string =
+  match typ_aux5 with
+  | Typ_wild -> " _ "
+  | (Typ_id id) -> (pp_id id)
+  | (Typ_var kid) -> (pp_kid kid)
+  | (Typ_fn (typ1,typ2,effect)) -> (pp_typ typ1) ^ " -> " ^ (pp_typ typ2) ^ " effectkw " ^ (pp_effect effect)
+  | (Typ_tup (typ_list)) -> " ( " ^ (String.concat "," (List.map (fun typ -> pp_typ typ) typ_list)) ^ " ) "
+  | (Typ_app (id,(typ_arg_list))) -> (pp_id id) ^ " < " ^ (String.concat "," (List.map (fun typ_arg -> pp_typ_arg typ_arg) typ_arg_list)) ^ " > "
+
+
+let pp_lit_aux (lit_aux5:lit_aux) : string =
+  match lit_aux5 with
+  | L_unit -> " ( " ^ " ) "
+  | L_zero -> " bitzero "
+  | L_one -> " bitone "
+  | L_true -> " true "
+  | L_false -> " false "
+  | (L_num num) -> (pp_num num)
+  | (L_hex hex) -> (pp_hex hex)
+  | (L_bin bin) -> (pp_bin bin)
+  | L_undef -> " undefined "
+  | (L_string string) -> (pp_string string)
+
+
+let pp_fexps_aux (fexps_aux5:fexps_aux) : string =
+  match fexps_aux5 with
+  | (FES_Fexps ((fexp_list),semi_opt)) -> (String.concat ";" (List.map (fun fexp -> pp_'a fexp fexp) fexp_list)) ^ " " ^ (pp_semi_opt semi_opt)
+
+
+let pp_typschm_aux (typschm_aux5:typschm_aux) : string =
+  match typschm_aux5 with
+  | (TypSchm_ts (typquant,typ)) -> (pp_typquant typquant) ^ " " ^ (pp_typ typ)
+
+
+let pp_lit (lit5:lit) : string =
+  match lit5 with
+  | (L_aux (lit_aux,l)) -> (pp_lit_aux lit_aux) ^ " " ^ (pp_l l)
+
+
+let pp_order_aux (order_aux5:order_aux) : string =
+  match order_aux5 with
+  | (Ord_var kid) -> (pp_kid kid)
+  | Ord_inc -> " inc "
+  | Ord_dec -> " dec "
+
+
+let pp_fexps (fexps5:fexps) : string =
+  match fexps5 with
+  | (FES_aux (fexps_aux,annot)) -> (pp_fexps_aux fexps_aux) ^ " " ^ (pp_annot annot)
+
+
+let pp_typschm (typschm5:typschm) : string =
+  match typschm5 with
+  | (TypSchm_aux (typschm_aux,l)) -> (pp_typschm_aux typschm_aux) ^ " " ^ (pp_l l)
+
+
+let rec pp_pat (pat5:pat) : string =
+  match pat5 with
+  | (P_aux (pat_aux,annot)) -> (pp_pat_aux pat_aux) ^ " " ^ (pp_annot annot)
+and
+pp_pat_aux (pat_aux5:pat_aux) : string =
+  match pat_aux5 with
+  | (P_lit lit) -> (pp_lit lit)
+  | P_wild -> " _ "
+  | (P_as (pat,id)) -> " ( " ^ (pp_pat pat) ^ " as " ^ (pp_id id) ^ " ) "
+  | (P_typ (typ,pat)) -> " ( " ^ (pp_typ typ) ^ " ) " ^ (pp_pat pat)
+  | (P_id id) -> (pp_id id)
+  | (P_app (id,(pat_list))) -> (pp_id id) ^ " ( " ^ (String.concat "," (List.map (fun pat -> pp_'a pat pat) pat_list)) ^ " ) "
+  | (P_record ((fpat_list),semi_opt)) -> " { " ^ (String.concat ";" (List.map (fun fpat -> pp_'a fpat fpat) fpat_list)) ^ " " ^ (pp_semi_opt semi_opt) ^ " } "
+  | (P_vector (pat_list)) -> " [ " ^ (String.concat "," (List.map (fun pat -> pp_'a pat pat) pat_list)) ^ " ] "
+  | (P_vector_indexed (num_pat_list)) -> " [ " ^ (String.concat "," (List.map (fun num,pat -> pp_int num,pp_'a pat pat) num_pat_list)) ^ " ] "
+  | (P_vector_concat (pat_list)) -> (String.concat ":" (List.map (fun pat -> pp_'a pat pat) pat_list))
+  | (P_tup (pat_list)) -> " ( " ^ (String.concat "," (List.map (fun pat -> pp_'a pat pat) pat_list)) ^ " ) "
+  | (P_list (pat_list)) -> " [|| " ^ (String.concat "," (List.map (fun pat -> pp_'a pat pat) pat_list)) ^ " ||] "
+
+
+let pp_order (order5:order) : string =
+  match order5 with
+  | (Ord_aux (order_aux,l)) -> (pp_order_aux order_aux) ^ " " ^ (pp_l l)
+
+
+let pp_reg_id_aux (reg_id_aux5:reg_id_aux) : string =
+  match reg_id_aux5 with
+  | (RI_id id) -> (pp_id id)
+
+
+let pp_kind_aux (kind_aux5:kind_aux) : string =
+  match kind_aux5 with
+  | (K_kind (base_kind_list)) -> (String.concat "->" (List.map (fun base_kind -> pp_base_kind base_kind) base_kind_list))
+
+
+let rec pp_letbind (letbind5:letbind) : string =
+  match letbind5 with
+  | (LB_aux (letbind_aux,annot)) -> (pp_letbind_aux letbind_aux) ^ " " ^ (pp_annot annot)
+and
+pp_letbind_aux (letbind_aux5:letbind_aux) : string =
+  match letbind_aux5 with
+  | (LB_val_explicit (typschm,pat,exp)) -> " let " ^ (pp_typschm typschm) ^ " " ^ (pp_pat pat) ^ " = " ^ (pp_exp exp)
+  | (LB_val_implicit (pat,exp)) -> " let " ^ (pp_pat pat) ^ " = " ^ (pp_exp exp)
+and
+pp_opt_default (opt_default5:opt_default) : string =
+  match opt_default5 with
+  | (Def_val_aux (opt_default_aux,annot)) -> (pp_opt_default_aux opt_default_aux) ^ " " ^ (pp_annot annot)
+and
+pp_opt_default_aux (opt_default_aux5:opt_default_aux) : string =
+  match opt_default_aux5 with
+  | Def_val_empty -> 
+  | (Def_val_dec exp) -> " ; " ^ " default " ^ " = " ^ (pp_exp exp)
+and
+pp_lexp (lexp5:lexp) : string =
+  match lexp5 with
+  | (LEXP_aux (lexp_aux,annot)) -> (pp_lexp_aux lexp_aux) ^ " " ^ (pp_annot annot)
+and
+pp_lexp_aux (lexp_aux5:lexp_aux) : string =
+  match lexp_aux5 with
+  | (LEXP_id id) -> (pp_id id)
+  | (LEXP_memory (id,(exp_list))) -> (pp_id id) ^ " ( " ^ (String.concat "," (List.map (fun exp -> pp_'a exp exp) exp_list)) ^ " ) "
+  | (LEXP_cast (typ,id)) -> " ( " ^ (pp_typ typ) ^ " ) " ^ (pp_id id)
+  | (LEXP_vector (lexp,exp)) -> (pp_lexp lexp) ^ " [ " ^ (pp_exp exp) ^ " ] "
+  | (LEXP_vector_range (lexp,exp1,exp2)) -> (pp_lexp lexp) ^ " [ " ^ (pp_exp exp1) ^ " .. " ^ (pp_exp exp2) ^ " ] "
+  | (LEXP_field (lexp,id)) -> (pp_lexp lexp) ^ " . " ^ (pp_id id)
+and
+pp_exp (exp5:exp) : string =
+  match exp5 with
+  | (E_aux (exp_aux,annot)) -> (pp_exp_aux exp_aux) ^ " " ^ (pp_annot annot)
+and
+pp_exp_aux (exp_aux5:exp_aux) : string =
+  match exp_aux5 with
+  | (E_block (exp_list)) -> " { " ^ (String.concat ";" (List.map (fun exp -> pp_'a exp exp) exp_list)) ^ " } "
+  | (E_nondet (exp_list)) -> " nondet " ^ " { " ^ (String.concat ";" (List.map (fun exp -> pp_'a exp exp) exp_list)) ^ " } "
+  | (E_id id) -> (pp_id id)
+  | (E_lit lit) -> (pp_lit lit)
+  | (E_cast (typ,exp)) -> " ( " ^ (pp_typ typ) ^ " ) " ^ (pp_exp exp)
+  | (E_app (id,(exp_list))) -> (pp_id id) ^ " ( " ^ (String.concat "," (List.map (fun exp -> pp_'a exp exp) exp_list)) ^ " ) "
+  | (E_app_infix (exp1,id,exp2)) -> (pp_exp exp1) ^ " " ^ (pp_id id) ^ " " ^ (pp_exp exp2)
+  | (E_tuple (exp_list)) -> " ( " ^ (String.concat "," (List.map (fun exp -> pp_'a exp exp) exp_list)) ^ " ) "
+  | (E_if (exp1,exp2,exp3)) -> " if " ^ (pp_exp exp1) ^ " then " ^ (pp_exp exp2) ^ " else " ^ (pp_exp exp3)
+  | (E_for (id,exp1,exp2,exp3,order,exp4)) -> " foreach " ^ " ( " ^ (pp_id id) ^ " from " ^ (pp_exp exp1) ^ " to " ^ (pp_exp exp2) ^ " by " ^ (pp_exp exp3) ^ " in " ^ (pp_order order) ^ " ) " ^ (pp_exp exp4)
+  | (E_vector (exp_list)) -> " [ " ^ (String.concat "," (List.map (fun exp -> pp_'a exp exp) exp_list)) ^ " ] "
+  | (E_vector_indexed ((num_exp_list),opt_default)) -> " [ " ^ (String.concat "," (List.map (fun num,exp -> pp_int num,pp_'a exp exp) num_exp_list)) ^ " " ^ (pp_opt_default opt_default) ^ " ] "
+  | (E_vector_access (exp,exp')) -> (pp_exp exp) ^ " [ " ^ (pp_exp exp') ^ " ] "
+  | (E_vector_subrange (exp,exp1,exp2)) -> (pp_exp exp) ^ " [ " ^ (pp_exp exp1) ^ " .. " ^ (pp_exp exp2) ^ " ] "
+  | (E_vector_update (exp,exp1,exp2)) -> " [ " ^ (pp_exp exp) ^ " with " ^ (pp_exp exp1) ^ " = " ^ (pp_exp exp2) ^ " ] "
+  | (E_vector_update_subrange (exp,exp1,exp2,exp3)) -> " [ " ^ (pp_exp exp) ^ " with " ^ (pp_exp exp1) ^ " : " ^ (pp_exp exp2) ^ " = " ^ (pp_exp exp3) ^ " ] "
+  | (E_vector_append (exp,exp2)) -> (pp_exp exp) ^ " : " ^ (pp_exp exp2)
+  | (E_list (exp_list)) -> " [|| " ^ (String.concat "," (List.map (fun exp -> pp_'a exp exp) exp_list)) ^ " ||] "
+  | (E_cons (exp1,exp2)) -> (pp_exp exp1) ^ " :: " ^ (pp_exp exp2)
+  | (E_record fexps) -> " { " ^ (pp_fexps fexps) ^ " } "
+  | (E_record_update (exp,fexps)) -> " { " ^ (pp_exp exp) ^ " with " ^ (pp_fexps fexps) ^ " } "
+  | (E_field (exp,id)) -> (pp_exp exp) ^ " . " ^ (pp_id id)
+  | (E_case (exp,(pexp_list))) -> " switch " ^ (pp_exp exp) ^ " { " ^ (String.concat " " (List.map (fun pexp -> pp_'a pexp pexp) pexp_list)) ^ " } "
+  | (E_let (letbind,exp)) -> (pp_letbind letbind) ^ " in " ^ (pp_exp exp)
+  | (E_assign (lexp,exp)) -> (pp_lexp lexp) ^ " := " ^ (pp_exp exp)
+  | (E_exit exp) -> " exit " ^ (pp_exp exp)
+  | (E_internal_cast (annot,exp)) -> " ( " ^ (pp_annot annot) ^ " ) " ^ (pp_exp exp)
+  | (E_internal_exp annot) -> (pp_annot annot)
+  | (E_internal_exp_user (annot,annot')) -> (pp_annot annot) ^ " , " ^ (pp_annot annot')
+
+
+let pp_reg_id (reg_id5:reg_id) : string =
+  match reg_id5 with
+  | (RI_aux (reg_id_aux,annot)) -> (pp_reg_id_aux reg_id_aux) ^ " " ^ (pp_annot annot)
+
+
+let rec pp_nexp (nexp5:nexp) : string =
+  match nexp5 with
+  | (Nexp_aux (nexp_aux,l)) -> (pp_nexp_aux nexp_aux) ^ " " ^ (pp_l l)
+and
+pp_nexp_aux (nexp_aux5:nexp_aux) : string =
+  match nexp_aux5 with
+  | (Nexp_var kid) -> (pp_kid kid)
+  | (Nexp_constant num) -> (pp_num num)
+  | (Nexp_times (nexp1,nexp2)) -> (pp_nexp nexp1) ^ " * " ^ (pp_nexp nexp2)
+  | (Nexp_sum (nexp1,nexp2)) -> (pp_nexp nexp1) ^ " + " ^ (pp_nexp nexp2)
+  | (Nexp_minus (nexp1,nexp2)) -> (pp_nexp nexp1) ^ " - " ^ (pp_nexp nexp2)
+  | (Nexp_exp nexp) -> " 2** " ^ (pp_nexp nexp)
+  | (Nexp_neg nexp) -> " neg " ^ (pp_nexp nexp)
+
+
+let pp_kind (kind5:kind) : string =
+  match kind5 with
+  | (K_aux (kind_aux,l)) -> (pp_kind_aux kind_aux) ^ " " ^ (pp_l l)
+
+
+let pp_type_union_aux (type_union_aux5:type_union_aux) : string =
+  match type_union_aux5 with
+  | (Tu_id id) -> (pp_id id)
+  | (Tu_ty_id (typ,id)) -> (pp_typ typ) ^ " " ^ (pp_id id)
+
+
+let pp_effect_opt_aux (effect_opt_aux5:effect_opt_aux) : string =
+  match effect_opt_aux5 with
+  | Effect_opt_pure -> 
+  | (Effect_opt_effect effect) -> " effectkw " ^ (pp_effect effect)
+
+
+let pp_name_scm_opt_aux (name_scm_opt_aux5:name_scm_opt_aux) : string =
+  match name_scm_opt_aux5 with
+  | Name_sect_none -> 
+  | (Name_sect_some regexp) -> " [ " ^ " name " ^ " = " ^ (pp_regexp regexp) ^ " ] "
+
+
+let pp_funcl_aux (funcl_aux5:funcl_aux) : string =
+  match funcl_aux5 with
+  | (FCL_Funcl (id,pat,exp)) -> (pp_id id) ^ " " ^ (pp_pat pat) ^ " = " ^ (pp_exp exp)
+
+
+let pp_rec_opt_aux (rec_opt_aux5:rec_opt_aux) : string =
+  match rec_opt_aux5 with
+  | Rec_nonrec -> 
+  | Rec_rec -> " rec "
+
+
+let pp_tannot_opt_aux (tannot_opt_aux5:tannot_opt_aux) : string =
+  match tannot_opt_aux5 with
+  | (Typ_annot_opt_some (typquant,typ)) -> (pp_typquant typquant) ^ " " ^ (pp_typ typ)
+
+
+let pp_alias_spec_aux (alias_spec_aux5:alias_spec_aux) : string =
+  match alias_spec_aux5 with
+  | (AL_subreg (reg_id,id)) -> (pp_reg_id reg_id) ^ " . " ^ (pp_id id)
+  | (AL_bit (reg_id,exp)) -> (pp_reg_id reg_id) ^ " [ " ^ (pp_exp exp) ^ " ] "
+  | (AL_slice (reg_id,exp,exp')) -> (pp_reg_id reg_id) ^ " [ " ^ (pp_exp exp) ^ " .. " ^ (pp_exp exp') ^ " ] "
+  | (AL_concat (reg_id,reg_id')) -> (pp_reg_id reg_id) ^ " : " ^ (pp_reg_id reg_id')
+
+
+let pp_base_kind_aux (base_kind_aux5:base_kind_aux) : string =
+  match base_kind_aux5 with
+  | BK_type -> " Type "
+  | BK_nat -> " Nat "
+  | BK_order -> " Order "
+  | BK_effect -> " Effect "
+
+
+let pp_n_constraint_aux (n_constraint_aux5:n_constraint_aux) : string =
+  match n_constraint_aux5 with
+  | (NC_fixed (nexp,nexp')) -> (pp_nexp nexp) ^ " = " ^ (pp_nexp nexp')
+  | (NC_bounded_ge (nexp,nexp')) -> (pp_nexp nexp) ^ " >= " ^ (pp_nexp nexp')
+  | (NC_bounded_le (nexp,nexp')) -> (pp_nexp nexp) ^ " <= " ^ (pp_nexp nexp')
+  | (NC_nat_set_bounded (kid,(num_list))) -> (pp_kid kid) ^ " IN " ^ " { " ^ (String.concat "," (List.map (fun num -> pp_int num) num_list)) ^ " } "
+
+
+let pp_kinded_id_aux (kinded_id_aux5:kinded_id_aux) : string =
+  match kinded_id_aux5 with
+  | (KOpt_none kid) -> (pp_kid kid)
+  | (KOpt_kind (kind,kid)) -> (pp_kind kind) ^ " " ^ (pp_kid kid)
+
+
+let pp_type_union (type_union5:type_union) : string =
+  match type_union5 with
+  | (Tu_aux (type_union_aux,l)) -> (pp_type_union_aux type_union_aux) ^ " " ^ (pp_l l)
+
+
+let pp_effect_opt (effect_opt5:effect_opt) : string =
+  match effect_opt5 with
+  | (Effect_opt_aux (effect_opt_aux,l)) -> (pp_effect_opt_aux effect_opt_aux) ^ " " ^ (pp_l l)
+
+
+let pp_name_scm_opt (name_scm_opt5:name_scm_opt) : string =
+  match name_scm_opt5 with
+  | (Name_sect_aux (name_scm_opt_aux,l)) -> (pp_name_scm_opt_aux name_scm_opt_aux) ^ " " ^ (pp_l l)
+
+
+let pp_funcl (funcl5:funcl) : string =
+  match funcl5 with
+  | (FCL_aux (funcl_aux,annot)) -> (pp_funcl_aux funcl_aux) ^ " " ^ (pp_annot annot)
+
+
+let pp_rec_opt (rec_opt5:rec_opt) : string =
+  match rec_opt5 with
+  | (Rec_aux (rec_opt_aux,l)) -> (pp_rec_opt_aux rec_opt_aux) ^ " " ^ (pp_l l)
+
+
+let pp_tannot_opt (tannot_opt5:tannot_opt) : string =
+  match tannot_opt5 with
+  | (Typ_annot_opt_aux (tannot_opt_aux,l)) -> (pp_tannot_opt_aux tannot_opt_aux) ^ " " ^ (pp_l l)
+
+
+let pp_alias_spec (alias_spec5:alias_spec) : string =
+  match alias_spec5 with
+  | (AL_aux (alias_spec_aux,annot)) -> (pp_alias_spec_aux alias_spec_aux) ^ " " ^ (pp_annot annot)
+
+
+let pp_base_kind (base_kind5:base_kind) : string =
+  match base_kind5 with
+  | (BK_aux (base_kind_aux,l)) -> (pp_base_kind_aux base_kind_aux) ^ " " ^ (pp_l l)
+
+
+let pp_n_constraint (n_constraint5:n_constraint) : string =
+  match n_constraint5 with
+  | (NC_aux (n_constraint_aux,l)) -> (pp_n_constraint_aux n_constraint_aux) ^ " " ^ (pp_l l)
+
+
+let pp_kinded_id (kinded_id5:kinded_id) : string =
+  match kinded_id5 with
+  | (KOpt_aux (kinded_id_aux,l)) -> (pp_kinded_id_aux kinded_id_aux) ^ " " ^ (pp_l l)
+
+
+let pp_scattered_def_aux (scattered_def_aux5:scattered_def_aux) : string =
+  match scattered_def_aux5 with
+  | (SD_scattered_function (rec_opt,tannot_opt,effect_opt,id)) -> " scattered " ^ " function " ^ (pp_rec_opt rec_opt) ^ " " ^ (pp_tannot_opt tannot_opt) ^ " " ^ (pp_effect_opt effect_opt) ^ " " ^ (pp_id id)
+  | (SD_scattered_funcl funcl) -> " function " ^ " clause " ^ (pp_funcl funcl)
+  | (SD_scattered_variant (id,name_scm_opt,typquant)) -> " scattered " ^ " typedef " ^ (pp_id id) ^ " " ^ (pp_name_scm_opt name_scm_opt) ^ " = " ^ " const " ^ " union " ^ (pp_typquant typquant)
+  | (SD_scattered_unioncl (id,type_union)) -> " union " ^ (pp_id id) ^ " member " ^ (pp_type_union type_union)
+  | (SD_scattered_end id) -> " end " ^ (pp_id id)
+
+
+let pp_type_def_aux (type_def_aux5:type_def_aux) : string =
+  match type_def_aux5 with
+  | (TD_abbrev (id,name_scm_opt,typschm)) -> " typedef " ^ (pp_id id) ^ " " ^ (pp_name_scm_opt name_scm_opt) ^ " = " ^ (pp_typschm typschm)
+  | (TD_record (id,name_scm_opt,typquant,(typ_id_list),semi_opt)) -> " typedef " ^ (pp_id id) ^ " " ^ (pp_name_scm_opt name_scm_opt) ^ " = " ^ " const " ^ " struct " ^ (pp_typquant typquant) ^ " { " ^ (String.concat ";" (List.map (fun typ,id -> pp_typ typ;pp_id id) typ_id_list)) ^ " " ^ (pp_semi_opt semi_opt) ^ " } "
+  | (TD_variant (id,name_scm_opt,typquant,(type_union_list),semi_opt)) -> " typedef " ^ (pp_id id) ^ " " ^ (pp_name_scm_opt name_scm_opt) ^ " = " ^ " const " ^ " union " ^ (pp_typquant typquant) ^ " { " ^ (String.concat ";" (List.map (fun type_union -> pp_type_union type_union) type_union_list)) ^ " " ^ (pp_semi_opt semi_opt) ^ " } "
+  | (TD_enum (id,name_scm_opt,(id_list),semi_opt)) -> " typedef " ^ (pp_id id) ^ " " ^ (pp_name_scm_opt name_scm_opt) ^ " = " ^ " enumerate " ^ " { " ^ (String.concat ";" (List.map (fun id -> pp_id id) id_list)) ^ " " ^ (pp_semi_opt semi_opt) ^ " } "
+  | (TD_register (id,nexp,nexp',(index_range_id_list))) -> " typedef " ^ (pp_id id) ^ " = " ^ " register " ^ " bits " ^ " [ " ^ (pp_nexp nexp) ^ " : " ^ (pp_nexp nexp') ^ " ] " ^ " { " ^ (String.concat ";" (List.map (fun index_range,id -> pp_index_range index_range;pp_id id) index_range_id_list)) ^ " } "
+
+
+let pp_fundef_aux (fundef_aux5:fundef_aux) : string =
+  match fundef_aux5 with
+  | (FD_function (rec_opt,tannot_opt,effect_opt,(funcl_list))) -> " function " ^ (pp_rec_opt rec_opt) ^ " " ^ (pp_tannot_opt tannot_opt) ^ " " ^ (pp_effect_opt effect_opt) ^ (String.concat "and" (List.map (fun funcl -> pp_'a funcl funcl) funcl_list))
+
+
+let pp_val_spec_aux (val_spec_aux5:val_spec_aux) : string =
+  match val_spec_aux5 with
+  | (VS_val_spec (typschm,id)) -> " val " ^ (pp_typschm typschm) ^ " " ^ (pp_id id)
+  | (VS_extern_no_rename (typschm,id)) -> " val " ^ " extern " ^ (pp_typschm typschm) ^ " " ^ (pp_id id)
+  | (VS_extern_spec (typschm,id,string)) -> " val " ^ " extern " ^ (pp_typschm typschm) ^ " " ^ (pp_id id) ^ " = " ^ (pp_string string)
+
+
+let pp_dec_spec_aux (dec_spec_aux5:dec_spec_aux) : string =
+  match dec_spec_aux5 with
+  | (DEC_reg (typ,id)) -> " register " ^ (pp_typ typ) ^ " " ^ (pp_id id)
+  | (DEC_alias (id,alias_spec)) -> " register " ^ " alias " ^ (pp_id id) ^ " = " ^ (pp_alias_spec alias_spec)
+  | (DEC_typ_alias (typ,id,alias_spec)) -> " register " ^ " alias " ^ (pp_typ typ) ^ " " ^ (pp_id id) ^ " = " ^ (pp_alias_spec alias_spec)
+
+
+let pp_default_spec_aux (default_spec_aux5:default_spec_aux) : string =
+  match default_spec_aux5 with
+  | (DT_kind (base_kind,kid)) -> " default " ^ (pp_base_kind base_kind) ^ " " ^ (pp_kid kid)
+  | (DT_order order) -> " default " ^ " Order " ^ (pp_order order)
+  | (DT_typ (typschm,id)) -> " default " ^ (pp_typschm typschm) ^ " " ^ (pp_id id)
+
+
+let pp_base_effect_aux (base_effect_aux5:base_effect_aux) : string =
+  match base_effect_aux5 with
+  | BE_rreg -> " rreg "
+  | BE_wreg -> " wreg "
+  | BE_rmem -> " rmem "
+  | BE_wmem -> " wmem "
+  | BE_barr -> " barr "
+  | BE_undef -> " undef "
+  | BE_unspec -> " unspec "
+  | BE_nondet -> " nondet "
+
+
+let pp_quant_item_aux (quant_item_aux5:quant_item_aux) : string =
+  match quant_item_aux5 with
+  | (QI_id kinded_id) -> (pp_kinded_id kinded_id)
+  | (QI_const n_constraint) -> (pp_n_constraint n_constraint)
+
+
+let pp_fexp_aux (fexp_aux5:fexp_aux) : string =
+  match fexp_aux5 with
+  | (FE_Fexp (id,exp)) -> (pp_id id) ^ " = " ^ (pp_exp exp)
+
+
+let pp_fpat_aux (fpat_aux5:fpat_aux) : string =
+  match fpat_aux5 with
+  | (FP_Fpat (id,pat)) -> (pp_id id) ^ " = " ^ (pp_pat pat)
+
+
+let pp_scattered_def (scattered_def5:scattered_def) : string =
+  match scattered_def5 with
+  | (SD_aux (scattered_def_aux,annot)) -> (pp_scattered_def_aux scattered_def_aux) ^ " " ^ (pp_annot annot)
+
+
+let pp_type_def (type_def5:type_def) : string =
+  match type_def5 with
+  | (TD_aux (type_def_aux,annot)) -> (pp_type_def_aux type_def_aux) ^ " " ^ (pp_annot annot)
+
+
+let pp_fundef (fundef5:fundef) : string =
+  match fundef5 with
+  | (FD_aux (fundef_aux,annot)) -> (pp_fundef_aux fundef_aux) ^ " " ^ (pp_annot annot)
+
+
+let pp_val_spec (val_spec5:val_spec) : string =
+  match val_spec5 with
+  | (VS_aux (val_spec_aux,annot)) -> (pp_val_spec_aux val_spec_aux) ^ " " ^ (pp_annot annot)
+
+
+let pp_dec_spec (dec_spec5:dec_spec) : string =
+  match dec_spec5 with
+  | (DEC_aux (dec_spec_aux,annot)) -> (pp_dec_spec_aux dec_spec_aux) ^ " " ^ (pp_annot annot)
+
+
+let pp_default_spec (default_spec5:default_spec) : string =
+  match default_spec5 with
+  | (DT_aux (default_spec_aux,l)) -> (pp_default_spec_aux default_spec_aux) ^ " " ^ (pp_l l)
+
+
+let pp_pexp_aux (pexp_aux5:pexp_aux) : string =
+  match pexp_aux5 with
+  | (Pat_exp (pat,exp)) -> (pp_pat pat) ^ " -> " ^ (pp_exp exp)
+
+
+let pp_typ_arg_aux (typ_arg_aux5:typ_arg_aux) : string =
+  match typ_arg_aux5 with
+  | (Typ_arg_nexp nexp) -> (pp_nexp nexp)
+  | (Typ_arg_typ typ) -> (pp_typ typ)
+  | (Typ_arg_order order) -> (pp_order order)
+  | (Typ_arg_effect effect) -> (pp_effect effect)
+
+
+let pp_ix (ix5:ix) : string = ix5
+
+let pp_base_effect (base_effect5:base_effect) : string =
+  match base_effect5 with
+  | (BE_aux (base_effect_aux,l)) -> (pp_base_effect_aux base_effect_aux) ^ " " ^ (pp_l l)
+
+
+let pp_quant_item (quant_item5:quant_item) : string =
+  match quant_item5 with
+  | (QI_aux (quant_item_aux,l)) -> (pp_quant_item_aux quant_item_aux) ^ " " ^ (pp_l l)
+
+
+let pp_fexp (fexp5:fexp) : string =
+  match fexp5 with
+  | (FE_aux (fexp_aux,annot)) -> (pp_fexp_aux fexp_aux) ^ " " ^ (pp_annot annot)
+
+
+let pp_fpat (fpat5:fpat) : string =
+  match fpat5 with
+  | (FP_aux (fpat_aux,annot)) -> (pp_fpat_aux fpat_aux) ^ " " ^ (pp_annot annot)
+
+
+let pp_defs (defs5:defs) : string =
+  match defs5 with
+  | (Defs (def_list)) -> (String.concat " " (List.map (fun def -> pp_'a def def) def_list))
+
+
+let pp_def (def5:def) : string =
+  match def5 with
+  | (DEF_type type_def) -> (pp_type_def type_def)
+  | (DEF_fundef fundef) -> (pp_fundef fundef)
+  | (DEF_val letbind) -> (pp_letbind letbind)
+  | (DEF_spec val_spec) -> (pp_val_spec val_spec)
+  | (DEF_default default_spec) -> (pp_default_spec default_spec)
+  | (DEF_scattered scattered_def) -> (pp_scattered_def scattered_def)
+  | (DEF_reg_dec dec_spec) -> (pp_dec_spec dec_spec)
+
+
+let pp_pexp (pexp5:pexp) : string =
+  match pexp5 with
+  | (Pat_aux (pexp_aux,annot)) -> (pp_pexp_aux pexp_aux) ^ " " ^ (pp_annot annot)
+
+
+let pp_typ_arg (typ_arg5:typ_arg) : string =
+  match typ_arg5 with
+  | (Typ_arg_aux (typ_arg_aux,l)) -> (pp_typ_arg_aux typ_arg_aux) ^ " " ^ (pp_l l)
+
+
+let rec pp_index_range (index_range5:index_range) : string =
+  match index_range5 with
+  | (BF_aux (index_range_aux,l)) -> (pp_index_range_aux index_range_aux) ^ " " ^ (pp_l l)
+and
+pp_index_range_aux (index_range_aux5:index_range_aux) : string =
+  match index_range_aux5 with
+  | (BF_single num) -> (pp_num num)
+  | (BF_range (num1,num2)) -> (pp_num num1) ^ " .. " ^ (pp_num num2)
+  | (BF_concat (index_range1,index_range2)) -> (pp_index_range index_range1) ^ " , " ^ (pp_index_range index_range2)
+
+
 
 type 
 n_constraint_aux =  (* constraint over kind $_$ *)
@@ -497,5 +1019,527 @@ type
 'a defs =  (* Definition sequence *)
    Defs of ('a def) list
 
+(** pretty printer *)
+let pp_x (y5:x) : string = y5
+
+let pp_kid_aux (kid_aux5:kid_aux) : string =
+  match kid_aux5 with
+  | (Var x) -> " ' " ^ (pp_x x)
+
+
+let pp_kid (kid5:kid) : string =
+  match kid5 with
+  | (Kid_aux (kid_aux,l)) -> (pp_kid_aux kid_aux) ^ " " ^ (pp_l l)
+
+
+let pp_id_aux (id_aux5:id_aux) : string =
+  match id_aux5 with
+  | (Id x) -> (pp_x x)
+  | (DeIid x) -> " ( " ^ " deinfix " ^ (pp_x x) ^ " ) "
+
+
+let pp_effect_aux (effect_aux5:effect_aux) : string =
+  match effect_aux5 with
+  | (Effect_var kid) -> (pp_kid kid)
+  | (Effect_set (base_effect_list)) -> " { " ^ (String.concat "," (List.map (fun base_effect -> pp_base_effect base_effect) base_effect_list)) ^ " } "
+
+
+let pp_typquant_aux (typquant_aux5:typquant_aux) : string =
+  match typquant_aux5 with
+  | (TypQ_tq (quant_item_list)) -> " forall " ^ (String.concat "," (List.map (fun quant_item -> pp_quant_item quant_item) quant_item_list)) ^ " . "
+  | TypQ_no_forall -> 
+
+
+let pp_id (id5:id) : string =
+  match id5 with
+  | (Id_aux (id_aux,l)) -> (pp_id_aux id_aux) ^ " " ^ (pp_l l)
+
+
+let pp_effect (effect5:effect) : string =
+  match effect5 with
+  | (Effect_aux (effect_aux,l)) -> (pp_effect_aux effect_aux) ^ " " ^ (pp_l l)
+
+
+let pp_typquant (typquant5:typquant) : string =
+  match typquant5 with
+  | (TypQ_aux (typquant_aux,l)) -> (pp_typquant_aux typquant_aux) ^ " " ^ (pp_l l)
+
+
+let rec pp_typ (typ5:typ) : string =
+  match typ5 with
+  | (Typ_aux (typ_aux,l)) -> (pp_typ_aux typ_aux) ^ " " ^ (pp_l l)
+and
+pp_typ_aux (typ_aux5:typ_aux) : string =
+  match typ_aux5 with
+  | Typ_wild -> " _ "
+  | (Typ_id id) -> (pp_id id)
+  | (Typ_var kid) -> (pp_kid kid)
+  | (Typ_fn (typ1,typ2,effect)) -> (pp_typ typ1) ^ " -> " ^ (pp_typ typ2) ^ " effectkw " ^ (pp_effect effect)
+  | (Typ_tup (typ_list)) -> " ( " ^ (String.concat "," (List.map (fun typ -> pp_typ typ) typ_list)) ^ " ) "
+  | (Typ_app (id,(typ_arg_list))) -> (pp_id id) ^ " < " ^ (String.concat "," (List.map (fun typ_arg -> pp_typ_arg typ_arg) typ_arg_list)) ^ " > "
+
+
+let pp_lit_aux (lit_aux5:lit_aux) : string =
+  match lit_aux5 with
+  | L_unit -> " ( " ^ " ) "
+  | L_zero -> " bitzero "
+  | L_one -> " bitone "
+  | L_true -> " true "
+  | L_false -> " false "
+  | (L_num num) -> (pp_num num)
+  | (L_hex hex) -> (pp_hex hex)
+  | (L_bin bin) -> (pp_bin bin)
+  | L_undef -> " undefined "
+  | (L_string string) -> (pp_string string)
+
+
+let pp_fexps_aux (fexps_aux5:fexps_aux) : string =
+  match fexps_aux5 with
+  | (FES_Fexps ((fexp_list),semi_opt)) -> (String.concat ";" (List.map (fun fexp -> pp_'a fexp fexp) fexp_list)) ^ " " ^ (pp_semi_opt semi_opt)
+
+
+let pp_order_aux (order_aux5:order_aux) : string =
+  match order_aux5 with
+  | (Ord_var kid) -> (pp_kid kid)
+  | Ord_inc -> " inc "
+  | Ord_dec -> " dec "
+
+
+let pp_typschm_aux (typschm_aux5:typschm_aux) : string =
+  match typschm_aux5 with
+  | (TypSchm_ts (typquant,typ)) -> (pp_typquant typquant) ^ " " ^ (pp_typ typ)
+
+
+let pp_lit (lit5:lit) : string =
+  match lit5 with
+  | (L_aux (lit_aux,l)) -> (pp_lit_aux lit_aux) ^ " " ^ (pp_l l)
+
+
+let pp_reg_id_aux (reg_id_aux5:reg_id_aux) : string =
+  match reg_id_aux5 with
+  | (RI_id id) -> (pp_id id)
+
+
+let pp_fexps (fexps5:fexps) : string =
+  match fexps5 with
+  | (FES_aux (fexps_aux,annot)) -> (pp_fexps_aux fexps_aux) ^ " " ^ (pp_annot annot)
+
+
+let pp_order (order5:order) : string =
+  match order5 with
+  | (Ord_aux (order_aux,l)) -> (pp_order_aux order_aux) ^ " " ^ (pp_l l)
+
+
+let pp_typschm (typschm5:typschm) : string =
+  match typschm5 with
+  | (TypSchm_aux (typschm_aux,l)) -> (pp_typschm_aux typschm_aux) ^ " " ^ (pp_l l)
+
+
+let rec pp_pat (pat5:pat) : string =
+  match pat5 with
+  | (P_aux (pat_aux,annot)) -> (pp_pat_aux pat_aux) ^ " " ^ (pp_annot annot)
+and
+pp_pat_aux (pat_aux5:pat_aux) : string =
+  match pat_aux5 with
+  | (P_lit lit) -> (pp_lit lit)
+  | P_wild -> " _ "
+  | (P_as (pat,id)) -> " ( " ^ (pp_pat pat) ^ " as " ^ (pp_id id) ^ " ) "
+  | (P_typ (typ,pat)) -> " ( " ^ (pp_typ typ) ^ " ) " ^ (pp_pat pat)
+  | (P_id id) -> (pp_id id)
+  | (P_app (id,(pat_list))) -> (pp_id id) ^ " ( " ^ (String.concat "," (List.map (fun pat -> pp_'a pat pat) pat_list)) ^ " ) "
+  | (P_record ((fpat_list),semi_opt)) -> " { " ^ (String.concat ";" (List.map (fun fpat -> pp_'a fpat fpat) fpat_list)) ^ " " ^ (pp_semi_opt semi_opt) ^ " } "
+  | (P_vector (pat_list)) -> " [ " ^ (String.concat "," (List.map (fun pat -> pp_'a pat pat) pat_list)) ^ " ] "
+  | (P_vector_indexed (num_pat_list)) -> " [ " ^ (String.concat "," (List.map (fun num,pat -> pp_int num,pp_'a pat pat) num_pat_list)) ^ " ] "
+  | (P_vector_concat (pat_list)) -> (String.concat ":" (List.map (fun pat -> pp_'a pat pat) pat_list))
+  | (P_tup (pat_list)) -> " ( " ^ (String.concat "," (List.map (fun pat -> pp_'a pat pat) pat_list)) ^ " ) "
+  | (P_list (pat_list)) -> " [|| " ^ (String.concat "," (List.map (fun pat -> pp_'a pat pat) pat_list)) ^ " ||] "
+
+
+let pp_kind_aux (kind_aux5:kind_aux) : string =
+  match kind_aux5 with
+  | (K_kind (base_kind_list)) -> (String.concat "->" (List.map (fun base_kind -> pp_base_kind base_kind) base_kind_list))
+
+
+let pp_reg_id (reg_id5:reg_id) : string =
+  match reg_id5 with
+  | (RI_aux (reg_id_aux,annot)) -> (pp_reg_id_aux reg_id_aux) ^ " " ^ (pp_annot annot)
+
+
+let rec pp_letbind (letbind5:letbind) : string =
+  match letbind5 with
+  | (LB_aux (letbind_aux,annot)) -> (pp_letbind_aux letbind_aux) ^ " " ^ (pp_annot annot)
+and
+pp_letbind_aux (letbind_aux5:letbind_aux) : string =
+  match letbind_aux5 with
+  | (LB_val_explicit (typschm,pat,exp)) -> " let " ^ (pp_typschm typschm) ^ " " ^ (pp_pat pat) ^ " = " ^ (pp_exp exp)
+  | (LB_val_implicit (pat,exp)) -> " let " ^ (pp_pat pat) ^ " = " ^ (pp_exp exp)
+and
+pp_opt_default (opt_default5:opt_default) : string =
+  match opt_default5 with
+  | (Def_val_aux (opt_default_aux,annot)) -> (pp_opt_default_aux opt_default_aux) ^ " " ^ (pp_annot annot)
+and
+pp_opt_default_aux (opt_default_aux5:opt_default_aux) : string =
+  match opt_default_aux5 with
+  | Def_val_empty -> 
+  | (Def_val_dec exp) -> " ; " ^ " default " ^ " = " ^ (pp_exp exp)
+and
+pp_lexp (lexp5:lexp) : string =
+  match lexp5 with
+  | (LEXP_aux (lexp_aux,annot)) -> (pp_lexp_aux lexp_aux) ^ " " ^ (pp_annot annot)
+and
+pp_lexp_aux (lexp_aux5:lexp_aux) : string =
+  match lexp_aux5 with
+  | (LEXP_id id) -> (pp_id id)
+  | (LEXP_memory (id,(exp_list))) -> (pp_id id) ^ " ( " ^ (String.concat "," (List.map (fun exp -> pp_'a exp exp) exp_list)) ^ " ) "
+  | (LEXP_cast (typ,id)) -> " ( " ^ (pp_typ typ) ^ " ) " ^ (pp_id id)
+  | (LEXP_vector (lexp,exp)) -> (pp_lexp lexp) ^ " [ " ^ (pp_exp exp) ^ " ] "
+  | (LEXP_vector_range (lexp,exp1,exp2)) -> (pp_lexp lexp) ^ " [ " ^ (pp_exp exp1) ^ " .. " ^ (pp_exp exp2) ^ " ] "
+  | (LEXP_field (lexp,id)) -> (pp_lexp lexp) ^ " . " ^ (pp_id id)
+and
+pp_exp (exp5:exp) : string =
+  match exp5 with
+  | (E_aux (exp_aux,annot)) -> (pp_exp_aux exp_aux) ^ " " ^ (pp_annot annot)
+and
+pp_exp_aux (exp_aux5:exp_aux) : string =
+  match exp_aux5 with
+  | (E_block (exp_list)) -> " { " ^ (String.concat ";" (List.map (fun exp -> pp_'a exp exp) exp_list)) ^ " } "
+  | (E_nondet (exp_list)) -> " nondet " ^ " { " ^ (String.concat ";" (List.map (fun exp -> pp_'a exp exp) exp_list)) ^ " } "
+  | (E_id id) -> (pp_id id)
+  | (E_lit lit) -> (pp_lit lit)
+  | (E_cast (typ,exp)) -> " ( " ^ (pp_typ typ) ^ " ) " ^ (pp_exp exp)
+  | (E_app (id,(exp_list))) -> (pp_id id) ^ " ( " ^ (String.concat "," (List.map (fun exp -> pp_'a exp exp) exp_list)) ^ " ) "
+  | (E_app_infix (exp1,id,exp2)) -> (pp_exp exp1) ^ " " ^ (pp_id id) ^ " " ^ (pp_exp exp2)
+  | (E_tuple (exp_list)) -> " ( " ^ (String.concat "," (List.map (fun exp -> pp_'a exp exp) exp_list)) ^ " ) "
+  | (E_if (exp1,exp2,exp3)) -> " if " ^ (pp_exp exp1) ^ " then " ^ (pp_exp exp2) ^ " else " ^ (pp_exp exp3)
+  | (E_for (id,exp1,exp2,exp3,order,exp4)) -> " foreach " ^ " ( " ^ (pp_id id) ^ " from " ^ (pp_exp exp1) ^ " to " ^ (pp_exp exp2) ^ " by " ^ (pp_exp exp3) ^ " in " ^ (pp_order order) ^ " ) " ^ (pp_exp exp4)
+  | (E_vector (exp_list)) -> " [ " ^ (String.concat "," (List.map (fun exp -> pp_'a exp exp) exp_list)) ^ " ] "
+  | (E_vector_indexed ((num_exp_list),opt_default)) -> " [ " ^ (String.concat "," (List.map (fun num,exp -> pp_int num,pp_'a exp exp) num_exp_list)) ^ " " ^ (pp_opt_default opt_default) ^ " ] "
+  | (E_vector_access (exp,exp')) -> (pp_exp exp) ^ " [ " ^ (pp_exp exp') ^ " ] "
+  | (E_vector_subrange (exp,exp1,exp2)) -> (pp_exp exp) ^ " [ " ^ (pp_exp exp1) ^ " .. " ^ (pp_exp exp2) ^ " ] "
+  | (E_vector_update (exp,exp1,exp2)) -> " [ " ^ (pp_exp exp) ^ " with " ^ (pp_exp exp1) ^ " = " ^ (pp_exp exp2) ^ " ] "
+  | (E_vector_update_subrange (exp,exp1,exp2,exp3)) -> " [ " ^ (pp_exp exp) ^ " with " ^ (pp_exp exp1) ^ " : " ^ (pp_exp exp2) ^ " = " ^ (pp_exp exp3) ^ " ] "
+  | (E_vector_append (exp,exp2)) -> (pp_exp exp) ^ " : " ^ (pp_exp exp2)
+  | (E_list (exp_list)) -> " [|| " ^ (String.concat "," (List.map (fun exp -> pp_'a exp exp) exp_list)) ^ " ||] "
+  | (E_cons (exp1,exp2)) -> (pp_exp exp1) ^ " :: " ^ (pp_exp exp2)
+  | (E_record fexps) -> " { " ^ (pp_fexps fexps) ^ " } "
+  | (E_record_update (exp,fexps)) -> " { " ^ (pp_exp exp) ^ " with " ^ (pp_fexps fexps) ^ " } "
+  | (E_field (exp,id)) -> (pp_exp exp) ^ " . " ^ (pp_id id)
+  | (E_case (exp,(pexp_list))) -> " switch " ^ (pp_exp exp) ^ " { " ^ (String.concat " " (List.map (fun pexp -> pp_'a pexp pexp) pexp_list)) ^ " } "
+  | (E_let (letbind,exp)) -> (pp_letbind letbind) ^ " in " ^ (pp_exp exp)
+  | (E_assign (lexp,exp)) -> (pp_lexp lexp) ^ " := " ^ (pp_exp exp)
+  | (E_exit exp) -> " exit " ^ (pp_exp exp)
+  | (E_internal_cast (annot,exp)) -> " ( " ^ (pp_annot annot) ^ " ) " ^ (pp_exp exp)
+  | (E_internal_exp annot) -> (pp_annot annot)
+  | (E_internal_exp_user (annot,annot')) -> (pp_annot annot) ^ " , " ^ (pp_annot annot')
+
+
+let rec pp_nexp (nexp5:nexp) : string =
+  match nexp5 with
+  | (Nexp_aux (nexp_aux,l)) -> (pp_nexp_aux nexp_aux) ^ " " ^ (pp_l l)
+and
+pp_nexp_aux (nexp_aux5:nexp_aux) : string =
+  match nexp_aux5 with
+  | (Nexp_var kid) -> (pp_kid kid)
+  | (Nexp_constant num) -> (pp_num num)
+  | (Nexp_times (nexp1,nexp2)) -> (pp_nexp nexp1) ^ " * " ^ (pp_nexp nexp2)
+  | (Nexp_sum (nexp1,nexp2)) -> (pp_nexp nexp1) ^ " + " ^ (pp_nexp nexp2)
+  | (Nexp_minus (nexp1,nexp2)) -> (pp_nexp nexp1) ^ " - " ^ (pp_nexp nexp2)
+  | (Nexp_exp nexp) -> " 2** " ^ (pp_nexp nexp)
+  | (Nexp_neg nexp) -> " neg " ^ (pp_nexp nexp)
+
+
+let pp_kind (kind5:kind) : string =
+  match kind5 with
+  | (K_aux (kind_aux,l)) -> (pp_kind_aux kind_aux) ^ " " ^ (pp_l l)
+
+
+let pp_alias_spec_aux (alias_spec_aux5:alias_spec_aux) : string =
+  match alias_spec_aux5 with
+  | (AL_subreg (reg_id,id)) -> (pp_reg_id reg_id) ^ " . " ^ (pp_id id)
+  | (AL_bit (reg_id,exp)) -> (pp_reg_id reg_id) ^ " [ " ^ (pp_exp exp) ^ " ] "
+  | (AL_slice (reg_id,exp,exp')) -> (pp_reg_id reg_id) ^ " [ " ^ (pp_exp exp) ^ " .. " ^ (pp_exp exp') ^ " ] "
+  | (AL_concat (reg_id,reg_id')) -> (pp_reg_id reg_id) ^ " : " ^ (pp_reg_id reg_id')
+
+
+let pp_name_scm_opt_aux (name_scm_opt_aux5:name_scm_opt_aux) : string =
+  match name_scm_opt_aux5 with
+  | Name_sect_none -> 
+  | (Name_sect_some regexp) -> " [ " ^ " name " ^ " = " ^ (pp_regexp regexp) ^ " ] "
+
+
+let pp_funcl_aux (funcl_aux5:funcl_aux) : string =
+  match funcl_aux5 with
+  | (FCL_Funcl (id,pat,exp)) -> (pp_id id) ^ " " ^ (pp_pat pat) ^ " = " ^ (pp_exp exp)
+
+
+let pp_effect_opt_aux (effect_opt_aux5:effect_opt_aux) : string =
+  match effect_opt_aux5 with
+  | Effect_opt_pure -> 
+  | (Effect_opt_effect effect) -> " effectkw " ^ (pp_effect effect)
+
+
+let pp_type_union_aux (type_union_aux5:type_union_aux) : string =
+  match type_union_aux5 with
+  | (Tu_id id) -> (pp_id id)
+  | (Tu_ty_id (typ,id)) -> (pp_typ typ) ^ " " ^ (pp_id id)
+
+
+let pp_tannot_opt_aux (tannot_opt_aux5:tannot_opt_aux) : string =
+  match tannot_opt_aux5 with
+  | (Typ_annot_opt_some (typquant,typ)) -> (pp_typquant typquant) ^ " " ^ (pp_typ typ)
+
+
+let pp_rec_opt_aux (rec_opt_aux5:rec_opt_aux) : string =
+  match rec_opt_aux5 with
+  | Rec_nonrec -> 
+  | Rec_rec -> " rec "
+
+
+let pp_base_kind_aux (base_kind_aux5:base_kind_aux) : string =
+  match base_kind_aux5 with
+  | BK_type -> " Type "
+  | BK_nat -> " Nat "
+  | BK_order -> " Order "
+  | BK_effect -> " Effect "
+
+
+let pp_n_constraint_aux (n_constraint_aux5:n_constraint_aux) : string =
+  match n_constraint_aux5 with
+  | (NC_fixed (nexp,nexp')) -> (pp_nexp nexp) ^ " = " ^ (pp_nexp nexp')
+  | (NC_bounded_ge (nexp,nexp')) -> (pp_nexp nexp) ^ " >= " ^ (pp_nexp nexp')
+  | (NC_bounded_le (nexp,nexp')) -> (pp_nexp nexp) ^ " <= " ^ (pp_nexp nexp')
+  | (NC_nat_set_bounded (kid,(num_list))) -> (pp_kid kid) ^ " IN " ^ " { " ^ (String.concat "," (List.map (fun num -> pp_int num) num_list)) ^ " } "
+
+
+let pp_kinded_id_aux (kinded_id_aux5:kinded_id_aux) : string =
+  match kinded_id_aux5 with
+  | (KOpt_none kid) -> (pp_kid kid)
+  | (KOpt_kind (kind,kid)) -> (pp_kind kind) ^ " " ^ (pp_kid kid)
+
+
+let pp_alias_spec (alias_spec5:alias_spec) : string =
+  match alias_spec5 with
+  | (AL_aux (alias_spec_aux,annot)) -> (pp_alias_spec_aux alias_spec_aux) ^ " " ^ (pp_annot annot)
+
+
+let pp_name_scm_opt (name_scm_opt5:name_scm_opt) : string =
+  match name_scm_opt5 with
+  | (Name_sect_aux (name_scm_opt_aux,l)) -> (pp_name_scm_opt_aux name_scm_opt_aux) ^ " " ^ (pp_l l)
+
+
+let pp_funcl (funcl5:funcl) : string =
+  match funcl5 with
+  | (FCL_aux (funcl_aux,annot)) -> (pp_funcl_aux funcl_aux) ^ " " ^ (pp_annot annot)
+
+
+let pp_effect_opt (effect_opt5:effect_opt) : string =
+  match effect_opt5 with
+  | (Effect_opt_aux (effect_opt_aux,l)) -> (pp_effect_opt_aux effect_opt_aux) ^ " " ^ (pp_l l)
+
+
+let pp_type_union (type_union5:type_union) : string =
+  match type_union5 with
+  | (Tu_aux (type_union_aux,l)) -> (pp_type_union_aux type_union_aux) ^ " " ^ (pp_l l)
+
+
+let pp_tannot_opt (tannot_opt5:tannot_opt) : string =
+  match tannot_opt5 with
+  | (Typ_annot_opt_aux (tannot_opt_aux,l)) -> (pp_tannot_opt_aux tannot_opt_aux) ^ " " ^ (pp_l l)
+
+
+let pp_rec_opt (rec_opt5:rec_opt) : string =
+  match rec_opt5 with
+  | (Rec_aux (rec_opt_aux,l)) -> (pp_rec_opt_aux rec_opt_aux) ^ " " ^ (pp_l l)
+
+
+let pp_base_kind (base_kind5:base_kind) : string =
+  match base_kind5 with
+  | (BK_aux (base_kind_aux,l)) -> (pp_base_kind_aux base_kind_aux) ^ " " ^ (pp_l l)
+
+
+let pp_n_constraint (n_constraint5:n_constraint) : string =
+  match n_constraint5 with
+  | (NC_aux (n_constraint_aux,l)) -> (pp_n_constraint_aux n_constraint_aux) ^ " " ^ (pp_l l)
+
+
+let pp_kinded_id (kinded_id5:kinded_id) : string =
+  match kinded_id5 with
+  | (KOpt_aux (kinded_id_aux,l)) -> (pp_kinded_id_aux kinded_id_aux) ^ " " ^ (pp_l l)
+
+
+let pp_dec_spec_aux (dec_spec_aux5:dec_spec_aux) : string =
+  match dec_spec_aux5 with
+  | (DEC_reg (typ,id)) -> " register " ^ (pp_typ typ) ^ " " ^ (pp_id id)
+  | (DEC_alias (id,alias_spec)) -> " register " ^ " alias " ^ (pp_id id) ^ " = " ^ (pp_alias_spec alias_spec)
+  | (DEC_typ_alias (typ,id,alias_spec)) -> " register " ^ " alias " ^ (pp_typ typ) ^ " " ^ (pp_id id) ^ " = " ^ (pp_alias_spec alias_spec)
+
+
+let pp_type_def_aux (type_def_aux5:type_def_aux) : string =
+  match type_def_aux5 with
+  | (TD_abbrev (id,name_scm_opt,typschm)) -> " typedef " ^ (pp_id id) ^ " " ^ (pp_name_scm_opt name_scm_opt) ^ " = " ^ (pp_typschm typschm)
+  | (TD_record (id,name_scm_opt,typquant,(typ_id_list),semi_opt)) -> " typedef " ^ (pp_id id) ^ " " ^ (pp_name_scm_opt name_scm_opt) ^ " = " ^ " const " ^ " struct " ^ (pp_typquant typquant) ^ " { " ^ (String.concat ";" (List.map (fun typ,id -> pp_typ typ;pp_id id) typ_id_list)) ^ " " ^ (pp_semi_opt semi_opt) ^ " } "
+  | (TD_variant (id,name_scm_opt,typquant,(type_union_list),semi_opt)) -> " typedef " ^ (pp_id id) ^ " " ^ (pp_name_scm_opt name_scm_opt) ^ " = " ^ " const " ^ " union " ^ (pp_typquant typquant) ^ " { " ^ (String.concat ";" (List.map (fun type_union -> pp_type_union type_union) type_union_list)) ^ " " ^ (pp_semi_opt semi_opt) ^ " } "
+  | (TD_enum (id,name_scm_opt,(id_list),semi_opt)) -> " typedef " ^ (pp_id id) ^ " " ^ (pp_name_scm_opt name_scm_opt) ^ " = " ^ " enumerate " ^ " { " ^ (String.concat ";" (List.map (fun id -> pp_id id) id_list)) ^ " " ^ (pp_semi_opt semi_opt) ^ " } "
+  | (TD_register (id,nexp,nexp',(index_range_id_list))) -> " typedef " ^ (pp_id id) ^ " = " ^ " register " ^ " bits " ^ " [ " ^ (pp_nexp nexp) ^ " : " ^ (pp_nexp nexp') ^ " ] " ^ " { " ^ (String.concat ";" (List.map (fun index_range,id -> pp_index_range index_range;pp_id id) index_range_id_list)) ^ " } "
+
+
+let pp_scattered_def_aux (scattered_def_aux5:scattered_def_aux) : string =
+  match scattered_def_aux5 with
+  | (SD_scattered_function (rec_opt,tannot_opt,effect_opt,id)) -> " scattered " ^ " function " ^ (pp_rec_opt rec_opt) ^ " " ^ (pp_tannot_opt tannot_opt) ^ " " ^ (pp_effect_opt effect_opt) ^ " " ^ (pp_id id)
+  | (SD_scattered_funcl funcl) -> " function " ^ " clause " ^ (pp_funcl funcl)
+  | (SD_scattered_variant (id,name_scm_opt,typquant)) -> " scattered " ^ " typedef " ^ (pp_id id) ^ " " ^ (pp_name_scm_opt name_scm_opt) ^ " = " ^ " const " ^ " union " ^ (pp_typquant typquant)
+  | (SD_scattered_unioncl (id,type_union)) -> " union " ^ (pp_id id) ^ " member " ^ (pp_type_union type_union)
+  | (SD_scattered_end id) -> " end " ^ (pp_id id)
+
+
+let pp_fundef_aux (fundef_aux5:fundef_aux) : string =
+  match fundef_aux5 with
+  | (FD_function (rec_opt,tannot_opt,effect_opt,(funcl_list))) -> " function " ^ (pp_rec_opt rec_opt) ^ " " ^ (pp_tannot_opt tannot_opt) ^ " " ^ (pp_effect_opt effect_opt) ^ (String.concat "and" (List.map (fun funcl -> pp_'a funcl funcl) funcl_list))
+
+
+let pp_default_spec_aux (default_spec_aux5:default_spec_aux) : string =
+  match default_spec_aux5 with
+  | (DT_kind (base_kind,kid)) -> " default " ^ (pp_base_kind base_kind) ^ " " ^ (pp_kid kid)
+  | (DT_order order) -> " default " ^ " Order " ^ (pp_order order)
+  | (DT_typ (typschm,id)) -> " default " ^ (pp_typschm typschm) ^ " " ^ (pp_id id)
+
+
+let pp_val_spec_aux (val_spec_aux5:val_spec_aux) : string =
+  match val_spec_aux5 with
+  | (VS_val_spec (typschm,id)) -> " val " ^ (pp_typschm typschm) ^ " " ^ (pp_id id)
+  | (VS_extern_no_rename (typschm,id)) -> " val " ^ " extern " ^ (pp_typschm typschm) ^ " " ^ (pp_id id)
+  | (VS_extern_spec (typschm,id,string)) -> " val " ^ " extern " ^ (pp_typschm typschm) ^ " " ^ (pp_id id) ^ " = " ^ (pp_string string)
+
+
+let pp_pexp_aux (pexp_aux5:pexp_aux) : string =
+  match pexp_aux5 with
+  | (Pat_exp (pat,exp)) -> (pp_pat pat) ^ " -> " ^ (pp_exp exp)
+
+
+let pp_quant_item_aux (quant_item_aux5:quant_item_aux) : string =
+  match quant_item_aux5 with
+  | (QI_id kinded_id) -> (pp_kinded_id kinded_id)
+  | (QI_const n_constraint) -> (pp_n_constraint n_constraint)
+
+
+let pp_typ_arg_aux (typ_arg_aux5:typ_arg_aux) : string =
+  match typ_arg_aux5 with
+  | (Typ_arg_nexp nexp) -> (pp_nexp nexp)
+  | (Typ_arg_typ typ) -> (pp_typ typ)
+  | (Typ_arg_order order) -> (pp_order order)
+  | (Typ_arg_effect effect) -> (pp_effect effect)
+
+
+let pp_dec_spec (dec_spec5:dec_spec) : string =
+  match dec_spec5 with
+  | (DEC_aux (dec_spec_aux,annot)) -> (pp_dec_spec_aux dec_spec_aux) ^ " " ^ (pp_annot annot)
+
+
+let pp_type_def (type_def5:type_def) : string =
+  match type_def5 with
+  | (TD_aux (type_def_aux,annot)) -> (pp_type_def_aux type_def_aux) ^ " " ^ (pp_annot annot)
+
+
+let pp_scattered_def (scattered_def5:scattered_def) : string =
+  match scattered_def5 with
+  | (SD_aux (scattered_def_aux,annot)) -> (pp_scattered_def_aux scattered_def_aux) ^ " " ^ (pp_annot annot)
+
+
+let pp_fundef (fundef5:fundef) : string =
+  match fundef5 with
+  | (FD_aux (fundef_aux,annot)) -> (pp_fundef_aux fundef_aux) ^ " " ^ (pp_annot annot)
+
+
+let pp_default_spec (default_spec5:default_spec) : string =
+  match default_spec5 with
+  | (DT_aux (default_spec_aux,l)) -> (pp_default_spec_aux default_spec_aux) ^ " " ^ (pp_l l)
+
+
+let pp_val_spec (val_spec5:val_spec) : string =
+  match val_spec5 with
+  | (VS_aux (val_spec_aux,annot)) -> (pp_val_spec_aux val_spec_aux) ^ " " ^ (pp_annot annot)
+
+
+let pp_fpat_aux (fpat_aux5:fpat_aux) : string =
+  match fpat_aux5 with
+  | (FP_Fpat (id,pat)) -> (pp_id id) ^ " = " ^ (pp_pat pat)
+
+
+let pp_base_effect_aux (base_effect_aux5:base_effect_aux) : string =
+  match base_effect_aux5 with
+  | BE_rreg -> " rreg "
+  | BE_wreg -> " wreg "
+  | BE_rmem -> " rmem "
+  | BE_wmem -> " wmem "
+  | BE_barr -> " barr "
+  | BE_undef -> " undef "
+  | BE_unspec -> " unspec "
+  | BE_nondet -> " nondet "
+
+
+let pp_fexp_aux (fexp_aux5:fexp_aux) : string =
+  match fexp_aux5 with
+  | (FE_Fexp (id,exp)) -> (pp_id id) ^ " = " ^ (pp_exp exp)
+
+
+let rec pp_index_range (index_range5:index_range) : string =
+  match index_range5 with
+  | (BF_aux (index_range_aux,l)) -> (pp_index_range_aux index_range_aux) ^ " " ^ (pp_l l)
+and
+pp_index_range_aux (index_range_aux5:index_range_aux) : string =
+  match index_range_aux5 with
+  | (BF_single num) -> (pp_num num)
+  | (BF_range (num1,num2)) -> (pp_num num1) ^ " .. " ^ (pp_num num2)
+  | (BF_concat (index_range1,index_range2)) -> (pp_index_range index_range1) ^ " , " ^ (pp_index_range index_range2)
+
+
+let pp_pexp (pexp5:pexp) : string =
+  match pexp5 with
+  | (Pat_aux (pexp_aux,annot)) -> (pp_pexp_aux pexp_aux) ^ " " ^ (pp_annot annot)
+
+
+let pp_quant_item (quant_item5:quant_item) : string =
+  match quant_item5 with
+  | (QI_aux (quant_item_aux,l)) -> (pp_quant_item_aux quant_item_aux) ^ " " ^ (pp_l l)
+
+
+let pp_ix (ix5:ix) : string = ix5
+
+let pp_typ_arg (typ_arg5:typ_arg) : string =
+  match typ_arg5 with
+  | (Typ_arg_aux (typ_arg_aux,l)) -> (pp_typ_arg_aux typ_arg_aux) ^ " " ^ (pp_l l)
+
+
+let pp_def (def5:def) : string =
+  match def5 with
+  | (DEF_type type_def) -> (pp_type_def type_def)
+  | (DEF_fundef fundef) -> (pp_fundef fundef)
+  | (DEF_val letbind) -> (pp_letbind letbind)
+  | (DEF_spec val_spec) -> (pp_val_spec val_spec)
+  | (DEF_default default_spec) -> (pp_default_spec default_spec)
+  | (DEF_scattered scattered_def) -> (pp_scattered_def scattered_def)
+  | (DEF_reg_dec dec_spec) -> (pp_dec_spec dec_spec)
+
+
+let pp_fpat (fpat5:fpat) : string =
+  match fpat5 with
+  | (FP_aux (fpat_aux,annot)) -> (pp_fpat_aux fpat_aux) ^ " " ^ (pp_annot annot)
+
+
+let pp_base_effect (base_effect5:base_effect) : string =
+  match base_effect5 with
+  | (BE_aux (base_effect_aux,l)) -> (pp_base_effect_aux base_effect_aux) ^ " " ^ (pp_l l)
+
+
+let pp_fexp (fexp5:fexp) : string =
+  match fexp5 with
+  | (FE_aux (fexp_aux,annot)) -> (pp_fexp_aux fexp_aux) ^ " " ^ (pp_annot annot)
+
+
+let pp_defs (defs5:defs) : string =
+  match defs5 with
+  | (Defs (def_list)) -> (String.concat " " (List.map (fun def -> pp_'a def def) def_list))
+
+
 
 
diff --git a/language/l2_parse.ml b/language/l2_parse.ml
index ed594d3b..4dacb804 100644
--- a/language/l2_parse.ml
+++ b/language/l2_parse.ml
@@ -1,4 +1,4 @@
-(* generated by Ott 0.24 from: l2_parse.ott *)
+(* generated by Ott 0.25 from: l2_parse.ott *)
 
 
 type text = string
@@ -441,5 +441,460 @@ type
 defs =  (* Definition sequence *)
    Defs of (def) list
 
+(** pretty printer *)
+let pp_x (y5:x) : string = y5
+
+let pp_kid_aux (kid_aux5:kid_aux) : string =
+  match kid_aux5 with
+  | (Var x) -> " ' " ^ (pp_x x)
+
+
+let pp_id_aux (id_aux5:id_aux) : string =
+  match id_aux5 with
+  | (Id x) -> (pp_x x)
+  | (DeIid x) -> " ( " ^ " deinfix " ^ (pp_x x) ^ " ) "
+
+
+let pp_typquant_aux (typquant_aux5:typquant_aux) : string =
+  match typquant_aux5 with
+  | (TypQ_tq (quant_item_list)) -> " forall " ^ (String.concat "," (List.map (fun quant_item -> pp_quant_item quant_item) quant_item_list)) ^ " . "
+  | TypQ_no_forall -> 
+
+
+let pp_kid (kid5:kid) : string =
+  match kid5 with
+  | (Kid_aux (kid_aux,l)) -> (pp_kid_aux kid_aux) ^ " " ^ (pp_l l)
+
+
+let pp_id (id5:id) : string =
+  match id5 with
+  | (Id_aux (id_aux,l)) -> (pp_id_aux id_aux) ^ " " ^ (pp_l l)
+
+
+let pp_typquant (typquant5:typquant) : string =
+  match typquant5 with
+  | (TypQ_aux (typquant_aux,l)) -> (pp_typquant_aux typquant_aux) ^ " " ^ (pp_l l)
+
+
+let rec pp_atyp (atyp5:atyp) : string =
+  match atyp5 with
+  | (ATyp_aux (atyp_aux,l)) -> (pp_atyp_aux atyp_aux) ^ " " ^ (pp_l l)
+and
+pp_atyp_aux (atyp_aux5:atyp_aux) : string =
+  match atyp_aux5 with
+  | (ATyp_id id) -> (pp_id id)
+  | (ATyp_var kid) -> (pp_kid kid)
+  | (ATyp_constant num) -> (pp_num num)
+  | (ATyp_times (atyp1,atyp2)) -> (pp_atyp atyp1) ^ " * " ^ (pp_atyp atyp2)
+  | (ATyp_sum (atyp1,atyp2)) -> (pp_atyp atyp1) ^ " + " ^ (pp_atyp atyp2)
+  | (ATyp_minus (atyp1,atyp2)) -> (pp_atyp atyp1) ^ " - " ^ (pp_atyp atyp2)
+  | (ATyp_exp atyp) -> " 2** " ^ (pp_atyp atyp)
+  | (ATyp_neg atyp) -> " neg " ^ (pp_atyp atyp)
+  | ATyp_inc -> " inc "
+  | ATyp_dec -> " dec "
+  | ATyp_default_ord -> " defaultOrd "
+  | (ATyp_set (base_effect_list)) -> " { " ^ (String.concat "," (List.map (fun base_effect -> pp_base_effect base_effect) base_effect_list)) ^ " } "
+  | (ATyp_fn (atyp1,atyp2,atyp3)) -> (pp_atyp atyp1) ^ " -> " ^ (pp_atyp atyp2) ^ " effect " ^ (pp_atyp atyp3)
+  | (ATyp_tup (atyp_list)) -> " ( " ^ (String.concat "," (List.map (fun atyp -> pp_atyp atyp) atyp_list)) ^ " ) "
+  | (ATyp_app (id,(atyp_list))) -> (pp_id id) ^ " < " ^ (String.concat "," (List.map (fun atyp -> pp_atyp atyp) atyp_list)) ^ " > "
+
+
+let pp_lit_aux (lit_aux5:lit_aux) : string =
+  match lit_aux5 with
+  | L_unit -> " ( " ^ " ) "
+  | L_zero -> " bitzero "
+  | L_one -> " bitone "
+  | L_true -> " true "
+  | L_false -> " false "
+  | (L_num num) -> (pp_num num)
+  | (L_hex hex) -> (pp_hex hex)
+  | (L_bin bin) -> (pp_bin bin)
+  | L_undef -> " undefined "
+  | (L_string string) -> (pp_string string)
+
+
+let pp_typschm_aux (typschm_aux5:typschm_aux) : string =
+  match typschm_aux5 with
+  | (TypSchm_ts (typquant,atyp)) -> (pp_typquant typquant) ^ " " ^ (pp_atyp atyp)
+
+
+let pp_lit (lit5:lit) : string =
+  match lit5 with
+  | (L_aux (lit_aux,l)) -> (pp_lit_aux lit_aux) ^ " " ^ (pp_l l)
+
+
+let pp_fexps_aux (fexps_aux5:fexps_aux) : string =
+  match fexps_aux5 with
+  | (FES_Fexps ((fexp_list),semi_opt)) -> (String.concat ";" (List.map (fun fexp -> pp_fexp fexp) fexp_list)) ^ " " ^ (pp_semi_opt semi_opt)
+
+
+let pp_typschm (typschm5:typschm) : string =
+  match typschm5 with
+  | (TypSchm_aux (typschm_aux,l)) -> (pp_typschm_aux typschm_aux) ^ " " ^ (pp_l l)
+
+
+let rec pp_pat (pat5:pat) : string =
+  match pat5 with
+  | (P_aux (pat_aux,l)) -> (pp_pat_aux pat_aux) ^ " " ^ (pp_l l)
+and
+pp_pat_aux (pat_aux5:pat_aux) : string =
+  match pat_aux5 with
+  | (P_lit lit) -> (pp_lit lit)
+  | P_wild -> " _ "
+  | (P_as (pat,id)) -> " ( " ^ (pp_pat pat) ^ " as " ^ (pp_id id) ^ " ) "
+  | (P_typ (atyp,pat)) -> " ( " ^ (pp_atyp atyp) ^ " ) " ^ (pp_pat pat)
+  | (P_id id) -> (pp_id id)
+  | (P_app (id,(pat_list))) -> (pp_id id) ^ " ( " ^ (String.concat "," (List.map (fun pat -> pp_pat pat) pat_list)) ^ " ) "
+  | (P_record ((fpat_list),semi_opt)) -> " { " ^ (String.concat ";" (List.map (fun fpat -> pp_fpat fpat) fpat_list)) ^ " " ^ (pp_semi_opt semi_opt) ^ " } "
+  | (P_vector (pat_list)) -> " [ " ^ (String.concat "," (List.map (fun pat -> pp_pat pat) pat_list)) ^ " ] "
+  | (P_vector_indexed (num_pat_list)) -> " [ " ^ (String.concat "," (List.map (fun num,pat -> pp_int num,pp_pat pat) num_pat_list)) ^ " ] "
+  | (P_vector_concat (pat_list)) -> (String.concat ":" (List.map (fun pat -> pp_pat pat) pat_list))
+  | (P_tup (pat_list)) -> " ( " ^ (String.concat "," (List.map (fun pat -> pp_pat pat) pat_list)) ^ " ) "
+  | (P_list (pat_list)) -> " [|| " ^ (String.concat "," (List.map (fun pat -> pp_pat pat) pat_list)) ^ " ||] "
+
+
+let pp_fexps (fexps5:fexps) : string =
+  match fexps5 with
+  | (FES_aux (fexps_aux,l)) -> (pp_fexps_aux fexps_aux) ^ " " ^ (pp_l l)
+
+
+let pp_kind_aux (kind_aux5:kind_aux) : string =
+  match kind_aux5 with
+  | (K_kind (base_kind_list)) -> (String.concat "->" (List.map (fun base_kind -> pp_base_kind base_kind) base_kind_list))
+
+
+let rec pp_letbind (letbind5:letbind) : string =
+  match letbind5 with
+  | (LB_aux (letbind_aux,l)) -> (pp_letbind_aux letbind_aux) ^ " " ^ (pp_l l)
+and
+pp_letbind_aux (letbind_aux5:letbind_aux) : string =
+  match letbind_aux5 with
+  | (LB_val_explicit (typschm,pat,exp)) -> " let " ^ (pp_typschm typschm) ^ " " ^ (pp_pat pat) ^ " = " ^ (pp_exp exp)
+  | (LB_val_implicit (pat,exp)) -> " let " ^ (pp_pat pat) ^ " = " ^ (pp_exp exp)
+and
+pp_opt_default (opt_default5:opt_default) : string =
+  match opt_default5 with
+  | (Def_val_aux (opt_default_aux,l)) -> (pp_opt_default_aux opt_default_aux) ^ " " ^ (pp_l l)
+and
+pp_opt_default_aux (opt_default_aux5:opt_default_aux) : string =
+  match opt_default_aux5 with
+  | Def_val_empty -> 
+  | (Def_val_dec exp) -> " ; " ^ " default " ^ " = " ^ (pp_exp exp)
+and
+pp_exp (exp5:exp) : string =
+  match exp5 with
+  | (E_aux (exp_aux,l)) -> (pp_exp_aux exp_aux) ^ " " ^ (pp_l l)
+and
+pp_exp_aux (exp_aux5:exp_aux) : string =
+  match exp_aux5 with
+  | (E_block (exp_list)) -> " { " ^ (String.concat ";" (List.map (fun exp -> pp_exp exp) exp_list)) ^ " } "
+  | (E_nondet (exp_list)) -> " nondet " ^ " { " ^ (String.concat ";" (List.map (fun exp -> pp_exp exp) exp_list)) ^ " } "
+  | (E_id id) -> (pp_id id)
+  | (E_lit lit) -> (pp_lit lit)
+  | (E_cast (atyp,exp)) -> " ( " ^ (pp_atyp atyp) ^ " ) " ^ (pp_exp exp)
+  | (E_app (id,(exp_list))) -> (pp_id id) ^ " ( " ^ (String.concat "," (List.map (fun exp -> pp_exp exp) exp_list)) ^ " ) "
+  | (E_app_infix (exp1,id,exp2)) -> (pp_exp exp1) ^ " " ^ (pp_id id) ^ " " ^ (pp_exp exp2)
+  | (E_tuple (exp_list)) -> " ( " ^ (String.concat "," (List.map (fun exp -> pp_exp exp) exp_list)) ^ " ) "
+  | (E_if (exp1,exp2,exp3)) -> " if " ^ (pp_exp exp1) ^ " then " ^ (pp_exp exp2) ^ " else " ^ (pp_exp exp3)
+  | (E_for (id,exp1,exp2,exp3,atyp,exp4)) -> " foreach " ^ (pp_id id) ^ " from " ^ (pp_exp exp1) ^ " to " ^ (pp_exp exp2) ^ " by " ^ (pp_exp exp3) ^ " in " ^ (pp_atyp atyp) ^ " " ^ (pp_exp exp4)
+  | (E_vector (exp_list)) -> " [ " ^ (String.concat "," (List.map (fun exp -> pp_exp exp) exp_list)) ^ " ] "
+  | (E_vector_indexed ((exp_list),opt_default)) -> " [ " ^ (String.concat "," (List.map (fun exp -> pp_exp exp) exp_list)) ^ " " ^ (pp_opt_default opt_default) ^ " ] "
+  | (E_vector_access (exp,exp')) -> (pp_exp exp) ^ " [ " ^ (pp_exp exp') ^ " ] "
+  | (E_vector_subrange (exp,exp1,exp2)) -> (pp_exp exp) ^ " [ " ^ (pp_exp exp1) ^ " .. " ^ (pp_exp exp2) ^ " ] "
+  | (E_vector_update (exp,exp1,exp2)) -> " [ " ^ (pp_exp exp) ^ " with " ^ (pp_exp exp1) ^ " = " ^ (pp_exp exp2) ^ " ] "
+  | (E_vector_update_subrange (exp,exp1,exp2,exp3)) -> " [ " ^ (pp_exp exp) ^ " with " ^ (pp_exp exp1) ^ " : " ^ (pp_exp exp2) ^ " = " ^ (pp_exp exp3) ^ " ] "
+  | (E_vector_append (exp,exp2)) -> (pp_exp exp) ^ " : " ^ (pp_exp exp2)
+  | (E_list (exp_list)) -> " [|| " ^ (String.concat "," (List.map (fun exp -> pp_exp exp) exp_list)) ^ " ||] "
+  | (E_cons (exp1,exp2)) -> (pp_exp exp1) ^ " :: " ^ (pp_exp exp2)
+  | (E_record fexps) -> " { " ^ (pp_fexps fexps) ^ " } "
+  | (E_record_update (exp,(exp_list))) -> " { " ^ (pp_exp exp) ^ " with " ^ (String.concat ";" (List.map (fun exp -> pp_exp exp) exp_list)) ^ " } "
+  | (E_field (exp,id)) -> (pp_exp exp) ^ " . " ^ (pp_id id)
+  | (E_case (exp,(pexp_list))) -> " switch " ^ (pp_exp exp) ^ " { " ^ (String.concat " " (List.map (fun pexp -> pp_pexp pexp) pexp_list)) ^ " } "
+  | (E_let (letbind,exp)) -> (pp_letbind letbind) ^ " in " ^ (pp_exp exp)
+  | (E_assign (exp,exp')) -> (pp_exp exp) ^ " := " ^ (pp_exp exp')
+  | (E_exit exp) -> " exit " ^ (pp_exp exp)
+
+
+let pp_kind (kind5:kind) : string =
+  match kind5 with
+  | (K_aux (kind_aux,l)) -> (pp_kind_aux kind_aux) ^ " " ^ (pp_l l)
+
+
+let pp_name_scm_opt_aux (name_scm_opt_aux5:name_scm_opt_aux) : string =
+  match name_scm_opt_aux5 with
+  | Name_sect_none -> 
+  | (Name_sect_some regexp) -> " [ " ^ " name " ^ " = " ^ (pp_regexp regexp) ^ " ] "
+
+
+let pp_rec_opt_aux (rec_opt_aux5:rec_opt_aux) : string =
+  match rec_opt_aux5 with
+  | Rec_nonrec -> 
+  | Rec_rec -> " rec "
+
+
+let pp_tannot_opt_aux (tannot_opt_aux5:tannot_opt_aux) : string =
+  match tannot_opt_aux5 with
+  | Typ_annot_opt_none -> 
+  | (Typ_annot_opt_some (typquant,atyp)) -> (pp_typquant typquant) ^ " " ^ (pp_atyp atyp)
+
+
+let pp_effect_opt_aux (effect_opt_aux5:effect_opt_aux) : string =
+  match effect_opt_aux5 with
+  | Effect_opt_pure -> 
+  | (Effect_opt_effect atyp) -> " effectkw " ^ (pp_atyp atyp)
+
+
+let pp_type_union_aux (type_union_aux5:type_union_aux) : string =
+  match type_union_aux5 with
+  | (Tu_id id) -> (pp_id id)
+  | (Tu_ty_id (atyp,id)) -> (pp_atyp atyp) ^ " " ^ (pp_id id)
+
+
+let pp_funcl_aux (funcl_aux5:funcl_aux) : string =
+  match funcl_aux5 with
+  | (FCL_Funcl (id,pat,exp)) -> (pp_id id) ^ " " ^ (pp_pat pat) ^ " = " ^ (pp_exp exp)
+
+
+let pp_base_kind_aux (base_kind_aux5:base_kind_aux) : string =
+  match base_kind_aux5 with
+  | BK_type -> " Type "
+  | BK_nat -> " Nat "
+  | BK_order -> " Order "
+  | BK_effect -> " Effect "
+
+
+let pp_kinded_id_aux (kinded_id_aux5:kinded_id_aux) : string =
+  match kinded_id_aux5 with
+  | (KOpt_none kid) -> (pp_kid kid)
+  | (KOpt_kind (kind,kid)) -> (pp_kind kind) ^ " " ^ (pp_kid kid)
+
+
+let pp_n_constraint_aux (n_constraint_aux5:n_constraint_aux) : string =
+  match n_constraint_aux5 with
+  | (NC_fixed (atyp,atyp')) -> (pp_atyp atyp) ^ " = " ^ (pp_atyp atyp')
+  | (NC_bounded_ge (atyp,atyp')) -> (pp_atyp atyp) ^ " >= " ^ (pp_atyp atyp')
+  | (NC_bounded_le (atyp,atyp')) -> (pp_atyp atyp) ^ " <= " ^ (pp_atyp atyp')
+  | (NC_nat_set_bounded (kid,(num_list))) -> (pp_kid kid) ^ " IN " ^ " { " ^ (String.concat "," (List.map (fun num -> pp_int num) num_list)) ^ " } "
+
+
+let pp_name_scm_opt (name_scm_opt5:name_scm_opt) : string =
+  match name_scm_opt5 with
+  | (Name_sect_aux (name_scm_opt_aux,l)) -> (pp_name_scm_opt_aux name_scm_opt_aux) ^ " " ^ (pp_l l)
+
+
+let pp_rec_opt (rec_opt5:rec_opt) : string =
+  match rec_opt5 with
+  | (Rec_aux (rec_opt_aux,l)) -> (pp_rec_opt_aux rec_opt_aux) ^ " " ^ (pp_l l)
+
+
+let pp_tannot_opt (tannot_opt5:tannot_opt) : string =
+  match tannot_opt5 with
+  | (Typ_annot_opt_aux (tannot_opt_aux,l)) -> (pp_tannot_opt_aux tannot_opt_aux) ^ " " ^ (pp_l l)
+
+
+let pp_effect_opt (effect_opt5:effect_opt) : string =
+  match effect_opt5 with
+  | (Effect_opt_aux (effect_opt_aux,l)) -> (pp_effect_opt_aux effect_opt_aux) ^ " " ^ (pp_l l)
+
+
+let pp_type_union (type_union5:type_union) : string =
+  match type_union5 with
+  | (Tu_aux (type_union_aux,l)) -> (pp_type_union_aux type_union_aux) ^ " " ^ (pp_l l)
+
+
+let pp_funcl (funcl5:funcl) : string =
+  match funcl5 with
+  | (FCL_aux (funcl_aux,l)) -> (pp_funcl_aux funcl_aux) ^ " " ^ (pp_l l)
+
+
+let pp_base_kind (base_kind5:base_kind) : string =
+  match base_kind5 with
+  | (BK_aux (base_kind_aux,l)) -> (pp_base_kind_aux base_kind_aux) ^ " " ^ (pp_l l)
+
+
+let pp_kinded_id (kinded_id5:kinded_id) : string =
+  match kinded_id5 with
+  | (KOpt_aux (kinded_id_aux,l)) -> (pp_kinded_id_aux kinded_id_aux) ^ " " ^ (pp_l l)
+
+
+let pp_n_constraint (n_constraint5:n_constraint) : string =
+  match n_constraint5 with
+  | (NC_aux (n_constraint_aux,l)) -> (pp_n_constraint_aux n_constraint_aux) ^ " " ^ (pp_l l)
+
+
+let pp_type_def_aux (type_def_aux5:type_def_aux) : string =
+  match type_def_aux5 with
+  | (TD_abbrev (id,name_scm_opt,typschm)) -> " typedef " ^ (pp_id id) ^ " " ^ (pp_name_scm_opt name_scm_opt) ^ " = " ^ (pp_typschm typschm)
+  | (TD_record (id,name_scm_opt,typquant,(atyp_id_list),semi_opt)) -> " typedef " ^ (pp_id id) ^ " " ^ (pp_name_scm_opt name_scm_opt) ^ " = " ^ " const " ^ " struct " ^ (pp_typquant typquant) ^ " { " ^ (String.concat ";" (List.map (fun atyp,id -> pp_atyp atyp;pp_id id) atyp_id_list)) ^ " " ^ (pp_semi_opt semi_opt) ^ " } "
+  | (TD_variant (id,name_scm_opt,typquant,(type_union_list),semi_opt)) -> " typedef " ^ (pp_id id) ^ " " ^ (pp_name_scm_opt name_scm_opt) ^ " = " ^ " const " ^ " union " ^ (pp_typquant typquant) ^ " { " ^ (String.concat ";" (List.map (fun type_union -> pp_type_union type_union) type_union_list)) ^ " " ^ (pp_semi_opt semi_opt) ^ " } "
+  | (TD_enum (id,name_scm_opt,(id_list),semi_opt)) -> " typedef " ^ (pp_id id) ^ " " ^ (pp_name_scm_opt name_scm_opt) ^ " = " ^ " enumerate " ^ " { " ^ (String.concat ";" (List.map (fun id -> pp_id id) id_list)) ^ " " ^ (pp_semi_opt semi_opt) ^ " } "
+  | (TD_register (id,atyp,atyp',(index_range_id_list))) -> " typedef " ^ (pp_id id) ^ " = " ^ " register " ^ " bits " ^ " [ " ^ (pp_atyp atyp) ^ " : " ^ (pp_atyp atyp') ^ " ] " ^ " { " ^ (String.concat ";" (List.map (fun index_range,id -> pp_index_range index_range;pp_id id) index_range_id_list)) ^ " } "
+
+
+let pp_scattered_def_aux (scattered_def_aux5:scattered_def_aux) : string =
+  match scattered_def_aux5 with
+  | (SD_scattered_function (rec_opt,tannot_opt,effect_opt,id)) -> " scattered " ^ " function " ^ (pp_rec_opt rec_opt) ^ " " ^ (pp_tannot_opt tannot_opt) ^ " " ^ (pp_effect_opt effect_opt) ^ " " ^ (pp_id id)
+  | (SD_scattered_funcl funcl) -> " function " ^ " clause " ^ (pp_funcl funcl)
+  | (SD_scattered_variant (id,name_scm_opt,typquant)) -> " scattered " ^ " typedef " ^ (pp_id id) ^ " " ^ (pp_name_scm_opt name_scm_opt) ^ " = " ^ " const " ^ " union " ^ (pp_typquant typquant)
+  | (SD_scattered_unioncl (id,type_union)) -> " union " ^ (pp_id id) ^ " member " ^ (pp_type_union type_union)
+  | (SD_scattered_end id) -> " end " ^ (pp_id id)
+
+
+let pp_dec_spec_aux (dec_spec_aux5:dec_spec_aux) : string =
+  match dec_spec_aux5 with
+  | (DEC_reg (atyp,id)) -> " register " ^ (pp_atyp atyp) ^ " " ^ (pp_id id)
+  | (DEC_alias (id,exp)) -> " register " ^ " alias " ^ (pp_id id) ^ " = " ^ (pp_exp exp)
+  | (DEC_typ_alias (atyp,id,exp)) -> " register " ^ " alias " ^ (pp_atyp atyp) ^ " " ^ (pp_id id) ^ " = " ^ (pp_exp exp)
+
+
+let pp_val_spec_aux (val_spec_aux5:val_spec_aux) : string =
+  match val_spec_aux5 with
+  | (VS_val_spec (typschm,id)) -> " val " ^ (pp_typschm typschm) ^ " " ^ (pp_id id)
+  | (VS_extern_no_rename (typschm,id)) -> " val " ^ " extern " ^ (pp_typschm typschm) ^ " " ^ (pp_id id)
+  | (VS_extern_spec (typschm,id,string)) -> " val " ^ " extern " ^ (pp_typschm typschm) ^ " " ^ (pp_id id) ^ " = " ^ (pp_string string)
+
+
+let pp_default_typing_spec_aux (default_typing_spec_aux5:default_typing_spec_aux) : string =
+  match default_typing_spec_aux5 with
+  | (DT_kind (base_kind,kid)) -> " default " ^ (pp_base_kind base_kind) ^ " " ^ (pp_kid kid)
+  | (DT_order (base_kind,atyp)) -> " default " ^ (pp_base_kind base_kind) ^ " " ^ (pp_atyp atyp)
+  | (DT_typ (typschm,id)) -> " default " ^ (pp_typschm typschm) ^ " " ^ (pp_id id)
+
+
+let pp_fundef_aux (fundef_aux5:fundef_aux) : string =
+  match fundef_aux5 with
+  | (FD_function (rec_opt,tannot_opt,effect_opt,(funcl_list))) -> " function " ^ (pp_rec_opt rec_opt) ^ " " ^ (pp_tannot_opt tannot_opt) ^ " " ^ (pp_effect_opt effect_opt) ^ (String.concat "and" (List.map (fun funcl -> pp_funcl funcl) funcl_list))
+
+
+let pp_fexp_aux (fexp_aux5:fexp_aux) : string =
+  match fexp_aux5 with
+  | (FE_Fexp (id,exp)) -> (pp_id id) ^ " = " ^ (pp_exp exp)
+
+
+let pp_base_effect_aux (base_effect_aux5:base_effect_aux) : string =
+  match base_effect_aux5 with
+  | BE_rreg -> " rreg "
+  | BE_wreg -> " wreg "
+  | BE_rmem -> " rmem "
+  | BE_wmem -> " wmem "
+  | BE_barr -> " barr "
+  | BE_undef -> " undef "
+  | BE_unspec -> " unspec "
+  | BE_nondet -> " nondet "
+
+
+let pp_quant_item_aux (quant_item_aux5:quant_item_aux) : string =
+  match quant_item_aux5 with
+  | (QI_id kinded_id) -> (pp_kinded_id kinded_id)
+  | (QI_const n_constraint) -> (pp_n_constraint n_constraint)
+
+
+let pp_pexp_aux (pexp_aux5:pexp_aux) : string =
+  match pexp_aux5 with
+  | (Pat_exp (pat,exp)) -> (pp_pat pat) ^ " -> " ^ (pp_exp exp)
+
+
+let pp_fpat_aux (fpat_aux5:fpat_aux) : string =
+  match fpat_aux5 with
+  | (FP_Fpat (id,pat)) -> (pp_id id) ^ " = " ^ (pp_pat pat)
+
+
+let pp_type_def (type_def5:type_def) : string =
+  match type_def5 with
+  | (TD_aux (type_def_aux,l)) -> (pp_type_def_aux type_def_aux) ^ " " ^ (pp_l l)
+
+
+let pp_scattered_def (scattered_def5:scattered_def) : string =
+  match scattered_def5 with
+  | (SD_aux (scattered_def_aux,l)) -> (pp_scattered_def_aux scattered_def_aux) ^ " " ^ (pp_l l)
+
+
+let pp_dec_spec (dec_spec5:dec_spec) : string =
+  match dec_spec5 with
+  | (DEC_aux (dec_spec_aux,l)) -> (pp_dec_spec_aux dec_spec_aux) ^ " " ^ (pp_l l)
+
+
+let pp_val_spec (val_spec5:val_spec) : string =
+  match val_spec5 with
+  | (VS_aux (val_spec_aux,l)) -> (pp_val_spec_aux val_spec_aux) ^ " " ^ (pp_l l)
+
+
+let pp_default_typing_spec (default_typing_spec5:default_typing_spec) : string =
+  match default_typing_spec5 with
+  | (DT_aux (default_typing_spec_aux,l)) -> (pp_default_typing_spec_aux default_typing_spec_aux) ^ " " ^ (pp_l l)
+
+
+let pp_fundef (fundef5:fundef) : string =
+  match fundef5 with
+  | (FD_aux (fundef_aux,l)) -> (pp_fundef_aux fundef_aux) ^ " " ^ (pp_l l)
+
+
+let pp_fexp (fexp5:fexp) : string =
+  match fexp5 with
+  | (FE_aux (fexp_aux,l)) -> (pp_fexp_aux fexp_aux) ^ " " ^ (pp_l l)
+
+
+let pp_base_effect (base_effect5:base_effect) : string =
+  match base_effect5 with
+  | (BE_aux (base_effect_aux,l)) -> (pp_base_effect_aux base_effect_aux) ^ " " ^ (pp_l l)
+
+
+let pp_ix (ix5:ix) : string = ix5
+
+let pp_defs (defs5:defs) : string =
+  match defs5 with
+  | (Defs (def_list)) -> (String.concat " " (List.map (fun def -> pp_def def) def_list))
+
+
+let pp_quant_item (quant_item5:quant_item) : string =
+  match quant_item5 with
+  | (QI_aux (quant_item_aux,l)) -> (pp_quant_item_aux quant_item_aux) ^ " " ^ (pp_l l)
+
+
+let rec pp_index_range (index_range5:index_range) : string =
+  match index_range5 with
+  | (BF_aux (index_range_aux,l)) -> (pp_index_range_aux index_range_aux) ^ " " ^ (pp_l l)
+and
+pp_index_range_aux (index_range_aux5:index_range_aux) : string =
+  match index_range_aux5 with
+  | (BF_single num) -> (pp_num num)
+  | (BF_range (num1,num2)) -> (pp_num num1) ^ " : " ^ (pp_num num2)
+  | (BF_concat (index_range1,index_range2)) -> (pp_index_range index_range1) ^ " , " ^ (pp_index_range index_range2)
+
+
+let pp_pexp (pexp5:pexp) : string =
+  match pexp5 with
+  | (Pat_aux (pexp_aux,l)) -> (pp_pexp_aux pexp_aux) ^ " " ^ (pp_l l)
+
+
+let pp_fpat (fpat5:fpat) : string =
+  match fpat5 with
+  | (FP_aux (fpat_aux,l)) -> (pp_fpat_aux fpat_aux) ^ " " ^ (pp_l l)
+
+
+let pp_def (def5:def) : string =
+  match def5 with
+  | (DEF_type type_def) -> (pp_type_def type_def)
+  | (DEF_fundef fundef) -> (pp_fundef fundef)
+  | (DEF_val letbind) -> (pp_letbind letbind)
+  | (DEF_spec val_spec) -> (pp_val_spec val_spec)
+  | (DEF_default default_typing_spec) -> (pp_default_typing_spec default_typing_spec)
+  | (DEF_scattered scattered_def) -> (pp_scattered_def scattered_def)
+  | (DEF_reg_dec dec_spec) -> (pp_dec_spec dec_spec)
+
+
+let rec pp_lexp (lexp5:lexp) : string =
+  match lexp5 with
+  | (LEXP_aux (lexp_aux,l)) -> (pp_lexp_aux lexp_aux) ^ " " ^ (pp_l l)
+and
+pp_lexp_aux (lexp_aux5:lexp_aux) : string =
+  match lexp_aux5 with
+  | (LEXP_id id) -> (pp_id id)
+  | (LEXP_mem (id,(exp_list))) -> (pp_id id) ^ " ( " ^ (String.concat "," (List.map (fun exp -> pp_exp exp) exp_list)) ^ " ) "
+  | (LEXP_vector (lexp,exp)) -> (pp_lexp lexp) ^ " [ " ^ (pp_exp exp) ^ " ] "
+  | (LEXP_vector_range (lexp,exp1,exp2)) -> (pp_lexp lexp) ^ " [ " ^ (pp_exp exp1) ^ " : " ^ (pp_exp exp2) ^ " ] "
+  | (LEXP_field (lexp,id)) -> (pp_lexp lexp) ^ " . " ^ (pp_id id)
+
+
 
 
diff --git a/language/manual.tex b/language/manual.tex
deleted file mode 100644
index 5d4b9d6a..00000000
--- a/language/manual.tex
+++ /dev/null
@@ -1,117 +0,0 @@
-\documentclass[11pt]{article}
-
-\usepackage{amsmath,amssymb,supertabular,geometry,fullpage}
-\geometry{a4paper,twoside,landscape,left=10.5mm,right=10.5mm,top=20mm,bottom=30mm}
-\usepackage{color}
-
-\begin{document}
-
-\input{doc_in}
-
-\title{Sail Manual}
-\author{Kathryn E Gray, Gabriel Kerneis, Peter Sewell}
-
-\maketitle
-
-\tableofcontents
-
-\newpage
-
-\section{Sail syntax}
-
-\ottgrammartabular{
-\ottl\ottinterrule
-\ottannot\ottinterrule
-\ottid\ottinterrule
-\ottkid\ottinterrule
-\ottbaseXXkind\ottinterrule
-\ottkind\ottinterrule
-\ottnexp\ottinterrule
-\ottorder\ottinterrule
-\ottbaseXXeffect\ottinterrule
-\otteffect\ottinterrule
-\otttyp\ottinterrule
-\otttypXXarg\ottinterrule
-\ottnXXconstraint\ottinterrule
-\ottkindedXXid\ottinterrule
-\ottquantXXitem\ottinterrule
-\otttypquant\ottinterrule
-\otttypschm\ottinterrule
-\ottnameXXscmXXopt\ottinterrule
-\otttypeXXdef\ottinterrule
-\otttypeXXunion\ottinterrule
-\ottindexXXrange\ottinterrule
-\ottlit\ottinterrule
-\ottsemiXXopt\ottinterrule
-\ottpat\ottinterrule
-\ottfpat\ottinterrule
-\ottexp\ottinterrule
-\ottlexp\ottinterrule
-\ottfexp\ottinterrule
-\ottfexps\ottinterrule
-\ottoptXXdefault\ottinterrule
-\ottpexp\ottinterrule
-\otttannotXXopt\ottinterrule
-\ottrecXXopt\ottinterrule
-\otteffectXXopt\ottinterrule
-\ottfuncl\ottinterrule
-\ottfundef\ottinterrule
-\ottletbind\ottinterrule
-\ottvalXXspec\ottinterrule
-\ottdefaultXXspec\ottinterrule
-\ottscatteredXXdef\ottinterrule
-\ottregXXid\ottinterrule
-\ottaliasXXspec\ottinterrule
-\ottdecXXspec\ottinterrule
-\ottdef\ottinterrule
-\ottdefs\ottinterrule}
-
-\newpage
-\section{Sail primitive types and functions}
-
-\ottgrammartabular{
-\ottbuiltXXinXXtypes\ottinterrule}
-
-\ottgrammartabular{
-\ottbuiltXXinXXtypeXXabbreviations\ottinterrule
-\ottfunctions\ottinterrule
-\ottfunctionsXXwithXXcoercions\ottinterrule}
-\newpage
-
-\section{Sail type system}
-
-\subsection{Internal type syntax}
-
-\ottgrammartabular{
-\ottk\ottinterrule
-\ottt\ottinterrule
-\ottoptx\ottinterrule
-\otttag\ottinterrule
-\ottne\ottinterrule
-\otttXXarg\ottinterrule
-\otttXXargs\ottinterrule
-\ottnec\ottinterrule
-\ottSXXN\ottinterrule
-\ottEXXd\ottinterrule
-\ottkinf\ottinterrule
-\otttid\ottinterrule
-\ottEXXk\ottinterrule
-\otttinf\ottinterrule
-\ottEXXa\ottinterrule
-\ottfieldXXtyps\ottinterrule
-\ottEXXr\ottinterrule
-\ottenumerateXXmap\ottinterrule
-\ottEXXe\ottinterrule
-\ottEXXt\ottinterrule
-\ottts\ottinterrule
-\ottE\ottinterrule
-\ottI\ottinterrule
-\ottformula\ottinterrule}
-
-
-\subsection{ Type relations }
-\ottdefnss
-
-\section{Sail operational semantics \{TODO\}}
-
-\end{document}
\ No newline at end of file