Improve contract generation in Typed Racket.

This fixes several issues:
 - `Parameter` generates impersonator contracts correctly
 - `Any` handling now copies immutable data when possible
 - `Any` now recognizes more atomic base types

Merge to 5.3.1.

original commit: c6dc1e6ece441a7d56c2f2229dc9c0e144f8ff6f
This commit is contained in:
Sam Tobin-Hochstadt 2012-10-25 00:18:50 -07:00
parent f19e523806
commit bde8ebbef0
4 changed files with 65 additions and 17 deletions

View File

@ -0,0 +1,7 @@
#lang typed/racket/base
(require/typed
rackunit
[current-check-around (Parameter Any)])

View File

@ -0,0 +1,11 @@
#lang racket/load
(module m1 racket
(define (f x y) (equal? x y))
(provide f))
(module m2 typed/racket
(require/typed 'm1 [f (Any Any -> Boolean)])
(f (vector 1 2) (vector 1 2)))
(require 'm2)

View File

@ -54,14 +54,24 @@
(let ([typ (if maker?
((map fld-t (Struct-flds (lookup-type-name (Name-id typ)))) #f . t:->* . typ)
typ)])
(with-syntax ([cnt (type->contract
typ
;; this is for a `require/typed', so the value is not from the typed side
#:typed-side #f
#:kind kind
(lambda () (tc-error/stx prop "Type ~a could not be converted to a contract." typ)))])
(quasisyntax/loc stx (define-values (n) (recursive-contract cnt #,(contract-kind->keyword kind))))))]
[_ (int-err "should never happen - not a define-values: ~a" (syntax->datum stx))]))
(with-syntax ([cnt (type->contract
typ
;; this is for a `require/typed', so the value is not from the typed side
#:typed-side #f
#:kind kind
(λ ()
(tc-error/stx
prop
"Type ~a could not be converted to a contract."
typ)))])
(quasisyntax/loc
stx
(define-values (n)
(recursive-contract
cnt
#,(contract-kind->keyword kind))))))]
[_ (int-err "should never happen - not a define-values: ~a"
(syntax->datum stx))]))
(define (change-contract-fixups forms)
(map (lambda (e)
@ -89,7 +99,6 @@
(for/fold ((acc i)) ((v args))
(contract-kind-max2 v acc)))
(define (contract-kind-min i . args)
(define (contract-kind-min2 x y)
(cond
@ -106,7 +115,7 @@
(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 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)))
@ -138,7 +147,9 @@
[(and
(> (length arrs) 1)
;; Keyword args, range and rest specs all the same.
(let ([xs (map (match-lambda [(arr: _ rng rest-spec _ kws) (list rng rest-spec kws)]) arrs)])
(let ([xs (map (match-lambda [(arr: _ rng rest-spec _ kws)
(list rng rest-spec kws)])
arrs)])
(foldl equal? (first xs) (rest xs)))
;; Positionals are monotonically increasing.
(let-values ([(_ ok?)
@ -338,11 +349,13 @@
(match-let ([(Mu-name: n-nm _) ty])
(with-syntax ([(n*) (generate-temporaries (list n-nm))])
(parameterize ([vars (cons (list n #'n*) (vars))]
[current-contract-kind (contract-kind-min kind chaperone-sym)])
[current-contract-kind
(contract-kind-min kind chaperone-sym)])
(define ctc (t->c b))
#`(letrec ([n* (recursive-contract
#,ctc
#,(contract-kind->keyword (current-contract-kind)))])
#,(contract-kind->keyword
(current-contract-kind)))])
n*))))]
[(Value: #f) #'false/c]
[(Instance: (? Mu? t))
@ -389,7 +402,9 @@
#`(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))]
[(Param: in out)
(set-impersonator!)
#`(parameter/c #,(t->c out))]
[(Hashtable: k v)
(when (equal? kind flat-sym) (exit (fail)))
#`(hash/c #,(t->c k #:kind chaperone-sym) #,(t->c v) #:immutable 'dont-care)]

View File

@ -1,12 +1,12 @@
#lang racket/base
(require racket/match racket/contract/base racket/contract/combinator)
(require racket/match racket/contract/base racket/contract/combinator racket/flonum racket/fixnum)
(define undef (letrec ([x x]) x))
(define (traverse b)
(define (fail v)
(raise-blame-error (blame-swap b) v "Attempted to use a higher-order value passed as `Any`"))
(raise-blame-error (blame-swap b) v "Attempted to use a higher-order value passed as `Any` in untyped code"))
(define (t v)
(define (wrap-struct s)
@ -43,10 +43,25 @@
(match v
[(? (lambda (e)
(or (number? e) (string? e) (char? e) (symbol? e)
(null? e) (regexp? e) (eq? undef e)
(null? e) (regexp? e) (eq? undef e) (path? e)
(flvector? e) (flvector? e) (regexp? e)
(keyword? e) (bytes? e) (boolean? e) (void? e))))
v]
[(cons x y) (cons (t x) (t y))]
[(? vector? (? immutable?))
;; fixme -- should have an immutable for/vector
(vector->immutable-vector
(for/vector #:length (vector-length v)
([i (in-vector v)]) (t i)))]
[(? box? (? immutable?)) (box-immutable (t (unbox v)))]
;; fixme -- handling keys
;; [(? hasheq? (? immutable?))
;; (for/hasheq ([(k v) (in-hash v)]) (values k v))]
;; [(? hasheqv? (? immutable?))
;; (for/hasheqv ([(k v) (in-hash v)]) (values k v))]
[(? hash? (? immutable?))
(for/hash ([(k v) (in-hash v)]) (values (t k) (t v)))]
[(? vector?) (chaperone-vector v
(lambda (v i e) (t e))
(lambda (v i e) (fail v)))]