From f9385af461009850f2455dab3fbd6690ace2da77 Mon Sep 17 00:00:00 2001 From: Andrew Kent Date: Mon, 21 Nov 2016 15:47:40 -0500 Subject: [PATCH] clean up tc-let-unit This commit cleans up some helper functions that have been pretty awful for a while. The code is (hopefully) more readable and it does less work (i.e. unneeded substitutions are no longer performed). --- .../typed-racket/env/lexical-env.rkt | 73 +++--- .../typed-racket/env/type-env-structs.rkt | 104 ++++---- .../typecheck/check-class-unit.rkt | 63 +++-- .../typecheck/check-unit-unit.rkt | 20 +- .../typed-racket/typecheck/tc-envops.rkt | 7 +- .../typed-racket/typecheck/tc-lambda-unit.rkt | 63 ++--- .../typed-racket/typecheck/tc-let-unit.rkt | 240 ++++++++++-------- .../typed-racket/typecheck/tc-send.rkt | 8 +- .../typed-racket/typecheck/tc-subst.rkt | 11 +- .../unit-tests/typecheck-tests.rkt | 12 +- 10 files changed, 336 insertions(+), 265 deletions(-) diff --git a/typed-racket-lib/typed-racket/env/lexical-env.rkt b/typed-racket-lib/typed-racket/env/lexical-env.rkt index 211e4283..406ddea4 100644 --- a/typed-racket-lib/typed-racket/env/lexical-env.rkt +++ b/typed-racket-lib/typed-racket/env/lexical-env.rkt @@ -20,57 +20,60 @@ (provide lexical-env with-lexical-env - with-lexical-env/extend-types - with-lexical-env/extend-types+aliases) + with-extended-lexical-env) (provide/cond-contract [lookup-type/lexical ((identifier?) (env? #:fail (or/c #f (-> any/c #f))) . ->* . (or/c Type? #f))] [lookup-alias/lexical ((identifier?) (env?) . ->* . (or/c Path? Empty?))]) ;; the current lexical environment -(define lexical-env (make-parameter empty-prop-env)) +(define lexical-env (make-parameter empty-env)) ;; run code in a new env (define-syntax-rule (with-lexical-env e . b) (parameterize ([lexical-env e]) . b)) ;; run code in an extended env -(define-syntax-rule (with-lexical-env/extend-types is ts . b) - (with-lexical-env (extend/values (lexical-env) is ts) . b)) +(define-syntax (with-extended-lexical-env stx) + (syntax-parse stx + [(_ [#:identifiers ids:expr + #:types tys:expr + (~optional (~seq #:aliased-objects objs:expr) + #:defaults ([objs #'#f]))] + . body) + (syntax/loc stx + (with-lexical-env (env-extend/bindings (lexical-env) ids tys objs) . body))])) -;; run code in an extended env + an alias extension -(define-syntax-rule (with-lexical-env/extend-types+aliases is ts os . b) - (with-lexical-env (extend+alias/values (lexical-env) is ts os) . b)) ;; find the type of identifier i, looking first in the lexical env, then in the top-level env ;; identifier -> Type (define (lookup-type/lexical i [env (lexical-env)] #:fail [fail #f]) - (lookup env i (λ (i) (lookup-type i (λ () - (cond - [(syntax-property i 'constructor-for) - => (λ (prop) - (define orig (un-rename prop)) - (define t (lookup-type/lexical orig env)) - (register-type i t) - t)] - [(syntax-procedure-alias-property i) - => (λ (prop) - (define orig (car (flatten prop))) - (define t (lookup-type/lexical orig env)) - (register-type i t) - t)] - [(syntax-procedure-converted-arguments-property i) - => (λ (prop) - (define orig (car (flatten prop))) - (define pre-t - (lookup-type/lexical - orig env #:fail (lambda (i) (lookup-fail i) #f))) - (define t (if pre-t - (kw-convert pre-t #f) - Err)) - (register-type i t) - t)] - [else ((or fail lookup-fail) i)])))))) + (env-lookup env i (λ (i) (lookup-type i (λ () + (cond + [(syntax-property i 'constructor-for) + => (λ (prop) + (define orig (un-rename prop)) + (define t (lookup-type/lexical orig env)) + (register-type i t) + t)] + [(syntax-procedure-alias-property i) + => (λ (prop) + (define orig (car (flatten prop))) + (define t (lookup-type/lexical orig env)) + (register-type i t) + t)] + [(syntax-procedure-converted-arguments-property i) + => (λ (prop) + (define orig (car (flatten prop))) + (define pre-t + (lookup-type/lexical + orig env #:fail (lambda (i) (lookup-fail i) #f))) + (define t (if pre-t + (kw-convert pre-t #f) + Err)) + (register-type i t) + t)] + [else ((or fail lookup-fail) i)])))))) ;; looks up the representative object for an id (i.e. itself or an alias if one exists) (define (lookup-alias/lexical i [env (lexical-env)]) - (lookup-alias env i -id-path)) \ No newline at end of file + (env-lookup-alias env i -id-path)) diff --git a/typed-racket-lib/typed-racket/env/type-env-structs.rkt b/typed-racket-lib/typed-racket/env/type-env-structs.rkt index 39d76e9d..bc0e0d6a 100644 --- a/typed-racket-lib/typed-racket/env/type-env-structs.rkt +++ b/typed-racket-lib/typed-racket/env/type-env-structs.rkt @@ -16,71 +16,87 @@ #:transparent #:property prop:custom-write (lambda (e prt mode) - (fprintf prt "(env ~a ~a)" (free-id-table-map (env-types e) list) (env-props e)))) + (fprintf prt "(env ~a ~a ~a)" + (free-id-table-map (env-types e) + (λ (id ty) (format "[~a ∈ ~a]" id ty))) + (env-props e) + (free-id-table-map (env-types e) + (λ (id ty) (format "[~a ≡ ~a]" id ty)))))) + +;; when interning is removed, the -empty-obj +;; shorthand will be visible in this file. until +;; then this will do -amk +(define -empty-obj (make-Empty)) (provide/cond-contract [env? predicate/c] - [extend (env? identifier? Type? . -> . env?)] - [extend/values (env? (listof identifier?) (listof Type?) . -> . env?)] - [lookup (env? identifier? (identifier? . -> . any) . -> . any)] + [env-set-type (env? identifier? Type? . -> . env?)] + [env-extend/bindings (env? (listof identifier?) + (listof Type?) + (or/c (listof OptObject?) #f) + . -> . + env?)] + [env-lookup (env? identifier? (identifier? . -> . any) . -> . any)] [env-props (env? . -> . (listof Prop?))] - [replace-props (env? (listof Prop?) . -> . env?)] - [empty-prop-env env?] - [extend+alias/values (env? (listof identifier?) (listof Type?) (listof OptObject?) . -> . env?)] - [lookup-alias (env? identifier? (identifier? . -> . (or/c OptObject? #f)) . -> . (or/c OptObject? #f))]) + [env-replace-props (env? (listof Prop?) . -> . env?)] + [empty-env env?] + [env-lookup-alias (env? identifier? (identifier? . -> . (or/c OptObject? #f)) . -> . (or/c OptObject? #f))]) -(define empty-prop-env +(define empty-env (env (make-immutable-free-id-table) null (make-immutable-free-id-table))) -(define (replace-props e props) +(define (env-replace-props e props) (match-let ([(env tys _ als) e]) (env tys props als))) -(define (lookup e key fail) +(define (env-lookup e key fail) (match-let ([(env tys _ _) e]) (free-id-table-ref tys key (λ () (fail key))))) -;; extend that works on single arguments -(define (extend e k v) - (extend/values e (list k) (list v))) - -;; extends an environment with types (no aliases) -(define (extend/values e ks vs) - (match-let* ([(env tys ps als) e] - [tys* (for/fold ([tys tys]) ([k (in-list ks)] [v (in-list vs)]) - (free-id-table-set tys k v))]) - (env tys* ps als))) +;; like hash-set, but for the type of an ident in the lexical environment +(define (env-set-type e ident type) + (match-let ([(env tys ps als) e]) + (env (free-id-table-set tys ident type) ps als))) ;; extends an environment with types and aliases -(define (extend+alias/values e ids ts os) - (match-let*-values - ([((env tys ps als)) e] - [(tys* als*) (for/fold ([tys tys] - [als als]) - ([id (in-list ids)] - [t (in-list ts)] - [o (in-list os)]) - (match o - ;; no alias, so just record the type as usual - [(Empty:) - (values (free-id-table-set tys id t) als)] - ;; id is aliased to an identifier - [(Path: '() id*) - ;; record the alias relation *and* type of that alias id - (values (free-id-table-set tys id* t) - (free-id-table-set als id o))] - ;; id is aliased to an object with a non-empty path - [(Path: p x) - ;; just record the alias - (values tys (free-id-table-set als id o))]))]) - (env tys* ps als*))) +;; e : the 'env' struct to be updated +;; idents : the identifiers which are getting types (or aliases) +;; types : the types for the 'idents' +;; aliased-objs : what object is each x ∈ 'idents' an alias for +;; (Empty means it does not alias anything). If +;; there are no aliases, you can pass #f +;; for 'aliased-objs' to simplify the computation. +(define (env-extend/bindings e idents types maybe-aliased-objs) + (match-define (env tys ps als) e) + ;; NOTE: we mutate the identifiers 'tys' and 'als' for convenience, + ;; but the free-id-tables themselves are immutable. + (define (update/type! id t) + (set! tys (free-id-table-set tys id t))) + (define (update/alias! id o) + (set! als (free-id-table-set als id o))) + (define (update/type+alias! id t o) + (match o + ;; no alias, so just record the type as usual + [(Empty:) (update/type! id t)] + ;; 'id' is aliased to the identifier 'id*'; + ;; record the alias relation 'id ≡ id*' *and* that 'id* ∈ t' + [(Path: '() id*) (update/type! id* t) + (update/alias! id o)] + ;; id is aliased to an object which is not a simple identifier; + ;; just record the alias. (NOTE: if we move to supporting more + ;; complicated objects, we _may_ want to add o ∈ t to Γ as well) + [o (update/alias! id o)])) + (if maybe-aliased-objs + (for-each update/type+alias! idents types maybe-aliased-objs) + (for-each update/type! idents types)) + (env tys ps als)) -(define (lookup-alias e key fail) +(define (env-lookup-alias e key fail) (match-let ([(env _ _ als) e]) (free-id-table-ref als key (λ () (fail key))))) diff --git a/typed-racket-lib/typed-racket/typecheck/check-class-unit.rkt b/typed-racket-lib/typed-racket/typecheck/check-class-unit.rkt index e4ff8525..4eee25f9 100644 --- a/typed-racket-lib/typed-racket/typecheck/check-class-unit.rkt +++ b/typed-racket-lib/typed-racket/typecheck/check-class-unit.rkt @@ -600,36 +600,41 @@ local-private-table private-method-types self-type)) (do-timestamp "built local tables") - (with-lexical-env/extend-types lexical-names/top-level lexical-types/top-level - (check-super-new super-new super-inits super-init-rest)) - (do-timestamp "checked super-new") - (with-lexical-env/extend-types lexical-names/top-level lexical-types/top-level + + (with-extended-lexical-env + [#:identifiers lexical-names/top-level + #:types lexical-types/top-level] + (check-super-new super-new super-inits super-init-rest) + (do-timestamp "checked super-new") (for ([stx other-top-level-exprs]) - (tc-expr stx))) - (do-timestamp "checked other top-level exprs") - (with-lexical-env/extend-types lexical-names/top-level lexical-types/top-level + (tc-expr stx)) + (do-timestamp "checked other top-level exprs") (check-field-set!s (hash-ref parse-info 'initializer-body) synthesized-init-val-stxs - inits)) - (do-timestamp "checked field initializers") - (define checked-method-types - (with-lexical-env/extend-types lexical-names lexical-types - (check-methods (append (hash-ref parse-info 'pubment-names) - (hash-ref parse-info 'overridable-names)) - internal-external-mapping method-stxs - methods self-type))) - (do-timestamp "checked methods") - (define checked-augment-types - (with-lexical-env/extend-types lexical-names lexical-types - (check-methods (hash-ref parse-info 'augment-names) - internal-external-mapping method-stxs - augments self-type))) - (do-timestamp "checked augments") - (with-lexical-env/extend-types lexical-names lexical-types - (check-private-methods method-stxs (hash-ref parse-info 'private-names) - private-method-types self-type)) - (do-timestamp "checked privates") - (do-timestamp "finished methods") + inits) + (do-timestamp "checked field initializers")) + + (define-values (checked-method-types checked-augment-types) + (with-extended-lexical-env + [#:identifiers lexical-names + #:types lexical-types] + (define checked-method-types + (check-methods (append (hash-ref parse-info 'pubment-names) + (hash-ref parse-info 'overridable-names)) + internal-external-mapping method-stxs + methods self-type)) + (do-timestamp "checked methods") + (define checked-augment-types + (check-methods (hash-ref parse-info 'augment-names) + internal-external-mapping method-stxs + augments self-type)) + (do-timestamp "checked augments") + (check-private-methods method-stxs (hash-ref parse-info 'private-names) + private-method-types self-type) + (do-timestamp "checked privates") + (do-timestamp "finished methods") + (values checked-method-types checked-augment-types))) + (define final-class-type (merge-types self-type checked-method-types checked-augment-types)) (check-method-presence-and-absence @@ -1119,7 +1124,9 @@ (length temp-names) (length init-types))) ;; Extend lexical type env with temporaries introduced in the ;; expansion of the field initialization or setter - (with-lexical-env/extend-types temp-names init-types + (with-extended-lexical-env + [#:identifiers temp-names + #:types init-types] (check-field-set!s #'(begins ...) synthed-stxs inits))] [_ (void)]))) diff --git a/typed-racket-lib/typed-racket/typecheck/check-unit-unit.rkt b/typed-racket-lib/typed-racket/typecheck/check-unit-unit.rkt index 04617bb3..9fa2b909 100644 --- a/typed-racket-lib/typed-racket/typecheck/check-unit-unit.rkt +++ b/typed-racket-lib/typed-racket/typecheck/check-unit-unit.rkt @@ -533,12 +533,12 @@ ;; but these may not exactly match with the provided links ;; so all of the extended signatures must be traversed to find the right ;; signatures for init-depends - (define extended-imports - (map cons import-links - (map (λ (l) (map Signature-name (flatten-sigs l))) import-sigs))) (define init-depend-links (for*/list ([sig-name (in-list (map Signature-name ini-deps))] - [(import-link import-family) (in-dict extended-imports)] + [(import-link import-family) + ;; step through the extended-imports + (in-parallel (in-list import-links) + (in-list (map (λ (l) (map Signature-name (flatten-sigs l))) import-sigs)))] #:when (member sig-name import-family free-identifier=?)) import-link)) ;; new init-depends are the init-depends of this unit that @@ -718,13 +718,13 @@ (define-values (ann/def-names ann/def-exprs) (process-ann/def-for-letrec annotation/definition-forms)) - (define signature-annotations - (for/list ([(k v) (in-dict local-sig-type-map)]) - (cons k (-> v)))) + (define-values (sig-ids sig-types) + (for/lists (_1 _2) ([(k v) (in-dict local-sig-type-map)]) + (values k (-> v)))) (define unit-type - (with-lexical-env/extend-types - (map car signature-annotations) - (map cdr signature-annotations) + (with-extended-lexical-env + [#:identifiers sig-ids + #:types sig-types] ;; Typechecking a unit body is structurally similar to that of ;; checking a let-body, so we resuse the machinary for checking ;; let expressions diff --git a/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt b/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt index b65b7808..773189db 100644 --- a/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt +++ b/typed-racket-lib/typed-racket/typecheck/tc-envops.rkt @@ -23,7 +23,7 @@ [props (let loop ([ps atoms] [negs '()] - [Γ (replace-props env props)]) + [Γ (env-replace-props env props)]) (match ps [(cons p ps) (match p @@ -34,7 +34,7 @@ [new-t (update t pt #t lo)]) (if (type-equal? new-t -Bottom) (values #f '()) - (loop ps negs (extend Γ x new-t))))] + (loop ps negs (env-set-type Γ x new-t))))] ;; process negative info _after_ positive info so we don't miss anything [(NotTypeProp: (Path: _ x) _) #:when (and (not (is-var-mutated? x)) @@ -49,7 +49,7 @@ [new-t (update t pt #f lo)]) (if (type-equal? new-t -Bottom) #f - (loop rst (extend Γ x new-t))))] + (loop rst (env-set-type Γ x new-t))))] [_ Γ]))]) (values Γ atoms))]))] [else (values #f '())])) @@ -57,6 +57,7 @@ ;; run code in an extended env and with replaced props. Requires the body to return a tc-results. ;; TODO make this only add the new prop instead of the entire environment once tc-id is fixed to ;; include the interesting props in its prop. +;; TODO figure out what the heck the above TODO means -amk ;; WARNING: this may bail out when code is unreachable (define-syntax (with-lexical-env/extend-props stx) (define-splicing-syntax-class unreachable? diff --git a/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt b/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt index 88c6df6f..a43446df 100644 --- a/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt +++ b/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt @@ -80,15 +80,15 @@ (if rest-id (list rest-id) null)) (make-arr* - arg-types - (abstract-results - (with-lexical-env/extend-types - (append rest-names arg-names) - (append rest-types arg-types) - (tc-body/check body expected)) - arg-names #:rest-id rest-id) - #:rest (and (Type? rest) rest) - #:drest (and (cons? rest) rest))) + arg-types + (abstract-results + (with-extended-lexical-env + [#:identifiers (append rest-names arg-names) + #:types (append rest-types arg-types)] + (tc-body/check body expected)) + arg-names #:rest-id rest-id) + #:rest (and (Type? rest) rest) + #:drest (and (cons? rest) rest))) ;; check-clause: Checks that a lambda clause has arguments and body matching the expected type ;; arg-list: The identifiers of the positional args in the lambda form @@ -99,21 +99,22 @@ ;; drest: The expected base type of the rest arg and its bound (poly dotted case) ;; ret-ty: The expected type of the body of the lambda. (define/cond-contract (check-clause arg-list rest-id body arg-tys rest-ty drest ret-ty) - ((listof identifier?) - (or/c #f identifier?) syntax? (listof Type?) (or/c #f Type?) - (or/c #f (cons/c Type? symbol?)) tc-results/c - . -> . - arr?) + ((listof identifier?) + (or/c #f identifier?) syntax? (listof Type?) (or/c #f Type?) + (or/c #f (cons/c Type? symbol?)) tc-results/c + . -> . + arr?) (let* ([arg-len (length arg-list)] [tys-len (length arg-tys)] - [arg-types (if (andmap type-annotation arg-list) - (get-types arg-list #:default Univ) - (cond - [(= arg-len tys-len) arg-tys] - [(< arg-len tys-len) (take arg-tys arg-len)] - [(> arg-len tys-len) (append arg-tys - (map (lambda _ (or rest-ty (Un))) - (drop arg-list tys-len)))]))]) + [arg-types + (if (andmap type-annotation arg-list) + (get-types arg-list #:default Univ) + (cond + [(= arg-len tys-len) arg-tys] + [(< arg-len tys-len) (take arg-tys arg-len)] + [(> arg-len tys-len) (append arg-tys + (map (lambda _ (or rest-ty (Un))) + (drop arg-list tys-len)))]))]) ;; Check that the number of formal arguments is valid for the expected type. ;; Thus it must be able to accept the number of arguments that the expected @@ -133,9 +134,9 @@ [else (define base-rest-type (cond - [(type-annotation rest-id) (get-type rest-id #:default Univ)] - [rest-ty rest-ty] - [else Univ])) + [(type-annotation rest-id) (get-type rest-id #:default Univ)] + [rest-ty rest-ty] + [else Univ])) (define extra-types (if (<= arg-len tys-len) (drop arg-tys arg-len) @@ -143,9 +144,9 @@ (apply Un base-rest-type extra-types)])) (tc-lambda-body arg-list arg-types - #:rest (and rest-type (list rest-id rest-type)) - #:expected ret-ty - body))) + #:rest (and rest-type (list rest-id rest-type)) + #:expected ret-ty + body))) ;; typecheck a single lambda, with argument list and body ;; drest-ty and drest-bound are both false or not false @@ -546,9 +547,9 @@ (define ft (t:->* args (tc-results->values return))) (define names (cons name formals)) (define objs (map (λ (_) -empty-obj) names)) - (with-lexical-env/extend-types - (cons name formals) - (cons ft args) + (with-extended-lexical-env + [#:identifiers (cons name formals) + #:types (cons ft args)] (values (replace-names names objs (ret ft)) (replace-names names objs (tc-body/check body return))))) diff --git a/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt b/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt index 5f7f5736..851f42be 100644 --- a/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt +++ b/typed-racket-lib/typed-racket/typecheck/tc-let-unit.rkt @@ -7,7 +7,8 @@ (private type-annotation parse-type syntax-properties) (env lexical-env type-alias-helper mvar-env global-env scoped-tvar-env - signature-env signature-helper) + signature-env signature-helper + type-env-structs) (rep prop-rep object-rep type-rep) syntax/free-vars (typecheck signatures tc-metafunctions tc-subst internal-forms tc-envops) @@ -24,82 +25,111 @@ (import tc-expr^) (export tc-let^) -;; get-names+objects (listof (listof identifier?)) (listof tc-results?) -> (listof (list/c identifier Object?)) -;; Given a list of bindings and the tc-results for the corresponding expressions, return a list of -;; tuples of the binding-name and corresponding objects from the results. -;; This is used to replace the names with the objects after the names go out of scope. -(define (get-names+objects namess results) - (append* - (for/list ([names namess] [results results]) - (match results - [(list (tc-result: _ _ os) ...) - (map list names os)])))) +;; consolidate-bound-ids-info +;; +;; This function can be viewed as a helper to +;; T-Let from the formalism (it's actually a helper +;; for 'check-let-body' in this file). +;; +;; It takes as arguments: +;; +;; namess : the local names bound by a let-values +;; (note: all let's are special cases of let-values) +;; +;; rhs-typess : the types (acutally tc-results) of the +;; expressions whose values are assigned +;; to the local identifiers found in 'namess' +;; +;; returns : 4 lists of index-associated values: +;; names +;; types +;; aliased-objs +;; props +;; - names is the idents bound for the body of this let +;; (i.e. (flatten namess)) +;; - types[i] is the type which should be added to Γ for names[i]. +;; - aliased-objs[i] is the object which names[i] is an alias for, +;; where Empty means it aliases no syntactic object. +;; - props[i] is the logical information that holds for the +;; body of the let which we learned while typechecking the +;; rhs expression for names[i]. +(define/cond-contract (consolidate-bound-ids-info namess rhs-typess) + (->i ([nss (listof (listof identifier?))] + [tss (listof (listof tc-result?))]) + #:pre (nss tss) (and (= (length nss) (length tss)) + (for/and ([ns (in-list nss)] + [ts (in-list tss)]) + (= (length ns) (length ts)))) + [result (values (listof identifier?) + (listof Type?) + (listof OptObject?) + (listof Prop?))]) + (for*/lists (idents types aliased-objects propositions) + ([(names results) (in-parallel (in-list namess) (in-list rhs-typess))] + [(name result) (in-parallel (in-list names) (in-list results))]) + (match-define (tc-result: type p+/p- obj) result) + (define mutated? (is-var-mutated? name)) + ;; n-obj is the object naming n (unless n is mutated, then + ;; its -empty-obj) + (define aliased-obj (if mutated? -empty-obj obj)) + (define-values (p+ p-) (match p+/p- + [(PropSet: p+ p-) (values p+ p-)] + ;; it's unclear if this 2nd clause is necessary any more. + [_ (values -tt -tt)])) + (define prop (cond ;; if n can't be #f, we can assume p+ + [(not (overlap? type -False)) p+] + [mutated? -tt] + [else ;; otherwise we know ((o ∉ #f) ∧ p+) ∨ ((o ∈ #f) ∧ p-) + (let ([obj (if (Object? obj) obj name)]) + (-or (-and (-not-type obj -False) p+) + (-and (-is-type obj -False) p-)))])) + (values name type aliased-obj prop))) -;; Checks that the body has the expected type when names are bound to the types spcified by results. -;; The exprs are also typechecked by using expr->type. -;; TODO: make this function sane. -;; The `check-thunk` argument serves the same purpose as in tc/letrec-values -(define/cond-contract (do-check expr->type namess expected-results exprs body expected - [check-thunk void]) - (((syntax? tc-results/c . -> . any/c) - (listof (listof identifier?)) (listof (listof tc-result?)) - (listof syntax?) syntax? (or/c #f tc-results/c)) - ((-> any/c)) +;; check-let-body +;; +;; Checks that the body has the expected type with the info +;; from the newly bound ids appropriately added to the type environment. +;; +;; bound-idss : all of the local names bound by a let +;; +;; bound-resultss : the types (tc-results actually) of all of the names +;; in 'bound-idss'. The info in 'bound-resultss' is what is used to +;; extend Γ while typechecking the environment. See the helper +;; function 'consolidate-bound-ids-info'. +(define/cond-contract (check-let-body bound-idss bound-resultss body expected + #:before-check-body [pre-body-thunk void]) + (((listof (listof identifier?)) + (listof (listof tc-result?)) + syntax? + (or/c #f tc-results/c)) + (#:before-check-body (-> any/c)) . ->* . tc-results/c) - (with-cond-contract t/p ([expected-types (listof (listof Type?))] - [objs (listof (listof OptObject?))] - [props (listof (listof Prop?))]) - (define-values (expected-types objs props) - (for/lists (e o p) - ([e-r (in-list expected-results)] - [names (in-list namess)]) - (match e-r - [(list (tc-result: e-ts (PropSet: ps+ ps-) os) ...) - (values e-ts - (map (λ (o n) (if (is-var-mutated? n) -empty-obj o)) os names) - (apply append - (for/list ([n (in-list names)] - [t (in-list e-ts)] - [p+ (in-list ps+)] - [p- (in-list ps-)] - [o (in-list os)]) - (cond - [(not (overlap? t (-val #f))) (list p+)] - [(is-var-mutated? n) (list)] - [else - (define obj (if (Object? o) o n)) - (list (-or (-and (-not-type obj (-val #f)) p+) - (-and (-is-type obj (-val #f)) p-)))]))))] - ;; amk: does this case ever occur? - [(list (tc-result: e-ts #f _) ...) - (values e-ts (make-list (length e-ts) -empty-obj) null)])))) + (define-values (idents types aliased-objs props) + (consolidate-bound-ids-info bound-idss bound-resultss)) + (define ids-to-erase + (for/list ([id (in-list idents)] + [obj (in-list aliased-objs)] + #:when (Empty? obj)) + id)) ;; extend the lexical environment for checking the body ;; with types and potential aliases - (let ([names (append* namess)] - [objs (append* objs)]) - (with-lexical-env/extend-types+aliases - names - (append* expected-types) - objs - (replace-names - names - objs - (with-lexical-env/extend-props - (apply append props) - ;; if a let rhs does not return, the body isn't checked - #:unreachable (for ([form (in-list (syntax->list body))]) - (register-ignored! form)) - ;; type-check the rhs exprs - (for ([expr (in-list exprs)] [results (in-list expected-results)]) - (match results - [(list (tc-result: ts fs os) ...) - (expr->type expr (ret ts fs os))])) - ;; Perform additional context-dependent checking that needs to be done - ;; in the context of the letrec body - (check-thunk) - ;; typecheck the body - (tc-body/check body (and expected (erase-props expected)))))))) + (with-extended-lexical-env + [#:identifiers idents + #:types types + #:aliased-objects aliased-objs] + (erase-names + ids-to-erase + (with-lexical-env/extend-props + props + ;; if a let rhs does not return, the body isn't checked + #:unreachable (for ([form (in-list (syntax->list body))]) + (register-ignored! form)) + ;; Perform additional context-dependent checking that needs to be done + ;; before checking the body + (pre-body-thunk) + ;; typecheck the body + (tc-body/check body (and expected (erase-props expected))))))) (define (tc-expr/maybe-expected/t e names) (syntax-parse names @@ -153,41 +183,43 @@ ;; For example, it is used to typecheck units and ensure that exported ;; variables are exported at the correct types (define (tc/letrec-values namess exprs body [expected #f] [check-thunk void]) - (let* ([names (stx-map syntax->list namess)] - [orig-flat-names (apply append names)] + (let* ([namess (stx-map syntax->list namess)] + [orig-flat-names (apply append namess)] [exprs (syntax->list exprs)]) - (register-aliases-and-declarations names exprs) + (register-aliases-and-declarations namess exprs) ;; First look at the clauses that do not bind the letrec names (define all-clauses - (for/list ([name-lst names] [expr exprs]) + (for/list ([name-lst (in-list namess)] + [expr (in-list exprs)]) (lr-clause name-lst expr))) (define-values (ordered-clauses remaining) (get-non-recursive-clauses all-clauses orig-flat-names)) (define-values (remaining-names remaining-exprs) - (for/lists (_1 _2) ([remaining-clause remaining]) + (for/lists (_1 _2) ([remaining-clause (in-list remaining)]) (match-define (lr-clause name expr) remaining-clause) (values name expr))) ;; Check those and then check the rest in the extended environment (check-non-recursive-clauses ordered-clauses - (lambda () - (cond - ;; after everything, check the body expressions - [(null? remaining-names) - (check-thunk) - (tc-body/check body (and expected (erase-props expected)))] - [else - (define flat-names (apply append remaining-names)) - (do-check tc-expr/check - remaining-names - ;; types the user gave. - (map (λ (l) (map tc-result (map get-type l))) remaining-names) - remaining-exprs body expected - check-thunk)]))))) + (λ () + ;; types the user gave. + (define given-rhs-types (map (λ (l) (map tc-result (map get-type l))) remaining-names)) + (check-let-body + remaining-names + given-rhs-types + body + expected + #:before-check-body + (λ () (begin (for ([expr (in-list remaining-exprs)] + [results (in-list given-rhs-types)]) + (match results + [(list (tc-result: ts fs os) ...) + (tc-expr/check expr (ret ts fs os))])) + (check-thunk)))))))) ;; An lr-clause is a ;; (lr-clause (Listof Identifier) Syntax) @@ -264,12 +296,12 @@ (get-type/infer names expr (lambda (e) (tc-expr/maybe-expected/t e names)) tc-expr/check)) - (with-lexical-env/extend-types - names - ts - (replace-names names - os - (loop (cdr clauses))))]))) + (with-extended-lexical-env + [#:identifiers names + #:types ts] + (replace-names names + os + (loop (cdr clauses))))]))) ;; this is so match can provide us with a syntax property to ;; say that this binding is only called in tail position @@ -286,16 +318,14 @@ (define (tc/let-values namess exprs body [expected #f]) (let* (;; a list of each name clause - [names (stx-map syntax->list namess)] + [namess (stx-map syntax->list namess)] ;; all the trailing expressions - the ones actually bound to the names [exprs (syntax->list exprs)]) - (register-aliases-and-declarations names exprs) + (register-aliases-and-declarations namess exprs) - (let* (;; the types of the exprs - #;[inferred-types (map (tc-expr-t/maybe-expected expected) exprs)] - ;; the annotated types of the name (possibly using the inferred types) - [results (for/list ([name (in-list names)] [e (in-list exprs)]) - (get-type/infer name e (tc-expr-t/maybe-expected expected) + ;; the annotated types of the name (possibly using the inferred types) + (let ([resultss (for/list ([names (in-list namess)] [e (in-list exprs)]) + (get-type/infer names e (tc-expr-t/maybe-expected expected) tc-expr/check))]) - (do-check void names results exprs body expected)))) + (check-let-body namess resultss body expected)))) diff --git a/typed-racket-lib/typed-racket/typecheck/tc-send.rkt b/typed-racket-lib/typed-racket/typecheck/tc-send.rkt index b8b3ab4b..c28544db 100644 --- a/typed-racket-lib/typed-racket/typecheck/tc-send.rkt +++ b/typed-racket-lib/typed-racket/typecheck/tc-send.rkt @@ -62,14 +62,18 @@ #:literal-sets (kernel-literals) #:literals (list) [(#%plain-app meth obj arg ...) - (with-lexical-env/extend-types vars types + (with-extended-lexical-env + [#:identifiers vars + #:types types] (tc-expr/check (syntax/loc app-stx (#%plain-app meth arg ...)) expected))] [(let-values ([(arg-var) arg] ...) (~and outer-loc (#%plain-app (~and inner-loc (#%plain-app cpce s-kp meth kpe kws num)) kws2 kw-args obj pos-arg ...))) - (with-lexical-env/extend-types vars types + (with-extended-lexical-env + [#:identifiers vars + #:types types] (tc-expr/check (with-syntax* ([inner-app (syntax/loc app-stx (#%plain-app cpce s-kp meth kpe kws num))] [outer-app (syntax/loc app-stx diff --git a/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt b/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt index 640bc28e..fdf749a8 100644 --- a/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt +++ b/typed-racket-lib/typed-racket/typecheck/tc-subst.rkt @@ -22,7 +22,10 @@ [replace-names (-> (listof identifier?) (listof OptObject?) tc-results/c - tc-results/c)]) + tc-results/c)] + [erase-names (-> (listof identifier?) + tc-results/c + tc-results/c)]) ;; Substitutes the given objects into the values and turns it into a @@ -68,6 +71,12 @@ (list nm o Univ))) (subst-tc-results res targets)) +(define (erase-names names res) + (define targets + (for/list ([nm (in-list names)]) + (list nm -empty-obj Univ))) + (subst-tc-results res targets)) + (define (subst-tc-results res targets) (define (sr t ps o) (subst-tc-result t ps o targets)) diff --git a/typed-racket-test/unit-tests/typecheck-tests.rkt b/typed-racket-test/unit-tests/typecheck-tests.rkt index 69385f5e..bf2f6e0a 100644 --- a/typed-racket-test/unit-tests/typecheck-tests.rkt +++ b/typed-racket-test/unit-tests/typecheck-tests.rkt @@ -115,9 +115,9 @@ ;; the golden function to the expanded syntax of the expression. (define (test/proc expr golden-fun (expected #f) (new-mapping '())) (define expanded-expr (tr-expand expr)) - (define result (with-lexical-env/extend-types - (map car new-mapping) - (map cadr new-mapping) + (define result (with-extended-lexical-env + [#:identifiers (map car new-mapping) + #:types (map cadr new-mapping)] (tc expanded-expr expected))) (define golden (golden-fun expanded-expr)) (check-tc-results result golden #:name "tc-expr")) @@ -141,9 +141,9 @@ "tc-expr raised the wrong error message")))))]) (define result (parameterize ([delay-errors? #t]) - (with-lexical-env/extend-types - (map car new-mapping) - (map cadr new-mapping) + (with-extended-lexical-env + [#:identifiers (map car new-mapping) + #:types (map cadr new-mapping)] (tc (tr-expand code) expected)))) (check-tc-results result golden #:name "tc-expr") (report-first-error)