improve surface syntax

Signed-off-by: Lîm Tsú-thuàn <[email protected]>
dannypsnl-fork · Nov 26, 2022 · c994d7a · c994d7a
1 parent 62163d2
commit c994d7a
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 4 deletions.
diff --git a/main.rkt b/main.rkt
@@ -10,7 +10,7 @@
    #:args ()
    ; let Nat : U = (N : U) -> (N -> N) -> N -> N;
    (define tm (parse
-               #'(let id : ((A : U) -> (A -> A)) = (lam A (lam x x))
+               #'(let id : ((A : U) -> (A -> A)) = (lam A x => x)
                    in (id U))))
    (define ty (infer-empty tm))
    (printf "type of term:~n~n~a~n~nis~n~n~a~n" tm (readback '() ty))))
diff --git a/parse.rkt b/parse.rkt
@@ -1,16 +1,20 @@
 #lang racket
 (provide parse)
 (require syntax/parse
+         syntax/stx
          "term.rkt")
 
 (define (parse stx)
   (syntax-parse stx
     #:datum-literals (U
-                      lam
-                      Pi :
-                      ->
+                      λ lam =>
+                      : ->
                       let = in)
     [U (Univ)]
+    [((~or λ lam) x ...+ => t)
+     (foldr (λ (x t) (Lam x t))
+            (parse #'t)
+            (stx-map syntax->datum #'(x ...)))]
     [(lam x t) (Lam (syntax->datum #'x) (parse #'t))]
     [(let x : a = t in u) (Let (syntax->datum #'x) (parse #'a) (parse #'t) (parse #'u))]
     [((x : a) -> b) (Pi (syntax->datum #'x) (parse #'a) (parse #'b))]