Skip to content

Commit

Permalink
rename to with/without and write a little documentation
Browse files Browse the repository at this point in the history
  • Loading branch information
@BrianHicks
BrianHicks committed May 12, 2021
1 parent 5480e88 commit e211d16
Show file tree
Hide file tree
Showing 2 changed files with 112 additions and 40 deletions.
84 changes: 78 additions & 6 deletions src/Database/Datalog.elm
View file
@@ -1,6 +1,6 @@
module Database.Datalog exposing
( Database, empty, Problem(..), insert, query
, Rule, rule, withMatching, withoutMatching, filter, planRule
, Rule, rule, with, without, filter, planRule
, Filter, eq, gt, lt, not_, or
, Term, var, int, string
)
Expand All @@ -9,7 +9,7 @@ module Database.Datalog exposing
@docs Database, empty, Problem, insert, query
@docs Rule, rule, withMatching, withoutMatching, filter, planRule
@docs Rule, rule, with, without, filter, planRule
@docs Filter, eq, gt, lt, not_, or
Expand Down Expand Up @@ -256,18 +256,90 @@ type Rule
= Rule Atom (List BodyAtom)


{-| Start making a new rule! You'll need to name it (the first argument)
and then name the fields you'll end up exporting.
Some rules to keep in mind:
- You have to provide at least one name.
- You have to bind every name you define using `with`.
If you have multiple rules with the same name, they'll be merged together
(for an example, see the docs for [`with`](#with).)
-}
rule : String -> List String -> Rule
rule name headVars =
Rule (Atom name (List.map Variable headVars)) []


withMatching : String -> List Term -> Rule -> Rule
withMatching name terms (Rule head body) =
{-| Add matches from the given name (TODO: table? rule? named tuple store?)
For example, if you have some greeks (Socrates, say) you can write a rule
like this to see which of them are mortal:
rule "mortal" [ "name" ]
|> with "greek" [ var "name" ]
It's fine to use this to set up recursive queries. For example, you could
compute reachability for all nodes in a graph using two rules like this:
[ rule "reachable" [ "a", "b" ]
|> with "link" [ var "a", var "b" ]
, rule "reachable" [ "a", "c" ]
|> with "link" [ var "a", var "b" ]
|> with "reachable" [ var "b", var "c" ]
]
If you introduce a variable in a `with` like that above, it's also fine!
-}
with : String -> List Term -> Rule -> Rule
with name terms (Rule head body) =
Rule head (BodyAtom Positive (Atom name terms) :: body)


withoutMatching : String -> List Term -> Rule -> Rule
withoutMatching name terms (Rule head body) =
{-| The opposite of [`with`](#with): remove any matching tuples based on
these names.
This has a few more rules than `with`, though:
- You can't introduce new names in a `without` (every name must be used
in a positive clause. If you could, we wouldn't have a way to know which
values are permissible and we'd have to invent stuff; a big no-no!)
- You can't use `without` recursively (if you could, you could get
inconsistent outcomes based on which rules you evaluate first.)
If you've used another datalog implementation before: this is just negation,
and the rules are more-or-less the same.
Here's an example of computing all the nodes in a graph that _aren't_
reachable from each other:
[ -- first, define `reachable` as in the example in `with`:
rule "reachable" [ "a", "b" ]
|> with "link" [ var "a", var "b" ]
, rule "reachable" [ "a", "c" ]
|> with "link" [ var "a", var "b" ]
|> with "reachable" [ var "b", var "c" ]
-- next, we need to know what is a valid node so we can
, rule "node" [ "a" ]
|> with "link" [ var "a", var "b" ]
, rule "node" [ "b" ]
|> with "link" [ var "a", var "b" ]
-- finally, we just say "a set of two nodes is unreachable if they're
-- individually in `node` but not together in `reachable`"
, rule "unreachable" [ "a", "b" ]
|> with "node" [ var "a" ]
|> with "node" [ var "b" ]
|> without "reachable" [ var "a", var "b" ]
]
-}
without : String -> List Term -> Rule -> Rule
without name terms (Rule head body) =
Rule head (BodyAtom Negative (Atom name terms) :: body)


Expand Down
68 changes: 34 additions & 34 deletions tests/Database/DatalogTests.elm
View file
Expand Up @@ -14,13 +14,13 @@ datalogTests =
[ test "a simple read turns into a Read -> Project" <|
\_ ->
rule "mortal" [ "who" ]
|> withMatching "greek" [ var "who" ]
|> with "greek" [ var "who" ]
|> planRule
|> Expect.equal (Ok (Database.Project [ 0 ] (Database.Read "greek")))
, test "a filtered read turns into a Select" <|
\_ ->
rule "mortal" [ "first name" ]
|> withMatching "greek" [ var "first name", string "of Athens" ]
|> with "greek" [ var "first name", string "of Athens" ]
|> planRule
|> Expect.equal
(Database.Read "greek"
Expand All @@ -31,8 +31,8 @@ datalogTests =
, test "sharing a variable between two atoms results in a join" <|
\_ ->
rule "reachable" [ "a", "c" ]
|> withMatching "link" [ var "a", var "b" ]
|> withMatching "reachable" [ var "b", var "c" ]
|> with "link" [ var "a", var "b" ]
|> with "reachable" [ var "b", var "c" ]
|> planRule
|> Expect.equal
(Database.JoinOn
Expand All @@ -46,7 +46,7 @@ datalogTests =
, test "filtering adds a predicate" <|
\_ ->
rule "adult" [ "name" ]
|> withMatching "person" [ var "name", var "age" ]
|> with "person" [ var "name", var "age" ]
|> filter (gt "age" (int 20))
|> planRule
|> Expect.equal
Expand All @@ -58,8 +58,8 @@ datalogTests =
, test "filtering using negation adds a predicate" <|
\_ ->
rule "sibling" [ "a", "b" ]
|> withMatching "parent" [ var "parent", var "a" ]
|> withMatching "parent" [ var "parent", var "b" ]
|> with "parent" [ var "parent", var "a" ]
|> with "parent" [ var "parent", var "b" ]
|> filter (not_ (eq "a" (var "b")))
|> planRule
|> Expect.equal
Expand All @@ -75,7 +75,7 @@ datalogTests =
, test "filtering using or adds a predicate" <|
\_ ->
rule "teen" [ "name" ]
|> withMatching "person" [ var "name", var "age" ]
|> with "person" [ var "name", var "age" ]
|> filter
(or
(gt "age" (int 12))
Expand All @@ -95,7 +95,7 @@ datalogTests =
, test "filtering using separate filters adds two filters" <|
\_ ->
rule "oldHockeyTeam" [ "name" ]
|> withMatching "team" [ var "name", var "league", var "age" ]
|> with "team" [ var "name", var "league", var "age" ]
|> filter (eq "league" (string "NHL"))
|> filter (gt "age" (int 50))
|> planRule
Expand All @@ -109,9 +109,9 @@ datalogTests =
, test "negation adds an outer join" <|
\_ ->
rule "unreachable" [ "a", "b" ]
|> withMatching "node" [ var "a" ]
|> withMatching "node" [ var "b" ]
|> withoutMatching "reachable" [ var "a", var "b" ]
|> with "node" [ var "a" ]
|> with "node" [ var "b" ]
|> without "reachable" [ var "a", var "b" ]
|> planRule
|> Expect.equal
(Database.OuterJoinOn
Expand All @@ -136,7 +136,7 @@ datalogTests =
, test "all terms in the head must appear in the body" <|
\_ ->
rule "bad" [ "a", "b" ]
|> withMatching "fine" [ var "a" ]
|> with "fine" [ var "a" ]
|> planRule
|> Expect.equal (Err (VariableDoesNotAppearInBody "b"))
, test "you can't have just filters" <|
Expand All @@ -148,15 +148,15 @@ datalogTests =
, test "you can't filter on an unbound name" <|
\_ ->
rule "bad" [ "a" ]
|> withMatching "fine" [ var "a" ]
|> with "fine" [ var "a" ]
|> filter (eq "b" (string "no"))
|> planRule
|> Expect.equal (Err (VariableDoesNotAppearInBody "b"))
, test "every name appearing in a negative atom must also appear in a positive atom" <|
\_ ->
rule "bad" [ "a" ]
|> withMatching "an atom to avoid the must-have-one-positive-atom rule" [ var "b" ]
|> withoutMatching "here's the problem" [ var "a" ]
|> with "an atom to avoid the must-have-one-positive-atom rule" [ var "b" ]
|> without "here's the problem" [ var "a" ]
|> planRule
|> Expect.equal (Err (VariableMustAppearInPositiveAtom "a"))
]
Expand All @@ -179,7 +179,7 @@ datalogTests =
|> Result.andThen
(query
[ rule "query" [ "who" ]
|> withMatching "greek" [ var "who" ]
|> with "greek" [ var "who" ]
]
)
|> Result.andThen (readError "query")
Expand All @@ -195,10 +195,10 @@ datalogTests =
|> Result.andThen
(query
[ rule "reachable" [ "a", "b" ]
|> withMatching "link" [ var "a", var "b" ]
|> with "link" [ var "a", var "b" ]
, rule "reachable" [ "a", "c" ]
|> withMatching "link" [ var "a", var "b" ]
|> withMatching "reachable" [ var "b", var "c" ]
|> with "link" [ var "a", var "b" ]
|> with "reachable" [ var "b", var "c" ]
]
)
|> Result.andThen (readError "reachable")
Expand Down Expand Up @@ -230,8 +230,8 @@ datalogTests =
|> Result.andThen
(query
[ rule "hometown" [ "name", "hometown" ]
|> withMatching "mascot" [ var "name", var "team" ]
|> withMatching "team" [ var "team", var "hometown" ]
|> with "mascot" [ var "name", var "team" ]
|> with "team" [ var "team", var "hometown" ]
]
)
|> Result.andThen (readError "hometown")
Expand All @@ -252,18 +252,18 @@ datalogTests =
|> Result.andThen
(query
[ rule "reachable" [ "a", "b" ]
|> withMatching "link" [ var "a", var "b" ]
|> with "link" [ var "a", var "b" ]
, rule "reachable" [ "a", "c" ]
|> withMatching "link" [ var "a", var "b" ]
|> withMatching "reachable" [ var "b", var "c" ]
|> with "link" [ var "a", var "b" ]
|> with "reachable" [ var "b", var "c" ]
, rule "node" [ "a" ]
|> withMatching "link" [ var "a", var "b" ]
|> with "link" [ var "a", var "b" ]
, rule "node" [ "b" ]
|> withMatching "link" [ var "a", var "b" ]
|> with "link" [ var "a", var "b" ]
, rule "unreachable" [ "a", "b" ]
|> withMatching "node" [ var "a" ]
|> withMatching "node" [ var "b" ]
|> withoutMatching "reachable" [ var "a", var "b" ]
|> with "node" [ var "a" ]
|> with "node" [ var "b" ]
|> without "reachable" [ var "a", var "b" ]
]
)
|> Result.andThen (readError "unreachable")
Expand Down Expand Up @@ -292,11 +292,11 @@ datalogTests =
|> Result.andThen
(query
[ rule "p" [ "x" ]
|> withMatching "x" [ var "x" ]
|> withoutMatching "q" [ var "x" ]
|> with "x" [ var "x" ]
|> without "q" [ var "x" ]
, rule "q" [ "x" ]
|> withMatching "x" [ var "x" ]
|> withoutMatching "p" [ var "x" ]
|> with "x" [ var "x" ]
|> without "p" [ var "x" ]
]
)
|> Expect.equal (Err CannotHaveNegationInRecursiveQuery)
Expand Down

0 comments on commit e211d16

Please sign in to comment.