;; hilog.ss

(load "newtry.ss")

(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 *rule-list* '())
(define reset-rules! (lambda () (set! *rule-list* '())))

(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 empty-substitution
  (lambda (sym)
    '<dead-end>))

(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) empty-substitution)))
	   (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 (substitution x)))
         (if (eq? '<dead-end> value-x)
	   (if (logic-variable? y)
	     (let ((value-y (substitution y)))
	       (let ((y (if (eq? '<dead-end> value-y) y value-y)))
		 (lambda (sym)
		   (if (eq? sym x) y (substitution sym)))))
	     (lambda (sym)
	       (if (eq? sym x) y (substitution sym))))
	   (unify y value-x substitution))))
      ((logic-variable? y) (unify y x substitution))
      ((and (pair? x) (pair? y))
       (let ((new-substitution (unify (car x) (car y) substitution)))
         (if new-substitution (unify (cdr x) (cdr y) new-substitution) #f)))
      (else #f))))

(define substitute
  (lambda (exp substitution)
    (cond
      ((logic-variable? exp)
       (let ((value (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)))))

;;;----------------------------- User's language ----------------------

(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-substitution
	       (unify `arg
		 (let ((var (substitute var substitution)) ...)
		   exp1)
		 substitution)))
	 (or new-substitution (fail))))]))

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

;;; ------------------------------------ End User's Language