Add stub for the typechecker

nbe.rkt

@@ -1,6 +1,4 @@
 #lang typed/racket
-;; Grammar (Λ)
-;; t := λ t | app t t | i
 
 (define-type denv (-> V (Promise D)))
 (define-type V Nonnegative-Integer)

type-checker.rkt

@@ -1,2 +1,30 @@
 #lang typed/racket
+
 (require "nbe.rkt")
+
+(define-type context (Immutable-HashTable V Term))
+
+(: context-len (-> context V))
+(define (context-len Γ)
+  (hash-count Γ))
+
+(: context-ext (-> context Term context))
+(define (context-ext Γ A)
+  (hash-set Γ (context-len Γ) A))
+
+(: context-get (-> context V Term))
+(define (context-get Γ i)
+  (if (< i (context-len Γ))
+      (subst (λ (j) `(var ,(+ i j 1))) (hash-ref Γ (- (context-len Γ) (add1 i))))
+      (error "context-get: out of bound")))
+
+(: context-empty context)
+(define context-empty (hash))
+
+(: synth (-> context Term Term))
+(define (synth Γ a)
+  (error "unimplmented"))
+
+(: check (-> context Term D Boolean))
+(define (check Γ a A)
+  (error "unimplemented"))