pat-expander-tests-def.rkt (5970B)
1 #lang turnstile 2 3 (provide (all-defined-out)) 4 5 (define-base-type Nothing) 6 (define-base-type Bool) 7 (define-base-type Int) 8 (define-base-type String) 9 (define-type-constructor Tuple #:arity >= 0) 10 (define-type-constructor Listof #:arity = 1) 11 (define-type-constructor Sequenceof #:arity >= 0) 12 13 (begin-for-syntax 14 (define-splicing-syntax-class (for-clause-group env) 15 #:attributes [[clause- 1] [env.x 1] [env.τ 1]] 16 [pattern (~seq (~var clause (for-clause env)) 17 ...) 18 #:with [clause- ...] #'[clause.clause- ... ...] 19 #:with [[env.x env.τ] ...] #'[[clause.env.x clause.env.τ] ... ...]]) 20 21 (define-splicing-syntax-class (guard-clause env) 22 #:attributes [[clause- 1]] 23 [pattern (~and (~seq #:when bool:expr) 24 (~typecheck 25 #:with [[x τ_x] ...] env 26 [[x ≫ x- : τ_x] ... ⊢ bool ≫ bool- ⇐ Bool])) 27 #:with [clause- ...] #`[#:when (let- ([x- x] ...) bool-)]] 28 [pattern (~and (~seq #:unless bool:expr) 29 (~typecheck 30 #:with [[x τ_x] ...] env 31 [[x ≫ x- : τ_x] ... ⊢ bool ≫ bool- ⇐ Bool])) 32 #:with [clause- ...] #`[#:unless (let- ([x- x] ...) bool-)]] 33 [pattern (~and (~seq #:break bool:expr) 34 (~typecheck 35 #:with [[x τ_x] ...] env 36 [[x ≫ x- : τ_x] ... ⊢ bool ≫ bool- ⇐ Bool])) 37 #:with [clause- ...] #`[#:break (let- ([x- x] ...) bool-)]] 38 [pattern (~and (~seq #:final bool:expr) 39 (~typecheck 40 #:with [[x τ_x] ...] env 41 [[x ≫ x- : τ_x] ... ⊢ bool ≫ bool- ⇐ Bool])) 42 #:with [clause- ...] #`[#:final (let- ([x- x] ...) bool-)]]) 43 44 (define-splicing-syntax-class (for-clause env) 45 #:attributes [[clause- 1] [env.x 1] [env.τ 1]] 46 [pattern (~and [x:id seq:expr] 47 (~typecheck 48 #:with [[y τ_y] ...] env 49 [[y ≫ y- : τ_y] ... ⊢ seq ≫ seq- ⇒ (~Sequenceof τ_x)])) 50 #:with [clause- ...] #'[[x (let- ([y- y] ...) seq-)]] 51 #:with [[env.x env.τ] ...] #'[[x τ_x]]] 52 [pattern (~and [(x:id ...) seq:expr] 53 (~typecheck 54 #:with [[y τ_y] ...] env 55 [[y ≫ y- : τ_y] ... ⊢ seq ≫ seq- ⇒ (~Sequenceof τ_x ...)])) 56 #:fail-unless (stx-length=? #'[x ...] #'[τ_x ...]) 57 (format "expected a ~v-valued sequence, given a ~v-valued one" 58 (stx-length #'[x ...]) 59 (stx-length #'[τ_x ...])) 60 #:with [clause- ...] #'[[(x ...) (let- ([y- y] ...) seq-)]] 61 #:with [[env.x env.τ] ...] #'[[x τ_x] ...]]) 62 63 (define-syntax-class (for-clauses env) 64 #:attributes [[clause- 1] [env.x 1] [env.τ 1]] 65 [pattern ((~var group (for-clause-group env))) 66 #:with [clause- ...] #'[group.clause- ...] 67 #:with [[env.x env.τ] ...] #'[[group.env.x group.env.τ] ...]] 68 [pattern ((~var fst (for-clause-group env)) 69 (~var guard (guard-clause (stx-append env #'[[fst.env.x fst.env.τ] ...]))) 70 . 71 (~var rst (for-clauses (stx-append env #'[[fst.env.x fst.env.τ] ...])))) 72 #:with [clause- ...] #'[fst.clause- ... guard.clause- ... rst.clause- ...] 73 #:with [[env.x env.τ] ...] #'[[fst.env.x fst.env.τ] ... [rst.env.x rst.env.τ] ...]]) 74 ) 75 76 ;; ------------------------------------------------------------------------ 77 78 ;; for/list 79 80 (define-typed-syntax for/list 81 [(_ (~var clauses (for-clauses #'[])) 82 body) ≫ 83 [[clauses.env.x ≫ x- : clauses.env.τ] ... 84 ⊢ body ≫ body- ⇒ τ] 85 -------- 86 [⊢ (for/list- (clauses.clause- ...) 87 (let- ([x- clauses.env.x] ...) body-)) 88 ⇒ (Listof τ)]]) 89 90 (define-typed-syntax in-range 91 [(_ n:expr) ≫ 92 [⊢ n ≫ n- ⇐ Int] 93 -------- 94 [⊢ (in-range- n-) ⇒ (Sequenceof Int)]]) 95 96 (define-typed-syntax in-naturals 97 [(_) ≫ --- [⊢ (in-naturals-) ⇒ (Sequenceof Int)]] 98 [(_ n:expr) ≫ 99 [⊢ n ≫ n- ⇐ Int] 100 -------- 101 [⊢ (in-naturals- n-) ⇒ (Sequenceof Int)]]) 102 103 (define-typed-syntax in-list 104 [(_ lst:expr) ≫ 105 [⊢ lst ≫ lst- ⇒ (~Listof τ)] 106 -------- 107 [⊢ (in-list- lst-) ⇒ (Sequenceof τ)]]) 108 109 (define-typed-syntax in-indexed 110 [(_ seq:expr) ≫ 111 [⊢ seq ≫ seq- ⇒ (~Sequenceof τ)] 112 -------- 113 [⊢ (in-indexed- seq-) ⇒ (Sequenceof τ Int)]]) 114 115 ;; ------------------------------------------------------------------------ 116 117 ;; Constructing Literals, Tuples, and Lists 118 119 (define-typed-syntax #%datum 120 [(_ . b:boolean) ≫ --- [⊢ (quote- b) ⇒ Bool]] 121 [(_ . i:integer) ≫ --- [⊢ (quote- i) ⇒ Int]] 122 [(_ . s:str) ≫ --- [⊢ (quote- s) ⇒ String]]) 123 124 (define-typed-syntax tuple 125 [(_ e:expr ...) ≫ 126 [⊢ [e ≫ e- ⇒ τ] ...] 127 -------- 128 [⊢ (vector-immutable- e- ...) ⇒ (Tuple τ ...)]]) 129 130 (define-typed-syntax list 131 [(_) ≫ --- [⊢ (quote- ()) ⇒ (Listof Nothing)]] 132 [(_ e0:expr e:expr ...) ≫ 133 [⊢ e0 ≫ e0- ⇒ τ] 134 [⊢ [e ≫ e- ⇐ τ] ...] 135 -------- 136 [⊢ (list- e0- e- ...) ⇒ (Listof τ)]]) 137 138 ;; ------------------------------------------------------------------------ 139 140 ;; Basic Bool Forms 141 142 (define-typed-syntax not 143 [(_ b:expr) ≫ [⊢ b ≫ b- ⇐ Bool] --- [⊢ (not- b-) ⇒ Bool]]) 144 145 (define-typed-syntax and 146 [(_ b:expr ...) ≫ 147 [⊢ [b ≫ b- ⇐ Bool] ...] 148 -------- 149 [⊢ (and- b- ...) ⇒ Bool]]) 150 151 ;; ------------------------------------------------------------------------ 152 153 ;; Basic Int Forms 154 155 (define-typed-syntax even? 156 [(_ i:expr) ≫ [⊢ i ≫ i- ⇐ Int] --- [⊢ (even?- i-) ⇒ Bool]]) 157 158 (define-typed-syntax odd? 159 [(_ i:expr) ≫ [⊢ i ≫ i- ⇐ Int] --- [⊢ (odd?- i-) ⇒ Bool]]) 160 161 ;; ------------------------------------------------------------------------ 162 163 ;; Basic String Forms 164 165 (define-typed-syntax string=? 166 [(_ a:expr b:expr) ≫ 167 [⊢ a ≫ a- ⇐ String] 168 [⊢ b ≫ b- ⇐ String] 169 -------- 170 [⊢ (string=?- a- b-) ⇒ Bool]]) 171