From 573f6506b37c0cd4ae9be8263553c08898f579bc Mon Sep 17 00:00:00 2001 From: Asumu Takikawa Date: Mon, 20 Oct 2014 21:06:31 -0400 Subject: [PATCH] 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 --- .../typed-racket/private/type-contract.rkt | 92 ++++--------------- .../static-contracts/combinators/name.rkt | 78 ++++++++++++++++ .../static-contracts/instantiate.rkt | 20 +++- 3 files changed, 115 insertions(+), 75 deletions(-) create mode 100644 pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/static-contracts/combinators/name.rkt diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/type-contract.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/type-contract.rkt index fca59e1d..8d2be1c4 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/type-contract.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/private/type-contract.rkt @@ -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)] diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/static-contracts/combinators/name.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/static-contracts/combinators/name.rkt new file mode 100644 index 00000000..522c4d72 --- /dev/null +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/static-contracts/combinators/name.rkt @@ -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)))]) diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/static-contracts/instantiate.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/static-contracts/instantiate.rkt index 18aeaf27..d35a5277 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/static-contracts/instantiate.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/static-contracts/instantiate.rkt @@ -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))]))