#lang racket


(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 (literal? l)
  (or (var? l)
      (and (neg? l)
           (var? (neg-subf l)))))

(define (make-neg t)
  (list 'neg t))

(define (neg-subf f)
  (cadr f))

(define (make-conj l p)
  (list 'conj l p))

(define (make-disj l p)
   (list 'disj l p))

(define (disj-left f)
  (second f))

(define (disj-rght f)
  (third f))

(define (conj-left f)
  (second f))

(define (conj-rght f)
  (third f))

(define (concat-map f x)
  (apply append (map f x)))

(define (make-nnf formula)
  (cond [(var? formula) formula]
        [(conj? formula) (make-conj (make-nnf (conj-left formula)) (make-nnf (conj-rght formula)))]
        [(disj? formula) (make-disj (make-nnf (disj-left formula)) (make-nnf (disj-rght formula)))]
        [(neg? formula) (nnf-help (neg-subf formula))]))

(define (nnf-help f)
  (cond [(var? f) (make-neg f)]
        [(neg? f) (make-nnf (neg-subf f))]
        [(conj? f) (make-disj (nnf-help (conj-left f)) (nnf-help (conj-rght f)))]
        [(disj? f) (make-conj (nnf-help (disj-left f)) (nnf-help (disj-rght f)))]))



;; --------------------ćw 6

;;konsultacja Klaudia Osowska
(define (cnf? f)
  (define (ok? x)
    (and (list? x)
         (= (length x) (length (filter literal? x)))))
  (and (list? f)
       (or (and (= (length f) 1) (ok? (car f)))
           (and (ok? (car f)) (cnf? (cdr f))))))


;;implementacja algorytmu udowodnienego na repetytorium
(define (make-cnf formula)
  (cond [(literal? formula) (list (list formula))]
        [(conj? formula) (append (make-cnf (conj-left formula)) (make-cnf (conj-rght formula)))]
        [(disj? formula) (cnf-help (make-cnf (disj-left formula)) (make-cnf (disj-rght formula)))]))

(define (cnf-help  f1 f2)
  (concat-map (lambda (x) (map (lambda (y) (append x y)) f2)) f1))


;;testy
(define test1 (make-conj (make-conj 'p 'q) (make-disj 't 's)))
(make-cnf (make-nnf test1))

(define test2 (make-disj (make-conj 'p 'q) (make-disj 't 's)))
(make-cnf (make-nnf test2))

(define test3 (make-conj (make-disj 'p 'q) (make-disj (make-neg 't) 's)))
(make-cnf (make-nnf test3))

(define test4 (make-disj (make-conj 'p 'q) (make-conj 't 's)))
(cnf? (make-cnf (make-nnf test4)))