sync ts to trunk

svn: r14257

collects/typed-scheme/env/type-environments.ss

@@ -10,6 +10,9 @@
          dotted-env
          initial-tvar-env
          env-map
+         env-filter
+         env-vals
+         env-keys+vals
          with-dotted-env/extend)
 
 (require (prefix-in r: "../utils/utils.ss"))
@@ -19,6 +22,17 @@
 ;; eq? has the type of equal?, and l is an alist (with conses!)
 (define-struct env (eq? l))
 
+(define (env-vals e)
+  (map cdr (env-l e)))
+
+(define (env-keys+vals e)
+  (env-l e))
+
+(define (env-filter f e)
+  (match e
+    [(struct env (eq? l))
+    (make-env eq? (filter f l))]))
+
 ;; the initial type variable environment - empty
 ;; this is used in the parsing of types
 (define initial-tvar-env (make-env eq? '()))

collects/typed-scheme/private/base-env.ss

@@ -102,10 +102,14 @@
 [fold-right (-polydots (c a b) ((list ((list c a) (b b) . ->... . c) c (-lst a))
                                 ((-lst b) b) . ->... . c))]
 [foldl
- (-poly (a b c)
+ (-poly (a b c d)
         (cl-> [((a b . -> . b) b (-lst a)) b]
-              [((a b c . -> . c) c (-lst a) (-lst b)) c]))]
+              [((a b c . -> . c) c (-lst a) (-lst b)) c]
-[foldr  (-poly (a b c) ((a b . -> . b) b (-lst a) . -> . b))]
+              [((a b c d . -> . d) d (-lst a) (-lst b) (-lst d)) d]))]
+[foldr  (-poly (a b c d)
+               (cl-> [((a b . -> . b) b (-lst a)) b]
+                     [((a b c . -> . c) c (-lst a) (-lst b)) c]
+                     [((a b c d . -> . d) d (-lst a) (-lst b) (-lst d)) d]))]
 [filter (-poly (a b) (cl->*
                       ((make-pred-ty (list a) B b)
                        (-lst a)
@@ -537,6 +541,10 @@
 
 [maybe-print-message (-String . -> . -Void)]
 
+[list->string ((-lst -Char) . -> . -String)]
+[string->list (-String . -> . (-lst -Char))]
+[sort (-poly (a) ((-lst a) (a a . -> . B) . -> . (-lst a)))]
+
 ;; scheme/list
 [last-pair (-poly (a) ((-mu x (Un a (-val '()) (-pair a x)))
                        . -> . 
@@ -567,3 +575,28 @@
 [real->decimal-string (N [-Nat] . ->opt .  -String)]
 
 [current-continuation-marks (-> -Cont-Mark-Set)]
+
+;; scheme/path
+
+[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))]
+[filename-extension (-Pathlike . -> . (-opt -Bytes))]
+[file-name-from-path (-Pathlike . -> . (-opt -Path))]
+[path-only (-Pathlike . -> . -Path)]
+[some-system-path->string (-Path . -> . -String)]
+[string->some-system-path 
+ (-String (Un (-val 'unix) (-val 'windows)) . -> . -Path)]
+
+;; 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)]

collects/typed-scheme/private/parse-type.ss

@@ -346,6 +346,26 @@
                                                                           (current-tvars))])
                                   (parse-type #'rest))
                                 (syntax-e #'bound)))))))]
+      [(dom ... rest ::: -> rng)
+       (and (eq? (syntax-e #'->) '->) 
+            (eq? (syntax-e #':::) '...))
+       (begin
+         (add-type-name-reference #'->)
+         (let ([bounds (filter (compose Dotted? cdr) (env-keys+vals (current-tvars)))])
+           (when (null? bounds)
+             (tc-error/stx stx "No type variable bound with ... in scope for ... type"))
+           (unless (null? (cdr bounds))
+             (tc-error/stx stx "Cannot infer bound for ... type"))
+           (match-let ([(cons var (struct Dotted (t))) (car bounds)])
+             (make-Function
+              (list
+               (make-arr-dots (map parse-type (syntax->list #'(dom ...)))
+                              (parse-type #'rng)
+                              (parameterize ([current-tvars (extend-env (list var)
+                                                                        (list (make-DottedBoth t))
+                                                                        (current-tvars))])
+                                (parse-type #'rest))
+                              var))))))]
       ;; has to be below the previous one
       [(dom ... -> rng) 
        (eq? (syntax-e #'->) '->)
@@ -365,6 +385,23 @@
                                                                         (current-tvars))])
                                 (parse-type #'dty))
                               (syntax-e #'bound))))]
+      [(values tys ... dty dd)
+       (and (eq? (syntax-e #'values) 'values) 
+            (eq? (syntax-e #'dd) '...))
+       (begin
+         (add-type-name-reference #'values)
+         (let ([bounds (filter (compose Dotted? cdr) (env-keys+vals (current-tvars)))])
+           (when (null? bounds)
+             (tc-error/stx stx "No type variable bound with ... in scope for ... type"))
+           (unless (null? (cdr bounds))
+             (tc-error/stx stx "Cannot infer bound for ... type"))
+           (match-let ([(cons var (struct Dotted (t))) (car bounds)])
+             (make-ValuesDots (map parse-type (syntax->list #'(tys ...)))
+                              (parameterize ([current-tvars (extend-env (list var) 
+                                                                        (list (make-DottedBoth t))
+                                                                        (current-tvars))])
+                                            (parse-type #'dty))
+                              var))))]
       [(values tys ...) 
        (eq? (syntax-e #'values) 'values)
        (-values (map parse-type (syntax->list #'(tys ...))))]

collects/typed-scheme/private/type-contract.ss

@@ -17,7 +17,7 @@
  mzlib/trace
  scheme/list
  (only-in scheme/contract -> ->* case-> cons/c flat-rec-contract provide/contract any/c)
- (for-template scheme/base scheme/contract (only-in scheme/class object% is-a?/c subclass?/c)))
+ (for-template scheme/base scheme/contract (utils poly-c) (only-in scheme/class object% is-a?/c subclass?/c)))
 
 (define (define/fixup-contract? stx)
   (or (syntax-property stx 'typechecker:contract-def)
@@ -51,7 +51,9 @@
 (define (type->contract ty fail)
   (define vars (make-parameter '()))
   (let/cc exit
-    (let t->c ([ty ty])
+    (let loop ([ty ty] [pos? #t])
+      (define (t->c t) (loop t pos?))
+      (define (t->c/neg t) (loop t (not pos?)))
       (match ty
         [(or (App: _ _ _) (Name: _)) (t->c (resolve-once ty))]
         [(Univ:) #'any/c]
@@ -71,13 +73,13 @@
              (define-values (dom* rngs* rst)
                (match a
                  [(arr: dom (Values: rngs) #f #f '())
-                  (values (map t->c dom) (map t->c rngs) #f)]
+                  (values (map t->c/neg dom) (map t->c rngs) #f)]
                  [(arr: dom rng #f #f '())
-                  (values (map t->c dom) (list (t->c rng)) #f)]
+                  (values (map t->c/neg dom) (list (t->c rng)) #f)]
                  [(arr: dom (Values: rngs) rst #f '() )
-                  (values (map t->c dom) (map t->c rngs) (t->c rst))]
+                  (values (map t->c/neg dom) (map t->c rngs) (t->c/neg rst))]
                  [(arr: dom rng rst #f '())
-                  (values (map t->c dom) (list (t->c rng)) (t->c rst))]))
+                  (values (map t->c/neg dom) (list (t->c rng)) (t->c/neg rst))]))
              (with-syntax 
                  ([(dom* ...) dom*]
                   [rng* (match rngs*
@@ -99,12 +101,22 @@
          #`(cons/c #,(t->c t1) #,(t->c t2))]
         [(Opaque: p? cert)
          #`(flat-contract #,(cert p?))]
-        [(F: v) (cond [(assoc v (vars)) => cadr]
+        [(F: v) (cond [(assoc v (vars)) => (if pos? second third)]
                       [else (int-err "unknown var: ~a" v)])]
+	[(Poly: vs (and b (Function: _)))
+         (match-let ([(Poly-names: vs-nm _) ty])
+           (with-syntax ([(vs+ ...) (generate-temporaries (for/list ([v vs-nm]) (symbol-append v '+)))]
+			 [(vs- ...) (generate-temporaries (for/list ([v vs-nm]) (symbol-append v '-)))])
+             (parameterize ([vars (append (map list
+					       vs
+					       (syntax->list #'(vs+ ...))
+					       (syntax->list #'(vs- ...)))
+					  (vars))])
+               #`(poly/c ([vs- vs+] ...) #,(t->c b)))))]
         [(Mu: n b)
          (match-let ([(Mu-name: n-nm _) ty])
            (with-syntax ([(n*) (generate-temporaries (list n-nm))])
-             (parameterize ([vars (cons (list n #'n*) (vars))])
+             (parameterize ([vars (cons (list n #'n* #'n*) (vars))])
                #`(flat-rec-contract n* #,(t->c b)))))]
         [(Value: #f) #'false/c]    
         [(Instance: _) #'(is-a?/c object%)]
@@ -112,10 +124,7 @@
         [(Value: '()) #'null?]
         [(Struct: _ _ _ _ #f pred? cert) (cert pred?)]
         [(Syntax: (Base: 'Symbol _)) #'identifier?]
-        [(Syntax: t)
+        [(Syntax: t) #`(syntax/c #,(t->c t))]
-         (if (equal? ty t:Any-Syntax)
-             #`syntax?
-             #`(syntax/c #,(t->c t)))]
         [(Value: v) #`(flat-named-contract #,(format "~a" v) (lambda (x) (equal? x '#,v)))]
         [(Param: in out) #`(parameter/c #,(t->c out))]
 	[(Hashtable: k v) #`hash?]

collects/typed-scheme/ts-reference.scrbl

@@ -1,7 +1,10 @@
 #lang scribble/doc
 
-@begin[(require scribble/manual)
+@begin[(require scribble/manual scribble/eval
-       (require (for-label typed-scheme))]
+                scheme/sandbox)
+       (require (for-label typed-scheme
+                           scheme/list srfi/14
+                           version/check))]
 
 @begin[
 (define (item* header . args) (apply item @bold[header]{: } args))
@@ -52,6 +55,8 @@ The following base types are parameteric in their type arguments.
                                the first is the type the parameter accepts, and the second is the type returned.}
 @defform[(Pair s t)]{is the pair containing @scheme[s] as the @scheme[car]
   and @scheme[t] as the @scheme[cdr]}
+@defform[(HashTable k v)]{is the type of a @rtech{hash table} with key type
+   @scheme[k] and value type @scheme[v].}
 
 @subsubsub*section{Type Constructors}
 
@@ -245,3 +250,47 @@ known to Typed Scheme, either via @scheme[define-struct:] or
 Like @scheme[do], but each @scheme[id] having the associated type @scheme[t], and 
 the final body @scheme[expr] having the type @scheme[u].
 }
+
+@section{Libraries Provided With Typed Scheme}
+
+The @schememodname[typed-scheme] language corresponds to the
+@schememodname[scheme/base] language---that is, any identifier provided
+by @schememodname[scheme/base], such as @scheme[mod] is available by default in
+@schememodname[typed-scheme].  
+
+@schememod[typed-scheme
+(modulo 12 2)
+]
+
+Any value provided by @schememodname[scheme] is available by simply
+@scheme[require]ing it; use of @scheme[require/typed] is not
+neccessary.  
+
+@schememod[typed-scheme
+(require scheme/list)
+(display (first (list 1 2 3)))
+]
+
+Some libraries have counterparts in the @schemeidfont{typed}
+collection, which provide the same exports as the untyped versions.
+Such libraries include @schememodname[srfi/14],
+@schememodname[net/url], and many others.  
+
+@schememod[typed-scheme
+(require typed/srfi/14)
+(char-set= (string->char-set "hello")
+           (string->char-set "olleh"))
+]
+
+To participate in making more libraries available, please visit 
+@link["http://www.ccs.neu.edu/home/samth/adapt/"]{here}.
+
+
+Other libraries can be used with Typed Scheme via
+@scheme[require/typed].
+
+@schememod[typed-scheme
+(require/typed version/check
+               [check-version (-> (U Symbol (Listof Any)))])
+(check-version)
+]

collects/typed-scheme/typecheck/provide-handling.ss

@@ -54,15 +54,18 @@
                             (define/contract cnt-id #,cnt id)
                             (define-syntax export-id
                               (if (unbox typed-context?)
-                                  (make-rename-transformer #'id)
+                                  (make-rename-transformer (syntax-property #'id 
-                                  (make-rename-transformer #'cnt-id)))
+                                                                            'not-free-identifier=? #t))
+                                  (make-rename-transformer (syntax-property #'cnt-id
+                                                                            'not-free-identifier=? #t))))
                             (#%provide (rename export-id out-id)))))]
                    [else 
                     (with-syntax ([(export-id) (generate-temporaries #'(id))])
                       #`(begin                             
                           (define-syntax export-id
                             (if (unbox typed-context?)
-                                (make-rename-transformer #'id)
+                                (make-rename-transformer (syntax-property #'id 
+                                                                          'not-free-identifier=? #t))
                                 (lambda (stx) (tc-error/stx stx "The type of ~a cannot be converted to a contract" (syntax-e #'id)))))
                           (provide (rename-out [export-id out-id]))))])))]
         [(mem? internal-id stx-defs) 
@@ -76,7 +79,8 @@
                      (if (unbox typed-context?)
                          (begin
                            (add-alias #'export-id #'id)
-                           (make-rename-transformer #'id))
+                           (make-rename-transformer (syntax-property #'id 
+                                                                     'not-free-identifier=? #t)))
                          (lambda (stx)
                            (tc-error/stx stx "Macro ~a from typed module used in untyped code" (syntax-e #'out-id)))))
                    (provide (rename-out [export-id out-id]))))))]

collects/typed-scheme/typecheck/tc-app-unit.ss

@@ -342,6 +342,19 @@
                                              drest-bound
                                              (subst-all (alist-delete drest-bound substitution eq?)
                                                         (car rngs*)))))]
+               ;; ... function, (List A B C etc) arg
+               [(and (car drests*)
+                     (not tail-bound)
+                     (eq? (cdr (car drests*)) dotted-var)
+                     (= (length (car doms*))
+                        (length arg-tys))
+                     (untuple tail-ty)
+                     (infer/dots fixed-vars dotted-var (append arg-tys (untuple tail-ty)) (car doms*)
+                                 (car (car drests*)) (car rngs*) (fv (car rngs*))))
+                => (lambda (substitution) 
+                     (define drest-bound (cdr (car drests*)))
+                     (do-apply-log substitution 'dots 'dots)
+                     (ret (subst-all substitution (car rngs*))))]
                ;; if nothing matches, around the loop again
                [else (loop (cdr doms*) (cdr rngs*) (cdr rests*) (cdr drests*))])))]
     [(tc-result: (PolyDots: vars (Function: '())))

collects/typed-scheme/types/abbrev.ss

@@ -96,6 +96,7 @@
 (define Err (make-Error))
 
 (define -Nat -Integer)
+(define -Real -Number)
 
 (define Any-Syntax
   (-mu x

collects/typed-scheme/utils/poly-c.ss

@@ -0,0 +1,70 @@
+#lang scheme/base
+
+(require scheme/contract (for-syntax scheme/base))
+
+(provide memory/c apply/c poly/c)
+
+(with-contract
+ poly-internals
+ ([memory/c
+   (->*
+    []
+    [ #:name any/c
+      #:to any/c
+      #:from any/c
+      #:weak boolean?
+      #:equal (or/c 'eq 'eqv 'equal)
+      #:table (-> (and/c hash? (not/c immutable?))) ]
+    (values flat-contract? flat-contract?))]
+  [apply/c (->* [any/c] [#:name any/c] contract?)])
+
+ (define (memory/c
+          #:name [name "memory/c"]
+          #:to [to (format "~a:to" name)]
+          #:from [from (format "~a:from" name)]
+          #:weak [weak? #t]
+          #:equal [equal 'eq]
+          #:table [make-table
+                   (case equal
+                     [(eq) (if weak? make-weak-hasheq make-hasheq)]
+                     [(eqv) (if weak? make-weak-hasheqv make-hasheqv)]
+                     [(equal) (if weak? make-weak-hash make-hash)])])
+   (let* ([table (make-table)])
+     (values
+      (flat-named-contract from
+        (lambda (v) (hash-set! table v #t) #t))
+      (flat-named-contract to
+        (lambda (v) (hash-ref table v #f))))))
+
+ (define (apply/c c
+                  #:name [name (build-compound-type-name 'apply/c c)])
+   (make-proj-contract
+    name
+    (lambda (pos neg src name2)
+      (lambda (p)
+        (let* ([ctc (coerce-contract 'apply/c c)]
+               [thunk (lambda () ((((proj-get ctc) ctc) pos neg src name2) p))])
+          (make-keyword-procedure
+           (lambda (keys vals . args) (keyword-apply (thunk) keys vals args))
+           (case-lambda
+             [() ((thunk))]
+             [(a) ((thunk) a)]
+             [(a b) ((thunk) a b)]
+             [(a b c) ((thunk) a b c)]
+             [(a b c d) ((thunk) a b c d)]
+             [(a b c d e) ((thunk) a b c d e)]
+             [(a b c d e f) ((thunk) a b c d e f)]
+             [(a b c d e f g) ((thunk) a b c d e f g)]
+             [(a b c d e f g h) ((thunk) a b c d e f g h)]
+             [args (apply (thunk) args)])))))
+    procedure?)))
+
+(define-syntax (poly/c stx)
+  (syntax-case stx ()
+    [(_ opts ... ([c- c+] ...) c)
+     (quasisyntax/loc stx
+       (apply/c
+        #:name (quote #,stx)
+        (recursive-contract
+         (let-values ([(c- c+) (memory/c #:from 'c- #:to 'c+ opts ...)] ...)
+           c))))]))

collects/typed-scheme/utils/utils.ss

@@ -20,7 +20,9 @@ at least theoretically.
          in-list-forever
          extend
          debug
-         in-syntax)
+         in-syntax
+	 symbol-append
+	 rep utils typecheck infer env private)
 
 (define-syntax (define-requirer stx)
   (syntax-parse stx