Adjust contract generation for some Instance types

This commit is contained in:
Asumu Takikawa 2014-11-25 16:45:57 -05:00
parent ea942c2110
commit e80f17cbad
2 changed files with 36 additions and 25 deletions

View File

@ -334,15 +334,15 @@
[(Name: name-id args #f)
(cond [;; recursive references are looked up in a special table
;; that's handled differently by sc instantiation
(lookup-name-sc name-id typed-side)]
(lookup-name-sc type typed-side)]
[else
(define rv recursive-values)
(define resolved-name (resolve-once type))
(register-name-sc name-id
(register-name-sc type
(λ () (loop resolved-name 'untyped rv))
(λ () (loop resolved-name 'typed rv))
(λ () (loop resolved-name 'both rv)))
(lookup-name-sc name-id typed-side)])]
(lookup-name-sc type typed-side)])]
;; Ordinary type applications or struct type names, just resolve
[(or (App: _ _ _) (Name/struct:)) (t->sc (resolve-once type))]
[(Univ:) (if (from-typed? typed-side) any-wrap/sc any/sc)]
@ -431,10 +431,20 @@
n*s
(list untyped typed both)
(recursive-sc-use (if (from-typed? typed-side) typed-n* untyped-n*)))])]
[(Instance: (? Mu? t))
(t->sc (make-Instance (resolve-once t)))]
;; Don't directly use the class static contract generated for Name,
;; because that will get an #:opaque class contract. This will do the
;; wrong thing for object types since it errors too eagerly.
[(Instance: (? Name? t))
(instanceof/sc (t->sc t))]
#:when (Class? (resolve-once t))
(cond [(lookup-name-sc type typed-side)]
[else
(define rv recursive-values)
(define resolved (make-Instance (resolve-once t)))
(register-name-sc type
(λ () (loop resolved 'untyped rv))
(λ () (loop resolved 'typed rv))
(λ () (loop resolved 'both rv)))
(lookup-name-sc type typed-side)])]
[(Instance: (Class: _ _ fields methods _ _))
(match-define (list (list field-names field-types) ...) fields)
(match-define (list (list public-names public-types) ...) methods)

View File

@ -11,6 +11,7 @@
(require "../structures.rkt"
"../constraints.rkt"
"../../rep/type-rep.rkt" ; only for contract
racket/contract
racket/dict
racket/match
@ -29,15 +30,15 @@
static-contract?
static-contract?
static-contract?)))]
[lookup-name-sc (-> identifier? symbol? (or/c #f static-contract?))]
[register-name-sc (-> identifier?
[lookup-name-sc (-> Type/c symbol? (or/c #f static-contract?))]
[register-name-sc (-> Type/c
(-> static-contract?)
(-> static-contract?)
(-> static-contract?)
any)]))
(define name-sc-table (make-parameter (make-free-id-table)))
(define name-defs-table (make-parameter (make-free-id-table)))
(define name-sc-table (make-parameter (make-hash)))
(define name-defs-table (make-parameter (make-hash)))
;; Use this table to track whether a contract has already been
;; generated for this name type yet. Stores booleans.
@ -52,42 +53,42 @@
(free-id-table-set! (name-defined-table) name #t))
(define-syntax-rule (with-new-name-tables e)
(parameterize ([name-sc-table (make-free-id-table)]
[name-defs-table (make-free-id-table)]
(parameterize ([name-sc-table (make-hash)]
[name-defs-table (make-hash)]
[name-defined-table (make-free-id-table)])
e))
(define (get-all-name-defs)
(define name-scs (name-sc-table))
(for/list ([(name defs) (in-dict (name-defs-table))])
(define scs (free-id-table-ref name-scs name))
(for/list ([(type defs) (in-dict (name-defs-table))])
(define scs (hash-ref name-scs type))
(define gen-names (map name-combinator-gen-name scs))
(cons gen-names defs)))
(define (lookup-name-sc name typed-side)
(define result (free-id-table-ref (name-sc-table) name #f))
(define (lookup-name-sc type typed-side)
(define result (hash-ref (name-sc-table) type #f))
(and result
(case typed-side
[(both) (car result)]
[(typed) (cadr result)]
[(untyped) (caddr result)])))
(define (register-name-sc name typed-thunk untyped-thunk both-thunk)
(define (register-name-sc type typed-thunk untyped-thunk both-thunk)
(define-values (typed-name untyped-name both-name)
(values (generate-temporary)
(generate-temporary)
(generate-temporary)))
(free-id-table-set! (name-sc-table)
name
(list (name-combinator null typed-name)
(name-combinator null untyped-name)
(name-combinator null both-name)))
(hash-set! (name-sc-table)
type
(list (name-combinator null typed-name)
(name-combinator null untyped-name)
(name-combinator null both-name)))
(define typed-sc (typed-thunk))
(define untyped-sc (untyped-thunk))
(define both-sc (both-thunk))
(free-id-table-set! (name-defs-table)
name
(list typed-sc untyped-sc both-sc)))
(hash-set! (name-defs-table)
type
(list typed-sc untyped-sc both-sc)))
(struct name-combinator combinator (gen-name)
#:transparent