diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,11 @@ +# Changelog + +All notable changes to this project (as seen by library users) will be documented in this file. +The CHANGELOG is available on [Github](https://github.com/luc-tielen/souffle-haskell.git/CHANGELOG.md). + +## [0.1.0] - 2021-04-11 + +### Added + +- Initial version of the library/DSL, split off from the souffle-haskell + package. diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,21 @@ +The MIT License + +Copyright (c) 2021 Luc Tielen + +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to deal +in the Software without restriction, including without limitation the rights +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in +all copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN +THE SOFTWARE. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,45 @@ +# Souffle-dsl + +[![License: MIT](https://img.shields.io/badge/License-MIT-yellow.svg)](https://github.com/luc-tielen/souffle-dsl/blob/master/LICENSE) +[![CircleCI](https://circleci.com/gh/luc-tielen/souffle-dsl.svg?style=svg&circle-token=07fcf633c70820100c529dda8869baa60d4b6dd8)](https://circleci.com/gh/luc-tielen/souffle-haskell) +[![Hackage](https://img.shields.io/hackage/v/souffle-dsl?style=flat-square)](https://hackage.haskell.org/package/souffle-dsl) + +This repo provides a Haskell EDSL for writing [Souffle](https://github.com/souffle-lang/souffle) +Datalog code directly in Haskell. This DSL was initially included in the +[souffle-haskell](https://github.com/luc-tielen/souffle-haskell.git) repo, but +is now a standalone package. + +## Documentation + +The documentation for the library can be found on +[Hackage](https://hackage.haskell.org/package/souffle-dsl). +The documentation from [souffle-haskell](https://hackage.haskell.org/package/souffle-haskell) +is also relevant. + +## Contributing + +TLDR: Nix-based project; the Makefile contains the most commonly used commands. + +Long version: + +The project makes use of [Nix](https://nixos.org/nix/download.html) to setup the development environment. +Setup your environment by entering the following command: + +```bash +$ cachix use luctielen # Optional (improves setup time *significantly*) +$ nix-shell +``` + +After this command, you can build the project: + +```bash +$ make configure # configures the project +$ make build # builds the haskell code +$ make lint # runs the linter +$ make hoogle # starts a local hoogle webserver +``` + +## Issues + +Found an issue or missing a piece of functionality? +Please open an issue with a description of the problem. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,3 @@ +import Distribution.Simple +main = defaultMain + diff --git a/lib/Language/Souffle/DSL.hs b/lib/Language/Souffle/DSL.hs new file mode 100644 --- /dev/null +++ b/lib/Language/Souffle/DSL.hs @@ -0,0 +1,1104 @@ +{-# LANGUAGE GADTs, RankNTypes, DataKinds, TypeOperators, ConstraintKinds #-} +{-# LANGUAGE UndecidableInstances, UndecidableSuperClasses, FlexibleContexts #-} +{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DerivingVia, ScopedTypeVariables #-} +{-# LANGUAGE PolyKinds, TypeFamilyDependencies #-} +{-# OPTIONS_GHC -Wno-redundant-constraints #-} + +{-| This module provides an experimental DSL for generating Souffle Datalog code, + directly from Haskell. + + The module is meant to be imported unqualified, unlike the rest of this + library. This allows for a syntax that is very close to the corresponding + Datalog syntax you would normally write. + + The functions and operators provided by this module follow a naming scheme: + + - If there is no clash with something imported via Prelude, the + function or operator is named exactly the same as in Souffle. + - If there is a clash for functions, an apostrophe is appended + (e.g. "max" in Datalog is 'max'' in Haskell). + - Most operators (besides those from the Num typeclass) start with a "." + (e.g. '.^' is the "^" operator in Datalog) + + The DSL makes heavy use of Haskell's typesystem to avoid + many kinds of errors. This being said, not everything can be checked at + compile-time (for example performing comparisons on ungrounded variables + can't be checked). For this reason you should regularly write the + Datalog code to a file while prototyping your algorithm and check it using + the Souffle executable for errors. + + A large subset of the Souffle language is covered, with some exceptions + such as "$", aggregates, ... There are no special functions for supporting + components either, but this is automatically possible by making use of + polymorphism in Haskell. + + Here's an example snippet of Haskell code that can generate Datalog code: + + @ + -- Assuming we have 2 types of facts named Edge and Reachable: + data Edge = Edge String String + data Reachable = Reachable String String + + program = do + Predicate edge <- predicateFor \@Edge + Predicate reachable <- predicateFor \@Reachable + a <- var "a" + b <- var "b" + c <- var "c" + reachable(a, b) |- edge(a, b) + reachable(a, b) |- do + edge(a, c) + reachable(c, b) + @ + + When rendered to a file (using 'renderIO'), this generates the following + Souffle code: + + @ + .decl edge(t1: symbol, t2: symbol) + .input edge + .decl reachable(t1: symbol, t2: symbol) + .output reachable + reachable(a, b) :- + edge(a, b) + reachable(a, b) :- do + edge(a, c) + reachable(c, b) + @ + + For more examples, take a look at the . +-} +module Language.Souffle.DSL + ( -- * DSL-related types and functions + -- ** Types + Predicate(..) + , Fragment + , Tuple + , DSL + , Head + , Body + , Term + , VarName + , UsageContext(..) + , Direction(..) + , ToPredicate + , FactMetadata(..) + , Metadata(..) + , StructureOpt(..) + , InlineOpt(..) + -- ** Basic building blocks + , predicateFor + , var + , __ + , underscore + , (|-) + , (\/) + , not' + -- ** Souffle operators + , (.<) + , (.<=) + , (.>) + , (.>=) + , (.=) + , (.!=) + , (.^) + , (.%) + , band + , bor + , bxor + , lor + , land + -- ** Souffle functions + , max' + , min' + , cat + , contains + , match + , ord + , strlen + , substr + , to_number + , to_string + -- * Functions for running a Datalog DSL fragment / AST directly. + , runSouffleInterpretedWith + , runSouffleInterpreted + , embedProgram + -- * Rendering functions + , render + , renderIO + -- * Helper type families useful in some situations + , Structure + , NoVarsInAtom + , SupportsArithmetic + ) where + +import Control.Monad.Reader +import Control.Monad.State +import Control.Monad.Writer +import Data.Int +import Data.Kind +import Data.List.NonEmpty (NonEmpty(..), toList) +import Data.Map ( Map ) +import qualified Data.Map as Map +import Data.Maybe (fromMaybe, catMaybes, mapMaybe) +import Data.Proxy +import Data.String +import qualified Data.Text as T +import qualified Data.Text.IO as TIO +import qualified Data.Text.Lazy as TL +import Data.Word +import GHC.Generics +import GHC.TypeLits +import Language.Haskell.TH.Syntax (qRunIO, qAddForeignFilePath, Q, Dec, ForeignSrcLang(..)) +import Language.Souffle.Class ( Program(..), Fact(..), ContainsFact, Direction(..) ) +import Language.Souffle.Internal.Constraints (SimpleProduct) +import qualified Language.Souffle.Interpreted as I +import System.Directory +import System.FilePath +import System.IO.Temp +import System.Process +import Text.Printf (printf) +import Type.Errors.Pretty + + +-- | A datatype that contains a function for generating Datalog AST fragments +-- that can be glued together using other functions in this module. +-- +-- The rank-N type allows using the inner function in multiple places to +-- generate different parts of the AST. This is one of the key things +-- that allows writing Haskell code in a very smilar way to the Datalog code. +-- +-- The inner function uses the 'Structure' of a type to compute what the +-- shape of the input tuple for the predicate should be. For example, if a +-- fact has a data constructor containing a Float and a String, +-- the resulting tuple will be of type ('Term' ctx Float, 'Term' ctx String). +-- +-- Currently, only facts with up to 10 fields are supported. If you need more +-- fields, please file an issue on +-- . +newtype Predicate a + = Predicate (forall f ctx. Fragment f ctx => Tuple ctx (Structure a) -> f ctx ()) + +type VarMap = Map VarName Int + +-- | The main monad in which Datalog AST fragments are combined together +-- using other functions in this module. +-- +-- - The "prog" type variable is used for performing many compile time checks. +-- This variable is filled (automatically) with a type that implements the +-- 'Program' typeclass. +-- - The "ctx" type variable is the context in which a DSL fragment is used. +-- For more information, see 'UsageContext'. +-- - The "a" type variable is the value contained inside +-- (just like other monads). +newtype DSL prog ctx a = DSL (StateT VarMap (Writer [AST]) a) + deriving (Functor, Applicative, Monad, MonadWriter [AST], MonadState VarMap) + via (StateT VarMap (Writer [AST])) + +addDefinition :: AST -> DSL prog 'Definition () +addDefinition dl = tell [dl] + +-- | This function runs the DSL fragment directly using the souffle interpreter +-- executable. +-- +-- It does this by saving the fragment to a temporary file right before +-- running the souffle interpreter. All created files are automatically +-- cleaned up after the souffle related actions have been executed. If this is +-- not your intended behavior, see 'runSouffleInterpretedWith' which allows +-- passing in different interpreter settings. +runSouffleInterpreted + :: (MonadIO m, Program prog) + => prog + -> DSL prog 'Definition () + -> (Maybe (I.Handle prog) -> I.SouffleM a) + -> m a +runSouffleInterpreted program dsl f = liftIO $ do + tmpDir <- getCanonicalTemporaryDirectory + souffleHsDir <- createTempDirectory tmpDir "souffle-haskell" + defaultCfg <- I.defaultConfig + let cfg = defaultCfg { I.cfgDatalogDir = souffleHsDir + , I.cfgFactDir = Just souffleHsDir + , I.cfgOutputDir = Just souffleHsDir + } + runSouffleInterpretedWith cfg program dsl f <* removeDirectoryRecursive souffleHsDir + +-- | This function runs the DSL fragment directly using the souffle interpreter +-- executable. +-- +-- It does this by saving the fragment to a file in the directory specified by +-- the 'I.cfgDatalogDir' field in the interpreter settings. Depending on the +-- chosen settings, the fact and output files may not be automatically cleaned +-- up after running the souffle interpreter. See 'I.runSouffleWith' for more +-- information on automatic cleanup. +runSouffleInterpretedWith + :: (MonadIO m, Program prog) + => I.Config + -> prog + -> DSL prog 'Definition () + -> (Maybe (I.Handle prog) -> I.SouffleM a) + -> m a +runSouffleInterpretedWith config program dsl f = liftIO $ do + let progName = programName program + datalogFile = I.cfgDatalogDir config progName <.> "dl" + renderIO program datalogFile dsl + I.runSouffleWith config program f + +-- | Embeds a Datalog program from a DSL fragment directly in a Haskell file. +-- +-- Note that due to TemplateHaskell staging restrictions, this function must +-- be used in a different module than the module where 'Program' and 'Fact' +-- instances are defined. +-- +-- In order to use this function correctly, you have to add the following +-- line to the top of the module where 'embedProgram' is used in order +-- for the embedded C++ code to be compiled correctly: +-- +-- > {-# OPTIONS_GHC -optc-std=c++17 -D__EMBEDDED_SOUFFLE__ #-} +embedProgram :: Program prog => prog -> DSL prog 'Definition () -> Q [Dec] +embedProgram program dsl = do + cppFile <- qRunIO $ do + tmpDir <- getCanonicalTemporaryDirectory + souffleHsDir <- createTempDirectory tmpDir "souffle-haskell" + let progName = programName program + datalogFile = souffleHsDir progName <.> "dl" + cppFile = souffleHsDir progName <.> "cpp" + renderIO program datalogFile dsl + callCommand $ printf "souffle -g %s %s" cppFile datalogFile + pure cppFile + qAddForeignFilePath LangCxx cppFile + pure [] + +runDSL :: Program prog => prog -> DSL prog 'Definition a -> DL +runDSL _ (DSL a) = Statements $ mapMaybe simplify $ execWriter (evalStateT a mempty) where + simplify = \case + Declare' name dir fields opts -> pure $ Declare name dir fields opts + Rule' name terms body -> Rule name terms <$> simplify body + Atom' name terms -> pure $ Atom name terms + And' exprs -> case mapMaybe simplify exprs of + [] -> Nothing + exprs' -> pure $ foldl1 And exprs' + Or' exprs -> case mapMaybe simplify exprs of + [] -> Nothing + exprs' -> pure $ foldl1 Or exprs' + Not' expr -> Not <$> simplify expr + Constrain' e -> pure $ Constrain e + +-- | Generates a unique variable, using the name argument as a hint. +-- +-- The type of the variable is determined the first predicate it is used in. +-- The 'NoVarsInAtom' constraint generates a user-friendly type error if the +-- generated variable is used inside a relation (which is not valid in +-- Datalog). +-- +-- Note: If a variable is created but not used using this function, you will +-- get a compile-time error because it can't deduce the constraint. +var :: NoVarsInAtom ctx => VarName -> DSL prog ctx' (Term ctx ty) +var name = do + count <- gets (fromMaybe 0 . Map.lookup name) + modify $ Map.insert name (count + 1) + let varName = if count == 0 then name else name <> "_" <> T.pack (show count) + pure $ VarTerm varName + +-- | Data type representing the head of a relation +-- (the part before ":-" in a Datalog relation). +-- +-- - The "ctx" type variable is the context in which this type is used. +-- For this type, this will always be 'Relation'. The variable is there to +-- perform some compile-time checks. +-- - The "unused" type variable is unused and only there so the type has the +-- same kind as 'Body' and 'DSL'. +-- +-- See also '|-'. +data Head ctx unused + = Head Name (NonEmpty SimpleTerm) + +-- | Data type representing the body of a relation +-- (what follows after ":-" in a Datalog relation). +-- +-- By being a monad, it supports do-notation which allows for a syntax +-- that is quite close to Datalog. +-- +-- - The "ctx" type variable is the context in which this type is used. +-- For this type, this will always be 'Relation'. The variable is there to +-- perform some compile-time checks. +-- - The "a" type variable is the value contained inside +-- (just like other monads). +-- +-- See also '|-'. +newtype Body ctx a = Body (Writer [AST] a) + deriving (Functor, Applicative, Monad, MonadWriter [AST]) + via (Writer [AST]) + +-- | Creates a fragment that is the logical disjunction (OR) of 2 sub-fragments. +-- This corresponds with ";" in Datalog. +(\/) :: Body ctx () -> Body ctx () -> Body ctx () +body1 \/ body2 = do + let rules1 = And' $ runBody body1 + rules2 = And' $ runBody body2 + tell [Or' [rules1, rules2]] + +-- | Creates a fragment that is the logical negation of a sub-fragment. +-- This is equivalent to "!" in Datalog. (But this operator can't be used +-- in Haskell since it only allows unary negation as a prefix operator.) +not' :: Body ctx a -> Body ctx () +not' body = do + let rules = And' $ runBody body + tell [Not' rules] + +runBody :: Body ctx a -> [AST] +runBody (Body m) = execWriter m + +data TypeInfo (a :: k) (ts :: [Type]) = TypeInfo + +-- | Constraint that makes sure a type can be converted to a predicate function. +-- It gives a user-friendly error in case any of the sub-constraints +-- are not met. +type ToPredicate prog a = + ( Fact a + , FactMetadata a + , ContainsFact prog a + , SimpleProduct a + , Assert (Length (Structure a) <=? 10) BigTupleError + , KnownDLTypes (Structure a) + , KnownDirection (FactDirection a) + , KnownSymbols (AccessorNames a) + , ToTerms (Structure a) + ) + +-- | A typeclass for optionally configuring extra settings +-- (for performance reasons). + +-- Since it contains no required functions, it is possible to derive this +-- typeclass automatically (this gives you the default behavior): +-- +-- @ +-- data Edge = Edge String String +-- deriving (Generic, Marshal, FactMetadata) +-- @ +class (Fact a, SimpleProduct a) => FactMetadata a where + -- | An optional function for configuring fact metadata. + -- + -- By default no extra options are configured. + -- For more information, see the 'Metadata' type. + factOpts :: Proxy a -> Metadata a + factOpts = const $ Metadata Automatic NoInline + +-- | A data type that allows for finetuning of fact settings +-- (for performance reasons). +data Metadata a + = Metadata (StructureOpt a) (InlineOpt (FactDirection a)) + +-- | Datatype describing the way a fact is stored inside Datalog. +-- A different choice of storage type can lead to an improvement in +-- performance (potentially). +-- +-- For more information, see this +-- and this +-- . +data StructureOpt (a :: Type) where + -- | Automatically choose the underlying storage for a relation. + -- This is the storage type that is used by default. + -- + -- For Souffle, it will choose a direct btree for facts with arity <= 6. + -- For larger facts, it will use an indirect btree. + Automatic :: StructureOpt a + -- | Uses a direct btree structure. + BTree :: StructureOpt a + -- | Uses a brie structure. This can improve performance in some cases and is + -- more memory efficient for particularly large relations. + Brie :: StructureOpt a + -- | A high performance datastructure optimised specifically for equivalence + -- relations. This is only valid for binary facts with 2 fields of the + -- same type. + EqRel :: (IsBinaryRelation a, Structure a ~ '[t, t]) => StructureOpt a + +type IsBinaryRelation a = + Assert (Length (Structure a) == 2) + ("Equivalence relations are only allowed with binary relations" <> ".") + +-- | Datatype indicating if we should inline a fact or not. +data InlineOpt (d :: Direction) where + -- | Inlines the fact, only possible for internal facts. + Inline :: InlineOpt 'Internal + -- | Does not inline the fact. + NoInline :: InlineOpt d + +-- | Generates a function for a type that implements 'Fact' and is a +-- 'SimpleProduct'. The predicate function takes the same amount of arguments +-- as the original fact type. Calling the function with a tuple of arguments, +-- creates fragments of datalog code that can be glued together using other +-- functions in this module. +-- +-- Note: You need to specify for which fact you want to return a predicate +-- for using TypeApplications. +predicateFor :: forall a prog. ToPredicate prog a => DSL prog 'Definition (Predicate a) +predicateFor = do + let typeInfo = TypeInfo :: TypeInfo a (Structure a) + p = Proxy :: Proxy a + name = T.pack $ factName p + accNames = fromMaybe genericNames $ accessorNames p + opts = toSimpleMetadata $ factOpts p + genericNames = map (("t" <>) . T.pack . show) [1..] + tys = getTypes (Proxy :: Proxy (Structure a)) + direction = getDirection (Proxy :: Proxy (FactDirection a)) + fields = zipWith FieldData tys accNames + definition = Declare' name direction fields opts + addDefinition definition + pure $ Predicate $ toFragment typeInfo name + +toSimpleMetadata :: Metadata a -> SimpleMetadata +toSimpleMetadata (Metadata struct inline) = + let structOpt = case struct of + Automatic -> AutomaticLayout + BTree -> BTreeLayout + Brie -> BrieLayout + EqRel -> EqRelLayout + inlineOpt = case inline of + Inline -> DoInline + NoInline -> DoNotInline + in SimpleMetadata structOpt inlineOpt + +class KnownDirection a where + getDirection :: Proxy a -> Direction +instance KnownDirection 'Input where getDirection = const Input +instance KnownDirection 'Output where getDirection = const Output +instance KnownDirection 'InputOutput where getDirection = const InputOutput +instance KnownDirection 'Internal where getDirection = const Internal + +-- | Turnstile operator from Datalog, used in relations. +-- +-- This is used for creating a DSL fragment that contains a relation. +-- NOTE: |- is used instead of :- due to limitations of the Haskell syntax. +(|-) :: Head 'Relation a -> Body 'Relation () -> DSL prog 'Definition () +Head name terms |- body = + let rules = runBody body + relation = Rule' name terms (And' rules) + in addDefinition relation + +infixl 0 |- + +-- | A typeclass used for generating AST fragments of Datalog code. +-- The generated fragments can be further glued together using the +-- various functions in this module. +class Fragment f ctx where + toFragment :: ToTerms ts => TypeInfo a ts -> Name -> Tuple ctx ts -> f ctx () + +instance Fragment Head 'Relation where + toFragment typeInfo name terms = + let terms' = toTerms (Proxy :: Proxy 'Relation) typeInfo terms + in Head name terms' + +instance Fragment Body 'Relation where + toFragment typeInfo name terms = + let terms' = toTerms (Proxy :: Proxy 'Relation) typeInfo terms + in tell [Atom' name terms'] + +instance Fragment (DSL prog) 'Definition where + toFragment typeInfo name terms = + let terms' = toTerms (Proxy :: Proxy 'Definition) typeInfo terms + in addDefinition $ Atom' name terms' + + +data RenderMode = Nested | TopLevel + +-- | Renders a DSL fragment to the corresponding Datalog code and writes it to +-- a file. +renderIO :: Program prog => prog -> FilePath -> DSL prog 'Definition () -> IO () +renderIO prog path = TIO.writeFile path . render prog + +-- | Renders a DSL fragment to the corresponding Datalog code. +render :: Program prog => prog -> DSL prog 'Definition () -> T.Text +render prog = flip runReader TopLevel . f . runDSL prog where + f = \case + Statements stmts -> + T.unlines <$> traverse f stmts + Declare name dir fields metadata -> + let fieldPairs = map renderField fields + renderedFactOpts = renderMetadata metadata + renderedOpts = if T.null renderedFactOpts then "" else " " <> renderedFactOpts + in pure $ T.intercalate "\n" $ catMaybes + [ Just $ ".decl " <> name <> "(" <> T.intercalate ", " fieldPairs <> ")" <> renderedOpts + , renderDir name dir + ] + Atom name terms -> do + let rendered = name <> "(" <> renderTerms (toList terms) <> ")" + end <- maybeDot + pure $ rendered <> end + Rule name terms body -> do + body' <- f body + let rendered = + name <> "(" <> renderTerms (toList terms) <> ") :-\n" <> + T.intercalate "\n" (map indent $ T.lines body') + pure rendered + And e1 e2 -> do + txt <- nested $ do + txt1 <- f e1 + txt2 <- f e2 + pure $ txt1 <> ",\n" <> txt2 + end <- maybeDot + pure $ txt <> end + Or e1 e2 -> do + txt <- nested $ do + txt1 <- f e1 + txt2 <- f e2 + pure $ txt1 <> ";\n" <> txt2 + end <- maybeDot + case end of + "." -> pure $ txt <> end + _ -> pure $ "(" <> txt <> ")" + Not e -> do + let maybeAddParens txt = case e of + And _ _ -> "(" <> txt <> ")" + _ -> txt + txt <- maybeAddParens <$> nested (f e) + end <- maybeDot + case end of + "." -> pure $ "!" <> txt <> end + _ -> pure $ "!" <> txt + Constrain t -> do + let t' = renderTerm t + end <- maybeDot + case end of + "." -> pure $ t' <> "." + _ -> pure t' + indent = (" " <>) + nested = local (const Nested) + maybeDot = ask >>= \case + TopLevel -> pure "." + Nested -> pure mempty + +renderDir :: VarName -> Direction -> Maybe T.Text +renderDir name = \case + Input -> Just $ ".input " <> name + Output -> Just $ ".output " <> name + InputOutput -> Just $ T.intercalate "\n" + $ catMaybes [renderDir name Input, renderDir name Output] + Internal -> Nothing + +renderField :: FieldData -> T.Text +renderField (FieldData ty accName) = + let txt = case ty of + DLNumber -> ": number" + DLUnsigned -> ": unsigned" + DLFloat -> ": float" + DLString -> ": symbol" + in accName <> txt + +renderMetadata :: SimpleMetadata -> T.Text +renderMetadata (SimpleMetadata struct inline) = + let structTxt = case struct of + AutomaticLayout -> Nothing + BTreeLayout -> Just "btree" + BrieLayout -> Just "brie" + EqRelLayout -> Just "eqrel" + inlineTxt = case inline of + DoInline -> Just "inline" + DoNotInline -> Nothing + in T.intercalate " " $ catMaybes [structTxt, inlineTxt] + +renderTerms :: [SimpleTerm] -> T.Text +renderTerms = T.intercalate ", " . map renderTerm + +renderTerm :: SimpleTerm -> T.Text +renderTerm = \case + I x -> T.pack $ show x + U x -> T.pack $ show x + F x -> T.pack $ printf "%f" x + S s -> "\"" <> T.pack s <> "\"" + V v -> v + Underscore -> "_" + + BinOp' op t1 t2 -> renderTerm t1 <> " " <> renderBinOp op <> " " <> renderTerm t2 + UnaryOp' op t1 -> renderUnaryOp op <> renderTerm t1 + Func' name ts -> renderFunc name <> "(" <> renderTerms (toList ts) <> ")" + where + renderFunc = \case + Max -> "max" + Min -> "min" + Cat -> "cat" + Contains -> "contains" + Match -> "match" + Ord -> "ord" + StrLen -> "strlen" + Substr -> "substr" + ToNumber -> "to_number" + ToString -> "to_string" + renderBinOp = \case + Plus -> "+" + Mul -> "*" + Subtract -> "-" + Div -> "/" + Pow -> "^" + Rem -> "%" + BinaryAnd -> "band" + BinaryOr -> "bor" + BinaryXor -> "bxor" + LogicalAnd -> "land" + LogicalOr -> "lor" + LessThan -> "<" + LessThanOrEqual -> "<=" + GreaterThan -> ">" + GreaterThanOrEqual -> ">=" + IsEqual -> "=" + IsNotEqual -> "!=" + renderUnaryOp Negate = "-" + + +type Name = T.Text + +-- | Type representing a variable name in Datalog. +type VarName = T.Text + +type AccessorName = T.Text + +data DLType + = DLNumber + | DLUnsigned + | DLFloat + | DLString + +data FieldData = FieldData DLType AccessorName + +-- | A type level tag describing in which context a DSL fragment is used. +-- This is only used on the type level and helps catch some semantic errors +-- at compile time. +data UsageContext + = Definition + -- ^ A DSL fragment is used in a top level definition. + | Relation + -- ^ A DSL fragment is used inside a relation (either head or body of a relation). + +-- | A type family used for generating a user-friendly type error in case +-- you use a variable in a DSL fragment where it is not allowed +-- (outside of relations). +type family NoVarsInAtom (ctx :: UsageContext) :: Constraint where + NoVarsInAtom ctx = Assert (ctx == 'Relation) NoVarsInAtomError + +type NoVarsInAtomError = + ( "You tried to use a variable in a top level fact, which is not supported in Souffle." + % "Possible solutions:" + % " - Move the fact inside a rule body." + % " - Replace the variable in the fact with a string, number, unsigned or float constant." + ) + +-- | Data type for representing Datalog terms. +-- +-- All constructors are hidden, but with the `Num`, 'Fractional' and +-- `IsString` instances it is possible to create terms using Haskell syntax +-- for literals. For non-literal values, smart constructors are provided. +-- (See for example 'underscore' / '__'.) +data Term ctx ty where + -- NOTE: type family is used here instead of "Term 'Relation ty"; + -- this allows giving a better type error in some situations. + VarTerm :: NoVarsInAtom ctx => VarName -> Term ctx ty + UnderscoreTerm :: Term ctx ty + NumberTerm :: Int32 -> Term ctx Int32 + UnsignedTerm :: Word32 -> Term ctx Word32 + FloatTerm :: Float -> Term ctx Float + StringTerm :: ToString ty => ty -> Term ctx ty + + UnaryOp :: Num ty => Op1 -> Term ctx ty -> Term ctx ty + BinOp :: Num ty => Op2 -> Term ctx ty -> Term ctx ty -> Term ctx ty + Func :: FuncName -> NonEmpty SimpleTerm -> Term ctx ty2 + +data Op2 + = Plus + | Mul + | Subtract + | Div + | Pow + | Rem + | BinaryAnd + | BinaryOr + | BinaryXor + | LogicalAnd + | LogicalOr + | LessThan + | LessThanOrEqual + | GreaterThan + | GreaterThanOrEqual + | IsEqual + | IsNotEqual + +data Op1 = Negate + +data FuncName + = Max + | Min + | Cat + | Contains + | Match + | Ord + | StrLen + | Substr + | ToNumber + | ToString + + +-- | Term representing a wildcard ("_") in Datalog. +underscore :: Term ctx ty +underscore = UnderscoreTerm + +-- | Term representing a wildcard ("_") in Datalog. Note that in the DSL this +-- is with 2 underscores. (Single underscore is reserved for typed holes!) +__ :: Term ctx ty +__ = underscore + +class ToString a where + toString :: a -> String + +instance ToString String where toString = id +instance ToString T.Text where toString = T.unpack +instance ToString TL.Text where toString = TL.unpack + +instance IsString (Term ctx String) where fromString = StringTerm +instance IsString (Term ctx T.Text) where fromString = StringTerm . T.pack +instance IsString (Term ctx TL.Text) where fromString = StringTerm . TL.pack + +-- | A helper typeclass, mainly used for avoiding a lot of boilerplate +-- in the 'Num' instance for 'Term'. +class Num ty => SupportsArithmetic ty where + fromInteger' :: Integer -> Term ctx ty + +instance SupportsArithmetic Int32 where + fromInteger' = NumberTerm . fromInteger +instance SupportsArithmetic Word32 where + fromInteger' = UnsignedTerm . fromInteger +instance SupportsArithmetic Float where + fromInteger' = FloatTerm . fromInteger + +instance (SupportsArithmetic ty, Num ty) => Num (Term ctx ty) where + fromInteger = fromInteger' + (+) = BinOp Plus + (*) = BinOp Mul + (-) = BinOp Subtract + negate = UnaryOp Negate + abs = error "'abs' is not supported for Souffle terms" + signum = error "'signum' is not supported for Souffle terms" + +instance Fractional (Term ctx Float) where + fromRational = FloatTerm . fromRational + (/) = BinOp Div + +-- | Exponentiation operator ("^" in Datalog). +(.^) :: Num ty => Term ctx ty -> Term ctx ty -> Term ctx ty +(.^) = BinOp Pow + +-- | Remainder operator ("%" in Datalog). +(.%) :: (Num ty, Integral ty) => Term ctx ty -> Term ctx ty -> Term ctx ty +(.%) = BinOp Rem + +-- | Creates a less than constraint (a < b), for use in the body of a relation. +(.<) :: Num ty => Term ctx ty -> Term ctx ty -> Body ctx () +(.<) = addConstraint LessThan +infix 1 .< + +-- | Creates a less than or equal constraint (a <= b), for use in the body of +-- a relation. +(.<=) :: Num ty => Term ctx ty -> Term ctx ty -> Body ctx () +(.<=) = addConstraint LessThanOrEqual +infix 1 .<= + +-- | Creates a greater than constraint (a > b), for use in the body of a relation. +(.>) :: Num ty => Term ctx ty -> Term ctx ty -> Body ctx () +(.>) = addConstraint GreaterThan +infix 1 .> + +-- | Creates a greater than or equal constraint (a >= b), for use in the body of +-- a relation. +(.>=) :: Num ty => Term ctx ty -> Term ctx ty -> Body ctx () +(.>=) = addConstraint GreaterThanOrEqual +infix 1 .>= + +-- | Creates a constraint that 2 terms should be equal to each other (a = b), +-- for use in the body of a relation. +(.=) :: Term ctx ty -> Term ctx ty -> Body ctx () +(.=) = addConstraint IsEqual +infix 1 .= + +-- | Creates a constraint that 2 terms should not be equal to each other +-- (a != b), for use in the body of a relation. +(.!=) :: Term ctx ty -> Term ctx ty -> Body ctx () +(.!=) = addConstraint IsNotEqual +infix 1 .!= + +addConstraint :: Op2 -> Term ctx ty -> Term ctx ty -> Body ctx () +addConstraint op e1 e2 = + let expr = BinOp' op (toTerm e1) (toTerm e2) + in tell [Constrain' expr] + +-- | Binary AND operator. +band :: (Num ty, Integral ty) => Term ctx ty -> Term ctx ty -> Term ctx ty +band = BinOp BinaryAnd + +-- | Binary OR operator. +bor :: (Num ty, Integral ty) => Term ctx ty -> Term ctx ty -> Term ctx ty +bor = BinOp BinaryOr + +-- | Binary XOR operator. +bxor :: (Num ty, Integral ty) => Term ctx ty -> Term ctx ty -> Term ctx ty +bxor = BinOp BinaryXor + +-- | Logical AND operator. +land :: (Num ty, Integral ty) => Term ctx ty -> Term ctx ty -> Term ctx ty +land = BinOp LogicalAnd + +-- | Logical OR operator. +lor :: (Num ty, Integral ty) => Term ctx ty -> Term ctx ty -> Term ctx ty +lor = BinOp LogicalOr + +-- | "max" function. +max' :: Num ty => Term ctx ty -> Term ctx ty -> Term ctx ty +max' = func2 Max + +-- | "min" function. +min' :: Num ty => Term ctx ty -> Term ctx ty -> Term ctx ty +min' = func2 Min + +-- | "cat" function (string concatenation). +cat :: ToString ty => Term ctx ty -> Term ctx ty -> Term ctx ty +cat = func2 Cat + +-- | "contains" predicate, checks if 2nd string contains the first. +contains :: ToString ty => Term ctx ty -> Term ctx ty -> Body ctx () +contains a b = + let expr = toTerm $ func2 Contains a b + in tell [Constrain' expr] + +-- | "match" predicate, checks if a wildcard string matches a given string. +match :: ToString ty => Term ctx ty -> Term ctx ty -> Body ctx () +match p s = + let expr = toTerm $ func2 Match p s + in tell [Constrain' expr] + +-- | "ord" function. +ord :: ToString ty => Term ctx ty -> Term ctx Int32 +ord = func1 Ord + +-- | "strlen" function. +strlen :: ToString ty => Term ctx ty -> Term ctx Int32 +strlen = func1 StrLen + +-- | "substr" function. +substr :: ToString ty => Term ctx ty -> Term ctx Int32 -> Term ctx Int32 -> Term ctx ty +substr a b c = Func Substr $ toTerm a :| [toTerm b, toTerm c] + +-- | "to_number" function. +to_number :: ToString ty => Term ctx ty -> Term ctx Int32 +to_number = func1 ToNumber + +-- | "to_string" function. +to_string :: ToString ty => Term ctx Int32 -> Term ctx ty +to_string = func1 ToString + +func1 :: FuncName -> Term ctx ty -> Term ctx ty2 +func1 name a = Func name $ toTerm a :| [] + +func2 :: FuncName -> Term ctx ty -> Term ctx ty -> Term ctx ty2 +func2 name a b = Func name $ toTerm a :| [toTerm b] + +data SimpleTerm + = V VarName + | I Int32 + | U Word32 + | F Float + | S String + | Underscore + + | BinOp' Op2 SimpleTerm SimpleTerm + | UnaryOp' Op1 SimpleTerm + | Func' FuncName (NonEmpty SimpleTerm) + +data SimpleMetadata = SimpleMetadata StructureOption InlineOption + +data StructureOption + = AutomaticLayout + | BTreeLayout + | BrieLayout + | EqRelLayout + +data InlineOption + = DoInline + | DoNotInline + +data AST + = Declare' VarName Direction [FieldData] SimpleMetadata + | Rule' Name (NonEmpty SimpleTerm) AST + | Atom' Name (NonEmpty SimpleTerm) + | And' [AST] + | Or' [AST] + | Not' AST + | Constrain' SimpleTerm + +data DL + = Statements [DL] + | Declare VarName Direction [FieldData] SimpleMetadata + | Rule Name (NonEmpty SimpleTerm) DL + | Atom Name (NonEmpty SimpleTerm) + | And DL DL + | Or DL DL + | Not DL + | Constrain SimpleTerm + + +class KnownDLTypes (ts :: [Type]) where + getTypes :: Proxy ts -> [DLType] + +instance KnownDLTypes '[] where + getTypes _ = [] + +instance (KnownDLType t, KnownDLTypes ts) => KnownDLTypes (t ': ts) where + getTypes _ = getType (Proxy :: Proxy t) : getTypes (Proxy :: Proxy ts) + +class KnownDLType t where + getType :: Proxy t -> DLType + +instance KnownDLType Int32 where getType = const DLNumber +instance KnownDLType Word32 where getType = const DLUnsigned +instance KnownDLType Float where getType = const DLFloat +instance KnownDLType String where getType = const DLString +instance KnownDLType T.Text where getType = const DLString +instance KnownDLType TL.Text where getType = const DLString + +type family AccessorNames a :: [Symbol] where + AccessorNames a = GetAccessorNames (Rep a) + +type family GetAccessorNames (f :: Type -> Type) :: [Symbol] where + GetAccessorNames (a :*: b) = GetAccessorNames a ++ GetAccessorNames b + GetAccessorNames (C1 ('MetaCons _ _ 'False) _) = '[] + GetAccessorNames (S1 ('MetaSel ('Just name) _ _ _) a) = '[name] ++ GetAccessorNames a + GetAccessorNames (M1 _ _ a) = GetAccessorNames a + GetAccessorNames (K1 _ _) = '[] + +class KnownSymbols (symbols :: [Symbol]) where + toStrings :: Proxy symbols -> [String] + +instance KnownSymbols '[] where + toStrings = const [] + +instance (KnownSymbol s, KnownSymbols symbols) => KnownSymbols (s ': symbols) where + toStrings _ = + let sym = symbolVal (Proxy :: Proxy s) + symbols = toStrings (Proxy :: Proxy symbols) + in sym : symbols + +accessorNames :: forall a. KnownSymbols (AccessorNames a) => Proxy a -> Maybe [T.Text] +accessorNames _ = case toStrings (Proxy :: Proxy (AccessorNames a)) of + [] -> Nothing + names -> Just $ T.pack <$> names + +-- | A type synonym for a tuple consisting of Datalog 'Term's. +-- Only tuples containing up to 10 elements are currently supported. +type Tuple ctx ts = TupleOf (MapType (Term ctx) ts) + +class ToTerms (ts :: [Type]) where + toTerms :: Proxy ctx -> TypeInfo a ts -> Tuple ctx ts -> NonEmpty SimpleTerm + +instance ToTerms '[t] where + toTerms _ _ a = + toTerm a :| [] + +instance ToTerms '[t1, t2] where + toTerms _ _ (a, b) = + toTerm a :| [toTerm b] + +instance ToTerms '[t1, t2, t3] where + toTerms _ _ (a, b, c) = + toTerm a :| [toTerm b, toTerm c] + +instance ToTerms '[t1, t2, t3, t4] where + toTerms _ _ (a, b, c, d) = + toTerm a :| [toTerm b, toTerm c, toTerm d] + +instance ToTerms '[t1, t2, t3, t4, t5] where + toTerms _ _ (a, b, c, d, e) = + toTerm a :| [toTerm b, toTerm c, toTerm d, toTerm e] + +instance ToTerms '[t1, t2, t3, t4, t5, t6] where + toTerms _ _ (a, b, c, d, e, f) = + toTerm a :| [toTerm b, toTerm c, toTerm d, toTerm e, toTerm f] + +instance ToTerms '[t1, t2, t3, t4, t5, t6, t7] where + toTerms _ _ (a, b, c, d, e, f, g) = + toTerm a :| [toTerm b, toTerm c, toTerm d, toTerm e, toTerm f, toTerm g] + +instance ToTerms '[t1, t2, t3, t4, t5, t6, t7, t8] where + toTerms _ _ (a, b, c, d, e, f, g, h) = + toTerm a :| [toTerm b, toTerm c, toTerm d, toTerm e, toTerm f, toTerm g, toTerm h] + +instance ToTerms '[t1, t2, t3, t4, t5, t6, t7, t8, t9] where + toTerms _ _ (a, b, c, d, e, f, g, h, i) = + toTerm a :| [toTerm b, toTerm c, toTerm d, toTerm e, toTerm f, toTerm g, toTerm h, toTerm i] + +instance ToTerms '[t1, t2, t3, t4, t5, t6, t7, t8, t9, t10] where + toTerms _ _ (a, b, c, d, e, f, g, h, i, j) = + toTerm a :| [ toTerm b, toTerm c, toTerm d, toTerm e, toTerm f + , toTerm g, toTerm h, toTerm i, toTerm j + ] + +toTerm :: Term ctx t -> SimpleTerm +toTerm = \case + VarTerm v -> V v + StringTerm s -> S $ toString s + NumberTerm x -> I x + UnsignedTerm x -> U x + FloatTerm x -> F x + UnderscoreTerm -> Underscore + + BinOp op t1 t2 -> BinOp' op (toTerm t1) (toTerm t2) + UnaryOp op t1 -> UnaryOp' op (toTerm t1) + Func name ts -> Func' name ts + + +-- Helper functions / type families / ... + +type family MapType (f :: Type -> Type) (ts :: [Type]) :: [Type] where + MapType _ '[] = '[] + MapType f (t ': ts) = f t ': MapType f ts + +type family Assert (c :: Bool) (msg :: ErrorMessage) :: Constraint where + Assert 'True _ = () + Assert 'False msg = TypeError msg + +type family (a :: k) == (b :: k) :: Bool where + a == a = 'True + _ == _ = 'False + +type family Length (xs :: [Type]) :: Nat where + Length '[] = 0 + Length (_ ': xs) = 1 + Length xs + +-- | A helper type family for computing the list of types used in a data type. +-- (The type family assumes a data type with a single data constructor.) +type family Structure a :: [Type] where + Structure a = Collect (Rep a) + +type family Collect (a :: Type -> Type) where + Collect (a :*: b) = Collect a ++ Collect b + Collect (M1 _ _ a) = Collect a + Collect (K1 _ ty) = '[ty] + +type family a ++ b = c where + '[] ++ b = b + a ++ '[] = a + (a ': b) ++ c = a ': (b ++ c) + +type family TupleOf (ts :: [Type]) = t where + TupleOf '[t] = t + TupleOf '[t1, t2] = (t1, t2) + TupleOf '[t1, t2, t3] = (t1, t2, t3) + TupleOf '[t1, t2, t3, t4] = (t1, t2, t3, t4) + TupleOf '[t1, t2, t3, t4, t5] = (t1, t2, t3, t4, t5) + TupleOf '[t1, t2, t3, t4, t5, t6] = (t1, t2, t3, t4, t5, t6) + TupleOf '[t1, t2, t3, t4, t5, t6, t7] = (t1, t2, t3, t4, t5, t6, t7) + TupleOf '[t1, t2, t3, t4, t5, t6, t7, t8] = (t1, t2, t3, t4, t5, t6, t7, t8) + TupleOf '[t1, t2, t3, t4, t5, t6, t7, t8, t9] = (t1, t2, t3, t4, t5, t6, t7, t8, t9) + TupleOf '[t1, t2, t3, t4, t5, t6, t7, t8, t9, t10] = (t1, t2, t3, t4, t5, t6, t7, t8, t9, t10) + TupleOf _ = TypeError BigTupleError + +type BigTupleError = + ( "The DSL only supports facts/tuples consisting of up to 10 elements." + % "If you need more arguments, please submit an issue on Github " + <> "(https://github.com/luc-tielen/souffle-haskell/issues)" + ) + diff --git a/souffle-dsl.cabal b/souffle-dsl.cabal new file mode 100644 --- /dev/null +++ b/souffle-dsl.cabal @@ -0,0 +1,93 @@ +cabal-version: 2.2 + +-- This file has been generated from package.yaml by hpack version 0.34.2. +-- +-- see: https://github.com/sol/hpack + +name: souffle-dsl +version: 0.1.0 +synopsis: Haskell EDSL for Souffle +description: Haskell EDSL for Souffle. +category: Logic Programming, DSL +homepage: https://github.com/luc-tielen/souffle-dsl#README.md +bug-reports: https://github.com/luc-tielen/souffle-dsl/issues +author: Luc Tielen +maintainer: luc.tielen@gmail.com +copyright: 2021 Luc Tielen +license: MIT +license-file: LICENSE +build-type: Simple +extra-source-files: + README.md + CHANGELOG.md + LICENSE + +source-repository head + type: git + location: https://github.com/luc-tielen/souffle-dsl + +library + exposed-modules: + Language.Souffle.DSL + other-modules: + Paths_souffle_dsl + autogen-modules: + Paths_souffle_dsl + hs-source-dirs: + lib + default-extensions: OverloadedStrings LambdaCase ScopedTypeVariables + ghc-options: -Wall -Weverything -Wno-safe -Wno-unsafe -Wno-implicit-prelude -Wno-missed-specializations -Wno-all-missed-specializations -Wno-missing-import-lists -Wno-type-defaults -Wno-missing-local-signatures -Wno-monomorphism-restriction -Wno-missing-deriving-strategies -Wno-prepositive-qualified-module -Wno-missing-safe-haskell-mode -optP-Wno-nonportable-include-path -fhide-source-paths -fno-show-valid-hole-fits -fno-sort-valid-hole-fits + cxx-options: -std=c++17 -Wall + build-depends: + base >=4.12 && <5 + , containers >=0.6.2.1 && <1 + , directory >=1.3.6.0 && <2 + , filepath >=1.4.2.1 && <2 + , mtl >=2.0 && <3 + , process >=1.6.9.0 && <2 + , souffle-haskell >=2.1.0 && <3 + , template-haskell >=2 && <3 + , temporary >=1.3 && <2 + , text >=1.2.4.0 && <2 + , type-errors-pretty >=0.0.1.0 && <1 + if os(linux) + extra-libraries: + stdc++ + default-language: Haskell2010 + +test-suite souffle-dsl-test + type: exitcode-stdio-1.0 + main-is: test.hs + other-modules: + Test.Language.Souffle.DSL.Fixtures + Test.Language.Souffle.DSL.FixturesCompiled + Test.Language.Souffle.DSLSpec + Paths_souffle_dsl + hs-source-dirs: + tests + default-extensions: OverloadedStrings LambdaCase ScopedTypeVariables + ghc-options: -Wall -Weverything -Wno-safe -Wno-unsafe -Wno-implicit-prelude -Wno-missed-specializations -Wno-all-missed-specializations -Wno-missing-import-lists -Wno-type-defaults -Wno-missing-local-signatures -Wno-monomorphism-restriction -Wno-missing-deriving-strategies -Wno-prepositive-qualified-module -Wno-missing-safe-haskell-mode -optP-Wno-nonportable-include-path -fhide-source-paths -fno-show-valid-hole-fits -fno-sort-valid-hole-fits + cxx-options: -std=c++17 -D__EMBEDDED_SOUFFLE__ + cxx-sources: + tests/fixtures/path.cpp + build-depends: + base >=4.12 && <5 + , containers >=0.6.2.1 && <1 + , directory >=1.3.6.0 && <2 + , filepath >=1.4.2.1 && <2 + , hedgehog ==1.* + , hspec >=2.6.1 && <3.0.0 + , hspec-hedgehog ==0.* + , mtl >=2.0 && <3 + , neat-interpolation ==0.* + , process >=1.6.9.0 && <2 + , souffle-dsl + , souffle-haskell + , template-haskell >=2 && <3 + , temporary >=1.3 && <2 + , text >=1.2.4.0 && <2 + , type-errors-pretty >=0.0.1.0 && <1 + if os(darwin) + extra-libraries: + c++ + default-language: Haskell2010 diff --git a/tests/Test/Language/Souffle/DSL/Fixtures.hs b/tests/Test/Language/Souffle/DSL/Fixtures.hs new file mode 100644 --- /dev/null +++ b/tests/Test/Language/Souffle/DSL/Fixtures.hs @@ -0,0 +1,31 @@ + +{-# LANGUAGE DataKinds, TypeFamilies, DeriveGeneric, DeriveAnyClass #-} + +module Test.Language.Souffle.DSL.Fixtures + ( module Test.Language.Souffle.DSL.Fixtures + ) where + +import GHC.Generics +import Language.Souffle.Class +import Language.Souffle.DSL + +data CompiledProgram = CompiledProgram + +instance Program CompiledProgram where + type ProgramFacts CompiledProgram = [Edge, Reachable] + programName = const "compiledprogram" + +data Edge = Edge String String + deriving (Generic, Marshal, FactMetadata) + +data Reachable = Reachable String String + deriving (Eq, Show, Generic, Marshal, FactMetadata) + +instance Fact Edge where + type FactDirection Edge = 'Input + factName = const "edge" + +instance Fact Reachable where + type FactDirection Reachable = 'Output + factName = const "reachable" + diff --git a/tests/Test/Language/Souffle/DSL/FixturesCompiled.hs b/tests/Test/Language/Souffle/DSL/FixturesCompiled.hs new file mode 100644 --- /dev/null +++ b/tests/Test/Language/Souffle/DSL/FixturesCompiled.hs @@ -0,0 +1,22 @@ + +{-# OPTIONS_GHC -optc-std=c++17 -D__EMBEDDED_SOUFFLE__ #-} +{-# LANGUAGE TypeApplications, TemplateHaskell #-} +module Test.Language.Souffle.DSL.FixturesCompiled () where + +-- NOTE: this module can't be grouped together with "Fixtures" +-- due to TemplateHaskell staging restriction. + +import Test.Language.Souffle.DSL.Fixtures +import Language.Souffle.DSL + +$(embedProgram CompiledProgram $ do + Predicate edge <- predicateFor @Edge + Predicate reachable <- predicateFor @Reachable + a <- var "a" + b <- var "b" + c <- var "c" + reachable(a, b) |- edge(a, b) + reachable(a, b) |- do + edge(a, c) + reachable(c, b) + ) diff --git a/tests/Test/Language/Souffle/DSLSpec.hs b/tests/Test/Language/Souffle/DSLSpec.hs new file mode 100644 --- /dev/null +++ b/tests/Test/Language/Souffle/DSLSpec.hs @@ -0,0 +1,1117 @@ + +{-# LANGUAGE DeriveGeneric, DeriveAnyClass, TypeApplications, QuasiQuotes, TypeOperators #-} +{-# LANGUAGE DataKinds, TypeFamilies #-} + +module Test.Language.Souffle.DSLSpec + ( module Test.Language.Souffle.DSLSpec + ) where + +import qualified Test.Language.Souffle.DSL.Fixtures as F +import Test.Hspec +import GHC.Generics +import Data.Int +import Data.Word +import Data.Maybe (fromJust) +import qualified Data.Text as T +import qualified Data.Text.Lazy as TL +import System.IO.Temp +import Language.Souffle.DSL +import Language.Souffle.Class +import Language.Souffle.Interpreted as I +import Language.Souffle.Compiled as C +import NeatInterpolation + + +data Point = Point { x :: Int32, y :: Int32 } + deriving (Generic, Marshal, FactMetadata) + +newtype IntFact = IntFact Int32 + deriving (Generic, Marshal, FactMetadata) + +newtype UnsignedFact = UnsignedFact Word32 + deriving (Generic, Marshal, FactMetadata) + +newtype FloatFact = FloatFact Float + deriving (Generic, Marshal, FactMetadata) + +data TextFact = TextFact T.Text TL.Text + deriving (Generic, Marshal, FactMetadata) + +data Triple = Triple String Int32 String + deriving (Generic, Marshal, FactMetadata) + +newtype Vertex = Vertex String + deriving (Generic, Marshal, FactMetadata) + +data Edge = Edge String String + deriving (Generic, Marshal, FactMetadata) + +data Reachable = Reachable String String + deriving (Eq, Show, Generic, Marshal, FactMetadata) + +newtype BTreeFact = BTreeFact Int32 + deriving (Generic, Marshal) + +newtype BrieFact = BrieFact Int32 + deriving (Generic, Marshal) + +data EqRelFact = EqRelFact Int32 Int32 + deriving (Generic, Marshal) + +data DSLProgram = DSLProgram + +instance Program DSLProgram where + type ProgramFacts DSLProgram = + [ Point + , IntFact + , FloatFact + , UnsignedFact + , TextFact + , BTreeFact + , BrieFact + , EqRelFact + , Triple + , Vertex + , Edge + , Reachable + ] + programName = const "dslprogram" + +instance Fact Point where + type FactDirection Point = 'Input + factName = const "point" +instance Fact IntFact where + type FactDirection IntFact = 'Input + factName = const "intfact" +instance Fact FloatFact where + type FactDirection FloatFact = 'Input + factName = const "floatfact" +instance Fact UnsignedFact where + type FactDirection UnsignedFact = 'Input + factName = const "unsignedfact" +instance Fact TextFact where + type FactDirection TextFact = 'InputOutput + factName = const "textfact" +instance Fact Triple where + type FactDirection Triple = 'Internal + factName = const "triple" +instance Fact Vertex where + type FactDirection Vertex = 'Output + factName = const "vertex" +instance Fact Edge where + type FactDirection Edge = 'Input + factName = const "edge" +instance Fact Reachable where + type FactDirection Reachable = 'Output + factName = const "reachable" +instance Fact BTreeFact where + type FactDirection BTreeFact = 'Internal + factName = const "btreefact" +instance Fact BrieFact where + type FactDirection BrieFact = 'Internal + factName = const "briefact" +instance Fact EqRelFact where + type FactDirection EqRelFact = 'Input + factName = const "eqrelfact" +instance FactMetadata BTreeFact where + factOpts = const $ Metadata BTree NoInline +instance FactMetadata BrieFact where + factOpts = const $ Metadata Brie Inline +instance FactMetadata EqRelFact where + factOpts = const $ Metadata EqRel NoInline + +spec :: Spec +spec = describe "Souffle DSL" $ parallel $ do + describe "code generation" $ parallel $ do + let prog ==> txt = + let rendered = T.strip $ render DSLProgram prog + expected = T.strip txt + in rendered `shouldBe` expected + + it "can render an empty program" $ + render DSLProgram (pure ()) `shouldBe` "" + + it "can render a program with an input type definition" $ do + let prog = do + Predicate _ <- predicateFor @Edge + pure () + prog ==> [text| + .decl edge(t1: symbol, t2: symbol) + .input edge + |] + + it "can render a program with an output type definition" $ do + let prog = do + Predicate _ <- predicateFor @Reachable + pure () + prog ==> [text| + .decl reachable(t1: symbol, t2: symbol) + .output reachable + |] + + it "can render a program with type declared both as in- and output" $ do + let prog = do + Predicate _ <- predicateFor @TextFact + pure () + prog ==> [text| + .decl textfact(t1: symbol, t2: symbol) + .input textfact + .output textfact + |] + + it "can render a program with type declared and only used internally" $ do + let prog = do + Predicate _ <- predicateFor @Triple + pure () + prog ==> [text| + .decl triple(t1: symbol, t2: number, t3: symbol) + |] + + it "renders type declaration based on type info" $ do + let prog = do + Predicate _ <- predicateFor @IntFact + Predicate _ <- predicateFor @UnsignedFact + Predicate _ <- predicateFor @FloatFact + Predicate _ <- predicateFor @Triple + Predicate _ <- predicateFor @BTreeFact + Predicate _ <- predicateFor @BrieFact + Predicate _ <- predicateFor @EqRelFact + pure () + prog ==> [text| + .decl intfact(t1: number) + .input intfact + .decl unsignedfact(t1: unsigned) + .input unsignedfact + .decl floatfact(t1: float) + .input floatfact + .decl triple(t1: symbol, t2: number, t3: symbol) + .decl btreefact(t1: number) btree + .decl briefact(t1: number) brie inline + .decl eqrelfact(t1: number, t2: number) eqrel + .input eqrelfact + |] + + it "uses record accessors as attribute names in type declaration if provided" $ do + let prog = do + Predicate _ <- predicateFor @Point + pure () + prog ==> [text| + .decl point(x: number, y: number) + .input point + |] + + it "can render facts" $ do + let prog = do + Predicate edge <- predicateFor @Edge + Predicate triple <- predicateFor @Triple + Predicate txt <- predicateFor @TextFact + Predicate unsigned <- predicateFor @UnsignedFact + Predicate float <- predicateFor @FloatFact + edge("a", "b") + triple("cde", 1000, "fgh") + txt("ijk", "lmn") + unsigned(42) + float(42.42) + float(0.01) + prog ==> [text| + .decl edge(t1: symbol, t2: symbol) + .input edge + .decl triple(t1: symbol, t2: number, t3: symbol) + .decl textfact(t1: symbol, t2: symbol) + .input textfact + .output textfact + .decl unsignedfact(t1: unsigned) + .input unsignedfact + .decl floatfact(t1: float) + .input floatfact + edge("a", "b"). + triple("cde", 1000, "fgh"). + textfact("ijk", "lmn"). + unsignedfact(42). + floatfact(42.42). + floatfact(0.01). + |] + + it "can render a relation with a single rule" $ do + let prog = do + Predicate edge <- predicateFor @Edge + Predicate reachable <- predicateFor @Reachable + a <- var "a" + b <- var "b" + reachable(a, b) |- edge(a, b) + prog ==> [text| + .decl edge(t1: symbol, t2: symbol) + .input edge + .decl reachable(t1: symbol, t2: symbol) + .output reachable + reachable(a, b) :- + edge(a, b). + |] + + it "can render a relation with multiple rules" $ do + let prog = do + Predicate edge <- predicateFor @Edge + Predicate reachable <- predicateFor @Reachable + a <- var "a" + b <- var "b" + reachable(a, b) |- do + edge(a, a) + edge(b, b) + edge(a, b) + prog ==> [text| + .decl edge(t1: symbol, t2: symbol) + .input edge + .decl reachable(t1: symbol, t2: symbol) + .output reachable + reachable(a, b) :- + edge(a, a), + edge(b, b), + edge(a, b). + |] + + it "can render a relation containing a wildcard" $ do + let prog = do + Predicate edge <- predicateFor @Edge + Predicate vertex <- predicateFor @Vertex + a <- var "a" + vertex(a) |- do + edge(a, __) + edge(__, a) + prog ==> [text| + .decl edge(t1: symbol, t2: symbol) + .input edge + .decl vertex(t1: symbol) + .output vertex + vertex(a) :- + edge(a, _), + edge(_, a). + |] + + it "can render a relation with a logical or in the rule block" $ do + let prog = do + Predicate edge <- predicateFor @Edge + Predicate reachable <- predicateFor @Reachable + a <- var "a" + b <- var "b" + reachable(a, b) |- do + let rules1 = do + edge(a, a) + edge(b, b) + rules2 = do + edge(a, b) + edge(b, a) + rules1 \/ rules2 + prog ==> [text| + .decl edge(t1: symbol, t2: symbol) + .input edge + .decl reachable(t1: symbol, t2: symbol) + .output reachable + reachable(a, b) :- + edge(a, a), + edge(b, b); + edge(a, b), + edge(b, a). + |] + + it "can render a relation with multiple clauses" $ do + let prog = do + Predicate edge <- predicateFor @Edge + Predicate reachable <- predicateFor @Reachable + a <- var "a" + b <- var "b" + c <- var "c" + reachable(a, b) |- edge(a, b) + reachable(a, b) |- do + edge(a, c) + reachable(c, b) + prog ==> [text| + .decl edge(t1: symbol, t2: symbol) + .input edge + .decl reachable(t1: symbol, t2: symbol) + .output reachable + reachable(a, b) :- + edge(a, b). + reachable(a, b) :- + edge(a, c), + reachable(c, b). + |] + + it "can render a mix of and- and or- clauses correctly" $ do + let prog = do + Predicate edge <- predicateFor @Edge + Predicate reachable <- predicateFor @Reachable + a <- var "a" + b <- var "b" + c <- var "c" + reachable(a, b) |- do + edge(a, c) \/ edge(a, b) + reachable(c, b) + prog ==> [text| + .decl edge(t1: symbol, t2: symbol) + .input edge + .decl reachable(t1: symbol, t2: symbol) + .output reachable + reachable(a, b) :- + (edge(a, c); + edge(a, b)), + reachable(c, b). + |] + + it "discards empty alternative blocks" $ do + let prog = do + Predicate edge <- predicateFor @Edge + Predicate reachable <- predicateFor @Reachable + a <- var "a" + b <- var "b" + c <- var "c" + reachable(a, b) |- do + pure () \/ edge(a, c) + reachable(c, b) + reachable(a, b) |- do + edge(a,c) \/ pure () + reachable(c, b) + reachable(a, b) |- do + pure () \/ do + edge(a, c) + reachable(c, b) + prog ==> [text| + .decl edge(t1: symbol, t2: symbol) + .input edge + .decl reachable(t1: symbol, t2: symbol) + .output reachable + reachable(a, b) :- + edge(a, c), + reachable(c, b). + reachable(a, b) :- + edge(a, c), + reachable(c, b). + reachable(a, b) :- + edge(a, c), + reachable(c, b). + |] + + it "discards rules with empty rule blocks completely" $ do + let prog = do + Predicate reachable <- predicateFor @Reachable + a <- var "a" + b <- var "b" + reachable(a, b) |- + pure () + reachable(a, b) |- do + pure () \/ pure () + pure () + prog ==> [text| + .decl reachable(t1: symbol, t2: symbol) + .output reachable + |] + + it "discards empty negations" $ do + let prog = do + Predicate reachable <- predicateFor @Reachable + a <- var "a" + b <- var "b" + reachable(a, b) |- do + not' $ pure () + prog ==> [text| + .decl reachable(t1: symbol, t2: symbol) + .output reachable + |] + + it "allows generically describing predicate relations" $ do + -- NOTE: type signature not required, but it results in more clear type errors + -- and can serve as documentation. + let transitive :: forall prog p1 p2 t. Structure p1 ~ Structure p2 + => Structure p1 ~ '[t, t] + => Predicate p1 -> Predicate p2 -> DSL prog 'Definition () + transitive (Predicate p1) (Predicate p2) = do + a <- var "a" + b <- var "b" + c <- var "c" + p1(a, b) |- p2(a, b) + p1(a, b) |- do + p2(a, c) + p1(c, b) + prog = do + edge <- predicateFor @Edge + reachable <- predicateFor @Reachable + transitive reachable edge + prog ==> [text| + .decl edge(t1: symbol, t2: symbol) + .input edge + .decl reachable(t1: symbol, t2: symbol) + .output reachable + reachable(a, b) :- + edge(a, b). + reachable(a, b) :- + edge(a, c), + reachable(c, b). + |] + + it "can render logical negation in rule block" $ do + let prog = do + Predicate edge <- predicateFor @Edge + Predicate triple <- predicateFor @Triple + a <- var "a" + b <- var "b" + c <- var "c" + triple(a, b, c) |- do + not' $ edge(a,c) + triple(a, b, c) |- do + not' $ do + edge(a,a) + edge(c,c) + triple(a, b, c) |- do + not' $ edge(a,a) \/ edge(c,c) + triple(a, b, c) |- do + not' $ not' $ edge(a,a) + prog ==> [text| + .decl edge(t1: symbol, t2: symbol) + .input edge + .decl triple(t1: symbol, t2: number, t3: symbol) + triple(a, b, c) :- + !edge(a, c). + triple(a, b, c) :- + !(edge(a, a), + edge(c, c)). + triple(a, b, c) :- + !(edge(a, a); + edge(c, c)). + triple(a, b, c) :- + !!edge(a, a). + |] + + it "generates unique var names to avoid name collisions" $ do + let prog = do + Predicate edge <- predicateFor @Edge + Predicate reachable <- predicateFor @Reachable + a <- var "a" + a' <- var "a" + reachable(a, a') |- edge(a, a') + prog ==> [text| + .decl edge(t1: symbol, t2: symbol) + .input edge + .decl reachable(t1: symbol, t2: symbol) + .output reachable + reachable(a, a_1) :- + edge(a, a_1). + |] + + describe "operators" $ parallel $ do + -- TODO: check for number, unsigned, float; check underscore is not allowed + describe "arithmetic" $ parallel $ do + it "supports +" $ do + let prog = do + Predicate int <- predicateFor @IntFact + Predicate unsigned <- predicateFor @UnsignedFact + Predicate float <- predicateFor @FloatFact + int(10 + 32) + int(10 + 80 + 10) + unsigned(10 + 32) + float(10.12 + 31.88) + prog ==> [text| + .decl intfact(t1: number) + .input intfact + .decl unsignedfact(t1: unsigned) + .input unsignedfact + .decl floatfact(t1: float) + .input floatfact + intfact(10 + 32). + intfact(10 + 80 + 10). + unsignedfact(10 + 32). + floatfact(10.12 + 31.88). + |] + + it "supports *" $ do + let prog = do + Predicate int <- predicateFor @IntFact + Predicate unsigned <- predicateFor @UnsignedFact + Predicate float <- predicateFor @FloatFact + int(10 * 32) + int(10 * 80 * 10) + unsigned(10 * 32) + float(10.12 * 31.88) + prog ==> [text| + .decl intfact(t1: number) + .input intfact + .decl unsignedfact(t1: unsigned) + .input unsignedfact + .decl floatfact(t1: float) + .input floatfact + intfact(10 * 32). + intfact(10 * 80 * 10). + unsignedfact(10 * 32). + floatfact(10.12 * 31.88). + |] + + it "supports binary -" $ do + let prog = do + Predicate int <- predicateFor @IntFact + Predicate unsigned <- predicateFor @UnsignedFact + Predicate float <- predicateFor @FloatFact + int(10 - 32) + int(10 - 80 - 10) + unsigned(10 - 32) + float(10.12 - 31.88) + prog ==> [text| + .decl intfact(t1: number) + .input intfact + .decl unsignedfact(t1: unsigned) + .input unsignedfact + .decl floatfact(t1: float) + .input floatfact + intfact(10 - 32). + intfact(10 - 80 - 10). + unsignedfact(10 - 32). + floatfact(10.12 - 31.88). + |] + + it "supports unary -" $ do + let prog = do + Predicate int <- predicateFor @IntFact + Predicate float <- predicateFor @FloatFact + int(-42) + int(-100) + float(-13.37) + prog ==> [text| + .decl intfact(t1: number) + .input intfact + .decl floatfact(t1: float) + .input floatfact + intfact(-42). + intfact(-100). + floatfact(-13.37). + |] + + it "supports /" $ do + let prog = do + Predicate float <- predicateFor @FloatFact + float(13.37 / 0.01) + prog ==> [text| + .decl floatfact(t1: float) + .input floatfact + floatfact(13.37 / 0.01). + |] + + it "supports ^" $ do + let prog = do + Predicate int <- predicateFor @IntFact + Predicate unsigned <- predicateFor @UnsignedFact + Predicate float <- predicateFor @FloatFact + int(10 .^ 32) + int(10 .^ 80 .^ 10) + unsigned(10 .^ 32) + float(42.42 .^ 2) + prog ==> [text| + .decl intfact(t1: number) + .input intfact + .decl unsignedfact(t1: unsigned) + .input unsignedfact + .decl floatfact(t1: float) + .input floatfact + intfact(10 ^ 32). + intfact(10 ^ 80 ^ 10). + unsignedfact(10 ^ 32). + floatfact(42.42 ^ 2.0). + |] + + it "supports %" $ do + let prog = do + Predicate int <- predicateFor @IntFact + Predicate unsigned <- predicateFor @UnsignedFact + int(10 .% 32) + int(10 .% 80 .% 10) + unsigned(10 .% 32) + prog ==> [text| + .decl intfact(t1: number) + .input intfact + .decl unsignedfact(t1: unsigned) + .input unsignedfact + intfact(10 % 32). + intfact(10 % 80 % 10). + unsignedfact(10 % 32). + |] + + describe "logical operators" $ parallel $ do + it "supports band" $ do + let prog = do + Predicate int <- predicateFor @IntFact + Predicate unsigned <- predicateFor @UnsignedFact + int(10 `band` 32) + int(10 `band` 80 `band` 10) + unsigned(10 `band` 32) + prog ==> [text| + .decl intfact(t1: number) + .input intfact + .decl unsignedfact(t1: unsigned) + .input unsignedfact + intfact(10 band 32). + intfact(10 band 80 band 10). + unsignedfact(10 band 32). + |] + + it "supports bor" $ do + let prog = do + Predicate int <- predicateFor @IntFact + Predicate unsigned <- predicateFor @UnsignedFact + int(10 `bor` 32) + int(10 `bor` 80 `bor` 10) + unsigned(10 `bor` 32) + prog ==> [text| + .decl intfact(t1: number) + .input intfact + .decl unsignedfact(t1: unsigned) + .input unsignedfact + intfact(10 bor 32). + intfact(10 bor 80 bor 10). + unsignedfact(10 bor 32). + |] + + it "supports bxor" $ do + let prog = do + Predicate int <- predicateFor @IntFact + Predicate unsigned <- predicateFor @UnsignedFact + int(10 `bxor` 32) + int(10 `bxor` 80 `bxor` 10) + unsigned(10 `bxor` 32) + prog ==> [text| + .decl intfact(t1: number) + .input intfact + .decl unsignedfact(t1: unsigned) + .input unsignedfact + intfact(10 bxor 32). + intfact(10 bxor 80 bxor 10). + unsignedfact(10 bxor 32). + |] + + it "supports land" $ do + let prog = do + Predicate int <- predicateFor @IntFact + Predicate unsigned <- predicateFor @UnsignedFact + int(10 `land` 32) + int(10 `land` 80 `land` 10) + unsigned(10 `land` 32) + prog ==> [text| + .decl intfact(t1: number) + .input intfact + .decl unsignedfact(t1: unsigned) + .input unsignedfact + intfact(10 land 32). + intfact(10 land 80 land 10). + unsignedfact(10 land 32). + |] + + it "supports lor" $ do + let prog = do + Predicate int <- predicateFor @IntFact + Predicate unsigned <- predicateFor @UnsignedFact + int(10 `lor` 32) + int(10 `lor` 80 `lor` 10) + unsigned(10 `lor` 32) + prog ==> [text| + .decl intfact(t1: number) + .input intfact + .decl unsignedfact(t1: unsigned) + .input unsignedfact + intfact(10 lor 32). + intfact(10 lor 80 lor 10). + unsignedfact(10 lor 32). + |] + + describe "comparisons and equality, inequality" $ parallel $ do + -- NOTE: the following generated programs are not correct + -- since vars are not grounded (but is done to keep tests succinct) + it "supports <" $ do + let prog = do + Predicate int <- predicateFor @IntFact + Predicate unsigned <- predicateFor @UnsignedFact + Predicate float <- predicateFor @FloatFact + a <- var "a" + b <- var "b" + c <- var "c" + int(a) |- a .< 10 + unsigned(b) |- b .< 10 + float(c) |- c .< 10.1 + prog ==> [text| + .decl intfact(t1: number) + .input intfact + .decl unsignedfact(t1: unsigned) + .input unsignedfact + .decl floatfact(t1: float) + .input floatfact + intfact(a) :- + a < 10. + unsignedfact(b) :- + b < 10. + floatfact(c) :- + c < 10.1. + |] + + it "supports <=" $ do + let prog = do + Predicate int <- predicateFor @IntFact + Predicate unsigned <- predicateFor @UnsignedFact + Predicate float <- predicateFor @FloatFact + a <- var "a" + b <- var "b" + c <- var "c" + int(a) |- a .<= 10 + unsigned(b) |- b .<= 10 + float(c) |- c .<= 10.1 + prog ==> [text| + .decl intfact(t1: number) + .input intfact + .decl unsignedfact(t1: unsigned) + .input unsignedfact + .decl floatfact(t1: float) + .input floatfact + intfact(a) :- + a <= 10. + unsignedfact(b) :- + b <= 10. + floatfact(c) :- + c <= 10.1. + |] + + it "supports >" $ do + let prog = do + Predicate int <- predicateFor @IntFact + Predicate unsigned <- predicateFor @UnsignedFact + Predicate float <- predicateFor @FloatFact + a <- var "a" + b <- var "b" + c <- var "c" + int(a) |- a .> 10 + unsigned(b) |- b .> 10 + float(c) |- c .> 10.1 + prog ==> [text| + .decl intfact(t1: number) + .input intfact + .decl unsignedfact(t1: unsigned) + .input unsignedfact + .decl floatfact(t1: float) + .input floatfact + intfact(a) :- + a > 10. + unsignedfact(b) :- + b > 10. + floatfact(c) :- + c > 10.1. + |] + + it "supports >=" $ do + let prog = do + Predicate int <- predicateFor @IntFact + Predicate unsigned <- predicateFor @UnsignedFact + Predicate float <- predicateFor @FloatFact + a <- var "a" + b <- var "b" + c <- var "c" + int(a) |- a .>= 10 + unsigned(b) |- b .>= 10 + float(c) |- c .>= 10.1 + prog ==> [text| + .decl intfact(t1: number) + .input intfact + .decl unsignedfact(t1: unsigned) + .input unsignedfact + .decl floatfact(t1: float) + .input floatfact + intfact(a) :- + a >= 10. + unsignedfact(b) :- + b >= 10. + floatfact(c) :- + c >= 10.1. + |] + + it "supports =" $ do + let prog = do + Predicate int <- predicateFor @IntFact + Predicate unsigned <- predicateFor @UnsignedFact + Predicate float <- predicateFor @FloatFact + Predicate vertex <- predicateFor @Vertex + a <- var "a" + b <- var "b" + c <- var "c" + d <- var "d" + int(a) |- a .= 10 + unsigned(b) |- b .= 10 + float(c) |- c .= 10.1 + vertex(d) |- d .= "abc" + prog ==> [text| + .decl intfact(t1: number) + .input intfact + .decl unsignedfact(t1: unsigned) + .input unsignedfact + .decl floatfact(t1: float) + .input floatfact + .decl vertex(t1: symbol) + .output vertex + intfact(a) :- + a = 10. + unsignedfact(b) :- + b = 10. + floatfact(c) :- + c = 10.1. + vertex(d) :- + d = "abc". + |] + + it "supports !=" $ do + let prog = do + Predicate int <- predicateFor @IntFact + Predicate unsigned <- predicateFor @UnsignedFact + Predicate float <- predicateFor @FloatFact + Predicate vertex <- predicateFor @Vertex + a <- var "a" + b <- var "b" + c <- var "c" + d <- var "d" + int(a) |- a .!= 10 + unsigned(b) |- b .!= 10 + float(c) |- c .!= 10.1 + vertex(d) |- d .!= "abc" + prog ==> [text| + .decl intfact(t1: number) + .input intfact + .decl unsignedfact(t1: unsigned) + .input unsignedfact + .decl floatfact(t1: float) + .input floatfact + .decl vertex(t1: symbol) + .output vertex + intfact(a) :- + a != 10. + unsignedfact(b) :- + b != 10. + floatfact(c) :- + c != 10.1. + vertex(d) :- + d != "abc". + |] + + describe "functors" $ parallel $ do + it "supports max" $ do + let prog = do + Predicate int <- predicateFor @IntFact + Predicate unsigned <- predicateFor @UnsignedFact + Predicate float <- predicateFor @FloatFact + int(max' 10 32) + int(max' (max' 10 80) 10) + unsigned(max' 10 32) + float(max' 42.42 2) + prog ==> [text| + .decl intfact(t1: number) + .input intfact + .decl unsignedfact(t1: unsigned) + .input unsignedfact + .decl floatfact(t1: float) + .input floatfact + intfact(max(10, 32)). + intfact(max(max(10, 80), 10)). + unsignedfact(max(10, 32)). + floatfact(max(42.42, 2.0)). + |] + + it "supports min" $ do + let prog = do + Predicate int <- predicateFor @IntFact + Predicate unsigned <- predicateFor @UnsignedFact + Predicate float <- predicateFor @FloatFact + int(min' 10 32) + int(min' (min' 10 80) 10) + unsigned(min' 10 32) + float(min' 42.42 2) + prog ==> [text| + .decl intfact(t1: number) + .input intfact + .decl unsignedfact(t1: unsigned) + .input unsignedfact + .decl floatfact(t1: float) + .input floatfact + intfact(min(10, 32)). + intfact(min(min(10, 80), 10)). + unsignedfact(min(10, 32)). + floatfact(min(42.42, 2.0)). + |] + + it "supports cat" $ do + let prog = do + Predicate vertex <- predicateFor @Vertex + vertex(cat "abc" "def") + vertex(cat "abc" $ cat "def" "ghi") + prog ==> [text| + .decl vertex(t1: symbol) + .output vertex + vertex(cat("abc", "def")). + vertex(cat("abc", cat("def", "ghi"))). + |] + + it "supports contains" $ do + let prog = do + Predicate vertex <- predicateFor @Vertex + Predicate int <- predicateFor @IntFact + a <- var "a" + b <- var "b" + int(0) |- do + vertex(a) + vertex(b) + contains a b + prog ==> [text| + .decl vertex(t1: symbol) + .output vertex + .decl intfact(t1: number) + .input intfact + intfact(0) :- + vertex(a), + vertex(b), + contains(a, b). + |] + + it "supports match" $ do + let prog = do + Predicate vertex <- predicateFor @Vertex + Predicate int <- predicateFor @IntFact + a <- var "a" + int(0) |- do + vertex(a) + match "*.a" a + prog ==> [text| + .decl vertex(t1: symbol) + .output vertex + .decl intfact(t1: number) + .input intfact + intfact(0) :- + vertex(a), + match("*.a", a). + |] + + it "supports ord" $ do + let prog = do + Predicate vertex <- predicateFor @Vertex + Predicate int <- predicateFor @IntFact + a <- var "a" + int(ord a) |- + vertex(a) + prog ==> [text| + .decl vertex(t1: symbol) + .output vertex + .decl intfact(t1: number) + .input intfact + intfact(ord(a)) :- + vertex(a). + |] + + it "supports strlen" $ do + let prog = do + Predicate vertex <- predicateFor @Vertex + Predicate int <- predicateFor @IntFact + a <- var "a" + int(strlen a) |- + vertex(a) + prog ==> [text| + .decl vertex(t1: symbol) + .output vertex + .decl intfact(t1: number) + .input intfact + intfact(strlen(a)) :- + vertex(a). + |] + + it "supports substr" $ do + let prog = do + Predicate vertex <- predicateFor @Vertex + a <- var "a" + vertex(a) |- + a .= substr "Hello" 1 3 + prog ==> [text| + .decl vertex(t1: symbol) + .output vertex + vertex(a) :- + a = substr("Hello", 1, 3). + |] + + + it "supports to_number" $ do + let prog = do + Predicate vertex <- predicateFor @Vertex + Predicate int <- predicateFor @IntFact + a <- var "a" + int(to_number a) |- + vertex(a) + prog ==> [text| + .decl vertex(t1: symbol) + .output vertex + .decl intfact(t1: number) + .input intfact + intfact(to_number(a)) :- + vertex(a). + |] + + it "supports to_string" $ do + let prog = do + Predicate vertex <- predicateFor @Vertex + Predicate int <- predicateFor @IntFact + a <- var "a" + vertex(to_string a) |- + int(a) + prog ==> [text| + .decl vertex(t1: symbol) + .output vertex + .decl intfact(t1: number) + .input intfact + vertex(to_string(a)) :- + intfact(a). + |] + + describe "running DSL code directly " $ parallel $ do + it "can run DSL with default config in interpreted mode" $ do + let ast = do + Predicate edge <- predicateFor @Edge + Predicate reachable <- predicateFor @Reachable + a <- var "a" + b <- var "b" + c <- var "c" + reachable(a, b) |- edge(a, b) + reachable(a, b) |- do + edge(a, c) + reachable(c, b) + action handle = do + let prog = fromJust handle + I.addFacts prog [Edge "a" "b", Edge "b" "c"] + I.run prog + I.getFacts prog + rs <- runSouffleInterpreted DSLProgram ast action + rs `shouldBe` [Reachable "a" "b", Reachable "a" "c", Reachable "b" "c"] + + it "can run DSL with modified config in interpreted mode" $ do + tmpDir <- getCanonicalTemporaryDirectory + souffleHsDir <- createTempDirectory tmpDir "souffle-haskell" + cfg <- I.defaultConfig + let config = cfg { I.cfgDatalogDir = souffleHsDir } + ast = do + Predicate edge <- predicateFor @Edge + Predicate reachable <- predicateFor @Reachable + a <- var "a" + b <- var "b" + c <- var "c" + reachable(a, b) |- edge(a, b) + reachable(a, b) |- do + edge(a, c) + reachable(c, b) + action handle = do + let prog = fromJust handle + I.addFacts prog [Edge "a" "b", Edge "b" "c"] + I.run prog + I.getFacts prog + rs <- runSouffleInterpretedWith config DSLProgram ast action + rs `shouldBe` [Reachable "a" "b", Reachable "a" "c", Reachable "b" "c"] + + it "can run DSL in compiled mode" $ do + rs <- C.runSouffle F.CompiledProgram $ \handle -> do + let prog = fromJust handle + C.addFacts prog [F.Edge "a" "b", F.Edge "b" "c"] + C.run prog + C.getFacts prog + rs `shouldBe` [F.Reachable "b" "c", F.Reachable "a" "c", F.Reachable "a" "b"] + diff --git a/tests/fixtures/path.cpp b/tests/fixtures/path.cpp new file mode 100644 --- /dev/null +++ b/tests/fixtures/path.cpp @@ -0,0 +1,508 @@ + +#include "souffle/CompiledSouffle.h" + +extern "C" { +} + +namespace souffle { +static const RamDomain RAM_BIT_SHIFT_MASK = RAM_DOMAIN_SIZE - 1; +struct t_btree_ii__0_1__11__10 { +using t_tuple = Tuple; +struct t_comparator_0{ + int operator()(const t_tuple& a, const t_tuple& b) const { + return (ramBitCast(a[0]) < ramBitCast(b[0])) ? -1 : (ramBitCast(a[0]) > ramBitCast(b[0])) ? 1 :((ramBitCast(a[1]) < ramBitCast(b[1])) ? -1 : (ramBitCast(a[1]) > ramBitCast(b[1])) ? 1 :(0)); + } +bool less(const t_tuple& a, const t_tuple& b) const { + return (ramBitCast(a[0]) < ramBitCast(b[0]))|| (ramBitCast(a[0]) == ramBitCast(b[0])) && ((ramBitCast(a[1]) < ramBitCast(b[1]))); + } +bool equal(const t_tuple& a, const t_tuple& b) const { +return (ramBitCast(a[0]) == ramBitCast(b[0]))&&(ramBitCast(a[1]) == ramBitCast(b[1])); + } +}; +using t_ind_0 = btree_set; +t_ind_0 ind_0; +using iterator = t_ind_0::iterator; +struct context { +t_ind_0::operation_hints hints_0_lower; +t_ind_0::operation_hints hints_0_upper; +}; +context createContext() { return context(); } +bool insert(const t_tuple& t) { +context h; +return insert(t, h); +} +bool insert(const t_tuple& t, context& h) { +if (ind_0.insert(t, h.hints_0_lower)) { +return true; +} else return false; +} +bool insert(const RamDomain* ramDomain) { +RamDomain data[2]; +std::copy(ramDomain, ramDomain + 2, data); +const t_tuple& tuple = reinterpret_cast(data); +context h; +return insert(tuple, h); +} +bool insert(RamDomain a0,RamDomain a1) { +RamDomain data[2] = {a0,a1}; +return insert(data); +} +bool contains(const t_tuple& t, context& h) const { +return ind_0.contains(t, h.hints_0_lower); +} +bool contains(const t_tuple& t) const { +context h; +return contains(t, h); +} +std::size_t size() const { +return ind_0.size(); +} +iterator find(const t_tuple& t, context& h) const { +return ind_0.find(t, h.hints_0_lower); +} +iterator find(const t_tuple& t) const { +context h; +return find(t, h); +} +range lowerUpperRange_00(const t_tuple& /* lower */, const t_tuple& /* upper */, context& /* h */) const { +return range(ind_0.begin(),ind_0.end()); +} +range lowerUpperRange_00(const t_tuple& /* lower */, const t_tuple& /* upper */) const { +return range(ind_0.begin(),ind_0.end()); +} +range lowerUpperRange_11(const t_tuple& lower, const t_tuple& upper, context& h) const { +t_comparator_0 comparator; +int cmp = comparator(lower, upper); +if (cmp == 0) { + auto pos = ind_0.find(lower, h.hints_0_lower); + auto fin = ind_0.end(); + if (pos != fin) {fin = pos; ++fin;} + return make_range(pos, fin); +} +if (cmp > 0) { + return make_range(ind_0.end(), ind_0.end()); +} +return make_range(ind_0.lower_bound(lower, h.hints_0_lower), ind_0.upper_bound(upper, h.hints_0_upper)); +} +range lowerUpperRange_11(const t_tuple& lower, const t_tuple& upper) const { +context h; +return lowerUpperRange_11(lower,upper,h); +} +range lowerUpperRange_10(const t_tuple& lower, const t_tuple& upper, context& h) const { +t_comparator_0 comparator; +int cmp = comparator(lower, upper); +if (cmp > 0) { + return make_range(ind_0.end(), ind_0.end()); +} +return make_range(ind_0.lower_bound(lower, h.hints_0_lower), ind_0.upper_bound(upper, h.hints_0_upper)); +} +range lowerUpperRange_10(const t_tuple& lower, const t_tuple& upper) const { +context h; +return lowerUpperRange_10(lower,upper,h); +} +bool empty() const { +return ind_0.empty(); +} +std::vector> partition() const { +return ind_0.getChunks(400); +} +void purge() { +ind_0.clear(); +} +iterator begin() const { +return ind_0.begin(); +} +iterator end() const { +return ind_0.end(); +} +void printStatistics(std::ostream& o) const { +o << " arity 2 direct b-tree index 0 lex-order [0,1]\n"; +ind_0.printStats(o); +} +}; +struct t_btree_ii__0_1__11 { +using t_tuple = Tuple; +struct t_comparator_0{ + int operator()(const t_tuple& a, const t_tuple& b) const { + return (ramBitCast(a[0]) < ramBitCast(b[0])) ? -1 : (ramBitCast(a[0]) > ramBitCast(b[0])) ? 1 :((ramBitCast(a[1]) < ramBitCast(b[1])) ? -1 : (ramBitCast(a[1]) > ramBitCast(b[1])) ? 1 :(0)); + } +bool less(const t_tuple& a, const t_tuple& b) const { + return (ramBitCast(a[0]) < ramBitCast(b[0]))|| (ramBitCast(a[0]) == ramBitCast(b[0])) && ((ramBitCast(a[1]) < ramBitCast(b[1]))); + } +bool equal(const t_tuple& a, const t_tuple& b) const { +return (ramBitCast(a[0]) == ramBitCast(b[0]))&&(ramBitCast(a[1]) == ramBitCast(b[1])); + } +}; +using t_ind_0 = btree_set; +t_ind_0 ind_0; +using iterator = t_ind_0::iterator; +struct context { +t_ind_0::operation_hints hints_0_lower; +t_ind_0::operation_hints hints_0_upper; +}; +context createContext() { return context(); } +bool insert(const t_tuple& t) { +context h; +return insert(t, h); +} +bool insert(const t_tuple& t, context& h) { +if (ind_0.insert(t, h.hints_0_lower)) { +return true; +} else return false; +} +bool insert(const RamDomain* ramDomain) { +RamDomain data[2]; +std::copy(ramDomain, ramDomain + 2, data); +const t_tuple& tuple = reinterpret_cast(data); +context h; +return insert(tuple, h); +} +bool insert(RamDomain a0,RamDomain a1) { +RamDomain data[2] = {a0,a1}; +return insert(data); +} +bool contains(const t_tuple& t, context& h) const { +return ind_0.contains(t, h.hints_0_lower); +} +bool contains(const t_tuple& t) const { +context h; +return contains(t, h); +} +std::size_t size() const { +return ind_0.size(); +} +iterator find(const t_tuple& t, context& h) const { +return ind_0.find(t, h.hints_0_lower); +} +iterator find(const t_tuple& t) const { +context h; +return find(t, h); +} +range lowerUpperRange_00(const t_tuple& /* lower */, const t_tuple& /* upper */, context& /* h */) const { +return range(ind_0.begin(),ind_0.end()); +} +range lowerUpperRange_00(const t_tuple& /* lower */, const t_tuple& /* upper */) const { +return range(ind_0.begin(),ind_0.end()); +} +range lowerUpperRange_11(const t_tuple& lower, const t_tuple& upper, context& h) const { +t_comparator_0 comparator; +int cmp = comparator(lower, upper); +if (cmp == 0) { + auto pos = ind_0.find(lower, h.hints_0_lower); + auto fin = ind_0.end(); + if (pos != fin) {fin = pos; ++fin;} + return make_range(pos, fin); +} +if (cmp > 0) { + return make_range(ind_0.end(), ind_0.end()); +} +return make_range(ind_0.lower_bound(lower, h.hints_0_lower), ind_0.upper_bound(upper, h.hints_0_upper)); +} +range lowerUpperRange_11(const t_tuple& lower, const t_tuple& upper) const { +context h; +return lowerUpperRange_11(lower,upper,h); +} +bool empty() const { +return ind_0.empty(); +} +std::vector> partition() const { +return ind_0.getChunks(400); +} +void purge() { +ind_0.clear(); +} +iterator begin() const { +return ind_0.begin(); +} +iterator end() const { +return ind_0.end(); +} +void printStatistics(std::ostream& o) const { +o << " arity 2 direct b-tree index 0 lex-order [0,1]\n"; +ind_0.printStats(o); +} +}; + +class Sf_path : public SouffleProgram { +private: +static inline bool regex_wrapper(const std::string& pattern, const std::string& text) { + bool result = false; + try { result = std::regex_match(text, std::regex(pattern)); } catch(...) { + std::cerr << "warning: wrong pattern provided for match(\"" << pattern << "\",\"" << text << "\").\n"; +} + return result; +} +private: +static inline std::string substr_wrapper(const std::string& str, size_t idx, size_t len) { + std::string result; + try { result = str.substr(idx,len); } catch(...) { + std::cerr << "warning: wrong index position provided by substr(\""; + std::cerr << str << "\"," << (int32_t)idx << "," << (int32_t)len << ") functor.\n"; + } return result; +} +public: +// -- initialize symbol table -- +SymbolTable symTable{ + R"_(a)_", + R"_(b)_", + R"_(c)_", +};// -- initialize record table -- +RecordTable recordTable; +// -- Table: @delta_reachable +Own rel_1_delta_reachable = mk(); +// -- Table: @new_reachable +Own rel_2_new_reachable = mk(); +// -- Table: edge +Own rel_3_edge = mk(); +souffle::RelationWrapper<0,t_btree_ii__0_1__11,Tuple,2,0> wrapper_rel_3_edge; +// -- Table: reachable +Own rel_4_reachable = mk(); +souffle::RelationWrapper<1,t_btree_ii__0_1__11,Tuple,2,0> wrapper_rel_4_reachable; +public: +Sf_path() : +wrapper_rel_3_edge(*rel_3_edge,symTable,"edge",std::array{{"s:symbol","s:symbol"}},std::array{{"n","m"}}), + +wrapper_rel_4_reachable(*rel_4_reachable,symTable,"reachable",std::array{{"s:symbol","s:symbol"}},std::array{{"n","m"}}){ +addRelation("edge",&wrapper_rel_3_edge,true,true); +addRelation("reachable",&wrapper_rel_4_reachable,false,true); +} +~Sf_path() { +} +private: +std::string inputDirectory; +std::string outputDirectory; +bool performIO; +std::atomic ctr{}; + +std::atomic iter{}; +void runFunction(std::string inputDirectoryArg = "", std::string outputDirectoryArg = "", bool performIOArg = false) { +this->inputDirectory = inputDirectoryArg; +this->outputDirectory = outputDirectoryArg; +this->performIO = performIOArg; +SignalHandler::instance()->set(); +#if defined(_OPENMP) +if (getNumThreads() > 0) {omp_set_num_threads(getNumThreads());} +#endif + +// -- query evaluation -- +{ + std::vector args, ret; +subroutine_0(args, ret); +} +{ + std::vector args, ret; +subroutine_1(args, ret); +} + +// -- relation hint statistics -- +SignalHandler::instance()->reset(); +} +public: +void run() override { runFunction("", "", false); } +public: +void runAll(std::string inputDirectoryArg = "", std::string outputDirectoryArg = "") override { runFunction(inputDirectoryArg, outputDirectoryArg, true); +} +public: +void printAll(std::string outputDirectoryArg = "") override { +try {std::map directiveMap({{"IO","file"},{"attributeNames","n\tm"},{"name","edge"},{"operation","output"},{"output-dir","."},{"params","{\"records\": {}, \"relation\": {\"arity\": 2, \"auxArity\": 0, \"params\": [\"n\", \"m\"]}}"},{"types","{\"ADTs\": {}, \"records\": {}, \"relation\": {\"arity\": 2, \"auxArity\": 0, \"types\": [\"s:symbol\", \"s:symbol\"]}}"}}); +if (!outputDirectoryArg.empty()) {directiveMap["output-dir"] = outputDirectoryArg;} +IOSystem::getInstance().getWriter(directiveMap, symTable, recordTable)->writeAll(*rel_3_edge); +} catch (std::exception& e) {std::cerr << e.what();exit(1);} +try {std::map directiveMap({{"IO","file"},{"attributeNames","n\tm"},{"name","reachable"},{"operation","output"},{"output-dir","."},{"params","{\"records\": {}, \"relation\": {\"arity\": 2, \"auxArity\": 0, \"params\": [\"n\", \"m\"]}}"},{"types","{\"ADTs\": {}, \"records\": {}, \"relation\": {\"arity\": 2, \"auxArity\": 0, \"types\": [\"s:symbol\", \"s:symbol\"]}}"}}); +if (!outputDirectoryArg.empty()) {directiveMap["output-dir"] = outputDirectoryArg;} +IOSystem::getInstance().getWriter(directiveMap, symTable, recordTable)->writeAll(*rel_4_reachable); +} catch (std::exception& e) {std::cerr << e.what();exit(1);} +} +public: +void loadAll(std::string inputDirectoryArg = "") override { +try {std::map directiveMap({{"IO","file"},{"attributeNames","n\tm"},{"fact-dir","."},{"name","edge"},{"operation","input"},{"params","{\"records\": {}, \"relation\": {\"arity\": 2, \"auxArity\": 0, \"params\": [\"n\", \"m\"]}}"},{"types","{\"ADTs\": {}, \"records\": {}, \"relation\": {\"arity\": 2, \"auxArity\": 0, \"types\": [\"s:symbol\", \"s:symbol\"]}}"}}); +if (!inputDirectoryArg.empty()) {directiveMap["fact-dir"] = inputDirectoryArg;} +IOSystem::getInstance().getReader(directiveMap, symTable, recordTable)->readAll(*rel_3_edge); +} catch (std::exception& e) {std::cerr << "Error loading data: " << e.what() << '\n';} +} +public: +void dumpInputs() override { +try {std::map rwOperation; +rwOperation["IO"] = "stdout"; +rwOperation["name"] = "edge"; +rwOperation["types"] = "{\"relation\": {\"arity\": 2, \"auxArity\": 0, \"types\": [\"s:symbol\", \"s:symbol\"]}}"; +IOSystem::getInstance().getWriter(rwOperation, symTable, recordTable)->writeAll(*rel_3_edge); +} catch (std::exception& e) {std::cerr << e.what();exit(1);} +} +public: +void dumpOutputs() override { +try {std::map rwOperation; +rwOperation["IO"] = "stdout"; +rwOperation["name"] = "edge"; +rwOperation["types"] = "{\"relation\": {\"arity\": 2, \"auxArity\": 0, \"types\": [\"s:symbol\", \"s:symbol\"]}}"; +IOSystem::getInstance().getWriter(rwOperation, symTable, recordTable)->writeAll(*rel_3_edge); +} catch (std::exception& e) {std::cerr << e.what();exit(1);} +try {std::map rwOperation; +rwOperation["IO"] = "stdout"; +rwOperation["name"] = "reachable"; +rwOperation["types"] = "{\"relation\": {\"arity\": 2, \"auxArity\": 0, \"types\": [\"s:symbol\", \"s:symbol\"]}}"; +IOSystem::getInstance().getWriter(rwOperation, symTable, recordTable)->writeAll(*rel_4_reachable); +} catch (std::exception& e) {std::cerr << e.what();exit(1);} +} +public: +SymbolTable& getSymbolTable() override { +return symTable; +} +void executeSubroutine(std::string name, const std::vector& args, std::vector& ret) override { +if (name == "stratum_0") { +subroutine_0(args, ret); +return;} +if (name == "stratum_1") { +subroutine_1(args, ret); +return;} +fatal("unknown subroutine"); +} +#ifdef _MSC_VER +#pragma warning(disable: 4100) +#endif // _MSC_VER +void subroutine_0(const std::vector& args, std::vector& ret) { +if (performIO) { +try {std::map directiveMap({{"IO","file"},{"attributeNames","n\tm"},{"fact-dir","."},{"name","edge"},{"operation","input"},{"params","{\"records\": {}, \"relation\": {\"arity\": 2, \"auxArity\": 0, \"params\": [\"n\", \"m\"]}}"},{"types","{\"ADTs\": {}, \"records\": {}, \"relation\": {\"arity\": 2, \"auxArity\": 0, \"types\": [\"s:symbol\", \"s:symbol\"]}}"}}); +if (!inputDirectory.empty()) {directiveMap["fact-dir"] = inputDirectory;} +IOSystem::getInstance().getReader(directiveMap, symTable, recordTable)->readAll(*rel_3_edge); +} catch (std::exception& e) {std::cerr << "Error loading data: " << e.what() << '\n';} +} +SignalHandler::instance()->setMsg(R"_(edge("a","b"). +in file /Users/luc/personal/souffle-hs/tests/fixtures/path.dl [11:1-11:16])_"); +[&](){ +CREATE_OP_CONTEXT(rel_3_edge_op_ctxt,rel_3_edge->createContext()); +Tuple tuple{{ramBitCast(RamSigned(0)),ramBitCast(RamSigned(1))}}; +rel_3_edge->insert(tuple,READ_OP_CONTEXT(rel_3_edge_op_ctxt)); +} +();SignalHandler::instance()->setMsg(R"_(edge("b","c"). +in file /Users/luc/personal/souffle-hs/tests/fixtures/path.dl [12:1-12:16])_"); +[&](){ +CREATE_OP_CONTEXT(rel_3_edge_op_ctxt,rel_3_edge->createContext()); +Tuple tuple{{ramBitCast(RamSigned(1)),ramBitCast(RamSigned(2))}}; +rel_3_edge->insert(tuple,READ_OP_CONTEXT(rel_3_edge_op_ctxt)); +} +();if (performIO) { +try {std::map directiveMap({{"IO","file"},{"attributeNames","n\tm"},{"name","edge"},{"operation","output"},{"output-dir","."},{"params","{\"records\": {}, \"relation\": {\"arity\": 2, \"auxArity\": 0, \"params\": [\"n\", \"m\"]}}"},{"types","{\"ADTs\": {}, \"records\": {}, \"relation\": {\"arity\": 2, \"auxArity\": 0, \"types\": [\"s:symbol\", \"s:symbol\"]}}"}}); +if (!outputDirectory.empty()) {directiveMap["output-dir"] = outputDirectory;} +IOSystem::getInstance().getWriter(directiveMap, symTable, recordTable)->writeAll(*rel_3_edge); +} catch (std::exception& e) {std::cerr << e.what();exit(1);} +} +} +#ifdef _MSC_VER +#pragma warning(default: 4100) +#endif // _MSC_VER +#ifdef _MSC_VER +#pragma warning(disable: 4100) +#endif // _MSC_VER +void subroutine_1(const std::vector& args, std::vector& ret) { +SignalHandler::instance()->setMsg(R"_(reachable(x,y) :- + edge(x,y). +in file /Users/luc/personal/souffle-hs/tests/fixtures/path.dl [14:1-14:31])_"); +if(!(rel_3_edge->empty())) { +[&](){ +CREATE_OP_CONTEXT(rel_3_edge_op_ctxt,rel_3_edge->createContext()); +CREATE_OP_CONTEXT(rel_4_reachable_op_ctxt,rel_4_reachable->createContext()); +for(const auto& env0 : *rel_3_edge) { +Tuple tuple{{ramBitCast(env0[0]),ramBitCast(env0[1])}}; +rel_4_reachable->insert(tuple,READ_OP_CONTEXT(rel_4_reachable_op_ctxt)); +} +} +();} +[&](){ +CREATE_OP_CONTEXT(rel_4_reachable_op_ctxt,rel_4_reachable->createContext()); +CREATE_OP_CONTEXT(rel_1_delta_reachable_op_ctxt,rel_1_delta_reachable->createContext()); +for(const auto& env0 : *rel_4_reachable) { +Tuple tuple{{ramBitCast(env0[0]),ramBitCast(env0[1])}}; +rel_1_delta_reachable->insert(tuple,READ_OP_CONTEXT(rel_1_delta_reachable_op_ctxt)); +} +} +();iter = 0; +for(;;) { +SignalHandler::instance()->setMsg(R"_(reachable(x,z) :- + edge(x,y), + reachable(y,z). +in file /Users/luc/personal/souffle-hs/tests/fixtures/path.dl [15:1-15:48])_"); +if(!(rel_3_edge->empty()) && !(rel_1_delta_reachable->empty())) { +[&](){ +CREATE_OP_CONTEXT(rel_3_edge_op_ctxt,rel_3_edge->createContext()); +CREATE_OP_CONTEXT(rel_4_reachable_op_ctxt,rel_4_reachable->createContext()); +CREATE_OP_CONTEXT(rel_1_delta_reachable_op_ctxt,rel_1_delta_reachable->createContext()); +CREATE_OP_CONTEXT(rel_2_new_reachable_op_ctxt,rel_2_new_reachable->createContext()); +for(const auto& env0 : *rel_3_edge) { +auto range = rel_1_delta_reachable->lowerUpperRange_10(Tuple{{ramBitCast(env0[1]), ramBitCast(MIN_RAM_SIGNED)}},Tuple{{ramBitCast(env0[1]), ramBitCast(MAX_RAM_SIGNED)}},READ_OP_CONTEXT(rel_1_delta_reachable_op_ctxt)); +for(const auto& env1 : range) { +if( !(rel_4_reachable->contains(Tuple{{ramBitCast(env0[0]),ramBitCast(env1[1])}},READ_OP_CONTEXT(rel_4_reachable_op_ctxt)))) { +Tuple tuple{{ramBitCast(env0[0]),ramBitCast(env1[1])}}; +rel_2_new_reachable->insert(tuple,READ_OP_CONTEXT(rel_2_new_reachable_op_ctxt)); +} +} +} +} +();} +if(rel_2_new_reachable->empty()) break; +[&](){ +CREATE_OP_CONTEXT(rel_4_reachable_op_ctxt,rel_4_reachable->createContext()); +CREATE_OP_CONTEXT(rel_2_new_reachable_op_ctxt,rel_2_new_reachable->createContext()); +for(const auto& env0 : *rel_2_new_reachable) { +Tuple tuple{{ramBitCast(env0[0]),ramBitCast(env0[1])}}; +rel_4_reachable->insert(tuple,READ_OP_CONTEXT(rel_4_reachable_op_ctxt)); +} +} +();std::swap(rel_1_delta_reachable, rel_2_new_reachable); +rel_2_new_reachable->purge(); +iter++; +} +iter = 0; +rel_1_delta_reachable->purge(); +rel_2_new_reachable->purge(); +if (performIO) { +try {std::map directiveMap({{"IO","file"},{"attributeNames","n\tm"},{"name","reachable"},{"operation","output"},{"output-dir","."},{"params","{\"records\": {}, \"relation\": {\"arity\": 2, \"auxArity\": 0, \"params\": [\"n\", \"m\"]}}"},{"types","{\"ADTs\": {}, \"records\": {}, \"relation\": {\"arity\": 2, \"auxArity\": 0, \"types\": [\"s:symbol\", \"s:symbol\"]}}"}}); +if (!outputDirectory.empty()) {directiveMap["output-dir"] = outputDirectory;} +IOSystem::getInstance().getWriter(directiveMap, symTable, recordTable)->writeAll(*rel_4_reachable); +} catch (std::exception& e) {std::cerr << e.what();exit(1);} +} +if (performIO) rel_4_reachable->purge(); +if (performIO) rel_3_edge->purge(); +} +#ifdef _MSC_VER +#pragma warning(default: 4100) +#endif // _MSC_VER +}; +SouffleProgram *newInstance_path(){return new Sf_path;} +SymbolTable *getST_path(SouffleProgram *p){return &reinterpret_cast(p)->symTable;} + +#ifdef __EMBEDDED_SOUFFLE__ +class factory_Sf_path: public souffle::ProgramFactory { +SouffleProgram *newInstance() { +return new Sf_path(); +}; +public: +factory_Sf_path() : ProgramFactory("path"){} +}; +extern "C" { +factory_Sf_path __factory_Sf_path_instance; +} +} +#else +} +int main(int argc, char** argv) +{ +try{ +souffle::CmdOptions opt(R"(path.dl)", +R"()", +R"()", +false, +R"()", +1); +if (!opt.parse(argc,argv)) return 1; +souffle::Sf_path obj; +#if defined(_OPENMP) +obj.setNumThreads(opt.getNumJobs()); + +#endif +obj.runAll(opt.getInputFileDir(), opt.getOutputFileDir()); +return 0; +} catch(std::exception &e) { souffle::SignalHandler::instance()->error(e.what());} +} + +#endif diff --git a/tests/test.hs b/tests/test.hs new file mode 100644 --- /dev/null +++ b/tests/test.hs @@ -0,0 +1,2 @@ +{-# OPTIONS_GHC -Wno-missing-export-lists #-} +{-# OPTIONS_GHC -F -pgmF hspec-discover #-}