diff --git a/kore/app/exec/Main.hs b/kore/app/exec/Main.hs index 6244d4d3aa..9ceff19b1c 100644 --- a/kore/app/exec/Main.hs +++ b/kore/app/exec/Main.hs @@ -91,9 +91,13 @@ import Kore.Reachability ( SomeClaim, StuckClaim (..), getConfiguration, + lensClaimPattern, ) import qualified Kore.Reachability.Claim as Claim import Kore.Rewrite +import Kore.Rewrite.ClaimPattern ( + getClaimPatternSort, + ) import Kore.Rewrite.RewritingVariable import Kore.Rewrite.RulePattern ( mapRuleVariables, @@ -113,9 +117,6 @@ import Kore.Syntax.Definition ( Sentence (..), ) import qualified Kore.Syntax.Definition as Definition.DoNotUse -import Kore.TopBottom ( - isTop, - ) import Kore.Unparser ( unparse, ) @@ -714,18 +715,22 @@ koreProve execOptions proveOptions = do maybeAlreadyProvenModule let ProveClaimsResult{stuckClaims, provenClaims} = proveResult - let (exitCode, final) - | noStuckClaims = success - | otherwise = - stuckPatterns - & OrPattern.toTermLike - & failure + let (exitCode, final) = + case foldFirst stuckClaims of + Nothing -> success -- stuckClaims is empty + Just claim -> + stuckPatterns + & OrPattern.toTermLike (getClaimPatternSort $ claimPattern claim) + & failure where - noStuckClaims = isTop stuckClaims stuckPatterns = OrPattern.fromPatterns (MultiAnd.map getStuckConfig stuckClaims) getStuckConfig = getRewritingPattern . getConfiguration . getStuckClaim + claimPattern claim = + claim + & getStuckClaim + & Lens.view lensClaimPattern lift $ for_ saveProofs $ saveProven specModule provenClaims lift $ renderResult execOptions (unparse final) return (kFileLocations definition, exitCode) diff --git a/kore/src/Kore/Builtin/AssociativeCommutative.hs b/kore/src/Kore/Builtin/AssociativeCommutative.hs index 7e9b4b0fa5..b086765a5b 100644 --- a/kore/src/Kore/Builtin/AssociativeCommutative.hs +++ b/kore/src/Kore/Builtin/AssociativeCommutative.hs @@ -115,6 +115,7 @@ import Kore.Rewrite.RewritingVariable ( import Kore.Simplify.Simplify as Simplifier import Kore.Sort ( Sort, + sameSort, ) import Kore.Syntax.Variable import Kore.Unification.Unify ( @@ -1400,7 +1401,10 @@ unifyEqualsElementLists let remainder2Terms = map fromConcreteOrWithVariable remainder2 - case elementListAsInternal tools (termLikeSort first) remainder2Terms of + case elementListAsInternal + tools + (sameSort (termLikeSort first) (termLikeSort second)) + remainder2Terms of Nothing -> debugUnifyBottomAndReturnBottom "Duplicated element in unification results" diff --git a/kore/src/Kore/Builtin/Builtin.hs b/kore/src/Kore/Builtin/Builtin.hs index 60e76be91b..f982adea50 100644 --- a/kore/src/Kore/Builtin/Builtin.hs +++ b/kore/src/Kore/Builtin/Builtin.hs @@ -96,9 +96,6 @@ import Kore.Simplify.Simplify ( import qualified Kore.Simplify.Simplify as AttemptedAxiomResults ( AttemptedAxiomResults (..), ) -import Kore.Sort ( - predicateSort, - ) import Kore.Unparser import Prelude.Kore @@ -448,19 +445,15 @@ isSymbol builtinName Symbol{symbolAttributes = Attribute.Symbol{hook}} = {- | Is the given sort hooked to the named builtin? -Returns Nothing if the sort is unknown (i.e. the _PREDICATE sort). -Returns Just False if the sort is a variable. +Returns Nothing if the sort is a variable. -} isSort :: Text -> SmtMetadataTools attr -> Sort -> Maybe Bool isSort builtinName tools sort - | isPredicateSort = Nothing | SortVariableSort _ <- sort = Nothing | otherwise = let MetadataTools{sortAttributes} = tools Attribute.Sort{hook} = sortAttributes sort in Just (getHook hook == Just builtinName) - where - isPredicateSort = sort == predicateSort -- | Run a function evaluator that can terminate early. getAttemptedAxiom :: diff --git a/kore/src/Kore/Builtin/EqTerm.hs b/kore/src/Kore/Builtin/EqTerm.hs index ea21d2a075..7d6734f026 100644 --- a/kore/src/Kore/Builtin/EqTerm.hs +++ b/kore/src/Kore/Builtin/EqTerm.hs @@ -9,12 +9,12 @@ module Kore.Builtin.EqTerm ( ) where import qualified Control.Monad as Monad +import Kore.Internal.ApplicationSorts (applicationSortsResult) import qualified Kore.Internal.MultiOr as MultiOr import qualified Kore.Internal.OrPattern as OrPattern import Kore.Internal.Pattern ( Pattern, ) -import qualified Kore.Internal.Pattern as Pattern import qualified Kore.Internal.SideCondition as SideCondition import Kore.Internal.TermLike as TermLike import Kore.Rewrite.RewritingVariable ( @@ -48,7 +48,6 @@ matchEqTerm selectSymbol (App_ symbol [operand1, operand2]) = do matchEqTerm _ _ = Nothing {- | Unification for an equality-like symbol. - This function is suitable only for equality simplification. -} unifyEqTerm :: @@ -63,8 +62,11 @@ 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' + (if value then pure else mkNotSimplified) solution' >>= Unify.scatter where - EqTerm{operand1, operand2} = eqTerm - eraseTerm = Pattern.fromCondition_ . Pattern.withoutTerm + EqTerm{symbol, operand1, operand2} = eqTerm + eqSort = applicationSortsResult . symbolSorts $ symbol + eraseTerm conditional = conditional $> (mkTop eqSort) + mkNotSimplified notChild = + notSimplifier SideCondition.top Not{notSort = eqSort, notChild} diff --git a/kore/src/Kore/Builtin/Int.hs b/kore/src/Kore/Builtin/Int.hs index 37c91c00c1..3026aa6d05 100644 --- a/kore/src/Kore/Builtin/Int.hs +++ b/kore/src/Kore/Builtin/Int.hs @@ -126,6 +126,7 @@ import Kore.Internal.Predicate ( ) import qualified Kore.Internal.SideCondition as SideCondition import Kore.Internal.Symbol ( + applicationSortsResult, symbolHook, ) import Kore.Internal.TermLike as TermLike @@ -524,10 +525,13 @@ unifyIntEq unifyChildren (NotSimplifier notSimplifier) unifyData = MultiOr.map eraseTerm solution & if internalBoolValue internalBool then pure - else notSimplifier SideCondition.top + else mkNotSimplified scattered <- Unify.scatter solution' return scattered{term = mkInternalBool internalBool} where UnifyIntEq{eqTerm, internalBool} = unifyData - EqTerm{operand1, operand2} = eqTerm - eraseTerm = Pattern.fromCondition_ . Pattern.withoutTerm + EqTerm{symbol, operand1, operand2} = eqTerm + eqSort = applicationSortsResult . symbolSorts $ symbol + eraseTerm conditional = conditional $> (mkTop eqSort) + mkNotSimplified notChild = + notSimplifier SideCondition.top Not{notSort = eqSort, notChild} diff --git a/kore/src/Kore/Builtin/Int/Int.hs b/kore/src/Kore/Builtin/Int/Int.hs index 8a28485967..190092eda6 100644 --- a/kore/src/Kore/Builtin/Int/Int.hs +++ b/kore/src/Kore/Builtin/Int/Int.hs @@ -101,7 +101,7 @@ asPartialPattern :: Maybe Integer -> Pattern variable asPartialPattern resultSort = - maybe Pattern.bottom (asPattern resultSort) + maybe (Pattern.bottomOf resultSort) (asPattern resultSort) randKey :: IsString s => s randKey = "INT.rand" diff --git a/kore/src/Kore/Builtin/KEqual.hs b/kore/src/Kore/Builtin/KEqual.hs index 01e9ff1db6..2129b40176 100644 --- a/kore/src/Kore/Builtin/KEqual.hs +++ b/kore/src/Kore/Builtin/KEqual.hs @@ -276,13 +276,16 @@ unifyKequalsEq unifyChildren (NotSimplifier notSimplifier) unifyData = MultiOr.map eraseTerm solution & if internalBoolValue internalBool then pure - else notSimplifier SideCondition.top + else mkNotSimplified scattered <- Unify.scatter solution' return (scattered :: Pattern RewritingVariableName){term = mkInternalBool internalBool} where UnifyKequalsEq{eqTerm, internalBool} = unifyData - EqTerm{operand1, operand2} = eqTerm - eraseTerm = Pattern.fromCondition_ . Pattern.withoutTerm + EqTerm{symbol, operand1, operand2} = eqTerm + eqSort = applicationSortsResult . symbolSorts $ symbol + eraseTerm conditional = conditional $> (mkTop eqSort) + mkNotSimplified notChild = + notSimplifier SideCondition.top Not{notSort = eqSort, notChild} -- | The @KEQUAL.ite@ hooked symbol applied to @term@-type arguments. data IfThenElse term = IfThenElse diff --git a/kore/src/Kore/Builtin/List.hs b/kore/src/Kore/Builtin/List.hs index 89b7aa9b8b..98c96627ed 100644 --- a/kore/src/Kore/Builtin/List.hs +++ b/kore/src/Kore/Builtin/List.hs @@ -277,7 +277,7 @@ evalGet _ resultSort [_list, _ix] = do emptyList <|> bothConcrete where maybeBottom = - maybe Pattern.bottom Pattern.fromTermLike + maybe (Pattern.bottomOf resultSort) Pattern.fromTermLike evalGet _ _ _ = Builtin.wrongArity getKey evalUpdate :: Builtin.Function @@ -629,7 +629,7 @@ unifyEquals "Cannot unify lists of different length." term1 term2 - return Pattern.bottom + return (Pattern.bottomOf $ termLikeSort term1) unifyEqualsFramedRightRight :: TermLike.Symbol -> diff --git a/kore/src/Kore/Builtin/Map.hs b/kore/src/Kore/Builtin/Map.hs index 62d32be10b..5639d36087 100644 --- a/kore/src/Kore/Builtin/Map.hs +++ b/kore/src/Kore/Builtin/Map.hs @@ -89,6 +89,7 @@ import Kore.Internal.Symbol ( ) import Kore.Internal.TermLike ( Key, + Not (..), TermLike, retractKey, termLikeSort, @@ -707,13 +708,14 @@ matchUnifyNotInKeys first second unifyNotInKeys :: forall unifier. MonadUnify unifier => + Sort -> TermSimplifier RewritingVariableName unifier -> NotSimplifier unifier -> UnifyNotInKeysResult -> unifier (Pattern RewritingVariableName) -unifyNotInKeys unifyChildren (NotSimplifier notSimplifier) unifyData = +unifyNotInKeys resultSort unifyChildren (NotSimplifier notSimplifier) unifyData = case unifyData of - NullKeysNullOpaques -> return Pattern.top + NullKeysNullOpaques -> return (Pattern.topOf resultSort) NonNullKeysOrMultipleOpaques unifyData' -> do -- Concrete keys are constructor-like, therefore they are defined @@ -750,18 +752,19 @@ unifyNotInKeys unifyChildren (NotSimplifier notSimplifier) unifyData = >>= Unify.scatter eraseTerm = - Pattern.fromCondition_ . Pattern.withoutTerm + Pattern.fromCondition resultSort . Pattern.withoutTerm unifyAndNegate t1 t2 = do -- Erasing the unified term is valid here because -- the terms are all wrapped in \ceil below. unificationSolutions <- - fmap eraseTerm - <$> Unify.gather (unifyChildren t1 t2) - notSimplifier - SideCondition.top - (OrPattern.fromPatterns unificationSolutions) + fmap eraseTerm <$> Unify.gather (unifyChildren t1 t2) + (notSimplifier SideCondition.top) + Not + { notSort = resultSort + , notChild = OrPattern.fromPatterns unificationSolutions + } >>= Unify.scatter - collectConditions terms = fold terms & Pattern.fromCondition_ + collectConditions terms = fold terms & Pattern.fromCondition resultSort diff --git a/kore/src/Kore/Builtin/String.hs b/kore/src/Kore/Builtin/String.hs index ca84bee763..77f8765d5f 100644 --- a/kore/src/Kore/Builtin/String.hs +++ b/kore/src/Kore/Builtin/String.hs @@ -574,10 +574,13 @@ unifyStringEq unifyChildren (NotSimplifier notSimplifier) unifyData = MultiOr.map eraseTerm solution & if internalBoolValue internalBool then pure - else notSimplifier SideCondition.top + else mkNotSimplified scattered <- Unify.scatter solution' return scattered{term = mkInternalBool internalBool} where UnifyStringEq{eqTerm, internalBool} = unifyData - EqTerm{operand1, operand2} = eqTerm - eraseTerm = Pattern.fromCondition_ . Pattern.withoutTerm + EqTerm{symbol, operand1, operand2} = eqTerm + eqSort = applicationSortsResult . symbolSorts $ symbol + eraseTerm conditional = conditional $> (mkTop eqSort) + mkNotSimplified notChild = + notSimplifier SideCondition.top Not{notSort = eqSort, notChild} diff --git a/kore/src/Kore/Builtin/String/String.hs b/kore/src/Kore/Builtin/String/String.hs index aa2240bf24..bb769f8674 100644 --- a/kore/src/Kore/Builtin/String/String.hs +++ b/kore/src/Kore/Builtin/String/String.hs @@ -91,7 +91,7 @@ asPartialPattern :: Maybe Text -> Pattern variable asPartialPattern resultSort = - maybe Pattern.bottom (asPattern resultSort) + maybe (Pattern.bottomOf resultSort) (asPattern resultSort) eqKey :: IsString s => s eqKey = "STRING.eq" diff --git a/kore/src/Kore/Equation/Validate.hs b/kore/src/Kore/Equation/Validate.hs index bb1003842b..6a8fe72376 100644 --- a/kore/src/Kore/Equation/Validate.hs +++ b/kore/src/Kore/Equation/Validate.hs @@ -13,6 +13,7 @@ import qualified Data.Functor.Foldable as Recursive import Data.Text ( pack, ) +import Kore.AST.AstWithLocation import Kore.AST.Error import Kore.Attribute.Axiom ( Assoc (..), @@ -36,11 +37,18 @@ import Kore.Equation.Sentence ( fromSentenceAxiom, ) import Kore.Internal.Predicate ( + Predicate, pattern PredicateCeil, pattern PredicateIn, ) import qualified Kore.Internal.Predicate as Predicate import qualified Kore.Internal.Symbol as Symbol +import Kore.Internal.TermLike ( + AstLocation, + InternalVariable, + TermLike, + mkSortVariable, + ) import qualified Kore.Internal.TermLike as TermLike import Kore.Syntax.Definition import Kore.Syntax.Variable @@ -50,6 +58,7 @@ import Kore.Unparser ( import Kore.Validate.Verifier import qualified Kore.Verified as Verified import Prelude.Kore +import Pretty (Doc) import qualified Pretty validateAxiom :: @@ -121,25 +130,42 @@ validateAxiom attrs verified = failOnJust eq "Expected variable, but found:" - $ asum $ getNotVar <$> termLikeF + (fmap unparseWithLocation $ asum $ getNotVar <$> termLikeF) getNotVar (TermLike.Var_ _) = Nothing getNotVar term = Just term + unparseWithLocation :: + AstWithLocation variable => + InternalVariable variable => + TermLike variable -> + (Doc ann, AstLocation) + unparseWithLocation t = (unparse t, locationFromAst t) + checkArg _ Nothing = return () checkArg eq (Just arg) = traverse_ ( failOnJust eq "Found invalid subterm in argument of function equation:" - . checkArgIn + . checkArgInAndUnparse ) $ Predicate.getMultiAndPredicate arg where - checkArgIn (PredicateIn (TermLike.Var_ _) term) = - findBadArgSubterm term - checkArgIn (PredicateCeil (TermLike.And_ _ (TermLike.Var_ _) term)) = - findBadArgSubterm term - checkArgIn badArg = Just $ Predicate.fromPredicate_ badArg - + checkArgInAndUnparse :: + AstWithLocation variable => + InternalVariable variable => + Predicate variable -> + Maybe (Doc ann, AstLocation) + checkArgInAndUnparse predicate = + checkArgIn predicate <&> unparseWithLocation + where + checkArgIn (PredicateIn (TermLike.Var_ _) term) = + findBadArgSubterm term + checkArgIn (PredicateCeil (TermLike.And_ _ (TermLike.Var_ _) term)) = + findBadArgSubterm term + checkArgIn badArg = + -- use dummy sort variable for pretty printing inside failOnJust + -- the term's AstLocation will be AstLocationNone + Just $ Predicate.fromPredicate (mkSortVariable "_") badArg findBadArgSubterm term = case term of _ | TermLike.isConstructorLike term -> descend @@ -175,14 +201,14 @@ validateAxiom attrs verified = descend = asum $ findBadArgSubterm <$> termF failOnJust _ _ Nothing = return () - failOnJust eq errorMessage (Just term) = + failOnJust eq errorMessage (Just (term, location)) = koreFailWithLocations - [term] + [location] ( pack $ show $ Pretty.vsep [ errorMessage - , Pretty.indent 4 $ unparse term + , Pretty.indent 4 term , "The equation that the above occurs in is:" , Pretty.indent 4 $ Pretty.pretty eq ] diff --git a/kore/src/Kore/Exec.hs b/kore/src/Kore/Exec.hs index ef60a42029..d444ed4cce 100644 --- a/kore/src/Kore/Exec.hs +++ b/kore/src/Kore/Exec.hs @@ -89,7 +89,7 @@ import Kore.Internal.Pattern ( ) import qualified Kore.Internal.Pattern as Pattern import Kore.Internal.Predicate ( - fromPredicate_, + fromPredicate, makeMultipleOrPredicate, ) import qualified Kore.Internal.Predicate as Predicate @@ -272,9 +272,9 @@ exec <$> finalConfigs exitCode <- getExitCode verifiedModule finalConfigs' let finalTerm = - forceSort initialSort $ - OrPattern.toTermLike - (MultiOr.map getRewritingPattern finalConfigs') + MultiOr.map getRewritingPattern finalConfigs' + & OrPattern.toTermLike initialSort + & sameTermLikeSort initialSort return (exitCode, finalTerm) where dropStrategy = snd @@ -429,9 +429,9 @@ search orPredicate = makeMultipleOrPredicate (Condition.toPredicate <$> solutions) return - . forceSort patternSort + . sameTermLikeSort patternSort . getRewritingTerm - . fromPredicate_ + . fromPredicate patternSort $ orPredicate where patternSort = termLikeSort termLike diff --git a/kore/src/Kore/Internal/Inj.hs b/kore/src/Kore/Internal/Inj.hs index 25702d4f54..6a0af3d195 100644 --- a/kore/src/Kore/Internal/Inj.hs +++ b/kore/src/Kore/Internal/Inj.hs @@ -85,7 +85,7 @@ instance Unparse a => Unparse (Inj a) where instance Synthetic Sort Inj where synthetic Inj{injFrom, injTo, injChild} = - injTo & seq (matchSort injFrom injChild) + injTo & seq (sameSort injFrom injChild) {-# INLINE synthetic #-} instance Synthetic (FreeVariables variable) Inj where diff --git a/kore/src/Kore/Internal/OrPattern.hs b/kore/src/Kore/Internal/OrPattern.hs index 18f2e668f7..74c5ba9c3b 100644 --- a/kore/src/Kore/Internal/OrPattern.hs +++ b/kore/src/Kore/Internal/OrPattern.hs @@ -17,7 +17,8 @@ module Kore.Internal.OrPattern ( bottom, isFalse, isPredicate, - top, + getSortIfNotBottom, + topOf, isTrue, toPattern, toTermLike, @@ -59,7 +60,7 @@ import Kore.Internal.TermLike ( InternalVariable, Sort, TermLike, - mkBottom_, + mkBottom, mkOr, ) import Kore.Syntax.Variable @@ -147,7 +148,7 @@ fromTermLike = fromPattern . Pattern.fromTermLike {- | @\\bottom@ @ -'isFalse' bottom == True +isFalse bottom == True @ -} bottom :: InternalVariable variable => OrPattern variable @@ -160,11 +161,11 @@ isFalse = isBottom {- | @\\top@ @ -'isTrue' top == True +isTrue (topOf _) == True @ -} -top :: InternalVariable variable => OrPattern variable -top = fromPattern Pattern.top +topOf :: InternalVariable variable => Sort -> OrPattern variable +topOf sort = fromPattern (Pattern.topOf sort) -- | 'isTrue' checks if the 'Or' has a single top pattern. isTrue :: OrPattern variable -> Bool @@ -174,11 +175,12 @@ isTrue = isTop toPattern :: forall variable. InternalVariable variable => + Sort -> OrPattern variable -> Pattern variable -toPattern multiOr = +toPattern sort multiOr = case toList multiOr of - [] -> Pattern.bottom + [] -> Pattern.bottomOf sort [patt] -> patt patts -> foldr1 mergeWithOr patts where @@ -208,14 +210,22 @@ toPattern multiOr = isPredicate :: OrPattern variable -> Bool isPredicate = all Pattern.isPredicate +-- | Gets the `Sort` of a non-empty 'OrPattern' and othewise returns `Nothing`. +getSortIfNotBottom :: OrPattern variable -> Maybe Sort +getSortIfNotBottom multiOr = + case toList multiOr of + [] -> Nothing + p : _ -> Just (Pattern.patternSort p) + -- | Transforms a 'Pattern' into a 'TermLike'. toTermLike :: InternalVariable variable => + Sort -> OrPattern variable -> TermLike variable -toTermLike multiOr = +toTermLike sort multiOr = case toList multiOr of - [] -> mkBottom_ + [] -> mkBottom sort [patt] -> Pattern.toTermLike patt patts -> foldr1 mkOr (Pattern.toTermLike <$> patts) diff --git a/kore/src/Kore/Internal/Pattern.hs b/kore/src/Kore/Internal/Pattern.hs index 464c31d922..813650f5ba 100644 --- a/kore/src/Kore/Internal/Pattern.hs +++ b/kore/src/Kore/Internal/Pattern.hs @@ -10,17 +10,14 @@ module Kore.Internal.Pattern ( syncSort, patternSort, fromCondition, - fromCondition_, fromTermAndPredicate, fromPredicateSorted, - bottom, bottomOf, isBottom, isTop, Kore.Internal.Pattern.mapVariables, splitTerm, toTermLike, - top, topOf, fromTermLike, Kore.Internal.Pattern.freeElementVariables, @@ -76,9 +73,7 @@ import Kore.Internal.TermLike ( TermLike, mkAnd, mkBottom, - mkBottom_, mkTop, - mkTop_, termLikeSort, ) import qualified Kore.Internal.TermLike as TermLike @@ -105,11 +100,6 @@ fromTermAndPredicate term predicate = , predicate , substitution = mempty } -fromCondition_ :: - InternalVariable variable => - Condition variable -> - Pattern variable -fromCondition_ = (<$) mkTop_ fromCondition :: InternalVariable variable => Sort -> @@ -234,17 +224,6 @@ toTermLike Conditional{term, predicate, substitution} = predicateTermLike = Predicate.fromPredicate sort predicate' sort = termLikeSort pattern' -{- |'bottom' is an expanded pattern that has a bottom condition and that -should become Bottom when transformed to a ML pattern. --} -bottom :: InternalVariable variable => Pattern variable -bottom = - Conditional - { term = mkBottom_ - , predicate = Predicate.makeFalsePredicate - , substitution = mempty - } - {- | An 'Pattern' where the 'term' is 'Bottom' of the given 'Sort'. The 'predicate' is set to 'makeFalsePredicate'. @@ -257,17 +236,6 @@ bottomOf resultSort = , substitution = mempty } -{- |'top' is an expanded pattern that has a top condition and that -should become Top when transformed to a ML pattern. --} -top :: InternalVariable variable => Pattern variable -top = - Conditional - { term = mkTop_ - , predicate = Predicate.makeTruePredicate - , substitution = mempty - } - -- | An 'Pattern' where the 'term' is 'Top' of the given 'Sort'. topOf :: InternalVariable variable => Sort -> Pattern variable topOf resultSort = @@ -337,7 +305,7 @@ coerceSort { term = if isTop term then mkTop sort - else TermLike.forceSort sort term + else TermLike.sameTermLikeSort sort term , -- Need to override this since a 'ceil' (say) over a predicate is that -- predicate with a different sort. predicate = predicate @@ -389,9 +357,10 @@ requireDefined Conditional{term, predicate, substitution} = fromMultiAnd :: InternalVariable variable => + Sort -> MultiAnd (Pattern variable) -> Pattern variable -fromMultiAnd patterns = +fromMultiAnd sort patterns = foldr ( \pattern1 -> pure @@ -401,4 +370,4 @@ fromMultiAnd patterns = ) Nothing patterns - & fromMaybe top + & fromMaybe (topOf sort) diff --git a/kore/src/Kore/Internal/Predicate.hs b/kore/src/Kore/Internal/Predicate.hs index 73e35f028c..ecc154e053 100644 --- a/kore/src/Kore/Internal/Predicate.hs +++ b/kore/src/Kore/Internal/Predicate.hs @@ -8,7 +8,6 @@ module Kore.Internal.Predicate ( unparseWithSort, unparse2WithSort, fromPredicate, - fromPredicate_, makePredicate, makeTruePredicate, makeFalsePredicate, @@ -137,9 +136,6 @@ import Kore.Internal.TermLike hiding ( simplifiedAttribute, ) import qualified Kore.Internal.TermLike as TermLike -import Kore.Sort ( - predicateSort, - ) import Kore.Substitute import Kore.TopBottom ( TopBottom (..), @@ -311,7 +307,7 @@ instance NFData variable => NFData (Predicate variable) where rnf annotation `seq` rnf pat instance InternalVariable variable => Pretty (Predicate variable) where - pretty = unparse . fromPredicate_ + pretty = unparse . fromPredicate (mkSortVariable "_") instance InternalVariable variable => SQL.Column (Predicate variable) where defineColumn = SQL.defineTextColumn @@ -593,12 +589,6 @@ fromPredicate sort = Recursive.fold worker OrF (Or () t1 t2) -> TermLike.mkOr t1 t2 TopF _ -> TermLike.mkTop sort -fromPredicate_ :: - InternalVariable variable => - Predicate variable -> - TermLike variable -fromPredicate_ = fromPredicate predicateSort - {- | Simple type used to track whether a predicate building function performed a simplification that changed the shape of the resulting term. This is needed when these functions are called while traversing the Predicate tree. @@ -821,7 +811,7 @@ makeInPredicate' :: TermLike variable -> (Predicate variable, HasChanged) makeInPredicate' t1 t2 = - (TermLike.makeSortsAgree makeInWorker t1 t2, NotChanged) + (TermLike.checkSortsAgree makeInWorker t1 t2, NotChanged) where makeInWorker t1' t2' _ = synthesize $ InF $ In () () t1' t2' @@ -838,7 +828,7 @@ makeEqualsPredicate' :: TermLike variable -> (Predicate variable, HasChanged) makeEqualsPredicate' t1 t2 = - (TermLike.makeSortsAgree makeEqualsWorker t1 t2, NotChanged) + (TermLike.checkSortsAgree makeEqualsWorker t1 t2, NotChanged) where makeEqualsWorker t1' t2' _ = synthesize $ EqualsF $ Equals () () t1' t2' @@ -966,7 +956,9 @@ instance pretty (NotPredicate termLikeF) = Pretty.vsep [ "Expected a predicate, but found:" - , Pretty.indent 4 (unparse $ fromPredicate_ <$> termLikeF) + , Pretty.indent + 4 + (unparse $ fromPredicate (mkSortVariable "_") <$> termLikeF) ] makePredicate :: @@ -1095,10 +1087,8 @@ cannotSimplifyNotSimplifiedError predF = ( "Unexpectedly marking term with NotSimplified children as simplified:\n" ++ show predF ++ "\n" - ++ unparseToString term + ++ (show . pretty $ synthesize predF) ) - where - term = fromPredicate_ (synthesize predF) simplifiedFromChildren :: HasCallStack => @@ -1221,7 +1211,8 @@ mapVariables :: mapVariables adj predicate = let termPredicate = TermLike.mapVariables adj - . fromPredicate_ + -- TODO (Andrei B): Try to avoid TermLike conversion + . fromPredicate (mkSortVariable "_") $ predicate in either errorMappingVariables diff --git a/kore/src/Kore/Internal/SideCondition.hs b/kore/src/Kore/Internal/SideCondition.hs index b401d9eae7..b82fff109f 100644 --- a/kore/src/Kore/Internal/SideCondition.hs +++ b/kore/src/Kore/Internal/SideCondition.hs @@ -111,7 +111,6 @@ import Kore.Internal.TermLike ( TermLike, isConstructorLike, pattern App_, - pattern Equals_, pattern Exists_, pattern Forall_, pattern Inj_, @@ -562,7 +561,7 @@ simplifyConjunctionByAssumption (toList -> andPredicates) = assumeEqualTerms = case predicate of PredicateEquals t1 t2 -> - case retractLocalFunction (TermLike.mkEquals_ t1 t2) of + case retractLocalFunction (Predicate.makeEqualsPredicate t1 t2) of Just (Pair t1' t2') -> Lens.over (field @"termLikeMap") $ HashMap.insert t1' t2' @@ -667,11 +666,11 @@ in either order, but the function pattern is always returned first in the 'Pair'. -} retractLocalFunction :: - TermLike variable -> + Predicate variable -> Maybe (Pair (TermLike variable)) retractLocalFunction = \case - Equals_ _ _ term1 term2 -> go term1 term2 <|> go term2 term1 + PredicateEquals term1 term2 -> go term1 term2 <|> go term2 term1 _ -> Nothing where go term1@(App_ symbol1 _) term2 diff --git a/kore/src/Kore/Internal/TermLike.hs b/kore/src/Kore/Internal/TermLike.hs index fcecd64f91..9a270b494e 100644 --- a/kore/src/Kore/Internal/TermLike.hs +++ b/kore/src/Kore/Internal/TermLike.hs @@ -36,10 +36,10 @@ module Kore.Internal.TermLike ( retractKey, refreshSetBinder, depth, - makeSortsAgree, + checkSortsAgree, -- * Utility functions for dealing with sorts - forceSort, + sameTermLikeSort, fullyOverrideSort, -- * Reachability modalities and application @@ -90,14 +90,6 @@ module Kore.Internal.TermLike ( mkEndianness, mkSignedness, - -- * Predicate constructors - mkBottom_, - mkCeil_, - mkEquals_, - mkFloor_, - mkIn_, - mkTop_, - -- * Sentence constructors mkAlias, mkAlias_, @@ -590,27 +582,18 @@ checkedSimplifiedFromChildren termLikeF = termLikeSort :: TermLike variable -> Sort termLikeSort = termSort . extractAttributes --- | Attempts to modify p to have sort s. -forceSort :: +-- | Check the given `TermLike` has the same sort as that supplied +sameTermLikeSort :: (InternalVariable variable, HasCallStack) => + -- | expected sort Sort -> TermLike variable -> TermLike variable -forceSort forcedSort = - if forcedSort == predicateSort - then id - else Recursive.apo forceSortWorker +sameTermLikeSort expectedSort term + | expectedSort == termSort = term + | otherwise = illSorted expectedSort term where - forceSortWorker original@(Recursive.project -> attrs :< pattern') = - (:<) - (attrs{termSort = forcedSort}) - ( case attrs of - TermAttributes{termSort = sort} - | sort == forcedSort -> Left <$> pattern' - | sort == predicateSort -> - forceSortPredicate forcedSort original - | otherwise -> illSorted forcedSort original - ) + termSort = termLikeSort term {- | Attempts to modify the pattern to have the given sort, ignoring the previous sort and without assuming that the pattern's sorts are consistent. @@ -723,35 +706,15 @@ forceSortPredicate SignednessF _ -> illSorted forcedSort original InjF _ -> illSorted forcedSort original -{- | Call the argument function with two patterns whose sorts agree. - -If one pattern is flexibly sorted, the result is the rigid sort of the other -pattern. If both patterns are flexibly sorted, then the result is -'predicateSort'. If both patterns have the same rigid sort, that is the -result. It is an error if the patterns are rigidly sorted but do not have the -same sort. --} -makeSortsAgree :: - (InternalVariable variable, HasCallStack) => +checkSortsAgree :: (TermLike variable -> TermLike variable -> Sort -> a) -> TermLike variable -> TermLike variable -> a -makeSortsAgree withPatterns = \pattern1 pattern2 -> - let sort1 = getRigidSort pattern1 - sort2 = getRigidSort pattern2 - sort = fromMaybe predicateSort (sort1 <|> sort2) - !pattern1' = forceSort sort pattern1 - !pattern2' = forceSort sort pattern2 - in withPatterns pattern1' pattern2' sort -{-# INLINE makeSortsAgree #-} - -getRigidSort :: TermLike variable -> Maybe Sort -getRigidSort pattern' = - case termLikeSort pattern' of - sort - | sort == predicateSort -> Nothing - | otherwise -> Just sort +checkSortsAgree withPatterns t1 t2 = withPatterns t1 t2 (sameSort s1 s2) + where + s1 = termLikeSort t1 + s2 = termLikeSort t2 -- | Construct an 'And' pattern. mkAnd :: @@ -760,7 +723,7 @@ mkAnd :: TermLike variable -> TermLike variable -> TermLike variable -mkAnd t1 t2 = updateCallStack $ makeSortsAgree mkAndWorker t1 t2 +mkAnd t1 t2 = updateCallStack $ checkSortsAgree mkAndWorker t1 t2 where mkAndWorker andFirst andSecond andSort = synthesize (AndF And{andSort, andFirst, andSecond}) @@ -769,23 +732,21 @@ mkAnd t1 t2 = updateCallStack $ makeSortsAgree mkAndWorker t1 t2 It is an error if the lists are not the same length, or if any 'TermLike' cannot be coerced to its corresponding 'Sort'. - -See also: 'forceSort' -} -forceSorts :: +sameTermLikeSorts :: HasCallStack => InternalVariable variable => [Sort] -> [TermLike variable] -> [TermLike variable] -forceSorts operandSorts children = +sameTermLikeSorts operandSorts children = alignWith forceTheseSorts operandSorts children where forceTheseSorts (This _) = (error . show . Pretty.vsep) ("Too few arguments:" : expected) forceTheseSorts (That _) = (error . show . Pretty.vsep) ("Too many arguments:" : expected) - forceTheseSorts (These sort termLike) = forceSort sort termLike + forceTheseSorts (These sort termLike) = sameTermLikeSort sort termLike expected = [ "Expected:" , Pretty.indent 4 (Unparser.arguments operandSorts) @@ -815,7 +776,7 @@ mkApplyAlias alias children = application = Application { applicationSymbolOrAlias = alias - , applicationChildren = forceSorts operandSorts children + , applicationChildren = sameTermLikeSorts operandSorts children } operandSorts = applicationSortsOperands (aliasSorts alias) @@ -850,7 +811,7 @@ symbolApplication :: symbolApplication symbol children = Application { applicationSymbolOrAlias = symbol - , applicationChildren = forceSorts operandSorts children + , applicationChildren = sameTermLikeSorts operandSorts children } where operandSorts = applicationSortsOperands (symbolSorts symbol) @@ -898,7 +859,7 @@ applyAlias sentence params children = where forceChildSort = \case - These sort pattern' -> forceSort sort pattern' + These sort pattern' -> sameTermLikeSort sort pattern' This _ -> (error . show . Pretty.vsep) ("Too few parameters:" : expected) @@ -971,10 +932,7 @@ applySymbol_ :: TermLike variable applySymbol_ sentence = updateCallStack . applySymbol sentence [] -{- | Construct a 'Bottom' pattern in the given sort. - -See also: 'mkBottom_' --} +-- | Construct a 'Bottom' pattern in the given sort. mkBottom :: HasCallStack => InternalVariable variable => @@ -983,23 +941,7 @@ mkBottom :: mkBottom bottomSort = updateCallStack $ synthesize (BottomF Bottom{bottomSort}) -{- | Construct a 'Bottom' pattern in 'predicateSort'. - -This should not be used outside "Kore.Internal.Predicate"; please use -'mkBottom' instead. - -See also: 'mkBottom' --} -mkBottom_ :: - HasCallStack => - InternalVariable variable => - TermLike variable -mkBottom_ = updateCallStack $ mkBottom predicateSort - -{- | Construct a 'Ceil' pattern in the given sort. - -See also: 'mkCeil_' --} +-- | Construct a 'Ceil' pattern in the given sort. mkCeil :: HasCallStack => InternalVariable variable => @@ -1012,20 +954,6 @@ mkCeil ceilResultSort ceilChild = where ceilOperandSort = termLikeSort ceilChild -{- | Construct a 'Ceil' pattern in 'predicateSort'. - -This should not be used outside "Kore.Internal.Predicate"; please use 'mkCeil' -instead. - -See also: 'mkCeil' --} -mkCeil_ :: - HasCallStack => - InternalVariable variable => - TermLike variable -> - TermLike variable -mkCeil_ = updateCallStack . mkCeil predicateSort - -- | Construct an internal bool pattern. mkInternalBool :: HasCallStack => @@ -1082,10 +1010,7 @@ mkDomainValue :: TermLike variable mkDomainValue = updateCallStack . synthesize . DomainValueF -{- | Construct an 'Equals' pattern in the given sort. - -See also: 'mkEquals_' --} +-- | Construct an 'Equals' pattern in the given sort. mkEquals :: HasCallStack => InternalVariable variable => @@ -1094,7 +1019,7 @@ mkEquals :: TermLike variable -> TermLike variable mkEquals equalsResultSort t1 = - updateCallStack . makeSortsAgree mkEqualsWorker t1 + updateCallStack . checkSortsAgree mkEqualsWorker t1 where mkEqualsWorker equalsFirst equalsSecond equalsOperandSort = synthesize (EqualsF equals) @@ -1107,21 +1032,6 @@ mkEquals equalsResultSort t1 = , equalsSecond } -{- | Construct a 'Equals' pattern in 'predicateSort'. - -This should not be used outside "Kore.Internal.Predicate"; please use -'mkEquals' instead. - -See also: 'mkEquals' --} -mkEquals_ :: - HasCallStack => - InternalVariable variable => - TermLike variable -> - TermLike variable -> - TermLike variable -mkEquals_ t1 t2 = updateCallStack $ mkEquals predicateSort t1 t2 - -- | Construct an 'Exists' pattern. mkExists :: HasCallStack => @@ -1145,10 +1055,7 @@ mkExistsN :: TermLike variable mkExistsN = (updateCallStack .) . appEndo . foldMap (Endo . mkExists) -{- | Construct a 'Floor' pattern in the given sort. - -See also: 'mkFloor_' --} +-- | Construct a 'Floor' pattern in the given sort. mkFloor :: HasCallStack => InternalVariable variable => @@ -1161,20 +1068,6 @@ mkFloor floorResultSort floorChild = where floorOperandSort = termLikeSort floorChild -{- | Construct a 'Floor' pattern in 'predicateSort'. - -This should not be used outside "Kore.Internal.Predicate"; please use 'mkFloor' -instead. - -See also: 'mkFloor' --} -mkFloor_ :: - HasCallStack => - InternalVariable variable => - TermLike variable -> - TermLike variable -mkFloor_ = updateCallStack . mkFloor predicateSort - -- | Construct a 'Forall' pattern. mkForall :: HasCallStack => @@ -1205,7 +1098,7 @@ mkIff :: TermLike variable -> TermLike variable -> TermLike variable -mkIff t1 t2 = updateCallStack $ makeSortsAgree mkIffWorker t1 t2 +mkIff t1 t2 = updateCallStack $ checkSortsAgree mkIffWorker t1 t2 where mkIffWorker iffFirst iffSecond iffSort = synthesize (IffF Iff{iffSort, iffFirst, iffSecond}) @@ -1217,7 +1110,7 @@ mkImplies :: TermLike variable -> TermLike variable -> TermLike variable -mkImplies t1 t2 = updateCallStack $ makeSortsAgree mkImpliesWorker t1 t2 +mkImplies t1 t2 = updateCallStack $ checkSortsAgree mkImpliesWorker t1 t2 where mkImpliesWorker impliesFirst impliesSecond impliesSort = synthesize (ImpliesF implies') @@ -1235,7 +1128,7 @@ mkIn :: TermLike variable -> TermLike variable -> TermLike variable -mkIn inResultSort t1 t2 = updateCallStack $ makeSortsAgree mkInWorker t1 t2 +mkIn inResultSort t1 t2 = updateCallStack $ checkSortsAgree mkInWorker t1 t2 where mkInWorker inContainedChild inContainingChild inOperandSort = synthesize (InF in') @@ -1248,21 +1141,6 @@ mkIn inResultSort t1 t2 = updateCallStack $ makeSortsAgree mkInWorker t1 t2 , inContainingChild } -{- | Construct a 'In' pattern in 'predicateSort'. - -This should not be used outside "Kore.Internal.Predicate"; please use 'mkIn' -instead. - -See also: 'mkIn' --} -mkIn_ :: - HasCallStack => - InternalVariable variable => - TermLike variable -> - TermLike variable -> - TermLike variable -mkIn_ t1 t2 = updateCallStack $ mkIn predicateSort t1 t2 - -- | Construct a 'Mu' pattern. mkMu :: HasCallStack => @@ -1270,7 +1148,7 @@ mkMu :: SetVariable variable -> TermLike variable -> TermLike variable -mkMu muVar = updateCallStack . makeSortsAgree mkMuWorker (mkSetVar muVar) +mkMu muVar = updateCallStack . checkSortsAgree mkMuWorker (mkSetVar muVar) where mkMuWorker (SetVar_ muVar') muChild _ = synthesize (MuF Mu{muVariable = muVar', muChild}) @@ -1305,7 +1183,7 @@ mkNu :: SetVariable variable -> TermLike variable -> TermLike variable -mkNu nuVar = updateCallStack . makeSortsAgree mkNuWorker (mkSetVar nuVar) +mkNu nuVar = updateCallStack . checkSortsAgree mkNuWorker (mkSetVar nuVar) where mkNuWorker (SetVar_ nuVar') nuChild _ = synthesize (NuF Nu{nuVariable = nuVar', nuChild}) @@ -1318,7 +1196,7 @@ mkOr :: TermLike variable -> TermLike variable -> TermLike variable -mkOr t1 t2 = updateCallStack $ makeSortsAgree mkOrWorker t1 t2 +mkOr t1 t2 = updateCallStack $ checkSortsAgree mkOrWorker t1 t2 where mkOrWorker orFirst orSecond orSort = synthesize (OrF Or{orSort, orFirst, orSecond}) @@ -1330,7 +1208,7 @@ mkRewrites :: TermLike variable -> TermLike variable -> TermLike variable -mkRewrites t1 t2 = updateCallStack $ makeSortsAgree mkRewritesWorker t1 t2 +mkRewrites t1 t2 = updateCallStack $ checkSortsAgree mkRewritesWorker t1 t2 where mkRewritesWorker rewritesFirst rewritesSecond rewritesSort = synthesize (RewritesF rewrites') @@ -1349,19 +1227,6 @@ mkTop :: mkTop topSort = updateCallStack $ synthesize (TopF Top{topSort}) -{- | Construct a 'Top' pattern in 'predicateSort'. - -This should not be used outside "Kore.Internal.Predicate"; please use -'mkTop' instead. - -See also: 'mkTop' --} -mkTop_ :: - HasCallStack => - InternalVariable variable => - TermLike variable -mkTop_ = updateCallStack $ mkTop predicateSort - -- | Construct an element variable pattern. mkElemVar :: HasCallStack => diff --git a/kore/src/Kore/ModelChecker/Simplification.hs b/kore/src/Kore/ModelChecker/Simplification.hs index 3f43564cf9..3e52f140bd 100644 --- a/kore/src/Kore/ModelChecker/Simplification.hs +++ b/kore/src/Kore/ModelChecker/Simplification.hs @@ -21,12 +21,13 @@ import qualified Kore.Internal.Predicate as Predicate import Kore.Internal.TermLike ( TermLike, mkAnd, - mkCeil_, + mkCeil, mkElemVar, mkNot, pattern Forall_, pattern Implies_, ) +import qualified Kore.Internal.TermLike as TermLike import Kore.Rewrite.RewritingVariable ( RewritingVariableName, ) @@ -59,7 +60,8 @@ checkImplicationIsTop lhs rhs = implicationLHS' = substitute subst implicationLHS implicationRHS' = substitute subst implicationRHS resultTerm = - mkCeil_ + mkCeil + sort ( mkAnd (mkAnd lhsMLPatt implicationLHS') (mkNot implicationRHS') @@ -87,6 +89,7 @@ checkImplicationIsTop lhs rhs = & map variableName & Set.fromList lhsMLPatt = Pattern.toTermLike lhs + sort = TermLike.termLikeSort rhs stripForallQuantifiers :: TermLike RewritingVariableName -> diff --git a/kore/src/Kore/ModelChecker/Step.hs b/kore/src/Kore/ModelChecker/Step.hs index 21ffa2b4d7..50f1530239 100644 --- a/kore/src/Kore/ModelChecker/Step.hs +++ b/kore/src/Kore/ModelChecker/Step.hs @@ -201,8 +201,9 @@ transitionRule transitionComputeWeakNext _ (Unprovable config) = return (Unprovable config) transitionComputeWeakNext rules (GoalLHS config) = transitionComputeWeakNextHelper rules config - transitionComputeWeakNext _ (GoalRemLHS _) = - return (GoalLHS Pattern.bottom) + transitionComputeWeakNext _ (GoalRemLHS pat) = + let patSort = Pattern.patternSort pat + in return (GoalLHS (Pattern.bottomOf patSort)) transitionComputeWeakNextHelper :: [RewriteRule RewritingVariableName] -> diff --git a/kore/src/Kore/Reachability/Claim.hs b/kore/src/Kore/Reachability/Claim.hs index b32ebe7baa..fafcf83da5 100644 --- a/kore/src/Kore/Reachability/Claim.hs +++ b/kore/src/Kore/Reachability/Claim.hs @@ -97,6 +97,8 @@ import Kore.Internal.Symbol ( Symbol, ) import Kore.Internal.TermLike ( + Not (..), + Sort, isFunctionPattern, mkIn, termLikeSort, @@ -275,13 +277,14 @@ deriveSeqClaim lensClaimPattern mkClaim claims claim = fmap (snd . Step.refreshRule mempty) $ Lens.forOf (field @"left") claimPattern $ \config -> Compose $ do + let claimPatSort = ClaimPattern.getClaimPatternSort claimPattern results <- Step.applyClaimsSequence mkClaim config (Lens.view lensClaimPattern <$> claims) & lift - deriveResults fromAppliedRule results + deriveResults claimPatSort fromAppliedRule results where fromAppliedRule = AppliedClaim @@ -556,8 +559,11 @@ checkImplicationWorker (ClaimPattern.refreshExistentials -> claimPattern) = Exists.makeEvaluate sideCondition existentials removed >>= Logic.scatter & OrPattern.observeAllT - & (>>= Not.simplifyEvaluated sideCondition) + & (>>= mkNotSimplified) & wereAnyUnified + where + mkNotSimplified notChild = + Not.simplify sideCondition Not{notSort = sort, notChild} wereAnyUnified :: StateT AnyUnified m a -> m (AnyUnified, a) wereAnyUnified act = swap <$> runStateT act mempty @@ -676,8 +682,9 @@ deriveWith lensClaimPattern mkRule takeStep rewrites claim = fmap (snd . Step.refreshRule mempty) $ Lens.forOf (field @"left") claimPattern $ \config -> Compose $ do + let claimPatSort = ClaimPattern.getClaimPatternSort claimPattern results <- takeStep rewrites config & lift - deriveResults fromAppliedRule results + deriveResults claimPatSort fromAppliedRule results where fromAppliedRule = AppliedAxiom @@ -699,6 +706,7 @@ deriveSeq' lensRulePattern mkRule = deriveResults :: Step.UnifyingRuleVariable representation ~ RewritingVariableName => + Sort -> (Step.UnifiedRule representation -> AppliedRule claim) -> Step.Results representation -> Strategy.TransitionT @@ -706,7 +714,7 @@ deriveResults :: simplifier (ApplyResult (Pattern RewritingVariableName)) -- TODO (thomas.tuegel): Remove claim argument. -deriveResults fromAppliedRule Results{results, remainders} = +deriveResults sort fromAppliedRule Results{results, remainders} = addResults <|> addRemainders where addResults = asum (addResult <$> results) @@ -715,7 +723,7 @@ deriveResults fromAppliedRule Results{results, remainders} = addResult Result{appliedRule, result} = do addRule appliedRule case toList result of - [] -> addRewritten Pattern.bottom + [] -> addRewritten (Pattern.bottomOf sort) configs -> asum (addRewritten <$> configs) addRewritten = pure . ApplyRewritten diff --git a/kore/src/Kore/Reachability/Prove.hs b/kore/src/Kore/Reachability/Prove.hs index d33b144c30..e95ec798e9 100644 --- a/kore/src/Kore/Reachability/Prove.hs +++ b/kore/src/Kore/Reachability/Prove.hs @@ -76,6 +76,7 @@ import Kore.Internal.Predicate ( pattern PredicateCeil, pattern PredicateNot, ) +import Kore.Internal.TermLike (Sort) import Kore.Log.DebugBeginClaim import Kore.Log.DebugProven import Kore.Log.DebugTransition ( @@ -144,16 +145,17 @@ type CommonTransitionRule m = the configuration will be '\\bottom'. -} lhsClaimStateTransformer :: + Sort -> ClaimStateTransformer SomeClaim (Pattern RewritingVariableName) -lhsClaimStateTransformer = +lhsClaimStateTransformer sort = ClaimStateTransformer { claimedTransformer = getConfiguration , remainingTransformer = getConfiguration , rewrittenTransformer = getConfiguration , stuckTransformer = getConfiguration - , provenValue = Pattern.bottom + , provenValue = Pattern.bottomOf sort } {- | @Verifer a@ is a 'Simplifier'-based action which returns an @a@. diff --git a/kore/src/Kore/Repl/Interpreter.hs b/kore/src/Kore/Repl/Interpreter.hs index c47dfd5307..36c7bdaec4 100644 --- a/kore/src/Kore/Repl/Interpreter.hs +++ b/kore/src/Kore/Repl/Interpreter.hs @@ -139,6 +139,8 @@ import qualified Kore.Internal.SideCondition as SideCondition ( fromConditionWithReplacements, ) import Kore.Internal.TermLike ( + Sort (..), + SortVariable (..), TermLike, ) import qualified Kore.Internal.TermLike as TermLike @@ -1393,8 +1395,11 @@ prettyClaimStateComponent transformation omitList = , provenValue = makeAuxReplOutput "Proven." } where + -- Sort variable used to unparse configurations. + -- This is only used for unparsing \bottom. + dummySort = SortVariableSort (SortVariable "R") prettyComponent = - unparseToString . OrPattern.toTermLike + unparseToString . OrPattern.toTermLike dummySort . MultiOr.map (fmap hide . getRewritingPattern) . transformation hide :: diff --git a/kore/src/Kore/Rewrite/ClaimPattern.hs b/kore/src/Kore/Rewrite/ClaimPattern.hs index d031cb5d69..a721cc2bab 100644 --- a/kore/src/Kore/Rewrite/ClaimPattern.hs +++ b/kore/src/Kore/Rewrite/ClaimPattern.hs @@ -15,6 +15,7 @@ module Kore.Rewrite.ClaimPattern ( forgetSimplified, parseRightHandSide, claimPatternToTerm, + getClaimPatternSort, ) where import Control.Error.Util ( @@ -62,6 +63,7 @@ import Kore.Internal.TermLike ( Modality, SomeVariable, SomeVariableName (..), + Sort, TermLike, Variable (..), VariableName, @@ -122,7 +124,7 @@ instance Pretty ClaimPattern where , "existentials:" , Pretty.indent 4 (Pretty.list $ unparse <$> existentials) , "right:" - , Pretty.indent 4 (unparse $ OrPattern.toTermLike right) + , Pretty.indent 4 (unparse $ OrPattern.toTermLike sort right) ] where ClaimPattern @@ -130,6 +132,7 @@ instance Pretty ClaimPattern where , right , existentials } = claimPattern' + sort = getClaimPatternSort claimPattern' instance TopBottom ClaimPattern where isTop _ = False @@ -138,6 +141,12 @@ instance TopBottom ClaimPattern where instance From ClaimPattern Attribute.PriorityAttributes where from = from @(Attribute.Axiom _ _) . attributes +getClaimPatternSort :: + ClaimPattern -> + Sort +getClaimPatternSort (ClaimPattern left _ _ _) = + Pattern.patternSort left + freeVariablesRight :: ClaimPattern -> FreeVariables RewritingVariableName @@ -145,10 +154,11 @@ freeVariablesRight claimPattern'@(ClaimPattern _ _ _ _) = freeVariables ( TermLike.mkExistsN existentials - (OrPattern.toTermLike right) + (OrPattern.toTermLike sort right) ) where ClaimPattern{right, existentials} = claimPattern' + sort = getClaimPatternSort claimPattern' freeVariablesLeft :: ClaimPattern -> @@ -231,7 +241,7 @@ claimPatternToTerm modality representation@(ClaimPattern _ _ _ _) = & Pattern.toTermLike & getRewritingTerm rightPattern = - TermLike.mkExistsN existentials (OrPattern.toTermLike right) + TermLike.mkExistsN existentials (OrPattern.toTermLike sort right) & getRewritingTerm substituteRight :: diff --git a/kore/src/Kore/Rewrite/Implication.hs b/kore/src/Kore/Rewrite/Implication.hs index 2b1cd4d96f..6a8edfa9ae 100644 --- a/kore/src/Kore/Rewrite/Implication.hs +++ b/kore/src/Kore/Rewrite/Implication.hs @@ -64,6 +64,7 @@ import Kore.Internal.TermLike ( Modality, SomeVariable, SomeVariableName (..), + Sort, TermLike, Variable (..), VariableName, @@ -126,7 +127,7 @@ instance Pretty (Implication modality) where , "existentials:" , Pretty.indent 4 (Pretty.list $ unparse <$> existentials) , "right:" - , Pretty.indent 4 (unparse $ OrPattern.toTermLike right) + , Pretty.indent 4 (pretty right) ] where Implication @@ -142,6 +143,11 @@ instance TopBottom (Implication modality) where instance From (Implication modality) Attribute.PriorityAttributes where from = from @(Attribute.Axiom _ _) . attributes +getImplicationSort :: + Implication modality -> + Sort +getImplicationSort (Implication left _ _ _ _) = Pattern.patternSort left + freeVariablesRight :: Implication modality -> FreeVariables RewritingVariableName @@ -149,9 +155,10 @@ freeVariablesRight implication'@(Implication _ _ _ _ _) = freeVariables ( TermLike.mkExistsN existentials - (OrPattern.toTermLike right) + (OrPattern.toTermLike sort right) ) where + sort = getImplicationSort implication' Implication{right, existentials} = implication' freeVariablesLeft :: @@ -229,14 +236,14 @@ implicationToTerm representation@(Implication _ _ _ _ _) = leftTerm = Pattern.term left & getRewritingTerm - sort = TermLike.termLikeSort leftTerm + sort = getImplicationSort representation leftCondition = Pattern.withoutTerm left & Condition.toPredicate & Predicate.fromPredicate sort & getRewritingTerm rightPattern = - TermLike.mkExistsN existentials (OrPattern.toTermLike right) + TermLike.mkExistsN existentials (OrPattern.toTermLike sort right) & getRewritingTerm substituteRight :: diff --git a/kore/src/Kore/Rewrite/Remainder.hs b/kore/src/Kore/Rewrite/Remainder.hs index cd6dafcf4f..a4b36adad7 100644 --- a/kore/src/Kore/Rewrite/Remainder.hs +++ b/kore/src/Kore/Rewrite/Remainder.hs @@ -134,7 +134,7 @@ ceilChildOfApplicationOrTop sideCondition patt = case patt of App_ _ children -> do ceil <- - traverse (Ceil.makeEvaluateTerm sideCondition) children + traverse (Ceil.makeEvaluateTerm termSort sideCondition) children >>= ( AndPredicates.simplifyEvaluatedMultiPredicate sideCondition . MultiAnd.make @@ -149,3 +149,5 @@ ceilChildOfApplicationOrTop sideCondition patt = , substitution = mempty } _ -> pure Condition.top + where + termSort = termLikeSort patt diff --git a/kore/src/Kore/Rewrite/Rule.hs b/kore/src/Kore/Rewrite/Rule.hs index 719c79db99..a555cac2ff 100644 --- a/kore/src/Kore/Rewrite/Rule.hs +++ b/kore/src/Kore/Rewrite/Rule.hs @@ -427,7 +427,7 @@ mkEqualityAxiom lhs rhs requires = Just requires' -> TermLike.mkImplies (requires' sortR) - (TermLike.mkAnd function TermLike.mkTop_) + (TermLike.mkAnd function (TermLike.mkTop sortR)) Nothing -> function where sortVariableR = SortVariable "R" diff --git a/kore/src/Kore/Rewrite/RulePattern.hs b/kore/src/Kore/Rewrite/RulePattern.hs index 0e6f049c0b..e68c3d8c88 100644 --- a/kore/src/Kore/Rewrite/RulePattern.hs +++ b/kore/src/Kore/Rewrite/RulePattern.hs @@ -88,6 +88,7 @@ import Kore.Internal.Symbol ( import Kore.Internal.TermLike ( TermLike, mkVar, + termLikeSort, ) import qualified Kore.Internal.TermLike as TermLike import Kore.Internal.Variable ( @@ -325,11 +326,14 @@ lhsToTerm :: Predicate variable -> TermLike variable lhsToTerm left Nothing requires = - TermLike.mkAnd (Predicate.fromPredicate_ requires) left + TermLike.mkAnd (Predicate.fromPredicate (termLikeSort left) requires) left lhsToTerm left (Just antiLeft) requires = TermLike.mkAnd (TermLike.mkNot (AntiLeft.toTermLike antiLeft)) - (TermLike.mkAnd (Predicate.fromPredicate_ requires) left) + ( TermLike.mkAnd + (Predicate.fromPredicate (termLikeSort left) requires) + left + ) -- | Wraps a term as a RHS injectTermIntoRHS :: diff --git a/kore/src/Kore/Rewrite/Search.hs b/kore/src/Kore/Rewrite/Search.hs index e2cdfd0ca7..600352b6cf 100644 --- a/kore/src/Kore/Rewrite/Search.hs +++ b/kore/src/Kore/Rewrite/Search.hs @@ -131,9 +131,9 @@ matchWith :: MaybeT m (OrCondition RewritingVariableName) matchWith sideCondition e1 e2 = do unifiers <- - lift $ - Unifier.runUnifierT Not.notSimplifier $ - unificationProcedure sideCondition t1 t2 + unificationProcedure sideCondition t1 t2 + & Unifier.runUnifierT Not.notSimplifier + & lift let mergeAndEvaluate :: Condition RewritingVariableName -> m (OrCondition RewritingVariableName) diff --git a/kore/src/Kore/Simplify/And.hs b/kore/src/Kore/Simplify/And.hs index 00fa6a5e8b..affe01b899 100644 --- a/kore/src/Kore/Simplify/And.hs +++ b/kore/src/Kore/Simplify/And.hs @@ -41,9 +41,10 @@ import Kore.Internal.SideCondition ( ) import Kore.Internal.TermLike ( And (..), + Sort, TermLike, mkAnd, - mkBottom_, + mkBottom, mkNot, pattern And_, pattern Not_, @@ -99,14 +100,15 @@ Also, we have -} simplify :: MonadSimplify simplifier => + Sort -> NotSimplifier (UnifierT simplifier) -> SideCondition RewritingVariableName -> MultiAnd (OrPattern RewritingVariableName) -> simplifier (OrPattern RewritingVariableName) -simplify notSimplifier sideCondition orPatterns = +simplify resultSort notSimplifier sideCondition orPatterns = OrPattern.observeAllT $ do patterns <- MultiAnd.traverse scatter orPatterns - makeEvaluate notSimplifier sideCondition patterns + makeEvaluate resultSort notSimplifier sideCondition patterns {- | 'makeEvaluate' simplifies a 'MultiAnd' of 'Pattern's. See the comment for 'simplify' to find more details. @@ -115,24 +117,26 @@ makeEvaluate :: forall simplifier. HasCallStack => MonadSimplify simplifier => + Sort -> NotSimplifier (UnifierT simplifier) -> SideCondition RewritingVariableName -> MultiAnd (Pattern RewritingVariableName) -> LogicT simplifier (Pattern RewritingVariableName) -makeEvaluate notSimplifier sideCondition patterns +makeEvaluate resultSort notSimplifier sideCondition patterns | isBottom patterns = empty - | Pattern.isTop patterns = return Pattern.top - | otherwise = makeEvaluateNonBool notSimplifier sideCondition patterns + | Pattern.isTop patterns = return (Pattern.topOf resultSort) + | otherwise = makeEvaluateNonBool resultSort notSimplifier sideCondition patterns makeEvaluateNonBool :: forall simplifier. HasCallStack => MonadSimplify simplifier => + Sort -> NotSimplifier (UnifierT simplifier) -> SideCondition RewritingVariableName -> MultiAnd (Pattern RewritingVariableName) -> LogicT simplifier (Pattern RewritingVariableName) -makeEvaluateNonBool notSimplifier sideCondition patterns = do +makeEvaluateNonBool resultSort notSimplifier sideCondition patterns = do let unify pattern1 term2 = do let (term1, condition1) = Pattern.splitTerm pattern1 unified <- termAnd notSimplifier term1 term2 @@ -140,7 +144,7 @@ makeEvaluateNonBool notSimplifier sideCondition patterns = do unified <- foldlM unify - Pattern.top + (Pattern.topOf resultSort) (term <$> toList patterns) let substitutions = Pattern.substitution unified @@ -172,8 +176,9 @@ applyAndIdempotenceAndFindContradictions :: applyAndIdempotenceAndFindContradictions patt = if noContradictions then foldl1' mkAndSimplified . Set.toList $ Set.union terms negatedTerms - else mkBottom_ + else mkBottom sort where + sort = TermLike.termLikeSort patt (terms, negatedTerms) = splitIntoTermsAndNegations patt noContradictions = Set.disjoint (Set.map mkNot terms) negatedTerms mkAndSimplified a b = diff --git a/kore/src/Kore/Simplify/AndTerms.hs b/kore/src/Kore/Simplify/AndTerms.hs index 7fe6f8830e..ba9da59c7d 100644 --- a/kore/src/Kore/Simplify/AndTerms.hs +++ b/kore/src/Kore/Simplify/AndTerms.hs @@ -79,6 +79,9 @@ import Kore.Simplify.NoConfusion import Kore.Simplify.NotSimplifier import Kore.Simplify.Overloading as Overloading import Kore.Simplify.Simplify as Simplifier +import Kore.Sort ( + sameSort, + ) import Kore.Unification.Unify as Unify import Kore.Unparser import Pair @@ -161,7 +164,11 @@ maybeTermEquals notSimplifier childTransformers first second = do | Just unifyData <- matchBytes first second = lift $ unifyBytes unifyData | Just unifyData <- matchBottomTermEquals first second = - lift $ bottomTermEquals SideCondition.topTODO unifyData + lift $ + bottomTermEquals + (sameSort (termLikeSort first) (termLikeSort second)) + SideCondition.topTODO + unifyData | Just unifyData <- matchVariableFunctionEquals first second = lift $ variableFunctionEquals unifyData | Just unifyData <- matchEqualInjectiveHeadsAndEquals first second = @@ -193,7 +200,12 @@ maybeTermEquals notSimplifier childTransformers first second = do | 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 + lift $ + Builtin.Map.unifyNotInKeys + (sameSort (termLikeSort first) (termLikeSort second)) + 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 = @@ -428,17 +440,19 @@ matchBottomTermEquals first second -- | Unify two patterns where the first is @\\bottom@. bottomTermEquals :: MonadUnify unifier => + Sort -> SideCondition RewritingVariableName -> BottomTermEquals -> unifier (Pattern RewritingVariableName) bottomTermEquals + resultSort sideCondition unifyData = do -- MonadUnify secondCeil <- makeEvaluateTermCeil sideCondition term case toList secondCeil of - [] -> return Pattern.top + [] -> return (Pattern.topOf resultSort) [Conditional{predicate = PredicateTrue, substitution}] | substitution == mempty -> debugUnifyBottomAndReturnBottom @@ -448,7 +462,7 @@ bottomTermEquals _ -> return Conditional - { term = mkTop_ + { term = mkTop resultSort , predicate = makeNotPredicate $ OrCondition.toPredicate $ diff --git a/kore/src/Kore/Simplify/Ceil.hs b/kore/src/Kore/Simplify/Ceil.hs index 047a9f8ece..92f2a4de83 100644 --- a/kore/src/Kore/Simplify/Ceil.hs +++ b/kore/src/Kore/Simplify/Ceil.hs @@ -69,7 +69,6 @@ import qualified Kore.Simplify.AndPredicates as And import Kore.Simplify.CeilSimplifier import Kore.Simplify.InjSimplifier import Kore.Simplify.Simplify as Simplifier -import qualified Kore.Sort as Sort import Kore.TopBottom import Kore.Unparser ( unparseToString, @@ -118,12 +117,13 @@ makeEvaluate sideCondition child | Pattern.isBottom child = return OrCondition.bottom | isTop term = return $ OrCondition.fromCondition condition | otherwise = do - termCeil <- makeEvaluateTerm sideCondition term + termCeil <- makeEvaluateTerm childSort sideCondition term And.simplifyEvaluatedMultiPredicate sideCondition (MultiAnd.make [MultiOr.make [condition], termCeil]) where (term, condition) = Pattern.splitTerm child + childSort = Pattern.patternSort child -- TODO: Ceil(function) should be an and of all the function's conditions, both -- implicit and explicit. @@ -132,15 +132,16 @@ makeEvaluate sideCondition child makeEvaluateTerm :: forall simplifier. MonadSimplify simplifier => + Sort -> SideCondition RewritingVariableName -> TermLike RewritingVariableName -> simplifier (OrCondition RewritingVariableName) -makeEvaluateTerm sideCondition ceilChild = +makeEvaluateTerm resultSort sideCondition ceilChild = runCeilSimplifierWith ceilSimplifier sideCondition Ceil - { ceilResultSort = Sort.predicateSort + { ceilResultSort = resultSort , ceilOperandSort = termLikeSort ceilChild , ceilChild } @@ -155,7 +156,7 @@ makeEvaluateTerm sideCondition ceilChild = -- \ceil conditions are reduced to Bool expressions using in_keys. newAxiomCeilSimplifier , newApplicationCeilSimplifier - , newBuiltinCeilSimplifier + , newBuiltinCeilSimplifier resultSort , newInjCeilSimplifier ] @@ -227,21 +228,22 @@ newInjCeilSimplifier = CeilSimplifier $ \input -> newBuiltinCeilSimplifier :: MonadReader (SideCondition RewritingVariableName) simplifier => MonadSimplify simplifier => + Sort -> CeilSimplifier simplifier (TermLike RewritingVariableName) (OrCondition RewritingVariableName) -newBuiltinCeilSimplifier = CeilSimplifier $ \input -> +newBuiltinCeilSimplifier ceilSort = CeilSimplifier $ \input -> case ceilChild input of InternalList_ internal -> do sideCondition <- Reader.ask - makeEvaluateInternalList sideCondition internal + makeEvaluateInternalList ceilSort sideCondition internal InternalMap_ internalMap -> do sideCondition <- Reader.ask - makeEvaluateInternalMap sideCondition internalMap + makeEvaluateInternalMap ceilSort sideCondition internalMap InternalSet_ internalSet -> do sideCondition <- Reader.ask - makeEvaluateInternalSet sideCondition internalSet + makeEvaluateInternalSet ceilSort sideCondition internalSet _ -> empty newAxiomCeilSimplifier :: @@ -277,15 +279,16 @@ newAxiomCeilSimplifier = CeilSimplifier $ \input -> do makeEvaluateInternalMap :: forall simplifier. MonadSimplify simplifier => + Sort -> SideCondition RewritingVariableName -> InternalMap Key (TermLike RewritingVariableName) -> MaybeT simplifier (OrCondition RewritingVariableName) -makeEvaluateInternalMap sideCondition internalMap = +makeEvaluateInternalMap resultSort sideCondition internalMap = runCeilSimplifierWith AssocComm.newMapCeilSimplifier sideCondition Ceil - { ceilResultSort = Sort.predicateSort + { ceilResultSort = resultSort , ceilOperandSort = builtinAcSort , ceilChild = internalMap } @@ -296,15 +299,16 @@ makeEvaluateInternalMap sideCondition internalMap = makeEvaluateInternalSet :: forall simplifier. MonadSimplify simplifier => + Sort -> SideCondition RewritingVariableName -> InternalSet Key (TermLike RewritingVariableName) -> MaybeT simplifier (OrCondition RewritingVariableName) -makeEvaluateInternalSet sideCondition internalSet = +makeEvaluateInternalSet resultSort sideCondition internalSet = runCeilSimplifierWith AssocComm.newSetCeilSimplifier sideCondition Ceil - { ceilResultSort = Sort.predicateSort + { ceilResultSort = resultSort , ceilOperandSort = builtinAcSort , ceilChild = internalSet } @@ -314,11 +318,12 @@ makeEvaluateInternalSet sideCondition internalSet = makeEvaluateInternalList :: forall simplifier. MonadSimplify simplifier => + Sort -> SideCondition RewritingVariableName -> InternalList (TermLike RewritingVariableName) -> simplifier (OrCondition RewritingVariableName) -makeEvaluateInternalList sideCondition internal = do - children <- mapM (makeEvaluateTerm sideCondition) (toList internal) +makeEvaluateInternalList listSort sideCondition internal = do + children <- mapM (makeEvaluateTerm listSort sideCondition) (toList internal) let ceils :: [OrCondition RewritingVariableName] ceils = children And.simplifyEvaluatedMultiPredicate sideCondition (MultiAnd.make ceils) @@ -349,12 +354,13 @@ makeSimplifiedCeil do childCeils <- if needsChildCeils - then mapM (makeEvaluateTerm sideCondition) (toList termLikeF) + then mapM (makeEvaluateTerm ceilSort sideCondition) (toList termLikeF) else return [] And.simplifyEvaluatedMultiPredicate sideCondition (MultiAnd.make (unsimplified : childCeils)) where + ceilSort = termLikeSort termLike needsChildCeils = case termLikeF of ApplyAliasF _ -> False EndiannessF _ -> True diff --git a/kore/src/Kore/Simplify/Equals.hs b/kore/src/Kore/Simplify/Equals.hs index 79eac812a6..9af31d0210 100644 --- a/kore/src/Kore/Simplify/Equals.hs +++ b/kore/src/Kore/Simplify/Equals.hs @@ -61,13 +61,14 @@ import qualified Kore.Simplify.Implies as Implies ( ) import qualified Kore.Simplify.Not as Not ( notSimplifier, - simplifyEvaluated, + simplify, simplifyEvaluatedPredicate, ) import qualified Kore.Simplify.Or as Or ( simplifyEvaluated, ) import Kore.Simplify.Simplify +import Kore.Sort (sameSort) import Kore.Unification.UnifierT ( runUnifierT, ) @@ -161,15 +162,20 @@ simplify :: SideCondition RewritingVariableName -> Equals Sort (OrPattern RewritingVariableName) -> simplifier (OrCondition RewritingVariableName) -simplify sideCondition Equals{equalsFirst = first, equalsSecond = second} = - simplifyEvaluated sideCondition first' second' - where - (first', second') = - minMaxBy (on compareForEquals OrPattern.toTermLike) first second +simplify + sideCondition + Equals + { equalsFirst = first + , equalsSecond = second + , equalsOperandSort = sort + } = simplifyEvaluated sort sideCondition first' second' + where + (first', second') = + minMaxBy (on compareForEquals (OrPattern.toTermLike sort)) first second -{- TODO (virgil): Preserve pattern sorts under simplification. +{- -One way to preserve the required sort annotations is to make 'simplifyEvaluated' +Another way to preserve the required sort annotations is to make 'simplifyEvaluated' take an argument of type > CofreeF (Equals Sort) (Attribute.Pattern variable) (OrPattern variable) @@ -182,11 +188,12 @@ carry around. -} simplifyEvaluated :: MonadSimplify simplifier => + Sort -> SideCondition RewritingVariableName -> OrPattern RewritingVariableName -> OrPattern RewritingVariableName -> simplifier (OrCondition RewritingVariableName) -simplifyEvaluated sideCondition first second +simplifyEvaluated sort sideCondition first second | first == second = return OrCondition.top -- TODO: Maybe simplify equalities with top and bottom to ceil and floor | otherwise = do @@ -202,12 +209,12 @@ simplifyEvaluated sideCondition first second makeEvaluateFunctionalOr sideCondition secondP firstPatterns _ | OrPattern.isPredicate first && OrPattern.isPredicate second -> - Iff.simplifyEvaluated sideCondition first second + Iff.simplifyEvaluated sort sideCondition first second & fmap (MultiOr.map Pattern.withoutTerm) | otherwise -> makeEvaluate - (OrPattern.toPattern first) - (OrPattern.toPattern second) + (OrPattern.toPattern sort first) + (OrPattern.toPattern sort second) sideCondition where firstPatterns = toList first @@ -221,36 +228,36 @@ makeEvaluateFunctionalOr :: [Pattern RewritingVariableName] -> simplifier (OrCondition RewritingVariableName) makeEvaluateFunctionalOr sideCondition first seconds = do - firstCeil <- makeEvaluateCeil sideCondition first - secondCeilsWithProofs <- mapM (makeEvaluateCeil sideCondition) seconds - firstNotCeil <- Not.simplifyEvaluated sideCondition firstCeil + let sort = Pattern.patternSort first + firstCeil <- makeEvaluateCeil sort sideCondition first + secondCeilsWithProofs <- mapM (makeEvaluateCeil sort sideCondition) seconds + let mkNotSimplified notChild = + Not.simplify sideCondition Not{notSort = sort, notChild} + firstNotCeil <- mkNotSimplified firstCeil let secondCeils = secondCeilsWithProofs - secondNotCeils <- traverse (Not.simplifyEvaluated sideCondition) secondCeils + secondNotCeils <- traverse mkNotSimplified secondCeils let oneNotBottom = foldl' Or.simplifyEvaluated OrPattern.bottom secondCeils allAreBottom <- - And.simplify - Not.notSimplifier - sideCondition + (And.simplify sort Not.notSimplifier sideCondition) (MultiAnd.make (firstNotCeil : secondNotCeils)) firstEqualsSeconds <- mapM - (makeEvaluateEqualsIfSecondNotBottom first) + (makeEvaluateEqualsIfSecondNotBottom sort first) (zip seconds secondCeils) oneIsNotBottomEquals <- - And.simplify - Not.notSimplifier - sideCondition + (And.simplify sort Not.notSimplifier sideCondition) (MultiAnd.make (firstCeil : oneNotBottom : firstEqualsSeconds)) MultiOr.merge allAreBottom oneIsNotBottomEquals & MultiOr.map Pattern.withoutTerm & return where makeEvaluateEqualsIfSecondNotBottom + sort Conditional{term = firstTerm} (Conditional{term = secondTerm}, secondCeil) = do equality <- makeEvaluateTermsAssumesNoBottom firstTerm secondTerm - Implies.simplifyEvaluated sideCondition secondCeil equality + Implies.simplifyEvaluated sort sideCondition secondCeil equality {- | evaluates an 'Equals' given its two 'Pattern' children. @@ -267,8 +274,8 @@ makeEvaluate second@Conditional{term = Top_ _} _ = Iff.makeEvaluate - first{term = mkTop_} -- remove the term's sort - second{term = mkTop_} -- remove the term's sort + first + second & MultiOr.map Pattern.withoutTerm & return makeEvaluate @@ -289,27 +296,26 @@ makeEvaluate second@Conditional{term = secondTerm} sideCondition = do - let first' = first{term = if termsAreEqual then mkTop_ else firstTerm} - firstCeil <- makeEvaluateCeil sideCondition first' - let second' = second{term = if termsAreEqual then mkTop_ else secondTerm} - secondCeil <- makeEvaluateCeil sideCondition second' - firstCeilNegation <- Not.simplifyEvaluated sideCondition firstCeil - secondCeilNegation <- Not.simplifyEvaluated sideCondition secondCeil + let first' = first{term = if termsAreEqual then mkTop sort else firstTerm} + firstCeil <- makeEvaluateCeil sort sideCondition first' + let second' = second{term = if termsAreEqual then mkTop sort else secondTerm} + secondCeil <- makeEvaluateCeil sort sideCondition second' + let mkNotSimplified notChild = + Not.simplify sideCondition Not{notSort = sort, notChild} + firstCeilNegation <- mkNotSimplified firstCeil + secondCeilNegation <- mkNotSimplified secondCeil termEquality <- makeEvaluateTermsAssumesNoBottom firstTerm secondTerm negationAnd <- - And.simplify - Not.notSimplifier - sideCondition + (And.simplify sort Not.notSimplifier sideCondition) (MultiAnd.make [firstCeilNegation, secondCeilNegation]) equalityAnd <- - And.simplify - Not.notSimplifier - sideCondition + (And.simplify sort Not.notSimplifier sideCondition) (MultiAnd.make [termEquality, firstCeil, secondCeil]) Or.simplifyEvaluated equalityAnd negationAnd & MultiOr.map Pattern.withoutTerm & return where + sort = sameSort (termLikeSort firstTerm) (termLikeSort secondTerm) termsAreEqual = firstTerm == secondTerm -- Do not export this. This not valid as a standalone function, it @@ -325,10 +331,11 @@ makeEvaluateTermsAssumesNoBottom firstTerm secondTerm = do makeEvaluateTermsAssumesNoBottomMaybe firstTerm secondTerm (return . fromMaybe def) result where + sort = termLikeSort firstTerm def = OrPattern.fromPattern Conditional - { term = mkTop_ + { term = mkTop sort , predicate = Predicate.markSimplified $ makeEqualsPredicate firstTerm secondTerm @@ -345,7 +352,8 @@ makeEvaluateTermsAssumesNoBottomMaybe :: MaybeT simplifier (OrPattern RewritingVariableName) makeEvaluateTermsAssumesNoBottomMaybe first second = do result <- termEquals first second - return (MultiOr.map Pattern.fromCondition_ result) + let sort = termLikeSort first + return (MultiOr.map (Pattern.fromCondition sort) result) {- | Combines two terms with 'Equals' into a predicate-substitution. diff --git a/kore/src/Kore/Simplify/Floor.hs b/kore/src/Kore/Simplify/Floor.hs index 4eb4b909b5..09e6969a8a 100644 --- a/kore/src/Kore/Simplify/Floor.hs +++ b/kore/src/Kore/Simplify/Floor.hs @@ -44,8 +44,8 @@ floor(a and b) = floor(a) and floor(b). simplify :: Floor Sort (OrPattern RewritingVariableName) -> OrPattern RewritingVariableName -simplify Floor{floorChild = child} = - simplifyEvaluatedFloor child +simplify Floor{floorResultSort = resultSort, floorChild = child} = + simplifyEvaluatedFloor resultSort child {- TODO (virgil): Preserve pattern sorts under simplification. @@ -61,35 +61,38 @@ to carry around. -} simplifyEvaluatedFloor :: + Sort -> OrPattern RewritingVariableName -> OrPattern RewritingVariableName -simplifyEvaluatedFloor child = +simplifyEvaluatedFloor resultSort child = case toList child of - [childP] -> makeEvaluateFloor childP - _ -> makeEvaluateFloor (OrPattern.toPattern child) + [childP] -> makeEvaluateFloor resultSort childP + _ -> makeEvaluateFloor resultSort (OrPattern.toPattern resultSort child) {- | 'makeEvaluateFloor' simplifies a 'Floor' of 'Pattern'. See 'simplify' for details. -} makeEvaluateFloor :: + Sort -> Pattern RewritingVariableName -> OrPattern RewritingVariableName -makeEvaluateFloor child - | Pattern.isTop child = OrPattern.top +makeEvaluateFloor resultSort child + | Pattern.isTop child = OrPattern.topOf resultSort | Pattern.isBottom child = OrPattern.bottom - | otherwise = makeEvaluateNonBoolFloor child + | otherwise = makeEvaluateNonBoolFloor resultSort child makeEvaluateNonBoolFloor :: + Sort -> Pattern RewritingVariableName -> OrPattern RewritingVariableName -makeEvaluateNonBoolFloor patt@Conditional{term = Top_ _} = - OrPattern.fromPattern patt{term = mkTop_} -- remove the term's sort +makeEvaluateNonBoolFloor resultSort patt@Conditional{term = Top_ _} = + OrPattern.fromPattern patt{term = mkTop resultSort} -- change the term's sort -- TODO(virgil): Also evaluate functional patterns to bottom for non-singleton -- sorts, and maybe other cases also -makeEvaluateNonBoolFloor patt = +makeEvaluateNonBoolFloor resultSort patt = floorCondition <> condition - & Pattern.fromCondition_ + & (Pattern.fromCondition resultSort) & OrPattern.fromPattern where (term, condition) = Pattern.splitTerm patt diff --git a/kore/src/Kore/Simplify/Forall.hs b/kore/src/Kore/Simplify/Forall.hs index ac62004a76..2044cc9fdf 100644 --- a/kore/src/Kore/Simplify/Forall.hs +++ b/kore/src/Kore/Simplify/Forall.hs @@ -29,13 +29,14 @@ import Kore.Internal.Pattern ( Pattern, ) import qualified Kore.Internal.Pattern as Pattern ( - bottom, + bottomOf, fromTermLike, isBottom, isTop, + patternSort, splitTerm, toTermLike, - top, + topOf, ) import Kore.Internal.Predicate ( makeForallPredicate, @@ -115,8 +116,8 @@ makeEvaluate :: Pattern RewritingVariableName -> Pattern RewritingVariableName makeEvaluate variable patt - | Pattern.isTop patt = Pattern.top - | Pattern.isBottom patt = Pattern.bottom + | Pattern.isTop patt = Pattern.topOf sort + | Pattern.isBottom patt = Pattern.bottomOf sort | not variableInTerm && not variableInCondition = patt | predicateIsBoolean = TermLike.markSimplified (mkForall variable term) @@ -133,6 +134,7 @@ makeEvaluate variable patt mkForall variable $ Pattern.toTermLike patt where + sort = Pattern.patternSort patt (term, predicate) = Pattern.splitTerm patt someVariable = mkSomeVariable variable someVariableName = variableName someVariable diff --git a/kore/src/Kore/Simplify/Iff.hs b/kore/src/Kore/Simplify/Iff.hs index 3abf99a946..b81c356602 100644 --- a/kore/src/Kore/Simplify/Iff.hs +++ b/kore/src/Kore/Simplify/Iff.hs @@ -40,7 +40,7 @@ import qualified Kore.Simplify.Implies as Implies ( import qualified Kore.Simplify.Not as Not ( makeEvaluate, notSimplifier, - simplifyEvaluated, + simplify, ) import Kore.Simplify.Simplify import Prelude.Kore @@ -56,8 +56,8 @@ simplify :: SideCondition RewritingVariableName -> Iff Sort (OrPattern RewritingVariableName) -> simplifier (OrPattern RewritingVariableName) -simplify sideCondition Iff{iffFirst = first, iffSecond = second} = - simplifyEvaluated sideCondition first second +simplify sideCondition Iff{iffFirst = first, iffSecond = second, iffSort = sort} = + simplifyEvaluated sort sideCondition first second {- | evaluates an 'Iff' given its two 'OrPattern' children. @@ -79,30 +79,28 @@ carry around. -} simplifyEvaluated :: MonadSimplify simplifier => + Sort -> SideCondition RewritingVariableName -> OrPattern RewritingVariableName -> OrPattern RewritingVariableName -> simplifier (OrPattern RewritingVariableName) -simplifyEvaluated - sideCondition - first - second - | OrPattern.isTrue first = return second - | OrPattern.isFalse first = Not.simplifyEvaluated sideCondition second - | OrPattern.isTrue second = return first - | OrPattern.isFalse second = Not.simplifyEvaluated sideCondition first - | otherwise = case (firstPatterns, secondPatterns) of - ([firstP], [secondP]) -> return $ makeEvaluate firstP secondP - _ -> do - fwd <- Implies.simplifyEvaluated sideCondition first second - bwd <- Implies.simplifyEvaluated sideCondition second first - And.simplify - Not.notSimplifier - sideCondition - (MultiAnd.make [fwd, bwd]) - where - firstPatterns = toList first - secondPatterns = toList second +simplifyEvaluated sort sideCondition first second + | OrPattern.isTrue first = return second + | OrPattern.isFalse first = + Not.simplify sideCondition Not{notSort = sort, notChild = second} + | OrPattern.isTrue second = return first + | OrPattern.isFalse second = + Not.simplify sideCondition Not{notSort = sort, notChild = first} + | otherwise = case (firstPatterns, secondPatterns) of + ([firstP], [secondP]) -> return $ makeEvaluate firstP secondP + _ -> do + fwd <- Implies.simplifyEvaluated sort sideCondition first second + bwd <- Implies.simplifyEvaluated sort sideCondition second first + (And.simplify sort Not.notSimplifier sideCondition) + (MultiAnd.make [fwd, bwd]) + where + firstPatterns = toList first + secondPatterns = toList second {- | evaluates an 'Iff' given its two 'Pattern' children. diff --git a/kore/src/Kore/Simplify/Implies.hs b/kore/src/Kore/Simplify/Implies.hs index ba85588df2..a2ffeff24c 100644 --- a/kore/src/Kore/Simplify/Implies.hs +++ b/kore/src/Kore/Simplify/Implies.hs @@ -31,7 +31,7 @@ import qualified Kore.Simplify.And as And import qualified Kore.Simplify.Not as Not ( makeEvaluate, notSimplifier, - simplifyEvaluated, + simplify, ) import Kore.Simplify.Simplify import Logic ( @@ -60,8 +60,8 @@ simplify :: simplifier (OrPattern RewritingVariableName) simplify sideCondition - Implies{impliesFirst = first, impliesSecond = second} = - simplifyEvaluated sideCondition first second + Implies{impliesFirst = first, impliesSecond = second, impliesSort = sort} = + simplifyEvaluated sort sideCondition first second {- | simplifies an Implies given its two 'OrPattern' children. @@ -84,42 +84,42 @@ carry around. -} simplifyEvaluated :: MonadSimplify simplifier => + Sort -> SideCondition RewritingVariableName -> OrPattern RewritingVariableName -> OrPattern RewritingVariableName -> simplifier (OrPattern RewritingVariableName) -simplifyEvaluated sideCondition first second +simplifyEvaluated sort sideCondition first second | OrPattern.isTrue first = return second - | OrPattern.isFalse first = return OrPattern.top - | OrPattern.isTrue second = return OrPattern.top - | OrPattern.isFalse second = Not.simplifyEvaluated sideCondition first + | OrPattern.isFalse first = return (OrPattern.topOf sort) + | OrPattern.isTrue second = return (OrPattern.topOf sort) + | OrPattern.isFalse second = + Not.simplify sideCondition Not{notSort = sort, notChild = first} | otherwise = OrPattern.observeAllT $ Logic.scatter second - >>= simplifyEvaluateHalfImplies sideCondition first + >>= simplifyEvaluateHalfImplies sort sideCondition first simplifyEvaluateHalfImplies :: MonadSimplify simplifier => + Sort -> SideCondition RewritingVariableName -> OrPattern RewritingVariableName -> Pattern RewritingVariableName -> LogicT simplifier (Pattern RewritingVariableName) -simplifyEvaluateHalfImplies - sideCondition - first - second - | OrPattern.isTrue first = return second - | OrPattern.isFalse first = return Pattern.top - | Pattern.isTop second = return Pattern.top - | Pattern.isBottom second = - Not.simplifyEvaluated sideCondition first - >>= Logic.scatter - | otherwise = - case toList first of - [firstP] -> Logic.scatter $ makeEvaluateImplies firstP second - firstPatterns -> - distributeEvaluateImplies sideCondition firstPatterns second - >>= Logic.scatter +simplifyEvaluateHalfImplies sort sideCondition first second + | OrPattern.isTrue first = return second + | OrPattern.isFalse first = return (Pattern.topOf sort) + | Pattern.isTop second = return (Pattern.topOf sort) + | Pattern.isBottom second = + Not.simplify sideCondition Not{notSort = sort, notChild = first} + >>= Logic.scatter + | otherwise = + case toList first of + [firstP] -> Logic.scatter $ makeEvaluateImplies firstP second + firstPatterns -> + distributeEvaluateImplies sideCondition firstPatterns second + >>= Logic.scatter distributeEvaluateImplies :: MonadSimplify simplifier => @@ -128,11 +128,10 @@ distributeEvaluateImplies :: Pattern RewritingVariableName -> simplifier (OrPattern RewritingVariableName) distributeEvaluateImplies sideCondition firsts second = - And.simplify - Not.notSimplifier - sideCondition + (And.simplify sort Not.notSimplifier sideCondition) (MultiAnd.make implications) where + sort = Pattern.patternSort second implications = map (\first -> makeEvaluateImplies first second) firsts makeEvaluateImplies :: @@ -145,13 +144,15 @@ makeEvaluateImplies | Pattern.isTop first = OrPattern.fromPatterns [second] | Pattern.isBottom first = - OrPattern.fromPatterns [Pattern.top] + OrPattern.fromPatterns [Pattern.topOf sort] | Pattern.isTop second = - OrPattern.fromPatterns [Pattern.top] + OrPattern.fromPatterns [Pattern.topOf sort] | Pattern.isBottom second = Not.makeEvaluate first | otherwise = makeEvaluateImpliesNonBool first second + where + sort = Pattern.patternSort first makeEvaluateImpliesNonBool :: Pattern RewritingVariableName -> diff --git a/kore/src/Kore/Simplify/In.hs b/kore/src/Kore/Simplify/In.hs index c5d9d0647d..98975b4436 100644 --- a/kore/src/Kore/Simplify/In.hs +++ b/kore/src/Kore/Simplify/In.hs @@ -89,9 +89,9 @@ makeEvaluateIn sideCondition first second | Pattern.isTop second = Ceil.makeEvaluate sideCondition first | Pattern.isBottom first || Pattern.isBottom second = return OrCondition.bottom | otherwise = - And.makeEvaluate - Not.notSimplifier - sideCondition + (And.makeEvaluate pattSort Not.notSimplifier sideCondition) (MultiAnd.make [first, second]) & OrPattern.observeAllT >>= Ceil.simplifyEvaluated sideCondition + where + pattSort = patternSort first diff --git a/kore/src/Kore/Simplify/InternalMap.hs b/kore/src/Kore/Simplify/InternalMap.hs index 26df572b31..0d71d243a9 100644 --- a/kore/src/Kore/Simplify/InternalMap.hs +++ b/kore/src/Kore/Simplify/InternalMap.hs @@ -27,17 +27,18 @@ import Prelude.Kore simplify :: InternalMap Key (OrPattern RewritingVariableName) -> OrPattern RewritingVariableName -simplify = - traverse (Logic.scatter >>> Compose) - >>> fmap (normalizeInternalMap >>> markSimplified) - >>> getCompose - >>> fmap Pattern.syncSort - >>> MultiOr.observeAll +simplify internalMap = + traverse (Logic.scatter >>> Compose) internalMap + & fmap (normalizeInternalMap (builtinAcSort internalMap) >>> markSimplified) + & getCompose + & fmap Pattern.syncSort + & MultiOr.observeAll normalizeInternalMap :: + Sort -> InternalMap Key (TermLike RewritingVariableName) -> TermLike RewritingVariableName -normalizeInternalMap map' = +normalizeInternalMap sort map' = case Lens.traverseOf (field @"builtinAcChild") Builtin.renormalize map' of Just normalizedMap -> -- If the InternalMap consists of a single compound, remove the @@ -45,7 +46,7 @@ normalizeInternalMap map' = getSingleOpaque normalizedMap -- Otherwise, inject the InternalMap into TermLike. & fromMaybe (mkInternalMap normalizedMap) - _ -> mkBottom_ + _ -> mkBottom sort where getSingleOpaque = retractSingleOpaqueElem . getNormalizedAc getNormalizedAc = getNormalizedMap . builtinAcChild diff --git a/kore/src/Kore/Simplify/InternalSet.hs b/kore/src/Kore/Simplify/InternalSet.hs index cd16cdc586..0bd24c53a6 100644 --- a/kore/src/Kore/Simplify/InternalSet.hs +++ b/kore/src/Kore/Simplify/InternalSet.hs @@ -27,17 +27,18 @@ import Prelude.Kore simplify :: InternalSet Key (OrPattern RewritingVariableName) -> OrPattern RewritingVariableName -simplify = - traverse (Logic.scatter >>> Compose) - >>> fmap (normalizeInternalSet >>> markSimplified) - >>> getCompose - >>> fmap Pattern.syncSort - >>> MultiOr.observeAll +simplify internalSet = + traverse (Logic.scatter >>> Compose) internalSet + & fmap (normalizeInternalSet (builtinAcSort internalSet) >>> markSimplified) + & getCompose + & fmap Pattern.syncSort + & MultiOr.observeAll normalizeInternalSet :: + Sort -> InternalSet Key (TermLike RewritingVariableName) -> TermLike RewritingVariableName -normalizeInternalSet map' = +normalizeInternalSet returnSort map' = case Lens.traverseOf (field @"builtinAcChild") Builtin.renormalize map' of Just normalizedSet -> -- If the InternalSet consists of a single compound, remove the @@ -45,7 +46,7 @@ normalizeInternalSet map' = getSingleOpaque normalizedSet -- Otherwise, inject the InternalSet into TermLike. & fromMaybe (mkInternalSet normalizedSet) - _ -> mkBottom_ + _ -> mkBottom returnSort where getSingleOpaque = retractSingleOpaqueElem . getNormalizedAc getNormalizedAc = getNormalizedSet . builtinAcChild diff --git a/kore/src/Kore/Simplify/Not.hs b/kore/src/Kore/Simplify/Not.hs index ba197c4cfb..d7e167aa2b 100644 --- a/kore/src/Kore/Simplify/Not.hs +++ b/kore/src/Kore/Simplify/Not.hs @@ -11,7 +11,6 @@ module Kore.Simplify.Not ( makeEvaluate, makeEvaluatePredicate, simplify, - simplifyEvaluated, simplifyEvaluatedPredicate, notSimplifier, ) where @@ -55,6 +54,7 @@ import qualified Kore.Internal.Substitution as Substitution import Kore.Internal.TermLike import qualified Kore.Internal.TermLike as TermLike ( markSimplified, + termLikeSort, ) import Kore.Rewrite.RewritingVariable ( RewritingVariableName, @@ -79,41 +79,13 @@ Right now this uses the following: simplify :: MonadSimplify simplifier => SideCondition RewritingVariableName -> - Not sort (OrPattern RewritingVariableName) -> + Not Sort (OrPattern RewritingVariableName) -> simplifier (OrPattern RewritingVariableName) -simplify sideCondition Not{notChild} = - simplifyEvaluated sideCondition notChild - -{- |'simplifyEvaluated' simplifies a 'Not' pattern given its -'OrPattern' child. - -See 'simplify' for details. --} - -{- TODO (virgil): Preserve pattern sorts under simplification. - -One way to preserve the required sort annotations is to make 'simplifyEvaluated' -take an argument of type - -> CofreeF (Not Sort) (Attribute.Pattern variable) (OrPattern variable) - -instead of an 'OrPattern' argument. The type of 'makeEvaluate' may -be changed analogously. The 'Attribute.Pattern' annotation will eventually -cache information besides the pattern sort, which will make it even more useful -to carry around. - --} -simplifyEvaluated :: - MonadSimplify simplifier => - SideCondition RewritingVariableName -> - OrPattern RewritingVariableName -> - simplifier (OrPattern RewritingVariableName) -simplifyEvaluated sideCondition simplified = +simplify sideCondition not'@Not{notSort} = OrPattern.observeAllT $ do - let not' = Not{notChild = simplified, notSort = ()} - andPattern <- - scatterAnd (MultiAnd.map makeEvaluateNot (distributeNot not')) - mkMultiAndPattern sideCondition andPattern + let evaluated = MultiAnd.map makeEvaluateNot (distributeNot not') + andPattern <- scatterAnd evaluated + mkMultiAndPattern notSort sideCondition andPattern simplifyEvaluatedPredicate :: MonadSimplify simplifier => @@ -198,9 +170,11 @@ makeTermNot (Not_ _ term) = MultiOr.singleton term makeTermNot (And_ _ term1 term2) = MultiOr.merge (makeTermNot term1) (makeTermNot term2) makeTermNot term - | isBottom term = MultiOr.singleton mkTop_ - | isTop term = MultiOr.singleton mkBottom_ + | isBottom term = MultiOr.singleton (mkTop sort) + | isTop term = MultiOr.singleton (mkBottom sort) | otherwise = MultiOr.singleton $ TermLike.markSimplified $ mkNot term + where + sort = TermLike.termLikeSort term -- | Distribute 'Not' over 'MultiOr' using de Morgan's identity. distributeNot :: @@ -223,10 +197,11 @@ scatterAnd = scatter . MultiAnd.distributeAnd -- | Conjoin and simplify a 'MultiAnd' of 'Pattern'. mkMultiAndPattern :: MonadSimplify simplifier => + Sort -> SideCondition RewritingVariableName -> MultiAnd (Pattern RewritingVariableName) -> LogicT simplifier (Pattern RewritingVariableName) -mkMultiAndPattern = And.makeEvaluate notSimplifier +mkMultiAndPattern resultSort = And.makeEvaluate resultSort notSimplifier -- | Conjoin and simplify a 'MultiAnd' of 'Condition'. mkMultiAndPredicate :: @@ -237,8 +212,5 @@ mkMultiAndPredicate predicates = -- implements And semantics. return $ fold predicates -notSimplifier :: - MonadSimplify simplifier => - NotSimplifier simplifier -notSimplifier = - NotSimplifier simplifyEvaluated +notSimplifier :: MonadSimplify simplifier => NotSimplifier simplifier +notSimplifier = NotSimplifier simplify diff --git a/kore/src/Kore/Simplify/NotSimplifier.hs b/kore/src/Kore/Simplify/NotSimplifier.hs index 1e487b0db8..89aa4747ec 100644 --- a/kore/src/Kore/Simplify/NotSimplifier.hs +++ b/kore/src/Kore/Simplify/NotSimplifier.hs @@ -15,10 +15,14 @@ import Kore.Internal.SideCondition ( import Kore.Rewrite.RewritingVariable ( RewritingVariableName, ) +import Kore.Syntax ( + Not, + Sort, + ) newtype NotSimplifier simplifier = NotSimplifier { runNotSimplifier :: SideCondition RewritingVariableName -> - OrPattern RewritingVariableName -> + Not Sort (OrPattern RewritingVariableName) -> simplifier (OrPattern RewritingVariableName) } diff --git a/kore/src/Kore/Simplify/Predicate.hs b/kore/src/Kore/Simplify/Predicate.hs index d94e917163..4981f9edfa 100644 --- a/kore/src/Kore/Simplify/Predicate.hs +++ b/kore/src/Kore/Simplify/Predicate.hs @@ -168,8 +168,9 @@ simplify sideCondition original = IffF iffF -> simplifyIff =<< traverse worker iffF CeilF ceilF -> simplifyCeil sideCondition =<< traverse simplifyTerm ceilF - FloorF floorF -> - simplifyFloor sideCondition =<< traverse simplifyTerm floorF + FloorF floorF@(Floor _ _ child) -> + simplifyFloor (termLikeSort child) sideCondition + =<< traverse simplifyTerm floorF ExistsF existsF -> traverse worker (Exists.refreshExists avoid existsF) >>= simplifyExists sideCondition @@ -416,10 +417,11 @@ simplifyCeil sideCondition = -} simplifyFloor :: MonadSimplify simplifier => + Sort -> SideCondition RewritingVariableName -> Floor sort (OrPattern RewritingVariableName) -> simplifier NormalForm -simplifyFloor sideCondition floor' = do +simplifyFloor termSort sideCondition floor' = do notTerm <- mkNotSimplifiedTerm floorChild ceilNotTerm <- mkCeilSimplified notTerm mkNotSimplified ceilNotTerm @@ -428,7 +430,7 @@ simplifyFloor sideCondition floor' = do mkNotSimplified notChild = simplifyNot Not{notSort = floorResultSort, notChild} mkNotSimplifiedTerm notChild = - Not.simplify sideCondition Not{notSort = floorResultSort, notChild} + Not.simplify sideCondition Not{notSort = termSort, notChild} mkCeilSimplified ceilChild = simplifyCeil sideCondition diff --git a/kore/src/Kore/Simplify/Simplify.hs b/kore/src/Kore/Simplify/Simplify.hs index 83eac98270..263e6520d1 100644 --- a/kore/src/Kore/Simplify/Simplify.hs +++ b/kore/src/Kore/Simplify/Simplify.hs @@ -94,6 +94,7 @@ import qualified Kore.Internal.SideCondition.SideCondition as SideCondition ( ) import Kore.Internal.Symbol import Kore.Internal.TermLike ( + Sort, TermAttributes, TermLike, TermLikeF (..), @@ -572,16 +573,17 @@ makeEvaluateTermCeil sideCondition child = makeEvaluateCeil :: MonadSimplify simplifier => + Sort -> SideCondition RewritingVariableName -> Pattern RewritingVariableName -> simplifier (OrPattern RewritingVariableName) -makeEvaluateCeil sideCondition child = +makeEvaluateCeil sort sideCondition child = do let (childTerm, childCondition) = Pattern.splitTerm child ceilCondition <- Predicate.makeCeilPredicate childTerm & Condition.fromPredicate & simplifyCondition sideCondition - Pattern.andCondition Pattern.top (ceilCondition <> childCondition) + Pattern.andCondition (Pattern.topOf sort) (ceilCondition <> childCondition) & pure & OrPattern.observeAllT diff --git a/kore/src/Kore/Simplify/SubstitutionSimplifier.hs b/kore/src/Kore/Simplify/SubstitutionSimplifier.hs index 44694ec975..42966a2c40 100644 --- a/kore/src/Kore/Simplify/SubstitutionSimplifier.hs +++ b/kore/src/Kore/Simplify/SubstitutionSimplifier.hs @@ -165,8 +165,10 @@ simplifyAnds :: NonEmpty (TermLike RewritingVariableName) -> monad (Pattern RewritingVariableName) simplifyAnds MakeAnd{makeAnd} sideCondition (NonEmpty.sort -> patterns) = - foldM simplifyAnds' Pattern.top patterns + foldM simplifyAnds' (Pattern.topOf resultSort) patterns where + resultSort :: TermLike.Sort + resultSort = TermLike.termLikeSort (NonEmpty.head patterns) simplifyAnds' :: Pattern RewritingVariableName -> TermLike RewritingVariableName -> diff --git a/kore/src/Kore/Simplify/TermLike.hs b/kore/src/Kore/Simplify/TermLike.hs index 3ec7902afa..caef76d68c 100644 --- a/kore/src/Kore/Simplify/TermLike.hs +++ b/kore/src/Kore/Simplify/TermLike.hs @@ -334,12 +334,13 @@ simplify sideCondition = \termLike -> , resultPredicate == condition = return $ OrPattern.fromPattern $ - Pattern.fromCondition_ $ + Pattern.fromCondition resultSort $ Condition.markPredicateSimplifiedConditional sideConditionRepresentation resultPredicate | otherwise = continuation where + resultSort = Pattern.patternSort result (resultTerm, resultPredicate) = Pattern.splitTerm result resultSubstitutionIsEmpty = case resultPredicate of @@ -360,6 +361,7 @@ simplify sideCondition = \termLike -> refreshSetBinder = TermLike.refreshSetBinder avoiding ~sort = termLikeSort termLike (_ :< termLikeF) = Recursive.project termLike + termSort = termLikeSort termLike in case termLikeF of -- Unimplemented cases ApplyAliasF _ -> doNotSimplify @@ -371,7 +373,7 @@ simplify sideCondition = \termLike -> -- AndF andF -> do let conjuncts = foldMap MultiAnd.fromTermLike andF - And.simplify Not.notSimplifier sideCondition + (And.simplify termSort Not.notSimplifier sideCondition) =<< MultiAnd.traverse (simplifyTermLike sideCondition) conjuncts @@ -574,7 +576,8 @@ simplifyOnly sideCondition = -- Matching Logic: AndF andF -> do let conjuncts = foldMap MultiAnd.fromTermLike andF - And.simplify Not.notSimplifier sideCondition + -- MultiAnd doesn't preserve the sort so we need to send it as an external argument + And.simplify sort Not.notSimplifier sideCondition =<< MultiAnd.traverse worker conjuncts OrF orF -> Or.simplify <$> traverse worker orF diff --git a/kore/src/Kore/Simplify/Top.hs b/kore/src/Kore/Simplify/Top.hs index 7dabd09de1..9b9bf78d88 100644 --- a/kore/src/Kore/Simplify/Top.hs +++ b/kore/src/Kore/Simplify/Top.hs @@ -20,7 +20,9 @@ import Kore.Rewrite.RewritingVariable ( ) import Kore.Sort import Kore.Syntax.Top -import Prelude.Kore () +import Prelude.Kore ( + (.), + ) -- | simplifies a Top pattern, which means returning an always-true or. @@ -28,4 +30,4 @@ import Prelude.Kore () simplify :: Top Sort child -> OrPattern RewritingVariableName -simplify _ = OrPattern.top +simplify = OrPattern.topOf . topSort diff --git a/kore/src/Kore/Sort.hs b/kore/src/Kore/Sort.hs index ec6d3f78ee..0698ee489e 100644 --- a/kore/src/Kore/Sort.hs +++ b/kore/src/Kore/Sort.hs @@ -11,11 +11,8 @@ module Kore.Sort ( getSortId, sortSubstitution, substituteSortVariables, - rigidSort, sameSort, - matchSort, matchSorts, - alignSorts, -- * Meta-sorts MetaSortType (..), @@ -27,7 +24,6 @@ module Kore.Sort ( stringMetaSort, predicateSortId, predicateSortActual, - predicateSort, -- * Exceptions SortMismatch (..), @@ -212,29 +208,6 @@ predicateSortActual = SortActual predicateSortId [] The final predicate sort is unknown until the predicate is attached to a pattern. -} -predicateSort :: Sort -{- TODO PREDICATE (thomas.tuegel): - -Add a constructor - -> data Sort = ... | FlexibleSort - -to use internally as a placeholder where the predicate sort is not yet -known. Using the sort _PREDICATE{} is a kludge; the backend will melt down if -the user tries to define a sort named _PREDICATE{}. (At least, this is not -actually a valid identifier in Kore.) - -Until this is fixed, the identifier _PREDICATE is reserved in -Kore.Validate.DefinitionVerifier.indexImplicitModule. - --} -predicateSort = SortActualSort predicateSortActual - -rigidSort :: Sort -> Maybe Sort -rigidSort sort - | sort == predicateSort = Nothing - | otherwise = Just sort - data SortMismatch = SortMismatch !Sort !Sort deriving stock (Eq, Show, Typeable) @@ -284,28 +257,9 @@ sameSort sort1 sort2 | sort1 == sort2 = sort1 | otherwise = sortMismatch sort1 sort2 -{- | Match the second sort to the first. - -If the second sort is flexible, it matches the first sort. If the second sort is -rigid, it must be equal to the first sort. --} -matchSort :: Sort -> Sort -> Sort -matchSort sort1 sort2 = - maybe sort1 (sameSort sort1) (rigidSort sort2) - matchSorts :: [Sort] -> [Sort] -> [Sort] matchSorts = alignWith matchTheseSorts where matchTheseSorts (This sort1) = missingArgument sort1 matchTheseSorts (That sort2) = unexpectedArgument sort2 - matchTheseSorts (These sort1 sort2) = matchSort sort1 sort2 - -alignSorts :: Foldable f => f Sort -> Sort -alignSorts = fromMaybe predicateSort . foldl' worker Nothing - where - worker Nothing sort2 = rigidSort sort2 - worker (Just sort1) sort2 = - Just $ maybe sort1 (alignSort sort1) (rigidSort sort2) - alignSort sort1 sort2 - | sort1 == sort2 = sort1 - | otherwise = sortMismatch sort1 sort2 + matchTheseSorts (These sort1 sort2) = sameSort sort1 sort2 diff --git a/kore/src/Kore/Syntax/And.hs b/kore/src/Kore/Syntax/And.hs index 3a1852e9d6..a7cb01d476 100644 --- a/kore/src/Kore/Syntax/And.hs +++ b/kore/src/Kore/Syntax/And.hs @@ -56,6 +56,6 @@ instance Ord variable => Synthetic (FreeVariables variable) (And sort) where instance Synthetic Sort (And Sort) where synthetic And{andSort, andFirst, andSecond} = andSort - & seq (matchSort andSort andFirst) - . seq (matchSort andSort andSecond) + & seq (sameSort andSort andFirst) + . seq (sameSort andSort andSecond) {-# INLINE synthetic #-} diff --git a/kore/src/Kore/Syntax/Ceil.hs b/kore/src/Kore/Syntax/Ceil.hs index 57b825ab9b..f09197b50b 100644 --- a/kore/src/Kore/Syntax/Ceil.hs +++ b/kore/src/Kore/Syntax/Ceil.hs @@ -60,5 +60,5 @@ instance Synthetic (FreeVariables variable) (Ceil sort) where instance Synthetic Sort (Ceil Sort) where synthetic Ceil{ceilOperandSort, ceilResultSort, ceilChild} = ceilResultSort - & seq (matchSort ceilOperandSort ceilChild) + & seq (sameSort ceilOperandSort ceilChild) {-# INLINE synthetic #-} diff --git a/kore/src/Kore/Syntax/DomainValue.hs b/kore/src/Kore/Syntax/DomainValue.hs index e191182484..c2b9b66854 100644 --- a/kore/src/Kore/Syntax/DomainValue.hs +++ b/kore/src/Kore/Syntax/DomainValue.hs @@ -54,7 +54,7 @@ instance Synthetic (FreeVariables variable) (DomainValue sort) where instance Synthetic Sort (DomainValue Sort) where synthetic DomainValue{domainValueSort, domainValueChild} = domainValueSort - & seq (matchSort stringMetaSort domainValueChild) + & seq (sameSort stringMetaSort domainValueChild) {-# INLINE synthetic #-} instance TopBottom a => TopBottom (DomainValue Sort a) where diff --git a/kore/src/Kore/Syntax/Equals.hs b/kore/src/Kore/Syntax/Equals.hs index 15b0e61154..b5e6a75241 100644 --- a/kore/src/Kore/Syntax/Equals.hs +++ b/kore/src/Kore/Syntax/Equals.hs @@ -113,8 +113,8 @@ instance Ord variable => Synthetic (FreeVariables variable) (Equals sort) where instance Synthetic Sort (Equals Sort) where synthetic equals = equalsResultSort - & seq (matchSort equalsOperandSort equalsFirst) - . seq (matchSort equalsOperandSort equalsSecond) + & seq (sameSort equalsOperandSort equalsFirst) + . seq (sameSort equalsOperandSort equalsSecond) where Equals{equalsOperandSort, equalsResultSort} = equals Equals{equalsFirst, equalsSecond} = equals diff --git a/kore/src/Kore/Syntax/Exists.hs b/kore/src/Kore/Syntax/Exists.hs index 3eb3302634..06aa0c15e9 100644 --- a/kore/src/Kore/Syntax/Exists.hs +++ b/kore/src/Kore/Syntax/Exists.hs @@ -89,7 +89,7 @@ instance instance Synthetic Sort (Exists Sort variable) where synthetic Exists{existsSort, existsChild} = - existsSort `matchSort` existsChild + existsSort `sameSort` existsChild {-# INLINE synthetic #-} instance diff --git a/kore/src/Kore/Syntax/Floor.hs b/kore/src/Kore/Syntax/Floor.hs index 366ba7b03e..b0c27024e4 100644 --- a/kore/src/Kore/Syntax/Floor.hs +++ b/kore/src/Kore/Syntax/Floor.hs @@ -58,5 +58,5 @@ instance Synthetic (FreeVariables variable) (Floor sort) where instance Synthetic Sort (Floor Sort) where synthetic Floor{floorOperandSort, floorResultSort, floorChild} = floorResultSort - & seq (matchSort floorOperandSort floorChild) + & seq (sameSort floorOperandSort floorChild) {-# INLINE synthetic #-} diff --git a/kore/src/Kore/Syntax/Forall.hs b/kore/src/Kore/Syntax/Forall.hs index 9bcc5c0c1e..e4e3f3704c 100644 --- a/kore/src/Kore/Syntax/Forall.hs +++ b/kore/src/Kore/Syntax/Forall.hs @@ -88,7 +88,7 @@ instance instance Synthetic Sort (Forall Sort variable) where synthetic Forall{forallSort, forallChild} = - forallSort `matchSort` forallChild + forallSort `sameSort` forallChild {-# INLINE synthetic #-} {- | A 'Lens.Lens' to view a 'Forall' as a 'Binder'. diff --git a/kore/src/Kore/Syntax/Iff.hs b/kore/src/Kore/Syntax/Iff.hs index 7e3ef0fd9a..4e8e7f23e4 100644 --- a/kore/src/Kore/Syntax/Iff.hs +++ b/kore/src/Kore/Syntax/Iff.hs @@ -68,6 +68,6 @@ instance Ord variable => Synthetic (FreeVariables variable) (Iff sort) where instance Synthetic Sort (Iff Sort) where synthetic Iff{iffSort, iffFirst, iffSecond} = iffSort - & seq (matchSort iffSort iffFirst) - . seq (matchSort iffSort iffSecond) + & seq (sameSort iffSort iffFirst) + . seq (sameSort iffSort iffSecond) {-# INLINE synthetic #-} diff --git a/kore/src/Kore/Syntax/Implies.hs b/kore/src/Kore/Syntax/Implies.hs index 8ef3744f5e..dd487780ce 100644 --- a/kore/src/Kore/Syntax/Implies.hs +++ b/kore/src/Kore/Syntax/Implies.hs @@ -68,6 +68,6 @@ instance Ord variable => Synthetic (FreeVariables variable) (Implies sort) where instance Synthetic Sort (Implies Sort) where synthetic Implies{impliesSort, impliesFirst, impliesSecond} = impliesSort - & seq (matchSort impliesSort impliesFirst) - . seq (matchSort impliesSort impliesSecond) + & seq (sameSort impliesSort impliesFirst) + . seq (sameSort impliesSort impliesSecond) {-# INLINE synthetic #-} diff --git a/kore/src/Kore/Syntax/In.hs b/kore/src/Kore/Syntax/In.hs index cec66007ba..ca2883f7c9 100644 --- a/kore/src/Kore/Syntax/In.hs +++ b/kore/src/Kore/Syntax/In.hs @@ -89,8 +89,8 @@ instance Ord variable => Synthetic (FreeVariables variable) (In sort) where instance Synthetic Sort (In Sort) where synthetic in' = inResultSort - & seq (matchSort inOperandSort inContainedChild) - . seq (matchSort inOperandSort inContainingChild) + & seq (sameSort inOperandSort inContainedChild) + . seq (sameSort inOperandSort inContainingChild) where In{inResultSort, inOperandSort} = in' In{inContainedChild, inContainingChild} = in' diff --git a/kore/src/Kore/Syntax/Mu.hs b/kore/src/Kore/Syntax/Mu.hs index 99128be412..0899e11abe 100644 --- a/kore/src/Kore/Syntax/Mu.hs +++ b/kore/src/Kore/Syntax/Mu.hs @@ -59,7 +59,7 @@ instance instance Synthetic Sort (Mu variable) where synthetic Mu{muVariable, muChild} = muSort - & seq (matchSort muSort muChild) + & seq (sameSort muSort muChild) where Variable{variableSort = muSort} = muVariable {-# INLINE synthetic #-} diff --git a/kore/src/Kore/Syntax/Next.hs b/kore/src/Kore/Syntax/Next.hs index b51450e935..99ee9eab2a 100644 --- a/kore/src/Kore/Syntax/Next.hs +++ b/kore/src/Kore/Syntax/Next.hs @@ -46,5 +46,5 @@ instance Synthetic (FreeVariables variable) (Next sort) where instance Synthetic Sort (Next Sort) where synthetic Next{nextSort, nextChild} = - nextSort `matchSort` nextChild + nextSort `sameSort` nextChild {-# INLINE synthetic #-} diff --git a/kore/src/Kore/Syntax/Not.hs b/kore/src/Kore/Syntax/Not.hs index f2e4d6d964..d704fd655a 100644 --- a/kore/src/Kore/Syntax/Not.hs +++ b/kore/src/Kore/Syntax/Not.hs @@ -59,5 +59,5 @@ instance Synthetic (FreeVariables variable) (Not child) where instance Synthetic Sort (Not Sort) where synthetic Not{notSort, notChild} = - notSort `matchSort` notChild + notSort `sameSort` notChild {-# INLINE synthetic #-} diff --git a/kore/src/Kore/Syntax/Nu.hs b/kore/src/Kore/Syntax/Nu.hs index e83af8ab33..c4333fa951 100644 --- a/kore/src/Kore/Syntax/Nu.hs +++ b/kore/src/Kore/Syntax/Nu.hs @@ -59,7 +59,7 @@ instance instance Synthetic Sort (Nu variable) where synthetic Nu{nuVariable, nuChild} = nuSort - & seq (matchSort nuSort nuChild) + & seq (sameSort nuSort nuChild) where Variable{variableSort = nuSort} = nuVariable {-# INLINE synthetic #-} diff --git a/kore/src/Kore/Syntax/Or.hs b/kore/src/Kore/Syntax/Or.hs index 1ca7f40bd3..be961946cf 100644 --- a/kore/src/Kore/Syntax/Or.hs +++ b/kore/src/Kore/Syntax/Or.hs @@ -81,6 +81,6 @@ instance Ord variable => Synthetic (FreeVariables variable) (Or sort) where instance Synthetic Sort (Or Sort) where synthetic Or{orSort, orFirst, orSecond} = orSort - & seq (matchSort orSort orFirst) - . seq (matchSort orSort orSecond) + & seq (sameSort orSort orFirst) + . seq (sameSort orSort orSecond) {-# INLINE synthetic #-} diff --git a/kore/src/Kore/Syntax/Rewrites.hs b/kore/src/Kore/Syntax/Rewrites.hs index 4b943e4ee8..162dd6e8d2 100644 --- a/kore/src/Kore/Syntax/Rewrites.hs +++ b/kore/src/Kore/Syntax/Rewrites.hs @@ -54,5 +54,5 @@ instance Ord variable => Synthetic (FreeVariables variable) (Rewrites sort) wher instance Synthetic Sort (Rewrites Sort) where synthetic Rewrites{rewritesSort, rewritesFirst, rewritesSecond} = rewritesSort - & seq (matchSort rewritesSort rewritesFirst) - . seq (matchSort rewritesSort rewritesSecond) + & seq (sameSort rewritesSort rewritesFirst) + . seq (sameSort rewritesSort rewritesSecond) diff --git a/kore/src/Prelude/Kore.hs b/kore/src/Prelude/Kore.hs index 5fac9ab999..8d06371b64 100644 --- a/kore/src/Prelude/Kore.hs +++ b/kore/src/Prelude/Kore.hs @@ -32,6 +32,9 @@ module Prelude.Kore ( -- * Filterable Filterable (..), + -- * Foldable + foldFirst, + -- * Witherable Witherable (..), @@ -201,3 +204,6 @@ minMaxBy :: (a -> a -> Ordering) -> a -> a -> (a, a) minMaxBy cmp a b | cmp a b == LT = (a, b) | otherwise = (b, a) + +foldFirst :: Foldable f => f a -> Maybe a +foldFirst = foldr (\x _ -> pure x) Nothing diff --git a/kore/test/Test/Kore/Attribute/Pattern/ConstructorLike.hs b/kore/test/Test/Kore/Attribute/Pattern/ConstructorLike.hs index 9d0de195fc..7328b99e46 100644 --- a/kore/test/Test/Kore/Attribute/Pattern/ConstructorLike.hs +++ b/kore/test/Test/Kore/Attribute/Pattern/ConstructorLike.hs @@ -33,7 +33,7 @@ test_TermLike = , testCase "Single constructor is constructor-like" $ Mock.a `shouldBeConstructorLike` True , testCase "Constructor-like with constructor at the top" $ - Mock.constr10 (Mock.builtinInt 3) `shouldBeConstructorLike` True + Mock.constrInt (Mock.builtinInt 3) `shouldBeConstructorLike` True , testCase "Simplifiable pattern contains symbol which is only functional" $ Mock.constr10 (Mock.f Mock.a) `shouldBeConstructorLike` False , testCase "Constructor-like pattern with constructor and sort injection" $ diff --git a/kore/test/Test/Kore/Builtin/Builtin.hs b/kore/test/Test/Kore/Builtin/Builtin.hs index afeed6ce49..f09433fe83 100644 --- a/kore/test/Test/Kore/Builtin/Builtin.hs +++ b/kore/test/Test/Kore/Builtin/Builtin.hs @@ -11,6 +11,7 @@ module Test.Kore.Builtin.Builtin ( simplify, evaluate, evaluateT, + evaluateExpectTopK, evaluateToList, indexedModule, verifiedModule, @@ -51,6 +52,7 @@ import Kore.Internal.InternalSet import Kore.Internal.OrPattern ( OrPattern, ) +import qualified Kore.Internal.OrPattern as OrPattern import Kore.Internal.Pattern ( Pattern, ) @@ -255,6 +257,15 @@ evaluateT :: t smt (OrPattern RewritingVariableName) evaluateT = lift . evaluate +evaluateExpectTopK :: + HasCallStack => + (MonadSMT smt, MonadLog smt, MonadProf smt, MonadMask smt) => + TermLike RewritingVariableName -> + Hedgehog.PropertyT smt () +evaluateExpectTopK termLike = do + actual <- evaluateT termLike + OrPattern.topOf kSort Hedgehog.=== actual + evaluateToList :: TermLike RewritingVariableName -> NoSMT [Pattern RewritingVariableName] diff --git a/kore/test/Test/Kore/Builtin/Int.hs b/kore/test/Test/Kore/Builtin/Int.hs index d5ccde92c9..d6c4f3df5e 100644 --- a/kore/test/Test/Kore/Builtin/Int.hs +++ b/kore/test/Test/Kore/Builtin/Int.hs @@ -402,12 +402,13 @@ test_euclidian_division_theorem = (asInternal <$> [a, b]) & evaluateT & fmap extractValue + extractValue :: OrPattern RewritingVariableName -> Integer - extractValue (OrPattern.toTermLike -> term) = + extractValue (OrPattern.toTermLike intSort -> term) = case term of InternalInt_ InternalInt{internalIntValue} -> internalIntValue - _ -> error "Expecting builtin int." + _ -> error "Expecting builtin Int" -- Bitwise operations test_and :: TestTree @@ -487,7 +488,7 @@ test_unifyEqual_NotEqual = testCaseWithoutSMT "unifyEqual BuiltinInteger: Not Equal" $ do let dv1 = asInternal 1 dv2 = asInternal 2 - actual <- evaluate $ mkEquals_ dv1 dv2 + actual <- evaluate $ mkEquals kSort dv1 dv2 assertEqual' "" OrPattern.bottom actual -- | "\equal"ed internal Integers that are equal @@ -495,8 +496,8 @@ test_unifyEqual_Equal :: TestTree test_unifyEqual_Equal = testCaseWithoutSMT "unifyEqual BuiltinInteger: Equal" $ do let dv1 = asInternal 2 - actual <- evaluate $ mkEquals_ dv1 dv1 - assertEqual' "" OrPattern.top actual + actual <- evaluate $ mkEquals kSort dv1 dv1 + assertEqual' "" (OrPattern.topOf kSort) actual -- | "\and"ed internal Integers that are not equal test_unifyAnd_NotEqual :: TestTree @@ -520,8 +521,8 @@ test_unifyAndEqual_Equal :: TestTree test_unifyAndEqual_Equal = testCaseWithoutSMT "unifyAnd BuiltinInteger: Equal" $ do let dv = asInternal 0 - actual <- evaluate $ mkEquals_ dv $ mkAnd dv dv - assertEqual' "" OrPattern.top actual + actual <- evaluate $ mkEquals kSort dv $ mkAnd dv dv + assertEqual' "" (OrPattern.topOf kSort) actual -- | Internal Integer "\and"ed with builtin function applied to variable test_unifyAnd_Fn :: TestTree @@ -576,7 +577,7 @@ test_unifyIntEq = makeEqualsPredicate (mkElemVar x) (mkElemVar y) & makeNotPredicate & Condition.fromPredicate - & Pattern.fromCondition_ + & Pattern.fromCondition boolSort -- unit test do actual <- unifyIntEq term1 term2 @@ -607,7 +608,7 @@ test_unifyIntEq = term2 = eqInt (mkElemVar x) (mkElemVar y) expect = Condition.assign (inject x) (mkElemVar y) - & Pattern.fromCondition_ + & Pattern.fromCondition boolSort -- unit test do actual <- unifyIntEq term1 term2 @@ -647,7 +648,7 @@ test_unifyIntEq = (addInt (mkElemVar y) (asInternal 1)) & makeNotPredicate & Condition.fromPredicate - & Pattern.fromCondition_ + & Pattern.fromCondition boolSort -- unit test do actual <- unifyIntEq term1 term2 diff --git a/kore/test/Test/Kore/Builtin/KEqual.hs b/kore/test/Test/Kore/Builtin/KEqual.hs index d82cd83a17..c9aff4af19 100644 --- a/kore/test/Test/Kore/Builtin/KEqual.hs +++ b/kore/test/Test/Kore/Builtin/KEqual.hs @@ -83,11 +83,12 @@ test_KEqual = actual <- evaluate original assertEqual' "" expect actual , testCaseWithoutSMT "kseq(x, dotk) equals kseq(x, dotk)" $ do - let expect = OrPattern.top + let expect = OrPattern.topOf kSort xConfigElemVarKItemSort = configElementVariableFromId "x" kItemSort original = - mkEquals_ + mkEquals + kSort (Test.Bool.asInternal True) ( keqBool (kseq (mkElemVar xConfigElemVarKItemSort) dotk) @@ -96,11 +97,12 @@ test_KEqual = actual <- evaluate original assertEqual' "" expect actual , testCaseWithoutSMT "kseq(inj(x), dotk) equals kseq(inj(x), dotk)" $ do - let expect = OrPattern.top + let expect = OrPattern.topOf kSort xConfigElemVarIdSort = configElementVariableFromId "x" idSort original = - mkEquals_ + mkEquals + kSort (Test.Bool.asInternal True) ( keqBool (kseq (inj kItemSort (mkElemVar xConfigElemVarIdSort)) dotk) @@ -109,9 +111,10 @@ test_KEqual = actual <- evaluate original assertEqual' "" expect actual , testCaseWithoutSMT "distinct constructor-like terms" $ do - let expect = OrPattern.top + let expect = OrPattern.topOf kSort original = - mkEquals_ + mkEquals + kSort (Test.Bool.asInternal False) ( keqBool (kseq (inj kItemSort dvX) dotk) @@ -119,6 +122,19 @@ test_KEqual = ) actual <- evaluate original assertEqual' "" expect actual + , testCaseWithoutSMT "kseq(x, dotk) and kseq(x, dotk)" $ do + let expect = OrPattern.fromTermLike $ Test.Bool.asInternal True + xConfigElemVarKItemSort = + configElementVariableFromId "x" kItemSort + original = + mkAnd + (Test.Bool.asInternal True) + ( keqBool + (kseq (mkElemVar xConfigElemVarKItemSort) dotk) + (kseq (mkElemVar xConfigElemVarKItemSort) dotk) + ) + actual <- evaluate original + assertEqual' "" expect actual , testCaseWithoutSMT "distinct domain values" $ do let expect = OrPattern.fromTermLike $ Test.Bool.asInternal False original = keqBool (inj kSort dvT) (inj kSort dvX) diff --git a/kore/test/Test/Kore/Builtin/List.hs b/kore/test/Test/Kore/Builtin/List.hs index 38f1485b0d..497aee7ba7 100644 --- a/kore/test/Test/Kore/Builtin/List.hs +++ b/kore/test/Test/Kore/Builtin/List.hs @@ -82,9 +82,9 @@ test_getUnit = [ mkApplySymbol unitListSymbol [] , Test.Int.asInternal k ] - predicate = mkEquals_ mkBottom_ patGet + predicate = mkEquals kSort (mkBottom intSort) patGet (===) OrPattern.bottom =<< evaluateT patGet - (===) OrPattern.top =<< evaluateT predicate + evaluateExpectTopK predicate test_getFirstElement :: TestTree test_getFirstElement = @@ -102,11 +102,11 @@ test_getFirstElement = case values of Seq.Empty -> Nothing v Seq.:<| _ -> Just v - patFirst = maybe mkBottom_ Test.Int.asInternal value - predicate = mkEquals_ patGet patFirst + patFirst = maybe (mkBottom intSort) Test.Int.asInternal value + predicate = mkEquals kSort patGet patFirst let expectGet = Test.Int.asPartialPattern value (===) (MultiOr.singleton expectGet) =<< evaluateT patGet - (===) OrPattern.top =<< evaluateT predicate + evaluateExpectTopK predicate test_getLastElement :: TestTree test_getLastElement = @@ -125,11 +125,11 @@ test_getLastElement = case values of Seq.Empty -> Nothing _ Seq.:|> v -> Just v - patFirst = maybe mkBottom_ Test.Int.asInternal value - predicate = mkEquals_ patGet patFirst + patFirst = maybe (mkBottom intSort) Test.Int.asInternal value + predicate = mkEquals kSort patGet patFirst let expectGet = Test.Int.asPartialPattern value (===) (MultiOr.singleton expectGet) =<< evaluateT patGet - (===) OrPattern.top =<< evaluateT predicate + evaluateExpectTopK predicate test_GetUpdate :: TestTree test_GetUpdate = @@ -147,17 +147,14 @@ test_GetUpdate = if 0 <= ix && ix < len then do let patGet = getList patUpdated $ Test.Int.asInternal ix - predicate = - mkEquals_ - patGet - value + predicate = mkEquals kSort patGet value expect = Pattern.fromTermLike value - (===) OrPattern.top =<< evaluateT predicate + evaluateExpectTopK predicate (===) (MultiOr.singleton expect) =<< evaluateT patGet else do - let predicate = mkEquals_ mkBottom_ patUpdated + let predicate = mkEquals kSort (mkBottom listSort) patUpdated (===) OrPattern.bottom =<< evaluateT patUpdated - (===) OrPattern.top =<< evaluateT predicate + evaluateExpectTopK predicate test_inUnit :: TestTree test_inUnit = @@ -170,9 +167,9 @@ test_inUnit = let patValue = Test.Int.asInternal value patIn = inList patValue unitList patFalse = Test.Bool.asInternal False - predicate = mkEquals_ patFalse patIn + predicate = mkEquals kSort patFalse patIn (===) (Test.Bool.asOrPattern False) =<< evaluateT patIn - (===) OrPattern.top =<< evaluateT predicate + evaluateExpectTopK predicate test_inElement :: TestTree test_inElement = @@ -186,9 +183,9 @@ test_inElement = patElement = elementList patValue patIn = inList patValue patElement patTrue = Test.Bool.asInternal True - predicate = mkEquals_ patIn patTrue + predicate = mkEquals kSort patIn patTrue (===) (Test.Bool.asOrPattern True) =<< evaluateT patIn - (===) OrPattern.top =<< evaluateT predicate + evaluateExpectTopK predicate test_inConcat :: TestTree test_inConcat = @@ -205,9 +202,9 @@ test_inConcat = patConcat = concatList patValues patElement patIn = inList patValue patConcat patTrue = Test.Bool.asInternal True - predicate = mkEquals_ patIn patTrue + predicate = mkEquals kSort patIn patTrue (===) (Test.Bool.asOrPattern True) =<< evaluateT patIn - (===) OrPattern.top =<< evaluateT predicate + evaluateExpectTopK predicate test_concatUnit :: TestTree test_concatUnit = @@ -221,13 +218,13 @@ test_concatUnit = patValues = asTermLike (Test.Int.asInternal <$> values) patConcat1 = mkApplySymbol concatListSymbol [patUnit, patValues] patConcat2 = mkApplySymbol concatListSymbol [patValues, patUnit] - predicate1 = mkEquals_ patValues patConcat1 - predicate2 = mkEquals_ patValues patConcat2 + predicate1 = mkEquals kSort patValues patConcat1 + predicate2 = mkEquals kSort patValues patConcat2 expectValues <- evaluateT patValues (===) expectValues =<< evaluateT patConcat1 (===) expectValues =<< evaluateT patConcat2 - (===) OrPattern.top =<< evaluateT predicate1 - (===) OrPattern.top =<< evaluateT predicate2 + evaluateExpectTopK predicate1 + evaluateExpectTopK predicate2 test_concatUnitSymbolic :: TestTree test_concatUnitSymbolic = @@ -241,13 +238,13 @@ test_concatUnitSymbolic = mkElemVar $ configElementVariableFromId (testId "x") listSort patConcat1 = mkApplySymbol concatListSymbol [patUnit, patSymbolic] patConcat2 = mkApplySymbol concatListSymbol [patSymbolic, patUnit] - predicate1 = mkEquals_ patSymbolic patConcat1 - predicate2 = mkEquals_ patSymbolic patConcat2 + predicate1 = mkEquals kSort patSymbolic patConcat1 + predicate2 = mkEquals kSort patSymbolic patConcat2 expectSymbolic <- evaluateT patSymbolic (===) expectSymbolic =<< evaluateT patConcat1 (===) expectSymbolic =<< evaluateT patConcat2 - (===) OrPattern.top =<< evaluateT predicate1 - (===) OrPattern.top =<< evaluateT predicate2 + evaluateExpectTopK predicate1 + evaluateExpectTopK predicate2 test_concatAssociates :: TestTree test_concatAssociates = @@ -268,11 +265,11 @@ test_concatAssociates = mkApplySymbol concatListSymbol [patConcat12, patList3] patConcat1_23 = mkApplySymbol concatListSymbol [patList1, patConcat23] - predicate = mkEquals_ patConcat12_3 patConcat1_23 + predicate = mkEquals kSort patConcat12_3 patConcat1_23 evalConcat12_3 <- evaluateT patConcat12_3 evalConcat1_23 <- evaluateT patConcat1_23 (===) evalConcat12_3 evalConcat1_23 - (===) OrPattern.top =<< evaluateT predicate + evaluateExpectTopK predicate test_concatSymbolic :: TestTree test_concatSymbolic = @@ -388,7 +385,7 @@ test_simplify :: TestTree test_simplify = testPropertyWithSolver "simplify elements" $ do let x = mkElemVar (configElementVariableFromId (testId "x") intSort) - original = asInternal [mkAnd x mkTop_] + original = asInternal [mkAnd x (mkTop intSort)] expected = MultiOr.singleton $ asPattern [x] (===) expected =<< evaluateT original @@ -413,26 +410,26 @@ test_size = [ testPropertyWithSolver "size(unit(_)) = 0" $ do let original = sizeList unitList zero = mkInt 0 - predicate = mkEquals_ zero original + predicate = mkEquals kSort zero original (===) (OrPattern.fromTermLike zero) =<< evaluateT original - (===) OrPattern.top =<< evaluateT predicate + evaluateExpectTopK predicate , testPropertyWithSolver "size(element(_)) = 1" $ do k <- forAll genInteger let original = sizeList (elementList $ mkInt k) one = mkInt 1 - predicate = mkEquals_ one original + predicate = mkEquals kSort one original (===) (OrPattern.fromTermLike one) =<< evaluateT original - (===) OrPattern.top =<< evaluateT predicate + evaluateExpectTopK predicate , testPropertyWithSolver "size(a + b) = size(a) + size(b)" $ do as <- asInternal . fmap mkInt <$> forAll genSeqInteger bs <- asInternal . fmap mkInt <$> forAll genSeqInteger let sizeConcat = sizeList (concatList as bs) addSize = addInt (sizeList as) (sizeList bs) - predicate = mkEquals_ sizeConcat addSize + predicate = mkEquals kSort sizeConcat addSize expect1 <- evaluateT sizeConcat expect2 <- evaluateT addSize (===) expect1 expect2 - (===) OrPattern.top =<< evaluateT predicate + evaluateExpectTopK predicate ] test_make :: [TestTree] diff --git a/kore/test/Test/Kore/Builtin/Map.hs b/kore/test/Test/Kore/Builtin/Map.hs index ddee37424a..ac45bd8dd6 100644 --- a/kore/test/Test/Kore/Builtin/Map.hs +++ b/kore/test/Test/Kore/Builtin/Map.hs @@ -154,21 +154,28 @@ genMapSortedVariable sort genElement = ) <&> HashMap.fromList +mkEquals_ :: + InternalVariable variable => + TermLike variable -> + TermLike variable -> + TermLike variable +mkEquals_ = mkEquals kSort + test_lookupUnit :: [TestTree] test_lookupUnit = [ testPropertyWithoutSolver "lookup{}(unit{}(), key) === \\bottom{}()" $ do key <- forAll genIntegerPattern let patLookup = lookupMap unitMap key - predicate = mkEquals_ mkBottom_ patLookup + predicate = mkEquals_ (mkBottom intSort) patLookup (===) OrPattern.bottom =<< evaluateT patLookup - (===) OrPattern.top =<< evaluateT predicate + evaluateExpectTopK predicate , testPropertyWithoutSolver "lookupOrDefault{}(unit{}(), key, default) === default" $ do key <- forAll genIntegerPattern def <- forAll genIntegerPattern let patLookup = lookupOrDefaultMap unitMap key def predicate = mkEquals_ def patLookup (===) (OrPattern.fromTermLike def) =<< evaluateT patLookup - (===) OrPattern.top =<< evaluateT predicate + evaluateExpectTopK predicate ] test_lookupUpdate :: [TestTree] @@ -181,7 +188,7 @@ test_lookupUpdate = predicate = mkEquals_ patLookup patVal expect = OrPattern.fromTermLike patVal (===) expect =<< evaluateT patLookup - (===) OrPattern.top =<< evaluateT predicate + evaluateExpectTopK predicate , testPropertyWithoutSolver "lookupOrDefault{}(update{}(map, key, val), key, def) === val" $ do patKey <- forAll genIntegerPattern patDef <- forAll genIntegerPattern @@ -192,7 +199,7 @@ test_lookupUpdate = predicate = mkEquals_ patLookup patVal expect = OrPattern.fromTermLike patVal (===) expect =<< evaluateT patLookup - (===) OrPattern.top =<< evaluateT predicate + evaluateExpectTopK predicate ] test_removeUnit :: TestTree @@ -205,7 +212,7 @@ test_removeUnit = predicate = mkEquals_ unitMap patRemove expect <- evaluateT unitMap (===) expect =<< evaluateT patRemove - (===) OrPattern.top =<< evaluateT predicate + evaluateExpectTopK predicate ) test_sizeUnit :: TestTree @@ -223,7 +230,7 @@ test_sizeUnit = predicate = mkEquals_ patExpected patActual expect <- evaluateT patExpected (===) expect =<< evaluateT patActual - (===) OrPattern.top =<< evaluateT predicate + evaluateExpectTopK predicate ) test_removeKeyNotIn :: TestTree @@ -239,7 +246,7 @@ test_removeKeyNotIn = predicate = mkEquals_ map' patRemove expect <- evaluateT map' (===) expect =<< evaluateT patRemove - (===) OrPattern.top =<< evaluateT predicate + evaluateExpectTopK predicate ) test_removeKeyIn :: TestTree @@ -256,7 +263,7 @@ test_removeKeyIn = predicate = mkEquals_ patRemove map' expect <- evaluateT map' (===) expect =<< evaluateT patRemove - (===) OrPattern.top =<< evaluateT predicate + evaluateExpectTopK predicate ) test_removeAllMapUnit :: TestTree @@ -269,7 +276,7 @@ test_removeAllMapUnit = predicate = mkEquals_ unitMap patRemoveAll expect <- evaluateT unitMap (===) expect =<< evaluateT patRemoveAll - (===) OrPattern.top =<< evaluateT predicate + evaluateExpectTopK predicate ) test_removeAllSetUnit :: TestTree @@ -282,7 +289,7 @@ test_removeAllSetUnit = predicate = mkEquals_ map' patRemoveAll expect <- evaluateT map' (===) expect =<< evaluateT patRemoveAll - (===) OrPattern.top =<< evaluateT predicate + evaluateExpectTopK predicate ) test_removeAll :: TestTree @@ -306,7 +313,7 @@ test_removeAll = predicate = mkEquals_ patRemoveAll1 patRemoveAll2 expect <- evaluateT patRemoveAll2 (===) expect =<< evaluateT patRemoveAll1 - (===) OrPattern.top =<< evaluateT predicate + evaluateExpectTopK predicate ) test_concatUnit :: TestTree @@ -323,8 +330,8 @@ test_concatUnit = expect <- evaluateT patMap (===) expect =<< evaluateT patConcat1 (===) expect =<< evaluateT patConcat2 - (===) OrPattern.top =<< evaluateT predicate1 - (===) OrPattern.top =<< evaluateT predicate2 + evaluateExpectTopK predicate1 + evaluateExpectTopK predicate2 ) test_lookupConcatUniqueKeys :: TestTree @@ -353,7 +360,7 @@ test_lookupConcatUniqueKeys = expect2 = OrPattern.fromTermLike patVal2 (===) expect1 =<< evaluateT patLookup1 (===) expect2 =<< evaluateT patLookup2 - (===) OrPattern.top =<< evaluateT predicate + evaluateExpectTopK predicate ) test_concatDuplicateKeys :: TestTree @@ -367,9 +374,9 @@ test_concatDuplicateKeys = let patMap1 = elementMap patKey patVal1 patMap2 = elementMap patKey patVal2 patConcat = concatMap patMap1 patMap2 - predicate = mkEquals_ mkBottom_ patConcat + predicate = mkEquals_ (mkBottom mapSort) patConcat (===) OrPattern.bottom =<< evaluateT patConcat - (===) OrPattern.top =<< evaluateT predicate + evaluateExpectTopK predicate ) test_concatCommutes :: TestTree @@ -385,7 +392,7 @@ test_concatCommutes = actual1 <- evaluateT patConcat1 actual2 <- evaluateT patConcat2 (===) actual1 actual2 - (===) OrPattern.top =<< evaluateT predicate + evaluateExpectTopK predicate ) test_concatAssociates :: TestTree @@ -404,7 +411,7 @@ test_concatAssociates = actual12_3 <- evaluateT patConcat12_3 actual1_23 <- evaluateT patConcat1_23 (===) actual12_3 actual1_23 - (===) OrPattern.top =<< evaluateT predicate + evaluateExpectTopK predicate ) test_inKeysUnit :: TestTree @@ -417,7 +424,7 @@ test_inKeysUnit = patInKeys = inKeysMap patKey patUnit predicate = mkEquals_ (Test.Bool.asInternal False) patInKeys (===) (Test.Bool.asOrPattern False) =<< evaluateT patInKeys - (===) OrPattern.top =<< evaluateT predicate + evaluateExpectTopK predicate ) test_keysUnit :: TestTree @@ -431,7 +438,7 @@ test_keysUnit = predicate = mkEquals_ patExpect patKeys expect <- evaluate patExpect assertEqual "" expect =<< evaluate patKeys - assertEqual "" OrPattern.top =<< evaluate predicate + assertEqual "" (OrPattern.topOf kSort) =<< evaluate predicate test_keysElement :: TestTree test_keysElement = @@ -446,7 +453,7 @@ test_keysElement = predicate = mkEquals_ patKeys patSymbolic expect <- evaluateT patKeys (===) expect =<< evaluateT patSymbolic - (===) OrPattern.top =<< evaluateT predicate + evaluateExpectTopK predicate ) test_keys :: TestTree @@ -462,7 +469,7 @@ test_keys = predicate = mkEquals_ patConcreteKeys patSymbolicKeys expect <- evaluateT patConcreteKeys (===) expect =<< evaluateT patSymbolicKeys - (===) OrPattern.top =<< evaluateT predicate + evaluateExpectTopK predicate ) test_keysListUnit :: TestTree @@ -476,7 +483,7 @@ test_keysListUnit = predicate = mkEquals_ patExpect patKeys expect <- evaluate patExpect assertEqual "" expect =<< evaluate patKeys - assertEqual "" OrPattern.top =<< evaluate predicate + assertEqual "" (OrPattern.topOf kSort) =<< evaluate predicate test_keysListElement :: TestTree test_keysListElement = @@ -491,7 +498,7 @@ test_keysListElement = predicate = mkEquals_ patKeys patSymbolic expect <- evaluateT patKeys (===) expect =<< evaluateT patSymbolic - (===) OrPattern.top =<< evaluateT predicate + evaluateExpectTopK predicate ) test_keysList :: TestTree @@ -507,7 +514,7 @@ test_keysList = predicate = mkEquals_ patConcreteKeys patSymbolicKeys expect <- evaluateT patConcreteKeys (===) expect =<< evaluateT patSymbolicKeys - (===) OrPattern.top =<< evaluateT predicate + evaluateExpectTopK predicate ) test_inKeysElement :: TestTree @@ -521,7 +528,7 @@ test_inKeysElement = patInKeys = inKeysMap patKey patMap predicate = mkEquals_ (Test.Bool.asInternal True) patInKeys (===) (Test.Bool.asOrPattern True) =<< evaluateT patInKeys - (===) OrPattern.top =<< evaluateT predicate + evaluateExpectTopK predicate ) test_values :: TestTree @@ -538,7 +545,7 @@ test_values = predicate = mkEquals_ patConcreteValues patValues expect <- evaluateT patValues (===) expect =<< evaluateT patConcreteValues - (===) OrPattern.top =<< evaluateT predicate + evaluateExpectTopK predicate ) test_inclusion :: [TestTree] @@ -559,7 +566,7 @@ test_inclusion = (mkNot (mkEquals_ patKey1 patKey2)) (mkEquals_ (Test.Bool.asInternal True) patInclusion) (===) (Test.Bool.asOrPattern True) =<< evaluateT patInclusion - (===) OrPattern.top =<< evaluateT predicate + evaluateExpectTopK predicate ) , testPropertyWithSolver "MAP.inclusion success: empty map <= empty map" @@ -567,7 +574,7 @@ test_inclusion = let patInclusion = inclusionMap unitMap unitMap predicate = mkEquals_ (Test.Bool.asInternal True) patInclusion (===) (Test.Bool.asOrPattern True) =<< evaluateT patInclusion - (===) OrPattern.top =<< evaluateT predicate + evaluateExpectTopK predicate ) , testPropertyWithSolver "MAP.inclusion success: empty map <= any map" @@ -576,7 +583,7 @@ test_inclusion = let patInclusion = inclusionMap unitMap patSomeMap predicate = mkEquals_ (Test.Bool.asInternal True) patInclusion (===) (Test.Bool.asOrPattern True) =<< evaluateT patInclusion - (===) OrPattern.top =<< evaluateT predicate + evaluateExpectTopK predicate ) , testPropertyWithSolver "MAP.inclusion failure: !(some map <= empty map)" @@ -587,7 +594,7 @@ test_inclusion = patInclusion = inclusionMap patSomeMap unitMap predicate = mkEquals_ (Test.Bool.asInternal False) patInclusion (===) (Test.Bool.asOrPattern False) =<< evaluateT patInclusion - (===) OrPattern.top =<< evaluateT predicate + evaluateExpectTopK predicate ) , testPropertyWithSolver "MAP.inclusion failure: lhs key not included in rhs map" @@ -605,7 +612,7 @@ test_inclusion = (mkNot (mkEquals_ patKey1 patKey2)) (mkEquals_ (Test.Bool.asInternal False) patInclusion) (===) (Test.Bool.asOrPattern False) =<< evaluateT patInclusion - (===) OrPattern.top =<< evaluateT predicate + evaluateExpectTopK predicate ) , testPropertyWithSolver "MAP.inclusion failure: lhs key maps differently in rhs map" @@ -627,7 +634,7 @@ test_inclusion = (mkNot (mkEquals_ patKey1 patKey2)) (mkEquals_ (Test.Bool.asInternal False) patInclusion) (===) (Test.Bool.asOrPattern False) =<< evaluateT patInclusion - (===) OrPattern.top =<< evaluateT predicate + evaluateExpectTopK predicate ) ] @@ -637,7 +644,9 @@ test_simplify = testCaseWithoutSMT "simplify builtin Map elements" $ do let x = mkIntConfigVar (testId "x") key = Test.Int.asKey 1 - original = asTermLike $ HashMap.fromList [(key, mkAnd x mkTop_)] + original = + HashMap.fromList [(key, mkAnd x (mkTop intSort))] + & asTermLike expected = MultiOr.singleton . asPattern $ HashMap.fromList [(key, x)] actual <- evaluate original @@ -697,7 +706,7 @@ test_unifyConcrete = expect <- evaluateT patExpect actual <- evaluateT patActual (===) expect actual - (===) OrPattern.top =<< evaluateT predicate + evaluateExpectTopK predicate ) -- Given a function to scramble the arguments to concat, i.e., diff --git a/kore/test/Test/Kore/Builtin/Set.hs b/kore/test/Test/Kore/Builtin/Set.hs index c8dad83e2f..850e748f57 100644 --- a/kore/test/Test/Kore/Builtin/Set.hs +++ b/kore/test/Test/Kore/Builtin/Set.hs @@ -213,6 +213,13 @@ test_unit = (OrPattern.fromTermLike expect) actual +mkEquals_ :: + InternalVariable variable => + TermLike variable -> + TermLike variable -> + TermLike variable +mkEquals_ = mkEquals kSort + test_getUnit :: TestTree test_getUnit = testPropertyWithSolver @@ -228,7 +235,7 @@ test_getUnit = patFalse = Test.Bool.asInternal False predicate = mkEquals_ patFalse patIn (===) (Test.Bool.asOrPattern False) =<< evaluateT patIn - (===) OrPattern.top =<< evaluateT predicate + evaluateExpectTopK predicate ) test_inElement :: TestTree @@ -242,7 +249,7 @@ test_inElement = patTrue = Test.Bool.asInternal True predicate = mkEquals_ patIn patTrue (===) (Test.Bool.asOrPattern True) =<< evaluateT patIn - (===) OrPattern.top =<< evaluateT predicate + evaluateExpectTopK predicate ) test_inUnitSymbolic :: TestTree @@ -260,7 +267,7 @@ test_inUnitSymbolic = patFalse = Test.Bool.asInternal False predicate = mkEquals_ patFalse patIn (===) (Test.Bool.asOrPattern False) =<< evaluateT patIn - (===) OrPattern.top =<< evaluateT predicate + evaluateExpectTopK predicate ) test_inElementSymbolic :: TestTree @@ -272,7 +279,7 @@ test_inElementSymbolic = let patElement = mkApplySymbol elementSetSymbolTestSort [patKey] patIn = mkApplySymbol inSetSymbolTestSort [patKey, patElement] patTrue = Test.Bool.asInternal True - conditionTerm = mkAnd patTrue (mkCeil_ patElement) + conditionTerm = mkAnd patTrue (mkCeil boolSort patElement) actual <- evaluateT patIn expected <- evaluateT conditionTerm actual === expected @@ -320,7 +327,7 @@ test_inConcat = patTrue = Test.Bool.asInternal True predicate = mkEquals_ patTrue patIn (===) (Test.Bool.asOrPattern True) =<< evaluateT patIn - (===) OrPattern.top =<< evaluateT predicate + evaluateExpectTopK predicate ) test_concatUnit :: TestTree @@ -339,8 +346,8 @@ test_concatUnit = expect <- evaluateT patValues (===) expect =<< evaluateT patConcat1 (===) expect =<< evaluateT patConcat2 - (===) OrPattern.top =<< evaluateT predicate1 - (===) OrPattern.top =<< evaluateT predicate2 + evaluateExpectTopK predicate1 + evaluateExpectTopK predicate2 ) test_concatAssociates :: TestTree @@ -367,7 +374,7 @@ test_concatAssociates = concat12_3 <- evaluateT patConcat12_3 concat1_23 <- evaluateT patConcat1_23 (===) concat12_3 concat1_23 - (===) OrPattern.top =<< evaluateT predicate + evaluateExpectTopK predicate ) test_concatNormalizes :: TestTree @@ -427,7 +434,7 @@ test_concatNormalizes = evalConcat <- evaluateT patConcat evalNormalized <- evaluateT patNormalized (===) evalConcat evalNormalized - (===) OrPattern.top =<< evaluateT predicate + evaluateExpectTopK predicate ) test_difference :: TestTree @@ -446,7 +453,7 @@ test_difference = predicate = mkEquals_ patSet3 patDifference expect <- evaluateT patSet3 (===) expect =<< evaluateT patDifference - (===) OrPattern.top =<< evaluateT predicate + evaluateExpectTopK predicate ) test_difference_symbolic :: [TestTree] @@ -536,7 +543,7 @@ test_toList = predicate = mkEquals_ expectedList actualList expect <- evaluateT expectedList (===) expect =<< evaluateT actualList - (===) OrPattern.top =<< evaluateT predicate + evaluateExpectTopK predicate ) where implToList = @@ -560,7 +567,7 @@ test_size = predicate = mkEquals_ patExpected patActual expect <- evaluateT patExpected (===) expect =<< evaluateT patActual - (===) OrPattern.top =<< evaluateT predicate + evaluateExpectTopK predicate ) test_intersection_unit :: TestTree @@ -570,7 +577,7 @@ test_intersection_unit = let original = intersectionSet as unitSet expect = OrPattern.fromTermLike $ asInternal HashSet.empty (===) expect =<< evaluateT original - (===) OrPattern.top =<< evaluateT (mkEquals_ original unitSet) + evaluateExpectTopK (mkEquals_ original unitSet) test_intersection_idem :: TestTree test_intersection_idem = @@ -580,7 +587,7 @@ test_intersection_idem = original = intersectionSet termLike termLike expect = OrPattern.fromTermLike $ asInternal as (===) expect =<< evaluateT original - (===) OrPattern.top =<< evaluateT (mkEquals_ original termLike) + evaluateExpectTopK (mkEquals_ original termLike) test_list2set :: TestTree test_list2set = @@ -595,8 +602,7 @@ test_list2set = original = list2setSet input expect = OrPattern.fromTermLike $ asInternal set (===) expect =<< evaluateT original - (===) OrPattern.top - =<< evaluateT (mkEquals_ original termLike) + evaluateExpectTopK (mkEquals_ original termLike) test_inclusion :: [TestTree] test_inclusion = @@ -614,7 +620,7 @@ test_inclusion = (mkNot (mkEquals_ patKey1 patKey2)) (mkEquals_ (Test.Bool.asInternal True) patInclusion) (===) (Test.Bool.asOrPattern True) =<< evaluateT patInclusion - (===) OrPattern.top =<< evaluateT predicate + evaluateExpectTopK predicate ) , testPropertyWithSolver "SET.inclusion success: empty set <= any set" @@ -623,7 +629,7 @@ test_inclusion = let patInclusion = inclusionSet unitSet patSomeSet predicate = mkEquals_ (Test.Bool.asInternal True) patInclusion (===) (Test.Bool.asOrPattern True) =<< evaluateT patInclusion - (===) OrPattern.top =<< evaluateT predicate + evaluateExpectTopK predicate ) , testPropertyWithSolver "SET.inclusion failure: not (some nonempty set <= empty set)" @@ -633,7 +639,7 @@ test_inclusion = patInclusion = inclusionSet patSomeSet unitSet predicate = mkEquals_ (Test.Bool.asInternal False) patInclusion (===) (Test.Bool.asOrPattern False) =<< evaluateT patInclusion - (===) OrPattern.top =<< evaluateT predicate + evaluateExpectTopK predicate ) , testPropertyWithSolver "SET.inclusion failure: lhs key not included in rhs set" @@ -649,7 +655,7 @@ test_inclusion = (mkNot (mkEquals_ patKey1 patKey2)) (mkEquals_ (Test.Bool.asInternal False) patInclusion) (===) (Test.Bool.asOrPattern False) =<< evaluateT patInclusion - (===) OrPattern.top =<< evaluateT predicate + evaluateExpectTopK predicate ) ] @@ -707,7 +713,7 @@ test_unifyConcreteIdem = predicate = mkEquals_ patSet patAnd expect <- evaluateT patSet (===) expect =<< evaluateT patAnd - (===) OrPattern.top =<< evaluateT predicate + evaluateExpectTopK predicate ) test_unifyConcreteDistinct :: TestTree diff --git a/kore/test/Test/Kore/Builtin/String.hs b/kore/test/Test/Kore/Builtin/String.hs index 561296ee0a..c042145b26 100644 --- a/kore/test/Test/Kore/Builtin/String.hs +++ b/kore/test/Test/Kore/Builtin/String.hs @@ -476,7 +476,7 @@ test_unifyStringEq = makeEqualsPredicate (mkElemVar x) (mkElemVar y) & makeNotPredicate & Condition.fromPredicate - & Pattern.fromCondition_ + & Pattern.fromCondition boolSort -- unit test do actual <- unifyStringEq term1 term2 @@ -507,7 +507,7 @@ test_unifyStringEq = term2 = eqString (mkElemVar x) (mkElemVar y) expect = Condition.assign (inject x) (mkElemVar y) - & Pattern.fromCondition_ + & Pattern.fromCondition boolSort -- unit test do actual <- unifyStringEq term1 term2 diff --git a/kore/test/Test/Kore/Equation/Application.hs b/kore/test/Test/Kore/Equation/Application.hs index f8a0010ed3..2d62add852 100644 --- a/kore/test/Test/Kore/Equation/Application.hs +++ b/kore/test/Test/Kore/Equation/Application.hs @@ -260,7 +260,7 @@ test_attemptEquation = "F(x) => G(x) doesn't apply to F(top)" (axiom_ (f x) (g x)) SideCondition.top - (f mkTop_) + (f (mkTop Mock.testSort)) , applies "F(x) => G(x) [concrete] applies to F(a)" (axiom_ (f x) (g x) & concrete [x]) @@ -447,7 +447,7 @@ test_attemptEquationUnification = "F(x) => G(x) doesn't apply to F(top)" (functionAxiomUnification_ fSymbol [x] (g x)) SideCondition.top - (f mkTop_) + (f (mkTop Mock.testSort)) , applies "F(x) => G(x) [concrete] applies to F(a)" (functionAxiomUnification_ fSymbol [x] (g x) & concrete [x]) diff --git a/kore/test/Test/Kore/Exec.hs b/kore/test/Test/Kore/Exec.hs index 2e9aaa1218..09ac7ba22b 100644 --- a/kore/test/Test/Kore/Exec.hs +++ b/kore/test/Test/Kore/Exec.hs @@ -647,7 +647,7 @@ applyAliasToNoArgs sort name = , aliasParams = [] , aliasSorts = applicationSorts [] sort , aliasLeft = [] - , aliasRight = mkTop_ + , aliasRight = mkTop sort } [] diff --git a/kore/test/Test/Kore/Internal/OrPattern.hs b/kore/test/Test/Kore/Internal/OrPattern.hs index c295a257fd..e260d40f12 100644 --- a/kore/test/Test/Kore/Internal/OrPattern.hs +++ b/kore/test/Test/Kore/Internal/OrPattern.hs @@ -122,7 +122,7 @@ test_distributeAnd = , testCase "\\top and (a or b) => a or b " $ do let conjunction = MultiAnd.make - [ MultiOr.singleton TermLike.mkTop_ + [ MultiOr.singleton (TermLike.mkTop Mock.testSort) , MultiOr.make [a, b] ] expect = @@ -135,7 +135,7 @@ test_distributeAnd = let conjunction = MultiAnd.make [ MultiOr.singleton a - , MultiOr.make [b, TermLike.mkBottom_] + , MultiOr.make [b, TermLike.mkBottom Mock.testSort] ] expect = MultiOr.make @@ -197,7 +197,7 @@ test_distributeApplication = let app = sigma2 [ MultiOr.singleton a - , MultiOr.make [b, TermLike.mkBottom_] + , MultiOr.make [b, TermLike.mkBottom Mock.testSort] ] expect = MultiOr.make diff --git a/kore/test/Test/Kore/Internal/Pattern.hs b/kore/test/Test/Kore/Internal/Pattern.hs index 85d8818fe5..690f489092 100644 --- a/kore/test/Test/Kore/Internal/Pattern.hs +++ b/kore/test/Test/Kore/Internal/Pattern.hs @@ -226,7 +226,7 @@ test_hasSimplifiedChildren = (setSimplifiedPred simplified mockPredicate2) ) patt = - Pattern.fromCondition_ + Pattern.fromCondition Mock.testSort . Condition.fromPredicate $ predicate assertEqual @@ -247,7 +247,7 @@ test_hasSimplifiedChildren = (setSimplifiedPred simplified mockPredicate2) ) patt = - Pattern.fromCondition_ + Pattern.fromCondition Mock.testSort . Condition.fromPredicate $ predicate assertEqual @@ -285,7 +285,7 @@ test_hasSimplifiedChildren = (setSimplifiedPred simplified mockPredicate1) (setSimplifiedPred simplified mockPredicate2) patt = - Pattern.fromCondition_ + Pattern.fromCondition Mock.testSort . Condition.fromPredicate $ predicate assertEqual @@ -309,17 +309,17 @@ test_hasSimplifiedChildren = ( Predicate.makeFloorPredicate ( Mock.functional20 (mkNu Mock.setX Mock.c) - (Mock.functionalConstr10 mkTop_) + (Mock.functionalConstr10 (mkTop Mock.testSort)) ) & Predicate.setSimplified fullySimplified ) ( Predicate.makeCeilPredicate - (Mock.tdivInt mkTop_ mkTop_) + (Mock.tdivInt (mkTop Mock.intSort) (mkTop Mock.intSort)) & Predicate.setSimplified fullySimplified ) & Predicate.setSimplified partiallySimplified patt = - Pattern.fromCondition_ + Pattern.fromCondition Mock.testSort . Condition.fromPredicate $ predicate assertEqual diff --git a/kore/test/Test/Kore/Internal/Predicate.hs b/kore/test/Test/Kore/Internal/Predicate.hs index 881d8cb0e8..5ecc7bdbac 100644 --- a/kore/test/Test/Kore/Internal/Predicate.hs +++ b/kore/test/Test/Kore/Internal/Predicate.hs @@ -165,8 +165,8 @@ test_predicate = "makePredicate yields wrapPredicate" ( traverse_ (uncurry makePredicateYieldsWrapPredicate) - [ ("Top", mkTop_) - , ("Bottom", mkBottom_) + [ ("Top", mkTop Mock.testSort) + , ("Bottom", mkBottom Mock.testSort) , ("And", mkAnd pa1 pa2) , ("Or", mkOr pa1 pa2) , ("Iff", mkIff pa1 pa2) @@ -183,24 +183,27 @@ test_predicate = , testGroup "keeps simplified bit" [ testCase "unsimplified stays unsimplified" $ - (mkEquals_ Mock.cf Mock.cg, NotSimplified) + (mkEquals Mock.topSort Mock.cf Mock.cg, NotSimplified) `makesPredicate` (makeEqualsPredicate Mock.cf Mock.cg, NotSimplified) , testCase "simplified stays simplified" $ - ( simplifiedTerm $ mkEquals_ Mock.cf Mock.cg + ( simplifiedTerm $ mkEquals Mock.topSort Mock.cf Mock.cg , IsSimplified ) `makesPredicate` (makeEqualsPredicate Mock.cf Mock.cg, IsSimplified) , testCase "Partial predicate stays simplified" $ ( simplifiedTerm $ - mkAnd mkTop_ (mkEquals_ Mock.cf Mock.cg) + mkAnd (mkTop Mock.topSort) (mkEquals Mock.topSort Mock.cf Mock.cg) , IsSimplified ) `makesPredicate` (makeEqualsPredicate Mock.cf Mock.cg, IsSimplified) , testCase "changed simplified becomes unsimplified" $ ( simplifiedTerm $ mkAnd - (mkAnd mkTop_ (mkEquals_ Mock.cf Mock.cg)) - (mkEquals_ Mock.cg Mock.ch) + ( mkAnd + (mkTop Mock.topSort) + (mkEquals Mock.topSort Mock.cf Mock.cg) + ) + (mkEquals Mock.topSort Mock.cg Mock.ch) , IsSimplified ) `makesPredicate` ( makeAndPredicate @@ -267,29 +270,33 @@ pr2 = pa1 :: TermLike VariableName pa1 = - mkEquals_ + mkEquals + Mock.topSort (mkElemVar $ a Mock.testSort) (mkElemVar $ b Mock.testSort) pa2 :: TermLike VariableName pa2 = - mkEquals_ + mkEquals + Mock.topSort (mkElemVar $ c Mock.testSort) (mkElemVar $ d Mock.testSort) ceilA :: TermLike VariableName ceilA = - mkCeil_ + mkCeil + Mock.topSort (mkElemVar $ a Mock.testSort) inA :: TermLike VariableName inA = - mkIn_ + mkIn + Mock.topSort (mkElemVar $ a Mock.testSort) (mkElemVar $ b Mock.testSort) floorA :: TermLike VariableName -floorA = mkFloor_ (mkElemVar $ a Mock.testSort) +floorA = mkFloor Mock.topSort (mkElemVar $ a Mock.testSort) a, b, c, d :: Sort -> ElementVariable VariableName a = mkElementVariable (testId "a") diff --git a/kore/test/Test/Kore/Internal/SideCondition.hs b/kore/test/Test/Kore/Internal/SideCondition.hs index 4b9a58345e..d5b0047b70 100644 --- a/kore/test/Test/Kore/Internal/SideCondition.hs +++ b/kore/test/Test/Kore/Internal/SideCondition.hs @@ -39,12 +39,12 @@ test_assumeDefined :: [TestTree] test_assumeDefined = [ testCase "Fails on \\bottom" $ do let term :: TermLike VariableName - term = mkBottom_ + term = mkBottom Mock.topSort actual = assumeDefined term assertEqual "" Nothing actual , testCase "Fails on nested \\bottom" $ do let term :: TermLike VariableName - term = Mock.f mkBottom_ + term = Mock.f (mkBottom Mock.testSort) actual = assumeDefined term assertEqual "" Nothing actual , testCase "And: implies subterms are defined" $ do @@ -73,7 +73,7 @@ test_assumeDefined = assertEqual "" expected actual , testCase "Ceil: implies subterms are defined" $ do let term :: TermLike VariableName - term = mkCeil_ Mock.plain00 + term = mkCeil Mock.topSort Mock.plain00 expected = [term, Mock.plain00] & HashSet.fromList @@ -141,7 +141,8 @@ test_assumeDefined = , testCase "In: implies subterms are defined" $ do let term :: TermLike VariableName term = - mkIn_ + mkIn + Mock.topSort (Mock.f (mkElemVar Mock.x)) (Mock.functional10 (Mock.g Mock.a)) expected = diff --git a/kore/test/Test/Kore/Reachability/Claim.hs b/kore/test/Test/Kore/Reachability/Claim.hs index 37d37307a7..e5edc7356b 100644 --- a/kore/test/Test/Kore/Reachability/Claim.hs +++ b/kore/test/Test/Kore/Reachability/Claim.hs @@ -229,7 +229,7 @@ test_checkImplication = actual <- checkImplication goal assertEqual "" [NotImpliedStuck goal] actual , testCase "Implied if both sides are \\bottom" $ do - let config = Pattern.bottom + let config = Pattern.bottomOf Mock.topSort dest = OrPattern.bottom goal = mkGoal config dest [] actual <- checkImplication goal @@ -243,19 +243,19 @@ test_simplifyRightHandSide = Pattern.fromTermAndPredicate Mock.b ( makeEqualsPredicate - TermLike.mkTop_ + (TermLike.mkTop Mock.boolSort) (Mock.builtinInt 3 `Mock.lessInt` Mock.builtinInt 2) ) claim = mkGoal - Pattern.top + (Pattern.topOf Mock.testSort) ( [Pattern.fromTermLike Mock.a, unsatisfiableBranch] & OrPattern.fromPatterns ) [] expected = mkGoal - Pattern.top + (Pattern.topOf Mock.testSort) (Mock.a & OrPattern.fromTermLike) [] actual <- diff --git a/kore/test/Test/Kore/Reachability/OnePathStrategy.hs b/kore/test/Test/Kore/Reachability/OnePathStrategy.hs index b629938ee0..b94d9ec37a 100644 --- a/kore/test/Test/Kore/Reachability/OnePathStrategy.hs +++ b/kore/test/Test/Kore/Reachability/OnePathStrategy.hs @@ -819,7 +819,7 @@ test_onePathStrategy = Mock.a ) ) - right' = Pattern.bottom + right' = Pattern.bottomOf Mock.testSort original = makeOnePathGoalFromPatterns left right expect = makeOnePathGoalFromPatterns left' right' [_actual] <- diff --git a/kore/test/Test/Kore/Reachability/Prove.hs b/kore/test/Test/Kore/Reachability/Prove.hs index 0c2b3eea76..779ed9384f 100644 --- a/kore/test/Test/Kore/Reachability/Prove.hs +++ b/kore/test/Test/Kore/Reachability/Prove.hs @@ -719,7 +719,7 @@ test_proveClaims = , testGroup "LHS is undefined" $ let mkTest name mkSimpleClaim = testCase name $ do - let claims = [mkSimpleClaim mkBottom_ Mock.a] + let claims = [mkSimpleClaim (mkBottom Mock.testSort) Mock.a] actual <- proveClaims_ Unlimited diff --git a/kore/test/Test/Kore/Repl/Interpreter.hs b/kore/test/Test/Kore/Repl/Interpreter.hs index bae667d28b..98193c6b44 100644 --- a/kore/test/Test/Kore/Repl/Interpreter.hs +++ b/kore/test/Test/Kore/Repl/Interpreter.hs @@ -39,7 +39,7 @@ import qualified Kore.Internal.OrPattern as OrPattern import qualified Kore.Internal.Pattern as Pattern import Kore.Internal.TermLike ( TermLike, - mkBottom_, + mkBottom, mkElemVar, ) import qualified Kore.Log as Log @@ -663,7 +663,10 @@ zeroToTen = emptyClaim :: SomeClaim emptyClaim = OnePath . OnePathClaim $ - claimWithName mkBottom_ mkBottom_ "emptyClaim" + claimWithName + (mkBottom kSort) + (mkBottom kSort) + "emptyClaim" zeroToZero :: SomeClaim zeroToZero = diff --git a/kore/test/Test/Kore/Rewrite/AntiLeft.hs b/kore/test/Test/Kore/Rewrite/AntiLeft.hs index 083d850de0..5e04a5e875 100644 --- a/kore/test/Test/Kore/Rewrite/AntiLeft.hs +++ b/kore/test/Test/Kore/Rewrite/AntiLeft.hs @@ -22,12 +22,12 @@ import Kore.Internal.Predicate ( import Kore.Internal.TermLike ( mkAnd, mkApplyAlias, - mkBottom_, - mkCeil_, + mkBottom, + mkCeil, mkElemVar, mkExists, mkOr, - mkTop_, + mkTop, ) import Kore.Internal.TermLike.TermLike ( TermLike, @@ -60,8 +60,11 @@ test_antiLeft = ( applyAliasToNoArgs "A" ( mkOr - (applyAliasToNoArgs "B" (mkAnd mkTop_ Mock.a)) - mkBottom_ + ( applyAliasToNoArgs + "B" + (mkAnd (mkTop Mock.testSort) Mock.a) + ) + (mkBottom Mock.testSort) ) ) ) @@ -80,9 +83,9 @@ test_antiLeft = ( mkOr ( applyAliasToNoArgs "B" - (mkAnd (mkCeil_ Mock.cg) Mock.a) + (mkAnd (mkCeil Mock.testSort Mock.cg) Mock.a) ) - mkBottom_ + (mkBottom Mock.testSort) ) ) ) @@ -99,10 +102,16 @@ test_antiLeft = ( applyAliasToNoArgs "A" ( mkOr - (applyAliasToNoArgs "B" (mkAnd mkTop_ Mock.a)) + ( applyAliasToNoArgs + "B" + (mkAnd (mkTop Mock.testSort) Mock.a) + ) ( mkOr - (applyAliasToNoArgs "C" (mkAnd mkTop_ Mock.b)) - mkBottom_ + ( applyAliasToNoArgs + "C" + (mkAnd (mkTop Mock.testSort) Mock.b) + ) + (mkBottom Mock.testSort) ) ) ) @@ -123,13 +132,19 @@ test_antiLeft = ( applyAliasToNoArgs "B" ( mkOr - (applyAliasToNoArgs "C" (mkAnd mkTop_ Mock.a)) - mkBottom_ + ( applyAliasToNoArgs + "C" + (mkAnd (mkTop Mock.testSort) Mock.a) + ) + (mkBottom Mock.testSort) ) ) ( mkOr - (applyAliasToNoArgs "D" (mkAnd mkTop_ Mock.b)) - mkBottom_ + ( applyAliasToNoArgs + "D" + (mkAnd (mkTop Mock.testSort) Mock.b) + ) + (mkBottom Mock.testSort) ) ) ) @@ -156,10 +171,13 @@ test_antiLeft = Mock.x ( applyAliasToNoArgs "B" - (mkAnd mkTop_ (Mock.f (mkElemVar Mock.x))) + ( mkAnd + (mkTop Mock.testSort) + (Mock.f (mkElemVar Mock.x)) + ) ) ) - mkBottom_ + (mkBottom Mock.testSort) ) ) ) @@ -168,7 +186,9 @@ test_antiLeft = ] parseAndApply :: - AntiLeftTerm -> TermLike VariableName -> IO (Predicate VariableName) + AntiLeftTerm -> + TermLike VariableName -> + IO (Predicate VariableName) parseAndApply (AntiLeftTerm antiLeftTerm) configurationTerm = do antiLeft <- case parse antiLeftTerm of Nothing -> diff --git a/kore/test/Test/Kore/Rewrite/Axiom/Identifier.hs b/kore/test/Test/Kore/Rewrite/Axiom/Identifier.hs index 67088cb5d6..570de2ecda 100644 --- a/kore/test/Test/Kore/Rewrite/Axiom/Identifier.hs +++ b/kore/test/Test/Kore/Rewrite/Axiom/Identifier.hs @@ -23,11 +23,14 @@ test_matchAxiomIdentifier = (Application Mock.sortInjectionId) , matches "\\ceil(f(a))" - (TermLike.mkCeil_ (Mock.f Mock.a)) + (TermLike.mkCeil Mock.topSort (Mock.f Mock.a)) (Ceil (Application Mock.fId)) , matches "\\ceil(\\ceil(f(a)))" - (TermLike.mkCeil_ (TermLike.mkCeil_ (Mock.f Mock.a))) + ( TermLike.mkCeil + Mock.topSort + (TermLike.mkCeil Mock.subSort (Mock.f Mock.a)) + ) (Ceil (Ceil (Application Mock.fId))) , notMatches "\\and(f(a), g(a))" @@ -35,7 +38,11 @@ test_matchAxiomIdentifier = , matches "x" (TermLike.mkElemVar Mock.x) Variable , matches "\\equals(x, f(a))" - (TermLike.mkEquals_ (TermLike.mkElemVar Mock.x) (Mock.f Mock.a)) + ( TermLike.mkEquals + Mock.topSort + (TermLike.mkElemVar Mock.x) + (Mock.f Mock.a) + ) (Equals Variable (Application Mock.fId)) , matches "\\exists(x, f(a))" @@ -44,7 +51,10 @@ test_matchAxiomIdentifier = , matches "\\exists(x, \\equals(x, f(a)))" ( TermLike.mkExists Mock.x $ - TermLike.mkEquals_ (TermLike.mkElemVar Mock.x) (Mock.f Mock.a) + TermLike.mkEquals + Mock.topSort + (TermLike.mkElemVar Mock.x) + (Mock.f Mock.a) ) (Exists (Equals Variable (Application Mock.fId))) , testGroup @@ -100,7 +110,7 @@ test_matchAxiomIdentifier = [ matches name termLike axiomIdentifier , matches ceilName - (TermLike.mkCeil_ termLike) + (TermLike.mkCeil Mock.topSort termLike) (Ceil axiomIdentifier) ] where diff --git a/kore/test/Test/Kore/Rewrite/Axiom/Matcher.hs b/kore/test/Test/Kore/Rewrite/Axiom/Matcher.hs index 916e51cb0d..d40c2fb398 100644 --- a/kore/test/Test/Kore/Rewrite/Axiom/Matcher.hs +++ b/kore/test/Test/Kore/Rewrite/Axiom/Matcher.hs @@ -99,7 +99,10 @@ test_matcherEqualHeads = ] , testCase "Bottom" $ do let expect = Just (makeTruePredicate, Map.empty) - actual <- matchDefinition mkBottom_ mkBottom_ + actual <- + matchDefinition + (mkBottom Mock.topSort) + (mkBottom Mock.topSort) assertEqual "" expect actual , testCase "Ceil" $ do let expect = @@ -109,8 +112,8 @@ test_matcherEqualHeads = ) actual <- matchDefinition - (mkCeil_ (Mock.plain10 (mkElemVar Mock.xConfig))) - (mkCeil_ (Mock.plain10 Mock.a)) + (mkCeil Mock.topSort (Mock.plain10 (mkElemVar Mock.xConfig))) + (mkCeil Mock.topSort (Mock.plain10 Mock.a)) assertEqual "" expect actual , testCase "Equals" $ do let expect = @@ -122,11 +125,13 @@ test_matcherEqualHeads = ) actual <- matchDefinition - ( mkEquals_ + ( mkEquals + Mock.topSort (Mock.plain10 (mkElemVar Mock.xConfig)) (Mock.plain10 Mock.a) ) - ( mkEquals_ + ( mkEquals + Mock.topSort (Mock.plain10 (mkElemVar Mock.yConfig)) (Mock.plain10 Mock.a) ) @@ -172,8 +177,8 @@ test_matcherEqualHeads = , testCase "Top" $ do actual <- matchDefinition - mkTop_ - mkTop_ + (mkTop Mock.topSort) + (mkTop Mock.topSort) assertEqual "" topCondition actual , testCase "Iff vs Or" $ do let expect = Nothing diff --git a/kore/test/Test/Kore/Rewrite/Axiom/Registry.hs b/kore/test/Test/Kore/Rewrite/Axiom/Registry.hs index 0dba68a4ea..9fa14e700d 100644 --- a/kore/test/Test/Kore/Rewrite/Axiom/Registry.hs +++ b/kore/test/Test/Kore/Rewrite/Axiom/Registry.hs @@ -407,8 +407,8 @@ testDef = , sentenceAxiomPattern = externalize $ mkRewrites - (mkAnd mkTop_ (mkApplySymbol fHead [])) - (mkAnd mkTop_ (mkApplySymbol tHead [])) + (mkAnd (mkTop sortS) (mkApplySymbol fHead [])) + (mkAnd (mkTop sortS) (mkApplySymbol tHead [])) } , SentenceAxiomSentence SentenceAxiom @@ -422,7 +422,7 @@ testDef = ( mkEquals sortVarS (mkCeil sortVar1S (mkApplySymbol fHead [])) - mkTop_ + (mkTop sortVar1S) ) (mkTop sortVarS) ) diff --git a/kore/test/Test/Kore/Rewrite/Function/Integration.hs b/kore/test/Test/Kore/Rewrite/Function/Integration.hs index 26a6ebfe89..fcf2a1090e 100644 --- a/kore/test/Test/Kore/Rewrite/Function/Integration.hs +++ b/kore/test/Test/Kore/Rewrite/Function/Integration.hs @@ -134,7 +134,7 @@ test_functionIntegration = ) ) (Mock.functional10 Mock.c) - assertEqual "" expect (OrPattern.toTermLike actual) + assertEqual "" expect (OrPattern.toTermLike Mock.testSort actual) , testCase "Simple evaluation (builtin branch)" $ do let expect = Mock.g Mock.c actual <- @@ -148,7 +148,7 @@ test_functionIntegration = ) ) (Mock.functional10 Mock.c) - assertEqual "" expect (OrPattern.toTermLike actual) + assertEqual "" expect (OrPattern.toTermLike Mock.testSort actual) , testCase "Simple evaluation (Axioms & Builtin branch, Builtin works)" $ do let expect = Mock.g Mock.c @@ -169,7 +169,7 @@ test_functionIntegration = ) ) (Mock.functional10 Mock.c) - assertEqual "" expect (OrPattern.toTermLike actual) + assertEqual "" expect (OrPattern.toTermLike Mock.testSort actual) , testCase "Simple evaluation (Axioms & Builtin branch, Builtin fails)" $ do let expect = Mock.g Mock.c @@ -189,7 +189,7 @@ test_functionIntegration = ) ) (Mock.functional10 Mock.c) - assertEqual "" expect (OrPattern.toTermLike actual) + assertEqual "" expect (OrPattern.toTermLike Mock.testSort actual) , testCase "Evaluates inside functions" $ do let expect = Mock.functional11 (Mock.functional11 Mock.c) actual <- @@ -202,7 +202,7 @@ test_functionIntegration = ) ) (Mock.functional10 (Mock.functional10 Mock.c)) - assertEqual "" expect (OrPattern.toTermLike actual) + assertEqual "" expect (OrPattern.toTermLike Mock.testSort actual) , testCase "Evaluates 'or'" $ do let expect = mkOr @@ -223,7 +223,7 @@ test_functionIntegration = (Mock.functional10 Mock.d) ) ) - assertEqual "" expect (OrPattern.toTermLike actual) + assertEqual "" expect (OrPattern.toTermLike Mock.testSort actual) , testCase "Evaluates on multiple branches" $ do let expect = Mock.functional11 @@ -246,7 +246,7 @@ test_functionIntegration = (Mock.functional10 Mock.c) ) ) - assertEqual "" expect (OrPattern.toTermLike actual) + assertEqual "" expect (OrPattern.toTermLike Mock.testSort actual) , testCase "Returns conditions" $ do let expect = Conditional @@ -452,7 +452,7 @@ test_functionIntegration = [ "Expected:" , Pretty.indent 4 (unparse expect) , "but found:" - , Pretty.indent 4 (unparse $ OrPattern.toTermLike actual) + , Pretty.indent 4 (Pretty.pretty actual) ] assertEqual message (MultiOr.singleton expect) actual , testCase "Evaluates only simplifications." $ do @@ -1664,11 +1664,11 @@ test_updateList = , equals "negative index" (updateList singletonList (mkInt (-1)) (mkInt 1)) - [mkBottom_] + [mkBottom listSort] , equals "positive index outside rage" (updateList singletonList (mkInt 1) (mkInt 1)) - [mkBottom_] + [mkBottom listSort] , applies "same abstract key" [updateListSimplifier] @@ -1850,7 +1850,7 @@ test_Ceil = [ simplifies "\\ceil(dummy(X)) => ... ~ \\ceil(dummy(Y))" ceilDummyRule - (mkCeil_ $ Builtin.dummyInt $ mkElemVar yConfigInt) + (mkCeil Builtin.kSort $ Builtin.dummyInt $ mkElemVar yConfigInt) , notSimplifies "\\ceil(dummy(X)) => \\not(\\equals(X, 0)) !~ dummy(Y)" ceilDummyRule @@ -1858,20 +1858,20 @@ test_Ceil = , simplifies "\\ceil(dummy(@X)) => ... ~ \\ceil(dummy(Y))" ceilDummySetRule - (mkCeil_ $ Builtin.dummyInt $ mkElemVar yConfigInt) + (mkCeil Builtin.kSort $ Builtin.dummyInt $ mkElemVar yConfigInt) ] ceilDummyRule :: Equation RewritingVariableName ceilDummyRule = axiom_ - (mkCeil_ $ Builtin.dummyInt $ mkElemVar xConfigInt) - (mkEquals_ (Builtin.eqInt (mkElemVar xConfigInt) (mkInt 0)) (mkBool False)) + (mkCeil Builtin.kSort $ Builtin.dummyInt $ mkElemVar xConfigInt) + (mkEquals Builtin.kSort (Builtin.eqInt (mkElemVar xConfigInt) (mkInt 0)) (mkBool False)) ceilDummySetRule :: Equation RewritingVariableName ceilDummySetRule = axiom_ - (mkCeil_ $ Builtin.dummyInt $ mkSetVar xsConfigInt) - (mkEquals_ (Builtin.eqInt (mkSetVar xsConfigInt) (mkInt 0)) (mkBool False)) + (mkCeil Builtin.kSort $ Builtin.dummyInt $ mkSetVar xsConfigInt) + (mkEquals Builtin.kSort (Builtin.eqInt (mkSetVar xsConfigInt) (mkInt 0)) (mkBool False)) -- Simplification tests: check that one or more rules applies or not withSimplified :: diff --git a/kore/test/Test/Kore/Rewrite/Implication.hs b/kore/test/Test/Kore/Rewrite/Implication.hs index f71cde3bb6..0ed290e4f7 100644 --- a/kore/test/Test/Kore/Rewrite/Implication.hs +++ b/kore/test/Test/Kore/Rewrite/Implication.hs @@ -91,7 +91,8 @@ test_substitute :: [TestTree] test_substitute = [ testCase "does not capture free variables from the substitution" $ do let dummy = - Pattern.fromCondition_ + Pattern.fromCondition + Mock.testSort (fromPredicate Predicate.makeTruePredicate) right = OrPattern.fromTermLike (mkElemVar y) imp = mkImplication () dummy right [x] diff --git a/kore/test/Test/Kore/Rewrite/MockSymbols.hs b/kore/test/Test/Kore/Rewrite/MockSymbols.hs index 422833fd27..370512f12a 100644 --- a/kore/test/Test/Kore/Rewrite/MockSymbols.hs +++ b/kore/test/Test/Kore/Rewrite/MockSymbols.hs @@ -444,6 +444,9 @@ constr11Symbol = symbol constr11Id [testSort] testSort & constructor constr20Symbol :: Symbol constr20Symbol = symbol constr20Id [testSort, testSort] testSort & constructor +constrIntSymbol :: Symbol +constrIntSymbol = symbol constr10Id [intSort] intSort & constructor + constrFunct20TestMapSymbol :: Symbol constrFunct20TestMapSymbol = symbol constrFunct20TestMapId [testSort, mapSort] testSort @@ -1183,13 +1186,15 @@ constr00 :: InternalVariable variable => HasCallStack => TermLike variable constr00 = Internal.mkApplySymbol constr00Symbol [] constr10 - , constr11 :: + , constr11 + , constrInt :: InternalVariable variable => HasCallStack => TermLike variable -> TermLike variable constr10 arg = Internal.mkApplySymbol constr10Symbol [arg] constr11 arg = Internal.mkApplySymbol constr11Symbol [arg] +constrInt arg = Internal.mkApplySymbol constrIntSymbol [arg] constr20 :: InternalVariable variable => diff --git a/kore/test/Test/Kore/Rewrite/RewriteStep.hs b/kore/test/Test/Kore/Rewrite/RewriteStep.hs index 0ce2ae7ca1..9934b599b0 100644 --- a/kore/test/Test/Kore/Rewrite/RewriteStep.hs +++ b/kore/test/Test/Kore/Rewrite/RewriteStep.hs @@ -990,12 +990,12 @@ test_applyRewriteRule_ = axiomSigmaTopId = RewriteRule $ rulePattern - (Mock.sigma (mkElemVar Mock.xRule) mkTop_) + (Mock.sigma (mkElemVar Mock.xRule) (mkTop Mock.testSort)) (mkElemVar Mock.xRule) claimSigmaTopId = claimPatternFromTerms - (Mock.sigma (mkElemVar Mock.xRule) mkTop_) + (Mock.sigma (mkElemVar Mock.xRule) (mkTop Mock.testSort)) (mkElemVar Mock.xRule) [] diff --git a/kore/test/Test/Kore/Rewrite/Rule.hs b/kore/test/Test/Kore/Rewrite/Rule.hs index b2715be222..6f1749db2b 100644 --- a/kore/test/Test/Kore/Rewrite/Rule.hs +++ b/kore/test/Test/Kore/Rewrite/Rule.hs @@ -105,8 +105,8 @@ axiomPatternsUnitTests = ( applyInj sortKItem ( mkRewrites - (mkAnd mkTop_ varI1) - (mkAnd mkTop_ varI2) + (mkAnd (mkTop sortAInt) varI1) + (mkAnd (mkTop sortAInt) varI2) ) ) moduleTest = @@ -152,8 +152,8 @@ axiomPatternsUnitTests = symbolInj [sortAInt, sortKItem] [ mkRewrites - (mkAnd mkTop_ varI1) - (mkAnd mkTop_ varI2) + (mkAnd (mkTop sortAInt) varI1) + (mkAnd (mkTop sortAInt) varI2) ] ) ) diff --git a/kore/test/Test/Kore/Rewrite/Rule/Combine.hs b/kore/test/Test/Kore/Rewrite/Rule/Combine.hs index 73d3356148..f86730c8f6 100644 --- a/kore/test/Test/Kore/Rewrite/Rule/Combine.hs +++ b/kore/test/Test/Kore/Rewrite/Rule/Combine.hs @@ -27,9 +27,9 @@ import Kore.Internal.TermLike ( TermLike, mkAnd, mkApplyAlias, - mkBottom_, + mkBottom, mkElemVar, - mkEquals_, + mkEquals, mkOr, ) import qualified Kore.Internal.TermLike as TermLike.DoNotUse @@ -206,9 +206,12 @@ test_combineRulesPredicate = ( mkOr ( applyAlias "B" - (mkAnd (mkEquals_ Mock.cf Mock.cg) Mock.ch) + ( mkAnd + (mkEquals Mock.testSort Mock.cf Mock.cg) + Mock.ch + ) ) - mkBottom_ + (mkBottom Mock.testSort) ) ) let expected = diff --git a/kore/test/Test/Kore/Simplify/And.hs b/kore/test/Test/Kore/Simplify/And.hs index 9d62cfdd0a..54d5e1eb7f 100644 --- a/kore/test/Test/Kore/Simplify/And.hs +++ b/kore/test/Test/Kore/Simplify/And.hs @@ -46,15 +46,15 @@ test_andSimplification = assertEqual "false and true = false" OrPattern.bottom - =<< evaluate (makeAnd [] [Pattern.top]) + =<< evaluate (makeAnd [] [Pattern.topOf Mock.testSort]) assertEqual "true and false = false" OrPattern.bottom - =<< evaluate (makeAnd [Pattern.top] []) + =<< evaluate (makeAnd [Pattern.topOf Mock.testSort] []) assertEqual "true and true = true" - OrPattern.top - =<< evaluate (makeAnd [Pattern.top] [Pattern.top]) + (OrPattern.topOf Mock.testSort) + =<< evaluate (makeAnd [Pattern.topOf Mock.testSort] [Pattern.topOf Mock.testSort]) , testCase "And with booleans" $ do assertEqual "false and something = false" @@ -67,11 +67,11 @@ test_andSimplification = assertEqual "true and something = something" (OrPattern.fromPatterns [fOfXExpanded]) - =<< evaluate (makeAnd [Pattern.top] [fOfXExpanded]) + =<< evaluate (makeAnd [Pattern.topOf Mock.testSort] [fOfXExpanded]) assertEqual "something and true = something" (OrPattern.fromPatterns [fOfXExpanded]) - =<< evaluate (makeAnd [fOfXExpanded] [Pattern.top]) + =<< evaluate (makeAnd [fOfXExpanded] [Pattern.topOf Mock.testSort]) , testCase "And with partial booleans" $ do assertEqual "false term and something = false" @@ -110,7 +110,7 @@ test_andSimplification = , testCase "And predicates" $ do let expect = Conditional - { term = mkTop_ + { term = mkTop Mock.testSort , predicate = makeAndPredicate (makeCeilPredicate fOfX) @@ -120,12 +120,12 @@ test_andSimplification = actual <- evaluatePatterns Conditional - { term = mkTop_ + { term = mkTop Mock.testSort , predicate = makeCeilPredicate fOfX , substitution = mempty } Conditional - { term = mkTop_ + { term = mkTop Mock.testSort , predicate = makeCeilPredicate gOfX , substitution = mempty } @@ -133,7 +133,7 @@ test_andSimplification = , testCase "And substitutions - simple" $ do let expect = Conditional - { term = mkTop_ + { term = mkTop Mock.testSort , predicate = makeTruePredicate , substitution = Substitution.unsafeWrap @@ -144,7 +144,7 @@ test_andSimplification = actual <- evaluatePatterns Conditional - { term = mkTop_ + { term = mkTop Mock.testSort , predicate = makeTruePredicate , substitution = Substitution.wrap $ @@ -152,7 +152,7 @@ test_andSimplification = [(inject Mock.yConfig, fOfX)] } Conditional - { term = mkTop_ + { term = mkTop Mock.testSort , predicate = makeTruePredicate , substitution = Substitution.wrap $ @@ -183,7 +183,7 @@ test_andSimplification = , testCase "And substitutions - separate predicate" $ do let expect = Conditional - { term = mkTop_ + { term = mkTop Mock.testSort , predicate = makeEqualsPredicate fOfX gOfX , substitution = Substitution.unsafeWrap [(inject Mock.yConfig, fOfX)] @@ -191,7 +191,7 @@ test_andSimplification = actual <- evaluatePatterns Conditional - { term = mkTop_ + { term = mkTop Mock.testSort , predicate = makeTruePredicate , substitution = Substitution.wrap $ @@ -199,7 +199,7 @@ test_andSimplification = [(inject Mock.yConfig, fOfX)] } Conditional - { term = mkTop_ + { term = mkTop Mock.testSort , predicate = makeTruePredicate , substitution = Substitution.wrap $ @@ -211,7 +211,7 @@ test_andSimplification = actual <- evaluatePatterns Conditional - { term = mkTop_ + { term = mkTop Mock.testSort , predicate = makeTruePredicate , substitution = Substitution.wrap $ @@ -224,7 +224,7 @@ test_andSimplification = ] } Conditional - { term = mkTop_ + { term = mkTop Mock.testSort , predicate = makeTruePredicate , substitution = Substitution.wrap $ @@ -244,7 +244,7 @@ test_andSimplification = assertEqual "Combines conditions with substitution merge condition" Pattern - { term = mkTop_ + { term = mkTop Mock.topSort , predicate = fst $ makeAndPredicate (fst $ makeAndPredicate @@ -259,12 +259,12 @@ test_andSimplification = , (gSymbol, mock.functionAttributes) ] Pattern - { term = mkTop_ + { term = mkTop Mock.topSort , predicate = makeCeilPredicate fOfX , substitution = [(y, fOfX)] } Pattern - { term = mkTop_ + { term = mkTop Mock.topSort , predicate = makeCeilPredicate gOfX , substitution = [(y, gOfX)] } @@ -352,7 +352,7 @@ test_andSimplification = , substitution = mempty } , Conditional - { term = mkTop_ + { term = mkTop Mock.testSort , predicate = makeAndPredicate (makeCeilPredicate fOfX) @@ -365,14 +365,14 @@ test_andSimplification = ( makeAnd [ fOfXExpanded , Conditional - { term = mkTop_ + { term = mkTop Mock.testSort , predicate = makeCeilPredicate fOfX , substitution = mempty } ] [ gOfXExpanded , Conditional - { term = mkTop_ + { term = mkTop Mock.testSort , predicate = makeCeilPredicate gOfX , substitution = mempty } @@ -435,13 +435,13 @@ test_andSimplification = } bottomTerm = Conditional - { term = mkBottom_ + { term = mkBottom Mock.topSort , predicate = makeTruePredicate , substitution = mempty } falsePredicate = Conditional - { term = mkTop_ + { term = mkTop Mock.topSort , predicate = makeFalsePredicate , substitution = mempty } @@ -466,7 +466,7 @@ evaluate :: IO (OrPattern RewritingVariableName) evaluate And{andFirst, andSecond} = MultiAnd.make [andFirst, andSecond] - & simplify Not.notSimplifier SideCondition.top + & simplify Mock.testSort Not.notSimplifier SideCondition.top & runSimplifier Mock.env evaluatePatterns :: @@ -475,6 +475,6 @@ evaluatePatterns :: IO (OrPattern RewritingVariableName) evaluatePatterns first second = MultiAnd.make [first, second] - & makeEvaluate Not.notSimplifier SideCondition.top + & makeEvaluate Mock.testSort Not.notSimplifier SideCondition.top & runSimplifierBranch Mock.env & fmap OrPattern.fromPatterns diff --git a/kore/test/Test/Kore/Simplify/AndTerms.hs b/kore/test/Test/Kore/Simplify/AndTerms.hs index 4a856c8bae..10886deba0 100644 --- a/kore/test/Test/Kore/Simplify/AndTerms.hs +++ b/kore/test/Test/Kore/Simplify/AndTerms.hs @@ -83,25 +83,25 @@ test_andTermsSimplification = "Predicates" [ testCase "\\and{s}(f{}(a), \\top{s}())" $ do let expected = Pattern.fromTermLike fOfA - actual <- simplifyUnify fOfA mkTop_ + actual <- simplifyUnify fOfA (mkTop Mock.testSort) assertEqual "" ([expected], [expected]) actual , testCase "\\and{s}(\\top{s}(), f{}(a))" $ do let expected = Pattern.fromTermLike fOfA - actual <- simplifyUnify mkTop_ fOfA + actual <- simplifyUnify (mkTop Mock.testSort) fOfA assertEqual "" ([expected], [expected]) actual , testCase "\\and{s}(f{}(a), \\bottom{s}())" $ do let expect = - ( [Pattern.bottom] - , [Pattern.bottom] + ( [Pattern.bottomOf Mock.testSort] + , [Pattern.bottomOf Mock.testSort] ) - actual <- simplifyUnify fOfA mkBottom_ + actual <- simplifyUnify fOfA (mkBottom Mock.testSort) assertEqual "" expect actual , testCase "\\and{s}(\\bottom{s}(), f{}(a))" $ do let expect = - ( [Pattern.bottom] - , [Pattern.bottom] + ( [Pattern.bottomOf Mock.testSort] + , [Pattern.bottomOf Mock.testSort] ) - actual <- simplifyUnify mkBottom_ fOfA + actual <- simplifyUnify (mkBottom Mock.testSort) fOfA assertEqual "" expect actual ] , testCase "equal patterns and" $ do @@ -935,7 +935,7 @@ test_andTermsSimplification = , testCase "different lengths" $ do let term7 = Mock.builtinList [Mock.a, Mock.a] term8 = Mock.builtinList [Mock.a] - expect = [Pattern.bottom] + expect = [Pattern.bottomOf Mock.listSort] actual <- unify term7 term8 assertEqual "" expect actual , testCase "fallback for external List symbols" $ do @@ -1125,29 +1125,41 @@ test_andTermsSimplification = "alias expansion" [ testCase "alias() vs top" $ do let x = mkVariable "x" - alias = mkAlias' "alias1" x mkTop_ + alias = mkAlias' "alias1" x $ mkTop Mock.testSort left = applyAlias' alias $ mkTop Mock.testSort & mkRewritingTerm - actual <- simplifyUnify left mkTop_ - assertExpectTop actual + actual <- simplifyUnify left (mkTop Mock.testSort) + let expect = + ( [Pattern.topOf Mock.testSort] + , [Pattern.topOf Mock.testSort] + ) + assertEqual "" expect actual , testCase "alias1() vs alias2()" $ do let x = mkVariable "x" - leftAlias = mkAlias' "leftAlias" x mkTop_ + leftAlias = mkAlias' "leftAlias" x $ mkTop Mock.testSort left = applyAlias' leftAlias $ mkTop Mock.testSort - rightAlias = mkAlias' "rightAlias" x mkTop_ + rightAlias = mkAlias' "rightAlias" x $ mkTop Mock.testSort right = applyAlias' rightAlias $ mkTop Mock.testSort actual <- simplifyUnify left right - assertExpectTop actual + let expect = + ( [Pattern.topOf Mock.testSort] + , [Pattern.topOf Mock.testSort] + ) + assertEqual "" expect actual , testCase "alias1(alias2()) vs top" $ do let x = mkVariable "x" y = mkVariable "y" - alias1 = mkAlias' "alias1" x mkTop_ + alias1 = mkAlias' "alias1" x (mkTop Mock.testSort) alias1App = applyAlias' alias1 $ mkSetVar (SetVariableName <$> y) alias2 = mkAlias' "alias2" x alias1App alias2App = applyAlias' alias2 $ mkTop Mock.testSort - actual <- simplifyUnify alias2App mkTop_ - assertExpectTop actual + expect = + ( [Pattern.topOf Mock.testSort] + , [Pattern.topOf Mock.testSort] + ) + actual <- simplifyUnify alias2App (mkTop $ termLikeSort alias2App) + assertEqual "" expect actual , testCase "alias1() vs injHead" $ do let expect = Conditional @@ -1304,12 +1316,6 @@ applyAlias' :: TermLike variable applyAlias' alias arg = applyAlias alias [] [arg] -assertExpectTop :: - ([Pattern RewritingVariableName], [Pattern RewritingVariableName]) -> - IO () -assertExpectTop = - assertEqual "" ([Pattern.top], [Pattern.top]) - test_equalsTermsSimplification :: [TestTree] test_equalsTermsSimplification = [ testCase "adds ceil when producing substitutions" $ do diff --git a/kore/test/Test/Kore/Simplify/Application.hs b/kore/test/Test/Kore/Simplify/Application.hs index e897964501..b7c91d731f 100644 --- a/kore/test/Test/Kore/Simplify/Application.hs +++ b/kore/test/Test/Kore/Simplify/Application.hs @@ -89,7 +89,7 @@ test_applicationSimplification = assertEqual "" expect actual , testCase "Application - bottom child makes everything bottom" $ do -- sigma(a or b, bottom) = bottom - let expect = OrPattern.fromPatterns [Pattern.bottom] + let expect = OrPattern.fromPatterns [Pattern.bottomOf Mock.testSort] actual <- evaluate Map.empty @@ -112,7 +112,7 @@ test_applicationSimplification = ( makeApplication Mock.sigmaSymbol [ [aExpanded] - , [Pattern.top] + , [Pattern.topOf Mock.testSort] ] ) assertEqual "" expect actual diff --git a/kore/test/Test/Kore/Simplify/Bottom.hs b/kore/test/Test/Kore/Simplify/Bottom.hs index 2f173f0b00..c622077a64 100644 --- a/kore/test/Test/Kore/Simplify/Bottom.hs +++ b/kore/test/Test/Kore/Simplify/Bottom.hs @@ -6,9 +6,7 @@ import Kore.Internal.OrPattern ( OrPattern, ) import qualified Kore.Internal.OrPattern as OrPattern -import qualified Kore.Internal.Pattern as Pattern ( - bottom, - ) +import qualified Kore.Internal.Pattern as Pattern import Kore.Rewrite.RewritingVariable ( RewritingVariableName, ) @@ -28,7 +26,7 @@ test_bottomSimplification = "Bottom evaluates to bottom" ( assertEqual "" - (OrPattern.fromPatterns [Pattern.bottom]) + (OrPattern.fromPatterns [Pattern.bottomOf Mock.testSort]) (evaluate Bottom{bottomSort = Mock.testSort}) ) ] diff --git a/kore/test/Test/Kore/Simplify/Ceil.hs b/kore/test/Test/Kore/Simplify/Ceil.hs index 7a2effc1b8..3512a3f3d7 100644 --- a/kore/test/Test/Kore/Simplify/Ceil.hs +++ b/kore/test/Test/Kore/Simplify/Ceil.hs @@ -77,7 +77,7 @@ test_ceilSimplification = actual1 <- evaluate ( makeCeil - [Pattern.top] + [Pattern.topOf Mock.testSort] ) assertEqual "ceil(top)" @@ -112,13 +112,13 @@ test_ceilSimplification = "expanded Ceil - bool operations" ( do -- ceil(top) = top - actual1 <- makeEvaluate Pattern.top + actual1 <- makeEvaluate (Pattern.topOf Mock.testSort) assertEqual "ceil(top)" OrCondition.top actual1 -- ceil(bottom) = bottom - actual2 <- makeEvaluate Pattern.bottom + actual2 <- makeEvaluate (Pattern.bottomOf Mock.testSort) assertEqual "ceil(bottom)" OrCondition.bottom @@ -350,7 +350,7 @@ test_ceilSimplification = ) ( appliedMockEvaluator Conditional - { term = mkTop_ + { term = mkTop Mock.testSort , predicate = makeEqualsPredicate Mock.a Mock.cf , substitution = mempty } diff --git a/kore/test/Test/Kore/Simplify/Equals.hs b/kore/test/Test/Kore/Simplify/Equals.hs index 638cf02c74..868ec3cc14 100644 --- a/kore/test/Test/Kore/Simplify/Equals.hs +++ b/kore/test/Test/Kore/Simplify/Equals.hs @@ -47,7 +47,6 @@ import Kore.Simplify.Equals ( makeEvaluateTermsToPredicate, simplify, ) -import Kore.Unparser import Prelude.Kore import qualified Pretty import qualified Test.Kore.Rewrite.MockSymbols as Mock @@ -302,12 +301,12 @@ test_equalsSimplification_Pattern = actual <- evaluate Conditional - { term = mkTop_ + { term = mkTop testSort , predicate = makeEqualsPredicate fOfA fOfB , substitution = mempty } Conditional - { term = mkTop_ + { term = mkTop testSort , predicate = makeEqualsPredicate gOfA gOfB , substitution = mempty } @@ -376,8 +375,8 @@ test_equalsSimplification_TermLike = "bottom == bottom" ( assertTermEquals Condition.topCondition - mkBottom_ - mkBottom_ + (mkBottom testSort) + (mkBottom testSort) ) , testCase "domain-value == domain-value" @@ -431,7 +430,7 @@ test_equalsSimplification_TermLike = "a != bottom" ( assertTermEquals Condition.bottomCondition - mkBottom_ + (mkBottom testSort) Mock.a ) , testCase @@ -914,15 +913,18 @@ assertBidirectionalEqualityResult actualEvaluateEquals <- evaluateOr orderedEquality let assertEqual' name expect actual = let message = - unlines - [ firstName ++ " vs " ++ secondName ++ ":" - , "Expected " <> name - , unparseToString - (OrPattern.toTermLike <$> orderedEquality) - , "would simplify to:" - , unlines (show . Pretty.pretty <$> toList expect) - , "but instead found:" - , unlines (show . Pretty.pretty <$> toList actual) + (show . Pretty.vsep) + [ Pretty.hsep + [ Pretty.pretty firstName + , "vs" + , Pretty.pretty secondName <> Pretty.colon + ] + , "Expected" Pretty.<+> name + , (Pretty.indent 4) (Pretty.pretty orderedEquality) + , "would simplify to" + , (Pretty.indent 4) (Pretty.pretty expect) + , "but instead found" + , (Pretty.indent 4) (Pretty.pretty actual) ] in assertEqual message expect actual assertEqual' @@ -976,8 +978,8 @@ assertTermEqualsMultiGeneric expect first second = do where termToPattern :: TermLike RewritingVariableName -> Pattern RewritingVariableName - termToPattern (Bottom_ _) = - Conditional.bottom + termToPattern (Bottom_ sort) = + Conditional.bottomOf sort termToPattern term = Conditional { term = term diff --git a/kore/test/Test/Kore/Simplify/Exists.hs b/kore/test/Test/Kore/Simplify/Exists.hs index f8cb1c3538..bde9fd1e09 100644 --- a/kore/test/Test/Kore/Simplify/Exists.hs +++ b/kore/test/Test/Kore/Simplify/Exists.hs @@ -40,7 +40,7 @@ test_simplify :: [TestTree] test_simplify = [ [plain10, plain11] `simplifiesTo` [plain10', plain11'] $ "\\or distribution" - , [Pattern.top] `simplifiesTo` [Pattern.top] $ + , [Pattern.topOf Mock.testSort] `simplifiesTo` [Pattern.topOf Mock.testSort] $ "\\top" , [] `simplifiesTo` [] $ "\\bottom" @@ -158,18 +158,18 @@ test_makeEvaluate = [ testGroup "Exists - Predicates" [ testCase "Top" $ do - let expect = OrPattern.fromPatterns [Pattern.top] + let expect = OrPattern.fromPatterns [Pattern.topOf Mock.testSort] actual <- makeEvaluate Mock.xConfig - (Pattern.top :: Pattern RewritingVariableName) + (Pattern.topOf Mock.testSort :: Pattern RewritingVariableName) assertEqual "" expect actual , testCase " Bottom" $ do let expect = OrPattern.fromPatterns [] actual <- makeEvaluate Mock.xConfig - (Pattern.bottom :: Pattern RewritingVariableName) + (Pattern.bottomOf Mock.testSort :: Pattern RewritingVariableName) assertEqual "" expect actual ] , testCase "exists applies substitution if possible" $ do @@ -284,12 +284,12 @@ test_makeEvaluate = , testCase "exists reevaluates" $ do -- exists x . (top and (f(x) = f(g(a)) and [x=g(a)]) -- = top.s - let expect = OrPattern.fromPatterns [Pattern.top] + let expect = OrPattern.fromPatterns [Pattern.topOf Mock.testSort] actual <- makeEvaluate Mock.xConfig Conditional - { term = mkTop_ + { term = mkTop Mock.testSort , predicate = makeEqualsPredicate fOfX (Mock.f gOfA) , substitution = Substitution.wrap $ diff --git a/kore/test/Test/Kore/Simplify/Floor.hs b/kore/test/Test/Kore/Simplify/Floor.hs index 3434d71a3f..90eab96d1d 100644 --- a/kore/test/Test/Kore/Simplify/Floor.hs +++ b/kore/test/Test/Kore/Simplify/Floor.hs @@ -14,11 +14,7 @@ import Kore.Internal.Pattern ( Conditional (..), Pattern, ) -import qualified Kore.Internal.Pattern as Pattern ( - bottom, - fromCondition, - top, - ) +import qualified Kore.Internal.Pattern as Pattern import Kore.Internal.Predicate ( makeAndPredicate, makeEqualsPredicate, @@ -41,6 +37,7 @@ import Test.Kore ( testId, ) import Test.Kore.Rewrite.MockSymbols ( + subSort, testSort, ) import Test.Kore.Simplify @@ -56,7 +53,7 @@ test_floorSimplification = "" ( OrPattern.fromPatterns [ Conditional - { term = mkTop_ + { term = mkTop testSort , predicate = makeFloorPredicate (mkOr a b) , substitution = mempty } @@ -75,11 +72,11 @@ test_floorSimplification = assertEqual "floor(top)" ( OrPattern.fromPatterns - [Pattern.top] + [Pattern.topOf testSort] ) ( evaluate ( makeFloor - [Pattern.top] + [Pattern.topOf subSort] ) ) -- floor(bottom) = bottom @@ -99,7 +96,7 @@ test_floorSimplification = assertEqual "floor(top)" ( OrPattern.fromPatterns - [Pattern.top] + [Pattern.topOf testSort] ) ( evaluate ( makeFloor @@ -113,19 +110,19 @@ test_floorSimplification = assertEqual "floor(top)" ( OrPattern.fromPatterns - [Pattern.top] + [Pattern.topOf testSort] ) ( makeEvaluate - (Pattern.top :: Pattern RewritingVariableName) + testSort + (Pattern.topOf subSort :: Pattern RewritingVariableName) ) -- floor(bottom) = bottom assertEqual "floor(bottom)" - ( OrPattern.fromPatterns - [] - ) + OrPattern.bottom ( makeEvaluate - (Pattern.bottom :: Pattern RewritingVariableName) + testSort + (Pattern.bottomOf subSort :: Pattern RewritingVariableName) ) ) , testCase @@ -136,7 +133,7 @@ test_floorSimplification = "floor(top)" ( OrPattern.fromPatterns [ Conditional - { term = mkTop_ + { term = mkTop testSort , predicate = makeAndPredicate (makeFloorPredicate a) @@ -149,6 +146,7 @@ test_floorSimplification = ] ) ( makeEvaluate + testSort Conditional { term = a , predicate = makeEqualsPredicate fOfA gOfA @@ -211,5 +209,8 @@ evaluate :: OrPattern RewritingVariableName evaluate = simplify . fmap simplifiedOrPattern -makeEvaluate :: Pattern RewritingVariableName -> OrPattern RewritingVariableName -makeEvaluate = makeEvaluateFloor . simplifiedPattern +makeEvaluate :: + Sort -> + Pattern RewritingVariableName -> + OrPattern RewritingVariableName +makeEvaluate sort = makeEvaluateFloor sort . simplifiedPattern diff --git a/kore/test/Test/Kore/Simplify/Forall.hs b/kore/test/Test/Kore/Simplify/Forall.hs index aab2f1cffb..3aa41067a6 100644 --- a/kore/test/Test/Kore/Simplify/Forall.hs +++ b/kore/test/Test/Kore/Simplify/Forall.hs @@ -61,21 +61,17 @@ test_forallSimplification = -- forall(top) = top assertEqual "forall(top)" - ( OrPattern.fromPatterns - [Pattern.top] - ) + (OrPattern.topOf Mock.topSort) ( evaluate ( makeForall Mock.xConfig - [Pattern.top] + [Pattern.topOf Mock.topSort] ) ) -- forall(bottom) = bottom assertEqual "forall(bottom)" - ( OrPattern.fromPatterns - [] - ) + (OrPattern.bottom) ( evaluate ( makeForall Mock.xConfig @@ -89,18 +85,18 @@ test_forallSimplification = -- forall(top) = top assertEqual "forall(top)" - Pattern.top + (Pattern.topOf Mock.topSort) ( makeEvaluate Mock.xConfig - (Pattern.top :: Pattern RewritingVariableName) + (Pattern.topOf Mock.topSort :: Pattern RewritingVariableName) ) -- forall(bottom) = bottom assertEqual "forall(bottom)" - Pattern.bottom + (Pattern.bottomOf Mock.topSort) ( makeEvaluate Mock.xConfig - (Pattern.bottom :: Pattern RewritingVariableName) + (Pattern.bottomOf Mock.topSort :: Pattern RewritingVariableName) ) ) , testCase @@ -115,11 +111,13 @@ test_forallSimplification = ( mkAnd ( mkAnd (Mock.f $ mkElemVar Mock.xConfig) - (mkCeil_ (Mock.h (mkElemVar Mock.xConfig))) + ( (mkCeil Mock.testSort) + (Mock.h (mkElemVar Mock.xConfig)) + ) ) ( mkAnd - (mkEquals_ (mkElemVar Mock.xConfig) gOfA) - (mkEquals_ (mkElemVar Mock.yConfig) fOfA) + (mkEquals Mock.testSort (mkElemVar Mock.xConfig) gOfA) + (mkEquals Mock.testSort (mkElemVar Mock.yConfig) fOfA) ) ) , predicate = makeTruePredicate @@ -165,7 +163,7 @@ test_forallSimplification = ( assertEqual "forall on term" Conditional - { term = mkForall Mock.xConfig (mkAnd fOfX (mkCeil_ gOfA)) + { term = mkForall Mock.xConfig (mkAnd fOfX (mkCeil Mock.testSort gOfA)) , predicate = makeTruePredicate , substitution = mempty } @@ -210,9 +208,9 @@ test_forallSimplification = ( mkAnd ( mkAnd fOfA - (mkCeil_ fOfX) + (mkCeil Mock.testSort fOfX) ) - (mkEquals_ (mkElemVar Mock.yConfig) fOfA) + (mkEquals Mock.testSort (mkElemVar Mock.yConfig) fOfA) ) , predicate = makeTruePredicate , substitution = mempty @@ -236,7 +234,7 @@ test_forallSimplification = ( assertEqual "forall on predicate" Conditional - { term = mkTop_ + { term = mkTop Mock.topSort , predicate = makeForallPredicate Mock.xConfig @@ -249,7 +247,7 @@ test_forallSimplification = ( makeEvaluate Mock.xConfig Conditional - { term = mkTop_ + { term = mkTop Mock.topSort , predicate = makeCeilPredicate fOfX , substitution = Substitution.wrap $ @@ -268,8 +266,8 @@ test_forallSimplification = mkForall Mock.xConfig ( mkAnd - (mkAnd fOfX (mkEquals_ fOfX gOfA)) - (mkEquals_ (mkElemVar Mock.yConfig) hOfA) + (mkAnd fOfX (mkEquals Mock.testSort fOfX gOfA)) + (mkEquals Mock.testSort (mkElemVar Mock.yConfig) hOfA) ) , predicate = makeTruePredicate , substitution = mempty diff --git a/kore/test/Test/Kore/Simplify/Iff.hs b/kore/test/Test/Kore/Simplify/Iff.hs index 735dc20481..a360da64de 100644 --- a/kore/test/Test/Kore/Simplify/Iff.hs +++ b/kore/test/Test/Kore/Simplify/Iff.hs @@ -41,10 +41,10 @@ test_simplify = (testSimplifyBoolean <$> [minBound ..] <*> [minBound ..]) , testGroup "Half-Boolean operations" - [ (top, termA) `becomes` [termA] $ "iff(⊤, a) = a" - , (termA, top) `becomes` [termA] $ "iff(a, ⊤) = a" - , (bottom, termA) `becomes` [termNotA] $ "iff(⊤, a) = ¬a" - , (termA, bottom) `becomes` [termNotA] $ "iff(a, ⊤) = ¬a" + [ (topOf Mock.testSort, termA) `becomes` [termA] $ "iff(⊤, a) = a" + , (termA, topOf Mock.testSort) `becomes` [termA] $ "iff(a, ⊤) = a" + , (bottomOf Mock.testSort, termA) `becomes` [termNotA] $ "iff(⊤, a) = ¬a" + , (termA, bottomOf Mock.testSort) `becomes` [termNotA] $ "iff(a, ⊤) = ¬a" ] ] where @@ -61,20 +61,20 @@ test_makeEvaluate = (testEvaluateBoolean <$> [minBound ..] <*> [minBound ..]) , testGroup "Half-Boolean operations" - [ (top, termA) `becomes` [termA] $ "iff(⊤, a) = a" - , (termA, top) `becomes` [termA] $ "iff(a, ⊤) = a" - , (bottom, termA) `becomes` [termNotA] $ "iff(⊤, a) = ¬a" - , (termA, bottom) `becomes` [termNotA] $ "iff(a, ⊤) = ¬a" + [ (topOf Mock.testSort, termA) `becomes` [termA] $ "iff(⊤, a) = a" + , (termA, topOf Mock.testSort) `becomes` [termA] $ "iff(a, ⊤) = a" + , (bottomOf Mock.testSort, termA) `becomes` [termNotA] $ "iff(⊤, a) = ¬a" + , (termA, bottomOf Mock.testSort) `becomes` [termNotA] $ "iff(a, ⊤) = ¬a" ] , testCase "iff with predicates and substitutions" - -- iff(top and predicate1 and subst1, top and predicate2 and subst2) - -- = top and (iff(predicate1 and subst1, predicate2 and subst2) + -- iff(topOf Mock.testSort and predicate1 and subst1, topOf Mock.testSort and predicate2 and subst2) + -- = topOf Mock.testSort and (iff(predicate1 and subst1, predicate2 and subst2) ( assertEqual - "iff(top and predicate, top and predicate)" + "iff(topOf Mock.testSort and predicate, topOf Mock.testSort and predicate)" ( OrPattern.fromPatterns [ Conditional - { term = mkTop_ + { term = mkTop Mock.testSort , predicate = makeIffPredicate ( makeAndPredicate @@ -97,7 +97,7 @@ test_makeEvaluate = ) ( makeEvaluate Conditional - { term = mkTop_ + { term = mkTop Mock.testSort , predicate = makeCeilPredicate Mock.cf , substitution = Substitution.wrap $ @@ -105,7 +105,7 @@ test_makeEvaluate = [(inject Mock.xConfig, Mock.a)] } Conditional - { term = mkTop_ + { term = mkTop Mock.testSort , predicate = makeCeilPredicate Mock.cg , substitution = Substitution.wrap $ @@ -125,16 +125,16 @@ test_makeEvaluate = ( mkAnd ( mkAnd (Mock.f Mock.a) - (mkCeil_ Mock.cf) + (mkCeil Mock.testSort Mock.cf) ) - (mkEquals_ (mkElemVar Mock.xConfig) Mock.a) + (mkEquals Mock.testSort (mkElemVar Mock.xConfig) Mock.a) ) ( mkAnd ( mkAnd (Mock.g Mock.b) - (mkCeil_ Mock.cg) + (mkCeil Mock.testSort Mock.cg) ) - (mkEquals_ (mkElemVar Mock.yConfig) Mock.b) + (mkEquals Mock.testSort (mkElemVar Mock.yConfig) Mock.b) ) , predicate = makeTruePredicate , substitution = mempty @@ -192,8 +192,8 @@ nameBool x valueBool :: Bool -> Pattern RewritingVariableName valueBool x - | x = Pattern.top - | otherwise = Pattern.bottom + | x = Pattern.topOf Mock.testSort + | otherwise = Pattern.bottomOf Mock.testSort termA :: Pattern RewritingVariableName termA = diff --git a/kore/test/Test/Kore/Simplify/Implies.hs b/kore/test/Test/Kore/Simplify/Implies.hs index ba8b284699..5fd9043de2 100644 --- a/kore/test/Test/Kore/Simplify/Implies.hs +++ b/kore/test/Test/Kore/Simplify/Implies.hs @@ -31,10 +31,10 @@ import Test.Tasty.HUnit test_simplifyEvaluated :: [TestTree] test_simplifyEvaluated = - [ ([Pattern.top], [Pattern.top]) `becomes_` [Pattern.top] - , ([Pattern.top], []) `becomes_` [] - , ([], [Pattern.top]) `becomes_` [Pattern.top] - , ([], []) `becomes_` [Pattern.top] + [ ([Pattern.topOf Mock.testSort], [Pattern.topOf Mock.testSort]) `becomes_` [Pattern.topOf Mock.testSort] + , ([Pattern.topOf Mock.testSort], []) `becomes_` [] + , ([], [Pattern.topOf Mock.testSort]) `becomes_` [Pattern.topOf Mock.testSort] + , ([], []) `becomes_` [Pattern.topOf Mock.testSort] , ([termA], [termB]) `becomes_` [aImpliesB] , ([equalsXA], [equalsXB]) `becomes_` [impliesEqualsXAEqualsXB] , ([equalsXA], [equalsXB, equalsXC]) @@ -131,6 +131,6 @@ simplifyEvaluated :: IO (OrPattern.OrPattern RewritingVariableName) simplifyEvaluated first second = runSimplifier mockEnv $ - Implies.simplifyEvaluated SideCondition.top first second + Implies.simplifyEvaluated Mock.testSort SideCondition.top first second where mockEnv = Mock.env diff --git a/kore/test/Test/Kore/Simplify/Integration.hs b/kore/test/Test/Kore/Simplify/Integration.hs index b206e038ba..dff3771c2b 100644 --- a/kore/test/Test/Kore/Simplify/Integration.hs +++ b/kore/test/Test/Kore/Simplify/Integration.hs @@ -96,9 +96,9 @@ test_simplificationIntegration = ( mkExists Mock.xConfig ( mkAnd - mkTop_ + (mkTop Mock.testSort) ( mkAnd - ( mkCeil_ + ( (mkCeil Mock.testSort) ( mkAnd ( Mock.constr10 ( mkElemVar @@ -108,20 +108,20 @@ test_simplificationIntegration = (Mock.constr10 Mock.a) ) ) - mkTop_ + (mkTop Mock.testSort) ) ) ) - mkBottom_ + (mkBottom Mock.testSort) ) ) - mkTop_ + (mkTop Mock.testSort) , predicate = makeTruePredicate , substitution = mempty } assertEqual "" expect actual , testCase "owise condition - owise case" $ do - let expect = OrPattern.fromPatterns [Pattern.top] + let expect = OrPattern.fromPatterns [Pattern.topOf Mock.testSort] actual <- evaluate Conditional @@ -135,9 +135,9 @@ test_simplificationIntegration = ( mkExists Mock.xConfig ( mkAnd - mkTop_ + (mkTop Mock.testSort) ( mkAnd - ( mkCeil_ + ( (mkCeil Mock.testSort) ( mkAnd ( Mock.constr10 ( mkElemVar @@ -147,14 +147,14 @@ test_simplificationIntegration = (Mock.constr11 Mock.a) ) ) - mkTop_ + (mkTop Mock.testSort) ) ) ) - mkBottom_ + (mkBottom Mock.testSort) ) ) - mkTop_ + (mkTop Mock.testSort) , predicate = makeTruePredicate , substitution = mempty } @@ -163,7 +163,7 @@ test_simplificationIntegration = let expects = OrPattern.fromPatterns [ Conditional - { term = mkTop_ + { term = (mkTop Mock.testSort) , predicate = makeAndPredicate ( makeAndPredicate @@ -190,7 +190,7 @@ test_simplificationIntegration = evaluate Conditional { term = - mkCeil_ + (mkCeil Mock.testSort) ( mkAnd ( Mock.constr20 (Mock.plain10 Mock.cf) @@ -311,7 +311,7 @@ test_simplificationIntegration = } assertEqual "" expect actual , testCase "exists variable equality" $ do - let expect = OrPattern.top + let expect = OrPattern.topOf Mock.testSort actual <- evaluateWithAxioms Map.empty @@ -319,7 +319,7 @@ test_simplificationIntegration = { term = mkExists Mock.xConfig - ( mkEquals_ + ( (mkEquals Mock.testSort) (mkElemVar Mock.xConfig) (mkElemVar Mock.yConfig) ) @@ -328,7 +328,7 @@ test_simplificationIntegration = } assertEqual "" expect actual , testCase "exists variable equality reverse" $ do - let expect = OrPattern.top + let expect = OrPattern.topOf Mock.testSort actual <- evaluateWithAxioms Map.empty @@ -336,7 +336,7 @@ test_simplificationIntegration = { term = mkExists Mock.xConfig - ( mkEquals_ + ( (mkEquals Mock.testSort) (mkElemVar Mock.yConfig) (mkElemVar Mock.xConfig) ) @@ -349,15 +349,15 @@ test_simplificationIntegration = evaluateWithAxioms Map.empty $ Pattern.fromTermLike $ mkExists Mock.xConfig $ - mkEquals_ (mkElemVar Mock.xConfig) (mkElemVar Mock.yConfig) - assertEqual "" OrPattern.top actual + (mkEquals Mock.testSort) (mkElemVar Mock.xConfig) (mkElemVar Mock.yConfig) + assertEqual "" (OrPattern.topOf Mock.testSort) actual , testCase "exists variable equality reverse" $ do actual <- evaluateWithAxioms Map.empty $ Pattern.fromTermLike $ mkExists Mock.xConfig $ - mkEquals_ (mkElemVar Mock.yConfig) (mkElemVar Mock.xConfig) - assertEqual "" OrPattern.top actual + (mkEquals Mock.testSort) (mkElemVar Mock.yConfig) (mkElemVar Mock.xConfig) + assertEqual "" (OrPattern.topOf Mock.testSort) actual , testCase "simplification with top predicate (exists variable capture)" $ do let requirement = \var -> @@ -524,7 +524,7 @@ test_simplificationIntegration = actual <- evaluate Conditional - { term = mkIff Mock.bSort0 mkBottom_ + { term = mkIff Mock.bSort0 (mkBottom Mock.testSort0) , predicate = makeTruePredicate , substitution = mempty } @@ -573,13 +573,13 @@ test_simplificationIntegration = mkIff ( mkIn Mock.boolSort - (mkCeil_ Mock.cf) + ((mkCeil Mock.setSort) Mock.cf) ( mkOr Mock.unitSet - (mkCeil_ Mock.cg) + ((mkCeil Mock.setSort) Mock.cg) ) ) - (mkCeil_ Mock.ch) + ((mkCeil Mock.boolSort) Mock.ch) , predicate = makeTruePredicate , substitution = mempty } @@ -607,13 +607,16 @@ test_simplificationIntegration = mkAnd ( Mock.concatList ( mkImplies - (mkImplies mkBottom_ mkTop_) - (mkIn_ Mock.cfSort0 Mock.cgSort0) + ( mkImplies + (mkBottom Mock.listSort) + (mkTop Mock.listSort) + ) + ((mkIn Mock.listSort) Mock.cfSort0 Mock.cgSort0) ) ( mkImplies ( mkAnd - (mkMu m mkBottom_) - mkBottom_ + (mkMu m (mkBottom Mock.listSort)) + (mkBottom Mock.listSort) ) (mkImplies Mock.unitList (mkNu ue Mock.unitList)) ) @@ -642,12 +645,12 @@ test_simplificationIntegration = { term = mkNu gt - ( mkEquals_ - ( mkIn_ - mkTop_ + ( (mkEquals Mock.stringSort) + ( (mkIn Mock.listSort) + (mkTop Mock.testSort1) (mkNu g (mkOr Mock.aSort1 (mkSetVar g))) ) - mkTop_ + (mkTop Mock.listSort) ) , predicate = makeTruePredicate , substitution = mempty @@ -675,7 +678,7 @@ test_simplificationIntegration = { term = mkMu k - ( mkEquals_ + ( (mkEquals Mock.stringSort) (Mock.functionalConstr21 Mock.cf Mock.cf) (Mock.functionalConstr21 Mock.ch Mock.cg) ) @@ -691,8 +694,10 @@ test_simplificationIntegration = evaluate ( mkNu q - ( mkFloor_ - ( mkIn_ + ( mkFloor + Mock.otherSort + ( mkIn + Mock.otherSort (Mock.g Mock.ch) (mkOr Mock.cf Mock.cg) ) @@ -724,7 +729,7 @@ test_simplificationIntegration = (mkStringLiteral "a") (mkStringLiteral "b") ) - mkBottom_ + (mkBottom Mock.subSort) , predicate = makeTruePredicate , substitution = mempty } diff --git a/kore/test/Test/Kore/Simplify/InternalList.hs b/kore/test/Test/Kore/Simplify/InternalList.hs index 98c1523e04..d9ab0382d4 100644 --- a/kore/test/Test/Kore/Simplify/InternalList.hs +++ b/kore/test/Test/Kore/Simplify/InternalList.hs @@ -67,7 +67,7 @@ test_simplify = ceilb = makeCeilPredicate (Mock.f Mock.b) & Condition.fromPredicate - bottom = OrPattern.fromPatterns [Pattern.bottom] + bottom = OrPattern.fromPatterns [Pattern.bottomOf Mock.listSort] becomes :: HasCallStack => TestName -> @@ -91,5 +91,7 @@ mkList children = , internalListChild = Seq.fromList children } -evaluate :: InternalList (OrPattern RewritingVariableName) -> OrPattern RewritingVariableName +evaluate :: + InternalList (OrPattern RewritingVariableName) -> + OrPattern RewritingVariableName evaluate = simplify diff --git a/kore/test/Test/Kore/Simplify/InternalMap.hs b/kore/test/Test/Kore/Simplify/InternalMap.hs index 1b94fd7210..61a7070d88 100644 --- a/kore/test/Test/Kore/Simplify/InternalMap.hs +++ b/kore/test/Test/Kore/Simplify/InternalMap.hs @@ -99,7 +99,7 @@ test_simplify = ceilb = makeCeilPredicate (Mock.f Mock.b) & Condition.fromPredicate - bottom = OrPattern.fromPatterns [Pattern.bottom] + bottom = OrPattern.fromPatterns [Pattern.bottomOf Mock.topSort] becomes :: HasCallStack => TestName -> diff --git a/kore/test/Test/Kore/Simplify/InternalSet.hs b/kore/test/Test/Kore/Simplify/InternalSet.hs index 7aaafe265a..dc277ac44e 100644 --- a/kore/test/Test/Kore/Simplify/InternalSet.hs +++ b/kore/test/Test/Kore/Simplify/InternalSet.hs @@ -73,7 +73,7 @@ test_simplify = ceila = makeCeilPredicate (Mock.f Mock.a) & Condition.fromPredicate - bottom = OrPattern.fromPatterns [Pattern.bottom] + bottom = OrPattern.fromPatterns [Pattern.bottomOf Mock.topSort] becomes :: HasCallStack => TestName -> diff --git a/kore/test/Test/Kore/Simplify/Not.hs b/kore/test/Test/Kore/Simplify/Not.hs index a978400138..4df3fe52f3 100644 --- a/kore/test/Test/Kore/Simplify/Not.hs +++ b/kore/test/Test/Kore/Simplify/Not.hs @@ -31,12 +31,12 @@ import Test.Tasty.HUnit.Ext test_simplifyEvaluated :: [TestTree] test_simplifyEvaluated = - [ [Pattern.top] `becomes_` [] - , [] `becomes_` [Pattern.top] + [ [Pattern.topOf Mock.testSort] `becomes_` [] + , [] `becomes_` [Pattern.topOf Mock.testSort] , [termX] `becomes_` [termNotX] , [termNotX] `becomes_` [termX] , [equalsXA] `becomes_` [notEqualsXA] - , equalsXAWithSortedBottom `patternBecomes` [Pattern.top] + , equalsXAWithSortedBottom `patternBecomes` [Pattern.topOf Mock.testSort] , [substXA] `becomes_` [notEqualsXA] , [equalsXA, equalsXB] `becomes_` [neitherXAB] , [xAndEqualsXA] `becomes_` [termNotX, notEqualsXASorted] @@ -154,14 +154,14 @@ substXA = fromSubstitution $ Substitution.unsafeWrap [(inject Mock.xConfig, Mock forceTermSort :: Pattern.Pattern RewritingVariableName -> Pattern.Pattern RewritingVariableName -forceTermSort = fmap (forceSort Mock.testSort) +forceTermSort = fmap (sameTermLikeSort Mock.testSort) fromPredicate :: Predicate.Predicate RewritingVariableName -> Pattern.Pattern RewritingVariableName fromPredicate = forceTermSort - . Pattern.fromCondition_ + . Pattern.fromCondition Mock.testSort . Condition.fromPredicate fromSubstitution :: @@ -169,13 +169,15 @@ fromSubstitution :: Pattern.Pattern RewritingVariableName fromSubstitution = forceTermSort - . Pattern.fromCondition_ + . Pattern.fromCondition Mock.testSort . Condition.fromSubstitution simplifyEvaluated :: OrPattern.OrPattern RewritingVariableName -> IO (OrPattern.OrPattern RewritingVariableName) simplifyEvaluated = - runSimplifier mockEnv . Not.simplifyEvaluated SideCondition.top + runSimplifier mockEnv . mkNotSimplified where mockEnv = Mock.env + mkNotSimplified notChild = + Not.simplify SideCondition.top Not{notSort = Mock.testSort, notChild} diff --git a/kore/test/Test/Kore/Simplify/Or.hs b/kore/test/Test/Kore/Simplify/Or.hs index db2535e566..77315526a6 100644 --- a/kore/test/Test/Kore/Simplify/Or.hs +++ b/kore/test/Test/Kore/Simplify/Or.hs @@ -9,6 +9,7 @@ import qualified Data.List as List import Data.Text ( Text, ) +import Kore.Internal.OrPattern (getSortIfNotBottom) import Kore.Internal.Predicate ( Predicate, makeEqualsPredicate, @@ -223,9 +224,11 @@ becomes ( stateIntention [ prettyOr or1 or2 , "to become:" - , Unparser.unparse $ OrPattern.toTermLike expected + , Unparser.unparse $ OrPattern.toTermLike termSort expected ] ) + where + termSort = fromMaybe (mkSortVariable "_") (getSortIfNotBottom expected) simplifiesTo :: HasCallStack => diff --git a/kore/test/Test/Kore/Simplify/OrPattern.hs b/kore/test/Test/Kore/Simplify/OrPattern.hs index 3261e75d5c..2af60c3ccc 100644 --- a/kore/test/Test/Kore/Simplify/OrPattern.hs +++ b/kore/test/Test/Kore/Simplify/OrPattern.hs @@ -12,7 +12,7 @@ import Kore.Internal.OrPattern ( import qualified Kore.Internal.OrPattern as OrPattern ( bottom, fromPatterns, - top, + topOf, ) import Kore.Internal.Predicate ( Predicate, @@ -38,8 +38,8 @@ import Test.Tasty.HUnit.Ext test_orPatternSimplification :: [TestTree] test_orPatternSimplification = [ testCase "Identity for top" $ do - actual <- runSimplifyPredicates makeTruePredicate OrPattern.top - assertEqual "" OrPattern.top actual + actual <- runSimplifyPredicates makeTruePredicate (OrPattern.topOf Mock.topSort) + assertEqual "" (OrPattern.topOf Mock.topSort) actual , testCase "Identity for bottom" $ do actual <- runSimplifyPredicates makeTruePredicate OrPattern.bottom assertEqual "" OrPattern.bottom actual diff --git a/kore/test/Test/Kore/Simplify/Pattern.hs b/kore/test/Test/Kore/Simplify/Pattern.hs index f309fc006f..a181db38cc 100644 --- a/kore/test/Test/Kore/Simplify/Pattern.hs +++ b/kore/test/Test/Kore/Simplify/Pattern.hs @@ -384,7 +384,7 @@ test_Pattern_simplify_equalityterm = -- ] first = Mock.cf second = - (OrPattern.toTermLike . OrPattern.fromPatterns) + (OrPattern.toTermLike Mock.testSort . OrPattern.fromPatterns) [ (Pattern.withCondition Mock.cg) (Condition.assign (inject Mock.xConfig) Mock.a) , Pattern.fromTermLike Mock.ch @@ -433,7 +433,7 @@ termLike = Pattern.fromTermLike -- | Term is \bottom, but not in a trivial way. notTop, orAs, bottomLike :: Pattern RewritingVariableName -notTop = termLike (mkNot mkTop_) +notTop = termLike (mkNot $ mkTop Mock.testSort) -- | Lifting disjunction to the top would duplicate terms. orAs = termLike (mkOr Mock.a Mock.a) diff --git a/kore/test/Test/Kore/Simplify/TermLike.hs b/kore/test/Test/Kore/Simplify/TermLike.hs index 77b603b27d..80a7f70e72 100644 --- a/kore/test/Test/Kore/Simplify/TermLike.hs +++ b/kore/test/Test/Kore/Simplify/TermLike.hs @@ -132,7 +132,7 @@ instance MonadSimplify TestSimplifier where test_simplifyOnly :: [TestTree] test_simplifyOnly = [ (test "LIST.List \\and simplification failure") - (mkAnd (Mock.concatList mkTop_ mkTop_) (Mock.builtinList [])) + (mkAnd (Mock.concatList (mkTop Mock.listSort) (mkTop Mock.listSort)) (Mock.builtinList [])) expectUnsimplified , (test "Non-function symbol without evaluators") Mock.plain00Subsort diff --git a/kore/test/Test/Kore/Simplify/Top.hs b/kore/test/Test/Kore/Simplify/Top.hs index dea6a41660..10425761a0 100644 --- a/kore/test/Test/Kore/Simplify/Top.hs +++ b/kore/test/Test/Kore/Simplify/Top.hs @@ -27,7 +27,7 @@ test_topSimplification = "Top evaluates to top" ( assertEqual "" - (OrPattern.fromPattern Pattern.top) + (OrPattern.fromPattern (Pattern.topOf testSort)) (evaluate Top{topSort = testSort}) ) ] diff --git a/kore/test/Test/Kore/Unification/Unifier.hs b/kore/test/Test/Kore/Unification/Unifier.hs index c6b3b301ef..5c2aa6dc60 100644 --- a/kore/test/Test/Kore/Unification/Unifier.hs +++ b/kore/test/Test/Kore/Unification/Unifier.hs @@ -815,7 +815,7 @@ simplifyPattern (UnificationTerm term) = do simplifiedPatterns <- Pattern.simplify expandedPattern case toList simplifiedPatterns of - [] -> return Pattern.bottom + [] -> return (Pattern.bottomOf Mock.testSort) (config : _) -> return config expandedPattern = Pattern.fromTermLike term diff --git a/kore/test/Test/Kore/Validate/DefinitionVerifier/Imports.hs b/kore/test/Test/Kore/Validate/DefinitionVerifier/Imports.hs index d191680058..f4d4466e42 100644 --- a/kore/test/Test/Kore/Validate/DefinitionVerifier/Imports.hs +++ b/kore/test/Test/Kore/Validate/DefinitionVerifier/Imports.hs @@ -405,7 +405,7 @@ sortVisibilityTests = SentenceAxiom { sentenceAxiomParameters = [] , sentenceAxiomPattern = - externalize $ mkAnd (mkTop sort) mkTop_ + externalize $ mkAnd (mkTop sort) (mkTop sort) , sentenceAxiomAttributes = Attributes [] } sortReferenceInNextPatternSentence = @@ -678,7 +678,8 @@ symbolVisibilityTests = SentenceAxiom { sentenceAxiomParameters = [] , sentenceAxiomPattern = - externalize $ mkAnd symbolPattern mkTop_ + mkAnd symbolPattern (mkTop $ termLikeSort symbolPattern) + & externalize , sentenceAxiomAttributes = Attributes [] } symbolReferenceInExistsPatternSentence = @@ -901,7 +902,8 @@ aliasVisibilityTests = SentenceAxiom { sentenceAxiomParameters = [] , sentenceAxiomPattern = - externalize $ mkAnd aliasPattern mkTop_ + mkAnd aliasPattern (mkTop $ termLikeSort aliasPattern) + & externalize , sentenceAxiomAttributes = Attributes [] } aliasReferenceInExistsPatternSentence =