diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,30 @@ +Copyright (c) 2012, Tristan Ravitch + +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions are met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * Redistributions in binary form must reproduce the above + copyright notice, this list of conditions and the following + disclaimer in the documentation and/or other materials provided + with the distribution. + + * Neither the name of Tristan Ravitch nor the names of other + contributors may be used to endorse or promote products derived + from this software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS +"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT +LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR +A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT +OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, +SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT +LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, +DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY +THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT +(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE +OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/datalog.cabal b/datalog.cabal new file mode 100644 --- /dev/null +++ b/datalog.cabal @@ -0,0 +1,94 @@ +-- Initial datalog.cabal generated by cabal init. For further +-- documentation, see http://haskell.org/cabal/users-guide/ + +name: datalog +version: 0.1.0.0 +synopsis: An implementation of datalog in Haskell +license: BSD3 +license-file: LICENSE +author: Tristan Ravitch +maintainer: travitch@cs.wisc.edu +category: Database +build-type: Simple +cabal-version: >=1.10 +description: This is an implementation of datalog in pure Haskell. + It is implemented as a library and can be used from within + any Haskell application. As a consequence, it supports both + standard Datalog operations and arbitrary predicates written + in Haskell. + . + One day it will have a command-line program as well. + +library + default-language: Haskell2010 + exposed-modules: Database.Datalog + other-modules: Database.Datalog.Adornment + Database.Datalog.Database + Database.Datalog.Errors + Database.Datalog.Evaluate + Database.Datalog.MagicSets + Database.Datalog.Relation + Database.Datalog.Rules + Database.Datalog.Stratification + build-depends: base == 4.*, + containers, + unordered-containers, + hashable, + failure, + text, + transformers >= 0.3, + vector >= 0.9 + hs-source-dirs: src + ghc-options: -Wall -auto-all + ghc-prof-options: -auto-all + +test-suite NQueensTest + default-language: Haskell2010 + hs-source-dirs: tests + type: exitcode-stdio-1.0 + main-is: NQueens.hs + ghc-options: -Wall -auto-all + ghc-prof-options: -auto-all + build-depends: datalog == 0.1.0.0, + base == 4.*, + text, + containers, + hashable, + test-framework, + test-framework-hunit, + HUnit + +test-suite AncestorTest + default-language: Haskell2010 + hs-source-dirs: tests + type: exitcode-stdio-1.0 + main-is: AncestorTest.hs + ghc-options: -Wall + ghc-prof-options: -auto-all + build-depends: datalog == 0.1.0.0, + base == 4.*, + text, + containers, + test-framework, + test-framework-hunit, + HUnit + +test-suite WorksForTest + default-language: Haskell2010 + hs-source-dirs: tests + type: exitcode-stdio-1.0 + main-is: WorksForTest.hs + ghc-options: -Wall + ghc-prof-options: -auto-all + build-depends: datalog == 0.1.0.0, + base == 4.*, + text, + containers, + hashable, + test-framework, + test-framework-hunit, + HUnit + +source-repository head + type: git + location: git://github.com/travitch/datalog.git diff --git a/src/Database/Datalog.hs b/src/Database/Datalog.hs new file mode 100644 --- /dev/null +++ b/src/Database/Datalog.hs @@ -0,0 +1,113 @@ +{-# LANGUAGE FlexibleContexts #-} +module Database.Datalog ( + -- * Types + Database, + Relation, + DatabaseBuilder, + QueryBuilder, + Term(LogicVar, BindVar, Anything, Atom), + QueryPlan, + DatalogError(..), + Query, + Failure, + + -- * Building the IDB + makeDatabase, + addRelation, + assertFact, + + -- * Building Logic Programs + (|-), + assertRule, + relationPredicateFromName, + inferencePredicate, + issueQuery, + lit, + negLit, + cond1, + cond2, + cond3, + cond4, + cond5, + + -- * Evaluating Queries + queryDatabase, + buildQueryPlan, + executeQueryPlan + ) where + +import Control.Failure +import Control.Monad ( foldM ) +import Data.Hashable +import Data.Text ( Text ) + +import Database.Datalog.Database +import Database.Datalog.Errors +import Database.Datalog.Evaluate +import Database.Datalog.Rules +import Database.Datalog.MagicSets +import Database.Datalog.Stratification + +import Debug.Trace +import Text.Printf +debug = flip trace + +-- | A fully-stratified query plan that is ready to be executed. +data QueryPlan a = QueryPlan (Query a) [[Rule a]] + +-- | This is a shortcut to build a query plan and execute in one step, +-- with no bindings provided. It doesn't make sense to have bindings +-- in one-shot queries. +queryDatabase :: (Failure DatalogError m, Eq a, Hashable a, Show a) + => Database a -- ^ The intensional database of facts + -> QueryBuilder m a (Query a) -- ^ A monad building up a set of rules and returning a Query + -> m [[a]] +queryDatabase idb qm = do + qp <- buildQueryPlan idb qm + executeQueryPlan qp idb [] + +-- | Given a query description, build a query plan by stratifying the +-- rules and performing the magic sets transformation. Throws an +-- error if the rules cannot be stratified. +buildQueryPlan :: (Failure DatalogError m, Eq a, Hashable a, Show a) + => Database a + -> QueryBuilder m a (Query a) + -> m (QueryPlan a) +buildQueryPlan idb qm = do + (q, rs) <- runQuery qm idb + rs' <- magicSetsRules q rs + strata <- stratifyRules rs' + return $! QueryPlan q strata + +-- | Execute a query plan with an intensional database and a set of +-- bindings (substituted in for 'BindVar's). Throw an error if: +-- +-- * The rules and database define the same relation +executeQueryPlan :: (Failure DatalogError m, Eq a, Hashable a, Show a) + => QueryPlan a -> Database a -> [(Text, a)] -> m [[a]] +executeQueryPlan (QueryPlan q strata) idb bindings = do + -- FIXME: Bindings is used to substitute in values for BoundVars in + -- the query. Those might actually affect the magic rules that are + -- required... This is the seed-rule and + -- seed-predicate-for-insertion code in the clojure implementation + sdb <- seedDatabase idb (concat strata) q bindings + edb <- applyStrata strata sdb + let q' = bindQuery q bindings + pt = queryToPartialTuple q' + p = queryPredicate q' + return $! map unTuple $ select edb p pt -- `debug` show edb + +-- Private helpers + +-- | Apply the rules in each stratum bottom-up. Compute a fixed-point +-- for each stratum +applyStrata :: (Failure DatalogError m, Eq a, Hashable a, Show a) + => [[Rule a]] -> Database a -> m (Database a) +applyStrata [] db = return db +applyStrata ss@(s:strata) db = do + -- Group the rules by their head relations. The delta table has to + -- be managed for all of the related rules at once. + db' <- foldM applyRuleSet db (partitionRules s) + case databaseHasDelta db' of + True -> applyStrata ss db' + False -> applyStrata strata db' diff --git a/src/Database/Datalog/Adornment.hs b/src/Database/Datalog/Adornment.hs new file mode 100644 --- /dev/null +++ b/src/Database/Datalog/Adornment.hs @@ -0,0 +1,35 @@ +module Database.Datalog.Adornment ( + Binding(..), + BindingPattern(..), + Adornment(..) + ) where + +import Data.Hashable + +data Binding = B {- Bound -} | F {- Free -} + deriving (Eq, Ord, Show) + +instance Hashable Binding where + hashWithSalt s B = s `hashWithSalt` (105 :: Int) + hashWithSalt s F = s `hashWithSalt` (709 :: Int) + +newtype BindingPattern = BindingPattern { bindingPattern :: [Binding] } + deriving (Eq, Ord) + +instance Show BindingPattern where + show (BindingPattern bs) = concatMap show bs + +instance Hashable BindingPattern where + hashWithSalt s (BindingPattern bs) = s `hashWithSalt` bs + +data Adornment = Free !Int -- ^ The index to bind a free variable + | BoundAtom + | Bound !Int -- ^ The index to look for the binding of this variable + deriving (Eq, Show) + +instance Hashable Adornment where + hashWithSalt s BoundAtom = s `hashWithSalt` (7776 :: Int) + hashWithSalt s (Free i) = + s `hashWithSalt` (1 :: Int) `hashWithSalt` i + hashWithSalt s (Bound i) = + s `hashWithSalt` (2 :: Int) `hashWithSalt` i diff --git a/src/Database/Datalog/Database.hs b/src/Database/Datalog/Database.hs new file mode 100644 --- /dev/null +++ b/src/Database/Datalog/Database.hs @@ -0,0 +1,204 @@ +{-# LANGUAGE DeriveDataTypeable, FlexibleContexts #-} +module Database.Datalog.Database ( + Relation, + Database, + DatabaseBuilder, + Tuple(..), + -- * Functions + makeDatabase, + addRelation, + assertFact, + databaseRelations, + databaseRelation, + dataForRelation, + addTupleToRelation, + addTupleToRelation', + replaceRelation, + ensureDatabaseRelation, + resetRelationDelta, + withDeltaRelation, + databaseHasDelta + ) where + +import Control.Failure +import Control.Monad.Trans.Class +import Control.Monad.Trans.State.Strict +import Data.Hashable +import Data.HashMap.Strict ( HashMap ) +import qualified Data.HashMap.Strict as HM +import Data.HashSet ( HashSet ) +import qualified Data.HashSet as HS +import Data.Monoid +import Data.Text ( Text ) + +import Database.Datalog.Errors +import Database.Datalog.Relation + +import Debug.Trace +debug = flip trace + +-- | A wrapper around lists that lets us more easily hide length +-- checks +newtype Tuple a = Tuple { unTuple :: [a] } + deriving (Eq, Show) + +instance (Hashable a) => Hashable (Tuple a) where + hashWithSalt s (Tuple es) = s `hashWithSalt` es + +-- | A relation whose elements are fixed-length lists of a +-- user-defined type. This is only used internally and is not exposed +-- to the user. +data DBRelation a = DBRelation { relationArity :: !Int + , relationName :: !Relation + , relationData :: [Tuple a] + , relationMembers :: !(HashSet (Tuple a)) + , relationDelta :: [Tuple a] + , relationIndex :: !(HashMap (Int, a) (Tuple a)) + } + deriving (Show) + +instance (Eq a, Hashable a) => Eq (DBRelation a) where + (DBRelation arity1 n1 _ ms1 _ _) == (DBRelation arity2 n2 _ ms2 _ _) = + arity1 == arity2 && n1 == n2 && ms1 == ms2 + +-- | A database is a collection of facts organized into relations +newtype Database a = Database (HashMap Relation (DBRelation a)) + +instance (Show a) => Show (Database a) where + show (Database db) = show db + +instance (Eq a, Hashable a) => Eq (Database a) where + (Database db1) == (Database db2) = db1 == db2 + +-- | The monad in which databases are constructed and initial facts +-- are asserted +type DatabaseBuilder m a = StateT (Database a) m + +-- | Make a new fact Database in a DatabaseBuilder monad. It can +-- fail, and errors will be returned however the caller indicates. +makeDatabase :: (Failure DatalogError m) + => DatabaseBuilder m a () -> m (Database a) +makeDatabase b = execStateT b (Database mempty) + +-- | Add a relation to the 'Database'. If the relation exists, an +-- error will be raised. The function returns a 'RelationHandle' that +-- can be used in conjuction with 'addTuple'. +addRelation :: (Failure DatalogError m, Eq a, Hashable a) + => Text -> Int -> DatabaseBuilder m a Relation +addRelation name arity = do + Database m <- get + case HM.lookup rel m of + Just _ -> lift $ failure (RelationExistsError name) + Nothing -> do + let r = DBRelation arity rel mempty mempty mempty mempty + put $! Database $! HM.insert rel r m + return rel + where + rel = Relation name + +-- | Add a tuple to the named 'Relation' in the database. If the +-- tuple is already present, the original 'Database' is unchanged. +assertFact :: (Failure DatalogError m, Eq a, Hashable a) + => Relation -> [a] -> DatabaseBuilder m a () +assertFact relHandle tup = do + db@(Database m) <- get + let rel = databaseRelation db relHandle + wrappedTuple <- toWrappedTuple rel tup + case HS.member wrappedTuple (relationMembers rel) of + True -> return () + False -> + let rel' = addTupleToRelation' rel wrappedTuple + in put $! Database $ HM.insert relHandle rel' m + +-- | Replace a relation in the database. The old relation is +-- discarded completely, so be sure to initialize the replacement with +-- all of the currently known facts. +replaceRelation :: Database a -> DBRelation a -> Database a +replaceRelation (Database db) r = + Database $ HM.insert (relationName r) r db + +-- | Add a tuple to the relation without updating the delta table. +-- This is needed for the initial database construction. +addTupleToRelation' :: (Eq a, Hashable a) => DBRelation a -> Tuple a -> DBRelation a +addTupleToRelation' rel t = + case HS.member t (relationMembers rel) of + True -> rel + False -> rel { relationData = t : relationData rel + , relationMembers = HS.insert t (relationMembers rel) + } + +-- | Add the given tuple to the given 'Relation'. It updates the +-- index in the process. The 'Tuple' is already validated so this is +-- a total function. +-- +-- It has already been verified that the tuple does not exist in the +-- relation (see 'addTuple') so no extra checks are required here. +addTupleToRelation :: (Eq a, Hashable a, Show a) => DBRelation a -> Tuple a -> DBRelation a +addTupleToRelation rel t = + case HS.member t (relationMembers rel) of + True -> rel + False -> rel { relationData = t : relationData rel + , relationMembers = HS.insert t (relationMembers rel) + , relationDelta = t : relationDelta rel + } + +-- | If the requested relation is not in the database, just use the +-- original database (the result is the same - an empty relation) +withDeltaRelation :: Database a -> Relation -> (Database a -> b) -> b +withDeltaRelation d@(Database db) r action = + action $ case HM.lookup r db of + Nothing -> d + Just dbrel -> + let rel' = dbrel { relationData = relationDelta dbrel } + in Database $ HM.insert r rel' db + +resetRelationDelta :: DBRelation a -> DBRelation a +resetRelationDelta rel = rel { relationDelta = mempty } + +-- | Get a relation by name. If it does not exist in the database, +-- return a new relation with the appropriate arity. +ensureDatabaseRelation :: (Eq a, Hashable a) + => Database a -> Relation -> Int -> DBRelation a +ensureDatabaseRelation (Database m) rel arity = + case HM.lookup rel m of + Just r -> r + Nothing -> DBRelation arity rel mempty mempty mempty mempty + +-- | Get an existing relation from the database +databaseRelation :: Database a -> Relation -> DBRelation a +databaseRelation (Database m) rel = + case HM.lookup rel m of + -- This really shouldn't be possible - it would be an error in the + -- API since users can't create them and they can only be obtained + -- in the same monad with the Database + Nothing -> error ("Invalid RelationHandle: " ++ show rel) + Just r -> r + +-- | Get all of the predicates referenced in the database +databaseRelations :: Database a -> [Relation] +databaseRelations (Database m) = HM.keys m + +-- | Get all of the tuples for the given predicate/relation in the database. +dataForRelation :: (Failure DatalogError m) + => Database a -> Relation -> m [Tuple a] +dataForRelation (Database m) rel = + case HM.lookup rel m of + Nothing -> failure $ NoRelationError rel + Just r -> return $ relationData r + +databaseHasDelta :: Database a -> Bool +databaseHasDelta (Database db) = + any (not . null . relationDelta) (HM.elems db)-- `debug` show (map toDbg (HM.elems db)) + -- where + -- toDbg r = show (relationName r) ++ ": " ++ show (not (null (relationDelta r))) + +-- | Convert the user-level tuple to a safe length-checked Tuple. +-- Signals failure (according to @m@) if the length is invalid. +-- +-- FIXME: It would also be nice to be able to check the column type... +toWrappedTuple :: (Failure DatalogError m) + => DBRelation a -> [a] -> DatabaseBuilder m a (Tuple a) +toWrappedTuple rel tup = + case relationArity rel == length tup of + False -> lift $ failure (SchemaError (relationName rel)) + True -> return $! Tuple tup diff --git a/src/Database/Datalog/Errors.hs b/src/Database/Datalog/Errors.hs new file mode 100644 --- /dev/null +++ b/src/Database/Datalog/Errors.hs @@ -0,0 +1,21 @@ +{-# LANGUAGE DeriveDataTypeable #-} +module Database.Datalog.Errors ( DatalogError(..) ) where + +import Control.Exception +import Data.Text ( Text ) +import Data.Typeable + +import Database.Datalog.Relation + +data DatalogError = SchemaError Relation + | RelationExistsError Text + | NoRelationError Relation + | MissingQueryError + | ExtraQueryError + | StratificationError + | RangeRestrictionViolation + | NonVariableInRuleHead + | NoVariableBinding Text + deriving (Typeable, Show) + +instance Exception DatalogError diff --git a/src/Database/Datalog/Evaluate.hs b/src/Database/Datalog/Evaluate.hs new file mode 100644 --- /dev/null +++ b/src/Database/Datalog/Evaluate.hs @@ -0,0 +1,387 @@ +{-# LANGUAGE BangPatterns, FlexibleContexts, ScopedTypeVariables #-} +-- | This module defines the evaluation strategy of the library. +-- +-- It currently uses a bottom-up semi-naive evaluator. +module Database.Datalog.Evaluate ( + applyRuleSet, + select + ) where + +import Control.Applicative +import Control.Failure +import Control.Monad ( foldM, liftM ) +import Control.Monad.ST.Strict +import Data.Graph +import Data.Hashable +import Data.HashMap.Strict ( HashMap ) +import qualified Data.HashMap.Strict as HM +import Data.Maybe ( fromMaybe ) +import Data.Monoid +import Data.Vector.Mutable ( STVector ) +import qualified Data.Vector.Mutable as V + +import Database.Datalog.Database +import Database.Datalog.Errors +import Database.Datalog.Rules + +import Debug.Trace +debug = flip trace + +-- | Bindings are vectors of values. Each variable in a rule is +-- assigned an index in the Bindings during the adornment process. +-- When evaluating a rule, if a free variable is encountered, all of +-- its possible values are entered at the index for that variable in a +-- Bindings vector. When a bound variable is encountered, its current +-- value is looked up from the Bindings. If that value does not match +-- the concrete tuple being examined, that tuple is rejected. +-- +-- The mapping of variable to index into the bindings vector is stored +-- in the Rule data structure. +newtype Bindings s a = Bindings (STVector s a) + + +-- | Apply a set of rules. All of the rules must have the same head +-- relation. This is what implements the semi-naive evaluation +-- strategy. For each rule of the form +-- +-- > T(x,y) |- G(x,z), T(z,y). +-- +-- simulate the rule +-- +-- > ΔT(x,y) |- G(x,z), ΔT(z,y). +-- +-- That is, at each step only look at the *new* tuples for each +-- recursive relation. The intuition is that, if a new tuple is to be +-- generated on the next step, it must reference a new tuple from this +-- step (otherwise it would have already been generated) If a relation +-- appears twice in a body: +-- +-- > T(x,y) |- T(x,z), T(z,y). +-- +-- we have to substitute ΔT once for *each* occurrence of T in the +-- body, with the other occurrences referencing the non-Δ table: +-- +-- > ΔT(x,y) |- ΔT(x,z), T(z,y). +-- > ΔT(x,y) |- T(x,z), ΔT(z,y). +-- +-- While collecting all of the new tuples (see projectLiteral), a new +-- Δ table is generated. +applyRuleSet :: (Failure DatalogError m, Eq a, Hashable a, Show a) + => Database a -> [Rule a] -> m (Database a) +applyRuleSet _ [] = error "applyRuleSet: Empty rule set not possible" +applyRuleSet db rss@(r:_) = return $ runST $ do + bss <- concat <$> mapM (applyRules db) (orderRules rss) + db' <- projectLiterals db h bss + return db' -- `debug` show db' + where + h = ruleHead r + +-- | Each of the lists of generated bindings has its own +-- ruleVariableMap, so zip them together so that project has them +-- paired up and ready to use. +-- +-- Apply a set of rules +applyRules :: (Eq a, Hashable a, Show a) + => Database a + -> [Rule a] + -> ST s [(Rule a, [Bindings s a])] +applyRules db rs = do + bs <- mapM (applyRule db) rs + return $ zip rs bs + +-- | Toplogically sort rules (with SCCs treated as a unit). This +-- means that dependency rules will be fired before the rules that +-- depend on them, which is the best evaluation order we can hope for. +orderRules :: forall a . (Eq a, Hashable a) => [Rule a] -> [[Rule a]] +orderRules rs = map toList (stronglyConnComp deps) + where + toList (AcyclicSCC r) = [r] + toList (CyclicSCC rss) = rss + toKeyM = HM.fromList (zip rs [0..]) + toKey :: Rule a -> Int + toKey r = fromMaybe (error "Missing toKeyM entry") $ HM.lookup r toKeyM + + deps = foldr toContext [] rs + toContext r@(Rule _ b _) acc = + -- All of the rules for a given relation are in the same SCC + -- stratum, so we will see them all in @rs@ + let brules = concatMap relationToRules b + in (r, toKey r, map toKey brules) : acc + relationToRules rel = filter (hasRelHead rel) rs + hasRelHead c (Rule h _ _) = + case c of + Literal ac -> adornedClauseRelation h == adornedClauseRelation ac + -- This should probably be impossible since negated terms + -- would be in a different stratum. + NegatedLiteral ac -> adornedClauseRelation h == adornedClauseRelation ac + _ -> False + +-- | A worker to apply a single rule to the database (producing a new +-- database). This handles deciding if we need to do any Δ-table +-- substitutions. If not, it just does a simple fold with +-- joinLiteral. +applyRule :: (Eq a, Hashable a, Show a) + => Database a -> Rule a -> ST s [Bindings s a] +applyRule db r = do + -- We need to substitute the ΔT table in for *one* occurrence of the + -- T relation in the rule body at a time. It must be substituted in at + -- *each* position where T appears. + case any (referencesRelation hr) b of + -- If the relation does not appear in the body at all, we don't + -- need to do the delta substitution. + False -> do + v0 <- V.new (HM.size m) + foldM (joinLiteral db) [Bindings v0] b + -- Otherwise, swap the delta table in for each each occurrence of + -- the relation in the body. + True -> concat <$> foldM (joinWithDeltaAt db hr b m) [] b + where + h = ruleHead r + hr = adornedClauseRelation h + b = ruleBody r + m = ruleVariableMap r + +-- | Return True if the given literal references the given Relation +referencesRelation:: Relation -> Literal AdornedClause a -> Bool +referencesRelation hrel rel = + case rel of + Literal l -> adornedClauseRelation l == hrel + NegatedLiteral l -> adornedClauseRelation l == hrel + _ -> False + +-- | The worker that substitutes a Δ-table for each clause referencing +-- the relation @hr@. +joinWithDeltaAt :: (Eq a, Hashable a) + => Database a + -> Relation + -> [Literal AdornedClause a] + -> HashMap k v + -> [[Bindings s a]] + -> Literal AdornedClause a + -> ST s [[Bindings s a]] +joinWithDeltaAt db hr b m acc c = + case referencesRelation hr c of + -- This clause doesn't reference the relation so don't do anything + False -> return acc + -- This clause does reference it, so we need to evaluate the + -- entire rule here. swapJoin handles substituting the Δ table + -- for the relation in this clause (see withDeltaRelation - it + -- makes a new database with the Δ swapped for the data of this + -- relation). + True -> do + v0 <- V.new (HM.size m) + bs <- foldM swapJoin [Bindings v0] b + return (bs : acc) + where + swapJoin bs thisClause = + case thisClause == c of + False -> joinLiteral db bs thisClause + True -> withDeltaRelation db hr $ \db' -> joinLiteral db' bs thisClause + +-- | Ensure that the relation named by the clause argument is in the +-- database. Get the DBRelation. Then fold over the Bindings, +-- constructing a tuple for each one (that is inserted into the +-- relation). Then build a new database with that relation replaced +-- with the new one. +projectLiterals :: (Eq a, Hashable a, Show a) + => Database a + -> AdornedClause a + -> [(Rule a, [Bindings s a])] + -> ST s (Database a) +projectLiterals db c bssMaps = do + let r = adornedClauseRelation c + rel = ensureDatabaseRelation db r (length (adornedClauseTerms c)) + rel' = resetRelationDelta rel + -- We reset the delta since we are computing the new delta for the + -- next iteration. The act of adding tuples to the relation + -- automatically computes the delta. + rel'' <- foldM (\irel (rule, bs) -> foldM (project rule) irel bs) rel' bssMaps + return $ replaceRelation db rel'' + where + project rule !r b = do + t <- bindingsToTuple (ruleHead rule) (ruleVariableMap rule) b + return $ addTupleToRelation r t + +-- | Determine if a PartialTuple and a concrete Tuple from the +-- database match. Walks the partial tuple (which is sorted by index) +-- and the current tuple in parallel and tries to avoid allocations as +-- much as possible. +tupleMatches :: (Eq a) => PartialTuple a -> Tuple a -> Bool +tupleMatches (PartialTuple pvs) (Tuple vs) = + parallelTupleWalk pvs vs + +parallelTupleWalk :: (Eq a) => [Maybe a] -> [a] -> Bool +parallelTupleWalk [] [] = True +parallelTupleWalk (p:ps) (v:vs) = + case p of + Nothing -> parallelTupleWalk ps vs + Just pv -> pv == v && parallelTupleWalk ps vs +parallelTupleWalk _ _ = error "Partial tuple length mismatch" + +{-# INLINE scanSpace #-} +-- | The common worker for 'select' and 'matchAny' +scanSpace :: (Eq a) + => ((Tuple a -> Bool) -> [Tuple a] -> b) + -> Database a + -> Relation + -> PartialTuple a + -> b +scanSpace f db p pt = f (tupleMatches pt) space + where + -- FIXME: This is where we use the index, if available. If not, + -- we have to fall back to a table scan. Instead of computing + -- indices up front, it may be best to only compute them on the + -- fly (and then only if they will be referenced again later). + -- They can be thrown away as soon as they can't be referenced + -- again. This will save storage and up-front costs. + + -- Note that the relation might not exist in the database here + -- because this is the first time data is being inferred for the + -- EDB. In that case, just start with empty data and the project + -- step will insert the table into the database for the next step. + space = fromMaybe mempty (dataForRelation db p) + +-- | Return all of the tuples in the given relation that match the +-- given PartialTuple +select :: (Eq a) => Database a -> Relation -> PartialTuple a -> [Tuple a] +select = scanSpace filter + +-- | Return true if any tuples in the given relation match the given +-- 'PartialTuple' +anyMatch :: (Eq a) => Database a -> Relation -> PartialTuple a -> Bool +anyMatch = scanSpace any + +{-# INLINE joinLiteralWith #-} +-- | The common worker for the non-conditional clause join functions. +joinLiteralWith :: AdornedClause a + -> [Bindings s a] + -> (Bindings s a -> PartialTuple a -> ST s [Bindings s a]) + -> ST s [Bindings s a] +joinLiteralWith c bs f = concatMapM (apply c f) bs + where + apply cl fn b = do + pt <- buildPartialTuple cl b + fn b pt + +-- | Join a literal with the current set of bindings. This can +-- increase the number of bindings (for a non-negated clause) or +-- decrease the number of bindings (for a negated or conditional +-- clause). +joinLiteral :: (Eq a, Hashable a) + => Database a + -> [Bindings s a] + -> Literal AdornedClause a + -> ST s [Bindings s a] +joinLiteral db bs (Literal c) = joinLiteralWith c bs (normalJoin db c) +joinLiteral db bs (NegatedLiteral c) = joinLiteralWith c bs (negatedJoin db c) +joinLiteral _ bs (ConditionalClause _ p vs m) = + foldM (applyJoinCondition p vs m) [] bs + +-- | Extract the values that the predicate requires from the current +-- bindings. Apply the predicate and if it returns True, retain the +-- set of bindings; otherwise, discard it. +applyJoinCondition :: (Eq a, Hashable a) + => ([a] -> Bool) + -> [Term a] + -> HashMap (Term a) Int + -> [Bindings s a] + -> Bindings s a + -> ST s [Bindings s a] +applyJoinCondition p vs m acc b@(Bindings binds) = do + vals <- mapM extractBinding vs + case p vals of + True -> return $! b : acc + False -> return acc + where + extractBinding t = + let Just ix = HM.lookup t m + in V.read binds ix + +-- | Non-negated join; it works by selecting all of the tuples +-- matching the input PartialTuple and then recording all of the newly +-- bound variable values (i.e., the free variables in the rule). This +-- produces one set of bindings for each possible value of the free +-- variables in the rule (or could be empty if there are no matching +-- tuples). +normalJoin :: (Eq a, Hashable a) => Database a -> AdornedClause a -> Bindings s a + -> PartialTuple a -> ST s [Bindings s a] +normalJoin db c binds pt = mapM (projectTupleOntoLiteral c binds) ts + where + ts = select db (adornedClauseRelation c) pt + +-- | Retain the input binding if there are no matches in the database +-- for the input PartialTuple. Otherwise reject it. +negatedJoin :: (Eq a, Hashable a) => Database a -> AdornedClause a -> Bindings s a + -> PartialTuple a -> ST s [Bindings s a] +negatedJoin db c binds pt = + case anyMatch db (adornedClauseRelation c) pt of + True -> return [] + False -> return [binds] + +-- | For each term in the clause, take it as a literal if it is bound +-- or is an atom. Otherwise, leave it as free (not mentioned in the +-- partial tuple). +buildPartialTuple :: AdornedClause a -> Bindings s a -> ST s (PartialTuple a) +buildPartialTuple c (Bindings bs) = + PartialTuple <$> mapM toPartial (adornedClauseTerms c) + where + toPartial ta = + case ta of + (Atom a, BoundAtom) -> return $! Just a + (_, Bound slot) -> do + b <- V.read bs slot + return $! Just b + _ -> return Nothing + + +-- | For each free variable in the tuple (according to the adorned +-- clause), enter its value into the input bindings +projectTupleOntoLiteral :: AdornedClause a -> Bindings s a -> Tuple a -> ST s (Bindings s a) +projectTupleOntoLiteral c (Bindings binds) (Tuple t) = do + -- We need a copy here because the input bindings are shared among + -- many calls to this function + b <- V.clone binds + let atoms = zip (adornedClauseTerms c) t + mapM_ (bindFreeVariable b) atoms + return $! Bindings b + where + bindFreeVariable b ((_, adornment), val) = + case adornment of + Free ix -> V.write b ix val + _ -> return () + +-- | Convert a set of variable bindings to a tuple that matches the +-- input clause (which should have all variables). This is basically +-- unifying variables with the head of the rule. +bindingsToTuple :: (Eq a, Hashable a, Show a) + => AdornedClause a + -> HashMap (Term a) Int + -> Bindings s a + -> ST s (Tuple a) +bindingsToTuple c vmap (Bindings bs) = do + vals <- mapM variableTermToValue (adornedClauseTerms c) + return $ Tuple vals + where + variableTermToValue (t, _) = + case HM.lookup t vmap of + Nothing -> error ("NonVariableInRuleHead " ++ show c ++ " " ++ show t ++ " " ++ show vmap) + Just ix -> V.read bs ix + + +-- Helpers + +{-# INLINE mapM' #-} +-- | This is an alternative definition of mapM that accumulates its +-- results on the heap instead of the stack. This should avoid some +-- stack overflows when processing some million+ element lists.. +mapM' :: (Monad m) => (a -> m b) -> [a] -> m [b] +mapM' f = go [] + where + go acc [] = return (reverse acc) + go acc (a:as) = do + x <- f a + go (x:acc) as + +{-# INLINE concatMapM #-} +concatMapM :: (Monad m) => (a -> m [b]) -> [a] -> m [b] +concatMapM f xs = liftM concat (mapM' f xs) diff --git a/src/Database/Datalog/MagicSets.hs b/src/Database/Datalog/MagicSets.hs new file mode 100644 --- /dev/null +++ b/src/Database/Datalog/MagicSets.hs @@ -0,0 +1,343 @@ +{-# LANGUAGE FlexibleContexts, BangPatterns #-} +module Database.Datalog.MagicSets ( magicSetsRules, seedDatabase ) where + +import Control.Failure +import Control.Monad ( MonadPlus(..), foldM ) +import Data.Hashable +import Data.HashMap.Strict ( HashMap ) +import qualified Data.HashMap.Strict as HM +import Data.HashSet ( HashSet ) +import qualified Data.HashSet as HS +import Data.List ( foldl' ) +import Data.Maybe ( fromMaybe ) +import Data.Monoid +import Data.Sequence ( Seq, (><), ViewL(..) ) +import qualified Data.Sequence as S +import Data.Text ( Text ) + +import Database.Datalog.Adornment +import Database.Datalog.Database +import Database.Datalog.Errors +import Database.Datalog.Relation +import Database.Datalog.Rules + +import Debug.Trace +debug = flip trace + +-- FIXME: All references to negated relations must refer to the +-- Rel[FFF] relation version because we don't transform those into +-- versions with bound variables + +seedDatabase :: (Failure DatalogError m, Eq a, Hashable a, Show a) + => Database a + -> [Rule a] + -> Query a + -> [(Text, a)] + -> m (Database a) +seedDatabase db0 rs (Query (Clause (Relation rname) ts)) bindings = do + (tup, bs) <- foldM toTuple ([], []) ts + let magicRel = MagicRelation (BindingPattern (reverse bs)) rname + r0 = ensureDatabaseRelation db0 magicRel (length tup) + -- If there is a rule that defines the magic relation, we need + -- to force the evaluator to evaluate that rule by toggling the + -- dirty bit (delta table). We do this by using + -- addTupleToRelation. If there is no rule defining the magic + -- table, we can't do that because the delta bit will never be + -- toggled off and the evaluator will loop forever. In that + -- case, we have to use addTupleToRelation' + r1 = case any (definesRelation magicRel) rs of + True -> addTupleToRelation r0 (Tuple (reverse tup)) + False -> addTupleToRelation' r0 (Tuple (reverse tup)) + return $! replaceRelation db0 r1 + where + toTuple acc@(tacc, bacc) t = + case t of + Atom a -> return (a : tacc, B : bacc) + BindVar name -> + case lookup name bindings of + Nothing -> failure (NoVariableBinding name) + Just v -> return (v : tacc, B : bacc) + LogicVar _ -> return (tacc, F : bacc) + FreshVar _ -> return (tacc, F : bacc) + Anything -> error "Anything should be removed before seedDatabase" + +definesRelation :: Relation -> Rule a -> Bool +definesRelation r (Rule ac _ _) = adornedClauseRelation ac == r + +-- | Returns the rules generated by the magic sets transformation +-- +-- If there are no BoundVars or Atoms in the query, don't perform the +-- transformation since it won't help much. +-- +-- Note that performing the simple magic sets transformation on a +-- negated literal can break stratification. For now, this +-- implementation will not compute magic sets for negated literals. +-- That is, if a relation appears as a negated literal, do not perform +-- the magic transformation on it. It isn't quite clear to me if it +-- is just literals appearing negated or all literals used to define +-- literals appearing negated. +-- +-- There is an algorithm in +-- +-- > I. Balbin, G.S. Port, K. Ramamohanarao, K. Meenakshi, Efficient bottom-up computation of queries on stratified databases, The Journal of Logic Programming, Volume 11, Issues 3–4, October–November 1991, Pages 295-344, ISSN 0743-1066, 10.1016/0743-1066(91)90030-S. +-- > (http://www.sciencedirect.com/science/article/pii/074310669190030S) +-- +-- that handles magic for negated literals. +magicSetsRules :: (Failure DatalogError m, Hashable a, Eq a, Show a) + => Query a -- ^ The goal query + -> [(Clause a, [Literal Clause a])] -- ^ The user-provided rules + -> m [Rule a] +magicSetsRules q rs = + -- mapM adornRule rs + transformRules (S.singleton (queryPattern q)) mempty + where + -- These cannot be transformed + negatedRelations = foldr collectNegatedRelations mempty rs + -- Any relations in this list are inferred by rules and are + -- therefore eligible for the magic transformation (relations + -- in the fact database are not). + rawRules = foldr groupRules mempty rs + groupRules r = HM.insertWith (++) (clauseRelation (fst r)) [r] + inferredRelations = HS.fromList $ HM.keys rawRules + + isInferred :: QueryPattern -> Bool + isInferred p = HS.member (queryPatternRelation p) inferredRelations + + transformRules !worklist !generated = + case S.viewl worklist of + EmptyL -> do + let filteredRules = concat (HM.elems generated) + recPreds = HS.fromList $ map queryPatternRelation (HM.keys generated) + magicFilterTables = concatMap (toMagicFilterTable recPreds) filteredRules + mapM adornRule (map fst filteredRules ++ magicFilterTables) + elt :< rest -> + case HM.lookup elt generated of + -- Already processed this binding pattern + Just _ -> transformRules rest generated + Nothing -> do + let matchingRules = fromMaybe (error "No rules for pattern") $ HM.lookup (queryPatternRelation elt) rawRules + (magic, newWork) <- foldM (magicTransform elt) (mempty, mempty) matchingRules + transformRules (rest >< newWork) (HM.insert elt magic generated) + +-- The QueryPattern doesn't affect the adornments added for the +-- sideways information passing strategy (for that, the terms in the +-- head area *always* bound). The QueryPattern is separate and is +-- only used to compute other QueryPatterns for the worklist and to +-- determine whether or not magic needs to be applied. + magicTransform :: (Failure DatalogError m, Hashable a, Eq a, Show a) + => QueryPattern + -> ([((Clause a, [Literal Clause a]), [QueryPattern])], Seq QueryPattern) + -> (Clause a, [Literal Clause a]) + -> m ([((Clause a, [Literal Clause a]), [QueryPattern])], Seq QueryPattern) + magicTransform bp (newRules, work) rawRule@(c, lits) = do + let hasB = hasBinding bp + isNeg = HS.member (clauseRelation c) negatedRelations + bodyBindingPattern = reverse $ snd $ foldl' bindVars (patternToInitialMap bp c, []) lits + adornedLits = zip lits bodyBindingPattern + newDeps = filter isInferred bodyBindingPattern + newWork = work >< S.fromList newDeps + case not hasB || isNeg of + True -> do + -- If a rule has no bindings in the head (or has a + -- negation), we don't do the magic transformation. We + -- still need to make sure all of its reachable literals are + -- processed, though. + return ((rawRule, []) : newRules, newWork) + False -> do + let (mf, mp) = buildMagicFilter bp c + return (((c, mf : lits), mp : bodyBindingPattern) : newRules, newWork) + +-- | For each literal referencing a recursive relation (even if it is +-- recursive in a different rule), generate a magic filter table +-- definition rule for it. +toMagicFilterTable :: (Eq a) + => HashSet Relation + -> ((Clause a, [Literal Clause a]), [QueryPattern]) + -> [(Clause a, [Literal Clause a])] +toMagicFilterTable ps ((c, lits), qps) = + map (buildMagicFilterRule lits) (filter (isRecPred . fst) body) + where + body = zip lits qps + isRecPred l = + case l of + Literal (Clause r _) -> r `HS.member` ps + _ -> False + +-- | Take a binding pattern and a rule head and create its magic +-- filter literal. The magic filter literal is the head clause +-- changed to reference a magic version of the same relation and with +-- the free columns deleted. +buildMagicFilter :: QueryPattern -> Clause a -> (Literal Clause a, QueryPattern) +buildMagicFilter qp (Clause (Relation t) ts) = + (Literal (Clause mrel retainedTs), QueryPattern mrel (BindingPattern (map (const F) retainedTs))) + where + mrel = MagicRelation bp t + bp = queryPatternBindings qp + retainedTs = takeBoundTerms qp ts +buildMagicFilter _ _ = error "Cannot have a magic relation yet" + +takeBoundTerms :: QueryPattern -> [Term a] -> [Term a] +takeBoundTerms (QueryPattern _ qp) ts = + map snd retainedTuples + where + allTuples = zip (bindingPattern qp) ts + retainedTuples = filter ((==B) . fst) allTuples + +-- | For each occurrence of the head clause in a literal, generate a +-- rule defining the magic filter. +-- +-- To do that for occurrence O, +-- +-- 1) Delete everything to the right of O in the body +-- +-- 2) Turn O into a magic clause and delete its free columns +-- +-- 3) Replace the head with O +buildMagicFilterRule :: (Eq a) + => [Literal Clause a] + -> (Literal Clause a, QueryPattern) + -> (Clause a, [Literal Clause a]) +buildMagicFilterRule lits (lc@(Literal c), qp) = + let retainedLits = takeWhile (/= lc) lits + retainedTerms = takeBoundTerms qp (clauseTerms c) + Relation relName = clauseRelation c + h = Clause (MagicRelation (queryPatternBindings qp) relName) retainedTerms + in (h, retainedLits) + + +bindVars :: (Eq a, Hashable a) + => (HashSet (Term a), [QueryPattern]) + -> Literal Clause a + -> (HashSet (Term a), [QueryPattern]) +bindVars acc@(alreadyBound, patts) l = + case l of + ConditionalClause _ _ _ _ -> acc + Literal (Clause r ts) -> + let (binds, qp) = foldl' bindVar (alreadyBound, []) ts + in (binds, QueryPattern r (BindingPattern (reverse qp)) : patts) + -- For now, we treat all variables in a negated literal as Free + -- because we don't want to generate any magic clauses for them + -- (that can break stratification). Treating them all as free + -- here gets them properly skipped later. + NegatedLiteral (Clause r ts) -> + let qp = map (const F) ts + in (alreadyBound, QueryPattern r (BindingPattern qp) : patts) + where + bindVar (bindings, bs) t = + case t `HS.member` bindings of + True -> (bindings, B : bs) + False -> + case t of + LogicVar _ -> (HS.insert t bindings, F : bs) + Anything -> error "Wildcard variables should have been rewritten already" + FreshVar _ -> (HS.insert t bindings, F : bs) + BindVar _ -> (bindings, B : bs) + Atom _ -> (bindings, B : bs) + + +patternToInitialMap :: (Eq a, Hashable a) => QueryPattern -> Clause a -> HashSet (Term a) +patternToInitialMap qp (Clause _ ts) = + HS.fromList $ takeBoundTerms qp ts + +data QueryPattern = QueryPattern { queryPatternRelation :: Relation + , queryPatternBindings :: BindingPattern + } + deriving (Eq, Show) + +instance Hashable QueryPattern where + hashWithSalt s (QueryPattern r bs) = + s `hashWithSalt` r `hashWithSalt` bs + +hasBinding :: QueryPattern -> Bool +hasBinding (QueryPattern _ bs) = any (==B) (bindingPattern bs) + +queryPattern :: Query a -> QueryPattern +queryPattern (Query c) = + QueryPattern (clauseRelation c) $ BindingPattern (map toBinding (clauseTerms c)) + where + toBinding t = + case t of + Atom _ -> B + BindVar _ -> B + LogicVar _ -> F + Anything -> F + FreshVar _ -> F + +-- If the input query binding doesn't have any bound elements, the +-- rule gets no magic. + +-- FIXME: This would be better if dead rules couldn't affect it... +-- a dead rule with a negation will be a problem. +collectNegatedRelations :: (Clause a, [Literal Clause a]) + -> HashSet Relation + -> HashSet Relation +collectNegatedRelations (_, cs) acc = + foldr addIfNegated acc cs + where + addIfNegated (NegatedLiteral (Clause h _)) s = HS.insert h s + addIfNegated _ s = s + +-- If the rule ends up with multiple binding patterns for the +-- recursive rule, the rule needs to be split. This means that, for +-- each binding pattern, the full set of rules defining that relation +-- must be duplicated + +-- If the query has a bound literal, that influences the rules it +-- corresponds to. Other rules are not affected. Those positions +-- bound in the query are bound in the associated rules. +-- +-- Note: all variables in the head must appear in the body +adornRule :: (Failure DatalogError m, Eq a, Hashable a) + => (Clause a, [Literal Clause a]) -> m (Rule a) +adornRule (hd, lits) = do + (vmap, lits') <- mapAccumM adornLiteral mempty lits + (allVars, Literal hd') <- adornLiteral vmap (Literal hd) + let headVars = HS.fromList (clauseTerms hd) + -- FIXME: This test isn't actually strict enough. All head vars + -- must appear in a non-negative literal + case headVars `HS.difference` (HS.fromList (HM.keys allVars)) == mempty of + True -> return $! Rule hd' lits' allVars + False -> failure RangeRestrictionViolation + +adornLiteral :: (Failure DatalogError m, Eq a, Hashable a) + => HashMap (Term a) Int + -> Literal Clause a + -> m (HashMap (Term a) Int, Literal AdornedClause a) +adornLiteral boundVars l = + case l of + Literal c -> adornClause Literal c + NegatedLiteral c -> adornClause NegatedLiteral c + ConditionalClause cid f ts _ -> + return (boundVars, ConditionalClause cid f ts boundVars) + where + adornClause constructor (Clause p ts) = do + (bound', ts') <- mapAccumM adornTerm boundVars ts + let c' = constructor $ AdornedClause p ts' + return (bound', c') + adornTerm bvs t = + case t of + BindVar _ -> error "Bind variables are only allowed in queries" + Anything -> error "Anything should have been removed already" + -- Atoms are always bound + Atom _ -> return (bvs, (t, BoundAtom)) + LogicVar _ -> + -- The first occurrence is Free, while the rest are Bound + case HM.lookup t bvs of + Just ix -> return (bvs, (t, Bound ix)) + Nothing -> + let ix = HM.size bvs + in return (HM.insert t ix bvs, (t, Free ix)) + FreshVar _ -> + let ix = HM.size bvs + in return (HM.insert t ix bvs, (t, Free ix)) + +-- Helpers missing from the standard libraries + +{-# INLINE mapAccumM #-} +-- | Monadic mapAccumL +mapAccumM :: (Monad m, MonadPlus p) => (acc -> x -> m (acc, y)) -> acc -> [x] -> m (acc, p y) +mapAccumM _ z [] = return (z, mzero) +mapAccumM f z (x:xs) = do + (z', y) <- f z x + (z'', ys) <- mapAccumM f z' xs + return (z'', return y `mplus` ys) diff --git a/src/Database/Datalog/Relation.hs b/src/Database/Datalog/Relation.hs new file mode 100644 --- /dev/null +++ b/src/Database/Datalog/Relation.hs @@ -0,0 +1,40 @@ +module Database.Datalog.Relation ( + Relation(..) + ) where + +import Data.Hashable +import Data.Text ( Text, unpack ) +import Text.Printf + +import Database.Datalog.Adornment + +-- Let Relation be user exposed, use this for internal versions: +-- +-- data InternalRelation = InternalRelation BindingPattern Text +-- | MagicRelation BindingPattern Text + + +-- | A wrapper to expose the relation name to callers without +-- revealing details of its implementation +data Relation = Relation Text + | MagicRelation BindingPattern Text + deriving (Eq, Ord) + +instance Show Relation where + show (Relation t) = unpack t + show (MagicRelation bs t) = printf "Magic_%s[%s]" (unpack t) (show bs) + +-- FIXME: May need a new relation that tracks its binding pattern, +-- too. This is probably important for cases where the same relation +-- appears in the same body literal with different binding patterns in +-- a given rule. These seem like they should be referencing different +-- tables... +-- +-- The transformRules step will have to be the one to do the +-- translation + +instance Hashable Relation where + hashWithSalt s (Relation t) = + s `hashWithSalt` t `hashWithSalt` (99 :: Int) + hashWithSalt s (MagicRelation p t) = + s `hashWithSalt` p `hashWithSalt` (2 :: Int) diff --git a/src/Database/Datalog/Rules.hs b/src/Database/Datalog/Rules.hs new file mode 100644 --- /dev/null +++ b/src/Database/Datalog/Rules.hs @@ -0,0 +1,379 @@ +{-# LANGUAGE FlexibleContexts, BangPatterns #-} +-- | FIXME: Change the adornment/query building process such that +-- conditional clauses are always processed last. This is necessary +-- so that all variables are bound. +-- +-- FIXME: Add an assertion to say that ConditionalClauses cannot have +-- Free variables. +module Database.Datalog.Rules ( + Adornment(..), + Term(..), + Clause(..), + AdornedClause(..), + Rule(..), + Literal(..), + Query(..), + QueryBuilder, + PartialTuple(..), + (|-), + assertRule, + relationPredicateFromName, + inferencePredicate, + ruleRelations, + issueQuery, + runQuery, + queryToPartialTuple, + queryPredicate, + lit, + negLit, + cond1, + cond2, + cond3, + cond4, + cond5, + bindQuery, + partitionRules + ) where + +import Control.Failure +import Control.Monad.Trans.Class +import Control.Monad.Trans.State.Strict +import Data.Function ( on ) +import Data.Hashable +import Data.HashMap.Strict ( HashMap ) +import qualified Data.HashMap.Strict as HM +import Data.List ( intercalate, groupBy, sortBy ) +import Data.Maybe ( mapMaybe ) +import Data.Monoid +import Data.Text ( Text ) +import qualified Data.Text as T +import Text.Printf + +import Database.Datalog.Adornment +import Database.Datalog.Relation +import Database.Datalog.Errors +import Database.Datalog.Database + +-- import Debug.Trace +-- debug = flip trace + +data QueryState a = QueryState { intensionalDatabase :: Database a + , conditionalIdSource :: Int + , queryRules :: [(Clause a, [Literal Clause a])] + } + +-- | The Monad in which queries are constructed and rules are declared +type QueryBuilder m a = StateT (QueryState a) m + +nextConditionalId :: (Failure DatalogError m) => QueryBuilder m a Int +nextConditionalId = do + s <- get + let cid = conditionalIdSource s + put s { conditionalIdSource = cid + 1 } + return cid + +data Term a = LogicVar !Text + -- ^ A basic logic variable. Equality is based on the + -- variable name. + | BindVar !Text + -- ^ A special variable available in queries that can be + -- bound at query execution time + | Anything + -- ^ A term that is allowed to take any value (this is + -- sugar for a fresh logic variable) + | Atom a + -- ^ A user-provided literal from the domain a + | FreshVar !Int + -- ^ A fresh logic variable, generated internally for + -- each Anything occurrence. Not exposed to the user + +instance (Show a) => Show (Term a) where + show (LogicVar t) = T.unpack t + show (BindVar t) = "??" ++ T.unpack t + show (Atom a) = show a + show Anything = "*" + show (FreshVar _) = "*" + +instance (Hashable a) => Hashable (Term a) where + hashWithSalt s (LogicVar t) = + s `hashWithSalt` t `hashWithSalt` (1 :: Int) + hashWithSalt s (BindVar t) = + s `hashWithSalt` t `hashWithSalt` (2 :: Int) + hashWithSalt s (Atom a) = s `hashWithSalt` a + hashWithSalt s Anything = s `hashWithSalt` (99 :: Int) + hashWithSalt s (FreshVar i) = + s `hashWithSalt` i `hashWithSalt` (22 :: Int) + +instance (Eq a) => Eq (Term a) where + (LogicVar t1) == (LogicVar t2) = t1 == t2 + (BindVar t1) == (BindVar t2) = t1 == t2 + (Atom a1) == (Atom a2) = a1 == a2 + Anything == Anything = True + FreshVar i1 == FreshVar i2 = i1 == i2 + _ == _ = False + +data Clause a = Clause { clauseRelation :: Relation + , clauseTerms :: [Term a] + } + +instance (Eq a) => Eq (Clause a) where + (Clause r1 ts1) == (Clause r2 ts2) = r1 == r2 && ts1 == ts2 + +instance (Show a) => Show (Clause a) where + show (Clause p ts) = + printf "%s(%s)" (show p) (intercalate ", " (map show ts)) + + +data AdornedClause a = AdornedClause { adornedClauseRelation :: Relation + , adornedClauseTerms :: [(Term a, Adornment)] + } + +instance (Eq a) => Eq (AdornedClause a) where + (AdornedClause r1 cs1) == (AdornedClause r2 cs2) = r1 == r2 && cs1 == cs2 + +instance (Hashable a) => Hashable (AdornedClause a) where + hashWithSalt s (AdornedClause r ts) = + s `hashWithSalt` r `hashWithSalt` ts + +instance (Show a) => Show (AdornedClause a) where + show (AdornedClause p ats) = + printf "%s(%s)" (show p) (intercalate ", " (map showAT ats)) + where + showAT (t, a) = printf "%s[%s]" (show t) (show a) + +-- | Body clauses can be normal clauses, negated clauses, or +-- conditionals. Conditionals are arbitrary-arity (via a list) +-- functions over literals and logic variables. +data Literal ctype a = Literal (ctype a) + | NegatedLiteral (ctype a) + | ConditionalClause Int ([a] -> Bool) [Term a] (HashMap (Term a) Int) + +-- | This equality instance is complicated because conditional clauses +-- contain functions. We assign a unique id at conditional clause +-- creation time so they have identity and we can compare on that. +-- Rules from different queries cannot be compared safely, but that +-- shouldn't be a problem because there isn't really a way to sneak a +-- rule reference out of a query. If there is a shady way to do so, +-- don't because it will be bad. +instance (Eq a, Eq (ctype a)) => Eq (Literal ctype a) where + (Literal c1) == (Literal c2) = c1 == c2 + (NegatedLiteral c1) == (NegatedLiteral c2) = c1 == c2 + (ConditionalClause cid1 _ _ _) == (ConditionalClause cid2 _ _ _) = cid1 == cid2 + _ == _ = False + +instance (Hashable a, Hashable (ctype a)) => Hashable (Literal ctype a) where + hashWithSalt s (Literal c) = + s `hashWithSalt` c `hashWithSalt` (1 :: Int) + hashWithSalt s (NegatedLiteral c) = + s `hashWithSalt` c `hashWithSalt` (2 :: Int) + hashWithSalt s (ConditionalClause cid _ ts vm) = + s `hashWithSalt` cid `hashWithSalt` ts `hashWithSalt` HM.size vm + +lit :: (Failure DatalogError m) => Relation -> [Term a] -> QueryBuilder m a (Literal Clause a) +lit p ts = return $ Literal $ Clause p ts + +negLit :: (Failure DatalogError m) => Relation -> [Term a] -> QueryBuilder m a (Literal Clause a) +negLit p ts = return $ NegatedLiteral $ Clause p ts + +cond1 :: (Failure DatalogError m, Eq a, Hashable a) + => (a -> Bool) + -> Term a + -> QueryBuilder m a (Literal Clause a) +cond1 p t = do + cid <- nextConditionalId + return $ ConditionalClause cid (\[x] -> p x) [t] mempty + +cond2 :: (Failure DatalogError m, Eq a, Hashable a) + => (a -> a -> Bool) + -> (Term a, Term a) + -> QueryBuilder m a (Literal Clause a) +cond2 p (t1, t2) = do + cid <- nextConditionalId + return $ ConditionalClause cid (\[x1, x2] -> p x1 x2) [t1, t2] mempty + + +cond3 :: (Failure DatalogError m, Eq a, Hashable a) + => (a -> a -> a -> Bool) + -> (Term a, Term a, Term a) + -> QueryBuilder m a (Literal Clause a) +cond3 p (t1, t2, t3) = do + cid <- nextConditionalId + return $ ConditionalClause cid (\[x1, x2, x3] -> p x1 x2 x3) [t1, t2, t3] mempty + +cond4 :: (Failure DatalogError m, Eq a, Hashable a) + => (a -> a -> a -> a -> Bool) + -> (Term a, Term a, Term a, Term a) + -> QueryBuilder m a (Literal Clause a) +cond4 p (t1, t2, t3, t4) = do + cid <- nextConditionalId + return $ ConditionalClause cid (\[x1, x2, x3, x4] -> p x1 x2 x3 x4) [t1, t2, t3, t4] mempty + +cond5 :: (Failure DatalogError m, Eq a, Hashable a) + => (a -> a -> a -> a -> a -> Bool) + -> (Term a, Term a, Term a, Term a, Term a) + -> QueryBuilder m a (Literal Clause a) +cond5 p (t1, t2, t3, t4, t5) = do + cid <- nextConditionalId + return $ ConditionalClause cid (\[x1, x2, x3, x4, x5] -> p x1 x2 x3 x4 x5) [t1, t2, t3, t4, t5] mempty + +instance (Show a, Show (ctype a)) => Show (Literal ctype a) where + show (Literal c) = show c + show (NegatedLiteral c) = '~' : show c + show (ConditionalClause _ _ ts _) = printf "f(%s)" (show ts) + +-- | A rule has a head and body clauses. Body clauses can be normal +-- clauses, negated clauses, or conditionals. +data Rule a = Rule { ruleHead :: AdornedClause a + , ruleBody :: [Literal AdornedClause a] + , ruleVariableMap :: HashMap (Term a) Int + } + +instance (Show a) => Show (Rule a) where + show (Rule h b _) = printf "%s |- %s" (show h) (intercalate ", " (map show b)) + +instance (Eq a) => Eq (Rule a) where + (Rule h1 b1 vms1) == (Rule h2 b2 vms2) = + h1 == h2 && b1 == b2 && vms1 == vms2 + +instance (Hashable a) => Hashable (Rule a) where + hashWithSalt s (Rule h b vms) = + s `hashWithSalt` h `hashWithSalt` b `hashWithSalt` HM.size vms + +newtype Query a = Query { unQuery :: Clause a } + +infixr 0 |- + +-- | Assert a rule +-- +-- FIXME: Check to make sure that clause arities match their declared +-- schema. +(|-), assertRule :: (Failure DatalogError m) + => (Relation, [Term a]) -- ^ The rule head + -> [QueryBuilder m a (Literal Clause a)] -- ^ Body literals + -> QueryBuilder m a () +(|-) = assertRule +assertRule (p, ts) b = do + -- FIXME: Assert that Anything does not appear in the head terms + -- (that is a range restriction violation). Also check the range + -- restriction here. + b' <- sequence b + let h = Clause p ts + b'' = fst $ foldr freshenVars ([], [0..]) b' + s <- get + put s { queryRules = (h, b'') : queryRules s } + +-- | Replace all instances of Anything with a FreshVar with a unique +-- (to the rule) index. This lets later evaluation stages ignore +-- these and just deal with clean FreshVars. +freshenVars :: Literal Clause a + -> ([Literal Clause a], [Int]) + -> ([Literal Clause a], [Int]) +freshenVars l (cs, ixSrc) = + case l of + ConditionalClause _ _ _ _ -> (l : cs, ixSrc) + Literal (Clause h ts) -> + let (ts', ixRest) = foldr freshen ([], ixSrc) ts + in (Literal (Clause h ts') : cs, ixRest) + NegatedLiteral (Clause h ts) -> + let (ts', ixRest) = foldr freshen ([], ixSrc) ts + in (NegatedLiteral (Clause h ts') : cs, ixRest) + where + freshen t (ts, src) = + case t of + Anything -> (FreshVar (head src) : ts, tail src) + _ -> (t : ts, src) + +-- FIXME: Unify these and require inferred relations to be declared in +-- the schema at db construction time. That also gives an opportunity +-- to name the columns + +-- | Retrieve a Relation handle from the IDB. If the Relation does +-- not exist, an error will be raised. +relationPredicateFromName :: (Failure DatalogError m) + => Text -> QueryBuilder m a Relation +relationPredicateFromName name = do + let rel = Relation name + idb <- gets intensionalDatabase + case rel `elem` databaseRelations idb of + False -> lift $ failure (NoRelationError rel) + True -> return rel + +-- | Create a new predicate that will be referenced by an EDB rule +inferencePredicate :: (Failure DatalogError m) + => Text -> QueryBuilder m a Relation +inferencePredicate = return . Relation + +-- | A partial tuple records the atoms in a tuple (with their indices +-- in the tuple). These are primarily used in database queries. +newtype PartialTuple a = PartialTuple [Maybe a] + +instance (Show a) => Show (PartialTuple a) where + show (PartialTuple vs) = show $ map show vs + +-- | Convert a 'Query' into a 'PartialTuple' that can be used in a +-- 'select' of the IDB +queryToPartialTuple :: Query a -> PartialTuple a +queryToPartialTuple (Query c) = + PartialTuple $! map takeAtom ts + where + ts = clauseTerms c + takeAtom t = + case t of + Atom a -> Just a + _ -> Nothing + + + +literalClauseRelation :: Literal AdornedClause a -> Maybe Relation +literalClauseRelation bc = + case bc of + Literal c -> Just $ adornedClauseRelation c + NegatedLiteral c -> Just $ adornedClauseRelation c + _ -> Nothing + +ruleRelations :: Rule a -> [Relation] +ruleRelations (Rule h bcs _) = adornedClauseRelation h : mapMaybe literalClauseRelation bcs + +-- | Turn a Clause into a Query. This is meant to be the last +-- statement in a QueryBuilder monad. +issueQuery :: (Failure DatalogError m) => Relation -> [Term a] -> QueryBuilder m a (Query a) +issueQuery r ts = return $ Query $ Clause r ts + + +-- | Run the QueryBuilder action to build a query and initial rule +-- database +-- +-- Rules are adorned (marking each variable as Free or Bound as they +-- appear) before being returned. +runQuery :: (Failure DatalogError m, Eq a, Hashable a) + => QueryBuilder m a (Query a) -> Database a -> m (Query a, [(Clause a, [Literal Clause a])]) +runQuery qm idb = do + (q, QueryState _ _ rs) <- runStateT qm (QueryState idb 0 []) + return (q, rs) + +-- | Group rules by their head relations. This is needed to perform +-- semi-naive evaluation easily. +partitionRules :: [Rule a] -> [[Rule a]] +partitionRules = groupBy gcmp . sortBy scmp + where + scmp = compare `on` (adornedClauseRelation . ruleHead) + gcmp = (==) `on` (adornedClauseRelation . ruleHead) + +queryPredicate :: Query a -> Relation +queryPredicate = clauseRelation . unQuery + +-- | Apply bindings to a query +bindQuery :: Query a -> [(Text, a)] -> Query a +bindQuery (Query (Clause r ts)) bs = + Query $ Clause r $ foldr applyBinding [] ts + where + applyBinding t acc = + case t of + LogicVar _ -> t : acc + BindVar name -> + case lookup name bs of + Nothing -> error ("No binding provided for BindVar " ++ show name) + Just b -> Atom b : acc + Anything -> t : acc + Atom _ -> t : acc + FreshVar _ -> error "Users cannot provide FreshVars" diff --git a/src/Database/Datalog/Stratification.hs b/src/Database/Datalog/Stratification.hs new file mode 100644 --- /dev/null +++ b/src/Database/Datalog/Stratification.hs @@ -0,0 +1,111 @@ +{-# LANGUAGE FlexibleContexts #-} +module Database.Datalog.Stratification ( stratifyRules ) where + +import Control.Failure +import Data.HashMap.Strict ( HashMap ) +import qualified Data.HashMap.Strict as HM +import Data.HashSet ( HashSet ) +import qualified Data.HashSet as HS +import Data.IntMap ( IntMap ) +import qualified Data.IntMap as IM +import Data.Monoid +import Data.Graph + +import Database.Datalog.Database +import Database.Datalog.Errors +import Database.Datalog.Rules + +-- | Stratify the input rules and magic rules; the rules should be +-- processed to a fixed-point in this order +stratifyRules :: (Failure DatalogError m) => [Rule a] -> m [[Rule a]] +stratifyRules rs = + case all hasNoInternalNegation comps of + False -> failure StratificationError + True -> return $ IM.elems $ foldr (assignRule stratumNumbers) mempty rs + where + (ctxts, negatedEdges) = makeRuleDependencies rs + comps = stronglyConnCompR ctxts + + hasNoInternalNegation ns = + case ns of + AcyclicSCC _ -> True + CyclicSCC vs -> + let compNodes = HS.fromList $ map (\(_, x, _) -> x) vs + internalEdges = foldr (isInternalEdge compNodes) mempty vs + in HS.null $ HS.intersection internalEdges negatedEdges + + stratumNumbers = foldr (computeStratumNumbers negatedEdges) mempty comps + +isInternalEdge :: HashSet Relation -> Context -> HashSet (Relation, Relation) -> HashSet (Relation, Relation) +isInternalEdge compNodes (_, n, tgts) acc = + acc `HS.union` HS.map (\t -> (n, t)) itgts + where + itgts = HS.fromList tgts `HS.intersection` compNodes + +-- | Given the stratum number for each Relation, place rules headed +-- with that Relation in their respective strata. This is +-- represented with an IntMap, which keeps the strata sorted. This is +-- expanded into a different form by the caller. +assignRule :: HashMap Relation Int -> Rule a -> IntMap [Rule a] -> IntMap [Rule a] +assignRule stratumNumbers r = IM.insertWith (++) snum [r] + where + headPred = adornedClauseRelation (ruleHead r) + Just snum = HM.lookup headPred stratumNumbers + +-- | The stratum number of each member of an SCC will be the same +-- because all rules in an SCC depend on one another, and the stratum +-- number is the maximum number of negations reachable from a node. +-- since they all depend on one another and there can't be negations +-- within an SCC, all rules in an SCC must have the same stratum +-- number (which makes sense - all members of an SCC need to be +-- re-evaluated until a fixed-point is reached). This makes the +-- stratum number computation easy - just take the maximum over all of +-- the rules in the SCC. +computeStratumNumber :: NegatedEdges -> HashMap Relation Int -> Context -> Int +computeStratumNumber negEdges m (_, r, deps) = + case deps of + [] -> 0 + -- deps is not empty; if a dependency is not present it must be in + -- this SCC and we can count it as zero because there are no + -- intervening negations. + deps' -> maximum $ map toStratNum deps' + where + toStratNum d = + case HS.member (r, d) negEdges of + True -> 1 + HM.lookupDefault 0 d m + False -> HM.lookupDefault 0 d m + + +-- | Assign a stratum number to each SCC. The stratum number is the +-- maximum number of negations reachable from a relation without +-- encountering a negation (negations within an SCC are impossible). +computeStratumNumbers :: NegatedEdges + -> SCC Context + -> HashMap Relation Int + -> HashMap Relation Int +computeStratumNumbers negEdges comp m = + case comp of + AcyclicSCC c@(r, _, _) -> HM.insert r (computeStratumNumber negEdges m c) m + CyclicSCC cs -> + -- The SCC can't be empty so maximum won't see an empty list + let sn = maximum $ map (computeStratumNumber negEdges m) cs + in foldr (\(r,_,_) acc -> HM.insert r sn acc) m cs + +type NegatedEdges = HashSet (Relation, Relation) +type Context = (Relation, Relation, [Relation]) + +makeRuleDependencies :: [Rule a] -> ([Context], NegatedEdges) +makeRuleDependencies = toContexts . foldr addRuleDeps (mempty, mempty) + where + addRuleDeps (Rule (AdornedClause hrel _) b _) acc = + foldr (addLitDeps hrel) acc b + addLitDeps hrel l acc@(m, es) = + case l of + Literal (AdornedClause r _) -> + (HM.insertWith HS.union hrel (HS.singleton r) m, es) + NegatedLiteral (AdornedClause r _) -> + (HM.insertWith HS.union hrel (HS.singleton r) m, + HS.insert (hrel, r) es) + ConditionalClause _ _ _ _ -> acc + toContexts (dg, es) = (HM.foldrWithKey toContext [] dg, es) + toContext hr brs acc = (hr, hr, HS.toList brs) : acc diff --git a/tests/AncestorTest.hs b/tests/AncestorTest.hs new file mode 100644 --- /dev/null +++ b/tests/AncestorTest.hs @@ -0,0 +1,107 @@ +{-# LANGUAGE OverloadedStrings #-} +module Main ( main ) where + +import Data.Set ( fromList ) +import Data.Text ( Text ) +import Test.Framework ( defaultMain, testGroup, Test ) +import Test.Framework.Providers.HUnit +import Test.HUnit hiding ( Test ) + +import Database.Datalog + +main :: IO () +main = defaultMain tests + +tests :: [Test] +tests = [ testGroup "t1" [ testCase "1" t1 + , testCase "2" t2 + , testCase "3" t3 + , testCase "4" t4 + ] ] + +db1 :: Maybe (Database Text) +db1 = makeDatabase $ do + parentOf <- addRelation "parentOf" 2 + let facts :: [[Text]] + facts = [ [ "Bob", "Mary" ] + , [ "Sue", "Mary" ] + , [ "Mary", "John" ] + , [ "Joe", "John" ] + ] + mapM_ (assertFact parentOf) facts + +t1 :: Assertion +t1 = do + let Just db = db1 + res <- queryDatabase db q + assertEqual "t1" expected (fromList res) + where + expected = fromList [ ["Mary", "John"] + , ["Joe", "John"] + , ["Bob", "John"] + , ["Sue", "John"] + ] + q = do + parentOf <- relationPredicateFromName "parentOf" + ancestorOf <- inferencePredicate "ancestorOf" + let x = LogicVar "x" + y = LogicVar "y" + z = LogicVar "z" + (ancestorOf, [x, y]) |- [ lit parentOf [x, y] ] + (ancestorOf, [x, y]) |- [ lit parentOf [x, z], lit ancestorOf [z, y] ] + issueQuery ancestorOf [x, Atom "John" ] + +t2 :: Assertion +t2 = do + let Just db = db1 + res <- queryDatabase db q + assertEqual "t2" expected (fromList res) + where + expected = fromList [ ["Bob", "Mary"] + , ["Sue", "Mary"] + ] + q = do + parentOf <- relationPredicateFromName "parentOf" + ancestorOf <- inferencePredicate "ancestorOf" + let x = LogicVar "x" + y = LogicVar "y" + z = LogicVar "z" + (ancestorOf, [x, y]) |- [ lit parentOf [x, y] ] + (ancestorOf, [x, y]) |- [ lit parentOf [x, z], lit ancestorOf [z, y] ] + issueQuery ancestorOf [x, Atom "Mary" ] + +t3 :: Assertion +t3 = do + let Just db = db1 + res <- queryDatabase db q + assertEqual "t3" expected (fromList res) + where + expected = fromList [ ["Sue", "John"] + , ["Sue", "Mary"] + ] + q = do + parentOf <- relationPredicateFromName "parentOf" + ancestorOf <- inferencePredicate "ancestorOf" + let x = LogicVar "x" + y = LogicVar "y" + z = LogicVar "z" + (ancestorOf, [x, y]) |- [ lit parentOf [x, y] ] + (ancestorOf, [x, y]) |- [ lit parentOf [x, z], lit ancestorOf [z, y] ] + issueQuery ancestorOf [Atom "Sue", x ] + +t4 :: Assertion +t4 = do + let Just db = db1 + res <- queryDatabase db q + assertEqual "t4" expected (fromList res) + where + expected = fromList [] + q = do + parentOf <- relationPredicateFromName "parentOf" + ancestorOf <- inferencePredicate "ancestorOf" + let x = LogicVar "x" + y = LogicVar "y" + z = LogicVar "z" + (ancestorOf, [x, y]) |- [ lit parentOf [x, y] ] + (ancestorOf, [x, y]) |- [ lit parentOf [x, z], lit ancestorOf [z, y] ] + issueQuery ancestorOf [x, Atom "Bob"] diff --git a/tests/NQueens.hs b/tests/NQueens.hs new file mode 100644 --- /dev/null +++ b/tests/NQueens.hs @@ -0,0 +1,168 @@ +{-# LANGUAGE OverloadedStrings, FlexibleContexts #-} +module Main ( main ) where + +import Control.Monad ( forM_ ) +import Data.List ( sort ) +import qualified Data.Set as S +import Test.Framework ( defaultMain, testGroup, Test ) +import Test.Framework.Providers.HUnit +import Test.HUnit hiding ( Test ) + +import Database.Datalog + +main :: IO () +main = defaultMain tests + +tests :: [Test] +tests = [ testGroup "t1" [ testCase "4queens" t4 + , testCase "5queens" t5 + , testCase "6queens" t6 + ] ] + +type Position = (Int, Int) + +dbN :: (Failure DatalogError m) => Int -> m (Database Position) +dbN n = makeDatabase $ do + let posTuples = [ (x, y) | x <- [1..n], y <- [1..n] ] + position <- addRelation "position" 1 + forM_ posTuples $ \(x, y) -> assertFact position [ (x, y) ] + +-- Note, the restrictions on x and y equality also imply that the +-- position rule can't select the same position more than once in a +-- solution +posCanAttack :: Position -> Position -> Bool +posCanAttack (x1, y1) (x2, y2) = + x1 == x2 || y1 == y2 || (abs (x1 - x2) == abs (y1 - y2)) + +unique :: [[Position]] -> [[Position]] +unique = S.toList . S.fromList + +-- Return False if any position can attack any others +noneCanAttack :: [Position] -> Bool +noneCanAttack [] = True +noneCanAttack [_] = True +noneCanAttack (p:ps) = not (any (posCanAttack p) ps) && noneCanAttack ps + +t4 :: Assertion +t4 = do + db4 <- dbN 4 + res <- queryDatabase db4 q + let res' = unique $ map sort res + print res' + assertBool "t4" $ all noneCanAttack res' && length res' == 2 + where + q = do + position <- relationPredicateFromName "position" + canAttack <- inferencePredicate "canAttack" + let x = LogicVar "X" + y = LogicVar "Y" + (canAttack, [x, y]) |- [ lit position [x] + , lit position [y] + , cond2 posCanAttack (x, y) + ] + let p1 = LogicVar "P1" + p2 = LogicVar "P2" + p3 = LogicVar "P3" + p4 = LogicVar "P4" + queens <- inferencePredicate "queens" + (queens, [p1, p2, p3, p4]) |- [ lit position [p1] + , lit position [p2] + , negLit canAttack [p1, p2] + , lit position [p3] + , negLit canAttack [p1, p3] + , negLit canAttack [p2, p3] + , lit position [p4] + , negLit canAttack [p1, p4] + , negLit canAttack [p2, p4] + , negLit canAttack [p3, p4] + ] + issueQuery queens [p1, p2, p3, p4] + +t5 :: Assertion +t5 = do + db5 <- dbN 5 + res <- queryDatabase db5 q + let res' = unique $ map sort res + print res' + assertBool "t5" $ all noneCanAttack res' && length res' == 10 + where + q = do + position <- relationPredicateFromName "position" + canAttack <- inferencePredicate "canAttack" + let x = LogicVar "X" + y = LogicVar "Y" + (canAttack, [x, y]) |- [ lit position [x] + , lit position [y] + , cond2 posCanAttack (x, y) + ] + let p1 = LogicVar "P1" + p2 = LogicVar "P2" + p3 = LogicVar "P3" + p4 = LogicVar "P4" + p5 = LogicVar "P5" + queens <- inferencePredicate "queens" + (queens, [p1, p2, p3, p4, p5]) |- [ lit position [p1] + , lit position [p2] + , negLit canAttack [p1, p2] + , lit position [p3] + , negLit canAttack [p1, p3] + , negLit canAttack [p2, p3] + , lit position [p4] + , negLit canAttack [p1, p4] + , negLit canAttack [p2, p4] + , negLit canAttack [p3, p4] + , lit position [p5] + , negLit canAttack [p1, p5] + , negLit canAttack [p2, p5] + , negLit canAttack [p3, p5] + , negLit canAttack [p4, p5] + ] + issueQuery queens [p1, p2, p3, p4, p5] + +t6 :: Assertion +t6 = do + db6 <- dbN 6 + res <- queryDatabase db6 q + let res' = unique $ map sort res + print res' + assertBool "t6" $ all noneCanAttack res' && length res' == 4 + where + q = do + position <- relationPredicateFromName "position" + canAttack <- inferencePredicate "canAttack" + let x = LogicVar "X" + y = LogicVar "Y" + (canAttack, [x, y]) |- [ lit position [x] + , lit position [y] + , cond2 posCanAttack (x, y) + ] + let p1 = LogicVar "P1" + p2 = LogicVar "P2" + p3 = LogicVar "P3" + p4 = LogicVar "P4" + p5 = LogicVar "P5" + p6 = LogicVar "P6" + queens <- inferencePredicate "queens" + (queens, [p1, p2, p3, p4, p5, p6]) |- [ lit position [p1] + , lit position [p2] + , negLit canAttack [p1, p2] + , lit position [p3] + , negLit canAttack [p1, p3] + , negLit canAttack [p2, p3] + , lit position [p4] + , negLit canAttack [p1, p4] + , negLit canAttack [p2, p4] + , negLit canAttack [p3, p4] + , lit position [p5] + , negLit canAttack [p1, p5] + , negLit canAttack [p2, p5] + , negLit canAttack [p3, p5] + , negLit canAttack [p4, p5] + , lit position [p6] + , negLit canAttack [p1, p6] + , negLit canAttack [p2, p6] + , negLit canAttack [p3, p6] + , negLit canAttack [p4, p6] + , negLit canAttack [p5, p6] + ] + issueQuery queens [p1, p2, p3, p4, p5, p6] diff --git a/tests/WorksForTest.hs b/tests/WorksForTest.hs new file mode 100644 --- /dev/null +++ b/tests/WorksForTest.hs @@ -0,0 +1,222 @@ +{-# LANGUAGE OverloadedStrings, FlexibleContexts #-} +module Main ( main ) where + +import Data.Hashable +import Data.Set ( fromList ) +import Data.Text ( Text ) +import Test.Framework ( defaultMain, testGroup, Test ) +import Test.Framework.Providers.HUnit +import Test.HUnit hiding ( Test ) + +import Database.Datalog + +main :: IO () +main = defaultMain tests + +tests :: [Test] +tests = [ testGroup "t1" [ testCase "1" t1 + , testCase "2" t2 + , testCase "3" t3 + , testCase "4" t4 + ] + ] + +data WorkInfo = EID !Int -- id + | EN !Text -- Name + | EP !Text -- Position + | J !Text -- Job + | EA !Int + deriving (Eq, Ord, Show) + +instance Hashable WorkInfo where + hashWithSalt s (EID i) = s `hashWithSalt` i `hashWithSalt` (1 :: Int) + hashWithSalt s (EN n) = s `hashWithSalt` n `hashWithSalt` (2 :: Int) + hashWithSalt s (EP p) = s `hashWithSalt` p `hashWithSalt` (3 :: Int) + hashWithSalt s (J j) = s `hashWithSalt` j `hashWithSalt` (4 :: Int) + hashWithSalt s (EA a) = s `hashWithSalt` a `hashWithSalt` (5 :: Int) + +db1 :: Maybe (Database WorkInfo) +db1 = makeDatabase $ do + employee <- addRelation "employee" 4 + let emplFacts = [ [ EID 1, EN "Bob", EP "Boss", EA 51] + , [ EID 2, EN "Mary", EP "Chief Accountant", EA 31] + , [ EID 3, EN "John", EP "Accountant", EA 22 ] + , [ EID 4, EN "Sameer", EP "Chief Programmer", EA 34 ] + , [ EID 5, EN "Lilian", EP "Programmer", EA 24 ] + , [ EID 6, EN "Li", EP "Technician", EA 40 ] + , [ EID 7, EN "Fred", EP "Sales", EA 29 ] + , [ EID 8, EN "Brenda", EP "Sales", EA 27 ] + , [ EID 9, EN "Miki", EP "Project Management", EA 44 ] + , [ EID 10, EN "Albert", EP "Technician", EA 23 ] + ] + mapM_ (assertFact employee) emplFacts + + bossOf <- addRelation "bossOf" 2 + let bossFacts = [ [ EID 1, EID 2 ] + , [ EID 2, EID 3 ] + , [ EID 1, EID 4 ] + , [ EID 4, EID 5 ] + , [ EID 4, EID 6 ] + , [ EID 1, EID 7 ] + , [ EID 7, EID 8 ] + , [ EID 1, EID 9 ] + , [ EID 6, EID 10 ] + ] + mapM_ (assertFact bossOf) bossFacts + + canDo <- addRelation "canDo" 2 + let canDoFacts = [ [ EP "Boss", J "Management" ] + , [ EP "Accountant", J "Accounting" ] + , [ EP "Chief Accountant", J "Accounting" ] + , [ EP "Programmer", J "Programming" ] + , [ EP "Chief Programmer", J "Programming" ] + , [ EP "Technician", J "Server Support" ] + , [ EP "Sales", J "Sales" ] + , [ EP "Project Management", J "Project Management" ] + ] + mapM_ (assertFact canDo) canDoFacts + + jobCanBeDoneBy <- addRelation "jobCanBeDoneBy" 2 + let replaceFacts = [ [ J "PC Support", J "Server Support" ] + , [ J "PC Support", J "Programming" ] + , [ J "Payroll", J "Accounting" ] + ] + mapM_ (assertFact jobCanBeDoneBy) replaceFacts + + jobExceptions <- addRelation "jobExceptions" 2 + assertFact jobExceptions [ EID 4, J "PC Support" ] + +q1 :: (Failure DatalogError m) => QueryBuilder m WorkInfo (Query WorkInfo) +q1 = do + employee <- relationPredicateFromName "employee" + bossOf <- relationPredicateFromName "bossOf" + worksFor <- inferencePredicate "worksFor" + let x = LogicVar "X" + y = LogicVar "Y" + z = LogicVar "Z" + eid = LogicVar "E-ID" + bid = LogicVar "B-ID" + (worksFor, [x, y]) |- [ lit bossOf [bid, eid] + , lit employee [eid, x, Anything, Anything] + , lit employee [bid, y, Anything, Anything] + ] + (worksFor, [x, y]) |- [ lit worksFor [x, z] + , lit worksFor [z, y] + ] + issueQuery worksFor [ BindVar "name", x ] + +t1 :: Assertion +t1 = do + let Just db = db1 + Just qp = buildQueryPlan db q1 + + res <- executeQueryPlan qp db [("name", EN "Albert")] + assertEqual "t1" expected (fromList res) + where + expected = fromList [ [EN "Albert", EN "Li"] + , [EN "Albert", EN "Sameer"] + , [EN "Albert", EN "Bob"] + ] +t2 :: Assertion +t2 = do + let Just db = db1 + Just qp = buildQueryPlan db q1 + + res <- executeQueryPlan qp db [("name", EN "Lilian")] + assertEqual "t2" expected (fromList res) + where + expected = fromList [ [EN "Lilian", EN "Sameer"] + , [EN "Lilian", EN "Bob"] + ] + +q2 :: (Failure DatalogError m) => QueryBuilder m WorkInfo (Query WorkInfo) +q2 = do + employee <- relationPredicateFromName "employee" + bossOf <- relationPredicateFromName "bossOf" + worksFor <- inferencePredicate "worksFor" + worksForYoung <- inferencePredicate "worksForYoung" + let x = LogicVar "X" + y = LogicVar "Y" + z = LogicVar "Z" + age = LogicVar "Age" + eid = LogicVar "E-ID" + bid = LogicVar "B-ID" + (worksFor, [x, y]) |- [ lit bossOf [bid, eid] + , lit employee [eid, x, Anything, Anything] + , lit employee [bid, y, Anything, Anything] + ] + (worksFor, [x, y]) |- [ lit worksFor [x, z] + , lit worksFor [z, y] + ] + (worksForYoung, [x, y]) |- [ lit worksFor [x, y] + , lit employee [eid, y, Anything, age] + , cond1 (\(EA a) -> a < 49) age + ] + issueQuery worksForYoung [ BindVar "name", y ] + +t3 :: Assertion +t3 = do + let Just db = db1 + Just qp = buildQueryPlan db q2 + + res <- executeQueryPlan qp db [("name", EN "Lilian")] + assertEqual "t3" expected (fromList res) + where + expected = fromList [ [EN "Lilian", EN "Sameer"] + ] + + +q3 :: (Failure DatalogError m) => QueryBuilder m WorkInfo (Query WorkInfo) +q3 = do + employee <- relationPredicateFromName "employee" + bossOf <- relationPredicateFromName "bossOf" + worksFor <- inferencePredicate "worksFor" + empJobStar <- inferencePredicate "employeeJob*" + empJob <- inferencePredicate "employeeJob" + canDo <- relationPredicateFromName "canDo" + jobReplacement <- relationPredicateFromName "jobCanBeDoneBy" + jobExceptions <- relationPredicateFromName "jobExceptions" + bj <- inferencePredicate "bj" + let x = LogicVar "X" + y = LogicVar "Y" + z = LogicVar "Z" + jid = LogicVar "ID" + pos = LogicVar "Pos" + eid = LogicVar "E-ID" + bid = LogicVar "B-ID" + (worksFor, [x, y]) |- [ lit bossOf [bid, eid] + , lit employee [eid, x, Anything, Anything] + , lit employee [bid, y, Anything, Anything] + ] + (worksFor, [x, y]) |- [ lit worksFor [x, z] + , lit worksFor [z, y] + ] + (empJobStar, [x, y]) |- [ lit employee [Anything, x, pos, Anything] + , lit canDo [pos, y] + ] + (empJobStar, [x, y]) |- [ lit jobReplacement [y, z] + , lit empJobStar [x, z] + ] + (empJobStar, [x, y]) |- [ lit canDo [Anything, y] + , lit employee [Anything, x, Atom (EP "Boss"), Anything] + ] + (empJob, [x, y]) |- [ lit empJobStar [x, y] + , lit employee [jid, x, Anything, Anything] + , negLit jobExceptions [jid, y] + ] + --(bj, [x, y]) |- [ lit worksFor [x, y] + -- , negLit empJob [y, Atom (J "PC Support")] + -- ] + issueQuery empJob [ BindVar "name", x ] + +t4 :: Assertion +t4 = do + let Just db = db1 + Just qp = buildQueryPlan db q3 + + res <- executeQueryPlan qp db [("name", EN "Li")] + assertEqual "t4" expected (fromList res) + where + expected = fromList [ [EN "Li", J "PC Support"] + , [EN "Li", J "Server Support"] + ]