Prevent unbound identifiers from being in the base env.

Fix some bugs caught by this.

svn: r18526

collects/tests/typed-scheme/succeed/cps.ss

@@ -0,0 +1,42 @@
+#lang typed/scheme
+
+;; variables
+(define-type Var Symbol)
+(define-type UserVar Var)
+(define-struct: ContVar ([v : Var]))
+(define-type AnyVar (U UserVar ContVar))
+
+;; constructors
+(define-struct: (V A) lamV ([x : V] [b : A]))
+(define-struct: (A B) app ([rator : A] [rand : B]))
+
+(define-type (lam A) (lamV Var A))
+(define-type (lamC A) (lamV ContVar A))
+
+;; non-partitioned CPS (from Dimitrios Vardoulakis)
+(define-type Λ (Rec L (U Var (lam L) (app L L))))
+(define-type Uv (Rec Uv
+                     (U Var (lam (lam (U (app (app Uv Uv) (Rec Cv (U Var (lam (U (app (app Uv Uv) Cv)
+                                                                                 (app Cv Uv))))))
+                                         (app (Rec Cv (U Var (lam (U (app (app Uv Uv) Cv)
+                                                                     (app Cv Uv)))))
+                                              Uv)))))))
+
+(define-type Cv (Rec Cv (U Var (lam (U (app (app Uv Uv) Cv)
+                                       (app Cv Uv))))))
+(define-type Call (U (app (app Uv Uv) Cv)
+                     (app Cv Uv)))
+(define-type CPS (U Cv Uv Call))
+
+(: f (CPS -> Λ))
+(define (f x) x)
+
+;; partitioned CPS (from Sabry and Felleisen LaSC 93)
+(define-type Λ2 (Rec L (U AnyVar (lamV AnyVar L) (app L L))))
+
+(define-type K (Rec K (U ContVar (app (U Var (lamC K)) K) (lam (app K (U Var (lamC K)))))))
+(define-type P (app K (U Var (lamC K))))
+(define-type W (U Var (lamC K)))
+
+(: f* (P -> Λ2))
+(define (f* x) x)

collects/tests/typed-scheme/succeed/even-odd.ss

@@ -8,7 +8,7 @@
 (define-type OddParity (Rec Odd (U (Z Odd) (O (Rec Even (U '() (Z Even) (O Odd)))))))
 
 (: append-one (case-lambda (EvenParity -> OddParity)
-                           (OddParity -> EvenParity)
+                           (OddParity -> EvenParity)                           
                            (Bitstring -> Bitstring)))
 (define (append-one l)
   (if (null? l)
@@ -16,3 +16,8 @@
       (if (Z? l) 
           (make-Z (append-one (Z-b l)))
           (make-O (append-one (O-b l))))))
+
+(: bs-id (Bitstring -> Bitstring))
+(define (bs-id x) x)
+
+(define: z : Bitstring (bs-id (append-one null)))

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

@@ -699,6 +699,7 @@
         [tc-e (filter even? (filter exact-integer? (list 1 2 3 'foo)))
               (-lst -Integer)]
         
+        #|
         [tc-err (plambda: (a ...) [as : a ... a]
                           (apply fold-left (lambda: ([c : Integer] [a : Char] . [xs : a ... a]) c)
                                  3 (list #\c) as))]
@@ -712,7 +713,7 @@
         [tc-e/t (plambda: (a ...) [as : a ... a]
                           (apply fold-left (lambda: ([c : Integer] [a : Char] . [xs : a ... a]) c)
                                  3 (list #\c) (map list as)))
-                (-polydots (a) ((list) (a a) . ->... . -Integer))]
+                (-polydots (a) ((list) (a a) . ->... . -Integer))]|#
         
         ;; First is same as second, but with map explicitly instantiated.
         [tc-e/t (plambda: (a ...) [ys : (a ... a -> Number) *]

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

@@ -11,6 +11,7 @@
  (only-in '#%kernel [apply kernel:apply])
  scheme/promise scheme/system
  (only-in string-constants/private/only-once maybe-print-message)
+ (only-in mzscheme make-namespace)
  (only-in scheme/match/runtime match:error matchable? match-equality-test)
  (for-syntax (only-in (types abbrev) [-Number N] [-Boolean B] [-Symbol Sym])
              (only-in (rep type-rep) make-HashtableTop make-MPairTop make-BoxTop make-VectorTop)))
@@ -78,10 +79,10 @@
 [cons (-poly (a b)
              (cl->* [->* (list a (-lst a)) (-lst a)]
                     [->* (list a b) (-pair a b)]))]
-[*cons (-poly (a b) (cl->
+#;[*cons (-poly (a b) (cl->
                      [(a b) (-pair a b)]
                      [(a (-lst a)) (-lst a)]))]
-[*list? (make-pred-ty (-lst Univ))]
+#;[*list? (make-pred-ty (-lst Univ))]
 
 [null? (make-pred-ty (-val null))]
 [eof-object? (make-pred-ty (-val eof))]
@@ -142,9 +143,9 @@
 		 ((-lst b) b) . ->... .(-lst c))))]
 [for-each (-polydots (c a b) ((list ((list a) (b b) . ->... . Univ) (-lst a))
                               ((-lst b) b) . ->... . -Void))]
-[fold-left (-polydots (c a b) ((list ((list c a) (b b) . ->... . c) c (-lst a))
+#;[fold-left (-polydots (c a b) ((list ((list c a) (b b) . ->... . c) c (-lst a))
                                ((-lst b) b) . ->... . c))]
-[fold-right (-polydots (c a b) ((list ((list c a) (b b) . ->... . c) c (-lst a))
+#;[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 d)
@@ -189,8 +190,6 @@
 [printf (->* (list -String) Univ -Void)]
 [fprintf (->* (list -Output-Port -String) Univ -Void)]
 [format (->* (list -String) Univ -String)]
-[fst (-poly (a b) (-> (-pair a b) a))]
-[snd (-poly (a b) (-> (-pair a b) b))]
 
 [sleep (N . -> . -Void)]
 
@@ -364,7 +363,7 @@
 [vector-length (-poly (a) ((-vec a) . -> . -Nat))]
 [vector (-poly (a) (->* (list) a (-vec a)))]
 [vector-immutable (-poly (a) (->* (list) a (-vec a)))]
-[vector->vector-immutable (-poly (a) (-> (-vec a) (-vec a)))]
+[vector->immutable-vector (-poly (a) (-> (-vec a) (-vec a)))]
 [vector-fill! (-poly (a) (-> (-vec a) a -Void))]
 ;; [vector->values no good type here]
 

collects/typed-scheme/utils/tc-utils.ss

@@ -161,7 +161,8 @@ don't depend on any other portion of the system
   (define-syntax-class spec
     #:transparent
     #:attributes (ty id)
-    (pattern [nm:identifier ty]
+    (pattern [nm:identifier ~! ty]
+             #:fail-unless (list? (identifier-template-binding #'nm)) "not a bound identifier"
              #:with id #'#'nm)
     (pattern [e:expr ty]
              #:with id #'e))