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.lem59
1 files changed, 35 insertions, 24 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index b6e1a8f5..a19e3d5f 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -1188,7 +1188,7 @@ let rec find_case t_level pexps value =
end
val interp_main : interp_mode -> top_level -> lenv -> lmem -> (exp tannot) -> (outcome * lmem * lenv)
-val exp_list : interp_mode -> top_level -> (list (exp tannot) -> (exp tannot)) -> (list value -> value) -> lenv -> lmem -> list value -> list (exp tannot) -> (outcome * lmem * lenv)
+val exp_list : interp_mode -> top_level -> ((list (exp tannot)) -> lenv -> ((exp tannot) * lenv)) -> (list value -> value) -> lenv -> lmem -> list value -> list (exp tannot) -> (outcome * lmem * lenv)
val interp_lbind : interp_mode -> top_level -> lenv -> lmem -> (letbind tannot) -> ((outcome * lmem * lenv) * (maybe ((exp tannot) -> (letbind tannot))))
val interp_alias_read : interp_mode -> top_level -> lenv -> lmem -> (alias_spec tannot) -> (outcome * lmem * lenv)
@@ -1220,7 +1220,9 @@ let rec exp_list mode t_level build_e build_v l_env l_mem vals exps =
(fun value lm le -> exp_list mode t_level build_e build_v l_env lm (vals++[value]) exps)
(fun a -> update_stack a (add_to_top_frame
(fun e env ->
- let (es,env') = to_exps mode env vals in (build_e (es++(e::exps)),env'))))
+ let (es,env') = to_exps mode env vals in
+ let (e,env'') = build_e (es++(e::exps)) env' in
+ (e,env''))))
end
and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
@@ -1414,12 +1416,13 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
| E_record(FES_aux (FES_Fexps fexps _) fes_annot) ->
let (fields,exps) = List.unzip (List.map (fun (FE_aux (FE_Fexp id exp) _) -> (id,exp)) fexps) in
exp_list mode t_level
- (fun es ->
- (E_aux
- (E_record
- (FES_aux (FES_Fexps
- (map2 (fun id exp -> (FE_aux (FE_Fexp id exp) (Unknown,Nothing))) fields es) false) fes_annot))
- (l,annot)))
+ (fun es env' ->
+ ((E_aux
+ (E_record
+ (FES_aux (FES_Fexps
+ (map2 (fun id exp -> (FE_aux (FE_Fexp id exp) (Unknown,Nothing))) fields es)
+ false) fes_annot))
+ (l,annot)), env'))
(fun vs -> (V_record typ (List.zip fields vs))) l_env l_mem [] exps
| E_record_update exp (FES_aux (FES_Fexps fexps _) fes_annot) ->
resolve_outcome
@@ -1429,13 +1432,13 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
let (fields,exps) = List.unzip (List.map (fun (FE_aux (FE_Fexp id exp) _) -> (id,exp)) fexps) in
resolve_outcome
(exp_list mode t_level
- (fun es ->
- let (e,_) = (to_exp <|mode with track_values = false|> eenv rv) in
- (E_aux (E_record_update e
+ (fun es env'->
+ let (e,env'') = (to_exp mode env' rv) in
+ ((E_aux (E_record_update e
(FES_aux (FES_Fexps
(map2 (fun id exp -> (FE_aux (FE_Fexp id exp) (Unknown,Nothing)))
fields es) false) fes_annot))
- (l,annot)))
+ (l,annot)), env''))
(fun vs -> (V_record t (List.zip fields vs))) l_env l_mem [] exps)
(fun vs lm le -> (Value (fupdate_record rv vs), lm, le))
(fun a -> a) (*Due to exp_list this won't happen, but we want to functionaly update on Value *)
@@ -1445,7 +1448,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
(add_to_top_frame
(fun e env -> (E_aux(E_record_update e (FES_aux(FES_Fexps fexps false) fes_annot)) (l,annot), env))))
| E_list(exps) ->
- exp_list mode t_level (fun exps -> E_aux (E_list exps) (l,annot)) V_list l_env l_mem [] exps
+ exp_list mode t_level (fun exps env' -> (E_aux (E_list exps) (l,annot),env')) V_list l_env l_mem [] exps
| E_cons hd tl ->
resolve_outcome
(interp_main mode t_level l_env l_mem hd)
@@ -1740,14 +1743,15 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
(E_aux (E_vector_append e1 e) (l,annot),env'))))) end)
(fun a -> update_stack a (add_to_top_frame (fun e env -> (E_aux (E_vector_append e e2) (l,annot),env))))
| E_tuple(exps) ->
- exp_list mode t_level (fun exps -> E_aux (E_tuple exps) (l,annot)) V_tuple l_env l_mem [] exps
+ exp_list mode t_level (fun exps env' -> (E_aux (E_tuple exps) (l,annot), env')) V_tuple l_env l_mem [] exps
| E_vector(exps) ->
let (is_inc,dir) = (match typ with
| T_app "vector" (T_args [ _; _; T_arg_order (Ord_aux Ord_inc _); _]) -> (true,IInc)
| _ -> (false,IDec) end) in
let base = (if is_inc then 0 else (List.length exps) - 1) in
exp_list mode t_level
- (fun exps -> E_aux (E_vector exps) (l,annot)) (fun vals -> V_vector base dir vals) l_env l_mem [] exps
+ (fun exps env' -> (E_aux (E_vector exps) (l,annot),env'))
+ (fun vals -> V_vector base dir vals) l_env l_mem [] exps
| E_vector_indexed iexps (Def_val_aux default dannot) ->
let (indexes,exps) = List.unzip iexps in
let (dir,base,len) = (match typ with
@@ -1758,8 +1762,8 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
(match default with
| Def_val_empty ->
exp_list mode t_level
- (fun es -> (E_aux (E_vector_indexed (map2 (fun i e -> (i,e)) indexes es)
- (Def_val_aux default dannot)) (l,annot)))
+ (fun es env' -> (E_aux (E_vector_indexed (map2 (fun i e -> (i,e)) indexes es)
+ (Def_val_aux default dannot)) (l,annot), env'))
(fun vals -> V_vector (if indexes=[] then 0 else (natFromInteger (List_extra.head indexes))) dir vals)
l_env l_mem [] exps
| Def_val_dec default_exp ->
@@ -1769,11 +1773,11 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
(interp_main mode t_level l_env l_mem default_exp)
(fun v lm le ->
exp_list mode t_level
- (fun es ->
- let (ev,_) = to_exp <|mode with track_values = false |> eenv v in
+ (fun es env' ->
+ let (ev,env'') = to_exp mode env' v in
(E_aux (E_vector_indexed (map2 (fun i e -> (i,e)) indexes es)
(Def_val_aux (Def_val_dec ev) dannot))
- (l,annot)))
+ (l,annot), env''))
(fun vs ->
(V_vector_sparse b len dir (map2 (fun i v -> ((natFromInteger i),v)) indexes vs) v)) l_env l_mem [] exps)
(fun a ->
@@ -1787,7 +1791,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
l_mem, l_env)
| E_app f args ->
(match (exp_list mode t_level
- (fun es -> E_aux (E_app f es) (l,annot))
+ (fun es env -> (E_aux (E_app f es) (l,annot),env))
(fun vs -> match vs with | [] -> V_lit (L_aux L_unit l) | [v] -> v | vs -> V_tuple vs end)
l_env l_mem [] args) with
| (Value v,lm,le) ->
@@ -2026,6 +2030,13 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
let (typ,tag,ncs,ef) = match annot with
| Nothing -> (T_var "fresh_v", Tag_empty, [], (Effect_aux (Effect_set []) Unknown))
| Just(t, tag, ncs, ef) -> (t,tag,ncs,ef) end in
+ let recenter_val typ value = match typ with
+ | T_app "reg" (T_args [T_arg_typ
+ (T_app "vector" (T_args [T_arg_nexp (Ne_const start); T_arg_nexp (Ne_const size); _; _ ]))]) ->
+ update_vector_start default_dir (natFromInteger start) (natFromInteger size) value
+ | T_abbrev _ (T_app "vector" (T_args [T_arg_nexp (Ne_const start); T_arg_nexp (Ne_const size); _; _ ])) ->
+ update_vector_start default_dir (natFromInteger start) (natFromInteger size) value
+ | _ -> value end in
match lexp with
| LEXP_id id ->
let name = get_id id in
@@ -2034,7 +2045,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
match detaint (in_lenv l_env id) with
| ((V_boxref n t) as v) ->
if is_top_level
- then ((Value (V_lit (L_aux L_unit l)), update_mem l_mem n value, l_env),Nothing)
+ then ((Value (V_lit (L_aux L_unit l)), update_mem l_mem n (recenter_val t value), l_env),Nothing)
else ((Value v, l_mem, l_env),Just (fun e env -> (LEXP_aux (LEXP_id id) (l,annot), env)))
| V_unknown ->
if is_top_level then
@@ -2150,7 +2161,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
l_mem,l_env),Nothing)
end
| LEXP_memory id exps ->
- match (exp_list mode t_level (fun exps -> E_aux (E_tuple exps) (Unknown,Nothing))
+ match (exp_list mode t_level (fun exps env -> (E_aux (E_tuple exps) (Unknown,Nothing),env))
(fun vs -> match vs with | [] -> V_lit (L_aux L_unit Unknown) | [v] -> v | vs -> V_tuple vs end)
l_env l_mem [] exps) with
| (Value v,lm,le) ->
@@ -2206,7 +2217,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
match detaint (in_lenv l_env id) with
| ((V_boxref n t) as v) ->
if is_top_level
- then ((Value (V_lit (L_aux L_unit l)), update_mem l_mem n value, l_env),Nothing)
+ then ((Value (V_lit (L_aux L_unit l)), update_mem l_mem n (recenter_val t value), l_env),Nothing)
else ((Value v, l_mem, l_env),Just (fun e env -> (LEXP_aux (LEXP_cast typc id) (l,annot), env)))
| V_unknown ->
if is_top_level
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 17:49:28 +0000