www

commit c9c0970307e7cd40c5705e9a87930d13ec7d3c70
parent 40a699cc8158c85451e57973cab812e6366b5c45
Author: Stephen Chang <stchang@ccs.neu.edu>
Date:   Wed, 12 Oct 2016 15:17:31 -0400

define-typed-syntax: properly handle implicit : with subsequent ⇒-props

- fixes #33

Diffstat:
M
turnstile/examples/fomega.rkt
 | 
2
+-
M
turnstile/examples/fomega2.rkt
 | 
2
+-
M
turnstile/turnstile.rkt
 | 
2
+-

3 files changed, 3 insertions(+), 3 deletions(-)
diff --git a/turnstile/examples/fomega.rkt b/turnstile/examples/fomega.rkt
@@ -96,7 +96,7 @@
   [⊢ e- ⇒ (∀ ([tv- : bvs.kind] ...) τ_e)])
 
 (define-typed-syntax (inst e τ ...) ≫
-  [⊢ e ≫ e- ⇒ : (~∀ (tv ...) τ_body) (⇒ (~∀★ k ...))]
+  [⊢ e ≫ e- ⇒ (~∀ (tv ...) τ_body) (⇒ (~∀★ k ...))]
   [⊢ τ ≫ τ- ⇐ k] ...
   #:with τ-inst (substs #'(τ- ...) #'(tv ...) #'τ_body)
   --------
diff --git a/turnstile/examples/fomega2.rkt b/turnstile/examples/fomega2.rkt
@@ -89,7 +89,7 @@
   [⊢ e- ⇒ (∀ ([tv- : bvs.kind] ...) τ_e)])
 
 (define-typed-syntax (inst e τ ...) ≫
-  [⊢ e ≫ e- ⇒ : (~∀ (tv ...) τ_body) (⇒ : (~∀★ k ...))]
+  [⊢ e ≫ e- ⇒ (~∀ (tv ...) τ_body) (⇒ : (~∀★ k ...))]
   [⊢ τ ≫ τ- ⇐ k] ...
   #:with τ-inst (substs #'(τ- ...) #'(tv ...) #'τ_body)
   --------
diff --git a/turnstile/turnstile.rkt b/turnstile/turnstile.rkt
@@ -89,7 +89,7 @@
     #:datum-literals (⇒)
     #:attributes (e-pat)
     [pattern (~or (~seq ⇒ tag-pat ; implicit : tag
-                        (~parse tag #':) (~parse (tag-prop.e-pat ...) #'()))
+                        (~parse tag #':) (tag-prop:⇒-prop) ...)
                   (~seq ⇒ tag:id tag-pat (tag-prop:⇒-prop) ...)) ; explicit tag
              #:with e-tmp (generate-temporary)
              #:with e-pat