Safe Haskell | None |
---|---|
Language | Haskell2010 |
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 tests.
Synopsis
- newtype Predicate a = Predicate (forall f ctx. Fragment f ctx => Tuple ctx (Structure a) -> f ctx ())
- class Fragment f ctx
- type Tuple ctx ts = TupleOf (MapType (Term ctx) ts)
- data DSL prog ctx a
- data Head ctx unused
- data Body ctx a
- data Term ctx ty
- type VarName = Text
- data UsageContext
- data Direction
- = Input
- | Output
- | InputOutput
- | Internal
- 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))
- class (Fact a, SimpleProduct a) => FactMetadata a where
- data Metadata a = Metadata (StructureOpt a) (InlineOpt (FactDirection a))
- data StructureOpt (a :: Type) where
- Automatic :: StructureOpt a
- BTree :: StructureOpt a
- Brie :: StructureOpt a
- EqRel :: (IsBinaryRelation a, Structure a ~ '[t, t]) => StructureOpt a
- data InlineOpt (d :: Direction) where
- predicateFor :: forall a prog. ToPredicate prog a => DSL prog Definition (Predicate a)
- var :: NoVarsInAtom ctx => VarName -> DSL prog ctx' (Term ctx ty)
- __ :: Term ctx ty
- underscore :: Term ctx ty
- (|-) :: Head Relation a -> Body Relation () -> DSL prog Definition ()
- (\/) :: Body ctx () -> Body ctx () -> Body ctx ()
- not' :: Body ctx a -> Body ctx ()
- (.<) :: Num ty => Term ctx ty -> Term ctx ty -> Body ctx ()
- (.<=) :: Num ty => Term ctx ty -> Term ctx ty -> Body ctx ()
- (.>) :: Num ty => Term ctx ty -> Term ctx ty -> Body ctx ()
- (.>=) :: Num ty => Term ctx ty -> Term ctx ty -> Body ctx ()
- (.=) :: Term ctx ty -> Term ctx ty -> Body ctx ()
- (.!=) :: Term ctx ty -> Term ctx ty -> Body ctx ()
- (.^) :: Num ty => Term ctx ty -> Term ctx ty -> Term ctx ty
- (.%) :: (Num ty, Integral ty) => Term ctx ty -> Term ctx ty -> Term ctx ty
- band :: (Num ty, Integral ty) => Term ctx ty -> Term ctx ty -> Term ctx ty
- bor :: (Num ty, Integral ty) => Term ctx ty -> Term ctx ty -> Term ctx ty
- bxor :: (Num ty, Integral ty) => Term ctx ty -> Term ctx ty -> Term ctx ty
- lor :: (Num ty, Integral ty) => Term ctx ty -> Term ctx ty -> Term ctx ty
- land :: (Num ty, Integral ty) => Term ctx ty -> Term ctx ty -> Term ctx ty
- max' :: Num ty => Term ctx ty -> Term ctx ty -> Term ctx ty
- min' :: Num ty => Term ctx ty -> Term ctx ty -> Term ctx ty
- cat :: ToString ty => Term ctx ty -> Term ctx ty -> Term ctx ty
- contains :: ToString ty => Term ctx ty -> Term ctx ty -> Body ctx ()
- match :: ToString ty => Term ctx ty -> Term ctx ty -> Body ctx ()
- ord :: ToString ty => Term ctx ty -> Term ctx Int32
- strlen :: ToString ty => Term ctx ty -> Term ctx Int32
- substr :: ToString ty => Term ctx ty -> Term ctx Int32 -> Term ctx Int32 -> Term ctx ty
- to_number :: ToString ty => Term ctx ty -> Term ctx Int32
- to_string :: ToString ty => Term ctx Int32 -> Term ctx ty
- runSouffleInterpretedWith :: (MonadIO m, Program prog) => Config -> prog -> DSL prog Definition () -> (Maybe (Handle prog) -> SouffleM a) -> m a
- runSouffleInterpreted :: (MonadIO m, Program prog) => prog -> DSL prog Definition () -> (Maybe (Handle prog) -> SouffleM a) -> m a
- embedProgram :: Program prog => prog -> DSL prog Definition () -> Q [Dec]
- render :: Program prog => prog -> DSL prog Definition () -> Text
- renderIO :: Program prog => prog -> FilePath -> DSL prog Definition () -> IO ()
- type family Structure a :: [Type] where ...
- type family NoVarsInAtom (ctx :: UsageContext) :: Constraint where ...
- class Num ty => SupportsArithmetic ty
DSL-related types and functions
Types
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 Github.
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.
toFragment
Instances
Fragment (Body :: UsageContext -> Type -> Type) Relation Source # | |
Defined in Language.Souffle.Experimental toFragment :: ToTerms ts => TypeInfo a ts -> Name -> Tuple Relation ts -> Body Relation () | |
Fragment (Head :: UsageContext -> Type -> Type) Relation Source # | |
Defined in Language.Souffle.Experimental toFragment :: ToTerms ts => TypeInfo a ts -> Name -> Tuple Relation ts -> Head Relation () | |
Fragment (DSL prog :: UsageContext -> Type -> Type) Definition Source # | |
Defined in Language.Souffle.Experimental toFragment :: ToTerms ts => TypeInfo a ts -> Name -> Tuple Definition ts -> DSL prog Definition () |
type Tuple ctx ts = TupleOf (MapType (Term ctx) ts) Source #
A type synonym for a tuple consisting of Datalog Term
s.
Only tuples containing up to 10 elements are currently supported.
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).
Instances
Fragment (DSL prog :: UsageContext -> Type -> Type) Definition Source # | |
Defined in Language.Souffle.Experimental toFragment :: ToTerms ts => TypeInfo a ts -> Name -> Tuple Definition ts -> DSL prog Definition () | |
Monad (DSL prog ctx) Source # | |
Functor (DSL prog ctx) Source # | |
Applicative (DSL prog ctx) Source # | |
Defined in Language.Souffle.Experimental |
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
andDSL
.
See also |-
.
Instances
Fragment (Head :: UsageContext -> Type -> Type) Relation Source # | |
Defined in Language.Souffle.Experimental toFragment :: ToTerms ts => TypeInfo a ts -> Name -> Tuple Relation ts -> Head Relation () |
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 |-
.
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
/ __
.)
Instances
Fractional (Term ctx Float) Source # | |
(SupportsArithmetic ty, Num ty) => Num (Term ctx ty) Source # | |
Defined in Language.Souffle.Experimental (+) :: Term ctx ty -> Term ctx ty -> Term ctx ty # (-) :: Term ctx ty -> Term ctx ty -> Term ctx ty # (*) :: Term ctx ty -> Term ctx ty -> Term ctx ty # negate :: Term ctx ty -> Term ctx ty # abs :: Term ctx ty -> Term ctx ty # signum :: Term ctx ty -> Term ctx ty # fromInteger :: Integer -> Term ctx ty # | |
IsString (Term ctx Text) Source # | |
Defined in Language.Souffle.Experimental fromString :: String -> Term ctx Text # | |
IsString (Term ctx Text) Source # | |
Defined in Language.Souffle.Experimental fromString :: String -> Term ctx Text # | |
IsString (Term ctx String) Source # | |
Defined in Language.Souffle.Experimental fromString :: String -> Term ctx String # |
data UsageContext Source #
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.
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). |
Instances
Fragment (Body :: UsageContext -> Type -> Type) Relation Source # | |
Defined in Language.Souffle.Experimental toFragment :: ToTerms ts => TypeInfo a ts -> Name -> Tuple Relation ts -> Body Relation () | |
Fragment (Head :: UsageContext -> Type -> Type) Relation Source # | |
Defined in Language.Souffle.Experimental toFragment :: ToTerms ts => TypeInfo a ts -> Name -> Tuple Relation ts -> Head Relation () | |
Fragment (DSL prog :: UsageContext -> Type -> Type) Definition Source # | |
Defined in Language.Souffle.Experimental toFragment :: ToTerms ts => TypeInfo a ts -> Name -> Tuple Definition ts -> DSL prog Definition () |
A datatype describing which operations a certain fact supports. The direction is from the datalog perspective, so that it aligns with ".decl" statements in Souffle.
Input | Fact can only be stored in Datalog (using |
Output | Fact can only be read from Datalog (using |
InputOutput | Fact supports both reading from / writing to Datalog. |
Internal | Supports neither reading from / writing to Datalog. This is used for facts that are only visible inside Datalog itself. |
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)) Source #
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.
class (Fact a, SimpleProduct a) => FactMetadata a where Source #
A typeclass for optionally configuring extra settings (for performance reasons).
Nothing
A data type that allows for finetuning of fact settings (for performance reasons).
Metadata (StructureOpt a) (InlineOpt (FactDirection a)) |
data StructureOpt (a :: Type) where Source #
Datatype describing the way a fact is stored inside Datalog. A different choice of storage type can lead to an improvement in performance (potentially).
Automatic :: StructureOpt a | 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. |
BTree :: StructureOpt a | Uses a direct btree structure. |
Brie :: StructureOpt a | Uses a brie structure. This can improve performance in some cases and is more memory efficient for particularly large relations. |
EqRel :: (IsBinaryRelation a, Structure a ~ '[t, t]) => 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. |
data InlineOpt (d :: Direction) where Source #
Datatype indicating if we should inline a fact or not.
Basic building blocks
predicateFor :: forall a prog. ToPredicate prog a => DSL prog Definition (Predicate a) Source #
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.
var :: NoVarsInAtom ctx => VarName -> DSL prog ctx' (Term ctx ty) Source #
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.
Term representing a wildcard ("_") in Datalog. Note that in the DSL this is with 2 underscores. (Single underscore is reserved for typed holes!)
underscore :: Term ctx ty Source #
Term representing a wildcard ("_") in Datalog.
(|-) :: Head Relation a -> Body Relation () -> DSL prog Definition () infixl 0 Source #
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.
(\/) :: Body ctx () -> Body ctx () -> Body ctx () Source #
Creates a fragment that is the logical disjunction (OR) of 2 sub-fragments. This corresponds with ";" in Datalog.
not' :: Body ctx a -> Body ctx () Source #
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.)
Souffle operators
(.<) :: Num ty => Term ctx ty -> Term ctx ty -> Body ctx () infix 1 Source #
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 () infix 1 Source #
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 () infix 1 Source #
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 () infix 1 Source #
Creates a greater than or equal constraint (a >= b), for use in the body of a relation.
(.=) :: Term ctx ty -> Term ctx ty -> Body ctx () infix 1 Source #
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 () infix 1 Source #
Creates a constraint that 2 terms should not be equal to each other (a != b), for use in the body of a relation.
(.^) :: Num ty => Term ctx ty -> Term ctx ty -> Term ctx ty Source #
Exponentiation operator ("^" in Datalog).
(.%) :: (Num ty, Integral ty) => Term ctx ty -> Term ctx ty -> Term ctx ty Source #
Remainder operator ("%" in Datalog).
band :: (Num ty, Integral ty) => Term ctx ty -> Term ctx ty -> Term ctx ty Source #
Binary AND operator.
bor :: (Num ty, Integral ty) => Term ctx ty -> Term ctx ty -> Term ctx ty Source #
Binary OR operator.
bxor :: (Num ty, Integral ty) => Term ctx ty -> Term ctx ty -> Term ctx ty Source #
Binary XOR operator.
lor :: (Num ty, Integral ty) => Term ctx ty -> Term ctx ty -> Term ctx ty Source #
Logical OR operator.
land :: (Num ty, Integral ty) => Term ctx ty -> Term ctx ty -> Term ctx ty Source #
Logical AND operator.
Souffle functions
cat :: ToString ty => Term ctx ty -> Term ctx ty -> Term ctx ty Source #
"cat" function (string concatenation).
contains :: ToString ty => Term ctx ty -> Term ctx ty -> Body ctx () Source #
"contains" predicate, checks if 2nd string contains the first.
match :: ToString ty => Term ctx ty -> Term ctx ty -> Body ctx () Source #
"match" predicate, checks if a wildcard string matches a given string.
substr :: ToString ty => Term ctx ty -> Term ctx Int32 -> Term ctx Int32 -> Term ctx ty Source #
"substr" function.
Functions for running a Datalog DSL fragment / AST directly.
runSouffleInterpretedWith :: (MonadIO m, Program prog) => Config -> prog -> DSL prog Definition () -> (Maybe (Handle prog) -> SouffleM a) -> m a Source #
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 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 runSouffleWith
for more
information on automatic cleanup.
runSouffleInterpreted :: (MonadIO m, Program prog) => prog -> DSL prog Definition () -> (Maybe (Handle prog) -> SouffleM a) -> m a Source #
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.
embedProgram :: Program prog => prog -> DSL prog Definition () -> Q [Dec] Source #
Rendering functions
render :: Program prog => prog -> DSL prog Definition () -> Text Source #
Renders a DSL fragment to the corresponding Datalog code.
renderIO :: Program prog => prog -> FilePath -> DSL prog Definition () -> IO () Source #
Renders a DSL fragment to the corresponding Datalog code and writes it to a file.
Helper type families useful in some situations
type family Structure a :: [Type] where ... Source #
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 NoVarsInAtom (ctx :: UsageContext) :: Constraint where ... Source #
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).
NoVarsInAtom ctx = Assert (ctx == Relation) NoVarsInAtomError |
class Num ty => SupportsArithmetic ty Source #
fromInteger'
Instances
SupportsArithmetic Float Source # | |
Defined in Language.Souffle.Experimental fromInteger' :: Integer -> Term ctx Float | |
SupportsArithmetic Int32 Source # | |
Defined in Language.Souffle.Experimental fromInteger' :: Integer -> Term ctx Int32 | |
SupportsArithmetic Word32 Source # | |
Defined in Language.Souffle.Experimental fromInteger' :: Integer -> Term ctx Word32 |