#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 (prop? f)
  (or (var? f)
      (and (neg? f)
           (prop? (neg-subf f)))
      (and (disj? f)
           (prop? (disj-left f))
           (prop? (disj-right f)))
      (and (conj? f)
           (prop? (conj-left f))
           (prop? (conj-right f)))))

;; konstruktory

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

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

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

;; selektory

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

(define (conj-left f) (cadr f))
(define (conj-right f) (caddr f))

(define (disj-left f) (cadr f))
(define (disj-right f) (caddr f))


;; zmienne wolne

(define (append xs ys)
  (if (null? xs)
      ys
      (cons (car xs) (append (cdr xs) ys))))


(define (free-vars f)
  (define (help f xs)
    (cond [(neg? f) (help (neg-subf f) xs)]
          [(conj? f) (help (conj-right f) (help (conj-left f) xs))]
          [(disj? f) (help (disj-right f) (help (disj-left f) xs))]
          [else (append xs (list f))]))
  (if (prop? f)
      (remove-duplicates (help f null))
      (display "error - ZLE DANE")))


(define formula (make-conj 'p 'q))

(define formula2 (make-neg (make-disj 'yellow (make-conj 'red 'quartz))))


;; ćwiczenie 3

(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 f xs)
  (cond [(conj? f)]))


;; ćwiczenie 4

(define (nnf? f)
  (cond [(var? f) f]
        [(neg? f)