(use srfi-1) ; fold

;; helpers and different kinds of propositions

(define (conjunction? form) (tagged? form 'and))

(define (conjuncts form)
  (if (conjunction? form) (cdr form) (list form)))

(define (verum? form)
  (and (conjunction? form) (null? (conjuncts form))))

(define (conjunction . args)
  (list->conjunction args))

(define (list->conjunction ls)
  (let ((conjs (append-map conjuncts ls)))
    (if (and (pair? conjs) (null? (cdr conjs))) (car conjs)
      (cons 'and conjs))))

(define (disjunction? form) (tagged? form 'or))

(define (disjuncts form)
  (if (disjunction? form) (cdr form) (list form)))

(define (falsum? form)
  (and (disjunction? form) (null? (disjuncts form))))

(define (disjunction . args)
  (list->disjunction args))

(define (list->disjunction ls)
  (let ((disjs (append-map disjuncts ls)))
    (if (and (pair? disjs) (null? (cdr disjs))) (car disjs)
      (cons 'or disjs))))

(define (negated? form) (tagged? form 'not))

(define (negated form)
  (cond ((negated? form) (cadr form))
	((verum? form) '(or))
	((falsum? form) '(and))
	(else `(not ,form))))

(define (atomic? form)
  (cond ((negated? form) (atomic? (negated form)))
	((or (conjunction? form) (disjunction? form)) #f)
	(else #t)))

(define atomic-term? symbol?)

(define (connective? form)
  (memq form '(not or and)))

(define (same-heads? f1 f2)
  (if (and (negated? f1) (negated? f2))
    (same-heads? (negated f1) (negated f2))
    (and (pair? f1) (pair? f2) (equal? (car f1) (car f2))
	 (not (connective? (car f1))))))

(define (univ-quant vars form) `(forall ,vars ,form))
(define (exist-quant vars form) `(exists ,vars ,form))
(define (univ-quant? form) (tagged? form 'forall))
(define (exist-quant? form) (tagged? form 'exists))

;; rewritings

(define (skolemise/context substs deps form)
  (cond ((and (variable? form) (assoc form substs)) => cdr)
	((variable? form) (error "Unbound variable:" form))
	((univ-quant? form)
	 (let ((new-substs (map (lambda (var) (cons var (generate-variable)))
				(cadr form))))
	   (skolemise/context (append new-substs substs)
			      (append (map cdr new-substs) deps)
			      (caddr form))))
	((exist-quant? form)
	 (let ((new-substs (map (lambda (var)
				  (cons var (if (null? deps) (generate-constant)
					      (cons (generate-constant) deps))))
				(cadr form))))
	   (skolemise/context (append new-substs substs) deps (caddr form))))
	((pair? form)
	 (cons (skolemise/context substs deps (car form))
	       (skolemise/context substs deps (cdr form))))
	(else form)))

(define (skolemise form) (skolemise/context '() '() form))

(define (rewrite-shorthands form)
  (cond ((conjunction? form)
	 (list->conjunction (map rewrite-shorthands (conjuncts form))))
	((disjunction? form)
	 (list->disjunction (map rewrite-shorthands (disjuncts form))))
	((negated? form)
	 (negated (rewrite-shorthands (negated form))))
	((univ-quant? form)
	 (univ-quant (cadr form) (rewrite-shorthands (caddr form))))
	((exist-quant? form)
	 (exist-quant (cadr form) (rewrite-shorthands (caddr form))))
	((tagged? form 'implies)
	 (disjunction (rewrite-shorthands (cadr form))
		      (negated (list->conjunction
				 (map rewrite-shorthands (cddr form))))))
	((tagged? form 'equiv)
	 (let loop ((forms (map rewrite-shorthands (cdr form))))
	   (if (null? (cdr forms)) '(and)
	     (conjunction (disjunction (car forms) (negated (cadr forms)))
			  (disjunction (negated (car forms)) (cadr forms))
			  (loop (cdr forms))))))
	(else form)))

(define (atomify-negations form)
  (cond ((conjunction? form)
	 (list->conjunction (map atomify-negations (conjuncts form))))
	((disjunction? form)
	 (list->disjunction (map atomify-negations (disjuncts form))))
	((or (univ-quant? form) (exist-quant? form))
	 (list (car form) (cadr form) (atomify-negations (caddr form))))
	((and (negated? form) (conjunction? (negated form)))
	 (list->disjunction (map atomify-negations
				 (map negated (conjuncts (negated form))))))
	((and (negated? form) (disjunction? (negated form)))
	 (list->conjunction (map atomify-negations
				 (map negated (disjuncts (negated form))))))
	((and (negated? form) (univ-quant? (negated form)))
	 (exist-quant (cadr (negated form))
		      (atomify-negations (negated (caddr (negated form))))))
	((and (negated? form) (exist-quant? (negated form)))
	 (univ-quant (cadr (negated form))
		     (atomify-negations (negated (caddr (negated form))))))
	(else form)))

(define (raise-conjunctions form)
  (cond ((conjunction? form)
	 (list->conjunction (map raise-conjunctions (conjuncts form))))
	((disjunction? form)
	 (let combine ((branches (map raise-conjunctions (disjuncts form))))
	   (if (null? branches) '(or)
	     (let ((current (car branches))
		   (rest (combine (cdr branches))))
	       (cond ((conjunction? current)
		      (list->conjunction
			(map (lambda (conjunct)
			       (raise-conjunctions
				 (disjunction conjunct rest)))
			     (conjuncts current))))
		     ((conjunction? rest)
		      (list->conjunction
			(map (lambda (conjunct)
			       (disjunction current conjunct))
			     (conjuncts rest))))
		     (else (disjunction (car branches) rest)))))))
	(else form)))

;; subsumption and simplification

(define (covers-literal? form1 form2)
  ; checks whether form1 is at least as strong as form2,
  ; variables taken literally
  (cond ((disjunction? form1)
	 (every (lambda (disjunct) (covers-literal? disjunct form2))
		(disjuncts form1)))
	((conjunction? form2)
	 (every (lambda (conjunct) (covers-literal? form1 conjunct))
		(conjuncts form2)))
	; warning: non-obvious order dependency.  Do not traverse this line.
	((conjunction? form1)
	 (any (lambda (conjunct) (covers-literal? conjunct form2))
	      (conjuncts form1)))
	((disjunction? form2)
	 (any (lambda (disjunct) (covers-literal? form1 disjunct))
	      (disjuncts form2)))
	(else (equal? form1 form2))))

(define (equivalent-literal? form1 form2)
  (and (covers-literal? form1 form2) (covers-literal? form2 form1)))

(define (clause-covers/binds binds form1 form2)
  ; checks whether form1 theta-subsumes form2.
  ; this is a great example of indeterminism :)
  (cond ((disjunction? form1)
	 (fold
	   (lambda (form bindss)
	     (append-map
	       (lambda (binds) (clause-covers/binds binds form form2))
	       bindss))
	   (list binds)
	   (disjuncts form1)))
	((disjunction? form2)
	 (append-map (lambda (form) (clause-covers/binds binds form1 form))
		     (disjuncts form2)))
	((verum? form2) (list binds))
	((verum? form1) '())
	((and (negated? form1) (not (negated? form2))) '())
	((and (not (negated? form1)) (negated? form2)) '())
	((generalises/binds binds form1 form2) => list)
	(else '())))

(define (clause-covers? form1 form2)
  (not (null? (clause-covers/binds '() form1 form2))))

(define (clause-equivalent? form1 form2)
  (and (clause-covers? form1 form2)
       (clause-covers? form2 form1)))

(define (impossible-together? form1 form2)
  (cond ((equal? form1 (negated form2)) #t)
	((disjunction? form1)
	 (every (lambda (disjunct) (impossible-together? disjunct form2))
		(disjuncts form1)))
	((conjunction? form1)
	 (any (lambda (conjunct) (impossible-together? conjunct form2))
	      (conjuncts form1)))
	((or (disjunction? form2) (conjunction? form2))
	 (impossible-together? form2 form1))
	(else #f)))

(define (trivial-alternatively? form1 form2)
  (cond ((equal? form1 (negated form2)) #t)
	((disjunction? form1)
	 (any (lambda (disjunct) (trivial-alternatively? disjunct form2))
	      (disjuncts form1)))
	((conjunction? form1)
	 (every (lambda (conjunct) (trivial-alternatively? conjunct form2))
		(conjuncts form1)))
	((or (disjunction? form2) (conjunction? form2))
	 (trivial-alternatively? form2 form1))
	(else #f)))

(define (clean-covered form)
  (cond ((conjunction? form)
	 (if (impossible-together? form form) '(or)
	   (list->conjunction
	     (cleanup-by-partial-order
	       covers-literal? (map clean-covered (conjuncts form))))))
	((disjunction? form)
	 (if (trivial-alternatively? form form) '(and)
	   (list->disjunction
	     (cleanup-by-partial-order
	       covers-literal? (map clean-covered (disjuncts form))))))
	(else form)))

;; putting all rewrites together

(define (into-cnf form)
  (clean-covered
    (raise-conjunctions
      (atomify-negations form))))

(define (traditional-fol->cnf form)
  (clean-covered
    (raise-conjunctions
      (skolemise
	(atomify-negations
	  (rewrite-shorthands form))))))

(define (proposition-negated clause)
  (into-cnf (negated (rewrite-variables-into-constants clause))))