From 02e4b62028411bc107ba63eff87b8d996baae695 Mon Sep 17 00:00:00 2001 From: Kathy Gray Date: Tue, 30 Sep 2014 16:52:38 +0100 Subject: Add type annotations to funcls to track effects and constraints from one function-clause --- src/initial_check.ml | 2 +- src/lem_interp/instruction_extractor.lem | 6 ++---- src/pretty_print.ml | 6 +++--- src/type_check.ml | 10 +++++----- 4 files changed, 11 insertions(+), 13 deletions(-) (limited to 'src') 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') -> -- cgit v1.2.3