 
 (defn logical-operator? [op]
   (or 
-    (= op "==") 
-    (= op "!=") 
-    (= op ">") 
-    (= op ">=") 
-    (= op "<") 
-    (= op "<=") 
     (= op "&&") 
     (= op "||")))
 

    (logical-operator? (.getText (.getChild exp 1)))))


(defn arithmetic-expression? [exp]
  (and
    (= (.getChildCount exp) 3)
    (arithmetic-operator? (.getText (.getChild exp 1)))))


(defn unary? [exp]

    (vector-access? rule)))


(defn creates-logic-result? [rule]
  (or
    (logical-expression? rule)
    (comparison-expression? rule)))


(defn match-inferior-type [rule]
  (cond 
    (logical-expression? rule) :bool
    (comparison-expression? rule) :real
    (arithmetic-expression? rule) :real
    :else nil))


(defn match-literal-type [term]
  (cond
    (.contains (.toString (.getPayload term)) "<53>") :bool
    (.contains (.toString (.getPayload term)) "<54>") :uninterpreted
    (.contains (.toString (.getPayload term)) "<52>") :real
    (.contains (.toString (.getPayload term)) "<51>") :real
    (.contains (.toString (.getPayload term)) "<55>") :uninterpreted
    (.contains (.toString (.getPayload term)) "<56>") :uninterpreted))


;Get the type of the opposite element of the binary relationship
(defn match-symmetric-type [rule]
  (if
    (= (.getChild (.getParent rule) 0) rule)
    (descendent-infer-type (.getChild (.getParent rule) 2))
    (descendent-infer-type (.getChild (.getParent rule) 0))))


(defn match-unary [rule]
  (let [fst (.getChild rule 0)
        sec (.getChild rule 1)
        fsttext (.getText fst)]
    (if
      (unary-operator? fsttext)
      (descendent-infer-type sec)
      (descendent-infer-type fst))))


(defn ascendent-infer-type [rule]
  (loop [ru rule
         vad (.getParent ru)]
    (cond
      ;Top-level boolean expression
      (nil? vad) :bool
      ;Return the reached type
      (match-inferior-type vad) (match-inferior-type vad)
      (and
        (ternary? vad)
        (= (.getChild vad 0) ru)) :bool
      ;Go down on the symmetric type
      (equality-expression? vad) (match-symmetric-type ru)
      ;Keep ascending
      :else (recur vad (.getParent vad)))))


(defn descendent-infer-type [rule]
  (loop [ru rule]
    (cond
      ;Last level expression
      (terminal? ru) (match-literal-type ru)
      ;Give boolean result
      (creates-logic-result? ru) :bool
      (arithmetic-expression? ru) :real
      (creates-identifier? ru) :uninterpreted
      ;Keep descending
      (unary? ru) (match-unary ru)
      (ternary? ru) (recur (.getChild ru 2))
      :else (recur (.getChild ru 0)))))


(defn retrieve-sorts [root]
