Avoid generating contraints for optimized-away contract definitions.

Closes #214.
This commit is contained in:
Vincent St-Amour 2015-11-10 16:39:12 -06:00
parent be29c556cd
commit 53e501bb8b
2 changed files with 56 additions and 2 deletions

View File

@ -47,9 +47,42 @@
(contract-restrict-recursive-values (compute-constraints sc kind)))
cache))))
;; computes the definitions that are in / used by `sc`
;; `(get-all-name-defs)` is not what we want directly, since it also includes
;; definitions that were optimized away
;; we restrict it to only variables bound in `sc`
(define (compute-defs sc)
(define all-name-defs (get-all-name-defs))
;; all-name-defs maps lists of ids to defs
;; we want to match if any id in the list matches
(define (ref b) (for/first ([(k v) (in-dict all-name-defs)]
#:when (for/or ([k* (in-list k)])
(free-identifier=? b k*)))
(cons k v)))
(define bound '())
;; ignores its second argument (variance, passed by sc-traverse)
(let loop ([sc sc] [_ #f])
(match sc
[(name/sc: name*)
(unless (member name* bound free-identifier=?)
(set! bound (cons name* bound))
;; traverse what `name` refers to
(define r (ref name*))
;; ref returns a rib, get the one definition we want
(define target (for/first ([k (car r)]
[v (cdr r)]
#:when (free-identifier=? name* k))
v))
(loop target #f))]
[else (sc-traverse sc loop)]))
(for*/hash ([b (in-list bound)]
[v (in-value (ref b))]
#:when v)
(values (car v) (cdr v))))
(define (compute-constraints sc max-kind)
(define memo-table (make-hash))
(define name-defs (get-all-name-defs))
(define name-defs (compute-defs sc))
(define (recur sc)
(cond [(hash-ref memo-table sc #f)]
[else
@ -138,7 +171,7 @@
[(? sc? sc)
(sc->contract sc recur)]))
(define ctc (recur sc))
(define name-defs (get-all-name-defs))
(define name-defs (compute-defs sc))
;; These are extra contract definitions for the name static contracts
;; that are used for this type. Since these are shared across multiple
;; contracts from a single contract fixup pass, we use the name-defined

View File

@ -0,0 +1,21 @@
#lang typed/racket
(struct (A B) Fum ([a : A] [b : B]))
(struct Fi ())
(struct Foo ())
(define-type Tail
(Rec T
(U (Fum (Listof Value) T)
Fi)))
(define-type Value
(Rec V
(U (Fum (Listof Value) V)
Foo)))
(provide fun1)
(: fun1 (-> Tail))
(define (fun1)
(error 'foo1))