From c34462722ec2b17353784cd4e7caa42ac5dddf04 Mon Sep 17 00:00:00 2001
From: Kathy Gray
Date: Wed, 19 Nov 2014 14:06:00 +0000
Subject: add value compare functions

---
 src/lem_interp/interp_interface.lem | 21 ++++++++++++++++++++-
 1 file changed, 20 insertions(+), 1 deletion(-)

(limited to 'src/lem_interp')

diff --git a/src/lem_interp/interp_interface.lem b/src/lem_interp/interp_interface.lem
index 5c77e807..91ef3d7f 100644
--- a/src/lem_interp/interp_interface.lem
+++ b/src/lem_interp/interp_interface.lem
@@ -32,7 +32,7 @@ type value =
 | Unknown
 (*To add: an abstract value representing an unknown but named memory address?*)
 
-instance (Ord value)
+instance (Ord bool)
   let compare = defaultCompare
   let (<) = defaultLess
   let (<=) = defaultLessEq
@@ -40,6 +40,25 @@ instance (Ord value)
   let (>=) = defaultGreaterEq
 end
 
+let valueCompare v1 v2 = 
+  match (v1,v2) with
+  | (Bitvector bits1 inc1 start1, Bitvector bits2 inc2 start2) ->
+    tripleCompare compare compare compare (bits1,inc1,start1) (bits2,inc2,start2)
+  | (Bytevector words1, Bytevector words2) -> compare words1 words2
+  | (Unknown,Unknown) -> EQ
+  | (Bitvector _ _ _, _)  -> LT
+  | (Bytevector _, _) -> LT
+  | (_, _) -> GT
+  end
+
+instance (Ord value)
+  let compare = valueCompare
+  let (<) v1 v2 = (valueCompare v1 v2) = LT
+  let (<=) v1 v2 = (valueCompare v1 v2) <> GT
+  let (>) v1 v2 = (valueCompare v1 v2) = GT
+  let (>=) v1 v2 = (valueCompare v1 v2) <> LT
+end
+
 
 type slice = (integer * integer)
 
-- 
cgit v1.2.3