Skip to content

Commit 4fb8352

Browse files
andreiburdusattuegelana-pantilie
authored
Fix variable to RewritingVariableName in Kore.Equation.Application (#2325)
Co-authored-by: andreiburdusa <[email protected]> Co-authored-by: Thomas Tuegel <[email protected]> Co-authored-by: ana-pantilie <[email protected]>
1 parent 9460590 commit 4fb8352

File tree

153 files changed

+5263
-4018
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

153 files changed

+5263
-4018
lines changed

‎kore/app/exec/Main.hs

Lines changed: 9 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -83,6 +83,9 @@ import System.IO
8383
, withFile
8484
)
8585

86+
import Data.Functor
87+
( (<&>)
88+
)
8689
import Kore.Attribute.Symbol as Attribute
8790
import Kore.BugReport
8891
import Kore.Exec
@@ -147,6 +150,9 @@ import Kore.Reachability
147150
import qualified Kore.Reachability.Claim as Claim
148151
import Kore.Rewriting.RewritingVariable
149152
import Kore.Step
153+
import Kore.Step.RulePattern
154+
( mapRuleVariables
155+
)
150156
import Kore.Step.Search
151157
( SearchType (..)
152158
)
@@ -801,7 +807,9 @@ koreMerge execOptions mergeOptions = do
801807
lift $ Text.putStrLn err
802808
return (ExitFailure 1)
803809
(Right mergedRule) -> do
804-
lift $ renderResult execOptions (vsep (map unparse mergedRule))
810+
let mergedRule' =
811+
mergedRule <&> mapRuleVariables getRewritingVariable
812+
lift $ renderResult execOptions (vsep (map unparse mergedRule'))
805813
return ExitSuccess
806814

807815
loadRuleIds :: FilePath -> IO [Text]

‎kore/src/Kore/Builtin/AssocComm/CeilSimplifier.hs

Lines changed: 47 additions & 43 deletions
Original file line numberDiff line numberDiff line change
@@ -63,6 +63,9 @@ import Kore.Internal.TermLike
6363
, termLikeSort
6464
)
6565
import qualified Kore.Internal.TermLike as TermLike
66+
import Kore.Rewriting.RewritingVariable
67+
( RewritingVariableName
68+
)
6669
import qualified Kore.Step.Simplification.AndPredicates as And
6770
import Kore.Step.Simplification.CeilSimplifier
6871
import qualified Kore.Step.Simplification.Equals as Equals
@@ -87,13 +90,12 @@ type MkNotMember normalized variable =
8790
-> Predicate variable
8891

8992
newSetCeilSimplifier
90-
:: forall variable simplifier
91-
. InternalVariable variable
92-
=> MonadReader (SideCondition variable) simplifier
93+
:: forall simplifier
94+
. MonadReader (SideCondition RewritingVariableName) simplifier
9395
=> MonadSimplify simplifier
9496
=> CeilSimplifier simplifier
95-
(BuiltinAssocComm NormalizedSet variable)
96-
(OrCondition variable)
97+
(BuiltinAssocComm NormalizedSet RewritingVariableName)
98+
(OrCondition RewritingVariableName)
9799
newSetCeilSimplifier =
98100
CeilSimplifier $ \ceil@Ceil { ceilChild } -> do
99101
let mkInternalAc normalizedAc =
@@ -114,13 +116,12 @@ newSetCeilSimplifier =
114116
ceil
115117

116118
newMapCeilSimplifier
117-
:: forall variable simplifier
118-
. InternalVariable variable
119-
=> MonadReader (SideCondition variable) simplifier
119+
:: forall simplifier
120+
. MonadReader (SideCondition RewritingVariableName) simplifier
120121
=> MonadSimplify simplifier
121122
=> CeilSimplifier simplifier
122-
(BuiltinAssocComm NormalizedMap variable)
123-
(OrCondition variable)
123+
(BuiltinAssocComm NormalizedMap RewritingVariableName)
124+
(OrCondition RewritingVariableName)
124125
newMapCeilSimplifier =
125126
CeilSimplifier $ \ceil@Ceil { ceilChild } -> do
126127
let mkInternalAc normalizedAc =
@@ -173,22 +174,22 @@ generalizeMapElement freeVariables' element =
173174
variable = refreshElementVariable avoiding x & fromMaybe x
174175

175176
newBuiltinAssocCommCeilSimplifier
176-
:: forall normalized variable simplifier
177-
. InternalVariable variable
178-
=> MonadReader (SideCondition variable) simplifier
177+
:: forall normalized simplifier
178+
. MonadReader (SideCondition RewritingVariableName) simplifier
179179
=> MonadSimplify simplifier
180180
=> Traversable (Value normalized)
181181
=> AcWrapper normalized
182-
=> MkBuiltinAssocComm normalized variable
183-
-> MkNotMember normalized variable
182+
=> MkBuiltinAssocComm normalized RewritingVariableName
183+
-> MkNotMember normalized RewritingVariableName
184184
-> CeilSimplifier simplifier
185-
(BuiltinAssocComm normalized variable)
186-
(OrCondition variable)
185+
(BuiltinAssocComm normalized RewritingVariableName)
186+
(OrCondition RewritingVariableName)
187187
newBuiltinAssocCommCeilSimplifier mkBuiltin mkNotMember =
188188
CeilSimplifier $ \Ceil { ceilChild } -> do
189189
let internalAc@InternalAc { builtinAcChild } = ceilChild
190190
sideCondition <- Reader.ask
191-
let normalizedAc :: NormalizedAc normalized Key (TermLike variable)
191+
let normalizedAc
192+
:: NormalizedAc normalized Key (TermLike RewritingVariableName)
192193
normalizedAc = unwrapAc builtinAcChild
193194
NormalizedAc
194195
{ elementsWithVariables = abstractElements
@@ -198,9 +199,9 @@ newBuiltinAssocCommCeilSimplifier mkBuiltin mkNotMember =
198199
= normalizedAc
199200

200201
let defineOpaquePair
201-
:: TermLike variable
202-
-> TermLike variable
203-
-> MultiAnd (OrCondition variable)
202+
:: TermLike RewritingVariableName
203+
-> TermLike RewritingVariableName
204+
-> MultiAnd (OrCondition RewritingVariableName)
204205
defineOpaquePair opaque1 opaque2 =
205206
internalAc
206207
{ builtinAcChild =
@@ -217,37 +218,40 @@ newBuiltinAssocCommCeilSimplifier mkBuiltin mkNotMember =
217218
& MultiAnd.singleton
218219

219220
defineOpaquePairs
220-
:: TermLike variable
221-
-> [TermLike variable]
222-
-> MultiAnd (OrCondition variable)
221+
:: TermLike RewritingVariableName
222+
-> [TermLike RewritingVariableName]
223+
-> MultiAnd (OrCondition RewritingVariableName)
223224
defineOpaquePairs this others =
224225
foldMap (defineOpaquePair this) others
225226

226-
definedOpaquePairs :: MultiAnd (OrCondition variable)
227+
definedOpaquePairs :: MultiAnd (OrCondition RewritingVariableName)
227228
definedOpaquePairs =
228229
mconcat
229230
$ zipWith defineOpaquePairs opaque
230231
$ tail $ List.tails opaque
231232

232233
let abstractKeys, concreteKeys
233-
:: [TermLike variable]
234+
:: [TermLike RewritingVariableName]
234235
abstractValues, concreteValues, allValues
235-
:: [Value normalized (TermLike variable)]
236+
:: [Value normalized (TermLike RewritingVariableName)]
236237
(abstractKeys, abstractValues) =
237238
unzip (unwrapElement <$> abstractElements)
238239
concreteKeys = from @Key <$> Map.keys concreteElements
239240
concreteValues = Map.elems concreteElements
240241
allValues = concreteValues <> abstractValues
241242

242243
let makeEvaluateTerm, defineAbstractKey, defineOpaque
243-
:: TermLike variable -> MaybeT simplifier (OrCondition variable)
244+
:: TermLike RewritingVariableName
245+
-> MaybeT simplifier (OrCondition RewritingVariableName)
244246
makeEvaluateTerm = makeEvaluateTermCeil sideCondition
245247
defineAbstractKey = makeEvaluateTerm
246248
defineOpaque = makeEvaluateTerm
247249

248250
defineValue
249-
:: Value normalized (TermLike variable)
250-
-> MaybeT simplifier (MultiAnd (OrCondition variable))
251+
:: Value normalized (TermLike RewritingVariableName)
252+
-> MaybeT
253+
simplifier
254+
(MultiAnd (OrCondition RewritingVariableName))
251255
defineValue = foldlM worker mempty
252256
where
253257
worker multiAnd termLike = do
@@ -267,7 +271,7 @@ newBuiltinAssocCommCeilSimplifier mkBuiltin mkNotMember =
267271
zipWithM distinctKey
268272
abstractKeys
269273
(tail $ List.tails abstractKeys)
270-
let conditions :: MultiAnd (OrCondition variable)
274+
let conditions :: MultiAnd (OrCondition RewritingVariableName)
271275
conditions =
272276
mconcat
273277
[ MultiAnd.make definedKeys
@@ -283,16 +287,16 @@ newBuiltinAssocCommCeilSimplifier mkBuiltin mkNotMember =
283287
where
284288

285289
distinctKey
286-
:: TermLike variable
287-
-> [TermLike variable]
288-
-> MaybeT simplifier (MultiAnd (OrCondition variable))
290+
:: TermLike RewritingVariableName
291+
-> [TermLike RewritingVariableName]
292+
-> MaybeT simplifier (MultiAnd (OrCondition RewritingVariableName))
289293
distinctKey thisKey otherKeys =
290294
MultiAnd.make <$> traverse (notEquals thisKey) otherKeys
291295

292296
notEquals
293-
:: TermLike variable
294-
-> TermLike variable
295-
-> MaybeT simplifier (OrCondition variable)
297+
:: TermLike RewritingVariableName
298+
-> TermLike RewritingVariableName
299+
-> MaybeT simplifier (OrCondition RewritingVariableName)
296300
notEquals t1 t2 = do
297301
sideCondition <- Reader.ask
298302
Equals.makeEvaluateTermsToPredicate tMin tMax sideCondition
@@ -302,18 +306,18 @@ newBuiltinAssocCommCeilSimplifier mkBuiltin mkNotMember =
302306
(tMin, tMax) = minMax t1 t2
303307

304308
notMember
305-
:: TermLike variable
306-
-> Element normalized (TermLike variable)
307-
-> MultiAnd (OrCondition variable)
309+
:: TermLike RewritingVariableName
310+
-> Element normalized (TermLike RewritingVariableName)
311+
-> MultiAnd (OrCondition RewritingVariableName)
308312
notMember termLike element =
309313
mkNotMember element termLike
310314
& OrCondition.fromPredicate
311315
& MultiAnd.singleton
312316

313317
notMembers
314-
:: NormalizedAc normalized Key (TermLike variable)
315-
-> TermLike variable
316-
-> MultiAnd (OrCondition variable)
318+
:: NormalizedAc normalized Key (TermLike RewritingVariableName)
319+
-> TermLike RewritingVariableName
320+
-> MultiAnd (OrCondition RewritingVariableName)
317321
notMembers normalizedAc termLike =
318322
Lens.foldMapOf foldElements (notMember termLike) normalizedAc
319323

0 commit comments

Comments
 (0)