diff --git a/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss b/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss index 6601529e..64da1f72 100644 --- a/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss +++ b/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss @@ -9,8 +9,9 @@ base-env-indexing) (typecheck typechecker) (rep type-rep filter-rep object-rep) - (rename-in (types utils union convenience) + (rename-in (types utils union convenience abbrev) [Un t:Un] + [true-filter -true-filter] [-> t:->]) (utils tc-utils utils) unstable/mutated-vars @@ -137,11 +138,11 @@ (tc-e/t 3 -Pos) (tc-e/t "foo" -String) (tc-e (+ 3 4) -Pos) - [tc-e/t (lambda: () 3) (t:-> -Pos : (-LFS (list) (list (make-LBot))))] - [tc-e/t (lambda: ([x : Number]) 3) (t:-> N -Pos : (-LFS (list) (list (make-LBot))))] - [tc-e/t (lambda: ([x : Number] [y : Boolean]) 3) (t:-> N B -Pos : (-LFS (list) (list (make-LBot))))] - [tc-e/t (lambda () 3) (t:-> -Pos : (-LFS (list) (list (make-LBot))))] - [tc-e (values 3 4) #:ret (ret (list -Pos -Pos) (list (-FS (list) (list (make-Bot))) (-FS (list) (list (make-Bot)))))] + [tc-e/t (lambda: () 3) (t:-> -Pos : -true-filter)] + [tc-e/t (lambda: ([x : Number]) 3) (t:-> N -Pos : -true-filter)] + [tc-e/t (lambda: ([x : Number] [y : Boolean]) 3) (t:-> N B -Pos : -true-filter)] + [tc-e/t (lambda () 3) (t:-> -Pos : -true-filter)] + [tc-e (values 3 4) #:ret (ret (list -Pos -Pos) (list -true-filter -true-filter))] [tc-e (cons 3 4) (-pair -Pos -Pos)] [tc-e (cons 3 (ann '() : (Listof Integer))) (make-Listof -Integer)] [tc-e (void) -Void] @@ -474,15 +475,15 @@ (t:-> Univ N)] [tc-e/t (let ([p? (lambda: ([x : Any]) (not (number? x)))]) (lambda: ([x : Any]) (if (p? x) 12 (add1 x)))) - (t:-> Univ N : (-LFS null (list (make-LTypeFilter -Number null 0))))] + (t:-> Univ N : (-FS -top (-filter -Number #'x)))] [tc-e/t (let* ([z 1] [p? (lambda: ([x : Any]) (number? z))]) (lambda: ([x : Any]) (if (p? x) 11 12))) - (t:-> Univ -Pos : (-LFS null (list (make-LBot))))] + (t:-> Univ -Pos : -true-filter)] [tc-e/t (let* ([z 1] [p? (lambda: ([x : Any]) (number? z))]) (lambda: ([x : Any]) (if (p? x) x 12))) - (t:-> Univ Univ : (-LFS (list (-not-filter (-val #f))) (list (-filter (-val #f)))) : (make-LPath null 0))] + (make-pred-ty Univ Univ (-val #f) 0 null)] [tc-e/t (let* ([z (ann 1 : Any)] [p? (lambda: ([x : Any]) (not (number? z)))]) (lambda: ([x : Any]) (if (p? x) x 12))) @@ -490,7 +491,7 @@ [tc-e/t (let* ([z 1] [p? (lambda: ([x : Any]) (not (number? z)))]) (lambda: ([x : Any]) (if (p? x) x 12))) - (t:-> Univ -Pos : (-LFS null (list (make-LBot))))] + (t:-> Univ -Pos : -true-filter)] [tc-e/t (let* ([z 1] [p? (lambda: ([x : Any]) z)]) (lambda: ([x : Any]) (if (p? x) x 12))) @@ -650,19 +651,21 @@ ;; instantiating non-dotted terms [tc-e/t (inst (plambda: (a) ([x : a]) x) Integer) (make-Function (list (make-arr* (list -Integer) -Integer - #:filters (-LFS (list (-not-filter (-val #f))) (list (-filter (-val #f)))) - #:object (make-LPath null 0))))] + #:names (list #'x) + #:filters (-FS (-not-filter (-val #f) #'x) + (-filter (-val #f) #'x)) + #:object (make-Path null #'x))))] [tc-e/t (inst (plambda: (a) [x : a *] (apply list x)) Integer) ((list) -Integer . ->* . (-lst -Integer))] ;; instantiating dotted terms [tc-e/t (inst (plambda: (a ...) [xs : a ... a] 3) Integer Boolean Integer) - (-Integer B -Integer . t:-> . -Pos : (-LFS null (list (make-LBot))))] + (-Integer B -Integer . t:-> . -Pos : -true-filter)] [tc-e/t (inst (plambda: (a ...) [xs : (a ... a -> Integer) ... a] 3) Integer Boolean Integer) ((-Integer B -Integer . t:-> . -Integer) (-Integer B -Integer . t:-> . -Integer) (-Integer B -Integer . t:-> . -Integer) - . t:-> . -Pos : (-LFS null (list (make-LBot))))] + . t:-> . -Pos : -true-filter)] [tc-e/t (plambda: (z x y ...) () (inst map z x y ... y)) (-polydots (z x y) (t:-> (cl->* @@ -722,13 +725,13 @@ (lambda: ([y : (a ... a -> Number)]) (apply y zs)) ys))) - (-polydots (a) ((list) ((list) (a a) . ->... . N) . ->* . ((list) (a a) . ->... . (-lst N)) : (-LFS null (list (make-LBot)))))] + (-polydots (a) ((list) ((list) (a a) . ->... . N) . ->* . ((list) (a a) . ->... . (-lst N)) : -true-filter))] [tc-e/t (plambda: (a ...) [ys : (a ... a -> Number) *] (lambda: [zs : a ... a] (map (lambda: ([y : (a ... a -> Number)]) (apply y zs)) ys))) - (-polydots (a) ((list) ((list) (a a) . ->... . N) . ->* . ((list) (a a) . ->... . (-lst N)) : (-LFS null (list (make-LBot)))))] + (-polydots (a) ((list) ((list) (a a) . ->... . N) . ->* . ((list) (a a) . ->... . (-lst N)) : -true-filter))] [tc-e/t (lambda: ((x : (All (t) t))) ((inst (inst x (All (t) (t -> t))) @@ -779,16 +782,16 @@ [user : Number] [gc : Number]) 'whatever)) - #:ret (ret (-val 'whatever) (-FS (list) (list (make-Bot))))] + #:ret (ret (-val 'whatever) -true-filter)] [tc-e (let: ([l : (Listof Any) (list 1 2 3)]) (if (andmap number? l) (+ 1 (car l)) 7)) -Number] (tc-e (or (string->number "7") 7) - #:ret (ret -Number (-FS (list) (list (make-Bot))))) + #:ret (ret -Number -true-filter)) [tc-e (let ([x 1]) (if x x (add1 x))) - #:ret (ret -Pos (-FS (list) (list (make-Bot))))] + #:ret (ret -Pos -true-filter)] [tc-e (let: ([x : (U (Vectorof Number) String) (vector 1 2 3)]) (if (vector? x) (vector-ref x 0) (string-length x))) -Number] diff --git a/collects/typed-scheme/env/init-envs.ss b/collects/typed-scheme/env/init-envs.ss index 472524a4..71726887 100644 --- a/collects/typed-scheme/env/init-envs.ss +++ b/collects/typed-scheme/env/init-envs.ss @@ -38,8 +38,17 @@ [(Mu-name: n b) `(make-Mu ,(sub n) ,(sub b))] [(Poly-names: ns b) `(make-Poly (list ,@(map sub ns)) ,(sub b))] [(PolyDots-names: ns b) `(make-PolyDots (list ,@(map sub ns)) ,(sub b))] - [(? (lambda (e) (or (LatentFilter? e) - (LatentObject? e) + [(arr: dom rng rest drest kws names) + `(make-arr ,(sub dom) ,(sub rng) ,(sub rest) ,(sub drest) ,(sub kws) + (list ,@(for/list ([i names]) `(quote-syntax ,i))))] + [(TypeFilter: t p i) + `(make-TypeFilter ,(sub t) ,(sub p) (quote-syntax ,i))] + [(NotTypeFilter: t p i) + `(make-NotTypeFilter ,(sub t) ,(sub p) (quote-syntax ,i))] + [(Path: p i) + `(make-Path ,(sub p) (quote-syntax ,i))] + [(? (lambda (e) (or (Filter? e) + (Object? e) (PathElem? e))) (app (lambda (v) (vector->list (struct->vector v))) (list-rest tag seq fv fi stx vals))) `(,(gen-constructor tag) ,@(map sub vals))] diff --git a/collects/typed-scheme/env/lexical-env.ss b/collects/typed-scheme/env/lexical-env.ss index f3386bd4..cd3d896c 100644 --- a/collects/typed-scheme/env/lexical-env.ss +++ b/collects/typed-scheme/env/lexical-env.ss @@ -4,7 +4,7 @@ "type-environments.ss" "type-env.ss" unstable/mutated-vars - (only-in scheme/contract ->* -> or/c any/c) + (only-in scheme/contract ->* -> or/c any/c listof cons/c) (utils tc-utils) (only-in (rep type-rep) Type/c) (typecheck tc-metafunctions) diff --git a/collects/typed-scheme/env/type-environments.ss b/collects/typed-scheme/env/type-environments.ss index 2ae35bc6..d8a48855 100644 --- a/collects/typed-scheme/env/type-environments.ss +++ b/collects/typed-scheme/env/type-environments.ss @@ -2,7 +2,7 @@ (require scheme/contract (prefix-in r: "../utils/utils.ss") - scheme/match (r:rep filter-rep rep-utils) unstable/struct + scheme/match (r:rep filter-rep rep-utils type-rep) unstable/struct (except-in (r:utils tc-utils) make-env) (r:typecheck tc-metafunctions)) @@ -49,7 +49,7 @@ ;; the environment for types of ... variables (define dotted-env (make-parameter (make-empty-env free-identifier=?))) -(define/contract (env-map f e) +(r:d/c (env-map f e) ((pair? . -> . pair?) env? . -> . env?) (make env (env-eq? e) (map f (env-l e)) (env-props e))) @@ -95,4 +95,4 @@ (syntax-rules () [(_ i t v . b) (parameterize ([dotted-env (extend/values (list i) (list (cons t v)) (dotted-env))]) . b)])) -(provide/contract [make-empty-env ((-> any/c any/c any/c) . -> . env?)]) +(r:p/c [make-empty-env ((-> any/c any/c any/c) . -> . env?)]) diff --git a/collects/typed-scheme/infer/infer-unit.ss b/collects/typed-scheme/infer/infer-unit.ss index 0980881a..a70e4378 100644 --- a/collects/typed-scheme/infer/infer-unit.ss +++ b/collects/typed-scheme/infer/infer-unit.ss @@ -1,14 +1,17 @@ #lang scheme/unit -(require "../utils/utils.ss" - (rep free-variance type-rep filter-rep rep-utils) - (types convenience union subtype remove-intersect resolve) - (except-in (utils tc-utils) make-env) - (env type-name-env) - (except-in (types utils) Dotted) +(require scheme/require + (except-in + (path-up + "utils/utils.ss" "utils/tc-utils.ss" + "rep/free-variance.ss" "rep/type-rep.ss" "rep/filter-rep.ss" "rep/rep-utils.ss" + "types/convenience.ss" "types/union.ss" "types/subtype.ss" "types/remove-intersect.ss" "types/resolve.ss" + "env/type-name-env.ss") + make-env) + (except-in (path-up "types/utils.ss") Dotted) + (only-in (path-up "env/type-environments.ss") lookup current-tvars) "constraint-structs.ss" - "signatures.ss" - (only-in (env type-environments) lookup current-tvars) + "signatures.ss" scheme/match mzlib/etc mzlib/trace @@ -101,11 +104,13 @@ (define (cgen/filter V X t s) (match* (t s) [(e e) (empty-cset X)] - ;; FIXME - is there something to be said about LBot? - [((LTypeFilter: t p i) (LTypeFilter: s p i)) (cset-meet (cgen V X t s) (cgen V X s t))] - [((LNotTypeFilter: t p i) (LNotTypeFilter: s p i)) (cset-meet (cgen V X t s) (cgen V X s t))] + [(e (Top:)) (empty-cset X)] + ;; FIXME - is there something to be said about the logical ones? + [((TypeFilter: t p i) (TypeFilter: s p i)) (cset-meet (cgen V X t s) (cgen V X s t))] + [((NotTypeFilter: t p i) (NotTypeFilter: s p i)) (cset-meet (cgen V X t s) (cgen V X s t))] [(_ _) (fail! t s)])) +#; (define (cgen/filters V X ts ss) (cond [(null? ss) (empty-cset X)] @@ -119,14 +124,14 @@ (define (cgen/filter-set V X t s) (match* (t s) [(e e) (empty-cset X)] - [((LFilterSet: t+ t-) (LFilterSet: s+ s-)) - (cset-meet (cgen/filters V X t+ s+) (cgen/filters V X t- s-))] + [((FilterSet: t+ t-) (FilterSet: s+ s-)) + (cset-meet (cgen/filter V X t+ s+) (cgen/filter V X t- s-))] [(_ _) (fail! t s)])) (define (cgen/object V X t s) (match* (t s) [(e e) (empty-cset X)] - [(e (LEmpty:)) (empty-cset X)] + [(e (Empty:)) (empty-cset X)] ;; FIXME - do something here [(_ _) (fail! t s)])) @@ -153,8 +158,8 @@ [ret-mapping (cg t s)]) (cset-meet* (list arg-mapping ret-mapping)))] - [((arr: ts t #f (cons dty dbound) '()) - (arr: ss s #f #f '())) + [((arr: ts t #f (cons dty dbound) '() names) + (arr: ss s #f #f '() names*)) (unless (memq dbound X) (fail! S T)) (unless (<= (length ts) (length ss)) @@ -164,10 +169,11 @@ (gensym dbound))] [new-tys (for/list ([var vars]) (substitute (make-F var) dbound dty))] - [new-cset (cgen/arr V (append vars X) (make-arr (append ts new-tys) t #f #f null) s-arr)]) + [new-names (generate-temporaries new-tys)] + [new-cset (cgen/arr V (append vars X) (make-arr (append ts new-tys) t #f #f null (append names new-names)) s-arr)]) (move-vars-to-dmap new-cset dbound vars))] [((arr: ts t #f #f '()) - (arr: ss s #f (cons dty dbound) '())) + (arr: ss s #f (cons dty dbound) '() names*)) (unless (memq dbound X) (fail! S T)) (unless (<= (length ss) (length ts)) @@ -177,7 +183,8 @@ (gensym dbound))] [new-tys (for/list ([var vars]) (substitute (make-F var) dbound dty))] - [new-cset (cgen/arr V (append vars X) t-arr (make-arr (append ss new-tys) s #f #f null))]) + [new-names (generate-temporaries new-tys)] + [new-cset (cgen/arr V (append vars X) t-arr (make-arr (append ss new-tys) s #f #f null (append names* new-names)))]) (move-vars-to-dmap new-cset dbound vars))] [((arr: ts t #f (cons t-dty dbound) '()) (arr: ss s #f (cons s-dty dbound) '())) @@ -201,7 +208,7 @@ (cset-meet* (list arg-mapping darg-mapping ret-mapping)))] [((arr: ts t t-rest #f '()) - (arr: ss s #f (cons s-dty dbound) '())) + (arr: ss s #f (cons s-dty dbound) '() names*)) (unless (memq dbound X) (fail! S T)) (if (<= (length ts) (length ss)) @@ -216,8 +223,9 @@ (gensym dbound))] [new-tys (for/list ([var vars]) (substitute (make-F var) dbound s-dty))] + [new-names (generate-temporaries new-tys)] [new-cset (cgen/arr V (append vars X) t-arr - (make-arr (append ss new-tys) s #f (cons s-dty dbound) null))]) + (make-arr (append ss new-tys) s #f (cons s-dty dbound) null (append names* new-names)))]) (move-vars+rest-to-dmap new-cset dbound vars)))] ;; If dotted <: starred is correct, add it below. Not sure it is. [((arr: ts t #f (cons t-dty dbound) '()) @@ -506,4 +514,4 @@ (define (i s t r) (infer/simple (list s) (list t) r)) -;(trace subst-gen cgen) +;(trace cgen cgen/arr) diff --git a/collects/typed-scheme/infer/promote-demote.ss b/collects/typed-scheme/infer/promote-demote.ss index 1eb261f1..003ae085 100644 --- a/collects/typed-scheme/infer/promote-demote.ss +++ b/collects/typed-scheme/infer/promote-demote.ss @@ -30,9 +30,9 @@ Univ (make-Hashtable (vp k) v))] [#:Param in out - (make-Param (var-demote in V) - (vp out))] - [#:arr dom rng rest drest kws + (make-Param (var-demote in V) + (vp out))] + [#:arr dom rng rest drest kws names (cond [(apply V-in? V (get-filters rng)) (make-top-arr)] @@ -41,7 +41,8 @@ (vp rng) (var-demote (car drest) V) #f - (for/list ([k kws]) (var-demote k V)))] + (for/list ([k kws]) (var-demote k V)) + names)] [else (make-arr (for/list ([d dom]) (var-demote d V)) (vp rng) @@ -49,7 +50,8 @@ (and drest (cons (var-demote (car drest) V) (cdr drest))) - (for/list ([k kws]) (var-demote k V)))])])) + (for/list ([k kws]) (var-demote k V)) + names)])])) (define (var-demote T V) (define (vd t) (var-demote t V)) @@ -63,9 +65,9 @@ (Un) (make-Hashtable (vd k) v))] [#:Param in out - (make-Param (var-promote in V) - (vd out))] - [#:arr dom rng rest drest kws + (make-Param (var-promote in V) + (vd out))] + [#:arr dom rng rest drest kws names (cond [(apply V-in? V (get-filters rng)) (make-top-arr)] @@ -74,7 +76,8 @@ (vd rng) (var-promote (car drest) V) #f - (for/list ([k kws]) (var-demote k V)))] + (for/list ([k kws]) (var-demote k V)) + names)] [else (make-arr (for/list ([d dom]) (var-promote d V)) (vd rng) @@ -82,4 +85,5 @@ (and drest (cons (var-promote (car drest) V) (cdr drest))) - (for/list ([k kws]) (var-demote k V)))])])) + (for/list ([k kws]) (var-demote k V)) + names)])])) diff --git a/collects/typed-scheme/no-check.ss b/collects/typed-scheme/no-check.ss index 6aff7220..2d4bf8d0 100644 --- a/collects/typed-scheme/no-check.ss +++ b/collects/typed-scheme/no-check.ss @@ -8,6 +8,7 @@ (all-defined-out) (all-from-out "private/prims.ss")) + (define-syntax (require/typed stx) (define-syntax-class opt-rename #:attributes (nm spec) diff --git a/collects/typed-scheme/private/base-env-numeric.ss b/collects/typed-scheme/private/base-env-numeric.ss index a7eb9b63..de984fde 100644 --- a/collects/typed-scheme/private/base-env-numeric.ss +++ b/collects/typed-scheme/private/base-env-numeric.ss @@ -41,15 +41,16 @@ ;; numeric predicates [zero? (make-pred-ty (list N) B -Zero)] [number? (make-pred-ty N)] -[integer? (Univ . -> . B : (-LFS (list (-filter (Un -Integer -Flonum))) (list (-not-filter -Integer))))] +[integer? (asym-pred (x) Univ B (-FS (-filter (Un -Integer -Flonum) x) + (-not-filter -Integer x)))] [exact-integer? (make-pred-ty -Integer)] [real? (make-pred-ty -Real)] [inexact-real? (make-pred-ty -Flonum)] [complex? (make-pred-ty N)] [rational? (make-pred-ty -Real)] -[exact? (N . -> . B : (-LFS (list) (list (-not-filter -ExactRational))))] -[inexact? (N . -> . B : (-LFS (list) (list (-not-filter -Flonum))))] -[fixnum? (Univ . -> . B : (-LFS (list (-filter -Integer)) null))] +[exact? (asym-pred (x) N B (-FS -top (-not-filter -ExactRational x)))] +[inexact? (asym-pred (x) N B (-FS -top (-not-filter -Flonum x)))] +[fixnum? (asym-pred (x) Univ B (-FS (-filter -Integer x) -top))] [positive? (-> -Real B)] [negative? (-> -Real B)] [exact-positive-integer? (make-pred-ty -Pos)] @@ -185,7 +186,6 @@ [unsafe-fllog fl-unop] [unsafe-flexp fl-unop] [unsafe-flsqrt fl-unop] -[unsafe-fx->fl (-Integer . -> . -Flonum)] [unsafe-fx+ fx-op] [unsafe-fx- fx-intop] @@ -262,7 +262,6 @@ [fllog fl-unop] [flexp fl-unop] [flsqrt fl-unop] -[->fl (-Integer . -> . -Flonum)] ;; safe flvector ops diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss index 0c2b5c9d..8a120f92 100644 --- a/collects/typed-scheme/private/base-env.ss +++ b/collects/typed-scheme/private/base-env.ss @@ -704,40 +704,3 @@ ;; mutable pairs - - -;; Byte and String Output (Section 12.3 of the Reference) -[write-char (cl-> [(-Char) -Void] - [(-Char -Output-Port) -Void])] -[write-byte (cl-> [(-Nat) -Void] - [(-Nat -Output-Port) -Void])] -[newline (cl-> [() -Void] - [(-Output-Port) -Void])] -[write-string (cl-> [(-String) -Nat] - [(-String -Output-Port) -Nat] - [(-String -Output-Port -Nat) -Nat] - [(-String -Output-Port -Nat -Nat) -Nat])] -[write-bytes (cl-> [(-Bytes) -Nat] - [(-Bytes -Output-Port) -Nat] - [(-Bytes -Output-Port -Nat) -Nat] - [(-Bytes -Output-Port -Nat -Nat) -Nat])] -[write-bytes-avail (cl-> [(-Bytes) -Nat] - [(-Bytes -Output-Port) -Nat] - [(-Bytes -Output-Port -Nat) -Nat] - [(-Bytes -Output-Port -Nat -Nat) -Nat])] -[write-bytes-avail* (cl-> [(-Bytes) (-opt -Nat)] - [(-Bytes -Output-Port) (-opt -Nat)] - [(-Bytes -Output-Port -Nat) (-opt -Nat)] - [(-Bytes -Output-Port -Nat -Nat) (-opt -Nat)])] -[write-bytes-avail/enable-break (cl-> [(-Bytes) -Nat] - [(-Bytes -Output-Port) -Nat] - [(-Bytes -Output-Port -Nat) -Nat] - [(-Bytes -Output-Port -Nat -Nat) -Nat])] -[write-special (cl-> [(Univ) -Boolean] - [(Univ -Output-Port) -Boolean])] -;; Need event type before we can include these -;;write-special-avail* -;;write-bytes-avail-evt -;;write-special-evt -[port-writes-atomic? (-Output-Port . -> . -Boolean)] -[port-writes-special? (-Output-Port . -> . -Boolean)] diff --git a/collects/typed-scheme/private/type-contract.ss b/collects/typed-scheme/private/type-contract.ss index a1d4ae6e..d1b0c647 100644 --- a/collects/typed-scheme/private/type-contract.ss +++ b/collects/typed-scheme/private/type-contract.ss @@ -68,7 +68,7 @@ (define-values (dom* opt-dom* rngs* rst) (match a ;; functions with no filters or objects - [(arr: dom (Values: (list (Result: rngs (LFilterSet: '() '()) (LEmpty:)) ...)) rst #f kws) + [(arr: dom (Values: (list (Result: rngs (FilterSet: (Top:) (Top:)) (Empty:)) ...)) rst #f kws) (let-values ([(mand-kws opt-kws) (partition (match-lambda [(Keyword: _ _ mand?) mand?]) kws)] [(conv) (match-lambda [(Keyword: kw kty _) (list kw (t->c/neg kty))])]) (values (append (map t->c/neg dom) (append-map conv mand-kws)) diff --git a/collects/typed-scheme/rep/filter-rep.ss b/collects/typed-scheme/rep/filter-rep.ss index 1ae4f5ab..44be1a90 100644 --- a/collects/typed-scheme/rep/filter-rep.ss +++ b/collects/typed-scheme/rep/filter-rep.ss @@ -9,15 +9,22 @@ (λ (e) (and (Filter? e) (not (NoFilter? e)) (not (FilterSet? e)))))) -(define LatentFilter/c +(define FilterSet/c + (flat-named-contract + 'FilterSet + (λ (e) (or (FilterSet? e) (NoFilter? e))))) + + +#;(define LatentFilter/c (flat-named-contract 'LatentFilter (λ (e) (and (LatentFilter? e) (not (LFilterSet? e)))))) -(provide Filter/c LatentFilter/c FilterSet/c LatentFilterSet/c index/c) +(provide Filter/c FilterSet/c); LatentFilter/c LatentFilterSet/c index/c) (df Bot () [#:fold-rhs #:base]) +(df Top () [#:fold-rhs #:base]) (df TypeFilter ([t Type?] [p (listof PathElem?)] [v identifier?]) [#:intern (list t p (hash-id v))] @@ -32,24 +39,29 @@ [#:fold-rhs (*NotTypeFilter (type-rec-id t) (map pathelem-rec-id p) v)]) ;; implication -(df ImpFilter ([a (non-empty-listof Filter/c)] [c (non-empty-listof Filter/c)]) - [#:frees (combine-frees (map free-vars* (append a c))) - (combine-frees (map free-idxs* (append a c)))]) +(df ImpFilter ([a Filter/c] [c Filter/c])) + +(df AndFilter ([fs (non-empty-listof Filter/c)]) + [#:fold-rhs (*AndFilter (map filter-rec-id fs))] + [#:frees (combine-frees (map free-vars* fs)) + (combine-frees (map free-idxs* fs))]) + +(df OrFilter ([fs (non-empty-listof Filter/c)]) + [#:fold-rhs (*OrFilter (map filter-rec-id fs))] + [#:frees (combine-frees (map free-vars* fs)) + (combine-frees (map free-idxs* fs))]) (df FilterSet (thn els) - [#:frees (combine-frees (map free-vars* (append thn els))) - (combine-frees (map free-idxs* (append thn els)))] - [#:fold-rhs (*FilterSet (map filter-rec-id thn) (map filter-rec-id els))] - [#:contract (->d ([t (cond [(ormap Bot? t) - (list/c Bot?)] - [(ormap Bot? e) - (flat-named-contract "e was Bot" (list/c))] - [else (listof Filter/c)])] - [e (cond [(ormap Bot? e) - (list/c Bot?)] - [(ormap Bot? t) - (flat-named-contract "t was Bot" (list/c))] - [else (listof Filter/c)])]) + [#:contract (->d ([t (cond [(Bot? t) + Bot?] + [(Bot? e) + Top?] + [else Filter/c])] + [e (cond [(Bot? e) + Bot?] + [(Bot? t) + Top?] + [else Filter/c])]) (#:syntax [stx #f]) [result FilterSet?])]) @@ -57,6 +69,7 @@ ;; should only be used for parsing type annotations and expected types (df NoFilter () [#:fold-rhs #:base]) +#| (define index/c (or/c natural-number/c keyword?)) (dlf LBot () [#:fold-rhs #:base]) @@ -69,6 +82,8 @@ [#:frees (lambda (frees*) (combine-frees (map (compose make-invariant frees*) (cons t p))))] [#:fold-rhs (*LNotTypeFilter (type-rec-id t) (map pathelem-rec-id p) idx)]) + + ;; implication (dlf LImpFilter ([a (non-empty-listof LatentFilter/c)] [c (non-empty-listof LatentFilter/c)]) [#:frees (combine-frees (map free-vars* (append a c))) @@ -92,15 +107,11 @@ (#:syntax [stx #f]) [result LFilterSet?])]) -(define FilterSet/c - (flat-named-contract - 'FilterSet - (λ (e) (or (FilterSet? e) (NoFilter? e))))) - (define LatentFilterSet/c (flat-named-contract 'LatentFilterSet (λ (e) (or (LFilterSet? e))))) +|# -(define filter-equal? eq?) +(define (filter-equal? a b) (= (Rep-seq a) (Rep-seq b))) (provide filter-equal?) \ No newline at end of file diff --git a/collects/typed-scheme/rep/object-rep.ss b/collects/typed-scheme/rep/object-rep.ss index 9c5214b3..be8fcb16 100644 --- a/collects/typed-scheme/rep/object-rep.ss +++ b/collects/typed-scheme/rep/object-rep.ss @@ -1,6 +1,7 @@ #lang scheme/base (require scheme/match scheme/contract "rep-utils.ss" "free-variance.ss" "filter-rep.ss") +(provide object-equal?) (dpe CarPE () [#:fold-rhs #:base]) (dpe CdrPE () [#:fold-rhs #:base]) @@ -16,12 +17,16 @@ [#:frees (combine-frees (map free-vars* p)) (combine-frees (map free-idxs* p))] [#:fold-rhs (*Path (map pathelem-rec-id p) v)]) -;; represents no info about the filters of this expression +;; represents no info about the object of this expression ;; should only be used for parsing type annotations and expected types (do NoObject () [#:fold-rhs #:base]) +(define (object-equal? o1 o2) (= (Rep-seq o1) (Rep-seq o2))) + +#| (dlo LEmpty () [#:fold-rhs #:base]) (dlo LPath ([p (listof PathElem?)] [idx index/c]) [#:frees (combine-frees (map free-vars* p)) (combine-frees (map free-idxs* p))] [#:fold-rhs (*LPath (map pathelem-rec-id p) idx)]) +|# \ No newline at end of file diff --git a/collects/typed-scheme/rep/type-rep.ss b/collects/typed-scheme/rep/type-rep.ss index fe192c15..da99c9dd 100644 --- a/collects/typed-scheme/rep/type-rep.ss +++ b/collects/typed-scheme/rep/type-rep.ss @@ -5,7 +5,7 @@ "rep-utils.ss" "object-rep.ss" "filter-rep.ss" "free-variance.ss" mzlib/trace scheme/match scheme/contract - (for-syntax scheme/base)) + (for-syntax scheme/base syntax/parse)) (define name-table (make-weak-hasheq)) @@ -132,9 +132,9 @@ [#:frees (λ (f) (f ty))] [#:fold-rhs (*Keyword kw (type-rec-id ty) required?)]) -(dt Result ([t Type/c] [f LFilterSet?] [o LatentObject?]) +(dt Result ([t Type/c] [f FilterSet?] [o Object?]) [#:frees (λ (frees) (combine-frees (map frees (list t f o))))] - [#:fold-rhs (*Result (type-rec-id t) (latentfilter-rec-id f) (latentobject-rec-id o))]) + [#:fold-rhs (*Result (type-rec-id t) (filter-rec-id f) (object-rec-id o))]) ;; types : Listof[Type] (dt Values ([rs (listof Result?)]) @@ -150,7 +150,11 @@ [rng (or/c Values? ValuesDots?)] [rest (or/c #f Type/c)] [drest (or/c #f (cons/c Type/c (or/c natural-number/c symbol?)))] - [kws (listof Keyword?)]) + [kws (listof Keyword?)] + ;; order is: fixed, rest/drest, keywords + [names (listof identifier?)]) + #:no-provide + [#:intern (list dom rng rest drest kws (map hash-id names))] [#:frees (combine-frees (append (map (compose flip-variances free-vars*) (append (if rest (list rest) null) @@ -179,7 +183,8 @@ (type-rec-id rng) (and rest (type-rec-id rest)) (and drest (cons (type-rec-id (car drest)) (cdr drest))) - (map type-rec-id kws))]) + (map type-rec-id kws) + names)]) ;; top-arr is the supertype of all function types (dt top-arr () [#:fold-rhs #:base]) @@ -396,7 +401,7 @@ ;; necessary to avoid infinite loops [#:Union elems (*Union (remove-dups (sort (map sb elems) type . boolean?)]) diff --git a/collects/typed-scheme/typecheck/tc-app.ss b/collects/typed-scheme/typecheck/tc-app.ss index 9bc405ca..85d7a0e8 100644 --- a/collects/typed-scheme/typecheck/tc-app.ss +++ b/collects/typed-scheme/typecheck/tc-app.ss @@ -52,36 +52,24 @@ (alt equal? equal?-able))) (match* ((single-value v1) (single-value v2)) [((tc-result1: t _ o) (tc-result1: (Value: (? ok? val)))) - (ret -Boolean (apply-filter (make-LFilterSet (list (make-LTypeFilter (-val val) null 0)) (list (make-LNotTypeFilter (-val val) null 0))) t o))] + (ret -Boolean + (-FS (-filter-at (-val val) o) + (-not-filter-at (-val val) o)))] [((tc-result1: (Value: (? ok? val))) (tc-result1: t _ o)) - (ret -Boolean (apply-filter (make-LFilterSet (list (make-LTypeFilter (-val val) null 0)) (list (make-LNotTypeFilter (-val val) null 0))) t o))] + (ret -Boolean + (-FS (-filter-at (-val val) o) + (-not-filter-at (-val val) o)))] [((tc-result1: t _ o) - (and (? (lambda _ (free-identifier=? #'member comparator))) - (tc-result1: (app untuple (list (and ts (Value: _)) ...))))) + (or (and (? (lambda _ (free-identifier=? #'member comparator))) + (tc-result1: (app untuple (list (and ts (Value: _)) ...)))) + (and (? (lambda _ (free-identifier=? #'memv comparator))) + (tc-result1: (app untuple (list (and ts (Value: (? eqv?-able))) ...)))) + (and (? (lambda _ (free-identifier=? #'memq comparator))) + (tc-result1: (app untuple (list (and ts (Value: (? eq?-able))) ...)))))) (let ([ty (apply Un ts)]) (ret (Un (-val #f) t) - (apply-filter - (make-LFilterSet (list (make-LTypeFilter ty null 0)) - (list (make-LNotTypeFilter ty null 0))) - t o)))] - [((tc-result1: t _ o) - (and (? (lambda _ (free-identifier=? #'memv comparator))) - (tc-result1: (app untuple (list (and ts (Value: (? eqv?-able))) ...))))) - (let ([ty (apply Un ts)]) - (ret (Un (-val #f) t) - (apply-filter - (make-LFilterSet (list (make-LTypeFilter ty null 0)) - (list (make-LNotTypeFilter ty null 0))) - t o)))] - [((tc-result1: t _ o) - (and (? (lambda _ (free-identifier=? #'memq comparator))) - (tc-result1: (app untuple (list (and ts (Value: (? eq?-able))) ...))))) - (let ([ty (apply Un ts)]) - (ret (Un (-val #f) t) - (apply-filter - (make-LFilterSet (list (make-LTypeFilter ty null 0)) - (list (make-LNotTypeFilter ty null 0))) - t o)))] + (-FS (-filter-at ty o) + (-not-filter-at ty o))))] [(_ _) (ret -Boolean)])) @@ -609,7 +597,7 @@ (= (length d) (length (syntax->list #'args)))) dom) - (Values: (list (Result: v (LFilterSet: '() '()) (LEmpty:)))) + (Values: (list (Result: v (FilterSet: (Top:) (Top:)) (Empty:)))) #f #f (list (Keyword: _ _ #f) ...))))))) ;(printf "f dom: ~a ~a~n" (syntax->datum #'f) dom) (let ([arg-tys (map (lambda (a t) (tc-expr/check a (ret t))) @@ -740,10 +728,13 @@ ;; syntax? syntax? arr? (listof tc-results?) (or/c #f tc-results) [boolean?] -> tc-results? (define (tc/funapp1 f-stx args-stx ftype0 argtys expected #:check [check? #t]) + ;(printf "got to here 0~a~n" args-stx) (match* (ftype0 argtys) ;; we check that all kw args are optional - [((arr: dom (Values: (list (Result: t-r lf-r lo-r) ...)) rest #f (list (Keyword: _ _ #f) ...)) + [((arr: dom (Values: (list (Result: t-r f-r o-r) ...)) rest #f (list (Keyword: _ _ #f) ...) + names) (list (tc-result1: t-a phi-a o-a) ...)) + ;(printf "got to here 1~a~n" args-stx) (when check? (cond [(and (not rest) (not (= (length dom) (length t-a)))) (tc-error/expr #:return (ret t-r) @@ -751,26 +742,27 @@ [(and rest (< (length t-a) (length dom))) (tc-error/expr #:return (ret t-r) "Wrong number of arguments, expected at least ~a and got ~a" (length dom) (length t-a))]) - (for ([dom-t (if rest (in-sequence-forever dom rest) (in-list dom))] [a (syntax->list args-stx)] [arg-t (in-list t-a)]) + (for ([dom-t (if rest (in-sequence-forever dom rest) (in-list dom))] + [a (in-list (syntax->list args-stx))] + [arg-t (in-list t-a)]) (parameterize ([current-orig-stx a]) (check-below arg-t dom-t)))) - (let* (;; Listof[Listof[LFilterSet]] - [lfs-f (for/list ([lf lf-r]) - (for/list ([i (in-indexes dom)]) - (split-lfilters lf i)))] - ;; Listof[FilterSet] - [f-r (for/list ([lfs lfs-f]) - (merge-filter-sets - (for/list ([lf lfs] [t t-a] [o o-a]) - (apply-filter lf t o))))] - ;; Listof[Object] - [o-r (for/list ([lo lo-r]) - (match lo - [(LPath: pi* i) - (match (object-index o-a i) - [(Path: pi x) (make-Path (append pi* pi) x)] - [_ (make-Empty)])] - [_ (make-Empty)]))]) - (ret t-r f-r o-r))] + ;(printf "got to here 2 ~a ~a ~a ~n" dom names o-a) + (let-values ([(names o-a) + (for/lists (n o) ([d (in-list dom)] + [nm (in-list names)] + [oa (in-list o-a)]) + (values nm oa))]) + ;(printf "got to here 3~a~n" args-stx) + (let* (;; Listof[FilterSet] + [f-r (for/list ([f f-r]) + (apply-filter f names o-a))] + ;; Listof[Object] + [o-r (for/list ([o o-r]) + (apply-object o names o-a))] + ;; Listof[Type] + [t-r (for/list ([t t-r]) + (apply-type t names o-a))]) + (ret t-r f-r o-r)))] [((arr: _ _ _ drest '()) _) (int-err "funapp with drest args NYI")] [((arr: _ _ _ _ kws) _) diff --git a/collects/typed-scheme/typecheck/tc-envops.ss b/collects/typed-scheme/typecheck/tc-envops.ss index c009e869..3efea8a9 100644 --- a/collects/typed-scheme/typecheck/tc-envops.ss +++ b/collects/typed-scheme/typecheck/tc-envops.ss @@ -15,8 +15,6 @@ (typecheck tc-metafunctions) (for-syntax scheme/base)) -(provide env+) - (define (replace-nth l i f) (cond [(null? l) (error 'replace-nth "list not long enough" l i f)] [(zero? i) (cons (f (car l)) (cdr l))] @@ -75,3 +73,5 @@ (set-box! flag #f)) new-t)) x Γ)]))) + +(p/c [env+ (env? (listof Filter/c) (box/c #t). -> . env?)]) \ No newline at end of file diff --git a/collects/typed-scheme/typecheck/tc-expr-unit.ss b/collects/typed-scheme/typecheck/tc-expr-unit.ss index dbe0f184..9d22a03c 100644 --- a/collects/typed-scheme/typecheck/tc-expr-unit.ss +++ b/collects/typed-scheme/typecheck/tc-expr-unit.ss @@ -135,8 +135,8 @@ (define (tc-id id) (let* ([ty (lookup-type/lexical id)]) (ret ty - (make-FilterSet (list (make-NotTypeFilter (-val #f) null id)) - (list (make-TypeFilter (-val #f) null id))) + (make-FilterSet (make-NotTypeFilter (-val #f) null id) + (make-TypeFilter (-val #f) null id)) (make-Path null id)))) ;; typecheck an expression, but throw away the effect @@ -174,7 +174,7 @@ (if (= (length ts) (length ts2)) (ret ts2 fs os) (ret ts2))] - [((tc-result1: t1 f1 o1) (tc-result1: t2 (FilterSet: (list) (list)) (Empty:))) + [((tc-result1: t1 f1 o1) (tc-result1: t2 (FilterSet: (Top:) (Top:)) (Empty:))) (cond [(not (subtype t1 t2)) (tc-error/expr "Expected ~a, but got ~a" t2 t1)]) @@ -183,6 +183,9 @@ (cond [(not (subtype t1 t2)) (tc-error/expr "Expected ~a, but got ~a" t2 t1)] + [(and (not (filter-equal? f1 f2)) + (object-equal? o1 o2)) + (tc-error/expr "Expected result with filter ~a, got filter ~a" f2 f1)] [(not (and (equal? f1 f2) (equal? o1 o2))) (tc-error/expr "Expected result with filter ~a and ~a, got filter ~a and ~a" f2 (print-object o2) f1 (print-object o1))]) expected] @@ -254,6 +257,7 @@ (add-typeof-expr form t) t)])))) +#; (define (tc-or e1 e2 or-part [expected #f]) (match (single-value e1) [(tc-result1: t1 (and f1 (FilterSet: fs+ fs-)) o1) @@ -345,14 +349,7 @@ [(let-values (((_) meth)) (let-values (((_ _) (#%plain-app find-method/who _ rcvr _))) (#%plain-app _ _ args ...))) - (tc/send #'rcvr #'meth #'(args ...) expected)] - ;; or - [(let-values ([(or-part) e1]) (if op1 op2 e2)) - (and - (identifier? #'op1) (identifier? #'op2) - (free-identifier=? #'or-part #'op1) - (free-identifier=? #'or-part #'op2)) - (tc-or #'e1 #'e2 #'or-part expected)] + (tc/send #'rcvr #'meth #'(args ...) expected)] ;; let [(let-values ([(name ...) expr] ...) . body) (tc/let-values #'((name ...) ...) #'(expr ...) #'body form expected)] @@ -415,12 +412,6 @@ (let-values (((_ _) (#%plain-app find-method/who _ rcvr _))) (#%plain-app _ _ args ...))) (tc/send #'rcvr #'meth #'(args ...))] - ;; or - [(let-values ([(or-part) e1]) (if op1 op2 e2)) - (and (identifier? #'op1) (identifier? #'op2) - (free-identifier=? #'or-part #'op1) - (free-identifier=? #'or-part #'op2)) - (tc-or #'e1 #'e2 #'or-part)] ;; let [(let-values ([(name ...) expr] ...) . body) (tc/let-values #'((name ...) ...) #'(expr ...) #'body form)] diff --git a/collects/typed-scheme/typecheck/tc-if.ss b/collects/typed-scheme/typecheck/tc-if.ss index 9bb9f5e7..184bb514 100644 --- a/collects/typed-scheme/typecheck/tc-if.ss +++ b/collects/typed-scheme/typecheck/tc-if.ss @@ -4,14 +4,14 @@ (require (rename-in "../utils/utils.ss" [infer r:infer])) (require "signatures.ss" (rep type-rep filter-rep object-rep) - (rename-in (types convenience subtype union utils comparison remove-intersect) + (rename-in (types convenience subtype union utils comparison remove-intersect abbrev) [remove *remove]) (env lexical-env type-environments) (r:infer infer) (utils tc-utils) (typecheck tc-envops tc-metafunctions) syntax/kerncase - mzlib/trace + mzlib/trace unstable/debug scheme/match) ;; if typechecking @@ -43,18 +43,27 @@ [(tc-result1: _ (and f1 (FilterSet: fs+ fs-)) _) (let*-values ([(flag+ flag-) (values (box #t) (box #t))] [(derived-imps+ derived-atoms+) - (combine-props fs+ (env-props (lexical-env)))]) - (match-let* ([(tc-results: ts fs2 os2) (with-lexical-env (env+ (lexical-env) fs+ flag+) (tc thn (unbox flag+)))] - [(tc-results: us fs3 os3) (with-lexical-env (env+ (lexical-env) fs- flag-) (tc els (unbox flag-)))]) + (combine-props (list fs+) (env-props (lexical-env)))]) + (match-let* ([(tc-results: ts fs2 os2) (with-lexical-env (env+ (lexical-env) (list fs+) flag+) (tc thn (unbox flag+)))] + [(tc-results: us fs3 os3) (with-lexical-env (env+ (lexical-env) (list fs-) flag-) (tc els (unbox flag-)))]) ;; if we have the same number of values in both cases (cond [(= (length ts) (length us)) - (let ([r - (combine-results - (for/list ([t ts] [u us] [o2 os2] [o3 os3] [f2 fs2] [f3 fs3]) - (combine-filter f1 f2 f3 t u o2 o3)))]) - (if expected - (check-below r expected) - r))] + (let ([r (combine-results + (for/list ([f2 fs2] [f3 fs3] [t2 ts] [t3 us] [o2 os2] [o3 os3]) + (let ([filter + (match* (f2 f3) + [((NoFilter:) _) + (-FS -top -top)] + [(_ (NoFilter:)) + (-FS -top -top)] + [((FilterSet: f2+ f2-) (FilterSet: f3+ f3-)) + (-FS (-or (-and fs+ f2+) (-and fs- f3+)) + (-or (-and fs+ f2-) (-and fs- f3-)))])] + [type (Un t2 t3)] + [object (if (object-equal? o2 o3) o2 (make-Empty))]) + ;(printf "result filter is: ~a\n" filter) + (ret type filter object))))]) + (if expected (check-below r expected) r))] ;; special case if one of the branches is unreachable [(and (= 1 (length us)) (type-equal? (car us) (Un))) (if expected (check-below (ret ts fs2 os2) expected) (ret ts fs2 os2))] @@ -63,7 +72,7 @@ ;; otherwise, error [else (tc-error/expr #:return (ret (or expected Err)) - "Expected the same number of values from both branches of if expression, but got ~a and ~a" + "Expected the same number of values from both branches of `if' expression, but got ~a and ~a" (length ts) (length us))])))] [(tc-results: t _ _) (tc-error/expr #:return (ret (or expected Err)) diff --git a/collects/typed-scheme/typecheck/tc-lambda-unit.ss b/collects/typed-scheme/typecheck/tc-lambda-unit.ss index e4656128..c3901b74 100644 --- a/collects/typed-scheme/typecheck/tc-lambda-unit.ss +++ b/collects/typed-scheme/typecheck/tc-lambda-unit.ss @@ -14,7 +14,8 @@ (types abbrev utils) (env type-environments lexical-env) (utils tc-utils) - mzlib/plt-match) + unstable/debug + scheme/match) (require (for-template scheme/base "internal-forms.ss")) (import tc-expr^) @@ -32,9 +33,7 @@ [(struct lam-result ((list (list arg-ids arg-tys) ...) (list (list kw kw-id kw-ty req?) ...) rest drest body)) (make-arr arg-tys - (abstract-filters (append (for/list ([i (in-naturals)] [_ arg-ids]) i) kw) - (append arg-ids kw-id) - body) + (abstract-filters body) #:kws (map make-Keyword kw kw-ty req?) #:rest rest #:drest drest)])) @@ -200,7 +199,7 @@ [(tc-result1: (Function: (list (arr: argss rets rests drests '()) ...))) (for/list ([args argss] [ret rets] [rest rests] [drest drests]) (tc/lambda-clause/check (car (syntax->list formals)) (car (syntax->list bodies)) - args (values->tc-results ret (formals->list (car (syntax->list formals)))) rest drest))] + args (values->tc-results ret) rest drest))] [_ (go (syntax->list formals) (syntax->list bodies) null null null)]))] ;; otherwise [else (go (syntax->list formals) (syntax->list bodies) null null null)])) diff --git a/collects/typed-scheme/typecheck/tc-metafunctions.ss b/collects/typed-scheme/typecheck/tc-metafunctions.ss index 435980a4..1cff7d37 100644 --- a/collects/typed-scheme/typecheck/tc-metafunctions.ss +++ b/collects/typed-scheme/typecheck/tc-metafunctions.ss @@ -5,14 +5,18 @@ [-> -->] [->* -->*] [one-of/c -one-of/c]) - (rep type-rep filter-rep) scheme/list + (rep type-rep filter-rep rep-utils) scheme/list scheme/contract scheme/match unstable/match (for-syntax scheme/base)) -(provide combine-filter apply-filter abstract-filter abstract-filters combine-props - split-lfilters merge-filter-sets values->tc-results tc-results->values) +;(provide (all-defined-out)) + +(define-syntax-rule (d/c/p (name . args) c . body) + (begin (d/c (name . args) c . body) + (p/c [name c]))) ;; this implements the sequence invariant described on the first page relating to Bot +#; (define (lcombine l1 l2) (cond [(memq (make-LBot) l1) (make-LFilterSet (list (make-LBot)) null)] @@ -21,31 +25,25 @@ [else (make-LFilterSet l1 l2)])) (define (combine l1 l2) - (cond [(memq (make-Bot) l1) - (make-FilterSet (list (make-Bot)) null)] - [(memq (make-Bot) l2) - (make-FilterSet null (list (make-Bot)))] - [else (make-FilterSet l1 l2)])) + (match* (l1 l2) + [(_ (Bot:)) (-FS -top -bot)] + [((Bot:) _) (-FS -bot -top)] + [(_ _) (-FS l1 l2)])) -(d/c (abstract-filters keys ids results) - ((listof index/c) (listof identifier?) tc-results? . -> . (or/c Values? ValuesDots?)) - (define (mk l [drest #f]) - (if drest (make-ValuesDots l (car drest) (cdr drest)) (make-Values l))) +(d/c/p (abstract-filters results) + (tc-results? . -> . (or/c Values? ValuesDots?)) (match results [(tc-results: ts fs os dty dbound) (make-ValuesDots - (for/list ([t ts] - [f fs] - [o os]) - (make-Result t (abstract-filter ids keys f) (abstract-object ids keys o))) + (for/list ([t ts] [f fs] [o os]) + (make-Result t f o)) dty dbound)] [(tc-results: ts fs os) (make-Values - (for/list ([t ts] - [f fs] - [o os]) - (make-Result t (abstract-filter ids keys f) (abstract-object ids keys o))))])) + (for/list ([t ts] [f fs] [o os]) + (make-Result t f o)))])) +#; (define/contract (abstract-object ids keys o) (-> (listof identifier?) (listof index/c) Object? LatentObject?) (define (lookup y) @@ -57,15 +55,17 @@ [(Path: p (lookup: idx)) (make-LPath p idx)] [_ (make-LEmpty)])) +#; (d/c (abstract-filter ids keys fs) (-> (listof identifier?) (listof index/c) FilterSet/c LatentFilterSet/c) (match fs [(FilterSet: f+ f-) - (lcombine + (combine (apply append (for/list ([f f+]) (abo ids keys f))) (apply append (for/list ([f f-]) (abo ids keys f))))] - [(NoFilter:) (lcombine null null)])) + [(NoFilter:) (combine -top -top)])) +#; (d/c (abo xs idxs f) ((listof identifier?) (listof index/c) Filter/c . -> . (or/c null? (list/c LatentFilter/c))) (define (lookup y) @@ -91,32 +91,116 @@ (define (merge-filter-sets fs) (match fs [(list (FilterSet: f+ f-) ...) - (make-FilterSet (remove-duplicates (apply append f+)) (remove-duplicates (apply append f-)))])) + (make-FilterSet (make-AndFilter f+) (make-AndFilter f-))])) -(d/c (apply-filter lfs t o) - (-> LatentFilterSet/c Type/c Object? FilterSet/c) - (match lfs - [(LFilterSet: lf+ lf-) - (combine - (apply append (for/list ([lf lf+]) (apo lf t o))) - (apply append (for/list ([lf lf-]) (apo lf t o))))])) +(d/c/p (apply-filter fs ids os [polarity #t]) + (->* (FilterSet/c (listof identifier?) (listof Object?)) (boolean?) FilterSet/c) + (match fs + [(FilterSet: f+ f-) + (combine (subst-filter* f+ ids os polarity) + (subst-filter* f- ids os polarity))])) -(d/c (apo lf s o) - (-> LatentFilter/c Type/c Object? (or/c '() (list/c Filter/c))) - (match* (lf s o) - [((ImpFilter: as cs) _ _) - (match* [(for/list ([a as]) (apo a s o)) - (for/list ([c cs]) (apo c s o))] - [((list (list a*) ...) - (list (list c*) ...)) (list (make-ImpFilter a* c*))] - [(_ _) null])] - [((LBot:) _ _) (list (make-Bot))] - [((LNotTypeFilter: (? (lambda (t) (subtype s t)) t) (list) _) _ _) (list (make-Bot))] - [((LTypeFilter: (? (lambda (t) (not (overlap s t))) t) (list) _) _ _) (list (make-Bot))] - [(_ _ (Empty:)) null] - [((LTypeFilter: t pi* _) _ (Path: pi x)) (list (make-TypeFilter t (append pi* pi) x))] - [((LNotTypeFilter: t pi* _) _ (Path: pi x)) (list (make-NotTypeFilter t (append pi* pi) x))])) +(d/c/p (apply-type t ids os [polarity #t]) + (->* (Type/c (listof identifier?) (listof Object?)) (boolean?) Type/c) + (for/fold ([t t]) ([i (in-list ids)] [o (in-list os)]) + (subst-type t i o polarity))) +(d/c/p (apply-object t ids os [polarity #t]) + (->* (Object? (listof identifier?) (listof Object?)) (boolean?) Object?) + (for/fold ([t t]) ([i (in-list ids)] [o (in-list os)]) + (subst-object t i o polarity))) + +(define (subst-filter* f ids os polarity) + (-> Filter/c (listof identifier?) (listof Object?) boolean? Filter/c) + (for/fold ([f f]) ([i (in-list ids)] [o (in-list os)]) + (subst-filter f i o polarity))) + +(d/c/p (subst-filter-set fs id o polarity) + (-> FilterSet? identifier? Object? boolean? FilterSet?) + (match fs + [(FilterSet: f+ f-) + (combine (subst-filter f+ id o polarity) + (subst-filter f- id o polarity))])) + +(define (subst-type t id o polarity) + (define (st t) (subst-type t id o polarity)) + (d/c (sf fs) (FilterSet? . -> . FilterSet?) (subst-filter-set fs id o polarity)) + (type-case (#:Type st + #:Filter sf + #:Object (lambda (f) (subst-object f id o polarity))) + t)) + +(define (subst-object t id o polarity) + (match t + [(NoObject:) t] + [(Empty:) t] + [(Path: p i) + (if (free-identifier=? i id) + (match o + [(Empty:) (make-Empty)] + ;; the result is not from an annotation, so it isn't a NoObject + [(NoObject:) (make-Empty)] + [(Path: p* i*) (make-Path (append p p*) i*)]) + t)])) + +;; this is the substitution metafunction +(d/c/p (subst-filter f id o polarity) + (-> Filter/c identifier? Object? boolean? Filter/c) + (define (ap f) (subst-filter f o polarity)) + (define (tf-matcher t p i id o polarity maker) + (match o + [(or (Empty:) (NoObject:)) (if polarity -top -bot)] + [(Path: p* i*) + (cond [(free-identifier=? i id) + (maker + (subst-type t id o polarity) + (append p p*) + i*)] + [(id-free-in? id t) (if polarity -top -bot)] + [else f])])) + (match f + [(ImpFilter: ant consq) + (make-ImpFilter (subst-filter ant id o (not polarity)) (ap consq))] + [(AndFilter: fs) (make-AndFilter (map ap fs))] + [(OrFilter: fs) (make-OrFilter (map ap fs))] + [(Bot:) -bot] + [(Top:) -top] + [(TypeFilter: t p i) + (tf-matcher t p i id o polarity make-TypeFilter)] + [(NotTypeFilter: t p i) + (tf-matcher t p i id o polarity make-NotTypeFilter)])) + +(define (id-free-in? id type) + (let/ec + return + (define (for-object o) + (object-case (#:Type for-type) + o + [#:Path p i + (if (free-identifier=? i id) + (return #t) + o)])) + (define (for-filter o) + (filter-case (#:Type for-type + #:Filter for-filter) + o + [#:NotTypeFilter t p i + (if (free-identifier=? i id) + (return #t) + o)] + [#:TypeFilter t p i + (if (free-identifier=? i id) + (return #t) + o)])) + (define (for-type t) + (type-case (#:Type for-type + #:Filter for-filter + #:Object for-object) + t)) + (for-type type))) + +#| +#; (define/contract (split-lfilters lf idx) (LatentFilterSet/c index/c . -> . LatentFilterSet/c) (define (idx= lf) @@ -133,6 +217,7 @@ (define-match-expander F-FS: (lambda (stx) #'(FilterSet: (list (Bot:)) _))) +#; (d/c (combine-filter f1 f2 f3 t2 t3 o2 o3) (FilterSet/c FilterSet/c FilterSet/c Type? Type? Object? Object? . -> . tc-results?) (define (mk f) (ret (Un t2 t3) f (make-Empty))) @@ -163,56 +248,28 @@ [(_ _ _) ;; could intersect f2 and f3 here (mk (make-FilterSet null null))])) +|# ;; (or/c Values? ValuesDots?) listof[identifier] -> tc-results? -(define (values->tc-results tc formals) +(d/c/p (values->tc-results tc) + ((or/c Values? ValuesDots?) . -> . tc-results?) (match tc - [(ValuesDots: (list (Result: ts lfs los) ...) dty dbound) - (ret ts - (for/list ([lf lfs]) - (or - (and (null? formals) - (match lf - [(LFilterSet: lf+ lf-) - (combine (if (memq (make-LBot) lf+) (list (make-Bot)) (list)) - (if (memq (make-LBot) lf-) (list (make-Bot)) (list)))])) - (merge-filter-sets - (for/list ([x formals] [i (in-naturals)]) - (apply-filter (split-lfilters lf i) Univ (make-Path null x)))))) - (for/list ([lo los]) - (or - (for/or ([x formals] [i (in-naturals)]) - (match lo - [(LEmpty:) #f] - [(LPath: p (== i)) (make-Path p x)])) - (make-Empty))) - dty dbound)] - [(Values: (list (Result: ts lfs los) ...)) - (ret ts - (for/list ([lf lfs]) - (or - (and (null? formals) - (match lf - [(LFilterSet: lf+ lf-) - (combine (if (memq (make-LBot) lf+) (list (make-Bot)) (list)) - (if (memq (make-LBot) lf-) (list (make-Bot)) (list)))])) - (merge-filter-sets - (for/list ([x formals] [i (in-naturals)]) - (apply-filter (split-lfilters lf i) Univ (make-Path null x)))))) - (for/list ([lo los]) - (or - (for/or ([x formals] [i (in-naturals)]) - (match lo - [(LEmpty:) #f] - [(LPath: p (== i)) (make-Path p x)])) - (make-Empty))))])) + [(ValuesDots: (list (Result: ts fs os) ...) dty dbound) + (ret ts fs os dty dbound)] + [(Values: (list (Result: ts fs os) ...)) + (ret ts fs os)])) (define (tc-results->values tc) (match tc [(tc-results: ts) (-values ts)])) +(provide combine-props tc-results->values subst-object subst-type) + (define (combine-props new-props old-props) - (define-values (new-imps new-atoms) (partition ImpFilter? new-props)) + (define-values (new-atoms new-formulas) + (partition (lambda (e) (or (TypeFilter? e) (NotTypeFilter? e))) new-props)) + (values new-formulas new-atoms) + #;#; (define-values (derived-imps derived-atoms) (for/fold ([derived-imps null] diff --git a/collects/typed-scheme/typecheck/tc-structs.ss b/collects/typed-scheme/typecheck/tc-structs.ss index 424cb02e..265ccd41 100644 --- a/collects/typed-scheme/typecheck/tc-structs.ss +++ b/collects/typed-scheme/typecheck/tc-structs.ss @@ -143,9 +143,7 @@ (for/list ([g (in-list getters)] [t (in-list external-fld-types/no-parent)] [i (in-naturals)]) (let ([func (if setters? (->* (list name) t) - (make-Function - (list (make-arr* (list name) t - #:object (make-LPath (list (make-StructPE name i)) 0)))))]) + (->acc (list name) t (list (make-StructPE name i))))]) (cons g (wrapper func)))) (if setters? (map (lambda (g t) (cons g (wrapper (->* (list name t) -Void)))) setters external-fld-types/no-parent) diff --git a/collects/typed-scheme/typed-scheme.ss b/collects/typed-scheme/typed-scheme.ss index 8e6aa08a..70c53def 100644 --- a/collects/typed-scheme/typed-scheme.ss +++ b/collects/typed-scheme/typed-scheme.ss @@ -42,7 +42,7 @@ [with-handlers ([(lambda (e) (and catch-errors? (exn:fail? e) (not (exn:fail:syntax? e)))) (lambda (e) (tc-error "Internal error: ~a" e))])] - [parameterize (;; disable fancy printing + [parameterize (;; enable fancy printing? [custom-printer #t] ;; a cheat to avoid units [infer-param infer] @@ -99,7 +99,9 @@ [(_ . form) (nest ([begin (set-box! typed-context? #t)] - [parameterize (;; a cheat to avoid units + [parameterize (;; disable fancy printing + [custom-printer #t] + ;; a cheat to avoid units [infer-param infer] ;; this paramter is for parsing types [current-tvars initial-tvar-env] diff --git a/collects/typed-scheme/types/abbrev.ss b/collects/typed-scheme/types/abbrev.ss index e30f9f12..c4c28ab4 100644 --- a/collects/typed-scheme/types/abbrev.ss +++ b/collects/typed-scheme/types/abbrev.ss @@ -9,6 +9,7 @@ scheme/match scheme/promise scheme/flonum + unstable/syntax (prefix-in c: scheme/contract) (for-syntax scheme/base syntax/parse) (for-template scheme/base scheme/contract scheme/promise scheme/tcp scheme/flonum)) @@ -26,8 +27,6 @@ (define -Param make-Param) (define -box make-Box) (define -vec make-Vector) -(define -LFS make-LFilterSet) -(define-syntax -FS (make-rename-transformer #'make-FilterSet)) (define-syntax *Un (syntax-rules () @@ -62,8 +61,8 @@ #'(app untuple (? values elem-pats))]))) -(d/c (-result t [f -no-lfilter] [o -no-lobj]) - (c:->* (Type/c) (LFilterSet? LatentObject?) Result?) +(d/c (-result t [f -no-filter] [o -no-obj]) + (c:->* (Type/c) (FilterSet? Object?) Result?) (make-Result t f o)) (d/c (-values args) @@ -115,11 +114,19 @@ (define -Pathlike* (*Un -String -Path (-val 'up) (-val 'same))) (define -Pattern (*Un -Bytes -Regexp -PRegexp -Byte-Regexp -Byte-PRegexp -String)) -(define -no-lfilter (make-LFilterSet null null)) -(define -no-filter (make-FilterSet null null)) -(define -no-lobj (make-LEmpty)) +(define -top (make-Top)) +(define -bot (make-Bot)) +(define -no-filter (make-FilterSet -top -top)) (define -no-obj (make-Empty)) + +(d/c (-FS + -) + (c:-> Filter/c Filter/c FilterSet?) + (match* (+ -) + [((Bot:) _) (make-FilterSet -bot -top)] + [(_ (Bot:)) (make-FilterSet -top -bot)] + [(+ -) (make-FilterSet + -)])) + (define -car (make-CarPE)) (define -cdr (make-CdrPE)) (define -syntax-e (make-SyntaxPE)) @@ -173,20 +180,26 @@ (define top-func (make-Function (list (make-top-arr)))) -(d/c (make-arr* dom rng +(d/c (make-arr* dom rng #:rest [rest #f] #:drest [drest #f] #:kws [kws null] - #:filters [filters -no-lfilter] #:object [obj -no-lobj]) + #:filters [filters -no-filter] #:object [obj -no-obj] + #:names [names (append + (generate-temporaries dom) + (if (or drest rest) (list (generate-temporary)) null) + (generate-temporaries kws))]) (c:->* ((listof Type/c) (or/c Values? ValuesDots? Type/c)) (#:rest (or/c #f Type/c) #:drest (or/c #f (cons/c Type/c symbol?)) #:kws (listof Keyword?) - #:filters LFilterSet? - #:object LatentObject?) + #:filters FilterSet? + #:object Object? + #:names (listof identifier?)) arr?) (make-arr dom (if (or (Values? rng) (ValuesDots? rng)) rng (make-Values (list (-result rng filters obj)))) - rest drest (sort #:key Keyword-kw kws keyword* stx) (define-syntax-class c @@ -228,10 +241,12 @@ (make-Function (list (make-arr* dom rng #:drest (cons dty 'dbound) #:filters filters)))])) (define (->acc dom rng path) + (define x (generate-temporary 'x)) (make-Function (list (make-arr* dom rng - #:filters (-LFS (list (-not-filter (-val #f) path)) - (list (-filter (-val #f) path))) - #:object (make-LPath path 0))))) + #:names (list x) + #:filters (-FS (-not-filter (-val #f) x path) + (-filter (-val #f) x path)) + #:object (make-Path path x))))) (define (cl->* . args) (define (funty-arities f) @@ -259,12 +274,70 @@ (define (-struct name parent flds accs [proc #f] [poly #f] [pred #'dummy] [cert values]) (make-Struct name parent flds proc poly pred cert accs)) -(define (-filter t [p null] [i 0]) - (make-LTypeFilter t p i)) +(d/c (-filter t i [p null]) + (c:->* (Type/c identifier?) ((listof PathElem?)) Filter/c) + (make-TypeFilter t p i)) -(define (-not-filter t [p null] [i 0]) - (make-LNotTypeFilter t p i)) +(define (-filter-at t o) + (match o + [(Path: p i) (-filter t i p)] + [_ -top])) +(define (-not-filter-at t o) + (match o + [(Path: p i) (-not-filter t i p)] + [_ -top])) +(define (opposite? f1 f2) + (match* (f1 f2) + [((TypeFilter: t1 p1 i1) + (NotTypeFilter: t2 p1 i2)) + (and (type-equal? t1 t2) + (free-identifier=? i1 i2))] + [((NotTypeFilter: t2 p1 i2) + (TypeFilter: t1 p1 i1)) + (and (type-equal? t1 t2) + (free-identifier=? i1 i2))] + [(_ _) #f])) + +(define (-or . args) + (let loop ([fs args] [result null]) + (if (null? fs) + (match result + [(list) -bot] + [(list f) f] + [(list f1 f2) (opposite? f1 f2) -top] + [_ (make-OrFilter result)]) + (match (car fs) + [(and t (Top:)) t] + [(OrFilter: fs*) (loop (cdr fs) (append fs* result))] + [(Bot:) (loop (cdr fs) result)] + [t (loop (cdr fs) (cons t result))])))) + +(define (-and . args) + (let loop ([fs args] [result null]) + (if (null? fs) + (match result + [(list) -top] + [(list f) f] + ;; don't think this is useful here + #;[(list f1 f2) (opposite? f1 f2) -bot] + [_ (make-AndFilter result)]) + (match (car fs) + [(and t (Bot:)) t] + [(AndFilter: fs*) (loop (cdr fs) (append fs* result))] + [(Top:) (loop (cdr fs) result)] + [t (loop (cdr fs) (cons t result))])))) + +(d/c (-not-filter t i [p null]) + (c:->* (Type/c identifier?) ((listof PathElem?)) Filter/c) + (make-NotTypeFilter t p i)) + +(define-syntax-rule (with-names (vars ...) . e) + (let-values ([(vars ...) (apply values (generate-temporaries '(vars ...)))]) + . e)) + +(define-syntax-rule (asym-pred (var) dom rng filter) + (with-names (var) (make-Function (list (make-arr* (list dom) rng #:names (list var) #:filters filter))))) (d/c make-pred-ty (case-> (c:-> Type/c Type/c) @@ -273,15 +346,22 @@ (c:-> (listof Type/c) Type/c Type/c integer? (listof PathElem?) Type/c)) (case-lambda [(in out t n p) - (->* in out : (-LFS (list (-filter t p n)) (list (-not-filter t p n))))] + (define xs (generate-temporaries in)) + (make-Function + (list + (make-arr* + in out + #:names xs + #:filters (-FS (-filter t (list-ref xs n) p) (-not-filter t (list-ref xs n) p)))))] [(in out t n) - (->* in out : (-LFS (list (-filter t null n)) (list (-not-filter t null n))))] + (make-pred-ty in out t n null)] [(in out t) - (make-pred-ty in out t 0)] - [(t) (make-pred-ty (list Univ) -Boolean t 0)])) + (make-pred-ty in out t 0 null)] + [(t) + (make-pred-ty (list Univ) -Boolean t 0 null)])) -(define true-filter (-FS (list) (list (make-Bot)))) -(define false-filter (-FS (list (make-Bot)) (list))) +(define true-filter (-FS -top -bot)) +(define false-filter (-FS -bot -top)) (define (opt-fn args opt-args result) (apply cl->* (for/list ([i (in-range (add1 (length opt-args)))]) diff --git a/collects/typed-scheme/types/printer.ss b/collects/typed-scheme/types/printer.ss index 2092712c..45eb107b 100644 --- a/collects/typed-scheme/types/printer.ss +++ b/collects/typed-scheme/types/printer.ss @@ -29,40 +29,20 @@ ns) #f)) -;; print out an effect -;; print-effect : Effect Port Boolean -> Void -(define (print-latentfilter c port write?) - (define (fp . args) (apply fprintf port args)) - (match c - [(LFilterSet: thn els) (fp "(") - (if (null? thn) - (fp "LTop") - (for ([i thn]) (fp "~a " i))) - (fp "|") - (if (null? els) - (fp "LTop") - (for ([i els]) (fp " ~a" i))) - (fp")")] - [(LNotTypeFilter: type path 0) (fp "(! ~a @ ~a)" type path)] - [(LTypeFilter: type path 0) (fp "(~a @ ~a)" type path)] - [(LNotTypeFilter: type path idx) (fp "(! ~a @ ~a ~a)" type path idx)] - [(LTypeFilter: type path idx) (fp "(~a @ ~a ~a)" type path idx)] - [(LBot:) (fp "LBot")] - [(LImpFilter: a c) (fp "(LImpFilter ~a ~a)" a c)] - [else (fp "(Unknown Latent Filter: ~a)" (struct->vector c))])) - (define (print-filter c port write?) (define (fp . args) (apply fprintf port args)) (match c - [(FilterSet: thn els) (fp "(") - (for ([i thn]) (fp "~a " i)) (fp "|") - (for ([i els]) (fp " ~a" i)) - (fp")")] + [(FilterSet: thn els) (fp "(~a | ~a)" thn els)] [(NoFilter:) (fp "-")] + [(NotTypeFilter: type (list) id) (fp "(! ~a @ ~a)" type (syntax-e id))] [(NotTypeFilter: type path id) (fp "(! ~a @ ~a ~a)" type path (syntax-e id))] + [(TypeFilter: type (list) id) (fp "(~a @ ~a)" type (syntax-e id))] [(TypeFilter: type path id) (fp "(~a @ ~a ~a)" type path (syntax-e id))] [(Bot:) (fp "Bot")] + [(Top:) (fp "Top")] [(ImpFilter: a c) (fp "(ImpFilter ~a ~a)" a c)] + [(AndFilter: a) (fp "(AndFilter") (for ([a0 a]) (fp " ~a" a0)) (fp ")")] + [(OrFilter: a) (fp "(OrFilter") (for ([a0 a]) (fp " ~a" a0)) (fp ")")] [else (fp "(Unknown Filter: ~a)" (struct->vector c))])) (define (print-pathelem c port write?) @@ -73,12 +53,6 @@ [(StructPE: t i) (fp "(~a ~a)" t i)] [else (fp "(Unknown Path Element: ~a)" (struct->vector c))])) -(define (print-latentobject c port write?) - (define (fp . args) (apply fprintf port args)) - (match c - [(LEmpty:) (fp "")] - [(LPath: pes i) (fp "~a" (append pes (list i)))])) - (define (print-object c port write?) (define (fp . args) (apply fprintf port args)) (match c @@ -114,17 +88,17 @@ (fp "~a ...~a~a " (car drest) (if (special-dots-printing?) "" " ") (cdr drest))) (match rng - [(Values: (list (Result: t (LFilterSet: (list) (list)) (LEmpty:)))) + [(Values: (list (Result: t (FilterSet: (Top:) (Top:)) (Empty:)))) (fp "-> ~a" t)] [(Values: (list (Result: t - (LFilterSet: (list (LTypeFilter: ft pth 0)) - (list (LNotTypeFilter: ft pth 0))) - (LEmpty:)))) + (FilterSet: (TypeFilter: ft pth id) + (NotTypeFilter: ft pth id)) + (Empty:)))) (if (null? pth) (fp "-> ~a : ~a" t ft) (begin (fp "-> ~a : ~a @" t ft) (for ([pe pth]) (fp " ~a" pe))))] - [(Values: (list (Result: t fs (LEmpty:)))) + [(Values: (list (Result: t fs (Empty:)))) (fp/filter "-> ~a : ~a" t fs)] [(Values: (list (Result: t lf lo))) (fp/filter "-> ~a : ~a ~a" t lf lo)] @@ -141,11 +115,16 @@ (match t [(Pair: a e) (cons a (tuple-elems e))] [(Value: '()) null])) - (match c + (match c + ;; if we know how it was written, print that + [(? Rep-stx a) + (fp "~a" (syntax->datum (Rep-stx a)))] [(Univ:) (fp "Any")] ;; special case number until something better happens ;;[(Base: 'Number _) (fp "Number")] - [(? has-name?) (fp "~a" (has-name? c))] + [(? has-name?) + #;(printf "has a name\n") + (fp "~a" (has-name? c))] [(StructTop: st) (fp "~a" st)] [(BoxTop:) (fp "Box")] [(VectorTop:) (fp "Vector")] @@ -183,7 +162,7 @@ (lambda (e) (fp " ") (print-arr e)) b) (fp ")")]))] - [(arr: _ _ _ _ _) (print-arr c)] + [(arr: _ _ _ _ _) (fp "(arr ") (print-arr c) (fp ")")] [(Vector: e) (fp "(Vectorof ~a)" e)] [(Box: e) (fp "(Boxof ~a)" e)] [(Union: elems) (fp "~a" (cons 'U elems))] @@ -227,8 +206,8 @@ [(Syntax: t) (fp "(Syntaxof ~a)" t)] [(Instance: t) (fp "(Instance ~a)" t)] [(Class: pf nf ms) (fp "(Class)")] - [(Result: t (LFilterSet: (list) (list)) (LEmpty:)) (fp "~a" t)] - [(Result: t fs (LEmpty:)) (fp "(~a : ~a)" t fs)] + [(Result: t (FilterSet: (Top:) (Top:)) (Empty:)) (fp "~a" t)] + [(Result: t fs (Empty:)) (fp "(~a : ~a)" t fs)] [(Result: t fs lo) (fp "(~a : ~a : ~a)" t fs lo)] [(Refinement: parent p? _) (fp "(Refinement ~a ~a)" parent (syntax-e p?))] @@ -238,7 +217,7 @@ (set-box! print-type* print-type) (set-box! print-filter* print-filter) -(set-box! print-latentfilter* print-latentfilter) +;(set-box! print-latentfilter* print-latentfilter) (set-box! print-object* print-object) -(set-box! print-latentobject* print-latentobject) +;(set-box! print-latentobject* print-latentobject) (set-box! print-pathelem* print-pathelem) diff --git a/collects/typed-scheme/types/subtype.ss b/collects/typed-scheme/types/subtype.ss index 582eb26e..2916c993 100644 --- a/collects/typed-scheme/types/subtype.ss +++ b/collects/typed-scheme/types/subtype.ss @@ -184,14 +184,12 @@ (d/c (combine-arrs arrs) (c-> (listof arr?) (or/c #f arr?)) (match arrs - [(list (arr: dom1 rng1 #f #f '()) (arr: dom rng #f #f '()) ...) + [(list (and a1 (arr: dom1 rng1 #f #f '() names)) (arr: dom rng #f #f '()) ...) (cond - [(null? dom) (make-arr dom1 rng1 #f #f '())] - ((not (apply = (length dom1) (map length dom))) - #f) - ((not (foldl type-equal? rng1 rng)) - #f) - [else (make-arr (apply map (lambda args (make-Union (sort args type Void)]))) (dt Color% (Class () () ([red (-> Number)]))) -(dt Snip% (Class () () ())) +(dt Snip% (Class () () ([get-count (-> Integer)]))) (dt Text% (Class () ()