3813 add selected hooks for INT, BOOL, MAP, LIST

booster/library/Booster/Builtin.hs

@@ -2,195 +2,37 @@
 Copyright   : (c) Runtime Verification, 2023
 License     : BSD-3-Clause
 
-Builtin functions. Only a select few functions are implemented.
+Builtin functions as described in [docs/hooks.md](https://github.com/runtimeverification/haskell-backend/blob/master/docs/hooks.md).
+Only selected functions are implemented.
 
 Built-in functions are looked up by their symbol attribute 'hook' from
 the definition's symbol map.
+
+The built-in function fails outright when its function is called with
+a wrong argument count. When required arguments are unevaluated, the
+hook returns 'Nothing'.
 -}
 module Booster.Builtin (
     hooks,
 ) where
 
-import Control.Monad
-import Control.Monad.Trans.Except
-import Data.ByteString.Char8 (ByteString)
-import Data.List (partition)
+import Data.ByteString (ByteString)
 import Data.Map (Map)
 import Data.Map qualified as Map
-import Data.Text (Text)
-import Prettyprinter (pretty, vsep)
-
-import Booster.Pattern.Base
-import Booster.Pattern.Bool
-import Booster.Pattern.Util
-import Booster.Prettyprinter
 
--- built-in functions may fail on arity or sort errors, and may be
--- partial (returning a Maybe type)
-type BuiltinFunction = [Term] -> Except Text (Maybe Term)
+import Booster.Builtin.BOOL
+import Booster.Builtin.Base
+import Booster.Builtin.INT
+import Booster.Builtin.KEQUAL
+import Booster.Builtin.LIST
+import Booster.Builtin.MAP
 
 hooks :: Map ByteString BuiltinFunction
 hooks =
     Map.unions
-        [ builtinsKEQUAL
+        [ builtinsBOOL
+        , builtinsINT
         , builtinsMAP
+        , builtinsLIST
+        , builtinsKEQUAL
         ]
-
-------------------------------------------------------------
-(~~>) :: ByteString -> BuiltinFunction -> (ByteString, BuiltinFunction)
-(~~>) = (,)
-
-------------------------------------------------------------
--- MAP hooks
--- only lookups and in_keys are implemented
-builtinsMAP :: Map ByteString BuiltinFunction
-builtinsMAP =
-    Map.mapKeys ("MAP." <>) $
-        Map.fromList
-            [ "lookup" ~~> mapLookupHook
-            , "lookupOrDefault" ~~> mapLookupOrDefaultHook
-            , "in_keys" ~~> mapInKeysHook
-            ]
-
-mapLookupHook :: BuiltinFunction
-mapLookupHook args
-    | [KMap _ pairs _mbRest, key] <- args =
-        -- if the key is not found, return Nothing (no result),
-        -- regardless of whether the key _could_ still be there.
-        pure $ lookup key pairs
-    | [_other, _] <- args =
-        -- other `shouldHaveSort` "SortMap"
-        pure Nothing -- not an internalised map, maybe a function call
-    | otherwise =
-        -- FIXME write a helper function for arity check
-        throwE . renderText $ "MAP.lookup: wrong arity " <> pretty (length args)
-
-mapLookupOrDefaultHook :: BuiltinFunction
-mapLookupOrDefaultHook args
-    | [KMap _ pairs mbRest, key, defaultValue] <- args = do
-        case lookup key pairs of
-            Just value ->
-                -- key was found, simply return
-                pure $ Just value
-            Nothing -- key could be in unevaluated or opaque part
-                | Just _ <- mbRest ->
-                    pure Nothing -- have opaque part, no result
-                | any ((\(Term a _) -> not a.isConstructorLike) . fst) pairs ->
-                    pure Nothing -- have unevaluated keys, no result
-                | otherwise -> -- certain that the key is not in the map
-                    pure $ Just defaultValue
-    | [_other, _, _] <- args =
-        -- other `shouldHaveSort` "SortMap"
-        pure Nothing -- not an internalised map, maybe a function call
-    | otherwise =
-        throwE . renderText $ "MAP.lookupOrDefault: wrong arity " <> pretty (length args)
-
-mapInKeysHook :: BuiltinFunction
-mapInKeysHook args
-    | [key, KMap _ pairs mbRest] <- args = do
-        -- only consider evaluated keys, return Nothing if any unevaluated ones are present
-        let (eval'edKeys, uneval'edKeys) =
-                partition (\(Term a _) -> a.isConstructorLike) (map fst pairs)
-        case (key `elem` eval'edKeys, key `elem` uneval'edKeys) of
-            (True, _) ->
-                -- constructor-like (evaluated) key is present
-                pure $ Just TrueBool
-            (False, True) ->
-                -- syntactically-equal unevaluated key is present
-                pure $ Just TrueBool
-            (False, False)
-                | Nothing <- mbRest -- no opaque rest
-                , null uneval'edKeys -> -- no keys unevaluated
-                    pure $ Just FalseBool
-                | otherwise -> -- key could be present once evaluated
-                    pure Nothing
-    | [_, _other] <- args = do
-        -- other `shouldHaveSort` "SortMap"
-        pure Nothing -- not an internalised map, maybe a function call
-    | otherwise =
-        throwE . renderText $ "MAP.in_keys: wrong arity " <> pretty (length args)
-
-------------------------------------------------------------
--- KEQUAL hooks
-builtinsKEQUAL :: Map ByteString BuiltinFunction
-builtinsKEQUAL =
-    Map.fromList
-        [ "KEQUAL.ite" ~~> iteHook
-        , "KEQUAL.eq" ~~> equalsKHook
-        , "KEQUAL.ne" ~~> nequalsKHook
-        ]
-
-iteHook :: BuiltinFunction
-iteHook args
-    | [cond, thenVal, elseVal] <- args = do
-        cond `shouldHaveSort` "SortBool"
-        unless (sortOfTerm thenVal == sortOfTerm elseVal) $
-            throwE . renderText . vsep $
-                [ "Different sorts in alternatives:"
-                , pretty thenVal
-                , pretty elseVal
-                ]
-        case cond of
-            TrueBool -> pure $ Just thenVal
-            FalseBool -> pure $ Just elseVal
-            _other -> pure Nothing
-    | otherwise =
-        throwE . renderText $ "KEQUAL.ite: wrong arity " <> pretty (length args)
-
-equalsKHook :: BuiltinFunction
-equalsKHook args
-    | [KSeq _ l, KSeq _ r] <- args = pure $ evalEqualsK l r
-    | otherwise =
-        throwE . renderText $ "KEQUAL.eq: wrong arity " <> pretty (length args)
-
-nequalsKHook :: BuiltinFunction
-nequalsKHook args
-    | [KSeq _ l, KSeq _ r] <- args = pure $ negateBool <$> evalEqualsK l r
-    | otherwise =
-        throwE . renderText $ "KEQUAL.ne: wrong arity " <> pretty (length args)
-
-evalEqualsK :: Term -> Term -> Maybe Term
-evalEqualsK (SymbolApplication sL _ argsL) (SymbolApplication sR _ argsR)
-    | isConstructorSymbol sL && isConstructorSymbol sR =
-        if sL == sR
-            then foldAndBool <$> zipWithM evalEqualsK argsL argsR
-            else pure FalseBool
-evalEqualsK (SymbolApplication symbol _ _) DomainValue{}
-    | isConstructorSymbol symbol = pure FalseBool
-evalEqualsK (SymbolApplication symbol _ _) Injection{}
-    | isConstructorSymbol symbol = pure FalseBool
-evalEqualsK (SymbolApplication symbol _ _) KMap{}
-    | isConstructorSymbol symbol = pure FalseBool
-evalEqualsK (SymbolApplication symbol _ _) KList{}
-    | isConstructorSymbol symbol = pure FalseBool
-evalEqualsK (SymbolApplication symbol _ _) KSet{}
-    | isConstructorSymbol symbol = pure FalseBool
-evalEqualsK DomainValue{} (SymbolApplication symbol _ _)
-    | isConstructorSymbol symbol = pure FalseBool
-evalEqualsK Injection{} (SymbolApplication symbol _ _)
-    | isConstructorSymbol symbol = pure FalseBool
-evalEqualsK KMap{} (SymbolApplication symbol _ _)
-    | isConstructorSymbol symbol = pure FalseBool
-evalEqualsK KList{} (SymbolApplication symbol _ _)
-    | isConstructorSymbol symbol = pure FalseBool
-evalEqualsK KSet{} (SymbolApplication symbol _ _)
-    | isConstructorSymbol symbol = pure FalseBool
-evalEqualsK (Injection s1L s2L l) (Injection s1R s2R r)
-    | s1L == s1R && s2L == s2R = evalEqualsK l r
-evalEqualsK l@DomainValue{} r@DomainValue{} =
-    pure $ if l == r then TrueBool else FalseBool
-evalEqualsK l r =
-    if l == r
-        then pure TrueBool
-        else fail "cannot evaluate" -- i.e., result is Nothing
-
--- check for simple (parameter-less) sorts
-shouldHaveSort :: Term -> SortName -> Except Text ()
-t `shouldHaveSort` s
-    | sortOfTerm t == SortApp s [] =
-        pure ()
-    | otherwise =
-        throwE . renderText . vsep $
-            [ pretty $ "Argument term has unexpected sort (expected " <> show s <> "):"
-            , pretty t
-            ]

booster/library/Booster/Builtin/BOOL.hs

@@ -0,0 +1,79 @@
+{- |
+Copyright   : (c) Runtime Verification, 2023
+License     : BSD-3-Clause
+
+Built-in functions (hooks) in the BOOL namespace, as described in
+[docs/hooks.md](https://github.com/runtimeverification/haskell-backend/blob/master/docs/hooks.md).
+-}
+module Booster.Builtin.BOOL (
+    builtinsBOOL,
+    boolTerm,
+) where
+
+import Data.ByteString.Char8 (ByteString)
+import Data.Map (Map)
+import Data.Map qualified as Map
+
+import Booster.Builtin.Base
+import Booster.Pattern.Base
+import Booster.Pattern.Bool
+
+builtinsBOOL :: Map ByteString BuiltinFunction
+builtinsBOOL =
+    Map.mapKeys ("BOOL." <>) $
+        Map.fromList
+            [ "or" ~~> orHook
+            , "and" ~~> andHook
+            , "xor" ~~> boolOperator (/=)
+            , "eq" ~~> boolOperator (==)
+            , "ne" ~~> boolOperator (/=)
+            , "not" ~~> notHook
+            , "implies" ~~> impliesHook
+            ]
+
+-- shortcut evaluations for or and and
+orHook :: BuiltinFunction
+orHook args
+    | length args /= 2 = arityError "BOOL.or" 2 args
+    | [TrueBool, _] <- args = pure $ Just TrueBool
+    | [_, TrueBool] <- args = pure $ Just TrueBool
+    | [FalseBool, FalseBool] <- args = pure $ Just FalseBool
+    | otherwise = pure Nothing -- arguments not determined
+
+andHook :: BuiltinFunction
+andHook args
+    | length args /= 2 = arityError "BOOL.and" 2 args
+    | [FalseBool, _] <- args = pure $ Just FalseBool
+    | [_, FalseBool] <- args = pure $ Just FalseBool
+    | [TrueBool, TrueBool] <- args = pure $ Just TrueBool
+    | otherwise = pure Nothing -- arguments not determined
+
+notHook :: BuiltinFunction
+notHook [arg]
+    | Just b <- readBoolTerm arg = pure . Just . boolTerm $ not b
+    | otherwise = pure Nothing
+notHook args = arityError "BOOL.not" 1 args
+
+impliesHook :: BuiltinFunction
+impliesHook args
+    | length args /= 2 = arityError "BOOL.implies" 2 args
+    | [FalseBool, _] <- args = pure $ Just TrueBool
+    | [TrueBool, FalseBool] <- args = pure $ Just FalseBool
+    | [TrueBool, TrueBool] <- args = pure $ Just TrueBool
+    | otherwise = pure Nothing -- arguments not determined
+
+boolOperator :: (Bool -> Bool -> Bool) -> BuiltinFunction
+boolOperator f args
+    | length args /= 2 = arityError "BOOL.<operator>" 2 args
+    | [Just arg1, Just arg2] <- map readBoolTerm args =
+        pure . Just . boolTerm $ f arg1 arg2
+    | otherwise = pure Nothing -- arguments not determined
+
+boolTerm :: Bool -> Term
+boolTerm True = TrueBool
+boolTerm False = FalseBool
+
+readBoolTerm :: Term -> Maybe Bool
+readBoolTerm TrueBool = Just True
+readBoolTerm FalseBool = Just False
+readBoolTerm _other = Nothing

booster/library/Booster/Builtin/Base.hs

@@ -0,0 +1,72 @@
+{- |
+Copyright   : (c) Runtime Verification, 2023
+License     : BSD-3-Clause
+
+Base type definitions and helpers for built-in functions (hooks).
+-}
+module Booster.Builtin.Base (
+    BuiltinFunction,
+    -- helpers
+    (~~>),
+    arityError,
+    isConstructorLike_,
+    shouldHaveSort,
+) where
+
+import Control.Monad.Trans.Except
+import Data.ByteString.Char8 (ByteString)
+import Data.Text (Text)
+import Data.Text qualified as Text
+import Data.Text.Encoding qualified as Text
+import Prettyprinter (pretty)
+
+import Booster.Pattern.Base
+import Booster.Pattern.Util
+import Booster.Prettyprinter
+
+{- |
+
+Built-in functions may fail on arity or sort errors, and may be
+partial (returning a Maybe type)
+
+The built-in function fails outright when its function is called with
+a wrong argument count. When required arguments are unevaluated, the
+hook returns 'Nothing'.
+-}
+type BuiltinFunction = [Term] -> Except Text (Maybe Term)
+
+------------------------------------------------------------
+-- Helpers
+
+(~~>) :: ByteString -> BuiltinFunction -> (ByteString, BuiltinFunction)
+(~~>) = (,)
+
+isConstructorLike_ :: Term -> Bool
+isConstructorLike_ = (.isConstructorLike) . getAttributes
+
+{- | checks that the arguments list has the expected length.
+
+Returns nothing if the arg.count matches, so it can be used as a
+fall-through case in hook function definitions.
+-}
+arityError :: Text -> Int -> [Term] -> Except Text (Maybe Term)
+arityError fname argCount args
+    | l == argCount =
+        pure Nothing
+    | otherwise =
+        throwE $ fname <> Text.pack msg
+  where
+    l = length args
+    msg = unwords [": wrong arity. Expected ", show argCount, ", got ", show l]
+
+-- check for simple (parameter-less) sorts
+shouldHaveSort :: Term -> SortName -> Except Text ()
+t `shouldHaveSort` s
+    | sortOfTerm t == SortApp s [] =
+        pure ()
+    | otherwise =
+        throwE $
+            Text.unlines
+                [ "Argument term has unexpected sort (expected " <> Text.decodeLatin1 s <> "):"
+                , renderText (pretty t)
+                ]