Skip to content

Commit 79f23bf

Browse files
jbertholdgithub-actions
jberthold
and
github-actions
authored
LIST.listRange in legacy kore, more list hooks and list matching in booster (#4108)
* `LIST.listRange` was previously not implemented in legacy kore (and therefore caused crashes). * More hooks from the `LIST` family have been implemented in booster - `LIST.update` is particularly interesting because it speeds up execution of proofs in `mir-semantics`. - other hooks were implemented to get parity between booster and legacy kore: `conca`, `in`, `make`, as well as `element` and `unit`, but the latter are mostly handled by custom list internalisation code. * List matching is improved to enable simplifications of expressions involving lists constructors. --------- Co-authored-by: github-actions <[email protected]>
1 parent 48c2b80 commit 79f23bf

File tree

9 files changed

+544
-88
lines changed

9 files changed

+544
-88
lines changed

‎booster/library/Booster/Builtin/LIST.hs

Lines changed: 112 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,7 @@ import Data.ByteString.Char8 (ByteString, pack)
1717
import Data.Map (Map)
1818
import Data.Map qualified as Map
1919

20+
import Booster.Builtin.BOOL (boolTerm)
2021
import Booster.Builtin.Base
2122
import Booster.Builtin.INT
2223
import Booster.Definition.Attributes.Base (
@@ -29,10 +30,48 @@ builtinsLIST :: Map ByteString BuiltinFunction
2930
builtinsLIST =
3031
Map.mapKeys ("LIST." <>) $
3132
Map.fromList
32-
[ "get" ~~> listGetHook
33+
[ "concat" ~~> listConcatHook
34+
, "element" ~~> listElementHook
35+
, "get" ~~> listGetHook
36+
, "in" ~~> listInHook
37+
, "make" ~~> listMakeHook
38+
, "range" ~~> listRangeHook
3339
, "size" ~~> listSizeHook
40+
, "unit" ~~> listUnitHook
41+
, "update" ~~> listUpdateHook
3442
]
3543

44+
-- | concatenate two lists
45+
listConcatHook :: BuiltinFunction
46+
listConcatHook [KList def1 heads1 rest1, KList def2 heads2 rest2]
47+
-- see Booster.Pattern.Base.internaliseKList
48+
| def1 /= def2 =
49+
pure Nothing -- actually a compiler error
50+
| Nothing <- rest1
51+
, Nothing <- rest2 =
52+
pure $ Just $ KList def1 (heads1 <> heads2) Nothing
53+
| Nothing <- rest1 =
54+
pure $ Just $ KList def2 (heads1 <> heads2) rest2
55+
| Nothing <- rest2
56+
, Just (mid1, tails1) <- rest1 =
57+
pure $ Just $ KList def1 heads1 $ Just (mid1, tails1 <> heads2)
58+
| otherwise -- opaque middle in both lists, unable to simplify
59+
=
60+
pure Nothing
61+
listConcatHook [KList def1 heads Nothing, other] =
62+
pure $ Just $ KList def1 heads (Just (other, []))
63+
listConcatHook [other, KList def2 heads Nothing] =
64+
pure $ Just $ KList def2 [] (Just (other, heads))
65+
listConcatHook other =
66+
arityError "LIST.concat" 2 other
67+
68+
-- | create a singleton list from a given element
69+
listElementHook :: BuiltinFunction
70+
listElementHook [elem'] =
71+
pure $ Just $ KList kItemListDef [elem'] Nothing
72+
listElementHook other =
73+
arityError "LIST.element" 1 other
74+
3675
listGetHook :: BuiltinFunction
3776
listGetHook [KList _ heads mbRest, intArg] =
3877
let headLen = length heads
@@ -67,6 +106,55 @@ listGetHook [_other, _] =
67106
listGetHook args =
68107
arityError "LIST.get" 2 args
69108

109+
listInHook :: BuiltinFunction
110+
listInHook [e, KList _ heads rest] =
111+
case rest of
112+
Nothing -> pure $ Just $ boolTerm (e `elem` heads)
113+
Just (_mid, tails)
114+
| e `elem` tails ->
115+
pure $ Just $ boolTerm True
116+
| otherwise -> -- could be in opaque _mid
117+
pure Nothing
118+
listInHook args =
119+
arityError "LIST.in" 2 args
120+
121+
listMakeHook :: BuiltinFunction
122+
listMakeHook [intArg, value] =
123+
case fromIntegral <$> readIntTerm intArg of
124+
Nothing ->
125+
intArg `shouldHaveSort` "SortInt" >> pure Nothing
126+
Just len ->
127+
pure $ Just $ KList kItemListDef (replicate len value) Nothing
128+
listMakeHook args =
129+
arityError "LIST.make" 2 args
130+
131+
listRangeHook :: BuiltinFunction
132+
listRangeHook [KList def heads rest, fromFront, fromBack] =
133+
case (fromIntegral <$> readIntTerm fromFront, fromIntegral <$> readIntTerm fromBack) of
134+
(Nothing, _) ->
135+
fromFront `shouldHaveSort` "SortInt" >> pure Nothing
136+
(_, Nothing) ->
137+
fromBack `shouldHaveSort` "SortInt" >> pure Nothing
138+
(Just frontDrop, Just backDrop)
139+
| frontDrop < 0 -> pure Nothing -- bottom
140+
| backDrop < 0 -> pure Nothing -- bottom
141+
| Nothing <- rest -> do
142+
let targetLen = length heads - frontDrop - backDrop
143+
if targetLen < 0
144+
then pure Nothing -- bottom
145+
else do
146+
let part = take targetLen $ drop frontDrop heads
147+
pure $ Just $ KList def part Nothing
148+
| Just (mid, tails) <- rest ->
149+
if length tails < backDrop
150+
then pure Nothing -- opaque middle, cannot drop from back
151+
else do
152+
let heads' = drop frontDrop heads
153+
tails' = reverse $ drop backDrop $ reverse tails
154+
pure $ Just $ KList def heads' $ Just (mid, tails')
155+
listRangeHook args =
156+
arityError "LIST.range" 3 args
157+
70158
listSizeHook :: BuiltinFunction
71159
listSizeHook = \case
72160
[KList _ heads Nothing] ->
@@ -78,6 +166,29 @@ listSizeHook = \case
78166
moreArgs ->
79167
arityError "LIST.size" 1 moreArgs
80168

169+
listUnitHook :: BuiltinFunction
170+
listUnitHook [] = pure $ Just $ KList kItemListDef [] Nothing
171+
listUnitHook args =
172+
arityError "LIST.unit" 0 args
173+
174+
listUpdateHook :: BuiltinFunction
175+
listUpdateHook [KList def heads rest, intArg, value] =
176+
case fromIntegral <$> readIntTerm intArg of
177+
Nothing ->
178+
intArg `shouldHaveSort` "SortInt" >> pure Nothing
179+
Just idx
180+
| idx < 0 ->
181+
pure Nothing -- bottom
182+
| otherwise ->
183+
case splitAt idx heads of
184+
(front, _target : back) ->
185+
pure $ Just $ KList def (front <> (value : back)) rest
186+
(_heads, []) ->
187+
-- idx >= length heads, indeterminate
188+
pure Nothing
189+
listUpdateHook args =
190+
arityError "LIST.update" 3 args
191+
81192
kItemListDef :: KListDefinition
82193
kItemListDef =
83194
KListDefinition

‎booster/library/Booster/Pattern/ApplyEquations.hs

Lines changed: 54 additions & 22 deletions
Original file line numberDiff line numberDiff line change
@@ -585,28 +585,60 @@ traverseTerm direction onRecurse onEval trm = do
585585
else
586586
SymbolApplication sym sorts
587587
<$> mapM onRecurse args
588-
-- maps, lists, and sets, are not currently evaluated because
589-
-- the matcher does not provide matches on collections.
590-
KMap def keyVals rest ->
591-
KMap def
592-
<$> mapM (\(k, v) -> (,) <$> onRecurse k <*> onRecurse v) keyVals
593-
<*> maybe (pure Nothing) ((Just <$>) . onRecurse) rest
594-
KList def heads rest ->
595-
KList def
596-
<$> mapM onRecurse heads
597-
<*> maybe
598-
(pure Nothing)
599-
( (Just <$>)
600-
. \(mid, tails) ->
601-
(,)
602-
<$> onRecurse mid
603-
<*> mapM onRecurse tails
604-
)
605-
rest
606-
KSet def keyVals rest ->
607-
KSet def
608-
<$> mapM onRecurse keyVals
609-
<*> maybe (pure Nothing) ((Just <$>) . onRecurse) rest
588+
kmap@(KMap def keyVals rest) -> do
589+
let handlePairs = mapM (\(k, v) -> (,) <$> onRecurse k <*> onRecurse v)
590+
if direction == BottomUp
591+
then do
592+
-- evaluate arguments first
593+
keyVals' <- handlePairs keyVals
594+
rest' <- traverse onRecurse rest
595+
-- then try to apply equations
596+
onEval $ KMap def keyVals' rest'
597+
else {- direction == TopDown -} do
598+
-- try to apply equations
599+
kmap' <- onEval kmap
600+
case kmap' of
601+
-- the result should be another internal KMap
602+
KMap _ keyVals' rest' ->
603+
KMap def
604+
<$> handlePairs keyVals'
605+
<*> traverse onRecurse rest'
606+
other ->
607+
-- unlikely to occur, but won't loop
608+
onRecurse other
609+
klist@(KList def heads rest) -> do
610+
let handleRest =
611+
traverse $ \(mid, tails) -> (,) <$> onRecurse mid <*> mapM onRecurse tails
612+
if direction == BottomUp
613+
then do
614+
heads' <- mapM onRecurse heads
615+
rest' <- handleRest rest
616+
onEval (KList def heads' rest')
617+
else {- direction == TopDown -} do
618+
klist' <- onEval klist
619+
case klist' of
620+
-- the result should be another internal KList
621+
KList _ heads' rest' ->
622+
KList def
623+
<$> mapM onRecurse heads'
624+
<*> handleRest rest'
625+
other ->
626+
onRecurse other
627+
kset@(KSet def elems rest)
628+
| direction == BottomUp -> do
629+
elems' <- mapM onRecurse elems
630+
rest' <- traverse onRecurse rest
631+
onEval $ KSet def elems' rest'
632+
| otherwise {- direction == TopDown -} -> do
633+
kset' <- onEval kset
634+
case kset' of
635+
-- the result should be another internal KSet
636+
KSet _ elems' rest' ->
637+
KSet def
638+
<$> mapM onRecurse elems'
639+
<*> traverse onRecurse rest'
640+
other ->
641+
onRecurse other
610642

611643
cached :: LoggerMIO io => CacheTag -> (Term -> EquationT io Term) -> Term -> EquationT io Term
612644
cached cacheTag cb t@(Term attributes _)

‎booster/library/Booster/Pattern/Match.hs

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -246,7 +246,6 @@ match1 _ t1@KList{} t2@DomainValue{}
246246
match1 Eval t1@KList{} t2@Injection{} = addIndeterminate t1 t2
247247
match1 _ t1@KList{} t2@Injection{} = failWith $ DifferentSymbols t1 t2
248248
match1 _ t1@KList{} t2@KMap{} = failWith $ DifferentSymbols t1 t2
249-
match1 Eval t1@KList{} t2@KList{} = addIndeterminate t1 t2
250249
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
251250
match1 _ t1@KList{} t2@KSet{} = failWith $ DifferentSymbols t1 t2
252251
match1 _ t1@KList{} t2@ConsApplication{} = failWith $ DifferentSymbols t1 t2

0 commit comments

Comments
 (0)