modified matchEquation to accept new equation format (#2688)

MirceaS · github-actions · web-flow · commit 797767163899 · 2021-06-29T13:49:40.000-06:00
* modified matchEquation to accept new equation format

* Format with fourmolu

* updated tests and documentation to support new equation format

* Added back tests that exercise the old equation format

Co-authored-by: github-actions &lt;github-actions@github.com&gt;
diff --git a/design-decisions/2020-05-02-function-rules.md b/design-decisions/2020-05-02-function-rules.md
@@ -32,7 +32,7 @@ rule fun(φ₁ᵢ({Y}), φ₂ᵢ({Y}), ...) => ψᵢ({Y}) requires Preᵢ({Y}) e
 Each rule is interpreted in Kore as an axiom,
 
 ```.kore
-axiom \implies(Preᵢ({Y}), (fun(φ₁ᵢ({Y}), φ₂ᵢ({Y}), ...) = ψᵢ({Y})) ∧ Postᵢ({Y})).
+axiom \implies(Preᵢ({Y}), (fun(φ₁ᵢ({Y}), φ₂ᵢ({Y}), ...) = (ψᵢ({Y}) ∧ Postᵢ({Y})))).
 ```
 
 ## Problems
@@ -82,8 +82,8 @@ rule fun(B) => C
 which is interpreted in Kore as two axioms,
 
 ```.kore
-axiom \implies(\top, (fun(A) = C) ∧ \top)
-axiom \implies(\top, (fun(B) = C) ∧ \top).
+axiom \implies(\top, (fun(A) = (C ∧ \top)))
+axiom \implies(\top, (fun(B) = (C ∧ \top))).
 ```
 
 The K language offers a shorthand notation,
@@ -96,7 +96,7 @@ which is intended to be equivalent to the pair of rules above.
 Under the current interpretation, this rule produces an axiom,
 
 ```.kore
-axiom \implies(\top, (fun(A ∨ B) = C) ∧ \top)
+axiom \implies(\top, (fun(A ∨ B) = (C ∧ \top)))
 ```
 
 which is **not** equivalent to the first interpretation.
@@ -126,7 +126,7 @@ rule fun(φ₁ᵢ({Y}), φ₂ᵢ({Y}), ...) => ψᵢ({Y}) requires Preᵢ({Y}) e
 will be interpreted in Kore as
 
 ```.kore
-axiom \implies(Preᵢ({Y}) ∧ Argsᵢ({X}, {Y}) ∧ Prioᵢ({X}), (fun(X₁, X₂, ...) = ψᵢ({Y})) ∧ Postᵢ({Y}))
+axiom \implies(Preᵢ({Y}) ∧ Argsᵢ({X}, {Y}) ∧ Prioᵢ({X}), (fun(X₁, X₂, ...) = (ψᵢ({Y}) ∧ Postᵢ({Y}))))
 ```
 
 where
@@ -216,8 +216,8 @@ axiom
             true = notBool(<=Int(L, X)),
             (X₁ ∈ L) ∧ (X₂ ∈ X)
         ),
-        \and(
-            _<=_<_(X₁, X₂, X₃) = false,
+        _<=_<_(X₁, X₂, X₃) = \and (
+            false,
             \top
         )
     )
@@ -232,8 +232,8 @@ axiom
                     (X₁ ∈ L) ∧ (X₂ ∈ X)
                 )
         ),
-        \and(
-            _<=_<_(X₁, X₂, X₃) = false,
+        _<=_<_(X₁, X₂, X₃) = \and(
+            false,
             \top
         )
     )
@@ -255,8 +255,8 @@ axiom
                     )
             )
         ),
-        \and(
-            _<=_<_(X₁, X₂, X₃) = true,
+        _<=_<_(X₁, X₂, X₃) = \and(
+            true,
             \top
         )
     )
diff --git a/kore/src/Kore/Equation/Equation.hs b/kore/src/Kore/Equation/Equation.hs
@@ -6,6 +6,7 @@ module Kore.Equation.Equation (
     Equation (..),
     mkEquation,
     toTermLike,
+    toTermLikeOld,
     mapVariables,
     refreshVariables,
     isSimplificationRule,
@@ -162,12 +163,13 @@ instance InternalVariable variable => Substitute (Equation variable) where
     rename = substitute . fmap mkVar
     {-# INLINE rename #-}
 
-toTermLike ::
+-- This function must be removed as part of https://github.com/kframework/kore/issues/2593
+toTermLikeOld ::
     InternalVariable variable =>
     Sort ->
     Equation variable ->
     TermLike variable
-toTermLike sort equation
+toTermLikeOld sort equation
     -- \ceil axiom
     | isTop requires
       , isTop ensures
@@ -228,6 +230,70 @@ toTermLike sort equation
         , ensures
         } = equation
 
+toTermLike ::
+    InternalVariable variable =>
+    Sort ->
+    Equation variable ->
+    TermLike variable
+toTermLike sort equation
+    -- \ceil axiom
+    | isTop requires
+      , isTop ensures
+      , TermLike.Ceil_ _ sort1 _ <- left
+      , TermLike.Top_ sort2 <- right
+      , sort1 == sort2 =
+        left
+    -- function rule
+    | Just argument' <- argument
+      , Just antiLeft' <- antiLeft =
+        let antiLeftTerm = fromPredicate sort antiLeft'
+            argumentTerm = fromPredicate sort argument'
+         in TermLike.mkImplies
+                ( TermLike.mkAnd
+                    antiLeftTerm
+                    ( TermLike.mkAnd
+                        requires'
+                        argumentTerm
+                    )
+                )
+                ( TermLike.mkEquals sort left $
+                    TermLike.mkAnd right ensures'
+                )
+    -- function rule without priority
+    | Just argument' <- argument =
+        let argumentTerm = fromPredicate sort argument'
+         in TermLike.mkImplies
+                ( TermLike.mkAnd
+                    requires'
+                    (TermLike.mkAnd argumentTerm $ TermLike.mkTop sort)
+                )
+                ( TermLike.mkEquals sort left $
+                    TermLike.mkAnd right ensures'
+                )
+    -- unconditional equation
+    | isTop requires
+      , isTop ensures =
+        TermLike.mkEquals sort left right
+    -- conditional equation
+    | otherwise =
+        TermLike.mkImplies
+            requires'
+            ( TermLike.mkEquals sort left $
+                TermLike.mkAnd right ensures'
+            )
+  where
+    requires' = fromPredicate sort requires
+    ensures' = fromPredicate rightSort ensures
+    Equation
+        { requires
+        , argument
+        , antiLeft
+        , left
+        , right
+        , ensures
+        } = equation
+    rightSort = TermLike.termLikeSort right
+
 instance
     InternalVariable variable =>
     HasFreeVariables (Equation variable) variable
diff --git a/kore/src/Kore/Equation/Sentence.hs b/kore/src/Kore/Equation/Sentence.hs
@@ -116,6 +116,8 @@ matchEquation attributes termLike
     isSubsortAxiom = (not . null . getSubsorts . Attribute.subsorts) attributes
 
     -- function rule without priority
+    -- TODO The pattern match below should be removed after the frontend is updated
+    -- to use the correct format
     match
         ( TermLike.Implies_
                 _
@@ -148,8 +150,43 @@ matchEquation attributes termLike
                         , ensures = ensures'
                         , attributes
                         }
+    match
+        ( TermLike.Implies_
+                _
+                ( TermLike.And_
+                        _
+                        requires
+                        argument@( TermLike.And_
+                                        _
+                                        (TermLike.In_ _ _ _ _)
+                                        _
+                                    )
+                    )
+                ( TermLike.Equals_
+                        _
+                        _
+                        left
+                        (TermLike.And_ _ right ensures)
+                    )
+            ) =
+            do
+                requires' <- makePredicate requires & Bifunctor.first RequiresError
+                argument' <- makePredicate argument & Bifunctor.first ArgumentError
+                ensures' <- makePredicate ensures & Bifunctor.first EnsuresError
+                pure
+                    Equation
+                        { requires = requires'
+                        , argument = Just argument'
+                        , antiLeft = Nothing
+                        , left
+                        , right
+                        , ensures = ensures'
+                        , attributes
+                        }
 
     -- function rule with priority
+    -- TODO The pattern match below should be removed after the frontend is updated
+    -- to use the correct format
     match
         ( TermLike.Implies_
                 _
@@ -183,6 +220,42 @@ matchEquation attributes termLike
                         , ensures = ensures'
                         , attributes
                         }
+    match
+        ( TermLike.Implies_
+                _
+                ( TermLike.And_
+                        _
+                        antiLeft
+                        ( TermLike.And_
+                                _
+                                requires
+                                argument
+                            )
+                    )
+                ( TermLike.Equals_
+                        _
+                        _
+                        left
+                        (TermLike.And_ _ right ensures)
+                    )
+            ) =
+            do
+                requires' <- makePredicate requires & Bifunctor.first RequiresError
+                argument' <- makePredicate argument & Bifunctor.first ArgumentError
+                antiLeft' <- makePredicate antiLeft & Bifunctor.first AntiLeftError
+                ensures' <- makePredicate ensures & Bifunctor.first EnsuresError
+                pure
+                    Equation
+                        { requires = requires'
+                        , argument = Just argument'
+                        , antiLeft = Just antiLeft'
+                        , left
+                        , right
+                        , ensures = ensures'
+                        , attributes
+                        }
+    -- TODO The pattern match below should be removed after the frontend is updated
+    -- to use the correct format
     match
         ( TermLike.Implies_
                 _
@@ -206,6 +279,30 @@ matchEquation attributes termLike
                         , ensures = ensures'
                         , attributes
                         }
+    match
+        ( TermLike.Implies_
+                _
+                requires
+                ( TermLike.Equals_
+                        _
+                        _
+                        left
+                        (TermLike.And_ _ right ensures)
+                    )
+            ) =
+            do
+                requires' <- makePredicate requires & Bifunctor.first RequiresError
+                ensures' <- makePredicate ensures & Bifunctor.first EnsuresError
+                pure
+                    Equation
+                        { requires = requires'
+                        , argument = Nothing
+                        , antiLeft = Nothing
+                        , left
+                        , right
+                        , ensures = ensures'
+                        , attributes
+                        }
     match (TermLike.Equals_ _ _ left right) =
         pure
             Equation
diff --git a/kore/test/Test/Kore/Equation/Sentence.hs b/kore/test/Test/Kore/Equation/Sentence.hs
@@ -30,7 +30,8 @@ test_fromSentenceAxiom =
             original = mkEquals sortR left right
             equation = mkEquation left right
         assertions original equation
-    , testCase "⌈f(x))⌉ → f(x) = g(x) ∧ ⌈h(x)⌉" $ do
+    , testCase "⌈f(x))⌉ → f(x) = g(x) ∧ ⌈h(x)⌉ (OLD FORMAT)" $ do
+        -- This test case must be removed as part of https://github.com/kframework/kore/issues/2593
         let requires = mkCeil sortR (Mock.f Mock.a)
             ensures = mkCeil sortR (Mock.h Mock.b)
             left = Mock.f (mkElemVar Mock.x)
@@ -43,8 +44,9 @@ test_fromSentenceAxiom =
                     { requires = wrapPredicate requires
                     , ensures = wrapPredicate ensures
                     }
-        assertions original equation
-    , testCase "New equation form: ⌈f(x)⌉ ∧ ⌈y ∈ x⌉ → f(y) = g(x) ∧ ⌈h(x)⌉" $ do
+        assertionsOld original equation
+    , testCase "New equation form: ⌈f(x)⌉ ∧ ⌈y ∈ x⌉ → f(y) = g(x) ∧ ⌈h(x)⌉ (OLD FORMAT)" $ do
+        -- This test case must be removed as part of https://github.com/kframework/kore/issues/2593
         let requires = mkCeil sortR (Mock.f Mock.a)
             ensures = mkCeil sortR (Mock.h Mock.b)
             argument = mkIn sortR (mkElemVar Mock.y) (mkElemVar Mock.x)
@@ -61,6 +63,38 @@ test_fromSentenceAxiom =
                     , argument = Just $ wrapPredicate argument
                     , ensures = wrapPredicate ensures
                     }
+        assertionsOld original equation
+    , testCase "⌈f(x))⌉ → f(x) = g(x) ∧ ⌈h(x)⌉" $ do
+        let requires = mkCeil sortR (Mock.f Mock.a)
+            ensures = mkCeil Mock.testSort (Mock.h Mock.b)
+            left = Mock.f (mkElemVar Mock.x)
+            right = Mock.g (mkElemVar Mock.x)
+            original =
+                mkImplies requires $
+                    mkEquals sortR left (mkAnd right ensures)
+            equation =
+                (mkEquation left right)
+                    { requires = wrapPredicate requires
+                    , ensures = wrapPredicate ensures
+                    }
+        assertions original equation
+    , testCase "New equation form: ⌈f(x)⌉ ∧ ⌈y ∈ x⌉ → f(y) = g(x) ∧ ⌈h(x)⌉" $ do
+        let requires = mkCeil sortR (Mock.f Mock.a)
+            ensures = mkCeil Mock.testSort (Mock.h Mock.b)
+            argument = mkIn sortR (mkElemVar Mock.y) (mkElemVar Mock.x)
+            argument' =
+                mkAnd argument (mkTop sortR)
+            left = Mock.f (mkElemVar Mock.y)
+            right = Mock.g (mkElemVar Mock.y)
+            original =
+                mkImplies (mkAnd requires argument') $
+                    mkEquals sortR left (mkAnd right ensures)
+            equation =
+                (mkEquation left right)
+                    { requires = wrapPredicate requires
+                    , argument = Just $ wrapPredicate argument
+                    , ensures = wrapPredicate ensures
+                    }
         assertions original equation
     ]
   where
@@ -78,6 +112,19 @@ test_fromSentenceAxiom =
             "Expected original pattern"
             original
             (toTermLike (termLikeSort original) actual)
+    -- This function must be removed as part of https://github.com/kframework/kore/issues/2593
+    assertionsOld ::
+        HasCallStack =>
+        TermLike VariableName ->
+        Equation VariableName ->
+        Assertion
+    assertionsOld original equation = do
+        actual <- expectRight $ test original
+        assertEqual "Expected equation" equation actual
+        assertEqual
+            "Expected original pattern"
+            original
+            (toTermLikeOld (termLikeSort original) actual)
     test original = fromSentenceAxiom (def, mkAxiom [sortVariableR] original)
 
 varI1, varI2 :: TermLike VariableName
