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.

.gitignore

@@ -0,0 +1,5 @@
+*~
+\#*
+.\#*
+.DS_Store
+compiled

LICENSE

@@ -0,0 +1,10 @@
+Copyright © 2015, William J. Bowman <wjb@williamjbowman.com>
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:
+
+1. Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
+
+2. Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

README.md

@@ -1,9 +1,8 @@
 cur
 ===
 
-CIC under Racket. A language with static dependent-types and dynamic
-types, type annotations and parentheses, theorem proving and
-meta-programming.
+A language with static dependent-types and dynamic types, type
+annotations and parentheses, theorem proving and meta-programming.
 
 ```
 Noun
@@ -13,23 +12,83 @@ cur (plural curs)
 2. (archaic) A detestable person.
 ```
 
+Disclaimer
+==========
+Cur is currently under active hackery and is not fit for use for any
+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
 ===============
 
-Requires redex-lib version 1.6 if you want answer in a reasonable amount
-of time. Otherwise, the type-checker may require exponential time
-or worse.
+Easy mode:
+Install cur via `raco pkg install cur`.
 
-Open up `stlc.rkt` to see an example of what advanced meta-programming can let you do.
+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.
 
-Open up `oll.rkt` to see the implementation of the meta-programs used to
-enable `stlc.rkt`, including the parsers for BNF syntax and inference rule
-syntax, and Coq and LaTeX generators.
 
-Open up `proofs-for-free.rkt` to see an implementation of the
+Try it out: open up DrRacket and put the following in the definition area:
+
+```racket
+#lang cur
+(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:
+```racket
+(sub1 (s (s z)))
+```
+
+Don't like parenthesis? Use Cur with sweet-expressions:
+```racket
+#lang sweet-exp cur
+require
+ cur/stdlib/sugar
+ cur/stdlib/bool
+ cur/stdlib/nat
+
+if true
+   false
+   true
+
+define + plus
+
+{z + s(z)}
+```
+
+See the docs: `raco docs cur`.
+
+Going further
+=============
+
+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 anything in `stdlib/` to see some standard dependent-type
+Open up `cur-lib/cur/stdlib/tactics` to see one way to implement tactics in Cur.
+
+Open up anything in `cur-lib/cur/stdlib/` to see some standard dependent-type
 formalisms.
 
-Open up `redex-curnel.rkt` to see the entire "trusted" 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

@@ -0,0 +1,48 @@
+#lang scribble/manual
+@(require
+   "scribblings/defs.rkt"
+   racket/function)
+
+@title[#:style '(toc)]{Cur}
+@author[@author+email["William J. Bowman" "wjb@williamjbowman.com"]]
+
+@defmodule[cur #:lang]
+
+The language @racketmodname[cur] is a dependently-typed language that arbitrary Racket meta-programs
+can manipulate.
+The core language of @racketmodname[cur] is essentially TT.
+The trusted core provides nothing beyond this language.
+However, untrusted code provides, via Racket meta-programming, features such as modules, top-level
+definitions, multi-arity functions, implicit partial application, syntax notations, a tactic DSL,
+interactive tactics, and a programming language meta-theory DSL.
+These features run at compile time and generate @tech{curnel forms}, forms in the core language,
+which are type-checked before they are run.
+
+Arbitrary @racketmodname[racket] code can run at @gtech{phases} higher than 0, but
+@racketmodname[racket] code at @gtech{phase} 0 is unsupported and should result in a syntax error.
+The language @racketmodname[cur] exports everything in @racketmodname[racket],
+@racketmodname[racket/syntax], and @racketmodname[syntax/parse] at @gtech{phase} 1.
+
+The language @racketmodname[cur] provides reflection features to equip users with the tools necessary
+to write advanced meta-programs.
+These features in includes compile-time functions for type-checking, performing naïve type inference,
+deciding equivalence between @racketmodname[cur] terms, expanding macros in @racketmodname[cur] forms,
+and evaluating @racketmodname[cur] forms at compile-time.
+Programmers can use these reflection feature with little fear, as the resulting @tech{curnel forms}
+will always be type-checked prior to running.
+
+The @tech{curnel forms} are provided by the trusted core of the language.
+The reflection forms and procedures are provided by mostly untrusted, but privileged, code.
+These features require knowledge of and manipulation of the language implementation and could not be
+implemented by a user via a library.
+Everything else in @racketmodname[cur] is provided by untrusted user-land code---code that any user
+(with sufficient meta-programming expertise) could write and ship as a library.
+
+@todo{Some repetition}
+
+@local-table-of-contents[]
+
+@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

@@ -0,0 +1,224 @@
+#lang scribble/manual
+@(require "defs.rkt")
+
+@title{Olly: Ott-like 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 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.
+
+@defform[(define-language name
+           maybe-vars
+           maybe-output-coq
+           maybe-output-latex
+           (nt-name (nt-metavar ...) maybe-bnfdef non-terminal-def ...) ...)
+         #:grammar
+         [(maybe-vars
+            (code:line)
+            (code:line #:vars (nt-metavar ...)))
+         (maybe-output-coq
+            (code:line)
+            (code:line #:output-coq coq-filename))
+         (maybe-output-latex
+            (code:line)
+            (code:line #:output-latex latex-filename))
+         (maybe-bnfdef
+            (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
+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].
+
+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 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
+the language definitions to the @racket[coq-filename], overwriting the file.
+
+If @racket[#:output-latex] is given, it should be a string representing a
+filename. The form @racket[define-language] will output Latex versions of
+the language definitions to the @racket[latex-filename], overwriting the file.
+
+
+Example:
+
+@racketblock[
+(define-language stlc
+  #:vars (x)
+  #:output-coq "stlc.v"
+  #: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 (#:bind x : A) e) (cons e e)
+                  (let (#:bind x #:bind x) = e in e)))
+]
+
+This example is equivalent to
+
+@racketblock[
+(data stlc-val : Type
+  (stlc-true : stlc-val)
+  (stlc-false : stlc-val)
+  (stlc-unit : stlc-val))
+
+(data stlc-type : Type
+  (stlc-boolty : stlc-type)
+  (stlc-unitty : stlc-type)
+  (stlc--> : (forall (x : stlc-type) (forall (y : stlc-type) stlc-type)))
+  (stlc-* : (forall (x : stlc-type) (forall (y : stlc-type) stlc-type))))
+
+(data stlc-term : 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-cons : (forall (x : stlc-term) (forall (y : 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/tests/stlc]}
+}
+
+@defform[(define-relation (name args ...)
+          maybe-output-coq
+          maybe-output-latex
+          [premises ...
+           horizontal-line name
+           conclusion]
+          ...)
+         #:grammar
+         [(maybe-output-coq
+            (code:line)
+            (code:line #:output-coq coq-filename))
+         (maybe-output-latex
+            (code:line)
+            (code:line #:output-latex latex-filename))]]{
+
+Provides a notation for defining inductively defined relations similar
+to the @racket[define-judgment-form] form Redex. Rather than attempt to
+explain the syntax in detail, here is an example:
+
+@racketblock[
+(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 : 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)]
+
+  [(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)
+   (has-type g e1 (stlc-* t1 t2))
+   (has-type (extend-gamma (extend-gamma g t1) t2) e2 t)
+   ---------------------- T-Let
+   (has-type g (stlc-let e1 e2) t)]
+
+  [(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 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)])]
+
+This example is equivalent to:
+
+@racketblock[
+(data has-type : (forall (x : Gamma)
+                   (forall (y : stlc-term)
+                     (forall (z : stlc-type)
+                       Type)))
+  (T-Unit : (forall (g : Gamma)
+              (has-type
+                g
+                (stlc-val->stlc-term stlc-unit)
+                stlc-unitty)))
+  ....)]
+}
+
+@todo{Need a Scribble library for defining Cur/Racket things in the same
+library in a nice way.}
+
+@defform[(generate-coq maybe-file maybe-exists expr)
+         #:grammar
+         [(maybe-file
+            (code:line)
+            (code:line #:file filename))
+          (maybe-exists
+            (code:line)
+            (code:line #:exists flag))]]{
+A Racket form; translates the Cur expression @racket[expr] to Coq code
+and outputs it to @racket[current-output-port], or to @racket[filename]
+if @racket[filename] is provided. If the file already exists, uses
+@racket[flag] to figure out what to do, defaulting to @racket['error].
+}
+

cur-doc/cur/scribblings/reflection.scrbl

@@ -0,0 +1,112 @@
+#lang scribble/manual
+
+@(require
+   "defs.rkt"
+   scribble/eval
+   (for-label (only-in racket local-expand)))
+
+@title{Reflection}
+To support the addition of new user-defined language features, @racketmodname[cur] provides access to
+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.
+
+@(define curnel-eval (curnel-sandbox "(require cur/stdlib/bool cur/stdlib/nat)"))
+
+@defproc[(cur-expand [syn syntax?] [id identifier?] ...)
+         syntax?]{
+Expands the Cur term @racket[syn] until the expansion reaches a either @tech{Curnel form} or one of
+the identifiers @racket[id]. See also @racket[local-expand].
+
+@todo{Figure out how to get evaluator to pretend to be at phase 1 so these examples work properly.}
+
+@margin-note{The examples in this file do not currently run in the REPL, but should work if used at
+phase 1 in Cur.}
+
+@examples[
+(eval:alts (define-syntax-rule (computed-type _) Type) (void))
+(eval:alts (cur-expand #'(λ (x : (computed-type bla)) x))
+           (eval:result @racket[#'(λ (x : Type) x)] "" ""))
+]
+}
+
+@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 (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[(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 (cur-type-check? #'(λ (x : Type) x))
+           (eval:result @racket[#t] "" ""))
+(eval:alts (cur-type-check? #'Type)
+           (eval:result @racket[#t] "" ""))
+(eval:alts (cur-type-check? #'x)
+           (eval:result @racket[#f] "" ""))
+]
+}
+
+@defproc[(cur-normalize [syn syntax?])
+         syntax?]{
+Runs the Cur term @racket[syn] to a value.
+
+@examples[
+(eval:alts (cur-normalize #'((λ (x : Type) x) Bool))
+           (eval:result @racket[#'Bool] "" ""))
+(eval:alts (cur-normalize #'(sub1 (s (s z))))
+           (eval:result @racket[#'(s z)] "" ""))
+]
+}
+
+@defproc[(cur-step [syn syntax?])
+         syntax?]{
+Runs the Cur term @racket[syn] for one step.
+
+@examples[
+(eval:alts (cur-step #'((λ (x : Type) x) Bool))
+           (eval:result @racket[#'Bool] "" ""))
+(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)))] "" ""))
+]
+}
+
+@defproc[(cur-equal? [e1 syntax?] [e2 syntax?])
+         boolean?]{
+Returns @racket[#t] if the Cur terms @racket[e1] and @racket[e2] and equivalent according to
+equal modulo α and β-equivalence.
+@examples[
+
+
+(eval:alts (cur-equal? #'(λ (a : Type) a) #'(λ (b : Type) b))
+           (eval:result @racket[#t] "" ""))
+(eval:alts (cur-equal? #'((λ (a : Type) a) Bool) #'Bool)
+           (eval:result @racket[#t] "" ""))
+(eval:alts (cur-equal? #'(λ (a : Type) (sub1 (s z))) #'(λ (a : Type) z))
+           (eval:result @racket[#f] "" ""))
+]
+}
+
+
+@defproc[(cur->datum [s syntax?])
+         (or/c symbol? list?)]{
+Converts @racket[s] to a datum representation of the @tech{curnel form}, after expansion.
+@examples[
+
+
+(eval:alts (cur->datum #'(λ (a : Type) a))
+           (eval:result @racket['(λ (a : (Unv 0) a))] "" ""))
+]
+}

cur-doc/cur/scribblings/stdlib.scrbl

@@ -0,0 +1,16 @@
+#lang scribble/manual
+@(require
+   "defs.rkt")
+
+@title[#:style '(toc)]{Standard Library}
+Cur has a small standard library, primary for demonstration purposes.
+
+@local-table-of-contents[]
+
+@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

@@ -0,0 +1,223 @@
+#lang scribble/manual
+
+@(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]
+
+@defform*[((define-tactic (name id ... id-ps))
+           (define-tactic name procedure-expr))]{
+Defines a new @tech{tactic}, at @gtech{phase} 1. A @deftech{tactic} is a Racket function from
+@tech{proof state} to @tech{proof state} that runs at @gtech{phase} 1. A @tech{tactic} takes any
+number of arguments, plus the @tech{proof state}. The @tech{proof state} must be the final argument of
+the tactic.
+
+@examples[#:eval curnel-eval
+(define-tactic (do-nothing ps)
+  ps)
+(define-tactic (switch-goal i ps)
+  (struct-copy proof-state ps
+    [current-goal i]))
+]
+}
+
+@defproc[(proof? [p any/c])
+         boolean?]{
+Returns @racket[#t] if @racket[p] is a proof, and @racket[#f] otherwise.
+A @deftech{proof} is either a Cur term as a syntax object, or a procedure expecting a proof to plug
+into the holes of the existing partial proof.
+}
+
+@defproc[(complete-proof? [p any/c])
+         boolean?]{
+Returns @racket[#t] is the proof @racket[p] has no holes, i.e., is a syntax object, and @racket[#f]
+otherwise.
+}
+
+@defproc[(new-proof)
+         proof?]{
+Returns an empty partial @tech{proof}, i.e., the identity function.
+}
+
+@defstruct[proof-state ([env dict?]
+                        [goals dict?]
+                        [current-goal natural-number/c]
+                        [proof (or/c syntax? procedure?)]
+                        [theorem syntax?])]{
+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 @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 @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 @tech{theorem} to be proved.
+}
+
+@defproc[(new-proof-state [prop syntax?])
+         proof-state?]{
+Returns a @racket[proof-state?] initialized with an empty environment, the list of goals initialized with
+@racket[prop], the current-goal set to @racket[0], an empty proof via @racket[(new-proof)], and the
+theorem set to @racket[prop].
+}
+
+@defproc[(proof-state-proof-complete? [ps proof-state?])
+         boolean?]{
+Returns @racket[#t] is the proof of the @racket[proof-state?] @racket[ps] is a
+@racket[complete-proof?], and @racket[#f] otherwise.
+}
+
+@defproc[(proof-state-goal-ref [ps proof-sate?] [i natural-number/c])
+         syntax?]{
+Returns the @racket[i]th @tech{goal} from the proof state @racket[ps].
+}
+
+@defproc[(proof-state-current-goal-ref [ps proof-state?])
+         syntax?]{
+Returns the @tech{goal} using the index from
+@racket[(proof-state-current-goal ps)].
+}
+
+@defproc[(proof-state-env-ref [ps proof-state?] [name symbol?])
+         syntax?]{
+Returns the type of the assumption @racket[name] in the local
+environment of @racket[ps].
+}
+
+@defproc[(proof-state-env-ref-by-type [ps proof-state?] [type syntax?])
+         (or/c symbol? #f)]{
+Returns the name of the assumption of type @racket[type] from the local
+environment of @racket[ps], or @racket[#f] is no
+assumption with @racket[type] exists.
+}
+
+@defproc[(proof-state-extend-env [ps proof-state?]
+                                 [name (or/c symbol?  identifier?)]
+                                 [type syntax?])
+         proof-state?]{
+Returns a proof state with the local environment of
+@racket[ps] updated to include the assumption @racket[name] of type
+@racket[type].
+}
+
+@defproc[(proof-state-current-goal-set [ps proof-state?]
+                                       [goal syntax?])
+         proof-state?]{
+Returns a proof state with the current goal in the goals list of
+@racket[ps] changed to @racket[goal].
+}
+
+@defproc[(proof-state-fill-proof-hole [ps proof-state?] [pf proof?])
+         proof-state?]{
+Returns a proof state with the current holes of the proof filled with
+@racket[pf].
+}
+
+@defproc[(proof-state-extend-proof-context [ps proof-state?]
+                                           [ctxt procedure?])
+         proof-state?]{
+Updates the proof in @racket[ps] by playing the current proof inside the
+holes of @racket[ctxt].
+}
+
+@defproc[(print-proof-state [ps proof-state?])
+         void?]{
+Pretty-prints @racket[ps] to the @racket[current-output-port].
+}
+
+@defproc[(lookup-tactic [name (or/c symbol? identifier?)])
+         procedure?]{
+Returns the tactic defined with name @racket[name]. Only works when the
+tactic is defined and a theorem has been defined but not proved.
+}
+
+@defform[(define-theorem name prop)]{
+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 ...) ...)]{
+Proves the theorem previously defined with @racket[define-theorem].  Currently, this proof is not
+saved anywhere, only checked against the most recent theorem defined via @racket[define-theorem].
+
+Note that the proof state is implicitly given to each call by @racket[proof] and should not appear as
+an explicit argument.
+
+@examples[#:eval curnel-eval
+(define-theorem a-silly-theorem (forall (x : Nat) Nat))
+(proof (intro x) (by-assumption))
+
+(define-theorem falseo (forall (x : Type) x))
+(eval:alts (proof (interactive)) (void))
+]
+}
+
+@todo{Examples, better documentation (e.g. don't say "returns a proof state"; the signature says so)}
+
+@section{Standard Tactics}
+The tactic system includes several standard tactics.
+
+@defmodule[cur/stdlib/tactics/standard]
+
+@defproc[(intro [name identifier?] [ps proof-state?])
+         proof-state?]{
+Matches when the current goal has the form @racket[(forall (id : type-expr) body-expr)], introducing
+the assumption @racket[id : type-expr] into the local environment of @racket[ps].
+}
+
+@defproc[(by-assumption [ps proof-state?])
+         proof-state?]{
+Matches with the current goal has a type that matches an assumption in the local environment of
+@racket[ps]. Completes the goal.
+}
+
+@defproc[(obvious [ps proof-state?])
+         proof-state?]{
+Attempts to prove the current goal by doing the obvious thing.
+}
+
+@defproc[(restart [ps proof-state?])
+         proof-state?]{
+Resets @racket[ps] to its state when the proof began. Clears the proof and goals, reinitializing the
+goals to the original theorem.
+}
+
+@defproc[(print [ps proof-state?])
+         proof-state?]{
+Prints @racket[ps], returning it unmodified.
+}
+
+@defproc[(forget [x identifier?] [ps proof-state?])
+         proof-state?]{
+Removes the assumption @racket[x] from the local environment of @racket[ps].
+}
+
+@section{Interactive Tactic}
+In Cur, interactivity is just a user-defined tactic.
+
+@defproc[(interactive [ps proof-state?])
+         proof-state?]{
+Starts a REPL that prints @racket[ps], reads a tactic (as @racket[proof] would), evaluates the
+tactic, and repeats. To quit, use @racket[(quit)].
+}
+
+@section{SarTactic (Sarcastic Tactics)}
+@defmodule[cur/stdlib/tactics/sartactic]
+
+The SarTactic library provides amusing wrappers around the standard tactics. This library exists
+mostly for the author's own amusement, and to ensure the extensibility of the tactic system.
+
+It defines the same tactics as @racketmodname[cur/stdlib/tactics/standard], but each tactics will
+insult the user, and will only work some of the time.

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

@@ -0,0 +1,489 @@
+#lang racket/base
+;; This module just provide module language sugar over the redex model.
+
+(require
+  (except-in "redex-core.rkt" apply)
+  redex/reduction-semantics
+  racket/provide-syntax
+  (for-syntax
+    (except-in racket import)
+    syntax/parse
+    racket/syntax
+    (except-in racket/provide-transform export)
+    racket/require-transform
+    (except-in "redex-core.rkt" apply)
+    redex/reduction-semantics))
+(provide
+  ;; Basic syntax
+  for-syntax
+  only-in
+  except-in
+  all-defined-out
+  rename-in
+  rename-out
+  prefix-out
+  prefix-in
+  submod
+  #%module-begin
+  (rename-out
+    [dep-module+ module+]
+    [dep-provide provide]
+    [dep-require require]
+
+    [dep-lambda λ]
+    [dep-app #%app]
+
+    [dep-forall Π]
+
+    [dep-inductive data]
+
+    [dep-elim elim]
+
+    [dep-top #%top]
+    [dep-top-interaction #%top-interaction]
+
+    ;      [dep-datum #%datum]
+    [dep-define define]
+    [dep-void void])
+  begin
+  Type
+  ;; DYI syntax extension
+  define-syntax
+  begin-for-syntax
+  define-for-syntax
+  syntax-case
+  syntax-rules
+  define-syntax-rule
+  (for-syntax
+   (all-from-out syntax/parse)
+   (all-from-out racket)
+   (all-from-out racket/syntax)
+    cur->datum
+    cur-expand
+    cur-type-infer
+    cur-type-check?
+    cur-normalize
+    cur-step
+    cur-equal?))
+
+(begin-for-syntax
+  ;; 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 term environment ~s" x))
+        x)))
+
+  (define delta
+    (make-parameter
+      (term ∅)
+      (lambda (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 (Γ-set ,(env) ,x ,t)))
+
+  (define (extend-Γ/term! env x t) (env (extend-Γ/term env x t)))
+
+  (define (extend-Γ/syn env x t)
+    (extend-Γ/term env (syntax->datum x) (cur->datum t)))
+
+  (define (extend-Γ/syn! env x t) (env (extend-Γ/syn env x t)))
+
+  (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-Δ/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 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)))))
+
+  (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 ,(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 ,(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)))
+  (define (disarm syn) (syntax-disarm syn orig-insp))
+
+  ;; Locally expand everything down to core forms.
+  (define (core-expand syn)
+    (disarm
+      (local-expand
+        syn
+        'expression
+        (append (syntax-e #'(term reduce subst-all dep-top #%app λ Π elim Unv #%datum void))))))
+
+  ;; Only type-check at the top-level, to prevent exponential
+  ;; type-checking. Redex is expensive enough.
+  (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)
+            #:literals (term reduce #%app subst-all)
+            #:datum-literals (elim Π λ : Unv)
+            [x:id (syntax->datum #'x)]
+            [(subst-all e _ _) (syntax->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
+            ;; Maybe make a syntax class for the binders, core forms,
+            ;; etc.
+            [(b:id (x:id : t) e)
+             (let* ([x (syntax->datum #'x)]
+                    [t (cur->datum #'t)]
+                    [e (parameterize ([gamma (extend-Γ/term gamma x t)])
+                         (cur->datum #'e))])
+               (term (,(syntax->datum #'b) (,x : ,t) ,e)))]
+            [(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 (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)
+    (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 ,(delta) ,(subst-bindings (cur->datum syn)))))
+
+  (define (syntax->curnel-syntax syn)
+    (quasisyntax/loc
+      syn
+      ;; 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 (cur-normalize syn)
+    (datum->cur
+      syn
+      (eval-cur syn)))
+
+  (define (cur-step syn)
+    (datum->cur
+      syn
+      (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 (convert ,(delta) ,(gamma) ,(eval-cur e1) ,(eval-cur e2))) #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 (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
+  ;; expanded until expansion reaches a Curnel form, or one of the
+  ;; identifiers in ls.
+  (define (cur-expand syn . ls)
+    (disarm
+      (local-expand
+        syn
+        'expression
+        (append (syntax-e #'(Type dep-inductive dep-lambda dep-app dep-elim dep-forall dep-top))
+                ls)))))
+
+;; -----------------------------------------------------------------
+;; Require/provide macros
+
+#| TODO NB XXX
+ | This is code some of the most hacky awful code I've ever written. But it works. ish
+ |#
+(begin-for-syntax
+  (define envs (list #'(void)))
+
+  (define (cur-identifier-bound? id)
+    (let ([x (syntax->datum id)])
+      (and (x? 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)
+               (apply append (map (lambda (e) (expand-export e modes))
+                                  (syntax->list syn))))))
+(define-syntax extend-env-and-provide
+  (make-provide-transformer
+    (lambda (syn modes)
+      (syntax-case syn ()
+        [(_ e ...)
+         (let-values ([(cur ~cur) (filter-cur-exports #'(e ...) modes)])
+           #| TODO: Ignoring the built envs for now
+           (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 #'delta)])
+             #`(extend-env/term! #,env #,(export-out-sym e) #,t))))
+           |#
+        ~cur)]))))
+
+(define-syntax (export-envs syn)
+  (syntax-case syn ()
+    [(_ gamma-out delta-out bind-out)
+     (begin
+       #`(begin-for-syntax
+          (define gamma-out (term #,(gamma)))
+          (define delta-out (term #,(delta)))
+          (define bind-out '#,(bind-subst))))]))
+
+;; TODO: This can only handle a single provide form, otherwise generates multiple *-out
+(define-syntax (dep-provide syn)
+  (syntax-case syn ()
+    [(_ e ...)
+     (begin
+       #| TODO NB:
+        | 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 ; delta.
+       (syntax-local-lift-module-end-declaration
+         #`(export-envs gamma-out delta-out bind-out))
+       #`(provide (extend-env-and-provide e ...)
+                  (for-syntax gamma-out delta-out bind-out)))]))
+(begin-for-syntax
+  (define out-gammas #`())
+  (define out-deltas #`())
+  (define out-binds #`())
+  (define gn 0)
+  (define sn 0)
+  (define bn 0)
+  (define (filter-cur-imports syn)
+    (for/fold ([imports '()]
+               [sources '()])
+              ([req-spec (syntax->list syn)])
+      (let-values ([(more-imports more-sources) (expand-import req-spec)])
+        (values (for/fold ([imports imports])
+                          ([imp more-imports])
+                  (cond
+                    [(equal? (import-src-sym imp) 'gamma-out)
+                     (let ([new-id (format-id (import-orig-stx imp)
+                                              "gamma-out~a" gn)])
+                       ;; TODO: Fewer set!s
+                       ;; TODO: Do not DIY gensym
+                       (set! gn (add1 gn))
+                       (set! out-gammas
+                             #`(#,@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) 'delta-out)
+                     (let ([new-id (format-id (import-orig-stx imp)
+                                              "delta-out~a" sn)])
+                       ;; TODO: Fewer set!s
+                       ;; TODO: Do not DIY gensym
+                       (set! sn (add1 sn))
+                       (set! out-deltas
+                             #`(#,@out-deltas (delta (term (Δ-union
+                                                             ,(delta)
+                                                             ,#,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) 'bind-out)
+                     (let ([new-id (format-id (import-orig-stx imp)
+                                              "bind-out~a" bn)])
+                       ;; TODO: Fewer set!s
+                       ;; TODO: Do not DIY gensym
+                       (set! bn (add1 bn))
+                       (set! out-binds
+                             #`(#,@out-binds (bind-subst (list (append
+                                                                 (first #,new-id)
+                                                                 (first (bind-subst)))
+                                                               (append
+                                                                 (second #,new-id)
+                                                                 (second (bind-subst)))))))
+                       (cons (struct-copy import imp [local-id new-id])
+                             imports))]
+                    [else (cons imp imports)]))
+                (append sources more-sources))))))
+
+(define-syntax extend-env-and-require
+  (make-require-transformer
+    (lambda (syn)
+      (syntax-case syn ()
+        [(_ e ...) (filter-cur-imports #'(e ...))]))))
+
+;; 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-deltas
+                             #,@out-binds)]))
+
+(define-syntax (dep-require syn)
+  (syntax-case syn ()
+    [(_ e ...)
+     #`(begin
+         (require (extend-env-and-require e ...))
+         (import-envs))]))
+
+(define-syntax (dep-module+ syn)
+  (syntax-case syn ()
+    [(_ name body ...)
+     #`(module+ name
+         (begin-for-syntax
+           (gamma (term #,(gamma)))
+           (delta (term #,(delta)))
+           (bind-subst '#,(bind-subst)))
+         body ...)]))
+
+;; -----------------------------------------------------------------
+;; Core wrapper macros
+;;
+;; TODO: Can these be simplified further?
+(define-syntax (dep-lambda syn)
+  (syntax-parse syn
+    #:datum-literals (:)
+    [(_ (x:id : t) e)
+     (syntax->curnel-syntax
+       (quasisyntax/loc syn (λ (x : t) e)))]))
+
+(define-syntax (dep-app syn)
+  (syntax-parse syn
+    [(_ e1:expr e2:expr)
+     (syntax->curnel-syntax
+       (quasisyntax/loc syn (#%app e1 e2)))]))
+
+(define-syntax (dep-forall syn)
+  (syntax-parse syn
+    #:datum-literals (:)
+    [(_ (x:id : t) e)
+     (syntax->curnel-syntax
+       (quasisyntax/loc syn (Π (x : t) e)))]))
+
+(define-syntax (Type syn)
+  (syntax-parse syn
+    [(_ i:nat)
+     (syntax->curnel-syntax
+       (quasisyntax/loc syn (Unv i)))]
+    [_ (quasisyntax/loc syn (Type 0))]))
+
+(define-syntax (dep-inductive syn)
+  (syntax-parse syn
+    #:datum-literals (:)
+    [(_ i:id : ti (x1:id : t1) ...)
+     (begin
+       (extend-Δ/syn! delta #'i #'ti #'((x1 : t1) ...))
+       #'(void))]))
+
+(define-syntax (dep-elim syn)
+  (syntax-parse syn
+    [(_ D:id motive (i ...) (m ...) e)
+     (syntax->curnel-syntax
+       (quasisyntax/loc syn (elim D motive (i ...) (m ...) e)))]))
+
+(define-syntax-rule (dep-void) (void))
+
+;; TODO: Not sure if this is the correct behavior for #%top
+(define-syntax (dep-top syn)
+  (syntax-case syn ()
+    [(_ . id)
+     ;; TODO NB FIXME: HACKS HACKS HACKS
+     (let ([t (core-expand #'id)])
+       (if (equal? (syntax->datum t) '(void))
+           #'(void)
+           (syntax->curnel-syntax t)))]))
+
+(define-syntax (dep-top-interaction syn)
+  (syntax-case syn ()
+    [(_ . form)
+     (begin
+       ;; TODO NB FIXME: HACKS
+       #`(begin
+           (export-envs gamma-out delta-out bind-out)
+           (begin-for-syntax
+             (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)
+  (syntax-parse syn
+    [(_ 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

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

cur-lib/cur/main.rkt

@@ -0,0 +1,31 @@
+#lang racket/base
+
+(module extra racket
+  (require
+    racket/syntax
+    syntax/parse
+    (for-template
+      (only-in "curnel/redex-lang.rkt"
+       cur-expand)))
+
+  (provide cur-match)
+
+  (define-syntax (cur-match syn)
+    (syntax-case syn ()
+      [(_ syn [pattern body] ...)
+       #'(syntax-parse (cur-expand syn)
+           [pattern body] ...)])))
+
+(require
+  (rename-in "curnel/redex-lang.rkt" [provide -provide])
+  (only-in racket/base eof)
+  (for-syntax 'extra)
+  'extra)
+(provide
+  (rename-out [-provide provide])
+  (for-syntax (all-from-out 'extra))
+  (except-out
+    (all-from-out
+     'extra
+     "curnel/redex-lang.rkt")
+    -provide))

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

@@ -0,0 +1,236 @@
+#lang s-exp "../../main.rkt"
+(require
+  (for-syntax racket/syntax))
+(provide
+  proof
+  define-theorem
+  define-tactic
+
+  (for-syntax
+    proof-state
+    proof-state-env
+    proof-state-goals
+    proof-state-current-goal
+    proof-state-proof
+    proof-state-theorem
+    new-proof
+    proof?
+    complete-proof?
+    new-proof-state
+    proof-state-proof-complete?
+    proof-state-goal-ref
+    proof-state-current-goal-ref
+    proof-state-current-goal-set
+    proof-state-env-ref
+    proof-state-env-ref-by-type
+    proof-state-extend-env
+    proof-state-fill-proof-hole
+    proof-state-extend-proof-context
+    current-hole-pretty-symbol
+    print-proof-state
+    lookup-tactic))
+
+#| NB:
+ | The design of Cur currently seems to prevent intermediate type-checking
+ | during a tactic-based proof, unless I were to either reimplement the
+ | type-checker or extend it with a notion of holes.
+ | TODO: A noation of holes may be useful in general.
+ |#
+
+#| NB:
+ | Per below, note that Cur already has contexts. The issue with
+ | type-checking intermediate results has to do with the fact that Cur
+ | contexts are not exposed properly, nor is type-checking defined on
+ | them.
+ |#
+
+;; ------------------------------------------------------------------------
+;;; Proof state interface
+
+#|
+ | A Goal, aka, Theorem is a syntax object representing a Cur proposition (type).
+ |
+ | A Expr is a syntax object representing Cur expression (term).
+ |
+ | A Hole is a procedure of type
+ |
+ | A Proof is (Either Ctxt Expr)
+ |
+ | A Ctxt is a procedure Proof -> Proof representing a Cur expression
+ | with a hole.
+ |
+ | A Environment is a map from Symbol to Theorems.
+ |
+ | A Proof-State is a struct containing:
+ |   env: An Environment, the assumptions introduced during a tactic
+ |        script.
+ |   goals: A map from Natural to Goal, the goals necessary to finish
+ |          this proof
+ |   current-goal: A Natural, the index into goals of the current Goal
+ |                 to be proved.
+ |   proof: A Proof, representing the proof so far. when the proof is
+ |          an Expr, the proof is complete.
+ |   theorem: A Theorem, the original statement of the theorem this proof is
+ |            attempting to prove.
+ |#
+;;; TODO: I'm partially implementing lens here.
+;;; TODO: Interface is mildly inconsistent.
+(begin-for-syntax
+  (define new-proof values)
+
+  (define (proof? p)
+    (or (syntax? p) (procedure? p)))
+
+  (define (complete-proof? p)
+    (syntax? p))
+
+  (define-struct proof-state (env goals current-goal proof theorem))
+
+
+  (define (new-proof-state prop)
+    (proof-state
+      (make-immutable-hash)
+      (dict-set (make-immutable-hash) 0 prop)
+      0
+      new-proof
+      prop))
+
+  ;; Given a Proof-State, return #t if the current-proof is complete
+  ;; (i.e. is a Expr and not a Ctxt), #f otherwise.
+  (define (proof-state-proof-complete? ps) (complete-proof? (proof-state-proof ps)))
+
+  ;;; Extra accessors
+
+  ;; Return the goal with index i in proof-state-goals
+  (define (proof-state-goal-ref ps i)
+    (dict-ref (proof-state-goals ps) i))
+
+  ;; Return the current-goal from proof-state-goals
+  (define (proof-state-current-goal-ref ps)
+    (proof-state-goal-ref ps (proof-state-current-goal ps)))
+
+  ;; Return the theorem named by name in the local environment
+  (define (proof-state-env-ref ps name)
+    (dict-ref (proof-state-env ps) name))
+
+  ;; Return the name of an assumption with type thm, or #f.
+  (define (proof-state-env-ref-by-type ps thm)
+    (for/first ([(k v) (in-dict (proof-state-env ps))]
+                #:when (cur-equal? v thm))
+      k))
+
+  ;;; Functional updators
+
+  (define (maybe-syntax->symbol name)
+    (if (syntax? name)
+        (syntax->datum name)
+        name))
+
+  ;; Extend the local environment with a new assumption, name, of type thm. Name can be a syntax
+  ;; object or a symbol.
+  (define (proof-state-extend-env ps name thm)
+    (struct-copy proof-state ps
+      [env (dict-set (proof-state-env ps) (maybe-syntax->symbol name) thm)]))
+
+  ;; Updates the current-goal to pf
+  (define (proof-state-current-goal-set ps pf)
+    (struct-copy proof-state ps
+      [goals (dict-set (proof-state-goals ps) (proof-state-current-goal ps) pf)]))
+
+  ;; Fill the current proof hole with pf
+  (define (proof-state-fill-proof-hole ps pf)
+    ;; TODO: Check for proof completion?
+    ;; TODO: What about multiple holes?
+    (struct-copy proof-state ps
+      [proof ((proof-state-proof ps) pf)]))
+
+  ;; Place the current proof in the context ctxt.
+  (define (proof-state-extend-proof-context ps ctxt)
+    (struct-copy proof-state ps
+      [proof (ctxt (proof-state-proof ps))]))
+
+  ;; How to display a hole, for pretty printing.
+  (define current-hole-pretty-symbol (make-parameter 'hole))
+
+  ;; A pretty printer for proof-state
+  (define (print-proof-state ps)
+    (for ([(k v) (in-dict (proof-state-env ps))])
+      (printf "~n~a : ~a~n" k (syntax->datum v)))
+    (printf "--------------------------------~n")
+    (cond
+      [(proof-state-current-goal-ref ps)
+       =>
+       (lambda (x) (printf "~a~n~n" (syntax->datum x)))]
+      [else (printf "Goal complete!~n~n")])))
+
+;; -----------------------------------------------------------------------
+;;; Syntax for tactic-based proofs similar to Coq.
+
+#|
+ | A tactic is a phase 1 Racket function that manipulates the current proof state.
+ | Tactic : Any ... Proof-State -> Proof-State
+ |
+ | Examples:
+ |
+ | (define-tactic command-name function)
+ | (define-tactic (command-name args ... ps) body)
+ |#
+(define-syntax define-tactic (make-rename-transformer #'define-for-syntax))
+
+(begin-for-syntax
+  ;; Takes a symbol or syntax object naming a tactic, and returns the
+  ;; procedure for that tactic.
+  (define (lookup-tactic syn)
+    (eval
+      (if (syntax? syn)
+          ;; NB: Ensure eval gets the right environment
+          (datum->syntax (current-theorem) (syntax->datum syn))
+          syn))))
+
+(begin-for-syntax
+  ;; The current theorem; used internally to achieve a Coq-like notation
+  ;; for defining theorems and tactic-based proofs.
+  (define current-theorem (make-parameter #f)))
+
+;; Define a theorem, with similar semantics to Coq theorems in that you
+;; can define the theorem then define the proof next.
+(define-syntax (define-theorem syn)
+  (syntax-case syn ()
+    [(_ name prop)
+     (current-theorem (cur-expand #'prop))
+     #'(define name prop)]))
+
+;; Aliases for theorems.
+;; (define-syntax define-lemma (make-rename-transformer #'define-theorem))
+
+(begin-for-syntax
+  ;; Given a list of tactics and their arguments, run the tactic script
+  ;; on the current theorem, returning the proof if the proof is valid.
+  (define (run-tactic-script f* args*)
+    (unless (current-theorem)
+      (raise-syntax-error
+        'proof
+        "You can't use proof without a first using define-theorem"))
+    (let* ([t (current-theorem)]
+           [ps ;; Thread proof state through tactic calls, and eval
+               ;; at compile-time.
+               (for/fold ([ps (new-proof-state t)])
+                         ([f f*] [args args*])
+                 (apply (lookup-tactic f) (append args (list ps))))]
+           [pf (proof-state-proof ps)])
+      (unless (proof-state-proof-complete? ps)
+        (raise-syntax-error 'qed "Proof contains holes" (pf (current-hole-pretty-symbol))))
+      (unless (cur-type-check? pf t)
+        (raise-syntax-error 'qed "Invalid proof" pf t))
+      pf)))
+
+;; The proof macro starts a proof environment. Every proof should begin
+;; with it.
+;; TODO: uh should probably save the proof. Perhaps theorem should
+;; TODO: define something else, then proof should be bound to theorem name.
+(define-syntax (proof syn)
+  (syntax-parse syn
+    [(_ (f args* ...) ... (~optional (~literal qed)))
+     (run-tactic-script
+       (syntax->list #'(f ...))
+       (map syntax->list (syntax->list #'((args* ...) ...))))]))

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

@@ -0,0 +1,126 @@
+#lang s-exp "../../main.rkt"
+(require
+  "base.rkt"
+  (prefix-in basic: "standard.rkt")
+  (for-syntax racket/syntax))
+
+(provide
+  (for-syntax
+    intro
+    interactive))
+
+;;; SARCASTIC INTERACTIVE TACTICS
+
+(begin-for-syntax
+  (define jabs
+    (list
+      "I don't think you know what you're doing."
+      "Does this look right to *you*?"
+      "Prove it."))
+
+  (define (random-ref ls)
+    (list-ref ls (random (length ls))))
+
+  (define (random-jab) (random-ref jabs))
+  )
+
+(define-tactic (print ps)
+  (basic:print ps)
+  (displayln (random-jab))
+  ps)
+
+(begin-for-syntax
+  (define intro-jabs
+    (list
+      "What a clever name."
+      "How original."
+      "I'm sure that seems like a good idea to *you*."
+      "Why don't you just assume false while you're at it?")))
+
+(define-tactic (intro name ps)
+  (displayln (random-ref intro-jabs))
+  (newline)
+  (basic:intro name ps))
+
+(define-tactic (forget ps)
+  (displayln "Like hell.")
+  ps)
+(define-tactic by-assumption basic:by-assumption)
+
+(begin-for-syntax
+  (define restart-jabs
+    (list
+      "Hahahahahahahaha."
+      "Lawl."
+      "Why didn't you just do it right the first time?"
+      "Stupid human."
+      "I've been waiting for this.")))
+(define-tactic (restart ps)
+  (displayln (random-ref restart-jabs))
+  (basic:restart ps))
+
+(begin-for-syntax
+  (define denied-obvious-jabs
+    (list
+      "It's not obvious to me."
+      "You expect me to know this?"
+      "If it's so obvious then just finish the proof already."
+      "Maybe you should hire a grad student."))
+  (define accept-obvious-jabs
+    (list
+      "I wasn't going to say anything, but this was taking you forever."
+      "Finally."
+      "Let me show you how it's done."
+      "You're right, I am better at proving things than you are."
+      "Aw that was *sooo* tough...")))
+(define-tactic (obvious ps)
+  (if (< (random 10) 3)
+      (begin
+        (displayln (random-ref accept-obvious-jabs))
+        (newline)
+        (basic:obvious ps))
+      (begin
+        (displayln (random-ref denied-obvious-jabs))
+        (newline)
+        ps)))
+
+(begin-for-syntax
+  (define no-quit-jabs
+    (list
+      "Na."
+      "How about instead I just delete all of your work?"
+      "I don't think you're ready yet.")))
+(define-tactic (interactive ps)
+  (printf "Starting interactive tactic session. Prepare to be sassed:~n")
+  (printf "Type (quit) to quit.~n")
+  (let loop ([ps ps] [cmds '()])
+    (if (proof-state-proof-complete? ps)
+        (basic:print ps)
+        (print ps))
+    (let ([cmd (read-syntax)])
+      (newline)
+      (syntax-case cmd (quit)
+        [(quit)
+         (if (< (random 10) 4)
+             (begin
+               (printf "Don't forget this. It took you long enough:~n")
+               (pretty-print (reverse (map syntax->datum cmds)))
+               (newline)
+               ps)
+             (begin
+               (displayln (random-ref no-quit-jabs))
+               (loop ps cmds)))]
+        [(tactic arg ...)
+          (with-handlers (#;[exn:fail:contract?
+                            (lambda (e)
+                              (printf "tactic ~a expected different arguments.~n"
+                                (syntax->datum #'tactic))
+                              (loop ps cmds))]
+                          #;[exn:fail:syntax?
+                            (lambda (e)
+                              (printf "~a is not a tactic.~n"
+                                (syntax->datum #'tactic))
+                              (loop ps cmds))])
+            (loop (apply (lookup-tactic #'tactic)
+                    (append (syntax->list #'(arg ...)) (list ps)))
+                  (cons cmd cmds)))]))))

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

@@ -0,0 +1,100 @@
+#lang s-exp "../../main.rkt"
+(require
+  "base.rkt"
+  (for-syntax racket/syntax))
+
+(provide
+  (for-syntax
+    intro
+    obvious
+    restart
+    forget
+    print
+    by-assumption
+    interactive))
+
+#| TODO:
+ | Tactics should probably not error on failure. Perhaps Maybe monad, or list monad, or return proof
+ | state unmodified, or raise exception, or ...
+ |#
+(define-tactic (intro name ps)
+  (cur-match (proof-state-current-goal-ref ps)
+    [(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) #`(λ (#,name : P) #,x)))])
+       ps)]
+    [_ (error 'intro "Can only intro when current goal is of the form (∀ (x : P) body)")]))
+
+(define-tactic (by-assumption ps)
+  (cond
+    [(proof-state-env-ref-by-type ps (proof-state-current-goal-ref ps))
+     =>
+     (lambda (x)
+       (let* ([ps (proof-state-fill-proof-hole ps x)]
+              [ps (proof-state-current-goal-set ps #f)])
+         ps))]
+    [else (error 'by-assumption "Cannot find an assumption that matches the goal")]))
+
+;; TODO: requires more support from curnel
+#;(begin-for-syntax
+  (define (inductive? ps type)
+    ))
+
+;; Do the obvious thing
+(define-tactic (obvious ps)
+  (cur-match (proof-state-current-goal-ref ps)
+    [(forall (x : P) t)
+     (obvious (intro #'x ps))]
+    [t:expr
+     (cond
+       ;; TODO: This would be cleaner if I could say "try all these things and do whichever works".
+       [(proof-state-env-ref-by-type ps #'t) (by-assumption ps)]
+       ;[(inductive? ps #'t) (by-constructor ps)]
+       [else (error 'obvious "This is not all that obvious to me.")])]))
+
+(define-tactic (restart ps) (new-proof-state (proof-state-theorem ps)))
+
+(define-tactic (print ps) (print-proof-state ps) ps)
+
+(define-tactic (forget x ps)
+  (struct-copy proof-state ps
+    [env (dict-remove (syntax-e x) (proof-state-env ps))]))
+
+;; Interactive you say? Sure whatevs, DIY
+(define-tactic (interactive ps)
+  (printf "Starting interactive tactic session:~n")
+  (printf "Type (quit) to quit.~n")
+  (let loop ([ps ps] [cmds '()])
+    (print ps)
+    (let ([cmd (read-syntax)])
+      (syntax-case cmd (quit)
+        [(quit)
+         (begin
+           (printf "Your tactic script:~n")
+           ;; TODO: Using clever trickery, could problem write a version of interactive that actually
+           ;; modifies the file.
+           (pretty-print (reverse (map syntax->datum cmds)))
+           (newline)
+           ps)]
+        ;; TODO: Maybe use (read-eval-print-loop) and its
+        ;; TODO: config parameters.
+        [(tactic arg ...)
+          (with-handlers (#;[exn:fail:contract?
+                            (lambda (e)
+                              (printf "tactic ~a expected different arguments.~n"
+                                (syntax->datum #'tactic))
+                              (loop ps cmds))]
+                          #;[exn:fail:syntax?
+                            (lambda (e)
+                              (printf "~a is not a tactic.~n"
+                                (syntax->datum #'tactic))
+                              (loop ps cmds))])
+            (loop (apply (lookup-tactic #'tactic)
+                    (append (syntax->list #'(arg ...)) (list ps)))
+                  (cons cmd cmds)))]))))
+
+;; TODO:
+;; Open interactive REPL for tactic DSL; exit with QED command, which
+;; returns a QED script
+;(define-syntax interactive-proof)

cur-lib/cur/stdlib/typeclass.rkt

@@ -0,0 +1,73 @@
+#lang s-exp "../main.rkt"
+(require
+  "nat.rkt"
+  "bool.rkt"
+  "sugar.rkt"
+  (for-syntax
+    racket/syntax
+    racket/dict
+    racket/list))
+(provide (for-syntax typeclasses) typeclass impl)
+
+;;; NB: This module is extremely unhygienic.
+#| TODO:
+ | These typeclasses are kind of broken. There are no typeclass constraints so....
+ |#
+(begin-for-syntax
+  #| NB:
+   | Need this thing to be global w.r.t. the runtime, i.e., exist once
+   | and for all no matter how many things import typeclass, i.e., not
+   | local to this module.
+   |#
+  (define typeclasses (make-hash)))
+(define-syntax (typeclass syn)
+  (syntax-case syn (: Type)
+    [(_ (class (param : Type)) (name : type) ...)
+     #`(begin
+         #,@(for/list ([name (syntax->list #'(name ...))]
+                       [type (syntax->list #'(type ...))])
+              (dict-set!
+                (dict-ref! typeclasses (syntax->datum #'class) (make-hash))
+                (syntax->datum name)
+                #`(lambda (param : Type) #,type))
+              #| NB:
+               | Due to implementation below, methods on typeclass must dispatch on type of first
+               | argument. Also prevents currying/point-free style. Maybe type system hooks to get
+               | "type of current hole" would help? Related: tactics/base.rkt
+               |#
+              #`(define-syntax (#,name syn)
+                  (syntax-case syn ()
+                    [(_ arg args (... ...))
+                     #`(#,(format-id syn "~a-~a" '#,name (cur-type-infer #'arg))
+                        arg
+                        args (... ...))]))))]))
+
+(define-syntax (impl syn)
+  #| TODO:
+   | Need racket-like define so I can extract name/args/defs.
+   |#
+  (define (process-def def)
+    (syntax-case def (define)
+      [(define (name (a : t) ...) body ...)
+       (values (syntax->datum #'name) #'(lambda (a : t) ... body ...))]
+      [(define name body)
+       (values (syntax->datum #'name) #'body)]))
+  (syntax-case syn ()
+    [(_ (class param) defs ...)
+     #`(begin
+         #,@(for/list ([def (syntax->list #'(defs ...))])
+              (let-values ([(name body) (process-def def)])
+                (unless (cur-type-check?
+                          body
+                          #`(#,(dict-ref
+                                 (dict-ref typeclasses (syntax->datum #'class))
+                                 name)
+                             param))
+                  (raise-syntax-error
+                    'impl
+                    ;"Invalid implementation of typeclass ~a. Must have type ~a."
+                    "Invalid implementation of typeclass."
+                    #'class
+                    #'body))
+                #`(define #,(format-id syn "~a-~a" name #'param)
+                    #,body))))]))

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/example.rkt

@@ -1,11 +1,17 @@
-#lang s-exp "redex-curnel.rkt"
+#lang racket/base
+;; #lang s-exp "../cur.rkt"
+
+(error "Known bug: examples.rkt way out of date")
+#| TODO NB XXX This file is woefully out of date
 
 ;; Use racket libraries over your dependently typed code!?!?
 ;; TODO: actually, I'm not sure this should work quite as well as it
 ;; seems to with check-equal?
 (require rackunit)
-(require (only-in "redex-curnel.rkt" [#%app real-app]
-                  [define real-define]))
+(require
+  (only-in "../cur.rkt"
+    [#%app real-app]
+    [define real-define]))
 
 (define-syntax (#%app syn)
   (syntax-case syn ()
@@ -446,3 +452,4 @@
    (has-type g e2 t1)
    ---------------------- T-App
    (has-type g (app e1 e2) t2)])
+|#

examples/proofs-for-free.rkt

@@ -1,6 +1,12 @@
-#lang s-exp "redex-curnel.rkt"
-(require "stdlib/sugar.rkt" "stdlib/prop.rkt" racket/trace 
-         (for-syntax racket/syntax))
+#lang racket/base
+(error "Known bug: proofs-for-free.rkt way out of date")
+#| TODO NB XXX This file is woefully out of date
+#lang s-exp "../cur.rkt"
+(require
+  "../stdlib/sugar.rkt"
+  "../stdlib/prop.rkt"
+  racket/trace
+  (for-syntax racket/syntax))
 
 ;; ---------
 (begin-for-syntax
@@ -77,6 +83,7 @@
 (define (CPSf-relation (f1 : CPSf) (f2 : CPSf))
   ;; TODO: Fix run so I can simply use (run CPSf) to perform
   ;; substitution
+  #;(translate (run CPSf))
   (translate (forall* (ans : Type) (k : (-> X ans)) ans)))
 #;(module+ test
   (require rackunit)
@@ -104,3 +111,4 @@
     ))
 
 #;(paramCPSf f X X rel k k)
+|#

oll.rkt

@@ -1,400 +0,0 @@
-#lang s-exp "redex-curnel.rkt"
-;; OLL: The OTT-Like Library
-;; TODO: Add latex extraction
-;; TODO: Automagically create a parser from bnf grammar
-(require "stdlib/sugar.rkt" "stdlib/nat.rkt" racket/trace)
-
-(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
-              (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 (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* v1
-    [(avar (n1 : nat))
-     (case* v2
-       [(avar (n2 : nat))
-        (nat-equal? n1 n2)])]))
-
-;; 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 case 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)" (syntax-e #'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"]
-       [(case e (ec eb) ...)
-        (format "(match ~a with~n~aend)"
-                (output-coq #'e)
-                (for/fold ([strs ""])
-                          ([con   (syntax->list #'(ec ...))]
-                           [body  (syntax->list #'(eb ...))])
-                  (let* ([ids (generate-temporaries (constructor-args con))]
-                         [names (map (compose ~a syntax->datum) ids)])
-                    (format "~a| (~a) => ~a~n" strs
-                      (for/fold ([str (output-coq con)])
-                                ([n names])
-                        (format "~a ~a" str n))
-                      (for/fold ([body (output-coq body)])
-                                ([n names])
-                        (format "(~a ~a)" body n))))))]
-       [(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 temp. : gamma, \\(forall temp. : term, \\(forall temp. : 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 #'(case z (z z) (s (lambda (n : nat) (s n)))))])
-      (check-regexp-match
-        "\\(match z with\n\\| \\(z\\) => z\n\\| \\(s .+\\) => \\(\\(fun n : nat => \\(s n\\)\\) .+\\)\nend\\)"
-        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)))))

redex-curnel.rkt

@@ -1,980 +0,0 @@
-#lang racket
-
-;; This module contains a model of CIC, ish.
-;; TODO: Strip to racket/base as much as possible
-(module core racket
-  (require
-    (only-in racket/set set=?)
-    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
-
-  ;; Core language. Surface langauge should provide short-hand, such as
-  ;; -> for non-dependent function types, and type inference.
-  (define-language cicL
-    (i ::= natural)
-    (U ::= (Unv i))
-    (x ::= variable-not-otherwise-mentioned)
-    (v ::= (Π (x : t) t) (μ (x : t) t) (λ (x : t) t) x U)
-    (t e ::= (case e (x e) ...) v (t t)))
-
-  (define x? (redex-match? cicL x))
-  (define t? (redex-match? cicL t))
-  (define e? (redex-match? cicL e))
-  (define v? (redex-match? cicL v))
-  (define U? (redex-match? cicL U))
-
-  (module+ test
-    (require rackunit)
-    (define-term Type (Unv 0))
-    (check-true (x? (term T)))
-    (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 (U? (term (Unv 0))))
-    (check-true (U? (term Type)))
-    (check-true (e? (term (λ (x_0 : (Unv 0)) x_0))))
-    (check-true (v? (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)))))
-
-  ;; 'A'
-  ;; Types of Universes
-  (define-judgment-form cicL
-    #:mode (unv-ok I O)
-    #:contract (unv-ok U U)
-
-    [(where i_1 ,(add1 (term i_0)))
-     -----------------
-     (unv-ok (Unv i_0) (Unv i_1))])
-
-  ;; 'R'
-  ;; Kinding, I think
-  (define-judgment-form cicL
-    #:mode (unv-kind I I O)
-    #:contract (unv-kind U U U)
-
-    [----------------
-     (unv-kind (Unv 0) (Unv 0) (Unv 0))]
-
-    [----------------
-     (unv-kind (Unv 0) (Unv i) (Unv i))]
-
-    [----------------
-     (unv-kind (Unv i) (Unv 0) (Unv 0))]
-
-    [(where i_3 ,(max (term i_1) (term i_2)))
-     ----------------
-     (unv-kind (Unv i_1) (Unv i_2) (Unv i_3))])
-
-  ;; NB: Substitution is hard
-  (define-metafunction cicL
-    subst-vars : (x any) ... any -> any
-    [(subst-vars (x_1 any_1) x_1) any_1]
-    [(subst-vars (x_1 any_1) (any_2 ...)) ((subst-vars (x_1 any_1) any_2) ...)]
-    [(subst-vars (x_1 any_1) any_2) any_2]
-    [(subst-vars (x_1 any_1) (x_2 any_2) ... any_3) (subst-vars (x_1 any_1) (subst-vars (x_2 any_2) ... any_3))]
-    [(subst-vars any) any])
-
-  (define-metafunction cicL
-    subst : t x t -> t
-    [(subst U x t) U]
-    [(subst x x t) t]
-    [(subst x_0 x t) x_0]
-    [(subst (any (x : t_0) t_1) x t) (any (x : (subst t_0 x t)) t_1)]
-    ;; TODO: Broken: needs capture avoiding, but currently require
-    ;; binders to be the same in term/type, so this is not a local
-    ;; change.
-    [(subst (any (x_0 : t_0) t_1) x t) (any (x_0 : (subst t_0 x t)) (subst t_1 x t)) ]
-    [(subst (e_0 e_1) x t) ((subst e_0 x t) (subst e_1 x t))]
-    [(subst (case e (x_0 e_0) ...) x t)
-     (case (subst e x t)
-       (x_0 (subst e_0 x t)) ...)])
-  (module+ test
-    (check-equal?
-      (term (Π (a : S) (Π (b : B) ((and S) B))))
-      (term (subst (Π (a : A) (Π (b : B) ((and A) B))) A S))))
-  ;; NB:
-  ;; TODO: Why do I not have tests for substitutions?!?!?!?!?!?!?!!?!?!?!?!?!?!!??!?!
-
-  (define-metafunction cicL
-    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 ...))])
-
-  (define-extended-language cic-redL cicL
-    (E hole (E t) (case E (x e) ...)))
-
-  (define-metafunction cicL
-    inductive-name : t -> x or #f
-    [(inductive-name x) x]
-    [(inductive-name (t_1 t_2)) (inductive-name t_1)]
-    [(inductive-name t) #f])
-  (module+ test
-    (check-equal?
-      (term and)
-      (term (inductive-name ((and A) B)))))
-
-  (define-metafunction cicL
-    inductive-apply : t t -> t
-    [(inductive-apply e x) e]
-    [(inductive-apply e (e_1 e_2))
-     ((inductive-apply e e_1) e_2)])
-
-  ;; TODO: Congruence-closure instead of β
-  (define ==β
-    (reduction-relation cic-redL
-      (==> ((Π (x : t_0) t_1) t_2)
-           (subst t_1 x t_2))
-      (==> ((λ (x : t) e_0) e_1)
-           (subst e_0 x e_1))
-      (==> ((μ (x : t) e_0) e_1)
-           ((subst e_0 x (μ (x : t) e_0)) e_1))
-      (==> (case e_9
-             (x_0 e_0) ... (x e) (x_r e_r) ...)
-           (inductive-apply e e_9)
-           (where x (inductive-name e_9)))
-      with
-      [(--> (in-hole E t_0) (in-hole E t_1))
-       (==> t_0 t_1)]))
-
-  (define-metafunction cic-redL
-    reduce : e -> e
-    [(reduce e) ,(car (apply-reduction-relation* ==β (term e)))])
-  (module+ test
-    (check-equal? (term (reduce (Unv 0))) (term (Unv 0)))
-    (check-equal? (term (reduce ((λ (x : t) x) (Unv 0)))) (term (Unv 0)))
-    (check-equal? (term (reduce ((Π (x : t) x) (Unv 0)))) (term (Unv 0)))
-    ;; NB: Currently not reducing under binders. I forget why.
-    (check-equal? (term (reduce (Π (x : t) ((Π (x_0 : t) x_0) (Unv 0)))))
-                  (term (Π (x : t) (Unv 0))))
-    (check-equal? (term (reduce (Π (x : t) ((Π (x_0 : t) x_0) x))))
-                  (term (Π (x : t) x)))
-    (check-equal? (term (reduce (case (s z) (z (s z)) (s (λ (x : nat)
-                                                            (s (s x)))))))
-                  (term (s (s z))))
-    (check-equal? (term (reduce (case (s (s (s z))) (z (s z)) (s (λ (x : nat)
-                                                            (s (s x)))))))
-                  (term (s (s (s (s z)))))))
-
-  ;; TODO: Bi-directional and inference?
-  ;; http://www.cs.ox.ac.uk/ralf.hinze/WG2.8/31/slides/stephanie.pdf
-
-  (define-extended-language cic-typingL cicL
-    (Σ Γ ::= ∅ (Γ x : t)))
-
-  (define Σ? (redex-match? cic-typingL Σ))
-  (define Γ? (redex-match? cic-typingL Γ))
-  (module+ test
-    ;; TODO: Rename these signatures, and use them in all future tests.
-    (define Σ (term (((∅ nat : (Unv 0)) zero : nat) s : (Π (x : nat) nat))))
-
-    (define Σ0 (term ∅))
-    (define Σ2 (term (((∅ nat : (Unv 0)) z : nat) s : (Π (x : nat) nat))))
-    (define Σ3 (term (∅ and : (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Unv 0))))))
-    (define Σ4 (term (,Σ3 conj : (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Π (a : A) (Π (b : B) ((and A) B))))))))
-
-    (check-true (Σ? Σ0))
-    (check-true (Σ? Σ2))
-    (check-true (Σ? Σ4))
-    (check-true (Σ? Σ3))
-    (check-true (Σ? Σ4)))
-
-  (define-metafunction cic-typingL
-    append-env : Γ Γ -> Γ
-    [(append-env Γ ∅) Γ]
-    [(append-env Γ_2 (Γ_1 x : t))
-     ((append-env Γ_2 Γ_1) x : t)])
-
-  ;; NB: Depends on clause order
-  (define-metafunction cic-typingL
-    lookup : Γ x -> t or #f
-    [(lookup ∅ x) #f]
-    [(lookup (Γ x : t) x) t]
-    [(lookup (Γ x_0 : t_0) x_1) (lookup Γ x_1)])
-
-  ;; NB: Depends on clause order
-  (define-metafunction cic-typingL
-    remove : Γ x -> Γ
-    [(remove ∅ x) ∅]
-    [(remove (Γ x : t) x) Γ]
-    [(remove (Γ x_0 : t_0) x_1) (remove Γ x_1)])
-
-  (define-metafunction cic-typingL
-    result-type : Σ t -> t or #f
-    [(result-type Σ (Π (x : t) e)) (result-type Σ e)]
-    [(result-type Σ (e_1 e_2)) (result-type Σ e_1)]
-    [(result-type Σ x) ,(and (term (lookup Σ x)) (term x))]
-    [(result-type Σ t) #f])
-  (module+ test
-    (check-equal? (term nat) (term (result-type ,Σ (Π (x : nat) nat))))
-    (check-equal? (term nat) (term (result-type ,Σ nat))))
-
-  (define-judgment-form cic-typingL
-    #:mode (constructor-for I I O)
-    #:contract (constructor-for Σ t x)
-
-    [(where t_0 (result-type Σ t))
-     -------------
-     (constructor-for (Σ x : t) t_0 x)]
-
-    [(constructor-for Σ t_1 x)
-     -------------
-     (constructor-for (Σ x_0 : t_0) t_1 x)])
-  (module+ test
-    (check-true
-      (judgment-holds (constructor-for ((∅ truth : (Unv 0)) T : truth) truth T)))
-    (check-true
-      (judgment-holds
-        (constructor-for ((∅ nat : (Unv 0)) zero : nat)
-                         nat zero)))
-    (check set=?
-      (judgment-holds
-        (constructor-for (((∅ nat : (Unv 0)) zero : nat) s : (Π (x : nat) nat))
-                         nat x) x)
-      (list (term zero) (term s))))
-  (define-metafunction cic-typingL
-    constructors-for : Σ x (x ...) -> #t or #f
-    [(constructors-for Σ x_0 (x ...))
-     ,((lambda (x y) (and (set=? x y) (= (length x) (length y))))
-       (term (x ...))
-       (judgment-holds (constructor-for Σ x_0 x_00) x_00))])
-  (module+ test
-    (check-true
-      (term (constructors-for (((∅ nat : (Unv 0)) zero : nat) s : (Π (x : nat) nat))
-                         nat (zero s))))
-    (check-false
-      (term (constructors-for (((∅ nat : (Unv 0)) zero : nat) s : (Π (x : nat) nat))
-                         nat (zero))))
-    (check-true
-      (term (constructors-for ,Σ4 and (conj)))))
-
-  (define-metafunction cicL
-    branch-type : t t t -> t
-    [(branch-type t_ind (Π (x_0 : t) e_0) (Π (x_1 : t) e_1))
-     (branch-type t_ind e_0 e_1)]
-    ;[(branch-type t_ind t_ind t) t])
-    [(branch-type t_ind t_other t) t])
-  (module+ test
-    (check-equal? (term (Unv 0)) (term (branch-type nat (lookup ,Σ zero) (Unv 0))))
-    (check-equal? (term nat) (term (branch-type nat nat nat)))
-    (check-equal? (term (Unv 0)) (term (branch-type nat (lookup ,Σ s) (Π (x : nat) (Unv 0)))))
-    (check-equal?
-      (term (Unv 0))
-      (term (branch-type and (lookup ,Σ4 conj)
-              (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Π (a : A) (Π (b : B) (Unv 0)))))))))
-
-  (define-metafunction cic-typingL
-    branch-types-match : Σ (x ...) (t ...) t t -> #t or #f
-    [(branch-types-match Σ (x ...) (t_11 ...) t t_1)
-     ,(andmap (curry equal? (term t)) (term ((branch-type t_1 (lookup Σ x) t_11) ...)))])
-  (module+ test
-    (check-true
-      (term (branch-types-match ((∅ truth : (Unv 0)) T : truth) () () (Unv 0) nat)))
-    (check-true
-      (term (branch-types-match ,Σ (zero s) ((Unv 0) (Π (x : nat) (Unv 0))) (Unv 0) nat)))
-    (check-true
-      (term (branch-types-match ,Σ (zero s) (nat (Π (x : nat) nat)) nat nat))))
-
-  ;; TODO: Add positivity checking.
-  (define-metafunction cicL
-    positive : t any -> #t or #f
-    ;; (Unv 0); not a inductive constructor
-    [(positive any_1 any_2) #t])
-
-  (module+ test
-    (check-true (term (positive nat nat)))
-    (check-true (term (positive (Π (x : (Unv 0)) (Π (y : (Unv 0)) (Unv 0))) #f)))
-    (check-true (term (positive (Π (x : nat) nat) nat)))
-    ;; (nat -> nat) -> nat
-    ;; Not sure if this is actually supposed to pass
-    (check-false (term (positive (Π (x : (Π (y : nat) nat)) nat) nat)))
-    ;; ((Unv 0) -> nat) -> nat
-    (check-true (term (positive (Π (x : (Π (y : (Unv 0)) nat)) nat) nat)))
-    ;; (((nat -> (Unv 0)) -> nat) -> nat)
-    (check-true (term (positive (Π (x : (Π (y : (Π (x : nat) (Unv 0))) nat)) nat) nat)))
-    ;; Not sure if this is actually supposed to pass
-    (check-false (term (positive (Π (x : (Π (y : (Π (x : nat) nat)) nat)) nat) nat)))
-
-    (check-true (term (positive (Unv 0) #f))))
-
-  (define-judgment-form cic-typingL
-    #:mode (wf I I)
-    #:contract (wf Σ Γ)
-
-    [-----------------
-     (wf ∅ ∅)]
-
-    [(types Σ Γ t t_0)
-     (wf Σ Γ)
-     -----------------
-     (wf Σ (Γ x : t))]
-
-    [(types Σ ∅ t t_0)
-     (wf Σ ∅)
-     (side-condition (positive t (result-type Σ t)))
-     -----------------
-     (wf (Σ x : t) ∅)])
-  (module+ test
-    (check-true (judgment-holds (wf ∅ ∅)))
-    (check-true (judgment-holds (wf (∅ truth : (Unv 0)) ∅)))
-    (check-true (judgment-holds (wf ∅ (∅ x : (Unv 0)))))
-    (check-true (judgment-holds (wf (∅ nat : (Unv 0)) (∅ x : nat))))
-    (check-true (judgment-holds (wf (∅ nat : (Unv 0)) (∅ x : (Π (x : nat) nat))))))
-
-  ;; TODO: Add termination checking
-  (define-metafunction cicL
-    terminates? : t -> #t or #f
-    [(terminates? t) #t])
-  (module+ test
-    (check-false (term (terminates? (μ (x : (Unv 0)) x))))
-    (check-false (term (terminates? (μ (x : (Unv 0)) (λ (y : (Unv 0)) (x y))))))
-    (check-true (term (terminates? (μ (x : (Unv 0)) (λ (y : (Unv 0)) y))))))
-
-  (define-judgment-form cic-typingL
-    #:mode (types I I I O)
-    #:contract (types Σ Γ e t)
-
-    [(unv-ok U_0 U_1)
-     (wf Σ Γ)
-     ----------------- "DTR-Axiom"
-     (types Σ Γ U_0 U_1)]
-
-    [(where t (lookup Σ x))
-     ----------------- "DTR-Inductive"
-     (types Σ Γ x t)]
-
-    ;; TODO: Require alpha-equiv here, at least.
-    [(where t (lookup Γ x))
-     ----------------- "DTR-Start"
-     (types Σ Γ x t)]
-
-    [(types Σ Γ t_0 U_1)
-     (types Σ (Γ x : t_0) t U_2)
-     (unv-kind U_1 U_2 U)
-     ----------------- "DTR-Product"
-     (types Σ Γ (Π (x : t_0) t) U)]
-
-    [(types Σ Γ e_0 (Π (x_0 : t_0) t_1))
-     (types Σ Γ e_1 t_0)
-     ----------------- "DTR-Application"
-     (types Σ Γ (e_0 e_1) (subst t_1 x_0 e_1))]
-
-    ;; TODO: This restriction that the names be the same is a little annoying
-    [(types Σ (Γ x : t_0) e t_1)
-     (types Σ Γ (Π (x : t_0) t_1) U)
-     ----------------- "DTR-Abstraction"
-     (types Σ Γ (λ (x : t_0) e) (Π (x : t_0) t_1))]
-
-    [(side-condition (terminates? (μ (x : t_0) e)))
-     (types Σ (Γ x : t_0) e t_0)
-     (types Σ Γ t_0 U)
-     ----------------- "DTR-Fix"
-     (types Σ Γ (μ (x : t_0) e) t_0)]
-
-    [(types Σ Γ e t_9)
-     (where t_1 (inductive-name t_9))
-     (side-condition (constructors-for Σ t_1 (x_0 x_1 ...)))
-     (types Σ Γ e_0 t_00)
-     (types Σ Γ e_1 t_11) ...
-     ;; TODO Some of these meta-functions aren't very consistent in terms
-     ;; of interface
-     (where t (branch-type t_1 (lookup Σ x_0) t_00))
-     (side-condition (branch-types-match Σ (x_1 ...) (t_11 ...) t t_1))
-     ----------------- "DTR-Case"
-     (types Σ Γ (case e (x_0 e_0) (x_1 e_1) ...) t)]
-
-    ;; TODO: This shouldn't be a special case, but I failed to forall
-    ;; quantify properly over the branches in the above case, and I'm lazy.
-    ;; TODO: Seem to need bidirectional checking to pull this off
-    ;; http://www.cs.ox.ac.uk/ralf.hinze/WG2.8/31/slides/stephanie.pdf
-    #;[(types Σ Γ e t_9)
-     (where t_1 (inductive-name t_9))
-     (side-condition (constructors-for Σ t_1 ()))
-     ----------------- "DTR-Case-Empty"
-     (types Σ Γ (case e) t)]
-
-    ;; TODO: beta-equiv
-    ;; This rule is no good for algorithmic checking; Redex infinitly
-    ;; searches it.
-    ;; Perhaps something closer to Zombies = type would be better.
-    ;; For now, reduce types
-    #;[(types Σ Γ e (in-hole E t))
-     (where t_0 (in-hole E t))
-     (where t_1 ,(car (apply-reduction-relation* ==β (term t_0))))
-     (types Σ Γ t_1 U)
-     ----------------- "DTR-Conversion"
-     (types Σ Γ e t_1)])
-  (module+ test
-    (check-true (judgment-holds (types ∅ ∅ (Unv 0) (Unv 1))))
-    (check-true (judgment-holds (types ∅ (∅ x : (Unv 0)) (Unv 0) (Unv 1))))
-    (check-true (judgment-holds (types ∅ (∅ x : (Unv 0)) x (Unv 0))))
-    (check-true (judgment-holds (types ∅ ((∅ x_0 : (Unv 0)) x_1 : (Unv 0))
-                                       (Π (x_3 : x_0) x_1) (Unv 0))))
-
-    (check-true (judgment-holds (types ∅ (∅ x_0 : (Unv 0)) x_0 U_1)))
-    (check-true (judgment-holds (types ∅ ((∅ x_0 : (Unv 0)) x_2 : x_0) (Unv 0) U_2)))
-    (check-true (judgment-holds (unv-kind (Unv 0) (Unv 0) (Unv 0))))
-    (check-true (judgment-holds (types ∅ (∅ x_0 : (Unv 0)) (Π (x_2 : x_0) (Unv 0)) t)))
-
-    (check-true (judgment-holds (types ∅ ∅ (λ (x : (Unv 0)) x) (Π (x : (Unv 0)) (Unv 0)))))
-    (check-true (judgment-holds (types ∅ ∅ (λ (y : (Unv 0)) (λ (x : y) x))
-                                       (Π (y : (Unv 0)) (Π (x : y) y)))))
-
-    (check-equal? (list (term (Unv 1)))
-      (judgment-holds
-        (types ∅ ((∅ x1 : (Unv 0)) x2 : (Unv 0)) (Π (t6 : x1) (Π (t2 : x2) (Unv 0)))
-               U)
-        U))
-    (check-true
-      (judgment-holds
-        (types ∅ ∅ (Π (x2 : (Unv 0)) (Unv 0))
-               U)))
-    (check-true
-      (judgment-holds
-        (types ∅ (∅ x1 : (Unv 0)) (λ (x2 : (Unv 0)) (Π (t6 : x1) (Π (t2 : x2) (Unv 0))))
-               t)))
-    (check-true
-      (judgment-holds (types ((∅ truth : (Unv 0)) T : truth)
-                             ∅
-                             T
-                             truth)))
-    (check-true
-      (judgment-holds (types ((∅ truth : (Unv 0)) T : truth)
-                             ∅
-                             (Unv 0)
-                             (Unv 1))))
-    (check-true
-      (judgment-holds (types ((∅ truth : (Unv 0)) T : truth)
-                             ∅
-                             (case T (T (Unv 0)))
-                             (Unv 1))))
-
-    (check-false
-      (judgment-holds (types ((∅ truth : (Unv 0)) T : truth)
-                             ∅
-                             (case T (T (Unv 0)) (T (Unv 0)))
-                             (Unv 1))))
-    (define-syntax-rule (nat-test syn ...)
-      (check-true (judgment-holds
-                    (types (((∅ nat : (Unv 0)) zero : nat) s : (Π (x : nat) nat))
-                           syn ...))))
-    (nat-test ∅ (Π (x : nat) nat) (Unv 0))
-    (nat-test ∅ (λ (x : nat) x) (Π (x : nat) nat))
-    (nat-test ∅ (case zero (zero zero) (s (λ (x : nat) x)))
-              nat)
-    (nat-test ∅ nat (Unv 0))
-    (nat-test ∅ zero nat)
-    (nat-test ∅ s (Π (x : nat) nat))
-    (nat-test ∅ (s zero) nat)
-    (nat-test ∅ (case zero (zero (s zero)) (s (λ (x : nat) (s (s x)))))
-              nat)
-    (nat-test ∅ (case zero (zero (s zero)) (s (λ (x : nat) (s (s x)))))
-              nat)
-    (check-false (judgment-holds
-                    (types (((∅ nat : (Unv 0)) zero : nat) s : (Π (x : nat) nat))
-                           ∅
-                           (case zero (zero (s zero)))
-                           nat)))
-    (define lam (term (λ (nat : (Unv 0)) nat)))
-    (check-equal?
-      (list (term (Π (nat : (Unv 0)) (Unv 0))))
-      (judgment-holds (types ,Σ0 ∅ ,lam t) t))
-    (check-equal?
-      (list (term (Π (nat : (Unv 0)) (Unv 0))))
-      (judgment-holds (types ,Σ2 ∅ ,lam t) t))
-    (check-equal?
-      (list (term (Π (x : (Π (y : (Unv 0)) y)) nat)))
-      (judgment-holds (types (∅ nat : (Unv 0)) ∅ (λ (x : (Π (y : (Unv 0)) y)) (x nat))
-                            t) t))
-    (check-equal?
-      (list (term (Π (y : (Unv 0)) (Unv 0))))
-      (judgment-holds (types (∅ nat : (Unv 0)) ∅ (λ (y : (Unv 0)) y) t) t))
-    (check-equal?
-      (list (term (Unv 0)))
-      (judgment-holds (types (∅ 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
-        (types ,Σ4 ∅ (Π (S : (Unv 0)) (Π (B : (Unv 0)) (Π (a : S) (Π (b : B) ((and S) B)))))
-               U) U))
-    (check-true
-      (judgment-holds (types ,Σ4 (∅ S : (Unv 0)) conj (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Π (a : A) (Π (b : B) ((and A) B))))))))
-    (check-true
-      (judgment-holds (types ,Σ4 (∅ S : (Unv 0)) S (Unv 0))))
-    (check-true
-      (judgment-holds (types ,Σ4 (∅ S : (Unv 0)) (conj S)
-                             (Π (B : (Unv 0)) (Π (a : S) (Π (b : B) ((and S) B)))))))
-    (check-true
-      (judgment-holds (types ,Σ4 (∅ S : (Unv 0)) (conj S)
-                             (Π (B : (Unv 0)) (Π (a : S) (Π (b : B) ((and S) B)))))))
-    (check-true
-      (judgment-holds (types ,Σ4 ∅ (λ (S : (Unv 0)) (conj S))
-                             (Π (S : (Unv 0)) (Π (B : (Unv 0)) (Π (a : S) (Π (b : B) ((and S) B))))))))
-    (check-true
-      (judgment-holds (types ((,Σ4 true : (Unv 0)) tt : true) ∅
-                             ((((conj true) true) tt) tt)
-                             ((and true) true))))
-    (check-true
-      (judgment-holds (types ((,Σ4 true : (Unv 0)) tt : true) ∅
-                             (case ((((conj true) true) tt) tt)
-                               (conj (λ (A : (Unv 0))
-                                        (λ (B : (Unv 0))
-                                           (λ (a : A)
-                                              (λ (b : B) a))))))
-                             A)))
-    (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)))))
-    (define gamma (term (∅ temp863 : pre)))
-    (check-true (judgment-holds (wf ,sigma ∅)))
-    (check-true (judgment-holds (wf ,sigma ,gamma)))
-    (check-true
-      (judgment-holds (types ,sigma ,gamma (Unv 0) t)))
-    (check-true
-      (judgment-holds (types ,sigma ,gamma pre t)))
-    (check-true
-      (judgment-holds (types ,sigma (,gamma tmp863 : pre) (Unv 0) (Unv 1))))
-    (check-true
-      (judgment-holds (types ,sigma (,gamma x : false) (case x) t)))))
-
-;; This module just provide module language sugar over the redex model.
-
-;; TODO: Strip to racket/base as much as possible.
-;; TODO: Remove trace,pretty, debugging stuff
-(module sugar racket
-  (require
-    racket/trace
-    racket/pretty
-    (submod ".." core)
-    redex/reduction-semantics
-    racket/provide-syntax
-    (for-syntax
-      (except-in racket import)
-      syntax/parse
-      racket/pretty
-      racket/trace
-      racket/syntax
-      (except-in racket/provide-transform export)
-      racket/require-transform
-      (except-in (submod ".." core) remove)
-      redex/reduction-semantics))
-  (provide
-    ;; Basic syntax
-    for-syntax
-    only-in
-    all-defined-out
-    rename-in
-    #%module-begin
-    begin
-    (rename-out
-      [dep-module+ module+]
-      [dep-provide provide]
-      [dep-require require]
-
-      [dep-lambda lambda]
-      [dep-lambda λ]
-      [dep-app #%app]
-
-      [dep-fix fix]
-
-      [dep-forall forall]
-      [dep-forall ∀]
-
-      [dep-inductive data]
-      [dep-case case]
-
-      [dep-var #%top]
-
-;      [dep-datum #%datum]
-      [dep-define define])
-    Type
-    ;; DYI syntax extension
-    define-syntax
-    begin-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
-      cur-expand
-      type-infer/syn
-      type-check/syn?
-      normalize/syn)
-    run)
-
-  (begin-for-syntax
-    (current-trace-notify
-      (parameterize ([pretty-print-depth #f]
-                     [pretty-print-columns 'infinity])
-        (lambda (x)
-          (pretty-display x)
-          (newline))))
-    (current-trace-print-args
-      (let ([cwtpr (current-trace-print-args)])
-        (lambda (s l kw l2 n)
-          (cwtpr s (map (lambda (x)
-                          (if (syntax? x)
-                              (cons 'syntax (syntax->datum x))
-                              x)) l) kw l2 n))))
-    (current-trace-print-results
-      (let ([cwtpr (current-trace-print-results)])
-        (lambda (s l n)
-         (cwtpr s (map (lambda (x) (if (syntax? x) (cons 'syntax (syntax->datum x)) x)) l) n)))))
-
-  (begin-for-syntax
-    ;; TODO: Gamma and Sigma 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))
-          x)))
-
-    (define sigma
-      (make-parameter (term ∅)
-        (lambda (x)
-          (unless (Σ? x)
-            (error 'core-error "We built a bad sigma ~s" x))
-          x)))
-
-    (define (extend-env/term env x t)
-      (term (,(env) ,x : ,t)))
-
-    (define (extend-env/term! env x t) (env (extend-env/term env x t)))
-
-    (define (extend-env/syn env x t)
-      (term (,(env) ,(syntax->datum x) : ,(cur->datum t))))
-
-    (define (extend-env/syn! env x t) (env (extend-env/syn env x t)))
-
-    (define bind-subst (make-parameter (list null null)))
-
-    (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 (type-infer/term t)
-      (let ([t (judgment-holds (types ,(sigma) ,(gamma) ,t t_0) t_0)])
-        (and (pair? t) (car t))))
-
-    (define (syntax->curnel-syntax syn) (denote syn (cur->datum syn)))
-
-    (define (denote syn t)
-      #`(term (reduce (subst-all #,(datum->syntax syn t) #,(first (bind-subst)) #,(second (bind-subst))))))
-
-    ;; TODO: Blanket disarming is probably a bad idea.
-    (define orig-insp (variable-reference->module-declaration-inspector
-                        (#%variable-reference)))
-    (define (disarm syn) (syntax-disarm syn orig-insp))
-
-    ;; Locally expand everything down to core forms.
-    (define (core-expand syn)
-      (disarm
-        (local-expand syn 'expression
-          (append (syntax-e #'(term reduce subst-all dep-var #%app λ Π μ case
-                               Unv #%datum))))))
-
-    ;; 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))
-
-    ;; Expand a piece of syntax into a curnel redex term
-    (define (cur->datum syn)
-      ;; Main loop; avoid type
-      (define reified-term
-        (parameterize ([inner-expand? #t])
-          (let cur->datum ([syn syn])
-            (syntax-parse (core-expand syn)
-              #:literals (term reduce #%app subst-all)
-              #:datum-literals (case Π λ μ : Unv)
-              [x:id (syntax->datum #'x)]
-              [(subst-all e _ _) (syntax->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
-              ;; Maybe make a syntax class for the binders, core forms,
-              ;; etc.
-              [(b:id (x:id : t) e)
-               (let* ([x (syntax->datum #'x)]
-                      [t (cur->datum #'t)]
-                      [e (parameterize ([gamma (extend-env/term gamma x t)])
-                           (cur->datum #'e))])
-                 (term (,(syntax->datum #'b) (,x : ,t) ,e)))]
-              [(case e (ec eb) ...)
-               (term (case ,(cur->datum #'e)
-                           ,@(map (lambda (c b) `(,c ,(cur->datum b)))
-                                  (syntax->datum #'(ec ...))
-                                  (syntax->list #'(eb ...)))))]
-              [(#%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))
-      reified-term)
-
-    ;; Reflection tools
-
-    ;; TODO: OOps, type-infer doesn't return a cur term but a redex term
-    ;; wrapped in syntax bla. This is bad.
-    (define (type-infer/syn syn)
-      (let ([t (type-infer/term (cur->datum syn))])
-        (and t (datum->syntax syn t))))
-
-    (define (type-check/syn? syn type)
-      (let ([t (type-infer/term (cur->datum syn))])
-        (equal? t (cur->datum type))))
-
-    (define (normalize/syn syn)
-      (denote syn (term (reduce (subst-all ,(cur->datum syn) ,(first (bind-subst)) ,(second (bind-subst)))))))
-
-    ;; Takes a Cur term syn and an arbitrary number of identifiers ls. The cur term is
-    ;; expanded until expansion reaches a Curnel form, or one of the
-    ;; identifiers in ls.
-    (define (cur-expand syn . ls)
-      (disarm (local-expand syn 'expression
-                (append (syntax-e #'(Type dep-inductive dep-case dep-lambda dep-app
-                                   dep-fix dep-forall dep-var))
-                        ls)))))
-
-    ;; TODO: OOps, run doesn't return a cur term but a redex term
-    ;; wrapped in syntax bla. This is bad.
-    (define-syntax (run syn)
-      (syntax-case syn ()
-        [(_ expr) (normalize/syn #'expr)]))
-
-  ;; -----------------------------------------------------------------
-  ;; Require/provide macros
-
-  ;; TODO: This is code some of the most hacky awful code I've ever
-  ;; written. But it works.
-  (begin-for-syntax
-    (define envs (list #'(void)))
-
-    (define (cur-identifier-bound? id)
-      (let ([x (syntax->datum id)])
-        (and (x? x)
-             (or (term (lookup ,(gamma) ,x))
-               (term (lookup ,(sigma) ,x))))))
-
-    (define (filter-cur-exports syn modes)
-      (partition (compose cur-identifier-bound? export-local-id)
-                 (apply append (map (lambda (e) (expand-export e modes))
-                                    (syntax->list syn))))))
-  (define-syntax extend-env-and-provide
-    (make-provide-transformer
-      (lambda (syn modes)
-        (syntax-case syn ()
-          [(_ e ...)
-           (let-values ([(cur ~cur) (filter-cur-exports #'(e ...) modes)])
-             (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)])
-                            #`(extend-env/term! #,env #,(export-out-sym e) #,t))))
-             ~cur)]))))
-
-  (define-syntax (export-envs syn)
-    (syntax-case syn ()
-      [(_ gamma-out sigma-out bind-out)
-       #`(begin-for-syntax
-           (define gamma-out (term #,(gamma)))
-           (define sigma-out (term #,(sigma)))
-           (define bind-out '#,(bind-subst)))]))
-
-  ;; TODO: This can only handle a single provide form, otherwise
-  ;; generates multiple *-out
-  (define-syntax (dep-provide syn)
-    (syntax-case syn ()
-      [(_ e ...)
-       (begin
-         ;; TODO: 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.
-         (syntax-local-lift-module-end-declaration
-           #`(export-envs gamma-out sigma-out bind-out))
-         #`(provide (extend-env-and-provide e ...)
-                    (for-syntax gamma-out sigma-out bind-out)))]))
-  (begin-for-syntax
-    (define out-gammas #`())
-    (define out-sigmas #`())
-    (define out-binds #`())
-    (define gn 0)
-    (define sn 0)
-    (define bn 0)
-    (define (filter-cur-imports syn)
-      (for/fold ([imports '()]
-                 [sources '()])
-                ([req-spec (syntax->list syn)])
-        (let-values ([(more-imports more-sources) (expand-import req-spec)])
-          (values (for/fold ([imports imports])
-                     ([imp more-imports])
-                     (cond
-                       [(equal? (import-src-sym imp) 'gamma-out)
-                        (let ([new-id (format-id (import-orig-stx imp)
-                                                 "gamma-out~a" gn)])
-                             ;; TODO: Fewer set!s
-                             ;; TODO: Do not DIY gensym
-                             (set! gn (add1 gn))
-                             (set! out-gammas
-                               #`(#,@out-gammas (gamma (term (append-env
-                                                               ,(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)
-                        (let ([new-id (format-id (import-orig-stx imp)
-                                                 "sigma-out~a" sn)])
-                             ;; TODO: Fewer set!s
-                             ;; TODO: Do not DIY gensym
-                             (set! sn (add1 sn))
-                             (set! out-sigmas
-                               #`(#,@out-sigmas (sigma (term (append-env
-                                                               ,(sigma)
-                                                               ,#,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) 'bind-out)
-                        (let ([new-id (format-id (import-orig-stx imp)
-                                                 "bind-out~a" bn)])
-                             ;; TODO: Fewer set!s
-                             ;; TODO: Do not DIY gensym
-                             (set! bn (add1 bn))
-                             (set! out-binds
-                               #`(#,@out-binds (bind-subst (list (append
-                                                                   (first #,new-id)
-                                                                   (first (bind-subst)))
-                                                                 (append
-                                                                   (second #,new-id)
-                                                                   (second (bind-subst)))))))
-                             (cons (struct-copy import imp [local-id new-id])
-                                   imports))]
-                       [else (cons imp imports)]))
-                  (append sources more-sources))))))
-
-  (define-syntax extend-env-and-require
-    (make-require-transformer (lambda (syn)
-                                (syntax-case syn ()
-                                  [(_ e ...) (filter-cur-imports #'(e ...))]))))
-
-    ;; TODO: rename in will need to rename variables in gamma and
-    ;; sigma.
-    (define-syntax (import-envs syn)
-      (syntax-case syn ()
-        [(_) #`(begin-for-syntax #,@out-gammas #,@out-sigmas
-                                 #,@out-binds)]))
-
-  (define-syntax (dep-require syn)
-    (syntax-case syn ()
-      [(_ e ...)
-       #`(begin
-          (require (extend-env-and-require e ...))
-          (import-envs))]))
-
-  (define-syntax (dep-module+ syn)
-    (syntax-case syn ()
-      [(_ name body ...)
-       #`(module+ name
-           (begin-for-syntax
-             (gamma (term #,(gamma)))
-             (sigma (term #,(sigma)))
-             (bind-subst '#,(bind-subst)))
-           body ...)]))
-
-  ;; -----------------------------------------------------------------
-  ;; Core wrapper macros
-  ;;
-  ;; TODO: Can these be simplified further?
-  ;; TODO: Can we make core-expand some kind of parameter that is only
-  ;; to ensure type-checking is only done at the outermost level, and
-  ;; not in the main loop?
-  #;(define-syntax (dep-datum syn) (denote #'syn))
-  (define-syntax (dep-lambda syn)
-    (syntax-case syn (:)
-      [(_ (x : t) e) (syntax->curnel-syntax #`(λ (x : t) e))]))
-
-  (define-syntax (dep-app syn)
-    (syntax-case syn ()
-      [(_ e1 e2) (syntax->curnel-syntax #`(#%app e1 e2))]))
-
-  (define-syntax (dep-case syn)
-    (syntax-case syn ()
-      [(_ e ...) (syntax->curnel-syntax #`(case e ...))]))
-
-  (define-syntax (dep-forall syn)
-    (syntax-case syn (:)
-      [(_ (x : t) e) (syntax->curnel-syntax #`(Π (x : t) e))]))
-
-  (define-syntax (Type syn)
-    (syntax-case syn ()
-      [(_ i) (syntax->curnel-syntax #'(Unv i))]
-      [_ #'(Type 0)]))
-
-  (define-syntax (dep-fix syn)
-   (syntax-case syn (:)
-     [(_ (x : t) e) (syntax->curnel-syntax #`(μ (x : t) e))]))
-
-  (define-syntax (dep-inductive syn)
-    (syntax-case syn (:)
-      [(_ i : ti (x1 : t1) ...)
-       (begin
-         (extend-env/syn! sigma #'i #'ti)
-         (for ([x (syntax->list #`(x1 ...))]
-               [t (syntax->list #`(t1 ...))])
-           (extend-env/syn! sigma x t))
-         #'(void))]))
-
-  ;; TODO: Not sure if this is the correct behavior for #%top
-  (define-syntax (dep-var syn)
-    (syntax-case syn ()
-      [(_ . id) #`(term (reduce id))]))
-
-  ;; TODO: Syntax-parse
-  (define-syntax (dep-define syn)
-    (syntax-case syn (:)
-      [(_ (name (x : t)) e)
-       #'(dep-define name (dep-lambda (x : t) e))]
-      [(_ id e)
-       ;; TODO: Can't actually run programs until I do something about
-       ;; #'e. Maybe denote final terms into Racket. Or keep an
-       ;; environment and have denote do a giant substitution
-       (let ([e (cur->datum #'e)]
-             [id (syntax->datum #'id)])
-         (extend-env/term! gamma id (type-infer/term e))
-         (add-binding/term! id e)
-         #'(void))])))
-
-(require (rename-in 'sugar [module+ dep-module+]))
-(provide (rename-out [dep-module+ module+]) (all-from-out 'sugar))
-(module+ test
-  (require (submod ".." core test)))

stdlib/bool.rkt

@@ -1,19 +0,0 @@
-#lang s-exp "../redex-curnel.rkt"
-(provide bool btrue bfalse if bnot)
-
-(data bool : Type
-  (btrue : bool)
-  (bfalse : bool))
-
-(define-syntax (if syn)
-  (syntax-case syn ()
-    [(_ t s f)
-     #'(case t
-         [btrue s]
-         [bfalse f])]))
-
-(define (bnot (x : bool)) (if x bfalse btrue))
-(module+ test
-  (require rackunit)
-  (check-equal? (bnot btrue) bfalse)
-  (check-equal? (bnot bfalse) btrue))

stdlib/maybe.rkt

@@ -1,16 +0,0 @@
-#lang s-exp "../redex-curnel.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")
-  ;; TODO: Dependent pattern matching doesn't work yet
-  #;(check-equal? (case* (some bool btrue)
-                  [(none (A : Type)) bfalse]
-                  [(some (A : Type) (x : bool))
-                   (if x btrue bfalse)])
-                btrue))

stdlib/nat.rkt

@@ -1,47 +0,0 @@
-#lang s-exp "../redex-curnel.rkt"
-(require "sugar.rkt" "bool.rkt")
-;; TODO: override (all-defined-out) to enable exporting all these
-;; properly.
-(provide nat z s add1 sub1 plus nat-equal?)
-(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 (lambda (x : nat) x)]))
-(module+ test
-  (check-equal? (sub1 (s z)) z))
-
-(define plus
-  (fix (plus : (forall* (n1 : nat) (n2 : nat) nat))
-    (lambda (n1 : nat)
-      (lambda (n2 : nat)
-        (case n1
-          [z n2]
-          [s (λ (x : nat) (plus x (s n2)))])))))
-(module+ test
-  (check-equal? (plus z z) z)
-  (check-equal? (plus (s (s z)) (s (s z))) (s (s (s (s z))))))
-
-(define-rec (nat-equal? (n1 : nat) (n2 : nat) : bool)
-  (case* n1
-    [z (case* n2
-         [z btrue]
-         [(s (n3 : nat)) bfalse])]
-    [(s (n3 : nat))
-       (case* n2
-         [z btrue]
-         [(s (n4 : nat)) (nat-equal? n3 n4)])]))
-(module+ test
-  (check-equal? btrue (nat-equal? z z))
-  (check-equal? bfalse (nat-equal? z (s z)))
-  (check-equal? btrue (nat-equal? (s z) (s z))))

stdlib/prop.rkt

@@ -1,61 +0,0 @@
-#lang s-exp "../redex-curnel.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 (run 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)))
-
-;; TODO: BAH! pattern matching on inductive families is still broken.
-(define proof:and-is-symmetric
-  (lambda* (P : Type) (Q : Type) (ab : (and P Q))
-    (case* ab
-      ((conj (P : Type) (Q : Type) (x : P) (y : Q)) (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 c (conj (lambda* (A : Type) (B : Type) (a : A) (b : B) 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 c (conj (lambda* (A : Type) (B : Type) (a : A) (b : B) b)))))
-
-(qed thm:proj2 proof:proj2)
-
-(data == : (forall* (A : Type) (x : A) (-> A Type))
-  (refl : (forall* (A : Type) (x : A) (== A x x))))

stdlib/sugar.rkt

@@ -1,87 +0,0 @@
-#lang s-exp "../redex-curnel.rkt"
-(provide ->
-         ->*
-         forall*
-         lambda*
-         #%app
-         define
-         case*
-         define-type
-         define-theorem
-         qed
-         real-app
-         define-rec)
-
-(require (only-in "../redex-curnel.rkt" [#%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 (define-rec syn)
-  (syntax-case syn (:)
-    [(_ (name (a : t) ... : t_res) body)
-     #'(define name (fix (name : (forall* (a : t) ... t_res))
-                      (lambda* (a : t) ... body)))]))
-(begin-for-syntax
-  (define (rewrite-clause clause)
-    (syntax-case clause (:)
-      [((con (a : A) ...) body) #'(con (lambda* (a : A) ... body))]
-      [(e body) #'(e body)])))
-
-(define-syntax (case* syn)
-  (syntax-case syn ()
-    [(_ e clause* ...)
-     #`(case e #,@(map rewrite-clause (syntax->list #'(clause* ...))))]))
-
-(define-syntax-rule (define-theorem name prop)
-  (define name prop))
-
-;; TODO: Current implementation doesn't do beta/eta while type-checking
-;; because reasons. So manually insert a run in the type annotation
-(define-syntax-rule (qed thm pf)
-  ((lambda (x : (run thm)) Type) pf))
-

stlc.rkt

@@ -1,138 +0,0 @@
-#lang s-exp "redex-curnel.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-rec (lookup-gamma (g : gamma) (x : var) : (maybe stlc-type))
-  (case* g
-    [emp-gamma (none stlc-type)]
-    [(extend-gamma (g1 : gamma) (v1 : var) (t1 : stlc-type))
-     (if (var-equal? v1 x)
-         (some stlc-type t1)
-         (lookup-gamma g1 x))]))
-
-(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)))