From d0c14c7e079c2eae046e43cda165e6d4f4ca5836 Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Thu, 22 Sep 2016 16:56:48 -0400 Subject: [PATCH] define-typed-syntax: support define-simple-macro-like single-clause syntax --- turnstile/examples/exist.rkt | 27 ++++----- turnstile/examples/ext-stlc.rkt | 18 +++--- turnstile/examples/fomega.rkt | 50 +++++++--------- turnstile/examples/fomega2.rkt | 22 ++++--- turnstile/examples/fsub.rkt | 39 ++++++------ turnstile/examples/stlc+box.rkt | 29 ++++----- turnstile/examples/stlc+cons.rkt | 90 +++++++++++++--------------- turnstile/examples/stlc+effect.rkt | 42 +++++++------ turnstile/examples/stlc+rec-iso.rkt | 24 ++++---- turnstile/examples/stlc+reco+var.rkt | 47 +++++++-------- turnstile/examples/stlc+tup.rkt | 11 ++-- turnstile/examples/stlc.rkt | 24 ++++---- turnstile/examples/sysf.rkt | 9 ++- turnstile/turnstile.rkt | 6 ++ 14 files changed, 205 insertions(+), 233 deletions(-) diff --git a/turnstile/examples/exist.rkt b/turnstile/examples/exist.rkt index 3ee71ab..4e88a45 100644 --- 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 index cfd1182..0daba41 100644 --- 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 (and e ...) ≫ + [⊢ e ≫ e- ⇐ Bool] ... + -------- + [⊢ (and- e- ...) ⇒ Bool]) -(define-typed-syntax or - [(_ e ...) ≫ - [⊢ e ≫ e- ⇐ Bool] ... - -------- - [⊢ (or- 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 index 727d427..82cc637 100644 --- 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 index 7ec1343..f2ac63a 100644 --- 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 index 5e5a791..bcd43f2 100644 --- 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 index af9755a..5330372 100644 --- 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 index 324ff13..a60cd78 100644 --- 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 index 1b21b3d..9b70c76 100644 --- 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 index 1eb8b92..78c6b58 100644 --- 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 index 4abe493..3ff715f 100644 --- 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 index 39582db..5b6ac5d 100644 --- 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 index cef703e..6a40b5d 100644 --- 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 index a256a32..c6dc0b8 100644 --- 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 index a6c4382..8dbccb0 100644 --- 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