variable_names.clj

(ns logic-introduction.core
    (:refer-clojure :exclude [inc reify ==])
    (:use [clojure.core.logic minikanren prelude nonrel match disequality]))

(defn geto [key env value]
  (matche [env]
          ([[[key :- value] . _]])
          ([[_ . ?rest]] (geto key ?rest value))))

(defn typedo [context exp resulttype]
  (conde
    ((geto exp context resulttype))
    ((matche [context exp resulttype]
             ([_ [:apply ?fun ?arg] _]
              (exist [argtype]
                     (!= ?fun ?arg)
                     (typedo context ?arg argtype)
                     (typedo context ?fun [argtype :> resulttype])))))))