www

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

stlc+overloading-tests.rkt (2881B)

      1 #lang s-exp "../stlc+overloading.rkt"
      2 (require turnstile/examples/tests/rackunit-typechecking)
      3 
      4 ;; -----------------------------------------------------------------------------
      5 ;; --- syntax for ψ types
      6 
      7 (typecheck-fail
      8  (signature (to-string0 α) (→ α Str Str))
      9  #:with-msg "Expected")
     10 
     11 (typecheck-fail
     12  (signature (to-string0 α) (→ Str Str))
     13  #:with-msg "Expected")
     14 
     15 (typecheck-fail
     16  (signature (to-string0 α) (→ α Str))
     17  #:with-msg "not allowed in an expression context")
     18 
     19 ;; -----------------------------------------------------------------------------
     20 ;; --- basic overloading
     21 
     22 ;; (signature (to-string α) (→ α Str))
     23 
     24 ;; (typecheck-fail
     25 ;;  (to-string 1)
     26 ;;  #:with-msg "Resolution for 'to-string' failed")
     27 
     28 ;; (typecheck-fail
     29 ;;  (to-string "yolo")
     30 ;;  #:with-msg "Resolution for 'to-string' failed")
     31 
     32 ;; ;; -- can later add cases to an overloaded name
     33 ;; (instance (to-string Nat)
     34 ;;   (λ ([x : Nat]) "nat"))
     35 
     36 ;; (instance (to-string Str)
     37 ;;   (λ ([x : Str]) "string"))
     38 
     39 ;; (check-type
     40 ;;  (to-string 3)
     41 ;;  : Str ⇒ "nat")
     42 
     43 ;; (typecheck-fail
     44 ;;  (to-string (+ 0 0))
     45 ;;  #:with-msg "Resolution for 'to-string' failed")
     46 
     47 ;; (instance (to-string Num)
     48 ;;   (λ ([x : Num]) "num"))
     49 
     50 ;; (check-type
     51 ;;  (to-string (+ 2 2))
     52 ;;  : Str ⇒ "num")
     53 
     54 ;; (check-type
     55 ;;  (to-string -1)
     56 ;;  : Str ⇒ "num")
     57 
     58 ;; (check-type
     59 ;;  (to-string "hi")
     60 ;;  : Str ⇒ "string")
     61 
     62 ;; ;; -- use 'resolve' to get exact matches
     63 
     64 ;; (check-type
     65 ;;  ((resolve to-string Nat) 1)
     66 ;;  : Str ⇒ "nat")
     67 
     68 ;; (check-type
     69 ;;  ((resolve to-string Num) 1)
     70 ;;  : Str ⇒ "num")
     71 
     72 ;; (typecheck-fail
     73 ;;  (resolve to-string Int)
     74 ;;  #:with-msg "Resolution for 'to-string' failed")
     75 
     76 ;; (typecheck-fail
     77 ;;  ((resolve to-string Num) "hello")
     78 ;;  #:with-msg "expected: +Num\n *given: +Str\n *expressions: \"hello\"")
     79 
     80 ;; ;; -- instances are type-checked. They must match
     81 ;; (typecheck-fail
     82 ;;  (instance (to-string Int)
     83 ;;            (λ ([x : Num]) "num"))
     84 ;;  #:with-msg "must be the instance type")
     85 
     86 ;; (typecheck-fail
     87 ;;  (instance (to-string Int)
     88 ;;            (λ ([x : Int]) 0))
     89 ;;  #:with-msg "must match template codomain")
     90 
     91 ;; (typecheck-fail
     92 ;;  (instance (to-string Int)
     93 ;;            42)
     94 ;;  #:with-msg "May only overload single-argument functions")
     95 
     96 ;; ;; -- no overlapping instances
     97 ;; (typecheck-fail
     98 ;;  (instance (to-string Nat)
     99 ;;            (λ ([x : Nat]) "wrong"))
    100 ;;  #:with-msg "Overlaps with existing instance")
    101 
    102 ;; -- can't instantiate non-overloadeds
    103 (typecheck-fail
    104  (λ ([x : (→ Int Int)])
    105    (instance (x Int)
    106              0))
    107  #:with-msg "Identifier 'x' is not overloaded")
    108 
    109 ;; ;; -- explicit resolve
    110 
    111 ;; ;; -- recursive instances are fine [TODO really want (List α)]
    112 ;; (instance (to-string (List Nat))
    113 ;;           (λ ([x : (List Nat)]) "listnat"))
    114 
    115 ;; (check-type
    116 ;;  (to-string (cons 1 (cons 2 (nil {Nat}))))
    117 ;;  : Str ⇒ "listnat")
    118 
    119 ;; ;; -- higher-order use
    120