Add a decoding function to interp_interface and interp_inter_imp. (Note, this is quite specific to Power's spec)

2 files changed, 56 insertions, 0 deletions

diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index afa58f6d..14a286cb 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -91,6 +91,53 @@ let memory_functions =
 		      (v,len,regs) end end)));
   ]
 
+let rec interp_to_value_helper thunk = 
+  match thunk() with
+    | Interp.Value value -> (Just value,Nothing)
+    | Interp.Error l msg -> (Nothing, Just (Internal_error msg))
+    | Interp.Action (Interp.Call_extern i value) stack ->
+      match List.lookup i external_functions with
+	| Nothing -> (Nothing, Just (Internal_error ("External function not available " ^ i)))
+	| Just f  -> 
+          interp_to_value_helper (fun _ -> Interp.resume (make_mode true false) stack (Just (f value)))
+      end 
+    | Interp.Action (Interp.Exit (E_aux e _)) _ ->
+      match e with
+	| E_id (Id_aux (Id "unsupported_instruction") _) -> (Nothing,Just Unsupported_instruction_error)
+	| E_id (Id_aux (Id "no_matching_pattern") _) -> (Nothing,Just Not_an_instruction_error)
+      end 
+    | _ -> (Nothing, Just (Internal_error "Memory or register requested in decode"))
+end
+
+let decode_to_istate top_level value = 
+  let mode = make_mode true false in
+  let (arg,_) = Interp.to_exp mode Interp.eenv (intern_value value) in
+  let (instr_decoded,error) = interp_to_value_helper 
+    (fun _ -> Interp.resume 
+      (make_mode true false) 
+      (Interp.Thunk_frame 
+	 (E_aux (E_app (Id_aux (Id "decode") Interp_ast.Unknown) [arg]) (Interp_ast.Unknown, Nothing)) 
+	 top_level Interp.eenv Interp.emem Interp.Top) Nothing) in
+  match (instr_decoded,error) with
+    | (Just instr, _) -> 
+      let (arg,_) = Interp.to_exp mode Interp.eenv instr in
+      let (instr_decoded,error) = interp_to_value_helper
+	(fun _ -> Interp.resume 
+	 (make_mode true false) 
+	 (Interp.Thunk_frame 
+	 (E_aux (E_app (Id_aux (Id "supported_instructions") Interp_ast.Unknown) [arg]) (Interp_ast.Unknown, Nothing)) 
+	 top_level Interp.eenv Interp.emem Interp.Top) Nothing) in
+      match (instr_decoded,error) with
+	| (Just instr,_) ->
+	  let (arg,_) = Interp.to_exp mode Interp.eenv instr in
+	  Instr (Interp.Thunk_frame
+		   (E_aux (E_app (Id_aux (Id "execute") Interp_ast.Unknown) [arg]) (Interp_ast.Unknown,Nothing))
+		   top_level Interp.eenv Interp.emem Interp.Top)
+	| (Nothing, Just err) -> err
+      end 
+    | (Nothing, Just err) -> err
+end
+
 let rec interp_to_outcome mode thunk = 
   match thunk () with
   | Interp.Value _ -> Done
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index d49edfd5..9f967b1e 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -66,6 +66,15 @@ val build_context : Interp_ast.defs Interp.tannot -> context (*defs should come
 val initial_instruction_state : context -> string -> list value -> instruction_state 
   (* string is a function name, list of value are the parameters to that function *)
 
+type i_state_or_error =
+  | Instr of instruction_state
+  | Unsupported_instruction_error
+  | Not_an_instruction_error
+  | Internal_error of string
+
+(*Function to decode an instruction and build the state to run it*)
+val decode_to_istate : context -> value -> i_state_or_error
+
 (* Big step of the interpreter, to the next request for an external action *)
 (* When interp_mode has eager_eval false, interpreter is (close to) small step *)
 val interp : interp_mode -> instruction_state -> outcome