diff --git a/collects/datalog/eval.rkt b/collects/datalog/eval.rkt index ac1e51f5fa..2bea9d00a8 100644 --- a/collects/datalog/eval.rkt +++ b/collects/datalog/eval.rkt @@ -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)]) \ No newline at end of file + [eval-statement (statement/c . -> . (or/c void (listof question/c)))]) \ No newline at end of file diff --git a/collects/datalog/main.rkt b/collects/datalog/main.rkt index c693521685..4aad39a3c3 100644 --- a/collects/datalog/main.rkt +++ b/collects/datalog/main.rkt @@ -2,5 +2,5 @@ (require "runtime.rkt" "stx.rkt") (provide make-theory - mutable-theory/c + theory/c (all-from-out "stx.rkt")) \ No newline at end of file diff --git a/collects/datalog/runtime.rkt b/collects/datalog/runtime.rkt index f0715fdb25..481d1c8786 100644 --- a/collects/datalog/runtime.rkt +++ b/collects/datalog/runtime.rkt @@ -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))]) \ No newline at end of file diff --git a/collects/datalog/scribblings/racket.scrbl b/collects/datalog/scribblings/racket.scrbl index f4e3ed4420..b0d2677f03 100644 --- a/collects/datalog/scribblings/racket.scrbl +++ b/collects/datalog/scribblings/racket.scrbl @@ -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. diff --git a/collects/datalog/sexp/lang.rkt b/collects/datalog/sexp/lang.rkt index 32a692b766..c62dc79da7 100644 --- a/collects/datalog/sexp/lang.rkt +++ b/collects/datalog/sexp/lang.rkt @@ -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 () diff --git a/collects/datalog/stx.rkt b/collects/datalog/stx.rkt index fdff1396e3..ddc0d354bb 100644 --- a/collects/datalog/stx.rkt +++ b/collects/datalog/stx.rkt @@ -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 diff --git a/collects/tests/datalog/racket.rkt b/collects/tests/datalog/racket.rkt index a2536584d6..f0b78e5877 100644 --- a/collects/tests/datalog/racket.rkt +++ b/collects/tests/datalog/racket.rkt @@ -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)) ) \ No newline at end of file diff --git a/collects/tests/datalog/runtime.rkt b/collects/tests/datalog/runtime.rkt index 202f8ffac6..d68fcdc820 100644 --- a/collects/tests/datalog/runtime.rkt +++ b/collects/tests/datalog/runtime.rkt @@ -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))