;; Code for converting an Otter proof object into a LaTeX file, from which
;; a human-readable proof can be produced, featuring:
;;  - Conversion of disjunctive normal form back into implicative form
;;  - Elimination of repetitive or unnecessary steps
;;  - Typesetting of unary and binary operators, with precedence levels
;;  - Reorganization of proof to improve flow and reduce number of
;;    long-distance references.
;;
;; For latest version see: http://moonflare.com/code/po2hr.php
;;
;; Copyright (c) 2003, Derrick Coetzee
;; All rights reserved.
;;
;; Redistribution and use in source and binary forms, with or without
;; modification, are permitted provided that the following conditions
;; are met:
;;
;; - Redistributions of source code must retain the above copyright
;;   notice, this list of conditions and the following disclaimer.
;;
;; - Redistributions in binary form must reproduce the above copyright
;;   notice, this list of conditions and the following disclaimer in
;;   the documentation and/or other materials provided with the
;;   distribution.
;;
;; - The name of Derrick Coetzee may not be used to endorse or promote
;;   products derived from this software without specific prior
;;   written permission.
;;
;; This software is provided by the copyright holders and contributors
;; "as is" and any express or implied warranties, including, but not
;; limited to, the implied warranties of merchantability and fitness
;; for a particular purpose are disclaimed. In no event shall the
;; copyright owner or contributors be liable for any direct, indirect,
;; incidental, special, exemplary, or consequential damages
;; (including, but not limited to, procurement of substitute goods or
;; services; loss of use, data, or profits; or business interruption)
;; however caused and on any theory of liability, whether in contract,
;; strict liability, or tort (including negligence or otherwise)
;; arising in any way out of the use of this software, even if advised
;; of the possibility of such damage.

;; We work in preserve case mode so that symbols in the input proof
;; object keep their case.
(SETF (READTABLE-CASE *READTABLE*) :PRESERVE)
;; The smallest-width statement (roughly in characters) to repeat
;; in-line whenever it is referenced, instead of using a reference.
(SETF *MIN-INLINE-OTTER-STATEMENT-SIZE* 30)

;; A table of binary operators. Each entry has the form (op (" latex "
;; precedence)), where op is the symbol used in the proof object for
;; the operator, latex the LaTeX to typeset the operator, and
;; precedence how tightly it binds, large numbers for more tightly,
;; which affects when parenthesis are inserted. Use only precedence
;; values < 100. The default table is for Prof. Belinfante's set
;; theory proofs.
(DEFPARAMETER *otter-infix-operator-table* (MAKE-HASH-TABLE))
(MAPCAR #'(LAMBDA (x)
            (SETF (GETHASH (FIRST x) *otter-infix-operator-table*) (SECOND x)))
        '((member        (" \\in "       40))
          (subclass      (" \\subseteq " 50))
          (and           (" \\;\\wedge\\; "    35))
          (or            (" \\;\\vee\\; "      35))
          (implies       (" \\implies "  20))
          (equal         (" = "          30))
          (cart          (" \\times "    60))
          (composite     (" \\circ "     60))
          (intersection  (" \\cap "      60))
          (union         (" \\cup "      60))
          ))

;; This table is just like the infix operator table, except it's
;; used for negated operators, such as (not (member x y)).
(DEFPARAMETER *otter-neg-infix-operator-table* (MAKE-HASH-TABLE))
(MAPCAR #'(LAMBDA (x)
            (SETF (GETHASH (FIRST x) *otter-neg-infix-operator-table*) (SECOND x)))
        '((member   (" \\notin "     40))
          (subclass (" \\nsubseteq " 50))
          (equal    (" \\neq "       30))
          ))

;; This table describes unary operators. In reality these
;; may have more than one argument, and they will be separated
;; with commas before prefixing/affixing the operator. An entry
;; (op (" before-latex " " after-latex " precedence consider-parens))
;; tells it that when it sees (op arg) to put the before-latex before
;; the arg and the after-latex after the arg. If consider-parens is
;; NIL, parenthesis are never placed around the expression; otherwise,
;; the precedence dictates when they will be added.
(DEFPARAMETER *otter-unary-operator-table* (MAKE-HASH-TABLE))
(MAPCAR #'(LAMBDA (x)
            (SETF (GETHASH (FIRST x) *otter-unary-operator-table*) (SECOND x)))
        '((singleton   ("\\left\\{" "\\right\\}"  90    NIL))
          (inverse     ("{{" "}^{-1}}"          90    T))
          (complement  ("{\\overline{" "}}"     90    NIL))
          (not         ("\\neg " ""             90    T))
          (P           ("\\mathscr{P}(" ")"     90    NIL))
          (pair        ("\\left\\langle " "\\right\\rangle " 90    NIL))
          ))

(DEFUN fold (func list)
    "Takes a list (x1 x2 ... xn-1 xn) and gives (func x1 (func x2 ... (func xn-1 xn)))
     For example, (fold #'+ '(1 2 3 4)) produces 1+(2+(3+4))."
    (IF (NULL (REST list))
        (FIRST list)
        (FUNCALL func (FIRST list) (fold func (REST list)))))

(DEFUN stringize-atom (atom)
     "Converts the given number, symbol, or string into string form"
     (COND ((NUMBERP atom) (FORMAT NIL "~D" atom))
           (T              (STRING atom))))

(DEFUN atom-length (name)
    "Gives a rough estimate of the printed width in characters
     of the given atom."
    (COND ((EQUAL name 'inverse)   1)
          ((EQUAL name 'cart)      1)
	  ((EQUAL name 'composite) 1)
          (T  (LENGTH name))))

(DEFUN statement-size-helper (expr num-params)
    (IF (CONSP expr) (+ (statement-size-helper (FIRST expr) (LIST-LENGTH (REST expr)))
                        (APPLY #'+ (MAPCAR
                                   #'(LAMBDA (x) (statement-size-helper x 0))
                                   (REST expr))))
                     (+ (atom-length (stringize-atom expr))
                        (IF (>= num-params 1)
                            (+ (- num-params 1) 2)
                            0))))

(DEFUN statement-size (expr)
    "Gives a rough estimate of the printed width in characters
     of the given statement"
    (statement-size-helper expr 0))

(DEFUN separated-list (stringizer values delimiter)
    "Takes a list of values and a function to convert each to a string,
     and returns a delimiter-separated list of the stringized values."
    (IF (NULL values)
        ""
        (IF (NULL (REST values))
            (FUNCALL stringizer (FIRST values))
            (CONCATENATE 'STRING
                (FUNCALL stringizer (FIRST values)) delimiter
                (separated-list stringizer (REST values) delimiter)))))

(DEFUN step-type (step)
    "Gets the operation being carried out in this step, such as 'reduce"
    (FIRST (SECOND step)))

(DEFUN markup (symname is-func)
    "Subscripts trailing numbers on a symbol, and, if is-func is NIL,
     formats multicharacter symbols appropriately so they don't appear
     as products."
    (LET* ((name (REMOVE #\$ (stringize-atom symname)))
           (numStart (POSITION-IF #'DIGIT-CHAR-P name)))
          (IF (OR (NULL numStart) (EQUAL numStart 0))
              (IF (AND (NOT is-func) (> (LENGTH name) 1))
		  (CONCATENATE 'STRING "\\text{\\emph{" name "}}")
		  name)
              (CONCATENATE 'STRING
                  (markup (SUBSEQ name 0 numStart) is-func)
                  "_{"
                  (SUBSEQ name numStart)
                  "}"))))

(DEFUN variable-to-latex (var-name)
    (markup var-name NIL))

(DEFUN function-to-latex (func-name)
  (CONCATENATE 'STRING "\\operatorname{" (markup func-name T) "}"))

(DEFUN precedence (name arguments)
    "Gets precedence of operator, or maximum precedence if not an operator"
    (LET ((infix-op  (GETHASH name *otter-infix-operator-table*))
          (neg-infix-op (IF (AND (EQUAL name 'not)
                                 (CONSP (FIRST arguments)))
                            (GETHASH (FIRST (FIRST arguments))
                                     *otter-neg-infix-operator-table*)))
          (unary-op  (GETHASH name *otter-unary-operator-table*)))
         (COND ((NOT (NULL infix-op))     (SECOND infix-op))
               ((NOT (NULL neg-infix-op)) (SECOND neg-infix-op))
               ((NOT (NULL unary-op))     (THIRD unary-op))
               (T  100))))

(DEFUN precedence-call (func-call)
    "Gets precedence of operator corresponding to this call, or
     maximum precedence if not an operator."
    (IF (CONSP func-call)
        (precedence (FIRST func-call) (REST func-call))
        100))

(DEFUN func-call-to-latex (name arguments)
    "Translates a function application to a string of LaTeX"
    (LET ((infix-op  (GETHASH name *otter-infix-operator-table*))
          (neg-infix-op (IF (AND (EQUAL name 'not) (CONSP (FIRST arguments)))
                            (GETHASH (FIRST (FIRST arguments))
                                     *otter-neg-infix-operator-table*)))
          (unary-op  (GETHASH name *otter-unary-operator-table*)))
    (COND ((OR (NOT (NULL infix-op)) (NOT (NULL neg-infix-op)))
               (separated-list
                #'(LAMBDA (arg)
                          (LET ((add-parens (<= (precedence-call arg)
                                                (precedence name arguments))))
                          (CONCATENATE 'STRING
                               (IF add-parens "\\left(" "")
                               (statement-to-latex-helper arg)
                               (IF add-parens "\\right)" ""))))
                (IF (NOT (NULL neg-infix-op)) (REST (FIRST arguments)) arguments)
                (IF (NOT (NULL neg-infix-op)) (FIRST neg-infix-op) (FIRST infix-op))))
          ((NOT (NULL unary-op))
              (LET ((add-parens (AND (FOURTH unary-op)
                                     (<= (precedence-call (FIRST arguments))
                                         (precedence name arguments)))))
              (CONCATENATE 'STRING
                 (FIRST unary-op)
                 (IF add-parens "\\left(" "")
                 (separated-list #'statement-to-latex-helper arguments ",")
                 (IF add-parens "\\right)" "")
                 (SECOND unary-op))))
          (T
              (CONCATENATE 'STRING
                 (function-to-latex name)
                 "\\left("
                 (separated-list #'statement-to-latex-helper arguments ",")
                 "\\right)")))))

(DEFUN free-name (name)
    "Returns true iff name is an Otter free variable"
    (AND (EQUAL (REMOVE-IF #'DIGIT-CHAR-P name) "v"))
         (EQUAL (CHAR name 0) #\v))

(DEFUN extract-frees (statement)
    "Gets all free variables in statement"
    (kill-dups (filter (LAMBDA (symname)
                 (IF (NOT (SYMBOLP symname)) NIL
                     (free-name (stringize-atom symname))))
                 (flatten statement))
               #'STRING<))

(DEFUN declare-frees (free-vars)
    "Creates a forall statement for a list of free-variables"
       (IF (NULL free-vars) ""
           (FORMAT NIL
"(\\forall ~A)\\ "
           (separated-list #'variable-to-latex free-vars ","))))

(DEFUN statement-to-latex-helper (statement)
    (COND ((NOT (CONSP statement))   (variable-to-latex statement))
          ((NULL (REST statement)) (statement-to-latex-helper (FIRST statement)))
          ((CONSP (FIRST statement))
              (separated-list #'statement-to-latex-helper statement " \\;\\vee\\; "))
          (T  (func-call-to-latex (FIRST statement) (REST statement)))))

(DEFUN statement-to-latex (statement)
    "Converts a step's resulting expression to a LaTeX string"
    (CONCATENATE 'STRING
        (declare-frees (extract-frees statement))
        (statement-to-latex-helper (DNF-to-implications statement))))

(DEFUN DNF-to-implications (statement)
    "Converts disjunctive normal form back to implicative form where
     possible, for human-readability."
    (LET ((left-clauses
            (MAPCAR #'(LAMBDA (not-statement) (SECOND not-statement))
                  (filter #'(LAMBDA (st) (EQUAL (FIRST st) 'not)) statement)))
          (right-clauses
            (filter #'(LAMBDA (st) (NOT (EQUAL (FIRST st) 'not))) statement)))
         (IF (OR (NULL left-clauses) (NULL right-clauses))  statement
             (LET ((left-side
                      (IF (NULL (REST left-clauses))
                          (FIRST left-clauses)
                          (CONS 'and left-clauses)))
                   (right-side
                      (IF (NULL (REST right-clauses))
                          (FIRST right-clauses)
                          (CONS 'or right-clauses))))
                 (CONS 'implies (CONS left-side (CONS right-side NIL)))))))

(DEFUN flatten (list)
    "Makes a list containing every element contained in list or
     in the flatten of any list in list"
    (IF (NULL list) NIL
    (IF (NOT (CONSP list)) (CONS list NIL)
        (APPEND (flatten (FIRST list)) (flatten (REST list))))))

(DEFUN filter (testfunc list)
    "Keeps all elements for which testfunc is true, kills the rest"
    (IF (NULL list) NIL
        (IF (FUNCALL testfunc (FIRST list))
            (CONS (FIRST list) (filter testfunc (REST list)))
            (filter testfunc (REST list)))))

(DEFUN to-end-helper (testfunc list matches)
    "Moves all elements matching the testfunc to the end"
    (IF (NULL list) matches
        (IF (FUNCALL testfunc (FIRST list))
            (to-end-helper testfunc (REST list) (CONS (FIRST list) matches))
            (CONS (FIRST list) (to-end-helper testfunc (REST list) matches)))))

(DEFUN to-end (testfunc list)
    "Moves all elements matching the testfunc to the end"
    (to-end-helper testfunc list NIL))

(DEFUN kill-dups-helper (sortedlist)
    (COND ((NULL sortedlist) NIL)
          ((NULL (REST sortedlist)) (CONS (FIRST sortedlist) NIL))
          (T  (IF (EQUAL (FIRST sortedlist) (SECOND sortedlist))
                  (kill-dups-helper (REST sortedlist))
                  (CONS (FIRST sortedlist) (kill-dups-helper (REST sortedlist)))))))

(DEFUN kill-dups (list predicate)
    "Removes duplicate elements from the list sorted with predicate"
    (kill-dups-helper (SORT list predicate)))

(DEFUN extract-skolems (statement)
    "Gets a list of all skolem variables and functions used in statement"
    (kill-dups (filter (LAMBDA (symname)
                 (IF (NOT (SYMBOLP symname)) NIL
                     (NOT (NULL (FIND #\$ (stringize-atom symname))))))
                 (flatten statement))
               #'STRING<))


(DEFUN step-refs-equation (number step prev-step)
    "Returns T iff the given step references the statement with the given number"
    (IF (OR (EQUAL number (FIRST step))
            (EQUAL number (FIRST prev-step)))
        NIL
        (COND ((EQUAL (step-type step) 'input) NIL)
              ((EQUAL (step-type step) 'instantiate)
                  (MEMBER (SECOND (SECOND step)) number))
              (T
                  (INTERSECTION number (remove-evens (REST (SECOND step))))))))

(DEFUN proof-refs-equation-helper (number proof prev-step)
    (IF (NULL proof) NIL
        (OR (step-refs-equation number (FIRST proof) prev-step)
            (proof-refs-equation-helper number (REST proof) (FIRST proof)))))

(DEFUN proof-refs-equation (number proof prev-step)
    "Returns true iff some step in the proof references the statement
     with the given number."
    (IF (< (statement-size (extract-statement (FIRST number) proof))
           *MIN-INLINE-OTTER-STATEMENT-SIZE*)
        NIL
        (proof-refs-equation-helper number proof prev-step)))

(DEFUN equation-to-latex (number statement proof)
    "Converts a statement into a LaTeX (possibly numbered) equation"
    (LET ((eq-refed   (proof-refs-equation number proof NIL)))
         (FORMAT NIL
"
\\begin{equation~A} \\label{~D}
~A
\\end{equation~A}"
              (IF (NULL eq-refed) "*" "")
              (FIRST number)
              (statement-to-latex statement)
              (IF (NULL eq-refed) "*" ""))))

(DEFUN input-to-latex (number statement prev-number prev-statement proof)
    "Converts an input step to LaTeX"
    (LET* ((skolems       (extract-skolems statement))
           (all-skolems   (fold #'UNION (MAPCAR #'extract-skolems proof)))
           (prev-skolems  (extract-skolems prev-statement))
           (equation      (equation-to-latex number statement proof)))
         (IF (AND (NULL (extract-skolems statement))
                  (< (statement-size statement)
                     *MIN-INLINE-OTTER-STATEMENT-SIZE*))
             ""
         (IF (AND (NOT (NULL prev-statement))
                  (EQUAL (NULL skolems) (NULL prev-skolems)))
             equation
         (IF (NULL skolems)
             (FORMAT NIL "We know the following: ~A" equation)
             (FORMAT NIL 
                  "There exist~A $~A$ such that the following hold: ~A"
                  (IF (EQUAL (LIST-LENGTH all-skolems) 1) "s" "")
                  (separated-list #'variable-to-latex all-skolems ",")
                  equation))))))

(DEFUN substitute-pair-to-latex (pair)
    "Converts a 'we substitute this for this' pair in an instantiate
     step to LaTeX"
    (FORMAT NIL "$~A$ for $~A$" (statement-to-latex-helper (REST pair))
                                (statement-to-latex-helper (FIRST pair))))

(DEFUN instantiate-to-latex (number step-instantiated substitute-pairs statement prev-number proof)
    "Converts an instantitate step to LaTeX"
    (LET ((equation (equation-to-latex number statement proof))
          (substs   (separated-list #'substitute-pair-to-latex substitute-pairs " and ")))
        (IF (MEMBER step-instantiated prev-number)
            (FORMAT NIL "We then substitute ~A to obtain ~A" substs equation)
            (FORMAT NIL "In ~A we substitute ~A to obtain ~A"
                    (ref-number step-instantiated proof) substs equation))))

(DEFUN propositional-to-latex (number step-proped statement prev-number proof)
    "Converts a propositional or 'reduce' step to LaTeX"
    (LET ((equation (equation-to-latex number statement proof)))
        (IF (MEMBER step-proped prev-number)
            (FORMAT NIL "which reduces to ~A" equation)
            (FORMAT NIL "We may reduce ~A to ~A" (ref-number step-proped proof) equation))))

(DEFUN extract-statement (number proof)
    "Extracts the statement from step number of the proof"
    (THIRD (FIRST (MEMBER-IF #'(LAMBDA (step) (MEMBER number (FIRST step))) proof))))

(DEFUN primary-number (number proof)
    "Extracts the number used in the original label statement"
    (FIRST (FIRST (FIRST (MEMBER-IF #'(LAMBDA (step) (MEMBER number (FIRST step))) proof)))))

(DEFUN ref-number (number proof)
    "Gets a LaTeX string referencing the equation with the given
     number, or a string with the entire statement if it is short"
    (LET ((statement (extract-statement number proof)))
    (IF (< (statement-size statement) *MIN-INLINE-OTTER-STATEMENT-SIZE*)
        (FORMAT NIL "$~A$" (statement-to-latex statement))
        (FORMAT NIL "(\\ref{~D})" (primary-number number proof)))))

(DEFUN resolve-to-latex (number steps-reduced statement prev-number proof)
    "Converts a resolve step to LaTeX, treating the final 'contradiction'
     step specially"
    (LET ((equation      (equation-to-latex number statement proof))
          (ref-statement (LAMBDA (x) (ref-number x proof))))
    (IF (INTERSECTION prev-number steps-reduced)
        (IF (NULL statement)
            (FORMAT NIL "but this contradicts ~A."
                (separated-list ref-statement (REMOVE-IF #'(LAMBDA (x) (MEMBER x prev-number)) steps-reduced) ", "))
            (FORMAT NIL "which together with ~A yields ~A"
                (separated-list ref-statement (REMOVE-IF #'(LAMBDA (x) (MEMBER x prev-number)) steps-reduced) ", ")
                equation))
        (IF (NULL statement)
            (FORMAT NIL "But ~A form a contradiction."
                (separated-list ref-statement steps-reduced ", "))
            (FORMAT NIL "Combining ~A, we get ~A"                
                (separated-list ref-statement steps-reduced ", ")
                equation)))))

(DEFUN flip-to-latex (number step-flipped statement prev-number proof)
    "Converts a flip step to LaTeX. Flip steps are removed, so this
     should no longer be used."
    (LET ((equation      (equation-to-latex number statement proof)))
    (IF (MEMBER step-flipped prev-number)
        (FORMAT NIL "which we can flip to get ~A" equation)
        (FORMAT NIL "Flipping the two sides in ~A we get ~A"                
                (ref-number step-flipped proof) equation))))

(DEFUN remove-evens (list)
    "Removes the 2nd, 4th, etc. elements from a list."
    (IF (NULL list) NIL
        (CONS (FIRST list)
            (remove-evens (REST (REST list))))))

(DEFUN step-to-latex (step prev-step proof)
    "Converts an arbitrary proof step to a LaTeX string"
    (COND ((EQUAL (step-type step) 'input)
              (input-to-latex (FIRST step) (THIRD step) (FIRST prev-step)
                              (IF (EQUAL (step-type prev-step) 'input)
                                  (THIRD prev-step) NIL)
                              proof))
          ((EQUAL (step-type step) 'instantiate)
              (instantiate-to-latex (FIRST step)
                                    (SECOND (SECOND step))
                                    (THIRD (SECOND step))
                                    (THIRD step)
                                    (FIRST prev-step)
                                    proof))
          ((OR (EQUAL (step-type step) 'resolve)
               (EQUAL (step-type step) 'paramod))
              (resolve-to-latex (FIRST step)
                                (remove-evens (REST (SECOND step)))
                                (THIRD step)
                                (FIRST prev-step)
                                proof))
          ((EQUAL (step-type step) 'flip)
              (flip-to-latex (FIRST step)
                             (SECOND (SECOND step))
                             (THIRD step)
                             (FIRST prev-step)
                             proof))
          ((EQUAL (step-type step) 'propositional)
              (propositional-to-latex (FIRST step)
                                      (SECOND (SECOND step))
                                      (THIRD step)
                                      (FIRST prev-step)
                                      proof))))

(DEFUN list-lexicographic-less (left-list right-list predicate)
    "Returns true iff the first non-matching element of left-list
     is less than the corresponding element of right-list, where
     nested lists are compared recursively using this function."
       (COND ((AND (NULL left-list) (NULL right-list))  NIL)
             ((NULL left-list)       1)
             ((NULL right-list)      NIL)
             ((NOT (NULL (FUNCALL predicate
                             (FIRST left-list) (FIRST right-list))))  1)
             ((NOT (NULL (FUNCALL predicate
                             (FIRST right-list) (FIRST left-list))))  NIL)
             (T      (list-lexicographic-less
                         (REST left-list) (REST right-list) predicate))))

(DEFUN cluster-skolems (left-step right-step)
    "Moves all input statements referencing skolems together, so we
     can make the 'there exists such that the following:' statement."
    (IF (AND (EQUAL (step-type left-step) 'input)
             (EQUAL (step-type right-step) 'input))
        (LET ((left-skolems   (extract-skolems (THIRD left-step)))
              (right-skolems  (extract-skolems (THIRD right-step))))
             (list-lexicographic-less left-skolems right-skolems
              #'(LAMBDA (left right) (STRING< (stringize-atom left) (stringize-atom right)))))
        (IF (OR (EQUAL (step-type left-step) 'input)
                (EQUAL (step-type right-step) 'input))
            (IF (EQUAL (step-type left-step) 'input) T NIL)
            (LET ((left-number   (FIRST left-step))
                  (right-number  (FIRST right-step)))
                 (< left-number right-number)))))

(DEFUN proof-to-latex-helper (remaining-proof prev-step proof)
    (IF (NULL remaining-proof) ""
        (CONCATENATE 'STRING
            (step-to-latex (FIRST remaining-proof) prev-step proof)
            (proof-to-latex-helper (REST remaining-proof) (FIRST remaining-proof) proof))))

(DEFUN gather-dup-step-numbers (statement proof)
    (IF (NULL proof) NIL
        (IF (EQUAL (THIRD (FIRST proof)) statement)
            (CONS (FIRST (FIRST proof))
                  (gather-dup-step-numbers statement (REST proof)))
            (gather-dup-step-numbers statement (REST proof)))))

(DEFUN remove-duplicate-steps-helper (proof done-part)
    (IF (NULL proof) (REVERSE done-part)
            (remove-duplicate-steps-helper
             (REST proof)
             (IF (NULL (extract-statement (FIRST (FIRST proof)) done-part))
                 (CONS (CONS (gather-dup-step-numbers
                              (THIRD (FIRST proof))
                              proof)
                       (REST (FIRST proof)))
                       done-part)
                 done-part))))

(DEFUN remove-duplicate-steps (proof)
    "Remove duplicate statements, amassing all step numbers for
     identical statements into the first of them"
    (remove-duplicate-steps-helper proof NIL))

(DEFUN move-inputs-helper (proof inputs)
    "Move non-skolemized inputs to the place right before they're used"
    (IF (NULL proof) NIL
    (IF (AND (EQUAL (step-type (FIRST proof)) 'input)
             (NULL (extract-skolems (THIRD (FIRST proof)))))
        (move-inputs-helper (REST proof) (CONS (FIRST proof) inputs))
        (LET ((used-inputs
               (filter #'(LAMBDA (input)
                                 (step-refs-equation (FIRST input)
                                                     (FIRST proof)
                                                     NIL))
                       inputs)))
        (APPEND used-inputs
                (CONS (FIRST proof)
                      (move-inputs-helper
                       (REST proof)
                       (SET-DIFFERENCE inputs used-inputs))))))))

(DEFUN move-inputs (proof)
    "Move non-skolemized inputs to the place right before they're used"
    (move-inputs-helper proof NIL))

(DEFUN short-inputs-to-end (proof)
    "Moves inputs which are so short that they will only be referenced
     inline to end of proof, where they will be later ignored. They must
     still be present for referencing to work, however."
  (to-end #'(LAMBDA (step)
                    (AND (EQUAL (step-type step) 'input)
                         (NULL (extract-skolems (THIRD step)))
                         (< (statement-size (THIRD step))
                            *MIN-INLINE-OTTER-STATEMENT-SIZE*)))
          proof))

(DEFUN remove-pairs-transitively (pair-list)
    "Takes a list of dotted pairs and combines pairs whose second
     and first elements match, for example changing the 'chain'
     (1 . 3) (3 . 4) (4 . 7) into (1 . 7)."
    (IF (NULL pair-list) NIL
    (LET* ((rest-removed  (remove-pairs-transitively (REST pair-list)))
           (transitive-match
            (FIRST (MEMBER-IF #'(LAMBDA (x) (EQUAL (FIRST x)
                                                   (REST (FIRST pair-list))))
                              rest-removed))))
          (IF (NULL transitive-match)
              (CONS (FIRST pair-list) rest-removed)
              (CONS (CONS (FIRST (FIRST pair-list)) (REST transitive-match))
                    (REMOVE transitive-match rest-removed))))))

(DEFUN merge-instantiates-helper (step-current step-next rest-proof proof)
    (COND ((NULL step-current) NIL)
          ((NULL step-next)    (CONS step-current NIL))
          ((AND (EQUAL (step-type step-current) 'instantiate)
                (EQUAL (step-type step-next)    'instantiate)
                (NOT (proof-refs-equation (FIRST step-current) proof NIL)))
           ; Nobody refs step-current except step-next, so merge
	   (LET  ((new-step  (LIST (FIRST step-next)
				  (LIST 'instantiate
					(SECOND (SECOND step-current))
					(remove-pairs-transitively
					 (APPEND (THIRD (SECOND step-current))
						 (THIRD (SECOND step-next)))))
				  (THIRD step-next))))
                   (merge-instantiates-helper new-step
                                              (FIRST rest-proof)
                                              (REST rest-proof)
                                              proof)))
           (T  (CONS step-current
                     (merge-instantiates-helper step-next
                                                (FIRST rest-proof)
                                                (REST rest-proof)
                                                proof)))))

(DEFUN merge-instantiates (proof)
    "Merges multiple consecutive instantiates steps into one
     instantiate step, eliminating redundant instantiations as well."
    (merge-instantiates-helper (FIRST proof) (SECOND proof) (REST (REST proof)) proof))

(DEFUN merge-flips-helper (proof done-part)
    (IF (NULL proof) (REVERSE done-part)
	(merge-flips-helper
	 (REST proof)
	 (IF (EQUAL (step-type (FIRST proof)) 'flip) done-part
	 (LET ((flip-step-numbers
		(fold #'UNION
		      (MAPCAR #'(LAMBDA (step) (AND (EQUAL (step-type step) 'flip)
						    (FIRST step)))
		      (filter #'(LAMBDA (step) (MEMBER (SECOND (SECOND step))
						       (FIRST (FIRST proof))))
			      proof)))))
	      (IF (NULL flip-step-numbers) (CONS (FIRST proof) done-part)
		  (CONS (CONS (UNION (FIRST (FIRST proof)) flip-step-numbers)
			      (REST (FIRST proof))) done-part)))))))

(DEFUN merge-flips (proof)
    "Removes all flip steps from the proof, pointing all references
     to the flipped steps to the non-flipped source step. Doing this
     operates on the assumption that flipping is so simple as to be
     obvious to humans."
    (merge-flips-helper proof NIL))

(DEFUN proof-to-latex (proof)
    "Converts an entire proof into a LaTeX string"
    (SORT proof #'cluster-skolems)
    (LET ((filtered-proof
            (merge-flips (merge-instantiates (short-inputs-to-end
             (move-inputs (remove-duplicate-steps proof)))))))
    (proof-to-latex-helper filtered-proof NIL filtered-proof)))

(DEFUN print-latex-proof (proof)
    "Outputs a LaTeX document describing the given proof"
    (FORMAT T
"\\documentclass[12pt]{article}

\\usepackage{fullpage,amsmath,amssymb,latexsym,mathrsfs}

\\begin{document}

\\noindent
Assume the theorem is false. ")
    (FORMAT T "~A" (proof-to-latex proof))
    (FORMAT T
"

\\end{document}"))