;schelog
;An embedding of Prolog in Scheme
;(c) Dorai Sitaram, dorai@cs.rice.edu, 1989, Rice University
;revised Feb. 1993


; 16/06/01 (felix): slightly changed for use with user-pass example.


(declare
  (unit schelog-support)
  (disable-interrupts)
  (fixnum)
  (usual-integrations) )


(include "schelog-macros")


;logic variables and their manipulation

(define schelog:*ref* "ref")

(define schelog:*unbound* '_)

(define schelog:make-ref
  ;;makes a fresh unbound ref;
  ;;unbound refs point to themselves
  (lambda opt
    (vector schelog:*ref*
      (if (null? opt) schelog:*unbound*
	(car opt)))))

(define _ schelog:make-ref)

(define schelog:ref?
  (lambda (r)
    (and (vector? r)
	 (eq? (vector-ref r 0) schelog:*ref*))))

(define schelog:deref
  (lambda (r)
    (vector-ref r 1)))

(define schelog:set-ref!
  (lambda (r v)
    (vector-set! r 1 v)))

(define schelog:unbound-ref?
  (lambda (r)
    (eq? (schelog:deref r) schelog:*unbound*)))

(define schelog:unbind-ref!
  (lambda (r)
    (schelog:set-ref! r schelog:*unbound*)))

;frozen logic vars

(define schelog:*frozen* "frozen")

(define schelog:freeze-ref
  (lambda (r)
    (schelog:make-ref (vector schelog:*frozen* r))))

(define schelog:thaw-frozen-ref
  (lambda (r)
    (vector-ref (schelog:deref r) 1)))

(define schelog:frozen-ref?
  (lambda (r)
    (let ((r2 (schelog:deref r)))
      (and (vector? r2)
	   (eq? (vector-ref r2 0) schelog:*frozen*)))))

;deref a structure completely (except the frozen ones, i.e.)

(define schelog:deref*
  (lambda (s)
    (cond ((schelog:ref? s)
	   (if (schelog:frozen-ref? s) s
	     (schelog:deref* (schelog:deref s))))
	  ((pair? s) (cons (schelog:deref* (car s))
                       (schelog:deref* (cdr s))))
	  ((vector? s)
	   (list->vector (map schelog:deref* (vector->list s))))
	  (else s))))


;the unify predicate

(define schelog:unify
  (lambda (t1 t2)
    (lambda (fk)
      (letrec
	((cleanup-n-fail
	   (lambda (s)
	     (for-each schelog:unbind-ref! s)
	     (fk 'fail)))
          (unify1
            (lambda (t1 t2 s)
              (cond ((eqv? t1 t2) s)
                ((schelog:ref? t1)
                  (cond ((schelog:unbound-ref? t1)
                          (schelog:set-ref! t1 t2)
                          (cons t1 s))
                    ((schelog:frozen-ref? t1)
                      (cond ((schelog:ref? t2)
                              (cond ((schelog:unbound-ref? t2)
                                      (schelog:set-ref! t2 t1)
                                      (cons t2 s))
                                ((schelog:frozen-ref? t2)
                                  (cleanup-n-fail s))
                                (else
                                  (unify1 t1 (schelog:deref t2) s))))
                        (else (cleanup-n-fail s))))
                    (else (unify1 (schelog:deref t1) t2 s))))
                ((schelog:ref? t2) (unify1 t2 t1 s))
                ((and (pair? t1) (pair? t2))
                  (unify1 (cdr t1) (cdr t2)
                    (unify1 (car t1) (car t2) s)))
                ((and (string? t1) (string? t2))
                  (if (string=? t1 t2) s
                    (cleanup-n-fail s)))
                ((and (vector? t1) (vector? t2))
                  (unify1 (vector->list t1)
                    (vector->list t2) s))
                (else
                  (for-each schelog:unbind-ref! s)
                  (fk 'fail))))))
	(let ((s (unify1 t1 t2 '())))
	  (lambda (d)
	    (cleanup-n-fail s)))))))

(define %=/2 schelog:unify)


;the fail and true preds

(define %fail/0
  (lambda (fk) (fk 'fail)))

(define %true/0
  (lambda (fk) fk))


;type predicates

(define schelog:constant?
  (lambda (x)
    (cond ((schelog:ref? x)
	   (cond ((schelog:unbound-ref? x) #f)
		 ((schelog:frozen-ref? x) #t)
		 (else (schelog:constant? (schelog:deref x)))))
	  ((pair? x) #f)
	  ((vector? x) #f)
	  (else #t))))

(define schelog:compound?
  (lambda (x)
    (cond ((schelog:ref? x) (cond ((schelog:unbound-ref? x) #f)
			  ((schelog:frozen-ref? x) #f)
			  (else (schelog:compound? (schelog:deref x)))))
	  ((pair? x) #t)
	  ((vector? x) #t)
	  (else #f))))

(define %constant/1
  (lambda (x)
    (lambda (fk)
      (if (schelog:constant? x) fk (fk 'fail)))))

(define %compound/1
  (lambda (x)
    (lambda (fk)
      (if (schelog:compound? x) fk (fk 'fail)))))

;metalogical type predicates

(define schelog:var?
  (lambda (x)
    (cond ((schelog:ref? x)
	   (cond ((schelog:unbound-ref? x) #t)
		 ((schelog:frozen-ref? x) #f)
		 (else (schelog:var? (schelog:deref x)))))
	  ((pair? x) (or (schelog:var? (car x)) (schelog:var? (cdr x))))
	  ((vector? x) (schelog:var? (vector->list x)))
	  (else #f))))

(define %var/1
  (lambda (x)
    (lambda (fk) (if (schelog:var? x) fk (fk 'fail)))))

(define %nonvar/1
  (lambda (x)
    (lambda (fk) (if (schelog:var? x) (fk 'fail) fk))))

; negation of unify

(define schelog:make-negation ;basically inlined cut-fail
  (lambda (p)
    (lambda args
      (lambda (fk)
	(if (call-with-current-continuation
	      (lambda (k)
		((apply p args) (lambda (d) (k #f)))))
	    (fk 'fail)
	    fk)))))

(define %/=/2
  (schelog:make-negation %=/2))

;identical

(define schelog:ident?
  (lambda (x y)
    (cond ((schelog:ref? x)
	   (cond ((schelog:unbound-ref? x)
		  (cond ((schelog:ref? y)
			 (cond ((schelog:unbound-ref? y) (eq? x y))
			       ((schelog:frozen-ref? y) #f)
			       (else (schelog:ident? x (schelog:deref y)))))
			(else #f)))
		 ((schelog:frozen-ref? x)
		  (cond ((schelog:ref? y)
			 (cond ((schelog:unbound-ref? y) #f)
			       ((schelog:frozen-ref? y) (eq? x y))
			       (else (schelog:ident? x (schelog:deref y)))))
			(else #f)))
		 (else (schelog:ident? (schelog:deref x) y))))
	  ((pair? x)
	   (cond ((schelog:ref? y)
		  (cond ((schelog:unbound-ref? y) #f)
			((schelog:frozen-ref? y) #f)
			(else (schelog:ident? x (schelog:deref y)))))
		 ((pair? y)
		  (and (schelog:ident? (car x) (car y))
		       (schelog:ident? (cdr x) (cdr y))))
		 (else #f)))
	  ((vector? x)
	   (cond ((schelog:ref? y)
		  (cond ((schelog:unbound-ref? y) #f)
			((schelog:frozen-ref? y) #f)
			(else (schelog:ident? x (schelog:deref y)))))
		 ((vector? y)
		  (schelog:ident? (vector->list x)
		    (vector->list y)))
		 (else #f)))
	  (else
	    (cond ((schelog:ref? y)
		   (cond ((schelog:unbound-ref? y) #f)
			 ((schelog:frozen-ref? y) #f)
			 (else (schelog:ident? x (schelog:deref y)))))
		  ((pair? y) #f)
		  ((vector? y) #f)
		  (else (eqv? x y)))))))

(define %==/2
  (lambda (x y)
    (lambda (fk) (if (schelog:ident? x y) fk (fk 'fail)))))

(define %/==/2
  (lambda (x y)
    (lambda (fk) (if (schelog:ident? x y) (fk 'fail) fk))))

;variables as objects

(define schelog:freeze
  (lambda (s)
    (let ((dict '()))
      (let loop ((s s))
	(cond ((schelog:ref? s)
	       (cond ((or (schelog:unbound-ref? s) (schelog:frozen-ref? s))
		      (let ((x (assq s dict)))
			(if x (cdr x)
			    (let ((y (schelog:freeze-ref s)))
			      (set! dict (cons (cons s y) dict))
			      y))))
		     ;((schelog:frozen-ref? s) s) ;?
		     (else (loop (schelog:deref s)))))
	      ((pair? s) (cons (loop (car s)) (loop (cdr s))))
	      ((vector? s)
	       (list->vector (map loop (vector->list s))))
	      (else s))))))

(define schelog:melt
  (lambda (f)
    (cond ((schelog:ref? f)
	   (cond ((schelog:unbound-ref? f) f)
		 ((schelog:frozen-ref? f) (schelog:thaw-frozen-ref f))
		 (else (schelog:melt (schelog:deref f)))))
	  ((pair? f)
	   (cons (schelog:melt (car f)) (schelog:melt (cdr f))))
	  ((vector? f)
	   (list->vector (map schelog:melt (vector->list f))))
	  (else f))))

(define schelog:melt-new
  (lambda (f)
    (let ((dict '()))
      (let loop ((f f))
	(cond ((schelog:ref? f)
	       (cond ((schelog:unbound-ref? f) f)
		     ((schelog:frozen-ref? f)
		      (let ((x (assq f dict)))
			(if x (cdr x)
			    (let ((y (schelog:make-ref)))
			      (set! dict (cons (cons f y) dict))
			      y))))
		     (else (loop (schelog:deref f)))))
	      ((pair? f) (cons (loop (car f)) (loop (cdr f))))
	      ((vector? f)
	       (list->vector (map loop (vector->list f))))
	      (else f))))))

(define schelog:copy
  (lambda (s)
    (schelog:melt-new (schelog:freeze s))))

(define %freeze
  (lambda (s f)
    (lambda (fk)
      ((%= (schelog:freeze s) f) fk))))

(define %melt
  (lambda (f s)
    (lambda (fk)
      ((%= (schelog:melt f) s) fk))))

(define %melt-new
  (lambda (f s)
    (lambda (fk)
      ((%= (schelog:melt-new f) s) fk))))

(define %copy
  (lambda (s c)
    (lambda (fk)
      ((%=/2 (schelog:copy s) c) fk))))

;negation as failure

(define %not/1
  (lambda (g)
    (lambda (fk)
      (if (call-with-current-continuation
	    (lambda (k)
	      ((schelog:deref* g) (lambda (d) (k #f)))))
	  (fk 'fail) fk))))



;defining arithmetic comparison operators

(define schelog:make-binary-arithmetic-relation
  (lambda (f)
    (lambda (x y)
      (%is/2 #t (f x y)))))

(define %=:=/2 (schelog:make-binary-arithmetic-relation =))
(define %>/2 (schelog:make-binary-arithmetic-relation >))
(define %>=/2 (schelog:make-binary-arithmetic-relation >=))
(define %</2 (schelog:make-binary-arithmetic-relation <))
(define %<=/2 (schelog:make-binary-arithmetic-relation <=))
(define %=/=/2 (schelog:make-binary-arithmetic-relation
               (lambda (m n) (not (= m n)))))


;assert, asserta

(define %empty-rel
  (lambda args
    %fail/0))


;set predicates

(define schelog:separate-bags
  (lambda (fvv bag acc)
    ;;(format #t "Accum: ~s~%" acc)
    (let ((bags (let loop ((acc acc)
                            (current-fvv #f) (current-bag '())
                            (bags '()))
                  (if (null? acc)
                    (cons (cons current-fvv current-bag) bags)
                    (let ((x (car acc)))
                      (let ((x-fvv (car x)) (x-lv (cdr x)))
                        (if (or (not current-fvv) (equal? x-fvv current-fvv))
                          (loop (cdr acc) x-fvv (cons x-lv current-bag) bags)
                          (loop (cdr acc) x-fvv (list x-lv)
                            (cons (cons current-fvv current-bag) bags)))))))))
      ;;(format #t "Bags: ~a~%" bags)
      (if (null? bags) (%=/2 bag '())
        (let ((fvv-bag (cons fvv bag)))
          (let loop ((bags bags))
            (if (null? bags) %fail/0
              (%or (%=/2 fvv-bag (car bags))
                (loop (cdr bags))))))))))

;%bag-of-1, %set-of-1 hold if there's at least one solution

(define %bag-of-1
  (lambda (x g b)
    (%and (%bag-of x g b)
      (%=/2 b (cons (_) (_))))))

(define %set-of-1
  (lambda (x g s)
    (%and (%set-of x g s)
      (%=/2 s (cons (_) (_))))))

(define schelog:set-cons
  (lambda (e s)
    (if (member e s) s (cons e s))))

(define schelog:goal-with-free-vars?
  (lambda (x)
    (and (pair? x) (eq? (car x) 'schelog:goal-with-free-vars))))

(define schelog:make-bag-of
  (lambda (kons)
    (lambda (lv goal bag)
      (let ((fvv '()))
        (if (schelog:goal-with-free-vars? goal)
          (begin (set! fvv (cadr goal))
            (set! goal (cddr goal))))
        (schelog:make-bag-of-aux kons fvv lv goal bag)))))

(define schelog:make-bag-of-aux
  (lambda (kons fvv lv goal bag)
    (lambda (fk)
      (call-with-current-continuation
       (lambda (sk)
	 (let ((lv2 (cons fvv lv)))
	   (let* ((acc '())
		  (fk-final
		   (lambda (d)
		     ;;(set! acc (reverse! acc))
		     (sk ((schelog:separate-bags fvv bag acc) fk))))
		  (fk-retry (goal fk-final)))
	     (set! acc (kons (schelog:deref* lv2) acc))
	     (fk-retry 'retry))))))))

(define %bag-of/3 (schelog:make-bag-of cons))
(define %set-of/3 (schelog:make-bag-of schelog:set-cons))

(define schelog:*more-k* 'forward)
(define schelog:*more-fk* 'forward)

(define %more
  (lambda ()
    (call-with-current-continuation
     (lambda (k)
       (set! schelog:*more-k* k)
       (if schelog:*more-fk* (schelog:*more-fk* 'more)
	   #f)))))

(define == %=/2)
(define %notunify %/=/2)
(define %ident %==/2)
(define %notident %/==/2)

(define more %more)

;end of embedding code.  The following are
;some utilities, written in Schelog

(define %member/2
  (lambda (x y)
    (%let (xs z zs)
      (%or
	(%= y (cons x xs))
	(%and (%= y (cons z zs))
	  (%member x zs))))))

(define %if-then-else/3
  (lambda (p q r)
    (%cut-delimiter
      (%or
	(%and p ! q)
	r))))

;the above could also have been written in a more
;Prolog-like fashion, viz.

'(define %member
  (%rel (x xs y ys)
    ((x (cons x xs)))
    ((x (cons y ys)) (%member x ys))))

'(define %if-then-else
  (%rel (p q r)
    ((p q r) p ! q)
    ((p q r) r)))

(define %append/3
  (%rel (x xs ys zs)
    (('() ys ys))
    (((cons x xs) ys (cons x zs))
      (%append xs ys zs))))

(define %repeat/0
  ;;failure-driven loop
  (%rel ()
    (())
    (() (%repeat))))

(define %eq %=:=/2)
(define %gt %>/2)
(define %ge %>=/2)
(define %lt %</2)
(define %le %<=/2)
(define %ne %=/=/2)


;;; So "is" works:

(define %-/2 -)
(define %+/2 +)
(define %mod/2 modulo)
(define %div/2 quotient)

(define (%repeat-query thunk)
  (let ([r (thunk)])
    (cond [(not r) (display "no\n")]
	  [else
	   (for-each
	    (lambda (s)
	      (display (car s))
	      (display " = ")
	      (write (cadr s))
	      (newline) ) 
	    r)
	   (display "yes\n") ] ) ) )
