 (defn env-put [env x t]
   (conj env [x t]))
 
+(defn mk-env [& args]
+  args)
+
+
 ;;{
 ;; ## Synthesis rules
 ;;}

(ns typetheory.typing
  (:require [clj-by.example :refer [example do-for-example]])
  (:require [clojure.spec :as s])
  (:require [clojure.test.check :as tc])
  (:require [clojure.test.check.generators :as gen])
  (:require [clojure.test.check.properties :as prop])
  (:require [typetheory.syntax :as sx])
  (:require [typetheory.beta :as b])
  )

(def ^:private +examples-enabled+)

;;          E |- rator rand : B [rand/x]
;;}

(defn type-of-app [def-env env rator rand]
  (let [[status trator] (type-of def-env env rator)]
    (if (= status :ko)
      [:ko {:msg "Cannot calculate operator (left-hand) type in application."
            :term [rator rand] :from trator}]
      (let [trator' (norm/normalize def-env trator)]
        (if (not (stx/prod? trator'))
          [:ko {:msg "Not a product type for operator (left-hand) in application." :term [rator rand] :operator-type trator}]
          (let [[_ [x A] B] trator']
            (if (not (type-check? def-env env rand A))
              [:ko {:msg "Cannot apply: type mismatch" :term [rator rand] :domain A :operand rand}]
              [:ok (stx/subst B x rand)])))))))


(example
 (type-of {} '[[bool :type] [y bool]]
          '[(lambda [x bool] x) y])
 => '[:ok bool])


;;{
;;    D |- ref :: [x1 t1] [x2 t2] ... [xN tN] -> t
;;    E |- e1 :: t1   E, x1:t1 |- e2 :: t2
;;    ...
;;    E, x1:t1, ..., xM-1:tM-1 |- eM :: tM
;; -------------------------------------------------------------------------------------
;;      D, E |- (ref e1 e2 ... eM)
;;              ::> (prod [xM+1 tM+1] ... (prod [xN tN] t [e1/x1, e2/x2, ...eM/xM]) ...)
;;}

