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

Refactor free variables.

Browse Source 
- free-idxs no longer holds free de Bruijn indexes
   This information is not needed, and not stored anywhere
 - free-idxs holds free *index* variables, in the sense of the TOPLAS submission
This commit is contained in:
Sam Tobin-Hochstadt 2010-06-01 16:30:41 -04:00
parent 7b2de53733
commit 662f982b72
3 changed files with 52 additions and 63 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
collects/typed-scheme/rep/rep-utils.rkt
View File

@ -248,7 +248,7 @@
(p/c (struct Rep ([seq exact-nonnegative-integer?] (p/c (struct Rep ([seq exact-nonnegative-integer?]
[free-vars (hash/c symbol? variance?)] [free-vars (hash/c symbol? variance?)]
[free-idxs (hash/c exact-nonnegative-integer? variance?)] [free-idxs (hash/c symbol? variance?)]
[stx (or/c #f syntax?)])) [stx (or/c #f syntax?)]))
[replace-syntax (Rep? syntax? . -> . Rep?)]) [replace-syntax (Rep? syntax? . -> . Rep?)])

93
collects/typed-scheme/rep/type-rep.rkt
View File

@ -41,11 +41,12 @@
;; this is ONLY used when a type error ocurrs ;; this is ONLY used when a type error ocurrs
(dt Error () [#:frees #f] [#:fold-rhs #:base]) (dt Error () [#:frees #f] [#:fold-rhs #:base])
;; de Bruijn indexes - should never appear outside of this file
;; bound type variables
;; i is an nat ;; i is an nat
(dt B ([i natural-number/c]) (dt B ([i natural-number/c]) [#:frees #f] [#:fold-rhs #:base])
[#:frees #hasheq() (make-immutable-hasheq (list (cons i Covariant)))]
[#:fold-rhs #:base])
;; free type variables
;; n is a Name ;; n is a Name
(dt F ([n symbol?]) [#:frees (make-immutable-hasheq (list (cons n Covariant))) #hasheq()] [#:fold-rhs #:base]) (dt F ([n symbol?]) [#:frees (make-immutable-hasheq (list (cons n Covariant))) #hasheq()] [#:fold-rhs #:base])
@ -57,8 +58,7 @@
;; stx is the syntax of the pair of parens ;; stx is the syntax of the pair of parens
(dt App ([rator Type/c] [rands (listof Type/c)] [stx (or/c #f syntax?)]) (dt App ([rator Type/c] [rands (listof Type/c)] [stx (or/c #f syntax?)])
[#:intern (list rator rands)] [#:intern (list rator rands)]
[#:frees (combine-frees (map free-vars* (cons rator rands))) [#:frees (λ (f) (combine-frees (map f (cons rator rands))))]
(combine-frees (map free-idxs* (cons rator rands)))]
[#:fold-rhs (*App (type-rec-id rator) [#:fold-rhs (*App (type-rec-id rator)
(map type-rec-id rands) (map type-rec-id rands)
stx)]) stx)])
@ -69,39 +69,44 @@
;; dotted list -- after expansion, becomes normal Pair-based list type ;; dotted list -- after expansion, becomes normal Pair-based list type
(dt ListDots ([dty Type/c] [dbound (or/c symbol? natural-number/c)]) (dt ListDots ([dty Type/c] [dbound (or/c symbol? natural-number/c)])
[#:frees (if (symbol? dbound) [#:frees (if (symbol? dbound)
(fix-bound (free-vars* dty) dbound) (hash-remove (free-vars* dty) dbound)
(free-vars* dty)) (free-vars* dty))
(if (number? dbound) (if (symbol? dbound)
(fix-bound (free-idxs* dty) dbound) (hash-set (free-idxs* dty) dbound Covariant)
(free-idxs* dty))] (free-idxs* dty))]
[#:fold-rhs (*ListDots (type-rec-id dty) dbound)]) [#:fold-rhs (*ListDots (type-rec-id dty) dbound)])
;; *mutable* pairs - distinct from regular pairs ;; *mutable* pairs - distinct from regular pairs
;; left and right are Types ;; left and right are Types
(dt MPair ([left Type/c] [right Type/c]) [#:key 'mpair]) (dt MPair ([left Type/c] [right Type/c])
[#:frees (λ (f) (make-invariant (combine-frees (list (f left) (f right)))))]
[#:key 'mpair])
;; elem is a Type ;; elem is a Type
(dt Vector ([elem Type/c]) (dt Vector ([elem Type/c])
[#:frees (make-invariant (free-vars* elem)) (make-invariant (free-idxs* elem))] [#:frees (λ (f) (make-invariant (f elem)))]
[#:key 'vector]) [#:key 'vector])
;; elems are all Types ;; elems are all Types
(dt HeterogenousVector ([elems (listof Type/c)]) (dt HeterogenousVector ([elems (listof Type/c)])
[#:frees (make-invariant (combine-frees (map free-vars* elems))) (make-invariant (combine-frees (map free-idxs* elems)))] [#:frees (λ (f) (make-invariant (combine-frees (map f elems))))]
[#:key 'vector] [#:key 'vector]
[#:fold-rhs (*HeterogenousVector (map type-rec-id elems))]) [#:fold-rhs (*HeterogenousVector (map type-rec-id elems))])
;; elem is a Type ;; elem is a Type
(dt Box ([elem Type/c]) [#:frees (make-invariant (free-vars* elem)) (make-invariant (free-idxs* elem))] (dt Box ([elem Type/c])
[#:frees (λ (f) (make-invariant (f elem)))]
[#:key 'box]) [#:key 'box])
;; elem is a Type ;; elem is a Type
(dt Channel ([elem Type/c]) [#:frees (make-invariant (free-vars* elem)) (make-invariant (free-idxs* elem))] (dt Channel ([elem Type/c])
[#:frees (λ (f) (make-invariant (f elem)))]
[#:key 'channel]) [#:key 'channel])
;; name is a Symbol (not a Name) ;; name is a Symbol (not a Name)
(dt Base ([name symbol?] [contract syntax?]) [#:frees #f] [#:fold-rhs #:base] [#:intern name] (dt Base ([name symbol?] [contract syntax?])
[#:frees #f] [#:fold-rhs #:base] [#:intern name]
[#:key (case name [#:key (case name
[(Number Integer) 'number] [(Number Integer) 'number]
[(Boolean) 'boolean] [(Boolean) 'boolean]
@ -111,7 +116,7 @@
[else #f])]) [else #f])])
;; body is a Scope ;; body is a Scope
(dt Mu ([body (scope-depth 1)]) #:no-provide [#:frees (free-vars* body) (without-below 1 (free-idxs* body))] (dt Mu ([body (scope-depth 1)]) #:no-provide [#:frees (λ (f) (f body))]
[#:fold-rhs (*Mu (*Scope (type-rec-id (Scope-t body))))] [#:fold-rhs (*Mu (*Scope (type-rec-id (Scope-t body))))]
[#:key (Type-key body)]) [#:key (Type-key body)])
@ -122,7 +127,7 @@
[body (scope-depth n)]) [body (scope-depth n)])
(#:syntax [stx (or/c #f syntax?)]) (#:syntax [stx (or/c #f syntax?)])
[result Poly?])] [result Poly?])]
[#:frees (free-vars* body) (without-below n (free-idxs* body))] [#:frees (λ (f) (f body))]
[#:fold-rhs (let ([body* (remove-scopes n body)]) [#:fold-rhs (let ([body* (remove-scopes n body)])
(*Poly n (add-scopes n (type-rec-id body*))))] (*Poly n (add-scopes n (type-rec-id body*))))]
[#:key (Type-key body)]) [#:key (Type-key body)])
@ -136,7 +141,7 @@
(#:syntax [stx (or/c #f syntax?)]) (#:syntax [stx (or/c #f syntax?)])
[result PolyDots?])] [result PolyDots?])]
[#:key (Type-key body)] [#:key (Type-key body)]
[#:frees (free-vars* body) (without-below n (free-idxs* body))] [#:frees (λ (f) (f body))]
[#:fold-rhs (let ([body* (remove-scopes n body)]) [#:fold-rhs (let ([body* (remove-scopes n body)])
(*PolyDots n (add-scopes n (type-rec-id body*))))]) (*PolyDots n (add-scopes n (type-rec-id body*))))])
@ -163,10 +168,10 @@
(dt ValuesDots ([rs (listof Result?)] [dty Type/c] [dbound (or/c symbol? natural-number/c)]) (dt ValuesDots ([rs (listof Result?)] [dty Type/c] [dbound (or/c symbol? natural-number/c)])
[#:frees (if (symbol? dbound) [#:frees (if (symbol? dbound)
(fix-bound (combine-frees (map free-vars* (cons dty rs))) dbound) (hash-remove (combine-frees (map free-vars* (cons dty rs))) dbound)
(combine-frees (map free-vars* (cons dty rs)))) (combine-frees (map free-vars* (cons dty rs))))
(if (number? dbound) (if (symbol? dbound)
(fix-bound (combine-frees (map free-idxs* (cons dty rs))) dbound) (hash-set (combine-frees (map free-idxs* (cons dty rs))) dbound Covariant)
(combine-frees (map free-idxs* (cons dty rs))))] (combine-frees (map free-idxs* (cons dty rs))))]
[#:fold-rhs (*ValuesDots (map type-rec-id rs) (type-rec-id dty) dbound)]) [#:fold-rhs (*ValuesDots (map type-rec-id rs) (type-rec-id dty) dbound)])
@ -184,10 +189,10 @@
dom)) dom))
(match drest (match drest
[(cons t (? symbol? bnd)) [(cons t (? symbol? bnd))
(list (fix-bound (flip-variances (free-vars* t)) bnd))] (list (hash-remove (flip-variances (free-vars* t)) bnd))]
[(cons t (? number? bnd)) [(cons t _)
(list (flip-variances (free-vars* t)))] (list (flip-variances (free-vars* t)))]
[#f null]) [_ null])
(list (free-vars* rng)))) (list (free-vars* rng))))
(combine-frees (combine-frees
(append (map (compose flip-variances free-idxs*) (append (map (compose flip-variances free-idxs*)
@ -196,10 +201,10 @@
dom)) dom))
(match drest (match drest
[(cons t (? symbol? bnd)) [(cons t (? symbol? bnd))
(list (hash-set (flip-variances (free-idxs* t)) bnd Contravariant))]
[(cons t _)
(list (flip-variances (free-idxs* t)))] (list (flip-variances (free-idxs* t)))]
[(cons t (? number? bnd)) [_ null])
(list (fix-bound (flip-variances (free-idxs* t)) bnd))]
[#f null])
(list (free-idxs* rng))))] (list (free-idxs* rng))))]
[#:fold-rhs (*arr (map type-rec-id dom) [#:fold-rhs (*arr (map type-rec-id dom)
(type-rec-id rng) (type-rec-id rng)
@ -215,8 +220,7 @@
;; arities : Listof[arr] ;; arities : Listof[arr]
(dt Function ([arities (listof arr/c)]) (dt Function ([arities (listof arr/c)])
[#:key 'procedure] [#:key 'procedure]
[#:frees (combine-frees (map free-vars* arities)) [#:frees (λ (f) (combine-frees (map f arities)))]
(combine-frees (map free-idxs* arities))]
[#:fold-rhs (*Function (map type-rec-id arities))]) [#:fold-rhs (*Function (map type-rec-id arities))])
@ -230,8 +234,6 @@
(dt Struct ([name symbol?] (dt Struct ([name symbol?]
[parent (or/c #f Struct? Name?)] [parent (or/c #f Struct? Name?)]
[flds (listof Type/c)] [flds (listof Type/c)]
#;
[flds (listof (cons/c Type/c boolean?))]
[proc (or/c #f Function?)] [proc (or/c #f Function?)]
[poly? (or/c #f (listof symbol?))] [poly? (or/c #f (listof symbol?))]
[pred-id identifier?] [pred-id identifier?]
@ -239,19 +241,12 @@
[acc-ids (listof identifier?)] [acc-ids (listof identifier?)]
[maker-id identifier?]) [maker-id identifier?])
[#:intern (list name parent flds proc)] [#:intern (list name parent flds proc)]
[#:frees (combine-frees (map free-vars* (append (if proc (list proc) null) [#:frees (λ (f) (combine-frees (map f (append (if proc (list proc) null)
(if parent (list parent) null) (if parent (list parent) null)
flds))))]
flds #;(map car flds))))
(combine-frees (map free-idxs* (append (if proc (list proc) null)
(if parent (list parent) null)
flds #;(map car flds))))]
[#:fold-rhs (*Struct name [#:fold-rhs (*Struct name
(and parent (type-rec-id parent)) (and parent (type-rec-id parent))
(map type-rec-id flds) (map type-rec-id flds)
#;
(for/list ([(t m?) (in-pairs (in-list flds))])
(cons (type-rec-id t) m?))
(and proc (type-rec-id proc)) (and proc (type-rec-id proc))
poly? poly?
pred-id pred-id
@ -290,8 +285,7 @@
(and sorted? (type<? last e)) (and sorted? (type<? last e))
e))]) e))])
sorted?))))]) sorted?))))])
[#:frees (combine-frees (map free-vars* elems)) [#:frees (λ (f) (combine-frees (map f elems)))]
(combine-frees (map free-idxs* elems))]
[#:fold-rhs ((get-union-maker) (map type-rec-id elems))] [#:fold-rhs ((get-union-maker) (map type-rec-id elems))]
[#:key (let loop ([res null] [ts elems]) [#:key (let loop ([res null] [ts elems])
(if (null? ts) res (if (null? ts) res
@ -317,8 +311,7 @@
[#:key (Type-key parent)] [#:key (Type-key parent)]
[#:intern (list parent (hash-id pred))] [#:intern (list parent (hash-id pred))]
[#:fold-rhs (*Refinement (type-rec-id parent) pred cert)] [#:fold-rhs (*Refinement (type-rec-id parent) pred cert)]
[#:frees (free-vars* parent) [#:frees (λ (f) (f parent))])
(free-idxs* parent)])
;; t : Type ;; t : Type
@ -330,14 +323,10 @@
(dt Class ([pos-flds (listof Type/c)] (dt Class ([pos-flds (listof Type/c)]
[name-flds (listof (list/c symbol? Type/c boolean?))] [name-flds (listof (list/c symbol? Type/c boolean?))]
[methods (listof (list/c symbol? Function?))]) [methods (listof (list/c symbol? Function?))])
[#:frees (combine-frees [#:frees (λ (f) (combine-frees
(map free-vars* (append pos-flds (map f (append pos-flds
(map cadr name-flds) (map cadr name-flds)
(map cadr methods)))) (map cadr methods)))))]
(combine-frees
(map free-idxs* (append pos-flds
(map cadr name-flds)
(map cadr methods))))]
[#:key 'class] [#:key 'class]
[#:fold-rhs (match (list pos-flds name-flds methods) [#:fold-rhs (match (list pos-flds name-flds methods)
[(list [(list

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

@ -68,9 +68,9 @@
;; implements angle bracket substitution from the formalism ;; implements angle bracket substitution from the formalism
;; substitute-dots : Listof[Type] Option[type] Name Type -> Type ;; substitute-dots : Listof[Type] Option[type] Name Type -> Type
(d/c (substitute-dots images rimage name target) (d/c (substitute-dots images rimage name target)
((listof Type/c) (or/c #f Type/c) symbol? Type? . -> . Type?) ((listof Type/c) (or/c #f (cons/c Type/c symbol?)) symbol? Type? . -> . Type?)
(define (sb t) (substitute-dots images rimage name t)) (define (sb t) (substitute-dots images rimage name t))
(if (hash-ref (free-vars* target) name #f) (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 (type-case (#:Type sb #:Filter (sub-f sb)) target
[#:ListDots dty dbound [#:ListDots dty dbound
(if (eq? name dbound) (if (eq? name dbound)
@ -116,7 +116,7 @@
;; substitute-dotted : Type Name Name Type -> Type ;; substitute-dotted : Type Name Name Type -> Type
(define (substitute-dotted image image-bound name target) (define (substitute-dotted image image-bound name target)
(define (sb t) (substitute-dotted image image-bound name t)) (define (sb t) (substitute-dotted image image-bound name t))
(if (hash-ref (free-vars* target) name #f) (if (hash-ref (free-idxs* target) name #f)
(type-case (#:Type sb #:Filter (sub-f sb)) (type-case (#:Type sb #:Filter (sub-f sb))
target target
[#:ValuesDots types dty dbound [#:ValuesDots types dty dbound
@ -135,7 +135,7 @@
(sb rng) (sb rng)
(and rest (sb rest)) (and rest (sb rest))
(and drest (and drest
(cons (sb (car drest)) (cons (substitute image (cdr drest) (sb (car drest)))
(if (eq? name (cdr drest)) image-bound (cdr drest)))) (if (eq? name (cdr drest)) image-bound (cdr drest))))
(map sb kws))]) (map sb kws))])
target)) target))