runtimeverification · ana-pantilie · Sep 16, 2020 · Sep 9, 2020 · Sep 10, 2020 · Sep 10, 2020
diff --git a/kore/src/Kore/Internal/MultiOr.hs b/kore/src/Kore/Internal/MultiOr.hs
@@ -12,7 +12,7 @@ Portability : portable
 {-# LANGUAGE UndecidableInstances #-}
 
 module Kore.Internal.MultiOr
-    ( MultiOr (..)
+    ( MultiOr
     , bottom
     , filterOr
     , flatten

diff --git a/kore/src/Kore/Step/Simplification/Not.hs b/kore/src/Kore/Step/Simplification/Not.hs
@@ -32,7 +32,7 @@ import Kore.Internal.MultiAnd
     )
 import qualified Kore.Internal.MultiAnd as MultiAnd
 import Kore.Internal.MultiOr
-    ( MultiOr (..)
+    ( MultiOr
     )
 import qualified Kore.Internal.MultiOr as MultiOr
 import Kore.Internal.OrCondition

diff --git a/kore/src/Kore/Strategies/Goal.hs b/kore/src/Kore/Strategies/Goal.hs
@@ -162,7 +162,7 @@ import Kore.Strategies.Rule
 import qualified Kore.Syntax.Sentence as Syntax
 import Kore.Syntax.Variable
 import Kore.TopBottom
-    ( isBottom
+    ( TopBottom (..)
     )
 import qualified Kore.Unification.Procedure as Unification
 import Kore.Unparser
@@ -184,18 +184,22 @@ See also: 'Strategy.pickFinal', 'extractUnproven'
  -}
 unprovenNodes
     :: forall goal a
-    .  Strategy.ExecutionGraph (ProofState a) (AppliedRule goal)
+    .  Ord a
+    => TopBottom a
+    => Strategy.ExecutionGraph (ProofState a) (AppliedRule goal)
     -> MultiOr.MultiOr a
 unprovenNodes executionGraph =
-    MultiOr.MultiOr
+    MultiOr.make
     $ mapMaybe extractUnproven
     $ Strategy.pickFinal executionGraph
 
 {- | Does the 'Strategy.ExecutionGraph' indicate a successful proof?
  -}
 proven
     :: forall goal a
-    .  Strategy.ExecutionGraph (ProofState a) (AppliedRule goal)
+    .  Ord a
+    => TopBottom a
+    => Strategy.ExecutionGraph (ProofState a) (AppliedRule goal)
     -> Bool
 proven = Foldable.null . unprovenNodes
 

diff --git a/kore/test/Test/Kore/Builtin/Map.hs b/kore/test/Test/Kore/Builtin/Map.hs
@@ -90,9 +90,7 @@ import Kore.Domain.Builtin
     ( NormalizedMap (..)
     )
 import qualified Kore.Domain.Builtin as Domain
-import Kore.Internal.MultiOr
-    ( MultiOr (..)
-    )
+import qualified Kore.Internal.MultiOr as MultiOr
 import Kore.Internal.Pattern
 import qualified Kore.Internal.Pattern as Pattern
 import Kore.Internal.Predicate
@@ -1223,7 +1221,7 @@ test_concretizeKeysAxiom =
             , rhs = injectTermIntoRHS v
             , attributes = Default.def
             }
-    expected = MultiOr
+    expected = MultiOr.make
         [ Conditional
             { term = val
             , predicate = makeTruePredicate intSort

diff --git a/kore/test/Test/Kore/Builtin/Set.hs b/kore/test/Test/Kore/Builtin/Set.hs
@@ -98,9 +98,7 @@ import Kore.Domain.Builtin
 import qualified Kore.Domain.Builtin as Domain
 import qualified Kore.Internal.Condition as Condition
 import qualified Kore.Internal.Conditional as Conditional
-import Kore.Internal.MultiOr
-    ( MultiOr (..)
-    )
+import qualified Kore.Internal.MultiOr as MultiOr
 import Kore.Internal.Pattern as Pattern
 import Kore.Internal.Predicate as Predicate
 import qualified Kore.Internal.Substitution as Substitution
@@ -1824,7 +1822,7 @@ test_concretizeKeysAxiom =
             , rhs = injectTermIntoRHS x
             , attributes = Default.def
             }
-    expected = MultiOr
+    expected = MultiOr.make
         [ Conditional
             { term = symbolicKey
             , predicate = makeTruePredicate intSort

diff --git a/kore/test/Test/Kore/Step/Simplification/And.hs b/kore/test/Test/Kore/Step/Simplification/And.hs
@@ -8,9 +8,7 @@ import Test.Tasty
 
 import qualified Kore.Internal.Condition as Condition
 import qualified Kore.Internal.MultiAnd as MultiAnd
-import Kore.Internal.MultiOr
-    ( MultiOr (MultiOr)
-    )
+import qualified Kore.Internal.MultiOr as MultiOr
 import Kore.Internal.OrPattern
     ( OrPattern
     )
@@ -276,7 +274,7 @@ test_andSimplification =
                             [(inject Mock.y, fOfX)]
                         }
             actual <- evaluatePatterns yExpanded fOfXExpanded
-            assertEqual "" (MultiOr [expect]) actual
+            assertEqual "" (MultiOr.make [expect]) actual
 
         , testCase "term-variable" $ do
             let expect =
@@ -287,7 +285,7 @@ test_andSimplification =
                             [(inject Mock.y, fOfX)]
                         }
             actual <- evaluatePatterns fOfXExpanded yExpanded
-            assertEqual "" (MultiOr [expect]) actual
+            assertEqual "" (MultiOr.make [expect]) actual
         ]
 
     , testGroup "constructor and"
@@ -310,7 +308,7 @@ test_andSimplification =
                         , predicate = makeTruePredicate_
                         , substitution = mempty
                         }
-            assertEqual "" (MultiOr [expect]) actual
+            assertEqual "" (MultiOr.make [expect]) actual
 
         , testCase "different constructors" $ do
             actual <-
@@ -325,7 +323,7 @@ test_andSimplification =
                         , predicate = makeTruePredicate_
                         , substitution = mempty
                         }
-            assertEqual "" (MultiOr []) actual
+            assertEqual "" (MultiOr.make []) actual
         ]
 
     -- (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 =
                     , predicate = makeCeilPredicate_ fOfX
                     , substitution = mempty
                     }
-        assertEqual "" (MultiOr [expect]) actual
+        assertEqual "" (MultiOr.make [expect]) actual
     , testCase "Contradictions result in bottom" $ do
         actual <-
             evaluatePatterns
@@ -436,7 +434,7 @@ test_andSimplification =
                         (makeCeilPredicate_ gOfX)
                     , substitution = mempty
                     }
-        assertEqual "" (MultiOr [expect]) actual
+        assertEqual "" (MultiOr.make [expect]) actual
     , testCase "Simplifies Implies - Negative" $ do
         let expect =
                 Conditional
@@ -462,7 +460,7 @@ test_andSimplification =
                             (makeCeilPredicate_ gOfX)
                     , substitution = mempty
                     }
-        assertEqual "" (MultiOr [expect]) actual
+        assertEqual "" (MultiOr.make [expect]) actual
     , testCase "Simplifies multiple Implies" $ do
         let expect =
                 Conditional
@@ -497,7 +495,7 @@ test_andSimplification =
                             )
                     , substitution = mempty
                     }
-        assertEqual "" (MultiOr [expect]) actual
+        assertEqual "" (MultiOr.make [expect]) actual
     , testCase "Does not replace and terms under intersecting quantifiers" $ do
         let expect =
                 Conditional
@@ -523,7 +521,7 @@ test_andSimplification =
                         makeExistsPredicate Mock.x (makeCeilPredicate_ fOfX)
                     , substitution = mempty
                     }
-        assertEqual "" (MultiOr [expect]) actual
+        assertEqual "" (MultiOr.make [expect]) actual
     , testCase "Replaces and terms under independent quantifiers" $ do
         let expect =
                 Conditional
@@ -553,7 +551,7 @@ test_andSimplification =
                             )
                     , substitution = mempty
                     }
-        assertEqual "" (MultiOr [expect]) actual
+        assertEqual "" (MultiOr.make [expect]) actual
     ]
   where
     yExpanded = Conditional