summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/lem_interp/Interp_interface.lem3
-rw-r--r--src/lem_interp/interp.lem73
-rw-r--r--src/lem_interp/interp_inter_imp.lem53
-rw-r--r--src/lem_interp/run_interp.ml8
4 files changed, 81 insertions, 56 deletions
diff --git a/src/lem_interp/Interp_interface.lem b/src/lem_interp/Interp_interface.lem
index 0e05fafe..00c22bbe 100644
--- a/src/lem_interp/Interp_interface.lem
+++ b/src/lem_interp/Interp_interface.lem
@@ -1,4 +1,5 @@
import Interp
+open import Num
type read_kind = Interp.read_kind
type write_kind = Interp.write_kind
@@ -42,7 +43,7 @@ type event =
(*Should multiple memory accesses be represented with a special form to denote this or potentially merged into one read or left in place*)
-val build_context : Interp.defs Interp.tannot -> context
+val build_context : Interp_ast.defs Interp.tannot -> context
val initial_instruction_state : context -> string -> value -> instruction_state
type interp_mode = <| eager_eval : bool |>
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index efd2f866..135fdb8e 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -122,7 +122,8 @@ type action =
(* Inverted call stack, where top item on the stack is waiting for an action to resolve and all other frames for the right stack *)
type stack =
| Top
- | Frame of maybe id * exp tannot * top_level * env * lmem * stack
+ | Hole_frame of id * exp tannot * top_level * env * lmem * stack (* Stack frame waiting to fill a hole with a value *)
+ | Thunk_frame of exp tannot * top_level * env * lmem * stack (* Paused stack frame *)
(*Internal representation of outcomes from running the interpreter. Actions request an external party to resolve a request *)
type outcome =
@@ -139,7 +140,7 @@ val to_top_env : defs tannot -> (maybe outcome * top_level)
val interp :interp_mode -> defs tannot -> exp tannot -> outcome
(* Takes a paused partially evaluated expression, puts the value into the environment, and runs again *)
-val resume : interp_mode -> stack -> value -> outcome
+val resume : interp_mode -> stack -> maybe value -> outcome
val to_register_fields : defs tannot -> list (id * list (id * index_range))
let rec to_register_fields (Defs defs) =
@@ -341,9 +342,22 @@ end
let add_to_top_frame e_builder stack =
match stack with
- | Frame id e t_level env mem stack -> Frame id (e_builder e) t_level env mem stack
+ | Top -> Top
+ | Hole_frame id e t_level env mem stack -> Hole_frame id (e_builder e) t_level env mem stack
+ | Thunk_frame e t_level env mem stack -> Thunk_frame (e_builder e) t_level env mem stack
end
+(*Converts a Hole_frame into a Thunk_frame, pushing to almost the top of the stack to insert the value at the innermost context *)
+val add_answer_to_stack : stack -> value -> stack
+let rec add_answer_to_stack stack v =
+ match stack with
+ | Top -> Top
+ | Hole_frame id e t_level env mem Top -> Thunk_frame e t_level ((id,v)::env) mem Top
+ | Thunk_frame e t_level env mem Top -> Thunk_frame e t_level env mem Top
+ | Hole_frame id e t_level env mem stack -> Hole_frame id e t_level env mem (add_answer_to_stack stack v)
+ | Thunk_frame e t_level env mem stack -> Thunk_frame e t_level env mem (add_answer_to_stack stack v)
+end
+
let id_of_string s = (Id_aux (Id s) Unknown)
let rec combine_typs ts =
@@ -678,7 +692,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
match (tag,v) with
| (Tag_extern _, V_register regform) ->
(Action (Read_reg regform Nothing)
- (Frame (Just (id_of_string "0"))
+ (Hole_frame (id_of_string "0")
(E_aux (E_id (id_of_string "0")) (Unknown, (val_annot (reg_to_t regform)))) t_level le lm Top), lm,le)
| (_,V_vector start inc items) ->
(match typ with
@@ -718,7 +732,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
| Just(V_register regform) -> regform
| _ -> Reg id annot end end in
(Action (Read_reg regf Nothing)
- (Frame (Just (Id_aux (Id "0") Unknown))
+ (Hole_frame (Id_aux (Id "0") Unknown)
(E_aux (E_id (Id_aux (Id "0") l)) (l,intern_annot annot)) t_level l_env l_mem Top),
l_mem,l_env)
| _ -> (Error l (String.stringAppend "Internal error: tag other than empty,enum,or extern " name),l_mem,l_env)
@@ -989,7 +1003,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
resolve_outcome (interp_main mode t_level env l_mem exp)
(fun ret lm le -> (Value ret Tag_empty, lm,l_env))
(fun a -> update_stack a
- (fun stack -> (Frame (Just (id_of_string "0")) (E_aux (E_id (Id_aux (Id "0") l)) (l,annot)) t_level l_env l_mem stack)))
+ (fun stack -> (Hole_frame (id_of_string "0") (E_aux (E_id (Id_aux (Id "0") l)) (l,annot)) t_level l_env l_mem stack)))
end)
| Nothing -> (Error l (String.stringAppend "Internal error: function with empty tag unfound " name),lm,le) end)
| Tag_spec ->
@@ -1002,7 +1016,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
resolve_outcome (interp_main mode t_level env l_mem exp)
(fun ret lm le -> (Value ret Tag_empty, lm,l_env))
(fun a -> update_stack a
- (fun stack -> (Frame (Just (id_of_string "0")) (E_aux (E_id (Id_aux (Id "0") l)) (l,annot)) t_level l_env l_mem stack)))
+ (fun stack -> (Hole_frame (id_of_string "0") (E_aux (E_id (Id_aux (Id "0") l)) (l,annot)) t_level l_env l_mem stack)))
end)
| Nothing -> (Error l (String.stringAppend "Specified function must be defined before executing " name),lm,le) end)
| Tag_ctor ->
@@ -1015,10 +1029,10 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
if has_memory_effect (match effect with | Effect_aux(Effect_set es) _ -> es | _ -> [] end)
then
(Action (Read_mem (id_of_string name_ext) v Nothing)
- (Frame (Just (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)
+ (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
(Action (Call_extern name_ext v)
- (Frame (Just (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)
+ (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)
| _ -> (Error l (String.stringAppend "Tag other than empty, spec, ctor, or extern on function call " name),lm,le) end)
| out -> out end)
| E_app_infix lft op r ->
@@ -1042,7 +1056,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
resolve_outcome (interp_main mode t_level env emem exp)
(fun ret lm le -> (Value ret Tag_empty,l_mem,l_env))
(fun a -> update_stack a
- (fun stack -> (Frame (Just (Id_aux (Id "0") l))
+ (fun stack -> (Hole_frame (Id_aux (Id "0") l)
(E_aux (E_id (Id_aux (Id "0") l)) (l,annot)) t_level l_env l_mem stack)))
end)end)
| Tag_spec ->
@@ -1055,13 +1069,13 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
resolve_outcome (interp_main mode t_level env emem exp)
(fun ret lm le -> (Value ret Tag_empty,l_mem,l_env))
(fun a -> update_stack a
- (fun stack -> (Frame (Just (Id_aux (Id "0") l))
+ (fun stack -> (Hole_frame (Id_aux (Id "0") l)
(E_aux (E_id (Id_aux (Id "0") l)) (l,annot)) t_level l_env l_mem stack)))
end)end)
| Tag_extern ext_name ->
let ext_name = match ext_name with Just s -> s | Nothing -> name end in
(Action (Call_extern ext_name (V_tuple [lv;rv]))
- (Frame (Just (Id_aux (Id "0") l))
+ (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) end)
(fun a -> update_stack a (add_to_top_frame (fun r ->E_aux (E_app_infix (to_exp lv) op r) (l,annot)))))
(fun a -> update_stack a (add_to_top_frame (fun lft -> (E_aux (E_app_infix lft op r) (l,annot)))))
@@ -1134,8 +1148,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
| Tag_extern _ ->
let regf = Reg id annot in
let request = (Action (Write_reg regf Nothing value)
- (Frame (Just (Id_aux (Id "0") l))
- (E_aux (E_id (Id_aux (Id "0") l)) (l,intern_annot annot)) t_level l_env l_mem Top),l_mem,l_env) in
+ (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level l_env l_mem Top),l_mem,l_env) in
if is_top_level then (request,Nothing) else (request,Just (fun e -> LEXP_aux (LEXP_id id) (l,annot)))
| _ -> ((Error l (String.stringAppend "Internal error: writing to id with tag other than extern or empty " (get_id id)),l_mem,l_env),Nothing)
end
@@ -1147,7 +1160,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
(match tag with
| Tag_extern ->
let request = (Action (Write_mem id v Nothing value)
- (Frame (Just (Id_aux (Id "0") l)) (E_aux (E_id (Id_aux (Id "0") l)) (l,intern_annot annot)) t_level l_env lm Top),lm,l_env) in
+ (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level l_env lm Top),lm,l_env) in
if is_top_level then (request,Nothing)
else (request,Just (fun e ->
(LEXP_aux (LEXP_memory id (match v with | V_tuple vs -> (List.map to_exp vs) | v -> [to_exp v]end)) (l,annot))))
@@ -1177,8 +1190,7 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
| Tag_extern _ ->
let regf = Reg id annot in
let request = (Action (Write_reg regf Nothing value)
- (Frame (Just (Id_aux (Id "0") l))
- (E_aux (E_id (Id_aux (Id "0") l)) (l,intern_annot annot)) t_level l_env l_mem Top),l_mem,l_env) in
+ (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level l_env l_mem Top),l_mem,l_env) in
if is_top_level then (request,Nothing) else (request,Just (fun e -> LEXP_aux (LEXP_cast typc id) (l,annot)))
| _ -> ((Error l (String.stringAppend "Internal error: writing to id with tag other than extern or empty " (get_id id)),l_mem,l_env),Nothing)
end
@@ -1197,12 +1209,10 @@ and create_write_message_or_update mode t_level value l_env l_mem is_top_level (
(match (nth,is_top_level,maybe_builder) with
| (V_register regform,true,_) ->
((Action (Write_reg regform Nothing value)
- (Frame (Just (Id_aux (Id "0") l))
- (E_aux (E_id (Id_aux (Id "0") l)) (l,intern_annot annot)) t_level l_env l_mem Top),l_mem,l_env),Nothing)
+ (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level l_env l_mem Top),l_mem,l_env),Nothing)
| (V_register regform,false,Just lexp_builder) ->
((Action (Write_reg regform Nothing value)
- (Frame (Just (Id_aux (Id "0") l))
- (E_aux (E_id (Id_aux (Id "0") l)) (l,intern_annot annot)) t_level l_env l_mem Top),l_mem,l_env),
+ (Thunk_frame (E_aux (E_lit (L_aux L_unit l)) (l,intern_annot annot)) t_level l_env l_mem Top),l_mem,l_env),
Just (next_builder lexp_builder))
| (V_boxref n t,true,_) -> ((Value (V_lit (L_aux L_unit Unknown)) Tag_empty, update_mem lm n value, l_env),Nothing)
| (v,true,_) -> ((Error l "Vector does not contain reg or register values",lm,l_env),Nothing)
@@ -1355,26 +1365,25 @@ let interp mode defs exp =
end
let rec resume mode stack value =
- match stack with
- | Top -> Error Unknown "Top hit without place to put value"
- | Frame (Just id) exp t_level env mem Top ->
+ match (stack,value) with
+ | (Top,_) -> Error Unknown "Top hit without expression to evaluate"
+ | (Hole_frame id exp t_level env mem Top,Just value) ->
match interp_main mode t_level ((id,value)::env) mem exp with | (o,_,_) -> o end
- | Frame Nothing exp t_level env mem Top ->
- match interp_main mode t_level env mem exp with | (o,_,_) -> o end
- | Frame (Just id) exp t_level env mem stack ->
- match resume mode stack value with
+ | (Hole_frame id exp t_level env mem stack,Just value) ->
+ match resume mode stack (Just value) with
| Value v tag ->
match interp_main mode t_level ((id,v)::env) mem exp with | (o,_,_) -> o end
- | Action action stack -> Action action (Frame (Just id) exp t_level env mem stack)
+ | Action action stack -> Action action (Hole_frame id exp t_level env mem stack)
| Error l s -> Error l s
end
- | Frame Nothing exp t_level env mem stack ->
+ | (Thunk_frame exp t_level env mem Top,_) ->
+ match interp_main mode t_level env mem exp with | (o,_,_) -> o end
+ | (Thunk_frame exp t_level env mem stack,value) ->
match resume mode stack value with
| Value v tag ->
match interp_main mode t_level env mem exp with | (o,_,_) -> o end
- | Action action stack -> Action action (Frame Nothing exp t_level env mem stack)
+ | Action action stack -> Action action (Thunk_frame exp t_level env mem stack)
| Error l s -> Error l s
end
-
end
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 59acb04a..66ad0293 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -1,30 +1,30 @@
import Interp
import Interp_lib
+open import Interp_ast
open import Interp_interface
-
-import Num
+open import Pervasives
val intern_value : value -> Interp.value
-val extern_value : Interp.value -> value
+val extern_value : bool -> Interp.value -> value
val extern_reg : Interp.reg_form -> maybe (integer * integer) -> reg_name
let build_context defs = Interp.to_top_env defs
let to_bits l = (List.map (fun b -> match b with
- | false -> (Interp.V_lit (Interp_ast.L_aux Interp_ast.L_zero Interp_ast.Unknown))
- | true -> (Interp.V_lit (Interp_ast.L_aux Interp_ast.L_one Interp_ast.Unknown)) end) l)
+ | false -> (Interp.V_lit (L_aux L_zero Interp_ast.Unknown))
+ | true -> (Interp.V_lit (L_aux L_one Interp_ast.Unknown)) end) l)
let from_bits l = (List.map (fun b -> match b with
- | Interp.V_lit (Interp_ast.L_aux Interp_ast.L_zero _) -> false
+ | Interp.V_lit (L_aux L_zero _) -> false
| _ -> true end) l)
let rec to_bytes l = match l with
| [] -> []
| (a::b::c::d::e::f::g::h::rest) ->
- (integerFromBoolList [a;b;c;d;e;f;g;h])::(to_bytes rest)
+ (natFromInteger(integerFromBoolList (true,[a;b;c;d;e;f;g;h])))::(to_bytes rest)
end
let intern_value v = match v with
| Bitvector bs -> Interp.V_vector 0 true (to_bits bs)
- | Bytevector bys -> Interp.V_vector 0 true (to_bits (List.concat (List.map (bitSeqFromInteger 8 Nothing) bys)))
+ | Bytevector bys -> Interp.V_vector 0 true (to_bits (List.concat (List.map (fun n -> boolListFrombitSeq 8 (bitSeqFromInteger (Just 8) (integerFromNat n))) bys)))
| Unknown -> Interp.V_unknown
end
@@ -37,27 +37,40 @@ let extern_value for_mem v = match v with
end
let extern_reg r slice = match (r,slice) with
- | (Interp.Reg(Id_aux (Id x,_)),Nothing) -> Reg x
- | (Interp.Reg(Id_aux (Id x,_)),Just(i1,i2)) -> Reg_slice x (i1,i2)
- | (Interp.SubReg (Id_aux (Id x,_)) (Interp.Reg(Id_aux (Id y,_))) (Interp_ast.BF_aux(Interp_ast.BF_single i) _),Nothing) -> Reg_field x y (i,i)
+ | (Interp.Reg (Id_aux (Id x) _) _,Nothing) -> Reg x
+ | (Interp.Reg (Id_aux (Id x) _) _,Just(i1,i2)) -> Reg_slice x (i1,i2)
+ | (Interp.SubReg (Id_aux (Id x) _) (Interp.Reg (Id_aux (Id y) _) _) (BF_aux(BF_single i) _),Nothing) -> Reg_field x y (i,i)
end
let initial_instruction_state top_level main arg =
- Interp.Frame Nothing (E_aux (E_app (Id_aux (Id main) Interp_ast.Unknown) [ intern_value arg ]) (Interp_ast.Unknown, Nothing)) top_level [] Interp.emem
+ Interp.Thunk_frame (E_aux (E_app (Id_aux (Id main) Interp_ast.Unknown) [ Interp.to_exp (intern_value arg) ]) (Interp_ast.Unknown, Nothing)) top_level [] Interp.emem
+
+(*For now, append to this list to add more external functions; should add to the mode record for more perhaps *)
+let external_functions =
+ Interp_lib.function_map
+
+type mem_function = (string * maybe read_kind * maybe write_kind * Interp.value -> value)
+
+let memory_functions =
+ [ ("MEM", Just(Interp.Read_plain), Just(Interp.Write_plain), (fun v -> extern_value true v));
+ ]
let interp mode i_state =
- match Interp.resume mode i_state None with
- | Interp.Value _ -> Done
+ match Interp.resume mode i_state Nothing with
+ | Interp.Value _ _ -> Done
| Interp.Error l msg -> Error msg (*Todo, add the l information the string format*)
| Interp.Action a next_state ->
match a with
- | Interp.Read_reg reg_form slice -> Read_reg reg_form (fun v -> Interp.add_answer_to_stack (intern_value v) next_state)
- | Interp.Write_reg reg_form slice value -> Write_reg reg_form (extern_value value) next_state
+ | Interp.Read_reg reg_form slice -> Read_reg (extern_reg reg_form slice) (fun v -> Interp.add_answer_to_stack next_state (intern_value v))
+ | Interp.Write_reg reg_form slice value -> Write_reg (extern_reg reg_form slice) (extern_value false value) next_state
| Interp.Read_mem (Id_aux (Id i) _) value slice
(*Need to lookup the Mem function used to determine appropriate value, and possible appropriate read_kind *)
- -> Read_mem Interp.Read_plain (extern_value value) (fun v -> Interp.add_answer_to_stack (intern_value v) next_state)
- | Interp.Write_mem (Id_aux (id i) _) loc_val slice write_val ->
- Write_mem Interp.Write_plain (extern_value loc_val) (extern_value write_val) next_state
- | Interp.Call_extern id value -> (*Connect here to a list of external functions*) foo
+ -> Read_mem Interp.Read_plain (extern_value true value) (fun v -> Interp.add_answer_to_stack next_state (intern_value v))
+ | Interp.Write_mem (Id_aux (Id i) _) loc_val slice write_val ->
+ Write_mem Interp.Write_plain (extern_value true loc_val) (extern_value true write_val) (fun b -> next_state)
+ | Interp.Call_extern (Id_aux (Id id) _) value ->
+ match List.lookup with
+ | Nothing -> Error ("External function not available " ^ id)
+ | Just f -> Interp.resume mode next_state Just value end
end
end
diff --git a/src/lem_interp/run_interp.ml b/src/lem_interp/run_interp.ml
index 517ba5ab..bd8640ba 100644
--- a/src/lem_interp/run_interp.ml
+++ b/src/lem_interp/run_interp.ml
@@ -73,8 +73,10 @@ let rec env_to_string = function
let rec stack_to_string = function
| Top -> "Top"
- | Frame(Some id,exp,t_level,env,mem,s) ->
- sprintf "(Frame of %s, e, (%s), m, %s)" (id_to_string id) (env_to_string env) (stack_to_string s)
+ | Hole_frame(id,exp,t_level,env,mem,s) ->
+ sprintf "(Hole_frame of %s, e, (%s), m, %s)" (id_to_string id) (env_to_string env) (stack_to_string s)
+ | Thunk_frame(exp,t_level,env,mem,s) ->
+ sprintf "(Thunk_frame of e, (%s), m, %s)" (env_to_string env) (stack_to_string s)
;;
let sub_to_string = function None -> "" | Some (x, y) -> sprintf " (%s, %s)"
@@ -216,7 +218,7 @@ let run
(*debugf "%s: suspended on action %s, with stack %s\n" name (act_to_string a) (stack_to_string s);*)
let return, env' = perform_action env a in
debugf "%s: action returned %s\n" name (val_to_string return);
- loop env' (resume {eager_eval = true} s return)
+ loop env' (resume {eager_eval = true} s (Some return))
| Error(l, e) -> debugf "%s: %s: error: %s\n" name (loc_to_string l) e; false, env in
debugf "%s: starting\n" name;
try
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 21:23:22 +0000