From a3433b919356338de38cbe9a05e0db5c61a07994 Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Wed, 12 Oct 2016 14:10:03 -0400 Subject: [PATCH] remove * version of pattern expanders --- macrotypes/examples/exist.rkt | 2 +- macrotypes/examples/stlc+rec-iso.rkt | 4 ++-- macrotypes/typecheck.rkt | 32 ++++++---------------------- turnstile/examples/exist.rkt | 2 +- turnstile/examples/stlc+rec-iso.rkt | 4 ++-- 5 files changed, 12 insertions(+), 32 deletions(-) diff --git a/macrotypes/examples/exist.rkt b/macrotypes/examples/exist.rkt index 47370ef..359ece2 100644 --- a/macrotypes/examples/exist.rkt +++ b/macrotypes/examples/exist.rkt @@ -15,7 +15,7 @@ (define-typed-syntax pack [(_ (τ:type e) as ∃τ:type) - #:with (~∃* (τ_abstract) τ_body) #'∃τ.norm + #:with (~∃ (τ_abstract) τ_body) #'∃τ.norm #:with [e- τ_e] (infer+erase #'e) #:when (typecheck? #'τ_e (subst #'τ.norm #'τ_abstract #'τ_body)) (⊢ e- : ∃τ.norm)]) diff --git a/macrotypes/examples/stlc+rec-iso.rkt b/macrotypes/examples/stlc+rec-iso.rkt index e4350de..5669b55 100644 --- a/macrotypes/examples/stlc+rec-iso.rkt +++ b/macrotypes/examples/stlc+rec-iso.rkt @@ -18,13 +18,13 @@ (define-typed-syntax unfld [(_ τ:type-ann e) - #:with (~μ* (tv) τ_body) #'τ.norm + #:with (~μ (tv) τ_body) #'τ.norm #:with [e- τ_e] (infer+erase #'e) #:when (typecheck? #'τ_e #'τ.norm) (⊢ e- : #,(subst #'τ.norm #'tv #'τ_body))]) (define-typed-syntax fld [(_ τ:type-ann e) - #:with (~μ* (tv) τ_body) #'τ.norm + #:with (~μ (tv) τ_body) #'τ.norm #:with [e- τ_e] (infer+erase #'e) #:when (typecheck? #'τ_e (subst #'τ.norm #'tv #'τ_body)) (⊢ e- : τ.norm)]) diff --git a/macrotypes/typecheck.rkt b/macrotypes/typecheck.rkt index 4c67dc2..381c4d7 100644 --- a/macrotypes/typecheck.rkt +++ b/macrotypes/typecheck.rkt @@ -61,7 +61,6 @@ (begin-for-syntax (define (mk-? id) (format-id id "~a?" id)) - (define (mk-* id) (format-id id "~a*" id)) (define (mk-~ id) (format-id id "~~~a" id)) (define-for-syntax (mk-? id) (format-id id "~a?" id)) (define-for-syntax (mk-~ id) (format-id id "~~~a" id)) @@ -595,7 +594,6 @@ (define (get-type-tags ts) (stx-map get-type-tag ts))) - (define-syntax define-basic-checked-id-stx (syntax-parser #:datum-literals (:) [(_ τ:id : kind) @@ -656,7 +654,6 @@ #:with τ-internal (generate-temporary #'τ) #:with τ? (mk-? #'τ) #:with τ-expander (mk-~ #'τ) - #:with τ-expander* (mk-* #'τ-expander) #`(begin (begin-for-syntax (define-syntax τ-expander @@ -689,19 +686,6 @@ #'expanded-τ) bvs-pat . pat))]))) - (define-syntax τ-expander* - (pattern-expander - (syntax-parser - [(_ . pat) - #'(~or - (τ-expander . pat) - (~and - any - (~do - (type-error #:src #'any - #:msg - "Expected ~a type, got: ~a" - #'τ #'any))))]))) (define arg-variances arg-variances-stx) (define (τ? t) (syntax-parse t @@ -772,8 +756,6 @@ #:with same-names? (format-id #'name "same-~as?" #'name) #:with name-out (format-id #'name "~a-out" #'name) #'(begin - ;; (provide (for-syntax current-is-name? is-name? #%tag? mk-name name name-bind name-ann name-ctx same-names?) - ;; #%tag define-base-name define-base-names define-name-cons) (define #%tag void) (begin-for-syntax (define (#%tag? t) (and (identifier? t) (free-identifier=? t #'#%tag))) @@ -806,19 +788,17 @@ (pattern ((~var || name-bind) (... ...)))) (define-syntax-class name-ann ; type instantiation #:attributes (norm) - (pattern stx - #:when (stx-pair? #'stx) - #:when (brace? #'stx) - #:with ((~var t name)) #'stx + (pattern (~and (_) + (~fail #:unless (brace? this-syntax)) + ((~var t name) ~!)) #:attr norm (delay #'t.norm)) (pattern any #:fail-when #t - (type-error #:src #'any #:msg - (format - (string-append + (format + (string-append "Improperly formatted ~a annotation: ~a; should have shape {τ}, " "where τ is a valid ~a.") - 'name (type->str #'any) 'name)) + 'name (type->str #'any) 'name) #:attr norm #f)) (define (name=? t1 t2) ;(printf "(τ=) t1 = ~a\n" #;τ1 (syntax->datum t1)) diff --git a/turnstile/examples/exist.rkt b/turnstile/examples/exist.rkt index 58196d0..5e9b48c 100644 --- a/turnstile/examples/exist.rkt +++ b/turnstile/examples/exist.rkt @@ -14,7 +14,7 @@ (define-type-constructor ∃ #:bvs = 1) (define-typed-syntax (pack (τ:type e) as ∃τ:type) ≫ - #:with (~∃* (τ_abstract) τ_body) #'∃τ.norm + #:with (~∃ (τ_abstract) τ_body) #'∃τ.norm #:with τ_e (subst #'τ.norm #'τ_abstract #'τ_body) [⊢ e ≫ e- ⇐ τ_e] -------- diff --git a/turnstile/examples/stlc+rec-iso.rkt b/turnstile/examples/stlc+rec-iso.rkt index ef77543..d5fe9c1 100644 --- a/turnstile/examples/stlc+rec-iso.rkt +++ b/turnstile/examples/stlc+rec-iso.rkt @@ -17,12 +17,12 @@ (define-type-constructor μ #:bvs = 1) (define-typed-syntax (unfld τ:type-ann e) ≫ - #:with (~μ* (tv) τ_body) #'τ.norm + #:with (~μ (tv) τ_body) #'τ.norm [⊢ e ≫ e- ⇐ τ.norm] -------- [⊢ e- ⇒ #,(subst #'τ.norm #'tv #'τ_body)]) (define-typed-syntax (fld τ:type-ann e) ≫ - #:with (~μ* (tv) τ_body) #'τ.norm + #:with (~μ (tv) τ_body) #'τ.norm #:with τ_e (subst #'τ.norm #'tv #'τ_body) [⊢ e ≫ e- ⇐ τ_e] --------