;;; -*- Mode: Lisp; Package: Prolog; Base: 10.; Options: ((World Compatibility)); -*-
;;; (C) Copyright 1983,1984,1985, Uppsala University

;;This defines predicates in LM-Prolog for use in the Dec-10 Prolog compatibility package 

(define-predicate asserta
  (:options (:argument-list (clause))
	    (:documentation "asserts CLAUSE in front of other clauses."))
  ((asserta ?clause)
   (clause-predicator ?predicator ?clause)
   (define-predicate ?predicator
     :(options (type dynamic)
	       (if-old-definition keep)
	       (place-clauses before))
     ?clause)))

(define-predicate assertz
  (:options (:argument-list (clause))
	    (:documentation "asserts CLAUSE behind other clauses."))
  ((assertz ?clause)
   (clause-predicator ?predicator ?clause)
   (define-predicate ?predicator
     :(options (type dynamic)
	       (if-old-definition keep)
	       (place-clauses after))
     ?clause)))

(define-predicate exploden
  (:options (:argument-list (asciis symbol))
	    (:documentation "converts between a symbol and a list of ASCII codes."))
  ((exploden ?asciis ?symbol)
   (cases ((not-variable ?symbol)
	   (lisp-value ?asciis (exploden '?symbol) :dont-invoke))
	  ((not-variable ?asciis)
	   (lisp-value ?symbol (implode '?asciis) :dont-invoke))
	  ((error :exploden-of-two-variables
		  "can't exploden ~n and ~n" ?asciis ?symbol)))))

(define-predicate compare
  (:options (:argument-list (relation x y))
	    (:documentation "depending on the outcome of comparing X and Y, RELATION is <, =, or >."))
  ((compare ?op ?x ?y)
   (lisp-value ?signum (prolog-compare '?x '?y) :dont-invoke)
   (rules (?signum ?op) ((-1 <)) ((0 =)) ((+1 >)))))

(define-predicate standard-order
  (:options (:argument-list (x y))
	    (:documentation "succeeds unless Y is before X in the standard order"))
  ((standard-order ?x ?y)
   (lisp-value ?signum (prolog-compare '?x '?y) :dont-invoke)
   (< ?signum +1)))

(define-predicate quantified-bag-of
  (:options (:argument-list (bag +outer term &rest predications))
	    (:documentation
	      "For some values of the variables in OUTER, this unifies BAG 
with instantiations of TERM corresponding to solutions of PREDICATIONS.")
	    (:deterministic :sometimes)))

(define-predicate quantified-set-of
  (:options (:argument-list (set +outer term &rest predications))
	    (:documentation
	      "For some values of the variables in OUTER, this unifies SET
with sorted, unique instantiations of TERM such that PREDICATIONS hold.")
	    (:deterministic :sometimes)))

;;I am too lazy to write intrinsics for these, therefore we redefine the provers:

(defun #.(prolog-db-symbol 'quantified-bag-of ':compatibility 'prover)
       (continuation bag outer term &rest predications)
  (let ((mark *trail*) collection)
    (prove-conjunction-if-need-be
      predications
      (faked-continuation (funcall #'collection-insert 'nil (locf collection) outer term)))
    (untrail mark)
    (collection-traverse
      mark continuation (%dereference bag) (%dereference outer) collection)))

(defun #.(prolog-db-symbol 'quantified-set-of ':compatibility 'prover)
       (continuation set outer term &rest predications)
  (let ((mark *trail*) collection)
    (prove-conjunction-if-need-be
      predications
      (faked-continuation (funcall #'collection-insert 't (locf collection) outer term)))
    (untrail mark)
    (collection-traverse
      mark continuation (%dereference set) (%dereference outer) collection)))

;;We will build a data structure
;;  ((,outer-instance ,term-instance ,term-instance ...)
;;   (,outer-instance ,term-instance ,term-instance ...)
;;   ...)
;;sorted on increasing CARs. Each CDR is either the reverse list of solutions (for bags)
;;or unique solutions in decreasing order (for sets).
(defun collection-insert (set-p location outer term)
  (collection-insert-1 set-p location
		       (copy-term (%dereference outer))
		       (copy-term (%dereference term)))
  nil);;force it to backtrack

(deffun collection-insert-1 (set-p location outer term)
  (cond ((null (contents location))
	 (setf (contents location)
	       (prolog-list* (prolog-list* outer term nil) nil)))
	(t (let ((signum (prolog-compare outer (caar (contents location)))))
	     (selectq signum
	       (-1 (push-in-area *prolog-work-area*
				 (prolog-list* outer term nil)
				 (contents location)))
	       (0  (cond (set-p (collection-insert-term
				 (locf (cdar (contents location))) term))
			 (t (push-in-area *prolog-work-area*
					  term
					  (cdar (contents location))))))
	       (+1 (collection-insert-1
		     set-p (locf (cdr (contents location))) outer term)))))))

(deffun collection-insert-term (location term)
  (cond ((null (contents location))
	 (setf (contents location) (prolog-list* term nil)))
	(t (let ((signum (prolog-compare term (car (contents location)))))
	     (selectq signum
	       (-1 (collection-insert-term (locf (cdr (contents location))) term))
	       (0)
	       (+1 (push-in-area *prolog-work-area* term (contents location))))))))

(deffun collection-traverse (mark continuation bag outer collection)
  (cond (collection
	 (cond ((and (unify outer (caar collection))
		     (unify bag (nreverse (cdar collection)))
		     (invoke continuation)))
	       ((untrail mark))
	       ((collection-traverse mark continuation bag outer (cdr collection)))))))

;;Pretty slow versions:
;;(define-predicate quantified-bag-of
;;  ((quantified-bag-of ?bag ?outer ?term . ?predicates)
;;   (set-of ?all (?outer ?term) . ?predicates)
;;   (unique-member-first ?whats-left ?outer ?all)
;;   (bag-of ?bag ?x (member (?outer ?x) ?whats-left))))
;;
;;(define-predicate quantified-set-of
;;  ((quantified-set-of ?sorted-set ?outer ?term . ?predicates)
;;   (set-of ?all (?outer ?term) . ?predicates)
;;   (unique-member-first ?whats-left ?outer ?all)
;;   (set-of ?set ?x (member (?outer ?x) ?whats-left))
;;   (sort ?sorted-set ?set standard-order)))
;;
;;(define-predicate unique-member-first
;;  ((unique-member-first ?left ?x ?list)
;;   (unique-member-first ?left ?x ?list ()))
;;  ((unique-member-first ?left ?x ((?one ?two) . ?rest) ?seen-already)
;;   (or (and (= ?x ?one)
;;	    (cannot-prove (member ?x ?seen-already))
;;	    (= ?left ((?one ?two) . ?rest)))
;;       (unique-member-first ?left ?x ?rest (?one . ?seen-already)))))

(deffun prolog-compare (x y)
  (cond ((or (and (symbolp x) (symbolp y)) (and (stringp x) (stringp y)))
	 (signum (string-compare x y)))
	((and (consp x) (consp y))
	 (let ((signum (prolog-compare (car x) (car y))))
	   (selectq signum
	     (0 (prolog-compare (cdr x) (cdr y)))
	     (otherwise signum))))
	((and (numberp x) (numberp y))
	 (signum (- x y)))
	((and (value-cell-p x) (not (value-cell-p y)))
	 -1)
	((and (value-cell-p y) (not (value-cell-p x)))
	 +1)
	(t (let ((signum (signum (string-compare (typep x) (typep y)))))
	     (selectq signum
	       (0 (signum (%pointer-difference x y)))
	       (otherwise signum))))))