Simplifying the syntax sugar

Right now, the syntax sugar provided by Cur is instructive, but annoying
to use.
Time to make it easier to use.

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]
 

cur-lib/cur/stdlib/list.rkt

@@ -10,20 +10,20 @@
  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
   (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/sugar.rkt

@@ -1,14 +1,12 @@
 #lang s-exp "../cur.rkt"
 (provide
   ->
-  ->*
+  lambda
-  forall*
-  lambda*
   (rename-out
     [-> →]
-    [->* →*]
+    [-> forall]
-    [lambda* λ*]
+    [-> ∀]
-    [forall* ∀*])
+    [lambda λ])
   #%app
   define
   elim
@@ -32,39 +30,80 @@
   (only-in "../cur.rkt"
     [elim real-elim]
     [#%app real-app]
-    [define real-define]))
+    #;[lambda real-lambda]
+    #;[forall real-forall]
+    [define real-define]
+    [type-infer/syn _type-infer/syn]))
 
+(begin-for-syntax
+  (define (type-infer/syn #:local-env [env '()] syn)
+    (or (syntax-property syn 'type)
+        (type-infer/syn #:local-env env syn)))
+
+  (define-syntax-class result-type
+    (pattern type:expr))
+
+  (define-syntax-class parameter-declaration
+    (pattern (name:id (~datum :) type:expr)
+             ;; NB: syntax-parse apparently screws up the order in
+             ;; which macros are expanded, so my hand-rolled gamma is not working
+             ;; NOTE: This syntax property cannot be trusted...
+             #:do (syntax-property #'name 'type #'type))
+
+    (pattern
+     type:expr
+     #:attr name (format-id #'type "~a" (gensym)))))
+
+;; 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))]))
 
 (define-syntax (#%app syn)
   (syntax-case syn ()
-    [(_ e) #'e]
+    [(_ e)
+     (quasisyntax/loc syn e)]
     [(_ e1 e2)
-     #'(real-app e1 e2)]
+     (quasisyntax/loc syn
+       (real-app e1 e2))]
     [(_ e1 e2 e3 ...)
-     #'(#%app (#%app e1 e2) e3 ...)]))
+     (quasisyntax/loc syn
+       (#%app (#%app e1 e2) e3 ...))]))
 
 (define-syntax define-type
   (syntax-rules ()
@@ -73,12 +112,15 @@
     [(_ 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 ...))