From e33437643340d4b7a01601476ec65c8d9f3e3abe Mon Sep 17 00:00:00 2001 From: "William J. Bowman" Date: Tue, 22 Mar 2016 13:16:30 -0400 Subject: [PATCH] Syntax parse in redex-lang forms For better errors and more robust extensions --- cur-lib/cur/curnel/redex-lang.rkt | 23 +++++++++++++---------- 1 file changed, 13 insertions(+), 10 deletions(-) diff --git a/cur-lib/cur/curnel/redex-lang.rkt b/cur-lib/cur/curnel/redex-lang.rkt index 6b200d8..34dbcd7 100644 --- a/cur-lib/cur/curnel/redex-lang.rkt +++ b/cur-lib/cur/curnel/redex-lang.rkt @@ -410,8 +410,9 @@ ;; ;; TODO: Can these be simplified further? (define-syntax (dep-lambda syn) - (syntax-case syn (:) - [(_ (x : t) e) + (syntax-parse syn + #:datum-literals (:) + [(_ (x:id : t) e) (syntax->curnel-syntax (quasisyntax/loc syn (λ (x : t) e)))])) @@ -422,28 +423,30 @@ (quasisyntax/loc syn (#%app e1 e2)))])) (define-syntax (dep-forall syn) - (syntax-case syn (:) - [(_ (x : t) e) + (syntax-parse syn + #:datum-literals (:) + [(_ (x:id : t) e) (syntax->curnel-syntax (quasisyntax/loc syn (Π (x : t) e)))])) (define-syntax (Type syn) - (syntax-case syn () - [(_ i) + (syntax-parse syn + [(_ i:nat) (syntax->curnel-syntax (quasisyntax/loc syn (Unv i)))] [_ (quasisyntax/loc syn (Type 0))])) (define-syntax (dep-inductive syn) - (syntax-case syn (:) - [(_ i : ti (x1 : t1) ...) + (syntax-parse syn + #:datum-literals (:) + [(_ i:id : ti (x1:id : t1) ...) (begin (extend-Δ/syn! delta #'i #'ti #'((x1 : t1) ...)) #'(void))])) (define-syntax (dep-elim syn) - (syntax-case syn () - [(_ D T) + (syntax-parse syn + [(_ D:id T) (syntax->curnel-syntax (quasisyntax/loc syn (elim D T)))]))