Add hook LIST.make (#2272)

Author: andreiburdusa

docs/hooks.md

@@ -702,6 +702,16 @@ The number of elements in the given list.
         [hook{}("LIST.size")]
 ~~~
 
+### LIST.make
+
+`LIST.make(n, x)` is a list of length `n` with `x` the value of every element.
+The result is `bottom` if n is negative.
+
+~~~
+    hooked-symbol make{}(Int{}, Elem{}) : List{}
+        [hook{}("LIST.make")]
+~~~
+
 ## LIST.updateAll
 
 `LIST.updateAll(L1, index, L2)` creates a new list using a list `L2` of size `N`

kore/src/Kore/Builtin/List.hs

@@ -194,6 +194,9 @@ symbolVerifiers =
     , ( sizeKey
       , Builtin.verifySymbol Int.assertSort [assertSort]
       )
+    , ( makeKey
+      , Builtin.verifySymbol assertSort [Int.assertSort, acceptAnySort]
+      )
     , ( updateAllKey
       , Builtin.verifySymbol assertSort [assertSort, Int.assertSort, assertSort]
       )
@@ -322,6 +325,15 @@ evalSize resultSort [_list] = do
         & return
 evalSize _ _ = Builtin.wrongArity sizeKey
 
+evalMake :: Builtin.Function
+evalMake resultSort [_len, value] = do
+    _len <- fromInteger <$> Int.expectBuiltinInt getKey _len
+    if _len >= 0
+        then
+            returnList resultSort (Seq.replicate _len value)
+        else return (Pattern.bottomOf resultSort)
+evalMake _ _ = Builtin.wrongArity sizeKey
+
 evalUpdateAll :: Builtin.Function
 evalUpdateAll resultSort [_list1, _ix, _list2] = do
     _list1 <- expectBuiltinList getKey _list1
@@ -352,6 +364,7 @@ builtinFunctions =
         , (updateKey, Builtin.functionEvaluator evalUpdate)
         , (inKey, Builtin.functionEvaluator evalIn)
         , (sizeKey, Builtin.functionEvaluator evalSize)
+        , (makeKey, Builtin.functionEvaluator evalMake)
         , (updateAllKey, Builtin.functionEvaluator evalUpdateAll)
         ]
 

kore/src/Kore/Builtin/List/List.hs

@@ -24,6 +24,7 @@ module Kore.Builtin.List.List
     , updateKey
     , inKey
     , sizeKey
+    , makeKey
     , updateAllKey
     ) where
 
@@ -199,5 +200,8 @@ inKey = "LIST.in"
 sizeKey :: IsString s => s
 sizeKey = "LIST.size"
 
+makeKey :: IsString s => s
+makeKey = "LIST.make"
+
 updateAllKey :: IsString s => s
 updateAllKey = "LIST.updateAll"

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

@@ -384,6 +384,10 @@ getListSymbol =
 sizeListSymbol :: Internal.Symbol
 sizeListSymbol = builtinSymbol "sizeList" intSort [listSort] & hook "LIST.size"
 
+makeListSymbol :: Internal.Symbol
+makeListSymbol =
+    builtinSymbol "makeList" listSort [intSort, intSort] & hook "LIST.make"
+
 updateListSymbol :: Internal.Symbol
 updateListSymbol = builtinSymbol "updateList" listSort
     [listSort, intSort, intSort] & hook "LIST.update"
@@ -411,6 +415,9 @@ getList list poz = mkApplySymbol getListSymbol [list, poz]
 sizeList :: TermLike VariableName -> TermLike VariableName
 sizeList l = mkApplySymbol sizeListSymbol [l]
 
+makeList :: TermLike VariableName -> TermLike VariableName -> TermLike VariableName
+makeList len x = mkApplySymbol makeListSymbol [len, x]
+
 updateList
     :: TermLike VariableName
     -> TermLike VariableName
@@ -1530,6 +1537,7 @@ listModule =
             , hookedSymbolDecl updateListSymbol
             , hookedSymbolDecl inListSymbol
             , hookedSymbolDecl sizeListSymbol
+            , hookedSymbolDecl makeListSymbol
             , hookedSymbolDecl updateAllListSymbol
             -- A second builtin List sort, to confuse 'asPattern'.
             , listSortDecl2

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

@@ -13,6 +13,7 @@ module Test.Kore.Builtin.List
     , test_inUnit
     , test_inElement
     , test_inConcat
+    , test_make
     , test_updateAll
     , hprop_unparse
     , test_size
@@ -418,6 +419,20 @@ test_size =
         (===) Pattern.top    =<< evaluateT predicate
     ]
 
+test_make :: [TestTree]
+test_make =
+    [ testCaseWithoutSMT "make(-1, 5) === \\bottom" $ do
+        result <- evaluate $ makeList (mkInt (-1)) (mkInt 5)
+        assertEqual' "" Pattern.bottom result
+    , testCaseWithoutSMT "make(0, 5) === []" $ do
+        result <- evaluate $ makeList (mkInt 0) (mkInt 5)
+        assertEqual' "" (Pattern.fromTermLike (asInternal [])) result
+    , testCaseWithoutSMT "make(3, 5) === [5, 5, 5]" $ do
+        result <- evaluate $ makeList (mkInt 3) (mkInt 5)
+        let expect = asInternal . fmap mkInt $ Seq.fromList [5, 5, 5]
+        assertEqual' "" (Pattern.fromTermLike expect) result
+    ]
+
 test_updateAll :: [TestTree]
 test_updateAll =
     [ testCaseWithoutSMT "updateAll([1, 2, 3], -1, [5]) === \\bottom" $ do