diff options
| -rw-r--r-- | src/lem_interp/interp.lem | 14 | ||||
| -rw-r--r-- | src/lem_interp/interp_utilities.lem | 20 |
2 files changed, 23 insertions, 11 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem index b61f724a..2ac078ba 100644 --- a/src/lem_interp/interp.lem +++ b/src/lem_interp/interp.lem @@ -58,7 +58,7 @@ 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 string_of_value v = match v with +let rec {ocaml} string_of_value v = match v with | V_boxref nat t -> "$#" ^ (show nat) ^ "$" | V_lit (L_aux lit _) -> (match lit with @@ -97,8 +97,9 @@ let rec string_of_value v = match v with | V_register_alias _ _ -> "register_as_alias" | V_track v _ -> "tainted " ^ (string_of_value v) end +let ~{ocaml} string_of_value _ = "" -let rec id_value_eq (i, v) (i', v') = i = i' && value_eq v v' +let rec {coq;ocaml} id_value_eq (i, v) (i', v') = i = i' && value_eq v v' and value_eq left right = (* XXX it is not clear whether t = t' will work in all cases *) match (left, right) with @@ -122,10 +123,15 @@ and value_eq left right = | (v,V_track v2 _) -> value_eq v v2 | (_, _) -> false end +let {isabelle;hol} id_value_eq = unsafe_structural_equality +let {isabelle;hol} value_eq = unsafe_structural_equality + +let {coq;ocaml} value_ineq n1 n2 = not (value_eq n1 n2) +let {isabelle;hol} value_ineq = unsafe_structural_inequality instance (Eq value) - let (=) = value_eq - let (<>) n1 n2 = not (value_eq n1 n2) + let (=) = value_eq + let (<>) = value_ineq end let reg_start_pos reg = diff --git a/src/lem_interp/interp_utilities.lem b/src/lem_interp/interp_utilities.lem index 7a667478..e80a2323 100644 --- a/src/lem_interp/interp_utilities.lem +++ b/src/lem_interp/interp_utilities.lem @@ -20,7 +20,7 @@ let unit_t = Typ_aux(Typ_app (Id_aux (Id "unit") Unknown) []) Unknown * Interp_ast *) val lit_eq: lit -> lit -> bool -let lit_eq (L_aux left _) (L_aux right _) = +let {ocaml;coq} lit_eq (L_aux left _) (L_aux right _) = match (left, right) with | (L_zero, L_zero) -> true | (L_one, L_one) -> true @@ -38,19 +38,24 @@ let lit_eq (L_aux left _) (L_aux right _) = | (L_string s, L_string s') -> s = s' | (_, _) -> false end +let {isabelle;hol} lit_eq = unsafe_structural_equality + +let {ocaml;coq} lit_ineq n1 n2 = not (lit_eq n1 n2) +let {isabelle;hol} lit_ineq = unsafe_structural_inequality instance (Eq lit) - let (=) = lit_eq - let (<>) n1 n2 = not (lit_eq n1 n2) + let (=) = lit_eq + let (<>) = lit_ineq 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 +let rec {ocaml} list_to_string format sep lst = match lst with | [] -> "" | [last] -> format last | one::rest -> (format one) ^ sep ^ (list_to_string format sep rest) -end +end +let ~{ocaml} list_to_string format sep list = "" val has_rmem_effect : list base_effect -> bool val has_barr_effect : list base_effect -> bool @@ -85,7 +90,7 @@ let get_effects (Typ_aux t _) = | _ -> [] end -let string_of_tag tag = match tag with +let {ocaml} string_of_tag tag = match tag with | Tag_empty -> "empty" | Tag_global -> "global" | Tag_ctor -> "ctor" @@ -95,7 +100,8 @@ let string_of_tag tag = match tag with | Tag_spec -> "spec" | Tag_enum i -> "enum" | Tag_alias -> "alias" -end +end +let ~{ocaml} string_of_tag tag = "" val find_type_def : defs tannot -> id -> maybe (type_def tannot) val find_function : defs tannot -> id -> maybe (list (funcl tannot)) |