From 7f0a330c0c354760c42935692525dba5e98f1588 Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Wed, 18 Jun 2008 17:21:53 -0400 Subject: [PATCH] Adding drest capability to lambda formal checking. --- .../typed-scheme/private/tc-lambda-unit.ss | 133 ++++++++++-------- .../typed-scheme/private/type-environments.ss | 7 +- 2 files changed, 79 insertions(+), 61 deletions(-) diff --git a/collects/typed-scheme/private/tc-lambda-unit.ss b/collects/typed-scheme/private/tc-lambda-unit.ss index ea8d5395a8..742b49099d 100644 --- a/collects/typed-scheme/private/tc-lambda-unit.ss +++ b/collects/typed-scheme/private/tc-lambda-unit.ss @@ -32,65 +32,81 @@ [(Remove-Effect: t v) (if (free-identifier=? v id) (make-Latent-Remove-Effect t) (fail))])) (cons (map rv thns) (map rv elss)))) +(define (expected-str tys-len rest-ty drest arg-len rest) + (format "Expected function with ~a argument~a~a, but got function with ~a argument~a~a" + tys-len + (if (= tys-len 1) "" "s") + (if (or rest-ty + drest) + " and a rest arg" + "") + arg-len + (if (= arg-len 1) "" "s") + (if rest " and a rest arg" ""))) + +;; listof[id] option[id] block listof[type] option[type] option[(cons type var)] type +(define (check-clause arg-list rest body arg-tys rest-ty drest ret-ty) + (let* ([arg-len (length arg-list)] + [tys-len (length arg-tys)] + [arg-types (if (andmap type-annotation arg-list) + (map get-type arg-list) + (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)))]))]) + (define (check-body) + (with-lexical-env/extend + arg-list arg-types + (match (tc-exprs/check (syntax->list body) ret-ty) + [(tc-result: t thn els) + (cond + ;; this is T-AbsPred + ;; if this function takes only one argument, and all the effects are about that one argument + [(and (not rest-ty) (not drest) (= 1 (length arg-list)) (remove-var (car arg-list) thn els)) + => (lambda (thn/els) (make-arr arg-types t rest-ty drest (car thn/els) (cdr thn/els)))] + ;; otherwise, the simple case + [else (make-arr arg-types t rest-ty drest null null)])] + [t (int-err "bad match - not a tc-result: ~a ~a ~a" t ret-ty (syntax->datum body))]))) + (for-each (lambda (a) (printf/log "Lambda Var: ~a~n" (syntax-e a))) arg-list) + (when (or (not (= arg-len tys-len)) + (and rest (and (not rest-ty) + (not drest)))) + (tc-error/delayed (expected-str tys-len rest-ty drest arg-len rest))) + (cond + [(not rest) + (check-body)] + [drest + (with-dotted-env/extend + rest (car drest) (cdr drest) + (check-body))] + [(dotted? rest) + => + (lambda (b) + (let ([dty (get-type rest)]) + (with-dotted-env/extend + rest dty b + (check-body))))] + [else + (let ([rest-type (cond + [rest-ty rest-ty] + [(type-annotation rest) (get-type rest)] + [(< arg-len tys-len) (list-ref arg-tys arg-len)] + [else (Un)])]) + (with-lexical-env/extend + (list rest) (list (-lst rest-type)) + (check-body)))]))) ;; typecheck a single lambda, with argument list and body -;; fixme: abstract the two cases! -;; syntax-list[id] block listof[type] type option[type] -> arr -(define (tc/lambda-clause/check args body arg-tys ret-ty rest-ty) - (define (expected-str tys-len rest-ty arg-len rest) - (format "Expected function with ~a argument~a~a, but got function with ~a argument~a~a" - tys-len - (if (= tys-len 1) "" "s") - (if rest-ty " and a rest arg" "") - arg-len - (if (= arg-len 1) "" "s") - (if rest " and a rest arg" ""))) - ;; listof[id] option[id] block listof[type] option[type] type - (define (check-clause arg-list rest body arg-tys rest-ty ret-ty) - (let* ([arg-len (length arg-list)] - [tys-len (length arg-tys)] - [arg-types (if (andmap type-annotation arg-list) - (map get-type arg-list) - (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 _ (if rest-ty rest-ty (Un))) - (drop arg-list tys-len)))]))]) - (define (check-body) - (with-lexical-env/extend - arg-list arg-types - (match (tc-exprs/check (syntax->list body) ret-ty) - [(tc-result: t thn els) - (cond - ;; this is T-AbsPred - ;; if this function takes only one argument, and all the effects are about that one argument - [(and (= 1 (length arg-list)) (remove-var (car arg-list) thn els)) - => (lambda (thn/els) (make-arr arg-types t rest-ty (car thn/els) (cdr thn/els)))] - ;; otherwise, the simple case - [else (make-arr arg-types t rest-ty)])] - [t (int-err "bad match - not a tc-result: ~a ~a ~a" t ret-ty (syntax->datum body))]))) - (for-each (lambda (a) (printf/log "Lambda Var: ~a~n" (syntax-e a))) arg-list) - (when (or (not (= arg-len tys-len)) - (and rest (not rest-ty))) - (tc-error/delayed (expected-str tys-len rest-ty arg-len rest))) - (cond - [(not rest) - (check-body)] - [else - (let ([rest-type (cond - [rest-ty rest-ty] - [(type-annotation rest) (get-type rest)] - [(< arg-len tys-len) (list-ref arg-tys arg-len)] - [else (Un)])]) - (with-lexical-env/extend - (list rest) (list (-lst rest-type)) - (check-body)))]))) +;; drest-ty and drest-bound are both false or not false +;; syntax-list[id] block listof[type] type option[type] option[(cons type var)] -> arr +(define (tc/lambda-clause/check args body arg-tys ret-ty rest-ty drest) (syntax-case args () [(args* ...) - (check-clause (syntax->list #'(args* ...)) #f body arg-tys rest-ty ret-ty)] + (check-clause (syntax->list #'(args* ...)) #f body arg-tys rest-ty drest ret-ty)] [(args* ... . rest) - (check-clause (syntax->list #'(args* ...)) #'rest body arg-tys rest-ty ret-ty)])) + (check-clause (syntax->list #'(args* ...)) #'rest body arg-tys rest-ty drest ret-ty)])) ;; syntax-list[id] block -> arr (define (tc/lambda-clause args body) @@ -164,12 +180,9 @@ (let loop ([expected expected]) (match expected [(Mu: _ _) (loop (unfold expected))] - [(Function: (list (arr: args ret rest #f _ _))) - (tc/lambda-clause/check (car (syntax->list formals)) (car (syntax->list bodies)) args ret rest) - expected] - [(Function: (list (arr: argss rets rests #f _ _) ...)) - (for ([args argss] [ret rets] [rest rests]) - (tc/lambda-clause/check (car (syntax->list formals)) (car (syntax->list bodies)) args ret rest)) + [(Function: (list (arr: argss rets rests drests _ _) ...)) + (for ([args argss] [ret rets] [rest rests] [drest drests]) + (tc/lambda-clause/check (car (syntax->list formals)) (car (syntax->list bodies)) args ret rest drest)) expected] [t (let ([t (tc/mono-lambda formals bodies #f)]) (check-below t expected))])) diff --git a/collects/typed-scheme/private/type-environments.ss b/collects/typed-scheme/private/type-environments.ss index f399bed4fa..536fdfc9c9 100644 --- a/collects/typed-scheme/private/type-environments.ss +++ b/collects/typed-scheme/private/type-environments.ss @@ -7,7 +7,8 @@ extend-env extend/values dotted-env - initial-tvar-env) + initial-tvar-env + with-dotted-env/extend) (require scheme/match "tc-utils.ss") @@ -61,3 +62,7 @@ [else (extend-env (list ks) (list vs) env)])) env kss vss)) +;; run code in an extended dotted env +(define-syntax with-dotted-env/extend + (syntax-rules () + [(_ i t v . b) (parameterize ([dotted-env (extend/values (list i) (list (cons t v)) (dotted-env))]) . b)]))