Fix cast under multiple cases of case-> (#589)

* fix cast under multiple cases of case->

* add test

* Comments explaining cast-table's lists of types and what they mean
This commit is contained in:
Alex Knauth 2017-09-30 19:19:18 -04:00 committed by GitHub
parent 9df037b0f6
commit ee7207d67d
3 changed files with 39 additions and 8 deletions

View File

@ -287,8 +287,10 @@
;; that `(cast-table-ref id)` can get that type here.
(λ ()
(define type-stx
(or (cast-table-ref id)
#f))
(let ([types (cast-table-ref id)])
(if types
#`(U #,@types)
#f)))
`#s(contract-def ,type-stx ,flat? ,maker? typed))))
@ -353,7 +355,7 @@
(make-contract-def-rhs/from-typed existing-ty-id #f #f)))
(define (store-existing-type existing-type)
(check-no-free-vars existing-type #'v)
(cast-table-set! existing-ty-id (datum->syntax #f existing-type #'v)))
(cast-table-add! existing-ty-id (datum->syntax #f existing-type #'v)))
(define (check-valid-type _)
(define type (parse-type #'ty))
(check-no-free-vars type #'ty))

View File

@ -1,7 +1,7 @@
#lang racket/base
(provide cast-table-ref
cast-table-set!)
cast-table-add!)
(require syntax/id-table)
@ -13,13 +13,30 @@
;; generated based on the existing type of the expression, which must be stored
;; in this table so that it can be looked up later in the contract-generation
;; pass.
;;
;; If a cast is within a `case->` functions, it is typechecked with multiple
;; types. The cast table holds all of those types, and the contract layer
;; must protect values of any one of those types. This is why the cast-table
;; contains lists, and why `cast-table-ref` returns a list on success.
;; cast-table : (Free-Id-Tableof (Listof Type-Stx))
;; interpretation:
;; A mapping from lifted-contract-def identifiers to the possible existing
;; types of values that the contract has to protect as they go from typed
;; to untyped code.
(define cast-table (make-free-id-table))
;; cast-table-set! : Id Type-Stx -> Void
(define (cast-table-set! id type-stx)
(free-id-table-set! cast-table id type-stx))
;; cast-table-add! : Id Type-Stx -> Void
;; Associates the given type with the given contract-def identifier, to signify
;; that the contract generated by `id` must protect values of type `type-stx`.
(define (cast-table-add! id type-stx)
(free-id-table-update! cast-table id
(λ (lst) (cons type-stx lst))
(λ () '())))
;; cast-table-ref : Id -> (U False Type-Stx)
;; cast-table-ref : Id -> (U False (Listof Type-Stx))
;; On success, returns a list containing all the types of values that the
;; contract must project as they go from typed to untyped code. On failure,
;; returns false.
(define (cast-table-ref id)
(free-id-table-ref cast-table id #f))

View File

@ -0,0 +1,12 @@
#lang typed/racket
(require typed/rackunit)
(: f : (case-> (-> (Boxof String) Any)
(-> (Boxof Integer) Any)))
(define (f x)
(cast x Any))
(check-equal? (f (box "a")) (box "a"))
(check-equal? (f (box 1)) (box 1))