diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-metafunctions.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-metafunctions.rkt index 0c89c55c71..b825c8fa1c 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-metafunctions.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-metafunctions.rkt @@ -14,154 +14,12 @@ tc-results->values) -;; abstract-results -;; -;; Given results from the range of a lambda, abstract any -;; identifier objects into index (numeric) objects. This is effectively -;; doing a kind of De Bruijn indexing for objects. -;; -;; When the body of a lambda is type-checked, its filters and object -;; may refer to variables that are in scope in that body. Since these -;; names are not in scope outside of the lambda, the type of the function -;; will instead store their De Bruijn indices. -;; -;; For example, given the function -;; -;; (λ (x) (number? x)) -;; -;; the typechecker will check the body and return -;; -;; Boolean ; N_x | !N_x ; ∅ -;; -;; but the `x`s have to be converted to indices to get the type -;; -;; N_(0,0) | !N_(0,0) -;; Any -------------------> Boolean -;; ∅ -;; -;; where the index (0,0) indicates the first argument of -;; the current function -;; -;; Comparatively, a curried predicate like -;; -;; (λ (x) (λ (y)(number? x))) -;; -;; gets the type -;; -;; N_(1,0) | !N_(1,0) -;; Any -> Any -------------------> Boolean -;; ∅ -;; -;; (ignoring filters on the first arrow) -;; where the index (1,0) indicates the first argument of -;; the enclosing lambda. -;; -;; The paper "Logical Types for Untyped Languages" takes a different -;; approach where all function types carry their names, so that the first -;; example would have the type: -;; -;; N_x | !N_x -;; x:Any ------------> Boolean -;; ∅ -;; -;; See tc-subst.rkt for the functions that take an abstracted function -;; type and substitute in a concrete object. -;; (define/cond-contract (abstract-results results arg-names) (tc-results/c (listof identifier?) . -> . SomeValues/c) - (define keys (for/list ([(nm k) (in-indexed arg-names)]) (list 0 k))) - (match results - [(tc-any-results: f) (-AnyValues (abo arg-names keys f))] - [(tc-results: ts fs os dty dbound) - (make-ValuesDots - (for/list ([t (in-list ts)] [f (in-list fs)] [o (in-list os)]) - (-result (abstract-type arg-names keys t) - (abstract-filter arg-names keys f) - (abstract-object arg-names keys o))) - (abstract-type arg-names keys dty) - dbound)] - [(tc-results: ts fs os) - (make-Values - (for/list ([t (in-list ts)] [f (in-list fs)] [o (in-list os)]) - (-result (abstract-type arg-names keys t) - (abstract-filter arg-names keys f) - (abstract-object arg-names keys o))))])) - -;; Abstract all given id objects into index objects (keys) in -;; the given type -(define/cond-contract (abstract-type ids keys type) - (-> (listof identifier?) (listof name-ref/c) Type/c Type/c) - (define (at type) (abstract-type ids keys type)) - (define (af filter) (abstract-filter ids keys filter)) - (define (ao obj) (abstract-object ids keys obj)) - (type-case - (#:Type at #:Filter af #:Object ao) - type - [#:arr - dom rng rest drest kws - (let ([at* - ;; when a new function type is encountered, increase - ;; the scope count in the keys so that names are - ;; substituted with the correct level of nesting - (λ (type) - (abstract-type ids (map add-scope keys) type))]) - (make-arr (map at dom) - (at* rng) ; only increase scope in range - (and rest (at rest)) - (and drest (cons (at (car drest)) (cdr drest))) - (map at kws)))])) - -;; Abstract all given id objects into index objects (keys) in -;; the given object -(define/cond-contract (abstract-object ids keys o) - (-> (listof identifier?) (listof name-ref/c) Object? Object?) - (define-lookup: lookup: ids keys) - (match o - [(Path: p (lookup: idx)) (make-Path p idx)] - [_ -empty-obj])) - -;; Abstract all given id objects into index objects (keys) in -;; the given filter set -(define/cond-contract (abstract-filter ids keys fs) - (-> (listof identifier?) (listof name-ref/c) FilterSet/c FilterSet/c) - (match fs - [(FilterSet: f+ f-) - (-FS (abo ids keys f+) (abo ids keys f-))] - [(NoFilter:) -top-filter])) - -(define/cond-contract (abo xs idxs f) - ((listof identifier?) (listof name-ref/c) Filter/c . -> . Filter/c) - (define (rec f) (abo xs idxs f)) - (define (sb-t t) t) - (define-lookup: lookup: xs idxs) - (filter-case (#:Type sb-t #:Filter rec) f - [#:TypeFilter - t p (lookup: idx) - (-filter t idx p)] - [#:NotTypeFilter - t p (lookup: idx) - (-not-filter t idx p)])) - -;; Look up the identifier in a mapping of a list of identifiers -;; to a list of path indices -(define/cond-contract (lookup-index target ids keys) - (-> identifier? (listof identifier?) (listof (list/c integer? integer?)) - (or/c #f (list/c integer? integer?))) - (for/first ([id (in-list ids)] [index (in-list keys)] - #:when (free-identifier=? id target)) - index)) - -;; Generates a match expander to make `lookup-index` convenient -(define-syntax-rule (define-lookup: lookup: ids keys) - (define-match-expander lookup: - (syntax-rules () - [(_ i) - (or ;; No need to look up if it's not an identifier, - ;; since that means it was already abstracted - ;; into an index. - (? identifier? (app (λ (id) (lookup-index id ids keys)) - (? values i))) - i)]))) + (tc-results->values + (replace-names + (for/list ([(nm k) (in-indexed (in-list arg-names))]) (list nm (make-Path null (list 0 k)))) + results))) (define (tc-results->values tc) (match (fix-results tc)