Skip to content

Commit 6ab0ba3

Browse files
ana-pantiliettuegel
ana-pantilie
and
ttuegel
authored
Do not export constructor of MultiOr (#2148)
* WIP: remove Functor instance from MultiOr * WIP: remove Functor instance from MultiOr * WIP: remove Functor instance from MultiOr * Simplification.Inj: refactor awkward map of MultiOr * WIP: remove Functor instance from MultiOr * WIP: remove Functor instance from MultiOr * Simplification.Builtin: use Logic monad instead of MultiOr as a monad * WIP: remove Functor instance from MultiOr * WIP: remove Functor instance of Result * Remove Functor instance from Result * MultiOr: traverseLogic * MultiOr: reimplement fullCrossProduct in terms of MultiAnd and MultiOr * Use old fullCrossProduct in Application simplification * MultiOr: split fullCrossProduct into distributeAnd and distributeApplication * Use MultiOr.traverse * test_distributeAnd + test_distributeApplication * WIP Address review comments * Update kore/src/Kore/Step/Simplification/Implies.hs Co-authored-by: Thomas Tuegel <[email protected]> * Update kore/src/Kore/Step/Simplification/In.hs Co-authored-by: Thomas Tuegel <[email protected]> * Update kore/src/Kore/Syntax/DomainValue.hs Co-authored-by: Thomas Tuegel <[email protected]> * Update kore/src/Kore/Internal/Inj.hs Co-authored-by: Thomas Tuegel <[email protected]> * Address review comments * Address review comment * MultiOr: do not export constructor Co-authored-by: Thomas Tuegel <[email protected]>
1 parent a65726e commit 6ab0ba3

File tree

7 files changed

+123
-88
lines changed

7 files changed

+123
-88
lines changed

‎kore/src/Kore/Internal/MultiOr.hs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ Portability : portable
1212
{-# LANGUAGE UndecidableInstances #-}
1313

1414
module Kore.Internal.MultiOr
15-
( MultiOr (..)
15+
( MultiOr
1616
, bottom
1717
, filterOr
1818
, flatten

‎kore/src/Kore/Step/Simplification/Not.hs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -32,7 +32,7 @@ import Kore.Internal.MultiAnd
3232
)
3333
import qualified Kore.Internal.MultiAnd as MultiAnd
3434
import Kore.Internal.MultiOr
35-
( MultiOr (..)
35+
( MultiOr
3636
)
3737
import qualified Kore.Internal.MultiOr as MultiOr
3838
import Kore.Internal.OrCondition

‎kore/src/Kore/Strategies/Goal.hs‎

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -162,7 +162,7 @@ import Kore.Strategies.Rule
162162
import qualified Kore.Syntax.Sentence as Syntax
163163
import Kore.Syntax.Variable
164164
import Kore.TopBottom
165-
( isBottom
165+
( TopBottom (..)
166166
)
167167
import qualified Kore.Unification.Procedure as Unification
168168
import Kore.Unparser
@@ -184,18 +184,22 @@ See also: 'Strategy.pickFinal', 'extractUnproven'
184184
-}
185185
unprovenNodes
186186
:: forall goal a
187-
. Strategy.ExecutionGraph (ProofState a) (AppliedRule goal)
187+
. Ord a
188+
=> TopBottom a
189+
=> Strategy.ExecutionGraph (ProofState a) (AppliedRule goal)
188190
-> MultiOr.MultiOr a
189191
unprovenNodes executionGraph =
190-
MultiOr.MultiOr
192+
MultiOr.make
191193
$ mapMaybe extractUnproven
192194
$ Strategy.pickFinal executionGraph
193195

194196
{- | Does the 'Strategy.ExecutionGraph' indicate a successful proof?
195197
-}
196198
proven
197199
:: forall goal a
198-
. Strategy.ExecutionGraph (ProofState a) (AppliedRule goal)
200+
. Ord a
201+
=> TopBottom a
202+
=> Strategy.ExecutionGraph (ProofState a) (AppliedRule goal)
199203
-> Bool
200204
proven = Foldable.null . unprovenNodes
201205

‎kore/test/Test/Kore/Builtin/Map.hs‎

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -90,9 +90,7 @@ import Kore.Domain.Builtin
9090
( NormalizedMap (..)
9191
)
9292
import qualified Kore.Domain.Builtin as Domain
93-
import Kore.Internal.MultiOr
94-
( MultiOr (..)
95-
)
93+
import qualified Kore.Internal.MultiOr as MultiOr
9694
import Kore.Internal.Pattern
9795
import qualified Kore.Internal.Pattern as Pattern
9896
import Kore.Internal.Predicate
@@ -1223,7 +1221,7 @@ test_concretizeKeysAxiom =
12231221
, rhs = injectTermIntoRHS v
12241222
, attributes = Default.def
12251223
}
1226-
expected = MultiOr
1224+
expected = MultiOr.make
12271225
[ Conditional
12281226
{ term = val
12291227
, predicate = makeTruePredicate intSort

‎kore/test/Test/Kore/Builtin/Set.hs‎

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -98,9 +98,7 @@ import Kore.Domain.Builtin
9898
import qualified Kore.Domain.Builtin as Domain
9999
import qualified Kore.Internal.Condition as Condition
100100
import qualified Kore.Internal.Conditional as Conditional
101-
import Kore.Internal.MultiOr
102-
( MultiOr (..)
103-
)
101+
import qualified Kore.Internal.MultiOr as MultiOr
104102
import Kore.Internal.Pattern as Pattern
105103
import Kore.Internal.Predicate as Predicate
106104
import qualified Kore.Internal.Substitution as Substitution
@@ -1824,7 +1822,7 @@ test_concretizeKeysAxiom =
18241822
, rhs = injectTermIntoRHS x
18251823
, attributes = Default.def
18261824
}
1827-
expected = MultiOr
1825+
expected = MultiOr.make
18281826
[ Conditional
18291827
{ term = symbolicKey
18301828
, predicate = makeTruePredicate intSort

‎kore/test/Test/Kore/Step/Simplification/And.hs‎

Lines changed: 11 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -8,9 +8,7 @@ import Test.Tasty
88

99
import qualified Kore.Internal.Condition as Condition
1010
import qualified Kore.Internal.MultiAnd as MultiAnd
11-
import Kore.Internal.MultiOr
12-
( MultiOr (MultiOr)
13-
)
11+
import qualified Kore.Internal.MultiOr as MultiOr
1412
import Kore.Internal.OrPattern
1513
( OrPattern
1614
)
@@ -276,7 +274,7 @@ test_andSimplification =
276274
[(inject Mock.y, fOfX)]
277275
}
278276
actual <- evaluatePatterns yExpanded fOfXExpanded
279-
assertEqual "" (MultiOr [expect]) actual
277+
assertEqual "" (MultiOr.make [expect]) actual
280278

281279
, testCase "term-variable" $ do
282280
let expect =
@@ -287,7 +285,7 @@ test_andSimplification =
287285
[(inject Mock.y, fOfX)]
288286
}
289287
actual <- evaluatePatterns fOfXExpanded yExpanded
290-
assertEqual "" (MultiOr [expect]) actual
288+
assertEqual "" (MultiOr.make [expect]) actual
291289
]
292290

293291
, testGroup "constructor and"
@@ -310,7 +308,7 @@ test_andSimplification =
310308
, predicate = makeTruePredicate_
311309
, substitution = mempty
312310
}
313-
assertEqual "" (MultiOr [expect]) actual
311+
assertEqual "" (MultiOr.make [expect]) actual
314312

315313
, testCase "different constructors" $ do
316314
actual <-
@@ -325,7 +323,7 @@ test_andSimplification =
325323
, predicate = makeTruePredicate_
326324
, substitution = mempty
327325
}
328-
assertEqual "" (MultiOr []) actual
326+
assertEqual "" (MultiOr.make []) actual
329327
]
330328

331329
-- (a or b) and (c or d) = (b and d) or (b and c) or (a and d) or (a and c)
@@ -395,7 +393,7 @@ test_andSimplification =
395393
, predicate = makeCeilPredicate_ fOfX
396394
, substitution = mempty
397395
}
398-
assertEqual "" (MultiOr [expect]) actual
396+
assertEqual "" (MultiOr.make [expect]) actual
399397
, testCase "Contradictions result in bottom" $ do
400398
actual <-
401399
evaluatePatterns
@@ -436,7 +434,7 @@ test_andSimplification =
436434
(makeCeilPredicate_ gOfX)
437435
, substitution = mempty
438436
}
439-
assertEqual "" (MultiOr [expect]) actual
437+
assertEqual "" (MultiOr.make [expect]) actual
440438
, testCase "Simplifies Implies - Negative" $ do
441439
let expect =
442440
Conditional
@@ -462,7 +460,7 @@ test_andSimplification =
462460
(makeCeilPredicate_ gOfX)
463461
, substitution = mempty
464462
}
465-
assertEqual "" (MultiOr [expect]) actual
463+
assertEqual "" (MultiOr.make [expect]) actual
466464
, testCase "Simplifies multiple Implies" $ do
467465
let expect =
468466
Conditional
@@ -497,7 +495,7 @@ test_andSimplification =
497495
)
498496
, substitution = mempty
499497
}
500-
assertEqual "" (MultiOr [expect]) actual
498+
assertEqual "" (MultiOr.make [expect]) actual
501499
, testCase "Does not replace and terms under intersecting quantifiers" $ do
502500
let expect =
503501
Conditional
@@ -523,7 +521,7 @@ test_andSimplification =
523521
makeExistsPredicate Mock.x (makeCeilPredicate_ fOfX)
524522
, substitution = mempty
525523
}
526-
assertEqual "" (MultiOr [expect]) actual
524+
assertEqual "" (MultiOr.make [expect]) actual
527525
, testCase "Replaces and terms under independent quantifiers" $ do
528526
let expect =
529527
Conditional
@@ -553,7 +551,7 @@ test_andSimplification =
553551
)
554552
, substitution = mempty
555553
}
556-
assertEqual "" (MultiOr [expect]) actual
554+
assertEqual "" (MultiOr.make [expect]) actual
557555
]
558556
where
559557
yExpanded = Conditional

0 commit comments

Comments
 (0)