commit a3433b919356338de38cbe9a05e0db5c61a07994
parent 299051e9029e050df34dac3b93bf179e787734e6
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Wed, 12 Oct 2016 14:10:03 -0400
remove * version of pattern expanders
Diffstat:
5 files changed, 12 insertions(+), 32 deletions(-)
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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]
--------
