Remove the Target type from Kore.Equation (#2344)

Co-authored-by: Thomas Tuegel <[email protected]>
Co-authored-by: Thomas Tuegel <[email protected]>

Author: andreiburdusa

kore/src/Kore/Equation/Application.hs

@@ -4,6 +4,7 @@ License     : NCSA
 
 -}
 
+{-# LANGUAGE Strict #-}
 module Kore.Equation.Application
     ( attemptEquation
     , AttemptEquationResult
@@ -113,10 +114,6 @@ import Kore.TopBottom
 import Kore.Unparser
     ( Unparse (..)
     )
-import Kore.Variables.Target
-    ( Target
-    )
-import qualified Kore.Variables.Target as Target
 import Log
     ( Entry (..)
     , MonadLog
@@ -155,7 +152,7 @@ attemptEquation
     => MonadSimplify simplifier
     => InternalVariable variable
     => SideCondition variable
-    -> TermLike (Target variable)
+    -> TermLike variable
     -> Equation variable
     -> simplifier (AttemptEquationResult variable)
 attemptEquation sideCondition termLike equation =
@@ -179,20 +176,16 @@ attemptEquation sideCondition termLike equation =
                         & whileMatch
                     (equation', predicate) <-
                         applyAndSelectMatchResult matchResults
-                    let matchPredicate' =
-                            Predicate.mapVariables
-                                (pure Target.unTarget)
-                                matchPredicate
                     return
                         ( equation'
-                        , makeAndPredicate predicate matchPredicate'
+                        , makeAndPredicate predicate matchPredicate
                         )
         let Equation { requires } = equation'
         checkRequires sideCondition predicate requires & whileCheckRequires
         let Equation { right, ensures } = equation'
         return $ Pattern.withCondition right $ from @(Predicate _) ensures
   where
-    equationRenamed = targetEquationVariables sideCondition termLike equation
+    equationRenamed = refreshVariables sideCondition termLike equation
     matchError =
         MatchError
         { matchTerm = termLike
@@ -203,7 +196,7 @@ attemptEquation sideCondition termLike equation =
         & MaybeT & noteT matchError
 
     applyAndSelectMatchResult
-        :: [MatchResult (Target variable)]
+        :: [MatchResult variable]
         -> ExceptT
             (AttemptEquationError variable)
             simplifier
@@ -234,13 +227,13 @@ applySubstitutionAndSimplify
     :: HasCallStack
     => MonadSimplify simplifier
     => InternalVariable variable
-    => Predicate (Target variable)
-    -> Maybe (Predicate (Target variable))
-    -> Map (SomeVariableName (Target variable)) (TermLike (Target variable))
+    => Predicate variable
+    -> Maybe (Predicate variable)
+    -> Map (SomeVariableName variable) (TermLike variable)
     -> ExceptT
-        (MatchError (Target variable))
+        (MatchError variable)
         simplifier
-        [MatchResult (Target variable)]
+        [MatchResult variable]
 applySubstitutionAndSimplify
     argument
     antiLeft
@@ -284,9 +277,9 @@ applyMatchResult
     :: forall monad variable
     .   Monad monad
     =>  InternalVariable variable
-    =>  Equation (Target variable)
-    ->  MatchResult (Target variable)
-    ->  ExceptT (ApplyMatchResultErrors (Target variable)) monad
+    =>  Equation variable
+    ->  MatchResult variable
+    ->  ExceptT (ApplyMatchResultErrors variable) monad
             (Equation variable, Predicate variable)
 applyMatchResult equation matchResult@(predicate, substitution) = do
     case errors of
@@ -297,21 +290,28 @@ applyMatchResult equation matchResult@(predicate, substitution) = do
                 }
         _      -> return ()
     let predicate' =
-            Predicate.substitute substitution predicate
-            & Predicate.mapVariables (pure Target.unTarget)
+            Predicate.substitute orientedSubstitution predicate
         equation' =
-            Equation.substitute substitution equation
-            & Equation.mapVariables (pure Target.unTarget)
+            Equation.substitute orientedSubstitution equation
     return (equation', predicate')
   where
-    equationVariables = freeVariables equation & FreeVariables.toList
+    orientedSubstitution = Substitution.orientSubstitution occursInEquation substitution
+
+    equationVariables = freeVariables equation
+
+    occursInEquation :: (SomeVariableName variable -> Bool)
+    occursInEquation = \someVariableName ->
+        Set.member someVariableName equationVariableNames
+
+    equationVariableNames =
+        Set.map variableName (FreeVariables.toSet equationVariables)
 
     errors =
-        concatMap checkVariable equationVariables
-        <> checkNonTargetVariables
+        concatMap checkVariable (FreeVariables.toList equationVariables)
+        <> checkNotInEquation
 
     checkVariable Variable { variableName } =
-        case Map.lookup variableName substitution of
+        case Map.lookup variableName orientedSubstitution of
             Nothing -> [NotMatched variableName]
             Just termLike ->
                 checkConcreteVariable variableName termLike
@@ -331,9 +331,9 @@ applyMatchResult equation matchResult@(predicate, substitution) = do
       | otherwise
       = empty
 
-    checkNonTargetVariables =
+    checkNotInEquation =
         NonMatchingSubstitution
-        <$> filter Target.isSomeNonTargetName (Map.keys substitution)
+        <$> filter (not . occursInEquation) (Map.keys orientedSubstitution)
 
     Equation { attributes } = equation
     concretes =
@@ -400,37 +400,27 @@ checkRequires sideCondition predicate requires =
         . Simplifier.localSimplifierAxioms (const mempty)
     withAxioms = id
 
-{- | Make the 'Equation' variables distinct from the initial pattern.
-
-The variables are marked 'Target' and renamed to avoid any variables in the
-'SideCondition' or the 'TermLike'.
-
- -}
-targetEquationVariables
+refreshVariables
     :: forall variable
     .  InternalVariable variable
     => SideCondition variable
-    -> TermLike (Target variable)
+    -> TermLike variable
     -> Equation variable
-    -> Equation (Target variable)
-targetEquationVariables sideCondition initial =
+    -> Equation variable
+refreshVariables sideCondition initial =
     snd
     . Equation.refreshVariables avoiding
-    . Equation.mapVariables Target.mkUnifiedTarget
   where
     avoiding = sideConditionVariables <> freeVariables initial
-    sideConditionVariables =
-        FreeVariables.mapFreeVariables
-            Target.mkUnifiedNonTarget
-            $ freeVariables sideCondition
+    sideConditionVariables = freeVariables sideCondition
 
 -- * Errors
 
 {- | Errors that can occur during 'attemptEquation'.
  -}
 data AttemptEquationError variable
-    = WhileMatch !(MatchError (Target variable))
-    | WhileApplyMatchResult !(ApplyMatchResultErrors (Target variable))
+    = WhileMatch !(MatchError variable)
+    | WhileApplyMatchResult !(ApplyMatchResultErrors variable)
     | WhileCheckRequires !(CheckRequiresError variable)
     deriving (Eq, Ord, Show)
     deriving (GHC.Generic)
@@ -445,27 +435,25 @@ mapAttemptEquationErrorVariables
 mapAttemptEquationErrorVariables adj =
     \case
         WhileMatch matchError ->
-            WhileMatch $ mapMatchErrorVariables adjTarget matchError
+            WhileMatch $ mapMatchErrorVariables adj matchError
         WhileApplyMatchResult applyMatchResultErrors ->
             WhileApplyMatchResult
             $ mapApplyMatchResultErrorsVariables
-                adjTarget
+                adj
                 applyMatchResultErrors
         WhileCheckRequires checkRequiresError ->
             WhileCheckRequires
             $ mapCheckRequiresErrorVariables adj checkRequiresError
-  where
-    adjTarget = fmap <$> adj
 
 whileMatch
     :: Functor monad
-    => ExceptT (MatchError (Target variable)) monad a
+    => ExceptT (MatchError variable) monad a
     -> ExceptT (AttemptEquationError variable) monad a
 whileMatch = withExceptT WhileMatch
 
 whileApplyMatchResult
     :: Functor monad
-    => ExceptT (ApplyMatchResultErrors (Target variable)) monad a
+    => ExceptT (ApplyMatchResultErrors variable) monad a
     -> ExceptT (AttemptEquationError variable) monad a
 whileApplyMatchResult = withExceptT WhileApplyMatchResult
 

kore/src/Kore/Internal/Substitution.hs

@@ -47,6 +47,7 @@ module Kore.Internal.Substitution
     , mkNormalization
     , applyNormalized
     , substitute
+    , orientSubstitution
     ) where
 
 import Prelude.Kore hiding
@@ -648,6 +649,106 @@ variables (NormalizedSubstitution subst) = Map.keysSet subst
 variables (Substitution subst) =
     foldMap (Set.singleton . assignedVariable) subst
 
+{- | Apply an orientation to all variable-renaming substitutions.
+
+A variable-renaming substitution is a pair of the form
+
+@
+X:S = Y:S
+@
+
+In a normalized substitution, the variable on the left-hand side of each
+substitution pair may not appear in any other substitution pair. The order of a
+variable-renaming pair is logically irrelevant, but often we have a preference
+for which of @X@ and @Y@ should appear on the left-hand side (that is, we have a
+preferred /orientation/).
+
+@orientSubstitution@ applies an orientation to a normalized substitution and
+yields a normalized substitution. The orientation is expressed as a function
+
+@
+SomeVariableName variable -> Bool
+@
+
+returning `True` when the named variable is preferred on the left-hand side of a
+variable-renaming substitution pair. Each variable-renaming pair is oriented so
+that the variable on the left-hand side is a preferred variable, if possible.
+@orientSubstitution@ does not alter substitution pairs where both or neither
+variable is preferred for the left-hand side.
+-}
+orientSubstitution
+    :: forall variable
+    .  InternalVariable variable
+    => (SomeVariableName variable -> Bool)
+    -- ^ Orientation: Is the named variable preferred on the left-hand side of
+    -- variable-renaming substitution pairs?
+    -> Map (SomeVariableName variable) (TermLike variable)
+    -- ^ Normalized substitution
+    -> Map (SomeVariableName variable) (TermLike variable)
+orientSubstitution toLeft substitution =
+    foldl' go substitution $ Map.toList substitution
+  where
+    go substitutionInProgress initialPair@(initialKey, _)
+      | Just (newKey, newValue) <- retractReorderedPair initialPair =
+        -- Re-orienting X = Y as Y = X.
+        let newPair = Map.singleton newKey newValue
+        in case Map.lookup newKey substitutionInProgress of
+            Nothing ->
+                -- There is no other Y = X substitution in the map.
+                substitutionInProgress
+                -- Remove X = Y pair.
+                & Map.delete initialKey
+                -- Apply Y = X to the right-hand side of all pairs.
+                & Map.map (TermLike.substitute newPair)
+                -- Insert Y = X pair.
+                & Map.insert newKey newValue
+            Just already ->
+                -- There is a substitution Y = T in the map.
+                substitutionInProgress
+                -- Remove Y = T.
+                & Map.delete newKey
+                -- Apply Y = X to the right-hand side of all pairs.
+                & Map.map (TermLike.substitute newPair)
+                -- Insert Y = X pair.
+                & Map.insert newKey newValue
+                -- Apply X = T to the right-hand side of all pairs. This
+                -- substitution never needs to be reoriented, but the reason why
+                -- is subtle:
+                -- 1. The Y = T substitution came from another swapped pair. It
+                --    was not present in the original substitution: the original
+                --    substitution was normalized, and the substitution we are
+                --    reorienting now had Y on the right-hand side, so Y was not
+                --    on the left-hand side of any pair in the original
+                --    subsitution.
+                -- 2. If Y = T came from another swapped pair, then T is not a
+                --    preferred variable.
+                -- 3. We just checked that X is not a preferred variable.
+                -- 4. Therefore, X = T is a valid orientation.
+                & Map.map
+                    (TermLike.substitute (Map.singleton initialKey already))
+                -- Insert X = T pair.
+                & Map.insert initialKey already
+      | otherwise = substitutionInProgress
+
+    retractReorderedPair
+        :: (SomeVariableName variable, TermLike variable)
+        -> Maybe (SomeVariableName variable, TermLike variable)
+    retractReorderedPair (xName, TermLike.Var_ (Variable yName ySort))
+      | isSameMultiplicity xName yName
+      , toLeft yName
+      , not (toLeft xName)
+      = Just (yName, TermLike.mkVar (Variable xName ySort))
+    retractReorderedPair _ = Nothing
+
+    isSameMultiplicity
+        :: SomeVariableName variable
+        -> SomeVariableName variable
+        -> Bool
+    isSameMultiplicity x y
+      | SomeVariableNameElement _ <- x, SomeVariableNameElement _ <- y = True
+      | SomeVariableNameSet     _ <- x, SomeVariableNameSet     _ <- y = True
+      | otherwise = False
+
 {- | The result of /normalizing/ a substitution.
 
 'normalized' holds the part of the substitution was normalized successfully.

kore/src/Kore/Step/Axiom/EvaluationStrategy.hs

@@ -7,6 +7,8 @@ Maintainer  : [email protected]
 Stability   : experimental
 Portability : portable
 -}
+
+{-# LANGUAGE Strict #-}
 module Kore.Step.Axiom.EvaluationStrategy
     ( builtinEvaluation
     , definitionEvaluation
@@ -119,7 +121,10 @@ attemptEquationAndAccumulateErrors condition term equation =
   where
     attemptEquation =
         ExceptRT . ExceptT
-        $ Equation.attemptEquation condition term equation
+        $ Equation.attemptEquation
+            condition
+            (TermLike.mapVariables (pure Target.unTarget) term)
+            equation
         >>= either (return . Left . Option . Just . Min) (fmap Right . apply)
     apply = Equation.applyEquation condition equation
 
@@ -143,8 +148,11 @@ simplificationEvaluation
 simplificationEvaluation equation =
     BuiltinAndAxiomSimplifier $ \term condition -> do
         let equation' = Equation.mapVariables (pure fromVariableName) equation
-            term' = TermLike.mapVariables Target.mkUnifiedNonTarget term
-        result <- Equation.attemptEquation condition term' equation'
+        result <-
+            Equation.attemptEquation
+                condition
+                term
+                equation'
         let apply = Equation.applyEquation condition equation'
         case result of
             Right applied -> do

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

@@ -4,6 +4,7 @@ License     : NCSA
 
  -}
 
+{-# LANGUAGE Strict #-}
 module Kore.Step.Simplification.SubstitutionSimplifier
     ( SubstitutionSimplifier (..)
     , substitutionSimplifier
@@ -376,7 +377,6 @@ simplifySubstitutionWorker sideCondition makeAnd' = \substitution -> do
         return substitution'
 
     sideConditionRepresentation = SideCondition.toRepresentation sideCondition
-
 data Private variable =
     Private
         { accum :: !(Condition variable)