;; cnf related stuff
(define-syntax A
  (syntax-rules ()
    ((A var body) `(forall var ,(lambda (var) `body)))))

(define-syntax E
  (syntax-rules ()
    ((E var body) `(ex var ,(lambda (var) `body)))))

(define subst-fm
  (lambda (fml)
    (cond
      ((not (pair? fml)) fml)
      ((eq? (car fml) 'forall) (let ((v (var (cadr fml))))
                                 `(forall ,v ,(subst-fm ((caddr fml) v)))))
      ((eq? (car fml) 'ex) (let ((v (var (cadr fml))))
                             `(exists ,v ,(subst-fm ((caddr fml) v)))))
      (else (cons (car fml) (map subst-fm (cdr fml)))))))

(define nnf
  (lambda (fml)
    (pmatch fml
      ((not (not ,a)) ()
       (nnf  a))
      ((not (forall ,var ,gfml)) ()
       (nnf  `(ex ,var ,(lambda (x) `(not ,(gfml x))))))
      ((not (ex ,var ,gfml)) ()
       (nnf  `(forall ,var ,(lambda (x) `(not ,(gfml x))))))
      ((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)))))
      ((forall ,varx ,gfml) ()
       (nnf (gfml (var varx))))
      ((and . ,fmls) ()
       `(and ,@(map (lambda (x) (nnf  x)) fmls)))
      ((or . ,fmls) ()
       `(or ,@(map (lambda (x) (nnf  x)) fmls)))
      ((ex ,v ,gfml) ()
       (let* ((fvars (rem-dups (fv (subst-fm `(ex ,v ,gfml)))))
              (fml-ex `(,(gensym) . ,fvars))
              (fml-sk (gfml fml-ex)))
         (nnf  fml-sk)))
      (else fml))))

(define fv
  (lambda (fml)
    (pmatch fml
      [,x (var? x) (list x)]
      [(not ,x) () (fv x)]
      [(,op ,x ,y) (member op '(and or => <=>)) (append (fv x) (fv y))]
      [(forall ,x ,t) () (remq x (fv t))]
      [(exists ,x ,t) () (remq x (fv t))]
      [(,f . ,args) () (apply append (map fvt args))]
      [else '()])))

(define fvt
  (lambda (fml)
    (pmatch fml
      [,x (var? x) (list x)]
      [(,f . ,args) () (apply append (map fvt args))]
      [else '()])))


;; cnf

(define distrib2
  (lambda (s1 s2)
    (cond
      [(null? s1) '()]
      [else (append (map (lambda (x) (append (car s1) x)) s2)
                    (distrib2 (cdr s1) s2))])))

(define rem-dups
  (lambda (ls)
    (cond
      [(null? ls) '()]
      [(member (car ls) (cdr ls)) (rem-dups (cdr ls))]
      [else (cons (car ls) (rem-dups (cdr ls)))])))

(define purecnf
  (lambda (fm)
    (pmatch fm
      [() () '()]
      [(or ,p ,q) () (distrib2 (purecnf p) (purecnf q))]
      [(and ,p ,q) () (append (purecnf p) (purecnf q))]
      [else (list (list fm))])))

(define negate
  (lambda (fml)
    (pmatch fml
      [(not ,a) () a]
      [,a () `(not ,a)])))

(define nontautology?
  (lambda (cl)
    (cond
      [(null? cl) #t]
      [(member (negate (car cl)) (cdr cl)) #f]
      [else (nontautology? (cdr cl))])))

(define filter
  (lambda (f ls)
    (cond
      [(null? ls) '()]
      [(f (car ls)) (cons (car ls) (filter f (cdr ls)))]
      [else (filter f (cdr ls))])))

(define clausal
  (lambda (fml)
    (filter nontautology? (map rem-dups (purecnf (nnf fml))))))