(setq *theory* "6ffc9680fbe00a58d70cdeb319f11205ed998131ce51bb96f16c7904faf74a3d")

(defun pfgize-name (c)
  (let ((c (format nil "~d" c)))
    (if (equal c "")
    "blank"
      (let ((c0 (char-code (aref c 0))))
    (if (or (and (>= c0 65) (<= c0 90)) (and (>= c0 97) (<= c0 122)))
        c
      (format nil "c~d" c))))))

(defun ivytrm-sig (m probsig)
  (if (consp m)
      (let ((f (car m)))
    (if (assoc f probsig)
        (ivyspine-sig (cdr m) probsig)
      (ivyspine-sig (cdr m) (acons f (list 'I (length (cdr m))) probsig))))
    probsig))

(defun ivyspine-sig (ml probsig)
  (if ml
      (ivyspine-sig (cdr ml) (ivytrm-sig (car ml) probsig))
    probsig))

(defun ivyatm-sig (a probsig)
  (if (consp a)
      (if (eq (car a) '=)
      (ivyspine-sig (cdr a) probsig)
    (let ((p (car a)))
      (if (assoc p probsig)
          (ivyspine-sig (cdr a) probsig)
        (ivyspine-sig (cdr a) (acons p (list 'O (length (cdr a))) probsig)))))
    probsig))

(defun ivycl-sig (cl probsig)
  (if (consp cl)
      (case (car cl)
    (OR
     (ivycl-sig (caddr cl) (ivycl-sig (cadr cl) probsig)))
    (NOT
     (ivyatm-sig (cadr cl) probsig))
    (t (ivyatm-sig cl probsig)))
    probsig))

(defun ivypf-sig (ivypf &optional probsig)
  (if ivypf
      (ivypf-sig (cdr ivypf) (ivycl-sig (caddar ivypf) probsig))
    probsig))

(defun pfg-tp-r (rtp ar)
  (if (> ar 0)
      (format nil "TpArr ind ~d" (pfg-tp-r rtp (- ar 1)))
    (if (eq rtp 'O)
    "Prop"
      "ind")))

(defun pfg-tp (tp)
  (pfg-tp-r (car tp) (cadr tp)))

(defun ivytrm-frees (m vl)
  (if (consp m)
      (ivyspine-frees (cdr m) vl)
    (if (member m vl)
    vl
      (cons m vl))))

(defun ivyspine-frees (ml vl)
  (if ml
      (ivyspine-frees (cdr ml) (ivytrm-frees (car ml) vl))
    vl))

(defun ivyatm-frees (a vl)
  (if (consp a)
      (ivyspine-frees (cdr a) vl)
    vl))

(defun ivycl-frees (cl &optional vl)
  (if (consp cl)
      (case (car cl)
    (OR
     (ivycl-frees (caddr cl) (ivycl-frees (cadr cl) vl)))
    (NOT
     (ivyatm-frees (cadr cl) vl))
    (t (ivyatm-frees cl vl)))
    vl))

(defun pfg-trm (m)
  (if (consp m)
      (pfg-spine (pfgize-name (car m)) (cdr m))
    (format nil "~d" m)))

(defun pfg-spine (h ml)
  (if ml
      (pfg-spine (format nil "Ap ~d ~d" h (pfg-trm (car ml))) (cdr ml))
    h))

(defun pfg-atm (a)
  (if (consp a)
      (if (eq (car a) '=)
      (pfg-spine "Eq ind" (cdr a))
    (pfg-spine (pfgize-name (car a)) (cdr a)))
    (format nil "unknownatomcase:~d" a)))

(defun pfg-lit (l)
  (if (and (consp l) (eq (car l) 'NOT))
      (format nil "Imp ~d False" (pfg-atm (cadr l)))
    (pfg-atm l)))

(defun pfg-lit-neg (l)
  (if (and (consp l) (eq (car l) 'NOT))
      (pfg-atm (cadr l))
    (format nil "Imp ~d False" (pfg-atm l))))

(defun pfg-clause-2 (cl)
  (if cl
      (format nil "Imp ~d ~d" (pfg-lit-neg (car cl)) (pfg-clause-2 (cdr cl)))
    (format nil "False")))

(defun pfg-clause-r (vl cl)
  (if vl
      (format nil "All ~d ind ~d" (car vl) (pfg-clause-r (cdr vl) cl))
    (pfg-clause-2 cl)))

(defun ivycl-marked-lits (cl pos)
  (if (consp cl)
      (case (car cl)
    (OR
     (if pos
         (cond ((equal (car pos) 1)
            (append (ivycl-marked-lits (cadr cl) (cdr pos)) (mapcar #'(lambda (l) (cons 'NIL l)) (ivycl-lits (caddr cl)))))
           ((equal (car pos) 2)
            (append (mapcar #'(lambda (l) (cons 'NIL l)) (ivycl-lits (cadr cl)))
                (ivycl-marked-lits (caddr cl) (cdr pos))))
           (t (break)))
       (break)))
    (t (list (cons 't cl))))
    (break)))

(defun ivycl-lits (cl)
  (if (consp cl)
      (case (car cl)
    (OR (append (ivycl-lits (cadr cl)) (ivycl-lits (caddr cl))))
    (t (list cl)))
    (if (eq cl 'FALSE)
    nil
      (format nil "unknownprop:~d" cl))))

(defun pfg-clause (cl)
  (pfg-clause-r (reverse (ivycl-frees cl)) (ivycl-lits cl)))

(setq *ivylineh* (make-hash-table :test #'equal))

(defun pfg-just-line (x)
  (let ((just (cadr x)))
    (if (consp just)
    (case (car just)
      (INPUT (format nil "H~d" (car x))) ; should not happen, but this seems reasonable if it does
      (INSTANTIATE
       (let ((vl (reverse (ivycl-frees (caddr (gethash (cadr just) *ivylineh*)))))
         (pf (format nil "H~d" (cadr just)))
         (theta (caddr just)))
         (dolist (x vl pf)
           (let ((m (assoc x theta)))
         (setq pf (format nil "TmAp ~d ~d" pf (pfg-trm (cdr m))))))))
      (FLIP
       (let ((pf (format nil "H~d" (cadr just)))
         (pos (caddr just)))
         (format nil "TODO: FLIP ~d AT ~d" pf pos)))
      (RESOLVE
       (let ((pf1 (format nil "H~d" (cadr just)))
         (pos1 (caddr just))
         (pf2 (format nil "H~d" (nth 3 just)))
         (pos2 (nth 4 just)))
                    ; need to generalize this
         (cond ((and (equal pos1 nil) (equal pos2 nil))
            (format nil "PrAp ~d ~d" pf2 pf1))
           (t
            (let* ((cl1 (ivycl-marked-lits (caddr (gethash (nth 1 just) *ivylineh*)) pos1))
               (cl2 (ivycl-marked-lits (caddr (gethash (nth 3 just) *ivylineh*)) pos2))
               (cl (ivycl-lits (caddr x)))
               (vl1 (reverse (ivycl-frees (caddr (gethash (nth 1 just) *ivylineh*)))))
               (vl2 (reverse (ivycl-frees (caddr (gethash (nth 3 just) *ivylineh*)))))
               (vl (reverse (ivycl-frees (caddr x))))
               (litcnt 0)
               (pf nil)
               (la nil))
              (when (or vl vl1 vl2)
            (error "unhandled resolve case with free vars"))
              (dolist (l cl)
            (incf litcnt)
            (push (cons l (format nil "A~d" litcnt)) la)
            (if pf
                (setq pf (format nil "~d PrLa A~d ~d" pf litcnt (pfg-lit-neg l)))
              (setq pf (format nil "PrLa A~d ~d" litcnt (pfg-lit-neg l)))))
              (when (cdr cl1)
            (dolist (l cl1)
              (if (car l)
                  (setq pf1 (format nil "PrAp ~d A0" pf1))
                (let ((a (assoc (cdr l) la :test #'equal)))
                  (setq pf1 (format nil "PrAp ~d ~d" pf1 (cdr a))))))
            (dolist (l cl1)
              (when (car l)
                (setq pf1 (format nil "PrLa A0 ~d ~d" (pfg-lit-neg (cdr l)) pf1)))))
              (dolist (l cl2)
            (if (car l)
                (setq pf2 (format nil "PrAp ~d ~d" pf2 pf1))
              (let ((a (assoc (cdr l) la :test #'equal)))
                (setq pf2 (format nil "PrAp ~d ~d" pf2 (cdr a))))))
              (if pf
              (format nil "~d ~d" pf pf2)
            pf2))))))
      (PARAMOD
       (let ((pf1 (format nil "H~d" (cadr just)))
         (pos1 (caddr just))
         (pf2 (format nil "H~d" (nth 3 just)))
         (pos2 (nth 4 just)))
         (format nil "TODO: PARAMOD ~d AT ~d WITH ~d AT ~d" pf1 pos1 pf2 pos2)))
      (t (format nil "UNKNOWNJUST:~d" (car just))))
      "UNKNOWNJUST")))

(defun ivy-to-pfg (fn gn)
  (let* ((f (open fn :direction :input))
     (g (open gn :direction :output :if-exists :supersede :if-does-not-exist :create))
     (ivypf nil)
     (emptyclauseline nil)
     (thmcnt 0))
    (if *theory*
    (format g "Document ~d~%" *theory*)
      (format g "Document Empty~%"))
    (if (equal *theory* "6ffc9680fbe00a58d70cdeb319f11205ed998131ce51bb96f16c7904faf74a3d")
    (format g "Base ind~%Let False : Prop := Prim 1~%")
      (format g "Base ind~%Def False : Prop := All p Prop p~%"))
    (loop while (setq ivypf (read f nil nil)) do
      (setq *ivylineh* (make-hash-table :test #'equal))
      (dolist (x ivypf) (setf (gethash (car x) *ivylineh*) x))
      (let* ((probsig (reverse (ivypf-sig ivypf)))
         (ivyinput (remove-if-not #'(lambda (x) (and (consp (cadr x)) (eq (caadr x) 'INPUT))) ivypf)))
        (format g "Thm ivy~d :" (incf thmcnt))
        (setq *probsig* probsig)
        (setq *g* g)
        (dolist (x probsig)
          (setq *x* x)
          (format g " All ~d ~d" (pfgize-name (car x)) (pfg-tp (cdr x))))
        (format g "~%")
        (dolist (inp ivyinput)
          (format g " Imp ~d~%" (pfg-clause (caddr inp))))
        (format g " False~% :=")
        (dolist (x probsig)
          (format g " TmLa ~d ~d" (pfgize-name (car x)) (pfg-tp (cdr x))))
        (format g "~%")
        (dolist (inp ivyinput)
          (format g " PrLa H~d ~d~%" (car inp) (pfg-clause (caddr inp))))
        (dolist (x ivypf)
          (unless (and (consp (cadr x)) (eq (caadr x) 'INPUT))
        (if (eq (caddr x) 'FALSE)
            (setq emptyclauseline x)
          (format g " PrAp PrLa H~d ~d~%" (car x) (pfg-clause (caddr x))))))
        (if emptyclauseline
        (format g " ~d~%" (pfg-just-line emptyclauseline))
          (format g " ...~%"))
        (dolist (x (reverse ivypf))
          (unless (and (consp (cadr x)) (eq (caadr x) 'INPUT))
        (unless (eq (caddr x) 'FALSE)
          (format g " ~d~%" (pfg-just-line x)))))))
    (close g)
    (close f)))