From bbcdfaf9cf0c7869e59ab6ec039f9786ed4effe7 Mon Sep 17 00:00:00 2001
From: Alex Knauth <alexander@knauth.org>
Date: Mon, 17 Apr 2017 12:41:02 -0700
Subject: [PATCH] =?UTF-8?q?add=20~typecheck=20and=20~=E2=8A=A2=20pattern?=
 =?UTF-8?q?=20expanders=20(#6)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

* 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 ~⊢
---
 .../examples/tests/pat-expander-tests-def.rkt | 171 ++++++++++++++++++
 .../examples/tests/pat-expander-tests.rkt     | 143 +++++++++++++++
 turnstile/scribblings/reference.scrbl         |  60 ++++++
 turnstile/turnstile.rkt                       |  12 ++
 4 files changed, 386 insertions(+)
 create mode 100644 turnstile/examples/tests/pat-expander-tests-def.rkt
 create mode 100644 turnstile/examples/tests/pat-expander-tests.rkt

diff --git a/turnstile/examples/tests/pat-expander-tests-def.rkt b/turnstile/examples/tests/pat-expander-tests-def.rkt
new file mode 100644
index 0000000..1c1894e
--- /dev/null
+++ 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
new file mode 100644
index 0000000..eabb010
--- /dev/null
+++ 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
index 482076e..1638831 100644
--- 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
index 3b85771..b6981ff 100644
--- 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