;; 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) (make-pand p (apply pand qs))]))

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

(define por
  (case-lambda
    [() #f]
    [(p) p]
    [(p . qs) (make-por p (apply por 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 (argument->statement arg)
  (apply p-> (append (argument-premises arg)
                     (list (apply pand (argument-conclusions arg))))))

(define (general-argument->statement arg)
  (lambda ps (argument->statement (apply arg ps))))

;; (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 (gensyms n)
  (let loop ([i 0]
             [xs '()])
    (if (>= i n)
        (reverse xs)
        (loop (add1 i)
              (cons (gensym (symbol->string (proof-variable i))) xs)))))

(define (proof-valid? proof%)
  (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 base-targets (append prems goals))
    (define targets
      (apply append base-targets (map (lambda (p) (if (pair? p) (cdr p) '())) base-targets)))
    (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))
       (printf "Proof complete!\n")
       (return #t))
     (printf "Unsolved goals:\n~{~a\n~}~{⊢ ~a\n~}\n"
             (reverse prems)
             (filter (lambda (g) (not (member g prems))) goals))
     #f)))

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

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

(define or.inl
  (argument (p q)
    [p]
    [(por p q)]))

(define or.inr
  (argument (p q)
    [q]
    [(por p q)]))

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

(define or.eliml
  (argument (p q)
    [(por p q)
     (~ p)]
    [q]))

(define or.elimr
  (argument (p q)
    [(por p q)
     (~ q)]
    [p]))

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

(define transitivity
  (argument (p q r)
    [(p-> p q)
     (p-> q r)]
    [(p-> p r)]))

(define cases
  (argument (p q r)
    [(por p q)
     (p-> p r)
     (p-> q r)]
    [r]))

;; TODO: 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]))

;; TODO: make this expressible better 
;; TODO: use proofs for other proofs nicely
;; the mismatch between what is written and what is shown is hideous
;; avoidable by being explicit ig
(define and-assoc.mp 
  (proof (p q r)
    (argument (p q r)
      [(pand p (pand q r))]
      [(pand (pand p q) r)])
    [p simplification]
    [(pand q r) simplification]
    [q simplification]
    [r simplification]
    [(pand p q) conjunction]
    [(pand (pand p q) r) conjunction]))

(proof-valid? and-assoc.mp)