NB, API changes: Faster/more primitive elim

This commit breaks previous API for eliminating inductive types.

The previous eliminator for inductive types was too complex. It performed
automagic currying, making it difficult to type check, and difficult and
expensive to reduce.

The new version must be fully applied, and magic should be implemented
in the surface language. A sketch of such magic is left in sugar.rkt,
but not yet implemented.

This new version gives a 40% speed up on the Cur test
suite. Unfortunately, Redex is still the major bottleneck, so no
algorithmic gains.

README.md

@@ -15,26 +15,40 @@ cur (plural curs)
 Disclaimer
 ==========
 Cur is currently under active hackery and is not fit for use for any
-particular purpose. It is fraught with unreadable code, errors, and
-hacks that should never have been written by a reasonable human being.
+particular purpose. It is fraught with unreadable code, errors,
+performance bugs, and hacks that should never have been written by a
+reasonable human being.
 These may or may not be fixed shortly.
 
 Getting started
 ===============
 
+Easy mode:
 Install cur via `raco pkg install cur`.
 
+Advanced mode:
+Cur is actually distributed as several packages.
+`cur-lib` provides the implementation and all standard
+libraries.
+`cur-doc` provides the documentation.
+`cur-test` provides a test suite and examples.
+
+
 Try it out: open up DrRacket and put the following in the definition area:
 
 ```racket
 #lang cur
-(require 
+(require
  cur/stdlib/bool
  cur/stdlib/nat)
 
 (if true
     false
     true)
+
+(: + (-> Nat Nat Nat))
+(define + plus)
+(+ z (s z))
 ```
 
 Try entering the following in the interaction area:
@@ -42,29 +56,39 @@ Try entering the following in the interaction area:
 (sub1 (s (s z)))
 ```
 
-See the docs: `raco docs cur`.
+Don't like parenthesis? Use Cur with sweet-expressions:
+```racket
+#lang sweet-exp cur
+require
+ cur/stdlib/sugar
+ cur/stdlib/bool
+ cur/stdlib/nat
 
-Most of the standard library is currently undocumented, so just see the source.
+if true
+   false
+   true
+
+define + plus
+
+{z + s(z)}
+```
+
+See the docs: `raco docs cur`.
 
 Going further
 =============
 
-Open up `examples/example.rkt` to see a tour of Cur's features.
-
-Open up `examples/stlc.rkt` to see an example of what advanced meta-programming can let you do.
-
-Open up `oll.rkt` to see the implementation of the meta-programs used to
-enable `examples/stlc.rkt`, including the parsers for BNF syntax and inference rule
-syntax, and Coq and LaTeX generators.
+Open up `cur-tests/cur/tests/stlc.rkt` to see an example of the
+simply-typed lambda-calculus modeled in Cur, with a parser and syntax
+extension to enable deeply embedding.
 
 Open up `examples/proofs-for-free.rkt` to see an implementation of the
 translation defined in [Proofs for Free](http://staff.city.ac.uk/~ross/papers/proofs.html) as a meta-program.
 
-Open up `stdlib/tactics` to see tactics, implemented entirely via
-meta-programming.
+Open up `cur-lib/cur/stdlib/tactics` to see one way to implement tactics in Cur.
 
-Open up anything in `stdlib/` to see some standard dependent-type
+Open up anything in `cur-lib/cur/stdlib/` to see some standard dependent-type
 formalisms.
 
-Open up `curnel/redex-core.rkt` to see the entire "trusted" (after a
-large test suite) core.
+Open up `cur-lib/cur/curnel/redex-core.rkt` to see the entire
+implementation of the core language, <600 lines of code.

cur-doc/cur/cur.scrbl

@@ -1,6 +1,6 @@
 #lang scribble/manual
 @(require
-   "defs.rkt"
+   "scribblings/defs.rkt"
    racket/function)
 
 @title[#:style '(toc)]{Cur}
@@ -42,7 +42,7 @@ Everything else in @racketmodname[cur] is provided by untrusted user-land code--
 
 @local-table-of-contents[]
 
-@include-section{curnel.scrbl}
-@include-section{reflection.scrbl}
-@include-section{stdlib.scrbl}
-@include-section{oll.scrbl}
+@include-section{scribblings/curnel.scrbl}
+@include-section{scribblings/reflection.scrbl}
+@include-section{scribblings/stdlib.scrbl}
+@include-section{scribblings/olly.scrbl}

cur-doc/cur/info.rkt

@@ -0,0 +1,2 @@
+#lang info
+(define scribblings '(("cur.scrbl" (multi-page))))

cur-doc/cur/scribblings/curnel.scrbl

@@ -0,0 +1,135 @@
+#lang scribble/manual
+
+@(require
+  "defs.rkt"
+  scribble/eval)
+
+@title{Curnel Forms}
+@deftech{Curnel forms} are the core forms provided @racketmodname[cur].
+These forms come directly from the trusted core and are all that remain after macro expansion.
+@todo{Link to guide regarding macro expansion}
+The core of @racketmodname[cur] is essentially TT with an impredicative universe @racket[(Type 0)].
+For a very understandable in-depth look at TT, see chapter 2 of
+@hyperlink["https://eb.host.cs.st-andrews.ac.uk/writings/thesis.pdf"
+           "Practical Implementation of a Dependently Typed Functional Programming Language"], by
+Edwin C. Brady.
+
+@(define curnel-eval (curnel-sandbox "(require cur/stdlib/nat cur/stdlib/bool cur/stdlib/prop)"))
+
+@defform*[((Type n)
+           Type)]{
+Define the universe of types at level @racket[n], where @racket[n] is any natural number.
+@racket[Type] is a synonym for @racket[(Type 0)]. Cur is impredicative
+in @racket[(Type 0)], although this is likely to change to a more
+restricted impredicative universe.
+
+@examples[#:eval curnel-eval
+          (Type 0)]
+
+@examples[#:eval curnel-eval
+          (Type 1)]
+
+@examples[#:eval curnel-eval
+          Type]
+}
+
+@defform[(λ (id : type-expr) body-expr)]{
+Produces a single-arity procedure, binding the identifier @racket[id] of type
+@racket[type-expr] in @racket[body-expr] and in the type of @racket[body-expr].
+Both @racket[type-expr] and @racket[body-expr] can contain non-curnel forms,
+such as macros.
+
+Currently, Cur will return the underlying representation of a procedure when a
+@racket[λ] is evaluated at the top-level.
+Do not rely on this representation.
+
+@examples[#:eval curnel-eval
+          (λ (x : Type) x)]
+
+@examples[#:eval curnel-eval
+          (λ (x : Type) (λ (y : x) y))]
+
+
+@defform[(#%app procedure argument)]{
+Applies the single-arity @racket[procedure] to @racket[argument].
+}
+
+@examples[#:eval curnel-eval
+          ((λ (x : (Type 1)) x) Type)]
+
+@examples[#:eval curnel-eval
+          (#%app (λ (x : (Type 1)) x) Type)]
+}
+
+@defform[(Π (id : type-expr) body-expr)]{
+Produces a dependent function type, binding the identifier @racket[id] of type
+@racket[type-expr] in @racket[body-expr].
+
+
+@examples[#:eval curnel-eval
+          (Π (x : Type) Type)]
+
+@examples[#:eval curnel-eval
+          (λ (x : (Π (x : (Type 1)) Type))
+            (x Type))]
+}
+
+@defform[(data id : type-expr (id* : type-expr*) ...)]{
+Defines an inductive datatype named @racket[id] of type @racket[type-expr], with constructors
+@racket[id*] each with the corresponding type @racket[type-expr*].
+Currently, Cur does not attempt to ensure the well-foundedness of the inductive definition.
+For instance, Cur does not currently perform strict positivity checking.
+
+@examples[#:eval curnel-eval
+          (data Bool : Type
+                (true : Bool)
+                (false : Bool))
+          ((λ (x : Bool) x) true)
+          (data False : Type)
+          (data And : (Π (A : Type) (Π (B : Type) Type))
+            (conj : (Π (A : Type) (Π (B : Type) (Π (a : A) (Π (b : B) ((And A) B)))))))
+          ((((conj Bool) Bool) true) false)]
+}
+
+@defform[(elim inductive-type motive (index ...) (method ...) disc)]{
+Fold over the term @racket[disc] of the inductively defined type @racket[inductive-type].
+The @racket[motive] is a function that expects the indices of the inductive
+type and a term of the inductive type and produces the type that this
+fold returns.
+The type of @racket[disc] is @racket[(inductive-type index ...)].
+@racket[elim] takes one method for each constructor of @racket[inductive-type].
+Each @racket[method] expects the arguments for its corresponding constructor,
+and the inductive hypotheses generated by recursively eliminating all recursive
+arguments of the constructor.
+
+The following example runs @racket[(sub1 (s z))].
+
+@examples[#:eval curnel-eval
+          (data Nat : Type
+            (z : Nat)
+            (s : (Π (n : Nat) Nat)))
+          (elim Nat (λ (x : Nat) Nat)
+                ()
+                (z
+                 (λ (n : Nat) (λ (IH : Nat) n)))
+                (s z))]
+}
+
+@defform[(define id expr)]{
+Binds @racket[id] to the result of @racket[expr].
+
+@examples[#:eval curnel-eval
+          (data Nat : Type
+            (z : Nat)
+            (s : (Π (n : Nat) Nat)))
+          (define sub1 (λ (n : Nat)
+                         (elim Nat (λ (x : Nat) Nat)
+                               ()
+                               (z
+                                (λ (n : Nat) (λ (IH : Nat) n)))
+                               n)))
+          (sub1 (s (s z)))
+          (sub1 (s z))
+          (sub1 z)]
+}
+@todo{Document @racket[require] and @racket[provide]}

cur-doc/cur/scribblings/defs.rkt

@@ -0,0 +1,22 @@
+#lang racket/base
+
+(require
+ scribble/base
+ scribble/manual
+ racket/sandbox)
+(provide (all-defined-out))
+
+(define (todo . ls)
+  (apply margin-note* "TODO: " ls))
+
+(define (gtech . x)
+  (apply tech x #:doc '(lib "scribblings/guide/guide.scrbl")))
+
+(define (curnel-sandbox init-string)
+  (parameterize ([sandbox-output 'string]
+                 [sandbox-error-output 'string]
+                 ;; TODO: Probs a bad idea
+                 [sandbox-eval-limits #f]
+                 [sandbox-memory-limit #f])
+    (make-module-evaluator
+     (format "#lang cur~n~a" init-string))))

cur-doc/cur/scribblings/olly.scrbl

@@ -1,12 +1,12 @@
 #lang scribble/manual
 @(require "defs.rkt")
 
-@title{OLL: Ott-like Library}
+@title{Olly: Ott-like LibrarY}
 
-@defmodule[cur/oll]
-The OLL provides syntax extensions for defining programming languages as inductive data. The library
+@defmodule[cur/olly]
+Olly provides syntax extensions for defining programming languages as inductive data. The library
 is inspired by Ott@todo{Citation needed}, which provides an language that resembles math notation for
-generating Coq definitions.  The purpose of the OLL is not to replace Ott, but to demonstrate how
+generating Coq definitions.  The purpose of Olly is not to replace Ott, but to demonstrate how
 powerful syntactic meta-programming can bring features previously only provided by external tools into
 the language.
 
@@ -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 OLL 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.}
 

cur-doc/cur/scribblings/reflection.scrbl

@@ -2,6 +2,7 @@
 
 @(require
    "defs.rkt"
+   scribble/eval
    (for-label (only-in racket local-expand)))
 
 @title{Reflection}
@@ -10,13 +11,7 @@ various parts of the language implementation as Racket forms at @gtech{phase} 1.
 The reflection features are @emph{unstable} and may change without warning.
 Many of these features are extremely hacky.
 
-@(require racket/sandbox scribble/eval)
-@(define curnel-eval
-   (parameterize ([sandbox-output 'string]
-                  [sandbox-error-output 'string]
-                  [sandbox-eval-limits #f]
-                  [sandbox-memory-limit #f])
-     (make-module-evaluator "#lang cur (require cur/stdlib/bool) (require cur/stdlib/nat)")))
+@(define curnel-eval (curnel-sandbox "(require cur/stdlib/bool cur/stdlib/nat)"))
 
 @defproc[(cur-expand [syn syntax?] [id identifier?] ...)
          syntax?]{
@@ -30,61 +25,61 @@ phase 1 in Cur.}
 
 @examples[
 (eval:alts (define-syntax-rule (computed-type _) Type) (void))
-(eval:alts (cur-expand #'(lambda (x : (computed-type bla)) x))
-           (eval:result @racket[#'(lambda (x : Type) x)] "" ""))
+(eval:alts (cur-expand #'(λ (x : (computed-type bla)) x))
+           (eval:result @racket[#'(λ (x : Type) x)] "" ""))
 ]
 }
 
-@defproc[(type-infer/syn [syn syntax?])
+@defproc[(cur-type-infer [syn syntax?])
          (or/c syntax? #f)]{
 Returns the type of the Cur term @racket[syn], or @racket[#f] if no type could be inferred.
 
 @examples[
-(eval:alts (type-infer/syn #'(lambda (x : Type) x))
-           (eval:result @racket[#'(forall (x : (Type 0)) (Type 0))] "" ""))
-(eval:alts (type-infer/syn #'Type)
+(eval:alts (cur-type-infer #'(λ (x : Type) x))
+           (eval:result @racket[#'(Π (x : (Type 0)) (Type 0))] "" ""))
+(eval:alts (cur-type-infer #'Type)
            (eval:result @racket[#'(Type 1)] "" ""))
 ]
 }
 
-@defproc[(type-check/syn? [syn syntax?])
+@defproc[(cur-type-check? [syn syntax?])
          boolean?]{
 Returns @racket[#t] if the Cur term @racket[syn] is well-typed, or @racket[#f] otherwise.
 
 @examples[
-(eval:alts (type-check/syn? #'(lambda (x : Type) x))
+(eval:alts (cur-type-check? #'(λ (x : Type) x))
            (eval:result @racket[#t] "" ""))
-(eval:alts (type-check/syn? #'Type)
+(eval:alts (cur-type-check? #'Type)
            (eval:result @racket[#t] "" ""))
-(eval:alts (type-check/syn? #'x)
+(eval:alts (cur-type-check? #'x)
            (eval:result @racket[#f] "" ""))
 ]
 }
 
-@defproc[(normalize/syn [syn syntax?])
+@defproc[(cur-normalize [syn syntax?])
          syntax?]{
 Runs the Cur term @racket[syn] to a value.
 
 @examples[
-(eval:alts (normalize/syn #'((lambda (x : Type) x) Bool))
+(eval:alts (cur-normalize #'((λ (x : Type) x) Bool))
            (eval:result @racket[#'Bool] "" ""))
-(eval:alts (normalize/syn #'(sub1 (s (s z))))
+(eval:alts (cur-normalize #'(sub1 (s (s z))))
            (eval:result @racket[#'(s z)] "" ""))
 ]
 }
 
-@defproc[(step/syn [syn syntax?])
+@defproc[(cur-step [syn syntax?])
          syntax?]{
 Runs the Cur term @racket[syn] for one step.
 
 @examples[
-(eval:alts (step/syn #'((lambda (x : Type) x) Bool))
+(eval:alts (cur-step #'((λ (x : Type) x) Bool))
            (eval:result @racket[#'Bool] "" ""))
-(eval:alts (step/syn #'(sub1 (s (s z))))
-           (eval:result @racket[#'(((((elim Nat (Type 0))
-                                      (lambda (x2 : Nat) Nat)) z)
-                                    (lambda (x2 : Nat) (lambda (ih-n2 : Nat) x2)))
-                                   (s (s z)))] "" ""))
+(eval:alts (cur-step #'(sub1 (s (s z))))
+           (eval:result @racket[#'(elim Nat (λ (x2 : Nat) Nat)
+                                        ()
+                                        (z (λ (x2 : Nat) (λ (ih-n2 : Nat) x2)))
+                                        (s (s z)))] "" ""))
 ]
 }
 
@@ -95,11 +90,11 @@ equal modulo α and β-equivalence.
 @examples[
 
 
-(eval:alts (cur-equal? #'(lambda (a : Type) a) #'(lambda (b : Type) b))
+(eval:alts (cur-equal? #'(λ (a : Type) a) #'(λ (b : Type) b))
            (eval:result @racket[#t] "" ""))
-(eval:alts (cur-equal? #'((lambda (a : Type) a) Bool) #'Bool)
+(eval:alts (cur-equal? #'((λ (a : Type) a) Bool) #'Bool)
            (eval:result @racket[#t] "" ""))
-(eval:alts (cur-equal? #'(lambda (a : Type) (sub1 (s z))) #'(lambda (a : Type) z))
+(eval:alts (cur-equal? #'(λ (a : Type) (sub1 (s z))) #'(λ (a : Type) z))
            (eval:result @racket[#f] "" ""))
 ]
 }
@@ -111,7 +106,7 @@ Converts @racket[s] to a datum representation of the @tech{curnel form}, after e
 @examples[
 
 
-(eval:alts (cur-?datum #'(lambda (a : Type) a))
+(eval:alts (cur->datum #'(λ (a : Type) a))
            (eval:result @racket['(λ (a : (Unv 0) a))] "" ""))
 ]
 }

cur-doc/cur/scribblings/stdlib.scrbl

@@ -7,5 +7,10 @@ Cur has a small standard library, primary for demonstration purposes.
 
 @local-table-of-contents[]
 
-@include-section{stdlib/tactics.scrbl}
 @include-section{stdlib/sugar.scrbl}
+@include-section{stdlib/bool.scrbl}
+@include-section{stdlib/nat.scrbl}
+@include-section{stdlib/maybe.scrbl}
+@include-section{stdlib/list.scrbl}
+@include-section{stdlib/typeclass.scrbl}
+@include-section{stdlib/tactics.scrbl}

cur-doc/cur/scribblings/stdlib/bool.scrbl

@@ -0,0 +1,54 @@
+#lang scribble/manual
+
+@(require
+  "../defs.rkt"
+  scribble/eval)
+
+@(define curnel-eval (curnel-sandbox "(require cur/stdlib/bool cur/stdlib/sugar)"))
+
+@title{Bool}
+@defmodule[cur/stdlib/bool]
+This library defines the datatype @racket[Bool] and several functions and forms for using them.
+
+@; TODO: Define a @defdata macro for Cur
+@deftogether[(@defthing[Bool Type]
+              @defthing[true Bool]
+	      @defthing[false Bool])]{
+The boolean datatype.
+}
+
+@defform[(if test-expr c-expr alt-expr)]{
+A syntactic form that expands to the inductive eliminator for @racket[Bool]. This form is currently non-dependent---the branches do not know that @racket[test-expr] is equal to @racket[true] or @racket[false].
+
+@examples[#:eval curnel-eval
+          (if true false true)
+	  (elim Bool (λ (x : Bool) Bool) () (false true) true)]
+}
+
+@defproc[(not [x Bool])
+         Bool]{
+Negates the boolean @racket[x].
+
+@examples[#:eval curnel-eval
+          (not true)
+	  (not false)]
+}
+
+@defproc[(and [x Bool] [y Bool])
+         Bool]{
+The boolean @racket[and]. True if and only if @racket[x] and @racket[y] are both either @racket[true] or @racket[false].
+
+@examples[#:eval curnel-eval
+          (and true true)
+	  (and false true)]
+}
+
+@defproc[(or [x Bool] [y Bool])
+         Bool]{
+The boolean @racket[or]. True if and only if either @racket[x] or @racket[y] is @racket[true].
+
+@examples[#:eval curnel-eval
+          (or true true)
+	  (or false true)
+	  (or false false)]
+}

cur-doc/cur/scribblings/stdlib/list.scrbl

@@ -0,0 +1,21 @@
+#lang scribble/manual
+
+@(require
+  "../defs.rkt"
+  scribble/eval)
+
+@(define curnel-eval (curnel-sandbox "(require cur/stdlib/bool cur/stdlib/nat cur/stdlib/sugar cur/stdlib/list)"))
+
+@title{List}
+@defmodule[cur/stdlib/list]
+This library defines the datatype @racket[List] and several functions on them.
+
+@deftogether[(@defthing[List (-> Type Type)]
+              @defthing[nil (forall (A : Type) (List A))]
+	      @defthing[cons (forall (A : Type) (a : A) (-> (List A) (List A)))])]{
+The polymorphic list datatype.
+}
+
+@defproc[(list-ref [A Type] [ls (List A)] [n Nat]) (Maybe A)]{
+Returns the @racket[n]th element of @racket[ls] in the @racket[Maybe] monad.
+}

cur-doc/cur/scribblings/stdlib/maybe.scrbl

@@ -0,0 +1,26 @@
+#lang scribble/manual
+
+@(require
+  "../defs.rkt"
+  scribble/eval)
+
+@(define curnel-eval (curnel-sandbox "(require cur/stdlib/bool cur/stdlib/maybe cur/stdlib/sugar)"))
+
+@title{Maybe}
+@defmodule[cur/stdlib/maybe]
+This library defines the datatype @racket[Maybe] and several forms for using them.
+
+@; TODO: Define a @defdata macro for Cur
+@deftogether[(@defthing[Maybe (∀ (A : Type) Type)]
+              @defthing[none (∀ (A : Type) (Maybe A))]
+	      @defthing[some (∀ (A : Type) (a : A) (Maybe A))])]{
+The maybe datatype.
+}
+
+@defform[(some/i a)]{
+A syntactic form for @racket[some] that attempts to infer the type of the expression @racket[a] to reduce annotation burden.
+
+@examples[#:eval curnel-eval
+          (some Bool true)
+	  (some/i true)]
+}

cur-doc/cur/scribblings/stdlib/nat.scrbl

@@ -0,0 +1,98 @@
+#lang scribble/manual
+
+@(require
+  "../defs.rkt"
+  scribble/eval)
+
+@(define curnel-eval (curnel-sandbox "(require cur/stdlib/bool cur/stdlib/nat cur/stdlib/sugar)"))
+
+@title{Nat}
+@defmodule[cur/stdlib/nat]
+This library defines the datatype @racket[Nat] and several functions on them.
+
+@deftogether[(@defthing[Nat Type]
+              @defthing[z Nat]
+	      @defthing[s (-> Nat Nat)])]{
+The natural number datatype.
+}
+
+@defproc[(add1 [n Nat]) Nat]{
+A more lispy name for @racket[s].
+
+@examples[#:eval curnel-eval
+          (s z)
+	  (add1 z)]
+}
+
+@defproc[(sub1 [n Nat]) Nat]{
+Return the predecessor of @racket[n], or @racket[z] is @racket[n] is @racket[z].
+
+@examples[#:eval curnel-eval
+          (sub1 (s z))]
+
+}
+
+@defproc[(plus [n Nat] [m Nat]) Nat]{
+Add @racket[n] and @racket[m].
+
+@examples[#:eval curnel-eval
+          (plus (s z) (s z))
+	  (plus z (s z))
+	  (plus (s (s z)) (s z))]
+}
+
+@defproc[(mult [n Nat] [m Nat]) Nat]{
+Multiply @racket[n] and @racket[m].
+
+@examples[#:eval curnel-eval
+          (mult (s z) (s z))
+	  (mult z (s z))
+	  (mult (s (s z)) (s z))]
+}
+
+
+@defproc[(exp [m Nat] [e Nat]) Nat]{
+Compute @racket[e] to the @racket[m]th exponent.
+Due to limitations in Cur, running @racket[exp] takes to long to be
+useful on numbers larger than @racket[(s z)].
+
+@;@examples[#:eval curnel-eval
+@;          (exp (s z) (s z))
+@;	  (exp z (s z))]
+}
+
+@defproc[(square [m Nat]) Nat]{
+Compute @racket[m] squared, i.e., @racket[(exp m (s (s z)))].
+Due to limitations in Cur, running @racket[square] takes to long to be
+useful on numbers larger than @racket[(s z)].
+
+@;@examples[#:eval curnel-eval
+@;	  (square z)]
+}
+
+@defproc[(nat-equal? [n Nat] [m Nat]) Bool]{
+Return @racket[true] if and only if @racket[n] is equal to @racket[m].
+
+@examples[#:eval curnel-eval
+          (nat-equal? (s z) (s z))
+	  (nat-equal? z (s z))]
+}
+
+@defproc[(even? [n Nat]) Bool]{
+Return @racket[true] if and only if @racket[n] is even.
+
+@examples[#:eval curnel-eval
+          (even? (s z))
+	  (even? z)
+	  (even? (s (s z)))]
+
+}
+
+@defproc[(odd? [n Nat]) Bool]{
+Return @racket[true] if and only if @racket[n] is not even.
+
+@examples[#:eval curnel-eval
+          (odd? (s z))
+	  (odd? z)
+	  (odd? (s (s z)))]
+}

cur-doc/cur/scribblings/stdlib/sugar.scrbl

@@ -0,0 +1,207 @@
+#lang scribble/manual
+
+@(require
+  "../defs.rkt"
+  scribble/eval)
+
+@(define curnel-eval (curnel-sandbox "(require cur/stdlib/nat cur/stdlib/bool cur/stdlib/sugar cur/stdlib/list)"))
+
+
+@title{Sugar}
+The @tech{curnel forms} are sort of terrible for actually writing code. Functions and applications are
+limited to single artity. Functions type must be specified using the dependent @racket[forall], even
+when the dependency is not used. Inductive elimination can only be done via the primitive eliminator
+and not via pattern matching. However, with the full force of Racket's syntactic extension system, we
+can define not only simply notation, but redefine what application means, or define a pattern matcher
+that expands into the eliminator.
+
+@defmodule[cur/stdlib/sugar]
+This library defines various syntactic extensions making Cur easier to write than writing raw TT.
+
+@defform*[((-> decl decl ... type)
+           (→ decl decl ... type)
+	   (forall decl decl ... type)
+	   (∀ decl decl ... type)
+	   (Π decl decl ... type)
+	   (Pi decl decl ... type))
+	  #:grammar
+	  [(decl
+	     type
+	     (code:line (identifier : type)))]]{
+A multi-artiy function type that supports dependent and non-dependent type declarations and automatic currying.
+We provide lots of names for this form, because there are lots of synonyms in the literature.
+
+@examples[#:eval curnel-eval
+          (data And : (-> Type Type Type)
+            (conj : (-> (A : Type) (B : Type) A B ((And A) B))))
+          ((((conj Bool) Bool) true) false)]
+
+@examples[#:eval curnel-eval
+          (data And : (forall Type Type Type)
+            (conj : (forall (A : Type) (B : Type) A B (And A B))))
+          ((((conj Bool) Bool) true) false)]
+
+}
+
+@defform*[((lambda (a : t) ... body)
+           (λ (a : t) ... body))]{
+Defines a multi-arity procedure that supports automatic currying.
+
+@examples[#:eval curnel-eval
+          ((lambda (x : Bool) (lambda (y : Bool) y)) true)
+          ((lambda (x : Bool) (y : Bool) y) true)
+          ]
+}
+
+@defform[(#%app f a ...)]{
+Defines multi-arity procedure application via automatic currying.
+
+@examples[#:eval curnel-eval
+          (data And : (-> Type Type Type)
+	    (conj : (-> (A : Type) (B : Type) A B ((And A) B))))
+          (conj Bool Bool true false)]
+}
+
+@defform[(: name type)]{
+Declare that the @emph{function} which will be defined as @racket[name] has type @racket[type].
+Must precede the definition of @racket[name].
+@racket[type] must expand to a function type of the form @racket[(Π (x : t1) t2)]
+When used, this form allows omitting the annotations on arguments in the definition @racket[name]
+}
+
+@defform*[((define name body)
+           (define (name x ...) body)
+	   (define (name (x : t) ...) body))]{
+Like the @racket[define] provided by @racketmodname[cur], but supports
+defining curried functions via @racket[lambda].
+The second form, @racket[(define (name x ...) body)], can only be used when
+a @racket[(: name type)] form appears earlier in the module.
+
+@examples[#:eval curnel-eval
+          (: id (forall (A : Type) (a : A) A))
+	  (define (id A a) a)]
+}
+
+@defform*[((define-type name type)
+           (define-type (name (a : t) ...) body))]{
+Like @racket[define], but uses @racket[forall] instead of @racket[lambda].
+}
+
+@defform[(match e [maybe-in] [maybe-return] [pattern body] ...)
+         #:grammar
+         [(maybe-in
+	    (code:line #:in type))
+	  (maybe-return
+	    (code:line #:return type))
+	  (pattern
+            constructor
+            (code:line (constructor (x : t) ...)))]]{
+A pattern-matcher-like syntax for inductive elimination.
+Does not actually do pattern matching; instead, relies on the
+constructors patterns being specified in the same order as when the
+inductive type was defined.
+Inside the @racket[body], @racket[recur] can be used to refer to the
+inductive hypotheses for an inductive argument.
+Generates a call to the inductive eliminator for @racket[e].
+Currently does not work on inductive type-families as types indices
+are not inferred.
+
+If @racket[#:in] is not specified, attempts to infer the type of @racket[e].
+If @racket[#:return] is not specified, attempts to infer the return type of the @racket[match].
+
+@examples[#:eval curnel-eval
+          (match z
+            [z true]
+            [(s (n : Nat))
+             false])]
+
+@examples[#:eval curnel-eval
+          (match (s z)
+	    #:in Nat
+	    #:return Bool
+            [z true]
+            [(s (n : Nat))
+	    (not (recur n))])]
+
+@examples[#:eval curnel-eval
+          ((match (nil Bool)
+            [(nil (A : Type))
+	     (lambda (n : Nat)
+	       (none A))]
+            [(cons (A : Type) (a : A) (rest : (List A)))
+	     (lambda (n : Nat)
+	       (match n
+	         [z (some A a)]
+		 [(s (n-1 : Nat))
+		  ((recur rest) n-1)]))])
+	   z)]
+
+}
+
+@defform[(recur id)]{
+A form valid only in the body of a @racket[match] clause.
+Generates a reference to the induction hypothesis for @racket[x]
+inferred by a @racket[match] clause.
+}
+
+@defform[(let (clause ...) body)
+         #:grammar
+         [(clause
+            (code:line (id expr))
+            (code:line ((id : type) expr)))]]{
+Evaluates the expressions @racket[expr] from each clause, left to right, and binds them to each
+@racket[id]. If a @racket[type] is not given for the @racket[id], attempts to infer the type of the
+corresponding @racket[expr], raising a syntax error if no type can be inferred.
+
+@examples[#:eval curnel-eval
+          (let ([x Type]
+                [y (λ (x : (Type 1)) x)])
+            (y x))
+          (let ([x uninferrable-expr]
+                [y (λ (x : (Type 1)) x)])
+            (y x))]
+}
+
+@defform[(:: e type)]{
+Check that expression @racket[e] has type @racket[type], causing a type-error if not, and producing
+@racket[(void)] if so.
+
+@examples[#:eval curnel-eval
+          (:: z Nat)
+          (:: true Nat)]
+}
+
+@defform[(run syn)]{
+Like @racket[cur-normalize], but is a syntactic form to be used in surface syntax.
+Allows a Cur term to be written by computing part of the term from
+another Cur term.
+
+@examples[#:eval curnel-eval
+          (lambda (x : (run (if true Bool Nat))) x)]
+
+}
+
+@defform[(step syn)]{
+Like @racket[run], but uses @racket[cur-step] to evaluate only one step and prints intermediate
+results before returning the result of evaluation.
+
+@examples[#:eval curnel-eval
+          (step (plus z z))]
+
+}
+
+@defform[(step-n natural syn)]{
+Like @racket[step], but expands to @racket[natural] calls to @racket[step].
+
+@examples[#:eval curnel-eval
+          (step-n 3 (plus z z))]
+
+}
+
+@defform[(query-type expr)]{
+Print the type of @racket[expr], at compile-time. Similar to Coq's @racketfont{Check}.
+
+@examples[#:eval curnel-eval
+          (query-type Bool)]
+
+}

cur-doc/cur/scribblings/stdlib/tactics.scrbl

@@ -1,12 +1,16 @@
 #lang scribble/manual
 
-@(require "../defs.rkt")
+@(require
+  "../defs.rkt"
+  scribble/eval)
 
 @title{Tactics}
 As Coq has shown, tactics have proven useful for doing complex proofs. In Cur, tactics are not
 built-in or provided by the language. However, any user can use meta-programming to add tactics to
 Cur. A tactic system ships in the standard library, written entirely in user-land code.
 
+@(define curnel-eval (curnel-sandbox "(require cur/stdlib/tactics/base cur/stdlib/tactics/standard cur/stdlib/bool cur/stdlib/nat)"))
+
 @section{Proof State and Defining Tactics}
 @defmodule[cur/stdlib/tactics/base]
 
@@ -17,11 +21,9 @@ Defines a new @tech{tactic}, at @gtech{phase} 1. A @deftech{tactic} is a Racket
 number of arguments, plus the @tech{proof state}. The @tech{proof state} must be the final argument of
 the tactic.
 
-Examples:
-@racketblock[
+@examples[#:eval curnel-eval
 (define-tactic (do-nothing ps)
   ps)
-
 (define-tactic (switch-goal i ps)
   (struct-copy proof-state ps
     [current-goal i]))
@@ -51,15 +53,17 @@ Returns an empty partial @tech{proof}, i.e., the identity function.
                         [current-goal natural-number/c]
                         [proof (or/c syntax? procedure?)]
                         [theorem syntax?])]{
-The environment @racket[env] is a map of assumptions local to the theorem from symbols (names) to the
+A structure representing the @deftech{proof state} for the proof of the current @tech{theorem}.
+
+The @deftech{environment} @racket[env] is a map of assumptions local to the @tech{proof} from symbols (names) to the
 type of the assumption as a syntax object.
-The list of goals @racket[goals] is a map from natural numbers to goals, types as syntax objects.
-The current goal @racket[current-goal] is a natural number indexing into @racket[goals], representing
+The list of @deftech{goals} @racket[goals] is a map from natural numbers to goals, types as syntax objects.
+The @deftech{current goal} @racket[current-goal] is a natural number indexing into @racket[goals], representing
 the goal currently in focus.
-The @racket[proof] is the @tech{proof} of the theorem so far. The @racket[proof] is either a
+The @racket[proof] is the @tech{proof} of the @tech{theorem} so far. The @racket[proof] is either a
 syntax object if complete, or a procedure which expects a proof to replace the current holes in the
 @racket[proof].
-The @racket[theorem] is the original statement of the theorem to be proved.
+The @racket[theorem] is the original statement of the @tech{theorem} to be proved.
 }
 
 @defproc[(new-proof-state [prop syntax?])
@@ -140,7 +144,8 @@ tactic is defined and a theorem has been defined but not proved.
 }
 
 @defform[(define-theorem name prop)]{
-Defines a new theorem.
+Defines a new @deftech{theorem}. Theorem are Cur types that can be
+inhabited using the tactic language starting with @racket[proof].
 }
 
 @defform[(proof (tactic args ...) ...)]{
@@ -150,16 +155,12 @@ saved anywhere, only checked against the most recent theorem defined via @racket
 Note that the proof state is implicitly given to each call by @racket[proof] and should not appear as
 an explicit argument.
 
-Examples:
-@racketblock[
+@examples[#:eval curnel-eval
 (define-theorem a-silly-theorem (forall (x : Nat) Nat))
-(proof
-  (intro x)
-  (by-assumption))
+(proof (intro x) (by-assumption))
 
 (define-theorem falseo (forall (x : Type) x))
-(proof
-  (interactive))
+(eval:alts (proof (interactive)) (void))
 ]
 }
 

cur-doc/cur/scribblings/stdlib/typeclass.scrbl

@@ -0,0 +1,42 @@
+#lang scribble/manual
+
+@(require
+  "../defs.rkt"
+  scribble/eval)
+
+@(define curnel-eval (curnel-sandbox "(require cur/stdlib/typeclass cur/stdlib/bool cur/stdlib/nat cur/stdlib/sugar)"))
+
+@title{Typeclass}
+@defmodule[cur/stdlib/typeclass]
+This library defines some macros that provide ad-hoc polymorphism
+similar to typeclasses, although lacking some of the crucial features
+of typeclasses such as typeclass constraints. These typeclasses are
+added entirely through meta-programming.
+
+@defform[(typeclass (class (param : Type)) (name : t) ...)]{
+Declares a new typeclass named @racket[class], whose parameter
+@racket[param] has type @racket[Type]. Implementations of this
+typeclass must define of the methods @racket[name ...] whose types
+are @racket[t ...].
+
+@examples[#:eval curnel-eval
+          (typeclass (Eqv (A : Type))
+	    (equal? : (forall (a : A) (b : A) Bool)))]
+}
+
+@defform[(impl (class param) defs ...)]{
+Provides an implementation of the typeclass @racket[class] for the
+type @racket[param]. The defintions @racket[defs ...] are Cur
+definitions for each of the methods of the typeclass.
+
+@examples[#:eval curnel-eval
+          (impl (Eqv Bool)
+            (define (equal? (a : Bool) (b : Bool))
+              (if a
+                  (if b true false)
+		  (if b false true))))
+          (impl (Eqv Nat)
+            (define equal? nat-equal?))
+          (equal? true true)
+	  (equal? z z)]
+}

cur-doc/info.rkt

@@ -0,0 +1,6 @@
+#lang info
+(define collection 'multi)
+(define deps '("base" "racket-doc"))
+(define build-deps '("scribble-lib" ("cur-lib" #:version "0.4") "sandbox-lib"))
+(define pkg-desc "Documentation for \"cur\".")
+(define pkg-authors '(wilbowma))

cur-lib/cur/curnel/redex-core.rkt

@@ -0,0 +1,562 @@
+#lang racket/base
+
+(require
+  racket/function
+  racket/list
+  redex/reduction-semantics)
+
+(provide
+  (all-defined-out))
+
+(set-cache-size! 10000)
+
+#| References:
+ |  http://www3.di.uminho.pt/~mjf/pub/SFV-CIC-2up.pdf
+ |  https://www.cs.uoregon.edu/research/summerschool/summer11/lectures/oplss-herbelin1.pdf
+ |  http://www.emn.fr/z-info/ntabareau/papers/universe_polymorphism.pdf
+ |  http://people.cs.kuleuven.be/~jesper.cockx/Without-K/Pattern-matching-without-K.pdf
+ |  http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.37.74
+ |  http://eb.host.cs.st-andrews.ac.uk/writings/thesis.pdf
+ |#
+
+#| ttL is the core language of Cur. Very similar to TT (Idirs core) and Luo's UTT. Surface
+ | langauge should provide short-hand, such as -> for non-dependent function types, and type
+ | inference.
+ |#
+(define-language ttL
+  (i j k  ::= natural)
+  (U ::= (Unv i))
+  (D x c ::= variable-not-otherwise-mentioned)
+  (Δ   ::= ∅ (Δ (D : t ((c : t) ...))))
+  (t e ::= U (λ (x : t) e) x (Π (x : t) t) (e e)
+     ;; (elim inductive-type motive (indices ...) (methods ...) discriminant)
+     (elim D e (e ...) (e ...) e))
+  #:binding-forms
+  (λ (x : t) e #:refers-to x)
+  (Π (x : t_0) t_1 #:refers-to x))
+
+(define x? (redex-match? ttL x))
+(define t? (redex-match? ttL t))
+(define e? (redex-match? ttL e))
+(define U? (redex-match? ttL U))
+(define Δ? (redex-match? ttL Δ))
+
+;;; ------------------------------------------------------------------------
+;;; Universe typing
+
+;; Universe types
+;; aka Axioms A of a PTS
+(define-judgment-form ttL
+  #:mode (unv-type I O)
+  #:contract (unv-type U U)
+
+  [(where i_1 ,(add1 (term i_0)))
+   -----------------
+   (unv-type (Unv i_0) (Unv i_1))])
+
+;; Universe predicativity rules. Impredicative in (Unv 0)
+;; aka Rules R of a PTS
+(define-judgment-form ttL
+  #:mode (unv-pred I I O)
+  #:contract (unv-pred U U U)
+
+  [----------------
+   (unv-pred (Unv i) (Unv 0) (Unv 0))]
+
+  [(where i_3 ,(max (term i_1) (term i_2)))
+   ----------------
+   (unv-pred (Unv i_1) (Unv i_2) (Unv i_3))])
+
+(define-metafunction ttL
+  α-equivalent?  : t t -> #t or #f
+  [(α-equivalent? t_0 t_1)
+   ,(alpha-equivalent? ttL (term t_0) (term t_1))])
+
+;; Replace x by t_1 in t_0
+(define-metafunction ttL
+  subst : t x t -> t
+  [(subst t_0 x t_1)
+   (substitute t_0 x t_1)])
+
+(define-metafunction ttL
+  subst-all : t (x ...) (e ...) -> t
+  [(subst-all t () ()) t]
+  [(subst-all t (x_0 x ...) (e_0 e ...))
+   (subst-all (subst t x_0 e_0) (x ...) (e ...))])
+
+;;; ------------------------------------------------------------------------
+;;; Primitive Operations on signatures Δ (those operations that do not require contexts)
+
+;;; TODO: Might be worth maintaining the above bijection between Δ and maps for performance reasons
+
+;; TODO: This is doing too many things
+;; NB: Depends on clause order
+(define-metafunction ttL
+  Δ-ref-type : Δ x -> t or #f
+  [(Δ-ref-type ∅ x) #f]
+  [(Δ-ref-type (Δ (x : t any)) x) t]
+  [(Δ-ref-type (Δ (x_0 : t_0 ((x_1 : t_1) ... (x : t) (x_2 : t_2) ...))) x) t]
+  [(Δ-ref-type (Δ (x_0 : t_0 any)) x) (Δ-ref-type Δ x)])
+
+(define-metafunction ttL
+  Δ-set : Δ x t ((x : t) ...) -> Δ
+  [(Δ-set Δ x t any) (Δ (x : t any))])
+
+(define-metafunction ttL
+  Δ-union : Δ Δ -> Δ
+  [(Δ-union Δ ∅) Δ]
+  [(Δ-union Δ_2 (Δ_1 (x : t any)))
+   ((Δ-union Δ_2 Δ_1) (x : t any))])
+
+;; TODO: Should not use Δ-ref-type
+(define-metafunction ttL
+  Δ-ref-constructor-type : Δ x x -> t
+  [(Δ-ref-constructor-type Δ x_D x_ci)
+   (Δ-ref-type Δ x_ci)])
+
+;; Get the list of constructors for the inducitvely defined type x_D
+;; NB: Depends on clause order
+(define-metafunction ttL
+  Δ-ref-constructors : Δ x -> (x ...) or #f
+  [(Δ-ref-constructors ∅ x_D) #f]
+  [(Δ-ref-constructors (Δ (x_D : t_D ((x : t) ...))) x_D)
+   (x ...)]
+  [(Δ-ref-constructors (Δ (x_1 : t_1 any)) x_D)
+   (Δ-ref-constructors Δ x_D)])
+
+;; TODO: Mix of pure Redex/escaping to Racket sometimes is getting confusing.
+;; TODO: Justify, or stop.
+
+;; NB: Depends on clause order
+(define-metafunction ttL
+  sequence-index-of : any (any ...) -> natural
+  [(sequence-index-of any_0 (any_0 any ...))
+   0]
+  [(sequence-index-of any_0 (any_1 any ...))
+   ,(add1 (term (sequence-index-of any_0 (any ...))))])
+
+;; Get the index of the constructor x_ci in the list of constructors for x_D
+(define-metafunction ttL
+  Δ-constructor-index : Δ x x -> natural
+  [(Δ-constructor-index Δ x_D x_ci)
+   (sequence-index-of x_ci (Δ-ref-constructors Δ x_D))])
+
+;;; ------------------------------------------------------------------------
+;;; Operations that involve contexts.
+
+(define-extended-language tt-ctxtL ttL
+  ;; Telescope.
+  ;; NB: There is a bijection between this an a vector of maps from x to t
+  (Ξ Φ ::= hole (Π (x : t) Ξ))
+  ;; Apply context
+  ;; NB: There is a bijection between this an a vector expressions
+  (Θ   ::= hole (Θ e)))
+
+(define Ξ? (redex-match? tt-ctxtL Ξ))
+(define Φ? (redex-match? tt-ctxtL Φ))
+(define Θ? (redex-match? tt-ctxtL Θ))
+
+;; TODO: Might be worth it to actually maintain the above bijections, for performance reasons.
+
+
+;; Applies the term t to the telescope Ξ.
+;; TODO: Test
+#| TODO:
+ | This essentially eta-expands t at the type-level. Why is this necessary? Shouldn't it be true
+ | that (convert t (Ξ-apply Ξ t))?
+ | Maybe not. t is a lambda whose type is convert to (Ξ-apply Ξ t)? Yes.
+ |#
+(define-metafunction tt-ctxtL
+  Ξ-apply : Ξ t -> t
+  [(Ξ-apply hole t) t]
+  [(Ξ-apply (Π (x : t) Ξ) t_0) (Ξ-apply Ξ (t_0 x))])
+
+;; Compute the number of arguments in a Ξ
+(define-metafunction tt-ctxtL
+  Ξ-length : Ξ -> natural
+  [(Ξ-length hole) 0]
+  [(Ξ-length (Π (x : t) Ξ)) ,(add1 (term (Ξ-length Ξ)))])
+
+(define-metafunction tt-ctxtL
+  list->Θ : (e ...) -> Θ
+  [(list->Θ ()) hole]
+  [(list->Θ (e e_r ...))
+   (in-hole (list->Θ (e_r ...)) (hole e))])
+
+(define-metafunction tt-ctxtL
+  apply : e e ... -> e
+  [(apply e_f e ...)
+   (in-hole (list->Θ (e ...)) e_f)])
+
+;; Reference an expression in Θ by index; index 0 corresponds to the the expression applied to a hole.
+(define-metafunction tt-ctxtL
+  Θ-ref : Θ natural -> e or #f
+  [(Θ-ref hole natural) #f]
+  [(Θ-ref (in-hole Θ (hole e)) 0) e]
+  [(Θ-ref (in-hole Θ (hole e)) natural) (Θ-ref Θ ,(sub1 (term natural)))])
+
+;;; ------------------------------------------------------------------------
+;;; Computing the types of eliminators
+
+;; Return the parameters of x_D as a telescope Ξ
+;; TODO: Define generic traversals of Δ and Γ ?
+(define-metafunction tt-ctxtL
+  Δ-ref-parameter-Ξ : Δ x -> Ξ or #f
+  [(Δ-ref-parameter-Ξ (Δ (x_D : (in-hole Ξ U) any)) x_D)
+   Ξ]
+  [(Δ-ref-parameter-Ξ (Δ (x_1 : t_1 any)) x_D)
+   (Δ-ref-parameter-Ξ Δ x_D)]
+  [(Δ-ref-parameter-Ξ Δ x)
+   #f])
+
+;; Returns the telescope of the arguments for the constructor x_ci of the inductively defined type x_D
+(define-metafunction tt-ctxtL
+  Δ-constructor-telescope : Δ x x -> Ξ
+  [(Δ-constructor-telescope Δ x_D x_ci)
+   Ξ
+   (where (in-hole Ξ (in-hole Θ x_D))
+     (Δ-ref-constructor-type Δ x_D x_ci))])
+
+;; Returns the parameter arguments as an apply context of the constructor x_ci of the inductively
+;; defined type x_D
+(define-metafunction tt-ctxtL
+  Δ-constructor-parameters : Δ x x -> Θ
+  [(Δ-constructor-parameters Δ x_D x_ci)
+   Θ
+   (where (in-hole Ξ (in-hole Θ x_D))
+     (Δ-ref-constructor-type Δ x_D x_ci))])
+
+;; Inner loop for Δ-constructor-inductive-telescope
+;; NB: Depends on clause order
+(define-metafunction tt-ctxtL
+  inductive-loop : x Φ -> Φ
+  [(inductive-loop x_D hole) hole]
+  [(inductive-loop x_D (Π (x : (in-hole Φ (in-hole Θ x_D))) Φ_1))
+   (Π (x : (in-hole Φ (in-hole Θ x_D))) (inductive-loop x_D Φ_1))]
+  [(inductive-loop x_D (Π (x : t) Φ_1))
+   (inductive-loop x_D Φ_1)])
+
+;; Returns the inductive arguments to the constructor x_ci of the inducitvely defined type x_D
+(define-metafunction tt-ctxtL
+  Δ-constructor-inductive-telescope : Δ x x -> Ξ
+  [(Δ-constructor-inductive-telescope Δ x_D x_ci)
+   (inductive-loop x_D (Δ-constructor-telescope Δ x_D x_ci))])
+
+;; Returns the inductive hypotheses required for eliminating the inductively defined type x_D with
+;; motive t_P, where the telescope Φ are the inductive arguments to a constructor for x_D
+(define-metafunction tt-ctxtL
+  hypotheses-loop : x t Φ -> Φ
+  [(hypotheses-loop x_D t_P hole) hole]
+  [(hypotheses-loop x_D t_P (name any_0 (Π (x : (in-hole Φ (in-hole Θ x_D))) Φ_1)))
+   ;; TODO: Instead of this nonsense, it might be simpler to pass in the type of t_P and use that
+   ;; as/to compute the type of the hypothesis.
+   (Π (x_h : (in-hole Φ ((in-hole Θ t_P) (Ξ-apply Φ x))))
+      (hypotheses-loop x_D t_P Φ_1))
+   (where x_h ,(variable-not-in (term (x_D t_P any_0)) 'x-ih))])
+
+;; Computes the type of the eliminator for the inductively defined type x_D with a motive whose result
+;; is in universe U.
+;;
+;; The type of (elim x_D U) is something like:
+;;  (∀ (P : (∀ a -> ... -> (D a ...) -> U))
+;;     (method_ci ...) -> ... ->
+;;     (a -> ... -> (D a ...) ->
+;;       (P a ... (D a ...))))
+;;
+;; x_D   is an inductively defined type
+;; U     is the sort the motive
+;; x_P   is the name of the motive
+;; Ξ_P*D is the telescope of the parameters of x_D and
+;;       the witness of type x_D (applied to the parameters)
+;; Ξ_m   is the telescope of the methods for x_D
+
+;; Returns the inductive hypotheses required for the elimination method of constructor c_i for
+;; inductive type D, when eliminating with motive t_P.
+(define-metafunction tt-ctxtL
+  Δ-constructor-inductive-hypotheses : Δ D c t -> Ξ
+  [(Δ-constructor-inductive-hypotheses Δ D c_i t_P)
+   (hypotheses-loop D t_P (Δ-constructor-inductive-telescope Δ D c_i))])
+
+;; Returns the type of the method corresponding to c_i
+(define-metafunction tt-ctxtL
+  Δ-constructor-method-type : Δ D c t -> t
+  [(Δ-constructor-method-type Δ D c_i t_P)
+   (in-hole Ξ_a (in-hole Ξ_h ((in-hole Θ_p t_P) (Ξ-apply Ξ_a c_i))))
+   (where Θ_p (Δ-constructor-parameters Δ D c_i))
+   (where Ξ_a (Δ-constructor-telescope Δ D c_i))
+   (where Ξ_h (Δ-constructor-inductive-hypotheses Δ D c_i t_P))])
+
+(define-metafunction tt-ctxtL
+  Δ-method-types : Δ D e -> (t ...)
+  [(Δ-method-types Δ D e)
+   ,(map (lambda (c) (term (Δ-constructor-method-type Δ D ,c e))) (term (c ...)))
+   (where (c ...) (Δ-ref-constructors Δ D))])
+
+(define-metafunction tt-ctxtL
+  Δ-motive-type : Δ D U -> t
+  [(Δ-motive-type Δ D U)
+   (in-hole Ξ_P*D U)
+   (where Ξ (Δ-ref-parameter-Ξ Δ D))
+   ;; A fresh name to bind the discriminant
+   (where x ,(variable-not-in (term (Δ D Ξ)) 'x-D))
+   ;; The telescope (∀ a -> ... -> (D a ...) hole), i.e.,
+   ;; of the indices and the inductive type applied to the
+   ;; indices
+   (where Ξ_P*D (in-hole Ξ (Π (x : (Ξ-apply Ξ D)) hole)))])
+
+;;; ------------------------------------------------------------------------
+;;; Dynamic semantics
+;;; The majority of this section is dedicated to evaluation of (elim x U), the eliminator for the
+;;; inductively defined type x with a motive whose result is in universe U
+
+(define-extended-language tt-redL tt-ctxtL
+  (v  ::= x U (Π (x : t) t) (λ (x : t) t) (in-hole Θv c))
+  (Θv ::= hole (Θv v))
+  (C-elim  ::= (elim D t_P (e_i ...) (e_m ...) hole))
+  ;; call-by-value
+  (E  ::= hole (E e) (v E)
+      (elim D e (e ...) (v ... E e ...) e)
+      (elim D e (e ...) (v ...) E)
+      ;; reduce under Π (helps with typing checking)
+      ;; TODO: Should be done in conversion judgment
+      (Π (x : v) E) (Π (x : E) e)))
+
+(define Θv? (redex-match? tt-redL Θv))
+(define E? (redex-match? tt-redL E))
+(define v? (redex-match? tt-redL v))
+
+#|
+ | The elim form must appear applied like so:
+ | (elim D U v_P m_0 ... m_i m_j ... m_n p ... (c_i a ...))
+ |
+ | Where:
+ |   D       is the inductive being eliminated
+ |   U         is the universe of the result of the motive
+ |   v_P       is the motive
+ |   m_{0..n}  are the methods
+ |   p ...     are the parameters of x_D
+ |   c_i       is a constructor of x_d
+ |   a ...     are the arguments to c_i
+ |
+ | Using contexts, this appears as (in-hole Θ ((elim D U) v_P))
+ |#
+(define-metafunction tt-ctxtL
+  is-inductive-argument : Δ D t -> #t or #f
+  ;; Think this only works in call-by-value. A better solution would
+  ;; be to check position of the argument w.r.t. the current
+  ;; method. requires more arguments, and more though.q
+  [(is-inductive-argument Δ D (in-hole Θ c_i))
+   ,(and (memq (term c_i) (term (Δ-ref-constructors Δ D))) #t)])
+
+;; Generate recursive applications of the eliminator for each inductive argument of type x_D.
+;; In more detail, given motive t_P, parameters Θ_p, methods Θ_m, and arguments Θ_i to constructor
+;; x_ci for x_D, for each inductively smaller term t_i of type (in-hole Θ_p x_D) inside Θ_i,
+;; generate: (elim x_D U t_P  Θ_m ... Θ_p ... t_i)
+;; TODO TTEESSSSSTTTTTTTT
+(define-metafunction tt-redL
+  Δ-inductive-elim : Δ D C-elim Θ -> Θ
+  ;; NB: If metafunction fails, recursive
+  ;; NB: elimination will be wrong. This will introduced extremely sublte bugs,
+  ;; NB: inconsistency, failure of type safety, and other bad things.
+  ;; NB: It should be tested and audited thoroughly
+  [(Δ-inductive-elim any ... hole)
+   hole]
+  [(Δ-inductive-elim Δ D C-elim (Θ_c t_i))
+   ((Δ-inductive-elim Δ D C-elim Θ_c)
+    (in-hole C-elim t_i))
+   (side-condition (term (is-inductive-argument Δ D t_i)))]
+  [(Δ-inductive-elim any ... (Θ_c t_i))
+   (Δ-inductive-elim any ... Θ_c)])
+
+(define tt-->
+  (reduction-relation tt-redL
+    (--> (Δ (in-hole E ((λ (x : t_0) t_1) t_2)))
+         (Δ (in-hole E (subst t_1 x t_2)))
+         -->β)
+    (--> (Δ (in-hole E (elim D e_motive (e_i ...) (v_m ...) (in-hole Θv_c c))))
+         (Δ (in-hole E (in-hole Θ_mi v_mi)))
+         ;; Find the method for constructor c_i, relying on the order of the arguments.
+         (where natural (Δ-constructor-index Δ D c))
+         (where v_mi ,(list-ref (term (v_m ...)) (term natural)))
+         ;; Generate the inductive recursion
+         (where Θ_ih (Δ-inductive-elim Δ D (elim D e_motive (e_i ...) (v_m ...) hole) Θv_c))
+         (where Θ_mi (in-hole Θ_ih Θv_c))
+         -->elim)))
+
+(define-metafunction tt-redL
+  step : Δ e -> e
+  [(step Δ e)
+   e_r
+   (where (_ e_r) ,(car (apply-reduction-relation tt--> (term (Δ e)))))])
+
+(define-metafunction tt-redL
+  reduce : Δ e -> e
+  [(reduce Δ e)
+   e_r
+   (where (_ e_r)
+          ,(car (apply-reduction-relation* tt--> (term (Δ e)) #:cache-all? #t)))])
+
+;;; ------------------------------------------------------------------------
+;;; Type checking and synthesis
+
+(define-extended-language tt-typingL tt-redL
+  ;; NB: There may be a bijection between Γ and Ξ. That's interesting.
+  ;; NB: Also a bijection between Γ and a list of maps from x to t.
+  (Γ   ::= ∅ (Γ x : t)))
+(define Γ? (redex-match? tt-typingL Γ))
+
+(define-judgment-form tt-typingL
+  #:mode (convert I I I I)
+  #:contract (convert Δ Γ t t)
+
+  [(side-condition ,(<= (term i_0) (term i_1)))
+   ----------------- "≼-Unv"
+   (convert Δ Γ (Unv i_0) (Unv i_1))]
+
+  [(where t_2 (reduce Δ t_0))
+   (where t_3 (reduce Δ t_1))
+   (side-condition (α-equivalent? t_2 t_3))
+   ----------------- "≼-αβ"
+   (convert Δ Γ t_0 t_1)]
+
+  [(convert Δ (Γ x : t_0) t_1 t_2)
+   ----------------- "≼-Π"
+   (convert Δ Γ (Π (x : t_0) t_1) (Π (x : t_0) t_2))])
+
+(define-metafunction tt-typingL
+  Γ-union : Γ Γ -> Γ
+  [(Γ-union Γ ∅) Γ]
+  [(Γ-union Γ_2 (Γ_1 x : t))
+   ((Γ-union Γ_2 Γ_1) x : t)])
+
+(define-metafunction tt-typingL
+  Γ-set : Γ x t -> Γ
+  [(Γ-set Γ x t) (Γ x : t)])
+
+;; NB: Depends on clause order
+(define-metafunction tt-typingL
+  Γ-ref : Γ x -> t or #f
+  [(Γ-ref ∅ x) #f]
+  [(Γ-ref (Γ x : t) x) t]
+  [(Γ-ref (Γ x_0 : t_0) x_1) (Γ-ref Γ x_1)])
+
+;; NB: Depends on clause order
+(define-metafunction tt-typingL
+  Γ-remove : Γ x -> Γ
+  [(Γ-remove ∅ x) ∅]
+  [(Γ-remove (Γ x : t) x) Γ]
+  [(Γ-remove (Γ x_0 : t_0) x_1) (Γ-remove Γ x_1)])
+
+(define-metafunction tt-typingL
+  nonpositive : x t -> #t or #f
+  [(nonpositive x (in-hole Θ x))
+   #t]
+  [(nonpositive x (Π (x_0 : (in-hole Θ x)) t))
+   #f]
+  [(nonpositive x (Π (x_0 : t_0) t))
+   ,(and (term (positive x t_0)) (term (nonpositive x t)))]
+  [(nonpositive x t) #t])
+
+(define-metafunction tt-typingL
+  positive : x t -> #t or #f
+  [(positive x (in-hole Θ x))
+   #f]
+  [(positive x (Π (x_0 : (in-hole Θ x)) t))
+   (positive x t)]
+  [(positive x (Π (x_0 : t_0) t))
+   ,(and (term (nonpositive x t_0)) (term (positive x t)))]
+  [(positive x t) #t])
+
+(define-metafunction tt-typingL
+  positive* : x (t ...) -> #t or #f
+  [(positive* x_D ()) #t]
+  [(positive* x_D (t_c t_rest ...))
+   ;; Replace the result of the constructor with (Unv 0), to avoid the result being considered a
+   ;; nonpositive position.
+   ,(and (term (positive x_D (in-hole Ξ (Unv 0)))) (term (positive* x_D (t_rest ...))))
+   (where (in-hole Ξ (in-hole Θ x_D)) t_c)])
+
+;; Holds when the signature Δ and typing context Γ are well-formed.
+(define-judgment-form tt-typingL
+  #:mode (wf I I)
+  #:contract (wf Δ Γ)
+
+  [----------------- "WF-Empty"
+   (wf ∅ ∅)]
+
+  [(type-infer Δ Γ t t_0)
+   (wf Δ Γ)
+   ----------------- "WF-Var"
+   (wf Δ (Γ x : t))]
+
+  [(wf Δ ∅)
+   (type-infer Δ ∅ t_D U_D)
+   (type-infer Δ (∅ x_D : t_D) t_c U_c) ...
+   ;; NB: Ugh this should be possible with pattern matching alone ....
+   (side-condition ,(map (curry equal? (term x_D)) (term (x_D* ...))))
+   (side-condition (positive* x_D (t_c ...)))
+   ----------------- "WF-Inductive"
+   (wf (Δ (x_D : t_D
+               ;; Checks that a constructor for x actually produces an x, i.e., that
+               ;; the constructor is well-formed.
+               ((x_c : (name t_c (in-hole Ξ (in-hole Θ x_D*)))) ...))) ∅)])
+
+;; TODO: Bi-directional and inference?
+;; TODO: http://www.cs.ox.ac.uk/ralf.hinze/WG2.8/31/slides/stephanie.pdf
+
+;; Holds when e has type t under signature Δ and typing context Γ
+(define-judgment-form tt-typingL
+  #:mode (type-infer I I I O)
+  #:contract (type-infer Δ Γ e t)
+
+  [(wf Δ Γ)
+   (unv-type U_0 U_1)
+   ----------------- "DTR-Unv"
+   (type-infer Δ Γ U_0 U_1)]
+
+  [(where t (Δ-ref-type Δ x))
+   ----------------- "DTR-Inductive"
+   (type-infer Δ Γ x t)]
+
+  [(where t (Γ-ref Γ x))
+   ----------------- "DTR-Start"
+   (type-infer Δ Γ x t)]
+
+  [(type-infer Δ (Γ x : t_0) e t_1)
+   (type-infer Δ Γ (Π (x : t_0) t_1) U)
+   ----------------- "DTR-Abstraction"
+   (type-infer Δ Γ (λ (x : t_0) e) (Π (x : t_0) t_1))]
+
+  [(type-infer Δ Γ t_0 U_1)
+   (type-infer Δ (Γ x : t_0) t U_2)
+   (unv-pred U_1 U_2 U)
+   ----------------- "DTR-Product"
+   (type-infer Δ Γ (Π (x : t_0) t) U)]
+
+  [(type-infer Δ Γ e_0 t)
+   ;; Cannot rely on type-infer producing normal forms.
+   (where (Π (x_0 : t_0) t_1) (reduce Δ t))
+   (type-check Δ Γ e_1 t_0)
+   (where t_3 (subst t_1 x_0 e_1))
+   ----------------- "DTR-Application"
+   (type-infer Δ Γ (e_0 e_1) t_3)]
+
+  [(type-check Δ Γ e_c (apply D e_i ...))
+
+   (type-infer Δ Γ e_motive (name t_motive (in-hole Ξ U)))
+   (convert Δ Γ t_motive (Δ-motive-type Δ D U))
+
+   (where (t_m ...) (Δ-method-types Δ D e_motive))
+   (type-check Δ Γ e_m t_m) ...
+   ----------------- "DTR-Elim_D"
+   (type-infer Δ Γ (elim D e_motive (e_i ...) (e_m ...) e_c)
+               (apply e_motive e_i ... e_c))])
+
+(define-judgment-form tt-typingL
+  #:mode (type-check I I I I)
+  #:contract (type-check Δ Γ e t)
+
+  [(type-infer Δ Γ e t_0)
+   (convert Δ Γ t t_0)
+   ----------------- "DTR-Check"
+   (type-check Δ Γ e t)])

cur-lib/cur/curnel/redex-lang.rkt

@@ -2,7 +2,7 @@
 ;; This module just provide module language sugar over the redex model.
 
 (require
-  "redex-core.rkt"
+  (except-in "redex-core.rkt" apply)
   redex/reduction-semantics
   racket/provide-syntax
   (for-syntax
@@ -11,7 +11,7 @@
     racket/syntax
     (except-in racket/provide-transform export)
     racket/require-transform
-    (except-in "redex-core.rkt" remove)
+    (except-in "redex-core.rkt" apply)
     redex/reduction-semantics))
 (provide
   ;; Basic syntax
@@ -30,12 +30,10 @@
     [dep-provide provide]
     [dep-require require]
 
-    [dep-lambda lambda]
     [dep-lambda λ]
     [dep-app #%app]
 
-    [dep-forall forall]
-    [dep-forall ∀]
+    [dep-forall Π]
 
     [dep-inductive data]
 
@@ -53,41 +51,42 @@
   define-syntax
   begin-for-syntax
   define-for-syntax
-  (for-syntax (all-from-out syntax/parse))
   syntax-case
   syntax-rules
   define-syntax-rule
-  (for-syntax (all-from-out racket))
-  ;; reflection
   (for-syntax
+   (all-from-out syntax/parse)
+   (all-from-out racket)
+   (all-from-out racket/syntax)
     cur->datum
     cur-expand
-    type-infer/syn
-    type-check/syn?
-    normalize/syn
-    step/syn
+    cur-type-infer
+    cur-type-check?
+    cur-normalize
+    cur-step
     cur-equal?))
 
 (begin-for-syntax
-  ;; TODO: Gamma and Sigma seem to get reset inside a module+
+  ;; TODO: Gamma and Delta seem to get reset inside a module+
   (define gamma
     (make-parameter
       (term ∅)
       (lambda (x)
         (unless (Γ? x)
-          (error 'core-error "We built a bad gamma ~s" x))
+          (error 'core-error "We built a bad term environment ~s" x))
         x)))
 
-  (define sigma
+  (define delta
     (make-parameter
       (term ∅)
       (lambda (x)
-        (unless (Σ? x)
-          (error 'core-error "We built a bad sigma ~s" x))
+        (unless (Δ? x)
+          (error 'core-error "We built a bad inductive declaration ~s" x))
         x)))
 
+  ;; These should be provided by core, so details of envs can be hidden.
   (define (extend-Γ/term env x t)
-    (term (,(env) ,x : ,t)))
+    (term (Γ-set ,(env) ,x ,t)))
 
   (define (extend-Γ/term! env x t) (env (extend-Γ/term env x t)))
 
@@ -96,38 +95,46 @@
 
   (define (extend-Γ/syn! env x t) (env (extend-Γ/syn env x t)))
 
-  (define (extend-Σ/term env x t c*)
-    (term (,(env) (,x : ,t (,@c*)))))
+  (define (extend-Δ/term env x t c*)
+    (term (Δ-set ,(env) ,x ,t (,@c*))))
 
-  (define (extend-Σ/term! env x t c*)
-    (env (extend-Σ/term env x t c*)))
+  (define (extend-Δ/term! env x t c*)
+    (env (extend-Δ/term env x t c*)))
 
-  (define (extend-Σ/syn env x t c*)
-    (extend-Σ/term env (syntax->datum x) (cur->datum t)
+  (define (extend-Δ/syn env x t c*)
+    (extend-Δ/term env (syntax->datum x) (cur->datum t)
                    (for/list ([c (syntax->list c*)])
                      (syntax-case c ()
                        [(c : ct)
                         (parameterize ([gamma (extend-Γ/syn gamma x t)])
                           (term (,(syntax->datum #'c) : ,(cur->datum #'ct))))]))))
 
-  (define (extend-Σ/syn! env x t c*)
-    (env (extend-Σ/syn env x t c*)))
+  (define (extend-Δ/syn! env x t c*)
+    (env (extend-Δ/syn env x t c*)))
 
-  (define bind-subst (make-parameter (list null null)))
+  (define subst? (list/c (listof x?)  (listof e?)))
+  (define bind-subst
+    (make-parameter
+     (list null null)
+     (lambda (x)
+       (unless (subst? x)
+           (error 'core-error "We build a bad subst ~s" x))
+       x)))
 
   (define (add-binding/term! x t)
     (let ([vars (first (bind-subst))]
           [exprs (second (bind-subst))])
       (bind-subst (list (cons x vars) (cons t exprs)))))
 
-  ;; TODO: Still absurdly slow. Probably doing n^2 checks of sigma and
-  ;; gamma. And lookup on sigma, gamma are linear, so probably n^2 lookup time.
+  (define (subst-bindings t)
+    (term (subst-all ,t ,(first (bind-subst)) ,(second (bind-subst)))))
+
   (define (type-infer/term t)
-    (let ([t (judgment-holds (type-infer ,(sigma) ,(gamma) ,t t_0) t_0)])
+    (let ([t (judgment-holds (type-infer ,(delta) ,(gamma) ,(subst-bindings t) t_0) t_0)])
       (and (pair? t) (car t))))
 
   (define (type-check/term? e t)
-    (and (judgment-holds (type-check ,(sigma) ,(gamma) ,e ,t)) #t))
+    (and (judgment-holds (type-check ,(delta) ,(gamma) ,(subst-bindings e) ,(subst-bindings t))) #t))
 
   ;; TODO: Blanket disarming is probably a bad idea.
   (define orig-insp (variable-reference->module-declaration-inspector (#%variable-reference)))
@@ -143,14 +150,14 @@
 
   ;; Only type-check at the top-level, to prevent exponential
   ;; type-checking. Redex is expensive enough.
-  ;; TODO: This results in less good error messages. Add an
-  ;; algorithm to find the smallest ill-typed term.
   (define inner-expand? (make-parameter #f))
 
   ;; Reifiy cur syntax into curnel datum
   (define (cur->datum syn)
     ;; Main loop; avoid type
     (define reified-term
+      ;; TODO: This results in less good error messages. Add an
+      ;; algorithm to find the smallest ill-typed term.
       (parameterize ([inner-expand? #t])
         (let cur->datum ([syn syn])
           (syntax-parse (core-expand syn)
@@ -158,7 +165,7 @@
             #:datum-literals (elim Π λ : Unv)
             [x:id (syntax->datum #'x)]
             [(subst-all e _ _) (syntax->datum #'e)]
-            [(reduce Σ e) (cur->datum #'e)]
+            [(reduce Δ e) (cur->datum #'e)]
             [(term e) (cur->datum #'e)]
             [(Unv i) (term (Unv ,(syntax->datum #'i)))]
             ;; TODO: should really check that b is one of the binders
@@ -170,80 +177,77 @@
                     [e (parameterize ([gamma (extend-Γ/term gamma x t)])
                          (cur->datum #'e))])
                (term (,(syntax->datum #'b) (,x : ,t) ,e)))]
-            [(elim t1 t2)
-             (let* ([t1 (cur->datum #'t1)]
-                    [t2 (cur->datum #'t2)])
-               (term (elim ,t1 ,t2)))]
+            [(elim D motive (i ...) (m ...) d)
+             (term (elim ,(cur->datum #'D) ,(cur->datum #'motive)
+                         ,(map cur->datum (syntax->list #'(i ...)))
+                         ,(map cur->datum (syntax->list #'(m ...)))
+                         ,(cur->datum #'d)))]
             [(#%app e1 e2)
              (term (,(cur->datum #'e1) ,(cur->datum #'e2)))]))))
-    (unless (and inner-expand? (type-infer/term reified-term))
-      ;; TODO: is this really a syntax error?
-      (raise-syntax-error 'cur "term is ill-typed:"
-                          (begin (printf "Sigma: ~s~nGamma: ~s~n" (sigma) (gamma))
-                                 reified-term)
-                          syn))
+    (unless (or (inner-expand?) (type-infer/term reified-term))
+      #;(printf "Delta: ~s~nGamma: ~s~n" (delta) (gamma))
+      (raise-syntax-error 'cur "term is ill-typed:" reified-term syn))
     reified-term)
 
   (define (datum->cur syn t)
-    (match t
-      [(list (quote term) e)
-       (quasisyntax/loc
-         syn
-         (datum->cur syn e))]
-      [(list (quote Unv) i)
-       (quasisyntax/loc
-         syn
-         (Type #,i))]
-      [(list (quote Π) (list x (quote :) t) body)
-       (quasisyntax/loc
-         syn
-         (dep-forall (#,(datum->syntax syn x) : #,(datum->cur syn t)) #,(datum->cur syn body)))]
-      [(list (quote λ) (list x (quote :) t) body)
-       (quasisyntax/loc
-         syn
-         (dep-lambda (#,(datum->syntax syn x) : #,(datum->cur syn t)) #,(datum->cur syn body)))]
-      [(list (list (quote elim) t1) t2)
-       (quasisyntax/loc
-         syn
-         (dep-elim #,(datum->cur syn t1) #,(datum->cur syn t2)))]
-      [(list e1 e2)
-       (quasisyntax/loc
-         syn
-         (dep-app #,(datum->cur syn e1) #,(datum->cur syn e2)))]
-      [_
-       (quasisyntax/loc
-         syn
-         #,(datum->syntax syn t))]))
+    (let datum->cur ([t t])
+      (match t
+        [(list (quote term) e)
+         (quasisyntax/loc syn
+           (datum->cur e))]
+        [(list (quote Unv) i)
+         (quasisyntax/loc syn
+           (Type #,i))]
+        [(list (quote Π) (list x (quote :) t) body)
+         (quasisyntax/loc syn
+           (dep-forall (#,(datum->syntax syn x) : #,(datum->cur t)) #,(datum->cur body)))]
+        [(list (quote λ) (list x (quote :) t) body)
+         (quasisyntax/loc syn
+           (dep-lambda (#,(datum->syntax syn x) : #,(datum->cur t)) #,(datum->cur body)))]
+        [(list (list (quote elim) t1) t2)
+         (quasisyntax/loc syn
+           (dep-elim #,(datum->cur t1) #,(datum->cur t2)))]
+        [(list e1 e2)
+         (quasisyntax/loc syn
+           (dep-app #,(datum->cur e1) #,(datum->cur e2)))]
+        [_
+         (quasisyntax/loc syn
+           #,(datum->syntax syn t))])))
 
   (define (eval-cur syn)
-    (term (reduce ,(sigma) (subst-all ,(cur->datum syn) ,(first (bind-subst)) ,(second (bind-subst))))))
+    (term (reduce ,(delta) ,(subst-bindings (cur->datum syn)))))
 
   (define (syntax->curnel-syntax syn)
     (quasisyntax/loc
       syn
-      (term (reduce #,(sigma) (subst-all #,(cur->datum syn) #,(first (bind-subst)) #,(second (bind-subst)))))))
+      ;; TODO: this subst-all should be #,(subst-bindings (cur->datum syn)), but doesn't work
+      (term (reduce #,(delta) (subst-all #,(cur->datum syn) #,(first (bind-subst)) #,(second (bind-subst)))))))
 
   ;; Reflection tools
 
-  (define (normalize/syn syn)
+  (define (cur-normalize syn)
     (datum->cur
       syn
       (eval-cur syn)))
 
-  (define (step/syn syn)
+  (define (cur-step syn)
     (datum->cur
       syn
-      (term (step ,(sigma) (subst-all ,(cur->datum syn) ,(first (bind-subst)) ,(second (bind-subst)))))))
+      (term (step ,(delta) ,(subst-bindings (cur->datum syn))))))
 
   ;; Are these two terms equivalent in type-systems internal equational reasoning?
   (define (cur-equal? e1 e2)
-    (and (judgment-holds (equivalent ,(sigma) ,(eval-cur e1) ,(eval-cur e2)) #t)))
+    (and (judgment-holds (convert ,(delta) ,(gamma) ,(eval-cur e1) ,(eval-cur e2))) #t))
 
-  (define (type-infer/syn syn)
-    (let ([t (type-infer/term (eval-cur syn))])
-      (and t (datum->cur syn t))))
+  ;; TODO: Document local-env
+  (define (cur-type-infer syn #:local-env [env '()])
+    (parameterize ([gamma (for/fold ([gamma (gamma)])
+                                    ([(x t) (in-dict env)])
+                            (extend-Γ/syn (thunk gamma) x t))])
+      (let ([t (type-infer/term (eval-cur syn))])
+        (and t (datum->cur syn t)))))
 
-  (define (type-check/syn? syn type)
+  (define (cur-type-check? syn type)
     (type-check/term? (eval-cur syn) (eval-cur type)))
 
   ;; Takes a Cur term syn and an arbitrary number of identifiers ls. The cur term is
@@ -269,8 +273,8 @@
   (define (cur-identifier-bound? id)
     (let ([x (syntax->datum id)])
       (and (x? x)
-        (or (term (lookup-Γ ,(gamma) ,x))
-          (term (lookup-Σ ,(sigma) ,x))))))
+        (or (term (Γ-ref ,(gamma) ,x))
+          (term (Δ-ref-type ,(delta) ,x))))))
 
   (define (filter-cur-exports syn modes)
     (partition (compose cur-identifier-bound? export-local-id)
@@ -286,18 +290,18 @@
            (set! envs (for/list ([e cur])
            (let* ([x (syntax->datum (export-local-id e))]
                   [t (type-infer/term x)]
-                  [env (if (term (lookup ,(gamma) ,x)) #'gamma #'sigma)])
+                  [env (if (term (lookup ,(gamma) ,x)) #'gamma #'delta)])
              #`(extend-env/term! #,env #,(export-out-sym e) #,t))))
            |#
         ~cur)]))))
 
 (define-syntax (export-envs syn)
   (syntax-case syn ()
-    [(_ gamma-out sigma-out bind-out)
+    [(_ gamma-out delta-out bind-out)
      (begin
        #`(begin-for-syntax
           (define gamma-out (term #,(gamma)))
-          (define sigma-out (term #,(sigma)))
+          (define delta-out (term #,(delta)))
           (define bind-out '#,(bind-subst))))]))
 
 ;; TODO: This can only handle a single provide form, otherwise generates multiple *-out
@@ -309,14 +313,14 @@
         | Ignoring the built envs above, for now.  The local-lift export seems to get executed before
         | the filtered environment is built.
         |#
-       ;; TODO: rename out will need to rename variables in gamma and ; sigma.
+       ;; TODO: rename out will need to rename variables in gamma and ; delta.
        (syntax-local-lift-module-end-declaration
-         #`(export-envs gamma-out sigma-out bind-out))
+         #`(export-envs gamma-out delta-out bind-out))
        #`(provide (extend-env-and-provide e ...)
-                  (for-syntax gamma-out sigma-out bind-out)))]))
+                  (for-syntax gamma-out delta-out bind-out)))]))
 (begin-for-syntax
   (define out-gammas #`())
-  (define out-sigmas #`())
+  (define out-deltas #`())
   (define out-binds #`())
   (define gn 0)
   (define sn 0)
@@ -336,21 +340,21 @@
                        ;; TODO: Do not DIY gensym
                        (set! gn (add1 gn))
                        (set! out-gammas
-                             #`(#,@out-gammas (gamma (term (append-Γ
+                             #`(#,@out-gammas (gamma (term (Γ-union
                                                              ,(gamma)
                                                              ,#,new-id)))))
                        (cons (struct-copy import imp [local-id new-id])
                              imports))]
                     ;; TODO: Many shared code between these two clauses
-                    [(equal? (import-src-sym imp) 'sigma-out)
+                    [(equal? (import-src-sym imp) 'delta-out)
                      (let ([new-id (format-id (import-orig-stx imp)
-                                              "sigma-out~a" sn)])
+                                              "delta-out~a" sn)])
                        ;; TODO: Fewer set!s
                        ;; TODO: Do not DIY gensym
                        (set! sn (add1 sn))
-                       (set! out-sigmas
-                             #`(#,@out-sigmas (sigma (term (append-Σ
-                                                             ,(sigma)
+                       (set! out-deltas
+                             #`(#,@out-deltas (delta (term (Δ-union
+                                                             ,(delta)
                                                              ,#,new-id)))))
                        (cons (struct-copy import imp [local-id new-id])
                              imports))]
@@ -379,11 +383,10 @@
       (syntax-case syn ()
         [(_ e ...) (filter-cur-imports #'(e ...))]))))
 
-;; TODO: rename in will need to rename variables in gamma and
-;; sigma.
+;; TODO: rename in will need to rename variables in gamma and delta.
 (define-syntax (import-envs syn)
   (syntax-case syn ()
-    [(_) #`(begin-for-syntax #,@out-gammas #,@out-sigmas
+    [(_) #`(begin-for-syntax #,@out-gammas #,@out-deltas
                              #,@out-binds)]))
 
 (define-syntax (dep-require syn)
@@ -399,7 +402,7 @@
      #`(module+ name
          (begin-for-syntax
            (gamma (term #,(gamma)))
-           (sigma (term #,(sigma)))
+           (delta (term #,(delta)))
            (bind-subst '#,(bind-subst)))
          body ...)]))
 
@@ -408,43 +411,45 @@
 ;;
 ;; TODO: Can these be simplified further?
 (define-syntax (dep-lambda syn)
-  (syntax-case syn (:)
-    [(_ (x : t) e)
+  (syntax-parse syn
+    #:datum-literals (:)
+    [(_ (x:id : t) e)
      (syntax->curnel-syntax
        (quasisyntax/loc syn (λ (x : t) e)))]))
 
 (define-syntax (dep-app syn)
-  (syntax-case syn ()
-    [(_ e1 e2)
+  (syntax-parse syn
+    [(_ e1:expr e2:expr)
      (syntax->curnel-syntax
        (quasisyntax/loc syn (#%app e1 e2)))]))
 
 (define-syntax (dep-forall syn)
-  (syntax-case syn (:)
-    [(_ (x : t) e)
+  (syntax-parse syn
+    #:datum-literals (:)
+    [(_ (x:id : t) e)
      (syntax->curnel-syntax
        (quasisyntax/loc syn (Π (x : t) e)))]))
 
 (define-syntax (Type syn)
-  (syntax-case syn ()
-    [(_ i)
+  (syntax-parse syn
+    [(_ i:nat)
      (syntax->curnel-syntax
        (quasisyntax/loc syn (Unv i)))]
     [_ (quasisyntax/loc syn (Type 0))]))
 
 (define-syntax (dep-inductive syn)
-  (syntax-case syn (:)
-    [(_ i : ti (x1 : t1) ...)
-     ;; TODO: Probably should occur only in definition context? and also, should not really produce void
+  (syntax-parse syn
+    #:datum-literals (:)
+    [(_ i:id : ti (x1:id : t1) ...)
      (begin
-       (extend-Σ/syn! sigma #'i #'ti #'((x1 : t1) ...))
+       (extend-Δ/syn! delta #'i #'ti #'((x1 : t1) ...))
        #'(void))]))
 
 (define-syntax (dep-elim syn)
-  (syntax-case syn ()
-    [(_ D T)
+  (syntax-parse syn
+    [(_ D:id motive (i ...) (m ...) e)
      (syntax->curnel-syntax
-       (quasisyntax/loc syn (elim D T)))]))
+       (quasisyntax/loc syn (elim D motive (i ...) (m ...) e)))]))
 
 (define-syntax-rule (dep-void) (void))
 
@@ -462,20 +467,14 @@
   (syntax-case syn ()
     [(_ . form)
      (begin
-       ;; TODO NB FIXME: HACKS HACKS HACKS
+       ;; TODO NB FIXME: HACKS
        #`(begin
-           (export-envs gamma-out sigma-out bind-out)
+           (export-envs gamma-out delta-out bind-out)
            (begin-for-syntax
-             ;; Try to detect when we are in DrRacket, and do the right thing.
-             (when (equal? 'debug-error-display-handler (object-name (error-display-handler)))
-                 (cond
-                   [(null? (namespace-mapped-symbols))
-                    (displayln "You will need to add a (provide ...) in the definitions area for the evaluator to load Cur definitions correctly.")]
-                   [(eq? 3 (length (namespace-mapped-symbols)))
-                    (bind-subst (namespace-variable-value (first (namespace-mapped-symbols))))
-                    (gamma (namespace-variable-value (second (namespace-mapped-symbols))))
-                    (sigma (namespace-variable-value (third (namespace-mapped-symbols))))]
-                   [else (void)])))
+             (define nm (map (lambda (x) (namespace-variable-value x #f (lambda x #t))) (namespace-mapped-symbols)))
+             (bind-subst (first (memf subst? nm)))
+             (gamma (first (memf Γ? nm)))
+             (delta (first (memf Δ? nm))))
           form))]))
 
 (define-syntax (dep-define syn)
@@ -483,6 +482,8 @@
     [(_ id:id e)
      (let ([e (cur->datum #'e)]
            [id (syntax->datum #'id)])
+       ;; NB: Have to roll our own namespace rather than use built-in define so id is resolved at
+       ;; compile time in redex, and at runtime in racket.
        (extend-Γ/term! gamma id (type-infer/term e))
        (add-binding/term! id e)
        #'(void))]))

cur-lib/cur/lang/reader.rkt

@@ -1,2 +1,2 @@
 #lang s-exp syntax/module-reader
-cur/cur
+cur

cur-lib/cur/olly.rkt

@@ -0,0 +1,449 @@
+#lang s-exp "main.rkt"
+;; Olly: The OTT-Like LibrarY
+;; TODO: Automagically create a parser from bnf grammar
+(require
+  "stdlib/sugar.rkt"
+  "stdlib/nat.rkt"
+  ;; TODO: "real-"? More like "curnel-"
+  (only-in
+   "main.rkt"
+   [#%app real-app]
+   [elim real-elim]
+   [Π real-forall]
+   [λ real-lambda]))
+
+(provide
+  define-relation
+  define-language
+  generate-coq
+
+  ;; private; exported for testing only
+  (for-syntax
+   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)))
+
+  (define (constructor-args syn)
+    (syntax-parse (cur-type-infer 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 (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:id motive (i ...) (m ...) d)
+             (format
+              "(~a_rect ~a~a~a ~a)"
+              (cur->coq #'var)
+              (cur->coq #'motive)
+              (for/fold ([strs ""])
+                        ([m (syntax->list #'(m ...))])
+                (format "~a ~a" strs (cur->coq m)))
+              (for/fold ([strs ""])
+                        ([i (syntax->list #'(i ...))])
+                (format "~a ~a" strs (cur->coq i)))
+              (cur->coq #'d))]
+            [(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))])
+       (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

cur-lib/cur/stdlib/bool.rkt

@@ -0,0 +1,24 @@
+#lang s-exp "../main.rkt"
+(require "sugar.rkt")
+(provide Bool true false if not and or)
+
+(data Bool : Type
+  (true : Bool)
+  (false : Bool))
+
+(define-syntax-rule (if t s f)
+  (match t
+    [true s]
+    [false f]))
+
+(define (not (x : Bool)) (if x false true))
+
+(define (and (x : Bool) (y : Bool))
+  (if x
+      y
+      (not y)))
+
+(define (or (x : Bool) (y : Bool))
+  (if x
+      true
+      y))

cur-lib/cur/stdlib/list.rkt

@@ -0,0 +1,33 @@
+#lang s-exp "../main.rkt"
+(require
+ "nat.rkt"
+ "maybe.rkt"
+ "sugar.rkt")
+
+(provide
+ List
+ nil
+ cons
+ list-ref
+ length)
+
+(data List : (-> (A : Type) Type)
+  (nil : (-> (A : Type) (List A)))
+  (cons : (-> (A : Type) A (List A) (List A))))
+
+(define (list-ref (A : Type) (ls : (List A)))
+  (match ls
+    [(nil (A : Type)) (lambda (n : Nat) (none A))]
+    [(cons (A : Type) (a : A) (rest : (List A)))
+     (lambda (n : Nat)
+       (match n
+         [z (some A a)]
+         [(s (n-1 : Nat))
+          ((recur rest) n-1)]))]))
+
+(define (length (A : Type) (ls : (List A)))
+  (match ls
+    [(nil (A : Type))
+     z]
+    [(cons (A : Type) (a : A) (rest : (List A)))
+     (s (recur rest))]))

cur-lib/cur/stdlib/maybe.rkt

@@ -0,0 +1,13 @@
+#lang s-exp "../main.rkt"
+(require "sugar.rkt")
+(provide Maybe none some some/i)
+
+(data Maybe : (forall (A : Type) Type)
+  (none : (forall (A : Type) (Maybe A)))
+  (some : (forall (A : Type) (a : A) (Maybe A))))
+
+(define-syntax (some/i syn)
+  (syntax-case syn ()
+   [(_ a)
+    (let ([a-ty (cur-type-infer #'a)])
+      #`(some #,a-ty a))]))

cur-lib/cur/stdlib/nat.rkt

@@ -0,0 +1,61 @@
+#lang s-exp "../main.rkt"
+(require "sugar.rkt" "bool.rkt")
+;; TODO: override (all-defined-out) to enable exporting all these
+;; properly.
+(provide Nat z s add1 sub1 plus mult exp square nat-equal? even? odd?)
+
+(data Nat : Type
+  (z : Nat)
+  (s : (-> Nat Nat)))
+
+(define (add1 (n : Nat)) (s n))
+
+(define (sub1 (n : Nat))
+  (match n
+    [z z]
+    [(s (x : Nat)) x]))
+
+(define (plus (n1 : Nat) (n2 : Nat))
+  (match n1
+    [z n2]
+    [(s (x : Nat))
+     (s (recur x))]))
+
+(define (mult (m : Nat) (n : Nat))
+  (match m
+    [z z]
+    [(s (x : Nat))
+     (plus n (recur x))]))
+
+(define (exp (m : Nat) (e : Nat))
+  (match m
+    [z (s z)]
+    [(s (x : Nat))
+     (mult e (recur x))]))
+
+(define square (run (exp (s (s z)))))
+
+(define (zero? (n : Nat))
+  (match n
+    [z true]
+    [(s (n : Nat))
+     false]))
+
+(define (nat-equal? (n : Nat))
+  (match n
+    [z zero?]
+    [(s (n-1 : Nat))
+     (lambda (m : Nat)
+       (match m
+         [z false]
+         [(s (m-1 : Nat))
+          ((recur n-1) m-1)]))]))
+
+(define (even? (n : Nat))
+  (match n
+    [z true]
+    [(s (n : Nat))
+     (not (recur n))]))
+
+(define (odd? (n : Nat))
+  (not (even? n)))

cur-lib/cur/stdlib/prop.rkt

@@ -0,0 +1,85 @@
+#lang s-exp "../main.rkt"
+(require "sugar.rkt")
+;; TODO: Handle multiple provide forms properly
+;; TODO: Handle (all-defined-out) properly
+(provide
+  True T
+  thm:anything-implies-true
+  pf:anything-implies-true
+  False
+  Not
+  And
+  conj conj/i
+  thm:and-is-symmetric pf:and-is-symmetric
+  thm:proj1 pf:proj1
+  thm:proj2 pf:proj2
+  == refl)
+
+(data True : Type (T : True))
+
+(define thm:anything-implies-true (forall (P : Type) True))
+(define pf:anything-implies-true (lambda (P : Type) T))
+
+(data False : Type)
+
+(define-type (Not (A : Type)) (-> A False))
+
+(data And : (forall (A : Type) (B : Type) Type)
+  (conj : (forall (A : Type) (B : Type)
+            (x : A) (y : B) (And A B))))
+
+(define-syntax (conj/i syn)
+  (syntax-case syn ()
+    [(_ a b)
+     (let ([a-type (cur-type-infer #'a)]
+           [b-type (cur-type-infer #'b)])
+       #`(conj #,a-type #,b-type a b))]))
+
+(define thm:and-is-symmetric
+  (forall (P : Type) (Q : Type) (ab : (And P Q)) (And Q P)))
+
+(define pf:and-is-symmetric
+  (lambda (P : Type) (Q : Type) (ab : (And P Q))
+          (match ab
+            [(conj (P : Type) (Q : Type) (x : P) (y : Q))
+             (conj/i y x)])))
+
+(define thm:proj1
+  (forall (A : Type) (B : Type) (c : (And A B)) A))
+
+(define pf:proj1
+  (lambda (A : Type) (B : Type) (c : (And A B))
+          (match c
+            [(conj (A : Type) (B : Type) (a : A) (b : B)) a])))
+
+(define thm:proj2
+  (forall (A : Type) (B : Type) (c : (And A B)) B))
+
+(define pf:proj2
+  (lambda (A : Type) (B : Type) (c : (And A B))
+          (match c
+            [(conj (A : Type) (B : Type) (a : A) (b : B)) b])))
+
+#| TODO: Disabled until #22 fixed
+(data Or : (forall (A : Type) (B : Type) Type)
+  (left : (forall (A : Type) (B : Type) (a : A) (Or A B)))
+  (right : (forall (A : Type) (B : Type) (b : B) (Or A B))))
+
+(define-theorem thm:A-or-A
+  (forall (A : Type) (o : (Or A A)) A))
+
+(define proof:A-or-A
+  (lambda (A : Type) (c : (Or A A))
+    ;; TODO: What should the motive be?
+    (elim Or (lambda (A : Type) (B : Type) (c : (Or A B)) A)
+          (A A)
+          ((lambda (A : Type) (B : Type) (a : A) a)
+           ;; TODO: How do we know B is A?
+           (lambda (A : Type) (B : Type) (b : B) b))
+          c)))
+
+(qed thm:A-or-A proof:A-or-A)
+|#
+
+(data == : (forall (A : Type) (x : A) (-> A Type))
+  (refl : (forall (A : Type) (x : A) (== A x x))))

cur-lib/cur/stdlib/sugar.rkt

@@ -0,0 +1,498 @@
+#lang s-exp "../main.rkt"
+(provide
+  ->
+  lambda
+  (rename-out
+    [-> →]
+    [-> forall]
+    [-> ∀]
+    [-> Π]
+    [-> Pi]
+    [lambda λ])
+  #%app
+  define
+  :
+  define-type
+  match
+  recur
+  let
+
+  ;; type-check
+  ::
+
+  ;; reflection in syntax
+  run
+  step
+  step-n
+  query-type)
+
+(require
+  (only-in "../main.rkt"
+    [#%app real-app]
+    [λ real-lambda]
+    [Π real-Π]
+    [define real-define]))
+
+(begin-for-syntax
+  (define-syntax-class result-type
+    (pattern type:expr))
+
+  (define-syntax-class parameter-declaration
+    (pattern (name:id (~datum :) type:expr))
+
+    (pattern
+     type:expr
+     #:attr name (format-id #'type "~a" (gensym 'anon-parameter)))))
+
+;; A multi-arity function type; takes parameter declaration of either
+;; a binding (name : type), or type whose name is generated.
+;; E.g.
+;; (-> (A : Type) A A)
+(define-syntax (-> syn)
+  (syntax-parse syn
+    [(_ d:parameter-declaration ...+ result:result-type)
+     (foldr (lambda (src name type r)
+              (quasisyntax/loc src
+                (real-Π (#,name : #,type) #,r)))
+            #'result
+            (attribute d)
+            (attribute d.name)
+            (attribute d.type))]))
+
+;; TODO: Add forall macro that allows specifying *names*, with types
+;; inferred. unlike -> which require types but not names
+;; E.g.
+;; (forall x (y : Nat) (== Nat x y))
+
+;; TODO: Allows argument-declarations to have types inferred, similar
+;; to above TODO forall
+(begin-for-syntax
+  ;; eta-expand syntax-class for error messages
+  (define-syntax-class argument-declaration
+    (pattern
+     e:parameter-declaration
+     #:attr name #'e.name
+     #:attr type #'e.type)))
+(define-syntax (lambda syn)
+  (syntax-parse syn
+    [(_ d:argument-declaration ...+ body:expr)
+     (foldr (lambda (src name type r)
+              (quasisyntax/loc src
+                (real-lambda (#,name : #,type) #,r)))
+            #'body
+            (attribute d)
+            (attribute d.name)
+            (attribute d.type))]))
+
+;; TODO: This makes for really bad error messages when an identifier is undefined.
+(define-syntax (#%app syn)
+  (syntax-case syn ()
+    [(_ e)
+     (quasisyntax/loc syn e)]
+    [(_ e1 e2)
+     (quasisyntax/loc syn
+       (real-app e1 e2))]
+    [(_ e1 e2 e3 ...)
+     (quasisyntax/loc syn
+       (#%app (#%app e1 e2) e3 ...))]))
+
+(define-syntax define-type
+  (syntax-rules ()
+    [(_ (name (a : t) ...) body)
+     (define name (-> (a : t) ... body))]
+    [(_ name type)
+     (define name type)]))
+
+;; Cooperates with define to allow Haskell-esque type annotations
+#| TODO NB:
+ | This method of cooperating macros is sort of a terrible
+ | hack. Instead, need principled way of adding/retrieving information
+ | to/from current module. E.g. perhaps provide extensions an interface to
+ | module's term environment and inductive signature. Then, :: could add
+ | new "id : type" to environment, and define could extract type and use.
+ |#
+(begin-for-syntax
+  (define annotation-dict (make-hash))
+  (define (annotation->types type-syn)
+    (let loop ([ls '()]
+               [syn type-syn])
+      (syntax-parse (cur-expand syn)
+        #:datum-literals (:)
+        [(real-Π (x:id : type) body)
+         (loop (cons #'type ls) #'body)]
+        [_ (reverse ls)]))))
+
+(define-syntax (: syn)
+  (syntax-parse syn
+    [(_ name:id type:expr)
+     ;; NB: Unhygenic; need to reuse Racket's identifiers, and make this type annotation a syntax property
+     (syntax-parse (cur-expand #'type)
+      #:datum-literals (:)
+      [(real-Π (x:id : type) body) (void)]
+      [_
+       (raise-syntax-error
+        ':
+        "Can only declare annotations for functions, but not a function type"
+        syn)])
+     (dict-set! annotation-dict (syntax->datum #'name) (annotation->types #'type))
+     #'(void)]))
+
+;; TODO: Allow inferring types as in above TODOs for lambda, forall
+(define-syntax (define syn)
+  (syntax-parse syn
+    #:datum-literals (:)
+    [(define (name:id x:id ...) body)
+     (cond
+       [(dict-ref annotation-dict (syntax->datum #'name)) =>
+        (lambda (anns)
+          (quasisyntax/loc syn
+            (real-define name (lambda #,@(for/list ([x (syntax->list #'(x ...))]
+                                                    [type anns])
+                                           #`(#,x : #,type)) body))))]
+       [else
+        (raise-syntax-error
+         'define
+         "Cannot omit type annotations unless you have declared them with (: name type) form first."
+         syn)])]
+    [(define (name (x : t) ...) body)
+     (quasisyntax/loc syn
+       (real-define name (lambda (x : t) ... body)))]
+    [(define id body)
+     (quasisyntax/loc syn
+       (real-define id body))]))
+
+#|
+(begin-for-syntax
+  (define (type->telescope syn)
+    (syntax-parse (cur-expand syn)
+      #:literals (real-Π)
+      #:datum-literals (:)
+      [(real-Π (x:id : t) body)
+       (cons #'(x : t) (type->telescope #'body))]
+      [_ '()]))
+
+  (define (type->body syn)
+    (syntax-parse syn
+      #:literals (real-Π)
+      #:datum-literals (:)
+      [(real-Π (x:id : t) body)
+       (type->body #'body)]
+      [e #'e]))
+
+  (define (constructor-indices D syn)
+    (let loop ([syn syn]
+               [args '()])
+      (syntax-parse (cur-expand syn)
+        #:literals (real-app)
+        [D:id args]
+        [(real-app e1 e2)
+         (loop #'e1 (cons #'e2 args))])))
+
+  (define (inductive-index-telescope D)
+    (type->telescope (cur-type-infer D)))
+
+  (define (inductive-method-telescope D motive)
+    (for/list ([syn (cur-constructor-map D)])
+      (with-syntax ([(c : t) syn]
+                    [name (gensym (format-symbol "~a-~a" #'c 'method))]
+                    [((arg : arg-type) ...) (type->telescope #'t)]
+                    [((rarg : rarg-type) ...) (constructor-recursive-args D #'((arg : arg-type) ...))]
+                    [((ih : ih-type) ...) (constructor-inductive-hypotheses #'((rarg : rarg-type) ...) motive)]
+                    [(iarg ...) (constructor-indices D (type->body #'t))]
+                    )
+        #`(name : (forall (arg : arg-type) ...
+                          (ih : ih-type) ...
+                          (motive iarg ...)))))))
+
+(define-syntax (elim syn)
+  (syntax-parse syn
+    [(elim D:id U e ...)
+     (with-syntax ([((x : t) ...) (inductive-index-telescope #'D)]
+                   [motive (gensym 'motive)]
+                   [y (gensym 'y)]
+                   [disc (gensym 'disc)]
+                   [((method : method-type) ...) (inductive-method-telescope #'D #'motive)])
+       #`((lambda
+            (motive : (forall (x : t) ... (y : (D x ...)) U))
+            (method : ) ...
+            (x : t) ...
+            (disc : (D x ...)) ...
+            (real-elim D motive (x ...) (method ...) disc))
+          e ...)
+       )
+     ]))
+|#
+
+;; Quite fragie to give a syntactic treatment of pattern matching -> eliminator. Replace with "Elimination with a Motive"
+(begin-for-syntax
+  (define ih-dict (make-hash))
+
+  (define-syntax-class curried-application
+    (pattern
+     ((~literal real-app) name:id e:expr)
+     #:attr args
+     (list #'e))
+
+    (pattern
+     ((~literal real-app) a:curried-application e:expr)
+     #:attr name #'a.name
+     #:attr args
+     ;; TODO BUG: repeated appends are not performant; cons then reverse in inductive-type-declaration
+     (append
+      (attribute a.args)
+      (list #'e))))
+
+  (define-syntax-class inductive-type-declaration
+    (pattern
+     x:id
+     #:attr inductive-name
+     #'x
+     #:attr indices
+     '()
+     #:attr decls
+     (list #`(#,(gensym 'anon-discriminant) : x))
+     #:attr abstract-indices
+     values)
+
+    (pattern
+     ;; BUG TODO NB: Because the inductive type may have been inferred, it may appear in Curnel syntax, i.e., nested applications starting with dep-app
+     ;; Best to ensure it *always* is in Curnel form, and pattern match on that.
+     a:curried-application
+     #:attr inductive-name
+     (attribute a.name)
+     #:attr indices
+     (attribute a.args)
+     #:attr names
+     (for/list ([e (attribute indices)])
+       (format-id e "~a" (gensym 'anon-index)))
+     #:attr types
+     ;; TODO: Detect failure, report error/suggestions
+     (for/list ([e (attribute indices)])
+       (or (cur-type-infer e)
+           (raise-syntax-error
+            'match
+            (format
+             "Could not infer type of index ~a"
+             e)
+            e)))
+     #:attr decls
+     (append
+      (for/list ([name (attribute names)]
+                 [type (attribute types)]
+                 [src (attribute indices)])
+        (quasisyntax/loc src
+          (#,name : #,type)))
+      (list
+       (quasisyntax/loc #'a
+         (#,(gensym 'anon-discriminant) : (inductive-name #,@(attribute names))))))
+     #:attr abstract-indices
+     (lambda (return)
+       ;; NB: unhygenic
+       ;; Normalize at compile-time, for efficiency at run-time
+       (cur-normalize
+        #`((lambda
+              ;; TODO: utteraly fragile; relines on the indices being referred to by name, not computed
+              ;; works only for simple type familes and simply matches on them
+             #,@(for/list ([name (attribute indices)]
+                           [type (attribute types)])
+                 #`(#,name : #,type))
+            #,return)
+          #,@(attribute names))))))
+
+  ;; todo: Support just names, inferring types
+  (define-syntax-class match-declaration
+    (pattern
+     ;; TODO: Use parameter-declaration defined earlier
+     (name:id (~datum :) type:expr)
+     #:attr decl
+     #'(name : type)))
+
+  (define-syntax-class match-prepattern
+    ;; TODO: Check that x is a valid constructor for the inductive type
+    (pattern
+     x:id
+     #:attr local-env
+     '()
+     #:attr decls
+     '()
+     #:attr types
+     '()
+     #:attr names
+     '())
+
+    (pattern
+     (x:id d:match-declaration ...+)
+     #:attr local-env
+     (for/fold ([d (make-immutable-hash)])
+               ([name (attribute d.name)]
+                [type (attribute d.type)])
+       (dict-set d name type))
+     #:attr decls
+     (attribute d.decl)
+     #:attr names
+     (attribute d.name)
+     #:attr types
+     (attribute d.type)))
+
+  (define-syntax-class (match-pattern D motive)
+    (pattern
+     d:match-prepattern
+     #:attr decls
+     ;; Infer the inductive hypotheses, add them to the pattern decls
+     ;; and update the dictionarty for the recur form
+     (for/fold ([decls (attribute d.decls)])
+               ([type-syn (attribute d.types)]
+                [name-syn (attribute d.names)]
+                [src (attribute d.decls)]
+                ;; NB: Non-hygenic
+                ;; BUG TODO: This fails when D is an inductive applied to arguments...
+                #:when (cur-equal? type-syn D))
+       (define/syntax-parse type:inductive-type-declaration (cur-expand type-syn))
+       (let ([ih-name (quasisyntax/loc src #,(format-id name-syn "ih-~a" name-syn))]
+             ;; Normalize at compile-time, for efficiency at run-time
+             [ih-type (cur-normalize #`(#,motive #,@(attribute type.indices) #,name-syn))])
+         (dict-set! ih-dict (syntax->datum name-syn) ih-name)
+         (append decls (list #`(#,ih-name : #,ih-type)))))))
+
+  (define-syntax-class (match-preclause maybe-return-type)
+    (pattern
+     (p:match-prepattern b:expr)
+     #:attr return-type
+     ;; TODO: Check that the infered type matches maybe-return-type, if it is provied
+     (or maybe-return-type
+         ;; Ignore errors when trying to infer this type; other attempt might succeed
+         (with-handlers ([values (lambda _ #f)])
+           (cur-type-infer #:local-env (attribute p.local-env) #'b)))))
+
+  (define-syntax-class (match-clause D motive)
+    (pattern
+     ((~var p (match-pattern D motive))
+      ;; TODO: nothing more advanced?
+      b:expr)
+     #:attr method
+     (quasisyntax/loc #'p
+       #,(if (null? (attribute p.decls))
+         #'b
+         #`(lambda #,@(attribute p.decls) b))))))
+
+(define-syntax (recur syn)
+  (syntax-case syn ()
+    [(_ id)
+     (dict-ref
+      ih-dict
+      (syntax->datum #'id)
+      (lambda ()
+        (raise-syntax-error
+         'match
+         ;; TODO: Detect when inside a match to provide better error
+         (format
+          "Cannot recur on ~a. Ether not inside a match or ~a is not an inductive argument."
+          (syntax->datum #'id)
+          (syntax->datum #'id))
+         syn)))]))
+
+(define-syntax (match syn)
+  (syntax-parse syn
+    [(_ d
+        ~!
+        (~optional
+         (~seq #:in ~! t)
+         #:defaults
+         ([t (or (cur-type-infer #'d)
+                 (raise-syntax-error
+                  'match
+                  "Could not infer discrimnant's type. Try using #:in to declare it."
+                  syn))]))
+        (~optional (~seq #:return ~! maybe-return-type))
+        (~peek (~seq (~var prec (match-preclause (attribute maybe-return-type))) ...))
+        ~!
+        (~parse D:inductive-type-declaration (cur-expand (attribute t)))
+        (~bind (return-type (ormap values (attribute prec.return-type))))
+        (~do (unless (attribute return-type)
+               (raise-syntax-error
+                'match
+                "Could not infer return type. Try using #:return to declare it."
+                syn)))
+        ;; BUG TODO: return-type is inferred with the indexes of the branches, but those must be abstracted in the motive...
+        ;; Replace each of the D.indicies with the equivalent name from D.decls
+        (~bind (motive (quasisyntax/loc syn
+                         (lambda #,@(attribute D.decls)
+                           #,((attribute D.abstract-indices) (attribute return-type))))))
+        (~var c (match-clause (attribute D) (attribute motive))) ...)
+     ;; TODO: Make all syntax extensions type check, report good error, rather than fail at Curnel
+     (quasisyntax/loc syn
+       (elim
+        D.inductive-name
+        motive
+        #,(attribute D.indices)
+        (c.method ...)
+        d))]))
+
+(begin-for-syntax
+  (define-syntax-class let-clause
+    (pattern
+      (~or (x:id e) ((x:id (~datum :) t) e))
+      #:attr id #'x
+      #:attr expr #'e
+      #:attr type (cond
+                    [(attribute t)
+                     ;; TODO: Code duplication in ::
+                     (unless (cur-type-check? #'e #'t)
+                       (raise-syntax-error
+                         'let
+                         (format "Term ~a does not have expected type ~a. Inferred type was ~a"
+                                 (cur->datum #'e) (cur->datum #'t) (cur->datum (cur-type-infer #'e)))
+                         #'e (quasisyntax/loc #'x (x e))))
+                     #'t]
+                    [(cur-type-infer #'e)]
+                    [else
+                      (raise-syntax-error
+                        'let
+                        "Could not infer type of let bound expression"
+                        #'e (quasisyntax/loc #'x (x e)))]))))
+(define-syntax (let syn)
+  (syntax-parse syn
+    [(let (c:let-clause ...) body)
+     #'((lambda (c.id : c.type) ... body) c.e ...)]))
+
+;; Normally type checking will only happen if a term is actually used/appears at top-level.
+;; This forces a term to be checked against a particular type.
+(define-syntax (:: syn)
+  (syntax-case syn ()
+    [(_ pf t)
+     (begin
+       ;; TODO: Code duplication in let-clause pattern
+       (unless (cur-type-check? #'pf #'t)
+         (raise-syntax-error
+           '::
+           (format "Term ~a does not have expected type ~a. Inferred type was ~a"
+                   (cur->datum #'pf) (cur->datum #'t) (cur->datum (cur-type-infer #'pf)))
+           syn))
+       #'(void))]))
+
+(define-syntax (run syn)
+  (syntax-case syn ()
+    [(_ expr) (cur-normalize #'expr)]))
+
+(define-syntax (step syn)
+  (syntax-case syn ()
+    [(_ expr)
+     (let ([t (cur-step #'expr)])
+       (displayln (cur->datum t))
+       t)]))
+
+(define-syntax (step-n syn)
+  (syntax-case syn ()
+    [(_ n expr)
+     (for/fold
+       ([expr #'expr])
+       ([i (in-range (syntax->datum #'n))])
+       #`(step #,expr))]))
+
+(define-syntax (query-type syn)
+  (syntax-case syn ()
+    [(_ term)
+     (begin
+       (printf "\"~a\" has type \"~a\"~n" (syntax->datum #'term) (syntax->datum (cur-type-infer #'term)))
+       ;; Void is undocumented and a hack, but sort of works
+       #'(void))]))

cur-lib/cur/stdlib/tactics/base.rkt

@@ -1,4 +1,4 @@
-#lang s-exp "../../cur.rkt"
+#lang s-exp "../../main.rkt"
 (require
   (for-syntax racket/syntax))
 (provide
@@ -10,6 +10,7 @@
     proof-state
     proof-state-env
     proof-state-goals
+    proof-state-current-goal
     proof-state-proof
     proof-state-theorem
     new-proof
@@ -219,7 +220,7 @@
            [pf (proof-state-proof ps)])
       (unless (proof-state-proof-complete? ps)
         (raise-syntax-error 'qed "Proof contains holes" (pf (current-hole-pretty-symbol))))
-      (unless (type-check/syn? pf t)
+      (unless (cur-type-check? pf t)
         (raise-syntax-error 'qed "Invalid proof" pf t))
       pf)))
 

cur-lib/cur/stdlib/tactics/sartactics.rkt

@@ -1,4 +1,4 @@
-#lang s-exp "../../cur.rkt"
+#lang s-exp "../../main.rkt"
 (require
   "base.rkt"
   (prefix-in basic: "standard.rkt")
@@ -124,12 +124,3 @@
             (loop (apply (lookup-tactic #'tactic)
                     (append (syntax->list #'(arg ...)) (list ps)))
                   (cons cmd cmds)))]))))
-
-(module+ test
-  (require
-    rackunit
-    "../bool.rkt")
-  (define-theorem meow (forall (x : Bool) Bool))
-  #;(proof
-    (interactive))
-  )

cur-lib/cur/stdlib/tactics/standard.rkt

@@ -1,4 +1,4 @@
-#lang s-exp "../../cur.rkt"
+#lang s-exp "../../main.rkt"
 (require
   "base.rkt"
   (for-syntax racket/syntax))
@@ -22,7 +22,7 @@
     [(forall (x:id : P:expr) body:expr)
      (let* ([ps (proof-state-extend-env ps name #'P)]
             [ps (proof-state-current-goal-set ps #'body)]
-            [ps (proof-state-fill-proof-hole ps (lambda (x) #`(lambda (#,name : P) #,x)))])
+            [ps (proof-state-fill-proof-hole ps (lambda (x) #`(λ (#,name : P) #,x)))])
        ps)]
     [_ (error 'intro "Can only intro when current goal is of the form (∀ (x : P) body)")]))
 
@@ -98,31 +98,3 @@
 ;; Open interactive REPL for tactic DSL; exit with QED command, which
 ;; returns a QED script
 ;(define-syntax interactive-proof)
-
-(module+ test
-  (require
-    rackunit
-    "../bool.rkt")
-  (define-theorem meow (forall (x : Bool) Bool))
-  (proof
-    (intro x)
-    (by-assumption))
-  (define-theorem meow1 (forall (x : Bool) Bool))
-  (proof
-    (obvious)
-    (print))
-  (define-theorem meow2 (forall (x : Bool) Bool))
-  (proof
-    (intro x)
-    (restart)
-    (intro x)
-    (by-assumption))
-  (define-theorem meow3 (forall (x : Bool) Bool))
-  (proof (obvious))
-  ;; TODO: Fix this unit test so it doesn't require interaction
-  (define-theorem meow4 (forall (x : Bool) Bool))
-  #;(proof
-    (interactive))
-  ;; TODO: Add check-cur-equal? for unit testing?
-  #;(check-pred (curry cur-equal? '(lambda (x : bool) x)))
-  )

cur-lib/cur/stdlib/typeclass.rkt

@@ -1,4 +1,4 @@
-#lang s-exp "../cur.rkt"
+#lang s-exp "../main.rkt"
 (require
   "nat.rkt"
   "bool.rkt"
@@ -7,6 +7,7 @@
     racket/syntax
     racket/dict
     racket/list))
+(provide (for-syntax typeclasses) typeclass impl)
 
 ;;; NB: This module is extremely unhygienic.
 #| TODO:
@@ -37,7 +38,7 @@
               #`(define-syntax (#,name syn)
                   (syntax-case syn ()
                     [(_ arg args (... ...))
-                     #`(#,(format-id syn "~a-~a" '#,name (type-infer/syn #'arg))
+                     #`(#,(format-id syn "~a-~a" '#,name (cur-type-infer #'arg))
                         arg
                         args (... ...))]))))]))
 
@@ -48,7 +49,7 @@
   (define (process-def def)
     (syntax-case def (define)
       [(define (name (a : t) ...) body ...)
-       (values (syntax->datum #'name) #'(lambda* (a : t) ... body ...))]
+       (values (syntax->datum #'name) #'(lambda (a : t) ... body ...))]
       [(define name body)
        (values (syntax->datum #'name) #'body)]))
   (syntax-case syn ()
@@ -56,7 +57,7 @@
      #`(begin
          #,@(for/list ([def (syntax->list #'(defs ...))])
               (let-values ([(name body) (process-def def)])
-                (unless (type-check/syn?
+                (unless (cur-type-check?
                           body
                           #`(#,(dict-ref
                                  (dict-ref typeclasses (syntax->datum #'class))
@@ -70,27 +71,3 @@
                     #'body))
                 #`(define #,(format-id syn "~a-~a" name #'param)
                     #,body))))]))
-
-(module+ test
-  (require rackunit)
-  (typeclass (Eqv (A : Type))
-    (equal? : (forall* (a : A) (b : A) Bool)))
-  (impl (Eqv Bool)
-    (define (equal? (a : Bool) (b : Bool))
-      (if a
-          (if b true false)
-          (if b false true))))
-  (impl (Eqv Nat)
-    (define equal? nat-equal?))
-  (check-equal?
-    (equal? z z)
-    true)
-  (check-equal?
-    (equal? z (s z))
-    false)
-  (check-equal?
-    (equal? true false)
-    false)
-  (check-equal?
-    (equal? true true)
-    true))

cur-lib/info.rkt

@@ -0,0 +1,7 @@
+#lang info
+(define collection 'multi)
+(define deps '("base" ("redex-lib" #:version "1.11")))
+(define build-deps '())
+(define pkg-desc "implementation (no documentation, tests) part of \"cur\".")
+(define version "0.4")
+(define pkg-authors '(wilbowma))

cur-test/cur/tests/olly.rkt

@@ -0,0 +1,58 @@
+#lang cur
+
+;; NB TODO: raco test reports incorrect number of total tests due to
+;; beign-for-syntax; but all failing tests correctly raise errors
+
+(require
+ rackunit
+ cur/stdlib/sugar
+ cur/olly)
+
+(begin-for-syntax
+  (require rackunit))
+
+;; 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"))
+   (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"))
+   (typeset-bnf #'((type (A B C) ::= unit (* A B) (+ A C))))))
+
+(begin-for-syntax
+  (check-equal?
+   (format "Inductive nat : Type :=~n| z : nat.~n")
+   (cur->coq #'(data nat : Type (z : nat))))
+  (check-regexp-match
+   "(forall .+ : Type, Type)"
+   (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 (cur->coq
+            #'(elim nat (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"
+   (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"
+   (cur->coq #'(define (add1 (n : nat)) (s n)))))

cur-test/cur/tests/plus.rkt

@@ -0,0 +1,24 @@
+#lang cur
+
+(require
+ cur/stdlib/sugar
+ rackunit)
+
+(data Nat : Type
+  (z : Nat)
+  (s : (Π (x : Nat) Nat)))
+
+(plus . : . (-> Nat Nat Nat))
+(define (plus n m)
+  (match n
+    [z m]
+    [(s (x : Nat))
+     (s (recur x))]))
+
+(check-equal?
+ (plus z z)
+ z)
+
+(check-equal?
+ (plus (s z) z)
+ (s z))

cur-test/cur/tests/redex-core.rkt

@@ -0,0 +1,649 @@
+#lang racket/base
+(require
+ redex/reduction-semantics
+ cur/curnel/redex-core
+ rackunit
+ racket/function
+ (only-in racket/set set=?))
+(define-syntax-rule (check-holds (e ...))
+  (check-true
+   (judgment-holds (e ...))))
+(define-syntax-rule (check-not-holds (e ...))
+  (check-false
+   (judgment-holds (e ...))))
+(define-syntax-rule (check-equiv? e1 e2)
+  (check (default-equiv) e1 e2))
+(define-syntax-rule (check-not-equiv? e1 e2)
+  (check (compose not (default-equiv)) e1 e2))
+
+(default-equiv (lambda (x y) (term (α-equivalent? ,x ,y))))
+
+;; Syntax tests
+;; ------------------------------------------------------------------------
+
+(define-term Type (Unv 0))
+(check-true (x? (term T)))
+(check-true (x? (term A)))
+(check-true (x? (term truth)))
+(check-true (x? (term zero)))
+(check-true (x? (term s)))
+(check-true (t? (term zero)))
+(check-true (t? (term s)))
+(check-true (x? (term nat)))
+(check-true (t? (term nat)))
+(check-true (t? (term A)))
+(check-true (t? (term S)))
+(check-true (U? (term (Unv 0))))
+(check-true (U? (term Type)))
+(check-true (e? (term (λ (x_0 : (Unv 0)) x_0))))
+(check-true (t? (term (λ (x_0 : (Unv 0)) x_0))))
+(check-true (t? (term (λ (x_0 : (Unv 0)) x_0))))
+
+;; TODO: Rename these signatures, and use them in all future tests.
+(define Δ (term ((∅ (nat : (Unv 0) ((zero : nat) (s : (Π (x : nat) nat)))))
+                 (bool : (Unv 0) ((true : bool) (false : bool))))))
+(define Δ0 (term ∅))
+(define Δ3 (term (∅ (and : (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Unv 0))) ()))))
+(define Δ4 (term (∅ (and : (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Unv 0)))
+                         ((conj : (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Π (a : A) (Π (b : B) ((and A) B)))))))))))
+(check-true (Δ? Δ0))
+(check-true (Δ? Δ))
+(check-true (Δ? Δ4))
+(check-true (Δ? Δ3))
+(check-true (Δ? Δ4))
+(define sigma (term ((((((∅ (true : (Unv 0) ((T : true))))
+                         (false : (Unv 0) ()))
+                        (equal : (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Unv 0)))
+                               ()))
+                       (nat : (Unv 0) ()))
+                      (heap : (Unv 0) ()))
+                     (pre : (Π (temp808 : heap) (Unv 0)) ()))))
+(check-true (Δ? (term (∅ (true : (Unv 0) ((T : true)))))))
+(check-true (Δ? (term (∅ (false : (Unv 0) ())))))
+(check-true (Δ? (term (∅ (equal : (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Unv 0)))
+                                ())))))
+(check-true (Δ? (term (∅ (nat : (Unv 0) ())))))
+(check-true (Δ? (term (∅ (pre : (Π (temp808 : heap) (Unv 0)) ())))))
+
+(check-true (Δ? (term ((∅ (true : (Unv 0) ((T : true)))) (false : (Unv 0) ())))))
+(check-true (Δ? (term (((∅ (true : (Unv 0) ((T : true)))) (false : (Unv 0) ()))
+                       (equal : (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Unv 0)))
+                              ())))))
+(check-true (Δ? sigma))
+(check-true (t? (term (Π (a : A) (Π (b : B) ((and A) B))))))
+
+
+;; α-equiv and subst tests
+;; ------------------------------------------------------------------------
+(check-true
+ (term
+  (α-equivalent?
+   (Π (a : S) (Π (b : B) ((and S) B)))
+   (subst (Π (a : A) (Π (b : B) ((and A) B))) A S))))
+
+;; Telescope tests
+;; ------------------------------------------------------------------------
+;; Are these telescopes the same when filled with alpha-equivalent, and equivalently renamed, termed
+(define (telescope-equiv x y)
+  (alpha-equivalent? ttL (term (in-hole ,x (Unv 0))) (term (in-hole ,y (Unv 0)))))
+(define-syntax-rule (check-telescope-equiv? e1 e2)
+  (check telescope-equiv e1 e2))
+(define-syntax-rule (check-telescope-not-equiv? e1 e2)
+  (check (compose not telescope-equiv) e1 e2))
+
+(check-telescope-equiv?
+ (term (Δ-ref-parameter-Ξ ,Δ nat))
+ (term hole))
+(check-telescope-equiv?
+ (term (Δ-ref-parameter-Ξ ,Δ4 and))
+ (term (Π (A : Type) (Π (B : Type) hole))))
+
+(check-true (x? (term false)))
+(check-true (Ξ? (term hole)))
+(check-true (t? (term (λ (y : false) (Π (x : Type) x)))))
+(check-true (redex-match? ttL ((x : t) ...) (term ())))
+
+;; Tests for inductive elimination
+;; ------------------------------------------------------------------------
+;; TODO: Insufficient tests, no tests of inductives with parameters, or complex induction.
+(check-true
+ (redex-match? tt-ctxtL (in-hole Θ_i (hole (in-hole Θ_r zero))) (term (hole zero))))
+(check-telescope-equiv?
+ (term (Δ-inductive-elim ,Δ nat
+                         (elim nat (λ (x : nat) nat) ()
+                               ((s zero) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+                               hole)
+                         (hole zero)))
+ (term (hole (elim nat (λ (x : nat) nat)
+                   ()
+                   ((s zero)
+                    (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+                   zero))))
+(check-telescope-equiv?
+ (term (Δ-inductive-elim ,Δ nat
+                         (elim nat (λ (x : nat) nat) ()
+                               ((s zero) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+                               hole)
+                         (hole (s zero))))
+ (term (hole (elim nat (λ (x : nat) nat) ()
+                   ((s zero) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+                   (s zero)))))
+(check-telescope-equiv?
+ (term (Δ-inductive-elim ,Δ nat
+                         (elim nat (λ (x : nat) nat) ()
+                               ((s zero) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+                               hole)
+                         hole))
+ (term hole))
+
+;; Tests for dynamic semantics
+;; ------------------------------------------------------------------------
+
+(check-true (v? (term (λ (x_0 : (Unv 0)) x_0))))
+(check-true (v? (term (refl Nat))))
+(check-true (v? (term ((refl Nat) z))))
+(check-true (v? (term zero)))
+(check-true (v? (term (s zero))))
+
+;; TODO: Move equivalence up here, and use in these tests.
+(check-equiv? (term (reduce ∅ (Unv 0))) (term (Unv 0)))
+(check-equiv? (term (reduce ∅ ((λ (x : t) x) (Unv 0)))) (term (Unv 0)))
+(check-not-equiv? (term (reduce ∅ ((Π (x : t) x) (Unv 0)))) (term (Unv 0)))
+(check-not-equiv? (term (reduce ∅ (Π (x : t) ((Π (x_0 : t) x_0) (Unv 0)))))
+                  (term (Π (x : t) (Unv 0))))
+(check-not-equiv? (term (reduce ∅ (Π (x : t) ((Π (x_0 : t) (x_0 x)) x))))
+                  (term (Π (x : t) (x x))))
+
+(check-equal? (term (Δ-constructor-index ,Δ nat zero)) 0)
+(check-equiv? (term (reduce ,Δ (elim nat (λ (x : nat) nat)
+                                     ()
+                                     ((s zero)
+                                      (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+                                     zero)))
+              (term (s zero)))
+(check-equiv? (term (reduce ,Δ (elim nat (λ (x : nat) nat)
+                                     ()
+                                     ((s zero)
+                                      (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+                                     (s zero))))
+              (term (s (s zero))))
+(check-equiv? (term (reduce ,Δ (elim nat (λ (x : nat) nat)
+                                     ()
+                                     ((s zero)
+                                      (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+                                (s (s (s zero))))))
+              (term (s (s (s (s zero))))))
+
+(check-equiv?
+ (term (reduce ,Δ
+               (elim nat (λ (x : nat) nat)
+                     ()
+                     ((s (s zero))
+                      (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
+                     (s (s zero)))))
+ (term (s (s (s (s zero))))))
+(check-equiv?
+ (term (step ,Δ
+             (elim nat (λ (x : nat) nat)
+                     ()
+                     ((s (s zero))
+                      (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
+                     (s (s zero)))))
+ (term
+  (((λ (x : nat) (λ (ih-x : nat) (s ih-x)))
+    (s zero))
+   (elim nat (λ (x : nat) nat)
+         ()
+         ((s (s zero))
+          (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
+         (s zero)))))
+(check-equiv?
+ (term (step ,Δ (step ,Δ
+                      (((λ (x : nat) (λ (ih-x : nat) (s ih-x)))
+                        (s zero))
+                       (elim nat (λ (x : nat) nat)
+                             ()
+                             ((s (s zero))
+                              (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
+                             (s zero))))))
+ (term
+  ((λ (ih-x1 : nat) (s ih-x1))
+   (((λ (x : nat) (λ (ih-x : nat) (s ih-x)))
+     zero)
+    (elim nat (λ (x : nat) nat)
+          ()
+          ((s (s zero))
+           (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
+          zero)))))
+
+(define-syntax-rule (check-equivalent e1 e2)
+  (check-holds (convert ∅ ∅ e1 e2)))
+(check-equivalent
+ (λ (x : Type) x) (λ (y : Type) y))
+(check-equivalent
+ (Π (x : Type) x) (Π (y : Type) y))
+
+;; Test static semantics
+;; ------------------------------------------------------------------------
+
+(check-true (term (positive* nat (nat))))
+(check-true (term (positive* nat ((Π (x : (Unv 0)) (Π (y : (Unv 0)) nat))))))
+(check-true (term (positive* nat ((Π (x : nat) nat)))))
+;; (nat -> nat) -> nat
+;; Not sure if this is actually supposed to pass
+(check-false (term (positive* nat ((Π (x : (Π (y : nat) nat)) nat)))))
+;; ((Unv 0) -> nat) -> nat
+(check-true (term (positive* nat ((Π (x : (Π (y : (Unv 0)) nat)) nat)))))
+;; (((nat -> (Unv 0)) -> nat) -> nat)
+(check-true (term (positive* nat ((Π (x : (Π (y : (Π (x : nat) (Unv 0))) nat)) nat)))))
+;; Not sure if this is actually supposed to pass
+;; ((nat -> nat) -> nat) -> nat
+(check-false (term (positive* nat ((Π (x : (Π (y : (Π (x : nat) nat)) nat)) nat)))))
+
+(check-true (judgment-holds (wf ,Δ0 ∅)))
+(check-true (redex-match? tt-redL (in-hole Ξ (Unv 0)) (term (Unv 0))))
+(check-true (redex-match? tt-redL (in-hole Ξ (in-hole Φ (in-hole Θ nat)))
+                          (term (Π (x : nat) nat))))
+(define (bindings-equal? l1 l2)
+  (map set=? l1 l2))
+(check-pred
+ (curry bindings-equal?
+        (list (list
+               (make-bind 'Ξ (term (Π (x : nat) hole)))
+               (make-bind 'Φ (term hole))
+               (make-bind 'Θ (term hole)))
+              (list
+               (make-bind 'Ξ (term hole))
+               (make-bind 'Φ (term (Π (x : nat) hole)))
+               (make-bind 'Θ (term hole)))))
+ (map match-bindings (redex-match tt-redL (in-hole Ξ (in-hole Φ (in-hole Θ nat)))
+                                  (term (Π (x : nat) nat)))))
+(check-pred
+ (curry bindings-equal?
+        (list
+         (list
+          (make-bind 'Φ (term (Π (x : nat) hole)))
+          (make-bind 'Θ (term hole)))))
+ (map match-bindings (redex-match tt-redL (in-hole hole (in-hole Φ (in-hole Θ nat)))
+                                  (term (Π (x : nat) nat)))))
+
+(check-true
+ (redex-match? tt-redL
+               (in-hole hole (in-hole hole (in-hole hole nat)))
+               (term nat)))
+(check-true
+ (redex-match? tt-redL
+               (in-hole hole (in-hole (Π (x : nat) hole) (in-hole hole nat)))
+               (term (Π (x : nat) nat))))
+(check-holds (wf (∅ (nat : (Unv 0) ())) ∅))
+
+(check-holds (wf ,Δ0 ∅))
+(check-holds (type-infer ∅ ∅ (Unv 0) U))
+(check-holds (type-infer ∅ (∅ nat : (Unv 0)) nat U))
+(check-holds (type-infer ∅ (∅ nat : (Unv 0)) (Π (x : nat) nat) U))
+(check-true (term (positive* nat (nat (Π (x : nat) nat)))))
+(check-holds
+ (wf (∅ (nat : (Unv 0) ((zero : nat)))) ∅))
+(check-holds
+ (wf (∅ (nat : (Unv 0) ((s : (Π (x : nat) nat))))) ∅))
+(check-holds (wf ,Δ ∅))
+
+(check-holds (wf ,Δ3 ∅))
+(check-holds (wf ,Δ4 ∅))
+(check-holds (wf (∅ (truth : (Unv 0) ())) ∅))
+(check-holds (wf ∅ (∅ x : (Unv 0))))
+(check-holds (wf (∅ (nat : (Unv 0) ())) (∅ x : nat)))
+(check-holds (wf (∅ (nat : (Unv 0) ())) (∅ x : (Π (x : nat) nat))))
+
+(check-holds (type-infer ∅ ∅ (Unv 0) (Unv 1)))
+(check-holds (type-infer ∅ (∅ x : (Unv 0)) (Unv 0) (Unv 1)))
+(check-holds (type-infer ∅ (∅ x : (Unv 0)) x (Unv 0)))
+(check-holds (type-infer ∅ ((∅ x_0 : (Unv 0)) x_1 : (Unv 0))
+                           (Π (x_3 : x_0) x_1) (Unv 0)))
+(check-holds (type-infer ∅ (∅ x_0 : (Unv 0)) x_0 U_1))
+(check-holds (type-infer ∅ ((∅ x_0 : (Unv 0)) x_2 : x_0) (Unv 0) U_2))
+(check-holds (unv-pred (Unv 0) (Unv 0) (Unv 0)))
+(check-holds (type-infer ∅ (∅ x_0 : (Unv 0)) (Π (x_2 : x_0) (Unv 0)) t))
+
+(check-holds (type-check ∅ ∅ (λ (x : (Unv 0)) x) (Π (x : (Unv 0)) (Unv 0))))
+(check-holds (type-check ∅ ∅ (λ (y : (Unv 0)) (λ (x : y) x))
+                             (Π (y : (Unv 0)) (Π (x : y) y))))
+
+(check-equal? (list (term (Unv 1)))
+              (judgment-holds
+               (type-infer ∅ ((∅ x1 : (Unv 0)) x2 : (Unv 0)) (Π (t6 : x1) (Π (t2 : x2) (Unv 0)))
+                             U)
+               U))
+;; ---- Elim
+;; TODO: Clean up/Reorganize these tests
+(define Δtruth (term (∅ (truth : (Unv 0) ((T : truth))))))
+(check-holds (type-infer ,Δtruth ∅ truth (in-hole Ξ U)))
+(check-holds (type-infer ,Δtruth ∅ T (in-hole Θ_ai truth)))
+(check-holds (type-infer ,Δtruth ∅ (λ (x : truth) (Unv 1))
+                         (in-hole Ξ (Π (x : (in-hole Θ truth)) U))))
+
+(check-equiv?
+ (term (Δ-motive-type ,Δtruth truth (Unv 2)))
+ (term (Π (x : truth) (Unv 2))))
+
+
+(check-holds (type-check ,Δtruth ∅ (Unv 0) ,(car (term (Δ-method-types ,Δtruth truth (λ (x : truth) (Unv 1)))))))
+
+(check-holds (type-check ,Δtruth ∅ (λ (x : truth) (Unv 1)) (Π (x : truth) (Unv 2))))
+
+(check-equiv?
+ (term (apply (λ (x : truth) (Unv 1)) T))
+ (term ((λ (x : truth) (Unv 1)) T)))
+
+(check-holds
+ (convert ,Δtruth ∅ (apply (λ (x : truth) (Unv 1)) T) (Unv 1)))
+
+(check-holds (type-infer ,Δtruth
+                         ∅
+                         (elim truth (λ (x : truth) (Unv 1))
+                               () ((Unv 0)) T)
+                         t))
+
+(check-holds (type-check ,Δtruth
+                         ∅
+                         (elim truth (λ (x : truth) (Unv 1))
+                               () ((Unv 0)) T)
+                         (Unv 1)))
+(check-not-holds (type-check (∅ (truth : (Unv 0) ((T : truth))))
+                             ∅
+                             (elim truth Type () (Type) T)
+                             (Unv 1)))
+(check-holds
+ (type-infer ∅ ∅ (Π (x2 : (Unv 0)) (Unv 0)) U))
+(check-holds
+ (type-infer ∅ (∅ x1 : (Unv 0)) (λ (x2 : (Unv 0)) (Π (t6 : x1) (Π (t2 : x2) (Unv 0))))
+               t))
+(check-holds
+ (type-infer ,Δ ∅ nat (in-hole Ξ U)))
+(check-holds
+ (type-infer ,Δ ∅ zero (in-hole Θ_ai nat)))
+(check-holds
+ (type-infer ,Δ ∅ (λ (x : nat) nat)
+             (in-hole Ξ (Π (x : (in-hole Θ nat)) U))))
+(define-syntax-rule (nat-test syn ...)
+  (check-holds (type-check ,Δ syn ...)))
+(nat-test ∅ (Π (x : nat) nat) (Unv 0))
+(nat-test ∅ (λ (x : nat) x) (Π (x : nat) nat))
+(nat-test ∅ (elim nat (λ (x : nat) nat) ()
+                  (zero (λ (x : nat) (λ (ih-x : nat) x)))
+                  zero)
+            nat)
+(nat-test ∅ nat (Unv 0))
+(nat-test ∅ zero nat)
+(nat-test ∅ s (Π (x : nat) nat))
+(nat-test ∅ (s zero) nat)
+(check-holds
+ (type-infer ,Δ ∅ (λ (x : nat)
+                    (elim nat (λ (x : nat) nat)
+                          ()
+                          (zero
+                           (λ (x : nat) (λ (ih-x : nat) x)))
+                          x))
+             t))
+(nat-test ∅ (elim nat (λ (x : nat) nat)
+                  ()
+                  (zero (λ (x : nat) (λ (ih-x : nat) x)))
+                  zero)
+            nat)
+(nat-test ∅ (elim nat (λ (x : nat) nat)
+                  ()
+                  ((s zero) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+                  zero)
+            nat)
+(nat-test ∅ (elim nat (λ (x : nat) nat)
+                  ()
+                  ((s zero) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+                  zero)
+            nat)
+(nat-test (∅ n : nat)
+          (elim nat (λ (x : nat) nat)
+                ()
+                (zero (λ (x : nat) (λ (ih-x : nat) x)))
+                n)
+          nat)
+(check-holds
+ (type-check (,Δ (bool : (Unv 0) ((btrue : bool) (bfalse : bool))))
+             (∅ n2 : nat)
+             (elim nat (λ (x : nat) bool)
+                   ()
+                   (btrue (λ (x : nat) (λ (ih-x : bool) bfalse)))
+                   n2)
+             bool))
+(check-not-holds
+ (type-check ,Δ ∅
+             (elim nat nat () ((s zero)) zero)
+             nat))
+(define lam (term (λ (nat : (Unv 0)) nat)))
+(check-equivalent
+ (Π (nat : (Unv 0)) (Unv 0))
+ ,(car (judgment-holds (type-infer ,Δ0 ∅ ,lam t) t)))
+(check-equivalent
+ (Π (nat : (Unv 0)) (Unv 0))
+ ,(car (judgment-holds (type-infer ,Δ ∅ ,lam t) t)))
+(check-equivalent
+ (Π (x : (Π (y : (Unv 0)) y)) nat)
+ ,(car (judgment-holds (type-infer (∅ (nat : (Unv 0) ())) ∅ (λ (x : (Π (y : (Unv 0)) y)) (x nat))
+                                   t) t)))
+(check-equivalent
+ (Π (y : (Unv 0)) (Unv 0))
+ ,(car (judgment-holds (type-infer (∅ (nat : (Unv 0) ())) ∅ (λ (y : (Unv 0)) y) t) t)))
+(check-equivalent
+ (Unv 0)
+ ,(car (judgment-holds (type-infer (∅ (nat : (Unv 0) ())) ∅
+                                   ((λ (x : (Π (y : (Unv 0)) (Unv 0))) (x nat))
+                                    (λ (y : (Unv 0)) y))
+                                   t) t)))
+(check-equal?
+ (list (term (Unv 0)) (term (Unv 1)))
+ (judgment-holds
+  (type-infer ,Δ4 ∅ (Π (S : (Unv 0)) (Π (B : (Unv 0)) (Π (a : S) (Π (b : B) ((and S) B)))))
+              U) U))
+(check-holds
+ (type-check ,Δ4 (∅ S : (Unv 0)) conj (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Π (a : A) (Π (b : B) ((and A) B)))))))
+(check-holds
+ (type-check ,Δ4 (∅ S : (Unv 0))
+             conj (Π (P : (Unv 0)) (Π (Q : (Unv 0)) (Π (x : P) (Π (y : Q) ((and P) Q)))))))
+(check-holds
+ (type-check ,Δ4 (∅ S : (Unv 0)) S (Unv 0)))
+(check-holds
+ (type-check ,Δ4 (∅ S : (Unv 0)) (conj S)
+             (Π (B : (Unv 0)) (Π (a : S) (Π (b : B) ((and S) B))))))
+(check-holds
+ (type-check ,Δ4 (∅ S : (Unv 0)) (conj S)
+             (Π (B : (Unv 0)) (Π (a : S) (Π (b : B) ((and S) B))))))
+(check-holds
+ (type-check ,Δ4 ∅ (λ (S : (Unv 0)) (conj S))
+             (Π (S : (Unv 0)) (Π (B : (Unv 0)) (Π (a : S) (Π (b : B) ((and S) B)))))))
+(check-holds
+ (type-check (,Δ4 (true : (Unv 0) ((tt : true)))) ∅
+             ((((conj true) true) tt) tt)
+             ((and true) true)))
+(check-holds
+ (type-infer ,Δ4 ∅ and (in-hole Ξ U_D)))
+(check-holds
+ (type-infer (,Δ4 (true : (Unv 0) ((tt : true)))) ∅
+             ((((conj true) true) tt) tt)
+             (in-hole Θ and)))
+(check-holds
+ (type-infer (,Δ4 (true : (Unv 0) ((tt : true)))) ∅
+             (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B)) true)))
+             (in-hole Ξ (Π (x : (in-hole Θ_Ξ and)) U_P))))
+(check-holds
+ (type-check (,Δ4 (true : (Unv 0) ((tt : true)))) ∅
+             (elim and
+                   (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B))
+                                                 true)))
+                   (true true)
+                   ((λ (A : (Unv 0))
+                      (λ (B : (Unv 0))
+                        (λ (a : A)
+                          (λ (b : B) tt)))))
+                   ((((conj true) true) tt) tt))
+             true))
+(check-true (Γ? (term (((∅ P : (Unv 0)) Q : (Unv 0)) ab : ((and P) Q)))))
+(check-holds
+ (type-infer ,Δ4 ∅ and (in-hole Ξ U)))
+(check-holds
+ (type-infer ,Δ4 (((∅ P : Type) Q : Type) ab : ((and P) Q))
+             ab (in-hole Θ and)))
+(check-true
+ (redex-match? tt-redL
+               (in-hole Ξ (Π (x : (in-hole Θ and)) U))
+               (term (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Π (x : ((and A) B)) (Unv 0)))))))
+(check-holds
+ (type-infer ,Δ4 (((∅ P : Type) Q : Type) ab : ((and P) Q))
+             (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B))
+                                           ((and B) A))))
+             (in-hole Ξ (Π (x : (in-hole Θ and)) U))))
+(check-holds
+ (convert ,Δ4 ∅
+             (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Π (x : ((and A) B)) (Unv 0))))
+             (Π (P : (Unv 0)) (Π (Q : (Unv 0)) (Π (x : ((and P) Q)) (Unv 0))))))
+(check-holds
+ (type-infer ,Δ4 ∅
+             (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B))
+                                           ((and B) A))))
+             (in-hole Ξ (Π (x : (in-hole Θ_Ξ and)) U_P))))
+(check-holds
+ (type-check ,Δ4
+             (((∅ P : (Unv 0)) Q : (Unv 0)) ab : ((and P) Q))
+             (elim and
+                   (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B))
+                                                 ((and B) A))))
+                   (P Q)
+                   ((λ (A : (Unv 0))
+                      (λ (B : (Unv 0))
+                        (λ (a : A)
+                          (λ (b : B) ((((conj B) A) b) a))))))
+                   ab)
+             ((and Q) P)))
+(check-holds
+ (type-check (,Δ4 (true : (Unv 0) ((tt : true)))) ∅
+             (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B)) ((and B) A))))
+             (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Π (x : ((and A) B)) (Unv 0))))))
+(check-holds
+ (type-infer (,Δ4 (true : (Unv 0) ((tt : true))))
+             ((∅ A : Type) B : Type)
+             (conj B)
+             t))
+(check-holds
+ (type-check (,Δ4 (true : (Unv 0) ((tt : true)))) ∅
+             (elim and
+                  (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B))
+                                                ((and B) A))))
+                 (true true)
+                 ((λ (A : (Unv 0))
+                   (λ (B : (Unv 0))
+                     (λ (a : A)
+                       (λ (b : B) ((((conj B) A) b) a))))))
+              ((((conj true) true) tt) tt))
+             ((and true) true)))
+(define gamma (term (∅ temp863 : pre)))
+(check-holds (wf ,sigma ∅))
+(check-holds (wf ,sigma ,gamma))
+(check-holds
+ (type-infer ,sigma ,gamma (Unv 0) t))
+(check-holds
+ (type-infer ,sigma ,gamma pre t))
+(check-holds
+ (type-check ,sigma (,gamma tmp863 : pre) (Unv 0) (Unv 1)))
+(check-holds
+ (type-infer ,sigma ,gamma pre t))
+(check-holds
+ (type-check ,sigma (,gamma tmp863 : pre) (Unv 0) (Unv 1)))
+(check-holds
+ (type-infer ,sigma (,gamma x : false) false (in-hole Ξ U_D)))
+(check-holds
+ (type-infer ,sigma (,gamma x : false) x (in-hole Θ false)))
+(check-holds
+ (type-infer ,sigma (,gamma x : false) (λ (y : false) (Π (x : Type) x))
+             (in-hole Ξ (Π (x : (in-hole Θ false)) U))))
+
+(check-holds
+ (type-check ,sigma (,gamma x : false)
+             (elim false (λ (y : false) (Π (x : Type) x)) () () x)
+             (Π (x : (Unv 0)) x)))
+
+;; nat-equal? tests
+(define zero?
+  (term (λ (n : nat)
+          (elim nat (λ (x : nat) bool) ()
+              (true (λ (x : nat) (λ (x_ih : bool) false)))
+              n))))
+(check-holds
+ (type-check ,Δ ∅ ,zero? (Π (x : nat) bool)))
+(check-equal?
+ (term (reduce ,Δ (,zero? zero)))
+ (term true))
+(check-equal?
+ (term (reduce ,Δ (,zero? (s zero))))
+ (term false))
+(define ih-equal?
+  (term (λ (ih : nat)
+          (elim nat (λ (x : nat) bool)
+              ()
+              (false
+               (λ (x : nat) (λ (y : bool) (x_ih x))))
+              ih))))
+(check-holds
+ (type-check ,Δ (∅ x_ih : (Π (x : nat) bool))
+             ,ih-equal?
+             (Π (x : nat) bool)))
+(check-holds
+ (type-infer ,Δ ∅ nat (Unv 0)))
+(check-holds
+ (type-infer ,Δ ∅ bool (Unv 0)))
+(check-holds
+ (type-infer ,Δ ∅ (λ (x : nat) (Π (x : nat) bool)) (Π (x : nat) (Unv 0))))
+(define nat-equal?
+  (term (λ (n : nat)
+          (elim nat (λ (x : nat) (Π (x : nat) bool))
+              ()
+              (,zero?
+              (λ (x : nat) (λ (x_ih : (Π (x : nat) bool))
+                             ,ih-equal?)))
+              n))))
+(check-holds
+ (type-check ,Δ (∅ nat-equal? : (Π (x-D«4158» : nat) ((λ (x«4159» : nat) (Π (x«4160» : nat) bool)) x-D«4158»)))
+             ((nat-equal? zero) zero)
+             bool))
+(check-holds
+ (type-check ,Δ ∅
+             ,nat-equal?
+             (Π (x : nat) (Π (y : nat) bool))))
+(check-equal?
+ (term (reduce ,Δ ((,nat-equal? zero) (s zero))))
+ (term false))
+(check-equal?
+ (term (reduce ,Δ ((,nat-equal? (s zero)) zero)))
+ (term false))
+
+;; == tests
+(define Δ= (term (,Δ (== : (Π (A : (Unv 0)) (Π (a : A) (Π (b : A) (Unv 0))))
+                         ((refl : (Π (A : (Unv 0)) (Π (a : A) (((== A) a) a)))))))))
+(check-true (Δ? Δ=))
+
+(define refl-elim
+  (term (elim == (λ (A1 : (Unv 0)) (λ (x1 : A1) (λ (y1 : A1) (λ (p2 : (((== A1) x1) y1)) nat))))
+                  (bool true true)
+                  ((λ (A1 : (Unv 0)) (λ (x1 : A1) zero)))
+                  ((refl bool) true))))
+(check-holds
+ (type-check ,Δ= ∅ ,refl-elim nat))
+(check-true
+ (redex-match?
+  tt-redL
+  (in-hole (Θ_p (in-hole Θ_i x_ci)) Θ_m)
+  (term (((((hole
+             (λ (A1 : (Unv 0)) (λ (x1 : A1) zero))) bool) true) true) ((refl bool) true)))))
+(check-telescope-equiv?
+ (term (Δ-ref-parameter-Ξ ,Δ= ==))
+ (term (Π (A : Type) (Π (a : A) (Π (b : A) hole)))))
+(check-equal?
+ (term (reduce ,Δ= ,refl-elim))
+ (term zero))

cur-test/cur/tests/stdlib/bool.rkt

@@ -0,0 +1,18 @@
+#lang cur
+(require
+ rackunit
+ cur/stdlib/bool
+ cur/stdlib/sugar)
+
+(check-equal? (not true) false)
+(check-equal? (not false) true)
+
+(check-equal? (and true false) false)
+(check-equal? (and false false) true)
+(check-equal? (and false true) false)
+(check-equal? (and true true) true)
+
+(check-equal? (or true false) true)
+(check-equal? (or false false) false)
+(check-equal? (or false true) true)
+(check-equal? (or true true) true)

cur-test/cur/tests/stdlib/list.rkt

@@ -0,0 +1,49 @@
+#lang cur
+(require
+ rackunit
+ cur/stdlib/sugar
+ cur/stdlib/bool
+ cur/stdlib/nat
+ cur/stdlib/maybe
+ cur/stdlib/list)
+
+(check-equal?
+ nil
+ nil)
+;; NB HACK: Hack to register :: as a test-case.
+;; TODO: Abstract this away
+(check-equal?
+ (void)
+ (:: (cons Bool true (nil Bool)) (List Bool)))
+(check-equal?
+ (void)
+ (:: (lambda (A : Type) (a : A)
+             (ih-a : (-> Nat (Maybe A))) 
+             (n : Nat)
+             (match n
+               [z (some A a)]
+               [(s (n-1 : Nat))
+                (ih-a n-1)]))
+     (forall (A : Type) (a : A) (ih-a : (-> Nat (Maybe A)))
+             (n : Nat)
+             (Maybe A))))
+(check-equal?
+ (void)
+ (:: (lambda (A : Type) (n : Nat) (none A)) (forall (A : Type) (-> Nat (Maybe A)))))
+(check-equal?
+ (void)
+ (:: (elim List (lambda (A : Type) (ls : (List A)) Nat)
+           (Bool)
+          ((lambda (A : Type) z)
+           (lambda (A : Type) (a : A) (ls : (List A)) (ih : Nat)
+                   z))
+          (nil Bool))
+    Nat))
+
+
+(check-equal?
+ (void)
+ (:: list-ref (forall (A : Type) (-> (List A) Nat (Maybe A)))))
+(check-equal?
+ ((list-ref Bool (cons Bool true (nil Bool))) z)
+ (some Bool true))

cur-test/cur/tests/stdlib/maybe.rkt

@@ -0,0 +1,20 @@
+#lang cur
+
+(require
+ rackunit
+ cur/stdlib/sugar
+ cur/stdlib/bool
+ cur/stdlib/maybe)
+
+(check-equal?
+ (some/i true)
+ (some Bool true))
+;; Disabled until #22 fixed
+#;(check-equal?
+   (match (some Bool true)
+     [(none (A : Type))
+      false]
+     [(some (A : Type) (x : A))
+      ;; TODO: Don't know how to use dependency yet
+      (if x true false)])
+   true)

cur-test/cur/tests/stdlib/nat.rkt

@@ -0,0 +1,32 @@
+#lang cur
+(require
+ cur/stdlib/sugar
+ cur/stdlib/nat
+ cur/stdlib/bool
+ rackunit)
+
+(check-equal? (add1 (s z)) (s (s z)))
+(check-equal? (sub1 (s z)) z)
+
+(check-equal? (plus z z) z)
+(check-equal? (plus (s (s z)) (s (s z))) (s (s (s (s z)))))
+
+(check-equal? (mult (s (s z)) z) z)
+(check-equal? (mult (s (s z)) (s z)) (s (s z)))
+
+;; TODO Disabled due to performance bugs
+#;(check-equal? (exp z z) (s z))
+#;(check-equal? (exp (s z) z) z)
+#;(check-equal? (square (s (s z))) (s (s (s (s z)))))
+
+(check-equal? (nat-equal? z z) true)
+(check-equal? (nat-equal? z (s z)) false)
+(check-equal? (nat-equal? (s z) (s z)) true)
+
+(check-equal? (even? z) true)
+(check-equal? (even? (s z)) false)
+(check-equal? (even? (s (s z))) true)
+(check-equal? (odd? z) false)
+(check-equal? (odd? (s z)) true)
+(check-equal? (odd? (s (s z))) false)
+(check-equal? (odd? (s (s (s z)))) true)

cur-test/cur/tests/stdlib/prop.rkt

@@ -0,0 +1,36 @@
+#lang cur
+(require
+ cur/stdlib/prop
+ cur/stdlib/sugar
+ cur/stdlib/bool
+ cur/stdlib/nat
+ rackunit)
+
+(:: pf:anything-implies-true thm:anything-implies-true)
+(:: pf:and-is-symmetric thm:and-is-symmetric)
+(:: pf:proj1 thm:proj1)
+(:: pf:proj2 thm:proj2)
+(check-equal?
+ (elim == (λ (A : Type) (x : A) (y : A) (p : (== A x y)) Nat)
+       (Bool
+        true
+        true)
+       ((λ (A : Type) (x : A) z))
+       (refl Bool true))
+ z)
+
+(check-equal?
+ (conj/i (conj/i T T) T)
+ (conj (And True True) True (conj True True T T) T))
+
+(define (id (A : Type) (x : A)) x)
+
+(check-equal?
+ ((id (== True T T))
+  (refl True (run (id True T))))
+ (refl True T))
+
+(check-equal?
+ ((id (== True T T))
+  (refl True (id True T)))
+ (refl True T))

cur-test/cur/tests/stdlib/sartactics.rkt

@@ -0,0 +1,12 @@
+#lang cur
+
+(require
+ rackunit
+ cur/stdlib/bool
+ cur/stdlib/sugar
+ cur/stdlib/tactics/base
+ cur/stdlib/tactics/sartactics)
+
+;; TODO: To much randomness for easy automated testing
+(define-theorem meow (forall (x : Bool) Bool))
+  #;(proof (interactive))

cur-test/cur/tests/stdlib/sugar.rkt

@@ -0,0 +1,51 @@
+#lang cur
+(require
+ rackunit
+ cur/stdlib/sugar)
+
+;; TODO: Missing tests for match, others
+(check-equal?
+ ((λ (x : (Type 1)) (y : (∀ (x : (Type 1)) (Type 1))) (y x))
+  Type
+  (λ (x : (Type 1)) x))
+ Type)
+
+(check-equal?
+ ((λ (x : (Type 1)) (y : (→ (Type 1) (Type 1))) (y x))
+  Type
+  (λ (x : (Type 1)) x))
+ Type)
+
+(check-equal?
+ ((λ (x : (Type 1)) (y : (→ (Type 1) (Type 1))) (y x))
+  Type
+  (λ (x : (Type 1)) x))
+ Type)
+
+(check-equal?
+ (let ([x Type]
+       [y (λ (x : (Type 1)) x)])
+   (y x))
+ Type)
+
+(check-equal?
+ (let ([(x : (Type 1)) Type]
+       [y (λ (x : (Type 1)) x)])
+   (y x))
+ Type)
+
+;; check that raises decent syntax error
+;; Can't use this because (lambda () ...) and thunk are not things in Cur at runtime
+#;(check-exn
+   exn:fail:syntax?
+   (let ([x : (Type 1) Type]
+         [y (λ (x : (Type 1)) x)])
+     (y x)))
+
+;; check that raises type error
+#;(check-exn
+   exn:fail:syntax?
+   (let ([x uninferrable-expr]
+         [y (λ (x : (Type 1)) x)])
+     (y x)))
+

cur-test/cur/tests/stdlib/tactics.rkt

@@ -0,0 +1,36 @@
+#lang cur
+
+(require
+ rackunit
+ cur/stdlib/sugar
+ cur/stdlib/bool
+ cur/stdlib/tactics/base
+ cur/stdlib/tactics/standard)
+(define-theorem meow (forall (x : Bool) Bool))
+(check-equal?
+ ((proof
+   (intro x)
+   (by-assumption)) true)
+ true)
+(define-theorem meow1 (forall (x : Bool) Bool))
+(check-equal?
+ ((proof
+   (obvious)
+   ;; TODO: Add ability to check output
+   #;(print)) true)
+ true)
+(define-theorem meow2 (forall (x : Bool) Bool))
+(check-equal?
+ ((proof
+  (intro x)
+  (restart)
+  (intro x)
+  (by-assumption)) true)
+ true)
+(define-theorem meow3 (forall (x : Bool) Bool))
+(check-equal?
+ ((proof (obvious)) true)
+ true)
+;; TODO: Fix this unit test so it doesn't require interaction
+(define-theorem meow4 (forall (x : Bool) Bool))
+#;(proof (interactive))

cur-test/cur/tests/stdlib/typeclass.rkt

@@ -0,0 +1,28 @@
+#lang cur
+
+(require
+ rackunit
+ cur/stdlib/sugar
+ cur/stdlib/bool
+ cur/stdlib/nat
+ cur/stdlib/typeclass)
+
+(typeclass (Eqv (A : Type))
+           (equal? : (forall (a : A) (b : A) Bool)))
+(impl (Eqv Bool)
+      (define (equal? (a : Bool) (b : Bool))
+        (if a b (not b))))
+(impl (Eqv Nat)
+      (define equal? nat-equal?))
+(check-equal?
+ (equal? z z)
+ true)
+(check-equal?
+ (equal? z (s z))
+ false)
+(check-equal?
+ (equal? true false)
+ false)
+(check-equal?
+ (equal? true true)
+ true)

cur-test/cur/tests/stlc.rkt

@@ -0,0 +1,132 @@
+#lang cur
+(require
+ rackunit
+ cur/stdlib/nat
+ cur/stdlib/list
+ cur/stdlib/sugar
+ cur/olly
+ cur/stdlib/maybe
+ cur/stdlib/bool
+ cur/stdlib/prop)
+
+(define-language stlc
+  #:vars (x)
+  #:output-coq "stlc.v"
+  #:output-latex "stlc.tex"
+  (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 (#:bind x : A) e) (cons e e)
+                  (let (#:bind x #:bind x) = e in e)))
+
+(define lookup-env (list-ref stlc-type))
+
+(define (extend-env (g : (List stlc-type)) (t : stlc-type))
+  (cons stlc-type t g))
+
+(define-relation (has-type (List stlc-type) stlc-term stlc-type)
+  #:output-coq "stlc.v"
+  #:output-latex "stlc.tex"
+  [(g : (List stlc-type))
+   ------------------------ T-Unit
+   (has-type g (stlc-val->stlc-term stlc-unit) stlc-unitty)]
+
+  [(g : (List stlc-type))
+   ------------------------ T-True
+   (has-type g (stlc-val->stlc-term stlc-true) stlc-boolty)]
+
+  [(g : (List stlc-type))
+   ------------------------ T-False
+   (has-type g (stlc-val->stlc-term stlc-false) stlc-boolty)]
+
+  [(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 (Nat->stlc-term x) t)]
+
+  [(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 : (List stlc-type)) (e1 : stlc-term) (e2 : stlc-term)
+               (t1 : stlc-type) (t2 : stlc-type)
+               (t : stlc-type)
+   (has-type g e1 (stlc-* t1 t2))
+   (has-type (extend-env (extend-env g t1) t2) e2 t)
+   ---------------------- T-Let
+   (has-type g (stlc-let e1 e2) t)]
+
+  [(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 t1 e1) (stlc--> t1 t2))]
+
+  [(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)
+   ---------------------- T-App
+   (has-type g (stlc-app e1 e2) t2)])
+
+;; A parser, for a deep-embedding of STLC.
+;; TODO: We should be able to generate these
+;; 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 (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)
+  (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)
+       #`(stlc-lambda #,(stlc #'t d) #,(stlc #'e (dict-set (dict-shift d) (syntax->datum #'x) #`z)))]
+      [(quote (e1 e2))
+       #`(stlc-cons #,(stlc #'e1 d) #,(stlc #'e2 d))]
+      [(let (x y) = e1 in e2)
+       #`(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 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 d) #,(stlc #'t2 d))]
+      [(t1 -> t2)
+       #`(stlc--> #,(stlc #'t1 d) #,(stlc #'t2 d))]
+      [bool #`stlc-boolty]
+      [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 stlc-unitty (Nat->stlc-term z)))
+(check-equal?
+ (begin-stlc ((lambda (x : 1) x) ()))
+ (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)))
+(check-equal?
+ (begin-stlc #t)
+ (stlc-val->stlc-term stlc-true))

cur-test/cur/tests/sweet-exp.rkt

@@ -0,0 +1,16 @@
+#lang sweet-exp cur
+require
+ cur/stdlib/sugar
+ cur/stdlib/bool
+ cur/stdlib/nat
+ rackunit
+
+check-equal?
+  if true false true
+  false
+
+define + plus
+
+check-equal?
+  {z + s(z)}
+  s(z)

cur-test/info.rkt

@@ -0,0 +1,7 @@
+#lang info
+(define collection 'multi)
+(define deps '())
+(define build-deps '("base" "rackunit-lib" ("cur-lib" #:version "0.4") "sweet-exp"))
+(define update-implies '("cur-lib"))
+(define pkg-desc "Tests for \"cur\".")
+(define pkg-authors '(wilbowma))

cur/info.rkt

@@ -0,0 +1,6 @@
+#lang info
+(define collection 'multi)
+(define deps '("cur-lib" "cur-doc" "cur-test"))
+(define implies '("cur-lib" "cur-doc" "cur-test"))
+(define pkg-desc "Dependent types with parenthesis and meta-programming.")
+(define pkg-authors '(wilbowma))

examples/stlc.rkt

@@ -1,144 +0,0 @@
-#lang s-exp "../cur.rkt"
-(require
-  "../stdlib/nat.rkt"
-  "../stdlib/sugar.rkt"
-  "../oll.rkt"
-  "../stdlib/maybe.rkt"
-  "../stdlib/bool.rkt"
-  "../stdlib/prop.rkt")
-
-(define-language stlc
-  #:vars (x)
-  #:output-coq "stlc.v"
-  #:output-latex "stlc.tex"
-  (val  (v)   ::= true false unit)
-  ;; TODO: Allow datum 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)))
-
-;; 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-gamma (g : Gamma) (x : Var))
-  (case* Gamma Type g () (lambda* (g : Gamma) (Maybe stlc-type))
-    [emp-gamma (none stlc-type)]
-    [(extend-gamma (g1 : Gamma) (v1 : Var) (t1 : stlc-type))
-     IH: ((ih-g1 : (Maybe stlc-type)))
-     (if (var-equal? v1 x)
-         (some stlc-type t1)
-         ih-g1)]))
-
-(define-relation (has-type Gamma stlc-term stlc-type)
-  #:output-coq "stlc.v"
-  #:output-latex "stlc.tex"
-  [(g : Gamma)
-   ------------------------ T-Unit
-   (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)]
-
-  [(g : Gamma)
-   ------------------------ T-False
-   (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))
-   ------------------------ T-Var
-   (has-type g (Var-->-stlc-term x) t)]
-
-  [(g : Gamma) (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)
-               (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)
-   ---------------------- T-Let
-   (has-type g (stlc-let x y 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)
-   ---------------------- T-Fun
-   (has-type g (stlc-lambda x t1 e1) (stlc--> t1 t2))]
-
-  [(g : Gamma) (e1 : stlc-term) (e2 : stlc-term)
-               (t1 : stlc-type) (t2 : stlc-type)
-   (has-type g e1 (stlc--> t1 t2))
-   (has-type g e2 t1)
-   ---------------------- T-App
-   (has-type g (stlc-app e1 e2) t2)])
-
-;; A parser, for a deep-embedding of STLC.
-;; TODO: We should be able to generate these
-;; 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-syntax (begin-stlc syn)
-  (set! index #'z)
-  (let stlc ([syn (syntax-case syn () [(_ e) #'e])])
-    (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)))))]
-      [(quote (e1 e2))
-       #`(stlc-cons #,(stlc #'e1) #,(stlc #'e2))]
-      [(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))]
-      [(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)]
-      [(t1 * t2)
-       #`(stlc-* #,(stlc #'t1) #,(stlc #'t2))]
-      [(t1 -> t2)
-       #`(stlc--> #,(stlc #'t1) #,(stlc #'t2))]
-      [bool #`stlc-boolty]
-      [e
-       (if (eq? 1 (syntax->datum #'e))
-           #'stlc-unitty
-           #'e)])))
-
-(module+ test
-  (require rackunit)
-  (check-equal?
-    (begin-stlc (lambda (x : 1) x))
-    (stlc-lambda (avar z) stlc-unitty (Var-->-stlc-term (avar 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)))
-  (check-equal?
-    (begin-stlc '(() ()))
-    (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)))

info.rkt

@@ -1,8 +0,0 @@
-#lang info
-(define collection "cur")
-(define deps '("base" "rackunit-lib" ("redex-lib" #:version "1.6")))
-(define build-deps '("scribble-lib" "racket-doc" "sandbox-lib"))
-(define scribblings '(("scribblings/cur.scrbl" (multi-page))))
-(define pkg-desc "Dependent types with parenthesis and meta-programming.")
-(define version "0.1")
-(define pkg-authors '(wilbowma))

oll.rkt

@@ -1,405 +0,0 @@
-#lang s-exp "cur.rkt"
-;; OLL: The OTT-Like Library
-;; TODO: Automagically create a parser from bnf grammar
-(require
-  "stdlib/sugar.rkt"
-  "stdlib/nat.rkt"
-  (only-in "curnel/redex-lang.rkt" [#%app real-app] [elim real-elim]))
-
-(provide
-  define-relation
-  define-language
-  Var
-  avar
-  var-equal?
-  generate-coq
-  #;(rename-out [oll-define-theorem define-theorem]))
-
-(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 : (forall* 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)))))
-
-(module+ test
-  (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)))))
-
-;; 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)))
-(module+ test
-  (require "stdlib/sugar.rkt")
-  (begin-for-syntax
-    (require rackunit)
-    (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)))))
-    (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)))))))
-;; 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))
-  (case* Var Type v1 () (lambda (v : Var) Bool)
-    [(avar (n1 : Nat)) IH: ()
-     (case* Var Type v2 () (lambda (v : Var) Bool)
-       [(avar (n2 : Nat)) IH: ()
-        (nat-equal? n1 n2)])]))
-(module+ test
-  (require rackunit)
-  (check-equal?
-    (var-equal? (avar z) (avar z))
-    true)
-  (check-equal?
-    (var-equal? (avar z) (avar (s z)))
-    false))
-
-;; See stlc.rkt for examples
-
-;; 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 #'define-theorem #'qed
-                              #'begin)
-       ;; TODO: Need to add these to a literal set and export it
-       ;; Or, maybe overwrite syntax-parse
-       #:literals (lambda forall data real-app real-elim define-theorem
-                          define qed begin Type)
-       [(begin e ...)
-        (for/fold ([str ""])
-                  ([e (syntax->list #'(e ...))])
-          (format "~a~n" (output-coq e)))]
-       [(define-theorem name prop)
-        (begin
-          (fprintf (current-error-port) "Warning: If theorem ~a is not followed by a proof using (qed ...), the resulting Coq code may be malformed.~n" (output-coq #'name))
-          (coq-lift-top-level
-            (format "Theorem ~a : ~a.~n"
-                    (output-coq #'name)
-                    (output-coq #'prop)))
-          "")]
-       [(qed thm proof)
-        ;; TODO: Have some sort of coq-lift-to-theorem, to auto match
-        ;; proofs and theorems.
-        (begin
-          (coq-lift-top-level
-            (format "Proof. exact ~a. Qed.~n" (output-coq #'proof)))
-          "")]
-       [(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)))
-          "")]
-       [(lambda ~! (x:id (~datum :) t) body:expr)
-        (format "(fun ~a : ~a => ~a)" (output-coq #'x) (output-coq #'t)
-                (output-coq #'body))]
-       [(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-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))
-       #'(begin))]))
-
-(module+ test
-  (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"))
-    (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))])
-      (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))])
-      (check-regexp-match
-        "\\(\\(\\(\\(nat_rect \\(fun x : nat => nat\\)\\) z\\) \\(fun x : nat => \\(fun ih_x : nat => ih_x\\)\\)\\) e\\)"
-        t))
-    (check-regexp-match
-      "Theorem thm_plus_commutes : \\(forall n : nat, \\(forall m : nat, \\(\\(\\(== nat\\) \\(\\(plus n\\) m\\)\\) \\(\\(plus m\\) n\\)\\)\\)\\).\n"
-      (parameterize ([coq-defns ""])
-        (output-coq #'(define-theorem thm:plus-commutes
-                                     (forall* (n : nat) (m : nat)
-                                              (== nat (plus n m) (plus m n)))))
-        (coq-defns)))
-    (check-regexp-match
-      "Function add1 \\(n : nat\\)  := \\(s n\\).\n"
-      (parameterize ([coq-defns ""])
-        (output-coq #'(define (add1 (n : nat)) (s n)))
-        (coq-defns)))))

scribblings/curnel.scrbl

@@ -1,135 +0,0 @@
-#lang scribble/manual
-
-@(require "defs.rkt")
-
-@title{Curnel Forms}
-@deftech{Curnel forms} are the core forms provided @racketmodname[cur].
-These forms come directly from the trusted core and are all that remain after macro expansion.
-@todo{Link to guide regarding macro expansion}
-The core of @racketmodname[cur] is essentially TT.
-For a very understandable in-depth look at TT, see chapter 2 of
-@hyperlink["https://eb.host.cs.st-andrews.ac.uk/writings/thesis.pdf"
-           "Practical Implementation of a Dependently Typed Functional Programming Language"], by
-Edwin C. Brady.
-
-@(require racket/sandbox scribble/eval)
-@(define curnel-eval
-   (parameterize ([sandbox-output 'string]
-                  [sandbox-error-output 'string]
-                  [sandbox-eval-limits #f]
-                  [sandbox-memory-limit #f])
-     (make-module-evaluator "#lang cur")))
-
-@defform[(Type n)]{
-Define the universe of types at level @racket[n], where @racket[n] is any natural number.
-
-
-@examples[#:eval curnel-eval
-          (Type 0)]
-
-@examples[#:eval curnel-eval
-          (Type 1)]
-}
-
-@defidform[Type]{
-A synonym for @racket[(Type 0)].
-
-
-@examples[#:eval curnel-eval
-          Type]
-}
-
-@defform*[((lambda (id : type-expr) body-expr)
-           (λ (id : type-expr) body-expr))]{
-Produces a single arity procedure, binding the identifier @racket[id] of type @racket[type-expr] in @racket[body-expr] and in the type of
-@racket[body-expr].
-Both @racket[type-expr] and @racket[body-expr] can contain non-curnel forms, such as macros.
-
-Currently, Cur will return the underlying representation of a procedure when a @racket[lambda] is
-evaluated at the top-level. Do not rely on this representation.
-
-@examples[#:eval curnel-eval
-          (lambda (x : Type) x)]
-
-@examples[#:eval curnel-eval
-          (λ (x : Type) (lambda (y : x) y))]
-
-
-@defform[(#%app procedure argument)]{
-Applies the single arity @racket[procedure] to @racket[argument].
-}
-
-@examples[#:eval curnel-eval
-          ((lambda (x : (Type 1)) x) Type)]
-
-@examples[#:eval curnel-eval
-          (#%app (lambda (x : (Type 1)) x) Type)]
-}
-
-@defform*[((forall (id : type-expr) body-expr)
-           (∀ (id : type-expr) body-expr))]{
-Produces a dependent function type, binding the identifier @racket[id] of type @racket[type-expr] in @racket[body-expr].
-
-
-@examples[#:eval curnel-eval
-          (forall (x : Type) Type)]
-
-@examples[#:eval curnel-eval
-          (lambda (x : (forall (x : (Type 1)) Type))
-            (x Type))]
-}
-
-@defform[(data id : type-expr (id* : type-expr*) ...)]{
-Defines an inductive datatype named @racket[id] of type @racket[type-expr], with constructors
-@racket[id*] each with the corresponding type @racket[type-expr*].
-Currently, Cur does not attempt to ensure the well-foundedness of the inductive definition.
-For instance, Cur does not currently perform strict positivity checking.
-
-@examples[#:eval curnel-eval
-          (data Bool : Type
-                (true : Bool)
-                (false : Bool))
-          ((lambda (x : Bool) x) true)
-          (data False : Type)
-          (data And : (forall (A : Type) (forall (B : Type) Type))
-            (conj : (forall (A : Type) (forall (B : Type) (forall (a : A) (forall (b : B) ((And A) B)))))))
-          ((((conj Bool) Bool) true) false)]
-}
-
-@defform[(elim type motive-universe)]{
-Returns the inductive eliminator for @racket[type] where the @racket[motive-universe] is the universe
-of the motive.
-The eliminator expects the next argument to be the motive, the next @racket[N] arguments to be the methods for
-each of the @racket[N] constructors of the inductive type @racket[type], the next @racket[P] arguments
-to be the parameters @racket[p_0 ... p_P] of the inductive @racket[type], and the final argument to be the term to
-eliminate of type @racket[(type p_0 ... p_P)].
-
-The following example runs @racket[(sub1 (s z))].
-
-@examples[#:eval curnel-eval
-          (data Nat : Type
-            (z : Nat)
-            (s : (forall (n : Nat) Nat)))
-          (((((elim Nat Type)
-              (lambda (x : Nat) Nat))
-             z)
-            (lambda (n : Nat) (lambda (IH : Nat) n)))
-           (s z))]
-}
-
-@defform[(define id expr)]{
-Binds @racket[id] to the result of @racket[expr].
-
-@examples[#:eval curnel-eval
-          (data Nat : Type
-            (z : Nat)
-            (s : (forall (n : Nat) Nat)))
-          (define sub1 (lambda (n : Nat)
-                         (((((elim Nat Type) (lambda (x : Nat) Nat))
-                           z)
-                          (lambda (n : Nat) (lambda (IH : Nat) n))) n)))
-          (sub1 (s (s z)))
-          (sub1 (s z))
-          (sub1 z)]
-}
-@todo{Document @racket[require] and @racket[provide]}

scribblings/defs.rkt

@@ -1,10 +0,0 @@
-#lang racket/base
-
-(require scribble/base scribble/manual)
-(provide (all-defined-out))
-
-(define (todo . ls)
-  (apply margin-note* "TODO: " ls))
-
-(define (gtech . x)
-  (apply tech x #:doc '(lib "scribblings/guide/guide.scrbl")))

scribblings/stdlib/sugar.scrbl

@@ -1,180 +0,0 @@
-#lang scribble/manual
-
-@(require "../defs.rkt")
-
-@;(TODO Move this to defs.rkt)
-@(require racket/sandbox scribble/eval)
-@(define curnel-eval
-   (parameterize ([sandbox-output 'string]
-                  [sandbox-error-output 'string]
-                  [sandbox-eval-limits #f]
-                  [sandbox-memory-limit #f])
-     (make-module-evaluator "#lang cur (require cur/stdlib/bool) (require cur/stdlib/sugar)")))
-
-
-@title{Sugar}
-The @tech{curnel forms} are sort of terrible for actually writing code. Functions and applications are
-limited to single artity. Functions type must be specified using the dependent @racket[forall], even
-when the dependency is not used. Inductive elimination can only be done via the primitive eliminator
-and not via pattern matching. However, with the full force of Racket's syntactic extension system, we
-can define not only simply notation, but redefine what application means, or define a pattern matcher
-that expands into the eliminator.
-
-@defmodule[cur/stdlib/sugar]
-This library defines various syntactic extensions making Cur easier to write than writing raw TT.
-
-@defform[(-> t1 t2)]{
-A non-dependent function type Equivalent to @racket[(forall (_ : t1) t2)], where @racket[_] indicates an variable that is not used.
-
-@examples[#:eval curnel-eval
-          (data And : (-> Type (-> Type Type))
-            (conj : (forall (A : Type) (forall (B : Type) (-> A (-> B ((And A) B)))))))
-          ((((conj Bool) Bool) true) false)]
-}
-
-@defform[(->* t ...)]{
-A non-dependent multi-arity function type that supports automatic currying.
-
-@examples[#:eval curnel-eval
-          (data And : (->* Type Type Type)
-            (conj : (forall (A : Type) (forall (B : Type) (->* A B ((And A) B))))))
-          ((((conj Bool) Bool) true) false)]
-}
-
-
-@defform[(forall* (a : t) ... type)]{
-A multi-arity function type that supports automatic currying.
-
-@examples[#:eval curnel-eval
-          (data And : (->* Type Type Type)
-            (conj : (forall* (A : Type) (B : Type)
-                      (->* A B ((And A) B)))))
-          ((((conj Bool) Bool) true) false)]
-
-}
-
-@defform[(lambda* (a : t) ... body)]{
-Defines a multi-arity procedure that supports automatic currying.
-
-@examples[#:eval curnel-eval
-          ((lambda (x : Bool) (lambda (y : Bool) y)) true)
-          ((lambda* (x : Bool) (y : Bool) y) true)
-          ]
-}
-
-@defform[(#%app f a ...)]{
-Defines multi-arity procedure application via automatic currying.
-
-@examples[#:eval curnel-eval
-          (data And : (->* Type Type Type)
-            (conj : (forall* (A : Type) (B : Type)
-                      (->* A B ((And A) B)))))
-          (conj Bool Bool true false)]
-}
-
-@defform*[((define name body)
-           (define (name (x : t) ...) body))]{
-Like the @racket[define] provided by @racketmodname[cur/curnel/redex-lang], but supports
-defining curried functions via @racket[lambda*].
-}
-
-@defform[(elim type motive-result-type e ...)]{
-Like the @racket[elim] provided by @racketmodname[cur/curnel/redex-lang], but supports
-automatically curries the remaining arguments @racket[e ...].
-
-@examples[#:eval curnel-eval
-          (require cur/stdlib/bool)
-          (elim Bool Type (lambda (x : Bool) Bool)
-            false
-            true
-            true)]
-}
-
-@defform*[((define-type name type)
-           (define-type (name (a : t) ...) body))]{
-Like @racket[define], but uses @racket[forall*] instead of @racket[lambda*].
-}
-
-@defform[(case e [pattern maybe-IH body] ...)
-         #:grammar
-         [(pattern
-            constructor
-            (code:line)
-            (code:line (constructor (x : t) ...)))
-          (maybe-IH
-            (code:line)
-            (code:line IH: ((x : t) ...)))]]{
-A pattern-matcher-like syntax for inductive elimination. Actually does not do pattern matching and
-relies on the constructors patterns being specified in the same order as when the inductive type was
-defined.
-
-@examples[#:eval curnel-eval
-          (require cur/stdlib/nat)
-          (case z
-            [z true]
-            [(s (n : Nat))
-             IH: ((_ : Bool))
-             false])]
-}
-
-@defform[(case* type motive-result-type e (parameters ...) motive [pattern maybe-IH body] ...)
-         #:grammar
-         [(pattern
-            constructor
-            (code:line)
-            (code:line (constructor (x : t) ...)))
-          (maybe-IH
-            (code:line)
-            (code:line IH: ((x : t) ...)))]]{
-A pattern-matcher-like syntax for inductive elimination that does not try to infer the type or motive.
-Necessary for more advanced types, like @racket[And], because @racket[case] is not very smart.
-
-@margin-note{Don't worry about all that output from requiring prop}
-@examples[#:eval curnel-eval
-          (require cur/stdlib/nat)
-          (case* Nat Type z () (lambda (x : Nat) Bool)
-            [z true]
-            [(s (n : Nat))
-             IH: ((_ : Bool))
-             false])
-          (require cur/stdlib/prop)
-          (case* And Type (conj Bool Nat true z) (Bool Nat)
-            (lambda* (A : Type) (B : Type) (ab : (And A B)) A)
-            [(conj (A : Type) (B : Type) (a : A) (b : B))
-             IH: ()
-             a])]
-}
-
-@defform[(run syn)]{
-Like @racket[normalize/syn], but is a syntactic form which allows a Cur term to be written by
-computing part of the term from another Cur term.
-
-@examples[#:eval curnel-eval
-          (lambda (x : (run (if true Bool Nat))) x)]
-
-}
-
-@defform[(step syn)]{
-Like @racket[run], but uses @racket[step/syn] to evaluate only one step and prints intermediate
-results before returning the result of evaluation.
-
-@examples[#:eval curnel-eval
-          (step (plus z z))]
-
-}
-
-@defform[(step-n natural syn)]{
-Like @racket[step], but expands to @racket[natural] calls to @racket[step].
-
-@examples[#:eval curnel-eval
-          (step-n 3 (plus z z))]
-
-}
-
-@defform[(query-type expr)]{
-Print the type of @racket[expr], at compile-time. Similar to Coq's @racketfont{Check}.
-
-@examples[#:eval curnel-eval
-          (query-type Bool)]
-
-}

stdlib/bool.rkt

@@ -1,41 +0,0 @@
-#lang s-exp "../cur.rkt"
-(require "sugar.rkt")
-(provide Bool true false if not and or)
-
-(data Bool : Type
-  (true : Bool)
-  (false : Bool))
-
-(define-syntax-rule (if t s f)
-  (case t
-    [true s]
-    [false f]))
-
-(define (not (x : Bool)) (if x false true))
-
-(module+ test
-  (require rackunit)
-  (check-equal? (not true) false)
-  (check-equal? (not false) true))
-
-(define (and (x : Bool) (y : Bool))
-  (if x
-      y
-      (not y)))
-
-(module+ test
-  (check-equal? (and true false) false)
-  (check-equal? (and false false) true)
-  (check-equal? (and false true) false)
-  (check-equal? (and true true) true))
-
-(define (or (x : Bool) (y : Bool))
-  (if x
-      true
-      y))
-
-(module+ test
-  (check-equal? (or true false) true)
-  (check-equal? (or false false) false)
-  (check-equal? (or false true) true)
-  (check-equal? (or true true) true))

stdlib/maybe.rkt

@@ -1,20 +0,0 @@
-#lang s-exp "../cur.rkt"
-(require "sugar.rkt")
-(provide Maybe none some)
-
-(data Maybe : (forall (A : Type) Type)
-  (none : (forall (A : Type) (Maybe A)))
-  (some : (forall* (A : Type) (a : A) (Maybe A))))
-
-(module+ test
-  (require rackunit "bool.rkt")
-  ;; Disabled until #22 fixed
-  #;(check-equal?
-    (case* Maybe Type (some Bool true) (Bool)
-      (lambda* (A : Type) (x : (Maybe A)) A)
-      [(none (A : Type)) IH: ()
-       false]
-      [(some (A : Type) (x : A)) IH: ()
-       ;; TODO: Don't know how to use dependency yet
-       (if x true false)])
-    true))

stdlib/nat.rkt

@@ -1,82 +0,0 @@
-#lang s-exp "../cur.rkt"
-(require "sugar.rkt" "bool.rkt")
-;; TODO: override (all-defined-out) to enable exporting all these
-;; properly.
-(provide Nat z s add1 sub1 plus )
-(module+ test
-  (require rackunit))
-
-(data Nat : Type
-  (z : Nat)
-  (s : (-> Nat Nat)))
-
-(define (add1 (n : Nat)) (s n))
-(module+ test
-  (check-equal? (add1 (s z)) (s (s z))))
-
-(define (sub1 (n : Nat))
-  (case n
-    [z z]
-    [(s (x : Nat)) IH: ((ih-n : Nat)) x]))
-(module+ test
-  (check-equal? (sub1 (s z)) z))
-
-(define (plus (n1 : Nat) (n2 : Nat))
-  (case n1
-    [z n2]
-    [(s (x : Nat))
-     IH: ((ih-n1 : Nat))
-     (s ih-n1)]))
-(module+ test
-  (check-equal? (plus z z) z)
-  (check-equal? (plus (s (s z)) (s (s z))) (s (s (s (s z))))))
-
-;; Credit to this function goes to Max
-(define nat-equal?
-  (elim Nat Type (lambda (x : Nat) (-> Nat Bool))
-    (elim Nat Type (lambda (x : Nat) Bool)
-          true
-          (lambda* (x : Nat) (ih-n2 : Bool) false))
-    (lambda* (x : Nat) (ih : (-> Nat Bool))
-      (elim Nat Type (lambda (x : Nat) Bool)
-            false
-            (lambda* (x : Nat) (ih-bla : Bool)
-                     (ih x))))))
-(module+ test
-  (check-equal? (nat-equal? z z) true)
-  (check-equal? (nat-equal? z (s z)) false)
-  (check-equal? (nat-equal? (s z) (s z)) true))
-
-(define (even? (n : Nat))
-  (elim Nat Type (lambda (x : Nat) Bool)
-        true
-        (lambda* (n : Nat) (odd? : Bool)
-           (not odd?))
-        n))
-
-(define (odd? (n : Nat))
-  (not (even? n)))
-
-(module+ test
-  (check-equal?
-    (even? z)
-    true)
-  (check-equal?
-    (even? (s z))
-    false)
-  (check-equal?
-    (even? (s (s z)))
-    true)
-  (check-equal?
-    (odd? z)
-    false)
-  (check-equal?
-    (odd? (s z))
-    true)
-  (check-equal?
-    (odd? (s (s z)))
-    false)
-  (check-equal?
-    (odd? (s (s (s z))))
-    true))
-

stdlib/prop.rkt

@@ -1,97 +0,0 @@
-#lang s-exp "../cur.rkt"
-(require "sugar.rkt")
-;; TODO: Handle multiple provide forms properly
-;; TODO: Handle (all-defined-out) properly
-(provide
-  True T
-  thm:anything-implies-true
-  False
-  Not
-  And
-  conj
-  thm:and-is-symmetric proof:and-is-symmetric
-  thm:proj1 proof:proj1
-  thm:proj2 proof:proj2
-  == refl)
-
-(data True : Type (T : True))
-
-(define-theorem thm:anything-implies-true (forall (P : Type) True))
-
-(qed thm:anything-implies-true (lambda (P : Type) T))
-
-(data False : Type)
-
-(define-type (Not (A : Type)) (-> A False))
-
-(data And : (forall* (A : Type) (B : Type) Type)
-  (conj : (forall* (A : Type) (B : Type)
-            (x : A) (y : B) (And A B))))
-
-(define-theorem thm:and-is-symmetric
-  (forall* (P : Type) (Q : Type) (ab : (And P Q)) (And Q P)))
-
-(define proof:and-is-symmetric
-  (lambda* (P : Type) (Q : Type) (ab : (And P Q))
-    (case* And Type ab (P Q)
-      (lambda* (P : Type) (Q : Type) (ab : (And P Q))
-         (And Q P))
-      ((conj (P : Type) (Q : Type) (x : P) (y : Q)) IH: () (conj Q P y x)))))
-
-(qed thm:and-is-symmetric proof:and-is-symmetric)
-
-(define-theorem thm:proj1
-  (forall* (A : Type) (B : Type) (c : (And A B)) A))
-
-(define proof:proj1
-  (lambda* (A : Type) (B : Type) (c : (And A B))
-    (case* And Type c (A B)
-      (lambda* (A : Type) (B : Type) (c : (And A B)) A)
-      ((conj (A : Type) (B : Type) (a : A) (b : B)) IH: () a))))
-
-(qed thm:proj1 proof:proj1)
-
-(define-theorem thm:proj2
-  (forall* (A : Type) (B : Type) (c : (And A B)) B))
-
-(define proof:proj2
-  (lambda* (A : Type) (B : Type) (c : (And A B))
-    (case* And Type c (A B)
-      (lambda* (A : Type) (B : Type) (c : (And A B)) B)
-      ((conj (A : Type) (B : Type) (a : A) (b : B)) IH: () b))))
-
-(qed thm:proj2 proof:proj2)
-
-#| TODO: Disabled until #22 fixed
-(data Or : (forall* (A : Type) (B : Type) Type)
-  (left : (forall* (A : Type) (B : Type) (a : A) (Or A B)))
-  (right : (forall* (A : Type) (B : Type) (b : B) (Or A B))))
-
-(define-theorem thm:A-or-A
-  (forall* (A : Type) (o : (Or A A)) A))
-
-(define proof:A-or-A
-  (lambda* (A : Type) (c : (Or A A))
-    ;; TODO: What should the motive be?
-    (elim Or Type (lambda* (A : Type) (B : Type) (c : (Or A B)) A)
-      (lambda* (A : Type) (B : Type) (a : A) a)
-      ;; TODO: How do we know B is A?
-      (lambda* (A : Type) (B : Type) (b : B) b)
-      A A c)))
-
-(qed thm:A-or-A proof:A-or-A)
-|#
-
-(data == : (forall* (A : Type) (x : A) (-> A Type))
-  (refl : (forall* (A : Type) (x : A) (== A x x))))
-
-(module+ test
-  (require rackunit "bool.rkt" "nat.rkt")
-  (check-equal?
-    (elim == Type (λ* (A : Type) (x : A) (y : A) (p : (== A x y)) Nat)
-         (λ* (A : Type) (x : A) z)
-         Bool
-         true
-         true
-         (refl Bool true))
-    z))

stdlib/sugar.rkt

@@ -1,170 +0,0 @@
-#lang s-exp "../cur.rkt"
-(provide
-  ->
-  ->*
-  forall*
-  lambda*
-  (rename-out
-    [-> →]
-    [->* →*]
-    [lambda* λ*]
-    [forall* ∀*])
-  #%app
-  define
-  elim
-  define-type
-  case
-  case*
-  run
-  step
-  step-n
-  query-type
-
-  ;; don't use these
-  define-theorem
-  qed
-  )
-
-(require
-  (only-in "../cur.rkt"
-    [elim real-elim]
-    [#%app real-app]
-    [define real-define]))
-
-
-(define-syntax (-> syn)
-  (syntax-case syn ()
-    [(_ t1 t2) #`(forall (#,(gensym) : t1) t2)]))
-
-(define-syntax ->*
-  (syntax-rules ()
-    [(->* a) a]
-    [(->* a a* ...)
-     (-> a (->* a* ...))]))
-
-(define-syntax forall*
-  (syntax-rules (:)
-    [(_ (a : t) (ar : tr) ... b)
-     (forall (a : t)
-        (forall* (ar : tr) ... b))]
-    [(_ b) b]))
-
-(define-syntax lambda*
-  (syntax-rules (:)
-    [(_ (a : t) (ar : tr) ... b)
-     (lambda (a : t)
-       (lambda* (ar : tr) ... b))]
-    [(_ b) b]))
-
-(define-syntax (#%app syn)
-  (syntax-case syn ()
-    [(_ e1 e2)
-     #'(real-app e1 e2)]
-    [(_ e1 e2 e3 ...)
-     #'(#%app (#%app e1 e2) e3 ...)]))
-
-(define-syntax define-type
-  (syntax-rules ()
-    [(_ (name (a : t) ...) body)
-     (define name (forall* (a : t) ... body))]
-    [(_ name type)
-     (define name type)]))
-
-(define-syntax (define syn)
-  (syntax-case syn ()
-    [(define (name (x : t) ...) body)
-     #'(real-define name (lambda* (x : t) ... body))]
-    [(define id body)
-     #'(real-define id body)]))
-
-(define-syntax-rule (elim t1 t2 e ...)
-  ((real-elim t1 t2) e ...))
-
-(begin-for-syntax
-  (define (rewrite-clause clause)
-    (syntax-case clause (: IH:)
-      [((con (a : A) ...) IH: ((x : t) ...) body)
-       #'(lambda* (a : A) ... (x : t) ... body)]
-      [(e body) #'body])))
-
-;; TODO: Expects clauses in same order as constructors as specified when
-;; TODO: inductive D is defined.
-;; TODO: Assumes D has no parameters
-(define-syntax (case syn)
-  ;; duplicated code
-  (define (clause-body syn)
-    (syntax-case (car (syntax->list syn)) (: IH:)
-      [((con (a : A) ...) IH: ((x : t) ...) body) #'body]
-      [(e body) #'body]))
-  (syntax-case syn (=>)
-    [(_ e clause* ...)
-     (let* ([D (type-infer/syn #'e)]
-            [M (type-infer/syn (clause-body #'(clause* ...)))]
-            [U (type-infer/syn M)])
-       #`(elim #,D #,U (lambda (x : #,D) #,M) #,@(map rewrite-clause (syntax->list #'(clause* ...)))
-               e))]))
-
-(define-syntax (case* syn)
-  (syntax-case syn ()
-    [(_ D U e (p ...) P clause* ...)
-     #`(elim D U P #,@(map rewrite-clause (syntax->list #'(clause* ...))) p ... e)]))
-
-(define-syntax-rule (define-theorem name prop)
-  (define name prop))
-
-(define-syntax (qed stx)
-  (syntax-case stx ()
-    [(_ t pf)
-     (begin
-       (unless (type-check/syn? #'pf #'t)
-         (raise-syntax-error 'qed "Invalid proof"
-           #'pf #'t))
-       #'pf)]))
-
-(define-syntax (run syn)
-  (syntax-case syn ()
-    [(_ expr) (normalize/syn #'expr)]))
-
-(define-syntax (step syn)
-  (syntax-case syn ()
-    [(_ expr)
-     (let ([t (step/syn #'expr)])
-       (displayln (cur->datum t))
-       t)]))
-
-(define-syntax (step-n syn)
-  (syntax-case syn ()
-    [(_ n expr)
-     (for/fold
-       ([expr #'expr])
-       ([i (in-range (syntax->datum #'n))])
-       #`(step #,expr))]))
-
-(define-syntax (query-type syn)
-  (syntax-case syn ()
-    [(_ term)
-     (begin
-       (printf "\"~a\" has type \"~a\"~n" (syntax->datum #'term) (syntax->datum (type-infer/syn #'term)))
-       ;; Void is undocumented and a hack, but sort of works
-       #'(void))]))
-
-(module+ test
-  (require rackunit (submod ".."))
-
-  (check-equal?
-    ((λ* (x : (Type 1)) (y : (∀* (x : (Type 1)) (Type 1))) (y x))
-     Type
-     (λ (x : (Type 1)) x))
-    Type)
-
-  (check-equal?
-    ((λ* (x : (Type 1)) (y : (→* (Type 1) (Type 1))) (y x))
-     Type
-     (λ (x : (Type 1)) x))
-    Type)
-
-  (check-equal?
-    ((λ* (x : (Type 1)) (y : (→ (Type 1) (Type 1))) (y x))
-     Type
-     (λ (x : (Type 1)) x))
-    Type))