www

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

stlc+lit-tests.rkt (2361B)

      1 #lang s-exp "../stlc+lit.rkt"
      2 (require "rackunit-typechecking.rkt")
      3 
      4 ;; thunk
      5 (check-type (λ () 1) : (→ Int))
      6 
      7 (check-type 1 : Int)
      8 (check-not-type 1 : (→ Int Int))
      9 
     10 (typecheck-fail "one" #:with-msg "Unsupported literal")
     11 (typecheck-fail #f #:with-msg "Unsupported literal")
     12 
     13 (check-type (λ ([x : Int] [y : Int]) x) : (→ Int Int Int))
     14 (check-not-type (λ ([x : Int]) x) : Int)
     15 (check-type (λ ([x : Int]) x) : (→ Int Int))
     16 
     17 (typecheck-fail
     18  (λ ([x : →]) x)
     19  #:with-msg "Improper usage of type constructor →: →, expected >= 1 arguments")
     20 (typecheck-fail
     21  (λ ([x : (→ →)]) x)
     22  #:with-msg "Improper usage of type constructor →: →, expected >= 1 arguments")
     23 (typecheck-fail
     24  (λ ([x : (→)]) x)
     25  #:with-msg "Improper usage of type constructor →: \\(→\\), expected >= 1 arguments")
     26 
     27 (check-type (λ ([f : (→ Int Int)]) 1) : (→ (→ Int Int) Int))
     28 (check-type ((λ ([x : Int]) x) 1) : Int ⇒ 1)
     29 
     30 (typecheck-fail ((λ ([x : Bool]) x) 1)
     31                 #:with-msg "Bool: unbound identifier")
     32 (typecheck-fail (λ ([x : (→ Bool Bool)]) x)
     33                 #:with-msg "Bool: unbound identifier")
     34 (typecheck-fail (λ ([x : Bool]) x)
     35                 #:with-msg "Bool: unbound identifier")
     36 (typecheck-fail
     37  (λ ([f : Int]) (f 1 2))
     38  #:with-msg
     39  "Expected → type, got: Int")
     40 
     41 (check-type (λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y))
     42             : (→ (→ Int Int Int) Int Int Int))
     43 (check-type ((λ ([f : (→ Int Int Int)] [x : Int] [y : Int]) (f x y)) + 1 2) : Int ⇒ 3)
     44 
     45 (typecheck-fail
     46  (+ 1 (λ ([x : Int]) x))
     47  #:with-msg (string-append "expected: +Int, Int\n *given: +Int, \\(→ Int Int\\)\n"
     48                            " *expressions: 1, \\(λ \\(\\(x : Int\\)\\) x\\)"))
     49 (typecheck-fail
     50  (λ ([x : (→ Int Int)]) (+ x x))
     51   #:with-msg "expected: +Int, Int\n *given: +\\(→ Int Int\\), \\(→ Int Int\\)\n *expressions: x, x")
     52 (typecheck-fail
     53  ((λ ([x : Int] [y : Int]) y) 1)
     54  #:with-msg "wrong number of arguments: expected 2, given 1")
     55 
     56 (check-type ((λ ([x : Int]) (+ x x)) 10) : Int ⇒ 20)
     57 
     58 (typecheck-fail (λ ([x : (→ 1 2)]) x) #:with-msg "not a well-formed type")
     59 (typecheck-fail (λ ([x : 1]) x) #:with-msg "not a well-formed type")
     60 (typecheck-fail (λ ([x : (+ 1 2)]) x) #:with-msg "not a well-formed type")
     61 (typecheck-fail (λ ([x : (λ ([y : Int]) y)]) x) #:with-msg "not a well-formed type")