From 606c2f97e45abe5da02aa6d678a59aac64f92031 Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Tue, 4 Dec 2018 15:12:21 -0800
Subject: [PATCH] Translate Cryptol (==) using the class dictionary, avoiding
 `Prelude.eq`.

NOTE: The cryptol simpset avoids unfolding the definition of `ecEq`,
to make it easier to recognize equational theorems as such.
The axiom `ecEq_refl` can be used to rewrite goals involving `ecEq`.
---
 saw/Cryptol.sawcore                 | 4 +++-
 src/Verifier/SAW/Cryptol/Simpset.hs | 1 +
 2 files changed, 4 insertions(+), 1 deletion(-)

diff --git a/saw/Cryptol.sawcore b/saw/Cryptol.sawcore
index fdae15c018..14f9baff40 100644
--- a/saw/Cryptol.sawcore
+++ b/saw/Cryptol.sawcore
@@ -970,7 +970,7 @@ ecSLt : (a : sort 0) -> PSignedCmp a -> a -> a -> Bool;
 ecSLt a pa x y = pa.scmp x y False;
 
 ecEq : (a : sort 0) -> PCmp a -> a -> a -> Bool;
-ecEq a _ = eq a;
+ecEq a pa = pa.eq;
 
 ecNotEq : (a : sort 0) -> PCmp a -> a -> a -> Bool;
 ecNotEq a pa x y = not (ecEq a pa x y);
@@ -1363,6 +1363,8 @@ ecSle =
 --------------------------------------------------------------------------------
 -- Rewrite rules
 
+axiom ecEq_refl : (a : sort 0) -> (pa : PCmp a) -> (x : a) -> Eq Bool (ecEq a pa x x) True;
+
 axiom replicate_False : (n : Nat) -> Eq (bitvector n) (replicate n Bool False) (bvNat n 0);
 
 axiom subNat_0 : (n : Nat) -> Eq Nat (subNat n 0) n;
diff --git a/src/Verifier/SAW/Cryptol/Simpset.hs b/src/Verifier/SAW/Cryptol/Simpset.hs
index 3ddb025c89..4757975cff 100644
--- a/src/Verifier/SAW/Cryptol/Simpset.hs
+++ b/src/Verifier/SAW/Cryptol/Simpset.hs
@@ -47,4 +47,5 @@ excludedNames =
   , "PLiteral"
   , "PLogic"
   , "PSignedCmp"
+  , "ecEq"
   ]