;; Unify.lisp: Orig:pazzani@ics.uci.edu, port:wdavies@cs.stanford.edu (define *success* '((#t / #t))) ;; (define (append-bds new old) (cond ((null? new) '()) ((null? old) '()) ((eq? new *success*) old) ((eq? old *success*) new) (else (append new old)))) ;; (define (variable? a) (and (symbol? a) (let ((first (string-ref (object->string a) 0))) (or (eq? first #\?) (eq? first #\G))))) ;; (define (constant? a) (and (not (pair? a)) (not (variable? a)))) ;; (define (contains tree item) (cond ((null? tree) #f) ((not (pair? tree)) (equal? tree item)) (else (or (contains (car tree) item) (contains (cdr tree) item))))) ;;; (define (subst new old subtree ) (cond ((equal? old subtree) new) ((not (pair? subtree)) subtree) (else (cons (subst new old (car subtree)) (subst new old (cdr subtree)))))) ;; (define (apply-substitution substs expr) (let ((c expr)) (map (lambda(s) (set! c (subst (car s) (caddr s) c))) substs) c)) ;; (define (unify l1 l2) (cond ((or (constant? l1) (or (variable? l1) (or (constant? l2) (variable? l2)))) (cond ((eq? l1 l2) *success*) ((variable? l1) (if (contains l2 l1) '() (list (list l2 '/ l1)))) ((variable? l2) (if (contains l1 l2) '() (list (list l1 '/ l2)))) (else '()))) (else (let ((s (unify (car l1) (car l2)))) (cond ((null? s) '()) (else (set! l1 (apply-substitution s l1)) (set! l2 (apply-substitution s l2)) (append-bds s (unify (cdr l1)(cdr l2))))))))) ;; (define (find-all-vars x vars) (if (not (pair? x)) (if (and (variable? x) (not (member x vars))) (cons x vars) vars) (find-all-vars (car x) (find-all-vars (cdr x) vars)))) ;; (define *cur* 0) ;; (define (gentemp x) (gensym)) ;; (define (copy-with-unique-vars list) (let ((vars (find-all-vars list '()))(l list)) (map (lambda (v) (set! l (subst (gentemp v) v l))) vars) l)) ;;; (define (cl-head cl) (if (eq? (length cl) 1) (car cl) (cadr cl))) (define (cl-body cl) (if (and (pair? cl)(pair? (cdr cl))) (cddr cl) '())) ;; (define (prove-it goals bds rules) (letrec ((prove-1-goal (lambda (goal bds rules) (let ((res '())) (map (lambda (cl) (set! res (append res (let ((new-cl (copy-with-unique-vars cl)) (new-bds '())) (set! new-bds (unify goal (cl-head new-cl))) (if (equal? new-bds '()) '() (prove-goals (cl-body new-cl) (append-bds bds new-bds) rules)))))) rules) res))) (prove-goals (lambda (goals bds rules) (cond ((null? goals) (list bds)) (else (set! goals (apply-substitution bds goals)) (let ((res '())) (map (lambda (solution) (set! res (append res (prove-goals (cdr goals) solution rules)))) (prove-1-goal (car goals) bds rules)) res) )))) ) (prove-goals goals bds rules))) (define (prove goals rules) (let ((bds (prove-it goals *success* rules))) (if (null? bds) '() (let ((res '())) (map (lambda (b) (set! res (append res (list (apply-substitution b goals))))) bds) res)))) ;;EOF