Skip to content

Commit 0b6711d

Browse files
ttuegelttuegel
committed
Add more helpers to test Kore definition
1 parent c540121 commit 0b6711d

File tree

4 files changed

+118
-74
lines changed

4 files changed

+118
-74
lines changed

‎kore/test/Test/Kore/Builtin/Definition.hs

Lines changed: 57 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -8,12 +8,22 @@ module Test.Kore.Builtin.Definition where
88
import Prelude.Kore
99

1010
import qualified Data.Bifunctor as Bifunctor
11+
import Data.ByteString
12+
( ByteString
13+
)
14+
import qualified Data.ByteString as ByteString
1115
import qualified Data.Default as Default
1216
import qualified Data.Map.Strict as Map
17+
import Data.Maybe
18+
( fromJust
19+
)
1320
import qualified Data.Sequence as Seq
1421
import Data.Text
1522
( Text
1623
)
24+
import Data.Word
25+
( Word8
26+
)
1727

1828
import Kore.Attribute.Constructor
1929
import Kore.Attribute.Functional
@@ -38,10 +48,12 @@ import qualified Kore.Builtin.Endianness as Endianness
3848
import qualified Kore.Builtin.Signedness as Signedness
3949
import Kore.Internal.ApplicationSorts
4050
import Kore.Internal.InternalBool
51+
import Kore.Internal.InternalBytes
4152
import Kore.Internal.InternalInt
4253
import Kore.Internal.InternalList
4354
import Kore.Internal.InternalMap
4455
import Kore.Internal.InternalSet
56+
import Kore.Internal.InternalString
4557
import Kore.Internal.Symbol
4658
( constructor
4759
, function
@@ -56,7 +68,6 @@ import Kore.Internal.Symbol
5668
import qualified Kore.Internal.Symbol as Internal
5769
import Kore.Internal.TermLike hiding
5870
( Symbol
59-
, bytesSort
6071
)
6172
import Kore.Syntax
6273
( Const (..)
@@ -1015,6 +1026,9 @@ builtinBool internalBoolValue =
10151026
, internalBoolValue
10161027
}
10171028

1029+
mkBool :: InternalVariable variable => Bool -> TermLike variable
1030+
mkBool = mkInternalBool . builtinBool
1031+
10181032
-- ** Int
10191033

10201034
-- | A sort to hook to the builtin @INT.Int@.
@@ -1038,6 +1052,9 @@ builtinInt internalIntValue =
10381052
, internalIntValue
10391053
}
10401054

1055+
mkInt :: InternalVariable variable => Integer -> TermLike variable
1056+
mkInt = mkInternalInt . builtinInt
1057+
10411058
-- ** KEQUAL
10421059

10431060
kSort :: Sort
@@ -1083,9 +1100,7 @@ listSortDecl =
10831100
, concatAttribute concatListSymbol
10841101
]
10851102

1086-
builtinList
1087-
:: [TermLike VariableName]
1088-
-> InternalList (TermLike VariableName)
1103+
builtinList :: [TermLike variable] -> InternalList (TermLike variable)
10891104
builtinList children =
10901105
InternalList
10911106
{ internalListSort = listSort
@@ -1095,6 +1110,9 @@ builtinList children =
10951110
, internalListChild = Seq.fromList children
10961111
}
10971112

1113+
mkList :: InternalVariable variable => [TermLike variable] -> TermLike variable
1114+
mkList = mkInternalList . builtinList
1115+
10981116
-- | Another sort with the same hook
10991117
listSort2 :: Sort
11001118
listSort2 =
@@ -1137,8 +1155,8 @@ mapSortDecl =
11371155

11381156
builtinMap
11391157
:: Ord key
1140-
=> [(key, TermLike VariableName)]
1141-
-> InternalMap key (TermLike VariableName)
1158+
=> [(key, TermLike variable)]
1159+
-> InternalMap key (TermLike variable)
11421160
builtinMap children =
11431161
InternalAc
11441162
{ builtinAcSort = mapSort
@@ -1153,6 +1171,15 @@ builtinMap children =
11531171
}
11541172
}
11551173

1174+
mkMap
1175+
:: InternalVariable variable
1176+
=> [(TermLike Concrete, TermLike variable)]
1177+
-> TermLike variable
1178+
mkMap =
1179+
mkInternalMap
1180+
. builtinMap
1181+
. (map . Bifunctor.first) (retractKey >>> fromJust)
1182+
11561183
-- ** Pair
11571184

11581185
pairSort :: Sort -> Sort -> Sort
@@ -1213,13 +1240,13 @@ testSort =
12131240
testSortDecl :: ParsedSentence
12141241
testSortDecl = sortDecl testSort
12151242

1216-
builtinSet
1243+
mkSet
12171244
:: InternalVariable variable
12181245
=> Foldable f
12191246
=> f (TermLike variable)
12201247
-> [TermLike variable]
12211248
-> TermLike variable
1222-
builtinSet elements opaque =
1249+
mkSet elements opaque =
12231250
mkInternalSet InternalAc
12241251
{ builtinAcSort = setSort
12251252
, builtinAcUnit = unitSetSymbol
@@ -1239,12 +1266,12 @@ builtinSet elements opaque =
12391266
asKey <$> toList elements
12401267
& partitionEithers
12411268

1242-
builtinSet_
1269+
mkSet_
12431270
:: InternalVariable variable
12441271
=> Foldable f
12451272
=> f (TermLike variable)
12461273
-> TermLike variable
1247-
builtinSet_ items = builtinSet items []
1274+
mkSet_ items = mkSet items []
12481275

12491276
-- ** String
12501277

@@ -1277,6 +1304,16 @@ userTokenSortDecl =
12771304
userTokenSort
12781305
[ hasDomainValuesAttribute ]
12791306

1307+
mkString :: InternalVariable variable => Text -> TermLike variable
1308+
mkString = mkInternalString . internalString
1309+
1310+
internalString :: Text -> InternalString
1311+
internalString internalStringValue =
1312+
InternalString
1313+
{ internalStringSort = stringSort
1314+
, internalStringValue
1315+
}
1316+
12801317
-- ** Bytes
12811318

12821319
bytesSort :: Sort
@@ -1313,6 +1350,16 @@ signednessSort =
13131350
signednessSortDecl :: ParsedSentence
13141351
signednessSortDecl = sortDecl signednessSort
13151352

1353+
builtinBytes :: ByteString -> InternalBytes
1354+
builtinBytes internalBytesValue =
1355+
InternalBytes
1356+
{ internalBytesSort = bytesSort
1357+
, internalBytesValue
1358+
}
1359+
1360+
mkBytes :: InternalVariable variable => [Word8] -> TermLike variable
1361+
mkBytes = mkInternalBytes' . builtinBytes . ByteString.pack
1362+
13161363
-- -------------------------------------------------------------
13171364
-- * Modules
13181365

‎kore/test/Test/Kore/Builtin/List.hs

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -462,9 +462,6 @@ test_updateAll =
462462
where
463463
original = asInternal . fmap mkInt $ Seq.fromList [1, 2, 3]
464464

465-
mkInt :: Integer -> TermLike VariableName
466-
mkInt = Test.Int.asInternal
467-
468465
-- | Specialize 'List.asPattern' to the builtin sort 'listSort'.
469466
asTermLike
470467
:: Foldable f

‎kore/test/Test/Kore/Builtin/Map.hs

Lines changed: 18 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -290,8 +290,8 @@ test_removeAll =
290290
when (set == Set.empty) discard
291291
let key = Set.elemAt 0 set
292292
diffSet = Set.delete key set
293-
patSet = builtinSet_ set & fromConcrete
294-
patDiffSet = builtinSet_ diffSet & fromConcrete
293+
patSet = mkSet_ set & fromConcrete
294+
patDiffSet = mkSet_ diffSet & fromConcrete
295295
patKey = fromConcrete key
296296
patRemoveAll1 = removeAllMap map' patSet
297297
patRemoveAll2 = removeAllMap
@@ -422,7 +422,7 @@ test_keysUnit =
422422
let
423423
patUnit = unitMap
424424
patKeys = keysMap patUnit
425-
patExpect = builtinSet_ Set.empty
425+
patExpect = mkSet_ Set.empty
426426
predicate = mkEquals_ patExpect patKeys
427427
expect <- evaluate patExpect
428428
assertEqual "" expect =<< evaluate patKeys
@@ -436,7 +436,7 @@ test_keysElement =
436436
key <- forAll genIntegerKey
437437
val <- forAll genIntegerPattern
438438
let patMap = asTermLike $ Map.singleton key val
439-
patKeys = builtinSet_ (Set.singleton $ from key) & fromConcrete
439+
patKeys = mkSet_ (Set.singleton $ from key) & fromConcrete
440440
patSymbolic = keysMap patMap
441441
predicate = mkEquals_ patKeys patSymbolic
442442
expect <- evaluateT patKeys
@@ -451,7 +451,7 @@ test_keys =
451451
(do
452452
map1 <- forAll (genConcreteMap genIntegerPattern)
453453
let keys1 = Map.keysSet map1 & Set.map from
454-
patConcreteKeys = builtinSet_ keys1 & fromConcrete
454+
patConcreteKeys = mkSet_ keys1 & fromConcrete
455455
patMap = asTermLike map1
456456
patSymbolicKeys = keysMap patMap
457457
predicate = mkEquals_ patConcreteKeys patSymbolicKeys
@@ -1227,23 +1227,23 @@ test_concretizeKeysAxiom =
12271227

12281228
test_renormalize :: [TestTree]
12291229
test_renormalize =
1230-
[ unchanged "abstract key is unchanged" (mkMap [(x, v)] [] [])
1230+
[ unchanged "abstract key is unchanged" (mkMap' [(x, v)] [] [])
12311231
, becomes "concrete key is normalized"
1232-
(mkMap [(from k1, v)] [] [])
1233-
(mkMap [] [(k1, v)] [])
1232+
(mkMap' [(from k1, v)] [] [])
1233+
(mkMap' [] [(k1, v)] [])
12341234
, becomes "opaque child is flattened"
1235-
(mkMap [] [(k1, v)] [mkMap [] [(k2, v)] []])
1236-
(mkMap [] [(k1, v), (k2, v)] [])
1235+
(mkMap' [] [(k1, v)] [mkMap' [] [(k2, v)] []])
1236+
(mkMap' [] [(k1, v), (k2, v)] [])
12371237
, becomes "child is flattened and normalized"
1238-
(mkMap [] [(k1, v)] [mkMap [(from k2, v)] [] []])
1239-
(mkMap [] [(k1, v), (k2, v)] [])
1238+
(mkMap' [] [(k1, v)] [mkMap' [(from k2, v)] [] []])
1239+
(mkMap' [] [(k1, v), (k2, v)] [])
12401240
, becomes "grandchild is flattened and normalized"
1241-
(mkMap [] [(k1, v)] [mkMap [(x, v)] [] [mkMap [(from k2, v)] [] []]])
1242-
(mkMap [(x, v)] [(k1, v), (k2, v)] [])
1241+
(mkMap' [] [(k1, v)] [mkMap' [(x, v)] [] [mkMap' [(from k2, v)] [] []]])
1242+
(mkMap' [(x, v)] [(k1, v), (k2, v)] [])
12431243
, denorm "duplicate key in map"
1244-
(mkMap [(from k1, v), (from k1, v)] [] [])
1244+
(mkMap' [(from k1, v), (from k1, v)] [] [])
12451245
, denorm "duplicate key in child"
1246-
(mkMap [(from k1, v)] [] [mkMap [(from k1, v)] [] []])
1246+
(mkMap' [(from k1, v)] [] [mkMap' [(from k1, v)] [] []])
12471247
]
12481248
where
12491249
x = mkIntVar (testId "x")
@@ -1279,15 +1279,15 @@ test_renormalize =
12791279
denorm name origin =
12801280
testCase name $ assertEqual "" Nothing (Ac.renormalize origin)
12811281

1282-
mkMap
1282+
mkMap'
12831283
:: [(TermLike VariableName, TermLike VariableName)]
12841284
-- ^ abstract elements
12851285
-> [(Key, TermLike VariableName)]
12861286
-- ^ concrete elements
12871287
-> [NormalizedMap Key (TermLike VariableName)]
12881288
-- ^ opaque terms
12891289
-> NormalizedMap Key (TermLike VariableName)
1290-
mkMap abstract concrete opaque =
1290+
mkMap' abstract concrete opaque =
12911291
wrapAc NormalizedAc
12921292
{ elementsWithVariables = MapElement <$> abstract
12931293
, concreteElements =

0 commit comments

Comments
 (0)