(load "mk.scm")
(load "pmatch.scm")
(load "copy-term.scm")
(load "cnf.scm")

(print-gensym #f)

(define ~~ ==)
(define == ==-unchecked)

(define negateo
  (lambda (tm neg)
    (fresh (na nd)
      (conde
        [(== `(not ,neg) tm)]
        [(never-pairo tm) (== `(not ,tm) neg)]
        [(== `(,na . ,nd) tm)
         (never-equalo na 'not)
         (== `(not ,tm) neg)]))))

(define res-step
  (lambda (cls out)
    (fresh (cl1 cl2 ccl1 ccl2 lit1 lit2 new-cls res-cl res-cl1 res-cl2 neg)
      (conde
        [(membero cl1 cls)
         (membero cl2 cls)
         (never-equalo cl1 cl2)
         
         (copy-termo cl1 ccl1)
         (copy-termo cl2 ccl2)
         
         (rembero lit1 ccl1 res-cl1)
         (rembero lit2 ccl2 res-cl2)
         
         (negateo lit2 neg)
         (~~ lit1 neg)
         
         (appendo res-cl1 res-cl2 res-cl)
         (== `(,res-cl . ,cls) out)]
        
        [(rembero cl1 cls new-cls)
         (factor-clauseo cl1 res-cl)
         (== `(,res-cl . ,new-cls) out)]))))

(define proof-loop
  (lambda (cls)
    (fresh (new-cls)
      (res-step cls new-cls)
      (conde
        [(membero '() new-cls)]
        [(proof-loop new-cls)]))))


(define factor-clauseo
  (lambda (ls out)
    (fresh (a d res copy)
      (conde
        [(== '() ls) (== '() out)]
        [(== `(,a . ,d) ls)
         (copy-termo a copy)
         (conde
           [(membero copy d) (factor-clauseo d out)]
           [(never-membero copy d)
            (factor-clauseo d res)
            (== `(,a . ,res) out)])]))))

(define resproveo
  (lambda (cls proof)
    (fresh (cls-o given ncls ocls ocls2)
      (proof-loop cls)
      (== proof 'done))))

(define prove
  (lambda (axioms thm)
    (let ((thm (clausal `(not ,thm)))
          (axioms (clausal (build-and axioms))))
      (printf "num clauses: ~s\n" (+ (length axioms) (length thm)))
      (pretty-print thm)
      (pretty-print axioms)
      (printf "--\n")
      (let ((result (run 1 (q)
                         (resproveo (append axioms thm) q))))
        (if (null? result)
            (error 'prove "failed to prove")
            (pretty-print result))))))

;; some extra utilities
(define build-and
  (lambda (ax)
    (cond
      [(null? ax) '()]
      [(null? (cdr ax)) (car ax)]
      [else `(and ,(car ax) ,(build-and (cdr ax)))])))

(define appendo 
  (lambda (l1 l2 l3)
    (conde
      ((== l1 '()) (== l2 l3))
      ((fresh (x l11 l31)
         (== l1 (cons x l11))
         (== l3 (cons x l31))
         (appendo l11 l2 l31))))))

(define membero
  (lambda (x ls)
    (fresh (a d)
      (== `(,a . ,d) ls)
      (conde
        [(~~ x a)]
        [(membero x d)]))))

(define rembero
  (lambda (x s1 sn)
    (fresh (a d res)
      (== `(,a . ,d) s1)
      (conde
        [(~~ x a) (== sn d)]
        [(rembero x d res)
         (== `(,a . ,res) sn)]))))

(define never-membero
  (lambda (x ls)
    (fresh (a d res)
      (conde
        [(== '() ls)]
        [(== `(,a . ,d) ls)
         (never-equalo x a)
         (never-membero x d)]))))