Reduce redundant information in AST

5 files changed, 140 insertions, 136 deletions

diff --git a/src/initial_check.ml b/src/initial_check.ml
index 78e44bf0..709eb42b 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -434,10 +434,10 @@ let to_ast_default (names, k_env, t_env) (default : Parse_ast.default_typing_spe
       let k,k_typ = to_ast_base_kind bk in
       let v = to_ast_var v in
       let key = var_to_string v in
-      DT_aux(DT_kind(k,v),(l,None)),(names,(Envmap.insert k_env (key,k_typ)),t_env)
+      DT_aux(DT_kind(k,v),l),(names,(Envmap.insert k_env (key,k_typ)),t_env)
     | Parse_ast.DT_typ(typschm,id) ->
       let tps,_,_ = to_ast_typschm k_env typschm in
-      DT_aux(DT_typ(tps,to_ast_id id),(l,None)),(names,k_env,t_env) (* Does t_env need to be updated here in this pass? *)
+      DT_aux(DT_typ(tps,to_ast_id id),l),(names,k_env,t_env) (* Does t_env need to be updated here in this pass? *)
     )
 
 let to_ast_spec (names,k_env,t_env) (val_:Parse_ast.val_spec) : (tannot val_spec) envs_out =
@@ -547,7 +547,7 @@ let to_ast_effects_opt (k_env : kind Envmap.t) (Parse_ast.Effect_opt_aux(e,l)) :
 
 let to_ast_funcl (names,k_env,t_env) (Parse_ast.FCL_aux(fcl,l) : Parse_ast.funcl) : (tannot funcl) =
   match fcl with
-  | Parse_ast.FCL_Funcl(id,pat,exp) -> FCL_aux(FCL_Funcl(to_ast_id id, to_ast_pat k_env pat, to_ast_exp k_env exp),(l,None))
+  | Parse_ast.FCL_Funcl(id,pat,exp) -> FCL_aux(FCL_Funcl(to_ast_id id, to_ast_pat k_env pat, to_ast_exp k_env exp),l)
 
 let to_ast_fundef  (names,k_env,t_env) (Parse_ast.FD_aux(fd,l):Parse_ast.fundef) : (tannot fundef) envs_out = 
   match fd with
@@ -569,92 +569,93 @@ let rec def_in_progress (id : id) (partial_defs : (id * partial_def) list) : par
     (match n,id with
     | Id_aux(Id(n),_), Id_aux(Id(i),_) -> if (n = i) then Some(pd) else def_in_progress id defs
     | _,_ -> def_in_progress id defs)
+
+let to_ast_dec (names,k_env,t_env) (Parse_ast.DEC_aux(Parse_ast.DEC_reg(typ,id),l)) =
+  let t = to_ast_typ k_env typ in
+  let id = to_ast_id id in
+  (DEC_aux(DEC_reg(t,id),(l,None)))
       
 let to_ast_def (names, k_env, t_env) partial_defs def : def_progress envs_out * (id * partial_def) list = 
   let envs = (names,k_env,t_env) in
   match def with
-  | Parse_ast.DEF_aux(d,l) ->
-    (match d with
-    | Parse_ast.DEF_type(t_def) -> 
-      let td,envs = to_ast_typedef envs t_def in
-      ((Finished(DEF_aux(DEF_type(td),(l,None)))),envs),partial_defs
-    | Parse_ast.DEF_fundef(f_def) -> 
-      let fd,envs = to_ast_fundef envs f_def in
-      ((Finished(DEF_aux(DEF_fundef(fd),(l,None)))),envs),partial_defs
-    | Parse_ast.DEF_val(lbind) -> 
-      let lb = to_ast_letbind k_env lbind in
-      ((Finished(DEF_aux(DEF_val(lb),(l,None)))),envs),partial_defs
-    | Parse_ast.DEF_spec(val_spec) -> 
-      let vs,envs = to_ast_spec envs val_spec in
-      ((Finished(DEF_aux(DEF_spec(vs),(l,None)))),envs),partial_defs
-    | Parse_ast.DEF_default(typ_spec) -> 
-      let default,envs = to_ast_default envs typ_spec in
-      ((Finished(DEF_aux(DEF_default(default),(l,None)))),envs),partial_defs
-    | Parse_ast.DEF_reg_dec(typ,id) ->
-      let t = to_ast_typ k_env typ in
+  | Parse_ast.DEF_type(t_def) -> 
+    let td,envs = to_ast_typedef envs t_def in
+    ((Finished(DEF_type(td))),envs),partial_defs
+  | Parse_ast.DEF_fundef(f_def) -> 
+    let fd,envs = to_ast_fundef envs f_def in
+    ((Finished(DEF_fundef(fd))),envs),partial_defs
+  | Parse_ast.DEF_val(lbind) -> 
+    let lb = to_ast_letbind k_env lbind in
+    ((Finished(DEF_val(lb))),envs),partial_defs
+  | Parse_ast.DEF_spec(val_spec) -> 
+    let vs,envs = to_ast_spec envs val_spec in
+    ((Finished(DEF_spec(vs))),envs),partial_defs
+  | Parse_ast.DEF_default(typ_spec) -> 
+    let default,envs = to_ast_default envs typ_spec in
+    ((Finished(DEF_default(default))),envs),partial_defs
+  | Parse_ast.DEF_reg_dec(dec) ->
+    let d = to_ast_dec envs dec in
+    ((Finished(DEF_reg_dec(d))),envs),partial_defs
+  | Parse_ast.DEF_scattered(Parse_ast.SD_aux(sd,l)) ->
+    (match sd with
+    | Parse_ast.SD_scattered_function(rec_opt, tannot_opt, effects_opt, id) ->
+      let rec_opt = to_ast_rec rec_opt in
+      let tannot,k_env',k_local = to_ast_tannot_opt k_env tannot_opt in
+      let effects_opt = to_ast_effects_opt k_env' effects_opt in
       let id = to_ast_id id in
-      ((Finished(DEF_aux(DEF_reg_dec(t,id),(l,None)))),envs),partial_defs (*If tracking types here, update tenv and None*)
-    | Parse_ast.DEF_scattered(Parse_ast.SD_aux(sd,_)) ->
-      (match sd with
-	| Parse_ast.SD_scattered_function(rec_opt, tannot_opt, effects_opt, id) ->
-	  let rec_opt = to_ast_rec rec_opt in
-	  let tannot,k_env',k_local = to_ast_tannot_opt k_env tannot_opt in
-	  let effects_opt = to_ast_effects_opt k_env' effects_opt in
-	  let id = to_ast_id id in
-	  (match (def_in_progress id partial_defs) with
-	    | None -> let partial_def = ref ((DEF_aux(DEF_fundef(FD_aux(FD_function(rec_opt,tannot,effects_opt,[]),(l,None))),(l,None))),false) in
-                      (No_def,envs),((id,(partial_def,k_local))::partial_defs)
-	    | Some(d,k) -> typ_error l "Scattered function definition header name already in use by scattered definition" (Some id) None None)
-	| Parse_ast.SD_scattered_funcl(funcl) -> 
-	  (match funcl with
-	    | Parse_ast.FCL_aux(Parse_ast.FCL_Funcl(id,_,_),_) -> 
-              let id = to_ast_id id in
-              (match (def_in_progress id partial_defs) with
-		| None -> typ_error l "Scattered function definition clause does not match any exisiting function definition headers" (Some id) None None
-		| Some(d,k) ->
-		  (match !d with
-		    | DEF_aux(DEF_fundef(FD_aux(FD_function(r,t,e,fcls),fl)),dl),false -> 
-		      let funcl = to_ast_funcl (names,Envmap.union k k_env,t_env) funcl in 
-		      d:= (DEF_aux(DEF_fundef(FD_aux(FD_function(r,t,e,fcls@[funcl]),fl)),dl),false);
-		      (No_def,envs),partial_defs
-		    | _,true -> typ_error l "Scattered funciton definition clauses extends ended defintion" (Some id) None None
-		    | _ -> typ_error l "Scattered function definition clause matches an existing scattered type definition header" (Some id) None None)))
-	| Parse_ast.SD_scattered_variant(id,naming_scheme_opt,typquant) -> 
-	  let id = to_ast_id id in
-	  let name = to_ast_namescm naming_scheme_opt in
-	  let typq, k_env',_ = to_ast_typquant k_env typquant in
-	  (match (def_in_progress id partial_defs) with
-	    | None -> let partial_def = ref ((DEF_aux(DEF_type(TD_aux(TD_variant(id,name,typq,[],false),(l,None))),(l,None))),false) in
-                      (Def_place_holder(id,l),(names,Envmap.insert k_env ((id_to_string id),{k=K_Typ}),t_env)),(id,(partial_def,k_env'))::partial_defs
-	    | Some(d,k) -> typ_error l "Scattered type definition header name already in use by scattered definition" (Some id) None None)
-	| Parse_ast.SD_scattered_unioncl(id,tu) -> 
-	  let id = to_ast_id id in
-	  (match (def_in_progress id partial_defs) with
-	    | None -> typ_error l "Scattered type definition clause does not match any existing type definition headers" (Some id) None None
-	    | Some(d,k) ->
-              (match !d with
-		| (DEF_aux(DEF_type(TD_aux(TD_variant(id,name,typq,arms,false),tl)),dl), false) -> 
-		  d:= (DEF_aux(DEF_type(TD_aux(TD_variant(id,name,typq,arms@[to_ast_type_union k tu],false),tl)),dl),false);
-		  (No_def,envs),partial_defs
-		| _,true -> typ_error l "Scattered type definition clause extends ended definition" (Some id) None None
-		| _ -> typ_error l "Scattered type definition clause matches an existing scattered function definition header" (Some id) None None))
-	| Parse_ast.SD_scattered_end(id) ->
-	  let id = to_ast_id id in
-	  (match (def_in_progress id partial_defs) with
-	    | None -> typ_error l "Scattered definition end does not match any open scattered definitions" (Some id) None None
-	    | Some(d,k) ->
-              (match !d with
-		| (DEF_aux(DEF_type(_),_) as def),false ->
-		  d:= (def,true);
-		  (No_def,envs),partial_defs
-		| (DEF_aux(DEF_fundef(_),_) as def),false ->
-		  d:= (def,true);
-		  ((Finished def), envs),partial_defs
-		| _, true -> 
-		  typ_error l "Scattered definition ended multiple times" (Some id) None None
-		| _ -> raise (Reporting_basic.err_unreachable l "Something in partial_defs other than fundef and type"))))
-    )
-
+      (match (def_in_progress id partial_defs) with
+      | None -> let partial_def = ref ((DEF_fundef(FD_aux(FD_function(rec_opt,tannot,effects_opt,[]),(l,None)))),false) in
+                (No_def,envs),((id,(partial_def,k_local))::partial_defs)
+      | Some(d,k) -> typ_error l "Scattered function definition header name already in use by scattered definition" (Some id) None None)
+    | Parse_ast.SD_scattered_funcl(funcl) -> 
+      (match funcl with
+      | Parse_ast.FCL_aux(Parse_ast.FCL_Funcl(id,_,_),_) -> 
+        let id = to_ast_id id in
+        (match (def_in_progress id partial_defs) with
+	| None -> typ_error l "Scattered function definition clause does not match any exisiting function definition headers" (Some id) None None
+	| Some(d,k) ->
+	  (match !d with
+	  | DEF_fundef(FD_aux(FD_function(r,t,e,fcls),fl)),false -> 
+	    let funcl = to_ast_funcl (names,Envmap.union k k_env,t_env) funcl in 
+	    d:= DEF_fundef(FD_aux(FD_function(r,t,e,fcls@[funcl]),fl)),false;
+	    (No_def,envs),partial_defs
+	  | _,true -> typ_error l "Scattered funciton definition clauses extends ended defintion" (Some id) None None
+	  | _ -> typ_error l "Scattered function definition clause matches an existing scattered type definition header" (Some id) None None)))
+    | Parse_ast.SD_scattered_variant(id,naming_scheme_opt,typquant) -> 
+      let id = to_ast_id id in
+      let name = to_ast_namescm naming_scheme_opt in
+      let typq, k_env',_ = to_ast_typquant k_env typquant in
+      (match (def_in_progress id partial_defs) with
+      | None -> let partial_def = ref ((DEF_type(TD_aux(TD_variant(id,name,typq,[],false),(l,None)))),false) in
+                (Def_place_holder(id,l),(names,Envmap.insert k_env ((id_to_string id),{k=K_Typ}),t_env)),(id,(partial_def,k_env'))::partial_defs
+      | Some(d,k) -> typ_error l "Scattered type definition header name already in use by scattered definition" (Some id) None None)
+    | Parse_ast.SD_scattered_unioncl(id,tu) -> 
+      let id = to_ast_id id in
+      (match (def_in_progress id partial_defs) with
+      | None -> typ_error l "Scattered type definition clause does not match any existing type definition headers" (Some id) None None
+      | Some(d,k) ->
+        (match !d with
+	| DEF_type(TD_aux(TD_variant(id,name,typq,arms,false),tl)), false -> 
+	  d:= DEF_type(TD_aux(TD_variant(id,name,typq,arms@[to_ast_type_union k tu],false),tl)),false;
+	  (No_def,envs),partial_defs
+	| _,true -> typ_error l "Scattered type definition clause extends ended definition" (Some id) None None
+	| _ -> typ_error l "Scattered type definition clause matches an existing scattered function definition header" (Some id) None None))
+    | Parse_ast.SD_scattered_end(id) ->
+      let id = to_ast_id id in
+      (match (def_in_progress id partial_defs) with
+      | None -> typ_error l "Scattered definition end does not match any open scattered definitions" (Some id) None None
+      | Some(d,k) ->
+        (match !d with
+	| (DEF_type(_) as def),false ->
+	  d:= (def,true);
+	  (No_def,envs),partial_defs
+	| (DEF_fundef(_) as def),false ->
+	  d:= (def,true);
+	  ((Finished def), envs),partial_defs
+	| _, true -> 
+	  typ_error l "Scattered definition ended multiple times" (Some id) None None
+	| _ -> raise (Reporting_basic.err_unreachable l "Something in partial_defs other than fundef and type"))))
+    
 let rec to_ast_defs_helper envs partial_defs = function
   | [] -> ([],envs,partial_defs)
   | d::ds  -> let ((d', envs), partial_defs) = to_ast_def envs partial_defs d in
@@ -675,7 +676,7 @@ let to_ast (default_names : Nameset.t) (kind_env : kind Envmap.t) (typ_env : tan
   List.iter 
     (fun (id,(d,k)) -> 
       (match !d with
-      | (DEF_aux(_,(l,_)),false) -> typ_error l "Scattered definition never ended" (Some id) None None
+      | (d,false) -> typ_error Unknown "Scattered definition never ended" (Some id) None None
       | (_, true) -> ()))
     partial_defs;
   (Defs defs),k_env
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 8e842730..64727503 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -122,7 +122,7 @@ val to_register_fields : defs tannot -> list (id * list (id * index_range))
 let rec to_register_fields (Defs defs) = 
   match defs with
   | [ ] -> [ ]
-  | (DEF_aux def (l,tannot))::defs -> 
+  | def::defs -> 
     match def with 
     | DEF_type (TD_aux (TD_register id n1 n2 indexes) l') ->
       (id,List.map (fun (a,b) -> (b,a)) indexes)::(to_register_fields (Defs defs))
@@ -134,9 +134,9 @@ val to_registers : defs tannot -> env
 let rec to_registers (Defs defs) = 
   match defs with
   | [ ] -> [ ]
-  | (DEF_aux def (l,tannot))::defs -> 
+  | def::defs -> 
     match def with 
-    | DEF_reg_dec typ id -> (id, V_register(Reg id tannot)) :: (to_registers (Defs defs))
+    | DEF_reg_dec (DEC_aux (DEC_reg typ id) (l,tannot)) -> (id, V_register(Reg id tannot)) :: (to_registers (Defs defs))
     | _ -> to_registers (Defs defs)
     end 
   end
@@ -164,7 +164,7 @@ val to_data_constructors : defs tannot -> list (id * typ)
 let rec to_data_constructors (Defs defs) =
   match defs with
   | [] -> []
-  | (DEF_aux def _) :: defs ->
+  | def :: defs ->
     match def with
     | DEF_type (TD_aux t _)->
       match t with 
@@ -426,7 +426,7 @@ let get_funcls id (FD_aux (FD_function _ _ _ fcls) _) =
 let rec find_function (Defs defs) id =
   match defs with 
   | [] -> Nothing
-  | (DEF_aux def _)::defs -> 
+  | def::defs -> 
     match def with
     | DEF_fundef f -> match get_funcls id f with
       | [] -> find_function (Defs defs) id
@@ -1273,13 +1273,13 @@ let rec to_global_letbinds (Defs defs) t_level =
   let  (Env defs' lets regs ctors subregs) = t_level in
   match defs with
   | [] -> ((Value (V_lit (L_aux L_unit Unknown)) Tag_empty, emem, []),t_level)
-  | (DEF_aux def (l,_))::defs ->
+  | def::defs ->
     match def with
     | DEF_val lbind ->
       match interp_letbind t_level [] emem lbind with
       | ((Value v tag,lm,le),_) -> to_global_letbinds (Defs defs) (Env defs' (lets++le) regs ctors subregs)
       | ((Action a s,lm,le),_) -> 
-	((Error l "Top level let may not access memory, registers or (for now) external functions", lm,le),t_level)
+	((Error Unknown "Top level let may not access memory, registers or (for now) external functions", lm,le),t_level)
       | (e,_) -> (e,t_level) end
     | _ -> to_global_letbinds (Defs defs) t_level
     end
diff --git a/src/parser.mly b/src/parser.mly
index 60f50737..06b26765 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -80,7 +80,7 @@ let tdloc td = TD_aux(td, loc())
 let funloc fn = FD_aux(fn, loc())
 let vloc v = VS_aux(v, loc ())
 let sdloc sd = SD_aux(sd, loc ())
-let dloc d = DEF_aux(d,loc ())
+let dloc d = d
 
 let mk_typschm tq t s e = TypSchm_aux((TypSchm_ts(tq,t)),(locn s e))
 let mk_rec i = (Rec_aux((Rec_rec), locn i i))
@@ -1138,7 +1138,7 @@ def:
   | default_typ
     { dloc (DEF_default($1)) }
   | Register atomic_typ id
-    { dloc (DEF_reg_dec($2,$3)) }
+    { dloc (DEF_reg_dec(DEC_aux(DEC_reg($2,$3),loc ()))) }
   | Scattered scattered_def
     { dloc (DEF_scattered $2) }
   | Function_ Clause funcl
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 153147d3..5f86b2ed 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -346,15 +346,18 @@ let pp_fundef ppf (FD_aux(FD_function(r, typa, efa, fcls),_)) =
   fprintf ppf "@[<0>%a %a%a%a @[<1>%a@] @[<1>%a@] @]@\n"
     kwd "function" pp_rec r pp_tannot_opt typa pp_effects_opt efa pp_funcl (List.hd fcls) (list_pp pp_funcls pp_funcls) (List.tl fcls)
 
-let pp_def ppf (DEF_aux(d,(l,_))) =
+let pp_dec ppf (DEC_aux(DEC_reg(typ,id),_)) =
+  fprintf ppf "@[<0>register %a %a@]@\n" pp_typ typ pp_id id
+
+let pp_def ppf d =
   match d with
   | DEF_default(df) -> pp_default ppf df
   | DEF_spec(v_spec) -> pp_spec ppf v_spec
   | DEF_type(t_def) -> pp_typdef ppf t_def
   | DEF_fundef(f_def) -> pp_fundef ppf f_def
   | DEF_val(lbind) -> fprintf ppf "@[<0>%a@]@\n" pp_let lbind
-  | DEF_reg_dec(typ,id) -> fprintf ppf "@[<0>%a %a %a@]@\n" kwd "register" pp_typ typ pp_id id
-  | _ -> raise (Reporting_basic.err_unreachable l "initial_check didn't remove all scattered Defs")
+  | DEF_reg_dec(dec) -> pp_dec ppf dec
+  | _ -> raise (Reporting_basic.err_unreachable Unknown "initial_check didn't remove all scattered Defs")
 
 let pp_defs ppf (Defs(defs)) =
   fprintf ppf "@[%a@]@\n" (list_pp pp_def pp_def) defs
@@ -712,13 +715,13 @@ and pp_lem_lexp ppf (LEXP_aux(lexp,(l,annot))) =
   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 pp_lem_default ppf (DT_aux(df,l)) =
   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
+  fprintf ppf "@[<0>(DT_aux %a %a)@]" print_de df pp_lem_l l
 
 let pp_lem_spec ppf (VS_aux(v,(l,annot))) =
   let print_spec ppf v =
@@ -786,9 +789,9 @@ let pp_lem_effects_opt ppf (Effect_opt_aux(e,l)) =
   | 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),(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_funcl ppf (FCL_aux(FCL_Funcl(id,pat,exp),l)) =
+  fprintf ppf "@[<0>(FCL_aux (%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
 
 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
@@ -796,18 +799,18 @@ let pp_lem_fundef ppf (FD_aux(FD_function(r, typa, efa, fcls),(l,annot))) =
     kwd "FD_function" pp_lem_rec r pp_lem_tannot_opt typa pp_lem_effects_opt efa (list_pp pp_funcls pp_funcls) fcls
     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_dec ppf (DEC_aux(DEC_reg(typ,id),(l,annot))) =
+  fprintf ppf "@[<0>(DEC_aux (DEC_reg %a %a) (%a,%a))@]" pp_lem_typ typ pp_lem_id id pp_lem_l l pp_annot annot
+
+let pp_lem_def 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(dec) -> fprintf ppf "(DEF_reg_dec %a);" pp_lem_dec dec
+  | _ -> raise (Reporting_basic.err_unreachable Unknown "initial_check didn't remove all scattered Defs")
 
 let pp_lem_defs ppf (Defs(defs)) =
   fprintf ppf "Defs [@[%a@]]@\n" (list_pp pp_lem_def pp_lem_def) defs
diff --git a/src/type_check.ml b/src/type_check.ml
index be944d31..2bb5700d 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -1208,13 +1208,13 @@ let check_val_spec envs (VS_aux(vs,(l,annot))) =
       (VS_aux(vs,(l,tannot)),
        Env(d_env,(Envmap.insert t_env (id_to_string id,tannot))))
 
-let check_default envs (DT_aux(ds,(l,annot))) =
+let check_default envs (DT_aux(ds,l)) =
   let (Env(d_env,t_env)) = envs in
   match ds with
-    | DT_kind _ -> ((DT_aux(ds,(l,annot))),envs)
+    | DT_kind _ -> ((DT_aux(ds,l)),envs)
     | DT_typ(typs,id) ->
       let tannot = typschm_to_tannot envs typs Default in
-      (DT_aux(ds,(l,tannot)),
+      (DT_aux(ds,l),
        Env(d_env,(Envmap.insert t_env (id_to_string id,tannot))))
 
 let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,annot))) =
@@ -1224,7 +1224,7 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,
               | Rec_aux(Rec_nonrec,_) -> false
 	      | Rec_aux(Rec_rec,_) -> true in
   let Some(id) = List.fold_right 
-    (fun (FCL_aux((FCL_Funcl(id,pat,exp)),(l,annot))) id' ->
+    (fun (FCL_aux((FCL_Funcl(id,pat,exp)),l)) id' ->
       match id' with
 	| Some(id') -> if id' = id_to_string id then Some(id') 
 	  else typ_error l ("Function declaration expects all definitions to have the same name, " 
@@ -1241,13 +1241,13 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,
       t,p_t,Some((ids,{t=Tfn(p_t,t,ef)}),Emp_global,constraints,ef) in
   let check t_env =
     List.split
-      (List.map (fun (FCL_aux((FCL_Funcl(id,pat,exp)),(l,annot))) ->
+      (List.map (fun (FCL_aux((FCL_Funcl(id,pat,exp)),l)) ->
 	let (pat',t_env',constraints',t') = check_pattern (Env(d_env,t_env)) Emp_local param_t pat in
         (*let _ = Printf.printf "about to check that %s and %s are consistent\n" (t_to_string t') (t_to_string param_t) in*)
 	let exp',_,_,constraints,ef = check_exp (Env(d_env,Envmap.union_merge (tannot_merge (Expr l) d_env) t_env t_env')) ret_t exp in
         (*let _ = Printf.printf "checked function %s : %s -> %s\n" (id_to_string id) (t_to_string param_t) (t_to_string ret_t) in*) 
 	(*let _ = (Pretty_print.pp_exp Format.std_formatter) exp' in*)
-	(FCL_aux((FCL_Funcl(id,pat',exp')),(l,tannot)),((constraints'@constraints),ef))) funcls) in
+	(FCL_aux((FCL_Funcl(id,pat',exp')),l),((constraints'@constraints),ef))) funcls) in
   match (in_env,tannot) with
     | Some(Some( (params,u),Spec,constraints,eft)), Some( (p',t),_,c',eft') ->
       (*let _ = Printf.printf "Function %s is in env\n" id in*)
@@ -1270,24 +1270,24 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,
       Env(d_env,(if is_rec then t_env else Envmap.insert t_env (id,tannot)))
 
 (*val check_def : envs -> tannot def -> (tannot def) envs_out*)
-let check_def envs (DEF_aux(def,(l,annot))) = 
+let check_def envs def = 
   let (Env(d_env,t_env)) = envs in
   match def with
-    | DEF_type tdef -> let td,envs = check_type_def envs tdef in
-		       (DEF_aux((DEF_type td),(l,annot)),envs)
-    | DEF_fundef fdef -> let fd,envs = check_fundef envs fdef in
-			 (DEF_aux(DEF_fundef(fd),(l,annot)),envs)
-    | DEF_val letdef -> let (letbind,t_env_let,_,eft) = check_lbind envs true Emp_global letdef in
-                        (DEF_aux(DEF_val letbind,(l,annot)),Env(d_env,Envmap.union t_env t_env_let))
-    | DEF_spec spec -> let vs,envs = check_val_spec envs spec in
-		       (DEF_aux(DEF_spec(vs),(l,annot)),envs)
-    | DEF_default default -> let ds,envs = check_default envs default in
-			     (DEF_aux((DEF_default(ds)),(l,annot)),envs)
-    | DEF_reg_dec(typ,id) -> 
-      let t = (typ_to_t typ) in
-      let i = id_to_string id in
-      let tannot = into_register d_env (Some(([],t),External (Some i),[],pure_e)) in
-      (DEF_aux(def,(l,tannot)),(Env(d_env,Envmap.insert t_env (i,tannot))))
+  | DEF_type tdef -> let td,envs = check_type_def envs tdef in
+		     (DEF_type td,envs)
+  | DEF_fundef fdef -> let fd,envs = check_fundef envs fdef in
+		       (DEF_fundef fd,envs)
+  | DEF_val letdef -> let (letbind,t_env_let,_,eft) = check_lbind envs true Emp_global letdef in
+                      (DEF_val letbind,Env(d_env,Envmap.union t_env t_env_let))
+  | DEF_spec spec -> let vs,envs = check_val_spec envs spec in
+		     (DEF_spec vs, envs)
+  | DEF_default default -> let ds,envs = check_default envs default in
+			   (DEF_default ds,envs)
+  | DEF_reg_dec(DEC_aux(DEC_reg(typ,id), (l,annot))) -> 
+    let t = (typ_to_t typ) in
+    let i = id_to_string id in
+    let tannot = into_register d_env (Some(([],t),External (Some i),[],pure_e)) in
+    (DEF_reg_dec(DEC_aux(DEC_reg(typ,id),(l,tannot))),(Env(d_env,Envmap.insert t_env (i,tannot))))
 
 
 (*val check : envs ->  tannot defs -> tannot defs*)