Replace abstract-results with replace-names.

Also moves large comment over to with replace names since it is now
doing the heavy lifting.

original commit: 050c1022c94a933dde368c20ad5701dd76768a39

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)