commit f545503d198e3b5562d253f146e2128ba8c1d3a3
parent d5b46b9ee40a7568920c3a5200df4f85be6f9acc
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Thu, 18 Aug 2016 15:59:05 -0400
allow optionally eliding more parens
- single env
- \vdash rhs
Diffstat:
2 files changed, 20 insertions(+), 13 deletions(-)
diff --git a/turnstile/examples/stlc.rkt b/turnstile/examples/stlc.rkt
@@ -12,25 +12,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- ...) e-) ⇒ (→ τ_in.norm ... τ_out)]]
[(λ (x:id ...) e) ⇐ (~→ τ_in ... τ_out) ≫
- [([x ≫ x- : τ_in] ...) ⊢ [e ≫ e- ⇐ τ_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] ...]
--------
- [⊢ [_ ≫ (#%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
@@ -161,7 +161,8 @@
(define-splicing-syntax-class inf
#:datum-literals (⊢ ⇒ ⇐ ≫ :)
#:attributes (depth es-stx es-stx-orig es-pat)
- [pattern (~seq [e-stx* ≫ e-pat* props:⇒-props] ooo:elipsis ...)
+ [pattern (~or (~seq e-stx* ≫ e-pat* props:⇒-props (~parse (ooo ...) #'()))
+ (~seq [e-stx* ≫ e-pat* props:⇒-props] ooo:elipsis ...))
#:with depth (stx-length #'[ooo ...])
#:with es-stx (with-depth #'e-stx* #'[ooo ...])
#:with es-stx-orig (with-depth #'e-stx* #'[ooo ...])
@@ -171,7 +172,8 @@
#'(~and props.e-pat
e-pat*)
#'[ooo ...]))]
- [pattern (~seq [e-stx* ≫ e-pat* props:⇐-props] ooo:elipsis ...)
+ [pattern (~or (~seq e-stx* ≫ e-pat* props:⇐-props (~parse (ooo ...) #'()))
+ (~seq [e-stx* ≫ e-pat* props:⇐-props] ooo:elipsis ...))
#:with e-tmp (generate-temporary #'e-pat*)
#:with τ-tmp (generate-temporary 'τ)
#:with τ-exp-tmp (generate-temporary 'τ_expected)
@@ -208,6 +210,8 @@
#:datum-literals (⊢)
[pattern (~or (~seq [⊢ inf:inf*] ooo:elipsis ...
(~parse ((ctx.x- ctx.ctx tvctx.x- tvctx.ctx) ...) #'()))
+ (~seq [ctx:id-props+≫* ⊢ inf:inf*] ooo:elipsis ...
+ (~parse ((tvctx.x- tvctx.ctx) ...) #'()))
(~seq [(ctx:id-props+≫*) ⊢ inf:inf*] ooo:elipsis ...
(~parse ((tvctx.x- tvctx.ctx) ...) #'()))
(~seq [(tvctx:id-props+≫*) (ctx:id-props+≫*) ⊢ inf:inf*] ooo:elipsis ...))
@@ -270,7 +274,8 @@
(define-syntax-class last-clause
#:datum-literals (⊢ ≫ ≻ ⇒ ⇐ :)
#:attributes ([pat 0] [stuff 1] [body 0])
- [pattern [⊢ [pat ≫ e-stx props:⇒-props/conclusion]]
+ [pattern (~or [⊢ pat ≫ e-stx props:⇒-props/conclusion]
+ [⊢ [pat ≫ e-stx props:⇒-props/conclusion]])
#:with [stuff ...] #'[]
#:with body:expr
(for/fold ([body #'(quasisyntax/loc this-syntax e-stx)])
@@ -278,9 +283,11 @@
[v (in-list (syntax->list #'[props.tag-expr ...]))])
(with-syntax ([body body] [k k] [v v])
#'(assign-type body #:tag 'k v)))]
- [pattern [⊢ [e-stx]]
+ [pattern (~or [⊢ [e-stx]] [⊢ (~and e-stx (~not [_ ≫ . rst]))])
#:with :last-clause #'[⊢ [_ ≫ e-stx ⇐ : _]]]
- [pattern (~or [⊢ [pat* ≫ e-stx ⇐ τ-pat]]
+ [pattern (~or [⊢ pat* ≫ e-stx ⇐ τ-pat]
+ [⊢ pat* ≫ e-stx ⇐ : τ-pat]
+ [⊢ [pat* ≫ e-stx ⇐ τ-pat]]
[⊢ [pat* ≫ e-stx ⇐ : τ-pat]])
#:with stx (generate-temporary 'stx)
#:with τ (generate-temporary #'τ-pat)
