suzanne.soy/racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Make tc-lambda-unit have one centralized definition of how to extend the environment.

Browse Source
This commit is contained in:
Eric Dobson 2014-06-22 17:16:17 -07:00
parent 3c179e0217
commit b6e96f0bf0
1 changed files with 98 additions and 106 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

204
pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-lambda-unit.rkt
View File

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