Updated documentation

Advanced match now works in all stdlib. case and case* deprecated.

README.md

@@ -45,10 +45,6 @@ Try it out: open up DrRacket and put the following in the definition area:
 (if true
     false
     true)
-
-(: + (-> Nat Nat Nat))
-(define + plus)
-(+ z (s z))
 ```
 
 Try entering the following in the interaction area:
@@ -56,23 +52,6 @@ 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

@@ -33,44 +33,43 @@ restricted impredicative universe.
           Type]
 }
 
-@defform[(λ (id : type-expr) body-expr)]{
+@defform*[((lambda (id : type-expr) body-expr)
-Produces a single-arity procedure, binding the identifier @racket[id] of type
+           (λ (id : type-expr) body-expr))]{
-@racket[type-expr] in @racket[body-expr] and in the type of @racket[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
-Both @racket[type-expr] and @racket[body-expr] can contain non-curnel forms,
+@racket[body-expr].
-such as macros.
+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
+Currently, Cur will return the underlying representation of a procedure when a @racket[lambda] is
-@racket[λ] is evaluated at the top-level.
+evaluated at the top-level. Do not rely on this representation.
-Do not rely on this representation.
 
 @examples[#:eval curnel-eval
-          (λ (x : Type) x)]
+          (lambda (x : Type) x)]
 
 @examples[#:eval curnel-eval
-          (λ (x : Type) (λ (y : x) y))]
+          (λ (x : Type) (lambda (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
-          ((λ (x : (Type 1)) x) Type)]
+          ((lambda (x : (Type 1)) x) Type)]
 
 @examples[#:eval curnel-eval
-          (#%app (λ (x : (Type 1)) x) Type)]
+          (#%app (lambda (x : (Type 1)) x) Type)]
 }
 
-@defform[(Π (id : type-expr) body-expr)]{
+@defform*[((forall (id : type-expr) body-expr)
-Produces a dependent function type, binding the identifier @racket[id] of type
+           (∀ (id : type-expr) body-expr))]{
-@racket[type-expr] in @racket[body-expr].
+Produces a dependent function type, binding the identifier @racket[id] of type @racket[type-expr] in @racket[body-expr].
 
 
 @examples[#:eval curnel-eval
-          (Π (x : Type) Type)]
+          (forall (x : Type) Type)]
 
 @examples[#:eval curnel-eval
-          (λ (x : (Π (x : (Type 1)) Type))
+          (lambda (x : (forall (x : (Type 1)) Type))
             (x Type))]
 }
 
@@ -84,34 +83,31 @@ For instance, Cur does not currently perform strict positivity checking.
           (data Bool : Type
                 (true : Bool)
                 (false : Bool))
-          ((λ (x : Bool) x) true)
+          ((lambda (x : Bool) x) true)
           (data False : Type)
-          (data And : (Π (A : Type) (Π (B : Type) Type))
+          (data And : (forall (A : Type) (forall (B : Type) Type))
-            (conj : (Π (A : Type) (Π (B : Type) (Π (a : A) (Π (b : B) ((And A) B)))))))
+            (conj : (forall (A : Type) (forall (B : Type) (forall (a : A) (forall (b : B) ((And A) B)))))))
           ((((conj Bool) Bool) true) false)]
 }
 
-@defform[(elim inductive-type motive (index ...) (method ...) disc)]{
+@defform[(elim type motive-universe)]{
-Fold over the term @racket[disc] of the inductively defined type @racket[inductive-type].
+Returns the inductive eliminator for @racket[type] where the @racket[motive-universe] is the universe
-The @racket[motive] is a function that expects the indices of the inductive
+of the motive.
-type and a term of the inductive type and produces the type that this
+The eliminator expects the next argument to be the motive, the next @racket[N] arguments to be the methods for
-fold returns.
+each of the @racket[N] constructors of the inductive type @racket[type], the next @racket[P] arguments
-The type of @racket[disc] is @racket[(inductive-type index ...)].
+to be the parameters @racket[p_0 ... p_P] of the inductive @racket[type], and the final argument to be the term to
-@racket[elim] takes one method for each constructor of @racket[inductive-type].
+eliminate of type @racket[(type p_0 ... p_P)].
-Each @racket[method] expects the arguments for its corresponding constructor,
-and the inductive hypotheses generated by recursively eliminating all recursive
-arguments of the constructor.
 
 The following example runs @racket[(sub1 (s z))].
 
 @examples[#:eval curnel-eval
           (data Nat : Type
             (z : Nat)
-            (s : (Π (n : Nat) Nat)))
+            (s : (forall (n : Nat) Nat)))
-          (elim Nat (λ (x : Nat) Nat)
+          (((((elim Nat Type)
-                ()
+              (lambda (x : Nat) Nat))
-                (z
+             z)
-                 (λ (n : Nat) (λ (IH : Nat) n)))
+            (lambda (n : Nat) (lambda (IH : Nat) n)))
            (s z))]
 }
 
@@ -121,13 +117,11 @@ Binds @racket[id] to the result of @racket[expr].
 @examples[#:eval curnel-eval
           (data Nat : Type
             (z : Nat)
-            (s : (Π (n : Nat) Nat)))
+            (s : (forall (n : Nat) Nat)))
-          (define sub1 (λ (n : Nat)
+          (define sub1 (lambda (n : Nat)
-                         (elim Nat (λ (x : Nat) Nat)
+                         (((((elim Nat Type) (lambda (x : Nat) Nat))
-                               ()
+                           z)
-                               (z
+                          (lambda (n : Nat) (lambda (IH : Nat) n))) n)))
-                                (λ (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-metavar ...) maybe-bnfdef non-terminal-def ...) ...)
+           (nt-name (nt-metavars) maybe-bnfdef constructors ...) ...)
          #:grammar
          [(maybe-vars
             (code:line)
-            (code:line #:vars (nt-metavar ...)))
+            (code:line #:vars (nt-metavars ...)))
          (maybe-output-coq
             (code:line)
             (code:line #:output-coq coq-filename))
@@ -27,51 +27,26 @@ the language.
             (code:line #:output-latex latex-filename))
          (maybe-bnfdef
             (code:line)
-            (code:line ::=))
+            (code:line ::=))]]{
-	 (non-terminal-def
-	    nt-metavar
-            (code:line terminal)
-            (code:line (terminal terminal-args ...)))
-	 (terminal-args
-	    nt-metavar
-	    (code:line literal)
-	    (code:line ())
-	    (code:line (#:bind nt-metavar . terminal-args))
-	    (code:line (terminal-args terminal-args ...)))]]{
 Defines a new language by generating inductive definitions for each
-non-terminal @racket[nt-name], whose syntax is generated by
+nonterminal @racket[nt-name], whose constructors are generated by
-@racket[non-terminal-def].
+@racket[constructors]. The constructors must either with a tag that can
-Each @racket[non-terminal-def] must either be a reference to a
+be used to name the constructor, or be another meta-variable.
-previously defined non-terminal using a @racket[nt-metavar], a
+The meta-variables @racket[nt-metavars] are replaced by the corresponding
-@racket[terminal] (an identifier), or a @racket[terminal] applied to
+inductive types in @racket[constructors].
-some @racket[terminal-args].
+The name of each inductive datatype is generated by
-The @racket[terminal-args] are a limited grammar of s-expressions,
+@racket[(format-id "~a-~a" name nt-name)].
-which can reference previously defined @racket[nt-metavar]s to be
-treated as arguments, literal symbols to be treated as syntax, binding
-declarations, or a nested @racket[terminal-arg].
 
-The inductive definitions are generated by generating a type for each
+Later nonterminals can refer to prior nonterminals, but they cannot be
-@racket[nt-name] whose name @racket[nt-type] is generated by
+mutually inductive due to limitations in Cur. When nonterminals appear
-@racket[(format-id name "~a-~a" name nt-name)] and whose constructors
+in @racket[constructors], a constructor is defined that coerces one
-are generated by each @racket[non-terminal-def].
+nonterminal to another.
-For @racket[terminal]s, the constructor is a base constructor whose
-name is generated by @racket[(format-id name "~a-~a" name terminal)].
-For @racket[nt-metavar]s, the constructor is a conversion constructor
-whose name is generated by @racket[(format-id name "~a->~a" nt-type
-nt-metavar-type)] where @racket[nt-metavar-type] is the name of the
-type generated for the nonterminal to which @racket[nt-metavars] refers.
-For @racket[(terminal terminal-args ...)], the constructor is a
-function that expects term of of the types generated by
-@racket[terminal-args ...].
 
 If @racket[#:vars] is given, it should be a list of meta-variables that
-representing variables in the language.
+representing variables in the language. These meta-variables should only
-These variables are represented as De Bruijn indices, and uses of
+appear in binding positions in @racket[constructors]. These variables
-variables in the syntax are treated as type @racket[Nat].
+are represented as De Bruijn indexes, and Olly provides some functions
-Binding positions in the syntax, represented by @racket[#:bind
+for working with De Bruijn indexes.
-nt-metavar], are erased in converting to De Bruijn indices, although
-this may change if the representation of variables used by
-@racket[define-language] changes.
 
 If @racket[#:output-coq] is given, it should be a string representing a
 filename. The form @racket[define-language] will output Coq versions of
@@ -91,8 +66,8 @@ Example:
   #:output-latex "stlc.tex"
   (val  (v)   ::= true false unit)
   (type (A B) ::= boolty unitty (-> A B) (* A A))
-  (term (e)   ::= x v (app e e) (lambda (#:bind x : A) e) (cons e e)
+  (term (e)   ::= x v (app e e) (lambda (x : A) e) (cons e e)
-                  (let (#:bind x #:bind x) = e in e)))
+                  (let (x x) = e in e)))
 ]
 
 This example is equivalent to
@@ -110,17 +85,20 @@ This example is equivalent to
   (stlc-* : (forall (x : stlc-type) (forall (y : stlc-type) stlc-type))))
 
 (data stlc-term : Type
-  (Var->-stlc-term : (forall (x : Nat) stlc-term))
+  (stlc-var-->-stlc-term : (forall (x : Var) stlc-term))
-  (stlc-val->-stlc-term : (forall (x : stlc-val) stlc-term))
+  (stlc-val-->-stlc-term : (forall (x : stlc-val) stlc-term))
-  (stlc-term-lambda : (forall (y : stlc-type)
+  (stlc-term-lambda : (forall (x : Var)
+                        (forall (y : stlc-type)
                           (forall (z : stlc-term)
-                            stlc-term)))
+                            stlc-term))))
   (stlc-term-cons : (forall (x : stlc-term) (forall (y : stlc-term) stlc-term)))
-  (stlc-term-let : (forall (e1 : stlc-term)
+  (stlc-term-let : (forall (x : Var)
+                     (forall (y : Var)
+                       (forall (e1 : stlc-term)
                          (forall (e2 : stlc-term)
-                       stlc-term))))]
+                           stlc-term))))))]
 
-@margin-note{This example is taken from @racketmodname[cur/tests/stlc]}
+@margin-note{This example is taken from @racketmodname[cur/examples/stlc]}
 }
 
 @defform[(define-relation (name args ...)
@@ -148,20 +126,20 @@ explain the syntax in detail, here is an example:
   #:output-latex "stlc.tex"
   [(g : Gamma)
    ------------------------ T-Unit
-   (has-type g (stlc-val->stlc-term stlc-unit) stlc-unitty)]
+   (has-type g (stlc-val-->-stlc-term stlc-unit) stlc-unitty)]
 
   [(g : Gamma)
    ------------------------ T-True
-   (has-type g (stlc-val->stlc-term stlc-true) stlc-boolty)]
+   (has-type g (stlc-val-->-stlc-term stlc-true) stlc-boolty)]
 
   [(g : Gamma)
    ------------------------ T-False
-   (has-type g (stlc-val->stlc-term stlc-false) stlc-boolty)]
+   (has-type g (stlc-val-->-stlc-term stlc-false) stlc-boolty)]
 
-  [(g : Gamma) (x : Nat) (t : stlc-type)
+  [(g : Gamma) (x : Var) (t : stlc-type)
    (== (Maybe stlc-type) (lookup-gamma g x) (some stlc-type t))
    ------------------------ T-Var
-   (has-type g (Var->stlc-term x) t)]
+   (has-type g (Var-->-stlc-term x) t)]
 
   [(g : Gamma) (e1 : stlc-term) (e2 : stlc-term)
                (t1 : stlc-type) (t2 : stlc-type)
@@ -173,15 +151,16 @@ explain the syntax in detail, here is an example:
   [(g : Gamma) (e1 : stlc-term) (e2 : stlc-term)
                (t1 : stlc-type) (t2 : stlc-type)
                (t : stlc-type)
+               (x : Var) (y : Var)
    (has-type g e1 (stlc-* t1 t2))
-   (has-type (extend-gamma (extend-gamma g t1) t2) e2 t)
+   (has-type (extend-gamma (extend-gamma g x t1) y t2) e2 t)
    ---------------------- T-Let
-   (has-type g (stlc-let e1 e2) t)]
+   (has-type g (stlc-let x y e1 e2) t)]
 
-  [(g : Gamma) (e1 : stlc-term) (t1 : stlc-type) (t2 : stlc-type)
+  [(g : Gamma) (e1 : stlc-term) (t1 : stlc-type) (t2 : stlc-type) (x : Var)
-   (has-type (extend-gamma g t1) e1 t2)
+   (has-type (extend-gamma g x t1) e1 t2)
    ---------------------- T-Fun
-   (has-type g (stlc-lambda t1 e1) (stlc--> t1 t2))]
+   (has-type g (stlc-lambda x t1 e1) (stlc--> t1 t2))]
 
   [(g : Gamma) (e1 : stlc-term) (e2 : stlc-term)
                (t1 : stlc-type) (t2 : stlc-type)
@@ -200,11 +179,22 @@ This example is equivalent to:
   (T-Unit : (forall (g : Gamma)
               (has-type
                 g
-                (stlc-val->stlc-term stlc-unit)
+                (stlc-val-->-stlc-term stlc-unit)
                 stlc-unitty)))
   ....)]
 }
 
+@deftogether[(@defthing[Var Type]
+              @defthing[avar (forall (x : Nat) Var)])]{
+The type of a De Bruijn variable.
+}
+
+@defproc[(var-equal? [v1 Var] [v2 Var])
+         Bool]{
+A Cur procedure; returns @racket[true] if @racket[v1] and @racket[v2]
+represent the same variable.
+}
+
 @todo{Need a Scribble library for defining Cur/Racket things in the same
 library in a nice way.}
 

cur-doc/cur/scribblings/reflection.scrbl

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

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}

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 (λ (x : Bool) Bool) () (false true) true)]
+	  (elim Bool Type (λ (x : Bool) Bool) false true true)]
 }
 
 @defproc[(not [x Bool])

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

@@ -21,24 +21,22 @@ 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)
+          (data And : (-> Type Type)
             (conj : (-> (A : Type) (B : Type) A B ((And A) B))))
           ((((conj Bool) Bool) true) false)]
+}
 
 @examples[#:eval curnel-eval
           (data And : (forall Type Type Type)
-            (conj : (forall (A : Type) (B : Type) A B (And A B))))
+            (conj : (forall (A : Type) (B : Type) A B ((And A) B))))
           ((((conj Bool) Bool) true) false)]
 
 }
@@ -62,24 +60,21 @@ Defines multi-arity procedure application via automatic currying.
           (conj Bool Bool true false)]
 }
 
-@defform[(: name type)]{
-Declare that the @emph{function} which will be defined as @racket[name] has type @racket[type].
-Must precede the definition of @racket[name].
-@racket[type] must expand to a function type of the form @racket[(Π (x : t1) t2)]
-When used, this form allows omitting the annotations on arguments in the definition @racket[name]
-}
-
 @defform*[((define name body)
-           (define (name x ...) body)
            (define (name (x : t) ...) body))]{
 Like the @racket[define] provided by @racketmodname[cur], but supports
 defining curried functions via @racket[lambda].
-The second form, @racket[(define (name x ...) body)], can only be used when
+}
-a @racket[(: name type)] form appears earlier in the module.
+
+@defform[(elim type motive-result-type e ...)]{
+Like the @racket[elim] provided by @racketmodname[cur], but supports
+automatically curries the remaining arguments @racket[e ...].
 
 @examples[#:eval curnel-eval
-          (: id (forall (A : Type) (a : A) A))
+          (elim Bool Type (lambda (x : Bool) Bool)
-	  (define (id A a) a)]
+            false
+            true
+            true)]
 }
 
 @defform*[((define-type name type)
@@ -125,6 +120,7 @@ If @racket[#:return] is not specified, attempts to infer the return type of the
 
 @examples[#:eval curnel-eval
           ((match (nil Bool)
+	    #:in (List Bool)
             [(nil (A : Type))
 	     (lambda (n : Nat)
 	       (none A))]
@@ -172,7 +168,7 @@ Check that expression @racket[e] has type @racket[type], causing a type-error if
 }
 
 @defform[(run syn)]{
-Like @racket[cur-normalize], but is a syntactic form to be used in surface syntax.
+Like @racket[normalize/syn], 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.
 
@@ -182,7 +178,7 @@ another Cur term.
 }
 
 @defform[(step syn)]{
-Like @racket[run], but uses @racket[cur-step] to evaluate only one step and prints intermediate
+Like @racket[run], but uses @racket[step/syn] to evaluate only one step and prints intermediate
 results before returning the result of evaluation.
 
 @examples[#:eval curnel-eval

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.4") "sandbox-lib"))
+(define build-deps '("scribble-lib" ("cur-lib" #:version "0.2") "sandbox-lib"))
 (define pkg-desc "Documentation for \"cur\".")
 (define pkg-authors '(wilbowma))

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

@@ -26,11 +26,11 @@
 (define-language ttL
   (i j k  ::= natural)
   (U ::= (Unv i))
-  (D x c ::= variable-not-otherwise-mentioned)
+  (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) ...))))
-  (t e ::= U (λ (x : t) e) x (Π (x : t) t) (e e)
+  (D x c ::= variable-not-otherwise-mentioned)
-     ;; (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,8 +44,6 @@
 ;;; ------------------------------------------------------------------------
 ;;; Universe typing
 
-;; Universe types
-;; aka Axioms A of a PTS
 (define-judgment-form ttL
   #:mode (unv-type I O)
   #:contract (unv-type U U)
@@ -55,7 +53,6 @@
    (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)
@@ -108,6 +105,27 @@
   [(Δ-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
@@ -127,6 +145,14 @@
 ;; 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
@@ -163,31 +189,47 @@
 ;; TODO: Test
 #| TODO:
  | This essentially eta-expands t at the type-level. Why is this necessary? Shouldn't it be true
- | that (convert t (Ξ-apply Ξ t))?
+ | that (equivalent t (Ξ-apply Ξ t))?
- | Maybe not. t is a lambda whose type is convert to (Ξ-apply Ξ t)? Yes.
+ | Maybe not. t is a lambda whose type is equivalent 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
@@ -209,6 +251,15 @@
   [(Δ-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 -> Ξ
@@ -226,6 +277,21 @@
    (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
@@ -254,6 +320,36 @@
       (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.
 ;;
@@ -269,40 +365,29 @@
 ;; Ξ_P*D is the telescope of the parameters of x_D and
 ;;       the witness of type x_D (applied to the parameters)
 ;; Ξ_m   is the telescope of the methods for x_D
-
-;; Returns the inductive hypotheses required for the elimination method of constructor c_i for
-;; inductive type D, when eliminating with motive t_P.
 (define-metafunction tt-ctxtL
-  Δ-constructor-inductive-hypotheses : Δ D c t -> Ξ
+  Δ-elim-type : Δ x U -> t
-  [(Δ-constructor-inductive-hypotheses Δ D c_i t_P)
+  [(Δ-elim-type Δ x_D U)
-   (hypotheses-loop D t_P (Δ-constructor-inductive-telescope Δ D c_i))])
+   (Π (x_P : (in-hole Ξ_P*D U))
-
+      ;; The methods Ξ_m for each constructor of type x_D
-;; Returns the type of the method corresponding to c_i
+      (in-hole Ξ_m
-(define-metafunction tt-ctxtL
+        ;; And finally, the parameters and discriminant
-  Δ-constructor-method-type : Δ D c t -> t
+        (in-hole Ξ_P*D
-  [(Δ-constructor-method-type Δ D c_i t_P)
+          ;; The result is (P a ... (x_D a ...)), i.e., the motive
-   (in-hole Ξ_a (in-hole Ξ_h ((in-hole Θ_p t_P) (Ξ-apply Ξ_a c_i))))
+          ;; applied to the paramters and discriminant
-   (where Θ_p (Δ-constructor-parameters Δ D c_i))
+          (Ξ-apply Ξ_P*D x_P))))
-   (where Ξ_a (Δ-constructor-telescope Δ D c_i))
+   ;; Get the parameters of x_D
-   (where Ξ_h (Δ-constructor-inductive-hypotheses Δ D c_i t_P))])
+   (where Ξ (Δ-ref-parameter-Ξ Δ x_D))
-
-(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))
+   (where x ,(variable-not-in (term (Δ Γ x_D Ξ)) 'x-D))
    ;; The telescope (∀ a -> ... -> (D a ...) hole), i.e.,
-   ;; of the indices and the inductive type applied to the
+   ;; of the parameters and the inductive type applied to the
-   ;; indices
+   ;; parameters
-   (where Ξ_P*D (in-hole Ξ (Π (x : (Ξ-apply Ξ D)) hole)))])
+   (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))])
 
 ;;; ------------------------------------------------------------------------
 ;;; Dynamic semantics
@@ -310,21 +395,16 @@
 ;;; inductively defined type x with a motive whose result is in universe U
 
 (define-extended-language tt-redL tt-ctxtL
-  (v  ::= x U (Π (x : t) t) (λ (x : t) t) (in-hole Θv c))
+  ;; 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))
-  (C-elim  ::= (elim D t_P (e_i ...) (e_m ...) hole))
+  ;; call-by-value, plus reduce under Π (helps with typing checking)
-  ;; call-by-value
+  (E   ::= hole (E e) (v E) (Π (x : v) E) (Π (x : E) e)))
-  (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 ...))
@@ -340,6 +420,75 @@
  |
  | 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
@@ -353,34 +502,39 @@
 ;; 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
+(define-metafunction tt-ctxtL
-  Δ-inductive-elim : Δ D C-elim Θ -> Θ
+  Δ-inductive-elim : Δ x U t Θ Θ Θ -> Θ
   ;; 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)
+  [(Δ-inductive-elim Δ x_D U t_P Θ_p Θ_m (Θ_i t_i))
-   hole]
+   ((Δ-inductive-elim Δ x_D U t_P Θ_p Θ_m Θ_i)
-  [(Δ-inductive-elim Δ D C-elim (Θ_c t_i))
+    (in-hole ((in-hole Θ_p Θ_m) t_i) ((elim x_D U) t_P)))
-   ((Δ-inductive-elim Δ D C-elim Θ_c)
+   (side-condition (term (is-inductive-argument Δ x_D t_i)))]
-    (in-hole C-elim t_i))
+  [(Δ-inductive-elim Δ x_D U t_P Θ_p Θ_m (Θ_i t_i))
-   (side-condition (term (is-inductive-argument Δ D t_i)))]
+   (Δ-inductive-elim Δ x_D U t_P Θ_p Θ_m Θ_i)]
-  [(Δ-inductive-elim any ... (Θ_c t_i))
+  [(Δ-inductive-elim Δ x_D U t_P Θ_p Θ_m hole)
-   (Δ-inductive-elim any ... Θ_c)])
+   hole])
 
 (define tt-->
   (reduction-relation tt-redL
     (--> (Δ (in-hole E ((λ (x : t_0) t_1) t_2)))
          (Δ (in-hole E (subst t_1 x t_2)))
          -->β)
-    (--> (Δ (in-hole E (elim D e_motive (e_i ...) (v_m ...) (in-hole Θv_c c))))
+    (--> (Δ (in-hole E (in-hole Θv ((elim D U) v_P))))
-         (Δ (in-hole E (in-hole Θ_mi v_mi)))
+         (Δ (in-hole E (in-hole Θ_r (in-hole Θv_i v_mi))))
-         ;; Find the method for constructor c_i, relying on the order of the arguments.
+         ;; Check that Θv is valid to avoid capturing other things
-         (where natural (Δ-constructor-index Δ D c))
+         (side-condition (term (Θ-valid Δ D Θv)))
-         (where v_mi ,(list-ref (term (v_m ...)) (term natural)))
+          ;; 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)))
          ;; Generate the inductive recursion
-         (where Θ_ih (Δ-inductive-elim Δ D (elim D e_motive (e_i ...) (v_m ...) hole) Θv_c))
+         (where Θ_r (Δ-inductive-elim Δ D U v_P Θv_p Θv_m Θv_i))
-         (where Θ_mi (in-hole Θ_ih Θv_c))
          -->elim)))
 
 (define-metafunction tt-redL
@@ -396,6 +550,16 @@
    (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
 
@@ -405,24 +569,6 @@
   (Γ   ::= ∅ (Γ 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 Γ ∅) Γ]
@@ -541,22 +687,16 @@
    ----------------- "DTR-Application"
    (type-infer Δ Γ (e_0 e_1) t_3)]
 
-  [(type-check Δ Γ e_c (apply D e_i ...))
+  [(where t (Δ-elim-type Δ D U))
-
+   (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 e_motive (e_i ...) (e_m ...) e_c)
+   (type-infer Δ Γ (elim D U) t)])
-               (apply e_motive e_i ... e_c))])
 
 (define-judgment-form tt-typingL
   #:mode (type-check I I I I)
   #:contract (type-check Δ Γ e t)
 
   [(type-infer Δ Γ e t_0)
-   (convert Δ Γ t t_0)
+   (equivalent Δ 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
-  (except-in "redex-core.rkt" apply)
+  "redex-core.rkt"
   redex/reduction-semantics
   racket/provide-syntax
   (for-syntax
@@ -11,7 +11,7 @@
     racket/syntax
     (except-in racket/provide-transform export)
     racket/require-transform
-    (except-in "redex-core.rkt" apply)
+    "redex-core.rkt"
     redex/reduction-semantics))
 (provide
   ;; Basic syntax
@@ -30,10 +30,10 @@
     [dep-provide provide]
     [dep-require require]
 
-    [dep-lambda λ]
+    [dep-lambda lambda]
     [dep-app #%app]
 
-    [dep-forall Π]
+    [dep-forall forall]
 
     [dep-inductive data]
 
@@ -60,10 +60,10 @@
    (all-from-out racket/syntax)
     cur->datum
     cur-expand
-    cur-type-infer
+    type-infer/syn
-    cur-type-check?
+    type-check/syn?
-    cur-normalize
+    normalize/syn
-    cur-step
+    step/syn
     cur-equal?))
 
 (begin-for-syntax
@@ -177,11 +177,10 @@
                     [e (parameterize ([gamma (extend-Γ/term gamma x t)])
                          (cur->datum #'e))])
                (term (,(syntax->datum #'b) (,x : ,t) ,e)))]
-            [(elim D motive (i ...) (m ...) d)
+            [(elim t1 t2)
-             (term (elim ,(cur->datum #'D) ,(cur->datum #'motive)
+             (let* ([t1 (cur->datum #'t1)]
-                         ,(map cur->datum (syntax->list #'(i ...)))
+                    [t2 (cur->datum #'t2)])
-                         ,(map cur->datum (syntax->list #'(m ...)))
+               (term (elim ,t1 ,t2)))]
-                         ,(cur->datum #'d)))]
             [(#%app e1 e2)
              (term (,(cur->datum #'e1) ,(cur->datum #'e2)))]))))
     (unless (or (inner-expand?) (type-infer/term reified-term))
@@ -225,29 +224,29 @@
 
   ;; Reflection tools
 
-  (define (cur-normalize syn)
+  (define (normalize/syn syn)
     (datum->cur
       syn
       (eval-cur syn)))
 
-  (define (cur-step syn)
+  (define (step/syn syn)
     (datum->cur
       syn
       (term (step ,(delta) ,(subst-bindings (cur->datum syn))))))
 
   ;; Are these two terms equivalent in type-systems internal equational reasoning?
   (define (cur-equal? e1 e2)
-    (and (judgment-holds (convert ,(delta) ,(gamma) ,(eval-cur e1) ,(eval-cur e2))) #t))
+    (and (judgment-holds (equivalent ,(delta) ,(eval-cur e1) ,(eval-cur e2))) #t))
 
   ;; TODO: Document local-env
-  (define (cur-type-infer syn #:local-env [env '()])
+  (define (type-infer/syn syn #:local-env [env '()])
     (parameterize ([gamma (for/fold ([gamma (gamma)])
                                     ([(x t) (in-dict env)])
                             (extend-Γ/syn (thunk gamma) x t))])
       (let ([t (type-infer/term (eval-cur syn))])
         (and t (datum->cur syn t)))))
 
-  (define (cur-type-check? syn type)
+  (define (type-check/syn? 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
@@ -411,9 +410,8 @@
 ;;
 ;; TODO: Can these be simplified further?
 (define-syntax (dep-lambda syn)
-  (syntax-parse syn
+  (syntax-case syn (:)
-    #:datum-literals (:)
+    [(_ (x : t) e)
-    [(_ (x:id : t) e)
      (syntax->curnel-syntax
        (quasisyntax/loc syn (λ (x : t) e)))]))
 
@@ -424,32 +422,30 @@
        (quasisyntax/loc syn (#%app e1 e2)))]))
 
 (define-syntax (dep-forall syn)
-  (syntax-parse syn
+  (syntax-case syn (:)
-    #:datum-literals (:)
+    [(_ (x : t) e)
-    [(_ (x:id : t) e)
      (syntax->curnel-syntax
        (quasisyntax/loc syn (Π (x : t) e)))]))
 
 (define-syntax (Type syn)
-  (syntax-parse syn
+  (syntax-case syn ()
-    [(_ i:nat)
+    [(_ i)
      (syntax->curnel-syntax
        (quasisyntax/loc syn (Unv i)))]
     [_ (quasisyntax/loc syn (Type 0))]))
 
 (define-syntax (dep-inductive syn)
-  (syntax-parse syn
+  (syntax-case syn (:)
-    #:datum-literals (:)
+    [(_ i : ti (x1 : t1) ...)
-    [(_ i:id : ti (x1:id : t1) ...)
      (begin
        (extend-Δ/syn! delta #'i #'ti #'((x1 : t1) ...))
        #'(void))]))
 
 (define-syntax (dep-elim syn)
-  (syntax-parse syn
+  (syntax-case syn ()
-    [(_ D:id motive (i ...) (m ...) e)
+    [(_ D T)
      (syntax->curnel-syntax
-       (quasisyntax/loc syn (elim D motive (i ...) (m ...) e)))]))
+       (quasisyntax/loc syn (elim D T)))]))
 
 (define-syntax-rule (dep-void) (void))
 

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,54 +1,245 @@
-#lang s-exp "main.rkt"
+#lang s-exp "cur.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
+  (only-in "cur.rkt" [#%app real-app] [elim real-elim] [forall real-forall] [lambda real-lambda]))
-   "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
-   typeset-relation
+   coq-defns
-   typeset-bnf
+   output-latex-bnf
-   cur->coq))
+   output-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 : (-> 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 (cur-type-infer syn)
+    (syntax-parse (type-infer/syn syn)
       #:datum-literals (Π :)
       [(Π (x:id : t) body)
        (cons #'x (constructor-args #'body))]
       [_ null]))
-
   (define (sanitize-id str)
     (let ([replace-by `((: _) (- _))])
       (for/fold ([str str])
                 ([p replace-by])
         (string-replace str (symbol->string (first p))
                         (symbol->string (second p))))))
-
+  (define (output-coq syn)
-  (define (cur->coq syn)
-    (parameterize ([coq-defns ""])
-      (define output
-        (let cur->coq ([syn syn])
     (syntax-parse (cur-expand syn #'define #'begin)
        ;; TODO: Need to add these to a literal set and export it
        ;; Or, maybe overwrite syntax-parse
@@ -56,394 +247,68 @@
        [(begin e ...)
         (for/fold ([str ""])
                   ([e (syntax->list #'(e ...))])
-               (format "~a~n" (cur->coq e)))]
+          (format "~a~n" (output-coq e)))]
        [(define name:id body)
         (begin
           (coq-lift-top-level
             (format "Definition ~a := ~a.~n"
-                        (cur->coq #'name)
+                    (output-coq #'name)
-                        (cur->coq #'body)))
+                    (output-coq #'body)))
           "")]
        [(define (name:id (x:id : t) ...) body)
         (begin
           (coq-lift-top-level
             (format "Function ~a ~a := ~a.~n"
-                        (cur->coq #'name)
+                    (output-coq #'name)
                     (for/fold ([str ""])
                               ([n (syntax->list #'(x ...))]
                                [t (syntax->list #'(t ...))])
-                          (format "~a(~a : ~a) " str (cur->coq n) (cur->coq t)))
+                      (format "~a(~a : ~a) " str (output-coq n) (output-coq t)))
-                        (cur->coq #'body)))
+                    (output-coq #'body)))
           "")]
        [(real-lambda ~! (x:id (~datum :) t) body:expr)
-             (format "(fun ~a : ~a => ~a)" (cur->coq #'x) (cur->coq #'t)
+        (format "(fun ~a : ~a => ~a)" (output-coq #'x) (output-coq #'t)
-                     (cur->coq #'body))]
+                (output-coq #'body))]
        [(real-forall ~! (x:id (~datum :) t) body:expr)
-             (format "(forall ~a : ~a, ~a)" (syntax-e #'x) (cur->coq #'t)
+        (format "(forall ~a : ~a, ~a)" (syntax-e #'x) (output-coq #'t)
-                     (cur->coq #'body))]
+                (output-coq #'body))]
        [(data ~! n:id (~datum :) t (x*:id (~datum :) t*) ...)
         (begin
           (coq-lift-top-level
             (format "Inductive ~a : ~a :=~a."
                    (sanitize-id (format "~a" (syntax-e #'n)))
-                        (cur->coq #'t)
+                   (output-coq #'t)
                    (for/fold ([strs ""])
                              ([clause (syntax->list #'((x* : t*) ...))])
                      (syntax-parse clause
                        [(x (~datum :) t)
                         (format "~a~n| ~a : ~a" strs (syntax-e #'x)
-                                     (cur->coq #'t))]))))
+                          (output-coq #'t))]))))
           "")]
        [(Type i) "Type"]
-            [(real-elim var:id motive (i ...) (m ...) d)
+       [(real-elim var t)
-             (format
+        (format "~a_rect" (output-coq #'var))]
-              "(~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))]
+        (format "(~a ~a)" (output-coq #'e1) (output-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))
+        (~optional (~seq #:exists flag)) body:expr)
-        body:expr)
+     (parameterize ([current-output-port (if (attribute file)
-     (parameterize ([current-output-port
+                                             (open-output-file (syntax->datum #'file)
-                     (if (attribute file)
-                         (open-output-file
-                          (syntax->datum #'file)
                                                                #:exists
                                                                (if (attribute flag)
                                                                    ;; TODO: AHH WHAT?
                                                                    (eval (syntax->datum #'flag))
                                                                    'error))
-                         (current-output-port))])
+                                             (current-output-port))]
-       (displayln (cur->coq #'body))
+                    [coq-defns ""])
+       (define output
+         (let ([body (output-coq #'body)])
+           (if (regexp-match "^\\s*$" body)
+               ""
+               (format "Eval compute in ~a." body))))
+       (displayln (format "~a~a" (coq-defns) output))
        #'(begin))]))
-
-;; 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 "../main.rkt"
+#lang s-exp "../cur.rkt"
 (require "sugar.rkt")
 (provide Bool true false if not and or)
 

cur-lib/cur/stdlib/list.rkt

@@ -1,4 +1,4 @@
-#lang s-exp "../main.rkt"
+#lang s-exp "../cur.rkt"
 (require
  "nat.rkt"
  "maybe.rkt"
@@ -8,8 +8,7 @@
  List
  nil
  cons
- list-ref
+ list-ref)
- length)
 
 (data List : (-> (A : Type) Type)
   (nil : (-> (A : Type) (List A)))
@@ -23,11 +22,16 @@
        (match n
          [z (some A a)]
          [(s (n-1 : Nat))
-          ((recur rest) n-1)]))]))
+          ((recur rest) n-1)]))])
-
+  #;(elim
-(define (length (A : Type) (ls : (List A)))
+   List
-  (match ls
+   Type
-    [(nil (A : Type))
+   (lambda (A : Type) (ls : (List A))
-     z]
+            (-> Nat (Maybe A)))
-    [(cons (A : Type) (a : A) (rest : (List A)))
+   (lambda (A : Type) (n : Nat) (none A))
-     (s (recur rest))]))
+   (lambda (A : Type) (a : A) (ls : (List A)) (ih : (-> Nat (Maybe A)))
+           (lambda (n : Nat)
+             (match n
+               [z (some A a)]
+               [(s (n-1 : Nat))
+                (ih n-1)])))))

cur-lib/cur/stdlib/maybe.rkt

@@ -1,4 +1,4 @@
-#lang s-exp "../main.rkt"
+#lang s-exp "../cur.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 (cur-type-infer #'a)])
+    (let ([a-ty (type-infer/syn #'a)])
       #`(some #,a-ty a))]))

cur-lib/cur/stdlib/nat.rkt

@@ -1,4 +1,4 @@
-#lang s-exp "../main.rkt"
+#lang s-exp "../cur.rkt"
 (require "sugar.rkt" "bool.rkt")
 ;; TODO: override (all-defined-out) to enable exporting all these
 ;; properly.

cur-lib/cur/stdlib/prop.rkt

@@ -1,4 +1,4 @@
-#lang s-exp "../main.rkt"
+#lang s-exp "../cur.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 (cur-type-infer #'a)]
+     (let ([a-type (type-infer/syn #'a)]
-           [b-type (cur-type-infer #'b)])
+           [b-type (type-infer/syn #'b)])
        #`(conj #,a-type #,b-type a b))]))
 
 (define thm:and-is-symmetric
@@ -71,12 +71,11 @@
 (define proof:A-or-A
   (lambda (A : Type) (c : (Or A A))
     ;; TODO: What should the motive be?
-    (elim Or (lambda (A : Type) (B : Type) (c : (Or A B)) A)
+    (elim Or Type (lambda (A : Type) (B : Type) (c : (Or A B)) A)
-          (A A)
+      (lambda (A : Type) (B : Type) (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))
+      (lambda (A : Type) (B : Type) (b : B) b)
-          c)))
+      A A c)))
 
 (qed thm:A-or-A proof:A-or-A)
 |#

cur-lib/cur/stdlib/sugar.rkt

@@ -1,4 +1,4 @@
-#lang s-exp "../main.rkt"
+#lang s-exp "../cur.rkt"
 (provide
   ->
   lambda
@@ -6,12 +6,10 @@
     [-> →]
     [-> forall]
     [-> ∀]
-    [-> Π]
-    [-> Pi]
     [lambda λ])
   #%app
   define
-  :
+  elim
   define-type
   match
   recur
@@ -27,10 +25,12 @@
   query-type)
 
 (require
-  (only-in "../main.rkt"
+  (only-in "../cur.rkt"
+    [elim real-elim]
     [#%app real-app]
-    [λ real-lambda]
+    ;; Somehow, using real-lambda instead of _lambda causes weird import error
-    [Π real-Π]
+    [lambda real-lambda]
+    #;[forall real-forall]
     [define real-define]))
 
 (begin-for-syntax
@@ -53,7 +53,7 @@
     [(_ d:parameter-declaration ...+ result:result-type)
      (foldr (lambda (src name type r)
               (quasisyntax/loc src
-                (real-Π (#,name : #,type) #,r)))
+                (forall (#,name : #,type) #,r)))
             #'result
             (attribute d)
             (attribute d.name)
@@ -95,65 +95,21 @@
     [(_ e1 e2 e3 ...)
      (quasisyntax/loc syn
        (#%app (#%app e1 e2) e3 ...))]))
+(module+ test
+  ((lambda (A : (Type 1)) (B : (Type 1)) A)
+   Type
+   Type))
 
 (define-syntax define-type
   (syntax-rules ()
     [(_ (name (a : t) ...) body)
-     (define name (-> (a : t) ... body))]
+     (define name (forall (a : t) ... body))]
     [(_ name type)
      (define name type)]))
 
-;; Cooperates with define to allow Haskell-esque type annotations
-#| TODO NB:
- | This method of cooperating macros is sort of a terrible
- | hack. Instead, need principled way of adding/retrieving information
- | to/from current module. E.g. perhaps provide extensions an interface to
- | module's term environment and inductive signature. Then, :: could add
- | new "id : type" to environment, and define could extract type and use.
- |#
-(begin-for-syntax
-  (define annotation-dict (make-hash))
-  (define (annotation->types type-syn)
-    (let loop ([ls '()]
-               [syn type-syn])
-      (syntax-parse (cur-expand syn)
-        #:datum-literals (:)
-        [(real-Π (x:id : type) body)
-         (loop (cons #'type ls) #'body)]
-        [_ (reverse ls)]))))
-
-(define-syntax (: syn)
-  (syntax-parse syn
-    [(_ name:id type:expr)
-     ;; NB: Unhygenic; need to reuse Racket's identifiers, and make this type annotation a syntax property
-     (syntax-parse (cur-expand #'type)
-      #:datum-literals (:)
-      [(real-Π (x:id : type) body) (void)]
-      [_
-       (raise-syntax-error
-        ':
-        "Can only declare annotations for functions, but not a function type"
-        syn)])
-     (dict-set! annotation-dict (syntax->datum #'name) (annotation->types #'type))
-     #'(void)]))
-
 ;; TODO: Allow inferring types as in above TODOs for lambda, forall
 (define-syntax (define syn)
-  (syntax-parse syn
+  (syntax-case 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)))]
@@ -161,67 +117,8 @@
      (quasisyntax/loc syn
        (real-define id body))]))
 
-#|
+(define-syntax-rule (elim t1 t2 e ...)
-(begin-for-syntax
+  ((real-elim t1 t2) e ...))
-  (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
@@ -268,7 +165,7 @@
      #:attr types
      ;; TODO: Detect failure, report error/suggestions
      (for/list ([e (attribute indices)])
-       (or (cur-type-infer e)
+       (or (type-infer/syn e)
            (raise-syntax-error
             'match
             (format
@@ -289,7 +186,7 @@
      (lambda (return)
        ;; NB: unhygenic
        ;; Normalize at compile-time, for efficiency at run-time
-       (cur-normalize
+       (normalize/syn
         #`((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
@@ -350,7 +247,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 (cur-normalize #`(#,motive #,@(attribute type.indices) #,name-syn))])
+             [ih-type (normalize/syn #`(#,motive #,@(attribute type.indices) #,name-syn))])
          (dict-set! ih-dict (syntax->datum name-syn) ih-name)
          (append decls (list #`(#,ih-name : #,ih-type)))))))
 
@@ -362,7 +259,7 @@
      (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)))))
+           (type-infer/syn #:local-env (attribute p.local-env) #'b)))))
 
   (define-syntax-class (match-clause D motive)
     (pattern
@@ -398,7 +295,7 @@
         (~optional
          (~seq #:in ~! t)
          #:defaults
-         ([t (or (cur-type-infer #'d)
+         ([t (or (type-infer/syn #'d)
                  (raise-syntax-error
                   'match
                   "Could not infer discrimnant's type. Try using #:in to declare it."
@@ -423,9 +320,15 @@
      (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
-        #,(attribute D.indices)
+        c.method ...
-        (c.method ...)
+        #,@(attribute D.indices)
         d))]))
 
 (begin-for-syntax
@@ -437,14 +340,14 @@
       #:attr type (cond
                     [(attribute t)
                      ;; TODO: Code duplication in ::
-                     (unless (cur-type-check? #'e #'t)
+                     (unless (type-check/syn? #'e #'t)
                        (raise-syntax-error
                          'let
                          (format "Term ~a does not have expected type ~a. Inferred type was ~a"
-                                 (cur->datum #'e) (cur->datum #'t) (cur->datum (cur-type-infer #'e)))
+                                 (cur->datum #'e) (cur->datum #'t) (cur->datum (type-infer/syn #'e)))
                          #'e (quasisyntax/loc #'x (x e))))
                      #'t]
-                    [(cur-type-infer #'e)]
+                    [(type-infer/syn #'e)]
                     [else
                       (raise-syntax-error
                         'let
@@ -455,29 +358,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/appears at top-level.
+;; Normally type checking will only happen if a term is actually used. This forces a term to be
-;; This forces a term to be checked against a particular type.
+;; checked against a particular type.
 (define-syntax (:: syn)
   (syntax-case syn ()
     [(_ pf t)
      (begin
        ;; TODO: Code duplication in let-clause pattern
-       (unless (cur-type-check? #'pf #'t)
+       (unless (type-check/syn? #'pf #'t)
          (raise-syntax-error
            '::
            (format "Term ~a does not have expected type ~a. Inferred type was ~a"
-                   (cur->datum #'pf) (cur->datum #'t) (cur->datum (cur-type-infer #'pf)))
+                   (cur->datum #'pf) (cur->datum #'t) (cur->datum (type-infer/syn #'pf)))
            syn))
        #'(void))]))
 
 (define-syntax (run syn)
   (syntax-case syn ()
-    [(_ expr) (cur-normalize #'expr)]))
+    [(_ expr) (normalize/syn #'expr)]))
 
 (define-syntax (step syn)
   (syntax-case syn ()
     [(_ expr)
-     (let ([t (cur-step #'expr)])
+     (let ([t (step/syn #'expr)])
        (displayln (cur->datum t))
        t)]))
 
@@ -493,6 +396,6 @@
   (syntax-case syn ()
     [(_ term)
      (begin
-       (printf "\"~a\" has type \"~a\"~n" (syntax->datum #'term) (syntax->datum (cur-type-infer #'term)))
+       (printf "\"~a\" has type \"~a\"~n" (syntax->datum #'term) (syntax->datum (type-infer/syn #'term)))
        ;; Void is undocumented and a hack, but sort of works
        #'(void))]))

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

@@ -1,4 +1,4 @@
-#lang s-exp "../../main.rkt"
+#lang s-exp "../../cur.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 (cur-type-check? pf t)
+      (unless (type-check/syn? 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 "../../main.rkt"
+#lang s-exp "../../cur.rkt"
 (require
   "base.rkt"
   (prefix-in basic: "standard.rkt")

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

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

cur-lib/cur/stdlib/typeclass.rkt

@@ -1,4 +1,4 @@
-#lang s-exp "../main.rkt"
+#lang s-exp "../cur.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 (cur-type-infer #'arg))
+                     #`(#,(format-id syn "~a-~a" '#,name (type-infer/syn #'arg))
                         arg
                         args (... ...))]))))]))
 
@@ -57,7 +57,7 @@
      #`(begin
          #,@(for/list ([def (syntax->list #'(defs ...))])
               (let-values ([(name body) (process-def def)])
-                (unless (cur-type-check?
+                (unless (type-check/syn?
                           body
                           #`(#,(dict-ref
                                  (dict-ref typeclasses (syntax->datum #'class))

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.4")
+(define version "0.2")
 (define pkg-authors '(wilbowma))

cur-test/cur/tests/olly.rkt

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

cur-test/cur/tests/plus.rkt

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

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

@@ -81,6 +81,23 @@
    (Π (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
@@ -98,10 +115,41 @@
  (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
 ;; ------------------------------------------------------------------------
@@ -109,32 +157,21 @@
 (check-true
  (redex-match? tt-ctxtL (in-hole Θ_i (hole (in-hole Θ_r zero))) (term (hole zero))))
 (check-telescope-equiv?
- (term (Δ-inductive-elim ,Δ nat
+ (term (Δ-inductive-elim ,Δ nat Type (λ (x : nat) nat) hole
-                         (elim nat (λ (x : nat) nat) ()
+                         ((hole (s zero)) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
-                               ((s zero) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
-                               hole)
                          (hole zero)))
- (term (hole (elim nat (λ (x : nat) nat)
+ (term (hole (((((elim nat Type) (λ (x : nat) nat))
-                   ()
+                (s zero))
-                   ((s zero)
                (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
               zero))))
 (check-telescope-equiv?
- (term (Δ-inductive-elim ,Δ nat
+ (term (Δ-inductive-elim ,Δ nat Type (λ (x : nat) nat) hole
-                         (elim nat (λ (x : nat) nat) ()
+                         ((hole (s zero)) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
-                               ((s zero) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
-                               hole)
                          (hole (s zero))))
- (term (hole (elim nat (λ (x : nat) nat) ()
+ (term (hole (((((elim nat Type) (λ (x : nat) nat))
-                   ((s zero) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+                (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
 ;; ------------------------------------------------------------------------
@@ -142,8 +179,6 @@
 (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)))
@@ -153,71 +188,63 @@
                   (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))
-(check-equal? (term (Δ-constructor-index ,Δ nat zero)) 0)
+                                  (s zero))
-(check-equiv? (term (reduce ,Δ (elim nat (λ (x : nat) nat)
+                                 (λ (x : nat) (λ (ih-x : nat)
-                                     ()
+                                                (s (s x)))))
-                                     ((s zero)
-                                      (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
                                 zero)))
               (term (s zero)))
-(check-equiv? (term (reduce ,Δ (elim nat (λ (x : nat) nat)
+(check-equiv? (term (reduce ,Δ (((((elim nat Type) (λ (x : nat) nat))
-                                     ()
+                                  (s zero))
-                                     ((s zero)
+                                 (λ (x : nat) (λ (ih-x : nat)
-                                      (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+                                                (s (s x)))))
                                 (s zero))))
               (term (s (s zero))))
-(check-equiv? (term (reduce ,Δ (elim nat (λ (x : nat) nat)
+(check-equiv? (term (reduce ,Δ (((((elim nat Type) (λ (x : nat) nat))
-                                     ()
+                                  (s zero))
-                                     ((s zero)
                                  (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
                                 (s (s (s zero))))))
               (term (s (s (s (s zero))))))
 
 (check-equiv?
  (term (reduce ,Δ
-               (elim nat (λ (x : nat) nat)
+               (((((elim nat Type) (λ (x : nat) nat))
-                     ()
+                  (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 (λ (x : nat) nat)
+             (((((elim nat Type) (λ (x : nat) nat))
-                     ()
+                (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 (λ (x : nat) nat)
+   (((((elim nat Type) (λ (x : nat) nat))
-         ()
+      (s (s zero)))
-         ((s (s zero))
      (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
     (s zero)))))
 (check-equiv?
  (term (step ,Δ (step ,Δ
                       (((λ (x : nat) (λ (ih-x : nat) (s ih-x)))
                         (s zero))
-                       (elim nat (λ (x : nat) nat)
+                       (((((elim nat Type) (λ (x : nat) nat))
-                             ()
+                          (s (s zero)))
-                             ((s (s zero))
                          (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
                         (s zero))))))
  (term
   ((λ (ih-x1 : nat) (s ih-x1))
    (((λ (x : nat) (λ (ih-x : nat) (s ih-x)))
      zero)
-    (elim nat (λ (x : nat) nat)
+    (((((elim nat Type) (λ (x : nat) nat))
-          ()
+       (s (s zero)))
-          ((s (s zero))
       (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
      zero)))))
 
 (define-syntax-rule (check-equivalent e1 e2)
-  (check-holds (convert ∅ ∅ e1 e2)))
+  (check-holds (equivalent ∅ e1 e2)))
 (check-equivalent
  (λ (x : Type) x) (λ (y : Type) y))
 (check-equivalent
@@ -316,42 +343,28 @@
                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-equiv?
+(check-telescope-equiv?
- (term (Δ-motive-type ,Δtruth truth (Unv 2)))
+ (term (Δ-methods-telescope ,Δtruth truth (λ (x : truth) (Unv 1))))
- (term (Π (x : truth) (Unv 2))))
+ (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-holds (type-check ,Δtruth ∅ (Unv 0) ,(car (term (Δ-method-types ,Δtruth truth (λ (x : truth) (Unv 1)))))))
-
-(check-holds (type-check ,Δtruth ∅ (λ (x : truth) (Unv 1)) (Π (x : truth) (Unv 2))))
-
-(check-equiv?
- (term (apply (λ (x : truth) (Unv 1)) T))
- (term ((λ (x : truth) (Unv 1)) T)))
-
-(check-holds
- (convert ,Δtruth ∅ (apply (λ (x : truth) (Unv 1)) T) (Unv 1)))
-
-(check-holds (type-infer ,Δtruth
                          ∅
-                         (elim truth (λ (x : truth) (Unv 1))
+                         ((((elim truth (Unv 2)) (λ (x : truth) (Unv 1))) (Unv 0))
-                               () ((Unv 0)) T)
+                          T)
-                         t))
-
-(check-holds (type-check ,Δtruth
-                         ∅
-                         (elim truth (λ (x : truth) (Unv 1))
-                               () ((Unv 0)) T)
                          (Unv 1)))
 (check-not-holds (type-check (∅ (truth : (Unv 0) ((T : truth))))
                              ∅
-                             (elim truth Type () (Type) T)
+                             ((((elim truth (Unv 1)) Type) Type) T)
                              (Unv 1)))
 (check-holds
  (type-infer ∅ ∅ (Π (x2 : (Unv 0)) (Unv 0)) U))
@@ -369,54 +382,47 @@
   (check-holds (type-check ,Δ syn ...)))
 (nat-test ∅ (Π (x : nat) nat) (Unv 0))
 (nat-test ∅ (λ (x : nat) x) (Π (x : nat) nat))
-(nat-test ∅ (elim nat (λ (x : nat) nat) ()
+(nat-test ∅ (((((elim nat Type) (λ (x : nat) nat)) zero)
-                  (zero (λ (x : nat) (λ (ih-x : nat) x)))
+              (λ (x : nat) (λ (ih-x : nat) x))) zero)
-                  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 ,Δ ∅ (λ (x : nat)
+ (type-infer ,Δ ∅ ((((elim nat (Unv 0)) (λ (x : nat) nat))
-                    (elim nat (λ (x : nat) nat)
+                    zero)
-                          ()
-                          (zero
                    (λ (x : nat) (λ (ih-x : nat) x)))
-                          x))
              t))
-(nat-test ∅ (elim nat (λ (x : nat) nat)
+(nat-test ∅ (((((elim nat (Unv 0)) (λ (x : nat) nat))
-                  ()
+               zero)
-                  (zero (λ (x : nat) (λ (ih-x : nat) x)))
+              (λ (x : nat) (λ (ih-x : nat) x)))
              zero)
             nat)
-(nat-test ∅ (elim nat (λ (x : nat) nat)
+(nat-test ∅ (((((elim nat (Unv 0)) (λ (x : nat) nat))
-                  ()
+               (s zero))
-                  ((s zero) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+              (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
              zero)
             nat)
-(nat-test ∅ (elim nat (λ (x : nat) nat)
+(nat-test ∅ (((((elim nat Type) (λ (x : nat) nat))
-                  ()
+               (s zero))
-                  ((s zero) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+              (λ (x : nat) (λ (ih-x : nat) (s (s x))))) zero)
-                  zero)
             nat)
 (nat-test (∅ n : nat)
-          (elim nat (λ (x : nat) nat)
+          (((((elim nat (Unv 0)) (λ (x : nat) nat)) zero) (λ (x : nat) (λ (ih-x : nat) x))) n)
-                ()
-                (zero (λ (x : nat) (λ (ih-x : nat) x)))
-                n)
           nat)
 (check-holds
  (type-check (,Δ (bool : (Unv 0) ((btrue : bool) (bfalse : bool))))
              (∅ n2 : nat)
-             (elim nat (λ (x : nat) bool)
+             (((((elim nat (Unv 0)) (λ (x : nat) bool))
-                   ()
+                btrue)
-                   (btrue (λ (x : nat) (λ (ih-x : bool) bfalse)))
+               (λ (x : nat) (λ (ih-x : bool) bfalse)))
               n2)
              bool))
 (check-not-holds
  (type-check ,Δ ∅
-             (elim nat nat () ((s zero)) zero)
+             ((((elim nat (Unv 0)) nat) (s zero)) zero)
              nat))
 (define lam (term (λ (nat : (Unv 0)) nat)))
 (check-equivalent
@@ -475,14 +481,14 @@
              (in-hole Ξ (Π (x : (in-hole Θ_Ξ and)) U_P))))
 (check-holds
  (type-check (,Δ4 (true : (Unv 0) ((tt : true)))) ∅
-             (elim and
+             ((((((elim and (Unv 0))
                   (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B))
-                                                 true)))
+                                                true))))
-                   (true true)
+                 (λ (A : (Unv 0))
-                   ((λ (A : (Unv 0))
                    (λ (B : (Unv 0))
                      (λ (a : A)
                        (λ (b : B) tt)))))
+                true) true)
               ((((conj true) true) tt) tt))
              true))
 (check-true (Γ? (term (((∅ P : (Unv 0)) Q : (Unv 0)) ab : ((and P) Q)))))
@@ -501,7 +507,7 @@
                                            ((and B) A))))
              (in-hole Ξ (Π (x : (in-hole Θ and)) U))))
 (check-holds
- (convert ,Δ4 ∅
+ (equivalent ,Δ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
@@ -512,15 +518,14 @@
 (check-holds
  (type-check ,Δ4
              (((∅ P : (Unv 0)) Q : (Unv 0)) ab : ((and P) Q))
-             (elim and
+             ((((((elim and (Unv 0))
                   (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B))
-                                                 ((and B) A))))
+                                                ((and B) A)))))
-                   (P Q)
+                 (λ (A : (Unv 0))
-                   ((λ (A : (Unv 0))
                    (λ (B : (Unv 0))
                      (λ (a : A)
                        (λ (b : B) ((((conj B) A) b) a))))))
-                   ab)
+                P) Q) ab)
              ((and Q) P)))
 (check-holds
  (type-check (,Δ4 (true : (Unv 0) ((tt : true)))) ∅
@@ -533,14 +538,14 @@
              t))
 (check-holds
  (type-check (,Δ4 (true : (Unv 0) ((tt : true)))) ∅
-             (elim and
+             ((((((elim and (Unv 0))
                   (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B))
-                                                ((and B) A))))
+                                                ((and B) A)))))
-                 (true true)
+                 (λ (A : (Unv 0))
-                 ((λ (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)))
@@ -563,18 +568,21 @@
 (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 (λ (y : false) (Π (x : Type) x)) () () x)
+             (((elim false (Unv 0)) (λ (y : false) (Π (x : Type) x))) x)
              (Π (x : (Unv 0)) x)))
 
 ;; nat-equal? tests
 (define zero?
-  (term (λ (n : nat)
+  (term ((((elim nat Type) (λ (x : nat) bool))
-          (elim nat (λ (x : nat) bool) ()
+          true)
-              (true (λ (x : nat) (λ (x_ih : bool) false)))
+         (λ (x : nat) (λ (x_ih : bool) false)))))
-              n))))
 (check-holds
  (type-check ,Δ ∅ ,zero? (Π (x : nat) bool)))
 (check-equal?
@@ -584,12 +592,9 @@
  (term (reduce ,Δ (,zero? (s zero))))
  (term false))
 (define ih-equal?
-  (term (λ (ih : nat)
+  (term ((((elim nat Type) (λ (x : nat) bool))
-          (elim nat (λ (x : nat) bool)
+          false)
-              ()
+         (λ (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?
@@ -601,13 +606,10 @@
 (check-holds
  (type-infer ,Δ ∅ (λ (x : nat) (Π (x : nat) bool)) (Π (x : nat) (Unv 0))))
 (define nat-equal?
-  (term (λ (n : nat)
+  (term ((((elim nat Type) (λ (x : nat) (Π (x : nat) bool)))
-          (elim nat (λ (x : nat) (Π (x : nat) bool))
+          ,zero?)
-              ()
-              (,zero?
          (λ (x : nat) (λ (x_ih : (Π (x : nat) bool))
-                             ,ih-equal?)))
+                        ,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)
@@ -629,12 +631,19 @@
 (check-true (Δ? Δ=))
 
 (define refl-elim
-  (term (elim == (λ (A1 : (Unv 0)) (λ (x1 : A1) (λ (y1 : A1) (λ (p2 : (((== A1) x1) y1)) nat))))
+  (term (((((((elim == (Unv 0)) (λ (A1 : (Unv 0)) (λ (x1 : A1) (λ (y1 : A1) (λ (p2 : (((==
-                  (bool true true)
+                                                                                        A1)
-                  ((λ (A1 : (Unv 0)) (λ (x1 : A1) zero)))
+                                                                                       x1)
-                  ((refl bool) true))))
+                                                                                      y1))
+                                                                              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

@@ -32,11 +32,11 @@
  (:: (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)
+ (:: (elim List Type (lambda (A : Type) (ls : (List A)) Nat)
-           (Bool)
+          (lambda (A : Type) z)
-          ((lambda (A : Type) z)
           (lambda (A : Type) (a : A) (ls : (List A)) (ih : Nat)
-                   z))
+                   z)
+          Bool
           (nil Bool))
     Nat))
 

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

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

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

@@ -11,7 +11,9 @@
            (equal? : (forall (a : A) (b : A) Bool)))
 (impl (Eqv Bool)
       (define (equal? (a : Bool) (b : Bool))
-        (if a b (not b))))
+        (if a
+            (if b true false)
+            (if b false true))))
 (impl (Eqv Nat)
       (define equal? nat-equal?))
 (check-equal?

cur-test/cur/tests/stlc.rkt

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

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

cur-test/info.rkt

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