diff --git a/kore/src/Kore/Builtin/AssociativeCommutative.hs b/kore/src/Kore/Builtin/AssociativeCommutative.hs index df9a83b994..7e9b4b0fa5 100644 --- a/kore/src/Kore/Builtin/AssociativeCommutative.hs +++ b/kore/src/Kore/Builtin/AssociativeCommutative.hs @@ -30,8 +30,10 @@ module Kore.Builtin.AssociativeCommutative ( renormalize, TermNormalizedAc, unifyEqualsNormalized, + matchUnifyEqualsNormalizedAc, UnitSymbol (..), VariableElements (..), + UnifyEqualsNormAc (..), ) where import Control.Error ( @@ -695,14 +697,16 @@ unifyEqualsNormalized :: ) -> InternalAc Key normalized (TermLike RewritingVariableName) -> InternalAc Key normalized (TermLike RewritingVariableName) -> - MaybeT unifier (Pattern RewritingVariableName) + UnifyEqualsNormAc normalized RewritingVariableName -> + unifier (Pattern RewritingVariableName) unifyEqualsNormalized tools first second unifyEqualsChildren normalized1 - normalized2 = + normalized2 + unifyData = do let InternalAc{builtinAcChild = firstNormalized} = normalized1 @@ -717,6 +721,7 @@ unifyEqualsNormalized unifyEqualsChildren firstNormalized secondNormalized + unifyData let unifierNormalizedTerm :: TermNormalizedAc normalized RewritingVariableName unifierCondition :: Condition RewritingVariableName @@ -757,17 +762,155 @@ unifyEqualsNormalized HasCallStack => InternalVariable variable => TermLike variable -> - MaybeT unifier (TermNormalizedAc normalized variable) + unifier (TermNormalizedAc normalized variable) normalize1 patt = case toNormalized patt of Bottom -> - lift $ - debugUnifyBottomAndReturnBottom - "Duplicated elements in normalization." - first - second + debugUnifyBottomAndReturnBottom + "Duplicated elements in normalization." + first + second Normalized n -> return n +data UnifyEqualsElementListsData normalized = UnifyEqualsElementListsData + { -- Given normalized data norm1, norm2, norm1 - norm2 and norm2 - norm1 + allElements1, allElements2 :: ![ConcreteOrWithVariable normalized RewritingVariableName] + , -- Is Just v if v is the sole opaque in norm1 - norm2, else Nothing + maybeVar :: !(Maybe (ElementVariable RewritingVariableName)) + } + +data UnifyEqualsNormAc normalized variable + = UnifyEqualsElementLists !(UnifyEqualsElementListsData normalized) + | UnifyOpaqueVar !(UnifyOpVarResult variable) + +matchUnifyEqualsNormalizedAc :: + forall normalized. + TermWrapper normalized => + SmtMetadataTools Attribute.Symbol -> + InternalAc Key normalized (TermLike RewritingVariableName) -> + InternalAc Key normalized (TermLike RewritingVariableName) -> + Maybe (UnifyEqualsNormAc normalized RewritingVariableName) +matchUnifyEqualsNormalizedAc + tools + normalized1 + normalized2 = + case (opaqueDifference1, opaqueDifference2) of + ([], []) -> + Just $ + UnifyEqualsElementLists $ + UnifyEqualsElementListsData + allElements1 + allElements2 + Nothing + ([ElemVar_ v1], _) + | null opaqueDifference2 -> + Just $ + UnifyEqualsElementLists $ + UnifyEqualsElementListsData + allElements1 + allElements2 + (Just v1) + | null allElements1 -> + fmap UnifyOpaqueVar $ + matchUnifyOpaqueVariable' + v1 + allElements2 + opaqueDifference2 + _ -> Nothing + where + matchUnifyOpaqueVariable' = + matchUnifyOpaqueVariable tools + + listToMap :: Hashable a => Ord a => [a] -> HashMap a Int + listToMap = List.foldl' (\m k -> HashMap.insertWith (+) k 1 m) HashMap.empty + mapToList :: HashMap a Int -> [a] + mapToList = + HashMap.foldrWithKey + (\key count result -> replicate count key ++ result) + [] + + NormalizedAc + { elementsWithVariables = preElementsWithVariables1 + , concreteElements = concreteElements1 + , opaque = opaque1 + } = + unwrapAc firstNormalized + NormalizedAc + { elementsWithVariables = preElementsWithVariables2 + , concreteElements = concreteElements2 + , opaque = opaque2 + } = + unwrapAc secondNormalized + + InternalAc{builtinAcChild = firstNormalized} = + normalized1 + InternalAc{builtinAcChild = secondNormalized} = + normalized2 + + opaque1Map = listToMap opaque1 + opaque2Map = listToMap opaque2 + + elementsWithVariables1 = unwrapElement <$> preElementsWithVariables1 + elementsWithVariables2 = unwrapElement <$> preElementsWithVariables2 + elementsWithVariables1Map = HashMap.fromList elementsWithVariables1 + elementsWithVariables2Map = HashMap.fromList elementsWithVariables2 + + commonElements = + HashMap.intersectionWith + (,) + concreteElements1 + concreteElements2 + commonVariables = + HashMap.intersectionWith + (,) + elementsWithVariables1Map + elementsWithVariables2Map + + -- Duplicates must be kept in case any of the opaque terms turns out to be + -- non-empty, in which case one of the terms is bottom, which + -- means that the unification result is bottom. + commonOpaqueMap = HashMap.intersectionWith max opaque1Map opaque2Map + + commonOpaqueKeys = HashMap.keysSet commonOpaqueMap + + elementDifference1 = + HashMap.toList (HashMap.difference concreteElements1 commonElements) + elementDifference2 = + HashMap.toList (HashMap.difference concreteElements2 commonElements) + elementVariableDifference1 = + HashMap.toList (HashMap.difference elementsWithVariables1Map commonVariables) + elementVariableDifference2 = + HashMap.toList (HashMap.difference elementsWithVariables2Map commonVariables) + opaqueDifference1 = + mapToList (withoutKeys opaque1Map commonOpaqueKeys) + opaqueDifference2 = + mapToList (withoutKeys opaque2Map commonOpaqueKeys) + + withoutKeys :: + Hashable k => + Eq k => + HashMap k v -> + HashSet k -> + HashMap k v + withoutKeys hmap (HashSet.toList -> hset) = + let keys = zip hset (repeat ()) & HashMap.fromList + in hmap `HashMap.difference` keys + + allElements1 = + map WithVariablePat elementVariableDifference1 + ++ map toConcretePat elementDifference1 + allElements2 = + map WithVariablePat elementVariableDifference2 + ++ map toConcretePat elementDifference2 + + toConcretePat :: + (Key, Value normalized (TermLike RewritingVariableName)) -> + ConcreteOrWithVariable + normalized + RewritingVariableName + toConcretePat (a, b) = + ConcretePat (from @Key @(TermLike RewritingVariableName) a, b) + {- | Unifies two AC structs represented as @NormalizedAc@. Currently allows at most one opaque term in the two arguments taken together. @@ -787,8 +930,8 @@ unifyEqualsNormalizedAc :: ) -> TermNormalizedAc normalized RewritingVariableName -> TermNormalizedAc normalized RewritingVariableName -> - MaybeT - unifier + UnifyEqualsNormAc normalized RewritingVariableName -> + unifier ( Conditional RewritingVariableName (TermNormalizedAc normalized RewritingVariableName) @@ -799,37 +942,26 @@ unifyEqualsNormalizedAc second unifyEqualsChildren normalized1 - normalized2 = + normalized2 + unifyData = do - (simpleUnifier, opaques) <- case (opaqueDifference1, opaqueDifference2) of - ([], []) -> - lift $ - unifyEqualsElementLists' - allElements1 - allElements2 - Nothing - ([ElemVar_ v1], _) - | null opaqueDifference2 -> - lift $ - unifyEqualsElementLists' - allElements1 - allElements2 - (Just v1) - | null allElements1 -> - unifyOpaqueVariable' v1 allElements2 opaqueDifference2 - (_, [ElemVar_ v2]) - | null opaqueDifference1 -> - lift $ - unifyEqualsElementLists' - allElements2 - allElements1 - (Just v2) - | null allElements2 -> - unifyOpaqueVariable' v2 allElements1 opaqueDifference1 - _ -> empty + (simpleUnifier, opaques) <- case unifyData of + UnifyEqualsElementLists unifyData' -> + unifyEqualsElementLists' + allElements1 + allElements2 + maybeVar + where + UnifyEqualsElementListsData{allElements1, allElements2, maybeVar} = unifyData' + UnifyOpaqueVar unifyData' -> + unifyOpaqueVariable + bottomWithExplanation + unifyEqualsChildren + unifyData' + let (unifiedElements, unifierCondition) = Conditional.splitTerm simpleUnifier - lift $ do + do -- unifier monad -- unify the parts not sent to unifyEqualsNormalizedElements. (commonElementsTerms, commonElementsCondition) <- @@ -874,9 +1006,6 @@ unifyEqualsNormalizedAc second unifyEqualsChildren - unifyOpaqueVariable' = - unifyOpaqueVariable tools bottomWithExplanation unifyEqualsChildren - NormalizedAc { elementsWithVariables = preElementsWithVariables1 , concreteElements = concreteElements1 @@ -915,45 +1044,6 @@ unifyEqualsNormalizedAc commonOpaqueMap = HashMap.intersectionWith max opaque1Map opaque2Map commonOpaque = mapToList commonOpaqueMap - commonOpaqueKeys = HashMap.keysSet commonOpaqueMap - - elementDifference1 = - HashMap.toList (HashMap.difference concreteElements1 commonElements) - elementDifference2 = - HashMap.toList (HashMap.difference concreteElements2 commonElements) - elementVariableDifference1 = - HashMap.toList (HashMap.difference elementsWithVariables1Map commonVariables) - elementVariableDifference2 = - HashMap.toList (HashMap.difference elementsWithVariables2Map commonVariables) - opaqueDifference1 = - mapToList (withoutKeys opaque1Map commonOpaqueKeys) - opaqueDifference2 = - mapToList (withoutKeys opaque2Map commonOpaqueKeys) - - withoutKeys :: - Hashable k => - Eq k => - HashMap k v -> - HashSet k -> - HashMap k v - withoutKeys hmap (HashSet.toList -> hset) = - let keys = zip hset (repeat ()) & HashMap.fromList - in hmap `HashMap.difference` keys - - allElements1 = - map WithVariablePat elementVariableDifference1 - ++ map toConcretePat elementDifference1 - allElements2 = - map WithVariablePat elementVariableDifference2 - ++ map toConcretePat elementDifference2 - - toConcretePat :: - (Key, Value normalized (TermLike RewritingVariableName)) -> - ConcreteOrWithVariable - normalized - RewritingVariableName - toConcretePat (a, b) = - ConcretePat (from @Key @(TermLike RewritingVariableName) a, b) unifyElementList :: forall key. @@ -1342,39 +1432,35 @@ unifyEqualsElementLists (unifyEqualsConcreteOrWithVariable unifyEqualsChildren) remainderError = nonEmptyRemainderError first second -unifyOpaqueVariable :: - ( MonadUnify unifier - , TermWrapper normalized +data NoCheckUnifyOpaqueChildrenData variable = NoCheckUnifyOpaqueChildrenData + { -- Given normalized data norm1, norm2, the sole opaque variable in norm1 - norm2 + v1 :: !(TermLike.ElementVariable variable) + , -- The term to unify against v1 + second :: !(TermLike variable) + } + +data UnifyOpVarResult variable + = NoCheckUnifyOpaqueChildren !(NoCheckUnifyOpaqueChildrenData variable) + | BottomWithExplanation + +matchUnifyOpaqueVariable :: + ( TermWrapper normalized , InternalVariable variable ) => SmtMetadataTools Attribute.Symbol -> - (forall a. Text -> unifier a) -> - -- | unifier function - (TermLike variable -> TermLike variable -> unifier (Pattern variable)) -> TermLike.ElementVariable variable -> [ConcreteOrWithVariable normalized variable] -> [TermLike variable] -> - MaybeT - unifier - ( Conditional - variable - [(TermLike variable, Value normalized (TermLike variable))] - , [TermLike variable] - ) -unifyOpaqueVariable _ _ unifyChildren v1 [] [second@(ElemVar_ _)] = - noCheckUnifyOpaqueChildren unifyChildren v1 second -unifyOpaqueVariable + Maybe (UnifyOpVarResult variable) +matchUnifyOpaqueVariable _ v1 [] [second@(ElemVar_ _)] = + Just $ NoCheckUnifyOpaqueChildren NoCheckUnifyOpaqueChildrenData{v1, second} +matchUnifyOpaqueVariable tools - bottomWithExplanation - unifyChildren v1 concreteOrVariableTerms opaqueTerms = case elementListAsNormalized pairs of - Nothing -> - lift $ - bottomWithExplanation - "Duplicated element in unification results" + Nothing -> Just BottomWithExplanation Just elementTerm -> let secondTerm = asInternal @@ -1384,12 +1470,42 @@ unifyOpaqueVariable elementTerm{opaque = opaqueTerms} ) in if TermLike.isFunctionPattern secondTerm - then noCheckUnifyOpaqueChildren unifyChildren v1 secondTerm - else empty + then + Just $ + NoCheckUnifyOpaqueChildren $ + NoCheckUnifyOpaqueChildrenData v1 secondTerm + else Nothing where sort = variableSort v1 pairs = map fromConcreteOrWithVariable concreteOrVariableTerms +unifyOpaqueVariable :: + ( MonadUnify unifier + , InternalVariable variable + ) => + (forall a. Text -> unifier a) -> + -- | unifier function + (TermLike variable -> TermLike variable -> unifier (Pattern variable)) -> + UnifyOpVarResult variable -> + unifier + ( Conditional + variable + [(TermLike variable, Value normalized (TermLike variable))] + , [TermLike variable] + ) +unifyOpaqueVariable + bottomWithExplanation + unifyChildren + unifyData = + case unifyData of + NoCheckUnifyOpaqueChildren unifyData' -> + noCheckUnifyOpaqueChildren unifyChildren v1 second + where + NoCheckUnifyOpaqueChildrenData{v1, second} = unifyData' + _ -> + bottomWithExplanation + "Duplicated element in unification results" + noCheckUnifyOpaqueChildren :: ( MonadUnify unifier , InternalVariable variable @@ -1397,14 +1513,13 @@ noCheckUnifyOpaqueChildren :: (TermLike variable -> TermLike variable -> unifier (Pattern variable)) -> TermLike.ElementVariable variable -> TermLike variable -> - MaybeT - unifier + unifier ( Conditional variable [(TermLike variable, Value normalized (TermLike variable))] , [TermLike variable] ) -noCheckUnifyOpaqueChildren unifyChildren v1 second = lift $ do +noCheckUnifyOpaqueChildren unifyChildren v1 second = do unifier <- unifyChildren (mkElemVar v1) second let (opaque, predicate) = Conditional.splitTerm unifier return ([] `Conditional.withCondition` predicate, [opaque]) diff --git a/kore/src/Kore/Builtin/Bool.hs b/kore/src/Kore/Builtin/Bool.hs index 6f53e56ea7..04845691eb 100644 --- a/kore/src/Kore/Builtin/Bool.hs +++ b/kore/src/Kore/Builtin/Bool.hs @@ -169,6 +169,7 @@ builtinFunctions = data UnifyBool = UnifyBool { bool1, bool2 :: !InternalBool + , term1, term2 :: !(TermLike RewritingVariableName) } {- | Matches @@ -187,10 +188,10 @@ matchBools :: TermLike RewritingVariableName -> TermLike RewritingVariableName -> Maybe UnifyBool -matchBools first second - | InternalBool_ bool1 <- first - , InternalBool_ bool2 <- second = - Just UnifyBool{bool1, bool2} +matchBools term1 term2 + | InternalBool_ bool1 <- term2 + , InternalBool_ bool2 <- term1 = + Just UnifyBool{bool1, bool2, term1, term2} | otherwise = Nothing {-# INLINE matchBools #-} @@ -198,20 +199,23 @@ matchBools first second unifyBool :: forall unifier. MonadUnify unifier => - TermLike RewritingVariableName -> - TermLike RewritingVariableName -> UnifyBool -> unifier (Pattern RewritingVariableName) -unifyBool termLike1 termLike2 unifyData +unifyBool unifyData | bool1 == bool2 = - return (Pattern.fromTermLike termLike1) + return (Pattern.fromTermLike term1) | otherwise = debugUnifyBottomAndReturnBottom "different Bool domain values" - termLike1 - termLike2 + term1 + term2 where - UnifyBool{bool1, bool2} = unifyData + UnifyBool{bool1, bool2, term1, term2} = unifyData + +data UnifyBoolAnd = UnifyBoolAnd + { term :: !(TermLike RewritingVariableName) + , boolAnd :: !BoolAnd + } {- | Matches @@ -222,18 +226,24 @@ unifyBool termLike1 termLike2 unifyData and @ -\\and{_}(\\dv{Bool}("true"), andBool(_,_)) +\\and{_}(\\dv{Bool}("true"), andBool(_,_)), @ + +symmetric in the two arguments. -} matchUnifyBoolAnd :: TermLike RewritingVariableName -> TermLike RewritingVariableName -> - Maybe BoolAnd + Maybe UnifyBoolAnd matchUnifyBoolAnd first second | Just True <- matchBool first , Just boolAnd <- matchBoolAnd second , isFunctionPattern second = - Just boolAnd + Just $ UnifyBoolAnd{term = first, boolAnd} + | Just True <- matchBool second + , Just boolAnd <- matchBoolAnd first + , isFunctionPattern first = + Just $ UnifyBoolAnd{term = second, boolAnd} | otherwise = Nothing {-# INLINE matchUnifyBoolAnd #-} @@ -242,12 +252,12 @@ unifyBoolAnd :: forall unifier. MonadUnify unifier => TermSimplifier RewritingVariableName unifier -> - TermLike RewritingVariableName -> - BoolAnd -> + UnifyBoolAnd -> unifier (Pattern RewritingVariableName) -unifyBoolAnd unifyChildren term boolAnd = +unifyBoolAnd unifyChildren unifyData = unifyBothWith unifyChildren term operand1 operand2 where + UnifyBoolAnd{term, boolAnd} = unifyData BoolAnd{operand1, operand2} = boolAnd {- |Takes a (function-like) pattern and unifies it against two other patterns. @@ -275,6 +285,11 @@ unifyBothWith unify termLike1 operand1 operand2 = do unify' term1 term2 = Pattern.withoutTerm <$> unify term1 term2 +data UnifyBoolOr = UnifyBoolOr + { term :: !(TermLike RewritingVariableName) + , boolOr :: !BoolOr + } + {- | Matches @ @@ -284,18 +299,24 @@ unifyBothWith unify termLike1 operand1 operand2 = do and @ -\\and{_}(\\dv{Bool}("false"), boolOr(_,_)) +\\and{_}(\\dv{Bool}("false"), boolOr(_,_)), @ + +symmetric in the two arguments. -} matchUnifyBoolOr :: TermLike RewritingVariableName -> TermLike RewritingVariableName -> - Maybe BoolOr + Maybe UnifyBoolOr matchUnifyBoolOr first second | Just False <- matchBool first , Just boolOr <- matchBoolOr second , isFunctionPattern second = - Just boolOr + Just UnifyBoolOr{term = first, boolOr} + | Just False <- matchBool second + , Just boolOr <- matchBoolOr first + , isFunctionPattern first = + Just UnifyBoolOr{term = second, boolOr} | otherwise = Nothing {-# INLINE matchUnifyBoolOr #-} @@ -303,17 +324,17 @@ unifyBoolOr :: forall unifier. MonadUnify unifier => TermSimplifier RewritingVariableName unifier -> - TermLike RewritingVariableName -> - BoolOr -> + UnifyBoolOr -> unifier (Pattern RewritingVariableName) -unifyBoolOr unifyChildren termLike boolOr = - unifyBothWith unifyChildren termLike operand1 operand2 +unifyBoolOr unifyChildren unifyData = + unifyBothWith unifyChildren term operand1 operand2 where + UnifyBoolOr{term, boolOr} = unifyData BoolOr{operand1, operand2} = boolOr data UnifyBoolNot = UnifyBoolNot - { boolNot :: BoolNot - , value :: Bool + { boolNot :: !BoolNot + , value :: !InternalBool } {- | Matches @@ -325,8 +346,10 @@ data UnifyBoolNot = UnifyBoolNot and @ -\\and{_}(notBool(_), \\dv{Bool}(_)) +\\and{_}(notBool(_), \\dv{Bool}(_)), @ + +symmetric in the two arguments. -} matchUnifyBoolNot :: TermLike RewritingVariableName -> @@ -335,24 +358,33 @@ matchUnifyBoolNot :: matchUnifyBoolNot first second | Just boolNot <- matchBoolNot first , isFunctionPattern first - , Just value <- matchBool second = - Just $ UnifyBoolNot boolNot value + , Just value <- matchInternalBool second = + Just UnifyBoolNot{boolNot, value} + | Just boolNot <- matchBoolNot second + , isFunctionPattern second + , Just value <- matchInternalBool first = + Just UnifyBoolNot{boolNot, value} | otherwise = Nothing {-# INLINE matchUnifyBoolNot #-} unifyBoolNot :: forall unifier. TermSimplifier RewritingVariableName unifier -> - TermLike RewritingVariableName -> UnifyBoolNot -> unifier (Pattern RewritingVariableName) -unifyBoolNot unifyChildren term unifyData = - let notValue = asInternal (termLikeSort term) (not value) +unifyBoolNot unifyChildren unifyData = + let notValue = asInternal internalBoolSort (not internalBoolValue) in unifyChildren notValue operand where UnifyBoolNot{boolNot, value} = unifyData + InternalBool{internalBoolValue, internalBoolSort} = value BoolNot{operand} = boolNot +matchInternalBool :: TermLike variable -> Maybe InternalBool +matchInternalBool (InternalBool_ internalBool) = + Just internalBool +matchInternalBool _ = Nothing + -- | Match a @BOOL.Bool@ builtin value. matchBool :: TermLike variable -> Maybe Bool matchBool (InternalBool_ InternalBool{internalBoolValue}) = diff --git a/kore/src/Kore/Builtin/Endianness.hs b/kore/src/Kore/Builtin/Endianness.hs index 0750b5a112..d3c38779fe 100644 --- a/kore/src/Kore/Builtin/Endianness.hs +++ b/kore/src/Kore/Builtin/Endianness.hs @@ -7,12 +7,10 @@ module Kore.Builtin.Endianness ( littleEndianKey, bigEndianKey, unifyEquals, + matchUnifyEqualsEndianness, module Kore.Builtin.Endianness.Endianness, ) where -import Control.Error ( - MaybeT, - ) import Data.Functor.Const import qualified Data.HashMap.Strict as HashMap import Data.String ( @@ -31,6 +29,7 @@ import Kore.Internal.TermLike import Kore.Log.DebugUnifyBottom ( debugUnifyBottomAndReturnBottom, ) +import Kore.Rewrite.RewritingVariable import Kore.Unification.Unify ( MonadUnify, ) @@ -77,18 +76,33 @@ littleEndianVerifier = endiannessVerifier LittleEndian bigEndianVerifier :: ApplicationVerifier Verified.Pattern bigEndianVerifier = endiannessVerifier BigEndian +data UnifyEqualsEndianness = UnifyEqualsEndianness + { end1, end2 :: !Endianness + , term1, term2 :: !(TermLike RewritingVariableName) + } + +-- | Matches two terms having the Endianness constructor. +matchUnifyEqualsEndianness :: + TermLike RewritingVariableName -> + TermLike RewritingVariableName -> + Maybe UnifyEqualsEndianness +matchUnifyEqualsEndianness term1 term2 + | Endianness_ end1 <- term1 + , Endianness_ end2 <- term2 = + Just UnifyEqualsEndianness{end1, end2, term1, term2} + | otherwise = Nothing +{-# INLINE matchUnifyEqualsEndianness #-} + unifyEquals :: - InternalVariable variable => MonadUnify unifier => - TermLike variable -> - TermLike variable -> - MaybeT unifier (Pattern variable) -unifyEquals termLike1@(Endianness_ end1) termLike2@(Endianness_ end2) - | end1 == end2 = return (Pattern.fromTermLike termLike1) + UnifyEqualsEndianness -> + unifier (Pattern RewritingVariableName) +unifyEquals unifyData + | end1 == end2 = return (Pattern.fromTermLike term1) | otherwise = - lift $ - debugUnifyBottomAndReturnBottom - "Cannot unify distinct constructors." - termLike1 - termLike2 -unifyEquals _ _ = empty + debugUnifyBottomAndReturnBottom + "Cannot unify distinct constructors." + term1 + term2 + where + UnifyEqualsEndianness{end1, end2, term1, term2} = unifyData diff --git a/kore/src/Kore/Builtin/EqTerm.hs b/kore/src/Kore/Builtin/EqTerm.hs index c0bd64520a..ea21d2a075 100644 --- a/kore/src/Kore/Builtin/EqTerm.hs +++ b/kore/src/Kore/Builtin/EqTerm.hs @@ -8,11 +8,7 @@ module Kore.Builtin.EqTerm ( unifyEqTerm, ) where -import Control.Error ( - MaybeT, - ) import qualified Control.Monad as Monad -import qualified Kore.Builtin.Bool as Bool import qualified Kore.Internal.MultiOr as MultiOr import qualified Kore.Internal.OrPattern as OrPattern import Kore.Internal.Pattern ( @@ -61,16 +57,14 @@ unifyEqTerm :: TermSimplifier RewritingVariableName unifier -> NotSimplifier unifier -> EqTerm (TermLike RewritingVariableName) -> - TermLike RewritingVariableName -> - MaybeT unifier (Pattern RewritingVariableName) -unifyEqTerm unifyChildren (NotSimplifier notSimplifier) eqTerm termLike2 - | Just value2 <- Bool.matchBool termLike2 = - lift $ do - solution <- unifyChildren operand1 operand2 & OrPattern.gather - let solution' = MultiOr.map eraseTerm solution - (if value2 then pure else notSimplifier SideCondition.top) solution' - >>= Unify.scatter - | otherwise = empty + Bool -> + unifier (Pattern RewritingVariableName) +unifyEqTerm unifyChildren (NotSimplifier notSimplifier) eqTerm value = + do + solution <- unifyChildren operand1 operand2 & OrPattern.gather + let solution' = MultiOr.map eraseTerm solution + (if value then pure else notSimplifier SideCondition.top) solution' + >>= Unify.scatter where EqTerm{operand1, operand2} = eqTerm eraseTerm = Pattern.fromCondition_ . Pattern.withoutTerm diff --git a/kore/src/Kore/Builtin/Int.hs b/kore/src/Kore/Builtin/Int.hs index 8a4b0f4a05..37c91c00c1 100644 --- a/kore/src/Kore/Builtin/Int.hs +++ b/kore/src/Kore/Builtin/Int.hs @@ -435,6 +435,7 @@ matchIntEqual = data UnifyInt = UnifyInt { int1, int2 :: !InternalInt + , term1, term2 :: !(TermLike RewritingVariableName) } {- | Matches @@ -453,10 +454,10 @@ matchInt :: TermLike RewritingVariableName -> TermLike RewritingVariableName -> Maybe UnifyInt -matchInt first second - | InternalInt_ int1 <- first - , InternalInt_ int2 <- second = - Just UnifyInt{int1, int2} +matchInt term1 term2 + | InternalInt_ int1 <- term1 + , InternalInt_ int2 <- term2 = + Just UnifyInt{int1, int2, term1, term2} | otherwise = Nothing {-# INLINE matchInt #-} @@ -464,14 +465,12 @@ matchInt first second unifyInt :: forall unifier. MonadUnify unifier => - TermLike RewritingVariableName -> - TermLike RewritingVariableName -> UnifyInt -> unifier (Pattern RewritingVariableName) -unifyInt term1 term2 unifyData = +unifyInt unifyData = assert (on (==) internalIntSort int1 int2) worker where - UnifyInt{int1, int2} = unifyData + UnifyInt{int1, int2, term1, term2} = unifyData worker :: unifier (Pattern RewritingVariableName) worker | on (==) internalIntValue int1 int2 = @@ -486,8 +485,10 @@ data UnifyIntEq = UnifyIntEq {- | Matches @ -\\equals{_, _}(eqInt{_}(_, _), \\dv{Bool}(_)) +\\equals{_, _}(eqInt{_}(_, _), \\dv{Bool}(_)), @ + +symmetric in the two arguments. -} matchUnifyIntEq :: TermLike RewritingVariableName -> @@ -498,6 +499,10 @@ matchUnifyIntEq first second , isFunctionPattern first , InternalBool_ internalBool <- second = Just UnifyIntEq{eqTerm, internalBool} + | Just eqTerm <- matchIntEqual second + , isFunctionPattern second + , InternalBool_ internalBool <- first = + Just UnifyIntEq{eqTerm, internalBool} | otherwise = Nothing {-# INLINE matchUnifyIntEq #-} diff --git a/kore/src/Kore/Builtin/KEqual.hs b/kore/src/Kore/Builtin/KEqual.hs index 5580f92465..01e9ff1db6 100644 --- a/kore/src/Kore/Builtin/KEqual.hs +++ b/kore/src/Kore/Builtin/KEqual.hs @@ -20,6 +20,7 @@ module Kore.Builtin.KEqual ( unifyKequalsEq, unifyIfThenElse, matchUnifyKequalsEq, + matchIfThenElse, -- * keys eqKey, @@ -231,11 +232,6 @@ data UnifyKequalsEq = UnifyKequalsEq , internalBool :: !InternalBool } -{- | Matches two terms when second is a bool term - and the first is a function pattern matching - the @KEQUAL.eq@ hooked symbol. --} - {- | Matches @ @@ -245,8 +241,10 @@ data UnifyKequalsEq = UnifyKequalsEq and @ -\\and{_}(eq(_,_), \\dv{Bool}(_)) +\\and{_}(eq(_,_), \\dv{Bool}(_)), @ + +symmetric in the two arguments. -} matchUnifyKequalsEq :: TermLike RewritingVariableName -> @@ -257,6 +255,10 @@ matchUnifyKequalsEq first second , isFunctionPattern first , InternalBool_ internalBool <- second = Just UnifyKequalsEq{eqTerm, internalBool} + | Just eqTerm <- matchKequalEq second + , isFunctionPattern second + , InternalBool_ internalBool <- first = + Just UnifyKequalsEq{eqTerm, internalBool} | otherwise = Nothing {-# INLINE matchUnifyKequalsEq #-} @@ -276,7 +278,7 @@ unifyKequalsEq unifyChildren (NotSimplifier notSimplifier) unifyData = then pure else notSimplifier SideCondition.top scattered <- Unify.scatter solution' - return scattered{term = mkInternalBool internalBool} + return (scattered :: Pattern RewritingVariableName){term = mkInternalBool internalBool} where UnifyKequalsEq{eqTerm, internalBool} = unifyData EqTerm{operand1, operand2} = eqTerm @@ -289,43 +291,65 @@ data IfThenElse term = IfThenElse , branch1, branch2 :: !term } --- | Match the @KEQUAL.eq@ hooked symbol. -matchIfThenElse :: TermLike variable -> Maybe (IfThenElse (TermLike variable)) -matchIfThenElse (App_ symbol [condition, branch1, branch2]) = do - hook' <- (getHook . symbolHook) symbol - Monad.guard (hook' == iteKey) - return IfThenElse{symbol, condition, branch1, branch2} -matchIfThenElse _ = Nothing +data UnifyIfThenElse = UnifyIfThenElse + { ifThenElse :: IfThenElse (TermLike RewritingVariableName) + , -- The term that was not matched by @matchIfThenElse@ + term :: TermLike RewritingVariableName + } + +{- | Matches + +@ +\\and{_}(ite(_,_,_), _) +@ + +symmetric in the two arguments. +-} +matchIfThenElse :: + TermLike RewritingVariableName -> + TermLike RewritingVariableName -> + Maybe UnifyIfThenElse +matchIfThenElse first second + | Just ifThenElse <- matchITE first = + Just $ UnifyIfThenElse{ifThenElse, term = second} + | Just ifThenElse <- matchITE second = + Just $ UnifyIfThenElse{ifThenElse, term = first} + | otherwise = Nothing + where + matchITE (App_ symbol [condition, branch1, branch2]) = do + hook' <- (getHook . symbolHook) symbol + Monad.guard (hook' == iteKey) + return IfThenElse{symbol, condition, branch1, branch2} + matchITE _ = Nothing +{-# INLINE matchIfThenElse #-} unifyIfThenElse :: forall unifier. MonadUnify unifier => TermSimplifier RewritingVariableName unifier -> - TermLike RewritingVariableName -> - TermLike RewritingVariableName -> - MaybeT unifier (Pattern RewritingVariableName) -unifyIfThenElse unifyChildren a b = - worker a b <|> worker b a + UnifyIfThenElse -> + unifier (Pattern RewritingVariableName) +unifyIfThenElse unifyChildren unifyData = + worker ifThenElse term where + UnifyIfThenElse{ifThenElse, term} = unifyData takeCondition value condition' = makeCeilPredicate (mkAnd (Bool.asInternal sort value) condition') & Condition.fromPredicate where sort = termLikeSort condition' - worker termLike1 termLike2 - | Just ifThenElse <- matchIfThenElse termLike1 = - lift (takeBranch1 ifThenElse <|> takeBranch2 ifThenElse) + worker ifThenElse' second' = + takeBranch1 ifThenElse' <|> takeBranch2 ifThenElse' where takeBranch1 IfThenElse{condition, branch1} = do - solution <- unifyChildren branch1 termLike2 + solution <- unifyChildren branch1 second' let branchCondition = takeCondition True condition Pattern.andCondition solution branchCondition & simplifyCondition SideCondition.top & Logic.lowerLogicT takeBranch2 IfThenElse{condition, branch2} = do - solution <- unifyChildren branch2 termLike2 + solution <- unifyChildren branch2 second' let branchCondition = takeCondition False condition Pattern.andCondition solution branchCondition & simplifyCondition SideCondition.top & Logic.lowerLogicT - worker _ _ = empty diff --git a/kore/src/Kore/Builtin/List.hs b/kore/src/Kore/Builtin/List.hs index deada77daf..89b7aa9b8b 100644 --- a/kore/src/Kore/Builtin/List.hs +++ b/kore/src/Kore/Builtin/List.hs @@ -30,6 +30,7 @@ module Kore.Builtin.List ( isSymbolElement, isSymbolUnit, unifyEquals, + matchUnifyEqualsList, -- * keys concatKey, @@ -65,6 +66,7 @@ import qualified Data.Sequence as Seq import Data.Text ( Text, ) +import qualified Kore.Attribute.Symbol as Attribute import qualified Kore.Builtin.Bool as Bool import Kore.Builtin.Builtin ( acceptAnySort, @@ -81,6 +83,7 @@ import Kore.Internal.Pattern ( Pattern, ) import qualified Kore.Internal.Pattern as Pattern +import Kore.Internal.Symbol import Kore.Internal.TermLike ( Key, Sort, @@ -371,6 +374,95 @@ builtinFunctions = , (updateAllKey, Builtin.functionEvaluator evalUpdateAll) ] +data FirstElemVarData = FirstElemVarData + { pat1, pat2 :: !(TermLike RewritingVariableName) + , term1, term2 :: !(TermLike RewritingVariableName) + } + +data AppAppData = AppAppData + { args1, args2 :: ![TermLike RewritingVariableName] + , symbol2 :: !Symbol + , term1, term2 :: !(TermLike RewritingVariableName) + } + +data ListListData = ListListData + { builtin1, builtin2 :: !(InternalList (TermLike RewritingVariableName)) + , term1, term2 :: !(TermLike RewritingVariableName) + } + +data FramedData = FramedData + { builtin1, builtin2 :: !(InternalList (TermLike RewritingVariableName)) + , term1, term2 :: !(TermLike RewritingVariableName) + , var :: !(TermLike RewritingVariableName) + } + +data UnifyEqualsList + = FirstElemVar !FirstElemVarData + | AppApp !AppAppData + | ListList !ListListData + | FramedRight !FramedData + | FramedLeft !FramedData + | WrongArity + +{- | Matches two lists of the following patterns: + +@ +\\equals{_, _}(x, f(y)) +@ + +@ +\\equals{_, _}(concat(args1), concat(args2)) +@ + +@ +\\equals{_, _}(list1, list2) +@ + +@ +\\equals{_, _}(list1, concat(args2)) +@ + +or similarly with \\and. Symmetric in the two arguments. +-} +matchUnifyEqualsList :: + SmtMetadataTools Attribute.Symbol -> + TermLike RewritingVariableName -> + TermLike RewritingVariableName -> + Maybe UnifyEqualsList +matchUnifyEqualsList tools first second + | Just True <- isListSort tools sort1 = + worker first second normFirst normSecond <|> worker second first normSecond normFirst + | otherwise = Nothing + where + sort1 = termLikeSort first + normFirst = normalize first + normSecond = normalize second + + worker term1 term2 pat1@(ElemVar_ _) pat2 + | TermLike.isFunctionPattern pat2 = + Just $ FirstElemVar FirstElemVarData{pat1, pat2, term1, term2} + | otherwise = Nothing + worker term1 term2 (App_ symbol1 args1) (App_ symbol2 args2) + | isSymbolConcat symbol1 + , isSymbolConcat symbol2 = + Just $ AppApp AppAppData{args1, args2, symbol2, term1, term2} + worker term1 term2 (InternalList_ builtin1) pat2 = + case pat2 of + InternalList_ builtin2 -> Just $ ListList ListListData{builtin1, builtin2, term1, term2} + App_ symbol2 args2 + | isSymbolConcat symbol2 -> + case args2 of + [InternalList_ builtin2, var@(Var_ _)] -> + Just $ FramedRight FramedData{builtin1, builtin2, term1, term2, var} + [var@(Var_ _), InternalList_ builtin2] -> + Just $ FramedLeft FramedData{builtin1, builtin2, term1, term2, var} + [_, _] -> Nothing + _ -> Just WrongArity + | otherwise -> Nothing + _ -> Nothing + worker _ _ _ _ = Nothing +{-# INLINE matchUnifyEqualsList #-} + {- | Simplify the conjunction or equality of two concrete List domain values. When it is used for simplifying equality, one should separately solve the @@ -387,43 +479,17 @@ unifyEquals :: TermLike RewritingVariableName -> unifier (Pattern RewritingVariableName) ) -> - TermLike RewritingVariableName -> - TermLike RewritingVariableName -> - MaybeT unifier (Pattern RewritingVariableName) + SmtMetadataTools Attribute.Symbol -> + UnifyEqualsList -> + unifier (Pattern RewritingVariableName) unifyEquals simplifyChild - first - second = - do - tools <- Simplifier.askMetadataTools - (Monad.guard . fromMaybe False) (isListSort tools sort1) - unifyEquals0 (normalize first) (normalize second) - where - sort1 = termLikeSort first - - propagateConditions :: - InternalVariable variable => - Traversable t => - t (Conditional variable a) -> - Conditional variable (t a) - propagateConditions = sequenceA - - unifyEquals0 :: - TermLike RewritingVariableName -> - TermLike RewritingVariableName -> - MaybeT unifier (Pattern RewritingVariableName) - - unifyEquals0 pat1@(ElemVar_ _) pat2 - | TermLike.isFunctionPattern pat2 = - lift $ simplifyChild pat1 pat2 - | otherwise = empty - unifyEquals0 pat1 pat2@(ElemVar_ _) - | TermLike.isFunctionPattern pat1 = - lift $ simplifyChild pat1 pat2 - | otherwise = empty - unifyEquals0 (App_ symbol1 args1) (App_ symbol2 args2) - | isSymbolConcat symbol1 - , isSymbolConcat symbol2 = + tools + unifyData = + case unifyData of + FirstElemVar FirstElemVarData{pat1, pat2} -> + simplifyChild pat1 pat2 + AppApp AppAppData{args1, args2, symbol2, term1, term2} -> case (args1, args2) of ( [InternalList_ builtin1, x1@(Var_ _)] , [InternalList_ builtin2, x2@(Var_ _)] @@ -434,7 +500,8 @@ unifyEquals x1 builtin2 x2 - & lift + term1 + term2 ( [x1@(Var_ _), InternalList_ builtin1] , [x2@(Var_ _), InternalList_ builtin2] ) -> @@ -444,36 +511,33 @@ unifyEquals builtin1 x2 builtin2 - & lift + term1 + term2 _ -> empty - unifyEquals0 (InternalList_ builtin1) pat2 = - case pat2 of - InternalList_ builtin2 -> - lift $ unifyEqualsConcrete builtin1 builtin2 - (App_ symbol2 args2) - | isSymbolConcat symbol2 -> - case args2 of - [InternalList_ builtin2, x@(Var_ _)] -> - unifyEqualsFramedRight builtin1 builtin2 x & lift - [x@(Var_ _), InternalList_ builtin2] -> - unifyEqualsFramedLeft builtin1 x builtin2 & lift - [_, _] -> empty - _ -> Builtin.wrongArity concatKey - | otherwise -> empty - _ -> empty - unifyEquals0 pat1 pat2 = - case pat2 of - dv@(InternalList_ _) -> unifyEquals0 dv pat1 - _ -> empty + ListList ListListData{builtin1, builtin2, term1, term2} -> + unifyEqualsConcrete builtin1 builtin2 term1 term2 + FramedRight FramedData{builtin1, builtin2, term1, term2, var} -> + unifyEqualsFramedRight builtin1 builtin2 var term1 term2 + FramedLeft FramedData{builtin1, builtin2, term1, term2, var} -> + unifyEqualsFramedLeft builtin1 var builtin2 term1 term2 + WrongArity -> Builtin.wrongArity concatKey + where + propagateConditions :: + InternalVariable variable => + Traversable t => + t (Conditional variable a) -> + Conditional variable (t a) + propagateConditions = sequenceA unifyEqualsConcrete :: InternalList (TermLike RewritingVariableName) -> InternalList (TermLike RewritingVariableName) -> + TermLike RewritingVariableName -> + TermLike RewritingVariableName -> unifier (Pattern RewritingVariableName) - unifyEqualsConcrete builtin1 builtin2 - | Seq.length list1 /= Seq.length list2 = bottomWithExplanation + unifyEqualsConcrete builtin1 builtin2 term1 term2 + | Seq.length list1 /= Seq.length list2 = bottomWithExplanation term1 term2 | otherwise = do - tools <- Simplifier.askMetadataTools Reflection.give tools $ do unified <- sequence $ Seq.zipWith simplifyChild list1 list2 let propagatedUnified = propagateConditions unified @@ -491,20 +555,25 @@ unifyEquals InternalList (TermLike RewritingVariableName) -> InternalList (TermLike RewritingVariableName) -> TermLike RewritingVariableName -> + TermLike RewritingVariableName -> + TermLike RewritingVariableName -> unifier (Pattern RewritingVariableName) unifyEqualsFramedRight internal1 internal2 frame2 - | Seq.length prefix2 > Seq.length list1 = bottomWithExplanation + term1 + term2 + | Seq.length prefix2 > Seq.length list1 = bottomWithExplanation term1 term2 | otherwise = do - tools <- Simplifier.askMetadataTools let listSuffix1 = asInternal tools internalListSort suffix1 prefixUnified <- unifyEqualsConcrete internal1{internalListChild = prefix1} internal2 + term1 + term2 suffixUnified <- simplifyChild frame2 listSuffix1 let result = TermLike.markSimplified (mkInternalList internal1) @@ -523,21 +592,26 @@ unifyEquals InternalList (TermLike RewritingVariableName) -> TermLike RewritingVariableName -> InternalList (TermLike RewritingVariableName) -> + TermLike RewritingVariableName -> + TermLike RewritingVariableName -> unifier (Pattern RewritingVariableName) unifyEqualsFramedLeft internal1 frame2 internal2 - | Seq.length suffix2 > Seq.length list1 = bottomWithExplanation + term1 + term2 + | Seq.length suffix2 > Seq.length list1 = bottomWithExplanation term1 term2 | otherwise = do - tools <- Simplifier.askMetadataTools let listPrefix1 = asInternal tools internalListSort prefix1 prefixUnified <- simplifyChild frame2 listPrefix1 suffixUnified <- unifyEqualsConcrete internal1{internalListChild = suffix1} internal2 + term1 + term2 let result = mkInternalList internal1 <$ prefixUnified @@ -550,11 +624,11 @@ unifyEquals (prefix1, suffix1) = Seq.splitAt prefixLength list1 where prefixLength = Seq.length list1 - Seq.length suffix2 - bottomWithExplanation = do + bottomWithExplanation term1 term2 = do debugUnifyBottom "Cannot unify lists of different length." - first - second + term1 + term2 return Pattern.bottom unifyEqualsFramedRightRight :: @@ -563,6 +637,8 @@ unifyEquals TermLike RewritingVariableName -> InternalList (TermLike RewritingVariableName) -> TermLike RewritingVariableName -> + TermLike RewritingVariableName -> + TermLike RewritingVariableName -> unifier (Pattern RewritingVariableName) unifyEqualsFramedRightRight symbol @@ -570,12 +646,15 @@ unifyEquals frame1 internal2 frame2 + term1 + term2 | length1 < length2 = do - tools <- Simplifier.askMetadataTools prefixUnified <- unifyEqualsConcrete internal1 internal2{internalListChild = prefix2} + term1 + term2 let listSuffix2 = asInternal tools internalListSort suffix2 suffix2Frame2 = mkApplySymbol symbol [listSuffix2, frame2] suffixUnified <- @@ -589,7 +668,7 @@ unifyEquals return result | length1 == length2 = do prefixUnified <- - unifyEqualsConcrete internal1 internal2 + unifyEqualsConcrete internal1 internal2 term1 term2 suffixUnified <- simplifyChild frame1 frame2 let result = TermLike.markSimplified initial @@ -597,7 +676,7 @@ unifyEquals <* suffixUnified return result | otherwise = - unifyEqualsFramedRightRight symbol internal2 frame2 internal1 frame1 + unifyEqualsFramedRightRight symbol internal2 frame2 internal1 frame1 term1 term2 where initial = mkApplySymbol symbol [mkInternalList internal1, frame1] InternalList{internalListSort} = internal1 @@ -613,6 +692,8 @@ unifyEquals InternalList (TermLike RewritingVariableName) -> TermLike RewritingVariableName -> InternalList (TermLike RewritingVariableName) -> + TermLike RewritingVariableName -> + TermLike RewritingVariableName -> unifier (Pattern RewritingVariableName) unifyEqualsFramedLeftLeft symbol @@ -620,8 +701,9 @@ unifyEquals internal1 frame2 internal2 + term1 + term2 | length1 < length2 = do - tools <- Simplifier.askMetadataTools let listPrefix2 = asInternal tools internalListSort prefix2 frame2Prefix2 = mkApplySymbol symbol [frame2, listPrefix2] prefixUnified <- simplifyChild frame1 frame2Prefix2 @@ -629,19 +711,21 @@ unifyEquals unifyEqualsConcrete internal1 internal2{internalListChild = suffix2} + term1 + term2 let result = TermLike.markSimplified initial <$ prefixUnified <* suffixUnified return result | length1 == length2 = do prefixUnified <- simplifyChild frame1 frame2 - suffixUnified <- unifyEqualsConcrete internal1 internal2 + suffixUnified <- unifyEqualsConcrete internal1 internal2 term1 term2 let result = TermLike.markSimplified initial <$ prefixUnified <* suffixUnified return result | otherwise = - unifyEqualsFramedLeftLeft symbol frame2 internal2 frame1 internal1 + unifyEqualsFramedLeftLeft symbol frame2 internal2 frame1 internal1 term1 term2 where initial = mkApplySymbol symbol [frame1, mkInternalList internal1] InternalList{internalListSort} = internal1 diff --git a/kore/src/Kore/Builtin/Map.hs b/kore/src/Kore/Builtin/Map.hs index 2482f03c4b..62d32be10b 100644 --- a/kore/src/Kore/Builtin/Map.hs +++ b/kore/src/Kore/Builtin/Map.hs @@ -21,6 +21,8 @@ module Kore.Builtin.Map ( -- * Unification unifyEquals, unifyNotInKeys, + matchUnifyNotInKeys, + matchUnifyEquals, -- * Raw evaluators evalConcat, @@ -30,9 +32,8 @@ module Kore.Builtin.Map ( ) where import Control.Error ( - MaybeT (MaybeT), + MaybeT, hoistMaybe, - runMaybeT, ) import qualified Control.Monad as Monad import Data.HashMap.Strict ( @@ -112,7 +113,6 @@ import Kore.Syntax.Sentence ( import Kore.Unification.Unify ( MonadUnify, ) -import qualified Kore.Unification.Unify as Monad.Unify import qualified Kore.Unification.Unify as Unify import Prelude.Kore @@ -521,69 +521,84 @@ internalize tools termLike where sort' = termLikeSort termLike -{- | Simplify the conjunction or equality of two concrete Map domain values. +data NormAcData = NormAcData + { normalized1, normalized2 :: !(InternalMap Key (TermLike RewritingVariableName)) + , term1, term2 :: !(TermLike RewritingVariableName) + , acData :: !(Ac.UnifyEqualsNormAc NormalizedMap RewritingVariableName) + } -When it is used for simplifying equality, one should separately solve the -case ⊥ = ⊥. One should also throw away the term in the returned pattern. +data UnifyEqualsMap + = ReturnBottom !(TermLike RewritingVariableName) !(TermLike RewritingVariableName) + | NormAc !NormAcData -The maps are assumed to have the same sort, but this is not checked. If -multiple sorts are hooked to the same builtin domain, the verifier should -reject the definition. --} -unifyEquals :: - forall unifier. - MonadUnify unifier => - TermSimplifier RewritingVariableName unifier -> +-- | Matches two concrete Map domain values. +matchUnifyEquals :: + SmtMetadataTools Attribute.Symbol -> TermLike RewritingVariableName -> TermLike RewritingVariableName -> - MaybeT unifier (Pattern RewritingVariableName) -unifyEquals unifyEqualsChildren first second = do - tools <- Simplifier.askMetadataTools - (Monad.guard . fromMaybe False) (isMapSort tools sort1) - MaybeT $ do - unifiers <- Monad.Unify.gather (runMaybeT (unifyEquals0 first second)) - case sequence unifiers of - Nothing -> return Nothing - Just us -> Monad.Unify.scatter (map Just us) + Maybe UnifyEqualsMap +matchUnifyEquals tools first second + | Just True <- isMapSort tools sort1 = + worker first second True <|> worker second first False + | otherwise = Nothing where sort1 = termLikeSort first - unifyEquals0 :: - TermLike RewritingVariableName -> + normalizedOrBottom :: TermLike RewritingVariableName -> - MaybeT unifier (Pattern RewritingVariableName) - unifyEquals0 (InternalMap_ normalized1) (InternalMap_ normalized2) = do - tools <- Simplifier.askMetadataTools - Ac.unifyEqualsNormalized - tools - first - second - unifyEqualsChildren - normalized1 - normalized2 - unifyEquals0 pat1 pat2 = do - firstDomain <- asDomain pat1 - secondDomain <- asDomain pat2 - unifyEquals0 firstDomain secondDomain + Ac.NormalizedOrBottom NormalizedMap RewritingVariableName + normalizedOrBottom = Ac.toNormalized + + worker a b isFirstMatched + | InternalMap_ normalized1 <- a + , InternalMap_ normalized2 <- b = + NormAc . NormAcData normalized1 normalized2 term1 term2 + <$> Ac.matchUnifyEqualsNormalizedAc + tools + normalized1 + normalized2 + | otherwise = case normalizedOrBottom a of + Ac.Bottom -> Just $ ReturnBottom term1 term2 + Ac.Normalized normalized1 -> + let a' = Ac.asInternal tools sort1 normalized1 + in case normalizedOrBottom b of + Ac.Bottom -> Just $ ReturnBottom term1 term2 + Ac.Normalized normalized2 -> + let b' = Ac.asInternal tools sort1 normalized2 + in worker a' b' isFirstMatched where - asDomain :: - TermLike RewritingVariableName -> - MaybeT unifier (TermLike RewritingVariableName) - asDomain patt = - case normalizedOrBottom of - Ac.Normalized normalized -> do - tools <- Simplifier.askMetadataTools - return (Ac.asInternal tools sort1 normalized) - Ac.Bottom -> - lift $ - debugUnifyBottomAndReturnBottom - "Duplicated elements in normalization." - first - second + (term1, term2) = if isFirstMatched then (a, b) else (b, a) + +{- | Simplify the conjunction or equality of two concrete Map domain values. + +When it is used for simplifying equality, one should separately solve the +case ⊥ = ⊥. One should also throw away the term in the returned pattern. +-} +unifyEquals :: + forall unifier. + MonadUnify unifier => + TermSimplifier RewritingVariableName unifier -> + SmtMetadataTools Attribute.Symbol -> + UnifyEqualsMap -> + unifier (Pattern RewritingVariableName) +unifyEquals unifyEqualsChildren tools unifyData = + case unifyData of + ReturnBottom term1 term2 -> + debugUnifyBottomAndReturnBottom + "Duplicated elements in normalization." + term1 + term2 + NormAc unifyData' -> + Ac.unifyEqualsNormalized + tools + term1 + term2 + unifyEqualsChildren + normalized1 + normalized2 + acData where - normalizedOrBottom :: - Ac.NormalizedOrBottom NormalizedMap RewritingVariableName - normalizedOrBottom = Ac.toNormalized patt + NormAcData{normalized1, normalized2, term1, term2, acData} = unifyData' data InKeys term = InKeys { symbol :: !Symbol @@ -609,30 +624,130 @@ matchInKeys :: Maybe (InKeys (TermLike variable)) matchInKeys = retract -unifyNotInKeys :: - forall unifier. - MonadUnify unifier => - TermSimplifier RewritingVariableName unifier -> - NotSimplifier unifier -> +data UnifyNotInKeys = UnifyNotInKeys + { inKeys :: !(InKeys (TermLike RewritingVariableName)) + , concreteKeys, mapKeys, opaqueElements :: ![TermLike RewritingVariableName] + , term :: !(TermLike RewritingVariableName) + } + +data UnifyNotInKeysResult + = NullKeysNullOpaques + | NonNullKeysOrMultipleOpaques !UnifyNotInKeys + +{- | Matches + +@ +\\equals{_, _}(\\dv{Bool}(false), inKeys(map, key)) +@ + +when @key@ does not belong to the keys of @map@. Symmetric in the two arguments. +-} +matchUnifyNotInKeys :: TermLike RewritingVariableName -> TermLike RewritingVariableName -> - MaybeT unifier (Pattern RewritingVariableName) -unifyNotInKeys unifyChildren (NotSimplifier notSimplifier) a b = - worker a b <|> worker b a + Maybe UnifyNotInKeysResult +matchUnifyNotInKeys first second + | Just False <- Bool.matchBool first + , Just inKeys@InKeys{mapTerm} <- matchInKeys second + , Ac.Normalized normalizedMap <- normalizedOrBottom mapTerm = + let symbolicKeys = getSymbolicKeysOfAc normalizedMap + concreteKeys = from @Key <$> getConcreteKeysOfAc normalizedMap + mapKeys = symbolicKeys <> concreteKeys + opaqueElements = opaque . unwrapAc $ normalizedMap + unifyData = + NonNullKeysOrMultipleOpaques + UnifyNotInKeys + { inKeys + , concreteKeys + , mapKeys + , opaqueElements + , term = first + } + in case (mapKeys, opaqueElements) of + -- null mapKeys && null opaqueElements + ([], []) -> Just NullKeysNullOpaques + -- (not (null mapKeys) || (length opaqueElements > 1)) + (_ : _, _) -> Just unifyData + (_, _ : _ : _) -> Just unifyData + -- otherwise + _ -> Nothing + | Just False <- Bool.matchBool second + , Just inKeys@InKeys{mapTerm} <- matchInKeys first + , Ac.Normalized normalizedMap <- normalizedOrBottom mapTerm = + let symbolicKeys = getSymbolicKeysOfAc normalizedMap + concreteKeys = from @Key <$> getConcreteKeysOfAc normalizedMap + mapKeys = symbolicKeys <> concreteKeys + opaqueElements = opaque . unwrapAc $ normalizedMap + unifyData = + NonNullKeysOrMultipleOpaques + UnifyNotInKeys + { inKeys + , concreteKeys + , mapKeys + , opaqueElements + , term = second + } + in case (mapKeys, opaqueElements) of + -- null mapKeys && null opaqueElements + ([], []) -> Just NullKeysNullOpaques + -- (not (null mapKeys) || (length opaqueElements > 1)) + (_ : _, _) -> Just unifyData + (_, _ : _ : _) -> Just unifyData + -- otherwise + _ -> Nothing + | otherwise = Nothing where normalizedOrBottom :: InternalVariable variable => TermLike variable -> Ac.NormalizedOrBottom NormalizedMap variable normalizedOrBottom = Ac.toNormalized +{-# INLINE matchUnifyNotInKeys #-} +unifyNotInKeys :: + forall unifier. + MonadUnify unifier => + TermSimplifier RewritingVariableName unifier -> + NotSimplifier unifier -> + UnifyNotInKeysResult -> + unifier (Pattern RewritingVariableName) +unifyNotInKeys unifyChildren (NotSimplifier notSimplifier) unifyData = + case unifyData of + NullKeysNullOpaques -> return Pattern.top + NonNullKeysOrMultipleOpaques unifyData' -> + do + -- Concrete keys are constructor-like, therefore they are defined + TermLike.assertConstructorLikeKeys concreteKeys $ return () + definedKey <- defineTerm keyTerm + definedMap <- defineTerm mapTerm + keyConditions <- traverse (unifyAndNegate keyTerm) mapKeys + + let keyInKeysOpaque = + (\term' -> inject @(TermLike _) (inKeys :: InKeys (TermLike RewritingVariableName)){mapTerm = term'}) + <$> opaqueElements + + opaqueConditions <- + traverse (unifyChildren term) keyInKeysOpaque + let conditions = + fmap Pattern.withoutTerm (keyConditions <> opaqueConditions) + <> [definedKey, definedMap] + return $ collectConditions conditions + where + UnifyNotInKeys + { inKeys + , concreteKeys + , mapKeys + , opaqueElements + , term + } = unifyData' + InKeys{keyTerm, mapTerm} = inKeys + where defineTerm :: TermLike RewritingVariableName -> - MaybeT unifier (Condition RewritingVariableName) - defineTerm termLike = - makeEvaluateTermCeil SideCondition.topTODO termLike + unifier (Condition RewritingVariableName) + defineTerm term = + makeEvaluateTermCeil SideCondition.topTODO term >>= Unify.scatter - & lift eraseTerm = Pattern.fromCondition_ . Pattern.withoutTerm @@ -650,39 +765,3 @@ unifyNotInKeys unifyChildren (NotSimplifier notSimplifier) a b = >>= Unify.scatter collectConditions terms = fold terms & Pattern.fromCondition_ - - worker :: - TermLike RewritingVariableName -> - TermLike RewritingVariableName -> - MaybeT unifier (Pattern RewritingVariableName) - worker termLike1 termLike2 - | Just boolValue <- Bool.matchBool termLike1 - , not boolValue - , Just inKeys@InKeys{keyTerm, mapTerm} <- matchInKeys termLike2 - , Ac.Normalized normalizedMap <- normalizedOrBottom mapTerm = - do - let symbolicKeys = getSymbolicKeysOfAc normalizedMap - concreteKeys = from @Key <$> getConcreteKeysOfAc normalizedMap - mapKeys = symbolicKeys <> concreteKeys - opaqueElements = opaque . unwrapAc $ normalizedMap - if null mapKeys && null opaqueElements - then return Pattern.top - else do - Monad.guard (not (null mapKeys) || (length opaqueElements > 1)) - -- Concrete keys are constructor-like, therefore they are defined - TermLike.assertConstructorLikeKeys concreteKeys $ return () - definedKey <- defineTerm keyTerm - definedMap <- defineTerm mapTerm - keyConditions <- lift $ traverse (unifyAndNegate keyTerm) mapKeys - - let keyInKeysOpaque = - (\term -> inject @(TermLike _) inKeys{mapTerm = term}) - <$> opaqueElements - - opaqueConditions <- - lift $ traverse (unifyChildren termLike1) keyInKeysOpaque - let conditions = - fmap Pattern.withoutTerm (keyConditions <> opaqueConditions) - <> [definedKey, definedMap] - return $ collectConditions conditions - worker _ _ = empty diff --git a/kore/src/Kore/Builtin/Set.hs b/kore/src/Kore/Builtin/Set.hs index 01c6881f1d..de013bd41d 100644 --- a/kore/src/Kore/Builtin/Set.hs +++ b/kore/src/Kore/Builtin/Set.hs @@ -29,12 +29,12 @@ module Kore.Builtin.Set ( -- * Unification unifyEquals, + matchUnifyEquals, ) where import Control.Error ( - MaybeT (MaybeT), + MaybeT, hoistMaybe, - runMaybeT, ) import qualified Control.Monad as Monad import Data.HashMap.Strict ( @@ -114,7 +114,6 @@ import qualified Kore.Syntax.Sentence as Sentence.DoNotUse ( import Kore.Unification.Unify ( MonadUnify, ) -import qualified Kore.Unification.Unify as Monad.Unify import Prelude.Kore -- | Builtin name of the @Set@ sort. @@ -526,73 +525,85 @@ internalize tools termLike where sort' = termLikeSort termLike -{- | Simplify the conjunction or equality of two concrete Set domain values. +data NormAcData = NormAcData + { normalized1, normalized2 :: !(InternalSet Key (TermLike RewritingVariableName)) + , term1, term2 :: !(TermLike RewritingVariableName) + , acData :: !(Ac.UnifyEqualsNormAc NormalizedSet RewritingVariableName) + } - When it is used for simplifying equality, one should separately solve the - case ⊥ = ⊥. One should also throw away the term in the returned pattern. +data UnifyEqualsMap + = ReturnBottom !(TermLike RewritingVariableName) !(TermLike RewritingVariableName) + | NormAc !NormAcData - The sets are assumed to have the same sort, but this is not checked. If - multiple sorts are hooked to the same builtin domain, the verifier should - reject the definition. +-- | Matches two concrete Set domain values. +matchUnifyEquals :: + SmtMetadataTools Attribute.Symbol -> + TermLike RewritingVariableName -> + TermLike RewritingVariableName -> + Maybe UnifyEqualsMap +matchUnifyEquals tools first second + | Just True <- isSetSort tools sort1 = + worker first second True <|> worker second first False + | otherwise = Nothing + where + sort1 = termLikeSort first + + normalizedOrBottom :: + TermLike RewritingVariableName -> + Ac.NormalizedOrBottom NormalizedSet RewritingVariableName + normalizedOrBottom = Ac.toNormalized + + worker a b isFirstMatched + | InternalSet_ normalized1 <- a + , InternalSet_ normalized2 <- b = + NormAc . NormAcData normalized1 normalized2 term1 term2 + <$> Ac.matchUnifyEqualsNormalizedAc + tools + normalized1 + normalized2 + | otherwise = case normalizedOrBottom a of + Ac.Bottom -> Just $ ReturnBottom term1 term2 + Ac.Normalized normalized1 -> + let a' = Ac.asInternal tools sort1 normalized1 + in case normalizedOrBottom b of + Ac.Bottom -> Just $ ReturnBottom term1 term2 + Ac.Normalized normalized2 -> + let b' = Ac.asInternal tools sort1 normalized2 + in worker a' b' isFirstMatched + where + (term1, term2) = if isFirstMatched then (a, b) else (b, a) + +{- | Simplify the conjunction or equality of two concrete Map domain values. + +When it is used for simplifying equality, one should separately solve the +case ⊥ = ⊥. One should also throw away the term in the returned pattern. + +The maps are assumed to have the same sort, but this is not checked. If +multiple sorts are hooked to the same builtin domain, the verifier should +reject the definition. -} unifyEquals :: forall unifier. MonadUnify unifier => - ( TermLike RewritingVariableName -> - TermLike RewritingVariableName -> - unifier (Pattern RewritingVariableName) - ) -> - TermLike RewritingVariableName -> - TermLike RewritingVariableName -> - MaybeT unifier (Pattern RewritingVariableName) -unifyEquals - unifyEqualsChildren - first - second = - do - tools <- Simplifier.askMetadataTools - (Monad.guard . fromMaybe False) (isSetSort tools sort1) - MaybeT $ do - unifiers <- Monad.Unify.gather (runMaybeT (unifyEquals0 first second)) - case sequence unifiers of - Nothing -> return Nothing - Just us -> Monad.Unify.scatter (map Just us) - where - sort1 = termLikeSort first - - unifyEquals0 :: - TermLike RewritingVariableName -> - TermLike RewritingVariableName -> - MaybeT unifier (Pattern RewritingVariableName) - unifyEquals0 (InternalSet_ normalized1) (InternalSet_ normalized2) = do - tools <- Simplifier.askMetadataTools + TermSimplifier RewritingVariableName unifier -> + SmtMetadataTools Attribute.Symbol -> + UnifyEqualsMap -> + unifier (Pattern RewritingVariableName) +unifyEquals unifyEqualsChildren tools unifyData = + case unifyData of + ReturnBottom term1 term2 -> + debugUnifyBottomAndReturnBottom + "Duplicated elements in normalization." + term1 + term2 + NormAc unifyData' -> Ac.unifyEqualsNormalized tools - first - second + term1 + term2 unifyEqualsChildren normalized1 normalized2 - unifyEquals0 pat1 pat2 = do - firstDomain <- asDomain pat1 - secondDomain <- asDomain pat2 - unifyEquals0 firstDomain secondDomain + acData where - asDomain :: - TermLike RewritingVariableName -> - MaybeT unifier (TermLike RewritingVariableName) - asDomain patt = - case normalizedOrBottom of - Ac.Normalized normalized -> do - tools <- Simplifier.askMetadataTools - return (Ac.asInternal tools sort1 normalized) - Ac.Bottom -> - lift $ - debugUnifyBottomAndReturnBottom - "Duplicated elements in normalization." - first - second - where - normalizedOrBottom :: - Ac.NormalizedOrBottom NormalizedSet RewritingVariableName - normalizedOrBottom = Ac.toNormalized patt + NormAcData{normalized1, normalized2, term1, term2, acData} = unifyData' diff --git a/kore/src/Kore/Builtin/Signedness.hs b/kore/src/Kore/Builtin/Signedness.hs index e74ee69494..65984f4c27 100644 --- a/kore/src/Kore/Builtin/Signedness.hs +++ b/kore/src/Kore/Builtin/Signedness.hs @@ -7,12 +7,10 @@ module Kore.Builtin.Signedness ( signedKey, unsignedKey, unifyEquals, + matchUnifyEqualsSignedness, module Kore.Builtin.Signedness.Signedness, ) where -import Control.Error ( - MaybeT, - ) import Data.Functor.Const import qualified Data.HashMap.Strict as HashMap import Data.String ( @@ -31,6 +29,7 @@ import Kore.Internal.TermLike import Kore.Log.DebugUnifyBottom ( debugUnifyBottomAndReturnBottom, ) +import Kore.Rewrite.RewritingVariable import Kore.Unification.Unify ( MonadUnify, ) @@ -77,18 +76,33 @@ signedVerifier = signednessVerifier Signed unsignedVerifier :: ApplicationVerifier Verified.Pattern unsignedVerifier = signednessVerifier Unsigned +data UnifyEqualsSignedness = UnifyEqualsSignedness + { sign1, sign2 :: !Signedness + , term1, term2 :: !(TermLike RewritingVariableName) + } + +-- | Matches two terms having the Signedness constructor. +matchUnifyEqualsSignedness :: + TermLike RewritingVariableName -> + TermLike RewritingVariableName -> + Maybe UnifyEqualsSignedness +matchUnifyEqualsSignedness term1 term2 + | Signedness_ sign1 <- term1 + , Signedness_ sign2 <- term2 = + Just UnifyEqualsSignedness{sign1, sign2, term1, term2} + | otherwise = Nothing +{-# INLINE matchUnifyEqualsSignedness #-} + unifyEquals :: - InternalVariable variable => MonadUnify unifier => - TermLike variable -> - TermLike variable -> - MaybeT unifier (Pattern variable) -unifyEquals termLike1@(Signedness_ sign1) termLike2@(Signedness_ sign2) - | sign1 == sign2 = return (Pattern.fromTermLike termLike1) + UnifyEqualsSignedness -> + unifier (Pattern RewritingVariableName) +unifyEquals unifyData + | sign1 == sign2 = return (Pattern.fromTermLike term1) | otherwise = - lift $ - debugUnifyBottomAndReturnBottom - "Cannot unify distinct constructors." - termLike1 - termLike2 -unifyEquals _ _ = empty + debugUnifyBottomAndReturnBottom + "Cannot unify distinct constructors." + term1 + term2 + where + UnifyEqualsSignedness{sign1, sign2, term1, term2} = unifyData diff --git a/kore/src/Kore/Builtin/String.hs b/kore/src/Kore/Builtin/String.hs index a4dca7a3ea..ca84bee763 100644 --- a/kore/src/Kore/Builtin/String.hs +++ b/kore/src/Kore/Builtin/String.hs @@ -485,6 +485,7 @@ matchStringEqual = data UnifyString = UnifyString { string1, string2 :: !InternalString + , term1, term2 :: !(TermLike RewritingVariableName) } {- | Matches @@ -503,10 +504,10 @@ matchString :: TermLike RewritingVariableName -> TermLike RewritingVariableName -> Maybe UnifyString -matchString first second - | InternalString_ string1 <- first - , InternalString_ string2 <- second = - Just UnifyString{string1, string2} +matchString term1 term2 + | InternalString_ string1 <- term1 + , InternalString_ string2 <- term2 = + Just UnifyString{string1, string2, term1, term2} | otherwise = Nothing {-# INLINE matchString #-} @@ -514,26 +515,31 @@ matchString first second unifyString :: forall unifier. MonadUnify unifier => - TermLike RewritingVariableName -> - TermLike RewritingVariableName -> UnifyString -> unifier (Pattern RewritingVariableName) -unifyString term1 term2 unifyData = +unifyString unifyData = assert (on (==) internalStringSort string1 string2) worker where worker :: unifier (Pattern RewritingVariableName) worker | on (==) internalStringValue string1 string2 = return $ Pattern.fromTermLike term1 - | otherwise = - debugUnifyBottomAndReturnBottom "distinct strings" term1 term2 - UnifyString{string1, string2} = unifyData + | otherwise = debugUnifyBottomAndReturnBottom "distinct strings" term1 term2 + UnifyString{string1, string2, term1, term2} = unifyData data UnifyStringEq = UnifyStringEq { eqTerm :: !(EqTerm (TermLike RewritingVariableName)) , internalBool :: !InternalBool } +{- | Matches + +@ +\\equals{_, _}(\\dv{Bool}(_), eqString{_}(_,_)), +@ + +symmetric in the two arguments. +-} matchUnifyStringEq :: TermLike RewritingVariableName -> TermLike RewritingVariableName -> @@ -543,6 +549,10 @@ matchUnifyStringEq first second , isFunctionPattern first , InternalBool_ internalBool <- second = Just UnifyStringEq{eqTerm, internalBool} + | Just eqTerm <- matchStringEqual second + , isFunctionPattern second + , InternalBool_ internalBool <- first = + Just UnifyStringEq{eqTerm, internalBool} | otherwise = Nothing {-# INLINE matchUnifyStringEq #-} diff --git a/kore/src/Kore/Simplify/AndTerms.hs b/kore/src/Kore/Simplify/AndTerms.hs index e9a9a9026f..7fe6f8830e 100644 --- a/kore/src/Kore/Simplify/AndTerms.hs +++ b/kore/src/Kore/Simplify/AndTerms.hs @@ -10,7 +10,9 @@ module Kore.Simplify.AndTerms ( TermTransformationOld, cannotUnifyDistinctDomainValues, functionAnd, + matchFunctionAnd, compareForEquals, + FunctionAnd (..), ) where import Control.Error ( @@ -75,13 +77,13 @@ import Kore.Simplify.ExpandAlias import Kore.Simplify.InjSimplifier import Kore.Simplify.NoConfusion import Kore.Simplify.NotSimplifier -import Kore.Simplify.OverloadSimplifier as OverloadSimplifier import Kore.Simplify.Overloading as Overloading import Kore.Simplify.Simplify as Simplifier import Kore.Unification.Unify as Unify import Kore.Unparser import Pair import Prelude.Kore +import qualified Pretty {- | Unify two terms without discarding the terms. @@ -112,13 +114,13 @@ termUnification notSimplifier = \term1 term2 -> TermLike RewritingVariableName -> TermLike RewritingVariableName -> unifier (Pattern RewritingVariableName) - termUnificationWorker pat1 pat2 = do + termUnificationWorker term1 term2 = do let maybeTermUnification :: MaybeT unifier (Pattern RewritingVariableName) maybeTermUnification = - maybeTermAnd notSimplifier termUnificationWorker pat1 pat2 + maybeTermAnd notSimplifier termUnificationWorker term1 term2 Error.maybeT - (incompleteUnificationPattern pat1 pat2) + (incompleteUnificationPattern term1 term2) pure maybeTermUnification @@ -139,79 +141,70 @@ maybeTermEquals :: MaybeT unifier (Pattern RewritingVariableName) maybeTermEquals notSimplifier childTransformers first second = do injSimplifier <- Simplifier.askInjSimplifier - OverloadSimplifier{isOverloaded} <- Simplifier.askOverloadSimplifier - worker injSimplifier isOverloaded + overloadSimplifier <- Simplifier.askOverloadSimplifier + tools <- Simplifier.askMetadataTools + worker injSimplifier overloadSimplifier tools where - worker injSimplifier isOverloaded + worker injSimplifier overloadSimplifier tools | Just unifyData <- Builtin.Int.matchInt first second = - lift $ Builtin.Int.unifyInt first second unifyData + lift $ Builtin.Int.unifyInt unifyData | Just unifyData <- Builtin.Bool.matchBools first second = - lift $ Builtin.Bool.unifyBool first second unifyData + lift $ Builtin.Bool.unifyBool unifyData | Just unifyData <- Builtin.String.matchString first second = - lift $ Builtin.String.unifyString first second unifyData + lift $ Builtin.String.unifyString unifyData | Just unifyData <- matchDomainValue first second = - lift $ unifyDomainValue first second unifyData + lift $ unifyDomainValue unifyData | Just unifyData <- matchStringLiteral first second = - lift $ unifyStringLiteral first second unifyData - | Just () <- matchEqualsAndEquals first second = - lift $ equalAndEquals first + lift $ unifyStringLiteral unifyData + | Just term <- matchEqualsAndEquals first second = + lift $ equalAndEquals term | Just unifyData <- matchBytes first second = lift $ unifyBytes unifyData - | Just () <- matchBottomTermEquals first = - lift $ bottomTermEquals SideCondition.topTODO first second - | Just () <- matchBottomTermEquals second = - lift $ bottomTermEquals SideCondition.topTODO second first - | Just var <- matchVariableFunctionEquals first second = - lift $ variableFunctionEquals first second var - | Just var <- matchVariableFunctionEquals second first = - lift $ variableFunctionEquals second first var + | Just unifyData <- matchBottomTermEquals first second = + lift $ bottomTermEquals SideCondition.topTODO unifyData + | Just unifyData <- matchVariableFunctionEquals first second = + lift $ variableFunctionEquals unifyData | Just unifyData <- matchEqualInjectiveHeadsAndEquals first second = lift $ equalInjectiveHeadsAndEquals childTransformers unifyData | Just unifyData <- matchInj injSimplifier first second = - lift $ unifySortInjection childTransformers first second unifyData - | Just () <- matchConstructorSortInjectionAndEquals first second = - lift $ constructorSortInjectionAndEquals first second - | Just () <- matchDifferentConstructors isOverloaded first second = - lift $ constructorAndEqualsAssumesDifferentHeads first second - | otherwise = - overloadedConstructorSortInjectionAndEquals childTransformers first second - <|> rest - - rest - | Just boolAndData <- Builtin.Bool.matchUnifyBoolAnd first second = - lift $ Builtin.Bool.unifyBoolAnd childTransformers first boolAndData - | Just boolAndData <- Builtin.Bool.matchUnifyBoolAnd second first = - lift $ Builtin.Bool.unifyBoolAnd childTransformers second boolAndData - | Just boolOrData <- Builtin.Bool.matchUnifyBoolOr first second = - lift $ Builtin.Bool.unifyBoolOr childTransformers first boolOrData - | Just boolOrData <- Builtin.Bool.matchUnifyBoolOr second first = - lift $ Builtin.Bool.unifyBoolOr childTransformers second boolOrData + lift $ unifySortInjection childTransformers unifyData + | Just unifyData <- matchConstructorSortInjectionAndEquals first second = + lift $ constructorSortInjectionAndEquals unifyData + | Just unifyData <- matchDifferentConstructors overloadSimplifier first second = + lift $ constructorAndEqualsAssumesDifferentHeads unifyData + | Just unifyData <- unifyOverloading overloadSimplifier (Pair first second) = + lift $ overloadedConstructorSortInjectionAndEquals childTransformers unifyData + | Just unifyData <- Builtin.Bool.matchUnifyBoolAnd first second = + lift $ Builtin.Bool.unifyBoolAnd childTransformers unifyData + | Just unifyData <- Builtin.Bool.matchUnifyBoolOr first second = + lift $ Builtin.Bool.unifyBoolOr childTransformers unifyData | Just boolNotData <- Builtin.Bool.matchUnifyBoolNot first second = - lift $ Builtin.Bool.unifyBoolNot childTransformers first boolNotData - | Just boolNotData <- Builtin.Bool.matchUnifyBoolNot second first = - lift $ Builtin.Bool.unifyBoolNot childTransformers second boolNotData + lift $ Builtin.Bool.unifyBoolNot childTransformers boolNotData | Just unifyData <- Builtin.Int.matchUnifyIntEq first second = lift $ Builtin.Int.unifyIntEq childTransformers notSimplifier unifyData - | Just unifyData <- Builtin.Int.matchUnifyIntEq second first = - lift $ Builtin.Int.unifyIntEq childTransformers notSimplifier unifyData - | Just unifyData <- Builtin.String.matchUnifyStringEq first second = lift $ Builtin.String.unifyStringEq childTransformers notSimplifier unifyData - | Just unifyData <- Builtin.String.matchUnifyStringEq second first = lift $ Builtin.String.unifyStringEq childTransformers notSimplifier unifyData - | otherwise = - asum - [ do - unifyData <- Error.hoistMaybe $ Builtin.KEqual.matchUnifyKequalsEq first second - lift $ Builtin.KEqual.unifyKequalsEq childTransformers notSimplifier unifyData - , do - unifyData <- Error.hoistMaybe $ Builtin.KEqual.matchUnifyKequalsEq second first - lift $ Builtin.KEqual.unifyKequalsEq childTransformers notSimplifier unifyData - , Builtin.Endianness.unifyEquals first second - , Builtin.Signedness.unifyEquals first second - , Builtin.Map.unifyEquals childTransformers first second - , Builtin.Map.unifyNotInKeys childTransformers notSimplifier first second - , Builtin.Set.unifyEquals childTransformers first second - , Builtin.List.unifyEquals childTransformers first second - , domainValueAndConstructorErrors first second - ] + | Just unifyData <- Builtin.String.matchUnifyStringEq first second = + lift $ Builtin.String.unifyStringEq childTransformers notSimplifier unifyData + | Just unifyData <- Builtin.KEqual.matchUnifyKequalsEq first second = + lift $ Builtin.KEqual.unifyKequalsEq childTransformers notSimplifier unifyData + | Just unifyData <- Builtin.Endianness.matchUnifyEqualsEndianness first second = + lift $ Builtin.Endianness.unifyEquals unifyData + | Just unifyData <- Builtin.Signedness.matchUnifyEqualsSignedness first second = + lift $ Builtin.Signedness.unifyEquals unifyData + | Just unifyData <- Builtin.Map.matchUnifyEquals tools first second = + lift $ Builtin.Map.unifyEquals childTransformers tools unifyData + | Just unifyData <- Builtin.Map.matchUnifyNotInKeys first second = + lift $ Builtin.Map.unifyNotInKeys childTransformers notSimplifier unifyData + | Just unifyData <- Builtin.Set.matchUnifyEquals tools first second = + lift $ Builtin.Set.unifyEquals childTransformers tools unifyData + | Just unifyData <- Builtin.List.matchUnifyEqualsList tools first second = + lift $ + Builtin.List.unifyEquals + childTransformers + tools + unifyData + | Just unifyData <- matchDomainValueAndConstructorErrors first second = + lift $ domainValueAndConstructorErrors unifyData + | otherwise = empty maybeTermAnd :: MonadUnify unifier => @@ -224,10 +217,11 @@ maybeTermAnd :: MaybeT unifier (Pattern RewritingVariableName) maybeTermAnd notSimplifier childTransformers first second = do injSimplifier <- Simplifier.askInjSimplifier - OverloadSimplifier{isOverloaded} <- Simplifier.askOverloadSimplifier - worker injSimplifier isOverloaded + overloadSimplifier <- Simplifier.askOverloadSimplifier + tools <- Simplifier.askMetadataTools + worker injSimplifier overloadSimplifier tools where - worker injSimplifier isOverloaded + worker injSimplifier overloadSimplifier tools | Just unifyData <- matchExpandAlias first second = let UnifyExpandAlias{term1, term2} = unifyData in maybeTermAnd @@ -235,22 +229,20 @@ maybeTermAnd notSimplifier childTransformers first second = do childTransformers term1 term2 - | Just unifyData <- matchBoolAnd first = - lift $ boolAnd first second unifyData - | Just unifyData <- matchBoolAnd second = - lift $ boolAnd second first unifyData + | Just unifyData <- matchBoolAnd first second = + lift $ boolAnd unifyData | Just unifyData <- Builtin.Int.matchInt first second = - lift $ Builtin.Int.unifyInt first second unifyData + lift $ Builtin.Int.unifyInt unifyData | Just unifyData <- Builtin.Bool.matchBools first second = - lift $ Builtin.Bool.unifyBool first second unifyData + lift $ Builtin.Bool.unifyBool unifyData | Just unifyData <- Builtin.String.matchString first second = - lift $ Builtin.String.unifyString first second unifyData + lift $ Builtin.String.unifyString unifyData | Just unifyData <- matchDomainValue first second = - lift $ unifyDomainValue first second unifyData + lift $ unifyDomainValue unifyData | Just unifyData <- matchStringLiteral first second = - lift $ unifyStringLiteral first second unifyData - | Just () <- matchEqualsAndEquals first second = - lift $ equalAndEquals first + lift $ unifyStringLiteral unifyData + | Just term <- matchEqualsAndEquals first second = + lift $ equalAndEquals term | Just unifyData <- matchBytes first second = lift $ unifyBytes unifyData | Just matched <- matchVariables first second = @@ -260,44 +252,46 @@ maybeTermAnd notSimplifier childTransformers first second = do | Just unifyData <- matchEqualInjectiveHeadsAndEquals first second = lift $ equalInjectiveHeadsAndEquals childTransformers unifyData | Just unifyData <- matchInj injSimplifier first second = - lift $ unifySortInjection childTransformers first second unifyData - | Just () <- matchConstructorSortInjectionAndEquals first second = - lift $ constructorSortInjectionAndEquals first second - | Just () <- matchDifferentConstructors isOverloaded first second = - lift $ constructorAndEqualsAssumesDifferentHeads first second - | otherwise = - overloadedConstructorSortInjectionAndEquals childTransformers first second - <|> rest - - rest - | Just boolAndData <- Builtin.Bool.matchUnifyBoolAnd first second = - lift $ Builtin.Bool.unifyBoolAnd childTransformers first boolAndData - | Just boolAndData <- Builtin.Bool.matchUnifyBoolAnd second first = - lift $ Builtin.Bool.unifyBoolAnd childTransformers second boolAndData - | Just boolOrData <- Builtin.Bool.matchUnifyBoolOr first second = - lift $ Builtin.Bool.unifyBoolOr childTransformers first boolOrData - | Just boolOrData <- Builtin.Bool.matchUnifyBoolOr second first = - lift $ Builtin.Bool.unifyBoolOr childTransformers second boolOrData + lift $ unifySortInjection childTransformers unifyData + | Just unifyData <- matchConstructorSortInjectionAndEquals first second = + lift $ constructorSortInjectionAndEquals unifyData + | Just unifyData <- matchDifferentConstructors overloadSimplifier first second = + lift $ constructorAndEqualsAssumesDifferentHeads unifyData + | Just unifyData <- unifyOverloading overloadSimplifier (Pair first second) = + lift $ overloadedConstructorSortInjectionAndEquals childTransformers unifyData + | Just unifyData <- Builtin.Bool.matchUnifyBoolAnd first second = + lift $ Builtin.Bool.unifyBoolAnd childTransformers unifyData + | Just unifyData <- Builtin.Bool.matchUnifyBoolOr first second = + lift $ Builtin.Bool.unifyBoolOr childTransformers unifyData | Just boolNotData <- Builtin.Bool.matchUnifyBoolNot first second = - lift $ Builtin.Bool.unifyBoolNot childTransformers first boolNotData - | Just boolNotData <- Builtin.Bool.matchUnifyBoolNot second first = - lift $ Builtin.Bool.unifyBoolNot childTransformers second boolNotData + lift $ Builtin.Bool.unifyBoolNot childTransformers boolNotData | Just unifyData <- Builtin.KEqual.matchUnifyKequalsEq first second = lift $ Builtin.KEqual.unifyKequalsEq childTransformers notSimplifier unifyData | Just unifyData <- Builtin.Int.matchUnifyIntEq first second = lift $ Builtin.Int.unifyIntEq childTransformers notSimplifier unifyData - | Just unifyData <- Builtin.String.matchUnifyStringEq first second = lift $ Builtin.String.unifyStringEq childTransformers notSimplifier unifyData - | otherwise = - asum - [ Builtin.KEqual.unifyIfThenElse childTransformers first second - , Builtin.Endianness.unifyEquals first second - , Builtin.Signedness.unifyEquals first second - , Builtin.Map.unifyEquals childTransformers first second - , Builtin.Set.unifyEquals childTransformers first second - , Builtin.List.unifyEquals childTransformers first second - , domainValueAndConstructorErrors first second - , Error.hoistMaybe (functionAnd first second) - ] + | Just unifyData <- Builtin.String.matchUnifyStringEq first second = + lift $ Builtin.String.unifyStringEq childTransformers notSimplifier unifyData + | Just unifyData <- Builtin.KEqual.matchIfThenElse first second = + lift $ Builtin.KEqual.unifyIfThenElse childTransformers unifyData + | Just unifyData <- Builtin.Endianness.matchUnifyEqualsEndianness first second = + lift $ Builtin.Endianness.unifyEquals unifyData + | Just unifyData <- Builtin.Signedness.matchUnifyEqualsSignedness first second = + lift $ Builtin.Signedness.unifyEquals unifyData + | Just unifyData <- Builtin.Map.matchUnifyEquals tools first second = + lift $ Builtin.Map.unifyEquals childTransformers tools unifyData + | Just unifyData <- Builtin.Set.matchUnifyEquals tools first second = + lift $ Builtin.Set.unifyEquals childTransformers tools unifyData + | Just unifyData <- Builtin.List.matchUnifyEqualsList tools first second = + lift $ + Builtin.List.unifyEquals + childTransformers + tools + unifyData + | Just unifyData <- matchDomainValueAndConstructorErrors first second = + lift $ domainValueAndConstructorErrors unifyData + | Just unifyData <- matchFunctionAnd first second = + return $ functionAnd unifyData + | otherwise = empty {- | Construct the conjunction or unification of two terms. @@ -318,8 +312,8 @@ type TermTransformationOld variable unifier = MaybeT unifier (Pattern variable) data UnifyBoolAnd - = UnifyBoolAndBottom - | UnifyBoolAndTop + = UnifyBoolAndBottom !Sort !(TermLike RewritingVariableName) + | UnifyBoolAndTop !(TermLike RewritingVariableName) {- | Matches @@ -330,17 +324,26 @@ data UnifyBoolAnd and @ -\\and{_}(\\top, _) +\\and{_}(\\top, _), @ + +symmetric in the two arguments. -} matchBoolAnd :: + TermLike RewritingVariableName -> TermLike RewritingVariableName -> Maybe UnifyBoolAnd -matchBoolAnd term - | Pattern.isBottom term = - Just UnifyBoolAndBottom - | Pattern.isTop term = - Just UnifyBoolAndTop +matchBoolAnd term1 term2 + | Pattern.isBottom term1 = + let sort = termLikeSort term1 + in Just $ UnifyBoolAndBottom sort term2 + | Pattern.isTop term1 = + Just $ UnifyBoolAndTop term2 + | Pattern.isBottom term2 = + let sort = termLikeSort term2 + in Just $ UnifyBoolAndBottom sort term1 + | Pattern.isTop term2 = + Just $ UnifyBoolAndTop term1 | otherwise = Nothing {-# INLINE matchBoolAnd #-} @@ -348,25 +351,23 @@ matchBoolAnd term -- | Simplify the conjunction of terms where one is a predicate. boolAnd :: MonadUnify unifier => - TermLike RewritingVariableName -> - TermLike RewritingVariableName -> UnifyBoolAnd -> unifier (Pattern RewritingVariableName) -boolAnd first second unifyData = +boolAnd unifyData = case unifyData of - UnifyBoolAndBottom -> do - explainBoolAndBottom first second - return $ Pattern.fromTermLike first - UnifyBoolAndTop -> - return $ Pattern.fromTermLike second + UnifyBoolAndBottom sort term -> do + explainBoolAndBottom term sort + return $ Pattern.fromTermLike $ mkBottom sort + UnifyBoolAndTop term -> do + return $ Pattern.fromTermLike term explainBoolAndBottom :: MonadUnify unifier => TermLike RewritingVariableName -> - TermLike RewritingVariableName -> + Sort -> unifier () -explainBoolAndBottom term1 term2 = - debugUnifyBottom "Cannot unify bottom." term1 term2 +explainBoolAndBottom term sort = + debugUnifyBottom "Cannot unify bottom." (mkBottom sort) term {- | Matches @@ -383,10 +384,10 @@ and matchEqualsAndEquals :: TermLike RewritingVariableName -> TermLike RewritingVariableName -> - Maybe () + Maybe (TermLike RewritingVariableName) matchEqualsAndEquals first second | first == second = - Just () + Just first | otherwise = Nothing {-# INLINE matchEqualsAndEquals #-} @@ -395,22 +396,32 @@ equalAndEquals :: Monad unifier => TermLike RewritingVariableName -> unifier (Pattern RewritingVariableName) -equalAndEquals first = +equalAndEquals term = -- TODO (thomas.tuegel): Preserve simplified flags. - return (Pattern.fromTermLike first) + return (Pattern.fromTermLike term) + +data BottomTermEquals = BottomTermEquals + { sort :: !Sort + , term :: !(TermLike RewritingVariableName) + } {- | Matches @ -\\equals{_, _}(\\bottom, _) +\\equals{_, _}(\\bottom, _), @ + +symmetric in the two arguments. -} matchBottomTermEquals :: TermLike RewritingVariableName -> - Maybe () -matchBottomTermEquals first - | Bottom_ _ <- first = - Just () + TermLike RewritingVariableName -> + Maybe BottomTermEquals +matchBottomTermEquals first second + | Bottom_ sort <- first = + Just BottomTermEquals{sort, term = second} + | Bottom_ sort <- second = + Just BottomTermEquals{sort, term = first} | otherwise = Nothing {-# INLINE matchBottomTermEquals #-} @@ -418,24 +429,22 @@ matchBottomTermEquals first bottomTermEquals :: MonadUnify unifier => SideCondition RewritingVariableName -> - TermLike RewritingVariableName -> - TermLike RewritingVariableName -> + BottomTermEquals -> unifier (Pattern RewritingVariableName) bottomTermEquals sideCondition - first - second = + unifyData = do -- MonadUnify - secondCeil <- makeEvaluateTermCeil sideCondition second + secondCeil <- makeEvaluateTermCeil sideCondition term case toList secondCeil of [] -> return Pattern.top [Conditional{predicate = PredicateTrue, substitution}] - | substitution == mempty -> do + | substitution == mempty -> debugUnifyBottomAndReturnBottom "Cannot unify bottom with non-bottom pattern." - first - second + (mkBottom sort) + term _ -> return Conditional @@ -446,6 +455,8 @@ bottomTermEquals OrPattern.map Condition.toPredicate secondCeil , substitution = mempty } + where + BottomTermEquals{sort, term} = unifyData data UnifyVariables = UnifyVariables {variable1, variable2 :: !(ElementVariable RewritingVariableName)} @@ -496,20 +507,30 @@ unifyVariableFunction UnifyVariableFunction{variable, term} = & Pattern.withCondition term & pure +data VariableFunctionEquals = VariableFunctionEquals + { var :: !(ElementVariable RewritingVariableName) + , term1, term2 :: !(TermLike RewritingVariableName) + } + {- | Matches @ -\\equals{_, _}(x, f(_)) +\\equals{_, _}(x, f(_)), @ + +symmetric in the two arguments. -} matchVariableFunctionEquals :: TermLike RewritingVariableName -> TermLike RewritingVariableName -> - Maybe (ElementVariable RewritingVariableName) + Maybe VariableFunctionEquals matchVariableFunctionEquals first second | ElemVar_ var <- first , isFunctionPattern second = - Just var + Just VariableFunctionEquals{term1 = first, term2 = second, var} + | ElemVar_ var <- second + , isFunctionPattern first = + Just VariableFunctionEquals{term1 = second, term2 = first, var} | otherwise = Nothing {-# INLINE matchVariableFunctionEquals #-} @@ -519,31 +540,34 @@ See also: 'isFunctionPattern' -} variableFunctionEquals :: MonadUnify unifier => - TermLike RewritingVariableName -> - TermLike RewritingVariableName -> - ElementVariable RewritingVariableName -> + VariableFunctionEquals -> unifier (Pattern RewritingVariableName) variableFunctionEquals - first - second - var = + unifyData = do -- MonadUnify predicate <- do - resultOr <- makeEvaluateTermCeil SideCondition.topTODO second + resultOr <- makeEvaluateTermCeil SideCondition.topTODO term2 case toList resultOr of - [] -> do + [] -> debugUnifyBottomAndReturnBottom "Unification of variable and bottom \ \when attempting to simplify equals." - first - second + term1 + term2 resultConditions -> Unify.scatter resultConditions let result = predicate <> Condition.fromSingleSubstitution - (Substitution.assign (inject var) second) - return (Pattern.withCondition second result) + (Substitution.assign (inject var) term2) + return (Pattern.withCondition term2 result) + where + VariableFunctionEquals{term1, term2, var} = unifyData + +data UnifyInjData = UnifyInjData + { term1, term2 :: !(TermLike RewritingVariableName) + , unifyInj :: !(UnifyInj (InjPair RewritingVariableName)) + } {- | Matches @@ -569,11 +593,12 @@ matchInj :: InjSimplifier -> TermLike RewritingVariableName -> TermLike RewritingVariableName -> - Maybe (UnifyInj (InjPair RewritingVariableName)) + Maybe UnifyInjData matchInj injSimplifier first second | Inj_ inj1 <- first , Inj_ inj2 <- second = - matchInjs injSimplifier inj1 inj2 + UnifyInjData first second + <$> matchInjs injSimplifier inj1 inj2 | otherwise = Nothing {-# INLINE matchInj #-} @@ -597,11 +622,9 @@ unifySortInjection :: forall unifier. MonadUnify unifier => TermSimplifier RewritingVariableName unifier -> - TermLike RewritingVariableName -> - TermLike RewritingVariableName -> - UnifyInj (InjPair RewritingVariableName) -> + UnifyInjData -> unifier (Pattern RewritingVariableName) -unifySortInjection termMerger term1 term2 unifyInj = do +unifySortInjection termMerger unifyData = do InjSimplifier{unifyInjs} <- Simplifier.askInjSimplifier unifyInjs unifyInj & maybe distinct merge where @@ -613,42 +636,47 @@ unifySortInjection termMerger term1 term2 unifyInj = do let (childTerm, childCondition) = Pattern.splitTerm childPattern inj' = evaluateInj inj{injChild = childTerm} return $ Pattern.withCondition inj' childCondition + UnifyInjData{unifyInj, term1, term2} = unifyData + +data ConstructorSortInjectionAndEquals = ConstructorSortInjectionAndEquals + { term1, term2 :: !(TermLike RewritingVariableName) + } {- | Matches @ -\\equals{_, _}(inj{_,_}(_), f(_)) +\\equals{_, _}(inj{_,_}(_), c(_)) @ @ -\\equals{_, _}(f(_), inj{_,_}(_)) +\\equals{_, _}(c(_), inj{_,_}(_)) @ and @ -\\and{_}(inj{_,_}(_), f(_)) +\\and{_}(inj{_,_}(_), c(_)) @ @ -\\and{_}(f(_), inj{_,_}(_)) +\\and{_}(c(_), inj{_,_}(_)) @ -when @f@ has the @constructor@ attribute. +when @c@ has the @constructor@ attribute. -} matchConstructorSortInjectionAndEquals :: TermLike RewritingVariableName -> TermLike RewritingVariableName -> - Maybe () + Maybe ConstructorSortInjectionAndEquals matchConstructorSortInjectionAndEquals first second | Inj_ _ <- first , App_ symbol _ <- second , Symbol.isConstructor symbol = - Just () + Just ConstructorSortInjectionAndEquals{term1 = first, term2 = second} | Inj_ _ <- second , App_ symbol _ <- first , Symbol.isConstructor symbol = - Just () + Just ConstructorSortInjectionAndEquals{term1 = first, term2 = second} | otherwise = Nothing {-# INLINE matchConstructorSortInjectionAndEquals #-} @@ -659,11 +687,12 @@ returns @\\bottom@. -} constructorSortInjectionAndEquals :: MonadUnify unifier => - TermLike RewritingVariableName -> - TermLike RewritingVariableName -> + ConstructorSortInjectionAndEquals -> unifier a -constructorSortInjectionAndEquals first second = - noConfusionInjectionConstructor first second +constructorSortInjectionAndEquals unifyData = + noConfusionInjectionConstructor term1 term2 + where + ConstructorSortInjectionAndEquals{term1, term2} = unifyData noConfusionInjectionConstructor :: MonadUnify unifier => @@ -685,48 +714,77 @@ See TermSimplifier RewritingVariableName unifier -> - TermLike RewritingVariableName -> - TermLike RewritingVariableName -> - MaybeT unifier (Pattern RewritingVariableName) -overloadedConstructorSortInjectionAndEquals termMerger firstTerm secondTerm = - do - eunifier <- - lift . Error.runExceptT $ - unifyOverloading (Pair firstTerm secondTerm) - case eunifier of - Right (Simple (Pair firstTerm' secondTerm')) -> - lift $ - termMerger firstTerm' secondTerm' - Right - ( WithNarrowing - Narrowing - { narrowingSubst - , narrowingVars - , overloadPair = Pair firstTerm' secondTerm' - } - ) -> do - boundPattern <- lift $ do - merged <- termMerger firstTerm' secondTerm' - Exists.makeEvaluate SideCondition.topTODO narrowingVars $ - merged `Pattern.andCondition` narrowingSubst - case OrPattern.toPatterns boundPattern of - [result] -> return result - [] -> - lift $ - debugUnifyBottomAndReturnBottom - ( "exists simplification for overloaded" - <> " constructors returned no pattern" - ) - firstTerm - secondTerm - _ -> empty - Left (Clash message) -> - lift $ - debugUnifyBottomAndReturnBottom - (fromString message) - firstTerm - secondTerm - Left Overloading.NotApplicable -> empty + OverloadingData -> + unifier (Pattern RewritingVariableName) +overloadedConstructorSortInjectionAndEquals termMerger unifyData = + case matchResult of + Resolution (Simple (Pair firstTerm' secondTerm')) -> + termMerger firstTerm' secondTerm' + Resolution + ( WithNarrowing + Narrowing + { narrowingSubst + , narrowingVars + , overloadPair = Pair firstTerm' secondTerm' + } + ) -> do + boundPattern <- do + merged <- termMerger firstTerm' secondTerm' + Exists.makeEvaluate SideCondition.topTODO narrowingVars $ + merged `Pattern.andCondition` narrowingSubst + case OrPattern.toPatterns boundPattern of + [result] -> return result + [] -> + debugUnifyBottomAndReturnBottom + ( "exists simplification for overloaded" + <> " constructors returned no pattern" + ) + term1 + term2 + _ -> scatter boundPattern + ClashResult message -> + debugUnifyBottomAndReturnBottom (fromString message) term1 term2 + where + OverloadingData{term1, term2, matchResult} = unifyData + +data DVConstrError + = DVConstr !(TermLike RewritingVariableName) !(TermLike RewritingVariableName) + | ConstrDV !(TermLike RewritingVariableName) !(TermLike RewritingVariableName) + +{- | Matches + +@ +\\equals{_, _}(\\dv{_}(_), c(_)) +@ + +@ +\\equals{_, _}(c(_), \\dv{_}(_)) +@ + +@ +\\and{_}(\\dv{_}(_), c(_)) +@ + +@ +\\and{_}(c(_), \\dv{_}(_)) +@ + +when @c@ is a constructor. +-} +matchDomainValueAndConstructorErrors :: + TermLike RewritingVariableName -> + TermLike RewritingVariableName -> + Maybe DVConstrError +matchDomainValueAndConstructorErrors first second + | DV_ _ _ <- first + , App_ secondHead _ <- second + , Symbol.isConstructor secondHead = + Just $ DVConstr first second + | App_ firstHead _ <- first + , Symbol.isConstructor firstHead + , DV_ _ _ <- second = + Just $ ConstrDV first second + | otherwise = Nothing {- | Unifcation or equality for a domain value pattern vs a constructor application. @@ -735,37 +793,28 @@ This unification case throws an error because domain values may not occur in a sort with constructors. -} domainValueAndConstructorErrors :: - Monad unifier => HasCallStack => - TermLike RewritingVariableName -> - TermLike RewritingVariableName -> - MaybeT unifier a -domainValueAndConstructorErrors - term1@(DV_ _ _) - term2@(App_ secondHead _) - | Symbol.isConstructor secondHead = - error - ( unlines - [ "Cannot handle DomainValue and Constructor:" - , unparseToString term1 - , unparseToString term2 - ] - ) -domainValueAndConstructorErrors - term1@(App_ firstHead _) - term2@(DV_ _ _) - | Symbol.isConstructor firstHead = - error - ( unlines - [ "Cannot handle Constructor and DomainValue:" - , unparseToString term1 - , unparseToString term2 - ] - ) -domainValueAndConstructorErrors _ _ = empty + DVConstrError -> + unifier a +domainValueAndConstructorErrors unifyData = + error $ + show + ( Pretty.vsep + [ cannotHandle + , fromString $ unparseToString term1 + , fromString $ unparseToString term2 + , "" + ] + ) + where + (term1, term2, cannotHandle) = + case unifyData of + DVConstr a b -> (a, b, "Cannot handle DomainValue and Constructor:") + ConstrDV a b -> (a, b, "Cannot handle Constructor and DomainValue:") data UnifyDomainValue = UnifyDomainValue { val1, val2 :: !(TermLike RewritingVariableName) + , term1, term2 :: !(TermLike RewritingVariableName) } {- | Matches @@ -784,11 +833,11 @@ matchDomainValue :: TermLike RewritingVariableName -> TermLike RewritingVariableName -> Maybe UnifyDomainValue -matchDomainValue first second - | DV_ sort1 val1 <- first - , DV_ sort2 val2 <- second +matchDomainValue term1 term2 + | DV_ sort1 val1 <- term1 + , DV_ sort2 val2 <- term2 , sort1 == sort2 = - Just UnifyDomainValue{val1, val2} + Just UnifyDomainValue{val1, val2, term1, term2} | otherwise = Nothing {-# INLINE matchDomainValue #-} @@ -805,16 +854,14 @@ See also: 'equalAndEquals' unifyDomainValue :: forall unifier. MonadUnify unifier => - TermLike RewritingVariableName -> - TermLike RewritingVariableName -> UnifyDomainValue -> unifier (Pattern RewritingVariableName) -unifyDomainValue term1 term2 unifyData +unifyDomainValue unifyData | val1 == val2 = return $ Pattern.fromTermLike term1 | otherwise = cannotUnifyDomainValues term1 term2 where - UnifyDomainValue{val1, val2} = unifyData + UnifyDomainValue{val1, val2, term1, term2} = unifyData cannotUnifyDistinctDomainValues :: Text cannotUnifyDistinctDomainValues = "distinct domain values" @@ -830,6 +877,7 @@ cannotUnifyDomainValues term1 term2 = -- | @UnifyStringLiteral@ represents unification of two string literals. data UnifyStringLiteral = UnifyStringLiteral { txt1, txt2 :: !Text + , term1, term2 :: !(TermLike RewritingVariableName) } -- | Matches the unification problem @"txt1"@ with @"txt2"@. @@ -837,10 +885,10 @@ matchStringLiteral :: TermLike RewritingVariableName -> TermLike RewritingVariableName -> Maybe UnifyStringLiteral -matchStringLiteral first second - | StringLiteral_ txt1 <- first - , StringLiteral_ txt2 <- second = - Just UnifyStringLiteral{txt1, txt2} +matchStringLiteral term1 term2 + | StringLiteral_ txt1 <- term1 + , StringLiteral_ txt2 <- term2 = + Just UnifyStringLiteral{txt1, txt2, term1, term2} | otherwise = Nothing {-# INLINE matchStringLiteral #-} @@ -848,16 +896,35 @@ matchStringLiteral first second unifyStringLiteral :: forall unifier. MonadUnify unifier => - TermLike RewritingVariableName -> - TermLike RewritingVariableName -> UnifyStringLiteral -> unifier (Pattern RewritingVariableName) -unifyStringLiteral term1 term2 unifyData +unifyStringLiteral unifyData | txt1 == txt2 = return $ Pattern.fromTermLike term1 | otherwise = debugUnifyBottomAndReturnBottom "distinct string literals" term1 term2 where - UnifyStringLiteral{txt1, txt2} = unifyData + UnifyStringLiteral{txt1, txt2, term1, term2} = unifyData + +data FunctionAnd = FunctionAnd + { term1, term2 :: !(TermLike RewritingVariableName) + } + +{- | Matches + +@ +\\and{_}(f(_), g(_)) +@ +-} +matchFunctionAnd :: + TermLike RewritingVariableName -> + TermLike RewritingVariableName -> + Maybe FunctionAnd +matchFunctionAnd term1 term2 + | isFunctionPattern term1 + , isFunctionPattern term2 = + Just FunctionAnd{term1, term2} + | otherwise = Nothing +{-# INLINE matchFunctionAnd #-} {- | Unify any two function patterns. @@ -868,23 +935,18 @@ on the left-hand side of the @\\equals@ predicate, and the other argument appears on the right-hand side. -} functionAnd :: - TermLike RewritingVariableName -> - TermLike RewritingVariableName -> - Maybe (Pattern RewritingVariableName) -functionAnd first second - | isFunctionPattern first - , isFunctionPattern second = - makeEqualsPredicate first' second' - & Predicate.markSimplified - -- Ceil predicate not needed since first being - -- bottom will make the entire term bottom. However, - -- one must be careful to not just drop the term. - & Condition.fromPredicate - & Pattern.withCondition first' -- different for Equals - & pure - | otherwise = empty + FunctionAnd -> + Pattern RewritingVariableName +functionAnd FunctionAnd{term1, term2} = + makeEqualsPredicate first' second' + & Predicate.markSimplified + -- Ceil predicate not needed since first being + -- bottom will make the entire term bottom. However, + -- one must be careful to not just drop the term. + & Condition.fromPredicate + & Pattern.withCondition first' -- different for Equals where - (first', second') = minMaxBy compareForEquals first second + (first', second') = minMaxBy compareForEquals term1 term2 {- | Normal ordering for terms in @\equals(_, _)@. diff --git a/kore/src/Kore/Simplify/NoConfusion.hs b/kore/src/Kore/Simplify/NoConfusion.hs index 79bdd336b0..16c0684257 100644 --- a/kore/src/Kore/Simplify/NoConfusion.hs +++ b/kore/src/Kore/Simplify/NoConfusion.hs @@ -22,6 +22,7 @@ import Kore.Log.DebugUnifyBottom ( import Kore.Rewrite.RewritingVariable ( RewritingVariableName, ) +import Kore.Simplify.OverloadSimplifier import Kore.Simplify.Simplify as Simplifier import Kore.Unification.Unify as Unify import Prelude.Kore hiding ( @@ -102,6 +103,10 @@ equalInjectiveHeadsAndEquals , secondChildren } = unifyData +data DifferentConstructors = DifferentConstructors + { term1, term2 :: !(TermLike RewritingVariableName) + } + {- | Matches @ @@ -117,12 +122,12 @@ and when @f /= g@ and @f,g@ either have the @constructor@ attribute or are overloaded. -} matchDifferentConstructors :: - (Symbol -> Bool) -> + OverloadSimplifier -> TermLike RewritingVariableName -> TermLike RewritingVariableName -> - Maybe () + Maybe DifferentConstructors matchDifferentConstructors - isOverloaded + OverloadSimplifier{isOverloaded} first second | App_ firstHead _ <- first @@ -130,7 +135,7 @@ matchDifferentConstructors , firstHead /= secondHead , Symbol.isConstructor firstHead || isOverloaded firstHead , Symbol.isConstructor secondHead || isOverloaded secondHead = - Just () + Just DifferentConstructors{term1 = first, term2 = second} | otherwise = empty {-# INLINE matchDifferentConstructors #-} @@ -141,15 +146,14 @@ to be different; therefore their conjunction is @\\bottom@. -} constructorAndEqualsAssumesDifferentHeads :: MonadUnify unifier => - TermLike RewritingVariableName -> - TermLike RewritingVariableName -> + DifferentConstructors -> unifier a constructorAndEqualsAssumesDifferentHeads - first - second = - do - debugUnifyBottomAndReturnBottom - "Cannot unify different constructors or incompatible \ - \sort injections." - first - second + unifyData = + debugUnifyBottomAndReturnBottom + "Cannot unify different constructors or incompatible \ + \sort injections." + term1 + term2 + where + DifferentConstructors{term1, term2} = unifyData diff --git a/kore/src/Kore/Simplify/Overloading.hs b/kore/src/Kore/Simplify/Overloading.hs index 39cec63253..7df12b3378 100644 --- a/kore/src/Kore/Simplify/Overloading.hs +++ b/kore/src/Kore/Simplify/Overloading.hs @@ -6,17 +6,18 @@ module Kore.Simplify.Overloading ( matchOverloading, -- for testing purposes unifyOverloading, + OverloadingData (..), UnifyOverloadingResult, MatchOverloadingResult, UnifyOverloadingError (..), Narrowing (..), OverloadingResolution (..), + MatchResult (..), ) where import qualified Control.Monad as Monad import Control.Monad.Trans.Except ( ExceptT, - catchE, throwE, ) import Data.Text ( @@ -31,13 +32,11 @@ import Kore.Attribute.Synthetic ( synthesize, ) import Kore.Debug -import Kore.Internal.ApplicationSorts ( - ApplicationSorts (..), - ) import Kore.Internal.Condition ( Condition, ) import qualified Kore.Internal.Condition as Condition +import Kore.Internal.Symbol import Kore.Internal.TermLike import Kore.Rewrite.RewritingVariable ( RewritingVariableName, @@ -46,7 +45,6 @@ import Kore.Rewrite.RewritingVariable ( import Kore.Simplify.OverloadSimplifier import Kore.Simplify.Simplify as Simplifier ( MonadSimplify (..), - isConstructorOrOverloaded, ) import Pair import Prelude.Kore hiding ( @@ -78,6 +76,23 @@ data OverloadingResolution variable deriving anyclass (SOP.Generic, SOP.HasDatatypeInfo) deriving anyclass (Debug, Diff) +data MatchResult + = ClashResult !String + | Resolution !(OverloadingResolution RewritingVariableName) + deriving stock (Eq, Ord, Show) + deriving stock (GHC.Generic) + deriving anyclass (SOP.Generic, SOP.HasDatatypeInfo) + deriving anyclass (Debug, Diff) + +flipResult :: + MatchResult -> + MatchResult +flipResult result = + case result of + Resolution (Simple (Pair term1 term2)) -> + Resolution (Simple (Pair term2 term1)) + _ -> result + -- | Describes the possible errors encountered during unification. data UnifyOverloadingError = -- | the unification problem could not be solved by the current method @@ -108,24 +123,26 @@ type MatchOverloadingResult unifier variable = unifier (Pair (TermLike variable)) -type OverloadingResult unifier a = ExceptT UnifyOverloadingError unifier a - -notApplicable :: Monad unifier => OverloadingResult unifier a -notApplicable = empty - -throwBottom :: Monad unifier => String -> OverloadingResult unifier a -throwBottom = throwE . Clash +throwBottom :: String -> Maybe MatchResult +throwBottom = Just . ClashResult matchOverloading :: MonadSimplify unifier => Pair (TermLike RewritingVariableName) -> MatchOverloadingResult unifier RewritingVariableName -matchOverloading termPair = - do - unifyResult <- unifyOverloading termPair - case unifyResult of - Simple pair -> return pair - _ -> notApplicable +matchOverloading termPair = do + overloadSimplifier <- askOverloadSimplifier + case unifyOverloading overloadSimplifier termPair of + Just OverloadingData{matchResult} -> case matchResult of + Resolution (Simple pair) -> return pair + ClashResult msg -> throwE $ Clash msg + _ -> empty + Nothing -> empty + +data OverloadingData = OverloadingData + { term1, term2 :: !(TermLike RewritingVariableName) + , matchResult :: !MatchResult + } {- | Tests whether the pair of terms can be coerced to have the same constructors @@ -141,54 +158,54 @@ matchOverloading termPair = the first and second terms in a pair are not interchangeable. -} unifyOverloading :: - forall unifier. - MonadSimplify unifier => + OverloadSimplifier -> Pair (TermLike RewritingVariableName) -> - UnifyOverloadingResult unifier RewritingVariableName -unifyOverloading termPair = case termPair of - Pair - (Inj_ inj@Inj{injChild = App_ firstHead firstChildren}) - secondTerm@(App_ secondHead _) -> - Simple . flipPairBack - <$> unifyOverloadingVsOverloaded - secondHead - secondTerm - (Application firstHead firstChildren) - inj{injChild = ()} - Pair - firstTerm@(App_ firstHead _) - (Inj_ inj@Inj{injChild = App_ secondHead secondChildren}) -> - Simple - <$> unifyOverloadingVsOverloaded + Maybe OverloadingData +unifyOverloading overloadSimplifier termPair = + OverloadingData term1 term2 <$> case termPair of + Pair + (Inj_ inj@Inj{injChild = App_ firstHead firstChildren}) + secondTerm@(App_ secondHead _) -> + flipResult + <$> unifyOverloadingVsOverloaded + overloadSimplifier + secondHead + secondTerm + (Application firstHead firstChildren) + inj{injChild = ()} + Pair + firstTerm@(App_ firstHead _) + (Inj_ inj@Inj{injChild = App_ secondHead secondChildren}) -> + unifyOverloadingVsOverloaded + overloadSimplifier firstHead firstTerm (Application secondHead secondChildren) inj{injChild = ()} - Pair - (Inj_ inj@Inj{injChild = App_ firstHead firstChildren}) - (Inj_ inj'@Inj{injChild = App_ secondHead secondChildren}) - | injFrom inj /= injFrom inj' -> -- this case should have been handled by now - Simple - <$> unifyOverloadingCommonOverload + Pair + (Inj_ inj@Inj{injChild = App_ firstHead firstChildren}) + (Inj_ inj'@Inj{injChild = App_ secondHead secondChildren}) + | injFrom inj /= injFrom inj' -> -- this case should have been handled by now + unifyOverloadingCommonOverload + overloadSimplifier (Application firstHead firstChildren) (Application secondHead secondChildren) inj{injChild = ()} - Pair firstTerm secondTerm -> - catchE - (worker firstTerm secondTerm) - ( \case - NotApplicable -> worker secondTerm firstTerm - clash -> throwE clash - ) + Pair firstTerm secondTerm -> + case worker firstTerm secondTerm of + Nothing -> worker secondTerm firstTerm + Just result -> Just result where + Pair term1 term2 = termPair worker :: TermLike RewritingVariableName -> TermLike RewritingVariableName -> - UnifyOverloadingResult unifier RewritingVariableName + Maybe MatchResult worker firstTerm@(App_ firstHead _) (Inj_ inj@Inj{injChild = ElemVar_ secondVar}) = unifyOverloadingVsOverloadedVariable + overloadSimplifier firstHead firstTerm secondVar @@ -197,19 +214,21 @@ unifyOverloading termPair = case termPair of (Inj_ Inj{injChild = firstTerm@(App_ firstHead firstChildren)}) (Inj_ inj@Inj{injChild = ElemVar_ secondVar}) = unifyOverloadingInjVsVariable + overloadSimplifier (Application firstHead firstChildren) secondVar (Attribute.freeVariables firstTerm) inj{injChild = ()} worker (App_ firstHead _) (Inj_ Inj{injChild}) = notUnifiableTest firstHead injChild - worker _ _ = notApplicable + worker _ _ = Nothing - flipPairBack (Pair x y) = Pair y x notUnifiableTest termHead child = do - OverloadSimplifier{isOverloaded} <- Simplifier.askOverloadSimplifier Monad.guard (isOverloaded termHead) notUnifiableError child + where + OverloadSimplifier{isOverloaded} = overloadSimplifier +{-# INLINE unifyOverloading #-} {- Handles the case inj{S1,injTo}(firstHead(firstChildren)) @@ -228,30 +247,32 @@ unifyOverloading termPair = case termPair of inj{S,injTo}(headUnion(inj2(secondChildren))) -} unifyOverloadingCommonOverload :: - MonadSimplify unifier => + OverloadSimplifier -> Application Symbol (TermLike RewritingVariableName) -> Application Symbol (TermLike RewritingVariableName) -> Inj () -> - MatchOverloadingResult unifier RewritingVariableName + Maybe MatchResult unifyOverloadingCommonOverload + overloadSimplifier (Application firstHead firstChildren) (Application secondHead secondChildren) - injProto@Inj{injTo} = - do - OverloadSimplifier - { isOverloaded - , resolveOverloading - , unifyOverloadWithinBound - } <- - Simplifier.askOverloadSimplifier - Monad.guard (isOverloaded firstHead && isOverloaded secondHead) + injProto@Inj{injTo} + | isOverloaded firstHead + , isOverloaded secondHead = case unifyOverloadWithinBound injProto firstHead secondHead injTo of - Nothing -> notUnifiableOverloads + Nothing -> Just $ ClashResult "overloaded constructors not unifiable" Just InjectedOverload{overload, injectionHead} -> let first' = resolveOverloading injProto overload firstChildren second' = resolveOverloading injProto overload secondChildren mkInj' = maybeMkInj injectionHead - in return $ Pair (mkInj' first') (mkInj' second') + in Just $ Resolution $ Simple $ Pair (mkInj' first') (mkInj' second') + | otherwise = Nothing + where + OverloadSimplifier + { isOverloaded + , resolveOverloading + , unifyOverloadWithinBound + } = overloadSimplifier {- Handles the case overloadingTerm@(overloadingHead(overloadingChildren)) @@ -267,28 +288,32 @@ unifyOverloadingCommonOverload overloadingHead(inj'(overloadedChildren)) -} unifyOverloadingVsOverloaded :: - MonadSimplify unifier => + OverloadSimplifier -> Symbol -> TermLike RewritingVariableName -> Application Symbol (TermLike RewritingVariableName) -> Inj () -> - MatchOverloadingResult unifier RewritingVariableName + Maybe MatchResult unifyOverloadingVsOverloaded + overloadSimplifier overloadingHead overloadingTerm (Application overloadedHead overloadedChildren) - injProto = - do - OverloadSimplifier{isOverloaded, isOverloading, resolveOverloading} <- - Simplifier.askOverloadSimplifier - Monad.guard (isOverloaded overloadingHead) - isSecondHeadConstructor <- isConstructorOrOverloaded overloadedHead - Monad.guard isSecondHeadConstructor + injProto + | isOverloaded overloadingHead + , isConstructor overloadedHead || isOverloaded overloadedHead = let ~overloadedTerm' = resolveOverloading injProto overloadingHead overloadedChildren - if isOverloading overloadingHead overloadedHead - then return $ Pair overloadingTerm overloadedTerm' - else throwBottom "different injected ctor" + in if isOverloading overloadingHead overloadedHead + then Just $ Resolution $ Simple $ Pair overloadingTerm overloadedTerm' + else throwBottom "different injected ctor" + | otherwise = Nothing + where + OverloadSimplifier + { isOverloaded + , isOverloading + , resolveOverloading + } = overloadSimplifier {- Handles the case overloadingTerm@(overloadingHead(overloadingChildren)) @@ -306,36 +331,39 @@ unifyOverloadingVsOverloaded overloadingHead(inj2(freshVars)) -} unifyOverloadingVsOverloadedVariable :: - MonadSimplify unifier => + OverloadSimplifier -> Symbol -> TermLike RewritingVariableName -> ElementVariable RewritingVariableName -> Inj () -> - UnifyOverloadingResult unifier RewritingVariableName + Maybe MatchResult unifyOverloadingVsOverloadedVariable + overloadSimplifier overloadingHead overloadingTerm overloadedVar injProto@Inj{injFrom} = do - OverloadSimplifier{isOverloaded, getOverloadedWithinSort} <- - Simplifier.askOverloadSimplifier Monad.guard (isOverloaded overloadingHead) case getOverloadedWithinSort injProto overloadingHead injFrom of - Right Nothing -> notUnifiableOverloads + Right Nothing -> Just notUnifiableOverloads Right (Just overHead) -> - WithNarrowing - <$> computeNarrowing - overloadingTerm - Nothing - overloadingHead - injProto - freeVars - overloadedVar - overHead + Just $ + Resolution $ + WithNarrowing $ + computeNarrowing + overloadSimplifier + overloadingTerm + Nothing + overloadingHead + injProto + freeVars + overloadedVar + overHead Left err -> error err where freeVars = freeVariables overloadingTerm + OverloadSimplifier{isOverloaded, getOverloadedWithinSort} = overloadSimplifier {- Handles the case inj{S1,injTo}(firstHead(firstChildren)) @@ -356,46 +384,50 @@ unifyOverloadingVsOverloadedVariable inj{S,injTo}(headUnion(inj2(freshVars))) -} unifyOverloadingInjVsVariable :: - MonadSimplify unifier => + OverloadSimplifier -> Application Symbol (TermLike RewritingVariableName) -> ElementVariable RewritingVariableName -> Attribute.FreeVariables RewritingVariableName -> Inj () -> - UnifyOverloadingResult unifier RewritingVariableName + Maybe MatchResult unifyOverloadingInjVsVariable + overloadSimplifier (Application firstHead firstChildren) overloadedVar freeVars - injProto = - do - OverloadSimplifier - { isOverloaded - , resolveOverloading - , unifyOverloadWithSortWithinBound - } <- - Simplifier.askOverloadSimplifier - Monad.guard (isOverloaded firstHead) + injProto + | isOverloaded firstHead = case unifyOverloadWithSortWithinBound firstHead injProto of Left err -> error err - Right Nothing -> notUnifiableOverloads + Right Nothing -> Just notUnifiableOverloads Right (Just InjectedOverloadPair{overloadingSymbol, overloadedSymbol}) -> - do - let (InjectedOverload headUnion maybeInjUnion) = overloadingSymbol - first' = resolveOverloading injProto headUnion firstChildren - WithNarrowing - <$> computeNarrowing - first' - maybeInjUnion - headUnion - injProto - freeVars - overloadedVar - overloadedSymbol + let (InjectedOverload headUnion maybeInjUnion) = overloadingSymbol + first' = resolveOverloading injProto headUnion firstChildren + in Just $ + Resolution $ + WithNarrowing $ + computeNarrowing + overloadSimplifier + first' + maybeInjUnion + headUnion + injProto + freeVars + overloadedVar + overloadedSymbol + | otherwise = Nothing + where + OverloadSimplifier + { isOverloaded + , resolveOverloading + , unifyOverloadWithSortWithinBound + } = overloadSimplifier computeNarrowing :: HasCallStack => - MonadSimplify unifier => + -- |overloading simpifier + OverloadSimplifier -> -- |overloading pair LHS TermLike RewritingVariableName -> -- |optional injection @@ -410,8 +442,9 @@ computeNarrowing :: ElementVariable RewritingVariableName -> -- |overloaded symbol injected into the variable's sort InjectedOverload -> - ExceptT UnifyOverloadingError unifier (Narrowing RewritingVariableName) + Narrowing RewritingVariableName computeNarrowing + overloadSimplifier first' injection' headUnion @@ -420,19 +453,15 @@ computeNarrowing overloadedVar overloaded | App_ _ freshTerms <- overloadedTerm = - do - OverloadSimplifier{resolveOverloading} <- - Simplifier.askOverloadSimplifier - let second' = - resolveOverloading injUnion headUnion freshTerms - return - Narrowing - { narrowingSubst = - Condition.assign (inject overloadedVar) narrowingTerm - , narrowingVars = - Attribute.getFreeElementVariables $ freeVariables narrowingTerm - , overloadPair = Pair (mkInj' first') (mkInj' second') - } + let second' = + resolveOverloading injUnion headUnion freshTerms + in Narrowing + { narrowingSubst = + Condition.assign (inject overloadedVar) narrowingTerm + , narrowingVars = + Attribute.getFreeElementVariables $ freeVariables narrowingTerm + , overloadPair = Pair (mkInj' first') (mkInj' second') + } | otherwise = error "This should not happen" where InjectedOverload{overload, injectionHead} = overloaded @@ -440,6 +469,7 @@ computeNarrowing overloadedTerm = freshSymbolInstance allVars overload "x" mkInj' = maybeMkInj injection' narrowingTerm = maybeMkInj injectionHead overloadedTerm + OverloadSimplifier{resolveOverloading} = overloadSimplifier -- | Generates fresh variables as arguments for a symbol to create a pattern. freshSymbolInstance :: @@ -474,15 +504,16 @@ maybeMkInj :: maybeMkInj maybeInj injChild = maybe injChild (flip mkInj injChild) maybeInj notUnifiableError :: - Monad unifier => TermLike RewritingVariableName -> OverloadingResult unifier a -notUnifiableError (DV_ _ _) = throwBottom "injected domain value" -notUnifiableError (InternalBool_ _) = throwBottom "injected builtin bool" -notUnifiableError (InternalInt_ _) = throwBottom "injected builtin int" -notUnifiableError (InternalList_ _) = throwBottom "injected builtin list" -notUnifiableError (InternalMap_ _) = throwBottom "injected builtin map" -notUnifiableError (InternalSet_ _) = throwBottom "injected builtin set" -notUnifiableError (InternalString_ _) = throwBottom "injected builtin string" -notUnifiableError _ = notApplicable - -notUnifiableOverloads :: Monad unifier => OverloadingResult unifier a -notUnifiableOverloads = throwBottom "overloaded constructors not unifiable" + TermLike RewritingVariableName -> Maybe MatchResult +notUnifiableError = \case + (DV_ _ _) -> Just $ ClashResult "injected domain value" + (InternalBool_ _) -> Just $ ClashResult "injected builtin bool" + (InternalInt_ _) -> Just $ ClashResult "injected builtin int" + (InternalList_ _) -> Just $ ClashResult "injected builtin list" + (InternalMap_ _) -> Just $ ClashResult "injected builtin map" + (InternalSet_ _) -> Just $ ClashResult "injected builtin set" + (InternalString_ _) -> Just $ ClashResult "injected builtin string" + _ -> Nothing + +notUnifiableOverloads :: MatchResult +notUnifiableOverloads = ClashResult "overloaded constructors not unifiable" diff --git a/kore/test/Test/Kore/Builtin/Bool.hs b/kore/test/Test/Kore/Builtin/Bool.hs index f3594a2f2d..312125067d 100644 --- a/kore/test/Test/Kore/Builtin/Bool.hs +++ b/kore/test/Test/Kore/Builtin/Bool.hs @@ -162,12 +162,12 @@ test_unifyBoolValues = testCase testName $ do case Bool.matchBools term1 term2 of Just unifyData -> do - actual <- unify term1 term2 unifyData + actual <- unify unifyData assertEqual "" expected actual Nothing -> assertEqual "" expected [Nothing] - unify term1 term2 unifyData = - run (lift $ Bool.unifyBool term1 term2 unifyData) + unify unifyData = + run (lift $ Bool.unifyBool unifyData) test_unifyBoolAnd :: [TestTree] test_unifyBoolAnd = @@ -194,13 +194,13 @@ test_unifyBoolAnd = test testName term1 term2 expected = testCase testName $ do case Bool.matchUnifyBoolAnd term1 term2 of - Just boolAnd -> do - actual <- unify term1 boolAnd + Just unifyData -> do + actual <- unify unifyData assertEqual "" expected actual Nothing -> assertEqual "" expected [Nothing] - unify term boolAnd = - Bool.unifyBoolAnd termSimplifier term boolAnd + unify unifyData = + Bool.unifyBoolAnd termSimplifier unifyData & lift & run @@ -229,13 +229,13 @@ test_unifyBoolOr = test testName term1 term2 expected = testCase testName $ do case Bool.matchUnifyBoolOr term1 term2 of - Just boolOr -> do - actual <- unify term1 boolOr + Just unifyData -> do + actual <- unify unifyData assertEqual "" expected actual Nothing -> assertEqual "" expected [Nothing] - unify term boolOr = - Bool.unifyBoolOr termSimplifier term boolOr + unify unifyData = + Bool.unifyBoolOr termSimplifier unifyData & lift & run diff --git a/kore/test/Test/Kore/Builtin/String.hs b/kore/test/Test/Kore/Builtin/String.hs index f14aaa71ec..561296ee0a 100644 --- a/kore/test/Test/Kore/Builtin/String.hs +++ b/kore/test/Test/Kore/Builtin/String.hs @@ -555,7 +555,6 @@ test_unifyStringEq = matched = String.matchUnifyStringEq term1 term2 - <|> String.matchUnifyStringEq term2 term1 simplifyCondition' :: Condition RewritingVariableName -> diff --git a/kore/test/Test/Kore/Simplify/AndTerms.hs b/kore/test/Test/Kore/Simplify/AndTerms.hs index 167f774c97..4a856c8bae 100644 --- a/kore/test/Test/Kore/Simplify/AndTerms.hs +++ b/kore/test/Test/Kore/Simplify/AndTerms.hs @@ -56,7 +56,9 @@ import Kore.Simplify.And ( termAnd, ) import Kore.Simplify.AndTerms ( + FunctionAnd (..), functionAnd, + matchFunctionAnd, termUnification, ) import Kore.Simplify.Equals ( @@ -1465,7 +1467,9 @@ test_functionAnd = Pattern.withCondition (f x) $ Condition.fromPredicate $ makeEqualsPredicate (f x) (f y) - let Just actual = functionAnd (f x) (f y) + let actual = functionAnd $ FunctionAnd (f x) (f y) + let matchResult = matchFunctionAnd (f x) (f y) + assertBool "" (isJust matchResult) assertEqual "" expect (Pattern.syncSort actual) assertBool "" (Pattern.isSimplified sideRepresentation actual) ] diff --git a/kore/test/Test/Kore/Simplify/Overloading.hs b/kore/test/Test/Kore/Simplify/Overloading.hs index 13116e8dd0..d7935328b6 100644 --- a/kore/test/Test/Kore/Simplify/Overloading.hs +++ b/kore/test/Test/Kore/Simplify/Overloading.hs @@ -438,7 +438,7 @@ unifies :: TestTree unifies comment (term1, term2) (term1', term2') = withUnification - (assertEqual "" (Right (Simple (Pair term1' term2')))) + (assertEqual "" (Just (Resolution (Simple (Pair term1' term2'))))) comment (Pair term1 term2) @@ -458,9 +458,11 @@ narrows comment (term1, term2) ((v, term), (term1', term2')) = where checkNarrowing :: UnificationResult -> Assertion checkNarrowing - ( Right - ( WithNarrowing - Narrowing{narrowingSubst, overloadPair} + ( Just + ( Resolution + ( WithNarrowing + Narrowing{narrowingSubst, overloadPair} + ) ) ) = do @@ -478,7 +480,7 @@ doesn'tUnify :: TestTree doesn'tUnify comment term1 term2 reason = withUnification - (assertEqual "" (Left (Clash reason))) + (assertEqual "" (Just (ClashResult reason))) comment (Pair term1 term2) @@ -490,7 +492,7 @@ unifyNotApplicable :: TestTree unifyNotApplicable comment term1 term2 = withUnification - (assertEqual "" (Left NotApplicable)) + (assertEqual "" Nothing) comment (Pair term1 term2) @@ -502,16 +504,16 @@ unifyNotApplicableTwice :: TestTree unifyNotApplicableTwice comment term1 term2 = withUnificationTwice - (assertEqual "" (Left NotApplicable)) + (assertEqual "" Nothing) comment (Pair term1 term2) -type MatchResult = +type TestMatchResult = Either UnifyOverloadingError (Pair (TermLike RewritingVariableName)) match :: Pair (TermLike RewritingVariableName) -> - IO MatchResult + IO TestMatchResult match termPair = runSimplifier Mock.env $ runExceptT matchResult where matchResult :: @@ -519,7 +521,7 @@ match termPair = runSimplifier Mock.env $ runExceptT matchResult matchResult = matchOverloading termPair withMatching :: - (MatchResult -> Assertion) -> + (TestMatchResult -> Assertion) -> TestName -> Pair (TermLike RewritingVariableName) -> TestTree @@ -529,7 +531,7 @@ withMatching check comment termPair = check actual withMatchingTwice :: - (MatchResult -> Assertion) -> + (TestMatchResult -> Assertion) -> TestName -> Pair (TermLike RewritingVariableName) -> TestTree @@ -543,15 +545,16 @@ withMatchingTwice check comment termPair = check actual' type UnificationResult = - Either UnifyOverloadingError (OverloadingResolution RewritingVariableName) + Maybe MatchResult unify :: Pair (TermLike RewritingVariableName) -> IO UnificationResult -unify termPair = runSimplifier Mock.env $ runExceptT unifyResult +unify termPair = + runSimplifier Mock.env $ return unifyResult where - unifyResult :: UnifyOverloadingResult (SimplifierT NoSMT) RewritingVariableName - unifyResult = unifyOverloading termPair + unifyResult :: Maybe MatchResult + unifyResult = matchResult <$> unifyOverloading Mock.overloadSimplifier termPair withUnification :: (UnificationResult -> Assertion) -> @@ -572,13 +575,13 @@ withUnificationTwice check comment termPair = testCase comment $ do actual <- unify termPair case actual of - Left _ -> assertFailure "Expected matching solution." - Right (Simple termPair') -> do + Just (Resolution (Simple termPair')) -> do actual' <- unify termPair' check actual' - Right (WithNarrowing Narrowing{overloadPair}) -> do + Just (Resolution (WithNarrowing Narrowing{overloadPair})) -> do actual' <- unify overloadPair check actual' + _ -> assertFailure "Expected matching solution." x1 :: TermLike RewritingVariableName x1 =