Adding FFI to Datalog
This commit is contained in:
parent
f05eb775eb
commit
a6852d8f61
|
@ -15,9 +15,9 @@
|
|||
(define-struct variable (srcloc sym) #:prefab)
|
||||
(define (variable-equal? v1 v2)
|
||||
(eq? (variable-sym v1) (variable-sym v2)))
|
||||
(define-struct constant (srcloc datum) #:prefab)
|
||||
(define-struct constant (srcloc value) #:prefab)
|
||||
(define (constant-equal? v1 v2)
|
||||
(datum-equal? (constant-datum v1) (constant-datum v2)))
|
||||
(equal? (constant-value v1) (constant-value v2)))
|
||||
|
||||
(define term/c (or/c variable? constant?))
|
||||
(define (term-equal? t1 t2)
|
||||
|
@ -29,15 +29,31 @@
|
|||
[else
|
||||
#f]))
|
||||
|
||||
(define (terms-equal? t1 t2)
|
||||
(and (= (length t1)
|
||||
(length t2))
|
||||
(andmap term-equal? t1 t2)))
|
||||
|
||||
(define-struct literal (srcloc predicate terms) #:prefab)
|
||||
(define (literal-equal? l1 l2)
|
||||
(and (datum-equal? (literal-predicate l1)
|
||||
(literal-predicate l2))
|
||||
(= (length (literal-terms l1))
|
||||
(length (literal-terms l2)))
|
||||
(andmap term-equal?
|
||||
(literal-terms l1)
|
||||
(literal-terms l2))))
|
||||
(terms-equal? (literal-terms l1) (literal-terms l2))))
|
||||
|
||||
(define-struct external (srcloc predicate-sym predicate arg-terms ans-terms) #:prefab)
|
||||
(define (external-equal? e1 e2)
|
||||
(match-define (external _1 _s1 p1 ar1 an1) e1)
|
||||
(match-define (external _2 _s2 p2 ar2 an2) e2)
|
||||
(and (equal? p1 p2)
|
||||
(terms-equal? ar1 ar2)
|
||||
(terms-equal? an1 an2)))
|
||||
|
||||
(define question/c (or/c literal? external?))
|
||||
(define (question-equal? q1 q2)
|
||||
(or (and (literal? q1) (literal? q2)
|
||||
(literal-equal? q1 q2))
|
||||
(and (external? q1) (external? q2)
|
||||
(external-equal? q1 q2))))
|
||||
|
||||
(define-struct clause (srcloc head body) #:prefab)
|
||||
(define (clause-equal? c1 c2)
|
||||
|
@ -45,13 +61,13 @@
|
|||
(clause-head c2))
|
||||
(= (length (clause-body c1))
|
||||
(length (clause-body c2)))
|
||||
(andmap literal-equal?
|
||||
(andmap question-equal?
|
||||
(clause-body c1)
|
||||
(clause-body c2))))
|
||||
|
||||
(define-struct assertion (srcloc clause) #:prefab)
|
||||
(define-struct retraction (srcloc clause) #:prefab)
|
||||
(define-struct query (srcloc literal) #:prefab)
|
||||
(define-struct query (srcloc question) #:prefab)
|
||||
|
||||
(define statement/c (or/c assertion? retraction? query?))
|
||||
(define program/c (listof statement/c))
|
||||
|
@ -64,7 +80,7 @@
|
|||
[sym symbol?])]
|
||||
[variable-equal? (variable? variable? . -> . boolean?)]
|
||||
[struct constant ([srcloc srcloc/c]
|
||||
[datum datum/c])]
|
||||
[value any/c])]
|
||||
[constant-equal? (constant? constant? . -> . boolean?)]
|
||||
[term/c contract?]
|
||||
[term-equal? (term/c term/c . -> . boolean?)]
|
||||
|
@ -72,15 +88,23 @@
|
|||
[predicate datum/c]
|
||||
[terms (listof term/c)])]
|
||||
[literal-equal? (literal? literal? . -> . boolean?)]
|
||||
[struct external ([srcloc srcloc/c]
|
||||
[predicate-sym symbol?]
|
||||
[predicate procedure?]
|
||||
[arg-terms (listof term/c)]
|
||||
[ans-terms (listof term/c)])]
|
||||
[external-equal? (external? external? . -> . boolean?)]
|
||||
[question/c contract?]
|
||||
[question-equal? (question/c question/c . -> . boolean?)]
|
||||
[struct clause ([srcloc srcloc/c]
|
||||
[head literal?]
|
||||
[body (listof literal?)])]
|
||||
[body (listof question/c)])]
|
||||
[clause-equal? (clause? clause? . -> . boolean?)]
|
||||
[struct assertion ([srcloc srcloc/c]
|
||||
[clause clause?])]
|
||||
[struct retraction ([srcloc srcloc/c]
|
||||
[clause clause?])]
|
||||
[struct query ([srcloc srcloc/c]
|
||||
[literal literal?])]
|
||||
[question question/c])]
|
||||
[statement/c contract?]
|
||||
[program/c contract?])
|
||||
|
|
|
@ -14,9 +14,9 @@
|
|||
"Unsafe clause in assertion"
|
||||
(datum->syntax #f (format-statement s) (assertion-srcloc s))))))
|
||||
|
||||
(define (print-literals ls)
|
||||
(define (print-questions ls)
|
||||
(displayln
|
||||
(format-literals ls)))
|
||||
(format-questions ls)))
|
||||
|
||||
(define (eval-program p)
|
||||
(for-each eval-top-level-statement p))
|
||||
|
@ -24,7 +24,7 @@
|
|||
(define (eval-top-level-statement s)
|
||||
(define v (eval-statement s))
|
||||
(unless (void? v)
|
||||
(print-literals v)))
|
||||
(print-questions v)))
|
||||
|
||||
(define (eval-statement s)
|
||||
(cond
|
||||
|
@ -33,7 +33,7 @@
|
|||
[(retraction? s)
|
||||
(retract! (current-theory) (retraction-clause s))]
|
||||
[(query? s)
|
||||
(prove (current-theory) (query-literal s))]))
|
||||
(prove (current-theory) (query-question s))]))
|
||||
|
||||
(define (eval-program/fresh p)
|
||||
(let loop ([thy (make-immutable-theory)]
|
||||
|
@ -48,14 +48,14 @@
|
|||
[(retraction? s)
|
||||
(retract thy (retraction-clause s))]
|
||||
[(query? s)
|
||||
(print-literals (prove thy (query-literal s)))
|
||||
(print-questions (prove thy (query-question s)))
|
||||
thy])
|
||||
(rest p))))))
|
||||
|
||||
(provide/contract
|
||||
[current-theory (parameter/c mutable-theory/c)]
|
||||
[print-literals ((listof literal?) . -> . void)]
|
||||
[print-questions ((listof question/c) . -> . void)]
|
||||
[eval-program (program/c . -> . void)]
|
||||
[eval-top-level-statement (statement/c . -> . void)]
|
||||
[eval-statement (statement/c . -> . (or/c void (listof literal?)))]
|
||||
[eval-statement (statement/c . -> . (or/c void (listof question/c)))]
|
||||
[eval-program/fresh (program/c . -> . immutable-theory/c)])
|
|
@ -4,19 +4,19 @@
|
|||
|
||||
(define (format-datum s)
|
||||
(cond
|
||||
[(string? s)
|
||||
(text (format "~S" s))]
|
||||
[(symbol? s)
|
||||
(text (symbol->string s))]))
|
||||
(text (symbol->string s))]
|
||||
[else
|
||||
(text (format "~S" s))]))
|
||||
(define (format-variable v)
|
||||
(format-datum (variable-sym v)))
|
||||
(define (format-constant c)
|
||||
(format-datum (constant-datum c)))
|
||||
(define (format-term t)
|
||||
(cond
|
||||
[(variable? t)
|
||||
(format-datum (constant-value c)))
|
||||
(define format-term
|
||||
(match-lambda
|
||||
[(? variable? t)
|
||||
(format-variable t)]
|
||||
[(constant? t)
|
||||
[(? constant? t)
|
||||
(format-constant t)]))
|
||||
(define (format-literal l)
|
||||
(match l
|
||||
|
@ -29,10 +29,27 @@
|
|||
lparen
|
||||
(v-concat/s (apply-infix ", " (map format-term terms)))
|
||||
rparen)]))
|
||||
(define (format-literals ls)
|
||||
(define format-external
|
||||
(match-lambda
|
||||
[(external _ pred-sym pred args anss)
|
||||
(h-append (format-datum pred-sym)
|
||||
lparen
|
||||
(v-concat/s (apply-infix ", " (map format-term args)))
|
||||
rparen
|
||||
(text " = ")
|
||||
lparen
|
||||
(v-concat/s (apply-infix ", " (map format-term anss)))
|
||||
rparen)]))
|
||||
(define format-question
|
||||
(match-lambda
|
||||
[(? literal? l)
|
||||
(format-literal l)]
|
||||
[(? external? e)
|
||||
(format-external e)]))
|
||||
(define (format-questions ls)
|
||||
(v-concat
|
||||
(append (map (lambda (l)
|
||||
(format-assertion (make-assertion #f (make-clause #f l (list)))))
|
||||
(h-append (format-question l) dot))
|
||||
ls)
|
||||
(list line))))
|
||||
(define (format-clause c)
|
||||
|
@ -49,7 +66,7 @@
|
|||
(h-append (format-clause (retraction-clause r))
|
||||
(char #\~)))
|
||||
(define (format-query q)
|
||||
(h-append (format-literal (query-literal q))
|
||||
(h-append (format-question (query-question q))
|
||||
(char #\?)))
|
||||
|
||||
(define (format-statement s)
|
||||
|
@ -66,7 +83,7 @@
|
|||
[format-constant (constant? . -> . doc?)]
|
||||
[format-term (term/c . -> . doc?)]
|
||||
[format-literal (literal? . -> . doc?)]
|
||||
[format-literals ((listof literal?) . -> . doc?)]
|
||||
[format-questions ((listof question/c) . -> . doc?)]
|
||||
[format-clause (clause? . -> . doc?)]
|
||||
[format-assertion (assertion? . -> . doc?)]
|
||||
[format-retraction (retraction? . -> . doc?)]
|
||||
|
|
|
@ -9,32 +9,52 @@
|
|||
[_
|
||||
t]))
|
||||
|
||||
(define (subst-terms env ts)
|
||||
(map (curry subst-term env) ts))
|
||||
|
||||
(define (subst-literal env lit)
|
||||
(make-literal (literal-srcloc lit)
|
||||
(literal-predicate lit)
|
||||
(map (lambda (t) (subst-term env t))
|
||||
(literal-terms lit))))
|
||||
(struct-copy
|
||||
literal lit
|
||||
[terms
|
||||
(subst-terms env (literal-terms lit))]))
|
||||
|
||||
(define (subst-external env ext)
|
||||
(struct-copy
|
||||
external ext
|
||||
[arg-terms
|
||||
(subst-terms env (external-arg-terms ext))]
|
||||
[ans-terms
|
||||
(subst-terms env (external-ans-terms ext))]))
|
||||
|
||||
(define (subst-question env q)
|
||||
(match q
|
||||
[(? literal?) (subst-literal env q)]
|
||||
[(? external?) (subst-external env q)]))
|
||||
|
||||
(define (subst-clause env c)
|
||||
(make-clause (clause-srcloc c)
|
||||
(subst-literal env (clause-head c))
|
||||
(map (lambda (l) (subst-literal env l))
|
||||
(clause-body c))))
|
||||
(clause (clause-srcloc c)
|
||||
(subst-literal env (clause-head c))
|
||||
(map (curry subst-question env)
|
||||
(clause-body c))))
|
||||
|
||||
(define (shuffle env lit)
|
||||
(match lit
|
||||
[(struct literal (_ pred terms))
|
||||
(let loop ([env env]
|
||||
[terms terms])
|
||||
(match terms
|
||||
[(list)
|
||||
env]
|
||||
[(list-rest (struct constant (_ value)) terms)
|
||||
(loop env terms)]
|
||||
[(list-rest (struct variable (srcloc var)) terms)
|
||||
(if (lookup env var)
|
||||
(loop env terms)
|
||||
(loop (extend env var (make-variable srcloc (gensym var))) terms))]))]))
|
||||
(define (shuffle-terms env terms)
|
||||
(match terms
|
||||
[(list)
|
||||
env]
|
||||
[(list-rest (constant _ value) terms)
|
||||
(shuffle-terms env terms)]
|
||||
[(list-rest (variable srcloc var) terms)
|
||||
(if (lookup env var)
|
||||
(shuffle-terms env terms)
|
||||
(shuffle-terms (extend env var (make-variable srcloc (gensym var)))
|
||||
terms))]))
|
||||
|
||||
(define (shuffle env q)
|
||||
(match q
|
||||
[(external _ _ pred arg-terms ans-terms)
|
||||
(shuffle-terms env (append arg-terms ans-terms))]
|
||||
[(literal _ pred terms)
|
||||
(shuffle-terms env terms)]))
|
||||
|
||||
(define (rename-clause c)
|
||||
(define env
|
||||
|
@ -44,11 +64,12 @@
|
|||
(clause-body c)))
|
||||
(subst-clause env c))
|
||||
|
||||
(define (rename-literal lit)
|
||||
(subst-literal (shuffle (empty-env) lit) lit))
|
||||
(define (rename-question q)
|
||||
(subst-question (shuffle (empty-env) q) q))
|
||||
|
||||
(provide/contract
|
||||
[subst-terms (env/c (listof term/c) . -> . (listof term/c))]
|
||||
[subst-term (env/c term/c . -> . term/c)]
|
||||
[subst-clause (env/c clause? . -> . clause?)]
|
||||
[rename-clause (clause? . -> . clause?)]
|
||||
[rename-literal (literal? . -> . literal?)])
|
||||
[rename-question (question/c . -> . question/c)])
|
|
@ -38,12 +38,22 @@
|
|||
[env (unify-terms env (rest ts1) (rest ts2))]))))
|
||||
|
||||
(define (unify l1 l2)
|
||||
(and (datum-equal? (literal-predicate l1)
|
||||
(literal-predicate l2))
|
||||
(unify-terms (empty-env)
|
||||
(literal-terms l1)
|
||||
(literal-terms l2))))
|
||||
(or (and (literal? l1) (literal? l2)
|
||||
(datum-equal? (literal-predicate l1)
|
||||
(literal-predicate l2))
|
||||
(unify-terms (empty-env)
|
||||
(literal-terms l1)
|
||||
(literal-terms l2)))
|
||||
(and (external? l1) (external? l2)
|
||||
(equal? (external-predicate l1)
|
||||
(external-predicate l2))
|
||||
(unify-terms (empty-env)
|
||||
(append (external-arg-terms l1)
|
||||
(external-ans-terms l1))
|
||||
(append (external-arg-terms l2)
|
||||
(external-ans-terms l2))))))
|
||||
|
||||
(provide/contract
|
||||
[unify (literal? literal? . -> . (or/c false/c env/c))]
|
||||
[unify (question/c question/c . -> . (or/c false/c env/c))]
|
||||
[unify-terms (env/c (listof term/c) (listof term/c) . -> . (or/c false/c env/c))]
|
||||
[unify-term (env/c term/c term/c . -> . (or/c false/c env/c))])
|
|
@ -35,13 +35,25 @@
|
|||
[_ #f]))
|
||||
|
||||
(define (variant? l1 l2)
|
||||
(and
|
||||
(datum-equal? (literal-predicate l1)
|
||||
(literal-predicate l2))
|
||||
(variant-terms
|
||||
(empty-env) (empty-env)
|
||||
(literal-terms l1)
|
||||
(literal-terms l2))))
|
||||
(or
|
||||
(and (literal? l1) (literal? l2)
|
||||
(datum-equal? (literal-predicate l1)
|
||||
(literal-predicate l2))
|
||||
(variant-terms
|
||||
(empty-env) (empty-env)
|
||||
(literal-terms l1)
|
||||
(literal-terms l2)))
|
||||
(and (external? l1) (external? l2)
|
||||
(equal? (external-predicate l1)
|
||||
(external-predicate l2))
|
||||
(variant-terms
|
||||
(empty-env) (empty-env)
|
||||
(external-arg-terms l1)
|
||||
(external-arg-terms l2))
|
||||
(variant-terms
|
||||
(empty-env) (empty-env)
|
||||
(external-ans-terms l1)
|
||||
(external-ans-terms l2)))))
|
||||
|
||||
(define (mem-literal lit ls)
|
||||
(ormap (lambda (l) (variant? lit l)) ls))
|
||||
|
@ -52,11 +64,21 @@
|
|||
[(variable? t)
|
||||
101]
|
||||
[(constant? t)
|
||||
(recur-hash (constant-datum t))]))
|
||||
(define ((mk-literal-hash recur-hash) l)
|
||||
(let loop ([code (recur-hash (literal-predicate l))]
|
||||
(recur-hash (constant-value t))]))
|
||||
(define ((mk-literal-hash recur-hash) q)
|
||||
(define-values
|
||||
(code terms)
|
||||
(match q
|
||||
[(? literal? l)
|
||||
(values (recur-hash (literal-predicate l))
|
||||
(literal-terms l))]
|
||||
[(? external? e)
|
||||
(values (recur-hash (external-predicate e))
|
||||
(append (external-arg-terms e)
|
||||
(external-ans-terms e)))]))
|
||||
(let loop ([code code]
|
||||
[i 0]
|
||||
[terms (literal-terms l)])
|
||||
[terms terms])
|
||||
(if (empty? terms)
|
||||
code
|
||||
(loop (+ code (term-hash (first terms) recur-hash) (* i -7))
|
||||
|
@ -78,6 +100,6 @@
|
|||
(provide/contract
|
||||
[literal-tbl/c contract?]
|
||||
[make-literal-tbl (-> literal-tbl/c)]
|
||||
[literal-tbl-find (literal-tbl/c literal? . -> . (or/c false/c any/c))]
|
||||
[literal-tbl-replace! (literal-tbl/c literal? any/c . -> . void)]
|
||||
[mem-literal (literal? (listof literal?) . -> . boolean?)])
|
||||
[literal-tbl-find (literal-tbl/c question/c . -> . (or/c false/c any/c))]
|
||||
[literal-tbl-replace! (literal-tbl/c question/c any/c . -> . void)]
|
||||
[mem-literal (question/c (listof question/c) . -> . boolean?)])
|
|
@ -11,7 +11,12 @@
|
|||
(andmap (lambda (v)
|
||||
(ormap (lambda (l)
|
||||
(ormap (lambda (t) (term-equal? t v))
|
||||
(literal-terms l)))
|
||||
(cond
|
||||
[(literal? l)
|
||||
(literal-terms l)]
|
||||
[(external? l)
|
||||
(append (external-arg-terms l)
|
||||
(external-ans-terms l))])))
|
||||
(clause-body c)))
|
||||
head-vars))
|
||||
|
||||
|
@ -52,20 +57,20 @@
|
|||
(hash-ref thy (literal-key lit) empty))
|
||||
|
||||
(define-struct subgoal
|
||||
(literal
|
||||
(question
|
||||
[facts #:mutable]
|
||||
[waiters #:mutable]))
|
||||
|
||||
(define (resolve c lit)
|
||||
(define (resolve c q)
|
||||
(define body (clause-body c))
|
||||
(and (not (empty? body))
|
||||
(cond
|
||||
[(unify (first body) (rename-literal lit))
|
||||
[(unify (first body) (rename-question q))
|
||||
=> (lambda (env)
|
||||
(subst-clause env (make-clause (clause-srcloc c) (clause-head c) (rest body))))]
|
||||
[else #f])))
|
||||
|
||||
(define (prove thy lit)
|
||||
(define (prove thy q)
|
||||
(define subgoals (make-literal-tbl))
|
||||
(define (fact! sg lit)
|
||||
(unless (mem-literal lit (subgoal-facts sg))
|
||||
|
@ -100,12 +105,25 @@
|
|||
(define renamed (rename-clause clause))
|
||||
(define selected (clause-head renamed))
|
||||
(cond
|
||||
[(unify (subgoal-literal sg) selected)
|
||||
[(unify (subgoal-question sg) selected)
|
||||
=> (lambda (env)
|
||||
(add-clause! sg (subst-clause env renamed)))]))
|
||||
(get thy (subgoal-literal sg))))
|
||||
(get thy (subgoal-question sg))))
|
||||
(define (search! sg)
|
||||
(match (subgoal-literal sg)
|
||||
(match (subgoal-question sg)
|
||||
[(external srcloc pred-sym pred args anss)
|
||||
(and (andmap constant? args)
|
||||
(call-with-values
|
||||
(λ ()
|
||||
(apply pred (map constant-value args)))
|
||||
(λ resolved-vals
|
||||
(define resolved-anss
|
||||
(map (curry constant #f)
|
||||
resolved-vals))
|
||||
(cond
|
||||
[(unify-terms (empty-env) anss resolved-anss)
|
||||
=> (λ (env)
|
||||
(fact! sg (external srcloc pred-sym pred args (subst-terms env anss))))]))))]
|
||||
[(struct literal (srcloc '= (list a b)))
|
||||
(define (equal-test a b)
|
||||
(when (term-equal? a b)
|
||||
|
@ -116,8 +134,8 @@
|
|||
[else (equal-test a b)])]
|
||||
[_
|
||||
(search-theory! sg)]))
|
||||
(define sg (make-subgoal lit empty empty))
|
||||
(literal-tbl-replace! subgoals lit sg)
|
||||
(define sg (make-subgoal q empty empty))
|
||||
(literal-tbl-replace! subgoals q sg)
|
||||
(search! sg)
|
||||
(subgoal-facts sg))
|
||||
|
||||
|
@ -133,4 +151,4 @@
|
|||
[retract (immutable-theory/c clause? . -> . immutable-theory/c)]
|
||||
[assume! (mutable-theory/c safe-clause? . -> . void)]
|
||||
[retract! (mutable-theory/c clause? . -> . void)]
|
||||
[prove (theory/c literal? . -> . (listof literal?))])
|
||||
[prove (theory/c question/c . -> . (listof question/c))])
|
|
@ -130,13 +130,14 @@ 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))
|
||||
@(require (for-label datalog
|
||||
racket))
|
||||
|
||||
@defmodulelang[datalog/sexp]
|
||||
|
||||
The semantics of this language is the same as the normal Datalog language, except it uses a parenthetical syntax.
|
||||
The semantics of this language is the same as the normal Datalog language, except it uses the parenthetical syntax described in @secref{interop}.
|
||||
|
||||
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.
|
||||
All identifiers in @racketmodname[racket/base] are available for use as predicate symbols or constant values. Top-level identifiers and datums are not otherwise allowed in the program. The program may contain @racket[require] expressions.
|
||||
|
||||
The following is a program:
|
||||
@racketmod[datalog/sexp
|
||||
|
@ -152,7 +153,13 @@ The following is a program:
|
|||
(path Z Y)))
|
||||
(? (path X Y))]
|
||||
|
||||
The Parenthetical Datalog REPL accepts new statements that are executed as if they were in the original program text.
|
||||
This is also a program:
|
||||
@racketmod[datalog/sexp
|
||||
(require racket/math)
|
||||
|
||||
(? (sqr 4 :- X))]
|
||||
|
||||
The Parenthetical Datalog REPL accepts new statements that are executed as if they were in the original program text, except @racket[require] is not allowed.
|
||||
|
||||
@include-section["racket.scrbl"]
|
||||
|
||||
|
|
|
@ -8,7 +8,7 @@
|
|||
"../main.rkt")
|
||||
"utils.rkt")
|
||||
|
||||
@title{Racket Interoperability}
|
||||
@title[#:tag "interop"]{Racket Interoperability}
|
||||
|
||||
@defmodule[datalog]
|
||||
|
||||
|
@ -45,7 +45,10 @@ The Datalog database can be directly used by Racket programs through this API.
|
|||
|
||||
(let ([x 'joseph2])
|
||||
(datalog family
|
||||
(? (parent x X))))]
|
||||
(? (parent x X))))
|
||||
|
||||
(datalog family
|
||||
(? (add1 1 :- X)))]
|
||||
|
||||
@defthing[mutable-theory/c contract?]{ A contract for Datalog theories. }
|
||||
|
||||
|
@ -58,11 +61,18 @@ The Datalog database can be directly used by Racket programs through this API.
|
|||
@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.
|
||||
|
||||
Statements are either assertions, retractions, or queries.
|
||||
|
||||
@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[(:- literal question ...)]{ A conditional clause. }
|
||||
|
||||
@defform[(? question)]{ Queries the literal and prints the result literals. }
|
||||
|
||||
Questions are either literals or external queries.
|
||||
Literals are represented as @racket[identifier] or @racket[(identifier term ...)].
|
||||
Questions are represented as @racket[(identifier term ... :- term ...)], where @racket[identifier] is bound to a procedure that when given the first set of terms as arguments returns the second set of terms as values.
|
||||
A term is either a non-capitalized identifiers for a constant symbol, a Racket datum for a constant datum, or a capitalized identifier for a variable symbol. Bound identifiers in terms are treated as datums.
|
||||
|
||||
|
|
|
@ -1,15 +1,36 @@
|
|||
#lang racket
|
||||
(require (for-syntax syntax/parse)
|
||||
#lang racket/base
|
||||
(require (for-syntax syntax/parse
|
||||
racket/list
|
||||
racket/base)
|
||||
datalog/stx
|
||||
datalog/runtime)
|
||||
|
||||
(define lang-theory (make-theory))
|
||||
|
||||
(define-syntax module-begin
|
||||
(syntax-rules ()
|
||||
[(_ stmt ...)
|
||||
(#%module-begin
|
||||
(datalog! lang-theory stmt ...))]))
|
||||
(define-for-syntax (partition-requires es)
|
||||
(define-values (rs stmts)
|
||||
(partition
|
||||
(λ (e-stx)
|
||||
(syntax-parse
|
||||
e-stx
|
||||
#:literals (require)
|
||||
[(require . r)
|
||||
#t]
|
||||
[_
|
||||
#f]))
|
||||
(syntax->list es)))
|
||||
(list rs stmts))
|
||||
|
||||
(define-syntax (module-begin stx)
|
||||
(syntax-case stx ()
|
||||
[(_ . es)
|
||||
(with-syntax ([((requires ...)
|
||||
(stmt ...))
|
||||
(partition-requires #'es)])
|
||||
(syntax/loc stx
|
||||
(#%module-begin
|
||||
requires ...
|
||||
(datalog! lang-theory stmt ...))))]))
|
||||
|
||||
(define-syntax top-interaction
|
||||
(syntax-rules ()
|
||||
|
@ -18,4 +39,7 @@
|
|||
|
||||
(provide (rename-out [top-interaction #%top-interaction]
|
||||
[module-begin #%module-begin])
|
||||
(except-out (all-from-out racket/base)
|
||||
#%top-interaction
|
||||
#%module-begin)
|
||||
! ~ ? :-)
|
|
@ -21,6 +21,10 @@
|
|||
|
||||
(define literal->sexp
|
||||
(match-lambda
|
||||
[(external _ pred-sym _ args anss)
|
||||
`(,pred-sym ,@(map term->datum args)
|
||||
:-
|
||||
,@(map term->datum anss))]
|
||||
[(literal _ pred ts)
|
||||
(list* pred (map term->datum ts))]))
|
||||
|
||||
|
@ -49,57 +53,63 @@
|
|||
(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)))]))
|
||||
[(_ (~and tstx (! c)))
|
||||
(quasisyntax/loc #'tstx
|
||||
(assertion #'#,#'tstx (datalog-clause c)))]
|
||||
[(_ (~and tstx (~ c)))
|
||||
(quasisyntax/loc #'tstx
|
||||
(retraction #'#,#'tstx (datalog-clause c)))]
|
||||
[(_ (~and tstx (? l)))
|
||||
(quasisyntax/loc #'tstx
|
||||
(query #'#,#'tstx (datalog-literal l)))]))
|
||||
|
||||
(define-syntax (datalog-clause stx)
|
||||
(syntax-parse
|
||||
stx
|
||||
#:literals (:-)
|
||||
[(_ (:- head body ...))
|
||||
(quasisyntax/loc stx
|
||||
(clause #'#,stx (datalog-literal head)
|
||||
[(_ (~and tstx (:- head body ...)))
|
||||
(quasisyntax/loc #'tstx
|
||||
(clause #'#,#'tstx (datalog-literal head)
|
||||
(list (datalog-literal body) ...)))]
|
||||
[(_ e)
|
||||
(quasisyntax/loc stx
|
||||
(clause #'#,stx (datalog-literal e) empty))]))
|
||||
(quasisyntax/loc #'e
|
||||
(clause #'#,#'e (datalog-literal e) empty))]))
|
||||
|
||||
(define-syntax (datalog-literal stx)
|
||||
(syntax-parse
|
||||
stx
|
||||
#:literals (:-)
|
||||
[(_ sym:id)
|
||||
(quasisyntax/loc stx
|
||||
(literal #'#,stx 'sym empty))]
|
||||
[(_ (sym:id e ...))
|
||||
(quasisyntax/loc stx
|
||||
(literal #'#,stx 'sym
|
||||
(quasisyntax/loc #'sym
|
||||
(literal #'#,#'sym 'sym empty))]
|
||||
[(_ (~and tstx (sym:id arg ... :- ans ...)))
|
||||
(quasisyntax/loc #'tstx
|
||||
(external #'#,#'tstx 'sym sym
|
||||
(list (datalog-term arg) ...)
|
||||
(list (datalog-term ans) ...)))]
|
||||
[(_ (~and tstx (sym:id e ...)))
|
||||
(quasisyntax/loc #'tstx
|
||||
(literal #'#,#'tstx '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))]
|
||||
(quasisyntax/loc #'sym
|
||||
(constant #'#,#'sym sym))]
|
||||
[(char-upper-case? (string-ref (symbol->string (syntax->datum #'sym)) 0))
|
||||
(quasisyntax/loc stx
|
||||
(variable #'#,stx 'sym))]
|
||||
(quasisyntax/loc #'sym
|
||||
(variable #'#,#'sym 'sym))]
|
||||
[else
|
||||
(quasisyntax/loc stx
|
||||
(constant #'#,stx 'sym))])]))
|
||||
(quasisyntax/loc #'sym
|
||||
(constant #'#,#'sym 'sym))])]
|
||||
[(_ sym:expr)
|
||||
(quasisyntax/loc #'sym
|
||||
(constant #'#,#'sym sym))]))
|
||||
|
||||
(provide datalog datalog!
|
||||
:- ! ~ ?)
|
||||
|
|
|
@ -22,22 +22,17 @@
|
|||
port->lines))
|
||||
(filter (lambda (l)
|
||||
(not (string=? l "")))
|
||||
(file->lines test-txt))
|
||||
))
|
||||
(file->lines test-txt))))
|
||||
|
||||
(define (test-files d)
|
||||
(for ([f (in-list (directory-list d))]
|
||||
#:when (regexp-match #rx"rkt$" (path->bytes f)))
|
||||
(test-example (path->string (path-replace-suffix f #"")))))
|
||||
|
||||
(test-suite
|
||||
(path->string examples-dir)
|
||||
|
||||
(test-example "ancestor")
|
||||
(test-example "bidipath")
|
||||
(test-example "laps")
|
||||
(test-example "long")
|
||||
(test-example "path")
|
||||
(test-example "pq")
|
||||
(test-example "revpath")
|
||||
(test-example "says")
|
||||
(test-example "true")
|
||||
(test-example "tutorial")))
|
||||
(test-files examples-dir)))
|
||||
|
||||
(define eval-tests
|
||||
(test-suite
|
||||
|
|
10
collects/tests/datalog/paren-examples/add1.rkt
Normal file
10
collects/tests/datalog/paren-examples/add1.rkt
Normal file
|
@ -0,0 +1,10 @@
|
|||
#lang datalog/sexp
|
||||
(? (add1 2 :- X))
|
||||
|
||||
(! (:- (add2 X Y)
|
||||
(add1 X :- Z)
|
||||
(add1 Z :- Y)))
|
||||
|
||||
(? (add2 1 3))
|
||||
|
||||
(? (add1 X :- 1))
|
3
collects/tests/datalog/paren-examples/add1.txt
Normal file
3
collects/tests/datalog/paren-examples/add1.txt
Normal file
|
@ -0,0 +1,3 @@
|
|||
add1(2) = (3).
|
||||
|
||||
add2(1, 3).
|
4
collects/tests/datalog/paren-examples/req.rkt
Normal file
4
collects/tests/datalog/paren-examples/req.rkt
Normal file
|
@ -0,0 +1,4 @@
|
|||
#lang datalog/sexp
|
||||
(require racket/math)
|
||||
|
||||
(? (sqr 4 :- X))
|
1
collects/tests/datalog/paren-examples/req.txt
Normal file
1
collects/tests/datalog/paren-examples/req.txt
Normal file
|
@ -0,0 +1 @@
|
|||
sqr(4) = (16).
|
|
@ -85,14 +85,14 @@
|
|||
'v1))))
|
||||
|
||||
(test-suite
|
||||
"rename-literal"
|
||||
(test-equal? "l" (rename-literal (make-literal #f 'lit (list (make-constant #f 'v1))))
|
||||
"rename-question"
|
||||
(test-equal? "l" (rename-question (make-literal #f 'lit (list (make-constant #f 'v1))))
|
||||
(make-literal #f 'lit (list (make-constant #f 'v1))))
|
||||
(test-not-false "l"
|
||||
(gensym-var?
|
||||
(first
|
||||
(literal-terms
|
||||
(rename-literal (make-literal #f 'lit (list (make-variable #f 'v1)))))))))
|
||||
(rename-question (make-literal #f 'lit (list (make-variable #f 'v1)))))))))
|
||||
|
||||
(test-suite
|
||||
"rename-clause"
|
||||
|
|
|
@ -3,7 +3,7 @@
|
|||
datalog/ast
|
||||
datalog/private/env
|
||||
datalog/private/unify)
|
||||
(require/expose datalog/private/unify (chase unify-terms))
|
||||
(require/expose datalog/private/unify (chase))
|
||||
|
||||
(provide unify-tests)
|
||||
|
||||
|
|
|
@ -54,4 +54,9 @@
|
|||
(list '(parent joseph2 joseph1)
|
||||
'(parent joseph2 lucy))
|
||||
|
||||
(datalog parent
|
||||
(? (add1 1 :- X)))
|
||||
=>
|
||||
(list '(add1 1 :- 2))
|
||||
|
||||
)
|
Loading…
Reference in New Issue
Block a user