Skip to content

Commit a0907df

Browse files
jbertholdjberthold
authored
3813 add selected hooks for INT, BOOL, MAP, LIST (#3828)
Context: #3813 Adds a number of hooks (as per documentation in https://github.com/runtimeverification/haskell-backend/blob/master/docs/hooks.md) and splits the `Booster.Builtin` module into several parts. * `Bool` : all hooked operations implemented * `Int`: selected binary and unary operations and comparisons * `List`: `get` (indexing) and `size` * `Map`: all hooked operations except `removeAll` and `keys` (which would require using internal sets)
1 parent 5db6dfc commit a0907df

File tree

14 files changed

+1445
-365
lines changed

14 files changed

+1445
-365
lines changed

‎booster/library/Booster/Builtin.hs

Lines changed: 17 additions & 175 deletions
Original file line numberDiff line numberDiff line change
@@ -2,195 +2,37 @@
22
Copyright : (c) Runtime Verification, 2023
33
License : BSD-3-Clause
44
5-
Builtin functions. Only a select few functions are implemented.
5+
Builtin functions as described in [docs/hooks.md](https://github.com/runtimeverification/haskell-backend/blob/master/docs/hooks.md).
6+
Only selected functions are implemented.
67
78
Built-in functions are looked up by their symbol attribute 'hook' from
89
the definition's symbol map.
10+
11+
The built-in function fails outright when its function is called with
12+
a wrong argument count. When required arguments are unevaluated, the
13+
hook returns 'Nothing'.
914
-}
1015
module Booster.Builtin (
1116
hooks,
1217
) where
1318

14-
import Control.Monad
15-
import Control.Monad.Trans.Except
16-
import Data.ByteString.Char8 (ByteString)
17-
import Data.List (partition)
19+
import Data.ByteString (ByteString)
1820
import Data.Map (Map)
1921
import Data.Map qualified as Map
20-
import Data.Text (Text)
21-
import Prettyprinter (pretty, vsep)
22-
23-
import Booster.Pattern.Base
24-
import Booster.Pattern.Bool
25-
import Booster.Pattern.Util
26-
import Booster.Prettyprinter
2722

28-
-- built-in functions may fail on arity or sort errors, and may be
29-
-- partial (returning a Maybe type)
30-
type BuiltinFunction = [Term] -> Except Text (Maybe Term)
23+
import Booster.Builtin.BOOL
24+
import Booster.Builtin.Base
25+
import Booster.Builtin.INT
26+
import Booster.Builtin.KEQUAL
27+
import Booster.Builtin.LIST
28+
import Booster.Builtin.MAP
3129

3230
hooks :: Map ByteString BuiltinFunction
3331
hooks =
3432
Map.unions
35-
[ builtinsKEQUAL
33+
[ builtinsBOOL
34+
, builtinsINT
3635
, builtinsMAP
36+
, builtinsLIST
37+
, builtinsKEQUAL
3738
]
38-
39-
------------------------------------------------------------
40-
(~~>) :: ByteString -> BuiltinFunction -> (ByteString, BuiltinFunction)
41-
(~~>) = (,)
42-
43-
------------------------------------------------------------
44-
-- MAP hooks
45-
-- only lookups and in_keys are implemented
46-
builtinsMAP :: Map ByteString BuiltinFunction
47-
builtinsMAP =
48-
Map.mapKeys ("MAP." <>) $
49-
Map.fromList
50-
[ "lookup" ~~> mapLookupHook
51-
, "lookupOrDefault" ~~> mapLookupOrDefaultHook
52-
, "in_keys" ~~> mapInKeysHook
53-
]
54-
55-
mapLookupHook :: BuiltinFunction
56-
mapLookupHook args
57-
| [KMap _ pairs _mbRest, key] <- args =
58-
-- if the key is not found, return Nothing (no result),
59-
-- regardless of whether the key _could_ still be there.
60-
pure $ lookup key pairs
61-
| [_other, _] <- args =
62-
-- other `shouldHaveSort` "SortMap"
63-
pure Nothing -- not an internalised map, maybe a function call
64-
| otherwise =
65-
-- FIXME write a helper function for arity check
66-
throwE . renderText $ "MAP.lookup: wrong arity " <> pretty (length args)
67-
68-
mapLookupOrDefaultHook :: BuiltinFunction
69-
mapLookupOrDefaultHook args
70-
| [KMap _ pairs mbRest, key, defaultValue] <- args = do
71-
case lookup key pairs of
72-
Just value ->
73-
-- key was found, simply return
74-
pure $ Just value
75-
Nothing -- key could be in unevaluated or opaque part
76-
| Just _ <- mbRest ->
77-
pure Nothing -- have opaque part, no result
78-
| any ((\(Term a _) -> not a.isConstructorLike) . fst) pairs ->
79-
pure Nothing -- have unevaluated keys, no result
80-
| otherwise -> -- certain that the key is not in the map
81-
pure $ Just defaultValue
82-
| [_other, _, _] <- args =
83-
-- other `shouldHaveSort` "SortMap"
84-
pure Nothing -- not an internalised map, maybe a function call
85-
| otherwise =
86-
throwE . renderText $ "MAP.lookupOrDefault: wrong arity " <> pretty (length args)
87-
88-
mapInKeysHook :: BuiltinFunction
89-
mapInKeysHook args
90-
| [key, KMap _ pairs mbRest] <- args = do
91-
-- only consider evaluated keys, return Nothing if any unevaluated ones are present
92-
let (eval'edKeys, uneval'edKeys) =
93-
partition (\(Term a _) -> a.isConstructorLike) (map fst pairs)
94-
case (key `elem` eval'edKeys, key `elem` uneval'edKeys) of
95-
(True, _) ->
96-
-- constructor-like (evaluated) key is present
97-
pure $ Just TrueBool
98-
(False, True) ->
99-
-- syntactically-equal unevaluated key is present
100-
pure $ Just TrueBool
101-
(False, False)
102-
| Nothing <- mbRest -- no opaque rest
103-
, null uneval'edKeys -> -- no keys unevaluated
104-
pure $ Just FalseBool
105-
| otherwise -> -- key could be present once evaluated
106-
pure Nothing
107-
| [_, _other] <- args = do
108-
-- other `shouldHaveSort` "SortMap"
109-
pure Nothing -- not an internalised map, maybe a function call
110-
| otherwise =
111-
throwE . renderText $ "MAP.in_keys: wrong arity " <> pretty (length args)
112-
113-
------------------------------------------------------------
114-
-- KEQUAL hooks
115-
builtinsKEQUAL :: Map ByteString BuiltinFunction
116-
builtinsKEQUAL =
117-
Map.fromList
118-
[ "KEQUAL.ite" ~~> iteHook
119-
, "KEQUAL.eq" ~~> equalsKHook
120-
, "KEQUAL.ne" ~~> nequalsKHook
121-
]
122-
123-
iteHook :: BuiltinFunction
124-
iteHook args
125-
| [cond, thenVal, elseVal] <- args = do
126-
cond `shouldHaveSort` "SortBool"
127-
unless (sortOfTerm thenVal == sortOfTerm elseVal) $
128-
throwE . renderText . vsep $
129-
[ "Different sorts in alternatives:"
130-
, pretty thenVal
131-
, pretty elseVal
132-
]
133-
case cond of
134-
TrueBool -> pure $ Just thenVal
135-
FalseBool -> pure $ Just elseVal
136-
_other -> pure Nothing
137-
| otherwise =
138-
throwE . renderText $ "KEQUAL.ite: wrong arity " <> pretty (length args)
139-
140-
equalsKHook :: BuiltinFunction
141-
equalsKHook args
142-
| [KSeq _ l, KSeq _ r] <- args = pure $ evalEqualsK l r
143-
| otherwise =
144-
throwE . renderText $ "KEQUAL.eq: wrong arity " <> pretty (length args)
145-
146-
nequalsKHook :: BuiltinFunction
147-
nequalsKHook args
148-
| [KSeq _ l, KSeq _ r] <- args = pure $ negateBool <$> evalEqualsK l r
149-
| otherwise =
150-
throwE . renderText $ "KEQUAL.ne: wrong arity " <> pretty (length args)
151-
152-
evalEqualsK :: Term -> Term -> Maybe Term
153-
evalEqualsK (SymbolApplication sL _ argsL) (SymbolApplication sR _ argsR)
154-
| isConstructorSymbol sL && isConstructorSymbol sR =
155-
if sL == sR
156-
then foldAndBool <$> zipWithM evalEqualsK argsL argsR
157-
else pure FalseBool
158-
evalEqualsK (SymbolApplication symbol _ _) DomainValue{}
159-
| isConstructorSymbol symbol = pure FalseBool
160-
evalEqualsK (SymbolApplication symbol _ _) Injection{}
161-
| isConstructorSymbol symbol = pure FalseBool
162-
evalEqualsK (SymbolApplication symbol _ _) KMap{}
163-
| isConstructorSymbol symbol = pure FalseBool
164-
evalEqualsK (SymbolApplication symbol _ _) KList{}
165-
| isConstructorSymbol symbol = pure FalseBool
166-
evalEqualsK (SymbolApplication symbol _ _) KSet{}
167-
| isConstructorSymbol symbol = pure FalseBool
168-
evalEqualsK DomainValue{} (SymbolApplication symbol _ _)
169-
| isConstructorSymbol symbol = pure FalseBool
170-
evalEqualsK Injection{} (SymbolApplication symbol _ _)
171-
| isConstructorSymbol symbol = pure FalseBool
172-
evalEqualsK KMap{} (SymbolApplication symbol _ _)
173-
| isConstructorSymbol symbol = pure FalseBool
174-
evalEqualsK KList{} (SymbolApplication symbol _ _)
175-
| isConstructorSymbol symbol = pure FalseBool
176-
evalEqualsK KSet{} (SymbolApplication symbol _ _)
177-
| isConstructorSymbol symbol = pure FalseBool
178-
evalEqualsK (Injection s1L s2L l) (Injection s1R s2R r)
179-
| s1L == s1R && s2L == s2R = evalEqualsK l r
180-
evalEqualsK l@DomainValue{} r@DomainValue{} =
181-
pure $ if l == r then TrueBool else FalseBool
182-
evalEqualsK l r =
183-
if l == r
184-
then pure TrueBool
185-
else fail "cannot evaluate" -- i.e., result is Nothing
186-
187-
-- check for simple (parameter-less) sorts
188-
shouldHaveSort :: Term -> SortName -> Except Text ()
189-
t `shouldHaveSort` s
190-
| sortOfTerm t == SortApp s [] =
191-
pure ()
192-
| otherwise =
193-
throwE . renderText . vsep $
194-
[ pretty $ "Argument term has unexpected sort (expected " <> show s <> "):"
195-
, pretty t
196-
]

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

Lines changed: 79 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,79 @@
1+
{- |
2+
Copyright : (c) Runtime Verification, 2023
3+
License : BSD-3-Clause
4+
5+
Built-in functions (hooks) in the BOOL namespace, as described in
6+
[docs/hooks.md](https://github.com/runtimeverification/haskell-backend/blob/master/docs/hooks.md).
7+
-}
8+
module Booster.Builtin.BOOL (
9+
builtinsBOOL,
10+
boolTerm,
11+
) where
12+
13+
import Data.ByteString.Char8 (ByteString)
14+
import Data.Map (Map)
15+
import Data.Map qualified as Map
16+
17+
import Booster.Builtin.Base
18+
import Booster.Pattern.Base
19+
import Booster.Pattern.Bool
20+
21+
builtinsBOOL :: Map ByteString BuiltinFunction
22+
builtinsBOOL =
23+
Map.mapKeys ("BOOL." <>) $
24+
Map.fromList
25+
[ "or" ~~> orHook
26+
, "and" ~~> andHook
27+
, "xor" ~~> boolOperator (/=)
28+
, "eq" ~~> boolOperator (==)
29+
, "ne" ~~> boolOperator (/=)
30+
, "not" ~~> notHook
31+
, "implies" ~~> impliesHook
32+
]
33+
34+
-- shortcut evaluations for or and and
35+
orHook :: BuiltinFunction
36+
orHook args
37+
| length args /= 2 = arityError "BOOL.or" 2 args
38+
| [TrueBool, _] <- args = pure $ Just TrueBool
39+
| [_, TrueBool] <- args = pure $ Just TrueBool
40+
| [FalseBool, FalseBool] <- args = pure $ Just FalseBool
41+
| otherwise = pure Nothing -- arguments not determined
42+
43+
andHook :: BuiltinFunction
44+
andHook args
45+
| length args /= 2 = arityError "BOOL.and" 2 args
46+
| [FalseBool, _] <- args = pure $ Just FalseBool
47+
| [_, FalseBool] <- args = pure $ Just FalseBool
48+
| [TrueBool, TrueBool] <- args = pure $ Just TrueBool
49+
| otherwise = pure Nothing -- arguments not determined
50+
51+
notHook :: BuiltinFunction
52+
notHook [arg]
53+
| Just b <- readBoolTerm arg = pure . Just . boolTerm $ not b
54+
| otherwise = pure Nothing
55+
notHook args = arityError "BOOL.not" 1 args
56+
57+
impliesHook :: BuiltinFunction
58+
impliesHook args
59+
| length args /= 2 = arityError "BOOL.implies" 2 args
60+
| [FalseBool, _] <- args = pure $ Just TrueBool
61+
| [TrueBool, FalseBool] <- args = pure $ Just FalseBool
62+
| [TrueBool, TrueBool] <- args = pure $ Just TrueBool
63+
| otherwise = pure Nothing -- arguments not determined
64+
65+
boolOperator :: (Bool -> Bool -> Bool) -> BuiltinFunction
66+
boolOperator f args
67+
| length args /= 2 = arityError "BOOL.<operator>" 2 args
68+
| [Just arg1, Just arg2] <- map readBoolTerm args =
69+
pure . Just . boolTerm $ f arg1 arg2
70+
| otherwise = pure Nothing -- arguments not determined
71+
72+
boolTerm :: Bool -> Term
73+
boolTerm True = TrueBool
74+
boolTerm False = FalseBool
75+
76+
readBoolTerm :: Term -> Maybe Bool
77+
readBoolTerm TrueBool = Just True
78+
readBoolTerm FalseBool = Just False
79+
readBoolTerm _other = Nothing

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

Lines changed: 72 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,72 @@
1+
{- |
2+
Copyright : (c) Runtime Verification, 2023
3+
License : BSD-3-Clause
4+
5+
Base type definitions and helpers for built-in functions (hooks).
6+
-}
7+
module Booster.Builtin.Base (
8+
BuiltinFunction,
9+
-- helpers
10+
(~~>),
11+
arityError,
12+
isConstructorLike_,
13+
shouldHaveSort,
14+
) where
15+
16+
import Control.Monad.Trans.Except
17+
import Data.ByteString.Char8 (ByteString)
18+
import Data.Text (Text)
19+
import Data.Text qualified as Text
20+
import Data.Text.Encoding qualified as Text
21+
import Prettyprinter (pretty)
22+
23+
import Booster.Pattern.Base
24+
import Booster.Pattern.Util
25+
import Booster.Prettyprinter
26+
27+
{- |
28+
29+
Built-in functions may fail on arity or sort errors, and may be
30+
partial (returning a Maybe type)
31+
32+
The built-in function fails outright when its function is called with
33+
a wrong argument count. When required arguments are unevaluated, the
34+
hook returns 'Nothing'.
35+
-}
36+
type BuiltinFunction = [Term] -> Except Text (Maybe Term)
37+
38+
------------------------------------------------------------
39+
-- Helpers
40+
41+
(~~>) :: ByteString -> BuiltinFunction -> (ByteString, BuiltinFunction)
42+
(~~>) = (,)
43+
44+
isConstructorLike_ :: Term -> Bool
45+
isConstructorLike_ = (.isConstructorLike) . getAttributes
46+
47+
{- | checks that the arguments list has the expected length.
48+
49+
Returns nothing if the arg.count matches, so it can be used as a
50+
fall-through case in hook function definitions.
51+
-}
52+
arityError :: Text -> Int -> [Term] -> Except Text (Maybe Term)
53+
arityError fname argCount args
54+
| l == argCount =
55+
pure Nothing
56+
| otherwise =
57+
throwE $ fname <> Text.pack msg
58+
where
59+
l = length args
60+
msg = unwords [": wrong arity. Expected ", show argCount, ", got ", show l]
61+
62+
-- check for simple (parameter-less) sorts
63+
shouldHaveSort :: Term -> SortName -> Except Text ()
64+
t `shouldHaveSort` s
65+
| sortOfTerm t == SortApp s [] =
66+
pure ()
67+
| otherwise =
68+
throwE $
69+
Text.unlines
70+
[ "Argument term has unexpected sort (expected " <> Text.decodeLatin1 s <> "):"
71+
, renderText (pretty t)
72+
]

0 commit comments

Comments
 (0)