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

Sort unions on re-construction to make contract happy.

Browse Source 
Use resolve-once more.
Improve `overlap', in particular use keys.
Resolve names and apps before doing structure comparison.

svn: r14884

original commit: 19c4aa6ba450fdbcaf927fd6391987cc4deca69e
This commit is contained in:
Sam Tobin-Hochstadt 2009-05-20 18:35:59 +00:00
parent fc2b7f344d
commit 1265433a2e
8 changed files with 86 additions and 60 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
collects/typed-scheme/env/init-envs.ss vendored
View File

@ -22,7 +22,7 @@
(define (gen-constructor sym)
(string->symbol (string-append "make-" (substring (symbol->string sym) 7))))
(match v
[(Union: elems) `(make-Union (list ,@(map sub elems)))]
[(Union: elems) `(make-Union (sort (list ,@(map sub elems)) < #:key Type-seq))]
[(Base: n cnt) `(make-Base ',n (quote-syntax ,cnt))]
[(Name: stx) `(make-Name (quote-syntax ,stx))]
[(Struct: name parent flds proc poly? pred-id cert)

13
collects/typed-scheme/infer/infer-unit.ss
View File

@ -2,7 +2,7 @@
(require (except-in "../utils/utils.ss"))
(require (rep free-variance type-rep filter-rep rep-utils)
(types convenience union subtype remove-intersect)
(types convenience union subtype remove-intersect resolve)
(except-in (utils tc-utils) make-env)
(env type-name-env)
(except-in (types utils) Dotted)
@ -347,9 +347,9 @@
(App: (Name: n*) args* _))
(unless (free-identifier=? n n*)
(fail! S T))
(let ([x (instantiate-poly (lookup-type-name n) args)]
[y (instantiate-poly (lookup-type-name n) args*)])
(cg x y))]
(cg (resolve-once S) (resolve-once T))]
[((App: _ _ _) _) (cg (resolve-once S) T)]
[(_ (App: _ _ _)) (cg S (resolve-once T))]
[((Values: ss) (Values: ts))
(unless (= (length ss) (length ts))
(fail! ss ts))
@ -471,7 +471,7 @@
(define (infer X S T R must-vars [expected #f])
(with-handlers ([exn:infer? (lambda _ #f)])
(let ([cs (cgen/list null X S T)])
;(printf "cs: ~a~n" cs)
(printf "cs: ~a~n" cs)
(if (not expected)
(subst-gen cs R must-vars)
(subst-gen (cset-meet cs (cgen null X R expected)) R must-vars)))))
@ -480,6 +480,7 @@
(define (infer/vararg X S T T-var R must-vars [expected #f])
(define new-T (if T-var (extend S T T-var) T))
(and ((length S) . >= . (length T))
(printf "calling infer~n")
(infer X S new-T R must-vars expected)))
;; like infer, but dotted-var is the bound on the ...
@ -506,4 +507,4 @@
(define (i s t r)
(infer/simple (list s) (list t) r))
;(trace cgen cgen/filters cgen/filter)
(trace subst-gen cgen)

1
collects/typed-scheme/infer/infer.ss
View File

@ -3,6 +3,7 @@
(require (except-in "../utils/utils.ss" infer))
(require "infer-unit.ss" "constraints.ss" "dmap.ss" "signatures.ss"
"restrict.ss" "promote-demote.ss"
mzlib/trace
(only-in scheme/unit provide-signature-elements
define-values/invoke-unit/infer link)
(utils unit-utils))

19
collects/typed-scheme/infer/restrict.ss
View File

@ -2,9 +2,9 @@
(require "../utils/utils.ss")
(require (rep type-rep)
(types utils union subtype remove-intersect)
(types utils union subtype remove-intersect resolve)
"signatures.ss"
scheme/match)
scheme/match mzlib/trace)
(import infer^)
(export restrict^)
@ -12,26 +12,27 @@
;; NEW IMPL
;; restrict t1 to be a subtype of t2
(define (restrict t1 t2)
(define (restrict* t1 t2)
;; we don't use union map directly, since that might produce too many elements
(define (union-map f l)
(match l
[(Union: es)
(let ([l (map f es)])
;(printf "l is ~a~n" l)
(printf "l is ~a~n" l)
(apply Un l))]))
(cond
[(subtype t1 t2) t1] ;; already a subtype
[(match t2
[(Poly: vars t)
(let ([subst (infer vars (list t1) (list t) t1 vars)])
(and subst (restrict t1 (subst-all subst t1))))]
(and subst (restrict* t1 (subst-all subst t1))))]
[_ #f])]
[(Union? t1) (union-map (lambda (e) (restrict e t2)) t1)]
[(Mu? t1)
(restrict (unfold t1) t2)]
[(Mu? t2) (restrict t1 (unfold t2))]
[(Union? t1) (union-map (lambda (e) (restrict* e t2)) t1)]
[(needs-resolving? t1) (restrict* (resolve-once t1) t2)]
[(needs-resolving? t2) (restrict* t1 (resolve-once t2))]
[(subtype t2 t1) t2] ;; we don't actually want this - want something that's a part of t1
[(not (overlap t1 t2)) (Un)] ;; there's no overlap, so the restriction is empty
[else t2] ;; t2 and t1 have a complex relationship, so we punt
))
(trace restrict*)
(define restrict restrict*)

2
collects/typed-scheme/rep/type-rep.ss
View File

@ -224,7 +224,7 @@
[else #f])])
;; elems : Listof[Type]
(dt Union ([elems (and/c (listof Type/c)
(dt Union ([elems (and/c (listof Type/c)
(lambda (es)
(let-values ([(sorted? k)
(for/fold ([sorted? #t]

1
collects/typed-scheme/typecheck/tc-app.ss
View File

@ -538,6 +538,7 @@
(PolyDots: vars
(Function: (list (and arrs (arr: doms rngs rests (and drests #f) '())) ...))))))
(list (tc-result1: argtys-t) ...))
(printf "simple poly case: ~a~n" 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)))

89
collects/typed-scheme/types/remove-intersect.ss
View File

@ -1,7 +1,7 @@
#lang scheme/base
(require (except-in "../utils/utils.ss" extend))
(require (rep type-rep)
(require (rep type-rep rep-utils)
(types union subtype resolve convenience utils)
scheme/match mzlib/trace)
@ -9,41 +9,62 @@
(define (overlap t1 t2)
(match (list t1 t2)
[(list (Univ:) _) #t]
[(list _ (Univ:)) #t]
[(list (F: _) _) #t]
[(list _ (F: _)) #t]
[(list (Name: n) (Name: n*)) (free-identifier=? n n*)]
[(list (? Mu?) _) (overlap (unfold t1) t2)]
[(list _ (? Mu?)) (overlap t1 (unfold t2))]
[(list (Union: e) t)
(ormap (lambda (t*) (overlap t* t)) e)]
[(list t (Union: e))
(ormap (lambda (t*) (overlap t t*)) e)]
[(or (list _ (? Poly?)) (list (? Poly?) _))
#t] ;; these can have overlap, conservatively
[(list (Base: s1 _) (Base: s2 _)) (or (subtype t1 t2) (subtype t2 t1))]
[(list (Base: _ _) (Value: _)) (subtype t2 t1)] ;; conservative
[(list (Value: _) (Base: _ _)) (subtype t1 t2)] ;; conservative
[(list (Syntax: t) (Syntax: t*))
(overlap t t*)]
[(or (list (Syntax: _) _)
(list _ (Syntax: _)))
#f]
[(list (Base: _ _) _) #f]
[(list _ (Base: _ _)) #f]
[(list (Value: (? pair? v)) (Pair: _ _)) #t]
[(list (Pair: _ _) (Value: (? pair? v))) #t]
[(list (Pair: a b) (Pair: a* b*))
(and (overlap a a*)
(overlap b b*))]
[(or (list (Pair: _ _) _)
(list _ (Pair: _ _)))
#f]
[else #t]))
(let ([ks (Type-key t1)] [kt (Type-key t2)])
(cond
[(and (symbol? ks) (symbol? kt) (not (eq? ks kt))) #f]
[(and (symbol? ks) (pair? kt) (not (memq ks kt))) #f]
[(and (symbol? kt) (pair? ks) (not (memq kt ks))) #f]
[(and (pair? ks) (pair? kt)
(for/and ([i (in-list ks)]) (not (memq i kt))))
#f]
[else
(match (list t1 t2)
[(list (Univ:) _) #t]
[(list _ (Univ:)) #t]
[(list (F: _) _) #t]
[(list _ (F: _)) #t]
[(list (Name: n) (Name: n*)) (free-identifier=? n n*)]
[(list (? Mu?) _) (overlap (unfold t1) t2)]
[(list _ (? Mu?)) (overlap t1 (unfold t2))]
[(list (Union: e) t)
(ormap (lambda (t*) (overlap t* t)) e)]
[(list t (Union: e))
(ormap (lambda (t*) (overlap t t*)) e)]
[(or (list _ (? Poly?)) (list (? Poly?) _))
#t] ;; these can have overlap, conservatively
[(list (Base: s1 _) (Base: s2 _)) (or (subtype t1 t2) (subtype t2 t1))]
[(list (Base: _ _) (Value: _)) (subtype t2 t1)] ;; conservative
[(list (Value: _) (Base: _ _)) (subtype t1 t2)] ;; conservative
[(list (Syntax: t) (Syntax: t*))
(overlap t t*)]
[(or (list (Syntax: _) _)
(list _ (Syntax: _)))
#f]
[(list (Base: _ _) _) #f]
[(list _ (Base: _ _)) #f]
[(list (Value: (? pair? v)) (Pair: _ _)) #t]
[(list (Pair: _ _) (Value: (? pair? v))) #t]
[(list (Pair: a b) (Pair: a* b*))
(and (overlap a a*)
(overlap b b*))]
[(or (list (Pair: _ _) _)
(list _ (Pair: _ _)))
#f]
[(list (Struct: n _ flds _ _ _ _)
(Struct: n _ flds* _ _ _ _))
(for/and ([f flds] [f* flds*]) (overlap f f*))]
;; n and n* must be different, so there's no overlap
[(list (Struct: n #f flds _ _ _ _)
(Struct: n* #f flds* _ _ _ _))
#f]
[(list (Struct: n p flds _ _ _ _)
(Struct: n* p* flds* _ _ _ _))
(and (= (length flds) (length flds*)) (for/and ([f flds] [f* flds*]) (overlap f f*)))]
[else #t])])))
(trace overlap)
;(trace restrict)

19
collects/typed-scheme/types/subtype.ss
View File

@ -260,15 +260,6 @@
;; for unions, we check the cross-product
[(list (Union: es) t) (and (andmap (lambda (elem) (subtype* A0 elem t)) es) A0)]
[(list s (Union: es)) (and (ormap (lambda (elem) (subtype*/no-fail A0 s elem)) es) A0)]
;; subtyping on immutable structs is covariant
[(list (Struct: nm _ flds #f _ _ _) (Struct: nm _ flds* #f _ _ _))
(subtypes* A0 flds flds*)]
[(list (Struct: nm _ flds proc _ _ _) (Struct: nm _ flds* proc* _ _ _))
(subtypes* A0 (cons proc flds) (cons proc* flds*))]
;; subtyping on structs follows the declared hierarchy
[(list (Struct: nm (? Type? parent) flds proc _ _ _) other)
;(printf "subtype - hierarchy : ~a ~a ~a~n" nm parent other)
(subtype* A0 parent other)]
;; applications and names are structs too
[(list (App: (Name: n) args stx) other)
(let ([t (lookup-type-name n)])
@ -311,6 +302,16 @@
(if (Type? t)
(subtype* A0 other t)
(fail! t s)))]
;; subtyping on immutable structs is covariant
[(list (Struct: nm _ flds #f _ _ _) (Struct: nm _ flds* #f _ _ _))
(printf "subtyping on structs: ~a ~a~n" flds flds*)
(subtypes* A0 flds flds*)]
[(list (Struct: nm _ flds proc _ _ _) (Struct: nm _ flds* proc* _ _ _))
(subtypes* A0 (cons proc flds) (cons proc* flds*))]
;; subtyping on structs follows the declared hierarchy
[(list (Struct: nm (? Type? parent) flds proc _ _ _) other)
;(printf "subtype - hierarchy : ~a ~a ~a~n" nm parent other)
(subtype* A0 parent other)]
;; Promises are covariant
[(list (Struct: 'Promise _ (list t) _ _ _ _) (Struct: 'Promise _ (list t*) _ _ _ _)) (subtype* A0 t t*)]
;; subtyping on values is pointwise