From 25049d9781ab4fa908c360f265929613a826a1d5 Mon Sep 17 00:00:00 2001
From: Thomas Tuegel <thomas.tuegel@runtimeverification.com>
Date: Thu, 13 Feb 2020 12:46:43 -0600
Subject: [PATCH 1/3] Variable: Eq, Ord, and Hashable ignore Sort

In domain-driven design terminology, Variable is an entity type: two variables
with the same name (variableName and variableCounter) but different sorts are
not different, as much as they are inconsistent.
---
 kore/src/Kore/Syntax/Variable.hs | 28 ++++++++++++++++++++++++++--
 1 file changed, 26 insertions(+), 2 deletions(-)

diff --git a/kore/src/Kore/Syntax/Variable.hs b/kore/src/Kore/Syntax/Variable.hs
index d5ff59fa61..4cc94ab856 100644
--- a/kore/src/Kore/Syntax/Variable.hs
+++ b/kore/src/Kore/Syntax/Variable.hs
@@ -56,9 +56,33 @@ data Variable = Variable
     , variableCounter :: !(Maybe (Sup Natural))
     , variableSort :: !Sort
     }
-    deriving (Eq, GHC.Generic, Ord, Show)
+    deriving (GHC.Generic, Show)
 
-instance Hashable Variable
+-- TODO (thomas.tuegel): Move variableSort out of Variable entirely, so that
+-- only the identifiers remain.
+
+instance Eq Variable where
+    (==) a b =
+            on (==) variableName a b
+        &&  on (==) variableCounter a b
+    {-# INLINE (==) #-}
+
+{- | 'Variable' is uniquely identified by 'variableName' and 'variableCounter'.
+
+Two 'Variable's with the same 'variableName' and 'variableCounter' but different
+'variableSort's are not different so much as they are /inconsistent/.
+
+ -}
+instance Ord Variable where
+    compare a b =
+            on compare variableName a b
+        <>  on compare variableCounter a b
+    {-# INLINE compare #-}
+
+instance Hashable Variable where
+    hashWithSalt salt Variable { variableName, variableCounter } =
+        salt `hashWithSalt` variableName `hashWithSalt` variableCounter
+    {-# INLINE hashWithSalt #-}
 
 instance NFData Variable
 

From 15b2b74f48cf993f08511631c1f7626cfdfaa281 Mon Sep 17 00:00:00 2001
From: Thomas Tuegel <thomas.tuegel@runtimeverification.com>
Date: Thu, 13 Feb 2020 12:47:47 -0600
Subject: [PATCH 2/3] unsafeWrap: HasCallStack

HasCallStack adds call stack information to the assertions, which is important
for diagnosing test failures.
---
 kore/src/Kore/Internal/Substitution.hs | 15 ++++++++-------
 1 file changed, 8 insertions(+), 7 deletions(-)

diff --git a/kore/src/Kore/Internal/Substitution.hs b/kore/src/Kore/Internal/Substitution.hs
index 311d9b34c2..fc52368c0b 100644
--- a/kore/src/Kore/Internal/Substitution.hs
+++ b/kore/src/Kore/Internal/Substitution.hs
@@ -314,24 +314,25 @@ wrap xs = Substitution xs
 -- | Wrap the list of substitutions to a normalized substitution. Do not use
 -- this unless you are sure you need it.
 unsafeWrap
-    :: Ord variable
+    :: HasCallStack
+    => Ord variable
     => [(UnifiedVariable variable, TermLike variable)]
     -> Substitution variable
 unsafeWrap =
     NormalizedSubstitution . List.foldl' insertNormalized Map.empty
   where
     insertNormalized subst (var, termLike) =
+        Map.insert var termLike subst
         -- The variable must not occur in the substitution
-        assert (Map.notMember var subst)
+        & assert (Map.notMember var subst)
         -- or in the right-hand side of this or any other substitution,
-        $ assert (not $ occurs termLike)
-        $ assert (not $ any occurs subst)
+        & assert (not $ occurs termLike)
+        & assert (not $ any occurs subst)
         -- this substitution must not depend on any substitution variable,
-        $ assert (not $ any depends $ Map.keys subst)
+        & assert (not $ any depends $ Map.keys subst)
         -- and if this is an element variable substitution, the substitution
         -- must be defined.
-        $ assert (not $ isElemVar var && isBottom termLike)
-        $ Map.insert var termLike subst
+        & assert (not $ isElemVar var && isBottom termLike)
       where
         occurs = TermLike.hasFreeVariable var
         depends var' = TermLike.hasFreeVariable var' termLike

From bd3c7353ed0dd0641a62781638b35d0e5cb8a8d0 Mon Sep 17 00:00:00 2001
From: Thomas Tuegel <thomas.tuegel@runtimeverification.com>
Date: Thu, 13 Feb 2020 12:48:11 -0600
Subject: [PATCH 3/3] test_matcherVariableFunction: Fix inconsistent variable
 naming

The variables x and xSub were given the same name, but different sorts.
---
 kore/test/Test/Kore/Step/Axiom/Matcher.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/kore/test/Test/Kore/Step/Axiom/Matcher.hs b/kore/test/Test/Kore/Step/Axiom/Matcher.hs
index af8ed3fbcf..76f93cdea3 100644
--- a/kore/test/Test/Kore/Step/Axiom/Matcher.hs
+++ b/kore/test/Test/Kore/Step/Axiom/Matcher.hs
@@ -384,7 +384,7 @@ test_matcherVariableFunction =
     ]
   where
     aSubSub = Mock.functional00SubSubSort
-    xSub = ElementVariable $ Variable (testId "x") mempty Mock.subSort
+    xSub = ElementVariable $ Variable (testId "xSub") mempty Mock.subSort
 
 test_matcherNonVarToPattern :: [TestTree]
 test_matcherNonVarToPattern =