LIST.listRange in legacy kore, more list hooks and list matching in booster

booster/library/Booster/Builtin/LIST.hs

@@ -17,6 +17,7 @@ import Data.ByteString.Char8 (ByteString, pack)
 import Data.Map (Map)
 import Data.Map qualified as Map
 
+import Booster.Builtin.BOOL (boolTerm)
 import Booster.Builtin.Base
 import Booster.Builtin.INT
 import Booster.Definition.Attributes.Base (
@@ -29,10 +30,48 @@ builtinsLIST :: Map ByteString BuiltinFunction
 builtinsLIST =
     Map.mapKeys ("LIST." <>) $
         Map.fromList
-            [ "get" ~~> listGetHook
+            [ "concat" ~~> listConcatHook
+            , "element" ~~> listElementHook
+            , "get" ~~> listGetHook
+            , "in" ~~> listInHook
+            , "make" ~~> listMakeHook
+            , "range" ~~> listRangeHook
             , "size" ~~> listSizeHook
+            , "unit" ~~> listUnitHook
+            , "update" ~~> listUpdateHook
             ]
 
+-- | concatenate two lists
+listConcatHook :: BuiltinFunction
+listConcatHook [KList def1 heads1 rest1, KList def2 heads2 rest2]
+    -- see Booster.Pattern.Base.internaliseKList
+    | def1 /= def2 =
+        pure Nothing -- actually a compiler error
+    | Nothing <- rest1
+    , Nothing <- rest2 =
+        pure $ Just $ KList def1 (heads1 <> heads2) Nothing
+    | Nothing <- rest1 =
+        pure $ Just $ KList def2 (heads1 <> heads2) rest2
+    | Nothing <- rest2
+    , Just (mid1, tails1) <- rest1 =
+        pure $ Just $ KList def1 heads1 $ Just (mid1, tails1 <> heads2)
+    | otherwise -- opaque middle in both lists, unable to simplify
+        =
+        pure Nothing
+listConcatHook [KList def1 heads Nothing, other] =
+    pure $ Just $ KList def1 heads (Just (other, []))
+listConcatHook [other, KList def2 heads Nothing] =
+    pure $ Just $ KList def2 [] (Just (other, heads))
+listConcatHook other =
+    arityError "LIST.concat" 2 other
+
+-- | create a singleton list from a given element
+listElementHook :: BuiltinFunction
+listElementHook [elem'] =
+    pure $ Just $ KList kItemListDef [elem'] Nothing
+listElementHook other =
+    arityError "LIST.element" 1 other
+
 listGetHook :: BuiltinFunction
 listGetHook [KList _ heads mbRest, intArg] =
     let headLen = length heads
@@ -67,6 +106,55 @@ listGetHook [_other, _] =
 listGetHook args =
     arityError "LIST.get" 2 args
 
+listInHook :: BuiltinFunction
+listInHook [e, KList _ heads rest] =
+    case rest of
+        Nothing -> pure $ Just $ boolTerm (e `elem` heads)
+        Just (_mid, tails)
+            | e `elem` tails ->
+                pure $ Just $ boolTerm True
+            | otherwise -> -- could be in opaque _mid
+                pure Nothing
+listInHook args =
+    arityError "LIST.in" 2 args
+
+listMakeHook :: BuiltinFunction
+listMakeHook [intArg, value] =
+    case fromIntegral <$> readIntTerm intArg of
+        Nothing ->
+            intArg `shouldHaveSort` "SortInt" >> pure Nothing
+        Just len ->
+            pure $ Just $ KList kItemListDef (replicate len value) Nothing
+listMakeHook args =
+    arityError "LIST.make" 2 args
+
+listRangeHook :: BuiltinFunction
+listRangeHook [KList def heads rest, fromFront, fromBack] =
+    case (fromIntegral <$> readIntTerm fromFront, fromIntegral <$> readIntTerm fromBack) of
+        (Nothing, _) ->
+            fromFront `shouldHaveSort` "SortInt" >> pure Nothing
+        (_, Nothing) ->
+            fromBack `shouldHaveSort` "SortInt" >> pure Nothing
+        (Just frontDrop, Just backDrop)
+            | frontDrop < 0 -> pure Nothing -- bottom
+            | backDrop < 0 -> pure Nothing -- bottom
+            | Nothing <- rest -> do
+                let targetLen = length heads - frontDrop - backDrop
+                if targetLen < 0
+                    then pure Nothing -- bottom
+                    else do
+                        let part = take targetLen $ drop frontDrop heads
+                        pure $ Just $ KList def part Nothing
+            | Just (mid, tails) <- rest ->
+                if length tails < backDrop
+                    then pure Nothing -- opaque middle, cannot drop from back
+                    else do
+                        let heads' = drop frontDrop heads
+                            tails' = reverse $ drop backDrop $ reverse tails
+                        pure $ Just $ KList def heads' $ Just (mid, tails')
+listRangeHook args =
+    arityError "LIST.range" 3 args
+
 listSizeHook :: BuiltinFunction
 listSizeHook = \case
     [KList _ heads Nothing] ->
@@ -78,6 +166,29 @@ listSizeHook = \case
     moreArgs ->
         arityError "LIST.size" 1 moreArgs
 
+listUnitHook :: BuiltinFunction
+listUnitHook [] = pure $ Just $ KList kItemListDef [] Nothing
+listUnitHook args =
+    arityError "LIST.unit" 0 args
+
+listUpdateHook :: BuiltinFunction
+listUpdateHook [KList def heads rest, intArg, value] =
+    case fromIntegral <$> readIntTerm intArg of
+        Nothing ->
+            intArg `shouldHaveSort` "SortInt" >> pure Nothing
+        Just idx
+            | idx < 0 ->
+                pure Nothing -- bottom
+            | otherwise ->
+                case splitAt idx heads of
+                    (front, _target : back) ->
+                        pure $ Just $ KList def (front <> (value : back)) rest
+                    (_heads, []) ->
+                        -- idx >= length heads, indeterminate
+                        pure Nothing
+listUpdateHook args =
+    arityError "LIST.update" 3 args
+
 kItemListDef :: KListDefinition
 kItemListDef =
     KListDefinition

booster/library/Booster/Pattern/ApplyEquations.hs

@@ -585,28 +585,60 @@ traverseTerm direction onRecurse onEval trm = do
                     else
                         SymbolApplication sym sorts
                             <$> mapM onRecurse args
-        -- maps, lists, and sets, are not currently evaluated because
-        -- the matcher does not provide matches on collections.
-        KMap def keyVals rest ->
-            KMap def
-                <$> mapM (\(k, v) -> (,) <$> onRecurse k <*> onRecurse v) keyVals
-                <*> maybe (pure Nothing) ((Just <$>) . onRecurse) rest
-        KList def heads rest ->
-            KList def
-                <$> mapM onRecurse heads
-                <*> maybe
-                    (pure Nothing)
-                    ( (Just <$>)
-                        . \(mid, tails) ->
-                            (,)
-                                <$> onRecurse mid
-                                <*> mapM onRecurse tails
-                    )
-                    rest
-        KSet def keyVals rest ->
-            KSet def
-                <$> mapM onRecurse keyVals
-                <*> maybe (pure Nothing) ((Just <$>) . onRecurse) rest
+        kmap@(KMap def keyVals rest) -> do
+            let handlePairs = mapM (\(k, v) -> (,) <$> onRecurse k <*> onRecurse v)
+            if direction == BottomUp
+                then do
+                    -- evaluate arguments first
+                    keyVals' <- handlePairs keyVals
+                    rest' <- traverse onRecurse rest
+                    -- then try to apply equations
+                    onEval $ KMap def keyVals' rest'
+                else {- direction == TopDown -} do
+                    -- try to apply equations
+                    kmap' <- onEval kmap
+                    case kmap' of
+                        -- the result should be another internal KMap
+                        KMap _ keyVals' rest' ->
+                            KMap def
+                                <$> handlePairs keyVals'
+                                <*> traverse onRecurse rest'
+                        other ->
+                            -- unlikely to occur, but won't loop
+                            onRecurse other
+        klist@(KList def heads rest) -> do
+            let handleRest =
+                    traverse $ \(mid, tails) -> (,) <$> onRecurse mid <*> mapM onRecurse tails
+            if direction == BottomUp
+                then do
+                    heads' <- mapM onRecurse heads
+                    rest' <- handleRest rest
+                    onEval (KList def heads' rest')
+                else {- direction == TopDown -} do
+                    klist' <- onEval klist
+                    case klist' of
+                        -- the result should be another internal KList
+                        KList _ heads' rest' ->
+                            KList def
+                                <$> mapM onRecurse heads'
+                                <*> handleRest rest'
+                        other ->
+                            onRecurse other
+        kset@(KSet def elems rest)
+            | direction == BottomUp -> do
+                elems' <- mapM onRecurse elems
+                rest' <- traverse onRecurse rest
+                onEval $ KSet def elems' rest'
+            | otherwise {- direction == TopDown -} -> do
+                kset' <- onEval kset
+                case kset' of
+                    -- the result should be another internal KSet
+                    KSet _ elems' rest' ->
+                        KSet def
+                            <$> mapM onRecurse elems'
+                            <*> traverse onRecurse rest'
+                    other ->
+                        onRecurse other
 
 cached :: LoggerMIO io => CacheTag -> (Term -> EquationT io Term) -> Term -> EquationT io Term
 cached cacheTag cb t@(Term attributes _)

booster/library/Booster/Pattern/Match.hs

@@ -246,7 +246,6 @@ match1 _       t1@KList{}                                 t2@DomainValue{}
 match1 Eval    t1@KList{}                                 t2@Injection{}                             = addIndeterminate t1 t2
 match1 _       t1@KList{}                                 t2@Injection{}                             = failWith $ DifferentSymbols t1 t2
 match1 _       t1@KList{}                                 t2@KMap{}                                  = failWith $ DifferentSymbols t1 t2
-match1 Eval    t1@KList{}                                 t2@KList{}                                 = addIndeterminate t1 t2
 match1 _       t1@(KList def1 heads1 rest1)               t2@(KList def2 heads2 rest2)               = if def1 == def2 then matchLists def1 heads1 rest1 heads2 rest2 else failWith $ DifferentSorts t1 t2
 match1 _       t1@KList{}                                 t2@KSet{}                                  = failWith $ DifferentSymbols t1 t2
 match1 _       t1@KList{}                                 t2@ConsApplication{}                       = failWith $ DifferentSymbols t1 t2