Add type annotations to lem grammar, including printing out the annotated ast, and extending the interpreter to expect annotations.

Annotations and locations are still not used by the interpreter.

1 files changed, 329 insertions, 196 deletions

diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 236bfc91..4190ad9b 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -1,3 +1,4 @@
+open Type_internal
 open Ast
 open Format
 
@@ -349,86 +350,115 @@ let pp_defs ppf (Defs(defs)) =
 
 
 (****************************************************************************
- * source to Lem ast pretty printer
+ * annotated source to Lem ast pretty printer
 ****************************************************************************)
 
-let pp_format_id_lem (Id_aux(i,_)) =
-  match i with
-  | Id(i) -> "(Id \"" ^ i ^ "\")"
-  | DeIid(x) -> "(DeIid \"" ^ x ^ "\")"
+let rec pp_format_l_lem = function
+  | Parse_ast.Unknown -> "Unknown"
+  | Parse_ast.Trans(s,None) -> "(Trans \"" ^ s ^ "\" Nothing)"
+  | Parse_ast.Trans(s,(Some l)) -> "(Trans \"" ^  s ^ "\" (Just " ^ (pp_format_l_lem l) ^ "))"
+  | Parse_ast.Range(p1,p2) -> "(Range \"" ^ p1.Lexing.pos_fname ^ "\" " ^
+                               (string_of_int p1.Lexing.pos_lnum) ^ " " ^ 
+                               (string_of_int (p1.Lexing.pos_cnum - p1.Lexing.pos_bol)) ^ " " ^
+                               (string_of_int p2.Lexing.pos_lnum) ^ " " ^
+                               (string_of_int (p2.Lexing.pos_cnum - p2.Lexing.pos_bol)) ^ ")"
+
+let pp_lem_l ppf l = base ppf (pp_format_l_lem l)
+
+let pp_format_id_lem (Id_aux(i,l)) =
+  "(Id_aux " ^
+    (match i with
+      | Id(i) -> "(Id \"" ^ i ^ "\")"
+      | DeIid(x) -> "(DeIid \"" ^ x ^ "\")") ^ " " ^
+   (pp_format_l_lem l) ^ ")"
 
 let pp_lem_id ppf id = base ppf (pp_format_id_lem id)
 
-let pp_format_var_lem (Kid_aux(Var v,_)) = "(Var \"" ^ v ^ "\")"
+let pp_format_var_lem (Kid_aux(Var v,l)) = "(Kid_aux (Var \"" ^ v ^ "\") " ^ (pp_format_l_lem l) ^ ")"
 
 let pp_lem_var ppf var = base ppf (pp_format_var_lem var)
 
-let pp_format_bkind_lem (BK_aux(k,_)) =
-  match k with
-  | BK_type -> "BK_type"
-  | BK_nat -> "BK_nat"
-  | BK_order -> "BK_order"
-  | BK_effect -> "BK_effect"
+let pp_format_bkind_lem (BK_aux(k,l)) =
+  "(BK_aux " ^
+  (match k with
+    | BK_type -> "BK_type"
+    | BK_nat -> "BK_nat"
+    | BK_order -> "BK_order"
+    | BK_effect -> "BK_effect") ^ " " ^
+  (pp_format_l_lem l) ^ ")"
 
 let pp_lem_bkind ppf bk = base ppf (pp_format_bkind_lem bk)
 
-let pp_format_kind_lem (K_aux(K_kind(klst),_)) = 
-  "(K_kind [" ^ list_format "; " pp_format_bkind_lem klst ^ "])"
+let pp_format_kind_lem (K_aux(K_kind(klst),l)) = 
+  "(K_aux (K_kind [" ^ list_format "; " pp_format_bkind_lem klst ^ "]) " ^ (pp_format_l_lem l) ^ ")"
 
 let pp_lem_kind ppf k = base ppf (pp_format_kind_lem k)
 
-let rec pp_format_typ_lem (Typ_aux(t,_)) =
-  match t with
-  | Typ_id(id) -> "(Typ_id " ^ pp_format_id_lem id ^ ")"
-  | Typ_var(var) -> "(Typ_var " ^ pp_format_var_lem var ^ ")"
-  | Typ_fn(arg,ret,efct) -> "(Typ_fn " ^ pp_format_typ_lem arg ^ " " ^ 
-                             pp_format_typ_lem ret ^ " " ^
-                            (pp_format_effects_lem efct) ^ ")"
-  | Typ_tup(typs) -> "(Typ_tup [" ^ (list_format "; " pp_format_typ_lem typs) ^ "])"
-  | Typ_app(id,args) -> "(Typ_app " ^ (pp_format_id_lem id) ^ " [" ^ (list_format "; " pp_format_typ_arg_lem args) ^ "])"
-  | Typ_wild -> "Typ_wild"
-and pp_format_nexp_lem (Nexp_aux(n,_)) = 
-  match n with
-  | Nexp_var(v) -> "(Nexp_var " ^ pp_format_var_lem v ^ ")"
-  | Nexp_constant(i) -> "(Nexp_constant " ^ string_of_int i ^ ")"
-  | Nexp_sum(n1,n2) -> "(Nexp_sum " ^ (pp_format_nexp_lem n1) ^ " " ^ (pp_format_nexp_lem n2) ^ ")"
-  | Nexp_times(n1,n2) -> "(Nexp_times " ^  (pp_format_nexp_lem n1) ^ " " ^ (pp_format_nexp_lem n2) ^ ")"
-  | Nexp_exp(n1) -> "(Nexp_exp " ^ (pp_format_nexp_lem n1) ^ ")"
-and pp_format_ord_lem (Ord_aux(o,_)) = 
-  match o with
-  | Ord_var(v) -> "(Ord_var " ^ pp_format_var_lem v ^ ")"
-  | Ord_inc -> "Ord_inc"
-  | Ord_dec -> "Ord_dec"  
-and pp_format_effects_lem (Effect_aux(e,_)) =
-  match e with
+let rec pp_format_typ_lem (Typ_aux(t,l)) =
+  "(Typ_aux " ^
+  (match t with
+    | Typ_id(id) -> "(Typ_id " ^ pp_format_id_lem id ^ ")"
+    | Typ_var(var) -> "(Typ_var " ^ pp_format_var_lem var ^ ")"
+    | Typ_fn(arg,ret,efct) -> "(Typ_fn " ^ pp_format_typ_lem arg ^ " " ^ 
+                              pp_format_typ_lem ret ^ " " ^
+                              (pp_format_effects_lem efct) ^ ")"
+    | Typ_tup(typs) -> "(Typ_tup [" ^ (list_format "; " pp_format_typ_lem typs) ^ "])"
+    | Typ_app(id,args) -> "(Typ_app " ^ (pp_format_id_lem id) ^ " [" ^ (list_format "; " pp_format_typ_arg_lem args) ^ "])"
+    | Typ_wild -> "Typ_wild") ^ " " ^
+    (pp_format_l_lem l) ^ ")"
+and pp_format_nexp_lem (Nexp_aux(n,l)) = 
+  "(Nexp_aux " ^
+  (match n with
+    | Nexp_var(v) -> "(Nexp_var " ^ pp_format_var_lem v ^ ")"
+    | Nexp_constant(i) -> "(Nexp_constant " ^ string_of_int i ^ ")"
+    | Nexp_sum(n1,n2) -> "(Nexp_sum " ^ (pp_format_nexp_lem n1) ^ " " ^ (pp_format_nexp_lem n2) ^ ")"
+    | Nexp_times(n1,n2) -> "(Nexp_times " ^  (pp_format_nexp_lem n1) ^ " " ^ (pp_format_nexp_lem n2) ^ ")"
+    | Nexp_exp(n1) -> "(Nexp_exp " ^ (pp_format_nexp_lem n1) ^ ")") ^ " " ^
+    (pp_format_l_lem l) ^ ")"
+and pp_format_ord_lem (Ord_aux(o,l)) = 
+  "(Ord_aux " ^ 
+  (match o with
+    | Ord_var(v) -> "(Ord_var " ^ pp_format_var_lem v ^ ")"
+    | Ord_inc -> "Ord_inc"
+    | Ord_dec -> "Ord_dec") ^ " " ^
+   (pp_format_l_lem l) ^ ")"
+and pp_format_base_effect_lem (BE_aux(e,l)) =
+  "(BE_aux " ^
+  (match e with
+    | BE_rreg -> "BE_rreg"
+    | BE_wreg -> "BE_wreg"
+    | BE_rmem -> "BE_rmem"
+    | BE_wmem -> "BE_wmem"
+    | BE_undef -> "BE_undef"
+    | BE_unspec -> "BE_unspec"
+    | BE_nondet -> "BE_nondet") ^ " " ^
+  (pp_format_l_lem l) ^ ")"
+and pp_format_effects_lem (Effect_aux(e,l)) =
+  "(Effect_aux " ^
+  (match e with
   | Effect_var(v) -> "(Effect_var " ^ pp_format_var v ^ ")"
   | Effect_set(efcts) ->
     "(Effect_set [" ^
-      (list_format "; " 
-         (fun (BE_aux(e,l)) ->
-	   match e with
-	   | BE_rreg -> "BE_rreg"
-	   | BE_wreg -> "BE_wreg"
-	   | BE_rmem -> "BE_rmem"
-	   | BE_wmem -> "BE_wmem"
-	   | BE_undef -> "BE_undef"
-	   | BE_unspec -> "BE_unspec"
-	   | BE_nondet -> "BE_nondet")
-	 efcts) ^ " ])"
-and pp_format_typ_arg_lem (Typ_arg_aux(t,_)) = 
-  match t with
+      (list_format "; " pp_format_base_effect_lem efcts) ^ " ])") ^ " " ^
+  (pp_format_l_lem l) ^ ")"
+and pp_format_typ_arg_lem (Typ_arg_aux(t,l)) = 
+  "(Typ_arg_aux " ^
+  (match t with
   | Typ_arg_typ(t) -> "(Typ_arg_typ " ^ pp_format_typ_lem t ^ ")"
   | Typ_arg_nexp(n) -> "(Typ_arg_nexp " ^ pp_format_nexp_lem n ^ ")"
   | Typ_arg_order(o) -> "(Typ_arg_order " ^ pp_format_ord_lem o ^ ")"
-  | Typ_arg_effect(e) -> "(Typ_arg_effect " ^ pp_format_effects_lem e ^ ")"
+  | Typ_arg_effect(e) -> "(Typ_arg_effect " ^ pp_format_effects_lem e ^ ")") ^ " " ^
+  (pp_format_l_lem l) ^ ")"
 
 let pp_lem_typ ppf t = base ppf (pp_format_typ_lem t)
 let pp_lem_nexp ppf n = base ppf (pp_format_nexp_lem n)
 let pp_lem_ord ppf o = base ppf (pp_format_ord_lem o)
 let pp_lem_effects ppf e = base ppf (pp_format_effects_lem e)
+let pp_lem_beffect ppf be = base ppf (pp_format_base_effect_lem be)
 
-let pp_format_nexp_constraint_lem (NC_aux(nc,_)) =
-  match nc with
+let pp_format_nexp_constraint_lem (NC_aux(nc,l)) =
+  "(NC_aux " ^
+  (match nc with
   | NC_fixed(n1,n2) -> "(NC_fixed " ^ pp_format_nexp_lem n1 ^ " " ^ pp_format_nexp_lem n2 ^ ")"
   | NC_bounded_ge(n1,n2) -> "(NC_bounded_ge " ^ pp_format_nexp_lem n1 ^ " " ^ pp_format_nexp_lem n2 ^ ")"
   | NC_bounded_le(n1,n2) -> "(NC_bounded_le " ^ pp_format_nexp_lem n1 ^ " " ^ pp_format_nexp_lem n2 ^ ")"
@@ -436,38 +466,46 @@ let pp_format_nexp_constraint_lem (NC_aux(nc,_)) =
     pp_format_var_lem id ^
       " [" ^
       list_format "; " string_of_int bounds ^
-      "])"
+      "])") ^ " " ^
+  (pp_format_l_lem l) ^ ")"
 
 let pp_lem_nexp_constraint ppf nc = base ppf (pp_format_nexp_constraint_lem nc)
 
-let pp_format_qi_lem (QI_aux(qi,_)) =
-  match qi with
+let pp_format_qi_lem (QI_aux(qi,lq)) =
+  "(QI_aux " ^ 
+  (match qi with
   | QI_const(n_const) -> "(QI_const " ^ pp_format_nexp_constraint_lem n_const ^ ")"
-  | QI_id(KOpt_aux(ki,_)) ->
-    "(QI_id " ^
+  | QI_id(KOpt_aux(ki,lk)) ->
+    "(QI_id (KOpt_aux " ^
     (match ki with
     | KOpt_none(var) -> "(KOpt_none " ^ pp_format_var_lem var ^ ")"
-    | KOpt_kind(k,var) -> "(KOpt_kind " ^ pp_format_kind_lem k ^ " " ^ pp_format_var_lem var ^ ")") ^ ")"
+    | KOpt_kind(k,var) -> "(KOpt_kind " ^ pp_format_kind_lem k ^ " " ^ pp_format_var_lem var ^ ")") ^ " " ^
+      (pp_format_l_lem lk) ^ "))") ^ " " ^ 
+  (pp_format_l_lem lq) ^ ")"
 
 let pp_lem_qi ppf qi = base ppf (pp_format_qi_lem qi)
 
-let pp_format_typquant_lem (TypQ_aux(tq,_)) =
-  match tq with
+let pp_format_typquant_lem (TypQ_aux(tq,l)) =
+  "(TypQ_aux " ^ 
+  (match tq with
   | TypQ_no_forall -> "TypQ_no_forall"
   | TypQ_tq(qlist) ->
     "(TypQ_tq [" ^ 
     (list_format "; " pp_format_qi_lem qlist) ^
-    "])"
+    "])") ^ " " ^ 
+  (pp_format_l_lem l) ^ ")"
 
 let pp_lem_typquant ppf tq = base ppf (pp_format_typquant_lem tq)
 
-let pp_format_typscm_lem (TypSchm_aux(TypSchm_ts(tq,t),_)) =
-  "(TypSchm_ts " ^ (pp_format_typquant_lem tq) ^ " " ^ pp_format_typ_lem t ^ ")"
+let pp_format_typscm_lem (TypSchm_aux(TypSchm_ts(tq,t),l)) =
+  "(TypSchm_aux (TypSchm_ts " ^ (pp_format_typquant_lem tq) ^ " " ^ pp_format_typ_lem t ^ ") " ^
+                (pp_format_l_lem l) ^ ")"
  
 let pp_lem_typscm ppf ts = base ppf (pp_format_typscm_lem ts)
 
-let pp_format_lit_lem (L_aux(l,_)) =
-  match l with
+let pp_format_lit_lem (L_aux(lit,l)) =
+  "(L_aux " ^
+  (match lit with
   | L_unit -> "L_unit"
   | L_zero -> "L_zero"
   | L_one -> "L_one"
@@ -477,12 +515,81 @@ let pp_format_lit_lem (L_aux(l,_)) =
   | L_hex(n) -> "(L_hex \"" ^ n ^ "\")"
   | L_bin(n) -> "(L_bin \"" ^ n ^ "\")"
   | L_undef -> "L_undef"
-  | L_string(s) -> "(L_string \"" ^ s ^ "\")" 
+  | L_string(s) -> "(L_string \"" ^ s ^ "\")") ^ " " ^
+  (pp_format_l_lem l) ^ ")"
 
 let pp_lem_lit ppf l = base ppf (pp_format_lit_lem l)
 
-let rec pp_format_pat_lem (P_aux(p,l)) =
-  match p with
+
+let rec pp_format_t t =
+  match t.t with
+    | Tid i -> "(T_id (Id_aux (Id \"" ^ i ^ "\") Unknown))"
+    | Tvar i -> "(T_var (Kid_aux (Var \"" ^ i ^ "\") Unknown))"
+    | Tfn(t1,t2,e) -> "(T_fn " ^ (pp_format_t t1) ^ " " ^ (pp_format_t t2) ^ " " ^ pp_format_e e ^ ")"
+    | Ttup(tups) -> "(T_tup [" ^ (list_format "; " pp_format_t tups) ^ "])"
+    | Tapp(i,args) -> "(T_app (Id_aux (Id \"" ^ i ^ "\") Unknown) (T_args [" ^  list_format "; " pp_format_targ args ^ "]))"
+    | Tuvar(_) -> "(T_var (Kid_aux (Var \"fresh_v\") Unknown))"
+and pp_format_targ = function
+  | TA_typ t -> "(T_arg_typ " ^ pp_format_t t ^ ")"
+  | TA_nexp n -> "(T_arg_nexp " ^ pp_format_n n ^ ")"
+  | TA_eft e -> "(T_arg_effect " ^ pp_format_e e ^ ")"
+  | TA_ord o -> "(T_arg_order " ^ pp_format_o o ^ ")"
+and pp_format_n n =
+  match n.nexp with
+    | Nvar i -> "(Ne_var (Kid_aux (Var \"" ^ i ^ "\") Unknown))"
+    | Nconst i -> "(Ne_const " ^ string_of_int i ^ ")"
+    | Nadd(n1,n2) -> "(Ne_add [" ^ (pp_format_n n1) ^ "; " ^ (pp_format_n n2) ^ "])"
+    | Nmult(n1,n2) -> "(Ne_mult " ^ (pp_format_n n1) ^ " " ^ (pp_format_n n2) ^ ")"
+    | N2n n -> "(Ne_exp " ^ (pp_format_n n) ^ ")"
+    | Nneg n -> "(Ne_unary " ^ (pp_format_n n) ^ ")"
+    | Nuvar(_) -> "(Ne_var (Kid_aux (Var \"fresh_v\") Unknown))"
+and pp_format_e e = 
+  "(Effect_aux " ^
+  (match e.effect with
+  | Evar i -> "(Effect_var (Kid_aux (Var \"" ^ i ^ "\") Unknown))"
+  | Eset es -> "(Effect_set [" ^
+                  (list_format "; " pp_format_base_effect_lem es) ^ " ])"
+  | Euvar(_) -> "(Effect_var (Kid_aux (Var \"fresh_v\") Unknown))")
+  ^ " Unknown)"
+and pp_format_o o = 
+  "(Ord_aux " ^ 
+  (match o.order with
+  | Ovar i -> "(Ord_var (Kid_aux (Var \"" ^ i ^ "\") Unknown))"
+  | Oinc -> "Ord_inc"
+  | Odec -> "Ord_dec"
+  | Ouvar(_) -> "(Ord_var (Kid_aux (Var \"fresh_v\") Unknown))")
+  ^ " Unknown)"
+
+let pp_format_tag = function
+  | Emp -> "Tag_empty"
+  | External (Some s) -> "(Tag_extern (Just \""^s^"\"))"
+  | External None -> "(Tag_extern Nothing)"
+  | Default -> "Tag_default"
+  | Constructor -> "Tag_ctor"
+  | Enum -> "Tag_enum"
+  | Spec -> "Tag_spec"
+
+let pp_format_nes nes = 
+  "[" ^ 
+  (list_format "; "
+     (fun ne -> match ne with
+       | LtEq(_,n1,n2) -> "(Nec_lteq " ^ pp_format_n n1 ^ " " ^ pp_format_n n2 ^ ")"
+       | Eq(_,n1,n2) -> "(Nec_eq " ^ pp_format_n n1 ^ " " ^ pp_format_n n2 ^ ")"
+       | GtEq(_,n1,n2) -> "(Nec_gteq " ^ pp_format_n n1 ^ " " ^ pp_format_n n2 ^ ")"
+       | In(_,i,ns) -> "(Nec_in (Kid_aux (Var \"" ^ i ^ "\") Unknown) [" ^ (list_format "; " string_of_int ns)^ "])")
+     nes) ^ "]"
+
+let pp_format_annot = function
+  | None -> "Nothing"
+  | Some((_,t),tag,nes,efct) -> 
+    "(Just (" ^ pp_format_t t ^ ", " ^ pp_format_tag tag ^ ", " ^ pp_format_nes nes ^ ", " ^ pp_format_e efct ^ "))"
+
+let pp_annot ppf ant = base ppf (pp_format_annot ant)
+
+
+let rec pp_format_pat_lem (P_aux(p,(l,annot))) =
+  "(P_aux " ^
+  (match p with
   | P_lit(lit) -> "(P_lit " ^ pp_format_lit_lem lit ^ ")"
   | P_wild -> "P_wild"
   | P_id(id) -> "(P_id " ^ pp_format_id_lem id ^ ")"
@@ -499,156 +606,182 @@ let rec pp_format_pat_lem (P_aux(p,l)) =
     "(P_vector_indexed [" ^ list_format "; " (fun (i,p) -> Printf.sprintf "(%d, %s)" i (pp_format_pat_lem p)) ipats ^ "])"
   | P_vector_concat(pats) -> "(P_vector_concat [" ^ list_format "; " pp_format_pat_lem pats ^ "])"
   | P_tup(pats) -> "(P_tup [" ^ (list_format "; " pp_format_pat_lem pats) ^ "])"
-  | P_list(pats) -> "(P_list [" ^ (list_format "; " pp_format_pat_lem pats) ^ "])"
+  | P_list(pats) -> "(P_list [" ^ (list_format "; " pp_format_pat_lem pats) ^ "])") ^ 
+  " (" ^ pp_format_l_lem l ^ ", " ^ pp_format_annot annot ^ "))"
 
 let pp_lem_pat ppf p = base ppf (pp_format_pat_lem p)
 
-let rec pp_lem_let ppf (LB_aux(lb,_)) =
-  match lb with
-  | LB_val_explicit(ts,pat,exp) -> 
-    fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "LB_val_explicit" pp_lem_typscm ts pp_lem_pat pat pp_lem_exp exp
-  | LB_val_implicit(pat,exp) -> 
-    fprintf ppf "@[<0>(%a %a %a)@]" kwd "LB_val_implicit" pp_lem_pat pat  pp_lem_exp exp
-
-and pp_lem_exp ppf (E_aux(e,_)) = 
-  match e with
-  | E_block(exps) -> fprintf ppf "@[<0>%a [%a] %a@]"
+let rec pp_lem_let ppf (LB_aux(lb,(l,annot))) =
+  let print_lb ppf lb = 
+    match lb with
+      | LB_val_explicit(ts,pat,exp) -> 
+	fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "LB_val_explicit" pp_lem_typscm ts pp_lem_pat pat pp_lem_exp exp
+      | LB_val_implicit(pat,exp) -> 
+	fprintf ppf "@[<0>(%a %a %a)@]" kwd "LB_val_implicit" pp_lem_pat pat  pp_lem_exp exp in
+  fprintf ppf "@[<0>(LB_aux %a (%a, %a))@]" print_lb lb pp_lem_l l pp_annot annot
+
+and pp_lem_exp ppf (E_aux(e,(l,annot))) = 
+  let print_e ppf e = 
+    match e with
+      | E_block(exps) -> fprintf ppf "@[<0>%a [%a] %a@]"
                                  kwd "(E_block" 
                                  (list_pp pp_semi_lem_exp pp_lem_exp) exps
                                  kwd ")"
-  | E_id(id) -> fprintf ppf "(%a %a)" kwd "E_id" pp_lem_id id
-  | E_lit(lit) -> fprintf ppf "(%a %a)" kwd "E_lit" pp_lem_lit lit
-  | E_cast(typ,exp) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "E_cast" pp_lem_typ typ pp_lem_exp exp 
-  | E_app(f,args) -> fprintf ppf "@[<0>(%a %a [%a])@]" kwd "E_app" pp_lem_id f (list_pp pp_semi_lem_exp pp_lem_exp) args
-  | E_app_infix(l,op,r) -> fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "E_app_infix" pp_lem_exp l pp_lem_id op pp_lem_exp r
-  | E_tuple(exps) -> fprintf ppf "@[<0>%a [%a] %a@]" kwd "(E_tuple" (list_pp pp_semi_lem_exp pp_lem_exp) exps kwd ")"
-  | E_if(c,t,e) -> fprintf ppf "@[<0>(%a %a @[<1>%a@] @[<1> %a@])@]" kwd "E_if" pp_lem_exp c pp_lem_exp t pp_lem_exp e
-  | E_for(id,exp1,exp2,exp3,order,exp4) ->
-    fprintf ppf "@[<0>(%a %a %a %a %a %a @ @[<1> %a @])@]" 
-      kwd "E_for" pp_lem_id id pp_lem_exp exp1 pp_lem_exp exp2 pp_lem_exp exp3 pp_lem_ord order pp_lem_exp exp4
-  | E_vector(exps) -> fprintf ppf "@[<0>(%a [%a])@]" kwd "E_vector" (list_pp pp_semi_lem_exp pp_lem_exp) exps
-  | E_vector_indexed(iexps) -> 
-    let iformat ppf (i,e) = fprintf ppf "@[<1>(%i %a %a) %a@]" i kwd ", " pp_lem_exp e kwd ";" in
-    let lformat ppf (i,e) = fprintf ppf "@[<1>(%i %a %a) @]" i kwd ", " pp_lem_exp e in
-    fprintf ppf "@[<0>(%a [%a]) @]" kwd "E_vector_indexed" (list_pp iformat lformat) iexps
-  | E_vector_access(v,e) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "E_vector_access" pp_lem_exp v pp_lem_exp e
-  | E_vector_subrange(v,e1,e2) -> 
-    fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "E_vector_subrange" pp_lem_exp v pp_lem_exp e1 pp_lem_exp e1 
-  | E_vector_update(v,e1,e2) -> 
-    fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "E_vector_update" pp_lem_exp v pp_lem_exp e1 pp_lem_exp e2
-  | E_vector_update_subrange(v,e1,e2,e3) -> 
-    fprintf ppf "@[<0>(%a %a %a %a %a)@]" kwd "E_vector_update_subrange" pp_lem_exp v pp_lem_exp e1 pp_lem_exp e2 pp_lem_exp e3 
-  | E_list(exps) -> fprintf ppf "@[<0>(%a [%a])@]" kwd "E_list" (list_pp pp_semi_lem_exp pp_lem_exp) exps
-  | E_cons(e1,e2) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "E_cons" pp_lem_exp e1 pp_lem_exp e2
-  | E_record(FES_aux(FES_Fexps(fexps,_),_)) -> 
-    fprintf ppf "@[<0>(%a [%a]))@]" kwd "E_record(FES_Fexps" (list_pp pp_semi_lem_fexp pp_lem_fexp) fexps
-  | E_record_update(exp,(FES_aux(FES_Fexps(fexps,_),_))) ->
-    fprintf ppf "@[<0>(%a %a (%a [%a]))@]" 
-      kwd "E_record_update" pp_lem_exp exp kwd "FES_Fexps" (list_pp pp_semi_lem_fexp pp_lem_fexp) fexps 
-  | E_field(fexp,id) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "E_field" pp_lem_exp fexp pp_lem_id id
-  | E_case(exp,pexps) -> 
-    fprintf ppf "@[<0>(%a %a [%a])@]" kwd "E_case" pp_lem_exp exp (list_pp pp_semi_lem_case pp_lem_case) pexps
-  | E_let(leb,exp) -> fprintf ppf "@[<0>(%a %a %a) @]" kwd "E_let" pp_lem_let leb pp_lem_exp exp
-  | E_assign(lexp,exp) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "E_assign" pp_lem_lexp lexp pp_lem_exp exp
+      | E_id(id) -> fprintf ppf "(%a %a)" kwd "E_id" pp_lem_id id
+      | E_lit(lit) -> fprintf ppf "(%a %a)" kwd "E_lit" pp_lem_lit lit
+      | E_cast(typ,exp) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "E_cast" pp_lem_typ typ pp_lem_exp exp 
+      | E_app(f,args) -> fprintf ppf "@[<0>(%a %a [%a])@]" kwd "E_app" pp_lem_id f (list_pp pp_semi_lem_exp pp_lem_exp) args
+      | E_app_infix(l,op,r) -> fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "E_app_infix" pp_lem_exp l pp_lem_id op pp_lem_exp r
+      | E_tuple(exps) -> fprintf ppf "@[<0>%a [%a] %a@]" kwd "(E_tuple" (list_pp pp_semi_lem_exp pp_lem_exp) exps kwd ")"
+      | E_if(c,t,e) -> fprintf ppf "@[<0>(%a %a @[<1>%a@] @[<1> %a@])@]" kwd "E_if" pp_lem_exp c pp_lem_exp t pp_lem_exp e
+      | E_for(id,exp1,exp2,exp3,order,exp4) ->
+	fprintf ppf "@[<0>(%a %a %a %a %a %a @ @[<1> %a @])@]" 
+	  kwd "E_for" pp_lem_id id pp_lem_exp exp1 pp_lem_exp exp2 pp_lem_exp exp3 pp_lem_ord order pp_lem_exp exp4
+      | E_vector(exps) -> fprintf ppf "@[<0>(%a [%a])@]" kwd "E_vector" (list_pp pp_semi_lem_exp pp_lem_exp) exps
+      | E_vector_indexed(iexps) -> 
+	let iformat ppf (i,e) = fprintf ppf "@[<1>(%i %a %a) %a@]" i kwd ", " pp_lem_exp e kwd ";" in
+	let lformat ppf (i,e) = fprintf ppf "@[<1>(%i %a %a) @]" i kwd ", " pp_lem_exp e in
+	fprintf ppf "@[<0>(%a [%a]) @]" kwd "E_vector_indexed" (list_pp iformat lformat) iexps
+      | E_vector_access(v,e) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "E_vector_access" pp_lem_exp v pp_lem_exp e
+      | E_vector_subrange(v,e1,e2) -> 
+	fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "E_vector_subrange" pp_lem_exp v pp_lem_exp e1 pp_lem_exp e1 
+      | E_vector_update(v,e1,e2) -> 
+	fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "E_vector_update" pp_lem_exp v pp_lem_exp e1 pp_lem_exp e2
+      | E_vector_update_subrange(v,e1,e2,e3) -> 
+	fprintf ppf "@[<0>(%a %a %a %a %a)@]" kwd "E_vector_update_subrange" pp_lem_exp v pp_lem_exp e1 pp_lem_exp e2 pp_lem_exp e3 
+      | E_list(exps) -> fprintf ppf "@[<0>(%a [%a])@]" kwd "E_list" (list_pp pp_semi_lem_exp pp_lem_exp) exps
+      | E_cons(e1,e2) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "E_cons" pp_lem_exp e1 pp_lem_exp e2
+      | E_record(FES_aux(FES_Fexps(fexps,_),_)) -> 
+	fprintf ppf "@[<0>(%a [%a]))@]" kwd "E_record(FES_Fexps" (list_pp pp_semi_lem_fexp pp_lem_fexp) fexps
+      | E_record_update(exp,(FES_aux(FES_Fexps(fexps,_),_))) ->
+	fprintf ppf "@[<0>(%a %a (%a [%a]))@]" 
+	  kwd "E_record_update" pp_lem_exp exp kwd "FES_Fexps" (list_pp pp_semi_lem_fexp pp_lem_fexp) fexps 
+      | E_field(fexp,id) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "E_field" pp_lem_exp fexp pp_lem_id id
+      | E_case(exp,pexps) -> 
+	fprintf ppf "@[<0>(%a %a [%a])@]" kwd "E_case" pp_lem_exp exp (list_pp pp_semi_lem_case pp_lem_case) pexps
+      | E_let(leb,exp) -> fprintf ppf "@[<0>(%a %a %a) @]" kwd "E_let" pp_lem_let leb pp_lem_exp exp
+      | E_assign(lexp,exp) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "E_assign" pp_lem_lexp lexp pp_lem_exp exp
+  in
+  fprintf ppf "@[<0>(E_aux %a (%a, %a))@]" print_e e pp_lem_l l pp_annot annot
 
 and pp_semi_lem_exp ppf e = fprintf ppf "@[<1>%a%a@]" pp_lem_exp e kwd ";"
 
-and pp_lem_fexp ppf (FE_aux(FE_Fexp(id,exp),_)) = fprintf ppf "@[<1>(%a %a %a)@]" kwd "FE_Fexp" pp_lem_id id pp_lem_exp exp
+and pp_lem_fexp ppf (FE_aux(FE_Fexp(id,exp),(l,annot))) = 
+  fprintf ppf "@[<1>(FE_aux (%a %a %a) (%a, %a))@]" kwd "FE_Fexp" pp_lem_id id pp_lem_exp exp pp_lem_l l pp_annot annot
 and pp_semi_lem_fexp ppf fexp = fprintf ppf "@[<1>%a %a@]" pp_lem_fexp fexp kwd ";"
 
-and pp_lem_case ppf (Pat_aux(Pat_exp(pat,exp),_)) = 
-  fprintf ppf "@[<1>(%a %a@ %a)@]" kwd "Pat_exp" pp_lem_pat pat pp_lem_exp exp
+and pp_lem_case ppf (Pat_aux(Pat_exp(pat,exp),(l,annot))) = 
+  fprintf ppf "@[<1>(Pat_aux (%a %a@ %a) (%a, %a))@]" kwd "Pat_exp" pp_lem_pat pat pp_lem_exp exp pp_lem_l l pp_annot annot
 and pp_semi_lem_case ppf case = fprintf ppf "@[<1>%a %a@]" pp_lem_case case kwd ";"
 
-and pp_lem_lexp ppf (LEXP_aux(lexp,_)) =
-  match lexp with
-  | LEXP_id(id) -> fprintf ppf "(%a %a)" kwd "LEXP_id" pp_lem_id id
-  | LEXP_memory(id,args) -> fprintf ppf "(%a %a [%a])" kwd "LEXP_memory" pp_lem_id id (list_pp pp_semi_lem_exp pp_lem_exp) args
-  | LEXP_vector(v,exp) -> fprintf ppf "@[(%a %a %a)@]" kwd "LEXP_vector" pp_lem_lexp v pp_lem_exp exp
-  | LEXP_vector_range(v,e1,e2) -> 
-    fprintf ppf "@[(%a %a %a %a)@]" kwd "LEXP_vector_range" pp_lem_lexp v  pp_lem_exp e1 pp_lem_exp e2
-  | LEXP_field(v,id) -> fprintf ppf "@[(%a %a %a)@]" kwd "LEXP_field" pp_lem_lexp v pp_lem_id id
-
-let pp_lem_default ppf (DT_aux(df,_)) =
-  match df with
-  | DT_kind(bk,var) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "DT_kind" pp_lem_bkind bk pp_lem_var var
-  | DT_typ(ts,id) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "DT_typ" pp_lem_typscm ts pp_lem_id id
-
-let pp_lem_spec ppf (VS_aux(v,_)) =
-  match v with
-  | VS_val_spec(ts,id) -> fprintf ppf "@[<0>(%a %a %a)@]@\n" kwd "VS_val_spec" pp_lem_typscm ts pp_lem_id id
-  | VS_extern_spec(ts,id,s) -> fprintf ppf "@[<0>(%a %a %a \"%s\")@]@\n" kwd "VS_extern_spec" pp_lem_typscm ts pp_lem_id id s
-  | VS_extern_no_rename(ts,id) -> fprintf ppf "@[<0>(%a %a %a)@]@\n" kwd "VS_extern_no_rename" pp_lem_typscm ts pp_lem_id id
-
-let pp_lem_namescm ppf (Name_sect_aux(ns,_)) =
+and pp_lem_lexp ppf (LEXP_aux(lexp,(l,annot))) =
+  let print_le ppf lexp = 
+    match lexp with
+      | LEXP_id(id) -> fprintf ppf "(%a %a)" kwd "LEXP_id" pp_lem_id id
+      | LEXP_memory(id,args) -> fprintf ppf "(%a %a [%a])" kwd "LEXP_memory" pp_lem_id id (list_pp pp_semi_lem_exp pp_lem_exp) args
+      | LEXP_vector(v,exp) -> fprintf ppf "@[(%a %a %a)@]" kwd "LEXP_vector" pp_lem_lexp v pp_lem_exp exp
+      | LEXP_vector_range(v,e1,e2) -> 
+	fprintf ppf "@[(%a %a %a %a)@]" kwd "LEXP_vector_range" pp_lem_lexp v  pp_lem_exp e1 pp_lem_exp e2
+      | LEXP_field(v,id) -> fprintf ppf "@[(%a %a %a)@]" kwd "LEXP_field" pp_lem_lexp v pp_lem_id id
+  in
+  fprintf ppf "@[(LEXP_aux %a (%a, %a))@]" print_le lexp pp_lem_l l pp_annot annot
+
+let pp_lem_default ppf (DT_aux(df,(l,annot))) =
+  let print_de ppf df =
+    match df with
+      | DT_kind(bk,var) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "DT_kind" pp_lem_bkind bk pp_lem_var var
+      | DT_typ(ts,id) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "DT_typ" pp_lem_typscm ts pp_lem_id id
+  in
+  fprintf ppf "@[<0>(DT_aux %a (%a, %a))@]" print_de df pp_lem_l l pp_annot annot
+
+let pp_lem_spec ppf (VS_aux(v,(l,annot))) =
+  let print_spec ppf v =
+    match v with
+      | VS_val_spec(ts,id) -> fprintf ppf "@[<0>(%a %a %a)@]@\n" kwd "VS_val_spec" pp_lem_typscm ts pp_lem_id id
+      | VS_extern_spec(ts,id,s) -> fprintf ppf "@[<0>(%a %a %a \"%s\")@]@\n" kwd "VS_extern_spec" pp_lem_typscm ts pp_lem_id id s
+      | VS_extern_no_rename(ts,id) -> fprintf ppf "@[<0>(%a %a %a)@]@\n" kwd "VS_extern_no_rename" pp_lem_typscm ts pp_lem_id id
+  in
+  fprintf ppf "@[<0>(VS_aux %a (%a, %a))@]" print_spec v pp_lem_l l pp_annot annot
+
+let pp_lem_namescm ppf (Name_sect_aux(ns,l)) =
   match ns with
-  | Name_sect_none -> fprintf ppf "Name_sect_none"
-  | Name_sect_some(s) -> fprintf ppf "(%a \"%s\")" kwd "Name_sect_some" s
+  | Name_sect_none -> fprintf ppf "(Name_sect_aux Name_sect_none %a)" pp_lem_l l
+  | Name_sect_some(s) -> fprintf ppf "(Name_sect_aux (Name_sect_some \"%s\") %a)" s pp_lem_l l
 
-let rec pp_lem_range ppf (BF_aux(r,_)) =
+let rec pp_lem_range ppf (BF_aux(r,l)) =
   match r with 
-  | BF_single(i) -> fprintf ppf "(BF_single %i)" i
-  | BF_range(i1,i2) -> fprintf ppf "(BF_range %i %i)" i1 i2
-  | BF_concat(ir1,ir2) -> fprintf ppf "(%a %a %a)" kwd "BF_concat" pp_lem_range ir1 pp_lem_range ir2
-
-let pp_lem_typdef ppf (TD_aux(td,_)) =
-  match td with
-  | TD_abbrev(id,namescm,typschm) -> 
-    fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "TD_abbrev" pp_lem_id id pp_lem_namescm namescm pp_lem_typscm typschm
-  | TD_record(id,nm,typq,fs,_) -> 
-    let f_pp ppf (typ,id) =
-      fprintf ppf "@[<1>(%a, %a)%a@]" pp_lem_typ typ pp_lem_id id kwd ";" in
-    fprintf ppf "@[<0>(%a %a %a %a [%a] false)@]" 
-      kwd "TD_record" pp_lem_id id pp_lem_namescm nm pp_lem_typquant typq (list_pp f_pp f_pp) fs
-  | TD_variant(id,nm,typq,ar,_) ->
-    let a_pp ppf (Tu_aux(typ_u,_)) = 
-      match typ_u with
-      | Tu_ty_id(typ,id) -> fprintf ppf "@[<1>(Tu_ty_id %a %a);@]" pp_lem_typ typ pp_lem_id id 
-      | Tu_id(id) -> fprintf ppf "@[<1>(Tu_id %a);@]" pp_lem_id id
-    in
-    fprintf ppf "@[<0>(%a %a %a %a [%a] false)@]" 
-      kwd "TD_variant" pp_lem_id id pp_lem_namescm nm pp_lem_typquant typq (list_pp a_pp a_pp) ar 
-  | TD_enum(id,ns,enums,_) ->
-    let pp_id_semi ppf id = fprintf ppf "%a%a " pp_lem_id id kwd ";" in
-    fprintf ppf "@[<0>(%a %a %a [%a] false)@]"
-      kwd "TD_enum" pp_lem_id id pp_lem_namescm ns (list_pp pp_id_semi pp_lem_id) enums
-  | TD_register(id,n1,n2,rs) -> 
-    let pp_rid ppf (r,id) = fprintf ppf "(%a, %a)%a " pp_lem_range r pp_lem_id id kwd ";" in
-    let pp_rids = (list_pp pp_rid pp_rid) in
-    fprintf ppf "@[<0>(%a %a %a %a [%a])@]"
-     kwd "TD_register" pp_lem_id id pp_lem_nexp n1 pp_lem_nexp n2 pp_rids rs
-
-let pp_lem_rec ppf (Rec_aux(r,_)) =
+  | BF_single(i) -> fprintf ppf "(BF_aux (BF_single %i) %a)" i pp_lem_l l
+  | BF_range(i1,i2) -> fprintf ppf "(BF_aux (BF_range %i %i) %a)" i1 i2 pp_lem_l l
+  | BF_concat(ir1,ir2) -> fprintf ppf "(BF_aux (BF_concat %a %a) %a)" pp_lem_range ir1 pp_lem_range ir2 pp_lem_l l
+
+let pp_lem_typdef ppf (TD_aux(td,(l,annot))) =
+  let print_td ppf td = 
+    match td with
+      | TD_abbrev(id,namescm,typschm) -> 
+	fprintf ppf "@[<0>(%a %a %a %a)@]" kwd "TD_abbrev" pp_lem_id id pp_lem_namescm namescm pp_lem_typscm typschm
+      | TD_record(id,nm,typq,fs,_) -> 
+	let f_pp ppf (typ,id) =
+	  fprintf ppf "@[<1>(%a, %a)%a@]" pp_lem_typ typ pp_lem_id id kwd ";" in
+	fprintf ppf "@[<0>(%a %a %a %a [%a] false)@]" 
+	  kwd "TD_record" pp_lem_id id pp_lem_namescm nm pp_lem_typquant typq (list_pp f_pp f_pp) fs
+      | TD_variant(id,nm,typq,ar,_) ->
+	let a_pp ppf (Tu_aux(typ_u,l)) = 
+	  match typ_u with
+	    | Tu_ty_id(typ,id) -> fprintf ppf "@[<1>(Tu_aux (Tu_ty_id %a %a) %a);@]" 
+	                          pp_lem_typ typ pp_lem_id id pp_lem_l l
+	    | Tu_id(id) -> fprintf ppf "@[<1>(Tu_aux (Tu_id %a) %a);@]" pp_lem_id id pp_lem_l l
+	in
+	fprintf ppf "@[<0>(%a %a %a %a [%a] false)@]" 
+	  kwd "TD_variant" pp_lem_id id pp_lem_namescm nm pp_lem_typquant typq (list_pp a_pp a_pp) ar 
+      | TD_enum(id,ns,enums,_) ->
+	let pp_id_semi ppf id = fprintf ppf "%a%a " pp_lem_id id kwd ";" in
+	fprintf ppf "@[<0>(%a %a %a [%a] false)@]"
+	  kwd "TD_enum" pp_lem_id id pp_lem_namescm ns (list_pp pp_id_semi pp_lem_id) enums
+      | TD_register(id,n1,n2,rs) -> 
+	let pp_rid ppf (r,id) = fprintf ppf "(%a, %a)%a " pp_lem_range r pp_lem_id id kwd ";" in
+	let pp_rids = (list_pp pp_rid pp_rid) in
+	fprintf ppf "@[<0>(%a %a %a %a [%a])@]"
+	  kwd "TD_register" pp_lem_id id pp_lem_nexp n1 pp_lem_nexp n2 pp_rids rs
+  in
+  fprintf ppf "@[<0>(TD_aux %a (%a, %a))@]" print_td td pp_lem_l l pp_annot annot
+
+let pp_lem_rec ppf (Rec_aux(r,l)) =
   match r with
-  | Rec_nonrec -> fprintf ppf "Rec_nonrec"
-  | Rec_rec -> fprintf ppf "Rec_rec"
-
-let pp_lem_tannot_opt ppf (Typ_annot_opt_aux(t,_)) =
+  | Rec_nonrec -> fprintf ppf "(Rec_aux Rec_nonrec %a)" pp_lem_l l
+  | Rec_rec -> fprintf ppf "(Rec_aux Rec_rec %a)" pp_lem_l l
+  
+let pp_lem_tannot_opt ppf (Typ_annot_opt_aux(t,l)) =
   match t with
-  | Typ_annot_opt_some(tq,typ) -> fprintf ppf "(Typ_annot_opt_some %a %a)" pp_lem_typquant tq pp_lem_typ typ
+  | Typ_annot_opt_some(tq,typ) -> 
+    fprintf ppf "(Typ_annot_opt_aux (Typ_annot_opt_some %a %a) %a)" pp_lem_typquant tq pp_lem_typ typ pp_lem_l l
 
-let pp_lem_effects_opt ppf (Effect_opt_aux(e,_)) =
+let pp_lem_effects_opt ppf (Effect_opt_aux(e,l)) =
   match e with
-  | Effect_opt_pure -> fprintf ppf "Effect_opt_pure"
-  | Effect_opt_effect e -> fprintf ppf "(Effect_opt_effect %a)" pp_lem_effects e
+  | Effect_opt_pure -> fprintf ppf "(Effect_opt_aux Effect_opt_pure %a)" pp_lem_l l
+  | Effect_opt_effect e -> fprintf ppf "(Effect_opt_aux (Effect_opt_effect %a) %a)" pp_lem_effects e pp_lem_l l
 
-let pp_lem_funcl ppf (FCL_aux(FCL_Funcl(id,pat,exp),_)) =
-  fprintf ppf "@[<0>(%a %a %a %a)@]@\n" kwd "FCL_Funcl" pp_lem_id id pp_lem_pat pat pp_lem_exp exp 
+let pp_lem_funcl ppf (FCL_aux(FCL_Funcl(id,pat,exp),(l,annot))) =
+  fprintf ppf "@[<0>(FCL_aux (%a %a %a %a) (%a, %a))@]@\n" 
+    kwd "FCL_Funcl" pp_lem_id id pp_lem_pat pat pp_lem_exp exp pp_lem_l l pp_annot annot
 
-let pp_lem_fundef ppf (FD_aux(FD_function(r, typa, efa, fcls),_)) =
+let pp_lem_fundef ppf (FD_aux(FD_function(r, typa, efa, fcls),(l,annot))) =
   let pp_funcls ppf funcl = fprintf ppf "%a %a" pp_lem_funcl funcl kwd ";" in
-  fprintf ppf "@[<0>(%a %a %a %a [%a])@]" 
+  fprintf ppf "@[<0>(FD_aux (%a %a %a %a [%a]) (%a, %a))@]" 
     kwd "FD_function" pp_lem_rec r pp_lem_tannot_opt typa pp_lem_effects_opt efa (list_pp pp_funcls pp_funcls) fcls
-
-let pp_lem_def ppf (DEF_aux(d,(l,_))) =
-  match d with
-  | DEF_default(df) -> fprintf ppf "(DEF_default %a);@\n" pp_lem_default df
-  | DEF_spec(v_spec) -> fprintf ppf "(DEF_spec %a);@\n" pp_lem_spec v_spec
-  | DEF_type(t_def) -> fprintf ppf "(DEF_type %a);@\n" pp_lem_typdef t_def
-  | DEF_fundef(f_def) -> fprintf ppf "(DEF_fundef %a);@\n" pp_lem_fundef f_def
-  | DEF_val(lbind) -> fprintf ppf "(DEF_val %a);@\n" pp_lem_let lbind
-  | DEF_reg_dec(typ,id) -> fprintf ppf "@[<0>(%a %a %a)@];@\n" kwd "DEF_reg_dec" pp_lem_typ typ pp_lem_id id
-  | _ -> raise (Reporting_basic.err_unreachable l "initial_check didn't remove all scattered Defs")
+    pp_lem_l l pp_annot annot
+
+let pp_lem_def ppf (DEF_aux(d,(l,annot))) =
+  let print_d ppf d = 
+    match d with
+      | DEF_default(df) -> fprintf ppf "(DEF_default %a)" pp_lem_default df
+      | DEF_spec(v_spec) -> fprintf ppf "(DEF_spec %a)" pp_lem_spec v_spec
+      | DEF_type(t_def) -> fprintf ppf "(DEF_type %a)" pp_lem_typdef t_def
+      | DEF_fundef(f_def) -> fprintf ppf "(DEF_fundef %a)" pp_lem_fundef f_def
+      | DEF_val(lbind) -> fprintf ppf "(DEF_val %a)" pp_lem_let lbind
+      | DEF_reg_dec(typ,id) -> fprintf ppf "@[<0>(%a %a %a)@]" kwd "DEF_reg_dec" pp_lem_typ typ pp_lem_id id
+      | _ -> raise (Reporting_basic.err_unreachable l "initial_check didn't remove all scattered Defs")
+  in
+  fprintf ppf "@[<0>(DEF_aux %a (%a, %a))@];@\n" print_d d pp_lem_l l pp_annot annot
 
 let pp_lem_defs ppf (Defs(defs)) =
   fprintf ppf "Defs [@[%a@]]@\n" (list_pp pp_lem_def pp_lem_def) defs