Skip to content

Commit a5206ba

Browse files
committed
add 'not-implemented' implementation of MAP.updateAll to kore
1 parent f501d87 commit a5206ba

File tree

2 files changed

+9
-0
lines changed

2 files changed

+9
-0
lines changed

kore/src/Kore/Builtin/Map.hs

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -204,6 +204,10 @@ symbolVerifiers =
204204
assertSort
205205
[assertSort, acceptAnySort, acceptAnySort]
206206
)
207+
,
208+
( Map.updateAllKey
209+
, Builtin.verifySymbol assertSort [assertSort, assertSort]
210+
)
207211
,
208212
( Map.in_keysKey
209213
, Builtin.verifySymbol Bool.assertSort [acceptAnySort, assertSort]
@@ -486,6 +490,7 @@ builtinFunctions key
486490
| key == Map.elementKey = Just $ Builtin.functionEvaluator evalElement
487491
| key == Map.unitKey = Just $ Builtin.functionEvaluator evalUnit
488492
| key == Map.updateKey = Just $ Builtin.functionEvaluator evalUpdate
493+
| key == Map.updateAllKey = Just $ Builtin.notImplemented
489494
| key == Map.in_keysKey = Just $ Builtin.functionEvaluator evalInKeys
490495
| key == Map.keysKey = Just $ Builtin.functionEvaluator evalKeys
491496
| key == Map.keys_listKey = Just $ Builtin.functionEvaluator evalKeysList

kore/src/Kore/Builtin/Map/Map.hs

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -34,6 +34,7 @@ module Kore.Builtin.Map.Map (
3434
removeKey,
3535
unitKey,
3636
updateKey,
37+
updateAllKey,
3738
sizeKey,
3839
valuesKey,
3940
inclusionKey,
@@ -73,6 +74,9 @@ unitKey = "MAP.unit"
7374
updateKey :: IsString s => s
7475
updateKey = "MAP.update"
7576

77+
updateAllKey :: IsString s => s
78+
updateAllKey = "MAP.updateAll"
79+
7680
in_keysKey :: IsString s => s
7781
in_keysKey = "MAP.in_keys"
7882

0 commit comments

Comments
 (0)