Updated documentation

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

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

@@ -12,7 +12,7 @@ This library defines the datatype @racket[List] and several functions on them.
 
 @deftogether[(@defthing[List (-> Type Type)]
               @defthing[nil (forall (A : Type) (List A))]
-	      @defthing[cons (forall* (A : Type) (a : A) (-> (List A) (List A)))])]{
+	      @defthing[cons (forall (A : Type) (a : A) (-> (List A) (List A)))])]{
 The polymorphic list datatype.
 }
 

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

@@ -4,7 +4,7 @@
   "../defs.rkt"
   scribble/eval)
 
-@(define curnel-eval (curnel-sandbox "(require cur/stdlib/nat cur/stdlib/bool cur/stdlib/sugar)"))
+@(define curnel-eval (curnel-sandbox "(require cur/stdlib/nat cur/stdlib/bool cur/stdlib/sugar cur/stdlib/list)"))
 
 
 @title{Sugar}
@@ -18,46 +18,36 @@ that expands into the eliminator.
 @defmodule[cur/stdlib/sugar]
 This library defines various syntactic extensions making Cur easier to write than writing raw TT.
 
-@defform*[((-> t1 t2)
+@defform*[((-> decl decl ... type)
-          (→ t1 t2))]{
+           (→ decl decl ... type)
-A non-dependent function type Equivalent to @racket[(forall (_ : t1) t2)], where @racket[_] indicates an variable that is not used.
+	   (forall decl decl ... type)
+	   (∀ decl decl ... type))
+	  #:grammar
+	  [(decl
+	     type
+	     (code:line (identifier : type)))]]{
+A multi-artiy function type that supports dependent and non-dependent type declarations and automatic currying.
 
 @examples[#:eval curnel-eval
-          (data And : (-> Type (-> Type Type))
+          (data And : (-> Type Type)
-            (conj : (forall (A : Type) (forall (B : Type) (-> A (-> B ((And A) B)))))))
+            (conj : (-> (A : Type) (B : Type) A B ((And A) B))))
           ((((conj Bool) Bool) true) false)]
 }
 
-@defform*[((->* t ...)
-          (→* t ...))]{
-A non-dependent multi-arity function type that supports automatic currying.
-
 @examples[#:eval curnel-eval
-          (data And : (->* Type Type Type)
+          (data And : (forall Type Type Type)
-            (conj : (forall (A : Type) (forall (B : Type) (->* A B ((And A) B))))))
+            (conj : (forall (A : Type) (B : Type) A B ((And A) B))))
-          ((((conj Bool) Bool) true) false)]
-}
-
-
-@defform*[((forall* (a : t) ... type)
-          (∀* (a : t) ... type))]{
-A multi-arity function type that supports automatic currying.
-
-@examples[#:eval curnel-eval
-          (data And : (->* Type Type Type)
-            (conj : (forall* (A : Type) (B : Type)
-                      (->* A B ((And A) B)))))
           ((((conj Bool) Bool) true) false)]
 
 }
 
-@defform*[((lambda* (a : t) ... body)
+@defform*[((lambda (a : t) ... body)
-           (λ* (a : t) ... body))]{
+           (λ (a : t) ... body))]{
 Defines a multi-arity procedure that supports automatic currying.
 
 @examples[#:eval curnel-eval
           ((lambda (x : Bool) (lambda (y : Bool) y)) true)
-          ((lambda* (x : Bool) (y : Bool) y) true)
+          ((lambda (x : Bool) (y : Bool) y) true)
           ]
 }
 
@@ -65,20 +55,19 @@ Defines a multi-arity procedure that supports automatic currying.
 Defines multi-arity procedure application via automatic currying.
 
 @examples[#:eval curnel-eval
-          (data And : (->* Type Type Type)
+          (data And : (-> Type Type Type)
-            (conj : (forall* (A : Type) (B : Type)
+	    (conj : (-> (A : Type) (B : Type) A B ((And A) B))))
-                      (->* A B ((And A) B)))))
           (conj Bool Bool true false)]
 }
 
 @defform*[((define name body)
            (define (name (x : t) ...) body))]{
-Like the @racket[define] provided by @racketmodname[cur/curnel/redex-lang], but supports
+Like the @racket[define] provided by @racketmodname[cur], but supports
-defining curried functions via @racket[lambda*].
+defining curried functions via @racket[lambda].
 }
 
 @defform[(elim type motive-result-type e ...)]{
-Like the @racket[elim] provided by @racketmodname[cur/curnel/redex-lang], but supports
+Like the @racket[elim] provided by @racketmodname[cur], but supports
 automatically curries the remaining arguments @racket[e ...].
 
 @examples[#:eval curnel-eval
@@ -90,12 +79,16 @@ automatically curries the remaining arguments @racket[e ...].
 
 @defform*[((define-type name type)
            (define-type (name (a : t) ...) body))]{
-Like @racket[define], but uses @racket[forall*] instead of @racket[lambda*].
+Like @racket[define], but uses @racket[forall] instead of @racket[lambda].
 }
 
-@defform[(match e [pattern body] ...)
+@defform[(match e [maybe-in] [maybe-return] [pattern body] ...)
          #:grammar
-         [(pattern
+         [(maybe-in
+	    (code:line #:in type))
+	  (maybe-return
+	    (code:line #:return type))
+	  (pattern
             constructor
             (code:line (constructor (x : t) ...)))]]{
 A pattern-matcher-like syntax for inductive elimination.
@@ -108,6 +101,9 @@ Generates a call to the inductive eliminator for @racket[e].
 Currently does not work on inductive type-families as types indices
 are not inferred.
 
+If @racket[#:in] is not specified, attempts to infer the type of @racket[e].
+If @racket[#:return] is not specified, attempts to infer the return type of the @racket[match].
+
 @examples[#:eval curnel-eval
           (match z
             [z true]
@@ -116,42 +112,32 @@ are not inferred.
 
 @examples[#:eval curnel-eval
           (match (s z)
+	    #:in Nat
+	    #:return Bool
             [z true]
             [(s (n : Nat))
 	    (not (recur n))])]
+
+@examples[#:eval curnel-eval
+          ((match (nil Bool)
+	    #:in (List Bool)
+            [(nil (A : Type))
+	     (lambda (n : Nat)
+	       (none A))]
+            [(cons (A : Type) (a : A) (rest : (List A)))
+	     (lambda (n : Nat)
+	       (match n
+	         [z (some A a)]
+		 [(s (n-1 : Nat))
+		  ((recur rest) n-1)]))])
+	   z)]
+
 }
 
 @defform[(recur id)]{
-A form valid only in the body of a @racket[match] clause. Generates a
+A form valid only in the body of a @racket[match] clause.
-reference to the induction hypothesis for @racket[x].
+Generates a reference to the induction hypothesis for @racket[x]
-}
+inferred by a @racket[match] clause.
-
-
-@defform[(case* type motive-result-type e (parameters ...) motive [pattern maybe-IH body] ...)
-         #:grammar
-         [(pattern
-            constructor
-            (code:line)
-            (code:line (constructor (x : t) ...)))
-          (maybe-IH
-            (code:line)
-            (code:line IH: ((x : t) ...)))]]{
-A pattern-matcher-like syntax for inductive elimination that does not try to infer the type or motive.
-Necessary for more advanced types, like @racket[And], because @racket[case] is not very smart.
-
-@margin-note{Don't worry about all that output from requiring prop}
-@examples[#:eval curnel-eval
-          (case* Nat Type z () (lambda (x : Nat) Bool)
-            [z true]
-            [(s (n : Nat))
-             IH: ((_ : Bool))
-             false])
-          (require cur/stdlib/prop)
-          (case* And Type (conj Bool Nat true z) (Bool Nat)
-            (lambda* (A : Type) (B : Type) (ab : (And A B)) A)
-            [(conj (A : Type) (B : Type) (a : A) (b : B))
-             IH: ()
-             a])]
 }
 
 @defform[(let (clause ...) body)
@@ -182,8 +168,9 @@ Check that expression @racket[e] has type @racket[type], causing a type-error if
 }
 
 @defform[(run syn)]{
-Like @racket[normalize/syn], but is a syntactic form which allows a Cur term to be written by
+Like @racket[normalize/syn], but is a syntactic form to be used in surface syntax.
-computing part of the term from another Cur term.
+Allows a Cur term to be written by computing part of the term from
+another Cur term.
 
 @examples[#:eval curnel-eval
           (lambda (x : (run (if true Bool Nat))) x)]

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

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

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

@@ -31,11 +31,9 @@
     [dep-require require]
 
     [dep-lambda lambda]
-    [dep-lambda λ]
     [dep-app #%app]
 
     [dep-forall forall]
-    [dep-forall ∀]
 
     [dep-inductive data]
 
@@ -191,35 +189,29 @@
     reified-term)
 
   (define (datum->cur syn t)
-    (match t
+    (let datum->cur ([t t])
-      [(list (quote term) e)
+      (match t
-       (quasisyntax/loc
+        [(list (quote term) e)
-         syn
+         (quasisyntax/loc syn
-         (datum->cur syn e))]
+           (datum->cur e))]
-      [(list (quote Unv) i)
+        [(list (quote Unv) i)
-       (quasisyntax/loc
+         (quasisyntax/loc syn
-         syn
+           (Type #,i))]
-         (Type #,i))]
+        [(list (quote Π) (list x (quote :) t) body)
-      [(list (quote Π) (list x (quote :) t) body)
+         (quasisyntax/loc syn
-       (quasisyntax/loc
+           (dep-forall (#,(datum->syntax syn x) : #,(datum->cur t)) #,(datum->cur body)))]
-         syn
+        [(list (quote λ) (list x (quote :) t) body)
-         (dep-forall (#,(datum->syntax syn x) : #,(datum->cur syn t)) #,(datum->cur syn body)))]
+         (quasisyntax/loc syn
-      [(list (quote λ) (list x (quote :) t) body)
+           (dep-lambda (#,(datum->syntax syn x) : #,(datum->cur t)) #,(datum->cur body)))]
-       (quasisyntax/loc
+        [(list (list (quote elim) t1) t2)
-         syn
+         (quasisyntax/loc syn
-         (dep-lambda (#,(datum->syntax syn x) : #,(datum->cur syn t)) #,(datum->cur syn body)))]
+           (dep-elim #,(datum->cur t1) #,(datum->cur t2)))]
-      [(list (list (quote elim) t1) t2)
+        [(list e1 e2)
-       (quasisyntax/loc
+         (quasisyntax/loc syn
-         syn
+           (dep-app #,(datum->cur e1) #,(datum->cur e2)))]
-         (dep-elim #,(datum->cur syn t1) #,(datum->cur syn t2)))]
+        [_
-      [(list e1 e2)
+         (quasisyntax/loc syn
-       (quasisyntax/loc
+           #,(datum->syntax syn t))])))
-         syn
-         (dep-app #,(datum->cur syn e1) #,(datum->cur syn e2)))]
-      [_
-       (quasisyntax/loc
-         syn
-         #,(datum->syntax syn t))]))
 
   (define (eval-cur syn)
     (term (reduce ,(delta) ,(subst-bindings (cur->datum syn)))))
@@ -424,8 +416,8 @@
        (quasisyntax/loc syn (λ (x : t) e)))]))
 
 (define-syntax (dep-app syn)
-  (syntax-case syn ()
+  (syntax-parse syn
-    [(_ e1 e2)
+    [(_ e1:expr e2:expr)
      (syntax->curnel-syntax
        (quasisyntax/loc syn (#%app e1 e2)))]))
 

cur-lib/cur/olly.rkt

@@ -4,7 +4,8 @@
 (require
   "stdlib/sugar.rkt"
   "stdlib/nat.rkt"
-  (only-in "cur.rkt" [#%app real-app] [elim real-elim]))
+  ;; TODO: "real-"? More like "curnel-"
+  (only-in "cur.rkt" [#%app real-app] [elim real-elim] [forall real-forall] [lambda real-lambda]))
 
 (provide
   define-relation
@@ -38,8 +39,7 @@
               x*:expr ...
               line:dash lab:id
               (name:id y* ...))
-              #:with rule #'(lab : (forall* d ...
+              #:with rule #'(lab : (-> d ... x* ... (name y* ...)))
-                                     (->* x* ... (name y* ...))))
               ;; TODO: convert meta-vars such as e1 to e_1
               #:attr latex (format "\\inferrule~n{~a}~n{~a}"
                              (string-trim
@@ -62,7 +62,7 @@
      #: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 ...)])
+      (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)
@@ -128,7 +128,7 @@
              #: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 ...))
+             #: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 ...)))))
 
@@ -243,7 +243,7 @@
     (syntax-parse (cur-expand syn #'define #'begin)
        ;; TODO: Need to add these to a literal set and export it
        ;; Or, maybe overwrite syntax-parse
-       #:literals (lambda forall data real-app real-elim define begin Type)
+       #:literals (real-lambda real-forall data real-app real-elim define begin Type)
        [(begin e ...)
         (for/fold ([str ""])
                   ([e (syntax->list #'(e ...))])
@@ -266,10 +266,10 @@
                       (format "~a(~a : ~a) " str (output-coq n) (output-coq t)))
                     (output-coq #'body)))
           "")]
-       [(lambda ~! (x:id (~datum :) t) body:expr)
+       [(real-lambda ~! (x:id (~datum :) t) body:expr)
         (format "(fun ~a : ~a => ~a)" (output-coq #'x) (output-coq #'t)
                 (output-coq #'body))]
-       [(forall ~! (x:id (~datum :) t) body:expr)
+       [(real-forall ~! (x:id (~datum :) t) body:expr)
         (format "(forall ~a : ~a, ~a)" (syntax-e #'x) (output-coq #'t)
                 (output-coq #'body))]
        [(data ~! n:id (~datum :) t (x*:id (~datum :) t*) ...)

cur-lib/cur/stdlib/list.rkt

@@ -10,20 +10,28 @@
  cons
  list-ref)
 
-(data List : (forall (A : Type) Type)
+(data List : (-> (A : Type) Type)
-  (nil : (forall (A : Type) (List A)))
+  (nil : (-> (A : Type) (List A)))
-  (cons : (forall* (A : Type) (->* A (List A) (List A)))))
+  (cons : (-> (A : Type) A (List A) (List A))))
 
-(define list-ref
+(define (list-ref (A : Type) (ls : (List A)))
-  (elim
+  (match ls
+    [(nil (A : Type)) (lambda (n : Nat) (none A))]
+    [(cons (A : Type) (a : A) (rest : (List A)))
+     (lambda (n : Nat)
+       (match n
+         [z (some A a)]
+         [(s (n-1 : Nat))
+          ((recur rest) n-1)]))])
+  #;(elim
    List
    Type
-   (lambda* (A : Type) (ls : (List A))
+   (lambda (A : Type) (ls : (List A))
             (-> Nat (Maybe A)))
-   (lambda* (A : Type) (n : Nat) (none A))
+   (lambda (A : Type) (n : Nat) (none A))
-   (lambda* (A : Type) (a : A) (ls : (List A)) (ih : (-> Nat (Maybe A)))
+   (lambda (A : Type) (a : A) (ls : (List A)) (ih : (-> Nat (Maybe A)))
-            (lambda (n : Nat)
+           (lambda (n : Nat)
-              (match n
+             (match n
-                [z (some A a)]
+               [z (some A a)]
-                [(s (n-1 : Nat))
+               [(s (n-1 : Nat))
-                 (ih n-1)])))))
+                (ih n-1)])))))

cur-lib/cur/stdlib/maybe.rkt

@@ -4,7 +4,7 @@
 
 (data Maybe : (forall (A : Type) Type)
   (none : (forall (A : Type) (Maybe A)))
-  (some : (forall* (A : Type) (a : A) (Maybe A))))
+  (some : (forall (A : Type) (a : A) (Maybe A))))
 
 (define-syntax (some/i syn)
   (syntax-case syn ()

cur-lib/cur/stdlib/nat.rkt

@@ -35,17 +35,21 @@
 
 (define square (run (exp (s (s z)))))
 
-;; Credit to this function goes to Max
+(define (zero? (n : Nat))
-(define nat-equal?
+  (match n
-  (elim Nat Type (lambda (x : Nat) (-> Nat Bool))
+    [z true]
-    (elim Nat Type (lambda (x : Nat) Bool)
+    [(s (n : Nat))
-          true
+     false]))
-          (lambda* (x : Nat) (ih-n2 : Bool) false))
+
-    (lambda* (x : Nat) (ih : (-> Nat Bool))
+(define (nat-equal? (n : Nat))
-      (elim Nat Type (lambda (x : Nat) Bool)
+  (match n
-            false
+    [z zero?]
-            (lambda* (x : Nat) (ih-bla : Bool)
+    [(s (n-1 : Nat))
-                     (ih x))))))
+     (lambda (m : Nat)
+       (match m
+         [z false]
+         [(s (m-1 : Nat))
+          ((recur n-1) m-1)]))]))
 
 (define (even? (n : Nat))
   (match n

cur-lib/cur/stdlib/prop.rkt

@@ -24,8 +24,8 @@
 
 (define-type (Not (A : Type)) (-> A False))
 
-(data And : (forall* (A : Type) (B : Type) Type)
+(data And : (forall (A : Type) (B : Type) Type)
-  (conj : (forall* (A : Type) (B : Type)
+  (conj : (forall (A : Type) (B : Type)
             (x : A) (y : B) (And A B))))
 
 (define-syntax (conj/i syn)
@@ -36,52 +36,49 @@
        #`(conj #,a-type #,b-type a b))]))
 
 (define thm:and-is-symmetric
-  (forall* (P : Type) (Q : Type) (ab : (And P Q)) (And Q P)))
+  (forall (P : Type) (Q : Type) (ab : (And P Q)) (And Q P)))
 
 (define pf:and-is-symmetric
-  (lambda* (P : Type) (Q : Type) (ab : (And P Q))
+  (lambda (P : Type) (Q : Type) (ab : (And P Q))
-    (case* And Type ab (P Q)
+          (match ab
-      (lambda* (P : Type) (Q : Type) (ab : (And P Q))
+            [(conj (P : Type) (Q : Type) (x : P) (y : Q))
-         (And Q P))
+             (conj/i y x)])))
-      ((conj (P : Type) (Q : Type) (x : P) (y : Q)) IH: () (conj/i y x)))))
 
 (define thm:proj1
-  (forall* (A : Type) (B : Type) (c : (And A B)) A))
+  (forall (A : Type) (B : Type) (c : (And A B)) A))
 
 (define pf:proj1
-  (lambda* (A : Type) (B : Type) (c : (And A B))
+  (lambda (A : Type) (B : Type) (c : (And A B))
-    (case* And Type c (A B)
+          (match c
-      (lambda* (A : Type) (B : Type) (c : (And A B)) A)
+            [(conj (A : Type) (B : Type) (a : A) (b : B)) a])))
-      ((conj (A : Type) (B : Type) (a : A) (b : B)) IH: () a))))
 
 (define thm:proj2
-  (forall* (A : Type) (B : Type) (c : (And A B)) B))
+  (forall (A : Type) (B : Type) (c : (And A B)) B))
 
 (define pf:proj2
-  (lambda* (A : Type) (B : Type) (c : (And A B))
+  (lambda (A : Type) (B : Type) (c : (And A B))
-    (case* And Type c (A B)
+          (match c
-      (lambda* (A : Type) (B : Type) (c : (And A B)) B)
+            [(conj (A : Type) (B : Type) (a : A) (b : B)) b])))
-      ((conj (A : Type) (B : Type) (a : A) (b : B)) IH: () b))))
 
 #| TODO: Disabled until #22 fixed
-(data Or : (forall* (A : Type) (B : Type) Type)
+(data Or : (forall (A : Type) (B : Type) Type)
-  (left : (forall* (A : Type) (B : Type) (a : A) (Or A B)))
+  (left : (forall (A : Type) (B : Type) (a : A) (Or A B)))
-  (right : (forall* (A : Type) (B : Type) (b : B) (Or A B))))
+  (right : (forall (A : Type) (B : Type) (b : B) (Or A B))))
 
 (define-theorem thm:A-or-A
-  (forall* (A : Type) (o : (Or A A)) A))
+  (forall (A : Type) (o : (Or A A)) A))
 
 (define proof:A-or-A
-  (lambda* (A : Type) (c : (Or A A))
+  (lambda (A : Type) (c : (Or A A))
     ;; TODO: What should the motive be?
-    (elim Or Type (lambda* (A : Type) (B : Type) (c : (Or A B)) A)
+    (elim Or Type (lambda (A : Type) (B : Type) (c : (Or A B)) 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)
       A A c)))
 
 (qed thm:A-or-A proof:A-or-A)
 |#
 
-(data == : (forall* (A : Type) (x : A) (-> A Type))
+(data == : (forall (A : Type) (x : A) (-> A Type))
-  (refl : (forall* (A : Type) (x : A) (== A x x))))
+  (refl : (forall (A : Type) (x : A) (== A x x))))

cur-lib/cur/stdlib/sugar.rkt

@@ -1,20 +1,16 @@
 #lang s-exp "../cur.rkt"
 (provide
   ->
-  ->*
+  lambda
-  forall*
-  lambda*
   (rename-out
     [-> →]
-    [->* →*]
+    [-> forall]
-    [lambda* λ*]
+    [-> ∀]
-    [forall* ∀*])
+    [lambda λ])
   #%app
   define
   elim
   define-type
-  case
-  case*
   match
   recur
   let
@@ -32,127 +28,249 @@
   (only-in "../cur.rkt"
     [elim real-elim]
     [#%app real-app]
+    ;; Somehow, using real-lambda instead of _lambda causes weird import error
+    [lambda real-lambda]
+    #;[forall real-forall]
     [define real-define]))
 
+(begin-for-syntax
+  (define-syntax-class result-type
+    (pattern type:expr))
+
+  (define-syntax-class parameter-declaration
+    (pattern (name:id (~datum :) type:expr))
+
+    (pattern
+     type:expr
+     #:attr name (format-id #'type "~a" (gensym 'anon-parameter)))))
+
+;; A multi-arity function type; takes parameter declaration of either
+;; a binding (name : type), or type whose name is generated.
+;; E.g.
+;; (-> (A : Type) A A)
 (define-syntax (-> syn)
-  (syntax-case syn ()
+  (syntax-parse syn
-    [(_ t1 t2) #`(forall (#,(gensym) : t1) t2)]))
+    [(_ d:parameter-declaration ...+ result:result-type)
+     (foldr (lambda (src name type r)
+              (quasisyntax/loc src
+                (forall (#,name : #,type) #,r)))
+            #'result
+            (attribute d)
+            (attribute d.name)
+            (attribute d.type))]))
 
-(define-syntax ->*
+;; TODO: Add forall macro that allows specifying *names*, with types
-  (syntax-rules ()
+;; inferred. unlike -> which require types but not names
-    [(->* a) a]
+;; E.g.
-    [(->* a a* ...)
+;; (forall x (y : Nat) (== Nat x y))
-     (-> a (->* a* ...))]))
 
-(define-syntax forall*
+;; TODO: Allows argument-declarations to have types inferred, similar
-  (syntax-rules (:)
+;; to above TODO forall
-    [(_ (a : t) (ar : tr) ... b)
+(begin-for-syntax
-     (forall (a : t)
+  ;; eta-expand syntax-class for error messages
-        (forall* (ar : tr) ... b))]
+  (define-syntax-class argument-declaration
-    [(_ b) b]))
+    (pattern
-
+     e:parameter-declaration
-(define-syntax lambda*
+     #:attr name #'e.name
-  (syntax-rules (:)
+     #:attr type #'e.type)))
-    [(_ (a : t) (ar : tr) ... b)
+(define-syntax (lambda syn)
-     (lambda (a : t)
+  (syntax-parse syn
-       (lambda* (ar : tr) ... b))]
+    [(_ d:argument-declaration ...+ body:expr)
-    [(_ b) b]))
+     (foldr (lambda (src name type r)
+              (quasisyntax/loc src
+                (real-lambda (#,name : #,type) #,r)))
+            #'body
+            (attribute d)
+            (attribute d.name)
+            (attribute d.type))]))
 
+;; TODO: This makes for really bad error messages when an identifier is undefined.
 (define-syntax (#%app syn)
   (syntax-case syn ()
-    [(_ e) #'e]
+    [(_ e)
+     (quasisyntax/loc syn e)]
     [(_ e1 e2)
-     #'(real-app e1 e2)]
+     (quasisyntax/loc syn
+       (real-app e1 e2))]
     [(_ e1 e2 e3 ...)
-     #'(#%app (#%app e1 e2) e3 ...)]))
+     (quasisyntax/loc syn
+       (#%app (#%app e1 e2) e3 ...))]))
+(module+ test
+  ((lambda (A : (Type 1)) (B : (Type 1)) A)
+   Type
+   Type))
 
 (define-syntax define-type
   (syntax-rules ()
     [(_ (name (a : t) ...) body)
-     (define name (forall* (a : t) ... body))]
+     (define name (forall (a : t) ... body))]
     [(_ name type)
      (define name type)]))
 
+;; TODO: Allow inferring types as in above TODOs for lambda, forall
 (define-syntax (define syn)
   (syntax-case syn ()
     [(define (name (x : t) ...) body)
-     #'(real-define name (lambda* (x : t) ... body))]
+     (quasisyntax/loc syn
+       (real-define name (lambda (x : t) ... body)))]
     [(define id body)
-     #'(real-define id body)]))
+     (quasisyntax/loc syn
+       (real-define id body))]))
 
 (define-syntax-rule (elim t1 t2 e ...)
   ((real-elim t1 t2) e ...))
 
+;; Quite fragie to give a syntactic treatment of pattern matching -> eliminator. Replace with "Elimination with a Motive"
 (begin-for-syntax
-  (define (rewrite-clause clause)
-    (syntax-case clause (: IH:)
-      [((con (a : A) ...) IH: ((x : t) ...) body)
-       #'(lambda* (a : A) ... (x : t) ... body)]
-      [(e body) #'body])))
-
-;; TODO: Expects clauses in same order as constructors as specified when
-;; TODO: inductive D is defined.
-;; TODO: Assumes D has no parameters
-(define-syntax (case syn)
-  ;; duplicated code
-  (define (clause-body syn)
-    (syntax-case (car (syntax->list syn)) (: IH:)
-      [((con (a : A) ...) IH: ((x : t) ...) body) #'body]
-      [(e body) #'body]))
-  (syntax-case syn (=>)
-    [(_ e clause* ...)
-     (let* ([D (type-infer/syn #'e)]
-            [M (type-infer/syn (clause-body #'(clause* ...)))]
-            [U (type-infer/syn M)])
-       #`(elim #,D #,U (lambda (x : #,D) #,M) #,@(map rewrite-clause (syntax->list #'(clause* ...)))
-               e))]))
-
-(define-syntax (case* syn)
-  (syntax-case syn ()
-    [(_ D U e (p ...) P clause* ...)
-     #`(elim D U P #,@(map rewrite-clause (syntax->list #'(clause* ...))) p ... e)]))
-
-(begin-for-syntax
-  (define-struct clause (args types decl body))
   (define ih-dict (make-hash))
-  (define (clause-parse syn)
-    (syntax-case syn (:)
-      [((con (a : A) ...) body)
-       (make-clause (syntax->list #'(a ...)) (syntax->list #'(A ...)) #'((a : A) ...) #'body)]
-      [(e body)
-       (make-clause '() '() #'() #'body)]))
 
-  (define (infer-result clauses)
+  (define-syntax-class curried-application
-    (or
+    (pattern
-     (for/or ([clause clauses])
+     ((~literal real-app) name:id e:expr)
-       (type-infer/syn
+     #:attr args
-        (clause-body clause)
+     (list #'e))
-        #:local-env (for/fold ([d '()])
-                              ([arg (clause-args clause)]
-                               [type (clause-types clause)])
-                          (dict-set d arg type))))
-     (raise-syntax-error
-      'match
-      "Could not infer type of result."
-      (clause-body (car clauses)))))
 
-  (define (infer-ihs D motive args types)
+    (pattern
-    (for/fold ([ih-dict (make-immutable-hash)])
+     ((~literal real-app) a:curried-application e:expr)
-              ([type-syn types]
+     #:attr name #'a.name
-               [arg-syn args]
+     #:attr args
-               ;; NB: Non-hygenic
+     ;; TODO BUG: repeated appends are not performant; cons then reverse in inductive-type-declaration
-               #:when (cur-equal? type-syn D))
+     (append
-      (dict-set ih-dict (syntax->datum arg-syn) `(,(format-id arg-syn "ih-~a" arg-syn) . ,#`(#,motive #,arg-syn)))))
+      (attribute a.args)
+      (list #'e))))
 
-  (define (clause->method D motive clause)
+  (define-syntax-class inductive-type-declaration
-    (dict-clear! ih-dict)
+    (pattern
-    (let* ([ihs (infer-ihs D motive (clause-args clause) (clause-types clause))]
+     x:id
-           [ih-args (dict-map
+     #:attr inductive-name
-                     ihs
+     #'x
-                     (lambda (k v)
+     #:attr indices
-                       (dict-set! ih-dict k (car v))
+     '()
-                       #`(#,(car v) : #,(cdr v))))])
+     #:attr decls
-      #`(lambda* #,@(clause-decl clause) #,@ih-args #,(clause-body clause)))))
+     (list #`(#,(gensym 'anon-discriminant) : x))
+     #:attr abstract-indices
+     values)
+
+    (pattern
+     ;; BUG TODO NB: Because the inductive type may have been inferred, it may appear in Curnel syntax, i.e., nested applications starting with dep-app
+     ;; Best to ensure it *always* is in Curnel form, and pattern match on that.
+     a:curried-application
+     #:attr inductive-name
+     (attribute a.name)
+     #:attr indices
+     (attribute a.args)
+     #:attr names
+     (for/list ([e (attribute indices)])
+       (format-id e "~a" (gensym 'anon-index)))
+     #:attr types
+     ;; TODO: Detect failure, report error/suggestions
+     (for/list ([e (attribute indices)])
+       (or (type-infer/syn e)
+           (raise-syntax-error
+            'match
+            (format
+             "Could not infer type of index ~a"
+             e)
+            e)))
+     #:attr decls
+     (append
+      (for/list ([name (attribute names)]
+                 [type (attribute types)]
+                 [src (attribute indices)])
+        (quasisyntax/loc src
+          (#,name : #,type)))
+      (list
+       (quasisyntax/loc #'a
+         (#,(gensym 'anon-discriminant) : (inductive-name #,@(attribute names))))))
+     #:attr abstract-indices
+     (lambda (return)
+       ;; NB: unhygenic
+       ;; Normalize at compile-time, for efficiency at run-time
+       (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
+             #,@(for/list ([name (attribute indices)]
+                           [type (attribute types)])
+                 #`(#,name : #,type))
+            #,return)
+          #,@(attribute names))))))
+
+  ;; todo: Support just names, inferring types
+  (define-syntax-class match-declaration
+    (pattern
+     ;; TODO: Use parameter-declaration defined earlier
+     (name:id (~datum :) type:expr)
+     #:attr decl
+     #'(name : type)))
+
+  (define-syntax-class match-prepattern
+    ;; TODO: Check that x is a valid constructor for the inductive type
+    (pattern
+     x:id
+     #:attr local-env
+     '()
+     #:attr decls
+     '()
+     #:attr types
+     '()
+     #:attr names
+     '())
+
+    (pattern
+     (x:id d:match-declaration ...+)
+     #:attr local-env
+     (for/fold ([d (make-immutable-hash)])
+               ([name (attribute d.name)]
+                [type (attribute d.type)])
+       (dict-set d name type))
+     #:attr decls
+     (attribute d.decl)
+     #:attr names
+     (attribute d.name)
+     #:attr types
+     (attribute d.type)))
+
+  (define-syntax-class (match-pattern D motive)
+    (pattern
+     d:match-prepattern
+     #:attr decls
+     ;; Infer the inductive hypotheses, add them to the pattern decls
+     ;; and update the dictionarty for the recur form
+     (for/fold ([decls (attribute d.decls)])
+               ([type-syn (attribute d.types)]
+                [name-syn (attribute d.names)]
+                [src (attribute d.decls)]
+                ;; NB: Non-hygenic
+                ;; BUG TODO: This fails when D is an inductive applied to arguments...
+                #:when (cur-equal? type-syn D))
+       (define/syntax-parse type:inductive-type-declaration (cur-expand type-syn))
+       (let ([ih-name (quasisyntax/loc src #,(format-id name-syn "ih-~a" name-syn))]
+             ;; Normalize at compile-time, for efficiency at run-time
+             [ih-type (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)))))))
+
+  (define-syntax-class (match-preclause maybe-return-type)
+    (pattern
+     (p:match-prepattern b:expr)
+     #:attr return-type
+     ;; TODO: Check that the infered type matches maybe-return-type, if it is provied
+     (or maybe-return-type
+         ;; Ignore errors when trying to infer this type; other attempt might succeed
+         (with-handlers ([values (lambda _ #f)])
+           (type-infer/syn #:local-env (attribute p.local-env) #'b)))))
+
+  (define-syntax-class (match-clause D motive)
+    (pattern
+     ((~var p (match-pattern D motive))
+      ;; TODO: nothing more advanced?
+      b:expr)
+     #:attr method
+     (quasisyntax/loc #'p
+       #,(if (null? (attribute p.decls))
+         #'b
+         #`(lambda #,@(attribute p.decls) b))))))
 
 (define-syntax (recur syn)
   (syntax-case syn ()
@@ -163,23 +281,55 @@
       (lambda ()
         (raise-syntax-error
          'match
-         (format "Cannot recur on ~a" (syntax->datum #'id))
+         ;; TODO: Detect when inside a match to provide better error
+         (format
+          "Cannot recur on ~a. Ether not inside a match or ~a is not an inductive argument."
+          (syntax->datum #'id)
+          (syntax->datum #'id))
          syn)))]))
 
-;; TODO: Test
 (define-syntax (match syn)
-  (syntax-case syn ()
+  (syntax-parse syn
-    [(_ e clause* ...)
+    [(_ d
-     (let* ([clauses (map clause-parse (syntax->list #'(clause* ...)))]
+        ~!
-            [R (infer-result clauses)]
+        (~optional
-            [D (or (type-infer/syn #'e)
+         (~seq #:in ~! t)
-                   (raise-syntax-error 'match "Could not infer discrimnant's type." syn))]
+         #:defaults
-	    [motive #`(lambda (x : #,D) #,R)]
+         ([t (or (type-infer/syn #'d)
-            [U (type-infer/syn R)])
+                 (raise-syntax-error
-       #`((elim #,D #,U)
+                  'match
-            #,motive
+                  "Could not infer discrimnant's type. Try using #:in to declare it."
-	    #,@(map (curry clause->method D motive) clauses)
+                  syn))]))
-	    e))]))
+        (~optional (~seq #:return ~! maybe-return-type))
+        (~peek (~seq (~var prec (match-preclause (attribute maybe-return-type))) ...))
+        ~!
+        (~parse D:inductive-type-declaration (cur-expand (attribute t)))
+        (~bind (return-type (ormap values (attribute prec.return-type))))
+        (~do (unless (attribute return-type)
+               (raise-syntax-error
+                'match
+                "Could not infer return type. Try using #:return to declare it."
+                syn)))
+        ;; BUG TODO: return-type is inferred with the indexes of the branches, but those must be abstracted in the motive...
+        ;; Replace each of the D.indicies with the equivalent name from D.decls
+        (~bind (motive (quasisyntax/loc syn
+                         (lambda #,@(attribute D.decls)
+                           #,((attribute D.abstract-indices) (attribute return-type))))))
+        (~var c (match-clause (attribute D) (attribute motive))) ...)
+     ;; TODO: Make all syntax extensions type check, report good error, rather than fail at Curnel
+     (quasisyntax/loc syn
+       (elim
+        D.inductive-name
+        #,(or
+           (type-infer/syn (attribute return-type))
+           (raise-syntax-error
+            'match
+            "Could not infer type of motive. Sorry, you'll have to use elim."
+            syn))
+        motive
+        c.method ...
+        #,@(attribute D.indices)
+        d))]))
 
 (begin-for-syntax
   (define-syntax-class let-clause
@@ -206,7 +356,7 @@
 (define-syntax (let syn)
   (syntax-parse syn
     [(let (c:let-clause ...) body)
-     #'((lambda* (c.id : c.type) ... body) c.e ...)]))
+     #'((lambda (c.id : c.type) ... body) c.e ...)]))
 
 ;; Normally type checking will only happen if a term is actually used. This forces a term to be
 ;; checked against a particular type.

cur-lib/cur/stdlib/typeclass.rkt

@@ -49,7 +49,7 @@
   (define (process-def def)
     (syntax-case def (define)
       [(define (name (a : t) ...) body ...)
-       (values (syntax->datum #'name) #'(lambda* (a : t) ... body ...))]
+       (values (syntax->datum #'name) #'(lambda (a : t) ... body ...))]
       [(define name body)
        (values (syntax->datum #'name) #'body)]))
   (syntax-case syn ()

cur-test/cur/tests/olly.rkt

@@ -67,7 +67,7 @@
      "\\| T-Bla : \\(forall g : gamma, \\(forall e : term, \\(forall t : type, \\(\\(\\(meow g\\) e\\) t\\)\\)\\)\\)\\."
      (second (string-split t "\n"))))
   (let ([t (output-coq #'(elim nat Type (lambda (x : nat) nat) z
-                               (lambda* (x : nat) (ih-x : nat) ih-x)
+                               (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\\)"
@@ -75,7 +75,7 @@
   (check-regexp-match
    "Definition thm_plus_commutes := \\(forall n : nat, \\(forall m : nat, \\(\\(\\(== nat\\) \\(\\(plus n\\) m\\)\\) \\(\\(plus m\\) n\\)\\)\\)\\).\n"
    (parameterize ([coq-defns ""])
-     (output-coq #'(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)))))
      (coq-defns)))
   (check-regexp-match

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

@@ -17,24 +17,24 @@
  (:: (cons Bool true (nil Bool)) (List Bool)))
 (check-equal?
  (void)
- (:: (lambda* (A : Type) (a : A)
+ (:: (lambda (A : Type) (a : A)
              (ih-a : (-> Nat (Maybe A))) 
              (n : Nat)
              (match n
                [z (some A a)]
                [(s (n-1 : Nat))
                 (ih-a n-1)]))
-    (forall* (A : Type) (a : A) (ih-a : (-> Nat (Maybe A)))
+     (forall (A : Type) (a : A) (ih-a : (-> Nat (Maybe A)))
              (n : Nat)
              (Maybe A))))
 (check-equal?
  (void)
- (:: (lambda* (A : Type) (n : Nat) (none A)) (forall (A : Type) (-> Nat (Maybe A)))))
+ (:: (lambda (A : Type) (n : Nat) (none A)) (forall (A : Type) (-> Nat (Maybe A)))))
 (check-equal?
  (void)
- (:: (elim List Type (lambda* (A : Type) (ls : (List A)) Nat)
+ (:: (elim List Type (lambda (A : Type) (ls : (List A)) Nat)
           (lambda (A : Type) z)
-          (lambda* (A : Type) (a : A) (ls : (List A)) (ih : Nat)
+          (lambda (A : Type) (a : A) (ls : (List A)) (ih : Nat)
                    z)
           Bool
           (nil Bool))
@@ -43,7 +43,7 @@
 
 (check-equal?
  (void)
- (:: list-ref (forall (A : Type) (->* (List A) Nat (Maybe A)))))
+ (:: list-ref (forall (A : Type) (-> (List A) Nat (Maybe A)))))
 (check-equal?
  ((list-ref Bool (cons Bool true (nil Bool))) z)
  (some Bool true))

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

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

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

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

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

@@ -5,19 +5,19 @@
 
 ;; TODO: Missing tests for match, others
 (check-equal?
- ((λ* (x : (Type 1)) (y : (∀* (x : (Type 1)) (Type 1))) (y x))
+ ((λ (x : (Type 1)) (y : (∀ (x : (Type 1)) (Type 1))) (y x))
   Type
   (λ (x : (Type 1)) x))
  Type)
 
 (check-equal?
- ((λ* (x : (Type 1)) (y : (→* (Type 1) (Type 1))) (y x))
+ ((λ (x : (Type 1)) (y : (→ (Type 1) (Type 1))) (y x))
   Type
   (λ (x : (Type 1)) x))
  Type)
 
 (check-equal?
- ((λ* (x : (Type 1)) (y : (→ (Type 1) (Type 1))) (y x))
+ ((λ (x : (Type 1)) (y : (→ (Type 1) (Type 1))) (y x))
   Type
   (λ (x : (Type 1)) x))
  Type)

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

@@ -8,7 +8,7 @@
  cur/stdlib/typeclass)
 
 (typeclass (Eqv (A : Type))
-           (equal? : (forall* (a : A) (b : A) Bool)))
+           (equal? : (forall (a : A) (b : A) Bool)))
 (impl (Eqv Bool)
       (define (equal? (a : Bool) (b : Bool))
         (if a

cur-test/cur/tests/stlc.rkt

@@ -21,16 +21,15 @@
 ;; TODO: Abstract this over stlc-type, and provide from in OLL
 (data Gamma : Type
   (emp-gamma : Gamma)
-  (extend-gamma : (->* Gamma Var stlc-type Gamma)))
+  (extend-gamma : (-> Gamma Var stlc-type Gamma)))
 
 (define (lookup-gamma (g : Gamma) (x : Var))
-  (case* Gamma Type g () (lambda* (g : Gamma) (Maybe stlc-type))
+  (match g
     [emp-gamma (none stlc-type)]
     [(extend-gamma (g1 : Gamma) (v1 : Var) (t1 : stlc-type))
-     IH: ((ih-g1 : (Maybe stlc-type)))
      (if (var-equal? v1 x)
          (some stlc-type t1)
-         ih-g1)]))
+         (recur g1))]))
 
 (define-relation (has-type Gamma stlc-term stlc-type)
   #:output-coq "stlc.v"
@@ -97,7 +96,7 @@
          ;; Replace x with a de bruijn index, by running a CIC term at
          ;; compile time.
          (normalize/syn
-           #`((lambda* (x : stlc-term)
+           #`((lambda (x : stlc-term)
                       (stlc-lambda (avar #,oldindex) #,(stlc #'t) #,(stlc #'e)))
              (Var-->-stlc-term (avar #,oldindex)))))]
       [(quote (e1 e2))
@@ -106,7 +105,7 @@
        (let* ([y index]
               [x #`(s #,y)])
          (set! index #`(s (s #,index)))
-         #`((lambda* (x : stlc-term) (y : stlc-term)
+         #`((lambda (x : stlc-term) (y : stlc-term)
               (stlc-let (avar #,x) (avar #,y) #,(stlc #'t) #,(stlc #'e1)
                    #,(stlc #'e2)))
             (Var-->-stlc-term (avar #,x))