Skip to content

Instantly share code, notes, and snippets.

@bennn

bennn/transient-2020-03-11.diff

Last active March 11, 2020 17:21
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save bennn/e2971f65448adaa5831288d585861f43 to your computer and use it in GitHub Desktop.
Save bennn/e2971f65448adaa5831288d585861f43 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
transient-2020-03-11.diff
diff --git a/typed-racket-lib/typed-racket/base-env/base-env-indexing-abs.rkt b/typed-racket-lib/typed-racket/base-env/base-env-indexing-abs.rkt
index 366513da..68bd95de 100644
--- a/typed-racket-lib/typed-racket/base-env/base-env-indexing-abs.rkt
+++ b/typed-racket-lib/typed-racket/base-env/base-env-indexing-abs.rkt
@@ -3,12 +3,18 @@
(require
"../utils/utils.rkt"
(for-template racket/base racket/list racket/unsafe/ops racket/flonum racket/extflonum racket/fixnum)
+ (for-syntax racket/base syntax/parse)
(utils tc-utils)
(rename-in (types abbrev numeric-tower) [-Number N] [-Boolean B] [-Symbol Sym]))
(provide indexing)
-(define-syntax-rule (make-env* [i t] ...) (make-env [i (λ () t)] ...))
+(define-syntax (make-env* stx)
+ (syntax-parse stx
+ [(_ [id ty (~optional trusted-positive? #:defaults ([trusted-positive? #'#true]))] ...)
+ #'(make-env [id ty trusted-positive?] ...)]))
+
+(define needs-transient-check #false)
(define-syntax-rule (indexing index-type)
(make-env*
@@ -56,8 +62,8 @@
- [list-ref (-poly (a) ((-lst a) index-type . -> . a))]
- [list-tail (-poly (a) ((-lst a) index-type . -> . (-lst a)))]
+ [list-ref (-poly (a) ((-lst a) index-type . -> . a)) needs-transient-check]
+ [list-tail (-poly (a) ((-lst a) index-type . -> . (-lst a))) needs-transient-check]
@@ -216,11 +222,11 @@
(-poly (a) ((-lst a) index-type . -> . (-values (list (-lst a) (-lst a)))))]
[vector-ref (-poly (a) (cl->* ((-vec a) index-type . -> . a)
- (-VectorTop index-type . -> . Univ)))]
+ (-VectorTop index-type . -> . Univ))) needs-transient-check]
[unsafe-vector-ref (-poly (a) (cl->* ((-vec a) index-type . -> . a)
- (-VectorTop index-type . -> . Univ)))]
+ (-VectorTop index-type . -> . Univ))) needs-transient-check]
[unsafe-vector*-ref (-poly (a) (cl->* ((-vec a) index-type . -> . a)
- (-VectorTop index-type . -> . Univ)))]
+ (-VectorTop index-type . -> . Univ))) needs-transient-check]
[build-vector (-poly (a) (index-type (-Index . -> . a) . -> . (-mvec a)))]
[vector-set! (-poly (a) (-> (-vec a) index-type a -Void))]
[unsafe-vector-set! (-poly (a) (-> (-vec a) index-type a -Void))]
diff --git a/typed-racket-lib/typed-racket/base-env/base-env.rkt b/typed-racket-lib/typed-racket/base-env/base-env.rkt
index c0b48e33..391ae2bb 100644
--- a/typed-racket-lib/typed-racket/base-env/base-env.rkt
+++ b/typed-racket-lib/typed-racket/base-env/base-env.rkt
@@ -2,6 +2,7 @@
;; This module defines Typed Racket's main base type environment.
+(begin
(require
(for-template
(except-in racket -> ->* one-of/c class)
@@ -50,6 +51,8 @@
-StructTypeTop
make-ListDots))
+(define needs-transient-check #false))
+
;; Racket Reference
;; Section 4.1
[boolean? (make-pred-ty B)]
@@ -495,135 +498,135 @@
[car (-poly (a b)
(cl->*
(->acc (list (-pair a b)) a (list -car))
- (->* (list (-lst a)) a)))]
+ (->* (list (-lst a)) a))) needs-transient-check]
[cdr (-poly (a b)
(cl->*
(->acc (list (-pair a b)) b (list -cdr))
- (->* (list (-lst a)) (-lst a))))]
+ (->* (list (-lst a)) (-lst a)))) needs-transient-check]
;; these type signatures do not cover all valid uses of these pair accessors
[caar (-poly (a b c)
(cl->* [->acc (list (-pair (-pair a b) c)) a (list -car -car)]
[-> (-lst (-pair a b)) a]
[-> (-pair (-lst a) b) a]
- [-> (-lst (-lst a)) a]))]
+ [-> (-lst (-lst a)) a])) needs-transient-check]
[cdar (-poly (a b c)
(cl->* [->acc (list (-pair (-pair a b) c)) b (list -cdr -car)]
[-> (-lst (-pair a b)) b]
[-> (-pair (-lst a) b) (-lst a)]
- [-> (-lst (-lst a)) (-lst a)]))]
+ [-> (-lst (-lst a)) (-lst a)])) needs-transient-check]
[cadr (-poly (a b c)
(cl->* [->acc (list (-pair a (-pair b c))) b (list -car -cdr)]
- [-> (-lst a) a]))]
+ [-> (-lst a) a])) needs-transient-check]
[cddr (-poly (a b c)
(cl->* [->acc (list (-pair a (-pair b c))) c (list -cdr -cdr)]
- [-> (-lst a) (-lst a)]))]
+ [-> (-lst a) (-lst a)])) needs-transient-check]
[caaar (-poly (a b c d)
(cl->* [->acc (list (-pair (-pair (-pair a b) c) d)) a (list -car -car -car)]
- [-> (-lst (-lst (-lst a))) a]))]
+ [-> (-lst (-lst (-lst a))) a])) needs-transient-check]
[cdaar (-poly (a b c d)
(cl->* [->acc (list (-pair (-pair (-pair a b) c) d)) b (list -cdr -car -car)]
- [-> (-lst (-lst (-lst a))) (-lst a)]))]
+ [-> (-lst (-lst (-lst a))) (-lst a)])) needs-transient-check]
[cadar (-poly (a b c d)
(cl->* [->acc (list (-pair (-pair a (-pair b c)) d)) b (list -car -cdr -car)]
- [-> (-lst (-lst a)) a]))]
+ [-> (-lst (-lst a)) a])) needs-transient-check]
[cddar (-poly (a b c d)
(cl->* [->acc (list (-pair (-pair a (-pair b c)) d)) c (list -cdr -cdr -car)]
- [-> (-lst (-lst a)) (-lst a)]))]
+ [-> (-lst (-lst a)) (-lst a)])) needs-transient-check]
[caadr (-poly (a b c d)
(cl->* [->acc (list (-pair a (-pair (-pair b c) d))) b (list -car -car -cdr)]
- [-> (-lst (-lst a)) a]))]
+ [-> (-lst (-lst a)) a])) needs-transient-check]
[cdadr (-poly (a b c d)
(cl->* [->acc (list (-pair a (-pair (-pair b c) d))) c (list -cdr -car -cdr)]
- [-> (-lst (-lst a)) (-lst a)]))]
+ [-> (-lst (-lst a)) (-lst a)])) needs-transient-check]
[caddr (-poly (a b c d)
(cl->* [->acc (list (-pair a (-pair b (-pair c d)))) c (list -car -cdr -cdr)]
- [-> (-lst a) a]))]
+ [-> (-lst a) a])) needs-transient-check]
[cdddr (-poly (a b c d)
(cl->* [->acc (list (-pair a (-pair b (-pair c d)))) d (list -cdr -cdr -cdr)]
- [-> (-lst a) (-lst a)]))]
+ [-> (-lst a) (-lst a)])) needs-transient-check]
[caaaar (-poly (a b c d e)
(cl->* [->acc (list (-pair (-pair (-pair (-pair a b) c) d) e)) a (list -car -car -car -car)]
- [-> (-lst (-lst (-lst (-lst a)))) a]))]
+ [-> (-lst (-lst (-lst (-lst a)))) a])) needs-transient-check]
[cdaaar (-poly (a b c d e)
(cl->* [->acc (list (-pair (-pair (-pair (-pair a b) c) d) e)) b (list -cdr -car -car -car)]
- [-> (-lst (-lst (-lst (-lst a)))) (-lst a)]))]
+ [-> (-lst (-lst (-lst (-lst a)))) (-lst a)])) needs-transient-check]
[cadaar (-poly (a b c d e)
(cl->* [->acc (list (-pair (-pair (-pair a (-pair b c)) d) e)) b (list -car -cdr -car -car)]
- [-> (-lst (-lst (-lst a))) a]))]
+ [-> (-lst (-lst (-lst a))) a])) needs-transient-check]
[cddaar (-poly (a b c d e)
(cl->* [->acc (list (-pair (-pair (-pair b (-pair b c)) d) e)) c (list -cdr -cdr -car -car)]
- [-> (-lst (-lst (-lst a))) (-lst a)]))]
+ [-> (-lst (-lst (-lst a))) (-lst a)])) needs-transient-check]
[caadar (-poly (a b c d e)
(cl->* [->acc (list (-pair (-pair a (-pair (-pair b c) d)) e)) b (list -car -car -cdr -car)]
- [-> (-lst (-lst (-lst a))) a]))]
+ [-> (-lst (-lst (-lst a))) a])) needs-transient-check]
[cdadar (-poly (a b c d e)
(cl->* [->acc (list (-pair (-pair a (-pair (-pair b c) d)) e)) c (list -cdr -car -cdr -car)]
- [-> (-lst (-lst (-lst a))) (-lst a)]))]
+ [-> (-lst (-lst (-lst a))) (-lst a)])) needs-transient-check]
[caddar (-poly (a b c d e)
(cl->* [->acc (list (-pair (-pair a (-pair b (-pair c d))) e)) c (list -car -cdr -cdr -car)]
- [-> (-lst (-lst a)) a]))]
+ [-> (-lst (-lst a)) a])) needs-transient-check]
[cdddar (-poly (a b c d e)
(cl->* [->acc (list (-pair (-pair a (-pair b (-pair c d))) e)) d (list -cdr -cdr -cdr -car)]
- [-> (-lst (-lst a)) (-lst a)]))]
+ [-> (-lst (-lst a)) (-lst a)])) needs-transient-check]
[caaadr (-poly (a b c d e)
(cl->* [->acc (list (-pair a (-pair (-pair (-pair b c) d) e))) b (list -car -car -car -cdr)]
- [-> (-lst (-lst (-lst a))) a]))]
+ [-> (-lst (-lst (-lst a))) a])) needs-transient-check]
[cdaadr (-poly (a b c d e)
(cl->* [->acc (list (-pair a (-pair (-pair (-pair b c) d) e))) c (list -cdr -car -car -cdr)]
- [-> (-lst (-lst (-lst a))) (-lst a)]))]
+ [-> (-lst (-lst (-lst a))) (-lst a)])) needs-transient-check]
[cadadr (-poly (a b c d e)
(cl->* [->acc (list (-pair a (-pair (-pair b (-pair c d)) e))) c (list -car -cdr -car -cdr)]
- [-> (-lst (-lst a)) a]))]
+ [-> (-lst (-lst a)) a])) needs-transient-check]
[cddadr (-poly (a b c d e)
(cl->* [->acc (list (-pair a (-pair (-pair b (-pair c d)) e))) d (list -cdr -cdr -car -cdr)]
- [-> (-lst (-lst a)) (-lst a)]))]
+ [-> (-lst (-lst a)) (-lst a)])) needs-transient-check]
[caaddr (-poly (a b c d e)
(cl->* [->acc (list (-pair a (-pair b (-pair (-pair c d) e)))) c (list -car -car -cdr -cdr)]
- [-> (-lst (-lst a)) a]))]
+ [-> (-lst (-lst a)) a])) needs-transient-check]
[cdaddr (-poly (a b c d e)
(cl->* [->acc (list (-pair a (-pair b (-pair (-pair c d) e)))) d (list -cdr -car -cdr -cdr)]
- [-> (-lst (-lst a)) (-lst a)]))]
+ [-> (-lst (-lst a)) (-lst a)])) needs-transient-check]
[cadddr (-poly (a b c d e)
(cl->* [->acc (list (-pair a (-pair b (-pair c (-pair d e))))) d (list -car -cdr -cdr -cdr)]
- [-> (-lst a) a]))]
+ [-> (-lst a) a])) needs-transient-check]
[cddddr (-poly (a b c d e)
(cl->* [->acc (list (-pair a (-pair b (-pair c (-pair d e))))) e (list -cdr -cdr -cdr -cdr)]
- [-> (-lst a) (-lst a)]))]
+ [-> (-lst a) (-lst a)])) needs-transient-check]
[first (-poly (a b)
(cl->*
(->acc (list (-pair a (-lst b))) a (list -car))
- (->* (list (-lst a)) a)))]
+ (->* (list (-lst a)) a))) needs-transient-check]
[second (-poly (a r t)
(cl->* [->acc (list (-lst* a r #:tail (-lst t))) r (list -car -cdr)]
- [->* (list (-lst a)) a]))]
+ [->* (list (-lst a)) a])) needs-transient-check]
[third (-poly (a b r t)
(cl->* [->acc (list (-lst* a b r #:tail (-lst t))) r (list -car -cdr -cdr)]
- [->* (list (-lst a)) a]))]
+ [->* (list (-lst a)) a])) needs-transient-check]
[fourth (-poly (a b c r t)
(cl->* [->acc (list (-lst* a b c r #:tail (-lst t))) r (list -car -cdr -cdr -cdr)]
- [->* (list (-lst a)) a]))]
+ [->* (list (-lst a)) a])) needs-transient-check]
[fifth (-poly (a b c d r t)
(cl->* [->acc (list (-lst* a b c d r #:tail (-lst t))) r (list -car -cdr -cdr -cdr -cdr)]
- [->* (list (-lst a)) a]))]
+ [->* (list (-lst a)) a])) needs-transient-check]
[sixth (-poly (a b c d e r t)
(cl->* [->acc (list (-lst* a b c d e r #:tail (-lst t))) r (list -car -cdr -cdr -cdr -cdr -cdr)]
- [->* (list (-lst a)) a]))]
+ [->* (list (-lst a)) a])) needs-transient-check]
[seventh (-poly (a b c d e f r t)
(cl->* [->acc (list (-lst* a b c d e f r #:tail (-lst t))) r (list -car -cdr -cdr -cdr -cdr -cdr -cdr)]
- [->* (list (-lst a)) a]))]
+ [->* (list (-lst a)) a])) needs-transient-check]
[eighth (-poly (a b c d e f g r t)
(cl->* [->acc (list (-lst* a b c d e f g r #:tail (-lst t))) r (list -car -cdr -cdr -cdr -cdr -cdr -cdr -cdr)]
- [->* (list (-lst a)) a]))]
+ [->* (list (-lst a)) a])) needs-transient-check]
[ninth (-poly (a b c d e f g h r t)
(cl->* [->acc (list (-lst* a b c d e f g h r #:tail (-lst t))) r (list -car -cdr -cdr -cdr -cdr -cdr -cdr -cdr -cdr)]
- [->* (list (-lst a)) a]))]
+ [->* (list (-lst a)) a])) needs-transient-check]
[tenth (-poly (a b c d e f g h i r t)
(cl->* [->acc (list (-lst* a b c d e f g h i r #:tail (-lst t))) r (list -car -cdr -cdr -cdr -cdr -cdr -cdr -cdr -cdr -cdr)]
- [->* (list (-lst a)) a]))]
+ [->* (list (-lst a)) a])) needs-transient-check]
[rest (-poly (a b)
(cl->*
(->acc (list (-pair a (-lst b))) (-lst b) (list -cdr))
@@ -665,7 +668,7 @@
(cl->* (Univ (-lst a) . -> . (-opt (-ne-lst a)))
(b (-lst a) (-> b a Univ)
. -> . (-opt (-ne-lst a)))))]
-[findf (-poly (a) ((a . -> . B) (-lst a) . -> . (-opt a)))]
+[findf (-poly (a) ((a . -> . B) (-lst a) . -> . (-opt a))) needs-transient-check]
[assq (-poly (a b) (Univ (-lst (-pair a b)) . -> . (-opt (-pair a b))))]
[assv (-poly (a b) (Univ (-lst (-pair a b)) . -> . (-opt (-pair a b))))]
@@ -699,11 +702,11 @@
(-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 c)) d]))]
+ [((a b c d . -> . d) d (-lst a) (-lst b) (-lst c)) d])) needs-transient-check]
[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 c)) d]))]
+ [((a b c d . -> . d) d (-lst a) (-lst b) (-lst c)) d])) needs-transient-check]
[filter (-poly (a b) (cl->*
((asym-pred a Univ (-PS (-is-type 0 b) -tt))
(-lst a)
@@ -748,7 +751,7 @@
(-> (asym-pred b Univ (-PS (-is-type 0 a) -tt)) (-lst b) (-values (list (-lst a) (-lst b))))
(-> (-> a Univ) (-lst a) (-values (list (-lst a) (-lst a))))))]
-[last (-poly (a) ((-lst a) . -> . a))]
+[last (-poly (a) ((-lst a) . -> . a)) needs-transient-check]
[add-between (-poly (a b) ((-lst a) b
#:splice? -Boolean #f
#:before-first (-lst b) #f
@@ -814,8 +817,8 @@
(-> (-lst a) -Nat (-seq (-lst a)))))]
[permutations (-poly (a) (-> (-lst a) (-lst (-lst a))))]
[in-permutations (-poly (a) (-> (-lst a) (-seq (-lst a))))]
-[argmin (-poly (a) ((a . -> . -Real) (-lst a) . -> . a))]
-[argmax (-poly (a) ((a . -> . -Real) (-lst a) . -> . a))]
+[argmin (-poly (a) ((a . -> . -Real) (-lst a) . -> . a)) needs-transient-check]
+[argmax (-poly (a) ((a . -> . -Real) (-lst a) . -> . a)) needs-transient-check]
[group-by (-poly (a b) (->opt (-> a b) (-lst a) [(-> b b Univ)] (-lst (-lst a))))]
[cartesian-product (-polydots (a) (->... '() ((-lst a) a) (-lst (make-ListDots a 'a))))]
[remf (-poly (a) (-> (-> a Univ) (-lst a) (-lst a)))]
@@ -828,10 +831,10 @@
[mcons (-poly (a b) (-> a b (-mpair a b)))]
[mcar (-poly (a b)
(cl->* (-> (-mpair a b) a)
- (-> (-mlst a) a)))]
+ (-> (-mlst a) a))) needs-transient-check]
[mcdr (-poly (a b)
(cl->* (-> (-mpair a b) b)
- (-> (-mlst a) (-mlst a))))]
+ (-> (-mlst a) (-mlst a)))) needs-transient-check]
[set-mcar! (-poly (a b)
(cl->* (-> (-mpair a b) a -Void)
(-> (-mlst a) a -Void)))]
@@ -840,10 +843,10 @@
(-> (-mlst a) (-mlst a) -Void)))]
[unsafe-mcar (-poly (a b)
(cl->* (-> (-mpair a b) a)
- (-> (-mlst a) a)))]
+ (-> (-mlst a) a))) needs-transient-check]
[unsafe-mcdr (-poly (a b)
(cl->* (-> (-mpair a b) b)
- (-> (-mlst a) (-mlst a))))]
+ (-> (-mlst a) (-mlst a)))) needs-transient-check]
[unsafe-set-mcar! (-poly (a b)
(cl->* (-> (-mpair a b) a -Void)
(-> (-mlst a) a -Void)))]
@@ -868,8 +871,8 @@
[vector-immutable (-poly (a) (->* (list) a (-ivec a)))]
[vector->immutable-vector (-poly (a) (-> (-vec a) (-ivec a)))]
[vector-fill! (-poly (a) (-> (-vec a) a -Void))]
-[vector-argmax (-poly (a) (-> (-> a -Real) (-vec a) a))]
-[vector-argmin (-poly (a) (-> (-> a -Real) (-vec a) a))]
+[vector-argmax (-poly (a) (-> (-> a -Real) (-vec a) a)) needs-transient-check]
+[vector-argmin (-poly (a) (-> (-> a -Real) (-vec a) a)) needs-transient-check]
[vector-memq (-poly (a) (-> Univ (-vec a) (-opt -Index)))]
[vector-memv (-poly (a) (-> Univ (-vec a) (-opt -Index)))]
[vector-member (-poly (a) (Univ (-vec a) . -> . (-opt -Index)))]
@@ -916,16 +919,16 @@
[box-immutable (-poly (a) (a . -> . (-box a)))]
[unbox (-poly (a) (cl->*
((-box a) . -> . a)
- (-BoxTop . -> . Univ)))]
+ (-BoxTop . -> . Univ))) needs-transient-check]
[set-box! (-poly (a) ((-box a) a . -> . -Void))]
[box-cas! (-poly (a) ((-box a) a a . -> . -Boolean))]
[unsafe-unbox (-poly (a) (cl->*
((-box a) . -> . a)
- (-BoxTop . -> . Univ)))]
+ (-BoxTop . -> . Univ))) needs-transient-check]
[unsafe-set-box! (-poly (a) ((-box a) a . -> . -Void))]
[unsafe-unbox* (-poly (a) (cl->*
((-box a) . -> . a)
- (-BoxTop . -> . Univ)))]
+ (-BoxTop . -> . Univ))) needs-transient-check]
[unsafe-set-box*! (-poly (a) ((-box a) a . -> . -Void))]
[unsafe-box*-cas! (-poly (a) ((-box a) a a . -> . -Boolean))]
[box? (make-pred-ty -BoxTop)]
@@ -959,7 +962,7 @@
[((-HT a b) a (-> c)) (Un b c)]
[(-HashTableTop a) Univ]
[(-HashTableTop a (-val #f)) Univ]
- [(-HashTableTop a (-> c)) Univ]))]
+ [(-HashTableTop a (-> c)) Univ])) needs-transient-check]
[hash-ref! (-poly (a b) (-> (-HT a b) a (-> b) b))]
[hash-has-key? (-HashTableTop Univ . -> . B)]
[hash-update! (-poly (a b)
@@ -1032,9 +1035,9 @@
[unsafe-immutable-hash-iterate-next
(-poly (a b) ((-Immutable-HT a b) -Integer . -> . (Un (-val #f) -Integer)))]
[unsafe-immutable-hash-iterate-key
- (-poly (a b) ((-Immutable-HT a b) -Integer . -> . a))]
+ (-poly (a b) ((-Immutable-HT a b) -Integer . -> . a)) needs-transient-check]
[unsafe-immutable-hash-iterate-value
- (-poly (a b) ((-Immutable-HT a b) -Integer . -> . b))]
+ (-poly (a b) ((-Immutable-HT a b) -Integer . -> . b)) needs-transient-check]
[unsafe-immutable-hash-iterate-pair
(-poly (a b) ((-Immutable-HT a b) -Integer . -> . (-pair a b)))]
[unsafe-immutable-hash-iterate-key+value
@@ -1045,9 +1048,9 @@
[unsafe-mutable-hash-iterate-next
(-poly (a b) ((-Mutable-HT a b) -Integer . -> . (Un (-val #f) -Integer)))]
[unsafe-mutable-hash-iterate-key
- (-poly (a b) ((-Mutable-HT a b) -Integer . -> . a))]
+ (-poly (a b) ((-Mutable-HT a b) -Integer . -> . a)) needs-transient-check]
[unsafe-mutable-hash-iterate-value
- (-poly (a b) ((-Mutable-HT a b) -Integer . -> . b))]
+ (-poly (a b) ((-Mutable-HT a b) -Integer . -> . b)) needs-transient-check]
[unsafe-mutable-hash-iterate-pair
(-poly (a b) ((-Mutable-HT a b) -Integer . -> . (-pair a b)))]
[unsafe-mutable-hash-iterate-key+value
@@ -1058,9 +1061,9 @@
[unsafe-weak-hash-iterate-next
(-poly (a b) ((-Weak-HT a b) -Integer . -> . (Un (-val #f) -Integer)))]
[unsafe-weak-hash-iterate-key
- (-poly (a b) ((-Weak-HT a b) -Integer . -> . a))]
+ (-poly (a b) ((-Weak-HT a b) -Integer . -> . a)) needs-transient-check]
[unsafe-weak-hash-iterate-value
- (-poly (a b) ((-Weak-HT a b) -Integer . -> . b))]
+ (-poly (a b) ((-Weak-HT a b) -Integer . -> . b)) needs-transient-check]
[unsafe-weak-hash-iterate-pair
(-poly (a b) ((-Weak-HT a b) -Integer . -> . (-pair a b)))]
[unsafe-weak-hash-iterate-key+value
@@ -1103,7 +1106,7 @@
[empty-sequence (-polydots (a) (-seq-dots '() a 'a))]
[sequence->list (-poly (a) ((-seq a) . -> . (-lst a)))]
[sequence-length (-SequenceTop . -> . -Nat)]
-[sequence-ref (-polydots (a) ((-seq-dots '() a 'a) -Integer . -> . (make-ValuesDots '() a 'a)))]
+[sequence-ref (-polydots (a) ((-seq-dots '() a 'a) -Integer . -> . (make-ValuesDots '() a 'a))) needs-transient-check]
[sequence-tail (-polydots (a) ((-seq-dots '() a 'a) -Integer . -> . (-seq-dots '() a 'a)))]
[sequence-append (-polydots (a) (->* '() (-seq-dots '() a 'a) (-seq-dots '() a 'a)))]
; We can't express the full type without multiple dotted type variables:
@@ -1114,7 +1117,7 @@
[sequence-andmap (-polydots (b a) ((->... '() (a a) b) (-seq-dots '() a 'a) . -> . (Un b (-val #t))))]
[sequence-ormap (-polydots (b a) ((->... '() (a a) b) (-seq-dots '() a 'a) . -> . (Un b (-val #f))))]
[sequence-for-each (-polydots (a) ((->... '() (a a) Univ) (-seq-dots '() a 'a) . -> . -Void))]
-[sequence-fold (-polydots (b a) ((->... (list b) (a a) b) b (-seq-dots '() a 'a) . -> . b))]
+[sequence-fold (-polydots (b a) ((->... (list b) (a a) b) b (-seq-dots '() a 'a) . -> . b)) needs-transient-check]
[sequence-count (-polydots (a) ((->... '() (a a) Univ) (-seq-dots '() a 'a) . -> . -Nat))]
[sequence-filter (-polydots (a b c)
(cl->*
@@ -1133,7 +1136,7 @@
[set-empty? (-poly (e) (-> (-list-or-set e) B))]
[set-count (-poly (e) (-> (-list-or-set e) -Index))]
[set-member? (-poly (e) (-> (-list-or-set e) e B))]
-[set-first (-poly (e) (-> (-list-or-set e) e))]
+[set-first (-poly (e) (-> (-list-or-set e) e)) needs-transient-check]
[set-rest (-poly (e) (set-abs -set (-> (-set e) (-set e))))]
[set-add (-poly (e) (set-abs -set (-> (-set e) e (-set e))))]
[set-remove (-poly (e) (set-abs -set (-> (-set e) Univ (-set e))))]
@@ -1291,7 +1294,7 @@
(-polydots (b a)
(cl->*
((-> (make-ValuesDots null a 'a)) (null (a a) . ->... . b) . -> . b)
- ((-> ManyUniv) ((list) Univ . ->* . b) . -> . b)))]
+ ((-> ManyUniv) ((list) Univ . ->* . b) . -> . b))) needs-transient-check]
;; Section 10.2
[raise (cl->* ((Un -Flat -Exn) . -> . (Un))
@@ -1327,7 +1330,7 @@
;; Section 10.3 (Delayed Evaluation)
[promise? (make-pred-ty (-Promise Univ))]
-[force (-poly (a) (->acc (list (-Promise a)) a (list -force)))]
+[force (-poly (a) (->acc (list (-Promise a)) a (list -force))) needs-transient-check]
[promise-forced? (-poly (a) (-> (-Promise a) B))]
[promise-running? (-poly (a) (-> (-Promise a) B))]
@@ -1338,12 +1341,12 @@
(-> (-> b) (make-Prompt-Tagof b (-> (-> d) d)) (Un b d))
(-> (-> b) (make-Prompt-Tagof b (->... '() (c c) d)) (->... '() (c c) d)
(Un b d))
- (-> (-> b) Univ)))]
+ (-> (-> b) Univ))) needs-transient-check]
[abort-current-continuation
(-polydots (a b d e c)
(cl->*
(->... (list (make-Prompt-Tagof b (->... '() (c c) d))) (c c) e)
- (->... (list (make-Prompt-Tagof b (->... '() (c c) ManyUniv))) (c c) e)))]
+ (->... (list (make-Prompt-Tagof b (->... '() (c c) ManyUniv))) (c c) e))) needs-transient-check]
[make-continuation-prompt-tag
(-poly (a b) (->opt [Sym] (make-Prompt-Tagof a b)))]
;; default-continuation-prompt-tag is defined in "base-contracted.rkt"
@@ -1352,13 +1355,13 @@
(cl->* (-> (-> (-> (Un)) (-values null)) (-values null))
(-> (-> (->... (list a) (c c) (Un))
(make-ValuesDots (list (-result b)) c 'c))
- (make-ValuesDots (list (-result (Un a b))) c 'c))))]
+ (make-ValuesDots (list (-result (Un a b))) c 'c)))) needs-transient-check]
[call/cc
(-polydots (a b c)
(cl->* (-> (-> (-> (Un)) (-values null)) (-values null))
(-> (-> (->... (list a) (c c) (Un))
(make-ValuesDots (list (-result b)) c 'c))
- (make-ValuesDots (list (-result (Un a b))) c 'c))))]
+ (make-ValuesDots (list (-result (Un a b))) c 'c)))) needs-transient-check]
[call-with-composable-continuation
(-polydots (b c a)
(-> ;; takes a continuation and should return the same
@@ -1367,25 +1370,25 @@
(make-Prompt-Tagof b c)
;; the continuation's input is the same as the
;; return type here
- (make-ValuesDots '() a 'a)))]
+ (make-ValuesDots '() a 'a))) needs-transient-check]
[call-with-escape-continuation
(-polydots (a b c)
(cl->* (-> (-> (-> (Un)) (-values null)) (-values null))
(-> (-> (->... (list a) (c c) (Un))
(make-ValuesDots (list (-result b)) c 'c))
- (make-ValuesDots (list (-result (Un a b))) c 'c))))]
+ (make-ValuesDots (list (-result (Un a b))) c 'c)))) needs-transient-check]
[call/ec
(-polydots (a b c)
(cl->* (-> (-> (-> (Un)) (-values null)) (-values null))
(-> (-> (->... (list a) (c c) (Un))
(make-ValuesDots (list (-result b)) c 'c))
- (make-ValuesDots (list (-result (Un a b))) c 'c))))]
-[call-with-continuation-barrier (-poly (a) (-> (-> a) a))]
+ (make-ValuesDots (list (-result (Un a b))) c 'c)))) needs-transient-check]
+[call-with-continuation-barrier (-poly (a) (-> (-> a) a)) needs-transient-check]
[continuation-prompt-available? (-> -Prompt-TagTop B)]
[continuation?
(asym-pred Univ B (-PS (-is-type 0 top-func) -tt))]
[continuation-prompt-tag? (make-pred-ty -Prompt-TagTop)]
-[dynamic-wind (-poly (a) (-> (-> ManyUniv) (-> a) (-> ManyUniv) a))]
+[dynamic-wind (-poly (a) (-> (-> ManyUniv) (-> a) (-> ManyUniv) a)) needs-transient-check]
;; Section 10.5 (Continuation Marks)
;; continuation-marks needs type for continuations as other
@@ -1418,9 +1421,9 @@
(->opt (-opt -Cont-Mark-Set) (make-Continuation-Mark-Keyof a)
[b -Prompt-TagTop]
(Un a b))
- (->opt (-opt -Cont-Mark-Set) Univ [Univ -Prompt-TagTop] Univ)))]
+ (->opt (-opt -Cont-Mark-Set) Univ [Univ -Prompt-TagTop] Univ))) needs-transient-check]
[call-with-immediate-continuation-mark
- (-poly (a) (->opt Univ (-> Univ a) [Univ] a))]
+ (-poly (a) (->opt Univ (-> Univ a) [Univ] a)) needs-transient-check]
[continuation-mark-key? (make-pred-ty -Continuation-Mark-KeyTop)]
[continuation-mark-set? (make-pred-ty -Cont-Mark-Set)]
[make-continuation-mark-key
@@ -1443,7 +1446,7 @@
[thread? (make-pred-ty -Thread)]
[current-thread (-> -Thread)]
[thread/suspend-to-kill (-> (-> Univ) -Thread)]
-[call-in-nested-thread (-poly (a) (->opt (-> a) [-Custodian] a))]
+[call-in-nested-thread (-poly (a) (->opt (-> a) [-Custodian] a)) needs-transient-check]
;; Section 11.1.2
[thread-suspend (-Thread . -> . -Void)]
@@ -1464,7 +1467,7 @@
[thread-send
(-poly (a) (cl->* (-> -Thread Univ -Void)
(-> -Thread Univ (-val #f) (-opt -Void))
- (-> -Thread Univ (-> a) (Un -Void a))))]
+ (-> -Thread Univ (-> a) (Un -Void a)))) needs-transient-check]
[thread-receive (-> Univ)]
[thread-try-receive (-> Univ)]
[thread-receive-evt (-> (-mu x (-evt x)))]
@@ -1472,20 +1475,20 @@
;; Section 11.2.1
[evt? (make-pred-ty (-evt Univ))]
-[sync (-poly (a) (->* '() (-evt a) a))]
+[sync (-poly (a) (->* '() (-evt a) a)) needs-transient-check]
[sync/timeout
(-poly (a b)
(cl->*
(->* (list (-val #f)) (-evt a) a)
(->* (list -NonNegReal) (-evt a) (-opt a))
- (->* (list (-> b)) (-evt a) (Un a b))))]
-[sync/enable-break (-poly (a) (->* '() (-evt a) a))]
+ (->* (list (-> b)) (-evt a) (Un a b)))) needs-transient-check]
+[sync/enable-break (-poly (a) (->* '() (-evt a) a)) needs-transient-check]
[sync/timeout/enable-break
(-poly (a b)
(cl->*
(->* (list (-val #f)) (-evt a) a)
(->* (list -NonNegReal) (-evt a) (-opt a))
- (->* (list (-> b)) (-evt a) (Un a b))))]
+ (->* (list (-> b)) (-evt a) (Un a b)))) needs-transient-check]
[choice-evt (-poly (a) (->* '() (-evt a) (-evt a)))]
[wrap-evt (-poly (a b) (-> (-evt a) (-> a b) (-evt b)))]
[handle-evt (-poly (a b) (-> (-evt a) (-> a b) (-evt b)))]
@@ -1512,8 +1515,8 @@
;; Section 11.2.2
[make-channel (-poly (a) (-> (-channel a)))]
[channel? (make-pred-ty -ChannelTop)]
-[channel-get (-poly (a) ((-channel a) . -> . a))]
-[channel-try-get (-poly (a) ((-channel a) . -> . (Un a (-val #f))))]
+[channel-get (-poly (a) ((-channel a) . -> . a)) needs-transient-check]
+[channel-try-get (-poly (a) ((-channel a) . -> . (Un a (-val #f)))) needs-transient-check]
[channel-put (-poly (a) ((-channel a) a . -> . -Void))]
[channel-put-evt (-poly (a) (-> (-channel a) a (-mu x (-evt x))))]
[channel-put-evt? (asym-pred Univ B (-PS (-is-type 0 (-mu x (-evt x))) -tt))]
@@ -1532,18 +1535,18 @@
(cl->* (->... (list -Semaphore (->... '() [a a] b))
[a a] b)
(->... (list -Semaphore (->... '() [a a] b) (-opt (-> b)))
- [a a] b)))]
+ [a a] b))) needs-transient-check]
[call-with-semaphore/enable-break
(-polydots (b a)
(cl->* (->... (list -Semaphore (->... '() [a a] b))
[a a] b)
(->... (list -Semaphore (->... '() [a a] b) (-opt (-> b)))
- [a a] b)))]
+ [a a] b))) needs-transient-check]
;; Section 11.3.1 (Thread Cells)
[thread-cell? (make-pred-ty -ThreadCellTop)]
[make-thread-cell (-poly (a) (->opt a [Univ] (-thread-cell a)))]
-[thread-cell-ref (-poly (a) (-> (-thread-cell a) a))]
+[thread-cell-ref (-poly (a) (-> (-thread-cell a) a)) needs-transient-check]
[thread-cell-set! (-poly (a) (-> (-thread-cell a) a -Void))]
[current-preserved-thread-cell-values
(cl->* (-> Univ) (-> Univ -Void))]
@@ -1561,12 +1564,12 @@
[parameter-procedure=? (-poly (a b c d) (-> (-Param a b) (-Param c d) B))]
[current-parameterization (-> -Parameterization)]
-[call-with-parameterization (-poly (a) (-> -Parameterization (-> a) a))]
+[call-with-parameterization (-poly (a) (-> -Parameterization (-> a) a)) needs-transient-check]
[parameterization? (make-pred-ty -Parameterization)]
;; Section 11.4 (Futures)
[future (-poly (A) ((-> A) . -> . (-future A)))]
-[touch (-poly (A) ((-future A) . -> . A))]
+[touch (-poly (A) ((-future A) . -> . A)) needs-transient-check]
[futures-enabled? (-> -Boolean)]
[current-future (-> (-opt (-future Univ)))]
[future? (make-pred-ty (-future Univ))]
@@ -1905,20 +1908,20 @@
(-values (list -Input-Port -Output-Port)))]
-[call-with-input-file (-poly (a) (-Pathlike (-Input-Port . -> . a) #:mode (Un (-val 'binary) (-val 'text)) #f . ->key . a))]
+[call-with-input-file (-poly (a) (-Pathlike (-Input-Port . -> . a) #:mode (Un (-val 'binary) (-val 'text)) #f . ->key . a)) needs-transient-check]
[call-with-output-file (-poly (a) (-Pathlike (-Output-Port . -> . a)
#:exists (one-of/c 'error 'append 'update 'replace 'truncate 'truncate/replace) #f
#:mode (one-of/c 'binary 'text) #f
- . ->key . a))]
+ . ->key . a)) needs-transient-check]
-[call-with-input-file* (-poly (a) (-Pathlike (-Input-Port . -> . a) #:mode (Un (-val 'binary) (-val 'text)) #f . ->key . a))]
+[call-with-input-file* (-poly (a) (-Pathlike (-Input-Port . -> . a) #:mode (Un (-val 'binary) (-val 'text)) #f . ->key . a)) needs-transient-check]
[call-with-output-file* (-poly (a) (-Pathlike (-Output-Port . -> . a)
#:exists (one-of/c 'error 'append 'update 'replace 'truncate 'truncate/replace) #f
#:mode (one-of/c 'binary 'text) #f
- . ->key . a))]
+ . ->key . a)) needs-transient-check]
[with-input-from-file
- (-poly (a) (->key -Pathlike (-> a) #:mode (one-of/c 'binary 'text) #f a))]
+ (-poly (a) (->key -Pathlike (-> a) #:mode (one-of/c 'binary 'text) #f a)) needs-transient-check]
[with-output-to-file
(-poly (a) (->key -Pathlike (-> a)
#:exists (one-of/c 'error 'append 'update 'can-update
@@ -1926,7 +1929,7 @@
'must-truncate 'truncate/replace)
#f
#:mode (one-of/c 'binary 'text) #f
- a))]
+ a)) needs-transient-check]
|#
[port-try-file-lock? (-> (Un -Input-Port -Output-Port) (one-of/c 'shared 'exclusive) B)]
@@ -2015,14 +2018,14 @@
[call-with-input-string
(-polydots (a)
(-> -String (-> -Input-Port (make-ValuesDots '() a 'a))
- (make-ValuesDots '() a 'a)))]
+ (make-ValuesDots '() a 'a))) needs-transient-check]
[call-with-input-bytes
(-polydots (a)
(-> -Bytes (-> -Input-Port (make-ValuesDots '() a 'a))
- (make-ValuesDots '() a 'a)))]
+ (make-ValuesDots '() a 'a))) needs-transient-check]
-[with-input-from-string (-poly (a) (-> -String (-> a) a))]
-[with-input-from-bytes (-poly (a) (-> -Bytes (-> a) a))]
+[with-input-from-string (-poly (a) (-> -String (-> a) a)) needs-transient-check]
+[with-input-from-bytes (-poly (a) (-> -Bytes (-> a) a)) needs-transient-check]
;; Section 13.1.10.2
[input-port-append (->* (list Univ) -Input-Port -Input-Port)]
@@ -2554,7 +2557,7 @@
[make-custodian-box (-poly (a) (-> -Custodian a (make-CustodianBox a)))]
[custodian-box? (make-pred-ty (-poly (a) (make-CustodianBox a)))]
-[custodian-box-value (-poly (a) (-> (make-CustodianBox a) a))]
+[custodian-box-value (-poly (a) (-> (make-CustodianBox a) a)) needs-transient-check]
;; Section 14.8 (Thread Groups)
[make-thread-group (->opt [-Thread-Group] -Thread-Group)]
@@ -2764,7 +2767,7 @@
(a)
(let ([funarg* (-Path (one-of/c 'file 'dir 'link) a . -> . (-values (list a Univ)))]
[funarg (-Path (one-of/c 'file 'dir 'link) a . -> . a)])
- ((Un funarg funarg*) a [(-opt -Pathlike) Univ]. ->opt . a)))]
+ ((Un funarg funarg*) a [(-opt -Pathlike) Univ]. ->opt . a))) needs-transient-check]
[make-directory* (-> -Pathlike -Void)]
[make-parent-directory* (-> -Pathlike -Void)]
@@ -3048,13 +3051,13 @@
(->* (list (-> (make-HeterogeneousVector (list -Symbol -String Univ (-opt -Symbol))) Univ)
(-> (make-ValuesDots null a 'a)))
(-opt (one-of/c 'none 'fatal 'error 'warning 'info 'debug))
- (make-ValuesDots null a 'a)))]
+ (make-ValuesDots null a 'a))) needs-transient-check]
[with-logging-to-port
(-polydots (a)
(->* (list -Output-Port (-> (make-ValuesDots null a 'a))
(one-of/c 'none 'fatal 'error 'warning 'info 'debug))
(-opt -Symbol)
- (make-ValuesDots null a 'a)))]
+ (make-ValuesDots null a 'a))) needs-transient-check]
;; Section 15.6 (Time)
[seconds->date (cl->* (-Integer . -> . -Date)
@@ -3121,7 +3124,7 @@
[(-> -String Univ)
;; Still permits unknown-proc args that accept rest arguments
(-> -String Univ)]
- b))))]
+ b)))) needs-transient-check]
;; Section 16.1 (Weak Boxes)
[make-weak-box (-poly (a) (-> a (-weak-box a)))]
@@ -3129,13 +3132,13 @@
(-poly (a b)
(cl->* (-> (-weak-box a) (-opt a))
(-> (-weak-box a) b (Un b a))
- (->opt -Weak-BoxTop [Univ] Univ)))]
+ (->opt -Weak-BoxTop [Univ] Univ))) needs-transient-check]
[weak-box? (make-pred-ty -Weak-BoxTop)]
;; Section 16.2 (Ephemerons)
[make-ephemeron (-poly (k v) (-> k v (make-Ephemeron v)))]
[ephemeron? (make-pred-ty (make-Ephemeron Univ))]
-[ephemeron-value (-poly (v) (-> (make-Ephemeron v) (Un (-val #f) v)))]
+[ephemeron-value (-poly (v) (-> (make-Ephemeron v) (Un (-val #f) v))) needs-transient-check]
;; Section 16.3 (Wills and Executors)
[make-will-executor (-> -Will-Executor)]
@@ -3162,15 +3165,15 @@
[unsafe-car (-poly (a b)
(cl->*
(->acc (list (-pair a b)) a (list -car))
- (->* (list (-lst a)) a)))]
+ (->* (list (-lst a)) a))) needs-transient-check]
[unsafe-cdr (-poly (a b)
(cl->*
(->acc (list (-pair a b)) b (list -cdr))
- (->* (list (-lst a)) (-lst a))))]
+ (->* (list (-lst a)) (-lst a)))) needs-transient-check]
[unsafe-vector-length (-VectorTop . -> . -Index)]
[unsafe-vector*-length (-VectorTop . -> . -Index)]
-[unsafe-struct-ref top-func]
-[unsafe-struct*-ref top-func]
+[unsafe-struct-ref top-func needs-transient-check]
+[unsafe-struct*-ref top-func needs-transient-check]
[unsafe-struct-set! top-func]
[unsafe-struct*-set! top-func]
@@ -3270,7 +3273,7 @@
(->optkey -Pathlike [(-> -Input-Port (Un))] #:mode (one-of/c 'binary 'text) #f (-lst Univ))
(->optkey -Pathlike [(-> -Input-Port a)] #:mode (one-of/c 'binary 'text) #f (-lst a)))))
[call-with-atomic-output-file
- (-poly (a) (->opt -Pathlike (-> -Output-Port -Path a) [(-opt -Security-Guard)] a))]
+ (-poly (a) (->opt -Pathlike (-> -Output-Port -Path a) [(-opt -Security-Guard)] a)) needs-transient-check]
(get-preference
(let ((use-lock-type Univ)
(timeout-lock-there-type (-opt (-> -Path Univ)))
@@ -3353,7 +3356,7 @@
#:max-delay
-Real
#f
- a)))
+ a)) needs-transient-check)
(sort
(-poly
(a b)
@@ -3377,7 +3380,7 @@
(->optkey (-lst a) ((-> b b Univ))
#:key (-> a b) #f
#:default (-> c) #f
- (Un a c)))))
+ (Un a c)))) needs-transient-check)
(remove-duplicates
(-poly
(a b)
@@ -3409,7 +3412,7 @@
#f
(-values (list -Input-Port -Output-Port))))
(call-with-input-file
- (-poly (a) (->key -Pathlike (-> -Input-Port a) #:mode (Un (-val 'binary) (-val 'text)) #f a)))
+ (-poly (a) (->key -Pathlike (-> -Input-Port a) #:mode (Un (-val 'binary) (-val 'text)) #f a)) needs-transient-check)
(call-with-output-file
(-poly (a)
(->key
@@ -3421,8 +3424,8 @@
#:mode
(one-of/c 'binary 'text)
#f
- a)))
-(call-with-input-file* (-poly (a) (->key -Pathlike (-> -Input-Port a) #:mode (Un (-val 'binary) (-val 'text)) #f a)))
+ a)) needs-transient-check)
+(call-with-input-file* (-poly (a) (->key -Pathlike (-> -Input-Port a) #:mode (Un (-val 'binary) (-val 'text)) #f a)) needs-transient-check)
(call-with-output-file*
(-poly
(a)
@@ -3435,8 +3438,8 @@
#:mode
(one-of/c 'binary 'text)
#f
- a)))
-(with-input-from-file (-poly (a) (->key -Pathlike (-> a) #:mode (Un (-val 'binary) (-val 'text)) #f a)))
+ a)) needs-transient-check)
+(with-input-from-file (-poly (a) (->key -Pathlike (-> a) #:mode (Un (-val 'binary) (-val 'text)) #f a)) needs-transient-check)
(with-output-to-file
(-poly
(a)
@@ -3449,7 +3452,7 @@
#:mode
(one-of/c 'binary 'text)
#f
- a)))
+ a)) needs-transient-check)
(port->lines
(->optkey [-Input-Port]
#:line-mode (one-of/c 'linefeed 'return 'return-linefeed 'any 'any-one) #f
diff --git a/typed-racket-lib/typed-racket/base-env/env-lang.rkt b/typed-racket-lib/typed-racket/base-env/env-lang.rkt
index d357eb3c..e1a5b9f1 100644
--- a/typed-racket-lib/typed-racket/base-env/env-lang.rkt
+++ b/typed-racket-lib/typed-racket/base-env/env-lang.rkt
@@ -9,8 +9,8 @@
(define-syntax (-#%module-begin stx)
(define-syntax-class clause
- #:description "[id type]"
- (pattern [id:identifier ty]))
+ #:description "[id type ?trust]"
+ (pattern [id:identifier ty (~optional trusted-cod? #:defaults ([trusted-cod? #'#true]))]))
(syntax-parse stx #:literals (require begin)
[(mb (~optional (~and extra (~or (begin . _) (require . args))))
~! :clause ...)
@@ -18,7 +18,7 @@
(begin
extra
(define e
- (make-env [id (λ () ty)] ...))
+ (make-env [id (λ () ty) trusted-cod?] ...))
(define (init)
(initialize-type-env e))
(provide init)))]
diff --git a/typed-racket-lib/typed-racket/base-env/prims-contract.rkt b/typed-racket-lib/typed-racket/base-env/prims-contract.rkt
index 4df335ef..e041a6d7 100644
--- a/typed-racket-lib/typed-racket/base-env/prims-contract.rkt
+++ b/typed-racket-lib/typed-racket/base-env/prims-contract.rkt
@@ -291,7 +291,7 @@
(if types
#`(U #,@types)
#f)))
- `#s(contract-def ,type-stx ,flat? ,maker? typed))))
+ `#s(contract-def ,type-stx ,flat? ,maker? ,(current-type-enforcement-mode)))))
(define (define-predicate stx)
diff --git a/typed-racket-lib/typed-racket/core.rkt b/typed-racket-lib/typed-racket/core.rkt
index 598b6fb6..33825177 100644
--- a/typed-racket-lib/typed-racket/core.rkt
+++ b/typed-racket-lib/typed-racket/core.rkt
@@ -3,7 +3,7 @@
(require (rename-in "utils/utils.rkt")
(for-syntax racket/base)
(for-template racket/base)
- (private with-types type-contract)
+ (private with-types type-contract syntax-properties)
(except-in syntax/parse id)
racket/match racket/syntax
syntax/flatten-begin
@@ -23,16 +23,30 @@
(~or (~and #:optimize (~bind [opt? #'#t])); kept for backward compatibility
(~and #:no-optimize (~bind [opt? #'#f]))))
(~optional
- (~and #:with-refinements refinement-reasoning?)))
+ (~and #:with-refinements refinement-reasoning?))
+ (~optional
+ (~or (~and #:guarded (~bind [te-strat #'guarded]))
+ (~and #:transient (~bind [te-strat #'transient]))
+ (~and #:erasure (~bind [te-strat #'erasure])))))
...
forms ...)
(let ([pmb-form (syntax/loc stx (#%plain-module-begin forms ...))])
(parameterize ([optimize? (or (and (not (attribute opt?)) (optimize?))
(and (attribute opt?) (syntax-e (attribute opt?))))]
[with-refinements? (or (attribute refinement-reasoning?)
- (with-refinements?))])
+ (with-refinements?))]
+ [current-type-enforcement-mode (if (attribute te-strat) (syntax-e #'te-strat) 'guarded)])
(tc-module/full stx pmb-form
(λ (new-mod pre-before-code pre-after-code)
+ (define ctc-cache (make-hash))
+ (define sc-cache (make-hash))
+ (define (change-contract-fixups/cache forms)
+ (change-contract-fixups forms ctc-cache sc-cache))
+ (define (change-provide-fixups/cache forms)
+ (change-provide-fixups forms ctc-cache sc-cache))
+ (define (defend/cache forms)
+ ;;bg; TODO cannot re-use other caches because `define`s will be out of order
+ (maybe-defend forms (make-hash) (make-hash)))
(with-syntax*
(;; pmb = #%plain-module-begin
[(pmb . body2) new-mod]
@@ -40,14 +54,17 @@
[transformed-body (begin0 (remove-provides #'body2) (do-time "Removed provides"))]
;; add the real definitions of contracts on requires
[transformed-body
- (begin0 (change-contract-fixups (syntax->list #'transformed-body))
- (do-time "Fixed contract ids"))]
+ (begin0
+ (change-contract-fixups/cache (syntax->list #'transformed-body))
+ (do-time "Fixed contract ids"))]
;; add the real definitions of contracts on the before- and after-code
- [(before-code ...) (change-provide-fixups (flatten-all-begins pre-before-code))]
- [(after-code ...) (begin0 (change-provide-fixups (flatten-all-begins pre-after-code))
+ [(before-code ...) (change-provide-fixups/cache (flatten-all-begins pre-before-code))]
+ [(after-code ...) (begin0
+ (change-provide-fixups/cache (flatten-all-begins pre-after-code))
(do-time "Generated contracts"))]
+ [((before-defend-code ...) . defended-body) (defend/cache #'transformed-body)]
;; potentially optimize the code based on the type information
- [(optimized-body ...) (maybe-optimize #'transformed-body)] ;; has own call to do-time
+ [(optimized-body ...) (maybe-optimize #'defended-body)]
;; add in syntax property on useless expression to draw check-syntax arrows
[check-syntax-help (syntax-property
(syntax-property
@@ -58,9 +75,10 @@
;; use the regular %#module-begin from `racket/base' for top-level printing
(arm #`(#%module-begin
#,(if (unbox include-extra-requires?) extra-requires #'(begin))
- before-code ... optimized-body ... after-code ... check-syntax-help)))))))]))
+ before-code ... before-defend-code ... optimized-body ... after-code ... check-syntax-help)))))))]))
(define (ti-core stx )
+ (current-type-enforcement-mode guarded)
(current-type-names (init-current-type-names))
(syntax-parse stx
#:literal-sets (kernel-literals)
diff --git a/typed-racket-lib/typed-racket/defender/defender.rkt b/typed-racket-lib/typed-racket/defender/defender.rkt
new file mode 100644
index 00000000..fbc03aac
--- /dev/null
+++ b/typed-racket-lib/typed-racket/defender/defender.rkt
@@ -0,0 +1,663 @@
+#lang racket/base
+
+;; TODO
+;; - [ ] build + test occurrence-type optimizer
+;; - [ ] build/test erasure-racket
+;;
+;; TODO
+;; - [ ] need with-new-name-tables here?
+;; - [ ] syntax-track-origin ? syntax/loc/track-origin ?
+
+(require
+ (only-in racket/format ~a)
+ racket/match
+ syntax/id-set
+ syntax/parse
+ typed-racket/rep/type-rep
+ typed-racket/rep/values-rep
+ typed-racket/static-contracts/utils
+ typed-racket/types/match-expanders
+ (only-in typed-racket/optimizer/unboxed-let
+ escapes?)
+ (only-in typed-racket/env/transient-env
+ transient-trusted-positive?)
+ (only-in typed-racket/typecheck/internal-forms
+ typed-struct
+ typed-struct/exec)
+ (only-in typed-racket/types/base-abbrev
+ make-CyclicListof
+ make-Listof)
+ (only-in typed-racket/types/abbrev
+ -Void
+ -String
+ -Symbol
+ -True
+ -False
+ ->
+ -values)
+ typed-racket/types/struct-table
+ typed-racket/types/type-table
+ typed-racket/types/union
+ typed-racket/types/utils
+ (only-in typed-racket/private/syntax-properties
+ type-ascription-property
+ type-inst-property
+ ignore^
+ ignore-some^
+ opt-lambda^
+ kw-lambda^)
+ (only-in racket/syntax
+ format-id
+ generate-temporary)
+ (only-in (submod typed-racket/private/type-contract test-exports)
+ type->contract)
+ (for-syntax
+ racket/base)
+ (for-template
+ racket
+ racket/unsafe/ops
+ typed-racket/types/numeric-predicates))
+
+(provide defend-top)
+
+(module+ test
+ (require rackunit))
+
+;; =============================================================================
+
+(define (defend-top stx ctc-cache sc-cache extra-defs*)
+ (let loop ([stx stx] [skip-dom? #f])
+ (syntax-parse stx
+ #:literals (values define-values #%plain-app begin define-syntaxes letrec-values)
+ [_
+ #:when (is-ignored? stx) ;; lookup in type-table's "ignored table"
+ stx]
+ [(~or _:ignore^ _:ignore-some^) ;; for struct definitions ... not sure what else
+ stx]
+ [((~or (~literal #%provide)
+ (~literal #%require)
+ (~literal begin-for-syntax)
+ (~literal define-syntaxes)
+ (~literal module)
+ (~literal module*)) . _)
+ ;; ignore the same things the optimizer ignores
+ stx]
+ [(~and _:kw-lambda^ ((~literal let-values) ([(f) fun]) body))
+ stx
+ #;(syntax/loc stx (let-values ([(f) fun]) body))]
+ [(~and _:opt-lambda^ ((~literal let-values) ([(f) fun]) body))
+ stx
+ #;(syntax/loc stx (let-values ([(f) fun]) body))]
+ [(op:lambda-identifier formals . body)
+ (define dom-map (type->domain-map (stx->arrow-type stx)))
+ (define body+ (loop #'body #f))
+ (void (readd-props! body+ #'body))
+ (define formals+
+ (if skip-dom? '() (protect-formals dom-map #'formals ctc-cache sc-cache extra-defs*)))
+ (define stx+
+ (with-syntax ([body+ body+])
+ (if (null? formals+)
+ (syntax/loc stx (op formals . body+))
+ (let ((stx (quasisyntax/loc stx (op formals (#%plain-app void . #,formals+) . body+))))
+ (register-ignored! (caddr (syntax-e stx)))
+ stx))))
+ (void (readd-props! stx+ stx))
+ stx+]
+ [(#%plain-app (letrec-values (((a:id) e0)) b:id) e1* ...)
+ #:when (free-identifier=? #'a #'b)
+ ;; (for ....) combinators expand to a recursive function that does not escape,
+ ;; no need to check the domain --- use (loop e #true) to skip
+ ;; TODO can the optimizer remove these checks instead?
+ (define skip? (not (escapes? #'a #'e0 #false)))
+ (with-syntax ((e0+ (loop #'e0 skip?))
+ ((e1*+ ...) (for/list ((e1 (in-list (syntax-e #'(e1* ...)))))
+ (loop e1 #f))))
+ (syntax/loc stx
+ (#%plain-app (letrec-values (((a) e0+)) b) e1*+ ...)))]
+ [(x* ...)
+ #:when (is-application? stx)
+ (define stx+
+ (syntax*->syntax stx
+ (for/list ([x (in-list (syntax-e #'(x* ...)))])
+ (define x+ (loop x #f))
+ (readd-props! x+ x)
+ x+)))
+ (void
+ (readd-props! stx+ stx))
+ (define-values [pre* f post*] (split-application stx+))
+ (if (or (is-ignored? f)
+ (blessed-codomain? f)
+ (cdr-list? f post*))
+ stx+
+ (let ()
+ (define cod-tc-res (maybe-type-of stx))
+ (define stx/dom
+ (with-syntax ([(pre ...) pre*]
+ [f f]
+ [post* post*])
+ (syntax/loc stx+ (pre ... f . post*))))
+ (add-typeof-expr stx/dom (ret Univ)) ;; TODO we can do better!
+ (define stx/cod
+ (protect-codomain cod-tc-res stx/dom ctc-cache sc-cache extra-defs*))
+ (readd-props! stx/cod stx)
+ stx/cod))]
+ [((~and x (~literal #%expression)) _)
+ #:when (type-inst-property #'x)
+ stx]
+ [((~literal #%expression) e)
+ #:when (type-ascription-property stx)
+ (define e+ (loop #'e #f))
+ (void (readd-props! e+ #'e))
+ (define e++
+ (with-syntax ([e+ e+])
+ (syntax/loc stx (#%expression e+))))
+ (void (readd-props! e++ stx))
+ e++]
+ [_
+ #:when (type-ascription-property stx)
+ (raise-user-error 'defend-top "strange type-ascription ~a" (syntax->datum stx))]
+ [(x* ...)
+ (define stx+
+ (syntax*->syntax stx
+ (for/list ((x (in-list (syntax-e #'(x* ...)))))
+ (define x+ (loop x #f))
+ (readd-props! x+ x)
+ x+)))
+ (readd-props! stx+ stx)
+ stx+]
+ [_
+ stx])))
+
+(define-syntax-class lambda-identifier
+ (pattern (~literal #%plain-lambda))
+ (pattern (~literal lambda)))
+
+(define (readd-props! new-stx old-stx)
+ (maybe-add-typeof-expr new-stx old-stx)
+ (maybe-add-test-position new-stx old-stx)
+ (void))
+
+(define (maybe-add-typeof-expr new-stx old-stx)
+ (let ((old-type (maybe-type-of old-stx)))
+ (when old-type
+ (add-typeof-expr new-stx old-type))))
+
+(define (maybe-add-test-position new-stx old-stx)
+ (maybe-add-test-true new-stx old-stx)
+ (maybe-add-test-false new-stx old-stx)
+ (void))
+
+(define (maybe-add-test-true new-stx old-stx)
+ (when (test-position-takes-true-branch old-stx)
+ (test-position-add-true new-stx))
+ (void))
+
+(define (maybe-add-test-false new-stx old-stx)
+ (when (test-position-takes-false-branch old-stx)
+ (test-position-add-false new-stx))
+ (void))
+
+;; -----------------------------------------------------------------------------
+
+;; is-application? : Syntax -> Boolean
+;; Returns #true if `stx` is a function application (an app that may need dynamic checking)
+(define (is-application? stx)
+ (syntax-parse stx
+ [((~literal #%plain-app) . _)
+ (has-type-annotation? stx)]
+ [_
+ #false]))
+
+;; split-application : Syntax -> (Values (Syntaxof List) Syntax (Syntaxof List))
+(define (split-application stx)
+ (syntax-parse stx
+ #:literals (#%plain-app)
+ #:datum-literals (apply)
+ [((~and a #%plain-app) (~and b apply) f . arg*)
+ (values #'(a b) #'f #'arg*)]
+ [((~and a #%plain-app) f . arg*)
+ (values #'(a) #'f #'arg*)]
+ [_
+ (raise-argument-error 'split-application "(Syntaxof App)" stx)]))
+
+(define (stx->arrow-type stx [num-args #f])
+ (define raw-type (tc-results->type1 (maybe-type-of stx)))
+ (let loop ([ty (and raw-type (normalize-type raw-type))])
+ (match ty
+ [(Fun: (list (? Arrow?)))
+ ty]
+ [(Param: in out)
+ (cond
+ [(not num-args)
+ (raise-arguments-error 'stx->arrow-type "cannot coerce parameter to arrow type, number of arguments is unknown" "type" ty "stx" stx)]
+ [(= 0 num-args)
+ (-> out)]
+ [(= 1 num-args)
+ (-> in -Void)]
+ [else
+ (raise-arguments-error 'stx->arrow-type "wrong number of arguments supplied to parameter" "type" ty "stx" stx "num-args" num-args)])]
+ [(Poly: _ b)
+ (loop b)]
+ [(Fun: arrs)
+ ;;bg; if case->, try combining the arrs to a union type
+ ;; this is possible when each `arr` has the same arity
+ (define arr (combine-arrs arrs))
+ (if arr
+ (loop (make-Fun (list arr)))
+ (raise-arguments-error 'stx->arrow-type "failed to parse arrow from case->"
+ "type" ty
+ "e" (syntax->datum stx)
+ "stx" stx
+ "cases" arrs))]
+ [(Union: _ ts)
+ ;; TODO okay to pick arbitrary?
+ ;; example type: (U (-> (Array Integer) (values (Indexes : (Top | Bot) : (struct-ref (0 0) 0)) (Index : (Top | Bot) : (struct-ref (0 0) 1)) (Index : (Top | Bot) : (vector-length (struct-ref (0 0) 0))) (Indexes : (Top | Bot)) ((-> Indexes Integer) : (Top | Bot) : (struct-ref (0 0) 4)))) (All (A) (-> (Array A) (values (Indexes : (Top | Bot) : (Array-shape (0 0))) (Index : (Top | Bot) : (Array-size (0 0))) (Index : (Top | Bot) : (vector-length (Array-shape (0 0)))) (Indexes : (Top | Bot)) ((-> Indexes A) : (Top | Bot) : (Array-unsafe-proc (0 0)))))))
+ (loop (car ts))]
+ [_
+ (raise-arguments-error 'stx->arrow-type "failed to parse arrow from type of syntax object"
+ "e" (syntax->datum stx)
+ "stx" stx
+ "type" ty)])))
+
+;; combine-arrs : (-> (Listof Arrow) (U #f Arrow))
+
+(module+ test
+ (check-equal? ;;bg; not happy about ~a ....
+ (~a (combine-arrs (list
+ (make-Arrow (list -Symbol -True (make-Listof -Symbol) Univ) #f '() (-values (list -String)))
+ (make-Arrow (list -False -False (make-Listof -Symbol) Univ) #f '() (-values (list -String)))
+ (make-Arrow (list -Symbol Univ (make-Listof -Symbol) -True) #f '() (-values (list -String)))
+ (make-Arrow (list -Symbol Univ -False -False) #f '() (-values (list -String))))))
+ (~a (make-Arrow (list (Un -Symbol -False)
+ (Un -True -False Univ)
+ (Un (make-Listof -Symbol) -False)
+ (Un Univ -True -False))
+ #f '() (-values (list -String)))))
+)
+
+(define (combine-arrs arrs)
+ (match arrs
+ [(list (Arrow: t** #f '() rng*) ...)
+ #:when (same-length? t**)
+ (define m+ (combine-dom* t**))
+ (define rng+ (combine-rng* rng*))
+ (make-Arrow m+ #f '() rng+)]
+ [_
+ #f]))
+
+(define (same-length? x**)
+ (or (null? x**)
+ (null? (cdr x**))
+ (and (= (length (car x**)) (length (cadr x**)))
+ (same-length? (cdr x**)))))
+
+(define (combine-dom* t**)
+ (if (andmap null? t**)
+ '()
+ (cons (apply Un (map car t**)) (combine-dom* (map cdr t**)))))
+
+(define (combine-rng* rng*)
+ (define t** (map some-values->type* rng*))
+ (and (same-length? t**)
+ (let ([t* (combine-dom* t**)])
+ (make-Values t*))))
+
+(define (tc-results->type* r)
+ (match r
+ [(tc-results: (list (tc-result: ts _ _) ...) #f)
+ ts]
+ [_
+ #f]))
+
+(define (tc-results->type1 r)
+ (match r
+ [(tc-result1: t)
+ t]
+ [_
+ #f]))
+
+(define REST-KEY 'rest)
+
+;; type->domain-map : Type -> TypeMap
+;; where TypeMap = (HashTable (U Fixnum 'rest Keyword) (U #f Type))
+;; Build a TypeMap from the domain of an arrow type.
+(define (type->domain-map t)
+ (match t
+ [(or (Fun: (list (Arrow: mand rst kws _)))
+ (Arrow: mand rst kws _))
+ (let* ([t# (make-immutable-hash)]
+ [t# ;; positional arguments
+ (for/fold ([acc t#])
+ ([d (in-list mand)]
+ [i (in-naturals)])
+ (hash-set acc i d))]
+ [t# ;; rest args
+ (cond
+ [(Type? rst)
+ (hash-set t# REST-KEY (make-Listof rst))]
+ [(Rest? rst)
+ (hash-set t# REST-KEY
+ (let ([tys (Rest-tys rst)])
+ (if (and (not (null? tys)) (null? (cdr tys)))
+ (make-Listof (car tys))
+ (raise-arguments-error 'type->domain-map "cannot handle rest type yet" "rest" tys "orig type" t))))]
+ [(RestDots? rst)
+ (raise-arguments-error 'type->domain-map "type without rest-dots"
+ "type" t)]
+ [else
+ t#])]
+ [t# ;; kwd args
+ (for/fold ([acc t#])
+ ([k (in-list kws)])
+ (match k
+ [(Keyword: kw ty _)
+ (hash-set acc kw ty)]
+ [_
+ (raise-arguments-error 'type->domain-map "arrow type (with good keywords)" "type" t)]))])
+ t#)]
+ [_
+ (raise-argument-error 'type->domain-map "arrow type" t)]))
+
+(define (type-map-ref map key)
+ (define (fail-thunk)
+ (raise-arguments-error 'type-map-ref "unbound key" "key" key "map" map))
+ (cond
+ [(fixnum? key)
+ (hash-ref map key (λ () (hash-ref map REST-KEY fail-thunk)))]
+ [(keyword? key)
+ (hash-ref map key fail-thunk)]
+ [(eq? REST-KEY key)
+ (hash-ref map key fail-thunk)]
+ [else
+ (raise-argument-error 'type-map-ref "(or/c fixnum? 'rest keyword?)" 1 map key)]))
+
+;;; type->codomain-type : Type Syntax -> (U #f SomeValues)
+;;; Get the codomain from an arrow type,
+;;; use `stx` to decide whether we can skip the codomain check.
+;;; 2020-03 : unused!
+;(define (type->codomain-type t stx)
+; (match t
+; [(Fun: (list (Arrow: _ _ _ cod)))
+; (if (blessed-codomain? stx)
+; #f
+; cod)]
+; [_
+; (raise-argument-error 'type->cod-type "arrow type" t)]))
+
+(define (blessed-codomain? stx)
+ (if (identifier? stx)
+ (or (syntax-property stx 'constructor-for) ;; 2020-03: could register in env/lexical-env instead
+ ;; 2020-03 : struct predicates handled earlier in type checker
+ (transient-trusted-positive? stx)
+ (and (typed-racket-identifier? stx)
+ (not (struct-accessor? stx))
+ (not (from-require/typed? stx))))
+ (is-lambda? stx)))
+
+(define (cdr-list? f post*)
+ ;; TODO put this in optimizer?
+ ;; TODO bless cddr ..., but check for N-level pair type too
+ (and
+ (identifier? f)
+ (or (free-identifier=? f #'cdr)
+ (free-identifier=? f #'unsafe-cdr))
+ (let* ((e (syntax-e post*))
+ (t (and (pair? e) (tc-results->type1 (maybe-type-of (car e))))))
+ (match t
+ [(or (Listof: _)
+ (Pair: _ (Listof: _))
+ (Pair: _ (Pair: _ _)))
+ #true]
+ [_
+ #false]))))
+
+;; from-require/typed? : Identifier -> Boolean
+;; Typed Racket adds this property to all require/typed identifiers,
+;; see `utils/require-contract.rkt`
+(define (from-require/typed? stx)
+ (syntax-property stx 'not-provide-all-defined))
+
+(define (typed-racket-identifier? stx)
+ (define ib (identifier-binding stx))
+ (and (pair? ib)
+ (or (identifier-binding-from-this-module? ib)
+ (identifier-binding-from-typed-racket-module? ib))))
+
+(define (identifier-binding-from-this-module? ib)
+ (match ib
+ [(list src-mpi _src-id nom-src-mpi nom-src-id 0 0 0)
+ (and (equal? src-mpi (module-path-index-join #f #f))
+ (equal? src-mpi nom-src-mpi))]
+ [_
+ #false]))
+
+(define (identifier-binding-from-typed-racket-module? ib)
+ (match ib
+ [(list src-mpi _src-id _nom-src-mpi _nom-src-id 0 0 0)
+ (typed-racket-mpi? src-mpi)]
+ [_
+ #false]))
+
+(define typed-racket-mpi?
+ (let ([cache (make-hash)])
+ (λ (mpi)
+ (hash-ref! cache mpi
+ (λ () ;; Typed Racket always installs a `#%type-decl` submodule
+ (let* ([mpi+ (module-path-index-join '(submod "." #%type-decl) mpi)])
+ (parameterize ([current-namespace (make-base-namespace)])
+ (with-handlers ([exn:fail:contract? (lambda (exn) #f)])
+ (and mpi+
+ (dynamic-require mpi+ #f)
+ #t)))))))))
+
+(define (protect-domain dom-type dom-stx ctc-cache sc-cache extra-defs*)
+ (define ctc-stx
+ (and dom-type (type->flat-contract dom-type ctc-cache sc-cache extra-defs*)))
+ (cond
+ [(not ctc-stx)
+ #f]
+ [else
+ (define err-msg
+ (parameterize ([error-print-width 20])
+ (format "~e : ~a" (#%plain-app syntax->datum dom-stx) dom-type)))
+ ;; TODO register ignored
+ (with-syntax ([ctc ctc-stx]
+ [err err-msg]
+ [dom dom-stx])
+ (define new-stx
+ (syntax/loc dom-stx
+ (if (#%plain-app ctc dom)
+ '#true
+ (#%plain-app error 'transient-assert (#%plain-app format #;'"die" '"got ~s in ~a" dom 'err)))))
+ (register-ignored! new-stx)
+ new-stx)]))
+
+;; protect-codomain : (U #f Tc-Results) (Syntaxof List) Hash Hash (Boxof Syntax) -> (Syntaxof List)
+(define (protect-codomain cod-tc-res app-stx ctc-cache sc-cache extra-defs*)
+ (define t* (tc-results->type* cod-tc-res))
+ (cond
+ [(or (not cod-tc-res) (not t*))
+ app-stx]
+ [(null? t*)
+ #;(raise-argument-error 'protect-codomain "non-empty tc-results" cod-tc-res)
+ app-stx]
+ [else
+ (define ctc-stx* ;; (Listof (U #f Syntax))
+ (for/list ([t (in-list t*)])
+ (type->flat-contract t ctc-cache sc-cache extra-defs*)))
+ (define err-msg
+ (parameterize ([error-print-width 20])
+ (format "~e : ~a" (#%plain-app syntax->datum app-stx) t*)))
+ (if (not (ormap values ctc-stx*))
+ ;; Nothing to check
+ app-stx
+ ;; Assemble everything into a syntax object that:
+ ;; - performs the application
+ ;; - binds the result(s) to temporary variable(s)
+ ;; - checks the tag of each temporary
+ (with-syntax ([app app-stx]
+ [err err-msg])
+ (define var-name 'dyn-cod)
+ (if (null? (cdr t*))
+ ;; -- application returns 1 result, just bind it and check it
+ (with-syntax ([(ctc) ctc-stx*]
+ [v (generate-temporary var-name)])
+ (define new-stx
+ (with-type
+ cod-tc-res
+ (syntax/loc app-stx
+ (let-values ([(v) app])
+ (if (#%plain-app ctc v)
+ v
+ (#%plain-app error 'transient-assert (#%plain-app format #;'"die" '"got ~s in ~a" v 'err)))))))
+ (define if-stx (caddr (syntax-e new-stx)))
+ (register-ignored! if-stx)
+ (define chk-stx (syntax-e (cadr (syntax-e if-stx))))
+ (register-ignored! chk-stx)
+ (test-position-add-true chk-stx)
+ (test-position-add-false chk-stx)
+ (register-ignored! (caddr (syntax-e if-stx)))
+ (register-ignored! (cadddr (syntax-e if-stx)))
+ new-stx)
+ ;; - application returns +1 results:
+ ;; - bind all,
+ ;; - check the ones with matching contracts,
+ ;; - return all
+ (with-syntax ([v* (for/list ([_t (in-list t*)])
+ ;; should be OK to do this instead of `generate-temporaries`, right?
+ (generate-temporary var-name))])
+ (define new-stx
+ (with-type
+ cod-tc-res
+ (quasisyntax/loc app-stx
+ (let-values ([v* app])
+ (if #,(make-and-stx
+ app-stx
+ (for/list ([ctc-stx (in-list ctc-stx*)]
+ [v (in-list (syntax-e #'v*))]
+ #:when ctc-stx)
+ (register-ignored! ctc-stx)
+ (test-position-add-true ctc-stx)
+ (test-position-add-false ctc-stx)
+ (quasisyntax/loc app-stx (#%plain-app #,ctc-stx #,v))))
+ (#%plain-app values . v*)
+ (#%plain-app error 'transient-assert 'err))))))
+ (register-ignored! (caddr (syntax-e new-stx)))
+ new-stx))))]))
+
+(define (make-and-stx loc stx*)
+ ;; TODO awkward, remove?
+ (for/fold ((acc (syntax/loc loc '#true)))
+ ((stx (in-list stx*)))
+ (quasisyntax/loc loc (if #,stx #,acc '#false))))
+
+(define-syntax-rule (with-type t e)
+ (let ((v e))
+ (add-typeof-expr v t)
+ v))
+
+;; protect-formals : TypeMap (Syntaxof List) Hash Hash (Boxof Syntax) -> (Syntaxof List)
+(define (protect-formals dom-map formals ctc-cache sc-cache extra-defs*)
+ (filter values
+ (let loop ([dom* formals] [position 0])
+ ;; wow this is off the hook ... sometimes called with (a b (c . d))
+ (cond
+ [(null? dom*)
+ '()]
+ [(not (pair? dom*))
+ (cond
+ [(identifier? dom*)
+ (define t (type-map-ref dom-map REST-KEY))
+ (list (protect-domain t (datum->syntax formals dom*) ctc-cache sc-cache extra-defs*))]
+ [(syntax? dom*)
+ (loop (syntax-e dom*) position)]
+ [else
+ (raise-arguments-error 'protect-formals "strange domain element in formals"
+ "elem" dom*
+ "formals" formals)])]
+ [(keyword? (syntax-e (car dom*)))
+ (raise-arguments-error 'protect-formals "unexpected keyword in domain"
+ "elem" (car dom*)
+ "formals" formals)]
+ [else
+ (define var (formal->var (car dom*)))
+ (define t (type-map-ref dom-map position))
+ (cons (protect-domain t var ctc-cache sc-cache extra-defs*)
+ (loop (cdr dom*) (+ position 1)))]))))
+
+(define (formal->var stx)
+ (syntax-parse stx
+ [_:id
+ stx]
+ [(x:id _)
+ (syntax/loc stx x)]))
+
+;; some-values->type* : (U Type SomeValues) -> (Listof Type)
+(define (some-values->type* sv)
+ (match sv
+ [(? Type?)
+ (list sv)]
+ [(Values: r*)
+ (map Result-t r*)]
+ [(AnyValues: _)
+ (raise-user-error 'some-values->type* "cannot generate contract for AnyValues type '~a'" sv)]
+ [(ValuesDots: _ _ _)
+ (raise-user-error 'some-values->type* "cannot generate contract for ValuesDots type '~a'" sv)]))
+
+(define (is-lambda? x)
+ (syntax-parse x
+ [((~or (~literal lambda) (~literal #%plain-lambda)) . _) #true]
+ [_ #false]))
+
+(define (has-type-annotation? x)
+ (match (maybe-type-of x)
+ [(tc-results: _ #f)
+ ;; #f = don't handle rest dots
+ #true]
+ [a
+ #false]))
+
+#;(define (needs-domain-check? t)
+ ;; TODO recursion is similar to `function-type?` in `type-contract.rkt`
+ (match t
+ [(Fun: arrs)
+ (ormap arr/non-empty-domain? arrs)]
+ [(Union: _ elems)
+ (ormap needs-domain-check? elems)]
+ [(Intersection: elems _)
+ (andmap needs-domain-check? elems)]
+ [(Poly: _ body)
+ (needs-domain-check? body)]
+ [(PolyDots: _ body)
+ (needs-domain-check? body)]
+ [_ #f]))
+
+(define (arr/non-empty-domain? arr)
+ (match arr
+ [(Arrow: '() #f '() _)
+ #false]
+ [(Arrow: _ _ _ _)
+ #true]
+ [_
+ (raise-argument-error 'arr/non-empty-domain "Arrow?" arr)]))
+
+(define (syntax*->syntax ctx stx*)
+ (datum->syntax ctx
+ (if (null? stx*)
+ '()
+ (cons (car stx*) (syntax*->syntax ctx (cdr stx*))))))
+
+(define (type->flat-contract t ctc-cache sc-cache extra-defs*)
+ (define (fail #:reason r)
+ (raise-user-error 'type->flat-contract "failed to convert type ~a to flat contract because ~a" t r))
+ (match-define (list defs ctc)
+ (type->contract t fail
+ #:typed-side #f
+ #:cache ctc-cache
+ #:sc-cache sc-cache))
+ (for-each register-ignored! defs)
+ (set-box! extra-defs* (append (reverse defs) (unbox extra-defs*)))
+ (if (or (free-identifier=? ctc #'any/c)
+ (free-identifier=? ctc #'none/c))
+ #f
+ ctc))
diff --git a/typed-racket-lib/typed-racket/env/global-env.rkt b/typed-racket-lib/typed-racket/env/global-env.rkt
index 87f271c6..abe0786a 100644
--- a/typed-racket-lib/typed-racket/env/global-env.rkt
+++ b/typed-racket-lib/typed-racket/env/global-env.rkt
@@ -19,7 +19,8 @@
unregister-type
check-all-registered-types
type-env-map
- type-env-for-each)
+ type-env-for-each
+ unhygienic-lookup-type)
;; free-id-table from id -> type or Box[type]
;; where id is a variable, and type is the type of the variable
@@ -51,7 +52,7 @@
(define t* (if (box? t) (unbox t) t))
(unless (equal? type t*)
(tc-error/delayed #:stx id "Duplicate type annotation of ~a for ~a, previous was ~a" type (syntax-e id) t*)))]
- [else (free-id-table-set! the-mapping id (box type))]))
+ [else (register-type id (box type))]))
;; add a bunch of types to the mapping
;; listof[id] listof[type] -> void
@@ -63,7 +64,26 @@
;; identifier -> type
(define (lookup-type id [fail-handler (λ () (lookup-fail id))])
(define v (free-id-table-ref the-mapping id fail-handler))
- (cond [(box? v) (unbox v)]
+ (post-lookup-type id v))
+
+(define (unhygienic-lookup-type id [fail-handler (λ () (lookup-fail id))])
+ (define v
+ (or
+ (for/first (((kk vv) (in-free-id-table the-mapping))
+ #:when (unhygienic-eq? id kk))
+ vv)
+ (and (procedure? fail-handler) (fail-handler))
+ fail-handler))
+ (post-lookup-type id v))
+
+(define (unhygienic-eq? id0 id1)
+ (and (eq? (syntax->datum id0) (syntax->datum id1))
+ (equal? (syntax-source id0) (syntax-source id1))
+ (equal? (syntax-line id0) (syntax-line id1))
+ (equal? (syntax-column id0) (syntax-column id1))))
+
+(define (post-lookup-type id v)
+ (cond [(box? v) (unbox v)]
[(procedure? v) (define t (v)) (register-type id t) t]
[else v]))
@@ -106,3 +126,4 @@
(define (type-env-for-each f)
(sorted-free-id-table-map the-mapping f))
+
diff --git a/typed-racket-lib/typed-racket/env/init-envs.rkt b/typed-racket-lib/typed-racket/env/init-envs.rkt
index ad84e816..b71d4590 100644
--- a/typed-racket-lib/typed-racket/env/init-envs.rkt
+++ b/typed-racket-lib/typed-racket/env/init-envs.rkt
@@ -5,6 +5,7 @@
(require "../utils/utils.rkt"
(utils tc-utils)
"global-env.rkt"
+ "transient-env.rkt"
"type-name-env.rkt"
"type-alias-env.rkt"
"mvar-env.rkt"
@@ -27,13 +28,14 @@
initialize-type-env
type->sexp ; for types/printer.rkt
object->sexp ; for testing
- make-env-init-codes)
+ make-env-init-codes
+ make-register-type-code)
(define-syntax (define-initial-env stx)
(syntax-parse stx
- [(_ initialize-env [id-expr ty] ...)
+ [(_ initialize-env [id-expr ty (~optional trusted-positive? #:defaults ([trusted-positive? #'#t]))] ...)
#`(begin
- (define initial-env (make-env [id-expr (λ () ty)] ... ))
+ (define initial-env (make-env [id-expr (λ () ty) trusted-positive?] ... ))
(define (initialize-env) (initialize-type-env initial-env))
(provide initialize-env))]))
@@ -41,7 +43,12 @@
(for-each (lambda (nm/ty) (register-resolved-type-alias (car nm/ty) (cadr nm/ty))) initial-type-names))
(define (initialize-type-env initial-env)
- (for-each (lambda (nm/ty) (register-type-if-undefined (car nm/ty) (cadr nm/ty))) initial-env))
+ (define (init nm/ty/sh)
+ (define id (car nm/ty/sh))
+ (when (caddr nm/ty/sh)
+ (register-transient-trusted-positive! id))
+ (register-type-if-undefined id (cadr nm/ty/sh)))
+ (for-each init initial-env))
;; stores definition syntaxes for lifting out common expressions
(define type-definitions (make-queue))
@@ -442,7 +449,13 @@
(define (tname-env-init-code)
(make-init-code
type-name-env-map
- (λ (id ty) #`(register-type-name #'#,id #,(quote-type ty)))))
+ make-register-type-name-code))
+
+(define (make-register-type-code id ty)
+ #`(register-type #'#,id #,(quote-type ty)))
+
+(define (make-register-type-name-code id ty)
+ #`(register-type-name #'#,id #,(quote-type ty)))
(define (tvariance-env-init-code)
(make-init-code
@@ -457,7 +470,7 @@
(define (env-init-code)
(make-init-code
type-env-map
- (λ (id ty) #`(register-type #'#,id #,(quote-type ty)))))
+ make-register-type-code))
(define (mvar-env-init-code mvar-env)
(make-init-code
diff --git a/typed-racket-lib/typed-racket/env/lexical-env.rkt b/typed-racket-lib/typed-racket/env/lexical-env.rkt
index eb12f4f3..27f3f9e9 100644
--- a/typed-racket-lib/typed-racket/env/lexical-env.rkt
+++ b/typed-racket-lib/typed-racket/env/lexical-env.rkt
@@ -70,7 +70,8 @@
(define (lookup-id-type/lexical i [env (lexical-env)] #:fail [fail #f])
(env-lookup-id
env i
- (λ (i) (lookup-type i (λ ()
+ (λ (i)
+ (lookup-type i (λ ()
(cond
[(syntax-property i 'constructor-for)
=> (λ (prop)
@@ -95,6 +96,10 @@
Err))
(register-type i t)
t)]
+ [(unhygienic-lookup-type i #f)
+ ;; TODO i should be a T-redirected identifier
+ ;; used in S code. Make this hygienic.
+ => values]
[else ((or fail lookup-fail) i)]))))))
(define (lookup-obj-type/lexical obj [env (lexical-env)] #:fail [fail #f])
diff --git a/typed-racket-lib/typed-racket/env/transient-env.rkt b/typed-racket-lib/typed-racket/env/transient-env.rkt
new file mode 100644
index 00000000..dea51dd3
--- /dev/null
+++ b/typed-racket-lib/typed-racket/env/transient-env.rkt
@@ -0,0 +1,30 @@
+#lang racket/base
+
+;; Global base environment, describes the output behavior of built-ins.
+;;
+;; In Transient, a function call (f x) usually needs to be guarded with a
+;; codomain shape-check ... so its rewritten to (check t? (f x))
+;; Some base functions do not need a codomain check; for example, the call
+;; (list 42) is sure to make a list, so (check list? (list 42)) is overkill.
+;; This environment contains all such functions.
+
+(provide
+ transient-trusted-positive?
+ ;; (-> identifier? boolean?)
+ ;; True if outputs from this identifier do not require a shape check
+
+ register-transient-trusted-positive!)
+
+(require
+ syntax/id-set)
+
+;; -----------------------------------------------------------------------------
+
+(define the-transient-map (mutable-free-id-set))
+
+(define (transient-trusted-positive? id)
+ (free-id-set-member? the-transient-map id))
+
+(define (register-transient-trusted-positive! id)
+ (free-id-set-add! the-transient-map id))
+
diff --git a/typed-racket-lib/typed-racket/optimizer/dead-code.rkt b/typed-racket-lib/typed-racket/optimizer/dead-code.rkt
index 57fdd3f7..29c6faf1 100644
--- a/typed-racket-lib/typed-racket/optimizer/dead-code.rkt
+++ b/typed-racket-lib/typed-racket/optimizer/dead-code.rkt
@@ -4,6 +4,7 @@
racket/syntax
(for-template racket/base)
"../utils/utils.rkt"
+ (only-in "../utils/tc-utils.rkt" current-type-enforcement-mode guarded)
(types type-table)
(optimizer utils logging))
@@ -40,9 +41,11 @@
(quasisyntax/loc/origin this-syntax #'kw
(if tst-opt thn-opt els-opt))]))
(pattern ((~and kw lambda) formals . bodies)
+ #:when (eq? guarded (current-type-enforcement-mode))
#:when (dead-lambda-branch? #'formals)
#:with opt this-syntax)
(pattern ((~and kw case-lambda) (formals . bodies) ...)
+ #:when (eq? guarded (current-type-enforcement-mode))
#:when (for/or ((formals (in-syntax #'(formals ...))))
(dead-lambda-branch? formals))
#:with opt
diff --git a/typed-racket-lib/typed-racket/optimizer/optimizer.rkt b/typed-racket-lib/typed-racket/optimizer/optimizer.rkt
index a9074eb5..37857d18 100644
--- a/typed-racket-lib/typed-racket/optimizer/optimizer.rkt
+++ b/typed-racket-lib/typed-racket/optimizer/optimizer.rkt
@@ -2,6 +2,7 @@
(require syntax/parse racket/pretty
"../utils/utils.rkt"
+ (only-in "../utils/tc-utils.rkt" erasure current-type-enforcement-mode)
(private syntax-properties)
(types type-table)
(optimizer utils
@@ -29,6 +30,10 @@
([(i:id) e-rhs:opt-expr]) e-body:expr ...))
#:with opt (quasisyntax/loc/origin this-syntax #'op
(op ([(i) e-rhs.opt]) e-body ...)))
+ (pattern (~and ((~or #%provide #%require begin-for-syntax define-syntaxes module module*)
+ . _)
+ opt))
+ (pattern (~and (~or (quote _) (quote-syntax . _) (#%top . _) :id) opt))
;; interesting cases, where something is optimized
(pattern :dead-code-opt-expr)
@@ -63,15 +68,14 @@
#%variable-reference with-continuation-mark))
e:opt-expr ...)
#:with opt (quasisyntax/loc/origin this-syntax #'kw
- (kw e.opt ...)))
- (pattern (~and ((~or #%provide #%require begin-for-syntax define-syntaxes module module*)
- . _)
- opt))
- (pattern (~and (~or (quote _) (quote-syntax . _) (#%top . _) :id) opt)))
+ (kw e.opt ...))))
(define (optimize-top stx)
+ (when (eq? erasure (current-type-enforcement-mode))
+ (raise-arguments-error 'optimize-top "cannot optimize in #:erasure mode" "stx" stx "(current-type-enforcement-mode)" (current-type-enforcement-mode)))
(parameterize ([optimize (syntax-parser [e:opt-expr* #'e.opt])])
(let ((result ((optimize) stx)))
(when *show-optimized-code*
(pretty-print (syntax->datum result)))
- result)))
+ result))
+ )
diff --git a/typed-racket-lib/typed-racket/optimizer/pair.rkt b/typed-racket-lib/typed-racket/optimizer/pair.rkt
index 09fb59bd..c3c9779a 100644
--- a/typed-racket-lib/typed-racket/optimizer/pair.rkt
+++ b/typed-racket-lib/typed-racket/optimizer/pair.rkt
@@ -5,8 +5,9 @@
(for-template racket/base racket/unsafe/ops racket/list)
(for-syntax racket/base syntax/parse racket/syntax)
"../utils/utils.rkt"
+ (only-in "../utils/tc-utils.rkt" current-type-enforcement-mode)
(rep type-rep)
- (types type-table utils base-abbrev resolve subtype)
+ (types type-table utils base-abbrev resolve subtype match-expanders)
(typecheck typechecker)
(optimizer utils logging))
@@ -133,8 +134,7 @@
;; optimize alt inside-out, as long as it's safe to
(let-values
([(t res)
- (for/fold ([t (match (type-of #'e.arg)
- [(tc-result1: t) t])]
+ (for/fold ([t (type-of%current-mode #'e.arg)]
[res #'e.arg])
([accessor (in-list (reverse (syntax->list #'e.alt)))])
(cond
@@ -156,3 +156,23 @@
(values t ; stays unsafe from now on
#`(#,accessor #,res))]))])
res)))
+
+;; Get the type from `stx` but flatten based on the type soundness guarantee for
+;; the current mode
+;; 2020-03-06 only works for pair types
+(define (type-of%current-mode stx)
+ (define orig-t (match (type-of stx) [(tc-result1: t) t]))
+ (case (current-type-enforcement-mode)
+ ((guarded)
+ orig-t)
+ ((transient)
+ (match orig-t
+ [(Listof: _)
+ (-lst Univ)]
+ [(Pair: _ _)
+ (-pair Univ Univ)]
+ [_
+ Univ]))
+ (else
+ (raise-arguments-error 'type-of%current-mode "cannot optimize in #:erasure mode"))))
+
diff --git a/typed-racket-lib/typed-racket/optimizer/unboxed-let.rkt b/typed-racket-lib/typed-racket/optimizer/unboxed-let.rkt
index 64bd5472..bacefd05 100644
--- a/typed-racket-lib/typed-racket/optimizer/unboxed-let.rkt
+++ b/typed-racket-lib/typed-racket/optimizer/unboxed-let.rkt
@@ -10,7 +10,7 @@
(rep type-rep) (env mvar-env)
(optimizer utils logging float-complex unboxed-tables))
-(provide unboxed-let-opt-expr)
+(provide unboxed-let-opt-expr escapes?)
;; possibly replace bindings of complex numbers by bindings of their 2
;; components useful for intermediate results used more than once and for
diff --git a/typed-racket-lib/typed-racket/optimizer/utils.rkt b/typed-racket-lib/typed-racket/optimizer/utils.rkt
index bc1e32fd..37ee07bb 100644
--- a/typed-racket-lib/typed-racket/optimizer/utils.rkt
+++ b/typed-racket-lib/typed-racket/optimizer/utils.rkt
@@ -156,3 +156,4 @@
#:with (sub-exprs ...) #'(e)]
[pattern (set! _ e:expr)
#:with (sub-exprs ...) #'(e)])
+
diff --git a/typed-racket-lib/typed-racket/private/type-annotation.rkt b/typed-racket-lib/typed-racket/private/type-annotation.rkt
index de06a0b3..087e53b4 100644
--- a/typed-racket-lib/typed-racket/private/type-annotation.rkt
+++ b/typed-racket-lib/typed-racket/private/type-annotation.rkt
@@ -29,7 +29,7 @@
(when (and (identifier? stx)
let-binding)
(define t1 (parse-type/id stx prop))
- (define t2 (lookup-type stx (lambda () #f)))
+ (define t2 (lookup-type stx (lambda () #f)))
(when (and t2 (not (equal? t1 t2)))
(maybe-finish-register-type stx)
(tc-error/delayed #:stx stx "Duplicate type annotation of ~a for ~a, previous was ~a" t1 (syntax-e stx) t2)))
diff --git a/typed-racket-lib/typed-racket/private/type-contract.rkt b/typed-racket-lib/typed-racket/private/type-contract.rkt
index 24692071..e00417e2 100644
--- a/typed-racket-lib/typed-racket/private/type-contract.rkt
+++ b/typed-racket-lib/typed-racket/private/type-contract.rkt
@@ -17,8 +17,8 @@
racket/format
racket/string
syntax/flatten-begin
- (only-in (types abbrev) -Bottom -Boolean)
- (static-contracts instantiate structures combinators constraints)
+ (only-in (types abbrev) -Bottom -Boolean VectorTop:)
+ (static-contracts instantiate structures combinators constraints utils) ;;bg
(only-in (submod typed-racket/static-contracts/instantiate internals) compute-constraints)
;; TODO make this from contract-req
(prefix-in c: racket/contract)
@@ -50,6 +50,10 @@
#t)]
[_ #f]))
+;; type : (syntaxof Type?)
+;; flat? : boolean?
+;; maker? : boolean?
+;; typed-side : (or/c 'untyped type-enforcement-mode)
(struct contract-def (type flat? maker? typed-side) #:prefab)
;; get-contract-def-property : Syntax -> (U False Contract-Def)
@@ -84,6 +88,8 @@
(define (generate-contract-def stx cache sc-cache)
(define prop (get-contract-def-property stx))
(match-define (contract-def type-stx flat? maker? typed-side) prop)
+ (when (and (type-enforcement-mode? typed-side) (not (eq? typed-side (current-type-enforcement-mode))))
+ (raise-arguments-error 'generate-contract-def "current TE mode does not match contract def side" "typed-side" typed-side "(current-type-enforcement-mode)" (current-type-enforcement-mode)))
(define *typ (if type-stx (parse-type type-stx) t:-Dead-Code))
(define kind (if (and type-stx flat?) 'flat 'impersonator))
(syntax-parse stx #:literals (define-values)
@@ -102,7 +108,7 @@
typ
;; this value is from the typed side (require/typed, make-predicate, etc)
;; unless it's used for with-type
- #:typed-side (from-typed? typed-side)
+ #:typed-side (from-typed? (case typed-side ((typed guarded transient erasure) 'typed) ((untyped) 'untyped) (else (error 'die-typed-side))))
#:kind kind
#:cache cache
#:sc-cache sc-cache
@@ -193,11 +199,9 @@
;; This box is only used for contracts generated for `require/typed`
;; and `cast`, contracts for `provides go into the `#%contract-defs`
;; submodule, which always has the above `require`s.
-(define include-extra-requires? (box #f))
+(define include-extra-requires? (box #t)) ;;bg; always true for now TODO
-(define (change-contract-fixups forms)
- (define ctc-cache (make-hash))
- (define sc-cache (make-hash))
+(define (change-contract-fixups forms [ctc-cache (make-hash)] [sc-cache (make-hash)])
(with-new-name-tables
(for/list ((e (in-list forms)))
(if (not (has-contract-def-property? e))
@@ -267,37 +271,41 @@
(define (from-typed? side)
(case side
[(typed both) #t]
- [(untyped) #f]))
+ [(untyped) #f]
+ [else (raise-argument-error 'from-typed? "side?" side)]))
(define (from-untyped? side)
(case side
[(untyped both) #t]
- [(typed) #f]))
+ [(typed) #f]
+ [else (raise-argument-error 'from-untyped? "side?" side)]))
(define (flip-side side)
(case side
[(typed) 'untyped]
[(untyped) 'typed]
- [(both) 'both]))
+ [(both) 'both]
+ [else (raise-argument-error 'flip-side "side?" side)]))
;; type->contract : Type Procedure
;; #:typed-side Boolean #:kind Symbol #:cache Hash
;; -> (U Any (List (Listof Syntax) Syntax))
(define (type->contract ty init-fail
#:typed-side [typed-side #t]
- #:kind [kind 'impersonator]
+ #:kind [pre-kind 'impersonator]
#:cache [cache (make-hash)]
#:sc-cache [sc-cache (make-hash)])
(let/ec escape
(define (fail #:reason [reason #f]) (escape (init-fail #:reason reason)))
- (instantiate/optimize
- (type->static-contract ty #:typed-side typed-side fail
- #:cache sc-cache)
- fail
- kind
- #:cache cache
- #:trusted-positive typed-side
- #:trusted-negative (not typed-side))))
+ (define sc
+ (type->static-contract ty fail
+ #:typed-side typed-side
+ #:cache sc-cache))
+ (define kind (if (eq? guarded (current-type-enforcement-mode)) pre-kind 'flat))
+ (instantiate/optimize sc fail kind
+ #:cache cache
+ #:trusted-positive typed-side
+ #:trusted-negative (not typed-side))))
(define any-wrap/sc (chaperone/sc #'any-wrap/c))
@@ -309,7 +317,8 @@
(case side
((untyped) (triple-untyped trip))
((typed) (triple-typed trip))
- ((both) (triple-both trip))))
+ ((both) (triple-both trip))
+ (else (raise-argument-error 'triple-lookup "side?" 1 trip side))))
(define (same sc)
(triple sc sc sc))
@@ -339,6 +348,19 @@
(define (type->static-contract type init-fail
#:typed-side [typed-side #t]
#:cache [sc-cache (make-hash)])
+ (case (current-type-enforcement-mode)
+ [(guarded)
+ (type->static-contract/guarded type init-fail #:typed-side typed-side #:cache sc-cache)]
+ [(transient)
+ (type->static-contract/transient type init-fail #:typed-side typed-side #:cache sc-cache)]
+ [(erasure)
+ any/sc]
+ [else
+ (raise-arguments-error 'type->static-contract "invalid type-enforcement strategy" "(current-type-enforcement-mode)" (current-type-enforcement-mode))]))
+
+(define (type->static-contract/guarded type init-fail
+ #:typed-side [typed-side #t]
+ #:cache [sc-cache (make-hash)])
(let/ec return
(define (fail #:reason reason) (return (init-fail #:reason reason)))
(let loop ([type type] [typed-side (if typed-side 'typed 'untyped)] [recursive-values (hash)])
@@ -350,6 +372,7 @@
(loop t 'both recursive-values))
(define (t->sc/fun t) (t->sc/function t fail typed-side recursive-values loop #f))
(define (t->sc/meth t) (t->sc/method t fail typed-side recursive-values loop))
+
(define (prop->sc p)
(match p
[(TypeProp: o (app t->sc tc))
@@ -370,20 +393,6 @@
(and-prop/sc (map prop->sc ps))]
[(OrProp: ps)
(or-prop/sc (map prop->sc ps))]))
-
- (define (obj->sc o)
- (match o
- [(Path: pes (? identifier? x))
- (for/fold ([obj (id/sc x)])
- ([pe (in-list (reverse pes))])
- (match pe
- [(CarPE:) (acc-obj/sc #'car obj)]
- [(CdrPE:) (acc-obj/sc #'cdr obj)]
- [(VecLenPE:) (acc-obj/sc #'vector-length obj)]))]
- [(LExp: const terms)
- (linear-exp/sc const
- (for/hash ([(obj coeff) (in-terms terms)])
- (values (obj->sc obj) coeff)))]))
(define (only-untyped sc)
(if (from-typed? typed-side)
(and/sc sc any-wrap/sc)
@@ -425,20 +434,22 @@
(lookup-name-sc type typed-side)])]
;; Ordinary type applications or struct type names, just resolve
[(or (App: _ _) (Name/struct:)) (t->sc (resolve-once type))]
- [(Univ:) (if (from-typed? typed-side) any-wrap/sc any/sc)]
+ [(Univ:) (only-untyped any/sc)]
[(Bottom:) (or/sc)]
[(Listof: elem-ty) (listof/sc (t->sc elem-ty))]
;; This comes before Base-ctc to use the Value-style logic
;; for the singleton base types (e.g. -Null, 1, etc)
[(Val-able: v)
- (if (and (c:flat-contract? v)
- ;; numbers used as contracts compare with =, but TR
- ;; requires an equal? check
- (not (number? v))
- ;; regexps don't match themselves when used as contracts
- (not (regexp? v)))
- (flat/sc #`(quote #,v))
- (flat/sc #`(flat-named-contract '#,v (lambda (x) (equal? x '#,v))) v))]
+ ;; bg this is for performance tuning
+ (cond
+ [(eof-object? v)
+ (flat/sc #'eof-object?)]
+ [(void? v)
+ (flat/sc #'void?)]
+ [(or (symbol? v) (boolean? v) (keyword? v) (null? v))
+ (flat/sc #`(λ (x) (eq? '#,v x)))]
+ [else #;(or (number? v) (regexp? v) (string? v) (bytes? v) (char? v))
+ (flat/sc #`(λ (x) (equal? '#,v x)))])]
[(Base-name/contract: sym ctc) (flat/sc ctc)]
[(Distinction: _ _ t) ; from define-new-subtype
(t->sc t)]
@@ -529,20 +540,30 @@
[(Mutable-VectorTop:)
(only-untyped mutable-vector?/sc)]
[(Box: t) (box/sc (t->sc/both t))]
- [(Pair: t1 t2)
- (cons/sc (t->sc t1) (t->sc t2))]
+ [(Pair: _ _)
+ (match type
+ [(List: elem-t*)
+ (apply list/sc (map t->sc elem-t*))]
+ [(List: elem-t* #:tail rest-t*)
+ (for/fold ((acc (t->sc rest-t*)))
+ ((t (in-list (reverse elem-t*))))
+ (cons/sc (t->sc t) acc))]
+ [_
+ (error 'type->static-contract "Pair-type match failed for type ~a" type)])]
[(Async-Channel: t) (async-channel/sc (t->sc t))]
[(Promise: t)
(promise/sc (t->sc t))]
[(Opaque: p?)
- (flat/sc #`(flat-named-contract (quote #,(syntax-e p?)) #,p?))]
+ ;; bg performance
+ (flat/sc p?)]
[(Continuation-Mark-Keyof: t)
(continuation-mark-key/sc (t->sc t))]
;; TODO: this is not quite right for case->
[(Prompt-Tagof: s (Fun: (list (Arrow: ts _ _ _))))
(prompt-tag/sc (map t->sc ts) (t->sc s))]
- [(F: v) #:when (string-prefix? (symbol->string v) "self-")
- (fail #:reason "contract generation not supported for Self")]
+ [(F: v)
+ #:when (string-prefix? (symbol->string v) "self-")
+ (fail #:reason "contract generation not supported for Self")]
;; TODO
[(F: v)
(triple-lookup
@@ -550,11 +571,13 @@
(λ () (error 'type->static-contract
"Recursive value lookup failed. ~a ~a" recursive-values v)))
typed-side)]
+ [(VectorTop:) (only-untyped vector?/sc)]
[(BoxTop:) (only-untyped box?/sc)]
[(ChannelTop:) (only-untyped channel?/sc)]
[(Async-ChannelTop:) (only-untyped async-channel?/sc)]
[(MPairTop:) (only-untyped mpair?/sc)]
[(ThreadCellTop:) (only-untyped thread-cell?/sc)]
+ [(ThreadCell: _) (fail #:reason "contract generation not supported for this type")]
[(Prompt-TagTop:) (only-untyped prompt-tag?/sc)]
[(Continuation-Mark-KeyTop:) (only-untyped continuation-mark-key?/sc)]
[(ClassTop:) (only-untyped class?/sc)]
@@ -594,7 +617,8 @@
(recursive-sc
n*s
(list untyped typed both)
- (recursive-sc-use (if (from-typed? typed-side) typed-n* untyped-n*)))])]
+ (recursive-sc-use (if (from-typed? typed-side) typed-n* untyped-n*)))]
+ [else (raise-argument-error 'Mu-case "side?" typed-side)])]
;; Don't directly use the class static contract generated for Name,
;; because that will get an #:opaque class contract. This will do the
;; wrong thing for object types since it errors too eagerly.
@@ -612,7 +636,7 @@
[(Instance: (Class: _ _ fields methods _ _))
(match-define (list (list field-names field-types) ...) fields)
(match-define (list (list public-names public-types) ...) methods)
- (object/sc (from-typed? typed-side)
+ (object/sc (from-typed? typed-side) ;; TODO 2020-02-10 probably need to keep side info
(append (map (λ (n sc) (member-spec 'method n sc))
public-names (map t->sc/meth public-types))
(map (λ (n sc) (member-spec 'field n sc))
@@ -744,6 +768,310 @@
[_
(fail #:reason "contract generation not supported for this type")]))))
+(define (type->static-contract/transient type init-fail
+ #:typed-side [_typed-side #t]
+ #:cache [sc-cache (make-hash)])
+ ;; TODO delete fail? let/ec?
+ (define typed-side 'both)
+ (let/ec return
+ (define (fail #:reason reason) (return (init-fail #:reason reason)))
+ (let loop ([type type] [recursive-values (hash)])
+ (define (t->sc t #:recursive-values (recursive-values recursive-values))
+ (loop t recursive-values))
+ (define (prop->sc p)
+ ;;bg copied from above, but uses different t->sc
+ (match p
+ [(TypeProp: o (app t->sc tc))
+ (cond
+ [(not (equal? flat-sym (get-max-contract-kind tc)))
+ (fail #:reason "proposition contract generation not supported for non-flat types")]
+ [else (is-flat-type/sc (obj->sc o) tc)])]
+ [(NotTypeProp: o (app t->sc tc))
+ (cond
+ [(not (equal? flat-sym (get-max-contract-kind tc)))
+ (fail #:reason "proposition contract generation not supported for non-flat types")]
+ [else (not-flat-type/sc (obj->sc o) tc)])]
+ [(LeqProp: (app obj->sc lhs) (app obj->sc rhs))
+ (leq/sc lhs rhs)]
+ [(AndProp: ps)
+ (and-prop/sc (map prop->sc ps))]
+ [(OrProp: ps)
+ (or-prop/sc (map prop->sc ps))]))
+ (cached-match
+ sc-cache type typed-side
+ ;; Applications of implicit recursive type aliases
+ ;;
+ ;; We special case this rather than just resorting to standard
+ ;; App resolution (see case below) because the resolution process
+ ;; will make type->static-contract infinite loop.
+ [(App: (Name: name _ #f) _)
+ ;; Key with (cons name 'app) instead of just name because the
+ ;; application of the Name is not necessarily the same as the
+ ;; Name type alone
+ (cond [(hash-ref recursive-values (cons name 'app) #f)]
+ [else
+ (define name* (generate-temporary name))
+ (recursive-sc (list name*)
+ (list
+ (t->sc (resolve-once type)
+ #:recursive-values
+ (hash-set recursive-values
+ (cons name 'app)
+ (recursive-sc-use name*))))
+ (recursive-sc-use name*))])]
+ ;; Implicit recursive aliases
+ [(Name: name-id args #f)
+ (cond [;; recursive references are looked up in a special table
+ ;; that's handled differently by sc instantiation
+ (lookup-name-sc type typed-side)]
+ [else
+ (define rv recursive-values)
+ (define resolved-name (resolve-once type))
+ (define resolved-sc (t->sc resolved-name #:recursive-values rv))
+ (register-name-sc type
+ (λ () resolved-sc)
+ (λ () resolved-sc)
+ (λ () resolved-sc))
+ (lookup-name-sc type typed-side)])]
+ ;; Ordinary type applications or struct type names, just resolve
+ [(or (App: _ _) (Name/struct:)) (t->sc (resolve-once type))]
+ [(Univ:) any/sc]
+ [(Bottom:) (or/sc)]
+ [(Listof: _) list?/sc]
+ ;; This comes before Base-ctc to use the Value-style logic
+ ;; for the singleton base types (e.g. -Null, 1, etc)
+ [(Val-able: v)
+ (cond
+ [(eof-object? v)
+ (flat/sc #'eof-object?)]
+ [(void? v)
+ (flat/sc #'void?)]
+ [(or (symbol? v) (boolean? v) (keyword? v) (null? v))
+ (flat/sc #`(λ (x) (eq? '#,v x)))]
+ [else #;(or (number? v) (regexp? v) (string? v) (bytes? v) (char? v))
+ (flat/sc #`(λ (x) (equal? '#,v x)))])]
+ [(Base-name/contract: sym ctc) (flat/sc ctc)]
+ [(Distinction: _ _ t) ; from define-new-subtype
+ (t->sc t)]
+ [(Refinement: par p?)
+ (and/sc (t->sc par) (flat/sc p?))]
+ [(BaseUnion: bbits nbits)
+ (define numeric (make-BaseUnion #b0 nbits))
+ (define other-scs (map t->sc (bbits->base-types bbits)))
+ (define numeric-sc (numeric-type->static-contract numeric))
+ (if numeric-sc
+ (apply or/sc numeric-sc other-scs)
+ (apply or/sc (append other-scs (map t->sc (nbits->base-types nbits)))))]
+ [(? Union? t)
+ (match (normalize-type t)
+ [(HashTableTop:)
+ ;;bg TODO needed?
+ hash?/sc]
+ [(Union-all-flat: elems)
+ (let* ([sc* (map t->sc elems)]
+ [sc* (remove-duplicates sc*)]
+ [sc* (remove-overlap sc*
+ (list
+ (cons vector?/sc (list mutable-vector?/sc immutable-vector?/sc))
+ (cons hash?/sc (list mutable-hash?/sc weak-hash?/sc immutable-hash?/sc))))])
+ (apply or/sc sc*))]
+ [t (t->sc t)])]
+ [(Intersection: ts raw-prop)
+ (define scs (map t->sc ts))
+ (define prop/sc
+ (cond
+ [(TrueProp? raw-prop) #f]
+ [else (define x (genid))
+ (define prop (Intersection-prop (-id-path x) type))
+ (define name (format "~a" `(λ (,(syntax->datum x)) ,prop)))
+ (flat-named-lambda/sc name
+ (id/sc x)
+ (prop->sc prop))]))
+ (apply and/sc (append scs (if prop/sc (list prop/sc) '())))]
+ [(or (? Fun? t)
+ (? DepFun? t))
+ (match t
+ [(Fun: arrows)
+ (apply or/sc (map arrow->sc/transient arrows))]
+ [(DepFun/ids: _ dom _ _)
+ (define num-mand-args (length dom))
+ (make-procedure-arity-flat/sc num-mand-args '() '())])]
+ [(Set: _) set?/sc]
+ [(Sequence: _) sequence?/sc]
+ [(SequenceTop:) sequence?/sc]
+ [(Immutable-HeterogeneousVector: ts)
+ (immutable-vector-length/sc (length ts))]
+ [(Immutable-Vector: _)
+ immutable-vector?/sc]
+ [(Mutable-HeterogeneousVector: ts)
+ (mutable-vector-length/sc (length ts))]
+ [(Mutable-Vector: _)
+ mutable-vector?/sc]
+ [(Mutable-VectorTop:)
+ mutable-vector?/sc]
+ [(Box: _)
+ box?/sc]
+ [(Pair: _ _)
+ (match type
+ [(List: elem-t*)
+ list?/sc]
+ [(List: elem-t* #:tail rest-t*)
+ cons?/sc]
+ [_
+ (error 'type->static-contract "Pair-type match failed for type ~a" type)])]
+ [(Async-Channel: _)
+ async-channel?/sc]
+ [(Promise: _)
+ promise?/sc]
+ [(Opaque: p?)
+ (flat/sc p?)]
+ [(Continuation-Mark-Keyof: _)
+ continuation-mark-key?/sc]
+ [(Continuation-Mark-KeyTop:)
+ continuation-mark-key?/sc]
+ [(Prompt-Tagof: _ _)
+ prompt-tag?/sc]
+ [(Prompt-TagTop:)
+ prompt-tag?/sc]
+ [(F: v)
+ ;;bg TODO need to check anything???
+ ;(triple-lookup
+ ; (hash-ref recursive-values v
+ ; (λ () (error 'type->static-contract
+ ; "Recursive value lookup failed. ~a ~a" recursive-values v)))
+ ; typed-side)
+ any/sc]
+ [(VectorTop:) vector?/sc]
+ [(BoxTop:) box?/sc]
+ [(ChannelTop:) channel?/sc]
+ [(Async-ChannelTop:) async-channel?/sc]
+ [(MPairTop:) mpair?/sc]
+ [(ThreadCellTop:) thread-cell?/sc]
+ [(ThreadCell: _) thread-cell?/sc]
+ [(ClassTop:) class?/sc]
+ [(UnitTop:) unit?/sc]
+ [(StructTypeTop:) struct-type?/sc]
+ [(StructTop: s) (flat/sc #'struct?)] ;;bg TODO test
+ [(Poly: vs b)
+ ;;bg: for tag checks, poly-vars don't matter ... types inside better have a shape
+ (let ((recursive-values (for/fold ([rv recursive-values]) ([v vs])
+ (hash-set rv v (same any/sc)))))
+ (t->sc b #:recursive-values recursive-values))]
+ [(PolyDots: (list vs ... dotted-v) b)
+ (let ((recursive-values (for/fold ([rv recursive-values]) ([v vs])
+ (hash-set rv v (same any/sc)))))
+ (t->sc b #:recursive-values recursive-values))]
+ [(PolyRow: vs constraints body)
+ (let ((recursive-values (for/fold ([rv recursive-values]) ([v vs])
+ (hash-set rv v (same any/sc)))))
+ (extend-row-constraints vs (list constraints)
+ (t->sc body #:recursive-values recursive-values)))]
+ [(Mu: n b)
+ ;;bg: should not hit the name, but leave it at any/sc
+ (define rv (hash-set recursive-values n (same any/sc)))
+ (t->sc b #:recursive-values rv)]
+ ;; Don't directly use the class static contract generated for Name,
+ ;; because that will get an #:opaque class contract. This will do the
+ ;; wrong thing for object types since it errors too eagerly.
+ [(Instance: (? Name? t))
+ #:when (Class? (resolve-once t))
+ (cond [(lookup-name-sc type typed-side)]
+ [else
+ (define rv recursive-values)
+ (define resolved (make-Instance (resolve-once t)))
+ (define resolved-sc (t->sc resolved #:recursive-values rv))
+ (register-name-sc type
+ (λ () resolved-sc)
+ (λ () resolved-sc)
+ (λ () resolved-sc))
+ (lookup-name-sc type typed-side)])]
+ [(Instance: (Class: _ _ fields methods _ _))
+ (make-object-shape/sc (map car fields) (map car methods))]
+ [(Class: row-var inits fields publics augments _)
+ (make-class-shape/sc inits fields publics augments)]
+ [(Unit: imports exports init-depends results)
+ (raise-user-error 'type->static-contract/transient "unit")]
+ [(Struct: _ _ _ _ _ pred? _)
+ ;; (flat-named-contract '#,(syntax-e pred?) (lambda (x) (#,pred? x)))
+ (flat/sc #`(lambda (x) (#,pred? x)))]
+ [(StructType: s)
+ (flat/sc #'struct-type?)]
+ [(Struct-Property: s)
+ (flat/sc #'struct-type-property?)]
+ [(or (Prefab: key _) (PrefabTop: key))
+ (flat/sc #`(struct-type-make-predicate
+ (prefab-key->struct-type (quote #,(abbreviate-prefab-key key))
+ #,(prefab-key->field-count key))))]
+ [(Syntax: (? Base:Symbol?)) identifier?/sc]
+ [(Syntax: t)
+ syntax?/sc]
+ [(Param: in out)
+ parameter?/sc]
+ [(or (Mutable-HashTable: _ _)
+ (Mutable-HashTableTop:))
+ mutable-hash?/sc]
+ [(Immutable-HashTable: _ _)
+ immutable-hash?/sc]
+ [(or (Weak-HashTable: _ _)
+ (Weak-HashTableTop:))
+ weak-hash?/sc]
+ [(Channel: t)
+ channel?/sc]
+ [(Evt: t)
+ evt?/sc]
+ [(Rest: (list _))
+ list?/sc]
+ [(? Rest? rst) (t->sc (Rest->Type rst))]
+ [(? Prop? rep) (prop->sc rep)]
+ [_
+ (fail #:reason "contract generation not supported for this type")]))))
+
+(define (remove-overlap sc* pattern*)
+ (for/fold ((acc sc*))
+ ((kv* (in-list pattern*)))
+ (define replacement (car kv*))
+ (define tgt* (cdr kv*))
+ (define-values [success? acc+] (remove** tgt* acc))
+ (if success?
+ (cons replacement acc+)
+ acc)))
+
+(define (remove** target* sc*)
+ (for/fold ((success? #t)
+ (sc* sc*))
+ ((t (in-list target*)))
+ (values (and success?
+ (member t sc*))
+ (filter (lambda (x) (not (equal? x t))) sc*))))
+
+(define (obj->sc o)
+ (match o
+ [(Path: pes (? identifier? x))
+ (for/fold ([obj (id/sc x)])
+ ([pe (in-list (reverse pes))])
+ (match pe
+ [(CarPE:) (acc-obj/sc #'car obj)]
+ [(CdrPE:) (acc-obj/sc #'cdr obj)]
+ [(VecLenPE:) (acc-obj/sc #'vector-length obj)]))]
+ [(LExp: const terms)
+ (linear-exp/sc const
+ (for/hash ([(obj coeff) (in-terms terms)])
+ (values (obj->sc obj) coeff)))]
+ [else
+ (raise-argument-error 'obj->sc "Object?" o)]))
+
+(define (partition-kws kws)
+ (partition (match-lambda [(Keyword: _ _ mand?) mand?]) kws))
+
+(define arrow->sc/transient
+ (let ((conv (match-lambda [(Keyword: kw _ _) kw])))
+ (match-lambda
+ [(Arrow: dom _ kws _)
+ (define num-mand-args (length dom))
+ (define-values (mand-kws opt-kws)
+ (let*-values ([(mand-kws opt-kws) (partition-kws kws)])
+ (values (map conv mand-kws) (map conv opt-kws))))
+ (make-procedure-arity-flat/sc num-mand-args mand-kws opt-kws)])))
(define (t->sc/function f fail typed-side recursive-values loop method?)
(define (t->sc t #:recursive-values (recursive-values recursive-values))
@@ -817,7 +1145,8 @@
(map conv opt-kws))))
(define range (map t->sc rngs))
(define rest (and rst (t->sc/neg rst)))
- (function/sc (from-typed? typed-side) (process-dom mand-args) opt-args mand-kws opt-kws rest range))
+ (function/sc (from-typed? typed-side) ;; TODO 2020-02-10 probably need to keep side info
+ (process-dom mand-args) opt-args mand-kws opt-kws rest range))
(handle-arrow-range first-arrow convert-arrow)]
[else
(define ((f case->) a)
@@ -834,7 +1163,7 @@
(and rst (t->sc/neg rst))
(map t->sc rngs))
(function/sc
- (from-typed? typed-side)
+ (from-typed? typed-side) ;; TODO 2020-02-10
(process-dom (map t->sc/neg dom))
null
(map conv mand-kws)
@@ -873,7 +1202,7 @@
(remove-duplicates
(apply append (map free-ids rngs))
free-identifier=?)))
- (->i/sc (from-typed? typed-side)
+ (->i/sc (from-typed? typed-side) ;; TODO 2020-02-10
ids
dom*
dom-deps
@@ -1094,11 +1423,13 @@
[_ #false]))))
(module predicates racket/base
- (require racket/extflonum (only-in racket/contract/base >=/c <=/c))
+ (require racket/extflonum #;(only-in racket/contract/base >=/c <=/c)) ;;bg performance, I think
(provide nonnegative? nonpositive?
extflonum? extflzero? extflnonnegative? extflnonpositive?)
- (define nonnegative? (>=/c 0))
- (define nonpositive? (<=/c 0))
+ (define nonnegative? (lambda (x) (and (real? x) (>= x 0))) #;(>=/c 0))
+ (define nonpositive? (lambda (x) (and (real? x) (<= x 0))) #;(<=/c 0))
+ ;;bg;;(define nonnegative? (>=/c 0))
+ ;;bg;;(define nonpositive? (<=/c 0))
(define extflzero? (lambda (x) (extfl= x 0.0t0)))
(define extflnonnegative? (lambda (x) (extfl>= x 0.0t0)))
(define extflnonpositive? (lambda (x) (extfl<= x 0.0t0))))
@@ -1157,10 +1488,10 @@
(define exact-number/sc (numeric/sc Exact-Number (and/c number? exact?)))
(define inexact-complex/sc
(numeric/sc Inexact-Complex
- (and/c number?
- (lambda (x)
- (and (inexact-real? (imag-part x))
- (inexact-real? (real-part x)))))))
+ (lambda (x)
+ (and (number? x)
+ (inexact-real? (imag-part x))
+ (inexact-real? (real-part x))))))
(define number/sc (numeric/sc Number number?))
(define extflonum-zero/sc (numeric/sc ExtFlonum-Zero (and/c extflonum? extflzero?)))
diff --git a/typed-racket-lib/typed-racket/private/with-types.rkt b/typed-racket-lib/typed-racket/private/with-types.rkt
index 958b8a82..19dd9fff 100644
--- a/typed-racket-lib/typed-racket/private/with-types.rkt
+++ b/typed-racket-lib/typed-racket/private/with-types.rkt
@@ -50,10 +50,10 @@
(define-values (fv-ctc-ids fv-ctc-defs)
(type-stxs->ids+defs (syntax->list fvtys) 'untyped))
(define-values (ex-ctc-ids ex-ctc-defs)
- (type-stxs->ids+defs (syntax->list extys) 'typed))
+ (type-stxs->ids+defs (syntax->list extys) guarded))
(define-values (region-ctc-ids region-ctc-defs)
(if expr?
- (type-stxs->ids+defs (values-stx->type-stxs resty) 'typed)
+ (type-stxs->ids+defs (values-stx->type-stxs resty) guarded)
(values null null)))
(define region-tc-result
(and expr? (parse-tc-results resty)))
@@ -183,7 +183,9 @@
[pattern (~seq #:result ty:expr)])
(syntax-parse stx
[(_ :typed-ids fv:free-vars . body)
- (with-type-helper stx #'body #'(fv.id ...) #'(fv.ty ...) #'(id ...) #'(ty ...) #f #f (syntax-local-context))]
+ (parameterize ([current-type-enforcement-mode 'guarded])
+ (with-type-helper stx #'body #'(fv.id ...) #'(fv.ty ...) #'(id ...) #'(ty ...) #f #f (syntax-local-context)))]
[(_ :result-ty fv:free-vars . body)
- (with-type-helper stx #'body #'(fv.id ...) #'(fv.ty ...) #'() #'() #'ty #t (syntax-local-context))]))
+ (parameterize ([current-type-enforcement-mode 'guarded])
+ (with-type-helper stx #'body #'(fv.id ...) #'(fv.ty ...) #'() #'() #'ty #t (syntax-local-context)))]))
diff --git a/typed-racket-lib/typed-racket/rep/type-rep.rkt b/typed-racket-lib/typed-racket/rep/type-rep.rkt
index 011e8d12..c40c31cb 100644
--- a/typed-racket-lib/typed-racket/rep/type-rep.rkt
+++ b/typed-racket-lib/typed-racket/rep/type-rep.rkt
@@ -987,6 +987,7 @@
;; Intersection
;; ts - the list of types (gives deterministic behavior)
+;; prop - ???
;; elems - the set equivalent of 'ts', useful for equality tests
(def-type Intersection ([ts (cons/c Type? (listof Type?))]
[prop (and/c Prop? (not/c FalseProp?))]
diff --git a/typed-racket-lib/typed-racket/static-contracts/combinators/derived.rkt b/typed-racket-lib/typed-racket/static-contracts/combinators/derived.rkt
index 30f800f1..cd1f1747 100644
--- a/typed-racket-lib/typed-racket/static-contracts/combinators/derived.rkt
+++ b/typed-racket-lib/typed-racket/static-contracts/combinators/derived.rkt
@@ -4,7 +4,7 @@
;; These are used during optimizations as simplifications.
;; Ex: (listof/sc any/sc) => list?/sc
-(require "simple.rkt" "structural.rkt"
+(require "simple.rkt" "structural.rkt" "any.rkt"
(for-template racket/base racket/list racket/set racket/promise
racket/class racket/unit racket/async-channel))
(provide (all-defined-out))
@@ -36,13 +36,76 @@
(define weak-hash?/sc (and/sc hash?/sc (flat/sc #'hash-weak?)))
(define empty-hash/sc (and/sc hash?/sc (flat/sc #'(λ (h) (zero? (hash-count h))))))
+(define sequence?/sc (flat/sc #'sequence?))
+
(define channel?/sc (flat/sc #'channel?))
(define async-channel?/sc (flat/sc #'async-channel?))
(define thread-cell?/sc (flat/sc #'thread-cell?))
(define prompt-tag?/sc (flat/sc #'continuation-prompt-tag?))
(define continuation-mark-key?/sc (flat/sc #'continuation-mark-key?))
+(define evt?/sc (flat/sc #'evt?))
(define class?/sc (flat/sc #'class?))
(define unit?/sc (flat/sc #'unit?))
(define struct-type?/sc (flat/sc #'struct-type?))
+
+(define procedure?/sc (flat/sc #'procedure?))
+(define parameter?/sc (flat/sc #'parameter?))
+
+(define (procedure-arity-includes/sc n kws-ok)
+ (flat/sc #`(λ (f) (procedure-arity-includes? f '#,n '#,kws-ok))))
+
+(define (procedure-mandatory-keywords/sc pre-kws)
+ (define kws (sort pre-kws keyword<?))
+ (if (null? kws)
+ any/sc
+ (flat/sc
+ #`(λ (f)
+ (let-values ([(mand-kws _) (procedure-keywords f)])
+ (equal? mand-kws '#,kws))))))
+
+(define (procedure-optional-keywords/sc pre-kws)
+ (define kws (sort pre-kws keyword<?))
+ (if (null? kws)
+ any/sc
+ (flat/sc
+ #`(λ (f)
+ (let-values ([(_ opt-kws) (procedure-keywords f)])
+ ;; Goal: "expected" \subseteq "actual"
+ (let loop ([expected-kws '#,kws]
+ [actual-kws opt-kws])
+ (cond
+ [(null? expected-kws)
+ #true]
+ [(or (null? actual-kws) (keyword<? (car expected-kws) (car actual-kws)))
+ #false]
+ [(keyword<? (car actual-kws) (car expected-kws))
+ (loop expected-kws (cdr actual-kws))]
+ [else
+ (loop (cdr expected-kws) (cdr actual-kws))])))))))
+
+(define (make-procedure-arity-flat/sc num-mand mand-kws opt-kws)
+ (flat/sc
+ #`(λ (f)
+ (and (procedure? f)
+ (procedure-arity-includes? f '#,num-mand '#,(not (null? mand-kws)))
+ #,@(if (null? mand-kws)
+ #'()
+ #`((let-values (((f-mand-kws _) (procedure-keywords f)))
+ (equal? '#,mand-kws f-mand-kws))))
+ #,@(if (null? opt-kws)
+ #'()
+ #`((let-values (((_ f-opt-kws) (procedure-keywords f)))
+ (let loop ((expected-kws '#,(sort opt-kws keyword<?))
+ (actual-kws f-opt-kws))
+ (cond
+ ((null? expected-kws)
+ #true)
+ ((or (null? actual-kws) (keyword<? (car expected-kws) (car actual-kws)))
+ #false)
+ ((keyword<? (car actual-kws) (car expected-kws))
+ (loop expected-kws (cdr actual-kws)))
+ (else
+ (loop (cdr expected-kws) (cdr actual-kws))))))))))))
+
diff --git a/typed-racket-lib/typed-racket/static-contracts/combinators/name.rkt b/typed-racket-lib/typed-racket/static-contracts/combinators/name.rkt
index 7da0532f..449c068a 100644
--- a/typed-racket-lib/typed-racket/static-contracts/combinators/name.rkt
+++ b/typed-racket-lib/typed-racket/static-contracts/combinators/name.rkt
@@ -72,7 +72,8 @@
(case typed-side
[(both) (car result)]
[(typed) (cadr result)]
- [(untyped) (caddr result)])))
+ [(untyped) (caddr result)]
+ [else (raise-argument-error 'lookup-name-sc "side?" typed-side)])))
(define (register-name-sc type typed-thunk untyped-thunk both-thunk)
(define-values (typed-name untyped-name both-name)
diff --git a/typed-racket-lib/typed-racket/static-contracts/combinators/object.rkt b/typed-racket-lib/typed-racket/static-contracts/combinators/object.rkt
index 49484509..7d1ad4f8 100644
--- a/typed-racket-lib/typed-racket/static-contracts/combinators/object.rkt
+++ b/typed-racket-lib/typed-racket/static-contracts/combinators/object.rkt
@@ -5,11 +5,12 @@
(require "../../utils/utils.rkt"
"../structures.rkt" "../constraints.rkt"
+ "simple.rkt"
racket/list racket/match
(contract-req)
racket/syntax
typed-racket/utils/opaque-object
- (for-template racket/base racket/class
+ (for-template racket/base racket/class racket/contract
typed-racket/utils/opaque-object)
(for-syntax racket/base syntax/parse))
@@ -18,6 +19,9 @@
(define field-modifiers '(field init init-field inherit-field))
(define method-modifiers '(method inherit super inner override augment augride))
+;; Bottom-out members
+(define (f-any _) #'any/c)
+
(struct object-combinator combinator (opaque?)
#:transparent
#:property prop:combinator-name "object/sc"
@@ -103,15 +107,12 @@
(define ((member-spec->form f) v)
(match v
[(member-spec modifier id sc)
- (with-syntax ([ctc-stx (and sc (f sc) empty)]
- [id-stx id])
- (define id/ctc
- (if sc #`(#,id #,(f sc)) id))
- (match modifier
- ['method id/ctc]
- ['inner #`(inner #,id/ctc)]
- ['init #`(init #,id/ctc)]
- ['field #`(field #,id/ctc)]))]))
+ (with-syntax ([id/ctc (if sc #`(#,id #,(f sc)) id)])
+ (case modifier
+ [(method) #'id/ctc]
+ [(inner) #'(inner id/ctc)]
+ [(init) #'(init id/ctc)]
+ [(field) #'(field id/ctc)]))]))
(define (spec->id/ctc f modifier vals)
(for/lists (_1 _2)
@@ -120,13 +121,14 @@
(values (member-spec-id spec)
(f (member-spec-sc spec)))))
-(define (object/sc->contract v f)
+(define (object/sc->contract v f)
(match v
[(object-combinator (member-seq vals) opaque?)
#`(#,(if opaque?
#'object/c-opaque
#'object/c)
#,@(map (member-spec->form f) vals))]))
+
(define (class/sc->contract v f)
(match v
[(class-combinator (member-seq vals) opaque absents)
@@ -159,13 +161,51 @@
(augment [pubment-name pubment-temp] ...)
(inherit [pubment-name pubment-temp] ...)
(absent #,@absents)))]))
+
(define (instance/sc->contract v f)
(match v
[(instanceof-combinator (list class))
#`(instanceof/c #,(f class))]))
+(define (make-class-shape/sc inits fields publics augments)
+ (define init* (map car inits))
+ (define field* (map car fields))
+ (define public* (map car publics))
+ (define augment* (map car augments))
+ (define pubment*
+ (for/list ([name (in-list public*)]
+ #:when (memq name augment*))
+ name))
+ (define override*
+ (for/list ([name (in-list public*)]
+ #:unless (memq name pubment*))
+ name))
+ (with-syntax ((ctc-stx
+ #`(class/c
+ (init . #,init*)
+ (field . #,field*)
+ (override . #,override*)
+ (augment . #,augment*)
+ . #,pubment*)))
+ (flat/sc
+ #'(let ((check-cls-shape (contract-first-order ctc-stx)))
+ (λ (cls)
+ (and (class? cls) (check-cls-shape cls)))))))
+
+(define (make-object-shape/sc field-name* method-name*)
+ (with-syntax ((ctc-stx #`(object/c (field . #,field-name*) . #,method-name*)))
+ (flat/sc
+ #'(let ((check-obj-shape (contract-first-order ctc-stx)))
+ (λ (this)
+ (and (object? this) (check-obj-shape this)))))))
+
+(provide
+ make-class-shape/sc
+ make-object-shape/sc)
+
(provide/cond-contract
[struct member-spec ([modifier symbol?] [id symbol?] [sc static-contract?])]
[object/sc (boolean? (listof object-member-spec?) . -> . static-contract?)]
[class/sc (boolean? (listof member-spec?) (listof symbol?) . -> . static-contract?)]
[instanceof/sc (static-contract? . -> . static-contract?)])
+
diff --git a/typed-racket-lib/typed-racket/static-contracts/combinators/structural.rkt b/typed-racket-lib/typed-racket/static-contracts/combinators/structural.rkt
index ef53394e..8236d06a 100644
--- a/typed-racket-lib/typed-racket/static-contracts/combinators/structural.rkt
+++ b/typed-racket-lib/typed-racket/static-contracts/combinators/structural.rkt
@@ -156,20 +156,20 @@
((list/sc . (#:covariant)) list/c #:flat)
((listof/sc (#:covariant)) listof #:flat)
((cons/sc (#:covariant) (#:covariant)) cons/c #:flat)
- ((set/sc (#:covariant #:chaperone)) set/c #:flat)
((struct-property/sc (#:invariant)) struct-type-property/c #:impersonator)
- ((immutable-vectorof/sc (#:covariant)) immutable-vectorof/c #:flat)
- ((mutable-vectorof/sc (#:invariant)) mutable-vectorof/c #:chaperone)
- ((vectorof/sc (#:invariant)) vectorof #:chaperone)
+ ((set/sc (#:covariant #:chaperone)) set/c #:flat)
+ ((vector/sc . (#:invariant)) vector/c #:chaperone)
((immutable-vector/sc . (#:covariant)) immutable-vector/c #:flat)
((mutable-vector/sc . (#:invariant)) mutable-vector/c #:chaperone)
- ((vector/sc . (#:invariant)) vector/c #:chaperone)
+ ((vectorof/sc (#:invariant)) vectorof #:chaperone)
+ ((immutable-vectorof/sc (#:covariant)) immutable-vectorof/c #:flat)
+ ((mutable-vectorof/sc (#:invariant)) mutable-vectorof/c #:chaperone)
((promise/sc (#:covariant)) promise-not-name/c #:chaperone)
((syntax/sc (#:covariant #:flat)) syntax/c #:flat)
- ((hash/sc (#:invariant) (#:invariant)) typed-racket-hash/c #:chaperone)
- ((mutable-hash/sc (#:invariant) (#:invariant)) mutable-hash/c #:chaperone)
- ((immutable-hash/sc (#:covariant) (#:covariant)) immutable-hash/c #:flat)
- ((weak-hash/sc (#:invariant) (#:invariant)) weak-hash/c #:chaperone)
+ ((hash/sc (#:invariant #:flat) (#:invariant)) hash/c #:chaperone)
+ ((mutable-hash/sc (#:invariant #:flat) (#:invariant)) mutable-hash/c #:chaperone)
+ ((immutable-hash/sc (#:covariant #:flat) (#:covariant)) immutable-hash/c #:flat)
+ ((weak-hash/sc (#:invariant #:flat) (#:invariant)) weak-hash/c #:chaperone)
((box/sc (#:invariant)) box/c #:chaperone)
((parameter/sc (#:contravariant) (#:covariant)) parameter/c #:chaperone)
((sequence/sc . (#:covariant)) sequence/c #:impersonator)
@@ -177,3 +177,4 @@
((continuation-mark-key/sc (#:invariant)) continuation-mark-key/c #:chaperone)
((evt/sc (#:covariant)) tr:evt/c #:chaperone)
((async-channel/sc (#:invariant)) async-channel/c #:chaperone))
+
diff --git a/typed-racket-lib/typed-racket/static-contracts/utils.rkt b/typed-racket-lib/typed-racket/static-contracts/utils.rkt
new file mode 100644
index 00000000..f32a72d0
--- /dev/null
+++ b/typed-racket-lib/typed-racket/static-contracts/utils.rkt
@@ -0,0 +1,5 @@
+#lang racket/base
+(provide
+ log-static-contract-info
+ log-static-contract-warning)
+(define-logger static-contract)
diff --git a/typed-racket-lib/typed-racket/tc-setup.rkt b/typed-racket-lib/typed-racket/tc-setup.rkt
index 0d092335..47af718a 100644
--- a/typed-racket-lib/typed-racket/tc-setup.rkt
+++ b/typed-racket-lib/typed-racket/tc-setup.rkt
@@ -10,10 +10,11 @@
(for-syntax racket/base)
(for-template racket/base))
(lazy-require [typed-racket/optimizer/optimizer (optimize-top)])
+(lazy-require [typed-racket/defender/defender (defend-top)])
(lazy-require [typed-racket/typecheck/tc-toplevel (tc-module)])
(lazy-require [typed-racket/typecheck/toplevel-trampoline (tc-toplevel-start)])
-(provide maybe-optimize init-current-type-names
+(provide maybe-optimize maybe-defend init-current-type-names
tc-module/full
tc-toplevel/full)
@@ -31,6 +32,7 @@
;; current code inspector has sufficient privileges
(if (and (optimize?)
(not (getenv "PLT_TR_NO_OPTIMIZE"))
+ (memq (current-type-enforcement-mode) (list guarded transient))
(authorized-code-inspector?))
(begin
(do-time "Starting optimizer")
@@ -38,6 +40,19 @@
(do-time "Optimized")))
body))
+(define (maybe-defend body ctc-cache sc-cache)
+ (case (current-type-enforcement-mode)
+ [(transient)
+ (do-time "Starting defender")
+ (define extra-def* (box '()))
+ (define body+
+ (for/list ([b (in-list (syntax-e body))])
+ (defend-top b ctc-cache sc-cache extra-def*)))
+ (do-time "Defended")
+ (cons (reverse (unbox extra-def*)) body+)]
+ [else
+ (cons '() body)]))
+
;; -> Promise<Dict<Name, Type>>
;; initialize the type names for printing
(define (init-current-type-names)
@@ -51,7 +66,7 @@
(define-logger online-check-syntax)
(define (tc-setup orig-stx stx expand-ctxt do-expand stop-forms k)
- (set-box! typed-context? #t)
+ (set-box! typed-context? #true)
;(start-timing (syntax-property stx 'enclosing-module-name))
(with-handlers
(#;[(λ (e) (and (exn:fail? e) (not (exn:fail:syntax? e)) (not (exn:fail:filesystem? e))))
diff --git a/typed-racket-lib/typed-racket/typecheck/provide-handling.rkt b/typed-racket-lib/typed-racket/typecheck/provide-handling.rkt
index d55ac4c4..aba6f8e9 100644
--- a/typed-racket-lib/typed-racket/typecheck/provide-handling.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/provide-handling.rkt
@@ -49,17 +49,18 @@
(define mapping (make-free-id-table))
;; quad/c in the signatures corresponds to four values:
- ;; (values syntax? syntax? identfier? (listof (list/c identifier? identifier?))
+ ;; (values syntax? syntax? identifier? (listof (list/c identifier? identifier?)) (listof (list/c identifier? type?)))
;; First return value is a syntax object of definitions, which will go in
;; the #%contract-defs submodule
;; Second is a syntax object of definitions to go in the main module, including
;; the defintion to be exported
;; Third is the id to export
;; Fourth is a list of two element lists representing type aliases
+ ;; FIFTH added by Ben for S -- T interaction, experiment
;; mk-ignored-quad : identifier -> quad/c
- (define (mk-ignored-quad i) (values #'(begin) #'(begin) i null))
+ (define (mk-ignored-quad i) (values #'(begin) #'(begin) i null null))
;; mk : id -> quad/c
;;
@@ -97,18 +98,18 @@
(define (mk-struct-syntax-quad internal-id new-id si constr-type)
(define type-is-constructor? #t) ;Conservative estimate (provide/contract does the same)
(match-define (list type-desc constr pred (list accs ...) muts super) (extract-struct-info si))
- (define-values (defns export-defns new-ids aliases)
- (for/lists (defns export-defns new-ids aliases)
+ (define-values (defns export-defns new-ids aliases rtss)
+ (for/lists (defns export-defns new-ids aliases rtss)
([e (in-list (list* type-desc pred super accs))])
(if (identifier? e)
(mk e)
(mk-ignored-quad e))))
;; Here, we recursively handle all of the identifiers referenced
;; in this static struct info.
- (define-values (constr-defn constr-export-defn constr-new-id constr-aliases)
+ (define-values (constr-defn constr-export-defn constr-new-id constr-aliases constr-rts)
(cond
[(not (identifier? constr))
- (values #'(begin) #'(begin) #f null)]
+ (values #'(begin) #'(begin) #f null null)]
[(free-identifier=? constr internal-id)
(mk-value-quad constr (generate-temporary constr) constr-type)]
[else
@@ -148,25 +149,34 @@
(make-rename-transformer #'protected-id)))
#'export-id
(cons (list #'export-id internal-id)
- (apply append constr-aliases aliases)))))
-
+ (apply append constr-aliases aliases))
+ (cons (list new-id constr-type)
+ (apply append constr-rts rtss)))))
;; mk-syntax-quad : identifier? identifier? -> quad/c
(define (mk-syntax-quad internal-id new-id)
- (with-syntax* ([id internal-id]
- [export-id new-id]
- [untyped-id (freshen-id #'id)])
- (values
- #`(begin)
- ;; There's no need to put this macro in the submodule since it
- ;; has no dependencies.
- #`(begin
- (define-syntax (untyped-id stx)
- (tc-error/stx stx "Macro ~a from typed module used in untyped code" 'untyped-id))
- (define-syntax export-id
- (make-typed-renaming #'id #'untyped-id)))
- new-id
- (list (list #'export-id #'id)))))
+ (case (current-type-enforcement-mode)
+ [(guarded)
+ (with-syntax* ([id internal-id]
+ [export-id new-id]
+ [untyped-id (freshen-id #'id)])
+ (values
+ #`(begin)
+ ;; There's no need to put this macro in the submodule since it
+ ;; has no dependencies.
+ #`(begin
+ (define-syntax (untyped-id stx)
+ (tc-error/stx stx "Macro ~a from typed module used in untyped code" 'untyped-id))
+ (define-syntax export-id
+ (make-typed-renaming #'id #'untyped-id '#,(current-type-enforcement-mode))))
+ new-id
+ (list (list #'export-id #'id))
+ null))]
+ [(transient erasure)
+ ;; export the syntax
+ (mk-ignored-quad internal-id)]
+ [else
+ (raise-arguments-error 'mk-syntax-quad "bad mode" "(current-type-enforcement-mode)" (current-type-enforcement-mode))]))
;; mk-value-quad : identifier? identifier? (or/c Type #f) -> quad/c
(define (mk-value-quad internal-id new-id ty)
@@ -186,19 +196,21 @@
;; For the main module
#`(begin (define-syntax local-untyped-id (#,mk-redirect-id (quote-syntax untyped-id)))
(define-syntax export-id
- (make-typed-renaming #'id #'local-untyped-id)))
+ (make-typed-renaming #'id #'local-untyped-id '#,(current-type-enforcement-mode))))
new-id
- null)))
+ null
+ (list (list new-id ty))
+ )))
;; Build the final provide with auxilliary definitions
- (for/lists (defs export-defs provides aliases)
+ (for/lists (defs export-defs provides aliases rts)
;; sort provs to generate deterministic output
([(internal-id external-ids) (in-sorted-free-id-table provs)])
- (define-values (defs export-def id alias) (mk internal-id))
+ (define-values (defs export-def id alias rt) (mk internal-id))
(define provide-forms
(for/list ([external-id (in-list external-ids)])
#`(rename-out [#,id #,external-id])))
(values #`(begin #,defs)
export-def
#`(provide #,@provide-forms)
- alias)))
+ alias rt)))
diff --git a/typed-racket-lib/typed-racket/typecheck/renamer.rkt b/typed-racket-lib/typed-racket/typecheck/renamer.rkt
index 1a73a321..abcaaf86 100644
--- a/typed-racket-lib/typed-racket/typecheck/renamer.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/renamer.rkt
@@ -6,13 +6,14 @@
;; a constructor for typed renamings that attach the required
;; 'not-free-identifier properties
-(define (make-typed-renaming target alternate)
+(define (make-typed-renaming target alternate enforcement-mode)
(typed-renaming (syntax-property target 'not-free-identifier=? #t)
- (syntax-property alternate 'not-free-identifier=? #t)))
+ (syntax-property alternate 'not-free-identifier=? #t)
+ enforcement-mode))
;; target : identifier
;; alternate : identifier
-(struct typed-renaming (target alternate)
+(struct typed-renaming (target alternate enforcement-mode)
;; prevent the rename transformer from expanding in
;; module-begin context because the typed context flag
;; will not be set until the module-begin
@@ -22,7 +23,7 @@
;; expansion time when the typed context flag is set correctly
#:property prop:rename-transformer
(λ (obj)
- (if (unbox typed-context?)
+ (if (eq? (current-type-enforcement-mode) (typed-renaming-enforcement-mode obj))
(typed-renaming-target obj)
(typed-renaming-alternate obj))))
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-app-helper.rkt b/typed-racket-lib/typed-racket/typecheck/tc-app-helper.rkt
index 51911833..af107aaa 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-app-helper.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-app-helper.rkt
@@ -19,7 +19,7 @@
. ->* . full-tc-results/c)])
(define (tc/funapp1 f-stx args-stx ftype0 arg-ress expected #:check [check? #t])
;; update tooltip-table with inferred function type
- (add-typeof-expr f-stx (ret (make-Fun (list ftype0))))
+ (add-typeof-expr f-stx (ret (make-Fun (list ftype0)))) ;;bg maybe should be set-typeof-expr
(match* (ftype0 arg-ress)
;; we check that all kw args are optional
[((Arrow: dom rst (list (Keyword: _ _ #f) ...) rng)
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-lambda.rkt b/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-lambda.rkt
index 68a45d21..5028e9e8 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-lambda.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-lambda.rkt
@@ -6,7 +6,7 @@
(prefix-in - (contract-req))
syntax/parse racket/match racket/list
racket/sequence
- (typecheck signatures find-annotation)
+ (typecheck signatures find-annotation tc-metafunctions)
(types abbrev utils generalize type-table)
(private type-annotation syntax-properties)
;; Needed to construct args to tc/let-values
@@ -24,18 +24,30 @@
(define-tc/app-syntax-class (tc/app-lambda expected)
#:literal-sets (kernel-literals)
;; let loop
- (pattern ((letrec-values ([(lp) (~and lam (#%plain-lambda (args ...) . body))]) lp*:id) . actuals)
+ (pattern ((~and loop (letrec-values ([(lp) (~and lam (#%plain-lambda (args ...) . body))]) lp*:id)) . actuals)
#:when expected
#:when (not (andmap type-annotation (syntax->list #'(lp args ...))))
#:when (free-identifier=? #'lp #'lp*)
- (let-loop-check #'lam #'lp #'actuals #'(args ...) #'body expected))
+ (let ([r (let-loop-check #'lam #'lp #'actuals #'(args ...) #'body expected)])
+ ;;bg TODO needed?
+ (define univ* (for/list ([_arg (in-list (syntax-e #'(args ...)))]) Univ))
+ (add-typeof-expr #'loop (ret (->* univ* Univ)))
+ r))
;; inference for ((lambda
(pattern ((~and lam (#%plain-lambda (x ...) . body)) args ...)
#:fail-when (plambda-property #'lam) #f
#:fail-unless (= (syntax-length #'(x ...))
(syntax-length #'(args ...))) #f
#:fail-when (andmap type-annotation (syntax->list #'(x ...))) #f
- (tc/let-values #'((x) ...) #'(args ...) #'body expected))
+ (let ([r (tc/let-values #'((x) ...) #'(args ...) #'body expected)])
+ ;;bg TODO needed? 2020-03-05 seems no, because literal lambda avoid cod-check
+ (define arg-ts
+ (for/list ([arg (in-list (syntax-e #'(args ...)))])
+ (match (type-of arg)
+ [(tc-result1: t) t])))
+ (define return-type (tc-results->values r))
+ (add-typeof-expr #'lam (ret (->* arg-ts return-type)))
+ r))
;; inference for ((lambda with dotted rest
(pattern ((~and lam (#%plain-lambda (x ... . rst:id) . body)) args ...)
#:fail-when (plambda-property #'lam) #f
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-apply.rkt b/typed-racket-lib/typed-racket/typecheck/tc-apply.rkt
index 299931d5..d7a7e5ab 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-apply.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-apply.rkt
@@ -62,6 +62,7 @@
(ormap Keyword-required? kws)))
(or
(for/or ([arrow (in-list arrows)])
+ ;; bg may need to bind this and `(add-typeof-expr f (ret (make-Fun (list arrow))))`
(match arrow
[(Arrow: domain rst _ rng)
;; Takes a possible substitution and computes
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt b/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt
index e564d3a8..f8344206 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-structs.rkt
@@ -7,7 +7,7 @@
(rep free-variance)
(private parse-type syntax-properties)
(types abbrev subtype utils resolve substitute struct-table)
- (env global-env type-name-env type-alias-env tvar-env)
+ (env global-env type-name-env type-alias-env tvar-env transient-env)
(utils tc-utils prefab identifier)
(typecheck typechecker def-binding internal-forms error-message)
(for-syntax syntax/parse racket/base)
@@ -187,7 +187,8 @@
(register-alias type-name)
(register-alias (struct-names-struct-name names))
(register-type-name type-name
- (make-Poly (struct-desc-tvars desc) sty)))
+ (make-Poly (struct-desc-tvars desc) sty))
+ (register-transient-trusted-positive! (struct-names-predicate names)))
;; Register the approriate types to the struct bindings.
(define/cond-contract (register-struct-bindings! sty names desc si)
diff --git a/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt b/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt
index ff1d80d5..f564c576 100644
--- a/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt
+++ b/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt
@@ -484,9 +484,10 @@
(with-syntax*
([the-variable-reference (generate-temporary #'blame)]
[mk-redirect (generate-temporary #'make-redirect)])
- (define-values (defs export-defs provs aliasess)
+ (define-values (defs export-defs provs aliasess rtss)
(generate-prov def-tbl provide-tbl #'the-variable-reference #'mk-redirect))
(define aliases (apply append aliasess))
+ (define rts (apply append rtss))
(define/with-syntax (new-defs ...) defs)
(define/with-syntax (new-export-defs ...) export-defs)
(define/with-syntax (new-provs ...) provs)
@@ -510,6 +511,9 @@
typed-racket/types/struct-table typed-racket/types/abbrev
(rename-in racket/private/sort [sort raw-sort]))
#,@(make-env-init-codes)
+ #,@(for/list ((rt (in-list rts)))
+ ;; 2020-03 : rts = ids + types, extra types to register to help typed -> transient interaction, not sure if helpful
+ (make-register-type-code (car rt) (cadr rt)))
#,@(for/list ([a (in-list aliases)])
(match-define (list from to) a)
#`(add-alias (quote-syntax #,from) (quote-syntax #,to))))))
diff --git a/typed-racket-lib/typed-racket/types/path-type.rkt b/typed-racket-lib/typed-racket/types/path-type.rkt
index 623af760..7ed3f5cc 100644
--- a/typed-racket-lib/typed-racket/types/path-type.rkt
+++ b/typed-racket-lib/typed-racket/types/path-type.rkt
@@ -5,7 +5,6 @@
(contract-req)
(rep object-rep type-rep values-rep)
(utils tc-utils prefab)
- (typecheck renamer)
(types subtype resolve numeric-tower)
(except-in (types utils abbrev kw-types) -> ->* one-of/c))
diff --git a/typed-racket-lib/typed-racket/types/type-table.rkt b/typed-racket-lib/typed-racket/types/type-table.rkt
index ba354330..bdc7bf45 100644
--- a/typed-racket-lib/typed-racket/types/type-table.rkt
+++ b/typed-racket-lib/typed-racket/types/type-table.rkt
@@ -17,6 +17,11 @@
(provide/cond-contract
[add-typeof-expr (syntax? tc-results/c . -> . any/c)]
+ [set-typeof-expr (syntax? tc-results/c . -> . any/c)] ;;bg
+ ;; need this to forget type information, because the 1st typechecking pass
+ ;; optimistically assumes everything is well typed, and the 2nd pass needs
+ ;; to pessimisitcally assume "Any" about things from untyped code
+
[type-of (syntax? . -> . tc-results/c)]
[reset-type-table (-> any/c)]
[type-table->tooltips
@@ -77,9 +82,18 @@
[else t]))
#f))
+(define (set-typeof-expr e t)
+ (hash-set! type-table e t))
+
+;; Need to define/provide this, because `type-of` doesnt actually raise an exception, just delays an int-err
+;; TODO though, probably an issue with missing type and argument happesn to be a format string
+(provide maybe-type-of)
+(define (maybe-type-of e)
+ (hash-ref type-table e #false))
+
(define (type-of e)
(hash-ref type-table e
- (lambda () (int-err (format "no type for ~s at: ~a line ~a col ~a"
+ (lambda () (int-err (format "no type for ~a at: ~a line ~a col ~a"
(syntax->datum e)
(syntax-source e)
(syntax-line e)
diff --git a/typed-racket-lib/typed-racket/utils/tc-utils.rkt b/typed-racket-lib/typed-racket/utils/tc-utils.rkt
index 54ed5e6b..e29b2b1a 100644
--- a/typed-racket-lib/typed-racket/utils/tc-utils.rkt
+++ b/typed-racket-lib/typed-racket/utils/tc-utils.rkt
@@ -42,6 +42,12 @@ don't depend on any other portion of the system
id-from?
id-from
+ current-type-enforcement-mode
+ type-enforcement-mode?
+ guarded
+ transient
+ erasure
+
(all-from-out "disappeared-use.rkt"))
;; a parameter representing the original location of the syntax being
@@ -282,20 +288,34 @@ don't depend on any other portion of the system
;; are we currently expanding in a typed module (or top-level form)?
(define typed-context? (box #f))
+(define guarded 'guarded)
+(define transient 'transient)
+(define erasure 'erasure)
+
+(define (type-enforcement-mode? x)
+ (and (symbol? x)
+ (or (eq? x guarded)
+ (eq? x transient)
+ (eq? x erasure))))
+
+;; if we are in a typed module, how do we enforce types?
+;; (or/c #f type-enforcement-mode?)
+(define current-type-enforcement-mode (make-parameter #f))
+
;; environment constructor
(define-syntax (make-env stx)
(define-syntax-class spec
#:transparent
- #:attributes (ty id)
- (pattern [nm:identifier ~! ty]
+ #:attributes (ty id trusted-pos)
+ (pattern [nm:identifier ~! ty (~optional trusted-pos #:defaults ([trusted-pos #'#f]))]
#:fail-when (and (not (list? (identifier-template-binding #'nm))) #'nm)
"not a bound identifier"
#:with id #'(quote-syntax nm))
- (pattern [e:expr ty]
+ (pattern [e:expr ty (~optional trusted-pos #:defaults ([trusted-pos #'#f]))]
#:with id #'e))
(syntax-parse stx
[(_ e:spec ...)
- #'(list (list e.id e.ty) ...)]))
+ #'(list (list e.id e.ty e.trusted-pos) ...)]))
;; id: identifier
;; sym: a symbol
@@ -309,3 +329,4 @@ don't depend on any other portion of the system
(define-syntax-class (id-from sym mod)
(pattern i:id
#:fail-unless (id-from? #'i sym mod) #f))
+
diff --git a/typed-racket-more/typed/untyped-utils.rkt b/typed-racket-more/typed/untyped-utils.rkt
index baab35b5..6964ef02 100644
--- a/typed-racket-more/typed/untyped-utils.rkt
+++ b/typed-racket-more/typed/untyped-utils.rkt
@@ -20,7 +20,7 @@
[(_ name:id typed-name:id untyped-name:id)
(syntax/loc stx
(define-syntax name
- (make-typed-renaming #'typed-name #'untyped-name)))]))
+ (make-typed-renaming #'typed-name #'untyped-name guarded)))]))
(define-for-syntax (freshen ids)
(stx-map (lambda (id) ((make-syntax-introducer) id)) ids))
diff --git a/typed-racket-test/transient/README.md b/typed-racket-test/transient/README.md
new file mode 100644
index 00000000..5392265a
--- /dev/null
+++ b/typed-racket-test/transient/README.md
@@ -0,0 +1,8 @@
+Summary
+---
+
+- `pass/` modules that compile & run successfully
+- `error/` modules that type-check, but correctly raise a run-time error
+- `unsupported-features/` examples that are not supported by the current
+ transient prototype
+
diff --git a/typed-racket-test/transient/error/filter.rkt b/typed-racket-test/transient/error/filter.rkt
new file mode 100644
index 00000000..21923fa0
--- /dev/null
+++ b/typed-racket-test/transient/error/filter.rkt
@@ -0,0 +1,14 @@
+#lang typed/racket/base #:transient
+
+(module u racket/base
+ (provide nats)
+ (define nats '(1 2 three four)))
+
+(require/typed 'u
+ (nats (Listof Natural)))
+
+(: myadd (-> Natural Natural))
+(define (myadd n)
+ (add1 n))
+
+(filter myadd nats)
diff --git a/typed-racket-test/transient/error/find.rkt b/typed-racket-test/transient/error/find.rkt
new file mode 100644
index 00000000..af32ade7
--- /dev/null
+++ b/typed-racket-test/transient/error/find.rkt
@@ -0,0 +1,15 @@
+#lang typed/racket/base #:transient
+
+(module a racket/base
+ (provide fake-int* checker)
+ (define fake-int* '(NaN xxx))
+ (define (checker x)
+ #true))
+
+(require/typed 'a
+ (fake-int* (Listof Integer))
+ (checker (-> Integer Boolean)))
+
+(define x : (U #f Integer)
+ (findf checker fake-int*))
+
diff --git a/typed-racket-test/transient/error/fold.rkt b/typed-racket-test/transient/error/fold.rkt
new file mode 100644
index 00000000..7e0e227d
--- /dev/null
+++ b/typed-racket-test/transient/error/fold.rkt
@@ -0,0 +1,13 @@
+#lang typed/racket/base #:transient
+
+(module a racket/base
+ (provide f)
+ (define (f acc i)
+ 'not-int))
+
+(require/typed 'a
+ (f (-> Integer Integer Integer)))
+
+(define x : (U #f Integer)
+ (foldl f 0 '(0 1 2)))
+
diff --git a/typed-racket-test/transient/error/for.rkt b/typed-racket-test/transient/error/for.rkt
new file mode 100644
index 00000000..d24280c1
--- /dev/null
+++ b/typed-racket-test/transient/error/for.rkt
@@ -0,0 +1,15 @@
+#lang typed/racket/base #:transient
+
+(module u racket/base
+ (provide nats)
+ (define nats '(1 2 three four)))
+
+(require/typed 'u
+ (nats (Listof Natural)))
+
+(: myadd (-> Natural Natural))
+(define (myadd n)
+ (add1 n))
+
+(for ((n (in-list nats)))
+ (myadd n))
diff --git a/typed-racket-test/transient/error/struct.rkt b/typed-racket-test/transient/error/struct.rkt
new file mode 100644
index 00000000..a041863a
--- /dev/null
+++ b/typed-racket-test/transient/error/struct.rkt
@@ -0,0 +1,16 @@
+#lang racket/base
+
+(module t typed/racket #:transient
+ (struct A ((x : Integer) (y : (Listof Integer)) (z : (-> Integer Integer))))
+ (: f (-> (Listof A) Integer))
+ (define (f x)
+ (define mya (car x))
+ (A-x mya))
+
+ (provide (struct-out A) f))
+
+(require 't)
+
+(define a (A 'NaN '() add1))
+
+(f (list a))
diff --git a/typed-racket-test/transient/error/submodule-list-0.rkt b/typed-racket-test/transient/error/submodule-list-0.rkt
new file mode 100644
index 00000000..e15de049
--- /dev/null
+++ b/typed-racket-test/transient/error/submodule-list-0.rkt
@@ -0,0 +1,10 @@
+#lang typed/racket/base #:transient
+
+(module u racket/base
+ (define x* (list "OOPS"))
+ (provide x*))
+
+(require/typed 'u
+ (x* (Listof Integer)))
+
+(+ (car x*) 1)
diff --git a/typed-racket-test/transient/error/submodule-struct-0.rkt b/typed-racket-test/transient/error/submodule-struct-0.rkt
new file mode 100644
index 00000000..8c1e14b6
--- /dev/null
+++ b/typed-racket-test/transient/error/submodule-struct-0.rkt
@@ -0,0 +1,12 @@
+#lang typed/racket #:transient
+
+(module u racket/base
+ (struct posn [x y])
+ (define origin (posn 0 #false))
+ (provide origin (struct-out posn)))
+
+(require/typed 'u
+ (#:struct posn ((x : Real) (y : Real)))
+ (origin posn))
+
+(+ (posn-x origin) (posn-y origin))
diff --git a/typed-racket-test/transient/error/values.rkt b/typed-racket-test/transient/error/values.rkt
new file mode 100644
index 00000000..85cbd039
--- /dev/null
+++ b/typed-racket-test/transient/error/values.rkt
@@ -0,0 +1,13 @@
+#lang typed/racket/base #:transient
+
+(module u racket/base
+ (provide f)
+ (define (f x)
+ (values x x)))
+
+(require/typed 'u
+ (f (-> Natural (Values (Boxof Symbol) Natural))))
+
+(define-values [a b] (f 2))
+
+(unbox a)
diff --git a/typed-racket-test/transient/manual/README.md b/typed-racket-test/transient/manual/README.md
new file mode 100644
index 00000000..2da6f649
--- /dev/null
+++ b/typed-racket-test/transient/manual/README.md
@@ -0,0 +1,6 @@
+manual
+===
+
+Tests that need to be manually inspected to see whether they pass.
+
+Read each file for instructions.
diff --git a/typed-racket-test/transient/manual/cdr.rkt b/typed-racket-test/transient/manual/cdr.rkt
new file mode 100644
index 00000000..cdec5930
--- /dev/null
+++ b/typed-racket-test/transient/manual/cdr.rkt
@@ -0,0 +1,16 @@
+#lang typed/racket/base #:transient
+
+;; Expand, and make sure no transient checks,
+;; because cdr applied to a list is OK
+
+(require racket/list racket/unsafe/ops)
+
+(define x0 : (Listof Symbol) '(A B C))
+(define x1 : (List Symbol Symbol) '(A B))
+
+(cdr x0)
+(cdr x1)
+(unsafe-cdr x0)
+(unsafe-cdr x1)
+
+;(rest (ann '(A . X) (Pairof Symbol Symbol)))
diff --git a/typed-racket-test/transient/manual/default-continuation-prompt-tag.rkt b/typed-racket-test/transient/manual/default-continuation-prompt-tag.rkt
new file mode 100644
index 00000000..560d54fc
--- /dev/null
+++ b/typed-racket-test/transient/manual/default-continuation-prompt-tag.rkt
@@ -0,0 +1,8 @@
+#lang typed/racket/base #:transient
+
+;; default-continuation-prompt-tag is separate from the base environment,
+;; so double-check that it does not get a codomain check
+;;
+;; to test, expand this module and make sure there's no "transient-assert"
+
+(default-continuation-prompt-tag)
diff --git a/typed-racket-test/transient/manual/for.rkt b/typed-racket-test/transient/manual/for.rkt
new file mode 100644
index 00000000..4a2a51cb
--- /dev/null
+++ b/typed-racket-test/transient/manual/for.rkt
@@ -0,0 +1,24 @@
+#lang typed/racket/base #:transient
+
+;; For combinators don't need a codomain check,
+;; or a domain check on the `for-loop` functions
+;;
+;; Expand, look for:
+;; - no "transient-assert" around the final result
+;; - no domain "transient-assert" for any functions
+;; - no transient-assert around unsafe-cdr
+
+(void?
+ (for ((x (in-list '(A B C))))
+ x))
+
+(list?
+ (for/list : (Listof Symbol) ((x '(A B C)))
+ x))
+
+(list?
+ (for/fold
+ ((acc : (Listof Symbol) '()))
+ ((x (in-list '(A B C))))
+ (cons x acc)))
+
diff --git a/typed-racket-test/transient/manual/nothing.rkt b/typed-racket-test/transient/manual/nothing.rkt
new file mode 100644
index 00000000..c8e5240b
--- /dev/null
+++ b/typed-racket-test/transient/manual/nothing.rkt
@@ -0,0 +1,14 @@
+#lang typed/racket/base #:transient
+
+;; type Nothing does not need a codomain check
+;;
+;; Expand this file, look for absence of "transient-assert"
+
+(module a racket/base
+ (provide f)
+ (define (f) (error 'die)))
+
+(require/typed 'a
+ (f (-> Nothing)))
+
+(f)
diff --git a/typed-racket-test/transient/manual/predicate.rkt b/typed-racket-test/transient/manual/predicate.rkt
new file mode 100644
index 00000000..12904ffa
--- /dev/null
+++ b/typed-racket-test/transient/manual/predicate.rkt
@@ -0,0 +1,18 @@
+#lang typed/racket/base #:transient
+
+;; List? should expand to a check for `list?`
+;; Vector? should expand to a check for `vector?`
+
+(define-type Big-T (List (Listof Integer) (List Symbol Integer Integer)))
+(define-predicate List? Big-T)
+
+(define-predicate Vector? (Vectorof Big-T))
+
+(: g (-> Any (U #f Big-T)))
+(define (g y)
+ (if (List? y)
+ y
+ #f))
+
+(void
+ (Vector? 4))
diff --git a/typed-racket-test/transient/manual/struct-predicate.rkt b/typed-racket-test/transient/manual/struct-predicate.rkt
new file mode 100644
index 00000000..bf567ecb
--- /dev/null
+++ b/typed-racket-test/transient/manual/struct-predicate.rkt
@@ -0,0 +1,19 @@
+#lang typed/racket/base #:transient
+
+;; Struct predicates don't need a typecheck
+;;
+;; Expand this file,
+;; make sure there are no transient-assert s
+
+(module a racket/base
+ (provide (struct-out a))
+ (struct a [x]))
+
+(require/typed 'a
+ (#:struct a ([x : Symbol])))
+
+(struct b ((y : Symbol)))
+
+(a? #f) ;; require/typed struct
+(b? #f) ;; TR struct
+(exn? #f) ;; builtin struct
diff --git a/typed-racket-test/transient/pass/alias.rkt b/typed-racket-test/transient/pass/alias.rkt
new file mode 100644
index 00000000..586da0cf
--- /dev/null
+++ b/typed-racket-test/transient/pass/alias.rkt
@@ -0,0 +1,9 @@
+#lang typed/racket/base #:transient
+
+;; Test trusted vs. untrusted primitives
+;; - + is a trusted identifier, its result is not checked
+;; - (begin +) is not a trusted identifier --- even though it evaluates to
+;; a function that could be trusted --- its result is checked
+
+(+ 2 2)
+((begin +) 2 2)
diff --git a/typed-racket-test/transient/pass/ann-inst.rkt b/typed-racket-test/transient/pass/ann-inst.rkt
new file mode 100644
index 00000000..4ce2fe35
--- /dev/null
+++ b/typed-racket-test/transient/pass/ann-inst.rkt
@@ -0,0 +1,6 @@
+#lang typed/racket/base #:transient
+
+;; Test the `ann` and `inst` forms
+
+((ann car (All (A B) (-> (Pairof A B) A))) '(A B))
+((inst car Symbol (Listof Symbol)) '(A B))
diff --git a/typed-racket-test/transient/pass/app-hetero.rkt b/typed-racket-test/transient/pass/app-hetero.rkt
new file mode 100644
index 00000000..70afdd1c
--- /dev/null
+++ b/typed-racket-test/transient/pass/app-hetero.rkt
@@ -0,0 +1,33 @@
+#lang racket/base
+(require rackunit)
+
+;; Test applications of `vector-ref` and `vector`, because these identifiers
+;; have special typing rules
+
+(module u racket/base
+ (provide f)
+ (define (f b)
+ ((vector-ref b 0) 2)))
+
+(module t typed/racket/base #:transient
+ (provide test1 test0)
+ (require/typed (submod ".." u)
+ (f (-> (Vector (-> String String)) Integer)))
+
+ (: q (-> String String))
+ (define (q n)
+ (string-append n n))
+
+ (define (test0)
+ (f (vector q)))
+
+ (define b (vector q))
+ (define (test1)
+ (f b)))
+(require 't)
+
+(check-exn #rx"transient-assert"
+ test0)
+
+(check-exn #rx"transient-assert"
+ test1)
diff --git a/typed-racket-test/transient/pass/apply.rkt b/typed-racket-test/transient/pass/apply.rkt
new file mode 100644
index 00000000..00d6f7f0
--- /dev/null
+++ b/typed-racket-test/transient/pass/apply.rkt
@@ -0,0 +1,6 @@
+#lang typed/racket/base #:transient
+
+;; Test that `(apply f ...)` does not check its result when `f` is a
+;; trusted function
+
+(void (apply string-append '("one" "two" "three")))
diff --git a/typed-racket-test/transient/pass/bad-vector-ref.rkt b/typed-racket-test/transient/pass/bad-vector-ref.rkt
new file mode 100644
index 00000000..8ad94fa9
--- /dev/null
+++ b/typed-racket-test/transient/pass/bad-vector-ref.rkt
@@ -0,0 +1,30 @@
+#lang racket/base
+
+;; Test applications of `vector-ref` that should fail due to mis-matched
+;; values and type constructors
+
+(module t typed/racket #:transient
+ (: f (-> (Vectorof Natural) Natural))
+ (define (f x)
+ (+ (vector-ref x 0)
+ (vector-ref x 1)))
+ (: g (-> (Vectorof (Vectorof Natural)) Natural))
+ (define (g x)
+ (define v (vector-ref x 0))
+ (+ (vector-ref (vector-ref x 0) 0) (vector-ref v 1)))
+ (: h (-> (Vector Natural Symbol) Natural))
+ (define (h x)
+ (vector-ref x 0))
+
+ (provide f g h))
+
+(require 't racket/contract rackunit)
+
+(check-exn #rx"transient-assert"
+ (λ () (f (vector 4 'A 4 4))))
+
+(check-exn #rx"transient-assert"
+ (λ () (g (vector 3))))
+
+(check-exn #rx"transient-assert"
+ (λ () (h (vector 1 'two 3))))
diff --git a/typed-racket-test/transient/pass/caar.rkt b/typed-racket-test/transient/pass/caar.rkt
new file mode 100644
index 00000000..24a534fa
--- /dev/null
+++ b/typed-racket-test/transient/pass/caar.rkt
@@ -0,0 +1,6 @@
+#lang typed/racket/base #:transient
+
+;; Test that nested elimination forms get checked
+
+(define (f)
+ (car (car '((1)))))
diff --git a/typed-racket-test/transient/pass/dead-code-values.rkt b/typed-racket-test/transient/pass/dead-code-values.rkt
new file mode 100644
index 00000000..9ec66487
--- /dev/null
+++ b/typed-racket-test/transient/pass/dead-code-values.rkt
@@ -0,0 +1,12 @@
+#lang typed/racket #:transient
+
+;; Test the 'values' case in defender/defender protect-codomain,
+;; ... application returns +1 results that need cod checks
+;; ... but also send the rewritten code through the optimizer
+
+(: forth-eval (-> Any Any (Values Symbol Symbol)))
+(define (forth-eval E S)
+ (match 'any
+ [(? pair? E+S)
+ ;; dead code
+ (values (car E+S) (cdr E+S))]))
diff --git a/typed-racket-test/transient/pass/define-syntax.rkt b/typed-racket-test/transient/pass/define-syntax.rkt
new file mode 100644
index 00000000..66c3b27a
--- /dev/null
+++ b/typed-racket-test/transient/pass/define-syntax.rkt
@@ -0,0 +1,12 @@
+#lang typed/racket/base #:transient
+
+;; Test that a simple macro works in locally-defensive code
+
+(define-syntax-rule (yo lo)
+ (+ lo lo))
+
+(: f (-> Integer Integer))
+(define (f x)
+ (yo (yo x)))
+
+(f 42)
diff --git a/typed-racket-test/transient/pass/distinguish-source.rkt b/typed-racket-test/transient/pass/distinguish-source.rkt
new file mode 100644
index 00000000..da4e3248
--- /dev/null
+++ b/typed-racket-test/transient/pass/distinguish-source.rkt
@@ -0,0 +1,29 @@
+#lang racket/base
+
+;; Test 3 kinds of typed functions:
+;; - a function defined by TR
+;; - a function imported through `require/typed`
+;; - a (safe) function from the standard library
+
+(module u racket/base
+ (provide f)
+ (define (f x)
+ x))
+
+(module t typed/racket/base #:transient
+ (require/typed (submod ".." u)
+ (f (-> (Listof String) (Listof Natural))))
+
+ (: g (-> Natural Boolean))
+ (define (g x)
+ (= x 4))
+
+ (define (test)
+ (filter g (f '("a" "bb" "ccc"))))
+
+ (provide test))
+(require 't rackunit)
+
+(check-exn (λ (e) (or (regexp-match? #rx"expected: Natural" (exn-message e))
+ (regexp-match? #rx"transient-assert" (exn-message e))))
+ test)
diff --git a/typed-racket-test/transient/pass/erasure-syntax.rkt b/typed-racket-test/transient/pass/erasure-syntax.rkt
new file mode 100644
index 00000000..b9aa0425
--- /dev/null
+++ b/typed-racket-test/transient/pass/erasure-syntax.rkt
@@ -0,0 +1,9 @@
+#lang racket/base
+
+(module a typed/racket/base #:erasure
+ (provide f)
+ (define-syntax-rule (f x)
+ (car (car x))))
+
+(require 'a)
+(f '((a) b c))
diff --git a/typed-racket-test/transient/pass/factorial.rkt b/typed-racket-test/transient/pass/factorial.rkt
new file mode 100644
index 00000000..60778fe3
--- /dev/null
+++ b/typed-racket-test/transient/pass/factorial.rkt
@@ -0,0 +1,10 @@
+#lang typed/racket #:transient
+
+;; Test factorial function, and the `for/product` combinator
+
+(: factorial (-> Natural Natural))
+(define (factorial x)
+ (for/product : Natural ([i : Natural (in-range x)])
+ (+ i 1)))
+
+(factorial 6)
diff --git a/typed-racket-test/transient/pass/flonum.rkt b/typed-racket-test/transient/pass/flonum.rkt
new file mode 100644
index 00000000..9f12f123
--- /dev/null
+++ b/typed-racket-test/transient/pass/flonum.rkt
@@ -0,0 +1,10 @@
+#lang typed/racket/base #:transient
+
+;; Test case-> type
+
+(require racket/flonum)
+
+(: flprobability? (case-> (Flonum -> Boolean) (Flonum Any -> Boolean)))
+(define (flprobability? p [log? #f])
+ (cond [log? (and (p . fl>= . -inf.0) (p . fl<= . 0.0))]
+ [else (and (p . fl>= . 0.0) (p . fl<= . 1.0))]))
diff --git a/typed-racket-test/transient/pass/for-array.rkt b/typed-racket-test/transient/pass/for-array.rkt
new file mode 100644
index 00000000..ccd914fa
--- /dev/null
+++ b/typed-racket-test/transient/pass/for-array.rkt
@@ -0,0 +1,18 @@
+#lang typed/racket #:transient
+
+;; Use 'for/array' and `array-shape`
+;; inspired by jpeg benchmark
+;;
+;; Must use both!
+
+(require
+ (only-in math/array for/array: for/array in-array array-shape Array))
+
+(: bg (-> (Array Symbol) Void))
+(define (bg mcu-array)
+ (void
+ ;; well this works ...
+ (for/array #:shape (vector-map (ann values (-> Index Integer)) (array-shape mcu-array))
+ ((mcu : Symbol (in-array mcu-array)))
+ (void))))
+
diff --git a/typed-racket-test/transient/pass/hello.rkt b/typed-racket-test/transient/pass/hello.rkt
new file mode 100644
index 00000000..39406e6b
--- /dev/null
+++ b/typed-racket-test/transient/pass/hello.rkt
@@ -0,0 +1,5 @@
+#lang typed/racket #:transient
+
+;; No-brainer test
+
+"hello world"
diff --git a/typed-racket-test/transient/pass/in-array.rkt b/typed-racket-test/transient/pass/in-array.rkt
new file mode 100644
index 00000000..1afca580
--- /dev/null
+++ b/typed-racket-test/transient/pass/in-array.rkt
@@ -0,0 +1,12 @@
+#lang typed/racket #:transient
+
+;; Use 'in-array'
+;; inspired by jpeg benchmark
+
+
+(require (only-in math/array in-array Array))
+
+(: read-dct-scan (-> (Array Integer) Void))
+(define (read-dct-scan dest)
+ (for ((mcu (in-array dest)))
+ (void)))
diff --git a/typed-racket-test/transient/pass/in-cycle.rkt b/typed-racket-test/transient/pass/in-cycle.rkt
new file mode 100644
index 00000000..51e7efe8
--- /dev/null
+++ b/typed-racket-test/transient/pass/in-cycle.rkt
@@ -0,0 +1,30 @@
+#lang typed/racket #:transient
+
+;; Plot error:
+;;
+;; /Users/ben/code/racket/fork/racket/share/pkgs/plot-lib/plot/private/plot3d/isosurface.rkt:130:23: Type Checker: No function domains matched in function application:
+;; Domains: Any (Sequenceof (Parameterof Plot-Pen-Style) Any)
+;; Any (Sequenceof (Parameterof Plot-Pen-Style))
+;; Any Integer
+;; Arguments: Any (Sequenceof Plot-Pen-Style)
+;; in: (in-cycle* line-styles)
+;;
+;; Try to reproduce ... failure so far (2019-08-22), but
+;; - error goes away if remove `rts` provides from the #%type-decl
+;; - error STAYS if remove only the unhygienic lookups
+;; so the problem is related to the new exports for the "contract + type" hack,
+;; and maybe by improving that we'll get a better fix
+;;
+;; Ok now we are simplified; the issue is a defined variable vs a for-loop variable
+
+(: in-cycle* (All (A) (-> (Sequenceof A) (Sequenceof A))))
+(define (in-cycle* s)
+ (define n (sequence-length s))
+ (if (zero? n) empty-sequence (in-cycle s)))
+
+(define xxx : String "hello")
+
+(: f (-> (Listof Symbol) Void))
+(define (f line-styles)
+ (for ([xxx (in-cycle* line-styles)])
+ (void)))
diff --git a/typed-racket-test/transient/pass/lambda.rkt b/typed-racket-test/transient/pass/lambda.rkt
new file mode 100644
index 00000000..c0595ec6
--- /dev/null
+++ b/typed-racket-test/transient/pass/lambda.rkt
@@ -0,0 +1,123 @@
+#lang typed/racket/base #:transient
+
+;; Test functions args, positional optional keyword rest
+
+;; -----------------------------------------------------------------------------
+;; --- positional
+
+(: f0 (-> Natural))
+(define (f0)
+ 4)
+
+(lambda () 0)
+
+
+(: f1 (-> Natural Natural))
+(define (f1 x)
+ (+ x 1))
+
+(lambda ((x : Natural))
+ (+ x 1))
+
+
+(: f2 (-> (Listof Natural) (Vectorof Natural) Natural))
+(define (f2 a b)
+ (+ (length a) (vector-length b)))
+
+(lambda ((a : (Listof Natural)) (b : (Vectorof Natural)))
+ (+ (length a) (vector-length b)))
+
+;; -----------------------------------------------------------------------------
+;; --- optional
+
+(: f3 (->* [(Listof Natural)] [(U #f Symbol)] Natural))
+(define (f3 a [b #f])
+ (+ (length a) (if b (string-length (symbol->string b)) 1)))
+
+(lambda ((a : (Listof Natural)) (b : (U #f Symbol) #f))
+ (+ (length a) (if b (string-length (symbol->string b)) 1)))
+
+(: f4 (->* [] [Integer (U #f Symbol)] Natural))
+(define (f4 [a -1] [b #f])
+ (+ (abs a) (if b (string-length (symbol->string b)) 1)))
+
+(lambda ([a : Integer -1] [b : (U #f Symbol) #f])
+ (+ (abs a) (if b (string-length (symbol->string b)) 1)))
+
+;; -----------------------------------------------------------------------------
+;; --- keyword
+
+(: f5 (-> #:a Symbol #:b (Listof Symbol) String))
+(define (f5 #:a a #:b b)
+ (if (null? b) "hello" "world"))
+
+(lambda (#:a (a : Symbol) #:b (b : (Listof Symbol)))
+ (if (null? b) "hello" "world"))
+
+(: f6 (->* [] [#:a Symbol #:b (Listof Symbol)] String))
+(define (f6 #:a [a 'a] #:b [b '(b b b)])
+ (if (= 3 (length b)) "one" "two"))
+
+(lambda (#:a [a : Symbol 'a] #:b [b : (Listof Symbol) '(b b b)])
+ (if (= 3 (length b)) "one" "two"))
+
+;; -----------------------------------------------------------------------------
+;; --- rest
+
+(: f7 (->* [] [] #:rest String String))
+(define (f7 . xs)
+ (if (null? xs)
+ "asdf"
+ (string-append (car xs) (cadr xs))))
+
+(f7)
+(f7 "a" "b")
+
+(ann
+ (lambda xs
+ (string-append (car xs) (cadr xs)))
+ (->* [] [] #:rest String String))
+
+;; -----------------------------------------------------------------------------
+;; --- misc
+
+(: choose-randomly (->* [ (Listof Symbol) Natural] [ #:random (U #f String)] String))
+(define (choose-randomly probabilities speed #:random (q #false))
+ (cond
+ [(string? q)
+ "string"]
+ [(not q)
+ "false"]
+ [else
+ "oh no something else"]))
+
+(choose-randomly '() 0 #:random "yes")
+(choose-randomly '() 0 #:random #false)
+(choose-randomly '() 0) ; this will error if keyword-arg functions are protected
+
+(define-type State Natural)
+(define-type Payoff Natural)
+(define-type Transition* (Listof Symbol))
+
+(struct automaton ({current : State}
+ {original : State}
+ {payoff : Payoff}
+ {table : Transition*}) #:transparent)
+
+(: make-random-automaton (-> Natural automaton))
+(define (make-random-automaton n)
+ (automaton n n n '()))
+
+;; -----------------------------------------------------------------------------
+;; --- kcfa
+
+(struct Exp ())
+
+(struct Call Exp ([a : Any] [b : Any] [c : Any]))
+
+(define (new-label)
+ 'aaa)
+
+(: make-call (-> Exp Exp * Exp))
+(define (make-call fun . args)
+ (Call (new-label) fun args))
diff --git a/typed-racket-test/transient/pass/list-ref.rkt b/typed-racket-test/transient/pass/list-ref.rkt
new file mode 100644
index 00000000..31a6a60c
--- /dev/null
+++ b/typed-racket-test/transient/pass/list-ref.rkt
@@ -0,0 +1,23 @@
+#lang typed/racket #:transient
+
+;; Test `list-ref` applications
+
+(: f (-> (Listof Natural) Natural))
+(define (f x)
+ (+ (car x)
+ (first x)))
+
+(f (list 4 4 4 4))
+
+(: g (-> (Listof (Listof Natural)) Natural))
+(define (g x)
+ (define l (list-ref x (+ 0 0)))
+ (+ (car l) (third l)))
+
+(g '((1 2 2 3 4)))
+
+(: h (-> (Pairof Natural Natural) Natural))
+(define (h x)
+ (+ (car x) (cdr x)))
+
+(h '(1 . 2))
diff --git a/typed-racket-test/transient/pass/ll-lambda.rkt b/typed-racket-test/transient/pass/ll-lambda.rkt
new file mode 100644
index 00000000..edf46562
--- /dev/null
+++ b/typed-racket-test/transient/pass/ll-lambda.rkt
@@ -0,0 +1,36 @@
+#lang racket/base
+
+;; Test tc-app lambda special case for ((lambda ...) ...)
+
+(module a typed/racket #:guarded
+ (: a Integer)
+ (: b (Listof Symbol))
+ (define-values [a b]
+ ((lambda ((x : Integer)) (values x (list 'A 'A))) 42)))
+
+(module r racket/base
+ (provide f)
+ (define (f x) (values x '(A A))))
+
+(module b typed/racket #:transient
+ (: x0 Integer)
+ (: x1 (Listof Symbol))
+ (define-values [x0 x1]
+ ((lambda ((x : Integer)) (values x (list 'A 'A))) 42))
+
+ (require/typed
+ (submod ".." r)
+ (f (-> Integer (Values Integer (Listof Symbol)))))
+
+ (: x2 Integer)
+ (: x3 (Listof Symbol))
+ (define-values [x2 x3]
+ ((lambda ((x : Integer)) (f x)) 42))
+
+ (: x4 Integer)
+ (: x5 (Listof Symbol))
+ (define-values [x4 x5]
+ (f 42))
+ )
+
+(require 'a 'b)
diff --git a/typed-racket-test/transient/pass/make-hasheq.rkt b/typed-racket-test/transient/pass/make-hasheq.rkt
new file mode 100644
index 00000000..4cd0445c
--- /dev/null
+++ b/typed-racket-test/transient/pass/make-hasheq.rkt
@@ -0,0 +1,5 @@
+#lang typed/racket/base #:transient
+
+;; Test the predicate for a mutable hashtable
+
+((begin make-hasheq))
diff --git a/typed-racket-test/transient/pass/match-define.rkt b/typed-racket-test/transient/pass/match-define.rkt
new file mode 100644
index 00000000..6d5585e5
--- /dev/null
+++ b/typed-racket-test/transient/pass/match-define.rkt
@@ -0,0 +1,11 @@
+#lang typed/racket #:transient
+
+;; Test that `match-define` works in locally-defensive code
+
+(struct foo ([x : Symbol]))
+
+(: g (-> foo Boolean))
+(define (g f)
+ (match-define (foo q) f)
+ (symbol=? q 'rrr))
+
diff --git a/typed-racket-test/transient/pass/module-client.rkt b/typed-racket-test/transient/pass/module-client.rkt
new file mode 100644
index 00000000..28826aea
--- /dev/null
+++ b/typed-racket-test/transient/pass/module-client.rkt
@@ -0,0 +1,25 @@
+#lang typed/racket/base #:transient
+
+;; Test:
+;; 1. enclosing module is locally-defensive
+;; 2. contains a Racket submodule
+;; 3. import a value with the right constructor & the wrong type
+;; 4. send the value back to untyped code, get low-level error from untyped
+
+(require "module-server.rkt" ) ;; import a typed function
+
+(: h (-> Real Real))
+(define (h n)
+ (* n n))
+
+(f 3 h)
+
+
+(module u racket/base
+ (provide xs)
+ (define xs '(A B C)))
+(require/typed 'u
+ (xs (Listof Natural)))
+
+(with-handlers ((exn:fail:contract? (lambda (_) #true)))
+ (filter zero? xs))
diff --git a/typed-racket-test/transient/pass/module-server.rkt b/typed-racket-test/transient/pass/module-server.rkt
new file mode 100644
index 00000000..dc04c952
--- /dev/null
+++ b/typed-racket-test/transient/pass/module-server.rkt
@@ -0,0 +1,9 @@
+#lang typed/racket/base #:transient
+
+;; Not a test, just provides a locally-defensive function
+
+(provide f filter)
+
+(: f (-> Real (-> Real Real) Real))
+(define (f r g)
+ (g (g r)))
diff --git a/typed-racket-test/transient/pass/poly-ref.rkt b/typed-racket-test/transient/pass/poly-ref.rkt
new file mode 100644
index 00000000..2afff263
--- /dev/null
+++ b/typed-racket-test/transient/pass/poly-ref.rkt
@@ -0,0 +1,11 @@
+#lang typed/racket/base #:transient
+
+;; Test that type variables do not have a run-time check
+;; (no need for a check, because a context cannot make assumptions about the value)
+
+(: f (All (A) (-> (Vectorof A) A)))
+(define (f x)
+ (vector-ref x 0))
+
+(f (vector 1 2 3))
+(f '#(four five six))
diff --git a/typed-racket-test/transient/pass/poly-require-typed.rkt b/typed-racket-test/transient/pass/poly-require-typed.rkt
new file mode 100644
index 00000000..a3161905
--- /dev/null
+++ b/typed-racket-test/transient/pass/poly-require-typed.rkt
@@ -0,0 +1,17 @@
+#lang racket/base
+
+;; Test require/typed with a polymorphic type
+
+(module util racket/base
+ (provide random-from)
+ (require racket/list)
+
+ (define (random-from xs)
+ (first (shuffle xs))))
+
+(module client typed/racket/base #:transient
+ (require/typed (submod ".." util)
+ (random-from (All (A) (-> (Listof A) A))))
+
+ (random-from '(1 2 3)))
+(require 'client)
diff --git a/typed-racket-test/transient/pass/poly-union.rkt b/typed-racket-test/transient/pass/poly-union.rkt
new file mode 100644
index 00000000..9681e1ba
--- /dev/null
+++ b/typed-racket-test/transient/pass/poly-union.rkt
@@ -0,0 +1,13 @@
+#lang typed/racket #:transient
+
+;; Test inspired by the suffixtree benchmark.
+;; Function returns a union of polymorphic variables and should have no check
+
+(: f (All (A B) (-> (-> A) (-> B) (U A B))))
+(define (f a b)
+ (: helper (-> Integer (U A B)))
+ (define (helper n)
+ (if (zero? n) (a) (b)))
+ (helper 0))
+
+(f (lambda () #true) (lambda () 'false))
diff --git a/typed-racket-test/transient/pass/primitives.rkt b/typed-racket-test/transient/pass/primitives.rkt
new file mode 100644
index 00000000..6889731b
--- /dev/null
+++ b/typed-racket-test/transient/pass/primitives.rkt
@@ -0,0 +1,9 @@
+#lang typed/racket #:transient
+
+;; Test trusted primitives
+
+(rest '(1 2 3))
+(apply + '(1 2 3))
+
+(struct foo ())
+(foo? 4)
diff --git a/typed-racket-test/transient/pass/provide-struct.rkt b/typed-racket-test/transient/pass/provide-struct.rkt
new file mode 100644
index 00000000..791057f3
--- /dev/null
+++ b/typed-racket-test/transient/pass/provide-struct.rkt
@@ -0,0 +1,24 @@
+#lang racket/base
+
+;; Test providing a struct (and its types)
+
+(module t typed/racket/base #:transient
+
+ (provide (struct-out foo) wepa)
+
+ (struct foo ((a : Natural)))
+
+ (define (wepa (f : foo))
+ (+ 1 (foo-a f))))
+
+(require 't rackunit)
+
+(check-pred values (foo 1))
+(check-pred values (foo 'a))
+
+(check-exn #rx"transient-assert"
+ (λ () (wepa (foo 'a))))
+
+(check-equal?
+ (foo-a (foo 'a))
+ 'a)
diff --git a/typed-racket-test/transient/pass/rec-factorial.rkt b/typed-racket-test/transient/pass/rec-factorial.rkt
new file mode 100644
index 00000000..b8d72d8a
--- /dev/null
+++ b/typed-racket-test/transient/pass/rec-factorial.rkt
@@ -0,0 +1,9 @@
+#lang typed/racket #:transient
+
+(: factorial (-> Natural Natural))
+(define (factorial n)
+ (if (zero? n)
+ 1
+ (* n (factorial (- n 1)))))
+
+(factorial 6)
diff --git a/typed-racket-test/transient/pass/scribble-example.rkt b/typed-racket-test/transient/pass/scribble-example.rkt
new file mode 100644
index 00000000..e10418f3
--- /dev/null
+++ b/typed-racket-test/transient/pass/scribble-example.rkt
@@ -0,0 +1,15 @@
+#lang racket/base
+
+(require scribble/example)
+
+(for ((the-eval (in-list (list
+ (make-base-eval #:lang 'typed/racket)
+ (make-base-eval '(require typed/racket))))))
+ (examples
+ #:label #f #:eval the-eval
+ (eval:error (define-predicate p? (All (A) (Listof A))))
+ (require/typed racket/base
+ [object-name (-> (U Struct-Type-Property Regexp)
+ (U String Bytes Symbol))])
+ (object-name #rx"a regexp")))
+
diff --git a/typed-racket-test/transient/pass/simple-object.rkt b/typed-racket-test/transient/pass/simple-object.rkt
new file mode 100644
index 00000000..facc2a79
--- /dev/null
+++ b/typed-racket-test/transient/pass/simple-object.rkt
@@ -0,0 +1,16 @@
+#lang typed/racket #:transient
+(require typed/rackunit)
+
+(define-type C% (Class (f (-> Integer Integer))))
+
+(define c% : C%
+ (class object%
+ (super-new)
+ (define/public (f x) (+ x 1))))
+
+(: g (-> (Vector (Instance C%)) Integer))
+(define (g vo)
+ (define o (vector-ref vo 0))
+ (send o f (send o f 2)))
+
+(check-equal? (g (vector (new c%))) 4)
diff --git a/typed-racket-test/transient/pass/struct.rkt b/typed-racket-test/transient/pass/struct.rkt
new file mode 100644
index 00000000..4bcd53fb
--- /dev/null
+++ b/typed-racket-test/transient/pass/struct.rkt
@@ -0,0 +1,19 @@
+#lang typed/racket #:transient
+
+;; Test structs: definition, creation, accessors
+
+(struct A ((x : Integer) (y : (Listof Integer)) (z : (-> Integer Integer))))
+
+(define a (A 1 '(1) (lambda ((x : Integer)) (+ x x))))
+
+(+ ((A-z a) (A-x a)) (car (A-y a)))
+
+((lambda (x) x) 3)
+
+
+(: f (-> (Listof A) Integer))
+(define (f x)
+ (define mya (car x))
+ (A-x mya))
+
+(f (list a))
diff --git a/typed-racket-test/transient/pass/submodule-list-0.rkt b/typed-racket-test/transient/pass/submodule-list-0.rkt
new file mode 100644
index 00000000..ffd2796c
--- /dev/null
+++ b/typed-racket-test/transient/pass/submodule-list-0.rkt
@@ -0,0 +1,12 @@
+#lang typed/racket/base #:transient
+
+;; Test importing a list
+
+(module u racket/base
+ (define x* (list 1))
+ (provide x*))
+
+(require/typed 'u
+ (x* (Listof Integer)))
+
+(+ (car x*) 1)
diff --git a/typed-racket-test/transient/pass/submodule-list-1.rkt b/typed-racket-test/transient/pass/submodule-list-1.rkt
new file mode 100644
index 00000000..c05210b2
--- /dev/null
+++ b/typed-racket-test/transient/pass/submodule-list-1.rkt
@@ -0,0 +1,12 @@
+#lang typed/racket/base #:transient
+
+;; Test importing a list with incorrect type
+
+(module u racket/base
+ (define x* (list "NaN"))
+ (provide x*))
+
+(require/typed 'u
+ (x* (Listof Integer)))
+
+(ann (append x* (list 1 2 3)) (Listof Integer))
diff --git a/typed-racket-test/transient/pass/submodule-struct-0.rkt b/typed-racket-test/transient/pass/submodule-struct-0.rkt
new file mode 100644
index 00000000..cebb9bdd
--- /dev/null
+++ b/typed-racket-test/transient/pass/submodule-struct-0.rkt
@@ -0,0 +1,14 @@
+#lang typed/racket #:transient
+
+;; Test importing a struct
+
+(module u racket/base
+ (struct posn [x y])
+ (define origin (posn 0 0))
+ (provide origin (struct-out posn)))
+
+(require/typed 'u
+ (#:struct posn ((x : Real) (y : Real)))
+ (origin posn))
+
+(+ (posn-x origin) (posn-y origin))
diff --git a/typed-racket-test/transient/pass/submodule-transient.rkt b/typed-racket-test/transient/pass/submodule-transient.rkt
new file mode 100644
index 00000000..908eb39c
--- /dev/null
+++ b/typed-racket-test/transient/pass/submodule-transient.rkt
@@ -0,0 +1,16 @@
+#lang typed/racket/base #:transient
+
+;; LD submodules in LD code
+
+(module t typed/racket/base #:transient
+ (: f (-> Real (-> Real Real) Real))
+ (define (f r g)
+ (g (g r)))
+ (provide f))
+(require 't)
+
+(: h (-> Real Real))
+(define (h n)
+ (* n n))
+
+(f 3 h)
diff --git a/typed-racket-test/transient/pass/submodule.rkt b/typed-racket-test/transient/pass/submodule.rkt
new file mode 100644
index 00000000..c7bd0164
--- /dev/null
+++ b/typed-racket-test/transient/pass/submodule.rkt
@@ -0,0 +1,12 @@
+#lang typed/racket/base #:transient
+
+;; Test importing a flat value
+
+(module u racket/base
+ (define x 3)
+ (provide x))
+
+(require/typed 'u
+ (x Byte))
+
+(+ x 1)
diff --git a/typed-racket-test/transient/pass/tc-app-list.rkt b/typed-racket-test/transient/pass/tc-app-list.rkt
new file mode 100644
index 00000000..81a18fa5
--- /dev/null
+++ b/typed-racket-test/transient/pass/tc-app-list.rkt
@@ -0,0 +1,20 @@
+#lang typed/racket/base #:transient
+
+;; Test special-cases in tc-app-list
+
+(list* '(1 2 3))
+
+(ann (reverse '(1 2 3)) (Listof Natural))
+(ann (reverse '(1 2 3)) (List Natural Natural Natural))
+(reverse '(1 2 3))
+(lambda ((xs : (Listof Natural)))
+ (reverse xs))
+(lambda ((xs : (Pairof Integer (Listof Integer))))
+ (reverse xs))
+
+(: main (-> String Void))
+(define (main filename)
+ (define raw (with-input-from-file filename read))
+ (if (list? raw)
+ (void (ann (reverse raw) (Listof Any)))
+ (error "bad input")))
diff --git a/typed-racket-test/transient/pass/tc-app-special.rkt b/typed-racket-test/transient/pass/tc-app-special.rkt
new file mode 100644
index 00000000..e39711e8
--- /dev/null
+++ b/typed-racket-test/transient/pass/tc-app-special.rkt
@@ -0,0 +1,6 @@
+#lang typed/racket/base #:transient
+
+;; Test `call-with-values` because it has a special typing rule
+
+(call-with-values (lambda () '42) (lambda ((n : Real)) (+ n 1)))
+(call-with-values (lambda () (values 1 42)) (lambda ((n : Real) (m : Real)) (+ n m)))
diff --git a/typed-racket-test/transient/pass/transient-provide.rkt b/typed-racket-test/transient/pass/transient-provide.rkt
new file mode 100644
index 00000000..3b5f9802
--- /dev/null
+++ b/typed-racket-test/transient/pass/transient-provide.rkt
@@ -0,0 +1,12 @@
+#lang racket/base
+
+;; Test providing value to untyped
+
+(module a typed/racket/base #:transient
+ (provide f)
+ (define (f (x : (Boxof Integer)))
+ (unbox x)))
+
+(require 'a rackunit)
+(check-exn #rx"transient-assert"
+ (lambda () (f 0)))
diff --git a/typed-racket-test/transient/pass/transient-syntax.rkt b/typed-racket-test/transient/pass/transient-syntax.rkt
new file mode 100644
index 00000000..7ddd1305
--- /dev/null
+++ b/typed-racket-test/transient/pass/transient-syntax.rkt
@@ -0,0 +1,9 @@
+#lang racket/base
+
+(module a typed/racket/base #:transient
+ (provide f)
+ (define-syntax-rule (f x)
+ (car (car x))))
+
+(require 'a)
+(f '((a) b c))
diff --git a/typed-racket-test/transient/pass/typed-provide.rkt b/typed-racket-test/transient/pass/typed-provide.rkt
new file mode 100644
index 00000000..e3d2fb11
--- /dev/null
+++ b/typed-racket-test/transient/pass/typed-provide.rkt
@@ -0,0 +1,28 @@
+#lang racket/base
+
+;; Test providing a value to an untyped context
+
+(module a typed/racket/base
+ (provide f)
+ (define (f (x : (Boxof (Boxof Integer))))
+ (unbox (unbox x))))
+
+(module b racket/base
+ (provide bbx)
+ (define bbx (box 0)))
+
+(module c typed/racket/base #:transient
+ (require (submod ".." a))
+ (require/typed (submod ".." b) (bbx (Boxof (Boxof Integer))))
+ (provide do-c bbx)
+ (define (do-c)
+ (f bbx)))
+
+(require 'a rackunit)
+(check-exn #rx"f: contract violation"
+ (lambda () (f 0)))
+
+(require 'c)
+(check-not-exn (lambda () (unbox bbx)))
+(check-exn #rx"f: contract violation"
+ do-c)
diff --git a/typed-racket-test/transient/pass/typed-untyped-id.rkt b/typed-racket-test/transient/pass/typed-untyped-id.rkt
new file mode 100644
index 00000000..121d0337
--- /dev/null
+++ b/typed-racket-test/transient/pass/typed-untyped-id.rkt
@@ -0,0 +1,27 @@
+#lang racket/base
+
+;; TODO 2020-02-21 remove the require/typed in the client,
+;; add a Transient case to typed/untyped id
+
+(module a racket/base
+ (require racket/contract)
+ (provide
+ (contract-out [f0 (-> symbol? symbol?)]))
+ (define (f0 x) 'a))
+
+(module b typed/racket/base
+ (provide f1)
+ (define (f1 (x : Symbol)) : Symbol 'a))
+
+(module c racket/base
+ (require (submod ".." a) (submod ".." b) typed/untyped-utils)
+ (define-typed/untyped-identifier f f1 f0)
+ (provide f))
+
+(module d typed/racket/base #:transient
+ ;; fail = (require (submod ".." c))
+ (require/typed (submod ".." c)
+ (f (-> Symbol Symbol)))
+ f)
+
+(require 'd)
diff --git a/typed-racket-test/transient/pass/untyped-contract-aux/lib.rkt b/typed-racket-test/transient/pass/untyped-contract-aux/lib.rkt
new file mode 100644
index 00000000..b9786863
--- /dev/null
+++ b/typed-racket-test/transient/pass/untyped-contract-aux/lib.rkt
@@ -0,0 +1,7 @@
+#lang typed/racket
+
+(provide f)
+
+(: f (-> (U Symbol String) Void))
+(define (f x)
+ (void))
diff --git a/typed-racket-test/transient/pass/untyped-contract-aux/untyped.rkt b/typed-racket-test/transient/pass/untyped-contract-aux/untyped.rkt
new file mode 100644
index 00000000..da800456
--- /dev/null
+++ b/typed-racket-test/transient/pass/untyped-contract-aux/untyped.rkt
@@ -0,0 +1,10 @@
+#lang racket/base
+
+(require
+ typed/racket/base
+ typed/untyped-utils)
+
+(require/untyped-contract "lib.rkt"
+ (f (-> Symbol Void)))
+
+(provide f)
diff --git a/typed-racket-test/transient/pass/untyped-contract-guarded.rkt b/typed-racket-test/transient/pass/untyped-contract-guarded.rkt
new file mode 100644
index 00000000..3cf86c13
--- /dev/null
+++ b/typed-racket-test/transient/pass/untyped-contract-guarded.rkt
@@ -0,0 +1,9 @@
+#lang typed/racket
+
+;; Identifier imported from untyped-contract should have original type,
+;; not the type for the refined contract
+
+(require "untyped-contract-aux/untyped.rkt")
+
+(define (g (z : (U Symbol String))) : Void
+ (f z))
diff --git a/typed-racket-test/transient/pass/untyped-contract-transient.rkt b/typed-racket-test/transient/pass/untyped-contract-transient.rkt
new file mode 100644
index 00000000..4966e52b
--- /dev/null
+++ b/typed-racket-test/transient/pass/untyped-contract-transient.rkt
@@ -0,0 +1,12 @@
+#lang typed/racket #:transient
+
+;; Identifier imported from untyped-contract stuck with refined type
+;; in a transient context.
+;; Need to deal with that refined type .... funny
+
+(require "untyped-contract-aux/untyped.rkt")
+
+(define (g (z : (U Symbol String))) : Void
+ ;; (f z) = type error
+ (f (assert z symbol?)))
+
diff --git a/typed-racket-test/transient/pass/vector-ref.rkt b/typed-racket-test/transient/pass/vector-ref.rkt
new file mode 100644
index 00000000..ee94bd51
--- /dev/null
+++ b/typed-racket-test/transient/pass/vector-ref.rkt
@@ -0,0 +1,23 @@
+#lang typed/racket #:transient
+
+;; Test successful vector-ref operations
+
+(: f (-> (Vectorof Natural) Natural))
+(define (f x)
+ (+ (vector-ref x 0)
+ (vector-ref x 1)))
+
+(f (vector 4 4 4 4))
+
+(: g (-> (Vectorof (Vectorof Natural)) Natural))
+(define (g x)
+ (define v (vector-ref x 0))
+ (+ (vector-ref (vector-ref x 0) 0) (vector-ref v 1)))
+
+(g (vector (vector 1 2 2 3 4)))
+
+(: h (-> (Vector Natural Symbol) Natural))
+(define (h x)
+ (vector-ref x 0))
+
+(h (vector 1 'asdf))
diff --git a/typed-racket-test/transient/pass/with-input-from-file.rkt b/typed-racket-test/transient/pass/with-input-from-file.rkt
new file mode 100644
index 00000000..c46de7a5
--- /dev/null
+++ b/typed-racket-test/transient/pass/with-input-from-file.rkt
@@ -0,0 +1,8 @@
+#lang typed/racket/base #:transient
+
+;; Test 'with-input-from-file'
+
+(: main (-> Path-String Void))
+(define (main filename)
+ (define q (with-input-from-file filename (lambda () (read))))
+ (void))
diff --git a/typed-racket-test/transient/pass/with-type-guarded.rkt b/typed-racket-test/transient/pass/with-type-guarded.rkt
new file mode 100644
index 00000000..480777cf
--- /dev/null
+++ b/typed-racket-test/transient/pass/with-type-guarded.rkt
@@ -0,0 +1,8 @@
+#lang racket/base
+
+(require (only-in typed/racket/base with-type String))
+
+(let ([x "hello"])
+ (with-type #:result String
+ #:freevars ([x String])
+ (string-append x " world")))
diff --git a/typed-racket-test/unit-tests/static-contract-instantiate-tests.rkt b/typed-racket-test/unit-tests/static-contract-instantiate-tests.rkt
index 3ec7c172..8e65411f 100644
--- a/typed-racket-test/unit-tests/static-contract-instantiate-tests.rkt
+++ b/typed-racket-test/unit-tests/static-contract-instantiate-tests.rkt
@@ -5,6 +5,7 @@
(require "test-utils.rkt" "evaluator.rkt"
rackunit
+ (except-in racket/class private)
(for-syntax
syntax/parse
racket/base
@@ -41,4 +42,13 @@
(let ([vector-1 (sc->contract (vector-length/sc 1))])
(check-true (vector-1 '#(1)))
(check-false (vector-1 '#()))
- (check-false (vector-1 '())))))
+ (check-false (vector-1 '())))
+ (let* ((chk-cls-0 (sc->contract (make-class-shape/sc '((i . t)) '((f . t)) '((p . t)) '((a . t)))))
+ (pre-cls (class object% (super-new) (define/pubment (a x) 42)))
+ (cls-0 (class pre-cls (super-new) (init i) (field (f 0)) (define/public (p x) (void)) (define/augment (a x) (void)))))
+ (check-true (chk-cls-0 cls-0))
+ (check-false (chk-cls-0 (class object% (super-new)))))
+ (let ((obj-0 (sc->contract (make-object-shape/sc '(f) '(m)))))
+ (check-true (obj-0 (new (class object% (super-new) (field (f 0)) (define/public (m x) (void))))))
+ (check-false (obj-0 (new (class object% (super-new) (field (f 0)))))))
+ ))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment