suzanne.soy/racket
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

* Added code to check that substitution gets rid of all appropriate

Browse Source 
variables (and fails if not)
 * Added weird dotted as subtype of * case (dcon-exact)
This commit is contained in:
Sam Tobin-Hochstadt 2008-06-20 13:07:08 -04:00
parent 654d7e2f46
commit 6296ffbfcf
6 changed files with 118 additions and 56 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
collects/typed-scheme/private/constraint-structs.ss
View File

@ -11,6 +11,10 @@
;; rest : option[c] ;; rest : option[c]
(define-struct dcon (fixed rest) #:prefab) (define-struct dcon (fixed rest) #:prefab)
;; fixed : Listof[c]
;; rest : c
(define-struct dcon-exact (fixed rest) #:prefab)
;; type : c ;; type : c
;; bound : vars ;; bound : vars
(define-struct dcon-dotted (type bound) #:prefab) (define-struct dcon-dotted (type bound) #:prefab)
@ -26,16 +30,21 @@
;; don't want to rule them out too early ;; don't want to rule them out too early
(define-struct cset (maps) #:prefab) (define-struct cset (maps) #:prefab)
(define (hashof k/c v/c) (define (hashof k/c v/c)
(flat-named-contract (flat-named-contract
(format "#<hashof ~a ~a>" k/c v/c) (format "#<hashof ~a ~a>" k/c v/c)
(lambda (h) (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) (and (hash? h)
(for/and ([(k v) 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?])) (provide/contract (struct c ([S Type?] [X symbol?] [T Type?]))
(struct dcon ([fixed (listof c?)] [rest (or/c c? false/c)])) (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 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?))]))) (struct cset ([maps (listof (cons/c (hashof symbol? c?) dmap?))])))

3
collects/typed-scheme/private/constraints.ss
View File

@ -28,9 +28,6 @@
(make-cset (list (cons (for/hash ([x X]) (values x (no-constraint x))) (make-cset (list (cons (for/hash ([x X]) (values x (no-constraint x)))
(make-dmap (make-immutable-hash null)))))) (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) (define (insert cs var S T)
(match cs (match cs

11
collects/typed-scheme/private/dmap.ss
View File

@ -9,6 +9,17 @@
;; dcon-meet : dcon dcon -> dcon ;; dcon-meet : dcon dcon -> dcon
(define (dcon-meet dc1 dc2) (define (dcon-meet dc1 dc2)
(match* (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))) [((struct dcon (fixed1 #f)) (struct dcon (fixed2 #f)))
(unless (= (length fixed1) (length fixed2)) (unless (= (length fixed1) (length fixed2))
(fail! fixed1 fixed2)) (fail! fixed1 fixed2))

91
collects/typed-scheme/private/infer-unit.ss
View File

@ -70,21 +70,23 @@
(lambda () (int-err "No constraint for new var ~a" v)))) (lambda () (int-err "No constraint for new var ~a" v))))
#f)))) #f))))
(define (move-rest-to-dmap cset dbound) (define (move-rest-to-dmap cset dbound #:exact [exact? #f])
(mover cset dbound (list dbound) (mover cset dbound (list dbound)
(lambda (cmap) (lambda (cmap)
(make-dcon null ((if exact? make-dcon-exact make-dcon)
(hash-ref cmap dbound null
(lambda () (int-err "No constraint for bound ~a" dbound))))))) (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) (mover cset dbound (list dbound)
(lambda (cmap) (lambda (cmap)
(make-dcon (for/list ([v vars]) ((if exact? make-dcon-exact make-dcon)
(hash-ref cmap v (for/list ([v vars])
(lambda () (int-err "No constraint for new var ~a" v)))) (hash-ref cmap v
(hash-ref cmap dbound (lambda () (int-err "No constraint for new var ~a" v))))
(lambda () (int-err "No constraint for bound ~a" dbound))))))) (hash-ref cmap dbound
(lambda () (int-err "No constraint for bound ~a" dbound)))))))
;; ss and ts have the same length ;; 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))]) (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)))] (move-vars+rest-to-dmap new-cset dbound vars)))]
;; If dotted <: starred is correct, add it below. Not sure it is. ;; 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)])) [(_ _) (fail! S T)]))
(define (cgen V X S T) (define (cgen V X S T)
@ -318,7 +342,12 @@
;; or, nothing worked, and we fail ;; or, nothing worked, and we fail
[else (fail! S T)])])))) [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]) (define (constraint->type v #:variable [variable #f])
(match v (match v
[(struct c (S X T)) [(struct c (S X T))
@ -331,16 +360,23 @@
[Invariant S]))])) [Invariant S]))]))
(match (car (cset-maps C)) (match (car (cset-maps C))
[(cons cmap (struct dmap (dm))) [(cons cmap (struct dmap (dm)))
(append (check-vars
(for/list ([(k dc) dm]) must-vars
(match dc (append
[(struct dcon (fixed rest)) (for/list ([(k dc) dm])
(list k (match dc
(for/list ([f fixed]) [(struct dcon (fixed rest))
(constraint->type f #:variable k)) (list k
(and rest (constraint->type rest)))])) (for/list ([f fixed])
(for/list ([(k v) cmap]) (constraint->type f #:variable k))
(list k (constraint->type v))))])) (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) (define (cgen/list X V S T)
(cset-meet* (for/list ([s S] [t T]) (cgen V X s t)))) (cset-meet* (for/list ([s S] [t T]) (cgen V X s t))))
@ -349,26 +385,27 @@
;; S : actual argument types ;; S : actual argument types
;; T : formal argument types ;; T : formal argument types
;; R : result type ;; R : result type
;; must-vars : variables that must be in the substitution
;; expected : boolean ;; expected : boolean
;; returns a substitution ;; returns a substitution
;; if R is #f, we don't care about the substituion ;; if R is #f, we don't care about the substituion
;; just return a boolean result ;; just return a boolean result
(define (infer X S T R [expected #f]) (define (infer X S T R must-vars [expected #f])
(with-handlers ([exn:infer? (lambda _ #f)]) (with-handlers ([exn:infer? (lambda _ #f)])
(let ([cs (cgen/list X null S T)]) (let ([cs (cgen/list X null S T)])
(if (not expected) (if (not expected)
(subst-gen cs R) (subst-gen cs R must-vars)
(cset-meet cs (cgen null X R expected)))))) (cset-meet cs (cgen null X R expected))))))
;; like infer, but T-var is the vararg type: ;; 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)) (define new-T (extend S T T-var))
(and ((length S) . >= . (length T)) (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 ... ;; like infer, but dotted-var is the bound on the ...
;; and T-dotted is the repeated type ;; 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)]) (with-handlers ([exn:infer? (lambda _ #f)])
(let* ([short-S (take S (length T))] (let* ([short-S (take S (length T))]
[rest-S (drop 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-dotted* (move-vars-to-dmap cs-dotted dotted-var new-vars)]
[cs (cset-meet cs-short cs-dotted*)]) [cs (cset-meet cs-short cs-dotted*)])
(if (not expected) (if (not expected)
(subst-gen cs R) (subst-gen cs R must-vars)
(cset-meet cs (cgen null X R expected)))))) (cset-meet cs (cgen null X R expected))))))
(define (infer/simple S T R) (define (infer/simple S T R)

52
collects/typed-scheme/private/tc-app-unit.ss
View File

@ -6,6 +6,7 @@
"tc-utils.ss" "tc-utils.ss"
"subtype.ss" "subtype.ss"
"infer.ss" "infer.ss"
(only-in "utils.ss" debug)
"union.ss" "union.ss"
"type-utils.ss" "type-utils.ss"
"type-effect-convenience.ss" "type-effect-convenience.ss"
@ -216,7 +217,8 @@
(cons (make-Listof (car rests*)) (cons (make-Listof (car rests*))
(car doms*)) (car doms*))
(car rests*) (car rests*)
(car rngs*))) (car rngs*)
(fv (car rngs*))))
=> (lambda (substitution) (ret (subst-all substitution (car rngs*))))] => (lambda (substitution) (ret (subst-all substitution (car rngs*))))]
;; actual work, when we have a * function and ... final arg ;; actual work, when we have a * function and ... final arg
[(and (car rests*) [(and (car rests*)
@ -228,7 +230,8 @@
(cons (make-Listof (car rests*)) (cons (make-Listof (car rests*))
(car doms*)) (car doms*))
(car rests*) (car rests*)
(car rngs*))) (car rngs*)
(fv (car rngs*))))
=> (lambda (substitution) (ret (subst-all substitution (car rngs*))))] => (lambda (substitution) (ret (subst-all substitution (car rngs*))))]
;; ... function, ... arg ;; ... function, ... arg
[(and (car drests*) [(and (car drests*)
@ -236,7 +239,7 @@
(eq? tail-bound (cdr (car drests*))) (eq? tail-bound (cdr (car drests*)))
(= (length (car doms*)) (= (length (car doms*))
(length arg-tys)) (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*))))] => (lambda (substitution) (ret (subst-all substitution (car rngs*))))]
;; if nothing matches, around the loop again ;; if nothing matches, around the loop again
[else (loop (cdr doms*) (cdr rngs*) (cdr rests*) (cdr drests*))])))] [else (loop (cdr doms*) (cdr rngs*) (cdr rests*) (cdr drests*))])))]
@ -269,7 +272,8 @@
(cons (make-Listof (car rests*)) (cons (make-Listof (car rests*))
(car doms*)) (car doms*))
(car rests*) (car rests*)
(car rngs*))) (car rngs*)
(fv (car rngs*))))
=> (lambda (substitution) (ret (subst-all substitution (car rngs*))))] => (lambda (substitution) (ret (subst-all substitution (car rngs*))))]
;; actual work, when we have a * function and ... final arg ;; actual work, when we have a * function and ... final arg
[(and (car rests*) [(and (car rests*)
@ -281,7 +285,8 @@
(cons (make-Listof (car rests*)) (cons (make-Listof (car rests*))
(car doms*)) (car doms*))
(car rests*) (car rests*)
(car rngs*))) (car rngs*)
(fv (car rngs*))))
=> (lambda (substitution) (ret (subst-all substitution (car rngs*))))] => (lambda (substitution) (ret (subst-all substitution (car rngs*))))]
;; ... function, ... arg, same bound on ... ;; ... function, ... arg, same bound on ...
[(and (car drests*) [(and (car drests*)
@ -289,7 +294,7 @@
(eq? tail-bound (cdr (car drests*))) (eq? tail-bound (cdr (car drests*)))
(= (length (car doms*)) (= (length (car doms*))
(length arg-tys)) (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*))))] => (lambda (substitution) (ret (subst-all substitution (car rngs*))))]
;; ... function, ... arg, different bound on ... ;; ... function, ... arg, different bound on ...
[(and (car drests*) [(and (car drests*)
@ -301,7 +306,7 @@
(list (make-DottedBoth (make-F tail-bound)) (list (make-DottedBoth (make-F tail-bound))
(make-DottedBoth (make-F (cdr (car drests*))))) (make-DottedBoth (make-F (cdr (car drests*)))))
(current-tvars))]) (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) => (lambda (substitution)
(define drest-bound (cdr (car drests*))) (define drest-bound (cdr (car drests*)))
(ret (substitute-dotted (cadr (assq drest-bound substitution)) (ret (substitute-dotted (cadr (assq drest-bound substitution))
@ -345,7 +350,8 @@
[_ (tc-error/expr #:return (ret (Un)) [_ (tc-error/expr #:return (ret (Un))
"Wrong number of arguments to parameter - expected 0 or 1, got ~a" "Wrong number of arguments to parameter - expected 0 or 1, got ~a"
(length argtypes))])] (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)) (if (= 1 (length doms))
(let-values ([(thn-eff els-eff) (let-values ([(thn-eff els-eff)
(tc-args argtypes arg-thn-effs arg-els-effs (car doms) (car rests) (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 "resolved ftype: ~a : ~a~n" (equal? rft ftype) rft)
;(printf "reresolving: ~a~n" (resolve-tc-result ftype)) ;(printf "reresolving: ~a~n" (resolve-tc-result ftype))
;(printf "argtypes: ~a~ndoms: ~a~n" argtypes doms) ;(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))) (tc-error "Polymorphic argument ~a to polymorphic function not allowed" x)))
argtypes) argtypes)
(let loop ([doms* doms] [rngs* rngs]) (let loop ([doms* doms] [rngs* rngs])
(cond [(null? doms*) (cond [(null? doms*)
(match t (match t
[(Poly-names: msg-vars (Function: (list (arr: msg-doms msg-rngs msg-rests msg-drests _ _) ...))) [(or (Poly-names: msg-vars (Function: (list (arr: msg-doms msg-rngs msg-rests msg-drests _ _) ...)))
(tc-error/expr #:return (ret (Un)) (PolyDots-names: msg-vars (Function: (list (arr: msg-doms msg-rngs msg-rests msg-drests _ _) ...))))
(string-append "Polymorphic function over ~a could not be applied to arguments:~n" (if (and (andmap null? msg-doms)
(domain-mismatches t msg-doms msg-rests msg-drests argtypes #f #f)) (null? argtypes))
(stringify msg-vars))] (tc-error/expr #:return (ret (-> (Un)))
[(PolyDots-names: msg-vars (Function: (list (arr: msg-doms msg-rngs msg-rests msg-drests _ _) ...))) "Could not infer types for applying polymorphic function over ~a~n"
(tc-error/expr #:return (ret (Un)) (stringify msg-vars))
(string-append "Polymorphic function over ~a ... could not be applied to arguments:~n" (tc-error/expr #:return (ret (->* (list) Univ (Un)))
(domain-mismatches t msg-doms msg-rests msg-drests argtypes #f #f)) (string-append
(stringify msg-vars))])] "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*)) [(and (= (length (car doms*))
(length argtypes)) (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) => (lambda (substitution)
(or expected (or expected
(let* ([s (lambda (t) (subst-all substitution t))] (let* ([s (lambda (t) (subst-all substitution t))]
@ -424,7 +432,7 @@
(unless (<= (length dom) (length argtypes)) (unless (<= (length dom) (length argtypes))
(tc-error "incorrect number of arguments to function: ~a ~a" dom argtypes)) (tc-error "incorrect number of arguments to function: ~a ~a" dom argtypes))
(let ([substitution (let ([substitution
(infer/vararg vars argtypes dom rest rng expected)]) (infer/vararg vars argtypes dom rest rng (fv rng) expected)])
(cond (cond
[(and expected substitution) expected] [(and expected substitution) expected]
[substitution [substitution
@ -449,7 +457,7 @@
(unless (eq? dbound dotted-var) (unless (eq? dbound dotted-var)
(int-err "dbound (~a) and dotted-var (~a) not the same" dbound dotted-var)) (int-err "dbound (~a) and dotted-var (~a) not the same" dbound dotted-var))
(let ([substitution (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 (cond
[(and expected substitution) expected] [(and expected substitution) expected]
[substitution [substitution

2
collects/typed-scheme/private/type-utils.ss
View File

@ -97,7 +97,7 @@
target)) target))
;; substitute many variables ;; substitute many variables
;; substitution = Listof[List[Name,Type]] ;; substitution = Listof[U List[Name,Type] List[Name,Listof[Type]]]
;; subst-all : substition Type -> Type ;; subst-all : substition Type -> Type
(define (subst-all s t) (define (subst-all s t)
(for/fold ([t t]) ([e s]) (for/fold ([t t]) ([e s])