NB, API changes: Faster/more primitive elim

This commit breaks previous API for eliminating inductive types.

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

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

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

README.md

@@ -45,6 +45,10 @@ 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:
@@ -52,6 +56,23 @@ 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`.
 
 Going further

cur-doc/cur/scribblings/curnel.scrbl

@@ -17,7 +17,7 @@ Edwin C. Brady.
 @(define curnel-eval (curnel-sandbox "(require cur/stdlib/nat cur/stdlib/bool cur/stdlib/prop)"))
 
 @defform*[((Type n)
-	   Type)]{
+           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
@@ -33,43 +33,44 @@ restricted impredicative universe.
           Type]
 }
 
-@defform*[((lambda (id : type-expr) body-expr)
+@defform[(λ (id : type-expr) body-expr)]{
-           (λ (id : type-expr) body-expr))]{
+Produces a single-arity procedure, binding the identifier @racket[id] of type
-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[type-expr] in @racket[body-expr] and in the type of @racket[body-expr].
-@racket[body-expr].
+Both @racket[type-expr] and @racket[body-expr] can contain non-curnel forms,
-Both @racket[type-expr] and @racket[body-expr] can contain non-curnel forms, such as macros.
+such as macros.
 
-Currently, Cur will return the underlying representation of a procedure when a @racket[lambda] is
+Currently, Cur will return the underlying representation of a procedure when a
-evaluated at the top-level. Do not rely on this representation.
+@racket[λ] is evaluated at the top-level.
+Do not rely on this representation.
 
 @examples[#:eval curnel-eval
-          (lambda (x : Type) x)]
+          (λ (x : Type) x)]
 
 @examples[#:eval curnel-eval
-          (λ (x : Type) (lambda (y : x) y))]
+          (λ (x : Type) (λ (y : x) y))]
 
 
 @defform[(#%app procedure argument)]{
-Applies the single arity @racket[procedure] to @racket[argument].
+Applies the single-arity @racket[procedure] to @racket[argument].
 }
 
 @examples[#:eval curnel-eval
-          ((lambda (x : (Type 1)) x) Type)]
+          ((λ (x : (Type 1)) x) Type)]
 
 @examples[#:eval curnel-eval
-          (#%app (lambda (x : (Type 1)) x) Type)]
+          (#%app (λ (x : (Type 1)) x) Type)]
 }
 
-@defform*[((forall (id : type-expr) body-expr)
+@defform[(Π (id : type-expr) body-expr)]{
-           (∀ (id : type-expr) body-expr))]{
+Produces a dependent function type, binding the identifier @racket[id] of type
-Produces a dependent function type, binding the identifier @racket[id] of type @racket[type-expr] in @racket[body-expr].
+@racket[type-expr] in @racket[body-expr].
 
 
 @examples[#:eval curnel-eval
-          (forall (x : Type) Type)]
+          (Π (x : Type) Type)]
 
 @examples[#:eval curnel-eval
-          (lambda (x : (forall (x : (Type 1)) Type))
+          (λ (x : (Π (x : (Type 1)) Type))
             (x Type))]
 }
 
@@ -83,32 +84,35 @@ For instance, Cur does not currently perform strict positivity checking.
           (data Bool : Type
                 (true : Bool)
                 (false : Bool))
-          ((lambda (x : Bool) x) true)
+          ((λ (x : Bool) x) true)
           (data False : Type)
-          (data And : (forall (A : Type) (forall (B : Type) Type))
+          (data And : (Π (A : Type) (Π (B : Type) Type))
-            (conj : (forall (A : Type) (forall (B : Type) (forall (a : A) (forall (b : B) ((And A) B)))))))
+            (conj : (Π (A : Type) (Π (B : Type) (Π (a : A) (Π (b : B) ((And A) B)))))))
           ((((conj Bool) Bool) true) false)]
 }
 
-@defform[(elim type motive-universe)]{
+@defform[(elim inductive-type motive (index ...) (method ...) disc)]{
-Returns the inductive eliminator for @racket[type] where the @racket[motive-universe] is the universe
+Fold over the term @racket[disc] of the inductively defined type @racket[inductive-type].
-of the motive.
+The @racket[motive] is a function that expects the indices of the inductive
-The eliminator expects the next argument to be the motive, the next @racket[N] arguments to be the methods for
+type and a term of the inductive type and produces the type that this
-each of the @racket[N] constructors of the inductive type @racket[type], the next @racket[P] arguments
+fold returns.
-to be the parameters @racket[p_0 ... p_P] of the inductive @racket[type], and the final argument to be the term to
+The type of @racket[disc] is @racket[(inductive-type index ...)].
-eliminate of type @racket[(type p_0 ... p_P)].
+@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 : (forall (n : Nat) Nat)))
+            (s : (Π (n : Nat) Nat)))
-          (((((elim Nat Type)
+          (elim Nat (λ (x : Nat) Nat)
-              (lambda (x : Nat) Nat))
+                ()
-             z)
+                (z
-            (lambda (n : Nat) (lambda (IH : Nat) n)))
+                 (λ (n : Nat) (λ (IH : Nat) n)))
-           (s z))]
+                (s z))]
 }
 
 @defform[(define id expr)]{
@@ -117,11 +121,13 @@ Binds @racket[id] to the result of @racket[expr].
 @examples[#:eval curnel-eval
           (data Nat : Type
             (z : Nat)
-            (s : (forall (n : Nat) Nat)))
+            (s : (Π (n : Nat) Nat)))
-          (define sub1 (lambda (n : Nat)
+          (define sub1 (λ (n : Nat)
-                         (((((elim Nat Type) (lambda (x : Nat) Nat))
+                         (elim Nat (λ (x : Nat) Nat)
-                           z)
+                               ()
-                          (lambda (n : Nat) (lambda (IH : Nat) n))) n)))
+                               (z
+                                (λ (n : Nat) (λ (IH : Nat) n)))
+                               n)))
           (sub1 (s (s z)))
           (sub1 (s z))
           (sub1 z)]

cur-doc/cur/scribblings/olly.scrbl

@@ -14,11 +14,11 @@ the language.
            maybe-vars
            maybe-output-coq
            maybe-output-latex
-           (nt-name (nt-metavars) maybe-bnfdef constructors ...) ...)
+           (nt-name (nt-metavar ...) maybe-bnfdef non-terminal-def ...) ...)
          #:grammar
          [(maybe-vars
             (code:line)
-            (code:line #:vars (nt-metavars ...)))
+            (code:line #:vars (nt-metavar ...)))
          (maybe-output-coq
             (code:line)
             (code:line #:output-coq coq-filename))
@@ -27,26 +27,51 @@ the language.
             (code:line #:output-latex latex-filename))
          (maybe-bnfdef
             (code:line)
-            (code:line ::=))]]{
+            (code:line ::=))
+	 (non-terminal-def
+	    nt-metavar
+            (code:line terminal)
+            (code:line (terminal terminal-args ...)))
+	 (terminal-args
+	    nt-metavar
+	    (code:line literal)
+	    (code:line ())
+	    (code:line (#:bind nt-metavar . terminal-args))
+	    (code:line (terminal-args terminal-args ...)))]]{
 Defines a new language by generating inductive definitions for each
-nonterminal @racket[nt-name], whose constructors are generated by
+non-terminal @racket[nt-name], whose syntax is generated by
-@racket[constructors]. The constructors must either with a tag that can
+@racket[non-terminal-def].
-be used to name the constructor, or be another meta-variable.
+Each @racket[non-terminal-def] must either be a reference to a
-The meta-variables @racket[nt-metavars] are replaced by the corresponding
+previously defined non-terminal using a @racket[nt-metavar], a
-inductive types in @racket[constructors].
+@racket[terminal] (an identifier), or a @racket[terminal] applied to
-The name of each inductive datatype is generated by
+some @racket[terminal-args].
-@racket[(format-id "~a-~a" name nt-name)].
+The @racket[terminal-args] are a limited grammar of s-expressions,
+which can reference previously defined @racket[nt-metavar]s to be
+treated as arguments, literal symbols to be treated as syntax, binding
+declarations, or a nested @racket[terminal-arg].
 
-Later nonterminals can refer to prior nonterminals, but they cannot be
+The inductive definitions are generated by generating a type for each
-mutually inductive due to limitations in Cur. When nonterminals appear
+@racket[nt-name] whose name @racket[nt-type] is generated by
-in @racket[constructors], a constructor is defined that coerces one
+@racket[(format-id name "~a-~a" name nt-name)] and whose constructors
-nonterminal to another.
+are generated by each @racket[non-terminal-def].
+For @racket[terminal]s, the constructor is a base constructor whose
+name is generated by @racket[(format-id name "~a-~a" name terminal)].
+For @racket[nt-metavar]s, the constructor is a conversion constructor
+whose name is generated by @racket[(format-id name "~a->~a" nt-type
+nt-metavar-type)] where @racket[nt-metavar-type] is the name of the
+type generated for the nonterminal to which @racket[nt-metavars] refers.
+For @racket[(terminal terminal-args ...)], the constructor is a
+function that expects term of of the types generated by
+@racket[terminal-args ...].
 
 If @racket[#:vars] is given, it should be a list of meta-variables that
-representing variables in the language. These meta-variables should only
+representing variables in the language.
-appear in binding positions in @racket[constructors]. These variables
+These variables are represented as De Bruijn indices, and uses of
-are represented as De Bruijn indexes, and Olly provides some functions
+variables in the syntax are treated as type @racket[Nat].
-for working with De Bruijn indexes.
+Binding positions in the syntax, represented by @racket[#:bind
+nt-metavar], are erased in converting to De Bruijn indices, although
+this may change if the representation of variables used by
+@racket[define-language] changes.
 
 If @racket[#:output-coq] is given, it should be a string representing a
 filename. The form @racket[define-language] will output Coq versions of
@@ -66,8 +91,8 @@ Example:
   #:output-latex "stlc.tex"
   (val  (v)   ::= true false unit)
   (type (A B) ::= boolty unitty (-> A B) (* A A))
-  (term (e)   ::= x v (app e e) (lambda (x : A) e) (cons e e)
+  (term (e)   ::= x v (app e e) (lambda (#:bind x : A) e) (cons e e)
-                  (let (x x) = e in e)))
+                  (let (#:bind x #:bind x) = e in e)))
 ]
 
 This example is equivalent to
@@ -85,20 +110,17 @@ This example is equivalent to
   (stlc-* : (forall (x : stlc-type) (forall (y : stlc-type) stlc-type))))
 
 (data stlc-term : Type
-  (stlc-var-->-stlc-term : (forall (x : Var) stlc-term))
+  (Var->-stlc-term : (forall (x : Nat) 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 (x : Var)
+  (stlc-term-lambda : (forall (y : stlc-type)
-                        (forall (y : stlc-type)
                           (forall (z : stlc-term)
-                            stlc-term))))
+                            stlc-term)))
   (stlc-term-cons : (forall (x : stlc-term) (forall (y : stlc-term) stlc-term)))
-  (stlc-term-let : (forall (x : Var)
+  (stlc-term-let : (forall (e1 : stlc-term)
-                     (forall (y : Var)
+                     (forall (e2 : stlc-term)
-                       (forall (e1 : stlc-term)
+                       stlc-term))))]
-                         (forall (e2 : stlc-term)
-                           stlc-term))))))]
 
-@margin-note{This example is taken from @racketmodname[cur/examples/stlc]}
+@margin-note{This example is taken from @racketmodname[cur/tests/stlc]}
 }
 
 @defform[(define-relation (name args ...)
@@ -126,20 +148,20 @@ explain the syntax in detail, here is an example:
   #:output-latex "stlc.tex"
   [(g : Gamma)
    ------------------------ T-Unit
-   (has-type g (stlc-val-->-stlc-term stlc-unit) stlc-unitty)]
+   (has-type g (stlc-val->stlc-term stlc-unit) stlc-unitty)]
 
   [(g : Gamma)
    ------------------------ T-True
-   (has-type g (stlc-val-->-stlc-term stlc-true) stlc-boolty)]
+   (has-type g (stlc-val->stlc-term stlc-true) stlc-boolty)]
 
   [(g : Gamma)
    ------------------------ T-False
-   (has-type g (stlc-val-->-stlc-term stlc-false) stlc-boolty)]
+   (has-type g (stlc-val->stlc-term stlc-false) stlc-boolty)]
 
-  [(g : Gamma) (x : Var) (t : stlc-type)
+  [(g : Gamma) (x : Nat) (t : stlc-type)
    (== (Maybe stlc-type) (lookup-gamma g x) (some stlc-type t))
    ------------------------ T-Var
-   (has-type g (Var-->-stlc-term x) t)]
+   (has-type g (Var->stlc-term x) t)]
 
   [(g : Gamma) (e1 : stlc-term) (e2 : stlc-term)
                (t1 : stlc-type) (t2 : stlc-type)
@@ -151,16 +173,15 @@ explain the syntax in detail, here is an example:
   [(g : Gamma) (e1 : stlc-term) (e2 : stlc-term)
                (t1 : stlc-type) (t2 : stlc-type)
                (t : stlc-type)
-               (x : Var) (y : Var)
    (has-type g e1 (stlc-* t1 t2))
-   (has-type (extend-gamma (extend-gamma g x t1) y t2) e2 t)
+   (has-type (extend-gamma (extend-gamma g t1) t2) e2 t)
    ---------------------- T-Let
-   (has-type g (stlc-let x y e1 e2) t)]
+   (has-type g (stlc-let e1 e2) t)]
 
-  [(g : Gamma) (e1 : stlc-term) (t1 : stlc-type) (t2 : stlc-type) (x : Var)
+  [(g : Gamma) (e1 : stlc-term) (t1 : stlc-type) (t2 : stlc-type)
-   (has-type (extend-gamma g x t1) e1 t2)
+   (has-type (extend-gamma g t1) e1 t2)
    ---------------------- T-Fun
-   (has-type g (stlc-lambda x t1 e1) (stlc--> t1 t2))]
+   (has-type g (stlc-lambda t1 e1) (stlc--> t1 t2))]
 
   [(g : Gamma) (e1 : stlc-term) (e2 : stlc-term)
                (t1 : stlc-type) (t2 : stlc-type)
@@ -179,22 +200,11 @@ This example is equivalent to:
   (T-Unit : (forall (g : Gamma)
               (has-type
                 g
-                (stlc-val-->-stlc-term stlc-unit)
+                (stlc-val->stlc-term stlc-unit)
                 stlc-unitty)))
   ....)]
 }
 
-@deftogether[(@defthing[Var Type]
-              @defthing[avar (forall (x : Nat) Var)])]{
-The type of a De Bruijn variable.
-}
-
-@defproc[(var-equal? [v1 Var] [v2 Var])
-         Bool]{
-A Cur procedure; returns @racket[true] if @racket[v1] and @racket[v2]
-represent the same variable.
-}
-
 @todo{Need a Scribble library for defining Cur/Racket things in the same
 library in a nice way.}
 

cur-doc/cur/scribblings/reflection.scrbl

@@ -25,61 +25,61 @@ phase 1 in Cur.}
 
 @examples[
 (eval:alts (define-syntax-rule (computed-type _) Type) (void))
-(eval:alts (cur-expand #'(lambda (x : (computed-type bla)) x))
+(eval:alts (cur-expand #'(λ (x : (computed-type bla)) x))
-           (eval:result @racket[#'(lambda (x : Type) x)] "" ""))
+           (eval:result @racket[#'(λ (x : Type) x)] "" ""))
 ]
 }
 
-@defproc[(type-infer/syn [syn syntax?])
+@defproc[(cur-type-infer [syn syntax?])
          (or/c syntax? #f)]{
 Returns the type of the Cur term @racket[syn], or @racket[#f] if no type could be inferred.
 
 @examples[
-(eval:alts (type-infer/syn #'(lambda (x : Type) x))
+(eval:alts (cur-type-infer #'(λ (x : Type) x))
-           (eval:result @racket[#'(forall (x : (Type 0)) (Type 0))] "" ""))
+           (eval:result @racket[#'(Π (x : (Type 0)) (Type 0))] "" ""))
-(eval:alts (type-infer/syn #'Type)
+(eval:alts (cur-type-infer #'Type)
            (eval:result @racket[#'(Type 1)] "" ""))
 ]
 }
 
-@defproc[(type-check/syn? [syn syntax?])
+@defproc[(cur-type-check? [syn syntax?])
          boolean?]{
 Returns @racket[#t] if the Cur term @racket[syn] is well-typed, or @racket[#f] otherwise.
 
 @examples[
-(eval:alts (type-check/syn? #'(lambda (x : Type) x))
+(eval:alts (cur-type-check? #'(λ (x : Type) x))
            (eval:result @racket[#t] "" ""))
-(eval:alts (type-check/syn? #'Type)
+(eval:alts (cur-type-check? #'Type)
            (eval:result @racket[#t] "" ""))
-(eval:alts (type-check/syn? #'x)
+(eval:alts (cur-type-check? #'x)
            (eval:result @racket[#f] "" ""))
 ]
 }
 
-@defproc[(normalize/syn [syn syntax?])
+@defproc[(cur-normalize [syn syntax?])
          syntax?]{
 Runs the Cur term @racket[syn] to a value.
 
 @examples[
-(eval:alts (normalize/syn #'((lambda (x : Type) x) Bool))
+(eval:alts (cur-normalize #'((λ (x : Type) x) Bool))
            (eval:result @racket[#'Bool] "" ""))
-(eval:alts (normalize/syn #'(sub1 (s (s z))))
+(eval:alts (cur-normalize #'(sub1 (s (s z))))
            (eval:result @racket[#'(s z)] "" ""))
 ]
 }
 
-@defproc[(step/syn [syn syntax?])
+@defproc[(cur-step [syn syntax?])
          syntax?]{
 Runs the Cur term @racket[syn] for one step.
 
 @examples[
-(eval:alts (step/syn #'((lambda (x : Type) x) Bool))
+(eval:alts (cur-step #'((λ (x : Type) x) Bool))
            (eval:result @racket[#'Bool] "" ""))
-(eval:alts (step/syn #'(sub1 (s (s z))))
+(eval:alts (cur-step #'(sub1 (s (s z))))
-           (eval:result @racket[#'(((((elim Nat (Type 0))
+           (eval:result @racket[#'(elim Nat (λ (x2 : Nat) Nat)
-                                      (lambda (x2 : Nat) Nat)) z)
+                                        ()
-                                    (lambda (x2 : Nat) (lambda (ih-n2 : Nat) x2)))
+                                        (z (λ (x2 : Nat) (λ (ih-n2 : Nat) x2)))
-                                   (s (s z)))] "" ""))
+                                        (s (s z)))] "" ""))
 ]
 }
 
@@ -90,11 +90,11 @@ equal modulo α and β-equivalence.
 @examples[
 
 
-(eval:alts (cur-equal? #'(lambda (a : Type) a) #'(lambda (b : Type) b))
+(eval:alts (cur-equal? #'(λ (a : Type) a) #'(λ (b : Type) b))
            (eval:result @racket[#t] "" ""))
-(eval:alts (cur-equal? #'((lambda (a : Type) a) Bool) #'Bool)
+(eval:alts (cur-equal? #'((λ (a : Type) a) Bool) #'Bool)
            (eval:result @racket[#t] "" ""))
-(eval:alts (cur-equal? #'(lambda (a : Type) (sub1 (s z))) #'(lambda (a : Type) z))
+(eval:alts (cur-equal? #'(λ (a : Type) (sub1 (s z))) #'(λ (a : Type) z))
            (eval:result @racket[#f] "" ""))
 ]
 }
@@ -106,7 +106,7 @@ Converts @racket[s] to a datum representation of the @tech{curnel form}, after e
 @examples[
 
 
-(eval:alts (cur-?datum #'(lambda (a : Type) a))
+(eval:alts (cur->datum #'(λ (a : Type) a))
            (eval:result @racket['(λ (a : (Unv 0) a))] "" ""))
 ]
 }

cur-doc/cur/scribblings/stdlib.scrbl

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

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

@@ -22,7 +22,7 @@ A syntactic form that expands to the inductive eliminator for @racket[Bool]. Thi
 
 @examples[#:eval curnel-eval
           (if true false true)
-	  (elim Bool Type (λ (x : Bool) Bool) false true true)]
+	  (elim Bool (λ (x : Bool) Bool) () (false true) true)]
 }
 
 @defproc[(not [x Bool])

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

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

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

@@ -4,7 +4,7 @@
   "../defs.rkt"
   scribble/eval)
 
-@(define curnel-eval (curnel-sandbox "(require cur/stdlib/nat cur/stdlib/bool cur/stdlib/sugar)"))
+@(define curnel-eval (curnel-sandbox "(require cur/stdlib/nat cur/stdlib/bool cur/stdlib/sugar cur/stdlib/list)"))
 
 
 @title{Sugar}
@@ -18,46 +18,38 @@ 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)
+@defform*[((-> decl decl ... type)
-          (→ t1 t2))]{
+           (→ decl decl ... type)
-A non-dependent function type Equivalent to @racket[(forall (_ : t1) t2)], where @racket[_] indicates an variable that is not used.
+	   (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))
+          (data And : (-> Type Type Type)
-            (conj : (forall (A : Type) (forall (B : Type) (-> A (-> B ((And A) B)))))))
+            (conj : (-> (A : Type) (B : Type) A B ((And A) B))))
           ((((conj Bool) Bool) true) false)]
-}
-
-@defform*[((->* t ...)
-          (→* t ...))]{
-A non-dependent multi-arity function type that supports automatic currying.
 
 @examples[#:eval curnel-eval
-          (data And : (->* Type Type Type)
+          (data And : (forall Type Type Type)
-            (conj : (forall (A : Type) (forall (B : Type) (->* A B ((And A) B))))))
+            (conj : (forall (A : Type) (B : Type) A B (And A B))))
-          ((((conj Bool) Bool) true) false)]
-}
-
-
-@defform*[((forall* (a : t) ... type)
-          (∀* (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)
+@defform*[((lambda (a : t) ... body)
-           (λ* (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)
+          ((lambda (x : Bool) (y : Bool) y) true)
           ]
 }
 
@@ -65,37 +57,43 @@ Defines a multi-arity procedure that supports automatic currying.
 Defines multi-arity procedure application via automatic currying.
 
 @examples[#:eval curnel-eval
-          (data And : (->* Type Type Type)
+          (data And : (-> Type Type Type)
-            (conj : (forall* (A : Type) (B : Type)
+	    (conj : (-> (A : Type) (B : Type) A B ((And A) B))))
-                      (->* A B ((And A) B)))))
           (conj Bool Bool true false)]
 }
 
-@defform*[((define name body)
+@defform[(: name type)]{
-           (define (name (x : t) ...) body))]{
+Declare that the @emph{function} which will be defined as @racket[name] has type @racket[type].
-Like the @racket[define] provided by @racketmodname[cur/curnel/redex-lang], but supports
+Must precede the definition of @racket[name].
-defining curried functions via @racket[lambda*].
+@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[(elim type motive-result-type e ...)]{
+@defform*[((define name body)
-Like the @racket[elim] provided by @racketmodname[cur/curnel/redex-lang], but supports
+           (define (name x ...) body)
-automatically curries the remaining arguments @racket[e ...].
+	   (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
-          (elim Bool Type (lambda (x : Bool) Bool)
+          (: id (forall (A : Type) (a : A) A))
-            false
+	  (define (id A a) a)]
-            true
-            true)]
 }
 
 @defform*[((define-type name type)
            (define-type (name (a : t) ...) body))]{
-Like @racket[define], but uses @racket[forall*] instead of @racket[lambda*].
+Like @racket[define], but uses @racket[forall] instead of @racket[lambda].
 }
 
-@defform[(match e [pattern body] ...)
+@defform[(match e [maybe-in] [maybe-return] [pattern body] ...)
          #:grammar
-         [(pattern
+         [(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.
@@ -108,6 +106,9 @@ 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]
@@ -116,42 +117,31 @@ are not inferred.
 
 @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
+A form valid only in the body of a @racket[match] clause.
-reference to the induction hypothesis for @racket[x].
+Generates a reference to the induction hypothesis for @racket[x]
-}
+inferred by a @racket[match] clause.
-
-
-@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
-          (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[(let (clause ...) body)
@@ -182,8 +172,9 @@ Check that expression @racket[e] has type @racket[type], causing a type-error if
 }
 
 @defform[(run syn)]{
-Like @racket[normalize/syn], but is a syntactic form which allows a Cur term to be written by
+Like @racket[cur-normalize], but is a syntactic form to be used in surface syntax.
-computing part of the term from another Cur term.
+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)]
@@ -191,7 +182,7 @@ computing part of the term from another Cur term.
 }
 
 @defform[(step syn)]{
-Like @racket[run], but uses @racket[step/syn] to evaluate only one step and prints intermediate
+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

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

@@ -21,7 +21,7 @@ are @racket[t ...].
 
 @examples[#:eval curnel-eval
           (typeclass (Eqv (A : Type))
-	    (equal? : (forall* (a : A) (b : A) Bool)))]
+	    (equal? : (forall (a : A) (b : A) Bool)))]
 }
 
 @defform[(impl (class param) defs ...)]{

cur-doc/info.rkt

@@ -1,6 +1,6 @@
 #lang info
 (define collection 'multi)
 (define deps '("base" "racket-doc"))
-(define build-deps '("scribble-lib" ("cur-lib" #:version "0.2") "sandbox-lib"))
+(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

@@ -2,6 +2,7 @@
 
 (require
   racket/function
+  racket/list
   redex/reduction-semantics)
 
 (provide
@@ -25,11 +26,11 @@
 (define-language ttL
   (i j k  ::= natural)
   (U ::= (Unv i))
-  (t e ::= U (λ (x : t) e) x (Π (x : t) t) (e e) (elim D U))
-  ;; Δ (signature). (inductive-name : type ((constructor : type) ...))
-  ;; NB: Δ is a map from a name x to a pair of it's type and a map of constructor names to their types
-  (Δ   ::= ∅ (Δ (D : t ((c : t) ...))))
   (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))
@@ -43,6 +44,8 @@
 ;;; ------------------------------------------------------------------------
 ;;; Universe typing
 
+;; Universe types
+;; aka Axioms A of a PTS
 (define-judgment-form ttL
   #:mode (unv-type I O)
   #:contract (unv-type U U)
@@ -52,6 +55,7 @@
    (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)
@@ -104,25 +108,6 @@
   [(Δ-union Δ_2 (Δ_1 (x : t any)))
    ((Δ-union Δ_2 Δ_1) (x : t any))])
 
-;; Returns the inductively defined type that x constructs
-;; NB: Depends on clause order
-(define-metafunction ttL
-  Δ-key-by-constructor : Δ x -> x
-  [(Δ-key-by-constructor (Δ (x : t ((x_0 : t_0) ... (x_c : t_c) (x_1 : t_1) ...))) x_c)
-   x]
-  [(Δ-key-by-constructor (Δ (x_1 : t_1 any)) x)
-   (Δ-key-by-constructor Δ x)])
-
-;; Returns the constructor map for the inductively defined type x_D in the signature Δ
-(define-metafunction ttL
-  Δ-ref-constructor-map : Δ x -> ((x : t) ...) or #f
-  ;; NB: Depends on clause order
-  [(Δ-ref-constructor-map ∅ x_D) #f]
-  [(Δ-ref-constructor-map (Δ (x_D : t_D any)) x_D)
-   any]
-  [(Δ-ref-constructor-map (Δ (x_1 : t_1 any)) x_D)
-   (Δ-ref-constructor-map Δ x_D)])
-
 ;; TODO: Should not use Δ-ref-type
 (define-metafunction ttL
   Δ-ref-constructor-type : Δ x x -> t
@@ -139,6 +124,9 @@
   [(Δ-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
@@ -170,45 +158,35 @@
 
 ;; TODO: Might be worth it to actually maintain the above bijections, for performance reasons.
 
-;; Return the parameters of x_D as a telescope Ξ
-;; TODO: Define generic traversals of Δ and Γ ?
-(define-metafunction tt-ctxtL
-  Δ-ref-parameter-Ξ : Δ x -> Ξ
-  [(Δ-ref-parameter-Ξ (Δ (x_D : (in-hole Ξ U) any)) x_D)
-   Ξ]
-  [(Δ-ref-parameter-Ξ (Δ (x_1 : t_1 any)) x_D)
-   (Δ-ref-parameter-Ξ Δ x_D)])
 
 ;; 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 (equivalent t (Ξ-apply Ξ t))?
+ | that (convert t (Ξ-apply Ξ t))?
- | Maybe not. t is a lambda whose type is equivalent to (Ξ-apply Ξ t)? Yes.
+ | 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))])
 
-;; Compose multiple telescopes into a single telescope:
-(define-metafunction tt-ctxtL
-  Ξ-compose : Ξ Ξ ... -> Ξ
-  [(Ξ-compose Ξ) Ξ]
-  [(Ξ-compose Ξ_0 Ξ_1 Ξ_rest ...)
-   (Ξ-compose (in-hole Ξ_0 Ξ_1) Ξ_rest ...)])
-
 ;; Compute the number of arguments in a Ξ
 (define-metafunction tt-ctxtL
   Ξ-length : Ξ -> natural
   [(Ξ-length hole) 0]
   [(Ξ-length (Π (x : t) Ξ)) ,(add1 (term (Ξ-length Ξ)))])
 
-;; Compute the number of applications in a Θ
 (define-metafunction tt-ctxtL
-  Θ-length : Θ -> natural
+  list->Θ : (e ...) -> Θ
-  [(Θ-length hole) 0]
+  [(list->Θ ()) hole]
-  [(Θ-length (Θ e)) ,(add1 (term (Θ-length Θ)))])
+  [(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
@@ -220,6 +198,17 @@
 ;;; ------------------------------------------------------------------------
 ;;; 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 -> Ξ
@@ -237,21 +226,6 @@
    (where (in-hole Ξ (in-hole Θ x_D))
      (Δ-ref-constructor-type Δ x_D x_ci))])
 
-;; Inner loop for Δ-constructor-noninductive-telescope
-(define-metafunction tt-ctxtL
-  noninductive-loop : x Φ -> Φ
-  [(noninductive-loop x_D hole) hole]
-  [(noninductive-loop x_D (Π (x : (in-hole Φ (in-hole Θ x_D))) Φ_1))
-   (noninductive-loop x_D Φ_1)]
-  [(noninductive-loop x_D (Π (x : t) Φ_1))
-   (Π (x : t) (noninductive-loop x_D Φ_1))])
-
-;; Returns the noninductive arguments to the constructor x_ci of the inductively defined type x_D
-(define-metafunction tt-ctxtL
-  Δ-constructor-noninductive-telescope : Δ x x -> Ξ
-  [(Δ-constructor-noninductive-telescope Δ x_D x_ci)
-   (noninductive-loop x_D (Δ-constructor-telescope Δ x_D x_ci))])
-
 ;; Inner loop for Δ-constructor-inductive-telescope
 ;; NB: Depends on clause order
 (define-metafunction tt-ctxtL
@@ -280,36 +254,6 @@
       (hypotheses-loop x_D t_P Φ_1))
    (where x_h ,(variable-not-in (term (x_D t_P any_0)) 'x-ih))])
 
-;; Returns the inductive hypotheses required for the elimination method of constructor x_ci for
-;; inductive type x_D, when eliminating with motive t_P.
-(define-metafunction tt-ctxtL
-  Δ-constructor-inductive-hypotheses : Δ x x t -> Ξ
-  [(Δ-constructor-inductive-hypotheses Δ x_D x_ci t_P)
-   (hypotheses-loop x_D t_P (Δ-constructor-inductive-telescope Δ x_D x_ci))])
-
-(define-metafunction tt-ctxtL
-  Δ-constructor-method-telescope : Δ x x t -> Ξ
-  [(Δ-constructor-method-telescope Δ x_D x_ci t_P)
-   (Π (x_mi : (in-hole Ξ_a (in-hole Ξ_h ((in-hole Θ_p t_P) (Ξ-apply Ξ_a x_ci)))))
-      hole)
-   (where Θ_p (Δ-constructor-parameters Δ x_D x_ci))
-   (where Ξ_a (Δ-constructor-telescope Δ x_D x_ci))
-   (where Ξ_h (Δ-constructor-inductive-hypotheses Δ x_D x_ci t_P))
-   (where x_mi ,(variable-not-in (term (t_P Δ)) 'x-mi))])
-
-;; fold Ξ-compose over map Δ-constructor-method-telescope over the list of constructors
-(define-metafunction tt-ctxtL
-  method-loop : Δ x t (x ...) -> Ξ
-  [(method-loop Δ x_D t_P ()) hole]
-  [(method-loop Δ x_D t_P (x_0 x_rest ...))
-   (Ξ-compose (Δ-constructor-method-telescope Δ x_D x_0 t_P) (method-loop Δ x_D t_P (x_rest ...)))])
-
-;; Returns the telescope of all methods required to eliminate the type x_D with motive t_P
-(define-metafunction tt-ctxtL
-  Δ-methods-telescope : Δ x t -> Ξ
-  [(Δ-methods-telescope Δ x_D t_P)
-   (method-loop Δ x_D t_P (Δ-ref-constructors Δ x_D))])
-
 ;; Computes the type of the eliminator for the inductively defined type x_D with a motive whose result
 ;; is in universe U.
 ;;
@@ -325,42 +269,40 @@
 ;; Ξ_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
-(define-metafunction tt-ctxtL
-  Δ-elim-type : Δ x U -> t
-  [(Δ-elim-type Δ x_D U)
-   (Π (x_P : (in-hole Ξ_P*D U))
-      ;; The methods Ξ_m for each constructor of type x_D
-      (in-hole Ξ_m
-        ;; And finally, the parameters and discriminant
-        (in-hole Ξ_P*D
-          ;; The result is (P a ... (x_D a ...)), i.e., the motive
-          ;; applied to the paramters and discriminant
-          (Ξ-apply Ξ_P*D x_P))))
-   ;; Get the parameters of x_D
-   (where Ξ (Δ-ref-parameter-Ξ Δ x_D))
-   ;; A fresh name to bind the discriminant
-   (where x ,(variable-not-in (term (Δ Γ x_D Ξ)) 'x-D))
-   ;; The telescope (∀ a -> ... -> (D a ...) hole), i.e.,
-   ;; of the parameters and the inductive type applied to the
-   ;; parameters
-   (where Ξ_P*D (in-hole Ξ (Π (x : (Ξ-apply Ξ x_D)) hole)))
-   ;; A fresh name for the motive
-   (where x_P ,(variable-not-in (term (Δ Γ x_D Ξ Ξ_P*D x)) 'x-P))
-   ;; The types of the methods for this inductive.
-   (where Ξ_m (Δ-methods-telescope Δ x_D x_P))])
 
-;; TODO: This might belong in the next section, since it's related to evaluation
+;; Returns the inductive hypotheses required for the elimination method of constructor c_i for
-;; Generate recursive applications of the eliminator for each inductive argument of type x_D.
+;; inductive type D, when eliminating with motive t_P.
-;; In more detaill, 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)
 (define-metafunction tt-ctxtL
-  Δ-inductive-elim : Δ x U t Θ Θ Θ -> Θ
+  Δ-constructor-inductive-hypotheses : Δ D c t -> Ξ
-  [(Δ-inductive-elim Δ x_D U t_P Θ_p Θ_m (in-hole Θ_i (hole (name t_i (in-hole Θ_r x_ci)))))
+  [(Δ-constructor-inductive-hypotheses Δ D c_i t_P)
-   ((Δ-inductive-elim Δ x_D U t_P Θ_p Θ_m Θ_i)
+   (hypotheses-loop D t_P (Δ-constructor-inductive-telescope Δ D c_i))])
-    (in-hole ((in-hole Θ_p Θ_m) t_i) ((elim x_D U) t_P)))
+
-   (side-condition (memq (term x_ci) (term (Δ-ref-constructors Δ x_D))))]
+;; Returns the type of the method corresponding to c_i
-  [(Δ-inductive-elim Δ x_D U t_P Θ_p Θ_m Θ_nr) hole])
+(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
@@ -368,55 +310,77 @@
 ;;; inductively defined type x with a motive whose result is in universe U
 
 (define-extended-language tt-redL tt-ctxtL
-  ;; NB: (in-hole Θv (elim x U)) is only a value when it's a partially applied elim. However,
+  (v  ::= x U (Π (x : t) t) (λ (x : t) t) (in-hole Θv c))
-  ;; determining whether or not it is partially applied cannot be done with the grammar alone.
+  (Θv ::= hole (Θv v))
-  (v   ::= x U (Π (x : t) t) (λ (x : t) t) (elim x U) (in-hole Θv x) (in-hole Θv (elim x U)))
+  (C-elim  ::= (elim D t_P (e_i ...) (e_m ...) hole))
-  (Θv  ::= hole (Θv v))
+  ;; call-by-value
-  ;; call-by-value, plus reduce under Π (helps with typing checking)
+  (E  ::= hole (E e) (v E)
-  (E   ::= hole (E e) (v E) (Π (x : v) E) (Π (x : E) 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 (in-hole Θv ((elim x_D U) v_P))))
+    (--> (Δ (in-hole E (elim D e_motive (e_i ...) (v_m ...) (in-hole Θv_c c))))
-         (Δ (in-hole E (in-hole Θ_r (in-hole Θv_i v_mi))))
+         (Δ (in-hole E (in-hole Θ_mi v_mi)))
-         #|
+         ;; Find the method for constructor c_i, relying on the order of the arguments.
-          | The elim form must appear applied like so:
+         (where natural (Δ-constructor-index Δ D c))
-          | (elim x_D U v_P m_0 ... m_i m_j ... m_n p ... (c_i a ...))
+         (where v_mi ,(list-ref (term (v_m ...)) (term natural)))
-          |
-          | Where:
-          |   x_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
-          | Unfortunately, Θ contexts turn all this inside out:
-          | TODO: Write better abstractions for this notation
-          |#
-          ;; Split Θv into its components: the paramters Θv_P for x_D, the methods Θv_m for x_D, and
-          ;; the discriminant: the constructor x_ci applied to its argument Θv_i
-         (where (in-hole (Θv_p (in-hole Θv_i x_ci)) Θv_m) Θv)
-         ;; Check that Θ_p actually matches the parameters of x_D, to ensure it doesn't capture other
-         ;; arguments.
-         (side-condition (equal? (term (Θ-length Θv_p)) (term (Ξ-length (Δ-ref-parameter-Ξ Δ x_D)))))
-         ;; Ensure x_ci is actually a constructor for x_D
-         (where (x_c* ...) (Δ-ref-constructors Δ x_D))
-         (side-condition (memq (term x_ci) (term (x_c* ...))))
-         ;; There should be a number of methods equal to the number of constructors; to ensure E
-         ;; doesn't capture methods and Θv_m doesn't capture other arguments
-         (side-condition (equal? (length (term (x_c* ...)))  (term (Θ-length Θv_m))))
-         ;; Find the method for constructor x_ci, relying on the order of the arguments.
-         (where v_mi (Θ-ref Θv_m (Δ-constructor-index Δ x_D x_ci)))
          ;; Generate the inductive recursion
-         (where Θ_r (Δ-inductive-elim Δ x_D U v_P Θv_p Θv_m Θv_i))
+         (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
@@ -430,23 +394,7 @@
   [(reduce Δ e)
    e_r
    (where (_ e_r)
-     ,(let ([r (apply-reduction-relation* tt--> (term (Δ e)) #:cache-all? #t)])
+          ,(car (apply-reduction-relation* tt--> (term (Δ e)) #:cache-all? #t)))])
-        ;; Efficient check for (= (length r) 1)
-        ;; NB: Check is overly aggressive and produces wrong error,
-        ;; because not reducing under lambda.
-        #;(unless (null? (cdr r))
-          (error "Church-Rosser broken" r))
-        (car r)))])
-
-(define-judgment-form tt-redL
-  #:mode (equivalent I I I)
-  #:contract (equivalent Δ t t)
-
-  [(where t_2 (reduce Δ t_0))
-   (where t_3 (reduce Δ t_1))
-   (side-condition (α-equivalent? t_2 t_3))
-   ----------------- "≡-αβ"
-   (equivalent Δ t_0 t_1)])
 
 ;;; ------------------------------------------------------------------------
 ;;; Type checking and synthesis
@@ -457,6 +405,24 @@
   (Γ   ::= ∅ (Γ 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 Γ ∅) Γ]
@@ -575,16 +541,22 @@
    ----------------- "DTR-Application"
    (type-infer Δ Γ (e_0 e_1) t_3)]
 
-  [(where t (Δ-elim-type Δ D U))
+  [(type-check Δ Γ e_c (apply D e_i ...))
-   (type-infer Δ Γ t U_e)
+
+   (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 U) t)])
+   (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)
-   (equivalent Δ t t_0)
+   (convert Δ Γ t t_0)
    ----------------- "DTR-Check"
    (type-check Δ Γ e t)])

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

@@ -2,7 +2,7 @@
 ;; This module just provide module language sugar over the redex model.
 
 (require
-  "redex-core.rkt"
+  (except-in "redex-core.rkt" apply)
   redex/reduction-semantics
   racket/provide-syntax
   (for-syntax
@@ -11,7 +11,7 @@
     racket/syntax
     (except-in racket/provide-transform export)
     racket/require-transform
-    "redex-core.rkt"
+    (except-in "redex-core.rkt" apply)
     redex/reduction-semantics))
 (provide
   ;; Basic syntax
@@ -30,12 +30,10 @@
     [dep-provide provide]
     [dep-require require]
 
-    [dep-lambda lambda]
     [dep-lambda λ]
     [dep-app #%app]
 
-    [dep-forall forall]
+    [dep-forall Π]
-    [dep-forall ∀]
 
     [dep-inductive data]
 
@@ -62,10 +60,10 @@
    (all-from-out racket/syntax)
     cur->datum
     cur-expand
-    type-infer/syn
+    cur-type-infer
-    type-check/syn?
+    cur-type-check?
-    normalize/syn
+    cur-normalize
-    step/syn
+    cur-step
     cur-equal?))
 
 (begin-for-syntax
@@ -179,10 +177,11 @@
                     [e (parameterize ([gamma (extend-Γ/term gamma x t)])
                          (cur->datum #'e))])
                (term (,(syntax->datum #'b) (,x : ,t) ,e)))]
-            [(elim t1 t2)
+            [(elim D motive (i ...) (m ...) d)
-             (let* ([t1 (cur->datum #'t1)]
+             (term (elim ,(cur->datum #'D) ,(cur->datum #'motive)
-                    [t2 (cur->datum #'t2)])
+                         ,(map cur->datum (syntax->list #'(i ...)))
-               (term (elim ,t1 ,t2)))]
+                         ,(map cur->datum (syntax->list #'(m ...)))
+                         ,(cur->datum #'d)))]
             [(#%app e1 e2)
              (term (,(cur->datum #'e1) ,(cur->datum #'e2)))]))))
     (unless (or (inner-expand?) (type-infer/term reified-term))
@@ -191,35 +190,29 @@
     reified-term)
 
   (define (datum->cur syn t)
-    (match t
+    (let datum->cur ([t t])
-      [(list (quote term) e)
+      (match t
-       (quasisyntax/loc
+        [(list (quote term) e)
-         syn
+         (quasisyntax/loc syn
-         (datum->cur syn e))]
+           (datum->cur e))]
-      [(list (quote Unv) i)
+        [(list (quote Unv) i)
-       (quasisyntax/loc
+         (quasisyntax/loc syn
-         syn
+           (Type #,i))]
-         (Type #,i))]
+        [(list (quote Π) (list x (quote :) t) body)
-      [(list (quote Π) (list x (quote :) t) body)
+         (quasisyntax/loc syn
-       (quasisyntax/loc
+           (dep-forall (#,(datum->syntax syn x) : #,(datum->cur t)) #,(datum->cur body)))]
-         syn
+        [(list (quote λ) (list x (quote :) t) body)
-         (dep-forall (#,(datum->syntax syn x) : #,(datum->cur syn t)) #,(datum->cur syn body)))]
+         (quasisyntax/loc syn
-      [(list (quote λ) (list x (quote :) t) body)
+           (dep-lambda (#,(datum->syntax syn x) : #,(datum->cur t)) #,(datum->cur body)))]
-       (quasisyntax/loc
+        [(list (list (quote elim) t1) t2)
-         syn
+         (quasisyntax/loc syn
-         (dep-lambda (#,(datum->syntax syn x) : #,(datum->cur syn t)) #,(datum->cur syn body)))]
+           (dep-elim #,(datum->cur t1) #,(datum->cur t2)))]
-      [(list (list (quote elim) t1) t2)
+        [(list e1 e2)
-       (quasisyntax/loc
+         (quasisyntax/loc syn
-         syn
+           (dep-app #,(datum->cur e1) #,(datum->cur e2)))]
-         (dep-elim #,(datum->cur syn t1) #,(datum->cur syn t2)))]
+        [_
-      [(list e1 e2)
+         (quasisyntax/loc syn
-       (quasisyntax/loc
+           #,(datum->syntax syn t))])))
-         syn
-         (dep-app #,(datum->cur syn e1) #,(datum->cur syn e2)))]
-      [_
-       (quasisyntax/loc
-         syn
-         #,(datum->syntax syn t))]))
 
   (define (eval-cur syn)
     (term (reduce ,(delta) ,(subst-bindings (cur->datum syn)))))
@@ -232,29 +225,29 @@
 
   ;; Reflection tools
 
-  (define (normalize/syn syn)
+  (define (cur-normalize syn)
     (datum->cur
       syn
       (eval-cur syn)))
 
-  (define (step/syn syn)
+  (define (cur-step syn)
     (datum->cur
       syn
       (term (step ,(delta) ,(subst-bindings (cur->datum syn))))))
 
   ;; Are these two terms equivalent in type-systems internal equational reasoning?
   (define (cur-equal? e1 e2)
-    (and (judgment-holds (equivalent ,(delta) ,(eval-cur e1) ,(eval-cur e2))) #t))
+    (and (judgment-holds (convert ,(delta) ,(gamma) ,(eval-cur e1) ,(eval-cur e2))) #t))
 
   ;; TODO: Document local-env
-  (define (type-infer/syn syn #:local-env [env '()])
+  (define (cur-type-infer syn #:local-env [env '()])
     (parameterize ([gamma (for/fold ([gamma (gamma)])
                                     ([(x t) (in-dict env)])
                             (extend-Γ/syn (thunk gamma) x t))])
       (let ([t (type-infer/term (eval-cur syn))])
         (and t (datum->cur syn t)))))
 
-  (define (type-check/syn? syn type)
+  (define (cur-type-check? syn type)
     (type-check/term? (eval-cur syn) (eval-cur type)))
 
   ;; Takes a Cur term syn and an arbitrary number of identifiers ls. The cur term is
@@ -418,42 +411,45 @@
 ;;
 ;; TODO: Can these be simplified further?
 (define-syntax (dep-lambda syn)
-  (syntax-case syn (:)
+  (syntax-parse syn
-    [(_ (x : t) e)
+    #:datum-literals (:)
+    [(_ (x:id : t) e)
      (syntax->curnel-syntax
        (quasisyntax/loc syn (λ (x : t) e)))]))
 
 (define-syntax (dep-app syn)
-  (syntax-case syn ()
+  (syntax-parse syn
-    [(_ e1 e2)
+    [(_ e1:expr e2:expr)
      (syntax->curnel-syntax
        (quasisyntax/loc syn (#%app e1 e2)))]))
 
 (define-syntax (dep-forall syn)
-  (syntax-case syn (:)
+  (syntax-parse syn
-    [(_ (x : t) e)
+    #:datum-literals (:)
+    [(_ (x:id : t) e)
      (syntax->curnel-syntax
        (quasisyntax/loc syn (Π (x : t) e)))]))
 
 (define-syntax (Type syn)
-  (syntax-case syn ()
+  (syntax-parse syn
-    [(_ i)
+    [(_ i:nat)
      (syntax->curnel-syntax
        (quasisyntax/loc syn (Unv i)))]
     [_ (quasisyntax/loc syn (Type 0))]))
 
 (define-syntax (dep-inductive syn)
-  (syntax-case syn (:)
+  (syntax-parse syn
-    [(_ i : ti (x1 : t1) ...)
+    #:datum-literals (:)
+    [(_ i:id : ti (x1:id : t1) ...)
      (begin
        (extend-Δ/syn! delta #'i #'ti #'((x1 : t1) ...))
        #'(void))]))
 
 (define-syntax (dep-elim syn)
-  (syntax-case syn ()
+  (syntax-parse syn
-    [(_ D T)
+    [(_ D:id motive (i ...) (m ...) e)
      (syntax->curnel-syntax
-       (quasisyntax/loc syn (elim D T)))]))
+       (quasisyntax/loc syn (elim D motive (i ...) (m ...) e)))]))
 
 (define-syntax-rule (dep-void) (void))
 

cur-lib/cur/lang/reader.rkt

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

cur-lib/cur/olly.rkt

@@ -1,314 +1,449 @@
-#lang s-exp "cur.rkt"
+#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"
-  (only-in "cur.rkt" [#%app real-app] [elim real-elim]))
+  ;; TODO: "real-"? More like "curnel-"
+  (only-in
+   "main.rkt"
+   [#%app real-app]
+   [elim real-elim]
+   [Π real-forall]
+   [λ real-lambda]))
 
 (provide
   define-relation
   define-language
-  Var
-  avar
-  var-equal?
   generate-coq
 
   ;; private; exported for testing only
   (for-syntax
-   coq-defns
+   typeset-relation
-   output-latex-bnf
+   typeset-bnf
-   output-coq
+   cur->coq))
-   new-name
-   fresh-name))
-
-(begin-for-syntax
-  (define-syntax-class dash
-    (pattern x:id
-             #:fail-unless (regexp-match #rx"-+" (symbol->string (syntax-e #'x)))
-             "Invalid dash"))
-
-  (define-syntax-class decl (pattern (x:id (~datum :) t:id)))
-
-  ;; TODO: Automatically infer decl ... by binding all free identifiers?
-  ;; TODO: Automatically infer decl ... for meta-variables that are the
-  ;; same as bnf grammar.
-  (define-syntax-class inferrence-rule
-    (pattern (d:decl ...
-              x*:expr ...
-              line:dash lab:id
-              (name:id y* ...))
-              #:with rule #'(lab : (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)))))
-
-;; TODO: Oh, this is a mess. Rewrite it.
-(begin-for-syntax
-  (define lang-name (make-parameter #'name))
-  (define nts (make-parameter (make-immutable-hash)))
-
-  (define-syntax-class nt
-    (pattern e:id #:fail-unless (hash-has-key? (nts) (syntax->datum #'e)) #f
-             #:attr name (hash-ref (nts) (syntax->datum #'e))
-             #:attr type (hash-ref (nts) (syntax->datum #'e))))
-
-  (define (flatten-args arg arg*)
-    (for/fold ([ls (syntax->list arg)])
-              ([e (syntax->list arg*)])
-      (append ls (syntax->list e))))
-
-  (define-syntax-class (right-clause type)
-    #;(pattern (~datum var)
-             #:attr clause-context #`(#,(new-name (lang-name) #'var) :
-                                      (-> #,(hash-ref (nts) 'var) #,(hash-ref (nts) type)))
-             #:attr name #'var
-             #:attr arg-context #'(var))
-    (pattern e:nt
-             #:attr clause-context #`(#,(new-name #'e.name #'->
-                                                  (hash-ref (nts) type)) :
-                                      (-> e.type #,(hash-ref (nts) type)))
-             #:attr name (fresh-name #'e.name)
-             #:attr arg-context #'(e.type))
-    (pattern x:id
-             #:attr clause-context #`(#,(new-name (lang-name) #'x) :
-                                      #,(hash-ref (nts) type))
-             #:attr name (new-name (lang-name) #'x)
-             #:attr arg-context #'())
-    (pattern ((~var e (right-clause type)) (~var e* (right-clause type)) ...)
-             #:attr name (fresh-name #'e.name)
-             #:attr clause-context #`(e.name : (->* #,@(flatten-args #'e.arg-context #'(e*.arg-context ...))
-                                                    #,(hash-ref (nts) type)))
-             #:attr arg-context #`(#,@(flatten-args #'e.arg-context #'(e*.arg-context ...)))))
-
-  (define-syntax-class (right type)
-    (pattern ((~var r (right-clause type)) ...)
-             #:attr clause #'(r.clause-context ...)))
-
-  #;(define-syntax-class left
-    (pattern (type:id (nt*:id ...+))
-             #:do ))
-
-  (define-syntax-class nt-clauses
-    (pattern ((type:id (nt*:id ...+)
-              (~do (nts (for/fold ([ht (nts)])
-                                  ([nt (syntax->datum #'(type nt* ...))])
-                          (hash-set ht nt (new-name (lang-name) #'type)))))
-              (~datum ::=)
-              . (~var rhs* (right (syntax->datum #'type)))) ...)
-             #:with defs (with-syntax ([(name* ...)
-                                        (map (λ (x) (hash-ref (nts) x))
-                                             (syntax->datum #'(type ...)))])
-                           #`((data name* : Type . rhs*.clause)
-                              ...)))))
-
-(begin-for-syntax
-  ;; TODO: More clever use of syntax-parse would enable something akin to what
-  ;; define-relation is doing---having attributes that contain the latex
-  ;; code for each clause.
-  ;; TODO: convert meta-vars such as e1 to e_1
-  (define (output-latex-bnf vars clauses)
-    (format "$$\\begin{array}{lrrl}~n~a~n\\end{array}$$"
-      (for/fold ([str ""])
-                ([clause (syntax->list clauses)])
-        (syntax-parse clause
-          #:datum-literals (::=)
-          [(type:id (nonterminal:id ...) ::= exprs ...)
-           (format "\\mbox{\\textit{~a}} & ~a & \\bnfdef & ~a\\\\~n"
-                   (symbol->string (syntax->datum #'type))
-                   (string-trim
-                     (for/fold ([str ""])
-                               ([nt (syntax->datum #'(nonterminal ...))])
-                       (format "~a~a," str nt))
-                     ","
-                     #:left? #f)
-                   (string-trim
-                     (for/fold ([str ""])
-                               ([expr (syntax->datum #'(exprs ...))])
-                       (format "~a~a \\bnfalt " str expr))
-                     " \\bnfalt "
-                     #:left? #f))]))))
-  (define (generate-latex-bnf file-name vars clauses)
-    (with-output-to-file file-name
-      (thunk (printf (output-latex-bnf vars clauses)))
-      #:exists 'append)))
-
-;; TODO: For better error messages, add context, rename some of these patterns. e.g.
-;;    (type (meta-vars) ::= ?? )
-;; TODO: Extend define-language with syntax such as ....
-;;   (term (e) ::= (e1 e2) ((lambda (x) e)
-;                           #:latex "(\\lambda ,x. ,e)"))
-(define-syntax (define-language syn)
-  (syntax-parse syn
-    [(_ name:id (~do (lang-name #'name))
-        (~do (nts (hash-set (make-immutable-hash) 'var #'Var)))
-        (~optional (~seq #:vars (x*:id ...)
-           (~do (nts (for/fold ([ht (nts)])
-                               ([v (syntax->datum #'(x* ...))])
-                       (hash-set ht v (hash-ref ht 'var)))))))
-        (~optional (~seq #:output-coq coq-file:str))
-        (~optional (~seq #:output-latex latex-file:str))
-        . clause*:nt-clauses)
-     (let ([output #`(begin . clause*.defs)])
-       (when (attribute latex-file)
-         (generate-latex-bnf (syntax->datum #'latex-file) #'vars #'clause*))
-       #`(begin
-           #,@(if (attribute coq-file)
-                 #`((generate-coq #:file coq-file #:exists 'append #,output))
-                 #'())
-           #,output))]))
-
-(data Var : Type (avar : (-> Nat Var)))
-
-(define (var-equal? (v1 : Var) (v2 : Var))
-  (match v1
-    [(avar (n1 : Nat))
-     (match v2
-       [(avar (n2 : Nat))
-        (nat-equal? n1 n2)])]))
-
-;; See stlc.rkt for examples
 
 ;; 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)
+    (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 (output-coq syn)
+
-    (syntax-parse (cur-expand syn #'define #'begin)
+  (define (cur->coq syn)
-       ;; TODO: Need to add these to a literal set and export it
+    (parameterize ([coq-defns ""])
-       ;; Or, maybe overwrite syntax-parse
+      (define output
-       #:literals (lambda forall data real-app real-elim define begin Type)
+        (let cur->coq ([syn syn])
-       [(begin e ...)
+          (syntax-parse (cur-expand syn #'define #'begin)
-        (for/fold ([str ""])
+            ;; TODO: Need to add these to a literal set and export it
-                  ([e (syntax->list #'(e ...))])
+            ;; Or, maybe overwrite syntax-parse
-          (format "~a~n" (output-coq e)))]
+            #:literals (real-lambda real-forall data real-app real-elim define begin Type)
-       [(define name:id body)
+            [(begin e ...)
-        (begin
+             (for/fold ([str ""])
-          (coq-lift-top-level
+                       ([e (syntax->list #'(e ...))])
-            (format "Definition ~a := ~a.~n"
+               (format "~a~n" (cur->coq e)))]
-                    (output-coq #'name)
+            [(define name:id body)
-                    (output-coq #'body)))
+             (begin
-          "")]
+               (coq-lift-top-level
-       [(define (name:id (x:id : t) ...) body)
+                (format "Definition ~a := ~a.~n"
-        (begin
+                        (cur->coq #'name)
-          (coq-lift-top-level
+                        (cur->coq #'body)))
-            (format "Function ~a ~a := ~a.~n"
+               "")]
-                    (output-coq #'name)
+            [(define (name:id (x:id : t) ...) body)
-                    (for/fold ([str ""])
+             (begin
-                              ([n (syntax->list #'(x ...))]
+               (coq-lift-top-level
-                               [t (syntax->list #'(t ...))])
+                (format "Function ~a ~a := ~a.~n"
-                      (format "~a(~a : ~a) " str (output-coq n) (output-coq t)))
+                        (cur->coq #'name)
-                    (output-coq #'body)))
+                        (for/fold ([str ""])
-          "")]
+                                  ([n (syntax->list #'(x ...))]
-       [(lambda ~! (x:id (~datum :) t) body:expr)
+                                   [t (syntax->list #'(t ...))])
-        (format "(fun ~a : ~a => ~a)" (output-coq #'x) (output-coq #'t)
+                          (format "~a(~a : ~a) " str (cur->coq n) (cur->coq t)))
-                (output-coq #'body))]
+                        (cur->coq #'body)))
-       [(forall ~! (x:id (~datum :) t) body:expr)
+               "")]
-        (format "(forall ~a : ~a, ~a)" (syntax-e #'x) (output-coq #'t)
+            [(real-lambda ~! (x:id (~datum :) t) body:expr)
-                (output-coq #'body))]
+             (format "(fun ~a : ~a => ~a)" (cur->coq #'x) (cur->coq #'t)
-       [(data ~! n:id (~datum :) t (x*:id (~datum :) t*) ...)
+                     (cur->coq #'body))]
-        (begin
+            [(real-forall ~! (x:id (~datum :) t) body:expr)
-          (coq-lift-top-level
+             (format "(forall ~a : ~a, ~a)" (syntax-e #'x) (cur->coq #'t)
-            (format "Inductive ~a : ~a :=~a."
+                     (cur->coq #'body))]
-                   (sanitize-id (format "~a" (syntax-e #'n)))
+            [(data ~! n:id (~datum :) t (x*:id (~datum :) t*) ...)
-                   (output-coq #'t)
+             (begin
-                   (for/fold ([strs ""])
+               (coq-lift-top-level
-                             ([clause (syntax->list #'((x* : t*) ...))])
+                (format "Inductive ~a : ~a :=~a."
-                     (syntax-parse clause
+                        (sanitize-id (format "~a" (syntax-e #'n)))
-                       [(x (~datum :) t)
+                        (cur->coq #'t)
-                        (format "~a~n| ~a : ~a" strs (syntax-e #'x)
+                        (for/fold ([strs ""])
-                          (output-coq #'t))]))))
+                                  ([clause (syntax->list #'((x* : t*) ...))])
-          "")]
+                          (syntax-parse clause
-       [(Type i) "Type"]
+                            [(x (~datum :) t)
-       [(real-elim var t)
+                             (format "~a~n| ~a : ~a" strs (syntax-e #'x)
-        (format "~a_rect" (output-coq #'var))]
+                                     (cur->coq #'t))]))))
-       [(real-app e1 e2)
+               "")]
-        (format "(~a ~a)" (output-coq #'e1) (output-coq #'e2))]
+            [(Type i) "Type"]
-       [e:id (sanitize-id (format "~a" (syntax->datum #'e)))])))
+            [(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)
+        (~optional (~seq #:exists flag))
-     (parameterize ([current-output-port (if (attribute file)
+        body:expr)
-                                             (open-output-file (syntax->datum #'file)
+     (parameterize ([current-output-port
-                                                               #:exists
+                     (if (attribute file)
-                                                               (if (attribute flag)
+                         (open-output-file
-                                                                   ;; TODO: AHH WHAT?
+                          (syntax->datum #'file)
-                                                                   (eval (syntax->datum #'flag))
+                          #:exists
-                                                                   'error))
+                          (if (attribute flag)
-                                             (current-output-port))]
+                              ;; TODO: AHH WHAT?
-                    [coq-defns ""])
+                              (eval (syntax->datum #'flag))
-       (define output
+                              'error))
-         (let ([body (output-coq #'body)])
+                         (current-output-port))])
-           (if (regexp-match "^\\s*$" body)
+       (displayln (cur->coq #'body))
-               ""
-               (format "Eval compute in ~a." body))))
-       (displayln (format "~a~a" (coq-defns) output))
        #'(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,4 +1,4 @@
-#lang s-exp "../cur.rkt"
+#lang s-exp "../main.rkt"
 (require "sugar.rkt")
 (provide Bool true false if not and or)
 

cur-lib/cur/stdlib/list.rkt

@@ -1,58 +1,33 @@
-#lang s-exp "../cur.rkt"
+#lang s-exp "../main.rkt"
 (require
- "bool.rkt"
  "nat.rkt"
  "maybe.rkt"
  "sugar.rkt")
 
-(data List : (forall (A : Type) Type)
+(provide
-  (nil : (forall (A : Type) (List A)))
+ List
-  (cons : (forall* (A : Type) (->* A (List A) (List A)))))
+ nil
+ cons
+ list-ref
+ length)
 
-(module+ test
+(data List : (-> (A : Type) Type)
-  (require rackunit)
+  (nil : (-> (A : Type) (List A)))
-  (check-equal?
+  (cons : (-> (A : Type) A (List A) (List A))))
-   nil
-   nil)
-  (:: (cons Bool true (nil Bool)) (List Bool))
-  (:: (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)))
-  (:: (lambda* (A : Type) (n : Nat) (none A)) (forall (A : Type) (-> Nat (Maybe A))))
-  (:: (elim List Type (lambda* (A : Type) (ls : (List A)) Nat)
-            (lambda (A : Type) z)
-            (lambda* (A : Type) (a : A) (ls : (List A)) (ih : Nat)
-                     z)
-            Bool
-            (nil Bool))
-      Nat)
-  )
 
 (define (list-ref (A : Type) (ls : (List A)))
-  ;; TODO: case* would not type-check when used. Investigate/provide better errors for case*
+  (match ls
-  (elim
+    [(nil (A : Type)) (lambda (n : Nat) (none A))]
-   List
+    [(cons (A : Type) (a : A) (rest : (List A)))
-   Type
+     (lambda (n : Nat)
-   (lambda* (A : Type) (ls : (List A))
+       (match n
-            (-> Nat (Maybe A)))
+         [z (some A a)]
-   (lambda* (A : Type) (n : Nat) (none A))
+         [(s (n-1 : Nat))
-   (lambda* (A : Type) (a : A) (ls : (List A)) (ih : (-> Nat (Maybe A)))
+          ((recur rest) n-1)]))]))
-            (lambda (n : Nat)
-              (match n
-                [z (some A a)]
-                [(s (n-1 : Nat))
-                 (ih n-1)])))
-   A
-   ls))
 
-(module+ test
+(define (length (A : Type) (ls : (List A)))
-  (check-equal?
+  (match ls
-   ((list-ref Bool (cons Bool true (nil Bool))) z)
+    [(nil (A : Type))
-   (some Bool true)))
+     z]
+    [(cons (A : Type) (a : A) (rest : (List A)))
+     (s (recur rest))]))

cur-lib/cur/stdlib/maybe.rkt

@@ -1,13 +1,13 @@
-#lang s-exp "../cur.rkt"
+#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))))
+  (some : (forall (A : Type) (a : A) (Maybe A))))
 
 (define-syntax (some/i syn)
   (syntax-case syn ()
    [(_ a)
-    (let ([a-ty (type-infer/syn #'a)])
+    (let ([a-ty (cur-type-infer #'a)])
       #`(some #,a-ty a))]))

cur-lib/cur/stdlib/nat.rkt

@@ -1,4 +1,4 @@
-#lang s-exp "../cur.rkt"
+#lang s-exp "../main.rkt"
 (require "sugar.rkt" "bool.rkt")
 ;; TODO: override (all-defined-out) to enable exporting all these
 ;; properly.
@@ -35,17 +35,21 @@
 
 (define square (run (exp (s (s z)))))
 
-;; Credit to this function goes to Max
+(define (zero? (n : Nat))
-(define nat-equal?
+  (match n
-  (elim Nat Type (lambda (x : Nat) (-> Nat Bool))
+    [z true]
-    (elim Nat Type (lambda (x : Nat) Bool)
+    [(s (n : Nat))
-          true
+     false]))
-          (lambda* (x : Nat) (ih-n2 : Bool) false))
+
-    (lambda* (x : Nat) (ih : (-> Nat Bool))
+(define (nat-equal? (n : Nat))
-      (elim Nat Type (lambda (x : Nat) Bool)
+  (match n
-            false
+    [z zero?]
-            (lambda* (x : Nat) (ih-bla : Bool)
+    [(s (n-1 : Nat))
-                     (ih x))))))
+     (lambda (m : Nat)
+       (match m
+         [z false]
+         [(s (m-1 : Nat))
+          ((recur n-1) m-1)]))]))
 
 (define (even? (n : Nat))
   (match n

cur-lib/cur/stdlib/prop.rkt

@@ -1,4 +1,4 @@
-#lang s-exp "../cur.rkt"
+#lang s-exp "../main.rkt"
 (require "sugar.rkt")
 ;; TODO: Handle multiple provide forms properly
 ;; TODO: Handle (all-defined-out) properly
@@ -24,64 +24,62 @@
 
 (define-type (Not (A : Type)) (-> A False))
 
-(data And : (forall* (A : Type) (B : Type) Type)
+(data And : (forall (A : Type) (B : Type) Type)
-  (conj : (forall* (A : Type) (B : 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 (type-infer/syn #'a)]
+     (let ([a-type (cur-type-infer #'a)]
-           [b-type (type-infer/syn #'b)])
+           [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)))
+  (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))
+  (lambda (P : Type) (Q : Type) (ab : (And P Q))
-    (case* And Type ab (P Q)
+          (match ab
-      (lambda* (P : Type) (Q : Type) (ab : (And P Q))
+            [(conj (P : Type) (Q : Type) (x : P) (y : Q))
-         (And Q P))
+             (conj/i y x)])))
-      ((conj (P : Type) (Q : Type) (x : P) (y : Q)) IH: () (conj/i y x)))))
 
 (define thm:proj1
-  (forall* (A : Type) (B : Type) (c : (And A B)) A))
+  (forall (A : Type) (B : Type) (c : (And A B)) A))
 
 (define pf:proj1
-  (lambda* (A : Type) (B : Type) (c : (And A B))
+  (lambda (A : Type) (B : Type) (c : (And A B))
-    (case* And Type c (A B)
+          (match c
-      (lambda* (A : Type) (B : Type) (c : (And A B)) A)
+            [(conj (A : Type) (B : Type) (a : A) (b : B)) a])))
-      ((conj (A : Type) (B : Type) (a : A) (b : B)) IH: () a))))
 
 (define thm:proj2
-  (forall* (A : Type) (B : Type) (c : (And A B)) B))
+  (forall (A : Type) (B : Type) (c : (And A B)) B))
 
 (define pf:proj2
-  (lambda* (A : Type) (B : Type) (c : (And A B))
+  (lambda (A : Type) (B : Type) (c : (And A B))
-    (case* And Type c (A B)
+          (match c
-      (lambda* (A : Type) (B : Type) (c : (And A B)) B)
+            [(conj (A : Type) (B : Type) (a : A) (b : B)) b])))
-      ((conj (A : Type) (B : Type) (a : A) (b : B)) IH: () b))))
 
 #| TODO: Disabled until #22 fixed
-(data Or : (forall* (A : Type) (B : Type) Type)
+(data Or : (forall (A : Type) (B : Type) Type)
-  (left : (forall* (A : Type) (B : Type) (a : A) (Or A B)))
+  (left : (forall (A : Type) (B : Type) (a : A) (Or A B)))
-  (right : (forall* (A : Type) (B : Type) (b : B) (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))
+  (forall (A : Type) (o : (Or A A)) A))
 
 (define proof:A-or-A
-  (lambda* (A : Type) (c : (Or A 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)
+    (elim Or (lambda (A : Type) (B : Type) (c : (Or A B)) A)
-      (lambda* (A : Type) (B : Type) (a : A) a)
+          (A A)
-      ;; TODO: How do we know B is A?
+          ((lambda (A : Type) (B : Type) (a : A) a)
-      (lambda* (A : Type) (B : Type) (b : B) b)
+           ;; TODO: How do we know B is A?
-      A A c)))
+           (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))
+(data == : (forall (A : Type) (x : A) (-> A Type))
-  (refl : (forall* (A : Type) (x : A) (== A x x))))
+  (refl : (forall (A : Type) (x : A) (== A x x))))

cur-lib/cur/stdlib/sugar.rkt

@@ -1,20 +1,18 @@
-#lang s-exp "../cur.rkt"
+#lang s-exp "../main.rkt"
 (provide
   ->
-  ->*
+  lambda
-  forall*
-  lambda*
   (rename-out
     [-> →]
-    [->* →*]
+    [-> forall]
-    [lambda* λ*]
+    [-> ∀]
-    [forall* ∀*])
+    [-> Π]
+    [-> Pi]
+    [lambda λ])
   #%app
   define
-  elim
+  :
   define-type
-  case
-  case*
   match
   recur
   let
@@ -29,130 +27,353 @@
   query-type)
 
 (require
-  (only-in "../cur.rkt"
+  (only-in "../main.rkt"
-    [elim real-elim]
     [#%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-case syn ()
+  (syntax-parse syn
-    [(_ t1 t2) #`(forall (#,(gensym) : t1) t2)]))
+    [(_ 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))]))
 
-(define-syntax ->*
+;; TODO: Add forall macro that allows specifying *names*, with types
-  (syntax-rules ()
+;; inferred. unlike -> which require types but not names
-    [(->* a) a]
+;; E.g.
-    [(->* a a* ...)
+;; (forall x (y : Nat) (== Nat x y))
-     (-> a (->* a* ...))]))
 
-(define-syntax forall*
+;; TODO: Allows argument-declarations to have types inferred, similar
-  (syntax-rules (:)
+;; to above TODO forall
-    [(_ (a : t) (ar : tr) ... b)
+(begin-for-syntax
-     (forall (a : t)
+  ;; eta-expand syntax-class for error messages
-        (forall* (ar : tr) ... b))]
+  (define-syntax-class argument-declaration
-    [(_ b) b]))
+    (pattern
-
+     e:parameter-declaration
-(define-syntax lambda*
+     #:attr name #'e.name
-  (syntax-rules (:)
+     #:attr type #'e.type)))
-    [(_ (a : t) (ar : tr) ... b)
+(define-syntax (lambda syn)
-     (lambda (a : t)
+  (syntax-parse syn
-       (lambda* (ar : tr) ... b))]
+    [(_ d:argument-declaration ...+ body:expr)
-    [(_ b) b]))
+     (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) #'e]
+    [(_ e)
+     (quasisyntax/loc syn e)]
     [(_ e1 e2)
-     #'(real-app e1 e2)]
+     (quasisyntax/loc syn
+       (real-app e1 e2))]
     [(_ e1 e2 e3 ...)
-     #'(#%app (#%app e1 e2) e3 ...)]))
+     (quasisyntax/loc syn
+       (#%app (#%app e1 e2) e3 ...))]))
 
 (define-syntax define-type
   (syntax-rules ()
     [(_ (name (a : t) ...) body)
-     (define name (forall* (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-case 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)
-     #'(real-define name (lambda* (x : t) ... body))]
+     (quasisyntax/loc syn
+       (real-define name (lambda (x : t) ... body)))]
     [(define id body)
-     #'(real-define id body)]))
+     (quasisyntax/loc syn
-
+       (real-define id body))]))
-(define-syntax-rule (elim t1 t2 e ...)
-  ((real-elim t1 t2) e ...))
 
+#|
 (begin-for-syntax
-  (define (rewrite-clause clause)
+  (define (type->telescope syn)
-    (syntax-case clause (: IH:)
+    (syntax-parse (cur-expand syn)
-      [((con (a : A) ...) IH: ((x : t) ...) body)
+      #:literals (real-Π)
-       #'(lambda* (a : A) ... (x : t) ... body)]
+      #:datum-literals (:)
-      [(e body) #'body])))
+      [(real-Π (x:id : t) body)
+       (cons #'(x : t) (type->telescope #'body))]
+      [_ '()]))
 
-;; TODO: Expects clauses in same order as constructors as specified when
+  (define (type->body syn)
-;; TODO: inductive D is defined.
+    (syntax-parse syn
-;; TODO: Assumes D has no parameters
+      #:literals (real-Π)
-(define-syntax (case syn)
+      #:datum-literals (:)
-  ;; duplicated code
+      [(real-Π (x:id : t) body)
-  (define (clause-body syn)
+       (type->body #'body)]
-    (syntax-case (car (syntax->list syn)) (: IH:)
+      [e #'e]))
-      [((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)
+  (define (constructor-indices D syn)
-  (syntax-case syn ()
+    (let loop ([syn syn]
-    [(_ D U e (p ...) P clause* ...)
+               [args '()])
-     #`(elim D U P #,@(map rewrite-clause (syntax->list #'(clause* ...))) p ... e)]))
+      (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-struct clause (args types decl body))
   (define ih-dict (make-hash))
-  (define (clause-parse syn)
-    (syntax-case syn (:)
-      [((con (a : A) ...) body)
-       (make-clause (syntax->list #'(a ...)) (syntax->list #'(A ...)) #'((a : A) ...) #'body)]
-      [(e body)
-       (make-clause '() '() #'() #'body)]))
 
-  (define (infer-result clauses)
+  (define-syntax-class curried-application
-    (or
+    (pattern
-     (for/or ([clause clauses])
+     ((~literal real-app) name:id e:expr)
-       (type-infer/syn
+     #:attr args
-        (clause-body clause)
+     (list #'e))
-        #:local-env (for/fold ([d '()])
-                              ([arg (clause-args clause)]
-                               [type (clause-types clause)])
-                          (dict-set d arg type))))
-     (raise-syntax-error
-      'match
-      "Could not infer type of result."
-      (clause-body (car clauses)))))
 
-  (define (infer-ihs D motive args types)
+    (pattern
-    (for/fold ([ih-dict (make-immutable-hash)])
+     ((~literal real-app) a:curried-application e:expr)
-              ([type-syn types]
+     #:attr name #'a.name
-               [arg-syn args]
+     #:attr args
-               ;; NB: Non-hygenic
+     ;; TODO BUG: repeated appends are not performant; cons then reverse in inductive-type-declaration
-               #:when (cur-equal? type-syn D))
+     (append
-      (dict-set ih-dict (syntax->datum arg-syn) `(,(format-id arg-syn "ih-~a" arg-syn) . ,#`(#,motive #,arg-syn)))))
+      (attribute a.args)
+      (list #'e))))
 
-  (define (clause->method D motive clause)
+  (define-syntax-class inductive-type-declaration
-    (dict-clear! ih-dict)
+    (pattern
-    (let* ([ihs (infer-ihs D motive (clause-args clause) (clause-types clause))]
+     x:id
-           [ih-args (dict-map
+     #:attr inductive-name
-                     ihs
+     #'x
-                     (lambda (k v)
+     #:attr indices
-                       (dict-set! ih-dict k (car v))
+     '()
-                       #`(#,(car v) : #,(cdr v))))])
+     #:attr decls
-      #`(lambda* #,@(clause-decl clause) #,@ih-args #,(clause-body clause)))))
+     (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 ()
@@ -163,23 +384,49 @@
       (lambda ()
         (raise-syntax-error
          'match
-         (format "Cannot recur on ~a" (syntax->datum #'id))
+         ;; 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)))]))
 
-;; TODO: Test
 (define-syntax (match syn)
-  (syntax-case syn ()
+  (syntax-parse syn
-    [(_ e clause* ...)
+    [(_ d
-     (let* ([clauses (map clause-parse (syntax->list #'(clause* ...)))]
+        ~!
-            [R (infer-result clauses)]
+        (~optional
-            [D (or (type-infer/syn #'e)
+         (~seq #:in ~! t)
-                   (raise-syntax-error 'match "Could not infer discrimnant's type." syn))]
+         #:defaults
-	    [motive #`(lambda (x : #,D) #,R)]
+         ([t (or (cur-type-infer #'d)
-            [U (type-infer/syn R)])
+                 (raise-syntax-error
-       #`((elim #,D #,U)
+                  'match
-            #,motive
+                  "Could not infer discrimnant's type. Try using #:in to declare it."
-	    #,@(map (curry clause->method D motive) clauses)
+                  syn))]))
-	    e))]))
+        (~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
@@ -190,14 +437,14 @@
       #:attr type (cond
                     [(attribute t)
                      ;; TODO: Code duplication in ::
-                     (unless (type-check/syn? #'e #'t)
+                     (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 (type-infer/syn #'e)))
+                                 (cur->datum #'e) (cur->datum #'t) (cur->datum (cur-type-infer #'e)))
                          #'e (quasisyntax/loc #'x (x e))))
                      #'t]
-                    [(type-infer/syn #'e)]
+                    [(cur-type-infer #'e)]
                     [else
                       (raise-syntax-error
                         'let
@@ -206,31 +453,31 @@
 (define-syntax (let syn)
   (syntax-parse syn
     [(let (c:let-clause ...) body)
-     #'((lambda* (c.id : c.type) ... body) c.e ...)]))
+     #'((lambda (c.id : c.type) ... body) c.e ...)]))
 
-;; Normally type checking will only happen if a term is actually used. This forces a term to be
+;; Normally type checking will only happen if a term is actually used/appears at top-level.
-;; checked against a particular type.
+;; 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 (type-check/syn? #'pf #'t)
+       (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 (type-infer/syn #'pf)))
+                   (cur->datum #'pf) (cur->datum #'t) (cur->datum (cur-type-infer #'pf)))
            syn))
        #'(void))]))
 
 (define-syntax (run syn)
   (syntax-case syn ()
-    [(_ expr) (normalize/syn #'expr)]))
+    [(_ expr) (cur-normalize #'expr)]))
 
 (define-syntax (step syn)
   (syntax-case syn ()
     [(_ expr)
-     (let ([t (step/syn #'expr)])
+     (let ([t (cur-step #'expr)])
        (displayln (cur->datum t))
        t)]))
 
@@ -246,6 +493,6 @@
   (syntax-case syn ()
     [(_ term)
      (begin
-       (printf "\"~a\" has type \"~a\"~n" (syntax->datum #'term) (syntax->datum (type-infer/syn #'term)))
+       (printf "\"~a\" has type \"~a\"~n" (syntax->datum #'term) (syntax->datum (cur-type-infer #'term)))
        ;; Void is undocumented and a hack, but sort of works
        #'(void))]))

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

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

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

@@ -1,4 +1,4 @@
-#lang s-exp "../../cur.rkt"
+#lang s-exp "../../main.rkt"
 (require
   "base.rkt"
   (prefix-in basic: "standard.rkt")

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

@@ -1,4 +1,4 @@
-#lang s-exp "../../cur.rkt"
+#lang s-exp "../../main.rkt"
 (require
   "base.rkt"
   (for-syntax racket/syntax))
@@ -22,7 +22,7 @@
     [(forall (x:id : P:expr) body:expr)
      (let* ([ps (proof-state-extend-env ps name #'P)]
             [ps (proof-state-current-goal-set ps #'body)]
-            [ps (proof-state-fill-proof-hole ps (lambda (x) #`(lambda (#,name : P) #,x)))])
+            [ps (proof-state-fill-proof-hole ps (lambda (x) #`(λ (#,name : P) #,x)))])
        ps)]
     [_ (error 'intro "Can only intro when current goal is of the form (∀ (x : P) body)")]))
 

cur-lib/cur/stdlib/typeclass.rkt

@@ -1,4 +1,4 @@
-#lang s-exp "../cur.rkt"
+#lang s-exp "../main.rkt"
 (require
   "nat.rkt"
   "bool.rkt"
@@ -38,7 +38,7 @@
               #`(define-syntax (#,name syn)
                   (syntax-case syn ()
                     [(_ arg args (... ...))
-                     #`(#,(format-id syn "~a-~a" '#,name (type-infer/syn #'arg))
+                     #`(#,(format-id syn "~a-~a" '#,name (cur-type-infer #'arg))
                         arg
                         args (... ...))]))))]))
 
@@ -49,7 +49,7 @@
   (define (process-def def)
     (syntax-case def (define)
       [(define (name (a : t) ...) body ...)
-       (values (syntax->datum #'name) #'(lambda* (a : t) ... body ...))]
+       (values (syntax->datum #'name) #'(lambda (a : t) ... body ...))]
       [(define name body)
        (values (syntax->datum #'name) #'body)]))
   (syntax-case syn ()
@@ -57,7 +57,7 @@
      #`(begin
          #,@(for/list ([def (syntax->list #'(defs ...))])
               (let-values ([(name body) (process-def def)])
-                (unless (type-check/syn?
+                (unless (cur-type-check?
                           body
                           #`(#,(dict-ref
                                  (dict-ref typeclasses (syntax->datum #'class))

cur-lib/info.rkt

@@ -3,5 +3,5 @@
 (define deps '("base" ("redex-lib" #:version "1.11")))
 (define build-deps '())
 (define pkg-desc "implementation (no documentation, tests) part of \"cur\".")
-(define version "0.2")
+(define version "0.4")
 (define pkg-authors '(wilbowma))

cur-test/cur/tests/olly.rkt

@@ -9,77 +9,50 @@
  cur/olly)
 
 (begin-for-syntax
-  (require rackunit)
+  (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))))
 
-(begin-for-syntax
+;; Can't test this way anymore.
+#;(begin-for-syntax
   (check-equal?
    (format "$$\\begin{array}{lrrl}~n~a~n\\end{array}$$"
            (format "\\mbox{\\textit{term}} & e & \\bnfdef & (e1 e2) \\bnfalt (lambda (x) e)\\\\~n"))
-   (output-latex-bnf #'(x)
+   (typeset-bnf #'((term (e) ::= (e1 e2) (lambda (x) e)))))
-                     #'((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)
+   (typeset-bnf #'((type (A B C) ::= unit (* A B) (+ A C))))))
-                     #'((type (A B C) ::= unit (* A B) (+ A C))))))
-
-(check-equal?
- (var-equal? (avar z) (avar z))
- true)
-(check-equal?
- (var-equal? (avar z) (avar (s z)))
- false)
 
 (begin-for-syntax
   (check-equal?
-   (parameterize ([coq-defns ""]) (output-coq #'(data nat : Type (z : nat))) (coq-defns))
+   (format "Inductive nat : Type :=~n| z : nat.~n")
-   (format "Inductive nat : Type :=~n| z : nat.~n"))
+   (cur->coq #'(data nat : Type (z : nat))))
   (check-regexp-match
    "(forall .+ : Type, Type)"
-   (output-coq #'(-> Type Type)))
+   (cur->coq #'(-> Type Type)))
-  (let ([t (parameterize ([coq-defns ""])
+  (let ([t (cur->coq
-             (output-coq #'(define-relation (meow gamma term type)
+            #'(define-relation (meow gamma term type)
-                             [(g : gamma) (e : term) (t : type)
+                [(g : gamma) (e : term) (t : type)
-                              --------------- T-Bla
+                 --------------- T-Bla
-                              (meow g e t)]))
+                 (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
+  (let ([t (cur->coq
-                               (lambda* (x : nat) (ih-x : nat) ih-x)
+            #'(elim nat (lambda (x : nat) nat)
-                               e))])
+                    ()
+                    (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\\)"
+     "\\(nat_rect \\(fun x : nat => nat\\) z \\(fun x : nat => \\(fun ih_x : nat => ih_x\\)\\) e\\)"
      t))
   (check-regexp-match
    "Definition thm_plus_commutes := \\(forall n : nat, \\(forall m : nat, \\(\\(\\(== nat\\) \\(\\(plus n\\) m\\)\\) \\(\\(plus m\\) n\\)\\)\\)\\).\n"
-   (parameterize ([coq-defns ""])
+   (cur->coq
-     (output-coq #'(define thm:plus-commutes (forall* (n : nat) (m : nat)
+    #'(define thm:plus-commutes (forall (n : nat) (m : nat)
-                                                      (== nat (plus n m) (plus m n)))))
+                                        (== nat (plus n m) (plus m n))))))
-     (coq-defns)))
   (check-regexp-match
    "Function add1 \\(n : nat\\)  := \\(s n\\).\n"
-   (parameterize ([coq-defns ""])
+   (cur->coq #'(define (add1 (n : nat)) (s n)))))
-     (output-coq #'(define (add1 (n : nat)) (s n)))
-     (coq-defns))))

cur-test/cur/tests/plus.rkt

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

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

@@ -81,23 +81,6 @@
    (Π (a : S) (Π (b : B) ((and S) B)))
    (subst (Π (a : A) (Π (b : B) ((and A) B))) A S))))
 
-;; Various accessor tests
-;; ------------------------------------------------------------------------
-
-(check-equal?
- (term (Δ-key-by-constructor ,Δ zero))
- (term nat))
-(check-equal?
- (term (Δ-key-by-constructor ,Δ s))
- (term nat))
-
-(check-equal?
- (term (Δ-ref-constructor-map ,Δ nat))
- (term ((zero : nat) (s : (Π (x : nat) nat)))))
-(check-equal?
- (term (Δ-ref-constructor-map ,sigma false))
- (term ()))
-
 ;; Telescope tests
 ;; ------------------------------------------------------------------------
 ;; Are these telescopes the same when filled with alpha-equivalent, and equivalently renamed, termed
@@ -115,41 +98,10 @@
  (term (Δ-ref-parameter-Ξ ,Δ4 and))
  (term (Π (A : Type) (Π (B : Type) hole))))
 
-(check-telescope-equiv?
- (term (Ξ-compose
-        (Π (x : t_0) (Π (y : t_1) hole))
-        (Π (z : t_2) (Π (a : t_3) hole))))
- (term (Π (x : t_0) (Π (y : t_1) (Π (z : t_2) (Π (a : t_3) hole))))))
-
-(check-telescope-equiv?
- (term (Δ-methods-telescope ,Δ nat (λ (x : nat) nat)))
- (term (Π (m-zero : ((λ (x : nat) nat) zero))
-          (Π (m-s : (Π (x : nat) (Π (x-ih : ((λ (x : nat) nat) x)) ((λ (x : nat) nat) (s x))))) hole))))
-(check-telescope-equiv?
- (term (Δ-methods-telescope ,Δ nat P))
- (term (Π (m-zero : (P zero))
-          (Π (m-s : (Π (x : nat) (Π (ih-x : (P x)) (P (s x)))))
-             hole))))
-(check-telescope-equiv?
- (term (Δ-methods-telescope ,Δ  nat (λ (x : nat) nat)))
- (term (Π (m-zero :  ((λ (x : nat) nat) zero))
-          (Π (m-s : (Π (x : nat) (Π (ih-x : ((λ (x : nat) nat) x)) ((λ (x : nat) nat) (s x)))))
-             hole))))
-(check-telescope-equiv?
- (term (Δ-methods-telescope ,Δ4 and (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B)) true)))))
- (term (Π (m-conj : (Π (A : Type) (Π (B : Type) (Π (a : A) (Π (b : B)
-                                                              ((((λ (A : Type) (λ (B : Type) (λ (x : ((and A) B)) true)))
-                                                                 A)
-                                                                B)
-                                                               ((((conj A) B) a) b)))))))
-          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 ())))
-(check-telescope-equiv?
- (term (Δ-methods-telescope ,sigma false (λ (y : false) (Π (x : Type) x))))
- (term hole))
 
 ;; Tests for inductive elimination
 ;; ------------------------------------------------------------------------
@@ -157,21 +109,32 @@
 (check-true
  (redex-match? tt-ctxtL (in-hole Θ_i (hole (in-hole Θ_r zero))) (term (hole zero))))
 (check-telescope-equiv?
- (term (Δ-inductive-elim ,Δ nat Type (λ (x : nat) nat) hole
+ (term (Δ-inductive-elim ,Δ nat
-                         ((hole (s zero)) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+                         (elim nat (λ (x : nat) nat) ()
+                               ((s zero) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+                               hole)
                          (hole zero)))
- (term (hole (((((elim nat Type) (λ (x : nat) nat))
+ (term (hole (elim nat (λ (x : nat) nat)
-                (s zero))
+                   ()
-               (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+                   ((s zero)
-              zero))))
+                    (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+                   zero))))
 (check-telescope-equiv?
- (term (Δ-inductive-elim ,Δ nat Type (λ (x : nat) nat) hole
+ (term (Δ-inductive-elim ,Δ nat
-                         ((hole (s zero)) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+                         (elim nat (λ (x : nat) nat) ()
+                               ((s zero) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+                               hole)
                          (hole (s zero))))
- (term (hole (((((elim nat Type) (λ (x : nat) nat))
+ (term (hole (elim nat (λ (x : nat) nat) ()
-                (s zero))
+                   ((s zero) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
-               (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+                   (s zero)))))
-              (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
 ;; ------------------------------------------------------------------------
@@ -179,6 +142,8 @@
 (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)))
@@ -188,63 +153,71 @@
                   (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-equiv? (term (reduce ,Δ (((((elim nat Type) (λ (x : nat) nat))
+
-                                  (s zero))
+(check-equal? (term (Δ-constructor-index ,Δ nat zero)) 0)
-                                 (λ (x : nat) (λ (ih-x : nat)
+(check-equiv? (term (reduce ,Δ (elim nat (λ (x : nat) nat)
-                                                (s (s x)))))
+                                     ()
-                                zero)))
+                                     ((s zero)
+                                      (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+                                     zero)))
               (term (s zero)))
-(check-equiv? (term (reduce ,Δ (((((elim nat Type) (λ (x : nat) nat))
+(check-equiv? (term (reduce ,Δ (elim nat (λ (x : nat) nat)
-                                  (s zero))
+                                     ()
-                                 (λ (x : nat) (λ (ih-x : nat)
+                                     ((s zero)
-                                                (s (s x)))))
+                                      (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
-                                (s zero))))
+                                     (s zero))))
               (term (s (s zero))))
-(check-equiv? (term (reduce ,Δ (((((elim nat Type) (λ (x : nat) nat))
+(check-equiv? (term (reduce ,Δ (elim nat (λ (x : nat) nat)
-                                  (s zero))
+                                     ()
-                                 (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+                                     ((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 Type) (λ (x : nat) nat))
+               (elim nat (λ (x : nat) nat)
-                  (s (s zero)))
+                     ()
-                 (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
+                     ((s (s zero))
-                (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 Type) (λ (x : nat) nat))
+             (elim nat (λ (x : nat) nat)
-                (s (s zero)))
+                     ()
-               (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
+                     ((s (s zero))
-              (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 Type) (λ (x : nat) nat))
+   (elim nat (λ (x : nat) nat)
-      (s (s zero)))
+         ()
-     (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
+         ((s (s zero))
-    (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 Type) (λ (x : nat) nat))
+                       (elim nat (λ (x : nat) nat)
-                          (s (s zero)))
+                             ()
-                         (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
+                             ((s (s zero))
-                        (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 Type) (λ (x : nat) nat))
+    (elim nat (λ (x : nat) nat)
-       (s (s zero)))
+          ()
-      (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
+          ((s (s zero))
-     zero)))))
+           (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
+          zero)))))
 
 (define-syntax-rule (check-equivalent e1 e2)
-  (check-holds (equivalent ∅ e1 e2)))
+  (check-holds (convert ∅ ∅ e1 e2)))
 (check-equivalent
  (λ (x : Type) x) (λ (y : Type) y))
 (check-equivalent
@@ -343,28 +316,42 @@
                U))
 ;; ---- Elim
 ;; TODO: Clean up/Reorganize these tests
-(check-true
- (redex-match? tt-typingL
-               (in-hole Θ_m (((elim x_D U) e_D) e_P))
-               (term ((((elim truth Type) T) (Π (x : truth) (Unv 1))) (Unv 0)))))
 (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-telescope-equiv?
+(check-equiv?
- (term (Δ-methods-telescope ,Δtruth truth (λ (x : truth) (Unv 1))))
+ (term (Δ-motive-type ,Δtruth truth (Unv 2)))
- (term (Π (m-T : ((λ (x : truth) (Unv 1)) T)) hole)))
+ (term (Π (x : truth) (Unv 2))))
-(check-holds (type-infer ,Δtruth ∅ (elim truth Type) t))
+
-(check-holds (type-check (∅ (truth : (Unv 0) ((T : truth))))
+
+(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 (Unv 2)) (λ (x : truth) (Unv 1))) (Unv 0))
+                         (elim truth (λ (x : truth) (Unv 1))
-                          T)
+                               () ((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 (Unv 1)) Type) Type) T)
+                             (elim truth Type () (Type) T)
                              (Unv 1)))
 (check-holds
  (type-infer ∅ ∅ (Π (x2 : (Unv 0)) (Unv 0)) U))
@@ -382,47 +369,54 @@
   (check-holds (type-check ,Δ syn ...)))
 (nat-test ∅ (Π (x : nat) nat) (Unv 0))
 (nat-test ∅ (λ (x : nat) x) (Π (x : nat) nat))
-(nat-test ∅ (((((elim nat Type) (λ (x : nat) nat)) zero)
+(nat-test ∅ (elim nat (λ (x : nat) nat) ()
-              (λ (x : nat) (λ (ih-x : nat) x))) zero)
+                  (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)
-;; TODO: Meta-function auto-currying and such
 (check-holds
- (type-infer ,Δ ∅ ((((elim nat (Unv 0)) (λ (x : nat) nat))
+ (type-infer ,Δ ∅ (λ (x : nat)
-                    zero)
+                    (elim nat (λ (x : nat) nat)
-                   (λ (x : nat) (λ (ih-x : nat) x)))
+                          ()
+                          (zero
+                           (λ (x : nat) (λ (ih-x : nat) x)))
+                          x))
              t))
-(nat-test ∅ (((((elim nat (Unv 0)) (λ (x : nat) nat))
+(nat-test ∅ (elim nat (λ (x : nat) nat)
-               zero)
+                  ()
-              (λ (x : nat) (λ (ih-x : nat) x)))
+                  (zero (λ (x : nat) (λ (ih-x : nat) x)))
-             zero)
+                  zero)
             nat)
-(nat-test ∅ (((((elim nat (Unv 0)) (λ (x : nat) nat))
+(nat-test ∅ (elim nat (λ (x : nat) nat)
-               (s zero))
+                  ()
-              (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+                  ((s zero) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
-             zero)
+                  zero)
             nat)
-(nat-test ∅ (((((elim nat Type) (λ (x : nat) nat))
+(nat-test ∅ (elim nat (λ (x : nat) nat)
-               (s zero))
+                  ()
-              (λ (x : nat) (λ (ih-x : nat) (s (s x))))) zero)
+                  ((s zero) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+                  zero)
             nat)
 (nat-test (∅ n : nat)
-          (((((elim nat (Unv 0)) (λ (x : nat) nat)) zero) (λ (x : nat) (λ (ih-x : nat) x))) n)
+          (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 (Unv 0)) (λ (x : nat) bool))
+             (elim nat (λ (x : nat) bool)
-                btrue)
+                   ()
-               (λ (x : nat) (λ (ih-x : bool) bfalse)))
+                   (btrue (λ (x : nat) (λ (ih-x : bool) bfalse)))
-              n2)
+                   n2)
              bool))
 (check-not-holds
  (type-check ,Δ ∅
-             ((((elim nat (Unv 0)) nat) (s zero)) zero)
+             (elim nat nat () ((s zero)) zero)
              nat))
 (define lam (term (λ (nat : (Unv 0)) nat)))
 (check-equivalent
@@ -481,15 +475,15 @@
              (in-hole Ξ (Π (x : (in-hole Θ_Ξ and)) U_P))))
 (check-holds
  (type-check (,Δ4 (true : (Unv 0) ((tt : true)))) ∅
-             ((((((elim and (Unv 0))
+             (elim and
-                  (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B))
+                   (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B))
-                                                true))))
+                                                 true)))
-                 (λ (A : (Unv 0))
+                   (true true)
-                   (λ (B : (Unv 0))
+                   ((λ (A : (Unv 0))
-                     (λ (a : A)
+                      (λ (B : (Unv 0))
-                       (λ (b : B) tt)))))
+                        (λ (a : A)
-                true) true)
+                          (λ (b : B) tt)))))
-              ((((conj true) true) tt) tt))
+                   ((((conj true) true) tt) tt))
              true))
 (check-true (Γ? (term (((∅ P : (Unv 0)) Q : (Unv 0)) ab : ((and P) Q)))))
 (check-holds
@@ -507,7 +501,7 @@
                                            ((and B) A))))
              (in-hole Ξ (Π (x : (in-hole Θ and)) U))))
 (check-holds
- (equivalent ,Δ4
+ (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
@@ -518,14 +512,15 @@
 (check-holds
  (type-check ,Δ4
              (((∅ P : (Unv 0)) Q : (Unv 0)) ab : ((and P) Q))
-             ((((((elim and (Unv 0))
+             (elim and
-                  (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B))
+                   (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B))
-                                                ((and B) A)))))
+                                                 ((and B) A))))
-                 (λ (A : (Unv 0))
+                   (P Q)
-                   (λ (B : (Unv 0))
+                   ((λ (A : (Unv 0))
-                     (λ (a : A)
+                      (λ (B : (Unv 0))
-                       (λ (b : B) ((((conj B) A) b) a))))))
+                        (λ (a : A)
-                P) Q) ab)
+                          (λ (b : B) ((((conj B) A) b) a))))))
+                   ab)
              ((and Q) P)))
 (check-holds
  (type-check (,Δ4 (true : (Unv 0) ((tt : true)))) ∅
@@ -538,14 +533,14 @@
              t))
 (check-holds
  (type-check (,Δ4 (true : (Unv 0) ((tt : true)))) ∅
-             ((((((elim and (Unv 0))
+             (elim and
                   (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B))
-                                                ((and B) A)))))
+                                                ((and B) A))))
-                 (λ (A : (Unv 0))
+                 (true true)
+                 ((λ (A : (Unv 0))
                    (λ (B : (Unv 0))
                      (λ (a : A)
                        (λ (b : B) ((((conj B) A) b) a))))))
-                true) true)
               ((((conj true) true) tt) tt))
              ((and true) true)))
 (define gamma (term (∅ temp863 : pre)))
@@ -568,21 +563,18 @@
 (check-holds
  (type-infer ,sigma (,gamma x : false) (λ (y : false) (Π (x : Type) x))
              (in-hole Ξ (Π (x : (in-hole Θ false)) U))))
-(check-true
+
- (redex-match? tt-typingL
-               ((in-hole Θ_m ((elim x_D U) e_P)) e_D)
-               (term (((elim false (Unv 1)) (λ (y : false) (Π (x : Type) x)))
-                      x))))
 (check-holds
  (type-check ,sigma (,gamma x : false)
-             (((elim false (Unv 0)) (λ (y : false) (Π (x : Type) x))) x)
+             (elim false (λ (y : false) (Π (x : Type) x)) () () x)
              (Π (x : (Unv 0)) x)))
 
 ;; nat-equal? tests
 (define zero?
-  (term ((((elim nat Type) (λ (x : nat) bool))
+  (term (λ (n : nat)
-          true)
+          (elim nat (λ (x : nat) bool) ()
-         (λ (x : nat) (λ (x_ih : bool) false)))))
+              (true (λ (x : nat) (λ (x_ih : bool) false)))
+              n))))
 (check-holds
  (type-check ,Δ ∅ ,zero? (Π (x : nat) bool)))
 (check-equal?
@@ -592,9 +584,12 @@
  (term (reduce ,Δ (,zero? (s zero))))
  (term false))
 (define ih-equal?
-  (term ((((elim nat Type) (λ (x : nat) bool))
+  (term (λ (ih : nat)
-          false)
+          (elim nat (λ (x : nat) bool)
-         (λ (x : nat) (λ (y : bool) (x_ih x))))))
+              ()
+              (false
+               (λ (x : nat) (λ (y : bool) (x_ih x))))
+              ih))))
 (check-holds
  (type-check ,Δ (∅ x_ih : (Π (x : nat) bool))
              ,ih-equal?
@@ -606,10 +601,13 @@
 (check-holds
  (type-infer ,Δ ∅ (λ (x : nat) (Π (x : nat) bool)) (Π (x : nat) (Unv 0))))
 (define nat-equal?
-  (term ((((elim nat Type) (λ (x : nat) (Π (x : nat) bool)))
+  (term (λ (n : nat)
-          ,zero?)
+          (elim nat (λ (x : nat) (Π (x : nat) bool))
-         (λ (x : nat) (λ (x_ih : (Π (x : nat) bool))
+              ()
-                        ,ih-equal?)))))
+              (,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)
@@ -631,19 +629,12 @@
 (check-true (Δ? Δ=))
 
 (define refl-elim
-  (term (((((((elim == (Unv 0)) (λ (A1 : (Unv 0)) (λ (x1 : A1) (λ (y1 : A1) (λ (p2 : (((==
+  (term (elim == (λ (A1 : (Unv 0)) (λ (x1 : A1) (λ (y1 : A1) (λ (p2 : (((== A1) x1) y1)) nat))))
-                                                                                        A1)
+                  (bool true true)
-                                                                                       x1)
+                  ((λ (A1 : (Unv 0)) (λ (x1 : A1) zero)))
-                                                                                      y1))
+                  ((refl bool) true))))
-                                                                              nat)))))
-             (λ (A1 : (Unv 0)) (λ (x1 : A1) zero))) bool) true) true) ((refl bool) true))))
 (check-holds
  (type-check ,Δ= ∅ ,refl-elim nat))
-(check-true
- (redex-match?
-  tt-redL
-  (Δ (in-hole E (in-hole Θ ((elim x_D U) e_P))))
-  (term (,Δ= ,refl-elim))))
 (check-true
  (redex-match?
   tt-redL

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

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

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

@@ -11,11 +11,10 @@
  (some Bool true))
 ;; Disabled until #22 fixed
 #;(check-equal?
-   (case* Maybe Type (some Bool true) (Bool)
+   (match (some Bool true)
-          (lambda* (A : Type) (x : (Maybe A)) A)
+     [(none (A : Type))
-          [(none (A : Type)) IH: ()
+      false]
-           false]
+     [(some (A : Type) (x : A))
-          [(some (A : Type) (x : A)) IH: ()
+      ;; TODO: Don't know how to use dependency yet
-           ;; TODO: Don't know how to use dependency yet
+      (if x true false)])
-           (if x true false)])
    true)

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

@@ -11,11 +11,11 @@
 (:: pf:proj1 thm:proj1)
 (:: pf:proj2 thm:proj2)
 (check-equal?
- (elim == Type (λ* (A : Type) (x : A) (y : A) (p : (== A x y)) Nat)
+ (elim == (λ (A : Type) (x : A) (y : A) (p : (== A x y)) Nat)
-       (λ* (A : Type) (x : A) z)
+       (Bool
-       Bool
+        true
-       true
+        true)
-       true
+       ((λ (A : Type) (x : A) z))
        (refl Bool true))
  z)
 

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

@@ -5,19 +5,19 @@
 
 ;; TODO: Missing tests for match, others
 (check-equal?
- ((λ* (x : (Type 1)) (y : (∀* (x : (Type 1)) (Type 1))) (y x))
+ ((λ (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))
+ ((λ (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))
+ ((λ (x : (Type 1)) (y : (→ (Type 1) (Type 1))) (y x))
   Type
   (λ (x : (Type 1)) x))
  Type)

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

@@ -8,12 +8,10 @@
  cur/stdlib/typeclass)
 
 (typeclass (Eqv (A : Type))
-           (equal? : (forall* (a : A) (b : A) Bool)))
+           (equal? : (forall (a : A) (b : A) Bool)))
 (impl (Eqv Bool)
       (define (equal? (a : Bool) (b : Bool))
-        (if a
+        (if a b (not b))))
-            (if b true false)
-            (if b false true))))
 (impl (Eqv Nat)
       (define equal? nat-equal?))
 (check-equal?

cur-test/cur/tests/stlc.rkt

@@ -2,6 +2,7 @@
 (require
  rackunit
  cur/stdlib/nat
+ cur/stdlib/list
  cur/stdlib/sugar
  cur/olly
  cur/stdlib/maybe
@@ -15,65 +16,55 @@
   (val  (v)   ::= true false unit)
   ;; TODO: Allow datum, like 1, as terminals
   (type (A B) ::= boolty unitty (-> A B) (* A A))
-  (term (e)   ::= x v (app e e) (lambda (x : A) e) (cons e e)
+  (term (e)   ::= x v (app e e) (lambda (#:bind x : A) e) (cons e e)
-                  (let (x x) = e in e)))
+                  (let (#:bind x #:bind x) = e in e)))
 
-;; TODO: Abstract this over stlc-type, and provide from in OLL
+(define lookup-env (list-ref stlc-type))
-(data Gamma : Type
-  (emp-gamma : Gamma)
-  (extend-gamma : (->* Gamma Var stlc-type Gamma)))
 
-(define (lookup-gamma (g : Gamma) (x : Var))
+(define (extend-env (g : (List stlc-type)) (t : stlc-type))
-  (case* Gamma Type g () (lambda* (g : Gamma) (Maybe stlc-type))
+  (cons stlc-type t g))
-    [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)
+(define-relation (has-type (List stlc-type) stlc-term stlc-type)
   #:output-coq "stlc.v"
   #:output-latex "stlc.tex"
-  [(g : Gamma)
+  [(g : (List stlc-type))
    ------------------------ T-Unit
-   (has-type g (stlc-val-->-stlc-term stlc-unit) stlc-unitty)]
+   (has-type g (stlc-val->stlc-term stlc-unit) stlc-unitty)]
 
-  [(g : Gamma)
+  [(g : (List stlc-type))
    ------------------------ T-True
-   (has-type g (stlc-val-->-stlc-term stlc-true) stlc-boolty)]
+   (has-type g (stlc-val->stlc-term stlc-true) stlc-boolty)]
 
-  [(g : Gamma)
+  [(g : (List stlc-type))
    ------------------------ T-False
-   (has-type g (stlc-val-->-stlc-term stlc-false) stlc-boolty)]
+   (has-type g (stlc-val->stlc-term stlc-false) stlc-boolty)]
 
-  [(g : Gamma) (x : Var) (t : stlc-type)
+  [(g : (List stlc-type)) (x : Nat) (t : stlc-type)
-   (== (Maybe stlc-type) (lookup-gamma g x) (some stlc-type t))
+   (== (Maybe stlc-type) (lookup-env g x) (some stlc-type t))
    ------------------------ T-Var
-   (has-type g (Var-->-stlc-term x) t)]
+   (has-type g (Nat->stlc-term x) t)]
 
-  [(g : Gamma) (e1 : stlc-term) (e2 : stlc-term)
+  [(g : (List stlc-type)) (e1 : stlc-term) (e2 : stlc-term)
                (t1 : stlc-type) (t2 : stlc-type)
    (has-type g e1 t1)
    (has-type g e2 t2)
    ---------------------- T-Pair
    (has-type g (stlc-cons e1 e2) (stlc-* t1 t2))]
 
-  [(g : Gamma) (e1 : stlc-term) (e2 : stlc-term)
+  [(g : (List stlc-type)) (e1 : stlc-term) (e2 : stlc-term)
                (t1 : stlc-type) (t2 : stlc-type)
                (t : stlc-type)
-               (x : Var) (y : Var)
    (has-type g e1 (stlc-* t1 t2))
-   (has-type (extend-gamma (extend-gamma g x t1) y t2) e2 t)
+   (has-type (extend-env (extend-env g t1) t2) e2 t)
    ---------------------- T-Let
-   (has-type g (stlc-let x y e1 e2) t)]
+   (has-type g (stlc-let e1 e2) t)]
 
-  [(g : Gamma) (e1 : stlc-term) (t1 : stlc-type) (t2 : stlc-type) (x : Var)
+  [(g : (List stlc-type)) (e1 : stlc-term) (t1 : stlc-type) (t2 : stlc-type)
-   (has-type (extend-gamma g x t1) e1 t2)
+   (has-type (extend-env g t1) e1 t2)
    ---------------------- T-Fun
-   (has-type g (stlc-lambda x t1 e1) (stlc--> t1 t2))]
+   (has-type g (stlc-lambda t1 e1) (stlc--> t1 t2))]
 
-  [(g : Gamma) (e1 : stlc-term) (e2 : stlc-term)
+  [(g : (List stlc-type)) (e1 : stlc-term) (e2 : stlc-term)
                (t1 : stlc-type) (t2 : stlc-type)
    (has-type g e1 (stlc--> t1 t2))
    (has-type g e2 t1)
@@ -85,59 +76,57 @@
 ;; TODO: When generating a parser, will need something like (#:name app (e e))
 ;; so I can name a constructor without screwing with syntax.
 (begin-for-syntax
-  (define index #'z))
+  (define (dict-shift d)
+    (for/fold ([d (make-immutable-hash)])
+              ([(k v) (in-dict d)])
+      (dict-set d k #`(s #,v)))))
 (define-syntax (begin-stlc syn)
-  (set! index #'z)
+  (let stlc ([syn (syntax-case syn () [(_ e) #'e])]
-  (let stlc ([syn (syntax-case syn () [(_ e) #'e])])
+             [d (make-immutable-hash)])
     (syntax-parse syn
       #:datum-literals (lambda : prj * -> quote let in cons bool)
       [(lambda (x : t) e)
-       (let ([oldindex index])
+       #`(stlc-lambda #,(stlc #'t d) #,(stlc #'e (dict-set (dict-shift d) (syntax->datum #'x) #`z)))]
-         (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))]
+       #`(stlc-cons #,(stlc #'e1 d) #,(stlc #'e2 d))]
       [(let (x y) = e1 in e2)
-       (let* ([y index]
+       #`(stlc-let #,(stlc #'t d) #,(stlc #'e1 d)
-              [x #`(s #,y)])
+                   #,(stlc #'e2 (dict-set* (dict-shift (dict-shift d))
-         (set! index #`(s (s #,index)))
+                                           (syntax->datum #'x) #`z
-         #`((lambda* (x : stlc-term) (y : stlc-term)
+                                           (syntax->datum #'y) #`(s z))))]
-              (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-app #,(stlc #'e1 d) #,(stlc #'e2 d))]
-      [() #'(stlc-val-->-stlc-term stlc-unit)]
+      [() #'(stlc-val->stlc-term stlc-unit)]
-      [#t #'(stlc-val-->-stlc-term stlc-true)]
+      [#t #'(stlc-val->stlc-term stlc-true)]
-      [#f #'(stlc-val-->-stlc-term stlc-false)]
+      [#f #'(stlc-val->stlc-term stlc-false)]
       [(t1 * t2)
-       #`(stlc-* #,(stlc #'t1) #,(stlc #'t2))]
+       #`(stlc-* #,(stlc #'t1 d) #,(stlc #'t2 d))]
       [(t1 -> t2)
-       #`(stlc--> #,(stlc #'t1) #,(stlc #'t2))]
+       #`(stlc--> #,(stlc #'t1 d) #,(stlc #'t2 d))]
       [bool #`stlc-boolty]
       [e
-       (if (eq? 1 (syntax->datum #'e))
+       (cond
-           #'stlc-unitty
+         [(eq? 1 (syntax->datum #'e))
-           #'e)])))
+          #'stlc-unitty]
+         [(dict-ref d (syntax->datum #'e) #f) =>
+          (lambda (x)
+            #`(Nat->stlc-term #,x))]
+         [else #'e])])))
 
 (check-equal?
  (begin-stlc (lambda (x : 1) x))
- (stlc-lambda (avar z) stlc-unitty (Var-->-stlc-term (avar z))))
+ (stlc-lambda stlc-unitty (Nat->stlc-term z)))
 (check-equal?
  (begin-stlc ((lambda (x : 1) x) ()))
- (stlc-app (stlc-lambda (avar z) stlc-unitty (Var-->-stlc-term (avar z)))
+ (stlc-app (stlc-lambda stlc-unitty (Nat->stlc-term z))
-           (stlc-val-->-stlc-term stlc-unit)))
+           (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-cons (stlc-val->stlc-term stlc-unit)
-            (stlc-val-->-stlc-term stlc-unit)))
+            (stlc-val->stlc-term stlc-unit)))
 (check-equal?
  (begin-stlc #t)
- (stlc-val-->-stlc-term stlc-true))
+ (stlc-val->stlc-term stlc-true))

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

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

cur-test/info.rkt

@@ -1,7 +1,7 @@
 #lang info
 (define collection 'multi)
 (define deps '())
-(define build-deps '("base" "rackunit-lib" ("cur-lib" #:version "0.2")))
+(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))