From 1147ae8bef113ad4b320f6982dbc57ae92b43b1f Mon Sep 17 00:00:00 2001 From: Eric Dobson Date: Sat, 1 Sep 2012 15:30:01 -0700 Subject: [PATCH] Make struct type contracts better --- .../unit-tests/contract-tests.rkt | 10 +- .../typed-racket/private/type-contract.rkt | 120 ++++++++++++------ 2 files changed, 91 insertions(+), 39 deletions(-) diff --git a/collects/tests/typed-racket/unit-tests/contract-tests.rkt b/collects/tests/typed-racket/unit-tests/contract-tests.rkt index 53cefd46024..bcf33465941 100644 --- a/collects/tests/typed-racket/unit-tests/contract-tests.rkt +++ b/collects/tests/typed-racket/unit-tests/contract-tests.rkt @@ -10,10 +10,18 @@ (define-syntax-rule (t e) (test-not-exn (format "~a" e) (lambda () (type->contract e (lambda _ (error "type could not be converted to contract")))))) +(define-syntax-rule (t/fail e) + (test-not-exn (format "~a" e) (lambda () + (let/ec exit + (type->contract e (lambda _ (exit #t))) + (error "type could be converted to contract"))))) + (define (contract-tests) (test-suite "Contract Tests" (t (-Number . -> . -Number)) - (t (-Promise -Number)))) + (t (-Promise -Number)) + (t/fail (-set Univ)) + )) (define-go contract-tests) (provide contract-tests) diff --git a/collects/typed-racket/private/type-contract.rkt b/collects/typed-racket/private/type-contract.rkt index b201195c127..22a0d6cc1fa 100644 --- a/collects/typed-racket/private/type-contract.rkt +++ b/collects/typed-racket/private/type-contract.rkt @@ -72,9 +72,43 @@ (define (no-duplicates l) (= (length l) (length (remove-duplicates l)))) -;(require racket/trace) +;; To avoid misspellings +(define impersonator-sym 'impersonator) +(define chaperone-sym 'chaperone) +(define flat-sym 'flat) + +(define (contract-kind-max . args) + (define (contract-kind-max2 x y) + (cond + ((equal? flat-sym x) y) + ((equal? flat-sym y) x) + ((equal? chaperone-sym x) y) + ((equal? chaperone-sym y) x) + (else impersonator-sym))) + (for/fold ((acc flat-sym)) ((v args)) + (contract-kind-max2 v acc))) + + +(define (contract-kind-min . args) + (define (contract-kind-min2 x y) + (cond + ((equal? flat-sym x) x) + ((equal? flat-sym y) y) + ((equal? chaperone-sym x) x) + ((equal? chaperone-sym y) y) + (else impersonator-sym))) + (for/fold ((acc flat-sym)) ((v args)) + (contract-kind-min2 v acc))) + + +(define (contract-kind->keyword sym) + (string->keyword (symbol->string sym))) + (define (type->contract ty fail #:out [out? #f] #:typed-side [from-typed? #t] #:kind [kind 'impersonator]) (define vars (make-parameter '())) + (define current-contract-kind (make-parameter flat-sym)) + (define (increase-current-contract-kind! kind) + (current-contract-kind (contract-kind-max (current-contract-kind) kind))) (let/ec exit (let loop ([ty ty] [pos? #t] [from-typed? from-typed?] [structs-seen null] [kind kind]) (define (t->c t #:seen [structs-seen structs-seen] #:kind [kind kind]) @@ -85,7 +119,7 @@ (match f [(Function: (list (top-arr:))) #'procedure?] [(Function: arrs) - (when (equal? kind 'flat) (exit (fail))) + (set-chaperone!) (let () (define ((f [case-> #f]) a) (define-values (dom* opt-dom* rngs* rst) @@ -133,16 +167,25 @@ [(list e) e] [l #`(case-> #,@l)]))] [_ (int-err "not a function" f)])) + + ;; Helpers for contract requirements + (define (set-impersonator!) + (when (not (equal? kind impersonator-sym)) (exit (fail))) + (increase-current-contract-kind! impersonator-sym)) + (define (set-chaperone!) + (when (equal? kind flat-sym) (exit (fail))) + (increase-current-contract-kind! chaperone-sym)) + + (match ty [(or (App: _ _ _) (Name: _)) (t->c (resolve-once ty))] ;; any/c doesn't provide protection in positive position [(Univ:) - (cond - ((and from-typed? (equal? kind 'impersonator)) - #'any-wrap/c) - ((not from-typed?) - #'any/c) - (else (exit (fail))))] + (if from-typed? + (begin + (set-impersonator!) + #'any-wrap/c) + #'any/c)] ;; we special-case lists: [(Mu: var (Union: (list (Value: '()) (Pair: elem-ty (F: var))))) (if (and (not from-typed?) (type-equal? elem-ty t:Univ)) @@ -211,24 +254,26 @@ ([cnts (append (map t->c vars) (map t->c notvars))]) #'(or/c . cnts)))] [(and t (Function: _)) (t->c/fun t)] - [(Set: t) #`(set/c #,(t->c t))] + [(Set: t) + #`(set/c #,(t->c t #:kind (contract-kind-min kind chaperone-sym)))] [(Sequence: ts) #`(sequence/c #,@(map t->c ts))] [(Vector: t) - (when (equal? kind 'flat) (exit (fail))) + (set-chaperone!) #`(vectorof #,(t->c t))] [(HeterogenousVector: ts) - (when (equal? kind 'flat) (exit (fail))) + (set-chaperone!) #`(vector/c #,@(map t->c ts))] [(Box: t) - (when (equal? kind 'flat) (exit (fail))) + (set-chaperone!) #`(box/c #,(t->c t))] [(Pair: t1 t2) #`(cons/c #,(t->c t1) #,(t->c t2))] [(Promise: t) - (when (equal? kind 'flat) (exit (fail))) + (set-chaperone!) #`(promise/c #,(t->c t))] [(Opaque: p? cert) #`(flat-named-contract (quote #,(syntax-e p?)) #,(cert p?))] + ;; TODO [(F: v) (cond [(assoc v (vars)) => second] [else (int-err "unknown var: ~a" v)])] [(Poly: vs b) @@ -239,29 +284,29 @@ ;; in negative position, use `parameteric/c' (match-let ([(Poly-names: vs-nm _) ty]) (with-syntax ([(v ...) (generate-temporaries vs-nm)]) + (set-impersonator!) (parameterize ([vars (append (map list vs (syntax->list #'(v ...))) (vars))]) #`(parametric->/c (v ...) #,(t->c b))))))] [(Mu: n b) (match-let ([(Mu-name: n-nm _) ty]) (with-syntax ([(n*) (generate-temporaries (list n-nm))]) - (parameterize ([vars (cons (list n #'n* #'n*) (vars))]) + (parameterize ([vars (cons (list n #'n*) (vars))] + [current-contract-kind flat-sym]) + (define ctc (t->c b)) #`(letrec ([n* (recursive-contract - #,(t->c b) - #,(case kind - ((flat) #'#:flat) - ((chaperone) #'#:chaperone) - ((impersonator) #'#:impersonator)))]) + #,ctc + #,(contract-kind->keyword (current-contract-kind)))]) n*))))] [(Value: #f) #'false/c] [(Instance: (Class: _ _ (list (list name fcn) ...))) - (when (equal? kind 'flat) (exit (fail))) + (set-impersonator!) (with-syntax ([(fcn-cnts ...) (for/list ([f fcn]) (t->c/fun f #:method #t))] [(names ...) name]) #'(object/c (names fcn-cnts) ...))] ;; init args not currently handled by class/c [(Class: _ (list (list by-name-init by-name-init-ty _) ...) (list (list name fcn) ...)) - (when (equal? kind 'flat) (exit (fail))) + (set-impersonator!) (with-syntax ([(fcn-cnt ...) (for/list ([f fcn]) (t->c/fun f #:method #t))] [(name ...) name] [(by-name-cnt ...) (for/list ([t by-name-init-ty]) (t->c/neg t))] @@ -274,32 +319,31 @@ => cdr] [proc (exit (fail))] - [(and (equal? kind 'flat) (ormap values mut?)) + [(and (equal? kind flat-sym) (ormap values mut?)) (exit (fail))] [poly? - (with-syntax* ([rec (generate-temporary 'rec)]) + (with-syntax* ([struct-ctc (generate-temporary 'struct-ctc)]) (define field-contracts (for/list ([fty flds] [mut? mut?]) - (define rec-kind - (cond - ((equal? kind 'flat) 'flat) - ((equal? kind 'chaperone) 'chaperone) - ((not mut?) 'chaperone) - (else 'impersonator))) - (define rec-kind-kw (string->keyword (symbol->string rec-kind))) - - (t->c fty #:seen (cons (cons ty #`(recursive-contract rec #,rec-kind-kw)) - structs-seen) - #:kind rec-kind))) - #`(letrec ((rec (struct/c #,nm #,@field-contracts))) rec))] + (with-syntax* ([rec (generate-temporary 'rec)]) + (define required-recursive-kind + (contract-kind-min kind (if mut? impersonator-sym chaperone-sym))) + (parameterize ((current-contract-kind flat-sym)) + (let ((fld-ctc (t->c fty #:seen (cons (cons ty #'rec) structs-seen) + #:kind required-recursive-kind))) + #`(let ((rec (recursive-contract struct-ctc #,(contract-kind->keyword (current-contract-kind))))) + #,fld-ctc)))))) + #`(letrec ((struct-ctc (struct/c #,nm #,@field-contracts))) struct-ctc))] [else #`(flat-named-contract '#,(syntax-e pred?) (lambda (x) (#,(cert pred?) x)))])] [(Syntax: (Base: 'Symbol _ _ _ _)) #'identifier?] - [(Syntax: t) #`(syntax/c #,(t->c t))] + [(Syntax: t) + #`(syntax/c #,(t->c t #:kind flat-sym))] [(Value: v) #`(flat-named-contract #,(format "~a" v) (lambda (x) (equal? x '#,v)))] + ;; TODO Is this sound? [(Param: in out) #`(parameter/c #,(t->c out))] [(Hashtable: k v) - (when (equal? kind 'flat) (exit (fail))) - #`(hash/c #,(t->c k) #,(t->c v) #:immutable 'dont-care)] + (when (equal? kind flat-sym) (exit (fail))) + #`(hash/c #,(t->c k #:kind chaperone-sym) #,(t->c v) #:immutable 'dont-care)] [else (exit (fail))]))))