src/lambda/tli.clj

   1 (ns lambda.tli
   2   (:refer-clojure :exclude [==])
   3   (:use [clojure.core.logic :exclude [is] :as l]))
   4
   5 ;;; utilities
   6 (defn reifier-for [tag x]
   7   (fn [c v r a]
   8     (let [x (walk* r (walk* a x))]
   9       (when (symbol? x)
  10         `(~tag ~x)))))
  11 (defn symbolo [x] (predc x symbol? (reifier-for 'sym x)))
  12
  13
  14 ;;; type := var | [:=> type type]
  15 ;;; exp  := name | (fn [name] exp) | (exp exp)
  16
  17 ;;; env := () | ([name type] . env)
  18 (defn env-lookupo [env x tx]
  19   (fresh [y ty env-rest]
  20          (conso [y ty] env-rest env)
  21          (conde
  22           ((== x y) (== tx ty))
  23           ((!= x y) (env-lookupo env-rest x tx)))))
  24
  25 (defn tio [env e t]
  26   (conde
  27    ((symbolo e) (env-lookupo env e t))
  28    ((fresh [x body tx tbody envx]
  29            (== e `(~'fn [~x] ~body))
  30            (conso [x tx] env envx)
  31            (== t [:=> tx tbody])
  32            (tio envx body tbody)))
  33    ((fresh [e1 e2 t1 t11 t12 t2]
  34            (== e `(~e1 ~e2))
  35            (== t1 [:=> t11 t12])
  36            (== t2 t11)
  37            (== t t12)
  38            (tio env e1 t1)
  39            (tio env e2 t2)))))