{-# LANGUAGE DataKinds                  #-}
{-# LANGUAGE DerivingStrategies         #-}
{-# LANGUAGE FlexibleContexts           #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase                 #-}
{-# LANGUAGE NamedFieldPuns             #-}
{-# LANGUAGE OverloadedStrings          #-}
{-# LANGUAGE TupleSections              #-}
{-|
  Module      : Auth.Biscuit.Datalog.Executor
  Copyright   : © Clément Delafargue, 2021
  License     : MIT
  Maintainer  : clement@delafargue.name
  The Datalog engine, tasked with deriving new facts from existing facts and rules, as well as matching available facts against checks and policies
-}
module Auth.Biscuit.Datalog.Executor
  ( ExecutionError (..)
  , Limits (..)
  , ResultError (..)
  , Bindings
  , Name
  , MatchedQuery (..)
  , Scoped
  , FactGroup (..)
  , countFacts
  , toScopedFacts
  , fromScopedFacts
  , keepAuthorized'
  , defaultLimits
  , evaluateExpression
  --
  , getFactsForRule
  , checkCheck
  , checkPolicy
  , getBindingsForRuleBody
  , getCombinations
  ) where

import           Control.Monad            (join, mfilter, zipWithM)
import           Data.Bitraversable       (bitraverse)
import           Data.Bits                (xor, (.&.), (.|.))
import qualified Data.ByteString          as ByteString
import           Data.Foldable            (fold)
import           Data.Functor.Compose     (Compose (..))
import           Data.List.NonEmpty       (NonEmpty)
import qualified Data.List.NonEmpty       as NE
import           Data.Map.Strict          (Map, (!?))
import qualified Data.Map.Strict          as Map
import           Data.Maybe               (isJust, mapMaybe)
import           Data.Set                 (Set)
import qualified Data.Set                 as Set
import           Data.Text                (Text, isInfixOf, unpack)
import qualified Data.Text                as Text
import           Data.Void                (absurd)
import           Numeric.Natural          (Natural)
import qualified Text.Regex.TDFA          as Regex
import qualified Text.Regex.TDFA.Text     as Regex
import           Validation               (Validation (..), failure)

import           Auth.Biscuit.Datalog.AST
import           Auth.Biscuit.Utils       (maybeToRight)

-- | A variable name
type Name = Text

-- | A list of bound variables, with the associated value
type Bindings  = Map Name Value

-- | A datalog query that was matched, along with the values
-- that matched
data MatchedQuery
  = MatchedQuery
  { MatchedQuery -> Query
matchedQuery :: Query
  , MatchedQuery -> Set Bindings
bindings     :: Set Bindings
  }
  deriving (MatchedQuery -> MatchedQuery -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: MatchedQuery -> MatchedQuery -> Bool
$c/= :: MatchedQuery -> MatchedQuery -> Bool
== :: MatchedQuery -> MatchedQuery -> Bool
$c== :: MatchedQuery -> MatchedQuery -> Bool
Eq, Int -> MatchedQuery -> ShowS
[MatchedQuery] -> ShowS
MatchedQuery -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [MatchedQuery] -> ShowS
$cshowList :: [MatchedQuery] -> ShowS
show :: MatchedQuery -> String
$cshow :: MatchedQuery -> String
showsPrec :: Int -> MatchedQuery -> ShowS
$cshowsPrec :: Int -> MatchedQuery -> ShowS
Show)

-- | The result of matching the checks and policies against all the available
-- facts.
data ResultError
  = NoPoliciesMatched [Check]
  -- ^ No policy matched. additionally some checks may have failed
  | FailedChecks      (NonEmpty Check)
  -- ^ An allow rule matched, but at least one check failed
  | DenyRuleMatched   [Check] MatchedQuery
  -- ^ A deny rule matched. additionally some checks may have failed
  deriving (ResultError -> ResultError -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ResultError -> ResultError -> Bool
$c/= :: ResultError -> ResultError -> Bool
== :: ResultError -> ResultError -> Bool
$c== :: ResultError -> ResultError -> Bool
Eq, Int -> ResultError -> ShowS
[ResultError] -> ShowS
ResultError -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ResultError] -> ShowS
$cshowList :: [ResultError] -> ShowS
show :: ResultError -> String
$cshow :: ResultError -> String
showsPrec :: Int -> ResultError -> ShowS
$cshowsPrec :: Int -> ResultError -> ShowS
Show)

-- | An error that can happen while running a datalog verification.
-- The datalog computation itself can be aborted by runtime failsafe
-- mechanisms, or it can run to completion but fail to fullfil checks
-- and policies ('ResultError').
data ExecutionError
  = Timeout
  -- ^ Verification took too much time
  | TooManyFacts
  -- ^ Too many facts were generated during evaluation
  | TooManyIterations
  -- ^ Evaluation did not converge in the alloted number of iterations
  | InvalidRule
  -- ^ Some rules were malformed: every variable present in their head must
  -- appear in their body
  | ResultError ResultError
  -- ^ The evaluation ran to completion, but checks and policies were not
  -- fulfilled.
  deriving (ExecutionError -> ExecutionError -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ExecutionError -> ExecutionError -> Bool
$c/= :: ExecutionError -> ExecutionError -> Bool
== :: ExecutionError -> ExecutionError -> Bool
$c== :: ExecutionError -> ExecutionError -> Bool
Eq, Int -> ExecutionError -> ShowS
[ExecutionError] -> ShowS
ExecutionError -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ExecutionError] -> ShowS
$cshowList :: [ExecutionError] -> ShowS
show :: ExecutionError -> String
$cshow :: ExecutionError -> String
showsPrec :: Int -> ExecutionError -> ShowS
$cshowsPrec :: Int -> ExecutionError -> ShowS
Show)

-- | Settings for the executor runtime restrictions.
-- See `defaultLimits` for default values.
data Limits
  = Limits
  { Limits -> Int
maxFacts      :: Int
  -- ^ maximum number of facts that can be produced before throwing `TooManyFacts`
  , Limits -> Int
maxIterations :: Int
  -- ^ maximum number of iterations before throwing `TooManyIterations`
  , Limits -> Int
maxTime       :: Int
  -- ^ maximum duration the verification can take (in μs)
  , Limits -> Bool
allowRegexes  :: Bool
  -- ^ whether or not allowing `.matches()` during verification (untrusted regex computation
  -- can enable DoS attacks). This security risk is mitigated by the 'maxTime' setting.
  }
  deriving (Limits -> Limits -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Limits -> Limits -> Bool
$c/= :: Limits -> Limits -> Bool
== :: Limits -> Limits -> Bool
$c== :: Limits -> Limits -> Bool
Eq, Int -> Limits -> ShowS
[Limits] -> ShowS
Limits -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Limits] -> ShowS
$cshowList :: [Limits] -> ShowS
show :: Limits -> String
$cshow :: Limits -> String
showsPrec :: Int -> Limits -> ShowS
$cshowsPrec :: Int -> Limits -> ShowS
Show)

-- | Default settings for the executor restrictions.
--   - 1000 facts
--   - 100 iterations
--   - 1000μs max
--   - regexes are allowed
--   - facts and rules are allowed in blocks
defaultLimits :: Limits
defaultLimits :: Limits
defaultLimits = Limits
  { maxFacts :: Int
maxFacts = Int
1000
  , maxIterations :: Int
maxIterations = Int
100
  , maxTime :: Int
maxTime = Int
1000
  , allowRegexes :: Bool
allowRegexes = Bool
True
  }

type Scoped a = (Set Natural, a)

newtype FactGroup = FactGroup { FactGroup -> Map (Set Natural) (Set Fact)
getFactGroup :: Map (Set Natural) (Set Fact) }
  deriving newtype (FactGroup -> FactGroup -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: FactGroup -> FactGroup -> Bool
$c/= :: FactGroup -> FactGroup -> Bool
== :: FactGroup -> FactGroup -> Bool
$c== :: FactGroup -> FactGroup -> Bool
Eq)

instance Show FactGroup where
  show :: FactGroup -> String
show (FactGroup Map (Set Natural) (Set Fact)
groups) =
    let showGroup :: (Set a, Set Fact) -> String
showGroup (Set a
origin, Set Fact
facts) = [String] -> String
unlines
          [ String
"For origin: " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> String
show (forall a. Set a -> [a]
Set.toList Set a
origin)
          , String
"Facts: \n" forall a. Semigroup a => a -> a -> a
<> [String] -> String
unlines (Text -> String
unpack forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fact -> Text
renderFact forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Set a -> [a]
Set.toList Set Fact
facts)
          ]
     in [String] -> String
unlines forall a b. (a -> b) -> a -> b
$ forall {a}. Show a => (Set a, Set Fact) -> String
showGroup forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k a. Map k a -> [(k, a)]
Map.toList Map (Set Natural) (Set Fact)
groups

instance Semigroup FactGroup where
  FactGroup Map (Set Natural) (Set Fact)
f1 <> :: FactGroup -> FactGroup -> FactGroup
<> FactGroup Map (Set Natural) (Set Fact)
f2 = Map (Set Natural) (Set Fact) -> FactGroup
FactGroup forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith forall a. Semigroup a => a -> a -> a
(<>) Map (Set Natural) (Set Fact)
f1 Map (Set Natural) (Set Fact)
f2
instance Monoid FactGroup where
  mempty :: FactGroup
mempty = Map (Set Natural) (Set Fact) -> FactGroup
FactGroup forall a. Monoid a => a
mempty

keepAuthorized :: FactGroup -> Set Natural -> FactGroup
keepAuthorized :: FactGroup -> Set Natural -> FactGroup
keepAuthorized (FactGroup Map (Set Natural) (Set Fact)
facts) Set Natural
authorizedOrigins =
  let isAuthorized :: Set Natural -> p -> Bool
isAuthorized Set Natural
k p
_ = Set Natural
k forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` Set Natural
authorizedOrigins
   in Map (Set Natural) (Set Fact) -> FactGroup
FactGroup forall a b. (a -> b) -> a -> b
$ forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey forall {p}. Set Natural -> p -> Bool
isAuthorized Map (Set Natural) (Set Fact)
facts

keepAuthorized' :: Bool -> Natural -> FactGroup -> Set EvalRuleScope -> Natural -> FactGroup
keepAuthorized' :: Bool
-> Natural
-> FactGroup
-> Set EvalRuleScope
-> Natural
-> FactGroup
keepAuthorized' Bool
allowPreviousInAuthorizer Natural
blockCount FactGroup
factGroup Set EvalRuleScope
trustedBlocks Natural
currentBlockId =
  let scope :: Set EvalRuleScope
scope = if forall (t :: * -> *) a. Foldable t => t a -> Bool
null Set EvalRuleScope
trustedBlocks then forall a. a -> Set a
Set.singleton forall (evalCtx :: EvaluationContext) (ctx :: DatalogContext).
RuleScope' evalCtx ctx
OnlyAuthority
                                    else Set EvalRuleScope
trustedBlocks
      toBlockIds :: EvalRuleScope -> Set Natural
toBlockIds = \case
        EvalRuleScope
OnlyAuthority    -> forall a. a -> Set a
Set.singleton Natural
0
        EvalRuleScope
Previous         -> if Bool
allowPreviousInAuthorizer Bool -> Bool -> Bool
|| Natural
currentBlockId forall a. Ord a => a -> a -> Bool
< Natural
blockCount
                            then forall a. Ord a => [a] -> Set a
Set.fromList [Natural
0..Natural
currentBlockId]
                            else forall a. Monoid a => a
mempty -- `Previous` is forbidden in the authorizer
                                        -- except when querying the authorizer contents
                                        -- after authorization
        BlockId (Set Natural
idx, PublicKey
_) -> Set Natural
idx
      allBlockIds :: Set Natural
allBlockIds = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap EvalRuleScope -> Set Natural
toBlockIds Set EvalRuleScope
scope
   in FactGroup -> Set Natural -> FactGroup
keepAuthorized FactGroup
factGroup forall a b. (a -> b) -> a -> b
$ forall a. Ord a => a -> Set a -> Set a
Set.insert Natural
currentBlockId forall a b. (a -> b) -> a -> b
$ forall a. Ord a => a -> Set a -> Set a
Set.insert Natural
blockCount Set Natural
allBlockIds

toScopedFacts :: FactGroup -> Set (Scoped Fact)
toScopedFacts :: FactGroup -> Set (Scoped Fact)
toScopedFacts (FactGroup Map (Set Natural) (Set Fact)
factGroups) =
  let distributeScope :: t -> Set a -> Set (t, a)
distributeScope t
scope = forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (t
scope,)
   in forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall {t} {a}. (Ord t, Ord a) => t -> Set a -> Set (t, a)
distributeScope) forall a b. (a -> b) -> a -> b
$ forall k a. Map k a -> [(k, a)]
Map.toList Map (Set Natural) (Set Fact)
factGroups

fromScopedFacts :: Set (Scoped Fact) -> FactGroup
fromScopedFacts :: Set (Scoped Fact) -> FactGroup
fromScopedFacts = Map (Set Natural) (Set Fact) -> FactGroup
FactGroup forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith forall a. Semigroup a => a -> a -> a
(<>) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> [a]
Set.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. a -> Set a
Set.singleton)

countFacts :: FactGroup -> Int
countFacts :: FactGroup -> Int
countFacts (FactGroup Map (Set Natural) (Set Fact)
facts) = forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum forall a b. (a -> b) -> a -> b
$ forall a. Set a -> Int
Set.size forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall k a. Map k a -> [a]
Map.elems Map (Set Natural) (Set Fact)
facts

-- todo handle Check All
checkCheck :: Limits -> Natural -> Natural -> FactGroup -> EvalCheck -> Validation (NonEmpty Check) ()
checkCheck :: Limits
-> Natural
-> Natural
-> FactGroup
-> EvalCheck
-> Validation (NonEmpty Check) ()
checkCheck Limits
l Natural
blockCount Natural
checkBlockId FactGroup
facts c :: EvalCheck
c@Check{Query' 'Eval 'Representation
cQueries :: forall (evalCtx :: EvaluationContext) (ctx :: DatalogContext).
Check' evalCtx ctx -> Query' evalCtx ctx
cQueries :: Query' 'Eval 'Representation
cQueries,CheckKind
cKind :: forall (evalCtx :: EvaluationContext) (ctx :: DatalogContext).
Check' evalCtx ctx -> CheckKind
cKind :: CheckKind
cKind} =
  let isQueryItemOk :: QueryItem' 'Eval 'Representation -> Maybe (Set Bindings)
isQueryItemOk = case CheckKind
cKind of
        CheckKind
One -> Limits
-> Natural
-> Natural
-> FactGroup
-> QueryItem' 'Eval 'Representation
-> Maybe (Set Bindings)
isQueryItemSatisfied Limits
l Natural
blockCount Natural
checkBlockId FactGroup
facts
        CheckKind
All -> Limits
-> Natural
-> Natural
-> FactGroup
-> QueryItem' 'Eval 'Representation
-> Maybe (Set Bindings)
isQueryItemSatisfiedForAllMatches Limits
l Natural
blockCount Natural
checkBlockId FactGroup
facts
   in if forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall a. Maybe a -> Bool
isJust forall b c a. (b -> c) -> (a -> b) -> a -> c
. QueryItem' 'Eval 'Representation -> Maybe (Set Bindings)
isQueryItemOk) Query' 'Eval 'Representation
cQueries
      then forall e a. a -> Validation e a
Success ()
      else forall e a. e -> Validation (NonEmpty e) a
failure (forall (elem :: EvaluationContext -> DatalogContext -> *).
ToEvaluation elem =>
elem 'Eval 'Representation -> elem 'Repr 'Representation
toRepresentation EvalCheck
c)

checkPolicy :: Limits -> Natural -> FactGroup -> EvalPolicy -> Maybe (Either MatchedQuery MatchedQuery)
checkPolicy :: Limits
-> Natural
-> FactGroup
-> EvalPolicy
-> Maybe (Either MatchedQuery MatchedQuery)
checkPolicy Limits
l Natural
blockCount FactGroup
facts (PolicyType
pType, Query' 'Eval 'Representation
query) =
  let bindings :: Set Bindings
bindings = forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold forall a b. (a -> b) -> a -> b
$ forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Limits
-> Natural
-> Natural
-> FactGroup
-> QueryItem' 'Eval 'Representation
-> Maybe (Set Bindings)
isQueryItemSatisfied Limits
l Natural
blockCount Natural
blockCount FactGroup
facts) Query' 'Eval 'Representation
query
   in if Bool -> Bool
not (forall (t :: * -> *) a. Foldable t => t a -> Bool
null Set Bindings
bindings)
      then forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ case PolicyType
pType of
        PolicyType
Allow -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ MatchedQuery{matchedQuery :: Query
matchedQuery = forall (elem :: EvaluationContext -> DatalogContext -> *).
ToEvaluation elem =>
elem 'Eval 'Representation -> elem 'Repr 'Representation
toRepresentation forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Query' 'Eval 'Representation
query, Set Bindings
bindings :: Set Bindings
bindings :: Set Bindings
bindings}
        PolicyType
Deny  -> forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ MatchedQuery{matchedQuery :: Query
matchedQuery = forall (elem :: EvaluationContext -> DatalogContext -> *).
ToEvaluation elem =>
elem 'Eval 'Representation -> elem 'Repr 'Representation
toRepresentation forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Query' 'Eval 'Representation
query, Set Bindings
bindings :: Set Bindings
bindings :: Set Bindings
bindings}
      else forall a. Maybe a
Nothing

isQueryItemSatisfied :: Limits -> Natural -> Natural -> FactGroup -> QueryItem' 'Eval 'Representation -> Maybe (Set Bindings)
isQueryItemSatisfied :: Limits
-> Natural
-> Natural
-> FactGroup
-> QueryItem' 'Eval 'Representation
-> Maybe (Set Bindings)
isQueryItemSatisfied Limits
l Natural
blockCount Natural
blockId FactGroup
allFacts QueryItem{[Predicate' 'InPredicate 'Representation]
qBody :: forall (evalCtx :: EvaluationContext) (ctx :: DatalogContext).
QueryItem' evalCtx ctx -> [Predicate' 'InPredicate ctx]
qBody :: [Predicate' 'InPredicate 'Representation]
qBody, [Expression]
qExpressions :: forall (evalCtx :: EvaluationContext) (ctx :: DatalogContext).
QueryItem' evalCtx ctx -> [Expression' ctx]
qExpressions :: [Expression]
qExpressions, Set EvalRuleScope
qScope :: forall (evalCtx :: EvaluationContext) (ctx :: DatalogContext).
QueryItem' evalCtx ctx -> Set (RuleScope' evalCtx ctx)
qScope :: Set EvalRuleScope
qScope} =
  let removeScope :: Set (a, Bindings) -> Set Bindings
removeScope = forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map forall a b. (a, b) -> b
snd
      facts :: Set (Scoped Fact)
facts = FactGroup -> Set (Scoped Fact)
toScopedFacts forall a b. (a -> b) -> a -> b
$ Bool
-> Natural
-> FactGroup
-> Set EvalRuleScope
-> Natural
-> FactGroup
keepAuthorized' Bool
False Natural
blockCount FactGroup
allFacts Set EvalRuleScope
qScope Natural
blockId
      bindings :: Set Bindings
bindings = forall {a}. Set (a, Bindings) -> Set Bindings
removeScope forall a b. (a -> b) -> a -> b
$ Limits
-> Set (Scoped Fact)
-> [Predicate' 'InPredicate 'Representation]
-> [Expression]
-> Set (Scoped Bindings)
getBindingsForRuleBody Limits
l Set (Scoped Fact)
facts [Predicate' 'InPredicate 'Representation]
qBody [Expression]
qExpressions
   in if forall a. Set a -> Int
Set.size Set Bindings
bindings forall a. Ord a => a -> a -> Bool
> Int
0
      then forall a. a -> Maybe a
Just Set Bindings
bindings
      else forall a. Maybe a
Nothing

-- | Given a set of scoped facts and a rule body, we generate a set of variable
-- bindings that satisfy the rule clauses (predicates match, and expression constraints
-- are fulfilled), and ensure that all bindings where predicates match also fulfill
-- expression constraints. This is the behaviour of `check all`.
isQueryItemSatisfiedForAllMatches :: Limits -> Natural -> Natural -> FactGroup -> QueryItem' 'Eval 'Representation -> Maybe (Set Bindings)
isQueryItemSatisfiedForAllMatches :: Limits
-> Natural
-> Natural
-> FactGroup
-> QueryItem' 'Eval 'Representation
-> Maybe (Set Bindings)
isQueryItemSatisfiedForAllMatches Limits
l Natural
blockCount Natural
blockId FactGroup
allFacts QueryItem{[Predicate' 'InPredicate 'Representation]
qBody :: [Predicate' 'InPredicate 'Representation]
qBody :: forall (evalCtx :: EvaluationContext) (ctx :: DatalogContext).
QueryItem' evalCtx ctx -> [Predicate' 'InPredicate ctx]
qBody, [Expression]
qExpressions :: [Expression]
qExpressions :: forall (evalCtx :: EvaluationContext) (ctx :: DatalogContext).
QueryItem' evalCtx ctx -> [Expression' ctx]
qExpressions, Set EvalRuleScope
qScope :: Set EvalRuleScope
qScope :: forall (evalCtx :: EvaluationContext) (ctx :: DatalogContext).
QueryItem' evalCtx ctx -> Set (RuleScope' evalCtx ctx)
qScope} =
  let removeScope :: Set (a, Bindings) -> Set Bindings
removeScope = forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map forall a b. (a, b) -> b
snd
      facts :: Set (Scoped Fact)
facts = FactGroup -> Set (Scoped Fact)
toScopedFacts forall a b. (a -> b) -> a -> b
$ Bool
-> Natural
-> FactGroup
-> Set EvalRuleScope
-> Natural
-> FactGroup
keepAuthorized' Bool
False Natural
blockCount FactGroup
allFacts Set EvalRuleScope
qScope Natural
blockId
      allVariables :: Set Text
allVariables = forall (ctx :: DatalogContext).
[Predicate' 'InPredicate ctx] -> Set Text
extractVariables [Predicate' 'InPredicate 'Representation]
qBody
      -- bindings that match facts
      candidateBindings :: [Set (Scoped Bindings)]
candidateBindings = Set (Scoped Fact)
-> [Predicate' 'InPredicate 'Representation]
-> [Set (Scoped Bindings)]
getCandidateBindings Set (Scoped Fact)
facts [Predicate' 'InPredicate 'Representation]
qBody
      -- bindings that unify correctly (each variable has a single possible match)
      legalBindingsForFacts :: Set (Scoped Bindings)
legalBindingsForFacts = Set Text -> [Set (Scoped Bindings)] -> Set (Scoped Bindings)
reduceCandidateBindings Set Text
allVariables [Set (Scoped Bindings)]
candidateBindings
      -- bindings that fulfill the constraints
      constraintFulfillingBindings :: Set (Scoped Bindings)
constraintFulfillingBindings = forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\Scoped Bindings
b -> forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Limits -> Scoped Bindings -> Expression -> Bool
satisfies Limits
l Scoped Bindings
b) [Expression]
qExpressions) Set (Scoped Bindings)
legalBindingsForFacts
   in if forall a. Set a -> Int
Set.size Set (Scoped Bindings)
constraintFulfillingBindings forall a. Ord a => a -> a -> Bool
> Int
0 -- there is at least one match that fulfills the constraints
      Bool -> Bool -> Bool
&& Set (Scoped Bindings)
constraintFulfillingBindings forall a. Eq a => a -> a -> Bool
== Set (Scoped Bindings)
legalBindingsForFacts -- all matches fulfill the constraints
      then forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall {a}. Set (a, Bindings) -> Set Bindings
removeScope Set (Scoped Bindings)
constraintFulfillingBindings
      else forall a. Maybe a
Nothing

-- | Given a rule and a set of available (scoped) facts, we find all fact
-- combinations that match the rule body, and generate new facts by applying
-- the bindings to the rule head (while keeping track of the facts origins)
getFactsForRule :: Limits -> Set (Scoped Fact) -> EvalRule -> Set (Scoped Fact)
getFactsForRule :: Limits -> Set (Scoped Fact) -> EvalRule -> Set (Scoped Fact)
getFactsForRule Limits
l Set (Scoped Fact)
facts Rule{Predicate' 'InPredicate 'Representation
rhead :: forall (evalCtx :: EvaluationContext) (ctx :: DatalogContext).
Rule' evalCtx ctx -> Predicate' 'InPredicate ctx
rhead :: Predicate' 'InPredicate 'Representation
rhead, [Predicate' 'InPredicate 'Representation]
body :: forall (evalCtx :: EvaluationContext) (ctx :: DatalogContext).
Rule' evalCtx ctx -> [Predicate' 'InPredicate ctx]
body :: [Predicate' 'InPredicate 'Representation]
body, [Expression]
expressions :: forall (evalCtx :: EvaluationContext) (ctx :: DatalogContext).
Rule' evalCtx ctx -> [Expression' ctx]
expressions :: [Expression]
expressions} =
  let legalBindings :: Set (Scoped Bindings)
      legalBindings :: Set (Scoped Bindings)
legalBindings = Limits
-> Set (Scoped Fact)
-> [Predicate' 'InPredicate 'Representation]
-> [Expression]
-> Set (Scoped Bindings)
getBindingsForRuleBody Limits
l Set (Scoped Fact)
facts [Predicate' 'InPredicate 'Representation]
body [Expression]
expressions
      newFacts :: [Scoped Fact]
newFacts = forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Predicate' 'InPredicate 'Representation
-> Scoped Bindings -> Maybe (Scoped Fact)
applyBindings Predicate' 'InPredicate 'Representation
rhead) forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList Set (Scoped Bindings)
legalBindings
   in forall a. Ord a => [a] -> Set a
Set.fromList [Scoped Fact]
newFacts

-- | Given a set of scoped facts and a rule body, we generate a set of variable
-- bindings that satisfy the rule clauses (predicates match, and expression constraints
-- are fulfilled)
getBindingsForRuleBody :: Limits -> Set (Scoped Fact) -> [Predicate] -> [Expression] -> Set (Scoped Bindings)
getBindingsForRuleBody :: Limits
-> Set (Scoped Fact)
-> [Predicate' 'InPredicate 'Representation]
-> [Expression]
-> Set (Scoped Bindings)
getBindingsForRuleBody Limits
l Set (Scoped Fact)
facts [Predicate' 'InPredicate 'Representation]
body [Expression]
expressions =
  let -- gather bindings from all the facts that match the query's predicates
      candidateBindings :: [Set (Scoped Bindings)]
candidateBindings = Set (Scoped Fact)
-> [Predicate' 'InPredicate 'Representation]
-> [Set (Scoped Bindings)]
getCandidateBindings Set (Scoped Fact)
facts [Predicate' 'InPredicate 'Representation]
body
      allVariables :: Set Text
allVariables = forall (ctx :: DatalogContext).
[Predicate' 'InPredicate ctx] -> Set Text
extractVariables [Predicate' 'InPredicate 'Representation]
body
      -- only keep bindings combinations where each variable has a single possible match
      legalBindingsForFacts :: Set (Scoped Bindings)
legalBindingsForFacts = Set Text -> [Set (Scoped Bindings)] -> Set (Scoped Bindings)
reduceCandidateBindings Set Text
allVariables [Set (Scoped Bindings)]
candidateBindings
      -- only keep bindings that satisfy the query expressions
   in forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\Scoped Bindings
b -> forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Limits -> Scoped Bindings -> Expression -> Bool
satisfies Limits
l Scoped Bindings
b) [Expression]
expressions) Set (Scoped Bindings)
legalBindingsForFacts

satisfies :: Limits
          -> Scoped Bindings
          -> Expression
          -> Bool
satisfies :: Limits -> Scoped Bindings -> Expression -> Bool
satisfies Limits
l Scoped Bindings
b Expression
e = Limits -> Bindings -> Expression -> Either String Value
evaluateExpression Limits
l (forall a b. (a, b) -> b
snd Scoped Bindings
b) Expression
e forall a. Eq a => a -> a -> Bool
== forall a b. b -> Either a b
Right (forall (inSet :: IsWithinSet) (pof :: PredicateOrFact)
       (ctx :: DatalogContext).
Bool -> Term' inSet pof ctx
LBool Bool
True)

applyBindings :: Predicate -> Scoped Bindings -> Maybe (Scoped Fact)
applyBindings :: Predicate' 'InPredicate 'Representation
-> Scoped Bindings -> Maybe (Scoped Fact)
applyBindings p :: Predicate' 'InPredicate 'Representation
p@Predicate{[Term' 'NotWithinSet 'InPredicate 'Representation]
terms :: forall (pof :: PredicateOrFact) (ctx :: DatalogContext).
Predicate' pof ctx -> [Term' 'NotWithinSet pof ctx]
terms :: [Term' 'NotWithinSet 'InPredicate 'Representation]
terms} (Set Natural
origins, Bindings
bindings) =
  let newTerms :: Maybe [Value]
newTerms = forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse Term' 'NotWithinSet 'InPredicate 'Representation -> Maybe Value
replaceTerm [Term' 'NotWithinSet 'InPredicate 'Representation]
terms
      replaceTerm :: Term -> Maybe Value
      replaceTerm :: Term' 'NotWithinSet 'InPredicate 'Representation -> Maybe Value
replaceTerm (Variable VariableType 'NotWithinSet 'InPredicate
n)  = forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup VariableType 'NotWithinSet 'InPredicate
n Bindings
bindings
      replaceTerm (LInteger Int
t)  = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (inSet :: IsWithinSet) (pof :: PredicateOrFact)
       (ctx :: DatalogContext).
Int -> Term' inSet pof ctx
LInteger Int
t
      replaceTerm (LString Text
t)   = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (inSet :: IsWithinSet) (pof :: PredicateOrFact)
       (ctx :: DatalogContext).
Text -> Term' inSet pof ctx
LString Text
t
      replaceTerm (LDate UTCTime
t)     = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (inSet :: IsWithinSet) (pof :: PredicateOrFact)
       (ctx :: DatalogContext).
UTCTime -> Term' inSet pof ctx
LDate UTCTime
t
      replaceTerm (LBytes ByteString
t)    = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (inSet :: IsWithinSet) (pof :: PredicateOrFact)
       (ctx :: DatalogContext).
ByteString -> Term' inSet pof ctx
LBytes ByteString
t
      replaceTerm (LBool Bool
t)     = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (inSet :: IsWithinSet) (pof :: PredicateOrFact)
       (ctx :: DatalogContext).
Bool -> Term' inSet pof ctx
LBool Bool
t
      replaceTerm (TermSet SetType 'NotWithinSet 'Representation
t)   = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (inSet :: IsWithinSet) (pof :: PredicateOrFact)
       (ctx :: DatalogContext).
SetType inSet ctx -> Term' inSet pof ctx
TermSet SetType 'NotWithinSet 'Representation
t
      replaceTerm (Antiquote SliceType 'Representation
t) = forall a. Void -> a
absurd SliceType 'Representation
t
   in (\[Value]
nt -> (Set Natural
origins, Predicate' 'InPredicate 'Representation
p { terms :: [Value]
terms = [Value]
nt})) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe [Value]
newTerms

-- | Given a list of possible matches for each predicate,
-- give all the combinations of one match per predicate,
-- keeping track of the origin of each match
getCombinations :: [[Scoped Bindings]] -> [Scoped [Bindings]]
getCombinations :: [[Scoped Bindings]] -> [Scoped [Bindings]]
getCombinations = forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
traverse forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose

-- | merge a list of bindings, only keeping variables where
-- bindings are consistent
mergeBindings :: [Bindings] -> Bindings
mergeBindings :: [Bindings] -> Bindings
mergeBindings =
  -- group all the values unified with each variable
  let combinations :: [Bindings] -> Map Name (NonEmpty Value)
      combinations :: [Bindings] -> Map Text (NonEmpty Value)
combinations = forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
(a -> a -> a) -> f (Map k a) -> Map k a
Map.unionsWith forall a. Semigroup a => a -> a -> a
(<>) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (f :: * -> *) a. Applicative f => a -> f a
pure)
      sameValues :: NonEmpty Value -> Maybe Value
sameValues = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. NonEmpty a -> a
NE.head forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. MonadPlus m => (a -> Bool) -> m a -> m a
mfilter ((forall a. Eq a => a -> a -> Bool
== Int
1) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> Int
length) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Eq a => NonEmpty a -> NonEmpty a
NE.nub
  -- only keep consistent matches, where each variable takes a single value
      keepConsistent :: Map k (NonEmpty Value) -> Map k Value
keepConsistent = forall a b k. (a -> Maybe b) -> Map k a -> Map k b
Map.mapMaybe NonEmpty Value -> Maybe Value
sameValues
   in forall {k}. Map k (NonEmpty Value) -> Map k Value
keepConsistent forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Bindings] -> Map Text (NonEmpty Value)
combinations

-- | given a set of bindings for each predicate of a query,
-- only keep combinations where every variable matches exactly
-- one value. This rejects both inconsitent bindings (where the
-- same variable
reduceCandidateBindings :: Set Name
                        -> [Set (Scoped Bindings)]
                        -> Set (Scoped Bindings)
reduceCandidateBindings :: Set Text -> [Set (Scoped Bindings)] -> Set (Scoped Bindings)
reduceCandidateBindings Set Text
allVariables [Set (Scoped Bindings)]
matches =
  let allCombinations :: [(Set Natural, [Bindings])]
      allCombinations :: [Scoped [Bindings]]
allCombinations = [[Scoped Bindings]] -> [Scoped [Bindings]]
getCombinations forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Set (Scoped Bindings)]
matches
      isComplete :: Scoped Bindings -> Bool
      isComplete :: Scoped Bindings -> Bool
isComplete = (forall a. Eq a => a -> a -> Bool
== Set Text
allVariables) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => [a] -> Set a
Set.fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k a. Map k a -> [k]
Map.keys forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd
   in forall a. Ord a => [a] -> Set a
Set.fromList forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter Scoped Bindings -> Bool
isComplete forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Bindings] -> Bindings
mergeBindings forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Scoped [Bindings]]
allCombinations

-- | Given a set of facts and a series of predicates, return, for each fact,
-- a set of bindings corresponding to matched facts
getCandidateBindings :: Set (Scoped Fact)
                     -> [Predicate]
                     -> [Set (Scoped Bindings)]
getCandidateBindings :: Set (Scoped Fact)
-> [Predicate' 'InPredicate 'Representation]
-> [Set (Scoped Bindings)]
getCandidateBindings Set (Scoped Fact)
facts [Predicate' 'InPredicate 'Representation]
predicates =
   let mapMaybeS :: (Ord a, Ord b) => (a -> Maybe b) -> Set a -> Set b
       mapMaybeS :: forall a b. (Ord a, Ord b) => (a -> Maybe b) -> Set a -> Set b
mapMaybeS a -> Maybe b
f = forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap forall a. a -> Set a
Set.singleton forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Maybe b
f)
       keepFacts :: Predicate -> Set (Scoped Bindings)
       keepFacts :: Predicate' 'InPredicate 'Representation -> Set (Scoped Bindings)
keepFacts Predicate' 'InPredicate 'Representation
p = forall a b. (Ord a, Ord b) => (a -> Maybe b) -> Set a -> Set b
mapMaybeS (Predicate' 'InPredicate 'Representation
-> Scoped Fact -> Maybe (Scoped Bindings)
factMatchesPredicate Predicate' 'InPredicate 'Representation
p) Set (Scoped Fact)
facts
    in Predicate' 'InPredicate 'Representation -> Set (Scoped Bindings)
keepFacts forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Predicate' 'InPredicate 'Representation]
predicates

isSame :: Term -> Value -> Bool
isSame :: Term' 'NotWithinSet 'InPredicate 'Representation -> Value -> Bool
isSame (LInteger Int
t) (LInteger Int
t') = Int
t forall a. Eq a => a -> a -> Bool
== Int
t'
isSame (LString Text
t)  (LString Text
t')  = Text
t forall a. Eq a => a -> a -> Bool
== Text
t'
isSame (LDate UTCTime
t)    (LDate UTCTime
t')    = UTCTime
t forall a. Eq a => a -> a -> Bool
== UTCTime
t'
isSame (LBytes ByteString
t)   (LBytes ByteString
t')   = ByteString
t forall a. Eq a => a -> a -> Bool
== ByteString
t'
isSame (LBool Bool
t)    (LBool Bool
t')    = Bool
t forall a. Eq a => a -> a -> Bool
== Bool
t'
isSame (TermSet SetType 'NotWithinSet 'Representation
t)  (TermSet SetType 'NotWithinSet 'Representation
t')  = SetType 'NotWithinSet 'Representation
t forall a. Eq a => a -> a -> Bool
== SetType 'NotWithinSet 'Representation
t'
isSame Term' 'NotWithinSet 'InPredicate 'Representation
_ Value
_                        = Bool
False

-- | Given a predicate and a fact, try to match the fact to the predicate,
-- and, in case of success, return the corresponding bindings
factMatchesPredicate :: Predicate -> Scoped Fact -> Maybe (Scoped Bindings)
factMatchesPredicate :: Predicate' 'InPredicate 'Representation
-> Scoped Fact -> Maybe (Scoped Bindings)
factMatchesPredicate Predicate{name :: forall (pof :: PredicateOrFact) (ctx :: DatalogContext).
Predicate' pof ctx -> Text
name = Text
predicateName, terms :: forall (pof :: PredicateOrFact) (ctx :: DatalogContext).
Predicate' pof ctx -> [Term' 'NotWithinSet pof ctx]
terms = [Term' 'NotWithinSet 'InPredicate 'Representation]
predicateTerms }
                     ( Set Natural
factOrigins
                     , Predicate{name :: forall (pof :: PredicateOrFact) (ctx :: DatalogContext).
Predicate' pof ctx -> Text
name = Text
factName, terms :: forall (pof :: PredicateOrFact) (ctx :: DatalogContext).
Predicate' pof ctx -> [Term' 'NotWithinSet pof ctx]
terms = [Value]
factTerms }
                     ) =
  let namesMatch :: Bool
namesMatch = Text
predicateName forall a. Eq a => a -> a -> Bool
== Text
factName
      lengthsMatch :: Bool
lengthsMatch = forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term' 'NotWithinSet 'InPredicate 'Representation]
predicateTerms forall a. Eq a => a -> a -> Bool
== forall (t :: * -> *) a. Foldable t => t a -> Int
length [Value]
factTerms
      allMatches :: Maybe [Bindings]
allMatches = forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m [c]
zipWithM Term' 'NotWithinSet 'InPredicate 'Representation
-> Value -> Maybe Bindings
compatibleMatch [Term' 'NotWithinSet 'InPredicate 'Representation]
predicateTerms [Value]
factTerms
      -- given a term and a value, generate (possibly empty) bindings if
      -- they can be unified:
      --   - if the term is a variable, then it can be unified with the value,
      --     generating a new binding pair
      --   - if the term is equal to the value then it can be unified, but no bindings
      --     are generated
      --   - if the term is a different value, then they can't be unified
      compatibleMatch :: Term -> Value -> Maybe Bindings
      compatibleMatch :: Term' 'NotWithinSet 'InPredicate 'Representation
-> Value -> Maybe Bindings
compatibleMatch (Variable VariableType 'NotWithinSet 'InPredicate
vname) Value
value = forall a. a -> Maybe a
Just (forall k a. k -> a -> Map k a
Map.singleton VariableType 'NotWithinSet 'InPredicate
vname Value
value)
      compatibleMatch Term' 'NotWithinSet 'InPredicate 'Representation
t Value
t' | Term' 'NotWithinSet 'InPredicate 'Representation -> Value -> Bool
isSame Term' 'NotWithinSet 'InPredicate 'Representation
t Value
t' = forall a. a -> Maybe a
Just forall a. Monoid a => a
mempty
                | Bool
otherwise   = forall a. Maybe a
Nothing
   in if Bool
namesMatch Bool -> Bool -> Bool
&& Bool
lengthsMatch
      then (Set Natural
factOrigins,) forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Bindings] -> Bindings
mergeBindings forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe [Bindings]
allMatches
      else forall a. Maybe a
Nothing

applyVariable :: Bindings
              -> Term
              -> Either String Value
applyVariable :: Bindings
-> Term' 'NotWithinSet 'InPredicate 'Representation
-> Either String Value
applyVariable Bindings
bindings = \case
  Variable VariableType 'NotWithinSet 'InPredicate
n  -> forall b a. b -> Maybe a -> Either b a
maybeToRight String
"Unbound variable" forall a b. (a -> b) -> a -> b
$ Bindings
bindings forall k a. Ord k => Map k a -> k -> Maybe a
!? VariableType 'NotWithinSet 'InPredicate
n
  LInteger Int
t  -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall (inSet :: IsWithinSet) (pof :: PredicateOrFact)
       (ctx :: DatalogContext).
Int -> Term' inSet pof ctx
LInteger Int
t
  LString Text
t   -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall (inSet :: IsWithinSet) (pof :: PredicateOrFact)
       (ctx :: DatalogContext).
Text -> Term' inSet pof ctx
LString Text
t
  LDate UTCTime
t     -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall (inSet :: IsWithinSet) (pof :: PredicateOrFact)
       (ctx :: DatalogContext).
UTCTime -> Term' inSet pof ctx
LDate UTCTime
t
  LBytes ByteString
t    -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall (inSet :: IsWithinSet) (pof :: PredicateOrFact)
       (ctx :: DatalogContext).
ByteString -> Term' inSet pof ctx
LBytes ByteString
t
  LBool Bool
t     -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall (inSet :: IsWithinSet) (pof :: PredicateOrFact)
       (ctx :: DatalogContext).
Bool -> Term' inSet pof ctx
LBool Bool
t
  TermSet SetType 'NotWithinSet 'Representation
t   -> forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ forall (inSet :: IsWithinSet) (pof :: PredicateOrFact)
       (ctx :: DatalogContext).
SetType inSet ctx -> Term' inSet pof ctx
TermSet SetType 'NotWithinSet 'Representation
t
  Antiquote SliceType 'Representation
v -> forall a. Void -> a
absurd SliceType 'Representation
v

evalUnary :: Unary -> Value -> Either String Value
evalUnary :: Unary -> Value -> Either String Value
evalUnary Unary
Parens Value
t = forall (f :: * -> *) a. Applicative f => a -> f a
pure Value
t
evalUnary Unary
Negate (LBool Bool
b) = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall (inSet :: IsWithinSet) (pof :: PredicateOrFact)
       (ctx :: DatalogContext).
Bool -> Term' inSet pof ctx
LBool forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not Bool
b)
evalUnary Unary
Negate Value
_ = forall a b. a -> Either a b
Left String
"Only booleans support negation"
evalUnary Unary
Length (LString Text
t) = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (inSet :: IsWithinSet) (pof :: PredicateOrFact)
       (ctx :: DatalogContext).
Int -> Term' inSet pof ctx
LInteger forall a b. (a -> b) -> a -> b
$ Text -> Int
Text.length Text
t
evalUnary Unary
Length (LBytes ByteString
bs) = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (inSet :: IsWithinSet) (pof :: PredicateOrFact)
       (ctx :: DatalogContext).
Int -> Term' inSet pof ctx
LInteger forall a b. (a -> b) -> a -> b
$ ByteString -> Int
ByteString.length ByteString
bs
evalUnary Unary
Length (TermSet SetType 'NotWithinSet 'Representation
s) = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (inSet :: IsWithinSet) (pof :: PredicateOrFact)
       (ctx :: DatalogContext).
Int -> Term' inSet pof ctx
LInteger forall a b. (a -> b) -> a -> b
$ forall a. Set a -> Int
Set.size SetType 'NotWithinSet 'Representation
s
evalUnary Unary
Length Value
_ = forall a b. a -> Either a b
Left String
"Only strings, bytes and sets support `.length()`"

evalBinary :: Limits -> Binary -> Value -> Value -> Either String Value
-- eq / ord operations
evalBinary :: Limits -> Binary -> Value -> Value -> Either String Value
evalBinary Limits
_ Binary
Equal (LInteger Int
i) (LInteger Int
i') = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (inSet :: IsWithinSet) (pof :: PredicateOrFact)
       (ctx :: DatalogContext).
Bool -> Term' inSet pof ctx
LBool (Int
i forall a. Eq a => a -> a -> Bool
== Int
i')
evalBinary Limits
_ Binary
Equal (LString Text
t) (LString Text
t')   = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (inSet :: IsWithinSet) (pof :: PredicateOrFact)
       (ctx :: DatalogContext).
Bool -> Term' inSet pof ctx
LBool (Text
t forall a. Eq a => a -> a -> Bool
== Text
t')
evalBinary Limits
_ Binary
Equal (LDate UTCTime
t) (LDate UTCTime
t')       = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (inSet :: IsWithinSet) (pof :: PredicateOrFact)
       (ctx :: DatalogContext).
Bool -> Term' inSet pof ctx
LBool (UTCTime
t forall a. Eq a => a -> a -> Bool
== UTCTime
t')
evalBinary Limits
_ Binary
Equal (LBytes ByteString
t) (LBytes ByteString
t')     = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (inSet :: IsWithinSet) (pof :: PredicateOrFact)
       (ctx :: DatalogContext).
Bool -> Term' inSet pof ctx
LBool (ByteString
t forall a. Eq a => a -> a -> Bool
== ByteString
t')
evalBinary Limits
_ Binary
Equal (LBool Bool
t) (LBool Bool
t')       = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (inSet :: IsWithinSet) (pof :: PredicateOrFact)
       (ctx :: DatalogContext).
Bool -> Term' inSet pof ctx
LBool (Bool
t forall a. Eq a => a -> a -> Bool
== Bool
t')
evalBinary Limits
_ Binary
Equal (TermSet SetType 'NotWithinSet 'Representation
t) (TermSet SetType 'NotWithinSet 'Representation
t')   = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (inSet :: IsWithinSet) (pof :: PredicateOrFact)
       (ctx :: DatalogContext).
Bool -> Term' inSet pof ctx
LBool (SetType 'NotWithinSet 'Representation
t forall a. Eq a => a -> a -> Bool
== SetType 'NotWithinSet 'Representation
t')
evalBinary Limits
_ Binary
Equal Value
_ Value
_                        = forall a b. a -> Either a b
Left String
"Equality mismatch"
evalBinary Limits
_ Binary
LessThan (LInteger Int
i) (LInteger Int
i') = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (inSet :: IsWithinSet) (pof :: PredicateOrFact)
       (ctx :: DatalogContext).
Bool -> Term' inSet pof ctx
LBool (Int
i forall a. Ord a => a -> a -> Bool
< Int
i')
evalBinary Limits
_ Binary
LessThan (LDate UTCTime
t) (LDate UTCTime
t')       = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (inSet :: IsWithinSet) (pof :: PredicateOrFact)
       (ctx :: DatalogContext).
Bool -> Term' inSet pof ctx
LBool (UTCTime
t forall a. Ord a => a -> a -> Bool
< UTCTime
t')
evalBinary Limits
_ Binary
LessThan Value
_ Value
_                        = forall a b. a -> Either a b
Left String
"< mismatch"
evalBinary Limits
_ Binary
GreaterThan (LInteger Int
i) (LInteger Int
i') = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (inSet :: IsWithinSet) (pof :: PredicateOrFact)
       (ctx :: DatalogContext).
Bool -> Term' inSet pof ctx
LBool (Int
i forall a. Ord a => a -> a -> Bool
> Int
i')
evalBinary Limits
_ Binary
GreaterThan (LDate UTCTime
t) (LDate UTCTime
t')       = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (inSet :: IsWithinSet) (pof :: PredicateOrFact)
       (ctx :: DatalogContext).
Bool -> Term' inSet pof ctx
LBool (UTCTime
t forall a. Ord a => a -> a -> Bool
> UTCTime
t')
evalBinary Limits
_ Binary
GreaterThan Value
_ Value
_                        = forall a b. a -> Either a b
Left String
"> mismatch"
evalBinary Limits
_ Binary
LessOrEqual (LInteger Int
i) (LInteger Int
i') = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (inSet :: IsWithinSet) (pof :: PredicateOrFact)
       (ctx :: DatalogContext).
Bool -> Term' inSet pof ctx
LBool (Int
i forall a. Ord a => a -> a -> Bool
<= Int
i')
evalBinary Limits
_ Binary
LessOrEqual (LDate UTCTime
t) (LDate UTCTime
t')       = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (inSet :: IsWithinSet) (pof :: PredicateOrFact)
       (ctx :: DatalogContext).
Bool -> Term' inSet pof ctx
LBool (UTCTime
t forall a. Ord a => a -> a -> Bool
<= UTCTime
t')
evalBinary Limits
_ Binary
LessOrEqual Value
_ Value
_                        = forall a b. a -> Either a b
Left String
"<= mismatch"
evalBinary Limits
_ Binary
GreaterOrEqual (LInteger Int
i) (LInteger Int
i') = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (inSet :: IsWithinSet) (pof :: PredicateOrFact)
       (ctx :: DatalogContext).
Bool -> Term' inSet pof ctx
LBool (Int
i forall a. Ord a => a -> a -> Bool
>= Int
i')
evalBinary Limits
_ Binary
GreaterOrEqual (LDate UTCTime
t) (LDate UTCTime
t')       = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (inSet :: IsWithinSet) (pof :: PredicateOrFact)
       (ctx :: DatalogContext).
Bool -> Term' inSet pof ctx
LBool (UTCTime
t forall a. Ord a => a -> a -> Bool
>= UTCTime
t')
evalBinary Limits
_ Binary
GreaterOrEqual Value
_ Value
_                        = forall a b. a -> Either a b
Left String
">= mismatch"
-- string-related operations
evalBinary Limits
_ Binary
Prefix (LString Text
t) (LString Text
t') = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (inSet :: IsWithinSet) (pof :: PredicateOrFact)
       (ctx :: DatalogContext).
Bool -> Term' inSet pof ctx
LBool (Text
t' Text -> Text -> Bool
`Text.isPrefixOf` Text
t)
evalBinary Limits
_ Binary
Prefix Value
_ Value
_                      = forall a b. a -> Either a b
Left String
"Only strings support `.starts_with()`"
evalBinary Limits
_ Binary
Suffix (LString Text
t) (LString Text
t') = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (inSet :: IsWithinSet) (pof :: PredicateOrFact)
       (ctx :: DatalogContext).
Bool -> Term' inSet pof ctx
LBool (Text
t' Text -> Text -> Bool
`Text.isSuffixOf` Text
t)
evalBinary Limits
_ Binary
Suffix Value
_ Value
_                      = forall a b. a -> Either a b
Left String
"Only strings support `.ends_with()`"
evalBinary Limits{Bool
allowRegexes :: Bool
allowRegexes :: Limits -> Bool
allowRegexes} Binary
Regex  (LString Text
t) (LString Text
r) | Bool
allowRegexes = Text -> Text -> Either String Value
regexMatch Text
t Text
r
                                                               | Bool
otherwise    = forall a b. a -> Either a b
Left String
"Regex evaluation is disabled"
evalBinary Limits
_ Binary
Regex Value
_ Value
_                       = forall a b. a -> Either a b
Left String
"Only strings support `.matches()`"
-- num operations
evalBinary Limits
_ Binary
Add (LInteger Int
i) (LInteger Int
i') = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (inSet :: IsWithinSet) (pof :: PredicateOrFact)
       (ctx :: DatalogContext).
Int -> Term' inSet pof ctx
LInteger (Int
i forall a. Num a => a -> a -> a
+ Int
i')
evalBinary Limits
_ Binary
Add (LString Text
t) (LString Text
t') = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (inSet :: IsWithinSet) (pof :: PredicateOrFact)
       (ctx :: DatalogContext).
Text -> Term' inSet pof ctx
LString (Text
t forall a. Semigroup a => a -> a -> a
<> Text
t')
evalBinary Limits
_ Binary
Add Value
_ Value
_ = forall a b. a -> Either a b
Left String
"Only integers and strings support addition"
evalBinary Limits
_ Binary
Sub (LInteger Int
i) (LInteger Int
i') = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (inSet :: IsWithinSet) (pof :: PredicateOrFact)
       (ctx :: DatalogContext).
Int -> Term' inSet pof ctx
LInteger (Int
i forall a. Num a => a -> a -> a
- Int
i')
evalBinary Limits
_ Binary
Sub Value
_ Value
_ = forall a b. a -> Either a b
Left String
"Only integers support subtraction"
evalBinary Limits
_ Binary
Mul (LInteger Int
i) (LInteger Int
i') = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (inSet :: IsWithinSet) (pof :: PredicateOrFact)
       (ctx :: DatalogContext).
Int -> Term' inSet pof ctx
LInteger (Int
i forall a. Num a => a -> a -> a
* Int
i')
evalBinary Limits
_ Binary
Mul Value
_ Value
_ = forall a b. a -> Either a b
Left String
"Only integers support multiplication"
evalBinary Limits
_ Binary
Div (LInteger Int
_) (LInteger Int
0) = forall a b. a -> Either a b
Left String
"Divide by 0"
evalBinary Limits
_ Binary
Div (LInteger Int
i) (LInteger Int
i') = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (inSet :: IsWithinSet) (pof :: PredicateOrFact)
       (ctx :: DatalogContext).
Int -> Term' inSet pof ctx
LInteger (Int
i forall a. Integral a => a -> a -> a
`div` Int
i')
evalBinary Limits
_ Binary
Div Value
_ Value
_ = forall a b. a -> Either a b
Left String
"Only integers support division"
-- bitwise operations
evalBinary Limits
_ Binary
BitwiseAnd (LInteger Int
i) (LInteger Int
i') = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (inSet :: IsWithinSet) (pof :: PredicateOrFact)
       (ctx :: DatalogContext).
Int -> Term' inSet pof ctx
LInteger (Int
i forall a. Bits a => a -> a -> a
.&. Int
i')
evalBinary Limits
_ Binary
BitwiseAnd Value
_ Value
_ = forall a b. a -> Either a b
Left String
"Only integers support bitwise and"
evalBinary Limits
_ Binary
BitwiseOr  (LInteger Int
i) (LInteger Int
i') = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (inSet :: IsWithinSet) (pof :: PredicateOrFact)
       (ctx :: DatalogContext).
Int -> Term' inSet pof ctx
LInteger (Int
i forall a. Bits a => a -> a -> a
.|. Int
i')
evalBinary Limits
_ Binary
BitwiseOr Value
_ Value
_ = forall a b. a -> Either a b
Left String
"Only integers support bitwise or"
evalBinary Limits
_ Binary
BitwiseXor (LInteger Int
i) (LInteger Int
i') = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (inSet :: IsWithinSet) (pof :: PredicateOrFact)
       (ctx :: DatalogContext).
Int -> Term' inSet pof ctx
LInteger (Int
i forall a. Bits a => a -> a -> a
`xor` Int
i')
evalBinary Limits
_ Binary
BitwiseXor Value
_ Value
_ = forall a b. a -> Either a b
Left String
"Only integers support bitwise xor"
-- boolean operations
evalBinary Limits
_ Binary
And (LBool Bool
b) (LBool Bool
b') = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (inSet :: IsWithinSet) (pof :: PredicateOrFact)
       (ctx :: DatalogContext).
Bool -> Term' inSet pof ctx
LBool (Bool
b Bool -> Bool -> Bool
&& Bool
b')
evalBinary Limits
_ Binary
And Value
_ Value
_ = forall a b. a -> Either a b
Left String
"Only booleans support &&"
evalBinary Limits
_ Binary
Or (LBool Bool
b) (LBool Bool
b') = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (inSet :: IsWithinSet) (pof :: PredicateOrFact)
       (ctx :: DatalogContext).
Bool -> Term' inSet pof ctx
LBool (Bool
b Bool -> Bool -> Bool
|| Bool
b')
evalBinary Limits
_ Binary
Or Value
_ Value
_ = forall a b. a -> Either a b
Left String
"Only booleans support ||"
-- set operations
evalBinary Limits
_ Binary
Contains (TermSet SetType 'NotWithinSet 'Representation
t) (TermSet SetType 'NotWithinSet 'Representation
t') = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (inSet :: IsWithinSet) (pof :: PredicateOrFact)
       (ctx :: DatalogContext).
Bool -> Term' inSet pof ctx
LBool (forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf SetType 'NotWithinSet 'Representation
t' SetType 'NotWithinSet 'Representation
t)
evalBinary Limits
_ Binary
Contains (TermSet SetType 'NotWithinSet 'Representation
t) Value
t' = case Value -> Maybe (Term' 'WithinSet 'InFact 'Representation)
valueToSetTerm Value
t' of
    Just Term' 'WithinSet 'InFact 'Representation
t'' -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (inSet :: IsWithinSet) (pof :: PredicateOrFact)
       (ctx :: DatalogContext).
Bool -> Term' inSet pof ctx
LBool (forall a. Ord a => a -> Set a -> Bool
Set.member Term' 'WithinSet 'InFact 'Representation
t'' SetType 'NotWithinSet 'Representation
t)
    Maybe (Term' 'WithinSet 'InFact 'Representation)
Nothing  -> forall a b. a -> Either a b
Left String
"Sets cannot contain nested sets nor variables"
evalBinary Limits
_ Binary
Contains (LString Text
t) (LString Text
t') = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (inSet :: IsWithinSet) (pof :: PredicateOrFact)
       (ctx :: DatalogContext).
Bool -> Term' inSet pof ctx
LBool (Text
t' Text -> Text -> Bool
`isInfixOf` Text
t)
evalBinary Limits
_ Binary
Contains Value
_ Value
_ = forall a b. a -> Either a b
Left String
"Only sets and strings support `.contains()`"
evalBinary Limits
_ Binary
Intersection (TermSet SetType 'NotWithinSet 'Representation
t) (TermSet SetType 'NotWithinSet 'Representation
t') = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (inSet :: IsWithinSet) (pof :: PredicateOrFact)
       (ctx :: DatalogContext).
SetType inSet ctx -> Term' inSet pof ctx
TermSet (forall a. Ord a => Set a -> Set a -> Set a
Set.intersection SetType 'NotWithinSet 'Representation
t SetType 'NotWithinSet 'Representation
t')
evalBinary Limits
_ Binary
Intersection Value
_ Value
_ = forall a b. a -> Either a b
Left String
"Only sets support `.intersection()`"
evalBinary Limits
_ Binary
Union (TermSet SetType 'NotWithinSet 'Representation
t) (TermSet SetType 'NotWithinSet 'Representation
t') = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (inSet :: IsWithinSet) (pof :: PredicateOrFact)
       (ctx :: DatalogContext).
SetType inSet ctx -> Term' inSet pof ctx
TermSet (forall a. Ord a => Set a -> Set a -> Set a
Set.union SetType 'NotWithinSet 'Representation
t SetType 'NotWithinSet 'Representation
t')
evalBinary Limits
_ Binary
Union Value
_ Value
_ = forall a b. a -> Either a b
Left String
"Only sets support `.union()`"

regexMatch :: Text -> Text -> Either String Value
regexMatch :: Text -> Text -> Either String Value
regexMatch Text
text Text
regexT = do
  Regex
regex  <- CompOption -> ExecOption -> Text -> Either String Regex
Regex.compile forall regex compOpt execOpt.
RegexOptions regex compOpt execOpt =>
compOpt
Regex.defaultCompOpt forall regex compOpt execOpt.
RegexOptions regex compOpt execOpt =>
execOpt
Regex.defaultExecOpt Text
regexT
  Maybe MatchArray
result <- Regex -> Text -> Either String (Maybe MatchArray)
Regex.execute Regex
regex Text
text
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (inSet :: IsWithinSet) (pof :: PredicateOrFact)
       (ctx :: DatalogContext).
Bool -> Term' inSet pof ctx
LBool forall a b. (a -> b) -> a -> b
$ forall a. Maybe a -> Bool
isJust Maybe MatchArray
result

-- | Given bindings for variables, reduce an expression to a single
-- datalog value
evaluateExpression :: Limits
                   -> Bindings
                   -> Expression
                   -> Either String Value
evaluateExpression :: Limits -> Bindings -> Expression -> Either String Value
evaluateExpression Limits
l Bindings
b = \case
    EValue Term' 'NotWithinSet 'InPredicate 'Representation
term -> Bindings
-> Term' 'NotWithinSet 'InPredicate 'Representation
-> Either String Value
applyVariable Bindings
b Term' 'NotWithinSet 'InPredicate 'Representation
term
    EUnary Unary
op Expression
e' -> Unary -> Value -> Either String Value
evalUnary Unary
op forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Limits -> Bindings -> Expression -> Either String Value
evaluateExpression Limits
l Bindings
b Expression
e'
    EBinary Binary
op Expression
e' Expression
e'' -> forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Limits -> Binary -> Value -> Value -> Either String Value
evalBinary Limits
l Binary
op) forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *) a. Monad m => m (m a) -> m a
join forall (t :: * -> * -> *) (f :: * -> *) a c b d.
(Bitraversable t, Applicative f) =>
(a -> f c) -> (b -> f d) -> t a b -> f (t c d)
bitraverse (Limits -> Bindings -> Expression -> Either String Value
evaluateExpression Limits
l Bindings
b) (Expression
e', Expression
e'')