diff options
Diffstat (limited to 'src/lem_interp')
| -rw-r--r-- | src/lem_interp/instruction_extractor.lem | 7 | ||||
| -rw-r--r-- | src/lem_interp/interp.lem | 4 | ||||
| -rw-r--r-- | src/lem_interp/interp_utilities.lem | 2 | ||||
| -rw-r--r-- | src/lem_interp/pretty_interp.ml | 2 |
4 files changed, 8 insertions, 7 deletions
diff --git a/src/lem_interp/instruction_extractor.lem b/src/lem_interp/instruction_extractor.lem index b49646ea..11947c17 100644 --- a/src/lem_interp/instruction_extractor.lem +++ b/src/lem_interp/instruction_extractor.lem @@ -103,7 +103,8 @@ end let rec extract_from_decode decoder = match decoder with | [] -> [] - | (FCL_aux (FCL_Funcl _ pat exp) _)::decoder -> + | (FCL_aux (FCL_Funcl _ (Pat_aux pexp _)) _)::decoder -> + let exp = match pexp with Pat_exp _ exp -> exp | Pat_when _ _ exp -> exp end in (match exp with | E_aux (E_app (Id_aux(Id id) _) parms) (_,(Just (_,Tag_ctor,_,_,_))) -> Instr_form id (List.map extract_parm parms) [] @@ -112,7 +113,7 @@ end let rec extract_effects_of_fcl id execute = match execute with | [] -> [] - | FCL_aux (FCL_Funcl _ (P_aux (P_app (Id_aux (Id i) _) _) _) _) (_,(Just(_,_,_,Effect_aux(Effect_set efs) _,_))) :: executes -> + | FCL_aux (FCL_Funcl _ (Pat_aux (Pat_exp (P_aux (P_app (Id_aux (Id i) _) _) _) _) _)) (_,(Just(_,_,_,Effect_aux(Effect_set efs) _,_))) :: executes -> if i = id then efs else extract_effects_of_fcl id executes @@ -134,7 +135,7 @@ let rec extract_patt_parm (P_aux p (_,tannot)) = let rec extract_from_execute fcls = match fcls with | [] -> [] - | FCL_aux (FCL_Funcl _ (P_aux (P_app (Id_aux (Id i) _) parms) _) _) (_,Just(_,_,_,Effect_aux(Effect_set efs) _,_))::fcls -> + | FCL_aux (FCL_Funcl _ (Pat_aux (Pat_exp (P_aux (P_app (Id_aux (Id i) _) parms) _) _) _)) (_,Just(_,_,_,Effect_aux(Effect_set efs) _,_))::fcls -> (Instr_form i (List.map extract_patt_parm parms) efs)::extract_from_execute fcls | _ :: fcls -> (* AA: Find out what breaks this *) diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem index 486728d9..431c1a08 100644 --- a/src/lem_interp/interp.lem +++ b/src/lem_interp/interp.lem @@ -639,7 +639,7 @@ let rec to_fdefs (Defs defs) = | FD_aux (FD_function _ _ _ fcls) _ -> match fcls with | [] -> to_fdefs (Defs defs) - | (FCL_aux (FCL_Funcl name _ _) _)::_ -> + | (FCL_aux (FCL_Funcl name _) _)::_ -> Map.insert (get_id name) fcls (to_fdefs (Defs defs)) end end) | _ -> to_fdefs (Defs defs) end end @@ -1625,7 +1625,7 @@ val find_funcl : top_level -> list (funcl tannot) -> value -> list (lenv * bool let rec find_funcl t_level funcls value = match funcls with | [] -> [] - | (FCL_aux (FCL_Funcl id pat exp) _)::funcls -> + | (FCL_aux (FCL_Funcl id (Pat_aux (Pat_exp pat exp) _)) _)::funcls -> let (is_matching,used_unknown,env) = match_pattern t_level pat value in if (is_matching && used_unknown) then (env,used_unknown,exp)::(find_funcl t_level funcls value) diff --git a/src/lem_interp/interp_utilities.lem b/src/lem_interp/interp_utilities.lem index a178df61..1e6c59ff 100644 --- a/src/lem_interp/interp_utilities.lem +++ b/src/lem_interp/interp_utilities.lem @@ -178,7 +178,7 @@ val find_type_def : defs tannot -> id -> maybe (type_def tannot) val find_function : defs tannot -> id -> maybe (list (funcl tannot)) let get_funcls id (FD_aux (FD_function _ _ _ fcls) _) = - List.filter (fun (FCL_aux (FCL_Funcl name pat exp) _) -> (get_id id) = (get_id name)) fcls + List.filter (fun (FCL_aux (FCL_Funcl name pexp) _) -> (get_id id) = (get_id name)) fcls let rec find_function (Defs defs) id = match defs with diff --git a/src/lem_interp/pretty_interp.ml b/src/lem_interp/pretty_interp.ml index 129b74c0..bf42795b 100644 --- a/src/lem_interp/pretty_interp.ml +++ b/src/lem_interp/pretty_interp.ml @@ -657,7 +657,7 @@ let doc_effects_opt (Effect_opt_aux(e,_)) = match e with | Effect_opt_pure -> string "pure" | Effect_opt_effect e -> doc_effects e -let doc_funcl env mem add_red (FCL_aux(FCL_Funcl(id,pat,exp),_)) = +let doc_funcl env mem add_red (FCL_aux(FCL_Funcl(id,Pat_aux (Pat_exp (pat, exp), _)),_)) = group (doc_op equals (separate space [doc_id id; doc_atomic_pat pat]) (doc_exp env mem add_red false exp)) let doc_fundef env mem add_red (FD_aux(FD_function(r, typa, efa, fcls),_)) = |