Skip to content

Commit eefb9b4

Browse files
emarzionttuegelgithub-actionsana-pantilie
authored
Continuation of Unification Loop Refactor (#2643)
Co-authored-by: Thomas Tuegel <ttuegel@mailbox.org> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: Thomas Tuegel <thomas.tuegel@runtimeverification.com> Co-authored-by: ana-pantilie <45069775+ana-pantilie@users.noreply.github.com>
1 parent 0521b0e commit eefb9b4

File tree

18 files changed

+1417
-932
lines changed

18 files changed

+1417
-932
lines changed

‎kore/src/Kore/Builtin/AssociativeCommutative.hs‎

Lines changed: 222 additions & 107 deletions
Large diffs are not rendered by default.

‎kore/src/Kore/Builtin/Bool.hs‎

Lines changed: 64 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -169,6 +169,7 @@ builtinFunctions =
169169

170170
data UnifyBool = UnifyBool
171171
{ bool1, bool2 :: !InternalBool
172+
, term1, term2 :: !(TermLike RewritingVariableName)
172173
}
173174

174175
{- | Matches
@@ -187,31 +188,34 @@ matchBools ::
187188
TermLike RewritingVariableName ->
188189
TermLike RewritingVariableName ->
189190
Maybe UnifyBool
190-
matchBools first second
191-
| InternalBool_ bool1 <- first
192-
, InternalBool_ bool2 <- second =
193-
Just UnifyBool{bool1, bool2}
191+
matchBools term1 term2
192+
| InternalBool_ bool1 <- term2
193+
, InternalBool_ bool2 <- term1 =
194+
Just UnifyBool{bool1, bool2, term1, term2}
194195
| otherwise = Nothing
195196
{-# INLINE matchBools #-}
196197

197198
-- | When bool values are equal, returns first term; otherwise returns bottom.
198199
unifyBool ::
199200
forall unifier.
200201
MonadUnify unifier =>
201-
TermLike RewritingVariableName ->
202-
TermLike RewritingVariableName ->
203202
UnifyBool ->
204203
unifier (Pattern RewritingVariableName)
205-
unifyBool termLike1 termLike2 unifyData
204+
unifyBool unifyData
206205
| bool1 == bool2 =
207-
return (Pattern.fromTermLike termLike1)
206+
return (Pattern.fromTermLike term1)
208207
| otherwise =
209208
debugUnifyBottomAndReturnBottom
210209
"different Bool domain values"
211-
termLike1
212-
termLike2
210+
term1
211+
term2
213212
where
214-
UnifyBool{bool1, bool2} = unifyData
213+
UnifyBool{bool1, bool2, term1, term2} = unifyData
214+
215+
data UnifyBoolAnd = UnifyBoolAnd
216+
{ term :: !(TermLike RewritingVariableName)
217+
, boolAnd :: !BoolAnd
218+
}
215219

216220
{- | Matches
217221
@@ -222,18 +226,24 @@ unifyBool termLike1 termLike2 unifyData
222226
and
223227
224228
@
225-
\\and{_}(\\dv{Bool}("true"), andBool(_,_))
229+
\\and{_}(\\dv{Bool}("true"), andBool(_,_)),
226230
@
231+
232+
symmetric in the two arguments.
227233
-}
228234
matchUnifyBoolAnd ::
229235
TermLike RewritingVariableName ->
230236
TermLike RewritingVariableName ->
231-
Maybe BoolAnd
237+
Maybe UnifyBoolAnd
232238
matchUnifyBoolAnd first second
233239
| Just True <- matchBool first
234240
, Just boolAnd <- matchBoolAnd second
235241
, isFunctionPattern second =
236-
Just boolAnd
242+
Just $ UnifyBoolAnd{term = first, boolAnd}
243+
| Just True <- matchBool second
244+
, Just boolAnd <- matchBoolAnd first
245+
, isFunctionPattern first =
246+
Just $ UnifyBoolAnd{term = second, boolAnd}
237247
| otherwise =
238248
Nothing
239249
{-# INLINE matchUnifyBoolAnd #-}
@@ -242,12 +252,12 @@ unifyBoolAnd ::
242252
forall unifier.
243253
MonadUnify unifier =>
244254
TermSimplifier RewritingVariableName unifier ->
245-
TermLike RewritingVariableName ->
246-
BoolAnd ->
255+
UnifyBoolAnd ->
247256
unifier (Pattern RewritingVariableName)
248-
unifyBoolAnd unifyChildren term boolAnd =
257+
unifyBoolAnd unifyChildren unifyData =
249258
unifyBothWith unifyChildren term operand1 operand2
250259
where
260+
UnifyBoolAnd{term, boolAnd} = unifyData
251261
BoolAnd{operand1, operand2} = boolAnd
252262

253263
{- |Takes a (function-like) pattern and unifies it against two other patterns.
@@ -275,6 +285,11 @@ unifyBothWith unify termLike1 operand1 operand2 = do
275285
unify' term1 term2 =
276286
Pattern.withoutTerm <$> unify term1 term2
277287

288+
data UnifyBoolOr = UnifyBoolOr
289+
{ term :: !(TermLike RewritingVariableName)
290+
, boolOr :: !BoolOr
291+
}
292+
278293
{- | Matches
279294
280295
@
@@ -284,36 +299,42 @@ unifyBothWith unify termLike1 operand1 operand2 = do
284299
and
285300
286301
@
287-
\\and{_}(\\dv{Bool}("false"), boolOr(_,_))
302+
\\and{_}(\\dv{Bool}("false"), boolOr(_,_)),
288303
@
304+
305+
symmetric in the two arguments.
289306
-}
290307
matchUnifyBoolOr ::
291308
TermLike RewritingVariableName ->
292309
TermLike RewritingVariableName ->
293-
Maybe BoolOr
310+
Maybe UnifyBoolOr
294311
matchUnifyBoolOr first second
295312
| Just False <- matchBool first
296313
, Just boolOr <- matchBoolOr second
297314
, isFunctionPattern second =
298-
Just boolOr
315+
Just UnifyBoolOr{term = first, boolOr}
316+
| Just False <- matchBool second
317+
, Just boolOr <- matchBoolOr first
318+
, isFunctionPattern first =
319+
Just UnifyBoolOr{term = second, boolOr}
299320
| otherwise = Nothing
300321
{-# INLINE matchUnifyBoolOr #-}
301322

302323
unifyBoolOr ::
303324
forall unifier.
304325
MonadUnify unifier =>
305326
TermSimplifier RewritingVariableName unifier ->
306-
TermLike RewritingVariableName ->
307-
BoolOr ->
327+
UnifyBoolOr ->
308328
unifier (Pattern RewritingVariableName)
309-
unifyBoolOr unifyChildren termLike boolOr =
310-
unifyBothWith unifyChildren termLike operand1 operand2
329+
unifyBoolOr unifyChildren unifyData =
330+
unifyBothWith unifyChildren term operand1 operand2
311331
where
332+
UnifyBoolOr{term, boolOr} = unifyData
312333
BoolOr{operand1, operand2} = boolOr
313334

314335
data UnifyBoolNot = UnifyBoolNot
315-
{ boolNot :: BoolNot
316-
, value :: Bool
336+
{ boolNot :: !BoolNot
337+
, value :: !InternalBool
317338
}
318339

319340
{- | Matches
@@ -325,8 +346,10 @@ data UnifyBoolNot = UnifyBoolNot
325346
and
326347
327348
@
328-
\\and{_}(notBool(_), \\dv{Bool}(_))
349+
\\and{_}(notBool(_), \\dv{Bool}(_)),
329350
@
351+
352+
symmetric in the two arguments.
330353
-}
331354
matchUnifyBoolNot ::
332355
TermLike RewritingVariableName ->
@@ -335,24 +358,33 @@ matchUnifyBoolNot ::
335358
matchUnifyBoolNot first second
336359
| Just boolNot <- matchBoolNot first
337360
, isFunctionPattern first
338-
, Just value <- matchBool second =
339-
Just $ UnifyBoolNot boolNot value
361+
, Just value <- matchInternalBool second =
362+
Just UnifyBoolNot{boolNot, value}
363+
| Just boolNot <- matchBoolNot second
364+
, isFunctionPattern second
365+
, Just value <- matchInternalBool first =
366+
Just UnifyBoolNot{boolNot, value}
340367
| otherwise = Nothing
341368
{-# INLINE matchUnifyBoolNot #-}
342369

343370
unifyBoolNot ::
344371
forall unifier.
345372
TermSimplifier RewritingVariableName unifier ->
346-
TermLike RewritingVariableName ->
347373
UnifyBoolNot ->
348374
unifier (Pattern RewritingVariableName)
349-
unifyBoolNot unifyChildren term unifyData =
350-
let notValue = asInternal (termLikeSort term) (not value)
375+
unifyBoolNot unifyChildren unifyData =
376+
let notValue = asInternal internalBoolSort (not internalBoolValue)
351377
in unifyChildren notValue operand
352378
where
353379
UnifyBoolNot{boolNot, value} = unifyData
380+
InternalBool{internalBoolValue, internalBoolSort} = value
354381
BoolNot{operand} = boolNot
355382

383+
matchInternalBool :: TermLike variable -> Maybe InternalBool
384+
matchInternalBool (InternalBool_ internalBool) =
385+
Just internalBool
386+
matchInternalBool _ = Nothing
387+
356388
-- | Match a @BOOL.Bool@ builtin value.
357389
matchBool :: TermLike variable -> Maybe Bool
358390
matchBool (InternalBool_ InternalBool{internalBoolValue}) =

‎kore/src/Kore/Builtin/Endianness.hs‎

Lines changed: 29 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -7,12 +7,10 @@ module Kore.Builtin.Endianness (
77
littleEndianKey,
88
bigEndianKey,
99
unifyEquals,
10+
matchUnifyEqualsEndianness,
1011
module Kore.Builtin.Endianness.Endianness,
1112
) where
1213

13-
import Control.Error (
14-
MaybeT,
15-
)
1614
import Data.Functor.Const
1715
import qualified Data.HashMap.Strict as HashMap
1816
import Data.String (
@@ -31,6 +29,7 @@ import Kore.Internal.TermLike
3129
import Kore.Log.DebugUnifyBottom (
3230
debugUnifyBottomAndReturnBottom,
3331
)
32+
import Kore.Rewrite.RewritingVariable
3433
import Kore.Unification.Unify (
3534
MonadUnify,
3635
)
@@ -77,18 +76,33 @@ littleEndianVerifier = endiannessVerifier LittleEndian
7776
bigEndianVerifier :: ApplicationVerifier Verified.Pattern
7877
bigEndianVerifier = endiannessVerifier BigEndian
7978

79+
data UnifyEqualsEndianness = UnifyEqualsEndianness
80+
{ end1, end2 :: !Endianness
81+
, term1, term2 :: !(TermLike RewritingVariableName)
82+
}
83+
84+
-- | Matches two terms having the Endianness constructor.
85+
matchUnifyEqualsEndianness ::
86+
TermLike RewritingVariableName ->
87+
TermLike RewritingVariableName ->
88+
Maybe UnifyEqualsEndianness
89+
matchUnifyEqualsEndianness term1 term2
90+
| Endianness_ end1 <- term1
91+
, Endianness_ end2 <- term2 =
92+
Just UnifyEqualsEndianness{end1, end2, term1, term2}
93+
| otherwise = Nothing
94+
{-# INLINE matchUnifyEqualsEndianness #-}
95+
8096
unifyEquals ::
81-
InternalVariable variable =>
8297
MonadUnify unifier =>
83-
TermLike variable ->
84-
TermLike variable ->
85-
MaybeT unifier (Pattern variable)
86-
unifyEquals termLike1@(Endianness_ end1) termLike2@(Endianness_ end2)
87-
| end1 == end2 = return (Pattern.fromTermLike termLike1)
98+
UnifyEqualsEndianness ->
99+
unifier (Pattern RewritingVariableName)
100+
unifyEquals unifyData
101+
| end1 == end2 = return (Pattern.fromTermLike term1)
88102
| otherwise =
89-
lift $
90-
debugUnifyBottomAndReturnBottom
91-
"Cannot unify distinct constructors."
92-
termLike1
93-
termLike2
94-
unifyEquals _ _ = empty
103+
debugUnifyBottomAndReturnBottom
104+
"Cannot unify distinct constructors."
105+
term1
106+
term2
107+
where
108+
UnifyEqualsEndianness{end1, end2, term1, term2} = unifyData

‎kore/src/Kore/Builtin/EqTerm.hs‎

Lines changed: 8 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -8,11 +8,7 @@ module Kore.Builtin.EqTerm (
88
unifyEqTerm,
99
) where
1010

11-
import Control.Error (
12-
MaybeT,
13-
)
1411
import qualified Control.Monad as Monad
15-
import qualified Kore.Builtin.Bool as Bool
1612
import qualified Kore.Internal.MultiOr as MultiOr
1713
import qualified Kore.Internal.OrPattern as OrPattern
1814
import Kore.Internal.Pattern (
@@ -61,16 +57,14 @@ unifyEqTerm ::
6157
TermSimplifier RewritingVariableName unifier ->
6258
NotSimplifier unifier ->
6359
EqTerm (TermLike RewritingVariableName) ->
64-
TermLike RewritingVariableName ->
65-
MaybeT unifier (Pattern RewritingVariableName)
66-
unifyEqTerm unifyChildren (NotSimplifier notSimplifier) eqTerm termLike2
67-
| Just value2 <- Bool.matchBool termLike2 =
68-
lift $ do
69-
solution <- unifyChildren operand1 operand2 & OrPattern.gather
70-
let solution' = MultiOr.map eraseTerm solution
71-
(if value2 then pure else notSimplifier SideCondition.top) solution'
72-
>>= Unify.scatter
73-
| otherwise = empty
60+
Bool ->
61+
unifier (Pattern RewritingVariableName)
62+
unifyEqTerm unifyChildren (NotSimplifier notSimplifier) eqTerm value =
63+
do
64+
solution <- unifyChildren operand1 operand2 & OrPattern.gather
65+
let solution' = MultiOr.map eraseTerm solution
66+
(if value then pure else notSimplifier SideCondition.top) solution'
67+
>>= Unify.scatter
7468
where
7569
EqTerm{operand1, operand2} = eqTerm
7670
eraseTerm = Pattern.fromCondition_ . Pattern.withoutTerm

‎kore/src/Kore/Builtin/Int.hs‎

Lines changed: 14 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -435,6 +435,7 @@ matchIntEqual =
435435

436436
data UnifyInt = UnifyInt
437437
{ int1, int2 :: !InternalInt
438+
, term1, term2 :: !(TermLike RewritingVariableName)
438439
}
439440

440441
{- | Matches
@@ -453,25 +454,23 @@ matchInt ::
453454
TermLike RewritingVariableName ->
454455
TermLike RewritingVariableName ->
455456
Maybe UnifyInt
456-
matchInt first second
457-
| InternalInt_ int1 <- first
458-
, InternalInt_ int2 <- second =
459-
Just UnifyInt{int1, int2}
457+
matchInt term1 term2
458+
| InternalInt_ int1 <- term1
459+
, InternalInt_ int2 <- term2 =
460+
Just UnifyInt{int1, int2, term1, term2}
460461
| otherwise = Nothing
461462
{-# INLINE matchInt #-}
462463

463464
-- | When int values are equal, returns first term; otherwise returns bottom.
464465
unifyInt ::
465466
forall unifier.
466467
MonadUnify unifier =>
467-
TermLike RewritingVariableName ->
468-
TermLike RewritingVariableName ->
469468
UnifyInt ->
470469
unifier (Pattern RewritingVariableName)
471-
unifyInt term1 term2 unifyData =
470+
unifyInt unifyData =
472471
assert (on (==) internalIntSort int1 int2) worker
473472
where
474-
UnifyInt{int1, int2} = unifyData
473+
UnifyInt{int1, int2, term1, term2} = unifyData
475474
worker :: unifier (Pattern RewritingVariableName)
476475
worker
477476
| on (==) internalIntValue int1 int2 =
@@ -486,8 +485,10 @@ data UnifyIntEq = UnifyIntEq
486485

487486
{- | Matches
488487
@
489-
\\equals{_, _}(eqInt{_}(_, _), \\dv{Bool}(_))
488+
\\equals{_, _}(eqInt{_}(_, _), \\dv{Bool}(_)),
490489
@
490+
491+
symmetric in the two arguments.
491492
-}
492493
matchUnifyIntEq ::
493494
TermLike RewritingVariableName ->
@@ -498,6 +499,10 @@ matchUnifyIntEq first second
498499
, isFunctionPattern first
499500
, InternalBool_ internalBool <- second =
500501
Just UnifyIntEq{eqTerm, internalBool}
502+
| Just eqTerm <- matchIntEqual second
503+
, isFunctionPattern second
504+
, InternalBool_ internalBool <- first =
505+
Just UnifyIntEq{eqTerm, internalBool}
501506
| otherwise = Nothing
502507
{-# INLINE matchUnifyIntEq #-}
503508

0 commit comments

Comments
 (0)