suzanne.soy/racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Switch to using substitutions in returns and remove old parts of the interface

Browse Source
This commit is contained in:
Jay McCarthy 2010-06-30 10:30:55 -06:00
parent 128d86da1f
commit 06844073c7
8 changed files with 87 additions and 86 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

24
collects/datalog/eval.rkt
View File

@ -4,7 +4,7 @@
"pretty.rkt"
"runtime.rkt")
(define current-theory (make-parameter (make-mutable-theory)))
(define current-theory (make-parameter (make-theory)))
(define (assume-if-safe assume thy s)
(let ([c (assertion-clause s)])
@ -35,27 +35,9 @@
[(query? s)
(prove (current-theory) (query-question s))]))
(define (eval-program/fresh p)
(let loop ([thy (make-immutable-theory)]
[p p])
(if (empty? p)
thy
(let ([s (first p)])
(loop
(cond
[(assertion? s)
(assume-if-safe assume thy s)]
[(retraction? s)
(retract thy (retraction-clause s))]
[(query? s)
(print-questions (prove thy (query-question s)))
thy])
(rest p))))))
(provide/contract
[current-theory (parameter/c mutable-theory/c)]
[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)))]
[eval-program/fresh (program/c . -> . immutable-theory/c)])
[eval-statement (statement/c . -> . (or/c void (listof question/c)))])

2
collects/datalog/main.rkt
View File

@ -2,5 +2,5 @@
(require "runtime.rkt"
"stx.rkt")
(provide make-theory
mutable-theory/c
theory/c
(all-from-out "stx.rkt"))

20
collects/datalog/runtime.rkt
View File

@ -20,17 +20,13 @@
(clause-body c)))
head-vars))
(define theory/c (coerce-contract 'exec hash?))
(define immutable-theory/c (and/c hash? immutable?))
(define mutable-theory/c (and/c hash? (not/c immutable?)))
(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-immutable-theory)
(make-immutable-hash empty))
(define (make-mutable-theory)
(define (make-theory)
(make-hash))
(define ((mk-assume hash-update) thy c)
@ -142,13 +138,7 @@
(provide/contract
[safe-clause? (clause? . -> . boolean?)]
[theory/c contract?]
[immutable-theory/c contract?]
[mutable-theory/c contract?]
[rename make-mutable-theory make-theory (-> mutable-theory/c)]
[make-mutable-theory (-> mutable-theory/c)]
[make-immutable-theory (-> immutable-theory/c)]
[assume (immutable-theory/c safe-clause? . -> . immutable-theory/c)]
[retract (immutable-theory/c clause? . -> . immutable-theory/c)]
[assume! (mutable-theory/c safe-clause? . -> . void)]
[retract! (mutable-theory/c clause? . -> . void)]
[make-theory (-> theory/c)]
[assume! (theory/c safe-clause? . -> . void)]
[retract! (theory/c clause? . -> . void)]
[prove (theory/c question/c . -> . (listof question/c))])

8
collects/datalog/scribblings/racket.scrbl
View File

@ -50,17 +50,17 @@ The Datalog database can be directly used by Racket programs through this API.
(datalog family
(? (add1 1 :- X)))]
@defthing[mutable-theory/c contract?]{ A contract for Datalog theories. }
@defthing[theory/c contract?]{ A contract for Datalog theories. }
@defproc[(make-theory) mutable-theory/c]{ Creates a theory for use with @racket[datalog]. }
@defproc[(make-theory) theory/c]{ Creates a theory for use with @racket[datalog]. }
@defform[(datalog thy-expr
stmt ...)
#:contracts ([thy-expr mutable-theory/c])]{ Executes the statements on the theory given by @racket[thy-expr]. Returns the answers to the final query as a list of S-expressions or returns @racket[empty]. }
#: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 mutable-theory/c])]{ Executes the statements on the theory given by @racket[thy-expr]. Prints the answers to every query in the list of statements. Returns @racket[(void)]. }
#: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.

2
collects/datalog/sexp/lang.rkt
View File

@ -33,7 +33,7 @@
(define theory (make-theory))
(datalog! theory stmt ...)
(provide/contract
[theory mutable-theory/c]))))]))
[theory theory/c]))))]))
(define-syntax (top-interaction stx)
(syntax-case stx ()

52
collects/datalog/stx.rkt
View File

@ -12,12 +12,9 @@
(define-syntax (? stx)
(raise-syntax-error '? "only allowed inside datalog" stx))
(define ->answer
(match-lambda
[(? void?)
empty]
[(? list? ls)
(map literal->sexp ls)]))
(define (->substitutions sel ls)
(if (void? ls) empty
(map sel ls)))
(define literal->sexp
(match-lambda
@ -38,7 +35,9 @@
[(_ thy-expr stmt ...)
(syntax/loc stx
(parameterize ([current-theory thy-expr])
(->answer (eval-statement (datalog-stmt stmt)))
(->substitutions
(datalog-stmt-var-selector stmt)
(eval-statement (datalog-stmt stmt)))
...))]))
(define-syntax (datalog! stx)
@ -63,6 +62,17 @@
(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
@ -93,6 +103,34 @@
(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

48
collects/tests/datalog/racket.rkt
View File

@ -14,19 +14,19 @@
(datalog parent
(? (parent X joseph2)))
=>
(list '(parent joseph3 joseph2))
(list (hasheq 'X 'joseph3))
(datalog parent
(? (parent joseph2 X)))
=>
(list '(parent joseph2 joseph1)
'(parent joseph2 lucy))
(list (hasheq 'X 'joseph1)
(hasheq 'X 'lucy))
(datalog parent
(? (parent joseph2 X))
(? (parent X joseph2)))
=>
(list '(parent joseph3 joseph2))
(list (hasheq 'X 'joseph3))
(datalog parent
(! (:- (ancestor A B)
@ -41,44 +41,44 @@
(datalog parent
(? (ancestor A B)))
=>
(list '(ancestor joseph3 joseph2)
'(ancestor joseph2 lucy)
'(ancestor joseph2 joseph1)
'(ancestor joseph3 lucy)
'(ancestor joseph3 joseph1))
(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 '(parent joseph2 joseph1)
'(parent joseph2 lucy))
(list (hasheq 'X 'joseph1)
(hasheq 'X 'lucy))
(datalog parent
(? (add1 1 :- X)))
=>
(list '(add1 1 :- 2))
(list (hasheq 'X 2))
(local [(local-require tests/datalog/examples/ancestor)]
(datalog theory
(? (ancestor A B))))
=>
'((ancestor ebbon bob)
(ancestor bob john)
(ancestor john douglas)
(ancestor bob douglas)
(ancestor ebbon john)
(ancestor ebbon douglas))
(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))))
=>
'((ancestor ebbon bob)
(ancestor bob john)
(ancestor john douglas)
(ancestor bob douglas)
(ancestor ebbon john)
(ancestor ebbon douglas))
(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))
)

17
collects/tests/datalog/runtime.rkt
View File

@ -20,31 +20,22 @@
(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
"imm simple"
(test-equal? "empty" (prove (make-immutable-theory) pl) empty)
(test-literal "ass->prov"
(first (prove (assume (make-immutable-theory) pc) pl))
pl)
(test-equal? "ass->ret->prov" (prove (retract (assume (make-immutable-theory) pc) pc) pl) empty)
(test-equal? "ret->prov" (prove (retract (make-immutable-theory) pc) pl) empty))
(test-suite
"mut simple"
(test-equal? "empty" (prove (make-mutable-theory) pl) empty)
(test-equal? "empty" (prove (make-theory) pl) empty)
(test-literal "ass->prov"
(let ([thy (make-mutable-theory)])
(let ([thy (make-theory)])
(assume! thy pc)
(first (prove thy pl)))
pl)
(test-equal? "ass->ret->prov"
(let ([thy (make-mutable-theory)])
(let ([thy (make-theory)])
(assume! thy pc)
(retract! thy pc)
(prove thy pl))
empty)
(test-equal? "ret->prov"
(let ([thy (make-mutable-theory)])
(let ([thy (make-theory)])
(retract! thy pc)
(prove thy pl))
empty))