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
This commit is contained in:
Sam Tobin-Hochstadt
parent
6aa8cbee9d
commit
c67aef8622
102
collects/typed-scheme/typecheck/check-below.rkt
Normal file
102
collects/typed-scheme/typecheck/check-below.rkt
Normal file
|
|
@ -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)]))
|
||||
|
|
@ -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?)]
|
||||
|
|
|
|||
|
|
@ -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)]))
|
||||
|
||||
|
|
|
|||
211
collects/typed-scheme/typecheck/tc-apply.rkt
Normal file
211
collects/typed-scheme/typecheck/tc-apply.rkt
Normal file
|
|
@ -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)]))
|
||||
|
|
@ -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)))
|
||||
|
|
|
|||
171
collects/typed-scheme/typecheck/tc-funapp.rkt
Normal file
171
collects/typed-scheme/typecheck/tc-funapp.rkt
Normal file
|
|
@ -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)]))
|
||||
|
|
@ -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^)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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@))
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user