diff --git a/collects/typed-scheme/typecheck/tc-app-unit.ss b/collects/typed-scheme/typecheck/tc-app-unit.ss deleted file mode 100644 index e0a64c4c64..0000000000 --- a/collects/typed-scheme/typecheck/tc-app-unit.ss +++ /dev/null @@ -1,834 +0,0 @@ -#lang scheme/unit - -(require (only-in "../utils/utils.ss" debug in-syntax printf/log in-pairs rep utils private env [infer r:infer])) -(require "signatures.ss" - stxclass - (for-syntax stxclass) - (rep type-rep effect-rep) - (utils tc-utils) - (private subtype type-utils union type-effect-convenience type-effect-printer resolve-type - type-annotation) - (r:infer infer) - (env type-environments) - (only-in srfi/1 alist-delete) - (only-in scheme/private/class-internal make-object do-make-object) - mzlib/trace mzlib/pretty syntax/kerncase scheme/match - (prefix-in c: scheme/contract) - (for-syntax scheme/base) - (for-template - (only-in '#%kernel [apply k:apply]) - "internal-forms.ss" scheme/base - (only-in scheme/private/class-internal make-object do-make-object))) -(require (r:infer constraint-structs)) - -(import tc-expr^ tc-lambda^ tc-dots^ tc-let^) -(export tc-app^) - -;; comparators that inform the type system -(define (comparator? i) - (or (free-identifier=? i #'eq?) - (free-identifier=? i #'equal?) - (free-identifier=? i #'eqv?) - (free-identifier=? i #'=) - (free-identifier=? i #'string=?))) - -;; typecheck eq? applications -;; identifier identifier expression expression expression -;; identifier expr expr expr expr -> tc-result -(define (tc/eq comparator v1 v2) - (define (e? i) (free-identifier=? i comparator)) - (define (do id val) - (define-syntax alt (syntax-rules () [(_ nm pred ...) - (and (e? #'nm) (or (pred val) ...))])) - (if (or (alt symbol=? symbol?) - (alt string=? string?) - (alt = number?) - (alt eq? boolean? keyword? symbol?) - (alt eqv? boolean? keyword? symbol? number?) - (alt equal? (lambda (x) #t))) - (values (list (make-Restrict-Effect (-val val) id)) - (list (make-Remove-Effect (-val val) id))) - (values (list) (list)))) - (match (list (tc-expr v1) (tc-expr v2)) - [(list (tc-result: id-t (list (Var-True-Effect: id1)) (list (Var-False-Effect: id2))) (tc-result: (Value: val))) - (do id1 val)] - [(list (tc-result: (Value: val)) (tc-result: id-t (list (Var-True-Effect: id1)) (list (Var-False-Effect: id2)))) - (do id1 val)] - [_ (values (list) (list))])) - - -;; typecheck an application: -;; arg-types: the types of the actual parameters -;; arg-effs: the effects of the arguments -;; dom-types: the types of the function's fixed arguments -;; rest-type: the type of the functions's rest parameter, or #f -;; latent-eff: the latent effect of the function -;; arg-stxs: the syntax for each actual parameter, for error reporting -;; [Type] [Type] Maybe[Type] [Syntax] -> (values Listof[Effect] Listof[Effect]) -(define (tc-args arg-types arg-thn-effs arg-els-effs dom-types rest-type latent-thn-eff latent-els-eff arg-stxs) - (define (var-true-effect-v e) (match e - [(Var-True-Effect: v) v])) - (define (var-false-effect-v e) (match e - [(Var-False-Effect: v) v])) - ;; special case for predicates: - (if (and (not (null? latent-thn-eff)) - (not (null? latent-els-eff)) - (not rest-type) - ;(printf "got to =~n") - (= (length arg-types) (length dom-types) 1) - ;(printf "got to var preds~n") - (= (length (car arg-thn-effs)) (length (car arg-els-effs)) 1) - (Var-True-Effect? (caar arg-thn-effs)) ;; thn-effs is a list for each arg - (Var-False-Effect? (caar arg-els-effs)) ;; same with els-effs - (free-identifier=? (var-true-effect-v (caar arg-thn-effs)) - (var-false-effect-v (caar arg-els-effs))) - (subtype (car arg-types) (car dom-types))) - ;; then this was a predicate application, so we construct the appropriate type effect - (values (map (add-var (var-true-effect-v (caar arg-thn-effs))) latent-thn-eff) - (map (add-var (var-true-effect-v (caar arg-thn-effs))) latent-els-eff)) - ;; otherwise, we just ignore the effects. - (let loop ([args arg-types] [doms dom-types] [stxs arg-stxs] [arg-count 1]) - (cond - [(and (null? args) (null? doms)) (values null null)] ;; here, we just return the empty effect - [(null? args) - (tc-error/delayed - "Insufficient arguments to function application, expected ~a, got ~a" - (length dom-types) (length arg-types)) - (values null null)] - [(and (null? doms) rest-type) - (if (subtype (car args) rest-type) - (loop (cdr args) doms (cdr stxs) (add1 arg-count)) - (begin - (tc-error/delayed #:stx (car stxs) - "Rest argument had wrong type, expected: ~a and got: ~a" - rest-type (car args)) - (values null null)))] - [(null? doms) - (tc-error/delayed "Too many arguments to function, expected ~a, got ~a" (length dom-types) (length arg-types)) - (values null null)] - [(subtype (car args) (car doms)) - (loop (cdr args) (cdr doms) (cdr stxs) (add1 arg-count))] - [else - (tc-error/delayed - #:stx (car stxs) - "Wrong function argument type, expected ~a, got ~a for argument ~a" - (car doms) (car args) arg-count) - (loop (cdr args) (cdr doms) (cdr stxs) (add1 arg-count))])))) - - -;(trace tc-args) - -(define (stringify-domain dom rst drst [rng #f]) - (let ([doms-string (if (null? dom) "" (string-append (stringify dom) " "))] - [rng-string (if rng (format " -> ~a" rng) "")]) - (cond [drst - (format "~a~a ... ~a~a" doms-string (car drst) (cdr drst) rng-string)] - [rst - (format "~a~a *~a" doms-string rst rng-string)] - [else (string-append (stringify dom) rng-string)]))) - -(define (domain-mismatches ty doms rests drests rngs arg-tys tail-ty tail-bound #:expected [expected #f]) - (define arguments-str - (stringify-domain arg-tys (if (not tail-bound) tail-ty #f) (if tail-bound (cons tail-ty tail-bound) #f))) - (cond - [(null? doms) - (int-err "How could doms be null: ~a ~a" ty)] - [(= 1 (length doms)) - (format "Domain: ~a~nArguments: ~a~n~a" - (stringify-domain (car doms) (car rests) (car drests)) - arguments-str - (if expected - (format "Result type: ~a~nExpected result: ~a~n" - (car rngs) expected) - ""))] - [else - (format "~a: ~a~nArguments: ~a~n~a" - (if expected "Types" "Domains") - (stringify (if expected - (map stringify-domain doms rests drests rngs) - (map stringify-domain doms rests drests)) - "~n\t") - arguments-str - (if expected - (format "Expected result: ~a~n" expected) - ""))])) - -(define (do-apply-log subst fun arg) - (match* (fun arg) - [('star 'list) (printf/log "Polymorphic apply called with uniform rest arg, list argument\n")] - [('star 'dots) (printf/log "Polymorphic apply called with uniform rest arg, dotted argument\n")] - [('dots 'dots) (printf/log "Polymorphic apply called with non-uniform rest arg, dotted argument\n")]) - (log-result subst)) - -(define (tc/apply f args) - (define f-ty (tc-expr f)) - ;; produces the first n-1 elements of the list, and the last element - (define (split l) - (let loop ([l l] [acc '()]) - (if (null? (cdr l)) - (values (reverse acc) (car l)) - (loop (cdr l) (cons (car l) acc))))) - (define-values (fixed-args tail) (split (syntax->list args))) - - (match f-ty - [(tc-result: (Function: (list (arr: doms rngs rests drests '() thn-effs els-effs) ...))) - (when (null? doms) - (tc-error/expr #:return (ret (Un)) - "empty case-lambda given as argument to apply")) - (let ([arg-tys (map tc-expr/t fixed-args)]) - (let loop ([doms* doms] [rngs* rngs] [rests* rests] [drests* drests]) - (cond [(null? doms*) - (let-values ([(tail-ty tail-bound) - (with-handlers ([exn:fail? (lambda _ (values (tc-expr/t tail) #f))]) - (tc/dots tail))]) - (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 tail-bound))))] - [(and (car rests*) - (let-values ([(tail-ty tail-bound) - (with-handlers ([exn:fail? (lambda _ (values #f #f))]) - (tc/dots tail))]) - (and tail-ty - (subtype (apply -lst* arg-tys #:tail (make-Listof tail-ty)) - (apply -lst* (car doms*) #:tail (make-Listof (car rests*))))))) - (printf/log "Non-poly apply, ... arg\n") - (ret (car rngs*))] - [(and (car rests*) - (let ([tail-ty (with-handlers ([exn:fail? (lambda _ #f)]) - (tc-expr/t tail))]) - (and tail-ty - (subtype (apply -lst* arg-tys #:tail tail-ty) - (apply -lst* (car doms*) #:tail (make-Listof (car rests*))))))) - - (printf/log (if (memq (syntax->datum f) '(+ - * / max min)) - "Simple arithmetic non-poly apply\n" - "Simple non-poly apply\n")) - (ret (car rngs*))] - [(and (car drests*) - (let-values ([(tail-ty tail-bound) - (with-handlers ([exn:fail? (lambda _ (values #f #f))]) - (tc/dots tail))]) - (and tail-ty - (eq? (cdr (car drests*)) tail-bound) - (subtypes arg-tys (car doms*)) - (subtype tail-ty (car (car drests*)))))) - (printf/log "Non-poly apply, ... arg\n") - (ret (car rngs*))] - [else (loop (cdr doms*) (cdr rngs*) (cdr rests*) (cdr drests*))])))] - [(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 of type ~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: (Poly-names: _ (Function: (list (arr: doms rngs rests drests '() _ _) ..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 - (cons tail-ty arg-tys) - (cons (make-Listof (car rests*)) - (car doms*)) - (car rests*) - (car rngs*) - (fv (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*) - (fv (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 vars (cons tail-ty arg-tys) (cons (car (car drests*)) (car doms*)) (car rngs*) (fv (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: (and vars (list fixed-vars ... dotted-var)) - (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))]) - (let loop ([doms* doms] [rngs* rngs] [rests* rests] [drests* drests]) - (cond [(null? doms*) - (match f-ty - [(tc-result: (PolyDots-names: _ (Function: (list (arr: doms rngs rests drests '() _ _) ..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 - (cons tail-ty arg-tys) - (cons (make-Listof (car rests*)) - (car doms*)) - (car rests*) - (car rngs*) - (fv (car rngs*)))) - => (lambda (substitution) - (do-apply-log substitution 'star 'list) - (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*) - (fv (car rngs*)))) - => (lambda (substitution) - (do-apply-log substitution 'star 'dots) - (ret (subst-all substitution (car rngs*))))] - ;; ... function, ... arg, same bound on ... - [(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*) (fv (car rngs*)))) - => (lambda (substitution) - (do-apply-log substitution 'dots 'dots) - (ret (subst-all substitution (car rngs*))))] - ;; ... function, ... arg, different bound on ... - [(and (car drests*) - tail-bound - (not (eq? tail-bound (cdr (car drests*)))) - (= (length (car doms*)) - (length arg-tys)) - (parameterize ([current-tvars (extend-env (list tail-bound (cdr (car drests*))) - (list (make-DottedBoth (make-F tail-bound)) - (make-DottedBoth (make-F (cdr (car drests*))))) - (current-tvars))]) - (infer vars (cons tail-ty arg-tys) (cons (car (car drests*)) (car doms*)) (car rngs*) (fv (car rngs*))))) - => (lambda (substitution) - (define drest-bound (cdr (car drests*))) - (do-apply-log substitution 'dots 'dots) - (ret (substitute-dotted (cadr (assq drest-bound substitution)) - tail-bound - drest-bound - (subst-all (alist-delete drest-bound substitution eq?) - (car rngs*)))))] - ;; ... 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*)))) - => (lambda (substitution) - (define drest-bound (cdr (car drests*))) - (do-apply-log substitution 'dots 'dots) - (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")] - [(tc-result: f-ty) (tc-error/expr #:return (ret (Un)) - "Type of argument to apply is not a function type: ~n~a" f-ty)])) - - - -(define (log-result subst) - (define (dmap-length d) - (match d - [(struct dcon (fixed rest)) (length fixed)] - [(struct dcon-exact (fixed rest)) (length fixed)])) - (define (dmap-rest? d) - (match d - [(struct dcon (fixed rest)) rest] - [(struct dcon-exact (fixed rest)) rest])) - (if (list? subst) - (for ([s subst]) - (match s - [(list v (list imgs ...) starred) - (printf/log "Instantiated ... variable ~a with ~a types\n" v (length imgs))] - [_ (void)])) - (for* ([(cmap dmap) (in-pairs (cset-maps subst))] - [(k v) (dmap-map dmap)]) - (printf/log "Instantiated ... variable ~a with ~a types~a\n" k (dmap-length v) - (if (dmap-rest? v) - " and a starred type" - ""))))) - -(define-syntax (handle-clauses stx) - (syntax-parse stx - [(_ (lsts ... rngs) f-stx pred infer t argtypes expected) - (with-syntax ([(vars ... rng) (generate-temporaries #'(lsts ... rngs))]) - (syntax/loc stx - (or (for/or ([vars lsts] ... [rng rngs] - #:when (pred vars ... rng)) - (let ([substitution (infer vars ... rng)]) - (and substitution - (log-result substitution) - (ret (or expected - (subst-all substitution rng)))))) - (poly-fail t argtypes #:name (and (identifier? f-stx) f-stx) #:expected expected))))])) - -(define (poly-fail t argtypes #:name [name #f] #:expected [expected #f]) - (match t - [(or (Poly-names: msg-vars (Function: (list (arr: msg-doms msg-rngs msg-rests msg-drests '() _ _) ...))) - (PolyDots-names: msg-vars (Function: (list (arr: msg-doms msg-rngs msg-rests msg-drests '() _ _) ...)))) - (let ([fcn-string (if name - (format "function ~a" (syntax->datum name)) - "function")]) - (if (and (andmap null? msg-doms) - (null? argtypes)) - (tc-error/expr #:return (ret (Un)) - (string-append - "Could not infer types for applying polymorphic " - fcn-string - "\n")) - (tc-error/expr #:return (ret (Un)) - (string-append - "Polymorphic " fcn-string " could not be applied to arguments:~n" - (domain-mismatches t msg-doms msg-rests msg-drests msg-rngs argtypes #f #f #:expected expected) - (if (not (for/and ([t (apply append (map fv/list msg-doms))]) (memq t msg-vars))) - (string-append "Type Variables: " (stringify msg-vars) "\n") - "")))))])) - - -(define (tc/funapp f-stx args-stx ftype0 argtys expected) - (match-let* ([(list (tc-result: argtypes arg-thn-effs arg-els-effs) ...) argtys]) - (let outer-loop ([ftype ftype0] - [argtypes argtypes] - [arg-thn-effs arg-thn-effs] - [arg-els-effs arg-els-effs] - [args args-stx]) - (match ftype - ;; procedural structs - [(tc-result: (and sty (Struct: _ _ _ (? Type? proc-ty) _ _ _)) thn-eff els-eff) - (outer-loop (ret proc-ty thn-eff els-eff) - (cons (tc-result-t ftype0) argtypes) - (cons (list) arg-thn-effs) - (cons (list) arg-els-effs) - #`(#,(syntax/loc f-stx dummy) #,@args))] - ;; mu types, etc - [(tc-result: (? needs-resolving? t) thn-eff els-eff) - (outer-loop (ret (resolve-once t) thn-eff els-eff) argtypes arg-thn-effs arg-els-effs args)] - ;; parameters - [(tc-result: (Param: in out)) - (match argtypes - [(list) (ret out)] - [(list t) - (if (subtype t in) - (ret -Void) - (tc-error/expr #:return (ret (Un)) - "Wrong argument to parameter - expected ~a and got ~a" in t))] - [_ (tc-error/expr #:return (ret (Un)) - "Wrong number of arguments to parameter - expected 0 or 1, got ~a" - (length argtypes))])] - ;; single clause functions - ;; FIXME - error on non-optional keywords - [(tc-result: (and t (Function: (list (arr: dom rng rest #f _ latent-thn-effs latent-els-effs)))) - thn-eff els-eff) - (let-values ([(thn-eff els-eff) - (tc-args argtypes arg-thn-effs arg-els-effs dom rest - latent-thn-effs latent-els-effs - (syntax->list args))]) - (ret rng thn-eff els-eff))] - ;; non-polymorphic case-lambda functions - [(tc-result: (and t (Function: (list (arr: doms rngs rests (and drests #f) '() latent-thn-effs latent-els-effs) ..1))) - thn-eff els-eff) - (let loop ([doms* doms] [rngs rngs] [rests* rests]) - (cond [(null? doms*) - (tc-error/expr - #:return (ret (Un)) - (string-append "No function domains matched in function application:\n" - (domain-mismatches t doms rests drests rngs argtypes #f #f)))] - [(subtypes/varargs argtypes (car doms*) (car rests*)) - (when (car rests*) - (printf/log "Simple varargs function application (~a)\n" (syntax->datum f-stx))) - (ret (car rngs))] - [else (loop (cdr doms*) (cdr rngs) (cdr rests*))]))] - ;; simple polymorphic functions, no rest arguments - [(tc-result: (and t - (or (Poly: vars - (Function: (list (arr: doms rngs (and rests #f) (and drests #f) '() thn-effs els-effs) ...))) - (PolyDots: (list vars ...) - (Function: (list (arr: doms rngs (and rests #f) (and drests #f) '() thn-effs els-effs) ...)))))) - (handle-clauses (doms rngs) f-stx - (lambda (dom _) (= (length dom) (length argtypes))) - (lambda (dom rng) (infer vars argtypes dom rng (fv rng) expected)) - t argtypes expected)] - ;; polymorphic varargs - [(tc-result: (and t - (or (Poly: vars (Function: (list (arr: doms rngs rests (and drests #f) '() thn-effs els-effs) ...))) - ;; we want to infer the dotted-var here as well, and we don't use these separately - ;; so we can just use "vars" instead of (list fixed-vars ... dotted-var) - (PolyDots: vars (Function: (list (arr: doms rngs rests (and drests #f) '() thn-effs els-effs) ...)))))) - (printf/log "Polymorphic varargs function application (~a)\n" (syntax->datum f-stx)) - (handle-clauses (doms rests rngs) f-stx - (lambda (dom rest rng) (<= (length dom) (length argtypes))) - (lambda (dom rest rng) (infer/vararg vars argtypes dom rest rng (fv rng) expected)) - t argtypes expected)] - ;; polymorphic ... type - [(tc-result: (and t (PolyDots: - (and vars (list fixed-vars ... dotted-var)) - (Function: (list (arr: doms rngs (and #f rests) (cons dtys dbounds) '() thn-effs els-effs) ...))))) - (printf/log "Polymorphic ... function application (~a)\n" (syntax->datum f-stx)) - (handle-clauses (doms dtys dbounds rngs) f-stx - (lambda (dom dty dbound rng) (and (<= (length dom) (length argtypes)) - (eq? dotted-var dbound))) - (lambda (dom dty dbound rng) - (infer/dots fixed-vars dotted-var argtypes dom dty rng (fv rng) #:expected expected)) - t argtypes expected)] - ;; Union of function types works if we can apply all of them - [(tc-result: (Union: (list (and fs (Function: _)) ...)) e1 e2) - (match-let ([(list (tc-result: ts) ...) (map (lambda (f) (outer-loop - (ret f e1 e2) argtypes arg-thn-effs arg-els-effs args)) fs)]) - (ret (apply Un ts)))] - ;; error type is a perfectly good fcn type - [(tc-result: (Error:)) (ret (make-Error))] - [(tc-result: f-ty _ _) (tc-error/expr #:return (ret (Un)) - "Cannot apply expression of type ~a, since it is not a function type" f-ty)])))) - -;(trace tc/funapp) - - - -(define (tc/app form) (tc/app/internal form #f)) - -(define (tc/app/check form expected) - (define t (tc/app/internal form expected)) - (check-below t expected) - (ret expected)) - -(define-syntax-class lv-clause - #:transparent - (pattern [(v:id ...) e:expr])) - -(define-syntax-class lv-clauses - #:transparent - (pattern (cl:lv-clause ...) - #:with (e ...) #'(cl.e ...) - #:with (vs ...) #'((cl.v ...) ...))) - -(define-syntax-class core-expr - #:literals (reverse letrec-syntaxes+values let-values #%plain-app - if letrec-values begin #%plain-lambda set! case-lambda - begin0 with-continuation-mark) - #:transparent - (pattern (let-values cls:lv-clauses body) - #:with (expr ...) #'(cls.e ... body)) - (pattern (letrec-values cls:lv-clauses body) - #:with (expr ...) #'(cls.e ... body)) - (pattern (letrec-syntaxes+values _ cls:lv-clauses body) - #:with (expr ...) #'(cls.e ... body)) - (pattern (#%plain-app expr ...)) - (pattern (if expr ...)) - (pattern (with-continuation-mark expr ...)) - (pattern (begin expr ...)) - (pattern (begin0 expr ...)) - (pattern (#%plain-lambda _ e) - #:with (expr ...) #'(e)) - (pattern (case-lambda [_ expr] ...)) - (pattern (set! _ e) - #:with (expr ...) #'(e)) - (pattern _ - #:with (expr ...) #'())) - -;; expr id -> type or #f -;; if there is a binding in stx of the form: -;; (let ([x (reverse name)]) e) -;; where x has a type annotation, return that annotation, otherwise #f -(define (find-annotation stx name) - (define (find s) (find-annotation s name)) - (define (match? b) - (syntax-parse b - #:literals (#%plain-app reverse) - [c:lv-clause - #:with (#%plain-app reverse n:id) #'c.e - #:with (v) #'(c.v ...) - #:when (free-identifier=? name #'n) - (type-annotation #'v)] - [_ #f])) - (syntax-parse stx - #:literals (let-values) - [(let-values cls:lv-clauses body) - (or (ormap match? (syntax->list #'cls)) - (find #'body))] - [e:core-expr - (ormap find (syntax->list #'(e.expr ...)))])) - - -(define (check-do-make-object cl pos-args names named-args) - (let* ([names (map syntax-e (syntax->list names))] - [name-assoc (map list names (syntax->list named-args))]) - (let loop ([t (tc-expr cl)]) - (match t - [(tc-result: (? Mu? t)) (loop (ret (unfold t)))] - [(tc-result: (and c (Class: pos-tys (list (and tnflds (list tnames _ _)) ...) _))) - (unless (= (length pos-tys) - (length (syntax->list pos-args))) - (tc-error/delayed "expected ~a positional arguments, but got ~a" - (length pos-tys) (length (syntax->list pos-args)))) - ;; use for, since they might be different lengths in error case - (for ([pa (in-syntax pos-args)] - [pt (in-list pos-tys)]) - (tc-expr/check pa pt)) - (for ([n names] - #:when (not (memq n tnames))) - (tc-error/delayed - "unknown named argument ~a for class~nlegal named arguments are ~a" - n (stringify tnames))) - (for-each (match-lambda - [(list tname tfty opt?) - (let ([s (cond [(assq tname name-assoc) => cadr] - [(not opt?) - (tc-error/delayed "value not provided for named init arg ~a" tname) - #f] - [else #f])]) - (if s - ;; this argument was present - (tc-expr/check s tfty) - ;; this argument wasn't provided, and was optional - #f))]) - tnflds) - (ret (make-Instance c))] - [(tc-result: t) - (tc-error/expr #:return (ret (Un)) "expected a class value for object creation, got: ~a" t)])))) - -(define (tc-keywords form arities kws kw-args pos-args expected) - (match arities - [(list (arr: dom rng rest #f ktys _ _)) - ;; assumes that everything is in sorted order - (let loop ([actual-kws kws] - [actuals (map tc-expr/t (syntax->list kw-args))] - [formals ktys]) - (match* (actual-kws formals) - [('() '()) - (void)] - [(_ '()) - (tc-error/expr #:return (ret (Un)) - "Unexpected keyword argument ~a" (car actual-kws))] - [('() (cons fst rst)) - (match fst - [(Keyword: k _ #t) - (tc-error/expr #:return (ret (Un)) - "Missing keyword argument ~a" k)] - [_ (loop actual-kws actuals rst)])] - [((cons k kws-rest) (cons (Keyword: k* t req?) form-rest)) - (cond [(eq? k k*) ;; we have a match - (unless (subtype (car actuals) t) - (tc-error/delayed - "Wrong function argument type, expected ~a, got ~a for keyword argument ~a" - t (car actuals) k)) - (loop kws-rest (cdr actuals) form-rest)] - [req? ;; this keyword argument was required - (tc-error/delayed "Missing keyword argument ~a" k*) - (loop kws-rest (cdr actuals) form-rest)] - [else ;; otherwise, ignore this formal param, and continue - (loop actual-kws actuals form-rest)])])) - (tc/funapp (car (syntax-e form)) kw-args (ret (make-Function arities)) (map tc-expr (syntax->list pos-args)) expected)] - [_ (int-err "case-lambda w/ keywords not supported")])) - - -(define (type->list t) - (match t - [(Pair: (Value: (? keyword? k)) b) (cons k (type->list b))] - [(Value: '()) null] - [_ (int-err "bad value in type->list: ~a" t)])) - -;; id: identifier -;; sym: a symbol -;; mod: a quoted require spec like 'scheme/base -;; is id the name sym defined in mod? -(define (id-from? id sym mod) - (and (eq? (syntax-e id) sym) - (eq? (module-path-index-resolve (syntax-source-module id)) - ((current-module-name-resolver) mod #f #f #f)))) - -(define (tc/app/internal form expected) - (kernel-syntax-case* form #f - (values apply k:apply not list list* call-with-values do-make-object make-object cons - andmap ormap) ;; the special-cased functions - ;; special case for delay - [(#%plain-app - mp1 - (#%plain-lambda () - (#%plain-app mp2 (#%plain-app call-with-values (#%plain-lambda () e) list)))) - (and (id-from? #'mp1 'make-promise 'scheme/promise) - (id-from? #'mp2 'make-promise 'scheme/promise)) - (ret (-Promise (tc-expr/t #'e)))] - ;; special cases for classes - [(#%plain-app make-object cl . args) - (check-do-make-object #'cl #'args #'() #'())] - [(#%plain-app do-make-object cl (#%plain-app list . pos-args) (#%plain-app list (#%plain-app cons 'names named-args) ...)) - (check-do-make-object #'cl #'pos-args #'(names ...) #'(named-args ...))] - [(#%plain-app do-make-object . args) - (int-err "bad do-make-object : ~a" (syntax->datum #'args))] - ;; call-with-values - [(#%plain-app call-with-values prod con) - (match-let* ([(tc-result: prod-t) (tc-expr #'prod)]) - (define (values-ty->list t) - (match t - [(Values: ts) ts] - [_ (list t)])) - (match prod-t - [(Function: (list (arr: (list) vals _ #f '() _ _))) - (tc/funapp #'con #'prod (tc-expr #'con) (map ret (values-ty->list vals)) expected)] - [_ (tc-error/expr #:return (ret (Un)) - "First argument to call with values must be a function that can accept no arguments, got: ~a" - prod-t)]))] - ;; special cases for `values' - ;; special case the single-argument version to preserve the effects - [(#%plain-app values arg) (tc-expr #'arg)] - [(#%plain-app values . args) - (let ([tys (map tc-expr/t (syntax->list #'args))]) - (ret (-values tys)))] - ;; special case for `list' - [(#%plain-app list . args) - (let ([tys (map tc-expr/t (syntax->list #'args))]) - (ret (apply -lst* tys)))] - ;; special case for `list*' - [(#%plain-app list* . args) - (match-let* ([(list last tys-r ...) (reverse (map tc-expr/t (syntax->list #'args)))] - [tys (reverse tys-r)]) - (ret (foldr make-Pair last tys)))] - ;; in eq? cases, call tc/eq - [(#%plain-app eq? v1 v2) - (and (identifier? #'eq?) (comparator? #'eq?)) - (begin - ;; make sure the whole expression is type correct - (tc/funapp #'eq? #'(v1 v2) (tc-expr #'eq?) (map tc-expr (syntax->list #'(v1 v2))) expected) - ;; check thn and els with the eq? info - (let-values ([(thn-eff els-eff) (tc/eq #'eq? #'v1 #'v2)]) - (ret B thn-eff els-eff)))] - ;; special case for `not' - [(#%plain-app not arg) - (match (tc-expr #'arg) - ;; if arg was a predicate application, we swap the effects - [(tc-result: t thn-eff els-eff) - (ret B (map var->type-eff els-eff) (map var->type-eff thn-eff))])] - [(#%plain-app k:apply . args) - (tc/app/internal #'(#%plain-app apply . args) expected)] - ;; special-er case for (apply values (list x y z)) - [(#%plain-app apply values e) - (cond [(with-handlers ([exn:fail? (lambda _ #f)]) - (untuple (tc-expr/t #'e))) - => (lambda (t) (ret (-values t)))] - [else (tc/apply #'values #'(e))])] - ;; special case for `apply' - [(#%plain-app apply f . args) (tc/apply #'f #'args)] - ;; special case for keywords - [(#%plain-app - (#%plain-app kpe kws num fn) - kw-list - (#%plain-app list . kw-arg-list) - . pos-args) - (eq? (syntax-e #'kpe) 'keyword-procedure-extract) - (match (tc-expr #'fn) - [(tc-result: (Function: arities)) - (tc-keywords form arities (type->list (tc-expr/t #'kws)) #'kw-arg-list #'pos-args expected)] - [(tc-result: t) (tc-error/expr #:return (ret (Un)) - "Cannot apply expression of type ~a, since it is not a function type" t)])] - ;; even more special case for match - [(#%plain-app (letrec-values ([(lp) (#%plain-lambda args . body)]) lp*) . actuals) - (and expected (not (andmap type-annotation (syntax->list #'args))) (free-identifier=? #'lp #'lp*)) - (let-loop-check form #'lp #'actuals #'args #'body expected)] - ;; or/andmap of ... argument - [(#%plain-app or/andmap f arg) - (and - (identifier? #'or/andmap) - (or (free-identifier=? #'or/andmap #'ormap) - (free-identifier=? #'or/andmap #'andmap)) - (with-handlers ([exn:fail? (lambda _ #f)]) - (tc/dots #'arg) - #t)) - (let-values ([(ty bound) (tc/dots #'arg)]) - (parameterize ([current-tvars (extend-env (list bound) - (list (make-DottedBoth (make-F bound))) - (current-tvars))]) - (match-let* ([ft (tc-expr #'f)] - [(tc-result: t) (tc/funapp #'f #'(arg) ft (list (ret ty)) #f)]) - (ret (Un (-val #f) t)))))] - ;; infer for ((lambda - [(#%plain-app (#%plain-lambda (x ...) . body) args ...) - (= (length (syntax->list #'(x ...))) - (length (syntax->list #'(args ...)))) - (tc/let-values/check #'((x) ...) #'(args ...) #'body - #'(let-values ([(x) args] ...) . body) - expected)] - ;; default case - [(#%plain-app f args ...) - (tc/funapp #'f #'(args ...) (tc-expr #'f) (map tc-expr (syntax->list #'(args ...))) expected)])) - -(define (let-loop-check form lp actuals args body expected) - (kernel-syntax-case* #`(#,args #,body #,actuals) #f (null?) - [((val acc ...) - ((if (#%plain-app null? val*) thn els)) - (actual actuals ...)) - (and (free-identifier=? #'val #'val*) - (ormap (lambda (a) (find-annotation #'(if (#%plain-app null? val*) thn els) a)) - (syntax->list #'(acc ...)))) - (let* ([ts1 (generalize (tc-expr/t #'actual))] - [ann-ts (for/list ([a (in-syntax #'(acc ...))] - [ac (in-syntax #'(actuals ...))]) - (or (find-annotation #'(if (#%plain-app null? val*) thn els) a) - (generalize (tc-expr/t ac))))] - [ts (cons ts1 ann-ts)]) - ;; check that the actual arguments are ok here - (map tc-expr/check (syntax->list #'(actuals ...)) ann-ts) - ;; then check that the function typechecks with the inferred types - (tc/rec-lambda/check form args body lp ts expected) - (ret expected))] - ;; special case when argument needs inference - [_ - (let ([ts (for/list ([ac (syntax->list actuals)] - [f (syntax->list args)]) - (or - (type-annotation f #:infer #t) - (generalize (tc-expr/t ac))))]) - (tc/rec-lambda/check form args body lp ts expected) - (ret expected))])) - -(define (matches? stx) - (let loop ([stx stx] [ress null] [acc*s null]) - (syntax-case stx (#%plain-app reverse) - [([(res) (#%plain-app reverse acc*)] . more) - (loop #'more (cons #'res ress) (cons #'acc* acc*s))] - [rest - (syntax->list #'rest) - (begin - ;(printf "ress: ~a~n" (map syntax-e ress)) - (list (reverse ress) (reverse acc*s) #'rest))] - [_ #f]))) - -;(trace tc/app/internal) diff --git a/collects/typed-scheme/typecheck/tc-if-unit.ss b/collects/typed-scheme/typecheck/tc-if-unit.ss deleted file mode 100644 index 3d077cdcde..0000000000 --- a/collects/typed-scheme/typecheck/tc-if-unit.ss +++ /dev/null @@ -1,192 +0,0 @@ -#lang scheme/unit - -(require (rename-in "../utils/utils.ss" [infer r:infer])) -(require "signatures.ss" - (rep type-rep filter-rep object-rep) - (rename-in (types convenience subtype union utils comparison remove-intersect) - [remove *remove]) - (env lexical-env) - (r:infer infer) - (utils tc-utils mutated-vars) - syntax/kerncase - mzlib/trace - mzlib/plt-match) - -;; if typechecking -(import tc-expr^) -(export tc-if^) - - - -;; combinators for typechecking in the context of effects -;; t/f tells us whether this is the true or the false branch of an if -;; neccessary for handling true/false effects -;; Boolean Expr listof[Effect] option[type] -> TC-Result -(define (tc-expr/eff t/f expr effs expected) - ;; this flag represents whether the refinement proves that this expression cannot be executed - (let ([flag (box #f)]) - ;; this does the operation on the old type - ;; type-op : (Type Type -> Type) Type -> _ Type -> Type - (define ((type-op f t) _ old) - (let ([new-t (f old t)]) - ;; if this operation produces an uninhabitable type, then this expression can't be executed - (when (type-equal? new-t (Un)) - (set-box! flag #t)) - ;; have to return something here, so that we can continue typechecking - new-t)) - ;; loop : listof[effect] -> tc-result - (let loop ([effs effs]) - ;; convenience macro for checking the rest of the list - (define-syntax check-rest - (syntax-rules () - [(check-rest f v) - (with-update-type/lexical f v (loop (cdr effs)))] - [(check-rest f t v) - (check-rest (type-op f t) v)])) - (if (null? effs) - ;; base case - (let* ([reachable? (not (unbox flag))]) - (unless reachable? - (warn-unreachable expr)) - (cond - ;; if flag is true, then we don't want to verify that this branch has the appropriate type - ;; in particular, it might be (void) - [(and expected reachable?) - (tc-expr/check expr expected)] - ;; this code is reachable, but we have no expected type - [reachable? - (tc-expr expr)] - ;; otherwise, this code is unreachable - ;; and the resulting type should be the empty type - [(check-unreachable-code?) - (tc-expr/check expr Univ) - (ret (Un))] - [else - (ret (Un))])) - ;; recursive case - (match (car effs) - ;; these effects have no consequence for the typechecking - [(True-Effect:) - (or t/f (set-box! flag #t)) - (loop (cdr effs))] - [(False-Effect:) - (and t/f (set-box! flag #t)) - (loop (cdr effs))] - ;; restrict v to have a type that's a subtype of t - [(Restrict-Effect: t v) - (check-rest restrict t v)] - ;; remove t from the type of v - [(Remove-Effect: t v) (check-rest *remove t v)] - ;; just replace the type of v with (-val #f) - [(Var-False-Effect: v) (check-rest (lambda (_ old) (-val #f)) v)] - ;; v cannot have type (-val #f) - [(Var-True-Effect: v) - (check-rest *remove (-val #f) v)]))))) - -;; the main function -(define (tc/if-twoarm tst thn els) - ;; check in the context of the effects, and return - (match-let* ([(tc-result: tst-ty tst-thn-eff tst-els-eff) (tc-expr tst)] - [(tc-result: thn-ty thn-thn-eff thn-els-eff) (tc-expr/eff #t thn tst-thn-eff #f)] - [(tc-result: els-ty els-thn-eff els-els-eff) (tc-expr/eff #f els tst-els-eff #f)]) - (match* (els-ty thn-thn-eff thn-els-eff els-thn-eff els-els-eff) - ;; this is the case for `or' - ;; the then branch has to be #t - ;; the else branch has to be a simple predicate - ;; FIXME - can something simpler be done by using demorgan's law? - ;; note that demorgan's law doesn't hold for scheme `and' and `or' because they can produce arbitrary values - ;; FIXME - mzscheme's or macro doesn't match this! - [(_ (list (True-Effect:)) (list (True-Effect:)) (list (Restrict-Effect: t v)) (list (Remove-Effect: t v*))) - (=> unmatch) - (match (list tst-thn-eff tst-els-eff) - ;; check that the test was also a simple predicate - [(list (list (Restrict-Effect: s u)) (list (Remove-Effect: s u*))) - (if (and - ;; check that all the predicates are for the for the same identifier - (free-identifier=? u u*) - (free-identifier=? v v*) - (free-identifier=? v u)) - ;; this is just a very simple or - (ret (Un (-val #t) els-ty) - ;; the then and else effects are just the union of the two types - (list (make-Restrict-Effect (Un s t) v)) - (list (make-Remove-Effect (Un s t) v))) - ;; otherwise, something complicated is happening and we bail - (unmatch))] - ;; similarly, bail here - [_ (unmatch)])] - ;; this is the case for `and' - [(_ _ _ (list (False-Effect:)) (list (False-Effect:))) - (ret (Un (-val #f) thn-ty) - ;; we change variable effects to type effects in the test, - ;; because only the boolean result of the test is used - ;; whereas, the actual value of the then branch is returned, not just the boolean result - (append (map var->type-eff tst-thn-eff) thn-thn-eff) - ;; no else effects for and, because any branch could have been false - (list))] - ;; if the else branch can never happen, just use the effect of the then branch - [((Union: (list)) _ _ _ _) - (ret thn-ty thn-thn-eff thn-els-eff)] - ;; otherwise this expression has no effects - [(_ _ _ _ _) - (ret (Un thn-ty els-ty))]))) - -;; checking version -(define (tc/if-twoarm/check tst thn els expected) - ;; check in the context of the effects, and return - (match-let* ([(tc-result: tst-ty tst-thn-eff tst-els-eff) (tc-expr tst)] - [(tc-result: thn-ty thn-thn-eff thn-els-eff) (tc-expr/eff #t thn tst-thn-eff expected)] - [(tc-result: els-ty els-thn-eff els-els-eff) (tc-expr/eff #f els tst-els-eff expected)]) - (match* (els-ty thn-thn-eff thn-els-eff els-thn-eff els-els-eff) - ;; this is the case for `or' - ;; the then branch has to be #t - ;; the else branch has to be a simple predicate - ;; FIXME - can something simpler be done by using demorgan's law? - ;; note that demorgan's law doesn't hold for scheme `and' and `or' because they can produce arbitrary values - ;; FIXME - mzscheme's or macro doesn't match this! - [(_ (list (True-Effect:)) (list (True-Effect:)) (list (Restrict-Effect: t v)) (list (Remove-Effect: t v*))) - (=> unmatch) - (match (list tst-thn-eff tst-els-eff) - ;; check that the test was also a simple predicate - [(list (list (Restrict-Effect: s u)) (list (Remove-Effect: s u*))) - (if (and - ;; check that all the predicates are for the for the same identifier - (free-identifier=? u u*) - (free-identifier=? v v*) - (free-identifier=? v u)) - ;; this is just a very simple or - (let ([t (Un (-val #t) els-ty)]) - (check-below t expected) - (ret t - ;; the then and else effects are just the union of the two types - (list (make-Restrict-Effect (Un s t) v)) - (list (make-Remove-Effect (Un s t) v)))) - ;; otherwise, something complicated is happening and we bail - (unmatch))] - ;; similarly, bail here - [_ (unmatch)])] - ;; this is the case for `and' - [(_ _ _ (list (False-Effect:)) (list (False-Effect:))) - (let ([t (Un thn-ty (-val #f))]) - (check-below t expected) - (ret t - ;; we change variable effects to type effects in the test, - ;; because only the boolean result of the test is used - ;; whereas, the actual value of the then branch is returned, not just the boolean result - (append (map var->type-eff tst-thn-eff) thn-thn-eff) - ;; no else effects for and, because any branch could have been false - (list)))] - ;; if the else branch can never happen, just use the effect of the then branch - [((Union: (list)) _ _ _ _) - (ret thn-ty - ;; we change variable effects to type effects in the test, - ;; because only the boolean result of the test is used - ;; whereas, the actual value of the then branch is returned, not just the boolean result - thn-thn-eff - ;; no else effects for and, because any branch could have been false - thn-els-eff)] - ;; otherwise this expression has no effects - [(_ _ _ _ _) - (let ([t (Un thn-ty els-ty)]) - (check-below t expected) - (ret t))]))) diff --git a/collects/typed-scheme/typecheck/tc-new-app-unit.ss b/collects/typed-scheme/typecheck/tc-new-app-unit.ss deleted file mode 100644 index a29568b275..0000000000 --- a/collects/typed-scheme/typecheck/tc-new-app-unit.ss +++ /dev/null @@ -1,18 +0,0 @@ -#lang scheme/unit - -(require "signatures.ss" "../utils/utils.ss") -(require (utils tc-utils)) - -(import tc-expr^ tc-lambda^ tc-dots^) -(export tc-app^) - -(define (tc/app . args) - (int-err "tc/app NYI")) - -(define (tc/app/check . args) - (int-err "tc/app/check NYI")) - -(define (tc/funapp . args) - (int-err "tc/funapp NYI")) - -