summaryrefslogtreecommitdiff
path: root/src/lem_interp/interp.lem
diff options
context:
space:
mode:
Diffstat (limited to 'src/lem_interp/interp.lem')
-rw-r--r--src/lem_interp/interp.lem81
1 files changed, 48 insertions, 33 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index da617824..b1ee613d 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -837,30 +837,33 @@ let rec to_exp mode env v : (exp tannot * lenv) =
| V_unknown -> (E_aux (E_id (id_of_string "-100")) annot, env)
end
-val env_to_let : interp_mode -> lenv -> (exp tannot) -> (exp tannot)
-let rec env_to_let_help mode env = match env with
- | [] -> []
+val env_to_let : interp_mode -> lenv -> (exp tannot) -> lenv -> ((exp tannot) * lenv)
+let rec env_to_let_help mode env taint_env = match env with
+ | [] -> ([],taint_env)
| (i,v)::env ->
let t = (val_typ v) in
let tan = (val_annot t) in
- let (e,_) = to_exp <| mode with track_values = false |> eenv v in
- (((P_aux (P_id i) (Unknown,tan)),e),t)::(env_to_let_help mode env)
+ let (e,taint_env) = to_exp mode taint_env v in
+ let (rest,taint_env) = env_to_let_help mode env taint_env in
+ ((((P_aux (P_id i) (Unknown,tan)),e),t)::rest, taint_env)
end
-let env_to_let mode (LEnv _ env) (E_aux e annot) =
- match env_to_let_help mode env with
- | [] -> E_aux e annot
- | [((p,e),t)] -> E_aux (E_let (LB_aux (LB_val_implicit p e) (Unknown,(val_annot t))) e) annot
- | pts -> let ts = List.map snd pts in
- let pes = List.map fst pts in
- let ps = List.map fst pes in
- let es = List.map snd pes in
- let t = T_tup ts in
- let tan = val_annot t in
- E_aux (E_let (LB_aux (LB_val_implicit (P_aux (P_tup ps) (Unknown,tan))
- (E_aux (E_tuple es) (Unknown,tan))) (Unknown,tan))
- (E_aux e annot))
- annot
+let env_to_let mode (LEnv _ env) (E_aux e annot) taint_env =
+ match env_to_let_help mode env taint_env with
+ | ([],taint_env) -> (E_aux e annot,taint_env)
+ | ([((p,e),t)],tain_env) ->
+ (E_aux (E_let (LB_aux (LB_val_implicit p e) (Unknown,(val_annot t))) e) annot,taint_env)
+ | (pts,taint_env) ->
+ let ts = List.map snd pts in
+ let pes = List.map fst pts in
+ let ps = List.map fst pes in
+ let es = List.map snd pes in
+ let t = T_tup ts in
+ let tan = val_annot t in
+ (E_aux (E_let (LB_aux (LB_val_implicit (P_aux (P_tup ps) (Unknown,tan))
+ (E_aux (E_tuple es) (Unknown,tan))) (Unknown,tan))
+ (E_aux e annot))
+ annot, taint_env)
end
(* match_pattern returns a tuple of (pattern_matches? , pattern_passed_due_to_unknown?, env_of_pattern *)
@@ -897,7 +900,7 @@ let rec match_pattern (P_aux p _) value_whole =
if matched_p then
(matched_p,used_unknown,(LEnv bi ((id,value_whole)::bounds)))
else (false,false,eenv)
- | P_typ typ pat -> match_pattern pat value (* Might like to destructure against the type to get information, but that's looking less useful *)
+ | P_typ typ pat -> match_pattern pat value_whole (* Might like to destructure against the type to get information, but that's looking less useful *)
| P_id id -> (true, false, (LEnv 0 [(id,value_whole)]))
| P_app (Id_aux id _) pats ->
match value with
@@ -1324,13 +1327,15 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
(fun v lm le ->
match find_case pats v with
| [] -> (Error l ("No matching patterns in case for value " ^ (string_of_value v)),lm,le)
- | [(env,used_unknown,exp)] ->
+ | [(env,_,exp)] ->
if mode.eager_eval
then interp_main mode t_level (union_env env l_env) lm exp
else debug_out Nothing Nothing exp t_level lm (union_env env l_env)
| multi_matches ->
- let lets = List.map (fun (env,_,exp) -> env_to_let mode env exp) multi_matches in
- interp_main mode t_level l_env lm (E_aux (E_block lets) (l,annot))
+ let (lets,taint_env) =
+ List.foldr (fun (env,_,exp) (rst,taint_env) ->
+ let (e,t_e) = env_to_let mode env exp taint_env in (e::rst,t_e)) ([],l_env) multi_matches in
+ interp_main mode t_level taint_env lm (E_aux (E_block lets) (l,annot))
end)
(fun a -> update_stack a (add_to_top_frame (fun e env -> (E_aux (E_case e pats) (l,annot), env))))
| E_record(FES_aux (FES_Fexps fexps _) fes_annot) ->
@@ -1715,7 +1720,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
| [] ->
(Error l ("No matching pattern for function " ^ name ^
" on value " ^ (string_of_value v)),l_mem,l_env)
- | [(env,used_unknown,exp)] ->
+ | [(env,_,exp)] ->
resolve_outcome
(if mode.eager_eval
then (interp_main mode t_level env emem exp)
@@ -1726,9 +1731,11 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
(E_aux (E_id (Id_aux (Id "0") l)) (l,(intern_annot annot)))
t_level l_env l_mem stack)))
| multi_matches ->
- let lets = List.map (fun (env,_,exp) -> env_to_let mode env exp) multi_matches in
- interp_main mode t_level l_env l_mem (E_aux (E_block lets) (l,annot))
- end)
+ let (lets,taint_env) =
+ List.foldr (fun (env,_,exp) (rst,taint_env) ->
+ let (e,t_e) = env_to_let mode env exp taint_env in (e::rst,t_e)) ([],l_env) multi_matches in
+ interp_main mode t_level taint_env lm (E_aux (E_block lets) (l,annot))
+ end)
| Nothing ->
(Error l (String.stringAppend "Internal error: function with empty tag unfound " name),lm,le) end)
| Tag_empty ->
@@ -1788,8 +1795,12 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
(Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level le lm Top), lm, le)
else if has_wmem_effect effects
then
- (*TODO This is wrong, need to split up value or unsplit generally*)
- (Action (Write_mem (id_of_string name_ext) v Nothing v)
+ let (wv,v) =
+ match v with
+ | V_tuple params_list ->
+ let reved = List.reverse params_list in
+ (List_extra.head reved,V_tuple (List.reverse (List_extra.tail reved))) end in
+ (Action (Write_mem (id_of_string name_ext) v Nothing wv)
(Hole_frame (Id_aux (Id "0") l)
(E_aux (E_id (Id_aux (Id "0") l)) (l, intern_annot annot)) t_level le lm Top),lm,le)
else
@@ -2090,8 +2101,10 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
t_level l_env l_mem stack))), l_mem,l_env), Nothing)
| (e,lm,le) -> ((e,lm,le),Nothing) end)
| multi_matches ->
- let lets = List.map (fun (env,_,exp) -> env_to_let mode env exp) multi_matches in
- (interp_main mode t_level l_env l_mem (E_aux (E_block lets) (l,annot)), Nothing)
+ let (lets,taint_env) =
+ List.foldr (fun (env,_,exp) (rst,taint_env) ->
+ let (e,t_e) = env_to_let mode env exp taint_env in (e::rst,t_e)) ([],l_env) multi_matches in
+ (interp_main mode t_level taint_env lm (E_aux (E_block lets) (l,annot)), Nothing)
end)
| Nothing ->
((Error l ("Internal error: function unfound " ^ name),lm,le),Nothing) end)
@@ -2473,7 +2486,7 @@ let interp mode external_functions defs exp =
let rec resume_with_env mode stack value =
match (stack,value) with
- | (Top,_) -> (Error Unknown "Top hit without expression to evaluate",eenv)
+ | (Top,_) -> (Error Unknown "Top hit without expression to evaluate in resume_with_env",eenv)
| (Hole_frame id exp t_level env mem Top,Just value) ->
match interp_main mode t_level (add_to_env (id,value) env) mem exp with | (o,_,e) -> (o,e) end
| (Hole_frame id exp t_level env mem stack,Just value) ->
@@ -2503,9 +2516,11 @@ let rec resume_with_env mode stack value =
let rec resume mode stack value =
match (stack,value) with
- | (Top,_) -> Error Unknown "Top hit without expression to evaluate"
+ | (Top,_) -> Error Unknown "Top hit without expression to evaluate in resume"
| (Hole_frame id exp t_level env mem Top,Just value) ->
match interp_main mode t_level (add_to_env (id,value) env) mem exp with | (o,_,_) -> o end
+ | (Hole_frame id exp t_level env mem Top,Nothing) ->
+ Error Unknown "Top hole frame hit wihtout a value in resume"
| (Hole_frame id exp t_level env mem stack,Just value) ->
match resume mode stack (Just value) with
| Value v ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 21:48:34 +0000