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

Use absent in some row poly class contracts

Browse Source 
When exporting row polymorphic functions from TR, just
use absent clauses to ensure that TR won't accidentally
try to add pre-existing fields/methods. No sealing is
needed because the typechecker enforces parameteric use
of the class.
This commit is contained in:
Asumu Takikawa 2015-02-28 00:39:32 -05:00
parent d30a824f02
commit 33543ce054
5 changed files with 43 additions and 25 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
typed-racket-lib/typed-racket/env/row-constraint-env.rkt vendored
View File

@ -36,7 +36,7 @@
(define (has-row-constraints? v)
(not (not (assq v (current-row-constraints)))))
;; lookup-row-constraints : Symbol -> Type
;; lookup-row-constraints : Symbol -> RowConstraint
;; returns the mapped-to constraints or #f
(define (lookup-row-constraints var)
(cdr (assq var (current-row-constraints))))

24
typed-racket-lib/typed-racket/private/type-contract.rkt
View File

@ -7,7 +7,7 @@
syntax/parse
(rep type-rep filter-rep object-rep)
(utils tc-utils)
(env type-name-env)
(env type-name-env row-constraint-env)
(rep rep-utils)
(types resolve union utils printer)
(prefix-in t: (types abbrev numeric-tower))
@ -454,7 +454,7 @@
public-names (map t->sc/meth public-types))
(map (λ (n sc) (member-spec 'field n sc))
field-names (map t->sc/both field-types))))]
[(Class: _ inits fields publics augments _)
[(Class: row-var inits fields publics augments _)
(match-define (list (list init-names init-types _) ...) inits)
(match-define (list (list field-names field-types) ...) fields)
(match-define (list (list public-names public-types) ...) publics)
@ -469,7 +469,19 @@
[type (in-list public-types)]
#:unless (memq name pubment-names))
(values name type)))
(class/sc (from-untyped? typed-side)
;; we need to generate absent clauses for non-opaque class contracts
;; that occur inside of a mixin type
(define absents
(cond [(F? row-var)
(define constraints (lookup-row-constraints (F-n row-var)))
;; the constraints with no corresponding type/contract need
;; to be absent
(append (remove* field-names (cadr constraints))
(remove* public-names (caddr constraints)))]
[else null]))
(class/sc ;; only enforce opaqueness if there's no row variable
;; and we are importing from untyped
(and (from-untyped? typed-side) (not row-var))
(append
(map (λ (n sc) (member-spec 'override n sc))
override-names (map t->sc/meth override-types))
@ -480,7 +492,8 @@
(map (λ (n sc) (member-spec 'init n sc))
init-names (map t->sc/neg init-types))
(map (λ (n sc) (member-spec 'field n sc))
field-names (map t->sc/both field-types))))]
field-names (map t->sc/both field-types)))
absents)]
[(Struct: nm par (list (fld: flds acc-ids mut?) ...) proc poly? pred?)
(cond
[(dict-ref recursive-values nm #f)]
@ -667,7 +680,8 @@
(if (not (from-untyped? typed-side))
(let ((recursive-values (for/fold ([rv recursive-values]) ([v vs])
(hash-set rv v (same any/sc)))))
(t->sc body #:recursive-values recursive-values))
(extend-row-constraints vs (list constraints)
(t->sc body #:recursive-values recursive-values)))
;; FIXME: needs sealing contracts, disabled for now
(fail #:reason "cannot generate contract for row polymorphic type")))

19
typed-racket-lib/typed-racket/static-contracts/combinators/object.rkt
View File

@ -16,7 +16,7 @@
(contract-out
[struct member-spec ([modifier symbol?] [id symbol?] [sc static-contract?])]
[object/sc (boolean? (listof object-member-spec?) . -> . static-contract?)]
[class/sc (boolean? (listof member-spec?) . -> . static-contract?)]
[class/sc (boolean? (listof member-spec?) (listof symbol?) . -> . static-contract?)]
[instanceof/sc (static-contract? . -> . static-contract?)]))
@ -41,17 +41,17 @@
(define (sc->constraints v f)
(merge-restricts* 'impersonator (map f (member-seq->list (combinator-args v)))))])
(struct class-combinator combinator (opaque)
(struct class-combinator combinator (opaque absents)
#:transparent
#:property prop:combinator-name "class/sc"
#:methods gen:sc
[(define (sc-map v f)
(match v
[(class-combinator args opaque)
(class-combinator (member-seq-sc-map f args) opaque)]))
[(class-combinator args opaque absents)
(class-combinator (member-seq-sc-map f args) opaque absents)]))
(define (sc-traverse v f)
(match v
[(class-combinator args opaque)
[(class-combinator args opaque absents)
(member-seq-sc-map f args)
(void)]))
(define (sc->contract v f)
@ -103,8 +103,8 @@
(define (object/sc opaque? specs)
(object-combinator (member-seq specs) opaque?))
(define (class/sc opaque? specs)
(class-combinator (member-seq specs) opaque?))
(define (class/sc opaque? specs absents)
(class-combinator (member-seq specs) opaque? absents))
(define (instanceof/sc class)
(instanceof-combinator (list class)))
@ -137,7 +137,7 @@
#,@(map (member-spec->form f) vals))]))
(define (class/sc->contract v f)
(match v
[(class-combinator (member-seq vals) opaque)
[(class-combinator (member-seq vals) opaque absents)
(define-values (override-names override-ctcs)
(spec->id/ctc f 'override vals))
(define-values (pubment-names pubment-ctcs)
@ -165,7 +165,8 @@
(inherit [override-name override-temp] ...)
[pubment-name pubment-temp] ...
(augment [pubment-name pubment-temp] ...)
(inherit [pubment-name pubment-temp] ...)))]))
(inherit [pubment-name pubment-temp] ...)
(absent #,@absents)))]))
(define (instance/sc->contract v f)
(match v
[(instanceof-combinator (list class))

11
typed-racket-test/unit-tests/contract-tests.rkt
View File

@ -211,20 +211,23 @@
(t-sc (Un (-lst Univ) -Number) (or/sc number/sc (listof/sc any-wrap/sc)))
;; classes
(t-sc (-class) (class/sc #f null))
(t-sc (-class) (class/sc #f null null))
(t-sc (-class #:init ([x -Number #f] [y -Number #f]))
(class/sc #f
(list (member-spec 'init 'x number/sc)
(member-spec 'init 'y number/sc))))
(member-spec 'init 'y number/sc))
null))
(t-sc (-class #:init ([x -Number #f] [y -Number #t]))
(class/sc #f
(list (member-spec 'init 'x number/sc)
(member-spec 'init 'y number/sc))))
(member-spec 'init 'y number/sc))
null))
(t-sc (-class #:init ([x -Number #f]) #:init-field ([y -Integer #f]))
(class/sc #f
(list (member-spec 'init 'x number/sc)
(member-spec 'init 'y integer/sc)
(member-spec 'field 'y integer/sc))))
(member-spec 'field 'y integer/sc))
null))
(t (-class #:method ([m (-poly (x) (-> x x))])))
(t (-class #:method ([m (-polydots (x) (->... (list) (x x) -Void))])))
(t (-class #:method ([m (-polyrow (x) (list null null null null)

12
typed-racket-test/unit-tests/static-contract-optimizer-tests.rkt
View File

@ -285,14 +285,14 @@
#:neg (object/sc #f (list (member-spec 'field 'x list?/sc))))
(check-optimize
(class/sc #t (list (member-spec 'field 'x (listof/sc any/sc))))
#:pos (class/sc #t (list (member-spec 'field 'x list?/sc)))
#:neg (class/sc #t (list (member-spec 'field 'x list?/sc))))
(class/sc #t (list (member-spec 'field 'x (listof/sc any/sc))) null)
#:pos (class/sc #t (list (member-spec 'field 'x list?/sc)) null)
#:neg (class/sc #t (list (member-spec 'field 'x list?/sc)) null))
(check-optimize
(class/sc #f (list (member-spec 'field 'x (listof/sc any/sc))))
#:pos (class/sc #f (list (member-spec 'field 'x list?/sc)))
#:neg (class/sc #f (list (member-spec 'field 'x list?/sc))))
(class/sc #f (list (member-spec 'field 'x (listof/sc any/sc))) null)
#:pos (class/sc #f (list (member-spec 'field 'x list?/sc)) null)
#:neg (class/sc #f (list (member-spec 'field 'x list?/sc)) null))
(check-optimize
(recursive-sc (list foo-id bar-id)