From 707dae25cac56dbc1620abfc5da10ba412030568 Mon Sep 17 00:00:00 2001 From: Noel Welsh Date: Tue, 30 Mar 2010 13:33:45 +0000 Subject: [PATCH 1/6] Add type definition for unsafe-vector*-ref and unsafe-vector*-length, which have recently been introduced, and a test case for in-vector (which uses the above). svn: r18667 original commit: cfab7a8d97c62814973a8b0e74089233873a896e --- collects/tests/typed-scheme/succeed/sequences.ss | 1 + collects/typed-scheme/private/base-env.ss | 2 ++ 2 files changed, 3 insertions(+) diff --git a/collects/tests/typed-scheme/succeed/sequences.ss b/collects/tests/typed-scheme/succeed/sequences.ss index c584ad85..00a162ef 100644 --- a/collects/tests/typed-scheme/succeed/sequences.ss +++ b/collects/tests/typed-scheme/succeed/sequences.ss @@ -7,3 +7,4 @@ (ann (for ([z (open-input-string "foobar")]) (add1 z)) Void) (ann (for ([z (in-list (list 1 2 3))]) (add1 z)) Void) +(ann (for ([z (in-vector (vector 1 2 3))]) (add1 z)) Void) \ No newline at end of file diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss index 0c2b5c9d..959ea1fb 100644 --- a/collects/typed-scheme/private/base-env.ss +++ b/collects/typed-scheme/private/base-env.ss @@ -651,7 +651,9 @@ ;; unsafe [unsafe-vector-ref (-poly (a) ((-vec a) -Nat . -> . a))] +[unsafe-vector*-ref (-poly (a) ((-vec a) -Nat . -> . a))] [unsafe-vector-length (-poly (a) ((-vec a) . -> . -Nat))] +[unsafe-vector*-length (-poly (a) ((-vec a) . -> . -Nat))] [unsafe-car (-poly (a b) (cl->* (->acc (list (-pair a b)) a (list -car))))] From e1c724381be3f118b38f2bfa3987598c33d3152e Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Thu, 8 Apr 2010 20:11:39 +0000 Subject: [PATCH 2/6] fix doc bugs reported by danny svn: r18765 original commit: 24ad4005e802bca01e540f38aa6ea49fe7c3cfb6 --- collects/typed-scheme/scribblings/begin.scrbl | 10 +++++----- collects/typed-scheme/scribblings/quick.scrbl | 6 +++--- 2 files changed, 8 insertions(+), 8 deletions(-) diff --git a/collects/typed-scheme/scribblings/begin.scrbl b/collects/typed-scheme/scribblings/begin.scrbl index 61a32344..011f28aa 100644 --- a/collects/typed-scheme/scribblings/begin.scrbl +++ b/collects/typed-scheme/scribblings/begin.scrbl @@ -36,22 +36,22 @@ form from @schememodname[scheme]---when porting a program from @schememodname[scheme] to @schememodname[typed/scheme], uses of @scheme[define-struct] should be changed to @scheme[define-struct:]. -@schemeblock[(: mag (pt -> Real))] +@schemeblock[(: mag (pt -> Number))] -This declares that @scheme[mag] has the type @scheme[(pt -> Real)]. +This declares that @scheme[mag] has the type @scheme[(pt -> Number)]. @;{@scheme[mag] must be defined at the top-level of the module containing the declaration.} -The type @scheme[(pt -> Real)] is a function type, that is, the type +The type @scheme[(pt -> Number)] is a function type, that is, the type of a procedure. The input type, or domain, is a single argument of type @scheme[pt], which refers to an instance of the @scheme[pt] structure. The @scheme[->] both indicates that this is a function type and separates the domain from the range, or output type, in this -case @scheme[Real]. +case @scheme[Number]. @schemeblock[ (define (mag p) - (sqrt (sqr (pt-x p)) (sqr (pt-y p)))) + (sqrt (+ (sqr (pt-x p)) (sqr (pt-y p))))) ] This definition is unchanged from the untyped version of the code. diff --git a/collects/typed-scheme/scribblings/quick.scrbl b/collects/typed-scheme/scribblings/quick.scrbl index a46bcc31..b0b7c25c 100644 --- a/collects/typed-scheme/scribblings/quick.scrbl +++ b/collects/typed-scheme/scribblings/quick.scrbl @@ -28,9 +28,9 @@ language: typed/scheme (define-struct: pt ([x : Real] [y : Real])) -(: mag (pt -> Real)) +(: mag (pt -> Number)) (define (mag p) - (sqrt (sqr (pt-x p)) (sqr (pt-y p)))) + (sqrt (+ (sqr (pt-x p)) (sqr (pt-y p))))) ] ) @@ -40,7 +40,7 @@ scheme (code:contract mag : pt -> number) (define (mag p) - (sqrt (sqr (pt-x p)) (sqr (pt-y p)))) + (sqrt (+ (sqr (pt-x p)) (sqr (pt-y p))))) ] Here is the same program, in @schememodname[typed/scheme]: From f07551ef24753d4abd21f3e73d48aaea9ce0aaeb Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Fri, 9 Apr 2010 20:06:53 +0000 Subject: [PATCH 3/6] Enable proper reader and repl config for typed/scheme svn: r18773 original commit: 0b55e34853ab9a4483703148aa522acaa532f698 --- collects/typed-scheme/module-info.ss | 18 ++++++++++++++++++ collects/typed-scheme/typed-reader.ss | 2 +- collects/typed/scheme/base/lang/reader.ss | 10 ++++++++++ collects/typed/scheme/lang/reader.ss | 10 ++++++++++ 4 files changed, 39 insertions(+), 1 deletion(-) create mode 100644 collects/typed-scheme/module-info.ss diff --git a/collects/typed-scheme/module-info.ss b/collects/typed-scheme/module-info.ss new file mode 100644 index 00000000..864540fe --- /dev/null +++ b/collects/typed-scheme/module-info.ss @@ -0,0 +1,18 @@ +#lang scheme/base +(require typed-scheme/typed-reader) +(provide module-info configure) + +(define ((module-info arg) key default) + (case key + [(configure-runtime) `(#(typed-scheme/module-info configure ()))] + [else default])) + +;; options currently always empty +(define (configure options) + (namespace-require 'scheme/base) + (eval '(begin + (require (for-syntax typed-scheme/utils/tc-utils scheme/base)) + (begin-for-syntax (set-box! typed-context? #t))) + (current-namespace)) + (current-readtable readtable)) + diff --git a/collects/typed-scheme/typed-reader.ss b/collects/typed-scheme/typed-reader.ss index ebce7135..3313c542 100644 --- a/collects/typed-scheme/typed-reader.ss +++ b/collects/typed-scheme/typed-reader.ss @@ -83,4 +83,4 @@ (parameterize ([current-readtable readtable]) (read-syntax src port))) -(provide (rename-out [*read read] [*read-syntax read-syntax])) +(provide readtable (rename-out [*read read] [*read-syntax read-syntax])) diff --git a/collects/typed/scheme/base/lang/reader.ss b/collects/typed/scheme/base/lang/reader.ss index f276a7b4..ce8f8d0f 100644 --- a/collects/typed/scheme/base/lang/reader.ss +++ b/collects/typed/scheme/base/lang/reader.ss @@ -4,5 +4,15 @@ typed/scheme/base #:read r:read #:read-syntax r:read-syntax +#:info make-info +#:module-info make-module-info + +(define (make-info key default use-default) + (case key + [else (use-default key default)])) + +(define make-module-info + `#(typed-scheme/module-info module-info ())) + (require (prefix-in r: typed-scheme/typed-reader)) diff --git a/collects/typed/scheme/lang/reader.ss b/collects/typed/scheme/lang/reader.ss index e5397c57..3a91f1a7 100644 --- a/collects/typed/scheme/lang/reader.ss +++ b/collects/typed/scheme/lang/reader.ss @@ -4,5 +4,15 @@ typed/scheme #:read r:read #:read-syntax r:read-syntax +#:info make-info +#:module-info make-module-info + +(define (make-info key default use-default) + (case key + [else (use-default key default)])) + +(define make-module-info + `#(typed-scheme/module-info module-info ())) + (require (prefix-in r: typed-scheme/typed-reader)) From 063e588872c9469256f6a114e54f2cdbc0ff64a5 Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Mon, 12 Apr 2010 22:23:39 +0000 Subject: [PATCH 4/6] Fix thinko in subtyping. svn: r18802 original commit: 25a817e4aa7a74f3148b56ffb9f627ee4f0329f3 --- .../tests/typed-scheme/fail/with-type-bug.ss | 5 +++ collects/typed-scheme/types/subtype.ss | 32 +++++++++---------- 2 files changed, 21 insertions(+), 16 deletions(-) create mode 100644 collects/tests/typed-scheme/fail/with-type-bug.ss diff --git a/collects/tests/typed-scheme/fail/with-type-bug.ss b/collects/tests/typed-scheme/fail/with-type-bug.ss new file mode 100644 index 00000000..0fcb77db --- /dev/null +++ b/collects/tests/typed-scheme/fail/with-type-bug.ss @@ -0,0 +1,5 @@ +#; +(exn-pred exn:fail:contract?) +#lang scheme +(require (prefix-in T: typed/scheme)) +((T:with-type #:result (T:Integer T:-> T:Integer) add1) 1/2) diff --git a/collects/typed-scheme/types/subtype.ss b/collects/typed-scheme/types/subtype.ss index 582eb26e..7b1e5a52 100644 --- a/collects/typed-scheme/types/subtype.ss +++ b/collects/typed-scheme/types/subtype.ss @@ -5,7 +5,7 @@ (types utils comparison resolve abbrev) (env type-name-env) (only-in (infer infer-dummy) unify) - scheme/match unstable/match unstable/debug + scheme/match unstable/match mzlib/trace (rename-in scheme/contract [-> c->] [->* c->*]) @@ -186,12 +186,11 @@ (match arrs [(list (arr: dom1 rng1 #f #f '()) (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 unmatch) (if (equal? v1 v2) A0 (unmatch))] ;; now we encode the numeric hierarchy - bletch [((Base: 'Integer _) (Base: 'Number _)) A0] - [((Base: 'Flonum _) (== -Real type-equal?)) A0] - [((Base: 'Integer _) (== -Real type-equal?)) A0] + [((Base: 'Flonum _) (== -Real =t)) A0] + [((Base: 'Integer _) (== -Real =t)) A0] [((Base: 'Flonum _) (Base: 'Number _)) A0] [((Base: 'Exact-Rational _) (Base: 'Number _)) A0] [((Base: 'Integer _) (Base: 'Exact-Rational _)) A0] [((Base: 'Exact-Positive-Integer _) (Base: 'Exact-Rational _)) A0] [((Base: 'Exact-Positive-Integer _) (Base: 'Number _)) A0] - [((Base: 'Exact-Positive-Integer _) (== -Nat type-equal?)) A0] + [((Base: 'Exact-Positive-Integer _) (== -Nat =t)) A0] [((Base: 'Exact-Positive-Integer _) (Base: 'Integer _)) A0] - [((== -Nat type-equal?) (Base: 'Number _)) A0] - [((== -Nat type-equal?) (Base: 'Exact-Rational _)) A0] - [((== -Nat type-equal?) (Base: 'Integer _)) A0] + [((== -Nat =t) (Base: 'Number _)) A0] + [((== -Nat =t) (Base: 'Exact-Rational _)) A0] + [((== -Nat =t) (Base: 'Integer _)) A0] ;; values are subtypes of their "type" [((Value: (? exact-integer? n)) (Base: 'Integer _)) A0] [((Value: (and n (? number?) (? exact?) (? rational?))) (Base: 'Exact-Rational _)) A0] - [((Value: (? exact-nonnegative-integer? n)) (== -Nat type-equal?)) A0] + [((Value: (? exact-nonnegative-integer? n)) (== -Nat =t)) A0] [((Value: (? exact-positive-integer? n)) (Base: 'Exact-Positive-Integer _)) A0] [((Value: (? inexact-real? n)) (Base: 'Flonum _)) A0] - [((Value: (? real? n)) (== -Real type-equal?)) A0] + [((Value: (? real? n)) (== -Real =t)) A0] [((Value: (? number? n)) (Base: 'Number _)) A0] [((Value: (? keyword?)) (Base: 'Keyword _)) A0] From ce7df534552d83e95e1a242c064b1d0e635f9b8f Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Wed, 14 Apr 2010 17:11:21 +0000 Subject: [PATCH 5/6] test improvements svn: r18814 original commit: 0c730ae50a4b60a982c0a1e6fee24875f2c630a1 --- .../unit-tests/typecheck-tests.ss | 31 ++++++++++--------- collects/typed-scheme/types/abbrev.ss | 2 ++ 2 files changed, 19 insertions(+), 14 deletions(-) diff --git a/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss b/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss index 6601529e..65791fcf 100644 --- a/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss +++ b/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss @@ -9,8 +9,10 @@ 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-lfilter -true-lfilter] + [true-filter -true-filter] [-> t:->]) (utils tc-utils utils) unstable/mutated-vars @@ -137,11 +139,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-lfilter)] + [tc-e/t (lambda: ([x : Number]) 3) (t:-> N -Pos : -true-lfilter)] + [tc-e/t (lambda: ([x : Number] [y : Boolean]) 3) (t:-> N B -Pos : -true-lfilter)] + [tc-e/t (lambda () 3) (t:-> -Pos : -true-lfilter)] + [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] @@ -478,11 +480,12 @@ [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-lfilter)] [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 +493,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-lfilter)] [tc-e/t (let* ([z 1] [p? (lambda: ([x : Any]) z)]) (lambda: ([x : Any]) (if (p? x) x 12))) @@ -657,7 +660,7 @@ ;; 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-lfilter)] [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) @@ -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-lfilter))] [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-lfilter))] [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/types/abbrev.ss b/collects/typed-scheme/types/abbrev.ss index e30f9f12..5fb3610b 100644 --- a/collects/typed-scheme/types/abbrev.ss +++ b/collects/typed-scheme/types/abbrev.ss @@ -282,6 +282,8 @@ (define true-filter (-FS (list) (list (make-Bot)))) (define false-filter (-FS (list (make-Bot)) (list))) +(define true-lfilter (-LFS (list) (list (make-LBot)))) +(define false-lfilter (-LFS (list (make-LBot)) (list))) (define (opt-fn args opt-args result) (apply cl->* (for/list ([i (in-range (add1 (length opt-args)))]) From 6890aab1758c3aa9304160899cdfbada1beada17 Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Wed, 14 Apr 2010 15:06:14 -0400 Subject: [PATCH 6/6] Update structure types to have constructor ids. Use constructor to generate better contracts for poly structs. original commit: 41e469d7aefd9aab480594caaba62dd7019ec0fd --- .../succeed/provide-poly-struct.ss | 12 ++++++ .../typed-scheme/unit-tests/subtype-tests.ss | 9 +++-- .../unit-tests/type-equal-tests.ss | 8 +++- collects/typed-scheme/env/init-envs.ss | 11 +++--- collects/typed-scheme/infer/infer-unit.ss | 2 +- .../typed-scheme/private/type-contract.ss | 38 +++++++++++-------- collects/typed-scheme/rep/type-rep.ss | 22 ++++++++--- collects/typed-scheme/typecheck/tc-app.ss | 2 +- collects/typed-scheme/typecheck/tc-envops.ss | 13 ++++--- collects/typed-scheme/typecheck/tc-structs.ss | 4 +- collects/typed-scheme/types/abbrev.ss | 6 +-- collects/typed-scheme/types/printer.ss | 4 +- .../typed-scheme/types/remove-intersect.ss | 16 ++++---- collects/typed-scheme/types/subtype.ss | 10 ++--- 14 files changed, 99 insertions(+), 58 deletions(-) create mode 100644 collects/tests/typed-scheme/succeed/provide-poly-struct.ss diff --git a/collects/tests/typed-scheme/succeed/provide-poly-struct.ss b/collects/tests/typed-scheme/succeed/provide-poly-struct.ss new file mode 100644 index 00000000..3fc0efad --- /dev/null +++ b/collects/tests/typed-scheme/succeed/provide-poly-struct.ss @@ -0,0 +1,12 @@ +#lang scheme/load + +(module m typed-scheme + (define-struct: (A) x ([v : A])) + (provide make-x x-v)) + +(module n scheme + (require 'm) + (x-v (make-x 1))) + +(require 'm) +(require 'n) diff --git a/collects/tests/typed-scheme/unit-tests/subtype-tests.ss b/collects/tests/typed-scheme/unit-tests/subtype-tests.ss index f8962ec0..c6f68f75 100644 --- a/collects/tests/typed-scheme/unit-tests/subtype-tests.ss +++ b/collects/tests/typed-scheme/unit-tests/subtype-tests.ss @@ -112,10 +112,11 @@ [(-values (list -Number)) (-values (list Univ))] - [(-poly (a) ((Un (make-Base 'foo #'dummy) (-struct 'bar #f (list -Number a) null)) . -> . (-lst a))) - ((Un (make-Base 'foo #'dummy) (-struct 'bar #f (list -Number (-pair -Number (-v a))) null)) . -> . (-lst (-pair -Number (-v a))))] - [(-poly (a) ((-struct 'bar #f (list -Number a) null) . -> . (-lst a))) - ((-struct 'bar #f (list -Number (-pair -Number (-v a))) null) . -> . (-lst (-pair -Number (-v a))))] + [(-poly (a) ((Un (make-Base 'foo #'dummy) (-struct 'bar #f (list -Number a) null #'values)) . -> . (-lst a))) + ((Un (make-Base 'foo #'dummy) (-struct 'bar #f (list -Number (-pair -Number (-v a))) null #'values)) + . -> . (-lst (-pair -Number (-v a))))] + [(-poly (a) ((-struct 'bar #f (list -Number a) null #'values) . -> . (-lst a))) + ((-struct 'bar #f (list -Number (-pair -Number (-v a))) null #'values) . -> . (-lst (-pair -Number (-v a))))] [(-poly (a) (a . -> . (make-Listof a))) ((-v b) . -> . (make-Listof (-v b)))] [(-poly (a) (a . -> . (make-Listof a))) ((-pair -Number (-v b)) . -> . (make-Listof (-pair -Number (-v b))))] diff --git a/collects/tests/typed-scheme/unit-tests/type-equal-tests.ss b/collects/tests/typed-scheme/unit-tests/type-equal-tests.ss index e49e57cf..43022800 100644 --- a/collects/tests/typed-scheme/unit-tests/type-equal-tests.ss +++ b/collects/tests/typed-scheme/unit-tests/type-equal-tests.ss @@ -37,10 +37,14 @@ [(-mu x (Un -Number -Symbol x)) (-mu y (Un -Number -Symbol y))] ;; found bug [FAIL (Un (-mu heap-node - (-struct 'heap-node #f (list (-base 'comparator) -Number (-v a) (Un heap-node (-base 'heap-empty))) null)) + (-struct 'heap-node #f + (list (-base 'comparator) -Number (-v a) (Un heap-node (-base 'heap-empty))) + null #'values)) (-base 'heap-empty)) (Un (-mu heap-node - (-struct 'heap-node #f (list (-base 'comparator) -Number (-pair -Number -Number) (Un heap-node (-base 'heap-empty))) null)) + (-struct 'heap-node #f + (list (-base 'comparator) -Number (-pair -Number -Number) (Un heap-node (-base 'heap-empty))) + null #'values)) (-base 'heap-empty))])) (define-go diff --git a/collects/typed-scheme/env/init-envs.ss b/collects/typed-scheme/env/init-envs.ss index 472524a4..c5e10464 100644 --- a/collects/typed-scheme/env/init-envs.ss +++ b/collects/typed-scheme/env/init-envs.ss @@ -1,10 +1,10 @@ #lang scheme/base (provide (all-defined-out)) -(require "../utils/utils.ss") - -(require "type-env.ss" +(require "../utils/utils.ss" + "type-env.ss" "type-name-env.ss" "type-alias-env.ss" + unstable/struct (rep type-rep object-rep filter-rep rep-utils) (for-template (rep type-rep object-rep filter-rep) (types union) @@ -25,11 +25,12 @@ [(Union: elems) `(make-Union (sort (list ,@(map sub elems)) < #:key Type-seq))] [(Base: n cnt) `(make-Base ',n (quote-syntax ,cnt))] [(Name: stx) `(make-Name (quote-syntax ,stx))] - [(Struct: name parent flds proc poly? pred-id cert acc-ids) + [(Struct: name parent flds proc poly? pred-id cert acc-ids maker-id) `(make-Struct ,(sub name) ,(sub parent) ,(sub flds) ,(sub proc) ,(sub poly?) (quote-syntax ,pred-id) (syntax-local-certifier) - (list ,@(for/list ([a acc-ids]) `(quote-syntax ,a))))] + (list ,@(for/list ([a acc-ids]) `(quote-syntax ,a))) + (quote-syntax ,maker-id))] [(App: rator rands stx) `(make-App ,(sub rator) ,(sub rands) (quote-syntax ,stx))] [(Opaque: pred cert) `(make-Opaque (quote-syntax ,pred) (syntax-local-certifier))] [(Refinement: parent pred cert) `(make-Refinement ,(sub parent) diff --git a/collects/typed-scheme/infer/infer-unit.ss b/collects/typed-scheme/infer/infer-unit.ss index 0980881a..82a8f823 100644 --- a/collects/typed-scheme/infer/infer-unit.ss +++ b/collects/typed-scheme/infer/infer-unit.ss @@ -322,7 +322,7 @@ (cg S e))) (fail! S T))] - [((Struct: nm p flds proc _ _ _ _) (Struct: nm p flds* proc* _ _ _ _)) + [((Struct: nm p flds proc _ _ _ _ _) (Struct: nm p flds* proc* _ _ _ _ _)) (let-values ([(flds flds*) (cond [(and proc proc*) (values (cons proc flds) (cons proc* flds*))] diff --git a/collects/typed-scheme/private/type-contract.ss b/collects/typed-scheme/private/type-contract.ss index a1d4ae6e..8bc39839 100644 --- a/collects/typed-scheme/private/type-contract.ss +++ b/collects/typed-scheme/private/type-contract.ss @@ -160,25 +160,33 @@ #;#'class? #'(class/c (name fcn-cnt) ... (init [by-name-init by-name-cnt] ...)))] [(Value: '()) #'null?] - [(Struct: nm par flds proc poly? pred? cert acc-ids) + [(Struct: nm par flds proc poly? pred? cert acc-ids maker-id) (cond [(assf (λ (t) (type-equal? t ty)) structs-seen) => - (lambda (pr) - (cdr pr))] + cdr] [proc (exit (fail))] - [poly? - (with-syntax* ([(x rec) (generate-temporaries '(x rec))] - [(fld-cnts ...) - (for/list ([fty flds] - [f-acc acc-ids]) - #`(#,(t->c fty #:seen (cons (cons ty #'rec) structs-seen)) - (#,f-acc x)))]) - #`(flat-rec-contract - rec - '#,(syntax-e pred?) - (lambda (x) (and fld-cnts ...))))] - [else #`(flat-named-contract '#,(syntax-e pred?) #,(cert pred?))])] + [poly? + (with-syntax* ([(rec blame val) (generate-temporaries '(rec blame val))] + [maker maker-id] + [cnt-name nm] + [(fld-cnts ...) + (for/list ([fty flds] + [f-acc acc-ids]) + #`(((contract-projection + #,(t->c fty #:seen (cons (cons ty #'(recursive-contract rec)) structs-seen))) + blame) + (#,f-acc val)))]) + #`(letrec ([rec + (make-contract + #:name 'cnt-name + #:first-order #,pred? + #:projection + (lambda (blame) + (lambda (val) + (maker fld-cnts ...))))]) + rec))] + [else #`(flat-named-contract '#,(syntax-e pred?) #,(cert pred?))])] [(Syntax: (Base: 'Symbol _)) #'identifier?] [(Syntax: t) #`(syntax/c #,(t->c t))] [(Value: v) #`(flat-named-contract #,(format "~a" v) (lambda (x) (equal? x '#,v)))] diff --git a/collects/typed-scheme/rep/type-rep.ss b/collects/typed-scheme/rep/type-rep.ss index fe192c15..3372f3fe 100644 --- a/collects/typed-scheme/rep/type-rep.ss +++ b/collects/typed-scheme/rep/type-rep.ss @@ -196,7 +196,7 @@ ;; name : symbol ;; parent : Struct -;; flds : Listof[Type] +;; flds : Listof[Cons[Type,Bool]] type and mutability ;; proc : Function Type ;; poly? : is this a polymorphic type? ;; pred-id : identifier for the predicate of the struct @@ -204,22 +204,34 @@ (dt Struct ([name symbol?] [parent (or/c #f Struct? Name?)] [flds (listof Type/c)] + #; + [flds (listof (cons/c Type/c boolean?))] [proc (or/c #f Function?)] [poly? boolean?] [pred-id identifier?] [cert procedure?] - [acc-ids (listof identifier?)]) + [acc-ids (listof identifier?)] + [maker-id identifier?]) [#:intern (list name parent flds proc)] - [#:frees (combine-frees (map free-vars* (append (if proc (list proc) null) (if parent (list parent) null) flds))) - (combine-frees (map free-idxs* (append (if proc (list proc) null) (if parent (list parent) null) flds)))] + [#:frees (combine-frees (map free-vars* (append (if proc (list proc) null) + (if parent (list parent) null) + + flds #;(map car flds)))) + (combine-frees (map free-idxs* (append (if proc (list proc) null) + (if parent (list parent) null) + flds #;(map car flds))))] [#:fold-rhs (*Struct name (and parent (type-rec-id parent)) (map type-rec-id flds) + #; + (for/list ([(t m?) (in-pairs (in-list flds))]) + (cons (type-rec-id t) m?)) (and proc (type-rec-id proc)) poly? pred-id cert - acc-ids)] + acc-ids + maker-id)] [#:key #f]) ;; A structure type descriptor diff --git a/collects/typed-scheme/typecheck/tc-app.ss b/collects/typed-scheme/typecheck/tc-app.ss index 9bc405ca..75c04c36 100644 --- a/collects/typed-scheme/typecheck/tc-app.ss +++ b/collects/typed-scheme/typecheck/tc-app.ss @@ -708,7 +708,7 @@ (lambda (dom rng rest a) (infer/vararg vars argtys-t dom rest rng (fv rng) (and expected (tc-results->values expected)))) t argtys expected)] ;; procedural structs - [((tc-result1: (and sty (Struct: _ _ _ (? Function? proc-ty) _ _ _ _))) _) + [((tc-result1: (and sty (Struct: _ _ _ (? Function? proc-ty) _ _ _ _ _))) _) (tc/funapp f-stx #`(#,(syntax/loc f-stx dummy) . #,args-stx) (ret proc-ty) (cons ftype0 argtys) expected)] ;; parameters are functions too [((tc-result1: (Param: in out)) (list)) (ret out)] diff --git a/collects/typed-scheme/typecheck/tc-envops.ss b/collects/typed-scheme/typecheck/tc-envops.ss index c009e869..1be93033 100644 --- a/collects/typed-scheme/typecheck/tc-envops.ss +++ b/collects/typed-scheme/typecheck/tc-envops.ss @@ -11,7 +11,7 @@ (types resolve) (only-in (env type-environments lexical-env) env? update-type/lexical env-map env-props replace-props) scheme/contract scheme/match - mzlib/trace unstable/debug + mzlib/trace unstable/debug unstable/struct (typecheck tc-metafunctions) (for-syntax scheme/base)) @@ -44,12 +44,15 @@ (make-Syntax (update t (make-NotTypeFilter u rst x)))] ;; struct ops - [((Struct: nm par flds proc poly pred cert acc-ids) + [((Struct: nm par flds proc poly pred cert acc-ids maker-id) (TypeFilter: u (list rst ... (StructPE: (? (lambda (s) (subtype t s)) s) idx)) x)) - (make-Struct nm par (replace-nth flds idx (lambda (e) (update e (make-TypeFilter u rst x)))) proc poly pred cert acc-ids)] - [((Struct: nm par flds proc poly pred cert acc-ids) + (make-Struct nm par + (replace-nth flds idx + (lambda (e) (update e (make-TypeFilter u rst x)))) + proc poly pred cert acc-ids maker-id)] + [((Struct: nm par flds proc poly pred cert acc-ids maker-id) (NotTypeFilter: u (list rst ... (StructPE: (? (lambda (s) (subtype t s)) s) idx)) x)) - (make-Struct nm par (replace-nth flds idx (lambda (e) (update e (make-NotTypeFilter u rst x)))) proc poly pred cert acc-ids)] + (make-Struct nm par (replace-nth flds idx (lambda (e) (update e (make-NotTypeFilter u rst x)))) proc poly pred cert acc-ids maker-id)] ;; otherwise [(t (TypeFilter: u (list) _)) diff --git a/collects/typed-scheme/typecheck/tc-structs.ss b/collects/typed-scheme/typecheck/tc-structs.ss index 424cb02e..510b3422 100644 --- a/collects/typed-scheme/typecheck/tc-structs.ss +++ b/collects/typed-scheme/typecheck/tc-structs.ss @@ -76,7 +76,7 @@ ;; Option[Struct-Ty] -> Listof[Type] (define (get-parent-flds p) (match p - [(Struct: _ _ flds _ _ _ _ _) flds] + [(Struct: _ _ flds _ _ _ _ _ _) flds] [(Name: n) (get-parent-flds (lookup-type-name n))] [#f null])) @@ -99,7 +99,7 @@ (define-values (struct-type-id maker pred getters setters) (struct-names nm flds setters?)) (let* ([name (syntax-e nm)] [fld-types (append parent-field-types types)] - [sty (make-Struct name parent fld-types proc-ty poly? pred (syntax-local-certifier) getters)] + [sty (make-Struct name parent fld-types proc-ty poly? pred (syntax-local-certifier) getters (or maker* maker))] [external-fld-types/no-parent types] [external-fld-types fld-types]) (if type-only diff --git a/collects/typed-scheme/types/abbrev.ss b/collects/typed-scheme/types/abbrev.ss index 5fb3610b..57688d1c 100644 --- a/collects/typed-scheme/types/abbrev.ss +++ b/collects/typed-scheme/types/abbrev.ss @@ -77,7 +77,7 @@ (define make-promise-ty (let ([s (string->uninterned-symbol "Promise")]) (lambda (t) - (make-Struct s #f (list t) #f #f #'promise? values (list #'values))))) + (make-Struct s #f (list t) #f #f #'promise? values (list #'values) #'values)))) (define -Listof (-poly (list-elem) (make-Listof list-elem))) @@ -256,8 +256,8 @@ (define (make-arr-dots dom rng dty dbound) (make-arr* dom rng #:drest (cons dty dbound))) -(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 (-struct name parent flds accs constructor [proc #f] [poly #f] [pred #'dummy] [cert values]) + (make-Struct name parent flds proc poly pred cert accs constructor)) (define (-filter t [p null] [i 0]) (make-LTypeFilter t p i)) diff --git a/collects/typed-scheme/types/printer.ss b/collects/typed-scheme/types/printer.ss index 2092712c..c2ab6366 100644 --- a/collects/typed-scheme/types/printer.ss +++ b/collects/typed-scheme/types/printer.ss @@ -166,8 +166,8 @@ (fp "~a" (cons 'List (tuple-elems t)))] [(Base: n cnt) (fp "~a" n)] [(Opaque: pred _) (fp "(Opaque ~a)" (syntax->datum pred))] - [(Struct: 'Promise par (list fld) proc _ _ _ _) (fp "(Promise ~a)" fld)] - [(Struct: nm par flds proc _ _ _ _) + [(Struct: 'Promise par (list fld) proc _ _ _ _ _) (fp "(Promise ~a)" fld)] + [(Struct: nm par flds proc _ _ _ _ _) (fp "#(struct:~a ~a" nm flds) (when proc (fp " ~a" proc)) diff --git a/collects/typed-scheme/types/remove-intersect.ss b/collects/typed-scheme/types/remove-intersect.ss index dbf1c41b..cbb0e55b 100644 --- a/collects/typed-scheme/types/remove-intersect.ss +++ b/collects/typed-scheme/types/remove-intersect.ss @@ -50,18 +50,18 @@ [(or (list (Pair: _ _) _) (list _ (Pair: _ _))) #f] - [(or (list (Value: '()) (Struct: n _ flds _ _ _ _ _)) - (list (Struct: n _ flds _ _ _ _ _) (Value: '()))) + [(or (list (Value: '()) (Struct: n _ flds _ _ _ _ _ _)) + (list (Struct: n _ flds _ _ _ _ _ _) (Value: '()))) #f] - [(list (Struct: n _ flds _ _ _ _ _) - (Struct: n _ flds* _ _ _ _ _)) + [(list (Struct: n _ flds _ _ _ _ _ _) + (Struct: n _ flds* _ _ _ _ _ _)) (for/and ([f flds] [f* flds*]) (overlap f f*))] ;; n and n* must be different, so there's no overlap - [(list (Struct: n #f flds _ _ _ _ _) - (Struct: n* #f flds* _ _ _ _ _)) + [(list (Struct: n #f flds _ _ _ _ _ _) + (Struct: n* #f flds* _ _ _ _ _ _)) #f] - [(list (Struct: n p flds _ _ _ _ _) - (Struct: n* p* flds* _ _ _ _ _)) + [(list (Struct: n p flds _ _ _ _ _ _) + (Struct: n* p* flds* _ _ _ _ _ _)) (and (= (length flds) (length flds*)) (for/and ([f flds] [f* flds*]) (overlap f f*)))] [else #t])]))) diff --git a/collects/typed-scheme/types/subtype.ss b/collects/typed-scheme/types/subtype.ss index 7b1e5a52..64cbbc2c 100644 --- a/collects/typed-scheme/types/subtype.ss +++ b/collects/typed-scheme/types/subtype.ss @@ -306,22 +306,22 @@ [(s (Union: es)) (or (and (ormap (lambda (elem) (subtype*/no-fail A0 s elem)) es) A0) (fail! s t))] ;; subtyping on immutable structs is covariant - [((Struct: nm _ flds #f _ _ _ _) (Struct: nm _ flds* #f _ _ _ _)) + [((Struct: nm _ flds #f _ _ _ _ _) (Struct: nm _ flds* #f _ _ _ _ _)) (subtypes* A0 flds flds*)] - [((Struct: nm _ flds proc _ _ _ _) (Struct: nm _ flds* proc* _ _ _ _)) + [((Struct: nm _ flds proc _ _ _ _ _) (Struct: nm _ flds* proc* _ _ _ _ _)) (subtypes* A0 (cons proc flds) (cons proc* flds*))] - [((Struct: _ _ _ _ _ _ _ _) (StructTop: (? (lambda (s2) (type-equal? s2 s))))) + [((Struct: _ _ _ _ _ _ _ _ _) (StructTop: (? (lambda (s2) (type-equal? s2 s))))) A0] [((Box: _) (BoxTop:)) A0] [((Vector: _) (VectorTop:)) A0] [((MPair: _ _) (MPairTop:)) A0] [((Hashtable: _ _) (HashtableTop:)) A0] ;; subtyping on structs follows the declared hierarchy - [((Struct: nm (? Type? parent) flds proc _ _ _ _) other) + [((Struct: nm (? Type? parent) flds proc _ _ _ _ _) other) ;(printf "subtype - hierarchy : ~a ~a ~a~n" nm parent other) (subtype* A0 parent other)] ;; Promises are covariant - [((Struct: 'Promise _ (list t) _ _ _ _ _) (Struct: 'Promise _ (list t*) _ _ _ _ _)) (subtype* A0 t t*)] + [((Struct: 'Promise _ (list t) _ _ _ _ _ _) (Struct: 'Promise _ (list t*) _ _ _ _ _ _)) (subtype* A0 t t*)] ;; subtyping on values is pointwise [((Values: vals1) (Values: vals2)) (subtypes* A0 vals1 vals2)] ;; trivial case for Result