(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 hits 0)
(define cache '())

(define resolv-cl
  (lambda (given cl res-cl)
    (fresh (cl-copy given-copy cl-f given-f res1 res2 lit1 lit2 neg)
      (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))))

(define resolv-cls
  (lambda (given cls res-cls)
    (fresh (cl res-cl res rest)
      (conde
        [(== '() cls) (== '() res-cls)]
        [(== `(,cl . ,rest) cls)
         (resolv-cls given rest res)
         (conda
           [(resolv-cl given cl res-cl)
            (== `(,res-cl . ,res) res-cls)]
           [(== res res-cls)])]))))

(define proof-loop
  (lambda (used unused)
    (fresh (cl rest usedp res-cls news unusedp)
      (== `(,cl . ,rest) unused)
      (== `(,cl . ,used) usedp)
      (resolv-cls cl usedp res-cls)
      (appendo rest res-cls news)

      ;;(incorporate cl res-cls rest news)

      (project (res-cls)
        (begin
          (cond
            [(member res-cls cache) (set! hits (add1 hits))]
            [else (set! cache (cons res-cls cache))])
          succeed))

      (project (used unused)
        (begin (printf "used: ~s, unused: ~s\n" (length used) (length unused))
               succeed))

      (conda
       [(membero '() res-cls)]
       [(proof-loop usedp news)]))))

(define factor-clauseo
  (lambda (ls out)
    (fresh (a d res)
      (conda
       [(== `() ls) (== `() out)]
       [(== `(,a . ,d) ls)
        (conda
         [(membero a d) (factor-clauseo d out)]
         [(factor-clauseo d res)
          (== `(,a . ,res) out)])]))))

(define resproveo
  (lambda (axioms thm proof)
    (fresh (cls)
      (appendo thm axioms cls)
      (proof-loop '() cls))))

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

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

;; some extra utilities

(define tautologyo
  (lambda (cl)
    (fresh (dum1 dum2 lit1 lit2 neg)
      (membero lit1 cl)
      (membero lit2 cl)
      (negateo lit1 neg)
      (~~ neg lit2))))

(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)
      (condu
        [(~~ x a)]
        [(membero x d)]))))

;; weird, conda works but not conde/never-equalo
(define rembero
  (lambda (x s1 sn)
    (fresh (a d res)
      (== `(,a . ,d) s1)
      (conda
        [(~~ x a) (== sn d)]
        [(rembero x d res)
         (== `(,a . ,res) sn)]))))

(define subsumes
  (lambda (x y)
    (fresh (a d res copy inst)
      (conde
        [(== '() x)]
        [(== `(,a . ,d) x)
         (copy-termo a copy)
         (instantiate-termo y inst)
         (membero copy inst)
         (subsumes d y)]))))

(define subsumed-in-ls
  (lambda (x ls)
    (fresh (a d)
      (== `(,a . ,d) ls)
      (conda
        [(subsumes a x)]
        [(subsumed-in-ls x d)]))))

(define replaceo
  (lambda (cl cls out)
    (fresh (a d res)
      (== `(,a . ,d) cls)
      (conda
       [(subsumes cl a) (== `(,cl . ,d) out)]
       [(replaceo cl d res)
        (== `(,a . ,res) out)]))))

(define incorporate
  (lambda (given cls unused out)
    (fresh (a d res)
      (conde
        [(== cls '()) (== out unused)]
        [(== `(,a . ,d) cls)
         (conda
          [(subsumed-in-ls a `(,given . ,unused))
           (incorporate given d unused out)
           (project (a)
             (begin (printf "threw out ~s\n" a) succeed))]
          [(replaceo a unused res)
           (incorporate given d res out)
           (project (a)
             (begin (printf "replaced ~s\n" a) succeed))]
          [(appendo unused `(,a) res)
           (incorporate given d res out)])]))))