From 6296ffbfcf85a624227f11f486fb195954e4479b Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Fri, 20 Jun 2008 13:07:08 -0400 Subject: [PATCH] * Added code to check that substitution gets rid of all appropriate variables (and fails if not) * Added weird dotted as subtype of * case (dcon-exact) --- .../private/constraint-structs.ss | 13 ++- collects/typed-scheme/private/constraints.ss | 3 - collects/typed-scheme/private/dmap.ss | 11 +++ collects/typed-scheme/private/infer-unit.ss | 93 +++++++++++++------ collects/typed-scheme/private/tc-app-unit.ss | 52 ++++++----- collects/typed-scheme/private/type-utils.ss | 2 +- 6 files changed, 118 insertions(+), 56 deletions(-) diff --git a/collects/typed-scheme/private/constraint-structs.ss b/collects/typed-scheme/private/constraint-structs.ss index 911f7ae883..700baecf95 100644 --- a/collects/typed-scheme/private/constraint-structs.ss +++ b/collects/typed-scheme/private/constraint-structs.ss @@ -11,6 +11,10 @@ ;; rest : option[c] (define-struct dcon (fixed rest) #:prefab) +;; fixed : Listof[c] +;; rest : c +(define-struct dcon-exact (fixed rest) #:prefab) + ;; type : c ;; bound : vars (define-struct dcon-dotted (type bound) #:prefab) @@ -26,16 +30,21 @@ ;; don't want to rule them out too early (define-struct cset (maps) #:prefab) + (define (hashof k/c v/c) (flat-named-contract (format "#" k/c v/c) (lambda (h) + (define k/c? (if (flat-contract? k/c) (flat-contract-predicate k/c) k/c)) + (define v/c? (if (flat-contract? v/c) (flat-contract-predicate v/c) v/c)) (and (hash? h) (for/and ([(k v) h]) - (and (k/c k) (v/c v))))))) + (and (k/c? k) + (v/c? v))))))) (provide/contract (struct c ([S Type?] [X symbol?] [T Type?])) (struct dcon ([fixed (listof c?)] [rest (or/c c? false/c)])) + (struct dcon-exact ([fixed (listof c?)] [rest c?])) (struct dcon-dotted ([type c?] [bound symbol?])) - (struct dmap ([map (hashof symbol? (lambda (e) (or (dcon? e) (dcon-dotted? e))))])) + (struct dmap ([map (hashof symbol? (or/c dcon? dcon-exact? dcon-dotted?))])) (struct cset ([maps (listof (cons/c (hashof symbol? c?) dmap?))]))) \ No newline at end of file diff --git a/collects/typed-scheme/private/constraints.ss b/collects/typed-scheme/private/constraints.ss index a0789ec301..2697109ebe 100644 --- a/collects/typed-scheme/private/constraints.ss +++ b/collects/typed-scheme/private/constraints.ss @@ -28,9 +28,6 @@ (make-cset (list (cons (for/hash ([x X]) (values x (no-constraint x))) (make-dmap (make-immutable-hash null)))))) -#; -(define (lookup cset var) - (hash-ref (cset-map cset) var (no-constraint var))) (define (insert cs var S T) (match cs diff --git a/collects/typed-scheme/private/dmap.ss b/collects/typed-scheme/private/dmap.ss index 9a26803485..ef2112bae1 100644 --- a/collects/typed-scheme/private/dmap.ss +++ b/collects/typed-scheme/private/dmap.ss @@ -9,6 +9,17 @@ ;; dcon-meet : dcon dcon -> dcon (define (dcon-meet dc1 dc2) (match* (dc1 dc2) + [((struct dcon-exact (fixed1 rest1)) (or (struct dcon (fixed2 rest2)) + (struct dcon-exact (fixed2 rest2)))) + (unless (and rest2 (= (length fixed1) (length fixed2))) + (fail! fixed1 fixed2)) + (make-dcon-exact + (for/list ([c1 fixed1] + [c2 fixed2]) + (c-meet c1 c2 (c-X c1))) + (c-meet rest1 rest2 (c-X rest1)))] + [((struct dcon (fixed1 rest1)) (struct dcon-exact (fixed2 rest2))) + (dcon-meet dc2 dc1)] [((struct dcon (fixed1 #f)) (struct dcon (fixed2 #f))) (unless (= (length fixed1) (length fixed2)) (fail! fixed1 fixed2)) diff --git a/collects/typed-scheme/private/infer-unit.ss b/collects/typed-scheme/private/infer-unit.ss index ff3fe1b38e..8e3c591684 100644 --- a/collects/typed-scheme/private/infer-unit.ss +++ b/collects/typed-scheme/private/infer-unit.ss @@ -70,21 +70,23 @@ (lambda () (int-err "No constraint for new var ~a" v)))) #f)))) -(define (move-rest-to-dmap cset dbound) +(define (move-rest-to-dmap cset dbound #:exact [exact? #f]) (mover cset dbound (list dbound) (lambda (cmap) - (make-dcon null - (hash-ref cmap dbound - (lambda () (int-err "No constraint for bound ~a" dbound))))))) + ((if exact? make-dcon-exact make-dcon) + null + (hash-ref cmap dbound + (lambda () (int-err "No constraint for bound ~a" dbound))))))) -(define (move-vars+rest-to-dmap cset dbound vars) +(define (move-vars+rest-to-dmap cset dbound vars #:exact [exact? #f]) (mover cset dbound (list dbound) (lambda (cmap) - (make-dcon (for/list ([v vars]) - (hash-ref cmap v - (lambda () (int-err "No constraint for new var ~a" v)))) - (hash-ref cmap dbound - (lambda () (int-err "No constraint for bound ~a" dbound))))))) + ((if exact? make-dcon-exact make-dcon) + (for/list ([v vars]) + (hash-ref cmap v + (lambda () (int-err "No constraint for new var ~a" v)))) + (hash-ref cmap dbound + (lambda () (int-err "No constraint for bound ~a" dbound))))))) ;; ss and ts have the same length @@ -208,6 +210,28 @@ (make-arr (append ss new-tys) s #f (cons s-dty dbound) s-thn-eff s-els-eff))]) (move-vars+rest-to-dmap new-cset dbound vars)))] ;; If dotted <: starred is correct, add it below. Not sure it is. + [((arr: ts t #f (cons t-dty dbound) t-thn-eff t-els-eff) + (arr: ss s s-rest #f s-thn-eff s-els-eff)) + (unless (memq dbound X) + (fail! S T)) + (if (< (length ts) (length ss)) + ;; the hard case + (let* ([num-vars (- (length ss) (length ts))] + [vars (for/list ([n (in-range num-vars)]) + (gensym dbound))] + [new-tys (for/list ([var vars]) + (substitute (make-F var) dbound t-dty))] + [new-cset (cgen/arr V (append vars X) + (make-arr (append ts new-tys) t #f (cons t-dty dbound) t-thn-eff t-els-eff) + s-arr)]) + (move-vars+rest-to-dmap new-cset dbound vars #:exact #t)) + ;; the simple case + (let* ([arg-mapping (cgen/list X V (extend ts ss s-rest) ts)] + [darg-mapping (move-rest-to-dmap (cgen (cons dbound V) X s-rest t-dty) dbound #:exact #t)] + [ret-mapping (cg t s)]) + (cset-meet* (list arg-mapping darg-mapping ret-mapping + (cgen/eff/list V X t-thn-eff s-thn-eff) + (cgen/eff/list V X t-els-eff s-els-eff)))))] [(_ _) (fail! S T)])) (define (cgen V X S T) @@ -318,7 +342,12 @@ ;; or, nothing worked, and we fail [else (fail! S T)])])))) -(define (subst-gen C R) +(define (check-vars must-vars subst) + (and (for/and ([v must-vars]) + (assq v subst)) + subst)) + +(define (subst-gen C R must-vars) (define (constraint->type v #:variable [variable #f]) (match v [(struct c (S X T)) @@ -331,16 +360,23 @@ [Invariant S]))])) (match (car (cset-maps C)) [(cons cmap (struct dmap (dm))) - (append - (for/list ([(k dc) dm]) - (match dc - [(struct dcon (fixed rest)) - (list k - (for/list ([f fixed]) - (constraint->type f #:variable k)) - (and rest (constraint->type rest)))])) - (for/list ([(k v) cmap]) - (list k (constraint->type v))))])) + (check-vars + must-vars + (append + (for/list ([(k dc) dm]) + (match dc + [(struct dcon (fixed rest)) + (list k + (for/list ([f fixed]) + (constraint->type f #:variable k)) + (and rest (constraint->type rest)))] + [(struct dcon-exact (fixed rest)) + (list k + (for/list ([f fixed]) + (constraint->type f #:variable k)) + (constraint->type rest))])) + (for/list ([(k v) cmap]) + (list k (constraint->type v)))))])) (define (cgen/list X V S T) (cset-meet* (for/list ([s S] [t T]) (cgen V X s t)))) @@ -349,26 +385,27 @@ ;; S : actual argument types ;; T : formal argument types ;; R : result type +;; must-vars : variables that must be in the substitution ;; expected : boolean ;; returns a substitution ;; if R is #f, we don't care about the substituion ;; just return a boolean result -(define (infer X S T R [expected #f]) - (with-handlers ([exn:infer? (lambda _ #f)]) +(define (infer X S T R must-vars [expected #f]) + (with-handlers ([exn:infer? (lambda _ #f)]) (let ([cs (cgen/list X null S T)]) (if (not expected) - (subst-gen cs R) + (subst-gen cs R must-vars) (cset-meet cs (cgen null X R expected)))))) ;; like infer, but T-var is the vararg type: -(define (infer/vararg X S T T-var R [expected #f]) +(define (infer/vararg X S T T-var R must-vars [expected #f]) (define new-T (extend S T T-var)) (and ((length S) . >= . (length T)) - (infer X S new-T R expected))) + (infer X S new-T R must-vars expected))) ;; like infer, but dotted-var is the bound on the ... ;; and T-dotted is the repeated type -(define (infer/dots X dotted-var S T T-dotted R [expected #f]) +(define (infer/dots X dotted-var S T T-dotted R must-vars [expected #f]) (with-handlers ([exn:infer? (lambda _ #f)]) (let* ([short-S (take S (length T))] [rest-S (drop S (length T))] @@ -380,7 +417,7 @@ [cs-dotted* (move-vars-to-dmap cs-dotted dotted-var new-vars)] [cs (cset-meet cs-short cs-dotted*)]) (if (not expected) - (subst-gen cs R) + (subst-gen cs R must-vars) (cset-meet cs (cgen null X R expected)))))) (define (infer/simple S T R) diff --git a/collects/typed-scheme/private/tc-app-unit.ss b/collects/typed-scheme/private/tc-app-unit.ss index 3122173d1e..1ae43acd43 100644 --- a/collects/typed-scheme/private/tc-app-unit.ss +++ b/collects/typed-scheme/private/tc-app-unit.ss @@ -6,6 +6,7 @@ "tc-utils.ss" "subtype.ss" "infer.ss" + (only-in "utils.ss" debug) "union.ss" "type-utils.ss" "type-effect-convenience.ss" @@ -216,7 +217,8 @@ (cons (make-Listof (car rests*)) (car doms*)) (car rests*) - (car rngs*))) + (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*) @@ -228,7 +230,8 @@ (cons (make-Listof (car rests*)) (car doms*)) (car rests*) - (car rngs*))) + (car rngs*) + (fv (car rngs*)))) => (lambda (substitution) (ret (subst-all substitution (car rngs*))))] ;; ... function, ... arg [(and (car drests*) @@ -236,7 +239,7 @@ (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*))) + (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*))])))] @@ -269,7 +272,8 @@ (cons (make-Listof (car rests*)) (car doms*)) (car rests*) - (car rngs*))) + (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*) @@ -281,7 +285,8 @@ (cons (make-Listof (car rests*)) (car doms*)) (car rests*) - (car rngs*))) + (car rngs*) + (fv (car rngs*)))) => (lambda (substitution) (ret (subst-all substitution (car rngs*))))] ;; ... function, ... arg, same bound on ... [(and (car drests*) @@ -289,7 +294,7 @@ (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*))) + (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*))))] ;; ... function, ... arg, different bound on ... [(and (car drests*) @@ -301,7 +306,7 @@ (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*)))) + (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*))) (ret (substitute-dotted (cadr (assq drest-bound substitution)) @@ -345,7 +350,8 @@ [_ (tc-error/expr #:return (ret (Un)) "Wrong number of arguments to parameter - expected 0 or 1, got ~a" (length argtypes))])] - [(tc-result: (and t (Function: (list (arr: doms rngs rests (and drests #f) latent-thn-effs latent-els-effs) ..1))) thn-eff els-eff) + [(tc-result: (and t (Function: (list (arr: doms rngs rests (and drests #f) latent-thn-effs latent-els-effs) ..1))) + thn-eff els-eff) (if (= 1 (length doms)) (let-values ([(thn-eff els-eff) (tc-args argtypes arg-thn-effs arg-els-effs (car doms) (car rests) @@ -373,25 +379,27 @@ ;(printf "resolved ftype: ~a : ~a~n" (equal? rft ftype) rft) ;(printf "reresolving: ~a~n" (resolve-tc-result ftype)) ;(printf "argtypes: ~a~ndoms: ~a~n" argtypes doms) - (for-each (lambda (x) (unless (not (Poly? x)) + (for-each (lambda (x) (unless (not (or (PolyDots? x) (Poly? x))) (tc-error "Polymorphic argument ~a to polymorphic function not allowed" x))) argtypes) (let loop ([doms* doms] [rngs* rngs]) (cond [(null? doms*) (match t - [(Poly-names: msg-vars (Function: (list (arr: msg-doms msg-rngs msg-rests msg-drests _ _) ...))) - (tc-error/expr #:return (ret (Un)) - (string-append "Polymorphic function over ~a could not be applied to arguments:~n" - (domain-mismatches t msg-doms msg-rests msg-drests argtypes #f #f)) - (stringify msg-vars))] - [(PolyDots-names: msg-vars (Function: (list (arr: msg-doms msg-rngs msg-rests msg-drests _ _) ...))) - (tc-error/expr #:return (ret (Un)) - (string-append "Polymorphic function over ~a ... could not be applied to arguments:~n" - (domain-mismatches t msg-doms msg-rests msg-drests argtypes #f #f)) - (stringify msg-vars))])] + [(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 _ _) ...)))) + (if (and (andmap null? msg-doms) + (null? argtypes)) + (tc-error/expr #:return (ret (-> (Un))) + "Could not infer types for applying polymorphic function over ~a~n" + (stringify msg-vars)) + (tc-error/expr #:return (ret (->* (list) Univ (Un))) + (string-append + "Polymorphic function over ~a could not be applied to arguments:~n" + (domain-mismatches t msg-doms msg-rests msg-drests argtypes #f #f)) + (stringify msg-vars)))])] [(and (= (length (car doms*)) (length argtypes)) - (infer (fv/list (cons (car rngs*) (car doms*))) argtypes (car doms*) (car rngs*) expected)) + (infer (fv/list (cons (car rngs*) (car doms*))) argtypes (car doms*) (car rngs*) (fv (car rngs*)) expected)) => (lambda (substitution) (or expected (let* ([s (lambda (t) (subst-all substitution t))] @@ -424,7 +432,7 @@ (unless (<= (length dom) (length argtypes)) (tc-error "incorrect number of arguments to function: ~a ~a" dom argtypes)) (let ([substitution - (infer/vararg vars argtypes dom rest rng expected)]) + (infer/vararg vars argtypes dom rest rng (fv rng) expected)]) (cond [(and expected substitution) expected] [substitution @@ -449,7 +457,7 @@ (unless (eq? dbound dotted-var) (int-err "dbound (~a) and dotted-var (~a) not the same" dbound dotted-var)) (let ([substitution - (infer/dots fixed-vars dotted-var argtypes dom dty rng expected)]) + (infer/dots fixed-vars dotted-var argtypes dom dty rng (fv rng) expected)]) (cond [(and expected substitution) expected] [substitution diff --git a/collects/typed-scheme/private/type-utils.ss b/collects/typed-scheme/private/type-utils.ss index 3eab138211..d6e191f1c8 100644 --- a/collects/typed-scheme/private/type-utils.ss +++ b/collects/typed-scheme/private/type-utils.ss @@ -97,7 +97,7 @@ target)) ;; substitute many variables -;; substitution = Listof[List[Name,Type]] +;; substitution = Listof[U List[Name,Type] List[Name,Listof[Type]]] ;; subst-all : substition Type -> Type (define (subst-all s t) (for/fold ([t t]) ([e s])