commit ebecdb663c725d39b30b1a63b97a1e27db8cf16a
parent 6d99f352dbe1a90f98c8209e184249a47fda9aa8
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Thu, 18 Aug 2016 16:49:23 -0400
allow arbitrary number of dashes in type rules
closes #23
Diffstat:
2 files changed, 9 insertions(+), 3 deletions(-)
diff --git a/turnstile/examples/stlc.rkt b/turnstile/examples/stlc.rkt
@@ -30,11 +30,11 @@
(define-typed-syntax λ #:datum-literals (:)
[(λ ([x:id : τ_in:type] ...) e) ≫
[([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-) ⇐ _]]])
(define-typed-syntax #%app
diff --git a/turnstile/turnstile.rkt b/turnstile/turnstile.rkt
@@ -58,7 +58,13 @@
(for-meta -1 (submod ".." typecheck+) (except-in macrotypes/typecheck #%module-begin))
(for-meta -2 (except-in macrotypes/typecheck #%module-begin)))
(define-syntax-class ---
- [pattern (~datum --------)])
+ [pattern dashes
+ #:do [(define str-dashes (symbol->string (syntax->datum #'dashes)))]
+ #:fail-unless (for/and ([d (in-string str-dashes)])
+ (char=? #\- d))
+ "expected a separator consisting of dashes"
+ #:fail-unless (>= (string-length str-dashes) 3)
+ "expected a separator of three or more dashes"])
(define-syntax-class elipsis
[pattern (~literal ...)])
