suzanne.soy/racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Fix type->contract on structures. Now uses struct/c.

Browse Source
This commit is contained in:
Eric Dobson 2012-08-21 08:52:23 -07:00 committed by Sam Tobin-Hochstadt
parent 8ba835a3c9
commit 9e1cf579a4
3 changed files with 71 additions and 60 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

23
collects/tests/typed-racket/succeed/contract-struct-equality.rkt Normal file
View File

@ -0,0 +1,23 @@
#lang racket/load
(module typed typed/racket
(provide g)
(struct: (A) foo ((v : A)))
(: f (foo Byte))
(define f (foo 2))
(: g (-> (foo Byte)))
(define (g) f))
(module typed-client typed/racket
(require 'typed)
(unless (equal? (g) (g))
(error 'typed2 "Failed")))
(module untyped-client racket
(require 'typed)
(unless (equal? (g) (g))
(error 'typed2 "Failed")))
(require 'typed-client)
(require 'untyped-client)

2
collects/typed-racket/base-env/prims.rkt
View File

@ -223,7 +223,7 @@ This file defines two sorts of primitives. All of them are provided into any mod
(type->contract (type->contract
typ typ
;; must be a flat contract ;; must be a flat contract
#:flat #t #:kind 'flat
;; the value is not from the typed side ;; the value is not from the typed side
#:typed-side #f #:typed-side #f
(lambda () (tc-error/stx #'ty "Type ~a could not be converted to a predicate." typ))) (lambda () (tc-error/stx #'ty "Type ~a could not be converted to a predicate." typ)))

106
collects/typed-racket/private/type-contract.rkt
View File

@ -57,9 +57,9 @@
typ typ
;; this is for a `require/typed', so the value is not from the typed side ;; this is for a `require/typed', so the value is not from the typed side
#:typed-side #f #:typed-side #f
#:flat flat? #:kind (if flat? 'flat 'impersonator)
(lambda () (tc-error/stx prop "Type ~a could not be converted to a contract." typ)))]) (lambda () (tc-error/stx prop "Type ~a could not be converted to a contract." typ)))])
(quasisyntax/loc stx (define-values (n) (recursive-contract cnt #,(if flat? #'#:flat #'#:impersonator))))))] (quasisyntax/loc stx (define-values (n) cnt))))]
[_ (int-err "should never happen - not a define-values: ~a" (syntax->datum stx))])) [_ (int-err "should never happen - not a define-values: ~a" (syntax->datum stx))]))
(define (change-contract-fixups forms) (define (change-contract-fixups forms)
@ -72,20 +72,20 @@
(define (no-duplicates l) (define (no-duplicates l)
(= (length l) (length (remove-duplicates l)))) (= (length l) (length (remove-duplicates l))))
;(require racket/trace)
(define (type->contract ty fail #:out [out? #f] #:typed-side [from-typed? #t] #:flat [flat? #f]) (define (type->contract ty fail #:out [out? #f] #:typed-side [from-typed? #t] #:kind [kind 'impersonator])
(define vars (make-parameter '())) (define vars (make-parameter '()))
(let/ec exit (let/ec exit
(let loop ([ty ty] [pos? #t] [from-typed? from-typed?] [structs-seen null] [flat? flat?]) (let loop ([ty ty] [pos? #t] [from-typed? from-typed?] [structs-seen null] [kind kind])
(define (t->c t #:seen [structs-seen structs-seen] #:flat [flat? flat?]) (define (t->c t #:seen [structs-seen structs-seen] #:kind [kind kind])
(loop t pos? from-typed? structs-seen flat?)) (loop t pos? from-typed? structs-seen kind))
(define (t->c/neg t #:seen [structs-seen structs-seen] #:flat [flat? flat?]) (define (t->c/neg t #:seen [structs-seen structs-seen] #:flat [kind kind])
(loop t (not pos?) (not from-typed?) structs-seen flat?)) (loop t (not pos?) (not from-typed?) structs-seen kind))
(define (t->c/fun f #:method [method? #f]) (define (t->c/fun f #:method [method? #f])
(match f (match f
[(Function: (list (top-arr:))) #'procedure?] [(Function: (list (top-arr:))) #'procedure?]
[(Function: arrs) [(Function: arrs)
(when flat? (exit (fail))) (when (equal? kind 'flat) (exit (fail)))
(let () (let ()
(define ((f [case-> #f]) a) (define ((f [case-> #f]) a)
(define-values (dom* opt-dom* rngs* rst) (define-values (dom* opt-dom* rngs* rst)
@ -136,7 +136,13 @@
(match ty (match ty
[(or (App: _ _ _) (Name: _)) (t->c (resolve-once ty))] [(or (App: _ _ _) (Name: _)) (t->c (resolve-once ty))]
;; any/c doesn't provide protection in positive position ;; any/c doesn't provide protection in positive position
[(Univ:) (if from-typed? #'any-wrap/c #'any/c)] [(Univ:)
(cond
((and from-typed? (equal? kind 'impersonator))
#'any-wrap/c)
((not from-typed?)
#'any/c)
(else (exit (fail))))]
;; we special-case lists: ;; we special-case lists:
[(Mu: var (Union: (list (Value: '()) (Pair: elem-ty (F: var))))) [(Mu: var (Union: (list (Value: '()) (Pair: elem-ty (F: var)))))
(if (and (not from-typed?) (type-equal? elem-ty t:Univ)) (if (and (not from-typed?) (type-equal? elem-ty t:Univ))
@ -208,18 +214,18 @@
[(Set: t) #`(set/c #,(t->c t))] [(Set: t) #`(set/c #,(t->c t))]
[(Sequence: ts) #`(sequence/c #,@(map t->c ts))] [(Sequence: ts) #`(sequence/c #,@(map t->c ts))]
[(Vector: t) [(Vector: t)
(when flat? (exit (fail))) (when (equal? kind 'flat) (exit (fail)))
#`(vectorof #,(t->c t))] #`(vectorof #,(t->c t))]
[(HeterogenousVector: ts) [(HeterogenousVector: ts)
(when flat? (exit (fail))) (when (equal? kind 'flat) (exit (fail)))
#`(vector/c #,@(map t->c ts))] #`(vector/c #,@(map t->c ts))]
[(Box: t) [(Box: t)
(when flat? (exit (fail))) (when (equal? kind 'flat) (exit (fail)))
#`(box/c #,(t->c t))] #`(box/c #,(t->c t))]
[(Pair: t1 t2) [(Pair: t1 t2)
#`(cons/c #,(t->c t1) #,(t->c t2))] #`(cons/c #,(t->c t1) #,(t->c t2))]
[(Promise: t) [(Promise: t)
(when flat? (exit (fail))) (when (equal? kind 'flat) (exit (fail)))
#`(promise/c #,(t->c t))] #`(promise/c #,(t->c t))]
[(Opaque: p? cert) [(Opaque: p? cert)
#`(flat-named-contract (quote #,(syntax-e p?)) #,(cert p?))] #`(flat-named-contract (quote #,(syntax-e p?)) #,(cert p?))]
@ -240,17 +246,22 @@
(match-let ([(Mu-name: n-nm _) ty]) (match-let ([(Mu-name: n-nm _) ty])
(with-syntax ([(n*) (generate-temporaries (list n-nm))]) (with-syntax ([(n*) (generate-temporaries (list n-nm))])
(parameterize ([vars (cons (list n #'n* #'n*) (vars))]) (parameterize ([vars (cons (list n #'n* #'n*) (vars))])
#`(letrec ([n* (recursive-contract #,(t->c b) #,(if flat? #'#:flat #'#:impersonator))]) #`(letrec ([n* (recursive-contract
#,(t->c b)
#,(case kind
((flat) #'#:flat)
((chaperone) #'#:chaperone)
((impersonator) #'#:impersonator)))])
n*))))] n*))))]
[(Value: #f) #'false/c] [(Value: #f) #'false/c]
[(Instance: (Class: _ _ (list (list name fcn) ...))) [(Instance: (Class: _ _ (list (list name fcn) ...)))
(when flat? (exit (fail))) (when (equal? kind 'flat) (exit (fail)))
(with-syntax ([(fcn-cnts ...) (for/list ([f fcn]) (t->c/fun f #:method #t))] (with-syntax ([(fcn-cnts ...) (for/list ([f fcn]) (t->c/fun f #:method #t))]
[(names ...) name]) [(names ...) name])
#'(object/c (names fcn-cnts) ...))] #'(object/c (names fcn-cnts) ...))]
;; init args not currently handled by class/c ;; init args not currently handled by class/c
[(Class: _ (list (list by-name-init by-name-init-ty _) ...) (list (list name fcn) ...)) [(Class: _ (list (list by-name-init by-name-init-ty _) ...) (list (list name fcn) ...))
(when flat? (exit (fail))) (when (equal? kind 'flat) (exit (fail)))
(with-syntax ([(fcn-cnt ...) (for/list ([f fcn]) (t->c/fun f #:method #t))] (with-syntax ([(fcn-cnt ...) (for/list ([f fcn]) (t->c/fun f #:method #t))]
[(name ...) name] [(name ...) name]
[(by-name-cnt ...) (for/list ([t by-name-init-ty]) (t->c/neg t))] [(by-name-cnt ...) (for/list ([t by-name-init-ty]) (t->c/neg t))]
@ -263,54 +274,31 @@
=> =>
cdr] cdr]
[proc (exit (fail))] [proc (exit (fail))]
[(and flat? (ormap values mut?)) [(and (equal? kind 'flat) (ormap values mut?))
(exit (fail))] (exit (fail))]
[poly? [poly?
(with-syntax* ([(rec blame val) (generate-temporaries '(rec blame val))] (with-syntax* ([rec (generate-temporary 'rec)])
[maker maker-id] (define field-contracts
[cnt-name nm]) (for/list ([fty flds] [mut? mut?])
;If it should be a flat contract, we make flat contracts for the type of each field, (define rec-kind
;extract the predicates, and apply the predicates to the corresponding field value (cond
(if flat? ((equal? kind 'flat) 'flat)
#`(letrec ([rec ((equal? kind 'chaperone) 'chaperone)
(make-flat-contract ((not mut?) 'chaperone)
#:name 'cnt-name (else 'impersonator)))
#:first-order (define rec-kind-kw (string->keyword (symbol->string rec-kind)))
(lambda (val)
(and (t->c fty #:seen (cons (cons ty #`(recursive-contract rec #,rec-kind-kw))
(#,pred? val) structs-seen)
#,@(for/list ([fty flds] [f-acc acc-ids]) #:kind rec-kind)))
#`((flat-contract-predicate #`(letrec ((rec (struct/c #,nm #,@field-contracts))) rec))]
#,(t->c fty #:seen (cons (cons ty #'(recursive-contract rec #:flat)) structs-seen))) [else #`(flat-named-contract '#,(syntax-e pred?) (lambda (x) (#,(cert pred?) x)))])]
(#,f-acc val))))))])
rec)
;Should make this case a chaperone/impersonator contract
(with-syntax ([(fld-cnts ...)
(for/list ([fty flds]
[f-acc acc-ids]
[m? mut?])
#`(((contract-projection
#,(t->c fty #:seen (cons (cons ty #'(recursive-contract rec)) structs-seen)))
blame)
(#,f-acc val)))])
#`(letrec ([rec
(make-contract
#:name 'cnt-name
#:first-order #,pred?
#:projection
(lambda (blame)
(lambda (val)
(unless (#,pred? val)
(raise-blame-error blame val "expected ~a value, got ~v" 'cnt-name val))
(maker fld-cnts ...))))])
rec))))]
[else #`(flat-named-contract '#,(syntax-e pred?) #,(cert pred?))])]
[(Syntax: (Base: 'Symbol _ _ _ _)) #'identifier?] [(Syntax: (Base: 'Symbol _ _ _ _)) #'identifier?]
[(Syntax: t) #`(syntax/c #,(t->c t))] [(Syntax: t) #`(syntax/c #,(t->c t))]
[(Value: v) #`(flat-named-contract #,(format "~a" v) (lambda (x) (equal? x '#,v)))] [(Value: v) #`(flat-named-contract #,(format "~a" v) (lambda (x) (equal? x '#,v)))]
[(Param: in out) #`(parameter/c #,(t->c out))] [(Param: in out) #`(parameter/c #,(t->c out))]
[(Hashtable: k v) [(Hashtable: k v)
(when flat? (exit (fail))) (when (equal? kind 'flat) (exit (fail)))
#`(hash/c #,(t->c k) #,(t->c v) #:immutable 'dont-care)] #`(hash/c #,(t->c k) #,(t->c v) #:immutable 'dont-care)]
[else [else
(exit (fail))])))) (exit (fail))]))))