{-# 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 <https://github.com/luc-tielen/souffle-haskell/blob/2c24e1e169da269c45fc192ab5efd4ff2196114b/tests/Test/Language/Souffle/ExperimentalSpec.hs tests>.
-}
module Language.Souffle.Experimental
  ( -- * 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
--   <https://github.com/luc-tielen/souffle-haskell/issues Github>.
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 (a -> DSL prog ctx b -> DSL prog ctx a
(a -> b) -> DSL prog ctx a -> DSL prog ctx b
(forall a b. (a -> b) -> DSL prog ctx a -> DSL prog ctx b)
-> (forall a b. a -> DSL prog ctx b -> DSL prog ctx a)
-> Functor (DSL prog ctx)
forall k (prog :: k) k (ctx :: k) a b.
a -> DSL prog ctx b -> DSL prog ctx a
forall k (prog :: k) k (ctx :: k) a b.
(a -> b) -> DSL prog ctx a -> DSL prog ctx b
forall a b. a -> DSL prog ctx b -> DSL prog ctx a
forall a b. (a -> b) -> DSL prog ctx a -> DSL prog ctx b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> DSL prog ctx b -> DSL prog ctx a
$c<$ :: forall k (prog :: k) k (ctx :: k) a b.
a -> DSL prog ctx b -> DSL prog ctx a
fmap :: (a -> b) -> DSL prog ctx a -> DSL prog ctx b
$cfmap :: forall k (prog :: k) k (ctx :: k) a b.
(a -> b) -> DSL prog ctx a -> DSL prog ctx b
Functor, Functor (DSL prog ctx)
a -> DSL prog ctx a
Functor (DSL prog ctx) =>
(forall a. a -> DSL prog ctx a)
-> (forall a b.
    DSL prog ctx (a -> b) -> DSL prog ctx a -> DSL prog ctx b)
-> (forall a b c.
    (a -> b -> c)
    -> DSL prog ctx a -> DSL prog ctx b -> DSL prog ctx c)
-> (forall a b. DSL prog ctx a -> DSL prog ctx b -> DSL prog ctx b)
-> (forall a b. DSL prog ctx a -> DSL prog ctx b -> DSL prog ctx a)
-> Applicative (DSL prog ctx)
DSL prog ctx a -> DSL prog ctx b -> DSL prog ctx b
DSL prog ctx a -> DSL prog ctx b -> DSL prog ctx a
DSL prog ctx (a -> b) -> DSL prog ctx a -> DSL prog ctx b
(a -> b -> c) -> DSL prog ctx a -> DSL prog ctx b -> DSL prog ctx c
forall a. a -> DSL prog ctx a
forall k (prog :: k) k (ctx :: k). Functor (DSL prog ctx)
forall k (prog :: k) k (ctx :: k) a. a -> DSL prog ctx a
forall k (prog :: k) k (ctx :: k) a b.
DSL prog ctx a -> DSL prog ctx b -> DSL prog ctx a
forall k (prog :: k) k (ctx :: k) a b.
DSL prog ctx a -> DSL prog ctx b -> DSL prog ctx b
forall k (prog :: k) k (ctx :: k) a b.
DSL prog ctx (a -> b) -> DSL prog ctx a -> DSL prog ctx b
forall k (prog :: k) k (ctx :: k) a b c.
(a -> b -> c) -> DSL prog ctx a -> DSL prog ctx b -> DSL prog ctx c
forall a b. DSL prog ctx a -> DSL prog ctx b -> DSL prog ctx a
forall a b. DSL prog ctx a -> DSL prog ctx b -> DSL prog ctx b
forall a b.
DSL prog ctx (a -> b) -> DSL prog ctx a -> DSL prog ctx b
forall a b c.
(a -> b -> c) -> DSL prog ctx a -> DSL prog ctx b -> DSL prog ctx c
forall (f :: * -> *).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: DSL prog ctx a -> DSL prog ctx b -> DSL prog ctx a
$c<* :: forall k (prog :: k) k (ctx :: k) a b.
DSL prog ctx a -> DSL prog ctx b -> DSL prog ctx a
*> :: DSL prog ctx a -> DSL prog ctx b -> DSL prog ctx b
$c*> :: forall k (prog :: k) k (ctx :: k) a b.
DSL prog ctx a -> DSL prog ctx b -> DSL prog ctx b
liftA2 :: (a -> b -> c) -> DSL prog ctx a -> DSL prog ctx b -> DSL prog ctx c
$cliftA2 :: forall k (prog :: k) k (ctx :: k) a b c.
(a -> b -> c) -> DSL prog ctx a -> DSL prog ctx b -> DSL prog ctx c
<*> :: DSL prog ctx (a -> b) -> DSL prog ctx a -> DSL prog ctx b
$c<*> :: forall k (prog :: k) k (ctx :: k) a b.
DSL prog ctx (a -> b) -> DSL prog ctx a -> DSL prog ctx b
pure :: a -> DSL prog ctx a
$cpure :: forall k (prog :: k) k (ctx :: k) a. a -> DSL prog ctx a
$cp1Applicative :: forall k (prog :: k) k (ctx :: k). Functor (DSL prog ctx)
Applicative, Applicative (DSL prog ctx)
a -> DSL prog ctx a
Applicative (DSL prog ctx) =>
(forall a b.
 DSL prog ctx a -> (a -> DSL prog ctx b) -> DSL prog ctx b)
-> (forall a b. DSL prog ctx a -> DSL prog ctx b -> DSL prog ctx b)
-> (forall a. a -> DSL prog ctx a)
-> Monad (DSL prog ctx)
DSL prog ctx a -> (a -> DSL prog ctx b) -> DSL prog ctx b
DSL prog ctx a -> DSL prog ctx b -> DSL prog ctx b
forall a. a -> DSL prog ctx a
forall k (prog :: k) k (ctx :: k). Applicative (DSL prog ctx)
forall k (prog :: k) k (ctx :: k) a. a -> DSL prog ctx a
forall k (prog :: k) k (ctx :: k) a b.
DSL prog ctx a -> DSL prog ctx b -> DSL prog ctx b
forall k (prog :: k) k (ctx :: k) a b.
DSL prog ctx a -> (a -> DSL prog ctx b) -> DSL prog ctx b
forall a b. DSL prog ctx a -> DSL prog ctx b -> DSL prog ctx b
forall a b.
DSL prog ctx a -> (a -> DSL prog ctx b) -> DSL prog ctx b
forall (m :: * -> *).
Applicative m =>
(forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: a -> DSL prog ctx a
$creturn :: forall k (prog :: k) k (ctx :: k) a. a -> DSL prog ctx a
>> :: DSL prog ctx a -> DSL prog ctx b -> DSL prog ctx b
$c>> :: forall k (prog :: k) k (ctx :: k) a b.
DSL prog ctx a -> DSL prog ctx b -> DSL prog ctx b
>>= :: DSL prog ctx a -> (a -> DSL prog ctx b) -> DSL prog ctx b
$c>>= :: forall k (prog :: k) k (ctx :: k) a b.
DSL prog ctx a -> (a -> DSL prog ctx b) -> DSL prog ctx b
$cp1Monad :: forall k (prog :: k) k (ctx :: k). Applicative (DSL prog ctx)
Monad, MonadWriter [AST], MonadState VarMap)
  via (StateT VarMap (Writer [AST]))

addDefinition :: AST -> DSL prog 'Definition ()
addDefinition :: AST -> DSL prog 'Definition ()
addDefinition dl :: AST
dl = [AST] -> DSL prog 'Definition ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [AST
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 :: prog
-> DSL prog 'Definition ()
-> (Maybe (Handle prog) -> SouffleM a)
-> m a
runSouffleInterpreted program :: prog
program dsl :: DSL prog 'Definition ()
dsl f :: Maybe (Handle prog) -> SouffleM a
f = IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO a -> m a) -> IO a -> m a
forall a b. (a -> b) -> a -> b
$ do
  FilePath
tmpDir <- IO FilePath
getCanonicalTemporaryDirectory
  FilePath
souffleHsDir <- FilePath -> FilePath -> IO FilePath
createTempDirectory FilePath
tmpDir "souffle-haskell"
  Config
defaultCfg <- IO Config
forall (m :: * -> *). MonadIO m => m Config
I.defaultConfig
  let cfg :: Config
cfg = Config
defaultCfg { cfgDatalogDir :: FilePath
I.cfgDatalogDir = FilePath
souffleHsDir
                       , cfgFactDir :: Maybe FilePath
I.cfgFactDir = FilePath -> Maybe FilePath
forall a. a -> Maybe a
Just FilePath
souffleHsDir
                       , cfgOutputDir :: Maybe FilePath
I.cfgOutputDir = FilePath -> Maybe FilePath
forall a. a -> Maybe a
Just FilePath
souffleHsDir
                       }
  Config
-> prog
-> DSL prog 'Definition ()
-> (Maybe (Handle prog) -> SouffleM a)
-> IO a
forall (m :: * -> *) prog a.
(MonadIO m, Program prog) =>
Config
-> prog
-> DSL prog 'Definition ()
-> (Maybe (Handle prog) -> SouffleM a)
-> m a
runSouffleInterpretedWith Config
cfg prog
program DSL prog 'Definition ()
dsl Maybe (Handle prog) -> SouffleM a
f IO a -> IO () -> IO a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* FilePath -> IO ()
removeDirectoryRecursive FilePath
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
-> prog
-> DSL prog 'Definition ()
-> (Maybe (Handle prog) -> SouffleM a)
-> m a
runSouffleInterpretedWith config :: Config
config program :: prog
program dsl :: DSL prog 'Definition ()
dsl f :: Maybe (Handle prog) -> SouffleM a
f = IO a -> m a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO a -> m a) -> IO a -> m a
forall a b. (a -> b) -> a -> b
$ do
  let progName :: FilePath
progName = prog -> FilePath
forall a. Program a => a -> FilePath
programName prog
program
      datalogFile :: FilePath
datalogFile = Config -> FilePath
I.cfgDatalogDir Config
config FilePath -> FilePath -> FilePath
</> FilePath
progName FilePath -> FilePath -> FilePath
<.> "dl"
  prog -> FilePath -> DSL prog 'Definition () -> IO ()
forall prog.
Program prog =>
prog -> FilePath -> DSL prog 'Definition () -> IO ()
renderIO prog
program FilePath
datalogFile DSL prog 'Definition ()
dsl
  Config -> prog -> (Maybe (Handle prog) -> SouffleM a) -> IO a
forall prog a.
Program prog =>
Config -> prog -> (Maybe (Handle prog) -> SouffleM a) -> IO a
I.runSouffleWith Config
config prog
program Maybe (Handle prog) -> SouffleM a
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 :: prog -> DSL prog 'Definition () -> Q [Dec]
embedProgram program :: prog
program dsl :: DSL prog 'Definition ()
dsl = do
  FilePath
cppFile <- IO FilePath -> Q FilePath
forall (m :: * -> *) a. Quasi m => IO a -> m a
qRunIO (IO FilePath -> Q FilePath) -> IO FilePath -> Q FilePath
forall a b. (a -> b) -> a -> b
$ do
    FilePath
tmpDir <- IO FilePath
getCanonicalTemporaryDirectory
    FilePath
souffleHsDir <- FilePath -> FilePath -> IO FilePath
createTempDirectory FilePath
tmpDir "souffle-haskell"
    let progName :: FilePath
progName = prog -> FilePath
forall a. Program a => a -> FilePath
programName prog
program
        datalogFile :: FilePath
datalogFile = FilePath
souffleHsDir FilePath -> FilePath -> FilePath
</> FilePath
progName FilePath -> FilePath -> FilePath
<.> "dl"
        cppFile :: FilePath
cppFile = FilePath
souffleHsDir FilePath -> FilePath -> FilePath
</> FilePath
progName FilePath -> FilePath -> FilePath
<.> "cpp"
    prog -> FilePath -> DSL prog 'Definition () -> IO ()
forall prog.
Program prog =>
prog -> FilePath -> DSL prog 'Definition () -> IO ()
renderIO prog
program FilePath
datalogFile DSL prog 'Definition ()
dsl
    FilePath -> IO ()
callCommand (FilePath -> IO ()) -> FilePath -> IO ()
forall a b. (a -> b) -> a -> b
$ FilePath -> FilePath -> FilePath -> FilePath
forall r. PrintfType r => FilePath -> r
printf "souffle -g %s %s" FilePath
cppFile FilePath
datalogFile
    FilePath -> IO FilePath
forall (f :: * -> *) a. Applicative f => a -> f a
pure FilePath
cppFile
  ForeignSrcLang -> FilePath -> Q ()
forall (m :: * -> *). Quasi m => ForeignSrcLang -> FilePath -> m ()
qAddForeignFilePath ForeignSrcLang
LangCxx FilePath
cppFile
  [Dec] -> Q [Dec]
forall (f :: * -> *) a. Applicative f => a -> f a
pure []

runDSL :: Program prog => prog -> DSL prog 'Definition a -> DL
runDSL :: prog -> DSL prog 'Definition a -> DL
runDSL _ (DSL a :: StateT VarMap (Writer [AST]) a
a) = [DL] -> DL
Statements ([DL] -> DL) -> [DL] -> DL
forall a b. (a -> b) -> a -> b
$ (AST -> Maybe DL) -> [AST] -> [DL]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe AST -> Maybe DL
simplify ([AST] -> [DL]) -> [AST] -> [DL]
forall a b. (a -> b) -> a -> b
$ Writer [AST] a -> [AST]
forall w a. Writer w a -> w
execWriter (StateT VarMap (Writer [AST]) a -> VarMap -> Writer [AST] a
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT StateT VarMap (Writer [AST]) a
a VarMap
forall a. Monoid a => a
mempty) where
  simplify :: AST -> Maybe DL
simplify = \case
    Declare' name :: VarName
name dir :: Direction
dir fields :: [FieldData]
fields opts :: SimpleMetadata
opts -> DL -> Maybe DL
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DL -> Maybe DL) -> DL -> Maybe DL
forall a b. (a -> b) -> a -> b
$ VarName -> Direction -> [FieldData] -> SimpleMetadata -> DL
Declare VarName
name Direction
dir [FieldData]
fields SimpleMetadata
opts
    Rule' name :: VarName
name terms :: NonEmpty SimpleTerm
terms body :: AST
body -> VarName -> NonEmpty SimpleTerm -> DL -> DL
Rule VarName
name NonEmpty SimpleTerm
terms (DL -> DL) -> Maybe DL -> Maybe DL
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AST -> Maybe DL
simplify AST
body
    Atom' name :: VarName
name terms :: NonEmpty SimpleTerm
terms -> DL -> Maybe DL
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DL -> Maybe DL) -> DL -> Maybe DL
forall a b. (a -> b) -> a -> b
$ VarName -> NonEmpty SimpleTerm -> DL
Atom VarName
name NonEmpty SimpleTerm
terms
    And' exprs :: [AST]
exprs -> case (AST -> Maybe DL) -> [AST] -> [DL]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe AST -> Maybe DL
simplify [AST]
exprs of
      [] -> Maybe DL
forall a. Maybe a
Nothing
      exprs' :: [DL]
exprs' -> DL -> Maybe DL
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DL -> Maybe DL) -> DL -> Maybe DL
forall a b. (a -> b) -> a -> b
$ (DL -> DL -> DL) -> [DL] -> DL
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 DL -> DL -> DL
And [DL]
exprs'
    Or' exprs :: [AST]
exprs -> case (AST -> Maybe DL) -> [AST] -> [DL]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe AST -> Maybe DL
simplify [AST]
exprs of
      [] -> Maybe DL
forall a. Maybe a
Nothing
      exprs' :: [DL]
exprs' -> DL -> Maybe DL
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DL -> Maybe DL) -> DL -> Maybe DL
forall a b. (a -> b) -> a -> b
$ (DL -> DL -> DL) -> [DL] -> DL
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldl1 DL -> DL -> DL
Or [DL]
exprs'
    Not' expr :: AST
expr -> DL -> DL
Not (DL -> DL) -> Maybe DL -> Maybe DL
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> AST -> Maybe DL
simplify AST
expr
    Constrain' e :: SimpleTerm
e -> DL -> Maybe DL
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DL -> Maybe DL) -> DL -> Maybe DL
forall a b. (a -> b) -> a -> b
$ SimpleTerm -> DL
Constrain SimpleTerm
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 :: VarName -> DSL prog ctx' (Term ctx ty)
var name :: VarName
name = do
  Int
count <- Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe 0 (Maybe Int -> Int)
-> DSL prog ctx' (Maybe Int) -> DSL prog ctx' Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (VarMap -> Maybe Int) -> DSL prog ctx' (Maybe Int)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (VarName -> VarMap -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup VarName
name)
  (VarMap -> VarMap) -> DSL prog ctx' ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((VarMap -> VarMap) -> DSL prog ctx' ())
-> (VarMap -> VarMap) -> DSL prog ctx' ()
forall a b. (a -> b) -> a -> b
$ VarName -> Int -> VarMap -> VarMap
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert VarName
name (Int
count Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1)
  let varName :: VarName
varName = if Int
count Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 0 then VarName
name else VarName
name VarName -> VarName -> VarName
forall a. Semigroup a => a -> a -> a
<> "_" VarName -> VarName -> VarName
forall a. Semigroup a => a -> a -> a
<> FilePath -> VarName
T.pack (Int -> FilePath
forall a. Show a => a -> FilePath
show Int
count)
  Term ctx ty -> DSL prog ctx' (Term ctx ty)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Term ctx ty -> DSL prog ctx' (Term ctx ty))
-> Term ctx ty -> DSL prog ctx' (Term ctx ty)
forall a b. (a -> b) -> a -> b
$ VarName -> Term ctx ty
forall (ctx :: UsageContext) ty.
NoVarsInAtom ctx =>
VarName -> Term ctx ty
VarTerm VarName
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 (a -> Body ctx b -> Body ctx a
(a -> b) -> Body ctx a -> Body ctx b
(forall a b. (a -> b) -> Body ctx a -> Body ctx b)
-> (forall a b. a -> Body ctx b -> Body ctx a)
-> Functor (Body ctx)
forall k (ctx :: k) a b. a -> Body ctx b -> Body ctx a
forall k (ctx :: k) a b. (a -> b) -> Body ctx a -> Body ctx b
forall a b. a -> Body ctx b -> Body ctx a
forall a b. (a -> b) -> Body ctx a -> Body ctx b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Body ctx b -> Body ctx a
$c<$ :: forall k (ctx :: k) a b. a -> Body ctx b -> Body ctx a
fmap :: (a -> b) -> Body ctx a -> Body ctx b
$cfmap :: forall k (ctx :: k) a b. (a -> b) -> Body ctx a -> Body ctx b
Functor, Functor (Body ctx)
a -> Body ctx a
Functor (Body ctx) =>
(forall a. a -> Body ctx a)
-> (forall a b. Body ctx (a -> b) -> Body ctx a -> Body ctx b)
-> (forall a b c.
    (a -> b -> c) -> Body ctx a -> Body ctx b -> Body ctx c)
-> (forall a b. Body ctx a -> Body ctx b -> Body ctx b)
-> (forall a b. Body ctx a -> Body ctx b -> Body ctx a)
-> Applicative (Body ctx)
Body ctx a -> Body ctx b -> Body ctx b
Body ctx a -> Body ctx b -> Body ctx a
Body ctx (a -> b) -> Body ctx a -> Body ctx b
(a -> b -> c) -> Body ctx a -> Body ctx b -> Body ctx c
forall a. a -> Body ctx a
forall k (ctx :: k). Functor (Body ctx)
forall k (ctx :: k) a. a -> Body ctx a
forall k (ctx :: k) a b. Body ctx a -> Body ctx b -> Body ctx a
forall k (ctx :: k) a b. Body ctx a -> Body ctx b -> Body ctx b
forall k (ctx :: k) a b.
Body ctx (a -> b) -> Body ctx a -> Body ctx b
forall k (ctx :: k) a b c.
(a -> b -> c) -> Body ctx a -> Body ctx b -> Body ctx c
forall a b. Body ctx a -> Body ctx b -> Body ctx a
forall a b. Body ctx a -> Body ctx b -> Body ctx b
forall a b. Body ctx (a -> b) -> Body ctx a -> Body ctx b
forall a b c.
(a -> b -> c) -> Body ctx a -> Body ctx b -> Body ctx c
forall (f :: * -> *).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: Body ctx a -> Body ctx b -> Body ctx a
$c<* :: forall k (ctx :: k) a b. Body ctx a -> Body ctx b -> Body ctx a
*> :: Body ctx a -> Body ctx b -> Body ctx b
$c*> :: forall k (ctx :: k) a b. Body ctx a -> Body ctx b -> Body ctx b
liftA2 :: (a -> b -> c) -> Body ctx a -> Body ctx b -> Body ctx c
$cliftA2 :: forall k (ctx :: k) a b c.
(a -> b -> c) -> Body ctx a -> Body ctx b -> Body ctx c
<*> :: Body ctx (a -> b) -> Body ctx a -> Body ctx b
$c<*> :: forall k (ctx :: k) a b.
Body ctx (a -> b) -> Body ctx a -> Body ctx b
pure :: a -> Body ctx a
$cpure :: forall k (ctx :: k) a. a -> Body ctx a
$cp1Applicative :: forall k (ctx :: k). Functor (Body ctx)
Applicative, Applicative (Body ctx)
a -> Body ctx a
Applicative (Body ctx) =>
(forall a b. Body ctx a -> (a -> Body ctx b) -> Body ctx b)
-> (forall a b. Body ctx a -> Body ctx b -> Body ctx b)
-> (forall a. a -> Body ctx a)
-> Monad (Body ctx)
Body ctx a -> (a -> Body ctx b) -> Body ctx b
Body ctx a -> Body ctx b -> Body ctx b
forall a. a -> Body ctx a
forall k (ctx :: k). Applicative (Body ctx)
forall k (ctx :: k) a. a -> Body ctx a
forall k (ctx :: k) a b. Body ctx a -> Body ctx b -> Body ctx b
forall k (ctx :: k) a b.
Body ctx a -> (a -> Body ctx b) -> Body ctx b
forall a b. Body ctx a -> Body ctx b -> Body ctx b
forall a b. Body ctx a -> (a -> Body ctx b) -> Body ctx b
forall (m :: * -> *).
Applicative m =>
(forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: a -> Body ctx a
$creturn :: forall k (ctx :: k) a. a -> Body ctx a
>> :: Body ctx a -> Body ctx b -> Body ctx b
$c>> :: forall k (ctx :: k) a b. Body ctx a -> Body ctx b -> Body ctx b
>>= :: Body ctx a -> (a -> Body ctx b) -> Body ctx b
$c>>= :: forall k (ctx :: k) a b.
Body ctx a -> (a -> Body ctx b) -> Body ctx b
$cp1Monad :: forall k (ctx :: k). Applicative (Body ctx)
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 :: Body ctx ()
body1 \/ :: Body ctx () -> Body ctx () -> Body ctx ()
\/ body2 :: Body ctx ()
body2 = do
  let rules1 :: AST
rules1 = [AST] -> AST
And' ([AST] -> AST) -> [AST] -> AST
forall a b. (a -> b) -> a -> b
$ Body ctx () -> [AST]
forall k (ctx :: k) a. Body ctx a -> [AST]
runBody Body ctx ()
body1
      rules2 :: AST
rules2 = [AST] -> AST
And' ([AST] -> AST) -> [AST] -> AST
forall a b. (a -> b) -> a -> b
$ Body ctx () -> [AST]
forall k (ctx :: k) a. Body ctx a -> [AST]
runBody Body ctx ()
body2
  [AST] -> Body ctx ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [[AST] -> AST
Or' [AST
rules1, AST
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 ctx a -> Body ctx ()
not' body :: Body ctx a
body = do
  let rules :: AST
rules = [AST] -> AST
And' ([AST] -> AST) -> [AST] -> AST
forall a b. (a -> b) -> a -> b
$ Body ctx a -> [AST]
forall k (ctx :: k) a. Body ctx a -> [AST]
runBody Body ctx a
body
  [AST] -> Body ctx ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [AST -> AST
Not' AST
rules]

runBody :: Body ctx a -> [AST]
runBody :: Body ctx a -> [AST]
runBody (Body m :: Writer [AST] a
m) = Writer [AST] a -> [AST]
forall w a. Writer w a -> w
execWriter Writer [AST] a
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 = Metadata a -> Proxy a -> Metadata a
forall a b. a -> b -> a
const (Metadata a -> Proxy a -> Metadata a)
-> Metadata a -> Proxy a -> Metadata a
forall a b. (a -> b) -> a -> b
$ StructureOpt a -> InlineOpt (FactDirection a) -> Metadata a
forall a.
StructureOpt a -> InlineOpt (FactDirection a) -> Metadata a
Metadata StructureOpt a
forall a. StructureOpt a
Automatic InlineOpt (FactDirection a)
forall (d :: Direction). InlineOpt d
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
--   <https://souffle-lang.github.io/tuning#datastructure link> and this
--   <https://souffle-lang.github.io/relations link>.
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 :: DSL prog 'Definition (Predicate a)
predicateFor = do
  let typeInfo :: TypeInfo a (Structure a)
typeInfo = TypeInfo a (Structure a)
forall k (a :: k) (ts :: [*]). TypeInfo a ts
TypeInfo :: TypeInfo a (Structure a)
      p :: Proxy a
p = Proxy a
forall k (t :: k). Proxy t
Proxy :: Proxy a
      name :: VarName
name = FilePath -> VarName
T.pack (FilePath -> VarName) -> FilePath -> VarName
forall a b. (a -> b) -> a -> b
$ Proxy a -> FilePath
forall a. Fact a => Proxy a -> FilePath
factName Proxy a
p
      accNames :: [VarName]
accNames = [VarName] -> Maybe [VarName] -> [VarName]
forall a. a -> Maybe a -> a
fromMaybe [VarName]
genericNames (Maybe [VarName] -> [VarName]) -> Maybe [VarName] -> [VarName]
forall a b. (a -> b) -> a -> b
$ Proxy a -> Maybe [VarName]
forall a.
KnownSymbols (AccessorNames a) =>
Proxy a -> Maybe [VarName]
accessorNames Proxy a
p
      opts :: SimpleMetadata
opts = Metadata a -> SimpleMetadata
forall a. Metadata a -> SimpleMetadata
toSimpleMetadata (Metadata a -> SimpleMetadata) -> Metadata a -> SimpleMetadata
forall a b. (a -> b) -> a -> b
$ Proxy a -> Metadata a
forall a. FactMetadata a => Proxy a -> Metadata a
factOpts Proxy a
p
      genericNames :: [VarName]
genericNames = (Integer -> VarName) -> [Integer] -> [VarName]
forall a b. (a -> b) -> [a] -> [b]
map (("t" VarName -> VarName -> VarName
forall a. Semigroup a => a -> a -> a
<>) (VarName -> VarName) -> (Integer -> VarName) -> Integer -> VarName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> VarName
T.pack (FilePath -> VarName)
-> (Integer -> FilePath) -> Integer -> VarName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> FilePath
forall a. Show a => a -> FilePath
show) [1..]
      tys :: [DLType]
tys = Proxy (Collect (Rep a)) -> [DLType]
forall (ts :: [*]). KnownDLTypes ts => Proxy ts -> [DLType]
getTypes (Proxy (Structure a)
forall k (t :: k). Proxy t
Proxy :: Proxy (Structure a))
      direction :: Direction
direction = Proxy (FactDirection a) -> Direction
forall k (a :: k). KnownDirection a => Proxy a -> Direction
getDirection (Proxy (FactDirection a)
forall k (t :: k). Proxy t
Proxy :: Proxy (FactDirection a))
      fields :: [FieldData]
fields = (DLType -> VarName -> FieldData)
-> [DLType] -> [VarName] -> [FieldData]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith DLType -> VarName -> FieldData
FieldData [DLType]
tys [VarName]
accNames
      definition :: AST
definition = VarName -> Direction -> [FieldData] -> SimpleMetadata -> AST
Declare' VarName
name Direction
direction [FieldData]
fields SimpleMetadata
opts
  AST -> DSL prog 'Definition ()
forall k (prog :: k). AST -> DSL prog 'Definition ()
addDefinition AST
definition
  Predicate a -> DSL prog 'Definition (Predicate a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Predicate a -> DSL prog 'Definition (Predicate a))
-> Predicate a -> DSL prog 'Definition (Predicate a)
forall a b. (a -> b) -> a -> b
$ (forall (f :: UsageContext -> * -> *) (ctx :: UsageContext).
 Fragment f ctx =>
 Tuple ctx (Structure a) -> f ctx ())
-> Predicate a
forall a.
(forall (f :: UsageContext -> * -> *) (ctx :: UsageContext).
 Fragment f ctx =>
 Tuple ctx (Structure a) -> f ctx ())
-> Predicate a
Predicate ((forall (f :: UsageContext -> * -> *) (ctx :: UsageContext).
  Fragment f ctx =>
  Tuple ctx (Structure a) -> f ctx ())
 -> Predicate a)
-> (forall (f :: UsageContext -> * -> *) (ctx :: UsageContext).
    Fragment f ctx =>
    Tuple ctx (Structure a) -> f ctx ())
-> Predicate a
forall a b. (a -> b) -> a -> b
$ TypeInfo a (Collect (Rep a))
-> VarName -> Tuple ctx (Collect (Rep a)) -> f ctx ()
forall (f :: UsageContext -> * -> *) (ctx :: UsageContext) k
       (ts :: [*]) (a :: k).
(Fragment f ctx, ToTerms ts) =>
TypeInfo a ts -> VarName -> Tuple ctx ts -> f ctx ()
toFragment TypeInfo a (Collect (Rep a))
TypeInfo a (Structure a)
typeInfo VarName
name

toSimpleMetadata :: Metadata a -> SimpleMetadata
toSimpleMetadata :: Metadata a -> SimpleMetadata
toSimpleMetadata (Metadata struct :: StructureOpt a
struct inline :: InlineOpt (FactDirection a)
inline) =
  let structOpt :: StructureOption
structOpt = case StructureOpt a
struct of
        Automatic -> StructureOption
AutomaticLayout
        BTree -> StructureOption
BTreeLayout
        Brie -> StructureOption
BrieLayout
        EqRel -> StructureOption
EqRelLayout
      inlineOpt :: InlineOption
inlineOpt = case InlineOpt (FactDirection a)
inline of
        Inline -> InlineOption
DoInline
        NoInline -> InlineOption
DoNotInline
  in StructureOption -> InlineOption -> SimpleMetadata
SimpleMetadata StructureOption
structOpt InlineOption
inlineOpt

class KnownDirection a where
  getDirection :: Proxy a -> Direction
instance KnownDirection 'Input where getDirection :: Proxy 'Input -> Direction
getDirection = Direction -> Proxy 'Input -> Direction
forall a b. a -> b -> a
const Direction
Input
instance KnownDirection 'Output where getDirection :: Proxy 'Output -> Direction
getDirection = Direction -> Proxy 'Output -> Direction
forall a b. a -> b -> a
const Direction
Output
instance KnownDirection 'InputOutput where getDirection :: Proxy 'InputOutput -> Direction
getDirection = Direction -> Proxy 'InputOutput -> Direction
forall a b. a -> b -> a
const Direction
InputOutput
instance KnownDirection 'Internal where getDirection :: Proxy 'Internal -> Direction
getDirection = Direction -> Proxy 'Internal -> Direction
forall a b. a -> b -> a
const Direction
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 :: VarName
name terms :: NonEmpty SimpleTerm
terms |- :: Head 'Relation a -> Body 'Relation () -> DSL prog 'Definition ()
|- body :: Body 'Relation ()
body =
  let rules :: [AST]
rules = Body 'Relation () -> [AST]
forall k (ctx :: k) a. Body ctx a -> [AST]
runBody Body 'Relation ()
body
      relation :: AST
relation = VarName -> NonEmpty SimpleTerm -> AST -> AST
Rule' VarName
name NonEmpty SimpleTerm
terms ([AST] -> AST
And' [AST]
rules)
  in AST -> DSL prog 'Definition ()
forall k (prog :: k). AST -> DSL prog 'Definition ()
addDefinition AST
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 a ts -> VarName -> Tuple 'Relation ts -> Head 'Relation ()
toFragment typeInfo :: TypeInfo a ts
typeInfo name :: VarName
name terms :: Tuple 'Relation ts
terms =
    let terms' :: NonEmpty SimpleTerm
terms' = Proxy 'Relation
-> TypeInfo a ts -> Tuple 'Relation ts -> NonEmpty SimpleTerm
forall (ts :: [*]) k (ctx :: UsageContext) (a :: k).
ToTerms ts =>
Proxy ctx -> TypeInfo a ts -> Tuple ctx ts -> NonEmpty SimpleTerm
toTerms (Proxy 'Relation
forall k (t :: k). Proxy t
Proxy :: Proxy 'Relation) TypeInfo a ts
typeInfo Tuple 'Relation ts
terms
     in VarName -> NonEmpty SimpleTerm -> Head 'Relation ()
forall k k (ctx :: k) (unused :: k).
VarName -> NonEmpty SimpleTerm -> Head ctx unused
Head VarName
name NonEmpty SimpleTerm
terms'

instance Fragment Body 'Relation where
  toFragment :: TypeInfo a ts -> VarName -> Tuple 'Relation ts -> Body 'Relation ()
toFragment typeInfo :: TypeInfo a ts
typeInfo name :: VarName
name terms :: Tuple 'Relation ts
terms =
    let terms' :: NonEmpty SimpleTerm
terms' = Proxy 'Relation
-> TypeInfo a ts -> Tuple 'Relation ts -> NonEmpty SimpleTerm
forall (ts :: [*]) k (ctx :: UsageContext) (a :: k).
ToTerms ts =>
Proxy ctx -> TypeInfo a ts -> Tuple ctx ts -> NonEmpty SimpleTerm
toTerms (Proxy 'Relation
forall k (t :: k). Proxy t
Proxy :: Proxy 'Relation) TypeInfo a ts
typeInfo Tuple 'Relation ts
terms
    in [AST] -> Body 'Relation ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [VarName -> NonEmpty SimpleTerm -> AST
Atom' VarName
name NonEmpty SimpleTerm
terms']

instance Fragment (DSL prog) 'Definition where
  toFragment :: TypeInfo a ts
-> VarName -> Tuple 'Definition ts -> DSL prog 'Definition ()
toFragment typeInfo :: TypeInfo a ts
typeInfo name :: VarName
name terms :: Tuple 'Definition ts
terms =
    let terms' :: NonEmpty SimpleTerm
terms' = Proxy 'Definition
-> TypeInfo a ts -> Tuple 'Definition ts -> NonEmpty SimpleTerm
forall (ts :: [*]) k (ctx :: UsageContext) (a :: k).
ToTerms ts =>
Proxy ctx -> TypeInfo a ts -> Tuple ctx ts -> NonEmpty SimpleTerm
toTerms (Proxy 'Definition
forall k (t :: k). Proxy t
Proxy :: Proxy 'Definition) TypeInfo a ts
typeInfo Tuple 'Definition ts
terms
     in AST -> DSL prog 'Definition ()
forall k (prog :: k). AST -> DSL prog 'Definition ()
addDefinition (AST -> DSL prog 'Definition ()) -> AST -> DSL prog 'Definition ()
forall a b. (a -> b) -> a -> b
$ VarName -> NonEmpty SimpleTerm -> AST
Atom' VarName
name NonEmpty SimpleTerm
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 -> FilePath -> DSL prog 'Definition () -> IO ()
renderIO prog :: prog
prog path :: FilePath
path = FilePath -> VarName -> IO ()
TIO.writeFile FilePath
path (VarName -> IO ())
-> (DSL prog 'Definition () -> VarName)
-> DSL prog 'Definition ()
-> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. prog -> DSL prog 'Definition () -> VarName
forall prog.
Program prog =>
prog -> DSL prog 'Definition () -> VarName
render prog
prog

-- | Renders a DSL fragment to the corresponding Datalog code.
render :: Program prog => prog -> DSL prog 'Definition () -> T.Text
render :: prog -> DSL prog 'Definition () -> VarName
render prog :: prog
prog = (Reader RenderMode VarName -> RenderMode -> VarName)
-> RenderMode -> Reader RenderMode VarName -> VarName
forall a b c. (a -> b -> c) -> b -> a -> c
flip Reader RenderMode VarName -> RenderMode -> VarName
forall r a. Reader r a -> r -> a
runReader RenderMode
TopLevel (Reader RenderMode VarName -> VarName)
-> (DSL prog 'Definition () -> Reader RenderMode VarName)
-> DSL prog 'Definition ()
-> VarName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DL -> Reader RenderMode VarName
f (DL -> Reader RenderMode VarName)
-> (DSL prog 'Definition () -> DL)
-> DSL prog 'Definition ()
-> Reader RenderMode VarName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. prog -> DSL prog 'Definition () -> DL
forall prog a. Program prog => prog -> DSL prog 'Definition a -> DL
runDSL prog
prog where
  f :: DL -> Reader RenderMode VarName
f = \case
    Statements stmts :: [DL]
stmts ->
      [VarName] -> VarName
T.unlines ([VarName] -> VarName)
-> ReaderT RenderMode Identity [VarName]
-> Reader RenderMode VarName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (DL -> Reader RenderMode VarName)
-> [DL] -> ReaderT RenderMode Identity [VarName]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse DL -> Reader RenderMode VarName
f [DL]
stmts
    Declare name :: VarName
name dir :: Direction
dir fields :: [FieldData]
fields metadata :: SimpleMetadata
metadata ->
      let fieldPairs :: [VarName]
fieldPairs = (FieldData -> VarName) -> [FieldData] -> [VarName]
forall a b. (a -> b) -> [a] -> [b]
map FieldData -> VarName
renderField [FieldData]
fields
          renderedFactOpts :: VarName
renderedFactOpts = SimpleMetadata -> VarName
renderMetadata SimpleMetadata
metadata
          renderedOpts :: VarName
renderedOpts = if VarName -> Bool
T.null VarName
renderedFactOpts then "" else " " VarName -> VarName -> VarName
forall a. Semigroup a => a -> a -> a
<> VarName
renderedFactOpts
       in VarName -> Reader RenderMode VarName
forall (f :: * -> *) a. Applicative f => a -> f a
pure (VarName -> Reader RenderMode VarName)
-> VarName -> Reader RenderMode VarName
forall a b. (a -> b) -> a -> b
$ VarName -> [VarName] -> VarName
T.intercalate "\n" ([VarName] -> VarName) -> [VarName] -> VarName
forall a b. (a -> b) -> a -> b
$ [Maybe VarName] -> [VarName]
forall a. [Maybe a] -> [a]
catMaybes
        [ VarName -> Maybe VarName
forall a. a -> Maybe a
Just (VarName -> Maybe VarName) -> VarName -> Maybe VarName
forall a b. (a -> b) -> a -> b
$ ".decl " VarName -> VarName -> VarName
forall a. Semigroup a => a -> a -> a
<> VarName
name VarName -> VarName -> VarName
forall a. Semigroup a => a -> a -> a
<> "(" VarName -> VarName -> VarName
forall a. Semigroup a => a -> a -> a
<> VarName -> [VarName] -> VarName
T.intercalate ", " [VarName]
fieldPairs VarName -> VarName -> VarName
forall a. Semigroup a => a -> a -> a
<> ")" VarName -> VarName -> VarName
forall a. Semigroup a => a -> a -> a
<> VarName
renderedOpts
        , VarName -> Direction -> Maybe VarName
renderDir VarName
name Direction
dir
        ]
    Atom name :: VarName
name terms :: NonEmpty SimpleTerm
terms -> do
      let rendered :: VarName
rendered = VarName
name VarName -> VarName -> VarName
forall a. Semigroup a => a -> a -> a
<> "(" VarName -> VarName -> VarName
forall a. Semigroup a => a -> a -> a
<> [SimpleTerm] -> VarName
renderTerms (NonEmpty SimpleTerm -> [SimpleTerm]
forall a. NonEmpty a -> [a]
toList NonEmpty SimpleTerm
terms) VarName -> VarName -> VarName
forall a. Semigroup a => a -> a -> a
<> ")"
      VarName
end <- Reader RenderMode VarName
maybeDot
      VarName -> Reader RenderMode VarName
forall (f :: * -> *) a. Applicative f => a -> f a
pure (VarName -> Reader RenderMode VarName)
-> VarName -> Reader RenderMode VarName
forall a b. (a -> b) -> a -> b
$ VarName
rendered VarName -> VarName -> VarName
forall a. Semigroup a => a -> a -> a
<> VarName
end
    Rule name :: VarName
name terms :: NonEmpty SimpleTerm
terms body :: DL
body -> do
      VarName
body' <- DL -> Reader RenderMode VarName
f DL
body
      let rendered :: VarName
rendered =
            VarName
name VarName -> VarName -> VarName
forall a. Semigroup a => a -> a -> a
<> "(" VarName -> VarName -> VarName
forall a. Semigroup a => a -> a -> a
<> [SimpleTerm] -> VarName
renderTerms (NonEmpty SimpleTerm -> [SimpleTerm]
forall a. NonEmpty a -> [a]
toList NonEmpty SimpleTerm
terms) VarName -> VarName -> VarName
forall a. Semigroup a => a -> a -> a
<> ") :-\n" VarName -> VarName -> VarName
forall a. Semigroup a => a -> a -> a
<>
            VarName -> [VarName] -> VarName
T.intercalate "\n" ((VarName -> VarName) -> [VarName] -> [VarName]
forall a b. (a -> b) -> [a] -> [b]
map VarName -> VarName
indent ([VarName] -> [VarName]) -> [VarName] -> [VarName]
forall a b. (a -> b) -> a -> b
$ VarName -> [VarName]
T.lines VarName
body')
      VarName -> Reader RenderMode VarName
forall (f :: * -> *) a. Applicative f => a -> f a
pure VarName
rendered
    And e1 :: DL
e1 e2 :: DL
e2 -> do
      VarName
txt <- Reader RenderMode VarName -> Reader RenderMode VarName
forall a.
ReaderT RenderMode Identity a -> ReaderT RenderMode Identity a
nested (Reader RenderMode VarName -> Reader RenderMode VarName)
-> Reader RenderMode VarName -> Reader RenderMode VarName
forall a b. (a -> b) -> a -> b
$ do
        VarName
txt1 <- DL -> Reader RenderMode VarName
f DL
e1
        VarName
txt2 <- DL -> Reader RenderMode VarName
f DL
e2
        VarName -> Reader RenderMode VarName
forall (f :: * -> *) a. Applicative f => a -> f a
pure (VarName -> Reader RenderMode VarName)
-> VarName -> Reader RenderMode VarName
forall a b. (a -> b) -> a -> b
$ VarName
txt1 VarName -> VarName -> VarName
forall a. Semigroup a => a -> a -> a
<> ",\n" VarName -> VarName -> VarName
forall a. Semigroup a => a -> a -> a
<> VarName
txt2
      VarName
end <- Reader RenderMode VarName
maybeDot
      VarName -> Reader RenderMode VarName
forall (f :: * -> *) a. Applicative f => a -> f a
pure (VarName -> Reader RenderMode VarName)
-> VarName -> Reader RenderMode VarName
forall a b. (a -> b) -> a -> b
$ VarName
txt VarName -> VarName -> VarName
forall a. Semigroup a => a -> a -> a
<> VarName
end
    Or e1 :: DL
e1 e2 :: DL
e2 -> do
      VarName
txt <- Reader RenderMode VarName -> Reader RenderMode VarName
forall a.
ReaderT RenderMode Identity a -> ReaderT RenderMode Identity a
nested (Reader RenderMode VarName -> Reader RenderMode VarName)
-> Reader RenderMode VarName -> Reader RenderMode VarName
forall a b. (a -> b) -> a -> b
$ do
        VarName
txt1 <- DL -> Reader RenderMode VarName
f DL
e1
        VarName
txt2 <- DL -> Reader RenderMode VarName
f DL
e2
        VarName -> Reader RenderMode VarName
forall (f :: * -> *) a. Applicative f => a -> f a
pure (VarName -> Reader RenderMode VarName)
-> VarName -> Reader RenderMode VarName
forall a b. (a -> b) -> a -> b
$ VarName
txt1 VarName -> VarName -> VarName
forall a. Semigroup a => a -> a -> a
<> ";\n" VarName -> VarName -> VarName
forall a. Semigroup a => a -> a -> a
<> VarName
txt2
      VarName
end <- Reader RenderMode VarName
maybeDot
      case VarName
end of
        "." -> VarName -> Reader RenderMode VarName
forall (f :: * -> *) a. Applicative f => a -> f a
pure (VarName -> Reader RenderMode VarName)
-> VarName -> Reader RenderMode VarName
forall a b. (a -> b) -> a -> b
$ VarName
txt VarName -> VarName -> VarName
forall a. Semigroup a => a -> a -> a
<> VarName
end
        _ -> VarName -> Reader RenderMode VarName
forall (f :: * -> *) a. Applicative f => a -> f a
pure (VarName -> Reader RenderMode VarName)
-> VarName -> Reader RenderMode VarName
forall a b. (a -> b) -> a -> b
$ "(" VarName -> VarName -> VarName
forall a. Semigroup a => a -> a -> a
<> VarName
txt VarName -> VarName -> VarName
forall a. Semigroup a => a -> a -> a
<> ")"
    Not e :: DL
e -> do
      let maybeAddParens :: VarName -> VarName
maybeAddParens txt :: VarName
txt = case DL
e of
            And _ _ -> "(" VarName -> VarName -> VarName
forall a. Semigroup a => a -> a -> a
<> VarName
txt VarName -> VarName -> VarName
forall a. Semigroup a => a -> a -> a
<> ")"
            _ -> VarName
txt
      VarName
txt <- VarName -> VarName
maybeAddParens (VarName -> VarName)
-> Reader RenderMode VarName -> Reader RenderMode VarName
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Reader RenderMode VarName -> Reader RenderMode VarName
forall a.
ReaderT RenderMode Identity a -> ReaderT RenderMode Identity a
nested (DL -> Reader RenderMode VarName
f DL
e)
      VarName
end <- Reader RenderMode VarName
maybeDot
      case VarName
end of
        "." -> VarName -> Reader RenderMode VarName
forall (f :: * -> *) a. Applicative f => a -> f a
pure (VarName -> Reader RenderMode VarName)
-> VarName -> Reader RenderMode VarName
forall a b. (a -> b) -> a -> b
$ "!" VarName -> VarName -> VarName
forall a. Semigroup a => a -> a -> a
<> VarName
txt VarName -> VarName -> VarName
forall a. Semigroup a => a -> a -> a
<> VarName
end
        _ -> VarName -> Reader RenderMode VarName
forall (f :: * -> *) a. Applicative f => a -> f a
pure (VarName -> Reader RenderMode VarName)
-> VarName -> Reader RenderMode VarName
forall a b. (a -> b) -> a -> b
$ "!" VarName -> VarName -> VarName
forall a. Semigroup a => a -> a -> a
<> VarName
txt
    Constrain t :: SimpleTerm
t -> do
      let t' :: VarName
t' = SimpleTerm -> VarName
renderTerm SimpleTerm
t
      VarName
end <- Reader RenderMode VarName
maybeDot
      case VarName
end of
        "." -> VarName -> Reader RenderMode VarName
forall (f :: * -> *) a. Applicative f => a -> f a
pure (VarName -> Reader RenderMode VarName)
-> VarName -> Reader RenderMode VarName
forall a b. (a -> b) -> a -> b
$ VarName
t' VarName -> VarName -> VarName
forall a. Semigroup a => a -> a -> a
<> "."
        _ -> VarName -> Reader RenderMode VarName
forall (f :: * -> *) a. Applicative f => a -> f a
pure VarName
t'
  indent :: VarName -> VarName
indent = ("  " VarName -> VarName -> VarName
forall a. Semigroup a => a -> a -> a
<>)
  nested :: ReaderT RenderMode Identity a -> ReaderT RenderMode Identity a
nested = (RenderMode -> RenderMode)
-> ReaderT RenderMode Identity a -> ReaderT RenderMode Identity a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (RenderMode -> RenderMode -> RenderMode
forall a b. a -> b -> a
const RenderMode
Nested)
  maybeDot :: Reader RenderMode VarName
maybeDot = ReaderT RenderMode Identity RenderMode
forall r (m :: * -> *). MonadReader r m => m r
ask ReaderT RenderMode Identity RenderMode
-> (RenderMode -> Reader RenderMode VarName)
-> Reader RenderMode VarName
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    TopLevel -> VarName -> Reader RenderMode VarName
forall (f :: * -> *) a. Applicative f => a -> f a
pure "."
    Nested -> VarName -> Reader RenderMode VarName
forall (f :: * -> *) a. Applicative f => a -> f a
pure VarName
forall a. Monoid a => a
mempty

renderDir :: VarName -> Direction -> Maybe T.Text
renderDir :: VarName -> Direction -> Maybe VarName
renderDir name :: VarName
name = \case
  Input -> VarName -> Maybe VarName
forall a. a -> Maybe a
Just (VarName -> Maybe VarName) -> VarName -> Maybe VarName
forall a b. (a -> b) -> a -> b
$ ".input " VarName -> VarName -> VarName
forall a. Semigroup a => a -> a -> a
<> VarName
name
  Output -> VarName -> Maybe VarName
forall a. a -> Maybe a
Just (VarName -> Maybe VarName) -> VarName -> Maybe VarName
forall a b. (a -> b) -> a -> b
$ ".output " VarName -> VarName -> VarName
forall a. Semigroup a => a -> a -> a
<> VarName
name
  InputOutput -> VarName -> Maybe VarName
forall a. a -> Maybe a
Just (VarName -> Maybe VarName) -> VarName -> Maybe VarName
forall a b. (a -> b) -> a -> b
$ VarName -> [VarName] -> VarName
T.intercalate "\n"
                      ([VarName] -> VarName) -> [VarName] -> VarName
forall a b. (a -> b) -> a -> b
$ [Maybe VarName] -> [VarName]
forall a. [Maybe a] -> [a]
catMaybes [VarName -> Direction -> Maybe VarName
renderDir VarName
name Direction
Input, VarName -> Direction -> Maybe VarName
renderDir VarName
name Direction
Output]
  Internal -> Maybe VarName
forall a. Maybe a
Nothing

renderField :: FieldData -> T.Text
renderField :: FieldData -> VarName
renderField (FieldData ty :: DLType
ty accName :: VarName
accName) =
  let txt :: VarName
txt = case DLType
ty of
        DLNumber -> ": number"
        DLUnsigned -> ": unsigned"
        DLFloat -> ": float"
        DLString -> ": symbol"
   in VarName
accName VarName -> VarName -> VarName
forall a. Semigroup a => a -> a -> a
<> VarName
txt

renderMetadata :: SimpleMetadata -> T.Text
renderMetadata :: SimpleMetadata -> VarName
renderMetadata (SimpleMetadata struct :: StructureOption
struct inline :: InlineOption
inline) =
  let structTxt :: Maybe VarName
structTxt = case StructureOption
struct of
        AutomaticLayout -> Maybe VarName
forall a. Maybe a
Nothing
        BTreeLayout -> VarName -> Maybe VarName
forall a. a -> Maybe a
Just "btree"
        BrieLayout -> VarName -> Maybe VarName
forall a. a -> Maybe a
Just "brie"
        EqRelLayout -> VarName -> Maybe VarName
forall a. a -> Maybe a
Just "eqrel"
      inlineTxt :: Maybe VarName
inlineTxt = case InlineOption
inline of
        DoInline -> VarName -> Maybe VarName
forall a. a -> Maybe a
Just "inline"
        DoNotInline -> Maybe VarName
forall a. Maybe a
Nothing
  in VarName -> [VarName] -> VarName
T.intercalate " " ([VarName] -> VarName) -> [VarName] -> VarName
forall a b. (a -> b) -> a -> b
$ [Maybe VarName] -> [VarName]
forall a. [Maybe a] -> [a]
catMaybes [Maybe VarName
structTxt, Maybe VarName
inlineTxt]

renderTerms :: [SimpleTerm] -> T.Text
renderTerms :: [SimpleTerm] -> VarName
renderTerms = VarName -> [VarName] -> VarName
T.intercalate ", " ([VarName] -> VarName)
-> ([SimpleTerm] -> [VarName]) -> [SimpleTerm] -> VarName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SimpleTerm -> VarName) -> [SimpleTerm] -> [VarName]
forall a b. (a -> b) -> [a] -> [b]
map SimpleTerm -> VarName
renderTerm

renderTerm :: SimpleTerm -> T.Text
renderTerm :: SimpleTerm -> VarName
renderTerm = \case
  I x :: Int32
x -> FilePath -> VarName
T.pack (FilePath -> VarName) -> FilePath -> VarName
forall a b. (a -> b) -> a -> b
$ Int32 -> FilePath
forall a. Show a => a -> FilePath
show Int32
x
  U x :: Word32
x -> FilePath -> VarName
T.pack (FilePath -> VarName) -> FilePath -> VarName
forall a b. (a -> b) -> a -> b
$ Word32 -> FilePath
forall a. Show a => a -> FilePath
show Word32
x
  F x :: Float
x -> FilePath -> VarName
T.pack (FilePath -> VarName) -> FilePath -> VarName
forall a b. (a -> b) -> a -> b
$ FilePath -> Float -> FilePath
forall r. PrintfType r => FilePath -> r
printf "%f" Float
x
  S s :: FilePath
s -> "\"" VarName -> VarName -> VarName
forall a. Semigroup a => a -> a -> a
<> FilePath -> VarName
T.pack FilePath
s VarName -> VarName -> VarName
forall a. Semigroup a => a -> a -> a
<> "\""
  V v :: VarName
v -> VarName
v
  Underscore -> "_"

  BinOp' op :: Op2
op t1 :: SimpleTerm
t1 t2 :: SimpleTerm
t2 -> SimpleTerm -> VarName
renderTerm SimpleTerm
t1 VarName -> VarName -> VarName
forall a. Semigroup a => a -> a -> a
<> " " VarName -> VarName -> VarName
forall a. Semigroup a => a -> a -> a
<> Op2 -> VarName
renderBinOp Op2
op VarName -> VarName -> VarName
forall a. Semigroup a => a -> a -> a
<> " " VarName -> VarName -> VarName
forall a. Semigroup a => a -> a -> a
<> SimpleTerm -> VarName
renderTerm SimpleTerm
t2
  UnaryOp' op :: Op1
op t1 :: SimpleTerm
t1 -> Op1 -> VarName
forall p. IsString p => Op1 -> p
renderUnaryOp Op1
op VarName -> VarName -> VarName
forall a. Semigroup a => a -> a -> a
<> SimpleTerm -> VarName
renderTerm SimpleTerm
t1
  Func' name :: FuncName
name ts :: NonEmpty SimpleTerm
ts -> FuncName -> VarName
renderFunc FuncName
name VarName -> VarName -> VarName
forall a. Semigroup a => a -> a -> a
<> "(" VarName -> VarName -> VarName
forall a. Semigroup a => a -> a -> a
<> [SimpleTerm] -> VarName
renderTerms (NonEmpty SimpleTerm -> [SimpleTerm]
forall a. NonEmpty a -> [a]
toList NonEmpty SimpleTerm
ts) VarName -> VarName -> VarName
forall a. Semigroup a => a -> a -> a
<> ")"
  where
    renderFunc :: FuncName -> VarName
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 :: Op2 -> VarName
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 :: Op1 -> p
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 :: Term ctx ty
underscore = Term ctx ty
forall (ctx :: UsageContext) ty. Term ctx ty
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
__ :: Term ctx ty
__ = Term ctx ty
forall (ctx :: UsageContext) ty. Term ctx ty
underscore

class ToString a where
  toString :: a -> String

instance ToString String where toString :: FilePath -> FilePath
toString = FilePath -> FilePath
forall a. a -> a
id
instance ToString T.Text where toString :: VarName -> FilePath
toString = VarName -> FilePath
T.unpack
instance ToString TL.Text where toString :: Text -> FilePath
toString = Text -> FilePath
TL.unpack

instance IsString (Term ctx String) where fromString :: FilePath -> Term ctx FilePath
fromString = FilePath -> Term ctx FilePath
forall ty (ctx :: UsageContext). ToString ty => ty -> Term ctx ty
StringTerm
instance IsString (Term ctx T.Text) where fromString :: FilePath -> Term ctx VarName
fromString = VarName -> Term ctx VarName
forall ty (ctx :: UsageContext). ToString ty => ty -> Term ctx ty
StringTerm (VarName -> Term ctx VarName)
-> (FilePath -> VarName) -> FilePath -> Term ctx VarName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> VarName
T.pack
instance IsString (Term ctx TL.Text) where fromString :: FilePath -> Term ctx Text
fromString = Text -> Term ctx Text
forall ty (ctx :: UsageContext). ToString ty => ty -> Term ctx ty
StringTerm (Text -> Term ctx Text)
-> (FilePath -> Text) -> FilePath -> Term ctx Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FilePath -> Text
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' :: Integer -> Term ctx Int32
fromInteger' = Int32 -> Term ctx Int32
forall (ctx :: UsageContext). Int32 -> Term ctx Int32
NumberTerm (Int32 -> Term ctx Int32)
-> (Integer -> Int32) -> Integer -> Term ctx Int32
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Int32
forall a. Num a => Integer -> a
fromInteger
instance SupportsArithmetic Word32 where
  fromInteger' :: Integer -> Term ctx Word32
fromInteger' = Word32 -> Term ctx Word32
forall (ctx :: UsageContext). Word32 -> Term ctx Word32
UnsignedTerm (Word32 -> Term ctx Word32)
-> (Integer -> Word32) -> Integer -> Term ctx Word32
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Word32
forall a. Num a => Integer -> a
fromInteger
instance SupportsArithmetic Float where
  fromInteger' :: Integer -> Term ctx Float
fromInteger' = Float -> Term ctx Float
forall (ctx :: UsageContext). Float -> Term ctx Float
FloatTerm (Float -> Term ctx Float)
-> (Integer -> Float) -> Integer -> Term ctx Float
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Integer -> Float
forall a. Num a => Integer -> a
fromInteger

instance (SupportsArithmetic ty, Num ty) => Num (Term ctx ty) where
  fromInteger :: Integer -> Term ctx ty
fromInteger = Integer -> Term ctx ty
forall ty (ctx :: UsageContext).
SupportsArithmetic ty =>
Integer -> Term ctx ty
fromInteger'
  + :: Term ctx ty -> Term ctx ty -> Term ctx ty
(+) = Op2 -> Term ctx ty -> Term ctx ty -> Term ctx ty
forall ty (ctx :: UsageContext).
Num ty =>
Op2 -> Term ctx ty -> Term ctx ty -> Term ctx ty
BinOp Op2
Plus
  * :: Term ctx ty -> Term ctx ty -> Term ctx ty
(*) = Op2 -> Term ctx ty -> Term ctx ty -> Term ctx ty
forall ty (ctx :: UsageContext).
Num ty =>
Op2 -> Term ctx ty -> Term ctx ty -> Term ctx ty
BinOp Op2
Mul
  (-) = Op2 -> Term ctx ty -> Term ctx ty -> Term ctx ty
forall ty (ctx :: UsageContext).
Num ty =>
Op2 -> Term ctx ty -> Term ctx ty -> Term ctx ty
BinOp Op2
Subtract
  negate :: Term ctx ty -> Term ctx ty
negate = Op1 -> Term ctx ty -> Term ctx ty
forall ty (ctx :: UsageContext).
Num ty =>
Op1 -> Term ctx ty -> Term ctx ty
UnaryOp Op1
Negate
  abs :: Term ctx ty -> Term ctx ty
abs = FilePath -> Term ctx ty -> Term ctx ty
forall a. HasCallStack => FilePath -> a
error "'abs' is not supported for Souffle terms"
  signum :: Term ctx ty -> Term ctx ty
signum = FilePath -> Term ctx ty -> Term ctx ty
forall a. HasCallStack => FilePath -> a
error "'signum' is not supported for Souffle terms"

instance Fractional (Term ctx Float) where
  fromRational :: Rational -> Term ctx Float
fromRational = Float -> Term ctx Float
forall (ctx :: UsageContext). Float -> Term ctx Float
FloatTerm (Float -> Term ctx Float)
-> (Rational -> Float) -> Rational -> Term ctx Float
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Rational -> Float
forall a. Fractional a => Rational -> a
fromRational
  / :: Term ctx Float -> Term ctx Float -> Term ctx Float
(/) = Op2 -> Term ctx Float -> Term ctx Float -> Term ctx Float
forall ty (ctx :: UsageContext).
Num ty =>
Op2 -> Term ctx ty -> Term ctx ty -> Term ctx ty
BinOp Op2
Div

-- | Exponentiation operator ("^" in Datalog).
(.^) :: Num ty => Term ctx ty -> Term ctx ty -> Term ctx ty
.^ :: Term ctx ty -> Term ctx ty -> Term ctx ty
(.^) = Op2 -> Term ctx ty -> Term ctx ty -> Term ctx ty
forall ty (ctx :: UsageContext).
Num ty =>
Op2 -> Term ctx ty -> Term ctx ty -> Term ctx ty
BinOp Op2
Pow

-- | Remainder operator ("%" in Datalog).
(.%) :: (Num ty, Integral ty) => Term ctx ty -> Term ctx ty -> Term ctx ty
.% :: Term ctx ty -> Term ctx ty -> Term ctx ty
(.%) = Op2 -> Term ctx ty -> Term ctx ty -> Term ctx ty
forall ty (ctx :: UsageContext).
Num ty =>
Op2 -> Term ctx ty -> Term ctx ty -> Term ctx ty
BinOp Op2
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 ()
.< :: Term ctx ty -> Term ctx ty -> Body ctx ()
(.<) = Op2 -> Term ctx ty -> Term ctx ty -> Body ctx ()
forall (ctx :: UsageContext) ty.
Op2 -> Term ctx ty -> Term ctx ty -> Body ctx ()
addConstraint Op2
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 ()
.<= :: Term ctx ty -> Term ctx ty -> Body ctx ()
(.<=) = Op2 -> Term ctx ty -> Term ctx ty -> Body ctx ()
forall (ctx :: UsageContext) ty.
Op2 -> Term ctx ty -> Term ctx ty -> Body ctx ()
addConstraint Op2
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 ()
.> :: Term ctx ty -> Term ctx ty -> Body ctx ()
(.>) = Op2 -> Term ctx ty -> Term ctx ty -> Body ctx ()
forall (ctx :: UsageContext) ty.
Op2 -> Term ctx ty -> Term ctx ty -> Body ctx ()
addConstraint Op2
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 ()
.>= :: Term ctx ty -> Term ctx ty -> Body ctx ()
(.>=) = Op2 -> Term ctx ty -> Term ctx ty -> Body ctx ()
forall (ctx :: UsageContext) ty.
Op2 -> Term ctx ty -> Term ctx ty -> Body ctx ()
addConstraint Op2
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 ()
.= :: Term ctx ty -> Term ctx ty -> Body ctx ()
(.=) = Op2 -> Term ctx ty -> Term ctx ty -> Body ctx ()
forall (ctx :: UsageContext) ty.
Op2 -> Term ctx ty -> Term ctx ty -> Body ctx ()
addConstraint Op2
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 ()
.!= :: Term ctx ty -> Term ctx ty -> Body ctx ()
(.!=) = Op2 -> Term ctx ty -> Term ctx ty -> Body ctx ()
forall (ctx :: UsageContext) ty.
Op2 -> Term ctx ty -> Term ctx ty -> Body ctx ()
addConstraint Op2
IsNotEqual
infix 1 .!=

addConstraint :: Op2 -> Term ctx ty -> Term ctx ty -> Body ctx ()
addConstraint :: Op2 -> Term ctx ty -> Term ctx ty -> Body ctx ()
addConstraint op :: Op2
op e1 :: Term ctx ty
e1 e2 :: Term ctx ty
e2 =
  let expr :: SimpleTerm
expr = Op2 -> SimpleTerm -> SimpleTerm -> SimpleTerm
BinOp' Op2
op (Term ctx ty -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx ty
e1) (Term ctx ty -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx ty
e2)
   in [AST] -> Body ctx ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [SimpleTerm -> AST
Constrain' SimpleTerm
expr]

-- | Binary AND operator.
band :: (Num ty, Integral ty) => Term ctx ty -> Term ctx ty -> Term ctx ty
band :: Term ctx ty -> Term ctx ty -> Term ctx ty
band = Op2 -> Term ctx ty -> Term ctx ty -> Term ctx ty
forall ty (ctx :: UsageContext).
Num ty =>
Op2 -> Term ctx ty -> Term ctx ty -> Term ctx ty
BinOp Op2
BinaryAnd

-- | Binary OR operator.
bor :: (Num ty, Integral ty) => Term ctx ty -> Term ctx ty -> Term ctx ty
bor :: Term ctx ty -> Term ctx ty -> Term ctx ty
bor = Op2 -> Term ctx ty -> Term ctx ty -> Term ctx ty
forall ty (ctx :: UsageContext).
Num ty =>
Op2 -> Term ctx ty -> Term ctx ty -> Term ctx ty
BinOp Op2
BinaryOr

-- | Binary XOR operator.
bxor :: (Num ty, Integral ty) => Term ctx ty -> Term ctx ty -> Term ctx ty
bxor :: Term ctx ty -> Term ctx ty -> Term ctx ty
bxor = Op2 -> Term ctx ty -> Term ctx ty -> Term ctx ty
forall ty (ctx :: UsageContext).
Num ty =>
Op2 -> Term ctx ty -> Term ctx ty -> Term ctx ty
BinOp Op2
BinaryXor

-- | Logical AND operator.
land :: (Num ty, Integral ty) => Term ctx ty -> Term ctx ty -> Term ctx ty
land :: Term ctx ty -> Term ctx ty -> Term ctx ty
land = Op2 -> Term ctx ty -> Term ctx ty -> Term ctx ty
forall ty (ctx :: UsageContext).
Num ty =>
Op2 -> Term ctx ty -> Term ctx ty -> Term ctx ty
BinOp Op2
LogicalAnd

-- | Logical OR operator.
lor :: (Num ty, Integral ty) => Term ctx ty -> Term ctx ty -> Term ctx ty
lor :: Term ctx ty -> Term ctx ty -> Term ctx ty
lor = Op2 -> Term ctx ty -> Term ctx ty -> Term ctx ty
forall ty (ctx :: UsageContext).
Num ty =>
Op2 -> Term ctx ty -> Term ctx ty -> Term ctx ty
BinOp Op2
LogicalOr

-- | "max" function.
max' :: Num ty => Term ctx ty -> Term ctx ty -> Term ctx ty
max' :: Term ctx ty -> Term ctx ty -> Term ctx ty
max' = FuncName -> Term ctx ty -> Term ctx ty -> Term ctx ty
forall (ctx :: UsageContext) ty ty2.
FuncName -> Term ctx ty -> Term ctx ty -> Term ctx ty2
func2 FuncName
Max

-- | "min" function.
min' :: Num ty => Term ctx ty -> Term ctx ty -> Term ctx ty
min' :: Term ctx ty -> Term ctx ty -> Term ctx ty
min' = FuncName -> Term ctx ty -> Term ctx ty -> Term ctx ty
forall (ctx :: UsageContext) ty ty2.
FuncName -> Term ctx ty -> Term ctx ty -> Term ctx ty2
func2 FuncName
Min

-- | "cat" function (string concatenation).
cat :: ToString ty => Term ctx ty -> Term ctx ty -> Term ctx ty
cat :: Term ctx ty -> Term ctx ty -> Term ctx ty
cat = FuncName -> Term ctx ty -> Term ctx ty -> Term ctx ty
forall (ctx :: UsageContext) ty ty2.
FuncName -> Term ctx ty -> Term ctx ty -> Term ctx ty2
func2 FuncName
Cat

-- | "contains" predicate, checks if 2nd string contains the first.
contains :: ToString ty => Term ctx ty -> Term ctx ty -> Body ctx ()
contains :: Term ctx ty -> Term ctx ty -> Body ctx ()
contains a :: Term ctx ty
a b :: Term ctx ty
b =
  let expr :: SimpleTerm
expr = Term ctx Any -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm (Term ctx Any -> SimpleTerm) -> Term ctx Any -> SimpleTerm
forall a b. (a -> b) -> a -> b
$ FuncName -> Term ctx ty -> Term ctx ty -> Term ctx Any
forall (ctx :: UsageContext) ty ty2.
FuncName -> Term ctx ty -> Term ctx ty -> Term ctx ty2
func2 FuncName
Contains Term ctx ty
a Term ctx ty
b
   in [AST] -> Body ctx ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [SimpleTerm -> AST
Constrain' SimpleTerm
expr]

-- | "match" predicate, checks if a wildcard string matches a given string.
match :: ToString ty => Term ctx ty -> Term ctx ty -> Body ctx ()
match :: Term ctx ty -> Term ctx ty -> Body ctx ()
match p :: Term ctx ty
p s :: Term ctx ty
s =
  let expr :: SimpleTerm
expr = Term ctx Any -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm (Term ctx Any -> SimpleTerm) -> Term ctx Any -> SimpleTerm
forall a b. (a -> b) -> a -> b
$ FuncName -> Term ctx ty -> Term ctx ty -> Term ctx Any
forall (ctx :: UsageContext) ty ty2.
FuncName -> Term ctx ty -> Term ctx ty -> Term ctx ty2
func2 FuncName
Match Term ctx ty
p Term ctx ty
s
  in [AST] -> Body ctx ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [SimpleTerm -> AST
Constrain' SimpleTerm
expr]

-- | "ord" function.
ord :: ToString ty => Term ctx ty -> Term ctx Int32
ord :: Term ctx ty -> Term ctx Int32
ord = FuncName -> Term ctx ty -> Term ctx Int32
forall (ctx :: UsageContext) ty ty2.
FuncName -> Term ctx ty -> Term ctx ty2
func1 FuncName
Ord

-- | "strlen" function.
strlen :: ToString ty => Term ctx ty -> Term ctx Int32
strlen :: Term ctx ty -> Term ctx Int32
strlen = FuncName -> Term ctx ty -> Term ctx Int32
forall (ctx :: UsageContext) ty ty2.
FuncName -> Term ctx ty -> Term ctx ty2
func1 FuncName
StrLen

-- | "substr" function.
substr :: ToString ty => Term ctx ty -> Term ctx Int32 -> Term ctx Int32 -> Term ctx ty
substr :: Term ctx ty -> Term ctx Int32 -> Term ctx Int32 -> Term ctx ty
substr a :: Term ctx ty
a b :: Term ctx Int32
b c :: Term ctx Int32
c = FuncName -> NonEmpty SimpleTerm -> Term ctx ty
forall (ctx :: UsageContext) ty2.
FuncName -> NonEmpty SimpleTerm -> Term ctx ty2
Func FuncName
Substr (NonEmpty SimpleTerm -> Term ctx ty)
-> NonEmpty SimpleTerm -> Term ctx ty
forall a b. (a -> b) -> a -> b
$ Term ctx ty -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx ty
a SimpleTerm -> [SimpleTerm] -> NonEmpty SimpleTerm
forall a. a -> [a] -> NonEmpty a
:| [Term ctx Int32 -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx Int32
b, Term ctx Int32 -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx Int32
c]

-- | "to_number" function.
to_number :: ToString ty => Term ctx ty -> Term ctx Int32
to_number :: Term ctx ty -> Term ctx Int32
to_number = FuncName -> Term ctx ty -> Term ctx Int32
forall (ctx :: UsageContext) ty ty2.
FuncName -> Term ctx ty -> Term ctx ty2
func1 FuncName
ToNumber

-- | "to_string" function.
to_string :: ToString ty => Term ctx Int32 -> Term ctx ty
to_string :: Term ctx Int32 -> Term ctx ty
to_string = FuncName -> Term ctx Int32 -> Term ctx ty
forall (ctx :: UsageContext) ty ty2.
FuncName -> Term ctx ty -> Term ctx ty2
func1 FuncName
ToString

func1 :: FuncName -> Term ctx ty -> Term ctx ty2
func1 :: FuncName -> Term ctx ty -> Term ctx ty2
func1 name :: FuncName
name a :: Term ctx ty
a = FuncName -> NonEmpty SimpleTerm -> Term ctx ty2
forall (ctx :: UsageContext) ty2.
FuncName -> NonEmpty SimpleTerm -> Term ctx ty2
Func FuncName
name (NonEmpty SimpleTerm -> Term ctx ty2)
-> NonEmpty SimpleTerm -> Term ctx ty2
forall a b. (a -> b) -> a -> b
$ Term ctx ty -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx ty
a SimpleTerm -> [SimpleTerm] -> NonEmpty SimpleTerm
forall a. a -> [a] -> NonEmpty a
:| []

func2 :: FuncName -> Term ctx ty -> Term ctx ty -> Term ctx ty2
func2 :: FuncName -> Term ctx ty -> Term ctx ty -> Term ctx ty2
func2 name :: FuncName
name a :: Term ctx ty
a b :: Term ctx ty
b = FuncName -> NonEmpty SimpleTerm -> Term ctx ty2
forall (ctx :: UsageContext) ty2.
FuncName -> NonEmpty SimpleTerm -> Term ctx ty2
Func FuncName
name (NonEmpty SimpleTerm -> Term ctx ty2)
-> NonEmpty SimpleTerm -> Term ctx ty2
forall a b. (a -> b) -> a -> b
$ Term ctx ty -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx ty
a SimpleTerm -> [SimpleTerm] -> NonEmpty SimpleTerm
forall a. a -> [a] -> NonEmpty a
:| [Term ctx ty -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx ty
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 :: Proxy '[] -> [DLType]
getTypes _ = []

instance (KnownDLType t, KnownDLTypes ts) => KnownDLTypes (t ': ts) where
  getTypes :: Proxy (t : ts) -> [DLType]
getTypes _ = Proxy t -> DLType
forall k (t :: k). KnownDLType t => Proxy t -> DLType
getType (Proxy t
forall k (t :: k). Proxy t
Proxy :: Proxy t) DLType -> [DLType] -> [DLType]
forall a. a -> [a] -> [a]
: Proxy ts -> [DLType]
forall (ts :: [*]). KnownDLTypes ts => Proxy ts -> [DLType]
getTypes (Proxy ts
forall k (t :: k). Proxy t
Proxy :: Proxy ts)

class KnownDLType t where
  getType :: Proxy t -> DLType

instance KnownDLType Int32 where getType :: Proxy Int32 -> DLType
getType = DLType -> Proxy Int32 -> DLType
forall a b. a -> b -> a
const DLType
DLNumber
instance KnownDLType Word32 where getType :: Proxy Word32 -> DLType
getType = DLType -> Proxy Word32 -> DLType
forall a b. a -> b -> a
const DLType
DLUnsigned
instance KnownDLType Float where getType :: Proxy Float -> DLType
getType = DLType -> Proxy Float -> DLType
forall a b. a -> b -> a
const DLType
DLFloat
instance KnownDLType String where getType :: Proxy FilePath -> DLType
getType = DLType -> Proxy FilePath -> DLType
forall a b. a -> b -> a
const DLType
DLString
instance KnownDLType T.Text where getType :: Proxy VarName -> DLType
getType = DLType -> Proxy VarName -> DLType
forall a b. a -> b -> a
const DLType
DLString
instance KnownDLType TL.Text where getType :: Proxy Text -> DLType
getType = DLType -> Proxy Text -> DLType
forall a b. a -> b -> a
const DLType
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 :: Proxy '[] -> [FilePath]
toStrings = [FilePath] -> Proxy '[] -> [FilePath]
forall a b. a -> b -> a
const []

instance (KnownSymbol s, KnownSymbols symbols) => KnownSymbols (s ': symbols) where
  toStrings :: Proxy (s : symbols) -> [FilePath]
toStrings _ =
    let sym :: FilePath
sym = Proxy s -> FilePath
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> FilePath
symbolVal (Proxy s
forall k (t :: k). Proxy t
Proxy :: Proxy s)
        symbols :: [FilePath]
symbols =  Proxy symbols -> [FilePath]
forall (symbols :: [Symbol]).
KnownSymbols symbols =>
Proxy symbols -> [FilePath]
toStrings (Proxy symbols
forall k (t :: k). Proxy t
Proxy :: Proxy symbols)
     in FilePath
sym FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
: [FilePath]
symbols

accessorNames :: forall a. KnownSymbols (AccessorNames a) => Proxy a -> Maybe [T.Text]
accessorNames :: Proxy a -> Maybe [VarName]
accessorNames _ = case Proxy (GetAccessorNames (Rep a)) -> [FilePath]
forall (symbols :: [Symbol]).
KnownSymbols symbols =>
Proxy symbols -> [FilePath]
toStrings (Proxy (AccessorNames a)
forall k (t :: k). Proxy t
Proxy :: Proxy (AccessorNames a)) of
  [] -> Maybe [VarName]
forall a. Maybe a
Nothing
  names :: [FilePath]
names -> [VarName] -> Maybe [VarName]
forall a. a -> Maybe a
Just ([VarName] -> Maybe [VarName]) -> [VarName] -> Maybe [VarName]
forall a b. (a -> b) -> a -> b
$ FilePath -> VarName
T.pack (FilePath -> VarName) -> [FilePath] -> [VarName]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [FilePath]
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 :: Proxy ctx
-> TypeInfo a '[t] -> Tuple ctx '[t] -> NonEmpty SimpleTerm
toTerms _ _ a :: Tuple ctx '[t]
a =
    Term ctx t -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Tuple ctx '[t]
Term ctx t
a SimpleTerm -> [SimpleTerm] -> NonEmpty SimpleTerm
forall a. a -> [a] -> NonEmpty a
:| []

instance ToTerms '[t1, t2] where
  toTerms :: Proxy ctx
-> TypeInfo a '[t1, t2]
-> Tuple ctx '[t1, t2]
-> NonEmpty SimpleTerm
toTerms _ _ (a, b) =
    Term ctx t1 -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx t1
a SimpleTerm -> [SimpleTerm] -> NonEmpty SimpleTerm
forall a. a -> [a] -> NonEmpty a
:| [Term ctx t2 -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx t2
b]

instance ToTerms '[t1, t2, t3] where
  toTerms :: Proxy ctx
-> TypeInfo a '[t1, t2, t3]
-> Tuple ctx '[t1, t2, t3]
-> NonEmpty SimpleTerm
toTerms _ _ (a, b, c) =
    Term ctx t1 -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx t1
a SimpleTerm -> [SimpleTerm] -> NonEmpty SimpleTerm
forall a. a -> [a] -> NonEmpty a
:| [Term ctx t2 -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx t2
b, Term ctx t3 -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx t3
c]

instance ToTerms '[t1, t2, t3, t4] where
  toTerms :: Proxy ctx
-> TypeInfo a '[t1, t2, t3, t4]
-> Tuple ctx '[t1, t2, t3, t4]
-> NonEmpty SimpleTerm
toTerms _ _ (a, b, c, d) =
    Term ctx t1 -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx t1
a SimpleTerm -> [SimpleTerm] -> NonEmpty SimpleTerm
forall a. a -> [a] -> NonEmpty a
:| [Term ctx t2 -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx t2
b, Term ctx t3 -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx t3
c, Term ctx t4 -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx t4
d]

instance ToTerms '[t1, t2, t3, t4, t5] where
  toTerms :: Proxy ctx
-> TypeInfo a '[t1, t2, t3, t4, t5]
-> Tuple ctx '[t1, t2, t3, t4, t5]
-> NonEmpty SimpleTerm
toTerms _ _ (a, b, c, d, e) =
    Term ctx t1 -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx t1
a SimpleTerm -> [SimpleTerm] -> NonEmpty SimpleTerm
forall a. a -> [a] -> NonEmpty a
:| [Term ctx t2 -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx t2
b, Term ctx t3 -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx t3
c, Term ctx t4 -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx t4
d, Term ctx t5 -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx t5
e]

instance ToTerms '[t1, t2, t3, t4, t5, t6] where
  toTerms :: Proxy ctx
-> TypeInfo a '[t1, t2, t3, t4, t5, t6]
-> Tuple ctx '[t1, t2, t3, t4, t5, t6]
-> NonEmpty SimpleTerm
toTerms _ _ (a, b, c, d, e, f) =
    Term ctx t1 -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx t1
a SimpleTerm -> [SimpleTerm] -> NonEmpty SimpleTerm
forall a. a -> [a] -> NonEmpty a
:| [Term ctx t2 -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx t2
b, Term ctx t3 -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx t3
c, Term ctx t4 -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx t4
d, Term ctx t5 -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx t5
e, Term ctx t6 -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx t6
f]

instance ToTerms '[t1, t2, t3, t4, t5, t6, t7] where
  toTerms :: Proxy ctx
-> TypeInfo a '[t1, t2, t3, t4, t5, t6, t7]
-> Tuple ctx '[t1, t2, t3, t4, t5, t6, t7]
-> NonEmpty SimpleTerm
toTerms _ _ (a, b, c, d, e, f, g) =
    Term ctx t1 -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx t1
a SimpleTerm -> [SimpleTerm] -> NonEmpty SimpleTerm
forall a. a -> [a] -> NonEmpty a
:| [Term ctx t2 -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx t2
b, Term ctx t3 -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx t3
c, Term ctx t4 -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx t4
d, Term ctx t5 -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx t5
e, Term ctx t6 -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx t6
f, Term ctx t7 -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx t7
g]

instance ToTerms '[t1, t2, t3, t4, t5, t6, t7, t8] where
  toTerms :: Proxy ctx
-> TypeInfo a '[t1, t2, t3, t4, t5, t6, t7, t8]
-> Tuple ctx '[t1, t2, t3, t4, t5, t6, t7, t8]
-> NonEmpty SimpleTerm
toTerms _ _ (a, b, c, d, e, f, g, h) =
    Term ctx t1 -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx t1
a SimpleTerm -> [SimpleTerm] -> NonEmpty SimpleTerm
forall a. a -> [a] -> NonEmpty a
:| [Term ctx t2 -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx t2
b, Term ctx t3 -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx t3
c, Term ctx t4 -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx t4
d, Term ctx t5 -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx t5
e, Term ctx t6 -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx t6
f, Term ctx t7 -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx t7
g, Term ctx t8 -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx t8
h]

instance ToTerms '[t1, t2, t3, t4, t5, t6, t7, t8, t9] where
  toTerms :: Proxy ctx
-> TypeInfo a '[t1, t2, t3, t4, t5, t6, t7, t8, t9]
-> Tuple ctx '[t1, t2, t3, t4, t5, t6, t7, t8, t9]
-> NonEmpty SimpleTerm
toTerms _ _ (a, b, c, d, e, f, g, h, i) =
    Term ctx t1 -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx t1
a SimpleTerm -> [SimpleTerm] -> NonEmpty SimpleTerm
forall a. a -> [a] -> NonEmpty a
:| [Term ctx t2 -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx t2
b, Term ctx t3 -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx t3
c, Term ctx t4 -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx t4
d, Term ctx t5 -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx t5
e, Term ctx t6 -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx t6
f, Term ctx t7 -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx t7
g, Term ctx t8 -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx t8
h, Term ctx t9 -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx t9
i]

instance ToTerms '[t1, t2, t3, t4, t5, t6, t7, t8, t9, t10] where
  toTerms :: Proxy ctx
-> TypeInfo a '[t1, t2, t3, t4, t5, t6, t7, t8, t9, t10]
-> Tuple ctx '[t1, t2, t3, t4, t5, t6, t7, t8, t9, t10]
-> NonEmpty SimpleTerm
toTerms _ _ (a, b, c, d, e, f, g, h, i, j) =
    Term ctx t1 -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx t1
a SimpleTerm -> [SimpleTerm] -> NonEmpty SimpleTerm
forall a. a -> [a] -> NonEmpty a
:| [ Term ctx t2 -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx t2
b, Term ctx t3 -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx t3
c, Term ctx t4 -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx t4
d, Term ctx t5 -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx t5
e, Term ctx t6 -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx t6
f
                , Term ctx t7 -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx t7
g, Term ctx t8 -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx t8
h, Term ctx t9 -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx t9
i, Term ctx t10 -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx t10
j
                ]

toTerm :: Term ctx t -> SimpleTerm
toTerm :: Term ctx t -> SimpleTerm
toTerm = \case
  VarTerm v :: VarName
v -> VarName -> SimpleTerm
V VarName
v
  StringTerm s :: t
s -> FilePath -> SimpleTerm
S (FilePath -> SimpleTerm) -> FilePath -> SimpleTerm
forall a b. (a -> b) -> a -> b
$ t -> FilePath
forall a. ToString a => a -> FilePath
toString t
s
  NumberTerm x :: Int32
x -> Int32 -> SimpleTerm
I Int32
x
  UnsignedTerm x :: Word32
x -> Word32 -> SimpleTerm
U Word32
x
  FloatTerm x :: Float
x -> Float -> SimpleTerm
F Float
x
  UnderscoreTerm -> SimpleTerm
Underscore

  BinOp op :: Op2
op t1 :: Term ctx t
t1 t2 :: Term ctx t
t2 -> Op2 -> SimpleTerm -> SimpleTerm -> SimpleTerm
BinOp' Op2
op (Term ctx t -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx t
t1) (Term ctx t -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx t
t2)
  UnaryOp op :: Op1
op t1 :: Term ctx t
t1 -> Op1 -> SimpleTerm -> SimpleTerm
UnaryOp' Op1
op (Term ctx t -> SimpleTerm
forall (ctx :: UsageContext) t. Term ctx t -> SimpleTerm
toTerm Term ctx t
t1)
  Func name :: FuncName
name ts :: NonEmpty SimpleTerm
ts -> FuncName -> NonEmpty SimpleTerm -> SimpleTerm
Func' FuncName
name NonEmpty SimpleTerm
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)"
  )