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

Refactor substitution.

Browse Source 
- new file types/substitute
 - use structs for substitutions

original commit: 44d46e4cd7ecc06a264282b31dd7ba47dee421f1
This commit is contained in:
Sam Tobin-Hochstadt 2010-06-17 17:20:48 -04:00
parent da323feea3
commit 6514ee71e1
9 changed files with 177 additions and 170 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
collects/tests/typed-scheme/unit-tests/subst-tests.rkt
View File

@ -2,7 +2,7 @@
(require "test-utils.ss" (for-syntax scheme/base)
(rep type-rep)
(types utils abbrev)
(types utils abbrev substitute)
rackunit)
(define-syntax-rule (s img var tgt result)

7
collects/typed-scheme/infer/constraints.rkt
View File

@ -62,13 +62,6 @@
(fail! S T))
(make-c S (or var X) T))]))
(define (subst-all/c sub -c)
(match -c
[(struct c (S X T))
(make-c (subst-all sub S)
(F-n (subst-all sub (make-F X)))
(subst-all sub T))]))
(define (cset-meet x y)
(match* (x y)
[((struct cset (maps1)) (struct cset (maps2)))

32
collects/typed-scheme/infer/infer-unit.rkt
View File

@ -5,7 +5,8 @@
(combine-in
(utils tc-utils)
(rep free-variance type-rep filter-rep rep-utils)
(types utils convenience union subtype remove-intersect resolve)
(types utils convenience union subtype remove-intersect resolve
substitute)
(env type-name-env index-env tvar-env))
make-env -> ->* one-of/c)
"constraint-structs.rkt"
@ -509,7 +510,7 @@
(cond
[(not no-entry) no-entry]
[(not entry) (cons v no-entry)]
[(= (length entry) 3) no-entry]
[(or (i-subst? entry) (i-subst/starred? entry) (i-subst/dotted? entry)) no-entry]
[else #f]))))
(and absent-entries
(append
@ -518,7 +519,7 @@
(evcase var
[Constant (int-err "attempted to demote dotted variable")]
[Covariant (int-err "attempted to demote dotted variable")]
[Contravariant (list missing null Univ)]
[Contravariant (i-subst/starred missing null Univ)]
[Invariant (int-err "attempted to demote dotted variable")])))
S)))
(match (car (cset-maps C))
@ -526,24 +527,29 @@
(let ([subst (append
(for/list ([(k dc) (in-hash dm)])
(match dc
[(dcon fixed #f)
(i-subst k
(for/list ([f fixed])
(constraint->type f idx-hash #:variable k)))]
[(dcon fixed rest)
(list k
(for/list ([f fixed])
(constraint->type f idx-hash #:variable k))
(and rest (constraint->type rest idx-hash)))]
(i-subst/starred k
(for/list ([f fixed])
(constraint->type f idx-hash #:variable k))
(constraint->type rest idx-hash))]
[(dcon-exact fixed rest)
(list k
(for/list ([f fixed])
(constraint->type f idx-hash #:variable k))
(constraint->type rest idx-hash))]))
(i-subst/starred
k
(for/list ([f fixed])
(constraint->type f idx-hash #:variable k))
(constraint->type rest idx-hash))]))
(for/list ([(k v) (in-hash cmap)])
(list k (constraint->type v var-hash))))])
(t-subst k (constraint->type v var-hash))))])
;; verify that we got all the important variables
(and (for/and ([v (fv R)])
(let ([entry (assq v subst)])
;; Make sure we got a subst entry for a type var
;; (i.e. just a type to substitute)
(and entry (= (length entry) 2))))
(and entry (t-subst? entry))))
(extend-idxs subst)))]))
;; V : a set of variables not to mention in the constraints

2
collects/typed-scheme/infer/restrict.rkt
View File

@ -2,7 +2,7 @@
(require "../utils/utils.rkt")
(require (rep type-rep)
(types utils union subtype remove-intersect resolve)
(types utils union subtype remove-intersect resolve substitute)
"signatures.rkt"
scheme/match mzlib/trace)

16
collects/typed-scheme/typecheck/tc-app.rkt
View File

@ -13,7 +13,7 @@
;; end fixme
(for-syntax syntax/parse scheme/base (utils tc-utils))
(private type-annotation)
(types utils abbrev union subtype resolve convenience type-table)
(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)
@ -417,16 +417,7 @@
(cons (make-ListDots tail-ty tail-bound) arg-tys)
(cons (make-ListDots (car (car drests*)) (cdr (car drests*))) (car doms*))
(car rngs*)))))
=> (lambda (substitution)
(define drest-bound (cdr (car drests*)))
(let ([dots-subst (assq drest-bound substitution)])
(unless dots-subst
(int-err "expected dotted substitution for ~a" drest-bound))
(do-ret (substitute-dotted (cadr dots-subst)
tail-bound
drest-bound
(subst-all (alist-delete drest-bound substitution eq?)
(car rngs*))))))]
=> (lambda (substitution) (do-ret (subst-all substitution (car rngs*))))]
;; ... function, (List A B C etc) arg
[(and (car drests*)
(not tail-bound)
@ -436,8 +427,7 @@
(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*))))
=> (lambda (substitution)
(define drest-bound (cdr (car drests*)))
=> (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*))])))]

4
collects/typed-scheme/typecheck/tc-structs.rkt
View File

@ -3,7 +3,7 @@
(require "../utils/utils.rkt"
(except-in (rep type-rep free-variance) Dotted)
(private parse-type)
(types convenience utils union resolve abbrev)
(types convenience utils union resolve abbrev substitute)
(env global-env type-env-structs type-name-env tvar-env)
(utils tc-utils)
"def-binding.rkt"
@ -199,7 +199,7 @@
;; wrap everything in the approriate forall
#:wrapper (lambda (t) (make-Poly tvars t))
#:type-wrapper (lambda (t) (make-App t new-tvars #f))
#:pred-wrapper (lambda (t) (subst-all (for/list ([t tvars]) (list t Univ)) t))
#:pred-wrapper (lambda (t) (subst-all (for/list ([t tvars]) (t-subst t Univ)) t))
#:poly? tvars))

145
collects/typed-scheme/types/substitute.rkt Normal file
View File

@ -0,0 +1,145 @@
#lang racket/base
(require "../utils/utils.rkt"
(rep type-rep filter-rep object-rep rep-utils)
(utils tc-utils)
(only-in (rep free-variance) combine-frees)
(env index-env tvar-env)
scheme/match
scheme/contract)
(provide subst-all substitute substitute-dots substitute-dotted subst
(struct-out t-subst) (struct-out i-subst) (struct-out i-subst/starred) (struct-out i-subst/dotted))
(define (subst v t e) (substitute t v e))
(d-s/c substitution ([name symbol?]))
(d-s/c (t-subst substitution) ([type Type/c]))
(d-s/c (i-subst substitution) ([types (listof Type/c)]))
(d-s/c (i-subst/starred substitution) ([types (listof Type/c)] [starred Type/c]))
(d-s/c (i-subst/dotted substitution) ([types (listof Type/c)] [dty Type/c] [dbound symbol?]))
;; substitute : Type Name Type -> Type
(d/c (substitute image name target #:Un [Un (get-union-maker)])
((Type/c symbol? Type?) (#:Un procedure?) . ->* . Type?)
(define (sb t) (substitute image name t))
(if (hash-ref (free-vars* target) name #f)
(type-case (#:Type sb #:Filter (sub-f sb) #:Object (sub-o sb))
target
[#:Union tys (Un (map sb tys))]
[#:F name* (if (eq? name* name) image target)]
[#:arr dom rng rest drest kws
(begin
(when (and (pair? drest)
(eq? name (cdr drest))
(not (bound-tvar? name)))
(int-err "substitute used on ... variable ~a in type ~a" name target))
(make-arr (map sb dom)
(sb rng)
(and rest (sb rest))
(and drest (cons (sb (car drest)) (cdr drest)))
(map sb kws)))]
[#:ValuesDots types dty dbound
(begin
(when (and (eq? name dbound) (not (bound-tvar? name)))
(int-err "substitute used on ... variable ~a in type ~a" name target))
(make-ValuesDots (map sb types) (sb dty) dbound))]
[#:ListDots dty dbound
(begin
(when (and (eq? name dbound) (not (bound-tvar? name)))
(int-err "substitute used on ... variable ~a in type ~a" name target))
(make-ListDots (sb dty) dbound))])
target))
;; implements angle bracket substitution from the formalism
;; substitute-dots : Listof[Type] Option[type] Name Type -> Type
(d/c (substitute-dots images rimage name target)
((listof Type/c) (or/c #f Type/c) symbol? Type? . -> . Type?)
(define (sb t) (substitute-dots images rimage name t))
(if (or (hash-ref (free-idxs* target) name #f) (hash-ref (free-vars* target) name #f))
(type-case (#:Type sb #:Filter (sub-f sb)) target
[#:ListDots dty dbound
(if (eq? name dbound)
;; We need to recur first, just to expand out any dotted usages of this.
(let ([expanded (sb dty)])
(for/fold ([t (make-Value null)])
([img images])
(make-Pair (substitute img name expanded) t)))
(make-ListDots (sb dty) dbound))]
[#:ValuesDots types dty dbound
(if (eq? name dbound)
(make-Values
(append
(map sb types)
;; We need to recur first, just to expand out any dotted usages of this.
(let ([expanded (sb dty)])
(for/list ([img images])
(make-Result
(substitute img name expanded)
(make-FilterSet (make-Top) (make-Top))
(make-Empty))))))
(make-ValuesDots (map sb types) (sb dty) dbound))]
[#:arr dom rng rest drest kws
(if (and (pair? drest)
(eq? name (cdr drest)))
(make-arr (append
(map sb dom)
;; We need to recur first, just to expand out any dotted usages of this.
(let ([expanded (sb (car drest))])
(map (lambda (img) (substitute img name expanded)) images)))
(sb rng)
rimage
#f
(map sb kws))
(make-arr (map sb dom)
(sb rng)
(and rest (sb rest))
(and drest (cons (sb (car drest)) (cdr drest)))
(map sb kws)))])
target))
;; implements curly brace substitution from the formalism
;; 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-idxs* target) name #f)
(type-case (#:Type sb #:Filter (sub-f sb))
target
[#:ValuesDots types dty dbound
(make-ValuesDots (map sb types)
(sb dty)
(if (eq? name dbound) image-bound dbound))]
[#:ListDots dty dbound
(make-ListDots (sb dty)
(if (eq? name dbound) image-bound dbound))]
[#:F name*
(if (eq? name* name)
image
target)]
[#:arr dom rng rest drest kws
(make-arr (map sb dom)
(sb rng)
(and rest (sb rest))
(and drest
(cons (substitute image (cdr drest) (sb (car drest)))
(if (eq? name (cdr drest)) image-bound (cdr drest))))
(map sb kws))])
target))
;; substitute many variables
;; substitution = Listof[U List[Name,Type] List[Name,Listof[Type]]]
;; subst-all : substitution Type -> Type
(d/c (subst-all s t)
((listof substitution?) Type/c . -> . Type/c)
(for/fold ([t t]) ([e s])
(match e
[(t-subst v img)
(substitute img v t)]
[(i-subst v imgs)
(substitute-dots imgs #f v t)]
[(i-subst/starred v imgs rest)
(substitute-dots imgs rest v t)]
[(i-subst/dotted v imgs dty dbound)
(int-err "i-subst/dotted nyi")
#;
(substitute-dotted imgs rest v t)])))

5
collects/typed-scheme/types/subtype.rkt
View File

@ -2,7 +2,7 @@
(require "../utils/utils.rkt"
(rep type-rep filter-rep object-rep rep-utils)
(utils tc-utils)
(types utils comparison resolve abbrev)
(types utils comparison resolve abbrev substitute)
(env type-name-env)
(only-in (infer infer-dummy) unify)
scheme/match unstable/match
@ -305,8 +305,7 @@
(=> unmatch)
(unless (= (length ns) (length ms))
(unmatch))
;(printf "Poly: ~n~a ~n~a~n" b1 (subst-all (map list ms (map make-F ns)) b2))
(subtype* A0 b1 (subst-all (map list ms (map make-F ns)) b2))]
(subtype* A0 b1 (subst-all (map t-subst ms (map make-F ns)) b2))]
[((Refinement: par _ _) t)
(subtype* A0 par t)]
;; use unification to see if we can use the polytype here

134
collects/typed-scheme/types/utils.rkt
View File

@ -4,6 +4,7 @@
(require (rep type-rep filter-rep object-rep rep-utils)
(utils tc-utils)
"substitute.rkt"
(only-in (rep free-variance) combine-frees)
(env index-env tvar-env)
scheme/match
@ -13,12 +14,6 @@
(for-syntax scheme/base syntax/parse))
(provide fv fv/list fi
substitute
substitute-dots
substitute-dotted
subst-all
subst
;ret
instantiate-poly
instantiate-poly-dotted
tc-result?
@ -33,125 +28,6 @@
current-poly-struct)
;; substitute : Type Name Type -> Type
(d/c (substitute image name target #:Un [Un (get-union-maker)])
((Type/c symbol? Type?) (#:Un procedure?) . ->* . Type?)
(define (sb t) (substitute image name t))
(if (hash-ref (free-vars* target) name #f)
(type-case (#:Type sb #:Filter (sub-f sb) #:Object (sub-o sb))
target
[#:Union tys (Un (map sb tys))]
[#:F name* (if (eq? name* name) image target)]
[#:arr dom rng rest drest kws
(begin
(when (and (pair? drest)
(eq? name (cdr drest))
(not (bound-tvar? name)))
(int-err "substitute used on ... variable ~a in type ~a" name target))
(make-arr (map sb dom)
(sb rng)
(and rest (sb rest))
(and drest (cons (sb (car drest)) (cdr drest)))
(map sb kws)))]
[#:ValuesDots types dty dbound
(begin
(when (and (eq? name dbound) (not (bound-tvar? name)))
(int-err "substitute used on ... variable ~a in type ~a" name target))
(make-ValuesDots (map sb types) (sb dty) dbound))]
[#:ListDots dty dbound
(begin
(when (and (eq? name dbound) (not (bound-tvar? name)))
(int-err "substitute used on ... variable ~a in type ~a" name target))
(make-ListDots (sb dty) dbound))])
target))
;; implements angle bracket substitution from the formalism
;; substitute-dots : Listof[Type] Option[type] Name Type -> Type
(d/c (substitute-dots images rimage name target)
((listof Type/c) (or/c #f Type/c) symbol? Type? . -> . Type?)
(define (sb t) (substitute-dots images rimage name t))
(if (or (hash-ref (free-idxs* target) name #f) (hash-ref (free-vars* target) name #f))
(type-case (#:Type sb #:Filter (sub-f sb)) target
[#:ListDots dty dbound
(if (eq? name dbound)
;; We need to recur first, just to expand out any dotted usages of this.
(let ([expanded (sb dty)])
(for/fold ([t (make-Value null)])
([img images])
(make-Pair (substitute img name expanded) t)))
(make-ListDots (sb dty) dbound))]
[#:ValuesDots types dty dbound
(if (eq? name dbound)
(make-Values
(append
(map sb types)
;; We need to recur first, just to expand out any dotted usages of this.
(let ([expanded (sb dty)])
(for/list ([img images])
(make-Result
(substitute img name expanded)
(make-FilterSet (make-Top) (make-Top))
(make-Empty))))))
(make-ValuesDots (map sb types) (sb dty) dbound))]
[#:arr dom rng rest drest kws
(if (and (pair? drest)
(eq? name (cdr drest)))
(make-arr (append
(map sb dom)
;; We need to recur first, just to expand out any dotted usages of this.
(let ([expanded (sb (car drest))])
(map (lambda (img) (substitute img name expanded)) images)))
(sb rng)
rimage
#f
(map sb kws))
(make-arr (map sb dom)
(sb rng)
(and rest (sb rest))
(and drest (cons (sb (car drest)) (cdr drest)))
(map sb kws)))])
target))
;; implements curly brace substitution from the formalism
;; 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-idxs* target) name #f)
(type-case (#:Type sb #:Filter (sub-f sb))
target
[#:ValuesDots types dty dbound
(make-ValuesDots (map sb types)
(sb dty)
(if (eq? name dbound) image-bound dbound))]
[#:ListDots dty dbound
(make-ListDots (sb dty)
(if (eq? name dbound) image-bound dbound))]
[#:F name*
(if (eq? name* name)
image
target)]
[#:arr dom rng rest drest kws
(make-arr (map sb dom)
(sb rng)
(and rest (sb rest))
(and drest
(cons (substitute image (cdr drest) (sb (car drest)))
(if (eq? name (cdr drest)) image-bound (cdr drest))))
(map sb kws))])
target))
;; substitute many variables
;; substitution = Listof[U List[Name,Type] List[Name,Listof[Type]]]
;; subst-all : substitution Type -> Type
(define (subst-all s t)
(for/fold ([t t]) ([e s])
(match e
[(list v (list imgs ...) starred)
(substitute-dots imgs starred v t)]
[(list v img)
(substitute img v t)])))
;; unfold : Type -> Type
;; must be applied to a Mu
(define (unfold t)
@ -164,13 +40,13 @@
[(Poly: ns body)
(unless (= (length types) (length ns))
(int-err "instantiate-poly: wrong number of types: expected ~a, got ~a" (length ns) (length types)))
(subst-all (map list ns types) body)]
(subst-all (map t-subst ns types) body)]
[(PolyDots: (list fixed ... dotted) body)
(unless (>= (length types) (length fixed))
(int-err "instantiate-poly: wrong number of types: expected at least ~a, got ~a" (length fixed) (length types)))
(let* ([fixed-tys (take types (length fixed))]
[rest-tys (drop types (length fixed))]
[body* (subst-all (map list fixed fixed-tys) body)])
[body* (subst-all (map t-subst fixed fixed-tys) body)])
(substitute-dots rest-tys #f dotted body*))]
[_ (int-err "instantiate-poly: requires Poly type, got ~a" t)]))
@ -180,7 +56,7 @@
(unless (= (length fixed) (length types))
(int-err "instantiate-poly-dotted: wrong number of types: expected ~a, got ~a, types were ~a"
(length fixed) (length types) types))
(let ([body* (subst-all (map list fixed types) body)])
(let ([body* (subst-all (map t-subst fixed types) body)])
(substitute-dotted image var dotted body*))]
[_ (int-err "instantiate-poly-dotted: requires PolyDots type, got ~a" t)]))
@ -277,8 +153,6 @@
[(list (tc-result1: t f o) ...)
(ret t f o)]))
(define (subst v t e) (substitute t v e))
;; type comparison