Skip to content

Commit 27f1c2b

Browse files
committed
first stab at type checking for borrow: not integrated into trans
1 parent c2fe288 commit 27f1c2b

File tree

7 files changed

+394
-351
lines changed

7 files changed

+394
-351
lines changed

src/rustc/middle/infer.rs

Lines changed: 117 additions & 35 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@ export infer_ctxt;
1515
export new_infer_ctxt;
1616
export mk_subty;
1717
export mk_eqty;
18+
export mk_assignty;
1819
export resolve_type_structure;
1920
export fixup_vars;
2021
export resolve_var;
@@ -76,6 +77,14 @@ fn mk_eqty(cx: infer_ctxt, a: ty::t, b: ty::t) -> ures {
7677
indent {|| cx.commit {|| cx.eq_tys(a, b) } }.to_ures()
7778
}
7879

80+
fn mk_assignty(cx: infer_ctxt, encl_node_id: ast::node_id,
81+
a: ty::t, b: ty::t) -> ures {
82+
#debug["mk_assignty(%s <: %s)", a.to_str(cx), b.to_str(cx)];
83+
indent {|| cx.commit {||
84+
cx.assign_tys(encl_node_id, a, b)
85+
} }.to_ures()
86+
}
87+
7988
fn compare_tys(tcx: ty::ctxt, a: ty::t, b: ty::t) -> ures {
8089
let infcx = new_infer_ctxt(tcx);
8190
mk_eqty(infcx, a, b)
@@ -677,12 +686,67 @@ impl resolve_methods for infer_ctxt {
677686
// Type assignment
678687
//
679688
// True if rvalues of type `a` can be assigned to lvalues of type `b`.
689+
// This may cause borrowing to the region scope for `encl_node_id`.
690+
//
691+
// The strategy here is somewhat non-obvious. The problem is
692+
// that the constraint we wish to contend with is not a subtyping
693+
// constraint. Currently, for variables, we only track what it
694+
// must be a subtype of, not what types it must be assignable to
695+
// (or from). Possibly, we should track that, but I leave that
696+
// refactoring for another day.
697+
//
698+
// Instead, we look at each variable involved and try to extract
699+
// *some* sort of bound. Typically, the type a is the argument
700+
// supplied to a call; it typically has a *lower bound* (which
701+
// comes from having been assigned a value). What we'd actually
702+
// *like* here is an upper-bound, but we generally don't have
703+
// one. The type b is the expected type and it typically has a
704+
// lower-bound too, which is good.
705+
//
706+
// The way we deal with the fact that we often don't have the
707+
// bounds we need is to be a bit careful. We try to get *some*
708+
// bound from each side, preferring the upper from a and the
709+
// lower from b. If we fail to get a bound from both sides, then
710+
// we just fall back to requiring that a <: b.
711+
//
712+
// Assuming we have a bound from both sides, we will then examine
713+
// these bounds and see if they have the form (@MT_a, &rb.MT_b)
714+
// (resp. ~MT_a). If they do not, we fall back to subtyping.
715+
//
716+
// If they *do*, then we know that the two types could never be
717+
// subtypes of one another. We will then construct a type @MT_b and
718+
// ensure that type a is a subtype of that. This allows for the
719+
// possibility of assigning from a type like (say) @[mut T1] to a type
720+
// &[const T2] where T1 <: T2. Basically we would require that @[mut
721+
// T1] <: @[const T2]. Next we require that the region for the
722+
// enclosing scope be a superregion of the region r. These two checks
723+
// together guarantee that the type A would be a subtype of the type B
724+
// if the @ were converted to a region r.
725+
//
726+
// You might wonder why we don't just make the type &e.MT_a where e is
727+
// the enclosing region and check that &e.MT_a <: B. The reason is
728+
// that the type @MT_a is (generally) just a *lower-bound*, so this
729+
// would be imposing @MT_a also as the upper-bound on type A. But
730+
// this upper-bound might be stricter than what is truly needed.
680731

681732
impl assignment for infer_ctxt {
682-
fn assign_tys(a: ty::t, b: ty::t,
683-
encl_blk_id: ast::node_id) -> ures {
733+
fn assign_tys(encl_node_id: ast::node_id,
734+
a: ty::t, b: ty::t) -> ures {
735+
736+
fn select(fst: option<ty::t>, snd: option<ty::t>) -> option<ty::t> {
737+
alt fst {
738+
some(t) { some(t) }
739+
none {
740+
alt snd {
741+
some(t) { some(t) }
742+
none { none }
743+
}
744+
}
745+
}
746+
}
684747

685-
#debug["assign_tys(%s, %s)", a.to_str(self), b.to_str(self)];
748+
#debug["assign_tys(encl_node_id=%?, %s -> %s)",
749+
encl_node_id, a.to_str(self), b.to_str(self)];
686750
let _r = indenter();
687751

688752
alt (ty::get(a).struct, ty::get(b).struct) {
@@ -691,59 +755,77 @@ impl assignment for infer_ctxt {
691755
}
692756

693757
(ty::ty_var(a_id), ty::ty_var(b_id)) {
694-
let {root:_, bounds:a_bounds} = self.get(self.vb, a_id);
695-
let {root:_, bounds:b_bounds} = self.get(self.vb, b_id);
696-
self.assign_vars_or_sub(a, b, a_bounds, b_bounds, encl_blk_id)
758+
let {root:_, bounds: a_bounds} = self.get(self.vb, a_id);
759+
let {root:_, bounds: b_bounds} = self.get(self.vb, b_id);
760+
let a_bnd = select(a_bounds.ub, a_bounds.lb);
761+
let b_bnd = select(b_bounds.lb, b_bounds.ub);
762+
self.assign_tys_or_sub(encl_node_id, a, b, a_bnd, b_bnd)
697763
}
698764

699765
(ty::ty_var(a_id), _) {
700766
let {root:_, bounds:a_bounds} = self.get(self.vb, a_id);
701-
let b_bounds = {lb: some(b), ub: none};
702-
self.assign_vars_or_sub(a, b, a_bounds, b_bounds, encl_blk_id)
767+
let a_bnd = select(a_bounds.ub, a_bounds.lb);
768+
self.assign_tys_or_sub(encl_node_id, a, b, a_bnd, some(b))
703769
}
704770

705771
(_, ty::ty_var(b_id)) {
706-
let a_bounds = {lb: none, ub: some(a)};
707772
let {root:_, bounds: b_bounds} = self.get(self.vb, b_id);
708-
self.assign_vars_or_sub(a, b, a_bounds, b_bounds, encl_blk_id)
773+
let b_bnd = select(b_bounds.lb, b_bounds.ub);
774+
self.assign_tys_or_sub(encl_node_id, a, b, some(a), b_bnd)
709775
}
710776

711-
(ty::ty_box(a_mt), ty::ty_rptr(_, _)) |
712-
(ty::ty_uniq(a_mt), ty::ty_rptr(_, _)) {
713-
let a_r = ty::re_scope(encl_blk_id);
714-
let a_ty = ty::mk_rptr(self.tcx, a_r, a_mt);
715-
self.sub_tys(a_ty, b).to_ures()
716-
}
717-
718-
_ {
719-
self.sub_tys(a, b).to_ures()
777+
(_, _) {
778+
self.assign_tys_or_sub(encl_node_id, a, b, some(a), some(b))
720779
}
721780
}
722781
}
723782

724-
fn assign_tys_or_sub(a: ty::t, b: ty::t,
725-
a_b: ty::t, b_b: ty::t,
726-
encl_blk_id: ast::node_id) -> ures {
727-
self.try {||
728-
self.assign_tys(a_b, b_b, encl_blk_id)
729-
}.chain_err {|_e|
730-
self.sub_tys(a, b)
731-
}
732-
}
783+
fn assign_tys_or_sub(
784+
encl_node_id: ast::node_id,
785+
a: ty::t, b: ty::t,
786+
a_bnd: option<ty::t>, b_bnd: option<ty::t>) -> ures {
733787

734-
fn assign_vars_or_sub(a: ty::t, b: ty::t,
735-
a_bounds: bounds<ty::t>, b_bounds: bounds<ty::t>,
736-
encl_blk_id: ast::node_id) -> ures {
788+
#debug["assign_tys_or_sub(encl_node_id=%?, %s -> %s, %s -> %s)",
789+
encl_node_id, a.to_str(self), b.to_str(self),
790+
a_bnd.to_str(self), b_bnd.to_str(self)];
791+
let _r = indenter();
737792

738-
alt (a_bounds.ub, b_bounds.lb) {
739-
(some(a_ub), some(b_lb)) {
740-
self.assign_tys_or_sub(a, b, a_ub, b_lb, encl_blk_id)
793+
alt (a_bnd, b_bnd) {
794+
(some(a_bnd), some(b_bnd)) {
795+
alt (ty::get(a_bnd).struct, ty::get(b_bnd).struct) {
796+
(ty::ty_box(mt_a), ty::ty_rptr(r_b, mt_b)) {
797+
let nr_b = ty::mk_box(self.tcx, mt_b);
798+
self.crosspolinate(encl_node_id, a, nr_b, r_b)
799+
}
800+
(ty::ty_uniq(mt_a), ty::ty_rptr(r_b, mt_b)) {
801+
let nr_b = ty::mk_uniq(self.tcx, mt_b);
802+
self.crosspolinate(encl_node_id, a, nr_b, r_b)
803+
}
804+
_ {
805+
self.sub_tys(a, b)
806+
}
807+
}
741808
}
742809
_ {
743-
self.sub_tys(a, b).to_ures()
810+
self.sub_tys(a, b)
744811
}
745812
}
746813
}
814+
815+
fn crosspolinate(encl_node_id: ast::node_id,
816+
a: ty::t, nr_b: ty::t, r_b: ty::region) -> ures {
817+
818+
#debug["crosspolinate(encl_node_id=%?, a=%s, nr_b=%s, r_b=%s)",
819+
encl_node_id, a.to_str(self), nr_b.to_str(self),
820+
r_b.to_str(self)];
821+
822+
indent {||
823+
self.sub_tys(a, nr_b).then {||
824+
let r_a = ty::re_scope(encl_node_id);
825+
sub(self).contraregions(r_a, r_b).to_ures()
826+
}
827+
}
828+
}
747829
}
748830

749831
// ______________________________________________________________________

0 commit comments

Comments
 (0)