Connect interpreter to representation of instructions.

Warning: this changes a few of the constructor names in the instruction_extractor.lem interface

3 files changed, 69 insertions, 28 deletions

diff --git a/src/lem_interp/instruction_extractor.lem b/src/lem_interp/instruction_extractor.lem
index d4a52890..d2597740 100644
--- a/src/lem_interp/instruction_extractor.lem
+++ b/src/lem_interp/instruction_extractor.lem
@@ -2,13 +2,13 @@ open import Interp_ast
 open import Interp_utilities
 open import Pervasives
 
-type typ = 
-| Bit
-| Bitvector of maybe integer
-| Other
+type instr_parm_typ = 
+| IBit
+| IBitvector of maybe integer
+| IOther
 
 type instruction_form = 
-|  Instr of string * list (string * typ) * list base_effect
+|  Instr_form of string * list (string * instr_parm_typ) * list base_effect
 |  Skipped 
 
 val extract_instructions : string -> string -> defs tannot -> list instruction_form
@@ -17,13 +17,14 @@ let extract_parm (E_aux e (_,tannot)) =
   match e with
     | E_id (Id_aux (Id i) _) ->
       match tannot with
-	| Just(T_id "bit",_,_,_) -> (i,Bit)
+	| Just(T_id "bit",_,_,_) -> (i,IBit)
+	| Just(T_id "bool",_,_,_) -> (i,IBit)
 	| Just(T_app "vector" (T_args [T_arg_nexp _; T_arg_nexp (Ne_const len); _; T_arg_typ (T_id "bit")]),_,_,_) ->
-	  (i,Bitvector (Just len))
+	  (i,IBitvector (Just len))
 	| Just(T_app "vector" (T_args [T_arg_nexp _; T_arg_nexp _; _; T_arg_typ (T_id "bit")]),_,_,_) ->
-	  (i,Bitvector Nothing)
-	| _ -> (i,Other) end
-    | _ -> ("UNKNOWN_PARM",Other)
+	  (i,IBitvector Nothing)
+	| _ -> (i,IOther) end
+    | _ -> ("UNKNOWN_PARM",IOther)
 end
 
 let rec extract_from_decode decoder = 
@@ -32,7 +33,7 @@ let rec extract_from_decode decoder =
     | (FCL_aux (FCL_Funcl _ pat exp) _)::decoder ->
       (match exp with
 	| E_aux (E_app (Id_aux(Id id) _) parms) (_,(Just (_,Tag_ctor,_,_))) ->
-	  Instr id (List.map extract_parm parms) []
+	  Instr_form id (List.map extract_parm parms) []
 	| _ -> Skipped end)::(extract_from_decode decoder)
 end 
 
@@ -49,8 +50,8 @@ let rec extract_effects instrs execute =
   match instrs with
     | [] -> []
     | Skipped::instrs -> Skipped::(extract_effects instrs execute)
-    | (Instr id parms [])::instrs -> 
-      (Instr id parms (extract_effects_of_fcl id execute))::(extract_effects instrs execute)
+    | (Instr_form id parms [])::instrs -> 
+      (Instr_form id parms (extract_effects_of_fcl id execute))::(extract_effects instrs execute)
 end
 
 let extract_instructions decode_name execute_name defs = 
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index a436d652..6febc709 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -7,6 +7,8 @@ open import String_extra (* for 'show' to convert nat to string) *)
 open import Interp_ast
 open import Interp_utilities
 
+open import Instruction_extractor
+
 type tannot = Interp_utilities.tannot
 
 val intern_annot : tannot -> tannot
@@ -112,9 +114,17 @@ type lenv = LEnv of nat * env
 let emem = LMem 1 Map.empty
 let eenv = LEnv 1 []
 
+type sub_reg_map = list (id * index_range)
+
 (*top_level is a tuple of 
-  (all definitions, letbound and enum values, register values, Typedef union constructors, sub register mappings, and register aliases) *)
-type top_level = Env of (defs tannot) * env * env * list (id * typ) * list (id * list (id * index_range)) * list (id * (alias_spec tannot))
+  (all definitions,
+   all extracted instructions (where possible),
+   letbound and enum values, 
+   register values, 
+   Typedef union constructors, 
+   sub register mappings, and register aliases) *)
+type top_level = 
+  | Env of (defs tannot) * list instruction_form * env * env * list (id * typ) * list (id * sub_reg_map) * list (id * (alias_spec tannot))
 
 type action = 
  | Read_reg of reg_form * maybe (integer * integer)
@@ -982,7 +992,7 @@ let rec exp_list mode t_level build_e build_v l_env l_mem vals exps =
   end
 
 and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
-  let (Env defs lets regs ctors subregs aliases) = t_level in 
+  let (Env defs instrs lets regs ctors subregs aliases) = t_level in 
   let (typ,tag,ncs,effect) = match annot with 
     | Nothing -> (T_var "fresh_v", Tag_empty, [], (Effect_aux (Effect_set []) Unknown))
     | Just(t, tag, ncs, ef) -> (t,tag,ncs,ef) end in
@@ -1757,7 +1767,7 @@ and interp_main mode t_level l_env l_mem (E_aux exp (l,annot)) =
     end
 
 and create_write_message_or_update mode t_level value l_env l_mem is_top_level ((LEXP_aux lexp (l,annot)):lexp tannot) : ((outcome * lmem * lenv) * maybe ((exp tannot) -> lenv -> ((lexp tannot) * lenv))) =
-   let (Env defs lets regs ctors subregs aliases) = t_level in
+   let (Env defs instrs lets regs ctors subregs aliases) = t_level in
   let (typ,tag,ncs,ef) = match annot with 
     | Nothing -> (T_var "fresh_v", Tag_empty, [], (Effect_aux (Effect_set []) Unknown))
     | Just(t, tag, ncs, ef) -> (t,tag,ncs,ef) end in
@@ -2068,7 +2078,7 @@ and interp_letbind mode t_level l_env l_mem (LB_aux lbind (l,annot)) =
 end	
 
 and interp_alias_read mode t_level l_env l_mem (AL_aux alspec (l,annot)) =
-  let (Env defs lets regs ctors subregs aliases) = t_level in 
+  let (Env defs instrs lets regs ctors subregs aliases) = t_level in 
   let stack = Hole_frame (Id_aux (Id "0") Unknown)
 		          (E_aux (E_id (Id_aux (Id "0") l)) (l,(intern_annot annot)))
 			  t_level l_env l_mem Top in
@@ -2113,14 +2123,14 @@ and interp_alias_read mode t_level l_env l_mem (AL_aux alspec (l,annot)) =
 			        (l,(intern_annot annot))) t_level l_env l_mem Top), l_mem,l_env) end
 
 let rec to_global_letbinds (Defs defs) t_level =
-  let  (Env defs' lets regs ctors subregs aliases) = t_level in
+  let  (Env defs' instrs lets regs ctors subregs aliases) = t_level in
   match defs with
   | [] -> ((Value (V_lit (L_aux L_unit Unknown)), emem, eenv),t_level)
   | def::defs ->
     match def with
     | DEF_val lbind ->
       match interp_letbind <|eager_eval=true; track_values=false;|> t_level eenv emem lbind with
-      | ((Value v,lm,(LEnv _ le)),_) -> to_global_letbinds (Defs defs) (Env defs' (lets++le) regs ctors subregs aliases)
+      | ((Value v,lm,(LEnv _ le)),_) -> to_global_letbinds (Defs defs) (Env defs' instrs (lets++le) regs ctors subregs aliases)
       | ((Action a s,lm,le),_) -> 
 	((Error Unknown "Top level let may not access memory, registers or (for now) external functions", lm,le),t_level)
       | (e,_) -> (e,t_level) end
@@ -2128,14 +2138,17 @@ let rec to_global_letbinds (Defs defs) t_level =
       match tdef with
       | TD_enum id ns ids _ -> 
         let enum_vals = map (fun eid -> (eid,V_ctor eid (T_id (get_id id)) unitv)) ids in
-        to_global_letbinds (Defs defs) (Env defs' (lets++enum_vals) regs ctors subregs aliases)
+        to_global_letbinds (Defs defs) (Env defs' instrs (lets++enum_vals) regs ctors subregs aliases)
       | _ -> to_global_letbinds (Defs defs) t_level end
     | _ -> to_global_letbinds (Defs defs) t_level
     end
   end
 
+(*TODO Contemplate making decode and execute environment variables instead of these constants*)
 let to_top_env defs = 
-  let t_level = Env defs [] (to_registers defs) (to_data_constructors defs) (to_register_fields defs) (to_aliases defs) in
+  let t_level = Env defs (extract_instructions "decode" "execute" defs) 
+                    [] (* empty letbind and enum values, call below will fill in any *) 
+		    (to_registers defs) (to_data_constructors defs) (to_register_fields defs) (to_aliases defs) in
   let (o,t_level) = to_global_letbinds defs t_level in
   match o with
     | (Value _,_,_) -> (Nothing,t_level)
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem
index c18f07f7..b930e8ec 100644
--- a/src/lem_interp/interp_inter_imp.lem
+++ b/src/lem_interp/interp_inter_imp.lem
@@ -1,5 +1,6 @@
 import Interp
 import Interp_lib
+import Instruction_extractor
 open import Interp_ast
 open import Interp_interface
 open import Pervasives
@@ -129,7 +130,7 @@ let memory_functions =
 	      end end end)));
   ]
 
-let rec interp_to_value_helper arg thunk = 
+let rec interp_to_value_helper arg instr thunk = 
   match thunk() with
     | Interp.Value value -> (Just value,Nothing)
     | Interp.Error l msg -> (Nothing, Just (Internal_error msg))
@@ -137,20 +138,36 @@ let rec interp_to_value_helper arg thunk =
       match List.lookup i external_functions with
 	| Nothing -> (Nothing, Just (Internal_error ("External function not available " ^ i)))
 	| Just f  -> 
-          interp_to_value_helper arg (fun _ -> Interp.resume (make_mode true false) stack (Just (f value)))
+          interp_to_value_helper arg instr (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 "unsupported_instruction") _) -> (Nothing,Just (Unsupported_instruction_error instr))
 	| E_id (Id_aux (Id "no_matching_pattern") _) -> (Nothing,Just (Not_an_instruction_error arg))
       end 
     | _ -> (Nothing, Just (Internal_error "Memory or register requested in decode"))
 end
 
+let rec find_instruction i = function
+  | [] -> Nothing
+  | Skipped::instrs -> find_instruction i instrs
+  | ((Instruction_extractor.Instr_form name parms effects) as instr)::instrs ->
+      if i = name
+      then Just instr
+      else find_instruction i instrs
+end
+
+let migrate_typ = function
+  | Instruction_extractor.IBit -> Bit
+  | Instruction_extractor.IBitvector len -> Bvector len
+  | Instruction_extractor.IOther -> Other
+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 value
+  let (Interp.Env _ instructions _ _ _ _ _) = top_level in
+  let (instr_decoded,error) = interp_to_value_helper value ("",[],[])
     (fun _ -> Interp.resume 
       (make_mode true false) 
       (Interp.Thunk_frame 
@@ -158,8 +175,18 @@ let decode_to_istate top_level value =
 	 top_level Interp.eenv Interp.emem Interp.Top) Nothing) in
   match (instr_decoded,error) with
     | (Just instr, _) -> 
+      let instr_external = match instr with
+	| Interp.V_ctor (Id_aux (Id i) _) _ parm ->
+	  match (find_instruction i instructions) with
+	    | Just(Instruction_extractor.Instr_form name parms effects) -> 
+	      match (parm,parms) with
+		| (Interp.V_lit (L_aux L_unit _),[]) -> (name, [], effects)
+		| (value,[(p_name,ie_typ)]) -> (name, [(p_name,(migrate_typ ie_typ),fst(extern_value mode false value))], effects)
+		| (Interp.V_tuple vals,parms) -> 
+		  (name, (Interp.map2 (fun value (p_name,ie_typ) -> (p_name,(migrate_typ ie_typ),fst(extern_value mode false value))) vals parms), effects)
+          end end end in 
       let (arg,_) = Interp.to_exp mode Interp.eenv instr in
-      let (instr_decoded,error) = interp_to_value_helper value
+      let (instr_decoded,error) = interp_to_value_helper value instr_external
 	(fun _ -> Interp.resume 
 	 (make_mode true false) 
 	 (Interp.Thunk_frame 
@@ -168,7 +195,7 @@ let decode_to_istate top_level value =
       match (instr_decoded,error) with
 	| (Just instr,_) ->
 	  let (arg,_) = Interp.to_exp mode Interp.eenv instr in
-	  Instr ("",[],[])
+	  Instr instr_external
 	    (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)