From 6d99f352dbe1a90f98c8209e184249a47fda9aa8 Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Thu, 18 Aug 2016 15:17:26 -0400 Subject: [PATCH] allow single env, implies empty tvctx --- turnstile/examples/stlc.rkt | 4 ++-- turnstile/turnstile.rkt | 8 +++++--- 2 files changed, 7 insertions(+), 5 deletions(-) diff --git a/turnstile/examples/stlc.rkt b/turnstile/examples/stlc.rkt index c9fd8b2..a6702dd 100644 --- a/turnstile/examples/stlc.rkt +++ b/turnstile/examples/stlc.rkt @@ -29,11 +29,11 @@ (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 ≫ x- : τ_in] ...) ⊢ [e ≫ e- ⇐ τ_out]] -------- [⊢ [_ ≫ (λ- (x- ...) e-) ⇐ _]]]) diff --git a/turnstile/turnstile.rkt b/turnstile/turnstile.rkt index 7958b04..c433461 100644 --- a/turnstile/turnstile.rkt +++ b/turnstile/turnstile.rkt @@ -199,9 +199,11 @@ (define-splicing-syntax-class inf-clause #:attributes (pat) #:datum-literals (⊢) - [pattern (~seq [⊢ (~and (~seq inf-stuff ...) (~seq inf:inf ...))] ooo:elipsis ...) - #:with [:inf-clause] #'[[() () ⊢ inf-stuff ...] ooo ...]] - [pattern (~seq [(tvctx:id-props+≫*) (ctx:id-props+≫*) ⊢ inf:inf*] ooo:elipsis ...) + [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 [(tvctx:id-props+≫*) (ctx:id-props+≫*) ⊢ inf:inf*] ooo:elipsis ...)) #:with clause-depth (stx-length #'[ooo ...]) #:with infs-pat (with-depth