From 56216d320e44366ef9ee6edce8964d026751ebaa Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Sun, 22 Mar 2009 12:41:26 +0000 Subject: [PATCH] =?UTF-8?q?Use=20'no-free-identifier=3D=3F=20property=20wi?= =?UTF-8?q?th=20rename=20transformers.=20Allow=20use=20of=20...=20without?= =?UTF-8?q?=20bound=20when=20only=20one=20...=20var=20in=20scope.?= svn: r14214 original commit: 6d8014783b16c2d31624f8bd5f6d25d9fb10b5e2 --- .../tests/typed-scheme/succeed/no-bound-fl.ss | 11 ++++++ .../unit-tests/parse-type-tests.ss | 6 +++ .../typed-scheme/env/type-environments.ss | 14 +++++++ collects/typed-scheme/private/parse-type.ss | 37 +++++++++++++++++++ .../typecheck/provide-handling.ss | 12 ++++-- 5 files changed, 76 insertions(+), 4 deletions(-) create mode 100644 collects/tests/typed-scheme/succeed/no-bound-fl.ss diff --git a/collects/tests/typed-scheme/succeed/no-bound-fl.ss b/collects/tests/typed-scheme/succeed/no-bound-fl.ss new file mode 100644 index 00000000..1f9bd526 --- /dev/null +++ b/collects/tests/typed-scheme/succeed/no-bound-fl.ss @@ -0,0 +1,11 @@ +#lang typed-scheme + +(: fold-left (All (a b ...) ((a b ... -> a) a (Listof b) ... -> a))) +(define (fold-left f a . bss) + (if (ormap null? bss) + a + (apply fold-left + f + (apply f a (map car bss)) + (map cdr bss)))) + diff --git a/collects/tests/typed-scheme/unit-tests/parse-type-tests.ss b/collects/tests/typed-scheme/unit-tests/parse-type-tests.ss index cfe775ea..c14f64d8 100644 --- a/collects/tests/typed-scheme/unit-tests/parse-type-tests.ss +++ b/collects/tests/typed-scheme/unit-tests/parse-type-tests.ss @@ -80,6 +80,10 @@ [(All (a ...) (a ... a -> Integer)) (-polydots (a) ( (list) (a a) . ->... . -Integer))] [(∀ (a) (Listof a)) (-poly (a) (make-Listof a))] [(∀ (a ...) (a ... a -> Integer)) (-polydots (a) ( (list) (a a) . ->... . -Integer))] + [(All (a ...) (a ... -> Number)) + (-polydots (a) ((list) [a a] . ->... . N))] + [(All (a ...) (values a ...)) + (-polydots (a) (make-ValuesDots (list) a 'a))] [(case-lambda (Number -> Boolean) (Number Number -> Number)) (cl-> [(N) B] [(N N) N])] [1 (-val 1)] @@ -91,6 +95,8 @@ [a (-v a) (extend-env (list 'a) (list (-v a)) initial-tvar-env)] + [(All (a ...) (a ... -> Number)) + (-polydots (a) ((list) [a a] . ->... . N))] )) diff --git a/collects/typed-scheme/env/type-environments.ss b/collects/typed-scheme/env/type-environments.ss index 0f159ec0..42eb02c9 100644 --- a/collects/typed-scheme/env/type-environments.ss +++ b/collects/typed-scheme/env/type-environments.ss @@ -8,6 +8,9 @@ extend/values dotted-env initial-tvar-env + env-filter + env-vals + env-keys+vals with-dotted-env/extend) (require (prefix-in r: "../utils/utils.ss")) @@ -17,6 +20,17 @@ ;; eq? has the type of equal?, and l is an alist (with conses!) (define-struct env (eq? l)) +(define (env-vals e) + (map cdr (env-l e))) + +(define (env-keys+vals e) + (env-l e)) + +(define (env-filter f e) + (match e + [(struct env (eq? l)) + (make-env eq? (filter f l))])) + ;; the initial type variable environment - empty ;; this is used in the parsing of types (define initial-tvar-env (make-env eq? '())) diff --git a/collects/typed-scheme/private/parse-type.ss b/collects/typed-scheme/private/parse-type.ss index 135384af..8cc2d1ce 100644 --- a/collects/typed-scheme/private/parse-type.ss +++ b/collects/typed-scheme/private/parse-type.ss @@ -350,6 +350,26 @@ (current-tvars))]) (parse-type #'rest)) (syntax-e #'bound)))))))] + [(dom ... rest ::: -> rng) + (and (eq? (syntax-e #'->) '->) + (eq? (syntax-e #':::) '...)) + (begin + (add-type-name-reference #'->) + (let ([bounds (filter (compose Dotted? cdr) (env-keys+vals (current-tvars)))]) + (when (null? bounds) + (tc-error/stx stx "No type variable bound with ... in scope for ... type")) + (unless (null? (cdr bounds)) + (tc-error/stx stx "Cannot infer bound for ... type")) + (match-let ([(cons var (struct Dotted (t))) (car bounds)]) + (make-Function + (list + (make-arr-dots (map parse-type (syntax->list #'(dom ...))) + (parse-type #'rng) + (parameterize ([current-tvars (extend-env (list var) + (list (make-DottedBoth t)) + (current-tvars))]) + (parse-type #'rest)) + var))))))] ;; has to be below the previous one [(dom ... -> rng) (eq? (syntax-e #'->) '->) @@ -369,6 +389,23 @@ (current-tvars))]) (parse-type #'dty)) (syntax-e #'bound))))] + [(values tys ... dty dd) + (and (eq? (syntax-e #'values) 'values) + (eq? (syntax-e #'dd) '...)) + (begin + (add-type-name-reference #'values) + (let ([bounds (filter (compose Dotted? cdr) (env-keys+vals (current-tvars)))]) + (when (null? bounds) + (tc-error/stx stx "No type variable bound with ... in scope for ... type")) + (unless (null? (cdr bounds)) + (tc-error/stx stx "Cannot infer bound for ... type")) + (match-let ([(cons var (struct Dotted (t))) (car bounds)]) + (make-ValuesDots (map parse-type (syntax->list #'(tys ...))) + (parameterize ([current-tvars (extend-env (list var) + (list (make-DottedBoth t)) + (current-tvars))]) + (parse-type #'dty)) + var))))] [(values tys ...) (eq? (syntax-e #'values) 'values) (-values (map parse-type (syntax->list #'(tys ...))))] diff --git a/collects/typed-scheme/typecheck/provide-handling.ss b/collects/typed-scheme/typecheck/provide-handling.ss index 791d6384..66b3576a 100644 --- a/collects/typed-scheme/typecheck/provide-handling.ss +++ b/collects/typed-scheme/typecheck/provide-handling.ss @@ -54,15 +54,18 @@ (define/contract cnt-id #,cnt id) (define-syntax export-id (if (unbox typed-context?) - (make-rename-transformer #'id) - (make-rename-transformer #'cnt-id))) + (make-rename-transformer (syntax-property #'id + 'not-free-identifier=? #t)) + (make-rename-transformer (syntax-property #'cnt-id + 'not-free-identifier=? #t)))) (#%provide (rename export-id out-id)))))] [else (with-syntax ([(export-id) (generate-temporaries #'(id))]) #`(begin (define-syntax export-id (if (unbox typed-context?) - (make-rename-transformer #'id) + (make-rename-transformer (syntax-property #'id + 'not-free-identifier=? #t)) (lambda (stx) (tc-error/stx stx "The type of ~a cannot be converted to a contract" (syntax-e #'id))))) (provide (rename-out [export-id out-id]))))])))] [(mem? internal-id stx-defs) @@ -76,7 +79,8 @@ (if (unbox typed-context?) (begin (add-alias #'export-id #'id) - (make-rename-transformer #'id)) + (make-rename-transformer (syntax-property #'id + 'not-free-identifier=? #t))) (lambda (stx) (tc-error/stx stx "Macro ~a from typed module used in untyped code" (syntax-e #'out-id))))) (provide (rename-out [export-id out-id]))))))]