exist-tests.rkt (15552B)
1 #lang s-exp "../exist.rkt" 2 (require "rackunit-typechecking.rkt") 3 4 (check-type (pack (Int 0) as (∃ (X) X)) : (∃ (X) X)) 5 (check-type (pack (Int 0) as (∃ (X) X)) : (∃ (Y) Y)) 6 (typecheck-fail (pack (Int 0) as (∃ (X) Y))) 7 (check-type (pack (Bool #t) as (∃ (X) X)) : (∃ (X) X)) 8 (typecheck-fail (pack (Int #t) as (∃ (X) X))) 9 10 (check-type (pack (Int (pack (Int 0) as (∃ (X) X))) as (∃ (Y) (∃ (X) X))) 11 : (∃ (Y) (∃ (X) X))) 12 (check-type (pack (Int +) as (∃ (X) (→ X Int Int))) : (∃ (X) (→ X Int Int))) 13 (check-type (pack (Int (pack (Int +) as (∃ (X) (→ X Int Int)))) 14 as (∃ (Y) (∃ (X) (→ X Y Int)))) 15 : (∃ (Y) (∃ (X) (→ X Y Int)))) 16 (check-not-type (pack (Int (pack (Int +) as (∃ (X) (→ X Int Int)))) 17 as (∃ (Y) (∃ (X) (→ X Y Int)))) 18 : (∃ (X) (∃ (X) (→ X X Int)))) 19 20 ; cant typecheck bc X has local scope, and no X elimination form 21 ;(check-type (open [x <= (pack (Int 0) as (∃ (X) X)) with X] x) : X) 22 23 (check-type 0 : Int) 24 (check-type (+ 0 1) : Int ⇒ 1) 25 (check-type ((λ ([x : Int]) (+ x 1)) 0) : Int ⇒ 1) 26 (typecheck-fail (open [x <= (pack (Int 0) as (∃ (X) X)) with] (+ x 1))) ; can't use as Int 27 28 (check-type (λ ([x : (∃ (X) X)]) x) : (→ (∃ (X) X) (∃ (Y) Y))) 29 (check-type ((λ ([x : (∃ (X) X)]) x) (pack (Int 0) as (∃ (Z) Z))) 30 : (∃ (X) X) ⇒ 0) 31 (check-type ((λ ([x : (∃ (X) X)]) x) (pack (Bool #t) as (∃ (Z) Z))) 32 : (∃ (X) X) ⇒ #t) 33 34 ;; example where the two binding X's are conflated, see exist.rkt for explanation 35 (check-type (open [x <= (pack (Int 0) as (∃ (X) X)) with X] ((λ ([y : X]) 1) x)) 36 : Int ⇒ 1) 37 38 (check-type 39 (pack (Int (tup [a = 5] [f = (λ ([x : Int]) (+ x 1))])) 40 as (∃ (X) (× [a : X] [f : (→ X X)]))) 41 : (∃ (X) (× [a : X] [f : (→ X X)]))) 42 43 (define p4 44 (pack (Int (tup [a = 5] [f = (λ ([x : Int]) (+ x 1))])) 45 as (∃ (X) (× [a : X] [f : (→ X Int)])))) 46 (check-type p4 : (∃ (X) (× [a : X] [f : (→ X Int)]))) 47 48 (check-not-type (open [x <= p4 with X] (proj x a)) : Int) ; type is X, not Int 49 ; type is (→ X X), not (→ Int Int) 50 (check-not-type (open [x <= p4 with X] (proj x f)) : (→ Int Int)) 51 (typecheck-fail (open [x <= p4 with X] (+ 1 (proj x a)))) 52 (check-type (open [x <= p4 with X] ((proj x f) (proj x a))) : Int ⇒ 6) 53 (check-type (open [x <= p4 with X] ((λ ([y : X]) ((proj x f) y)) (proj x a))) : Int ⇒ 6) 54 55 (check-type 56 (open [x <= (pack (Int 0) as (∃ (Y) Y)) with X] 57 ((λ ([y : X]) 1) x)) 58 : Int ⇒ 1) 59 60 (check-type 61 (pack (Int (tup [a = 5] [f = (λ ([x : Int]) (+ x 1))])) 62 as (∃ (X) (× [a : Int] [f : (→ Int Int)]))) 63 : (∃ (X) (× [a : Int] [f : (→ Int Int)]))) 64 65 (typecheck-fail 66 (pack (Int (tup [a = 5] [f = (λ ([x : Int]) (+ x 1))])) 67 as (∃ (X) (× [a : Int] [f : (→ Bool Int)])))) 68 69 (typecheck-fail 70 (pack (Int (tup [a = 5] [f = (λ ([x : Int]) (+ x 1))])) 71 as (∃ (X) (× [a : X] [f : (→ X Bool)])))) 72 73 (check-type 74 (pack (Bool (tup [a = #t] [f = (λ ([x : Bool]) (if x 1 2))])) 75 as (∃ (X) (× [a : X] [f : (→ X Int)]))) 76 : (∃ (X) (× [a : X] [f : (→ X Int)]))) 77 78 (define counterADT 79 (pack (Int (tup [new = 1] 80 [get = (λ ([i : Int]) i)] 81 [inc = (λ ([i : Int]) (+ i 1))])) 82 as (∃ (Counter) (× [new : Counter] 83 [get : (→ Counter Int)] 84 [inc : (→ Counter Counter)])))) 85 (check-type counterADT : 86 (∃ (Counter) (× [new : Counter] 87 [get : (→ Counter Int)] 88 [inc : (→ Counter Counter)]))) 89 (typecheck-fail 90 (open [counter <= counterADT with Counter] 91 (+ (proj counter new) 1)) 92 #:with-msg "expected: +Int, Int\n *given: +Counter, Int\n *expressions: \\(proj counter new\\), 1") 93 (typecheck-fail 94 (open [counter <= counterADT with Counter] 95 ((λ ([x : Int]) x) (proj counter new))) 96 #:with-msg "expected: +Int\n *given: +Counter\n *expressions: \\(proj counter new\\)") 97 (check-type 98 (open [counter <= counterADT with Counter] 99 ((proj counter get) ((proj counter inc) (proj counter new)))) 100 : Int ⇒ 2) 101 102 (check-type 103 (open [counter <= counterADT with Counter] 104 (let ([inc (proj counter inc)] 105 [get (proj counter get)]) 106 (let ([add3 (λ ([c : Counter]) (inc (inc (inc c))))]) 107 (get (add3 (proj counter new)))))) 108 : Int ⇒ 4) 109 110 (check-type 111 (open [counter <= counterADT with Counter] 112 (let ([get (proj counter get)] 113 [inc (proj counter inc)] 114 [new (λ () (proj counter new))]) 115 (letrec ([(is-even? : (→ Int Bool)) 116 (λ ([n : Int]) 117 (or (zero? n) 118 (is-odd? (sub1 n))))] 119 [(is-odd? : (→ Int Bool)) 120 (λ ([n : Int]) 121 (and (not (zero? n)) 122 (is-even? (sub1 n))))]) 123 (open [flipflop <= 124 (pack (Counter (tup [new = (new)] 125 [read = (λ ([c : Counter]) (is-even? (get c)))] 126 [toggle = (λ ([c : Counter]) (inc c))] 127 [reset = (λ ([c : Counter]) (new))])) 128 as (∃ (FlipFlop) (× [new : FlipFlop] 129 [read : (→ FlipFlop Bool)] 130 [toggle : (→ FlipFlop FlipFlop)] 131 [reset : (→ FlipFlop FlipFlop)]))) 132 with FlipFlop] 133 (let ([read (proj flipflop read)] 134 [togg (proj flipflop toggle)]) 135 (read (togg (togg (togg (togg (proj flipflop new))))))))))) 136 : Bool ⇒ #f) 137 138 (define counterADT2 139 (pack ((× [x : Int]) 140 (tup [new = (tup [x = 1])] 141 [get = (λ ([i : (× [x : Int])]) (proj i x))] 142 [inc = (λ ([i : (× [x : Int])]) (tup [x = (+ 1 (proj i x))]))])) 143 as (∃ (Counter) (× [new : Counter] 144 [get : (→ Counter Int)] 145 [inc : (→ Counter Counter)])))) 146 (check-type counterADT2 : 147 (∃ (Counter) (× [new : Counter] 148 [get : (→ Counter Int)] 149 [inc : (→ Counter Counter)]))) 150 151 ;; same as above, but with different internal counter representation 152 (check-type 153 (open [counter <= counterADT2 with Counter] 154 (let ([get (proj counter get)] 155 [inc (proj counter inc)] 156 [new (λ () (proj counter new))]) 157 (letrec ([(is-even? : (→ Int Bool)) 158 (λ ([n : Int]) 159 (or (zero? n) 160 (is-odd? (sub1 n))))] 161 [(is-odd? : (→ Int Bool)) 162 (λ ([n : Int]) 163 (and (not (zero? n)) 164 (is-even? (sub1 n))))]) 165 (open [flipflop <= 166 (pack (Counter (tup [new = (new)] 167 [read = (λ ([c : Counter]) (is-even? (get c)))] 168 [toggle = (λ ([c : Counter]) (inc c))] 169 [reset = (λ ([c : Counter]) (new))])) 170 as (∃ (FlipFlop) (× [new : FlipFlop] 171 [read : (→ FlipFlop Bool)] 172 [toggle : (→ FlipFlop FlipFlop)] 173 [reset : (→ FlipFlop FlipFlop)]))) 174 with 175 FlipFlop] 176 (let ([read (proj flipflop read)] 177 [togg (proj flipflop toggle)]) 178 (read (togg (togg (togg (togg (proj flipflop new))))))))))) 179 : Bool ⇒ #f) 180 181 ;; err cases 182 (typecheck-fail 183 (pack (Int 1) as Int) 184 #:with-msg 185 "Expected ∃ type, got: Int") 186 (typecheck-fail 187 (open [x <= 2 with X] 3) 188 #:with-msg 189 "Expected ∃ type, got: Int") 190 191 ;; previous tets from stlc+reco+var-tests.rkt --------------------------------- 192 ;; define-type-alias 193 (define-type-alias Integer Int) 194 (define-type-alias ArithBinOp (→ Int Int Int)) 195 ;(define-type-alias C Complex) ; error, Complex undefined 196 197 (check-type ((λ ([x : Int]) (+ x 2)) 3) : Integer) 198 (check-type ((λ ([x : Integer]) (+ x 2)) 3) : Int) 199 (check-type ((λ ([x : Integer]) (+ x 2)) 3) : Integer) 200 (check-type + : ArithBinOp) 201 (check-type (λ ([f : ArithBinOp]) (f 1 2)) : (→ (→ Int Int Int) Int)) 202 203 ;; records (ie labeled tuples) 204 (check-type "Stephen" : String) 205 (check-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) : 206 (× [name : String] [phone : Int] [male? : Bool])) 207 (check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) name) 208 : String ⇒ "Stephen") 209 (check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) name) 210 : String ⇒ "Stephen") 211 (check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) phone) 212 : Int ⇒ 781) 213 (check-type (proj (tup [name = "Stephen"] [phone = 781] [male? = #t]) male?) 214 : Bool ⇒ #t) 215 (check-not-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) : 216 (× [my-name : String] [phone : Int] [male? : Bool])) 217 (check-not-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) : 218 (× [name : String] [my-phone : Int] [male? : Bool])) 219 (check-not-type (tup [name = "Stephen"] [phone = 781] [male? = #t]) : 220 (× [name : String] [phone : Int] [is-male? : Bool])) 221 222 ;; variants 223 (check-type (var coffee = (void) as (∨ [coffee : Unit])) : (∨ [coffee : Unit])) 224 (check-not-type (var coffee = (void) as (∨ [coffee : Unit])) : (∨ [coffee : Unit] [tea : Unit])) 225 (typecheck-fail ((λ ([x : (∨ [coffee : Unit] [tea : Unit])]) x) 226 (var coffee = (void) as (∨ [coffee : Unit])))) 227 (check-type (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit])) : (∨ [coffee : Unit] [tea : Unit])) 228 (check-type (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit] [coke : Unit])) 229 : (∨ [coffee : Unit] [tea : Unit] [coke : Unit])) 230 231 (typecheck-fail 232 (case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit])) 233 [coffee x => 1])) ; not enough clauses 234 (typecheck-fail 235 (case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit])) 236 [coffee x => 1] 237 [teaaaaaa x => 2])) ; wrong clause 238 (typecheck-fail 239 (case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit])) 240 [coffee x => 1] 241 [tea x => 2] 242 [coke x => 3])) ; too many clauses 243 (typecheck-fail 244 (case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit])) 245 [coffee x => "1"] 246 [tea x => 2])) ; mismatched branch types 247 (check-type 248 (case (var coffee = 1 as (∨ [coffee : Int] [tea : Unit])) 249 [coffee x => x] 250 [tea x => 2]) : Int ⇒ 1) 251 (define-type-alias Drink (∨ [coffee : Int] [tea : Unit] [coke : Bool])) 252 (check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20) 253 (check-type (λ ([x : Int]) (+ (+ x x) (+ x x))) : (→ Int Int)) 254 (check-type 255 (case ((λ ([d : Drink]) d) 256 (var coffee = 1 as (∨ [coffee : Int] [tea : Unit] [coke : Bool]))) 257 [coffee x => (+ (+ x x) (+ x x))] 258 [tea x => 2] 259 [coke y => 3]) 260 : Int ⇒ 4) 261 262 (check-type 263 (case ((λ ([d : Drink]) d) (var coffee = 1 as Drink)) 264 [coffee x => (+ (+ x x) (+ x x))] 265 [tea x => 2] 266 [coke y => 3]) 267 : Int ⇒ 4) 268 269 ;; previous tests: ------------------------------------------------------------ 270 ;; tests for tuples ----------------------------------------------------------- 271 ;; old tuple syntax not supported here 272 ;(check-type (tup 1 2 3) : (× Int Int Int)) 273 ;(check-type (tup 1 "1" #f +) : (× Int String Bool (→ Int Int Int))) 274 ;(check-not-type (tup 1 "1" #f +) : (× Unit String Bool (→ Int Int Int))) 275 ;(check-not-type (tup 1 "1" #f +) : (× Int Unit Bool (→ Int Int Int))) 276 ;(check-not-type (tup 1 "1" #f +) : (× Int String Unit (→ Int Int Int))) 277 ;(check-not-type (tup 1 "1" #f +) : (× Int String Bool (→ Int Int Unit))) 278 ; 279 ;(check-type (proj (tup 1 "2" #f) 0) : Int ⇒ 1) 280 ;(check-type (proj (tup 1 "2" #f) 1) : String ⇒ "2") 281 ;(check-type (proj (tup 1 "2" #f) 2) : Bool ⇒ #f) 282 ;(typecheck-fail (proj (tup 1 "2" #f) 3)) ; index too large 283 ;(typecheck-fail (proj 1 2)) ; not tuple 284 285 ;; ext-stlc.rkt tests --------------------------------------------------------- 286 ;; should still pass 287 288 ;; new literals and base types 289 (check-type "one" : String) ; literal now supported 290 (check-type #f : Bool) ; literal now supported 291 292 (check-type (λ ([x : Bool]) x) : (→ Bool Bool)) ; Bool is now valid type 293 294 ;; Unit 295 (check-type (void) : Unit) 296 (check-type void : (→ Unit)) 297 (typecheck-fail ((λ ([x : Unit]) x) 2)) 298 (typecheck-fail ((λ ([x : Unit])) void)) 299 (check-type ((λ ([x : Unit]) x) (void)) : Unit) 300 301 ;; begin 302 (typecheck-fail (begin)) 303 (check-type (begin 1) : Int) 304 ;(typecheck-fail (begin 1 2 3)) 305 (check-type (begin (void) 1) : Int ⇒ 1) 306 307 ;;ascription 308 (typecheck-fail (ann 1 : Bool)) 309 (check-type (ann 1 : Int) : Int ⇒ 1) 310 (check-type ((λ ([x : Int]) (ann x : Int)) 10) : Int ⇒ 10) 311 312 ; let 313 (check-type (let () (+ 1 1)) : Int ⇒ 2) 314 (check-type (let ([x 10]) (+ 1 2)) : Int) 315 (typecheck-fail (let ([x #f]) (+ x 1))) 316 (check-type (let ([x 10] [y 20]) ((λ ([z : Int] [a : Int]) (+ a z)) x y)) : Int ⇒ 30) 317 (typecheck-fail (let ([x 10] [y (+ x 1)]) (+ x y))) ; unbound identifier 318 319 (check-type (let* ([x 10] [y (+ x 1)]) (+ x y)) : Int ⇒ 21) 320 (typecheck-fail (let* ([x #t] [y (+ x 1)]) 1)) 321 322 ; letrec 323 (typecheck-fail (letrec ([(x : Int) #f] [(y : Int) 1]) y)) 324 (typecheck-fail (letrec ([(y : Int) 1] [(x : Int) #f]) x)) 325 326 (check-type (letrec ([(x : Int) 1] [(y : Int) (+ x 1)]) (+ x y)) : Int ⇒ 3) 327 328 ;; recursive 329 (check-type 330 (letrec ([(countdown : (→ Int String)) 331 (λ ([i : Int]) 332 (if (= i 0) 333 "liftoff" 334 (countdown (- i 1))))]) 335 (countdown 10)) : String ⇒ "liftoff") 336 337 ;; mutually recursive 338 (check-type 339 (letrec ([(is-even? : (→ Int Bool)) 340 (λ ([n : Int]) 341 (or (zero? n) 342 (is-odd? (sub1 n))))] 343 [(is-odd? : (→ Int Bool)) 344 (λ ([n : Int]) 345 (and (not (zero? n)) 346 (is-even? (sub1 n))))]) 347 (is-odd? 11)) : Bool ⇒ #t) 348 349 ;; tests from stlc+lit-tests.rkt -------------------------- 350 ; most should pass, some failing may now pass due to added types/forms 351 (check-type 1 : Int) 352 ;(check-not-type 1 : (Int → Int)) 353 ;(typecheck-fail "one") ; literal now supported 354 ;(typecheck-fail #f) ; literal now supported 355 (check-type (λ ([x : Int] [y : Int]) x) : (→ Int Int Int)) 356 (check-not-type (λ ([x : Int]) x) : Int) 357 (check-type (λ ([x : Int]) x) : (→ Int Int)) 358 (check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) Int)) 359 (check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1) 360 (typecheck-fail ((λ ([x : Bool]) x) 1)) ; Bool now valid type, but arg has wrong type 361 ;(typecheck-fail (λ ([x : Bool]) x)) ; Bool is now valid type 362 (typecheck-fail (λ ([f : Int]) (f 1 2))) ; applying f with non-fn type 363 (check-type (λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) 364 : (→ (→ Int Int Int) Int Int Int)) 365 (check-type ((λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) + 1 2) : Int ⇒ 3) 366 (typecheck-fail (+ 1 (λ ([x : Int]) x))) ; adding non-Int 367 (typecheck-fail (λ ([x : (→ Int Int)]) (+ x x))) ; x should be Int 368 (typecheck-fail ((λ ([x : Int] [y : Int]) y) 1)) ; wrong number of args 369 (check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20) 370