Added uses of unstable/struct

original commit: 07f57aac9b3f52552397bd53597de192ff62fbbc

collects/tests/typed-scheme/fail/all-bad-syntax.rkt

@@ -1,5 +1,5 @@
 #;
-(exn-pred 1)
+(exn-pred 2)
 #lang typed-scheme
 
 (require scheme/list)
@@ -22,4 +22,4 @@
                         (list key)
                         (rt)))
               #;empty))
-(+ 'foo)
+(+ 'foo)

collects/tests/typed-scheme/fail/inexact-complex.rkt

@@ -0,0 +1,9 @@
+#;
+(exn-pred 2)
+#lang typed/scheme
+
+(ann 1+2i Inexact-Complex)
+
+(: f (Real -> Inexact-Complex))
+(define (f x)
+  (* x 2.0)) ; x can be exact 0

collects/tests/typed-scheme/fail/multi-arr-parse.rkt

@@ -0,0 +1,6 @@
+#;
+(exn-pred #rx".*once in a form.*")
+#lang typed/scheme
+
+(: foo : (Integer -> Integer -> Integer))
+(define foo 1)

collects/tests/typed-scheme/fail/nonnegative-float.rkt

@@ -0,0 +1,5 @@
+#;
+(exn-pred 1)
+#lang typed/scheme
+
+(ann (- 1.0 0.5) Nonnegative-Float) ; can't prove it's nonnegative

collects/tests/typed-scheme/fail/unsafe-struct-parent.rkt

@@ -0,0 +1,19 @@
+#;
+(exn-pred 7)
+#lang typed/scheme
+(require racket/unsafe/ops)
+
+(define-struct: foo ((x : Integer) (y : String)))
+(define-struct: (bar foo) ((z : Float)))
+
+(define a (make-foo 1 "1"))
+(define b (make-bar 2 "2" 2.0))
+
+(+ (unsafe-struct-ref a 1) 2)
+(+ (unsafe-struct-ref b 1) 2)
+
+(unsafe-struct-set! a 0 "2")
+(unsafe-struct-set! a 1 2)
+(unsafe-struct-set! b 0 3.0)
+(unsafe-struct-set! b 1 3)
+(unsafe-struct-set! b 2 "3")

collects/tests/typed-scheme/fail/unsafe-struct.rkt

@@ -0,0 +1,13 @@
+#;
+(exn-pred 3)
+#lang typed/scheme
+(require racket/unsafe/ops)
+
+(define-struct: x ((a : Integer) (b : String)) #:mutable)
+
+(define x1 (make-x 1 "1"))
+
+(+ (unsafe-struct-ref x1 1) 1)
+
+(unsafe-struct-set! x1 0 "2")
+(unsafe-struct-set! x1 1 1)

collects/tests/typed-scheme/main.rkt

@@ -5,12 +5,12 @@
 (require rackunit rackunit/text-ui
          mzlib/etc scheme/port
          compiler/compiler
-         scheme/match
+         scheme/match mzlib/compile
          "unit-tests/all-tests.ss"
          "unit-tests/test-utils.ss")
 
 (define (scheme-file? s)
-  (regexp-match ".*[.](rkt|ss|scm)" (path->string s)))
+  (regexp-match ".*[.](rkt|ss|scm)$" (path->string s)))
 
 (define-namespace-anchor a)
 
@@ -23,9 +23,13 @@
                          [(number? e)
                           (and (exn:fail:syntax? val)
                                (= e (length (exn:fail:syntax-exprs val))))]
-                         [else                          
-                          (regexp-match e (exn-message val))]))))
+                         [(or (string? e) (regexp? e))
+                          (regexp-match e (exn-message val))]
+                         [else (error 'exn-pred "bad argument" e)]))))
    args))
+
+(define (cfile file)
+  ((compile-zos #f) (list file) 'auto))
   
 (define (exn-pred p)
   (let ([sexp (with-handlers
@@ -61,9 +65,8 @@
     (make-test-suite dir tests)))
 
 (define (dr p)
-  #;((compile-zos #f) (list p) 'auto)
   (parameterize ([current-namespace (make-base-empty-namespace)])    
-    (dynamic-require `(file ,(path->string p)) #f)))
+    (dynamic-require `(file ,(if (string? p) p (path->string p))) #f)))
 
 (define succ-tests (mk-tests "succeed" 
                              dr
@@ -86,10 +89,54 @@
   (test-suite "Typed Scheme Tests"
               unit-tests int-tests))
 
-(define (go [unit? #f]) (test/gui (if unit? unit-tests tests)))
-(define (go/text [unit? #f]) (run-tests (if unit? unit-tests tests) 'verbose))
+(provide tests int-tests unit-tests)
 
-(provide go go/text)
+(define (go tests) (test/gui tests))
+(define (go/text tests) (run-tests tests 'verbose))
+
+(define (just-one p*)
+  (define-values (path p b) (split-path p*))
+  (define f
+    (if (equal? "fail/" (path->string path))
+        (lambda (p thnk)
+          (define-values (pred info) (exn-pred p))
+          (parameterize ([error-display-handler void])
+            (with-check-info
+             (['predicates info])
+             (check-exn pred thnk))))
+        (lambda (p thnk) (check-not-exn thnk))))
+  (test-suite 
+   (path->string p)
+   (f
+    (build-path path p)
+    (lambda ()
+      (parameterize ([read-accept-reader #t]
+                     [current-load-relative-directory
+                      (path->complete-path path)]
+                     [current-directory path]
+                     [current-output-port (open-output-nowhere)])
+        (dr p))))))
+
+(define (compile-benchmarks)
+  (define (find dir)
+    (for/list ([d (directory-list dir)]
+               #:when (scheme-file? d))
+      d))
+  (define shootout (collection-path "tests" "racket" "benchmarks" "shootout" "typed"))
+  (define common (collection-path "tests" "racket" "benchmarks" "common" "typed"))
+  (define (mk path)
+    (make-test-suite (path->string path)
+                     (for/list ([p (find path)])                       
+                       (parameterize ([current-load-relative-directory
+                                       (path->complete-path path)]
+                                      [current-directory path])
+                         (test-suite (path->string p)
+                                     (check-not-exn (λ () (cfile (build-path path p)))))))))
+  (test-suite "compiling"
+              (mk shootout)
+              (mk common)))
+
+(provide go go/text just-one compile-benchmarks)
 
 
 

collects/tests/typed-scheme/optimizer/generic/begin-float.rkt

@@ -0,0 +1,4 @@
+(module begin-float typed/scheme #:optimize
+  (require racket/unsafe/ops)
+  (begin (- 2.0 3.0)
+         (* 2.0 3.0)))

collects/tests/typed-scheme/optimizer/generic/binary-fixnum.rkt

@@ -0,0 +1,5 @@
+(module binary-fixnum typed/scheme #:optimize
+  (require racket/unsafe/ops)
+  (: f (All (X) ((Vectorof X) -> Natural)))
+  (define (f v)
+    (bitwise-and (vector-length v) 1)))

collects/tests/typed-scheme/optimizer/generic/binary-nonzero-fixnum.rkt

@@ -0,0 +1,3 @@
+(module binary-nonzero-fixnum typed/scheme #:optimize
+  (require racket/unsafe/ops)
+  (quotient (vector-length '#(1 2 3)) 2))

collects/tests/typed-scheme/optimizer/generic/define-begin-float.rkt

@@ -0,0 +1,4 @@
+(module define-begin-float typed/scheme #:optimize
+  (require racket/unsafe/ops)
+  (define a (begin (display (- 2.0 3.0))
+                   (* 2.0 3.0))))

collects/tests/typed-scheme/optimizer/generic/define-call-float.rkt

@@ -0,0 +1,3 @@
+(module define-call-float typed/scheme #:optimize
+  (require racket/unsafe/ops)
+  (define x (cons (+ 1.0 2.0) 3.0)))

collects/tests/typed-scheme/optimizer/generic/define-float.rkt

@@ -0,0 +1,3 @@
+(module define-float typed/scheme #:optimize
+  (require racket/unsafe/ops)
+  (define x (+ 1.0 2.0)))

collects/tests/typed-scheme/optimizer/generic/define-pair.rkt

@@ -0,0 +1,3 @@
+(module define-pair typed/scheme #:optimize
+  (require racket/unsafe/ops)
+  (define x (car '(1 3))))

collects/tests/typed-scheme/optimizer/generic/different-langs.rkt

@@ -0,0 +1,4 @@
+;; to see if the harness supports having the 2 versions of a test being
+;; written in different languages
+(module different-langs typed/scheme #:optimize
+  (+ 1 2))

collects/tests/typed-scheme/optimizer/generic/double-float.rkt

@@ -0,0 +1,3 @@
+(module double-float typed/scheme #:optimize
+  (require racket/unsafe/ops)
+  (+ 2.0 2.0 2.0))

collects/tests/typed-scheme/optimizer/generic/exact-inexact.rkt

@@ -0,0 +1,3 @@
+(module exact-inexact typed/scheme #:optimize
+  (require racket/flonum)
+  (exact->inexact (expt 10 100))) ; must not be a fixnum

collects/tests/typed-scheme/optimizer/generic/fixnum-comparison.rkt

@@ -0,0 +1,3 @@
+(module fixnum-comparison typed/scheme #:optimize
+  (require racket/unsafe/ops)
+  (< (vector-length '#(1 2 3)) (string-length "asdf")))

collects/tests/typed-scheme/optimizer/generic/float-comp.rkt

@@ -0,0 +1,3 @@
+(module float-comp typed/scheme #:optimize
+  (require racket/unsafe/ops)
+  (< 1.0 2.0))

collects/tests/typed-scheme/optimizer/generic/float-fun.rkt

@@ -0,0 +1,5 @@
+(module float-fun typed/scheme #:optimize
+  (require racket/unsafe/ops)
+  (: f (Float -> Float))
+  (define (f x)
+    (+ x 1.0)))

collects/tests/typed-scheme/optimizer/generic/float-promotion.rkt

@@ -0,0 +1,4 @@
+(module float-promotion typed/scheme #:optimize
+  (require racket/unsafe/ops racket/flonum)
+  (+ 1 2.0)
+  (+ (expt 100 100) 2.0))

collects/tests/typed-scheme/optimizer/generic/flvector-length.rkt

@@ -0,0 +1,3 @@
+(module flvector-length typed/scheme #:optimize
+  (require racket/unsafe/ops racket/flonum)
+  (flvector-length (flvector 0.0 1.2)))

collects/tests/typed-scheme/optimizer/generic/fx-fl.rkt

@@ -0,0 +1,3 @@
+(module fx-fl typed/scheme #:optimize
+  (require racket/unsafe/ops)
+  (exact->inexact 1))

collects/tests/typed-scheme/optimizer/generic/in-list.rkt

@@ -0,0 +1,4 @@
+(module in-list typed/scheme #:optimize
+  (require racket/unsafe/ops)
+  (for: ((i : Natural '(1 2 3)))
+    (display i)))

collects/tests/typed-scheme/optimizer/generic/invalid-binary-nonzero-fixnum.rkt

@@ -0,0 +1,4 @@
+(module invalid-binary-nonzero-fixnum typed/scheme #:optimize
+  (: f ( -> Void))
+  (define (f) ; in a function, to prevent evaluation
+    (display (quotient 4 0)))) ; 2 fixnums, but the second is 0, cannot optimize

collects/tests/typed-scheme/optimizer/generic/invalid-exact-inexact.rkt

@@ -0,0 +1,2 @@
+(module exact-inexact typed/scheme #:optimize
+  (exact->inexact 1.0)) ; not an integer, can't optimize

collects/tests/typed-scheme/optimizer/generic/invalid-float-comp.rkt

@@ -0,0 +1,3 @@
+(module float-comp typed/scheme #:optimize
+  (require racket/unsafe/ops)
+  (< 1.0 2))

collects/tests/typed-scheme/optimizer/generic/invalid-float-promotion.rkt

@@ -0,0 +1,2 @@
+(module float-promotion typed/scheme #:optimize
+  (/ 1 2.0)) ; result is not a float, can't optimize

collects/tests/typed-scheme/optimizer/generic/invalid-inexact-complex-parts.rkt

@@ -0,0 +1,2 @@
+(module invalid-inexact-complex-parts.rkt typed/scheme #:optimize
+  (real-part 1+2i))

collects/tests/typed-scheme/optimizer/generic/invalid-make-flrectangular.rkt

@@ -0,0 +1,2 @@
+(module invalid-make-flrectangular typed/scheme #:optimize
+  (make-rectangular 1 2))

collects/tests/typed-scheme/optimizer/generic/invalid-sqrt.rkt

@@ -0,0 +1,2 @@
+(module invalid-sqrt typed/scheme #:optimize
+  (sqrt -2.0)) ; not a nonnegative flonum, can't optimize

collects/tests/typed-scheme/optimizer/generic/invalid-vector-ref.rkt

@@ -0,0 +1,4 @@
+(module invalid-vector-ref typed/scheme #:optimize
+  (: f ((Vectorof Integer) -> Integer))
+  (define (f x)
+    (vector-ref x 0))) ; type is (Vectorof Integer), length is unknown, can't optimize

collects/tests/typed-scheme/optimizer/generic/invalid-vector-set.rkt

@@ -0,0 +1,4 @@
+(module invalid-vector-set typed/scheme #:optimize
+  (: f ((Vectorof Integer) -> Void))
+  (define (f x)
+    (vector-set! x 0 2))) ; type is (Vectorof Integer), length is ot known, can't optimize

collects/tests/typed-scheme/optimizer/generic/known-vector-length.rkt

@@ -0,0 +1,3 @@
+(module known-vector-length typed/scheme #:optimize
+  (require racket/unsafe/ops)
+  (+ 2 (vector-length (ann (vector 1 2) (Vector Integer Integer)))))

collects/tests/typed-scheme/optimizer/generic/let-float.rkt

@@ -0,0 +1,4 @@
+(module let-float typed/scheme #:optimize
+  (require racket/unsafe/ops)
+  (let ((x (+ 3.0 2.0)))
+    (* 9.0 x)))

collects/tests/typed-scheme/optimizer/generic/make-flrectangular.rkt

@@ -0,0 +1,4 @@
+(module make-flrectangular typed/scheme #:optimize
+  (require racket/unsafe/ops racket/flonum)
+  (make-rectangular 1.0 2.2)
+  (make-flrectangular 1.0 2.2))

collects/tests/typed-scheme/optimizer/generic/n-ary-float.rkt

@@ -0,0 +1,3 @@
+(module n-ary-float typed/scheme #:optimize
+  (require racket/unsafe/ops)
+  (+ 1.0 2.0 3.0))

collects/tests/typed-scheme/optimizer/generic/nested-float.rkt

@@ -0,0 +1,3 @@
+(module nested-float typed/scheme #:optimize
+  (require racket/unsafe/ops)
+  (+ 2.0 (+ 3.0 4.0)))

collects/tests/typed-scheme/optimizer/generic/nested-float2.rkt

@@ -0,0 +1,3 @@
+(module nested-float typed/scheme #:optimize
+  (require racket/unsafe/ops)
+  (+ 2.0 (* 3.0 4.0)))

collects/tests/typed-scheme/optimizer/generic/nested-pair1.rkt

@@ -0,0 +1,3 @@
+(module nested-pair typed/scheme #:optimize
+  (require racket/unsafe/ops)
+  (car (cdr '(1 2))))

collects/tests/typed-scheme/optimizer/generic/nested-pair2.rkt

@@ -0,0 +1,3 @@
+(module nested-pair2 typed/scheme #:optimize
+  (require racket/unsafe/ops)
+  (car (cdr (cons 3 (cons (cons 2 '()) 1)))))

collects/tests/typed-scheme/optimizer/generic/pair-fun.rkt

@@ -0,0 +1,7 @@
+(module pair-fun typed/scheme #:optimize
+  (require racket/unsafe/ops)
+  (: f ((Listof Integer) -> Integer))
+  (define (f x)
+    (if (null? x)
+        1
+        (car x))))

collects/tests/typed-scheme/optimizer/generic/quote.rkt

@@ -0,0 +1,2 @@
+(module quote typed/scheme #:optimize
+  '(+ 1.0 2.0))

collects/tests/typed-scheme/optimizer/generic/simple-float.rkt

@@ -0,0 +1,3 @@
+(module simple-float typed/scheme #:optimize
+  (require racket/unsafe/ops)
+  (+ 2.0 3.0))

collects/tests/typed-scheme/optimizer/generic/simple-pair.rkt

@@ -0,0 +1,3 @@
+(module simple-pair typed/scheme #:optimize
+  (require racket/unsafe/ops)
+  (car (cons 1 2)))

collects/tests/typed-scheme/optimizer/generic/sqrt.rkt

@@ -0,0 +1,5 @@
+(module sqrt typed/scheme #:optimize
+  (require racket/unsafe/ops)
+  (: f (Nonnegative-Float -> Nonnegative-Float))
+  (define (f x)
+    (sqrt x)))

collects/tests/typed-scheme/optimizer/generic/structs.rkt

@@ -0,0 +1,6 @@
+(module structs typed/scheme #:optimize
+  (require racket/unsafe/ops)
+  (define-struct: pt ((x : Integer) (y : Integer)) #:mutable)
+  (define a (pt 3 4))
+  (pt-x a)
+  (set-pt-y! a 5))

collects/tests/typed-scheme/optimizer/generic/unary-fixnum-nested.rkt

@@ -0,0 +1,3 @@
+(module unary-fixnum-nested typed/scheme #:optimize
+  (require racket/unsafe/ops racket/fixnum)
+  (abs (bitwise-not (length '(1 2 3)))))

collects/tests/typed-scheme/optimizer/generic/unary-fixnum.rkt

@@ -0,0 +1,3 @@
+(module unary-fixnum typed/scheme #:optimize
+  (require racket/unsafe/ops)
+  (bitwise-not 4))

collects/tests/typed-scheme/optimizer/generic/unary-float.rkt

@@ -0,0 +1,3 @@
+(module float-unary typed/scheme #:optimize
+  (require racket/unsafe/ops)
+  (sin 2.0))

collects/tests/typed-scheme/optimizer/generic/vector-length-nested.rkt

@@ -0,0 +1,7 @@
+(module vector-length typed/scheme #:optimize
+  (require racket/unsafe/ops)
+  (vector-length
+   (vector-ref
+    (ann (vector (vector 1 2) 2 3)
+         (Vector (Vectorof Integer) Integer Integer))
+    0)))

collects/tests/typed-scheme/optimizer/generic/vector-length.rkt

@@ -0,0 +1,3 @@
+(module vector-length typed/scheme #:optimize
+  (require racket/unsafe/ops)
+  (vector-length (vector 1 2 3)))

collects/tests/typed-scheme/optimizer/generic/vector-ref-set-ref.rkt

@@ -0,0 +1,7 @@
+(module vector-ref-set-ref typed/scheme #:optimize
+  (require racket/unsafe/ops)
+  (: x (Vector Integer String))
+  (define x (vector 1 "1"))
+  (vector-ref x 0)
+  (vector-set! x 1 "2")
+  (vector-ref x 1))

collects/tests/typed-scheme/optimizer/generic/vector-ref.rkt

@@ -0,0 +1,3 @@
+(module vector-ref typed/scheme #:optimize
+  (require racket/unsafe/ops)
+  (vector-ref (ann (vector 1 2) (Vector Integer Integer)) 0))

collects/tests/typed-scheme/optimizer/generic/vector-ref2.rkt

@@ -0,0 +1,3 @@
+(module vector-ref2 typed/scheme #:optimize
+  (require racket/unsafe/ops)
+  (vector-ref (vector 1 2 3) 0))

collects/tests/typed-scheme/optimizer/generic/vector-set-quote.rkt

@@ -0,0 +1,5 @@
+(module vector-set-quote typed/scheme #:optimize
+  (require racket/unsafe/ops)
+  (vector-set! (ann (vector '(1 2)) (Vector Any))
+               0
+               '(+ 1.0 2.0))) ; we should not optimize under quote

collects/tests/typed-scheme/optimizer/generic/vector-set.rkt

@@ -0,0 +1,5 @@
+(module vector-set typed/scheme #:optimize
+  (require racket/unsafe/ops)
+  (vector-set! (ann (vector 1 2) (Vector Integer Integer))
+               0
+               1))

collects/tests/typed-scheme/optimizer/generic/vector-set2.rkt

@@ -0,0 +1,3 @@
+(module invalid-vector-set typed/scheme #:optimize
+  (require racket/unsafe/ops)
+  (vector-set! (vector 1 2) 0 2)) ; type is (Vectorof Integer), length is ot known, can't optimize

collects/tests/typed-scheme/optimizer/run.rkt

@@ -0,0 +1,44 @@
+#lang racket
+(require racket/runtime-path)
+
+;; since Typed Scheme's optimizer does source to source transformations,
+;; we compare the expansion of automatically optimized and hand optimized
+;; modules
+(define (read-and-expand file)
+  ;; drop the type tables added by typed scheme, since they can be in a
+  ;; different order each time, and that would make tests fail when they
+  ;; shouldn't
+  (filter
+   ;; drop the "module", its name and its language, so that we can write
+   ;; the 2 versions of each test in different languages (typed and
+   ;; untyped) if need be
+   (match-lambda [(list 'define-values-for-syntax '() _ ...) #f] [_ #t])
+   (cadddr
+    (syntax->datum
+     (parameterize ([current-namespace (make-base-namespace)])
+       (with-handlers
+           ([exn:fail? (lambda (exn)
+                         (printf "~a\n" (exn-message exn))
+                         #'(#f #f #f (#f)))]) ; for cadddr
+         (expand (with-input-from-file file read-syntax))))))))
+
+(define (test gen)
+  (let-values (((base name _) (split-path gen)))
+    (or (regexp-match ".*~" name) ; we ignore backup files
+        (equal? (read-and-expand gen)
+                (read-and-expand (build-path base "../hand-optimized/" name)))
+        (begin (printf "~a failed\n\n" name)
+               #f))))
+
+(define-runtime-path here ".")
+
+(let ((n-failures
+       (if (> (vector-length (current-command-line-arguments)) 0)
+           (if (test (format "generic/~a.rkt"
+                             (vector-ref (current-command-line-arguments) 0)))
+               0 1)
+           (for/fold ((n-failures 0))
+             ((gen (in-directory (build-path here "generic"))))
+             (+ n-failures (if (test gen) 0 1))))))
+  (unless (= n-failures 0)
+    (error (format "~a tests failed." n-failures))))

collects/tests/typed-scheme/run.rkt

@@ -1,7 +1,37 @@
-#lang racket/base
-(require racket/vector)
+#lang racket
+(require racket/vector racket/gui/dynamic)
 
 (require "main.ss")
+
+(define exec (make-parameter go/text))
+(define the-tests (make-parameter tests))
+(define skip-all? #f)
+(define nightly? (make-parameter #f))
+(define opt? (make-parameter #f))
+(define bench? (make-parameter #f))
 (current-namespace (make-base-namespace))
-(unless (= 0 (go/text (vector-member "unit" (current-command-line-arguments))))
-  (error "Typed Scheme Tests did not pass."))
+(command-line
+ #:once-each
+ ["--unit" "run just the unit tests" (the-tests unit-tests)]
+ ["--int" "run just the integration tests" (the-tests int-tests)]
+ ["--nightly" "for the nightly builds" (nightly? #t)]
+ ["--just" path "run only this test" (the-tests (just-one path))]
+ ["--opt" "run the optimizer tests" (opt? #t)]
+ ["--benchmarks" "compile the typed benchmarks" (bench? #t)]
+ ["--gui" "run using the gui" 
+          (if (gui-available?)
+              (begin (exec go))
+              (error "GUI not available"))]
+ )
+
+(cond [(and (nightly?) (eq? 'cgc (system-type 'gc)))
+       (printf "Skipping Typed Racket tests.\n")]
+      [(unless (= 0 ((exec) (the-tests)))
+         (error "Typed Racket Tests did not pass."))
+       (when (opt?)
+         (parameterize ([current-command-line-arguments #()])
+           (dynamic-require '(file "optimizer/run.rkt") #f))
+         (printf "Typed Racket Optimizer tests passed"))
+       (when (bench?)
+         (unless (= 0 ((exec) (compile-benchmarks)))
+           (error "Typed Racket Tests did not pass.")))])

collects/tests/typed-scheme/succeed/apply-dots-list.rkt

@@ -1,4 +1,3 @@
-
 ;; Change the lang to scheme for untyped version
 #lang typed-scheme
 

collects/tests/typed-scheme/succeed/for-ann.rkt

@@ -0,0 +1,3 @@
+#lang typed/racket
+
+(ann (for ([#{i : Integer} '(1 2 3)]) (display i)) Void)

collects/tests/typed-scheme/succeed/for-in-range.rkt

@@ -0,0 +1,3 @@
+#lang typed/racket
+
+(for: ([i : Integer (in-range 10 0 -1)]) i)

collects/tests/typed-scheme/succeed/for-seq.rkt

@@ -0,0 +1,19 @@
+#lang typed/racket
+
+(: Approximate (Natural -> Void))
+(define (Approximate n) ; works
+ (for: : Void ([i : Integer (in-range 10)])
+     (display i)))
+
+(for: : Void ((i : Integer (ann '(1 2 3) (Sequenceof Integer))) ; doesn't
+             (j : Char "abc"))
+     (display (list i j)))
+
+
+(for: : Void ; doesn't
+     ([from-to : (List Symbol Symbol)
+               (ann '([a t] [c g]) (Sequenceof (List Symbol Symbol)))])
+     #t)
+
+
+(for/list: : (Listof Integer) ([i : Integer (in-range 10)]) i) ; works

collects/tests/typed-scheme/succeed/for.rkt

@@ -18,7 +18,7 @@
        (with-output-to-string
          (lambda ()
            (for: : Void
-                 ((i : Exact-Positive-Integer '(1 2 3))
+                 ((i : Integer '(1 2 3))
                   (j : Char "abc")
                   #:when (odd? i)
                   (k : True #(#t #t))
@@ -32,22 +32,22 @@
 
 (check equal?
        (for/list: : (Listof Integer)
-                  ((i : Exact-Positive-Integer '(1 2 3))
-                   (j : Exact-Positive-Integer '(10 20 30))
+                  ((i : Integer '(1 2 3))
+                   (j : Integer '(10 20 30))
                    #:when (odd? i))
                   (+ i j 10))
        '(21 43))
 
 (check equal?
        (for/or: : Boolean
-                ((i : Exact-Positive-Integer '(1 2 3)))
+                ((i : Integer '(1 2 3)))
                 (>= i 3))
        #t)
 
 (check equal?
        (for/or: : Boolean
-                ((i : Exact-Positive-Integer '(1 2 3))
-                 (j : Exact-Positive-Integer '(2 1 3)))
+                ((i : Integer '(1 2 3))
+                 (j : Integer '(2 1 3)))
                 (>= i j))
        #t)
 
@@ -56,9 +56,9 @@
                       (for/lists: : (values (Listof Integer) (Listof Integer))
                                   ((x : (Listof Integer))
                                    (y : (Listof Integer)))
-                                  ((i : Exact-Positive-Integer '(1 2 3))
+                                  ((i : Integer '(1 2 3))
                                    #:when #t
-                                   (j : Exact-Positive-Integer '(10 20 30))
+                                   (j : Integer '(10 20 30))
                                    #:when (> j 12))
                                   (values i j))])
                     (append x y))
@@ -67,19 +67,19 @@
 (check =
        (for/fold: : Integer
                   ((acc : Integer 0))
-                  ((i : Exact-Positive-Integer '(1 2 3))
-                   (j : Exact-Positive-Integer '(10 20 30)))
+                  ((i : Integer '(1 2 3))
+                   (j : Integer '(10 20 30)))
                   (+ acc i j))
        66)
 
 (check =
        (for/fold: : Integer
                   ((acc : Integer 0))
-                  ((i : Exact-Positive-Integer '(1 2 3))
+                  ((i : Integer '(1 2 3))
                    #:when (even? i)
-                   (j : Exact-Positive-Integer '(10 20 30))
+                   (j : Integer '(10 20 30))
                    #:when #t
-                   (k : Exact-Positive-Integer '(100 200 300)))
+                   (k : Integer '(100 200 300)))
                   (+ acc i j k))
        1998)
 
@@ -87,8 +87,8 @@
        (with-output-to-string
          (lambda ()
            (for*: : Void
-                  ((i : Exact-Positive-Integer '(1 2 3))
-                   (j : Exact-Positive-Integer '(10 20 30)))
+                  ((i : Integer '(1 2 3))
+                   (j : Integer '(10 20 30)))
                   (display (list i j)))))
        "(1 10)(1 20)(1 30)(2 10)(2 20)(2 30)(3 10)(3 20)(3 30)")
 
@@ -97,8 +97,8 @@
                       (for*/lists: : (values (Listof Integer) (Listof Integer))
                                    ((x : (Listof Integer))
                                     (y : (Listof Integer)))
-                                   ((i : Exact-Positive-Integer '(1 2 3))
-                                    (j : Exact-Positive-Integer '(10 20 30))
+                                   ((i : Integer '(1 2 3))
+                                    (j : Integer '(10 20 30))
                                     #:when (> j 12))
                                    (values i j))])
                     (append x y))
@@ -107,9 +107,9 @@
 (check =
        (for*/fold: : Integer
                    ((acc : Integer 0))
-                   ((i : Exact-Positive-Integer '(1 2 3))
+                   ((i : Integer '(1 2 3))
                     #:when (even? i)
-                    (j : Exact-Positive-Integer '(10 20 30))
-                    (k : Exact-Positive-Integer '(100 200 300)))
+                    (j : Integer '(10 20 30))
+                    (k : Integer '(100 200 300)))
                    (+ acc i j k))
        1998)

collects/tests/typed-scheme/succeed/generalize-vectors.rkt

@@ -0,0 +1,13 @@
+#lang typed/scheme
+
+(define x (vector 1.0 2.0)) ; should generalize to (Vectorof Float) even though it only contains Nonnegative-Floats
+(vector-set! x 0 -2.0)
+
+(define y (make-vector 2 1.0))
+(vector-set! y 0 -2.0)
+
+(define z #(1.0 2.0))
+(ann z (Vectorof Float))
+
+(define w (build-vector 3 (lambda: ((x : Integer)) (add1 x))))
+(vector-set! w 0 -2)

collects/tests/typed-scheme/succeed/hari-vector-bug.rkt

@@ -0,0 +1,20 @@
+#lang typed/racket
+(define-struct: (A) Base ([prevbase : (Block A)]
+                          [elems : (Vectorof A)]))
+(define-struct: Mt ())
+
+(define-type-alias Block (All (A) (U Mt (Base A))))
+
+(: get-base : (All (A) ((Block A) -> (Base A))))
+(define (get-base block)
+ (if (Mt? block)
+     (error "" 'get-base)
+     (make-Base (Base-prevbase block)
+                (Base-elems block))))
+
+(: get-base2 : (All (A) ((Block A) -> (Base A))))
+(define (get-base2 block)
+ (if (Base? block)
+     (make-Base (Base-prevbase block)
+                (Base-elems block))
+     (error "" 'get-base)))

collects/tests/typed-scheme/succeed/inexact-complex.rkt

@@ -0,0 +1,9 @@
+#lang typed/scheme
+
+(ann 1.1+2.0i Inexact-Complex)
+(ann 1+2.0i Inexact-Complex)
+(ann (real-part 1.1+2.0i) Float)
+(ann (real-part 1+2.0i) Float)
+(ann (imag-part 1.1+2.0i) Float)
+(ann (+ 2.0 2.0+2.0i) Inexact-Complex)
+(ann (+ 2 2.0+2.0i) Inexact-Complex)

collects/tests/typed-scheme/succeed/kw.rkt

@@ -4,3 +4,11 @@
   (open-input-file "foo" #:mode 'binary)  
   (open-input-file "foo" #:mode 'text)
   (open-input-file "foo"))
+
+((inst sort Real Real) (list 1 2 3) >)
+
+((inst sort Real Real) (list 1 2 3) #:key (λ: ([x : Real]) (/ 1 x)) >)
+
+((inst sort Real String) (list 1 2 3) #:key number->string string<?)
+
+((inst sort Real String) (list 1 2 3) #:key number->string string<? #:cache-keys? #t)

collects/tests/typed-scheme/succeed/list-dots.rkt

@@ -0,0 +1,35 @@
+#lang typed/racket
+
+;; tests for the new iteration of ...
+
+(: f (All (a ...) ((List a ...) -> (List a ... a))))
+(define (f x) x)
+
+(: g (All (a ...) (a ... -> (List a ...))))
+(define (g . x) x)
+
+(g 7 7 7)
+
+(: h (All (a ...) (a ... -> (Listof Any))))
+(define (h . x) x)
+
+(: h2 (All (a ...) ((Pair String a) ... -> (Listof (Pair String Any)))))
+(define (h2 . x) x)
+
+(: h3 (All (a ...) ((Pair String a) ... -> (Listof Any))))
+(define (h3 . x) x)
+
+(: h4 (All (a ...) (a ... -> Number)))
+(define (h4 . x) (length x))
+
+(: i (All (a ...) (List a ...) (a ... -> Number) -> Number))
+(define (i xs f) (apply f xs))
+
+(: i2 (All (a ...) (List a ...) (Any * -> Number) -> Number))
+(define (i2 xs f) (apply f xs))
+
+(: i3 (All (a ...) (List a ...) (List a ...) ((Pairof a a) ... -> Number) -> Number))
+(define (i3 xs ys f) (apply f (map cons xs ys)))
+
+(: i4 (All (a ...) (List a ...) (Listof Number) ((Pairof a Number) ... -> Number) -> Number))
+(define (i4 xs ys f) (apply f (map cons xs ys)))

collects/tests/typed-scheme/succeed/manual-examples.rkt

@@ -30,7 +30,7 @@
   (define-typed-struct leaf ([val : Number]))
   (define-typed-struct node ([left : (Un node leaf)] [right : (Un node leaf)]))
   
-  (define: (tree-height [t : (Un node leaf)]) : Number
+  (define: (tree-height [t : (Un node leaf)]) : Integer
     (cond [(leaf? t) 1]
           [else (max (tree-height (node-left t))
                      (tree-height (node-right t)))]))
@@ -46,7 +46,7 @@
   
   (define-type-alias tree (Un node leaf))
   
-  (define: (tree-height [t : tree]) : Number
+  (define: (tree-height [t : tree]) : Integer
     (cond [(leaf? t) 1]
           [else (max (tree-height (node-left t))
                      (tree-height (node-right t)))]))

collects/tests/typed-scheme/succeed/map-nonempty.rkt

@@ -1,6 +1,6 @@
 #lang typed/scheme
 
-(: x (Pair Number (Listof Number)))
+(: x (Pair Integer (Listof Integer)))
 (define x (cons 1 (list 1 2 3 4)))
 
-(apply max (ann (map add1 x) : (Pair Number (Listof Number))))
+(apply max (ann (map add1 x) : (Pair Integer (Listof Integer))))

collects/tests/typed-scheme/succeed/mpair.rkt

@@ -0,0 +1,6 @@
+#lang typed/racket
+
+(define: x : (MPairof Integer Integer) (mcons 1 2))
+(set-mcar! x -7)
+(mcar x)
+(mcdr x)

collects/tests/typed-scheme/succeed/new-metrics.rkt

@@ -93,16 +93,16 @@
 ;; ----------------------------------------
 ;; depth
 
-(: sexp-depth (Any -> Number))
+(: sexp-depth (Any -> Integer))
 (define (sexp-depth sexp)
   (cond
     [(pair? sexp)
      (+ (max-sexp-depth sexp) 1)]
     [else 0]))
 
-(: max-sexp-depth (Any -> Number))
+(: max-sexp-depth (Any -> Integer))
 (define (max-sexp-depth losx)
-  (improper-foldr (λ: ([t : Any] [r : Number]) (max (sexp-depth t) r)) 0 losx))
+  (improper-foldr (λ: ([t : Any] [r : Integer]) (max (sexp-depth t) r)) 0 losx))
 
 (: avg-sexp-depth ((Listof Any) -> Number))
 (define (avg-sexp-depth sexps)
@@ -201,7 +201,7 @@
 ;; ----------------------------------------
 ;; expression size
 
-(: atoms (Any -> Number))
+(: atoms (Any -> Integer))
 (define (atoms sexp)
   (cond
     [(null? sexp) 0]

collects/tests/typed-scheme/succeed/nonnegative-float.rkt

@@ -0,0 +1,6 @@
+#lang typed/scheme
+
+(ann (+ 1.0 2.1) Nonnegative-Float)
+(ann (+ 1 2.1) Nonnegative-Float)
+(ann (* 1.2 3.1) Nonnegative-Float)
+(ann (sqrt 3.5) Nonnegative-Float)

collects/tests/typed-scheme/succeed/optimize-simple.rkt

@@ -0,0 +1,3 @@
+#lang typed/racket #:optimize
+
+(+ 3 4)

collects/tests/typed-scheme/succeed/pair-test3.rkt

@@ -11,7 +11,7 @@
   '((((1 . "1") . (#t))
      . ((#f . #\f) . ("2")))
     . ((("3" . 4) . (1.0))
-       . ((#(2.0 3.0 4.0) . #t)
+       . ((#(2.0 3.0 -4.0) . #t)
           . ((2.0 3.0 4.0) . #f)))))
 
 

collects/tests/typed-scheme/succeed/pr10057.rkt

@@ -0,0 +1,5 @@
+#lang typed-scheme
+(require scheme/match)
+(ann (match '(a b c)
+       [(list sym more ...) 1]
+       [else 1]) Integer)

collects/tests/typed-scheme/succeed/priority-queue.scm

@@ -76,7 +76,7 @@
 		(error "priority queue empty"))))
 
 (pdefine: (a) (insert [x : a] [p : number] [pq : (priority-queue a)]) : (priority-queue a)
-	  (make (heap:insert (#{cons :: (case-lambda (a (list-of a) -> (list-of a)) (number a -> (cons number a)))} p x) (heap pq))))
+	  (make (heap:insert (cons p x) (heap pq))))
 
 ;; FIXME -- too many annotations needed on cons
 (pdefine: (a) (insert* [xs : (list-of a)] [ps : (list-of number)] [pq : (priority-queue a)]) : (priority-queue a)

collects/tests/typed-scheme/succeed/provide-case-rest.rkt

@@ -0,0 +1,8 @@
+#lang typed/racket
+
+(provide foo)
+
+(define foo
+ (case-lambda:
+   (((x : Number)) x)
+   (((x : Number) (y : Number) z : Number *) y)))

collects/tests/typed-scheme/succeed/racket-struct.rkt

@@ -0,0 +1,7 @@
+#lang typed/racket
+
+(struct: x ([y : Number]))
+
+(x 1)
+(x-y (x 7))
+(ann x? (Any -> Boolean : x))

collects/tests/typed-scheme/succeed/rec-het-vec-infer.rkt

@@ -0,0 +1,9 @@
+#lang typed/racket
+
+(define-type (Set X) (Rec Set (U Null (Vector X Set))))
+
+(: get-set-root (All (X) ((Set X) -> X)))
+(define (get-set-root s) (error 'fail))
+
+(: set-size (All (X) ((Set X) -> X)))
+(define (set-size x) (get-set-root x))

collects/tests/typed-scheme/succeed/test-child-field.rkt

@@ -0,0 +1,10 @@
+#lang typed/racket
+
+(define-struct:  x ([a : Any]))
+(define-struct: (A) (y x) ([b : A]))
+
+(: f : (y Any) -> String)
+(define (f v)
+  (if (string? (y-b v))
+      (y-b v)
+      "foo"))

collects/tests/typed-scheme/succeed/threads-and-channels.rkt

@@ -0,0 +1,50 @@
+#lang typed/scheme
+
+(: chan (Channelof Symbol))
+(define chan (make-channel))
+
+(define (reader)
+  (thread
+   (lambda ()
+     (let: loop : True ((i : Integer 10))
+       (if (= i 0)
+           #t
+           (begin (channel-get chan)
+                  (loop (- i 1))))))))
+
+(: writer (Symbol -> Thread))
+(define (writer x)
+  (thread
+   (lambda ()
+     (channel-put chan x)
+     (channel-put chan x))))
+
+(reader)
+(writer 'a)
+(writer 'b)
+(writer 'c)
+(writer 'd)
+(writer 'e)
+
+
+(define-type JumpingChannel (Rec JumpingChannel (Channelof (Pair JumpingChannel Symbol))))
+(: jump-chan JumpingChannel)
+(define jump-chan (make-channel))
+
+(define (jumping-reader)
+  (thread
+   (lambda ()
+     (let: loop : True ((i : Integer 3)
+                        (c : JumpingChannel jump-chan))
+       (if (= i 0)
+           #t
+           (loop (- i 1)
+                 (car (channel-get c))))))))
+
+(jumping-reader)
+(let: ((c2 : JumpingChannel (make-channel)))
+  (channel-put jump-chan (cons c2 'a))
+  (let: ((c3 : JumpingChannel (make-channel)))
+    (channel-put c2 (cons c3 'b))
+    (let: ((c4 : JumpingChannel (make-channel)))
+      (channel-put c3 (cons c4 'c)))))

collects/tests/typed-scheme/succeed/unsafe-struct-parent.rkt

@@ -0,0 +1,26 @@
+#lang typed/scheme
+(require racket/unsafe/ops)
+
+(define-struct: foo ((x : Integer) (y : String)))
+(define-struct: (bar foo) ((z : Float)))
+
+(define a (make-foo 1 "1"))
+(define b (make-bar 2 "2" 2.0))
+
+(= (+ (unsafe-struct-ref a 0) 2) 3)
+(string=? (string-append (unsafe-struct-ref a 1) "\n") "1\n")
+(= (+ (unsafe-struct-ref b 0) 2) 4)
+(string=? (string-append (unsafe-struct-ref b 1) "\n") "2\n")
+(= (+ (unsafe-struct-ref b 2) 2.0) 4.0)
+
+(unsafe-struct-set! a 0 2)
+(unsafe-struct-set! a 1 "2")
+(unsafe-struct-set! b 0 3)
+(unsafe-struct-set! b 1 "3")
+(unsafe-struct-set! b 2 3.0)
+
+(= (+ (unsafe-struct-ref a 0) 2) 4)
+(string=? (string-append (unsafe-struct-ref a 1) "\n") "2\n")
+(= (+ (unsafe-struct-ref b 0) 2) 5)
+(string=? (string-append (unsafe-struct-ref b 1) "\n") "3\n")
+(= (+ (unsafe-struct-ref b 2) 2.0) 5.0)

collects/tests/typed-scheme/succeed/unsafe-struct.rkt

@@ -0,0 +1,14 @@
+#lang typed/scheme
+(require racket/unsafe/ops)
+
+(define-struct: x ((a : Integer) (b : String)) #:mutable)
+
+(define x1 (make-x 1 "1"))
+
+(= (+ (unsafe-struct-ref x1 0) 2) 3)
+(string=? (string-append (unsafe-struct-ref x1 1) "\n") "1\n")
+
+(unsafe-struct-set! x1 0 2)
+(unsafe-struct-set! x1 1 "2")
+(= (+ (unsafe-struct-ref x1 0) 2) 4)
+(string=? (string-append (unsafe-struct-ref x1 1) "\n") "2\n")

collects/tests/typed-scheme/unit-tests/parse-type-tests.rkt

@@ -1,12 +1,13 @@
 #lang scheme/base
 (require "test-utils.ss" (for-syntax scheme/base)
+         racket/set
          (utils tc-utils)
-	 (env type-alias-env type-environments type-name-env init-envs)
+	 (env type-alias-env type-env-structs tvar-env type-name-env init-envs)
 	 (rep type-rep)
 	 (rename-in (types comparison subtype union utils convenience)
                     [Un t:Un] [-> t:->])
-         (private base-types-new base-types-extra colon)
-         (for-template (private base-types-new base-types-extra base-env colon))
+         (private base-types base-types-extra colon)
+         (for-template (private base-types base-types-extra base-env colon))
          (private parse-type)
          rackunit)
 
@@ -74,6 +75,11 @@
    [(-> (values Number Boolean Number)) (t:-> (-values (list N B N)))]
    [(Number -> Number) (t:-> N N)]
    [(Number -> Number) (t:-> N N)]
+   [(All (A) Number -> Number) (-poly (a) (t:-> N N))]
+   [(All (A) (Number -> Number)) (-poly (a) (t:-> N N))]
+   [(All (A) A -> A) (-poly (a) (t:-> a a))]
+   [(All (A) A → A) (-poly (a) (t:-> a a))]
+   [(All (A) (A -> A)) (-poly (a) (t:-> a a))]
    ;; requires transformer time stuff that doesn't work
    #;[(Refinement even?) (make-Refinement #'even?)]
    [(Number Number Number Boolean -> Number) (N N N B . t:-> . N)]
@@ -100,8 +106,7 @@
    
    [(Listof Number) (make-Listof  N)]
    
-   [a (-v a) (extend-env (list 'a) (list (-v a))
-                            initial-tvar-env)]
+   [a (-v a) (set-add initial-tvar-env 'a)]
    [(All (a ...) (a ... -> Number))
     (-polydots (a) ((list) [a a] . ->... . N))]
    

collects/tests/typed-scheme/unit-tests/subst-tests.rkt

@@ -2,7 +2,7 @@
 
 (require "test-utils.ss" (for-syntax scheme/base)
          (rep type-rep)
-	 (types utils abbrev)
+	 (types utils abbrev substitute)
          rackunit)
 
 (define-syntax-rule (s img var tgt result)

collects/tests/typed-scheme/unit-tests/subtype-tests.rkt

@@ -3,7 +3,7 @@
 (require "test-utils.ss"
          (types subtype convenience union)
 	 (rep type-rep)
-	 (env init-envs type-environments)
+	 (env init-envs type-env-structs)
 	 (r:infer infer infer-dummy)
          rackunit
          (for-syntax scheme/base))
@@ -112,11 +112,15 @@
    
    [(-values (list -Number)) (-values (list Univ))]
    
-   [(-poly (a) ((Un (make-Base 'foo #'dummy) (-struct 'bar #f (list -Number a) null #'values)) . -> . (-lst a)))
-    ((Un (make-Base 'foo #'dummy) (-struct 'bar #f (list -Number (-pair -Number (-v a))) null #'values)) 
+   [(-poly (b) ((Un (make-Base 'foo #'dummy)
+                    (-struct 'bar #f 
+                             (list (make-fld -Number #'values #f) (make-fld b #'values #f))
+                             #'values))
+                . -> . (-lst b)))
+    ((Un (make-Base 'foo #'dummy) (-struct 'bar #f (list (make-fld -Number #'values #f) (make-fld (-pair -Number (-v a)) #'values #f)) #'values))
      . -> . (-lst (-pair -Number (-v a))))]
-   [(-poly (a) ((-struct 'bar #f (list -Number a) null #'values) . -> . (-lst a)))
-    ((-struct 'bar #f (list -Number (-pair -Number (-v a))) null #'values) . -> . (-lst (-pair -Number (-v a))))]
+   [(-poly (b) ((-struct 'bar #f (list (make-fld -Number #'values #f) (make-fld b #'values #f)) #'values) . -> . (-lst b)))
+    ((-struct 'bar #f (list (make-fld -Number #'values #f) (make-fld (-pair -Number (-v a)) #'values #f)) #'values) . -> . (-lst (-pair -Number (-v a))))]
    
    [(-poly (a) (a . -> . (make-Listof a))) ((-v b) . -> . (make-Listof (-v b)))]
    [(-poly (a) (a . -> . (make-Listof a))) ((-pair -Number (-v b)) . -> . (make-Listof (-pair -Number (-v b))))]
@@ -128,6 +132,9 @@
    (FAIL (-> Univ) (null Univ . ->* . Univ))
 
    [(cl->* (-Number . -> . -String) (-Boolean . -> . -String)) ((Un -Boolean -Number) . -> . -String)]
+   [(-struct 'a #f null #'values) (-struct 'a #f null #'values)]
+   [(-struct 'a #f (list (make-fld -String #'values #f)) #'values) (-struct 'a #f (list (make-fld -String #'values #f)) #'values)]
+   [(-struct 'a #f (list (make-fld -String #'values #f)) #'values) (-struct 'a #f (list (make-fld Univ #'values #f)) #'values)]
    ))
 
 (define-go 

collects/tests/typed-scheme/unit-tests/type-equal-tests.rkt

@@ -24,6 +24,8 @@
        #'(test-suite "Tests for type equality"
                      cl1 ... cl2 ...))]))
 
+(define (fld* t) (make-fld t (datum->syntax #'here 'values) #f))
+
 (define (type-equal-tests)
   (te-tests
    [-Number -Number]
@@ -38,13 +40,12 @@
    ;; found bug
    [FAIL (Un (-mu heap-node 
                   (-struct 'heap-node #f
-                           (list (-base 'comparator) -Number (-v a) (Un heap-node (-base 'heap-empty)))
-                           null #'values)) 
+                           (map fld* (list (-base 'comparator) -Number (-v a) (Un heap-node (-base 'heap-empty))))
+                           #'values)) 
              (-base 'heap-empty))
          (Un (-mu heap-node 
                   (-struct 'heap-node #f
-                           (list (-base 'comparator) -Number (-pair -Number -Number) (Un heap-node (-base 'heap-empty)))
-                           null #'values)) 
+                           (map fld* (list (-base 'comparator) -Number (-pair -Number -Number) (Un heap-node (-base 'heap-empty)))) #'values))
              (-base 'heap-empty))]))
 
 (define-go

collects/tests/typed-scheme/unit-tests/typecheck-tests.rkt

@@ -15,17 +15,18 @@
                     [true-lfilter -true-lfilter]
                     [true-filter -true-filter]
                     [-> t:->])
-         (utils tc-utils utils)
+         (except-in (utils tc-utils utils) infer)
+         typed-scheme/infer/infer-dummy typed-scheme/infer/infer
          unstable/mutated-vars
-         (env type-name-env type-environments init-envs)
+         (env type-name-env type-env-structs init-envs)
          rackunit rackunit/text-ui
          syntax/parse
          (for-syntax (utils tc-utils)
                      (typecheck typechecker)
-	             (env type-env)
+	             (env global-env)
 	             (private base-env base-env-numeric
 			      base-env-indexing))
-         (for-template (private base-env base-types-new base-types-extra
+         (for-template (private base-env base-types base-types-extra
 				base-env-numeric
 				base-env-indexing))
          (for-syntax syntax/kerncase syntax/parse))
@@ -37,7 +38,6 @@
 (define Sym -Symbol)
 (define -Pos -ExactPositiveInteger)
 (define R -Real)
-(define F -Flonum)
 
 (define (g) (run typecheck-tests))
 
@@ -62,20 +62,24 @@
     [(_ e)
      #`(parameterize ([delay-errors? #f]
                       [current-namespace (namespace-anchor->namespace anch)]
+                      [custom-printer #t]
+                      [infer-param infer]
                       [orig-module-stx (quote-syntax e)])
          (let ([ex (expand 'e)])
-           (find-mutated-vars ex)
-           (values (lambda () (tc-expr ex)) ex)))]))
+           (parameterize ([mutated-vars (find-mutated-vars ex)])
+             (values (lambda () (tc-expr ex)) ex))))]))
 
 (define-syntax (tc-expr/expand stx)
   (syntax-case stx ()
     [(_ e)
      #`(parameterize ([delay-errors? #f]
                       [current-namespace (namespace-anchor->namespace anch)]
+                      [custom-printer #t]
+                      [infer-param infer]
                       [orig-module-stx (quote-syntax e)])
          (let ([ex (expand 'e)])
-           (find-mutated-vars ex)
-           (tc-expr ex)))]))
+           (parameterize ([mutated-vars (find-mutated-vars ex)])
+             (tc-expr ex))))]))
 
 ;; check that an expression typechecks correctly
 (define-syntax (tc-e stx)
@@ -136,24 +140,24 @@
                    (+ 1 (car x))
                    5))
          N]
-        (tc-e/t (if (let ([y 12]) y) 3 4) -Pos)
-        (tc-e/t 3 -Pos)
+        (tc-e/t (if (let ([y 12]) y) 3 4) -PositiveFixnum)
+        (tc-e/t 3 -PositiveFixnum)
         (tc-e/t "foo" -String)
         (tc-e (+ 3 4) -Pos)
-        [tc-e/t (lambda: () 3) (t:-> -Pos : -true-lfilter)]
-        [tc-e/t (lambda: ([x : Number]) 3) (t:-> N -Pos : -true-lfilter)]
-        [tc-e/t (lambda: ([x : Number] [y : Boolean]) 3) (t:-> N B -Pos : -true-lfilter)]
-        [tc-e/t (lambda () 3) (t:-> -Pos : -true-lfilter)]
-        [tc-e (values 3 4) #:ret (ret (list -Pos -Pos) (list -true-filter -true-filter))]
-        [tc-e (cons 3 4) (-pair -Pos -Pos)]
+        [tc-e/t (lambda: () 3) (t:-> -PositiveFixnum : -true-lfilter)]
+        [tc-e/t (lambda: ([x : Number]) 3) (t:-> N -PositiveFixnum : -true-lfilter)]
+        [tc-e/t (lambda: ([x : Number] [y : Boolean]) 3) (t:-> N B -PositiveFixnum : -true-lfilter)]
+        [tc-e/t (lambda () 3) (t:-> -PositiveFixnum : -true-lfilter)]
+        [tc-e (values 3 4) #:ret (ret (list -PositiveFixnum -PositiveFixnum) (list -true-filter -true-filter))]
+        [tc-e (cons 3 4) (-pair -PositiveFixnum -PositiveFixnum)]
         [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 -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 #(3 4 5) (make-HeterogenousVector (list -Nat -Nat -Nat))]
+        [tc-e/t '(2 3 4) (-lst* -PositiveFixnum -PositiveFixnum -PositiveFixnum)]
+        [tc-e/t '(2 3 #t) (-lst* -PositiveFixnum -PositiveFixnum (-val #t))]
+        [tc-e/t #(2 3 #t) (make-HeterogenousVector (list -Nat -Nat (-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)))]
@@ -164,9 +168,9 @@
         [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 -top -top))])]
-        [tc-e/t (values 3) -Pos]
+        [tc-e/t (values 3) -PositiveFixnum]
         [tc-e (values) #:ret (ret null)]
-        [tc-e (values 3 #f) #:ret (ret (list -Pos (-val #f)) (list (-FS -top -bot) (-FS -bot -top)))]
+        [tc-e (values 3 #f) #:ret (ret (list -PositiveFixnum (-val #f)) (list (-FS -top -bot) (-FS -bot -top)))]
         [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))
@@ -196,8 +200,8 @@
 			'bc))
 	      N]
         [tc-e/t (let: ((x : Number 3)) (if (boolean? x) (not x) #t)) (-val #t)]
-        [tc-e/t (begin 3) -Pos]
-        [tc-e/t (begin #f 3) -Pos]
+        [tc-e/t (begin 3) -PositiveFixnum]
+        [tc-e/t (begin #f 3) -PositiveFixnum]
         [tc-e/t (begin #t) (-val #t)]
         [tc-e/t (begin0 #t) (-val #t)]
         [tc-e/t (begin0 #t 3) (-val #t)]
@@ -205,14 +209,14 @@
         [tc-e #f #:ret (ret (-val #f) (-FS -bot -top))]
         [tc-e/t '#t (-val #t)]
         [tc-e '#f #:ret (ret (-val #f) (-FS -bot -top))]
-        [tc-e/t (if #f 'a 3) -Pos]
+        [tc-e/t (if #f 'a 3) -PositiveFixnum]
         [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]))
-              -Pos]
+              -PositiveFixnum]
         [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]
@@ -236,7 +240,7 @@
                     (if (list? x)
                         (begin (car x) 1)
                         2))
-              -Pos]
+              -PositiveFixnum]
         
         
         [tc-e (let: ([x : (U Number Boolean) 3])
@@ -245,7 +249,7 @@
                         3))
               N]
         
-        [tc-e (let ([x 1]) x) -Pos]
+        [tc-e (let ([x 1]) x) -PositiveFixnum]
         [tc-e (let ([x 1]) (boolean? x)) #:ret (ret -Boolean (-FS -bot -top))]
         [tc-e (boolean? number?) #:ret (ret -Boolean (-FS -bot -top))]
         
@@ -266,9 +270,9 @@
                 (if (eq? x 1)
                     12
                     14))
-              -Pos]
+              -PositiveFixnum]
         
-        [tc-e (car (append (list 1 2) (list 3 4))) -Pos]
+        [tc-e (car (append (list 1 2) (list 3 4))) -PositiveFixnum]
         
         [tc-e 
          (let-syntax ([a 
@@ -278,8 +282,8 @@
                  (string-append "foo" (a v))))
          -String]
         
-        [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-e (apply (plambda: (a) [x : a *] x) '(5)) (-lst -PositiveFixnum)]
+        [tc-e (apply append (list '(1 2 3) '(4 5 6))) (-lst -PositiveFixnum)]
         
         [tc-err ((case-lambda: [([x : Number]) x]
                                [([y : Number] [x : Number]) x])
@@ -315,9 +319,9 @@
         [tc-e (let* ([sym 'squarf]
                      [x (if (= 1 2) 3 sym)])
                 x)
-              (t:Un (-val 'squarf) -Pos)]
+              (t:Un (-val 'squarf) -PositiveFixnum)]
         
-        [tc-e/t (if #t 1 2) -Pos]
+        [tc-e/t (if #t 1 2) -PositiveFixnum]
         
         
         ;; eq? as predicate
@@ -342,12 +346,12 @@
                      [x (if (= 1 2) 3 sym)])
                 (if (eq? x sym) 3 x))
               #:proc (syntax-parser [(_ _ (_ ([(x) _]) _))
-                                     (ret -Pos (-FS -top -top))])]
+                                     (ret -PositiveFixnum (-FS -top -top))])]
         [tc-e (let* ([sym 'squarf]
                      [x (if (= 1 2) 3 sym)])
                 (if (eq? sym x) 3 x))
                #:proc (syntax-parser [(_ _ (_ ([(x) _]) _))
-                                      (ret -Pos (-FS -top -top))])]
+                                      (ret -PositiveFixnum (-FS -top -top))])]
         ;; equal? as predicate for symbols
         [tc-e (let: ([x : (Un 'foo Number) 'foo])
                     (if (equal? x 'foo) 3 x))
@@ -360,22 +364,22 @@
                      [x (if (= 1 2) 3 sym)])
                 (if (equal? x sym) 3 x))
                #:proc (syntax-parser [(_ _ (_ ([(x) _]) _))
-                                      (ret -Pos (-FS -top -top))])]
+                                      (ret -PositiveFixnum (-FS -top -top))])]
         [tc-e (let* ([sym 'squarf]
                      [x (if (= 1 2) 3 sym)])
                 (if (equal? sym x) 3 x))
               #:proc (syntax-parser [(_ _ (_ ([(x) _]) _))
-                                     (ret -Pos (-FS -top -top))])]
+                                     (ret -PositiveFixnum (-FS -top -top))])]
         
         [tc-e (let: ([x : (Listof Symbol)'(a b c)])
                     (cond [(memq 'a x) => car]
                           [else 'foo]))
               Sym]
         
-        [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 (list 1 2 3) (-lst* -PositiveFixnum -PositiveFixnum -PositiveFixnum)]
+        [tc-e (list 1 2 3 'a) (-lst* -PositiveFixnum -PositiveFixnum -PositiveFixnum (-val 'a))]
         
-        [tc-e `(1 2 ,(+ 3 4)) (-lst* -Pos -Pos -Pos)]
+        [tc-e `(1 2 ,(+ 3 4)) (-lst* -PositiveFixnum -PositiveFixnum -Pos)]
         
         [tc-e (let: ([x : Any 1])
                     (when (and (list? x) (not (null? x)))
@@ -394,7 +398,7 @@
                       'foo))
                 (t:Un (-val 'foo) (-pair Univ (-lst Univ)))]
         
-        [tc-e (cadr (cadr (list 1 (list 1 2 3) 3))) -Pos]
+        [tc-e (cadr (cadr (list 1 (list 1 2 3) 3))) -PositiveFixnum]
         
         
         
@@ -409,7 +413,7 @@
         [tc-e/t (let: ([x : Any 3])
                       (if (and (list? x) (not (null? x)))
                           (begin (car x) 1) 2))
-              -Pos]
+              -PositiveFixnum]
         
         ;; set! tests
         [tc-e (let: ([x : Any 3])
@@ -466,7 +470,7 @@
         [tc-e/t (let* ([z 1]
                        [p? (lambda: ([x : Any]) (number? z))])
                   (lambda: ([x : Any]) (if (p? x) 11 12)))
-                (t:-> Univ -Pos : -true-lfilter)]
+                (t:-> Univ -PositiveFixnum : -true-lfilter)]
         [tc-e/t (let* ([z 1]
                        [p? (lambda: ([x : Any]) (number? z))])
                   (lambda: ([x : Any]) (if (p? x) x 12)))
@@ -479,7 +483,7 @@
         [tc-e/t (let* ([z 1]
                        [p? (lambda: ([x : Any]) (not (number? z)))])
                   (lambda: ([x : Any]) (if (p? x) x 12)))
-                (t:-> Univ -Pos : -true-lfilter)]
+                (t:-> Univ -PositiveFixnum : -true-lfilter)]
         [tc-e/t (let* ([z 1]
                        [p? (lambda: ([x : Any]) z)])
                   (lambda: ([x : Any]) (if (p? x) x 12)))
@@ -510,7 +514,7 @@
         ;; w-c-m
         [tc-e/t (with-continuation-mark 'key 'mark 
                 3)
-              -Pos]
+              -PositiveFixnum]
         [tc-err (with-continuation-mark (5 4) 1
                   3)]
         [tc-err (with-continuation-mark 1 (5 4) 
@@ -539,14 +543,14 @@
         [tc-err (call-with-values (lambda () (values 2 1))
                                   (lambda: ([x : String] [y : Number]) (+ x y)))]
         ;; quote-syntax
-        [tc-e/t #'3 (-Syntax -Pos)]
-        [tc-e/t #'(1 2 3) (-Syntax (-lst* -Pos -Pos -Pos))]
+        [tc-e/t #'3 (-Syntax -PositiveFixnum)]
+        [tc-e/t #'(1 2 3) (-Syntax (-lst* -PositiveFixnum -PositiveFixnum -PositiveFixnum))]
         
         ;; testing some primitives
         [tc-e (let ([app apply]
                     [f (lambda: [x : Number *] 3)])
                 (app f (list 1 2 3)))
-              -Pos]
+              -PositiveFixnum]
         [tc-e ((lambda () (call/cc (lambda: ([k : (Number -> (U))]) (if (read) 5 (k 10))))))
               N]
         
@@ -584,7 +588,7 @@
                         (+ z w)))
                     (g 4))
                   5)
-                -Pos]
+                -PositiveFixnum]
         
         [tc-err (let ()
                   (define x x)
@@ -615,11 +619,11 @@
         
         [tc-e/t (if #f 1 'foo) (-val 'foo)]
         
-        [tc-e (list* 1 2 3) (-pair -Pos (-pair -Pos -Pos))]
+        [tc-e (list* 1 2 3) (-pair -PositiveFixnum (-pair -PositiveFixnum -PositiveFixnum))]
         
         [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 -Pos)]
-        [tc-e (apply append (list 1) (list 2) (list 3) (list (list 1) (list "foo"))) (-lst (t:Un -String -Pos))]
+        [tc-e (apply append (list 1) (list 2) (list 3) (list (list 1) (list 1))) (-lst -PositiveFixnum)]
+        [tc-e (apply append (list 1) (list 2) (list 3) (list (list 1) (list "foo"))) (-lst (t:Un -String -PositiveFixnum))]
         [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)))]
@@ -647,12 +651,12 @@
         
         ;; instantiating dotted terms
         [tc-e/t (inst (plambda: (a ...) [xs : a ... a] 3) Integer Boolean Integer)
-                (-Integer B -Integer . t:-> . -Pos : -true-lfilter)]
+                (-Integer B -Integer . t:-> . -PositiveFixnum : -true-lfilter)]
         [tc-e/t (inst (plambda: (a ...) [xs : (a ... a -> Integer) ... a] 3) Integer Boolean Integer)
                 ((-Integer B -Integer . t:-> . -Integer)
                  (-Integer B -Integer . t:-> . -Integer)
                  (-Integer B -Integer . t:-> . -Integer)
-                 . t:-> . -Pos : -true-filter)]
+                 . t:-> . -PositiveFixnum : -true-filter)]
         
         [tc-e/t (plambda: (z x y ...) () (inst map z x y ... y))
               (-polydots (z x y) (t:-> (cl->*
@@ -739,7 +743,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 -Pos -Pos -Pos))]
+        [tc-e (apply values (list 1 2 3)) #:ret (ret (list -PositiveFixnum -PositiveFixnum -PositiveFixnum))]
         
         [tc-e/t (ann (if #t 3 "foo") Integer) -Integer]
         
@@ -779,7 +783,7 @@
         (tc-e (or (string->number "7") 7) 
               #:ret (ret -Number -true-filter))
         [tc-e (let ([x 1]) (if x x (add1 x))) 
-              #:ret (ret -Pos (-FS -top -top))]
+              #:ret (ret -PositiveFixnum (-FS -top -top))]
         [tc-e (let: ([x : (U (Vectorof Number) String) (vector 1 2 3)])
                 (if (vector? x) (vector-ref x 0) (string-length x)))
          -Number]
@@ -793,7 +797,8 @@
               Univ]        
         [tc-e (floor 1/2) -Integer]
         [tc-e (ceiling 1/2) -Integer]
-        [tc-e (truncate 0.5) -Flonum]
+        [tc-e (truncate 0.5) -NonnegativeFlonum]
+        [tc-e (truncate -0.5) -Flonum]
         [tc-e/t (ann (lambda (x) (lambda (x) x))
                      (Integer -> (All (X) (X -> X))))
                 (t:-> -Integer (-poly (x) (t:-> x x)))]
@@ -802,6 +807,25 @@
                              (eq? 'r x)
                              (eq? 's x)))
                 (make-pred-ty (t:Un (-val 'q) (-val 'r) (-val 's)))]
+        [tc-e (let: ([x : Exact-Positive-Integer 1])
+                (vector-ref #("a" "b") x)
+                (vector-ref #("a" "b") (sub1 x))
+                (vector-ref #("a" "b") (- x 1)))
+              -String]
+        [tc-err (string-append "bar" (if (zero? (ann 0.0 Float)) #f "foo"))]
+        [tc-err (do: : Void
+                     ([j : Natural (+ i 'a) (+ j i)])
+                     ((>= j 10))
+                     #f)]
+        [tc-err (apply +)]
+        [tc-e/t
+         (let ([x eof])
+           (if (procedure? x)
+               x
+               (lambda (z) (eq? x z))))
+         (make-pred-ty (-val eof))]
+        [tc-e ((inst map Number (Pairof Number Number)) car (ann (list (cons 1 2) (cons 2 3) (cons 4 5)) (Listof (Pairof Number Number))))
+              (-lst -Number)]
         )
   (test-suite
    "check-type tests"
@@ -811,10 +835,21 @@
    (test-not-exn "Doesn't fail on equal types" (lambda () (check-type #'here N N))))
   (test-suite
    "tc-literal tests"
-   (tc-l 5 -ExactPositiveInteger)
-   (tc-l 5# -Flonum)
-   (tc-l 5.0 -Flonum)
-   (tc-l 5.1 -Flonum)
+   (tc-l 5 -PositiveFixnum)
+   (tc-l -5 -NegativeFixnum)
+   (tc-l 0 -Zero)
+   (tc-l 0.0 -NonnegativeFlonum)
+   (tc-l -0.0 -Flonum)
+   (tc-l 5# -NonnegativeFlonum)
+   (tc-l 5.0 -NonnegativeFlonum)
+   (tc-l 5.1 -NonnegativeFlonum)
+   (tc-l -5# -Flonum)
+   (tc-l -5.0 -Flonum)
+   (tc-l -5.1 -Flonum)
+   (tc-l 1+1i N)
+   (tc-l 1+1.0i -InexactComplex)
+   (tc-l 1.0+1i -InexactComplex)
+   (tc-l 1.0+1.1i -InexactComplex)
    (tc-l #t (-val #t))
    (tc-l "foo" -String)
    (tc-l foo (-val 'foo))
@@ -822,8 +857,8 @@
    (tc-l #f (-val #f))
    (tc-l #"foo" -Bytes)
    [tc-l () (-val null)]
-   [tc-l (3 . 4) (-pair -Pos -Pos)]
-   [tc-l #hash((1 . 2) (3 . 4)) (make-Hashtable -Pos -Pos)])
+   [tc-l (3 . 4) (-pair -PositiveFixnum -PositiveFixnum)]
+   [tc-l #hash((1 . 2) (3 . 4)) (make-Hashtable -PositiveFixnum -PositiveFixnum)])
   ))
 
 

collects/tests/typed-scheme/xfail/for-inference.rkt

@@ -59,3 +59,23 @@
 (for/last: : (Option Integer)
            ((i : Exact-Positive-Integer '(1 2 3)))
            i)
+
+;; unlike the usual cases with #:when clauses, inference does something, but does it wrong
+(for/list: : (Listof Integer)
+           (#:when #t
+            (i : Exact-Positive-Integer '(1 2 3))
+            (j : Exact-Positive-Integer '(10 20 30)))
+           (+ i j 10))
+
+;; that same bug makes for/hash:, for/hasheq: and for/hasheqv: unusable
+;; this infers Nothing for the type of the elements of the HashTable
+;; since they don't work, these functions are not currently documented
+(for/hash: : (HashTable Integer Char)
+           ((i : Exact-Positive-Integer '(1 2 3))
+            (j : Char "abc"))
+           (values i j))
+
+;; same thing for for/and:
+(for/and: : Boolean
+          ((i : Exact-Positive-Integer '(1 2 3)))
+          (< i 3))

collects/tests/typed-scheme/xfail/xmodule-mutation.rkt

@@ -0,0 +1,19 @@
+#lang racket/load
+
+(module m typed/racket
+  (: x Any)
+  (define x "foo")
+  (: f (-> Void))
+  (define (f) (set! x 1))
+  (provide f x))
+
+(module n typed/racket
+  (require 'm)
+  (if (string? x)
+      (begin
+        (f)
+        ;; this should be a type error!
+        (string-append x "foo"))
+      0))
+
+(require 'n)

collects/typed-scheme/env/global-env.rkt

@@ -1,5 +1,8 @@
 #lang scheme/base
 
+;; Top-level type environment
+;; maps identifiers to their types, updated by mutation
+
 (require "../utils/utils.rkt" 
 	 syntax/id-table
          (utils tc-utils)

collects/typed-scheme/env/index-env.rkt

@@ -0,0 +1,31 @@
+#lang racket/base
+
+;; this implements the Theta environment from the TOPLAS paper
+
+;; this environment maps type variables names (symbols)
+;; to types representing the type variable
+;; technically, the mapped-to type is unnecessary, but it's convenient to have it around? maybe?
+
+(require racket/require racket/set (path-up "utils/tc-utils.rkt"))
+(provide (all-defined-out))
+
+;; the initial type variable environment - empty
+;; this is used in the parsing of types
+(define initial-index-env (seteq))
+
+;; a parameter for the current type variables
+(define current-indexes (make-parameter initial-index-env))
+
+;; takes a single index
+(define-syntax-rule (extend-indexes index . body)
+ (parameterize ([current-indexes (set-add (current-indexes) index)]) . body))
+
+(define (bound-index? v) (set-member? (current-indexes) v))
+
+(define (infer-index stx)
+  (define bounds (set-map (current-indexes) values))
+  (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"))
+  (car bounds))

collects/typed-scheme/env/init-envs.rkt

@@ -1,10 +1,10 @@
 #lang scheme/base
 (provide (all-defined-out))
 (require "../utils/utils.rkt"
-         "type-env.rkt" 
+         "global-env.rkt" 
 	 "type-name-env.rkt"
 	 "type-alias-env.rkt"
-         unstable/struct
+         unstable/struct racket/dict
          (rep type-rep object-rep filter-rep rep-utils)
 	 (for-template (rep type-rep object-rep filter-rep) 
 		       (types union)
@@ -25,11 +25,11 @@
     [(Union: elems) `(make-Union (sort (list ,@(map sub elems)) < #:key Type-seq))]
     [(Base: n cnt) `(make-Base ',n (quote-syntax ,cnt))]
     [(Name: stx) `(make-Name (quote-syntax ,stx))]
-    [(Struct: name parent flds proc poly? pred-id cert acc-ids maker-id)
+    [(fld: t acc mut) `(make-fld ,(sub t) (quote-syntax ,acc) ,mut)]
+    [(Struct: name parent flds proc poly? pred-id cert maker-id)
      `(make-Struct ,(sub name) ,(sub parent) 
                    ,(sub flds) ,(sub proc) ,(sub poly?)
                    (quote-syntax ,pred-id) (syntax-local-certifier)
-                   (list ,@(for/list ([a acc-ids]) `(quote-syntax ,a)))
                    (quote-syntax ,maker-id))]
     [(App: rator rands stx) `(make-App ,(sub rator) ,(sub rands) (quote-syntax ,stx))]
     [(Opaque: pred cert) `(make-Opaque (quote-syntax ,pred) (syntax-local-certifier))]
@@ -80,7 +80,7 @@
                  (show-sharing #f)
                  (booleans-as-true/false #f))                   
     (with-syntax ([registers (filter (lambda (x) x) (type-name-env-map f))])
-      #'(begin (begin-for-syntax  . registers)))))
+      #'(begin-for-syntax  . registers))))
 
 (define (talias-env-init-code)    
   (define (f id ty)
@@ -91,18 +91,20 @@
                  (show-sharing #f)
                  (booleans-as-true/false #f))                   
     (with-syntax ([registers (filter (lambda (x) x) (type-alias-env-map f))])
-      #'(begin (begin-for-syntax  . registers)))))
+      #'(begin-for-syntax  . registers))))
 
-(define (env-init-code)    
+(define (env-init-code syntax-provide? provide-tbl def-tbl)
   (define (f id ty)
-    (if (bound-in-this-module id)
+    (if (and (bound-in-this-module id)
+             ;; if there are no syntax provides, then we only need this identifier if it's provided
+             #;(or syntax-provide? (dict-ref provide-tbl id #f)))     
         #`(register-type #'#,id #,(datum->syntax #'here (print-convert ty)))
         #f))
   (parameterize ((current-print-convert-hook converter)
                  (show-sharing #f)
                  (booleans-as-true/false #f))                   
-    (with-syntax ([registers (filter (lambda (x) x) (type-env-map f))])
-      #'(begin (begin-for-syntax  . registers)))))
+    (with-syntax ([registers (filter values (type-env-map f))])
+      #'(begin-for-syntax . registers))))
 
 
 

collects/typed-scheme/env/lexical-env.rkt

@@ -1,9 +1,15 @@
 #lang scheme/base
 
+;; this environment maps *lexical* variables to types
+;; it also contains the proposition environment
+
+;; these environments are unified in "Logical Types for Scheme"
+;; but split here for performance
+
 (require "../utils/utils.rkt"
-	 "type-environments.rkt" 
-	 "type-env.rkt"
-	 unstable/mutated-vars
+	 "type-env-structs.rkt"
+         "global-env.rkt"
+	 unstable/mutated-vars syntax/id-table
          (only-in scheme/contract ->* -> or/c any/c listof cons/c)
          (utils tc-utils)
          (only-in (rep type-rep) Type/c)
@@ -13,11 +19,11 @@
 (provide lexical-env with-lexical-env with-lexical-env/extend with-update-type/lexical
          with-lexical-env/extend/props)
 (p/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?)])
+ [lookup-type/lexical ((identifier?) (prop-env? #:fail (or/c #f (-> any/c #f))) . ->* . (or/c Type/c #f))]
+ [update-type/lexical (((identifier? Type/c . -> . Type/c) identifier?) (prop-env?) . ->* . env?)])
 
 ;; the current lexical environment
-(define lexical-env (make-parameter (make-empty-env free-identifier=?)))
+(define lexical-env (make-parameter (make-empty-prop-env (make-immutable-free-id-table))))
 
 ;; run code in a new env
 (define-syntax-rule (with-lexical-env e . b)
@@ -34,14 +40,7 @@
 ;; find the type of identifier i, looking first in the lexical env, then in the top-level env
 ;; identifer -> Type
 (define (lookup-type/lexical i [env (lexical-env)] #:fail [fail #f])
-  (lookup env i 
-          (lambda (i) (lookup-type 
-                       i (lambda () 
-                           (cond [(lookup (dotted-env) i (lambda _ #f))
-                                  =>
-                                  (lambda (a)
-                                    (-lst (substitute Univ (cdr a) (car a))))]
-                                 [else ((or fail lookup-fail) i)]))))))
+  (lookup env i (λ (i) (lookup-type i (λ () ((or fail lookup-fail) i))))))
 
 ;; refine the type of i in the lexical env
 ;; (identifier type -> type) identifier -> environment

collects/typed-scheme/env/tvar-env.rkt

@@ -0,0 +1,24 @@
+#lang racket/base
+
+;; this implements the Delta environment from the TOPLAS paper 
+;; (as well as every other paper on System F)
+
+;; this environment maps type variables names (symbols)
+;; to types representing the type variable
+;; technically, the mapped-to type is unnecessary, but it's convenient to have it around? maybe?
+
+(require racket/set)
+(provide (all-defined-out))
+
+;; the initial type variable environment - empty
+;; this is used in the parsing of types
+(define initial-tvar-env (seteq))
+
+;; a parameter for the current type variables
+(define current-tvars (make-parameter initial-tvar-env))
+
+;; takes a list of vars
+(define-syntax-rule (extend-tvars vars . body)
+ (parameterize ([current-tvars (foldr (λ (v s) (set-add s v)) (current-tvars) vars)]) . body))
+
+(define (bound-tvar? v) (set-member? (current-tvars) v))

collects/typed-scheme/env/type-env-structs.rkt

@@ -0,0 +1,93 @@
+#lang scheme/base  
+
+(require scheme/contract unstable/sequence racket/dict syntax/id-table
+         (prefix-in r: "../utils/utils.rkt")
+         scheme/match (r:rep filter-rep rep-utils type-rep) unstable/struct
+         (except-in (r:utils tc-utils) make-env))
+
+(provide extend
+         env?
+         lookup
+         extend-env
+         extend/values
+         env-map
+         make-empty-env
+         env-filter
+         env-keys+vals
+         env-props
+         replace-props
+         prop-env? make-empty-prop-env)
+
+;; eq? has the type of equal?, and l is an alist (with conses!)
+;; props is a list of known propositions
+(r:d-s/c env ([l (and/c (not/c dict-mutable?) dict?)]) #:transparent)
+(r:d-s/c (prop-env env) ([props (listof Filter/c)]) #:transparent)
+
+(define (mk-env orig dict)
+  (match orig
+    [(prop-env _ p) (prop-env dict p)]
+    [_ (env dict)]))
+
+(define (env-filter f e)
+  (match e
+    [(env l)
+     (mk-env e 
+             (for/fold ([h l])
+               ([(k v) (in-dict l)]
+                #:when (not (f (cons k v))))
+               (dict-remove h k)))]))
+
+(r:d/c (make-empty-env dict)
+       (dict? . -> . env?)
+       (env dict))
+
+(r:d/c (make-empty-prop-env dict)
+       (dict? . -> . prop-env?)
+       (prop-env dict null))
+
+(r:d/c (env-props e)
+       (prop-env? . -> . (listof Filter/c))
+       (prop-env-props e))
+
+(define (env-keys+vals e)
+  (match e
+    [(env l) (for/list ([(k v) (in-dict l)]) (cons k v))]))  
+
+(r:d/c (env-map f e)
+  ((any/c any/c . -> . any/c) env? . -> . env?)
+  (mk-env e (dict-map f (env-l e))))
+
+;; extend that works on single arguments
+(define (extend e k v) 
+  (match e
+    [(env l) (mk-env e (dict-set l k v))]
+    [_ (int-err "extend: expected environment, got ~a" e)]))
+
+(define (extend-env ks vs e)
+  (match e
+    [(env l) (mk-env e (for/fold ([h l])
+                         ([k (in-list ks)] [v (in-list vs)]) (dict-set h k v)))]
+    [_ (int-err "extend-env: expected environment, got ~a" e)]))
+
+(define (replace-props e props)
+  (match e
+    [(prop-env l p)
+     (prop-env l props)]))
+
+(define (lookup e key fail)
+  (match e
+    [(env l) (dict-ref l key (λ () (fail key)))]
+    [_ (int-err "lookup: expected environment, got ~a" e)]))
+
+
+;; takes two lists of sets to be added, which are either added one at a time, if the 
+;; elements are not lists, or all at once, if the elements are lists
+(define (extend/values kss vss env)
+  (foldr (lambda (ks vs env) 
+           (cond [(and (list? ks) (list? vs))
+                  (extend-env ks vs env)]
+                 [(or (list? ks) (list? vs))
+                  (int-err "not both lists in extend/values: ~a ~a" ks vs)]
+                 [else (extend env ks vs)]))
+         env kss vss))
+