Add type annotations to funcls to track effects and constraints from one function-clause

4 files changed, 11 insertions, 13 deletions

diff --git a/src/initial_check.ml b/src/initial_check.ml
index d26f6b84..0c080553 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -646,7 +646,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,def_ord) (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 def_ord pat, to_ast_exp k_env def_ord exp),l)
+    FCL_aux(FCL_Funcl(to_ast_id id, to_ast_pat k_env def_ord pat, to_ast_exp k_env def_ord exp),(l,NoTyp))
 
 let to_ast_fundef  (names,k_env,def_ord) (Parse_ast.FD_aux(fd,l):Parse_ast.fundef) : (tannot fundef) envs_out = 
   match fd with
diff --git a/src/lem_interp/instruction_extractor.lem b/src/lem_interp/instruction_extractor.lem
index 52361911..74e5fd4c 100644
--- a/src/lem_interp/instruction_extractor.lem
+++ b/src/lem_interp/instruction_extractor.lem
@@ -38,11 +38,9 @@ end
 
 let rec extract_effects_of_pat id execute = match execute with
   | [] -> []
-  | FCL_aux (FCL_Funcl _ (P_aux (P_app (Id_aux (Id i) _) _) _) exp) _ :: executes ->
+  | FCL_aux (FCL_Funcl _ (P_aux (P_app (Id_aux (Id i) _) _) _) _) (_,(Just(_,_,_,Effect_aux(Effect_set efs) _))) :: executes ->
     if i = id 
-    then match exp with
-      | E_aux e (_,Just(_,_,_,Effect_aux (Effect_set efs) _)) -> efs
-      | _ -> [] end
+    then efs
     else extract_effects_of_pat id executes
   | _::executes -> extract_effects_of_pat id executes
 end
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index a4581162..faa75224 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -528,9 +528,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)) =
-  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_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),(l,annot))) =
   let pp_funcls ppf funcl = fprintf ppf "%a %a" pp_lem_funcl funcl kwd ";" in
diff --git a/src/type_check.ml b/src/type_check.ml
index 8bdede1d..5421b1b8 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -1576,7 +1576,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)) id' ->
+    (fun (FCL_aux((FCL_Funcl(id,pat,exp)),(l,annot))) 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, " 
@@ -1593,20 +1593,20 @@ let check_fundef envs (FD_aux(FD_function(recopt,tannotopt,effectopt,funcls),(l,
       t,p_t,Base((ids,{t=Tfn(p_t,t,IP_none,ef)}),Emp_global,constraints,ef) in
   let check t_env imp_param =
     List.split
-      (List.map (fun (FCL_aux((FCL_Funcl(id,pat,exp)),l)) ->
+      (List.map (fun (FCL_aux((FCL_Funcl(id,pat,exp)),(l,_))) ->
 	let (pat',t_env',cs_p,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',_,_,cs_e,ef = 
 	  check_exp (Env(d_env,Envmap.union_merge (tannot_merge (Expr l) d_env) t_env t_env')) imp_param 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 cs = [CondCons(Fun l,cs_p,cs_e)] in
-	(FCL_aux((FCL_Funcl(id,pat',exp')),l),(cs,ef))) funcls) in
-  let update_pattern var (FCL_aux ((FCL_Funcl(id,(P_aux(pat,t)),exp)),l)) = 
+	(FCL_aux((FCL_Funcl(id,pat',exp')),(l,(Base(([],ret_t),Emp_global,cs,ef)))),(cs,ef))) funcls) in
+  let update_pattern var (FCL_aux ((FCL_Funcl(id,(P_aux(pat,t)),exp)),annot)) = 
     let pat' = match pat with
       | P_lit (L_aux (L_unit,l')) -> P_aux(P_id (Id_aux (Id var, l')), t)
       | P_tup pats -> P_aux(P_tup ((P_aux (P_id (Id_aux (Id var, l)), t))::pats), t)
       | _ ->  P_aux(P_tup [(P_aux (P_id (Id_aux (Id var,l)), t));(P_aux(pat,t))], t)
-    in (FCL_aux ((FCL_Funcl(id,pat',exp)),l))
+    in (FCL_aux ((FCL_Funcl(id,pat',exp)),annot))
   in
   match (in_env,tannot) with
     | Some(Base( (params,u),Spec,constraints,eft)), Base( (p',t),_,c',eft') ->