;; hilog.ss

(load "newtry.ss")

(define *rule-list* '())
(define reset-rules! (lambda () (set! *rule-list* '())))

(define make-rule  (lambda (a b c) (cons a (cons b c))))
(define rule->vars car)
(define rule->head cadr)
(define rule->tail cddr)

(define-syntax make-term
  (let ((ops-list '(conj disj neg cut! is scheme)))
    (lambda (x)
      (syntax-case x ()
	[(_ (name rest ...))
	 (memq (syntax-object->datum (syntax name)) ops-list)
	 (syntax (name rest ...))]	
	[(_ (functor arg ...))
	 (syntax
	   (lambda (substitution)
	     (let ((r (instantiate-rule	(choose *rule-list*))))
	       (let ((new-sub (unify `(functor arg ...) (car r) substitution)))
		 (if new-sub ((cdr r) new-sub) (fail))))))]))))

(define-syntax composer
  (syntax-rules ()
    [(_ base) base]
    [(_ base c0 c1 ...) (composer (c0 base) c1 ...)]))

(define-syntax conj
  (syntax-rules ()
    [(_ cl1 ...)
     (lambda (substitution)
       (composer substitution (make-term cl1) ...))]))

(define-syntax <-
  (syntax-rules ()
    [(<- (var ...) (functor arg ...) ant  ...)
     (set! *rule-list*
       (append *rule-list*
	 (list
	   (make-rule '(var ...) (lambda (var ...) `(functor arg ...))
	     (lambda (var ...) (conj ant ...))))))]))

(define instantiate-rule
  (lambda (r)
    (let ((logic-vars
	    (map
	      (lambda (v)
		(symbol->logic-variable (gensym)))
	      (rule->vars r))))
      (cons
	(apply (rule->head r) logic-vars)
	(apply (rule->tail r) logic-vars)))))

(define offline-mode #f) ;;; This is only for testing/debugging

(define-syntax with-inference
  (syntax-rules ()
    [(_ (logic-var ...) query b0 b1 ...)
     (begin
       (if offline-mode
	   (begin (printf "Query:~n") (pretty-print 'query) (newline)))
       (reset-paths!)
       (let ((logic-var (symbol->logic-variable (gensym))) ...)
	 (let ((new-sub ((make-term query) '())))
	   (let ((logic-var (substitute logic-var new-sub)) ... )
	     b0 b1 ... 
	     (fail)))))]))

(define unify
  (lambda (x y substitution) ; x and y are expressions.
    (cond
      ((equal? x y) substitution)
      ((logic-variable? x)
       (let ((value-x (apply-subst substitution x)))
         (if (eq? '<dead-end> value-x)
             (if (occurs? x y substitution)
	       #f
	       (cons (cons x y) substitution))
             (unify value-x y substitution))))
      ((logic-variable? y) (unify y x substitution))
      ((and (pair? x) (pair? y))
       (let ((new-sub (unify (car x) (car y) substitution)))
         (if new-sub (unify (cdr x) (cdr y) new-sub) #f)))
      (else #f))))

(define occurs?
  (lambda (log-var exp substitution)
    (letrec
      ((occurs?
	 (lambda (exp)
           (cond
             ((pair? exp)
              (or (occurs? (car exp)) (occurs? (cdr exp))))
             (else (and
		     (logic-variable? exp)
		     (or (eq? exp log-var)
		       (occurs? (apply-subst substitution exp)))))))))
      (occurs? exp))))

(define apply-subst
  (lambda (substitution var)
    (let ((p (assq var substitution)))
      (if (pair? p)
        (if (logic-variable? (cdr p))
	  (apply-subst substitution (cdr p))
	  (cdr p))
        '<dead-end>))))

(define substitute
  (lambda (exp substitution)
    (cond
      ((logic-variable? exp)
       (let ((value (apply-subst substitution exp)))
	 (if (eq? '<dead-end> value)
	   '<anything>
	   (substitute value substitution))))
      ((pair? exp)
       (cons
	 (substitute (car exp) substitution)
	 (substitute (cdr exp) substitution)))
      (else exp))))

(define logic-variable?
  (lambda (v)
    (and (symbol? v) (eq? (string-ref (symbol->string v) 0) #\?))))

(define symbol->logic-variable
  (lambda (sym)
    (string->symbol (string-append "?" (symbol->string sym)))))
;;;----------------------------------------------------------------------
(define-syntax disj
  (syntax-rules ()
    [(_ cl1 ...)
     (lambda (substitution)
       (mark)
       ((choose (list (make-term cl1) ...))
	substitution))]))

(define-syntax neg
  (syntax-rules ()
    [(_ exp)
     (lambda (substitution)
       (let ((save-paths *paths*))
	 (initialize-paths!)
	 ((choose
	    (list
	      (lambda ()
		((make-term exp) substitution)
		(set! *paths* save-paths)
		(fail))
	      (lambda ()
		(set! *paths* save-paths)
		substitution))))))]))

(define-syntax cut!
  (syntax-rules ()
    [(_) (lambda (substitution) (cut) substitution)]))	

(define-syntax is
  (syntax-rules ()
    [(_ (var ...) arg exp1)
     (lambda (substitution)
       (let ((new-sub
	       (unify `arg
		 (let ((var (substitute var substitution)) ...)
		   exp1)
		 substitution)))
	 (or new-sub (fail))))]))

(define-syntax scheme
  (syntax-rules ()
    [(_ (var ...) exp)
     (lambda (substitution)
       (let ((var (substitute var substitution)) ...)
	 (if exp substitution (fail))))]))