commit d0c14c7e079c2eae046e43cda165e6d4f4ca5836
parent bce55e8741cfb05ce36feb14d528763474be6abc
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Thu, 22 Sep 2016 16:56:48 -0400
define-typed-syntax: support define-simple-macro-like single-clause syntax
Diffstat:
14 files changed, 206 insertions(+), 234 deletions(-)
diff --git a/turnstile/examples/exist.rkt b/turnstile/examples/exist.rkt
@@ -14,16 +14,15 @@
(define-type-constructor ∃ #:bvs = 1)
-(define-typed-syntax pack
- [(_ (τ:type e) as ∃τ:type) ≫
- #:with (~∃* (τ_abstract) τ_body) #'∃τ.norm
- #:with τ_e (subst #'τ.norm #'τ_abstract #'τ_body)
- [⊢ e ≫ e- ⇐ τ_e]
- --------
- [⊢ e- ⇒ ∃τ.norm]])
+(define-typed-syntax (pack (τ:type e) as ∃τ:type) ≫
+ #:with (~∃* (τ_abstract) τ_body) #'∃τ.norm
+ #:with τ_e (subst #'τ.norm #'τ_abstract #'τ_body)
+ [⊢ e ≫ e- ⇐ τ_e]
+ --------
+ [⊢ e- ⇒ ∃τ.norm])
-(define-typed-syntax open #:datum-literals (<= with)
- [(_ [x:id <= e_packed with X:id] e) ≫
+(define-typed-syntax
+ (open [x:id (~datum <=) e_packed (~datum with) X:id] e) ≫
;; The subst below appears to be a hack, but it's not really.
;; It's the (TaPL) type rule itself that is fast and loose.
;; Leveraging the macro system's management of binding reveals this.
@@ -67,8 +66,8 @@
;; ------------------------------
;; Γ ⊢ (open [x <= e_packed with X_2] e) : τ_e
;;
- [⊢ e_packed ≫ e_packed- ⇒ (~∃ (Y) τ_body)]
- #:with τ_x (subst #'X #'Y #'τ_body)
- [([X ≫ X- : #%type]) ([x ≫ x- : τ_x]) ⊢ e ≫ e- ⇒ τ_e]
- --------
- [⊢ (let- ([x- e_packed-]) e-) ⇒ τ_e]])
+ [⊢ e_packed ≫ e_packed- ⇒ (~∃ (Y) τ_body)]
+ #:with τ_x (subst #'X #'Y #'τ_body)
+ [([X ≫ X- : #%type]) ([x ≫ x- : τ_x]) ⊢ e ≫ e- ⇒ τ_e]
+ --------
+ [⊢ (let- ([x- e_packed-]) e-) ⇒ τ_e])
diff --git a/turnstile/examples/ext-stlc.rkt b/turnstile/examples/ext-stlc.rkt
@@ -48,17 +48,15 @@
(define-primop sub1 : (→ Int Int))
(define-primop not : (→ Bool Bool))
-(define-typed-syntax and
- [(_ e ...) ≫
- [⊢ e ≫ e- ⇐ Bool] ...
- --------
- [⊢ (and- e- ...) ⇒ Bool]])
-
-(define-typed-syntax or
- [(_ e ...) ≫
- [⊢ e ≫ e- ⇐ Bool] ...
- --------
- [⊢ (or- e- ...) ⇒ Bool]])
+(define-typed-syntax (and e ...) ≫
+ [⊢ e ≫ e- ⇐ Bool] ...
+ --------
+ [⊢ (and- e- ...) ⇒ Bool])
+
+(define-typed-syntax (or e ...) ≫
+ [⊢ e ≫ e- ⇐ Bool] ...
+ --------
+ [⊢ (or- e- ...) ⇒ Bool])
(begin-for-syntax
(define current-join
diff --git a/turnstile/examples/fomega.rkt b/turnstile/examples/fomega.rkt
@@ -82,35 +82,31 @@
(current-type=? type=?)
(current-typecheck-relation (current-type=?)))
-(define-typed-syntax Λ
- [(_ bvs:kind-ctx e) ≫
- [([bvs.x ≫ tv- : bvs.kind] ...) () ⊢ e ≫ e- ⇒ τ_e]
- --------
- [⊢ e- ⇒ (∀ ([tv- : bvs.kind] ...) τ_e)]])
+(define-typed-syntax (Λ bvs:kind-ctx e) ≫
+ [([bvs.x ≫ tv- : bvs.kind] ...) () ⊢ e ≫ e- ⇒ τ_e]
+ --------
+ [⊢ e- ⇒ (∀ ([tv- : bvs.kind] ...) τ_e)])
-(define-typed-syntax inst
- [(_ e τ ...) ≫
- [⊢ e ≫ e- ⇒ : (~∀ (tv ...) τ_body) (⇒ : (~∀★ k ...))]
- [⊢ τ ≫ τ- ⇐ k] ...
- #:with τ-inst (substs #'(τ- ...) #'(tv ...) #'τ_body)
- --------
- [⊢ e- ⇒ τ-inst]])
+(define-typed-syntax (inst e τ ...) ≫
+ [⊢ e ≫ e- ⇒ : (~∀ (tv ...) τ_body) (⇒ : (~∀★ k ...))]
+ [⊢ τ ≫ τ- ⇐ k] ...
+ #:with τ-inst (substs #'(τ- ...) #'(tv ...) #'τ_body)
+ --------
+ [⊢ e- ⇒ τ-inst])
;; TODO: merge with regular λ and app?
;; - see fomega2.rkt
-(define-typed-syntax tyλ
- [(_ bvs:kind-ctx τ_body) ≫
- [[bvs.x ≫ tv- : bvs.kind] ... ⊢ τ_body ≫ τ_body- ⇒ k_body]
- #:fail-unless ((current-kind?) #'k_body)
- (format "not a valid type: ~a\n" (type->str #'τ_body))
- --------
- [⊢ (λ- (tv- ...) τ_body-) ⇒ (⇒ bvs.kind ... k_body)]])
+(define-typed-syntax (tyλ bvs:kind-ctx τ_body) ≫
+ [[bvs.x ≫ tv- : bvs.kind] ... ⊢ τ_body ≫ τ_body- ⇒ k_body]
+ #:fail-unless ((current-kind?) #'k_body)
+ (format "not a valid type: ~a\n" (type->str #'τ_body))
+ --------
+ [⊢ (λ- (tv- ...) τ_body-) ⇒ (⇒ bvs.kind ... k_body)])
-(define-typed-syntax tyapp
- [(_ τ_fn τ_arg ...) ≫
- [⊢ τ_fn ≫ τ_fn- ⇒ (~⇒ k_in ... k_out)]
- #:fail-unless (stx-length=? #'[k_in ...] #'[τ_arg ...])
- (num-args-fail-msg #'τ_fn #'[k_in ...] #'[τ_arg ...])
- [⊢ τ_arg ≫ τ_arg- ⇐ k_in] ...
- --------
- [⊢ (#%app- τ_fn- τ_arg- ...) ⇒ k_out]])
+(define-typed-syntax (tyapp τ_fn τ_arg ...) ≫
+ [⊢ τ_fn ≫ τ_fn- ⇒ (~⇒ k_in ... k_out)]
+ #:fail-unless (stx-length=? #'[k_in ...] #'[τ_arg ...])
+ (num-args-fail-msg #'τ_fn #'[k_in ...] #'[τ_arg ...])
+ [⊢ τ_arg ≫ τ_arg- ⇐ k_in] ...
+ --------
+ [⊢ (#%app- τ_fn- τ_arg- ...) ⇒ k_out])
diff --git a/turnstile/examples/fomega2.rkt b/turnstile/examples/fomega2.rkt
@@ -78,17 +78,15 @@
(current-type=? type=?)
(current-typecheck-relation (current-type=?)))
-(define-typed-syntax Λ
- [(_ bvs:kind-ctx e) ≫
- [[bvs.x ≫ tv- : bvs.kind] ... ⊢ e ≫ e- ⇒ τ_e]
- --------
- [⊢ e- ⇒ (∀ ([tv- : bvs.kind] ...) τ_e)]])
+(define-typed-syntax (Λ bvs:kind-ctx e) ≫
+ [[bvs.x ≫ tv- : bvs.kind] ... ⊢ e ≫ e- ⇒ τ_e]
+ --------
+ [⊢ e- ⇒ (∀ ([tv- : bvs.kind] ...) τ_e)])
-(define-typed-syntax inst
- [(_ e τ ...) ≫
- [⊢ e ≫ e- ⇒ : (~∀ (tv ...) τ_body) (⇒ : (~∀★ k ...))]
- [⊢ τ ≫ τ- ⇐ k] ...
- #:with τ-inst (substs #'(τ- ...) #'(tv ...) #'τ_body)
- --------
- [⊢ e- ⇒ τ-inst]])
+(define-typed-syntax (inst e τ ...) ≫
+ [⊢ e ≫ e- ⇒ : (~∀ (tv ...) τ_body) (⇒ : (~∀★ k ...))]
+ [⊢ τ ≫ τ- ⇐ k] ...
+ #:with τ-inst (substs #'(τ- ...) #'(tv ...) #'τ_body)
+ --------
+ [⊢ e- ⇒ τ-inst])
diff --git a/turnstile/examples/fsub.rkt b/turnstile/examples/fsub.rkt
@@ -44,11 +44,10 @@
;; 2) instantiation of ∀
;; Problem: need type annotations, even in expanded form
;; Solution: store type annotations in a (quasi) kind <:
-(define-typed-syntax ∀ #:datum-literals (<:)
- [(_ ([tv:id <: τ:type] ...) τ_body) ≫
- --------
- ; eval first to overwrite the old #%type
- [⊢ #,((current-type-eval) #'(sysf:∀ (tv ...) τ_body)) ⇒ (<: τ.norm ...)]])
+(define-typed-syntax (∀ ([tv:id (~datum <:) τ:type] ...) τ_body) ≫
+ --------
+ ; eval first to overwrite the old #%type
+ [⊢ #,((current-type-eval) #'(sysf:∀ (tv ...) τ_body)) ⇒ (<: τ.norm ...)])
(begin-for-syntax
(define-syntax ~∀
(pattern-expander
@@ -73,20 +72,18 @@
#:src #'any
#:msg "Expected ∀ type, got: ~a" #'any))))]))))
-(define-typed-syntax Λ #:datum-literals (<:)
- [(_ ([tv:id <: τsub:type] ...) e) ≫
- ;; NOTE: store the subtyping relation of tv and τsub in the
- ;; environment with a syntax property using another tag: '<:
- ;; The "expose" function looks for this tag to enforce the bound,
- ;; as in TaPL (fig 28-1)
- [([tv ≫ tv- : #%type <: τsub] ...) () ⊢ e ≫ e- ⇒ τ_e]
- --------
- [⊢ e- ⇒ (∀ ([tv- <: τsub] ...) τ_e)]])
-(define-typed-syntax inst
- [(_ e τ:type ...) ≫
- [⊢ e ≫ e- ⇒ (~∀ ([tv <: τ_sub] ...) τ_body)]
- [τ.norm τ⊑ τ_sub #:for τ] ...
- #:with τ_inst (substs #'(τ.norm ...) #'(tv ...) #'τ_body)
- --------
- [⊢ e- ⇒ τ_inst]])
+(define-typed-syntax (Λ ([tv:id (~datum <:) τsub:type] ...) e) ≫
+ ;; NOTE: store the subtyping relation of tv and τsub in the
+ ;; environment with a syntax property using another tag: '<:
+ ;; The "expose" function looks for this tag to enforce the bound,
+ ;; as in TaPL (fig 28-1)
+ [([tv ≫ tv- : #%type <: τsub] ...) () ⊢ e ≫ e- ⇒ τ_e]
+ --------
+ [⊢ e- ⇒ (∀ ([tv- <: τsub] ...) τ_e)])
+(define-typed-syntax (inst e τ:type ...) ≫
+ [⊢ e ≫ e- ⇒ (~∀ ([tv <: τ_sub] ...) τ_body)]
+ [τ.norm τ⊑ τ_sub #:for τ] ...
+ #:with τ_inst (substs #'(τ.norm ...) #'(tv ...) #'τ_body)
+ --------
+ [⊢ e- ⇒ τ_inst])
diff --git a/turnstile/examples/stlc+box.rkt b/turnstile/examples/stlc+box.rkt
@@ -11,22 +11,19 @@
(define-type-constructor Ref)
-(define-typed-syntax ref
- [(_ e) ≫
- [⊢ e ≫ e- ⇒ τ]
- --------
- [⊢ (box- e-) ⇒ (Ref τ)]])
+(define-typed-syntax (ref e) ≫
+ [⊢ e ≫ e- ⇒ τ]
+ --------
+ [⊢ (box- e-) ⇒ (Ref τ)])
-(define-typed-syntax deref
- [(_ e) ≫
- [⊢ e ≫ e- ⇒ (~Ref τ)]
- --------
- [⊢ (unbox- e-) ⇒ τ]])
+(define-typed-syntax (deref e) ≫
+ [⊢ e ≫ e- ⇒ (~Ref τ)]
+ --------
+ [⊢ (unbox- e-) ⇒ τ])
-(define-typed-syntax := #:literals (:=)
- [(_ e_ref e) ≫
- [⊢ e_ref ≫ e_ref- ⇒ (~Ref τ)]
- [⊢ e ≫ e- ⇐ τ]
- --------
- [⊢ (set-box!- e_ref- e-) ⇒ Unit]])
+(define-typed-syntax (:= e_ref e) ≫
+ [⊢ e_ref ≫ e_ref- ⇒ (~Ref τ)]
+ [⊢ e ≫ e- ⇐ τ]
+ --------
+ [⊢ (set-box!- e_ref- e-) ⇒ Unit])
diff --git a/turnstile/examples/stlc+cons.rkt b/turnstile/examples/stlc+cons.rkt
@@ -20,29 +20,25 @@
[:id ⇐ (~List τ) ≫
--------
[⊢ null-]])
-(define-typed-syntax cons
- [(cons e1 e2) ≫
- [⊢ e1 ≫ e1- ⇒ τ1]
- [⊢ e2 ≫ e2- ⇐ (List τ1)]
- --------
- [⊢ _ ≫ (cons- e1- e2-) ⇒ (List τ1)]])
-(define-typed-syntax isnil
- [(_ e) ≫
- [⊢ e ≫ e- ⇒ (~List _)]
- --------
- [⊢ (null?- e-) ⇒ Bool]])
-(define-typed-syntax head
- [(_ e) ≫
- [⊢ e ≫ e- ⇒ (~List τ)]
- --------
- [⊢ (car- e-) ⇒ τ]])
-(define-typed-syntax tail
- [(_ e) ≫
- [⊢ e ≫ e- ⇒ τ-lst]
- #:fail-unless (List? #'τ-lst)
- (format "Expected a list type, got: ~a" (type->str #'τ-lst))
- --------
- [⊢ (cdr- e-) ⇒ τ-lst]])
+(define-typed-syntax (cons e1 e2) ≫
+ [⊢ e1 ≫ e1- ⇒ τ1]
+ [⊢ e2 ≫ e2- ⇐ (List τ1)]
+ --------
+ [⊢ (cons- e1- e2-) ⇒ (List τ1)])
+(define-typed-syntax (isnil e) ≫
+ [⊢ e ≫ e- ⇒ (~List _)]
+ --------
+ [⊢ (null?- e-) ⇒ Bool])
+(define-typed-syntax (head e) ≫
+ [⊢ e ≫ e- ⇒ (~List τ)]
+ --------
+ [⊢ (car- e-) ⇒ τ])
+(define-typed-syntax (tail e) ≫
+ [⊢ e ≫ e- ⇒ τ-lst]
+ #:fail-unless (List? #'τ-lst)
+ (format "Expected a list type, got: ~a" (type->str #'τ-lst))
+ --------
+ [⊢ (cdr- e-) ⇒ τ-lst])
(define-typed-syntax list
[(_) ≫
--------
@@ -53,29 +49,25 @@
[(_ x . rst) ≫ ; no expected type
--------
[≻ (cons x (list . rst))]])
-(define-typed-syntax reverse
- [(_ e) ≫
- [⊢ e ≫ e- ⇒ τ-lst]
- #:fail-unless (List? #'τ-lst)
- (format "Expected a list type, got: ~a" (type->str #'τ-lst))
- --------
- [⊢ (reverse- e-) ⇒ τ-lst]])
-(define-typed-syntax length
- [(_ e) ≫
- [⊢ e ≫ e- ⇒ τ-lst]
- #:fail-unless (List? #'τ-lst)
- (format "Expected a list type, got: ~a" (type->str #'τ-lst))
- --------
- [⊢ (length- e-) ⇒ Int]])
-(define-typed-syntax list-ref
- [(_ e n) ≫
- [⊢ e ≫ e- ⇒ (~List τ)]
- [⊢ n ≫ n- ⇐ Int]
- --------
- [⊢ (list-ref- e- n-) ⇒ τ]])
-(define-typed-syntax member
- [(_ v e) ≫
- [⊢ e ≫ e- ⇒ (~List τ)]
- [⊢ v ≫ v- ⇐ τ]
- --------
- [⊢ (member- v- e-) ⇒ Bool]])
+(define-typed-syntax (reverse e) ≫
+ [⊢ e ≫ e- ⇒ τ-lst]
+ #:fail-unless (List? #'τ-lst)
+ (format "Expected a list type, got: ~a" (type->str #'τ-lst))
+ --------
+ [⊢ (reverse- e-) ⇒ τ-lst])
+(define-typed-syntax (length e) ≫
+ [⊢ e ≫ e- ⇒ τ-lst]
+ #:fail-unless (List? #'τ-lst)
+ (format "Expected a list type, got: ~a" (type->str #'τ-lst))
+ --------
+ [⊢ (length- e-) ⇒ Int])
+(define-typed-syntax (list-ref e n) ≫
+ [⊢ e ≫ e- ⇒ (~List τ)]
+ [⊢ n ≫ n- ⇐ Int]
+ --------
+ [⊢ (list-ref- e- n-) ⇒ τ])
+(define-typed-syntax (member v e) ≫
+ [⊢ e ≫ e- ⇒ (~List τ)]
+ [⊢ v ≫ v- ⇐ τ]
+ --------
+ [⊢ (member- v- e-) ⇒ Bool])
diff --git a/turnstile/examples/stlc+effect.rkt b/turnstile/examples/stlc+effect.rkt
@@ -31,21 +31,20 @@
(define-typed-syntax effect:#%app #:export-as #%app
[(_ efn e ...) ≫
[⊢ efn ≫ e_fn-
- (⇒ : (~→ τ_in ... τ_out)
- (⇒ ν (~locs tyns ...))
- (⇒ := (~locs tyas ...))
- (⇒ ! (~locs tyds ...)))
- (⇒ ν (~locs fns ...))
- (⇒ := (~locs fas ...))
- (⇒ ! (~locs fds ...))]
+ (⇒ : (~→ τ_in ... τ_out)
+ (⇒ ν (~locs tyns ...))
+ (⇒ := (~locs tyas ...))
+ (⇒ ! (~locs tyds ...)))
+ (⇒ ν (~locs fns ...))
+ (⇒ := (~locs fas ...))
+ (⇒ ! (~locs fds ...))]
#:fail-unless (stx-length=? #'[e ...] #'[τ_in ...])
(num-args-fail-msg #'efn #'[τ_in ...] #'[e ...])
- [⊢ [e ≫ e_arg-
+ [⊢ e ≫ e_arg-
(⇐ : τ_in)
(⇒ ν (~locs ns ...))
(⇒ := (~locs as ...))
- (⇒ ! (~locs ds ...))]
- ...]
+ (⇒ ! (~locs ds ...))] ...
--------
[⊢ (#%app- e_fn- e_arg- ...)
(⇒ : τ_out)
@@ -53,20 +52,19 @@
(⇒ := (locs fas ... tyas ... as ... ...))
(⇒ ! (locs fds ... tyds ... ds ... ...))]])
-(define-typed-syntax λ
- [(_ bvs:type-ctx e) ≫
- [[bvs.x ≫ x- : bvs.type] ... ⊢
- e ≫ e-
- (⇒ : τ_res)
- (⇒ ν (~locs ns ...))
- (⇒ := (~locs as ...))
- (⇒ ! (~locs ds ...))]
- --------
- [⊢ (λ- (x- ...) e-)
- (⇒ : (→ bvs.type ... τ_res)
+(define-typed-syntax (λ bvs:type-ctx e) ≫
+ [[bvs.x ≫ x- : bvs.type] ...
+ ⊢ e ≫ e-
+ (⇒ : τ_res)
+ (⇒ ν (~locs ns ...))
+ (⇒ := (~locs as ...))
+ (⇒ ! (~locs ds ...))]
+ --------
+ [⊢ (λ- (x- ...) e-)
+ (⇒ : (→ bvs.type ... τ_res)
(⇒ ν (locs ns ...))
(⇒ := (locs as ...))
- (⇒ ! (locs ds ...)))]])
+ (⇒ ! (locs ds ...)))])
(define-type-constructor Ref)
diff --git a/turnstile/examples/stlc+rec-iso.rkt b/turnstile/examples/stlc+rec-iso.rkt
@@ -36,16 +36,14 @@
(current-type=? type=?)
(current-typecheck-relation type=?))
-(define-typed-syntax unfld
- [(_ τ:type-ann e) ≫
- #:with (~μ* (tv) τ_body) #'τ.norm
- [⊢ e ≫ e- ⇐ τ.norm]
- --------
- [⊢ e- ⇒ #,(subst #'τ.norm #'tv #'τ_body)]])
-(define-typed-syntax fld
- [(_ τ:type-ann e) ≫
- #:with (~μ* (tv) τ_body) #'τ.norm
- #:with τ_e (subst #'τ.norm #'tv #'τ_body)
- [⊢ e ≫ e- ⇐ τ_e]
- --------
- [⊢ e- ⇒ τ.norm]])
+(define-typed-syntax (unfld τ:type-ann e) ≫
+ #:with (~μ* (tv) τ_body) #'τ.norm
+ [⊢ e ≫ e- ⇐ τ.norm]
+ --------
+ [⊢ e- ⇒ #,(subst #'τ.norm #'tv #'τ_body)])
+(define-typed-syntax (fld τ:type-ann e) ≫
+ #:with (~μ* (tv) τ_body) #'τ.norm
+ #:with τ_e (subst #'τ.norm #'tv #'τ_body)
+ [⊢ e ≫ e- ⇐ τ_e]
+ --------
+ [⊢ e- ⇒ τ.norm])
diff --git a/turnstile/examples/stlc+reco+var.rkt b/turnstile/examples/stlc+reco+var.rkt
@@ -87,20 +87,18 @@
(add-orig res (get-orig res))])))
;; records
-(define-typed-syntax tup #:datum-literals (=)
- [(_ [l:id = e] ...) ≫
- [⊢ e ≫ e- ⇒ τ] ...
- --------
- [⊢ (list- (list- 'l e-) ...) ⇒ (× [l : τ] ...)]])
-(define-typed-syntax proj #:literals (quote)
- [(_ e_rec l:id) ≫
- [⊢ e_rec ≫ e_rec- ⇒ τ_e]
- #:fail-unless (×? #'τ_e)
- (format "Expected expression ~s to have × type, got: ~a"
- (syntax->datum #'e_rec) (type->str #'τ_e))
- #:with τ_l (×-ref #'τ_e #'l)
- --------
- [⊢ (cadr- (assoc- 'l e_rec-)) ⇒ τ_l]])
+(define-typed-syntax (tup [l:id (~datum =) e] ...) ≫
+ [⊢ e ≫ e- ⇒ τ] ...
+ --------
+ [⊢ (list- (list- 'l e-) ...) ⇒ (× [l : τ] ...)])
+(define-typed-syntax (proj e_rec l:id) ≫
+ [⊢ e_rec ≫ e_rec- ⇒ τ_e]
+ #:fail-unless (×? #'τ_e)
+ (format "Expected expression ~s to have × type, got: ~a"
+ (syntax->datum #'e_rec) (type->str #'τ_e))
+ #:with τ_l (×-ref #'τ_e #'l)
+ --------
+ [⊢ (cadr- (assoc- 'l e_rec-)) ⇒ τ_l])
(define-type-constructor ∨/internal #:arity >= 0)
@@ -161,14 +159,13 @@
--------
[⊢ (list- 'l e)]])
-(define-typed-syntax case #:datum-literals (of =>)
- [(_ e [l:id x:id => e_l] ...) ≫
- #:fail-unless (not (null? (syntax->list #'(l ...)))) "no clauses"
- [⊢ e ≫ e- ⇒ (~∨* [l_x : τ_x] ...)]
- #:fail-unless (stx-length=? #'(l ...) #'(l_x ...)) "wrong number of case clauses"
- #:fail-unless (typechecks? #'(l ...) #'(l_x ...)) "case clauses not exhaustive"
- [[x ≫ x- : τ_x] ⊢ e_l ≫ e_l- ⇒ τ_el] ...
- --------
- [⊢ (let- ([l_e (car- e-)])
- (cond- [(symbol=?- l_e 'l) (let- ([x- (cadr- e-)]) e_l-)] ...))
- ⇒ (⊔ τ_el ...)]])
+(define-typed-syntax (case e [l:id x:id (~datum =>) e_l] ...) ≫
+ #:fail-unless (not (null? (syntax->list #'(l ...)))) "no clauses"
+ [⊢ e ≫ e- ⇒ (~∨* [l_x : τ_x] ...)]
+ #:fail-unless (stx-length=? #'(l ...) #'(l_x ...)) "wrong number of case clauses"
+ #:fail-unless (typechecks? #'(l ...) #'(l_x ...)) "case clauses not exhaustive"
+ [[x ≫ x- : τ_x] ⊢ e_l ≫ e_l- ⇒ τ_el] ...
+ --------
+ [⊢ (let- ([l_e (car- e-)])
+ (cond- [(symbol=?- l_e 'l) (let- ([x- (cadr- e-)]) e_l-)] ...))
+ ⇒ (⊔ τ_el ...)])
diff --git a/turnstile/examples/stlc+tup.rkt b/turnstile/examples/stlc+tup.rkt
@@ -26,10 +26,9 @@
--------
[⊢ (list- e- ...) ⇒ (× τ ...)]])
-(define-typed-syntax proj
- [(_ e_tup n:nat) ≫
- [⊢ e_tup ≫ e_tup- ⇒ (~× τ ...)]
- #:fail-unless (< (syntax-e #'n) (stx-length #'[τ ...])) "index too large"
- --------
- [⊢ (list-ref- e_tup- n) ⇒ #,(stx-list-ref #'[τ ...] (syntax-e #'n))]])
+(define-typed-syntax (proj e_tup n:nat) ≫
+ [⊢ e_tup ≫ e_tup- ⇒ (~× τ ...)]
+ #:fail-unless (< (syntax-e #'n) (stx-length #'[τ ...])) "index too large"
+ --------
+ [⊢ (list-ref- e_tup- n) ⇒ #,(stx-list-ref #'[τ ...] (syntax-e #'n))])
diff --git a/turnstile/examples/stlc.rkt b/turnstile/examples/stlc.rkt
@@ -20,17 +20,15 @@
---------
[⊢ (λ- (x- ...) e-)]])
-(define-typed-syntax #%app
- [(_ e_fn e_arg ...) ≫
- [⊢ e_fn ≫ e_fn- ⇒ (~→ τ_in ... τ_out)]
- #:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...])
- (num-args-fail-msg #'e_fn #'[τ_in ...] #'[e_arg ...])
- [⊢ e_arg ≫ e_arg- ⇐ τ_in] ...
- --------
- [⊢ (#%app- e_fn- e_arg- ...) ⇒ τ_out]])
+(define-typed-syntax (#%app e_fn e_arg ...) ≫
+ [⊢ e_fn ≫ e_fn- ⇒ (~→ τ_in ... τ_out)]
+ #:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...])
+ (num-args-fail-msg #'e_fn #'[τ_in ...] #'[e_arg ...])
+ [⊢ e_arg ≫ e_arg- ⇐ τ_in] ...
+ --------
+ [⊢ (#%app- e_fn- e_arg- ...) ⇒ τ_out])
-(define-typed-syntax ann #:datum-literals (:)
- [(_ e : τ:type) ≫
- [⊢ e ≫ e- ⇐ τ.norm]
- --------
- [⊢ e- ⇒ τ.norm]])
+(define-typed-syntax (ann e (~datum :) τ:type) ≫
+ [⊢ e ≫ e- ⇐ τ.norm]
+ --------
+ [⊢ e- ⇒ τ.norm])
diff --git a/turnstile/examples/sysf.rkt b/turnstile/examples/sysf.rkt
@@ -14,11 +14,10 @@
(define-type-constructor ∀ #:bvs >= 0)
-(define-typed-syntax Λ
- [(_ (tv:id ...) e) ≫
- [([tv ≫ tv- : #%type] ...) () ⊢ e ≫ e- ⇒ τ]
- --------
- [⊢ e- ⇒ (∀ (tv- ...) τ)]])
+(define-typed-syntax (Λ (tv:id ...) e) ≫
+ [([tv ≫ tv- : #%type] ...) () ⊢ e ≫ e- ⇒ τ]
+ --------
+ [⊢ e- ⇒ (∀ (tv- ...) τ)])
(define-typed-syntax inst
[(_ e τ:type ...) ≫
diff --git a/turnstile/turnstile.rkt b/turnstile/turnstile.rkt
@@ -367,6 +367,12 @@
(define-syntax define-typed-syntax
(lambda (stx)
(syntax-parse stx
+ ;; single-clause def
+ [(def (name:id . pats) . rst)
+ ;; cannot always bind name as pat var, eg #%app, so replace with _
+ #:with r:rule #'[(_ . pats) . rst]
+ #'(-define-typed-syntax name r.norm)]
+ ;; multi-clause def
[(def name:id
(~and (~seq kw-stuff ...) :stxparse-kws)
rule:rule
