Converted cur-lib to simpler sugar

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

@@ -40,11 +40,11 @@
   (elim Nat Type (lambda (x : Nat) (-> Nat Bool))
     (elim Nat Type (lambda (x : Nat) Bool)
           true
-          (lambda* (x : Nat) (ih-n2 : Bool) false))
+          (lambda (x : Nat) (ih-n2 : Bool) false))
-    (lambda* (x : Nat) (ih : (-> Nat Bool))
+    (lambda (x : Nat) (ih : (-> Nat Bool))
       (elim Nat Type (lambda (x : Nat) Bool)
             false
-            (lambda* (x : Nat) (ih-bla : Bool)
+            (lambda (x : Nat) (ih-bla : Bool)
                      (ih x))))))
 
 (define (even? (n : Nat))

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,31 +36,31 @@
        #`(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)
-      (lambda* (P : Type) (Q : Type) (ab : (And P Q))
+      (lambda (P : Type) (Q : Type) (ab : (And P Q))
          (And Q P))
       ((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)
-      (lambda* (A : Type) (B : Type) (c : (And A B)) A)
+      (lambda (A : Type) (B : Type) (c : (And A 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)
-      (lambda* (A : Type) (B : Type) (c : (And A B)) B)
+      (lambda (A : Type) (B : Type) (c : (And A B)) B)
       ((conj (A : Type) (B : Type) (a : A) (b : B)) IH: () b))))
 
 #| TODO: Disabled until #22 fixed
@@ -83,5 +83,5 @@
 (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

@@ -30,25 +30,17 @@
   (only-in "../cur.rkt"
     [elim real-elim]
     [#%app real-app]
-    #;[lambda real-lambda]
+    ;; Somehow, using real-lambda instead of _lambda causes weird import error
+    [lambda _lambda]
     #;[forall real-forall]
-    [define real-define]
+    [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)
+    (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
@@ -88,7 +80,7 @@
     [(_ d:argument-declaration ...+ body:expr)
      (foldr (lambda (src name type r)
               (quasisyntax/loc src
-                (real-lambda (#,name : #,type) #,r)))
+                (_lambda (#,name : #,type) #,r)))
             #'body
             (attribute d)
             (attribute d.name)
@@ -108,7 +100,7 @@
 (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)]))
 
@@ -129,7 +121,7 @@
   (define (rewrite-clause clause)
     (syntax-case clause (: IH:)
       [((con (a : A) ...) IH: ((x : t) ...) body)
-       #'(lambda* (a : A) ... (x : t) ... body)]
+       #'(lambda (a : A) ... (x : t) ... body)]
       [(e body) #'body])))
 
 ;; TODO: Expects clauses in same order as constructors as specified when
@@ -186,6 +178,11 @@
                #:when (cur-equal? type-syn D))
       (dict-set ih-dict (syntax->datum arg-syn) `(,(format-id arg-syn "ih-~a" arg-syn) . ,#`(#,motive #,arg-syn)))))
 
+  (define (make-method args body)
+    (if (null? args)
+        body
+        #`(lambda #,@args #,body)))
+
   (define (clause->method D motive clause)
     (dict-clear! ih-dict)
     (let* ([ihs (infer-ihs D motive (clause-args clause) (clause-types clause))]
@@ -194,7 +191,7 @@
                      (lambda (k v)
                        (dict-set! ih-dict k (car v))
                        #`(#,(car v) : #,(cdr v))))])
-      #`(lambda* #,@(clause-decl clause) #,@ih-args #,(clause-body clause)))))
+      (make-method (append (syntax->list (clause-decl clause)) ih-args) (clause-body clause)))))
 
 (define-syntax (recur syn)
   (syntax-case syn ()
@@ -248,7 +245,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 ()