diff options
| -rw-r--r-- | src/lem_interp/interp.lem | 330 | ||||
| -rw-r--r-- | src/lem_interp/run_interp.ml | 23 |
2 files changed, 193 insertions, 160 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem index c7a9da00..6346252c 100644 --- a/src/lem_interp/interp.lem +++ b/src/lem_interp/interp.lem @@ -80,7 +80,7 @@ type env = list (id * value) let emem = Mem 1 Map.empty type reg_form = - | Reg of id * typ + | Reg of id * t | SubReg of id * reg_form * index_range (* These may need to be refined or expanded based on memory requirement *) @@ -100,14 +100,14 @@ type stack = type outcome = | Value of value | Action of action * stack - | Error of string (* When we store location information, it should be added here *) + | Error of l * string (* interprets the exp sequentially in the presence of a set of top level definitions and returns a value or a memory request *) val interp : defs tannot -> exp tannot -> outcome val to_registers : defs tannot -> list (id * reg_form) -let rec to_registers (Defs defs) = - match defs with +let rec to_registers (Defs defs) = [] +(* match defs with | [ ] -> [ ] | (DEF_aux def _)::defs -> match def with @@ -132,7 +132,7 @@ and to_reg_ranges base_id base_reg ranges = match ranges with | [ ] -> [ ] | (irange,id)::ranges -> (id,(SubReg base_id base_reg irange))::(to_reg_ranges base_id base_reg ranges) - end + end*) val has_memory_effect : list base_effect -> bool let rec has_memory_effect efcts = @@ -569,7 +569,7 @@ let resolve_outcome to_match value_thunk action_thunk = match to_match with | (Value v,lm,le) -> value_thunk v lm le | (Action action stack,lm,le) -> (action_thunk (Action action stack), lm,le) - | (Error s,lm,le) -> (Error s,lm,le) + | (Error l s,lm,le) -> (Error l s,lm,le) end let update_stack (Action act stack) fn = Action act (fn stack) @@ -584,39 +584,50 @@ let rec exp_list t_level build_e build_v l_env l_mem vals exps = (fun a -> update_stack a (add_to_top_frame (fun e -> (build_e ((List.map to_exp vals)++(e::exps)))))) end -and interp_main t_level l_env l_mem (E_aux exp annot) = - match exp with - | E_lit lit -> if is_lit_vector lit then (Value (litV_to_vec lit),l_mem,l_env) else (Value (V_lit lit), l_mem,l_env) +and interp_main t_level l_env l_mem (E_aux exp (l,annot)) = + let (Env defs externs lets regs mems ctors) = t_level in + let (typ,tag,ncs,effect) = match annot with + | Nothing -> (T_var (Kid_aux (Var "fresh_v") Unknown), + Tag_empty, [], (Effect_aux (Effect_set []) Unknown)) + | Just(t, tag, ncs, ef) -> (t,tag,ncs,ef) end in + match exp with + | E_lit lit -> + if is_lit_vector lit then (Value (litV_to_vec lit),l_mem,l_env) else (Value (V_lit lit), l_mem,l_env) | E_cast typ exp -> interp_main t_level l_env l_mem exp (* Potentially introduce coercions ie vectors and numbers *) - | E_id id -> match in_env l_env id with - | Just(value) -> match value with - | V_boxref n ->(Value (in_mem l_mem n),l_mem,l_env) - | _ -> (Value value,l_mem,l_env) end - | Nothing -> match t_level with - | (Env defs externs lets regs mems ctors) -> - match in_env lets id with - | Just(value) -> (Value value,l_mem,l_env) - | Nothing -> - match in_reg regs id with - | Just(regf) -> - (Action (Read_reg regf Nothing) - (Frame (Id_aux (Id "0") Unknown) - (E_aux (E_id (Id_aux (Id "0") Unknown)) annot) l_env l_mem Top), l_mem, l_env) - | Nothing -> - let name = get_id id in - (Error (String.stringAppend "unbound identifier " name ),l_mem,l_env) - end - end - end - end + | E_id id -> + let name = get_id id in + match tag with + | Tag_empty -> + match in_env l_env id with + | Just(value) -> match value with + | V_boxref n -> (Value (in_mem l_mem n),l_mem,l_env) + | _ -> (Value value,l_mem,l_env) end + | Nothing -> + match in_env lets id with + | Just(value) -> (Value value,l_mem,l_env) + | Nothing -> (Error l (String.stringAppend "Internal error: unbound id on Tag_none " name), l_mem,l_env) + end end + | Tag_enum -> + match in_env lets id with + | Just(value) -> (Value value,l_mem,l_env) + | Nothing -> (Error l (String.stringAppend "Internal error: unbound id on Tag_enum " name), l_mem,l_env) + end + | Tag_extern _ -> (* Need to change from "register" to which register where different from id *) + let regf = Reg id typ in + (Action (Read_reg regf Nothing) + (Frame (Id_aux (Id "0") Unknown) + (E_aux (E_id (Id_aux (Id "0") l)) (l,Just(typ,Tag_empty,ncs,effect))) 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) + end | E_if cond thn els -> resolve_outcome (interp_main t_level l_env l_mem cond) (fun value lm le -> match value with | V_lit(L_aux L_true _) -> interp_main t_level l_env lm thn | V_lit(L_aux L_false _) -> interp_main t_level l_env lm els - | _ -> (Error "Type error, not provided boolean for if",lm,l_env) end) - (fun a -> update_stack a (add_to_top_frame (fun c -> (E_aux (E_if c thn els) annot)))) + | _ -> (Error l "Type error, not provided boolean for if",lm,l_env) end) + (fun a -> update_stack a (add_to_top_frame (fun c -> (E_aux (E_if c thn els) (l,annot))))) | E_for id from to_ by order exp -> resolve_outcome (interp_main t_level l_env l_mem from) (fun from_val lm le -> @@ -647,36 +658,36 @@ and interp_main t_level l_env l_mem (E_aux exp annot) = (Unknown,Nothing)) (E_aux (E_lit (L_aux (L_num to_num) Unknown)) (Unknown,Nothing)) (E_aux (E_lit (L_aux (L_num by_num) Unknown)) (Unknown,Nothing)) - order exp) annot)]) - annot) - | _ -> (Error "by must be a number",lm,le) end) + order exp) (l,annot))]) + (l,annot)) + | _ -> (Error l "by must be a number",lm,le) end) (fun a -> update_stack a (add_to_top_frame (fun b -> (E_aux (E_for id (E_aux (E_lit (L_aux (L_num from_num) Unknown)) (Unknown,Nothing)) (E_aux (E_lit (L_aux (L_num to_num) Unknown)) (Unknown,Nothing)) - b order exp) annot)))) - | _ -> (Error "to must be a number",lm,le) end) + b order exp) (l,annot))))) + | _ -> (Error l "to must be a number",lm,le) end) (fun a -> update_stack a (add_to_top_frame (fun t -> (E_aux (E_for id (E_aux (E_lit (L_aux (L_num from_num) Unknown)) (Unknown,Nothing)) - t by order exp) annot)))) - | _ -> (Error "from must be a number",lm,le) end) - (fun a -> update_stack a (add_to_top_frame (fun f -> (E_aux (E_for id f to_ by order exp) annot)))) + t by order exp) (l,annot))))) + | _ -> (Error l "from must be a number",lm,le) end) + (fun a -> update_stack a (add_to_top_frame (fun f -> (E_aux (E_for id f to_ by order exp) (l,annot))))) | E_case exp pats -> resolve_outcome (interp_main t_level l_env l_mem exp) (fun v lm le -> match find_case pats v with - | Nothing -> (Error "No matching patterns in case",lm,le) + | Nothing -> (Error l "No matching patterns in case",lm,le) | Just (env,exp) -> interp_main t_level (env++l_env) lm exp end) - (fun a -> update_stack a (add_to_top_frame (fun e -> (E_aux (E_case e pats) annot)))) + (fun a -> update_stack a (add_to_top_frame (fun e -> (E_aux (E_case e pats) (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 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)) - annot)) + (l,annot))) (fun vs -> (V_record (List.zip fields vs))) l_env l_mem [] exps | E_record_update exp (FES_aux (FES_Fexps fexps _) fes_annot) -> resolve_outcome (interp_main t_level l_env l_mem exp) @@ -690,35 +701,35 @@ and interp_main t_level l_env l_mem (E_aux exp annot) = (FES_aux (FES_Fexps (map2 (fun id exp -> (FE_aux (FE_Fexp id exp) (Unknown,Nothing))) fields es) false) fes_annot)) - annot)) + (l,annot))) (fun vs -> (V_record (List.zip fields vs))) l_env l_mem [] exps) (fun vs lm le -> (Value (fupdate_record rv vs), lm, le)) (fun a -> a) - | _ -> (Error "record upate requires record",lm,le) end) + | _ -> (Error l "record upate requires record",lm,le) end) (fun a -> update_stack a (add_to_top_frame - (fun e -> E_aux(E_record_update e (FES_aux(FES_Fexps fexps false) fes_annot)) annot))) + (fun e -> E_aux(E_record_update e (FES_aux(FES_Fexps fexps false) fes_annot)) (l,annot)))) | E_list(exps) -> - exp_list t_level (fun exps -> E_aux (E_list exps) annot) V_list l_env l_mem [] exps + exp_list t_level (fun exps -> E_aux (E_list exps) (l,annot)) V_list l_env l_mem [] exps | E_cons hd tl -> resolve_outcome (interp_main t_level l_env l_mem hd) (fun hdv lm le -> resolve_outcome (interp_main t_level l_env lm tl) (fun tlv lm le -> match tlv with | V_list t -> (Value(V_list (hdv::t)),lm,le) - | _ -> (Error ":: of non-list value",lm,le) end) - (fun a -> update_stack a (add_to_top_frame (fun t ->E_aux (E_cons (to_exp hdv) t) annot)))) - (fun a -> update_stack a (add_to_top_frame (fun h -> E_aux (E_cons h tl) annot))) + | _ -> (Error l ":: of non-list value",lm,le) end) + (fun a -> update_stack a (add_to_top_frame (fun t ->E_aux (E_cons (to_exp hdv) t) (l,annot))))) + (fun a -> update_stack a (add_to_top_frame (fun h -> E_aux (E_cons h tl) (l,annot)))) | E_field exp id -> resolve_outcome (interp_main t_level l_env l_mem exp) (fun value lm le -> match value with | V_record fexps -> match in_env fexps id with | Just v -> (Value v,lm,l_env) - | Nothing -> (Error "Field not found in record",lm,le) end - | _ -> (Error "Field access requires a record",lm,le) + | Nothing -> (Error l "Field not found in record",lm,le) end + | _ -> (Error l "Field access requires a record",lm,le) end ) - (fun a -> update_stack a (add_to_top_frame (fun e -> E_aux(E_field e id) annot))) + (fun a -> update_stack a (add_to_top_frame (fun e -> E_aux(E_field e id) (l,annot)))) | E_vector_access vec i -> resolve_outcome (interp_main t_level l_env l_mem i) (fun iv lm le -> @@ -728,11 +739,11 @@ and interp_main t_level l_env l_mem (E_aux exp annot) = (fun vvec lm le -> match vvec with | V_vector base inc vals -> (Value (access_vector vvec n),lm,le) - | _ -> (Error "Vector access of non-vector",lm,le)end) + | _ -> (Error l "Vector access of non-vector",lm,le)end) (fun a -> update_stack a - (add_to_top_frame (fun v -> (E_aux (E_vector_access v (E_aux (E_lit (L_aux (L_num n) ln)) (ln,Nothing))) annot)))) - | _ -> (Error "Vector access not given a number for index",lm,l_env) end) - (fun a -> update_stack a (add_to_top_frame (fun i -> E_aux (E_vector_access vec i) annot))) + (add_to_top_frame (fun v -> (E_aux (E_vector_access v (E_aux (E_lit (L_aux (L_num n) ln)) (ln,Nothing))) (l,annot))))) + | _ -> (Error l "Vector access not given a number for index",lm,l_env) end) + (fun a -> update_stack a (add_to_top_frame (fun i -> E_aux (E_vector_access vec i) (l,annot)))) | E_vector_subrange vec i1 i2 -> resolve_outcome (interp_main t_level l_env l_mem i1) (fun i1v lm le -> @@ -746,21 +757,21 @@ and interp_main t_level l_env l_mem (E_aux exp annot) = (fun vvec lm le -> match vvec with | V_vector base inc vals -> (Value (slice_vector vvec n1 n2),lm,le) - | _ -> (Error "Vector slice of non-vector",lm,le)end) + | _ -> (Error l "Vector slice of non-vector",lm,le)end) (fun a -> update_stack a (add_to_top_frame (fun v -> (E_aux (E_vector_subrange v (E_aux (E_lit (L_aux (L_num n1) ln1)) (ln1,Nothing)) (E_aux (E_lit (L_aux (L_num n2) ln2)) (ln2,Nothing))) - annot)))) - | _ -> (Error "vector slice given non number for last index",lm,le) end) + (l,annot))))) + | _ -> (Error l "vector slice given non number for last index",lm,le) end) (fun a -> update_stack a (add_to_top_frame (fun i2 -> (E_aux (E_vector_subrange vec (E_aux (E_lit (L_aux (L_num n1) ln1)) (ln1,Nothing)) - i2) annot)))) - | _ -> (Error "Vector slice given non-number for first index",lm,le) end) - (fun a -> update_stack a (add_to_top_frame (fun i1 -> (E_aux (E_vector_subrange vec i1 i2) annot)))) + i2) (l,annot))))) + | _ -> (Error l "Vector slice given non-number for first index",lm,le) end) + (fun a -> update_stack a (add_to_top_frame (fun i1 -> (E_aux (E_vector_subrange vec i1 i2) (l,annot))))) | E_vector_update vec i exp -> resolve_outcome (interp_main t_level l_env l_mem i) (fun vi lm le -> @@ -772,18 +783,18 @@ and interp_main t_level l_env l_mem (E_aux exp annot) = (fun vec lm le -> match vec with | V_vector base inc vals -> (Value (fupdate_vec vec n1 vup), lm,le) - | _ -> (Error "Update of vector given non-vector",lm,le) end) + | _ -> (Error l "Update of vector given non-vector",lm,le) end) (fun a -> update_stack a (add_to_top_frame (fun v -> E_aux (E_vector_update v (E_aux (E_lit (L_aux (L_num n1) ln1)) (ln1,Nothing)) - (to_exp vup)) annot)))) + (to_exp vup)) (l,annot))))) (fun a -> update_stack a (add_to_top_frame (fun e -> E_aux (E_vector_update vec (E_aux (E_lit (L_aux (L_num n1) ln1)) (ln1,Nothing)) - e) annot))) - | _ -> (Error "Update of vector requires number for access",lm,le) end) - (fun a -> update_stack a (add_to_top_frame (fun i -> E_aux (E_vector_update vec i exp) annot))) + e) (l,annot)))) + | _ -> (Error l "Update of vector requires number for access",lm,le) end) + (fun a -> update_stack a (add_to_top_frame (fun i -> E_aux (E_vector_update vec i exp) (l,annot)))) | E_vector_update_subrange vec i1 i2 exp -> resolve_outcome (interp_main t_level l_env l_mem i1) (fun vi1 lm le -> @@ -801,33 +812,33 @@ and interp_main t_level l_env l_mem (E_aux exp annot) = (fun vvec lm le -> match vvec with | V_vector m inc vals -> (Value (fupdate_vector_slice vvec v_rep n1 n2),lm,le) - | _ -> (Error "Vector update requires vector",lm,le) end) + | _ -> (Error l "Vector update requires vector",lm,le) end) (fun a -> update_stack a (add_to_top_frame (fun v -> E_aux (E_vector_update_subrange v (E_aux (E_lit (L_aux (L_num n1) ln1)) (ln1,Nothing)) (E_aux (E_lit (L_aux (L_num n2) ln2)) (ln2,Nothing)) - (to_exp v_rep)) annot))))) + (to_exp v_rep)) (l,annot)))))) (fun a -> update_stack a (add_to_top_frame - (fun e -> E_aux (E_vector_update_subrange vec (to_exp vi1) (to_exp vi2) e) annot))) - | _ -> (Error "vector update requires number",lm,le) end) + (fun e -> E_aux (E_vector_update_subrange vec (to_exp vi1) (to_exp vi2) e) (l,annot)))) + | _ -> (Error l "vector update requires number",lm,le) end) (fun a -> - update_stack a (add_to_top_frame (fun i2 -> E_aux (E_vector_update_subrange vec (to_exp vi1) i2 exp) annot))) - | _ -> (Error "vector update requires number",lm,le) end) - (fun a -> update_stack a (add_to_top_frame (fun i1 -> E_aux (E_vector_update_subrange vec i1 i2 exp) annot))) + update_stack a (add_to_top_frame (fun i2 -> E_aux (E_vector_update_subrange vec (to_exp vi1) i2 exp) (l,annot)))) + | _ -> (Error l "vector update requires number",lm,le) end) + (fun a -> update_stack a (add_to_top_frame (fun i1 -> E_aux (E_vector_update_subrange vec i1 i2 exp) (l,annot)))) | E_tuple(exps) -> - exp_list t_level (fun exps -> E_aux (E_tuple exps) annot) V_tuple l_env l_mem [] exps + exp_list t_level (fun exps -> E_aux (E_tuple exps) (l,annot)) V_tuple l_env l_mem [] exps | E_vector(exps) -> - exp_list t_level (fun exps -> E_aux (E_vector exps) annot) (fun vals -> V_vector 0 true vals) l_env l_mem [] exps + exp_list t_level (fun exps -> E_aux (E_vector exps) (l,annot)) (fun vals -> V_vector 0 true vals) l_env l_mem [] exps | E_vector_indexed(iexps) -> let (indexes,exps) = List.unzip iexps in - exp_list t_level (fun es -> (E_aux (E_vector_indexed (map2 (fun i e -> (i,e)) indexes es)) annot)) + exp_list t_level (fun es -> (E_aux (E_vector_indexed (map2 (fun i e -> (i,e)) indexes es)) (l,annot))) (fun vals -> V_vector (List_extra.head indexes) true vals) (*Need to see increasing or not, can look at types later*) l_env l_mem [] exps | E_block(exps) -> interp_block t_level l_env l_env l_mem exps | E_app f args -> - (match (exp_list t_level (fun es -> E_aux (E_app f es) annot) - (fun vs -> match vs with | [] -> V_lit (L_aux L_unit Unknown) | [v] -> v | vs -> V_tuple vs end) + (match (exp_list t_level (fun es -> E_aux (E_app f es) (l,annot)) + (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) -> (match (f,t_level) with @@ -837,13 +848,13 @@ and interp_main t_level l_env l_mem (E_aux exp annot) = (match find_funcl funcls v with | Nothing -> let name = get_id id in - (Error (String.stringAppend "No matching pattern for function " name ),l_mem,l_env) + (Error l (String.stringAppend "No matching pattern for function " name ),l_mem,l_env) | Just(env,exp) -> resolve_outcome (interp_main t_level env l_mem exp) (fun ret lm le -> (Value ret, lm,l_env)) (fun a -> update_stack a - (fun stack -> (Frame (Id_aux (Id "0") Unknown) - (E_aux (E_id (Id_aux (Id "0") Unknown)) annot) l_env l_mem stack))) + (fun stack -> (Frame (Id_aux (Id "0") l) + (E_aux (E_id (Id_aux (Id "0") l)) (l,annot)) l_env l_mem stack))) end) | Nothing -> (match in_ctors ctors id with @@ -852,21 +863,21 @@ and interp_main t_level l_env l_mem (E_aux exp annot) = (match find_memory mems id with | Just(typ) -> (Action (Read_mem id v Nothing) - (Frame (Id_aux (Id "0") Unknown) (E_aux (E_id (Id_aux (Id "0") Unknown)) annot) le lm Top), lm, le) + (Frame (Id_aux (Id "0") l) (E_aux (E_id (Id_aux (Id "0") l)) (l,annot)) le lm Top), lm, le) | Nothing -> (match find_extern externs id with | Just(str) -> (Action (Call_extern str v) - (Frame (Id_aux (Id "0") Unknown) (E_aux (E_id (Id_aux (Id "0") Unknown)) annot) le lm Top), lm, le) - | Nothing -> (Error (String.stringAppend "Unknown function call " (get_id id)),lm,le) end) + (Frame (Id_aux (Id "0") l) (E_aux (E_id (Id_aux (Id "0") l)) (l,annot)) le lm Top), lm, le) + | Nothing -> (Error l (String.stringAppend "Unknown function call " (get_id id)),lm,le) end) end) end) end) end) | out -> out end) - | E_app_infix l op r -> + | E_app_infix lft op r -> let op = match op with | Id_aux (Id x) il -> Id_aux (DeIid x) il | _ -> op end in - resolve_outcome (interp_main t_level l_env l_mem l) + resolve_outcome (interp_main t_level l_env l_mem lft) (fun lv lm le -> resolve_outcome (interp_main t_level l_env lm r) (fun rv lm le -> @@ -877,29 +888,29 @@ and interp_main t_level l_env l_mem (E_aux exp annot) = (match find_extern externs op with | Just(str) -> (Action (Call_extern str (V_tuple [lv;rv])) - (Frame (Id_aux (Id "0") Unknown) - (E_aux (E_id (Id_aux (Id "0") Unknown)) annot) le lm Top),lm,le) + (Frame (Id_aux (Id "0") l) + (E_aux (E_id (Id_aux (Id "0") l)) (l,annot)) le lm Top),lm,le) | Nothing -> - (Error (String.stringAppend "No matching function " (get_id op)),lm,l_env) end) + (Error l (String.stringAppend "No matching function " (get_id op)),lm,l_env) end) | Just (funcls) -> (match find_funcl funcls (V_tuple [lv;rv]) with - | Nothing -> (Error "No matching pattern for function",lm,l_env) + | Nothing -> (Error l "No matching pattern for function",lm,l_env) | Just(env,exp) -> resolve_outcome (interp_main t_level env emem exp) (fun ret lm le -> (Value ret,l_mem,l_env)) (fun a -> update_stack a - (fun stack -> (Frame (Id_aux (Id "0") Unknown) - (E_aux (E_id (Id_aux (Id "0") Unknown)) annot) l_env l_mem stack))) + (fun stack -> (Frame (Id_aux (Id "0") l) + (E_aux (E_id (Id_aux (Id "0") l)) (l,annot)) l_env l_mem stack))) end) end) end)) - (fun a -> update_stack a (add_to_top_frame (fun r ->E_aux (E_app_infix (to_exp lv) op r) annot)))) - (fun a -> update_stack a (add_to_top_frame (fun l -> (E_aux (E_app_infix l op r) annot)))) + (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))))) | E_let (lbind : letbind tannot) exp -> match (interp_letbind t_level l_env l_mem lbind) with | ((Value v,lm,le),_) -> interp_main t_level le lm exp | (((Action a s as o),lm,le),Just lbuild) -> - ((update_stack o (add_to_top_frame (fun e -> (E_aux (E_let (lbuild e) exp) annot)))),lm,le) + ((update_stack o (add_to_top_frame (fun e -> (E_aux (E_let (lbuild e) exp) (l,annot))))),lm,le) | (e,_) -> e end | E_assign lexp exp -> resolve_outcome (interp_main t_level l_env l_mem exp) @@ -916,9 +927,9 @@ and interp_main t_level l_env l_mem (E_aux exp annot) = | (Action (Write_mem id a range value) stack) -> (Action (Write_mem id a range value) stack) | _ -> update_stack a (add_to_top_frame - (fun e -> (E_aux (E_assign (lexp_builder e) (to_exp v)) annot) )) end)) + (fun e -> (E_aux (E_assign (lexp_builder e) (to_exp v)) (l,annot)) )) end)) end)) - (fun a -> update_stack a (add_to_top_frame (fun v -> (E_aux (E_assign lexp v) annot)))) + (fun a -> update_stack a (add_to_top_frame (fun v -> (E_aux (E_assign lexp v) (l,annot))))) end and interp_block t_level init_env local_env local_mem exps = @@ -931,34 +942,41 @@ and interp_main t_level l_env l_mem (E_aux exp annot) = (fun a -> update_stack a (add_to_top_frame (fun e -> (E_aux (E_block(e::exps)) (Unknown,Nothing))))) end -and create_write_message_or_update t_level value l_env l_mem is_top_level ((LEXP_aux lexp annot):lexp tannot) = +and create_write_message_or_update t_level value l_env l_mem is_top_level ((LEXP_aux lexp (l,annot)):lexp tannot) = let (Env defs externs lets regs mems ctors) = t_level in + let (typ,tag,ncs,ef) = match annot with + | Nothing -> (T_var (Kid_aux (Var "fresh_v") Unknown), + Tag_empty, [], (Effect_aux (Effect_set []) Unknown)) + | Just(t, tag, ncs, ef) -> (t,tag,ncs,ef) end in match lexp with | LEXP_id id -> - match in_env l_env id with - | Just (V_boxref n) -> - if is_top_level - then ((Value (V_lit (L_aux L_unit Unknown)), update_mem l_mem n value, l_env),Nothing) - else ((Value (in_mem l_mem n), l_mem, l_env),Just (fun e -> LEXP_aux (LEXP_id id) annot)) - | Just v -> - if is_top_level then ((Error "Writes must be to reg values",l_mem,l_env),Nothing) - else ((Value v,l_mem,l_env),Just (fun e -> LEXP_aux(LEXP_id id) annot)) - | Nothing -> - match in_reg regs id with - | Just regf -> + match tag with + | Tag_empty -> + match in_env l_env id with + | Just (V_boxref n) -> + if is_top_level + then ((Value (V_lit (L_aux L_unit l)), update_mem l_mem n value, l_env),Nothing) + else ((Value (in_mem l_mem n), l_mem, l_env),Just (fun e -> LEXP_aux (LEXP_id id) (l,annot))) + | Just v -> + if is_top_level then ((Error l "Writes must be to reg values",l_mem,l_env),Nothing) + else ((Value v,l_mem,l_env),Just (fun e -> LEXP_aux(LEXP_id id) (l,annot))) + | Nothing -> + if is_top_level + then begin + let (Mem c m) = l_mem in + let l_mem = (Mem (c+1) m) in + ((Value (V_lit (L_aux L_unit l)), update_mem l_mem c value, (id,(V_boxref c))::l_env),Nothing) + end + else ((Error l (String.stringAppend "Undefined id " (get_id id)),l_mem,l_env),Nothing) + end + | Tag_extern _ -> + let regf = Reg id typ in let request = (Action (Write_reg regf Nothing value) - (Frame (Id_aux (Id "0") Unknown) - (E_aux (E_id (Id_aux (Id "0") Unknown)) annot) 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) annot)) - | Nothing -> - if is_top_level - then begin - let (Mem c m) = l_mem in - let l_mem = (Mem (c+1) m) in - ((Value (V_lit (L_aux L_unit Unknown)), update_mem l_mem c value, (id,(V_boxref c))::l_env),Nothing) - end - else ((Error "Undefined id",l_mem,l_env),Nothing) - end + (Frame (Id_aux (Id "0") l) + (E_aux (E_id (Id_aux (Id "0") l)) + (l,Just(typ,Tag_empty,ncs,ef))) 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 | LEXP_memory id exps -> match (exp_list t_level (fun exps -> E_aux (E_tuple exps) (Unknown,Nothing)) @@ -966,11 +984,11 @@ and create_write_message_or_update t_level value l_env l_mem is_top_level ((LEXP l_env l_mem [] exps) with | (Value v,lm,le) -> let request = (Action (Write_mem id v Nothing value) - (Frame (Id_aux (Id "0") Unknown) (E_aux (E_id (Id_aux (Id "0") Unknown)) annot) l_env lm Top),lm,l_env) in + (Frame (Id_aux (Id "0") l) (E_aux (E_id (Id_aux (Id "0") l)) (l,annot)) 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)) annot))) - | (Action a s,lm, le) -> ((Action a s,lm,le), Just (fun (E_aux (E_tuple es) _) -> (LEXP_aux (LEXP_memory id es) annot))) + (LEXP_aux (LEXP_memory id (match v with | V_tuple vs -> (List.map to_exp vs) | v -> [to_exp v]end)) (l,annot)))) + | (Action a s,lm, le) -> ((Action a s,lm,le), Just (fun (E_aux (E_tuple es) _) -> (LEXP_aux (LEXP_memory id es) (l,annot)))) | e -> (e,Nothing) end | LEXP_vector lexp exp -> match (interp_main t_level l_env l_mem exp) with @@ -978,7 +996,7 @@ and create_write_message_or_update t_level value l_env l_mem is_top_level ((LEXP (match i with | V_lit (L_aux (L_num n) ln) -> let next_builder le_builder = (fun e -> - LEXP_aux (LEXP_vector (le_builder e) (E_aux (E_lit (L_aux (L_num n) ln)) (ln,Nothing))) annot) in + LEXP_aux (LEXP_vector (le_builder e) (E_aux (E_lit (L_aux (L_num n) ln)) (ln,Nothing))) (l,annot)) in (match (create_write_message_or_update t_level value l_env lm false lexp) with | ((Value v,lm,le),maybe_builder) -> (match v with @@ -986,10 +1004,10 @@ and create_write_message_or_update t_level value l_env l_mem is_top_level ((LEXP let nth = access_vector v n in (match (nth,is_top_level,maybe_builder) with | (V_boxref n,true,_) -> ((Value (V_lit (L_aux L_unit Unknown)), update_mem lm n value, l_env),Nothing) - | (v,true,_) -> ((Error "Vector does not contain reg values",lm,l_env),Nothing) + | (v,true,_) -> ((Error l "Vector does not contain reg values",lm,l_env),Nothing) | ((V_boxref n),false, Just lexp_builder) -> ((Value (in_mem lm n),lm, l_env),Just (next_builder lexp_builder)) | (v,false, Just lexp_builder) -> ((Value v,lm,le), Just (next_builder lexp_builder)) end) - | _ -> ((Error "Vector access of non-vector",lm,l_env),Nothing) end) + | _ -> ((Error l "Vector access of non-vector",lm,l_env),Nothing) end) | ((Action a s,lm,le),Just lexp_builder) -> (match (a,is_top_level) with | ((Write_reg regf Nothing value),true) -> ((Action (Write_reg regf (Just (n,n)) value) s, lm,le), Nothing) @@ -1000,8 +1018,8 @@ and create_write_message_or_update t_level value l_env l_mem is_top_level ((LEXP ((Action (Write_mem id a (Just (n,n)) value) s,lm,le), Just (next_builder lexp_builder)) | _ -> ((Action a s,lm,le), Just (next_builder lexp_builder)) end) | e -> e end) - | _ -> ((Error "Vector access must be a number",lm,le),Nothing) end) - | (Action a s,lm,le) -> ((Action a s,lm,le), Just (fun e -> (LEXP_aux (LEXP_vector lexp e) annot))) + | _ -> ((Error l "Vector access must be a number",lm,le),Nothing) end) + | (Action a s,lm,le) -> ((Action a s,lm,le), Just (fun e -> (LEXP_aux (LEXP_vector lexp e) (l,annot)))) | e -> (e,Nothing) end | LEXP_vector_range lexp exp1 exp2 -> match (interp_main t_level l_env l_mem exp1) with @@ -1015,7 +1033,7 @@ and create_write_message_or_update t_level value l_env l_mem is_top_level ((LEXP let next_builder le_builder = (fun e -> LEXP_aux (LEXP_vector_range (le_builder e) (E_aux (E_lit (L_aux (L_num n1) ln1)) (ln1,Nothing)) - (E_aux (E_lit (L_aux (L_num n2) ln2)) (ln2,Nothing))) annot) in + (E_aux (E_lit (L_aux (L_num n2) ln2)) (ln2,Nothing))) (l,annot)) in (match (create_write_message_or_update t_level value l_env lm false lexp) with | ((Value v,lm,le), Just lexp_builder) -> (match (v,is_top_level) with @@ -1023,7 +1041,7 @@ and create_write_message_or_update t_level value l_env l_mem is_top_level ((LEXP ((Value (V_lit (L_aux L_unit Unknown)), update_vector_slice (slice_vector v n1 n2) value lm, l_env), Nothing) | (V_vector m inc vs,false) -> ((Value (slice_vector v n1 n2),lm,l_env), Just (next_builder lexp_builder)) - | _ -> ((Error "Vector required",lm,le),Nothing) end) + | _ -> ((Error l "Vector required",lm,le),Nothing) end) | ((Action (Write_reg regf Nothing value) s, lm,le), Just lexp_builder) -> ((Action (Write_reg regf (Just (n1,n2)) value) s,lm,le), Just (next_builder lexp_builder)) | ((Action (Write_mem id a Nothing value) s,lm,le), Just lexp_builder) -> @@ -1031,15 +1049,15 @@ and create_write_message_or_update t_level value l_env l_mem is_top_level ((LEXP | ((Action a s,lm,le), Just lexp_builder) -> ((Action a s,lm,le), Just (next_builder lexp_builder)) | e -> e end) - | _ -> ((Error "Vector slice requires a number", lm, le),Nothing) end) + | _ -> ((Error l "Vector slice requires a number", lm, le),Nothing) end) | (Action a s,lm,le) -> ((Action a s,lm, le), Just (fun e -> LEXP_aux (LEXP_vector_range lexp (E_aux (E_lit (L_aux (L_num n1) ln1)) (ln1,Nothing)) - e) annot)) + e) (l,annot))) | e -> (e,Nothing) end) - | _ -> ((Error "Vector slice requires a number", lm, le),Nothing) end) + | _ -> ((Error l "Vector slice requires a number", lm, le),Nothing) end) | (Action a s,lm,le) -> - ((Action a s, lm,le), Just (fun e -> LEXP_aux (LEXP_vector_range lexp e exp2) annot)) + ((Action a s, lm,le), Just (fun e -> LEXP_aux (LEXP_vector_range lexp e exp2) (l,annot))) | e -> (e,Nothing) end | LEXP_field lexp id -> (match (create_write_message_or_update t_level value l_env l_mem false lexp) with @@ -1047,37 +1065,37 @@ and create_write_message_or_update t_level value l_env l_mem is_top_level ((LEXP match (in_env fexps id,is_top_level) with | (Just (V_boxref n),true) -> ((Value (V_lit (L_aux L_unit Unknown)), update_mem lm n value, l_env),Nothing) | (Just (V_boxref n),false) -> - ((Value (in_mem lm n),lm,l_env),Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) annot)) - | (Just v, true) -> ((Error "Field access requires record",lm,le),Nothing) - | (Just v,false) -> ((Value v,lm,l_env),Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) annot)) - | (Nothing,_) -> ((Error "Field not found in specified record",lm,le),Nothing) end + ((Value (in_mem lm n),lm,l_env),Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) (l,annot))) + | (Just v, true) -> ((Error l "Field access requires record",lm,le),Nothing) + | (Just v,false) -> ((Value v,lm,l_env),Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) (l,annot))) + | (Nothing,_) -> ((Error l "Field not found in specified record",lm,le),Nothing) end | ((Action a s,lm,le), Just lexp_builder) -> match a with - | Read_reg _ _ -> ((Action a s,lm,le), Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) annot)) - | Read_mem _ _ _ -> ((Action a s,lm,le), Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) annot)) - | Call_extern _ _ -> ((Action a s,lm,le), Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) annot)) - | _ -> ((Error "Unimplemented feature, writing to a field in a register or memory",lm,le),Nothing) + | Read_reg _ _ -> ((Action a s,lm,le), Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) (l,annot))) + | Read_mem _ _ _ -> ((Action a s,lm,le), Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) (l,annot))) + | Call_extern _ _ -> ((Action a s,lm,le), Just (fun e -> LEXP_aux (LEXP_field (lexp_builder e) id) (l,annot))) + | _ -> ((Error l "Unimplemented feature, writing to a field in a register or memory",lm,le),Nothing) end | e -> e end) end -and interp_letbind t_level l_env l_mem (LB_aux lbind annot) = +and interp_letbind t_level l_env l_mem (LB_aux lbind (l,annot)) = match lbind with | LB_val_explicit t pat exp -> match (interp_main t_level l_env l_mem exp) with | (Value v,lm,le) -> (match match_pattern pat v with - | (true,env) -> ((Value (V_lit (L_aux L_unit Unknown)), lm, env++l_env),Nothing) - | _ -> ((Error "Pattern in letbind did not match value",lm,le),Nothing) end) - | (Action a s,lm,le) -> ((Action a s,lm,le),(Just (fun e -> (LB_aux (LB_val_explicit t pat e) annot)))) + | (true,env) -> ((Value (V_lit (L_aux L_unit l)), lm, env++l_env),Nothing) + | _ -> ((Error l "Pattern in letbind did not match value",lm,le),Nothing) end) + | (Action a s,lm,le) -> ((Action a s,lm,le),(Just (fun e ->(LB_aux (LB_val_explicit t pat e) (l,annot))))) | e -> (e,Nothing) end | LB_val_implicit pat exp -> match (interp_main t_level l_env l_mem exp) with | (Value v,lm,le) -> (match match_pattern pat v with - | (true,env) -> ((Value (V_lit (L_aux L_unit Unknown)), lm, env++l_env),Nothing) - | _ -> ((Error "Pattern in letbind did not match value",lm,le),Nothing) end) - | (Action a s,lm,le) -> ((Action a s,lm,le),(Just (fun e -> (LB_aux (LB_val_implicit pat e) annot)))) + | (true,env) -> ((Value (V_lit (L_aux L_unit l)), lm, env++l_env),Nothing) + | _ -> ((Error l "Pattern in letbind did not match value",lm,le),Nothing) end) + | (Action a s,lm,le) -> ((Action a s,lm,le),(Just (fun e -> (LB_aux (LB_val_implicit pat e) (l,annot))))) | e -> (e,Nothing) end end @@ -1085,12 +1103,12 @@ let rec to_global_letbinds (Defs defs) t_level = let (Env defs' externs lets regs mems ctors) = t_level in match defs with | [] -> ((Value (V_lit (L_aux L_unit Unknown)), emem, []),t_level) - | (DEF_aux def _)::defs -> + | (DEF_aux def (l,_))::defs -> match def with | DEF_val lbind -> match interp_letbind t_level [] emem lbind with | ((Value v,lm,le),_) -> to_global_letbinds (Defs defs) (Env defs' externs (lets++le) regs mems ctors) - | ((Action a s,lm,le),_) -> ((Error "Top level let may not access memory, registers or (for now) external functions", lm,le),t_level) + | ((Action a s,lm,le),_) -> ((Error l "Top level let may not access memory, registers or (for now) external functions", lm,le),t_level) | (e,_) -> (e,t_level) end | _ -> to_global_letbinds (Defs defs) t_level end @@ -1110,7 +1128,7 @@ let interp defs exp = let rec resume_main t_level stack value = match stack with - | Top -> Error "Top hit without place to put value" + | Top -> Error Unknown "Top hit without place to put value" | Frame id exp env mem Top -> match interp_main t_level ((id,value)::env) mem exp with | (o,_,_) -> o end | Frame id exp env mem stack -> @@ -1118,7 +1136,7 @@ let rec resume_main t_level stack value = | Value v -> match interp_main t_level ((id,v)::env) mem exp with | (o,_,_) -> o end | Action action stack -> Action action (Frame id exp env mem stack) - | Error s -> Error s + | Error l s -> Error l s end end diff --git a/src/lem_interp/run_interp.ml b/src/lem_interp/run_interp.ml index 76973c04..32cfa789 100644 --- a/src/lem_interp/run_interp.ml +++ b/src/lem_interp/run_interp.ml @@ -22,6 +22,14 @@ let id_to_string = function | Id_aux(Id s,_) | Id_aux(DeIid s,_) -> s ;; +let loc_to_string = function + | Unknown -> "Unknown" + | Trans(s,_) -> s + | Range(s,fline,fchar,tline,tchar) -> + "in " ^ s ^ " from line " ^ (string_of_int fline) ^ " character " ^ (string_of_int fchar) ^ + " to line " ^ (string_of_int tline) ^ " character " ^ (string_of_int tchar) +;; + let bitvec_to_string l = "0b" ^ (String.concat "" (List.map (function | V_lit(L_aux(L_zero, _)) -> "0" | V_lit(L_aux(L_one, _)) -> "1" @@ -82,15 +90,22 @@ let act_to_string = function sprintf "extern call %s applied to %s" name (val_to_string arg) ;; +let id_compare i1 i2 = + match (i1, i1) with + | (Id_aux(Id(i1),_),Id_aux(Id(i2),_)) + | (Id_aux(Id(i1),_),Id_aux(DeIid(i2),_)) + | (Id_aux(DeIid(i1),_),Id_aux(Id(i2),_)) + | (Id_aux(DeIid(i1),_),Id_aux(DeIid(i2),_)) -> compare i1 i2 + module Reg = struct - include Map.Make(struct type t = id let compare = compare end) + include Map.Make(struct type t = id let compare = id_compare end) end ;; module Mem = struct include Map.Make(struct type t = (id * big_int) let compare (i1, v1) (i2, v2) = - match compare i1 i2 with + match id_compare i1 i2 with | 0 -> compare_big_int v1 v2 | n -> n end) @@ -164,8 +179,8 @@ let run (name, test) = let return, env' = perform_action env a in eprintf "%s: action returned %s\n" name (val_to_string return); loop env' (resume test s return) - | Error e -> eprintf "%s: error: %s\n" name e; false in - let entry = E_aux(E_app(Id_aux((Id "main"),Unknown), [E_aux(E_lit (L_aux(L_unit,Interp_ast.Unknown)),(Unknown,None))]),(Unknown,None)) in + | Error(l, e) -> eprintf "%s: %s: error: %s\n" name (loc_to_string l) e; false in + let entry = E_aux(E_app(Id_aux((Id "main"),Unknown), [E_aux(E_lit (L_aux(L_unit,Unknown)),(Unknown,None))]),(Unknown,None)) in eprintf "%s: starting\n" name; try Printexc.record_backtrace true; |