add type class instantiations (required as reg_name currently contains big_ints)

1 files changed, 98 insertions, 0 deletions

diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index 7c675c75..93194fe2 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -32,6 +32,15 @@ type value =
 | Unknown
 (*To add: an abstract value representing an unknown but named memory address?*)
 
+instance (Ord value)
+  let compare = defaultCompare
+  let (<) = defaultLess
+  let (<=) = defaultLessEq
+  let (>) = defaultGreater
+  let (>=) = defaultGreaterEq
+end
+
+
 type slice = (integer * integer)
 
 
@@ -53,6 +62,8 @@ accessed. The slice specifies where this field is in the register*)
 (* The first three components are as in Reg_field; the final slice
 specifies a part of the field, indexed w.r.t. the register as a whole *)
 
+
+(* because reg_name contains slice which currently contains Big_int.big_int, the default OCaml comparison is not sufficient and we need to define explicit type classes *)
 let reg_nameEqual r1 r2 = 
   match (r1,r2) with
   | (Reg s1, Reg s2) -> s1=s2
@@ -67,6 +78,32 @@ instance  (Eq reg_name)
   let (<>) x y = not (reg_nameEqual x y)
 end
 
+let reg_nameCompare r1 r2 = 
+  match (r1,r2) with
+  | (Reg s1, Reg s2) -> compare s1 s2
+  | (Reg_slice s1 sl1, Reg_slice s2 sl2) -> pairCompare compare compare (s1,sl1) (s2,sl2)
+  | (Reg_field s1 f1 sl1, Reg_field s2 f2 sl2) -> 
+      tripleCompare compare compare compare (s1,f1,sl1) (s2,f2,sl2)
+  | (Reg_f_slice s1 f1 sl1 sl1', Reg_f_slice s2 f2 sl2 sl2') -> 
+      pairCompare compare (tripleCompare compare compare compare) (s1,(f1,sl1,sl1')) (s2,(f2,sl2,sl2'))
+  | (Reg _, _)  -> LT
+  | (Reg_slice _ _, _) -> LT
+  | (Reg_field _ _ _, _) -> LT
+  | (_, _) -> GT
+  end
+
+instance (SetType reg_name)
+  let setElemCompare = reg_nameCompare
+end
+
+instance (Ord reg_name)
+  let compare = reg_nameCompare
+  let (<)  r1 r2 = (reg_nameCompare r1 r2) = LT
+  let (<=) r1 r2 = (reg_nameCompare r1 r2) <> GT
+  let (>)  r1 r2 = (reg_nameCompare r1 r2) = GT
+  let (>=) r1 r2 = (reg_nameCompare r1 r2) <> LT
+end
+
 
 
 type outcome =
@@ -100,6 +137,67 @@ type event =
 (*should there be a representation for escape down here?*)
 (*To discuss: Should multiple memory accesses be represented with a special form to denote this or potentially merged into one read or left in place*)
 
+
+
+(* more explicit type classes to work around the occurrences of big_int in reg_name *)
+instance (Ord read_kind)
+  let compare = defaultCompare
+  let (<) = defaultLess
+  let (<=) = defaultLessEq
+  let (>) = defaultGreater
+  let (>=) = defaultGreaterEq
+end
+instance (Ord write_kind)
+  let compare = defaultCompare
+  let (<) = defaultLess
+  let (<=) = defaultLessEq
+  let (>) = defaultGreater
+  let (>=) = defaultGreaterEq
+end
+instance (Ord barrier_kind)
+  let compare = defaultCompare
+  let (<) = defaultLess
+  let (<=) = defaultLessEq
+  let (>) = defaultGreater
+  let (>=) = defaultGreaterEq
+end
+
+(* maybe isn't a member of type Ord - this should be in the Lem standard library*)
+instance forall 'a. Ord 'a => (Ord (maybe 'a))
+  let compare = maybeCompare compare
+  let (<)  r1 r2 = (maybeCompare compare r1 r2) = LT
+  let (<=) r1 r2 = (maybeCompare compare r1 r2) <> GT
+  let (>)  r1 r2 = (maybeCompare compare r1 r2) = GT
+  let (>=) r1 r2 = (maybeCompare compare r1 r2) <> LT
+end
+
+
+let eventCompare e1 e2 = 
+  match (e1,e2) with
+  | (E_read_mem rk1 v1 i1 tr1, E_read_mem rk2 v2 i2 tr2) -> compare (rk1, (v1,i1,tr1)) (rk2,(v2, i2, tr2)) 
+  | (E_write_mem wk1 v1 i1 tr1 v1' tr1', E_write_mem wk2 v2 i2 tr2 v2' tr2') -> compare ((wk1,v1,i1),(tr1,v1',tr1'))  ((wk2,v2,i2),(tr2,v2',tr2')) 
+  | (E_barrier bk1, E_barrier bk2) -> compare bk1 bk2
+  | (E_read_reg r1, E_read_reg r2) -> compare r1 r2
+  | (E_write_reg r1 v1, E_write_reg r2 v2) -> compare (r1,v1) (r2,v2)
+  | (E_error s1, E_error s2) -> compare s1 s2
+  | (E_read_mem _ _ _ _, _) -> LT
+  | (E_write_mem _ _ _ _ _ _, _) -> LT
+  | (E_barrier _, _) -> LT
+  | (E_read_reg _, _) -> LT
+  | (E_write_reg _ _, _) -> LT
+  | _ -> GT
+  end
+
+
+
+
+
+instance (SetType event)
+  let setElemCompare = eventCompare
+end
+
+
+
 (* Functions to build up the initial state for interpretation *)
 val build_context : Interp_ast.defs Interp.tannot -> context (*defs should come from a .lem file generated by Sail*)
 val initial_instruction_state : context -> string -> list value -> instruction_state