From c67aef8622befd981cd1b6621037fb6bc10189d6 Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Fri, 2 Jul 2010 15:02:48 -0400 Subject: [PATCH] Refactoring of tc-app. - Move `check-below' into its own module - Move `tc/apply' to its own unit - Move `tc/funapp' and `tc/funapp1' to own module, outside of unit original commit: 219682bbbef3f1593bde169796087b56e354a7fc --- .../typed-scheme/typecheck/check-below.rkt | 102 ++++++ .../typed-scheme/typecheck/signatures.rkt | 7 +- collects/typed-scheme/typecheck/tc-app.rkt | 344 +----------------- collects/typed-scheme/typecheck/tc-apply.rkt | 211 +++++++++++ .../typed-scheme/typecheck/tc-expr-unit.rkt | 92 +---- collects/typed-scheme/typecheck/tc-funapp.rkt | 171 +++++++++ collects/typed-scheme/typecheck/tc-if.rkt | 12 +- .../typed-scheme/typecheck/tc-lambda-unit.rkt | 2 +- .../typed-scheme/typecheck/tc-let-unit.rkt | 1 + .../typed-scheme/typecheck/typechecker.rkt | 4 +- 10 files changed, 507 insertions(+), 439 deletions(-) create mode 100644 collects/typed-scheme/typecheck/check-below.rkt create mode 100644 collects/typed-scheme/typecheck/tc-apply.rkt create mode 100644 collects/typed-scheme/typecheck/tc-funapp.rkt diff --git a/collects/typed-scheme/typecheck/check-below.rkt b/collects/typed-scheme/typecheck/check-below.rkt new file mode 100644 index 00000000..9f06b138 --- /dev/null +++ b/collects/typed-scheme/typecheck/check-below.rkt @@ -0,0 +1,102 @@ +#lang racket/base + +(require (rename-in "../utils/utils.rkt" [private private-in]) + racket/match (prefix-in - racket/contract) + (types utils convenience union subtype remove-intersect type-table filter-ops) + (private-in parse-type type-annotation) + (rep type-rep) + (only-in (infer infer) restrict) + (except-in (utils tc-utils stxclass-util)) + (env lexical-env type-env-structs tvar-env index-env) + (except-in syntax/parse id) + (only-in srfi/1 split-at)) + +(p/c + [check-below (->d ([s (or/c Type/c tc-results?)] [t (or/c Type/c tc-results?)]) () [_ (if (Type? s) Type/c tc-results?)])]) + +(define (print-object o) + (match o + [(Empty:) "no object"] + [_ (format "object ~a" o)])) + +;; check-below : (/\ (Results Type -> Result) +;; (Results Results -> Result) +;; (Type Results -> Type) +;; (Type Type -> Type)) +(define (check-below tr1 expected) + (define (filter-better? f1 f2) + (match* (f1 f2) + [(f f) #t] + [((FilterSet: f1+ f1-) (FilterSet: f2+ f2-)) + (and (implied-atomic? f2+ f1+) + (implied-atomic? f2- f1-))] + [(_ _) #f])) + (define (object-better? o1 o2) + (match* (o1 o2) + [(o o) #t] + [(o (or (NoObject:) (Empty:))) #t] + [(_ _) #f])) + (match* (tr1 expected) + ;; these two have to be first so that errors can be allowed in cases where multiple values are expected + [((tc-result1: (? (lambda (t) (type-equal? t (Un))))) (tc-results: ts2 (NoFilter:) (NoObject:))) + (ret ts2)] + [((tc-result1: (? (lambda (t) (type-equal? t (Un))))) _) + expected] + + [((tc-results: ts fs os) (tc-results: ts2 (NoFilter:) (NoObject:))) + (unless (= (length ts) (length ts2)) + (tc-error/expr "Expected ~a values, but got ~a" (length ts2) (length ts))) + (unless (for/and ([t ts] [s ts2]) (subtype t s)) + (tc-error/expr "Expected ~a, but got ~a" (stringify ts2) (stringify ts))) + (if (= (length ts) (length ts2)) + (ret ts2 fs os) + (ret ts2))] + [((tc-result1: t1 f1 o1) (tc-result1: t2 (FilterSet: (Top:) (Top:)) (Empty:))) + (cond + [(not (subtype t1 t2)) + (tc-error/expr "Expected ~a, but got ~a" t2 t1)]) + expected] + [((tc-result1: t1 f1 o1) (tc-result1: t2 f2 o2)) + (cond + [(not (subtype t1 t2)) + (tc-error/expr "Expected ~a, but got ~a" t2 t1)] + [(and (not (filter-better? f1 f2)) + (object-better? o1 o2)) + (tc-error/expr "Expected result with filter ~a, got filter ~a" f2 f1)] + [(and (filter-better? f1 f2) + (not (object-better? o1 o2))) + (tc-error/expr "Expected result with object ~a, got object ~a" o2 o1)] + [(and (not (filter-better? f1 f2)) + (not (object-better? o1 o2))) + (tc-error/expr "Expected result with filter ~a and ~a, got filter ~a and ~a" f2 (print-object o2) f1 (print-object o1))]) + expected] + [((tc-results: t1 f o dty dbound) (tc-results: t2 f o dty dbound)) + (unless (andmap subtype t1 t2) + (tc-error/expr "Expected ~a, but got ~a" (stringify t2) (stringify t1))) + expected] + [((tc-results: t1 fs os) (tc-results: t2 fs os)) + (unless (= (length t1) (length t2)) + (tc-error/expr "Expected ~a values, but got ~a" (length t2) (length t1))) + (unless (for/and ([t t1] [s t2]) (subtype t s)) + (tc-error/expr "Expected ~a, but got ~a" (stringify t2) (stringify t1))) + expected] + [((tc-result1: t1 f o) (? Type? t2)) + (unless (subtype t1 t2) + (tc-error/expr "Expected ~a, but got ~a" t2 t1)) + (ret t2 f o)] + [((? Type? t1) (tc-result1: t2 (FilterSet: (list) (list)) (Empty:))) + (unless (subtype t1 t2) + (tc-error/expr "Expected ~a, but got ~a" t2 t1)) + t1] + [((? Type? t1) (tc-result1: t2 f o)) + (if (subtype t1 t2) + (tc-error/expr "Expected result with filter ~a and ~a, got ~a" f (print-object o) t1) + (tc-error/expr "Expected ~a, but got ~a" t2 t1)) + t1] + [((? Type? t1) (? Type? t2)) + (unless (subtype t1 t2) + (tc-error/expr "Expected ~a, but got ~a" t2 t1)) + expected] + [((tc-results: ts fs os dty dbound) (tc-results: ts* fs* os* dty* dbound*)) + (int-err "dotted types in check-below nyi: ~a ~a" dty dty*)] + [(a b) (int-err "unexpected input for check-below: ~a ~a" a b)])) diff --git a/collects/typed-scheme/typecheck/signatures.rkt b/collects/typed-scheme/typecheck/signatures.rkt index 3411232e..0e12899a 100644 --- a/collects/typed-scheme/typecheck/signatures.rkt +++ b/collects/typed-scheme/typecheck/signatures.rkt @@ -11,7 +11,6 @@ [cnt tc-literal (->* (syntax?) ((or/c #f Type/c)) Type/c)] [cnt tc-expr/check (syntax? tc-results? . -> . tc-results?)] [cnt tc-expr/check/t (syntax? tc-results? . -> . Type/c)] - [cnt check-below (->d ([s (or/c Type/c tc-results?)] [t (or/c Type/c tc-results?)]) () [_ (if (Type? s) Type/c tc-results?)])] [cnt tc-exprs ((listof syntax?) . -> . tc-results?)] [cnt tc-exprs/check ((listof syntax?) tc-results? . -> . tc-results?)] [cnt tc-expr/t (syntax? . -> . Type/c)] @@ -32,8 +31,10 @@ (define-signature tc-app^ ([cnt tc/app (syntax? . -> . tc-results?)] - [cnt tc/app/check (syntax? tc-results? . -> . tc-results?)] - [cnt tc/funapp (syntax? syntax? tc-results? (listof tc-results?) (or/c #f tc-results?) . -> . tc-results?)])) + [cnt tc/app/check (syntax? tc-results? . -> . tc-results?)])) + +(define-signature tc-apply^ + ([cnt tc/apply (syntax? syntax? . -> . tc-results?)])) (define-signature tc-let^ ([cnt tc/let-values ((syntax? syntax? syntax? syntax?) ((or/c #f tc-results?)) . ->* . tc-results?)] diff --git a/collects/typed-scheme/typecheck/tc-app.rkt b/collects/typed-scheme/typecheck/tc-app.rkt index c086e6e8..5215073c 100644 --- a/collects/typed-scheme/typecheck/tc-app.rkt +++ b/collects/typed-scheme/typecheck/tc-app.rkt @@ -1,12 +1,12 @@ -#lang scheme/unit +#lang racket/unit (require (rename-in "../utils/utils.rkt" [infer r:infer]) - "signatures.rkt" "tc-metafunctions.rkt" - "tc-app-helper.rkt" "find-annotation.rkt" - "tc-subst.rkt" (prefix-in c: scheme/contract) - syntax/parse scheme/match mzlib/trace scheme/list + "signatures.rkt" "tc-metafunctions.rkt" "check-below.rkt" + "tc-app-helper.rkt" "find-annotation.rkt" "tc-funapp.rkt" + "tc-subst.rkt" (prefix-in c: racket/contract) + syntax/parse racket/match racket/trace scheme/list unstable/sequence unstable/debug - ;; fixme - don't need to be bound in this phase - only to make syntax/parse happy + ;; fixme - don't need to be bound in this phase - only to make tests work scheme/bool racket/unsafe/ops (only-in racket/private/class-internal make-object do-make-object) @@ -27,7 +27,7 @@ "internal-forms.rkt" scheme/base scheme/bool '#%paramz (only-in racket/private/class-internal make-object do-make-object))) -(import tc-expr^ tc-lambda^ tc-let^) +(import tc-expr^ tc-lambda^ tc-let^ tc-apply^) (export tc-app^) @@ -249,193 +249,6 @@ (tc/rec-lambda/check form args body lp ts expected) expected)])) -(define (tc/apply f args) - (define (do-ret t) - (match t - [(Values: (list (Result: ts _ _) ...)) (ret ts)] - [(ValuesDots: (list (Result: ts _ _) ...) dty dbound) (ret ts (for/list ([t ts]) (-FS null null)) (for/list ([t ts]) (make-Empty)) dty dbound)] - [_ (int-err "do-ret fails: ~a" t)])) - (define f-ty (single-value f)) - ;; produces the first n-1 elements of the list, and the last element - (define (split l) (let-values ([(f r) (split-at l (sub1 (length l)))]) - (values f (car r)))) - (define-values (fixed-args tail) - (let ([args* (syntax->list args)]) - (if (null? args*) - (tc-error "apply requires a final list argument, given only a function argument of type ~a" (match f-ty [(tc-result1: t) t])) - (split args*)))) - - (match f-ty - ;; apply of simple function - [(tc-result1: (Function: (list (arr: doms rngs rests drests (list (Keyword: _ _ #f) ...)) ...))) - ;; special case for (case-lambda) - (when (null? doms) - (tc-error/expr #:return (ret (Un)) - "empty case-lambda given as argument to apply")) - (match-let ([arg-tys (map tc-expr/t fixed-args)] - [(tc-result1: tail-ty) (single-value tail)]) - (let loop ([doms* doms] [rngs* rngs] [rests* rests] [drests* drests]) - (cond - ;; we've run out of cases to try, so error out - [(null? doms*) - (tc-error/expr #:return (ret (Un)) - (string-append - "Bad arguments to function in apply:~n" - (domain-mismatches f-ty doms rests drests rngs arg-tys tail-ty #f)))] - ;; this case of the function type has a rest argument - [(and (car rests*) - ;; check that the tail expression is a subtype of the rest argument - (subtype (apply -lst* arg-tys #:tail tail-ty) - (apply -lst* (car doms*) #:tail (make-Listof (car rests*))))) - (do-ret (car rngs*))] - ;; the function expects a dotted rest arg, so make sure we have a ListDots - [(and (car drests*) - (match tail-ty - [(ListDots: tail-ty tail-bound) - ;; the check that it's the same bound - (and (eq? (cdr (car drests*)) tail-bound) - ;; and that the types are correct - (subtypes arg-tys (car doms*)) - (subtype tail-ty (car (car drests*))))] - [_ #f])) - (do-ret (car rngs*))] - ;; otherwise, nothing worked, move on to the next case - [else (loop (cdr doms*) (cdr rngs*) (cdr rests*) (cdr drests*))])))] - ;; apply of simple polymorphic function - [(tc-result1: (Poly: vars (Function: (list (arr: doms rngs rests drests (list (Keyword: _ _ #f) ...)) ..1)))) - (let*-values ([(arg-tys) (map tc-expr/t fixed-args)] - [(tail-ty tail-bound) (match (tc-expr/t tail) - [(ListDots: tail-ty tail-bound) - (values tail-ty tail-bound)] - [t (values t #f)])]) - (let loop ([doms* doms] [rngs* rngs] [rests* rests] [drests* drests]) - (cond [(null? doms*) - (match f-ty - [(tc-result1: (Poly-names: _ (Function: (list (arr: doms rngs rests drests (list (Keyword: _ _ #f) ...)) ..1)))) - (tc-error/expr #:return (ret (Un)) - (string-append - "Bad arguments to polymorphic function in apply:~n" - (domain-mismatches f-ty doms rests drests rngs 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 null - (cons tail-ty arg-tys) - (cons (make-Listof (car rests*)) - (car doms*)) - (car rests*) - (car rngs*))) - => (lambda (substitution) (do-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 null - (cons (make-Listof tail-ty) arg-tys) - (cons (make-Listof (car rests*)) - (car doms*)) - (car rests*) - (car rngs*))) - => (lambda (substitution) (do-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 vars null (cons tail-ty arg-tys) (cons (car (car drests*)) (car doms*)) - (car rngs*))) - => (lambda (substitution) (do-ret (subst-all substitution (car rngs*))))] - ;; if nothing matches, around the loop again - [else (loop (cdr doms*) (cdr rngs*) (cdr rests*) (cdr drests*))])))] - [(tc-result1: (Poly: vars (Function: '()))) - (tc-error/expr #:return (ret (Un)) - "Function has no cases")] - [(tc-result1: (PolyDots: (and vars (list fixed-vars ... dotted-var)) - (Function: (list (arr: doms rngs rests drests (list (Keyword: _ _ #f) ...)) ..1)))) - (let*-values ([(arg-tys) (map tc-expr/t fixed-args)] - [(tail-ty tail-bound) (match (tc-expr/t tail) - [(ListDots: tail-ty tail-bound) - (values tail-ty tail-bound)] - [t (values t #f)])]) - (let loop ([doms* doms] [rngs* rngs] [rests* rests] [drests* drests]) - (define (finish substitution) (do-ret (subst-all substitution (car rngs*)))) - (cond [(null? doms*) - (match f-ty - [(tc-result1: (PolyDots-names: _ (Function: (list (arr: doms rngs rests drests (list (Keyword: _ _ #f) ...)) ..1)))) - (tc-error/expr #:return (ret (Un)) - (string-append - "Bad arguments to polymorphic function in apply:~n" - (domain-mismatches f-ty doms rests drests rngs 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 fixed-vars (list dotted-var) - (cons tail-ty arg-tys) - (cons (make-Listof (car rests*)) - (car doms*)) - (car rests*) - (car rngs*))) - => finish] - ;; actual work, when we have a * function and ... final arg - [(and (car rests*) - tail-bound - (<= (length (car doms*)) - (length arg-tys)) - (infer/vararg fixed-vars (list dotted-var) - (cons (make-Listof tail-ty) arg-tys) - (cons (make-Listof (car rests*)) - (car doms*)) - (car rests*) - (car rngs*))) - => finish] - ;; ... function, ... arg, same bound on ... - [(and (car drests*) - tail-bound - (eq? tail-bound (cdr (car drests*))) - (= (length (car doms*)) - (length arg-tys)) - (infer fixed-vars (list dotted-var) - (cons (make-ListDots tail-ty tail-bound) arg-tys) - (cons (make-ListDots (car (car drests*)) (cdr (car drests*))) (car doms*)) - (car rngs*))) - => finish] - ;; ... function, ... arg, different bound on ... - [(and (car drests*) - tail-bound - (not (eq? tail-bound (cdr (car drests*)))) - (= (length (car doms*)) - (length arg-tys)) - (extend-tvars (list tail-bound (cdr (car drests*))) - (extend-indexes (cdr (car drests*)) - ;; don't need to add tail-bound - it must already be an index - (infer fixed-vars (list dotted-var) - (cons (make-ListDots tail-ty tail-bound) arg-tys) - (cons (make-ListDots (car (car drests*)) (cdr (car drests*))) (car doms*)) - (car rngs*))))) - => finish] - ;; ... function, (List A B C etc) arg - [(and (car drests*) - (not tail-bound) - (eq? (cdr (car drests*)) dotted-var) - (= (length (car doms*)) - (length arg-tys)) - (untuple tail-ty) - (infer/dots fixed-vars dotted-var (append arg-tys (untuple tail-ty)) (car doms*) - (car (car drests*)) (car rngs*) (fv (car rngs*)))) - => finish] - ;; if nothing matches, around the loop again - [else (loop (cdr doms*) (cdr rngs*) (cdr rests*) (cdr drests*))])))] - [(tc-result1: (PolyDots: vars (Function: '()))) - (tc-error/expr #:return (ret (Un)) - "Function has no cases")] - [(tc-result1: f-ty) (tc-error/expr #:return (ret (Un)) - "Type of argument to apply is not a function type: ~n~a" f-ty)])) ;; the main dispatching function ;; syntax tc-results? -> tc-results? @@ -908,147 +721,4 @@ (in-range (length dom))) -(define-syntax (handle-clauses stx) - (syntax-parse stx - [(_ (lsts ... arrs) f-stx args-stx pred infer t argtys expected) - (with-syntax ([(vars ... a) (generate-temporaries #'(lsts ... arrs))]) - (syntax/loc stx - (or (for/or ([vars lsts] ... [a arrs] - #:when (pred vars ... a)) - (let ([substitution (infer vars ... a)]) - (and substitution - (tc/funapp1 f-stx args-stx (subst-all substitution a) argtys expected #:check #f)))) - (poly-fail t argtys #:name (and (identifier? f-stx) f-stx) #:expected expected))))])) - -(define (tc/funapp f-stx args-stx ftype0 argtys expected) - ;(syntax? syntax? tc-results? (listof tc-results?) (or/c #f tc-results?) . -> . tc-results?) - (match* (ftype0 argtys) - ;; we special-case this (no case-lambda) for improved error messages - [((tc-result1: (and t (Function: (list (and a (arr: dom (Values: (list (Result: t-r lf-r lo-r) ...)) rest #f kws)))))) - argtys) - (tc/funapp1 f-stx args-stx a argtys expected)] - [((tc-result1: (and t (Function: (and arrs (list (arr: doms rngs rests (and drests #f) kws) ...))))) - (and argtys (list (tc-result1: argtys-t) ...))) - (or - ;; find the first function where the argument types match - (for/first ([dom doms] [rng rngs] [rest rests] [a arrs] - #:when (subtypes/varargs argtys-t dom rest)) - ;; then typecheck here - ;; we call the separate function so that we get the appropriate filters/objects - (tc/funapp1 f-stx args-stx a argtys expected #:check #f)) - ;; if nothing matched, error - (tc-error/expr - #:return (or expected (ret (Un))) - (string-append "No function domains matched in function application:\n" - (domain-mismatches t doms rests drests rngs argtys-t #f #f))))] - ;; any kind of dotted polymorphic function without mandatory keyword args - [((tc-result1: (and t (PolyDots: - (and vars (list fixed-vars ... dotted-var)) - (Function: (list (and arrs (arr: doms rngs rests drests (list (Keyword: _ _ #f) ...))) ...))))) - (list (tc-result1: argtys-t) ...)) - (handle-clauses (doms rngs rests drests arrs) f-stx args-stx - ;; only try inference if the argument lengths are appropriate - (lambda (dom _ rest drest a) - (cond [rest (<= (length dom) (length argtys))] - [drest (and (<= (length dom) (length argtys)) - (eq? dotted-var (cdr drest)))] - [else (= (length dom) (length argtys))])) - ;; only try to infer the free vars of the rng (which includes the vars in filters/objects) - ;; note that we have to use argtys-t here, since argtys is a list of tc-results - (lambda (dom rng rest drest a) - (cond - [drest - (infer/dots fixed-vars dotted-var argtys-t dom (car drest) rng (fv rng) - #:expected (and expected (tc-results->values expected)))] - [rest - (infer/vararg fixed-vars (list dotted-var) argtys-t dom rest rng - (and expected (tc-results->values expected)))] - ;; no rest or drest - [else (infer fixed-vars (list dotted-var) argtys-t dom rng - (and expected (tc-results->values expected)))])) - t argtys expected)] - ;; regular polymorphic functions without dotted rest, and without mandatory keyword args - [((tc-result1: - (and t - (Poly: - vars - (Function: (list (and arrs (arr: doms rngs rests (and drests #f) (list (Keyword: _ _ #f) ...))) ...))))) - (list (tc-result1: argtys-t) ...)) - (handle-clauses (doms rngs rests arrs) f-stx args-stx - ;; only try inference if the argument lengths are appropriate - (lambda (dom _ rest a) ((if rest <= =) (length dom) (length argtys))) - ;; only try to infer the free vars of the rng (which includes the vars in filters/objects) - ;; note that we have to use argtys-t here, since argtys is a list of tc-results - (lambda (dom rng rest a) (infer/vararg vars null argtys-t dom rest rng (and expected (tc-results->values expected)))) - t argtys expected)] - ;; procedural structs - [((tc-result1: (and sty (Struct: _ _ _ (? Function? proc-ty) _ _ _ _))) _) - (tc/funapp f-stx #`(#,(syntax/loc f-stx dummy) . #,args-stx) (ret proc-ty) (cons ftype0 argtys) expected)] - ;; parameters are functions too - [((tc-result1: (Param: in out)) (list)) (ret out)] - [((tc-result1: (Param: in out)) (list (tc-result1: t))) - (if (subtype t in) - (ret -Void true-filter) - (tc-error/expr #:return (ret -Void true-filter) - "Wrong argument to parameter - expected ~a and got ~a" in t))] - [((tc-result1: (Param: _ _)) _) - (tc-error/expr #:return (ret (Un)) - "Wrong number of arguments to parameter - expected 0 or 1, got ~a" - (length argtys))] - ;; resolve names, polymorphic apps, mu, etc - [((tc-result1: (? needs-resolving? t) f o) _) - (tc/funapp f-stx args-stx (ret (resolve-once t) f o) argtys expected)] - ;; a union of functions can be applied if we can apply all of the elements - [((tc-result1: (Union: (and ts (list (Function: _) ...)))) _) - (ret (for/fold ([result (Un)]) ([fty ts]) - (match (tc/funapp f-stx args-stx (ret fty) argtys expected) - [(tc-result1: t) (Un result t)])))] - ;; error type is a perfectly good fcn type - [((tc-result1: (Error:)) _) (ret (make-Error))] - ;; otherwise fail - [((tc-result1: f-ty) _) - ;(printf "ft: ~a argt: ~a~n" ftype0 argtys) - (tc-error/expr #:return (ret (Un)) - "Cannot apply expression of type ~a, since it is not a function type" f-ty)])) - - -;; syntax? syntax? arr? (listof tc-results?) (or/c #f tc-results) [boolean?] -> tc-results? -(d/c (tc/funapp1 f-stx args-stx ftype0 argtys expected #:check [check? #t]) - ((syntax? syntax? arr? (c:listof tc-results?) (c:or/c #f tc-results?)) (#:check boolean?) . c:->* . tc-results?) - ;(printf "got to here 0~a~n" args-stx) - (match* (ftype0 argtys) - ;; we check that all kw args are optional - [((arr: dom (Values: (and results (list (Result: t-r f-r o-r) ...))) rest #f (and kws (list (Keyword: _ _ #f) ...))) - (list (tc-result1: t-a phi-a o-a) ...)) - ;(printf "got to here 1~a~n" args-stx) - (when check? - (cond [(and (not rest) (not (= (length dom) (length t-a)))) - (tc-error/expr #:return (ret t-r) - "Wrong number of arguments, expected ~a and got ~a" (length dom) (length t-a))] - [(and rest (< (length t-a) (length dom))) - (tc-error/expr #:return (ret t-r) - "Wrong number of arguments, expected at least ~a and got ~a" (length dom) (length t-a))]) - (for ([dom-t (if rest (in-sequence-forever dom rest) (in-list dom))] - [a (in-list (syntax->list args-stx))] - [arg-t (in-list t-a)]) - (parameterize ([current-orig-stx a]) (check-below arg-t dom-t)))) - ;(printf "got to here 2 ~a ~a ~a ~n" dom names o-a) - (let* ([dom-count (length dom)] - [arg-count (+ dom-count (if rest 1 0) (length kws))]) - (let-values - ([(o-a t-a) (for/lists (os ts) - ([nm (in-range arg-count)] - [oa (in-sequence-forever (in-list o-a) (make-Empty))] - [ta (in-sequence-forever (in-list t-a) (Un))]) - (values (if (>= nm dom-count) (make-Empty) oa) - ta))]) - (define-values (t-r f-r o-r) - (for/lists (t-r f-r o-r) - ([r (in-list results)]) - (open-Result r o-a t-a))) - (ret t-r f-r o-r)))] - [((arr: _ _ _ drest '()) _) - (int-err "funapp with drest args ~a ~a NYI" drest argtys)] - [((arr: _ _ _ _ kws) _) - (int-err "funapp with keyword args ~a NYI" kws)])) diff --git a/collects/typed-scheme/typecheck/tc-apply.rkt b/collects/typed-scheme/typecheck/tc-apply.rkt new file mode 100644 index 00000000..a28ef371 --- /dev/null +++ b/collects/typed-scheme/typecheck/tc-apply.rkt @@ -0,0 +1,211 @@ +#lang racket/unit + +(require (rename-in "../utils/utils.rkt" [infer r:infer]) + "signatures.rkt" "tc-app-helper.rkt" + racket/match racket/list + (for-syntax (utils tc-utils)) + (private type-annotation) + (types utils abbrev union subtype resolve convenience type-table substitute) + (utils tc-utils) + (only-in srfi/1 alist-delete) + (except-in (env type-env-structs tvar-env index-env) extend) + (rep type-rep filter-rep object-rep rep-utils) + (r:infer infer) + '#%paramz + (for-template + racket/unsafe/ops + (only-in '#%kernel [apply k:apply]) + "internal-forms.rkt" racket/base racket/bool '#%paramz + (only-in racket/private/class-internal make-object do-make-object))) + +(import tc-expr^ tc-lambda^ tc-let^ tc-app^) +(export tc-apply^) + +(define (do-ret t) + (match t + [(Values: (list (Result: ts _ _) ...)) (ret ts)] + [(ValuesDots: (list (Result: ts _ _) ...) dty dbound) (ret ts (for/list ([t ts]) (-FS null null)) (for/list ([t ts]) (make-Empty)) dty dbound)] + [_ (int-err "do-ret fails: ~a" t)])) + +(define (tc/apply f args) + (define f-ty (single-value f)) + ;; produces the first n-1 elements of the list, and the last element + (define (split l) (let-values ([(f r) (split-at l (sub1 (length l)))]) + (values f (car r)))) + (define-values (fixed-args tail) + (let ([args* (syntax->list args)]) + (if (null? args*) + (tc-error "apply requires a final list argument, given only a function argument of type ~a" (match f-ty [(tc-result1: t) t])) + (split args*)))) + + (match f-ty + ;; apply of simple function + [(tc-result1: (Function: (list (arr: doms rngs rests drests (list (Keyword: _ _ #f) ...)) ...))) + ;; special case for (case-lambda) + (when (null? doms) + (tc-error/expr #:return (ret (Un)) + "empty case-lambda given as argument to apply")) + (match-let ([arg-tys (map tc-expr/t fixed-args)] + [(tc-result1: tail-ty) (single-value tail)]) + (let loop ([doms* doms] [rngs* rngs] [rests* rests] [drests* drests]) + (cond + ;; we've run out of cases to try, so error out + [(null? doms*) + (tc-error/expr #:return (ret (Un)) + (string-append + "Bad arguments to function in apply:~n" + (domain-mismatches f-ty doms rests drests rngs arg-tys tail-ty #f)))] + ;; this case of the function type has a rest argument + [(and (car rests*) + ;; check that the tail expression is a subtype of the rest argument + (subtype (apply -lst* arg-tys #:tail tail-ty) + (apply -lst* (car doms*) #:tail (make-Listof (car rests*))))) + (do-ret (car rngs*))] + ;; the function expects a dotted rest arg, so make sure we have a ListDots + [(and (car drests*) + (match tail-ty + [(ListDots: tail-ty tail-bound) + ;; the check that it's the same bound + (and (eq? (cdr (car drests*)) tail-bound) + ;; and that the types are correct + (subtypes arg-tys (car doms*)) + (subtype tail-ty (car (car drests*))))] + [_ #f])) + (do-ret (car rngs*))] + ;; otherwise, nothing worked, move on to the next case + [else (loop (cdr doms*) (cdr rngs*) (cdr rests*) (cdr drests*))])))] + ;; apply of simple polymorphic function + [(tc-result1: (Poly: vars (Function: (list (arr: doms rngs rests drests (list (Keyword: _ _ #f) ...)) ..1)))) + (let*-values ([(arg-tys) (map tc-expr/t fixed-args)] + [(tail-ty tail-bound) (match (tc-expr/t tail) + [(ListDots: tail-ty tail-bound) + (values tail-ty tail-bound)] + [t (values t #f)])]) + (let loop ([doms* doms] [rngs* rngs] [rests* rests] [drests* drests]) + (cond [(null? doms*) + (match f-ty + [(tc-result1: (Poly-names: _ (Function: (list (arr: doms rngs rests drests (list (Keyword: _ _ #f) ...)) ..1)))) + (tc-error/expr #:return (ret (Un)) + (string-append + "Bad arguments to polymorphic function in apply:~n" + (domain-mismatches f-ty doms rests drests rngs 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 null + (cons tail-ty arg-tys) + (cons (make-Listof (car rests*)) + (car doms*)) + (car rests*) + (car rngs*))) + => (lambda (substitution) (do-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 null + (cons (make-Listof tail-ty) arg-tys) + (cons (make-Listof (car rests*)) + (car doms*)) + (car rests*) + (car rngs*))) + => (lambda (substitution) (do-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 vars null (cons tail-ty arg-tys) (cons (car (car drests*)) (car doms*)) + (car rngs*))) + => (lambda (substitution) (do-ret (subst-all substitution (car rngs*))))] + ;; if nothing matches, around the loop again + [else (loop (cdr doms*) (cdr rngs*) (cdr rests*) (cdr drests*))])))] + [(tc-result1: (Poly: vars (Function: '()))) + (tc-error/expr #:return (ret (Un)) + "Function has no cases")] + [(tc-result1: (PolyDots: (and vars (list fixed-vars ... dotted-var)) + (Function: (list (arr: doms rngs rests drests (list (Keyword: _ _ #f) ...)) ..1)))) + (let*-values ([(arg-tys) (map tc-expr/t fixed-args)] + [(tail-ty tail-bound) (match (tc-expr/t tail) + [(ListDots: tail-ty tail-bound) + (values tail-ty tail-bound)] + [t (values t #f)])]) + (let loop ([doms* doms] [rngs* rngs] [rests* rests] [drests* drests]) + (define (finish substitution) (do-ret (subst-all substitution (car rngs*)))) + (cond [(null? doms*) + (match f-ty + [(tc-result1: (PolyDots-names: _ (Function: (list (arr: doms rngs rests drests (list (Keyword: _ _ #f) ...)) ..1)))) + (tc-error/expr #:return (ret (Un)) + (string-append + "Bad arguments to polymorphic function in apply:~n" + (domain-mismatches f-ty doms rests drests rngs 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 fixed-vars (list dotted-var) + (cons tail-ty arg-tys) + (cons (make-Listof (car rests*)) + (car doms*)) + (car rests*) + (car rngs*))) + => finish] + ;; actual work, when we have a * function and ... final arg + [(and (car rests*) + tail-bound + (<= (length (car doms*)) + (length arg-tys)) + (infer/vararg fixed-vars (list dotted-var) + (cons (make-Listof tail-ty) arg-tys) + (cons (make-Listof (car rests*)) + (car doms*)) + (car rests*) + (car rngs*))) + => finish] + ;; ... function, ... arg, same bound on ... + [(and (car drests*) + tail-bound + (eq? tail-bound (cdr (car drests*))) + (= (length (car doms*)) + (length arg-tys)) + (infer fixed-vars (list dotted-var) + (cons (make-ListDots tail-ty tail-bound) arg-tys) + (cons (make-ListDots (car (car drests*)) (cdr (car drests*))) (car doms*)) + (car rngs*))) + => finish] + ;; ... function, ... arg, different bound on ... + [(and (car drests*) + tail-bound + (not (eq? tail-bound (cdr (car drests*)))) + (= (length (car doms*)) + (length arg-tys)) + (extend-tvars (list tail-bound (cdr (car drests*))) + (extend-indexes (cdr (car drests*)) + ;; don't need to add tail-bound - it must already be an index + (infer fixed-vars (list dotted-var) + (cons (make-ListDots tail-ty tail-bound) arg-tys) + (cons (make-ListDots (car (car drests*)) (cdr (car drests*))) (car doms*)) + (car rngs*))))) + => finish] + ;; ... function, (List A B C etc) arg + [(and (car drests*) + (not tail-bound) + (eq? (cdr (car drests*)) dotted-var) + (= (length (car doms*)) + (length arg-tys)) + (untuple tail-ty) + (infer/dots fixed-vars dotted-var (append arg-tys (untuple tail-ty)) (car doms*) + (car (car drests*)) (car rngs*) (fv (car rngs*)))) + => finish] + ;; if nothing matches, around the loop again + [else (loop (cdr doms*) (cdr rngs*) (cdr rests*) (cdr drests*))])))] + [(tc-result1: (PolyDots: vars (Function: '()))) + (tc-error/expr #:return (ret (Un)) + "Function has no cases")] + [(tc-result1: 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/typecheck/tc-expr-unit.rkt b/collects/typed-scheme/typecheck/tc-expr-unit.rkt index 4e3f12e7..0889fdea 100644 --- a/collects/typed-scheme/typecheck/tc-expr-unit.rkt +++ b/collects/typed-scheme/typecheck/tc-expr-unit.rkt @@ -1,10 +1,11 @@ #lang scheme/unit -(require (rename-in "../utils/utils.rkt" [private private-in])) -(require syntax/kerncase mzlib/trace +(require (rename-in "../utils/utils.rkt" [private private-in]) + syntax/kerncase mzlib/trace scheme/match (prefix-in - scheme/contract) "signatures.rkt" "tc-envops.rkt" "tc-metafunctions.rkt" "tc-subst.rkt" + "check-below.rkt" "tc-funapp.rkt" (types utils convenience union subtype remove-intersect type-table filter-ops) (private-in parse-type type-annotation) (rep type-rep) @@ -165,93 +166,6 @@ (match (tc-expr/check e t) [(tc-result1: t) t])) -(define (print-object o) - (match o - [(Empty:) "no object"] - [_ (format "object ~a" o)])) - -;; check-below : (/\ (Results Type -> Result) -;; (Results Results -> Result) -;; (Type Results -> Type) -;; (Type Type -> Type)) -(define (check-below tr1 expected) - (define (filter-better? f1 f2) - (match* (f1 f2) - [(f f) #t] - [((FilterSet: f1+ f1-) (FilterSet: f2+ f2-)) - (and (implied-atomic? f2+ f1+) - (implied-atomic? f2- f1-))] - [(_ _) #f])) - (define (object-better? o1 o2) - (match* (o1 o2) - [(o o) #t] - [(o (or (NoObject:) (Empty:))) #t] - [(_ _) #f])) - (match* (tr1 expected) - ;; these two have to be first so that errors can be allowed in cases where multiple values are expected - [((tc-result1: (? (lambda (t) (type-equal? t (Un))))) (tc-results: ts2 (NoFilter:) (NoObject:))) - (ret ts2)] - [((tc-result1: (? (lambda (t) (type-equal? t (Un))))) _) - expected] - - [((tc-results: ts fs os) (tc-results: ts2 (NoFilter:) (NoObject:))) - (unless (= (length ts) (length ts2)) - (tc-error/expr "Expected ~a values, but got ~a" (length ts2) (length ts))) - (unless (for/and ([t ts] [s ts2]) (subtype t s)) - (tc-error/expr "Expected ~a, but got ~a" (stringify ts2) (stringify ts))) - (if (= (length ts) (length ts2)) - (ret ts2 fs os) - (ret ts2))] - [((tc-result1: t1 f1 o1) (tc-result1: t2 (FilterSet: (Top:) (Top:)) (Empty:))) - (cond - [(not (subtype t1 t2)) - (tc-error/expr "Expected ~a, but got ~a" t2 t1)]) - expected] - [((tc-result1: t1 f1 o1) (tc-result1: t2 f2 o2)) - (cond - [(not (subtype t1 t2)) - (tc-error/expr "Expected ~a, but got ~a" t2 t1)] - [(and (not (filter-better? f1 f2)) - (object-better? o1 o2)) - (tc-error/expr "Expected result with filter ~a, got filter ~a" f2 f1)] - [(and (filter-better? f1 f2) - (not (object-better? o1 o2))) - (tc-error/expr "Expected result with object ~a, got object ~a" o2 o1)] - [(and (not (filter-better? f1 f2)) - (not (object-better? o1 o2))) - (tc-error/expr "Expected result with filter ~a and ~a, got filter ~a and ~a" f2 (print-object o2) f1 (print-object o1))]) - expected] - [((tc-results: t1 f o dty dbound) (tc-results: t2 f o dty dbound)) - (unless (andmap subtype t1 t2) - (tc-error/expr "Expected ~a, but got ~a" (stringify t2) (stringify t1))) - expected] - [((tc-results: t1 fs os) (tc-results: t2 fs os)) - (unless (= (length t1) (length t2)) - (tc-error/expr "Expected ~a values, but got ~a" (length t2) (length t1))) - (unless (for/and ([t t1] [s t2]) (subtype t s)) - (tc-error/expr "Expected ~a, but got ~a" (stringify t2) (stringify t1))) - expected] - [((tc-result1: t1 f o) (? Type? t2)) - (unless (subtype t1 t2) - (tc-error/expr "Expected ~a, but got ~a" t2 t1)) - (ret t2 f o)] - [((? Type? t1) (tc-result1: t2 (FilterSet: (list) (list)) (Empty:))) - (unless (subtype t1 t2) - (tc-error/expr "Expected ~a, but got ~a" t2 t1)) - t1] - [((? Type? t1) (tc-result1: t2 f o)) - (if (subtype t1 t2) - (tc-error/expr "Expected result with filter ~a and ~a, got ~a" f (print-object o) t1) - (tc-error/expr "Expected ~a, but got ~a" t2 t1)) - t1] - [((? Type? t1) (? Type? t2)) - (unless (subtype t1 t2) - (tc-error/expr "Expected ~a, but got ~a" t2 t1)) - expected] - [((tc-results: ts fs os dty dbound) (tc-results: ts* fs* os* dty* dbound*)) - (int-err "dotted types in check-below nyi: ~a ~a" dty dty*)] - [(a b) (int-err "unexpected input for check-below: ~a ~a" a b)])) - (define (tc-expr/check/type form expected) #;(syntax? Type/c . -> . tc-results?) (tc-expr/check form (ret expected))) diff --git a/collects/typed-scheme/typecheck/tc-funapp.rkt b/collects/typed-scheme/typecheck/tc-funapp.rkt new file mode 100644 index 00000000..56365a4a --- /dev/null +++ b/collects/typed-scheme/typecheck/tc-funapp.rkt @@ -0,0 +1,171 @@ +#lang racket/base + +(require (rename-in "../utils/utils.rkt" [infer r:infer]) + "signatures.rkt" "tc-metafunctions.rkt" + "tc-app-helper.rkt" "find-annotation.rkt" + "tc-subst.rkt" "check-below.rkt" + (prefix-in c: scheme/contract) + syntax/parse scheme/match mzlib/trace scheme/list + unstable/sequence unstable/debug + ;; fixme - don't need to be bound in this phase - only to make syntax/parse happy + scheme/bool + racket/unsafe/ops + (only-in racket/private/class-internal make-object do-make-object) + (only-in '#%kernel [apply k:apply]) + ;; end fixme + (for-syntax syntax/parse scheme/base (utils tc-utils)) + (private type-annotation) + (types utils abbrev union subtype resolve convenience type-table substitute) + (utils tc-utils) + (only-in srfi/1 alist-delete) + (except-in (env type-env-structs tvar-env index-env) extend) + (rep type-rep filter-rep object-rep rep-utils) + (r:infer infer) + '#%paramz + (for-template + racket/unsafe/ops + (only-in '#%kernel [apply k:apply]) + "internal-forms.rkt" scheme/base scheme/bool '#%paramz + (only-in racket/private/class-internal make-object do-make-object))) + +(provide tc/funapp) + +(define-syntax (handle-clauses stx) + (syntax-parse stx + [(_ (lsts ... arrs) f-stx args-stx pred infer t argtys expected) + (with-syntax ([(vars ... a) (generate-temporaries #'(lsts ... arrs))]) + (syntax/loc stx + (or (for/or ([vars lsts] ... [a arrs] + #:when (pred vars ... a)) + (let ([substitution (infer vars ... a)]) + (and substitution + (tc/funapp1 f-stx args-stx (subst-all substitution a) argtys expected #:check #f)))) + (poly-fail t argtys #:name (and (identifier? f-stx) f-stx) #:expected expected))))])) + +(d/c (tc/funapp f-stx args-stx ftype0 argtys expected) + (syntax? syntax? tc-results? (listof tc-results?) (or/c #f tc-results?) . -> . tc-results?) + (match* (ftype0 argtys) + ;; we special-case this (no case-lambda) for improved error messages + [((tc-result1: (and t (Function: (list (and a (arr: dom (Values: _) rest #f kws)))))) argtys) + (tc/funapp1 f-stx args-stx a argtys expected)] + [((tc-result1: (and t (Function: (and arrs (list (arr: doms rngs rests (and drests #f) kws) ...))))) + (and argtys (list (tc-result1: argtys-t) ...))) + (or + ;; find the first function where the argument types match + (for/first ([dom doms] [rng rngs] [rest rests] [a arrs] + #:when (subtypes/varargs argtys-t dom rest)) + ;; then typecheck here + ;; we call the separate function so that we get the appropriate filters/objects + (tc/funapp1 f-stx args-stx a argtys expected #:check #f)) + ;; if nothing matched, error + (tc-error/expr + #:return (or expected (ret (Un))) + (string-append "No function domains matched in function application:\n" + (domain-mismatches t doms rests drests rngs argtys-t #f #f))))] + ;; any kind of dotted polymorphic function without mandatory keyword args + [((tc-result1: (and t (PolyDots: + (and vars (list fixed-vars ... dotted-var)) + (Function: (list (and arrs (arr: doms rngs rests drests (list (Keyword: _ _ #f) ...))) ...))))) + (list (tc-result1: argtys-t) ...)) + (handle-clauses (doms rngs rests drests arrs) f-stx args-stx + ;; only try inference if the argument lengths are appropriate + (lambda (dom _ rest drest a) + (cond [rest (<= (length dom) (length argtys))] + [drest (and (<= (length dom) (length argtys)) + (eq? dotted-var (cdr drest)))] + [else (= (length dom) (length argtys))])) + ;; only try to infer the free vars of the rng (which includes the vars in filters/objects) + ;; note that we have to use argtys-t here, since argtys is a list of tc-results + (lambda (dom rng rest drest a) + (cond + [drest + (infer/dots fixed-vars dotted-var argtys-t dom (car drest) rng (fv rng) + #:expected (and expected (tc-results->values expected)))] + [rest + (infer/vararg fixed-vars (list dotted-var) argtys-t dom rest rng + (and expected (tc-results->values expected)))] + ;; no rest or drest + [else (infer fixed-vars (list dotted-var) argtys-t dom rng + (and expected (tc-results->values expected)))])) + t argtys expected)] + ;; regular polymorphic functions without dotted rest, and without mandatory keyword args + [((tc-result1: + (and t + (Poly: + vars + (Function: (list (and arrs (arr: doms rngs rests (and drests #f) (list (Keyword: _ _ #f) ...))) ...))))) + (list (tc-result1: argtys-t) ...)) + (handle-clauses (doms rngs rests arrs) f-stx args-stx + ;; only try inference if the argument lengths are appropriate + (lambda (dom _ rest a) ((if rest <= =) (length dom) (length argtys))) + ;; only try to infer the free vars of the rng (which includes the vars in filters/objects) + ;; note that we have to use argtys-t here, since argtys is a list of tc-results + (lambda (dom rng rest a) (infer/vararg vars null argtys-t dom rest rng (and expected (tc-results->values expected)))) + t argtys expected)] + ;; procedural structs + [((tc-result1: (and sty (Struct: _ _ _ (? Function? proc-ty) _ _ _ _))) _) + (tc/funapp f-stx #`(#,(syntax/loc f-stx dummy) . #,args-stx) (ret proc-ty) (cons ftype0 argtys) expected)] + ;; parameters are functions too + [((tc-result1: (Param: in out)) (list)) (ret out)] + [((tc-result1: (Param: in out)) (list (tc-result1: t))) + (if (subtype t in) + (ret -Void true-filter) + (tc-error/expr #:return (ret -Void true-filter) + "Wrong argument to parameter - expected ~a and got ~a" in t))] + [((tc-result1: (Param: _ _)) _) + (tc-error/expr #:return (ret (Un)) + "Wrong number of arguments to parameter - expected 0 or 1, got ~a" + (length argtys))] + ;; resolve names, polymorphic apps, mu, etc + [((tc-result1: (? needs-resolving? t) f o) _) + (tc/funapp f-stx args-stx (ret (resolve-once t) f o) argtys expected)] + ;; a union of functions can be applied if we can apply all of the elements + [((tc-result1: (Union: (and ts (list (Function: _) ...)))) _) + (ret (for/fold ([result (Un)]) ([fty ts]) + (match (tc/funapp f-stx args-stx (ret fty) argtys expected) + [(tc-result1: t) (Un result t)])))] + ;; error type is a perfectly good fcn type + [((tc-result1: (Error:)) _) (ret (make-Error))] + ;; otherwise fail + [((tc-result1: f-ty) _) + ;(printf "ft: ~a argt: ~a~n" ftype0 argtys) + (tc-error/expr #:return (ret (Un)) + "Cannot apply expression of type ~a, since it is not a function type" f-ty)])) + + +;; syntax? syntax? arr? (listof tc-results?) (or/c #f tc-results) [boolean?] -> tc-results? +(d/c (tc/funapp1 f-stx args-stx ftype0 argtys expected #:check [check? #t]) + ((syntax? syntax? arr? (c:listof tc-results?) (c:or/c #f tc-results?)) (#:check boolean?) . c:->* . tc-results?) + (match* (ftype0 argtys) + ;; we check that all kw args are optional + [((arr: dom (Values: (and results (list (Result: t-r f-r o-r) ...))) rest #f (and kws (list (Keyword: _ _ #f) ...))) + (list (tc-result1: t-a phi-a o-a) ...)) + (when check? + (cond [(and (not rest) (not (= (length dom) (length t-a)))) + (tc-error/expr #:return (ret t-r) + "Wrong number of arguments, expected ~a and got ~a" (length dom) (length t-a))] + [(and rest (< (length t-a) (length dom))) + (tc-error/expr #:return (ret t-r) + "Wrong number of arguments, expected at least ~a and got ~a" (length dom) (length t-a))]) + (for ([dom-t (if rest (in-sequence-forever dom rest) (in-list dom))] + [a (in-list (syntax->list args-stx))] + [arg-t (in-list t-a)]) + (parameterize ([current-orig-stx a]) (check-below arg-t dom-t)))) + (let* ([dom-count (length dom)] + [arg-count (+ dom-count (if rest 1 0) (length kws))]) + (let-values + ([(o-a t-a) (for/lists (os ts) + ([nm (in-range arg-count)] + [oa (in-sequence-forever (in-list o-a) (make-Empty))] + [ta (in-sequence-forever (in-list t-a) (Un))]) + (values (if (>= nm dom-count) (make-Empty) oa) + ta))]) + (define-values (t-r f-r o-r) + (for/lists (t-r f-r o-r) + ([r (in-list results)]) + (open-Result r o-a t-a))) + (ret t-r f-r o-r)))] + [((arr: _ _ _ drest '()) _) + (int-err "funapp with drest args ~a ~a NYI" drest argtys)] + [((arr: _ _ _ _ kws) _) + (int-err "funapp with keyword args ~a NYI" kws)])) diff --git a/collects/typed-scheme/typecheck/tc-if.rkt b/collects/typed-scheme/typecheck/tc-if.rkt index 288d9de5..c415ef8b 100644 --- a/collects/typed-scheme/typecheck/tc-if.rkt +++ b/collects/typed-scheme/typecheck/tc-if.rkt @@ -1,8 +1,6 @@ -#lang scheme/unit - - -(require (rename-in "../utils/utils.rkt" [infer r:infer])) -(require "signatures.rkt" +#lang racket/unit +(require (rename-in "../utils/utils.rkt" [infer r:infer]) + "signatures.rkt" "check-below.rkt" (rep type-rep filter-rep object-rep) (rename-in (types convenience subtype union utils comparison remove-intersect abbrev filter-ops) [remove *remove]) @@ -11,8 +9,8 @@ (utils tc-utils) (typecheck tc-envops tc-metafunctions) syntax/kerncase - mzlib/trace unstable/debug - scheme/match) + racket/trace unstable/debug + racket/match) ;; if typechecking (import tc-expr^) diff --git a/collects/typed-scheme/typecheck/tc-lambda-unit.rkt b/collects/typed-scheme/typecheck/tc-lambda-unit.rkt index 66494e60..b213cce5 100644 --- a/collects/typed-scheme/typecheck/tc-lambda-unit.rkt +++ b/collects/typed-scheme/typecheck/tc-lambda-unit.rkt @@ -3,7 +3,7 @@ (require (rename-in "../utils/utils.rkt" [infer r:infer]) "signatures.rkt" "tc-metafunctions.rkt" - "tc-subst.rkt" + "tc-subst.rkt" "check-below.rkt" mzlib/trace scheme/list syntax/private/util syntax/stx diff --git a/collects/typed-scheme/typecheck/tc-let-unit.rkt b/collects/typed-scheme/typecheck/tc-let-unit.rkt index 012ef3ee..cbd401cc 100644 --- a/collects/typed-scheme/typecheck/tc-let-unit.rkt +++ b/collects/typed-scheme/typecheck/tc-let-unit.rkt @@ -2,6 +2,7 @@ (require (rename-in "../utils/utils.rkt" [infer r:infer])) (require "signatures.rkt" "tc-metafunctions.rkt" "tc-subst.rkt" + "check-below.rkt" (types utils convenience) (private type-annotation parse-type) (env lexical-env type-alias-env global-env type-env-structs) diff --git a/collects/typed-scheme/typecheck/typechecker.rkt b/collects/typed-scheme/typecheck/typechecker.rkt index 90c46d4e..9a2d2962 100644 --- a/collects/typed-scheme/typecheck/typechecker.rkt +++ b/collects/typed-scheme/typecheck/typechecker.rkt @@ -8,10 +8,10 @@ define-values/invoke-unit/infer link) "signatures.rkt" "tc-if.rkt" "tc-lambda-unit.rkt" "tc-app.rkt" - "tc-let-unit.rkt" + "tc-let-unit.rkt" "tc-apply.rkt" "tc-expr-unit.rkt" "check-subforms-unit.rkt") (provide-signature-elements tc-expr^ check-subforms^) (define-values/invoke-unit/infer - (link tc-if@ tc-lambda@ tc-app@ tc-let@ tc-expr@ check-subforms@)) + (link tc-if@ tc-lambda@ tc-app@ tc-let@ tc-expr@ check-subforms@ tc-apply@))