;; okay, i'll keep these procedures for the sake of nesting

(define (make-pand p q) `(∧ ,p ,q))

(define pand
  (case-lambda
    [() #t]
    [(p) p]
    [(p . qs) (fold-left make-pand p qs)]))

(define (make-por p q) `(∨ ,p ,q))

(define por
  (case-lambda
    [() #f]
    [(p) p]
    [(p . qs) (fold-left make-por p qs)]))

;; iirc, or: (not p) or q
(define (make-p-> p q) `(→ ,p ,q))

;; could fold but laziness
(define p->
  (case-lambda
    [() #t]
    [(p) p]
    [(p . qs) (make-p-> p (apply p-> qs))]))

(define (p<-> p q) (pand (p-> p q) (p-> q p)))
;; maybe could have some pretty-printing logic? this definition is just 2 good 2 pass up
(define (pnot p) (p-> p #f))
(define ~ pnot)

;; maybe a var is just a sym? no forall lel
;; existence l8r
;; nah
;; valued vars? :o

;; (define-record-type forall
;;   (fields vars p)
;;   (nongenerative forall))
;; (define-syntax forall
;;   (syntax-rules ()
;;     [(forall (var* ...) p)
;;      (make-forall
;;       '(var* ...)
;;       (let ([var* 'var*] ...) p))]
;;     [(forall var p) (forall (var) p)]))

(define-record-type argument
  (fields premises conclusions)
  (nongenerative argument))

(define-syntax argument
  (syntax-rules ()
    [(_ (var* ...) (premise* ...) (conclusion* ...))
     (lambda (var* ...)
       (make-argument (list premise* ...) (list conclusion* ...)))]))

(define modus-ponens
  (argument (p q)
    [(p-> p q)
     p]
    [q]))

(define modus-tollens
  (argument (p q)
    [(p-> p q)
     (~ q)]
    [(~ p)]))

;; YES: multiple conclusions (no more simplification-{l,r})
(define simplification
  (argument (p q)
    [(pand p q)]
    [p q]))

(define conjunction
  (argument (p q)
    [p
     q]
    [(pand p q)]))

;; (follows (P* ... (-> p q) p Q* ...) q modus-ponens) => #t
;; iterative argument
;; laws of inference are taken as fact
;; norm vars
;; order irrelevant
;; search for reqs?

(define (premises<=? p1 p2)
  (and (andmap (lambda (prem) (member prem p2)) p1)
       #t))

(define (follows? prems q by)
  (and (member q (argument-conclusions by))
       (premises<=? (argument-premises by) prems)))

(define-record-type step
  (fields conclusion rule)
  (nongenerative step))

(define-record-type proof
  (fields argument steps)
  (nongenerative proof))

(define-syntax proof
  (syntax-rules ()
    [(_ (var* ...) arg (conclusion* rule*) ...)
     (lambda (var* ...)
       (make-proof (arg var* ...)
                   (list (make-step conclusion* rule*) ...)))])) 

;; bleh
;; huh, procedure-arity-mask can handle 1000+ no problem
;; returns the lowest arity
(define (procedure-arity proc)
  (define mask (procedure-arity-mask proc))
  (let loop ([i 0])
    (if (logbit? i mask)
        i
        (loop (add1 i)))))

;; so over-general lel
(define proof-variable
  (let* ([bases '#(p q r s t u)]
         [bases-count (vector-length bases)])
    (lambda (n)
      (define base (vector-ref bases (mod n bases-count)))
      (define num  (floor (/ n bases-count)))
      (string->symbol
       (format "~a~a"
               base
               (if (zero? num) "" num))))))

(define (placeholder-saturate f)
  ;; map iota is bad but convenient (macro so needed)
  (apply f (map proof-variable (iota (procedure-arity f)))))

;; i think i prefer the turnstile to therefore
(define (argument-pp arg port)
  (define prems (argument-premises arg))
  (define concls (argument-conclusions arg))
  (format port "~{~a\n~}~{⊢ ~a\n~}"
          prems concls))

(define (general-argument-pp arg port)
  (argument-pp (placeholder-saturate arg) port))

(define (cartesian-exponent xs n)
  (assert (and (integer? n) (>= n 0)))
  (case n
    [0 '()]
    [1 (map list xs)]
    [else
     (let ([exp-1 (cartesian-exponent xs (sub1 n))])
       (apply append
              (map (lambda (xs2)
                     (map (lambda (x)
                            (cons x xs2))
                          xs))
                   exp-1)))]))

(define (proof-valid? proof%)
  (define (gensyms n xs)
    (if (zero? n)
        ;; less confusing to apply (proof g0 g1 ...)
        (reverse xs)
        (gensyms (sub1 n)
                 (cons (gensym (symbol->string (proof-variable (sub1 n)))) xs))))
  (define proof (apply proof% (gensyms (procedure-arity proof%) '())))
  (define arg   (proof-argument proof))
  ;; reversing here lets us recover a nice order at the end
  (define prems (reverse (argument-premises arg)))
  (define goals (argument-conclusions arg))

  (define (fail concl rule)
    (printf "Failed to apply rule:\n")
    (argument-pp rule #t)
    (printf "Proof state:\n~{~a\n~}⊢ ~a\n"
            (reverse prems) concl)
    #f)

  (define (handle-general-step concl rule)
    (define targets
      (apply append prems (map (lambda (p) (if (pair? p) (cdr p) '())) prems)))
    (ormap
       (lambda (ts) (follows? prems concl (apply rule ts)))
       (cartesian-exponent targets (procedure-arity rule))))

  (call/1cc
   (lambda (return)
     (for-each
      (lambda (step)
        (define concl (step-conclusion step))
        (define rule  (step-rule step))
        (define ok?
          (if (procedure? rule)
              (handle-general-step concl rule)
              (follows? prems concl rule)))
        (if ok?
            (set! prems (cons concl prems))
            (begin
              (fail concl (if (procedure? rule) (placeholder-saturate rule) rule))
              (return #f))))
      (proof-steps proof))
     (when (or (member #f prems) (premises<=? goals prems))
       (return #t))
     (format #t "Unsolved goals:\n~{~a\n~}~{⊢ ~a\n~}\n"
             prems (filter (lambda (g) (not (member g prems))) goals)))))

;; TODO: i can just guess lol
;; this really isn't far from the macroless version....
(define and-comm
  (proof (p q)
    (argument (p q)
      [(pand p q)]
      [(pand q p)])
    [p (simplification p q)]
    [q (simplification p q)]
    [(pand q p) (conjunction q p)]))

(define and-comm-ez
  (proof (p q)
    (argument (p q)
      [(pand p q)]
      [(pand q p)])
    [p simplification]
    [q simplification]
    [(pand q p) conjunction]))