#lang scheme
(require "ast.ss"
"private/env.ss"
"private/subst.ss"
"private/unify.ss"
"private/variant.ss")
(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))
(literal-terms l)))
(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 (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)
(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
(literal
[facts #:mutable]
[waiters #:mutable]))
(define (resolve c lit)
(define body (clause-body c))
(and (not (empty? body))
(cond
[(unify (first body) (rename-literal lit))
=> (lambda (env)
(subst-clause env (make-clause (clause-srcloc c) (clause-head c) (rest body))))]
[else #f])))
(define (prove thy lit)
(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-literal sg) selected)
=> (lambda (env)
(add-clause! sg (subst-clause env renamed)))]))
(get thy (subgoal-literal sg))))
(define (search! sg)
(match (subgoal-literal sg)
[(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 lit empty empty))
(literal-tbl-replace! subgoals lit sg)
(search! sg)
(subgoal-facts sg))
(provide/contract
[safe-clause? (clause? . -> . boolean?)]
[theory/c contract?]
[immutable-theory/c contract?]
[mutable-theory/c contract?]
[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)]
[prove (theory/c literal? . -> . (listof literal?))])