     (vector-access? rule)))
 
 
-(defn infer-type [rule])
-
-
-;Get the type of the other element of the binary relationship
+(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)
-    (infer-type (.getChild (.getParent rule) 2))
-    (infer-type (.getChild (.getParent rule) 0))))
+    (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]

    (parentheses-expression? rule) (dump-parentheses rule)
    (logical-expression? rule) (visit-infix-expression rule)
    (arithmetic-expression? rule) (visit-infix-expression rule)
    (unary? rule) (visit-unary rule)
    (ternary? rule) (visit-ternary rule)
    (method-call? rule) (visit-method-call rule)

    (= op "%")))


(defn comparison-operator? [op]
  (or
    (= op ">") 
    (= op ">=") 
    (= op "<") 
    (= op "<="))) 


(defn unary-operator? [op]
  (or
    (= op "++")
