(load "alphamk.scm")

; some syntactic sugar for quantifiers
(define-syntax A
  (syntax-rules ()
    ((A v body) (let* ((nv (nom 'v))
                       (v `(var ,nv)))
                  `(forall ,(tie nv `body))))))

(define-syntax E
  (syntax-rules ()
    ((E v body) (let* ((nv (nom 'v))
                       (v `(var ,nv)))
                  `(exists ,(tie nv `body))))))


(define fv
  (letrec ((rd (lambda (ls)
                 (cond
                   [(null? ls) '()]
                   [(member (car ls) (cdr ls)) (rd (cdr ls))]
                   [else (cons (car ls) (cdr ls))]))))
    (lambda (t)
      (rd (fvt t)))))

(define fvt
  (lambda (t)
    (pmatch t
      [(var (nom-tag ,x)) (list t)]
      [(forall (tie-tag ,v ,t)) (remove `(var ,v) (fvt t))]
      [(exists (tie-tag ,v ,t)) (remove `(var ,v) (fvt t))]
      [(,a . ,d) (guard (pair? a)) (append (fvt a) (fvt d))]
      [(,a . ,d) (fvt d)]
      [else '()])))

(define (nnf fml)
  (pmatch fml

    ; trivial re-writing using the standard tautologies
    ((not (not ,a))
      (nnf  a))
    ((not (forall (tie-tag ,var ,gfml)))
     (nnf `(exists ,(tie var `(not ,gfml)))))
    ((not (exists (tie-tag ,var ,gfml)))
     (nnf `(forall ,(tie var `(not ,gfml)))))
    ((not (and . ,fmls))
      (nnf  `(or ,@(map (lambda (x) `(not ,x)) fmls))))
    ((not (or . ,fmls))
      (nnf  `(and ,@(map (lambda (x) `(not ,x)) fmls))))
    ((=> ,a ,b)
      (nnf  `(or (not ,a) ,b)))
    ((not (=> ,a ,b))
      (nnf  `(and ,a (not ,b))))
    ((<=> ,a ,b)
      (nnf  `(or (and ,a ,b) (and (not ,a) (not ,b)))))
    ((not (<=> ,a ,b))
      (nnf  `(or (and (not ,a) ,b) (and ,a (not ,b)))))

    
    ; propagate inside
    ((and . ,fmls)
      `(and ,@(map nnf fmls)))
    ((or . ,fmls)
      `(or ,@(map nnf fmls)))

    ((forall (tie-tag ,var ,gfml))
     `(forall (tie-tag ,var ,(nnf gfml))))
    
    ((exists (tie-tag ,var ,gfml))
     (let ((sk `(,(gensym) . ,(fv fml))))
       (nnf (replace `(var ,var) sk gfml))))


    ((sk . ,args) `(sk . ,args))
    ((var ,x) fml)
    ((not ,x) `(not ,(nnf x)))
    (,x (guard (symbol? x)) `(var ,x))
    ((,f . ,args) `(app ,f . ,(map nnf args)))))

(define replace
  (lambda (old new fml)
    (let loop ((fml fml))
      (cond
        [(null? fml) '()]
        [(equal? (car fml) old) (cons new (loop (cdr fml)))]
        [(and (pair? (car fml)) (eq? (caar fml) 'var)) fml]
        [(pair? (car fml)) (cons (loop (car fml)) (loop (cdr fml)))]
        [else (cons (car fml) (loop (cdr fml)))]))))

(define succeed
  (lambda (p)
    p))

(define-syntax all
  (syntax-rules ()
    [(_ b0 b ...) (exists () b0 b ...)]))

(define ==-check ==)

(define leantap
  (lambda (fml unexpl literals proof)
    (exists (a b c u new-term neg)

      (conde
        [(== fml `(and ,a . ,b))
         (appendo b unexpl u)
         (leantap a u literals proof)]
        [(== fml `(or ,a))     
         (leantap a unexpl literals proof)]
        [(== fml `(or ,a ,b . ,c))
         (exists (p1 p2)
           (leantap a unexpl literals p1)
           (leantap `(or ,b . ,c) unexpl literals p2)
           (appendo p1 p2 proof))]
        [(fresh (v)
           (exists (x1)
             (== fml `(forall ,(tie v a)))
             (appendo unexpl (list fml) u)
             (subst-fm a x1 v new-term)
             (leantap new-term u literals proof)))]
        [(negateo fml neg)
         (conda              ;; this should be a choice point
           ((exists (ut)
              (untag-term neg ut)
              (membero ut literals)
              (== proof (list ut))))
           ((exists (n ut n-lits)
              (== unexpl `(,n . ,u))
              (untag-term fml ut)
              (== `(,ut . ,literals) n-lits)
              (leantap n u n-lits proof))))]))))



(define untag-term
  (lambda (t out)
    (exists (x res f)
      (conde
        [(== `(not ,x) t) (untag-term x res) (== `(not ,res) out)]
        [(== `(app ,f . ,x) t)
         (mapo untag-term x res)
         (== `(,f . ,res) out)]
        [(== `(var ,x) t) (== x out)]))))


(define negateo
  (lambda (fml neg)
    (exists (a)
      (conde
        ((== fml `(not (var ,a))) (== `(var ,a) neg))
        ((== `(var ,a) fml) (== `(not ,fml) neg))
        ((== `(app . ,a) fml) (== `(not ,fml) neg))
        ((== `(not (app . ,a)) fml) (== `(app . ,a) neg))))))

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


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


(define subst-fm
  (lambda (fml new old out)
    (exists (a b res1 res2 f args resargs body res op n)
      (fresh (var)
        (conde
          [(conde [(== op 'or)] [(== op 'and)])
           (== `(,op . ,a) fml)
           (== `(,op . ,res) out)
           (mapo (lambda (fml out) (subst-fm fml new old out)) a res)]
          [(== `(app ,f . ,args) fml)
           (== `(app ,f . ,resargs) out)
           (mapo (lambda (fml out) (subst-fm fml new old out)) args resargs)]
          [(== `(forall ,(tie var body)) fml)
           (== `(forall ,(tie var res)) out)
           (hash var old)
           (subst-fm body new old res)]
          [(== `(var ,a) fml)
           (conde
             [(== a old) (== `(var ,new) out)]
             [(hash old a) (== `(var ,a) out)])]
          [(== `(not ,a) fml)
           (== `(not ,res) out)
           (subst-fm a new old res)])))))



(define mapo
  (lambda (rel ls out)
    (exists (a d rres res)
      (conde
        [(== '() ls) (== '() out)]
        [(== `(,a . ,d) ls)
         (== `(,rres . ,res) out)
         (rel a rres)
         (mapo rel d res)]))))



(define (prove axioms theorem)
  (printf "Axioms: ")
  (map (lambda (x) (printf "~s\n" x)) axioms) 
  (printf "Theorem: ~s\n" theorem)
  (let* ((neg-formula `(and (not ,theorem) ,@axioms))
	 (nf (nnf neg-formula)))
    (printf "NNF is:\n")
    (pretty-print nf)
    (newline)
    (printf "The proof is: ~s\n\n" 
      (run 1 (q) (leantap nf '() '() q)))))