Skip to content

Commit c282007

Browse files
ana-pantiliettuegelrv-jenkins
authored
Function evaluator: stop at first applicable equation (#2128)
* Refactor definitionEvaluation * RED test_attemptEquations: stop at first applied equation * GRN test_attemptEquations: stop at first applied equation * Clean-up * RED test_iterateUntil: empty list * GRN iterateUntil: empty list * RED test_iterateUntil: one error result * GRN iterateUntil: one result * RED test_iterateUntil: two error results * GRN iterateUntil: appendErrorAndContinue * test_iterateUntil: stops at first good result * EvaluationStrategy.definitionEvaluation: use iterateUntil + clean-up * Clean-up * Address review comments: use ExceptRT + add attemptEquations * test_attemptEquations: test attemptEquations stops at first good result * test_attemptEquations: refactor * Clean-up * Clean-up * attemptEquations: return result instead of action * Generalize signature of attemptEquations Co-authored-by: Thomas Tuegel <[email protected]> Co-authored-by: rv-jenkins <[email protected]>
1 parent 91aa4f2 commit c282007

File tree

2 files changed

+110
-27
lines changed

2 files changed

+110
-27
lines changed

‎kore/src/Kore/Step/Axiom/EvaluationStrategy.hs‎

Lines changed: 65 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -13,11 +13,20 @@ module Kore.Step.Axiom.EvaluationStrategy
1313
, simplificationEvaluation
1414
, firstFullEvaluation
1515
, simplifierWithFallback
16+
-- * For testing
17+
, attemptEquationAndAccumulateErrors
18+
, attemptEquations
1619
) where
1720

1821
import Prelude.Kore
1922

20-
import qualified Data.Bifunctor as Bifunctor
23+
import Control.Monad.Except
24+
( ExceptT (..)
25+
, runExceptT
26+
)
27+
import Data.EitherR
28+
( ExceptRT (..)
29+
)
2130
import qualified Data.Foldable as Foldable
2231
import Data.Semigroup
2332
( Min (..)
@@ -27,12 +36,16 @@ import qualified Data.Text as Text
2736

2837
import qualified Kore.Attribute.Symbol as Attribute
2938
import Kore.Equation
30-
( Equation
39+
( AttemptEquationError
40+
, Equation
3141
)
3242
import qualified Kore.Equation as Equation
3343
import qualified Kore.Internal.MultiOr as MultiOr
3444
( extractPatterns
3545
)
46+
import Kore.Internal.OrPattern
47+
( OrPattern
48+
)
3649
import qualified Kore.Internal.OrPattern as OrPattern
3750
import Kore.Internal.SideCondition
3851
( SideCondition
@@ -47,6 +60,9 @@ import qualified Kore.Step.Simplification.Simplify as AttemptedAxiom
4760
import Kore.Unparser
4861
( unparse
4962
)
63+
import Kore.Variables.Target
64+
( Target
65+
)
5066
import qualified Kore.Variables.Target as Target
5167
import qualified Pretty
5268

@@ -73,31 +89,53 @@ definitionEvaluation equations =
7389
Equation.mapVariables (pure fromVariableName)
7490
<$> equations
7591
term' = TermLike.mapVariables Target.mkUnifiedNonTarget term
76-
let -- Attempt an equation, pairing it with its result, if applicable.
77-
attemptEquation equation =
78-
Equation.attemptEquation condition term' equation
79-
>>= return . Bifunctor.second apply
80-
where
81-
apply = Equation.applyEquation condition equation
82-
traverse attemptEquation equations' >>=
83-
(partitionEithers >>> \case
84-
(_, applied : _) -> do
85-
results <- applied
86-
(return . Applied) AttemptedAxiomResults
87-
{ results
88-
, remainders = OrPattern.bottom
89-
}
90-
(errors, []) ->
91-
case minError of
92-
Just (Equation.WhileCheckRequires _) ->
93-
(return . NotApplicableUntilConditionChanges)
94-
(SideCondition.toRepresentation condition)
95-
_ -> return NotApplicable
96-
where
97-
minError =
98-
(fmap getMin . getOption)
99-
(foldMap (Option . Just . Min) errors)
100-
)
92+
result <-
93+
attemptEquations
94+
(attemptEquationAndAccumulateErrors condition term')
95+
equations'
96+
case result of
97+
Right results ->
98+
(return . Applied) AttemptedAxiomResults
99+
{ results
100+
, remainders = OrPattern.bottom
101+
}
102+
Left minError ->
103+
case getMin <$> getOption minError of
104+
Just (Equation.WhileCheckRequires _) ->
105+
(return . NotApplicableUntilConditionChanges)
106+
(SideCondition.toRepresentation condition)
107+
_ -> return NotApplicable
108+
109+
attemptEquationAndAccumulateErrors
110+
:: (InternalVariable variable, MonadSimplify simplifier)
111+
=> SideCondition variable
112+
-> TermLike (Target variable)
113+
-> Equation variable
114+
-> ExceptRT
115+
(OrPattern variable)
116+
simplifier
117+
(Option (Min (AttemptEquationError variable)))
118+
attemptEquationAndAccumulateErrors condition term equation =
119+
attemptEquation
120+
where
121+
attemptEquation =
122+
ExceptRT . ExceptT
123+
$ Equation.attemptEquation condition term equation
124+
>>= either (return . Left . Option . Just . Min) (fmap Right . apply)
125+
apply = Equation.applyEquation condition equation
126+
127+
attemptEquations
128+
:: MonadSimplify simplifier
129+
=> Monoid error
130+
=> (Equation variable -> ExceptRT result simplifier error)
131+
-> [Equation variable]
132+
-> simplifier (Either error result)
133+
attemptEquations accumulator equations =
134+
Foldable.foldlM
135+
(\err equation -> mappend err <$> accumulator equation)
136+
mempty
137+
equations
138+
& runExceptRT & runExceptT
101139

102140
-- | Create an evaluator from a single simplification rule.
103141
simplificationEvaluation

‎kore/test/Test/Kore/Step/Axiom/EvaluationStrategy.hs‎

Lines changed: 45 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,12 +3,19 @@ module Test.Kore.Step.Axiom.EvaluationStrategy
33
, test_firstFullEvaluation
44
, test_simplifierWithFallback
55
, test_builtinEvaluation
6+
, test_attemptEquations
67
) where
78

89
import Prelude.Kore
910

1011
import Test.Tasty
1112

13+
import Data.IORef
14+
( modifyIORef'
15+
, newIORef
16+
, readIORef
17+
)
18+
1219
import qualified Kore.Internal.OrPattern as OrPattern
1320
import Kore.Internal.Pattern as Pattern
1421
( Conditional (Conditional)
@@ -43,6 +50,44 @@ import qualified Test.Kore.Step.MockSymbols as Mock
4350
import Test.Kore.Step.Simplification
4451
import Test.Tasty.HUnit.Ext
4552

53+
test_attemptEquations :: [TestTree]
54+
test_attemptEquations =
55+
[ testCase "Stops attempting equations at first successful result" $ do
56+
counter <- newIORef (0 :: Int)
57+
let condition =
58+
SideCondition.assumeTruePredicate makeTruePredicate_
59+
term = Mock.functionalConstr10 Mock.a
60+
equations =
61+
[ notApplicable1, applicable, notApplicable2, applicable
62+
]
63+
_ <-
64+
attemptEquations
65+
(attemptEquationAndAccumulateErrors' counter condition term)
66+
equations
67+
& runSimplifier Mock.env
68+
updatedCounter <- readIORef counter
69+
assertEqual "" 2 updatedCounter
70+
]
71+
where
72+
attemptEquationAndAccumulateErrors' counter condition term equation = do
73+
liftIO $ modifyIORef' counter (+ 1)
74+
attemptEquationAndAccumulateErrors condition term equation
75+
applicable =
76+
axiom
77+
(Mock.functionalConstr10 (mkElemVar Mock.x))
78+
Mock.a
79+
(makeEqualsPredicate_ (mkElemVar Mock.x) Mock.a)
80+
notApplicable1 =
81+
axiom
82+
(Mock.functionalConstr10 (mkElemVar Mock.x))
83+
Mock.c
84+
(makeEqualsPredicate_ (mkElemVar Mock.x) Mock.c)
85+
notApplicable2 =
86+
axiom
87+
(Mock.functionalConstr10 (mkElemVar Mock.x))
88+
Mock.b
89+
(makeEqualsPredicate_ (mkElemVar Mock.x) Mock.b)
90+
4691
test_definitionEvaluation :: [TestTree]
4792
test_definitionEvaluation =
4893
[ testCase "Simple evaluation" $ do

0 commit comments

Comments
 (0)