suzanne.soy/macrotypes
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

allow single env, implies empty tvctx

Browse Source
This commit is contained in:
Stephen Chang 2016-08-18 15:17:26 -04:00
parent aa0136cf29
commit 6d99f352db
2 changed files with 7 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
turnstile/examples/stlc.rkt
View File

@ -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-) ⇐ _]]])

8
turnstile/turnstile.rkt
View File

@ -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