Factor class VariableName out of SortedVariable

kore/src/Kore/Attribute/Pattern.hs

@@ -89,6 +89,9 @@ data Pattern variable =
         }
     deriving (Eq, GHC.Generic, Show)
 
+-- TODO (thomas.tuegel): Lift 'simplified' to the 'Conditional' level once we
+-- treat the latter as an aggregate root.
+
 instance NFData variable => NFData (Pattern variable)
 
 instance Hashable variable => Hashable (Pattern variable)

kore/src/Kore/Internal/SideCondition.hs

@@ -36,23 +36,21 @@ import qualified Kore.Internal.Condition as Condition
 import Kore.Internal.Predicate
     ( Predicate
     )
-import qualified Kore.Internal.SideCondition.SideCondition as SideCondition.Representation
-    ( fromText
-    )
 import qualified Kore.Internal.SideCondition.SideCondition as SideCondition
     ( Representation
     )
 import Kore.Internal.Variable
     ( ElementVariable
     , InternalVariable
     , SetVariable
+    , Variable
+    , toVariable
     )
 import Kore.TopBottom
     ( TopBottom (..)
     )
 import Kore.Unparser
     ( Unparse (..)
-    , unparseToText
     )
 import qualified Pretty
 import qualified SQL
@@ -175,4 +173,5 @@ toRepresentationCondition
     => Condition variable
     -> SideCondition.Representation
 toRepresentationCondition condition =
-    SideCondition.Representation.fromText $ unparseToText condition
+    from @(Condition Variable)
+    $ Condition.mapVariables (fmap toVariable) (fmap toVariable) condition

kore/src/Kore/Internal/SideCondition/SideCondition.hs

@@ -5,49 +5,80 @@ License     : NCSA
 
 module Kore.Internal.SideCondition.SideCondition
     ( Representation
-    , fromText
     ) where
 
 import Prelude.Kore
 
 import Control.DeepSeq
-    ( NFData
+    ( NFData (..)
     )
 import Data.Hashable
-    ( Hashable
+    ( Hashable (..)
     , Hashed
     , hashed
     )
-import Data.Text
-    ( Text
-    )
-import qualified Generics.SOP as SOP
-    ( Generic
-    , HasDatatypeInfo
-    )
-import qualified GHC.Generics as GHC
 
+import Data.Type.Equality
+    ( (:~:) (..)
+    , testEquality
+    )
 import Kore.Debug
-    ( Debug
+    ( Debug (..)
     , Diff (..)
     )
+import Type.Reflection
+    ( SomeTypeRep (..)
+    , TypeRep
+    , Typeable
+    , typeRep
+    )
+
+data Representation where
+    Representation :: Ord a => !(TypeRep a) -> !(Hashed a) -> Representation
+
+instance Eq Representation where
+    (==) (Representation typeRep1 hashed1) (Representation typeRep2 hashed2) =
+        case testEquality typeRep1 typeRep2 of
+            Nothing -> False
+            Just Refl -> hashed1 == hashed2
+    {-# INLINE (==) #-}
+
+instance Ord Representation where
+    compare
+        (Representation typeRep1 hashed1)
+        (Representation typeRep2 hashed2)
+      =
+        case testEquality typeRep1 typeRep2 of
+            Nothing -> compare (SomeTypeRep typeRep1) (SomeTypeRep typeRep2)
+            Just Refl -> compare hashed1 hashed2
+    {-# INLINE compare #-}
 
-newtype Representation =
-    Representation
-        { getRepresentation :: Hashed Text
-        }
-    deriving (Eq, GHC.Generic, Hashable, NFData, Ord, Show)
+instance Show Representation where
+    showsPrec prec (Representation typeRep1 _) =
+        showParen (prec >= 10)
+        $ showString "Representation " . shows typeRep1 . showString " _"
+    {-# INLINE showsPrec #-}
 
-instance SOP.Generic Representation
+instance Hashable Representation where
+    hashWithSalt salt (Representation typeRep1 hashed1) =
+        salt `hashWithSalt` typeRep1 `hashWithSalt` hashed1
+    {-# INLINE hashWithSalt #-}
 
-instance SOP.HasDatatypeInfo Representation
+instance NFData Representation where
+    rnf (Representation typeRep1 hashed1) = typeRep1 `seq` hashed1 `seq` ()
+    {-# INLINE rnf #-}
 
-instance Debug Representation
+mkRepresentation :: (Ord a, Hashable a, Typeable a) => a -> Representation
+mkRepresentation = Representation typeRep . hashed
 
-instance Diff Representation
+instance Debug Representation where
+    debugPrec _ _ = "_"
+    {-# INLINE debugPrec #-}
 
-instance From Text Representation where
-    from = Representation . hashed
+instance Diff Representation where
+    diffPrec _ _ = Nothing
+    {-# INLINE diffPrec #-}
 
-fromText :: Text -> Representation
-fromText = from
+instance (Ord a, Hashable a, Typeable a) => From a Representation where
+    from = mkRepresentation
+    {-# INLINE from #-}

kore/src/Kore/Internal/Variable.hs

@@ -81,5 +81,5 @@ these constraints.
 type InternalVariable variable =
     ( Ord variable, SubstitutionOrd variable
     , Debug variable, Show variable, Unparse variable
-    , SortedVariable variable, FreshVariable variable
+    , VariableName variable, SortedVariable variable, FreshVariable variable
     )

kore/src/Kore/Step/EquationalStep.hs

@@ -385,9 +385,7 @@ applyRulesSequence sideCondition initial rules =
     matchRules sideCondition initial rules'
     >>= finalizeRulesSequence sideCondition initial
   where
-    -- TODO (thomas.tuegel): Include freeVariables sideCondition
-    avoidConfigVars = freeVariables initial
-    rules' = EqualityPattern.targetRuleVariables avoidConfigVars <$> rules
+    rules' = EqualityPattern.targetRuleVariables sideCondition initial <$> rules
 
 -- | Matches a list a rules against a configuration. See 'matchRule'.
 matchRules

kore/src/Kore/Step/RewriteStep.hs

@@ -251,8 +251,7 @@ applyRulesWithFinalizer
     -> unifier (Results RulePattern variable)
 applyRulesWithFinalizer finalize unificationProcedure rules initial = do
     let sideCondition = SideCondition.topTODO
-        configurationVariables = freeVariables initial
-        rules' = targetRuleVariables configurationVariables <$> rules
+        rules' = targetRuleVariables sideCondition initial <$> rules
     results <- unifyRules unificationProcedure sideCondition initial rules'
     debugAppliedRewriteRules initial results
     finalize initial results

kore/src/Kore/Step/Simplification/ExpandAlias.hs

@@ -33,7 +33,7 @@ import Kore.Internal.TermLike
     , substitute
     )
 import Kore.Syntax.Variable
-    ( SortedVariable (..)
+    ( fromVariable
     )
 import Kore.Unification.Unify
     ( MonadUnify

kore/src/Kore/Step/Step.hs

@@ -48,6 +48,7 @@ import qualified Data.Text.Prettyprint.Doc as Pretty
 import qualified Branch
 import Kore.Attribute.Pattern.FreeVariables
     ( FreeVariables (..)
+    , HasFreeVariables (freeVariables)
     )
 import qualified Kore.Attribute.Pattern.FreeVariables as FreeVariables
 import Kore.Internal.Condition
@@ -257,13 +258,16 @@ The rule's variables are:
 targetRuleVariables
     :: InternalVariable variable
     => UnifyingRule rule
-    => FreeVariables (Target variable)
+    => SideCondition (Target variable)
+    -> Pattern (Target variable)
     -> rule variable
     -> rule (Target variable)
-targetRuleVariables avoiding =
+targetRuleVariables sideCondition initial =
     snd
     . refreshRule avoiding
     . mapRuleVariables Target.mkElementTarget Target.mkSetTarget
+  where
+    avoiding = freeVariables sideCondition <> freeVariables initial
 
 {- | Unwrap the variables in a 'RulePattern'. Inverse of 'targetRuleVariables'.
  -}

kore/src/Kore/Syntax/Variable.hs

@@ -13,6 +13,9 @@ module Kore.Syntax.Variable
     , isOriginalVariable
     , illegalVariableCounter
     , externalizeFreshVariable
+    , VariableName
+    , toVariable
+    , fromVariable
     , SortedVariable (..)
     , unparse2SortedVariable
     , Concrete
@@ -78,6 +81,12 @@ instance Unparse Variable where
         unparse2 variableName
         <> Pretty.pretty variableCounter
 
+instance From Variable Variable where
+    from = id
+    {-# INLINE from #-}
+
+instance VariableName Variable
+
 {- | Is the variable original (as opposed to generated)?
  -}
 isOriginalVariable :: Variable -> Bool
@@ -112,37 +121,41 @@ externalizeFreshVariable variable@Variable { variableName, variableCounter } =
             , idLocation = AstLocationGeneratedVariable
             }
 
-{- | 'SortedVariable' is a Kore variable with a known sort.
+{- | 'VariableName' is the name of a Kore variable.
+
+A 'VariableName' has instances:
+
+* @'From' variable 'Variable'@
+* @'From' 'Variable' variable@
+
+such that both implementations of 'from' are injective,
+
+prop> (==) (fromVariable x) (fromVariable y) === (==) x y
 
-The instances of @SortedVariable@ must encompass the 'Variable' type by
-implementing 'fromVariable', i.e. we must be able to construct a
-@SortedVariable@ given a parsed 'Variable'.
+prop> (==) x y === (==) (toVariable x) (toVariable y)
 
-'toVariable' may delete information so that
+ -}
+class
+    (Ord variable, From variable Variable, From Variable variable)
+    => VariableName variable
+
+-- | An injection from 'Variable' to any 'VariableName'.
+fromVariable :: forall variable. VariableName variable => Variable -> variable
+fromVariable = from @Variable @variable
 
-> toVariable . fromVariable === id :: Variable -> Variable
+-- | An injection from any 'VariableName' to 'Variable'.
+toVariable :: forall variable. VariableName variable => variable -> Variable
+toVariable = from @variable @Variable
 
-but the reverse is not required.
+{- | 'SortedVariable' is a Kore variable with a known sort.
 
  -}
 class SortedVariable variable where
     -- | The known 'Sort' of the given variable.
     sortedVariableSort :: variable -> Sort
-    sortedVariableSort variable =
-        variableSort
-      where
-        Variable { variableSort } = toVariable variable
-
-    -- | Convert a variable from the parsed syntax of Kore.
-    fromVariable :: Variable -> variable
-    -- | Extract the parsed syntax of a Kore variable.
-    toVariable :: variable -> Variable
--- TODO(traiansf): the 'SortedVariable' class mixes different concerns.
 
 instance SortedVariable Variable where
     sortedVariableSort = variableSort
-    fromVariable = id
-    toVariable = id
 
 {- | Unparse any 'SortedVariable' in an Applicative Kore binder.
 
@@ -188,5 +201,13 @@ instance Unparse Concrete where
 
 instance SortedVariable Concrete where
     sortedVariableSort = \case {}
-    toVariable = \case {}
-    fromVariable = error "Cannot construct a variable in a concrete term!"
+
+instance VariableName Concrete
+
+instance From Variable Concrete where
+    from = error "Cannot construct a variable in a concrete term!"
+    {-# INLINE from #-}
+
+instance From Concrete Variable where
+    from = \case {}
+    {-# INLINE from #-}

kore/src/Kore/Variables/Target.hs

@@ -129,9 +129,16 @@ instance
   where
     sortedVariableSort (Target variable) = sortedVariableSort variable
     sortedVariableSort (NonTarget variable) = sortedVariableSort variable
-    fromVariable = Target . fromVariable
-    toVariable (Target var) = toVariable var
-    toVariable (NonTarget var) = toVariable var
+
+instance VariableName variable => VariableName (Target variable)
+
+instance From variable1 variable2 => From variable1 (Target variable2) where
+    from = Target . from @variable1 @variable2
+    {-# INLINE from #-}
+
+instance From variable1 variable2 => From (Target variable1) variable2 where
+    from = from @variable1 @variable2 . unTarget
+    {-# INLINE from #-}
 
 {- | Ensures that fresh variables are unique under 'unwrapStepperVariable'.
  -}

kore/test/Test/Kore/ASTVerifier/DefinitionVerifier.hs

@@ -85,6 +85,7 @@ import qualified Kore.Internal.TermLike as Internal
 import Kore.Sort
 import Kore.Syntax hiding
     ( PatternF (..)
+    , VariableName
     )
 import Kore.Syntax.Definition
 import qualified Kore.Syntax.PatternF as Syntax

kore/test/Test/Kore/Internal/Pattern.hs

@@ -155,8 +155,14 @@ instance Unparse V where
 
 instance SortedVariable V where
     sortedVariableSort _ = sortVariable
-    fromVariable = undefined
-    toVariable = undefined
+
+instance From Variable V where
+    from = error "Not implemented"
+
+instance From V Variable where
+    from = error "Not implemented"
+
+instance VariableName V
 
 instance FreshVariable V where
     refreshVariable avoiding v@(V name)
@@ -186,8 +192,14 @@ instance Unparse W where
 
 instance SortedVariable W where
     sortedVariableSort _ = sortVariable
-    fromVariable = undefined
-    toVariable = undefined
+
+instance From Variable W where
+    from = error "Not implemented"
+
+instance From W Variable where
+    from = error "Not implemented"
+
+instance VariableName W
 
 instance FreshVariable W where
     refreshVariable avoiding w@(W name)

kore/test/Test/Kore/Step/Function/Integration.hs

@@ -1348,7 +1348,7 @@ appliedMockEvaluator result =
 
 mapVariables
     :: forall variable
-    .  (FreshVariable variable, SortedVariable variable)
+    .  (FreshVariable variable, VariableName variable)
     => Pattern Variable
     -> Pattern variable
 mapVariables =