www

Unnamed repository; edit this file 'description' to name the repository.
Log | Files | Refs | README

stlc+union+case.rkt (4410B)

      1 #lang s-exp "../stlc+union+case.rkt"
      2 (require "rackunit-typechecking.rkt")
      3 
      4 (check-type 1 : Nat)
      5 (check-type -1 : NegInt)
      6 (check-type 1.1 : Float)
      7 (check-type (+ 1 1.1) : Num -> 2.1)
      8 (check-type (+ 1.1 1) : Num -> 2.1)
      9 (typecheck-fail (+ "1" 1) #:with-msg "expected Num, given String")
     10 
     11 ;; case-> subtyping
     12 (check-type ((λ ([f : (→ Int Int)]) (f 10)) add1) : Int -> 11)
     13 (check-type ((λ ([f : (case-> (→ Int Int))]) (f 10)) add1) : Int -> 11)
     14 (check-type ((λ ([f : (case-> (→ Nat Nat)
     15                               (→ Int Int))]) (f 10)) add1) : Int -> 11)
     16 (check-not-type ((λ ([f : (case-> (→ Int Int))]) (f 10)) add1) : Nat)
     17 (check-type ((λ ([f : (case-> (→ Nat Nat)
     18                               (→ Int Int))]) (f 10)) add1) : Nat -> 11)
     19 (typecheck-fail ((λ ([f : (case-> (→ Zero Zero)
     20                                   (→ Int Int))]) (f 10)) add1) 
     21  #:with-msg "expected \\(case-> \\(→ Zero Zero\\) \\(→ Int Int\\)\\), given \\(case→ \\(→ Nat Nat\\) \\(→ Int Int\\)")
     22 
     23 ;; Alex's example
     24 ;; illustrates flattening
     25 (define-type-alias A Int)
     26 (define-type-alias B String)
     27 (define-type-alias C Bool)
     28 (define-type-alias AC (U A C))
     29 (define-type-alias BC (U B C))
     30 (define-type-alias A-BC (U A BC))
     31 (define-type-alias B-AC (U B AC))
     32 (check-type ((λ ([x : A-BC]) x) ((λ ([x : B-AC]) x) "1")) : A-BC -> "1")
     33 
     34 ; check pruning and collapsing
     35 (define-type-alias NN (U Nat Nat))
     36 (check-type ((λ ([x : NN]) x) 1) : Nat -> 1)
     37 (define-type-alias NNN (U (U Nat Nat) (U (U Nat Nat Nat) (U Nat Nat))))
     38 (check-type ((λ ([x : NNN]) x) 1) : Nat -> 1)
     39 
     40 ; check that pruning and collapsing don't throw away types when the union
     41 ; contains another empty union
     42 (typecheck-fail
     43  (λ ([x : (U (U) String)])
     44    (ann x : (U)))
     45  #:with-msg
     46  "expected \\(U\\), given \\(U \\(U\\) String\\)")
     47 
     48 
     49 ;; tests from stlc+sub ---------------------
     50 (check-type 1 : Num)
     51 (check-type 1 : Int)
     52 (check-type -1 : Num)
     53 (check-type -1 : Int)
     54 (check-not-type -1 : Nat)
     55 (check-type ((λ ([x : Num]) x) -1) : Num ⇒ -1)
     56 (check-type ((λ ([x : Int]) x) -1) : Int ⇒ -1)
     57 (typecheck-fail ((λ ([x : Nat]) x) -1) #:with-msg "expected Nat, given NegInt")
     58 (check-type (λ ([x : Int]) x) : (→ Int Int))
     59 ; TODO: no function subtypes for now
     60 ;(check-type (λ ([x : Int]) x) : (→ Int Num)) ; covariant output
     61 (check-not-type (λ ([x : Int]) x) : (→ Int Nat))
     62 ;(check-type (λ ([x : Int]) x) : (→ Nat Int)) ; contravariant input
     63 (check-not-type (λ ([x : Int]) x) : (→ Num Int))
     64 
     65 (check-type ((λ ([f : (→ Int Int)]) (f -1)) add1) : Int ⇒ 0)
     66 ; (check-type ((λ ([f : (→ Nat Int)]) (f 1)) add1) : Int ⇒ 2)
     67 (typecheck-fail ((λ ([f : (→ Num Int)]) (f 1.1)) add1))
     68 ;(check-type ((λ ([f : (→ Nat Num)]) (f 1)) add1) : Num ⇒ 2)
     69 (typecheck-fail ((λ ([f : (→ Num Num)]) (f 1.1)) add1))
     70 
     71 (check-type + : (→ Num Num Num))
     72 ;(check-type + : (→ Int Num Num))
     73 ;(check-type + : (→ Int Int Num))
     74 ;(check-not-type + : (→ Top Int Num))
     75 (check-not-type + : (→ Int Int Int))
     76 ;(check-type + : (→ Nat Int Top))
     77 
     78 ;; previous tests -------------------------------------------------------------
     79 ;; some change due to more specific types
     80 (check-not-type 1 : (→ Int Int))
     81 (check-type "one" : String) 
     82 (check-type #f : Bool)
     83 (check-type (λ ([x : Int] [y : Int]) x) : (→ Int Int Int))
     84 (check-type ((λ ([x : Int] [y : Int]) x) -1 1) : Int -> -1)
     85 (check-not-type (λ ([x : Int]) x) : Int)
     86 (check-type (λ ([x : Int]) x) : (→ Int Int))
     87 (check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) PosInt))
     88 (check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) Nat))
     89 (check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1)
     90 (typecheck-fail ((λ ([x : Sym]) x) 1)) ; Sym is not valid type
     91 (typecheck-fail (λ ([x : Sym]) x)) ; Sym is not valid type
     92 (typecheck-fail (λ ([f : Int]) (f 1 2))) ; applying f with non-fn type
     93 (check-type (λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y))
     94             : (→ (→ Int Int Int) Int Int Int))
     95 (check-type ((λ ([f : (→ Num Num Num)] [x : Int] [y : Int]) (f x y)) + 1 2) : Num ⇒ 3)
     96 (typecheck-fail (+ 1 (λ ([x : Int]) x))) ; adding non-Int
     97 (typecheck-fail (λ ([x : (→ Int Int)]) (+ x x))) ; x should be Int
     98 (typecheck-fail ((λ ([x : Int] [y : Int]) y) 1)) ; wrong number of args
     99 (check-type ((λ ([x : Int]) (+ x x)) 10) : Num ⇒ 20)
    100 
    101 (check-not-type (λ ([x : Int] [y : Int]) x) : (→ Int Int))
    102 (check-not-type (λ ([x : Int]) x) : (→ Int Int Int Int))