;;; Proof checking support for both propositional (pl) and first-order (fol) logic
;;; For 6.034 by Tomas Lozano-Perez, Spring 2002

(require 'common-list-functions)

;;; Propositional Logic resolution

(define (pl-neg-literal? p)
  (and (pair? p) (eq? (car p) 'not)))

(define pl-pos-literal? symbol?)

(define (pl-literal? p)
  (or (pl-pos-literal? p) (pl-neg-literal? p)))

(define (pl-opposite-literal p)
  (cond ((pl-pos-literal? p) `(not ,p))
	((pl-neg-literal? p)
	 (cadr p))
	(else (error "This is not a literal - so cannot get opposite:" p))))

(define (pl-all-resolvents clause1 clause2)
  (define (disjunction formula)
    (cond ((null? formula) '())
	  ((> (length formula) 1) (cons 'or formula))
	  (else (car formula))))
  (define (normalize formula)
    (cond ((pl-literal? formula) `(or ,formula))
	  ;; These clauses have to be sets for binary resolution to be complete.
	  ((eq? (car formula) 'or) (rem-duplicates formula equal?))
	  (else formula)))
  (let ((c1 (normalize clause1))
	(c2 (normalize clause2)))
    (cond ((and (pair? c1) (eq? (car c1) 'or) 
		(pair? c2) (eq? (car c2) 'or))
	   ;; could return () meaning no resolvents
	   (let ((c1d (cdr c1))		; remove 'or
		 (c2d (cdr c2)))
	     (apply append
		    (map (lambda (p) 
			   (if (and (pl-neg-literal? p) 
				    (member (pl-opposite-literal p) c2d))
			       ;; resolution rule
			       (list (disjunction (append (remove p c1d)
							  (remove (pl-opposite-literal p) c2d))))
			       '()))
			 c1d))))
	  (else
	   ;; Ill formed sentences. Unfortunately, error messages from comparison
	   ;; functions, don't do too well.  So, just return no answer.
	   '()
	   ))))

;;; First Order Logic Resolution

(define *logical-connectives* '(and or not => <=>))
(define *logical-quantifiers* '(all exi))

(define (op f) (and (pair? f) (car f)))
(define (args f) (and (pair? f) (cdr f)))
(define (arg1 f) (and (pair? f) (cadr f)))

(define (fol-atomic? sentence)
  (not (or (member (op sentence) *logical-connectives*)
	   (member (op sentence) *logical-quantifiers*))))

(define (fol-literal? sentence)
  (or (fol-atomic? sentence)
      (and (eq? (op sentence) 'not) (fol-atomic? (arg1 sentence)))))

(define (fol-neg-literal? sentence)
  (eq? (op sentence) 'not))

(define fol-pos-literal? fol-atomic?)

(define (fol-all-resolvents clause1 clause2)
  (define (disjunction formula)
    (cond ((null? formula) '())
	  ((> (length formula) 1) (cons 'or formula))
	  (else (car formula))))
  (define (normalize formula)
    (rename-variables			; standardize apart
     (cond ((fol-literal? formula) `(or ,formula))
	   ;; Could really do factoring here...but we're doing factoring separately
	   ((eq? (car formula) 'or) (rem-duplicates formula equal?))
	   (else formula))))
  (let ((c1 (normalize clause1))
	(c2 (normalize clause2)))
    ;;(print c1 c2)
    (cond ((and (eq? (op c1) 'or) 
		(eq? (op c2) 'or))
	   ;; could return () meaning no resolvents, note that a contradiction
	   ;; is ( () ).
	   (let ((c1d (args c1))	; remove 'or
		 (c2d (args c2)))
	     (map disjunction
		  (apply append
			 (if (< (length c1d) (length c2d))
			     (map (lambda (p) (fol-resolvents p c1d c2d)) c1d)
			     (map (lambda (p) (fol-resolvents p c2d c1d)) c2d))))))
	  (else
	   ;; Ill formed sentences Unfortunately, error messages from comparison
	   ;; functions, don't do too well.  So, just return no answer.
	   '()
	   ))))

(define (fol-resolvents literal1 clause1 clause2)
  ;; returns a list of resolvents involving literal1 from clause1
  (let ((clause1-no-literal (remove literal1 clause1))
	(neg1 (fol-neg-literal? literal1))
	(pos1 (fol-pos-literal? literal1)))
    (apply append
	   (map (lambda (literal2)
		  (let ((bindings
			 (cond ((and pos1 (fol-neg-literal? literal2))
				(unify literal1 (arg1 literal2)))
			       ((and neg1 (fol-pos-literal? literal2))
				(unify (arg1 literal1) literal2))
			       (else *fail*))))
		    (if (equal? bindings *fail*)
			'()
			(list (subst-bindings bindings
					      (append (remove literal1 clause1)
						      (remove literal2 clause2)))))))
		clause2))))

(define (fol-all-binary-factorings clause)
  (if (eq? (op clause) 'or)
      (let ((matches (fol-all-binary-factorings-aux (args clause))))
	;;(pretty-print matches)
	(map (lambda (match)
	       (subst-bindings (caddr match)
			       (remove (second match) clause)))
	     matches))
      '()))

(define (fol-all-binary-factorings-aux cl)
  (if (null? cl) 
      '()
      (append
       (fol-binary-factorings (car cl) (cdr cl))
       (fol-all-binary-factorings-aux (cdr cl)))))

;; returns list of (lit1 lit2 bindings)
(define (fol-binary-factorings lit x)
  (if (null? x)
      '()
      (let ((b (unify lit (car x))))
	(if (eq? b *fail*)
	    (fol-binary-factorings lit (cdr x))
	    (cons (list lit (car x) b)
		  (fol-binary-factorings lit (cdr x)))))))

(define *t:factors* #f)

(define (compare-factors l input ans)
  ;; initialize

  (let ((n *t:current-answer-name*))
    (cond ((= n 1)
	   ;; accumulate the factors
	   (set! *t:factors*
		 (map (lambda (i) (car (t:get-answer-by-name i))) l))))

    ;;(print *t:factors*)

    (and (member n l)
	 ;; Read single clause
	 (let ((in (t:string-read-safe input)))
	   (and (mem? in *t:factors* variant?) ; is it in the factor set
		;; is it different from the other axioms
		(every (lambda (i)
			 (or (not (t:get-response-string-by-name i))
			     (not (variant? in 
					    (t:string-read-safe
					     (t:get-response-string-by-name i))))))
		       (remove n l))
		))
	 )
    ))

;;; This is the generalization of equal? that we need for fol formulas
(define (variant? formula1 formula2)
  (define (lex-variant? x y bindings)
    (cond ((eq? bindings *fail*) *fail*)
	  ((equal? x y) bindings)
	  ((or (null? x) (null? y)) *fail*)
	  ((and (variable? x) (variable? y))
	   (let ((b (get-binding x bindings)))
	     (if b
		 (if (equal? (binding-val b) y) bindings *fail*)
		 (extend-bindings x y bindings))))
	  ((and (pair? x) (pair? y))
	   (lex-variant? (cdr x) (cdr y) 
			 (lex-variant? (car x) (car y) bindings)))
	  (else *fail*)))
  (lex-variant? (if (eq? (op formula1) 'or) formula1 `(or ,formula1))
		(if (eq? (op formula2) 'or) formula2 `(or ,formula2))
		*no-bindings*))
	 
;;; Checking proofs

(define *t:found-contradiction* #f)
(define *t:axioms* #f)

(define (ensure-or formula)
  (if (null? formula) formula 
      (if (eq? (car formula) 'or) formula (list 'or formula))))

(define (compare-pl-proof n-axioms input ans)
  (compare-proof n-axioms input ans
		 (lambda (x y) (set-equal? x y equal?))
		 pl-all-resolvents
		 ;; no factorings in propositional case
		 (lambda (x) '())))

(define (compare-fol-proof n-axioms input ans)
  (compare-proof n-axioms input ans
		 (lambda (x y) (set-equal? (ensure-or x) (ensure-or y) variant?))
		 fol-all-resolvents
		 fol-all-binary-factorings))

(define (compare-proof n-axioms input ans equiv-test get-resolvents get-factorings)
  ;; initialize
  (let ((n *t:current-answer-name*))
    (cond ((= n 1)
	   (set! *t:found-contradiction* #f)
	   ;; accumulate the axioms
	   (set! *t:axioms*
		 (do ((i 1 (+ i 1))
		      (ax '()))
		     ((> i n-axioms) ax)
		   (set! ax (cons (car (t:get-answer-by-name i)) ax))))))

    ;;(print *t:axioms*)

    (cond ((<= n n-axioms)
	   ;; It's an axiom, read single clause
	   (let ((in (t:string-read-safe input)))
	     (and (mem? in *t:axioms* equiv-test) ; is it in the axiom set
		  ;; is it different from the other axioms
		  (do ((i 1 (+ i 1))
		       (different #t))
		      ((or (= i n) (not different)) 
		       different)
		    (if (equiv-test in (t:string-read-safe
					(t:get-response-string-by-name i)))
			(set! different #f)))
		  ))
	   )
	  (else
	   ;; It's a proof step, first part is steps:(s1 s2) then clause
	   (let* ((in (t:string-read*-safe input))
		  (steps (t:safe-first in))
		  (clause (t:safe-second in)))
	     (define (prev-clause i)
	       (let ((response (t:get-response-string-by-name i)))
		 (if (<= i n-axioms)
		     (t:string-read-safe response)
		     (t:safe-second (t:string-read*-safe response)))))
	     (cond ((equal? in '(Done))
		    *t:found-contradiction*)
		   (else
		    ;; does it follow?
		    (cond ((and (= (length steps) 2) ; are the steps ok?
				(number? (first steps))
				(number? (second steps))
				(< 0 (first steps) n)
				(< 0 (second steps) n))
			   ;; Check clause
			   (and (let ((resolvents 
				       (get-resolvents
					(prev-clause (t:safe-first steps))
					(prev-clause (t:safe-second steps))
					)))
				  (mem? clause resolvents equiv-test))
				;; Indicate if we got valid contradiction
				(cond ((null? clause)
				       (set! *t:found-contradiction* #t) #t)
				      (else
				       #t))))
			  ((and (= (length steps) 2) ; factoring
				(eq? (first steps) 'f)
				(number? (second steps))
				(< 0 (second steps) n))
			   (let ((factorings
				  (get-factorings
				   (prev-clause (t:safe-second steps))
				   )))
			     (mem? clause factorings equiv-test))
			   )
			  )))
	     )
	   ))
    ))

(define (check-fol-proof negated-goal min-steps input ans)
  (check-proof negated-goal min-steps input ans
		 (lambda (x y) (set-equal? (ensure-or x) (ensure-or y) variant?))
		 fol-all-resolvents
		 fol-all-binary-factorings))

(define (check-proof negated-goal min-steps input ans
		     equiv-test get-resolvents get-factorings)
  ;; initialize
  (let* ((n *t:current-answer-name*)
	 (in (t:string-read*-safe input))
	 (info (t:safe-first in))
	 (clause (t:safe-second in)))
    (define (prev-clause i)
      (let ((response (t:string-read*-safe (t:get-response-string-by-name i))))
	(if (equal? (t:safe-first in) '(negated-goal))
	    negated-goal
	    (t:safe-second response))))
    (if (= n 1)
	(set! *t:found-contradiction* #f))
    (cond  ((member info '(Done (Axiom) (Negated-Goal)))
	    ;; if it all works, say yes
	    *t:found-contradiction*
	    )
	   (else
	    ;; It's a proof step, first part is steps:(s1 s2) then clause
	    (cond ((and (= (length steps) 2) ; are the steps ok?
			(number? (first steps))
			(number? (second steps))
			(< 0 (first steps) n)
			(< 0 (second steps) n))
		   ;; Check clause
		   (and (let ((resolvents 
			       (get-resolvents
				(prev-clause (t:safe-first steps))
				(prev-clause (t:safe-second steps))
				)))
			  (mem? clause resolvents equiv-test))
			;; Indicate if we got valid contradiction
			(cond ((null? clause)
			       (set! *t:found-contradiction* (> n min-steps))
			       #t)
			      (else
			       #t))))
		  ((and (= (length steps) 2) ; factoring
			(eq? (first steps) 'f)
			(number? (second steps))
			(< 0 (second steps) n))
		   (let ((factorings
			  (get-factorings
			   (prev-clause (t:safe-second steps))
			   )))
		     (mem? clause factorings equiv-test))
		   )
		  )
	    ))
    ))

(define (check-whole-fol-proof negated-goal contradiction min-steps input ans)
  (check-whole-proof negated-goal contradiction min-steps input ans
		     (lambda (x y) (set-equal? (ensure-or x) (ensure-or y) variant?))
		     fol-all-resolvents
		     fol-all-binary-factorings))

(define (check-whole-proof negated-goal contradiction min-steps input ans
			   equiv-test get-resolvents get-factorings)
  (let* ((proof (t:string-read*-safe input))
	 (parsed-proof (parse-proof proof)))
    (define (prev-clause i)
      (let ((response (assoc i parsed-proof)))
	(if (equal? (t:safe-second response) '(negated-goal))
	    negated-goal
	    (t:safe-third response))))
    (define (cl-mem x l test)
      (cond ((pair? l)
	     (if (test x (car l)) #t
		 (cl-mem x (cdr l) test)))
	    (else #f)))
    (set! *t:found-contradiction* #f)
    (and 
     (every
      (lambda (proof-step)
	(let ((n (list-ref proof-step 0))
	      (info (list-ref proof-step 1))
	      (clause (list-ref proof-step 2)))
	  (cond  ((member info '((Axiom) (Negated-Goal)))
		  (print n)
		  #t)
		 (else
		  ;; It's a proof step, first part is steps: (s1 s2) then clause
		  ;; does it follow?
		  (cond ((and (= (length info) 2) ; are the info ok?
			      (number? (first info))
			      (number? (second info))
			      (< 0 (first info) n)
			      (< 0 (second info) n))
			 ;; Check clause
			 (and (let ((resolvents 
				     (get-resolvents
				      (cons 'or (prev-clause (t:safe-first info)))
				      (cons 'or (prev-clause (t:safe-second info)))
				      )))
				(cond ((and (null? (cdr clause))
					    (equal? (caar clause) 'ans)
					    (equal? clause contradiction)
					    (member '() resolvents)
					    )
				       ;; Indicate if we got valid contradiction
				       (set! *t:found-contradiction* #t)
				       #t)
				      (else
				       (cl-mem (if (null? clause)
						   clause
						   (cons 'or clause))
					       resolvents equiv-test))))
			      (begin (print n) #t)
			      ))
			((and (= (length info) 2) ; factoring
			      (eq? (first info) 'f)
			      (number? (second info))
			      (< 0 (second info) n))
			 (let ((factorings
				(get-factorings
				 (prev-clause (t:safe-second info))
				 )))
			   (cl-mem clause factorings equiv-test))
			 )
			))
		 )))
      parsed-proof)
     *t:found-contradiction*)
    ))

;;; Returns an assoc list ((1 (axiom) ((..))) (2 ...) ...)
(define (parse-proof proof)
  (cond ((null? proof) '())
	((pair? (car proof))
	 (cond ((and (number? (caar proof)) (>= (length proof) 3))
		(cons (list (caar proof) ; step #
			    (cadr proof) ; (axiom), (i j), (negated goal)
			    (caddr proof) ; clause
			    )
		      (parse-proof (cdddr proof))))
	       ((equal? (caar proof) 'unifier:)
		(parse-proof (cdr proof)))
	       (else (error "Ill formed proof:" proof))))
	(else 
	 (error "Ill formed proof:" proof))))

;;(trace fol-all-resolvents)
;;(trace variant?)
;;(trace ensure-or)