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.
Bumped version
2016-03-24 16:03:51 -04:00 · 2016-03-22 18:22:36 -04:00 · 2016-03-22 13:33:51 -04:00 · 2016-03-22 13:16:30 -04:00 · 2016-03-18 16:39:32 -04:00 · 2016-03-17 17:02:10 -04:00
31 changed files with 651 additions and 605 deletions
--- a/README.md
+++ b/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
--- a/cur-doc/cur/scribblings/curnel.scrbl
+++ b/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)
-           (λ (id : type-expr) body-expr))]{
-Produces a single arity procedure, binding the identifier @racket[id] of type @racket[type-expr] in @racket[body-expr] and in the type of
-@racket[body-expr].
-Both @racket[type-expr] and @racket[body-expr] can contain non-curnel forms, such as macros.
+@defform[(λ (id : type-expr) body-expr)]{
+Produces a single-arity procedure, binding the identifier @racket[id] of type
+@racket[type-expr] in @racket[body-expr] and in the type of @racket[body-expr].
+Both @racket[type-expr] and @racket[body-expr] can contain non-curnel forms,
+such as macros.

-Currently, Cur will return the underlying representation of a procedure when a @racket[lambda] is
-evaluated at the top-level. Do not rely on this representation.
+Currently, Cur will return the underlying representation of a procedure when a
+@racket[λ] is evaluated at the top-level.
+Do not rely on this representation.

@examples[#:eval curnel-eval
-          (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)
-           (∀ (id : type-expr) body-expr))]{
-Produces a dependent function type, binding the identifier @racket[id] of type @racket[type-expr] in @racket[body-expr].
+@defform[(Π (id : type-expr) body-expr)]{
+Produces a dependent function type, binding the identifier @racket[id] of type
+@racket[type-expr] in @racket[body-expr].


@examples[#:eval curnel-eval
-          (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))
-            (conj : (forall (A : Type) (forall (B : Type) (forall (a : A) (forall (b : B) ((And A) B)))))))
+          (data And : (Π (A : Type) (Π (B : Type) Type))
+            (conj : (Π (A : Type) (Π (B : Type) (Π (a : A) (Π (b : B) ((And A) B)))))))
          ((((conj Bool) Bool) true) false)]
 }

-@defform[(elim type motive-universe)]{
-Returns the inductive eliminator for @racket[type] where the @racket[motive-universe] is the universe
-of the motive.
-The eliminator expects the next argument to be the motive, the next @racket[N] arguments to be the methods for
-each of the @racket[N] constructors of the inductive type @racket[type], the next @racket[P] arguments
-to be the parameters @racket[p_0 ... p_P] of the inductive @racket[type], and the final argument to be the term to
-eliminate of type @racket[(type p_0 ... p_P)].
+@defform[(elim inductive-type motive (index ...) (method ...) disc)]{
+Fold over the term @racket[disc] of the inductively defined type @racket[inductive-type].
+The @racket[motive] is a function that expects the indices of the inductive
+type and a term of the inductive type and produces the type that this
+fold returns.
+The type of @racket[disc] is @racket[(inductive-type index ...)].
+@racket[elim] takes one method for each constructor of @racket[inductive-type].
+Each @racket[method] expects the arguments for its corresponding constructor,
+and the inductive hypotheses generated by recursively eliminating all recursive
+arguments of the constructor.

 The following example runs @racket[(sub1 (s z))].

@examples[#:eval curnel-eval
          (data Nat : Type
            (z : Nat)
-            (s : (forall (n : Nat) Nat)))
-          (((((elim Nat Type)
-              (lambda (x : Nat) Nat))
-             z)
-            (lambda (n : Nat) (lambda (IH : Nat) n)))
-           (s z))]
+            (s : (Π (n : Nat) Nat)))
+          (elim Nat (λ (x : Nat) Nat)
+                ()
+                (z
+                 (λ (n : Nat) (λ (IH : Nat) n)))
+                (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)))
-          (define sub1 (lambda (n : Nat)
-                         (((((elim Nat Type) (lambda (x : Nat) Nat))
-                           z)
-                          (lambda (n : Nat) (lambda (IH : Nat) n))) n)))
+            (s : (Π (n : Nat) Nat)))
+          (define sub1 (λ (n : Nat)
+                         (elim Nat (λ (x : Nat) Nat)
+                               ()
+                               (z
+                                (λ (n : Nat) (λ (IH : Nat) n)))
+                               n)))
          (sub1 (s (s z)))
          (sub1 (s z))
          (sub1 z)]
--- a/cur-doc/cur/scribblings/reflection.scrbl
+++ b/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:result @racket[#'(lambda (x : Type) x)] "" ""))
+(eval:alts (cur-expand #'(λ (x : (computed-type bla)) x))
+           (eval:result @racket[#'(λ (x : Type) x)] "" ""))
 ]
 }

-@defproc[(type-infer/syn [syn syntax?])
+@defproc[(cur-type-infer [syn syntax?])
         (or/c syntax? #f)]{
 Returns the type of the Cur term @racket[syn], or @racket[#f] if no type could be inferred.

@examples[
-(eval:alts (type-infer/syn #'(lambda (x : Type) x))
-           (eval:result @racket[#'(forall (x : (Type 0)) (Type 0))] "" ""))
-(eval:alts (type-infer/syn #'Type)
+(eval:alts (cur-type-infer #'(λ (x : Type) x))
+           (eval:result @racket[#'(Π (x : (Type 0)) (Type 0))] "" ""))
+(eval:alts (cur-type-infer #'Type)
           (eval:result @racket[#'(Type 1)] "" ""))
 ]
 }

-@defproc[(type-check/syn? [syn syntax?])
+@defproc[(cur-type-check? [syn syntax?])
         boolean?]{
 Returns @racket[#t] if the Cur term @racket[syn] is well-typed, or @racket[#f] otherwise.

@examples[
-(eval:alts (type-check/syn? #'(lambda (x : Type) x))
+(eval:alts (cur-type-check? #'(λ (x : Type) x))
           (eval:result @racket[#t] "" ""))
-(eval:alts (type-check/syn? #'Type)
+(eval:alts (cur-type-check? #'Type)
           (eval:result @racket[#t] "" ""))
-(eval:alts (type-check/syn? #'x)
+(eval:alts (cur-type-check? #'x)
           (eval:result @racket[#f] "" ""))
 ]
 }

-@defproc[(normalize/syn [syn syntax?])
+@defproc[(cur-normalize [syn syntax?])
         syntax?]{
 Runs the Cur term @racket[syn] to a value.

@examples[
-(eval:alts (normalize/syn #'((lambda (x : Type) x) Bool))
+(eval:alts (cur-normalize #'((λ (x : Type) x) Bool))
           (eval:result @racket[#'Bool] "" ""))
-(eval:alts (normalize/syn #'(sub1 (s (s z))))
+(eval:alts (cur-normalize #'(sub1 (s (s z))))
           (eval:result @racket[#'(s z)] "" ""))
 ]
 }

-@defproc[(step/syn [syn syntax?])
+@defproc[(cur-step [syn syntax?])
         syntax?]{
 Runs the Cur term @racket[syn] for one step.

@examples[
-(eval:alts (step/syn #'((lambda (x : Type) x) Bool))
+(eval:alts (cur-step #'((λ (x : Type) x) Bool))
           (eval:result @racket[#'Bool] "" ""))
-(eval:alts (step/syn #'(sub1 (s (s z))))
-           (eval:result @racket[#'(((((elim Nat (Type 0))
-                                      (lambda (x2 : Nat) Nat)) z)
-                                    (lambda (x2 : Nat) (lambda (ih-n2 : Nat) x2)))
-                                   (s (s z)))] "" ""))
+(eval:alts (cur-step #'(sub1 (s (s z))))
+           (eval:result @racket[#'(elim Nat (λ (x2 : Nat) Nat)
+                                        ()
+                                        (z (λ (x2 : Nat) (λ (ih-n2 : Nat) x2)))
+                                        (s (s z)))] "" ""))
 ]
 }

@ -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))] "" ""))
 ]
 }
--- a/cur-doc/cur/scribblings/stdlib.scrbl
+++ b/cur-doc/cur/scribblings/stdlib.scrbl
@ -7,10 +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}
--- a/cur-doc/cur/scribblings/stdlib/bool.scrbl
+++ b/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])
--- a/cur-doc/cur/scribblings/stdlib/sugar.scrbl
+++ b/cur-doc/cur/scribblings/stdlib/sugar.scrbl
@ -21,12 +21,15 @@ This library defines various syntactic extensions making Cur easier to write tha
@defform*[((-> decl decl ... type)
           (→ decl decl ... type)
 	   (forall decl decl ... type)
-	   (∀ 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)
@ -59,21 +62,24 @@ Defines multi-arity procedure application via automatic currying.
          (conj Bool Bool true false)]
 }

-@defform*[((define name body)
-           (define (name (x : t) ...) body))]{
-Like the @racket[define] provided by @racketmodname[cur], but supports
-defining curried functions via @racket[lambda].
+@defform[(: name type)]{
+Declare that the @emph{function} which will be defined as @racket[name] has type @racket[type].
+Must precede the definition of @racket[name].
+@racket[type] must expand to a function type of the form @racket[(Π (x : t1) t2)]
+When used, this form allows omitting the annotations on arguments in the definition @racket[name]
 }

-@defform[(elim type motive-result-type e ...)]{
-Like the @racket[elim] provided by @racketmodname[cur], but supports
-automatically curries the remaining arguments @racket[e ...].
+@defform*[((define name body)
+           (define (name x ...) body)
+	   (define (name (x : t) ...) body))]{
+Like the @racket[define] provided by @racketmodname[cur], but supports
+defining curried functions via @racket[lambda].
+The second form, @racket[(define (name x ...) body)], can only be used when
+a @racket[(: name type)] form appears earlier in the module.

@examples[#:eval curnel-eval
-          (elim Bool Type (lambda (x : Bool) Bool)
-            false
-            true
-            true)]
+          (: id (forall (A : Type) (a : A) A))
+	  (define (id A a) a)]
 }

@defform*[((define-type name type)
@ -166,7 +172,7 @@ 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 to be used in surface syntax.
+Like @racket[cur-normalize], but is a syntactic form to be used in surface syntax.
 Allows a Cur term to be written by computing part of the term from
 another Cur term.

@ -176,7 +182,7 @@ 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
--- a/cur-doc/info.rkt
+++ b/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))
--- a/cur-lib/cur/curnel/redex-core.rkt
+++ b/cur-lib/cur/curnel/redex-core.rkt
@ -26,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))
@ -44,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)
@ -53,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)
@ -105,27 +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 or #f
-  [(Δ-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)]
-  [(Δ-key-by-constructor Δ x)
-   #f])
-
-;; 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
@ -145,14 +127,6 @@
 ;; TODO: Mix of pure Redex/escaping to Racket sometimes is getting confusing.
 ;; TODO: Justify, or stop.

-;; Return the number of constructors that D has
-(define-metafunction ttL
-  Δ-constructor-count : Δ D -> natural or #f
-  [(Δ-constructor-count Δ D)
-   ,(length (term (x ...)))
-   (where (x ...) (Δ-ref-constructors Δ D))]
-  [(Δ-constructor-count Δ D) #f])
-
 ;; NB: Depends on clause order
 (define-metafunction ttL
  sequence-index-of : any (any ...) -> natural
@ -189,47 +163,31 @@
 ;; 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))?
- | Maybe not. t is a lambda whose type is equivalent to (Ξ-apply Ξ t)? Yes.
+ | that (convert t (Ξ-apply Ξ t))?
+ | Maybe not. t is a lambda whose type is convert to (Ξ-apply Ξ t)? Yes.
 |#
 (define-metafunction tt-ctxtL
  Ξ-apply : Ξ t -> t
  [(Ξ-apply hole t) t]
  [(Ξ-apply (Π (x : t) Ξ) t_0) (Ξ-apply Ξ (t_0 x))])

-;; 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
-  [(Θ-length hole) 0]
-  [(Θ-length (Θ e)) ,(add1 (term (Θ-length Θ)))])
-
-;; Convert an apply context to a sequence of terms
-(define-metafunction tt-ctxtL
-  Θ->list : Θ -> (e ...)
-  [(Θ->list hole) ()]
-  [(Θ->list (Θ e))
-   (e_r ... e)
-   (where (e_r ...) (Θ->list Θ))])
-
 (define-metafunction tt-ctxtL
  list->Θ : (e ...) -> Θ
  [(list->Θ ()) hole]
  [(list->Θ (e e_r ...))
   (in-hole (list->Θ (e_r ...)) (hole e))])

+(define-metafunction tt-ctxtL
+  apply : e e ... -> e
+  [(apply e_f e ...)
+   (in-hole (list->Θ (e ...)) e_f)])
+
 ;; Reference an expression in Θ by index; index 0 corresponds to the the expression applied to a hole.
 (define-metafunction tt-ctxtL
  Θ-ref : Θ natural -> e or #f
@ -251,15 +209,6 @@
  [(Δ-ref-parameter-Ξ Δ x)
   #f])

-;; Return the number of parameters of D
-(define-metafunction tt-ctxtL
-  Δ-parameter-count : Δ D -> natural or #f
-  [(Δ-parameter-count Δ D)
-   (Ξ-length Ξ)
-   (where Ξ (Δ-ref-parameter-Ξ Δ D))]
-  [(Δ-parameter-count Δ D)
-   #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 -> Ξ
@ -277,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
@ -320,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.
 ;;
@ -365,29 +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
+
+;; Returns the inductive hypotheses required for the elimination method of constructor c_i for
+;; inductive type D, when eliminating with motive t_P.
 (define-metafunction tt-ctxtL
-  Δ-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))
+  Δ-constructor-inductive-hypotheses : Δ D c t -> Ξ
+  [(Δ-constructor-inductive-hypotheses Δ D c_i t_P)
+   (hypotheses-loop D t_P (Δ-constructor-inductive-telescope Δ D c_i))])
+
+;; Returns the type of the method corresponding to c_i
+(define-metafunction tt-ctxtL
+  Δ-constructor-method-type : Δ D c t -> t
+  [(Δ-constructor-method-type Δ D c_i t_P)
+   (in-hole Ξ_a (in-hole Ξ_h ((in-hole Θ_p t_P) (Ξ-apply Ξ_a c_i))))
+   (where Θ_p (Δ-constructor-parameters Δ D c_i))
+   (where Ξ_a (Δ-constructor-telescope Δ D c_i))
+   (where Ξ_h (Δ-constructor-inductive-hypotheses Δ D c_i t_P))])
+
+(define-metafunction tt-ctxtL
+  Δ-method-types : Δ D e -> (t ...)
+  [(Δ-method-types Δ D e)
+   ,(map (lambda (c) (term (Δ-constructor-method-type Δ D ,c e))) (term (c ...)))
+   (where (c ...) (Δ-ref-constructors Δ D))])
+
+(define-metafunction tt-ctxtL
+  Δ-motive-type : Δ D U -> t
+  [(Δ-motive-type Δ D U)
+   (in-hole Ξ_P*D U)
+   (where Ξ (Δ-ref-parameter-Ξ Δ D))
   ;; A fresh name to bind the discriminant
-   (where x ,(variable-not-in (term (Δ Γ x_D Ξ)) 'x-D))
+   (where x ,(variable-not-in (term (Δ 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))])
+   ;; of the indices and the inductive type applied to the
+   ;; indices
+   (where Ξ_P*D (in-hole Ξ (Π (x : (Ξ-apply Ξ D)) hole)))])

 ;;; ------------------------------------------------------------------------
 ;;; Dynamic semantics
@ -395,16 +310,21 @@
 ;;; 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,
-  ;; determining whether or not it is partially applied cannot be done with the grammar alone.
-  (v   ::= x U (Π (x : t) t) (λ (x : t) t) (elim x U) (in-hole Θv x) (in-hole Θv (elim x U)))
-  (Θv  ::= hole (Θv v))
-  ;; call-by-value, plus reduce under Π (helps with typing checking)
-  (E   ::= hole (E e) (v E) (Π (x : v) E) (Π (x : E) e)))
+  (v  ::= x U (Π (x : t) t) (λ (x : t) t) (in-hole Θv c))
+  (Θv ::= hole (Θv v))
+  (C-elim  ::= (elim D t_P (e_i ...) (e_m ...) hole))
+  ;; call-by-value
+  (E  ::= hole (E e) (v E)
+      (elim D e (e ...) (v ... E e ...) e)
+      (elim D e (e ...) (v ...) E)
+      ;; reduce under Π (helps with typing checking)
+      ;; TODO: Should be done in conversion judgment
+      (Π (x : v) E) (Π (x : E) e)))

 (define Θv? (redex-match? tt-redL Θv))
 (define E? (redex-match? tt-redL E))
 (define v? (redex-match? tt-redL v))
+
 #|
 | The elim form must appear applied like so:
 | (elim D U v_P m_0 ... m_i m_j ... m_n p ... (c_i a ...))
@ -420,75 +340,6 @@
 |
 | Using contexts, this appears as (in-hole Θ ((elim D U) v_P))
 |#
-
-
-;;; NB: Next 3 meta-function Assume of Θ n constructors, j parameters, n+j+1-th element is discriminant
-
-;; Given the apply context Θ in which an elimination of D with motive
-;; v of type U appears, extract the parameters p ... from Θ.
-(define-metafunction tt-redL
-  elim-parameters : Δ D Θ -> Θ
-  [(elim-parameters Δ D Θ)
-    ;; Drop the methods, take the parameters
-   (list->Θ
-    ,(take
-      (drop (term (Θ->list Θ)) (term (Δ-constructor-count Δ D)))
-      (term (Δ-parameter-count Δ D))))])
-
-;; Given the apply context Θ in which an elimination of D with motive
-;; v of type U appears, extract the methods m_0 ... m_n from Θ.
-(define-metafunction tt-redL
-  elim-methods : Δ D Θ -> Θ
-  [(elim-methods Δ D Θ)
-   ;; Take the methods, one for each constructor
-   (list->Θ
-    ,(take
-      (term (Θ->list Θ))
-      (term (Δ-constructor-count Δ D))))])
-
-;; Given the apply context Θ in which an elimination of D with motive
-;; v of type U appears, extract the discriminant (c_i a ...) from Θ.
-(define-metafunction tt-redL
-  elim-discriminant : Δ D Θ -> e
-  [(elim-discriminant Δ D Θ)
-   ;; Drop the methods, the parameters, and take the last element
-   ,(car
-     (drop
-      (drop (term (Θ->list Θ)) (term (Δ-constructor-count Δ D)))
-      (term (Δ-parameter-count Δ D))))])
-
-;; Check that Θ is valid and ready to be evaluated as the arguments to an elim.
-;; has length m = n + j + 1 and D has n constructors and j parameters,
-;; and the 1 represents the discriminant.
-;; discharges assumption for previous 3 meta-functions
-(define-metafunction tt-redL
-  Θ-valid : Δ D Θ -> #t or #f
-  [(Θ-valid Δ D Θ)
-   #t
-   (where natural_m (Θ-length Θ))
-   (where natural_n (Δ-constructor-count Δ D))
-   (where natural_j (Δ-parameter-count Δ D))
-   (side-condition (= (+ (term natural_n) (term natural_j) 1) (term natural_m)))
-   ;; As Cur allows reducing (through reflection) open terms, 
-   ;; check that the discriminant is a canonical form so that
-   ;; reduction can proceed; otherwise not valid.
-   (where (in-hole Θ_i c_i) (elim-discriminant Δ D Θ))
-   (where D (Δ-key-by-constructor Δ c_i))]
-  [(Θ-valid Δ D Θ) #f])
-
-(module+ test
-  (require rackunit)
-  (check-equal?
-   (term (Θ-length (((hole (s zero)) (λ (x : nat) (λ (ih-x : nat) (s (s x))))) zero)))
-   3)
-  (check-true
-   (term
-    (Θ-valid
-     ((∅ (nat : (Unv 0) ((zero : nat) (s : (Π (x : nat) nat))))) (bool : (Unv 0) ((true : bool) (false : bool))))
-     nat
-     (((hole (s zero)) (λ (x : nat) (λ (ih-x : nat) (s (s x))))) zero)))))
-
-
 (define-metafunction tt-ctxtL
  is-inductive-argument : Δ D t -> #t or #f
  ;; Think this only works in call-by-value. A better solution would
@ -502,39 +353,34 @@
 ;; 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-ctxtL
-  Δ-inductive-elim : Δ x U t Θ Θ Θ -> Θ
+(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 Δ x_D U t_P Θ_p Θ_m (Θ_i t_i))
-   ((Δ-inductive-elim Δ x_D U t_P Θ_p Θ_m Θ_i)
-    (in-hole ((in-hole Θ_p Θ_m) t_i) ((elim x_D U) t_P)))
-   (side-condition (term (is-inductive-argument Δ x_D t_i)))]
-  [(Δ-inductive-elim Δ x_D U t_P Θ_p Θ_m (Θ_i t_i))
-   (Δ-inductive-elim Δ x_D U t_P Θ_p Θ_m Θ_i)]
-  [(Δ-inductive-elim Δ x_D U t_P Θ_p Θ_m hole)
-   hole])
+  [(Δ-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 D U) v_P))))
-         (Δ (in-hole E (in-hole Θ_r (in-hole Θv_i v_mi))))
-         ;; Check that Θv is valid to avoid capturing other things
-         (side-condition (term (Θ-valid Δ D Θv)))
-          ;; Split Θv into its components: the paramters Θv_P for x_D, the methods Θv_m for x_D, and
-          ;; the discriminant: the constructor c_i applied to its argument Θv_i
-         (where Θv_p (elim-parameters Δ D Θv))
-         (where Θv_m (elim-methods Δ D Θv))
-         (where (in-hole Θv_i c_i) (elim-discriminant Δ D Θv))
-         ;; Find the method for constructor x_ci, relying on the order of the arguments.
-         (where v_mi (Θ-ref Θv_m (Δ-constructor-index Δ D c_i)))
+    (--> (Δ (in-hole E (elim D e_motive (e_i ...) (v_m ...) (in-hole Θv_c c))))
+         (Δ (in-hole E (in-hole Θ_mi v_mi)))
+         ;; Find the method for constructor c_i, relying on the order of the arguments.
+         (where natural (Δ-constructor-index Δ D c))
+         (where v_mi ,(list-ref (term (v_m ...)) (term natural)))
         ;; Generate the inductive recursion
-         (where Θ_r (Δ-inductive-elim Δ 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
@ -550,16 +396,6 @@
   (where (_ e_r)
          ,(car (apply-reduction-relation* tt--> (term (Δ e)) #:cache-all? #t)))])

-(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

@ -569,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 Γ ∅) Γ]
@ -687,16 +541,22 @@
   ----------------- "DTR-Application"
   (type-infer Δ Γ (e_0 e_1) t_3)]

-  [(where t (Δ-elim-type Δ D U))
-   (type-infer Δ Γ t U_e)
+  [(type-check Δ Γ e_c (apply D e_i ...))
+
+   (type-infer Δ Γ e_motive (name t_motive (in-hole Ξ U)))
+   (convert Δ Γ t_motive (Δ-motive-type Δ D U))
+
+   (where (t_m ...) (Δ-method-types Δ D e_motive))
+   (type-check Δ Γ e_m t_m) ...
   ----------------- "DTR-Elim_D"
-   (type-infer Δ Γ (elim D 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)])
--- a/cur-lib/cur/curnel/redex-lang.rkt
+++ b/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,10 +30,10 @@
    [dep-provide provide]
    [dep-require require]

-    [dep-lambda lambda]
+    [dep-lambda λ]
    [dep-app #%app]

-    [dep-forall forall]
+    [dep-forall Π]

    [dep-inductive data]

@ -60,10 +60,10 @@
   (all-from-out racket/syntax)
    cur->datum
    cur-expand
-    type-infer/syn
-    type-check/syn?
-    normalize/syn
-    step/syn
+    cur-type-infer
+    cur-type-check?
+    cur-normalize
+    cur-step
    cur-equal?))

 (begin-for-syntax
@ -177,10 +177,11 @@
                    [e (parameterize ([gamma (extend-Γ/term gamma x t)])
                         (cur->datum #'e))])
               (term (,(syntax->datum #'b) (,x : ,t) ,e)))]
-            [(elim t1 t2)
-             (let* ([t1 (cur->datum #'t1)]
-                    [t2 (cur->datum #'t2)])
-               (term (elim ,t1 ,t2)))]
+            [(elim D motive (i ...) (m ...) d)
+             (term (elim ,(cur->datum #'D) ,(cur->datum #'motive)
+                         ,(map cur->datum (syntax->list #'(i ...)))
+                         ,(map cur->datum (syntax->list #'(m ...)))
+                         ,(cur->datum #'d)))]
            [(#%app e1 e2)
             (term (,(cur->datum #'e1) ,(cur->datum #'e2)))]))))
    (unless (or (inner-expand?) (type-infer/term reified-term))
@ -224,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
@ -410,8 +411,9 @@
 ;;
 ;; TODO: Can these be simplified further?
 (define-syntax (dep-lambda syn)
-  (syntax-case syn (:)
-    [(_ (x : t) e)
+  (syntax-parse syn
+    #:datum-literals (:)
+    [(_ (x:id : t) e)
     (syntax->curnel-syntax
       (quasisyntax/loc syn (λ (x : t) e)))]))

@ -422,30 +424,32 @@
       (quasisyntax/loc syn (#%app e1 e2)))]))

 (define-syntax (dep-forall syn)
-  (syntax-case syn (:)
-    [(_ (x : t) e)
+  (syntax-parse syn
+    #:datum-literals (:)
+    [(_ (x:id : t) e)
     (syntax->curnel-syntax
       (quasisyntax/loc syn (Π (x : t) e)))]))

 (define-syntax (Type syn)
-  (syntax-case syn ()
-    [(_ i)
+  (syntax-parse syn
+    [(_ i:nat)
     (syntax->curnel-syntax
       (quasisyntax/loc syn (Unv i)))]
    [_ (quasisyntax/loc syn (Type 0))]))

 (define-syntax (dep-inductive syn)
-  (syntax-case syn (:)
-    [(_ i : ti (x1 : t1) ...)
+  (syntax-parse syn
+    #:datum-literals (:)
+    [(_ i:id : ti (x1:id : t1) ...)
     (begin
       (extend-Δ/syn! delta #'i #'ti #'((x1 : t1) ...))
       #'(void))]))

 (define-syntax (dep-elim syn)
-  (syntax-case syn ()
-    [(_ D T)
+  (syntax-parse syn
+    [(_ D:id motive (i ...) (m ...) e)
     (syntax->curnel-syntax
-       (quasisyntax/loc syn (elim D T)))]))
+       (quasisyntax/loc syn (elim D motive (i ...) (m ...) e)))]))

 (define-syntax-rule (dep-void) (void))

--- a/cur-lib/cur/lang/reader.rkt
+++ b/cur-lib/cur/lang/reader.rkt
@ -1,2 +1,2 @@
 #lang s-exp syntax/module-reader
-cur/cur
+cur
--- a/cur-lib/cur/main.rkt
+++ b/cur-lib/cur/main.rkt
--- a/cur-lib/cur/olly.rkt
+++ b/cur-lib/cur/olly.rkt
@ -1,11 +1,16 @@
-#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"
  ;; TODO: "real-"? More like "curnel-"
-  (only-in "cur.rkt" [#%app real-app] [elim real-elim] [forall real-forall] [lambda real-lambda]))
+  (only-in
+   "main.rkt"
+   [#%app real-app]
+   [elim real-elim]
+   [Π real-forall]
+   [λ real-lambda]))

 (provide
  define-relation
@ -27,7 +32,7 @@
    (coq-defns (format "~a~a~n" (coq-defns) str)))

  (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))]
@ -90,8 +95,18 @@
                                     (cur->coq #'t))]))))
               "")]
            [(Type i) "Type"]
-            [(real-elim var t)
-             (format "~a_rect" (cur->coq #'var))]
+            [(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)))])))
--- a/cur-lib/cur/stdlib/bool.rkt
+++ b/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)

--- a/cur-lib/cur/stdlib/list.rkt
+++ b/cur-lib/cur/stdlib/list.rkt
@ -1,4 +1,4 @@
-#lang s-exp "../cur.rkt"
+#lang s-exp "../main.rkt"
 (require
 "nat.rkt"
 "maybe.rkt"
--- a/cur-lib/cur/stdlib/maybe.rkt
+++ b/cur-lib/cur/stdlib/maybe.rkt
@ -1,4 +1,4 @@
-#lang s-exp "../cur.rkt"
+#lang s-exp "../main.rkt"
 (require "sugar.rkt")
 (provide Maybe none some some/i)

@ -9,5 +9,5 @@
 (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))]))
--- a/cur-lib/cur/stdlib/nat.rkt
+++ b/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.
--- a/cur-lib/cur/stdlib/prop.rkt
+++ b/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
@ -31,8 +31,8 @@
 (define-syntax (conj/i syn)
  (syntax-case syn ()
    [(_ a b)
-     (let ([a-type (type-infer/syn #'a)]
-           [b-type (type-infer/syn #'b)])
+     (let ([a-type (cur-type-infer #'a)]
+           [b-type (cur-type-infer #'b)])
       #`(conj #,a-type #,b-type a b))]))

 (define thm:and-is-symmetric
@ -71,11 +71,12 @@
 (define proof:A-or-A
  (lambda (A : Type) (c : (Or A A))
    ;; TODO: What should the motive be?
-    (elim Or Type (lambda (A : Type) (B : Type) (c : (Or A B)) A)
-      (lambda (A : Type) (B : Type) (a : A) a)
-      ;; TODO: How do we know B is A?
-      (lambda (A : Type) (B : Type) (b : B) b)
-      A A c)))
+    (elim Or (lambda (A : Type) (B : Type) (c : (Or A B)) A)
+          (A A)
+          ((lambda (A : Type) (B : Type) (a : A) a)
+           ;; TODO: How do we know B is A?
+           (lambda (A : Type) (B : Type) (b : B) b))
+          c)))

 (qed thm:A-or-A proof:A-or-A)
 |#
--- a/cur-lib/cur/stdlib/sugar.rkt
+++ b/cur-lib/cur/stdlib/sugar.rkt
@ -1,4 +1,4 @@
-#lang s-exp "../cur.rkt"
+#lang s-exp "../main.rkt"
 (provide
  ->
  lambda
@ -6,10 +6,12 @@
    [-> →]
    [-> forall]
    [-> ∀]
+    [-> Π]
+    [-> Pi]
    [lambda λ])
  #%app
  define
-  elim
+  :
  define-type
  match
  recur
@ -25,10 +27,10 @@
  query-type)

 (require
-  (only-in "../cur.rkt"
-    [elim real-elim]
+  (only-in "../main.rkt"
    [#%app real-app]
-    [lambda real-lambda]
+    [λ real-lambda]
+    [Π real-Π]
    [define real-define]))

 (begin-for-syntax
@ -51,7 +53,7 @@
    [(_ d:parameter-declaration ...+ result:result-type)
     (foldr (lambda (src name type r)
              (quasisyntax/loc src
-                (forall (#,name : #,type) #,r)))
+                (real-Π (#,name : #,type) #,r)))
            #'result
            (attribute d)
            (attribute d.name)
@ -97,13 +99,61 @@
 (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)
     (quasisyntax/loc syn
       (real-define name (lambda (x : t) ... body)))]
@ -111,8 +161,67 @@
     (quasisyntax/loc syn
       (real-define id body))]))

-(define-syntax-rule (elim t1 t2 e ...)
-  ((real-elim t1 t2) e ...))
+#|
+(begin-for-syntax
+  (define (type->telescope syn)
+    (syntax-parse (cur-expand syn)
+      #:literals (real-Π)
+      #:datum-literals (:)
+      [(real-Π (x:id : t) body)
+       (cons #'(x : t) (type->telescope #'body))]
+      [_ '()]))
+
+  (define (type->body syn)
+    (syntax-parse syn
+      #:literals (real-Π)
+      #:datum-literals (:)
+      [(real-Π (x:id : t) body)
+       (type->body #'body)]
+      [e #'e]))
+
+  (define (constructor-indices D syn)
+    (let loop ([syn syn]
+               [args '()])
+      (syntax-parse (cur-expand syn)
+        #:literals (real-app)
+        [D:id args]
+        [(real-app e1 e2)
+         (loop #'e1 (cons #'e2 args))])))
+
+  (define (inductive-index-telescope D)
+    (type->telescope (cur-type-infer D)))
+
+  (define (inductive-method-telescope D motive)
+    (for/list ([syn (cur-constructor-map D)])
+      (with-syntax ([(c : t) syn]
+                    [name (gensym (format-symbol "~a-~a" #'c 'method))]
+                    [((arg : arg-type) ...) (type->telescope #'t)]
+                    [((rarg : rarg-type) ...) (constructor-recursive-args D #'((arg : arg-type) ...))]
+                    [((ih : ih-type) ...) (constructor-inductive-hypotheses #'((rarg : rarg-type) ...) motive)]
+                    [(iarg ...) (constructor-indices D (type->body #'t))]
+                    )
+        #`(name : (forall (arg : arg-type) ...
+                          (ih : ih-type) ...
+                          (motive iarg ...)))))))
+
+(define-syntax (elim syn)
+  (syntax-parse syn
+    [(elim D:id U e ...)
+     (with-syntax ([((x : t) ...) (inductive-index-telescope #'D)]
+                   [motive (gensym 'motive)]
+                   [y (gensym 'y)]
+                   [disc (gensym 'disc)]
+                   [((method : method-type) ...) (inductive-method-telescope #'D #'motive)])
+       #`((lambda
+            (motive : (forall (x : t) ... (y : (D x ...)) U))
+            (method : ) ...
+            (x : t) ...
+            (disc : (D x ...)) ...
+            (real-elim D motive (x ...) (method ...) disc))
+          e ...)
+       )
+     ]))
+|#

 ;; Quite fragie to give a syntactic treatment of pattern matching -> eliminator. Replace with "Elimination with a Motive"
 (begin-for-syntax
@ -159,7 +268,7 @@
     #:attr types
     ;; TODO: Detect failure, report error/suggestions
     (for/list ([e (attribute indices)])
-       (or (type-infer/syn e)
+       (or (cur-type-infer e)
           (raise-syntax-error
            'match
            (format
@ -180,7 +289,7 @@
     (lambda (return)
       ;; NB: unhygenic
       ;; Normalize at compile-time, for efficiency at run-time
-       (normalize/syn
+       (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
@ -241,7 +350,7 @@
       (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 (normalize/syn #`(#,motive #,@(attribute type.indices) #,name-syn))])
+             [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)))))))

@ -253,7 +362,7 @@
     (or maybe-return-type
         ;; Ignore errors when trying to infer this type; other attempt might succeed
         (with-handlers ([values (lambda _ #f)])
-           (type-infer/syn #:local-env (attribute p.local-env) #'b)))))
+           (cur-type-infer #:local-env (attribute p.local-env) #'b)))))

  (define-syntax-class (match-clause D motive)
    (pattern
@ -289,7 +398,7 @@
        (~optional
         (~seq #:in ~! t)
         #:defaults
-         ([t (or (type-infer/syn #'d)
+         ([t (or (cur-type-infer #'d)
                 (raise-syntax-error
                  'match
                  "Could not infer discrimnant's type. Try using #:in to declare it."
@ -314,15 +423,9 @@
     (quasisyntax/loc syn
       (elim
        D.inductive-name
-        #,(or
-           (type-infer/syn (attribute return-type))
-           (raise-syntax-error
-            'match
-            "Could not infer type of motive. Sorry, you'll have to use elim."
-            syn))
        motive
-        c.method ...
-        #,@(attribute D.indices)
+        #,(attribute D.indices)
+        (c.method ...)
        d))]))

 (begin-for-syntax
@ -334,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
@ -352,29 +455,29 @@
    [(let (c:let-clause ...) body)
     #'((lambda (c.id : c.type) ... body) c.e ...)]))

-;; Normally type checking will only happen if a term is actually used. This forces a term to be
-;; checked against a particular type.
+;; Normally type checking will only happen if a term is actually used/appears at top-level.
+;; This forces a term to be checked against a particular type.
 (define-syntax (:: syn)
  (syntax-case syn ()
    [(_ pf t)
     (begin
       ;; TODO: Code duplication in let-clause pattern
-       (unless (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)]))

@ -390,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))]))
--- a/cur-lib/cur/stdlib/tactics/base.rkt
+++ b/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)))

--- a/cur-lib/cur/stdlib/tactics/sartactics.rkt
+++ b/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")
--- a/cur-lib/cur/stdlib/tactics/standard.rkt
+++ b/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)")]))

--- a/cur-lib/cur/stdlib/typeclass.rkt
+++ b/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 (... ...))]))))]))

@ -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))
--- a/cur-lib/info.rkt
+++ b/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))
--- a/cur-test/cur/tests/olly.rkt
+++ b/cur-test/cur/tests/olly.rkt
@ -41,11 +41,12 @@
     "\\| T-Bla : \\(forall g : gamma, \\(forall e : term, \\(forall t : type, \\(\\(\\(meow g\\) e\\) t\\)\\)\\)\\)\\."
     (second (string-split t "\n"))))
  (let ([t (cur->coq
-            #'(elim nat Type (lambda (x : nat) nat) z
-                    (lambda (x : nat) (ih-x : nat) ih-x)
+            #'(elim nat (lambda (x : nat) nat)
+                    ()
+                    (z (lambda (x : nat) (ih-x : nat) ih-x))
                    e))])
    (check-regexp-match
-     "\\(\\(\\(\\(nat_rect \\(fun x : nat => nat\\)\\) z\\) \\(fun x : nat => \\(fun ih_x : nat => ih_x\\)\\)\\) e\\)"
+     "\\(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"
--- a/cur-test/cur/tests/plus.rkt
+++ b/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))
--- a/cur-test/cur/tests/redex-core.rkt
+++ b/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
-                         ((hole (s zero)) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+ (term (Δ-inductive-elim ,Δ nat
+                         (elim nat (λ (x : nat) nat) ()
+                               ((s zero) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+                               hole)
                         (hole zero)))
- (term (hole (((((elim nat Type) (λ (x : nat) nat))
-                (s zero))
-               (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
-              zero))))
+ (term (hole (elim nat (λ (x : nat) nat)
+                   ()
+                   ((s zero)
+                    (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+                   zero))))
 (check-telescope-equiv?
- (term (Δ-inductive-elim ,Δ nat Type (λ (x : nat) nat) hole
-                         ((hole (s zero)) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+ (term (Δ-inductive-elim ,Δ nat
+                         (elim nat (λ (x : nat) nat) ()
+                               ((s zero) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+                               hole)
                         (hole (s zero))))
- (term (hole (((((elim nat Type) (λ (x : nat) nat))
-                (s zero))
-               (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
-              (s zero)))))
+ (term (hole (elim nat (λ (x : nat) nat) ()
+                   ((s zero) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+                   (s zero)))))
+(check-telescope-equiv?
+ (term (Δ-inductive-elim ,Δ nat
+                         (elim nat (λ (x : nat) nat) ()
+                               ((s zero) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+                               hole)
+                         hole))
+ (term hole))

 ;; Tests for dynamic semantics
 ;; ------------------------------------------------------------------------
@ -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))
-                                 (λ (x : nat) (λ (ih-x : nat)
-                                                (s (s x)))))
-                                zero)))
+
+(check-equal? (term (Δ-constructor-index ,Δ nat zero)) 0)
+(check-equiv? (term (reduce ,Δ (elim nat (λ (x : nat) nat)
+                                     ()
+                                     ((s zero)
+                                      (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+                                     zero)))
              (term (s zero)))
-(check-equiv? (term (reduce ,Δ (((((elim nat Type) (λ (x : nat) nat))
-                                  (s zero))
-                                 (λ (x : nat) (λ (ih-x : nat)
-                                                (s (s x)))))
-                                (s zero))))
+(check-equiv? (term (reduce ,Δ (elim nat (λ (x : nat) nat)
+                                     ()
+                                     ((s zero)
+                                      (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+                                     (s zero))))
              (term (s (s zero))))
-(check-equiv? (term (reduce ,Δ (((((elim nat Type) (λ (x : nat) nat))
-                                  (s zero))
-                                 (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+(check-equiv? (term (reduce ,Δ (elim nat (λ (x : nat) nat)
+                                     ()
+                                     ((s zero)
+                                      (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
                                (s (s (s zero))))))
              (term (s (s (s (s zero))))))

 (check-equiv?
 (term (reduce ,Δ
-               (((((elim nat Type) (λ (x : nat) nat))
-                  (s (s zero)))
-                 (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
-                (s (s zero)))))
+               (elim nat (λ (x : nat) nat)
+                     ()
+                     ((s (s zero))
+                      (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
+                     (s (s zero)))))
 (term (s (s (s (s zero))))))
 (check-equiv?
 (term (step ,Δ
-             (((((elim nat Type) (λ (x : nat) nat))
-                (s (s zero)))
-               (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
-              (s (s zero)))))
+             (elim nat (λ (x : nat) nat)
+                     ()
+                     ((s (s zero))
+                      (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
+                     (s (s zero)))))
 (term
  (((λ (x : nat) (λ (ih-x : nat) (s ih-x)))
    (s zero))
-   (((((elim nat Type) (λ (x : nat) nat))
-      (s (s zero)))
-     (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
-    (s zero)))))
+   (elim nat (λ (x : nat) nat)
+         ()
+         ((s (s zero))
+          (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
+         (s zero)))))
 (check-equiv?
 (term (step ,Δ (step ,Δ
                      (((λ (x : nat) (λ (ih-x : nat) (s ih-x)))
                        (s zero))
-                       (((((elim nat Type) (λ (x : nat) nat))
-                          (s (s zero)))
-                         (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
-                        (s zero))))))
+                       (elim nat (λ (x : nat) nat)
+                             ()
+                             ((s (s zero))
+                              (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
+                             (s zero))))))
 (term
  ((λ (ih-x1 : nat) (s ih-x1))
   (((λ (x : nat) (λ (ih-x : nat) (s ih-x)))
     zero)
-    (((((elim nat Type) (λ (x : nat) nat))
-       (s (s zero)))
-      (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
-     zero)))))
+    (elim nat (λ (x : nat) nat)
+          ()
+          ((s (s zero))
+           (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
+          zero)))))

 (define-syntax-rule (check-equivalent e1 e2)
-  (check-holds (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?
- (term (Δ-methods-telescope ,Δtruth truth (λ (x : truth) (Unv 1))))
- (term (Π (m-T : ((λ (x : truth) (Unv 1)) T)) hole)))
-(check-holds (type-infer ,Δtruth ∅ (elim truth Type) t))
-(check-holds (type-check (∅ (truth : (Unv 0) ((T : truth))))
+(check-equiv?
+ (term (Δ-motive-type ,Δtruth truth (Unv 2)))
+ (term (Π (x : truth) (Unv 2))))
+
+
+(check-holds (type-check ,Δtruth ∅ (Unv 0) ,(car (term (Δ-method-types ,Δtruth truth (λ (x : truth) (Unv 1)))))))
+
+(check-holds (type-check ,Δtruth ∅ (λ (x : truth) (Unv 1)) (Π (x : truth) (Unv 2))))
+
+(check-equiv?
+ (term (apply (λ (x : truth) (Unv 1)) T))
+ (term ((λ (x : truth) (Unv 1)) T)))
+
+(check-holds
+ (convert ,Δtruth ∅ (apply (λ (x : truth) (Unv 1)) T) (Unv 1)))
+
+(check-holds (type-infer ,Δtruth
                         ∅
-                         ((((elim truth (Unv 2)) (λ (x : truth) (Unv 1))) (Unv 0))
-                          T)
+                         (elim truth (λ (x : truth) (Unv 1))
+                               () ((Unv 0)) T)
+                         t))
+
+(check-holds (type-check ,Δtruth
+                         ∅
+                         (elim truth (λ (x : truth) (Unv 1))
+                               () ((Unv 0)) T)
                         (Unv 1)))
 (check-not-holds (type-check (∅ (truth : (Unv 0) ((T : truth))))
                             ∅
-                             ((((elim truth (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)
-              (λ (x : nat) (λ (ih-x : nat) x))) zero)
+(nat-test ∅ (elim nat (λ (x : nat) nat) ()
+                  (zero (λ (x : nat) (λ (ih-x : nat) x)))
+                  zero)
            nat)
 (nat-test ∅ nat (Unv 0))
 (nat-test ∅ zero nat)
 (nat-test ∅ s (Π (x : nat) nat))
 (nat-test ∅ (s zero) nat)
-;; TODO: Meta-function auto-currying and such
 (check-holds
- (type-infer ,Δ ∅ ((((elim nat (Unv 0)) (λ (x : nat) nat))
-                    zero)
-                   (λ (x : nat) (λ (ih-x : nat) x)))
+ (type-infer ,Δ ∅ (λ (x : nat)
+                    (elim nat (λ (x : nat) nat)
+                          ()
+                          (zero
+                           (λ (x : nat) (λ (ih-x : nat) x)))
+                          x))
             t))
-(nat-test ∅ (((((elim nat (Unv 0)) (λ (x : nat) nat))
-               zero)
-              (λ (x : nat) (λ (ih-x : nat) x)))
-             zero)
+(nat-test ∅ (elim nat (λ (x : nat) nat)
+                  ()
+                  (zero (λ (x : nat) (λ (ih-x : nat) x)))
+                  zero)
            nat)
-(nat-test ∅ (((((elim nat (Unv 0)) (λ (x : nat) nat))
-               (s zero))
-              (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
-             zero)
+(nat-test ∅ (elim nat (λ (x : nat) nat)
+                  ()
+                  ((s zero) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+                  zero)
            nat)
-(nat-test ∅ (((((elim nat Type) (λ (x : nat) nat))
-               (s zero))
-              (λ (x : nat) (λ (ih-x : nat) (s (s x))))) zero)
+(nat-test ∅ (elim nat (λ (x : nat) nat)
+                  ()
+                  ((s zero) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+                  zero)
            nat)
 (nat-test (∅ n : nat)
-          (((((elim nat (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))
-                btrue)
-               (λ (x : nat) (λ (ih-x : bool) bfalse)))
-              n2)
+             (elim nat (λ (x : nat) bool)
+                   ()
+                   (btrue (λ (x : nat) (λ (ih-x : bool) bfalse)))
+                   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))
-                  (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B))
-                                                true))))
-                 (λ (A : (Unv 0))
-                   (λ (B : (Unv 0))
-                     (λ (a : A)
-                       (λ (b : B) tt)))))
-                true) true)
-              ((((conj true) true) tt) tt))
+             (elim and
+                   (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B))
+                                                 true)))
+                   (true true)
+                   ((λ (A : (Unv 0))
+                      (λ (B : (Unv 0))
+                        (λ (a : A)
+                          (λ (b : B) tt)))))
+                   ((((conj true) true) tt) tt))
             true))
 (check-true (Γ? (term (((∅ P : (Unv 0)) Q : (Unv 0)) ab : ((and P) Q)))))
 (check-holds
@ -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))
-                  (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B))
-                                                ((and B) A)))))
-                 (λ (A : (Unv 0))
-                   (λ (B : (Unv 0))
-                     (λ (a : A)
-                       (λ (b : B) ((((conj B) A) b) a))))))
-                P) Q) ab)
+             (elim and
+                   (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B))
+                                                 ((and B) A))))
+                   (P Q)
+                   ((λ (A : (Unv 0))
+                      (λ (B : (Unv 0))
+                        (λ (a : A)
+                          (λ (b : B) ((((conj B) A) b) a))))))
+                   ab)
             ((and Q) P)))
 (check-holds
 (type-check (,Δ4 (true : (Unv 0) ((tt : true)))) ∅
@ -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)))))
-                 (λ (A : (Unv 0))
+                                                ((and B) A))))
+                 (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))
-          true)
-         (λ (x : nat) (λ (x_ih : bool) false)))))
+  (term (λ (n : nat)
+          (elim nat (λ (x : nat) bool) ()
+              (true (λ (x : nat) (λ (x_ih : bool) false)))
+              n))))
 (check-holds
 (type-check ,Δ ∅ ,zero? (Π (x : nat) bool)))
 (check-equal?
@ -592,9 +584,12 @@
 (term (reduce ,Δ (,zero? (s zero))))
 (term false))
 (define ih-equal?
-  (term ((((elim nat Type) (λ (x : nat) bool))
-          false)
-         (λ (x : nat) (λ (y : bool) (x_ih x))))))
+  (term (λ (ih : nat)
+          (elim nat (λ (x : nat) bool)
+              ()
+              (false
+               (λ (x : nat) (λ (y : bool) (x_ih x))))
+              ih))))
 (check-holds
 (type-check ,Δ (∅ x_ih : (Π (x : nat) bool))
             ,ih-equal?
@ -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)))
-          ,zero?)
-         (λ (x : nat) (λ (x_ih : (Π (x : nat) bool))
-                        ,ih-equal?)))))
+  (term (λ (n : nat)
+          (elim nat (λ (x : nat) (Π (x : nat) bool))
+              ()
+              (,zero?
+              (λ (x : nat) (λ (x_ih : (Π (x : nat) bool))
+                             ,ih-equal?)))
+              n))))
 (check-holds
 (type-check ,Δ (∅ nat-equal? : (Π (x-D«4158» : nat) ((λ (x«4159» : nat) (Π (x«4160» : nat) bool)) x-D«4158»)))
             ((nat-equal? zero) zero)
@ -631,19 +629,12 @@
 (check-true (Δ? Δ=))

 (define refl-elim
-  (term (((((((elim == (Unv 0)) (λ (A1 : (Unv 0)) (λ (x1 : A1) (λ (y1 : A1) (λ (p2 : (((==
-                                                                                        A1)
-                                                                                       x1)
-                                                                                      y1))
-                                                                              nat)))))
-             (λ (A1 : (Unv 0)) (λ (x1 : A1) zero))) bool) true) true) ((refl bool) true))))
+  (term (elim == (λ (A1 : (Unv 0)) (λ (x1 : A1) (λ (y1 : A1) (λ (p2 : (((== A1) x1) y1)) nat))))
+                  (bool true true)
+                  ((λ (A1 : (Unv 0)) (λ (x1 : A1) zero)))
+                  ((refl bool) true))))
 (check-holds
 (type-check ,Δ= ∅ ,refl-elim nat))
-(check-true
- (redex-match?
-  tt-redL
-  (Δ (in-hole E (in-hole Θ ((elim x_D U) e_P))))
-  (term (,Δ= ,refl-elim))))
 (check-true
 (redex-match?
  tt-redL
--- a/cur-test/cur/tests/stdlib/list.rkt
+++ b/cur-test/cur/tests/stdlib/list.rkt
@ -32,11 +32,11 @@
 (:: (lambda (A : Type) (n : Nat) (none A)) (forall (A : Type) (-> Nat (Maybe A)))))
 (check-equal?
 (void)
- (:: (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
+ (:: (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))

--- a/cur-test/cur/tests/stdlib/prop.rkt
+++ b/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)
-       (λ (A : Type) (x : A) z)
-       Bool
-       true
-       true
+ (elim == (λ (A : Type) (x : A) (y : A) (p : (== A x y)) Nat)
+       (Bool
+        true
+        true)
+       ((λ (A : Type) (x : A) z))
       (refl Bool true))
 z)

--- a/cur-test/cur/tests/stdlib/typeclass.rkt
+++ b/cur-test/cur/tests/stdlib/typeclass.rkt
@ -11,9 +11,7 @@
           (equal? : (forall (a : A) (b : A) Bool)))
 (impl (Eqv Bool)
      (define (equal? (a : Bool) (b : Bool))
-        (if a
-            (if b true false)
-            (if b false true))))
+        (if a b (not b))))
 (impl (Eqv Nat)
      (define equal? nat-equal?))
 (check-equal?
--- a/cur-test/cur/tests/sweet-exp.rkt
+++ b/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)
--- a/cur-test/info.rkt
+++ b/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))
Author	SHA1	Message	Date
William J. Bowman	832b7be5db	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.	2016-03-24 16:03:51 -04:00
William J. Bowman	185cc71c62	Bumped version Should have done this earlier when APIs changed; but I didn't.	2016-03-22 18:22:36 -04:00
William J. Bowman	8cb4bc3f96	Added pre-definition type ascription	2016-03-22 13:33:51 -04:00
William J. Bowman	e334376433	Syntax parse in redex-lang forms For better errors and more robust extensions	2016-03-22 13:16:30 -04:00
William J. Bowman	59e241ecb2	Simplify parts of Curnel implementation	2016-03-18 16:39:32 -04:00
William J. Bowman	db7471c9d6	Fixed typo in README	2016-03-17 17:02:10 -04:00
William J. Bowman	e0e23a60a1	Fixed typo in README	2016-03-17 17:01:40 -04:00
William J. Bowman	b8ca2ad9dc	Added support for sweet-expressions * Moved cur.rkt to main.rkt, which fixes some reader issues * Added sweet-expression tests * Added notes about sweet-expressions to README * Added sweet-exp as dependency to tests	2016-03-17 16:59:54 -04:00
William J. Bowman	4f272dc507	NB XXX: Renamed reflection API functions The names of reflection API functions were previously confusing. They included weird patterns that only made sense inside the Cur implementation. As they are Racket functions, they ought to somehow indicate that these functions are for Cur, which they did not.	2016-03-17 16:03:53 -04:00
William J. Bowman	8b3159bb6f	Reorganized stdlib docs a bit Sugar should come first; tactics last	2016-03-17 15:38:17 -04:00
William J. Bowman	ab6d62252f	Making the core language more like Curnel Previously, the core language of Cur, i.e. the default object language, was stupidly providing syntax sugar. E.g., both λ and lambda as syntax for functions. Now, the default object language is much closer to the Curnel, and this syntax sugar is moved to the sugar library.	2016-03-17 15:33:19 -04:00