proposed split of decode into decode-to-instruction and instruction-to-instructionstate

2 files changed, 21 insertions, 3 deletions

diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index 06782451..120241f4 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -301,16 +301,24 @@ let decode_to_istate top_level value =
     | (Nothing, Just err) -> Decode_error err
 end
 
+
+let decode_to_instruction top_level value = 
+  match decode_to_istate top_level value with
+  | Instr inst is -> IDE_instr inst
+  | Decode_error de -> IDE_decode_error de
+  end
+
+
 let instruction_to_istate top_level ((name, parms, _) as instr) = 
   let mode = make_mode true false in
   let get_value (name,typ,v) = let (e,_) = Interp.to_exp mode Interp.eenv (intern_value v) in e in
-  (Instr instr
+(*  (Instr instr*)
     (Interp.Thunk_frame
        (E_aux (E_app (Id_aux (Id "execute") Interp_ast.Unknown) 
 		 [(E_aux (E_app (Id_aux (Id name) Interp_ast.Unknown) (List.map get_value parms))
 		        (Interp_ast.Unknown,Interp.ctor_annot (T_id "ast")) (*This type shouldn't be hard-coded*))])
 	      (Interp_ast.Unknown,Nothing))
-       top_level Interp.eenv Interp.emem Interp.Top))
+       top_level Interp.eenv Interp.emem Interp.Top) (*)*)
 
 let rec interp_to_outcome mode thunk = 
   match thunk () with
diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index 4d3e4b35..ca0ab9f3 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -123,6 +123,11 @@ type decode_error =
   | Not_an_instruction_error of value
   | Internal_error of string
 
+type instruction_or_decode_error =
+  | IDE_instr of instruction
+  | IDE_decode_error of decode_error
+
+(** propose to remove the following type and use the above instead *)
 type i_state_or_error =
   | Instr of instruction * instruction_state
   | Decode_error of decode_error
@@ -132,9 +137,14 @@ val num_to_bits : nat -> v_kind -> integer
 (** proposed: *)
 val nat_to_bytevector : nat -> list word8 
 
-(*Function to decode an instruction and build the state to run it*)
+
+(** propose to remove this: Function to decode an instruction and build the state to run it*)
 val decode_to_istate : context -> value -> i_state_or_error
 
+(** propose to add this, and then use instruction_to_istate on the result: Function to decode an instruction and build the state to run it*)
+(** PS made a placeholder in interp_inter_imp.lem, but it just uses decode_to_istate and throws away the istate; surely it's easy to just do what's necessary to get the instruction.   This sort-of works, but it crashes on ioid 10 after 167 steps - maybe instruction_to_istate (which I wasn't using directly before) isn't quite right? *)
+val decode_to_instruction : context -> value -> instruction_or_decode_error
+
 (*Function to generate the state to run from an instruction form; is always an Instr*)
 val instruction_to_istate : context -> instruction -> i_state_or_error