|
239 | 239 | (define (change-contract-fixups forms [ctc-cache (make-hash)]) |
240 | 240 | (with-new-name-tables |
241 | 241 | (for/list ((e (in-list forms))) |
242 | | - (if (not (has-contract-def-property? e)) |
243 | | - e |
244 | | - (begin (set-box! include-extra-requires? #t) |
245 | | - (generate-contract-def e ctc-cache)))))) |
| 242 | + (cond |
| 243 | + [(not (has-contract-def-property? e)) e] |
| 244 | + [else |
| 245 | + (set-box! include-extra-requires? #t) |
| 246 | + (generate-contract-def e ctc-cache)])))) |
246 | 247 |
|
247 | 248 | ;; TODO: These are probably all in a specific place, which could avoid |
248 | 249 | ;; the big traversal |
|
386 | 387 | (loop t (flip-side typed-side) recursive-values)) |
387 | 388 | (define (t->sc/both t #:recursive-values (recursive-values recursive-values)) |
388 | 389 | (loop t 'both recursive-values)) |
389 | | - (define (t->sc/fun t #:maybe-existential [opt-exi #f]) (t->sc/function t fail typed-side recursive-values loop #f #:maybe-existential opt-exi)) |
390 | | - (define (t->sc/meth t) (t->sc/method t fail typed-side recursive-values loop)) |
| 390 | + (define (t->sc/meth t) |
| 391 | + (t->sc/method t fail typed-side recursive-values loop)) |
391 | 392 |
|
392 | 393 | (define (struct->recursive-sc name-base key flds sc-ctor) |
393 | 394 | (define key* (generate-temporary name-base)) |
|
554 | 555 | ;; Avoid putting (-> any T) contracts on struct predicates (where Boolean <: T) |
555 | 556 | ;; Optimization: if the value is typed, we can assume it's not wrapped |
556 | 557 | ;; in a type-unsafe chaperone/impersonator and use the unsafe contract |
557 | | - (let* ([unsafe-spp/sc (flat/sc #'struct-predicate-procedure?)] |
558 | | - [safe-spp/sc (flat/sc #'struct-predicate-procedure?/c)] |
559 | | - [optimized/sc (if (from-typed? typed-side) |
560 | | - unsafe-spp/sc |
561 | | - safe-spp/sc)] |
562 | | - [spt-pred-procedure?/sc (flat/sc #'struct-type-property-predicate-procedure?)]) |
563 | | - (or/sc optimized/sc spt-pred-procedure?/sc (t->sc/fun t)))] |
| 558 | + (define unsafe-spp/sc (flat/sc #'struct-predicate-procedure?)) |
| 559 | + (define safe-spp/sc (flat/sc #'struct-predicate-procedure?/c)) |
| 560 | + (define optimized/sc (if (from-typed? typed-side) unsafe-spp/sc safe-spp/sc)) |
| 561 | + (define spt-pred-procedure?/sc (flat/sc #'struct-type-property-predicate-procedure?)) |
| 562 | + (or/sc optimized/sc spt-pred-procedure?/sc (t->sc/fun t))] |
564 | 563 | [(? Fun? t) (t->sc/fun t)] |
565 | 564 | [(? DepFun? t) (t->sc/fun t)] |
566 | 565 | [(Set: t) (set/sc (t->sc t))] |
|
835 | 834 | [else (is-flat-type/sc (obj->sc o) sc)])] |
836 | 835 | [(NotTypeProp: o t) |
837 | 836 | (define sc (t->sc t bound-all-vars)) |
838 | | - (cond |
839 | | - [(not (equal? flat-sym (get-max-contract-kind sc))) |
840 | | - (raise-user-error 'type->static-contract/shallow "proposition contract generation not supported for non-flat types")] |
841 | | - [else (not-flat-type/sc (obj->sc o) sc)])] |
| 837 | + (unless (equal? flat-sym (get-max-contract-kind sc)) |
| 838 | + (raise-user-error 'type->static-contract/shallow |
| 839 | + "proposition contract generation not supported for non-flat types")) |
| 840 | + (not-flat-type/sc (obj->sc o) sc)] |
842 | 841 | [(LeqProp: (app obj->sc lhs) (app obj->sc rhs)) |
843 | 842 | (leq/sc lhs rhs)] |
844 | 843 | [(AndProp: ps) |
|
1136 | 1135 | (define (t->sc/function f fail typed-side recursive-values loop method? #:maybe-existential [opt-exi #f]) |
1137 | 1136 | (define (t->sc t #:recursive-values (recursive-values recursive-values)) |
1138 | 1137 | (loop t typed-side recursive-values)) |
1139 | | - (define (t->sc/neg t #:recursive-values (recursive-values recursive-values)) |
1140 | | - (loop t (flip-side typed-side) recursive-values)) |
1141 | | - |
1142 | 1138 | (define (arr-params->exist/sc exi dom rst kw rng prop+type) |
1143 | 1139 | (define (occur? t) |
1144 | | - (if (or (not t) (empty? t)) #f |
| 1140 | + (if (or (not t) (empty? t)) |
| 1141 | + #f |
1145 | 1142 | (set-member? (free-vars-names (free-vars* t)) exi))) |
1146 | | - |
| 1143 | + |
1147 | 1144 | (match* (rng prop+type) |
1148 | 1145 | [((Fun: (list (Arrow: (list-rest (F: n1) a ... _) rst_i kw_i _))) (F: n1)) |
1149 | | - #:when (and (not (ormap occur? (list rst kw rst_i kw_i))) |
1150 | | - (eq? n1 exi)) |
| 1146 | + #:when (and (not (ormap occur? (list rst kw rst_i kw_i))) (eq? n1 exi)) |
1151 | 1147 | (void)] |
1152 | | - [(_ _) (fail #:reason |
1153 | | - "contract generation only supports Some Type in this form: (Some (X) (-> ty1 ... (-> X ty ... ty2) : X)) or (-> ty1 ... (Some (X) (-> X ty ... ty2) : X))")]) |
1154 | | - |
| 1148 | + [(_ _) |
| 1149 | + (fail |
| 1150 | + #:reason |
| 1151 | + "contract generation only supports Some Type in this form: (Some (X) (-> ty1 ... (-> X ty ... ty2) : X)) or (-> ty1 ... (Some (X) (-> X ty ... ty2) : X))")]) |
| 1152 | + |
1155 | 1153 | (define/with-syntax name exi) |
1156 | 1154 | (define lhs (t->sc/neg dom)) |
1157 | 1155 | (define eq-name (flat/sc #'(eq/c name))) |
1158 | | - (define rhs (t->sc rng |
1159 | | - #:recursive-values (hash-set recursive-values exi |
1160 | | - (same eq-name)))) |
| 1156 | + (define rhs (t->sc rng #:recursive-values (hash-set recursive-values exi (same eq-name)))) |
1161 | 1157 | (exist/sc (list #'name) lhs rhs)) |
1162 | 1158 |
|
1163 | 1159 |
|
1164 | 1160 | ;; handle-arrow-range : Arr (-> Static-Contact) -> Static-Contract |
1165 | 1161 | ;; Match the range of an arr and determine if a contract can be generated |
1166 | 1162 | ;; and call the given thunk or raise an error |
1167 | 1163 | (define (handle-arrow-range arrow proceed) |
1168 | | - (match arrow |
1169 | | - [(or (Arrow: _ _ _ rng) |
1170 | | - (DepFun: _ _ rng)) |
1171 | | - (handle-range rng proceed)])) |
| 1164 | + (match-define (or (Arrow: _ _ _ rng) (DepFun: _ _ rng)) arrow) |
| 1165 | + (handle-range rng proceed)) |
1172 | 1166 | (define (handle-range rng proceed) |
1173 | 1167 | (match rng |
1174 | 1168 | [(Values: (list (Result: _ |
|
1267 | 1261 | (when (and (not (empty? kws))) |
1268 | 1262 | (fail #:reason (~a "cannot generate contract for case function type" |
1269 | 1263 | " with optional keyword arguments"))) |
1270 | | - (when (ormap (lambda (n-exi) |
1271 | | - (> n-exi 0)) |
| 1264 | + (when (ormap positive? |
1272 | 1265 | n-exis) |
1273 | 1266 | (fail #:reason (~a "cannot generate contract for case function type with existentials"))) |
1274 | 1267 |
|
|
1287 | 1280 | (handle-arrow-range (first arrows) |
1288 | 1281 | (lambda () |
1289 | 1282 | (convert-single-arrow (first arrows)))) |
1290 | | - (case->/sc (map (lambda (arr) |
1291 | | - (handle-arrow-range arr (lambda () |
1292 | | - (convert-one-arrow-in-many arr)))) |
1293 | | - arrows)))])] |
| 1283 | + (case->/sc (for/list ([arr (in-list arrows)]) |
| 1284 | + (handle-arrow-range arr (lambda () (convert-one-arrow-in-many arr))))))])] |
1294 | 1285 | [(DepFun/ids: ids dom pre rng) |
1295 | 1286 | (define (continue) |
1296 | | - (match rng |
1297 | | - [(Values: (list (Result: rngs _ _) ...)) |
1298 | | - (define (dom-id? id) (member id ids free-identifier=?)) |
1299 | | - (define-values (dom* dom-deps) |
1300 | | - (for/lists (_1 _2) ([d (in-list dom)]) |
1301 | | - (values (t->sc/neg d) |
1302 | | - (filter dom-id? (free-ids d))))) |
1303 | | - (define pre* (if (TrueProp? pre) #f (t->sc/neg pre))) |
1304 | | - (define pre-deps (filter dom-id? (free-ids pre))) |
1305 | | - (define rng* (map t->sc rngs)) |
1306 | | - (define rng-deps (filter dom-id? |
1307 | | - (remove-duplicates |
1308 | | - (apply append (map free-ids rngs)) |
1309 | | - free-identifier=?))) |
1310 | | - (->i/sc (from-typed? typed-side) |
1311 | | - ids |
1312 | | - dom* |
1313 | | - dom-deps |
1314 | | - pre* |
1315 | | - pre-deps |
1316 | | - rng* |
1317 | | - rng-deps)])) |
| 1287 | + (match-define (Values: (list (Result: rngs _ _) ...)) rng) |
| 1288 | + (define (dom-id? id) |
| 1289 | + (member id ids free-identifier=?)) |
| 1290 | + (define-values (dom* dom-deps) |
| 1291 | + (for/lists (_1 _2) ([d (in-list dom)]) (values (t->sc/neg d) (filter dom-id? (free-ids d))))) |
| 1292 | + (define pre* |
| 1293 | + (if (TrueProp? pre) |
| 1294 | + #f |
| 1295 | + (t->sc/neg pre))) |
| 1296 | + (define pre-deps (filter dom-id? (free-ids pre))) |
| 1297 | + (define rng* (map t->sc rngs)) |
| 1298 | + (define rng-deps |
| 1299 | + (filter dom-id? (remove-duplicates (apply append (map free-ids rngs)) free-identifier=?))) |
| 1300 | + (->i/sc (from-typed? typed-side) ids dom* dom-deps pre* pre-deps rng* rng-deps)) |
1318 | 1301 | (handle-range rng continue)])) |
1319 | 1302 |
|
1320 | 1303 | ;; Generate a contract for a object/class method clause |
1321 | 1304 | ;; Precondition: type is a valid method type |
1322 | 1305 | (define (t->sc/method type fail typed-side recursive-values loop) |
1323 | 1306 | ;; helper for mutually recursive calls in Poly cases |
1324 | | - (define (rec body #:recursive-values rv) |
1325 | | - (t->sc/method body fail typed-side rv loop)) |
1326 | 1307 | (match type |
1327 | | - [(? Poly?) |
1328 | | - (t->sc/poly type fail typed-side recursive-values rec)] |
1329 | | - [(? PolyDots?) |
1330 | | - (t->sc/polydots type fail typed-side recursive-values rec)] |
1331 | | - [(? PolyRow?) |
1332 | | - (t->sc/polyrow type fail typed-side recursive-values rec)] |
1333 | | - [(? Fun?) |
1334 | | - (t->sc/function type fail typed-side recursive-values loop #t)] |
| 1308 | + [(? Poly?) (t->sc/poly type fail typed-side recursive-values rec)] |
| 1309 | + [(? PolyDots?) (t->sc/polydots type fail typed-side recursive-values rec)] |
| 1310 | + [(? PolyRow?) (t->sc/polyrow type fail typed-side recursive-values rec)] |
| 1311 | + [(? Fun?) (t->sc/function type fail typed-side recursive-values loop #t)] |
1335 | 1312 | [_ (fail #:reason "invalid method type")])) |
1336 | 1313 |
|
1337 | 1314 | (define (is-a-function-type? initial) |
|
1546 | 1523 | (require racket/extflonum) |
1547 | 1524 | (provide nonnegative? nonpositive? |
1548 | 1525 | extflonum? extflzero? extflnonnegative? extflnonpositive?) |
1549 | | - (define nonnegative? (lambda (x) (>= x 0))) |
1550 | | - (define nonpositive? (lambda (x) (<= x 0))) |
1551 | | - (define extflzero? (lambda (x) (extfl= x 0.0t0))) |
1552 | | - (define extflnonnegative? (lambda (x) (extfl>= x 0.0t0))) |
1553 | | - (define extflnonpositive? (lambda (x) (extfl<= x 0.0t0)))) |
| 1526 | + (define (nonnegative? x) |
| 1527 | + (>= x 0)) |
| 1528 | + (define (nonpositive? x) |
| 1529 | + (<= x 0)) |
| 1530 | + (define (extflzero? x) |
| 1531 | + (extfl= x 0.0t0)) |
| 1532 | + (define (extflnonnegative? x) |
| 1533 | + (extfl>= x 0.0t0)) |
| 1534 | + (define (extflnonpositive? x) |
| 1535 | + (extfl<= x 0.0t0))) |
1554 | 1536 |
|
1555 | 1537 | (module numeric-contracts racket/base |
1556 | 1538 | (require |
|
0 commit comments