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

* Add constraints when matching t1...a to t2...b

Browse Source 
* Do inference when you have (apply f ... xs), f and xs are dotted,
   and on different bounds.
 * Add fold-right to extra-procs and its type to base-env
This commit is contained in:
Sam Tobin-Hochstadt 2008-06-19 16:55:06 -04:00
parent bb8d8e23d8
commit b9e1676a55
7 changed files with 149 additions and 95 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
collects/typed-scheme/private/base-env.ss
View File

@ -130,6 +130,8 @@
((-lst b) b) . ->... . -Void))]
[fold-left (-polydots (c a b) ((list ((list c a) (b b) . ->... . c) c (-lst a))
((-lst b) b) . ->... . c))]
[fold-right (-polydots (c a b) ((list ((list c a) (b b) . ->... . c) c (-lst a))
((-lst b) b) . ->... . c))]
[foldl
(-poly (a b c)
(cl-> [((a b . -> . b) b (make-lst a)) b]

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

@ -11,7 +11,11 @@
;; rest : option[c]
(define-struct dcon (fixed rest) #:prefab)
;; map : hash mapping variable to dcon
;; type : c
;; bound : vars
(define-struct dcon-dotted (type bound) #:prefab)
;; map : hash mapping variable to dcon or dcon-dotted
(define-struct dmap (map) #:prefab)
;; maps is a list of pairs of
@ -32,5 +36,6 @@
(provide/contract (struct c ([S Type?] [X symbol?] [T Type?]))
(struct dcon ([fixed (listof c?)] [rest (or/c c? false/c)]))
(struct dmap ([map (hashof symbol? dcon?)]))
(struct dcon-dotted ([type c?] [bound symbol?]))
(struct dmap ([map (hashof symbol? (lambda (e) (or (dcon? e) (dcon-dotted? e))))]))
(struct cset ([maps (listof (cons/c (hashof symbol? c?) dmap?))])))

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

@ -37,6 +37,14 @@
[c2 (in-list-forever shorter srest)])
(c-meet c1 c2 (c-X c1)))
(c-meet lrest srest (c-X lrest))))]
[((struct dcon-dotted (c1 bound1)) (struct dcon-dotted (c2 bound2)))
(unless (eq? bound1 bound2)
(fail! bound1 bound2))
(make-dcon-dotted (c-meet c1 c2 bound1) bound1)]
[((struct dcon _) (struct dcon-dotted _))
(fail! dc1 dc2)]
[((struct dcon-dotted _) (struct dcon _))
(fail! dc1 dc2)]
[(_ _) (int-err "Got non-dcons: ~a ~a" dc1 dc2)]))
(define (dmap-meet dm1 dm2)

9
collects/typed-scheme/private/extra-procs.ss
View File

@ -6,5 +6,10 @@
(error "Assertion failed - value was #f"))
v)
(define (fold-right f c as . bss)
(if (or (null? as)
(ormap null? bss))
c
(apply f
(apply fold-right f c (cdr as) (map cdr bss))
(car as) (map car bss))))

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

@ -35,6 +35,10 @@
(if (eq? dbound v)
rest
(hash-ref fixed v (no-constraint v)))]
[(struct dcon-dotted (type bound))
(if (eq? bound v)
type
(no-constraint v))]
[_ (no-constraint v)])))
(define (map/cset f cset)
@ -107,95 +111,106 @@
(define (cgen/arr V X t-arr s-arr)
(define (cg S T) (cgen V X S T))
(match* (t-arr s-arr)
[((arr: ts t #f #f t-thn-eff t-els-eff)
(arr: ss s #f #f s-thn-eff s-els-eff))
(cset-meet*
(list (cgen/list X V ss ts)
(cg t s)
(cgen/eff/list V X t-thn-eff s-thn-eff)
(cgen/eff/list V X t-els-eff s-els-eff)))]
[((arr: ts t t-rest #f t-thn-eff t-els-eff)
(arr: ss s s-rest #f s-thn-eff s-els-eff))
(let ([arg-mapping
(cond [(and t-rest s-rest (<= (length ts) (length ss)))
(cgen/list X V (cons s-rest ss) (cons t-rest (extend ss ts t-rest)))]
[(and t-rest s-rest (>= (length ts) (length ss)))
(cgen/list X V (cons s-rest (extend ts ss s-rest)) (cons t-rest ts))]
[(and t-rest (not s-rest) (<= (length ts) (length ss)))
(cgen/list X V ss (extend ss ts t-rest))]
[(and s-rest (not t-rest) (>= (length ts) (length ss)))
(cgen/list X V (extend ts ss s-rest) ts)]
[else (fail! S T)])]
[ret-mapping (cg t s)])
(cset-meet*
(list arg-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))))]
[((arr: ts t #f (cons dty dbound) t-thn-eff t-els-eff)
(arr: ss s #f #f s-thn-eff s-els-eff))
(unless (memq dbound X)
(fail! S T))
(unless (<= (length ts) (length ss))
(fail! S T))
(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 dty))]
[new-cset (cgen/arr V (append vars X) (make-arr (append ts new-tys) t #f #f t-thn-eff t-els-eff) s-arr)])
(move-vars-to-dmap new-cset dbound vars))]
[((arr: ts t #f #f t-thn-eff t-els-eff)
(arr: ss s #f (cons dty dbound) s-thn-eff s-els-eff))
(unless (memq dbound X)
(fail! S T))
(unless (<= (length ss) (length ts))
(fail! S T))
(let* ([num-vars (- (length ts) (length ss))]
[vars (for/list ([n (in-range num-vars)])
(gensym dbound))]
[new-tys (for/list ([var vars])
(substitute (make-F var) dbound dty))]
[new-cset (cgen/arr V (append vars X) t-arr (make-arr (append ss new-tys) s #f #f s-thn-eff s-els-eff))])
(move-vars-to-dmap new-cset dbound vars))]
[((arr: ts t #f (cons t-dty dbound) t-thn-eff t-els-eff)
(arr: ss s #f (cons s-dty dbound) s-thn-eff s-els-eff))
(unless (= (length ts) (length ss))
(fail! S T))
;; If we want to infer the dotted bound, then why is it in both types?
(when (memq dbound X)
(fail! S T))
(let* ([arg-mapping (cgen/list X V ss ts)]
[darg-mapping (cgen (cons dbound V) X s-dty t-dty)]
[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))))]
[((arr: ts t t-rest #f t-thn-eff t-els-eff)
(arr: ss s #f (cons s-dty dbound) s-thn-eff s-els-eff))
(unless (memq dbound X)
(fail! S T))
(if (<= (length ts) (length ss))
;; the simple case
(let* ([arg-mapping (cgen/list X V ss (extend ss ts t-rest))]
[darg-mapping (move-rest-to-dmap (cgen (cons dbound V) X s-dty t-rest) dbound)]
[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))))
;; the hard case
(let* ([num-vars (- (length ts) (length ss))]
[vars (for/list ([n (in-range num-vars)])
(gensym dbound))]
[new-tys (for/list ([var vars])
(substitute (make-F var) dbound s-dty))]
[new-cset (cgen/arr V (append vars X) t-arr
(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.
[(_ _) (fail! S T)]))
[((arr: ts t #f #f t-thn-eff t-els-eff)
(arr: ss s #f #f s-thn-eff s-els-eff))
(cset-meet*
(list (cgen/list X V ss ts)
(cg t s)
(cgen/eff/list V X t-thn-eff s-thn-eff)
(cgen/eff/list V X t-els-eff s-els-eff)))]
[((arr: ts t t-rest #f t-thn-eff t-els-eff)
(arr: ss s s-rest #f s-thn-eff s-els-eff))
(let ([arg-mapping
(cond [(and t-rest s-rest (<= (length ts) (length ss)))
(cgen/list X V (cons s-rest ss) (cons t-rest (extend ss ts t-rest)))]
[(and t-rest s-rest (>= (length ts) (length ss)))
(cgen/list X V (cons s-rest (extend ts ss s-rest)) (cons t-rest ts))]
[(and t-rest (not s-rest) (<= (length ts) (length ss)))
(cgen/list X V ss (extend ss ts t-rest))]
[(and s-rest (not t-rest) (>= (length ts) (length ss)))
(cgen/list X V (extend ts ss s-rest) ts)]
[else (fail! S T)])]
[ret-mapping (cg t s)])
(cset-meet*
(list arg-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))))]
[((arr: ts t #f (cons dty dbound) t-thn-eff t-els-eff)
(arr: ss s #f #f s-thn-eff s-els-eff))
(unless (memq dbound X)
(fail! S T))
(unless (<= (length ts) (length ss))
(fail! S T))
(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 dty))]
[new-cset (cgen/arr V (append vars X) (make-arr (append ts new-tys) t #f #f t-thn-eff t-els-eff) s-arr)])
(move-vars-to-dmap new-cset dbound vars))]
[((arr: ts t #f #f t-thn-eff t-els-eff)
(arr: ss s #f (cons dty dbound) s-thn-eff s-els-eff))
(unless (memq dbound X)
(fail! S T))
(unless (<= (length ss) (length ts))
(fail! S T))
(let* ([num-vars (- (length ts) (length ss))]
[vars (for/list ([n (in-range num-vars)])
(gensym dbound))]
[new-tys (for/list ([var vars])
(substitute (make-F var) dbound dty))]
[new-cset (cgen/arr V (append vars X) t-arr (make-arr (append ss new-tys) s #f #f s-thn-eff s-els-eff))])
(move-vars-to-dmap new-cset dbound vars))]
[((arr: ts t #f (cons t-dty dbound) t-thn-eff t-els-eff)
(arr: ss s #f (cons s-dty dbound) s-thn-eff s-els-eff))
(unless (= (length ts) (length ss))
(fail! S T))
;; If we want to infer the dotted bound, then why is it in both types?
(when (memq dbound X)
(fail! S T))
(let* ([arg-mapping (cgen/list X V ss ts)]
[darg-mapping (cgen (cons dbound V) X s-dty t-dty)]
[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))))]
[((arr: ts t #f (cons t-dty dbound) t-thn-eff t-els-eff)
(arr: ss s #f (cons s-dty dbound*) s-thn-eff s-els-eff))
(unless (= (length ts) (length ss))
(fail! S T))
(let* ([arg-mapping (cgen/list X V ss ts)]
[darg-mapping (cgen V (cons dbound* X) s-dty t-dty)]
[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))))]
[((arr: ts t t-rest #f t-thn-eff t-els-eff)
(arr: ss s #f (cons s-dty dbound) s-thn-eff s-els-eff))
(unless (memq dbound X)
(fail! S T))
(if (<= (length ts) (length ss))
;; the simple case
(let* ([arg-mapping (cgen/list X V ss (extend ss ts t-rest))]
[darg-mapping (move-rest-to-dmap (cgen (cons dbound V) X s-dty t-rest) dbound)]
[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))))
;; the hard case
(let* ([num-vars (- (length ts) (length ss))]
[vars (for/list ([n (in-range num-vars)])
(gensym dbound))]
[new-tys (for/list ([var vars])
(substitute (make-F var) dbound s-dty))]
[new-cset (cgen/arr V (append vars X) t-arr
(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.
[(_ _) (fail! S T)]))
(define (cgen V X S T)
(define (cgen V X S T)
(define (cg S T) (cgen V X S T))
(define empty (empty-cset X))
(define (singleton S X T)
@ -224,7 +239,6 @@
(fail! S T))
(singleton (var-promote S V) v Univ)]
;; two unions with the same number of elements, so we just try to unify them pairwise
#;[((Union: l1) (Union: l2))
(=> unmatch)

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

@ -13,6 +13,7 @@
"type-annotation.ss"
"resolve-type.ss"
"type-environments.ss"
(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
(for-template
@ -324,7 +325,7 @@
(car rests*)
(car rngs*)))
=> (lambda (substitution) (ret (subst-all substitution (car rngs*))))]
;; ... function, ... arg
;; ... function, ... arg, same bound on ...
[(and (car drests*)
tail-bound
(eq? tail-bound (cdr (car drests*)))
@ -332,6 +333,24 @@
(length arg-tys))
(infer vars (cons tail-ty arg-tys) (cons (car (car drests*)) (car doms*)) (car rngs*)))
=> (lambda (substitution) (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*))))
=> (lambda (substitution)
(define drest-bound (cdr (car drests*)))
(ret (substitute-dotted (cadr (assq drest-bound substitution))
tail-bound
drest-bound
(subst-all (alist-delete drest-bound substitution eq?)
(car rngs*)))))]
;; if nothing matches, around the loop again
[else (loop (cdr doms*) (cdr rngs*) (cdr rests*) (cdr drests*))])))]
[(tc-result: (PolyDots: vars (Function: '())))

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

@ -12,6 +12,7 @@
(provide fv fv/list
substitute
substitute-dots
substitute-dotted
subst-all
subst
ret
@ -76,7 +77,7 @@
target))
;; implements sd from the formalism
;; substitute-dotted : Type Name Type Name -> Type
;; substitute-dotted : Type Name Name Type -> Type
(define (substitute-dotted image image-bound name target)
(define (sb t) (substitute-dotted image image-bound name t))
(if (hash-ref (free-vars* target) name #f)