improve rackunit-typechecking

- speed up by eliminating duplicate expansion in check-type
- use given type annotation as expected-type
  - eliminates unneeded type annotations

tapl/stlc+tup.rkt

@@ -16,7 +16,8 @@
    #:with ty-expected (get-expected-type stx)
    #:with (e_ann ...) (if (syntax-e #'ty-expected)
                           (syntax-parse (local-expand #'ty-expected 'expression null)
-                           [(~× ty_exp ...) #'((add-expected e ty_exp) ...)])
+                           [(~× ty_exp ...) #'((add-expected e ty_exp) ...)]
+                           [_ #'(e ...)])
                           #'(e ...))
    #:with ([e- τ] ...) (infers+erase #'(e_ann ...))
    (⊢ (list e- ...) : (× τ ...))])

tapl/tests/rackunit-typechecking.rkt

@@ -1,6 +1,6 @@
 #lang racket/base
 (require (for-syntax rackunit) rackunit "../typecheck.rkt")
-(provide (all-defined-out))
+(provide check-type typecheck-fail check-not-type check-props)
 
 (begin-for-syntax
   (define (add-esc s) (string-append "\\" s))
@@ -18,11 +18,18 @@
 
 (define-syntax (check-type stx)
   (syntax-parse stx #:datum-literals (: ⇒ ->)
-    [(_ e : τ (~or ⇒ ->) v)
-     (syntax/loc stx
-       (check-type-and-result e : τ ⇒ v))]
+    ;; duplicate code to avoid redundant expansions
+    [(_ e : τ-expected (~or ⇒ ->) v)
+     #:with e+ (expand/df #'(add-expected e τ-expected))
+     #:with τ (typeof #'e+)
+     #:fail-unless (typecheck? #'τ ((current-type-eval) #'τ-expected))
+                   (format
+                    "Expression ~a [loc ~a:~a] has type ~a, expected ~a"
+                    (syntax->datum #'e) (syntax-line #'e) (syntax-column #'e)
+                    (type->str #'τ) (type->str #'τ-expected))
+     (syntax/loc stx (check-equal? e+ (add-expected v τ-expected)))]
     [(_ e : τ-expected)
-     #:with τ (typeof (expand/df #'e))
+     #:with τ (typeof (expand/df #'(add-expected e τ-expected)))
      #:fail-unless
      (typecheck? #'τ ((current-type-eval) #'τ-expected))
      (format
@@ -81,11 +88,3 @@
               "Expected type check failure but expression ~a has valid type, OR wrong err msg received."
               (syntax->datum #'e)))
      #'(void)]))
-
-(define-syntax (check-type-and-result stx)
-  (syntax-parse stx #:datum-literals (: ⇒)
-    [(_ e : τ ⇒ v)
-     #`(begin
-         (check-type e : τ)
-         #,(syntax/loc stx
-             (check-equal? e v)))]))

tapl/tests/stlc+occurrence-tests.rkt

@@ -118,13 +118,13 @@
           #t
           #f))
  : (→ (∪ Boolean Int) Boolean))
-(check-type-and-result
+(check-type
  ((λ ([x : (∪ Boolean Int)])
      (test (Boolean ? x)
            #t
            #f)) #t)
   : Boolean ⇒ #t)
-(check-type-and-result
+(check-type
  ((λ ([x : (∪ Boolean Int)])
      (test (Boolean ? x)
            #t
@@ -138,19 +138,19 @@
           (+ 1 x)
           0))
  : (→ (∪ Int Boolean) (∪ Num Nat)))
-(check-type-and-result
+(check-type
  ((λ ([x : (∪ Int Boolean)])
     (test (Int ? x)
           (+ 1 x)
           0)) #f)
  : Num ⇒ 0)
-(check-type-and-result
+(check-type
  ((λ ([x : (∪ Int Boolean)])
     (test (Int ? x)
           (+ 1 x)
           1)) #t)
  : Num ⇒ 1)
-(check-type-and-result
+(check-type
  ((λ ([x : (∪ Int Boolean)])
     (test (Int ? x)
           (+ 1 x)
@@ -190,7 +190,7 @@
           x))
  : (→ (∪ Boolean Int) (∪ Nat Boolean)))
 
-(check-type-and-result
+(check-type
  ((λ ([x : (∪ Int Boolean)])
      (test (Num ? x)
            #f
@@ -199,7 +199,7 @@
  ⇒ #t)
 
 ;; Should filter all the impossible types 
-(check-type-and-result
+(check-type
  ((λ ([x : (∪ Nat Int Num Boolean)])
      (test (Num ? x)
            #f
@@ -208,7 +208,7 @@
  ⇒ #t)
 
 ;; Can refine non-union types
-(check-type-and-result
+(check-type
  ((λ ([x : Top])
     (test (Str ? x)
           x
@@ -304,7 +304,7 @@
           (x 1 0))))
  : (→ (∪ (→ Int Int Int) (→ Int Int)) Int))
 
-(check-type-and-result
+(check-type
  ((λ ([x : (∪ (→ Int Int Int) (→ Int Int) Int)])
     (test ((→ Int Int) ? x)
           (x 0)
@@ -313,7 +313,7 @@
           (x 1 0)))) 1)
  : Int ⇒ 1)
 
-(check-type-and-result
+(check-type
  ((λ ([x : (∪ (→ Int Int Int) (→ Int Int) Int)])
     (test ((→ Int Int) ? x)
           (x 0)
@@ -322,7 +322,7 @@
           (x 1 0)))) (λ ([y : Int]) 5))
  : Int ⇒ 5)
 
-(check-type-and-result
+(check-type
  ((λ ([x : (∪ (→ Int Int Int) (→ Int Int) Int)])
     (test ((→ Int Int) ? x)
           (x 0)
@@ -362,21 +362,21 @@
           "bool"))
  : (→ (∪ Int Str Boolean) Str))
 
-(check-type-and-result
+(check-type
  ((λ ([x : (∪ Str Boolean)])
      (test ((∪ Int Nat Num) ? x)
            x
            (+ 1 2))) "hi")
  : Num ⇒ 3)
 
-(check-type-and-result
+(check-type
   ((λ ([x : (∪ Str Int Boolean)])
       (test ((∪ Int Str) ? x)
             x
             "error")) 1)
   : (∪ Str Int) ⇒ 1)
 
-(check-type-and-result
+(check-type
   ((λ ([x : (∪ Str Int Boolean)])
       (test ((∪ Int Str) ? x)
             x
@@ -415,7 +415,7 @@
           0))
  : (→ (× (∪ Int Str) Int) Num))
 
-(check-type-and-result
+(check-type
  ((λ ([v : (× (∪ Int Str) Int)])
     (test (Int ? (proj v 0))
           (+ (proj v 0) (proj v 1))
@@ -423,7 +423,7 @@
   (tup ((λ ([x : (∪ Int Str)]) x) -2) -3))
  : Num ⇒ -5)
 
-(check-type-and-result
+(check-type
  ((λ ([v : (× (∪ Int Str) Int)])
     (test (Int ? (proj v 0))
           (+ (proj v 0) (proj v 1))
@@ -440,7 +440,7 @@
           (+ (proj x 0) (+ (proj x 1) (proj x 2)))))
  : (→ (∪ (× Int Int Int) Int) Num))
 
-(check-type-and-result
+(check-type
  ((λ ([x : (∪ Int (× Int Int Int))])
      (test (Int ? x)
            (+ 1 x)
@@ -448,7 +448,7 @@
   0)
  : Num ⇒ 1)
 
-(check-type-and-result
+(check-type
  ((λ ([x : (∪ Int (× Int Int Int))])
      (test (Int ? x)
            (+ 1 x)
@@ -456,7 +456,7 @@
   (tup 2 2 2))
  : Num ⇒ 6)
 
-(check-type-and-result
+(check-type
  ((λ ([x : (∪ Int (× Str Nat) (× Int Int Int))])
      (test (Int ? x)
            (+ 1 x)
@@ -466,7 +466,7 @@
   (tup 2 2 2))
  : Num ⇒ 6)
 
-(check-type-and-result
+(check-type
  ((λ ([x : (∪ Int (× Str Nat) (× Int Int Int))])
      (test (Int ? x)
            (+ 1 x)
@@ -478,7 +478,7 @@
 
 ;; -- All together now
 
-(check-type-and-result
+(check-type
  ((λ ([x : (∪ Int (× Boolean Boolean) (× Int (∪ Str Int)))])
      (test (Int ? x)
            "just an int"
@@ -490,7 +490,7 @@
   (tup 33 "success"))
  : Str ⇒ "success")
 
-(check-type-and-result
+(check-type
  ((λ ([x : (∪ Int (× Int Int) (× Int (∪ Str Int)))])
      (test (Int ? x)
            "just an int"

tapl/tests/stlc+overloading-tests.rkt

@@ -36,7 +36,7 @@
 (instance (to-string Str)
   (λ ([x : Str]) "string"))
 
-(check-type-and-result
+(check-type
  (to-string 3)
  : Str ⇒ "nat")
 
@@ -47,25 +47,25 @@
 (instance (to-string Num)
   (λ ([x : Num]) "num"))
 
-(check-type-and-result
+(check-type
  (to-string (+ 2 2))
  : Str ⇒ "num")
 
-(check-type-and-result
+(check-type
  (to-string -1)
  : Str ⇒ "num")
 
-(check-type-and-result
+(check-type
  (to-string "hi")
  : Str ⇒ "string")
 
 ;; -- use 'resolve' to get exact matches
 
-(check-type-and-result
+(check-type
  ((resolve to-string Nat) 1)
  : Str ⇒ "nat")
 
-(check-type-and-result
+(check-type
  ((resolve to-string Num) 1)
  : Str ⇒ "num")
 
@@ -112,7 +112,7 @@
 (instance (to-string (List Nat))
           (λ ([x : (List Nat)]) "listnat"))
 
-(check-type-and-result
+(check-type
  (to-string (cons 1 (cons 2 (nil {Nat}))))
  : Str ⇒ "listnat")