Fixed reduction of (elim ==)

Fixed eliminator reduction, at least for the == type. Code currently
does the minimum required to make #23 work, but may have introduced bugs
in the process.

README.md

@@ -15,25 +15,15 @@ cur (plural curs)
 Disclaimer
 ==========
 Cur is currently under active hackery and is not fit for use for any
-particular purpose. It is fraught with unreadable code, errors,
+particular purpose. It is fraught with unreadable code, errors, and
-performance bugs, and hacks that should never have been written by a
+hacks that should never have been written by a reasonable human being.
-reasonable human being.
 These may or may not be fixed shortly.
 
 Getting started
 ===============
 
-Easy mode:
 Install cur via `raco pkg install cur`.
 
-Advanced mode:
-Cur is actually distributed as several packages.
-`cur-lib` provides the implementation and all standard
-libraries.
-`cur-doc` provides the documentation.
-`cur-test` provides a test suite and examples.
-
-
 Try it out: open up DrRacket and put the following in the definition area:
 
 ```racket
@@ -45,10 +35,6 @@ Try it out: open up DrRacket and put the following in the definition area:
 (if true
     false
     true)
-
-(: + (-> Nat Nat Nat))
-(define + plus)
-(+ z (s z))
 ```
 
 Try entering the following in the interaction area:
@@ -56,39 +42,29 @@ Try entering the following in the interaction area:
 (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`.
 
+Most of the standard library is currently undocumented, so just see the source.
+
 Going further
 =============
 
-Open up `cur-tests/cur/tests/stlc.rkt` to see an example of the
+Open up `examples/example.rkt` to see a tour of Cur's features.
-simply-typed lambda-calculus modeled in Cur, with a parser and syntax
+
-extension to enable deeply embedding.
+Open up `examples/stlc.rkt` to see an example of what advanced meta-programming can let you do.
+
+Open up `oll.rkt` to see the implementation of the meta-programs used to
+enable `examples/stlc.rkt`, including the parsers for BNF syntax and inference rule
+syntax, and Coq and LaTeX generators.
 
 Open up `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 `cur-lib/cur/stdlib/tactics` to see one way to implement tactics in Cur.
+Open up `stdlib/tactics` to see tactics, implemented entirely via
+meta-programming.
 
-Open up anything in `cur-lib/cur/stdlib/` to see some standard dependent-type
+Open up anything in `stdlib/` to see some standard dependent-type
 formalisms.
 
-Open up `cur-lib/cur/curnel/redex-core.rkt` to see the entire
+Open up `curnel/redex-core.rkt` to see the entire "trusted" (after a
-implementation of the core language, <600 lines of code.
+large test suite) core.

cur-doc/cur/info.rkt

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

cur-doc/cur/scribblings/curnel.scrbl

@@ -1,135 +0,0 @@
-#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

@@ -1,22 +0,0 @@
-#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/reflection.scrbl

@@ -1,112 +0,0 @@
-#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/bool.scrbl

@@ -1,54 +0,0 @@
-#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

@@ -1,21 +0,0 @@
-#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

@@ -1,26 +0,0 @@
-#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

@@ -1,98 +0,0 @@
-#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

@@ -1,207 +0,0 @@
-#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/typeclass.scrbl

@@ -1,42 +0,0 @@
-#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

@@ -1,6 +0,0 @@
-#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

@@ -1,562 +0,0 @@
-#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/olly.rkt

@@ -1,449 +0,0 @@
-#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

@@ -1,24 +0,0 @@
-#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

@@ -1,33 +0,0 @@
-#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

@@ -1,13 +0,0 @@
-#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

@@ -1,61 +0,0 @@
-#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

@@ -1,85 +0,0 @@
-#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

@@ -1,498 +0,0 @@
-#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/info.rkt

@@ -1,7 +0,0 @@
-#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

@@ -1,58 +0,0 @@
-#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

@@ -1,24 +0,0 @@
-#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

@@ -1,649 +0,0 @@
-#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

@@ -1,18 +0,0 @@
-#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

@@ -1,49 +0,0 @@
-#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

@@ -1,20 +0,0 @@
-#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

@@ -1,32 +0,0 @@
-#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

@@ -1,36 +0,0 @@
-#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

@@ -1,12 +0,0 @@
-#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

@@ -1,51 +0,0 @@
-#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

@@ -1,36 +0,0 @@
-#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

@@ -1,28 +0,0 @@
-#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

@@ -1,132 +0,0 @@
-#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

@@ -1,16 +0,0 @@
-#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

@@ -1,7 +0,0 @@
-#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

@@ -1,6 +0,0 @@
-#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))

curnel/redex-lang.rkt

@@ -2,7 +2,7 @@
 ;; This module just provide module language sugar over the redex model.
 
 (require
-  (except-in "redex-core.rkt" apply)
+  "redex-core.rkt"
   redex/reduction-semantics
   racket/provide-syntax
   (for-syntax
@@ -11,7 +11,7 @@
     racket/syntax
     (except-in racket/provide-transform export)
     racket/require-transform
-    (except-in "redex-core.rkt" apply)
+    (except-in "redex-core.rkt" remove)
     redex/reduction-semantics))
 (provide
   ;; Basic syntax
@@ -30,10 +30,12 @@
     [dep-provide provide]
     [dep-require require]
 
+    [dep-lambda lambda]
     [dep-lambda λ]
     [dep-app #%app]
 
-    [dep-forall Π]
+    [dep-forall forall]
+    [dep-forall ∀]
 
     [dep-inductive data]
 
@@ -51,42 +53,39 @@
   define-syntax
   begin-for-syntax
   define-for-syntax
+  (for-syntax (all-from-out syntax/parse))
   syntax-case
   syntax-rules
   define-syntax-rule
+  (for-syntax (all-from-out racket))
+  ;; reflection
   (for-syntax
-   (all-from-out syntax/parse)
-   (all-from-out racket)
-   (all-from-out racket/syntax)
-    cur->datum
     cur-expand
-    cur-type-infer
+    type-infer/syn
-    cur-type-check?
+    type-check/syn?
-    cur-normalize
+    normalize/syn
-    cur-step
     cur-equal?))
 
 (begin-for-syntax
-  ;; TODO: Gamma and Delta seem to get reset inside a module+
+  ;; 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 term environment ~s" x))
+          (error 'core-error "We built a bad gamma ~s" x))
         x)))
 
-  (define delta
+  (define sigma
     (make-parameter
       (term ∅)
       (lambda (x)
-        (unless (Δ? x)
+        (unless (Σ? x)
-          (error 'core-error "We built a bad inductive declaration ~s" x))
+          (error 'core-error "We built a bad sigma ~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)))
+    (term (,(env) ,x : ,t)))
 
   (define (extend-Γ/term! env x t) (env (extend-Γ/term env x t)))
 
@@ -95,46 +94,45 @@
 
   (define (extend-Γ/syn! env x t) (env (extend-Γ/syn env x t)))
 
-  (define (extend-Δ/term env x t c*)
+  (define (extend-Σ/term env x t c*)
-    (term (Δ-set ,(env) ,x ,t (,@c*))))
+    (term (,(env) (,x : ,t (,@c*)))))
 
-  (define (extend-Δ/term! env x t c*)
+  (define (extend-Σ/term! env x t c*)
-    (env (extend-Δ/term env x t c*)))
+    (env (extend-Σ/term env x t c*)))
 
-  (define (extend-Δ/syn env x t c*)
+  (define (extend-Σ/syn env x t c*)
-    (extend-Δ/term env (syntax->datum x) (cur->datum t)
+    (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*)
+  (define (extend-Σ/syn! env x t c*)
-    (env (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)))
-  (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)
+  ;; TODO: Still absurdly slow. Probably doing n^2 checks of sigma and
-    (term (subst-all ,t ,(first (bind-subst)) ,(second (bind-subst)))))
+  ;; gamma. And lookup on sigma, gamma are linear, so probably n^2 lookup time.
-
   (define (type-infer/term t)
-    (let ([t (judgment-holds (type-infer ,(delta) ,(gamma) ,(subst-bindings t) t_0) t_0)])
+    (let ([t (judgment-holds (type-infer ,(sigma) ,(gamma) ,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))
+    (and (judgment-holds (type-check ,(sigma) ,(gamma) ,e ,t)) #t))
+
+  (define (syntax->curnel-syntax syn) (denote syn (cur->datum syn)))
+
+  (define (denote syn t)
+    (quasisyntax/loc
+      syn
+      (term (reduce #,(sigma) (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)))
@@ -150,14 +148,14 @@
 
   ;; Only type-check at the top-level, to prevent exponential
   ;; type-checking. Redex is expensive enough.
+  ;; TODO: This results in less good error messages. Add an
+  ;; algorithm to find the smallest ill-typed term.
   (define inner-expand? (make-parameter #f))
 
-  ;; Reifiy cur syntax into curnel datum
+  ;; Expand a piece of syntax into a curnel redex term
   (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)
@@ -165,7 +163,7 @@
             #:datum-literals (elim Π λ : Unv)
             [x:id (syntax->datum #'x)]
             [(subst-all e _ _) (syntax->datum #'e)]
-            [(reduce Δ e) (cur->datum #'e)]
+            [(reduce Σ e) (cur->datum #'e)]
             [(term e) (cur->datum #'e)]
             [(Unv i) (term (Unv ,(syntax->datum #'i)))]
             ;; TODO: should really check that b is one of the binders
@@ -177,78 +175,45 @@
                     [e (parameterize ([gamma (extend-Γ/term gamma x t)])
                          (cur->datum #'e))])
                (term (,(syntax->datum #'b) (,x : ,t) ,e)))]
-            [(elim D motive (i ...) (m ...) d)
+            [(elim t1 t2)
-             (term (elim ,(cur->datum #'D) ,(cur->datum #'motive)
+             (let* ([t1 (cur->datum #'t1)]
-                         ,(map cur->datum (syntax->list #'(i ...)))
+                    [t2 (cur->datum #'t2)])
-                         ,(map cur->datum (syntax->list #'(m ...)))
+               (term ((elim ,t1) ,t2)))]
-                         ,(cur->datum #'d)))]
             [(#%app e1 e2)
              (term (,(cur->datum #'e1) ,(cur->datum #'e2)))]))))
-    (unless (or (inner-expand?) (type-infer/term reified-term))
+    (unless (and inner-expand? (type-infer/term reified-term))
-      #;(printf "Delta: ~s~nGamma: ~s~n" (delta) (gamma))
+      ;; TODO: is this really a syntax error?
-      (raise-syntax-error 'cur "term is ill-typed:" reified-term syn))
+      (raise-syntax-error 'cur "term is ill-typed:"
+                          (begin (printf "Sigma: ~s~nGamma: ~s~n" (sigma) (gamma))
+                                 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
-
+  #| TODO:
-  (define (cur-normalize syn)
+   | Why is this not just (define (normalize/syn syn) (denote syn syn))?
-    (datum->cur
+   | Well, because that has a very different meaning. Apparently.
+   |#
+  (define (normalize/syn syn)
+    (denote
       syn
-      (eval-cur syn)))
+      (term (reduce ,(sigma) (subst-all ,(cur->datum syn) ,(first (bind-subst)) ,(second (bind-subst)))))))
 
-  (define (cur-step syn)
+  (define (run-cur->datum syn)
-    (datum->cur
+    (cur->datum (normalize/syn syn)))
-      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))
+    (and (judgment-holds (equivalent ,(sigma) ,(run-cur->datum e1) ,(run-cur->datum e2)) #t)))
 
-  ;; TODO: Document local-env
+  ;; TODO: OOps, type-infer doesn't return a cur term but a redex term
-  (define (cur-type-infer syn #:local-env [env '()])
+  ;; wrapped in syntax bla. This is bad.
-    (parameterize ([gamma (for/fold ([gamma (gamma)])
+  (define (type-infer/syn syn)
-                                    ([(x t) (in-dict env)])
+    (let ([t (type-infer/term (run-cur->datum syn))])
-                            (extend-Γ/syn (thunk gamma) x t))])
+      (and t (datum->syntax syn t))))
-      (let ([t (type-infer/term (eval-cur syn))])
-        (and t (datum->cur syn t)))))
 
-  (define (cur-type-check? syn type)
+  (define (type-check/syn? syn type)
-    (type-check/term? (eval-cur syn) (eval-cur type)))
+    (type-check/term? (run-cur->datum syn) (run-cur->datum 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
@@ -273,8 +238,8 @@
   (define (cur-identifier-bound? id)
     (let ([x (syntax->datum id)])
       (and (x? x)
-        (or (term (Γ-ref ,(gamma) ,x))
+        (or (term (lookup-Γ ,(gamma) ,x))
-          (term (Δ-ref-type ,(delta) ,x))))))
+          (term (lookup-Σ ,(sigma) ,x))))))
 
   (define (filter-cur-exports syn modes)
     (partition (compose cur-identifier-bound? export-local-id)
@@ -290,18 +255,18 @@
            (set! envs (for/list ([e cur])
            (let* ([x (syntax->datum (export-local-id e))]
                   [t (type-infer/term x)]
-                  [env (if (term (lookup ,(gamma) ,x)) #'gamma #'delta)])
+                  [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 delta-out bind-out)
+    [(_ gamma-out sigma-out bind-out)
      (begin
        #`(begin-for-syntax
           (define gamma-out (term #,(gamma)))
-          (define delta-out (term #,(delta)))
+          (define sigma-out (term #,(sigma)))
           (define bind-out '#,(bind-subst))))]))
 
 ;; TODO: This can only handle a single provide form, otherwise generates multiple *-out
@@ -313,14 +278,14 @@
         | Ignoring the built envs above, for now.  The local-lift export seems to get executed before
         | the filtered environment is built.
         |#
-       ;; TODO: rename out will need to rename variables in gamma and ; delta.
+       ;; TODO: rename out will need to rename variables in gamma and ; sigma.
        (syntax-local-lift-module-end-declaration
-         #`(export-envs gamma-out delta-out bind-out))
+         #`(export-envs gamma-out sigma-out bind-out))
        #`(provide (extend-env-and-provide e ...)
-                  (for-syntax gamma-out delta-out bind-out)))]))
+                  (for-syntax gamma-out sigma-out bind-out)))]))
 (begin-for-syntax
   (define out-gammas #`())
-  (define out-deltas #`())
+  (define out-sigmas #`())
   (define out-binds #`())
   (define gn 0)
   (define sn 0)
@@ -340,21 +305,21 @@
                        ;; TODO: Do not DIY gensym
                        (set! gn (add1 gn))
                        (set! out-gammas
-                             #`(#,@out-gammas (gamma (term (Γ-union
+                             #`(#,@out-gammas (gamma (term (append-Γ
                                                              ,(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)
+                    [(equal? (import-src-sym imp) 'sigma-out)
                      (let ([new-id (format-id (import-orig-stx imp)
-                                              "delta-out~a" sn)])
+                                              "sigma-out~a" sn)])
                        ;; TODO: Fewer set!s
                        ;; TODO: Do not DIY gensym
                        (set! sn (add1 sn))
-                       (set! out-deltas
+                       (set! out-sigmas
-                             #`(#,@out-deltas (delta (term (Δ-union
+                             #`(#,@out-sigmas (sigma (term (append-Σ
-                                                             ,(delta)
+                                                             ,(sigma)
                                                              ,#,new-id)))))
                        (cons (struct-copy import imp [local-id new-id])
                              imports))]
@@ -383,10 +348,11 @@
       (syntax-case syn ()
         [(_ e ...) (filter-cur-imports #'(e ...))]))))
 
-;; TODO: rename in will need to rename variables in gamma and delta.
+;; 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-deltas
+    [(_) #`(begin-for-syntax #,@out-gammas #,@out-sigmas
                              #,@out-binds)]))
 
 (define-syntax (dep-require syn)
@@ -402,7 +368,7 @@
      #`(module+ name
          (begin-for-syntax
            (gamma (term #,(gamma)))
-           (delta (term #,(delta)))
+           (sigma (term #,(sigma)))
            (bind-subst '#,(bind-subst)))
          body ...)]))
 
@@ -410,46 +376,45 @@
 ;; Core wrapper macros
 ;;
 ;; TODO: Can these be simplified further?
+#;(define-syntax (dep-datum syn) (denote #'syn))
 (define-syntax (dep-lambda syn)
-  (syntax-parse syn
+  (syntax-case syn (:)
-    #:datum-literals (:)
+    [(_ (x : t) e)
-    [(_ (x:id : t) e)
      (syntax->curnel-syntax
        (quasisyntax/loc syn (λ (x : t) e)))]))
 
 (define-syntax (dep-app syn)
-  (syntax-parse syn
+  (syntax-case syn ()
-    [(_ e1:expr e2:expr)
+    [(_ e1 e2)
      (syntax->curnel-syntax
        (quasisyntax/loc syn (#%app e1 e2)))]))
 
 (define-syntax (dep-forall syn)
-  (syntax-parse syn
+  (syntax-case syn (:)
-    #:datum-literals (:)
+    [(_ (x : t) e)
-    [(_ (x:id : t) e)
      (syntax->curnel-syntax
        (quasisyntax/loc syn (Π (x : t) e)))]))
 
 (define-syntax (Type syn)
-  (syntax-parse syn
+  (syntax-case syn ()
-    [(_ i:nat)
+    [(_ i)
      (syntax->curnel-syntax
        (quasisyntax/loc syn (Unv i)))]
     [_ (quasisyntax/loc syn (Type 0))]))
 
 (define-syntax (dep-inductive syn)
-  (syntax-parse syn
+  (syntax-case syn (:)
-    #:datum-literals (:)
+    [(_ i : ti (x1 : t1) ...)
-    [(_ i:id : ti (x1:id : t1) ...)
+     ;; TODO: Probably should occur only in definition context? and also, should not really produce void
      (begin
-       (extend-Δ/syn! delta #'i #'ti #'((x1 : t1) ...))
+       (extend-Σ/syn! sigma #'i #'ti #'((x1 : t1) ...))
        #'(void))]))
 
 (define-syntax (dep-elim syn)
-  (syntax-parse syn
+  (syntax-case syn ()
-    [(_ D:id motive (i ...) (m ...) e)
+    [(_ D T)
      (syntax->curnel-syntax
-       (quasisyntax/loc syn (elim D motive (i ...) (m ...) e)))]))
+       (quasisyntax/loc syn (elim D T)))]))
 
 (define-syntax-rule (dep-void) (void))
 
@@ -461,20 +426,26 @@
      (let ([t (core-expand #'id)])
        (if (equal? (syntax->datum t) '(void))
            #'(void)
-           (syntax->curnel-syntax t)))]))
+           (normalize/syn t)))]))
 
 (define-syntax (dep-top-interaction syn)
   (syntax-case syn ()
     [(_ . form)
      (begin
-       ;; TODO NB FIXME: HACKS
+       ;; TODO NB FIXME: HACKS HACKS HACKS
        #`(begin
-           (export-envs gamma-out delta-out bind-out)
+           (export-envs gamma-out sigma-out bind-out)
            (begin-for-syntax
-             (define nm (map (lambda (x) (namespace-variable-value x #f (lambda x #t))) (namespace-mapped-symbols)))
+             ;; Try to detect when we are in DrRacket, and do the right thing.
-             (bind-subst (first (memf subst? nm)))
+             (when (equal? 'debug-error-display-handler (object-name (error-display-handler)))
-             (gamma (first (memf Γ? nm)))
+                 (cond
-             (delta (first (memf Δ? nm))))
+                   [(null? (namespace-mapped-symbols))
+                    (displayln "You will need to add a (provide ...) in the definitions area for the evaluator to load Cur definitions correctly.")]
+                   [(eq? 3 (length (namespace-mapped-symbols)))
+                    (bind-subst (namespace-variable-value (first (namespace-mapped-symbols))))
+                    (gamma (namespace-variable-value (second (namespace-mapped-symbols))))
+                    (sigma (namespace-variable-value (third (namespace-mapped-symbols))))]
+                   [else (void)])))
           form))]))
 
 (define-syntax (dep-define syn)
@@ -482,8 +453,6 @@
     [(_ 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))]))

examples/stlc.rkt

@@ -0,0 +1,144 @@
+#lang s-exp "../cur.rkt"
+(require
+  "../stdlib/nat.rkt"
+  "../stdlib/sugar.rkt"
+  "../oll.rkt"
+  "../stdlib/maybe.rkt"
+  "../stdlib/bool.rkt"
+  "../stdlib/prop.rkt")
+
+(define-language stlc
+  #:vars (x)
+  #:output-coq "stlc.v"
+  #:output-latex "stlc.tex"
+  (val  (v)   ::= true false unit)
+  ;; TODO: Allow datum as terminals
+  (type (A B) ::= boolty unitty (-> A B) (* A A))
+  (term (e)   ::= x v (app e e) (lambda (x : A) e) (cons e e)
+                  (let (x x) = e in e)))
+
+;; TODO: Abstract this over stlc-type, and provide from in OLL
+(data Gamma : Type
+  (emp-gamma : Gamma)
+  (extend-gamma : (->* Gamma Var stlc-type Gamma)))
+
+(define (lookup-gamma (g : Gamma) (x : Var))
+  (case* Gamma Type g () (lambda* (g : Gamma) (Maybe stlc-type))
+    [emp-gamma (none stlc-type)]
+    [(extend-gamma (g1 : Gamma) (v1 : Var) (t1 : stlc-type))
+     IH: ((ih-g1 : (Maybe stlc-type)))
+     (if (var-equal? v1 x)
+         (some stlc-type t1)
+         ih-g1)]))
+
+(define-relation (has-type Gamma stlc-term stlc-type)
+  #:output-coq "stlc.v"
+  #:output-latex "stlc.tex"
+  [(g : Gamma)
+   ------------------------ T-Unit
+   (has-type g (stlc-val-->-stlc-term stlc-unit) stlc-unitty)]
+
+  [(g : Gamma)
+   ------------------------ T-True
+   (has-type g (stlc-val-->-stlc-term stlc-true) stlc-boolty)]
+
+  [(g : Gamma)
+   ------------------------ T-False
+   (has-type g (stlc-val-->-stlc-term stlc-false) stlc-boolty)]
+
+  [(g : Gamma) (x : Var) (t : stlc-type)
+   (== (Maybe stlc-type) (lookup-gamma g x) (some stlc-type t))
+   ------------------------ T-Var
+   (has-type g (Var-->-stlc-term x) t)]
+
+  [(g : Gamma) (e1 : stlc-term) (e2 : stlc-term)
+               (t1 : stlc-type) (t2 : stlc-type)
+   (has-type g e1 t1)
+   (has-type g e2 t2)
+   ---------------------- T-Pair
+   (has-type g (stlc-cons e1 e2) (stlc-* t1 t2))]
+
+  [(g : Gamma) (e1 : stlc-term) (e2 : stlc-term)
+               (t1 : stlc-type) (t2 : stlc-type)
+               (t : stlc-type)
+               (x : Var) (y : Var)
+   (has-type g e1 (stlc-* t1 t2))
+   (has-type (extend-gamma (extend-gamma g x t1) y t2) e2 t)
+   ---------------------- T-Let
+   (has-type g (stlc-let x y e1 e2) t)]
+
+  [(g : Gamma) (e1 : stlc-term) (t1 : stlc-type) (t2 : stlc-type) (x : Var)
+   (has-type (extend-gamma g x t1) e1 t2)
+   ---------------------- T-Fun
+   (has-type g (stlc-lambda x t1 e1) (stlc--> t1 t2))]
+
+  [(g : Gamma) (e1 : stlc-term) (e2 : stlc-term)
+               (t1 : stlc-type) (t2 : stlc-type)
+   (has-type g e1 (stlc--> t1 t2))
+   (has-type g e2 t1)
+   ---------------------- T-App
+   (has-type g (stlc-app e1 e2) t2)])
+
+;; A parser, for a deep-embedding of STLC.
+;; TODO: We should be able to generate these
+;; TODO: When generating a parser, will need something like (#:name app (e e))
+;; so I can name a constructor without screwing with syntax.
+(begin-for-syntax
+  (define index #'z))
+(define-syntax (begin-stlc syn)
+  (set! index #'z)
+  (let stlc ([syn (syntax-case syn () [(_ e) #'e])])
+    (syntax-parse syn
+      #:datum-literals (lambda : prj * -> quote let in cons bool)
+      [(lambda (x : t) e)
+       (let ([oldindex index])
+         (set! index #`(s #,index))
+         ;; Replace x with a de bruijn index, by running a CIC term at
+         ;; compile time.
+         (normalize/syn
+           #`((lambda* (x : stlc-term)
+                      (stlc-lambda (avar #,oldindex) #,(stlc #'t) #,(stlc #'e)))
+             (Var-->-stlc-term (avar #,oldindex)))))]
+      [(quote (e1 e2))
+       #`(stlc-cons #,(stlc #'e1) #,(stlc #'e2))]
+      [(let (x y) = e1 in e2)
+       (let* ([y index]
+              [x #`(s #,y)])
+         (set! index #`(s (s #,index)))
+         #`((lambda* (x : stlc-term) (y : stlc-term)
+              (stlc-let (avar #,x) (avar #,y) #,(stlc #'t) #,(stlc #'e1)
+                   #,(stlc #'e2)))
+            (Var-->-stlc-term (avar #,x))
+            (Var-->-stlc-term (avar #,y))))
+       #`(let x  i #,(stlc #'e1))]
+      [(e1 e2)
+       #`(stlc-app #,(stlc #'e1) #,(stlc #'e2))]
+      [() #'(stlc-val-->-stlc-term stlc-unit)]
+      [#t #'(stlc-val-->-stlc-term stlc-true)]
+      [#f #'(stlc-val-->-stlc-term stlc-false)]
+      [(t1 * t2)
+       #`(stlc-* #,(stlc #'t1) #,(stlc #'t2))]
+      [(t1 -> t2)
+       #`(stlc--> #,(stlc #'t1) #,(stlc #'t2))]
+      [bool #`stlc-boolty]
+      [e
+       (if (eq? 1 (syntax->datum #'e))
+           #'stlc-unitty
+           #'e)])))
+
+(module+ test
+  (require rackunit)
+  (check-equal?
+    (begin-stlc (lambda (x : 1) x))
+    (stlc-lambda (avar z) stlc-unitty (Var-->-stlc-term (avar z))))
+  (check-equal?
+    (begin-stlc ((lambda (x : 1) x) ()))
+    (stlc-app (stlc-lambda (avar z) stlc-unitty (Var-->-stlc-term (avar z)))
+              (stlc-val-->-stlc-term stlc-unit)))
+  (check-equal?
+    (begin-stlc '(() ()))
+    (stlc-cons (stlc-val-->-stlc-term stlc-unit)
+               (stlc-val-->-stlc-term stlc-unit)))
+  (check-equal?
+    (begin-stlc #t)
+    (stlc-val-->-stlc-term stlc-true)))

info.rkt

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

lang/reader.rkt

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

oll.rkt

@@ -0,0 +1,405 @@
+#lang s-exp "cur.rkt"
+;; OLL: The OTT-Like Library
+;; TODO: Automagically create a parser from bnf grammar
+(require
+  "stdlib/sugar.rkt"
+  "stdlib/nat.rkt"
+  (only-in "curnel/redex-lang.rkt" [#%app real-app] [elim real-elim]))
+
+(provide
+  define-relation
+  define-language
+  Var
+  avar
+  var-equal?
+  generate-coq
+  #;(rename-out [oll-define-theorem define-theorem]))
+
+(begin-for-syntax
+  (define-syntax-class dash
+    (pattern x:id
+             #:fail-unless (regexp-match #rx"-+" (symbol->string (syntax-e #'x)))
+             "Invalid dash"))
+
+  (define-syntax-class decl (pattern (x:id (~datum :) t:id)))
+
+  ;; TODO: Automatically infer decl ... by binding all free identifiers?
+  ;; TODO: Automatically infer decl ... for meta-variables that are the
+  ;; same as bnf grammar.
+  (define-syntax-class inferrence-rule
+    (pattern (d:decl ...
+              x*:expr ...
+              line:dash lab:id
+              (name:id y* ...))
+              #:with rule #'(lab : (forall* d ...
+                                     (->* x* ... (name y* ...))))
+              ;; TODO: convert meta-vars such as e1 to e_1
+              #:attr latex (format "\\inferrule~n{~a}~n{~a}"
+                             (string-trim
+                               (for/fold ([str ""])
+                                        ([hyp (syntax->datum #'(x* ...))])
+                                 (format "~a~a \\+" str hyp))
+                               " \\+"
+                               #:left? #f)
+                             (format "~a" (syntax->datum #'(name y* ...)))))))
+(define-syntax (define-relation syn)
+  (syntax-parse syn
+    [(_ (n:id types* ...)
+        (~optional (~seq #:output-coq coq-file:str))
+        (~optional (~seq #:output-latex latex-file:str))
+        rules:inferrence-rule ...)
+     #:fail-unless (andmap (curry equal? (length (syntax->datum #'(types* ...))))
+                           (map length (syntax->datum #'((rules.y* ...)
+                                                          ...))))
+     "Mismatch between relation declared and relation definition"
+     #:fail-unless (andmap (curry equal? (syntax->datum #'n))
+                           (syntax->datum #'(rules.name ...)))
+     "Mismatch between relation declared name and result of inference rule"
+      (let ([output #`(data n : (->* types* ... Type) rules.rule ...)])
+        ;; TODO: Pull this out into a separate function and test. Except
+        ;; that might make using attritbutes more difficult.
+        (when (attribute latex-file)
+          (with-output-to-file (syntax->datum #'latex-file)
+            (thunk
+              (printf (format "\\fbox{$~a$}$~n$\\begin{mathpar}~n~a~n\\end{mathpar}$$"
+                       (syntax->datum #'(n types* ...))
+                       (string-trim
+                         (for/fold ([str ""])
+                                   ([rule (attribute rules.latex)])
+                           (format "~a~a\\and~n" str rule))
+                         "\\and"
+                         #:left? #f))))
+            #:exists 'append))
+        #`(begin
+            #,@(if (attribute coq-file)
+                   #`((generate-coq #:file coq-file #:exists
+                                    'append #,output))
+                   #'())
+               #,output))]))
+
+(begin-for-syntax
+  (require racket/syntax)
+  (define (new-name name . id*)
+    (apply format-id name (for/fold ([str "~a"])
+                                    ([_ id*])
+                            (string-append str "-~a")) name (map syntax->datum id*)))
+
+  (define (fresh-name id)
+    (datum->syntax id (gensym (syntax->datum id)))))
+
+(module+ test
+  (begin-for-syntax
+    (require rackunit)
+    (define (check-id-equal? v1 v2)
+      (check-equal?
+        (syntax->datum v1)
+        (syntax->datum v2)))
+    (define (check-id-match? v1 v2)
+       (check-regexp-match
+         v1
+         (symbol->string (syntax->datum v2))))
+    (check-id-match?
+      #px"term\\d+"
+      (fresh-name #'term))
+    (check-id-equal?
+      #'stlc-lambda
+      (new-name #'stlc #'lambda))
+    (check-id-match?
+      #px"stlc-term\\d+"
+      (new-name #'stlc (fresh-name #'term)))))
+
+;; TODO: Oh, this is a mess. Rewrite it.
+(begin-for-syntax
+  (define lang-name (make-parameter #'name))
+  (define nts (make-parameter (make-immutable-hash)))
+
+  (define-syntax-class nt
+    (pattern e:id #:fail-unless (hash-has-key? (nts) (syntax->datum #'e)) #f
+             #:attr name (hash-ref (nts) (syntax->datum #'e))
+             #:attr type (hash-ref (nts) (syntax->datum #'e))))
+
+  (define (flatten-args arg arg*)
+    (for/fold ([ls (syntax->list arg)])
+              ([e (syntax->list arg*)])
+      (append ls (syntax->list e))))
+
+  (define-syntax-class (right-clause type)
+    #;(pattern (~datum var)
+             #:attr clause-context #`(#,(new-name (lang-name) #'var) :
+                                      (-> #,(hash-ref (nts) 'var) #,(hash-ref (nts) type)))
+             #:attr name #'var
+             #:attr arg-context #'(var))
+    (pattern e:nt
+             #:attr clause-context #`(#,(new-name #'e.name #'->
+                                                  (hash-ref (nts) type)) :
+                                      (-> e.type #,(hash-ref (nts) type)))
+             #:attr name (fresh-name #'e.name)
+             #:attr arg-context #'(e.type))
+    (pattern x:id
+             #:attr clause-context #`(#,(new-name (lang-name) #'x) :
+                                      #,(hash-ref (nts) type))
+             #:attr name (new-name (lang-name) #'x)
+             #:attr arg-context #'())
+    (pattern ((~var e (right-clause type)) (~var e* (right-clause type)) ...)
+             #:attr name (fresh-name #'e.name)
+             #:attr clause-context #`(e.name : (->* #,@(flatten-args #'e.arg-context #'(e*.arg-context ...))
+                                                    #,(hash-ref (nts) type)))
+             #:attr arg-context #`(#,@(flatten-args #'e.arg-context #'(e*.arg-context ...)))))
+
+  (define-syntax-class (right type)
+    (pattern ((~var r (right-clause type)) ...)
+             #:attr clause #'(r.clause-context ...)))
+
+  #;(define-syntax-class left
+    (pattern (type:id (nt*:id ...+))
+             #:do ))
+
+  (define-syntax-class nt-clauses
+    (pattern ((type:id (nt*:id ...+)
+              (~do (nts (for/fold ([ht (nts)])
+                                  ([nt (syntax->datum #'(type nt* ...))])
+                          (hash-set ht nt (new-name (lang-name) #'type)))))
+              (~datum ::=)
+              . (~var rhs* (right (syntax->datum #'type)))) ...)
+             #:with defs (with-syntax ([(name* ...)
+                                        (map (λ (x) (hash-ref (nts) x))
+                                             (syntax->datum #'(type ...)))])
+                           #`((data name* : Type . rhs*.clause)
+                              ...)))))
+
+(begin-for-syntax
+  ;; TODO: More clever use of syntax-parse would enable something akin to what
+  ;; define-relation is doing---having attributes that contain the latex
+  ;; code for each clause.
+  ;; TODO: convert meta-vars such as e1 to e_1
+  (define (output-latex-bnf vars clauses)
+    (format "$$\\begin{array}{lrrl}~n~a~n\\end{array}$$"
+      (for/fold ([str ""])
+                ([clause (syntax->list clauses)])
+        (syntax-parse clause
+          #:datum-literals (::=)
+          [(type:id (nonterminal:id ...) ::= exprs ...)
+           (format "\\mbox{\\textit{~a}} & ~a & \\bnfdef & ~a\\\\~n"
+                   (symbol->string (syntax->datum #'type))
+                   (string-trim
+                     (for/fold ([str ""])
+                               ([nt (syntax->datum #'(nonterminal ...))])
+                       (format "~a~a," str nt))
+                     ","
+                     #:left? #f)
+                   (string-trim
+                     (for/fold ([str ""])
+                               ([expr (syntax->datum #'(exprs ...))])
+                       (format "~a~a \\bnfalt " str expr))
+                     " \\bnfalt "
+                     #:left? #f))]))))
+  (define (generate-latex-bnf file-name vars clauses)
+    (with-output-to-file file-name
+      (thunk (printf (output-latex-bnf vars clauses)))
+      #:exists 'append)))
+(module+ test
+  (require "stdlib/sugar.rkt")
+  (begin-for-syntax
+    (require rackunit)
+    (check-equal?
+      (format "$$\\begin{array}{lrrl}~n~a~n\\end{array}$$"
+        (format "\\mbox{\\textit{term}} & e & \\bnfdef & (e1 e2) \\bnfalt (lambda (x) e)\\\\~n"))
+      (output-latex-bnf #'(x)
+                    #'((term (e) ::= (e1 e2) (lambda (x) e)))))
+    (check-equal?
+      (format "$$\\begin{array}{lrrl}~n~a~n\\end{array}$$"
+        (format "\\mbox{\\textit{type}} & A,B,C & \\bnfdef & unit \\bnfalt (* A B) \\bnfalt (+ A C)\\\\~n"))
+      (output-latex-bnf #'(x)
+                    #'((type (A B C) ::= unit (* A B) (+ A C)))))))
+;; TODO: For better error messages, add context, rename some of these patterns. e.g.
+;;    (type (meta-vars) ::= ?? )
+;; TODO: Extend define-language with syntax such as ....
+;;   (term (e) ::= (e1 e2) ((lambda (x) e)
+;                           #:latex "(\\lambda ,x. ,e)"))
+(define-syntax (define-language syn)
+  (syntax-parse syn
+    [(_ name:id (~do (lang-name #'name))
+        (~do (nts (hash-set (make-immutable-hash) 'var #'Var)))
+        (~optional (~seq #:vars (x*:id ...)
+           (~do (nts (for/fold ([ht (nts)])
+                               ([v (syntax->datum #'(x* ...))])
+                       (hash-set ht v (hash-ref ht 'var)))))))
+        (~optional (~seq #:output-coq coq-file:str))
+        (~optional (~seq #:output-latex latex-file:str))
+        . clause*:nt-clauses)
+     (let ([output #`(begin . clause*.defs)])
+       (when (attribute latex-file)
+         (generate-latex-bnf (syntax->datum #'latex-file) #'vars #'clause*))
+       #`(begin
+           #,@(if (attribute coq-file)
+                 #`((generate-coq #:file coq-file #:exists 'append #,output))
+                 #'())
+           #,output))]))
+
+(data Var : Type (avar : (-> Nat Var)))
+
+(define (var-equal? (v1 : Var) (v2 : Var))
+  (case* Var Type v1 () (lambda (v : Var) Bool)
+    [(avar (n1 : Nat)) IH: ()
+     (case* Var Type v2 () (lambda (v : Var) Bool)
+       [(avar (n2 : Nat)) IH: ()
+        (nat-equal? n1 n2)])]))
+(module+ test
+  (require rackunit)
+  (check-equal?
+    (var-equal? (avar z) (avar z))
+    true)
+  (check-equal?
+    (var-equal? (avar z) (avar (s z)))
+    false))
+
+;; See stlc.rkt for examples
+
+;; Generate Coq from Cur:
+
+(begin-for-syntax
+  (define coq-defns (make-parameter ""))
+  (define (coq-lift-top-level str)
+    (coq-defns (format "~a~a~n" (coq-defns) str)))
+  ;; TODO: OOps, type-infer doesn't return a cur term but a redex syntax bla
+  (define (constructor-args syn)
+    (syntax-parse (type-infer/syn syn)
+      #:datum-literals (Π :)
+      [(Π (x:id : t) body)
+       (cons #'x (constructor-args #'body))]
+      [_ null]))
+  (define (sanitize-id str)
+    (let ([replace-by `((: _) (- _))])
+      (for/fold ([str str])
+                ([p replace-by])
+        (string-replace str (symbol->string (first p))
+                        (symbol->string (second p))))))
+  (define (output-coq syn)
+    (syntax-parse (cur-expand syn #'define #'define-theorem #'qed
+                              #'begin)
+       ;; TODO: Need to add these to a literal set and export it
+       ;; Or, maybe overwrite syntax-parse
+       #:literals (lambda forall data real-app real-elim define-theorem
+                          define qed begin Type)
+       [(begin e ...)
+        (for/fold ([str ""])
+                  ([e (syntax->list #'(e ...))])
+          (format "~a~n" (output-coq e)))]
+       [(define-theorem name prop)
+        (begin
+          (fprintf (current-error-port) "Warning: If theorem ~a is not followed by a proof using (qed ...), the resulting Coq code may be malformed.~n" (output-coq #'name))
+          (coq-lift-top-level
+            (format "Theorem ~a : ~a.~n"
+                    (output-coq #'name)
+                    (output-coq #'prop)))
+          "")]
+       [(qed thm proof)
+        ;; TODO: Have some sort of coq-lift-to-theorem, to auto match
+        ;; proofs and theorems.
+        (begin
+          (coq-lift-top-level
+            (format "Proof. exact ~a. Qed.~n" (output-coq #'proof)))
+          "")]
+       [(define name:id body)
+        (begin
+          (coq-lift-top-level
+            (format "Definition ~a := ~a.~n"
+                    (output-coq #'name)
+                    (output-coq #'body)))
+          "")]
+       [(define (name:id (x:id : t) ...) body)
+        (begin
+          (coq-lift-top-level
+            (format "Function ~a ~a := ~a.~n"
+                    (output-coq #'name)
+                    (for/fold ([str ""])
+                              ([n (syntax->list #'(x ...))]
+                               [t (syntax->list #'(t ...))])
+                      (format "~a(~a : ~a) " str (output-coq n) (output-coq t)))
+                    (output-coq #'body)))
+          "")]
+       [(lambda ~! (x:id (~datum :) t) body:expr)
+        (format "(fun ~a : ~a => ~a)" (output-coq #'x) (output-coq #'t)
+                (output-coq #'body))]
+       [(forall ~! (x:id (~datum :) t) body:expr)
+        (format "(forall ~a : ~a, ~a)" (syntax-e #'x) (output-coq #'t)
+                (output-coq #'body))]
+       [(data ~! n:id (~datum :) t (x*:id (~datum :) t*) ...)
+        (begin
+          (coq-lift-top-level
+            (format "Inductive ~a : ~a :=~a."
+                   (sanitize-id (format "~a" (syntax-e #'n)))
+                   (output-coq #'t)
+                   (for/fold ([strs ""])
+                             ([clause (syntax->list #'((x* : t*) ...))])
+                     (syntax-parse clause
+                       [(x (~datum :) t)
+                        (format "~a~n| ~a : ~a" strs (syntax-e #'x)
+                          (output-coq #'t))]))))
+          "")]
+       [(Type i) "Type"]
+       [(real-elim var t)
+        (format "~a_rect" (output-coq #'var))]
+       [(real-app e1 e2)
+        (format "(~a ~a)" (output-coq #'e1) (output-coq #'e2))]
+       [e:id (sanitize-id (format "~a" (syntax->datum #'e)))])))
+
+(define-syntax (generate-coq syn)
+  (syntax-parse syn
+    [(_ (~optional (~seq #:file file))
+        (~optional (~seq #:exists flag)) body:expr)
+     (parameterize ([current-output-port (if (attribute file)
+                                             (open-output-file (syntax->datum #'file)
+                                                               #:exists
+                                                               (if (attribute flag)
+                                                                   ;; TODO: AHH WHAT?
+                                                                   (eval (syntax->datum #'flag))
+                                                                   'error))
+                                             (current-output-port))]
+                    [coq-defns ""])
+       (define output
+         (let ([body (output-coq #'body)])
+           (if (regexp-match "^\\s*$" body)
+               ""
+               (format "Eval compute in ~a." body))))
+       (displayln (format "~a~a" (coq-defns) output))
+       #'(begin))]))
+
+(module+ test
+  (begin-for-syntax
+    (check-equal?
+      (parameterize ([coq-defns ""]) (output-coq #'(data nat : Type (z : nat))) (coq-defns))
+      (format "Inductive nat : Type :=~n| z : nat.~n"))
+    (check-regexp-match
+      "(forall .+ : Type, Type)"
+      (output-coq #'(-> Type Type)))
+    (let ([t (parameterize ([coq-defns ""])
+               (output-coq #'(define-relation (meow gamma term type)
+                               [(g : gamma) (e : term) (t : type)
+                                --------------- T-Bla
+                                (meow g e t)]))
+               (coq-defns))])
+      (check-regexp-match
+        "Inductive meow : \\(forall .+ : gamma, \\(forall .+ : term, \\(forall .+ : type, Type\\)\\)\\) :="
+        (first (string-split t "\n")))
+      (check-regexp-match
+        "\\| T-Bla : \\(forall g : gamma, \\(forall e : term, \\(forall t : type, \\(\\(\\(meow g\\) e\\) t\\)\\)\\)\\)\\."
+        (second (string-split t "\n"))))
+    (let ([t (output-coq #'(elim nat Type (lambda (x : nat) nat) z
+                             (lambda* (x : nat) (ih-x : nat) ih-x)
+                             e))])
+      (check-regexp-match
+        "\\(\\(\\(\\(nat_rect \\(fun x : nat => nat\\)\\) z\\) \\(fun x : nat => \\(fun ih_x : nat => ih_x\\)\\)\\) e\\)"
+        t))
+    (check-regexp-match
+      "Theorem thm_plus_commutes : \\(forall n : nat, \\(forall m : nat, \\(\\(\\(== nat\\) \\(\\(plus n\\) m\\)\\) \\(\\(plus m\\) n\\)\\)\\)\\).\n"
+      (parameterize ([coq-defns ""])
+        (output-coq #'(define-theorem thm:plus-commutes
+                                     (forall* (n : nat) (m : nat)
+                                              (== nat (plus n m) (plus m n)))))
+        (coq-defns)))
+    (check-regexp-match
+      "Function add1 \\(n : nat\\)  := \\(s n\\).\n"
+      (parameterize ([coq-defns ""])
+        (output-coq #'(define (add1 (n : nat)) (s n)))
+        (coq-defns)))))

scribblings/cur.scrbl

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

scribblings/curnel.scrbl

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

scribblings/defs.rkt

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

scribblings/oll.scrbl

@@ -1,12 +1,12 @@
 #lang scribble/manual
 @(require "defs.rkt")
 
-@title{Olly: Ott-like LibrarY}
+@title{OLL: Ott-like Library}
 
-@defmodule[cur/olly]
+@defmodule[cur/oll]
-Olly provides syntax extensions for defining programming languages as inductive data. The library
+The OLL 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
+generating Coq definitions.  The purpose of the OLL is not to replace Ott, but to demonstrate how
 powerful syntactic meta-programming can bring features previously only provided by external tools into
 the language.
 
@@ -14,11 +14,11 @@ the language.
            maybe-vars
            maybe-output-coq
            maybe-output-latex
-           (nt-name (nt-metavar ...) maybe-bnfdef non-terminal-def ...) ...)
+           (nt-name (nt-metavars) maybe-bnfdef constructors ...) ...)
          #:grammar
          [(maybe-vars
             (code:line)
-            (code:line #:vars (nt-metavar ...)))
+            (code:line #:vars (nt-metavars ...)))
          (maybe-output-coq
             (code:line)
             (code:line #:output-coq coq-filename))
@@ -27,51 +27,26 @@ the language.
             (code:line #:output-latex latex-filename))
          (maybe-bnfdef
             (code:line)
-            (code:line ::=))
+            (code:line ::=))]]{
-	 (non-terminal-def
-	    nt-metavar
-            (code:line terminal)
-            (code:line (terminal terminal-args ...)))
-	 (terminal-args
-	    nt-metavar
-	    (code:line literal)
-	    (code:line ())
-	    (code:line (#:bind nt-metavar . terminal-args))
-	    (code:line (terminal-args terminal-args ...)))]]{
 Defines a new language by generating inductive definitions for each
-non-terminal @racket[nt-name], whose syntax is generated by
+nonterminal @racket[nt-name], whose constructors are generated by
-@racket[non-terminal-def].
+@racket[constructors]. The constructors must either with a tag that can
-Each @racket[non-terminal-def] must either be a reference to a
+be used to name the constructor, or be another meta-variable.
-previously defined non-terminal using a @racket[nt-metavar], a
+The meta-variables @racket[nt-metavars] are replaced by the corresponding
-@racket[terminal] (an identifier), or a @racket[terminal] applied to
+inductive types in @racket[constructors].
-some @racket[terminal-args].
+The name of each inductive datatype is generated by
-The @racket[terminal-args] are a limited grammar of s-expressions,
+@racket[(format-id "~a-~a" name nt-name)].
-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
+Later nonterminals can refer to prior nonterminals, but they cannot be
-@racket[nt-name] whose name @racket[nt-type] is generated by
+mutually inductive due to limitations in Cur. When nonterminals appear
-@racket[(format-id name "~a-~a" name nt-name)] and whose constructors
+in @racket[constructors], a constructor is defined that coerces one
-are generated by each @racket[non-terminal-def].
+nonterminal to another.
-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.
+representing variables in the language. These meta-variables should only
-These variables are represented as De Bruijn indices, and uses of
+appear in binding positions in @racket[constructors]. These variables
-variables in the syntax are treated as type @racket[Nat].
+are represented as De Bruijn indexes, and OLL provides some functions
-Binding positions in the syntax, represented by @racket[#:bind
+for working with De Bruijn indexes.
-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
@@ -91,8 +66,8 @@ Example:
   #:output-latex "stlc.tex"
   (val  (v)   ::= true false unit)
   (type (A B) ::= boolty unitty (-> A B) (* A A))
-  (term (e)   ::= x v (app e e) (lambda (#:bind x : A) e) (cons e e)
+  (term (e)   ::= x v (app e e) (lambda (x : A) e) (cons e e)
-                  (let (#:bind x #:bind x) = e in e)))
+                  (let (x x) = e in e)))
 ]
 
 This example is equivalent to
@@ -110,17 +85,20 @@ This example is equivalent to
   (stlc-* : (forall (x : stlc-type) (forall (y : stlc-type) stlc-type))))
 
 (data stlc-term : Type
-  (Var->-stlc-term : (forall (x : Nat) stlc-term))
+  (stlc-var-->-stlc-term : (forall (x : Var) stlc-term))
-  (stlc-val->-stlc-term : (forall (x : stlc-val) stlc-term))
+  (stlc-val-->-stlc-term : (forall (x : stlc-val) stlc-term))
-  (stlc-term-lambda : (forall (y : stlc-type)
+  (stlc-term-lambda : (forall (x : Var)
+                        (forall (y : stlc-type)
                           (forall (z : stlc-term)
-                            stlc-term)))
+                            stlc-term))))
   (stlc-term-cons : (forall (x : stlc-term) (forall (y : stlc-term) stlc-term)))
-  (stlc-term-let : (forall (e1 : stlc-term)
+  (stlc-term-let : (forall (x : Var)
+                     (forall (y : Var)
+                       (forall (e1 : stlc-term)
                          (forall (e2 : stlc-term)
-                       stlc-term))))]
+                           stlc-term))))))]
 
-@margin-note{This example is taken from @racketmodname[cur/tests/stlc]}
+@margin-note{This example is taken from @racketmodname[cur/examples/stlc]}
 }
 
 @defform[(define-relation (name args ...)
@@ -148,20 +126,20 @@ explain the syntax in detail, here is an example:
   #:output-latex "stlc.tex"
   [(g : Gamma)
    ------------------------ T-Unit
-   (has-type g (stlc-val->stlc-term stlc-unit) stlc-unitty)]
+   (has-type g (stlc-val-->-stlc-term stlc-unit) stlc-unitty)]
 
   [(g : Gamma)
    ------------------------ T-True
-   (has-type g (stlc-val->stlc-term stlc-true) stlc-boolty)]
+   (has-type g (stlc-val-->-stlc-term stlc-true) stlc-boolty)]
 
   [(g : Gamma)
    ------------------------ T-False
-   (has-type g (stlc-val->stlc-term stlc-false) stlc-boolty)]
+   (has-type g (stlc-val-->-stlc-term stlc-false) stlc-boolty)]
 
-  [(g : Gamma) (x : Nat) (t : stlc-type)
+  [(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)]
+   (has-type g (Var-->-stlc-term x) t)]
 
   [(g : Gamma) (e1 : stlc-term) (e2 : stlc-term)
                (t1 : stlc-type) (t2 : stlc-type)
@@ -173,15 +151,16 @@ explain the syntax in detail, here is an example:
   [(g : Gamma) (e1 : stlc-term) (e2 : stlc-term)
                (t1 : stlc-type) (t2 : stlc-type)
                (t : stlc-type)
+               (x : Var) (y : Var)
    (has-type g e1 (stlc-* t1 t2))
-   (has-type (extend-gamma (extend-gamma g t1) t2) e2 t)
+   (has-type (extend-gamma (extend-gamma g x t1) y t2) e2 t)
    ---------------------- T-Let
-   (has-type g (stlc-let e1 e2) t)]
+   (has-type g (stlc-let x y e1 e2) t)]
 
-  [(g : Gamma) (e1 : stlc-term) (t1 : stlc-type) (t2 : stlc-type)
+  [(g : Gamma) (e1 : stlc-term) (t1 : stlc-type) (t2 : stlc-type) (x : Var)
-   (has-type (extend-gamma g t1) e1 t2)
+   (has-type (extend-gamma g x t1) e1 t2)
    ---------------------- T-Fun
-   (has-type g (stlc-lambda t1 e1) (stlc--> t1 t2))]
+   (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)
@@ -200,11 +179,22 @@ This example is equivalent to:
   (T-Unit : (forall (g : Gamma)
               (has-type
                 g
-                (stlc-val->stlc-term stlc-unit)
+                (stlc-val-->-stlc-term stlc-unit)
                 stlc-unitty)))
   ....)]
 }
 
+@deftogether[(@defthing[Var Type]
+              @defthing[avar (forall (x : Nat) Var)])]{
+The type of a De Bruijn variable.
+}
+
+@defproc[(var-equal? [v1 Var] [v2 Var])
+         Bool]{
+A Cur procedure; returns @racket[true] if @racket[v1] and @racket[v2]
+represent the same variable.
+}
+
 @todo{Need a Scribble library for defining Cur/Racket things in the same
 library in a nice way.}
 

scribblings/reflection.scrbl

@@ -0,0 +1,89 @@
+#lang scribble/manual
+
+@(require
+   "defs.rkt"
+   (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.
+
+@(require racket/sandbox scribble/eval)
+@(define curnel-eval
+   (parameterize ([sandbox-output 'string]
+                  [sandbox-error-output 'string]
+                  [sandbox-eval-limits #f]
+                  [sandbox-memory-limit #f])
+     (make-module-evaluator "#lang cur (require cur/stdlib/bool) (require cur/stdlib/nat)")))
+
+@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 #'(lambda (x : (computed-type bla)) x))
+           (eval:result @racket[#'(lambda (x : Type) x)] "" ""))
+]
+}
+
+@defproc[(type-infer/syn [syn syntax?])
+         (or/c syntax? #f)]{
+Returns the type of the Cur term @racket[syn], or @racket[#f] if no type could be inferred.
+
+@examples[
+(eval:alts (type-infer/syn #'(lambda (x : Type) x))
+           (eval:result @racket[#'(Π (x : (Unv 0)) (Unv 0))] "" ""))
+(eval:alts (type-infer/syn #'Type)
+           (eval:result @racket[#'(Unv 1)] "" ""))
+]
+}
+
+@defproc[(type-check/syn? [syn syntax?])
+         boolean?]{
+Returns @racket[#t] if the Cur term @racket[syn] is well-typed, or @racket[#f] otherwise.
+
+@examples[
+(eval:alts (type-infer/syn #'(lambda (x : Type) x))
+           (eval:result @racket[#'(Π (x : (Unv 0)) (Unv 0))] "" ""))
+(eval:alts (type-infer/syn #'Type)
+           (eval:result @racket[#'(Unv 1)] "" ""))
+]
+}
+
+@defproc[(normalize/syn [syn syntax?])
+         syntax?]{
+Runs the Cur term @racket[syn] to a value.
+
+@examples[
+(eval:alts (normalize/syn #'((lambda (x : Type) x) Bool))
+           (eval:result @racket[#'Bool] "" ""))
+(eval:alts (normalize/syn #'(sub1 (s (s z))))
+           (eval:result @racket[#'(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? #'(lambda (a : Type) a) #'(lambda (b : Type) b))
+           (eval:result @racket[#t] "" ""))
+(eval:alts (cur-equal? #'((lambda (a : Type) a) Bool) #'Bool)
+           (eval:result @racket[#t] "" ""))
+(eval:alts (cur-equal? #'(lambda (a : Type) (sub1 (s z))) #'(lambda (a : Type) z))
+           (eval:result @racket[#f] "" ""))
+]
+}
+

scribblings/stdlib.scrbl

@@ -7,10 +7,5 @@ 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}
+@include-section{stdlib/sugar.scrbl}

scribblings/stdlib/sugar.scrbl

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

scribblings/stdlib/tactics.scrbl

@@ -1,16 +1,12 @@
 #lang scribble/manual
 
-@(require
+@(require "../defs.rkt")
-  "../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]
 
@@ -21,9 +17,11 @@ Defines a new @tech{tactic}, at @gtech{phase} 1. A @deftech{tactic} is a Racket
 number of arguments, plus the @tech{proof state}. The @tech{proof state} must be the final argument of
 the tactic.
 
-@examples[#:eval curnel-eval
+Examples:
+@racketblock[
 (define-tactic (do-nothing ps)
   ps)
+
 (define-tactic (switch-goal i ps)
   (struct-copy proof-state ps
     [current-goal i]))
@@ -53,17 +51,15 @@ Returns an empty partial @tech{proof}, i.e., the identity function.
                         [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 environment @racket[env] is a map of assumptions local to the theorem from symbols (names) to the
-
-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 list of 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 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
+The @racket[proof] is the @tech{proof} of the 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.
+The @racket[theorem] is the original statement of the theorem to be proved.
 }
 
 @defproc[(new-proof-state [prop syntax?])
@@ -144,8 +140,7 @@ 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
+Defines a new theorem.
-inhabited using the tactic language starting with @racket[proof].
 }
 
 @defform[(proof (tactic args ...) ...)]{
@@ -155,12 +150,16 @@ saved anywhere, only checked against the most recent theorem defined via @racket
 Note that the proof state is implicitly given to each call by @racket[proof] and should not appear as
 an explicit argument.
 
-@examples[#:eval curnel-eval
+Examples:
+@racketblock[
 (define-theorem a-silly-theorem (forall (x : Nat) Nat))
-(proof (intro x) (by-assumption))
+(proof
+  (intro x)
+  (by-assumption))
 
 (define-theorem falseo (forall (x : Type) x))
-(eval:alts (proof (interactive)) (void))
+(proof
+  (interactive))
 ]
 }
 

stdlib/bool.rkt

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

stdlib/maybe.rkt

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

stdlib/nat.rkt

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

stdlib/prop.rkt

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

stdlib/sugar.rkt

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

stdlib/tactics/base.rkt

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

stdlib/tactics/sartactics.rkt

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

stdlib/tactics/standard.rkt

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

stdlib/typeclass.rkt

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