Fix instantiate and abstract to handle bounds properly.
NEW INVARIANT - only use instantiate w/ names
This commit is contained in:
Sam Tobin-Hochstadt
parent
a7c63840e4
commit
017f756c77
|
|
@ -5,7 +5,7 @@
|
||||||
|
|
||||||
(require "unify.ss" "type-comparison.ss" "type-rep.ss" "effect-rep.ss" "subtype.ss"
|
(require "unify.ss" "type-comparison.ss" "type-rep.ss" "effect-rep.ss" "subtype.ss"
|
||||||
"planet-requires.ss" "tc-utils.ss" "union.ss"
|
"planet-requires.ss" "tc-utils.ss" "union.ss"
|
||||||
"resolve-type.ss"
|
"resolve-type.ss" "type-utils.ss"
|
||||||
"type-effect-convenience.ss"
|
"type-effect-convenience.ss"
|
||||||
(lib "trace.ss")
|
(lib "trace.ss")
|
||||||
(lib "plt-match.ss")
|
(lib "plt-match.ss")
|
||||||
|
|
|
||||||
|
|
@ -1,215 +1,215 @@
|
||||||
#lang scheme/base
|
#lang scheme/base
|
||||||
|
|
||||||
(require "planet-requires.ss" "rep-utils.ss" "effect-rep.ss" "tc-utils.ss"
|
(require "planet-requires.ss" "rep-utils.ss" "effect-rep.ss" "tc-utils.ss"
|
||||||
"free-variance.ss"
|
"free-variance.ss"
|
||||||
mzlib/trace scheme/match
|
mzlib/trace scheme/match
|
||||||
(for-syntax scheme/base))
|
(for-syntax scheme/base))
|
||||||
|
|
||||||
(define name-table (make-weak-hasheq))
|
(define name-table (make-weak-hasheq))
|
||||||
|
|
||||||
;; Name = Symbol
|
;; Name = Symbol
|
||||||
|
|
||||||
;; Type is defined in rep-utils.ss
|
;; Type is defined in rep-utils.ss
|
||||||
|
|
||||||
;; t must be a Type
|
;; t must be a Type
|
||||||
(dt Scope (t))
|
(dt Scope (t))
|
||||||
|
|
||||||
;; i is an nat
|
;; i is an nat
|
||||||
(dt B (i)
|
(dt B (i)
|
||||||
[#:frees empty-hash-table (make-immutable-hasheq (list (cons i Covariant)))]
|
[#:frees empty-hash-table (make-immutable-hasheq (list (cons i Covariant)))]
|
||||||
[#:fold-rhs #:base])
|
[#:fold-rhs #:base])
|
||||||
|
|
||||||
;; n is a Name
|
;; n is a Name
|
||||||
(dt F (n) [#:frees (make-immutable-hasheq (list (cons n Covariant))) empty-hash-table] [#:fold-rhs #:base])
|
(dt F (n) [#:frees (make-immutable-hasheq (list (cons n Covariant))) empty-hash-table] [#:fold-rhs #:base])
|
||||||
|
|
||||||
;; id is an Identifier
|
;; id is an Identifier
|
||||||
(dt Name (id) [#:intern (hash-id id)] [#:frees #f] [#:fold-rhs #:base])
|
(dt Name (id) [#:intern (hash-id id)] [#:frees #f] [#:fold-rhs #:base])
|
||||||
|
|
||||||
;; rator is a type
|
;; rator is a type
|
||||||
;; rands is a list of types
|
;; rands is a list of types
|
||||||
;; stx is the syntax of the pair of parens
|
;; stx is the syntax of the pair of parens
|
||||||
(dt App (rator rands stx)
|
(dt App (rator rands stx)
|
||||||
[#:intern (list rator rands)]
|
[#:intern (list rator rands)]
|
||||||
[#:frees (combine-frees (map free-vars* (cons rator rands)))
|
[#:frees (combine-frees (map free-vars* (cons rator rands)))
|
||||||
(combine-frees (map free-idxs* (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)])
|
||||||
|
|
||||||
;; left and right are Types
|
;; left and right are Types
|
||||||
(dt Pair (left right))
|
(dt Pair (left right))
|
||||||
|
|
||||||
;; elem is a Type
|
;; elem is a Type
|
||||||
(dt Vector (elem) [#:frees (make-invariant (free-vars* elem)) (make-invariant (free-idxs* elem))])
|
(dt Vector (elem) [#:frees (make-invariant (free-vars* elem)) (make-invariant (free-idxs* elem))])
|
||||||
|
|
||||||
;; elem is a Type
|
;; elem is a Type
|
||||||
(dt Box (elem) [#:frees (make-invariant (free-vars* elem)) (make-invariant (free-idxs* elem))])
|
(dt Box (elem) [#:frees (make-invariant (free-vars* elem)) (make-invariant (free-idxs* elem))])
|
||||||
|
|
||||||
;; name is a Symbol (not a Name)
|
;; name is a Symbol (not a Name)
|
||||||
(dt Base (name) [#:frees #f] [#:fold-rhs #:base])
|
(dt Base (name) [#:frees #f] [#:fold-rhs #:base])
|
||||||
|
|
||||||
;; body is a Scope
|
;; body is a Scope
|
||||||
(dt Mu (body) #:no-provide [#:frees (free-vars* body) (without-below 1 (free-idxs* body))]
|
(dt Mu (body) #:no-provide [#:frees (free-vars* body) (without-below 1 (free-idxs* body))]
|
||||||
[#:fold-rhs (*Mu (*Scope (type-rec-id (Scope-t body))))])
|
[#:fold-rhs (*Mu (*Scope (type-rec-id (Scope-t body))))])
|
||||||
|
|
||||||
;; n is how many variables are bound here
|
;; n is how many variables are bound here
|
||||||
;; body is a Scope
|
;; body is a Scope
|
||||||
(dt Poly (n body) #:no-provide
|
(dt Poly (n body) #:no-provide
|
||||||
[#:frees (free-vars* body) (without-below n (free-idxs* body))]
|
[#:frees (free-vars* body) (without-below n (free-idxs* 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*))))])
|
||||||
|
|
||||||
;; n is how many variables are bound here
|
;; n is how many variables are bound here
|
||||||
;; there are n-1 'normal' vars and 1 ... var
|
;; there are n-1 'normal' vars and 1 ... var
|
||||||
;; body is a Scope
|
;; body is a Scope
|
||||||
(dt PolyDots (n body) #:no-provide
|
(dt PolyDots (n body) #:no-provide
|
||||||
[#:frees (free-vars* body) (without-below n (free-idxs* body))]
|
[#:frees (free-vars* body) (without-below n (free-idxs* 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*))))])
|
||||||
|
|
||||||
;; pred : identifier
|
;; pred : identifier
|
||||||
;; cert : syntax certifier
|
;; cert : syntax certifier
|
||||||
(dt Opaque (pred cert) [#:intern (hash-id pred)] [#:frees #f] [#:fold-rhs #:base])
|
(dt Opaque (pred cert) [#:intern (hash-id pred)] [#:frees #f] [#:fold-rhs #:base])
|
||||||
|
|
||||||
;; name : symbol
|
;; name : symbol
|
||||||
;; parent : Struct
|
;; parent : Struct
|
||||||
;; flds : Listof[Type]
|
;; flds : Listof[Type]
|
||||||
;; proc : Function Type
|
;; proc : Function Type
|
||||||
;; poly? : is this a polymorphic type?
|
;; poly? : is this a polymorphic type?
|
||||||
;; pred-id : identifier for the predicate of the struct
|
;; pred-id : identifier for the predicate of the struct
|
||||||
;; cert : syntax certifier for pred-id
|
;; cert : syntax certifier for pred-id
|
||||||
(dt Struct (name parent flds proc poly? pred-id cert)
|
(dt Struct (name parent flds proc poly? pred-id cert)
|
||||||
[#:intern (list name parent flds proc)]
|
[#:intern (list name parent flds proc)]
|
||||||
[#:frees (combine-frees (map free-vars* (append (if proc (list proc) null) (if parent (list parent) null) flds)))
|
[#:frees (combine-frees (map free-vars* (append (if proc (list proc) null) (if parent (list parent) null) flds)))
|
||||||
(combine-frees (map free-idxs* (append (if proc (list proc) null) (if parent (list parent) null) flds)))]
|
(combine-frees (map free-idxs* (append (if proc (list proc) null) (if parent (list parent) null) 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)
|
||||||
(and proc (type-rec-id proc))
|
(and proc (type-rec-id proc))
|
||||||
poly?
|
poly?
|
||||||
pred-id
|
pred-id
|
||||||
cert)])
|
cert)])
|
||||||
|
|
||||||
;; dom : Listof[Type]
|
;; dom : Listof[Type]
|
||||||
;; rng : Type
|
;; rng : Type
|
||||||
;; rest : Option[Type]
|
;; rest : Option[Type]
|
||||||
;; drest : Option[Cons[Type,Name or nat]]
|
;; drest : Option[Cons[Type,Name or nat]]
|
||||||
;; rest and drest NOT both true
|
;; rest and drest NOT both true
|
||||||
;; thn-eff : Effect
|
;; thn-eff : Effect
|
||||||
;; els-eff : Effect
|
;; els-eff : Effect
|
||||||
;; arr is NOT a Type
|
;; arr is NOT a Type
|
||||||
(dt arr (dom rng rest drest thn-eff els-eff)
|
(dt arr (dom rng rest drest thn-eff els-eff)
|
||||||
[#:frees (combine-frees (append (map flip-variances (map free-vars* (append (if rest (list rest) null) dom)))
|
[#:frees (combine-frees (append (map flip-variances (map free-vars* (append (if rest (list rest) null) dom)))
|
||||||
(match drest
|
(match drest
|
||||||
[(cons t (? symbol? bnd))
|
[(cons t (? symbol? bnd))
|
||||||
(let ([vs (free-vars* t)])
|
(let ([vs (free-vars* t)])
|
||||||
(flip-variances (fix-bound vs bnd)))]
|
(flip-variances (fix-bound vs bnd)))]
|
||||||
[(cons t bnd) (flip-variances (free-vars* t))]
|
[(cons t bnd) (flip-variances (free-vars* t))]
|
||||||
[_ null])
|
[_ null])
|
||||||
(list (free-vars* rng))
|
(list (free-vars* rng))
|
||||||
(map make-invariant
|
(map make-invariant
|
||||||
(map free-vars* (append thn-eff els-eff)))))
|
(map free-vars* (append thn-eff els-eff)))))
|
||||||
(combine-frees (append (map flip-variances (map free-idxs* (append (if rest (list rest) null) dom)))
|
(combine-frees (append (map flip-variances (map free-idxs* (append (if rest (list rest) null) dom)))
|
||||||
(match drest
|
(match drest
|
||||||
[(cons t (? number? bnd))
|
[(cons t (? number? bnd))
|
||||||
(let ([vs (free-idxs* t)])
|
(let ([vs (free-idxs* t)])
|
||||||
(flip-variances (fix-bound vs bnd)))]
|
(flip-variances (fix-bound vs bnd)))]
|
||||||
[(cons t bnd) (flip-variances (free-idxs* t))]
|
[(cons t bnd) (flip-variances (free-idxs* t))]
|
||||||
[_ null])
|
[_ null])
|
||||||
(list (free-idxs* rng))
|
(list (free-idxs* rng))
|
||||||
(map make-invariant
|
(map make-invariant
|
||||||
(map free-idxs* (append thn-eff els-eff)))))]
|
(map free-idxs* (append thn-eff els-eff)))))]
|
||||||
[#:fold-rhs (*arr (map type-rec-id dom)
|
[#:fold-rhs (*arr (map type-rec-id dom)
|
||||||
(type-rec-id rng)
|
(type-rec-id rng)
|
||||||
(and rest (type-rec-id rest))
|
(and rest (type-rec-id rest))
|
||||||
(and drest (cons (type-rec-id (car drest)) (cdr drest)))
|
(and drest (cons (type-rec-id (car drest)) (cdr drest)))
|
||||||
(map effect-rec-id thn-eff)
|
(map effect-rec-id thn-eff)
|
||||||
(map effect-rec-id els-eff))])
|
(map effect-rec-id els-eff))])
|
||||||
|
|
||||||
;; top-arr is the supertype of all function types
|
;; top-arr is the supertype of all function types
|
||||||
(dt top-arr ()
|
(dt top-arr ()
|
||||||
[#:frees #f] [#:fold-rhs #:base])
|
[#:frees #f] [#:fold-rhs #:base])
|
||||||
|
|
||||||
;; arities : Listof[arr]
|
;; arities : Listof[arr]
|
||||||
(dt Function (arities) [#:frees (combine-frees (map free-vars* arities))
|
(dt Function (arities) [#:frees (combine-frees (map free-vars* arities))
|
||||||
(combine-frees (map free-idxs* arities))]
|
(combine-frees (map free-idxs* arities))]
|
||||||
[#:fold-rhs (*Function (map type-rec-id arities))])
|
[#:fold-rhs (*Function (map type-rec-id arities))])
|
||||||
|
|
||||||
;; v : Scheme Value
|
;; v : Scheme Value
|
||||||
(dt Value (v) [#:frees #f] [#:fold-rhs #:base])
|
(dt Value (v) [#:frees #f] [#:fold-rhs #:base])
|
||||||
|
|
||||||
;; elems : Listof[Type]
|
;; elems : Listof[Type]
|
||||||
(dt Union (elems) [#:frees (combine-frees (map free-vars* elems))
|
(dt Union (elems) [#:frees (combine-frees (map free-vars* elems))
|
||||||
(combine-frees (map free-idxs* elems))]
|
(combine-frees (map free-idxs* elems))]
|
||||||
[#:fold-rhs ((unbox union-maker) (map type-rec-id elems))])
|
[#:fold-rhs ((unbox union-maker) (map type-rec-id elems))])
|
||||||
|
|
||||||
(dt Univ () [#:frees #f] [#:fold-rhs #:base])
|
(dt Univ () [#:frees #f] [#:fold-rhs #:base])
|
||||||
|
|
||||||
;; types : Listof[Type]
|
;; types : Listof[Type]
|
||||||
(dt Values (types) [#:frees (combine-frees (map free-vars* types))
|
(dt Values (types) [#:frees (combine-frees (map free-vars* types))
|
||||||
(combine-frees (map free-idxs* types))]
|
(combine-frees (map free-idxs* types))]
|
||||||
[#:fold-rhs (*Values (map type-rec-id types))])
|
[#:fold-rhs (*Values (map type-rec-id types))])
|
||||||
|
|
||||||
;; in : Type
|
;; in : Type
|
||||||
;; out : Type
|
;; out : Type
|
||||||
(dt Param (in out))
|
(dt Param (in out))
|
||||||
|
|
||||||
;; key : Type
|
;; key : Type
|
||||||
;; value : Type
|
;; value : Type
|
||||||
(dt Hashtable (key value))
|
(dt Hashtable (key value))
|
||||||
|
|
||||||
;; t : Type
|
;; t : Type
|
||||||
(dt Syntax (t))
|
(dt Syntax (t))
|
||||||
|
|
||||||
;; pos-flds : (Listof Type)
|
;; pos-flds : (Listof Type)
|
||||||
;; name-flds : (Listof (Tuple Symbol Type Boolean))
|
;; name-flds : (Listof (Tuple Symbol Type Boolean))
|
||||||
;; methods : (Listof (Tuple Symbol Function))
|
;; methods : (Listof (Tuple Symbol Function))
|
||||||
(dt Class (pos-flds name-flds methods)
|
(dt Class (pos-flds name-flds methods)
|
||||||
[#:frees (combine-frees
|
[#:frees (combine-frees
|
||||||
(map free-vars* (append pos-flds
|
(map free-vars* (append pos-flds
|
||||||
(map cadr name-flds)
|
(map cadr name-flds)
|
||||||
(map cadr methods))))
|
(map cadr methods))))
|
||||||
(combine-frees
|
(combine-frees
|
||||||
(map free-idxs* (append pos-flds
|
(map free-idxs* (append pos-flds
|
||||||
(map cadr name-flds)
|
(map cadr name-flds)
|
||||||
(map cadr methods))))]
|
(map cadr methods))))]
|
||||||
|
|
||||||
[#:fold-rhs (match (list pos-flds name-flds methods)
|
[#:fold-rhs (match (list pos-flds name-flds methods)
|
||||||
[(list
|
[(list
|
||||||
pos-tys
|
pos-tys
|
||||||
(list (list init-names init-tys) ___)
|
(list (list init-names init-tys) ___)
|
||||||
(list (list mname mty) ___))
|
(list (list mname mty) ___))
|
||||||
(*Class
|
(*Class
|
||||||
(map type-rec-id pos-tys)
|
(map type-rec-id pos-tys)
|
||||||
(map list
|
(map list
|
||||||
init-names
|
init-names
|
||||||
(map type-rec-id init-tys))
|
(map type-rec-id init-tys))
|
||||||
(map list mname (map type-rec-id mty)))])])
|
(map list mname (map type-rec-id mty)))])])
|
||||||
|
|
||||||
;; cls : Class
|
;; cls : Class
|
||||||
(dt Instance (cls))
|
(dt Instance (cls))
|
||||||
|
|
||||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||||
|
|
||||||
;; Ugly hack - should use units
|
;; Ugly hack - should use units
|
||||||
|
|
||||||
(define union-maker (box #f))
|
(define union-maker (box #f))
|
||||||
|
|
||||||
(define (set-union-maker! v) (set-box! union-maker v))
|
(define (set-union-maker! v) (set-box! union-maker v))
|
||||||
|
|
||||||
(provide set-union-maker!)
|
(provide set-union-maker!)
|
||||||
|
|
||||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||||
|
|
||||||
;; remove-dups: List[Type] -> List[Type]
|
;; remove-dups: List[Type] -> List[Type]
|
||||||
;; removes duplicate types from a SORTED list
|
;; removes duplicate types from a SORTED list
|
||||||
(define (remove-dups types)
|
(define (remove-dups types)
|
||||||
(cond [(null? types) types]
|
(cond [(null? types) types]
|
||||||
[(null? (cdr types)) types]
|
[(null? (cdr types)) types]
|
||||||
[(type-equal? (car types) (cadr types)) (remove-dups (cdr types))]
|
[(type-equal? (car types) (cadr types)) (remove-dups (cdr types))]
|
||||||
[else (cons (car types) (remove-dups (cdr types)))]))
|
[else (cons (car types) (remove-dups (cdr types)))]))
|
||||||
|
|
||||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||||
|
|
||||||
;; type/effect fold
|
;; type/effect fold
|
||||||
|
|
||||||
|
|
@ -261,258 +261,273 @@
|
||||||
|
|
||||||
(provide type-case effect-case)
|
(provide type-case effect-case)
|
||||||
|
|
||||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||||
|
|
||||||
|
|
||||||
;; sub-eff : (Type -> Type) Eff -> Eff
|
;; sub-eff : (Type -> Type) Eff -> Eff
|
||||||
(define (sub-eff sb eff)
|
(define (sub-eff sb eff)
|
||||||
(effect-case sb eff))
|
(effect-case sb eff))
|
||||||
|
|
||||||
(define (add-scopes n t)
|
(define (add-scopes n t)
|
||||||
(if (zero? n) t
|
(if (zero? n) t
|
||||||
(add-scopes (sub1 n) (*Scope t))))
|
(add-scopes (sub1 n) (*Scope t))))
|
||||||
|
|
||||||
(define (remove-scopes n sc)
|
(define (remove-scopes n sc)
|
||||||
(if (zero? n)
|
(if (zero? n)
|
||||||
sc
|
sc
|
||||||
(match sc
|
(match sc
|
||||||
[(Scope: sc*) (remove-scopes (sub1 n) sc*)]
|
[(Scope: sc*) (remove-scopes (sub1 n) sc*)]
|
||||||
[_ (int-err "Tried to remove too many scopes: ~a" sc)])))
|
[_ (int-err "Tried to remove too many scopes: ~a" sc)])))
|
||||||
|
|
||||||
;; abstract-many : Names Type -> Scope^n
|
;; abstract-many : Names Type -> Scope^n
|
||||||
;; where n is the length of names
|
;; where n is the length of names
|
||||||
(define (abstract-many names ty)
|
(define (abstract-many names ty)
|
||||||
(define (nameTo name count type)
|
(define (nameTo name count type)
|
||||||
(let loop ([outer 0] [ty type])
|
(let loop ([outer 0] [ty type])
|
||||||
(define (sb t) (loop outer t))
|
(define (sb t) (loop outer t))
|
||||||
(type-case
|
(type-case
|
||||||
sb ty
|
sb ty
|
||||||
[#:F name* (if (eq? name name*) (*B (+ count outer)) ty)]
|
[#:F name* (if (eq? name name*) (*B (+ count outer)) ty)]
|
||||||
;; necessary to avoid infinite loops
|
;; necessary to avoid infinite loops
|
||||||
[#:Union elems (*Union (remove-dups (sort (map sb elems) type<?)))]
|
[#:Union elems (*Union (remove-dups (sort (map sb elems) type<?)))]
|
||||||
[#:Mu (Scope: body) (*Mu (*Scope (loop (add1 outer) body)))]
|
;; functions
|
||||||
[#:PolyDots n body*
|
[#:arr dom rng rest drest thn-eff els-eff
|
||||||
(let ([body (remove-scopes n body*)])
|
(*arr (map sb dom)
|
||||||
(*PolyDots n (*Scope (loop (+ n outer) body))))]
|
(sb rng)
|
||||||
[#:Poly n body*
|
(if rest (sb rest) #f)
|
||||||
(let ([body (remove-scopes n body*)])
|
(if drest
|
||||||
(*Poly n (*Scope (loop (+ n outer) body))))])))
|
(cons (sb (car drest))
|
||||||
(let ([n (length names)])
|
(if (eq? (cdr drest) name) (+ count outer) (cdr drest)))
|
||||||
(let loop ([ty ty] [names names] [count (sub1 n)])
|
#f)
|
||||||
(if (zero? count)
|
(map (lambda (e) (sub-eff sb e)) thn-eff)
|
||||||
(add-scopes n (nameTo (car names) 0 ty))
|
(map (lambda (e) (sub-eff sb e)) els-eff))]
|
||||||
(loop (nameTo (car names) count ty)
|
[#:Mu (Scope: body) (*Mu (*Scope (loop (add1 outer) body)))]
|
||||||
(cdr names)
|
[#:PolyDots n body*
|
||||||
(sub1 count))))))
|
(let ([body (remove-scopes n body*)])
|
||||||
|
(*PolyDots n (*Scope (loop (+ n outer) body))))]
|
||||||
|
[#:Poly n body*
|
||||||
|
(let ([body (remove-scopes n body*)])
|
||||||
|
(*Poly n (*Scope (loop (+ n outer) body))))])))
|
||||||
|
(let ([n (length names)])
|
||||||
|
(let loop ([ty ty] [names names] [count (sub1 n)])
|
||||||
|
(if (zero? count)
|
||||||
|
(add-scopes n (nameTo (car names) 0 ty))
|
||||||
|
(loop (nameTo (car names) count ty)
|
||||||
|
(cdr names)
|
||||||
|
(sub1 count))))))
|
||||||
|
|
||||||
;; instantiate-many : List[Type] Scope^n -> Type
|
;; instantiate-many : List[Type] Scope^n -> Type
|
||||||
;; where n is the length of types
|
;; where n is the length of types
|
||||||
(define (instantiate-many images sc)
|
;; all of the types MUST be Fs
|
||||||
(define (replace image count type)
|
(define (instantiate-many images sc)
|
||||||
(let loop ([outer 0] [ty type])
|
(define (replace image count type)
|
||||||
(define (sb t) (loop outer t))
|
(let loop ([outer 0] [ty type])
|
||||||
(type-case
|
(define (sb t) (loop outer t))
|
||||||
sb ty
|
(type-case
|
||||||
[#:B idx (if (= (+ count outer) idx)
|
sb ty
|
||||||
image
|
[#:B idx (if (= (+ count outer) idx)
|
||||||
ty)]
|
image
|
||||||
;; necessary to avoid infinite loops
|
ty)]
|
||||||
[#:Union elems (*Union (remove-dups (sort (map sb elems) type<?)))]
|
;; necessary to avoid infinite loops
|
||||||
[#:Mu (Scope: body) (*Mu (*Scope (loop (add1 outer) body)))]
|
[#:Union elems (*Union (remove-dups (sort (map sb elems) type<?)))]
|
||||||
[#:PolyDots n body*
|
;; functions
|
||||||
(let ([body (remove-scopes n body*)])
|
[#:arr dom rng rest drest thn-eff els-eff
|
||||||
(*PolyDots n (*Scope (loop (+ n outer) body))))]
|
(*arr (map sb dom)
|
||||||
[#:Poly n body*
|
(sb rng)
|
||||||
(let ([body (remove-scopes n body*)])
|
(if rest (sb rest) #f)
|
||||||
(*Poly n (*Scope (loop (+ n outer) body))))])))
|
(if drest
|
||||||
(let ([n (length images)])
|
(cons (sb (car drest))
|
||||||
(let loop ([ty (remove-scopes n sc)] [images images] [count (sub1 n)])
|
(if (= (cdr drest) (+ count outer)) (F-n image) (cdr drest)))
|
||||||
(if (zero? count)
|
#f)
|
||||||
(replace (car images) 0 ty)
|
(map (lambda (e) (sub-eff sb e)) thn-eff)
|
||||||
(loop (replace (car images) count ty)
|
(map (lambda (e) (sub-eff sb e)) els-eff))]
|
||||||
(cdr images)
|
[#:Mu (Scope: body) (*Mu (*Scope (loop (add1 outer) body)))]
|
||||||
(sub1 count))))))
|
[#:PolyDots n body*
|
||||||
|
(let ([body (remove-scopes n body*)])
|
||||||
|
(*PolyDots n (*Scope (loop (+ n outer) body))))]
|
||||||
|
[#:Poly n body*
|
||||||
|
(let ([body (remove-scopes n body*)])
|
||||||
|
(*Poly n (*Scope (loop (+ n outer) body))))])))
|
||||||
|
(let ([n (length images)])
|
||||||
|
(let loop ([ty (remove-scopes n sc)] [images images] [count (sub1 n)])
|
||||||
|
(if (zero? count)
|
||||||
|
(replace (car images) 0 ty)
|
||||||
|
(loop (replace (car images) count ty)
|
||||||
|
(cdr images)
|
||||||
|
(sub1 count))))))
|
||||||
|
|
||||||
(define (abstract name ty)
|
(define (abstract name ty)
|
||||||
(abstract-many (list name) ty))
|
(abstract-many (list name) ty))
|
||||||
|
|
||||||
(define (instantiate type sc)
|
(define (instantiate type sc)
|
||||||
(instantiate-many (list type) sc))
|
(instantiate-many (list type) sc))
|
||||||
|
|
||||||
#;(trace instantiate-many abstract-many)
|
#;(trace instantiate-many abstract-many)
|
||||||
|
|
||||||
;; the 'smart' constructor
|
;; the 'smart' constructor
|
||||||
(define (Mu* name body)
|
(define (Mu* name body)
|
||||||
(let ([v (*Mu (abstract name body))])
|
(let ([v (*Mu (abstract name body))])
|
||||||
(hash-set! name-table v name)
|
(hash-set! name-table v name)
|
||||||
v))
|
v))
|
||||||
|
|
||||||
;; the 'smart' destructor
|
;; the 'smart' destructor
|
||||||
(define (Mu-body* name t)
|
(define (Mu-body* name t)
|
||||||
(match t
|
(match t
|
||||||
[(Mu: scope)
|
[(Mu: scope)
|
||||||
(instantiate (*F name) scope)]))
|
(instantiate (*F name) scope)]))
|
||||||
|
|
||||||
;; the 'smart' constructor
|
;; the 'smart' constructor
|
||||||
(define (Poly* names body)
|
(define (Poly* names body)
|
||||||
(if (null? names) body
|
(if (null? names) body
|
||||||
(let ([v (*Poly (length names) (abstract-many names body))])
|
(let ([v (*Poly (length names) (abstract-many names body))])
|
||||||
(hash-set! name-table v names)
|
(hash-set! name-table v names)
|
||||||
v)))
|
v)))
|
||||||
|
|
||||||
;; the 'smart' destructor
|
;; the 'smart' destructor
|
||||||
(define (Poly-body* names t)
|
(define (Poly-body* names t)
|
||||||
(match t
|
(match t
|
||||||
[(Poly: n scope)
|
[(Poly: n scope)
|
||||||
(unless (= (length names) n)
|
(unless (= (length names) n)
|
||||||
(error "Wrong number of names"))
|
(error "Wrong number of names"))
|
||||||
(instantiate-many (map *F names) scope)]))
|
(instantiate-many (map *F names) scope)]))
|
||||||
|
|
||||||
;; the 'smart' constructor
|
;; the 'smart' constructor
|
||||||
(define (PolyDots* names body)
|
(define (PolyDots* names body)
|
||||||
(if (null? names) body
|
(if (null? names) body
|
||||||
(let ([v (*PolyDots (length names) (abstract-many names body))])
|
(let ([v (*PolyDots (length names) (abstract-many names body))])
|
||||||
(hash-set! name-table v names)
|
(hash-set! name-table v names)
|
||||||
v)))
|
v)))
|
||||||
|
|
||||||
;; the 'smart' destructor
|
;; the 'smart' destructor
|
||||||
(define (PolyDots-body* names t)
|
(define (PolyDots-body* names t)
|
||||||
(match t
|
(match t
|
||||||
[(PolyDots: n scope)
|
[(PolyDots: n scope)
|
||||||
(unless (= (length names) n)
|
(unless (= (length names) n)
|
||||||
(error "Wrong number of names"))
|
(error "Wrong number of names"))
|
||||||
(instantiate-many (map *F names) scope)]))
|
(instantiate-many (map *F names) scope)]))
|
||||||
|
|
||||||
(print-struct #t)
|
(print-struct #t)
|
||||||
|
|
||||||
(define-match-expander Mu-unsafe:
|
(define-match-expander Mu-unsafe:
|
||||||
(lambda (stx)
|
(lambda (stx)
|
||||||
(syntax-case stx ()
|
(syntax-case stx ()
|
||||||
[(_ bp) #'(? Mu? (app (lambda (t) (Scope-t (Mu-body t))) bp))])))
|
[(_ bp) #'(? Mu? (app (lambda (t) (Scope-t (Mu-body t))) bp))])))
|
||||||
|
|
||||||
(define-match-expander Poly-unsafe:
|
(define-match-expander Poly-unsafe:
|
||||||
(lambda (stx)
|
(lambda (stx)
|
||||||
(syntax-case stx ()
|
(syntax-case stx ()
|
||||||
[(_ n bp) #'(? Poly? (app (lambda (t) (list (Poly-n t) (Poly-body t))) (list n bp)))])))
|
[(_ n bp) #'(? Poly? (app (lambda (t) (list (Poly-n t) (Poly-body t))) (list n bp)))])))
|
||||||
|
|
||||||
(define-match-expander PolyDots-unsafe:
|
(define-match-expander PolyDots-unsafe:
|
||||||
(lambda (stx)
|
(lambda (stx)
|
||||||
(syntax-case stx ()
|
(syntax-case stx ()
|
||||||
[(_ n bp) #'(? PolyDots? (app (lambda (t) (list (PolyDots-n t) (PolyDots-body t))) (list n bp)))])))
|
[(_ n bp) #'(? PolyDots? (app (lambda (t) (list (PolyDots-n t) (PolyDots-body t))) (list n bp)))])))
|
||||||
|
|
||||||
(define-match-expander Mu:*
|
(define-match-expander Mu:*
|
||||||
(lambda (stx)
|
(lambda (stx)
|
||||||
(syntax-case stx ()
|
(syntax-case stx ()
|
||||||
[(_ np bp)
|
[(_ np bp)
|
||||||
#'(? Mu?
|
#'(? Mu?
|
||||||
(app (lambda (t) (let ([sym (gensym)])
|
(app (lambda (t) (let ([sym (gensym)])
|
||||||
(list sym (Mu-body* sym t))))
|
(list sym (Mu-body* sym t))))
|
||||||
(list np bp)))])))
|
(list np bp)))])))
|
||||||
|
|
||||||
(define-match-expander Mu-name:
|
(define-match-expander Mu-name:
|
||||||
(lambda (stx)
|
(lambda (stx)
|
||||||
(syntax-case stx ()
|
(syntax-case stx ()
|
||||||
[(_ np bp)
|
[(_ np bp)
|
||||||
#'(? Mu?
|
#'(? Mu?
|
||||||
(app (lambda (t) (let ([sym (hash-ref name-table t (lambda _ (gensym)))])
|
(app (lambda (t) (let ([sym (hash-ref name-table t (lambda _ (gensym)))])
|
||||||
(list sym (Mu-body* sym t))))
|
(list sym (Mu-body* sym t))))
|
||||||
(list np bp)))])))
|
(list np bp)))])))
|
||||||
|
|
||||||
;; This match expander wraps the smart constructor
|
;; This match expander wraps the smart constructor
|
||||||
;; names are generated with gensym
|
;; names are generated with gensym
|
||||||
(define-match-expander Poly:*
|
(define-match-expander Poly:*
|
||||||
(lambda (stx)
|
(lambda (stx)
|
||||||
(syntax-case stx ()
|
(syntax-case stx ()
|
||||||
[(_ nps bp)
|
[(_ nps bp)
|
||||||
#'(? Poly?
|
#'(? Poly?
|
||||||
(app (lambda (t)
|
(app (lambda (t)
|
||||||
(let* ([n (Poly-n t)]
|
(let* ([n (Poly-n t)]
|
||||||
[syms (build-list n (lambda _ (gensym)))])
|
[syms (build-list n (lambda _ (gensym)))])
|
||||||
(list syms (Poly-body* syms t))))
|
(list syms (Poly-body* syms t))))
|
||||||
(list nps bp)))])))
|
(list nps bp)))])))
|
||||||
|
|
||||||
;; This match expander uses the names from the hashtable
|
;; This match expander uses the names from the hashtable
|
||||||
(define-match-expander Poly-names:
|
(define-match-expander Poly-names:
|
||||||
(lambda (stx)
|
(lambda (stx)
|
||||||
(syntax-case stx ()
|
(syntax-case stx ()
|
||||||
[(_ nps bp)
|
[(_ nps bp)
|
||||||
#'(? Poly?
|
#'(? Poly?
|
||||||
(app (lambda (t)
|
(app (lambda (t)
|
||||||
(let* ([n (Poly-n t)]
|
(let* ([n (Poly-n t)]
|
||||||
[syms (hash-ref name-table t)])
|
[syms (hash-ref name-table t)])
|
||||||
(list syms (Poly-body* syms t))))
|
(list syms (Poly-body* syms t))))
|
||||||
(list nps bp)))])))
|
(list nps bp)))])))
|
||||||
|
|
||||||
;; This match expander wraps the smart constructor
|
;; This match expander wraps the smart constructor
|
||||||
;; names are generated with gensym
|
;; names are generated with gensym
|
||||||
(define-match-expander PolyDots:*
|
(define-match-expander PolyDots:*
|
||||||
(lambda (stx)
|
(lambda (stx)
|
||||||
(syntax-case stx ()
|
(syntax-case stx ()
|
||||||
[(_ nps bp)
|
[(_ nps bp)
|
||||||
#'(? PolyDots?
|
#'(? PolyDots?
|
||||||
(app (lambda (t)
|
(app (lambda (t)
|
||||||
(let* ([n (PolyDots-n t)]
|
(let* ([n (PolyDots-n t)]
|
||||||
[syms (build-list n (lambda _ (gensym)))])
|
[syms (build-list n (lambda _ (gensym)))])
|
||||||
(list syms (PolyDots-body* syms t))))
|
(list syms (PolyDots-body* syms t))))
|
||||||
(list nps bp)))])))
|
(list nps bp)))])))
|
||||||
|
|
||||||
;; This match expander uses the names from the hashtable
|
;; This match expander uses the names from the hashtable
|
||||||
(define-match-expander PolyDots-names:
|
(define-match-expander PolyDots-names:
|
||||||
(lambda (stx)
|
(lambda (stx)
|
||||||
(syntax-case stx ()
|
(syntax-case stx ()
|
||||||
[(_ nps bp)
|
[(_ nps bp)
|
||||||
#'(? PolyDots?
|
#'(? PolyDots?
|
||||||
(app (lambda (t)
|
(app (lambda (t)
|
||||||
(let* ([n (PolyDots-n t)]
|
(let* ([n (PolyDots-n t)]
|
||||||
[syms (hash-ref name-table t)])
|
[syms (hash-ref name-table t)])
|
||||||
(list syms (PolyDots-body* syms t))))
|
(list syms (PolyDots-body* syms t))))
|
||||||
(list nps bp)))])))
|
(list nps bp)))])))
|
||||||
|
|
||||||
;; unfold : Type -> Type
|
;; type equality
|
||||||
;; must be applied to a Mu
|
(define type-equal? eq?)
|
||||||
(define (unfold t)
|
|
||||||
(match t
|
|
||||||
[(Mu: sc) (instantiate t sc)]
|
|
||||||
[_ (int-err "unfold: requires Mu type, got ~a" t)]))
|
|
||||||
|
|
||||||
;; type equality
|
;; inequality - good
|
||||||
(define type-equal? eq?)
|
|
||||||
|
|
||||||
;; inequality - good
|
(define (type<? s t)
|
||||||
|
(< (Type-seq s) (Type-seq t)))
|
||||||
|
|
||||||
(define (type<? s t)
|
(define (type-compare s t)
|
||||||
(< (Type-seq s) (Type-seq t)))
|
(cond [(eq? s t) 0]
|
||||||
|
[(type<? s t) 1]
|
||||||
|
[else -1]))
|
||||||
|
|
||||||
(define (type-compare s t)
|
;(trace subst subst-all)
|
||||||
(cond [(eq? s t) 0]
|
|
||||||
[(type<? s t) 1]
|
|
||||||
[else -1]))
|
|
||||||
|
|
||||||
;(trace subst subst-all)
|
(provide
|
||||||
|
Mu-name: Poly-names:
|
||||||
|
PolyDots-names:
|
||||||
|
Type-seq Effect-seq
|
||||||
|
Mu-unsafe: Poly-unsafe:
|
||||||
|
PolyDots-unsafe:
|
||||||
|
Mu? Poly? PolyDots?
|
||||||
|
arr
|
||||||
|
Type? Effect?
|
||||||
|
Poly-n
|
||||||
|
PolyDots-n
|
||||||
|
free-vars*
|
||||||
|
type-equal? type-compare type<?
|
||||||
|
remove-dups
|
||||||
|
(rename-out [Mu:* Mu:]
|
||||||
|
[Poly:* Poly:]
|
||||||
|
[PolyDots:* PolyDots:]
|
||||||
|
[Mu* make-Mu]
|
||||||
|
[Poly* make-Poly]
|
||||||
|
[Mu-body* Mu-body]
|
||||||
|
[Poly-body* Poly-body]
|
||||||
|
[PolyDots-body* PolyDots-body]))
|
||||||
|
|
||||||
(provide
|
;(trace unfold)
|
||||||
unfold
|
|
||||||
Mu-name: Poly-names:
|
|
||||||
PolyDots-names:
|
|
||||||
Type-seq Effect-seq
|
|
||||||
Mu-unsafe: Poly-unsafe:
|
|
||||||
PolyDots-unsafe:
|
|
||||||
Mu? Poly? PolyDots?
|
|
||||||
arr
|
|
||||||
Type? Effect?
|
|
||||||
Poly-n
|
|
||||||
PolyDots-n
|
|
||||||
free-vars*
|
|
||||||
type-equal? type-compare type<?
|
|
||||||
remove-dups
|
|
||||||
(rename-out [Mu:* Mu:]
|
|
||||||
[Poly:* Poly:]
|
|
||||||
[PolyDots:* PolyDots:]
|
|
||||||
[Mu* make-Mu]
|
|
||||||
[Poly* make-Poly]
|
|
||||||
[Mu-body* Mu-body]
|
|
||||||
[Poly-body* Poly-body]
|
|
||||||
[PolyDots-body* PolyDots-body]))
|
|
||||||
|
|
||||||
;(trace unfold)
|
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -17,7 +17,8 @@
|
||||||
tc-result:
|
tc-result:
|
||||||
tc-result-equal?
|
tc-result-equal?
|
||||||
effects-equal?
|
effects-equal?
|
||||||
tc-result-t)
|
tc-result-t
|
||||||
|
unfold)
|
||||||
|
|
||||||
|
|
||||||
;; substitute : Type Name Type -> Type
|
;; substitute : Type Name Type -> Type
|
||||||
|
|
@ -35,7 +36,12 @@
|
||||||
(foldr (lambda (e acc) (substitute (cadr e) (car e) acc)) t s))
|
(foldr (lambda (e acc) (substitute (cadr e) (car e) acc)) t s))
|
||||||
|
|
||||||
|
|
||||||
|
;; unfold : Type -> Type
|
||||||
|
;; must be applied to a Mu
|
||||||
|
(define (unfold t)
|
||||||
|
(match t
|
||||||
|
[(Mu: name b) (substitute t name b)]
|
||||||
|
[_ (int-err "unfold: requires Mu type, got ~a" t)]))
|
||||||
|
|
||||||
(define (instantiate-poly t types)
|
(define (instantiate-poly t types)
|
||||||
(match t
|
(match t
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue
Block a user