make string functions used to UI and debugging output empty strings for theorem provers, use structural (in)equality for Isabelle and HOL for literals and values

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))