Adding datalog macro
This commit is contained in:
Jay McCarthy
parent
1f3c3df835
commit
da7d4d4042
|
|
@ -17,17 +17,16 @@
|
|||
datalog/private/compiler)
|
||||
|
||||
(define (this-read-syntax [src #f] [in (current-input-port)])
|
||||
(list
|
||||
(compile-program
|
||||
(parameterize ([current-source-name src])
|
||||
(parse-program in)))))
|
||||
(compile-program
|
||||
(parameterize ([current-source-name src])
|
||||
(parse-program in))))
|
||||
|
||||
; XXX This is almost certainly wrong.
|
||||
(define (even-read src ip)
|
||||
(begin0
|
||||
(compile-statement
|
||||
(parameterize ([current-source-name src])
|
||||
(parse-statement ip)))
|
||||
(parse-statement ip)))
|
||||
(current-read-interaction odd-read)))
|
||||
(define (odd-read src ip)
|
||||
(current-read-interaction even-read)
|
||||
|
|
|
|||
|
|
@ -1,11 +1,6 @@
|
|||
#lang racket
|
||||
(require "ast.rkt"
|
||||
"parse.rkt"
|
||||
"pretty.rkt"
|
||||
"runtime.rkt"
|
||||
"eval.rkt")
|
||||
(provide (all-from-out "ast.rkt"
|
||||
"parse.rkt"
|
||||
"pretty.rkt"
|
||||
"runtime.rkt"
|
||||
"eval.rkt"))
|
||||
(require "runtime.rkt"
|
||||
"stx.rkt")
|
||||
(provide make-theory
|
||||
mutable-theory/c
|
||||
(all-from-out "stx.rkt"))
|
||||
|
|
@ -2,17 +2,15 @@
|
|||
(require racket/contract
|
||||
racket/match
|
||||
datalog/ast
|
||||
(only-in datalog/sexp/lang
|
||||
? :- ! ~))
|
||||
(require (for-template datalog/sexp/lang))
|
||||
datalog/stx)
|
||||
(require (for-template datalog/stx))
|
||||
|
||||
(provide/contract
|
||||
[compile-program (program/c . -> . syntax?)]
|
||||
[compile-program (program/c . -> . (listof syntax?))]
|
||||
[compile-statement (statement/c . -> . syntax?)])
|
||||
|
||||
(define (compile-program p)
|
||||
(quasisyntax
|
||||
(#%module-begin #,@(map compile-statement p))))
|
||||
(map compile-statement p))
|
||||
|
||||
(define compile-statement
|
||||
(match-lambda
|
||||
|
|
|
|||
|
|
@ -126,6 +126,7 @@
|
|||
[theory/c contract?]
|
||||
[immutable-theory/c contract?]
|
||||
[mutable-theory/c contract?]
|
||||
[rename make-mutable-theory make-theory (-> mutable-theory/c)]
|
||||
[make-mutable-theory (-> mutable-theory/c)]
|
||||
[make-immutable-theory (-> immutable-theory/c)]
|
||||
[assume (immutable-theory/c safe-clause? . -> . immutable-theory/c)]
|
||||
|
|
|
|||
|
|
@ -24,7 +24,7 @@ on tabling intermediate results ensures that all queries terminate.
|
|||
|
||||
@section[#:tag "datalog"]{Datalog Module Language}
|
||||
|
||||
@defmodulelang[datalog]
|
||||
@defmodulelang[@racketmodname[datalog] #:module-paths (datalog/lang/reader)]
|
||||
|
||||
In Datalog input, whitespace characters are ignored except when they separate adjacent tokens or when they occur in strings.
|
||||
Comments are also considered to be whitespace. The character @litchar["%"] introduces a comment, which extends to the next line break.
|
||||
|
|
@ -130,11 +130,11 @@ The Datalog REPL accepts new statements that are executed as if they were in the
|
|||
@include-section["tutorial.scrbl"]
|
||||
|
||||
@section{Parenthetical Datalog Module Language}
|
||||
@(require (for-label datalog/sexp/lang))
|
||||
@(require (for-label datalog))
|
||||
|
||||
@defmodulelang[datalog/sexp]
|
||||
|
||||
The semantics of this language is the same as the normal Datalog language, except it uses a @secref["parenstx"].
|
||||
The semantics of this language is the same as the normal Datalog language, except it uses a parenthetical syntax.
|
||||
|
||||
Literals are represented as S-expressions with non-capitalized identifiers for constant symbols, strings for constant strings, and capitalized identifiers for variable symbols. Top-level identifiers and strings are not otherwise allowed in the program.
|
||||
|
||||
|
|
@ -154,18 +154,6 @@ The following is a program:
|
|||
|
||||
The Parenthetical Datalog REPL accepts new statements that are executed as if they were in the original program text.
|
||||
|
||||
@subsection[#:tag "parenstx"]{Parenthetical Syntax}
|
||||
|
||||
@defmodule[datalog/sexp/lang]
|
||||
|
||||
@defform[(! clause)]{ Asserts the clause. }
|
||||
@defform[(~ clause)]{ Retracts the literal. }
|
||||
@defform[(? literal)]{ Queries the literal and prints the result literals. }
|
||||
|
||||
@defform[(:- literal literal ...)]{ A conditional clause. }
|
||||
|
||||
@defform[(= term term)]{ An equality literal. }
|
||||
|
||||
@include-section["racket.scrbl"]
|
||||
|
||||
@section{Acknowledgments}
|
||||
|
|
|
|||
|
|
@ -10,610 +10,59 @@
|
|||
|
||||
@title{Racket Interoperability}
|
||||
|
||||
@defmodule[datalog/main]
|
||||
@defmodule[datalog]
|
||||
|
||||
The Datalog database can be directly used by Racket programs through this API.
|
||||
|
||||
@examples[#:eval the-eval
|
||||
(define example-program
|
||||
#<<END
|
||||
ancestor(A, B) :-
|
||||
parent(A, B).
|
||||
ancestor(A, B) :-
|
||||
parent(A, C),
|
||||
D = C,
|
||||
ancestor(D, B).
|
||||
parent(john, douglas).
|
||||
parent(bob, john).
|
||||
parent(ebbon, bob).
|
||||
ancestor(A, B)?
|
||||
END
|
||||
)
|
||||
(format-program
|
||||
(parse-program
|
||||
(open-input-string
|
||||
example-program)))
|
||||
(void
|
||||
(eval-program/fresh
|
||||
(parse-program
|
||||
(open-input-string
|
||||
example-program))))]
|
||||
|
||||
|
||||
@section{Abstract Syntax}
|
||||
|
||||
This library provides the structures that represent Datalog syntax. It can be required via:
|
||||
|
||||
@defmodule[datalog/ast]
|
||||
|
||||
@defthing[srcloc/c contract?]{
|
||||
Contract for the third argument to @racket[datum->syntax].
|
||||
(define family (make-theory))
|
||||
|
||||
(datalog family
|
||||
(! (parent joseph2 joseph1))
|
||||
(! (parent joseph2 lucy))
|
||||
(! (parent joseph3 joseph2)))
|
||||
|
||||
(datalog family
|
||||
(? (parent X joseph2)))
|
||||
|
||||
Equivalent to
|
||||
@racketblock[
|
||||
(or/c syntax?
|
||||
false/c
|
||||
(list/c any/c
|
||||
(or/c exact-positive-integer? #f)
|
||||
(or/c exact-nonnegative-integer? #f)
|
||||
(or/c exact-nonnegative-integer? #f)
|
||||
(or/c exact-positive-integer? #f)))
|
||||
]
|
||||
}
|
||||
|
||||
@defthing[datum/c contract?]{
|
||||
Contract for @deftech{datum}s.
|
||||
Equivalent to @racket[(or/c string? symbol?)].
|
||||
}
|
||||
|
||||
@defproc[(datum-equal? [d1 datum/c] [d2 datum/c])
|
||||
boolean?]{
|
||||
Equivalent to @racket[(equal? d1 d2)].
|
||||
|
||||
@examples[#:eval the-eval
|
||||
(datum-equal? 'sym1 'sym2)
|
||||
(datum-equal? 'sym1 'sym1)
|
||||
(datum-equal? "str1" "str2")
|
||||
(datum-equal? "str1" "str1")]
|
||||
}
|
||||
|
||||
@defstruct[variable ([srcloc srcloc/c]
|
||||
[sym symbol?])]{
|
||||
A logic variable in Datalog.
|
||||
(This structure does not enforce the requirements for what characters variables can contain, so if you print one out,
|
||||
it might not be parseable, but it will be executeable.)
|
||||
}
|
||||
|
||||
@defproc[(variable-equal? [v1 variable?] [v2 variable?])
|
||||
boolean?]{
|
||||
Equivalent to @racket[(equal? v1 v2)] modulo source location.
|
||||
|
||||
@examples[#:eval the-eval
|
||||
(variable-equal? (make-variable #f 'sym)
|
||||
(make-variable #'sym 'sym))
|
||||
(variable-equal? (make-variable #f 'sym1)
|
||||
(make-variable #f 'sym2))]
|
||||
}
|
||||
|
||||
@defstruct[constant ([srcloc srcloc/c]
|
||||
[datum datum/c])]{
|
||||
A constant in Datalog.
|
||||
(This structure does not enforce the requirements for what characters constants can contain, so if you print one out,
|
||||
it might not be parseable, but it will be executeable.)
|
||||
}
|
||||
|
||||
@defproc[(constant-equal? [c1 constant?] [c2 constant?])
|
||||
boolean?]{
|
||||
Equivalent to @racket[(equal? c1 c2)] modulo source location.
|
||||
|
||||
@examples[#:eval the-eval
|
||||
(constant-equal? (make-constant #f 'sym)
|
||||
(make-constant #'sym 'sym))
|
||||
(constant-equal? (make-constant #f 'sym)
|
||||
(make-constant #f "str"))]
|
||||
}
|
||||
|
||||
@defthing[term/c contract?]{
|
||||
Contract for @deftech{term}s. Equivalent to @racket[(or/c variable? constant?)].
|
||||
}
|
||||
|
||||
@defproc[(term-equal? [t1 term/c] [t2 term/c])
|
||||
boolean?]{
|
||||
Equivalent to @racket[(equal? t1 t2)] modulo source location.
|
||||
|
||||
@examples[#:eval the-eval
|
||||
(term-equal? (make-constant #f 'sym) (make-constant #'sym 'sym))
|
||||
(term-equal? (make-constant #f 'sym) (make-constant #f "str"))]
|
||||
}
|
||||
|
||||
@defstruct[literal ([srcloc srcloc/c]
|
||||
[predicate datum/c]
|
||||
[terms (listof term/c)])]{
|
||||
A literal in Datalog.
|
||||
}
|
||||
|
||||
@defproc[(literal-equal? [l1 literal?] [l2 literal?])
|
||||
boolean?]{
|
||||
Equivalent to @racket[(equal? l1 l2)] modulo source location.
|
||||
|
||||
@examples[#:eval the-eval
|
||||
(literal-equal? (make-literal #f 'ancestor (list))
|
||||
(make-literal #'ancestor 'ancestor (list)))
|
||||
(literal-equal? (make-literal #f 'ancestor (list))
|
||||
(make-literal #f 'parent (list)))
|
||||
(literal-equal? (make-literal #f 'ancestor (list))
|
||||
(make-literal #f 'ancestor
|
||||
(list (make-constant #f 'jack))))]
|
||||
}
|
||||
|
||||
@defstruct[clause ([srcloc srcloc/c]
|
||||
[head literal?]
|
||||
[body (listof literal?)])]{
|
||||
A Datalog clause.
|
||||
}
|
||||
|
||||
@defproc[(clause-equal? [c1 clause?] [c2 clause?])
|
||||
boolean?]{
|
||||
Equivalent to @racket[(equal? c1 c2)] modulo source location.
|
||||
|
||||
@examples[#:eval the-eval
|
||||
(clause-equal?
|
||||
(make-clause #f (make-literal #f 'ancestor (list)) (list))
|
||||
(make-clause #'clause
|
||||
(make-literal #f 'ancestor (list)) (list)))
|
||||
(clause-equal?
|
||||
(make-clause #f (make-literal #f 'ancestor (list)) (list))
|
||||
(make-clause #f (make-literal #f 'parent (list)) (list)))]
|
||||
}
|
||||
|
||||
@defstruct[assertion ([srcloc srcloc/c]
|
||||
[clause clause?])]{
|
||||
A Datalog assertion.
|
||||
}
|
||||
|
||||
@defstruct[retraction ([srcloc srcloc/c]
|
||||
[clause clause?])]{
|
||||
A Datalog retraction.
|
||||
}
|
||||
|
||||
@defstruct[query ([srcloc srcloc/c]
|
||||
[literal literal?])]{
|
||||
A Datalog query.
|
||||
}
|
||||
|
||||
@defthing[statement/c contract?]{
|
||||
Contract for @deftech{statement}s.
|
||||
Equivalent to @racket[(or/c assertion? retraction? query?)].
|
||||
}
|
||||
|
||||
@defthing[program/c contract?]{
|
||||
Contract for @deftech{program}s.
|
||||
Equivalent to @racket[(listof statement/c)].
|
||||
}
|
||||
|
||||
@section{Datalog Parsing}
|
||||
|
||||
This library provides facilities for parsing Datalog source. It can be required via:
|
||||
|
||||
@defmodule[datalog/parse]
|
||||
|
||||
@defparam[current-source-name name any/c]{ A parameter used by the parsing functions to set the source name on the read ASTs. }
|
||||
|
||||
@defproc[(parse-literal [ip input-port?])
|
||||
literal?]{
|
||||
Parses a @racket[literal] from @racket[ip].
|
||||
|
||||
@examples[#:eval the-eval
|
||||
(parse-literal (open-input-string "parent(john,douglas)"))
|
||||
(parse-literal (open-input-string "zero-arity-literal"))
|
||||
(parse-literal (open-input-string "\"=\"(3,3)"))
|
||||
(parse-literal
|
||||
(open-input-string "\"\"(-0-0-0,&&&,***,\"\00\")"))
|
||||
(parse-literal (open-input-string "3 = 3"))]
|
||||
}
|
||||
|
||||
@defproc[(parse-clause [ip input-port?])
|
||||
clause?]{
|
||||
Parses a @racket[clause] from @racket[ip].
|
||||
|
||||
@examples[#:eval the-eval
|
||||
(parse-clause
|
||||
(open-input-string "parent(john, douglas)"))
|
||||
(parse-clause
|
||||
(open-input-string "ancestor(A, B) :- parent(A, B)"))
|
||||
(parse-clause
|
||||
(open-input-string
|
||||
(string-append "ancestor(A, B) :- parent(A, C),"
|
||||
"ancestor(C, B)")))]
|
||||
}
|
||||
|
||||
@defproc[(parse-statement [ip input-port?])
|
||||
statement/c]{
|
||||
Parses a @tech{statement} from @racket[ip].
|
||||
|
||||
@examples[#:eval the-eval
|
||||
(parse-statement
|
||||
(open-input-string "parent(john, douglas)."))
|
||||
(parse-statement
|
||||
(open-input-string "parent(john, douglas)~"))
|
||||
(parse-statement
|
||||
(open-input-string "parent(john, douglas)?"))]
|
||||
}
|
||||
|
||||
@defproc[(parse-program [ip input-port?])
|
||||
program/c]{
|
||||
Parses a @tech{program} from @racket[ip].
|
||||
|
||||
@examples[#:eval the-eval
|
||||
(parse-program
|
||||
(open-input-string
|
||||
(string-append
|
||||
"edge(a, b). edge(b, c)."
|
||||
"edge(c, d). edge(d, a)."
|
||||
"path(X, Y) :- edge(X, Y)."
|
||||
"path(X, Y) :- edge(X, Z), path(Z, Y)."
|
||||
"path(X, Y)?")))]
|
||||
}
|
||||
|
||||
@section{Pretty-Printing}
|
||||
|
||||
This library provides facilities for pretty-printing Datalog source. It can be required via:
|
||||
|
||||
@defmodule[datalog/pretty]
|
||||
|
||||
@defproc[(format-datum [d datum/c])
|
||||
string?]{
|
||||
Formats a @tech{datum}.
|
||||
|
||||
@examples[#:eval the-eval
|
||||
(format-datum 'sym)
|
||||
(format-datum "str")]
|
||||
}
|
||||
|
||||
@defproc[(format-variable [v variable?])
|
||||
string?]{
|
||||
Formats a @racket[variable].
|
||||
|
||||
@examples[#:eval the-eval
|
||||
(format-variable (make-variable #f 'Ancestor))]
|
||||
}
|
||||
|
||||
@defproc[(format-constant [c constant?])
|
||||
string?]{
|
||||
Formats a @racket[constant].
|
||||
|
||||
@examples[#:eval the-eval
|
||||
(format-constant (make-constant #f 'joseph))
|
||||
(format-constant (make-constant #f "whom"))]
|
||||
}
|
||||
(datalog family
|
||||
(? (parent joseph2 X)))
|
||||
|
||||
@defproc[(format-term [t term/c])
|
||||
string?]{
|
||||
Formats a @tech{term}.
|
||||
|
||||
@examples[#:eval the-eval
|
||||
(format-term (make-variable #f 'Ancestor))
|
||||
(format-term (make-constant #f 'joseph))
|
||||
(format-term (make-constant #f "whom"))]
|
||||
}
|
||||
|
||||
@defproc[(format-literal [l literal?])
|
||||
string?]{
|
||||
Formats a @racket[literal].
|
||||
|
||||
@examples[#:eval the-eval
|
||||
(format-literal (make-literal #f 'true (list)))
|
||||
(format-literal
|
||||
(make-literal #f 'ancestor
|
||||
(list (make-variable #f 'A) (make-constant #f 'jay))))
|
||||
(format-literal
|
||||
(make-literal #f '=
|
||||
(list (make-constant #f 'joseph) (make-constant #f 'jay))))]
|
||||
}
|
||||
|
||||
@defproc[(format-literals [ls (listof literal?)])
|
||||
string?]{
|
||||
Formats a list of @racket[literal]s as @racket[assertion]s for formatting @racket[prove] results.
|
||||
|
||||
@examples[#:eval the-eval
|
||||
(format-literals
|
||||
(list
|
||||
(make-literal #f 'true (list))
|
||||
(make-literal #f 'ancestor
|
||||
(list (make-constant #f 'joseph) (make-constant #f 'jay)))
|
||||
(make-literal #f '=
|
||||
(list (make-constant #f 'joseph) (make-constant #f 'jay)))))]
|
||||
}
|
||||
|
||||
@defproc[(format-clause [c clause?])
|
||||
string?]{
|
||||
Formats a @racket[clause].
|
||||
|
||||
@examples[#:eval the-eval
|
||||
(format-clause
|
||||
(make-clause
|
||||
#f (make-literal #f 'ancestor
|
||||
(list (make-constant #f 'joseph)
|
||||
(make-constant #f 'jay)))
|
||||
(list)))
|
||||
(format-clause
|
||||
(make-clause
|
||||
#f (make-literal
|
||||
#f 'ancestor
|
||||
(list (make-constant #f 'A) (make-constant #f 'B)))
|
||||
(list (make-literal
|
||||
#f 'parent
|
||||
(list (make-constant #f 'A) (make-constant #f 'B))))))
|
||||
(format-clause
|
||||
(make-clause
|
||||
#f (make-literal
|
||||
#f 'ancestor
|
||||
(list (make-constant #f 'A) (make-constant #f 'B)))
|
||||
(list (make-literal
|
||||
#f 'parent
|
||||
(list (make-constant #f 'A) (make-constant #f 'C)))
|
||||
(make-literal
|
||||
#f 'ancestor
|
||||
(list (make-constant #f 'C) (make-constant #f 'B))))))]
|
||||
}
|
||||
|
||||
@defproc[(format-assertion [a assertion?])
|
||||
string?]{
|
||||
Formats a @racket[assertion].
|
||||
|
||||
@examples[#:eval the-eval
|
||||
(format-assertion
|
||||
(make-assertion
|
||||
#f (make-clause
|
||||
#f (make-literal #f 'ancestor
|
||||
(list (make-constant #f 'joseph)
|
||||
(make-constant #f 'jay)))
|
||||
(list))))]
|
||||
}
|
||||
|
||||
@defproc[(format-retraction [r retraction?])
|
||||
string?]{
|
||||
Formats a @racket[retraction].
|
||||
|
||||
@examples[#:eval the-eval
|
||||
(format-retraction
|
||||
(make-retraction
|
||||
#f (make-clause
|
||||
#f (make-literal #f 'ancestor
|
||||
(list (make-constant #f 'joseph)
|
||||
(make-constant #f 'jay)))
|
||||
(list))))]
|
||||
}
|
||||
|
||||
@defproc[(format-query [q query?])
|
||||
string?]{
|
||||
Formats a @racket[query].
|
||||
|
||||
@examples[#:eval the-eval
|
||||
(format-query
|
||||
(make-query
|
||||
#f (make-literal #f 'ancestor
|
||||
(list (make-constant #f 'joseph)
|
||||
(make-constant #f 'jay)))))]
|
||||
}
|
||||
|
||||
@defproc[(format-statement [s statement/c])
|
||||
string?]{
|
||||
Formats a @tech{statement}.
|
||||
|
||||
@examples[#:eval the-eval
|
||||
(format-statement
|
||||
(make-query
|
||||
#f (make-literal #f 'ancestor
|
||||
(list (make-constant #f 'joseph)
|
||||
(make-constant #f 'jay)))))]
|
||||
}
|
||||
|
||||
@defproc[(format-program [p program/c])
|
||||
string?]{
|
||||
Formats a @tech{program}.
|
||||
|
||||
@examples[#:eval the-eval
|
||||
(format-program
|
||||
(list
|
||||
(make-assertion
|
||||
#f (make-clause
|
||||
#f (make-literal #f 'ancestor
|
||||
(list (make-constant #f 'joseph)
|
||||
(make-constant #f 'jay)))
|
||||
(list)))
|
||||
(make-query
|
||||
#f (make-literal #f 'ancestor
|
||||
(list (make-constant #f 'joseph)
|
||||
(make-constant #f 'jay))))))]
|
||||
}
|
||||
|
||||
@section{Runtime System}
|
||||
|
||||
This library implements the Datalog runtime system. It can be required via:
|
||||
|
||||
@defmodule[datalog/runtime]
|
||||
|
||||
@defthing[theory/c contract?]{
|
||||
A contract for @deftech{theories}.
|
||||
}
|
||||
|
||||
@defthing[immutable-theory/c contract?]{
|
||||
A contract for immutable @tech{theories}.
|
||||
}
|
||||
|
||||
@defthing[mutable-theory/c contract?]{
|
||||
A contract for mutable @tech{theories}.
|
||||
}
|
||||
|
||||
@defproc[(make-mutable-theory)
|
||||
mutable-theory/c]{
|
||||
Constructs a mutable @tech{theory}.
|
||||
}
|
||||
|
||||
@defproc[(make-immutable-theory)
|
||||
immutable-theory/c]{
|
||||
Constructs a immutable @tech{theory}.
|
||||
}
|
||||
|
||||
@defproc[(safe-clause? [c clause?])
|
||||
boolean?]{
|
||||
Determines if a @racket[clause] is safe.
|
||||
A @racket[clause] is safe if every @racket[variable] in its head occurs in some @racket[literal] in its body.
|
||||
(datalog family
|
||||
(? (parent joseph2 X))
|
||||
(? (parent X joseph2)))
|
||||
|
||||
@examples[#:eval the-eval
|
||||
(safe-clause?
|
||||
(parse-clause (open-input-string "ancestor(joseph,jay)")))
|
||||
(safe-clause?
|
||||
(parse-clause
|
||||
(open-input-string "ancestor(A,B) :- parent(A,B)")))
|
||||
(safe-clause?
|
||||
(parse-clause
|
||||
(open-input-string "ancestor(A,B) :- parent(A,jay)")))]
|
||||
}
|
||||
|
||||
@defproc[(assume [thy immutable-theory/c]
|
||||
[c safe-clause?])
|
||||
immutable-theory/c]{
|
||||
Adds @racket[c] to @racket[thy] in a persistent way.
|
||||
}
|
||||
|
||||
@defproc[(retract [thy immutable-theory/c]
|
||||
[c clause?])
|
||||
immutable-theory/c]{
|
||||
Removes @racket[c] from @racket[thy] in a persistent way.
|
||||
}
|
||||
|
||||
@defproc[(assume! [thy mutable-theory/c]
|
||||
[c safe-clause?])
|
||||
mutable-theory/c]{
|
||||
Adds @racket[c] to @racket[thy].
|
||||
}
|
||||
|
||||
@defproc[(retract! [thy mutable-theory/c]
|
||||
[c clause?])
|
||||
mutable-theory/c]{
|
||||
Removes @racket[c] from @racket[thy].
|
||||
}
|
||||
|
||||
@defproc[(prove [thy theory/c]
|
||||
[l literal?])
|
||||
(listof literal?)]{
|
||||
Attempts to prove @racket[l] using the @tech{theory} @racket[thy], returning all
|
||||
the results of the query.
|
||||
(datalog family
|
||||
(! (:- (ancestor A B)
|
||||
(parent A B)))
|
||||
(! (:- (ancestor A B)
|
||||
(parent A C)
|
||||
(= D C)
|
||||
(ancestor D B))))
|
||||
|
||||
@examples[#:eval the-eval
|
||||
(format-literals
|
||||
(prove
|
||||
(assume
|
||||
(make-immutable-theory)
|
||||
(parse-clause (open-input-string "parent(joseph1,joseph2)")))
|
||||
(parse-literal
|
||||
(open-input-string "parent(joseph1,joseph2)"))))
|
||||
(format-literals
|
||||
(prove
|
||||
(retract
|
||||
(assume
|
||||
(make-immutable-theory)
|
||||
(parse-clause
|
||||
(open-input-string "parent(joseph1,joseph2)")))
|
||||
(parse-clause (open-input-string "parent(joseph1,joseph2)")))
|
||||
(parse-literal
|
||||
(open-input-string "parent(joseph1,joseph2)"))))
|
||||
(format-literals
|
||||
(prove
|
||||
(assume
|
||||
(make-immutable-theory)
|
||||
(parse-clause (open-input-string "parent(joseph1,joseph2)")))
|
||||
(parse-literal (open-input-string "parent(A,B)"))))]
|
||||
}
|
||||
|
||||
@section{Evaluation}
|
||||
|
||||
This library provides facilities for evaluating Datalog. It can be required via:
|
||||
|
||||
@defmodule[datalog/eval]
|
||||
|
||||
@defthing[current-theory (parameter/c mutable-theory/c)]{
|
||||
The @tech{theory} used by @racket[eval-program] and @racket[eval-stmt].
|
||||
}
|
||||
|
||||
@defproc[(print-literals [ls (listof literal?)]) void]{
|
||||
Pretty formats the literals for display. }
|
||||
|
||||
@defproc[(eval-program [p program/c])
|
||||
void]{
|
||||
Evaluates @racket[p] using @racket[(current-theory)] as the @tech{theory}, printing query answers as it goes.
|
||||
|
||||
This will raise a syntax error if given an @racket[assertion] of a @racket[clause] that is not a @racket[safe-clause?].
|
||||
(datalog family
|
||||
(? (ancestor A B)))
|
||||
|
||||
@examples[#:eval the-eval
|
||||
(parameterize ([current-theory (make-mutable-theory)])
|
||||
(eval-program
|
||||
(parse-program
|
||||
(open-input-string
|
||||
(string-append
|
||||
"edge(a, b). edge(b, c). edge(c, d). edge(d, a)."
|
||||
"path(X, Y) :- edge(X, Y)."
|
||||
"path(X, Y) :- edge(X, Z), path(Z, Y)."
|
||||
"path(X, Y)?")))))
|
||||
(eval-program
|
||||
(parse-program
|
||||
(open-input-string
|
||||
"path(X, Y) :- edge(X, a).")))]
|
||||
}
|
||||
(let ([x 'joseph2])
|
||||
(datalog family
|
||||
(? (parent x X))))]
|
||||
|
||||
@defproc[(eval-top-level-statement [s statement/c])
|
||||
void]{
|
||||
Evaluates @racket[s] using @racket[(current-theory)] as the @tech{theory}, printing query answers if @racket[s] is a query.
|
||||
|
||||
This will raise a syntax error if given an @racket[assertion] of a @racket[clause] that is not a @racket[safe-clause?].
|
||||
}
|
||||
|
||||
@defproc[(eval-statement [s statement/c])
|
||||
(or/c void (listof literal?))]{
|
||||
Evaluates @racket[s] using @racket[(current-theory)] as the @tech{theory}.
|
||||
|
||||
This will raise a syntax error if given an @racket[assertion] of a @racket[clause] that is not a @racket[safe-clause?].
|
||||
@defthing[mutable-theory/c contract?]{ A contract for Datalog theories. }
|
||||
|
||||
@examples[#:eval the-eval
|
||||
(parameterize ([current-theory (make-mutable-theory)])
|
||||
(eval-statement
|
||||
(parse-statement
|
||||
(open-input-string
|
||||
"edge(a, b).")))
|
||||
(eval-statement
|
||||
(parse-statement
|
||||
(open-input-string
|
||||
"path(X, Y) :- edge(X, Y).")))
|
||||
(eval-statement
|
||||
(parse-statement
|
||||
(open-input-string
|
||||
"path(X, Y)?"))))
|
||||
(eval-statement
|
||||
(parse-statement
|
||||
(open-input-string
|
||||
"path(X, Y) :- edge(X, a).")))]
|
||||
}
|
||||
|
||||
@defproc[(eval-program/fresh [p program/c])
|
||||
immutable-theory/c]{
|
||||
Evaluates @racket[p] in a fresh @tech{theory} and returns the final @tech{theory}, printing query answers as it goes.
|
||||
@defproc[(make-theory) mutable-theory/c]{ Creates a theory for use with @racket[datalog]. }
|
||||
|
||||
This will raise a syntax error if given an @racket[assertion] of a @racket[clause] that is not a @racket[safe-clause?].
|
||||
@defform[(datalog thy-expr
|
||||
stmt ...)
|
||||
#:contracts ([thy-expr mutable-theory/c])]{ Executes the statements on the theory given by @racket[thy-expr]. Returns the answers to the final query as a list of S-expressions or returns @racket[empty]. }
|
||||
|
||||
@defform[(datalog! thy-expr
|
||||
stmt ...)
|
||||
#:contracts ([thy-expr mutable-theory/c])]{ Executes the statements on the theory given by @racket[thy-expr]. Prints the answers to every query in the list of statements. Returns @racket[(void)]. }
|
||||
|
||||
Literals are represented as S-expressions with non-capitalized identifiers for constant symbols, strings for constant strings, and capitalized identifiers for variable symbols. Bound identifiers are treated as constants; they must evaluate to either a symbol or string.
|
||||
|
||||
@examples[#:eval the-eval
|
||||
(void
|
||||
(eval-program/fresh
|
||||
(parse-program
|
||||
(open-input-string
|
||||
(string-append
|
||||
"edge(a, b). edge(b, c). edge(c, d). edge(d, a)."
|
||||
"path(X, Y) :- edge(X, Y)."
|
||||
"path(X, Y) :- edge(X, Z), path(Z, Y)."
|
||||
"path(X, Y)?")))))
|
||||
(eval-program/fresh
|
||||
(parse-program
|
||||
(open-input-string
|
||||
"path(X, Y) :- edge(X, a).")))]
|
||||
}
|
||||
@defform[(! clause)]{ Asserts the clause. }
|
||||
@defform[(~ clause)]{ Retracts the literal. }
|
||||
@defform[(? literal)]{ Queries the literal and prints the result literals. }
|
||||
|
||||
@defform[(:- literal literal ...)]{ A conditional clause. }
|
||||
|
|
@ -24,7 +24,7 @@ this:
|
|||
|
||||
@racketinput[#,(tt "parent(john, douglas).")]
|
||||
|
||||
Each item in the parenthesized list following the name of the table is called a @tech{term}.
|
||||
Each item in the parenthesized list following the name of the table is called a @deftech{term}.
|
||||
A term can be either a logical @racket[variable] or a @racket[constant].
|
||||
Thus far, all the terms shown have been constant terms.
|
||||
|
||||
|
|
|
|||
|
|
@ -1,80 +1,21 @@
|
|||
#lang racket
|
||||
(require (for-syntax syntax/parse)
|
||||
racket/stxparam
|
||||
"../eval.rkt"
|
||||
"../ast.rkt")
|
||||
datalog/stx
|
||||
datalog/runtime)
|
||||
|
||||
(define-syntax (:- stx)
|
||||
(raise-syntax-error ':- "only allowed inside ! and ~" stx))
|
||||
(define lang-theory (make-theory))
|
||||
|
||||
(define-syntax-parameter top
|
||||
(λ (stx) (raise-syntax-error '#%top "undefined identifier" stx)))
|
||||
(define-syntax-parameter datum
|
||||
(λ (stx) (raise-syntax-error '#%datum "only allowed inside literals" stx)))
|
||||
(define-syntax module-begin
|
||||
(syntax-rules ()
|
||||
[(_ stmt ...)
|
||||
(#%module-begin
|
||||
(datalog! lang-theory stmt ...))]))
|
||||
|
||||
(define-syntax (literal-top stx)
|
||||
(syntax-parse
|
||||
stx
|
||||
[(_ . sym:id)
|
||||
(if (char-upper-case? (string-ref (symbol->string (syntax->datum #'sym)) 0))
|
||||
(quasisyntax/loc stx
|
||||
(variable #'#,stx 'sym))
|
||||
(quasisyntax/loc stx
|
||||
(constant #'#,stx 'sym)))]))
|
||||
(define-syntax top-interaction
|
||||
(syntax-rules ()
|
||||
[(_ . stmt)
|
||||
(datalog! lang-theory stmt)]))
|
||||
|
||||
(define-syntax (literal-datum stx)
|
||||
(syntax-parse
|
||||
stx
|
||||
[(_ . sym:str)
|
||||
(quasisyntax/loc stx
|
||||
(constant #'#,stx 'sym))]))
|
||||
|
||||
(define-syntax (->literal stx)
|
||||
(syntax-parse
|
||||
stx
|
||||
[(_ sym:id)
|
||||
(quasisyntax/loc stx
|
||||
(literal #'#,stx 'sym empty))]
|
||||
[(_ (sym:id e ...))
|
||||
(quasisyntax/loc stx
|
||||
(literal #'#,stx 'sym
|
||||
(syntax-parameterize ([top (make-rename-transformer #'literal-top)]
|
||||
[datum (make-rename-transformer #'literal-datum)])
|
||||
(list e ...))))]))
|
||||
|
||||
(define-syntax (->simple-clause stx)
|
||||
(syntax-case stx (:-)
|
||||
[(_ (:- head body ...))
|
||||
(quasisyntax/loc stx
|
||||
(clause #'#,stx (->literal head)
|
||||
(list (->literal body) ...)))]
|
||||
[(_ e)
|
||||
(quasisyntax/loc stx
|
||||
(clause #'#,stx (->literal e) empty))]))
|
||||
|
||||
(define-syntax-rule (define-paren-stx op struct)
|
||||
(define-syntax (op stx)
|
||||
(syntax-case stx ()
|
||||
[(_ c)
|
||||
(quasisyntax/loc stx
|
||||
(eval-top-level-statement (struct #'#,stx (->simple-clause c))))])))
|
||||
|
||||
(define-paren-stx ! assertion)
|
||||
(define-paren-stx ~ retraction)
|
||||
|
||||
(define-syntax (? stx)
|
||||
(syntax-case stx ()
|
||||
[(_ c)
|
||||
(quasisyntax/loc stx
|
||||
(eval-top-level-statement (query #'#,stx (->literal c))))]))
|
||||
|
||||
(define-syntax (= stx)
|
||||
(quasisyntax/loc stx
|
||||
(constant #'#,stx '=)))
|
||||
|
||||
(provide (rename-out [top #%top]
|
||||
[datum #%datum])
|
||||
#%top-interaction
|
||||
#%module-begin
|
||||
! ~ ?
|
||||
:- =)
|
||||
(provide (rename-out [top-interaction #%top-interaction]
|
||||
[module-begin #%module-begin])
|
||||
! ~ ? :-)
|
||||
105
collects/datalog/stx.rkt
Normal file
105
collects/datalog/stx.rkt
Normal file
|
|
@ -0,0 +1,105 @@
|
|||
#lang racket
|
||||
(require (for-syntax syntax/parse)
|
||||
datalog/ast
|
||||
datalog/eval)
|
||||
|
||||
(define-syntax (:- stx)
|
||||
(raise-syntax-error ':- "only allowed inside ! and ~" stx))
|
||||
(define-syntax (! stx)
|
||||
(raise-syntax-error '! "only allowed inside datalog" stx))
|
||||
(define-syntax (~ stx)
|
||||
(raise-syntax-error '~ "only allowed inside datalog" stx))
|
||||
(define-syntax (? stx)
|
||||
(raise-syntax-error '? "only allowed inside datalog" stx))
|
||||
|
||||
(define ->answer
|
||||
(match-lambda
|
||||
[(? void?)
|
||||
empty]
|
||||
[(? list? ls)
|
||||
(map literal->sexp ls)]))
|
||||
|
||||
(define literal->sexp
|
||||
(match-lambda
|
||||
[(literal _ pred ts)
|
||||
(list* pred (map term->datum ts))]))
|
||||
|
||||
(define term->datum
|
||||
(match-lambda
|
||||
[(constant _ v)
|
||||
v]))
|
||||
|
||||
(define-syntax (datalog stx)
|
||||
(syntax-case stx ()
|
||||
[(_ thy-expr stmt ...)
|
||||
(syntax/loc stx
|
||||
(parameterize ([current-theory thy-expr])
|
||||
(->answer (eval-statement (datalog-stmt stmt)))
|
||||
...))]))
|
||||
|
||||
(define-syntax (datalog! stx)
|
||||
(syntax-case stx ()
|
||||
[(_ thy-expr stmt ...)
|
||||
(syntax/loc stx
|
||||
(parameterize ([current-theory thy-expr])
|
||||
(eval-top-level-statement (datalog-stmt stmt))
|
||||
...))]))
|
||||
|
||||
(define-syntax (datalog-stmt stx)
|
||||
(syntax-parse
|
||||
stx
|
||||
#:literals (! ~ ?)
|
||||
[(_ (! c))
|
||||
(quasisyntax/loc stx
|
||||
(assertion #'#,stx (datalog-clause c)))]
|
||||
[(_ (~ c))
|
||||
(quasisyntax/loc stx
|
||||
(retraction #'#,stx (datalog-clause c)))]
|
||||
[(_ (? l))
|
||||
(quasisyntax/loc stx
|
||||
(query #'#,stx (datalog-literal l)))]))
|
||||
|
||||
(define-syntax (datalog-clause stx)
|
||||
(syntax-parse
|
||||
stx
|
||||
#:literals (:-)
|
||||
[(_ (:- head body ...))
|
||||
(quasisyntax/loc stx
|
||||
(clause #'#,stx (datalog-literal head)
|
||||
(list (datalog-literal body) ...)))]
|
||||
[(_ e)
|
||||
(quasisyntax/loc stx
|
||||
(clause #'#,stx (datalog-literal e) empty))]))
|
||||
|
||||
(define-syntax (datalog-literal stx)
|
||||
(syntax-parse
|
||||
stx
|
||||
[(_ sym:id)
|
||||
(quasisyntax/loc stx
|
||||
(literal #'#,stx 'sym empty))]
|
||||
[(_ (sym:id e ...))
|
||||
(quasisyntax/loc stx
|
||||
(literal #'#,stx 'sym
|
||||
(list (datalog-term e)
|
||||
...)))]))
|
||||
|
||||
(define-syntax (datalog-term stx)
|
||||
(syntax-parse
|
||||
stx
|
||||
[(_ sym:str)
|
||||
(quasisyntax/loc stx
|
||||
(constant #'#,stx 'sym))]
|
||||
[(_ sym:id)
|
||||
(cond
|
||||
[(identifier-binding #'sym 0)
|
||||
(quasisyntax/loc stx
|
||||
(constant #'#,stx sym))]
|
||||
[(char-upper-case? (string-ref (symbol->string (syntax->datum #'sym)) 0))
|
||||
(quasisyntax/loc stx
|
||||
(variable #'#,stx 'sym))]
|
||||
[else
|
||||
(quasisyntax/loc stx
|
||||
(constant #'#,stx 'sym))])]))
|
||||
|
||||
(provide datalog datalog!
|
||||
:- ! ~ ?)
|
||||
|
|
@ -1,5 +1,6 @@
|
|||
#lang racket
|
||||
(require rackunit
|
||||
(require racket/runtime-path
|
||||
rackunit
|
||||
rackunit/text-ui
|
||||
"ast.rkt"
|
||||
|
||||
|
|
@ -17,6 +18,8 @@
|
|||
"runtime.rkt"
|
||||
"eval.rkt")
|
||||
|
||||
(define-runtime-path racket-mod "racket.rkt")
|
||||
|
||||
(run-tests
|
||||
(test-suite
|
||||
"Datalog"
|
||||
|
|
@ -34,4 +37,7 @@
|
|||
variant-tests
|
||||
|
||||
runtime-tests
|
||||
eval-tests))
|
||||
eval-tests
|
||||
|
||||
(test-case "Racket Interop"
|
||||
(dynamic-require racket-mod #f))))
|
||||
57
collects/tests/datalog/racket.rkt
Normal file
57
collects/tests/datalog/racket.rkt
Normal file
|
|
@ -0,0 +1,57 @@
|
|||
#lang racket
|
||||
(require datalog tests/eli-tester)
|
||||
|
||||
(define parent (make-theory))
|
||||
|
||||
(test
|
||||
(datalog parent
|
||||
(! (parent joseph2 joseph1))
|
||||
(! (parent joseph2 lucy))
|
||||
(! (parent joseph3 joseph2)))
|
||||
=>
|
||||
empty
|
||||
|
||||
(datalog parent
|
||||
(? (parent X joseph2)))
|
||||
=>
|
||||
(list '(parent joseph3 joseph2))
|
||||
|
||||
(datalog parent
|
||||
(? (parent joseph2 X)))
|
||||
=>
|
||||
(list '(parent joseph2 joseph1)
|
||||
'(parent joseph2 lucy))
|
||||
|
||||
(datalog parent
|
||||
(? (parent joseph2 X))
|
||||
(? (parent X joseph2)))
|
||||
=>
|
||||
(list '(parent joseph3 joseph2))
|
||||
|
||||
(datalog parent
|
||||
(! (:- (ancestor A B)
|
||||
(parent A B)))
|
||||
(! (:- (ancestor A B)
|
||||
(parent A C)
|
||||
(= D C) ; Unification required
|
||||
(ancestor D B))))
|
||||
=>
|
||||
empty
|
||||
|
||||
(datalog parent
|
||||
(? (ancestor A B)))
|
||||
=>
|
||||
(list '(ancestor joseph3 joseph2)
|
||||
'(ancestor joseph2 lucy)
|
||||
'(ancestor joseph2 joseph1)
|
||||
'(ancestor joseph3 lucy)
|
||||
'(ancestor joseph3 joseph1))
|
||||
|
||||
(let ([x 'joseph2])
|
||||
(datalog parent
|
||||
(? (parent x X))))
|
||||
=>
|
||||
(list '(parent joseph2 joseph1)
|
||||
'(parent joseph2 lucy))
|
||||
|
||||
)
|
||||
Loading…
Reference in New Issue
Block a user