From 961a5b7bb9d650d99ad881e6015cc487275eb124 Mon Sep 17 00:00:00 2001
From: "William J. Bowman" <wjb@williamjbowman.com>
Date: Tue, 12 Jan 2016 19:07:19 -0500
Subject: [PATCH] Rewrote Olly

Olly is now properly designed. This also fixes some issues with binding,
i.e. fixes #32, and extraction to Coq and Latex
Makes progress on #9.
---
 cur-doc/cur/scribblings/olly.scrbl | 118 ++---
 cur-lib/cur/olly.rkt               | 668 +++++++++++++++++------------
 cur-test/cur/tests/olly.rkt        |  70 +--
 cur-test/cur/tests/stlc.rkt        | 126 +++---
 4 files changed, 537 insertions(+), 445 deletions(-)

diff --git a/cur-doc/cur/scribblings/olly.scrbl b/cur-doc/cur/scribblings/olly.scrbl
index 59b04ce..0556ebd 100644
--- a/cur-doc/cur/scribblings/olly.scrbl
+++ b/cur-doc/cur/scribblings/olly.scrbl
@@ -14,11 +14,11 @@ the language.
            maybe-vars
            maybe-output-coq
            maybe-output-latex
-           (nt-name (nt-metavars) maybe-bnfdef constructors ...) ...)
+           (nt-name (nt-metavar ...) maybe-bnfdef non-terminal-def ...) ...)
          #:grammar
          [(maybe-vars
             (code:line)
-            (code:line #:vars (nt-metavars ...)))
+            (code:line #:vars (nt-metavar ...)))
          (maybe-output-coq
             (code:line)
             (code:line #:output-coq coq-filename))
@@ -27,26 +27,51 @@ the language.
             (code:line #:output-latex latex-filename))
          (maybe-bnfdef
             (code:line)
-            (code:line ::=))]]{
+            (code:line ::=))
+	 (non-terminal-def
+	    nt-metavar
+            (code:line terminal)
+            (code:line (terminal terminal-args ...)))
+	 (terminal-args
+	    nt-metavar
+	    (code:line literal)
+	    (code:line ())
+	    (code:line (#:bind nt-metavar . terminal-args))
+	    (code:line (terminal-args terminal-args ...)))]]{
 Defines a new language by generating inductive definitions for each
-nonterminal @racket[nt-name], whose constructors are generated by
-@racket[constructors]. The constructors must either with a tag that can
-be used to name the constructor, or be another meta-variable.
-The meta-variables @racket[nt-metavars] are replaced by the corresponding
-inductive types in @racket[constructors].
-The name of each inductive datatype is generated by
-@racket[(format-id "~a-~a" name nt-name)].
+non-terminal @racket[nt-name], whose syntax is generated by
+@racket[non-terminal-def].
+Each @racket[non-terminal-def] must either be a reference to a
+previously defined non-terminal using a @racket[nt-metavar], a
+@racket[terminal] (an identifier), or a @racket[terminal] applied to
+some @racket[terminal-args].
+The @racket[terminal-args] are a limited grammar of s-expressions,
+which can reference previously defined @racket[nt-metavar]s to be
+treated as arguments, literal symbols to be treated as syntax, binding
+declarations, or a nested @racket[terminal-arg].
 
-Later nonterminals can refer to prior nonterminals, but they cannot be
-mutually inductive due to limitations in Cur. When nonterminals appear
-in @racket[constructors], a constructor is defined that coerces one
-nonterminal to another.
+The inductive definitions are generated by generating a type for each
+@racket[nt-name] whose name @racket[nt-type] is generated by
+@racket[(format-id name "~a-~a" name nt-name)] and whose constructors
+are generated by each @racket[non-terminal-def].
+For @racket[terminal]s, the constructor is a base constructor whose
+name is generated by @racket[(format-id name "~a-~a" name terminal)].
+For @racket[nt-metavar]s, the constructor is a conversion constructor
+whose name is generated by @racket[(format-id name "~a->~a" nt-type
+nt-metavar-type)] where @racket[nt-metavar-type] is the name of the
+type generated for the nonterminal to which @racket[nt-metavars] refers.
+For @racket[(terminal terminal-args ...)], the constructor is a
+function that expects term of of the types generated by
+@racket[terminal-args ...].
 
 If @racket[#:vars] is given, it should be a list of meta-variables that
-representing variables in the language. These meta-variables should only
-appear in binding positions in @racket[constructors]. These variables
-are represented as De Bruijn indexes, and Olly provides some functions
-for working with De Bruijn indexes.
+representing variables in the language.
+These variables are represented as De Bruijn indices, and uses of
+variables in the syntax are treated as type @racket[Nat].
+Binding positions in the syntax, represented by @racket[#:bind
+nt-metavar], are erased in converting to De Bruijn indices, although
+this may change if the representation of variables used by
+@racket[define-language] changes.
 
 If @racket[#:output-coq] is given, it should be a string representing a
 filename. The form @racket[define-language] will output Coq versions of
@@ -66,8 +91,8 @@ Example:
   #:output-latex "stlc.tex"
   (val  (v)   ::= true false unit)
   (type (A B) ::= boolty unitty (-> A B) (* A A))
-  (term (e)   ::= x v (app e e) (lambda (x : A) e) (cons e e)
-                  (let (x x) = e in e)))
+  (term (e)   ::= x v (app e e) (lambda (#:bind x : A) e) (cons e e)
+                  (let (#:bind x #:bind x) = e in e)))
 ]
 
 This example is equivalent to
@@ -85,20 +110,17 @@ This example is equivalent to
   (stlc-* : (forall (x : stlc-type) (forall (y : stlc-type) stlc-type))))
 
 (data stlc-term : Type
-  (stlc-var-->-stlc-term : (forall (x : Var) stlc-term))
-  (stlc-val-->-stlc-term : (forall (x : stlc-val) stlc-term))
-  (stlc-term-lambda : (forall (x : Var)
-                        (forall (y : stlc-type)
+  (Var->-stlc-term : (forall (x : Nat) stlc-term))
+  (stlc-val->-stlc-term : (forall (x : stlc-val) stlc-term))
+  (stlc-term-lambda : (forall (y : stlc-type)
                           (forall (z : stlc-term)
-                            stlc-term))))
+                            stlc-term)))
   (stlc-term-cons : (forall (x : stlc-term) (forall (y : stlc-term) stlc-term)))
-  (stlc-term-let : (forall (x : Var)
-                     (forall (y : Var)
-                       (forall (e1 : stlc-term)
-                         (forall (e2 : stlc-term)
-                           stlc-term))))))]
+  (stlc-term-let : (forall (e1 : stlc-term)
+                     (forall (e2 : stlc-term)
+                       stlc-term))))]
 
-@margin-note{This example is taken from @racketmodname[cur/examples/stlc]}
+@margin-note{This example is taken from @racketmodname[cur/tests/stlc]}
 }
 
 @defform[(define-relation (name args ...)
@@ -126,20 +148,20 @@ explain the syntax in detail, here is an example:
   #:output-latex "stlc.tex"
   [(g : Gamma)
    ------------------------ T-Unit
-   (has-type g (stlc-val-->-stlc-term stlc-unit) stlc-unitty)]
+   (has-type g (stlc-val->stlc-term stlc-unit) stlc-unitty)]
 
   [(g : Gamma)
    ------------------------ T-True
-   (has-type g (stlc-val-->-stlc-term stlc-true) stlc-boolty)]
+   (has-type g (stlc-val->stlc-term stlc-true) stlc-boolty)]
 
   [(g : Gamma)
    ------------------------ T-False
-   (has-type g (stlc-val-->-stlc-term stlc-false) stlc-boolty)]
+   (has-type g (stlc-val->stlc-term stlc-false) stlc-boolty)]
 
-  [(g : Gamma) (x : Var) (t : stlc-type)
+  [(g : Gamma) (x : Nat) (t : stlc-type)
    (== (Maybe stlc-type) (lookup-gamma g x) (some stlc-type t))
    ------------------------ T-Var
-   (has-type g (Var-->-stlc-term x) t)]
+   (has-type g (Var->stlc-term x) t)]
 
   [(g : Gamma) (e1 : stlc-term) (e2 : stlc-term)
                (t1 : stlc-type) (t2 : stlc-type)
@@ -151,16 +173,15 @@ explain the syntax in detail, here is an example:
   [(g : Gamma) (e1 : stlc-term) (e2 : stlc-term)
                (t1 : stlc-type) (t2 : stlc-type)
                (t : stlc-type)
-               (x : Var) (y : Var)
    (has-type g e1 (stlc-* t1 t2))
-   (has-type (extend-gamma (extend-gamma g x t1) y t2) e2 t)
+   (has-type (extend-gamma (extend-gamma g t1) t2) e2 t)
    ---------------------- T-Let
-   (has-type g (stlc-let x y e1 e2) t)]
+   (has-type g (stlc-let e1 e2) t)]
 
-  [(g : Gamma) (e1 : stlc-term) (t1 : stlc-type) (t2 : stlc-type) (x : Var)
-   (has-type (extend-gamma g x t1) e1 t2)
+  [(g : Gamma) (e1 : stlc-term) (t1 : stlc-type) (t2 : stlc-type)
+   (has-type (extend-gamma g t1) e1 t2)
    ---------------------- T-Fun
-   (has-type g (stlc-lambda x t1 e1) (stlc--> t1 t2))]
+   (has-type g (stlc-lambda t1 e1) (stlc--> t1 t2))]
 
   [(g : Gamma) (e1 : stlc-term) (e2 : stlc-term)
                (t1 : stlc-type) (t2 : stlc-type)
@@ -179,22 +200,11 @@ This example is equivalent to:
   (T-Unit : (forall (g : Gamma)
               (has-type
                 g
-                (stlc-val-->-stlc-term stlc-unit)
+                (stlc-val->stlc-term stlc-unit)
                 stlc-unitty)))
   ....)]
 }
 
-@deftogether[(@defthing[Var Type]
-              @defthing[avar (forall (x : Nat) Var)])]{
-The type of a De Bruijn variable.
-}
-
-@defproc[(var-equal? [v1 Var] [v2 Var])
-         Bool]{
-A Cur procedure; returns @racket[true] if @racket[v1] and @racket[v2]
-represent the same variable.
-}
-
 @todo{Need a Scribble library for defining Cur/Racket things in the same
 library in a nice way.}
 
diff --git a/cur-lib/cur/olly.rkt b/cur-lib/cur/olly.rkt
index dc4aa06..9b80ced 100644
--- a/cur-lib/cur/olly.rkt
+++ b/cur-lib/cur/olly.rkt
@@ -10,305 +10,425 @@
 (provide
   define-relation
   define-language
-  Var
-  avar
-  var-equal?
   generate-coq
 
   ;; private; exported for testing only
   (for-syntax
-   coq-defns
-   output-latex-bnf
-   output-coq
-   new-name
-   fresh-name))
-
-(begin-for-syntax
-  (define-syntax-class dash
-    (pattern x:id
-             #:fail-unless (regexp-match #rx"-+" (symbol->string (syntax-e #'x)))
-             "Invalid dash"))
-
-  (define-syntax-class decl (pattern (x:id (~datum :) t:id)))
-
-  ;; TODO: Automatically infer decl ... by binding all free identifiers?
-  ;; TODO: Automatically infer decl ... for meta-variables that are the
-  ;; same as bnf grammar.
-  (define-syntax-class inferrence-rule
-    (pattern (d:decl ...
-              x*:expr ...
-              line:dash lab:id
-              (name:id y* ...))
-              #:with rule #'(lab : (-> d ... x* ... (name y* ...)))
-              ;; TODO: convert meta-vars such as e1 to e_1
-              #:attr latex (format "\\inferrule~n{~a}~n{~a}"
-                             (string-trim
-                               (for/fold ([str ""])
-                                        ([hyp (syntax->datum #'(x* ...))])
-                                 (format "~a~a \\+" str hyp))
-                               " \\+"
-                               #:left? #f)
-                             (format "~a" (syntax->datum #'(name y* ...)))))))
-(define-syntax (define-relation syn)
-  (syntax-parse syn
-    [(_ (n:id types* ...)
-        (~optional (~seq #:output-coq coq-file:str))
-        (~optional (~seq #:output-latex latex-file:str))
-        rules:inferrence-rule ...)
-     #:fail-unless (andmap (curry equal? (length (syntax->datum #'(types* ...))))
-                           (map length (syntax->datum #'((rules.y* ...)
-                                                          ...))))
-     "Mismatch between relation declared and relation definition"
-     #:fail-unless (andmap (curry equal? (syntax->datum #'n))
-                           (syntax->datum #'(rules.name ...)))
-     "Mismatch between relation declared name and result of inference rule"
-      (let ([output #`(data n : (-> types* ... Type) rules.rule ...)])
-        ;; TODO: Pull this out into a separate function and test. Except
-        ;; that might make using attritbutes more difficult.
-        (when (attribute latex-file)
-          (with-output-to-file (syntax->datum #'latex-file)
-            (thunk
-              (printf (format "\\fbox{$~a$}$~n$\\begin{mathpar}~n~a~n\\end{mathpar}$$"
-                       (syntax->datum #'(n types* ...))
-                       (string-trim
-                         (for/fold ([str ""])
-                                   ([rule (attribute rules.latex)])
-                           (format "~a~a\\and~n" str rule))
-                         "\\and"
-                         #:left? #f))))
-            #:exists 'append))
-        #`(begin
-            #,@(if (attribute coq-file)
-                   #`((generate-coq #:file coq-file #:exists
-                                    'append #,output))
-                   #'())
-               #,output))]))
-
-(begin-for-syntax
-  (require racket/syntax)
-  (define (new-name name . id*)
-    (apply format-id name (for/fold ([str "~a"])
-                                    ([_ id*])
-                            (string-append str "-~a")) name (map syntax->datum id*)))
-
-  (define (fresh-name id)
-    (datum->syntax id (gensym (syntax->datum id)))))
-
-;; TODO: Oh, this is a mess. Rewrite it.
-(begin-for-syntax
-  (define lang-name (make-parameter #'name))
-  (define nts (make-parameter (make-immutable-hash)))
-
-  (define-syntax-class nt
-    (pattern e:id #:fail-unless (hash-has-key? (nts) (syntax->datum #'e)) #f
-             #:attr name (hash-ref (nts) (syntax->datum #'e))
-             #:attr type (hash-ref (nts) (syntax->datum #'e))))
-
-  (define (flatten-args arg arg*)
-    (for/fold ([ls (syntax->list arg)])
-              ([e (syntax->list arg*)])
-      (append ls (syntax->list e))))
-
-  (define-syntax-class (right-clause type)
-    #;(pattern (~datum var)
-             #:attr clause-context #`(#,(new-name (lang-name) #'var) :
-                                      (-> #,(hash-ref (nts) 'var) #,(hash-ref (nts) type)))
-             #:attr name #'var
-             #:attr arg-context #'(var))
-    (pattern e:nt
-             #:attr clause-context #`(#,(new-name #'e.name #'->
-                                                  (hash-ref (nts) type)) :
-                                      (-> e.type #,(hash-ref (nts) type)))
-             #:attr name (fresh-name #'e.name)
-             #:attr arg-context #'(e.type))
-    (pattern x:id
-             #:attr clause-context #`(#,(new-name (lang-name) #'x) :
-                                      #,(hash-ref (nts) type))
-             #:attr name (new-name (lang-name) #'x)
-             #:attr arg-context #'())
-    (pattern ((~var e (right-clause type)) (~var e* (right-clause type)) ...)
-             #:attr name (fresh-name #'e.name)
-             #:attr clause-context #`(e.name : (-> #,@(flatten-args #'e.arg-context #'(e*.arg-context ...))
-                                                    #,(hash-ref (nts) type)))
-             #:attr arg-context #`(#,@(flatten-args #'e.arg-context #'(e*.arg-context ...)))))
-
-  (define-syntax-class (right type)
-    (pattern ((~var r (right-clause type)) ...)
-             #:attr clause #'(r.clause-context ...)))
-
-  #;(define-syntax-class left
-    (pattern (type:id (nt*:id ...+))
-             #:do ))
-
-  (define-syntax-class nt-clauses
-    (pattern ((type:id (nt*:id ...+)
-              (~do (nts (for/fold ([ht (nts)])
-                                  ([nt (syntax->datum #'(type nt* ...))])
-                          (hash-set ht nt (new-name (lang-name) #'type)))))
-              (~datum ::=)
-              . (~var rhs* (right (syntax->datum #'type)))) ...)
-             #:with defs (with-syntax ([(name* ...)
-                                        (map (λ (x) (hash-ref (nts) x))
-                                             (syntax->datum #'(type ...)))])
-                           #`((data name* : Type . rhs*.clause)
-                              ...)))))
-
-(begin-for-syntax
-  ;; TODO: More clever use of syntax-parse would enable something akin to what
-  ;; define-relation is doing---having attributes that contain the latex
-  ;; code for each clause.
-  ;; TODO: convert meta-vars such as e1 to e_1
-  (define (output-latex-bnf vars clauses)
-    (format "$$\\begin{array}{lrrl}~n~a~n\\end{array}$$"
-      (for/fold ([str ""])
-                ([clause (syntax->list clauses)])
-        (syntax-parse clause
-          #:datum-literals (::=)
-          [(type:id (nonterminal:id ...) ::= exprs ...)
-           (format "\\mbox{\\textit{~a}} & ~a & \\bnfdef & ~a\\\\~n"
-                   (symbol->string (syntax->datum #'type))
-                   (string-trim
-                     (for/fold ([str ""])
-                               ([nt (syntax->datum #'(nonterminal ...))])
-                       (format "~a~a," str nt))
-                     ","
-                     #:left? #f)
-                   (string-trim
-                     (for/fold ([str ""])
-                               ([expr (syntax->datum #'(exprs ...))])
-                       (format "~a~a \\bnfalt " str expr))
-                     " \\bnfalt "
-                     #:left? #f))]))))
-  (define (generate-latex-bnf file-name vars clauses)
-    (with-output-to-file file-name
-      (thunk (printf (output-latex-bnf vars clauses)))
-      #:exists 'append)))
-
-;; TODO: For better error messages, add context, rename some of these patterns. e.g.
-;;    (type (meta-vars) ::= ?? )
-;; TODO: Extend define-language with syntax such as ....
-;;   (term (e) ::= (e1 e2) ((lambda (x) e)
-;                           #:latex "(\\lambda ,x. ,e)"))
-(define-syntax (define-language syn)
-  (syntax-parse syn
-    [(_ name:id (~do (lang-name #'name))
-        (~do (nts (hash-set (make-immutable-hash) 'var #'Var)))
-        (~optional (~seq #:vars (x*:id ...)
-           (~do (nts (for/fold ([ht (nts)])
-                               ([v (syntax->datum #'(x* ...))])
-                       (hash-set ht v (hash-ref ht 'var)))))))
-        (~optional (~seq #:output-coq coq-file:str))
-        (~optional (~seq #:output-latex latex-file:str))
-        . clause*:nt-clauses)
-     (let ([output #`(begin . clause*.defs)])
-       (when (attribute latex-file)
-         (generate-latex-bnf (syntax->datum #'latex-file) #'vars #'clause*))
-       #`(begin
-           #,@(if (attribute coq-file)
-                 #`((generate-coq #:file coq-file #:exists 'append #,output))
-                 #'())
-           #,output))]))
-
-(data Var : Type (avar : (-> Nat Var)))
-
-(define (var-equal? (v1 : Var) (v2 : Var))
-  (match v1
-    [(avar (n1 : Nat))
-     (match v2
-       [(avar (n2 : Nat))
-        (nat-equal? n1 n2)])]))
-
-;; See stlc.rkt for examples
+   typeset-relation
+   typeset-bnf
+   cur->coq))
 
 ;; Generate Coq from Cur:
 
 (begin-for-syntax
   (define coq-defns (make-parameter ""))
+
   (define (coq-lift-top-level str)
     (coq-defns (format "~a~a~n" (coq-defns) str)))
-  ;; TODO: OOps, type-infer doesn't return a cur term but a redex syntax bla
+
   (define (constructor-args syn)
     (syntax-parse (type-infer/syn syn)
       #:datum-literals (Π :)
       [(Π (x:id : t) body)
        (cons #'x (constructor-args #'body))]
       [_ null]))
+
   (define (sanitize-id str)
     (let ([replace-by `((: _) (- _))])
       (for/fold ([str str])
                 ([p replace-by])
         (string-replace str (symbol->string (first p))
                         (symbol->string (second p))))))
-  (define (output-coq syn)
-    (syntax-parse (cur-expand syn #'define #'begin)
-       ;; TODO: Need to add these to a literal set and export it
-       ;; Or, maybe overwrite syntax-parse
-       #:literals (real-lambda real-forall data real-app real-elim define begin Type)
-       [(begin e ...)
-        (for/fold ([str ""])
-                  ([e (syntax->list #'(e ...))])
-          (format "~a~n" (output-coq e)))]
-       [(define name:id body)
-        (begin
-          (coq-lift-top-level
-            (format "Definition ~a := ~a.~n"
-                    (output-coq #'name)
-                    (output-coq #'body)))
-          "")]
-       [(define (name:id (x:id : t) ...) body)
-        (begin
-          (coq-lift-top-level
-            (format "Function ~a ~a := ~a.~n"
-                    (output-coq #'name)
-                    (for/fold ([str ""])
-                              ([n (syntax->list #'(x ...))]
-                               [t (syntax->list #'(t ...))])
-                      (format "~a(~a : ~a) " str (output-coq n) (output-coq t)))
-                    (output-coq #'body)))
-          "")]
-       [(real-lambda ~! (x:id (~datum :) t) body:expr)
-        (format "(fun ~a : ~a => ~a)" (output-coq #'x) (output-coq #'t)
-                (output-coq #'body))]
-       [(real-forall ~! (x:id (~datum :) t) body:expr)
-        (format "(forall ~a : ~a, ~a)" (syntax-e #'x) (output-coq #'t)
-                (output-coq #'body))]
-       [(data ~! n:id (~datum :) t (x*:id (~datum :) t*) ...)
-        (begin
-          (coq-lift-top-level
-            (format "Inductive ~a : ~a :=~a."
-                   (sanitize-id (format "~a" (syntax-e #'n)))
-                   (output-coq #'t)
-                   (for/fold ([strs ""])
-                             ([clause (syntax->list #'((x* : t*) ...))])
-                     (syntax-parse clause
-                       [(x (~datum :) t)
-                        (format "~a~n| ~a : ~a" strs (syntax-e #'x)
-                          (output-coq #'t))]))))
-          "")]
-       [(Type i) "Type"]
-       [(real-elim var t)
-        (format "~a_rect" (output-coq #'var))]
-       [(real-app e1 e2)
-        (format "(~a ~a)" (output-coq #'e1) (output-coq #'e2))]
-       [e:id (sanitize-id (format "~a" (syntax->datum #'e)))])))
+
+  (define (cur->coq syn)
+    (parameterize ([coq-defns ""])
+      (define output
+        (let cur->coq ([syn syn])
+          (syntax-parse (cur-expand syn #'define #'begin)
+            ;; TODO: Need to add these to a literal set and export it
+            ;; Or, maybe overwrite syntax-parse
+            #:literals (real-lambda real-forall data real-app real-elim define begin Type)
+            [(begin e ...)
+             (for/fold ([str ""])
+                       ([e (syntax->list #'(e ...))])
+               (format "~a~n" (cur->coq e)))]
+            [(define name:id body)
+             (begin
+               (coq-lift-top-level
+                (format "Definition ~a := ~a.~n"
+                        (cur->coq #'name)
+                        (cur->coq #'body)))
+               "")]
+            [(define (name:id (x:id : t) ...) body)
+             (begin
+               (coq-lift-top-level
+                (format "Function ~a ~a := ~a.~n"
+                        (cur->coq #'name)
+                        (for/fold ([str ""])
+                                  ([n (syntax->list #'(x ...))]
+                                   [t (syntax->list #'(t ...))])
+                          (format "~a(~a : ~a) " str (cur->coq n) (cur->coq t)))
+                        (cur->coq #'body)))
+               "")]
+            [(real-lambda ~! (x:id (~datum :) t) body:expr)
+             (format "(fun ~a : ~a => ~a)" (cur->coq #'x) (cur->coq #'t)
+                     (cur->coq #'body))]
+            [(real-forall ~! (x:id (~datum :) t) body:expr)
+             (format "(forall ~a : ~a, ~a)" (syntax-e #'x) (cur->coq #'t)
+                     (cur->coq #'body))]
+            [(data ~! n:id (~datum :) t (x*:id (~datum :) t*) ...)
+             (begin
+               (coq-lift-top-level
+                (format "Inductive ~a : ~a :=~a."
+                        (sanitize-id (format "~a" (syntax-e #'n)))
+                        (cur->coq #'t)
+                        (for/fold ([strs ""])
+                                  ([clause (syntax->list #'((x* : t*) ...))])
+                          (syntax-parse clause
+                            [(x (~datum :) t)
+                             (format "~a~n| ~a : ~a" strs (syntax-e #'x)
+                                     (cur->coq #'t))]))))
+               "")]
+            [(Type i) "Type"]
+            [(real-elim var t)
+             (format "~a_rect" (cur->coq #'var))]
+            [(real-app e1 e2)
+             (format "(~a ~a)" (cur->coq #'e1) (cur->coq #'e2))]
+            [e:id (sanitize-id (format "~a" (syntax->datum #'e)))])))
+      (format
+       "~a~a"
+       (coq-defns)
+       (if (regexp-match "^\\s*$" output)
+           ""
+           (format "Eval compute in ~a." output))))))
 
 (define-syntax (generate-coq syn)
   (syntax-parse syn
     [(_ (~optional (~seq #:file file))
-        (~optional (~seq #:exists flag)) body:expr)
-     (parameterize ([current-output-port (if (attribute file)
-                                             (open-output-file (syntax->datum #'file)
-                                                               #:exists
-                                                               (if (attribute flag)
-                                                                   ;; TODO: AHH WHAT?
-                                                                   (eval (syntax->datum #'flag))
-                                                                   'error))
-                                             (current-output-port))]
-                    [coq-defns ""])
-       (define output
-         (let ([body (output-coq #'body)])
-           (if (regexp-match "^\\s*$" body)
-               ""
-               (format "Eval compute in ~a." body))))
-       (displayln (format "~a~a" (coq-defns) output))
+        (~optional (~seq #:exists flag))
+        body:expr)
+     (parameterize ([current-output-port
+                     (if (attribute file)
+                         (open-output-file
+                          (syntax->datum #'file)
+                          #:exists
+                          (if (attribute flag)
+                              ;; TODO: AHH WHAT?
+                              (eval (syntax->datum #'flag))
+                              'error))
+                         (current-output-port))])
+       (displayln (cur->coq #'body))
        #'(begin))]))
+
+;; TODO: Should these display or return a string?
+(begin-for-syntax
+  (define (display-mathpartir)
+    (displayln
+     "%% Requires mathpartir, http://pauillac.inria.fr/~remy/latex/mathpartir.html")
+    (displayln
+     "%% or mttex, https://github.com/wilbowma/mttex")
+    (displayln
+     "\\usepackage{mathpartir}"))
+
+  (define (display-bnf)
+    (displayln
+     "%% Some auxillary defs. These should deleted if using mttex, https://github.com/wilbowma/mttex")
+    (displayln
+     "\\newcommand{\\bnfdef}{{\\bf ::=}}")
+    (displayln
+     "\\newcommand{\\bnfalt}{{\\bf \\mid}}")))
+
+;; ------------------------------------
+;; define-relation
+
+(begin-for-syntax
+  (define-syntax-class horizontal-line
+    (pattern
+     x:id
+     #:when (regexp-match? #rx"-+" (symbol->string (syntax-e #'x)))))
+
+  (define-syntax-class hypothesis
+    (pattern (x:id (~datum :) t))
+    (pattern (~not e:horizontal-line)))
+
+  ;; Alias syntax-classes with names for better error messages
+  (define-syntax-class rule-name
+    (pattern x:id))
+
+  (define-syntax-class relation-name
+    (pattern x:id))
+
+  (define-syntax-class relation-index
+    (pattern e:expr))
+
+  (define-syntax-class (conclusion n args lab)
+    (pattern
+     (name:id arg:expr ...)
+     #:attr rule-label-symbol (syntax-e lab)
+     #:attr rule-name-symbol (syntax-e #'name)
+     #:attr relation-name-symbol (syntax-e n)
+     #:fail-unless (eq? (attribute rule-name-symbol) (attribute relation-name-symbol))
+     (format "In rule ~a, name of conclusion ~a did not match name of relation ~a"
+             (attribute rule-label-symbol)
+             (attribute rule-name-symbol)
+             (attribute relation-name-symbol))
+     #:attr rule-arg-count (length (attribute arg))
+     #:attr relation-arg-count (length args)
+     #:fail-unless (= (attribute rule-arg-count) (attribute relation-arg-count))
+     (format "In rule ~a, conclusion applied to ~a arguments, while relation declared to have ~a arguments"
+             (attribute rule-label-symbol)
+             (attribute rule-arg-count)
+             (attribute relation-arg-count))))
+
+  ;; TODO: Automatically infer hypotheses that are merely declarations by binding all free identifiers?
+  ;; TODO: Automatically infer hypotheses as above for meta-variables that are the
+  ;; same as bnf grammar, as a simple first case
+  (define-syntax-class (inferrence-rule name indices)
+    (pattern (h:hypothesis ...
+              #;line:horizontal-line
+              (~optional line:horizontal-line)
+              ~!
+              lab:rule-name
+              (~var t (conclusion name indices (attribute lab))))
+             #:with constr-decl
+             #'(lab : (-> h ... (t.name t.arg ...)))
+             ;; TODO: convert meta-vars such as e1 to e_1
+             #:attr latex
+             (format
+              "\\inferrule~n{~a}~n{~a}"
+              (string-trim
+               (for/fold ([str ""])
+                         ;; TODO: Perhaps omit hypotheses that are merely delcarations of free variables
+                         ([hyp (syntax->datum #'(h ...))])
+                 (format "~a~a \\+" str hyp))
+               " \\+"
+               #:left? #f)
+              (format "~a" (syntax->datum #'(t.name t.arg ...))))))
+
+  ;; TODO: Should this display or return a string?
+  (define (typeset-relation form rules-latex)
+    (display-mathpartir)
+    (printf
+     "\\fbox{$~a$}$~n$\\begin{mathpar}~n~a~n\\end{mathpar}"
+     form
+     (string-trim
+      (for/fold ([str ""])
+                ([rule rules-latex])
+        (format "~a~a\\and~n" str rule))
+      "\\and"
+      #:left? #f))))
+
+(define-syntax (define-relation syn)
+  (syntax-parse syn
+    [(_ (name:relation-name index:relation-index ...)
+        (~optional (~seq #:output-coq coq-file:str))
+        (~optional (~seq #:output-latex latex-file:str))
+        (~var rule (inferrence-rule (attribute name) (attribute index))) ...)
+      (let ([output #`(data name : (-> index ... Type) rule.constr-decl ...)])
+        (when (attribute latex-file)
+          (with-output-to-file (syntax->datum #'latex-file)
+            (thunk
+             (typeset-relation
+              (syntax->datum #'(name index ...))
+              (attribute rule.latex)))
+            #:exists 'append))
+        (when (attribute coq-file)
+          (with-output-to-file (syntax->datum #'coq-file)
+            (thunk (displayln (cur->coq output)))
+            #:exists 'append))
+        output)]))
+
+;; ------------------------------------
+;; define-language
+
+(begin-for-syntax
+  ;; A mutable dictionary from non-terminal meta-variables names to their types.
+  (define mv-map (make-parameter #f))
+
+  ;; A set containing the meta-variables that represent variables.
+  (define vars (make-parameter #f))
+
+  ;; The language name for the language currently being parsed
+  (define lang-name (make-parameter #f))
+
+  ;; A meta-variable is any identifiers that belongs to the mv-map
+  (define-syntax-class meta-variable
+    (pattern
+     x:id
+     #:attr sym (syntax->datum #'x)
+     #:fail-unless (dict-has-key? (mv-map) (attribute sym)) #f
+     #:attr type (dict-ref (mv-map) (attribute sym))))
+
+  ;; A var-meta-variable is a meta-variable that is declared to be
+  ;; treated as a variable in the defined language.
+  (define-syntax-class var-meta-variable
+    (pattern
+     x:id
+     #:fail-unless (set-member? (vars) (syntax->datum #'x)) #f))
+
+  ;; A terminal is a idnetifiers that is not a meta-variable. A terminal will always represent a constructor.
+  (define-syntax-class terminal
+    (pattern
+     x:id
+     #:attr sym (syntax->datum #'x)
+     #:fail-when (dict-has-key? (mv-map) (attribute sym)) #f
+     #:attr constructor-name
+     (format-id #'x "~a-~a" (lang-name) #'x)))
+
+  ;; A terminal-args can appear as the argument to a terminal in
+  ;; an expression, or as a sub-expression in a terminal-args.
+  ;; Each terminal-args export args, a list of types the
+  ;; terminal-args represents and the list of types the non-terminal's
+  ;; constructor expects in this case.
+  (define-syntax-class (terminal-args non-terminal-type)
+    ;; A meta-variable is a terminal-args
+    (pattern
+     e:meta-variable
+     #:attr args
+     (list #'e.type)
+     #:attr latex
+     (format "~a" (syntax-e #'e)))
+
+    ;; An identifier is a terminal-args, but is treated as syntax
+    (pattern
+     x:id
+     #:attr args
+     '()
+     #:attr latex
+     (format "~a" (syntax-e #'x)))
+
+    ;; So is an empty list
+    (pattern
+     ()
+     #:attr args
+     '()
+     #:attr latex
+     "")
+
+    ;; We use De-Bruijn indices, so binding positions are removed.
+    (pattern
+     (#:bind x:var-meta-variable . (~var t (terminal-args non-terminal-type)))
+     #:attr args
+     (attribute t.args)
+     #:attr latex
+     (format "~a ~a" (syntax-e #'x) (attribute t.latex)))
+
+    ;; A terminal-args applied to other nested expressions is a terminal-args
+    (pattern
+     ((~var h (terminal-args non-terminal-type))
+      (~var t (terminal-args non-terminal-type)) ...)
+     #:attr args
+     (for/fold ([ls (attribute h.args)])
+               ([args (attribute t.args)])
+       (append ls args))
+     #:attr latex
+     (format "~a ~a" (attribute h.latex) (apply string-append (attribute t.latex)))))
+
+  ;; a expression is parameterized by the name of the non-terminal to
+  ;; which is belongs,
+  ;; Each expression exports a constr-decl, which declares a
+  ;; constructor for the non-terminal type.
+  (define-syntax-class (expression non-terminal-type)
+    ;; A meta-variable is a valid expression.
+    ;; Generates a conversion constructor in constr-decl, and the type of
+    (pattern
+     e:meta-variable
+     #:attr constructor-name
+     (format-id #'e "~a->~a" #'e.type non-terminal-type)
+     #:attr constr-decl
+     #`(constructor-name : (-> e.type #,non-terminal-type))
+     #:attr latex
+     (format "~a" (syntax-e #'e)))
+
+    ;; An identifier is a valid expression, generating a base constructor.
+    (pattern
+     x:terminal
+     #:attr constr-decl
+     #`(x.constructor-name : #,non-terminal-type)
+     #:attr latex
+     (format "~a" (syntax-e #'x)))
+
+    ;; A terminal applied to a terminal-args is a valid expression.
+    (pattern
+     (x:terminal . (~var c (terminal-args non-terminal-type)))
+     #:attr constr-decl
+     #`(x.constructor-name : (-> #,@(attribute c.args) #,non-terminal-type))
+     #:attr latex
+     (format "(~a ~a)" (syntax-e #'x) (attribute c.latex))))
+
+  (define-syntax-class non-terminal-def
+    (pattern
+     (name:id
+      (meta-var:id ...+)
+      (~optional (~datum ::=))
+      ;; Create a name for the type of this non-terminal, from the
+      ;; language name and the non-terminal name.
+      (~bind [nt-type (format-id #'name "~a-~a" (lang-name) #'name)])
+      ;; Imperatively update the map from meta-variables to the
+      ;; nt-type, to be used when generating the types of the constructors
+      ;; for this and later non-terminal.
+      (~do (for ([mv (syntax->datum #'(meta-var ...))])
+             (dict-set! (mv-map) mv (attribute nt-type))))
+      (~var c (expression (attribute nt-type))) ...)
+     ;; Generates the inductive data type for this non-terminal definition.
+     #:attr def
+     #`(data nt-type : Type c.constr-decl ...)
+     #:attr latex
+     (format
+      "\\mbox{\\textit{~a}} & ~a & \\bnfdef & ~a\\\\~n"
+      (symbol->string (syntax->datum #'name))
+      (string-trim
+       (for/fold ([str ""])
+                 ([nt (syntax->datum #'(meta-var ...))])
+         (format "~a~a," str nt))
+       ","
+       #:left? #f)
+      (string-trim
+       (for/fold ([str ""])
+                 ([expr (attribute c.latex)])
+         (format "~a~a \\bnfalt " str expr))
+       " \\bnfalt "
+       #:left? #f))))
+
+  ;; TODO: Should this display or return a string?
+  (define (typeset-bnf nt-latex)
+    (display-mathpartir)
+    (display-bnf)
+    (printf
+     "\begin{displaymath}~n\\begin{array}{lrrl}~n~a~n\\end{array}~n\end{displaymath}"
+     (apply string-append nt-latex))))
+
+;; TODO: For better error messages, add context
+;; TODO: Extend define-language with syntax such as ....
+;;   (term (e) ::= (e1 e2) ((lambda (x) e)
+(define-syntax (define-language syn)
+  (define/syntax-parse
+    (_ name:id
+       (~optional (~seq #:vars (x:id ...)))
+       (~optional (~seq #:output-coq coq-file:str))
+       (~optional (~seq #:output-latex latex-file:str))
+       .
+       non-terminal-defs)
+    syn)
+  (parameterize ([mv-map (make-hash)]
+                 [lang-name #'name]
+                 [vars (apply set (map syntax->datum (or (attribute x) '())))])
+    (cond
+      [(attribute x) =>
+       (lambda (xls)
+         (for ([x xls])
+           (dict-set! (mv-map) (syntax-e x) #'Nat)))])
+    (syntax-parse #'non-terminal-defs
+      [(def:non-terminal-def ...)
+       (let ([output #`(begin def.def ...)])
+         (when (attribute latex-file)
+           (with-output-to-file (syntax-e #'latex-file)
+             (thunk (typeset-bnf (attribute def.latex)))
+             #:exists 'append))
+         (when (attribute coq-file)
+           (with-output-to-file (syntax-e #'coq-file)
+             (thunk (displayln (cur->coq output)))
+             #:exists 'append))
+         output)])))
+
+;; See stlc.rkt for examples
diff --git a/cur-test/cur/tests/olly.rkt b/cur-test/cur/tests/olly.rkt
index 1812caa..a2cda7b 100644
--- a/cur-test/cur/tests/olly.rkt
+++ b/cur-test/cur/tests/olly.rkt
@@ -9,77 +9,49 @@
  cur/olly)
 
 (begin-for-syntax
-  (require rackunit)
-  (define (check-id-equal? v1 v2)
-    (check-equal?
-     (syntax->datum v1)
-     (syntax->datum v2)))
-  (define (check-id-match? v1 v2)
-    (check-regexp-match
-     v1
-     (symbol->string (syntax->datum v2))))
-  (check-id-match?
-   #px"term\\d+"
-   (fresh-name #'term))
-  (check-id-equal?
-   #'stlc-lambda
-   (new-name #'stlc #'lambda))
-  (check-id-match?
-   #px"stlc-term\\d+"
-   (new-name #'stlc (fresh-name #'term))))
+  (require rackunit))
 
-(begin-for-syntax
+;; Can't test this way anymore.
+#;(begin-for-syntax
   (check-equal?
    (format "$$\\begin{array}{lrrl}~n~a~n\\end{array}$$"
            (format "\\mbox{\\textit{term}} & e & \\bnfdef & (e1 e2) \\bnfalt (lambda (x) e)\\\\~n"))
-   (output-latex-bnf #'(x)
-                     #'((term (e) ::= (e1 e2) (lambda (x) e)))))
+   (typeset-bnf #'((term (e) ::= (e1 e2) (lambda (x) e)))))
   (check-equal?
    (format "$$\\begin{array}{lrrl}~n~a~n\\end{array}$$"
            (format "\\mbox{\\textit{type}} & A,B,C & \\bnfdef & unit \\bnfalt (* A B) \\bnfalt (+ A C)\\\\~n"))
-   (output-latex-bnf #'(x)
-                     #'((type (A B C) ::= unit (* A B) (+ A C))))))
-
-(check-equal?
- (var-equal? (avar z) (avar z))
- true)
-(check-equal?
- (var-equal? (avar z) (avar (s z)))
- false)
+   (typeset-bnf #'((type (A B C) ::= unit (* A B) (+ A C))))))
 
 (begin-for-syntax
   (check-equal?
-   (parameterize ([coq-defns ""]) (output-coq #'(data nat : Type (z : nat))) (coq-defns))
-   (format "Inductive nat : Type :=~n| z : nat.~n"))
+   (format "Inductive nat : Type :=~n| z : nat.~n")
+   (cur->coq #'(data nat : Type (z : nat))))
   (check-regexp-match
    "(forall .+ : Type, Type)"
-   (output-coq #'(-> Type Type)))
-  (let ([t (parameterize ([coq-defns ""])
-             (output-coq #'(define-relation (meow gamma term type)
-                             [(g : gamma) (e : term) (t : type)
-                              --------------- T-Bla
-                              (meow g e t)]))
-             (coq-defns))])
+   (cur->coq #'(-> Type Type)))
+  (let ([t (cur->coq
+            #'(define-relation (meow gamma term type)
+                [(g : gamma) (e : term) (t : type)
+                 --------------- T-Bla
+                 (meow g e t)]))])
     (check-regexp-match
      "Inductive meow : \\(forall .+ : gamma, \\(forall .+ : term, \\(forall .+ : type, Type\\)\\)\\) :="
      (first (string-split t "\n")))
     (check-regexp-match
      "\\| T-Bla : \\(forall g : gamma, \\(forall e : term, \\(forall t : type, \\(\\(\\(meow g\\) e\\) t\\)\\)\\)\\)\\."
      (second (string-split t "\n"))))
-  (let ([t (output-coq #'(elim nat Type (lambda (x : nat) nat) z
-                               (lambda (x : nat) (ih-x : nat) ih-x)
-                               e))])
+  (let ([t (cur->coq
+            #'(elim nat Type (lambda (x : nat) nat) z
+                    (lambda (x : nat) (ih-x : nat) ih-x)
+                    e))])
     (check-regexp-match
      "\\(\\(\\(\\(nat_rect \\(fun x : nat => nat\\)\\) z\\) \\(fun x : nat => \\(fun ih_x : nat => ih_x\\)\\)\\) e\\)"
      t))
   (check-regexp-match
    "Definition thm_plus_commutes := \\(forall n : nat, \\(forall m : nat, \\(\\(\\(== nat\\) \\(\\(plus n\\) m\\)\\) \\(\\(plus m\\) n\\)\\)\\)\\).\n"
-   (parameterize ([coq-defns ""])
-     (output-coq #'(define thm:plus-commutes (forall (n : nat) (m : nat)
-                                                      (== nat (plus n m) (plus m n)))))
-     (coq-defns)))
+   (cur->coq
+    #'(define thm:plus-commutes (forall (n : nat) (m : nat)
+                                        (== nat (plus n m) (plus m n))))))
   (check-regexp-match
    "Function add1 \\(n : nat\\)  := \\(s n\\).\n"
-   (parameterize ([coq-defns ""])
-     (output-coq #'(define (add1 (n : nat)) (s n)))
-     (coq-defns))))
+   (cur->coq #'(define (add1 (n : nat)) (s n)))))
diff --git a/cur-test/cur/tests/stlc.rkt b/cur-test/cur/tests/stlc.rkt
index 915b5cf..d38d930 100644
--- a/cur-test/cur/tests/stlc.rkt
+++ b/cur-test/cur/tests/stlc.rkt
@@ -2,6 +2,7 @@
 (require
  rackunit
  cur/stdlib/nat
+ cur/stdlib/list
  cur/stdlib/sugar
  cur/olly
  cur/stdlib/maybe
@@ -15,64 +16,55 @@
   (val  (v)   ::= true false unit)
   ;; TODO: Allow datum, like 1, as terminals
   (type (A B) ::= boolty unitty (-> A B) (* A A))
-  (term (e)   ::= x v (app e e) (lambda (x : A) e) (cons e e)
-                  (let (x x) = e in e)))
+  (term (e)   ::= x v (app e e) (lambda (#:bind x : A) e) (cons e e)
+                  (let (#:bind x #:bind x) = e in e)))
 
-;; TODO: Abstract this over stlc-type, and provide from in OLL
-(data Gamma : Type
-  (emp-gamma : Gamma)
-  (extend-gamma : (-> Gamma Var stlc-type Gamma)))
+(define lookup-env (list-ref stlc-type))
 
-(define (lookup-gamma (g : Gamma) (x : Var))
-  (match g
-    [emp-gamma (none stlc-type)]
-    [(extend-gamma (g1 : Gamma) (v1 : Var) (t1 : stlc-type))
-     (if (var-equal? v1 x)
-         (some stlc-type t1)
-         (recur g1))]))
+(define (extend-env (g : (List stlc-type)) (t : stlc-type))
+  (cons stlc-type t g))
 
-(define-relation (has-type Gamma stlc-term stlc-type)
+(define-relation (has-type (List stlc-type) stlc-term stlc-type)
   #:output-coq "stlc.v"
   #:output-latex "stlc.tex"
-  [(g : Gamma)
+  [(g : (List stlc-type))
    ------------------------ T-Unit
-   (has-type g (stlc-val-->-stlc-term stlc-unit) stlc-unitty)]
+   (has-type g (stlc-val->stlc-term stlc-unit) stlc-unitty)]
 
-  [(g : Gamma)
+  [(g : (List stlc-type))
    ------------------------ T-True
-   (has-type g (stlc-val-->-stlc-term stlc-true) stlc-boolty)]
+   (has-type g (stlc-val->stlc-term stlc-true) stlc-boolty)]
 
-  [(g : Gamma)
+  [(g : (List stlc-type))
    ------------------------ T-False
-   (has-type g (stlc-val-->-stlc-term stlc-false) stlc-boolty)]
+   (has-type g (stlc-val->stlc-term stlc-false) stlc-boolty)]
 
-  [(g : Gamma) (x : Var) (t : stlc-type)
-   (== (Maybe stlc-type) (lookup-gamma g x) (some stlc-type t))
+  [(g : (List stlc-type)) (x : Nat) (t : stlc-type)
+   (== (Maybe stlc-type) (lookup-env g x) (some stlc-type t))
    ------------------------ T-Var
-   (has-type g (Var-->-stlc-term x) t)]
+   (has-type g (Nat->stlc-term x) t)]
 
-  [(g : Gamma) (e1 : stlc-term) (e2 : stlc-term)
+  [(g : (List stlc-type)) (e1 : stlc-term) (e2 : stlc-term)
                (t1 : stlc-type) (t2 : stlc-type)
    (has-type g e1 t1)
    (has-type g e2 t2)
    ---------------------- T-Pair
    (has-type g (stlc-cons e1 e2) (stlc-* t1 t2))]
 
-  [(g : Gamma) (e1 : stlc-term) (e2 : stlc-term)
+  [(g : (List stlc-type)) (e1 : stlc-term) (e2 : stlc-term)
                (t1 : stlc-type) (t2 : stlc-type)
                (t : stlc-type)
-               (x : Var) (y : Var)
    (has-type g e1 (stlc-* t1 t2))
-   (has-type (extend-gamma (extend-gamma g x t1) y t2) e2 t)
+   (has-type (extend-env (extend-env g t1) t2) e2 t)
    ---------------------- T-Let
-   (has-type g (stlc-let x y e1 e2) t)]
+   (has-type g (stlc-let e1 e2) t)]
 
-  [(g : Gamma) (e1 : stlc-term) (t1 : stlc-type) (t2 : stlc-type) (x : Var)
-   (has-type (extend-gamma g x t1) e1 t2)
+  [(g : (List stlc-type)) (e1 : stlc-term) (t1 : stlc-type) (t2 : stlc-type)
+   (has-type (extend-env g t1) e1 t2)
    ---------------------- T-Fun
-   (has-type g (stlc-lambda x t1 e1) (stlc--> t1 t2))]
+   (has-type g (stlc-lambda t1 e1) (stlc--> t1 t2))]
 
-  [(g : Gamma) (e1 : stlc-term) (e2 : stlc-term)
+  [(g : (List stlc-type)) (e1 : stlc-term) (e2 : stlc-term)
                (t1 : stlc-type) (t2 : stlc-type)
    (has-type g e1 (stlc--> t1 t2))
    (has-type g e2 t1)
@@ -84,59 +76,57 @@
 ;; TODO: When generating a parser, will need something like (#:name app (e e))
 ;; so I can name a constructor without screwing with syntax.
 (begin-for-syntax
-  (define index #'z))
+  (define (dict-shift d)
+    (for/fold ([d (make-immutable-hash)])
+              ([(k v) (in-dict d)])
+      (dict-set d k #`(s #,v)))))
 (define-syntax (begin-stlc syn)
-  (set! index #'z)
-  (let stlc ([syn (syntax-case syn () [(_ e) #'e])])
+  (let stlc ([syn (syntax-case syn () [(_ e) #'e])]
+             [d (make-immutable-hash)])
     (syntax-parse syn
       #:datum-literals (lambda : prj * -> quote let in cons bool)
       [(lambda (x : t) e)
-       (let ([oldindex index])
-         (set! index #`(s #,index))
-         ;; Replace x with a de bruijn index, by running a CIC term at
-         ;; compile time.
-         (normalize/syn
-           #`((lambda (x : stlc-term)
-                      (stlc-lambda (avar #,oldindex) #,(stlc #'t) #,(stlc #'e)))
-             (Var-->-stlc-term (avar #,oldindex)))))]
+       #`(stlc-lambda #,(stlc #'t d) #,(stlc #'e (dict-set (dict-shift d) (syntax->datum #'x) #`z)))]
       [(quote (e1 e2))
-       #`(stlc-cons #,(stlc #'e1) #,(stlc #'e2))]
+       #`(stlc-cons #,(stlc #'e1 d) #,(stlc #'e2 d))]
       [(let (x y) = e1 in e2)
-       (let* ([y index]
-              [x #`(s #,y)])
-         (set! index #`(s (s #,index)))
-         #`((lambda (x : stlc-term) (y : stlc-term)
-              (stlc-let (avar #,x) (avar #,y) #,(stlc #'t) #,(stlc #'e1)
-                   #,(stlc #'e2)))
-            (Var-->-stlc-term (avar #,x))
-            (Var-->-stlc-term (avar #,y))))
-       #`(let x  i #,(stlc #'e1))]
+       #`(stlc-let #,(stlc #'t d) #,(stlc #'e1 d)
+                   #,(stlc #'e2 (dict-set* (dict-shift (dict-shift d))
+                                           (syntax->datum #'x) #`z
+                                           (syntax->datum #'y) #`(s z))))]
       [(e1 e2)
-       #`(stlc-app #,(stlc #'e1) #,(stlc #'e2))]
-      [() #'(stlc-val-->-stlc-term stlc-unit)]
-      [#t #'(stlc-val-->-stlc-term stlc-true)]
-      [#f #'(stlc-val-->-stlc-term stlc-false)]
+       #`(stlc-app #,(stlc #'e1 d) #,(stlc #'e2 d))]
+      [() #'(stlc-val->stlc-term stlc-unit)]
+      [#t #'(stlc-val->stlc-term stlc-true)]
+      [#f #'(stlc-val->stlc-term stlc-false)]
       [(t1 * t2)
-       #`(stlc-* #,(stlc #'t1) #,(stlc #'t2))]
+       #`(stlc-* #,(stlc #'t1 d) #,(stlc #'t2 d))]
       [(t1 -> t2)
-       #`(stlc--> #,(stlc #'t1) #,(stlc #'t2))]
+       #`(stlc--> #,(stlc #'t1 d) #,(stlc #'t2 d))]
       [bool #`stlc-boolty]
       [e
-       (if (eq? 1 (syntax->datum #'e))
-           #'stlc-unitty
-           #'e)])))
+       (cond
+         [(eq? 1 (syntax->datum #'e))
+          #'stlc-unitty]
+         [(dict-ref d (syntax->datum #'e) #f) =>
+          (lambda (x)
+            #`(Nat->stlc-term #,x))]
+         [else #'e])])))
 
 (check-equal?
  (begin-stlc (lambda (x : 1) x))
- (stlc-lambda (avar z) stlc-unitty (Var-->-stlc-term (avar z))))
+ (stlc-lambda stlc-unitty (Nat->stlc-term z)))
 (check-equal?
  (begin-stlc ((lambda (x : 1) x) ()))
- (stlc-app (stlc-lambda (avar z) stlc-unitty (Var-->-stlc-term (avar z)))
-           (stlc-val-->-stlc-term stlc-unit)))
+ (stlc-app (stlc-lambda stlc-unitty (Nat->stlc-term z))
+           (stlc-val->stlc-term stlc-unit)))
+(check-equal?
+ (begin-stlc (lambda (x : 1) (lambda (y : 1) x)))
+ (stlc-lambda stlc-unitty (stlc-lambda stlc-unitty (Nat->stlc-term (s z)))))
 (check-equal?
  (begin-stlc '(() ()))
- (stlc-cons (stlc-val-->-stlc-term stlc-unit)
-            (stlc-val-->-stlc-term stlc-unit)))
+ (stlc-cons (stlc-val->stlc-term stlc-unit)
+            (stlc-val->stlc-term stlc-unit)))
 (check-equal?
  (begin-stlc #t)
- (stlc-val-->-stlc-term stlc-true))
+ (stlc-val->stlc-term stlc-true))