From 0741a1b994e8733eac5080d6382127782cfb1be0 Mon Sep 17 00:00:00 2001 From: andreiburdusa Date: Fri, 22 May 2020 12:11:21 +0300 Subject: [PATCH 1/3] Add SideCondition argument to simplifyAnds --- .../Simplification/SubstitutionSimplifier.hs | 16 ++++++++-------- kore/test/Test/Kore/Unification/Unifier.hs | 2 +- 2 files changed, 9 insertions(+), 9 deletions(-) diff --git a/kore/src/Kore/Step/Simplification/SubstitutionSimplifier.hs b/kore/src/Kore/Step/Simplification/SubstitutionSimplifier.hs index d7db4b3ada..bbe29972ee 100644 --- a/kore/src/Kore/Step/Simplification/SubstitutionSimplifier.hs +++ b/kore/src/Kore/Step/Simplification/SubstitutionSimplifier.hs @@ -75,7 +75,6 @@ import Kore.Internal.SideCondition ) import qualified Kore.Internal.SideCondition as SideCondition ( toRepresentation - , topTODO ) import Kore.Internal.Substitution ( Assignment @@ -179,10 +178,11 @@ simplifyAnds . ( InternalVariable variable , Monad monad ) - => MakeAnd monad + => SideCondition variable + -> MakeAnd monad -> NonEmpty (TermLike variable) -> monad (Pattern variable) -simplifyAnds MakeAnd { makeAnd } (NonEmpty.sort -> patterns) = +simplifyAnds sideCondition MakeAnd { makeAnd } (NonEmpty.sort -> patterns) = foldM simplifyAnds' Pattern.top patterns where simplifyAnds' @@ -194,7 +194,6 @@ simplifyAnds MakeAnd { makeAnd } (NonEmpty.sort -> patterns) = AndF And { andFirst, andSecond } -> foldM simplifyAnds' intermediate [andFirst, andSecond] _ -> do - let sideCondition = SideCondition.topTODO simplified <- makeAnd intermediateTerm @@ -210,13 +209,14 @@ deduplicateSubstitution . ( InternalVariable variable , Monad monad ) - => MakeAnd monad + => SideCondition variable + -> MakeAnd monad -> Substitution variable -> monad ( Predicate variable , Map (UnifiedVariable variable) (TermLike variable) ) -deduplicateSubstitution makeAnd' = +deduplicateSubstitution sideCondition makeAnd' = worker Predicate.makeTruePredicate_ . checkSetVars . Substitution.toMultiMap where checkSetVars m @@ -228,7 +228,7 @@ deduplicateSubstitution makeAnd' = (\k v -> Any $ isSetVar k && isNotSingleton v) isNotSingleton = isNothing . getSingleton - simplifyAnds' = simplifyAnds makeAnd' + simplifyAnds' = simplifyAnds sideCondition makeAnd' worker :: Predicate variable @@ -373,7 +373,7 @@ simplifySubstitutionWorker sideCondition makeAnd' = \substitution -> do (Map (UnifiedVariable variable) (TermLike variable)) deduplicate substitution = do (predicate, substitution') <- - deduplicateSubstitution makeAnd' substitution + deduplicateSubstitution sideCondition makeAnd' substitution & lift . lift addPredicate predicate return substitution' diff --git a/kore/test/Test/Kore/Unification/Unifier.hs b/kore/test/Test/Kore/Unification/Unifier.hs index c502bc8f96..37d8fb64d5 100644 --- a/kore/test/Test/Kore/Unification/Unifier.hs +++ b/kore/test/Test/Kore/Unification/Unifier.hs @@ -193,7 +193,7 @@ simplifyAnds => NonEmpty (TermLike Variable) -> unifier (Pattern Variable) simplifyAnds = - SubstitutionSimplifier.simplifyAnds + SubstitutionSimplifier.simplifyAnds SideCondition.top (Unification.unificationMakeAnd Not.notSimplifier) andSimplifySuccess From 68829389734d4f8556700e37e3283fb7c603043b Mon Sep 17 00:00:00 2001 From: andreiburdusa Date: Fri, 22 May 2020 12:20:33 +0300 Subject: [PATCH 2/3] stylish --- kore/src/Kore/Step/Simplification/SubstitutionSimplifier.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kore/src/Kore/Step/Simplification/SubstitutionSimplifier.hs b/kore/src/Kore/Step/Simplification/SubstitutionSimplifier.hs index bbe29972ee..a55af03f4c 100644 --- a/kore/src/Kore/Step/Simplification/SubstitutionSimplifier.hs +++ b/kore/src/Kore/Step/Simplification/SubstitutionSimplifier.hs @@ -209,7 +209,7 @@ deduplicateSubstitution . ( InternalVariable variable , Monad monad ) - => SideCondition variable + => SideCondition variable -> MakeAnd monad -> Substitution variable -> monad From 2fad079551bd4aa0c71fa85809e7903bab015be1 Mon Sep 17 00:00:00 2001 From: andreiburdusa Date: Fri, 22 May 2020 18:41:25 +0300 Subject: [PATCH 3/3] Addressed comments --- .../Step/Simplification/SubstitutionSimplifier.hs | 12 ++++++------ kore/test/Test/Kore/Unification/Unifier.hs | 3 ++- 2 files changed, 8 insertions(+), 7 deletions(-) diff --git a/kore/src/Kore/Step/Simplification/SubstitutionSimplifier.hs b/kore/src/Kore/Step/Simplification/SubstitutionSimplifier.hs index a55af03f4c..9426ce20f9 100644 --- a/kore/src/Kore/Step/Simplification/SubstitutionSimplifier.hs +++ b/kore/src/Kore/Step/Simplification/SubstitutionSimplifier.hs @@ -178,11 +178,11 @@ simplifyAnds . ( InternalVariable variable , Monad monad ) - => SideCondition variable - -> MakeAnd monad + => MakeAnd monad + -> SideCondition variable -> NonEmpty (TermLike variable) -> monad (Pattern variable) -simplifyAnds sideCondition MakeAnd { makeAnd } (NonEmpty.sort -> patterns) = +simplifyAnds MakeAnd { makeAnd } sideCondition (NonEmpty.sort -> patterns) = foldM simplifyAnds' Pattern.top patterns where simplifyAnds' @@ -209,8 +209,8 @@ deduplicateSubstitution . ( InternalVariable variable , Monad monad ) - => SideCondition variable - -> MakeAnd monad + => MakeAnd monad + -> SideCondition variable -> Substitution variable -> monad ( Predicate variable @@ -373,7 +373,7 @@ simplifySubstitutionWorker sideCondition makeAnd' = \substitution -> do (Map (UnifiedVariable variable) (TermLike variable)) deduplicate substitution = do (predicate, substitution') <- - deduplicateSubstitution sideCondition makeAnd' substitution + deduplicateSubstitution makeAnd' sideCondition substitution & lift . lift addPredicate predicate return substitution' diff --git a/kore/test/Test/Kore/Unification/Unifier.hs b/kore/test/Test/Kore/Unification/Unifier.hs index 37d8fb64d5..7f292cfe8c 100644 --- a/kore/test/Test/Kore/Unification/Unifier.hs +++ b/kore/test/Test/Kore/Unification/Unifier.hs @@ -193,8 +193,9 @@ simplifyAnds => NonEmpty (TermLike Variable) -> unifier (Pattern Variable) simplifyAnds = - SubstitutionSimplifier.simplifyAnds SideCondition.top + SubstitutionSimplifier.simplifyAnds (Unification.unificationMakeAnd Not.notSimplifier) + SideCondition.top andSimplifySuccess :: HasCallStack