checkpoint

svn: r16915

original commit: 485c8a356708bb1f59c942529dd77bd455a6c82d

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))
 

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)

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")))

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)]

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]

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]

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)         

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]))