summaryrefslogtreecommitdiff
path: root/src/lem_interp/interp.lem
diff options
context:
space:
mode:
Diffstat (limited to 'src/lem_interp/interp.lem')
-rw-r--r--src/lem_interp/interp.lem119
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)
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 09:54:08 +0000