Add an EquationVariableName to RewritingVariableName

* Add an EquationVariableName to RewritingVariableName

* Add missed case for compareSubstitution

Co-authored-by: Octavian Mircea Sebe <[email protected]>
Co-authored-by: rv-jenkins <[email protected]>

Author: 3 people

kore/src/Kore/Rewriting/RewritingVariable.hs

@@ -7,6 +7,7 @@ License     : NCSA
 module Kore.Rewriting.RewritingVariable
     ( RewritingVariableName
     , RewritingVariable
+    , isEquationVariable
     , isConfigVariable
     , isRuleVariable
     , isSomeConfigVariable
@@ -15,6 +16,7 @@ module Kore.Rewriting.RewritingVariable
     , isSomeRuleVariableName
     , isElementRuleVariable
     , isElementRuleVariableName
+    , mkEquationVariable
     , mkConfigVariable
     , mkRuleVariable
     , mkElementConfigVariable
@@ -59,7 +61,8 @@ import Kore.Variables.Fresh
 {- | The name of a 'RewritingVariable'.
  -}
 data RewritingVariableName
-    = ConfigVariableName !VariableName
+    = EquationVariableName !VariableName
+    | ConfigVariableName !VariableName
     | RuleVariableName   !VariableName
     deriving (Eq, Ord, Show)
     deriving (GHC.Generic)
@@ -68,24 +71,32 @@ data RewritingVariableName
     deriving anyclass (Debug, Diff)
 
 instance SubstitutionOrd RewritingVariableName where
+    compareSubstitution (EquationVariableName _) (RuleVariableName _) = LT
+    compareSubstitution (EquationVariableName _) (ConfigVariableName _) = LT
+    compareSubstitution (RuleVariableName _) (EquationVariableName _) = GT
     compareSubstitution (RuleVariableName _) (ConfigVariableName _) = LT
+    compareSubstitution (ConfigVariableName _) (EquationVariableName _) = GT
     compareSubstitution (ConfigVariableName _) (RuleVariableName _) = GT
     compareSubstitution variable1 variable2 =
         on compareSubstitution toVariableName variable1 variable2
 
 instance FreshPartialOrd RewritingVariableName where
     minBoundName =
         \case
-            RuleVariableName var   -> RuleVariableName (minBoundName var)
-            ConfigVariableName var -> ConfigVariableName (minBoundName var)
+            EquationVariableName var -> EquationVariableName (minBoundName var)
+            RuleVariableName var     -> RuleVariableName (minBoundName var)
+            ConfigVariableName var   -> ConfigVariableName (minBoundName var)
     {-# INLINE minBoundName #-}
 
     maxBoundName =
         \case
-            RuleVariableName var   -> RuleVariableName (maxBoundName var)
-            ConfigVariableName var -> ConfigVariableName (maxBoundName var)
+            EquationVariableName var -> EquationVariableName (maxBoundName var)
+            RuleVariableName var     -> RuleVariableName (maxBoundName var)
+            ConfigVariableName var   -> ConfigVariableName (maxBoundName var)
     {-# INLINE maxBoundName #-}
 
+    nextName (EquationVariableName name1) (EquationVariableName name2) =
+        EquationVariableName <$> nextName name1 name2
     nextName (RuleVariableName name1) (RuleVariableName name2) =
         RuleVariableName <$> nextName name1 name2
     nextName (ConfigVariableName name1) (ConfigVariableName name2) =
@@ -94,13 +105,16 @@ instance FreshPartialOrd RewritingVariableName where
     {-# INLINE nextName #-}
 
 instance Unparse RewritingVariableName where
+    unparse (EquationVariableName variable) = "Equation" <> unparse variable
     unparse (ConfigVariableName variable) = "Config" <> unparse variable
     unparse (RuleVariableName variable) = "Rule" <> unparse variable
 
+    unparse2 (EquationVariableName variable) = "Equation" <> unparse2 variable
     unparse2 (ConfigVariableName variable) = "Config" <> unparse2 variable
     unparse2 (RuleVariableName variable) = "Rule" <> unparse2 variable
 
 instance From RewritingVariableName VariableName where
+    from (EquationVariableName variable) = variable
     from (ConfigVariableName variable) = variable
     from (RuleVariableName variable) = variable
 
@@ -168,12 +182,19 @@ getRewritingVariable
     :: AdjSomeVariableName (RewritingVariableName -> VariableName)
 getRewritingVariable = pure (from @RewritingVariableName @VariableName)
 
+mkEquationVariable :: VariableName -> RewritingVariableName
+mkEquationVariable = EquationVariableName
+
 mkConfigVariable :: VariableName -> RewritingVariableName
 mkConfigVariable = ConfigVariableName
 
 mkRuleVariable :: VariableName -> RewritingVariableName
 mkRuleVariable = RuleVariableName
 
+isEquationVariable :: RewritingVariableName -> Bool
+isEquationVariable (EquationVariableName _) = True
+isEquationVariable _ = False
+
 isConfigVariable :: RewritingVariableName -> Bool
 isConfigVariable (ConfigVariableName _) = True
 isConfigVariable _ = False