diff --git a/collects/tests/typed-scheme/succeed/cps.ss b/collects/tests/typed-scheme/succeed/cps.ss new file mode 100644 index 0000000000..503c2129f8 --- /dev/null +++ b/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) \ No newline at end of file diff --git a/collects/tests/typed-scheme/succeed/even-odd.ss b/collects/tests/typed-scheme/succeed/even-odd.ss index 7634f7a25c..b26a054bf8 100644 --- a/collects/tests/typed-scheme/succeed/even-odd.ss +++ b/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))) diff --git a/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss b/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss index d6f0a656f6..6601529ebb 100644 --- a/collects/tests/typed-scheme/unit-tests/typecheck-tests.ss +++ b/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) *] diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss index 0e092355a0..8a120f92cd 100644 --- a/collects/typed-scheme/private/base-env.ss +++ b/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] diff --git a/collects/typed-scheme/utils/tc-utils.ss b/collects/typed-scheme/utils/tc-utils.ss index 687f11563c..2ee3352333 100644 --- a/collects/typed-scheme/utils/tc-utils.ss +++ b/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))