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


;; subsumption

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

(define remove-subsumptions
  (lambda (res-cl cls clsp)
    (fresh (a d res c1 c2)
      (conde
        [(== cls '()) (== clsp '())]
        [(== `(,a . ,d) cls)
         (condu
          [(fresh ()
             (copy-termo res-cl c1)
             (copy-termo a c2)
             (subsumes c1 c2))
           (remove-subsumptions res-cl d clsp)]
          [(== `(,a . ,res) clsp)
           (remove-subsumptions res-cl d res)])]))))



(define proof-loop
  (lambda (given cls proof out)
    (fresh (cl ncl cl-f given-f lit1 lit2 neg res1 res2 res-cl cl-copy given-copy clsp)
      (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
       [(tautologyo res-cl)
        fail]
       [succeed])

      (conda
       [(fresh (ncl) (membero ncl cls) (subsumes ncl res-cl))
        fail]
       [succeed])

      (remove-subsumptions res-cl cls clsp)

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