(load "resolution.scm")

(define proof-loop
  (lambda (given cls setsup proof out)
    (fresh (cl ncl cl-f given-f lit1 lit2 neg res1 res2 res-cl cl-copy given-copy)
      (membero cl cls)
      (copy-termo cl cl-copy)
      (copy-termo given given-copy)

      (factor-clauseo cl-copy cl-f)
      (factor-clauseo given-copy given-f)

      (rembero lit1 cl-f res1)
      (rembero lit2 given-f res2)

      (negateo lit2 neg)
      (~~ lit1 neg)
            
      (appendo res1 res2 res-cl)

      (conda
       [(fresh () (membero cl setsup) (membero given setsup))  fail]
       [succeed])

      (conda
       [(tautologyo res-cl)
        fail]
       [succeed])

      (conde
        [(== '() res-cl) (== `(() ,cl . ,proof) out)]
        [(proof-loop res-cl `(,given . ,cls) setsup `(,res-cl ,cl . ,proof) out)]))))

(define resproveo
  (lambda (axioms thm setsup proof)
    (fresh (cls-o given ncls ocls ocls2)
      (rembero given thm ncls)
      (appendo ncls axioms ocls)
      (proof-loop given ocls setsup `(,given) proof))))

(define prove
  (lambda (axioms thm)
    (let ((thm (clausal `(not ,thm)))
          (axioms (make-axioms axioms thm)))
      (let ((setsup (set-of-support (append axioms thm))))
        (printf "num clauses: ~s\n" (+ (length axioms) (length thm)))
        (printf "set of support size: ~s\n" (length setsup))
        (pretty-print thm)
        (pretty-print axioms)
        (pretty-print setsup)
        (printf "--\n")
        (let ((result (run 1 (q)
                           (resproveo axioms thm setsup q))))
          (pretty-print result))))))

(define make-axioms
  (lambda (axioms thm)
    (clausal (build-and axioms))))

(define negative-clause?
  (lambda (cl)
    (pmatch cl
      [() () #t]
      [((not ,x) . ,rest) () (negative-clause? rest)]
      [else #f])))

(define set-of-support
  (lambda (cls)
    (filter negative-clause? cls)))