Merge.

1 files changed, 23 insertions, 96 deletions

diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem
index 6edebc49..6febc709 100644
--- a/src/lem_interp/interp.lem
+++ b/src/lem_interp/interp.lem
@@ -5,14 +5,11 @@ import List_extra (* For 'nth' and 'head' where we know that they cannot fail *)
 open import String_extra (* for 'show' to convert nat to string) *)
 
 open import Interp_ast
+open import Interp_utilities
 
-type tannot = maybe (t * tag * list nec * effect)
+open import Instruction_extractor
 
-let get_exp_l (E_aux e (l,annot)) = l
-
-val pure : effect
-let pure = Effect_aux(Effect_set []) Unknown
-let unit_t = Typ_aux(Typ_app (Id_aux (Id "unit") Unknown) []) Unknown
+type tannot = Interp_utilities.tannot
 
 val intern_annot : tannot -> tannot
 let intern_annot annot =
@@ -24,38 +21,10 @@ let intern_annot annot =
 
 let val_annot typ = Just(typ,Tag_empty,[],pure)
 
-(* Workaround Lem's inability to scrap my (type classes) boilerplate.
- * Implementing only Eq, and only for literals - hopefully this will
- * be enough, but we should in principle implement ordering for everything in
- * Interp_ast *)
-
-val lit_eq: lit -> lit -> bool
-let lit_eq (L_aux left _) (L_aux right _) =
-   match (left, right) with
-   | (L_unit, L_unit) -> true
-   | (L_zero, L_zero) -> true
-   | (L_one, L_one) -> true
-   | (L_true, L_true) -> true
-   | (L_false, L_false) -> true
-   | (L_num n, L_num m) -> n = m
-   | (L_hex h, L_hex h') -> h = h'
-   | (L_bin b, L_bin b') -> b = b'
-   | (L_undef, L_undef) -> true
-   | (L_string s, L_string s') -> s = s'
-   | (_, _) -> false
-end
-
-instance (Eq lit)
-  let (=) = lit_eq
-  let (<>) n1 n2 = not (lit_eq n1 n2)
-end
-
 (* This is different from OCaml: it will drop elements from the longest list. *)
 let foldr2 f x l l' = List.foldr (Tuple.uncurry f) x (List.zip l l')
 let map2 f l l' = List.map (Tuple.uncurry f) (List.zip l l')
 
-let get_id id = match id with (Id_aux (Id s) _) -> s | (Id_aux (DeIid s) _ ) -> s end
-
 type reg_form =
  | Reg of id * tannot
  | SubReg of id * reg_form * index_range
@@ -76,12 +45,6 @@ type value =
  | V_register_alias of (alias_spec tannot) * tannot (* Same as above, but to a concatenation of two registers *)
  | V_track of value * (list reg_form) (* Used when memory system wants to track what register(s) a value came from *)
 
-let rec list_to_string format sep lst = match lst with 
-  | [] -> ""
-  | [last] -> format last
-  | one::rest -> (format one) ^ sep ^ (list_to_string format sep rest)
-end
-
 let rec string_of_value v = match v with
   | V_boxref nat t -> "$#" ^ (show nat) ^ "$"
   | V_lit (L_aux lit _) -> 
@@ -151,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)
@@ -228,36 +199,6 @@ let rec to_aliases (Defs defs) =
       end 
     end
 
-val has_rmem_effect : list base_effect -> bool
-val has_barr_effect : list base_effect -> bool
-val has_wmem_effect : list base_effect -> bool
-let rec has_effect which efcts =
-  match efcts with
-  | [] -> false
-  | (BE_aux e _)::efcts ->
-    match (which,e) with
-    | (BE_rreg,BE_rreg)    -> true 
-    | (BE_wreg,BE_wreg)    -> true 
-    | (BE_rmem,BE_rmem)    -> true 
-    | (BE_wmem,BE_wmem)    -> true 
-    | (BE_barr,BE_barr)    -> true 
-    | (BE_undef,BE_undef)  -> true 
-    | (BE_unspec,BE_unspec) -> true 
-    | (BE_nondet,BE_nondet) -> true 
-    | _ -> has_effect which efcts
-    end 
-  end
-let has_rmem_effect = has_effect BE_rmem
-let has_barr_effect = has_effect BE_barr
-let has_wmem_effect = has_effect BE_wmem
-
-let get_typ (TypSchm_aux (TypSchm_ts tq t) _) = t
-let get_effects (Typ_aux t _) =
-  match t with
-    | Typ_fn a r (Effect_aux (Effect_set eff) _) -> eff
-    | _ -> []
-  end
-
 val to_data_constructors : defs tannot -> list (id * typ)
 let rec to_data_constructors (Defs defs) =
   match defs with
@@ -760,23 +701,6 @@ let env_to_let mode (LEnv _ env) (E_aux e annot) =
 	           annot
 end
 
-val find_type_def : defs tannot -> id -> maybe (type_def tannot)
-val find_function : defs tannot -> id -> maybe (list (funcl tannot))
-
-let get_funcls id (FD_aux (FD_function _ _ _ fcls) _) =
-  List.filter (fun (FCL_aux (FCL_Funcl name pat exp) _) -> (get_id id) = (get_id name)) fcls
-
-let rec find_function (Defs defs) id =
-  match defs with 
-  | [] -> Nothing
-  | def::defs -> 
-    match def with
-    | DEF_fundef f -> match get_funcls id f with
-      | [] -> find_function (Defs defs) id
-      | funcs -> Just funcs end
-    | _ -> find_function (Defs defs) id
-    end end
-
 (* match_pattern returns a tuple of (pattern_matches? , pattern_passed_due_to_unknown?, env_of_pattern *)
 val match_pattern : pat tannot -> value -> bool * bool * lenv
 let rec match_pattern (P_aux p _) value_whole =
@@ -1068,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
@@ -1843,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
@@ -2154,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
@@ -2199,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
@@ -2214,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)