1 files changed, 93 insertions, 0 deletions
diff --git a/src/lem_interp/interp_utilities.lem b/src/lem_interp/interp_utilities.lem
new file mode 100644
index 00000000..37ed814d
--- /dev/null
+++ b/src/lem_interp/interp_utilities.lem
@@ -0,0 +1,93 @@
+open import Interp_ast
+open import Pervasives
+
+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
+
+(* 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
+
+let get_id id = match id with (Id_aux (Id s) _) -> s | (Id_aux (DeIid s) _ ) -> s end
+
+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 
+
+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 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
+
+