#lang racket

(define (neg t)
  (list 'neg t))
(define (neg-subf t)
  (cadr t))

(define (conj t f)
  (list 'conj t f))
(define (conj-right t)
  (third t))
(define (conj-left t)
  (second t))
(define (disj t f)
  (list 'disj t f))
(define (disj-left t)
  (second t))
(define (disj-right t)
  (third t))

(define (var? t)
  (symbol? t))
(define (neg? t)
  (and (list? t)
       (= 2 (length t))
       (eq? 'neg (car t))))
(define (conj? t)
  (and (list? t)
       (= 3 (length t))
       (eq? 'conj (car t))))
(define (disj? t)
  (and (list? t)
       (= 3 (length t))
       (eq? 'disj (car t))))
(define (prop? f)
  (or (var? f)
      (and (neg? f)
           (prop? (neg-subf f)))
      (and (conj? f)
           (prop? (conj-left f))
           (prop? (conj-right f)))
      (and (disj? f)
           (prop? (disj-left f))
           (prop? (disj-right f)))))

;(define (flatten tree)
;  (define (dfs t l)
  ;  (cond [(leaf? t) l]
     ;     [else
       ;    (dfs (node-left t) (cons (node-val t) (dfs (node-right t) l)))]))
  ;(dfs tree '()))
(define (free-vars xs)
  (define (notin? var list)
    (cond[(null? list) #t]
         [(eq? var (car list)) #f]
         [else (notin? var (cdr list))]))
  (define (rek xs l)
    (cond [(var? xs) (if (notin? xs l)
                         (cons xs l)
                         l)]
          [(lit? xs) (if (notin? (var xs) l)
                         (cons (var xs) l)
                         l)]
          [(neg? xs) (rek (neg-subf xs) l)]
          [(conj? xs) (rek (conj-left xs) (rek (conj-right xs) l))]
          [(disj? xs) (rek (disj-left xs) (rek (disj-right xs) l))]
          [else (display "error")]))
  (rek xs '()))

( define ( gen-vals xs )
(if ( null? xs )
( list null )
( let*
(( vss ( gen-vals ( cdr xs ) ) )
( x ( car xs ) )
( vst ( map ( lambda ( vs ) ( cons ( list x true ) vs ) ) vss ) )
( vsf ( map ( lambda ( vs ) ( cons ( list x false ) vs ) ) vss ) ) )
( append vst vsf ) ) ) )

(define (eval-formula form eval)
  (define (find-val list var)
    (cond[(null? list) (display "error")]
         [(eq? var (caar list)) (cdar list)]
         [else (find-val (cdr list) var)]))
  (define (rek form)
    (cond [(var? form) (find-val eval form)]
          [(lit? form) (xor (negged? form) (find-val eval (var form)))]
          [(neg? form) (not (rek (neg-subf form)))]
          [(conj? form) (and (rek(conj-left form)) (rek(conj-right form)))]
          [(disj? form) (or (rek(disj-left form)) (rek(disj-right form)))]
          [else (display "error")]))
  (rek form))

(define (falsifable-eval? form)
  (let([gen (gen-vals (free-vars form))]) ;; gen - wszystkie wartosciowania
    (define (rek gen)
      (cond[(null? gen) #f]
           [(eval-formula form (car gen)) (rek (cdr gen))] ;; jesli formula jest prawda, dajesz nastepne wartosciowanie
           [else (car gen)])) ;; inito
    (rek gen)))
(define (lit? t)
  (and (eq? 'lit (car t))
       (list? t)
       (= 3 (length t))
       (symbol? (third t))))
(define (lit p t)
  (list 'lit p t))
(define (var t)
  (third t))
(define (negged? t)
  (second t))
(define (nnf? form)
  (cond [(neg? form) (var? (neg-subf form))]
        [(var? form) #t]
        [(lit? form) #t]
        [(conj? form) (and (nnf? (conj-left form)) (nnf? (conj-right form)))]
        [(disj? form) (and (nnf? (disj-left form)) (nnf? (disj-right form)))]))

;(falsifable-eval? (disj 'a (neg (conj 'a 'b))))
(define (convert-to-nnf form)
  (define (neg-this form)
    (cond[(var? form) (lit #t form)]
         [(lit? form) (lit (not (negged? form)) (var form))]
         [(conj? form) (disj (neg-this (conj-left form)) (neg-this (conj-right form)))]
         [(disj? form) (conj (neg-this (disj-left form)) (neg-this (disj-right form)))]
         [(neg? form)  (neg-subf form)]
         [else (display "error")]))
  (define (improve form)
    (cond [(neg? form) (neg-this (neg-subf form))]
          [(var? form) (lit #f form)]
          [(lit? form) form]
          [(conj? form) (conj (improve (conj-left form)) (improve (conj-right form)))]
          [(disj? form) (disj (improve (disj-left form)) (improve (disj-right form)))]
          [else (display "error")]))
  (improve form))

;(convert-to-nnf (neg (conj 'b (conj (lit #t 'v) (disj 'c 'a)))))
;(falsifable-eval? (disj (list 'lit #t 'a) (conj (neg 'a ) 'b)))

(define (cnf? form)
  (define (dnf? form)
    (cond[(null? form) #t]
         [(disj? form) (and (dnf? (disj-left form)) (dnf? (disj-right form)))]
         [(var? form) #t]
         [(lit? form) #t]
         [else #f]))
  (cond[(null? form) #t]
       [(conj? form) (and (cnf? (conj-left form)) (cnf? (conj-right form)))]
       [(not (dnf? form)) #f]
       [else #t]))
(cnf? (conj (conj 'a (disj 'b (conj 'a 'c))) (conj 'a 'v)))