commit aa0136cf2996c9d9b5e698aaff0f2b7f18e56f18
parent e673527813262d9d8636ad4cb0131aa4c41c9158
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Thu, 18 Aug 2016 14:52:50 -0400
make prop tag optional, defaults to :
Diffstat:
2 files changed, 24 insertions(+), 15 deletions(-)
diff --git a/turnstile/examples/stlc.rkt b/turnstile/examples/stlc.rkt
@@ -29,25 +29,25 @@
(define-typed-syntax λ #:datum-literals (:)
[(λ ([x:id : τ_in:type] ...) e) ≫
- [() ([x ≫ x- : τ_in.norm] ...) ⊢ [e ≫ e- ⇒ : τ_out]]
+ [() ([x ≫ x- : τ_in.norm] ...) ⊢ [e ≫ e- ⇒ τ_out]]
--------
- [⊢ [_ ≫ (λ- (x- ...) e-) ⇒ : (→ τ_in.norm ... τ_out)]]]
- [(λ (x:id ...) e) ⇐ : (~→ τ_in ... τ_out) ≫
- [() ([x ≫ x- : τ_in] ...) ⊢ [e ≫ e- ⇐ : τ_out]]
+ [⊢ [_ ≫ (λ- (x- ...) e-) ⇒ (→ τ_in.norm ... τ_out)]]]
+ [(λ (x:id ...) e) ⇐ (~→ τ_in ... τ_out) ≫
+ [() ([x ≫ x- : τ_in] ...) ⊢ [e ≫ e- ⇐ τ_out]]
--------
- [⊢ [_ ≫ (λ- (x- ...) e-) ⇐ : _]]])
+ [⊢ [_ ≫ (λ- (x- ...) e-) ⇐ _]]])
(define-typed-syntax #%app
[(_ e_fn e_arg ...) ≫
- [⊢ [e_fn ≫ e_fn- ⇒ : (~→ τ_in ... τ_out)]]
+ [⊢ [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] ...]
+ [⊢ [e_arg ≫ e_arg- ⇐ τ_in] ...]
--------
- [⊢ [_ ≫ (#%app- e_fn- e_arg- ...) ⇒ : τ_out]]])
+ [⊢ [_ ≫ (#%app- e_fn- e_arg- ...) ⇒ τ_out]]])
(define-typed-syntax ann #:datum-literals (:)
[(ann e : τ:type) ≫
- [⊢ [e ≫ e- ⇐ : τ.norm]]
+ [⊢ [e ≫ e- ⇐ τ.norm]]
--------
- [⊢ [_ ≫ e- ⇒ : τ.norm]]])
+ [⊢ [_ ≫ e- ⇒ τ.norm]]])
diff --git a/turnstile/turnstile.rkt b/turnstile/turnstile.rkt
@@ -79,7 +79,9 @@
(define-splicing-syntax-class ⇒-prop
#:datum-literals (⇒)
#:attributes (e-pat)
- [pattern (~seq ⇒ tag:id tag-pat (tag-prop:⇒-prop) ...)
+ [pattern (~or (~seq ⇒ tag-pat ; implicit : tag
+ (~parse tag #':) (~parse (tag-prop.e-pat ...) #'()))
+ (~seq ⇒ tag:id tag-pat (tag-prop:⇒-prop) ...)) ; explicit tag
#:with e-tmp (generate-temporary)
#:with e-pat
#'(~and e-tmp
@@ -89,7 +91,11 @@
(define-splicing-syntax-class ⇒-prop/conclusion
#:datum-literals (⇒)
#:attributes (tag tag-expr)
- [pattern (~seq ⇒ tag:id tag-stx (tag-prop:⇒-prop/conclusion) ...)
+ [pattern (~or (~seq ⇒ tag-stx
+ (~parse tag #':)
+ (~parse (tag-prop.tag ...) #'())
+ (~parse (tag-prop.tag-expr ...) #'()))
+ (~seq ⇒ tag:id tag-stx (tag-prop:⇒-prop/conclusion) ...))
#:with tag-expr
(for/fold ([tag-expr #'#`tag-stx])
([k (in-list (syntax->list #'[tag-prop.tag ...]))]
@@ -99,7 +105,8 @@
(define-splicing-syntax-class ⇐-prop
#:datum-literals (⇐ :)
#:attributes (τ-stx e-pat)
- [pattern (~seq ⇐ : τ-stx)
+ [pattern (~or (~seq ⇐ τ-stx)
+ (~seq ⇐ : τ-stx))
#:with e-tmp (generate-temporary)
#:with τ-tmp (generate-temporary)
#:with τ-exp (generate-temporary)
@@ -258,7 +265,8 @@
#'(assign-type body #:tag 'k v)))]
[pattern [⊢ [e-stx]]
#:with :last-clause #'[⊢ [_ ≫ e-stx ⇐ : _]]]
- [pattern [⊢ [pat* ≫ e-stx ⇐ : τ-pat]]
+ [pattern (~or [⊢ [pat* ≫ e-stx ⇐ τ-pat]]
+ [⊢ [pat* ≫ e-stx ⇐ : τ-pat]])
#:with stx (generate-temporary 'stx)
#:with τ (generate-temporary #'τ-pat)
#:with pat
@@ -288,7 +296,8 @@
(define-splicing-syntax-class pat #:datum-literals (⇐ :)
[pattern (~seq pat)
#:attr transform-body identity]
- [pattern (~seq pat* left:⇐ : τ-pat)
+ [pattern (~or (~seq pat* left:⇐ τ-pat)
+ (~seq pat* left:⇐ : τ-pat))
#:with stx (generate-temporary 'stx)
#:with τ (generate-temporary #'τ-pat)
#:with b (generate-temporary 'body)
