suzanne.soy/typed-racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Add value-mismatch to check-below, and fixup some poly dotted cases.

Browse Source 
original commit: ec14598ad88574294b00e003aa929478a5b36018
This commit is contained in:
Eric Dobson 2014-04-02 22:26:25 -07:00
parent 8e5b550ee8
commit bb45c93b71
4 changed files with 64 additions and 26 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

62
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/check-below.rkt
View File

@ -2,6 +2,7 @@
(require "../utils/utils.rkt"
racket/match (prefix-in - (contract-req))
racket/format
(types utils union subtype filter-ops abbrev)
(utils tc-utils)
(rep type-rep object-rep filter-rep)
@ -36,6 +37,22 @@
(define t2* (if (Type/c? t2) (pretty-format-type t2 #:indent 9) t2))
(tc-error/fields "type mismatch" #:more more "expected" t1* "given" t2* #:delayed? #t))
;; value-mismatch : tc-results/c tc-results/c -> void?
;; Helper to print messages of the form
;; "Expecte n values, but got m values"
(define (value-mismatch expected actual)
(define (value-string ty)
(match ty
[(tc-result1: _) "1 value"]
[(tc-results: ts) (~a (length ts) " values")]
;; TODO simplify this case
[(tc-results: ts _ _ dty _) (~a (length ts) " " (if (= (length ts) 1) "value" "values")
" and `" dty " ...'")]
[(tc-any-results:) "unknown number"]))
(type-mismatch
(value-string expected) (value-string actual)
"mismatch in number of values"))
;; expected-but-got : (U Type String) (U Type String) -> Void
;;
;; Helper to print messages of the form
@ -105,8 +122,9 @@
(fix-results expected)]
[((tc-results: ts fs os) (tc-results: ts2 (NoFilter:) (NoObject:)))
(unless (= (length ts) (length ts2))
(type-mismatch (length ts2) (length ts) "mismatch in number of values"))
(value-mismatch tr1 expected))
(unless (for/and ([t (in-list ts)] [s (in-list ts2)]) (subtype t s))
(expected-but-got (stringify ts2) (stringify ts)))
(if (= (length ts) (length ts2))
@ -128,43 +146,39 @@
(format "`~a' and `~a'" f1 (print-object o1))
"mismatch in filter and object")])
(ret t2 (fix-filter f2 f1) (fix-object o2 o1))]
;; case where expected is like (Values a ... a) but got something else
[((tc-results: t1 f o) (tc-results: t2 f o dty dbound))
(unless (= (length t1) (length t2))
(type-mismatch (format "~a values and `~a ...'" (length t2) dty)
(format "~a values" (length t1))
"mismatch in number of values"))
(unless (for/and ([t (in-list t1)] [s (in-list t2)]) (subtype t s))
(expected-but-got (stringify t2) (stringify t1)))
(value-mismatch expected tr1)
(fix-results expected)]
;; case where you have (Values a ... a) but expected something else
[((tc-results: t1 f o dty dbound) (tc-results: t2 f o))
(unless (= (length t1) (length t2))
(type-mismatch (format "~a values" (length t2))
(format "~a values and `~a'" (length t1) dty)
"mismatch in number of values"))
(unless (for/and ([t (in-list t1)] [s (in-list t2)]) (subtype t s))
(expected-but-got (stringify t2) (stringify t1)))
(value-mismatch expected tr1)
(fix-results expected)]
[((tc-results: t1 f o dty1 dbound) (tc-results: t2 f o dty2 dbound))
(unless (= (length t1) (length t2))
(type-mismatch (length t2) (length t1) "mismatch in number of non-dotted values"))
(unless (andmap subtype t1 t2)
(expected-but-got (stringify t2) (stringify t1)))
(unless (subtype dty1 dty2)
(type-mismatch dty2 dty1 "mismatch in ... argument"))
(cond
[(= (length t1) (length t2))
(unless (andmap subtype t1 t2)
(expected-but-got (stringify t2) (stringify t1)))
(unless (subtype dty1 dty2)
(type-mismatch dty2 dty1 "mismatch in ... argument"))]
[else
(value-mismatch expected tr1)])
(fix-results expected)]
[((tc-results: t1 fs os) (tc-results: t2 fs os))
(unless (= (length t1) (length t2))
(type-mismatch (length t2) (length t1) "mismatch in number of values"))
(value-mismatch expected tr1))
(unless (for/and ([t (in-list t1)] [s (in-list t2)]) (subtype t s))
(expected-but-got (stringify t2) (stringify t1)))
(fix-results expected)]
[((tc-any-results:) (tc-result1: t _ _))
(type-mismatch "1 value" "unknown number")
[((tc-any-results:) (tc-results: ts fs os))
(value-mismatch expected tr1)
(fix-results expected)]
[((tc-any-results:) (tc-results: t2 fs os))
(type-mismatch (format "~a values" (length t2)) "unknown number")
[((tc-any-results:) (tc-results: ts fs os dty dbound))
(value-mismatch expected tr1)
(fix-results expected)]
[((? Type/c? t1) (? Type/c? t2))

2
pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/fail/internal-vector-error.rkt
View File

@ -1,5 +1,5 @@
#;
(exn-pred #rx"expected: 2\n given: 1")
(exn-pred #rx"expected: 2 values\n given: 1 value")
#lang typed/racket
;; This test ensures that the following snippet doesn't

2
pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/fail/pr13365-variation-2.rkt
View File

@ -1,5 +1,5 @@
#;
(exn-pred #rx"expected: String\n given:")
(exn-pred #rx"expected: 1 value and `a ...'\n given: 1 value")
#lang typed/racket
(: f (All (a ...) (a ... a -> (Values String a ... a))))

24
pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/check-below-tests.rkt
View File

@ -139,6 +139,30 @@
tc-any-results
(ret -Symbol))
(test-below #:fail
(ret -Symbol -true-filter -empty-obj)
(ret -Symbol -true-filter -empty-obj Univ 'B))
(test-below #:fail
(ret -Symbol -true-filter -empty-obj Univ 'B)
(ret -Symbol -true-filter -empty-obj))
(test-below #:fail
(ret -Symbol)
(ret -Symbol -no-filter -empty-obj Univ 'B)
#:result (ret -Symbol -top-filter -empty-obj Univ 'B))
(test-below #:fail
tc-any-results
(ret -Symbol -no-filter -empty-obj Univ 'B)
#:result (ret (list -Symbol) (list -top-filter) (list -empty-obj) Univ 'B))
(test-below #:fail
(ret -Symbol -top-filter -empty-obj Univ 'B)
(ret (list -Symbol -Symbol) (list -top-filter -top-filter) (list -empty-obj -empty-obj) Univ 'B))
;; Enable these once check-below is fixed
;; Currently does not fail
#;