diff options
Diffstat (limited to 'src/lem_interp/interp_inter_imp.lem')
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 15 |
1 files changed, 10 insertions, 5 deletions
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index 028b5def..59acb04a 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -6,17 +6,21 @@ import Num val intern_value : value -> Interp.value val extern_value : 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 | 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))) l) -let from_bits l = (List.map (fun | Interp.V_lit (Interp_ast.L_aux Interp_ast.L_zero _) -> false - | _ -> true) l) +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) +let from_bits l = (List.map (fun b -> match b with + | Interp.V_lit (Interp_ast.L_aux Interp_ast.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) +end let intern_value v = match v with | Bitvector bs -> Interp.V_vector 0 true (to_bits bs) @@ -36,6 +40,7 @@ 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) +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 @@ -53,6 +58,6 @@ let interp mode i_state = -> 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*) + | Interp.Call_extern id value -> (*Connect here to a list of external functions*) foo end end |