Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Remove support for old encoding of equations #2890

Merged
merged 10 commits into from
Oct 27, 2021
Merged

Remove support for old encoding of equations #2890

Show file tree
Hide file tree
Changes from 9 commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
2689385
Remove support for old encoding of equations
ana-pantilie Oct 21, 2021
7988554
Format with fourmolu
invalid-email-address Oct 21, 2021
91958ba
Change encoding in prelude.kore
ana-pantilie Oct 22, 2021
2f53579
Merge branch 'remove-old-equation-encoding' of github.com:kframework/…
ana-pantilie Oct 22, 2021
2197c67
Regenerate regression tests with modified prelude.kore
ana-pantilie Oct 22, 2021
d20773b
Modify encoding in unit tests
ana-pantilie Oct 22, 2021
c0f6b13
Merge branch 'master' into remove-old-equation-encoding
ana-pantilie Oct 25, 2021
d91b765
Replace files in issue-2221 with minimzed K example
ana-pantilie Oct 25, 2021
352abc9
Remove issue-2244 because it can't be regenerated
ana-pantilie Oct 25, 2021
d6d7757
Merge remote-tracking branch 'origin/master' into remove-old-equation…
ana-pantilie Oct 27, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
68 changes: 0 additions & 68 deletions kore/src/Kore/Equation/Equation.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,6 @@ module Kore.Equation.Equation (
Equation (..),
mkEquation,
toTermLike,
toTermLikeOld,
mapVariables,
refreshVariables,
isSimplificationRule,
Expand Down Expand Up @@ -210,73 +209,6 @@ instance InternalVariable variable => Substitute (Equation variable) where
rename = substitute . fmap mkVar
{-# INLINE rename #-}

-- This function must be removed as part of https://github.com/kframework/kore/issues/2593
toTermLikeOld ::
InternalVariable variable =>
Sort ->
Equation variable ->
TermLike variable
toTermLikeOld 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.mkAnd
(TermLike.mkEquals sort left 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.mkAnd
(TermLike.mkEquals sort left right)
ensures'
)
-- unconditional equation
| isTop requires
, isTop ensures =
TermLike.mkEquals sort left right
-- conditional equation
| otherwise =
TermLike.mkImplies
requires'
( TermLike.mkAnd
(TermLike.mkEquals sort left right)
ensures'
)
where
requires' = fromPredicate sort requires
ensures' = fromPredicate sort ensures
Equation
{ requires
, argument
, antiLeft
, left
, right
, ensures
} = equation

toTermLike ::
InternalVariable variable =>
Sort ->
Expand Down
94 changes: 0 additions & 94 deletions kore/src/Kore/Equation/Sentence.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -116,40 +116,6 @@ 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_
_
( TermLike.And_
_
requires
argument@( TermLike.And_
_
(TermLike.In_ _ _ _ _)
_
)
)
( TermLike.And_
_
(TermLike.Equals_ _ _ left 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
}
match
( TermLike.Implies_
_
Expand Down Expand Up @@ -185,41 +151,6 @@ matchEquation attributes termLike
}

-- 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_
_
( TermLike.And_
_
antiLeft
( TermLike.And_
_
requires
argument
)
)
( TermLike.And_
_
(TermLike.Equals_ _ _ left 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
}
match
( TermLike.Implies_
_
Expand Down Expand Up @@ -254,31 +185,6 @@ matchEquation attributes termLike
, ensures = ensures'
, attributes
}
-- TODO The pattern match below should be removed after the frontend is updated
-- to use the correct format
match
( TermLike.Implies_
_
requires
( TermLike.And_
_
(TermLike.Equals_ _ _ left 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.Implies_
_
Expand Down
47 changes: 0 additions & 47 deletions kore/test/Test/Kore/Equation/Sentence.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,40 +30,6 @@ test_fromSentenceAxiom =
original = mkEquals sortR left right
equation = mkEquation left right
assertions original equation
, 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)
right = Mock.g (mkElemVar Mock.x)
original =
mkImplies requires $
mkAnd (mkEquals sortR left right) ensures
equation =
(mkEquation left right)
{ requires = wrapPredicate requires
, ensures = wrapPredicate ensures
}
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)
argument' =
mkAnd argument (mkTop sortR)
left = Mock.f (mkElemVar Mock.y)
right = Mock.g (mkElemVar Mock.y)
original =
mkImplies (mkAnd requires argument') $
mkAnd (mkEquals sortR left right) ensures
equation =
(mkEquation left right)
{ requires = wrapPredicate requires
, 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)
Expand Down Expand Up @@ -112,19 +78,6 @@ 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
Expand Down
30 changes: 17 additions & 13 deletions kore/test/Test/Kore/Exec.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -41,13 +41,17 @@ import qualified Kore.Builtin.Int as Int
import Kore.Equation.Equation (
Equation (..),
mkEquation,
toTermLikeOld,
toTermLike,
)
import qualified Kore.Error
import Kore.Exec
import Kore.IndexedModule.IndexedModule
import Kore.Internal.ApplicationSorts
import Kore.Internal.Pattern as Pattern
import Kore.Internal.Pattern (
Conditional (Conditional),
Pattern,
)
import qualified Kore.Internal.Pattern as Pattern
import Kore.Internal.Predicate (
makeFalsePredicate,
makeTruePredicate,
Expand Down Expand Up @@ -266,12 +270,12 @@ test_matchDisjunction =
]
, moduleAttributes = Attributes []
}
initial = fromTermLike $ applyToNoArgs mySort "initial"
next1 = fromTermLike $ applyToNoArgs mySort "next1"
next2 = fromTermLike $ applyToNoArgs mySort "next2"
final1 = fromTermLike $ applyToNoArgs mySort "final1"
final2 = fromTermLike $ applyToNoArgs mySort "final2"
unreachable = fromTermLike $ applyToNoArgs mySort "unreachable"
initial = Pattern.fromTermLike $ applyToNoArgs mySort "initial"
next1 = Pattern.fromTermLike $ applyToNoArgs mySort "next1"
next2 = Pattern.fromTermLike $ applyToNoArgs mySort "next2"
final1 = Pattern.fromTermLike $ applyToNoArgs mySort "final1"
final2 = Pattern.fromTermLike $ applyToNoArgs mySort "final2"
unreachable = Pattern.fromTermLike $ applyToNoArgs mySort "unreachable"

test_checkFunctions :: TestTree
test_checkFunctions =
Expand Down Expand Up @@ -354,7 +358,7 @@ test_checkFunctions =
SentenceAxiomSentence
( mkAxiom
[]
( toTermLikeOld
( toTermLike
mySort
( mkEquation
myF
Expand Down Expand Up @@ -427,7 +431,7 @@ test_checkFunctionsIgnoreSimpl =
SentenceAxiomSentence
( mkAxiom
[]
( toTermLikeOld
( toTermLike
mySort
( mkEquation
myF
Expand Down Expand Up @@ -502,7 +506,7 @@ test_checkBothMatch =
mySentence name pr =
SentenceAxiomSentence $
mkAxiom [] $
toTermLikeOld mySort $
toTermLike mySort $
Equation
{ left = myF
, requires = pr
Expand Down Expand Up @@ -573,7 +577,7 @@ test_checkBothMatchIgnoreSimpl =
mySentence name pr =
SentenceAxiomSentence $
mkAxiom [] $
toTermLikeOld mySort $
toTermLike mySort $
Equation
{ left = myF
, requires = pr
Expand All @@ -588,7 +592,7 @@ test_checkBothMatchIgnoreSimpl =
mySentenceSimpl name pr =
SentenceAxiomSentence
( mkAxiom [] $
toTermLikeOld mySort $
toTermLike mySort $
Equation
{ left = myF
, requires = pr
Expand Down
Loading