[RED] Test.Kore.Internal.Key

Author: ttuegel

kore/kore.cabal

@@ -1,6 +1,6 @@
 cabal-version: 2.2
 
--- This file has been generated from package.yaml by hpack version 0.34.1.
+-- This file has been generated from package.yaml by hpack version 0.34.2.
 --
 -- see: https://github.com/sol/hpack
 
@@ -954,6 +954,7 @@ test-suite kore-test
       Test.Kore.IndexedModule.SortGraph
       Test.Kore.Internal.ApplicationSorts
       Test.Kore.Internal.Condition
+      Test.Kore.Internal.Key
       Test.Kore.Internal.MultiAnd
       Test.Kore.Internal.OrCondition
       Test.Kore.Internal.OrPattern

kore/test/Test/Kore/Internal/Key.hs

@@ -0,0 +1,51 @@
+module Test.Kore.Internal.Key
+    ( test_retractKey
+    ) where
+
+import Prelude.Kore
+
+import Test.Tasty
+
+import Kore.Internal.TermLike
+    ( Concrete
+    , DomainValue (..)
+    , TermLike
+    , mkDomainValue
+    , mkStringLiteral
+    , retractKey
+    )
+
+import Test.Kore.Builtin.Definition
+    ( mkBool
+    , mkBytes
+    , mkInt
+    , mkList
+    , mkMap
+    , mkSet_
+    , mkString
+    , userTokenSort
+    )
+import Test.Tasty.HUnit.Ext
+
+test_retractKey :: [TestTree]
+test_retractKey =
+    [ test "Int" (mkInt 1)
+    , test "Bool" (mkBool True)
+    , test "String" (mkString "string")
+    , test "Bytes" (mkBytes [0x00, 0xFF])
+    , test "Set" (mkSet_ [mkInt 1])
+    , test "Map" (mkMap [(mkInt 1, mkString "one")])
+    , test "List" (mkList [mkInt 1, mkInt 2])
+    , test "token"
+        (mkDomainValue DomainValue
+            { domainValueSort = userTokenSort
+            , domainValueChild = mkStringLiteral "token"
+            }
+        )
+    ]
+  where
+    test :: HasCallStack => TestName -> TermLike Concrete -> TestTree
+    test testName term =
+        testCase testName $ do
+            let actual = retractKey term
+            assertBool "expected key" (isJust actual)