www

commit b4bc922ddae7ee998d19b103194a28453fe28843
parent 48b625c2f429a5be41fe3a124e7532752eab0de5
Author: Stephen Chang <stchang@ccs.neu.edu>
Date:   Thu, 22 Oct 2015 13:22:22 -0400

add stlc+sub tests

Diffstat:
M
tapl/stlc+sub.rkt
 | 
1
+
M
tapl/tests/stlc+sub-tests.rkt
 | 
6
++++++

2 files changed, 7 insertions(+), 0 deletions(-)
diff --git a/tapl/stlc+sub.rkt b/tapl/stlc+sub.rkt
@@ -1,5 +1,6 @@
 #lang s-exp "typecheck.rkt"
 (extends "stlc+lit.rkt" #:except #%datum +)
+(reuse add1 #:from "ext-stlc.rkt")
 (provide (for-syntax subs? current-sub?))
 
 ;; Simply-Typed Lambda Calculus, plus subtyping
diff --git a/tapl/tests/stlc+sub-tests.rkt b/tapl/tests/stlc+sub-tests.rkt
@@ -21,6 +21,12 @@
 (check-type (λ ([x : Int]) x) : (→ Nat Int)) ; contravariant input
 (check-not-type (λ ([x : Int]) x) : (→ Num Int))
 
+(check-type ((λ ([f : (→ Int Int)]) (f -1)) add1) : Int ⇒ 0)
+(check-type ((λ ([f : (→ Nat Int)]) (f 1)) add1) : Int ⇒ 2)
+(typecheck-fail ((λ ([f : (→ Num Int)]) (f 1.1)) add1))
+(check-type ((λ ([f : (→ Nat Num)]) (f 1)) add1) : Num ⇒ 2)
+(typecheck-fail ((λ ([f : (→ Num Num)]) (f 1.1)) add1))
+
 (check-type + : (→ Num Num Num))
 (check-type + : (→ Int Num Num))
 (check-type + : (→ Int Int Num))