(ns lab4
  (:require [clojure.test :refer :all]))

(defn variable [name]
  {:pre [(keyword? name)]}
  (list ::var name))

(defn variable? [expr]
  (= (first expr) ::var))

(defn variable-name [v]
  (second v))

(defn same-variables? [v1 v2]
  (and
    (variable? v1)
    (variable? v2)
    (= (variable-name v1)
       (variable-name v2))))

(defn args [expr] (rest expr))

(defn constant [val]
  {:pre [(boolean? val)]}
  (list ::const val))

(defn constant? [expr]
  (= (first expr) ::const))

(defn constant-value [expr]
  {:pre [(constant? expr)]}
  (second expr))

(defn atom? [expr] (or (variable? expr) (constant? expr)))

(defn applyToArgs [func expr]
  (cons (first expr) (map func (args expr)))
  )

(defn negation? [expr]
  (= (first expr) ::neg))

; disjunction
(defn disjunction [expr1 expr2]
  (cond
    (and (constant? expr1) (= true (constant-value expr1))) (constant true)
    (and (constant? expr1) (= false (constant-value expr1))) expr2
    (and (constant? expr2) (= true (constant-value expr2))) (constant true)
    (and (constant? expr2) (= false (constant-value expr2))) expr1
    :else (cons ::disj (list expr1 expr2))))

(defn disjunction? [expr]
  (= (first expr) ::disj))

(deftest disjunction_test
  (testing "disj basic"
    (let [c (disjunction (variable :x) (variable :y))]
      (is (disjunction? c))
      (is (same-variables? (first (args c)) (variable :x)))
      (is (same-variables? (second (args c)) (variable :y))))
    )
  (testing "disj with const"
    (is (same-variables? (disjunction (variable :x) (constant false)) (variable :x)))
    (is (same-variables? (disjunction (constant false) (variable :x)) (variable :x)))
    (is (= (disjunction (variable :x) (constant true)) (constant true)))
    (is (= (disjunction (constant true) (variable :x)) (constant true)))
    )
  )

; conjunction
(defn conjunction [expr1 expr2]
  (cond
    (and (constant? expr1) (= true (constant-value expr1))) expr2
    (and (constant? expr1) (= false (constant-value expr1))) (constant false)
    (and (constant? expr2) (= true (constant-value expr2))) expr1
    (and (constant? expr2) (= false (constant-value expr2))) (constant false)
    (not (or (variable? expr1) (negation? expr1))) (applyToArgs (fn [expr] (conjunction expr expr2)) expr1)
    (not (or (variable? expr2) (negation? expr2))) (applyToArgs (fn [expr] (conjunction expr1 expr)) expr2)
    :else (cons ::conj (list expr1 expr2)))
  )

(defn conjunction? [expr]
  (= (first expr) ::conj))

(deftest conjunction_test
  (testing "conj basic"
    (let [c (conjunction (variable :x) (variable :y))]
      (is (conjunction? c))
      (is (same-variables? (first (args c)) (variable :x)))
      (is (same-variables? (second (args c)) (variable :y))))
    )
  (testing "conj with const"
    (is (= (conjunction (variable :x) (constant false)) (constant false)))
    (is (= (conjunction (constant false) (variable :x)) (constant false)))
    (is (same-variables? (conjunction (variable :x) (constant true)) (variable :x)))
    (is (same-variables? (conjunction (constant true) (variable :x)) (variable :x)))
    )
  (testing "distributive"
    (let [d1 (disjunction (variable :x) (variable :y))
          d2 (disjunction (variable :y) (variable :x))
          c (conjunction d1 d2)]
      )
    )
  )

; negation
(defn negation [expr]
  (cond
    (negation? expr) (first (args expr))
    (constant? expr) (constant (not (constant-value expr)))
    (variable? expr) (list ::neg expr)
    (conjunction? expr) (disjunction (negation (first (rest expr))) (negation (second (rest expr))))
    (disjunction? expr) (conjunction (negation (first (rest expr))) (negation (second (rest expr))))
    ))

(deftest negation_test
  (testing "negation basic"
    (let [c (negation (variable :x))]
      (is (negation? c))
      (is (same-variables? (first (args c)) (variable :x))))
    (is (same-variables? (negation (negation (variable :x))) (variable :x)))
    )
  (testing "negation with const"
    (is (= (constant-value (negation (constant true))) false))
    (is (= (constant-value (negation (constant false))) true))
    )
  )

; implication
(defn implication [expr1 expr2]
  (disjunction (negation expr1) expr2))

(deftest implication_test
  (testing "impl with const"
    (is (same-variables? (negation (implication (variable :x) (constant false))) (variable :x)))
    (is (= (implication (constant false) (variable :x)) (constant true)))
    (is (= (implication (variable :x) (constant true)) (constant true)))
    (is (same-variables? (implication (constant true) (variable :x)) (variable :x)))
    )
  )

(defn print-atom [atom]
  {:pre [(atom? atom)]}
  (if (variable? atom)
    (print (name (variable-name atom)))
    (print (constant-value atom))))

(defn print-expr [expr]
  (cond
    (atom? expr) (print-atom expr)
    (negation? expr) (do
                       (print "~")
                       (print-atom (first (args expr))))
    (conjunction? expr) (do
                          (print "(")
                          (print-expr (first (args expr)))
                          (print ")*(")
                          (print-expr (second (args expr)))
                          (print ")")
                          )
    (disjunction? expr) (do
                          (print-expr (first (args expr)))
                          (print " + ")
                          (print-expr (second (args expr))))
    )
  )


(defn substitute [expr var const]
  {:pre [(variable? var) (constant? const)]}
  (cond
    (and (variable? expr) (same-variables? expr var)) const
    (and (variable? expr) (not (same-variables? expr var))) expr
    (constant? expr) expr
    (conjunction? expr) (conjunction (substitute (first (args expr)) var const) (substitute (second (args expr)) var const))
    (disjunction? expr) (disjunction (substitute (first (args expr)) var const) (substitute (second (args expr)) var const))
    (negation? expr) (negation (substitute (first (args expr)) var const))))

;(println (negation (conjunction (variable :x) (variable :y))))
;(println (negation (disjunction (variable :x) (variable :y))))
;(println (conjunction (variable :x) (variable :b)))
;(println (disjunction (variable :x) (variable :b)))

;(print-expr (variable :x))
;(print-expr (constant false))
;(print-expr (disjunction (conjunction (negation (variable :a)) (variable :b)) (conjunction (variable :c) (variable :d))))
;(println)
;(print (implication (disjunction (variable :x) (variable :y)) (conjunction (variable :x) (variable :y))))


;(run-tests 'lab4)

;(let [i1 (implication (variable :x) (variable :y))
;      i2 (implication (variable :y) (variable :x))
;      c (conjunction i1 i2)
;      cx (substitute c (variable :y) (constant true))
;      dnf (substitute c (variable :z) (constant true))]
;  (do
;    (print-expr c)
;    (println)
;    (print-expr cx)
;    (println)
;    (print-expr dnf)
;    ))

;(let [d1 (disjunction (variable :x) (variable :y))
;      d2 (disjunction (variable :a) (variable :b))
;      c (conjunction d1 d2)]
;  (do
;    ;(print-expr (applyToArgs (fn [expr] (negation expr)) d1))
;    ;(println)
;    (print-expr c))
;  )


;(let [d1 (disjunction (negation (variable :x)) (variable :y))
;      d2 (disjunction (negation (variable :y)) (variable :x))
;      c (conjunction d1 d2)]
;  (do
;    (print-expr c))
;  )


(let [i1 (implication (variable :x) (variable :y))
      i2 (implication (variable :y) (variable :x))
      c (conjunction i1 i2)]
  (do
    (println c)
    (print-expr c)
    )
  )

;(let [expr (disjunction (variable :x) (variable :y))
;      expr_withTrue (substitute expr (variable :x) (constant true))
;      x (variable :x)
;      x_withTrue (substitute x (variable :x) (constant true))]
;  (do
;    (print-expr expr)
;    (println)
;    (print-expr expr_withTrue)))