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

Use (listof tc-result?) instead of tc-results? when inferring types.

Browse Source 
tc-results? does not represent Bottom in a way that maintains the number
of values that generated the Bottom.

original commit: fd3d01d822ddef3bfa34a11574742651c37f007b
This commit is contained in:
Eric Dobson 2014-06-22 12:07:39 -07:00
parent 8201d0d052
commit 0acb67a97f
7 changed files with 57 additions and 36 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

31
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/type-annotation.rkt
View File

@ -4,7 +4,8 @@
(rep type-rep)
(utils tc-utils)
(env global-env mvar-env scoped-tvar-env)
(except-in (types subtype union utils generalize))
(except-in (types subtype abbrev union utils generalize)
-> ->* one-of/c)
(private parse-type syntax-properties)
(contract-req)
syntax/parse
@ -67,36 +68,40 @@
(define (get-types stxs #:default [default #f])
(map (lambda (e) (get-type e #:default default)) stxs))
;; list[identifier] stx (stx -> tc-results/c) (stx tc-results/c -> tc-results/c) -> tc-results/c
;; stxs : the identifiers, possibly with type annotations on them
;; expr : the RHS expression
;; tc-expr : a function like `tc-expr' from tc-expr-unit
;; tc-expr/check : a function like `tc-expr/check' from tc-expr-unit
(define/cond-contract (get-type/infer stxs expr tc-expr tc-expr/check)
((listof identifier?) syntax? (syntax? . -> . tc-results/c) (syntax? tc-results/c . -> . tc-results/c) . -> . tc-results/c)
((listof identifier?) syntax? (syntax? . -> . tc-results/c) (syntax? tc-results/c . -> . tc-results/c)
. -> . (listof tc-result?))
(match stxs
[(list stx ...)
(let ([anns (for/list ([s (in-list stxs)]) (type-annotation s #:infer #t))])
(if (for/and ([a (in-list anns)]) a)
(tc-expr/check expr (ret anns))
(let ([ty (tc-expr expr)])
(match ty
(match (tc-expr/check expr (ret anns))
[(tc-results: tys fs os)
(map tc-result tys fs os)])
(let ([res (tc-expr expr)])
(match res
[(tc-any-results: _)
(tc-error/expr
"Expression should produce ~a values, but produces an unknown number of values"
(length stxs))]
[(tc-results: (list (== -Bottom)) _ _)
(for/list ([_ (in-range (length stxs))])
(tc-result -Bottom))]
[(tc-results: tys fs os)
(if (not (= (length stxs) (length tys)))
(tc-error/expr #:return (ret (map (lambda _ (Un)) stxs))
"Expression should produce ~a values, but produces ~a values of types ~a"
(length stxs) (length tys) (stringify tys))
(combine-results
(for/list ([stx (in-list stxs)] [ty (in-list tys)]
[a (in-list anns)] [f (in-list fs)] [o (in-list os)])
(cond [a (check-type stx ty a) (tc-result a f o)]
;; mutated variables get generalized, so that we don't infer too small a type
[(is-var-mutated? stx) (tc-result (generalize ty) f o)]
[else (tc-result ty f o)]))))]))))]))
(for/list ([stx (in-list stxs)] [ty (in-list tys)]
[a (in-list anns)] [f (in-list fs)] [o (in-list os)])
(cond [a (check-type stx ty a) (tc-result a f o)]
;; mutated variables get generalized, so that we don't infer too small a type
[(is-var-mutated? stx) (tc-result (generalize ty) f o)]
[else (tc-result ty f o)])))]))))]))
;; check that e-type is compatible with ty in context of stx
;; otherwise, error

27
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt
View File

@ -29,7 +29,7 @@
(append*
(for/list ([names namess] [results results])
(match results
[(tc-results: _ _ os)
[(list (tc-result: _ _ os) ...)
(map list names os)]))))
;; Checks that the body has the expected type when names are bound to the types spcified by results.
@ -37,7 +37,7 @@
;; TODO: make this function sane.
(define/cond-contract (do-check expr->type namess expected-results exprs body expected)
((syntax? tc-results/c . -> . any/c)
(listof (listof identifier?)) (listof tc-results/c)
(listof (listof identifier?)) (listof (listof tc-result?))
(listof syntax?) syntax? (or/c #f tc-results/c)
. -> .
tc-results/c)
@ -48,7 +48,7 @@
([e-r (in-list expected-results)]
[names (in-list namess)])
(match e-r
[(tc-results: e-ts (list (FilterSet: fs+ fs-) ...) os)
[(list (tc-result: e-ts (FilterSet: fs+ fs-) os) ...)
(values e-ts
(apply append
(for/list ([n (in-list names)]
@ -58,7 +58,7 @@
(list)
(list (-imp (-not-filter (-val #f) n) f+)
(-imp (-filter (-val #f) n) f-))))))]
[(tc-results: e-ts (list (NoFilter:) ...) _)
[(list (tc-result: e-ts (NoFilter:) _) ...)
(values e-ts null)]))))
;; extend the lexical environment for checking the body
(with-lexical-env/extend
@ -69,9 +69,10 @@
(with-lexical-env/extend-props
(apply append props)
;; type-check the rhs exprs
(for-each expr->type
exprs
expected-results)
(for ([expr (in-list exprs)] [results (in-list expected-results)])
(match results
[(list (tc-result: ts fs os) ...)
(expr->type expr (ret ts fs os))]))
;; typecheck the body
(tc-body/check body (and expected (erase-filter expected)))))))
@ -138,7 +139,7 @@
(do-check tc-expr/check
remaining-names
;; types the user gave.
(map (λ (l) (ret (map get-type l))) remaining-names)
(map (λ (l) (map tc-result (map get-type l))) remaining-names)
remaining-exprs body expected)])))))
;; An lr-clause is a
@ -212,7 +213,7 @@
(cond [(null? clauses) (k)]
[else
(match-define (lr-clause names expr) (car clauses))
(match-define (tc-results: ts fs os)
(match-define (list (tc-result: ts fs os) ...)
(get-type/infer names expr
(lambda (e) (tc-expr/maybe-expected/t e names))
tc-expr/check))
@ -241,7 +242,7 @@
;; the types of the exprs
#;[inferred-types (map (tc-expr-t/maybe-expected expected) exprs)]
;; the annotated types of the name (possibly using the inferred types)
[types (for/list ([name (in-list names)] [e (in-list exprs)])
(get-type/infer name e (tc-expr-t/maybe-expected expected)
tc-expr/check))])
(do-check void names types exprs body expected)))
[results (for/list ([name (in-list names)] [e (in-list exprs)])
(get-type/infer name e (tc-expr-t/maybe-expected expected)
tc-expr/check))])
(do-check void names results exprs body expected)))

2
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt
View File

@ -164,7 +164,7 @@
;; the module (hence we haven't synthesized a type for yet).
[_
(match (get-type/infer vars #'expr tc-expr tc-expr/check)
[(tc-results: ts)
[(list (tc-result: ts) ...)
(for/list ([i (in-list vars)] [t (in-list ts)])
(register-type i t)
(free-id-table-set! unann-defs i #t)

14
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/types/tc-result.rkt
View File

@ -91,7 +91,7 @@
;; make-tc-result*: Type/c FilterSet/c Object? -> tc-result?
;; Smart constructor for a tc-result.
(define (-tc-result type filter object)
(define (-tc-result type [filter -top-filter] [object -empty-obj])
(cond
[(or (equal? type -Bottom) (equal? filter -bot-filter))
(tc-result -Bottom -bot-filter object)]
@ -146,22 +146,20 @@
[dbound symbol?])
[res tc-results/c])])
(define (combine-results tcs)
(match tcs
[(list (tc-result: t f o) ...)
(ret t f o)]))
(define tc-result-equal? equal?)
(provide tc-result: tc-results: tc-any-results: tc-result1: Result1: Results:
tc-results)
(provide/cond-contract
[rename -tc-result tc-result (Type/c FilterSet/c Object? . c:-> . tc-result?)]
[combine-results ((c:listof tc-result?) . c:-> . tc-results?)]
[rename -tc-result tc-result
(c:case->
(Type/c . c:-> . tc-result?)
(Type/c FilterSet/c Object? . c:-> . tc-result?))]
[tc-any-results ((c:or/c Filter/c NoFilter?) . c:-> . tc-any-results?)]
[tc-result-t (tc-result? . c:-> . Type/c)]
[rename tc-results-ts* tc-results-ts (tc-results? . c:-> . (c:listof Type/c))]
[tc-result-equal? (tc-result? tc-result? . c:-> . boolean?)]
[tc-result? (c:any/c . c:-> . boolean?)]
[tc-results? (c:any/c . c:-> . boolean?)]
[tc-results/c c:flat-contract?]
[tc-results1/c c:flat-contract?]

9
pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/fail/define-values-bottom.rkt Normal file
View File

@ -0,0 +1,9 @@
#;
(exn-pred "runtime")
#lang typed/racket
;; Make sure -Bottom and multiple values play nice together at the module level.
(define-values (a b)
(error 'runtime))
b

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

@ -1,5 +1,5 @@
#;
(exn-pred (regexp-quote "in: (for/flvector"))
(exn-pred (regexp-quote "in: from"))
#lang typed/racket/base
;; Test for PR 14389. Make sure that the reported source location

8
pkgs/typed-racket-pkgs/typed-racket-test/tests/typed-racket/unit-tests/typecheck-tests.rkt
View File

@ -3094,6 +3094,14 @@
(tr:define (f #:foo [foo 'foo]) foo)
(error "dummy"))
#:msg #rx"expected: String.*given: 'foo"]
;; Make sure -Bottom and multiple values play nice together.
[tc-e
(let ()
(define-values (a b) (error 'nyi))
b)
-Bottom]
)
(test-suite