From 7fe635dfee0ad73505c324a615db3607d1fc3e9a Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Thu, 19 Nov 2009 19:47:51 +0000 Subject: [PATCH 01/17] start on typed/scheme svn: r16896 original commit: d28add0fa915e099e11fbd7ef44fb2e3e2c0ee40 --- collects/typed-scheme/minimal.ss | 4 ++-- collects/typed-scheme/private/base-env.ss | 8 +++++++- collects/typed/private/wrap.ss | 10 ++++++++++ collects/typed/scheme.ss | 4 ++++ collects/typed/scheme/base.ss | 16 ++++++++++++++++ collects/typed/scheme/base/lang/reader.ss | 8 ++++++++ collects/typed/scheme/lang/reader.ss | 8 ++++++++ collects/typed/scheme/system.ss | 11 +---------- 8 files changed, 56 insertions(+), 13 deletions(-) create mode 100644 collects/typed/private/wrap.ss create mode 100644 collects/typed/scheme.ss create mode 100644 collects/typed/scheme/base.ss create mode 100644 collects/typed/scheme/base/lang/reader.ss create mode 100644 collects/typed/scheme/lang/reader.ss diff --git a/collects/typed-scheme/minimal.ss b/collects/typed-scheme/minimal.ss index 40bcc4c9..f3b6d039 100644 --- a/collects/typed-scheme/minimal.ss +++ b/collects/typed-scheme/minimal.ss @@ -1,9 +1,9 @@ #lang scheme/base (provide #%module-begin provide require rename-in rename-out prefix-in only-in all-from-out except-out except-in - providing begin) + providing begin subtract-in) -(require (for-syntax scheme/base)) +(require (for-syntax scheme/base) scheme/require) (define-for-syntax ts-mod 'typed-scheme/typed-scheme) diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss index 39c1c2cf..2f60de6a 100644 --- a/collects/typed-scheme/private/base-env.ss +++ b/collects/typed-scheme/private/base-env.ss @@ -8,7 +8,7 @@ '#%paramz "extra-procs.ss" (only-in '#%kernel [apply kernel:apply]) - scheme/promise + scheme/promise scheme/system (only-in string-constants/private/only-once maybe-print-message) (only-in scheme/match/runtime match:error matchable? match-equality-test) (for-syntax (only-in (types abbrev) [-Number N] [-Boolean B] [-Symbol Sym]))) @@ -830,3 +830,9 @@ [vector-split-at-right (-poly (a) ((list (-vec a)) -Integer . ->* . (-values (list (-vec a) (-vec a)))))] + +;; scheme/system +[system (-String . -> . -Boolean)] +[system* ((list -Pathlike) -String . ->* . -Boolean)] +[system/exit-code (-String . -> . -Integer)] +[system*/exit-code ((list -Pathlike) -String . ->* . -Integer)] diff --git a/collects/typed/private/wrap.ss b/collects/typed/private/wrap.ss new file mode 100644 index 00000000..8f2bb87b --- /dev/null +++ b/collects/typed/private/wrap.ss @@ -0,0 +1,10 @@ +#lang scheme + +(define-syntax (mb stx) + (syntax-case stx () + [(_ id) + #'(#%plain-module-begin + (require id) + (provide (all-from-out id)))])) + +(provide (rename-out [mb #%module-begin])) \ No newline at end of file diff --git a/collects/typed/scheme.ss b/collects/typed/scheme.ss new file mode 100644 index 00000000..37e8e2ad --- /dev/null +++ b/collects/typed/scheme.ss @@ -0,0 +1,4 @@ +#lang s-exp typed-scheme/minimal + +(require typed/scheme/base (subtract-in scheme typed/scheme/base scheme/contract)) +(provide (all-from-out typed/scheme/base scheme)) \ No newline at end of file diff --git a/collects/typed/scheme/base.ss b/collects/typed/scheme/base.ss new file mode 100644 index 00000000..8798e922 --- /dev/null +++ b/collects/typed/scheme/base.ss @@ -0,0 +1,16 @@ +#lang s-exp typed-scheme/minimal + + + +(providing (libs (except scheme/base #%module-begin #%top-interaction with-handlers lambda #%app) + (except typed-scheme/private/prims) + (except typed-scheme/private/base-types) + (except typed-scheme/private/base-types-extra)) + (basics #%module-begin + #%top-interaction + lambda + #%app)) +(require typed-scheme/private/base-env typed-scheme/private/base-special-env + (for-syntax typed-scheme/private/base-types-extra)) +(provide (rename-out [with-handlers: with-handlers]) + (for-syntax (all-from-out typed-scheme/private/base-types-extra))) diff --git a/collects/typed/scheme/base/lang/reader.ss b/collects/typed/scheme/base/lang/reader.ss new file mode 100644 index 00000000..009b1f17 --- /dev/null +++ b/collects/typed/scheme/base/lang/reader.ss @@ -0,0 +1,8 @@ +#lang s-exp syntax/module-reader + +typed-scheme + +#:read r:read +#:read-syntax r:read-syntax + +(require (prefix-in r: typed-scheme/typed-reader)) diff --git a/collects/typed/scheme/lang/reader.ss b/collects/typed/scheme/lang/reader.ss new file mode 100644 index 00000000..009b1f17 --- /dev/null +++ b/collects/typed/scheme/lang/reader.ss @@ -0,0 +1,8 @@ +#lang s-exp syntax/module-reader + +typed-scheme + +#:read r:read +#:read-syntax r:read-syntax + +(require (prefix-in r: typed-scheme/typed-reader)) diff --git a/collects/typed/scheme/system.ss b/collects/typed/scheme/system.ss index f10fe2e2..61bc8bc1 100644 --- a/collects/typed/scheme/system.ss +++ b/collects/typed/scheme/system.ss @@ -1,10 +1 @@ -#lang typed-scheme - -(require typed/private/utils) - -(require/typed/provide - scheme/system - [system (String -> Boolean)] - [system* (Path-String String * -> Boolean)] - [system/exit-code (String -> Integer)] - [system*/exit-code (Path-String String * -> Integer)]) +#lang s-exp typed/private/wrap scheme/system \ No newline at end of file From a1f96d6ce8dc8e2125f7aa19d8ce26e40be63d3b Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Fri, 20 Nov 2009 00:06:32 +0000 Subject: [PATCH 02/17] checkpoint svn: r16908 original commit: 111b71c844707b146bbc1500dc086ef3c5ef7070 --- .../typed-scheme/private/base-env-numeric.ss | 94 +++++++++++++++ collects/typed-scheme/private/base-env.ss | 109 ++++-------------- collects/typed-scheme/private/base-types.ss | 8 ++ .../typed-scheme/typecheck/tc-expr-unit.ss | 10 +- collects/typed-scheme/types/abbrev.ss | 27 +++-- collects/typed-scheme/types/subtype.ss | 86 ++++++++------ 6 files changed, 199 insertions(+), 135 deletions(-) create mode 100644 collects/typed-scheme/private/base-env-numeric.ss diff --git a/collects/typed-scheme/private/base-env-numeric.ss b/collects/typed-scheme/private/base-env-numeric.ss new file mode 100644 index 00000000..682cb7a2 --- /dev/null +++ b/collects/typed-scheme/private/base-env-numeric.ss @@ -0,0 +1,94 @@ +#lang s-exp "env-lang.ss" + +(require + scheme/tcp + scheme + scheme/unsafe/ops + (only-in rnrs/lists-6 fold-left) + '#%paramz + "extra-procs.ss" + (only-in '#%kernel [apply kernel:apply]) + scheme/promise scheme/system + (only-in string-constants/private/only-once maybe-print-message) + (only-in scheme/match/runtime match:error matchable? match-equality-test) + (for-syntax (only-in (types abbrev) [-Number N] [-Boolean B] [-Symbol Sym]))) + +;; numeric operations +[modulo (cl->* (-Integer -Integer . -> . -Integer))] +[= (->* (list N N) N B)] +[>= (->* (list N N) N B)] +[< (->* (list N N) N B)] +[<= (->* (list N N) N B)] +[> (->* (list N N) N B)] +[zero? (N . -> . B)] +[* (cl->* (->* '() -Integer -Integer) (->* '() N N))] +[/ (cl->* (->* (list N) N N))] +[+ (cl->* (->* '() -Integer -Integer) (->* '() N N))] +[- (cl->* (->* (list -Integer) -Integer -Integer) (->* (list N) N N))] +[max (cl->* (->* (list -Integer) -Integer -Integer) + (->* (list N) N N))] +[min (cl->* (->* (list -Integer) -Integer -Integer) + (->* (list N) N N))] +[positive? (-> N B)] +[negative? (-> N B)] +[odd? (-> -Integer B)] +[even? (-> -Integer B)] +[add1 (cl->* (-> -Integer -Integer) + (-> N N))] +[sub1 (cl->* (-> -Integer -Integer) + (-> N N))] +[quotient (-Integer -Integer . -> . -Integer)] +[remainder (-Integer -Integer . -> . -Integer)] +[quotient/remainder + (make-Function (list (make-arr (list -Integer -Integer) (-values (list -Integer -Integer)))))] + +[exact? (N . -> . B)] +[inexact? (N . -> . B)] +[exact->inexact (N . -> . N)] +[inexact->exact (N . -> . N)] + +[number? (make-pred-ty N)] +[integer? (Univ . -> . B : (-LFS (list (-filter N)) (list (-not-filter -Integer))))] +[exact-integer? (make-pred-ty -Integer)] + +[real? (Univ . -> . B : (-LFS (list (-filter N)) (list)))] +[complex? (Univ . -> . B : (-LFS (list (-filter N)) (list)))] +[rational? (Univ . -> . B : (-LFS (list (-filter N)) (list)))] +[floor (-> N N)] +[ceiling (-> N N)] +[truncate (-> N N)] +[make-rectangular (N N . -> . N)] +[make-polar (N N . -> . N)] +[real-part (N . -> . N)] +[imag-part (N . -> . N)] +[magnitude (N . -> . N)] +[angle (N . -> . N)] +[numerator (N . -> . -Integer)] +[denominator (N . -> . -Integer)] +[rationalize (N N . -> . N)] +[expt (cl->* (-Integer -Integer . -> . -Integer) (N N . -> . N))] +[sqrt (N . -> . N)] +[log (N . -> . N)] +[exp (N . -> . N)] +[cos (N . -> . N)] +[sin (N . -> . N)] +[tan (N . -> . N)] +[acos (N . -> . N)] +[asin (N . -> . N)] +[atan (N . -> . N)] +[gcd (null -Integer . ->* . -Integer)] +[lcm (null -Integer . ->* . -Integer)] + +[round (N . -> . -Integer)] + +;; scheme/math + +[sgn (-Real . -> . -Real)] +[pi N] +[sqr (N . -> . N)] +[sgn (N . -> . N)] +[conjugate (N . -> . N)] +[sinh (N . -> . N)] +[cosh (N . -> . N)] +[tanh (N . -> . N)] +;; end numeric ops diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss index 2f60de6a..1c7f92a6 100644 --- a/collects/typed-scheme/private/base-env.ss +++ b/collects/typed-scheme/private/base-env.ss @@ -11,7 +11,10 @@ scheme/promise scheme/system (only-in string-constants/private/only-once maybe-print-message) (only-in scheme/match/runtime match:error matchable? match-equality-test) - (for-syntax (only-in (types abbrev) [-Number N] [-Boolean B] [-Symbol Sym]))) + (for-syntax (only-in (types abbrev) [-Number N] [-Boolean B] [-Symbol Sym])) + ;; require the split-out files + "base-env-numeric.ss" + ) [raise (Univ . -> . (Un))] @@ -55,19 +58,12 @@ [null? (make-pred-ty (-val null))] [eof-object? (make-pred-ty (-val eof))] [null (-val null)] -[number? (make-pred-ty N)] [char? (make-pred-ty -Char)] -[integer? (Univ . -> . B : (-LFS (list (-filter N)) (list (-not-filter -Integer))))] -[exact-integer? (make-pred-ty -Integer)] + [boolean? (make-pred-ty B)] -[add1 (cl->* (-> -Integer -Integer) - (-> N N))] -[sub1 (cl->* (-> -Integer -Integer) - (-> N N))] [eq? (-> Univ Univ B)] [eqv? (-> Univ Univ B)] [equal? (-> Univ Univ B)] -[even? (-> N B)] [assert (-poly (a) (-> (Un a (-val #f)) a))] [gensym (cl-> [(Sym) Sym] [() Sym])] @@ -167,20 +163,6 @@ [sleep (N . -> . -Void)] -[= (->* (list N N) N B)] -[>= (->* (list N N) N B)] -[< (->* (list N N) N B)] -[<= (->* (list N N) N B)] -[> (->* (list N N) N B)] -[zero? (N . -> . B)] -[* (cl->* (->* '() -Integer -Integer) (->* '() N N))] -[/ (cl->* (->* (list N) N N))] -[+ (cl->* (->* '() -Integer -Integer) (->* '() N N))] -[- (cl->* (->* (list -Integer) -Integer -Integer) (->* (list N) N N))] -[max (cl->* (->* (list -Integer) -Integer -Integer) - (->* (list N) N N))] -[min (cl->* (->* (list -Integer) -Integer -Integer) - (->* (list N) N N))] [build-list (-poly (a) (-Integer (-Integer . -> . a) . -> . (-lst a)))] [reverse (-poly (a) (-> (-lst a) (-lst a)))] [append (-poly (a) (->* (list) (-lst a) (-lst a)))] @@ -229,10 +211,10 @@ [string-copy (-> -String -String)] [string->immutable-string (-> -String -String)] -[string-ref (-> -String N -Char)] +[string-ref (-> -String -Nat -Char)] [substring (cl->* - (-> -String N -String) - (-> -String N N -String))] + (-> -String -Nat -String) + (-> -String -Nat -Nat -String))] [string->path (-> -String -Path)] [file-exists? (-> -Pathlike B)] @@ -248,7 +230,7 @@ #:mode (one-of/c 'binary 'text) #f a))] -[random (cl-> [(-Integer) -Integer] [() N])] +[random (cl-> [(-Nat) -Nat] [() -Real])] [assq (-poly (a b) (a (-lst (-pair a b)) . -> . (-opt (-pair a b))))] [assv (-poly (a b) (a (-lst (-pair a b)) . -> . (-opt (-pair a b))))] @@ -258,10 +240,6 @@ [list-ref (-poly (a) ((-lst a) -Integer . -> . a))] [list-tail (-poly (a) ((-lst a) -Integer . -> . (-lst a)))] -[positive? (-> N B)] -[negative? (-> N B)] -[odd? (-> -Integer B)] -[even? (-> -Integer B)] [apply (-poly (a b) (((list) a . ->* . b) (-lst a) . -> . b))] [kernel:apply (-poly (a b) (((list) a . ->* . b) (-lst a) . -> . b))] @@ -270,7 +248,7 @@ (list (make-arr (list ((list) (a a) . ->... . b) (-lst a)) - (-values (list (-pair b (-val '())) N N N))))))] + (-values (list (-pair b (-val '())) -Integer -Integer -Integer))))))] [call/cc (-poly (a b) (((a . -> . (Un)) . -> . b) . -> . (Un a b)))] [call/ec (-poly (a b) (((a . -> . (Un)) . -> . b) . -> . (Un a b)))] @@ -278,12 +256,6 @@ [call-with-escape-continuation (-poly (a b) (((a . -> . (Un)) . -> . b) . -> . (Un a b)))] [struct->vector (Univ . -> . (-vec Univ))] - -[quotient (-Integer -Integer . -> . -Integer)] -[remainder (-Integer -Integer . -> . -Integer)] -[quotient/remainder - (make-Function (list (make-arr (list -Integer -Integer) (-values (list -Integer -Integer)))))] - ;; parameter stuff [parameterization-key Sym] @@ -313,7 +285,8 @@ [regexp-match (let ([?outp (-opt -Output-Port)] - [?N (-opt N)] + [N -Nat] + [?N (-opt -Nat)] [optlist (lambda (t) (-opt (-lst (-opt t))))] [-StrRx (Un -String -Regexp -PRegexp)] [-BtsRx (Un -Bytes -Byte-Regexp -Byte-PRegexp)] @@ -332,7 +305,8 @@ [(-Pattern -InpBts N ?N ?outp) (optlist -Bytes)]))] [regexp-match* - (let ([?N (-opt N)] + (let ([N -Nat] + [?N (-opt -Nat)] [-StrRx (Un -String -Regexp -PRegexp)] [-BtsRx (Un -Bytes -Byte-Regexp -Byte-PRegexp)] [-InpBts (Un -Input-Port -Bytes)]) @@ -342,9 +316,9 @@ (-Pattern -InpBts [N ?N] . ->opt . (-lst -Bytes))))] [regexp-try-match (let ([?outp (-opt -Output-Port)] - [?N (-opt N)] + [?N (-opt -Nat)] [optlist (lambda (t) (-opt (-lst (-opt t))))]) - (->opt -Pattern -Input-Port [N ?N ?outp] (optlist -Bytes)))] + (->opt -Pattern -Input-Port [-Nat ?N ?outp] (optlist -Bytes)))] [regexp-match-exact? (-Pattern (Un -String -Bytes -Input-Port) . -> . B)] @@ -352,7 +326,8 @@ [regexp-match-positions (let ([?outp (-opt -Output-Port)] - [?N (-opt N)] + [N -Nat] + [?N (-opt -Nat)] [optlist (lambda (t) (-opt (-lst (-opt t))))] [-StrRx (Un -String -Regexp -PRegexp)] [-BtsRx (Un -Bytes -Byte-Regexp -Byte-PRegexp)] @@ -360,12 +335,12 @@ (->opt -Pattern (Un -String -InpBts) [N ?N ?outp] (optlist (-pair -Nat -Nat))))] [regexp-match-positions* (let ([?outp (-opt -Output-Port)] - [?N (-opt N)] + [?N (-opt -Nat)] [optlist (lambda (t) (-opt (-lst (-opt t))))] [-StrRx (Un -String -Regexp -PRegexp)] [-BtsRx (Un -Bytes -Byte-Regexp -Byte-PRegexp)] [-InpBts (Un -Input-Port -Bytes)]) - (->opt -Pattern (Un -String -InpBts) [N ?N ?outp] (-lst (-pair -Nat -Nat))))] + (->opt -Pattern (Un -String -InpBts) [-Nat ?N ?outp] (-lst (-pair -Nat -Nat))))] #; [regexp-match-peek-positions*] #; @@ -383,7 +358,6 @@ [string->number (cl-> [(-String) N] [(-String N) N])] [current-milliseconds (-> -Integer)] -[modulo (cl->* (-Integer -Integer . -> . -Integer))] ;; errors @@ -395,38 +369,6 @@ ;; this is a hack [match:error ((list) Univ . ->* . (Un))] -[exact? (N . -> . B)] -[inexact? (N . -> . B)] -[exact->inexact (N . -> . N)] -[inexact->exact (N . -> . N)] - -[real? (Univ . -> . B : (-LFS (list (-filter N)) (list)))] -[complex? (Univ . -> . B : (-LFS (list (-filter N)) (list)))] -[rational? (Univ . -> . B : (-LFS (list (-filter N)) (list)))] -[floor (-> N N)] -[ceiling (-> N N)] -[truncate (-> N N)] -[make-rectangular (N N . -> . N)] -[make-polar (N N . -> . N)] -[real-part (N . -> . N)] -[imag-part (N . -> . N)] -[magnitude (N . -> . N)] -[angle (N . -> . N)] -[numerator (N . -> . -Integer)] -[denominator (N . -> . -Integer)] -[rationalize (N N . -> . N)] -[expt (cl->* (-Integer -Integer . -> . -Integer) (N N . -> . N))] -[sqrt (N . -> . N)] -[log (N . -> . N)] -[exp (N . -> . N)] -[cos (N . -> . N)] -[sin (N . -> . N)] -[tan (N . -> . N)] -[acos (N . -> . N)] -[asin (N . -> . N)] -[atan (N . -> . N)] -[gcd (null -Integer . ->* . -Integer)] -[lcm (null -Integer . ->* . -Integer)] [arithmetic-shift (-Integer -Integer . -> . -Integer)] [bitwise-and (null -Integer . ->* . -Integer)] @@ -480,7 +422,6 @@ [current-output-port (-Param -Output-Port -Output-Port)] [current-error-port (-Param -Output-Port -Output-Port)] [current-input-port (-Param -Input-Port -Input-Port)] -[round (N . -> . -Integer)] [seconds->date (-Integer . -> . (make-Name #'date))] [current-seconds (-> -Integer)] [current-print (-Param (Univ . -> . Univ) (Univ . -> . Univ))] @@ -765,16 +706,6 @@ (funarg* a (-opt -Pathlike) . -> . a) (funarg* a (-opt -Pathlike) Univ . -> . a))))] -;; scheme/math - -[sgn (-Real . -> . -Real)] -[pi N] -[sqr (N . -> . N)] -[sgn (N . -> . N)] -[conjugate (N . -> . N)] -[sinh (N . -> . N)] -[cosh (N . -> . N)] -[tanh (N . -> . N)] ;; scheme/pretty diff --git a/collects/typed-scheme/private/base-types.ss b/collects/typed-scheme/private/base-types.ss index 32e03043..bd9a6089 100644 --- a/collects/typed-scheme/private/base-types.ss +++ b/collects/typed-scheme/private/base-types.ss @@ -1,7 +1,15 @@ #lang s-exp "type-env-lang.ss" [Number -Number] +[Complex -Number] [Integer -Integer] +[Real -Real] +[Exact-Rational -ExactRational] +[Flonum -Flonum] +[Exact-Positive-Integer -ExactPositiveInteger] +[Exact-Nonnegative-Integer -ExactNonnegativeInteger] +[Natural -ExactNonnegativeInteger] + [Void -Void] [Boolean -Boolean] [Symbol -Symbol] diff --git a/collects/typed-scheme/typecheck/tc-expr-unit.ss b/collects/typed-scheme/typecheck/tc-expr-unit.ss index b57abb2f..85a5b9d8 100644 --- a/collects/typed-scheme/typecheck/tc-expr-unit.ss +++ b/collects/typed-scheme/typecheck/tc-expr-unit.ss @@ -32,8 +32,14 @@ [i:exp expected] [i:boolean (-val (syntax-e #'i))] [i:identifier (-val (syntax-e #'i))] - [i:exact-integer -Integer] - [(~var i (3d real?)) -Number] + [0 -Zero] + [(~var i (3d exact-positive-integer?)) -ExactPositiveInteger] + [(~var i (3d exact-nonnegative-integer?)) -ExactNonnegativeInteger] + [(~var i (3d exact-integer?)) -Integer] + [(~var i (3d (lambda (e) (and (exact? e) (rational? e))))) -ExactRational] + [(~var i (3d inexact-real?)) -Flonum] + [(~var i (3d real?)) -Real] + [(~var i (3d number?)) -Number] [i:str -String] [i:char -Char] [i:keyword (-val (syntax-e #'i))] diff --git a/collects/typed-scheme/types/abbrev.ss b/collects/typed-scheme/types/abbrev.ss index 27e9ed6e..164483b0 100644 --- a/collects/typed-scheme/types/abbrev.ss +++ b/collects/typed-scheme/types/abbrev.ss @@ -67,9 +67,6 @@ (define -Listof (-poly (list-elem) (make-Listof list-elem))) - -(define -Number (make-Base 'Number #'number?)) -(define -Integer (make-Base 'Integer #'exact-integer?)) (define -Boolean (make-Base 'Boolean #'boolean?)) (define -Symbol (make-Base 'Symbol #'symbol?)) (define -Void (make-Base 'Void #'void?)) @@ -96,15 +93,11 @@ (define Univ (make-Univ)) (define Err (make-Error)) -(define -Nat -Integer) -(define -Real -Number) - (define -Port (*Un -Output-Port -Input-Port)) (define -Pathlike (*Un -String -Path)) (define -Pathlike* (*Un -String -Path (-val 'up) (-val 'same))) (define -Pattern (*Un -Bytes -Regexp -PRegexp -Byte-Regexp -Byte-PRegexp -String)) -(define -Byte -Number) (define -no-lfilter (make-LFilterSet null null)) (define -no-filter (make-FilterSet null null)) @@ -114,6 +107,26 @@ (define -car (make-CarPE)) (define -cdr (make-CdrPE)) +;; Numeric hierarchy +(define -Number (make-Base 'Number #'number?)) + +(define -Flonum (make-Base 'Flonum #'inexact-real?)) + +(define -ExactRational + (make-Base 'Exact-Rational #'(and/c rational? exact?))) +(define -Integer (make-Base 'Integer #'exact-integer?)) +(define -ExactPositiveInteger + (make-Base 'Exact-Positive-Integer #'exact-positive-integer?)) + +(define -Zero (-val 0)) +(define -Real (*Un -Flonum -ExactRational)) +(define -ExactNonnegativeInteger (*Un -Zero -ExactPositiveInteger)) +(define -Nat -ExactNonnegativeInteger) + +(define -Byte -Number) + + + ;; convenient syntax (define-syntax -v diff --git a/collects/typed-scheme/types/subtype.ss b/collects/typed-scheme/types/subtype.ss index 3bbb1d6d..04de5214 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 + scheme/match unstable/match mzlib/trace (for-syntax scheme/base syntax/parse)) @@ -210,34 +210,46 @@ [else (let* ([A0 (remember s t A)]) (parameterize ([current-seen A0]) - (match (list s t) - [(list _ (Univ:)) A0] + (match* (s t) + [(_ (Univ:)) A0] ;; error is top and bot - [(list _ (Error:)) A0] - [(list (Error:) _) A0] + [(_ (Error:)) A0] + [((Error:) _) A0] ;; (Un) is bot - [(list _ (Union: (list))) (fail! s t)] - [(list (Union: (list)) _) A0] + [(_ (Union: (list))) (fail! s t)] + [((Union: (list)) _) A0] ;; value types - [(list (Value: v1) (Value: v2)) (=> unmatch) (if (equal? v1 v2) A0 (unmatch))] - ;; integers are numbers too - [(list (Base: 'Integer _) (Base: 'Number _)) A0] + [((Value: v1) (Value: v2)) (=> 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 _) (Base: 'Number _)) A0] + [((Base: 'Exact-Rational _) (Base: 'Number _)) A0] + [((Base: 'Exact-Positive-Integer _) (Base: 'Exact-Rational _)) A0] + [((Base: 'Exact-Positive-Integer _) (Base: 'Number _)) A0] + ;; values are subtypes of their "type" - [(list (Value: (? integer? n)) (Base: 'Integer _)) A0] - [(list (Value: (? number? n)) (Base: 'Number _)) A0] - [(list (Value: (? boolean? n)) (Base: 'Boolean _)) A0] - [(list (Value: (? symbol? n)) (Base: 'Symbol _)) A0] - [(list (Value: (? string? n)) (Base: 'String _)) A0] + [((Value: (? integer? n)) (Base: 'Integer _)) A0] + [((Value: (? exact-nonnegative-integer? n)) (Base: 'Exact-Nonnegative-Integer _)) 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: (? number? n)) (Base: 'Number _)) A0] + + [((Value: (? boolean? n)) (Base: 'Boolean _)) A0] + [((Value: (? symbol? n)) (Base: 'Symbol _)) A0] + [((Value: (? string? n)) (Base: 'String _)) A0] ;; tvars are equal if they are the same variable - [(list (F: t) (F: t*)) (if (eq? t t*) A0 (fail! s t))] + [((F: t) (F: t*)) (if (eq? t t*) A0 (fail! s t))] ;; special-case for case-lambda/union - [(list (Function: arr1) (Function: (list arr2))) + [((Function: arr1) (Function: (list arr2))) (when (null? arr1) (fail! s t)) (or (arr-subtype*/no-fail A0 (combine-arrs arr1) arr2) (supertype-of-one/arr A0 arr2 arr1) (fail! s t))] ;; case-lambda - [(list (Function: arr1) (Function: arr2)) + [((Function: arr1) (Function: arr2)) (when (null? arr1) (fail! s t)) (let loop-arities ([A* A0] [arr2 arr2]) @@ -246,65 +258,65 @@ [(supertype-of-one/arr A* (car arr2) arr1) => (lambda (A) (loop-arities A (cdr arr2)))] [else (fail! s t)]))] ;; recur structurally on pairs - [(list (Pair: a d) (Pair: a* d*)) + [((Pair: a d) (Pair: a* d*)) (let ([A1 (subtype* A0 a a*)]) (and A1 (subtype* A1 d d*)))] ;; quantification over two types preserves subtyping - [(list (Poly: ns b1) (Poly: ms b2)) + [((Poly: ns b1) (Poly: ms b2)) (=> unmatch) (unless (= (length ns) (length ms)) (unmatch)) ;(printf "Poly: ~n~a ~n~a~n" b1 (subst-all (map list ms (map make-F ns)) b2)) (subtype* A0 b1 (subst-all (map list ms (map make-F ns)) b2))] - [(list (Refinement: par _ _) t) + [((Refinement: par _ _) t) (subtype* A0 par t)] ;; use unification to see if we can use the polytype here - [(list (Poly: vs b) s) + [((Poly: vs b) s) (=> unmatch) (if (unify vs (list b) (list s)) A0 (unmatch))] - [(list s (Poly: vs b)) + [(s (Poly: vs b)) (=> unmatch) (if (null? (fv b)) (subtype* A0 s b) (unmatch))] ;; rec types, applications and names (that aren't the same - [(list (? needs-resolving? s) other) + [((? needs-resolving? s) other) (let ([s* (resolve-once s)]) (if (Type? s*) ;; needed in case this was a name that hasn't been resolved yet (subtype* A0 s* other) (fail! s t)))] - [(list other (? needs-resolving? t)) + [(other (? needs-resolving? t)) (let ([t* (resolve-once t)]) (if (Type? t*) ;; needed in case this was a name that hasn't been resolved yet (subtype* A0 other t*) (fail! s t)))] ;; for unions, we check the cross-product - [(list (Union: es) t) (and (andmap (lambda (elem) (subtype* A0 elem t)) es) A0)] - [(list s (Union: es)) (and (ormap (lambda (elem) (subtype*/no-fail A0 s elem)) es) A0)] + [((Union: es) t) (and (andmap (lambda (elem) (subtype* A0 elem t)) es) A0)] + [(s (Union: es)) (and (ormap (lambda (elem) (subtype*/no-fail A0 s elem)) es) A0)] ;; subtyping on immutable structs is covariant - [(list (Struct: nm _ flds #f _ _ _) (Struct: nm _ flds* #f _ _ _)) + [((Struct: nm _ flds #f _ _ _) (Struct: nm _ flds* #f _ _ _)) (subtypes* A0 flds flds*)] - [(list (Struct: nm _ flds proc _ _ _) (Struct: nm _ flds* proc* _ _ _)) + [((Struct: nm _ flds proc _ _ _) (Struct: nm _ flds* proc* _ _ _)) (subtypes* A0 (cons proc flds) (cons proc* flds*))] ;; subtyping on structs follows the declared hierarchy - [(list (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 - [(list (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 - [(list (Values: vals1) (Values: vals2)) (subtypes* A0 vals1 vals2)] + [((Values: vals1) (Values: vals2)) (subtypes* A0 vals1 vals2)] ;; trivial case for Result - [(list (Result: t f o) (Result: t* f o)) + [((Result: t f o) (Result: t* f o)) (subtype* A0 t t*)] ;; we can ignore interesting results - [(list (Result: t f o) (Result: t* (LFilterSet: (list) (list)) (LEmpty:))) + [((Result: t f o) (Result: t* (LFilterSet: (list) (list)) (LEmpty:))) (subtype* A0 t t*)] ;; subtyping on other stuff - [(list (Syntax: t) (Syntax: t*)) + [((Syntax: t) (Syntax: t*)) (subtype* A0 t t*)] - [(list (Instance: t) (Instance: t*)) + [((Instance: t) (Instance: t*)) (subtype* A0 t t*)] ;; otherwise, not a subtype - [_ (fail! s t) #;(printf "failed")])))])))) + [(_ _) (fail! s t) #;(printf "failed")])))])))) (define (type-compare? a b) (and (subtype a b) (subtype b a))) From 9e87d52ba16c52d49a8faf48343a1d6279538886 Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Fri, 20 Nov 2009 03:56:57 +0000 Subject: [PATCH 03/17] many fixes svn: r16913 original commit: 1da2c7cd7d45b7f8a53d1892609e135820ef4301 --- .../unit-tests/typecheck-tests.ss | 124 +++++++++--------- .../typed-scheme/private/base-env-numeric.ss | 26 +++- .../typed-scheme/typecheck/tc-expr-unit.ss | 2 +- collects/typed-scheme/types/abbrev.ss | 2 +- collects/typed-scheme/types/convenience.ss | 1 + collects/typed-scheme/types/subtype.ss | 5 + 6 files changed, 91 insertions(+), 69 deletions(-) diff --git a/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss b/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss index 758e98e8..e3b2e210 100644 --- a/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss +++ b/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss @@ -29,6 +29,9 @@ (define N -Number) (define B -Boolean) (define Sym -Symbol) +(define -Pos -ExactPositiveInteger) +(define R -Real) +(define F -Flonum) (define (g) (run typecheck-tests)) @@ -73,9 +76,9 @@ (syntax-case stx () [(_ expr ty) (syntax/loc stx (tc-e expr #:ret (ret ty)))] [(_ expr #:proc p) - (syntax/loc stx + (quasisyntax/loc stx (let-values ([(t e) (tc-expr/expand/values expr)]) - (check-tc-result-equal? (format "~s" 'expr) (t) (p e))))] + #,(syntax/loc stx (check-tc-result-equal? (format "~s" 'expr) (t) (p e)))))] [(_ expr #:ret r) (syntax/loc stx (check-tc-result-equal? (format "~a" 'expr) (tc-expr/expand expr) r))] @@ -127,24 +130,24 @@ (+ 1 (car x)) 5)) N] - (tc-e/t (if (let ([y 12]) y) 3 4) -Integer) - (tc-e/t 3 -Integer) + (tc-e/t (if (let ([y 12]) y) 3 4) -Pos) + (tc-e/t 3 -Pos) (tc-e/t "foo" -String) - (tc-e (+ 3 4) -Integer) - [tc-e/t (lambda: () 3) (t:-> -Integer : (-LFS (list) (list (make-LBot))))] - [tc-e/t (lambda: ([x : Number]) 3) (t:-> N -Integer : (-LFS (list) (list (make-LBot))))] - [tc-e/t (lambda: ([x : Number] [y : Boolean]) 3) (t:-> N B -Integer : (-LFS (list) (list (make-LBot))))] - [tc-e/t (lambda () 3) (t:-> -Integer : (-LFS (list) (list (make-LBot))))] - [tc-e (values 3 4) #:ret (ret (list -Integer -Integer) (list (-FS (list) (list (make-Bot))) (-FS (list) (list (make-Bot)))))] - [tc-e (cons 3 4) (-pair -Integer -Integer)] - [tc-e (cons 3 #{'() : (Listof -Integer)}) (make-Listof -Integer)] + (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 (cons 3 4) (-pair -Pos -Pos)] + [tc-e (cons 3 (ann '() : (Listof Integer))) (make-Listof -Integer)] [tc-e (void) -Void] [tc-e (void 3 4) -Void] [tc-e (void #t #f '(1 2 3)) -Void] - [tc-e/t #(3 4 5) (make-Vector -Integer)] - [tc-e/t '(2 3 4) (-lst* -Integer -Integer -Integer)] - [tc-e/t '(2 3 #t) (-lst* -Integer -Integer (-val #t))] - [tc-e/t #(2 3 #t) (make-Vector (t:Un -Integer (-val #t)))] + [tc-e/t #(3 4 5) (make-Vector -Pos)] + [tc-e/t '(2 3 4) (-lst* -Pos -Pos -Pos)] + [tc-e/t '(2 3 #t) (-lst* -Pos -Pos (-val #t))] + [tc-e/t #(2 3 #t) (make-Vector (t:Un -Pos (-val #t)))] [tc-e/t '(#t #f) (-lst* (-val #t) (-val #f))] [tc-e/t (plambda: (a) ([l : (Listof a)]) (car l)) (make-Poly '(a) (t:-> (make-Listof (-v a)) (-v a)))] @@ -152,12 +155,12 @@ (make-Poly '(a) (t:-> (make-Listof (-v a)) (-v a)))] [tc-e/t (case-lambda: [([a : Number] [b : Number]) (+ a b)]) (t:-> N N N)] [tc-e (let: ([x : Number 5]) x) #:proc (get-let-name x 0 (-path -Number #'x))] - [tc-e (let-values ([(x) 4]) (+ x 1)) -Integer] + [tc-e (let-values ([(x) 4]) (+ x 1)) -Pos] [tc-e (let-values ([(#{x : Number} #{y : Boolean}) (values 3 #t)]) (and (= x 1) (not y))) #:proc (syntax-parser [(_ ([(_ y) . _]) . _) (ret -Boolean (-FS (list (make-TypeFilter (-val #f) null #'y)) null))])] - [tc-e/t (values 3) -Integer] + [tc-e/t (values 3) -Pos] [tc-e (values) #:ret (ret null)] - [tc-e (values 3 #f) #:ret (ret (list -Integer (-val #f)) (list (-FS (list) (list (make-Bot))) (-FS (list (make-Bot)) (list))))] + [tc-e (values 3 #f) #:ret (ret (list -Pos (-val #f)) (list (-FS (list) (list (make-Bot))) (-FS (list (make-Bot)) (list))))] [tc-e (map #{values @ Symbol} '(a b c)) (make-Listof Sym)] [tc-e (letrec: ([fact : (Number -> Number) (lambda: ([n : Number]) (if (zero? n) 1 (* n (fact (- n 1)))))]) (fact 20)) @@ -187,8 +190,8 @@ 'bc)) N] [tc-e/t (let: ((x : Number 3)) (if (boolean? x) (not x) #t)) (-val #t)] - [tc-e/t (begin 3) -Integer] - [tc-e/t (begin #f 3) -Integer] + [tc-e/t (begin 3) -Pos] + [tc-e/t (begin #f 3) -Pos] [tc-e/t (begin #t) (-val #t)] [tc-e/t (begin0 #t) (-val #t)] [tc-e/t (begin0 #t 3) (-val #t)] @@ -196,14 +199,14 @@ [tc-e #f #:ret (ret (-val #f) (-FS (list (make-Bot)) null))] [tc-e/t '#t (-val #t)] [tc-e '#f #:ret (ret (-val #f) (-FS (list (make-Bot)) null))] - [tc-e/t (if #f 'a 3) -Integer] + [tc-e/t (if #f 'a 3) -Pos] [tc-e/t (if #f #f #t) (t:Un (-val #t))] [tc-e (when #f 3) -Void] [tc-e/t '() (-val '())] [tc-e/t (let: ([x : (Listof Number) '(1)]) (cond [(pair? x) 1] [(null? x) 1])) - -Integer] + -Pos] [tc-e/t (lambda: ([x : Number] . [y : Number *]) (car y)) (->* (list N) N N)] [tc-e ((lambda: ([x : Number] . [y : Number *]) (car y)) 3) N] [tc-e ((lambda: ([x : Number] . [y : Number *]) (car y)) 3 4 5) N] @@ -225,8 +228,9 @@ [tc-e/t (let: ([x : Any 3]) (if (list? x) - (begin (car x) 1) 2)) - -Integer] + (begin (car x) 1) + 2)) + -Pos] [tc-e (let: ([x : (U Number Boolean) 3]) @@ -235,7 +239,7 @@ 3)) N] - [tc-e (let ([x 1]) x) #:proc (get-let-name x 0 (-path -Integer #'x))] + [tc-e (let ([x 1]) x) #:proc (get-let-name x 0 (-path -Pos #'x))] [tc-e (let ([x 1]) (boolean? x)) #:ret (ret -Boolean (-FS (list (make-Bot)) null))] [tc-e (boolean? number?) #:ret (ret -Boolean (-FS (list (make-Bot)) null))] @@ -257,9 +261,9 @@ (if (eq? x 1) 12 14)) - -Integer] + -Pos] - [tc-e (car (append (list 1 2) (list 3 4))) -Integer] + [tc-e (car (append (list 1 2) (list 3 4))) -Pos] [tc-e (let-syntax ([a @@ -269,8 +273,8 @@ (string-append "foo" (a v)))) -String] - [tc-e (apply (plambda: (a) [x : a *] x) '(5)) (-lst -Integer)] - [tc-e (apply append (list '(1 2 3) '(4 5 6))) (-lst -Integer)] + [tc-e (apply (plambda: (a) [x : a *] x) '(5)) (-lst -Pos)] + [tc-e (apply append (list '(1 2 3) '(4 5 6))) (-lst -Pos)] [tc-err ((case-lambda: [([x : Number]) x] [([y : Number] [x : Number]) x]) @@ -306,9 +310,9 @@ [tc-e (let* ([sym 'squarf] [x (if (= 1 2) 3 sym)]) x) - #:proc (syntax-parser [(_ _ (_ ([(x) _]) _)) (-path (t:Un (-val 'squarf) -Integer) #'x)])] + #:proc (syntax-parser [(_ _ (_ ([(x) _]) _)) (-path (t:Un (-val 'squarf) -Pos) #'x)])] - [tc-e/t (if #t 1 2) -Integer] + [tc-e/t (if #t 1 2) -Pos] ;; eq? as predicate @@ -333,12 +337,12 @@ [x (if (= 1 2) 3 sym)]) (if (eq? x sym) 3 x)) #:proc (syntax-parser [(_ _ (_ ([(x) _]) _)) - (ret -Integer (-FS (list) (list (make-NotTypeFilter (-val 'squarf) null #'x) (make-TypeFilter (-val #f) null #'x))))])] + (ret -Pos (-FS (list) (list (make-NotTypeFilter (-val 'squarf) null #'x) (make-TypeFilter (-val #f) null #'x))))])] [tc-e (let* ([sym 'squarf] [x (if (= 1 2) 3 sym)]) (if (eq? sym x) 3 x)) #:proc (syntax-parser [(_ _ (_ ([(x) _]) _)) - (ret -Integer (-FS (list) (list (make-NotTypeFilter (-val 'squarf) null #'x) (make-TypeFilter (-val #f) null #'x))))])] + (ret -Pos (-FS (list) (list (make-NotTypeFilter (-val 'squarf) null #'x) (make-TypeFilter (-val #f) null #'x))))])] ;; equal? as predicate for symbols [tc-e (let: ([x : (Un 'foo Number) 'foo]) (if (equal? x 'foo) 3 x)) @@ -351,22 +355,22 @@ [x (if (= 1 2) 3 sym)]) (if (equal? x sym) 3 x)) #:proc (syntax-parser [(_ _ (_ ([(x) _]) _)) - (ret -Integer (-FS (list) (list (make-NotTypeFilter (-val 'squarf) null #'x) (make-TypeFilter (-val #f) null #'x))))])] + (ret -Pos (-FS (list) (list (make-NotTypeFilter (-val 'squarf) null #'x) (make-TypeFilter (-val #f) null #'x))))])] [tc-e (let* ([sym 'squarf] [x (if (= 1 2) 3 sym)]) (if (equal? sym x) 3 x)) #:proc (syntax-parser [(_ _ (_ ([(x) _]) _)) - (ret -Integer (-FS (list) (list (make-NotTypeFilter (-val 'squarf) null #'x) (make-TypeFilter (-val #f) null #'x))))])] + (ret -Pos (-FS (list) (list (make-NotTypeFilter (-val 'squarf) null #'x) (make-TypeFilter (-val #f) null #'x))))])] [tc-e (let: ([x : (Listof Symbol)'(a b c)]) (cond [(memq 'a x) => car] [else 'foo])) Sym] - [tc-e (list 1 2 3) (-lst* -Integer -Integer -Integer)] - [tc-e (list 1 2 3 'a) (-lst* -Integer -Integer -Integer (-val 'a))] - #; - [tc-e `(1 2 ,(+ 3 4)) (-lst* N N N)] + [tc-e (list 1 2 3) (-lst* -Pos -Pos -Pos)] + [tc-e (list 1 2 3 'a) (-lst* -Pos -Pos -Pos (-val 'a))] + + [tc-e `(1 2 ,(+ 3 4)) (-lst* -Pos -Pos -Pos)] [tc-e (let: ([x : Any 1]) (when (and (list? x) (not (null? x))) @@ -385,7 +389,7 @@ 'foo)) (t:Un (-val 'foo) (-pair Univ (-lst Univ)))] - [tc-e (cadr (cadr (list 1 (list 1 2 3) 3))) -Integer] + [tc-e (cadr (cadr (list 1 (list 1 2 3) 3))) -Pos] @@ -400,7 +404,7 @@ [tc-e/t (let: ([x : Any 3]) (if (and (list? x) (not (null? x))) (begin (car x) 1) 2)) - -Integer] + -Pos] ;; set! tests [tc-e (let: ([x : Any 3]) @@ -457,7 +461,7 @@ [tc-e/t (let* ([z 1] [p? (lambda: ([x : Any]) (number? z))]) (lambda: ([x : Any]) (if (p? x) 11 12))) - (t:-> Univ -Integer : (-LFS null (list (make-LBot))))] + (t:-> Univ -Pos : (-LFS null (list (make-LBot))))] [tc-e/t (let* ([z 1] [p? (lambda: ([x : Any]) (number? z))]) (lambda: ([x : Any]) (if (p? x) x 12))) @@ -469,7 +473,7 @@ [tc-e/t (let* ([z 1] [p? (lambda: ([x : Any]) (not (number? z)))]) (lambda: ([x : Any]) (if (p? x) x 12))) - (t:-> Univ -Integer : (-LFS null (list (make-LBot))))] + (t:-> Univ -Pos : (-LFS null (list (make-LBot))))] [tc-e/t (let* ([z 1] [p? (lambda: ([x : Any]) z)]) (lambda: ([x : Any]) (if (p? x) x 12))) @@ -500,7 +504,7 @@ ;; w-c-m [tc-e/t (with-continuation-mark 'key 'mark 3) - -Integer] + -Pos] [tc-err (with-continuation-mark (5 4) 1 3)] [tc-err (with-continuation-mark 1 (5 4) @@ -529,14 +533,14 @@ [tc-err (call-with-values (lambda () (values 2 1)) (lambda: ([x : String] [y : Number]) (+ x y)))] ;; quote-syntax - [tc-e/t #'3 (-Syntax -Integer)] - [tc-e/t #'(1 2 3) (-Syntax (-lst* -Integer -Integer -Integer))] + [tc-e/t #'3 (-Syntax -Pos)] + [tc-e/t #'(1 2 3) (-Syntax (-lst* -Pos -Pos -Pos))] ;; testing some primitives [tc-e (let ([app apply] [f (lambda: [x : Number *] 3)]) (app f (list 1 2 3))) - -Integer] + -Pos] [tc-e ((lambda () (call/cc (lambda: ([k : (Number -> (U))]) (if (read) 5 (k 10)))))) N] @@ -565,7 +569,7 @@ (define y 2) (define z (+ x y)) (* x z)) - -Integer] + -Pos] [tc-e/t (let () (define: (f [x : Number]) : Number @@ -574,7 +578,7 @@ (+ z w))) (g 4)) 5) - -Integer] + -Pos] [tc-err (let () (define x x) @@ -605,11 +609,11 @@ [tc-e/t (if #f 1 'foo) (-val 'foo)] - [tc-e (list* 1 2 3) (-pair -Integer (-pair -Integer -Integer))] + [tc-e (list* 1 2 3) (-pair -Pos (-pair -Pos -Pos))] [tc-err (apply append (list 1) (list 2) (list 3) (list (list 1) "foo"))] - [tc-e (apply append (list 1) (list 2) (list 3) (list (list 1) (list 1))) (-lst -Integer)] - [tc-e (apply append (list 1) (list 2) (list 3) (list (list 1) (list "foo"))) (-lst (t:Un -String -Integer))] + [tc-e (apply append (list 1) (list 2) (list 3) (list (list 1) (list 1))) (-lst -Pos)] + [tc-e (apply append (list 1) (list 2) (list 3) (list (list 1) (list "foo"))) (-lst (t:Un -String -Pos))] [tc-err (plambda: (b ...) [y : b ... b] (apply append (map list y)))] [tc-e/t (plambda: (b ...) [y : (Listof Integer) ... b] (apply append y)) (-polydots (b) (->... (list) ((-lst -Integer) b) (-lst -Integer)))] @@ -636,12 +640,12 @@ ;; instantiating dotted terms [tc-e/t (inst (plambda: (a ...) [xs : a ... a] 3) Integer Boolean Integer) - (-Integer B -Integer . t:-> . -Integer : (-LFS null (list (make-LBot))))] + (-Integer B -Integer . t:-> . -Pos : (-LFS null (list (make-LBot))))] [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:-> . -Integer : (-LFS null (list (make-LBot))))] + . t:-> . -Pos : (-LFS null (list (make-LBot))))] [tc-e/t (plambda: (z x y ...) () (inst map z x y ... y)) (-polydots (z x y) (t:-> ((list ((list x) (y y) . ->... . z) (-lst x)) ((-lst y) y) . ->... . (-lst z))))] @@ -724,7 +728,7 @@ [tc-e/t (ann (lambda (x) x) (All (a) (a -> a))) (-poly (a) (a . t:-> . a))] - [tc-e (apply values (list 1 2 3)) #:ret (ret (list -Integer -Integer -Integer))] + [tc-e (apply values (list 1 2 3)) #:ret (ret (list -Pos -Pos -Pos))] [tc-e/t (ann (if #t 3 "foo") Integer) -Integer] @@ -749,10 +753,10 @@ ) (test-suite "tc-literal tests" - (tc-l 5 -Integer) - (tc-l 5# N) - (tc-l 5.0 N) - (tc-l 5.1 N) + (tc-l 5 -ExactPositiveInteger) + (tc-l 5# -Flonum) + (tc-l 5.0 -Flonum) + (tc-l 5.1 -Flonum) (tc-l #t (-val #t)) (tc-l "foo" -String) (tc-l foo (-val 'foo)) diff --git a/collects/typed-scheme/private/base-env-numeric.ss b/collects/typed-scheme/private/base-env-numeric.ss index 682cb7a2..daf138b7 100644 --- a/collects/typed-scheme/private/base-env-numeric.ss +++ b/collects/typed-scheme/private/base-env-numeric.ss @@ -11,19 +11,31 @@ scheme/promise scheme/system (only-in string-constants/private/only-once maybe-print-message) (only-in scheme/match/runtime match:error matchable? match-equality-test) - (for-syntax (only-in (types abbrev) [-Number N] [-Boolean B] [-Symbol Sym]))) + (for-syntax (only-in (types abbrev) [-Number N] [-Boolean B] [-Symbol Sym] [-Real R]))) ;; numeric operations [modulo (cl->* (-Integer -Integer . -> . -Integer))] [= (->* (list N N) N B)] -[>= (->* (list N N) N B)] -[< (->* (list N N) N B)] -[<= (->* (list N N) N B)] -[> (->* (list N N) N B)] +[>= (->* (list R R) R B)] +[< (->* (list R R) R B)] +[<= (->* (list R R) R B)] +[> (->* (list R R) R B)] [zero? (N . -> . B)] -[* (cl->* (->* '() -Integer -Integer) (->* '() N N))] +[* (cl->* (->* '() -ExactPositiveInteger -ExactPositiveInteger) + (->* '() -Nat -Nat) + (->* '() -Integer -Integer) + (->* '() -ExactRational -ExactRational) + ;; Reals are just Rat + Int + (->* '() -Real -Flonum) + (->* '() N N))] [/ (cl->* (->* (list N) N N))] -[+ (cl->* (->* '() -Integer -Integer) (->* '() N N))] +[+ (cl->* (->* '() -ExactPositiveInteger -ExactPositiveInteger) + (->* '() -Nat -Nat) + (->* '() -Integer -Integer) + (->* '() -ExactRational -ExactRational) + ;; Reals are just Rat + Int + (->* '() -Real -Flonum) + (->* '() N N))] [- (cl->* (->* (list -Integer) -Integer -Integer) (->* (list N) N N))] [max (cl->* (->* (list -Integer) -Integer -Integer) (->* (list N) N N))] diff --git a/collects/typed-scheme/typecheck/tc-expr-unit.ss b/collects/typed-scheme/typecheck/tc-expr-unit.ss index 85a5b9d8..0cbdb44b 100644 --- a/collects/typed-scheme/typecheck/tc-expr-unit.ss +++ b/collects/typed-scheme/typecheck/tc-expr-unit.ss @@ -36,7 +36,7 @@ [(~var i (3d exact-positive-integer?)) -ExactPositiveInteger] [(~var i (3d exact-nonnegative-integer?)) -ExactNonnegativeInteger] [(~var i (3d exact-integer?)) -Integer] - [(~var i (3d (lambda (e) (and (exact? e) (rational? e))))) -ExactRational] + [(~var i (3d (lambda (e) (and (number? e) (exact? e) (rational? e))))) -ExactRational] [(~var i (3d inexact-real?)) -Flonum] [(~var i (3d real?)) -Real] [(~var i (3d number?)) -Number] diff --git a/collects/typed-scheme/types/abbrev.ss b/collects/typed-scheme/types/abbrev.ss index 164483b0..0a390beb 100644 --- a/collects/typed-scheme/types/abbrev.ss +++ b/collects/typed-scheme/types/abbrev.ss @@ -113,7 +113,7 @@ (define -Flonum (make-Base 'Flonum #'inexact-real?)) (define -ExactRational - (make-Base 'Exact-Rational #'(and/c rational? exact?))) + (make-Base 'Exact-Rational #'(and/c number? rational? exact?))) (define -Integer (make-Base 'Integer #'exact-integer?)) (define -ExactPositiveInteger (make-Base 'Exact-Positive-Integer #'exact-positive-integer?)) diff --git a/collects/typed-scheme/types/convenience.ss b/collects/typed-scheme/types/convenience.ss index 70dce20c..f281022b 100644 --- a/collects/typed-scheme/types/convenience.ss +++ b/collects/typed-scheme/types/convenience.ss @@ -30,6 +30,7 @@ (let loop ([t* t]) (match t* [(Value: '()) (-lst Univ)] + [(Value: 0) -Nat] [(Mu: var (Union: (list (Value: '()) (Pair: _ (F: var))))) t*] [(Pair: t1 (Value: '())) (-lst t1)] [(Pair: t1 t2) diff --git a/collects/typed-scheme/types/subtype.ss b/collects/typed-scheme/types/subtype.ss index 04de5214..a2e961e3 100644 --- a/collects/typed-scheme/types/subtype.ss +++ b/collects/typed-scheme/types/subtype.ss @@ -228,6 +228,11 @@ [((Base: 'Exact-Rational _) (Base: 'Number _)) A0] [((Base: 'Exact-Positive-Integer _) (Base: 'Exact-Rational _)) A0] [((Base: 'Exact-Positive-Integer _) (Base: 'Number _)) A0] + [((Base: 'Exact-Positive-Integer _) (Base: 'Exact-Nonnegative-Integer _)) A0] + [((Base: 'Exact-Positive-Integer _) (Base: 'Integer _)) A0] + [((Base: 'Exact-Nonnegative-Integer _) (Base: 'Number _)) A0] + [((Base: 'Exact-Nonnegative-Integer _) (Base: 'Exact-Rational _)) A0] + [((Base: 'Exact-Nonnegative-Integer _) (Base: 'Integer _)) A0] ;; values are subtypes of their "type" [((Value: (? integer? n)) (Base: 'Integer _)) A0] From 7d85ae8997fa79fa7d982459ef72fe5a3a22f439 Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Fri, 20 Nov 2009 05:20:23 +0000 Subject: [PATCH 04/17] checkpoint svn: r16915 original commit: 485c8a356708bb1f59c942529dd77bd455a6c82d --- .../unit-tests/parse-type-tests.ss | 4 +- .../unit-tests/typecheck-tests.ss | 4 +- collects/typed-scheme/main.ss | 4 +- .../typed-scheme/private/base-env-numeric.ss | 49 +++++++++++++------ .../typed-scheme/private/base-types-new.ss | 45 +++++++++++++++++ collects/typed-scheme/private/base-types.ss | 2 +- .../typed-scheme/private/type-contract.ss | 2 +- .../typed-scheme/typecheck/tc-expr-unit.ss | 24 +++++++-- 8 files changed, 108 insertions(+), 26 deletions(-) create mode 100644 collects/typed-scheme/private/base-types-new.ss diff --git a/collects/tests/typed-scheme/unit-tests/parse-type-tests.ss b/collects/tests/typed-scheme/unit-tests/parse-type-tests.ss index f88298c9..a62938aa 100644 --- a/collects/tests/typed-scheme/unit-tests/parse-type-tests.ss +++ b/collects/tests/typed-scheme/unit-tests/parse-type-tests.ss @@ -5,8 +5,8 @@ (rep type-rep) (rename-in (types comparison subtype union utils convenience) [Un t:Un] [-> t:->]) - (private base-types base-types-extra colon) - (for-template (private base-types base-types-extra base-env colon)) + (private base-types-new base-types-extra colon) + (for-template (private base-types-new base-types-extra base-env colon)) (private parse-type) (schemeunit)) diff --git a/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss b/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss index e3b2e210..a9e1d062 100644 --- a/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss +++ b/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss @@ -19,7 +19,7 @@ (typecheck typechecker) (env type-env) (private base-env)) - (for-template (private base-env base-types base-types-extra))) + (for-template (private base-env base-types-new base-types-extra))) (require (for-syntax syntax/kerncase syntax/parse)) @@ -255,7 +255,7 @@ [tc-err (5 4)] [tc-err (apply 5 '(2))] [tc-err (map (lambda: ([x : Any] [y : Any]) 1) '(1))] - [tc-e (map add1 '(1)) (-lst -Integer)] + [tc-e (map add1 '(1)) (-lst -Pos)] [tc-e/t (let ([x 5]) (if (eq? x 1) diff --git a/collects/typed-scheme/main.ss b/collects/typed-scheme/main.ss index e2f553da..d6fee54a 100644 --- a/collects/typed-scheme/main.ss +++ b/collects/typed-scheme/main.ss @@ -2,7 +2,7 @@ -(providing (libs (except scheme/base #%module-begin #%top-interaction with-handlers lambda #%app) +(providing (libs (except scheme/base #%module-begin #%top-interaction with-handlers number? lambda #%app) (except "private/prims.ss") (except "private/base-types.ss") (except "private/base-types-extra.ss")) @@ -12,5 +12,5 @@ #%app)) (require "private/base-env.ss" "private/base-special-env.ss" (for-syntax "private/base-types-extra.ss")) -(provide (rename-out [with-handlers: with-handlers]) +(provide (rename-out [with-handlers: with-handlers] [real? number?]) (for-syntax (all-from-out "private/base-types-extra.ss"))) diff --git a/collects/typed-scheme/private/base-env-numeric.ss b/collects/typed-scheme/private/base-env-numeric.ss index daf138b7..1f96254c 100644 --- a/collects/typed-scheme/private/base-env-numeric.ss +++ b/collects/typed-scheme/private/base-env-numeric.ss @@ -11,7 +11,7 @@ scheme/promise scheme/system (only-in string-constants/private/only-once maybe-print-message) (only-in scheme/match/runtime match:error matchable? match-equality-test) - (for-syntax (only-in (types abbrev) [-Number N] [-Boolean B] [-Symbol Sym] [-Real R]))) + (for-syntax (only-in (types abbrev) [-Number N] [-Boolean B] [-Symbol Sym] [-Real R] [-ExactPositiveInteger -Pos]))) ;; numeric operations [modulo (cl->* (-Integer -Integer . -> . -Integer))] @@ -25,18 +25,26 @@ (->* '() -Nat -Nat) (->* '() -Integer -Integer) (->* '() -ExactRational -ExactRational) - ;; Reals are just Rat + Int - (->* '() -Real -Flonum) + (->* '() -Flonum -Flonum) + (->* '() -Real -Real) (->* '() N N))] -[/ (cl->* (->* (list N) N N))] +[/ (cl->* (->* (list -Integer) -Integer -ExactRational) + (->* (list -ExactRational) -ExactRational -ExactRational) + (->* (list -Flonum) -Flonum -Flonum) + (->* (list -Real) -Real -Real) + (->* (list N) N N))] [+ (cl->* (->* '() -ExactPositiveInteger -ExactPositiveInteger) (->* '() -Nat -Nat) (->* '() -Integer -Integer) (->* '() -ExactRational -ExactRational) - ;; Reals are just Rat + Int - (->* '() -Real -Flonum) + (->* '() -Flonum -Flonum) + (->* '() -Real -Real) (->* '() N N))] -[- (cl->* (->* (list -Integer) -Integer -Integer) (->* (list N) N N))] +[- (cl->* (->* (list -Integer) -Integer -Integer) + (->* (list -ExactRational) -ExactRational -ExactRational) + (->* (list -Flonum) -Flonum -Flonum) + (->* (list -Real) -Real -Real) + (->* (list N) N N))] [max (cl->* (->* (list -Integer) -Integer -Integer) (->* (list N) N N))] [min (cl->* (->* (list -Integer) -Integer -Integer) @@ -45,9 +53,18 @@ [negative? (-> N B)] [odd? (-> -Integer B)] [even? (-> -Integer B)] -[add1 (cl->* (-> -Integer -Integer) +[add1 (cl->* (-> -Pos -Pos) + (-> -Nat -Nat) + (-> -Integer -Integer) + (-> -ExactRational -ExactRational) + (-> -Flonum -Flonum) + (-> -Real -Real) (-> N N))] -[sub1 (cl->* (-> -Integer -Integer) +[sub1 (cl->* (-> -Pos -Nat) + (-> -Integer -Integer) + (-> -ExactRational -ExactRational) + (-> -Flonum -Flonum) + (-> -Real -Real) (-> N N))] [quotient (-Integer -Integer . -> . -Integer)] [remainder (-Integer -Integer . -> . -Integer)] @@ -56,16 +73,20 @@ [exact? (N . -> . B)] [inexact? (N . -> . B)] -[exact->inexact (N . -> . N)] -[inexact->exact (N . -> . N)] +[exact->inexact (cl->* + (-Real . -> . -Flonum) + (N . -> . N))] +[inexact->exact (cl->* + (-Real . -> . -ExactRational) + (N . -> . N))] [number? (make-pred-ty N)] [integer? (Univ . -> . B : (-LFS (list (-filter N)) (list (-not-filter -Integer))))] [exact-integer? (make-pred-ty -Integer)] -[real? (Univ . -> . B : (-LFS (list (-filter N)) (list)))] -[complex? (Univ . -> . B : (-LFS (list (-filter N)) (list)))] -[rational? (Univ . -> . B : (-LFS (list (-filter N)) (list)))] +[real? (make-pred-ty -Real)] +[complex? (make-pred-ty N)] +[rational? (make-pred-ty -Real)] [floor (-> N N)] [ceiling (-> N N)] [truncate (-> N N)] diff --git a/collects/typed-scheme/private/base-types-new.ss b/collects/typed-scheme/private/base-types-new.ss new file mode 100644 index 00000000..bd9a6089 --- /dev/null +++ b/collects/typed-scheme/private/base-types-new.ss @@ -0,0 +1,45 @@ +#lang s-exp "type-env-lang.ss" + +[Number -Number] +[Complex -Number] +[Integer -Integer] +[Real -Real] +[Exact-Rational -ExactRational] +[Flonum -Flonum] +[Exact-Positive-Integer -ExactPositiveInteger] +[Exact-Nonnegative-Integer -ExactNonnegativeInteger] +[Natural -ExactNonnegativeInteger] + +[Void -Void] +[Boolean -Boolean] +[Symbol -Symbol] +[String -String] +[Any Univ] +[Port -Port] +[Path -Path] +[Path-String -Pathlike] +[Regexp -Regexp] +[PRegexp -PRegexp] +[Char -Char] +[Namespace -Namespace] +[Input-Port -Input-Port] +[Output-Port -Output-Port] +[Bytes -Bytes] +[EOF (-val eof)] +[Sexpof (-poly (a) (-Sexpof a))] ;; recursive union of sexps with a +[Syntaxof (-poly (a) (-Syntax a))] ;; syntax-e yields a +[Syntax-E In-Syntax] ;; possible results of syntax-e on "2D" syntax +[Syntax Any-Syntax] ;; (Syntaxof Syntax-E): "2D" syntax +[Datum Syntax-Sexp] ;; (Sexpof Syntax), datum->syntax yields "2D" syntax +[Sexp -Sexp] ;; (Sexpof (U)), syntax->datum of "2D" syntax +[Identifier Ident] +[Procedure top-func] +[Keyword -Keyword] +[Listof -Listof] +[Vectorof (-poly (a) (make-Vector a))] +[Option (-poly (a) (-opt a))] +[HashTable (-poly (a b) (-HT a b))] +[Promise (-poly (a) (-Promise a))] +[Pair (-poly (a b) (-pair a b))] +[Boxof (-poly (a) (make-Box a))] +[Continuation-Mark-Set -Cont-Mark-Set] diff --git a/collects/typed-scheme/private/base-types.ss b/collects/typed-scheme/private/base-types.ss index bd9a6089..99719989 100644 --- a/collects/typed-scheme/private/base-types.ss +++ b/collects/typed-scheme/private/base-types.ss @@ -1,6 +1,6 @@ #lang s-exp "type-env-lang.ss" -[Number -Number] +[Number -Real] [Complex -Number] [Integer -Integer] [Real -Real] diff --git a/collects/typed-scheme/private/type-contract.ss b/collects/typed-scheme/private/type-contract.ss index 0d8806c7..6e348b96 100644 --- a/collects/typed-scheme/private/type-contract.ss +++ b/collects/typed-scheme/private/type-contract.ss @@ -57,7 +57,7 @@ [(Mu: var (Union: (list (Value: '()) (Pair: elem-ty (F: var))))) #`(listof #,(t->c elem-ty))] [(? (lambda (e) (eq? t:Any-Syntax e))) #'syntax?] - [(Base: sym cnt) cnt] + [(Base: sym cnt) #`(flat-named-contract '#,sym (flat-contract-predicate #,cnt))] [(Refinement: par p? cert) #`(and/c #,(t->c par) (flat-contract #,(cert p?)))] [(Union: elems) diff --git a/collects/typed-scheme/typecheck/tc-expr-unit.ss b/collects/typed-scheme/typecheck/tc-expr-unit.ss index 0cbdb44b..a1af3449 100644 --- a/collects/typed-scheme/typecheck/tc-expr-unit.ss +++ b/collects/typed-scheme/typecheck/tc-expr-unit.ss @@ -47,10 +47,26 @@ [i:byte-pregexp -Byte-PRegexp] [i:byte-regexp -Byte-Regexp] [i:regexp -Regexp] - [(i ...) - (-Tuple (map tc-literal (syntax->list #'(i ...))))] - [i #:declare i (3d vector?) - (make-Vector (apply Un (map tc-literal (vector->list (syntax-e #'i)))))] + [(i ...) + (match expected + [(Mu: var (Union: (list (Value: '()) (Pair: elem-ty (F: var))))) + (-Tuple + (for/list ([l (in-list (syntax->list #'(i ...)))]) + (tc-literal l elem-ty)))] + ;; errors are handled elsewhere + [_ (-Tuple + (for/list ([l (in-list (syntax->list #'(i ...)))]) + (tc-literal l #f)))])] + [(~var i (3d vector?)) + (match expected + [(Vector: t) + (make-Vector (apply Un + (for/list ([l (syntax-e #'i)]) + (tc-literal l t))))] + ;; errors are handled elsewhere + [_ (make-Vector (apply Un + (for/list ([l (syntax-e #'i)]) + (tc-literal l #f))))])] [_ Univ])) From 28890f267f6e790f4d7a4af57bb2294eb4c14aa3 Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Fri, 20 Nov 2009 15:20:23 +0000 Subject: [PATCH 05/17] Skip backup files in tests. More specific numeric types. More subtyping relationships. svn: r16922 original commit: 6497745560505fc1366188909543031b2925e0bb --- collects/tests/typed-scheme/main.ss | 4 +- .../typed-scheme/private/base-env-numeric.ss | 64 +++++++++---------- collects/typed-scheme/types/subtype.ss | 14 ++-- 3 files changed, 43 insertions(+), 39 deletions(-) diff --git a/collects/tests/typed-scheme/main.ss b/collects/tests/typed-scheme/main.ss index 2b223600..74d68762 100644 --- a/collects/tests/typed-scheme/main.ss +++ b/collects/tests/typed-scheme/main.ss @@ -46,7 +46,9 @@ (define path (build-path (this-expression-source-directory) dir)) (define tests (for/list ([p (directory-list path)] - #:when (scheme-file? p)) + #:when (scheme-file? p) + ;; skip backup files + #:when (not (regexp-match #rx".*~" (path->string p)))) (test-case (path->string p) (test diff --git a/collects/typed-scheme/private/base-env-numeric.ss b/collects/typed-scheme/private/base-env-numeric.ss index 1f96254c..55eb34f7 100644 --- a/collects/typed-scheme/private/base-env-numeric.ss +++ b/collects/typed-scheme/private/base-env-numeric.ss @@ -20,35 +20,25 @@ [< (->* (list R R) R B)] [<= (->* (list R R) R B)] [> (->* (list R R) R B)] -[zero? (N . -> . B)] -[* (cl->* (->* '() -ExactPositiveInteger -ExactPositiveInteger) - (->* '() -Nat -Nat) - (->* '() -Integer -Integer) - (->* '() -ExactRational -ExactRational) - (->* '() -Flonum -Flonum) - (->* '() -Real -Real) - (->* '() N N))] -[/ (cl->* (->* (list -Integer) -Integer -ExactRational) - (->* (list -ExactRational) -ExactRational -ExactRational) - (->* (list -Flonum) -Flonum -Flonum) - (->* (list -Real) -Real -Real) - (->* (list N) N N))] -[+ (cl->* (->* '() -ExactPositiveInteger -ExactPositiveInteger) - (->* '() -Nat -Nat) - (->* '() -Integer -Integer) - (->* '() -ExactRational -ExactRational) - (->* '() -Flonum -Flonum) - (->* '() -Real -Real) - (->* '() N N))] -[- (cl->* (->* (list -Integer) -Integer -Integer) - (->* (list -ExactRational) -ExactRational -ExactRational) - (->* (list -Flonum) -Flonum -Flonum) - (->* (list -Real) -Real -Real) - (->* (list N) N N))] -[max (cl->* (->* (list -Integer) -Integer -Integer) - (->* (list N) N N))] -[min (cl->* (->* (list -Integer) -Integer -Integer) - (->* (list N) N N))] +[zero? (make-pred-ty (list N) B -Zero)] +[* (apply cl->* + (for/list ([t (list -Pos -Nat -Integer -ExactRational -Flonum -Real N)]) + (->* (list) t t)))] +[/ (apply cl->* + (for/list ([t (list -Integer -ExactRational -Flonum -Real N)]) + (->* (list t) t t)))] +[+ (apply cl->* + (for/list ([t (list -Pos -Nat -Integer -ExactRational -Flonum -Real N)]) + (->* (list) t t)))] +[- (apply cl->* + (for/list ([t (list -Integer -ExactRational -Flonum -Real N)]) + (->* (list t) t t)))] +[max (apply cl->* + (for/list ([t (list -Pos -Nat -Integer -ExactRational -Flonum -Real N)]) + (->* (list t) t t)))] +[min (apply cl->* + (for/list ([t (list -Pos -Nat -Integer -ExactRational -Flonum -Real N)]) + (->* (list t) t t)))] [positive? (-> N B)] [negative? (-> N B)] [odd? (-> -Integer B)] @@ -100,8 +90,12 @@ [denominator (N . -> . -Integer)] [rationalize (N N . -> . N)] [expt (cl->* (-Integer -Integer . -> . -Integer) (N N . -> . N))] -[sqrt (N . -> . N)] -[log (N . -> . N)] +[sqrt (cl->* + (-Real . -> . -Real) + (N . -> . N))] +[log (cl->* + (-Pos . -> . -Real) + (N . -> . N))] [exp (N . -> . N)] [cos (N . -> . N)] [sin (N . -> . N)] @@ -118,7 +112,13 @@ [sgn (-Real . -> . -Real)] [pi N] -[sqr (N . -> . N)] +[sqr (cl->* (-> -Pos -Pos) + (-> -Nat -Nat) + (-> -Integer -Integer) + (-> -ExactRational -ExactRational) + (-> -Flonum -Flonum) + (-> -Real -Real) + (-> N N))] [sgn (N . -> . N)] [conjugate (N . -> . N)] [sinh (N . -> . N)] diff --git a/collects/typed-scheme/types/subtype.ss b/collects/typed-scheme/types/subtype.ss index a2e961e3..be894406 100644 --- a/collects/typed-scheme/types/subtype.ss +++ b/collects/typed-scheme/types/subtype.ss @@ -226,17 +226,19 @@ [((Base: 'Integer _) (== -Real type-equal?)) 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 _) (Base: 'Exact-Nonnegative-Integer _)) A0] + [((Base: 'Exact-Positive-Integer _) (== -Nat type-equal?)) A0] [((Base: 'Exact-Positive-Integer _) (Base: 'Integer _)) A0] - [((Base: 'Exact-Nonnegative-Integer _) (Base: 'Number _)) A0] - [((Base: 'Exact-Nonnegative-Integer _) (Base: 'Exact-Rational _)) A0] - [((Base: 'Exact-Nonnegative-Integer _) (Base: 'Integer _)) A0] + [((== -Nat type-equal?) (Base: 'Number _)) A0] + [((== -Nat type-equal?) (Base: 'Exact-Rational _)) A0] + [((== -Nat type-equal?) (Base: 'Integer _)) A0] ;; values are subtypes of their "type" - [((Value: (? integer? n)) (Base: 'Integer _)) A0] - [((Value: (? exact-nonnegative-integer? n)) (Base: 'Exact-Nonnegative-Integer _)) A0] + [((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-positive-integer? n)) (Base: 'Exact-Positive-Integer _)) A0] [((Value: (? inexact-real? n)) (Base: 'Flonum _)) A0] [((Value: (? real? n)) (== -Real type-equal?)) A0] From e5c1d9e02b59a47fdaaf8386a46611d1fb2e240f Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Sat, 21 Nov 2009 00:11:37 +0000 Subject: [PATCH 06/17] checkpoint svn: r16931 original commit: 750c971d0727b495c55fb090e38d3fb3001d3624 --- .../tests/typed-scheme/fail/back-and-forth.ss | 4 +- .../tests/typed-scheme/succeed/metrics.ss | 18 +- .../tests/typed-scheme/succeed/new-metrics.ss | 14 +- .../tests/typed-scheme/succeed/random-bits.ss | 2 +- .../typed-scheme/private/base-env-numeric.ss | 123 ++++++---- collects/typed-scheme/private/base-env.ss | 211 +++++++----------- .../typed-scheme/private/base-types-new.ss | 5 +- collects/typed-scheme/private/env-lang.ss | 31 +-- collects/typed-scheme/rep/type-rep.ss | 5 + collects/typed-scheme/types/abbrev.ss | 1 + collects/typed-scheme/utils/tc-utils.ss | 6 +- collects/typed/framework/framework.ss | 4 +- collects/typed/mred/mred.ss | 2 +- collects/typed/scheme/base.ss | 2 +- collects/typed/scheme/base/lang/reader.ss | 2 +- collects/typed/scheme/lang/reader.ss | 2 +- 16 files changed, 208 insertions(+), 224 deletions(-) diff --git a/collects/tests/typed-scheme/fail/back-and-forth.ss b/collects/tests/typed-scheme/fail/back-and-forth.ss index f8c00930..023eaf60 100644 --- a/collects/tests/typed-scheme/fail/back-and-forth.ss +++ b/collects/tests/typed-scheme/fail/back-and-forth.ss @@ -1,9 +1,9 @@ #; -(exn-pred exn:fail:contract? #rx".*contract.*\\(-> number\\? number\\?\\).*") +(exn-pred exn:fail:contract? #rx".*contract.*\\(-> Number Number\\).*") #lang scheme/load -(module m typed-scheme +(module m typed/scheme (: f (Number -> Number)) (define (f x) (add1 x)) (provide f)) diff --git a/collects/tests/typed-scheme/succeed/metrics.ss b/collects/tests/typed-scheme/succeed/metrics.ss index ad067480..7918168a 100644 --- a/collects/tests/typed-scheme/succeed/metrics.ss +++ b/collects/tests/typed-scheme/succeed/metrics.ss @@ -84,11 +84,11 @@ [table `((,a-hits ,b-hits) (,a-misses ,b-misses))] - [expected (lambda: ([i : Integer] [j : Integer]) + [expected (lambda: ([i : Natural] [j : Natural]) (/ (* (row-total i table) (col-total j table)) total-subjects))]) (exact->inexact (table-sum - (lambda: ([i : Integer] [j : Integer]) + (lambda: ([i : Natural] [j : Natural]) (/ (sqr (- (expected i j) (table-ref i j table))) (expected i j))) table))))) @@ -473,7 +473,7 @@ (show result )))) ;; applies only to the combined metric [or more generally to listof-answer results] -(pdefine: (a b c) (total [experiment-number : Integer] [result : (Result (Listof number) b c)]) : (Listof number) +(pdefine: (a b c) (total [experiment-number : Natural] [result : (Result (Listof number) b c)]) : (Listof number) (define: (total/s [s : Table]) : number (apply + (list-ref (pivot s) experiment-number))) (list (total/s (result-seqA result)) (total/s (result-seqB result)))) @@ -491,7 +491,7 @@ [(null? l) '()] [else (let ([n (length (car l))]) - (build-list n (lambda: ([i : Integer]) (map (lambda: ([j : (Listof X)]) (list-ref j i)) l))))])) + (build-list n (lambda: ([i : Natural]) (map (lambda: ([j : (Listof X)]) (list-ref j i)) l))))])) (define: (sqr [x : number]) : number (* x x)) (define: (variance [xs : (Listof number)]): number @@ -499,16 +499,16 @@ (/ (apply + (map (lambda: ([x : number]) (sqr (- x avg))) xs)) (sub1 (length xs))))) -(define: (table-ref [i : Integer] [j : Integer] [table : Table]): number +(define: (table-ref [i : Natural] [j : Natural] [table : Table]): number (list-ref (list-ref table i) j)) -(define: (row-total [i : Integer] [table : Table]) : number +(define: (row-total [i : Natural] [table : Table]) : number (apply + (list-ref table i))) -(define: (col-total [j : Integer] [table : Table]) : number +(define: (col-total [j : Natural] [table : Table]) : number (apply + (map (lambda: ([x : (Listof number)]) (list-ref x j)) table))) -(define: (table-sum [f : (Integer Integer -> number)] [table : Table]) : number +(define: (table-sum [f : (Natural Natural -> Real)] [table : Table]) : number (let ([rows (length table)] [cols (length (car table))]) - (let: loop : number ([i : Integer 0] [j : Integer 0] [sum : number 0]) + (let loop ([i 0] [j 0] [#{sum : Real} 0]) (cond [(>= j cols) sum] [(>= i rows) (loop 0 (add1 j) sum)] diff --git a/collects/tests/typed-scheme/succeed/new-metrics.ss b/collects/tests/typed-scheme/succeed/new-metrics.ss index cb1218a5..a621fa9d 100644 --- a/collects/tests/typed-scheme/succeed/new-metrics.ss +++ b/collects/tests/typed-scheme/succeed/new-metrics.ss @@ -61,7 +61,7 @@ [table `((,a-hits ,b-hits) (,a-misses ,b-misses))] - [expected (λ: ([i : Integer] [j : Integer]) + [expected (λ: ([i : Natural] [j : Natural]) (/ (* (row-total i table) (col-total j table)) total-subjects))]) (exact->inexact (table-sum @@ -425,7 +425,7 @@ (show result)))) ;; applies only to the combined metric [or more generally to listof-answer results] -(: total (All (b c) (Integer (result (Listof Number) b c) -> (Listof Number)))) +(: total (All (b c) (Natural (result (Listof Number) b c) -> (Listof Number)))) (define (total experiment-number result) (: total/s (Table -> Number)) (define (total/s s) (apply + (list-ref (pivot s) experiment-number))) @@ -447,7 +447,7 @@ [(null? l) '()] [else (let ([n (length (car l))]) - (build-list n (λ: ([i : Integer]) (map (λ: ([j : (Listof X)]) (list-ref j i)) l))))])) + (build-list n (λ: ([i : Natural]) (map (λ: ([j : (Listof X)]) (list-ref j i)) l))))])) (: variance ((Listof Number) -> Number)) (define (variance xs) @@ -455,16 +455,16 @@ (/ (apply + (map (λ: ([x : Number]) (sqr (- x avg))) xs)) (sub1 (length xs))))) -(: table-ref (Integer Integer Table -> Number)) +(: table-ref (Natural Natural Table -> Number)) (define (table-ref i j table) (list-ref (list-ref table i) j)) -(: row-total (Integer Table -> Number)) +(: row-total (Natural Table -> Number)) (define (row-total i table) (apply + (list-ref table i))) -(: col-total (Integer Table -> Number)) +(: col-total (Natural Table -> Number)) (define (col-total j table) (apply + (map (λ: ([x : (Listof Number)]) (list-ref x j)) table))) -(: table-sum ((Integer Integer -> Number) Table -> Number)) +(: table-sum ((Natural Natural -> Number) Table -> Number)) (define (table-sum f table) (let ([rows (length table)] [cols (length (car table))]) diff --git a/collects/tests/typed-scheme/succeed/random-bits.ss b/collects/tests/typed-scheme/succeed/random-bits.ss index eea51558..d6f1ba20 100644 --- a/collects/tests/typed-scheme/succeed/random-bits.ss +++ b/collects/tests/typed-scheme/succeed/random-bits.ss @@ -351,7 +351,7 @@ (define: w-sqr1 : Nb 209) ; w^2 mod m1 (define: w-sqr2 : Nb 22853) ; w^2 mod m2 - (define: (lc [i0 : Nb] [i1 : Nb] [i2 : Nb] [j0 : Nb] [j1 : Nb] [j2 : Nb] [m : Nb ] [w-sqr : Nb ]): Nb ; linear combination + (define: (lc [i0 : Natural] [i1 : Natural] [i2 : Natural] [j0 : Natural] [j1 : Natural] [j2 : Natural] [m : Nb] [w-sqr : Nb ]): Nb ; linear combination (let ((a0h (quotient (vector-ref A i0) w)) (a0l (modulo (vector-ref A i0) w)) (a1h (quotient (vector-ref A i1) w)) diff --git a/collects/typed-scheme/private/base-env-numeric.ss b/collects/typed-scheme/private/base-env-numeric.ss index 55eb34f7..957a21db 100644 --- a/collects/typed-scheme/private/base-env-numeric.ss +++ b/collects/typed-scheme/private/base-env-numeric.ss @@ -1,66 +1,89 @@ #lang s-exp "env-lang.ss" -(require - scheme/tcp - scheme - scheme/unsafe/ops - (only-in rnrs/lists-6 fold-left) - '#%paramz - "extra-procs.ss" - (only-in '#%kernel [apply kernel:apply]) - scheme/promise scheme/system - (only-in string-constants/private/only-once maybe-print-message) - (only-in scheme/match/runtime match:error matchable? match-equality-test) - (for-syntax (only-in (types abbrev) [-Number N] [-Boolean B] [-Symbol Sym] [-Real R] [-ExactPositiveInteger -Pos]))) +(begin + (require + scheme/tcp + scheme + scheme/unsafe/ops + (only-in rnrs/lists-6 fold-left) + '#%paramz + "extra-procs.ss" + (only-in '#%kernel [apply kernel:apply]) + scheme/promise scheme/system + (only-in string-constants/private/only-once maybe-print-message) + (only-in scheme/match/runtime match:error matchable? match-equality-test) + (for-syntax (only-in (types abbrev) [-Number N] [-Boolean B] [-Symbol Sym] [-Real R] [-ExactPositiveInteger -Pos]))) + + (define-for-syntax all-num-types (list -Pos -Nat -Integer -ExactRational -Flonum -Real N)) -;; numeric operations -[modulo (cl->* (-Integer -Integer . -> . -Integer))] -[= (->* (list N N) N B)] -[>= (->* (list R R) R B)] -[< (->* (list R R) R B)] -[<= (->* (list R R) R B)] -[> (->* (list R R) R B)] + (define-for-syntax fl-comp (-> -Flonum -Flonum B)) + (define-for-syntax fl-op (-> -Flonum -Flonum -Flonum)) + (define-for-syntax fl-unop (-> -Flonum -Flonum)) + + (define-for-syntax real-comp (->* (list R R) R B)) + ) + +;; numeric predicates [zero? (make-pred-ty (list N) B -Zero)] -[* (apply cl->* - (for/list ([t (list -Pos -Nat -Integer -ExactRational -Flonum -Real N)]) - (->* (list) t t)))] -[/ (apply cl->* - (for/list ([t (list -Integer -ExactRational -Flonum -Real N)]) - (->* (list t) t t)))] -[+ (apply cl->* - (for/list ([t (list -Pos -Nat -Integer -ExactRational -Flonum -Real N)]) - (->* (list) t t)))] +[number? (make-pred-ty N)] +[integer? (Univ . -> . B : (-LFS (list (-filter -Real)) (list (-not-filter -Integer))))] +[exact-integer? (make-pred-ty -Integer)] +[real? (make-pred-ty -Real)] +[complex? (make-pred-ty N)] +[rational? (make-pred-ty -Real)] + +[positive? (-> -Real B)] +[negative? (-> -Real B)] + +[odd? (-> -Integer B)] +[even? (-> -Integer B)] + +[modulo (cl->* (-Integer -Integer . -> . -Integer))] + +[= (->* (list N N) N B)] + +[>= real-comp] +[< real-comp] +[<= real-comp] +[> real-comp] + + +[* (apply cl->* (for/list ([t all-num-types]) (->* (list) t t)))] +[+ (apply cl->* (for/list ([t all-num-types]) (->* (list) t t)))] + [- (apply cl->* (for/list ([t (list -Integer -ExactRational -Flonum -Real N)]) (->* (list t) t t)))] -[max (apply cl->* - (for/list ([t (list -Pos -Nat -Integer -ExactRational -Flonum -Real N)]) - (->* (list t) t t)))] -[min (apply cl->* - (for/list ([t (list -Pos -Nat -Integer -ExactRational -Flonum -Real N)]) - (->* (list t) t t)))] -[positive? (-> N B)] -[negative? (-> N B)] -[odd? (-> -Integer B)] -[even? (-> -Integer B)] +[/ (apply cl->* + (->* (list -Integer) -Integer -ExactRational) + (for/list ([t (list -ExactRational -Flonum -Real N)]) + (->* (list t) t t)))] + +[max (apply cl->* (for/list ([t all-num-types]) (->* (list t) t t)))] +[min (apply cl->* (for/list ([t all-num-types]) (->* (list t) t t)))] + + [add1 (cl->* (-> -Pos -Pos) - (-> -Nat -Nat) + (-> -Nat -Pos) (-> -Integer -Integer) (-> -ExactRational -ExactRational) (-> -Flonum -Flonum) (-> -Real -Real) (-> N N))] + [sub1 (cl->* (-> -Pos -Nat) (-> -Integer -Integer) (-> -ExactRational -ExactRational) (-> -Flonum -Flonum) (-> -Real -Real) (-> N N))] + [quotient (-Integer -Integer . -> . -Integer)] [remainder (-Integer -Integer . -> . -Integer)] [quotient/remainder (make-Function (list (make-arr (list -Integer -Integer) (-values (list -Integer -Integer)))))] +;; exactness [exact? (N . -> . B)] [inexact? (N . -> . B)] [exact->inexact (cl->* @@ -70,13 +93,6 @@ (-Real . -> . -ExactRational) (N . -> . N))] -[number? (make-pred-ty N)] -[integer? (Univ . -> . B : (-LFS (list (-filter N)) (list (-not-filter -Integer))))] -[exact-integer? (make-pred-ty -Integer)] - -[real? (make-pred-ty -Real)] -[complex? (make-pred-ty N)] -[rational? (make-pred-ty -Real)] [floor (-> N N)] [ceiling (-> N N)] [truncate (-> N N)] @@ -124,4 +140,17 @@ [sinh (N . -> . N)] [cosh (N . -> . N)] [tanh (N . -> . N)] -;; end numeric ops +;; unsafe numeric ops + +[unsafe-flabs fl-unop] + +[unsafe-fl+ fl-op] +[unsafe-fl- fl-op] +[unsafe-fl* fl-op] +[unsafe-fl/ fl-op] + +[unsafe-fl= fl-comp] +[unsafe-fl<= fl-comp] +[unsafe-fl>= fl-comp] +[unsafe-fl> fl-comp] +[unsafe-fl< fl-comp] diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss index 1c7f92a6..0a2b64ee 100644 --- a/collects/typed-scheme/private/base-env.ss +++ b/collects/typed-scheme/private/base-env.ss @@ -65,8 +65,7 @@ [eqv? (-> Univ Univ B)] [equal? (-> Univ Univ B)] [assert (-poly (a) (-> (Un a (-val #f)) a))] -[gensym (cl-> [(Sym) Sym] - [() Sym])] +[gensym (->opt [Sym] Sym)] [string-append (->* null -String -String)] [open-input-string (-> -String -Input-Port)] [open-output-file @@ -77,15 +76,12 @@ 'must-truncate 'truncate/replace) #f -Output-Port)] -[read (cl-> - [(-Port) -Sexp] - [() -Sexp])] +[read (->opt [-Input-Port] -Sexp)] [ormap (-polydots (a c b) (->... (list (->... (list a) (b b) c) (-lst a)) ((-lst b) b) c))] [andmap (-polydots (a c b) (cl->* ;(make-pred-ty (list (make-pred-ty (list a) B d) (-lst a)) B (-lst d)) (->... (list (->... (list a) (b b) c) (-lst a)) ((-lst b) b) c)))] -[newline (cl-> [() -Void] - [(-Port) -Void])] +[newline (->opt [-Output-Port] -Void)] [not (-> Univ B)] [box (-poly (a) (a . -> . (-box a)))] [unbox (-poly (a) ((-box a) . -> . a))] @@ -130,12 +126,9 @@ [remove (-poly (a) (a (-lst a) . -> . (-lst a)))] [remq (-poly (a) (a (-lst a) . -> . (-lst a)))] [remv (-poly (a) (a (-lst a) . -> . (-lst a)))] -[remove* (-poly (a b) (cl-> [((-lst a) (-lst a)) (-lst a)] - [((-lst a) (-lst b) (a b . -> . B)) (-lst b)]))] -[remq* (-poly (a b) (cl-> [((-lst a) (-lst a)) (-lst a)] - [((-lst a) (-lst b) (a b . -> . B)) (-lst b)]))] -[remv* (-poly (a b) (cl-> [((-lst a) (-lst a)) (-lst a)] - [((-lst a) (-lst b) (a b . -> . B)) (-lst b)]))] +[remove* (-poly (a b) ((-lst a) (-lst a) [(a b . -> . B)] . ->opt . (-lst b)))] +[remq* (-poly (a b) (cl-> [((-lst a) (-lst a)) (-lst a)]))] +[remv* (-poly (a b) (cl-> [((-lst a) (-lst a)) (-lst a)]))] (error (make-Function (list @@ -143,16 +136,14 @@ (make-arr (list -String) (Un) #:rest Univ) (make-arr (list Sym) (Un))))) -[namespace-variable-value - (cl-> [(Sym) Univ] - [(Sym B -Namespace (-> Univ)) Univ])] +[namespace-variable-value (Sym [Univ (-opt (-> Univ)) -Namespace] . ->opt . Univ)] [match:error (Univ . -> . (Un))] [match-equality-test (-Param (Univ Univ . -> . Univ) (Univ Univ . -> . Univ))] [matchable? (make-pred-ty (Un -String -Bytes))] -[display (cl-> [(Univ) -Void] [(Univ -Port) -Void])] -[write (cl-> [(Univ) -Void] [(Univ -Port) -Void])] -[print (cl-> [(Univ) -Void] [(Univ -Port) -Void])] +[display (Univ [-Output-Port] . ->opt . -Void)] +[write (Univ [-Output-Port] . ->opt . -Void)] +[print (Univ [-Output-Port] . ->opt . -Void)] [void (->* '() Univ -Void)] [void? (make-pred-ty -Void)] [printf (->* (list -String) Univ -Void)] @@ -163,10 +154,10 @@ [sleep (N . -> . -Void)] -[build-list (-poly (a) (-Integer (-Integer . -> . a) . -> . (-lst a)))] +[build-list (-poly (a) (-Nat (-Nat . -> . a) . -> . (-lst a)))] [reverse (-poly (a) (-> (-lst a) (-lst a)))] [append (-poly (a) (->* (list) (-lst a) (-lst a)))] -[length (-poly (a) (-> (-lst a) -Integer))] +[length (-poly (a) (-> (-lst a) -Nat))] [memq (-poly (a) (-> a (-lst a) (-opt (-lst a))))] [memv (-poly (a) (-> a (-lst a) (-opt (-lst a))))] [memf (-poly (a) ((a . -> . B) (-lst a) . -> . (-opt (-lst a))))] @@ -212,9 +203,7 @@ [string-copy (-> -String -String)] [string->immutable-string (-> -String -String)] [string-ref (-> -String -Nat -Char)] -[substring (cl->* - (-> -String -Nat -String) - (-> -String -Nat -Nat -String))] +[substring (->opt -String -Nat [-Nat] -String)] [string->path (-> -String -Path)] [file-exists? (-> -Pathlike B)] @@ -238,8 +227,8 @@ [assf (-poly (a b) ((a . -> . Univ) (-lst (-pair a b)) . -> . (-opt (-pair a b))))] -[list-ref (-poly (a) ((-lst a) -Integer . -> . a))] -[list-tail (-poly (a) ((-lst a) -Integer . -> . (-lst a)))] +[list-ref (-poly (a) ((-lst a) -Nat . -> . a))] +[list-tail (-poly (a) ((-lst a) -Nat . -> . (-lst a)))] [apply (-poly (a b) (((list) a . ->* . b) (-lst a) . -> . b))] [kernel:apply (-poly (a b) (((list) a . ->* . b) (-lst a) . -> . b))] @@ -248,7 +237,7 @@ (list (make-arr (list ((list) (a a) . ->... . b) (-lst a)) - (-values (list (-pair b (-val '())) -Integer -Integer -Integer))))))] + (-values (list (-pair b (-val '())) -Nat -Nat -Nat))))))] [call/cc (-poly (a b) (((a . -> . (Un)) . -> . b) . -> . (Un a b)))] [call/ec (-poly (a b) (((a . -> . (Un)) . -> . b) . -> . (Un a b)))] @@ -278,11 +267,9 @@ [pregexp (-String . -> . -PRegexp)] [byte-regexp (-Bytes . -> . -Byte-Regexp)] [byte-pregexp (-Bytes . -> . -Byte-PRegexp)] -[regexp-quote (cl-> [(-String) -String] - [(-String -Boolean) -String] - [(-Bytes) -Bytes] - [(-Bytes -Boolean) -Bytes])] - +[regexp-quote (cl->* + (-String [-Boolean] . ->opt . -String) + (-Bytes [-Boolean] . ->opt . -Bytes))] [regexp-match (let ([?outp (-opt -Output-Port)] [N -Nat] @@ -291,19 +278,10 @@ [-StrRx (Un -String -Regexp -PRegexp)] [-BtsRx (Un -Bytes -Byte-Regexp -Byte-PRegexp)] [-InpBts (Un -Input-Port -Bytes)]) - (cl-> [(-StrRx -String ) (optlist -String)] - [(-StrRx -String N ) (optlist -String)] - [(-StrRx -String N ?N ) (optlist -String)] - [(-StrRx -String N ?N ?outp) (optlist -String)] - [(-BtsRx -String ) (optlist -Bytes)] - [(-BtsRx -String N ) (optlist -Bytes)] - [(-BtsRx -String N ?N ) (optlist -Bytes)] - [(-BtsRx -String N ?N ?outp) (optlist -Bytes)] - [(-Pattern -InpBts ) (optlist -Bytes)] - [(-Pattern -InpBts N ) (optlist -Bytes)] - [(-Pattern -InpBts N ?N ) (optlist -Bytes)] - [(-Pattern -InpBts N ?N ?outp) (optlist -Bytes)]))] - + (cl->* + (-StrRx -String [N ?N ?outp] . ->opt . (optlist -String)) + (-BtsRx -String [N ?N ?outp] . ->opt . (optlist -Bytes)) + (-Pattern -InpBts [N ?N ?outp] . ->opt . (optlist -Bytes))))] [regexp-match* (let ([N -Nat] [?N (-opt -Nat)] @@ -354,8 +332,8 @@ [-> -String -String] [-> -Bytes -Bytes])] -[number->string (cl-> [(N) -String] [(N N) -String])] -[string->number (cl-> [(-String) N] [(-String N) N])] +[number->string (->opt N [N] -String)] +[string->number (->opt -String [N] -String)] [current-milliseconds (-> -Integer)] @@ -364,7 +342,7 @@ [raise-type-error (cl-> [(Sym -String Univ) (Un)] - [(Sym -String N (-lst Univ)) (Un)])] + [(Sym -String -Nat (-lst Univ)) (Un)])] ;; this is a hack @@ -376,12 +354,12 @@ [bitwise-not (null -Integer . ->* . -Integer)] [bitwise-xor (null -Integer . ->* . -Integer)] -[make-string (cl-> [(-Integer) -String] [(-Integer -Char) -String])] -[abs (N . -> . N)] -[substring (cl-> [(-String -Integer) -String] - [(-String -Integer -Integer) -String])] -[string-length (-String . -> . -Integer)] -[string-set! (-String -Integer -Char . -> . -Void)] +[make-string (cl-> [(-Nat) -String] [(-Nat -Char) -String])] +[abs (-Real . -> . -Real)] +[substring (->opt -String [-Nat] -String)] +[string-length (-String . -> . -Nat)] +[unsafe-string-length (-String . -> . -Nat)] +[string-set! (-String -Nat -Char . -> . -Void)] [file-exists? (-Pathlike . -> . B)] [string->symbol (-String . -> . Sym)] @@ -391,24 +369,21 @@ ;; vectors [vector? (make-pred-ty (-vec Univ))] -[vector-ref (-poly (a) ((-vec a) N . -> . a))] -[build-vector (-poly (a) (-Integer (-Integer . -> . a) . -> . (-vec a)))] +[vector-ref (-poly (a) ((-vec a) -Nat . -> . a))] +[build-vector (-poly (a) (-Nat (-Nat . -> . a) . -> . (-vec a)))] -[vector-set! (-poly (a) (-> (-vec a) N a -Void))] +[vector-set! (-poly (a) (-> (-vec a) -Nat a -Void))] [vector->list (-poly (a) (-> (-vec a) (-lst a)))] [list->vector (-poly (a) (-> (-lst a) (-vec a)))] -[vector-length (-poly (a) ((-vec a) . -> . -Integer))] -[make-vector (-poly (a) (cl-> [(-Integer) (-vec -Integer)] - [(-Integer a) (-vec a)]))] +[vector-length (-poly (a) ((-vec a) . -> . -Nat))] +[make-vector (-poly (a) (cl-> [(-Nat) (-vec -Integer)] + [(-Nat a) (-vec a)]))] [vector (-poly (a) (->* (list) a (-vec a)))] [vector-immutable (-poly (a) (->* (list) a (-vec a)))] [vector->vector-immutable (-poly (a) (-> (-vec a) (-vec a)))] [vector-fill! (-poly (a) (-> (-vec a) a -Void))] -[vector-copy! (-poly (a) - (cl->* ((-vec a) -Integer (-vec a) . -> . -Void) - ((-vec a) -Integer (-vec a) -Integer . -> . -Void) - ((-vec a) -Integer (-vec a) -Integer -Integer . -> . -Void)))] +[vector-copy! (-poly (a) ((-vec a) -Nat (-vec a) [-Nat -Nat] . ->opt . -Void))] ;; [vector->values no good type here] @@ -461,51 +436,36 @@ [bytes-ref (-> -Bytes -Integer -Integer)] [bytes-append (->* (list -Bytes) -Bytes -Bytes)] [subbytes (cl-> [(-Bytes -Integer) -Bytes] [(-Bytes -Integer -Integer) -Bytes])] -[bytes-length (-> -Bytes -Integer)] -[read-bytes-line (cl-> [() -Bytes] - [(-Input-Port) -Bytes] - [(-Input-Port Sym) -Bytes])] +[bytes-length (-> -Bytes -Nat)] +[unsafe-bytes-length (-> -Bytes -Nat)] + +[read-bytes-line (->opt [-Input-Port Sym] -Bytes)] [open-input-file (->key -Pathlike #:mode (Un (-val 'binary) (-val 'text)) #f -Input-Port)] [close-input-port (-> -Input-Port -Void)] [close-output-port (-> -Output-Port -Void)] -[read-line (cl-> [() -String] - [(-Input-Port) -String] - [(-Input-Port Sym) -String])] +[read-line (->opt [-Input-Port Sym] -String)] [copy-file (-> -Pathlike -Pathlike -Void)] [bytes->string/utf-8 (-> -Bytes -String)] [force (-poly (a) (-> (-Promise a) a))] [bytes* (list -Bytes) -Bytes B)] [regexp-replace* - (cl->* (-Pattern (Un -Bytes -String) (Un -Bytes -String) . -> . -Bytes) - (-Pattern -String -String . -> . -String))] + (cl->* (-Pattern -String -String . -> . -String) + (-Pattern (Un -Bytes -String) (Un -Bytes -String) . -> . -Bytes))] [peek-char - (cl->* [-> (Un -Char (-val eof))] - [-Input-Port . -> . (Un -Char (-val eof))] - [-Input-Port N . -> . (Un -Char (-val eof))])] + (cl->* [->opt [-Input-Port -Nat] (Un -Char (-val eof))])] [peek-byte - (cl->* [-> (Un -Byte (-val eof))] - [-Input-Port . -> . (Un -Byte (-val eof))] - [-Input-Port N . -> . (Un -Byte (-val eof))])] + (cl->* [->opt [-Input-Port -Nat] (Un -Byte (-val eof))])] [read-char - (cl->* [-> (Un -Char (-val eof))] - [-Input-Port . -> . (Un -Char (-val eof))])] + (cl->* [->opt [-Input-Port] (Un -Char (-val eof))])] [read-byte (cl->* [-> (Un -Byte (-val eof))] [-Input-Port . -> . (Un -Byte (-val eof))])] [make-pipe - (cl->* [-> (-values (list -Input-Port -Output-Port))] - [N . -> . (-values (list -Input-Port -Output-Port))])] + (cl->* [->opt [N] (-values (list -Input-Port -Output-Port))])] [open-output-bytes - (cl->* [-> -Output-Port] - [Univ . -> . -Output-Port])] -[get-output-bytes - (cl->* [-Output-Port . -> . -Bytes] - [-Output-Port Univ . -> . -Bytes] - [-Output-Port Univ N . -> . -Bytes] - [-Output-Port Univ N N . -> . -Bytes] - [-Output-Port N . -> . -Bytes] - [-Output-Port N N . -> . -Bytes])] + (cl->* [[Univ] . ->opt . -Output-Port])] +[get-output-bytes (-Output-Port [Univ N N] . ->opt . -Bytes)] #;[exn:fail? (-> Univ B)] #;[exn:fail:read? (-> Univ B)] @@ -519,8 +479,7 @@ (-> (-HT a b) (-> a b c) -Void))] [delete-file (-> -Pathlike -Void)] -[make-namespace (cl->* (-> -Namespace) - (-> (Un (-val 'empty) (-val 'initial)) -Namespace))] +[make-namespace (->opt [(Un (-val 'empty) (-val 'initial))] -Namespace)] [make-base-namespace (-> -Namespace)] [eval (-> -Sexp Univ)] @@ -556,18 +515,9 @@ [prop (-opt S)] [cert (-opt S)]) (cl->* - (-> ctxt Sym I) - (-> ctxt Pre A) - (-> ctxt Univ S) - (-> ctxt Sym srcloc I) - (-> ctxt Pre srcloc A) - (-> ctxt Univ srcloc S) - (-> ctxt Sym srcloc prop I) - (-> ctxt Pre srcloc prop A) - (-> ctxt Univ srcloc prop S) - (-> ctxt Sym srcloc prop cert I) - (-> ctxt Pre srcloc prop cert A) - (-> ctxt Univ srcloc prop cert S))))] + (->opt ctxt Sym [srcloc prop cert] I) + (->opt ctxt Pre [srcloc prop cert] A) + (->opt ctxt Univ [srcloc prop cert] S))))] [syntax->datum (cl->* (-> Any-Syntax -Sexp) (-> (-Syntax Univ) Univ))] @@ -620,14 +570,14 @@ ((list a) (b b) . ->... . (-opt c)) (-lst a)) ((-lst b) b) . ->... . (-lst c)))] -[take (-poly (a) ((-lst a) -Integer . -> . (-lst a)))] -[drop (-poly (a) ((-lst a) -Integer . -> . (-lst a)))] -[take-right (-poly (a) ((-lst a) -Integer . -> . (-lst a)))] -[drop-right (-poly (a) ((-lst a) -Integer . -> . (-lst a)))] +[take (-poly (a) ((-lst a) -Nat . -> . (-lst a)))] +[drop (-poly (a) ((-lst a) -Nat . -> . (-lst a)))] +[take-right (-poly (a) ((-lst a) -Nat . -> . (-lst a)))] +[drop-right (-poly (a) ((-lst a) -Nat . -> . (-lst a)))] [split-at - (-poly (a) ((list (-lst a)) -Integer . ->* . (-values (list (-lst a) (-lst a)))))] + (-poly (a) ((list (-lst a)) -Nat . ->* . (-values (list (-lst a) (-lst a)))))] [split-at-right - (-poly (a) ((list (-lst a)) -Integer . ->* . (-values (list (-lst a) (-lst a)))))] + (-poly (a) ((list (-lst a)) -Nat . ->* . (-values (list (-lst a) (-lst a)))))] [last (-poly (a) ((-lst a) . -> . a))] [add-between (-poly (a b) ((-lst a) b . -> . (-lst (Un a b))))] @@ -651,7 +601,9 @@ [tcp-accept (-TCP-Listener . -> . (-values (list -Input-Port -Output-Port)) )] [tcp-accept/enable-break (-TCP-Listener . -> . (-values (list -Input-Port -Output-Port)) )] [tcp-accept-ready? (-TCP-Listener . -> . B )] -[tcp-addresses (-Port . -> . (-values (list N N)))] +[tcp-addresses (cl->* + (-Port [(-val #f)] . ->opt . (-values (list -String -String))) + (-Port (-val #t) . -> . (-values (list -String -Nat -String -Nat))))] [tcp-close (-TCP-Listener . -> . -Void )] [tcp-connect (-String -Integer . -> . (-values (list -Input-Port -Output-Port)))] [tcp-connect/enable-break (-String -Integer . -> . (-values (list -Input-Port -Output-Port)))] @@ -672,8 +624,7 @@ [current-continuation-marks (-> -Cont-Mark-Set)] ;; scheme/port -[port->lines (cl->* (-Input-Port . -> . (-lst -String)) - (-> (-lst -String)))] +[port->lines (cl->* ([-Input-Port] . ->opt . (-lst -String)))] [with-output-to-string (-> (-> Univ) -String)] [open-output-nowhere (-> -Output-Port)] @@ -683,8 +634,7 @@ [explode-path (-Pathlike . -> . (-lst (Un -Path (-val 'up) (-val 'same))))] [find-relative-path (-Pathlike -Pathlike . -> . -Path)] [simple-form-path (-Pathlike . -> . -Path)] -[normalize-path (cl->* (-Pathlike . -> . -Path) - (-Pathlike -Pathlike . -> . -Path))] +[normalize-path (cl->* (-Pathlike [-Pathlike] . ->opt . -Path))] [filename-extension (-Pathlike . -> . (-opt -Bytes))] [file-name-from-path (-Pathlike . -> . (-opt -Path))] [path-only (-Pathlike . -> . -Path)] @@ -699,28 +649,22 @@ (let ([funarg* (-Path (one-of/c 'file 'dir 'link) a . -> . (-values (list a Univ)))] [funarg (-Path (one-of/c 'file 'dir 'link) a . -> . a)]) (cl->* - (funarg a . -> . a) - (funarg a (-opt -Pathlike) . -> . a) - (funarg a (-opt -Pathlike) Univ . -> . a) - (funarg* a . -> . a) - (funarg* a (-opt -Pathlike) . -> . a) - (funarg* a (-opt -Pathlike) Univ . -> . a))))] + (funarg a [(-opt -Pathlike) Univ]. ->opt . a) + (funarg* a [(-opt -Pathlike) Univ]. ->opt . a))))] ;; scheme/pretty -[pretty-print - (cl->* (Univ . -> . -Void) - (Univ -Output-Port . -> . -Void))] -[pretty-display - (cl->* (Univ . -> . -Void) - (Univ -Output-Port . -> . -Void))] -[pretty-format - (cl->* (Univ . -> . -Void) - (Univ -Integer . -> . -Void))] +[pretty-print (Univ [-Output-Port] . ->opt . -Void)] +[pretty-display (Univ [-Output-Port] . ->opt . -Void)] +[pretty-format (Univ [-Output-Port] . ->opt . -Void)] ;; unsafe +[unsafe-vector-length (-poly (a) ((-vec a) . -> . -Nat))] +[unsafe-car (-poly (a b) + (cl->* + (->acc (list (-pair a b)) a (list -car))))] [unsafe-cdr (-poly (a b) (cl->* (->acc (list (-pair a b)) b (list -cdr))))] @@ -767,3 +711,6 @@ [system* ((list -Pathlike) -String . ->* . -Boolean)] [system/exit-code (-String . -> . -Integer)] [system*/exit-code ((list -Pathlike) -String . ->* . -Integer)] + + +;; mutable pairs diff --git a/collects/typed-scheme/private/base-types-new.ss b/collects/typed-scheme/private/base-types-new.ss index bd9a6089..dd8ff7ae 100644 --- a/collects/typed-scheme/private/base-types-new.ss +++ b/collects/typed-scheme/private/base-types-new.ss @@ -1,11 +1,11 @@ #lang s-exp "type-env-lang.ss" -[Number -Number] [Complex -Number] +[Number -Number] [Integer -Integer] [Real -Real] [Exact-Rational -ExactRational] -[Flonum -Flonum] +[Float -Flonum] [Exact-Positive-Integer -ExactPositiveInteger] [Exact-Nonnegative-Integer -ExactNonnegativeInteger] [Natural -ExactNonnegativeInteger] @@ -41,5 +41,6 @@ [HashTable (-poly (a b) (-HT a b))] [Promise (-poly (a) (-Promise a))] [Pair (-poly (a b) (-pair a b))] +[MPair (-poly (a b) (-mpair a b))] [Boxof (-poly (a) (make-Box a))] [Continuation-Mark-Set -Cont-Mark-Set] diff --git a/collects/typed-scheme/private/env-lang.ss b/collects/typed-scheme/private/env-lang.ss index 434b5f5a..8b3e6feb 100644 --- a/collects/typed-scheme/private/env-lang.ss +++ b/collects/typed-scheme/private/env-lang.ss @@ -4,7 +4,7 @@ (require (for-syntax (utils tc-utils) (env init-envs) - scheme/base + scheme/base syntax/parse (r:infer infer) (only-in (r:infer infer-dummy) infer-param) (except-in (rep object-rep filter-rep type-rep) make-arr) @@ -12,21 +12,22 @@ (only-in (types convenience) [make-arr* make-arr]))) (define-syntax (#%module-begin stx) - (syntax-case stx (require) - [(mb (require . args) [id ty] ...) - (begin - (unless (andmap identifier? (syntax->list #'(id ...))) - (raise-syntax-error #f "not all ids")) - #'(#%plain-module-begin - (begin - (require . args) - (define-for-syntax e - (parameterize ([infer-param infer]) - (make-env [id ty] ...))) - (begin-for-syntax - (initialize-type-env e)))))] + (define-syntax-class clause + #:description "[id type]" + (pattern [id:identifier ty])) + (syntax-parse stx #:literals (require begin) + [(mb (~optional (~and extra (~or (begin . _) (require . args)))) + ~! :clause ...) + #'(#%plain-module-begin + (begin + extra + (define-for-syntax e + (parameterize ([infer-param infer]) + (make-env [id ty] ...))) + (begin-for-syntax + (initialize-type-env e))))] [(mb . rest) - #'(mb (require) . rest)])) + #'(mb (begin) . rest)])) (provide #%module-begin require diff --git a/collects/typed-scheme/rep/type-rep.ss b/collects/typed-scheme/rep/type-rep.ss index d0685d2c..c3bd256e 100644 --- a/collects/typed-scheme/rep/type-rep.ss +++ b/collects/typed-scheme/rep/type-rep.ss @@ -66,6 +66,11 @@ ;; left and right are Types (dt Pair ([left Type/c] [right Type/c]) [#:key 'pair]) +;; *mutable* pairs - distinct from regular pairs +;; left and right are Types +(dt MPair ([left Type/c] [right Type/c]) [#:key 'mpair]) + + ;; elem is a Type (dt Vector ([elem Type/c]) [#:frees (make-invariant (free-vars* elem)) (make-invariant (free-idxs* elem))] diff --git a/collects/typed-scheme/types/abbrev.ss b/collects/typed-scheme/types/abbrev.ss index 0a390beb..4ebd614f 100644 --- a/collects/typed-scheme/types/abbrev.ss +++ b/collects/typed-scheme/types/abbrev.ss @@ -20,6 +20,7 @@ (define -App make-App) (define -pair make-Pair) +(define -mpair make-MPair) (define -val make-Value) (define -Param make-Param) (define -box make-Box) diff --git a/collects/typed-scheme/utils/tc-utils.ss b/collects/typed-scheme/utils/tc-utils.ss index e6547683..48fd8124 100644 --- a/collects/typed-scheme/utils/tc-utils.ss +++ b/collects/typed-scheme/utils/tc-utils.ss @@ -58,9 +58,9 @@ don't depend on any other portion of the system stx)) (define (raise-typecheck-error msg stxs) - (raise (make-exn:fail:syntax (string-append "typecheck: " msg) - (current-continuation-marks) - stxs))) + (if (null? (cdr stxs)) + (raise-syntax-error 'typecheck msg (car stxs)) + (raise-syntax-error 'typecheck msg #f #f stxs))) (define delayed-errors null) diff --git a/collects/typed/framework/framework.ss b/collects/typed/framework/framework.ss index 513cfa1d..a447016b 100644 --- a/collects/typed/framework/framework.ss +++ b/collects/typed/framework/framework.ss @@ -19,8 +19,8 @@ [last-paragraph (-> Number)] [delete (Number Number -> Void)] [auto-wrap (Any -> Void)] - [paragraph-end-position (Number -> Number)] - [paragraph-start-position (Number -> Number)] + [paragraph-end-position (Number -> Natural)] + [paragraph-start-position (Number -> Natural)] [get-start-position (-> Number)] [get-end-position (-> Number)] [insert (String Number Number -> Void)]))) diff --git a/collects/typed/mred/mred.ss b/collects/typed/mred/mred.ss index 053d102a..60e475e4 100644 --- a/collects/typed/mred/mred.ss +++ b/collects/typed/mred/mred.ss @@ -23,7 +23,7 @@ ())) (dt Choice% (Class () ([parent Any] [label String] [choices (Listof Any)] [callback Any]) - ([get-selection (-> (Option Integer))] + ([get-selection (-> (Option Natural))] [set-selection (Integer -> Any)] [get-string-selection (-> (Option String))] [set-string-selection (String -> Void)]))) diff --git a/collects/typed/scheme/base.ss b/collects/typed/scheme/base.ss index 8798e922..860cb02e 100644 --- a/collects/typed/scheme/base.ss +++ b/collects/typed/scheme/base.ss @@ -4,7 +4,7 @@ (providing (libs (except scheme/base #%module-begin #%top-interaction with-handlers lambda #%app) (except typed-scheme/private/prims) - (except typed-scheme/private/base-types) + (except typed-scheme/private/base-types-new) (except typed-scheme/private/base-types-extra)) (basics #%module-begin #%top-interaction diff --git a/collects/typed/scheme/base/lang/reader.ss b/collects/typed/scheme/base/lang/reader.ss index 009b1f17..f276a7b4 100644 --- a/collects/typed/scheme/base/lang/reader.ss +++ b/collects/typed/scheme/base/lang/reader.ss @@ -1,6 +1,6 @@ #lang s-exp syntax/module-reader -typed-scheme +typed/scheme/base #:read r:read #:read-syntax r:read-syntax diff --git a/collects/typed/scheme/lang/reader.ss b/collects/typed/scheme/lang/reader.ss index 009b1f17..e5397c57 100644 --- a/collects/typed/scheme/lang/reader.ss +++ b/collects/typed/scheme/lang/reader.ss @@ -1,6 +1,6 @@ #lang s-exp syntax/module-reader -typed-scheme +typed/scheme #:read r:read #:read-syntax r:read-syntax From b2056bab7dd5a0a444d3b13dab000aa1f292e7eb Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Sat, 21 Nov 2009 22:21:36 +0000 Subject: [PATCH 07/17] use `make-provide/contract-transformer' svn: r16949 original commit: 406b5c384d446b9b275971d14a690b7c71d12cac --- .../typed-scheme/typecheck/provide-handling.ss | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/collects/typed-scheme/typecheck/provide-handling.ss b/collects/typed-scheme/typecheck/provide-handling.ss index 5fb645ca..22c86fe9 100644 --- a/collects/typed-scheme/typecheck/provide-handling.ss +++ b/collects/typed-scheme/typecheck/provide-handling.ss @@ -8,6 +8,8 @@ (private type-contract typed-renaming) (rep type-rep) (utils tc-utils) + scheme/contract/private/provide + unstable/syntax "def-binding.ss") (require (for-template scheme/base @@ -56,8 +58,19 @@ (cond [(type->contract (def-binding-ty b) (lambda () #f) #:out #t) => (lambda (cnt) - (with-syntax ([(export-id cnt-id) (generate-temporaries #'(id id))]) + (with-syntax ([(export-id cnt-id) (generate-temporaries #'(id id))] + [module-source (generate-temporary 'module-source)] + ;; don't actually need to verify - this is generated + [the-contract (generate-temporary 'generated-contract)]) #`(begin + (define module-source (#%variable-reference)) + (define the-contract #,cnt) + (define-syntax cnt-id + (make-provide/contract-transformer + (quote-syntax the-contract) + (quote-syntax id) + (quote-syntax module-source))) + #; (define/contract cnt-id #,cnt id) (define-syntax export-id (if (unbox typed-context?) From 5eb7939579e106cd644395b45dfe3de1042485fa Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Sat, 21 Nov 2009 23:24:02 +0000 Subject: [PATCH 08/17] check that we get correct blame svn: r16950 original commit: 5ea3e28078bc1ba5c0744f7fe3ebb76aadbfc464 --- collects/tests/typed-scheme/fail/back-and-forth.ss | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/collects/tests/typed-scheme/fail/back-and-forth.ss b/collects/tests/typed-scheme/fail/back-and-forth.ss index 023eaf60..b23c7703 100644 --- a/collects/tests/typed-scheme/fail/back-and-forth.ss +++ b/collects/tests/typed-scheme/fail/back-and-forth.ss @@ -1,5 +1,5 @@ #; -(exn-pred exn:fail:contract? #rx".*contract.*\\(-> Number Number\\).*") +(exn-pred exn:fail:contract? #rx".*violator.*contract.*\\(-> Number Number\\).*") #lang scheme/load @@ -8,11 +8,11 @@ (define (f x) (add1 x)) (provide f)) -(module n scheme +(module violator scheme (require 'm) (f 'foo)) (module o typed-scheme - (require 'n)) + (require 'violator)) (require 'o) From e326c243bc380d3313aaa6daa6b386feda63f5b9 Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Tue, 24 Nov 2009 04:04:31 +0000 Subject: [PATCH 09/17] improve error messages with `syntax-parse' svn: r17023 original commit: 176920530f5625da0b860e8b194f3a906dc9bcfe --- collects/typed-scheme/private/prims.ss | 24 +++++++++++++++++------- 1 file changed, 17 insertions(+), 7 deletions(-) diff --git a/collects/typed-scheme/private/prims.ss b/collects/typed-scheme/private/prims.ss index 190c832a..5723b612 100644 --- a/collects/typed-scheme/private/prims.ss +++ b/collects/typed-scheme/private/prims.ss @@ -307,19 +307,29 @@ This file defines two sorts of primitives. All of them are provided into any mod #t))])) (define-syntax (define-typed-struct stx) - (syntax-case stx (:) - [(_ nm ([fld : ty] ...) . opts) + (define-syntax-class fld-spec + #:literals (:) + #:description "[field-name : type]" + (pattern [fld:id : ty])) + (define-syntax-class struct-name + #:description "struct name (with optional super-struct name)" + #:attributes (name super) + (pattern (name:id super:id)) + (pattern name:id + #:with super #f)) + (syntax-parse stx + [(_ nm:struct-name (fs:fld-spec ...) . opts) (let ([mutable (if (memq '#:mutable (syntax->datum #'opts)) '(#:mutable) '())]) - (with-syntax ([d-s (syntax-property (syntax/loc stx (define-struct nm (fld ...) . opts)) + (with-syntax ([d-s (syntax-property (syntax/loc stx (define-struct nm (fs.fld ...) . opts)) 'typechecker:ignore #t)] - [dtsi (internal (quasisyntax/loc stx (define-typed-struct-internal nm ([fld : ty] ...) #,@mutable)))]) + [dtsi (internal (quasisyntax/loc stx (define-typed-struct-internal nm (fs ...) #,@mutable)))]) #'(begin d-s dtsi)))] - [(_ (vars ...) nm ([fld : ty] ...) . opts) - (with-syntax ([d-s (syntax-property (syntax/loc stx (define-struct nm (fld ...) . opts)) + [(_ (vars:id ...) nm:struct-name (fs:fld-spec ...) . opts) + (with-syntax ([d-s (syntax-property (syntax/loc stx (define-struct nm (fs.fld ...) . opts)) 'typechecker:ignore #t)] - [dtsi (internal (syntax/loc stx (define-typed-struct-internal (vars ...) nm ([fld : ty] ...))))]) + [dtsi (internal (syntax/loc stx (define-typed-struct-internal (vars ...) nm (fs ...))))]) #'(begin d-s dtsi))])) (define-syntax (require-typed-struct stx) From 09febf87c276c601f692f2b31e5ddcc76aee1be4 Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Tue, 24 Nov 2009 17:10:44 +0000 Subject: [PATCH 10/17] checkpoint svn: r17045 original commit: 29c4a84183f15c98093973fae3fe7ec20a9fd8a3 --- collects/tests/typed-scheme/fail/back-and-forth.ss | 7 ++++--- collects/typed-scheme/ts-reference.scrbl | 2 +- collects/typed-scheme/typecheck/provide-handling.ss | 8 ++------ collects/typed-scheme/typecheck/tc-toplevel.ss | 8 +++++--- 4 files changed, 12 insertions(+), 13 deletions(-) diff --git a/collects/tests/typed-scheme/fail/back-and-forth.ss b/collects/tests/typed-scheme/fail/back-and-forth.ss index b23c7703..eac8be7d 100644 --- a/collects/tests/typed-scheme/fail/back-and-forth.ss +++ b/collects/tests/typed-scheme/fail/back-and-forth.ss @@ -1,18 +1,19 @@ #; -(exn-pred exn:fail:contract? #rx".*violator.*contract.*\\(-> Number Number\\).*") +(exn-pred exn:fail:contract? #rx".*violator.*contract.*\\(-> Number Number\\).*f.*") #lang scheme/load (module m typed/scheme (: f (Number -> Number)) (define (f x) (add1 x)) - (provide f)) + (define g 17) + (provide f g)) (module violator scheme (require 'm) (f 'foo)) -(module o typed-scheme +(module o typed/scheme (require 'violator)) (require 'o) diff --git a/collects/typed-scheme/ts-reference.scrbl b/collects/typed-scheme/ts-reference.scrbl index f52c4a98..7981ffe7 100644 --- a/collects/typed-scheme/ts-reference.scrbl +++ b/collects/typed-scheme/ts-reference.scrbl @@ -228,7 +228,7 @@ This is legal only in expression contexts.} appropriate number of type variables. This is legal only in expression contexts.} -@schemevarfont|{#{e @ t ...}}| This is identical to @scheme[(inst e t ...)]. +@litchar|{#{e @ t ...}}| This is identical to @scheme[(inst e t ...)]. @subsection{Require} diff --git a/collects/typed-scheme/typecheck/provide-handling.ss b/collects/typed-scheme/typecheck/provide-handling.ss index 22c86fe9..8943cc59 100644 --- a/collects/typed-scheme/typecheck/provide-handling.ss +++ b/collects/typed-scheme/typecheck/provide-handling.ss @@ -33,7 +33,7 @@ (make-typed-renaming (syntax-property id 'not-free-identifier=? #t) alt) (make-rename-transformer (syntax-property id 'not-free-identifier=? #t)))) -(define (generate-prov stx-defs val-defs) +(define (generate-prov stx-defs val-defs pos-blame-id) (define mapping (make-free-identifier-mapping)) (lambda (form) (define (mem? i vd) @@ -59,19 +59,15 @@ => (lambda (cnt) (with-syntax ([(export-id cnt-id) (generate-temporaries #'(id id))] - [module-source (generate-temporary 'module-source)] - ;; don't actually need to verify - this is generated + [module-source pos-blame-id] [the-contract (generate-temporary 'generated-contract)]) #`(begin - (define module-source (#%variable-reference)) (define the-contract #,cnt) (define-syntax cnt-id (make-provide/contract-transformer (quote-syntax the-contract) (quote-syntax id) (quote-syntax module-source))) - #; - (define/contract cnt-id #,cnt id) (define-syntax export-id (if (unbox typed-context?) (renamer #'id #:alt #'cnt-id) diff --git a/collects/typed-scheme/typecheck/tc-toplevel.ss b/collects/typed-scheme/typecheck/tc-toplevel.ss index 86023b30..1b2a000e 100644 --- a/collects/typed-scheme/typecheck/tc-toplevel.ss +++ b/collects/typed-scheme/typecheck/tc-toplevel.ss @@ -3,7 +3,7 @@ (require (rename-in "../utils/utils.ss" [infer r:infer])) (require syntax/kerncase - unstable/list + unstable/list unstable/syntax mzlib/etc scheme/match "signatures.ss" @@ -253,9 +253,11 @@ ;; report delayed errors (report-all-errors) ;; compute the new provides - (with-syntax - ([((new-provs ...) ...) (map (generate-prov stx-defs val-defs) provs)]) + (with-syntax* + ([the-variable-reference (generate-temporary #'blame)] + [((new-provs ...) ...) (map (generate-prov stx-defs val-defs #'the-variable-reference) provs)]) #`(begin + (define the-variable-reference (#%variable-reference)) #,(env-init-code) #,(tname-env-init-code) #,(talias-env-init-code) From 445c65e12ea8fbe1fc08b44f438bfd7d20051c2a Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Wed, 25 Nov 2009 02:30:41 +0000 Subject: [PATCH 11/17] checkpoint svn: r17054 original commit: e3bafbe298688ec0efe47a09254492f93027fa71 --- .../typed-scheme/fail/too-many-errors.ss | 11 + .../typed-scheme/succeed/map-nonempty.ss | 6 + collects/typed-scheme/env/init-envs.ss | 25 +-- collects/typed-scheme/infer/promote-demote.ss | 2 +- collects/typed-scheme/private/base-env.ss | 9 +- collects/typed-scheme/private/parse-type.ss | 4 +- collects/typed-scheme/rep/free-variance.ss | 103 --------- collects/typed-scheme/rep/interning.ss | 9 +- collects/typed-scheme/rep/rep-utils.ss | 197 +++++++++++++++--- collects/typed-scheme/rep/type-rep.ss | 47 +++-- collects/typed-scheme/typecheck/tc-app.ss | 43 ++-- collects/typed-scheme/types/abbrev.ss | 15 +- collects/typed-scheme/types/convenience.ss | 6 +- collects/typed-scheme/types/printer.ss | 1 + .../typed-scheme/types/remove-intersect.ss | 3 +- collects/typed-scheme/types/subtype.ss | 2 +- collects/typed-scheme/types/union.ss | 2 +- collects/typed-scheme/types/utils.ss | 3 +- collects/typed-scheme/utils/utils.ss | 10 +- collects/typed/net/cgi.ss | 1 + 20 files changed, 294 insertions(+), 205 deletions(-) create mode 100644 collects/tests/typed-scheme/fail/too-many-errors.ss create mode 100644 collects/tests/typed-scheme/succeed/map-nonempty.ss diff --git a/collects/tests/typed-scheme/fail/too-many-errors.ss b/collects/tests/typed-scheme/fail/too-many-errors.ss new file mode 100644 index 00000000..6d726847 --- /dev/null +++ b/collects/tests/typed-scheme/fail/too-many-errors.ss @@ -0,0 +1,11 @@ +#lang typed/scheme + +(: f : Number -> Number) +(define (f a b) + (+ a b)) + +(define: (g [a : Number] [b : Number]) : Number + (+ a b)) + +(f 1 2) +(g 1 2) diff --git a/collects/tests/typed-scheme/succeed/map-nonempty.ss b/collects/tests/typed-scheme/succeed/map-nonempty.ss new file mode 100644 index 00000000..0fddf079 --- /dev/null +++ b/collects/tests/typed-scheme/succeed/map-nonempty.ss @@ -0,0 +1,6 @@ +#lang typed/scheme + +(: x (Pair Number (Listof Number))) +(define x (cons 1 (list 1 2 3 4))) + +(apply max (ann (map add1 x) : (Pair Number (Listof Number)))) \ No newline at end of file diff --git a/collects/typed-scheme/env/init-envs.ss b/collects/typed-scheme/env/init-envs.ss index 73d1a9a1..a92069c7 100644 --- a/collects/typed-scheme/env/init-envs.ss +++ b/collects/typed-scheme/env/init-envs.ss @@ -22,27 +22,28 @@ (define (gen-constructor sym) (string->symbol (string-append "make-" (substring (symbol->string sym) 7)))) (match v - [(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))] + [(Union: elems) `(make-Union (sort (list ,@(map sub elems)) < #:key Type-seq) ',(Type-name v))] + [(Base: n cnt) `(make-Base ',n (quote-syntax ,cnt) ',(Type-name v))] + [(Name: stx) `(make-Name (quote-syntax ,stx) ',(Type-name v))] [(Struct: name parent flds proc poly? pred-id cert) - `(make-Struct ,(sub name) ,(sub parent) ,(sub flds) ,(sub proc) ,(sub poly?) (quote-syntax ,pred-id) (syntax-local-certifier))] - [(App: rator rands stx) `(make-App ,(sub rator) ,(sub rands) (quote-syntax ,stx))] - [(Opaque: pred cert) `(make-Opaque (quote-syntax ,pred) (syntax-local-certifier))] + `(make-Struct ,(sub name) ,(sub parent) ,(sub flds) ,(sub proc) ,(sub poly?) (quote-syntax ,pred-id) (syntax-local-certifier) ',(Type-name v))] + [(App: rator rands stx) `(make-App ,(sub rator) ,(sub rands) (quote-syntax ,stx) ',(Type-name v))] + [(Opaque: pred cert) `(make-Opaque (quote-syntax ,pred) (syntax-local-certifier) ',(Type-name v))] [(Refinement: parent pred cert) `(make-Refinement ,(sub parent) (quote-syntax ,pred) - (syntax-local-certifier))] - [(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))] + (syntax-local-certifier) + ',(Type-name v))] + [(Mu-name: n b) `(make-Mu ,(sub n) ,(sub b) ',(Type-name v))] + [(Poly-names: ns b) `(make-Poly (list ,@(map sub ns)) ,(sub b) ',(Type-name v))] + [(PolyDots-names: ns b) `(make-PolyDots (list ,@(map sub ns)) ,(sub b) ',(Type-name v))] [(? (lambda (e) (or (LatentFilter? e) (LatentObject? e) (PathElem? e))) (app (lambda (v) (vector->list (struct->vector v))) (list-rest tag seq vals))) `(,(gen-constructor tag) ,@(map sub vals))] [(? (lambda (e) (or (Type? e))) - (app (lambda (v) (vector->list (struct->vector v))) (list-rest tag key seq vals))) - `(,(gen-constructor tag) ,@(map sub vals))] + (app (lambda (v) (vector->list (struct->vector v))) (list-rest tag key seq name vals))) + `(,(gen-constructor tag) ,@(map sub vals) ',name)] [_ (basic v)])) (define (bound-in-this-module id) diff --git a/collects/typed-scheme/infer/promote-demote.ss b/collects/typed-scheme/infer/promote-demote.ss index 1eb261f1..316ed06b 100644 --- a/collects/typed-scheme/infer/promote-demote.ss +++ b/collects/typed-scheme/infer/promote-demote.ss @@ -1,7 +1,7 @@ #lang scheme/unit (require "../utils/utils.ss") -(require (rep type-rep rep-utils) +(require (rep type-rep) (types convenience union utils) "signatures.ss" scheme/list scheme/match) diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss index 0a2b64ee..98d2c9da 100644 --- a/collects/typed-scheme/private/base-env.ss +++ b/collects/typed-scheme/private/base-env.ss @@ -98,8 +98,13 @@ [list? (make-pred-ty (-lst Univ))] [list (-poly (a) (->* '() a (-lst a)))] [procedure? (make-pred-ty top-func)] -[map (-polydots (c a b) ((list ((list a) (b b) . ->... . c) (-lst a)) - ((-lst b) b) . ->... .(-lst c)))] +[map (-polydots (c a b) + (cl->* + (-> (-> a c) (-pair a (-lst a)) (-pair c (-lst c))) + ((list + ((list a) (b b) . ->... . c) + (-lst a)) + ((-lst b) b) . ->... .(-lst c))))] [for-each (-polydots (c a b) ((list ((list a) (b b) . ->... . Univ) (-lst a)) ((-lst b) b) . ->... . -Void))] [fold-left (-polydots (c a b) ((list ((list c a) (b b) . ->... . c) c (-lst a)) diff --git a/collects/typed-scheme/private/parse-type.ss b/collects/typed-scheme/private/parse-type.ss index 613c5a57..f3db1d68 100644 --- a/collects/typed-scheme/private/parse-type.ss +++ b/collects/typed-scheme/private/parse-type.ss @@ -238,12 +238,12 @@ (lambda (t) ;(printf "found a type alias ~a~n" #'id) (add-type-name-reference #'id) - t)] + t #;(add-name t (syntax-e #'id)))] ;; if it's a type name, we just use the name [(lookup-type-name #'id (lambda () #f)) (add-type-name-reference #'id) ;(printf "found a type name ~a~n" #'id) - (make-Name #'id)] + (add-name (make-Name #'id) (syntax-e #'id))] [(free-identifier=? #'id #'t:->) (tc-error/delayed "Incorrect use of -> type constructor") Err] diff --git a/collects/typed-scheme/rep/free-variance.ss b/collects/typed-scheme/rep/free-variance.ss index 7e4014e3..c53a5086 100644 --- a/collects/typed-scheme/rep/free-variance.ss +++ b/collects/typed-scheme/rep/free-variance.ss @@ -1,104 +1 @@ #lang scheme/base -(require "../utils/utils.ss") - -(require (for-syntax scheme/base) - (utils tc-utils) - mzlib/etc) - -;; this file contains support for calculating the free variables/indexes of types -;; actual computation is done in rep-utils.ss and type-rep.ss - -(define-values (Covariant Contravariant Invariant Constant Dotted) - (let () - (define-struct Variance () #:inspector #f) - (define-struct (Covariant Variance) () #:inspector #f) - (define-struct (Contravariant Variance) () #:inspector #f) - (define-struct (Invariant Variance) () #:inspector #f) - (define-struct (Constant Variance) () #:inspector #f) - ;; not really a variance, but is disjoint with the others - (define-struct (Dotted Variance) () #:inspector #f) - (values (make-Covariant) (make-Contravariant) (make-Invariant) (make-Constant) (make-Dotted)))) - - -(provide Covariant Contravariant Invariant Constant Dotted) - -;; hashtables for keeping track of free variables and indexes -(define index-table (make-weak-hasheq)) -;; maps Type to List[Cons[Number,Variance]] -(define var-table (make-weak-hasheq)) -;; maps Type to List[Cons[Symbol,Variance]] - -(define (free-idxs* t) (hash-ref index-table t (lambda _ (int-err "type ~a not in index-table" (syntax-e t))))) -(define (free-vars* t) (hash-ref var-table t (lambda _ (int-err "type ~a not in var-table" (syntax-e t))))) - - -(define empty-hash-table (make-immutable-hasheq null)) - -(provide free-vars* free-idxs* empty-hash-table make-invariant) - -;; frees = HT[Idx,Variance] where Idx is either Symbol or Number -;; (listof frees) -> frees -(define (combine-frees freess) - (define ht (make-hasheq)) - (define (combine-var v w) - (cond - [(eq? v w) v] - [(eq? v Dotted) w] - [(eq? w Dotted) v] - [(eq? v Constant) w] - [(eq? w Constant) v] - [else Invariant])) - (for* ([old-ht (in-list freess)] - [(sym var) (in-hash old-ht)]) - (let* ([sym-var (hash-ref ht sym (lambda () #f))]) - (if sym-var - (hash-set! ht sym (combine-var var sym-var)) - (hash-set! ht sym var)))) - ht) - -;; given a set of free variables, change bound to ... -;; (if bound wasn't free, this will add it as Dotted -;; appropriately so that things that expect to see -;; it as "free" will -- fixes the case where the -;; dotted pre-type base doesn't use the bound). -(define (fix-bound vs bound) - (define vs* (hash-map* (lambda (k v) v) vs)) - (hash-set! vs* bound Dotted) - vs*) - -;; frees -> frees -(define (flip-variances vs) - (hash-map* - (lambda (k v) - (evcase - v - [Covariant Contravariant] - [Contravariant Covariant] - [v v])) - vs)) - -(define (make-invariant vs) - (hash-map* - (lambda (k v) Invariant) - vs)) - -(define (hash-map* f ht) - (define new-ht (make-hasheq)) - (for ([(k v) (in-hash ht)]) - (hash-set! new-ht k (f k v))) - new-ht) - -(define (without-below n frees) - (define new-ht (make-hasheq)) - (for ([(k v) (in-hash frees)]) - (when (>= k n) (hash-set! new-ht k v))) - new-ht) - -(provide combine-frees flip-variances without-below unless-in-table var-table index-table empty-hash-table - fix-bound) - -(define-syntax (unless-in-table stx) - (syntax-case stx () - [(_ table val . body) - (quasisyntax/loc stx - (hash-ref table val #,(syntax/loc #'body (lambda () . body))))])) diff --git a/collects/typed-scheme/rep/interning.ss b/collects/typed-scheme/rep/interning.ss index 3dfd9aef..a370b34d 100644 --- a/collects/typed-scheme/rep/interning.ss +++ b/collects/typed-scheme/rep/interning.ss @@ -14,12 +14,9 @@ #'(define *name (let ([table (make-ht)]) (lambda (arg ...) - (let ([key key-expr]) - (hash-ref table key - (lambda () - (let ([new (make-name (count!) e ... arg ...)]) - (hash-set! table key new) - new)))))))])) + (let* ([key key-expr] + [new-seq (hash-ref table key count!)]) + (make-name new-seq e ... arg ...)))))])) (define (make-count!) (let ([state 0]) diff --git a/collects/typed-scheme/rep/rep-utils.ss b/collects/typed-scheme/rep/rep-utils.ss index ca994b19..d1194589 100644 --- a/collects/typed-scheme/rep/rep-utils.ss +++ b/collects/typed-scheme/rep/rep-utils.ss @@ -2,9 +2,8 @@ (require "../utils/utils.ss") (require mzlib/struct - scheme/match + scheme/match scheme/list syntax/boundmap - "free-variance.ss" "interning.ss" unstable/syntax unstable/match mzlib/etc @@ -25,9 +24,11 @@ (provide == defintern hash-id (for-syntax fold-target)) + + (define-for-syntax fold-target #'fold-target) -(define-for-syntax (mk par ht-stx key?) +(define-for-syntax (mk par ht-stx key? name?) (define-syntax-class opt-cnt-id #:attributes (i cnt) (pattern i:id @@ -67,6 +68,8 @@ #:with e fold-target) (pattern ex:expr #:with e #'#'ex)) + (unless (equal? key? name?) + (error "key? not name")) (lambda (stx) (syntax-parse stx [(dform nm:id flds:idlist (~or @@ -85,7 +88,7 @@ [*maker (format-id #'nm "*~a" #'nm)] [**maker (format-id #'nm "**~a" #'nm)] [*maker-cnt (if enable-contracts? - (or (attribute cnt) #'(flds.cnt ... . -> . pred)) + (or (attribute cnt) #`((flds.cnt ...) #,(if name? #'(any/c) #'()) . ->* . pred)) #'any/c)] [ht-stx ht-stx] [bfs-fold-rhs (cond [(attribute fold-rhs) @@ -105,26 +108,30 @@ (p/c (rename *maker maker *maker-cnt))))] [intern (let ([mk (lambda (int) - (if key? - #`(defintern (**maker . flds.fs) maker #,int #:extra-arg #,(attribute key-expr)) - #`(defintern (**maker . flds.fs) maker #,int)))]) - (syntax-parse #'flds.fs - [_ #:fail-unless (attribute intern?) #f - (mk #'intern?)] - [() (mk #'#f)] - [(f) (mk #'f)] - [_ (mk #'(list . flds.fs))]))] - [(ign-pats ...) (if key? #'(_ _) #'(_))] + (if (and key? name?) + #`(defintern (**maker name-val . flds.fs) maker #,int #:extra-arg #,(attribute key-expr)) + #`(defintern (**maker . flds.fs) maker #,int)))]) + (syntax-parse #'flds.fs + [_ #:fail-unless (attribute intern?) #f + (mk #'intern?)] + [() (mk #'#f)] + [(f) (mk #'f)] + [_ (mk #'(list . flds.fs))]))] + [(ign-pats ...) (if (and name? key?) #'(_ _ _) #'(_))] [frees-def (if (attribute frees) #'frees.def #'(begin))] [frees (with-syntax ([(f1 f2) (if (attribute frees) #'(frees.f1 frees.f2) (list (combiner #'free-vars* #'flds.fs) - (combiner #'free-idxs* #'flds.fs)))]) + (combiner #'free-idxs* #'flds.fs)))] + [(fs ...) #'flds.fs] + [name-val-formal + (if name? #'([name-val #f]) #'())] + [name-val-expr (if name? #'(name-val) #'())]) (quasisyntax/loc stx (w/c nm ([*maker *maker-cnt]) - (define (*maker . flds.fs) - (define v (**maker . flds.fs)) + (define (*maker fs ... #,@#'name-val-formal) + (define v (**maker #,@#'name-val-expr fs ...)) frees-def (unless-in-table var-table v @@ -228,23 +235,29 @@ (define-syntax (make-prim-type stx) (define default-flds #'(seq)) (define-syntax-class type-name-base - #:attributes (i lower-s first-letter key? (fld-names 1)) + #:attributes (i lower-s first-letter key? (fld-names 1) name?) #:transparent (pattern i:id #:attr lower-s (string-downcase (symbol->string (attribute i.datum))) #:with (fld-names ...) default-flds #:with key? #'#f + #:with name? #'#f #:attr first-letter (string-ref (attribute lower-s) 0)) (pattern [i:id #:d d-name:id] #:with (fld-names ...) default-flds #:attr lower-s (string-downcase (symbol->string (attribute i.datum))) #:with key? #'#f + #:with name? #'#f #:attr first-letter (symbol->string (attribute d-name.datum))) - (pattern [i:id #:key] + (pattern [i:id #:key (~optional (~and name-kw #:name))] #:with (fld-names ...) (datum->syntax #f (append (syntax->list default-flds) - (syntax->list #'(key)))) + (list #'key) + (if (attribute name-kw) + (list #'name) + null))) #:attr lower-s (string-downcase (symbol->string (attribute i.datum))) #:with key? #'#t + #:with name? (if (attribute name-kw) #'#t #'#f) #:attr first-letter (string-ref (attribute lower-s) 0))) (define-syntax-class type-name #:transparent @@ -258,7 +271,7 @@ #:with ht (format-id #'i "~a-name-ht" (attribute lower-s)) #:with rec-id (format-id #'i "~a-rec-id" (attribute lower-s)) #:with d-id (format-id #'i "d~a" (attribute first-letter)) - #:with (_ _ pred? accs ...) + #:with (_ _ pred? seq-acc accs ...) (datum->syntax #f (build-struct-names #'name (syntax->list #'(fld-names ...)) #f #t #'name)))) (syntax-parse stx [(_ i:type-name ...) @@ -267,11 +280,15 @@ [fresh-ids-list #'(fresh-ids ...)] [(anys ...) (for/list ([i (syntax->list #'fresh-ids-list)]) #'any/c)]) #'(begin - (provide i.d-id ... i.printer ... i.name ... i.pred? ... i.accs ... ... + (provide i.d-id ... i.printer ... i.name ... i.pred? ... i.seq-acc ... i.accs ... ... (for-syntax i.ht ... i.rec-id ...)) - (define-syntax i.d-id (mk #'i.name #'i.ht i.key?)) ... + (define-syntax i.d-id (mk #'i.name #'i.ht i.key? i.name?)) ... (define-for-syntax i.ht (make-hasheq)) ... - (define-struct/printer i.name (i.fld-names ...) (lambda (a b c) ((unbox i.printer) a b c))) ... + (define-struct/printer i.name (i.fld-names ...) (lambda (a b c) ((unbox i.printer) a b c)) + [prop:equal+hash (list (lambda (a b rec) + (eq? (i.seq-acc a) (i.seq-acc b))) + (lambda (a rec) (i.seq-acc a)) + (lambda (a secondary) (secondary a)))]) ... (define-for-syntax i.rec-id #'i.rec-id) ... (provide i.case ...) (define-syntaxes (i.case ...) @@ -284,9 +301,139 @@ '(i.keyword ...))) (list i.ht ...)))))))])) -(make-prim-type [Type #:key] +(make-prim-type [Type #:key #:name] Filter [LatentFilter #:d lf] Object [LatentObject #:d lo] [PathElem #:d pe]) + +;; free-variance.ss starts here: + +(require "../utils/utils.ss") + +(require (for-syntax scheme/base) + (utils tc-utils) + scheme/contract + mzlib/etc) + +;; this file contains support for calculating the free variables/indexes of types +;; actual computation is done in rep-utils.ss and type-rep.ss + +(define-values (Covariant Contravariant Invariant Constant Dotted) + (let () + (define-struct Variance () #:inspector #f) + (define-struct (Covariant Variance) () #:inspector #f) + (define-struct (Contravariant Variance) () #:inspector #f) + (define-struct (Invariant Variance) () #:inspector #f) + (define-struct (Constant Variance) () #:inspector #f) + ;; not really a variance, but is disjoint with the others + (define-struct (Dotted Variance) () #:inspector #f) + (values (make-Covariant) (make-Contravariant) (make-Invariant) (make-Constant) (make-Dotted)))) + +(define (variance? e) + (memq e (list Covariant Contravariant Invariant Constant Dotted))) + + +(provide Covariant Contravariant Invariant Constant Dotted) + +;; hashtables for keeping track of free variables and indexes +(define index-table (make-weak-hash)) +;; maps Type to List[Cons[Number,Variance]] +(define var-table (make-weak-hash)) +;; maps Type to List[Cons[Symbol,Variance]] + +(define input/c (or/c Type? Filter? LatentFilter? Object? LatentObject? PathElem?)) + +(d/c (free-idxs* t) + (-> input/c (hash/c integer? variance?)) + (hash-ref index-table t (lambda _ (int-err "type ~a not in index-table" t)))) +(d/c (free-vars* t) + (-> input/c (hash/c symbol? variance?)) + (hash-ref var-table t (lambda _ (int-err "type ~a not in var-table ~a" t (take (reverse (hash-map var-table list)) 20))))) + + +(define empty-hash-table (make-immutable-hasheq null)) + +;; Type? is not available here! grrr +(p/c + [free-vars* (-> input/c (hash/c symbol? variance?))] + [free-idxs* (-> input/c (hash/c integer? variance?))]) + +(provide empty-hash-table) + +;; frees = HT[Idx,Variance] where Idx is either Symbol or Number +;; (listof frees) -> frees +(define (combine-frees freess) + (define ht (make-hasheq)) + (define (combine-var v w) + (cond + [(eq? v w) v] + [(eq? v Dotted) w] + [(eq? w Dotted) v] + [(eq? v Constant) w] + [(eq? w Constant) v] + [else Invariant])) + (for* ([old-ht (in-list freess)] + [(sym var) (in-hash old-ht)]) + (let* ([sym-var (hash-ref ht sym (lambda () #f))]) + (if sym-var + (hash-set! ht sym (combine-var var sym-var)) + (hash-set! ht sym var)))) + ht) + +;; given a set of free variables, change bound to ... +;; (if bound wasn't free, this will add it as Dotted +;; appropriately so that things that expect to see +;; it as "free" will -- fixes the case where the +;; dotted pre-type base doesn't use the bound). +(define (fix-bound vs bound) + (define vs* (hash-map* (lambda (k v) v) vs)) + (hash-set! vs* bound Dotted) + vs*) + +;; frees -> frees +(define (flip-variances vs) + (hash-map* + (lambda (k v) + (evcase + v + [Covariant Contravariant] + [Contravariant Covariant] + [v v])) + vs)) + +(define (make-invariant vs) + (hash-map* + (lambda (k v) Invariant) + vs)) + +(define (hash-map* f ht) + (define new-ht (make-hasheq)) + (for ([(k v) (in-hash ht)]) + (hash-set! new-ht k (f k v))) + new-ht) + +(define (without-below n frees) + (define new-ht (make-hasheq)) + (for ([(k v) (in-hash frees)]) + (when (>= k n) (hash-set! new-ht k v))) + new-ht) + +(define table/c (hash/c (or/c integer? symbol?) variance?)) + +(p/c [combine-frees (-> (listof table/c) table/c)] + [flip-variances (-> table/c table/c)] + [make-invariant (-> table/c table/c)] + [without-below (-> integer? table/c table/c)]) + +(provide unless-in-table var-table index-table empty-hash-table fix-bound) + +(define-syntax (unless-in-table stx) + (syntax-case stx () + [(_ table val . body) + (quasisyntax/loc stx + (hash-ref table val #,(syntax/loc #'body (lambda () . body))))])) + + +;; free-variance.ss ends here diff --git a/collects/typed-scheme/rep/type-rep.ss b/collects/typed-scheme/rep/type-rep.ss index c3bd256e..a23d9c75 100644 --- a/collects/typed-scheme/rep/type-rep.ss +++ b/collects/typed-scheme/rep/type-rep.ss @@ -28,6 +28,8 @@ ;; t must be a Type (dt Scope ([t (or/c Type/c Scope?)]) [#:key (Type-key t)]) + + (define (scope-depth k) (flat-named-contract (format "Scope of depth ~a" k) @@ -100,7 +102,7 @@ (dt Poly (n body) #:no-provide [#:contract (->d ([n natural-number/c] [body (scope-depth n)]) - () + ([_ any/c]) [result Poly?])] [#:frees (free-vars* body) (without-below n (free-idxs* body))] [#:fold-rhs (let ([body* (remove-scopes n body)]) @@ -113,7 +115,7 @@ (dt PolyDots (n body) #:no-provide [#:contract (->d ([n natural-number/c] [body (scope-depth n)]) - () + ([_ any/c]) [result PolyDots?])] [#:key (Type-key body)] [#:frees (free-vars* body) (without-below n (free-idxs* body))] @@ -229,17 +231,21 @@ ;; elems : Listof[Type] (dt Union ([elems (and/c (listof Type/c) - (lambda (es) - (let-values ([(sorted? k) - (for/fold ([sorted? #t] - [last -1]) - ([e es]) - (let ([seq (Type-seq e)]) - (values - (and sorted? - (< last seq)) - seq)))]) - sorted?)))]) + (flat-named-contract + 'sorted-types + (lambda (es) + (let-values ([(sorted? k) + (for/fold ([sorted? #t] + [last -1]) + ([e es]) + (let ([seq (Type-seq e)]) + (values + (and sorted? + (< last seq)) + seq)))]) + (unless sorted? + (printf "seqs ~a~n" (map Type-seq es))) + sorted?))))]) [#:frees (combine-frees (map free-vars* elems)) (combine-frees (map free-idxs* elems))] [#:fold-rhs ((get-union-maker) (map type-rec-id elems))] @@ -341,7 +347,7 @@ [_ (int-err "Tried to remove too many scopes: ~a" sc)]))) ;; type equality -(define type-equal? eq?) +(define (type-equal? t1 t2) (eq? (Type-seq t1) (Type-seq t2))) ;; inequality - good @@ -465,8 +471,8 @@ #;(trace instantiate-many abstract-many) ;; the 'smart' constructor -(define (Mu* name body) - (let ([v (*Mu (abstract name body))]) +(define (Mu* name body [print-name #f]) + (let ([v (*Mu (abstract name body) print-name)]) (hash-set! name-table v name) v)) @@ -477,9 +483,9 @@ (instantiate (*F name) scope)])) ;; the 'smart' constructor -(define (Poly* names body) +(define (Poly* names body [print-name #f]) (if (null? names) body - (let ([v (*Poly (length names) (abstract-many names body))]) + (let ([v (*Poly (length names) (abstract-many names body) print-name)]) (hash-set! name-table v names) v))) @@ -492,9 +498,9 @@ (instantiate-many (map *F names) scope)])) ;; the 'smart' constructor -(define (PolyDots* names body) +(define (PolyDots* names body [print-name #f]) (if (null? names) body - (let ([v (*PolyDots (length names) (abstract-many names body))]) + (let ([v (*PolyDots (length names) (abstract-many names body) print-name)]) (hash-set! name-table v names) v))) @@ -610,6 +616,7 @@ remove-dups sub-lf sub-lo sub-pe Values: Values? Values-rs + Type-key Type-seq Type-name type-case (rename-out [Mu:* Mu:] [Poly:* Poly:] [PolyDots:* PolyDots:] diff --git a/collects/typed-scheme/typecheck/tc-app.ss b/collects/typed-scheme/typecheck/tc-app.ss index 4c214123..89a37e48 100644 --- a/collects/typed-scheme/typecheck/tc-app.ss +++ b/collects/typed-scheme/typecheck/tc-app.ss @@ -606,15 +606,33 @@ #:return (or expected (ret (Un))) (string-append "No function domains matched in function application:\n" (domain-mismatches t doms rests drests rngs argtys-t #f #f))))] - ;; polymorphic functions without dotted rest, and without mandatory keyword args + ;; any kind of polymorphic function + [((tc-result1: (and t (PolyDots: + (and vars (list fixed-vars ... dotted-var)) + (Function: (list (and arrs (arr: doms rngs rests drests (list (Keyword: _ _ #f) ...))) ...))))) + (list (tc-result1: argtys-t) ...)) + (handle-clauses (doms rngs rests drests arrs) f-stx args-stx + ;; only try inference if the argument lengths are appropriate + (lambda (dom _ rest drest a) + (cond [rest (<= (length dom) (length argtys))] + [drest (and (<= (length dom) (length argtys)) + (eq? dotted-var (cdr drest)))] + [else (= (length dom) (length argtys))])) + ;; only try to infer the free vars of the rng (which includes the vars in filters/objects) + ;; note that we have to use argtys-t here, since argtys is a list of tc-results + (lambda (dom rng rest drest a) + (if drest + (infer/dots fixed-vars dotted-var argtys-t dom (car drest) rng (fv rng) + #:expected (and expected (tc-results->values expected))) + (infer/vararg vars argtys-t dom rest rng (fv rng) + (and expected (tc-results->values expected))))) + t argtys expected)] + ;; regular polymorphic functions without dotted rest, and without mandatory keyword args [((tc-result1: (and t - (or (Poly: - vars - (Function: (list (and arrs (arr: doms rngs rests (and drests #f) (list (Keyword: _ _ #f) ...))) ...))) - (PolyDots: - vars - (Function: (list (and arrs (arr: doms rngs rests (and drests #f) (list (Keyword: _ _ #f) ...))) ...)))))) + (Poly: + vars + (Function: (list (and arrs (arr: doms rngs rests (and drests #f) (list (Keyword: _ _ #f) ...))) ...))))) (list (tc-result1: argtys-t) ...)) (handle-clauses (doms rngs rests arrs) f-stx args-stx ;; only try inference if the argument lengths are appropriate @@ -623,17 +641,6 @@ ;; note that we have to use argtys-t here, since argtys is a list of tc-results (lambda (dom rng rest a) (infer/vararg vars argtys-t dom rest rng (fv rng) (and expected (tc-results->values expected)))) t argtys expected)] - ;; polymorphic ... type - [((tc-result1: (and t (PolyDots: - (and vars (list fixed-vars ... dotted-var)) - (Function: (list (and arrs (arr: doms rngs (and #f rests) (cons dtys dbounds) (list (Keyword: _ _ #f) ...))) ...))))) - (list (tc-result1: argtys-t) ...)) - (handle-clauses (doms dtys dbounds rngs arrs) f-stx args-stx - (lambda (dom dty dbound rng arr) (and (<= (length dom) (length argtys)) - (eq? dotted-var dbound))) - (lambda (dom dty dbound rng arr) - (infer/dots fixed-vars dotted-var argtys-t dom dty rng (fv rng) #:expected (and expected (tc-results->values expected)))) - t argtys expected)] ;; procedural structs [((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)] diff --git a/collects/typed-scheme/types/abbrev.ss b/collects/typed-scheme/types/abbrev.ss index 4ebd614f..ea31a542 100644 --- a/collects/typed-scheme/types/abbrev.ss +++ b/collects/typed-scheme/types/abbrev.ss @@ -2,7 +2,7 @@ (require "../utils/utils.ss") -(require (rep type-rep object-rep filter-rep) +(require (except-in (rep type-rep object-rep filter-rep rep-utils) Dotted) "printer.ss" "utils.ss" (utils tc-utils) scheme/list @@ -15,8 +15,17 @@ (provide (all-defined-out) (rename-out [make-Listof -lst])) -;; convenient constructors +(define (add-name type name) + (define-values (struct-type skipped?) (struct-info type)) + (define mk (struct-type-make-constructor struct-type)) + (define flds (vector->list (struct->vector type))) + (when skipped? + (error "shouldn't skip")) + (match flds + [(list* _ fld1 fld2 old-name flds) + (apply mk fld1 fld2 (or old-name name) flds)])) +;; convenient constructors (define -App make-App) (define -pair make-Pair) @@ -121,7 +130,7 @@ (define -Zero (-val 0)) (define -Real (*Un -Flonum -ExactRational)) -(define -ExactNonnegativeInteger (*Un -Zero -ExactPositiveInteger)) +(define -ExactNonnegativeInteger (*Un -ExactPositiveInteger -Zero)) (define -Nat -ExactNonnegativeInteger) (define -Byte -Number) diff --git a/collects/typed-scheme/types/convenience.ss b/collects/typed-scheme/types/convenience.ss index f281022b..17fb639e 100644 --- a/collects/typed-scheme/types/convenience.ss +++ b/collects/typed-scheme/types/convenience.ss @@ -46,19 +46,19 @@ (define In-Syntax (-mu e - (*Un -Number -Boolean -Symbol -String -Keyword -Char + (*Un -Boolean -Symbol -String -Keyword -Char -Number (make-Vector (-Syntax e)) (make-Box (-Syntax e)) (-mu list (*Un (-val '()) (-pair (-Syntax e) - (*Un (-Syntax e) list))))))) + (*Un list (-Syntax e)))))))) (define Any-Syntax (-Syntax In-Syntax)) (define (-Sexpof t) (-mu sexp - (Un -Number -Boolean -Symbol -String -Keyword -Char + (Un -Boolean -Symbol -String -Keyword -Char -Number (-val '()) (-pair sexp sexp) (make-Vector sexp) diff --git a/collects/typed-scheme/types/printer.ss b/collects/typed-scheme/types/printer.ss index 33d6602b..ac650fdb 100644 --- a/collects/typed-scheme/types/printer.ss +++ b/collects/typed-scheme/types/printer.ss @@ -131,6 +131,7 @@ [(Value: '()) null])) (match c [(Univ:) (fp "Any")] + [(? Type-name) (fp "~a" (Type-name c))] [(? has-name?) (fp "~a" (has-name? c))] ;; names are just the printed as the original syntax [(Name: stx) (fp "~a" (syntax-e stx))] diff --git a/collects/typed-scheme/types/remove-intersect.ss b/collects/typed-scheme/types/remove-intersect.ss index 1dce9f4d..8400f7e6 100644 --- a/collects/typed-scheme/types/remove-intersect.ss +++ b/collects/typed-scheme/types/remove-intersect.ss @@ -1,7 +1,8 @@ #lang scheme/base (require "../utils/utils.ss" - (rep type-rep rep-utils) + (rep type-rep) + (only-in (rep rep-utils) Type-key) (types union subtype resolve convenience utils) scheme/match mzlib/trace) diff --git a/collects/typed-scheme/types/subtype.ss b/collects/typed-scheme/types/subtype.ss index be894406..a41c83f3 100644 --- a/collects/typed-scheme/types/subtype.ss +++ b/collects/typed-scheme/types/subtype.ss @@ -1,6 +1,6 @@ #lang scheme/base (require "../utils/utils.ss" - (rep type-rep filter-rep object-rep rep-utils) + (except-in (rep type-rep filter-rep object-rep rep-utils) Dotted) (utils tc-utils) (types utils comparison resolve abbrev) (env type-name-env) diff --git a/collects/typed-scheme/types/union.ss b/collects/typed-scheme/types/union.ss index 5019cada..d71a07a6 100644 --- a/collects/typed-scheme/types/union.ss +++ b/collects/typed-scheme/types/union.ss @@ -2,7 +2,7 @@ (require "../utils/utils.ss") -(require (rep type-rep rep-utils) +(require (rep type-rep) (utils tc-utils) (types utils subtype abbrev printer comparison) scheme/match mzlib/trace) diff --git a/collects/typed-scheme/types/utils.ss b/collects/typed-scheme/types/utils.ss index affbc234..10b08828 100644 --- a/collects/typed-scheme/types/utils.ss +++ b/collects/typed-scheme/types/utils.ss @@ -2,9 +2,8 @@ (require "../utils/utils.ss") -(require (rep type-rep filter-rep object-rep rep-utils) +(require (except-in (rep type-rep filter-rep object-rep rep-utils) Dotted) (utils tc-utils) - (only-in (rep free-variance) combine-frees) scheme/match scheme/list mzlib/trace diff --git a/collects/typed-scheme/utils/utils.ss b/collects/typed-scheme/utils/utils.ss index 8300d461..77f5ae15 100644 --- a/collects/typed-scheme/utils/utils.ss +++ b/collects/typed-scheme/utils/utils.ss @@ -145,7 +145,7 @@ at least theoretically. ;; - 1 printers have to be defined at the same time as the structs ;; - 2 we want to support things printing corectly even when the custom printer is off -(define-for-syntax printing? #t) +(define-for-syntax printing? #f) (define-syntax-rule (defprinter t ...) (begin @@ -170,16 +170,16 @@ at least theoretically. (define-syntax (define-struct/printer stx) (syntax-case stx () - [(form name (flds ...) printer) + [(form name (flds ...) printer . props) #`(define-struct/properties name (flds ...) #,(if printing? - #'([prop:custom-write (lambda (a b c) (if (custom-printer) (printer a b c) (pseudo-printer a b c)))]) - #'([prop:custom-write pseudo-printer])) + #'([prop:custom-write (lambda (a b c) (if (custom-printer) (printer a b c) (pseudo-printer a b c)))] . props) + #'([prop:custom-write pseudo-printer] . props)) #f)])) ;; turn contracts on and off - off by default for performance. -(define-for-syntax enable-contracts? #f) +(define-for-syntax enable-contracts? #t) (provide (for-syntax enable-contracts?) p/c w/c cnt d-s/c d/c) ;; these are versions of the contract forms conditionalized by `enable-contracts?' diff --git a/collects/typed/net/cgi.ss b/collects/typed/net/cgi.ss index 9318478a..ee070c78 100644 --- a/collects/typed/net/cgi.ss +++ b/collects/typed/net/cgi.ss @@ -3,6 +3,7 @@ (require typed/private/utils) (require-typed-struct cgi-error () net/cgi) + (require-typed-struct (incomplete-%-suffix cgi-error) ([chars : (Listof Char)]) net/cgi) (require-typed-struct (invalid-%-suffix cgi-error) ([char : Char]) net/cgi) From 1261ce2cdbfeca5d7ae5bbee7bb973377a41dc5e Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Thu, 10 Dec 2009 17:15:17 +0000 Subject: [PATCH 12/17] revert all of the interning changes since they didn't work svn: r17262 original commit: 16c152e5a4ca1797f20c127d443e4689e292e55f --- collects/typed-scheme/env/init-envs.ss | 25 ++- collects/typed-scheme/infer/promote-demote.ss | 2 +- collects/typed-scheme/private/parse-type.ss | 4 +- collects/typed-scheme/rep/free-variance.ss | 103 +++++++++ collects/typed-scheme/rep/interning.ss | 9 +- collects/typed-scheme/rep/rep-utils.ss | 197 +++--------------- collects/typed-scheme/rep/type-rep.ss | 47 ++--- collects/typed-scheme/types/abbrev.ss | 15 +- collects/typed-scheme/types/convenience.ss | 6 +- collects/typed-scheme/types/printer.ss | 1 - .../typed-scheme/types/remove-intersect.ss | 3 +- collects/typed-scheme/types/subtype.ss | 2 +- collects/typed-scheme/types/union.ss | 2 +- collects/typed-scheme/types/utils.ss | 3 +- collects/typed-scheme/utils/utils.ss | 10 +- 15 files changed, 185 insertions(+), 244 deletions(-) diff --git a/collects/typed-scheme/env/init-envs.ss b/collects/typed-scheme/env/init-envs.ss index a92069c7..73d1a9a1 100644 --- a/collects/typed-scheme/env/init-envs.ss +++ b/collects/typed-scheme/env/init-envs.ss @@ -22,28 +22,27 @@ (define (gen-constructor sym) (string->symbol (string-append "make-" (substring (symbol->string sym) 7)))) (match v - [(Union: elems) `(make-Union (sort (list ,@(map sub elems)) < #:key Type-seq) ',(Type-name v))] - [(Base: n cnt) `(make-Base ',n (quote-syntax ,cnt) ',(Type-name v))] - [(Name: stx) `(make-Name (quote-syntax ,stx) ',(Type-name v))] + [(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) - `(make-Struct ,(sub name) ,(sub parent) ,(sub flds) ,(sub proc) ,(sub poly?) (quote-syntax ,pred-id) (syntax-local-certifier) ',(Type-name v))] - [(App: rator rands stx) `(make-App ,(sub rator) ,(sub rands) (quote-syntax ,stx) ',(Type-name v))] - [(Opaque: pred cert) `(make-Opaque (quote-syntax ,pred) (syntax-local-certifier) ',(Type-name v))] + `(make-Struct ,(sub name) ,(sub parent) ,(sub flds) ,(sub proc) ,(sub poly?) (quote-syntax ,pred-id) (syntax-local-certifier))] + [(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) (quote-syntax ,pred) - (syntax-local-certifier) - ',(Type-name v))] - [(Mu-name: n b) `(make-Mu ,(sub n) ,(sub b) ',(Type-name v))] - [(Poly-names: ns b) `(make-Poly (list ,@(map sub ns)) ,(sub b) ',(Type-name v))] - [(PolyDots-names: ns b) `(make-PolyDots (list ,@(map sub ns)) ,(sub b) ',(Type-name v))] + (syntax-local-certifier))] + [(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) (PathElem? e))) (app (lambda (v) (vector->list (struct->vector v))) (list-rest tag seq vals))) `(,(gen-constructor tag) ,@(map sub vals))] [(? (lambda (e) (or (Type? e))) - (app (lambda (v) (vector->list (struct->vector v))) (list-rest tag key seq name vals))) - `(,(gen-constructor tag) ,@(map sub vals) ',name)] + (app (lambda (v) (vector->list (struct->vector v))) (list-rest tag key seq vals))) + `(,(gen-constructor tag) ,@(map sub vals))] [_ (basic v)])) (define (bound-in-this-module id) diff --git a/collects/typed-scheme/infer/promote-demote.ss b/collects/typed-scheme/infer/promote-demote.ss index 316ed06b..1eb261f1 100644 --- a/collects/typed-scheme/infer/promote-demote.ss +++ b/collects/typed-scheme/infer/promote-demote.ss @@ -1,7 +1,7 @@ #lang scheme/unit (require "../utils/utils.ss") -(require (rep type-rep) +(require (rep type-rep rep-utils) (types convenience union utils) "signatures.ss" scheme/list scheme/match) diff --git a/collects/typed-scheme/private/parse-type.ss b/collects/typed-scheme/private/parse-type.ss index d0756184..ffc9a56c 100644 --- a/collects/typed-scheme/private/parse-type.ss +++ b/collects/typed-scheme/private/parse-type.ss @@ -260,12 +260,12 @@ (lambda (t) ;(printf "found a type alias ~a~n" #'id) (add-type-name-reference #'id) - t #;(add-name t (syntax-e #'id)))] + t)] ;; if it's a type name, we just use the name [(lookup-type-name #'id (lambda () #f)) (add-type-name-reference #'id) ;(printf "found a type name ~a~n" #'id) - (add-name (make-Name #'id) (syntax-e #'id))] + (make-Name #'id)] [(free-identifier=? #'id #'t:->) (tc-error/delayed "Incorrect use of -> type constructor") Err] diff --git a/collects/typed-scheme/rep/free-variance.ss b/collects/typed-scheme/rep/free-variance.ss index c53a5086..7e4014e3 100644 --- a/collects/typed-scheme/rep/free-variance.ss +++ b/collects/typed-scheme/rep/free-variance.ss @@ -1 +1,104 @@ #lang scheme/base +(require "../utils/utils.ss") + +(require (for-syntax scheme/base) + (utils tc-utils) + mzlib/etc) + +;; this file contains support for calculating the free variables/indexes of types +;; actual computation is done in rep-utils.ss and type-rep.ss + +(define-values (Covariant Contravariant Invariant Constant Dotted) + (let () + (define-struct Variance () #:inspector #f) + (define-struct (Covariant Variance) () #:inspector #f) + (define-struct (Contravariant Variance) () #:inspector #f) + (define-struct (Invariant Variance) () #:inspector #f) + (define-struct (Constant Variance) () #:inspector #f) + ;; not really a variance, but is disjoint with the others + (define-struct (Dotted Variance) () #:inspector #f) + (values (make-Covariant) (make-Contravariant) (make-Invariant) (make-Constant) (make-Dotted)))) + + +(provide Covariant Contravariant Invariant Constant Dotted) + +;; hashtables for keeping track of free variables and indexes +(define index-table (make-weak-hasheq)) +;; maps Type to List[Cons[Number,Variance]] +(define var-table (make-weak-hasheq)) +;; maps Type to List[Cons[Symbol,Variance]] + +(define (free-idxs* t) (hash-ref index-table t (lambda _ (int-err "type ~a not in index-table" (syntax-e t))))) +(define (free-vars* t) (hash-ref var-table t (lambda _ (int-err "type ~a not in var-table" (syntax-e t))))) + + +(define empty-hash-table (make-immutable-hasheq null)) + +(provide free-vars* free-idxs* empty-hash-table make-invariant) + +;; frees = HT[Idx,Variance] where Idx is either Symbol or Number +;; (listof frees) -> frees +(define (combine-frees freess) + (define ht (make-hasheq)) + (define (combine-var v w) + (cond + [(eq? v w) v] + [(eq? v Dotted) w] + [(eq? w Dotted) v] + [(eq? v Constant) w] + [(eq? w Constant) v] + [else Invariant])) + (for* ([old-ht (in-list freess)] + [(sym var) (in-hash old-ht)]) + (let* ([sym-var (hash-ref ht sym (lambda () #f))]) + (if sym-var + (hash-set! ht sym (combine-var var sym-var)) + (hash-set! ht sym var)))) + ht) + +;; given a set of free variables, change bound to ... +;; (if bound wasn't free, this will add it as Dotted +;; appropriately so that things that expect to see +;; it as "free" will -- fixes the case where the +;; dotted pre-type base doesn't use the bound). +(define (fix-bound vs bound) + (define vs* (hash-map* (lambda (k v) v) vs)) + (hash-set! vs* bound Dotted) + vs*) + +;; frees -> frees +(define (flip-variances vs) + (hash-map* + (lambda (k v) + (evcase + v + [Covariant Contravariant] + [Contravariant Covariant] + [v v])) + vs)) + +(define (make-invariant vs) + (hash-map* + (lambda (k v) Invariant) + vs)) + +(define (hash-map* f ht) + (define new-ht (make-hasheq)) + (for ([(k v) (in-hash ht)]) + (hash-set! new-ht k (f k v))) + new-ht) + +(define (without-below n frees) + (define new-ht (make-hasheq)) + (for ([(k v) (in-hash frees)]) + (when (>= k n) (hash-set! new-ht k v))) + new-ht) + +(provide combine-frees flip-variances without-below unless-in-table var-table index-table empty-hash-table + fix-bound) + +(define-syntax (unless-in-table stx) + (syntax-case stx () + [(_ table val . body) + (quasisyntax/loc stx + (hash-ref table val #,(syntax/loc #'body (lambda () . body))))])) diff --git a/collects/typed-scheme/rep/interning.ss b/collects/typed-scheme/rep/interning.ss index a370b34d..3dfd9aef 100644 --- a/collects/typed-scheme/rep/interning.ss +++ b/collects/typed-scheme/rep/interning.ss @@ -14,9 +14,12 @@ #'(define *name (let ([table (make-ht)]) (lambda (arg ...) - (let* ([key key-expr] - [new-seq (hash-ref table key count!)]) - (make-name new-seq e ... arg ...)))))])) + (let ([key key-expr]) + (hash-ref table key + (lambda () + (let ([new (make-name (count!) e ... arg ...)]) + (hash-set! table key new) + new)))))))])) (define (make-count!) (let ([state 0]) diff --git a/collects/typed-scheme/rep/rep-utils.ss b/collects/typed-scheme/rep/rep-utils.ss index d1194589..ca994b19 100644 --- a/collects/typed-scheme/rep/rep-utils.ss +++ b/collects/typed-scheme/rep/rep-utils.ss @@ -2,8 +2,9 @@ (require "../utils/utils.ss") (require mzlib/struct - scheme/match scheme/list + scheme/match syntax/boundmap + "free-variance.ss" "interning.ss" unstable/syntax unstable/match mzlib/etc @@ -24,11 +25,9 @@ (provide == defintern hash-id (for-syntax fold-target)) - - (define-for-syntax fold-target #'fold-target) -(define-for-syntax (mk par ht-stx key? name?) +(define-for-syntax (mk par ht-stx key?) (define-syntax-class opt-cnt-id #:attributes (i cnt) (pattern i:id @@ -68,8 +67,6 @@ #:with e fold-target) (pattern ex:expr #:with e #'#'ex)) - (unless (equal? key? name?) - (error "key? not name")) (lambda (stx) (syntax-parse stx [(dform nm:id flds:idlist (~or @@ -88,7 +85,7 @@ [*maker (format-id #'nm "*~a" #'nm)] [**maker (format-id #'nm "**~a" #'nm)] [*maker-cnt (if enable-contracts? - (or (attribute cnt) #`((flds.cnt ...) #,(if name? #'(any/c) #'()) . ->* . pred)) + (or (attribute cnt) #'(flds.cnt ... . -> . pred)) #'any/c)] [ht-stx ht-stx] [bfs-fold-rhs (cond [(attribute fold-rhs) @@ -108,30 +105,26 @@ (p/c (rename *maker maker *maker-cnt))))] [intern (let ([mk (lambda (int) - (if (and key? name?) - #`(defintern (**maker name-val . flds.fs) maker #,int #:extra-arg #,(attribute key-expr)) - #`(defintern (**maker . flds.fs) maker #,int)))]) - (syntax-parse #'flds.fs - [_ #:fail-unless (attribute intern?) #f - (mk #'intern?)] - [() (mk #'#f)] - [(f) (mk #'f)] - [_ (mk #'(list . flds.fs))]))] - [(ign-pats ...) (if (and name? key?) #'(_ _ _) #'(_))] + (if key? + #`(defintern (**maker . flds.fs) maker #,int #:extra-arg #,(attribute key-expr)) + #`(defintern (**maker . flds.fs) maker #,int)))]) + (syntax-parse #'flds.fs + [_ #:fail-unless (attribute intern?) #f + (mk #'intern?)] + [() (mk #'#f)] + [(f) (mk #'f)] + [_ (mk #'(list . flds.fs))]))] + [(ign-pats ...) (if key? #'(_ _) #'(_))] [frees-def (if (attribute frees) #'frees.def #'(begin))] [frees (with-syntax ([(f1 f2) (if (attribute frees) #'(frees.f1 frees.f2) (list (combiner #'free-vars* #'flds.fs) - (combiner #'free-idxs* #'flds.fs)))] - [(fs ...) #'flds.fs] - [name-val-formal - (if name? #'([name-val #f]) #'())] - [name-val-expr (if name? #'(name-val) #'())]) + (combiner #'free-idxs* #'flds.fs)))]) (quasisyntax/loc stx (w/c nm ([*maker *maker-cnt]) - (define (*maker fs ... #,@#'name-val-formal) - (define v (**maker #,@#'name-val-expr fs ...)) + (define (*maker . flds.fs) + (define v (**maker . flds.fs)) frees-def (unless-in-table var-table v @@ -235,29 +228,23 @@ (define-syntax (make-prim-type stx) (define default-flds #'(seq)) (define-syntax-class type-name-base - #:attributes (i lower-s first-letter key? (fld-names 1) name?) + #:attributes (i lower-s first-letter key? (fld-names 1)) #:transparent (pattern i:id #:attr lower-s (string-downcase (symbol->string (attribute i.datum))) #:with (fld-names ...) default-flds #:with key? #'#f - #:with name? #'#f #:attr first-letter (string-ref (attribute lower-s) 0)) (pattern [i:id #:d d-name:id] #:with (fld-names ...) default-flds #:attr lower-s (string-downcase (symbol->string (attribute i.datum))) #:with key? #'#f - #:with name? #'#f #:attr first-letter (symbol->string (attribute d-name.datum))) - (pattern [i:id #:key (~optional (~and name-kw #:name))] + (pattern [i:id #:key] #:with (fld-names ...) (datum->syntax #f (append (syntax->list default-flds) - (list #'key) - (if (attribute name-kw) - (list #'name) - null))) + (syntax->list #'(key)))) #:attr lower-s (string-downcase (symbol->string (attribute i.datum))) #:with key? #'#t - #:with name? (if (attribute name-kw) #'#t #'#f) #:attr first-letter (string-ref (attribute lower-s) 0))) (define-syntax-class type-name #:transparent @@ -271,7 +258,7 @@ #:with ht (format-id #'i "~a-name-ht" (attribute lower-s)) #:with rec-id (format-id #'i "~a-rec-id" (attribute lower-s)) #:with d-id (format-id #'i "d~a" (attribute first-letter)) - #:with (_ _ pred? seq-acc accs ...) + #:with (_ _ pred? accs ...) (datum->syntax #f (build-struct-names #'name (syntax->list #'(fld-names ...)) #f #t #'name)))) (syntax-parse stx [(_ i:type-name ...) @@ -280,15 +267,11 @@ [fresh-ids-list #'(fresh-ids ...)] [(anys ...) (for/list ([i (syntax->list #'fresh-ids-list)]) #'any/c)]) #'(begin - (provide i.d-id ... i.printer ... i.name ... i.pred? ... i.seq-acc ... i.accs ... ... + (provide i.d-id ... i.printer ... i.name ... i.pred? ... i.accs ... ... (for-syntax i.ht ... i.rec-id ...)) - (define-syntax i.d-id (mk #'i.name #'i.ht i.key? i.name?)) ... + (define-syntax i.d-id (mk #'i.name #'i.ht i.key?)) ... (define-for-syntax i.ht (make-hasheq)) ... - (define-struct/printer i.name (i.fld-names ...) (lambda (a b c) ((unbox i.printer) a b c)) - [prop:equal+hash (list (lambda (a b rec) - (eq? (i.seq-acc a) (i.seq-acc b))) - (lambda (a rec) (i.seq-acc a)) - (lambda (a secondary) (secondary a)))]) ... + (define-struct/printer i.name (i.fld-names ...) (lambda (a b c) ((unbox i.printer) a b c))) ... (define-for-syntax i.rec-id #'i.rec-id) ... (provide i.case ...) (define-syntaxes (i.case ...) @@ -301,139 +284,9 @@ '(i.keyword ...))) (list i.ht ...)))))))])) -(make-prim-type [Type #:key #:name] +(make-prim-type [Type #:key] Filter [LatentFilter #:d lf] Object [LatentObject #:d lo] [PathElem #:d pe]) - -;; free-variance.ss starts here: - -(require "../utils/utils.ss") - -(require (for-syntax scheme/base) - (utils tc-utils) - scheme/contract - mzlib/etc) - -;; this file contains support for calculating the free variables/indexes of types -;; actual computation is done in rep-utils.ss and type-rep.ss - -(define-values (Covariant Contravariant Invariant Constant Dotted) - (let () - (define-struct Variance () #:inspector #f) - (define-struct (Covariant Variance) () #:inspector #f) - (define-struct (Contravariant Variance) () #:inspector #f) - (define-struct (Invariant Variance) () #:inspector #f) - (define-struct (Constant Variance) () #:inspector #f) - ;; not really a variance, but is disjoint with the others - (define-struct (Dotted Variance) () #:inspector #f) - (values (make-Covariant) (make-Contravariant) (make-Invariant) (make-Constant) (make-Dotted)))) - -(define (variance? e) - (memq e (list Covariant Contravariant Invariant Constant Dotted))) - - -(provide Covariant Contravariant Invariant Constant Dotted) - -;; hashtables for keeping track of free variables and indexes -(define index-table (make-weak-hash)) -;; maps Type to List[Cons[Number,Variance]] -(define var-table (make-weak-hash)) -;; maps Type to List[Cons[Symbol,Variance]] - -(define input/c (or/c Type? Filter? LatentFilter? Object? LatentObject? PathElem?)) - -(d/c (free-idxs* t) - (-> input/c (hash/c integer? variance?)) - (hash-ref index-table t (lambda _ (int-err "type ~a not in index-table" t)))) -(d/c (free-vars* t) - (-> input/c (hash/c symbol? variance?)) - (hash-ref var-table t (lambda _ (int-err "type ~a not in var-table ~a" t (take (reverse (hash-map var-table list)) 20))))) - - -(define empty-hash-table (make-immutable-hasheq null)) - -;; Type? is not available here! grrr -(p/c - [free-vars* (-> input/c (hash/c symbol? variance?))] - [free-idxs* (-> input/c (hash/c integer? variance?))]) - -(provide empty-hash-table) - -;; frees = HT[Idx,Variance] where Idx is either Symbol or Number -;; (listof frees) -> frees -(define (combine-frees freess) - (define ht (make-hasheq)) - (define (combine-var v w) - (cond - [(eq? v w) v] - [(eq? v Dotted) w] - [(eq? w Dotted) v] - [(eq? v Constant) w] - [(eq? w Constant) v] - [else Invariant])) - (for* ([old-ht (in-list freess)] - [(sym var) (in-hash old-ht)]) - (let* ([sym-var (hash-ref ht sym (lambda () #f))]) - (if sym-var - (hash-set! ht sym (combine-var var sym-var)) - (hash-set! ht sym var)))) - ht) - -;; given a set of free variables, change bound to ... -;; (if bound wasn't free, this will add it as Dotted -;; appropriately so that things that expect to see -;; it as "free" will -- fixes the case where the -;; dotted pre-type base doesn't use the bound). -(define (fix-bound vs bound) - (define vs* (hash-map* (lambda (k v) v) vs)) - (hash-set! vs* bound Dotted) - vs*) - -;; frees -> frees -(define (flip-variances vs) - (hash-map* - (lambda (k v) - (evcase - v - [Covariant Contravariant] - [Contravariant Covariant] - [v v])) - vs)) - -(define (make-invariant vs) - (hash-map* - (lambda (k v) Invariant) - vs)) - -(define (hash-map* f ht) - (define new-ht (make-hasheq)) - (for ([(k v) (in-hash ht)]) - (hash-set! new-ht k (f k v))) - new-ht) - -(define (without-below n frees) - (define new-ht (make-hasheq)) - (for ([(k v) (in-hash frees)]) - (when (>= k n) (hash-set! new-ht k v))) - new-ht) - -(define table/c (hash/c (or/c integer? symbol?) variance?)) - -(p/c [combine-frees (-> (listof table/c) table/c)] - [flip-variances (-> table/c table/c)] - [make-invariant (-> table/c table/c)] - [without-below (-> integer? table/c table/c)]) - -(provide unless-in-table var-table index-table empty-hash-table fix-bound) - -(define-syntax (unless-in-table stx) - (syntax-case stx () - [(_ table val . body) - (quasisyntax/loc stx - (hash-ref table val #,(syntax/loc #'body (lambda () . body))))])) - - -;; free-variance.ss ends here diff --git a/collects/typed-scheme/rep/type-rep.ss b/collects/typed-scheme/rep/type-rep.ss index 2e28f10a..5db6f744 100644 --- a/collects/typed-scheme/rep/type-rep.ss +++ b/collects/typed-scheme/rep/type-rep.ss @@ -28,8 +28,6 @@ ;; t must be a Type (dt Scope ([t (or/c Type/c Scope?)]) [#:key (Type-key t)]) - - (define (scope-depth k) (flat-named-contract (format "Scope of depth ~a" k) @@ -102,7 +100,7 @@ (dt Poly (n body) #:no-provide [#:contract (->d ([n natural-number/c] [body (scope-depth n)]) - ([_ any/c]) + () [result Poly?])] [#:frees (free-vars* body) (without-below n (free-idxs* body))] [#:fold-rhs (let ([body* (remove-scopes n body)]) @@ -115,7 +113,7 @@ (dt PolyDots (n body) #:no-provide [#:contract (->d ([n natural-number/c] [body (scope-depth n)]) - ([_ any/c]) + () [result PolyDots?])] [#:key (Type-key body)] [#:frees (free-vars* body) (without-below n (free-idxs* body))] @@ -231,21 +229,17 @@ ;; elems : Listof[Type] (dt Union ([elems (and/c (listof Type/c) - (flat-named-contract - 'sorted-types - (lambda (es) - (let-values ([(sorted? k) - (for/fold ([sorted? #t] - [last -1]) - ([e es]) - (let ([seq (Type-seq e)]) - (values - (and sorted? - (< last seq)) - seq)))]) - (unless sorted? - (printf "seqs ~a~n" (map Type-seq es))) - sorted?))))]) + (lambda (es) + (let-values ([(sorted? k) + (for/fold ([sorted? #t] + [last -1]) + ([e es]) + (let ([seq (Type-seq e)]) + (values + (and sorted? + (< last seq)) + seq)))]) + sorted?)))]) [#:frees (combine-frees (map free-vars* elems)) (combine-frees (map free-idxs* elems))] [#:fold-rhs ((get-union-maker) (map type-rec-id elems))] @@ -347,7 +341,7 @@ [_ (int-err "Tried to remove too many scopes: ~a" sc)]))) ;; type equality -(define (type-equal? t1 t2) (eq? (Type-seq t1) (Type-seq t2))) +(define type-equal? eq?) ;; inequality - good @@ -471,8 +465,8 @@ #;(trace instantiate-many abstract-many) ;; the 'smart' constructor -(define (Mu* name body [print-name #f]) - (let ([v (*Mu (abstract name body) print-name)]) +(define (Mu* name body) + (let ([v (*Mu (abstract name body))]) (hash-set! name-table v name) v)) @@ -483,9 +477,9 @@ (instantiate (*F name) scope)])) ;; the 'smart' constructor -(define (Poly* names body [print-name #f]) +(define (Poly* names body) (if (null? names) body - (let ([v (*Poly (length names) (abstract-many names body) print-name)]) + (let ([v (*Poly (length names) (abstract-many names body))]) (hash-set! name-table v names) v))) @@ -498,9 +492,9 @@ (instantiate-many (map *F names) scope)])) ;; the 'smart' constructor -(define (PolyDots* names body [print-name #f]) +(define (PolyDots* names body) (if (null? names) body - (let ([v (*PolyDots (length names) (abstract-many names body) print-name)]) + (let ([v (*PolyDots (length names) (abstract-many names body))]) (hash-set! name-table v names) v))) @@ -616,7 +610,6 @@ remove-dups sub-lf sub-lo sub-pe Values: Values? Values-rs - Type-key Type-seq Type-name type-case (rename-out [Mu:* Mu:] [Poly:* Poly:] [PolyDots:* PolyDots:] diff --git a/collects/typed-scheme/types/abbrev.ss b/collects/typed-scheme/types/abbrev.ss index ea31a542..4ebd614f 100644 --- a/collects/typed-scheme/types/abbrev.ss +++ b/collects/typed-scheme/types/abbrev.ss @@ -2,7 +2,7 @@ (require "../utils/utils.ss") -(require (except-in (rep type-rep object-rep filter-rep rep-utils) Dotted) +(require (rep type-rep object-rep filter-rep) "printer.ss" "utils.ss" (utils tc-utils) scheme/list @@ -15,18 +15,9 @@ (provide (all-defined-out) (rename-out [make-Listof -lst])) -(define (add-name type name) - (define-values (struct-type skipped?) (struct-info type)) - (define mk (struct-type-make-constructor struct-type)) - (define flds (vector->list (struct->vector type))) - (when skipped? - (error "shouldn't skip")) - (match flds - [(list* _ fld1 fld2 old-name flds) - (apply mk fld1 fld2 (or old-name name) flds)])) - ;; convenient constructors + (define -App make-App) (define -pair make-Pair) (define -mpair make-MPair) @@ -130,7 +121,7 @@ (define -Zero (-val 0)) (define -Real (*Un -Flonum -ExactRational)) -(define -ExactNonnegativeInteger (*Un -ExactPositiveInteger -Zero)) +(define -ExactNonnegativeInteger (*Un -Zero -ExactPositiveInteger)) (define -Nat -ExactNonnegativeInteger) (define -Byte -Number) diff --git a/collects/typed-scheme/types/convenience.ss b/collects/typed-scheme/types/convenience.ss index 17fb639e..f281022b 100644 --- a/collects/typed-scheme/types/convenience.ss +++ b/collects/typed-scheme/types/convenience.ss @@ -46,19 +46,19 @@ (define In-Syntax (-mu e - (*Un -Boolean -Symbol -String -Keyword -Char -Number + (*Un -Number -Boolean -Symbol -String -Keyword -Char (make-Vector (-Syntax e)) (make-Box (-Syntax e)) (-mu list (*Un (-val '()) (-pair (-Syntax e) - (*Un list (-Syntax e)))))))) + (*Un (-Syntax e) list))))))) (define Any-Syntax (-Syntax In-Syntax)) (define (-Sexpof t) (-mu sexp - (Un -Boolean -Symbol -String -Keyword -Char -Number + (Un -Number -Boolean -Symbol -String -Keyword -Char (-val '()) (-pair sexp sexp) (make-Vector sexp) diff --git a/collects/typed-scheme/types/printer.ss b/collects/typed-scheme/types/printer.ss index ac650fdb..33d6602b 100644 --- a/collects/typed-scheme/types/printer.ss +++ b/collects/typed-scheme/types/printer.ss @@ -131,7 +131,6 @@ [(Value: '()) null])) (match c [(Univ:) (fp "Any")] - [(? Type-name) (fp "~a" (Type-name c))] [(? has-name?) (fp "~a" (has-name? c))] ;; names are just the printed as the original syntax [(Name: stx) (fp "~a" (syntax-e stx))] diff --git a/collects/typed-scheme/types/remove-intersect.ss b/collects/typed-scheme/types/remove-intersect.ss index 8400f7e6..1dce9f4d 100644 --- a/collects/typed-scheme/types/remove-intersect.ss +++ b/collects/typed-scheme/types/remove-intersect.ss @@ -1,8 +1,7 @@ #lang scheme/base (require "../utils/utils.ss" - (rep type-rep) - (only-in (rep rep-utils) Type-key) + (rep type-rep rep-utils) (types union subtype resolve convenience utils) scheme/match mzlib/trace) diff --git a/collects/typed-scheme/types/subtype.ss b/collects/typed-scheme/types/subtype.ss index a41c83f3..be894406 100644 --- a/collects/typed-scheme/types/subtype.ss +++ b/collects/typed-scheme/types/subtype.ss @@ -1,6 +1,6 @@ #lang scheme/base (require "../utils/utils.ss" - (except-in (rep type-rep filter-rep object-rep rep-utils) Dotted) + (rep type-rep filter-rep object-rep rep-utils) (utils tc-utils) (types utils comparison resolve abbrev) (env type-name-env) diff --git a/collects/typed-scheme/types/union.ss b/collects/typed-scheme/types/union.ss index d71a07a6..5019cada 100644 --- a/collects/typed-scheme/types/union.ss +++ b/collects/typed-scheme/types/union.ss @@ -2,7 +2,7 @@ (require "../utils/utils.ss") -(require (rep type-rep) +(require (rep type-rep rep-utils) (utils tc-utils) (types utils subtype abbrev printer comparison) scheme/match mzlib/trace) diff --git a/collects/typed-scheme/types/utils.ss b/collects/typed-scheme/types/utils.ss index 10b08828..affbc234 100644 --- a/collects/typed-scheme/types/utils.ss +++ b/collects/typed-scheme/types/utils.ss @@ -2,8 +2,9 @@ (require "../utils/utils.ss") -(require (except-in (rep type-rep filter-rep object-rep rep-utils) Dotted) +(require (rep type-rep filter-rep object-rep rep-utils) (utils tc-utils) + (only-in (rep free-variance) combine-frees) scheme/match scheme/list mzlib/trace diff --git a/collects/typed-scheme/utils/utils.ss b/collects/typed-scheme/utils/utils.ss index 77f5ae15..8300d461 100644 --- a/collects/typed-scheme/utils/utils.ss +++ b/collects/typed-scheme/utils/utils.ss @@ -145,7 +145,7 @@ at least theoretically. ;; - 1 printers have to be defined at the same time as the structs ;; - 2 we want to support things printing corectly even when the custom printer is off -(define-for-syntax printing? #f) +(define-for-syntax printing? #t) (define-syntax-rule (defprinter t ...) (begin @@ -170,16 +170,16 @@ at least theoretically. (define-syntax (define-struct/printer stx) (syntax-case stx () - [(form name (flds ...) printer . props) + [(form name (flds ...) printer) #`(define-struct/properties name (flds ...) #,(if printing? - #'([prop:custom-write (lambda (a b c) (if (custom-printer) (printer a b c) (pseudo-printer a b c)))] . props) - #'([prop:custom-write pseudo-printer] . props)) + #'([prop:custom-write (lambda (a b c) (if (custom-printer) (printer a b c) (pseudo-printer a b c)))]) + #'([prop:custom-write pseudo-printer])) #f)])) ;; turn contracts on and off - off by default for performance. -(define-for-syntax enable-contracts? #t) +(define-for-syntax enable-contracts? #f) (provide (for-syntax enable-contracts?) p/c w/c cnt d-s/c d/c) ;; these are versions of the contract forms conditionalized by `enable-contracts?' From 21f9c0ec16eb412cc316e4f4c6d4a07787ba4419 Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Fri, 11 Dec 2009 00:25:59 +0000 Subject: [PATCH 13/17] fixes svn: r17265 original commit: 791ec557876881eaeafc29a43b339b7a7d632d84 --- collects/tests/typed-scheme/succeed/logic.ss | 2 -- collects/tests/typed-scheme/unit-tests/subtype-tests.ss | 2 +- collects/typed-scheme/rep/filter-rep.ss | 6 +++--- collects/typed-scheme/typecheck/tc-metafunctions.ss | 9 +++++---- collects/typed-scheme/types/abbrev.ss | 1 - collects/typed-scheme/types/printer.ss | 6 ++++-- collects/typed-scheme/utils/utils.ss | 2 +- 7 files changed, 14 insertions(+), 14 deletions(-) diff --git a/collects/tests/typed-scheme/succeed/logic.ss b/collects/tests/typed-scheme/succeed/logic.ss index 34f3fd0a..c21abe72 100644 --- a/collects/tests/typed-scheme/succeed/logic.ss +++ b/collects/tests/typed-scheme/succeed/logic.ss @@ -2,7 +2,6 @@ #lang typed-scheme (: f ((U Number #f) (cons Any Any) -> Number)) - (define (f x y) (cond [(and (number? x) (number? (car y))) (+ x (car y))] @@ -11,6 +10,5 @@ [else 0])) (: bool-to-0-or-1 (Boolean -> Number)) - (define (bool-to-0-or-1 b) (if b 1 0)) \ No newline at end of file diff --git a/collects/tests/typed-scheme/unit-tests/subtype-tests.ss b/collects/tests/typed-scheme/unit-tests/subtype-tests.ss index c84dcce5..bb3be770 100644 --- a/collects/tests/typed-scheme/unit-tests/subtype-tests.ss +++ b/collects/tests/typed-scheme/unit-tests/subtype-tests.ss @@ -126,7 +126,7 @@ ;; polymorphic function types should be subtypes of the function top [(-poly (a) (a . -> . a)) top-func] - [(cl->* (-Number . -> . -String) (-Boolean . -> . -String)) ((Un -Number -Boolean) . -> . -String)] + [(cl->* (-Number . -> . -String) (-Boolean . -> . -String)) ((Un -Boolean -Number) . -> . -String)] )) (define-go diff --git a/collects/typed-scheme/rep/filter-rep.ss b/collects/typed-scheme/rep/filter-rep.ss index 3c66be2a..56c0f41a 100644 --- a/collects/typed-scheme/rep/filter-rep.ss +++ b/collects/typed-scheme/rep/filter-rep.ss @@ -32,7 +32,7 @@ [#:fold-rhs (*NotTypeFilter (type-rec-id t) (map pathelem-rec-id p) v)]) ;; implication -(df ImpFilter ([a (listof Filter/c)] [c (listof Filter/c)]) +(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)))]) @@ -70,8 +70,8 @@ [#:fold-rhs (*LNotTypeFilter (type-rec-id t) (map pathelem-rec-id p) idx)]) ;; implication -(df LImpFilter ([a (listof LatentFilter/c)] [c (listof LatentFilter/c)]) - #;[#:frees (combine-frees (map free-vars* (append a c))) +(df LImpFilter ([a (non-empty-listof LatentFilter/c)] [c (non-empty-listof LatentFilter/c)]) + [#:frees (combine-frees (map free-vars* (append a c))) (combine-frees (map free-idxs* (append a c)))]) diff --git a/collects/typed-scheme/typecheck/tc-metafunctions.ss b/collects/typed-scheme/typecheck/tc-metafunctions.ss index 3d98e766..096f7a14 100644 --- a/collects/typed-scheme/typecheck/tc-metafunctions.ss +++ b/collects/typed-scheme/typecheck/tc-metafunctions.ss @@ -146,11 +146,12 @@ [((FilterSet: f1+ f1-) (T-FS:) (FilterSet: f3+ f3-)) (mk (combine null (append f1- f3-)))] ;; and [((FilterSet: f1+ f1-) (FilterSet: f2+ f2-) (F-FS:)) - (mk (combine (append f1+ f2+) - #;null - (append (for/list ([f f1-]) + (mk (combine (append f1+ f2+) + (append (for/list ([f f1-] + #:when (not (null? f2+))) (make-ImpFilter f2+ (list f))) - (for/list ([f f2-]) + (for/list ([f f2-] + #:when (not (null? f1+))) (make-ImpFilter f1+ (list f))))))] [(f f* f*) (mk f*)] [(_ _ _) diff --git a/collects/typed-scheme/types/abbrev.ss b/collects/typed-scheme/types/abbrev.ss index 04559f03..8d141416 100644 --- a/collects/typed-scheme/types/abbrev.ss +++ b/collects/typed-scheme/types/abbrev.ss @@ -261,7 +261,6 @@ (define true-filter (-FS (list) (list (make-Bot)))) (define false-filter (-FS (list (make-Bot)) (list))) - (define (opt-fn args opt-args result) (apply cl->* (for/list ([i (in-range (add1 (length opt-args)))]) (make-Function (list (make-arr* (append args (take opt-args i)) result)))))) diff --git a/collects/typed-scheme/types/printer.ss b/collects/typed-scheme/types/printer.ss index 33d6602b..beb0cad5 100644 --- a/collects/typed-scheme/types/printer.ss +++ b/collects/typed-scheme/types/printer.ss @@ -45,7 +45,8 @@ (fp")")] [(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")])) + [(LBot:) (fp "LBot")] + [(LImpFilter: a c) (fp "(LImpFilter ~a ~a)" a c)])) (define (print-filter c port write?) (define (fp . args) (apply fprintf port args)) @@ -57,7 +58,8 @@ [(NoFilter:) (fp "-")] [(NotTypeFilter: type path id) (fp "(! ~a @ ~a ~a)" type path (syntax-e id))] [(TypeFilter: type path id) (fp "(~a @ ~a ~a)" type path (syntax-e id))] - [(Bot:) (fp "Bot")])) + [(Bot:) (fp "Bot")] + [(ImpFilter: a c) (fp "(ImpFilter ~a ~a)" a c)])) (define (print-pathelem c port write?) (define (fp . args) (apply fprintf port args)) diff --git a/collects/typed-scheme/utils/utils.ss b/collects/typed-scheme/utils/utils.ss index 3fb7d363..ab40d625 100644 --- a/collects/typed-scheme/utils/utils.ss +++ b/collects/typed-scheme/utils/utils.ss @@ -145,7 +145,7 @@ at least theoretically. ;; - 1 printers have to be defined at the same time as the structs ;; - 2 we want to support things printing corectly even when the custom printer is off -(define-for-syntax printing? #f) +(define-for-syntax printing? #t) (define-syntax-rule (defprinter t ...) (begin From 09c67a3952247e9f7ea1f61cf1ee5c4022b31c85 Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Fri, 11 Dec 2009 17:01:55 +0000 Subject: [PATCH 14/17] fix unit tests svn: r17269 original commit: 3e497704aafae52c6c12ec7c45436573210212d9 --- .../unit-tests/typecheck-tests.ss | 26 +++++++++++++++---- 1 file changed, 21 insertions(+), 5 deletions(-) diff --git a/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss b/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss index a9e1d062..b5de92e5 100644 --- a/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss +++ b/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss @@ -161,7 +161,7 @@ [tc-e/t (values 3) -Pos] [tc-e (values) #:ret (ret null)] [tc-e (values 3 #f) #:ret (ret (list -Pos (-val #f)) (list (-FS (list) (list (make-Bot))) (-FS (list (make-Bot)) (list))))] - [tc-e (map #{values @ Symbol} '(a b c)) (make-Listof Sym)] + [tc-e (map #{values @ Symbol} '(a b c)) (-pair Sym (make-Listof Sym))] [tc-e (letrec: ([fact : (Number -> Number) (lambda: ([n : Number]) (if (zero? n) 1 (* n (fact (- n 1)))))]) (fact 20)) N] @@ -255,7 +255,7 @@ [tc-err (5 4)] [tc-err (apply 5 '(2))] [tc-err (map (lambda: ([x : Any] [y : Any]) 1) '(1))] - [tc-e (map add1 '(1)) (-lst -Pos)] + [tc-e (map add1 '(1)) (-pair -Pos (-lst -Pos))] [tc-e/t (let ([x 5]) (if (eq? x 1) @@ -397,9 +397,23 @@ [tc-e (let: ([x : Any 1]) (and (number? x) (boolean? x))) #:ret (ret B (-FS (list (make-Bot)) null))] [tc-e (let: ([x : Any 1]) (and (number? x) x)) - #:proc (get-let-name x 0 (ret (t:Un N (-val #f)) (-FS (list (make-TypeFilter N null #'x) (make-NotTypeFilter (-val #f) null #'x)) null)))] + #:proc (get-let-name x 0 (ret (t:Un N (-val #f)) (-FS + (list (make-TypeFilter N null #'x) (make-NotTypeFilter (-val #f) null #'x)) + (list (make-ImpFilter + (list (make-NotTypeFilter (-val #f) null #'x)) + (list (make-NotTypeFilter N null #'x))) + (make-ImpFilter + (list (make-TypeFilter N null #'x)) + (list (make-TypeFilter (-val #f) null #'x)))))))] [tc-e (let: ([x : Any 1]) (and x (boolean? x))) - #:proc (get-let-name x 0 (ret -Boolean (-FS (list (make-NotTypeFilter (-val #f) null #'x) (make-TypeFilter -Boolean null #'x)) null)))] + #:proc (get-let-name x 0 (ret -Boolean (-FS (list (make-NotTypeFilter (-val #f) null #'x) (make-TypeFilter -Boolean null #'x)) + (list + (make-ImpFilter + (list (make-TypeFilter B null #'x)) + (list (make-TypeFilter (-val #f) null #'x))) + (make-ImpFilter + (list (make-NotTypeFilter (-val #f) null #'x)) + (list (make-NotTypeFilter B null #'x)))))))] [tc-e/t (let: ([x : Any 3]) (if (and (list? x) (not (null? x))) @@ -648,7 +662,9 @@ . t:-> . -Pos : (-LFS null (list (make-LBot))))] [tc-e/t (plambda: (z x y ...) () (inst map z x y ... y)) - (-polydots (z x y) (t:-> ((list ((list x) (y y) . ->... . z) (-lst x)) ((-lst y) y) . ->... . (-lst z))))] + (-polydots (z x y) (t:-> (cl->* + ((t:-> x z) (-pair x (-lst x)) . t:-> . (-pair z (-lst z))) + ((list ((list x) (y y) . ->... . z) (-lst x)) ((-lst y) y) . ->... . (-lst z)))))] ;; error tests [tc-err (#%variable-reference number?)] From 43c534dbdfe70b08692d1bfb92fa45448583dfe3 Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Fri, 11 Dec 2009 17:09:51 +0000 Subject: [PATCH 15/17] fix sorting svn: r17270 original commit: dde2c1fb18fa716928af955d889f205caacbc378 --- collects/typed-scheme/types/subtype.ss | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/collects/typed-scheme/types/subtype.ss b/collects/typed-scheme/types/subtype.ss index be894406..3f6e8303 100644 --- a/collects/typed-scheme/types/subtype.ss +++ b/collects/typed-scheme/types/subtype.ss @@ -6,7 +6,9 @@ (env type-name-env) (only-in (infer infer-dummy) unify) scheme/match unstable/match - mzlib/trace + mzlib/trace (rename-in scheme/contract + [-> c->] + [->* c->*]) (for-syntax scheme/base syntax/parse)) ;; exn representing failure of subtyping @@ -179,7 +181,8 @@ ;(trace subtypes*/varargs) -(define (combine-arrs arrs) +(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 '()) ...) (cond @@ -188,7 +191,7 @@ #f) ((not (foldl type-equal? rng1 rng)) #f) - [else (make-arr (apply map (lambda args (make-Union args)) (cons dom1 dom)) rng1 #f #f '())])] + [else (make-arr (apply map (lambda args (make-Union (sort args type Date: Fri, 11 Dec 2009 23:00:37 +0000 Subject: [PATCH 16/17] Fix abstraction of implications. Fix contract for lookup-typed/lexical. Default cases for printing. Abstract out indexing functions for Nat/Integer split. svn: r17272 original commit: d0c8a19ce84ce1ef674c1c43e69b56ee7e0a63a2 --- collects/typed-scheme/env/lexical-env.ss | 4 +- collects/typed-scheme/env/type-env.ss | 3 +- collects/typed-scheme/main.ss | 5 +- .../private/base-env-indexing-abs.ss | 113 ++++++++++++++++++ .../typed-scheme/private/base-env-indexing.ss | 11 ++ collects/typed-scheme/private/base-env.ss | 91 +------------- collects/typed-scheme/private/base-types.ss | 1 - collects/typed-scheme/private/env-lang.ss | 6 +- collects/typed-scheme/rep/filter-rep.ss | 6 +- .../typecheck/tc-metafunctions.ss | 12 +- collects/typed-scheme/types/printer.ss | 15 ++- collects/typed/scheme/base.ss | 7 +- 12 files changed, 165 insertions(+), 109 deletions(-) create mode 100644 collects/typed-scheme/private/base-env-indexing-abs.ss create mode 100644 collects/typed-scheme/private/base-env-indexing.ss diff --git a/collects/typed-scheme/env/lexical-env.ss b/collects/typed-scheme/env/lexical-env.ss index 36c3eecd..f3386bd4 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 ->* ->) + (only-in scheme/contract ->* -> or/c any/c) (utils tc-utils) (only-in (rep type-rep) Type/c) (typecheck tc-metafunctions) @@ -12,7 +12,7 @@ (provide lexical-env with-lexical-env with-lexical-env/extend with-update-type/lexical) (p/c - [lookup-type/lexical ((identifier?) (env?) . ->* . Type/c)] + [lookup-type/lexical ((identifier?) (env? #:fail (or/c #f (-> any/c #f))) . ->* . (or/c Type/c #f))] [update-type/lexical (((identifier? Type/c . -> . Type/c) identifier?) (env?) . ->* . env?)]) ;; the current lexical environment diff --git a/collects/typed-scheme/env/type-env.ss b/collects/typed-scheme/env/type-env.ss index d454e062..37418e41 100644 --- a/collects/typed-scheme/env/type-env.ss +++ b/collects/typed-scheme/env/type-env.ss @@ -22,7 +22,8 @@ ;; add a single type to the mapping ;; identifier type -> void (define (register-type id type) - ;(printf "register-type ~a~n" (syntax-e id)) + #;(when (eq? (syntax-e id) 'vector-ref) + (printf "register-type ~a~n" id)) (module-identifier-mapping-put! the-mapping id type)) ;; add a single type to the mapping diff --git a/collects/typed-scheme/main.ss b/collects/typed-scheme/main.ss index d6fee54a..52a8263a 100644 --- a/collects/typed-scheme/main.ss +++ b/collects/typed-scheme/main.ss @@ -10,7 +10,10 @@ #%top-interaction lambda #%app)) -(require "private/base-env.ss" "private/base-special-env.ss" +(require "private/base-env.ss" + "private/base-special-env.ss" + "private/base-env-numeric.ss" + "private/base-env-indexing-old.ss" (for-syntax "private/base-types-extra.ss")) (provide (rename-out [with-handlers: with-handlers] [real? number?]) (for-syntax (all-from-out "private/base-types-extra.ss"))) diff --git a/collects/typed-scheme/private/base-env-indexing-abs.ss b/collects/typed-scheme/private/base-env-indexing-abs.ss new file mode 100644 index 00000000..63581174 --- /dev/null +++ b/collects/typed-scheme/private/base-env-indexing-abs.ss @@ -0,0 +1,113 @@ +#lang scheme + +(require + "../utils/utils.ss" + scheme/tcp + scheme/unsafe/ops + (only-in rnrs/lists-6 fold-left) + '#%paramz + "extra-procs.ss" + (utils tc-utils ) + (types union convenience) + (only-in '#%kernel [apply kernel:apply]) + scheme/promise scheme/system + (only-in string-constants/private/only-once maybe-print-message) + (only-in scheme/match/runtime match:error matchable? match-equality-test) + (for-template scheme) + (rename-in (types abbrev) [-Number N] [-Boolean B] [-Symbol Sym] [-Nat -Nat*])) + +(provide indexing) + +(define-syntax-rule (indexing -Nat) + (make-env + + [build-list (-poly (a) (-Nat (-Nat* . -> . a) . -> . (-lst a)))] + + [string-ref (-> -String -Nat -Char)] + [substring (->opt -String -Nat [-Nat] -String)] + [make-string (cl-> [(-Nat) -String] [(-Nat -Char) -String])] + [string-set! (-String -Nat -Char . -> . -Void)] + + [list-ref (-poly (a) ((-lst a) -Nat . -> . a))] + [list-tail (-poly (a) ((-lst a) -Nat . -> . (-lst a)))] + + [regexp-match + (let ([?outp (-opt -Output-Port)] + [N -Nat] + [?N (-opt -Nat)] + [optlist (lambda (t) (-opt (-lst (-opt t))))] + [-StrRx (Un -String -Regexp -PRegexp)] + [-BtsRx (Un -Bytes -Byte-Regexp -Byte-PRegexp)] + [-InpBts (Un -Input-Port -Bytes)]) + (cl->* + (-StrRx -String [N ?N ?outp] . ->opt . (optlist -String)) + (-BtsRx -String [N ?N ?outp] . ->opt . (optlist -Bytes)) + (-Pattern -InpBts [N ?N ?outp] . ->opt . (optlist -Bytes))))] + [regexp-match* + (let ([N -Nat] + [?N (-opt -Nat)] + [-StrRx (Un -String -Regexp -PRegexp)] + [-BtsRx (Un -Bytes -Byte-Regexp -Byte-PRegexp)] + [-InpBts (Un -Input-Port -Bytes)]) + (cl->* + (-StrRx -String [N ?N] . ->opt . (-lst -String)) + (-BtsRx -String [N ?N] . ->opt . (-lst -Bytes)) + (-Pattern -InpBts [N ?N] . ->opt . (-lst -Bytes))))] + [regexp-try-match + (let ([?outp (-opt -Output-Port)] + [?N (-opt -Nat)] + [optlist (lambda (t) (-opt (-lst (-opt t))))]) + (->opt -Pattern -Input-Port [-Nat ?N ?outp] (optlist -Bytes)))] + + [regexp-match-positions + (let ([?outp (-opt -Output-Port)] + [N -Nat] + [?N (-opt -Nat)] + [optlist (lambda (t) (-opt (-lst (-opt t))))] + [-StrRx (Un -String -Regexp -PRegexp)] + [-BtsRx (Un -Bytes -Byte-Regexp -Byte-PRegexp)] + [-InpBts (Un -Input-Port -Bytes)]) + (->opt -Pattern (Un -String -InpBts) [N ?N ?outp] (optlist (-pair -Nat -Nat))))] + [regexp-match-positions* + (let ([?outp (-opt -Output-Port)] + [?N (-opt -Nat)] + [optlist (lambda (t) (-opt (-lst (-opt t))))] + [-StrRx (Un -String -Regexp -PRegexp)] + [-BtsRx (Un -Bytes -Byte-Regexp -Byte-PRegexp)] + [-InpBts (Un -Input-Port -Bytes)]) + (->opt -Pattern (Un -String -InpBts) [-Nat ?N ?outp] (-lst (-pair -Nat -Nat))))] + + + [take (-poly (a) ((-lst a) -Nat . -> . (-lst a)))] + [drop (-poly (a) ((-lst a) -Nat . -> . (-lst a)))] + [take-right (-poly (a) ((-lst a) -Nat . -> . (-lst a)))] + [drop-right (-poly (a) ((-lst a) -Nat . -> . (-lst a)))] + [split-at + (-poly (a) ((list (-lst a)) -Nat . ->* . (-values (list (-lst a) (-lst a)))))] + [split-at-right + (-poly (a) ((list (-lst a)) -Nat . ->* . (-values (list (-lst a) (-lst a)))))] + + [vector-ref (-poly (a) ((-vec a) -Nat . -> . a))] + [build-vector (-poly (a) (-Nat (-Nat . -> . a) . -> . (-vec a)))] + [vector-set! (-poly (a) (-> (-vec a) -Nat a -Void))] + [vector-copy! (-poly (a) ((-vec a) -Nat (-vec a) [-Nat -Nat] . ->opt . -Void))] + [make-vector (-poly (a) (cl-> [(-Nat) (-vec -Integer)] + [(-Nat a) (-vec a)]))] + + [peek-char + (cl->* [->opt [-Input-Port -Nat] (Un -Char (-val eof))])] + [peek-byte + (cl->* [->opt [-Input-Port -Nat] (Un -Byte (-val eof))])] + + ;; string.ss + [real->decimal-string (N [-Nat] . ->opt . -String)] + + [random (cl-> [(-Nat) -Nat*] [() -Real])] + + [raise-type-error + (cl-> + [(Sym -String Univ) (Un)] + [(Sym -String -Nat (-lst Univ)) (Un)])] + + )) + \ No newline at end of file diff --git a/collects/typed-scheme/private/base-env-indexing.ss b/collects/typed-scheme/private/base-env-indexing.ss new file mode 100644 index 00000000..57e74fc6 --- /dev/null +++ b/collects/typed-scheme/private/base-env-indexing.ss @@ -0,0 +1,11 @@ +#lang scheme + +(require + (rename-in "../utils/utils.ss" [infer r:infer]) + (for-syntax (types abbrev) (env init-envs) (r:infer infer-dummy infer) + "base-env-indexing-abs.ss")) + +(define-for-syntax e (parameterize ([infer-param infer]) (indexing -Nat))) +(begin-for-syntax (initialize-type-env e)) + + diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss index 98d2c9da..132c3cec 100644 --- a/collects/typed-scheme/private/base-env.ss +++ b/collects/typed-scheme/private/base-env.ss @@ -11,10 +11,7 @@ scheme/promise scheme/system (only-in string-constants/private/only-once maybe-print-message) (only-in scheme/match/runtime match:error matchable? match-equality-test) - (for-syntax (only-in (types abbrev) [-Number N] [-Boolean B] [-Symbol Sym])) - ;; require the split-out files - "base-env-numeric.ss" - ) + (for-syntax (only-in (types abbrev) [-Number N] [-Boolean B] [-Symbol Sym]))) [raise (Univ . -> . (Un))] @@ -91,8 +88,12 @@ [pair? (make-pred-ty (-pair Univ Univ)) #;(-poly (a b) (make-pred-ty (-pair a b)))] [empty? (make-pred-ty (-val null))] [empty (-val null)] + [string? (make-pred-ty -String)] [string (->* '() -Char -String)] +[string-length (-String . -> . -Nat)] +[unsafe-string-length (-String . -> . -Nat)] + [symbol? (make-pred-ty Sym)] [keyword? (make-pred-ty -Keyword)] [list? (make-pred-ty (-lst Univ))] @@ -159,7 +160,6 @@ [sleep (N . -> . -Void)] -[build-list (-poly (a) (-Nat (-Nat . -> . a) . -> . (-lst a)))] [reverse (-poly (a) (-> (-lst a) (-lst a)))] [append (-poly (a) (->* (list) (-lst a) (-lst a)))] [length (-poly (a) (-> (-lst a) -Nat))] @@ -207,8 +207,6 @@ [string-copy (-> -String -String)] [string->immutable-string (-> -String -String)] -[string-ref (-> -String -Nat -Char)] -[substring (->opt -String -Nat [-Nat] -String)] [string->path (-> -String -Path)] [file-exists? (-> -Pathlike B)] @@ -224,7 +222,6 @@ #:mode (one-of/c 'binary 'text) #f a))] -[random (cl-> [(-Nat) -Nat] [() -Real])] [assq (-poly (a b) (a (-lst (-pair a b)) . -> . (-opt (-pair a b))))] [assv (-poly (a b) (a (-lst (-pair a b)) . -> . (-opt (-pair a b))))] @@ -232,9 +229,6 @@ [assf (-poly (a b) ((a . -> . Univ) (-lst (-pair a b)) . -> . (-opt (-pair a b))))] -[list-ref (-poly (a) ((-lst a) -Nat . -> . a))] -[list-tail (-poly (a) ((-lst a) -Nat . -> . (-lst a)))] - [apply (-poly (a b) (((list) a . ->* . b) (-lst a) . -> . b))] [kernel:apply (-poly (a b) (((list) a . ->* . b) (-lst a) . -> . b))] [time-apply (-polydots (b a) @@ -275,55 +269,11 @@ [regexp-quote (cl->* (-String [-Boolean] . ->opt . -String) (-Bytes [-Boolean] . ->opt . -Bytes))] -[regexp-match - (let ([?outp (-opt -Output-Port)] - [N -Nat] - [?N (-opt -Nat)] - [optlist (lambda (t) (-opt (-lst (-opt t))))] - [-StrRx (Un -String -Regexp -PRegexp)] - [-BtsRx (Un -Bytes -Byte-Regexp -Byte-PRegexp)] - [-InpBts (Un -Input-Port -Bytes)]) - (cl->* - (-StrRx -String [N ?N ?outp] . ->opt . (optlist -String)) - (-BtsRx -String [N ?N ?outp] . ->opt . (optlist -Bytes)) - (-Pattern -InpBts [N ?N ?outp] . ->opt . (optlist -Bytes))))] -[regexp-match* - (let ([N -Nat] - [?N (-opt -Nat)] - [-StrRx (Un -String -Regexp -PRegexp)] - [-BtsRx (Un -Bytes -Byte-Regexp -Byte-PRegexp)] - [-InpBts (Un -Input-Port -Bytes)]) - (cl->* - (-StrRx -String [N ?N] . ->opt . (-lst -String)) - (-BtsRx -String [N ?N] . ->opt . (-lst -Bytes)) - (-Pattern -InpBts [N ?N] . ->opt . (-lst -Bytes))))] -[regexp-try-match - (let ([?outp (-opt -Output-Port)] - [?N (-opt -Nat)] - [optlist (lambda (t) (-opt (-lst (-opt t))))]) - (->opt -Pattern -Input-Port [-Nat ?N ?outp] (optlist -Bytes)))] [regexp-match-exact? (-Pattern (Un -String -Bytes -Input-Port) . -> . B)] -[regexp-match-positions - (let ([?outp (-opt -Output-Port)] - [N -Nat] - [?N (-opt -Nat)] - [optlist (lambda (t) (-opt (-lst (-opt t))))] - [-StrRx (Un -String -Regexp -PRegexp)] - [-BtsRx (Un -Bytes -Byte-Regexp -Byte-PRegexp)] - [-InpBts (Un -Input-Port -Bytes)]) - (->opt -Pattern (Un -String -InpBts) [N ?N ?outp] (optlist (-pair -Nat -Nat))))] -[regexp-match-positions* - (let ([?outp (-opt -Output-Port)] - [?N (-opt -Nat)] - [optlist (lambda (t) (-opt (-lst (-opt t))))] - [-StrRx (Un -String -Regexp -PRegexp)] - [-BtsRx (Un -Bytes -Byte-Regexp -Byte-PRegexp)] - [-InpBts (Un -Input-Port -Bytes)]) - (->opt -Pattern (Un -String -InpBts) [-Nat ?N ?outp] (-lst (-pair -Nat -Nat))))] #; [regexp-match-peek-positions*] #; @@ -344,11 +294,6 @@ ;; errors -[raise-type-error - (cl-> - [(Sym -String Univ) (Un)] - [(Sym -String -Nat (-lst Univ)) (Un)])] - ;; this is a hack [match:error ((list) Univ . ->* . (Un))] @@ -359,12 +304,7 @@ [bitwise-not (null -Integer . ->* . -Integer)] [bitwise-xor (null -Integer . ->* . -Integer)] -[make-string (cl-> [(-Nat) -String] [(-Nat -Char) -String])] [abs (-Real . -> . -Real)] -[substring (->opt -String [-Nat] -String)] -[string-length (-String . -> . -Nat)] -[unsafe-string-length (-String . -> . -Nat)] -[string-set! (-String -Nat -Char . -> . -Void)] [file-exists? (-Pathlike . -> . B)] [string->symbol (-String . -> . Sym)] @@ -374,21 +314,14 @@ ;; vectors [vector? (make-pred-ty (-vec Univ))] -[vector-ref (-poly (a) ((-vec a) -Nat . -> . a))] -[build-vector (-poly (a) (-Nat (-Nat . -> . a) . -> . (-vec a)))] - -[vector-set! (-poly (a) (-> (-vec a) -Nat a -Void))] [vector->list (-poly (a) (-> (-vec a) (-lst a)))] [list->vector (-poly (a) (-> (-lst a) (-vec a)))] [vector-length (-poly (a) ((-vec a) . -> . -Nat))] -[make-vector (-poly (a) (cl-> [(-Nat) (-vec -Integer)] - [(-Nat a) (-vec a)]))] [vector (-poly (a) (->* (list) a (-vec a)))] [vector-immutable (-poly (a) (->* (list) a (-vec a)))] [vector->vector-immutable (-poly (a) (-> (-vec a) (-vec a)))] [vector-fill! (-poly (a) (-> (-vec a) a -Void))] -[vector-copy! (-poly (a) ((-vec a) -Nat (-vec a) [-Nat -Nat] . ->opt . -Void))] ;; [vector->values no good type here] @@ -457,10 +390,6 @@ [regexp-replace* (cl->* (-Pattern -String -String . -> . -String) (-Pattern (Un -Bytes -String) (Un -Bytes -String) . -> . -Bytes))] -[peek-char - (cl->* [->opt [-Input-Port -Nat] (Un -Char (-val eof))])] -[peek-byte - (cl->* [->opt [-Input-Port -Nat] (Un -Byte (-val eof))])] [read-char (cl->* [->opt [-Input-Port] (Un -Char (-val eof))])] [read-byte @@ -575,14 +504,6 @@ ((list a) (b b) . ->... . (-opt c)) (-lst a)) ((-lst b) b) . ->... . (-lst c)))] -[take (-poly (a) ((-lst a) -Nat . -> . (-lst a)))] -[drop (-poly (a) ((-lst a) -Nat . -> . (-lst a)))] -[take-right (-poly (a) ((-lst a) -Nat . -> . (-lst a)))] -[drop-right (-poly (a) ((-lst a) -Nat . -> . (-lst a)))] -[split-at - (-poly (a) ((list (-lst a)) -Nat . ->* . (-values (list (-lst a) (-lst a)))))] -[split-at-right - (-poly (a) ((list (-lst a)) -Nat . ->* . (-values (list (-lst a) (-lst a)))))] [last (-poly (a) ((-lst a) . -> . a))] [add-between (-poly (a b) ((-lst a) b . -> . (-lst (Un a b))))] @@ -623,8 +544,6 @@ [generate-temporaries ((Un (-Syntax Univ) (-lst Univ)) . -> . (-lst (-Syntax Sym)))] [check-duplicate-identifier ((-lst (-Syntax Sym)) . -> . (-opt (-Syntax Sym)))] -;; string.ss -[real->decimal-string (N [-Nat] . ->opt . -String)] [current-continuation-marks (-> -Cont-Mark-Set)] diff --git a/collects/typed-scheme/private/base-types.ss b/collects/typed-scheme/private/base-types.ss index 99719989..8136c20a 100644 --- a/collects/typed-scheme/private/base-types.ss +++ b/collects/typed-scheme/private/base-types.ss @@ -3,7 +3,6 @@ [Number -Real] [Complex -Number] [Integer -Integer] -[Real -Real] [Exact-Rational -ExactRational] [Flonum -Flonum] [Exact-Positive-Integer -ExactPositiveInteger] diff --git a/collects/typed-scheme/private/env-lang.ss b/collects/typed-scheme/private/env-lang.ss index 8b3e6feb..c1cd3f3b 100644 --- a/collects/typed-scheme/private/env-lang.ss +++ b/collects/typed-scheme/private/env-lang.ss @@ -11,7 +11,7 @@ (types convenience union) (only-in (types convenience) [make-arr* make-arr]))) -(define-syntax (#%module-begin stx) +(define-syntax (-#%module-begin stx) (define-syntax-class clause #:description "[id type]" (pattern [id:identifier ty])) @@ -29,9 +29,9 @@ [(mb . rest) #'(mb (begin) . rest)])) -(provide #%module-begin +(provide (rename-out [-#%module-begin #%module-begin]) require - (all-from-out scheme/base) + (except-out (all-from-out scheme/base) #%module-begin) types rep private utils (for-syntax (types-out convenience union) diff --git a/collects/typed-scheme/rep/filter-rep.ss b/collects/typed-scheme/rep/filter-rep.ss index 56c0f41a..e3a95d30 100644 --- a/collects/typed-scheme/rep/filter-rep.ss +++ b/collects/typed-scheme/rep/filter-rep.ss @@ -70,9 +70,9 @@ [#:fold-rhs (*LNotTypeFilter (type-rec-id t) (map pathelem-rec-id p) idx)]) ;; implication -(df LImpFilter ([a (non-empty-listof LatentFilter/c)] [c (non-empty-listof LatentFilter/c)]) - [#:frees (combine-frees (map free-vars* (append a c))) - (combine-frees (map free-idxs* (append a c)))]) +(dlf LImpFilter ([a (non-empty-listof LatentFilter/c)] [c (non-empty-listof LatentFilter/c)]) + [#:frees (combine-frees (map free-vars* (append a c))) + (combine-frees (map free-idxs* (append a c)))]) (dlf LFilterSet (thn els) diff --git a/collects/typed-scheme/typecheck/tc-metafunctions.ss b/collects/typed-scheme/typecheck/tc-metafunctions.ss index 096f7a14..39d44def 100644 --- a/collects/typed-scheme/typecheck/tc-metafunctions.ss +++ b/collects/typed-scheme/typecheck/tc-metafunctions.ss @@ -66,7 +66,7 @@ (apply append (for/list ([f f-]) (abo ids keys f))))])) (d/c (abo xs idxs f) - (-> (listof identifier?) (listof index/c) Filter/c (or/c '() (list/c LatentFilter/c))) + ((listof identifier?) (listof index/c) Filter/c . -> . (or/c null? (list/c LatentFilter/c))) (define (lookup y) (for/first ([x xs] [i idxs] #:when (free-identifier=? x y)) i)) (define-match-expander lookup: @@ -76,10 +76,12 @@ [(Bot:) (list (make-LBot))] [(TypeFilter: t p (lookup: idx)) (list (make-LTypeFilter t p idx))] [(NotTypeFilter: t p (lookup: idx)) (list (make-LNotTypeFilter t p idx))] - [(ImpFilter: a c) - (match* [(abo a) (abo c)] - [((list a*) (list c*)) (list (make-LImpFilter a* c*))] - [(_ _) null])] + [(ImpFilter: as cs) + (let ([a* (apply append (for/list ([f as]) (abo xs idxs f)))] + [c* (apply append (for/list ([f cs]) (abo xs idxs f)))]) + (if (< (length a*) (length as)) ;; if we removed some things, we can't be sure + null + (list (make-LImpFilter a* c*))))] [_ null])) (define (merge-filter-sets fs) diff --git a/collects/typed-scheme/types/printer.ss b/collects/typed-scheme/types/printer.ss index beb0cad5..b39ccfdb 100644 --- a/collects/typed-scheme/types/printer.ss +++ b/collects/typed-scheme/types/printer.ss @@ -46,7 +46,8 @@ [(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)])) + [(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)) @@ -59,14 +60,16 @@ [(NotTypeFilter: type path id) (fp "(! ~a @ ~a ~a)" type path (syntax-e id))] [(TypeFilter: type path id) (fp "(~a @ ~a ~a)" type path (syntax-e id))] [(Bot:) (fp "Bot")] - [(ImpFilter: a c) (fp "(ImpFilter ~a ~a)" a c)])) + [(ImpFilter: a c) (fp "(ImpFilter ~a ~a)" a c)] + [else (fp "(Unknown Filter: ~a)" (struct->vector c))])) (define (print-pathelem c port write?) (define (fp . args) (apply fprintf port args)) (match c [(CarPE:) (fp "car")] [(CdrPE:) (fp "cdr")] - [(StructPE: t i) (fp "(~a ~a)" t i)])) + [(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)) @@ -79,7 +82,8 @@ (match c [(NoObject:) (fp "-")] [(Empty:) (fp "")] - [(Path: pes i) (fp "~a" (append pes (list (syntax-e i))))])) + [(Path: pes i) (fp "~a" (append pes (list (syntax-e i))))] + [else (fp "(Unknown Object: ~a)" (struct->vector c))])) ;; print out a type ;; print-type : Type Port Boolean -> Void @@ -121,7 +125,8 @@ (fp/filter "-> ~a : ~a ~a" t lf lo)] [_ (fp "-> ~a" rng)]) - (fp ")")])) + (fp ")")] + [else (fp "(Unknown Function Type: ~a)" (struct->vector a))])) (define (tuple? t) (match t [(Pair: a (? tuple?)) #t] diff --git a/collects/typed/scheme/base.ss b/collects/typed/scheme/base.ss index 860cb02e..000da9a2 100644 --- a/collects/typed/scheme/base.ss +++ b/collects/typed/scheme/base.ss @@ -10,7 +10,10 @@ #%top-interaction lambda #%app)) -(require typed-scheme/private/base-env typed-scheme/private/base-special-env - (for-syntax typed-scheme/private/base-types-extra)) +(require typed-scheme/private/base-env + typed-scheme/private/base-special-env + typed-scheme/private/base-env-numeric + typed-scheme/private/base-env-indexing + (for-syntax typed-scheme/private/base-types-extra)) (provide (rename-out [with-handlers: with-handlers]) (for-syntax (all-from-out typed-scheme/private/base-types-extra))) From e820082489300b25043ff338da283f1fb0ca9af6 Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Fri, 11 Dec 2009 23:08:48 +0000 Subject: [PATCH 17/17] Fix type of sqrt svn: r17273 original commit: a1f647121d84c02b9224b11500db5a2732db6087 --- collects/typed-scheme/private/base-env-numeric.ss | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/collects/typed-scheme/private/base-env-numeric.ss b/collects/typed-scheme/private/base-env-numeric.ss index 957a21db..f0c05718 100644 --- a/collects/typed-scheme/private/base-env-numeric.ss +++ b/collects/typed-scheme/private/base-env-numeric.ss @@ -107,7 +107,7 @@ [rationalize (N N . -> . N)] [expt (cl->* (-Integer -Integer . -> . -Integer) (N N . -> . N))] [sqrt (cl->* - (-Real . -> . -Real) + (-Nat . -> . -Real) (N . -> . N))] [log (cl->* (-Pos . -> . -Real)