From 3e2d020a194208d74348cea5a4a01a4b0570fe30 Mon Sep 17 00:00:00 2001 From: Ben Greenman Date: Fri, 8 Jul 2016 03:10:11 -0400 Subject: [PATCH] Implement object/c-opaque-stronger An opaque object contract is stronger than another (opaque) object contract if: - it has stronger field/method contracts on fields/methods common to both - and it has no more field/method contracts than the other, if the other is opaque --- .../typed-racket/utils/opaque-object.rkt | 62 +++++- .../succeed/opaque-object-name.rkt | 52 +++++ .../succeed/opaque-object-stronger.rkt | 186 ++++++++++++++++++ .../succeed/pr267-variation-0.rkt | 26 +++ 4 files changed, 319 insertions(+), 7 deletions(-) create mode 100644 typed-racket-test/succeed/opaque-object-name.rkt create mode 100644 typed-racket-test/succeed/opaque-object-stronger.rkt create mode 100644 typed-racket-test/succeed/pr267-variation-0.rkt diff --git a/typed-racket-lib/typed-racket/utils/opaque-object.rkt b/typed-racket-lib/typed-racket/utils/opaque-object.rkt index c92390a1..c8e2deeb 100644 --- a/typed-racket-lib/typed-racket/utils/opaque-object.rkt +++ b/typed-racket-lib/typed-racket/utils/opaque-object.rkt @@ -27,6 +27,9 @@ ;; blame parties (e.g., a particular module). (require racket/class + (only-in racket/private/class-c-old + base-object/c? build-object/c-type-name object/c-width-subtype? + object/c-common-methods-stronger? object/c-common-fields-stronger?) racket/match racket/contract/base racket/contract/combinator @@ -57,21 +60,55 @@ (dynamic-object/c (append methods remaining-methods) (append method-ctcs (for/list ([m remaining-methods]) - (restrict-typed->/c))) + (restrict-typed->/c m))) (append fields remaining-fields) (append field-ctcs (for/list ([m remaining-fields]) - (restrict-typed-field/c obj m))))) + (restrict-typed-field/c m))))) ;; FIXME: this is a bit sketchy because we have to construct ;; a contract that depends on the actual object that we got ;; since we don't know its methods beforehand (((contract-late-neg-projection guard/c) blame) obj neg-party))) +(define (object/c-opaque-name ctc) + (build-object/c-type-name 'object/c-opaque + (base-object/c-opaque-method-names ctc) + (base-object/c-opaque-method-ctcs ctc) + (base-object/c-opaque-field-names ctc) + (base-object/c-opaque-field-ctcs ctc))) + +;; Similar to object/c-stronger, but without width subtyping. +;; (Intuition: unspecified fields are guarded by the strongest possible contract) +;; An opaque object contract `this` is stronger than `that` when: +;; - `that` is an opaque contract +;; and `this` specifies at most the same members as `that` +;; and `this` has stronger contracts on all members +;; - `that` is an object/c contract +;; and `this` has stronger contracts on their common members +(define (object/c-opaque-stronger this that) + (define that-opaque? (base-object/c-opaque? that)) + (cond + [(or that-opaque? + (base-object/c? that)) + (define this-ctc (base-object/c-opaque-obj/c this)) + (define that-ctc (if that-opaque? (base-object/c-opaque-obj/c that) that)) + (and + (if that-opaque? + ;; then members of `this` should be a SUBSET of members of `that` + (object/c-width-subtype? that-ctc this-ctc) + #t) + (object/c-common-fields-stronger? this-ctc that-ctc) + (object/c-common-methods-stronger? this-ctc that-ctc) + #t)] + [else #f])) + (struct base-object/c-opaque - (obj/c ; keep a copy of the normal object/c for first-order checks + (obj/c ; keep a copy of the normal object/c for first-order and stronger checks method-names method-ctcs field-names field-ctcs) #:property prop:contract (build-contract-property + #:stronger object/c-opaque-stronger + #:name object/c-opaque-name #:first-order (λ (ctc) (define obj/c (base-object/c-opaque-obj/c ctc)) (λ (val) @@ -126,10 +163,16 @@ "cannot call uncontracted typed method")) (apply values args)))))) -(struct restrict-typed->/c () +;; Returns original method name +(define (restrict-typed->-name ctc) + (define name (restrict-typed->/c-name ctc)) + (build-compound-type-name 'restrict-typed->/c name)) + +(struct restrict-typed->/c (name) #:property prop:chaperone-contract (build-chaperone-contract-property - #:name (λ (ctc) ') ; FIXME + #:name restrict-typed->-name + #:stronger equal? #:late-neg-projection restrict-typed->-late-neg-projection)) (define (restrict-typed-field-late-neg-proj ctc) @@ -147,8 +190,13 @@ blame val #:missing-party neg-party "cannot read or write field hidden by Typed Racket")))) -(struct restrict-typed-field/c (obj name) +(define (restrict-typed-field-name ctc) + (define name (restrict-typed-field/c-name ctc)) + (build-compound-type-name 'restrict-typed-field/c name)) + +(struct restrict-typed-field/c (name) #:property prop:flat-contract (build-flat-contract-property - #:name (λ (ctc) ') ; FIXME + #:name restrict-typed-field-name + #:stronger equal? #:late-neg-projection restrict-typed-field-late-neg-proj)) diff --git a/typed-racket-test/succeed/opaque-object-name.rkt b/typed-racket-test/succeed/opaque-object-name.rkt new file mode 100644 index 00000000..bb2b7f47 --- /dev/null +++ b/typed-racket-test/succeed/opaque-object-name.rkt @@ -0,0 +1,52 @@ +#lang racket +(require typed-racket/utils/opaque-object rackunit + (for-syntax (only-in syntax/srcloc build-source-location-list))) + +;; -------------------------------------------------------------------------------------------------- + +;; object/c-opaque names should be lists: +;; - with 'object/c-opaque as the first element +;; - and 1 element for each member of the contract (field spec, method, ...) +(define-syntax (test-object/c-opaque-name-shape stx) + (syntax-case stx () + [(_ . ctc-spec*) + #`(begin + #,@(for/list ([ctc-spec (in-list (syntax-e #'ctc-spec*))]) + #`(let ([nm (contract-name (object/c-opaque #,@ctc-spec))]) + (with-check-info* (list (make-check-location '#,(build-source-location-list ctc-spec))) + (lambda () + (check-equal? (car nm) 'object/c-opaque) + (check-equal? (length nm) (+ 1 #,(length (syntax-e ctc-spec)))))))))])) + +(test-object/c-opaque-name-shape + [] + [(field [i integer?] [j string?])] + [(field [k (<=/c 0)]) + (m (->m (-> integer? integer?) zero?))] + [(m1 (->m (-> integer? integer?) zero?)) + (m2 (->m boolean?)) + (m3 (->m natural-number/c any/c))] + [(field [a real?] [b (-> string?)]) + (m1 (->m (-> integer? integer?) zero?)) + (m2 (->m boolean?)) + (m3 (->m natural-number/c any/c))] +) + +;; -------------------------------------------------------------------------------------------------- + +(define-syntax (test-object/c-vs-opaque-name stx) + (syntax-case stx () + [(_ . ctc-spec*) + #`(begin + #,@(for/list ([ctc-spec (in-list (syntax-e #'ctc-spec*))]) + #`(check-not-equal? + (contract-name (object/c #,@ctc-spec)) + (contract-name (object/c-opaque #,@ctc-spec)))))])) + +(test-object/c-vs-opaque-name + [] + [(field [i integer?]) + (f (->m string? boolean?))] + [(hd (->m any/c)) + (tl (->m object?))] +) diff --git a/typed-racket-test/succeed/opaque-object-stronger.rkt b/typed-racket-test/succeed/opaque-object-stronger.rkt new file mode 100644 index 00000000..6c83661e --- /dev/null +++ b/typed-racket-test/succeed/opaque-object-stronger.rkt @@ -0,0 +1,186 @@ +#lang racket +(require typed-racket/utils/opaque-object) + +;; -------------------------------------------------------------------------------------------------- +;; test helpers + +(define (test-stronger? ctc-stronger ctc-weaker) + (unless (contract-stronger? ctc-stronger ctc-weaker) + (error 'pr267 + "contract ~a is unexpectedly weaker than ~a" + (contract-name ctc-stronger) + (contract-name ctc-weaker)))) + +(define (test-not-stronger? ctc-stronger ctc-weaker) + (when (contract-stronger? ctc-stronger ctc-weaker) + (error 'pr267 + "contract ~a is unexpectedly stronger than ~a" + (contract-name ctc-stronger) + (contract-name ctc-weaker)))) + +;; -------------------------------------------------------------------------------------------------- +;; stronger? tests + +(let () ;; object/c-opaque with the same members + (test-stronger? + (object/c-opaque) + (object/c-opaque)) + + (test-stronger? + (object/c-opaque + (field (f1 integer?)) + (m1 (->m object? object?))) + (object/c-opaque + (field (f1 integer?)) + (m1 (->m object? object?)))) + + (test-stronger? + (object/c-opaque + (m1 (->m any/c object? (-> integer? integer?)))) + (object/c-opaque + (m1 (->m any/c object? (-> integer? integer?))))) +) + +(let () ;; object/c-opaque with fewer members (unspecified = opaque) + (test-stronger? + (object/c-opaque) + (object/c-opaque + (field (x symbol?)))) + + (test-stronger? + (object/c-opaque + (field (x symbol?))) + (object/c-opaque + (field (x symbol?)) + (y (->m none/c none/c)))) + + (test-stronger? + (object/c-opaque + (f (->m void? any/c))) + (object/c-opaque + (f (->m void? any/c)) + (g (->m integer? integer? integer?)))) + + (test-stronger? + (object/c-opaque + (field (a integer?)) + (c (-> real? real?))) + (object/c-opaque + (field (a integer?) + (b integer?)) + (c (-> real? real?)) + (d (-> real? real?)))) + +) + +(let () ;; object/c-opaque with stronger members + + (test-stronger? + (object/c-opaque + (m1 (->m any/c integer?))) + (object/c-opaque + (m1 (->m any/c any/c)))) + + (test-stronger? + (object/c-opaque + (m1 (->m any/c any/c))) + (object/c-opaque + (m1 (->m integer? any/c)))) + + (test-stronger? + (object/c-opaque + (m1 (->m any/c integer?)) + (m2 (->m any/c (listof boolean?)))) + (object/c-opaque + (m1 (->m any/c integer?)) + (m2 (->m any/c (listof any/c))))) + + (test-stronger? + (object/c-opaque + (a (->m symbol?)) + (b (->m (between/c 2 3))) + (c (->m any/c (listof (char-in #\A #\B))))) + (object/c-opaque + (a (->m symbol?)) + (b (->m (between/c 0 5))) + (c (->m any/c (listof (char-in #\A #\Z)))))) +) + +(let () ;; vs. object/c + (test-stronger? + (object/c-opaque) + (object/c + (field (a boolean?)) + (b (->m string? any/c)))) + + (test-stronger? + (object/c-opaque + (field (x any/c)) + (h (->m (-> boolean? boolean? boolean?) integer?))) + (object/c)) + + (test-stronger? + (object/c-opaque + (field (x integer?)) + (m1 (->m any/c any/c any/c))) + (object/c + (field (x integer?)) + (m1 (->m any/c any/c any/c)))) + + (test-stronger? + (object/c-opaque + (m1 (->m any/c (m any/c ( any/c (listof zero?))))) + (object/c-opaque + (field (a symbol?) + (b real?) + (c (-> any/c (listof exact-nonnegative-integer?)))))) +) + +(let () ;; an object/c is never stronger than an object/c-opaque + (test-not-stronger? + (object/c-opaque + (f (->m integer? integer?))) + (object/c + (f (->m any/c none/c)))) + + (test-not-stronger? + (object/c + (f (->m any/c none/c))) + (object/c-opaque + (f (->m integer? integer?)))) + + (test-not-stronger? + (object/c + (field (x integer?)) + (m1 (->m any/c any/c any/c))) + (object/c-opaque + (field (x real?)) + (m1 (->m any/c any/c any/c)))) + +) diff --git a/typed-racket-test/succeed/pr267-variation-0.rkt b/typed-racket-test/succeed/pr267-variation-0.rkt new file mode 100644 index 00000000..6a5021a5 --- /dev/null +++ b/typed-racket-test/succeed/pr267-variation-0.rkt @@ -0,0 +1,26 @@ +#lang racket + +;; Regression test for PR 267 +;; https://github.com/racket/typed-racket/pull/267 +;; Issue reported separately as: +;; https://github.com/racket/racket/issues/1198 +;; becuase it was really a racket/contract issue +;; (impersonate-vector contracts were using chaperone-contract) + +(define con + (object/c (field [a* any/c]) + (regenerate (->m (object/c (field [a* (vectorof (object/c))])))))) + +(define population% + (class object% + (super-new) + (init-field a*) + (define/public (regenerate) + (vector-ref (get-field a* this) 0) + this))) + +(define pop + (contract con (new population% [a* (vector (new (class object% (super-new))))]) 'p 'n)) + +(void (send (send pop regenerate) regenerate)) +