From 81b1178a1749e06f097c270563e253accb727246 Mon Sep 17 00:00:00 2001 From: Eric Dobson Date: Mon, 18 Jul 2011 13:12:00 -0400 Subject: [PATCH] Fixed TR contracts to be more/less strict --- collects/typed-scheme/infer/infer-unit.rkt | 47 +++++++++++++--------- collects/typed-scheme/infer/signatures.rkt | 20 ++++----- 2 files changed, 39 insertions(+), 28 deletions(-) diff --git a/collects/typed-scheme/infer/infer-unit.rkt b/collects/typed-scheme/infer/infer-unit.rkt index 308155600a..65650612b6 100644 --- a/collects/typed-scheme/infer/infer-unit.rkt +++ b/collects/typed-scheme/infer/infer-unit.rkt @@ -27,11 +27,11 @@ (define (seen-before s t) (cons (Type-seq s) (Type-seq t))) (define/cond-contract (remember s t A) - (Type/c Type/c (listof (cons/c exact-nonnegative-integer? exact-nonnegative-integer?)) . -> . + (Type? Type? (listof (cons/c exact-nonnegative-integer? exact-nonnegative-integer?)) . -> . (listof (cons/c exact-nonnegative-integer? exact-nonnegative-integer?))) (cons (seen-before s t) A)) (define/cond-contract (seen? s t) - (Type/c Type/c . -> . boolean?) + (Type? Type? . -> . boolean?) (member (seen-before s t) (current-seen))) @@ -139,7 +139,8 @@ (hash-set! dotted-var-store key all) all)))) -(define (cgen/filter V X Y s t) +(define/cond-contract (cgen/filter V X Y s t) + ((listof symbol?) (listof symbol?) (listof symbol?) Filter? Filter? . -> . cset?) (match* (s t) [(e e) (empty-cset X Y)] [(e (Top:)) (empty-cset X Y)] @@ -149,21 +150,24 @@ [(_ _) (fail! s t)])) ;; s and t must be *latent* filter sets -(define (cgen/filter-set V X Y s t) +(define/cond-contract (cgen/filter-set V X Y s t) + ((listof symbol?) (listof symbol?) (listof symbol?) FilterSet? FilterSet? . -> . cset?) (match* (s t) [(e e) (empty-cset X Y)] [((FilterSet: s+ s-) (FilterSet: t+ t-)) (cset-meet (cgen/filter V X Y s+ t+) (cgen/filter V X Y s- t-))] [(_ _) (fail! s t)])) -(define (cgen/object V X Y s t) +(define/cond-contract (cgen/object V X Y s t) + ((listof symbol?) (listof symbol?) (listof symbol?) Object? Object? . -> . cset?) (match* (s t) [(e e) (empty-cset X Y)] [(e (Empty:)) (empty-cset X Y)] ;; FIXME - do something here [(_ _) (fail! s t)])) -(define (cgen/arr V X Y s-arr t-arr) +(define/cond-contract (cgen/arr V X Y s-arr t-arr) + ((listof symbol?) (listof symbol?) (listof symbol?) Type? Type? . -> . cset?) (define (cg S T) (cgen V X Y S T)) (match* (s-arr t-arr) ;; the simplest case - no rests, drests, keywords @@ -287,7 +291,8 @@ (cset-meet* (list arg-mapping darg-mapping ret-mapping)))])] [(_ _) (fail! s-arr t-arr)])) -(define (cgen/flds V X Y flds-s flds-t) +(define/cond-contract (cgen/flds V X Y flds-s flds-t) + ((listof symbol?) (listof symbol?) (listof symbol?) Type? Type? . -> . cset?) (cset-meet* (for/list ([s (in-list flds-s)] [t (in-list flds-t)]) (match* (s t) @@ -305,10 +310,10 @@ ;; implements the V |-_X S <: T => C judgment from Pierce+Turner, extended with ;; the index variables from the TOPLAS paper (define/cond-contract (cgen V X Y S T) - ((listof symbol?) (listof symbol?) (listof symbol?) Type/c Type/c . -> . cset?) + ((listof symbol?) (listof symbol?) (listof symbol?) Type? Type? . -> . cset?) ;; useful quick loop (define/cond-contract (cg S T) - (Type/c Type/c . -> . cset?) + (Type? Type? . -> . cset?) (cgen V X Y S T)) ;; this places no constraints on any variables in X (define empty (empty-cset X Y)) @@ -677,23 +682,29 @@ ;; constraint explosion. (cset-meet (cgen V X Y s t) expected-cset)))) + + ;; X : variables to infer ;; Y : indices to infer ;; S : actual argument types ;; T : formal argument types ;; R : result type -;; expected : boolean +;; expected : #f or the expected type ;; returns a substitution ;; if R is #f, we don't care about the substituion ;; just return a boolean result -(define (infer X Y S T R [expected #f]) - (with-handlers ([exn:infer? (lambda _ #f)]) - (let* ([expected-cset (if expected - (cgen null X Y R expected) - (empty-cset '() '()))] - [cs (cgen/list null X Y S T #:expected-cset expected-cset)] - [cs* (cset-meet cs expected-cset)]) - (if R (subst-gen cs* Y R) #t)))) +(define infer + (let () + (define/contract (infer X Y S T R [expected #f]) + (((listof symbol?) (listof symbol?) (listof Type/c) (listof Type/c) Type?) ((or/c #f Type?)) . ->* . (or/c boolean? substitution/c)) + (with-handlers ([exn:infer? (lambda _ #f)]) + (let* ([expected-cset (if expected + (cgen null X Y R expected) + (empty-cset '() '()))] + [cs (cgen/list null X Y S T #:expected-cset expected-cset)] + [cs* (cset-meet cs expected-cset)]) + (if R (subst-gen cs* Y R) #t)))) + infer)) ;to export a variable binding and not syntax ;; like infer, but T-var is the vararg type: (define (infer/vararg X Y S T T-var R [expected #f]) diff --git a/collects/typed-scheme/infer/signatures.rkt b/collects/typed-scheme/infer/signatures.rkt index 36b32e6d00..daff06cebd 100644 --- a/collects/typed-scheme/infer/signatures.rkt +++ b/collects/typed-scheme/infer/signatures.rkt @@ -8,8 +8,8 @@ ([cond-contracted dmap-meet (dmap? dmap? . -> . dmap?)])) (define-signature promote-demote^ - ([cond-contracted var-promote (Type? (listof symbol?) . -> . Type?)] - [cond-contracted var-demote (Type? (listof symbol?) . -> . Type?)])) + ([cond-contracted var-promote (Type/c (listof symbol?) . -> . Type/c)] + [cond-contracted var-demote (Type/c (listof symbol?) . -> . Type/c)])) (define-signature constraints^ ([cond-contracted exn:infer? (any/c . -> . boolean?)] @@ -22,12 +22,12 @@ [cond-contracted cset-meet* ((listof cset?) . -> . cset?)] no-constraint [cond-contracted empty-cset ((listof symbol?) (listof symbol?) . -> . cset?)] - [cond-contracted insert (cset? symbol? Type? Type? . -> . cset?)] + [cond-contracted insert (cset? symbol? Type/c Type/c . -> . cset?)] [cond-contracted cset-combine ((listof cset?) . -> . cset?)] [cond-contracted c-meet ((c? c?) (symbol?) . ->* . c?)])) (define-signature restrict^ - ([cond-contracted restrict (Type? Type? . -> . Type?)])) + ([cond-contracted restrict (Type/c Type/c . -> . Type/c)])) (define-signature infer^ ([cond-contracted infer ((;; variables from the forall @@ -35,9 +35,9 @@ ;; indexes from the forall (listof symbol?) ;; actual argument types from call site - (listof Type?) + (listof Type/c) ;; domain - (listof Type?) + (listof Type/c) ;; range (or/c #f Type?)) ;; optional expected type @@ -48,16 +48,16 @@ ;; indexes from the forall (listof symbol?) ;; actual argument types from call site - (listof Type?) + (listof Type/c) ;; domain - (listof Type?) + (listof Type/c) ;; rest - (or/c #f Type?) + (or/c #f Type/c) ;; range (or/c #f Type?)) ;; [optional] expected type ((or/c #f Type?)) . ->* . any)] [cond-contracted infer/dots (((listof symbol?) symbol? - (listof Type?) (listof Type?) Type? Type? (listof symbol?)) + (listof Type/c) (listof Type/c) Type/c Type? (listof symbol?)) (#:expected (or/c #f Type?)) . ->* . any)]))