Skip to content

Commit de6c605

Browse files
committed
static-contracts: improve optimizer's test for flat scs
* Add `instantiate/optimize` to the static contracts API (new function in `instantiate.rkt`) * Add optional kwd arg `#:recursive-kinds` to sc optimizer * SC optimizer uses recursive kinds to tell if a `name/sc` or `recursive-sc` will generate a flat contract * `instantiate/optimize` - solves for a recursive kinds table - calls `optimize` with the table - calls `instantiate` with the same table
1 parent 26f65f1 commit de6c605

File tree

4 files changed

+77
-26
lines changed

4 files changed

+77
-26
lines changed

typed-racket-lib/typed-racket/private/type-contract.rkt

Lines changed: 7 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@
1717
racket/format
1818
syntax/flatten-begin
1919
(only-in (types abbrev) -Bottom -Boolean)
20-
(static-contracts instantiate optimize structures combinators constraints)
20+
(static-contracts instantiate structures combinators constraints)
2121
(only-in (submod typed-racket/static-contracts/instantiate internals) compute-constraints)
2222
;; TODO make this from contract-req
2323
(prefix-in c: racket/contract)
@@ -287,15 +287,14 @@
287287
#:sc-cache [sc-cache (make-hash)])
288288
(let/ec escape
289289
(define (fail #:reason [reason #f]) (escape (init-fail #:reason reason)))
290-
(instantiate
291-
(optimize
292-
(type->static-contract ty #:typed-side typed-side fail
293-
#:cache sc-cache)
294-
#:trusted-positive typed-side
295-
#:trusted-negative (not typed-side))
290+
(instantiate/optimize
291+
(type->static-contract ty #:typed-side typed-side fail
292+
#:cache sc-cache)
296293
fail
297294
kind
298-
#:cache cache)))
295+
#:cache cache
296+
#:trusted-positive typed-side
297+
#:trusted-negative (not typed-side))))
299298

300299
(define any-wrap/sc (chaperone/sc #'any-wrap/c))
301300

typed-racket-lib/typed-racket/static-contracts/instantiate.rkt

Lines changed: 19 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@
1515
"combinators/case-lambda.rkt"
1616
"combinators/parametric.rkt"
1717
"kinds.rkt"
18+
"optimize.rkt"
1819
"parametric-check.rkt"
1920
"structures.rkt"
2021
"constraints.rkt"
@@ -23,33 +24,46 @@
2324
(provide static-contract-may-contain-free-ids?)
2425

2526
(provide/cond-contract
27+
[instantiate/optimize
28+
(parametric->/c (a) ((static-contract? (-> #:reason (or/c #f string?) a))
29+
(contract-kind? #:cache hash? #:trusted-positive boolean? #:trusted-negative boolean?)
30+
. ->* . (or/c a (list/c (listof syntax?) syntax?))))]
2631
[instantiate
2732
(parametric->/c (a) ((static-contract? (-> #:reason (or/c #f string?) a))
28-
(contract-kind? #:cache hash?)
33+
(contract-kind? #:cache hash? #:recursive-kinds #f)
2934
. ->* . (or/c a (list/c (listof syntax?) syntax?))))]
3035
[should-inline-contract? (-> syntax? boolean?)])
3136

32-
3337
;; Providing these so that tests can work directly with them.
3438
(module* internals #f
3539
(provide compute-constraints
3640
compute-recursive-kinds
3741
instantiate/inner))
3842

43+
(define (instantiate/optimize sc fail [kind 'impersonator] #:cache [cache #f] #:trusted-positive [trusted-positive #f] #:trusted-negative [trusted-negative #f])
44+
(define recursive-kinds
45+
(with-handlers [(exn:fail:constraint-failure?
46+
(lambda (exn) (fail #:reason (exn:fail:constraint-failure-reason exn))))]
47+
(compute-recursive-kinds
48+
(contract-restrict-recursive-values (compute-constraints sc kind)))))
49+
(define sc/opt (optimize sc #:trusted-positive trusted-positive #:trusted-negative trusted-negative #:recursive-kinds recursive-kinds))
50+
(instantiate sc/opt fail kind #:cache cache #:recursive-kinds recursive-kinds))
51+
3952
;; kind is the greatest kind of contract that is supported, if a greater kind would be produced the
4053
;; fail procedure is called.
4154
;;
4255
;; The cache is used to share contract definitions across multiple calls to
4356
;; type->contract in a given contract fixup pass. If it's #f then that means don't
4457
;; do any sharing (useful for testing).
45-
(define (instantiate sc fail [kind 'impersonator] #:cache [cache #f])
58+
(define (instantiate sc fail [kind 'impersonator] #:cache [cache #f] #:recursive-kinds [recursive-kinds #f])
4659
(if (parametric-check sc)
4760
(fail #:reason "multiple parametric contracts are not supported")
4861
(with-handlers [(exn:fail:constraint-failure?
4962
(lambda (exn) (fail #:reason (exn:fail:constraint-failure-reason exn))))]
5063
(instantiate/inner sc
51-
(compute-recursive-kinds
52-
(contract-restrict-recursive-values (compute-constraints sc kind)))
64+
(or recursive-kinds
65+
(compute-recursive-kinds
66+
(contract-restrict-recursive-values (compute-constraints sc kind))))
5367
cache))))
5468

5569
;; computes the definitions that are in / used by `sc`

typed-racket-lib/typed-racket/static-contracts/optimize.rkt

Lines changed: 29 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@
1717

1818

1919
(provide/cond-contract
20-
[optimize ((static-contract?) (#:trusted-positive boolean? #:trusted-negative boolean?)
20+
[optimize ((static-contract?) (#:trusted-positive boolean? #:trusted-negative boolean? #:recursive-kinds hash?)
2121
. ->* . static-contract?)])
2222

2323
;; Reduce a static contract to a smaller simpler one that protects in the same way
@@ -110,25 +110,22 @@
110110

111111

112112
;; Reduce a static contract assuming that we trusted the current side
113-
(define (trusted-side-reduce sc)
113+
(define ((make-trusted-side-reduce flat-sc?) sc)
114114
(match sc
115115
[(->/sc: mand-args opt-args mand-kw-args opt-kw-args rest-arg (list (any/sc:) ...))
116116
(function/sc #t mand-args opt-args mand-kw-args opt-kw-args rest-arg #f)]
117117
[(arr/sc: args rest (list (any/sc:) ...))
118118
(arr/sc args rest #f)]
119119
[(none/sc:) any/sc]
120-
[(or/sc: (? flat-terminal-kind?) ...) any/sc]
121-
[(? flat-terminal-kind?) any/sc]
120+
[(or/sc: (? flat-sc?) ...) any/sc]
121+
[(? flat-sc?) any/sc]
122122
[(syntax/sc: (? recursive-sc?))
123123
;;bg; _temporary_ case to allow contracts from the `Syntax` type.
124124
;; This is temporary until TR has types for immutable-vector
125125
;; and box-immutable & changes the definition of the `Syntax` type.
126126
any/sc]
127127
[else sc]))
128128

129-
(define (flat-terminal-kind? sc)
130-
(eq? 'flat (sc-terminal-kind sc)))
131-
132129
;; The side of a static contract describes the source of the values that
133130
;; the contract needs to check.
134131
;; - 'positive : values exported by the server module
@@ -176,12 +173,13 @@
176173
;; update-side : sc? weak-side? -> weak-side?
177174
;; Change the current side to something safe & strong-as-possible
178175
;; for optimizing the sub-contracts of the given `sc`.
179-
(define (update-side sc side)
176+
(define ((make-update-side flat-sc?) sc side)
180177
(match sc
181178
[(or/sc: scs ...)
182-
#:when (not (andmap flat-terminal-kind? scs))
179+
#:when (not (andmap flat-sc? scs))
183180
(weaken-side side)]
184-
[(? guarded-sc?)
181+
[_
182+
#:when (guarded-sc? sc)
185183
(strengthen-side side)]
186184
[_
187185
;; Keep same side by default.
@@ -194,8 +192,7 @@
194192
;; type constructor. E.g. list/sc is "real" and or/sc is not.
195193
(define (guarded-sc? sc)
196194
(match sc
197-
[(or (? flat-terminal-kind?)
198-
(->/sc: _ _ _ _ _ _)
195+
[(or (->/sc: _ _ _ _ _ _)
199196
(arr/sc: _ _ _)
200197
(async-channel/sc: _)
201198
(box/sc: _)
@@ -292,9 +289,28 @@
292289
(sc-map sc trim)]))
293290
(trim sc 'covariant))
294291

292+
(define (make-sc->kind recursive-kinds)
293+
(if recursive-kinds
294+
(λ (sc)
295+
(let loop ([sc sc])
296+
(match sc
297+
[(recursive-sc _ _ body)
298+
(loop body)]
299+
[(or (recursive-sc-use id)
300+
(name/sc: id))
301+
(hash-ref recursive-kinds id #f)]
302+
[_
303+
(sc-terminal-kind sc)])))
304+
sc-terminal-kind))
295305

296306
;; If we trust a specific side then we drop all contracts protecting that side.
297-
(define (optimize sc #:trusted-positive [trusted-positive #f] #:trusted-negative [trusted-negative #f])
307+
(define (optimize sc #:trusted-positive [trusted-positive #f] #:trusted-negative [trusted-negative #f] #:recursive-kinds [recursive-kinds #f])
308+
(define flat-sc?
309+
(let ([sc->kind (make-sc->kind recursive-kinds)])
310+
(λ (sc) (eq? 'flat (sc->kind sc)))))
311+
(define trusted-side-reduce (make-trusted-side-reduce flat-sc?))
312+
(define update-side (make-update-side flat-sc?))
313+
298314
;; single-step: reduce and trusted-side-reduce if appropriate
299315
(define (single-step sc maybe-weak-side)
300316
(define trusted
Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
#lang racket/base
2+
3+
;; Test that the `Spec` type can be converted to a contract that
4+
;; successfully **runs**
5+
6+
(module t typed/racket/base
7+
(provide f g)
8+
9+
(define-type Spec
10+
(-> (U Spec String)))
11+
12+
(: f (-> Spec))
13+
(define (f)
14+
(λ () "hello"))
15+
16+
(: g (-> (Rec T (-> (U T String)))))
17+
(define (g)
18+
(λ () "hello")))
19+
20+
(require 't)
21+
22+
(void f g)

0 commit comments

Comments
 (0)