Generalize mutated variables when inferring types.

This commit is contained in:
Sam Tobin-Hochstadt 2010-06-27 20:07:33 -04:00
parent e7c33c2244
commit 90d8a3cc13
2 changed files with 21 additions and 29 deletions

View File

@ -112,49 +112,41 @@
(map (lambda (e) (get-type e #:default default)) stxs)) (map (lambda (e) (get-type e #:default default)) stxs))
;; list[identifier] stx (stx -> tc-results?) (stx tc-results? -> tc-results?) -> tc-results? ;; list[identifier] stx (stx -> tc-results?) (stx tc-results? -> tc-results?) -> tc-results?
;; 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
(d/c (get-type/infer stxs expr tc-expr tc-expr/check) (d/c (get-type/infer stxs expr tc-expr tc-expr/check)
((listof identifier?) syntax? (syntax? . -> . tc-results?) (syntax? tc-results? . -> . tc-results?) . -> . tc-results?) ((listof identifier?) syntax? (syntax? . -> . tc-results?) (syntax? tc-results? . -> . tc-results?) . -> . tc-results?)
(match stxs (match stxs
['()
(tc-expr/check expr (ret null))]
[(list stx)
(cond [(type-annotation stx #:infer #t)
=> (lambda (ann)
(tc-expr/check expr (ret ann)))]
[else (tc-expr expr)])]
[(list stx ...) [(list stx ...)
(let ([anns (for/list ([s stxs]) (type-annotation s #:infer #t))]) (let ([anns (for/list ([s stxs]) (type-annotation s #:infer #t))])
(if (for/and ([a anns]) a) (if (for/and ([a anns]) a)
(begin (tc-expr/check expr (ret anns))) (tc-expr/check expr (ret anns))
(let ([ty (tc-expr expr)]) (let ([ty (tc-expr expr)])
(match ty (match ty
[(tc-results: tys) [(tc-results: tys fs os)
(if (not (= (length stxs) (length tys))) (if (not (= (length stxs) (length tys)))
(begin (begin
(tc-error/delayed (tc-error/delayed
"Expression should produce ~a values, but produces ~a values of types ~a" "Expression should produce ~a values, but produces ~a values of types ~a"
(length stxs) (length tys) (stringify tys)) (length stxs) (length tys) (stringify tys))
(ret (map (lambda _ (Un)) stxs))) (ret (map (lambda _ (Un)) stxs)))
(ret (combine-results
(for/list ([stx stxs] [ty tys] [a anns]) (for/list ([stx stxs] [ty tys] [a anns] [f fs] [o os])
(cond [a => (lambda (ann) (check-type stx ty ann) ann)] (cond [a (check-type stx ty a) (ret a f o)]
[else ty]))))] ;; mutated variables get generalized, so that we don't infer too small a type
[ty (tc-error/delayed [(is-var-mutated? stx) (ret (generalize ty) f o)]
"Expression should produce ~a values, but produces one values of type ~a" [else (ret ty f o)]))))]))))]))
(length stxs) ty)
(ret (map (lambda _ (Un)) stxs))]))))]))
;; check that e-type is compatible with ty in context of stx ;; check that e-type is compatible with ty in context of stx
;; otherwise, error ;; otherwise, error
;; syntax type type -> void ;; syntax type type -> void
(define (check-type stx e-type ty) (define (check-type stx e-type ty)
(let ([stx* (current-orig-stx)])
(parameterize ([current-orig-stx stx]) (parameterize ([current-orig-stx stx])
(unless (subtype e-type ty) (unless (subtype e-type ty)
;(printf "orig-stx: ~a" (syntax->datum stx*)) ;(printf "orig-stx: ~a" (syntax->datum stx*))
(tc-error "Body had type:~n~a~nVariable had type:~n~a~n" e-type ty))))) (tc-error "Body had type:~n~a~nVariable had type:~n~a~n" e-type ty))))
(define (dotted? stx) (define (dotted? stx)
(cond [(syntax-property stx type-dotted-symbol) => syntax-e] (cond [(syntax-property stx type-dotted-symbol) => syntax-e]

View File

@ -1,4 +1,4 @@
#lang scheme/unit #lang racket/unit
(require (rename-in "../utils/utils.rkt" [infer r:infer])) (require (rename-in "../utils/utils.rkt" [infer r:infer]))
(require "signatures.rkt" "tc-metafunctions.rkt" "tc-subst.rkt" (require "signatures.rkt" "tc-metafunctions.rkt" "tc-subst.rkt"
@ -7,12 +7,12 @@
(env lexical-env type-alias-env global-env type-env-structs) (env lexical-env type-alias-env global-env type-env-structs)
(rep type-rep) (rep type-rep)
syntax/free-vars syntax/free-vars
mzlib/trace unstable/debug racket/trace unstable/debug
scheme/match (prefix-in c: scheme/contract) racket/match (prefix-in c: racket/contract)
(except-in scheme/contract -> ->* one-of/c) (except-in racket/contract -> ->* one-of/c)
syntax/kerncase syntax/parse syntax/kerncase syntax/parse
(for-template (for-template
scheme/base racket/base
"internal-forms.rkt")) "internal-forms.rkt"))
(require (only-in srfi/1/list s:member)) (require (only-in srfi/1/list s:member))