Skip to content

Commit 1c6663d

Browse files
committed
switching order of LogicT and ExceptT
1 parent efbdade commit 1c6663d

File tree

1 file changed

+6
-14
lines changed

1 file changed

+6
-14
lines changed

kore/src/Kore/Equation/Simplification.hs

Lines changed: 6 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -30,18 +30,10 @@ import Kore.Internal.MultiAnd
3030
( MultiAnd
3131
)
3232
import qualified Kore.Internal.MultiAnd as MultiAnd
33-
-- import Kore.Internal.OrPattern
34-
-- ( OrPattern
35-
-- )
36-
-- import Kore.Internal.Pattern
37-
-- ( Pattern
38-
-- )
39-
-- import qualified Kore.Internal.Pattern as Pattern
4033
import qualified Kore.Internal.Predicate as Predicate
4134
import qualified Kore.Internal.SideCondition as SideCondition
4235
import qualified Kore.Internal.Substitution as Substitution
4336
import qualified Kore.Internal.TermLike as TermLike
44-
-- import qualified Kore.Step.Simplification.Pattern as Pattern
4537
import Kore.Step.Simplification.Simplify
4638
( InternalVariable
4739
, MonadSimplify
@@ -83,15 +75,15 @@ simplifyEquation
8375
-> simplifier (MultiAnd (Equation variable))
8476
simplifyEquation equation =
8577
do
86-
simplifiedCond <- lift $
78+
simplifiedCond <-
8779
Simplifier.simplifyCondition
8880
SideCondition.top
8981
(fromPredicate argument')
90-
Monad.unless
82+
lift $ Monad.unless
9183
((isTop . predicate) simplifiedCond)
9284
(throwE equation)
9385
let Conditional { substitution, predicate } = simplifiedCond
94-
Monad.unless (isTop predicate) (throwE equation)
86+
lift $ Monad.unless (isTop predicate) (throwE equation)
9587
let subst = Substitution.toMap substitution
9688
left' = TermLike.substitute subst left
9789
requires' = Predicate.substitute subst requires
@@ -107,14 +99,14 @@ simplifyEquation equation =
10799
, ensures = Predicate.forgetSimplified ensures'
108100
, attributes = attributes
109101
}
110-
& returnOriginalIfAborted
111102
& Logic.observeAllT
103+
& returnOriginalIfAborted
112104
& fmap MultiAnd.make
113105
where
114106
argument' =
115107
fromMaybe Predicate.makeTruePredicate argument
116-
returnOriginalIfAborted =
117-
fmap (either id id) . runExceptT
108+
returnOriginalIfAborted xs =
109+
fmap (either (: []) id) (runExceptT xs)
118110
Equation
119111
{ requires
120112
, argument

0 commit comments

Comments
 (0)