diff --git a/kore/src/Kore/Builtin/AssociativeCommutative.hs b/kore/src/Kore/Builtin/AssociativeCommutative.hs index b086765a5b..1b188086a2 100644 --- a/kore/src/Kore/Builtin/AssociativeCommutative.hs +++ b/kore/src/Kore/Builtin/AssociativeCommutative.hs @@ -1076,7 +1076,8 @@ unifyEqualsNormalizedAc TermLike RewritingVariableName -> unifier (Pattern RewritingVariableName) simplify term = - lowerLogicT $ simplifyConditionalTerm SideCondition.topTODO term + simplifyPatternScatter SideCondition.topTODO (Pattern.fromTermLike term) + & lowerLogicT simplifyPair :: ( TermLike RewritingVariableName @@ -1119,11 +1120,13 @@ unifyEqualsNormalizedAc `andCondition` simplifiedValueCondition ) where + -- TODO: can this be rewritten? simplifyTermLike' :: TermLike RewritingVariableName -> unifier (Pattern RewritingVariableName) simplifyTermLike' term = - lowerLogicT $ simplifyConditionalTerm SideCondition.topTODO term + simplifyPatternScatter SideCondition.topTODO (Pattern.fromTermLike term) + & lowerLogicT buildResultFromUnifiers :: forall normalized unifier variable. diff --git a/kore/src/Kore/Internal/OrPattern.hs b/kore/src/Kore/Internal/OrPattern.hs index 74c5ba9c3b..201cc805ad 100644 --- a/kore/src/Kore/Internal/OrPattern.hs +++ b/kore/src/Kore/Internal/OrPattern.hs @@ -5,6 +5,7 @@ License : BSD-3-Clause module Kore.Internal.OrPattern ( OrPattern, coerceSort, + markSimplified, isSimplified, hasSimplifiedChildren, hasSimplifiedChildrenIgnoreConditions, @@ -81,6 +82,12 @@ import Prelude.Kore -- | The disjunction of 'Pattern'. type OrPattern variable = MultiOr (Pattern variable) +markSimplified :: + InternalVariable variable => + OrPattern variable -> + OrPattern variable +markSimplified = MultiOr.map Pattern.markSimplified + isSimplified :: SideCondition.Representation -> OrPattern variable -> Bool isSimplified sideCondition = all (Pattern.isSimplified sideCondition) diff --git a/kore/src/Kore/Internal/SideCondition.hs b/kore/src/Kore/Internal/SideCondition.hs index b82fff109f..b96b4b0263 100644 --- a/kore/src/Kore/Internal/SideCondition.hs +++ b/kore/src/Kore/Internal/SideCondition.hs @@ -281,6 +281,23 @@ addAssumptions predicates sideCondition = predicates <> assumedTrue sideCondition } +areIncludedIn :: + Eq variable => + Foldable f => + f (Predicate variable) -> + SideCondition variable -> + Bool +areIncludedIn predicates sideCondition = + all (flip isIncludedIn sideCondition) predicates + +isIncludedIn :: + Eq variable => + Predicate variable -> + SideCondition variable -> + Bool +isIncludedIn predicate SideCondition{assumedTrue} = + predicate `elem` assumedTrue + {- | Assumes a 'Condition' to be true in the context of another 'SideCondition' and recalculates the term replacements table from the combined predicate. @@ -292,19 +309,22 @@ addConditionWithReplacements :: SideCondition variable addConditionWithReplacements (from @(Condition _) @(MultiAnd _) -> newCondition) - sideCondition = - let combinedConditions = oldCondition <> newCondition - (assumedTrue, assumptions) = - simplifyConjunctionByAssumption combinedConditions - & extract - Assumptions replacementsTermLike replacementsPredicate = assumptions - in SideCondition - { assumedTrue - , replacementsTermLike - , replacementsPredicate - , definedTerms - , simplifiedFunctions - } + sideCondition + | newCondition `areIncludedIn` sideCondition = + sideCondition + | otherwise = + let combinedConditions = oldCondition <> newCondition + (assumedTrue, assumptions) = + simplifyConjunctionByAssumption combinedConditions + & extract + Assumptions replacementsTermLike replacementsPredicate = assumptions + in SideCondition + { assumedTrue + , replacementsTermLike + , replacementsPredicate + , definedTerms + , simplifiedFunctions + } where SideCondition { assumedTrue = oldCondition diff --git a/kore/src/Kore/Rewrite/Function/Evaluator.hs b/kore/src/Kore/Rewrite/Function/Evaluator.hs index a5d73ae8cb..e70acb0c43 100644 --- a/kore/src/Kore/Rewrite/Function/Evaluator.hs +++ b/kore/src/Kore/Rewrite/Function/Evaluator.hs @@ -271,7 +271,7 @@ maybeEvaluatePattern | toSimplify == unchangedPatt = return (OrPattern.fromPattern unchangedPatt) | otherwise = - reevaluateFunctions sideCondition toSimplify + simplifyPattern sideCondition toSimplify evaluateSortInjection :: InternalVariable variable => @@ -323,22 +323,6 @@ sortInjectionSorts symbol = , "should have two sort parameters." ] -{- | 'reevaluateFunctions' re-evaluates functions after a user-defined function -was evaluated. --} -reevaluateFunctions :: - MonadSimplify simplifier => - SideCondition RewritingVariableName -> - -- | Function evaluation result. - Pattern RewritingVariableName -> - simplifier (OrPattern RewritingVariableName) -reevaluateFunctions sideCondition rewriting = do - let (rewritingTerm, rewritingCondition) = Pattern.splitTerm rewriting - OrPattern.observeAllT $ do - simplifiedTerm <- simplifyConditionalTerm sideCondition rewritingTerm - simplifyCondition sideCondition $ - Pattern.andCondition simplifiedTerm rewritingCondition - -- | Ands the given condition-substitution to the given function evaluation. mergeWithConditionAndSubstitution :: MonadSimplify simplifier => diff --git a/kore/src/Kore/Simplify/Data.hs b/kore/src/Kore/Simplify/Data.hs index 70d0c26b9a..e1ce002719 100644 --- a/kore/src/Kore/Simplify/Data.hs +++ b/kore/src/Kore/Simplify/Data.hs @@ -48,9 +48,8 @@ import Kore.IndexedModule.MetadataTools ( import qualified Kore.IndexedModule.MetadataToolsBuilder as MetadataTools import qualified Kore.IndexedModule.OverloadGraph as OverloadGraph import qualified Kore.IndexedModule.SortGraph as SortGraph -import Kore.Internal.TermLike ( - TermLike, - ) +import Kore.Internal.Pattern (Pattern) +import qualified Kore.Internal.Pattern as Pattern import qualified Kore.Rewrite.Axiom.EvaluationStrategy as Axiom.EvaluationStrategy import Kore.Rewrite.Axiom.Identifier ( matchAxiomIdentifier, @@ -66,6 +65,7 @@ import Kore.Rewrite.RewritingVariable ( import qualified Kore.Simplify.Condition as Condition import Kore.Simplify.InjSimplifier import Kore.Simplify.OverloadSimplifier +import qualified Kore.Simplify.Pattern as Pattern import Kore.Simplify.Simplify import qualified Kore.Simplify.SubstitutionSimplifier as SubstitutionSimplifier import qualified Kore.Simplify.TermLike as TermLike @@ -117,10 +117,10 @@ instance (MonadMask prof, MonadProf prof) => MonadProf (SimplifierT prof) where traceProfSimplify :: MonadProf prof => - TermLike RewritingVariableName -> + Pattern RewritingVariableName -> prof a -> prof a -traceProfSimplify termLike = +traceProfSimplify (Pattern.toTermLike -> termLike) = maybe id traceProf ident where ident = @@ -137,14 +137,12 @@ instance askMetadataTools = asks metadataTools {-# INLINE askMetadataTools #-} - simplifyTermLike sideCondition termLike = - traceProfSimplify termLike (TermLike.simplify sideCondition termLike) - {-# INLINE simplifyTermLike #-} + simplifyPattern sideCondition patt = + traceProfSimplify patt (Pattern.makeEvaluate sideCondition patt) + {-# INLINE simplifyPattern #-} - simplifyTermLikeOnly sideCondition termLike = - (traceProfSimplify termLike) - (TermLike.simplifyOnly sideCondition termLike) - {-# INLINE simplifyTermLikeOnly #-} + simplifyTerm = TermLike.simplify + {-# INLINE simplifyTerm #-} simplifyCondition topCondition conditional = do ConditionSimplifier simplify <- asks simplifierCondition diff --git a/kore/src/Kore/Simplify/Exists.hs b/kore/src/Kore/Simplify/Exists.hs index fd62d00bbd..a73af44d0c 100644 --- a/kore/src/Kore/Simplify/Exists.hs +++ b/kore/src/Kore/Simplify/Exists.hs @@ -70,9 +70,6 @@ import Kore.Rewrite.RewritingVariable ( import qualified Kore.Simplify.AndPredicates as And ( simplifyEvaluatedMultiPredicate, ) -import qualified Kore.Simplify.Pattern as Pattern ( - makeEvaluate, - ) import Kore.Simplify.Simplify import Kore.Substitute import qualified Kore.TopBottom as TopBottom @@ -308,7 +305,8 @@ makeEvaluateBoundLeft sideCondition variable boundTerm normalized = Conditional.predicate normalized } orPattern <- - lift $ Pattern.makeEvaluate sideCondition substituted + simplifyPattern sideCondition substituted + & lift Logic.scatter (toList orPattern) where someVariableName = inject (variableName variable) diff --git a/kore/src/Kore/Simplify/Pattern.hs b/kore/src/Kore/Simplify/Pattern.hs index 92a711e42b..b4467ed821 100644 --- a/kore/src/Kore/Simplify/Pattern.hs +++ b/kore/src/Kore/Simplify/Pattern.hs @@ -46,9 +46,10 @@ import Kore.Rewrite.RewritingVariable ( import Kore.Simplify.Simplify ( MonadSimplify, simplifyCondition, - simplifyConditionalTerm, + simplifyTerm, ) import Kore.Substitute +import qualified Logic import Prelude.Kore -- | Simplifies the 'Pattern' and removes the exists quantifiers at the top. @@ -110,21 +111,35 @@ This should only be used when it's certain that the the 'Pattern'. -} makeEvaluate :: + forall simplifier. MonadSimplify simplifier => SideCondition RewritingVariableName -> Pattern RewritingVariableName -> simplifier (OrPattern RewritingVariableName) -makeEvaluate sideCondition pattern' = - OrPattern.observeAllT $ do - withSimplifiedCondition <- simplifyCondition sideCondition pattern' - let (term, simplifiedCondition) = - Conditional.splitTerm withSimplifiedCondition - term' = substitute (toMap $ substitution simplifiedCondition) term - termSideCondition = - SideCondition.addConditionWithReplacements - simplifiedCondition - sideCondition - simplifiedTerm <- simplifyConditionalTerm termSideCondition term' - let simplifiedPattern = - Conditional.andCondition simplifiedTerm simplifiedCondition - simplifyCondition sideCondition simplifiedPattern +makeEvaluate sideCondition = + loop . OrPattern.fromPattern + where + loop input = do + output <- + OrPattern.traverse worker input + & fmap OrPattern.flatten + if input == output + then pure output + else loop output + + worker pattern' = + OrPattern.observeAllT $ do + withSimplifiedCondition <- simplifyCondition sideCondition pattern' + let (term, simplifiedCondition) = + Conditional.splitTerm withSimplifiedCondition + term' = substitute (toMap $ substitution simplifiedCondition) term + termSideCondition = + SideCondition.addConditionWithReplacements + simplifiedCondition + sideCondition + simplifiedTerm <- + simplifyTerm termSideCondition term' + >>= Logic.scatter + let simplifiedPattern = + Conditional.andCondition simplifiedTerm simplifiedCondition + simplifyCondition sideCondition simplifiedPattern diff --git a/kore/src/Kore/Simplify/Predicate.hs b/kore/src/Kore/Simplify/Predicate.hs index 4981f9edfa..e6a75ae5a8 100644 --- a/kore/src/Kore/Simplify/Predicate.hs +++ b/kore/src/Kore/Simplify/Predicate.hs @@ -133,14 +133,14 @@ simplify sideCondition original = replacePredicate = SideCondition.replacePredicate sideCondition -- If the child 'TermLike' is a term representing a predicate, - -- 'simplifyTermLikeOnly' will not attempt to simplify it, so + -- 'simplifyTerm' will not attempt to simplify it, so -- it should be transformed into a 'Predicate' and simplified -- accordingly. - simplifyTerm term + simplifyTerm' term | Right predicate <- Predicate.makePredicate term = toOrPattern (termLikeSort term) <$> worker predicate | otherwise = - simplifyTermLikeOnly sideCondition term + simplifyTerm sideCondition term repr = SideCondition.toRepresentation sideCondition @@ -167,10 +167,10 @@ simplify sideCondition original = ImpliesF impliesF -> simplifyImplies =<< traverse worker impliesF IffF iffF -> simplifyIff =<< traverse worker iffF CeilF ceilF -> - simplifyCeil sideCondition =<< traverse simplifyTerm ceilF + simplifyCeil sideCondition =<< traverse simplifyTerm' ceilF FloorF floorF@(Floor _ _ child) -> simplifyFloor (termLikeSort child) sideCondition - =<< traverse simplifyTerm floorF + =<< traverse simplifyTerm' floorF ExistsF existsF -> traverse worker (Exists.refreshExists avoid existsF) >>= simplifyExists sideCondition @@ -179,9 +179,9 @@ simplify sideCondition original = >>= simplifyForall sideCondition EqualsF equalsF@(Equals _ _ term _) -> simplifyEquals sideCondition (termLikeSort term) - =<< traverse simplifyTerm equalsF + =<< traverse simplifyTerm' equalsF InF inF -> - simplifyIn sideCondition =<< traverse simplifyTerm inF + simplifyIn sideCondition =<< traverse simplifyTerm' inF where _ :< predicateF = Recursive.project predicate ~avoid = freeVariableNames sideCondition diff --git a/kore/src/Kore/Simplify/Rule.hs b/kore/src/Kore/Simplify/Rule.hs index 7ad7c2736f..6db9a9855a 100644 --- a/kore/src/Kore/Simplify/Rule.hs +++ b/kore/src/Kore/Simplify/Rule.hs @@ -20,6 +20,7 @@ import Kore.Internal.Predicate ( pattern PredicateTrue, ) import qualified Kore.Internal.Predicate as Predicate +import qualified Kore.Internal.SideCondition as SideCondition import qualified Kore.Internal.Substitution as Substitution import Kore.Internal.TermLike ( TermLike, @@ -34,7 +35,6 @@ import Kore.Rewrite.RewritingVariable ( RewritingVariableName, ) import Kore.Rewrite.RulePattern -import qualified Kore.Simplify.Pattern as Pattern import Kore.Simplify.Simplify ( MonadSimplify, ) @@ -64,7 +64,7 @@ simplifyRulePattern :: simplifier (RulePattern RewritingVariableName) simplifyRulePattern rule = do let RulePattern{left} = rule - simplifiedLeft <- simplifyPattern left + simplifiedLeft <- simplifyPattern' left case OrPattern.toPatterns simplifiedLeft of [Conditional{term, predicate, substitution}] | PredicateTrue <- predicate -> do @@ -109,7 +109,7 @@ simplifyClaimPattern :: simplifier ClaimPattern simplifyClaimPattern claim = do let ClaimPattern{left} = claim - simplifiedLeft <- simplifyPattern (Pattern.term left) + simplifiedLeft <- simplifyPattern' (Pattern.term left) case OrPattern.toPatterns simplifiedLeft of [Conditional{term, predicate, substitution}] | PredicateTrue <- predicate -> @@ -132,10 +132,12 @@ simplifyClaimPattern claim = do return claim -- | Simplify a 'TermLike' using only matching logic rules. -simplifyPattern :: +simplifyPattern' :: MonadSimplify simplifier => TermLike RewritingVariableName -> simplifier (OrPattern RewritingVariableName) -simplifyPattern termLike = +simplifyPattern' termLike = Simplifier.localSimplifierAxioms (const mempty) $ - Pattern.simplify (Pattern.fromTermLike termLike) + Simplifier.simplifyPattern + SideCondition.top + (Pattern.fromTermLike termLike) diff --git a/kore/src/Kore/Simplify/Simplify.hs b/kore/src/Kore/Simplify/Simplify.hs index 263e6520d1..1fe4a773d4 100644 --- a/kore/src/Kore/Simplify/Simplify.hs +++ b/kore/src/Kore/Simplify/Simplify.hs @@ -5,7 +5,7 @@ License : BSD-3-Clause module Kore.Simplify.Simplify ( InternalVariable, MonadSimplify (..), - simplifyConditionalTerm, + simplifyPatternScatter, TermSimplifier, -- * Condition simplifiers @@ -145,33 +145,29 @@ class (MonadLog m, MonadSMT m) => MonadSimplify m where askMetadataTools = lift askMetadataTools {-# INLINE askMetadataTools #-} - -- | Simplify a 'TermLike' to a disjunction of function-like 'Pattern's. - simplifyTermLike :: + simplifyPattern :: SideCondition RewritingVariableName -> - TermLike RewritingVariableName -> + Pattern RewritingVariableName -> m (OrPattern RewritingVariableName) - default simplifyTermLike :: + default simplifyPattern :: (MonadTrans t, MonadSimplify n, m ~ t n) => SideCondition RewritingVariableName -> - TermLike RewritingVariableName -> + Pattern RewritingVariableName -> m (OrPattern RewritingVariableName) - simplifyTermLike sideCondition termLike = - lift (simplifyTermLike sideCondition termLike) + simplifyPattern sideCondition termLike = + lift (simplifyPattern sideCondition termLike) - -- | Simplify a 'TermLike' to a disjunction of 'Pattern'. - -- - -- Unlike 'simplifyTermLike', this method does not simplify the condition. - simplifyTermLikeOnly :: + simplifyTerm :: SideCondition RewritingVariableName -> TermLike RewritingVariableName -> m (OrPattern RewritingVariableName) - default simplifyTermLikeOnly :: + default simplifyTerm :: (MonadTrans t, MonadSimplify n, m ~ t n) => SideCondition RewritingVariableName -> TermLike RewritingVariableName -> m (OrPattern RewritingVariableName) - simplifyTermLikeOnly sideCondition termLike = - lift (simplifyTermLikeOnly sideCondition termLike) + simplifyTerm sideCondition termLike = + lift (simplifyTerm sideCondition termLike) simplifyCondition :: SideCondition RewritingVariableName -> @@ -266,16 +262,14 @@ instance MonadSimplify m => MonadSimplify (RWST r () s m) -- TODO (thomas.tuegel): Factor out these types. --- | Simplify a pattern subject to conditions. -simplifyConditionalTerm :: +simplifyPatternScatter :: forall simplifier. (MonadLogic simplifier, MonadSimplify simplifier) => SideCondition RewritingVariableName -> - TermLike RewritingVariableName -> + Pattern RewritingVariableName -> simplifier (Pattern RewritingVariableName) -simplifyConditionalTerm sideCondition termLike = - simplifyTermLike sideCondition termLike >>= Logic.scatter - +simplifyPatternScatter sideCondition patt = + simplifyPattern sideCondition patt >>= Logic.scatter -- * Predicate simplifiers {- | 'ConditionSimplifier' wraps a function that simplifies diff --git a/kore/src/Kore/Simplify/SubstitutionSimplifier.hs b/kore/src/Kore/Simplify/SubstitutionSimplifier.hs index 42966a2c40..39821a660d 100644 --- a/kore/src/Kore/Simplify/SubstitutionSimplifier.hs +++ b/kore/src/Kore/Simplify/SubstitutionSimplifier.hs @@ -85,8 +85,8 @@ import Kore.Rewrite.RewritingVariable ( ) import Kore.Simplify.Simplify ( MonadSimplify, - simplifyConditionalTerm, - simplifyTermLike, + simplifyPattern, + simplifyPatternScatter, ) import qualified Kore.TopBottom as TopBottom import Kore.Unification.SubstitutionNormalization ( @@ -153,7 +153,8 @@ simplificationMakeAnd = makeAnd termLike1 termLike2 sideCondition = do simplified <- mkAnd termLike1 termLike2 - & simplifyConditionalTerm sideCondition + & Pattern.fromTermLike + & simplifyPatternScatter sideCondition TopBottom.guardAgainstBottom simplified return simplified @@ -353,7 +354,7 @@ simplifySubstitutionWorker sideCondition makeAnd' = \substitution -> do SomeVariableNameElement _ | isSimplified -> return subst | otherwise -> do - termLike' <- simplifyTermLike' termLike + termLike' <- simplifyTermLike termLike return $ Substitution.assign uVar termLike' where isSimplified = @@ -361,14 +362,14 @@ simplifySubstitutionWorker sideCondition makeAnd' = \substitution -> do sideConditionRepresentation termLike - simplifyTermLike' :: + simplifyTermLike :: TermLike RewritingVariableName -> Impl RewritingVariableName simplifier (TermLike RewritingVariableName) - simplifyTermLike' termLike = do - orPattern <- simplifyTermLike sideCondition termLike + simplifyTermLike termLike = do + orPattern <- simplifyPattern sideCondition (Pattern.fromTermLike termLike) case OrPattern.toPatterns orPattern of [] -> do addCondition Condition.bottom diff --git a/kore/src/Kore/Simplify/TermLike.hs b/kore/src/Kore/Simplify/TermLike.hs index caef76d68c..657aaceae3 100644 --- a/kore/src/Kore/Simplify/TermLike.hs +++ b/kore/src/Kore/Simplify/TermLike.hs @@ -4,7 +4,6 @@ License : BSD-3-Clause -} module Kore.Simplify.TermLike ( simplify, - simplifyOnly, ) where import qualified Control.Lens.Combinators as Lens @@ -17,13 +16,6 @@ import Kore.Attribute.Pattern.FreeVariables ( freeVariableNames, freeVariables, ) -import Kore.Internal.Condition ( - Condition, - ) -import qualified Kore.Internal.Condition as Condition -import Kore.Internal.Conditional ( - Conditional (Conditional), - ) import qualified Kore.Internal.Conditional as Conditional import Kore.Internal.From import qualified Kore.Internal.MultiAnd as MultiAnd @@ -32,21 +24,11 @@ import Kore.Internal.OrPattern ( OrPattern, ) import qualified Kore.Internal.OrPattern as OrPattern -import Kore.Internal.Pattern ( - Pattern, - ) import qualified Kore.Internal.Pattern as Pattern -import qualified Kore.Internal.Predicate as Predicate import Kore.Internal.SideCondition ( SideCondition, ) import qualified Kore.Internal.SideCondition as SideCondition -import qualified Kore.Internal.SideCondition.SideCondition as SideCondition ( - Representation, - ) -import qualified Kore.Internal.Substitution as Substitution ( - toMap, - ) import Kore.Internal.TermLike ( TermLike, TermLikeF (..), @@ -62,24 +44,12 @@ import qualified Kore.Simplify.And as And ( import qualified Kore.Simplify.Application as Application ( simplify, ) -import qualified Kore.Simplify.Bottom as Bottom ( - simplify, - ) -import qualified Kore.Simplify.Ceil as Ceil ( - simplify, - ) import qualified Kore.Simplify.DomainValue as DomainValue ( simplify, ) -import qualified Kore.Simplify.Equals as Equals ( - simplify, - ) import qualified Kore.Simplify.Exists as Exists ( simplify, ) -import qualified Kore.Simplify.Floor as Floor ( - simplify, - ) import qualified Kore.Simplify.Forall as Forall ( simplify, ) @@ -89,9 +59,6 @@ import qualified Kore.Simplify.Iff as Iff ( import qualified Kore.Simplify.Implies as Implies ( simplify, ) -import qualified Kore.Simplify.In as In ( - simplify, - ) import qualified Kore.Simplify.Inhabitant as Inhabitant ( simplify, ) @@ -139,13 +106,9 @@ import Kore.Simplify.Simplify import qualified Kore.Simplify.StringLiteral as StringLiteral ( simplify, ) -import qualified Kore.Simplify.Top as Top ( - simplify, - ) import qualified Kore.Simplify.Variable as Variable ( simplify, ) -import Kore.Substitute import Kore.Syntax ( Ceil (..), Equals (..), @@ -154,357 +117,21 @@ import Kore.Syntax ( refreshExists, refreshForall, ) -import Kore.TopBottom ( - TopBottom (..), - ) -import Kore.Unparser ( - unparse, - ) import qualified Kore.Variables.Binding as Binding -import qualified Logic import Prelude.Kore -import Pretty ( - Pretty (..), - ) -import qualified Pretty -- TODO(virgil): Add a Simplifiable class and make all pattern types -- instances of that. -{- | Simplify 'TermLike' pattern to a disjunction of function-like 'Pattern's. - All the resulting terms and conditions will be fully simplified, because after - the term simplification procedure, the condition simplifier will be called as well. --} -simplify :: - forall simplifier. - HasCallStack => - MonadSimplify simplifier => - MonadThrow simplifier => - SideCondition RewritingVariableName -> - TermLike RewritingVariableName -> - simplifier (OrPattern RewritingVariableName) -simplify sideCondition = \termLike -> - simplifyInternalWorker termLike - >>= ensureSimplifiedResult sideConditionRepresentation termLike - where - sideConditionRepresentation = SideCondition.toRepresentation sideCondition - - simplifyChildren :: - Traversable t => - t (TermLike RewritingVariableName) -> - simplifier (t (OrPattern RewritingVariableName)) - simplifyChildren = traverse (simplifyTermLike sideCondition) - - simplifyInternalWorker :: - TermLike RewritingVariableName -> - simplifier (OrPattern RewritingVariableName) - simplifyInternalWorker termLike - | Just termLike' <- continueSimplificationWith termLike = - assertTermNotPredicate $ do - unfixedTermOr <- descendAndSimplify termLike' - let termOr = - OrPattern.coerceSort - (termLikeSort termLike') - unfixedTermOr - returnIfSimplifiedOrContinue - termLike' - (OrPattern.toPatterns termOr) - ( do - termPredicateList <- Logic.observeAllT $ do - termOrElement <- Logic.scatter termOr - simplified <- - simplifyCondition sideCondition termOrElement - return (applyTermSubstitution simplified) - - returnIfSimplifiedOrContinue - termLike' - termPredicateList - ( do - resultsList <- mapM resimplify termPredicateList - return (MultiOr.mergeAll resultsList) - ) - ) - | otherwise = - case Predicate.makePredicate termLike of - Left _ -> return . OrPattern.fromTermLike $ termLike - Right predicate -> do - condition <- - Condition.fromPredicate predicate - & ensureSimplifiedCondition - sideConditionRepresentation - termLike - condition - & Pattern.fromCondition (termLikeSort termLike) - & OrPattern.fromPattern - & pure - where - continueSimplificationWith :: - TermLike RewritingVariableName -> - Maybe (TermLike RewritingVariableName) - continueSimplificationWith original = - let isOriginalNotSimplified - | TermLike.isSimplified sideConditionRepresentation original = - Nothing - | otherwise = Just original - in SideCondition.replaceTerm sideCondition original - <|> isOriginalNotSimplified - - resimplify :: - Pattern RewritingVariableName -> - simplifier (OrPattern RewritingVariableName) - resimplify result = do - let (resultTerm, resultPredicate) = Pattern.splitTerm result - simplified <- simplifyInternalWorker resultTerm - return - ( MultiOr.map - (`Conditional.andCondition` resultPredicate) - simplified - ) - - applyTermSubstitution :: - InternalVariable variable => - Pattern variable -> - Pattern variable - applyTermSubstitution conditional@Conditional{substitution} = - fmap (substitute (Substitution.toMap substitution)) conditional - - assertTermNotPredicate getResults = do - results <- getResults - let -- The term of a result should never be any predicate other than - -- Top or Bottom. - hasPredicateTerm Conditional{term = term'} - | isTop term' || isBottom term' = False - | otherwise = Predicate.isPredicate term' - unsimplified = - filter hasPredicateTerm $ OrPattern.toPatterns results - if null unsimplified - then return results - else - (error . show . Pretty.vsep) - [ "Incomplete simplification!" - , Pretty.indent 2 "input:" - , Pretty.indent 4 (unparse termLike) - , Pretty.indent 2 "unsimplified results:" - , (Pretty.indent 4 . Pretty.vsep) - (unparse <$> unsimplified) - , "Expected all predicates to be removed from the term." - ] - - returnIfSimplifiedOrContinue :: - TermLike RewritingVariableName -> - [Pattern RewritingVariableName] -> - simplifier (OrPattern RewritingVariableName) -> - simplifier (OrPattern RewritingVariableName) - returnIfSimplifiedOrContinue originalTerm resultList continuation = - case resultList of - [] -> return OrPattern.bottom - [result] -> - returnIfResultSimplifiedOrContinue - originalTerm - result - continuation - _ -> continuation - - returnIfResultSimplifiedOrContinue :: - TermLike RewritingVariableName -> - Pattern RewritingVariableName -> - simplifier (OrPattern RewritingVariableName) -> - simplifier (OrPattern RewritingVariableName) - returnIfResultSimplifiedOrContinue originalTerm result continuation - | Pattern.isSimplified sideConditionRepresentation result - , isTop resultTerm - , resultSubstitutionIsEmpty - , SideCondition.cannotReplaceTerm sideCondition (Pattern.term result) = - return (OrPattern.fromPattern result) - | Pattern.isSimplified sideConditionRepresentation result - , isTop resultPredicate - , SideCondition.cannotReplaceTerm sideCondition (Pattern.term result) = - return (OrPattern.fromPattern result) - | isTop resultPredicate && resultTerm == originalTerm - , SideCondition.cannotReplaceTerm sideCondition (Pattern.term result) = - return - ( OrPattern.fromTermLike - ( TermLike.markSimplifiedConditional - sideConditionRepresentation - resultTerm - ) - ) - | isTop resultTerm - , Right condition <- termAsPredicate - , resultPredicate == condition = - return $ - OrPattern.fromPattern $ - Pattern.fromCondition resultSort $ - Condition.markPredicateSimplifiedConditional - sideConditionRepresentation - resultPredicate - | otherwise = continuation - where - resultSort = Pattern.patternSort result - (resultTerm, resultPredicate) = Pattern.splitTerm result - resultSubstitutionIsEmpty = - case resultPredicate of - Conditional{substitution} -> substitution == mempty - termAsPredicate = - Condition.fromPredicate <$> Predicate.makePredicate originalTerm - - descendAndSimplify :: - TermLike RewritingVariableName -> - simplifier (OrPattern RewritingVariableName) - descendAndSimplify termLike = - let ~doNotSimplify = - assert - (TermLike.isSimplified sideConditionRepresentation termLike) - return - (OrPattern.fromTermLike termLike) - avoiding = freeVariables termLike <> freeVariables sideCondition - refreshSetBinder = TermLike.refreshSetBinder avoiding - ~sort = termLikeSort termLike - (_ :< termLikeF) = Recursive.project termLike - termSort = termLikeSort termLike - in case termLikeF of - -- Unimplemented cases - ApplyAliasF _ -> doNotSimplify - -- Do not simplify non-simplifiable patterns. - EndiannessF _ -> doNotSimplify - SignednessF _ -> doNotSimplify - -- We should never attempt to simplify a Rewrites term as this is only used for rules parsing. - RewritesF _ -> error "Attempting to simplify a Rewrites term. This is an error. Please report it at https://github.com/kframework/kore/issues" - -- - AndF andF -> do - let conjuncts = foldMap MultiAnd.fromTermLike andF - (And.simplify termSort Not.notSimplifier sideCondition) - =<< MultiAnd.traverse - (simplifyTermLike sideCondition) - conjuncts - ApplySymbolF applySymbolF -> - Application.simplify sideCondition - =<< simplifyChildren applySymbolF - InjF injF -> - Inj.simplify =<< simplifyChildren injF - CeilF ceilF -> do - ceilF' <- simplifyChildren ceilF - conditions <- Ceil.simplify sideCondition ceilF' - pure (OrPattern.fromOrCondition sort conditions) - EqualsF equalsF -> do - equalsF' <- simplifyChildren equalsF - conditions <- Equals.simplify sideCondition equalsF' - pure (OrPattern.fromOrCondition sort conditions) - ExistsF exists -> do - simplifiedChildren <- - simplifyChildren (refresh exists) - Exists.simplify sideCondition simplifiedChildren - where - avoid = - freeVariableNames termLike - <> freeVariableNames sideCondition - refresh = refreshExists avoid - IffF iffF -> - Iff.simplify sideCondition =<< simplifyChildren iffF - ImpliesF impliesF -> - Implies.simplify sideCondition =<< simplifyChildren impliesF - InF inF -> do - inF' <- simplifyChildren inF - conditions <- In.simplify sideCondition inF' - pure (OrPattern.fromOrCondition sort conditions) - NotF notF -> - Not.simplify sideCondition =<< simplifyChildren notF - -- - BottomF bottomF -> - Bottom.simplify <$> simplifyChildren bottomF - InternalListF internalF -> - InternalList.simplify <$> simplifyChildren internalF - InternalMapF internalMapF -> - InternalMap.simplify <$> simplifyChildren internalMapF - InternalSetF internalSetF -> - InternalSet.simplify <$> simplifyChildren internalSetF - DomainValueF domainValueF -> - DomainValue.simplify <$> simplifyChildren domainValueF - FloorF floorF -> Floor.simplify <$> simplifyChildren floorF - ForallF forall -> - Forall.simplify <$> simplifyChildren (refresh forall) - where - avoid = - freeVariableNames termLike - <> freeVariableNames sideCondition - refresh = refreshForall avoid - InhabitantF inhF -> - Inhabitant.simplify <$> simplifyChildren inhF - MuF mu -> - Mu.simplify <$> simplifyChildren (refresh mu) - where - refresh = Lens.over Binding.muBinder refreshSetBinder - NuF nu -> - Nu.simplify <$> simplifyChildren (refresh nu) - where - refresh = Lens.over Binding.nuBinder refreshSetBinder - -- TODO(virgil): Move next up through patterns. - NextF nextF -> Next.simplify <$> simplifyChildren nextF - OrF orF -> Or.simplify <$> simplifyChildren orF - TopF topF -> Top.simplify <$> simplifyChildren topF - -- - StringLiteralF stringLiteralF -> - return $ StringLiteral.simplify (getConst stringLiteralF) - InternalBoolF internalBoolF -> - return $ InternalBool.simplify (getConst internalBoolF) - InternalBytesF internalBytesF -> - return $ InternalBytes.simplify (getConst internalBytesF) - InternalIntF internalIntF -> - return $ InternalInt.simplify (getConst internalIntF) - InternalStringF internalStringF -> - return $ InternalString.simplify (getConst internalStringF) - VariableF variableF -> - return $ Variable.simplify (getConst variableF) - -{- | We expect each predicate in the result to have been fully - simplified with a different side condition. - See 'Kore.Simplify.Condition.simplifyPredicates'. --} -ensureSimplifiedResult :: - Monad simplifier => - SideCondition.Representation -> - TermLike RewritingVariableName -> - OrPattern RewritingVariableName -> - simplifier (OrPattern RewritingVariableName) -ensureSimplifiedResult repr termLike results - | OrPattern.hasSimplifiedChildrenIgnoreConditions results = - pure results - | otherwise = - (error . show . Pretty.vsep) - [ "Internal error: expected simplified results, but found:" - , (Pretty.indent 4 . Pretty.vsep) - (unparse <$> OrPattern.toPatterns results) - , Pretty.indent 2 "while simplifying:" - , Pretty.indent 4 (unparse termLike) - , Pretty.indent 2 "with side condition:" - , Pretty.indent 4 (Pretty.pretty repr) - ] - -ensureSimplifiedCondition :: - Monad simplifier => - SideCondition.Representation -> - TermLike RewritingVariableName -> - Condition RewritingVariableName -> - simplifier (Condition RewritingVariableName) -ensureSimplifiedCondition repr termLike condition - | Condition.isSimplified repr condition = pure condition - | otherwise = - (error . show . Pretty.vsep) - [ "Internal error: expected simplified condition, but found:" - , Pretty.indent 4 (pretty condition) - , Pretty.indent 2 "while simplifying:" - , Pretty.indent 4 (unparse termLike) - ] - -- | Simplify the given 'TermLike'. Do not simplify any side conditions. -simplifyOnly :: +simplify :: forall simplifier. MonadSimplify simplifier => MonadThrow simplifier => SideCondition RewritingVariableName -> TermLike RewritingVariableName -> simplifier (OrPattern RewritingVariableName) -simplifyOnly sideCondition = +simplify sideCondition = loop . OrPattern.fromTermLike where loop :: diff --git a/kore/test/Test/Kore/Builtin/Bool.hs b/kore/test/Test/Kore/Builtin/Bool.hs index 8abfbbfaf5..531286f0bb 100644 --- a/kore/test/Test/Kore/Builtin/Bool.hs +++ b/kore/test/Test/Kore/Builtin/Bool.hs @@ -111,7 +111,7 @@ testBinary symb impl = a <- forAll Gen.bool b <- forAll Gen.bool let expect = asOrPattern $ impl a b - actual <- evaluateT $ mkApplySymbol symb (asInternal <$> [a, b]) + actual <- evaluateTermT $ mkApplySymbol symb (asInternal <$> [a, b]) (===) expect actual where name = expectHook symb @@ -127,7 +127,7 @@ testUnary symb impl = testPropertyWithSolver (Text.unpack name) $ do a <- forAll Gen.bool let expect = asOrPattern $ impl a - actual <- evaluateT $ mkApplySymbol symb (asInternal <$> [a]) + actual <- evaluateTermT $ mkApplySymbol symb (asInternal <$> [a]) (===) expect actual where name = expectHook symb diff --git a/kore/test/Test/Kore/Builtin/Builtin.hs b/kore/test/Test/Kore/Builtin/Builtin.hs index 8bbfe6132d..88ebfd1ea5 100644 --- a/kore/test/Test/Kore/Builtin/Builtin.hs +++ b/kore/test/Test/Kore/Builtin/Builtin.hs @@ -9,8 +9,10 @@ module Test.Kore.Builtin.Builtin ( testEvaluators, testSymbolWithoutSolver, simplify, - evaluate, - evaluateT, + evaluateTerm, + evaluateTermT, + evaluatePredicate, + evaluatePredicateT, evaluateExpectTopK, evaluateToList, indexedModule, @@ -24,6 +26,7 @@ module Test.Kore.Builtin.Builtin ( simplifyPattern, ) where +import Control.Monad ((>=>)) import Control.Monad.Catch ( MonadMask, ) @@ -53,7 +56,10 @@ import qualified Kore.IndexedModule.MetadataToolsBuilder as MetadataTools ( ) import qualified Kore.IndexedModule.OverloadGraph as OverloadGraph import qualified Kore.IndexedModule.SortGraph as SortGraph -import Kore.Internal.Conditional (Condition) +import Kore.Internal.Condition ( + Condition, + ) +import qualified Kore.Internal.Condition as Condition import Kore.Internal.InternalSet import Kore.Internal.OrPattern ( OrPattern, @@ -62,6 +68,8 @@ import qualified Kore.Internal.OrPattern as OrPattern import Kore.Internal.Pattern ( Pattern, ) +import qualified Kore.Internal.Pattern as Pattern +import Kore.Internal.Predicate (Predicate) import qualified Kore.Internal.SideCondition as SideCondition ( top, ) @@ -82,12 +90,12 @@ import Kore.Rewrite.RulePattern ( import qualified Kore.Rewrite.Step as Step import Kore.Simplify.AndTerms (termUnification) import qualified Kore.Simplify.Condition as Simplifier.Condition -import Kore.Simplify.Data +import Kore.Simplify.Data hiding (simplifyPattern) import Kore.Simplify.InjSimplifier import qualified Kore.Simplify.Not as Not import Kore.Simplify.OverloadSimplifier import qualified Kore.Simplify.Pattern as Pattern -import Kore.Simplify.Simplify +import Kore.Simplify.Simplify hiding (simplifyPattern) import qualified Kore.Simplify.SubstitutionSimplifier as SubstitutionSimplifier import qualified Kore.Simplify.TermLike as TermLike import Kore.Syntax.Definition ( @@ -250,22 +258,41 @@ simplify = . runNoSMT . runSimplifier testEnv . Logic.observeAllT - . simplifyConditionalTerm SideCondition.top + . (simplifyTerm SideCondition.top >=> Logic.scatter) -evaluate :: +evaluateTerm :: (MonadSMT smt, MonadLog smt, MonadProf smt, MonadMask smt) => TermLike RewritingVariableName -> smt (OrPattern RewritingVariableName) -evaluate termLike = - runSimplifier testEnv $ do - TermLike.simplify SideCondition.top termLike +evaluateTerm termLike = + runSimplifier testEnv $ + Pattern.simplify (Pattern.fromTermLike termLike) -evaluateT :: +evaluatePredicate :: + (MonadSMT smt, MonadLog smt, MonadProf smt, MonadMask smt) => + Predicate RewritingVariableName -> + smt (OrPattern RewritingVariableName) +evaluatePredicate predicate = + runSimplifier testEnv $ + Pattern.simplify + ( Pattern.fromCondition kSort + . Condition.fromPredicate + $ predicate + ) + +evaluateTermT :: MonadTrans t => (MonadSMT smt, MonadLog smt, MonadProf smt, MonadMask smt) => TermLike RewritingVariableName -> t smt (OrPattern RewritingVariableName) -evaluateT = lift . evaluate +evaluateTermT = lift . evaluateTerm + +evaluatePredicateT :: + MonadTrans t => + (MonadSMT smt, MonadLog smt, MonadProf smt, MonadMask smt) => + Predicate RewritingVariableName -> + t smt (OrPattern RewritingVariableName) +evaluatePredicateT = lift . evaluatePredicate evaluateExpectTopK :: HasCallStack => @@ -273,7 +300,7 @@ evaluateExpectTopK :: TermLike RewritingVariableName -> Hedgehog.PropertyT smt () evaluateExpectTopK termLike = do - actual <- evaluateT termLike + actual <- evaluateTermT termLike OrPattern.topOf kSort Hedgehog.=== actual evaluateToList :: diff --git a/kore/test/Test/Kore/Builtin/Int.hs b/kore/test/Test/Kore/Builtin/Int.hs index 04eaddb05a..b8a76f2660 100644 --- a/kore/test/Test/Kore/Builtin/Int.hs +++ b/kore/test/Test/Kore/Builtin/Int.hs @@ -81,6 +81,7 @@ import Kore.Builtin.Int ( ) import qualified Kore.Builtin.Int as Int import qualified Kore.Internal.Condition as Condition +import Kore.Internal.From import Kore.Internal.InternalInt import Kore.Internal.Key as Key import qualified Kore.Internal.MultiOr as MultiOr @@ -130,7 +131,7 @@ testUnary symb impl = testPropertyWithSolver (Text.unpack name) $ do a <- forAll genInteger let expect = asOrPattern $ impl a - actual <- evaluateT $ mkApplySymbol symb (asInternal <$> [a]) + actual <- evaluateTermT $ mkApplySymbol symb (asInternal <$> [a]) (===) expect actual where name = expectHook symb @@ -147,7 +148,7 @@ testBinary symb impl = a <- forAll genInteger b <- forAll genInteger let expect = asOrPattern $ impl a b - actual <- evaluateT $ mkApplySymbol symb (asInternal <$> [a, b]) + actual <- evaluateTermT $ mkApplySymbol symb (asInternal <$> [a, b]) (===) expect actual where name = expectHook symb @@ -164,7 +165,7 @@ testComparison symb impl = a <- forAll genInteger b <- forAll genInteger let expect = Test.Bool.asOrPattern $ impl a b - actual <- evaluateT $ mkApplySymbol symb (asInternal <$> [a, b]) + actual <- evaluateTermT $ mkApplySymbol symb (asInternal <$> [a, b]) (===) expect actual where name = expectHook symb @@ -180,7 +181,7 @@ testPartialUnary symb impl = testPropertyWithSolver (Text.unpack name) $ do a <- forAll genInteger let expect = asPartialOrPattern $ impl a - actual <- evaluateT $ mkApplySymbol symb (asInternal <$> [a]) + actual <- evaluateTermT $ mkApplySymbol symb (asInternal <$> [a]) (===) expect actual where name = expectHook symb @@ -197,7 +198,7 @@ testPartialBinary symb impl = a <- forAll genInteger b <- forAll genInteger let expect = asPartialOrPattern $ impl a b - actual <- evaluateT $ mkApplySymbol symb (asInternal <$> [a, b]) + actual <- evaluateTermT $ mkApplySymbol symb (asInternal <$> [a, b]) (===) expect actual where name = expectHook symb @@ -215,7 +216,7 @@ testPartialBinaryZero symb impl = testPropertyWithSolver (Text.unpack name ++ " zero") $ do a <- forAll genInteger let expect = asPartialOrPattern $ impl a 0 - actual <- evaluateT $ mkApplySymbol symb (asInternal <$> [a, 0]) + actual <- evaluateTermT $ mkApplySymbol symb (asInternal <$> [a, 0]) (===) expect actual where name = expectHook symb @@ -233,7 +234,7 @@ testPartialTernary symb impl = b <- forAll genInteger c <- forAll genInteger let expect = asPartialOrPattern $ impl a b c - actual <- evaluateT $ mkApplySymbol symb (asInternal <$> [a, b, c]) + actual <- evaluateTermT $ mkApplySymbol symb (asInternal <$> [a, b, c]) (===) expect actual where name = expectHook symb @@ -383,7 +384,7 @@ test_euclidian_division_theorem = mkApplySymbol symbol (asInternal <$> [a, b]) - & evaluateT + & evaluateTermT & fmap extractValue extractValue :: OrPattern RewritingVariableName -> Integer @@ -463,7 +464,7 @@ testInt :: [TermLike RewritingVariableName] -> OrPattern RewritingVariableName -> TestTree -testInt name = testSymbolWithoutSolver evaluate name +testInt name = testSymbolWithoutSolver evaluateTerm name -- | "\equal"ed internal Integers that are not equal test_unifyEqual_NotEqual :: TestTree @@ -471,7 +472,7 @@ test_unifyEqual_NotEqual = testCaseWithoutSMT "unifyEqual BuiltinInteger: Not Equal" $ do let dv1 = asInternal 1 dv2 = asInternal 2 - actual <- evaluate $ mkEquals kSort dv1 dv2 + actual <- evaluatePredicate $ fromEquals_ dv1 dv2 assertEqual' "" OrPattern.bottom actual -- | "\equal"ed internal Integers that are equal @@ -479,7 +480,7 @@ test_unifyEqual_Equal :: TestTree test_unifyEqual_Equal = testCaseWithoutSMT "unifyEqual BuiltinInteger: Equal" $ do let dv1 = asInternal 2 - actual <- evaluate $ mkEquals kSort dv1 dv1 + actual <- evaluatePredicate $ fromEquals_ dv1 dv1 assertEqual' "" (OrPattern.topOf kSort) actual -- | "\and"ed internal Integers that are not equal @@ -488,7 +489,7 @@ test_unifyAnd_NotEqual = testCaseWithoutSMT "unifyAnd BuiltinInteger: Not Equal" $ do let dv1 = asInternal 1 dv2 = asInternal 2 - actual <- evaluate $ mkAnd dv1 dv2 + actual <- evaluateTerm $ mkAnd dv1 dv2 assertEqual' "" OrPattern.bottom actual -- | "\and"ed internal Integers that are equal @@ -496,7 +497,7 @@ test_unifyAnd_Equal :: TestTree test_unifyAnd_Equal = testCaseWithoutSMT "unifyAnd BuiltinInteger: Equal" $ do let dv1 = asInternal 2 - actual <- evaluate $ mkAnd dv1 dv1 + actual <- evaluateTerm $ mkAnd dv1 dv1 assertEqual' "" (OrPattern.fromTermLike dv1) actual -- | "\and"ed then "\equal"ed internal Integers that are equal @@ -504,7 +505,7 @@ test_unifyAndEqual_Equal :: TestTree test_unifyAndEqual_Equal = testCaseWithoutSMT "unifyAnd BuiltinInteger: Equal" $ do let dv = asInternal 0 - actual <- evaluate $ mkEquals kSort dv $ mkAnd dv dv + actual <- evaluatePredicate $ fromEquals_ dv $ mkAnd dv dv assertEqual' "" (OrPattern.topOf kSort) actual -- | Internal Integer "\and"ed with builtin function applied to variable @@ -522,7 +523,7 @@ test_unifyAnd_Fn = , substitution = mempty } & MultiOr.singleton - actual <- evaluateT $ mkAnd dv fnPat + actual <- evaluateTermT $ mkAnd dv fnPat (===) expect actual test_reflexivity_symbolic :: TestTree @@ -530,7 +531,7 @@ test_reflexivity_symbolic = testCaseWithoutSMT "evaluate symbolic reflexivity for equality" $ do let x = mkElemVar $ "x" `ofSort` intSort expect = Test.Bool.asOrPattern True - actual <- evaluate $ mkApplySymbol eqIntSymbol [x, x] + actual <- evaluateTerm $ mkApplySymbol eqIntSymbol [x, x] assertEqual' "" expect actual test_symbolic_eq_not_conclusive :: TestTree @@ -541,7 +542,7 @@ test_symbolic_eq_not_conclusive = expect = MultiOr.singleton . fromTermLike $ mkApplySymbol eqIntSymbol [x, y] - actual <- evaluate $ mkApplySymbol eqIntSymbol [x, y] + actual <- evaluateTerm $ mkApplySymbol eqIntSymbol [x, y] assertEqual' "" expect actual ofSort :: Text.Text -> Sort -> ElementVariable RewritingVariableName diff --git a/kore/test/Test/Kore/Builtin/InternalBytes.hs b/kore/test/Test/Kore/Builtin/InternalBytes.hs index 7d46075705..4e324a482e 100644 --- a/kore/test/Test/Kore/Builtin/InternalBytes.hs +++ b/kore/test/Test/Kore/Builtin/InternalBytes.hs @@ -75,7 +75,7 @@ test_update = bytes = BS.pack [val] expect = asOrPattern bytes actual <- - evaluateT $ + evaluateTermT $ mkApplySymbol updateBytesSymbol [ asInternal bytes @@ -91,7 +91,7 @@ test_update = val' = toInteger $ ord val expect = OrPattern.bottom actual <- - evaluateT $ + evaluateTermT $ mkApplySymbol updateBytesSymbol [ asInternal bytes @@ -106,7 +106,7 @@ test_update = val' = toInteger $ ord val expect = OrPattern.bottom actual <- - evaluateT $ + evaluateTermT $ mkApplySymbol updateBytesSymbol [ asInternal bytes @@ -140,7 +140,7 @@ test_get = let bytes = E.encode8Bit str expect = OrPattern.bottom actual <- - evaluateT $ + evaluateTermT $ mkApplySymbol getBytesSymbol [ asInternal bytes @@ -152,7 +152,7 @@ test_get = let bytes = E.encode8Bit str expect = OrPattern.bottom actual <- - evaluateT $ + evaluateTermT $ mkApplySymbol getBytesSymbol [ asInternal bytes @@ -163,7 +163,7 @@ test_get = idx <- forAll $ Gen.int (Range.linear 0 256) let expect = OrPattern.bottom actual <- - evaluateT $ + evaluateTermT $ mkApplySymbol getBytesSymbol [ asInternal "" @@ -195,7 +195,7 @@ test_substr = let bytes = E.encode8Bit str expect = OrPattern.bottom actual <- - evaluateT $ + evaluateTermT $ mkApplySymbol substrBytesSymbol [ asInternal bytes @@ -209,7 +209,7 @@ test_substr = let bytes = E.encode8Bit str expect = OrPattern.bottom actual <- - evaluateT $ + evaluateTermT $ mkApplySymbol substrBytesSymbol [ asInternal bytes @@ -224,7 +224,7 @@ test_substr = let bytes = E.encode8Bit str expect = OrPattern.bottom actual <- - evaluateT $ + evaluateTermT $ mkApplySymbol substrBytesSymbol [ asInternal bytes @@ -280,7 +280,7 @@ test_replaceAt = let bytes = E.encode8Bit str expect = asOrPattern bytes actual <- - evaluateT $ + evaluateTermT $ mkApplySymbol replaceAtBytesSymbol [ asInternal bytes @@ -293,7 +293,7 @@ test_replaceAt = idx <- forAll $ Gen.int (Range.linear 0 256) let expect = OrPattern.bottom actual <- - evaluateT $ + evaluateTermT $ mkApplySymbol replaceAtBytesSymbol [ asInternal "" @@ -311,7 +311,7 @@ test_replaceAt = bytes' = E.encode8Bit new expect = OrPattern.bottom actual <- - evaluateT $ + evaluateTermT $ mkApplySymbol replaceAtBytesSymbol [ asInternal bytes @@ -353,7 +353,7 @@ test_padRight = let bytes = E.encode8Bit str expect = asOrPattern bytes actual <- - evaluateT $ + evaluateTermT $ mkApplySymbol padRightBytesSymbol [ asInternal bytes @@ -379,7 +379,7 @@ test_padLeft = let bytes = E.encode8Bit str expect = asOrPattern bytes actual <- - evaluateT $ + evaluateTermT $ mkApplySymbol padLeftBytesSymbol [ asInternal bytes @@ -404,7 +404,7 @@ test_reverse = let bytes = E.encode8Bit str expect = asOrPattern bytes actual <- - evaluateT $ + evaluateTermT $ mkApplySymbol reverseBytesSymbol [ mkApplySymbol @@ -444,7 +444,7 @@ test_concat = let bytes = E.encode8Bit str expect = asOrPattern bytes actual <- - evaluateT $ + evaluateTermT $ mkApplySymbol concatBytesSymbol [ asInternal bytes @@ -456,7 +456,7 @@ test_concat = let bytes = E.encode8Bit str expect = asOrPattern bytes actual <- - evaluateT $ + evaluateTermT $ mkApplySymbol concatBytesSymbol [ asInternal "" @@ -479,7 +479,7 @@ test_reverse_length = let bytes = E.encode8Bit str expect = Test.Int.asOrPattern $ toInteger $ BS.length bytes actual <- - evaluateT $ + evaluateTermT $ mkApplySymbol lengthBytesSymbol [ mkApplySymbol @@ -497,7 +497,7 @@ test_update_get = let bytes = E.encode8Bit str expect = asOrPattern bytes actual <- - evaluateT $ + evaluateTermT $ mkApplySymbol updateBytesSymbol [ asInternal bytes @@ -516,7 +516,7 @@ test_bytes2string_string2bytes = str <- forAll genString let expect = Test.String.asOrPattern str actual <- - evaluateT $ + evaluateTermT $ mkApplySymbol bytes2stringBytesSymbol [ mkApplySymbol @@ -534,7 +534,7 @@ test_decodeBytes_encodeBytes = map testProp encodings str <- forAll genString let expect = Test.String.asOrPattern str actual <- - evaluateT $ + evaluateTermT $ mkApplySymbol decodeBytesBytesSymbol [ Test.String.asInternal encoding @@ -717,4 +717,4 @@ testBytes :: [TermLike RewritingVariableName] -> OrPattern RewritingVariableName -> TestTree -testBytes name = testSymbolWithoutSolver evaluate name +testBytes name = testSymbolWithoutSolver evaluateTerm name diff --git a/kore/test/Test/Kore/Builtin/KEqual.hs b/kore/test/Test/Kore/Builtin/KEqual.hs index c66ce1b56a..01e787efc7 100644 --- a/kore/test/Test/Kore/Builtin/KEqual.hs +++ b/kore/test/Test/Kore/Builtin/KEqual.hs @@ -14,6 +14,7 @@ import Hedgehog import qualified Hedgehog.Gen as Gen import qualified Kore.Builtin.Builtin as Builtin import qualified Kore.Builtin.KEqual as KEqual +import Kore.Internal.From import qualified Kore.Internal.MultiOr as MultiOr import Kore.Internal.Pattern ( Pattern, @@ -67,7 +68,7 @@ testBinary symb impl = b <- forAll Gen.bool let expect = Test.Bool.asOrPattern (impl a b) actual <- - evaluateT + evaluateTermT . mkApplySymbol symb $ inj kSort . Test.Bool.asInternal <$> [a, b] (===) expect actual @@ -81,47 +82,44 @@ test_KEqual = OrPattern.fromTermLike $ Test.Bool.asInternal True original = keqBool dotk dotk - actual <- evaluate original + actual <- evaluateTerm original assertEqual' "" expect actual , testCaseWithoutSMT "kseq(x, dotk) equals kseq(x, dotk)" $ do let expect = OrPattern.topOf kSort xConfigElemVarKItemSort = configElementVariableFromId "x" kItemSort original = - mkEquals - kSort + fromEquals_ (Test.Bool.asInternal True) ( keqBool (kseq (mkElemVar xConfigElemVarKItemSort) dotk) (kseq (mkElemVar xConfigElemVarKItemSort) dotk) ) - actual <- evaluate original + actual <- evaluatePredicate original assertEqual' "" expect actual , testCaseWithoutSMT "kseq(inj(x), dotk) equals kseq(inj(x), dotk)" $ do let expect = OrPattern.topOf kSort xConfigElemVarIdSort = configElementVariableFromId "x" idSort original = - mkEquals - kSort + fromEquals_ (Test.Bool.asInternal True) ( keqBool (kseq (inj kItemSort (mkElemVar xConfigElemVarIdSort)) dotk) (kseq (inj kItemSort (mkElemVar xConfigElemVarIdSort)) dotk) ) - actual <- evaluate original + actual <- evaluatePredicate original assertEqual' "" expect actual , testCaseWithoutSMT "distinct constructor-like terms" $ do let expect = OrPattern.topOf kSort original = - mkEquals - kSort + fromEquals_ (Test.Bool.asInternal False) ( keqBool (kseq (inj kItemSort dvX) dotk) (kseq (inj kItemSort dvT) dotk) ) - actual <- evaluate original + actual <- evaluatePredicate original assertEqual' "" expect actual , testCaseWithoutSMT "kseq(x, dotk) and kseq(x, dotk)" $ do let expect = OrPattern.fromTermLike $ Test.Bool.asInternal True @@ -134,12 +132,12 @@ test_KEqual = (kseq (mkElemVar xConfigElemVarKItemSort) dotk) (kseq (mkElemVar xConfigElemVarKItemSort) dotk) ) - actual <- evaluate original + actual <- evaluateTerm 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) - actual <- evaluate original + actual <- evaluateTerm original assertEqual' "" expect actual , testCaseWithoutSMT "distinct domain value K lists" $ do let expect = Test.Bool.asOrPattern False @@ -147,24 +145,24 @@ test_KEqual = keqBool (kseq (inj kItemSort dvT) dotk) (kseq (inj kItemSort dvX) dotk) - actual <- evaluate original + actual <- evaluateTerm original assertEqual' "" expect actual , testCaseWithoutSMT "Bottom ==K Top" $ do let expect = OrPattern.bottom original = keqBool (mkBottom kSort) (mkTop kSort) - actual <- evaluate original + actual <- evaluateTerm original assertEqual' "" expect actual , testCaseWithoutSMT "X ==K X" $ do let xVar = mkElemVar $ configElementVariableFromId "x" kSort expect = OrPattern.fromTermLike $ Test.Bool.asInternal True original = keqBool xVar xVar - actual <- evaluate original + actual <- evaluateTerm original assertEqual' "" expect actual , testCaseWithoutSMT "X =/=K X" $ do let xVar = mkElemVar $ configElementVariableFromId "x" kSort expect = OrPattern.fromTermLike $ Test.Bool.asInternal False original = kneqBool xVar xVar - actual <- evaluate original + actual <- evaluateTerm original assertEqual' "" expect actual ] @@ -178,7 +176,7 @@ test_KIte = (Test.Bool.asInternal True) (inj kSort $ Test.Bool.asInternal False) (inj kSort $ Test.Bool.asInternal True) - actual <- evaluate original + actual <- evaluateTerm original assertEqual' "" expect actual , testCaseWithoutSMT "false" $ do let expect = @@ -189,7 +187,7 @@ test_KIte = (Test.Bool.asInternal False) (inj kSort $ Test.Bool.asInternal False) (inj kSort $ Test.Bool.asInternal True) - actual <- evaluate original + actual <- evaluateTerm original assertEqual' "" expect actual , testCaseWithoutSMT "abstract" $ do let original = kiteK x y z @@ -197,7 +195,7 @@ test_KIte = x = mkElemVar $ configElementVariableFromId (testId "x") boolSort y = mkElemVar $ configElementVariableFromId (testId "y") kSort z = mkElemVar $ configElementVariableFromId (testId "z") kSort - actual <- evaluate original + actual <- evaluateTerm original assertEqual' "" expect actual ] diff --git a/kore/test/Test/Kore/Builtin/Krypto.hs b/kore/test/Test/Kore/Builtin/Krypto.hs index 173b8b9719..f06a47f3ba 100644 --- a/kore/test/Test/Kore/Builtin/Krypto.hs +++ b/kore/test/Test/Kore/Builtin/Krypto.hs @@ -46,9 +46,7 @@ import Kore.Simplify.Simplify ( ) import qualified Kore.TopBottom as TopBottom import Prelude.Kore -import Test.Kore.Builtin.Builtin hiding ( - evaluate, - ) +import Test.Kore.Builtin.Builtin import Test.Kore.Builtin.Definition import qualified Test.Kore.Builtin.Int as Test.Int import Test.SMT ( diff --git a/kore/test/Test/Kore/Builtin/List.hs b/kore/test/Test/Kore/Builtin/List.hs index 497aee7ba7..e4e8ec399b 100644 --- a/kore/test/Test/Kore/Builtin/List.hs +++ b/kore/test/Test/Kore/Builtin/List.hs @@ -39,6 +39,7 @@ import Hedgehog import qualified Hedgehog.Gen as Gen import qualified Hedgehog.Range as Range import qualified Kore.Builtin.List as List +import Kore.Internal.From import qualified Kore.Internal.MultiOr as MultiOr import Kore.Internal.Pattern as Pattern import Kore.Internal.Predicate ( @@ -82,9 +83,9 @@ test_getUnit = [ mkApplySymbol unitListSymbol [] , Test.Int.asInternal k ] - predicate = mkEquals kSort (mkBottom intSort) patGet - (===) OrPattern.bottom =<< evaluateT patGet - evaluateExpectTopK predicate + predicate = fromEquals_ (mkBottom listSort) patGet + (===) OrPattern.bottom =<< evaluateTermT patGet + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate test_getFirstElement :: TestTree test_getFirstElement = @@ -103,10 +104,10 @@ test_getFirstElement = Seq.Empty -> Nothing v Seq.:<| _ -> Just v patFirst = maybe (mkBottom intSort) Test.Int.asInternal value - predicate = mkEquals kSort patGet patFirst + predicate = fromEquals_ patGet patFirst let expectGet = Test.Int.asPartialPattern value - (===) (MultiOr.singleton expectGet) =<< evaluateT patGet - evaluateExpectTopK predicate + (===) (MultiOr.singleton expectGet) =<< evaluateTermT patGet + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate test_getLastElement :: TestTree test_getLastElement = @@ -126,10 +127,10 @@ test_getLastElement = Seq.Empty -> Nothing _ Seq.:|> v -> Just v patFirst = maybe (mkBottom intSort) Test.Int.asInternal value - predicate = mkEquals kSort patGet patFirst + predicate = fromEquals_ patGet patFirst let expectGet = Test.Int.asPartialPattern value - (===) (MultiOr.singleton expectGet) =<< evaluateT patGet - evaluateExpectTopK predicate + (===) (MultiOr.singleton expectGet) =<< evaluateTermT patGet + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate test_GetUpdate :: TestTree test_GetUpdate = @@ -147,14 +148,17 @@ test_GetUpdate = if 0 <= ix && ix < len then do let patGet = getList patUpdated $ Test.Int.asInternal ix - predicate = mkEquals kSort patGet value + predicate = + fromEquals_ + patGet + value expect = Pattern.fromTermLike value - evaluateExpectTopK predicate - (===) (MultiOr.singleton expect) =<< evaluateT patGet + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate + (===) (MultiOr.singleton expect) =<< evaluateTermT patGet else do - let predicate = mkEquals kSort (mkBottom listSort) patUpdated - (===) OrPattern.bottom =<< evaluateT patUpdated - evaluateExpectTopK predicate + let predicate = fromEquals_ (mkBottom listSort) patUpdated + (===) OrPattern.bottom =<< evaluateTermT patUpdated + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate test_inUnit :: TestTree test_inUnit = @@ -167,9 +171,9 @@ test_inUnit = let patValue = Test.Int.asInternal value patIn = inList patValue unitList patFalse = Test.Bool.asInternal False - predicate = mkEquals kSort patFalse patIn - (===) (Test.Bool.asOrPattern False) =<< evaluateT patIn - evaluateExpectTopK predicate + predicate = fromEquals_ patFalse patIn + (===) (Test.Bool.asOrPattern False) =<< evaluateTermT patIn + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate test_inElement :: TestTree test_inElement = @@ -183,9 +187,9 @@ test_inElement = patElement = elementList patValue patIn = inList patValue patElement patTrue = Test.Bool.asInternal True - predicate = mkEquals kSort patIn patTrue - (===) (Test.Bool.asOrPattern True) =<< evaluateT patIn - evaluateExpectTopK predicate + predicate = fromEquals_ patIn patTrue + (===) (Test.Bool.asOrPattern True) =<< evaluateTermT patIn + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate test_inConcat :: TestTree test_inConcat = @@ -202,9 +206,9 @@ test_inConcat = patConcat = concatList patValues patElement patIn = inList patValue patConcat patTrue = Test.Bool.asInternal True - predicate = mkEquals kSort patIn patTrue - (===) (Test.Bool.asOrPattern True) =<< evaluateT patIn - evaluateExpectTopK predicate + predicate = fromEquals_ patIn patTrue + (===) (Test.Bool.asOrPattern True) =<< evaluateTermT patIn + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate test_concatUnit :: TestTree test_concatUnit = @@ -218,13 +222,13 @@ test_concatUnit = patValues = asTermLike (Test.Int.asInternal <$> values) patConcat1 = mkApplySymbol concatListSymbol [patUnit, patValues] patConcat2 = mkApplySymbol concatListSymbol [patValues, patUnit] - predicate1 = mkEquals kSort patValues patConcat1 - predicate2 = mkEquals kSort patValues patConcat2 - expectValues <- evaluateT patValues - (===) expectValues =<< evaluateT patConcat1 - (===) expectValues =<< evaluateT patConcat2 - evaluateExpectTopK predicate1 - evaluateExpectTopK predicate2 + predicate1 = fromEquals_ patValues patConcat1 + predicate2 = fromEquals_ patValues patConcat2 + expectValues <- evaluateTermT patValues + (===) expectValues =<< evaluateTermT patConcat1 + (===) expectValues =<< evaluateTermT patConcat2 + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate1 + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate2 test_concatUnitSymbolic :: TestTree test_concatUnitSymbolic = @@ -238,13 +242,13 @@ test_concatUnitSymbolic = mkElemVar $ configElementVariableFromId (testId "x") listSort patConcat1 = mkApplySymbol concatListSymbol [patUnit, patSymbolic] patConcat2 = mkApplySymbol concatListSymbol [patSymbolic, patUnit] - predicate1 = mkEquals kSort patSymbolic patConcat1 - predicate2 = mkEquals kSort patSymbolic patConcat2 - expectSymbolic <- evaluateT patSymbolic - (===) expectSymbolic =<< evaluateT patConcat1 - (===) expectSymbolic =<< evaluateT patConcat2 - evaluateExpectTopK predicate1 - evaluateExpectTopK predicate2 + predicate1 = fromEquals_ patSymbolic patConcat1 + predicate2 = fromEquals_ patSymbolic patConcat2 + expectSymbolic <- evaluateTermT patSymbolic + (===) expectSymbolic =<< evaluateTermT patConcat1 + (===) expectSymbolic =<< evaluateTermT patConcat2 + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate1 + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate2 test_concatAssociates :: TestTree test_concatAssociates = @@ -265,11 +269,11 @@ test_concatAssociates = mkApplySymbol concatListSymbol [patConcat12, patList3] patConcat1_23 = mkApplySymbol concatListSymbol [patList1, patConcat23] - predicate = mkEquals kSort patConcat12_3 patConcat1_23 - evalConcat12_3 <- evaluateT patConcat12_3 - evalConcat1_23 <- evaluateT patConcat1_23 + predicate = fromEquals_ patConcat12_3 patConcat1_23 + evalConcat12_3 <- evaluateTermT patConcat12_3 + evalConcat1_23 <- evaluateTermT patConcat1_23 (===) evalConcat12_3 evalConcat1_23 - evaluateExpectTopK predicate + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate test_concatSymbolic :: TestTree test_concatSymbolic = @@ -307,7 +311,7 @@ test_concatSymbolic = ) } & MultiOr.singleton - unified <- evaluateT patUnifiedXY + unified <- evaluateTermT patUnifiedXY expect === unified let patConcatX' = concatList patSymbolicXs patElemX @@ -327,7 +331,7 @@ test_concatSymbolic = ) } & MultiOr.singleton - unified' <- evaluateT patUnifiedXY' + unified' <- evaluateTermT patUnifiedXY' expect' === unified' test_concatSymbolicDifferentLengths :: TestTree @@ -373,7 +377,7 @@ test_concatSymbolicDifferentLengths = ) } & MultiOr.singleton - unified <- evaluateT patUnifiedXY + unified <- evaluateTermT patUnifiedXY expect === unified ofSort :: Text -> Sort -> ElementVariable RewritingVariableName @@ -387,7 +391,7 @@ test_simplify = let x = mkElemVar (configElementVariableFromId (testId "x") intSort) original = asInternal [mkAnd x (mkTop intSort)] expected = MultiOr.singleton $ asPattern [x] - (===) expected =<< evaluateT original + (===) expected =<< evaluateTermT original test_isBuiltin :: [TestTree] test_isBuiltin = @@ -410,41 +414,41 @@ test_size = [ testPropertyWithSolver "size(unit(_)) = 0" $ do let original = sizeList unitList zero = mkInt 0 - predicate = mkEquals kSort zero original - (===) (OrPattern.fromTermLike zero) =<< evaluateT original - evaluateExpectTopK predicate + predicate = fromEquals_ zero original + (===) (OrPattern.fromTermLike zero) =<< evaluateTermT original + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate , testPropertyWithSolver "size(element(_)) = 1" $ do k <- forAll genInteger let original = sizeList (elementList $ mkInt k) one = mkInt 1 - predicate = mkEquals kSort one original - (===) (OrPattern.fromTermLike one) =<< evaluateT original - evaluateExpectTopK predicate + predicate = fromEquals_ one original + (===) (OrPattern.fromTermLike one) =<< evaluateTermT original + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT 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 kSort sizeConcat addSize - expect1 <- evaluateT sizeConcat - expect2 <- evaluateT addSize + predicate = fromEquals_ sizeConcat addSize + expect1 <- evaluateTermT sizeConcat + expect2 <- evaluateTermT addSize (===) expect1 expect2 - evaluateExpectTopK predicate + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate ] test_make :: [TestTree] test_make = [ testCaseWithoutSMT "make(-1, 5) === \\bottom" $ do - result <- evaluate $ makeList (mkInt (-1)) (mkInt 5) + result <- evaluateTerm $ makeList (mkInt (-1)) (mkInt 5) assertEqual' "" OrPattern.bottom result , testCaseWithoutSMT "make(0, 5) === []" $ do - result <- evaluate $ makeList (mkInt 0) (mkInt 5) + result <- evaluateTerm $ makeList (mkInt 0) (mkInt 5) assertEqual' "" (OrPattern.fromTermLike $ asInternal []) result , testCaseWithoutSMT "make(3, 5) === [5, 5, 5]" $ do - result <- evaluate $ makeList (mkInt 3) (mkInt 5) + result <- evaluateTerm $ makeList (mkInt 3) (mkInt 5) let expect = asInternal . fmap mkInt $ Seq.fromList [5, 5, 5] assertEqual' "" (OrPattern.fromTermLike expect) result ] @@ -453,17 +457,17 @@ test_updateAll :: [TestTree] test_updateAll = [ testCaseWithoutSMT "updateAll([1, 2, 3], -1, [5]) === \\bottom" $ do result <- - evaluate $ + evaluateTerm $ updateAllList original (mkInt (-1)) (elementList $ mkInt 5) assertEqual' "" OrPattern.bottom result , testCaseWithoutSMT "updateAll([1, 2, 3], 10, []) === [1, 2, 3]" $ do result <- - evaluate $ + evaluateTerm $ updateAllList original (mkInt 10) unitList assertEqual' "" (OrPattern.fromTermLike original) result , testCaseWithoutSMT "updateAll([1, 2, 3], 1, [5]) === [1, 5, 3]" $ do result <- - evaluate $ + evaluateTerm $ updateAllList original (mkInt 1) (elementList $ mkInt 5) let expect = asInternal . fmap mkInt $ Seq.fromList [1, 5, 3] assertEqual' "" (OrPattern.fromTermLike expect) result @@ -471,7 +475,7 @@ test_updateAll = do let new = asInternal . fmap mkInt $ Seq.fromList [1, 2, 3, 4] result <- - evaluate $ + evaluateTerm $ updateAllList original (mkInt 0) new assertEqual' "" OrPattern.bottom result ] diff --git a/kore/test/Test/Kore/Builtin/Map.hs b/kore/test/Test/Kore/Builtin/Map.hs index ac45bd8dd6..14348f6143 100644 --- a/kore/test/Test/Kore/Builtin/Map.hs +++ b/kore/test/Test/Kore/Builtin/Map.hs @@ -77,6 +77,7 @@ import qualified Hedgehog.Range as Range import qualified Kore.Builtin.AssociativeCommutative as Ac import qualified Kore.Builtin.Map as Map import qualified Kore.Builtin.Map.Map as Map +import Kore.Internal.From import Kore.Internal.InternalMap import qualified Kore.Internal.MultiOr as MultiOr import Kore.Internal.Pattern @@ -154,28 +155,21 @@ 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 intSort) patLookup - (===) OrPattern.bottom =<< evaluateT patLookup - evaluateExpectTopK predicate + predicate = fromEquals_ (mkBottom mapSort) patLookup + (===) OrPattern.bottom =<< evaluateTermT patLookup + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT 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 - evaluateExpectTopK predicate + predicate = fromEquals_ def patLookup + (===) (OrPattern.fromTermLike def) =<< evaluateTermT patLookup + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate ] test_lookupUpdate :: [TestTree] @@ -185,10 +179,10 @@ test_lookupUpdate = patVal <- forAll genIntegerPattern patMap <- forAll genMapPattern let patLookup = lookupMap (updateMap patMap patKey patVal) patKey - predicate = mkEquals_ patLookup patVal + predicate = fromEquals_ patLookup patVal expect = OrPattern.fromTermLike patVal - (===) expect =<< evaluateT patLookup - evaluateExpectTopK predicate + (===) expect =<< evaluateTermT patLookup + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate , testPropertyWithoutSolver "lookupOrDefault{}(update{}(map, key, val), key, def) === val" $ do patKey <- forAll genIntegerPattern patDef <- forAll genIntegerPattern @@ -196,10 +190,10 @@ test_lookupUpdate = patMap <- forAll genMapPattern let patUpdate = updateMap patMap patKey patVal patLookup = lookupOrDefaultMap patUpdate patKey patDef - predicate = mkEquals_ patLookup patVal + predicate = fromEquals_ patLookup patVal expect = OrPattern.fromTermLike patVal - (===) expect =<< evaluateT patLookup - evaluateExpectTopK predicate + (===) expect =<< evaluateTermT patLookup + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate ] test_removeUnit :: TestTree @@ -209,10 +203,10 @@ test_removeUnit = ( do key <- forAll genIntegerPattern let patRemove = removeMap unitMap key - predicate = mkEquals_ unitMap patRemove - expect <- evaluateT unitMap - (===) expect =<< evaluateT patRemove - evaluateExpectTopK predicate + predicate = fromEquals_ unitMap patRemove + expect <- evaluateTermT unitMap + (===) expect =<< evaluateTermT patRemove + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate ) test_sizeUnit :: TestTree @@ -227,10 +221,10 @@ test_sizeUnit = mkApplySymbol sizeMapSymbol [asTermLike someMap] - predicate = mkEquals_ patExpected patActual - expect <- evaluateT patExpected - (===) expect =<< evaluateT patActual - evaluateExpectTopK predicate + predicate = fromEquals_ patExpected patActual + expect <- evaluateTermT patExpected + (===) expect =<< evaluateTermT patActual + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate ) test_removeKeyNotIn :: TestTree @@ -240,13 +234,13 @@ test_removeKeyNotIn = ( do key <- forAll genIntegerPattern map' <- forAll genMapPattern - isInMap <- evaluateT $ lookupMap map' key + isInMap <- evaluateTermT $ lookupMap map' key unless (OrPattern.bottom == isInMap) discard let patRemove = removeMap map' key - predicate = mkEquals_ map' patRemove - expect <- evaluateT map' - (===) expect =<< evaluateT patRemove - evaluateExpectTopK predicate + predicate = fromEquals_ map' patRemove + expect <- evaluateTermT map' + (===) expect =<< evaluateTermT patRemove + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate ) test_removeKeyIn :: TestTree @@ -257,13 +251,13 @@ test_removeKeyIn = key <- forAll genIntegerPattern val <- forAll genIntegerPattern map' <- forAll genMapPattern - isInMap <- evaluateT $ lookupMap map' key + isInMap <- evaluateTermT $ lookupMap map' key unless (OrPattern.bottom == isInMap) discard let patRemove = removeMap (updateMap map' key val) key - predicate = mkEquals_ patRemove map' - expect <- evaluateT map' - (===) expect =<< evaluateT patRemove - evaluateExpectTopK predicate + predicate = fromEquals_ patRemove map' + expect <- evaluateTermT map' + (===) expect =<< evaluateTermT patRemove + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate ) test_removeAllMapUnit :: TestTree @@ -273,10 +267,10 @@ test_removeAllMapUnit = ( do set <- forAll Test.Set.genSetPattern let patRemoveAll = removeAllMap unitMap set - predicate = mkEquals_ unitMap patRemoveAll - expect <- evaluateT unitMap - (===) expect =<< evaluateT patRemoveAll - evaluateExpectTopK predicate + predicate = fromEquals_ unitMap patRemoveAll + expect <- evaluateTermT unitMap + (===) expect =<< evaluateTermT patRemoveAll + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate ) test_removeAllSetUnit :: TestTree @@ -286,10 +280,10 @@ test_removeAllSetUnit = ( do map' <- forAll genMapPattern let patRemoveAll = removeAllMap map' unitSet - predicate = mkEquals_ map' patRemoveAll - expect <- evaluateT map' - (===) expect =<< evaluateT patRemoveAll - evaluateExpectTopK predicate + predicate = fromEquals_ map' patRemoveAll + expect <- evaluateTermT map' + (===) expect =<< evaluateTermT patRemoveAll + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate ) test_removeAll :: TestTree @@ -310,10 +304,10 @@ test_removeAll = removeAllMap (removeMap map' patKey) patDiffSet - predicate = mkEquals_ patRemoveAll1 patRemoveAll2 - expect <- evaluateT patRemoveAll2 - (===) expect =<< evaluateT patRemoveAll1 - evaluateExpectTopK predicate + predicate = fromEquals_ patRemoveAll1 patRemoveAll2 + expect <- evaluateTermT patRemoveAll2 + (===) expect =<< evaluateTermT patRemoveAll1 + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate ) test_concatUnit :: TestTree @@ -325,13 +319,13 @@ test_concatUnit = let patConcat2 = concatMap patUnit patMap patConcat1 = concatMap patMap patUnit patUnit = unitMap - predicate1 = mkEquals_ patMap patConcat1 - predicate2 = mkEquals_ patMap patConcat2 - expect <- evaluateT patMap - (===) expect =<< evaluateT patConcat1 - (===) expect =<< evaluateT patConcat2 - evaluateExpectTopK predicate1 - evaluateExpectTopK predicate2 + predicate1 = fromEquals_ patMap patConcat1 + predicate2 = fromEquals_ patMap patConcat2 + expect <- evaluateTermT patMap + (===) expect =<< evaluateTermT patConcat1 + (===) expect =<< evaluateTermT patConcat2 + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate1 + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate2 ) test_lookupConcatUniqueKeys :: TestTree @@ -350,17 +344,17 @@ test_lookupConcatUniqueKeys = patLookup1 = lookupMap patConcat patKey1 patLookup2 = lookupMap patConcat patKey2 predicate = - mkImplies - (mkNot (mkEquals_ patKey1 patKey2)) - ( mkAnd - (mkEquals_ patLookup1 patVal1) - (mkEquals_ patLookup2 patVal2) + fromImplies + (fromNot (fromEquals_ patKey1 patKey2)) + ( fromAnd + (fromEquals_ patLookup1 patVal1) + (fromEquals_ patLookup2 patVal2) ) expect1 = OrPattern.fromTermLike patVal1 expect2 = OrPattern.fromTermLike patVal2 - (===) expect1 =<< evaluateT patLookup1 - (===) expect2 =<< evaluateT patLookup2 - evaluateExpectTopK predicate + (===) expect1 =<< evaluateTermT patLookup1 + (===) expect2 =<< evaluateTermT patLookup2 + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate ) test_concatDuplicateKeys :: TestTree @@ -374,9 +368,9 @@ test_concatDuplicateKeys = let patMap1 = elementMap patKey patVal1 patMap2 = elementMap patKey patVal2 patConcat = concatMap patMap1 patMap2 - predicate = mkEquals_ (mkBottom mapSort) patConcat - (===) OrPattern.bottom =<< evaluateT patConcat - evaluateExpectTopK predicate + predicate = fromEquals_ (mkBottom mapSort) patConcat + (===) OrPattern.bottom =<< evaluateTermT patConcat + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate ) test_concatCommutes :: TestTree @@ -388,11 +382,11 @@ test_concatCommutes = patMap2 <- forAll genMapPattern let patConcat1 = concatMap patMap1 patMap2 patConcat2 = concatMap patMap2 patMap1 - predicate = mkEquals_ patConcat1 patConcat2 - actual1 <- evaluateT patConcat1 - actual2 <- evaluateT patConcat2 + predicate = fromEquals_ patConcat1 patConcat2 + actual1 <- evaluateTermT patConcat1 + actual2 <- evaluateTermT patConcat2 (===) actual1 actual2 - evaluateExpectTopK predicate + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate ) test_concatAssociates :: TestTree @@ -407,11 +401,11 @@ test_concatAssociates = patConcat23 = concatMap patMap2 patMap3 patConcat12_3 = concatMap patConcat12 patMap3 patConcat1_23 = concatMap patMap1 patConcat23 - predicate = mkEquals_ patConcat12_3 patConcat1_23 - actual12_3 <- evaluateT patConcat12_3 - actual1_23 <- evaluateT patConcat1_23 + predicate = fromEquals_ patConcat12_3 patConcat1_23 + actual12_3 <- evaluateTermT patConcat12_3 + actual1_23 <- evaluateTermT patConcat1_23 (===) actual12_3 actual1_23 - evaluateExpectTopK predicate + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate ) test_inKeysUnit :: TestTree @@ -422,9 +416,9 @@ test_inKeysUnit = patKey <- forAll genIntegerPattern let patUnit = unitMap patInKeys = inKeysMap patKey patUnit - predicate = mkEquals_ (Test.Bool.asInternal False) patInKeys - (===) (Test.Bool.asOrPattern False) =<< evaluateT patInKeys - evaluateExpectTopK predicate + predicate = fromEquals_ (Test.Bool.asInternal False) patInKeys + (===) (Test.Bool.asOrPattern False) =<< evaluateTermT patInKeys + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate ) test_keysUnit :: TestTree @@ -435,10 +429,10 @@ test_keysUnit = let patUnit = unitMap patKeys = keysMap patUnit patExpect = mkSet_ HashSet.empty - predicate = mkEquals_ patExpect patKeys - expect <- evaluate patExpect - assertEqual "" expect =<< evaluate patKeys - assertEqual "" (OrPattern.topOf kSort) =<< evaluate predicate + predicate = fromEquals_ patExpect patKeys + expect <- evaluateTerm patExpect + assertEqual "" expect =<< evaluateTerm patKeys + assertEqual "" (OrPattern.topOf kSort) =<< evaluatePredicate predicate test_keysElement :: TestTree test_keysElement = @@ -450,10 +444,10 @@ test_keysElement = let patMap = asTermLike $ HashMap.singleton key val patKeys = mkSet_ (HashSet.singleton $ from key) & fromConcrete patSymbolic = keysMap patMap - predicate = mkEquals_ patKeys patSymbolic - expect <- evaluateT patKeys - (===) expect =<< evaluateT patSymbolic - evaluateExpectTopK predicate + predicate = fromEquals_ patKeys patSymbolic + expect <- evaluateTermT patKeys + (===) expect =<< evaluateTermT patSymbolic + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate ) test_keys :: TestTree @@ -466,10 +460,10 @@ test_keys = patConcreteKeys = mkSet_ keys1 & fromConcrete patMap = asTermLike map1 patSymbolicKeys = keysMap patMap - predicate = mkEquals_ patConcreteKeys patSymbolicKeys - expect <- evaluateT patConcreteKeys - (===) expect =<< evaluateT patSymbolicKeys - evaluateExpectTopK predicate + predicate = fromEquals_ patConcreteKeys patSymbolicKeys + expect <- evaluateTermT patConcreteKeys + (===) expect =<< evaluateTermT patSymbolicKeys + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate ) test_keysListUnit :: TestTree @@ -480,10 +474,10 @@ test_keysListUnit = let patUnit = unitMap patKeys = keysListMap patUnit patExpect = Test.List.asTermLike [] - predicate = mkEquals_ patExpect patKeys - expect <- evaluate patExpect - assertEqual "" expect =<< evaluate patKeys - assertEqual "" (OrPattern.topOf kSort) =<< evaluate predicate + predicate = fromEquals_ patExpect patKeys + expect <- evaluateTerm patExpect + assertEqual "" expect =<< evaluateTerm patKeys + assertEqual "" (OrPattern.topOf kSort) =<< evaluatePredicate predicate test_keysListElement :: TestTree test_keysListElement = @@ -495,10 +489,10 @@ test_keysListElement = let patMap = asTermLike $ HashMap.singleton key val patKeys = Test.List.asTermLike [from key] patSymbolic = keysListMap patMap - predicate = mkEquals_ patKeys patSymbolic - expect <- evaluateT patKeys - (===) expect =<< evaluateT patSymbolic - evaluateExpectTopK predicate + predicate = fromEquals_ patKeys patSymbolic + expect <- evaluateTermT patKeys + (===) expect =<< evaluateTermT patSymbolic + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate ) test_keysList :: TestTree @@ -511,10 +505,10 @@ test_keysList = patConcreteKeys = Test.List.asTermLike keys1 patMap = asTermLike map1 patSymbolicKeys = keysListMap patMap - predicate = mkEquals_ patConcreteKeys patSymbolicKeys - expect <- evaluateT patConcreteKeys - (===) expect =<< evaluateT patSymbolicKeys - evaluateExpectTopK predicate + predicate = fromEquals_ patConcreteKeys patSymbolicKeys + expect <- evaluateTermT patConcreteKeys + (===) expect =<< evaluateTermT patSymbolicKeys + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate ) test_inKeysElement :: TestTree @@ -526,9 +520,9 @@ test_inKeysElement = patVal <- forAll genIntegerPattern let patMap = elementMap patKey patVal patInKeys = inKeysMap patKey patMap - predicate = mkEquals_ (Test.Bool.asInternal True) patInKeys - (===) (Test.Bool.asOrPattern True) =<< evaluateT patInKeys - evaluateExpectTopK predicate + predicate = fromEquals_ (Test.Bool.asInternal True) patInKeys + (===) (Test.Bool.asOrPattern True) =<< evaluateTermT patInKeys + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate ) test_values :: TestTree @@ -542,10 +536,10 @@ test_values = Test.List.asTermLike $ builtinList values patMap = asTermLike map1 patValues = valuesMap patMap - predicate = mkEquals_ patConcreteValues patValues - expect <- evaluateT patValues - (===) expect =<< evaluateT patConcreteValues - evaluateExpectTopK predicate + predicate = fromEquals_ patConcreteValues patValues + expect <- evaluateTermT patValues + (===) expect =<< evaluateTermT patConcreteValues + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate ) test_inclusion :: [TestTree] @@ -562,28 +556,28 @@ test_inclusion = patMap2 = concatMap patMap1 (elementMap patKey2 patVal2) patInclusion = inclusionMap patMap1 patMap2 predicate = - mkImplies - (mkNot (mkEquals_ patKey1 patKey2)) - (mkEquals_ (Test.Bool.asInternal True) patInclusion) - (===) (Test.Bool.asOrPattern True) =<< evaluateT patInclusion - evaluateExpectTopK predicate + fromImplies + (fromNot (fromEquals_ patKey1 patKey2)) + (fromEquals_ (Test.Bool.asInternal True) patInclusion) + (===) (Test.Bool.asOrPattern True) =<< evaluateTermT patInclusion + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate ) , testPropertyWithSolver "MAP.inclusion success: empty map <= empty map" ( do let patInclusion = inclusionMap unitMap unitMap - predicate = mkEquals_ (Test.Bool.asInternal True) patInclusion - (===) (Test.Bool.asOrPattern True) =<< evaluateT patInclusion - evaluateExpectTopK predicate + predicate = fromEquals_ (Test.Bool.asInternal True) patInclusion + (===) (Test.Bool.asOrPattern True) =<< evaluateTermT patInclusion + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate ) , testPropertyWithSolver "MAP.inclusion success: empty map <= any map" ( do patSomeMap <- forAll genMapPattern let patInclusion = inclusionMap unitMap patSomeMap - predicate = mkEquals_ (Test.Bool.asInternal True) patInclusion - (===) (Test.Bool.asOrPattern True) =<< evaluateT patInclusion - evaluateExpectTopK predicate + predicate = fromEquals_ (Test.Bool.asInternal True) patInclusion + (===) (Test.Bool.asOrPattern True) =<< evaluateTermT patInclusion + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate ) , testPropertyWithSolver "MAP.inclusion failure: !(some map <= empty map)" @@ -592,9 +586,9 @@ test_inclusion = patVal1 <- forAll genIntegerPattern let patSomeMap = elementMap patKey1 patVal1 patInclusion = inclusionMap patSomeMap unitMap - predicate = mkEquals_ (Test.Bool.asInternal False) patInclusion - (===) (Test.Bool.asOrPattern False) =<< evaluateT patInclusion - evaluateExpectTopK predicate + predicate = fromEquals_ (Test.Bool.asInternal False) patInclusion + (===) (Test.Bool.asOrPattern False) =<< evaluateTermT patInclusion + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate ) , testPropertyWithSolver "MAP.inclusion failure: lhs key not included in rhs map" @@ -608,11 +602,11 @@ test_inclusion = patMap2 = concatMap patMap1 (elementMap patKey2 patVal2) patInclusion = inclusionMap patMap2 patMap1 predicate = - mkImplies - (mkNot (mkEquals_ patKey1 patKey2)) - (mkEquals_ (Test.Bool.asInternal False) patInclusion) - (===) (Test.Bool.asOrPattern False) =<< evaluateT patInclusion - evaluateExpectTopK predicate + fromImplies + (fromNot (fromEquals_ patKey1 patKey2)) + (fromEquals_ (Test.Bool.asInternal False) patInclusion) + (===) (Test.Bool.asOrPattern False) =<< evaluateTermT patInclusion + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate ) , testPropertyWithSolver "MAP.inclusion failure: lhs key maps differently in rhs map" @@ -630,11 +624,11 @@ test_inclusion = patMap2 = concatMap (elementMap patKey1 patVal1') (elementMap patKey2 patVal2) patInclusion = inclusionMap patMap1 patMap2 predicate = - mkImplies - (mkNot (mkEquals_ patKey1 patKey2)) - (mkEquals_ (Test.Bool.asInternal False) patInclusion) - (===) (Test.Bool.asOrPattern False) =<< evaluateT patInclusion - evaluateExpectTopK predicate + fromImplies + (fromNot (fromEquals_ patKey1 patKey2)) + (fromEquals_ (Test.Bool.asInternal False) patInclusion) + (===) (Test.Bool.asOrPattern False) =<< evaluateTermT patInclusion + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate ) ] @@ -649,7 +643,7 @@ test_simplify = & asTermLike expected = MultiOr.singleton . asPattern $ HashMap.fromList [(key, x)] - actual <- evaluate original + actual <- evaluateTerm original assertEqual "expected simplified Map" expected actual -- | Maps with symbolic keys are not simplified. @@ -664,7 +658,7 @@ test_symbolic = expect = MultiOr.singleton $ asVariablePattern varMap if HashMap.null elements then discard - else (===) expect =<< evaluateT patMap + else (===) expect =<< evaluateTermT patMap ) test_isBuiltin :: [TestTree] @@ -702,11 +696,9 @@ test_unifyConcrete = asTermLike (uncurry mkAnd <$> map12) patActual = mkAnd (asTermLike map1) (asTermLike map2) - predicate = mkEquals_ patExpect patActual - expect <- evaluateT patExpect - actual <- evaluateT patActual + expect <- evaluateTermT patExpect + actual <- evaluateTermT patActual (===) expect actual - evaluateExpectTopK predicate ) -- Given a function to scramble the arguments to concat, i.e., @@ -835,7 +827,7 @@ test_unifySelectFromEmpty = where emptyMap = asTermLike HashMap.empty doesNotUnifyWith pat1 pat2 = - (===) OrPattern.bottom =<< evaluateT (mkAnd pat1 pat2) + (===) OrPattern.bottom =<< evaluateTermT (mkAnd pat1 pat2) test_unifySelectFromSingleton :: TestTree test_unifySelectFromSingleton = @@ -1203,7 +1195,7 @@ test_concretizeKeys = testCaseWithoutSMT "unify a concrete Map with a symbolic Map" $ do - actual <- evaluate original + actual <- evaluateTerm original assertEqual "expected simplified Map" expected actual where x = @@ -1252,7 +1244,7 @@ test_concretizeKeysAxiom = "unify a concrete Map with a symbolic Map in an axiom" $ do let concreteMap = asTermLike $ HashMap.fromList [(key, val)] - config <- evaluate $ pair symbolicKey concreteMap + config <- evaluateTerm $ pair symbolicKey concreteMap actual <- MultiOr.traverse (flip runStep axiom) config assertEqual "expected MAP.lookup" expected (MultiOr.flatten actual) where diff --git a/kore/test/Test/Kore/Builtin/Set.hs b/kore/test/Test/Kore/Builtin/Set.hs index 850e748f57..af95f135fe 100644 --- a/kore/test/Test/Kore/Builtin/Set.hs +++ b/kore/test/Test/Kore/Builtin/Set.hs @@ -87,6 +87,7 @@ import qualified Kore.Builtin.Set as Set import qualified Kore.Builtin.Set.Set as Set import qualified Kore.Internal.Condition as Condition import qualified Kore.Internal.Conditional as Conditional +import Kore.Internal.From import Kore.Internal.InternalSet import qualified Kore.Internal.MultiOr as MultiOr import Kore.Internal.Pattern as Pattern @@ -207,19 +208,12 @@ test_unit = TestTree becomes original expect name = testCase name $ do - actual <- runNoSMT $ evaluate original + actual <- runNoSMT $ evaluateTerm original assertEqual "" (OrPattern.fromTermLike expect) actual -mkEquals_ :: - InternalVariable variable => - TermLike variable -> - TermLike variable -> - TermLike variable -mkEquals_ = mkEquals kSort - test_getUnit :: TestTree test_getUnit = testPropertyWithSolver @@ -233,9 +227,9 @@ test_getUnit = , mkApplySymbol unitSetSymbol [] ] patFalse = Test.Bool.asInternal False - predicate = mkEquals_ patFalse patIn - (===) (Test.Bool.asOrPattern False) =<< evaluateT patIn - evaluateExpectTopK predicate + predicate = fromEquals_ patFalse patIn + (===) (Test.Bool.asOrPattern False) =<< evaluateTermT patIn + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate ) test_inElement :: TestTree @@ -247,9 +241,9 @@ test_inElement = let patIn = mkApplySymbol inSetSymbol [patKey, patElement] patElement = mkApplySymbol elementSetSymbol [patKey] patTrue = Test.Bool.asInternal True - predicate = mkEquals_ patIn patTrue - (===) (Test.Bool.asOrPattern True) =<< evaluateT patIn - evaluateExpectTopK predicate + predicate = fromEquals_ patIn patTrue + (===) (Test.Bool.asOrPattern True) =<< evaluateTermT patIn + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate ) test_inUnitSymbolic :: TestTree @@ -265,9 +259,9 @@ test_inUnitSymbolic = , mkApplySymbol unitSetSymbol [] ] patFalse = Test.Bool.asInternal False - predicate = mkEquals_ patFalse patIn - (===) (Test.Bool.asOrPattern False) =<< evaluateT patIn - evaluateExpectTopK predicate + predicate = fromEquals_ patFalse patIn + (===) (Test.Bool.asOrPattern False) =<< evaluateTermT patIn + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate ) test_inElementSymbolic :: TestTree @@ -280,8 +274,8 @@ test_inElementSymbolic = patIn = mkApplySymbol inSetSymbolTestSort [patKey, patElement] patTrue = Test.Bool.asInternal True conditionTerm = mkAnd patTrue (mkCeil boolSort patElement) - actual <- evaluateT patIn - expected <- evaluateT conditionTerm + actual <- evaluateTermT patIn + expected <- evaluateTermT conditionTerm actual === expected ) @@ -298,15 +292,15 @@ test_inConcatSymbolic = HashSet.insert patKey (HashSet.fromList keys) patIn = mkApplySymbol inSetSymbolTestSort [patKey, patSet] patTrue = Test.Bool.asPattern True - conditionTerm = mkCeil boolSort patSet - condition <- evaluateT conditionTerm + conditionTerm = fromCeil_ patSet + condition <- evaluatePredicateT conditionTerm let expected = MultiOr.map ( Condition.andCondition patTrue . Conditional.withoutTerm ) condition - actual <- evaluateT patIn + actual <- evaluateTermT patIn Pattern.assertEquivalent' (===) (from expected :: [Pattern RewritingVariableName]) @@ -325,9 +319,9 @@ test_inConcat = mkSet_ (HashSet.insert elem' values) & fromConcrete patElem = fromConcrete elem' patTrue = Test.Bool.asInternal True - predicate = mkEquals_ patTrue patIn - (===) (Test.Bool.asOrPattern True) =<< evaluateT patIn - evaluateExpectTopK predicate + predicate = fromEquals_ patTrue patIn + (===) (Test.Bool.asOrPattern True) =<< evaluateTermT patIn + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate ) test_concatUnit :: TestTree @@ -341,13 +335,13 @@ test_concatUnit = mkApplySymbol concatSetSymbol [patUnit, patValues] patConcat2 = mkApplySymbol concatSetSymbol [patValues, patUnit] - predicate1 = mkEquals_ patValues patConcat1 - predicate2 = mkEquals_ patValues patConcat2 - expect <- evaluateT patValues - (===) expect =<< evaluateT patConcat1 - (===) expect =<< evaluateT patConcat2 - evaluateExpectTopK predicate1 - evaluateExpectTopK predicate2 + predicate1 = fromEquals_ patValues patConcat1 + predicate2 = fromEquals_ patValues patConcat2 + expect <- evaluateTermT patValues + (===) expect =<< evaluateTermT patConcat1 + (===) expect =<< evaluateTermT patConcat2 + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate1 + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate2 ) test_concatAssociates :: TestTree @@ -370,11 +364,11 @@ test_concatAssociates = mkApplySymbol concatSetSymbol [patConcat12, patSet3] patConcat1_23 = mkApplySymbol concatSetSymbol [patSet1, patConcat23] - predicate = mkEquals_ patConcat12_3 patConcat1_23 - concat12_3 <- evaluateT patConcat12_3 - concat1_23 <- evaluateT patConcat1_23 + predicate = fromEquals_ patConcat12_3 patConcat1_23 + concat12_3 <- evaluateTermT patConcat12_3 + concat1_23 <- evaluateTermT patConcat1_23 (===) concat12_3 concat1_23 - evaluateExpectTopK predicate + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate ) test_concatNormalizes :: TestTree @@ -430,11 +424,11 @@ test_concatNormalizes = `with` OpaqueSet (mkElemVar setVar) patNormalized = asInternalNormalized normalized - predicate = mkEquals_ patConcat patNormalized - evalConcat <- evaluateT patConcat - evalNormalized <- evaluateT patNormalized + predicate = fromEquals_ patConcat patNormalized + evalConcat <- evaluateTermT patConcat + evalNormalized <- evaluateTermT patNormalized (===) evalConcat evalNormalized - evaluateExpectTopK predicate + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate ) test_difference :: TestTree @@ -450,10 +444,10 @@ test_difference = differenceSet (mkSet_ set1 & fromConcrete) (mkSet_ set2 & fromConcrete) - predicate = mkEquals_ patSet3 patDifference - expect <- evaluateT patSet3 - (===) expect =<< evaluateT patDifference - evaluateExpectTopK predicate + predicate = fromEquals_ patSet3 patDifference + expect <- evaluateTermT patSet3 + (===) expect =<< evaluateTermT patDifference + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate ) test_difference_symbolic :: [TestTree] @@ -540,10 +534,10 @@ test_toList = & mkSet_ actualList = mkApplySymbol toListSetSymbol [internalSet] - predicate = mkEquals_ expectedList actualList - expect <- evaluateT expectedList - (===) expect =<< evaluateT actualList - evaluateExpectTopK predicate + predicate = fromEquals_ expectedList actualList + expect <- evaluateTermT expectedList + (===) expect =<< evaluateTermT actualList + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate ) where implToList = @@ -564,10 +558,10 @@ test_size = patActual = mkApplySymbol sizeSetSymbol [mkSet_ set] & fromConcrete - predicate = mkEquals_ patExpected patActual - expect <- evaluateT patExpected - (===) expect =<< evaluateT patActual - evaluateExpectTopK predicate + predicate = fromEquals_ patExpected patActual + expect <- evaluateTermT patExpected + (===) expect =<< evaluateTermT patActual + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate ) test_intersection_unit :: TestTree @@ -576,8 +570,8 @@ test_intersection_unit = as <- forAll genSetPattern let original = intersectionSet as unitSet expect = OrPattern.fromTermLike $ asInternal HashSet.empty - (===) expect =<< evaluateT original - evaluateExpectTopK (mkEquals_ original unitSet) + (===) expect =<< evaluateTermT original + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT (fromEquals_ original unitSet) test_intersection_idem :: TestTree test_intersection_idem = @@ -586,8 +580,8 @@ test_intersection_idem = let termLike = mkSet_ as & fromConcrete original = intersectionSet termLike termLike expect = OrPattern.fromTermLike $ asInternal as - (===) expect =<< evaluateT original - evaluateExpectTopK (mkEquals_ original termLike) + (===) expect =<< evaluateTermT original + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT (fromEquals_ original termLike) test_list2set :: TestTree test_list2set = @@ -601,8 +595,9 @@ test_list2set = input = Test.List.asTermLike $ Test.Int.asInternal <$> someSeq original = list2setSet input expect = OrPattern.fromTermLike $ asInternal set - (===) expect =<< evaluateT original - evaluateExpectTopK (mkEquals_ original termLike) + (===) expect =<< evaluateTermT original + (===) (OrPattern.topOf kSort) + =<< evaluatePredicateT (fromEquals_ original termLike) test_inclusion :: [TestTree] test_inclusion = @@ -616,20 +611,20 @@ test_inclusion = patSet2 = concatSet patSet1 (elementSet patKey2) patInclusion = inclusionSet patSet1 patSet2 predicate = - mkImplies - (mkNot (mkEquals_ patKey1 patKey2)) - (mkEquals_ (Test.Bool.asInternal True) patInclusion) - (===) (Test.Bool.asOrPattern True) =<< evaluateT patInclusion - evaluateExpectTopK predicate + fromImplies + (fromNot (fromEquals_ patKey1 patKey2)) + (fromEquals_ (Test.Bool.asInternal True) patInclusion) + (===) (Test.Bool.asOrPattern True) =<< evaluateTermT patInclusion + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate ) , testPropertyWithSolver "SET.inclusion success: empty set <= any set" ( do patSomeSet <- forAll genSetPattern let patInclusion = inclusionSet unitSet patSomeSet - predicate = mkEquals_ (Test.Bool.asInternal True) patInclusion - (===) (Test.Bool.asOrPattern True) =<< evaluateT patInclusion - evaluateExpectTopK predicate + predicate = fromEquals_ (Test.Bool.asInternal True) patInclusion + (===) (Test.Bool.asOrPattern True) =<< evaluateTermT patInclusion + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate ) , testPropertyWithSolver "SET.inclusion failure: not (some nonempty set <= empty set)" @@ -637,9 +632,9 @@ test_inclusion = patKey <- forAll genIntegerPattern let patSomeSet = elementSet patKey patInclusion = inclusionSet patSomeSet unitSet - predicate = mkEquals_ (Test.Bool.asInternal False) patInclusion - (===) (Test.Bool.asOrPattern False) =<< evaluateT patInclusion - evaluateExpectTopK predicate + predicate = fromEquals_ (Test.Bool.asInternal False) patInclusion + (===) (Test.Bool.asOrPattern False) =<< evaluateTermT patInclusion + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate ) , testPropertyWithSolver "SET.inclusion failure: lhs key not included in rhs set" @@ -651,11 +646,11 @@ test_inclusion = patSet2 = concatSet patSet1 (elementSet patKey2) patInclusion = inclusionSet patSet2 patSet1 predicate = - mkImplies - (mkNot (mkEquals_ patKey1 patKey2)) - (mkEquals_ (Test.Bool.asInternal False) patInclusion) - (===) (Test.Bool.asOrPattern False) =<< evaluateT patInclusion - evaluateExpectTopK predicate + fromImplies + (fromNot (fromEquals_ patKey1 patKey2)) + (fromEquals_ (Test.Bool.asInternal False) patInclusion) + (===) (Test.Bool.asOrPattern False) =<< evaluateTermT patInclusion + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate ) ] @@ -685,7 +680,7 @@ test_symbolic = ) if HashSet.null values then discard - else (===) (MultiOr.singleton expect) =<< evaluateT patMap + else (===) (MultiOr.singleton expect) =<< evaluateTermT patMap ) -- | Construct a pattern for a map which may have symbolic keys. @@ -710,10 +705,10 @@ test_unifyConcreteIdem = ( do patSet <- forAll genSetPattern let patAnd = mkAnd patSet patSet - predicate = mkEquals_ patSet patAnd - expect <- evaluateT patSet - (===) expect =<< evaluateT patAnd - evaluateExpectTopK predicate + predicate = fromEquals_ patSet patAnd + expect <- evaluateTermT patSet + (===) expect =<< evaluateTermT patAnd + (===) (OrPattern.topOf kSort) =<< evaluatePredicateT predicate ) test_unifyConcreteDistinct :: TestTree @@ -728,9 +723,9 @@ test_unifyConcreteDistinct = patSet1 = mkSet_ set1 & fromConcrete patSet2 = mkSet_ set2 & fromConcrete conjunction = mkAnd patSet1 patSet2 - predicate = mkEquals_ patSet1 conjunction - (===) OrPattern.bottom =<< evaluateT conjunction - (===) OrPattern.bottom =<< evaluateT predicate + predicate = fromEquals_ patSet1 conjunction + (===) OrPattern.bottom =<< evaluateTermT conjunction + (===) OrPattern.bottom =<< evaluatePredicateT predicate ) test_unifyFramingVariable :: TestTree @@ -859,7 +854,7 @@ test_unifySelectFromEmpty = doesNotUnifyWith pat1 pat2 = do annotateShow pat1 annotateShow pat2 - (===) OrPattern.bottom =<< evaluateT (mkAnd pat1 pat2) + (===) OrPattern.bottom =<< evaluateTermT (mkAnd pat1 pat2) test_unifySelectFromSingleton :: TestTree test_unifySelectFromSingleton = @@ -1892,7 +1887,7 @@ return a partial result for unifying the second element of the pair. test_concretizeKeys :: TestTree test_concretizeKeys = testCaseWithoutSMT "unify Set with symbolic keys" $ do - actual <- evaluate original + actual <- evaluateTerm original assertEqual "" expected actual where x = @@ -1941,7 +1936,7 @@ return a partial result for unifying the second element of the pair. test_concretizeKeysAxiom :: TestTree test_concretizeKeysAxiom = testCaseWithoutSMT "unify Set with symbolic keys in axiom" $ do - config <- evaluate $ pair symbolicKey concreteSet + config <- evaluateTerm $ pair symbolicKey concreteSet actual <- MultiOr.traverse (flip runStep axiom) config assertEqual "" expected (MultiOr.flatten actual) where diff --git a/kore/test/Test/Kore/Builtin/String.hs b/kore/test/Test/Kore/Builtin/String.hs index 3c2614f34c..1a789717d9 100644 --- a/kore/test/Test/Kore/Builtin/String.hs +++ b/kore/test/Test/Kore/Builtin/String.hs @@ -73,7 +73,7 @@ testComparison name impl symb = a <- forAll genString b <- forAll genString let expect = Test.Bool.asOrPattern $ impl a b - actual <- evaluateT $ mkApplySymbol symb (asInternal <$> [a, b]) + actual <- evaluateTermT $ mkApplySymbol symb (asInternal <$> [a, b]) (===) expect actual test_eq :: TestTree @@ -446,7 +446,7 @@ testString :: [TermLike RewritingVariableName] -> OrPattern RewritingVariableName -> TestTree -testString name = testSymbolWithoutSolver evaluate name +testString name = testSymbolWithoutSolver evaluateTerm name ofSort :: Text.Text -> Sort -> ElementVariable RewritingVariableName idName `ofSort` sort = configElementVariableFromId (testId idName) sort diff --git a/kore/test/Test/Kore/Reachability/MockAllPath.hs b/kore/test/Test/Kore/Reachability/MockAllPath.hs index 906c1c2c90..754b9529dc 100644 --- a/kore/test/Test/Kore/Reachability/MockAllPath.hs +++ b/kore/test/Test/Kore/Reachability/MockAllPath.hs @@ -415,8 +415,8 @@ instance MonadCatch AllPathIdentity where instance MonadSimplify AllPathIdentity where askMetadataTools = undefined - simplifyTermLike = undefined - simplifyTermLikeOnly = undefined + simplifyPattern = undefined + simplifyTerm = undefined simplifyCondition = undefined askSimplifierAxioms = undefined localSimplifierAxioms = undefined diff --git a/kore/test/Test/Kore/Rewrite/Rule/Simplify.hs b/kore/test/Test/Kore/Rewrite/Rule/Simplify.hs index c10f2e2175..20d2a7018f 100644 --- a/kore/test/Test/Kore/Rewrite/Rule/Simplify.hs +++ b/kore/test/Test/Kore/Rewrite/Rule/Simplify.hs @@ -478,7 +478,7 @@ instance MFunctor TestSimplifierT where hoist f = TestSimplifierT . hoist f . runTestSimplifierT instance MonadSimplify m => MonadSimplify (TestSimplifierT m) where - simplifyTermLike sideCondition termLike = do + simplifyTerm sideCondition termLike = do TestEnv{replacements, input, requires} <- Reader.ask let rule = getOnePathClaim input leftTerm = diff --git a/kore/test/Test/Kore/Simplify/Integration.hs b/kore/test/Test/Kore/Simplify/Integration.hs index dff3771c2b..074d7ea8ba 100644 --- a/kore/test/Test/Kore/Simplify/Integration.hs +++ b/kore/test/Test/Kore/Simplify/Integration.hs @@ -22,8 +22,6 @@ import Kore.Equation ( ) import qualified Kore.Equation as Equation import qualified Kore.Internal.Condition as Condition -import Kore.Internal.From -import qualified Kore.Internal.MultiAnd as MultiAnd import Kore.Internal.SideCondition ( SideCondition, ) @@ -57,7 +55,6 @@ import qualified Kore.Simplify.Pattern as Pattern ( import Kore.Simplify.Simplify import Kore.Unparser import Prelude.Kore -import qualified Pretty import Test.Kore import Test.Kore.Equation.Common ( functionAxiomUnification, @@ -529,70 +526,6 @@ test_simplificationIntegration = , substitution = mempty } assertEqual "" expected actual - , testCase "Or to pattern" $ do - let expected = - ( OrPattern.fromPatterns - . map - ( Pattern.fromCondition Mock.boolSort - . Condition.fromPredicate - . Predicate.fromMultiAnd - . MultiAnd.make - ) - ) - [ - [ fromImplies (fromAnd cfCeil cgCeil) chCeil - , fromImplies cfCeil chCeil - , fromImplies chCeil (fromAnd cfCeil cgCeil) - ] - , - [ fromImplies (fromAnd cfCeil cgCeil) chCeil - , fromImplies cfCeil chCeil - , fromImplies chCeil cfCeil - ] - ] - -- Uncomment when using the new Iff simplifier: - -- ( OrPattern.fromPatterns - -- . map - -- ( Pattern.fromCondition Mock.boolSort - -- . Condition.fromPredicate - -- . Predicate.fromMultiAnd - -- . MultiAnd.make - -- ) - -- ) - -- [ [fromNot cfCeil, fromNot chCeil] - -- , [chCeil, cgCeil, cfCeil] - -- , [chCeil, cfCeil, fromNot cgCeil] - -- ] - cfCeil = makeCeilPredicate Mock.cf - cgCeil = makeCeilPredicate Mock.cg - chCeil = makeCeilPredicate Mock.ch - actual <- - evaluate - Conditional - { term = - mkIff - ( mkIn - Mock.boolSort - ((mkCeil Mock.setSort) Mock.cf) - ( mkOr - Mock.unitSet - ((mkCeil Mock.setSort) Mock.cg) - ) - ) - ((mkCeil Mock.boolSort) Mock.ch) - , predicate = makeTruePredicate - , substitution = mempty - } - let message = - (show . Pretty.vsep) - [ "Expected:" - , (Pretty.indent 4 . Pretty.vsep) - (map unparse . toList $ expected) - , "but found:" - , (Pretty.indent 4 . Pretty.vsep) - (map unparse . toList $ actual) - ] - assertEqual message expected actual , testCase "Builtin and simplification failure" $ do let m = mkSetVariable (testId "m") Mock.listSort @@ -632,9 +565,9 @@ test_simplificationIntegration = assertBool "Expected simplified term" (TermLike.isSimplified sideRepresentation term) assertBool (unlines ["Expected simplified condition:", message]) (Condition.isSimplified sideRepresentation condition) assertBool message (Pattern.isSimplified sideRepresentation pattern') - , testCase "Equals-in simplification" $ do + , testCase "Nu-And simplification" $ do let gt = - mkSetVariable (testId "gt") Mock.stringSort + mkSetVariable (testId "gt") Mock.testSort1 & mapSetVariable (pure mkConfigVariable) g = mkSetVariable (testId "g") Mock.testSort1 @@ -645,12 +578,12 @@ test_simplificationIntegration = { term = mkNu gt - ( (mkEquals Mock.stringSort) - ( (mkIn Mock.listSort) + ( mkAnd + ( mkAnd (mkTop Mock.testSort1) (mkNu g (mkOr Mock.aSort1 (mkSetVar g))) ) - (mkTop Mock.listSort) + (mkTop Mock.testSort1) ) , predicate = makeTruePredicate , substitution = mempty @@ -668,36 +601,31 @@ test_simplificationIntegration = , substitution = mempty } assertBool "" (OrPattern.isSimplified sideRepresentation actual) - , testCase "Distributed equals simplification" $ do + , testCase "Nu over distributed and simplification" $ do let k = - mkSetVariable (testId "k") Mock.stringSort + mkSetVariable (testId "k") Mock.testSort & mapSetVariable (pure mkConfigVariable) actual <- evaluate - Conditional - { term = - mkMu - k - ( (mkEquals Mock.stringSort) - (Mock.functionalConstr21 Mock.cf Mock.cf) - (Mock.functionalConstr21 Mock.ch Mock.cg) - ) - , predicate = makeTruePredicate - , substitution = mempty - } + ( mkMu + k + ( mkAnd + (Mock.functionalConstr21 Mock.cf Mock.cf) + (Mock.functionalConstr21 Mock.ch Mock.cg) + ) + & Pattern.fromTermLike + ) assertBool "" (OrPattern.isSimplified sideRepresentation actual) - , testCase "nu-floor-in-or simplification" $ do + , testCase "nu-not-and-or simplification" $ do let q = - mkSetVariable (testId "q") Mock.otherSort + mkSetVariable (testId "q") Mock.testSort & mapSetVariable (pure mkConfigVariable) actual <- evaluate ( mkNu q - ( mkFloor - Mock.otherSort - ( mkIn - Mock.otherSort + ( mkNot + ( mkAnd (Mock.g Mock.ch) (mkOr Mock.cf Mock.cg) ) diff --git a/kore/test/Test/Kore/Simplify/TermLike.hs b/kore/test/Test/Kore/Simplify/TermLike.hs index 80a7f70e72..fbdeda6300 100644 --- a/kore/test/Test/Kore/Simplify/TermLike.hs +++ b/kore/test/Test/Kore/Simplify/TermLike.hs @@ -125,9 +125,9 @@ instance MonadSimplify TestSimplifier where TestSimplifier (simplifyCondition sideCondition condition) - -- Throw an error if any term would be simplified. - simplifyTermLike = undefined - simplifyTermLikeOnly = undefined + -- Throw an error if any pattern/term would be simplified. + simplifyPattern = undefined + simplifyTerm = undefined test_simplifyOnly :: [TestTree] test_simplifyOnly = @@ -172,7 +172,7 @@ test_simplifyOnly = test testName input maybeExpect = testCase testName $ do let expect = fromMaybe (OrPattern.fromTermLike input) maybeExpect - actual <- simplifyOnly input + actual <- simplify input let message = (show . Pretty.vsep) [ "Expected:" @@ -189,9 +189,9 @@ test_simplifyOnly = SideCondition.mkRepresentation (SideCondition.top @RewritingVariableName) -simplifyOnly :: +simplify :: TermLike RewritingVariableName -> IO (OrPattern RewritingVariableName) -simplifyOnly = +simplify = runSimplifier Mock.env - . TermLike.simplifyOnly SideCondition.top + . TermLike.simplify SideCondition.top