stlc+rec-iso-tests.rkt (9419B)
1 #lang s-exp "../stlc+rec-iso.rkt" 2 (require "rackunit-typechecking.rkt") 3 4 (define-type-alias IntList (μ (X) (∨ [nil : Unit] [cons : (× Int X)]))) 5 (define-type-alias ILBody (∨ [nil : Unit] [cons : (× Int IntList)])) 6 7 ;; nil 8 (define nil (fld {IntList} (var nil = (void) as ILBody))) 9 (check-type nil : IntList) 10 11 ;; cons 12 (define cons (λ ([n : Int] [lst : IntList]) (fld {IntList} (var cons = (tup n lst) as ILBody)))) 13 (check-type cons : (→ Int IntList IntList)) 14 (check-type (cons 1 nil) : IntList) 15 (typecheck-fail (cons 1 2)) 16 (typecheck-fail (cons "1" nil)) 17 18 ;; isnil 19 (define isnil 20 (λ ([lst : IntList]) 21 (case (unfld {IntList} lst) 22 [nil n => #t] 23 [cons p => #f]))) 24 (check-type isnil : (→ IntList Bool)) 25 (check-type (isnil nil) : Bool ⇒ #t) 26 (check-type (isnil (cons 1 nil)) : Bool ⇒ #f) 27 (typecheck-fail (isnil 1)) 28 (typecheck-fail (isnil (cons 1 2))) 29 (check-type (λ ([f : (→ IntList Bool)]) (f nil)) : (→ (→ IntList Bool) Bool)) 30 (check-type ((λ ([f : (→ IntList Bool)]) (f nil)) isnil) : Bool ⇒ #t) 31 32 ;; hd 33 (define hd 34 (λ ([lst : IntList]) 35 (case (unfld {IntList} lst) 36 [nil n => 0] 37 [cons p => (proj p 0)]))) 38 (check-type hd : (→ IntList Int)) 39 (check-type (hd nil) : Int ⇒ 0) 40 (typecheck-fail (hd 1)) 41 (check-type (hd (cons 11 nil)) : Int ⇒ 11) 42 43 ;; tl 44 (define tl 45 (λ ([lst : IntList]) 46 (case (unfld {IntList} lst) 47 [nil n => lst] 48 [cons p => (proj p 1)]))) 49 (check-type tl : (→ IntList IntList)) 50 (check-type (tl nil) : IntList ⇒ nil) 51 (check-type (tl (cons 1 nil)) : IntList ⇒ nil) 52 (check-type (tl (cons 1 (cons 2 nil))) : IntList ⇒ (cons 2 nil)) 53 (typecheck-fail (tl 1)) 54 55 ;; some typecheck failure msgs 56 (typecheck-fail 57 (fld {Int} 1) 58 #:with-msg 59 "Expected μ type, got: Int") 60 (typecheck-fail 61 (unfld {Int} 1) 62 #:with-msg 63 "Expected μ type, got: Int") 64 65 ;; previous stlc+var tests ---------------------------------------------------- 66 ;; define-type-alias 67 (define-type-alias Integer Int) 68 (define-type-alias ArithBinOp (→ Int Int Int)) 69 ;(define-type-alias C Complex) ; error, Complex undefined 70 71 (check-type ((λ ([x : Int]) (+ x 2)) 3) : Integer) 72 (check-type ((λ ([x : Integer]) (+ x 2)) 3) : Int) 73 (check-type ((λ ([x : Integer]) (+ x 2)) 3) : Integer) 74 (check-type + : ArithBinOp) 75 (check-type (λ ([f : ArithBinOp]) (f 1 2)) : (→ (→ Int Int Int) Int)) 76 77 ;; records (ie labeled tuples) 78 ; no records, only tuples 79 (check-type "Stephen" : String) 80 ;(check-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) : 81 ; (× [: "name" String] [: "phone" Int] [: "male?" Bool])) 82 ;(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "name") 83 ; : String ⇒ "Stephen") 84 ;(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "name") 85 ; : String ⇒ "Stephen") 86 ;(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "phone") 87 ; : Int ⇒ 781) 88 ;(check-type (proj (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) "male?") 89 ; : Bool ⇒ #t) 90 ;(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) : 91 ; (× [: "my-name" String] [: "phone" Int] [: "male?" Bool])) 92 ;(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) : 93 ; (× [: "name" String] [: "my-phone" Int] [: "male?" Bool])) 94 ;(check-not-type (tup ["name" = "Stephen"] ["phone" = 781] ["male?" = #t]) : 95 ; (× [: "name" String] [: "phone" Int] [: "is-male?" Bool])) 96 97 ;; variants 98 (check-type (var coffee = (void) as (∨ [coffee : Unit])) : (∨ [coffee : Unit])) 99 (check-not-type (var coffee = (void) as (∨ [coffee : Unit])) : (∨ [coffee : Unit] [tea : Unit])) 100 (typecheck-fail ((λ ([x : (∨ [coffee : Unit] [tea : Unit])]) x) 101 (var coffee = (void) as (∨ [coffee : Unit])))) 102 (check-type (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit])) : (∨ [coffee : Unit] [tea : Unit])) 103 (check-type (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit] [coke : Unit])) 104 : (∨ [coffee : Unit] [tea : Unit] [coke : Unit])) 105 106 (typecheck-fail 107 (case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit])) 108 [coffee x => 1])) ; not enough clauses 109 (typecheck-fail 110 (case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit])) 111 [coffee x => 1] 112 [teaaaaaa x => 2])) ; wrong clause 113 (typecheck-fail 114 (case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit])) 115 [coffee x => 1] 116 [tea x => 2] 117 [coke x => 3])) ; too many clauses 118 (typecheck-fail 119 (case (var coffee = (void) as (∨ [coffee : Unit] [tea : Unit])) 120 [coffee x => "1"] 121 [tea x => 2])) ; mismatched branch types 122 (check-type 123 (case (var coffee = 1 as (∨ [coffee : Int] [tea : Unit])) 124 [coffee x => x] 125 [tea x => 2]) : Int ⇒ 1) 126 (define-type-alias Drink (∨ [coffee : Int] [tea : Unit] [coke : Bool])) 127 (check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20) 128 (check-type (λ ([x : Int]) (+ (+ x x) (+ x x))) : (→ Int Int)) 129 (check-type 130 (case ((λ ([d : Drink]) d) 131 (var coffee = 1 as (∨ [coffee : Int] [tea : Unit] [coke : Bool]))) 132 [coffee x => (+ (+ x x) (+ x x))] 133 [tea x => 2] 134 [coke y => 3]) 135 : Int ⇒ 4) 136 137 (check-type 138 (case ((λ ([d : Drink]) d) (var coffee = 1 as Drink)) 139 [coffee x => (+ (+ x x) (+ x x))] 140 [tea x => 2] 141 [coke y => 3]) 142 : Int ⇒ 4) 143 144 ;; previous tests: ------------------------------------------------------------ 145 ;; tests for tuples ----------------------------------------------------------- 146 (check-type (tup 1 2 3) : (× Int Int Int)) 147 (check-type (tup 1 "1" #f +) : (× Int String Bool (→ Int Int Int))) 148 (check-not-type (tup 1 "1" #f +) : (× Unit String Bool (→ Int Int Int))) 149 (check-not-type (tup 1 "1" #f +) : (× Int Unit Bool (→ Int Int Int))) 150 (check-not-type (tup 1 "1" #f +) : (× Int String Unit (→ Int Int Int))) 151 (check-not-type (tup 1 "1" #f +) : (× Int String Bool (→ Int Int Unit))) 152 153 (check-type (proj (tup 1 "2" #f) 0) : Int ⇒ 1) 154 (check-type (proj (tup 1 "2" #f) 1) : String ⇒ "2") 155 (check-type (proj (tup 1 "2" #f) 2) : Bool ⇒ #f) 156 (typecheck-fail (proj (tup 1 "2" #f) 3)) ; index too large 157 (typecheck-fail 158 (proj 1 2) 159 #:with-msg 160 "Expected × type, got: Int") 161 162 ;; ext-stlc.rkt tests --------------------------------------------------------- 163 ;; should still pass 164 165 ;; new literals and base types 166 (check-type "one" : String) ; literal now supported 167 (check-type #f : Bool) ; literal now supported 168 169 (check-type (λ ([x : Bool]) x) : (→ Bool Bool)) ; Bool is now valid type 170 171 ;; Unit 172 (check-type (void) : Unit) 173 (check-type void : (→ Unit)) 174 (typecheck-fail ((λ ([x : Unit]) x) 2)) 175 (typecheck-fail ((λ ([x : Unit])) void)) 176 (check-type ((λ ([x : Unit]) x) (void)) : Unit) 177 178 ;; begin 179 (typecheck-fail (begin)) 180 (check-type (begin 1) : Int) 181 ;(typecheck-fail (begin 1 2 3)) 182 (check-type (begin (void) 1) : Int ⇒ 1) 183 184 ;;ascription 185 (typecheck-fail (ann 1 : Bool)) 186 (check-type (ann 1 : Int) : Int ⇒ 1) 187 (check-type ((λ ([x : Int]) (ann x : Int)) 10) : Int ⇒ 10) 188 189 ; let 190 (check-type (let () (+ 1 1)) : Int ⇒ 2) 191 (check-type (let ([x 10]) (+ 1 2)) : Int) 192 (typecheck-fail (let ([x #f]) (+ x 1))) 193 (check-type (let ([x 10] [y 20]) ((λ ([z : Int] [a : Int]) (+ a z)) x y)) : Int ⇒ 30) 194 (typecheck-fail (let ([x 10] [y (+ x 1)]) (+ x y))) ; unbound identifier 195 196 (check-type (let* ([x 10] [y (+ x 1)]) (+ x y)) : Int ⇒ 21) 197 (typecheck-fail (let* ([x #t] [y (+ x 1)]) 1)) 198 199 ; letrec 200 (typecheck-fail (letrec ([(x : Int) #f] [(y : Int) 1]) y)) 201 (typecheck-fail (letrec ([(y : Int) 1] [(x : Int) #f]) x)) 202 203 (check-type (letrec ([(x : Int) 1] [(y : Int) (+ x 1)]) (+ x y)) : Int ⇒ 3) 204 205 ;; recursive 206 (check-type 207 (letrec ([(countdown : (→ Int String)) 208 (λ ([i : Int]) 209 (if (= i 0) 210 "liftoff" 211 (countdown (- i 1))))]) 212 (countdown 10)) : String ⇒ "liftoff") 213 214 ;; mutually recursive 215 (check-type 216 (letrec ([(is-even? : (→ Int Bool)) 217 (λ ([n : Int]) 218 (or (zero? n) 219 (is-odd? (sub1 n))))] 220 [(is-odd? : (→ Int Bool)) 221 (λ ([n : Int]) 222 (and (not (zero? n)) 223 (is-even? (sub1 n))))]) 224 (is-odd? 11)) : Bool ⇒ #t) 225 226 ;; tests from stlc+lit-tests.rkt -------------------------- 227 ; most should pass, some failing may now pass due to added types/forms 228 (check-type 1 : Int) 229 ;(check-not-type 1 : (Int → Int)) 230 ;(typecheck-fail "one") ; literal now supported 231 ;(typecheck-fail #f) ; literal now supported 232 (check-type (λ ([x : Int] [y : Int]) x) : (→ Int Int Int)) 233 (check-not-type (λ ([x : Int]) x) : Int) 234 (check-type (λ ([x : Int]) x) : (→ Int Int)) 235 (check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) Int)) 236 (check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1) 237 (typecheck-fail ((λ ([x : Bool]) x) 1)) ; Bool now valid type, but arg has wrong type 238 ;(typecheck-fail (λ ([x : Bool]) x)) ; Bool is now valid type 239 (typecheck-fail (λ ([f : Int]) (f 1 2))) ; applying f with non-fn type 240 (check-type (λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) 241 : (→ (→ Int Int Int) Int Int Int)) 242 (check-type ((λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) + 1 2) : Int ⇒ 3) 243 (typecheck-fail (+ 1 (λ ([x : Int]) x))) ; adding non-Int 244 (typecheck-fail (λ ([x : (→ Int Int)]) (+ x x))) ; x should be Int 245 (typecheck-fail ((λ ([x : Int] [y : Int]) y) 1)) ; wrong number of args 246 (check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20) 247