Adding fake lambdas to get arrows on clauses.
original commit: 77b6709da1760b1766c4e1fd05366e47460c53b7
This commit is contained in:
Jay McCarthy
parent
380eb82c43
dfb1da8e37
5c82f510da
a5c2d46d36
f514febf9d
f43cb23c83
93a28ed14e
a89d757639
0a86976eb1
commit
5e021c9a87
110
collects/datalog/ast.rkt
Normal file
110
collects/datalog/ast.rkt
Normal file
|
|
@ -0,0 +1,110 @@
|
|||
#lang racket
|
||||
|
||||
(define srcloc/c
|
||||
(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))))
|
||||
|
||||
(define datum/c (or/c string? symbol?))
|
||||
(define datum-equal? equal?)
|
||||
|
||||
(define-struct variable (srcloc sym) #:prefab)
|
||||
(define (variable-equal? v1 v2)
|
||||
(eq? (variable-sym v1) (variable-sym v2)))
|
||||
(define-struct constant (srcloc value) #:prefab)
|
||||
(define (constant-equal? v1 v2)
|
||||
(equal? (constant-value v1) (constant-value v2)))
|
||||
|
||||
(define term/c (or/c variable? constant?))
|
||||
(define (term-equal? t1 t2)
|
||||
(cond
|
||||
[(and (variable? t1) (variable? t2))
|
||||
(variable-equal? t1 t2)]
|
||||
[(and (constant? t1) (constant? t2))
|
||||
(constant-equal? t1 t2)]
|
||||
[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))
|
||||
(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)
|
||||
(and (literal-equal? (clause-head c1)
|
||||
(clause-head c2))
|
||||
(= (length (clause-body c1))
|
||||
(length (clause-body c2)))
|
||||
(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 question) #:prefab)
|
||||
|
||||
(define statement/c (or/c assertion? retraction? query?))
|
||||
(define program/c (listof statement/c))
|
||||
|
||||
(provide/contract
|
||||
[srcloc/c contract?]
|
||||
[datum/c contract?]
|
||||
[datum-equal? (datum/c datum/c . -> . boolean?)]
|
||||
[struct variable ([srcloc srcloc/c]
|
||||
[sym symbol?])]
|
||||
[variable-equal? (variable? variable? . -> . boolean?)]
|
||||
[struct constant ([srcloc srcloc/c]
|
||||
[value any/c])]
|
||||
[constant-equal? (constant? constant? . -> . boolean?)]
|
||||
[term/c contract?]
|
||||
[term-equal? (term/c term/c . -> . boolean?)]
|
||||
[struct literal ([srcloc srcloc/c]
|
||||
[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 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]
|
||||
[question question/c])]
|
||||
[statement/c contract?]
|
||||
[program/c contract?])
|
||||
43
collects/datalog/eval.rkt
Normal file
43
collects/datalog/eval.rkt
Normal file
|
|
@ -0,0 +1,43 @@
|
|||
#lang racket
|
||||
(require racket/list
|
||||
"ast.rkt"
|
||||
"pretty.rkt"
|
||||
"runtime.rkt")
|
||||
|
||||
(define current-theory (make-parameter (make-theory)))
|
||||
|
||||
(define (assume-if-safe assume thy s)
|
||||
(let ([c (assertion-clause s)])
|
||||
(if (safe-clause? c)
|
||||
(assume thy c)
|
||||
(raise-syntax-error 'datalog
|
||||
"Unsafe clause in assertion"
|
||||
(datum->syntax #f (format-statement s) (assertion-srcloc s))))))
|
||||
|
||||
(define (print-questions ls)
|
||||
(displayln
|
||||
(format-questions ls)))
|
||||
|
||||
(define (eval-program p)
|
||||
(for-each eval-top-level-statement p))
|
||||
|
||||
(define (eval-top-level-statement s)
|
||||
(define v (eval-statement s))
|
||||
(unless (void? v)
|
||||
(print-questions v)))
|
||||
|
||||
(define (eval-statement s)
|
||||
(cond
|
||||
[(assertion? s)
|
||||
(assume-if-safe assume! (current-theory) s)]
|
||||
[(retraction? s)
|
||||
(retract! (current-theory) (retraction-clause s))]
|
||||
[(query? s)
|
||||
(prove (current-theory) (query-question s))]))
|
||||
|
||||
(provide/contract
|
||||
[current-theory (parameter/c theory/c)]
|
||||
[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 question/c)))])
|
||||
3
collects/datalog/info.rkt
Normal file
3
collects/datalog/info.rkt
Normal file
|
|
@ -0,0 +1,3 @@
|
|||
#lang setup/infotab
|
||||
(define scribblings '(["scribblings/datalog.scrbl" (multi-page) (language)]))
|
||||
(define compile-omit-paths '("tests"))
|
||||
33
collects/datalog/lang/reader.rkt
Normal file
33
collects/datalog/lang/reader.rkt
Normal file
|
|
@ -0,0 +1,33 @@
|
|||
(module reader syntax/module-reader
|
||||
#:language 'datalog/sexp/lang
|
||||
#:read (lambda ([in (current-input-port)]) (this-read-syntax #f in))
|
||||
#:read-syntax this-read-syntax
|
||||
#:whole-body-readers? #t
|
||||
#:info (lambda (key defval default)
|
||||
; XXX Should have different comment character key
|
||||
(case key
|
||||
[(drracket:submit-predicate)
|
||||
(dynamic-require 'datalog/tool/submit 'repl-submit?)]
|
||||
[(color-lexer)
|
||||
(dynamic-require 'datalog/tool/syntax-color 'get-syntax-token)]
|
||||
[(configure-runtime)
|
||||
(λ () (current-read-interaction even-read))]
|
||||
[else (default key defval)]))
|
||||
(require datalog/parse
|
||||
datalog/private/compiler)
|
||||
|
||||
(define (this-read-syntax [src #f] [in (current-input-port)])
|
||||
(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)))
|
||||
(current-read-interaction odd-read)))
|
||||
(define (odd-read src ip)
|
||||
(current-read-interaction even-read)
|
||||
eof))
|
||||
6
collects/datalog/main.rkt
Normal file
6
collects/datalog/main.rkt
Normal file
|
|
@ -0,0 +1,6 @@
|
|||
#lang racket
|
||||
(require "runtime.rkt"
|
||||
"stx.rkt")
|
||||
(provide make-theory
|
||||
theory/c
|
||||
(all-from-out "stx.rkt"))
|
||||
81
collects/datalog/parse.rkt
Normal file
81
collects/datalog/parse.rkt
Normal file
|
|
@ -0,0 +1,81 @@
|
|||
#lang racket
|
||||
(require parser-tools/lex
|
||||
parser-tools/yacc
|
||||
"private/lex.rkt"
|
||||
"ast.rkt")
|
||||
|
||||
(define current-source-name (make-parameter #f))
|
||||
|
||||
(define (make-srcloc start-pos end-pos)
|
||||
(list (current-source-name)
|
||||
(position-line start-pos)
|
||||
(position-col start-pos)
|
||||
(position-offset start-pos)
|
||||
(- (position-offset end-pos) (position-offset start-pos))))
|
||||
|
||||
(define-values
|
||||
(program-parser statement-parser clause-parser literal-parser)
|
||||
(apply
|
||||
values
|
||||
(parser
|
||||
(start program statement clause literal)
|
||||
(end EOF)
|
||||
(tokens dtokens dpunct)
|
||||
(src-pos)
|
||||
(error
|
||||
(lambda (tok-ok? tok-name tok-value start-pos end-pos)
|
||||
(raise-syntax-error 'datalog
|
||||
(if tok-ok?
|
||||
(format "Unexpected token ~S" tok-name)
|
||||
(format "Invalid token ~S" tok-name))
|
||||
(datum->syntax #f tok-value (make-srcloc start-pos end-pos)))))
|
||||
(grammar
|
||||
(program [(statements) $1])
|
||||
(statements [(statement) (list $1)]
|
||||
[(statement statements) (list* $1 $2)])
|
||||
(statement [(assertion) $1]
|
||||
[(query) $1]
|
||||
[(retraction) $1])
|
||||
(assertion [(clause DOT) (make-assertion (make-srcloc $1-start-pos $2-end-pos) $1)])
|
||||
(retraction [(clause TILDE) (make-retraction (make-srcloc $1-start-pos $2-end-pos) $1)])
|
||||
(query [(literal QMARK) (make-query (make-srcloc $1-start-pos $2-end-pos) $1)])
|
||||
(clause [(literal TSTILE body) (make-clause (make-srcloc $1-start-pos $3-end-pos) $1 $3)]
|
||||
[(literal) (make-clause (make-srcloc $1-start-pos $1-end-pos) $1 empty)])
|
||||
(body [(literal COMMA body) (list* $1 $3)]
|
||||
[(literal) (list $1)])
|
||||
(literal [(predicate-sym LPAREN RPAREN) (make-literal (make-srcloc $1-start-pos $3-end-pos) $1 empty)]
|
||||
[(predicate-sym LPAREN terms RPAREN) (make-literal (make-srcloc $1-start-pos $4-end-pos) $1 $3)]
|
||||
[(predicate-sym) (make-literal (make-srcloc $1-start-pos $1-end-pos) $1 empty)]
|
||||
[(term EQUAL term) (make-literal (make-srcloc $1-start-pos $3-end-pos) '= (list $1 $3))])
|
||||
(predicate-sym [(IDENTIFIER) (string->symbol $1)]
|
||||
[(STRING) $1])
|
||||
(terms [(term) (list $1)]
|
||||
[(term COMMA terms) (list* $1 $3)])
|
||||
(term [(VARIABLE) (make-variable (make-srcloc $1-start-pos $1-end-pos) (string->symbol $1))]
|
||||
[(constant) (make-constant (make-srcloc $1-start-pos $1-end-pos) $1)])
|
||||
(constant [(IDENTIFIER) (string->symbol $1)]
|
||||
[(STRING) $1]))
|
||||
|
||||
(suppress))))
|
||||
|
||||
(define ((mk-parser which) ip)
|
||||
(define (go)
|
||||
(port-count-lines! ip)
|
||||
(which (lambda () (dlexer ip))))
|
||||
(if (current-source-name)
|
||||
(go)
|
||||
(parameterize ([current-source-name (object-name ip)]
|
||||
[file-path (object-name ip)])
|
||||
(go))))
|
||||
|
||||
(define parse-literal (mk-parser literal-parser))
|
||||
(define parse-clause (mk-parser clause-parser))
|
||||
(define parse-statement (mk-parser statement-parser))
|
||||
(define parse-program (mk-parser program-parser))
|
||||
|
||||
(provide/contract
|
||||
[current-source-name (parameter/c any/c)]
|
||||
[parse-literal (input-port? . -> . literal?)]
|
||||
[parse-clause (input-port? . -> . clause?)]
|
||||
[parse-statement (input-port? . -> . statement/c)]
|
||||
[parse-program (input-port? . -> . program/c)])
|
||||
92
collects/datalog/pretty.rkt
Normal file
92
collects/datalog/pretty.rkt
Normal file
|
|
@ -0,0 +1,92 @@
|
|||
#lang racket
|
||||
(require "private/pprint.rkt"
|
||||
"ast.rkt")
|
||||
|
||||
(define (format-datum s)
|
||||
(cond
|
||||
[(symbol? 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-value c)))
|
||||
(define format-term
|
||||
(match-lambda
|
||||
[(? variable? t)
|
||||
(format-variable t)]
|
||||
[(? constant? t)
|
||||
(format-constant t)]))
|
||||
(define (format-literal l)
|
||||
(match l
|
||||
[(struct literal (_ pred (list)))
|
||||
(format-datum pred)]
|
||||
[(struct literal (_ '= (list a b)))
|
||||
(h-append (format-term a) space (text "=") space (format-term b))]
|
||||
[(struct literal (_ pred terms))
|
||||
(h-append (format-datum pred)
|
||||
lparen
|
||||
(v-concat/s (apply-infix ", " (map format-term terms)))
|
||||
rparen)]))
|
||||
(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)
|
||||
(h-append (format-question l) dot))
|
||||
ls)
|
||||
(list line))))
|
||||
(define (format-clause c)
|
||||
(if (empty? (clause-body c))
|
||||
(format-literal (clause-head c))
|
||||
(nest 4
|
||||
(v-concat/s
|
||||
(list* (h-append (format-literal (clause-head c)) space (text ":-") space)
|
||||
(apply-infix ", " (map format-literal (clause-body c))))))))
|
||||
(define (format-assertion a)
|
||||
(h-append (format-clause (assertion-clause a))
|
||||
dot))
|
||||
(define (format-retraction r)
|
||||
(h-append (format-clause (retraction-clause r))
|
||||
(char #\~)))
|
||||
(define (format-query q)
|
||||
(h-append (format-question (query-question q))
|
||||
(char #\?)))
|
||||
|
||||
(define (format-statement s)
|
||||
(cond
|
||||
[(assertion? s) (format-assertion s)]
|
||||
[(retraction? s) (format-retraction s)]
|
||||
[(query? s) (format-query s)]))
|
||||
(define (format-program p)
|
||||
(v-concat (map format-statement p)))
|
||||
|
||||
(provide/contract
|
||||
[format-datum (datum/c . -> . doc?)]
|
||||
[format-variable (variable? . -> . doc?)]
|
||||
[format-constant (constant? . -> . doc?)]
|
||||
[format-term (term/c . -> . doc?)]
|
||||
[format-literal (literal? . -> . doc?)]
|
||||
[format-questions ((listof question/c) . -> . doc?)]
|
||||
[format-clause (clause? . -> . doc?)]
|
||||
[format-assertion (assertion? . -> . doc?)]
|
||||
[format-retraction (retraction? . -> . doc?)]
|
||||
[format-query (query? . -> . doc?)]
|
||||
[format-statement (statement/c . -> . doc?)]
|
||||
[format-program (program/c . -> . doc?)])
|
||||
56
collects/datalog/private/compiler.rkt
Normal file
56
collects/datalog/private/compiler.rkt
Normal file
|
|
@ -0,0 +1,56 @@
|
|||
#lang racket/base
|
||||
(require racket/contract
|
||||
racket/match
|
||||
datalog/ast
|
||||
datalog/stx)
|
||||
(require (for-template datalog/stx))
|
||||
|
||||
(provide/contract
|
||||
[compile-program (program/c . -> . (listof syntax?))]
|
||||
[compile-statement (statement/c . -> . syntax?)])
|
||||
|
||||
(define (compile-program p)
|
||||
(map compile-statement p))
|
||||
|
||||
(define compile-statement
|
||||
(match-lambda
|
||||
[(assertion srcloc c)
|
||||
(define srcstx (datum->syntax #f 'x srcloc))
|
||||
(quasisyntax/loc srcstx
|
||||
(! #,(compile-clause c)))]
|
||||
[(retraction srcloc c)
|
||||
(define srcstx (datum->syntax #f 'x srcloc))
|
||||
(quasisyntax/loc srcstx
|
||||
(~ #,(compile-clause c)))]
|
||||
[(query srcloc l)
|
||||
(define srcstx (datum->syntax #f 'x srcloc))
|
||||
(quasisyntax/loc srcstx
|
||||
(? #,(compile-literal l)))]))
|
||||
|
||||
(define compile-clause
|
||||
(match-lambda
|
||||
[(clause srcloc head (list))
|
||||
(define srcstx (datum->syntax #f 'x srcloc))
|
||||
(compile-literal head)]
|
||||
[(clause srcloc head body)
|
||||
(define srcstx (datum->syntax #f 'x srcloc))
|
||||
(quasisyntax/loc srcstx
|
||||
(:- #,@(map compile-literal (list* head body))))]))
|
||||
|
||||
(define compile-literal
|
||||
(match-lambda
|
||||
[(literal srcloc '= (and ts (app length 2)))
|
||||
(define srcstx (datum->syntax #f 'x srcloc))
|
||||
(quasisyntax/loc srcstx
|
||||
(= #,@(map compile-term ts)))]
|
||||
[(literal srcloc pred ts)
|
||||
(define srcstx (datum->syntax #f 'x srcloc))
|
||||
(quasisyntax/loc srcstx
|
||||
(#,pred #,@(map compile-term ts)))]))
|
||||
|
||||
(define compile-term
|
||||
(match-lambda
|
||||
[(variable srcloc sym)
|
||||
(datum->syntax #f sym srcloc)]
|
||||
[(constant srcloc sym)
|
||||
(datum->syntax #f sym srcloc)]))
|
||||
17
collects/datalog/private/env.rkt
Normal file
17
collects/datalog/private/env.rkt
Normal file
|
|
@ -0,0 +1,17 @@
|
|||
#lang racket
|
||||
(require "../ast.rkt")
|
||||
|
||||
(define env/c
|
||||
(and/c hash? immutable?))
|
||||
(define (empty-env)
|
||||
(make-immutable-hash empty))
|
||||
(define (lookup env var [def #f])
|
||||
(hash-ref env var def))
|
||||
(define (extend env var val)
|
||||
(hash-set env var val))
|
||||
|
||||
(provide/contract
|
||||
[env/c contract?]
|
||||
[empty-env (-> env/c)]
|
||||
[lookup ((env/c symbol?) (term/c) . ->* . (or/c false/c term/c))]
|
||||
[extend (env/c symbol? term/c . -> . void)])
|
||||
45
collects/datalog/private/lex.rkt
Normal file
45
collects/datalog/private/lex.rkt
Normal file
|
|
@ -0,0 +1,45 @@
|
|||
#lang racket
|
||||
(require parser-tools/lex
|
||||
(prefix-in : parser-tools/lex-sre))
|
||||
|
||||
(define-tokens dtokens (VARIABLE IDENTIFIER STRING))
|
||||
(define-empty-tokens dpunct (LPAREN COMMA RPAREN TSTILE DOT EQUAL TILDE QMARK EOF))
|
||||
(define-lex-abbrev line-break #\newline)
|
||||
(define-lex-abbrev id-chars (char-complement (char-set "(,)=:.~?\"% \n")))
|
||||
(define-lex-abbrev variable-re (:: upper-case (:* (:or upper-case lower-case (char-set "0123456789_")))))
|
||||
(define-lex-abbrev identifier-re (:: id-chars (:* (:or upper-case id-chars))))
|
||||
(define-lex-abbrev comment-re (:: "%" (complement (:: any-string line-break any-string)) line-break))
|
||||
|
||||
(define get-string-token
|
||||
(lexer
|
||||
[(:~ #\" #\\) (cons (car (string->list lexeme))
|
||||
(get-string-token input-port))]
|
||||
[(:: #\\ #\\) (cons #\\ (get-string-token input-port))]
|
||||
[(:: #\\ #\newline) (cons #\newline (get-string-token input-port))]
|
||||
[(:: #\\ #\") (cons #\" (get-string-token input-port))]
|
||||
[#\" null]))
|
||||
|
||||
(define dlexer
|
||||
(lexer-src-pos
|
||||
[whitespace
|
||||
(return-without-pos (dlexer input-port))]
|
||||
[comment-re
|
||||
(return-without-pos (dlexer input-port))]
|
||||
[variable-re
|
||||
(token-VARIABLE lexeme)]
|
||||
[identifier-re
|
||||
(token-IDENTIFIER lexeme)]
|
||||
[":-" (token-TSTILE)]
|
||||
[#\" (token-STRING (list->string (get-string-token input-port)))]
|
||||
[#\( (token-LPAREN)]
|
||||
[#\, (token-COMMA)]
|
||||
[#\) (token-RPAREN)]
|
||||
[#\. (token-DOT)]
|
||||
[#\~ (token-TILDE)]
|
||||
[#\? (token-QMARK)]
|
||||
[#\= (token-EQUAL)]
|
||||
[(eof) (token-EOF)]))
|
||||
|
||||
(provide dtokens dpunct
|
||||
line-break id-chars variable-re identifier-re comment-re
|
||||
dlexer)
|
||||
20
collects/datalog/private/pprint.rkt
Normal file
20
collects/datalog/private/pprint.rkt
Normal file
|
|
@ -0,0 +1,20 @@
|
|||
#lang racket
|
||||
(provide (all-defined-out))
|
||||
|
||||
(define (text s) s)
|
||||
(define (h-append . ss) (apply string-append ss))
|
||||
(define (v-concat/s ss)
|
||||
(apply string-append ss))
|
||||
(define (v-concat ss)
|
||||
(apply string-append (add-between ss "\n")))
|
||||
(define (apply-infix d ds)
|
||||
(add-between ds d))
|
||||
(define line "\n")
|
||||
(define comma ",")
|
||||
(define space " ")
|
||||
(define lparen "(")
|
||||
(define rparen ")")
|
||||
(define dot ".")
|
||||
(define (nest n d) d)
|
||||
(define char string)
|
||||
(define doc? string?)
|
||||
75
collects/datalog/private/subst.rkt
Normal file
75
collects/datalog/private/subst.rkt
Normal file
|
|
@ -0,0 +1,75 @@
|
|||
#lang racket
|
||||
(require "../ast.rkt"
|
||||
"env.rkt")
|
||||
|
||||
(define (subst-term env t)
|
||||
(match t
|
||||
[(struct variable (_ var))
|
||||
(lookup env var t)]
|
||||
[_
|
||||
t]))
|
||||
|
||||
(define (subst-terms env ts)
|
||||
(map (curry subst-term env) ts))
|
||||
|
||||
(define (subst-literal env 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)
|
||||
(clause (clause-srcloc c)
|
||||
(subst-literal env (clause-head c))
|
||||
(map (curry subst-question env)
|
||||
(clause-body c))))
|
||||
|
||||
(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
|
||||
(foldl (lambda (e a)
|
||||
(shuffle a e))
|
||||
(shuffle (empty-env) (clause-head c))
|
||||
(clause-body c)))
|
||||
(subst-clause env c))
|
||||
|
||||
(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-question (question/c . -> . question/c)])
|
||||
59
collects/datalog/private/unify.rkt
Normal file
59
collects/datalog/private/unify.rkt
Normal file
|
|
@ -0,0 +1,59 @@
|
|||
#lang racket
|
||||
(require "../ast.rkt"
|
||||
"env.rkt")
|
||||
|
||||
(define (chase env t)
|
||||
(match t
|
||||
[(struct variable (_ var))
|
||||
(cond
|
||||
[(lookup env var)
|
||||
=> (lambda (term) (chase env term))]
|
||||
[else t])]
|
||||
[_ t]))
|
||||
|
||||
(define (unify-term env t1 t2)
|
||||
(define t1-p (chase env t1))
|
||||
(define t2-p (chase env t2))
|
||||
(if (term-equal? t1-p t2-p)
|
||||
env
|
||||
(match t1-p
|
||||
[(struct variable (_ var))
|
||||
(extend env var t2-p)]
|
||||
[_
|
||||
(match t2-p
|
||||
[(struct variable (_ var))
|
||||
(extend env var t1-p)]
|
||||
[_
|
||||
#f])])))
|
||||
|
||||
(define (unify-terms env ts1 ts2)
|
||||
(if (empty? ts1)
|
||||
(if (empty? ts2)
|
||||
env
|
||||
#f)
|
||||
(if (empty? ts2)
|
||||
#f
|
||||
(match (unify-term env (first ts1) (first ts2))
|
||||
[#f #f]
|
||||
[env (unify-terms env (rest ts1) (rest ts2))]))))
|
||||
|
||||
(define (unify l1 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 (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))])
|
||||
105
collects/datalog/private/variant.rkt
Normal file
105
collects/datalog/private/variant.rkt
Normal file
|
|
@ -0,0 +1,105 @@
|
|||
#lang racket
|
||||
(require "../ast.rkt"
|
||||
"env.rkt")
|
||||
|
||||
; Variants
|
||||
(define (variant-terms env1 env2 ts1 ts2)
|
||||
(if (empty? ts1)
|
||||
(empty? ts2)
|
||||
(and (not (empty? ts2))
|
||||
(variant-term
|
||||
env1 env2
|
||||
(first ts1) (first ts2)
|
||||
(rest ts1) (rest ts2)))))
|
||||
|
||||
(define (variant-term env1 env2 t1 t2 ts1 ts2)
|
||||
(or (and (variable? t1) (variable? t2)
|
||||
(variant-var
|
||||
env1 env2
|
||||
(variable-sym t1) (variable-sym t2)
|
||||
ts1 ts2))
|
||||
(and (term-equal? t1 t2)
|
||||
(variant-terms env1 env2 ts1 ts2))))
|
||||
|
||||
(define (variant-var env1 env2 v1 v2 ts1 ts2)
|
||||
(match (cons (lookup env1 v1) (lookup env2 v2))
|
||||
[(list-rest #f #f)
|
||||
(variant-terms
|
||||
(extend env1 v1 (make-variable #f v2))
|
||||
(extend env2 v2 (make-variable #f v1))
|
||||
ts1 ts2)]
|
||||
[(list (struct variable (_ v1-p)) (struct variable (_ v2-p)))
|
||||
(and (datum-equal? v1-p v2)
|
||||
(datum-equal? v2-p v1)
|
||||
(variant-terms env1 env2 ts1 ts2))]
|
||||
[_ #f]))
|
||||
|
||||
(define (variant? l1 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))
|
||||
|
||||
; Literal Tables modulo variant?
|
||||
(define (term-hash t recur-hash)
|
||||
(cond
|
||||
[(variable? t)
|
||||
101]
|
||||
[(constant? t)
|
||||
(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 terms])
|
||||
(if (empty? terms)
|
||||
code
|
||||
(loop (+ code (term-hash (first terms) recur-hash) (* i -7))
|
||||
(add1 i)
|
||||
(rest terms)))))
|
||||
|
||||
(define literal-tbl/c
|
||||
(coerce-contract 'variant dict?))
|
||||
(define (make-literal-tbl)
|
||||
(make-custom-hash
|
||||
variant?
|
||||
(mk-literal-hash equal-hash-code)
|
||||
(mk-literal-hash equal-secondary-hash-code)))
|
||||
(define (literal-tbl-find ltbl s)
|
||||
(dict-ref ltbl s #f))
|
||||
(define (literal-tbl-replace! ltbl s x)
|
||||
(dict-set! ltbl s x))
|
||||
|
||||
(provide/contract
|
||||
[literal-tbl/c contract?]
|
||||
[make-literal-tbl (-> literal-tbl/c)]
|
||||
[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?)])
|
||||
144
collects/datalog/runtime.rkt
Normal file
144
collects/datalog/runtime.rkt
Normal file
|
|
@ -0,0 +1,144 @@
|
|||
#lang racket
|
||||
(require "ast.rkt"
|
||||
"private/env.rkt"
|
||||
"private/subst.rkt"
|
||||
"private/unify.rkt"
|
||||
"private/variant.rkt")
|
||||
|
||||
; A clause is safe if every variable in its head occurs in some literal in its body.
|
||||
(define (safe-clause? c)
|
||||
(define head-vars (filter variable? (literal-terms (clause-head c))))
|
||||
(andmap (lambda (v)
|
||||
(ormap (lambda (l)
|
||||
(ormap (lambda (t) (term-equal? t v))
|
||||
(cond
|
||||
[(literal? l)
|
||||
(literal-terms l)]
|
||||
[(external? l)
|
||||
(append (external-arg-terms l)
|
||||
(external-ans-terms l))])))
|
||||
(clause-body c)))
|
||||
head-vars))
|
||||
|
||||
(define theory/c (and/c hash? (not/c immutable?)))
|
||||
(define (literal-key l)
|
||||
(format "~a/~a" (literal-predicate l) (length (literal-terms l))))
|
||||
(define (clause-key c)
|
||||
(literal-key (clause-head c)))
|
||||
|
||||
(define (make-theory)
|
||||
(make-hash))
|
||||
|
||||
(define ((mk-assume hash-update) thy c)
|
||||
(hash-update
|
||||
thy (clause-key c)
|
||||
(lambda (clauses)
|
||||
(list* c clauses))
|
||||
empty))
|
||||
(define ((mk-retract hash-update) thy rc)
|
||||
(hash-update
|
||||
thy (clause-key rc)
|
||||
(lambda (clauses)
|
||||
(filter (lambda (c)
|
||||
(not (clause-equal? c rc)))
|
||||
clauses))
|
||||
empty))
|
||||
|
||||
(define assume (mk-assume hash-update))
|
||||
(define retract (mk-retract hash-update))
|
||||
(define assume! (mk-assume hash-update!))
|
||||
(define retract! (mk-retract hash-update!))
|
||||
|
||||
(define (get thy lit)
|
||||
(hash-ref thy (literal-key lit) empty))
|
||||
|
||||
(define-struct subgoal
|
||||
(question
|
||||
[facts #:mutable]
|
||||
[waiters #:mutable]))
|
||||
|
||||
(define (resolve c q)
|
||||
(define body (clause-body c))
|
||||
(and (not (empty? body))
|
||||
(cond
|
||||
[(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 q)
|
||||
(define subgoals (make-literal-tbl))
|
||||
(define (fact! sg lit)
|
||||
(unless (mem-literal lit (subgoal-facts sg))
|
||||
(set-subgoal-facts! sg (list* lit (subgoal-facts sg)))
|
||||
(for-each (lambda (w)
|
||||
(cond
|
||||
[(resolve (cdr w) lit)
|
||||
=> (lambda (cs-p) (add-clause! (car w) cs-p))]))
|
||||
(subgoal-waiters sg))))
|
||||
(define (rule! sg1 c s)
|
||||
(define sg2 (literal-tbl-find subgoals s))
|
||||
(if sg2
|
||||
(begin
|
||||
(set-subgoal-waiters! sg2 (list* (cons sg1 c) (subgoal-waiters sg2)))
|
||||
(for-each (lambda (fact)
|
||||
(cond
|
||||
[(resolve c fact)
|
||||
=> (lambda (cs) (add-clause! sg1 cs))]))
|
||||
(subgoal-facts sg2)))
|
||||
(let ([sg2 (make-subgoal s empty (list (cons sg1 c)))])
|
||||
(literal-tbl-replace! subgoals s sg2)
|
||||
(search! sg2))))
|
||||
(define (add-clause! sg c)
|
||||
(match c
|
||||
[(struct clause (_ lit (list)))
|
||||
(fact! sg lit)]
|
||||
[(struct clause (_ _ (list-rest selected _)))
|
||||
(rule! sg c selected)]))
|
||||
(define (search-theory! sg)
|
||||
(for-each
|
||||
(lambda (clause)
|
||||
(define renamed (rename-clause clause))
|
||||
(define selected (clause-head renamed))
|
||||
(cond
|
||||
[(unify (subgoal-question sg) selected)
|
||||
=> (lambda (env)
|
||||
(add-clause! sg (subst-clause env renamed)))]))
|
||||
(get thy (subgoal-question sg))))
|
||||
(define (search! 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)
|
||||
(fact! sg (make-literal srcloc '= (list a b)))))
|
||||
(cond
|
||||
[(unify-term (empty-env) a b)
|
||||
=> (lambda (env) (equal-test (subst-term env a) (subst-term env b)))]
|
||||
[else (equal-test a b)])]
|
||||
[_
|
||||
(search-theory! sg)]))
|
||||
(define sg (make-subgoal q empty empty))
|
||||
(literal-tbl-replace! subgoals q sg)
|
||||
(search! sg)
|
||||
(subgoal-facts sg))
|
||||
|
||||
(provide/contract
|
||||
[safe-clause? (clause? . -> . boolean?)]
|
||||
[theory/c contract?]
|
||||
[make-theory (-> theory/c)]
|
||||
[assume! (theory/c safe-clause? . -> . void)]
|
||||
[retract! (theory/c clause? . -> . void)]
|
||||
[prove (theory/c question/c . -> . (listof question/c))])
|
||||
178
collects/datalog/scribblings/datalog.scrbl
Normal file
178
collects/datalog/scribblings/datalog.scrbl
Normal file
|
|
@ -0,0 +1,178 @@
|
|||
#lang scribble/doc
|
||||
@(require scribble/manual
|
||||
scribble/eval
|
||||
scribble/basic
|
||||
scribble/bnf
|
||||
"utils.rkt")
|
||||
|
||||
@title[#:tag "top"]{@bold{Datalog}: Deductive database programming}
|
||||
@author[(author+email "Jay McCarthy" "jay@racket-lang.org")]
|
||||
|
||||
@link["http://en.wikipedia.org/wiki/Datalog"]{Datalog} is
|
||||
@itemize[
|
||||
@item{a declarative logic language in which each
|
||||
formula is a function-free Horn clause, and every variable
|
||||
in the head of a clause must appear in the body of the clause.}
|
||||
@item{a lightweight deductive database system where queries and database updates are expressed
|
||||
in the logic language.}
|
||||
]
|
||||
|
||||
The use of Datalog syntax and an implementation based
|
||||
on tabling intermediate results ensures that all queries terminate.
|
||||
|
||||
@table-of-contents[]
|
||||
|
||||
@section[#:tag "datalog"]{Datalog Module Language}
|
||||
|
||||
@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.
|
||||
Comments do not occur inside strings.
|
||||
|
||||
A variable is a sequence of Unicode "Uppercase" and "Lowercase" letters, digits, and the underscore character. A variable must begin with a Unicode "Uppercase" letter.
|
||||
|
||||
An identifier is a sequence of printing characters that does not contain any of the following characters: @litchar["("], @litchar["`"],
|
||||
@litchar["'"], @litchar[")"], @litchar["="], @litchar[":"], @litchar["."], @litchar["~"], @litchar["?"], @litchar["\""], @litchar["%"], and space.
|
||||
An identifier must not begin with a Latin capital letter. Note that the characters that start punctuation are forbidden in identifiers,
|
||||
but the hyphen character is allowed.
|
||||
|
||||
A string is a sequence of characters enclosed in double quotes. Characters other than double quote, newline, and backslash may be directly
|
||||
included in a string. The remaining characters may be specified using escape characters, @litchar["\\\""], @litchar["\\\n"], and
|
||||
@litchar["\\\\"] respectively.
|
||||
|
||||
A literal, is a predicate symbol followed by an optional parenthesized list of comma separated terms. A predicate symbol is either an identifier
|
||||
or a string. A term is either a variable or a constant. As with predicate symbols, a constant is either an identifier or a string. As a special case,
|
||||
two terms separated by @litchar["="] is a literal for the equality predicate.
|
||||
The following are literals:
|
||||
@verbatim[#:indent 4 #<<END
|
||||
parent(john, douglas)
|
||||
zero-arity-literal
|
||||
"="(3,3)
|
||||
""(-0-0-0,&&&,***,"\00")
|
||||
END
|
||||
]
|
||||
|
||||
A clause is a head literal followed by an optional body. A body is a comma separated list of literals. A clause without a body is called a @deftech{fact},
|
||||
and a rule when it has one. The punctuation @litchar[":-"] separates the head of a rule from its body. A clause is safe if every variable in its head
|
||||
occurs in some literal in its body. The following are safe clauses:
|
||||
|
||||
@verbatim[#:indent 4 #<<END
|
||||
parent(john, douglas)
|
||||
ancestor(A, B) :-
|
||||
parent(A, B)
|
||||
ancestor(A, B) :-
|
||||
parent(A, C),
|
||||
ancestor(C, B)
|
||||
END
|
||||
]
|
||||
|
||||
A program is a sequence of zero or more statements. A statement is an assertion, a retraction, or a query. An assertion is a clause followed by
|
||||
a period, and it adds the clause to the database if it is safe. A retraction is a clause followed by a tilde, and it removes the clause from
|
||||
the database. A query is a literal followed by a question mark.
|
||||
|
||||
The following BNF describes the syntax of Datalog.
|
||||
|
||||
@BNF[
|
||||
(list (nonterm "program")
|
||||
(kleenestar (nonterm "statement")))
|
||||
(list (nonterm "statement")
|
||||
(nonterm "assertion")
|
||||
(nonterm "retraction")
|
||||
(nonterm "query"))
|
||||
(list (nonterm "assertion")
|
||||
(BNF-seq (nonterm "clause") (litchar ".")))
|
||||
(list (nonterm "retraction")
|
||||
(BNF-seq (nonterm "clause") (litchar "~")))
|
||||
(list (nonterm "query")
|
||||
(BNF-seq (nonterm "literal") (litchar "?")))
|
||||
(list (nonterm "clause")
|
||||
(BNF-seq (nonterm "literal") (litchar ":-") (nonterm "body"))
|
||||
(nonterm "literal"))
|
||||
(list (nonterm "body")
|
||||
(BNF-seq (nonterm "literal") (litchar ",") (nonterm "body"))
|
||||
(nonterm "literal"))
|
||||
(list (nonterm "literal")
|
||||
(BNF-seq (nonterm "predicate-sym") (litchar "(") (litchar ")"))
|
||||
(BNF-seq (nonterm "predicate-sym") (litchar "(") (nonterm "terms") (litchar ")"))
|
||||
(nonterm "predicate-sym")
|
||||
(BNF-seq (nonterm "term") (litchar "=") (nonterm "term")))
|
||||
(list (nonterm "predicate-sym")
|
||||
(nonterm "IDENTIFIER")
|
||||
(nonterm "STRING"))
|
||||
(list (nonterm "terms")
|
||||
(nonterm "term")
|
||||
(BNF-seq (nonterm "term") (litchar ",") (nonterm "terms")))
|
||||
(list (nonterm "term")
|
||||
(nonterm "VARIABLE")
|
||||
(nonterm "constant"))
|
||||
(list (nonterm "constant")
|
||||
(nonterm "IDENTIFIER")
|
||||
(nonterm "STRING"))
|
||||
]
|
||||
|
||||
The effect of running a Datalog program is to modify the database as directed
|
||||
by its statements, and then to return the literals designated by the query.
|
||||
The modified database is provided as @racket[theory].
|
||||
|
||||
The following is a program:
|
||||
|
||||
@verbatim[#:indent 4 #<<END
|
||||
#lang datalog
|
||||
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)?
|
||||
END
|
||||
]
|
||||
|
||||
The Datalog REPL accepts new statements that are executed as if they were in the original program text.
|
||||
|
||||
@include-section["tutorial.scrbl"]
|
||||
|
||||
@section{Parenthetical Datalog Module Language}
|
||||
@(require (for-label datalog
|
||||
racket))
|
||||
|
||||
@defmodulelang[datalog/sexp]
|
||||
|
||||
The semantics of this language is the same as the normal Datalog language, except it uses the parenthetical syntax described in @secref{interop}.
|
||||
|
||||
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
|
||||
|
||||
(! (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))]
|
||||
|
||||
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"]
|
||||
|
||||
@section{Acknowledgments}
|
||||
|
||||
This package was once structurally based on Dave Herman's @racketmodname[(planet dherman/javascript)] library and
|
||||
John Ramsdell's @link["http://www.ccs.neu.edu/home/ramsdell/tools/datalog/datalog.html"]{Datalog library}.
|
||||
|
||||
The package uses the tabled logic programming algorithm described in
|
||||
@link["http://scholar.google.com/scholar?q=author:%22Chen%22+intitle:%22Efficient+top-down+computation+of+queries+under+the+...%22+&oi=scholarr"]{Efficient Top-Down Computation of Queries under the Well-Founded Semantics} by W. Chen, T. Swift, and D. S. Warren.
|
||||
Another important reference is
|
||||
@link["http://portal.acm.org/citation.cfm?id=227597"]{Tabled Evaluation with Delaying for General Logic Programs} by W. Chen and D. S. Warren.
|
||||
Datalog is described in
|
||||
@link["http://doi.ieeecomputersociety.org/10.1109/69.43410"]{What You Always Wanted to Know About Datalog (And Never Dared to Ask)}
|
||||
by Stefano Ceri, Georg Gottlob, and Letizia Tanca.
|
||||
86
collects/datalog/scribblings/racket.scrbl
Normal file
86
collects/datalog/scribblings/racket.scrbl
Normal file
|
|
@ -0,0 +1,86 @@
|
|||
#lang scribble/doc
|
||||
@(require scribble/manual
|
||||
scribble/eval
|
||||
scribble/basic
|
||||
scribble/bnf
|
||||
(for-label racket/base
|
||||
racket/contract
|
||||
"../main.rkt")
|
||||
"utils.rkt")
|
||||
|
||||
@title[#:tag "interop"]{Racket Interoperability}
|
||||
|
||||
@defmodule[datalog]
|
||||
|
||||
The Datalog database can be directly used by Racket programs through this API.
|
||||
|
||||
@examples[#:eval the-eval
|
||||
(define family (make-theory))
|
||||
|
||||
(datalog family
|
||||
(! (parent joseph2 joseph1))
|
||||
(! (parent joseph2 lucy))
|
||||
(! (parent joseph3 joseph2)))
|
||||
|
||||
(datalog family
|
||||
(? (parent X joseph2)))
|
||||
|
||||
(datalog family
|
||||
(? (parent joseph2 X)))
|
||||
|
||||
(datalog family
|
||||
(? (parent joseph2 X))
|
||||
(? (parent X joseph2)))
|
||||
|
||||
(datalog family
|
||||
(! (:- (ancestor A B)
|
||||
(parent A B)))
|
||||
(! (:- (ancestor A B)
|
||||
(parent A C)
|
||||
(= D C)
|
||||
(ancestor D B))))
|
||||
|
||||
(datalog family
|
||||
(? (ancestor A B)))
|
||||
|
||||
(let ([x 'joseph2])
|
||||
(datalog family
|
||||
(? (parent x X))))
|
||||
|
||||
(datalog family
|
||||
(? (add1 1 :- X)))]
|
||||
|
||||
@defthing[theory/c contract?]{ A contract for Datalog theories. }
|
||||
|
||||
@defproc[(make-theory) theory/c]{ Creates a theory for use with @racket[datalog]. }
|
||||
|
||||
@defform[(datalog thy-expr
|
||||
stmt ...)
|
||||
#:contracts ([thy-expr theory/c])]{ Executes the statements on the theory given by @racket[thy-expr]. Returns the answers to the final query as a list of substitution dictionaries or returns @racket[empty]. }
|
||||
|
||||
@defform[(datalog! thy-expr
|
||||
stmt ...)
|
||||
#:contracts ([thy-expr 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)]. }
|
||||
|
||||
Statements are either assertions, retractions, or queries.
|
||||
|
||||
@defform[(! clause)]{ Asserts the clause. }
|
||||
@defform[(~ clause)]{ Retracts the literal. }
|
||||
|
||||
@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 ...)].
|
||||
External queries 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.
|
||||
|
||||
External queries invalidate Datalog's guaranteed termination. For example, this program does not terminate:
|
||||
@racketblock[
|
||||
(datalog (make-theory)
|
||||
(! (:- (loop X)
|
||||
(add1 X :- Z)
|
||||
(loop Z)))
|
||||
(? (loop 1)))
|
||||
]
|
||||
108
collects/datalog/scribblings/tutorial.scrbl
Normal file
108
collects/datalog/scribblings/tutorial.scrbl
Normal file
|
|
@ -0,0 +1,108 @@
|
|||
#lang scribble/doc
|
||||
@(require scribble/manual
|
||||
scribble/eval
|
||||
scribble/basic
|
||||
scribble/bnf
|
||||
(for-label racket/base
|
||||
racket/contract
|
||||
"../main.rkt")
|
||||
"utils.rkt")
|
||||
|
||||
@title{Tutorial}
|
||||
|
||||
Start DrRacket and type
|
||||
|
||||
@racketmod[datalog]
|
||||
|
||||
in the Definitions window. Click @onscreen{Run}, then click in the REPL.
|
||||
|
||||
@racketinput[]
|
||||
|
||||
@tech{Facts} are stored in tables. If the name of the table is @litchar["parent"], and
|
||||
@litchar["john"] is the parent of @litchar["douglas"], store the fact in the database with
|
||||
this:
|
||||
|
||||
@racketinput[#,(tt "parent(john, douglas).")]
|
||||
|
||||
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.
|
||||
|
||||
A query can be used to see if a particular row is in a table. Type this to see if @litchar["john"]
|
||||
is the parent of @litchar["douglas"]:
|
||||
|
||||
@racketinput[#,(tt "parent(john, douglas)?")]
|
||||
@racketblock[#,(racketresultfont (tt "parent(john, douglas)."))]
|
||||
|
||||
Type this to see if @litchar["john"] is the parent of @litchar["ebbon"]:
|
||||
|
||||
@racketinput[#,(tt "parent(john, ebbon)?")]
|
||||
|
||||
The query produced no results because @litchar["john"] is not the parent of @litchar["ebbon"]. Let's add more rows.
|
||||
|
||||
@racketinput[#,(tt "parent(bob, john).")]
|
||||
@racketinput[#,(tt "parent(ebbon, bob).")]
|
||||
|
||||
Type the following to list all rows in the @litchar["parent"] table:
|
||||
|
||||
@racketinput[#,(tt "parent(A, B)?")]
|
||||
@racketblock[#,(racketresultfont (tt "parent(john, douglas)."))]
|
||||
@racketblock[#,(racketresultfont (tt "parent(bob, john)."))]
|
||||
@racketblock[#,(racketresultfont (tt "parent(ebbon, bob)."))]
|
||||
|
||||
Type the following to list all the children of @litchar["john"]:
|
||||
|
||||
@racketinput[#,(tt "parent(john, B)?")]
|
||||
@racketblock[#,(racketresultfont (tt "parent(john, douglas)."))]
|
||||
|
||||
A term that begins with a capital letter is a logical variable.When producing a set of answers, the
|
||||
Datalog interpreter lists all rows that match the query when each variable in the query is substituted
|
||||
for a constant. The following example produces no answers, as there are no substitutions for the variable
|
||||
@litchar["A"] that produce a fact in the database. This is because no one is the parent of oneself.
|
||||
|
||||
@racketinput[#,(tt "parent(A, A)?")]
|
||||
|
||||
A deductive database can use rules of inference to derive new facts. Consider the following rule:
|
||||
|
||||
@racketinput[#,(tt "ancestor(A, B) :- parent(A, B).")]
|
||||
|
||||
The rule says that if A is the parent of B, then A is an ancestor of B.
|
||||
The other rule defining an ancestor says that if A is the parent of C,
|
||||
C is an ancestor of B, then A is an ancestor of B.
|
||||
|
||||
@racketinput[#,(tt "ancestor(A, B) :-")
|
||||
#,(tt " parent(A, C),")
|
||||
#,(tt " ancestor(C, B).")]
|
||||
|
||||
In the interpreter, DrRacket knows that the clause is not complete, so by pressing Return, it doesn't interpret the line.
|
||||
|
||||
Rules are used to answer queries just as is done for facts.
|
||||
|
||||
@racketinput[#,(tt "ancestor(A, B)?")]
|
||||
@racketblock[#,(racketresultfont (tt "ancestor(ebbon, bob)."))]
|
||||
@racketblock[#,(racketresultfont (tt "ancestor(bob, john)."))]
|
||||
@racketblock[#,(racketresultfont (tt "ancestor(john, douglas)."))]
|
||||
@racketblock[#,(racketresultfont (tt "ancestor(bob, douglas)."))]
|
||||
@racketblock[#,(racketresultfont (tt "ancestor(ebbon, john)."))]
|
||||
@racketblock[#,(racketresultfont (tt "ancestor(ebbon, douglas)."))]
|
||||
@racketinput[#,(tt "ancestor(X,john)?")]
|
||||
@racketblock[#,(racketresultfont (tt "ancestor(bob, john)."))]
|
||||
@racketblock[#,(racketresultfont (tt "ancestor(ebbon, john)."))]
|
||||
|
||||
A fact or a rule can be retracted from the database using tilde syntax:
|
||||
|
||||
@racketinput[#,(tt "parent(bob, john)~")]
|
||||
@racketinput[#,(tt "parent(A, B)?")]
|
||||
@racketblock[#,(racketresultfont (tt "parent(john, douglas)."))]
|
||||
@racketblock[#,(racketresultfont (tt "parent(ebbon, bob)."))]
|
||||
@racketinput[#,(tt "ancestor(A, B)?")]
|
||||
@racketblock[#,(racketresultfont (tt "ancestor(ebbon, bob)."))]
|
||||
@racketblock[#,(racketresultfont (tt "ancestor(john, douglas)."))]
|
||||
|
||||
Unlike Prolog, the order in which clauses are asserted is irrelevant. All queries terminate, and every possible answer is derived.
|
||||
|
||||
@racketinput[#,(tt "q(X) :- p(X).")]
|
||||
@racketinput[#,(tt "q(a).")]
|
||||
@racketinput[#,(tt "p(X) :- q(X).")]
|
||||
@racketinput[#,(tt "q(X)?")]
|
||||
@racketblock[#,(racketresultfont (tt "q(a)."))]
|
||||
10
collects/datalog/scribblings/utils.rkt
Normal file
10
collects/datalog/scribblings/utils.rkt
Normal file
|
|
@ -0,0 +1,10 @@
|
|||
#lang racket/base
|
||||
|
||||
(require scribble/eval)
|
||||
|
||||
(provide the-eval)
|
||||
|
||||
(define the-eval
|
||||
(let ([the-eval (make-base-eval)])
|
||||
(the-eval `(require datalog))
|
||||
the-eval))
|
||||
50
collects/datalog/sexp/lang.rkt
Normal file
50
collects/datalog/sexp/lang.rkt
Normal file
|
|
@ -0,0 +1,50 @@
|
|||
#lang racket/base
|
||||
(require (for-syntax syntax/parse
|
||||
racket/list
|
||||
racket/base)
|
||||
racket/contract
|
||||
datalog/stx
|
||||
datalog/runtime)
|
||||
|
||||
(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 ([theory (datum->syntax #'es 'theory)]
|
||||
[((requires ...)
|
||||
(stmt ...))
|
||||
(partition-requires #'es)])
|
||||
(syntax/loc stx
|
||||
(#%module-begin
|
||||
requires ...
|
||||
(define theory (make-theory))
|
||||
(datalog! theory stmt ...)
|
||||
(provide/contract
|
||||
[theory theory/c]))))]))
|
||||
|
||||
(define-syntax (top-interaction stx)
|
||||
(syntax-case stx ()
|
||||
[(_ . stmt)
|
||||
(with-syntax ([theory (datum->syntax #'stmt 'theory)])
|
||||
(syntax/loc stx
|
||||
(datalog! theory stmt)))]))
|
||||
|
||||
(provide (rename-out [top-interaction #%top-interaction]
|
||||
[module-begin #%module-begin])
|
||||
(except-out (all-from-out racket/base)
|
||||
#%top-interaction
|
||||
#%module-begin)
|
||||
! ~ ? :-)
|
||||
2
collects/datalog/sexp/lang/reader.rkt
Normal file
2
collects/datalog/sexp/lang/reader.rkt
Normal file
|
|
@ -0,0 +1,2 @@
|
|||
(module reader syntax/module-reader
|
||||
#:language 'datalog/sexp/lang)
|
||||
190
collects/datalog/stx.rkt
Normal file
190
collects/datalog/stx.rkt
Normal file
|
|
@ -0,0 +1,190 @@
|
|||
#lang racket
|
||||
(require (for-syntax syntax/parse
|
||||
racket/local
|
||||
racket/function
|
||||
racket/list)
|
||||
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 (->substitutions sel ls)
|
||||
(if (void? ls) empty
|
||||
(map sel ls)))
|
||||
|
||||
(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))]))
|
||||
|
||||
(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])
|
||||
(->substitutions
|
||||
(datalog-stmt-var-selector stmt)
|
||||
(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 (! ~ ?)
|
||||
[(_ (~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-stmt-var-selector stx)
|
||||
(syntax-parse
|
||||
stx
|
||||
#:literals (! ~ ?)
|
||||
[(_ (~and tstx (! c)))
|
||||
(quasisyntax/loc #'tstx (λ (l) (hasheq)))]
|
||||
[(_ (~and tstx (~ c)))
|
||||
(quasisyntax/loc #'tstx (λ (l) (hasheq)))]
|
||||
[(_ (~and tstx (? l)))
|
||||
(quasisyntax/loc #'tstx (datalog-literal-var-selector l))]))
|
||||
|
||||
(define-syntax (datalog-clause stx)
|
||||
(syntax-parse
|
||||
stx
|
||||
#:literals (:-)
|
||||
[(_ (~and tstx (:- head body ...)))
|
||||
(local [(define (datalog-literal-variables stx)
|
||||
(syntax-parse
|
||||
stx
|
||||
#:literals (:-)
|
||||
[sym:id
|
||||
empty]
|
||||
[(~and tstx (sym:id arg ... :- ans ...))
|
||||
(append-map datalog-term-variables
|
||||
(syntax->list #'(arg ... ans ...)))]
|
||||
[(~and tstx (sym:id e ...))
|
||||
(append-map datalog-term-variables
|
||||
(syntax->list #'(e ...)))]))
|
||||
(define (datalog-term-variables stx)
|
||||
(syntax-parse
|
||||
stx
|
||||
[sym:id
|
||||
(list #'sym)]
|
||||
[sym:expr
|
||||
empty]))
|
||||
(define head-vars (datalog-literal-variables #'head))
|
||||
(define body-vars
|
||||
(append-map datalog-literal-variables (syntax->list #'(body ...))))
|
||||
(define body-vars-in-head
|
||||
(filter
|
||||
(λ (bv)
|
||||
(findf (curry bound-identifier=? bv)
|
||||
head-vars))
|
||||
body-vars))
|
||||
(define fake-lam
|
||||
(quasisyntax/loc #'tstx
|
||||
(lambda #,head-vars
|
||||
(void #,@body-vars-in-head))))]
|
||||
(syntax-local-lift-expression
|
||||
fake-lam))
|
||||
(quasisyntax/loc #'tstx
|
||||
(clause #'#,#'tstx (datalog-literal head)
|
||||
(list (datalog-literal body) ...)))]
|
||||
[(_ e)
|
||||
(quasisyntax/loc #'e
|
||||
(clause #'#,#'e (datalog-literal e) empty))]))
|
||||
|
||||
(define-syntax (datalog-literal stx)
|
||||
(syntax-parse
|
||||
stx
|
||||
#:literals (:-)
|
||||
[(_ sym:id)
|
||||
(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-literal-var-selector stx)
|
||||
(syntax-parse
|
||||
stx
|
||||
#:literals (:-)
|
||||
[(_ sym:id)
|
||||
(quasisyntax/loc #'sym (λ (l) (hasheq)))]
|
||||
[(_ (~and tstx (sym:id arg ... :- ans ...)))
|
||||
(quasisyntax/loc #'tstx
|
||||
(match-lambda
|
||||
[(external _srcloc _predsym _pred args anss)
|
||||
(terms->hasheq (list (datalog-term arg) ...
|
||||
(datalog-term ans) ...)
|
||||
(append args anss))]))]
|
||||
[(_ (~and tstx (sym:id e ...)))
|
||||
(quasisyntax/loc #'tstx
|
||||
(match-lambda
|
||||
[(literal _srcloc _predsym ts)
|
||||
(terms->hasheq (list (datalog-term e) ...)
|
||||
ts)]))]))
|
||||
|
||||
(define (terms->hasheq src-ts res-ts)
|
||||
(for/fold ([h (hasheq)])
|
||||
([src (in-list src-ts)]
|
||||
[res (in-list res-ts)])
|
||||
(if (variable? src)
|
||||
(hash-set h (variable-sym src) (constant-value res))
|
||||
h)))
|
||||
|
||||
(define-syntax (datalog-term stx)
|
||||
(syntax-parse
|
||||
stx
|
||||
[(_ sym:id)
|
||||
(cond
|
||||
[(identifier-binding #'sym 0)
|
||||
(quasisyntax/loc #'sym
|
||||
(constant #'#,#'sym sym))]
|
||||
[(char-upper-case? (string-ref (symbol->string (syntax->datum #'sym)) 0))
|
||||
(quasisyntax/loc #'sym
|
||||
(variable #'#,#'sym 'sym))]
|
||||
[else
|
||||
(quasisyntax/loc #'sym
|
||||
(constant #'#,#'sym 'sym))])]
|
||||
[(_ sym:expr)
|
||||
(quasisyntax/loc #'sym
|
||||
(constant #'#,#'sym sym))]))
|
||||
|
||||
(provide datalog datalog!
|
||||
:- ! ~ ?)
|
||||
BIN
collects/datalog/tool/datalog.png
Normal file
BIN
collects/datalog/tool/datalog.png
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 2.1 KiB |
54
collects/datalog/tool/submit.rkt
Normal file
54
collects/datalog/tool/submit.rkt
Normal file
|
|
@ -0,0 +1,54 @@
|
|||
#lang racket/base
|
||||
|
||||
(define (delimiter-pair? x y)
|
||||
(and (char=? x #\() (char=? y #\))))
|
||||
|
||||
(define (repl-submit? ip has-white-space?)
|
||||
(let loop ([blank? #t]
|
||||
[string-char #f]
|
||||
[delimiter-stack null]
|
||||
[closed? #f])
|
||||
(let ([c (read-char ip)])
|
||||
(if (eof-object? c)
|
||||
(and closed?
|
||||
(not blank?)
|
||||
(not string-char)
|
||||
(null? delimiter-stack))
|
||||
(case c
|
||||
[(#\. #\? #\~)
|
||||
(if string-char
|
||||
(loop #f string-char delimiter-stack #f)
|
||||
(loop #f #f delimiter-stack #t))]
|
||||
[(#\()
|
||||
(if string-char
|
||||
(loop #f string-char delimiter-stack #f)
|
||||
(loop #f #f (cons c delimiter-stack) #f))]
|
||||
[(#\))
|
||||
(cond
|
||||
[string-char
|
||||
(loop #f string-char delimiter-stack #f)]
|
||||
[(and (pair? delimiter-stack)
|
||||
(delimiter-pair? (car delimiter-stack) c))
|
||||
(loop #f #f (cdr delimiter-stack) #f)]
|
||||
[else
|
||||
(loop #f #f delimiter-stack #f)])]
|
||||
[(#\")
|
||||
(cond
|
||||
[(and string-char (char=? c string-char))
|
||||
(loop #f #f delimiter-stack #f)]
|
||||
[string-char
|
||||
(loop #f string-char delimiter-stack #f)]
|
||||
[else
|
||||
(loop #f c delimiter-stack #f)])]
|
||||
[(#\\)
|
||||
(if string-char
|
||||
(begin (read-char ip)
|
||||
(loop #f string-char delimiter-stack #f))
|
||||
(loop #f string-char delimiter-stack #f))]
|
||||
[else
|
||||
(loop (and blank? (char-whitespace? c))
|
||||
string-char
|
||||
delimiter-stack
|
||||
closed?)])))))
|
||||
|
||||
(provide repl-submit?)
|
||||
36
collects/datalog/tool/syntax-color.rkt
Normal file
36
collects/datalog/tool/syntax-color.rkt
Normal file
|
|
@ -0,0 +1,36 @@
|
|||
#lang racket/base
|
||||
(require parser-tools/lex
|
||||
(prefix-in : parser-tools/lex-sre)
|
||||
"../private/lex.rkt")
|
||||
|
||||
(provide get-syntax-token)
|
||||
|
||||
(define (syn-val lex a b c d)
|
||||
(values lex a b (position-offset c) (position-offset d)))
|
||||
|
||||
(define (colorize-string my-start-pos)
|
||||
(define lxr
|
||||
(lexer
|
||||
[(:~ #\" #\\) (lxr input-port)]
|
||||
[(:: #\\ #\\) (lxr input-port)]
|
||||
[(:: #\\ #\newline) (lxr input-port)]
|
||||
[(:: #\\ #\") (lxr input-port)]
|
||||
[(eof) (syn-val "" 'error #f my-start-pos end-pos)]
|
||||
[#\" (syn-val "" 'string #f my-start-pos end-pos)]))
|
||||
lxr)
|
||||
|
||||
(define get-syntax-token
|
||||
(lexer
|
||||
[(:+ whitespace)
|
||||
(syn-val lexeme 'whitespace #f start-pos end-pos)]
|
||||
[comment-re
|
||||
(syn-val lexeme 'comment #f start-pos end-pos)]
|
||||
[variable-re
|
||||
(syn-val lexeme 'symbol #f start-pos end-pos)]
|
||||
[identifier-re
|
||||
(syn-val lexeme 'identifier #f start-pos end-pos)]
|
||||
[(:or #\) #\() (syn-val lexeme 'parenthesis #f start-pos end-pos)]
|
||||
[(:or #\= #\? #\~ #\. #\, ":-") (syn-val lexeme 'parenthesis #f start-pos end-pos)]
|
||||
[(eof) (syn-val lexeme 'eof #f start-pos end-pos)]
|
||||
[#\" ((colorize-string start-pos) input-port)]
|
||||
[any-char (syn-val lexeme 'error #f start-pos end-pos)]))
|
||||
80
collects/tests/datalog/ast.rkt
Normal file
80
collects/tests/datalog/ast.rkt
Normal file
|
|
@ -0,0 +1,80 @@
|
|||
#lang racket
|
||||
(require rackunit
|
||||
datalog/ast)
|
||||
|
||||
(provide ast-tests)
|
||||
|
||||
(define ast-tests
|
||||
(test-suite
|
||||
"ast"
|
||||
|
||||
(test-suite
|
||||
"datum-equal?"
|
||||
(test-not-false "str/str" (datum-equal? "str" "str"))
|
||||
(test-false "str/str" (datum-equal? "str1" "str2"))
|
||||
(test-not-false "sym/sym" (datum-equal? 'sym1 'sym1))
|
||||
(test-false "sym/sym" (datum-equal? 'sym1 'sym2))
|
||||
(test-false "str/sym" (datum-equal? "str" 'sym))
|
||||
(test-false "sym/str" (datum-equal? 'sym "str")))
|
||||
|
||||
(test-suite
|
||||
"variable-equal?"
|
||||
(test-not-false "var/var" (variable-equal? (make-variable #f 'sym1) (make-variable #f 'sym1)))
|
||||
(test-not-false "var/var" (variable-equal? (make-variable #f 'sym1) (make-variable #'sym1 'sym1)))
|
||||
(test-false "var/var" (variable-equal? (make-variable #f 'sym1) (make-variable #f 'sym2)))
|
||||
(test-false "var/var" (variable-equal? (make-variable #f 'sym1) (make-variable #'sym2 'sym2))))
|
||||
|
||||
(test-suite
|
||||
"constant-equal?"
|
||||
(test-not-false "sym/sym" (constant-equal? (make-constant #f 'sym1) (make-constant #f 'sym1)))
|
||||
(test-not-false "sym/sym" (constant-equal? (make-constant #f 'sym1) (make-constant #'sym1 'sym1)))
|
||||
(test-false "sym/sym" (constant-equal? (make-constant #f 'sym1) (make-constant #'sym1 'sym2)))
|
||||
(test-not-false "str/str" (constant-equal? (make-constant #f "sym1") (make-constant #f "sym1")))
|
||||
(test-not-false "str/str" (constant-equal? (make-constant #f "sym1") (make-constant #'sym1 "sym1")))
|
||||
(test-false "str/str" (constant-equal? (make-constant #f "sym1") (make-constant #'sym1 "sym2")))
|
||||
(test-false "sym/str" (constant-equal? (make-constant #f 'sym1) (make-constant #'sym1 "sym2")))
|
||||
(test-false "str/sym" (constant-equal? (make-constant #'sym1 "sym2") (make-constant #f 'sym1))))
|
||||
|
||||
(test-suite
|
||||
"term-equal?"
|
||||
(test-not-false "var/var" (term-equal? (make-variable #f 'sym1) (make-variable #f 'sym1)))
|
||||
(test-not-false "var/var" (term-equal? (make-variable #f 'sym1) (make-variable #'sym1 'sym1)))
|
||||
(test-false "var/var" (term-equal? (make-variable #f 'sym1) (make-variable #f 'sym2)))
|
||||
(test-false "var/var" (term-equal? (make-variable #f 'sym1) (make-variable #'sym2 'sym2)))
|
||||
(test-not-false "sym/sym" (term-equal? (make-constant #f 'sym1) (make-constant #f 'sym1)))
|
||||
(test-not-false "sym/sym" (term-equal? (make-constant #f 'sym1) (make-constant #'sym1 'sym1)))
|
||||
(test-false "sym/sym" (term-equal? (make-constant #f 'sym1) (make-constant #'sym1 'sym2)))
|
||||
(test-not-false "str/str" (term-equal? (make-constant #f "sym1") (make-constant #f "sym1")))
|
||||
(test-not-false "str/str" (term-equal? (make-constant #f "sym1") (make-constant #'sym1 "sym1")))
|
||||
(test-false "str/str" (term-equal? (make-constant #f "sym1") (make-constant #'sym1 "sym2")))
|
||||
(test-false "sym/str" (term-equal? (make-constant #f 'sym1) (make-constant #'sym1 "sym2")))
|
||||
(test-false "str/sym" (term-equal? (make-constant #'sym1 "sym2") (make-constant #f 'sym1)))
|
||||
(test-false "con/var" (term-equal? (make-constant #'sym1 "sym2") (make-variable #f 'sym1)))
|
||||
(test-false "var/con" (term-equal? (make-variable #f 'sym1) (make-constant #'sym1 "sym2"))))
|
||||
|
||||
(test-suite
|
||||
"literal-equal?"
|
||||
(test-not-false "lit" (literal-equal? (make-literal #f 'lit1 empty) (make-literal #'lit1 'lit1 empty)))
|
||||
(test-not-false "lit" (literal-equal? (make-literal #f 'lit1 (list (make-variable #f 'sym1)))
|
||||
(make-literal #'lit1 'lit1 (list (make-variable #f 'sym1)))))
|
||||
(test-not-false "lit" (literal-equal? (make-literal #f 'lit1 (list (make-variable #f 'sym1)))
|
||||
(make-literal #'lit1 'lit1 (list (make-variable #'sym1 'sym1)))))
|
||||
(test-false "lit" (literal-equal? (make-literal #f 'lit1 empty) (make-literal #'lit1 'lit2 empty)))
|
||||
(test-false "lit" (literal-equal? (make-literal #f 'lit1 (list (make-variable #f 'sym1))) (make-literal #'lit1 'lit2 empty)))
|
||||
(test-false "lit" (literal-equal? (make-literal #f 'lit1 (list (make-variable #f 'sym1)))
|
||||
(make-literal #'lit1 'lit2 (list (make-variable #'sym1 'sym2))))))
|
||||
|
||||
(test-suite
|
||||
"clause-equal?"
|
||||
(test-not-false "lit" (clause-equal? (make-clause #f (make-literal #f 'lit1 empty) empty)
|
||||
(make-clause #f (make-literal #f 'lit1 empty) empty)))
|
||||
(test-not-false "lit" (clause-equal? (make-clause #f (make-literal #f 'lit1 empty) (list (make-literal #f 'lit1 empty)))
|
||||
(make-clause #f (make-literal #f 'lit1 empty) (list (make-literal #f 'lit1 empty)))))
|
||||
(test-not-false "lit" (clause-equal? (make-clause #f (make-literal #f 'lit1 empty) empty)
|
||||
(make-clause #'cl1 (make-literal #f 'lit1 empty) empty)))
|
||||
(test-false "lit" (clause-equal? (make-clause #f (make-literal #f 'lit1 empty) empty)
|
||||
(make-clause #f (make-literal #f 'lit2 empty) empty)))
|
||||
(test-false "lit" (clause-equal? (make-clause #f (make-literal #f 'lit1 empty) (list (make-literal #f 'lit1 empty)))
|
||||
(make-clause #f (make-literal #f 'lit1 empty) empty)))
|
||||
(test-false "lit" (clause-equal? (make-clause #f (make-literal #f 'lit1 empty) (list (make-literal #f 'lit1 empty)))
|
||||
(make-clause #f (make-literal #f 'lit1 empty) (list (make-literal #f 'lit2 empty))))))))
|
||||
42
collects/tests/datalog/eval.rkt
Normal file
42
collects/tests/datalog/eval.rkt
Normal file
|
|
@ -0,0 +1,42 @@
|
|||
#lang racket
|
||||
(require rackunit
|
||||
racket/runtime-path
|
||||
datalog/parse
|
||||
datalog/eval)
|
||||
|
||||
(provide eval-tests)
|
||||
|
||||
(define-runtime-path here ".")
|
||||
|
||||
(define (test-examples examples-dir)
|
||||
|
||||
(define (test-example t)
|
||||
(define test-rkt (build-path examples-dir (format "~a.rkt" t)))
|
||||
(define test-txt (build-path examples-dir (format "~a.txt" t)))
|
||||
(test-equal? t
|
||||
(filter (lambda (l)
|
||||
(not (string=? l "")))
|
||||
(with-input-from-string
|
||||
(with-output-to-string
|
||||
(lambda () (dynamic-require test-rkt #f)))
|
||||
port->lines))
|
||||
(filter (lambda (l)
|
||||
(not (string=? l "")))
|
||||
(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-files examples-dir)))
|
||||
|
||||
(define eval-tests
|
||||
(test-suite
|
||||
"eval"
|
||||
|
||||
(test-examples (build-path here "examples"))
|
||||
(test-examples (build-path here "paren-examples"))))
|
||||
12
collects/tests/datalog/examples/ancestor.rkt
Normal file
12
collects/tests/datalog/examples/ancestor.rkt
Normal file
|
|
@ -0,0 +1,12 @@
|
|||
#lang datalog
|
||||
% Equality test
|
||||
ancestor(A, B) :-
|
||||
parent(A, B).
|
||||
ancestor(A, B) :-
|
||||
parent(A, C),
|
||||
D = C, % Unification required
|
||||
ancestor(D, B).
|
||||
parent(john, douglas).
|
||||
parent(bob, john).
|
||||
parent(ebbon, bob).
|
||||
ancestor(A, B)?
|
||||
7
collects/tests/datalog/examples/bidipath.rkt
Normal file
7
collects/tests/datalog/examples/bidipath.rkt
Normal file
|
|
@ -0,0 +1,7 @@
|
|||
#lang datalog
|
||||
% path test from Chen & Warren
|
||||
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) :- path(X, Z), edge(Z, Y).
|
||||
path(X, Y)?
|
||||
12
collects/tests/datalog/examples/laps.rkt
Normal file
12
collects/tests/datalog/examples/laps.rkt
Normal file
|
|
@ -0,0 +1,12 @@
|
|||
#lang datalog
|
||||
% Laps Test
|
||||
contains(ca, store, rams_couch, rams).
|
||||
contains(rams, fetch, rams_couch, will).
|
||||
contains(ca, fetch, Name, Watcher) :-
|
||||
contains(ca, store, Name, Owner),
|
||||
contains(Owner, fetch, Name, Watcher).
|
||||
trusted(ca).
|
||||
permit(User, Priv, Name) :-
|
||||
contains(Auth, Priv, Name, User),
|
||||
trusted(Auth).
|
||||
permit(User, Priv, Name)?
|
||||
8
collects/tests/datalog/examples/long.rkt
Normal file
8
collects/tests/datalog/examples/long.rkt
Normal file
|
|
@ -0,0 +1,8 @@
|
|||
#lang datalog
|
||||
abcdefghi(z123456789,
|
||||
z1234567890123456789,
|
||||
z123456789012345678901234567890123456789,
|
||||
z1234567890123456789012345678901234567890123456789012345678901234567890123456789).
|
||||
|
||||
this_is_a_long_identifier_and_tests_the_scanners_concat_when_read_with_a_small_buffer.
|
||||
this_is_a_long_identifier_and_tests_the_scanners_concat_when_read_with_a_small_buffer?
|
||||
6
collects/tests/datalog/examples/path.rkt
Normal file
6
collects/tests/datalog/examples/path.rkt
Normal file
|
|
@ -0,0 +1,6 @@
|
|||
#lang datalog
|
||||
% path test from Chen & Warren
|
||||
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)?
|
||||
6
collects/tests/datalog/examples/pq.rkt
Normal file
6
collects/tests/datalog/examples/pq.rkt
Normal file
|
|
@ -0,0 +1,6 @@
|
|||
#lang datalog
|
||||
% p q test from Chen & Warren
|
||||
q(X) :- p(X).
|
||||
q(a).
|
||||
p(X) :- q(X).
|
||||
q(X)?
|
||||
6
collects/tests/datalog/examples/revpath.rkt
Normal file
6
collects/tests/datalog/examples/revpath.rkt
Normal file
|
|
@ -0,0 +1,6 @@
|
|||
#lang datalog
|
||||
% path test from Chen & Warren
|
||||
edge(a, b). edge(b, c). edge(c, d). edge(d, a).
|
||||
path(X, Y) :- edge(X, Y).
|
||||
path(X, Y) :- path(X, Z), edge(Z, Y).
|
||||
path(X, Y)?
|
||||
5
collects/tests/datalog/examples/says.rkt
Normal file
5
collects/tests/datalog/examples/says.rkt
Normal file
|
|
@ -0,0 +1,5 @@
|
|||
#lang datalog
|
||||
tpme(tpme1).
|
||||
ms(m1,'TPME',tpme1,ek,tp).
|
||||
says(TPME,M) :- tpme(TPME),ms(M,'TPME',TPME,A,B).
|
||||
says(A,B)?
|
||||
3
collects/tests/datalog/examples/true.rkt
Normal file
3
collects/tests/datalog/examples/true.rkt
Normal file
|
|
@ -0,0 +1,3 @@
|
|||
#lang datalog
|
||||
true.
|
||||
true?
|
||||
42
collects/tests/datalog/examples/tutorial.rkt
Normal file
42
collects/tests/datalog/examples/tutorial.rkt
Normal file
|
|
@ -0,0 +1,42 @@
|
|||
#lang datalog
|
||||
|
||||
parent(john,douglas).
|
||||
parent(john,douglas)?
|
||||
% parent(john, douglas).
|
||||
|
||||
parent(john,ebbon)?
|
||||
|
||||
parent(bob,john).
|
||||
parent(ebbon,bob).
|
||||
parent(A,B)?
|
||||
% parent(john, douglas).
|
||||
% parent(bob, john).
|
||||
% parent(ebbon, bob).
|
||||
|
||||
parent(john,B)?
|
||||
% parent(john, douglas).
|
||||
|
||||
parent(A,A)?
|
||||
|
||||
ancestor(A,B) :- parent(A,B).
|
||||
ancestor(A,B) :- parent(A,C), ancestor(C, B).
|
||||
ancestor(A, B)?
|
||||
% ancestor(ebbon, bob).
|
||||
% ancestor(bob, john).
|
||||
% ancestor(john, douglas).
|
||||
% ancestor(bob, douglas).
|
||||
% ancestor(ebbon, john).
|
||||
% ancestor(ebbon, douglas).
|
||||
|
||||
ancestor(X,john)?
|
||||
% ancestor(bob, john).
|
||||
% ancestor(ebbon, john).
|
||||
|
||||
parent(bob, john)~
|
||||
parent(A,B)?
|
||||
% parent(john, douglas).
|
||||
% parent(ebbon, bob).
|
||||
|
||||
ancestor(A,B)?
|
||||
% ancestor(john, douglas).
|
||||
% ancestor(ebbon, bob).
|
||||
45
collects/tests/datalog/main.rkt
Normal file
45
collects/tests/datalog/main.rkt
Normal file
|
|
@ -0,0 +1,45 @@
|
|||
#lang racket
|
||||
(require racket/runtime-path
|
||||
rackunit
|
||||
rackunit/text-ui
|
||||
"ast.rkt"
|
||||
|
||||
"private/lex.rkt"
|
||||
"tool/syntax-color.rkt"
|
||||
"parse.rkt"
|
||||
|
||||
"pretty.rkt"
|
||||
|
||||
"private/env.rkt"
|
||||
"private/subst.rkt"
|
||||
"private/unify.rkt"
|
||||
"private/variant.rkt"
|
||||
|
||||
"runtime.rkt"
|
||||
"eval.rkt")
|
||||
|
||||
(define-runtime-path racket-mod "racket.rkt")
|
||||
(define stdout (current-output-port))
|
||||
|
||||
(run-tests
|
||||
(test-suite
|
||||
"Datalog"
|
||||
ast-tests
|
||||
|
||||
lex-tests
|
||||
syntax-color-tests
|
||||
parse-tests
|
||||
|
||||
pretty-tests
|
||||
|
||||
env-tests
|
||||
subst-tests
|
||||
unify-tests
|
||||
variant-tests
|
||||
|
||||
runtime-tests
|
||||
eval-tests
|
||||
|
||||
(test-case "Racket Interop"
|
||||
(parameterize ([current-output-port stdout])
|
||||
(dynamic-require racket-mod #f)))))
|
||||
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).
|
||||
12
collects/tests/datalog/paren-examples/ancestor.rkt
Normal file
12
collects/tests/datalog/paren-examples/ancestor.rkt
Normal file
|
|
@ -0,0 +1,12 @@
|
|||
#lang datalog/sexp
|
||||
; Equality test
|
||||
(! (:- (ancestor A B)
|
||||
(parent A B)))
|
||||
(! (:- (ancestor A B)
|
||||
(parent A C)
|
||||
(= D C) ; Unification required
|
||||
(ancestor D B)))
|
||||
(! (parent john douglas))
|
||||
(! (parent bob john))
|
||||
(! (parent ebbon bob))
|
||||
(? (ancestor A B))
|
||||
6
collects/tests/datalog/paren-examples/ancestor.txt
Normal file
6
collects/tests/datalog/paren-examples/ancestor.txt
Normal file
|
|
@ -0,0 +1,6 @@
|
|||
ancestor(ebbon, bob).
|
||||
ancestor(bob, john).
|
||||
ancestor(john, douglas).
|
||||
ancestor(bob, douglas).
|
||||
ancestor(ebbon, john).
|
||||
ancestor(ebbon, douglas).
|
||||
15
collects/tests/datalog/paren-examples/bidipath.rkt
Normal file
15
collects/tests/datalog/paren-examples/bidipath.rkt
Normal file
|
|
@ -0,0 +1,15 @@
|
|||
#lang datalog/sexp
|
||||
; path test from Chen & Warren
|
||||
(! (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)
|
||||
(path X Z)
|
||||
(edge Z Y)))
|
||||
(? (path X Y))
|
||||
17
collects/tests/datalog/paren-examples/bidipath.txt
Normal file
17
collects/tests/datalog/paren-examples/bidipath.txt
Normal file
|
|
@ -0,0 +1,17 @@
|
|||
path(a, a).
|
||||
path(a, d).
|
||||
path(a, c).
|
||||
path(a, b).
|
||||
path(b, b).
|
||||
path(b, a).
|
||||
path(b, d).
|
||||
path(b, c).
|
||||
path(c, c).
|
||||
path(c, b).
|
||||
path(c, a).
|
||||
path(c, d).
|
||||
path(d, d).
|
||||
path(d, c).
|
||||
path(d, b).
|
||||
path(d, a).
|
||||
|
||||
13
collects/tests/datalog/paren-examples/laps.rkt
Normal file
13
collects/tests/datalog/paren-examples/laps.rkt
Normal file
|
|
@ -0,0 +1,13 @@
|
|||
#lang datalog/sexp
|
||||
; Laps Test
|
||||
(! (contains ca store rams_couch rams))
|
||||
(! (contains rams fetch rams_couch will))
|
||||
(! (:- (contains ca fetch Name Watcher)
|
||||
(contains ca store Name Owner)
|
||||
(contains Owner fetch Name Watcher)))
|
||||
(! (trusted ca))
|
||||
(! (:- (permit User Priv Name)
|
||||
(contains Auth Priv Name User)
|
||||
(trusted Auth)))
|
||||
(? (permit User Priv Name))
|
||||
|
||||
2
collects/tests/datalog/paren-examples/laps.txt
Normal file
2
collects/tests/datalog/paren-examples/laps.txt
Normal file
|
|
@ -0,0 +1,2 @@
|
|||
permit(rams, store, rams_couch).
|
||||
permit(will, fetch, rams_couch).
|
||||
8
collects/tests/datalog/paren-examples/long.rkt
Normal file
8
collects/tests/datalog/paren-examples/long.rkt
Normal file
|
|
@ -0,0 +1,8 @@
|
|||
#lang datalog/sexp
|
||||
(! (abcdefghi z123456789
|
||||
z1234567890123456789
|
||||
z123456789012345678901234567890123456789
|
||||
z1234567890123456789012345678901234567890123456789012345678901234567890123456789))
|
||||
(! this_is_a_long_identifier_and_tests_the_scanners_concat_when_read_with_a_small_buffer)
|
||||
(? this_is_a_long_identifier_and_tests_the_scanners_concat_when_read_with_a_small_buffer)
|
||||
|
||||
1
collects/tests/datalog/paren-examples/long.txt
Normal file
1
collects/tests/datalog/paren-examples/long.txt
Normal file
|
|
@ -0,0 +1 @@
|
|||
this_is_a_long_identifier_and_tests_the_scanners_concat_when_read_with_a_small_buffer.
|
||||
12
collects/tests/datalog/paren-examples/path.rkt
Normal file
12
collects/tests/datalog/paren-examples/path.rkt
Normal file
|
|
@ -0,0 +1,12 @@
|
|||
#lang datalog/sexp
|
||||
; path test from Chen & Warren
|
||||
(! (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))
|
||||
17
collects/tests/datalog/paren-examples/path.txt
Normal file
17
collects/tests/datalog/paren-examples/path.txt
Normal file
|
|
@ -0,0 +1,17 @@
|
|||
path(a, a).
|
||||
path(a, d).
|
||||
path(a, c).
|
||||
path(a, b).
|
||||
path(b, a).
|
||||
path(b, d).
|
||||
path(b, c).
|
||||
path(b, b).
|
||||
path(c, a).
|
||||
path(c, d).
|
||||
path(c, c).
|
||||
path(c, b).
|
||||
path(d, b).
|
||||
path(d, c).
|
||||
path(d, d).
|
||||
path(d, a).
|
||||
|
||||
8
collects/tests/datalog/paren-examples/pq.rkt
Normal file
8
collects/tests/datalog/paren-examples/pq.rkt
Normal file
|
|
@ -0,0 +1,8 @@
|
|||
#lang datalog/sexp
|
||||
; p q test from Chen & Warren
|
||||
(! (:- (q X)
|
||||
(p X)))
|
||||
(! (q a))
|
||||
(! (:- (p X)
|
||||
(q X)))
|
||||
(? (q X))
|
||||
1
collects/tests/datalog/paren-examples/pq.txt
Normal file
1
collects/tests/datalog/paren-examples/pq.txt
Normal file
|
|
@ -0,0 +1 @@
|
|||
q(a).
|
||||
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).
|
||||
12
collects/tests/datalog/paren-examples/revpath.rkt
Normal file
12
collects/tests/datalog/paren-examples/revpath.rkt
Normal file
|
|
@ -0,0 +1,12 @@
|
|||
#lang datalog/sexp
|
||||
; path test from Chen & Warren
|
||||
(! (edge a b))
|
||||
(! (edge b c))
|
||||
(! (edge c d))
|
||||
(! (edge d a))
|
||||
(! (:- (path X Y)
|
||||
(edge X Y)))
|
||||
(! (:- (path X Y)
|
||||
(path X Z)
|
||||
(edge Z Y)))
|
||||
(? (path X Y))
|
||||
17
collects/tests/datalog/paren-examples/revpath.txt
Normal file
17
collects/tests/datalog/paren-examples/revpath.txt
Normal file
|
|
@ -0,0 +1,17 @@
|
|||
path(a, a).
|
||||
path(a, d).
|
||||
path(a, c).
|
||||
path(a, b).
|
||||
path(b, b).
|
||||
path(b, a).
|
||||
path(b, d).
|
||||
path(b, c).
|
||||
path(c, c).
|
||||
path(c, b).
|
||||
path(c, a).
|
||||
path(c, d).
|
||||
path(d, d).
|
||||
path(d, c).
|
||||
path(d, b).
|
||||
path(d, a).
|
||||
|
||||
7
collects/tests/datalog/paren-examples/says.rkt
Normal file
7
collects/tests/datalog/paren-examples/says.rkt
Normal file
|
|
@ -0,0 +1,7 @@
|
|||
#lang datalog/sexp
|
||||
(! (tpme tpme1))
|
||||
(! (ms m1 "TPME" tpme1 ek tp))
|
||||
(! (:- (says TPME M)
|
||||
(tpme TPME)
|
||||
(ms M "TPME" TPME A B)))
|
||||
(? (says A B))
|
||||
1
collects/tests/datalog/paren-examples/says.txt
Normal file
1
collects/tests/datalog/paren-examples/says.txt
Normal file
|
|
@ -0,0 +1 @@
|
|||
says(tpme1, m1).
|
||||
3
collects/tests/datalog/paren-examples/true.rkt
Normal file
3
collects/tests/datalog/paren-examples/true.rkt
Normal file
|
|
@ -0,0 +1,3 @@
|
|||
#lang datalog/sexp
|
||||
(! true)
|
||||
(? true)
|
||||
1
collects/tests/datalog/paren-examples/true.txt
Normal file
1
collects/tests/datalog/paren-examples/true.txt
Normal file
|
|
@ -0,0 +1 @@
|
|||
true.
|
||||
28
collects/tests/datalog/paren-examples/tutorial.rkt
Normal file
28
collects/tests/datalog/paren-examples/tutorial.rkt
Normal file
|
|
@ -0,0 +1,28 @@
|
|||
#lang datalog/sexp
|
||||
(! (parent john douglas))
|
||||
(? (parent john douglas))
|
||||
|
||||
(? (parent john ebbon))
|
||||
|
||||
(! (parent bob john))
|
||||
(! (parent ebbon bob))
|
||||
(? (parent A B))
|
||||
|
||||
(? (parent john B))
|
||||
|
||||
(? (parent A A))
|
||||
|
||||
(! (:- (ancestor A B)
|
||||
(parent A B)))
|
||||
(! (:- (ancestor A B)
|
||||
(parent A C)
|
||||
(ancestor C B)))
|
||||
(? (ancestor A B))
|
||||
|
||||
(? (ancestor X john))
|
||||
|
||||
(~ (parent bob john))
|
||||
|
||||
(? (parent A B))
|
||||
|
||||
(? (ancestor A B))
|
||||
26
collects/tests/datalog/paren-examples/tutorial.txt
Normal file
26
collects/tests/datalog/paren-examples/tutorial.txt
Normal file
|
|
@ -0,0 +1,26 @@
|
|||
parent(john, douglas).
|
||||
|
||||
|
||||
parent(john, douglas).
|
||||
parent(bob, john).
|
||||
parent(ebbon, bob).
|
||||
|
||||
parent(john, douglas).
|
||||
|
||||
|
||||
ancestor(ebbon, bob).
|
||||
ancestor(bob, john).
|
||||
ancestor(john, douglas).
|
||||
ancestor(bob, douglas).
|
||||
ancestor(ebbon, john).
|
||||
ancestor(ebbon, douglas).
|
||||
|
||||
ancestor(bob, john).
|
||||
ancestor(ebbon, john).
|
||||
|
||||
parent(john, douglas).
|
||||
parent(ebbon, bob).
|
||||
|
||||
ancestor(ebbon, bob).
|
||||
ancestor(john, douglas).
|
||||
|
||||
52
collects/tests/datalog/parse.rkt
Normal file
52
collects/tests/datalog/parse.rkt
Normal file
|
|
@ -0,0 +1,52 @@
|
|||
#lang racket
|
||||
(require rackunit
|
||||
datalog/ast
|
||||
datalog/parse
|
||||
"util.rkt")
|
||||
|
||||
(provide parse-tests)
|
||||
|
||||
(define (test-literal-parse str res)
|
||||
(test-literal str (parse-literal (open-input-string str)) res))
|
||||
(define (test-clause-parse str res)
|
||||
(test-clause str (parse-clause (open-input-string str)) res))
|
||||
|
||||
(define parse-tests
|
||||
(test-suite
|
||||
"parse"
|
||||
|
||||
(test-suite
|
||||
"literal"
|
||||
(test-literal-parse "parent(john, douglas)"
|
||||
(make-literal #f 'parent (list (make-constant #f 'john) (make-constant #f 'douglas))))
|
||||
(test-literal-parse "1 = 2"
|
||||
(make-literal #f '= (list (make-constant #f '|1|) (make-constant #f '|2|))))
|
||||
(test-literal-parse "zero-arity-literal"
|
||||
(make-literal #f 'zero-arity-literal empty))
|
||||
(test-literal-parse "zero-arity-literal()"
|
||||
(make-literal #f 'zero-arity-literal empty))
|
||||
(test-literal-parse "\"=\"(3,3)"
|
||||
(make-literal #f "=" (list (make-constant #f '|3|) (make-constant #f '|3|))))
|
||||
(test-literal-parse "\"\"(-0-0-0,&&&,***,\"\00\")"
|
||||
(make-literal #f "" (list (make-constant #f '-0-0-0)
|
||||
(make-constant #f '&&&)
|
||||
(make-constant #f '***)
|
||||
(make-constant #f "\00")))))
|
||||
|
||||
(test-suite
|
||||
"clause"
|
||||
(test-clause-parse "parent(john, douglas)"
|
||||
(make-clause #f (make-literal #f 'parent (list (make-constant #f 'john) (make-constant #f 'douglas))) empty))
|
||||
(test-clause-parse "ancestor(A, B) :- parent(A, B)"
|
||||
(make-clause #f (make-literal #f 'ancestor (list (make-variable #f 'A) (make-variable #f 'B)))
|
||||
(list (make-literal #f 'parent (list (make-variable #f 'A) (make-variable #f 'B))))))
|
||||
(test-clause-parse "ancestor(A, B) :- parent(A, C), ancestor(C, B)"
|
||||
(make-clause #f (make-literal #f 'ancestor (list (make-variable #f 'A) (make-variable #f 'B)))
|
||||
(list (make-literal #f 'parent (list (make-variable #f 'A) (make-variable #f 'C)))
|
||||
(make-literal #f 'ancestor (list (make-variable #f 'C) (make-variable #f 'B)))))))
|
||||
|
||||
(test-suite
|
||||
"statement"
|
||||
(test-not-false "assertion" (assertion? (parse-statement (open-input-string "parent(john, douglas)."))))
|
||||
(test-not-false "retraction" (retraction? (parse-statement (open-input-string "parent(john, douglas)~"))))
|
||||
(test-not-false "query" (query? (parse-statement (open-input-string "parent(john, douglas)?")))))))
|
||||
49
collects/tests/datalog/pretty.rkt
Normal file
49
collects/tests/datalog/pretty.rkt
Normal file
|
|
@ -0,0 +1,49 @@
|
|||
#lang racket
|
||||
(require rackunit
|
||||
datalog/parse
|
||||
datalog/pretty)
|
||||
(provide pretty-tests)
|
||||
|
||||
(define pretty-tests
|
||||
(test-suite
|
||||
"Pretty"
|
||||
|
||||
(test-equal? "program"
|
||||
(format-program
|
||||
(parse-program
|
||||
(open-input-string #<<END
|
||||
parent(john, douglas).
|
||||
parent(john, douglas)?
|
||||
parent(john, ebbon)?
|
||||
parent(bob, john).
|
||||
parent(ebbon, bob).
|
||||
parent(A, B)?
|
||||
parent(john, B)?
|
||||
parent(A, A)?
|
||||
ancestor(A, B) :- parent(A, B).
|
||||
ancestor(A, B) :-
|
||||
parent(A, C),
|
||||
ancestor(C, B).
|
||||
ancestor(A, B)?
|
||||
parent(bob, john)~
|
||||
parent(A,B)?
|
||||
ancestor(A,B)?
|
||||
END
|
||||
)))
|
||||
#<<END
|
||||
parent(john, douglas).
|
||||
parent(john, douglas)?
|
||||
parent(john, ebbon)?
|
||||
parent(bob, john).
|
||||
parent(ebbon, bob).
|
||||
parent(A, B)?
|
||||
parent(john, B)?
|
||||
parent(A, A)?
|
||||
ancestor(A, B) :- parent(A, B).
|
||||
ancestor(A, B) :- parent(A, C), ancestor(C, B).
|
||||
ancestor(A, B)?
|
||||
parent(bob, john)~
|
||||
parent(A, B)?
|
||||
ancestor(A, B)?
|
||||
END
|
||||
)))
|
||||
22
collects/tests/datalog/private/env.rkt
Normal file
22
collects/tests/datalog/private/env.rkt
Normal file
|
|
@ -0,0 +1,22 @@
|
|||
#lang racket
|
||||
(require rackunit
|
||||
datalog/ast
|
||||
datalog/private/env)
|
||||
|
||||
(provide env-tests)
|
||||
|
||||
(define t1 (make-constant #f 't1))
|
||||
(define t2 (make-constant #f 't2))
|
||||
|
||||
(define env-tests
|
||||
(test-suite
|
||||
"env"
|
||||
|
||||
(test-equal? "default" (lookup (empty-env) 'v) #f)
|
||||
(test-equal? "default" (lookup (empty-env) 'v t1) t1)
|
||||
(test-equal? "extend" (lookup (extend (empty-env) 'v1 t1) 'v1) t1)
|
||||
(test-equal? "extend"
|
||||
(lookup (extend (extend (empty-env) 'v1 t1)
|
||||
'v1 t1)
|
||||
'v1)
|
||||
t1)))
|
||||
37
collects/tests/datalog/private/lex.rkt
Normal file
37
collects/tests/datalog/private/lex.rkt
Normal file
|
|
@ -0,0 +1,37 @@
|
|||
#lang racket
|
||||
(require rackunit
|
||||
parser-tools/lex
|
||||
datalog/private/lex)
|
||||
|
||||
(provide lex-tests)
|
||||
|
||||
(define (test-lexer str tok-name [tok-value str])
|
||||
(define pv (dlexer (open-input-string str)))
|
||||
(define v (position-token-token pv))
|
||||
(test-equal? (format "lexer: ~a: <~a,~a>" str tok-name tok-value)
|
||||
(cons tok-name tok-value)
|
||||
(cons (token-name v) (token-value v))))
|
||||
|
||||
(define lex-tests
|
||||
(test-suite
|
||||
"lex"
|
||||
|
||||
(test-lexer "=" 'EQUAL #f)
|
||||
(test-lexer "?" 'QMARK #f)
|
||||
(test-lexer "~" 'TILDE #f)
|
||||
(test-lexer "." 'DOT #f)
|
||||
(test-lexer ")" 'RPAREN #f)
|
||||
(test-lexer "," 'COMMA #f)
|
||||
(test-lexer "(" 'LPAREN #f)
|
||||
(test-lexer "\"\"" 'STRING "")
|
||||
(test-lexer "\"foo\"" 'STRING "foo")
|
||||
(test-lexer "\"\\\"\"" 'STRING "\"")
|
||||
(test-lexer ":-" 'TSTILE #f)
|
||||
(test-lexer "" 'EOF #f)
|
||||
(test-lexer "Va1_" 'VARIABLE)
|
||||
(test-lexer "val_" 'IDENTIFIER)
|
||||
(test-lexer "912Kadf" 'IDENTIFIER)
|
||||
(test-lexer " =" 'EQUAL #f)
|
||||
(test-lexer "% 12453\n=" 'EQUAL #f)
|
||||
|
||||
))
|
||||
114
collects/tests/datalog/private/subst.rkt
Normal file
114
collects/tests/datalog/private/subst.rkt
Normal file
|
|
@ -0,0 +1,114 @@
|
|||
#lang racket
|
||||
(require rackunit
|
||||
datalog/private/subst
|
||||
datalog/ast
|
||||
datalog/private/env)
|
||||
(require/expose datalog/private/subst (subst-literal shuffle))
|
||||
|
||||
(provide subst-tests)
|
||||
|
||||
(define (gensym-var? v)
|
||||
(define s (variable-sym v))
|
||||
(not (eq? s (string->symbol (symbol->string s)))))
|
||||
|
||||
(define subst-tests
|
||||
(test-suite
|
||||
"subst"
|
||||
|
||||
(test-suite
|
||||
"subst-term"
|
||||
(test-equal? "con"
|
||||
(subst-term (empty-env) (make-constant #f 'v1))
|
||||
(make-constant #f 'v1))
|
||||
(test-equal? "var def"
|
||||
(subst-term (empty-env) (make-variable #f 'v1))
|
||||
(make-variable #f 'v1))
|
||||
(test-equal? "var"
|
||||
(subst-term (extend (empty-env) 'v1 (make-constant #f 'v1)) (make-variable #f 'v1))
|
||||
(make-constant #f 'v1)))
|
||||
|
||||
(test-suite
|
||||
"subst-literal"
|
||||
(test-equal? "con"
|
||||
(subst-literal (empty-env) (make-literal #f 'lit (list (make-constant #f 'v1))))
|
||||
(make-literal #f 'lit (list (make-constant #f 'v1))))
|
||||
(test-equal? "var def"
|
||||
(subst-literal (extend (empty-env) 'v1 (make-constant #f 'v1)) (make-literal #f 'lit (list (make-variable #f 'v1))))
|
||||
(make-literal #f 'lit (list (make-constant #f 'v1))))
|
||||
(test-equal? "var def"
|
||||
(subst-literal (extend (empty-env) 'v1 (make-constant #f 'v1)) (make-literal #f 'lit (list (make-variable #f 'v1))))
|
||||
(make-literal #f 'lit (list (make-constant #f 'v1)))))
|
||||
|
||||
(test-suite
|
||||
"subst-clause"
|
||||
(test-equal? "con"
|
||||
(subst-clause (empty-env) (make-clause #f (make-literal #f 'lit (list (make-constant #f 'v1))) empty))
|
||||
(make-clause #f (make-literal #f 'lit (list (make-constant #f 'v1))) empty))
|
||||
(test-equal? "var def"
|
||||
(subst-clause (extend (empty-env) 'v1 (make-constant #f 'v1))
|
||||
(make-clause #f (make-literal #f 'lit (list (make-variable #f 'v1))) empty))
|
||||
(make-clause #f (make-literal #f 'lit (list (make-constant #f 'v1))) empty))
|
||||
(test-equal? "var def"
|
||||
(subst-clause (extend (empty-env) 'v1 (make-constant #f 'v1))
|
||||
(make-clause #f (make-literal #f 'lit (list (make-variable #f 'v1))) empty))
|
||||
(make-clause #f (make-literal #f 'lit (list (make-constant #f 'v1))) empty))
|
||||
|
||||
(test-equal? "con"
|
||||
(subst-clause (empty-env) (make-clause #f (make-literal #f 'lit (list (make-constant #f 'v1)))
|
||||
(list (make-literal #f 'lit (list (make-constant #f 'v1))))))
|
||||
(make-clause #f (make-literal #f 'lit (list (make-constant #f 'v1)))
|
||||
(list (make-literal #f 'lit (list (make-constant #f 'v1))))))
|
||||
(test-equal? "var def"
|
||||
(subst-clause (extend (empty-env) 'v1 (make-constant #f 'v1))
|
||||
(make-clause #f (make-literal #f 'lit (list (make-variable #f 'v1)))
|
||||
(list (make-literal #f 'lit (list (make-variable #f 'v1))))))
|
||||
(make-clause #f (make-literal #f 'lit (list (make-constant #f 'v1)))
|
||||
(list (make-literal #f 'lit (list (make-constant #f 'v1))))))
|
||||
(test-equal? "var def"
|
||||
(subst-clause (extend (empty-env) 'v1 (make-constant #f 'v1))
|
||||
(make-clause #f (make-literal #f 'lit (list (make-variable #f 'v1)))
|
||||
(list (make-literal #f 'lit (list (make-variable #f 'v1))))))
|
||||
(make-clause #f (make-literal #f 'lit (list (make-constant #f 'v1)))
|
||||
(list (make-literal #f 'lit (list (make-constant #f 'v1)))))))
|
||||
|
||||
(test-suite
|
||||
"shuffle"
|
||||
(test-equal? "con"
|
||||
(shuffle (empty-env) (make-literal #f 'lit (list (make-constant #f 'v1))))
|
||||
(empty-env))
|
||||
(test-equal? "var"
|
||||
(shuffle (extend (empty-env) 'v1 (make-constant #f 'k1)) (make-literal #f 'lit (list (make-variable #f 'v1))))
|
||||
(extend (empty-env) 'v1 (make-constant #f 'k1)))
|
||||
(test-not-false "var"
|
||||
(gensym-var? (lookup (shuffle (empty-env)
|
||||
(make-literal #f 'lit (list (make-variable #f 'v1))))
|
||||
'v1))))
|
||||
|
||||
(test-suite
|
||||
"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-question (make-literal #f 'lit (list (make-variable #f 'v1)))))))))
|
||||
|
||||
(test-suite
|
||||
"rename-clause"
|
||||
(test-equal? "c" (rename-clause (make-clause #f (make-literal #f 'lit (list (make-constant #f 'v1))) empty))
|
||||
(make-clause #f (make-literal #f 'lit (list (make-constant #f 'v1))) empty))
|
||||
(test-not-false "c"
|
||||
(gensym-var?
|
||||
(first
|
||||
(literal-terms
|
||||
(clause-head
|
||||
(rename-clause (make-clause #f (make-literal #f 'lit (list (make-variable #f 'v1))) empty)))))))
|
||||
(test-not-false "c"
|
||||
(gensym-var?
|
||||
(first
|
||||
(literal-terms
|
||||
(first
|
||||
(clause-body
|
||||
(rename-clause (make-clause #f (make-literal #f 'lit (list (make-constant #f 'v1)))
|
||||
(list (make-literal #f 'lit (list (make-variable #f 'v1)))))))))))))))
|
||||
54
collects/tests/datalog/private/unify.rkt
Normal file
54
collects/tests/datalog/private/unify.rkt
Normal file
|
|
@ -0,0 +1,54 @@
|
|||
#lang racket
|
||||
(require rackunit
|
||||
datalog/ast
|
||||
datalog/private/env
|
||||
datalog/private/unify)
|
||||
(require/expose datalog/private/unify (chase))
|
||||
|
||||
(provide unify-tests)
|
||||
|
||||
(define unify-tests
|
||||
(test-suite
|
||||
"unify"
|
||||
|
||||
(test-suite
|
||||
"chase"
|
||||
(test-equal? "con" (chase (empty-env) (make-constant #f 'k1))
|
||||
(make-constant #f 'k1))
|
||||
(test-equal? "var" (chase (empty-env) (make-variable #f 'v1))
|
||||
(make-variable #f 'v1))
|
||||
(test-equal? "var->con"
|
||||
(chase (extend (empty-env) 'v1 (make-constant #f 'k1)) (make-variable #f 'v1))
|
||||
(make-constant #f 'k1))
|
||||
(test-equal? "var->var->con"
|
||||
(chase (extend (extend (empty-env) 'v2 (make-constant #f 'k1))
|
||||
'v1 (make-variable #f 'v2))
|
||||
(make-variable #f 'v1))
|
||||
(make-constant #f 'k1)))
|
||||
|
||||
(test-suite
|
||||
"unify-term"
|
||||
(test-equal? "con/con" (unify-term (empty-env) (make-constant #f 'k1) (make-constant #f 'k1))
|
||||
(empty-env))
|
||||
(test-false "con/con" (unify-term (empty-env) (make-constant #f 'k1) (make-constant #f 'k2)))
|
||||
(test-equal? "var/con" (unify-term (empty-env) (make-variable #f 'v1) (make-constant #f 'k2))
|
||||
(extend (empty-env) 'v1 (make-constant #f 'k2)))
|
||||
(test-equal? "con/var" (unify-term (empty-env) (make-constant #f 'k2) (make-variable #f 'v1))
|
||||
(extend (empty-env) 'v1 (make-constant #f 'k2)))
|
||||
(test-equal? "var/var" (unify-term (empty-env) (make-variable #f 'v1) (make-variable #f 'v2))
|
||||
(extend (empty-env) 'v1 (make-variable #f 'v2))))
|
||||
|
||||
(test-suite
|
||||
"unify-terms"
|
||||
(test-equal? "con/con" (unify-terms (empty-env) (list (make-constant #f 'k1)) (list (make-constant #f 'k1)))
|
||||
(empty-env))
|
||||
(test-false "con/con" (unify-terms (empty-env) (list (make-constant #f 'k1)) (list (make-constant #f 'k2))))
|
||||
(test-false "/con" (unify-terms (empty-env) (list) (list (make-constant #f 'k2))))
|
||||
(test-false "con/" (unify-terms (empty-env) (list (make-constant #f 'k2)) (list))))
|
||||
|
||||
(test-suite
|
||||
"unify"
|
||||
(test-false "lit/lit" (unify (make-literal #f 'lit1 empty) (make-literal #f 'lit2 empty)))
|
||||
(test-equal? "con/con" (unify (make-literal #f 'lit1 (list (make-constant #f 'k1)))
|
||||
(make-literal #f 'lit1 (list (make-constant #f 'k1))))
|
||||
(empty-env)))))
|
||||
59
collects/tests/datalog/private/variant.rkt
Normal file
59
collects/tests/datalog/private/variant.rkt
Normal file
|
|
@ -0,0 +1,59 @@
|
|||
#lang racket
|
||||
(require rackunit
|
||||
datalog/ast
|
||||
datalog/private/variant)
|
||||
(require/expose datalog/private/variant
|
||||
(variant-terms variant-term variant-var variant? term-hash mk-literal-hash))
|
||||
|
||||
(provide variant-tests)
|
||||
|
||||
(define (test-not-equal? n v1 v2)
|
||||
(test-case n (check-not-equal? v1 v2)))
|
||||
|
||||
(define variant-tests
|
||||
(test-suite
|
||||
"variant"
|
||||
|
||||
(test-suite
|
||||
"variant?"
|
||||
(test-not-false "same" (variant? (make-literal #f 'lit1 empty) (make-literal #f 'lit1 empty)))
|
||||
(test-false "dif lit" (variant? (make-literal #f 'lit1 empty) (make-literal #f 'lit2 empty)))
|
||||
(test-not-false "same" (variant? (make-literal #f 'lit1 (list (make-constant #f 'k1)))
|
||||
(make-literal #f 'lit1 (list (make-constant #f 'k1)))))
|
||||
(test-false "dif con" (variant? (make-literal #f 'lit1 (list (make-constant #f 'k1)))
|
||||
(make-literal #f 'lit1 (list (make-constant #f 'k2)))))
|
||||
(test-false "dif var/con" (variant? (make-literal #f 'lit1 (list (make-variable #f 'v1)))
|
||||
(make-literal #f 'lit1 (list (make-constant #f 'k1)))))
|
||||
(test-false "dif con/var" (variant? (make-literal #f 'lit1 (list (make-constant #f 'k1)))
|
||||
(make-literal #f 'lit1 (list (make-variable #f 'v1)))))
|
||||
(test-not-false "same" (variant? (make-literal #f 'lit1 (list (make-variable #f 'v1)))
|
||||
(make-literal #f 'lit1 (list (make-variable #f 'v1)))))
|
||||
|
||||
(test-not-false "var (dif name)" (variant? (make-literal #f 'lit1 (list (make-variable #f 'v2)))
|
||||
(make-literal #f 'lit1 (list (make-variable #f 'v1))))))
|
||||
|
||||
(test-suite
|
||||
"mem-literal"
|
||||
(test-false "mt" (mem-literal (make-literal #f 'lit1 empty) empty))
|
||||
(test-not-false "in" (mem-literal (make-literal #f 'lit1 empty) (list (make-literal #f 'lit1 empty))))
|
||||
(test-not-false "var" (mem-literal (make-literal #f 'lit1 (list (make-variable #f 'v2)))
|
||||
(list (make-literal #f 'lit1 (list (make-variable #f 'v1)))))))
|
||||
|
||||
(test-suite
|
||||
"term-hash"
|
||||
(test-equal? "var" (term-hash (make-variable #f (gensym)) equal-hash-code) 101)
|
||||
(test-equal? "con" (term-hash (make-constant #f 'v2) equal-hash-code) (equal-hash-code 'v2)))
|
||||
|
||||
(local [(define literal-hash (mk-literal-hash equal-hash-code))
|
||||
(define (literal-hash-equal? l1 l2)
|
||||
(equal? (literal-hash l1) (literal-hash l2)))]
|
||||
(test-suite
|
||||
"mk-literal-hash"
|
||||
(test-not-false "same" (literal-hash-equal? (make-literal #f 'lit1 empty) (make-literal #f 'lit1 empty)))
|
||||
(test-not-false "same" (literal-hash-equal? (make-literal #f 'lit1 (list (make-constant #f 'k1)))
|
||||
(make-literal #f 'lit1 (list (make-constant #f 'k1)))))
|
||||
(test-not-false "same" (literal-hash-equal? (make-literal #f 'lit1 (list (make-variable #f 'v1)))
|
||||
(make-literal #f 'lit1 (list (make-variable #f 'v1)))))
|
||||
|
||||
(test-not-false "var (dif name)" (literal-hash-equal? (make-literal #f 'lit1 (list (make-variable #f 'v2)))
|
||||
(make-literal #f 'lit1 (list (make-variable #f 'v1)))))))))
|
||||
84
collects/tests/datalog/racket.rkt
Normal file
84
collects/tests/datalog/racket.rkt
Normal file
|
|
@ -0,0 +1,84 @@
|
|||
#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 (hasheq 'X 'joseph3))
|
||||
|
||||
(datalog parent
|
||||
(? (parent joseph2 X)))
|
||||
=>
|
||||
(list (hasheq 'X 'joseph1)
|
||||
(hasheq 'X 'lucy))
|
||||
|
||||
(datalog parent
|
||||
(? (parent joseph2 X))
|
||||
(? (parent X joseph2)))
|
||||
=>
|
||||
(list (hasheq 'X 'joseph3))
|
||||
|
||||
(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 (hasheq 'A 'joseph3 'B 'joseph2)
|
||||
(hasheq 'A 'joseph2 'B 'lucy)
|
||||
(hasheq 'A 'joseph2 'B 'joseph1)
|
||||
(hasheq 'A 'joseph3 'B 'lucy)
|
||||
(hasheq 'A 'joseph3 'B 'joseph1))
|
||||
|
||||
(let ([x 'joseph2])
|
||||
(datalog parent
|
||||
(? (parent x X))))
|
||||
=>
|
||||
(list (hasheq 'X 'joseph1)
|
||||
(hasheq 'X 'lucy))
|
||||
|
||||
(datalog parent
|
||||
(? (add1 1 :- X)))
|
||||
=>
|
||||
(list (hasheq 'X 2))
|
||||
|
||||
(local [(local-require tests/datalog/examples/ancestor)]
|
||||
(datalog theory
|
||||
(? (ancestor A B))))
|
||||
=>
|
||||
(list (hasheq 'A 'ebbon 'B 'bob)
|
||||
(hasheq 'A 'bob 'B 'john)
|
||||
(hasheq 'A 'john 'B 'douglas)
|
||||
(hasheq 'A 'bob 'B 'douglas)
|
||||
(hasheq 'A 'ebbon 'B 'john)
|
||||
(hasheq 'A 'ebbon 'B 'douglas))
|
||||
|
||||
(local [(local-require tests/datalog/paren-examples/ancestor)]
|
||||
(datalog theory
|
||||
(? (ancestor A B))))
|
||||
=>
|
||||
(list (hasheq 'A 'ebbon 'B 'bob)
|
||||
(hasheq 'A 'bob 'B 'john)
|
||||
(hasheq 'A 'john 'B 'douglas)
|
||||
(hasheq 'A 'bob 'B 'douglas)
|
||||
(hasheq 'A 'ebbon 'B 'john)
|
||||
(hasheq 'A 'ebbon 'B 'douglas))
|
||||
|
||||
)
|
||||
44
collects/tests/datalog/runtime.rkt
Normal file
44
collects/tests/datalog/runtime.rkt
Normal file
|
|
@ -0,0 +1,44 @@
|
|||
#lang racket
|
||||
(require rackunit
|
||||
datalog/parse
|
||||
datalog/runtime
|
||||
"util.rkt")
|
||||
|
||||
(provide runtime-tests)
|
||||
|
||||
(define pc (parse-clause (open-input-string "parent(john, douglas)")))
|
||||
(define pl (parse-literal (open-input-string "parent(john, douglas)")))
|
||||
|
||||
(define runtime-tests
|
||||
(test-suite
|
||||
"runtime"
|
||||
|
||||
(test-suite
|
||||
"safe-clause?"
|
||||
(test-not-false "safe" (safe-clause? pc))
|
||||
(test-not-false "safe" (safe-clause? (parse-clause (open-input-string "ancestor(A, B) :- parent(A, B)"))))
|
||||
(test-false "not safe" (safe-clause? (parse-clause (open-input-string "ancestor(A, B) :- parent(jay, B)"))))
|
||||
(test-not-false "safe" (safe-clause? (parse-clause (open-input-string "ancestor(A, B) :- parent(A, C), ancestor(C, B)")))))
|
||||
|
||||
(test-suite
|
||||
"mut simple"
|
||||
(test-equal? "empty" (prove (make-theory) pl) empty)
|
||||
(test-literal "ass->prov"
|
||||
(let ([thy (make-theory)])
|
||||
(assume! thy pc)
|
||||
(first (prove thy pl)))
|
||||
pl)
|
||||
(test-equal? "ass->ret->prov"
|
||||
(let ([thy (make-theory)])
|
||||
(assume! thy pc)
|
||||
(retract! thy pc)
|
||||
(prove thy pl))
|
||||
empty)
|
||||
(test-equal? "ret->prov"
|
||||
(let ([thy (make-theory)])
|
||||
(retract! thy pc)
|
||||
(prove thy pl))
|
||||
empty))
|
||||
|
||||
))
|
||||
|
||||
37
collects/tests/datalog/tool/syntax-color.rkt
Normal file
37
collects/tests/datalog/tool/syntax-color.rkt
Normal file
|
|
@ -0,0 +1,37 @@
|
|||
#lang racket
|
||||
(require rackunit
|
||||
datalog/tool/syntax-color)
|
||||
|
||||
(provide syntax-color-tests)
|
||||
|
||||
(define (test-color str key)
|
||||
(define-values (lex color b start end) (get-syntax-token (open-input-string str)))
|
||||
(test-equal? (format "Syntax Color: ~a: ~a" key str) color key))
|
||||
|
||||
(define syntax-color-tests
|
||||
(test-suite
|
||||
"syntax-color"
|
||||
|
||||
(test-color " " 'whitespace)
|
||||
(test-color " " 'whitespace)
|
||||
(test-color "\t" 'whitespace)
|
||||
(test-color "\n" 'whitespace)
|
||||
(test-color "% \n" 'comment)
|
||||
(test-color "% 12 31 2 6\n" 'comment)
|
||||
(test-color "Var" 'symbol)
|
||||
(test-color "V124_3" 'symbol)
|
||||
(test-color "var" 'identifier)
|
||||
(test-color "123var" 'identifier)
|
||||
(test-color "(" 'parenthesis)
|
||||
(test-color ")" 'parenthesis)
|
||||
(test-color "=" 'parenthesis)
|
||||
(test-color "?" 'parenthesis)
|
||||
(test-color "~" 'parenthesis)
|
||||
(test-color "." 'parenthesis)
|
||||
(test-color "," 'parenthesis)
|
||||
(test-color ":-" 'parenthesis)
|
||||
(test-color "\"foo\"" 'string)
|
||||
(test-color "\"fo\\\"o\"" 'string)
|
||||
(test-color "\"fo\no\"" 'string)
|
||||
(test-color "\"foo" 'error)
|
||||
(test-color ":" 'error)))
|
||||
12
collects/tests/datalog/util.rkt
Normal file
12
collects/tests/datalog/util.rkt
Normal file
|
|
@ -0,0 +1,12 @@
|
|||
#lang racket
|
||||
(require rackunit
|
||||
datalog/ast)
|
||||
|
||||
(provide test-literal test-clause)
|
||||
|
||||
(define (test-literal str l1 l2)
|
||||
(test-case
|
||||
str (check literal-equal? l1 l2)))
|
||||
(define (test-clause str c1 c2)
|
||||
(test-case
|
||||
str (check clause-equal? c1 c2)))
|
||||
2
collects/tests/racklog/lang/laps.txt
Normal file
2
collects/tests/racklog/lang/laps.txt
Normal file
|
|
@ -0,0 +1,2 @@
|
|||
permit(rams, store, rams_couch).
|
||||
permit(will, fetch, rams_couch).
|
||||
1
collects/tests/racklog/lang/long.txt
Normal file
1
collects/tests/racklog/lang/long.txt
Normal file
|
|
@ -0,0 +1 @@
|
|||
this_is_a_long_identifier_and_tests_the_scanners_concat_when_read_with_a_small_buffer.
|
||||
1
collects/tests/racklog/lang/says.txt
Normal file
1
collects/tests/racklog/lang/says.txt
Normal file
|
|
@ -0,0 +1 @@
|
|||
says(tpme1, m1).
|
||||
1
collects/tests/racklog/lang/true.txt
Normal file
1
collects/tests/racklog/lang/true.txt
Normal file
|
|
@ -0,0 +1 @@
|
|||
true.
|
||||
Loading…
Reference in New Issue
Block a user