1 files changed, 40 insertions, 0 deletions
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
new file mode 100644
index 00000000..8b7fdec3
--- /dev/null
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -0,0 +1,40 @@
+import Interp
+import Interp_lib
+open import Interp_interface
+
+val intern_value : value -> Interp.value
+val extern_value : Interp.value -> value
+
+let build_context defs = Interp.to_top_env defs
+
+let intern_value v = match v with
+  | Bitvector bs -> Interp.V_vector 0 true (List.map (fun | 0 -> (Interp.V_lit (Interp_ast.L_aux Interp_ast.L_zero Interp_ast.Unknown)) 
+							  | _ -> (Interp.V_lit (Interp_ast.L_aux Interp_ast.L_one Interp_ast.Unknown))) bs)
+  | Unknown -> Interp.V_unknown
+end
+
+let extern_value v = match v with
+  | Interp.V_vector _ true bits -> Bitvector (List.map (fun | Interp.V_lit (Interp_ast.L_aux Interp_ast.L_zero _) -> 0
+							    | _ -> 1) bits)
+  | _ -> Unknown
+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
+
+let interp mode i_state = 
+  match Interp.resume mode i_state None 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_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*)
+    end 
+  end