;; 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 ((vars
	    (map
	      (lambda (v)
		(symbol->variable (gensym)))
	      (rule->vars r))))
      (cons
	(apply (rule->head r) vars)
	(apply (rule->tail r) vars)))))

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

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

(define bound?
  (lambda (var substitution)
    (letrec
      ((loop (lambda (val)
	       (cond
		 ((variable? val)
		  (cond
		    ((eq? var val) #f)
		    (else (loop (apply-subst substitution val)))))
		 (else #t)))))
      (loop (apply-subst substitution var)))))

(define extend
  (lambda (var val substitution)
    (rec f
      (lambda (value)
	(let ((new-value (apply-subst substitution value)))
	  (if (variable? new-value)
	      (if (eq? var new-value)
	          (apply-subst subst val)
	          (f new-value))
	      new-value))))))

(define empty-subst (lambda (x) x))

(define unify
  (lambda (x y substitution) ; x and y are expressions.
    (cond
      ((equal? x y) substitution)
      ((variable? x)
       (if (bound? x substitution)
	   (unify y (apply-subst substitution x) substitution)
	   (if (occurs? x y substitution)
	     #f
	     (extend x y substitution))))
      ((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 (var exp substitution) #f))

'(define occurs?
  (lambda (var exp substitution)
    (letrec
      ((loop
	 (lambda (exp)
           (cond
             ((pair? exp)
              (or (occurs? (car exp)) (occurs? (cdr exp))))
             ((variable? exp)
	      (if (eq? exp var)
		#t
		(if (bound? exp substitution)
		  (loop (apply-subst substitution exp))
		  #f)))
	     (else #f)))))
      (loop exp))))

(define apply-subst
  (lambda (substitution var)
    (substitution var)))

(define substitute
  (lambda (exp substitution)
    (cond
      ((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 variable?
  (lambda (v)
    (and (symbol? v) (eq? (string-ref (symbol->string v) 0) #\?))))

(define symbol->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))))]))