/usr/share/racket/pkgs/datalog/runtime.rkt is in racket-common 6.7-3.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 | #lang racket/base
(require racket/contract
racket/list
racket/match
racket/function
"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)])]
[(struct literal (srcloc '!= (list a b)))
(define (equal-test a b)
(unless (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))])
|