From dfdfae95d7d16ef3fa97503cfa0156101dc275b3 Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Tue, 17 Jun 2008 18:10:17 -0400 Subject: [PATCH] Checkpoint. --- collects/typed-scheme/private/lexical-env.ss | 4 +- collects/typed-scheme/private/parse-type.ss | 19 ++--- .../typed-scheme/private/promote-demote.ss | 4 +- collects/typed-scheme/private/tc-app-unit.ss | 78 +++++++++++++------ collects/typed-scheme/private/tc-utils.ss | 5 +- .../private/type-effect-convenience.ss | 3 - collects/typed-scheme/private/type-env.ss | 2 +- .../typed-scheme/private/type-name-env.ss | 3 +- collects/typed-scheme/private/type-utils.ss | 13 +++- 9 files changed, 82 insertions(+), 49 deletions(-) diff --git a/collects/typed-scheme/private/lexical-env.ss b/collects/typed-scheme/private/lexical-env.ss index 131c018ce4..79b9a47a16 100644 --- a/collects/typed-scheme/private/lexical-env.ss +++ b/collects/typed-scheme/private/lexical-env.ss @@ -1,6 +1,6 @@ #lang scheme/base -(require "type-environments.ss" "tc-utils.ss" "type-env.ss" "mutated-vars.ss") +(require "type-environments.ss" "tc-utils.ss" "type-env.ss" "mutated-vars.ss" "type-utils.ss") (provide (all-defined-out)) @@ -24,7 +24,7 @@ (lambda (i) (lookup-type i (lambda () (if (lookup (dotted-env) i (lambda _ #f)) - (tc-error "Rest variable ~a with ... type used in an inappropriate context" (syntax-e i)) + (tc-error/expr "Rest variable ~a with ... type used in an inappropriate context" (syntax-e i)) (lookup-fail (syntax-e i)))))))) ;; refine the type of i in the lexical env diff --git a/collects/typed-scheme/private/parse-type.ss b/collects/typed-scheme/private/parse-type.ss index 686bd2b17f..a5f61ed0b8 100644 --- a/collects/typed-scheme/private/parse-type.ss +++ b/collects/typed-scheme/private/parse-type.ss @@ -73,7 +73,7 @@ (make-pred-ty (list (parse-type #'dom)) (parse-type #'rng) (parse-type #'pred-ty)))] [(dom ... rest ::: -> rng) (and (eq? (syntax-e #'->) '->) - (symbolic-identifier=? #'::: (quote-syntax *))) + (eq? (syntax-e #':::) '*)) (begin (add-type-name-reference #'->) (->* (map parse-type (syntax->list #'(dom ...))) (parse-type #'rest) (parse-type #'rng)))] @@ -106,17 +106,12 @@ (-values (map parse-type (syntax->list #'(tys ...))))] [(case-lambda tys ...) (eq? (syntax-e #'case-lambda) 'case-lambda) - (make-Function (map (lambda (ty) - (syntax-case* ty (->) symbolic-identifier=? - [(dom ... -> rng) - (make-arr - (map parse-type (syntax->list #'(dom ...))) - (parse-type #'rng))])) - (syntax->list #'(tys ...))))] - ;; I wish I could write this - #;[(case-lambda ([dom ... -> rng] ...)) (make-funty (list (make-arr (list (parse-type #'dom) ...) (parse-type #'rng)) ...))] - #;[(list-of t) (make-lst (parse-type #'t))] - #;[(Listof t) (make-lst (parse-type #'t))] + (make-Function + (for/list ([ty (syntax->list #'(tys ...))]) + (let ([t (parse-type ty)]) + (match t + [(Function: (list arr)) arr] + [_ (tc-error/stx ty "Component of case-lambda type was not a function clause")]))))] [(Vectorof t) (eq? (syntax-e #'Vectorof) 'Vectorof) (begin diff --git a/collects/typed-scheme/private/promote-demote.ss b/collects/typed-scheme/private/promote-demote.ss index 60fd33009e..4ec9cf8504 100644 --- a/collects/typed-scheme/private/promote-demote.ss +++ b/collects/typed-scheme/private/promote-demote.ss @@ -30,7 +30,7 @@ (cond [(apply V-in? V (append thn els)) (make-arr null (Un) Univ #f null null)] - [(and drest (V-in? V (cdr drest))) + [(and drest (V-in? V (car drest))) (make-arr (for/list ([d dom]) (var-demote d V)) (vp rng) (var-demote (car drest) V) @@ -66,7 +66,7 @@ (cond [(apply V-in? V (append thn els)) (make-arr null (Un) Univ #f null null)] - [(and drest (V-in? V (cdr drest))) + [(and drest (V-in? V (car drest))) (make-arr (for/list ([d dom]) (var-promote d V)) (vd rng) (var-promote (car drest) V) diff --git a/collects/typed-scheme/private/tc-app-unit.ss b/collects/typed-scheme/private/tc-app-unit.ss index b8f4d9da1a..fc2e5cd1fc 100644 --- a/collects/typed-scheme/private/tc-app-unit.ss +++ b/collects/typed-scheme/private/tc-app-unit.ss @@ -204,17 +204,17 @@ (subtype tail-ty (car (car drests*)))))) (ret (car rngs*))] [else (loop (cdr doms*) (cdr rngs*) (cdr rests*) (cdr drests*))])))] - [(tc-result: (Poly: vars (Function: (list (arr: doms rngs rests #f thn-effs els-effs) ..1)))) + [(tc-result: (Poly: vars (Function: (list (arr: doms rngs rests drests thn-effs els-effs) ..1)))) (let*-values ([(arg-tys) (map tc-expr/t fixed-args)] [(tail-ty tail-bound) (with-handlers ([exn:fail:syntax? (lambda _ (values (tc-expr/t tail) #f))]) (tc/dots tail))]) (for-each (lambda (x) (unless (not (Poly? x)) (tc-error "Polymorphic argument ~a to polymorphic function in apply not allowed" x))) (cons tail-ty arg-tys)) - (let loop ([doms* doms] [rngs* rngs] [rests* rests]) + (let loop ([doms* doms] [rngs* rngs] [rests* rests] [drests* drests]) (cond [(null? doms*) (match f-ty - [(tc-result: (Poly-names: vars (Function: (list (arr: doms rngs rests #f thn-effs els-effs) ..1)))) + [(tc-result: (Poly-names: vars (Function: (list (arr: doms rngs rests drests thn-effs els-effs) ..1)))) (cond [(null? doms) (int-err "how could doms be null: ~a ~a" doms f-ty)] [(= 1 (length doms)) @@ -250,6 +250,7 @@ (car rests*) (car rngs*))) => (lambda (substitution) (ret (subst-all substitution (car rngs*))))] + ;; actual work, when we have a * function and ... final arg [(and (car rests*) tail-bound (<= (length (car doms*)) @@ -261,22 +262,32 @@ (car rests*) (car rngs*))) => (lambda (substitution) (ret (subst-all substitution (car rngs*))))] - [else (loop (cdr doms*) (cdr rngs*) (cdr rests*))])))] + ;; ... function, ... arg + [(and (car drests*) + tail-bound + (eq? tail-bound (cdr (car drests*))) + (= (length (car doms*)) + (length arg-tys)) + (infer vars (cons tail-ty arg-tys) (cons (car (car drests*)) (car doms*)) (car rngs*))) + => (lambda (substitution) (ret (subst-all substitution (car rngs*))))] + ;; if nothing matches, around the loop again + [else (loop (cdr doms*) (cdr rngs*) (cdr rests*) (cdr drests*))])))] [(tc-result: (Poly: vars (Function: '()))) (tc-error/expr #:return (ret (Un)) "Function has no cases")] - [(tc-result: (PolyDots: (list fixed-vars ... dotted-var) + [(tc-result: (PolyDots: (and vars (list fixed-vars ... dotted-var)) (Function: (list (arr: doms rngs rests drests thn-effs els-effs) ..1)))) - (let*-values ([(arg-tys tail-ty) (values (map tc-expr/t fixed-args) - (tc-expr/t tail))] - [(arg-tys0) (append arg-tys (list tail-ty))]) + (let*-values ([(arg-tys) (map tc-expr/t fixed-args)] + [(tail-ty tail-bound) (with-handlers ([exn:fail:syntax? (lambda _ (values (tc-expr/t tail) #f))]) + (tc/dots tail))]) (for-each (lambda (x) (unless (not (Poly? x)) (tc-error "Polymorphic argument ~a to polymorphic function in apply not allowed" x))) (cons tail-ty arg-tys)) (let loop ([doms* doms] [rngs* rngs] [rests* rests] [drests* drests]) (cond [(null? doms*) (match f-ty - [(tc-result: (PolyDots-names: vars (Function: (list (arr: doms rngs rests drests thn-effs els-effs) ..1)))) + [(tc-result: (PolyDots-names: (list fixed-vars ... dotted-var) + (Function: (list (arr: doms rngs rests drests thn-effs els-effs) ..1)))) (cond [(null? doms) (int-err "how could doms be null: ~a ~a" doms f-ty)] [(= 1 (length doms)) @@ -284,11 +295,11 @@ (tc-error/expr #:return (ret (Un)) "polymorphic function domain did not match -~ndomain was: ~a~nrest argument was: ~a~narguments were ~a~n" - (car doms) (car rests) (stringify arg-tys0)) + (car doms) (car rests) (printable-h arg-tys tail-ty tail-bound)) (tc-error/expr #:return (ret (Un)) "polymorphic function domain did not match -~ndomain was: ~a~narguments were ~a~n" - (car doms) (stringify arg-tys0)))] + (car doms) (printable-h arg-tys tail-ty tail-bound)))] [else (tc-error/expr #:return (ret (Un)) @@ -299,22 +310,45 @@ (format "~a rest argument: " (stringify dom) rest) (stringify dom))) "\n") - (stringify arg-tys0))])])] - [(and (= (length (car doms*)) + (printable-h arg-tys tail-ty tail-bound))])])] + ;; the actual work, when we have a * function and a list final argument + [(and (car rests*) + (not tail-bound) + (<= (length (car doms*)) + (length arg-tys)) + (infer/vararg vars + (cons tail-ty arg-tys) + (cons (make-Listof (car rests*)) + (car doms*)) + (car rests*) + (car rngs*))) + => (lambda (substitution) (ret (subst-all substitution (car rngs*))))] + ;; actual work, when we have a * function and ... final arg + [(and (car rests*) + tail-bound + (<= (length (car doms*)) + (length arg-tys)) + (infer/vararg vars + (cons (make-Listof tail-ty) arg-tys) + (cons (make-Listof (car rests*)) + (car doms*)) + (car rests*) + (car rngs*))) + => (lambda (substitution) (ret (subst-all substitution (car rngs*))))] + ;; ... function, ... arg + [(and (car drests*) + tail-bound + (eq? tail-bound (cdr (car drests*))) + (= (length (car doms*)) (length arg-tys)) - (infer (append fixed-vars (list dotted-var)) - arg-tys0 (append (car doms*) (list (make-Listof (car rests*)))) (car rngs*))) - => (lambda (substitution) - (let* ([s (lambda (t) (subst-all substitution t))] - [new-doms* (append (map s (car doms*)) (list (make-Listof (s (car rests*)))))]) - (unless (andmap subtype arg-tys0 new-doms*) - (int-err "Inconsistent substitution - arguments not subtypes: ~n~a~n~a~n" arg-tys0 new-doms*))) - (ret (subst-all substitution (car rngs*))))] + (infer vars (cons tail-ty arg-tys) (cons (car (car drests*)) (car doms*)) (car rngs*))) + => (lambda (substitution) (ret (subst-all substitution (car rngs*))))] + ;; if nothing matches, around the loop again [else (loop (cdr doms*) (cdr rngs*) (cdr rests*) (cdr drests*))])))] [(tc-result: (PolyDots: vars (Function: '()))) (tc-error/expr #:return (ret (Un)) "Function has no cases")] - [f-ty (tc-error/expr #:return (ret (Un)) + [(tc-result: f-ty) (tc-error/expr #:return (ret (Un)) "Type of argument to apply is not a function type: ~n~a" f-ty)])) diff --git a/collects/typed-scheme/private/tc-utils.ss b/collects/typed-scheme/private/tc-utils.ss index 59e65f6fc1..d90ecf436d 100644 --- a/collects/typed-scheme/private/tc-utils.ss +++ b/collects/typed-scheme/private/tc-utils.ss @@ -97,10 +97,6 @@ ;; this is used only for printing type names (define current-type-names (make-parameter (lambda () '()))) -;; error for unbound variables -(define (lookup-fail e) (tc-error "unbound identifier ~a" e)) - - ;; for reporting internal errors in the type checker (define-struct (exn:fail:tc exn:fail) ()) @@ -125,3 +121,4 @@ (define (add-type-name-reference t) (type-name-references (cons t (type-name-references)))) + diff --git a/collects/typed-scheme/private/type-effect-convenience.ss b/collects/typed-scheme/private/type-effect-convenience.ss index b18e8bd137..8a1c95efdf 100644 --- a/collects/typed-scheme/private/type-effect-convenience.ss +++ b/collects/typed-scheme/private/type-effect-convenience.ss @@ -249,8 +249,5 @@ (exit t)))] [_ (exit t)])))) -(define (tc-error/expr msg #:return [return (Un)] #:stx [stx (current-orig-stx)] . rest) - (tc-error/delayed #:stx stx (apply format msg rest)) - return) diff --git a/collects/typed-scheme/private/type-env.ss b/collects/typed-scheme/private/type-env.ss index 7467776502..146847a647 100644 --- a/collects/typed-scheme/private/type-env.ss +++ b/collects/typed-scheme/private/type-env.ss @@ -1,7 +1,7 @@ #lang scheme/base (require (lib "boundmap.ss" "syntax") - "tc-utils.ss") + "tc-utils.ss" "type-utils.ss") (provide register-type finish-register-type diff --git a/collects/typed-scheme/private/type-name-env.ss b/collects/typed-scheme/private/type-name-env.ss index 5ebaa8dde1..370b77e7c6 100644 --- a/collects/typed-scheme/private/type-name-env.ss +++ b/collects/typed-scheme/private/type-name-env.ss @@ -2,7 +2,8 @@ (require syntax/boundmap mzlib/trace - "tc-utils.ss") + "tc-utils.ss" + "type-utils.ss") (provide register-type-name lookup-type-name diff --git a/collects/typed-scheme/private/type-utils.ss b/collects/typed-scheme/private/type-utils.ss index 42bf4788a0..6d182581cc 100644 --- a/collects/typed-scheme/private/type-utils.ss +++ b/collects/typed-scheme/private/type-utils.ss @@ -23,7 +23,9 @@ unfold (struct-out Dotted) (struct-out DottedBoth) - just-Dotted?) + just-Dotted? + tc-error/expr + lookup-fail) ;; substitute : Type Name Type -> Type @@ -139,4 +141,11 @@ (define (just-Dotted? S) (and (Dotted? S) - (not (DottedBoth? S)))) \ No newline at end of file + (not (DottedBoth? S)))) + +(define (tc-error/expr msg #:return [return (make-Union null)] #:stx [stx (current-orig-stx)] . rest) + (tc-error/delayed #:stx stx (apply format msg rest)) + return) + +;; error for unbound variables +(define (lookup-fail e) (tc-error/expr "unbound identifier ~a" e))