diff options
Diffstat (limited to 'src/lem_interp/interp.lem')
| -rw-r--r-- | src/lem_interp/interp.lem | 90 |
1 files changed, 2 insertions, 88 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem index 6edebc49..a436d652 100644 --- a/src/lem_interp/interp.lem +++ b/src/lem_interp/interp.lem @@ -5,14 +5,9 @@ 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) - -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 +19,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 +43,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 _) -> @@ -228,36 +189,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 +691,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 = |