fix unit tests

runtimeverification · Aug 16, 2024 · 743d5f8 · 743d5f8
1 parent c07c357
commit 743d5f8
Show file tree

Hide file tree

Showing 2 changed files with 18 additions and 41 deletions.
diff --git a/booster/unit-tests/Test/Booster/Pattern/Rewrite.hs b/booster/unit-tests/Test/Booster/Pattern/Rewrite.hs
@@ -83,66 +83,46 @@ rule1, rule1', rule2, rule3, rule4 :: RewriteRule "Rewrite"
 rule1 =
     rule
         (Just "con1-f1")
-        ( Pattern_
-            [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( con1{}( \dv{SomeSort{}}("thing") ) ), RuleVar:SortK{}) ) |]
-        )
-        ( Pattern_
-            [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( f1{}(   \dv{SomeSort{}}("thing") ) ), RuleVar:SortK{}) ) |]
-        )
+        [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( con1{}( \dv{SomeSort{}}("thing") ) ), RuleVar:SortK{}) ) |]
+        [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( f1{}(   \dv{SomeSort{}}("thing") ) ), RuleVar:SortK{}) ) |]
         42
 rule1' =
     rule
         (Just "con1-f1'")
-        ( Pattern_
-            [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( con1{}( X:SomeSort{} ) ), RuleVar:SortK{}) ) |]
-        )
-        ( Pattern_
-            [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( f1{}(   X:SomeSort{} ) ), RuleVar:SortK{}) ) |]
-        )
+        [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( con1{}( X:SomeSort{} ) ), RuleVar:SortK{}) ) |]
+        [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( f1{}(   X:SomeSort{} ) ), RuleVar:SortK{}) ) |]
         50
 rule2 =
     rule
         (Just "con1-f2")
-        ( Pattern_
-            [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( con1{}( X:SomeSort{} ) ),                  RuleVar:SortK{}) ) |]
-        )
-        ( Pattern_
-            [trm| kCell{}( kseq{}( inj{AnotherSort{}, SortKItem{}}( con4{}( X:SomeSort{}, X:SomeSort{} ) ), RuleVar:SortK{}) ) |]
-        )
+        [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( con1{}( X:SomeSort{} ) ),                  RuleVar:SortK{}) ) |]
+        [trm| kCell{}( kseq{}( inj{AnotherSort{}, SortKItem{}}( con4{}( X:SomeSort{}, X:SomeSort{} ) ), RuleVar:SortK{}) ) |]
         50
 rule3 =
     rule
         (Just "con3-con1")
-        ( Pattern_
-            [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( con3{}( \dv{SomeSort{}}("otherThing"), Y:SomeSort{} ) ), RuleVar:SortK{}) ) |]
-        )
-        ( Pattern_
-            [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( con1{}( \dv{SomeSort{}}("somethingElse") ) ),            RuleVar:SortK{}) ) |]
-        )
+        [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( con3{}( \dv{SomeSort{}}("otherThing"), Y:SomeSort{} ) ), RuleVar:SortK{}) ) |]
+        [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( con1{}( \dv{SomeSort{}}("somethingElse") ) ),            RuleVar:SortK{}) ) |]
         42
 rule4 =
     rule
         (Just "con4-f2-partial")
-        ( Pattern_
-            [trm| kCell{}( kseq{}( inj{AnotherSort{}, SortKItem{}}( con4{}( X:SomeSort{}, Y:SomeSort{} ) ), RuleVar:SortK{}) ) |]
-        )
-        ( Pattern_
-            [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( f2{}(   Y:SomeSort{} ) ), RuleVar:SortK{}) ) |]
-        )
+        [trm| kCell{}( kseq{}( inj{AnotherSort{}, SortKItem{}}( con4{}( X:SomeSort{}, Y:SomeSort{} ) ), RuleVar:SortK{}) ) |]
+        [trm| kCell{}( kseq{}( inj{SomeSort{}, SortKItem{}}( f2{}(   Y:SomeSort{} ) ), RuleVar:SortK{}) ) |]
         42
         `withComputedAttributes` ComputedAxiomAttributes False [UndefinedSymbol "f2"]
 
 kCell :: Symbol
 kCell =
     [symb| symbol Lbl'-LT-'k'-GT-'{}(SortK{}) : SortKCell{} [constructor{}()] |]
 
-rule :: Maybe Text -> Pattern -> Pattern -> Priority -> RewriteRule "Rewrite"
+rule :: Maybe Text -> Term -> Term -> Priority -> RewriteRule "Rewrite"
 rule ruleLabel lhs rhs priority =
     RewriteRule
-        { lhs = lhs.term
-        , rhs = rhs.term
-        , requires = lhs.constraints
-        , ensures = rhs.constraints
+        { lhs
+        , rhs
+        , requires = []
+        , ensures = []
         , attributes =
             AxiomAttributes
                 { location = Nothing

diff --git a/booster/unit-tests/Test/Booster/Syntax/Json/Internalise.hs b/booster/unit-tests/Test/Booster/Syntax/Json/Internalise.hs
@@ -9,7 +9,6 @@ module Test.Booster.Syntax.Json.Internalise (
 import Control.Monad.Trans.Except
 import Data.Coerce
 import Data.Map qualified as Map
-import Data.Set qualified as Set
 import Data.Text (Text)
 import Test.Tasty
 import Test.Tasty.HUnit
@@ -53,7 +52,7 @@ testBasicPredicates =
 
     shouldBeBool name pat expected =
         testCase name $
-            Right (InternalisedPredicates (Set.singleton expected) mempty mempty [])
+            Right (InternalisedPredicates [expected] mempty mempty [])
                 @=? runExcept (internalise pat)
 
     expectUnsupported description pat expected =
@@ -106,7 +105,7 @@ testSubstitutions =
                     , "X" .==> var' "Z"
                     ]
                 )
-                (hasEquations [(var_ "X", var_ "Y"), (var_ "X", var_ "Z")])
+                (hasEquations [(var_ "X", var_ "Z"), (var_ "X", var_ "Y")])
         ]
   where
     test name syntax expected =
@@ -124,9 +123,7 @@ testSubstitutions =
          in InternalisedPredicates mempty mempty expectedSubstitution mempty
 
     hasEquations pairs =
-        let expectedPreds =
-                Set.fromList [t ==. t' | (t, t') <- pairs]
-         in InternalisedPredicates expectedPreds mempty mempty mempty
+        InternalisedPredicates [t ==. t' | (t, t') <- pairs] mempty mempty mempty
 
 -- basically a semigroup instance but in the general case the
 -- substitutions would have to be trimmed. We don't need it in the