Cacher is the code snippet organizer for pro developers

;; Adolfo Neto, 2011
;; A signed formula will be represented as
	;; (SIGN (CONECTIVE formula))
;; I am not representing atomic formulas yet...


(defn getsign [formula]
  "gets the sign of a signed formula"
  (first formula)
  )

(defn getconnective [formula]
  "gets the main connective of the signed formula"
  (first (second formula))
  )

(defn TAnd
  "Applies the T-AND rule to the formula.
   Example: T A&B ==> T A, T B
   "
  [formula]
  (if (and
       (= (getsign formula) 'T)
       (= (getconnective formula) '&)
       )
    (vector
     (vector 'T (second (second formula)))
     (vector 'T (nth (second formula) 2))
     )
    'nil)
 )

;; Adolfo Neto, 2011
;; 03/02/2011

(use 'clojure.test)

(load-file "formula.clj")

(def t-and-example '[T [& A B]])
(def t-and-example-2 '[T [& C D]])

(deftest getsign-test
  (is (= 'T (getsign t-and-example)))
  )

(deftest getconnective-test
  (is (= '& (getconnective t-and-example)))
  )

(deftest tand-test
  (is (= '[[T A] [T B]] (TAnd t-and-example)))
  (is (= '[[T C] [T D]] (TAnd t-and-example-2)))
  )

(run-tests)