Make struct type contracts better
original commit: 745403a88e353c82ed850d7954254896cf1446f7
This commit is contained in:
parent
90ef1eac37
commit
66ccae0e72
|
@ -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)
|
||||
|
|
|
@ -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))]))))
|
||||
|
||||
|
|
Loading…
Reference in New Issue
Block a user