Unitize some more.
This commit is contained in:
parent
bf61e29fac
commit
49be490b51
|
@ -8,84 +8,10 @@
|
||||||
mzlib/trace
|
mzlib/trace
|
||||||
scheme/list)
|
scheme/list)
|
||||||
|
|
||||||
(import constraints^)
|
(import constraints^ promote-demote^)
|
||||||
(export infer^)
|
(export infer^)
|
||||||
|
|
||||||
(define (V-in? V . ts)
|
|
||||||
(for/or ([e (append* (map fv ts))])
|
|
||||||
(memq e V)))
|
|
||||||
|
|
||||||
(define (var-promote T V)
|
|
||||||
(define (vp t) (var-promote t V))
|
|
||||||
(define (inv t) (if (V-in? V t) Univ t))
|
|
||||||
(type-case vp T
|
|
||||||
[#:F name (if (memq name V) Univ T)]
|
|
||||||
[#:Vector t (make-Vector (inv t))]
|
|
||||||
[#:Box t (make-Box (inv t))]
|
|
||||||
[#:Hashtable k v
|
|
||||||
(if (V-in? V v)
|
|
||||||
Univ
|
|
||||||
(make-Hashtable (vp k) v))]
|
|
||||||
[#:Param in out
|
|
||||||
(make-Param (var-demote in V)
|
|
||||||
(vp out))]
|
|
||||||
[#:arr dom rng rest drest thn els
|
|
||||||
(cond
|
|
||||||
[(apply V-in? V (append thn els))
|
|
||||||
(make-arr null (Un) Univ #f null null)]
|
|
||||||
[(and drest (V-in? V (cdr drest)))
|
|
||||||
(make-arr (for/list ([d dom]) (var-demote d V))
|
|
||||||
(vp rng)
|
|
||||||
(var-demote (car drest) V)
|
|
||||||
#f
|
|
||||||
thn
|
|
||||||
els)]
|
|
||||||
[else
|
|
||||||
(make-arr (for/list ([d dom]) (var-demote d V))
|
|
||||||
(vp rng)
|
|
||||||
(and rest (var-demote rest V))
|
|
||||||
(and drest
|
|
||||||
(cons (var-demote (car drest)
|
|
||||||
(cons (cdr drest) V))
|
|
||||||
(cdr drest)))
|
|
||||||
thn
|
|
||||||
els)])]))
|
|
||||||
|
|
||||||
(define (var-demote T V)
|
|
||||||
(define (vd t) (var-demote t V))
|
|
||||||
(define (inv t) (if (V-in? V t) (Un) t))
|
|
||||||
(type-case vd T
|
|
||||||
[#:F name (if (memq name V) (Un) T)]
|
|
||||||
[#:Vector t (make-Vector (inv t))]
|
|
||||||
[#:Box t (make-Box (inv t))]
|
|
||||||
[#:Hashtable k v
|
|
||||||
(if (V-in? V v)
|
|
||||||
(Un)
|
|
||||||
(make-Hashtable (vd k) v))]
|
|
||||||
[#:Param in out
|
|
||||||
(make-Param (var-promote in V)
|
|
||||||
(vd out))]
|
|
||||||
[#:arr dom rng rest drest thn els
|
|
||||||
(cond
|
|
||||||
[(apply V-in? V (append thn els))
|
|
||||||
(make-arr null (Un) Univ #f null null)]
|
|
||||||
[(and drest (V-in? V (cdr drest)))
|
|
||||||
(make-arr (for/list ([d dom]) (var-promote d V))
|
|
||||||
(vd rng)
|
|
||||||
(var-promote (car drest) V)
|
|
||||||
#f
|
|
||||||
thn
|
|
||||||
els)]
|
|
||||||
[else
|
|
||||||
(make-arr (for/list ([d dom]) (var-promote d V))
|
|
||||||
(vd rng)
|
|
||||||
(and rest (var-promote rest V))
|
|
||||||
(and drest
|
|
||||||
(cons (var-promote (car drest)
|
|
||||||
(cons (cdr drest) V))
|
|
||||||
(cdr drest)))
|
|
||||||
thn
|
|
||||||
els)])]))
|
|
||||||
|
|
||||||
(define (empty-set) '())
|
(define (empty-set) '())
|
||||||
|
|
||||||
|
|
|
@ -1,11 +1,11 @@
|
||||||
#lang scheme/base
|
#lang scheme/base
|
||||||
|
|
||||||
(require "infer-unit.ss" "constraints.ss" "dmap.ss" "signatures.ss"
|
(require "infer-unit.ss" "constraints.ss" "dmap.ss" "signatures.ss"
|
||||||
"restrict.ss"
|
"restrict.ss" "promote-demote.ss"
|
||||||
(only-in scheme/unit provide-signature-elements)
|
(only-in scheme/unit provide-signature-elements)
|
||||||
"unit-utils.ss")
|
"unit-utils.ss")
|
||||||
|
|
||||||
(provide-signature-elements restrict^ infer^)
|
(provide-signature-elements restrict^ infer^)
|
||||||
|
|
||||||
(define-values/link-units/infer
|
(define-values/link-units/infer
|
||||||
infer@ constraints@ dmap@ restrict@)
|
infer@ constraints@ dmap@ restrict@ promote-demote@)
|
88
collects/typed-scheme/private/promote-demote.ss
Normal file
88
collects/typed-scheme/private/promote-demote.ss
Normal file
|
@ -0,0 +1,88 @@
|
||||||
|
#lang scheme/unit
|
||||||
|
|
||||||
|
(require "type-effect-convenience.ss" "type-rep.ss" "effect-rep.ss" "rep-utils.ss"
|
||||||
|
"free-variance.ss" "type-utils.ss" "union.ss" "tc-utils.ss" "type-name-env.ss"
|
||||||
|
"subtype.ss" "remove-intersect.ss" "signatures.ss" "utils.ss"
|
||||||
|
scheme/match
|
||||||
|
mzlib/etc
|
||||||
|
mzlib/trace
|
||||||
|
scheme/list)
|
||||||
|
|
||||||
|
(import)
|
||||||
|
(export promote-demote^)
|
||||||
|
|
||||||
|
(define (V-in? V . ts)
|
||||||
|
(for/or ([e (append* (map fv ts))])
|
||||||
|
(memq e V)))
|
||||||
|
|
||||||
|
(define (var-promote T V)
|
||||||
|
(define (vp t) (var-promote t V))
|
||||||
|
(define (inv t) (if (V-in? V t) Univ t))
|
||||||
|
(type-case vp T
|
||||||
|
[#:F name (if (memq name V) Univ T)]
|
||||||
|
[#:Vector t (make-Vector (inv t))]
|
||||||
|
[#:Box t (make-Box (inv t))]
|
||||||
|
[#:Hashtable k v
|
||||||
|
(if (V-in? V v)
|
||||||
|
Univ
|
||||||
|
(make-Hashtable (vp k) v))]
|
||||||
|
[#:Param in out
|
||||||
|
(make-Param (var-demote in V)
|
||||||
|
(vp out))]
|
||||||
|
[#:arr dom rng rest drest thn els
|
||||||
|
(cond
|
||||||
|
[(apply V-in? V (append thn els))
|
||||||
|
(make-arr null (Un) Univ #f null null)]
|
||||||
|
[(and drest (V-in? V (cdr drest)))
|
||||||
|
(make-arr (for/list ([d dom]) (var-demote d V))
|
||||||
|
(vp rng)
|
||||||
|
(var-demote (car drest) V)
|
||||||
|
#f
|
||||||
|
thn
|
||||||
|
els)]
|
||||||
|
[else
|
||||||
|
(make-arr (for/list ([d dom]) (var-demote d V))
|
||||||
|
(vp rng)
|
||||||
|
(and rest (var-demote rest V))
|
||||||
|
(and drest
|
||||||
|
(cons (var-demote (car drest)
|
||||||
|
(cons (cdr drest) V))
|
||||||
|
(cdr drest)))
|
||||||
|
thn
|
||||||
|
els)])]))
|
||||||
|
|
||||||
|
(define (var-demote T V)
|
||||||
|
(define (vd t) (var-demote t V))
|
||||||
|
(define (inv t) (if (V-in? V t) (Un) t))
|
||||||
|
(type-case vd T
|
||||||
|
[#:F name (if (memq name V) (Un) T)]
|
||||||
|
[#:Vector t (make-Vector (inv t))]
|
||||||
|
[#:Box t (make-Box (inv t))]
|
||||||
|
[#:Hashtable k v
|
||||||
|
(if (V-in? V v)
|
||||||
|
(Un)
|
||||||
|
(make-Hashtable (vd k) v))]
|
||||||
|
[#:Param in out
|
||||||
|
(make-Param (var-promote in V)
|
||||||
|
(vd out))]
|
||||||
|
[#:arr dom rng rest drest thn els
|
||||||
|
(cond
|
||||||
|
[(apply V-in? V (append thn els))
|
||||||
|
(make-arr null (Un) Univ #f null null)]
|
||||||
|
[(and drest (V-in? V (cdr drest)))
|
||||||
|
(make-arr (for/list ([d dom]) (var-promote d V))
|
||||||
|
(vd rng)
|
||||||
|
(var-promote (car drest) V)
|
||||||
|
#f
|
||||||
|
thn
|
||||||
|
els)]
|
||||||
|
[else
|
||||||
|
(make-arr (for/list ([d dom]) (var-promote d V))
|
||||||
|
(vd rng)
|
||||||
|
(and rest (var-promote rest V))
|
||||||
|
(and drest
|
||||||
|
(cons (var-promote (car drest)
|
||||||
|
(cons (cdr drest) V))
|
||||||
|
(cdr drest)))
|
||||||
|
thn
|
||||||
|
els)])]))
|
|
@ -2,6 +2,9 @@
|
||||||
(require scheme/unit)
|
(require scheme/unit)
|
||||||
(provide (all-defined-out))
|
(provide (all-defined-out))
|
||||||
|
|
||||||
|
(define-signature promote-demote^
|
||||||
|
(var-promote var-demote))
|
||||||
|
|
||||||
(define-signature constraints^
|
(define-signature constraints^
|
||||||
((struct cset (maps))
|
((struct cset (maps))
|
||||||
exn:infer?
|
exn:infer?
|
||||||
|
|
Loading…
Reference in New Issue
Block a user