Respect the identity of variables, Part 1

kore/package.yaml

@@ -50,6 +50,7 @@ dependencies:
   - data-default >=0.7
   - deepseq >=1.4
   - directory >=1.3
+  - distributive >=0.6
   - errors >=2.3
   - exceptions >=0.10
   - extra >=1.6
@@ -127,6 +128,7 @@ default-extensions:
   - TypeFamilies
   - TypeOperators
   - TypeSynonymInstances
+  - UndecidableInstances
   - ViewPatterns
 
 ghc-options:

kore/src/From.hs

@@ -8,6 +8,8 @@ module From
     ( From (..)
     ) where
 
+import Data.Void
+
 {- | Convert type @from@ into @to@.
 
 Valid instances are /total/. @from@ should be a homomorphism
@@ -40,3 +42,9 @@ let b = let a :: A = _ in from @_ @B a
  -}
 class From from to where
     from :: from -> to
+
+{- | This instance implements the principle /ex falso quodlibet/.
+ -}
+instance From Void any where
+    from = absurd
+    {-# INLINE from #-}

kore/src/Injection.hs

@@ -20,6 +20,7 @@ import Data.Dynamic
     , fromDynamic
     , toDyn
     )
+import Data.Void
 
 {- | The canonical injection or inclusion of @from ↪ into@.
 
@@ -80,3 +81,14 @@ instance Typeable a => Injection Dynamic a where
 
     retract = fromDynamic
     {-# INLINE retract #-}
+
+{- | 'Void' can be 'inject'ed into any type by the principle of /ex falso
+quodlibet/.  Because 'Void' contains no data, it can likewise be 'retract'ed
+from any type.
+ -}
+instance Injection a Void where
+    inject = \case {}
+    {-# INLINE inject #-}
+
+    retract = const Nothing
+    {-# INLINE retract #-}

kore/src/Kore/AST/AstWithLocation.hs

@@ -57,7 +57,7 @@ instance AstWithLocation Sort where
         locationFromAst sortActual
 
 instance AstWithLocation Variable where
-    locationFromAst = locationFromAst . variableName
+    locationFromAst Variable { variableName } = locationFromAst variableName
 
 instance
     AstWithLocation variable => AstWithLocation (ElementVariable variable)

kore/src/Kore/Attribute/Axiom.hs

@@ -86,10 +86,8 @@ import Kore.Internal.Symbol
     ( Symbol (..)
     , toSymbolOrAlias
     )
-import Kore.Syntax.ElementVariable
-import Kore.Syntax.SetVariable
-import Kore.Syntax.Variable
-    ( Variable (..)
+import Kore.Syntax.Variable hiding
+    ( Concrete
     )
 import qualified SQL
 
@@ -266,14 +264,15 @@ parseAxiomAttributes freeVariables (Attributes attrs) =
     Foldable.foldlM (flip $ parseAxiomAttribute freeVariables) Default.def attrs
 
 mapAxiomVariables
-    :: Ord variable2
-    => (ElementVariable variable1 -> ElementVariable variable2)
-    -> (SetVariable variable1 -> SetVariable variable2)
-    -> Axiom symbol variable1 -> Axiom symbol variable2
-mapAxiomVariables e s axiom@Axiom { concrete, symbolic } =
+    ::  (NamedVariable variable1, NamedVariable variable2)
+    =>  AdjSomeVariableName
+            (VariableNameOf variable1 -> VariableNameOf variable2)
+    ->  Axiom symbol variable1
+    ->  Axiom symbol variable2
+mapAxiomVariables adj axiom@Axiom { concrete, symbolic } =
     axiom
-        { concrete = mapConcreteVariables e s concrete
-        , symbolic = mapSymbolicVariables e s symbolic
+        { concrete = mapConcreteVariables adj concrete
+        , symbolic = mapSymbolicVariables adj symbolic
         }
 
 getPriorityOfAxiom

kore/src/Kore/Attribute/Axiom/Concrete.hs

@@ -35,14 +35,10 @@ import Kore.Attribute.Pattern.FreeVariables
 import qualified Kore.Attribute.Pattern.FreeVariables as FreeVariables
 import Kore.Debug
 import qualified Kore.Error
-import Kore.Syntax.ElementVariable
-import Kore.Syntax.SetVariable
-import Kore.Syntax.Variable
-    ( Variable
+import Kore.Syntax.Variable hiding
+    ( Concrete
     )
 import Kore.Variables.UnifiedVariable
-    ( UnifiedVariable
-    )
 
 {- | @Concrete@ represents the @concrete@ attribute for axioms.
  -}
@@ -133,12 +129,13 @@ instance From (Concrete Variable) Attributes where
         . unConcrete
 
 mapConcreteVariables
-    :: Ord variable2
-    => (ElementVariable variable1 -> ElementVariable variable2)
-    -> (SetVariable variable1 -> SetVariable variable2)
-    ->  Concrete variable1 -> Concrete variable2
-mapConcreteVariables mapElemVar mapSetVar (Concrete freeVariables) =
-    Concrete (mapFreeVariables mapElemVar mapSetVar freeVariables)
+    ::  (NamedVariable variable1, NamedVariable variable2)
+    =>  AdjSomeVariableName
+            (VariableNameOf variable1 -> VariableNameOf variable2)
+    ->  Concrete variable1
+    ->  Concrete variable2
+mapConcreteVariables adj (Concrete freeVariables) =
+    Concrete (mapFreeVariables adj freeVariables)
 
 isConcrete
     :: Ord variable => Concrete variable -> UnifiedVariable variable -> Bool

kore/src/Kore/Attribute/Axiom/Symbolic.hs

@@ -30,14 +30,8 @@ import Kore.Attribute.Pattern.FreeVariables
     )
 import qualified Kore.Attribute.Pattern.FreeVariables as FreeVariables
 import Kore.Debug
-import Kore.Syntax.ElementVariable
-import Kore.Syntax.SetVariable
 import Kore.Syntax.Variable
-    ( Variable
-    )
 import Kore.Variables.UnifiedVariable
-    ( UnifiedVariable
-    )
 
 {- | @Symbolic@ represents the @symbolic@ attribute for axioms.
  -}
@@ -97,12 +91,13 @@ instance From (Symbolic Variable) Attributes where
         . unSymbolic
 
 mapSymbolicVariables
-    :: Ord variable2
-    => (ElementVariable variable1 -> ElementVariable variable2)
-    -> (SetVariable variable1 -> SetVariable variable2)
-    ->  Symbolic variable1 -> Symbolic variable2
-mapSymbolicVariables mapElemVar mapSetVar (Symbolic freeVariables) =
-    Symbolic (mapFreeVariables mapElemVar mapSetVar freeVariables)
+    ::  (NamedVariable variable1, NamedVariable variable2)
+    =>  AdjSomeVariableName
+            (VariableNameOf variable1 -> VariableNameOf variable2)
+    ->  Symbolic variable1
+    ->  Symbolic variable2
+mapSymbolicVariables adj (Symbolic freeVariables) =
+    Symbolic (mapFreeVariables adj freeVariables)
 
 isSymbolic
     :: Ord variable => Symbolic variable -> UnifiedVariable variable -> Bool

kore/src/Kore/Attribute/Pattern.hs

@@ -63,11 +63,8 @@ import qualified Kore.Internal.SideCondition.SideCondition as SideCondition
 import Kore.Sort
     ( Sort
     )
+import Kore.Syntax.Variable
 import Kore.Variables.UnifiedVariable
-    ( ElementVariable
-    , SetVariable
-    , UnifiedVariable (..)
-    )
 
 {- | @Pattern@ are the attributes of a pattern collected during verification.
  -}
@@ -176,28 +173,30 @@ See also: 'traverseVariables'
 
  -}
 mapVariables
-    :: Ord variable2
-    => (ElementVariable variable1 -> ElementVariable variable2)
-    -> (SetVariable variable1 -> SetVariable variable2)
-    -> Pattern variable1 -> Pattern variable2
-mapVariables mapElemVar mapSetVar =
+    ::  (NamedVariable variable1, NamedVariable variable2)
+    =>  AdjSomeVariableName
+            (VariableNameOf variable1 -> VariableNameOf variable2)
+    ->  Pattern variable1
+    ->  Pattern variable2
+mapVariables adj =
     Lens.over (field @"freeVariables")
-        (mapFreeVariables mapElemVar mapSetVar)
+        (mapFreeVariables adj)
 
 {- | Use the provided traversal to replace the free variables in a 'Pattern'.
 
 See also: 'mapVariables'
 
  -}
 traverseVariables
-    ::  forall m variable1 variable2.
-        (Monad m, Ord variable2)
-    => (ElementVariable variable1 -> m (ElementVariable variable2))
-    -> (SetVariable variable1 -> m (SetVariable variable2))
-    -> Pattern variable1
-    -> m (Pattern variable2)
-traverseVariables trElemVar trSetVar =
-    field @"freeVariables" (traverseFreeVariables trElemVar trSetVar)
+    ::  forall m variable1 variable2
+    .   Monad m
+    =>  (NamedVariable variable1, NamedVariable variable2)
+    =>  AdjSomeVariableName
+            (VariableNameOf variable1 -> m (VariableNameOf variable2))
+    ->  Pattern variable1
+    ->  m (Pattern variable2)
+traverseVariables adj =
+    field @"freeVariables" (traverseFreeVariables adj)
 
 {- | Delete the given variable from the set of free variables.
  -}

kore/src/Kore/Attribute/Pattern/FreeVariables.hs

@@ -28,14 +28,13 @@ import Data.Set
     ( Set
     )
 import qualified Data.Set as Set
-import qualified Data.Traversable as Traversable
 import qualified Generics.SOP as SOP
 import qualified GHC.Generics as GHC
 
 import Kore.Attribute.Synthetic
 import Kore.Debug
 import Kore.Syntax.ElementVariable
-import Kore.Syntax.SetVariable
+import Kore.Syntax.Variable
 import Kore.Variables.UnifiedVariable
 
 newtype FreeVariables variable =
@@ -75,6 +74,10 @@ toList :: FreeVariables variable -> [UnifiedVariable variable]
 toList = Set.toList . getFreeVariables
 {-# INLINE toList #-}
 
+fromList :: Ord variable => [UnifiedVariable variable] -> FreeVariables variable
+fromList = foldMap freeVariable
+{-# INLINE fromList #-}
+
 toSet :: FreeVariables variable -> Set (UnifiedVariable variable)
 toSet = getFreeVariables
 {-# INLINE toSet #-}
@@ -114,24 +117,21 @@ freeVariable variable = FreeVariables (Set.singleton variable)
 {-# INLINE freeVariable #-}
 
 mapFreeVariables
-    :: Ord variable2
-    => (ElementVariable variable1 -> ElementVariable variable2)
-    -> (SetVariable variable1 -> SetVariable variable2)
-    -> FreeVariables variable1 -> FreeVariables variable2
-mapFreeVariables mapElemVar mapSetVar (FreeVariables freeVars) =
-    FreeVariables (Set.map (mapUnifiedVariable mapElemVar mapSetVar) freeVars)
+    ::  (NamedVariable variable1, NamedVariable variable2)
+    =>  AdjSomeVariableName
+            (VariableNameOf variable1 -> VariableNameOf variable2)
+    ->  FreeVariables variable1 -> FreeVariables variable2
+mapFreeVariables adj = fromList . map (mapUnifiedVariable adj) . toList
 {-# INLINE mapFreeVariables #-}
 
 traverseFreeVariables
-    :: (Applicative f, Ord variable2)
-    => (ElementVariable variable1 -> f (ElementVariable variable2))
-    -> (SetVariable variable1 -> f (SetVariable variable2))
-    -> FreeVariables variable1 -> f (FreeVariables variable2)
-traverseFreeVariables traverseElemVar traverseSetVar (FreeVariables freeVars) =
-    FreeVariables . Set.fromList
-    <$> Traversable.traverse traversal (Set.toList freeVars)
-  where
-    traversal = traverseUnifiedVariable traverseElemVar traverseSetVar
+    ::  Applicative f
+    =>  (NamedVariable variable1, NamedVariable variable2)
+    =>  AdjSomeVariableName
+            (VariableNameOf variable1 -> f (VariableNameOf variable2))
+    ->  FreeVariables variable1 -> f (FreeVariables variable2)
+traverseFreeVariables adj =
+    fmap fromList . traverse (traverseUnifiedVariable adj) . toList
 {-# INLINE traverseFreeVariables #-}
 
 {- | Extracts the list of free element variables

kore/src/Kore/Builtin/AssociativeCommutative.hs

@@ -99,6 +99,7 @@ import Kore.Internal.TermLike
     , Concrete
     , pattern ElemVar_
     , InternalVariable
+    , NamedVariable
     , TermLike
     , mkApplySymbol
     , mkBuiltin
@@ -158,7 +159,7 @@ class
     @
     -}
     toNormalized
-        :: Ord variable
+        :: NamedVariable variable
         => TermLike variable
         -> NormalizedOrBottom normalized variable
 
@@ -355,7 +356,7 @@ deriving instance
 {- | The semigroup defined by the `concat` operation.
 -}
 instance
-    (Ord variable, TermWrapper normalized)
+    (NamedVariable variable, TermWrapper normalized)
     => Semigroup (NormalizedOrBottom normalized variable)
   where
     Bottom <> _ = Bottom
@@ -365,7 +366,7 @@ instance
 
 concatNormalized
     :: forall normalized variable
-    .  (TermWrapper normalized, Ord variable)
+    .  (TermWrapper normalized, NamedVariable variable)
     => normalized (TermLike Concrete) (TermLike variable)
     -> normalized (TermLike Concrete) (TermLike variable)
     -> Maybe (normalized (TermLike Concrete) (TermLike variable))
@@ -406,7 +407,7 @@ internal representations themselves; this "flattening" step also recurses to
 
  -}
 renormalize
-    :: (TermWrapper normalized, Ord variable)
+    :: (TermWrapper normalized, NamedVariable variable)
     => normalized (TermLike Concrete) (TermLike variable)
     -> Maybe (normalized (TermLike Concrete) (TermLike variable))
 renormalize = normalizeAbstractElements >=> flattenOpaque
@@ -457,7 +458,7 @@ Return 'Nothing' if there are any duplicate (concrete or abstract) keys.
 
  -}
 normalizeAbstractElements
-    :: (TermWrapper normalized, Ord variable)
+    :: (TermWrapper normalized, NamedVariable variable)
     => normalized (TermLike Concrete) (TermLike variable)
     -> Maybe (normalized (TermLike Concrete) (TermLike variable))
 normalizeAbstractElements (Domain.unwrapAc -> normalized) = do
@@ -478,7 +479,7 @@ normalizeAbstractElements (Domain.unwrapAc -> normalized) = do
 -- remains abstract.
 extractConcreteElement
     ::  Domain.AcWrapper collection
-    =>  Ord variable
+    =>  NamedVariable variable
     =>  Domain.Element collection (TermLike variable)
     ->  Either
             (TermLike Concrete, Domain.Value collection (TermLike variable))
@@ -494,7 +495,7 @@ extractConcreteElement element =
 
  -}
 flattenOpaque
-    :: (TermWrapper normalized, Ord variable)
+    :: (TermWrapper normalized, NamedVariable variable)
     => normalized (TermLike Concrete) (TermLike variable)
     -> Maybe (normalized (TermLike Concrete) (TermLike variable))
 flattenOpaque (Domain.unwrapAc -> normalized) = do
@@ -509,7 +510,7 @@ flattenOpaque (Domain.unwrapAc -> normalized) = do
 {- | The monoid defined by the `concat` and `unit` operations.
 -}
 instance
-    (Ord variable, TermWrapper normalized)
+    (NamedVariable variable, TermWrapper normalized)
     => Monoid (NormalizedOrBottom normalized variable)
   where
     mempty = Normalized $ Domain.wrapAc Domain.emptyNormalizedAc
@@ -680,7 +681,7 @@ disjointMap input =
 
 splitVariableConcrete
     :: forall variable a
-    .  Ord variable
+    .  NamedVariable variable
     =>  [(TermLike variable, a)]
     -> ([(TermLike variable, a)], [(TermLike Concrete, a)])
 splitVariableConcrete terms =

kore/src/Kore/Builtin/Builtin.hs

@@ -463,7 +463,9 @@ If the pattern is not concrete and normalized, the function is
 See also: 'Kore.Proof.Value.Value'
 
  -}
-toKey :: Ord variable => TermLike variable -> Maybe (TermLike Concrete)
+toKey
+    :: NamedVariable variable
+    => TermLike variable -> Maybe (TermLike Concrete)
 toKey purePattern = do
     p <- TermLike.asConcrete purePattern
     -- TODO (thomas.tuegel): Use the return value as the term.