commit bbcdfaf9cf0c7869e59ab6ec039f9786ed4effe7
parent f9199f6e3710018c2162f0453ae10ef164534063
Author: Alex Knauth <alexander@knauth.org>
Date: Mon, 17 Apr 2017 12:41:02 -0700
add ~typecheck and ~⊢ pattern expanders (#6)
* add ~typecheck and ~⊢ pattern expanders
So that in normal macros, syntax classes, and normal syntax-parse
expressions, you can use use the Turnstile syntax to do typechecking
* add documentation for ~typecheck and ~⊢
Diffstat:
4 files changed, 386 insertions(+), 0 deletions(-)
diff --git a/turnstile/examples/tests/pat-expander-tests-def.rkt b/turnstile/examples/tests/pat-expander-tests-def.rkt
@@ -0,0 +1,171 @@
+#lang turnstile
+
+(provide (all-defined-out))
+
+(define-base-type Nothing)
+(define-base-type Bool)
+(define-base-type Int)
+(define-base-type String)
+(define-type-constructor Tuple #:arity >= 0)
+(define-type-constructor Listof #:arity = 1)
+(define-type-constructor Sequenceof #:arity >= 0)
+
+(begin-for-syntax
+ (define-splicing-syntax-class (for-clause-group env)
+ #:attributes [[clause- 1] [env.x 1] [env.τ 1]]
+ [pattern (~seq (~var clause (for-clause env))
+ ...)
+ #:with [clause- ...] #'[clause.clause- ... ...]
+ #:with [[env.x env.τ] ...] #'[[clause.env.x clause.env.τ] ... ...]])
+
+ (define-splicing-syntax-class (guard-clause env)
+ #:attributes [[clause- 1]]
+ [pattern (~and (~seq #:when bool:expr)
+ (~typecheck
+ #:with [[x τ_x] ...] env
+ [[x ≫ x- : τ_x] ... ⊢ bool ≫ bool- ⇐ Bool]))
+ #:with [clause- ...] #`[#:when (let- ([x- x] ...) bool-)]]
+ [pattern (~and (~seq #:unless bool:expr)
+ (~typecheck
+ #:with [[x τ_x] ...] env
+ [[x ≫ x- : τ_x] ... ⊢ bool ≫ bool- ⇐ Bool]))
+ #:with [clause- ...] #`[#:unless (let- ([x- x] ...) bool-)]]
+ [pattern (~and (~seq #:break bool:expr)
+ (~typecheck
+ #:with [[x τ_x] ...] env
+ [[x ≫ x- : τ_x] ... ⊢ bool ≫ bool- ⇐ Bool]))
+ #:with [clause- ...] #`[#:break (let- ([x- x] ...) bool-)]]
+ [pattern (~and (~seq #:final bool:expr)
+ (~typecheck
+ #:with [[x τ_x] ...] env
+ [[x ≫ x- : τ_x] ... ⊢ bool ≫ bool- ⇐ Bool]))
+ #:with [clause- ...] #`[#:final (let- ([x- x] ...) bool-)]])
+
+ (define-splicing-syntax-class (for-clause env)
+ #:attributes [[clause- 1] [env.x 1] [env.τ 1]]
+ [pattern (~and [x:id seq:expr]
+ (~typecheck
+ #:with [[y τ_y] ...] env
+ [[y ≫ y- : τ_y] ... ⊢ seq ≫ seq- ⇒ (~Sequenceof τ_x)]))
+ #:with [clause- ...] #'[[x (let- ([y- y] ...) seq-)]]
+ #:with [[env.x env.τ] ...] #'[[x τ_x]]]
+ [pattern (~and [(x:id ...) seq:expr]
+ (~typecheck
+ #:with [[y τ_y] ...] env
+ [[y ≫ y- : τ_y] ... ⊢ seq ≫ seq- ⇒ (~Sequenceof τ_x ...)]))
+ #:fail-unless (stx-length=? #'[x ...] #'[τ_x ...])
+ (format "expected a ~v-valued sequence, given a ~v-valued one"
+ (stx-length #'[x ...])
+ (stx-length #'[τ_x ...]))
+ #:with [clause- ...] #'[[(x ...) (let- ([y- y] ...) seq-)]]
+ #:with [[env.x env.τ] ...] #'[[x τ_x] ...]])
+
+ (define-syntax-class (for-clauses env)
+ #:attributes [[clause- 1] [env.x 1] [env.τ 1]]
+ [pattern ((~var group (for-clause-group env)))
+ #:with [clause- ...] #'[group.clause- ...]
+ #:with [[env.x env.τ] ...] #'[[group.env.x group.env.τ] ...]]
+ [pattern ((~var fst (for-clause-group env))
+ (~var guard (guard-clause (stx-append env #'[[fst.env.x fst.env.τ] ...])))
+ .
+ (~var rst (for-clauses (stx-append env #'[[fst.env.x fst.env.τ] ...]))))
+ #:with [clause- ...] #'[fst.clause- ... guard.clause- ... rst.clause- ...]
+ #:with [[env.x env.τ] ...] #'[[fst.env.x fst.env.τ] ... [rst.env.x rst.env.τ] ...]])
+ )
+
+;; ------------------------------------------------------------------------
+
+;; for/list
+
+(define-typed-syntax for/list
+ [(_ (~var clauses (for-clauses #'[]))
+ body) ≫
+ [[clauses.env.x ≫ x- : clauses.env.τ] ...
+ ⊢ body ≫ body- ⇒ τ]
+ --------
+ [⊢ (for/list- (clauses.clause- ...)
+ (let- ([x- clauses.env.x] ...) body-))
+ ⇒ (Listof τ)]])
+
+(define-typed-syntax in-range
+ [(_ n:expr) ≫
+ [⊢ n ≫ n- ⇐ Int]
+ --------
+ [⊢ (in-range- n-) ⇒ (Sequenceof Int)]])
+
+(define-typed-syntax in-naturals
+ [(_) ≫ --- [⊢ (in-naturals-) ⇒ (Sequenceof Int)]]
+ [(_ n:expr) ≫
+ [⊢ n ≫ n- ⇐ Int]
+ --------
+ [⊢ (in-naturals- n-) ⇒ (Sequenceof Int)]])
+
+(define-typed-syntax in-list
+ [(_ lst:expr) ≫
+ [⊢ lst ≫ lst- ⇒ (~Listof τ)]
+ --------
+ [⊢ (in-list- lst-) ⇒ (Sequenceof τ)]])
+
+(define-typed-syntax in-indexed
+ [(_ seq:expr) ≫
+ [⊢ seq ≫ seq- ⇒ (~Sequenceof τ)]
+ --------
+ [⊢ (in-indexed- seq-) ⇒ (Sequenceof τ Int)]])
+
+;; ------------------------------------------------------------------------
+
+;; Constructing Literals, Tuples, and Lists
+
+(define-typed-syntax #%datum
+ [(_ . b:boolean) ≫ --- [⊢ (quote- b) ⇒ Bool]]
+ [(_ . i:integer) ≫ --- [⊢ (quote- i) ⇒ Int]]
+ [(_ . s:str) ≫ --- [⊢ (quote- s) ⇒ String]])
+
+(define-typed-syntax tuple
+ [(_ e:expr ...) ≫
+ [⊢ [e ≫ e- ⇒ τ] ...]
+ --------
+ [⊢ (vector-immutable- e- ...) ⇒ (Tuple τ ...)]])
+
+(define-typed-syntax list
+ [(_) ≫ --- [⊢ (quote- ()) ⇒ (Listof Nothing)]]
+ [(_ e0:expr e:expr ...) ≫
+ [⊢ e0 ≫ e0- ⇒ τ]
+ [⊢ [e ≫ e- ⇐ τ] ...]
+ --------
+ [⊢ (list- e0- e- ...) ⇒ (Listof τ)]])
+
+;; ------------------------------------------------------------------------
+
+;; Basic Bool Forms
+
+(define-typed-syntax not
+ [(_ b:expr) ≫ [⊢ b ≫ b- ⇐ Bool] --- [⊢ (not- b-) ⇒ Bool]])
+
+(define-typed-syntax and
+ [(_ b:expr ...) ≫
+ [⊢ [b ≫ b- ⇐ Bool] ...]
+ --------
+ [⊢ (and- b- ...) ⇒ Bool]])
+
+;; ------------------------------------------------------------------------
+
+;; Basic Int Forms
+
+(define-typed-syntax even?
+ [(_ i:expr) ≫ [⊢ i ≫ i- ⇐ Int] --- [⊢ (even?- i-) ⇒ Bool]])
+
+(define-typed-syntax odd?
+ [(_ i:expr) ≫ [⊢ i ≫ i- ⇐ Int] --- [⊢ (odd?- i-) ⇒ Bool]])
+
+;; ------------------------------------------------------------------------
+
+;; Basic String Forms
+
+(define-typed-syntax string=?
+ [(_ a:expr b:expr) ≫
+ [⊢ a ≫ a- ⇐ String]
+ [⊢ b ≫ b- ⇐ String]
+ --------
+ [⊢ (string=?- a- b-) ⇒ Bool]])
+
diff --git a/turnstile/examples/tests/pat-expander-tests.rkt b/turnstile/examples/tests/pat-expander-tests.rkt
@@ -0,0 +1,143 @@
+#lang turnstile
+
+(require turnstile/rackunit-typechecking
+ "pat-expander-tests-def.rkt")
+
+;; The for/list macro defined in "pat-expander-tests-def.rkt" uses the
+;; ~typecheck pattern-expander to typecheck the for clauses within a
+;; syntax class.
+
+;; These tests make sure that #:when conditions can refer to
+;; identifiers defined in previous clauses.
+
+(check-type (for/list () 1) : (Listof Int) -> (list 1))
+(check-type (for/list () #t) : (Listof Bool) -> (list #t))
+(check-type (for/list () #f) : (Listof Bool) -> (list #f))
+
+(check-type (for/list (#:when #t) 1) : (Listof Int) -> (list 1))
+(check-type (for/list (#:when #f) 1) : (Listof Int) -> (list))
+(check-type (for/list ([x (in-range 5)]) x)
+ : (Listof Int)
+ -> (list 0 1 2 3 4))
+
+(check-type (for/list ([(s i) (in-indexed (in-list (list "a" "b" "c")))])
+ (tuple s i))
+ : (Listof (Tuple String Int))
+ -> (list (tuple "a" 0) (tuple "b" 1) (tuple "c" 2)))
+
+(check-type (for/list ([(s i) (in-indexed (in-list (list "a" "b" "c")))]
+ #:when (even? i))
+ (tuple s i))
+ : (Listof (Tuple String Int))
+ -> (list (tuple "a" 0) (tuple "c" 2)))
+
+(check-type (for/list ([(s i) (in-indexed (in-list (list "a" "b" "c" "d" "e")))]
+ #:when (even? i)
+ [j (in-range i)])
+ (tuple s i j))
+ : (Listof (Tuple String Int Int))
+ -> (list (tuple "c" 2 0)
+ (tuple "c" 2 1)
+ (tuple "e" 4 0)
+ (tuple "e" 4 1)
+ (tuple "e" 4 2)
+ (tuple "e" 4 3)))
+
+;; ------------------------------------------------------------------------
+
+;; Test based on section 11 of the racket guide
+
+(check-type (for/list ([book (in-list (list "Guide" "Reference" "Notes"))]
+ #:when (not (string=? book "Notes"))
+ [i (in-naturals 1)]
+ [chapter (in-list (list "Intro" "Details" "Conclusion" "Index"))]
+ #:when (not (string=? chapter "Index")))
+ (tuple book i chapter))
+ : (Listof (Tuple String Int String))
+ -> (list (tuple "Guide" 1 "Intro")
+ (tuple "Guide" 2 "Details")
+ (tuple "Guide" 3 "Conclusion")
+ (tuple "Reference" 1 "Intro")
+ (tuple "Reference" 2 "Details")
+ (tuple "Reference" 3 "Conclusion")))
+
+(check-type (for/list ([book (in-list (list "Guide" "Story" "Reference"))]
+ #:break (string=? book "Story")
+ [chapter (in-list (list "Intro" "Details" "Conclusion"))])
+ (tuple book chapter))
+ : (Listof (Tuple String String))
+ -> (list (tuple "Guide" "Intro")
+ (tuple "Guide" "Details")
+ (tuple "Guide" "Conclusion")))
+
+(check-type (for/list ([book (in-list (list "Guide" "Story" "Reference"))]
+ #:when #true
+ [chapter (in-list (list "Intro" "Details" "Conclusion"))]
+ #:break (and (string=? book "Story")
+ (string=? chapter "Conclusion")))
+ (tuple book chapter))
+ : (Listof (Tuple String String))
+ -> (list (tuple "Guide" "Intro")
+ (tuple "Guide" "Details")
+ (tuple "Guide" "Conclusion")
+ (tuple "Story" "Intro")
+ (tuple "Story" "Details")))
+
+(check-type (for/list ([book (in-list (list "Guide" "Story" "Reference"))]
+ #:when #true
+ [chapter (in-list (list "Intro" "Details" "Conclusion"))]
+ #:final (and (string=? book "Story")
+ (string=? chapter "Conclusion")))
+ (tuple book chapter))
+ : (Listof (Tuple String String))
+ -> (list (tuple "Guide" "Intro")
+ (tuple "Guide" "Details")
+ (tuple "Guide" "Conclusion")
+ (tuple "Story" "Intro")
+ (tuple "Story" "Details")
+ (tuple "Story" "Conclusion")))
+
+(check-type (for/list ([book (in-list (list "Guide" "Story" "Reference"))]
+ #:final (string=? book "Story")
+ [chapter (in-list (list "Intro" "Details" "Conclusion"))])
+ (tuple book chapter))
+ : (Listof (Tuple String String))
+ -> (list (tuple "Guide" "Intro")
+ (tuple "Guide" "Details")
+ (tuple "Guide" "Conclusion")
+ (tuple "Story" "Intro")))
+
+;; ------------------------------------------------------------------------
+
+;; Tests based on section 3.18 of the racket reference
+
+(check-type (for/list ([i (in-list (list 1 2 3))]
+ [j (in-list (list "a" "b" "c"))]
+ #:when (odd? i)
+ [k (in-list (list #t #f))])
+ (tuple i j k))
+ : (Listof (Tuple Int String Bool))
+ -> (list (tuple 1 "a" #t)
+ (tuple 1 "a" #f)
+ (tuple 3 "c" #t)
+ (tuple 3 "c" #f)))
+
+(check-type (for/list ([i (in-list (list 1 2 3))]
+ [j (in-list (list "a" "b" "c"))]
+ #:break (not (odd? i))
+ [k (in-list (list #t #f))])
+ (tuple i j k))
+ : (Listof (Tuple Int String Bool))
+ -> (list (tuple 1 "a" #true)
+ (tuple 1 "a" #false)))
+
+(check-type (for/list ([i (in-list (list 1 2 3))]
+ [j (in-list (list "a" "b" "c"))]
+ #:final (not (odd? i))
+ [k (in-list (list #t #f))])
+ (tuple i j k))
+ : (Listof (Tuple Int String Bool))
+ -> (list (tuple 1 "a" #true)
+ (tuple 1 "a" #false)
+ (tuple 2 "b" #true)))
+
diff --git a/turnstile/scribblings/reference.scrbl b/turnstile/scribblings/reference.scrbl
@@ -234,6 +234,66 @@ A @racket[syntax-parse]-like form that supports
@racket[define-typed-syntax]-style clauses. In particular, see the
"rule" part of @racket[define-typed-syntax]'s grammar above.}
+@; ~typecheck and ~⊢
+
+@defform[(~typecheck premise ...)]{
+A @racket[syntax-parse] @tech[#:doc '(lib "syntax/scribblings/syntax.scrbl")]{pattern expander}
+that supports typechecking syntax.
+
+For example the pattern
+
+@racketblock[
+ (~typecheck
+ [⊢ a ≫ a- ⇒ τ_a]
+ [⊢ b ≫ b- ⇐ τ_a])]
+
+typechecks @racket[a] and @racket[b], expecting @racket[b] to have the
+type of @racket[a], and binding @racket[a-] and @racket[b-] to the
+expanded versions.
+
+This is most useful in places where you want to do typechecking in
+something other than a type rule, like in a function or a syntax
+class.
+
+@(let ([ev (make-base-eval)])
+ (ev '(require turnstile/turnstile))
+ @examples[
+ #:eval ev
+ (begin-for-syntax
+ (struct clause [stx- result-type])
+ (code:comment "f : Stx -> Clause")
+ (define (f stx)
+ (syntax-parse stx
+ [(~and [condition:expr body:expr]
+ (~typecheck
+ [⊢ condition ≫ condition- ⇐ Bool]
+ [⊢ body ≫ body- ⇒ τ_body]))
+ (clause #'[condition- body-] #'τ_body)])))
+ ])}
+
+@defform*[[(~⊢ tc ...)]]{
+A shorthand @tech[#:doc '(lib "syntax/scribblings/syntax.scrbl")]{pattern expander}
+for @racket[(~typcheck [⊢ tc ...])].
+
+For example the pattern @racket[(~⊢ a ≫ a- ⇒ τ_a)] typechecks
+@racket[a], binding the expanded version to @racket[a-] and the type
+to @racket[τ_a].
+
+@(let ([ev (make-base-eval)])
+ (ev '(require turnstile/turnstile))
+ @examples[
+ #:eval ev
+ (begin-for-syntax
+ (struct clause [stx- result-type])
+ (code:comment "f : Stx -> Clause")
+ (define (f stx)
+ (syntax-parse stx
+ [(~and [condition:expr body:expr]
+ (~⊢ condition ≫ condition- ⇐ Bool)
+ (~⊢ body ≫ body- ⇒ τ_body))
+ (clause #'[condition- body-] #'τ_body)])))
+ ])}
+
@; define-primop --------------------------------------------------------------
@defform*[((define-primop typed-op-id τ)
(define-primop typed-op-id : τ)
diff --git a/turnstile/turnstile.rkt b/turnstile/turnstile.rkt
@@ -6,6 +6,7 @@
(rename-out [define-typed-syntax define-typerule]
[define-typed-syntax define-syntax/typecheck])
(for-syntax syntax-parse/typecheck
+ ~typecheck ~⊢
(rename-out
[syntax-parse/typecheck syntax-parse/typed-syntax])))
@@ -403,6 +404,17 @@
(for-meta 2 'syntax-classes))
(begin-for-syntax
+ (define-syntax ~typecheck
+ (pattern-expander
+ (syntax-parser
+ [(_ clause:clause ...)
+ #'(~and clause.pat ...)])))
+ (define-syntax ~⊢
+ (pattern-expander
+ (syntax-parser
+ [(_ . stuff)
+ #'(~typecheck [⊢ . stuff])])))
+
(define-syntax syntax-parse/typecheck
(syntax-parser
[(_ stx-expr
