diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt index f0f93d8b65..04bb1bfd42 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt @@ -3,8 +3,9 @@ (require "../utils/utils.rkt" racket/dict racket/list syntax/parse racket/syntax syntax/stx racket/match syntax/id-table racket/set + unstable/sequence (contract-req) - (rep type-rep object-rep) + (rep type-rep object-rep rep-utils) (rename-in (types abbrev utils union) [-> t:->] [->* t:->*] @@ -13,26 +14,14 @@ (types type-table) (typecheck signatures tc-metafunctions tc-subst) (env lexical-env tvar-env index-env scoped-tvar-env) - (utils tc-utils)) + (utils tc-utils) + (for-syntax + syntax/parse + racket/base)) (import tc-expr^) (export tc-lambda^) -(define-struct/cond-contract lam-result ([args (listof (list/c identifier? Type/c))] - [rest (or/c #f (list/c identifier? Type/c))] - [drest (or/c #f (list/c identifier? (cons/c Type/c symbol?)))] - [body tc-results/c]) - #:transparent) - -(define (lam-result->type lr) - (match lr - [(struct lam-result ((list (list arg-ids arg-tys) ...) rest drest body)) - (make-arr* - arg-tys - (abstract-results body arg-ids - #:rest-id (or (and rest (first rest))) (and drest (first drest))) - #:rest (and rest (second rest)) - #:drest (and drest (second drest)))])) (define-syntax-class cl-rhs #:literal-sets (kernel-literals) @@ -64,13 +53,57 @@ (if (= arg-len 1) "" "s") (if rest " and a rest arg" ""))) -;; listof[id] option[id] block listof[type] option[type] option[(cons type var)] tc-result -> lam-result -(define/cond-contract (check-clause arg-list rest body arg-tys rest-ty drest ret-ty) +;; tc-lambda-body: Typechecks the body with the given args and names and returns the resulting arr?. +;; arg-names: The identifiers of the positional args +;; arg-types: The types of the positional args +;; raw-rest: Either #f for no rest argument or (list rest-id rest-type) where rest-id is the +;; identifier of the rest arg, and rest-type is the type. +;; expected: The expected type of the body forms. +;; body: The body of the lambda to typecheck. +(define/cond-contract + (tc-lambda-body arg-names arg-types #:rest [raw-rest #f] #:expected [expected #f] body) + (->* ((listof identifier?) (listof Type/c) syntax?) + (#:rest (or/c #f (list/c identifier? (or/c Type/c (cons/c Type/c symbol?)))) + #:expected (or/c #f tc-results/c)) + arr?) + (define-values (rest-id rest) + (if raw-rest + (values (first raw-rest) (second raw-rest)) + (values #f #f))) + + (define rest-types + (cond + [(not rest) (list)] + [(cons? rest) (list (make-ListDots (car rest) (cdr rest)))] + [else (list (-lst rest))])) + (define rest-names + (if rest-id (list rest-id) null)) + + (make-arr* + arg-types + (abstract-results + (with-lexical-env/extend + (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))) + +;; 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 +;; rest-id: The identifier of the rest arg, or #f for no rest arg +;; body: The body of the lambda to typecheck. +;; arg-tys: The expected positional argument types. +;; rest-ty: The expected base type of the rest arg (not poly dotted case) +;; 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/c) (or/c #f Type/c) (or/c #f (cons/c Type/c symbol?)) tc-results/c . -> . - lam-result?) + arr?) (let* ([arg-len (length arg-list)] [tys-len (length arg-tys)] [arg-types (if (andmap type-annotation arg-list) @@ -81,63 +114,48 @@ [(> arg-len tys-len) (append arg-tys (map (lambda _ (or rest-ty (Un))) (drop arg-list tys-len)))]))]) - (define (check-body [rest-ty rest-ty]) - (with-lexical-env/extend - arg-list arg-types - (make-lam-result (for/list ([al (in-list arg-list)] - [at (in-list arg-types)]) - (list al at)) - (and rest-ty (list (or rest (generate-temporary)) rest-ty)) - (and drest (list (or rest (generate-temporary)) drest)) - (tc-body/check body ret-ty)))) + ;; 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 ;; type has. So we check for two cases: if the function doesn't accept ;; enough arguments, or if it requires too many arguments. ;; This allows a form like (lambda args body) to have the type (-> Symbol ;; Number) with out a rest arg. - (when (or (and (< arg-len tys-len) (not rest)) + (when (or (and (< arg-len tys-len) (not rest-id)) (and (> arg-len tys-len) (not (or rest-ty drest)))) - (tc-error/delayed (expected-str tys-len rest-ty drest arg-len rest))) - (cond - [(not rest) - (check-body)] - [drest - (with-lexical-env/extend - (list rest) (list (make-ListDots (car drest) (cdr drest))) - (check-body))] - [(dotted? rest) - => - (lambda (b) - (let ([dty (extend-tvars (list b) (get-type rest #:default Univ))]) - (with-lexical-env/extend - (list rest) (list (make-ListDots dty b)) - (check-body))))] - [else - (define base-rest-type - (cond - [(type-annotation rest) (get-type rest #:default Univ)] - [rest-ty rest-ty] - [else Univ])) - (define extra-types - (if (<= arg-len tys-len) - (drop arg-tys arg-len) - null)) - (define rest-type (apply Un base-rest-type extra-types)) + (tc-error/delayed (expected-str tys-len rest-ty drest arg-len rest-id))) + (define rest-type + (cond + [(not rest-id) #f] + [drest drest] + [(dotted? rest-id) + => (λ (b) (cons (extend-tvars (list b) (get-type rest-id #:default Univ)) b))] + [else + (define base-rest-type + (cond + [(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) + null)) + (apply Un base-rest-type extra-types)])) - (with-lexical-env/extend - (list rest) (list (-lst rest-type)) - (check-body rest-type))]))) + (tc-lambda-body arg-list arg-types + #: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 ;; tc/lambda-clause/check: formals syntax listof[Type/c] tc-result -;; option[Type/c] option[(cons Type/c symbol)] -> lam-result +;; option[Type/c] option[(cons Type/c symbol)] -> arr? (define (tc/lambda-clause/check formals body arg-tys ret-ty rest-ty drest) (check-clause (formals-positional formals) (formals-rest formals) body arg-tys rest-ty drest ret-ty)) ;; typecheck a single opt-lambda clause with argument list and body -;; tc/opt-lambda-clause: listof[identifier] syntax -> listof[lam-result] +;; tc/opt-lambda-clause: listof[identifier] syntax -> listof[arr?] (define (tc/opt-lambda-clause arg-list body aux-table flag-table) ;; arg-types: Listof[Type/c] (define arg-types @@ -166,17 +184,11 @@ [(free-identifier=? i v) (-val #f)] [else t]))))))) (for/list ([arg-types (in-list new-arg-types)]) - (with-lexical-env/extend - arg-list arg-types - (lam-result - (map list arg-list arg-types) - #f - #f - (tc-body/check body #f))))) + (tc-lambda-body arg-list arg-types body))) -;; formals syntax -> listof[lam-result] +;; formals syntax -> listof[arr?] (define (tc/lambda-clause formals body) (define-values (aux-table flag-table) (syntax-parse body @@ -190,8 +202,7 @@ (tc/opt-lambda-clause arg-list body aux-table flag-table)] [else (define arg-types (get-types arg-list #:default Univ)) - (define combined-args (map list arg-list arg-types)) - (list + (define rest-type (cond ;; Lambda with poly dotted rest argument [(and rest-id (dotted? rest-id)) @@ -201,36 +212,18 @@ (if (bound-tvar? bound) (tc-error "Bound on ... type (~a) is not an appropriate type variable" bound) (tc-error/stx rest-id "Bound on ... type (~a) was not in scope" bound))) - (let ([rest-type (extend-tvars (list bound) - (get-type rest-id #:default Univ))]) - (with-lexical-env/extend - (cons rest-id arg-list) - (cons (make-ListDots rest-type bound) arg-types) - (lam-result - combined-args - #f - (list rest-id (cons rest-type bound)) - (tc-body/check body #f)))))] + (cons (extend-tvars (list bound) (get-type rest-id #:default Univ)) bound))] ;; Lambda with regular rest argument [rest-id - (let ([rest-type (get-type rest-id #:default Univ)]) - (with-lexical-env/extend - (cons rest-id arg-list) - (cons (make-Listof rest-type) arg-types) - (lam-result - combined-args - (list rest-id rest-type) - #f - (tc-body/check body #f))))] + (get-type rest-id #:default Univ)] ;; Lambda with no rest argument - [else - (with-lexical-env/extend - arg-list arg-types - (lam-result - combined-args - #f - #f - (tc-body/check body #f)))]))])) + [else #f])) + + (list + (tc-lambda-body arg-list arg-types + #:rest (and rest-type (list rest-id rest-type)) + body))])) + ;; positional: natural? - the number of positional arguments ;; rest: boolean? - if there is a positional argument @@ -290,7 +283,7 @@ (and (member new-positional positionals) (not new-rest)))) -;; tc/mono-lambda : (listof (list formals syntax?)) (or/c #f tc-results) -> (listof lam-result) +;; tc/mono-lambda : (listof (list formals syntax?)) (or/c #f tc-results) -> (listof arr?) ;; typecheck a sequence of case-lambda clauses (define (tc/mono-lambda formals+bodies expected) (define expected-type @@ -349,7 +342,7 @@ [(Function: (list)) #f] [_ #t])) ;; TODO improve error message. - (tc-error/expr #:return (list (lam-result null (list (generate-temporary) Univ) #f (ret (Un)))) + (tc-error/expr #:return (list (make-arr* null (Un) #:rest Univ)) "Expected a function of type ~a, but got a function with the wrong arity" expected-type) (apply append @@ -363,12 +356,11 @@ f* b* args (values->tc-results ret (formals->objects f*)) rest drest))]))))) (define (tc/mono-lambda/type formals bodies expected) - (make-Function (map lam-result->type - (tc/mono-lambda - (map list - (stx-map make-formals formals) - (syntax->list bodies)) - expected)))) + (make-Function + (tc/mono-lambda + (for/list ([f (in-syntax formals)] [b (in-syntax bodies)]) + (list (make-formals f) b)) + expected))) (define (plambda-prop stx) (define d (plambda-property stx))