(use srfi-1) ; append-map, filter, remove, delete-duplicates
(use srfi-11) ; let-values

;; unifiable terms
; XXX not currently used (leads to combinatory explosions)

(define (unifiable-subterms term1 term2) ; XXX check this logic
  (append
    (if (same-heads? term1 term2)
      (cons (list term1 term2) (map list (cdr term1) (cdr term2))) '())
    (if (pair? term1)
      (append-map (lambda (term) (unifiable-subterms term term2)) (cdr term1))
      '())
    (if (pair? term2)
      (append-map (lambda (term) (unifiable-subterms term1 term)) (cdr term2))
      '())))

(define (atomic-formula-unifiable-subterms form1 form2)
  (append
    (if (same-heads? form1 form2) (map list (cdr form1) (cdr form2)) '())
    (append-crossmap unifiable-subterms (cdr form1) (cdr form2))))

(define (unifiable-terms form1 form2)
  (cond ((conjunction? form1)
	 (append-map (lambda (form) (unifiable-terms form form2))
		     (conjuncts form1)))
	((disjunction? form1)
	 (append-map (lambda (form) (unifiable-terms form form2))
		     (disjuncts form1)))
	((conjunction? form2)
	 (append-map (lambda (form) (unifiable-terms form1 form))
		     (conjuncts form2)))
	((disjunction? form2)
	 (append-map (lambda (form) (unifiable-terms form1 form))
		     (disjuncts form2)))
	((negated? form1) (unifiable-terms (negated form1) form2))
	((negated? form2) (unifiable-terms form1 (negated form2)))
	((and (pair? form1) (pair? form2))
	 (atomic-formula-unifiable-subterms form1 form2))
	(else '())))

(define (unifiable-term-classes theory1 theory2)
  (equivalence-classes (append-crossmap unifiable-terms theory1 theory2)))

;; rule forming

(define (cleanup-substitution-sets set1 set2)
  (let-values
    (((factual1 nf1) (partition (lambda (c) (member (negated c) set1)) set1))
     ; XXX take into account factual disjunctions -- negated is barbarian
     ((factual2 nf2) (partition (lambda (c) (member (negated c) set2)) set2)))
    (let ((filt1 (remove (lambda (c) (member c set2)) factual1))
	  ; XXX use equivalent-literal?
	  (filt2 (remove (lambda (c) (member c set1)) factual2))
	  (new-nf1 (lset-difference equivalent-literal? nf1 nf2))
	  (new-nf2 (lset-difference equivalent-literal? nf2 nf1)))
      (values (append filt1 new-nf1) (append filt2 new-nf2)))))

(define (map-atomic-formulae f form)
  (define (rec form) (map-atomic-formulae f form))
  (cond ((conjunction? form)
	 (list->conjunction (map rec (conjuncts form))))
	((disjunction? form)
	 (list->disjunction (map rec (disjuncts form))))
	((negated? form)
	 (negated (rec (negated form))))
	(else (f form))))

(define (replace-event form event)
  (map-atomic-formulae
    (lambda (form)
      (if (and (pair? form) (pair? (cdr form)))
	(cons (car form) (cons event (cddr form)))
	form))
    form))

(define (substitution-set theory event)
  (delete-duplicates
    (map (lambda (form) (replace-event form event)) theory)))

;; theory merging

(define (theory-merge theory1 theory2)
  (let* ((event (generate-constant))
	 (ss1 (substitution-set theory1 event))
	 (ss2 (substitution-set theory2 event)))
    (let-values
      (((unique1 unique2) (cleanup-substitution-sets ss1 ss2)))
      (conjuncts
	(clean-covered
	  (list->conjunction
	    (append (crossmap disjunction unique1 unique2)
		    theory1 theory2)))))))