From 7d85ae8997fa79fa7d982459ef72fe5a3a22f439 Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Fri, 20 Nov 2009 05:20:23 +0000 Subject: [PATCH] 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]))