match2.mlish (6336B)
1 #lang s-exp "../../mlish.rkt" 2 (require "../rackunit-typechecking.rkt") 3 4 ;; alternate match that supports nested patterns 5 6 (define-type (Test X) 7 (A X) 8 (B (× X X)) 9 (C (× X (× X X)))) 10 11 (typecheck-fail 12 (match2 (B (tup 2 3)) with 13 [B x -> x]) 14 #:with-msg "clauses not exhaustive; missing: A, C") 15 16 (typecheck-fail 17 (match2 (B (tup 2 3)) with 18 [A x -> x] 19 [C (x,y) -> y] 20 [B x -> x]) #:with-msg "branches have incompatible types: Int and \\(× Int Int\\)") 21 22 (typecheck-fail 23 (match2 (B (tup 2 3)) with 24 [A x -> (tup x x)] 25 [C x -> x] 26 [B x -> x]) 27 #:with-msg "branches have incompatible types: \\(× Int Int\\) and \\(× Int \\(× Int Int\\)\\)") 28 29 (check-type 30 (match2 (B (tup 2 3)) with 31 [A x -> (tup x x)] 32 [C (x,y) -> y] 33 [B x -> x]) : (× Int Int) -> (list 2 3)) 34 35 (typecheck-fail 36 (match2 (A (tup 2 3)) with 37 [A x -> x]) #:with-msg "clauses not exhaustive; missing: B, C") 38 39 (check-type 40 (match2 (A (tup 2 3)) with 41 [B (x,y) -> y] 42 [C (x,y) -> x] 43 [A x -> x]) : (× Int Int) -> (list 2 3)) 44 45 (check-type 46 (match2 (A (tup 2 3)) with 47 [B (x,y) -> y] 48 [A x -> x] 49 [C (x,y) -> x]) : (× Int Int) -> (list 2 3)) 50 51 (typecheck-fail 52 (match2 (A (tup 2 3)) with 53 [B (x,y) -> y] 54 [A x -> x] 55 [C x -> x]) #:with-msg "branches have incompatible types") 56 57 (check-type 58 (match2 (A 1) with 59 [A x -> x] 60 [_ -> -1]) : Int -> 1) 61 62 (typecheck-fail 63 (match2 (B 1) with 64 [B x -> x]) 65 #:with-msg "expected: \\(× X X\\)\n *given: Int") 66 67 (check-type 68 (match2 (B (tup 2 3)) with 69 [B (tup x y) -> (+ x y)] 70 [_ -> -1]) : Int -> 5) 71 72 (check-type 73 (match2 (C (tup 2 (tup 3 4))) with 74 [C (tup x (tup y z)) -> (+ x (+ y z))] 75 [_ -> -1]) : Int -> 9) 76 77 (check-type 78 (match2 (C (tup 2 (tup 3 4))) with 79 [A x -> x] 80 [_ -> 100]) : Int -> 100) 81 82 83 84 ;; lists 85 86 (typecheck-fail 87 (match2 (list 1) with 88 [list x -> x]) #:with-msg "missing nil clause") 89 90 (typecheck-fail 91 (match2 (list 1) with 92 [nil -> 0] 93 [list x -> x]) 94 #:with-msg "missing clause for non-empty, arbitrary length list") 95 96 (check-type 97 (match2 (list 1) with 98 [nil -> 0] 99 [x :: xs -> x]) : Int -> 1) 100 101 (check-type 102 (match2 (list 1) with 103 [nil -> 0] 104 [list x -> x] 105 [x :: xs -> x]) : Int -> 1) 106 107 (check-type 108 (match2 (list 1) with 109 [list -> 0] 110 [list x -> x] 111 [x :: xs -> x]) : Int -> 1) 112 113 (check-type 114 (match2 (list 1) with 115 [list x -> x] 116 [_ -> 0]) : Int -> 1) 117 118 (check-type 119 (match2 (list 1) with 120 [x :: xs -> x] 121 [nil -> 0]) : Int -> 1) 122 123 (check-type 124 (match2 (list 1) with 125 [_ -> -1] 126 [list x -> x] 127 [nil -> 0]) : Int -> -1) 128 129 (check-type 130 (match2 (list 1) with 131 [_ -> -1] 132 [list x -> x] 133 [list -> 0]) : Int -> -1) 134 135 (check-type 136 (match2 (list 1) with 137 [_ -> 0]) : Int -> 0) 138 139 (typecheck-fail 140 (match2 (list 1) with 141 [nil -> 0]) 142 #:with-msg "missing clause for non-empty, arbitrary length list") 143 144 (check-type 145 (match2 (list 1 2) with 146 [list x y -> (+ x y)] 147 [_ -> 0]) : Int -> 3) 148 149 (check-type 150 (match2 (list 1 2) with 151 [list -> 0] 152 [list x y -> (+ x y)] 153 [_ -> -1]) : Int -> 3) 154 155 (check-type 156 (match2 (list (list 3 4) (list 5 6)) with 157 [list -> 0] 158 [list (list w x) (list y z) -> (+ (+ x y) (+ z w))] 159 [_ -> -1]) : Int -> 18) 160 161 (check-type 162 (match2 (list (tup 3 4) (tup 5 6)) with 163 [list -> 0] 164 [list (tup w x) (tup y z) -> (+ (+ x y) (+ z w))] 165 [_ -> -1]) : Int -> 18) 166 167 (check-type 168 (match2 (nil {Int}) with 169 [nil -> 0] 170 [list x y -> (+ x y)] 171 [_ -> -1]) : Int -> 0) 172 173 (check-type 174 (match2 (list 1 2) with 175 [nil -> 0] 176 [list x y -> (+ x y)] 177 [_ -> -1]) : Int -> 3) 178 179 (check-type 180 (match2 (list 1 2 3) with 181 [nil -> 0] 182 [list x y -> (+ x y)] 183 [_ -> -1]) : Int -> -1) 184 185 ;; 0-arity constructors 186 (define-type (Test2 X) 187 AA 188 (BB X)) 189 190 (check-type 191 (match2 (BB 1) with 192 [AA -> 0] 193 [BB x -> x]) : Int -> 1) 194 195 (check-type 196 (match2 (BB (AA {Int})) with 197 [AA -> 0] 198 [BB AA -> 1] 199 [_ -> 2]) : Int -> 1) 200 201 ;; drop parens around 0-arity constructors 202 (check-type 203 (match2 (BB 1) with 204 [AA -> 0] 205 [BB x -> x]) : Int -> 1) 206 207 (check-type 208 (match2 (BB (AA {Int})) with 209 [AA -> 0] 210 [BB AA -> 1] 211 [_ -> 2]) : Int -> 1) 212 213 ;; nicer cons pattern syntax (::) 214 (check-type 215 (match2 (list 1 2) with 216 [nil -> -1] 217 [x :: xs -> x]) 218 : Int -> 1) 219 220 (check-type 221 (match2 (list 1 2) with 222 [nil -> -1] 223 [x :: y :: xs -> y]) : Int -> 2) 224 225 (check-type 226 (match2 (list (tup 1 2) (tup 3 4)) with 227 [nil -> -1] 228 [(tup x y) :: (tup a b) :: xs -> (+ a b)]) : Int -> 7) 229 230 (check-type 231 (match2 (list (list 2 3 4) (list 5 6 7) (list 9 10)) with 232 [nil -> -1] 233 [x :: (y :: z :: zs) :: xs -> z]) : Int -> 6) 234 235 (check-type 236 (match2 (list (list 2 3 4) (list 5 6 7) (list 9 10)) with 237 [nil -> -1] 238 [x :: (list a b c) :: xs -> c]) : Int -> 7) 239 240 (typecheck-fail 241 (match2 (list (list #t #f)) with 242 [nil -> -1] 243 [(list x y) :: tl -> (+ x y)]) 244 #:with-msg "expected: Int\n *given: Bool") 245 246 ;; comma tup pattern syntax 247 248 (check-type 249 (match2 (tup 1 2) with 250 [(x,y) -> (+ x y)]) : Int -> 3) 251 252 (check-type 253 (match2 (tup 1 2 4) with 254 [(_,y,z) -> (+ z y)]) : Int -> 6) 255 256 (check-type 257 (match2 (list (tup 1 2) (tup 3 4) (tup 5 6)) with 258 [(x,y) :: (a,b) :: rst -> (+ y a)] 259 [_ -> -1]) : Int -> 5) 260 261 (check-type 262 (match2 (list (tup (BB 1) (AA {Int})) (tup (BB 2) (AA {Int}))) with 263 [((BB x),AA) :: ((BB y),AA) :: rst -> (+ y x)] 264 [_ -> -1]) : Int -> 3) 265 266 (check-type 267 (match2 (tup (tup (tup 1 2) (tup 3)) (tup 4 (tup 6 7))) with 268 [(((x,y),z),(a,(b,c))) -> (+ c y)]) : Int -> 9) 269 270 (check-type 271 (match2 (tup (tup (tup 1 2) (tup 3)) (tup 4 (tup 6 7))) with 272 [(((x,y),z),(_,(_,c))) -> (+ c y)]) : Int -> 9) 273 274 (check-type 275 (match2 (tup (tup (tup 1 2) (tup 3)) (tup 4 (tup 6 7))) with 276 [(((_,y),_),(_,(_,c))) -> (+ c y)]) : Int -> 9) 277 278 (typecheck-fail 279 (match2 (tup (BB 1) (BB 2)) with 280 [((BB x),(BB y)) -> (+ x y)]) 281 #:with-msg "clauses not exhaustive; missing: AA") 282 283 ;; TODO: should tail 284 #;(typecheck-fail 285 (match2 (tup (BB 1) (BB 2)) with 286 [((BB x),(BB y)) -> (+ x y)] 287 [(AA,AA) -> 0]) 288 #:with-msg "clauses not exhaustive; missing: AA") 289 290 ;; falls off; runtime match exception 291 #;(match2 (tup (BB 2) (AA {Int})) with 292 [((BB x),(BB y)) -> (+ x y)] 293 [(AA,AA) -> 0]) 294 295 (check-type 296 (match2 (tup (BB 1) (BB 2)) with 297 [((BB x),(BB y)) -> (+ x y)] 298 [_ -> -1]) : Int -> 3)