;---------------------------------------------------------------
;                Kazimir Majorinc, 2011
;
; This program performs automated theorem finding of the programs
; of propositional calculus. 

(setf [print.supressed] true [println.supressed] true)
(load "http://www.instprog.com/Instprog.default-library.lsp")
(setf [print.supressed] nil [println.supressed] nil)

(pretty-print 200)

; Adjust file-prefix and folder name

(define file-prefix "L4-11")
(define folder-name (append "C:\\Newlisp\\finder\\" file-prefix "\\"))

(setf N 1000000000000); maximal number of combined rule application

(setf upper-limit-for-theorem-size 14)
(setf tautology-testing nil)
(setf report-to-file-period 900)
(setf axioms-have-priority true)
;---------------------------------------------------------------
; L4 Mendellson                       
                       
(define axioms '((A -> (B -> A))
                 ((A -> (B -> C)) -> ((A -> B) -> (A -> C)))
                 ((A and B) -> A)
                 ((A and B) -> B)
                 (A -> (B -> (A and B)))
                 (A -> (A or B))
                 (B -> (A or B))
                 ((A -> B) -> ((B -> C) -> ((A or B) -> C)))
                 ((A -> B) -> ((A -> (not B)) -> (not A)))
                 ((not (not A)) -> A)))
;---------------------------------------------------------------
(define (human-readable-proof0 p) ; p is the name of the theorem, tm-1 or so
  (let((proof-of-p               (aval 'proof (eval p)))
       (human-readable-theorem-p (infix<->prefix (aval 'theorem (eval p)))))
    (if (= proof-of-p 'axiom)
      (list (list (format "%-17s" (string p ".") )
                  human-readable-theorem-p ", axiom"))
      (append (human-readable-proof0 (proof-of-p 1))
              (human-readable-proof0 (proof-of-p 2))
              (list (list (format "%-17s" (string p "."))
                          human-readable-theorem-p 
                           ", M:" (proof-of-p 1)
                           ", m:" (proof-of-p 2)
                           ", u:" (proof-of-p 3)))))))
(define (human-readable-proof p)
  (unique (human-readable-proof0 p)))
;---------------------------------------------------------------
(define (print-theorem idx tm-name)
  (===)
  ;(println (format "%-17s" "in-this-list") (string idx))
  (println (format "%-17s" "tm-name") tm-name)
  (println (format "%-17s" "in-theory") (string (+ (find tm-name theory) 1)))
  (println (format "%-17s" "times-derived") 
           (eval (sym (string (aval 'theorem (eval tm-name))))))
  (---)
  (dolist(j (eval tm-name))
    (if (= (j 0) 'theorem)
      (println (format "%-17s" (string (j 0))) (infix<->prefix (j 1)))
      (println (format "%-17s" (string (j 0))) (j 1))))
  (---)
  (dolist(j (human-readable-proof tm-name))
     (dolist(k j)(print k))
         (println)))
;---------------------------------------------------------------
(define (print-theory-report) 
  (letn (L   '((- (apply date-value (now)) T0)
             development-time
              N 
              i
              (length theory)
              row 
              col 
              square
              chose-next-theorem-counter
              theorem-counter
              major-isnt-implication
              major-is-implication
              unification-failed
              unification-succeeded  
              theorem-was-already-derived
              theorem-is-too-long
              theorem-is-short-enough
              try-modus-ponens-counter
              candidates-counter
              candidate-is-instance-counter
              candidate-is-not-instance-counter
              satisfactory-candidate-found-counter
              max-theorem-size
              max-proof-size
              max-proof-steps))
    (dotimes(j (+ upper-limit-for-theorem-size 2))
         (push (expand '(length (class-theory j)) 'j) L -1))
    (dolist(j L)
      (let((oldj (+sym j (quote _))))
        (print j "," (eval j) "," (eval oldj))
        (when (and (number? (eval j))
                   (number? (eval oldj)))
          (print "," (- (eval j) (eval oldj))))
        (println)
        (set oldj (if (eval j) (eval j) 0))))
    (---)))
;---------------------------------------------------------------
(define (save-all-reports)
 (inc rc)
 (let ((saving-time (apply date-value (now))))
   (print (date) ", theory=" 
          (length theory) ", i=" i ", saving " )
   (with-device (open (string folder-name file-prefix "-natural-" rc ".txt") "write")
     (box-standard "THEORY NATURALLY SORTED")
     (dolist(i theory)(print-theorem (+ $idx 1) i)))
   (with-device (open (string folder-name file-prefix "-theory-" rc ".csv") "write")
     (println "No,theorem,times-derived,theorem-size,proof-size,proof-steps,coefficient")
     (dolist(i theory)
       (println (+ $idx 1) "," 
                (prefix<->infix (aval 'theorem (eval i))) ","
                (eval (sym (string (aval 'theorem (eval i))))) ","
                (aval 'theorem-size (eval i)) "," 
                (aval 'proof-size   (eval i)) "," 
                (aval 'proof-steps  (eval i)) ","
                (exp (div (log (aval 'proof-size (eval i))) 
                          (aval 'theorem-size (eval i)))))))
   (with-device (open (string folder-name file-prefix "-data.csv") "append")
     (box-standard "THEORY REPORT")
     (print-theory-report))
   (println (- (apply date-value (now)) saving-time) " seconds.")))
;---------------------------------------------------------------
(define (read-axioms-into-repository)
  (dolist(j axioms)
    (inc theorem-counter)
    (letn ((theorem-name   (+sym 'tm- theorem-counter))
           (theorem        (canon (prefix<->infix j)))
           (theorem-size   (width-noq theorem))
           (proof          'axiom)
           (proof-size     theorem-size)
           (proof-steps    1)
           (axioms-used    (list theorem-name)))
     (set (sym (string theorem)) 1)
     (setf max-theorem-size (max max-theorem-size theorem-size))
     (set theorem-name 
          (assoc-list 'theorem      'theorem-size 'proof 
                      'axioms-used  'proof-size   'proof-steps))
     (if axioms-have-priority (setf axiom-class 0)
                              (setf axiom-class theorem-size))
     (push theorem-name (class-theory axiom-class) -1 )
     (println "Pushed " theorem-name " into (class-theory " axiom-class 
              ")(" (length (class-theory axiom-class)) ")"))))
;---------------------------------------------------------------
(define (chose-next-theorem)
  (inc chose-next-theorem-counter)
  (setf satisfactory-candidate-found nil)
  (dotimes(j (min (+ max-theorem-size 1) 
                  (+ upper-limit-for-theorem-size 1))
             satisfactory-candidate-found)
    (when (> (length (class-theory j)) 0)
      (until (or satisfactory-candidate-found
                 (empty? (class-theory j)))         
        (inc candidates-counter)
        (setf candidate-name             (pop (class-theory j)))
        (setf candidate                  (eval candidate-name))
        (setf candidate-theorem          (aval 'theorem      candidate))
        
        (setf const-candidate-theorem
              (prefix-variables-in-formula 'c candidate-theorem))
        (setf candidate-size             (aval 'theorem-size candidate))
        (if (exists (lambda(xx)
                       (list? (unify (aval 'theorem (eval xx))
                                     const-candidate-theorem)))
                      theory)        
            (inc candidate-is-instance-counter)           
            (begin (inc candidate-is-not-instance-counter)
                   (setf satisfactory-candidate-found true))))))
  (cond (satisfactory-candidate-found 
        (inc satisfactory-candidate-found-counter)
        (when (and tautology-testing 
                   (not (tautology? candidate-theorem)))
          (throw-error (string candidate-name
                               candidate-theorem
                               " isn't tautology.")))
        (set (sym (string candidate-name "m")) 
            (suffix-variables-in-formula "m" candidate-theorem))
        (push candidate-name theory -1)
        (setf (atheory (- (length theory) 1)) candidate-name)
        (setfmax max-proof-size  (aval 'proof-size candidate))
        (setfmax max-proof-steps (aval 'proof-steps candidate)))                    
   ('(not satisfactory-candidate-found)
         (println "All candidates exhausted.")
         (save-all-reports)
         (exit))))
;---------------------------------------------------------------
(define (try-modus-ponens row col)
  (inc try-modus-ponens-counter)
  (setf     item-major-name   (atheory (- row 1)))
  (setf     item-major        (eval item-major-name))
  (setf     premise-major     (aval 'theorem item-major))
  (cond 
    ((!= (operator premise-major) '->)(inc major-isnt-implication))
    ('(=  (operator premise-major) '->)(inc major-is-implication)
      (setf item-minor-name (atheory (- col 1)))
      (setf item-minor      (eval item-minor-name))
      (setf premise-minor   (aval 'theorem item-minor))
      (setf premise-minorm  (eval (sym (string item-minor-name "m"))))
      (setf antecendent     (first (arguments premise-major)))
      (setf u               (unify antecendent premise-minorm))
      (cond 
        ((not (list? u)) (inc unification-failed))
        ('(list? u)      (inc unification-succeeded)
           (setf    consequent       (last  (arguments premise-major)))
           (setf    theorem          (expand consequent u))
           (setf    theorem-size     (width-noq theorem))
           (cond 
             ((> theorem-size upper-limit-for-theorem-size)
                 (inc theorem-is-too-long))   
             ('(<= theorem-size upper-limit-for-theorem-size)
                (inc theorem-is-short-enough)
                (setf max-theorem-size (max max-theorem-size theorem-size))
                (setf theorem          (canon theorem))
                (setf theorem-sym      (sym (string theorem)))
                (setf etheorem-sym     (eval theorem-sym))
                (cond 
                  ((nil? etheorem-sym)
                     (inc  theorem-counter)                  
                     (set  theorem-sym        1)                                                      
                     (setf theorem-name (sym (string "tm-" theorem-counter)))                         
                     (set  theorem-name 
                       (list (list 'theorem      theorem)
                             (list 'theorem-size theorem-size)
                             (list 'proof        (list 'modus-ponens 
                                                        item-major-name 
                                                        item-minor-name 
                                                        u))
                             (list 'axioms-used  (unique (append (aval 'axioms-used item-major)
                                                                 (aval 'axioms-used item-minor))))
                             (list 'proof-size   (+ (aval 'proof-size item-major)
                                                    (aval 'proof-size item-minor)
                                                    theorem-size))
                             (list 'proof-steps  (+ (aval 'proof-steps item-major)
                                                    (aval 'proof-steps item-minor)
                                                    1))))
                     (push theorem-name (class-theory theorem-size) -1 )) 
                  ('(not (nil? etheorem-sym))(inc theorem-was-already-derived)
                     (set theorem-sym (+ etheorem-sym 1)))))))))))
;---------------------------------------------------------------
(setf theory (list))
(setf atheory (array 1000000))
(setf class-theory (array (+ upper-limit-for-theorem-size 3) '(())))
(setf max-theorem-size 0)
(setf T0 (apply date-value (now)))
(setf max-coefficient 0)
(setf max-proof-size 0)
(setf max-proof-steps 0)
(setf last-square 0)
(setf development-time 60)
(read-axioms-into-repository)
(setf Tlast (apply date-value (now)))
;---------------------------------------------------------------    
(setf i 1)
(while (<= i N) 
  (setf row    (cantors-row2 i))
  (setf col    (cantors-column2 i))
  (setf square (cantors-square i))
  (when (> square last-square)
     (chose-next-theorem)
     (setf Tnow (apply date-value (now)))
     (when (>= Tnow (+ Tlast development-time))
        (setf saving-time 
          (/. (time (begin (print "> ")
                            (save-all-reports)))
              1000))
        (setf development-time (max (* 9 saving-time) 60))
        (setf Tlast (apply date-value (now))))
     (when (= (% square 10) 0)
       (println "- " (date) ", theory=" (length theory) ", i=" i
                ", saving expected in " (- development-time 
                                           (- (apply date-value (now))
                                              Tlast)) " seconds."))
     (setf last-square square))
  (try-modus-ponens row col)
  (setf i (+ i 1)))
(print "] ")
(save-all-reports)
(exit)