Use a new approach to generating Name contracts
This handles contract generation for recursive or mutually recursive Name types in the static contract framework. Instead of just generating recursive-sc static contracts, it memoizes the recursive contract within a single type->contract call by indirecting through a table. When static contracts are instantiated, the table is consulted for computing contract kind information and for generating the actual contracts for the recursive names. original commit: 608dfcf3356fb4957331dc7c140b9ac176d36991
This commit is contained in:
Asumu Takikawa
parent
55c8541c82
commit
573f6506b3
|
|
@ -149,15 +149,16 @@
|
|||
[(both) 'both]))
|
||||
|
||||
(define (type->contract ty init-fail #:typed-side [typed-side #t] #:kind [kind 'impersonator])
|
||||
(let/ec escape
|
||||
(define (fail #:reason [reason #f]) (escape (init-fail #:reason reason)))
|
||||
(instantiate
|
||||
(optimize
|
||||
(type->static-contract ty #:typed-side typed-side fail)
|
||||
#:trusted-positive typed-side
|
||||
#:trusted-negative (not typed-side))
|
||||
fail
|
||||
kind)))
|
||||
(with-new-name-tables
|
||||
(let/ec escape
|
||||
(define (fail #:reason [reason #f]) (escape (init-fail #:reason reason)))
|
||||
(instantiate
|
||||
(optimize
|
||||
(type->static-contract ty #:typed-side typed-side fail)
|
||||
#:trusted-positive typed-side
|
||||
#:trusted-negative (not typed-side))
|
||||
fail
|
||||
kind))))
|
||||
|
||||
|
||||
|
||||
|
|
@ -217,72 +218,17 @@
|
|||
(recursive-sc-use name*))])]
|
||||
;; Implicit recursive aliases
|
||||
[(Name: name-id dep-ids args #f)
|
||||
;; FIXME: this may not be correct for different aliases that have
|
||||
;; the same name that are somehow used together, if that's
|
||||
;; possible
|
||||
(define name (syntax-e name-id))
|
||||
(define deps (map syntax-e dep-ids))
|
||||
(cond [;; recursive references are looked up, see F case
|
||||
(hash-ref recursive-values name #f) =>
|
||||
(λ (rv) (triple-lookup rv typed-side))]
|
||||
(cond [;; recursive references are looked up in a special table
|
||||
;; that's handled differently by sc instantiation
|
||||
(lookup-name-sc name-id typed-side)]
|
||||
[else
|
||||
;; see Mu case, which uses similar machinery
|
||||
(match-define (and n*s (list untyped-n* typed-n* both-n*))
|
||||
(generate-temporaries (list name name name)))
|
||||
(define-values (untyped-deps typed-deps both-deps)
|
||||
(values (generate-temporaries deps)
|
||||
(generate-temporaries deps)
|
||||
(generate-temporaries deps)))
|
||||
;; Set recursive references for the `name` itself
|
||||
(define *rv
|
||||
(hash-set recursive-values name
|
||||
(triple (recursive-sc-use untyped-n*)
|
||||
(recursive-sc-use typed-n*)
|
||||
(recursive-sc-use both-n*))))
|
||||
;; Add in references for the dependency aliases
|
||||
(define rv
|
||||
(for/fold ([rv *rv])
|
||||
([dep (in-list deps)]
|
||||
[untyped-dep (in-list untyped-deps)]
|
||||
[typed-dep (in-list typed-deps)]
|
||||
[both-dep (in-list both-deps)])
|
||||
(hash-set rv dep
|
||||
(triple (recursive-sc-use untyped-dep)
|
||||
(recursive-sc-use typed-dep)
|
||||
(recursive-sc-use both-dep)))))
|
||||
(define rv recursive-values)
|
||||
(define resolved-name (resolve-once type))
|
||||
(define resolved-deps
|
||||
(for/list ([dep (in-list dep-ids)])
|
||||
(resolve-once (lookup-type-alias dep values))))
|
||||
|
||||
;; resolved-deps->scs : (U 'untyped 'typed 'both)
|
||||
;; -> (Listof Static-Contract)
|
||||
(define (resolved-deps->scs typed-side)
|
||||
(for/list ([resolved-dep (in-list resolved-deps)]
|
||||
[dep (in-list deps)])
|
||||
(loop resolved-dep typed-side rv)))
|
||||
|
||||
;; Now actually generate the static contracts
|
||||
(case typed-side
|
||||
[(both) (recursive-sc
|
||||
(append (list both-n*) both-deps)
|
||||
(cons (loop resolved-name 'both rv)
|
||||
(resolved-deps->scs 'both))
|
||||
(recursive-sc-use both-n*))]
|
||||
[(typed untyped)
|
||||
(define untyped (loop resolved-name 'untyped rv))
|
||||
(define typed (loop resolved-name 'typed rv))
|
||||
(define both (loop resolved-name 'both rv))
|
||||
(define-values (untyped-dep-scs typed-dep-scs both-dep-scs)
|
||||
(values
|
||||
(resolved-deps->scs 'untyped)
|
||||
(resolved-deps->scs 'typed)
|
||||
(resolved-deps->scs 'both)))
|
||||
(recursive-sc
|
||||
(append n*s untyped-deps typed-deps both-deps)
|
||||
(append (list untyped typed both)
|
||||
untyped-dep-scs typed-dep-scs both-dep-scs)
|
||||
(recursive-sc-use (if (from-typed? typed-side) typed-n* untyped-n*)))])])]
|
||||
(register-name-sc name-id
|
||||
(λ () (loop resolved-name 'untyped rv))
|
||||
(λ () (loop resolved-name 'typed rv))
|
||||
(λ () (loop resolved-name 'both rv)))
|
||||
(lookup-name-sc name-id typed-side)])]
|
||||
;; Ordinary type applications or struct type names, just resolve
|
||||
[(or (App: _ _ _) (Name: _ _ _ #t)) (t->sc (resolve-once type))]
|
||||
[(Univ:) (if (from-typed? typed-side) any-wrap/sc any/sc)]
|
||||
|
|
|
|||
|
|
@ -0,0 +1,78 @@
|
|||
#lang racket/base
|
||||
|
||||
;; Static contracts for Name types
|
||||
;;
|
||||
;; This module keeps track of Name types global to
|
||||
;; a single type->contract use, which allows the instantiation
|
||||
;; process to lift out the contracts for the potentially
|
||||
;; mutually recursive Name types. This reduces the amount of
|
||||
;; duplication that would result if we used ordinary recursive
|
||||
;; static contracts.
|
||||
|
||||
(require "../structures.rkt"
|
||||
"../constraints.rkt"
|
||||
racket/contract
|
||||
racket/dict
|
||||
racket/syntax
|
||||
syntax/id-table)
|
||||
|
||||
(provide with-new-name-tables
|
||||
get-all-name-defs
|
||||
lookup-name-sc
|
||||
lookup-name-defs
|
||||
register-name-sc)
|
||||
|
||||
(define name-sc-table (make-parameter (make-free-id-table)))
|
||||
(define name-defs-table (make-parameter (make-free-id-table)))
|
||||
|
||||
(define-syntax-rule (with-new-name-tables e)
|
||||
(parameterize ([name-sc-table (make-free-id-table)]
|
||||
[name-defs-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))
|
||||
(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))
|
||||
(and result
|
||||
(case typed-side
|
||||
[(both) (car result)]
|
||||
[(typed) (cadr result)]
|
||||
[(untyped) (caddr result)])))
|
||||
|
||||
(define (lookup-name-defs name)
|
||||
(free-id-table-ref (name-defs-table) name #f))
|
||||
|
||||
(define (register-name-sc name 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)))
|
||||
(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)))
|
||||
|
||||
(struct name-combinator combinator (gen-name)
|
||||
#:transparent
|
||||
#:property prop:combinator-name "name/sc"
|
||||
#:methods gen:sc
|
||||
[(define (sc-map v f) v)
|
||||
(define (sc-traverse v f)
|
||||
(void))
|
||||
(define (sc->contract v f)
|
||||
(name-combinator-gen-name v))
|
||||
(define (sc->constraints v f)
|
||||
(variable-contract-restrict (name-combinator-gen-name v)))])
|
||||
|
|
@ -9,6 +9,7 @@
|
|||
racket/sequence
|
||||
racket/contract
|
||||
(for-template racket/base racket/contract)
|
||||
"combinators/name.rkt"
|
||||
"kinds.rkt"
|
||||
"parametric-check.rkt"
|
||||
"structures.rkt"
|
||||
|
|
@ -39,13 +40,19 @@
|
|||
(contract-restrict-recursive-values (compute-constraints sc kind)))))))
|
||||
|
||||
(define (compute-constraints sc max-kind)
|
||||
(define name-defs (get-all-name-defs))
|
||||
(define (recur sc)
|
||||
(match sc
|
||||
[(recursive-sc names values body)
|
||||
(close-loop names (map recur values) (recur body))]
|
||||
[(? sc?)
|
||||
(sc->constraints sc recur)]))
|
||||
(define constraints (recur sc))
|
||||
(define constraints
|
||||
(if (null? name-defs)
|
||||
(recur sc)
|
||||
(close-loop (apply append (dict-keys name-defs))
|
||||
(map recur (apply append (dict-values name-defs)))
|
||||
(recur sc))))
|
||||
(validate-constraints (add-constraint constraints max-kind))
|
||||
constraints)
|
||||
|
||||
|
|
@ -89,4 +96,13 @@
|
|||
#`(letrec (#,@bindings #,@raw-bindings) #,(recur body))]
|
||||
[(? sc? sc)
|
||||
(sc->contract sc recur)]))
|
||||
(recur sc))
|
||||
(define name-defs (get-all-name-defs))
|
||||
(cond [(null? name-defs) (recur sc)]
|
||||
[else
|
||||
(define bindings
|
||||
(for/list ([name (in-list (apply append (dict-keys name-defs)))]
|
||||
[sc (in-list (apply append (dict-values name-defs)))])
|
||||
#`[#,name (recursive-contract #,(recur sc)
|
||||
#,(kind->keyword
|
||||
(hash-ref recursive-kinds name)))]))
|
||||
#`(letrec (#,@bindings) #,(recur sc))]))
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user