user0/rust
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Beginnings of support for constrained types

Browse source 
Programs with constrained types now parse and typecheck, but
typestate doesn't check them specially, so the one relevant test
case so far is XFAILed.

Also rewrote all of the constraint-related data structures in the
process (again), for some reason. I got rid of a superfluous
data structure in the context that was mapping front-end constraints
to resolved constraints, instead handling constraints in the same
way in which everything else gets resolved.
This commit is contained in:
Tim Chevalier 2011-07-19 17:52:34 -07:00
parent da2a7e5bd2
commit bd4aeef78b
20 changed files with 606 additions and 366 deletions
Download patch file Download diff file Expand all files Collapse all files

37
src/comp/middle/resolve.rs
View file

@ -1,5 +1,6 @@
import syntax::ast;
import syntax::ast::*;
import ast::ident;
import ast::fn_ident;
import ast::def;
@ -19,6 +20,7 @@ import middle::ty::constr_table;
import syntax::visit;
import visit::vt;
import std::ivec;
import std::int;
import std::map::hashmap;
import std::list;
import std::list::list;
@ -28,6 +30,7 @@ import std::option;
import std::option::some;
import std::option::none;
import std::str;
import syntax::print::pprust::*;
export resolve_crate;
export def_map;
@ -109,7 +112,6 @@ type def_map = hashmap[node_id, def];
type env =
rec(cstore::cstore cstore,
def_map def_map,
constr_table fn_constrs,
ast_map::map ast_map,
hashmap[ast::node_id, import_state] imports,
hashmap[ast::node_id, @indexed_mod] mod_map,
@ -124,12 +126,11 @@ tag dir { inside; outside; }
tag namespace { ns_value; ns_type; ns_module; }
fn resolve_crate(session sess, &ast_map::map amap, @ast::crate crate) ->
tup(def_map, constr_table) {
fn resolve_crate(session sess, &ast_map::map amap, @ast::crate crate)
-> def_map {
auto e =
@rec(cstore=sess.get_cstore(),
def_map=new_int_hash[def](),
fn_constrs = new_int_hash[ty::constr_def[]](),
ast_map=amap,
imports=new_int_hash[import_state](),
mod_map=new_int_hash[@indexed_mod](),
@ -140,7 +141,7 @@ fn resolve_crate(session sess, &ast_map::map amap, @ast::crate crate) ->
resolve_imports(*e);
check_for_collisions(e, *crate);
resolve_names(e, crate);
ret tup(e.def_map, e.fn_constrs);
ret e.def_map;
}
@ -249,7 +250,7 @@ fn resolve_names(&@env e, &@ast::crate c) {
visit_arm=bind walk_arm(e, _, _, _),
visit_expr=bind walk_expr(e, _, _, _),
visit_ty=bind walk_ty(e, _, _, _),
visit_constr=bind walk_constr(e, _, _, _),
visit_constr=bind walk_constr(e, _, _, _, _, _),
visit_fn=bind visit_fn_with_scope(e, _, _, _, _, _, _, _)
with *visit::default_visitor());
visit::visit_crate(*c, cons(scope_crate, @nil), visit::mk_vt(v));
@ -277,10 +278,9 @@ fn resolve_names(&@env e, &@ast::crate c) {
case (_) { }
}
}
fn walk_constr(@env e, &@ast::constr c, &scopes sc, &vt[scopes] v) {
maybe_insert(e, c.node.id,
lookup_path_strict(*e, sc, c.span, c.node.path.node,
ns_value));
fn walk_constr(@env e, &ast::path p, &span sp, node_id id,
&scopes sc, &vt[scopes] v) {
maybe_insert(e, id, lookup_path_strict(*e, sc, sp, p.node, ns_value));
}
fn walk_arm(@env e, &ast::arm a, &scopes sc, &vt[scopes] v) {
for (@ast::pat p in a.pats) { walk_pat(*e, sc, p); }
@ -411,29 +411,18 @@ fn resolve_constr(@env e, node_id id, &@ast::constr c, &scopes sc,
if (option::is_some(new_def)) {
alt (option::get(new_def)) {
case (ast::def_fn(?pred_id, ast::pure_fn)) {
let ty::constr_general[uint] c_ =
rec(path=c.node.path, args=c.node.args, id=pred_id);
let ty::constr_def new_constr = respan(c.span, c_);
add_constr(e, id, new_constr);
e.def_map.insert(c.node.id, ast::def_fn(pred_id,
ast::pure_fn));
}
case (_) {
e.sess.span_err(c.span,
"Non-predicate in constraint: " +
ast::path_to_str(c.node.path));
path_to_str(c.node.path));
}
}
}
}
fn add_constr(&@env e, node_id id, &ty::constr_def c) {
e.fn_constrs.insert(id,
alt (e.fn_constrs.find(id)) {
case (none) { ~[c] }
case (some(?cs)) { cs + ~[c] }
});
}
// Import resolution
fn resolve_import(&env e, &@ast::view_item it, scopes sc) {
auto defid;

162
src/comp/middle/tstate/auxiliary.rs
View file

@ -72,12 +72,12 @@ fn comma_str(&(@constr_arg_use)[] args) -> str {
ret rslt;
}
fn constraint_to_str(&ty::ctxt tcx, &constr c) -> str {
alt (c.node.c) {
case (ninit(?i)) {
fn constraint_to_str(&ty::ctxt tcx, &sp_constr c) -> str {
alt (c.node) {
case (ninit(_,?i)) {
ret "init(" + i + " [" + tcx.sess.span_str(c.span) + "])";
}
case (npred(?p, ?args)) {
case (npred(?p, _, ?args)) {
ret path_to_str(p) + "(" + comma_str(args) + ")" + "[" +
tcx.sess.span_str(c.span) + "]";
}
@ -204,31 +204,36 @@ to represent predicate *arguments* however. This type
Both types store an ident and span, for error-logging purposes.
*/
type pred_desc_ = rec((@constr_arg_use)[] args, uint bit_num);
type pred_args_ = rec((@constr_arg_use)[] args, uint bit_num);
type pred_desc = spanned[pred_desc_];
type pred_args = spanned[pred_args_];
// FIXME: Should be node_id, since we can only talk
// about locals.
type constr_arg_use = constr_arg_general[tup(ident, def_id)];
// The attached node ID is the *defining* node ID
// for this local.
type constr_arg_use = spanned[constr_arg_general_[inst]];
tag constraint {
cinit(uint, span, ident);
cpred(path, @mutable pred_desc[]);
// FIXME: really only want it to be mutable during collect_locals.
// freeze it after that.
cpred(path, @mutable (pred_args[]));
}
tag constr__ {
ninit(ident);
npred(path, (@constr_arg_use)[]);
// An ninit variant has a node_id because it refers to a local var.
// An npred has a def_id since the definition of the typestate
// predicate need not be local.
// FIXME: would be nice to give both a def_id field,
// and give ninit a constraint saying it's local.
tag tsconstr {
ninit(node_id, ident);
npred(path, def_id, (@constr_arg_use)[]);
}
type constr_ = rec(node_id id, constr__ c);
type sp_constr = spanned[tsconstr];
type constr = spanned[constr_];
type norm_constraint = rec(uint bit_num, sp_constr c);
type norm_constraint = rec(uint bit_num, constr c);
type constr_map = @std::map::hashmap[node_id, constraint];
type constr_map = @std::map::hashmap[def_id, constraint];
type fn_info = rec(constr_map constrs,
uint num_constraints,
@ -240,6 +245,12 @@ type fn_info = rec(constr_map constrs,
// bug?
@mutable node_id[] used_vars);
fn tsconstr_to_def_id(&tsconstr t) -> def_id {
alt (t) {
case (ninit(?id,_)) { local_def(id) }
case (npred(_,?id,_)) { id }
}
}
/* mapping from node ID to typestate annotation */
type node_ann_table = @mutable ts_ann[mutable];
@ -468,7 +479,7 @@ fn controlflow_expr(&crate_ctxt ccx, @expr e) -> controlflow {
}
}
fn constraints_expr(&ty::ctxt cx, @expr e) -> (@ty::constr_def)[] {
fn constraints_expr(&ty::ctxt cx, @expr e) -> (@ty::constr)[] {
alt (ty::struct(cx, ty::node_id_to_type(cx, e.id))) {
case (ty::ty_fn(_, _, _, _, ?cs)) { ret cs; }
case (_) { ret ~[]; }
@ -489,18 +500,17 @@ fn node_id_to_def(&crate_ctxt ccx, node_id id) -> option::t[def] {
ret ccx.tcx.def_map.find(id);
}
fn norm_a_constraint(node_id id, &constraint c) -> norm_constraint[] {
fn norm_a_constraint(def_id id, &constraint c) -> norm_constraint[] {
alt (c) {
case (cinit(?n, ?sp, ?i)) {
ret ~[rec(bit_num=n, c=respan(sp, rec(id=id, c=ninit(i))))];
ret ~[rec(bit_num=n, c=respan(sp, ninit(id._1, i)))];
}
case (cpred(?p, ?descs)) {
let norm_constraint[] rslt = ~[];
for (pred_desc pd in *descs) {
for (pred_args pd in *descs) {
rslt += ~[rec(bit_num=pd.node.bit_num,
c=respan(pd.span,
rec(id=id,
c=npred(p, pd.node.args))))];
npred(p, id, pd.node.args)))];
}
ret rslt;
}
@ -512,19 +522,23 @@ fn norm_a_constraint(node_id id, &constraint c) -> norm_constraint[] {
// non-exhaustive match in trans.
fn constraints(&fn_ctxt fcx) -> norm_constraint[] {
let norm_constraint[] rslt = ~[];
for each (@tup(node_id, constraint) p in fcx.enclosing.constrs.items()) {
for each (@tup(def_id, constraint) p in fcx.enclosing.constrs.items()) {
rslt += norm_a_constraint(p._0, p._1);
}
ret rslt;
}
fn match_args(&fn_ctxt fcx, &pred_desc[] occs, &(@constr_arg_use)[] occ) ->
// FIXME
// Would rather take an immutable vec as an argument,
// should freeze it at some earlier point.
fn match_args(&fn_ctxt fcx, &(@mutable pred_args[]) occs,
&(@constr_arg_use)[] occ) ->
uint {
log "match_args: looking at " +
constr_args_to_str(std::util::fst[ident, def_id], occ);
for (pred_desc pd in occs) {
log "match_args: candidate " + pred_desc_to_str(pd);
fn eq(&tup(ident, def_id) p, &tup(ident, def_id) q) -> bool {
constr_args_to_str(std::util::fst[ident, node_id], occ);
for (pred_args pd in *occs) {
log "match_args: candidate " + pred_args_to_str(pd);
fn eq(&inst p, &inst q) -> bool {
ret p._1 == q._1;
}
if (ty::args_eq(eq, pd.node.args, occ)) { ret pd.node.bit_num; }
@ -532,12 +546,12 @@ fn match_args(&fn_ctxt fcx, &pred_desc[] occs, &(@constr_arg_use)[] occ) ->
fcx.ccx.tcx.sess.bug("match_args: no match for occurring args");
}
fn node_id_for_constr(ty::ctxt tcx, node_id t) -> node_id {
fn def_id_for_constr(ty::ctxt tcx, node_id t) -> def_id {
alt (tcx.def_map.find(t)) {
case (none) {
tcx.sess.bug("node_id_for_constr: bad node_id " + int::str(t));
}
case (some(def_fn(?i,_))) { ret i._1; }
case (some(def_fn(?i,_))) { ret i; }
case (_) {
tcx.sess.bug("node_id_for_constr: pred is not a function");
}
@ -550,11 +564,11 @@ fn expr_to_constr_arg(ty::ctxt tcx, &@expr e) -> @constr_arg_use {
alt (tcx.def_map.find(e.id)) {
case (some(def_local(?l_id))) {
ret @respan(p.span, carg_ident(tup(p.node.idents.(0),
l_id)));
l_id._1)));
}
case (some(def_arg(?a_id))) {
ret @respan(p.span, carg_ident(tup(p.node.idents.(0),
a_id)));
a_id._1)));
}
case (_) {
tcx.sess.bug("exprs_to_constr_args: non-local variable " +
@ -582,7 +596,7 @@ fn exprs_to_constr_args(ty::ctxt tcx, &(@expr)[] args)
rslt
}
fn expr_to_constr(ty::ctxt tcx, &@expr e) -> constr {
fn expr_to_constr(ty::ctxt tcx, &@expr e) -> sp_constr {
alt (e.node) {
case (
// FIXME change the first pattern to expr_path to test a
@ -591,9 +605,8 @@ fn expr_to_constr(ty::ctxt tcx, &@expr e) -> constr {
alt (operator.node) {
case (expr_path(?p)) {
ret respan(e.span,
rec(id=node_id_for_constr(tcx, operator.id),
c=npred(p, exprs_to_constr_args(tcx,
args))));
npred(p, def_id_for_constr(tcx, operator.id),
exprs_to_constr_args(tcx, args)));
}
case (_) {
tcx.sess.span_fatal(operator.span,
@ -610,19 +623,19 @@ fn expr_to_constr(ty::ctxt tcx, &@expr e) -> constr {
}
}
fn pred_desc_to_str(&pred_desc p) -> str {
fn pred_args_to_str(&pred_args p) -> str {
"<" + uint::str(p.node.bit_num) + ", " +
constr_args_to_str(std::util::fst[ident, def_id],
constr_args_to_str(std::util::fst[ident, node_id],
p.node.args) + ">"
}
fn substitute_constr_args(&ty::ctxt cx, &(@expr)[] actuals,
&@ty::constr_def c) -> constr__ {
&@ty::constr c) -> tsconstr {
let (@constr_arg_use)[] rslt = ~[];
for (@constr_arg a in c.node.args) {
rslt += ~[substitute_arg(cx, actuals, a)];
}
ret npred(c.node.path, rslt);
ret npred(c.node.path, c.node.id, rslt);
}
fn substitute_arg(&ty::ctxt cx, &(@expr)[] actuals, @constr_arg a) ->
@ -642,8 +655,8 @@ fn substitute_arg(&ty::ctxt cx, &(@expr)[] actuals, @constr_arg a) ->
}
}
fn pred_desc_matches(&(constr_arg_general_[tup(ident, def_id)])[] pattern,
&pred_desc desc) -> bool {
fn pred_args_matches(&(constr_arg_general_[inst])[] pattern,
&pred_args desc) -> bool {
auto i = 0u;
for (@constr_arg_use c in desc.node.args) {
auto n = pattern.(i);
@ -679,17 +692,17 @@ fn pred_desc_matches(&(constr_arg_general_[tup(ident, def_id)])[] pattern,
ret true;
}
fn find_instance_(&(constr_arg_general_[tup(ident, def_id)])[] pattern,
&pred_desc[] descs) -> option::t[uint] {
for (pred_desc d in descs) {
if (pred_desc_matches(pattern, d)) {
fn find_instance_(&(constr_arg_general_[inst])[] pattern,
&pred_args[] descs) -> option::t[uint] {
for (pred_args d in descs) {
if (pred_args_matches(pattern, d)) {
ret some(d.node.bit_num);
}
}
ret none;
}
type inst = tup(ident, def_id);
type inst = tup(ident, node_id);
type subst = tup(inst, inst)[];
fn find_instances(&fn_ctxt fcx, &subst subst, &constraint c)
@ -703,7 +716,7 @@ fn find_instances(&fn_ctxt fcx, &subst subst, &constraint c)
alt (c) {
case (cinit(_,_,_)) { /* this is dealt with separately */ }
case (cpred(?p, ?descs)) {
for (pred_desc d in *descs) {
for (pred_args d in *descs) {
if (args_mention(d.node.args, find_in_subst_bool, subst)) {
auto old_bit_num = d.node.bit_num;
auto new = replace(subst, d);
@ -720,7 +733,7 @@ fn find_instances(&fn_ctxt fcx, &subst subst, &constraint c)
rslt
}
fn find_in_subst(def_id id, &subst s) -> option::t[inst] {
fn find_in_subst(node_id id, &subst s) -> option::t[inst] {
for (tup(inst, inst) p in s) {
if (id == p._0._1) {
ret some(p._1);
@ -729,7 +742,7 @@ fn find_in_subst(def_id id, &subst s) -> option::t[inst] {
ret none;
}
fn find_in_subst_bool(&subst s, def_id id) -> bool {
fn find_in_subst_bool(&subst s, node_id id) -> bool {
is_some(find_in_subst(id, s))
}
@ -745,7 +758,7 @@ fn insts_to_str(&(constr_arg_general_[inst])[] stuff) -> str {
rslt
}
fn replace(subst subst, pred_desc d) -> (constr_arg_general_[inst])[] {
fn replace(subst subst, pred_args d) -> (constr_arg_general_[inst])[] {
let (constr_arg_general_[inst])[] rslt = ~[];
for (@constr_arg_use c in d.node.args) {
alt (c.node) {
@ -824,6 +837,15 @@ fn local_node_id_to_def_id(&fn_ctxt fcx, &node_id i) -> option::t[def_id] {
}
}
fn local_node_id_to_local_def_id(&fn_ctxt fcx, &node_id i)
-> option::t[node_id] {
alt (local_node_id_to_def(fcx, i)) {
case (some (def_local(?d_id))) { some(d_id._1) }
case (some (def_arg(?a_id))) { some(a_id._1) }
case (_) { none }
}
}
fn copy_in_postcond(&fn_ctxt fcx, node_id parent_exp, inst dest, inst src,
oper_type ty) {
auto post = node_id_to_ts_ann(fcx.ccx, parent_exp).conditions.
@ -859,7 +881,7 @@ fn copy_in_poststate_two(&fn_ctxt fcx, &poststate src_post,
}
}
for each (@tup(node_id, constraint) p in
for each (@tup(def_id, constraint) p in
fcx.enclosing.constrs.items()) {
// replace any occurrences of the src def_id with the
// dest def_id
@ -878,7 +900,7 @@ fn copy_in_poststate_two(&fn_ctxt fcx, &poststate src_post,
fn forget_in_postcond(&fn_ctxt fcx, node_id parent_exp, node_id dead_v) {
// In the postcondition given by parent_exp, clear the bits
// for any constraints mentioning dead_v
auto d = local_node_id_to_def_id(fcx, dead_v);
auto d = local_node_id_to_local_def_id(fcx, dead_v);
alt (d) {
case (some(?d_id)) {
for (norm_constraint c in constraints(fcx)) {
@ -896,7 +918,7 @@ fn forget_in_postcond_still_init(&fn_ctxt fcx, node_id parent_exp,
node_id dead_v) {
// In the postcondition given by parent_exp, clear the bits
// for any constraints mentioning dead_v
auto d = local_node_id_to_def_id(fcx, dead_v);
auto d = local_node_id_to_local_def_id(fcx, dead_v);
alt (d) {
case (some(?d_id)) {
for (norm_constraint c in constraints(fcx)) {
@ -913,7 +935,7 @@ fn forget_in_postcond_still_init(&fn_ctxt fcx, node_id parent_exp,
fn forget_in_poststate(&fn_ctxt fcx, &poststate p, node_id dead_v) -> bool {
// In the poststate given by parent_exp, clear the bits
// for any constraints mentioning dead_v
auto d = local_node_id_to_def_id(fcx, dead_v);
auto d = local_node_id_to_local_def_id(fcx, dead_v);
auto changed = false;
alt (d) {
case (some(?d_id)) {
@ -932,7 +954,7 @@ fn forget_in_poststate_still_init(&fn_ctxt fcx, &poststate p, node_id dead_v)
-> bool {
// In the poststate given by parent_exp, clear the bits
// for any constraints mentioning dead_v
auto d = local_node_id_to_def_id(fcx, dead_v);
auto d = local_node_id_to_local_def_id(fcx, dead_v);
auto changed = false;
alt (d) {
case (some(?d_id)) {
@ -947,37 +969,35 @@ fn forget_in_poststate_still_init(&fn_ctxt fcx, &poststate p, node_id dead_v)
ret changed;
}
fn any_eq(&(def_id)[] v, def_id d) -> bool {
for (def_id i in v) {
fn any_eq(&(node_id)[] v, node_id d) -> bool {
for (node_id i in v) {
if (i == d) { ret true; }
}
false
}
fn constraint_mentions(&fn_ctxt fcx, &norm_constraint c, def_id v) -> bool {
ret (alt (c.c.node.c) {
case (ninit(_)) {
v == local_def(c.c.node.id)
}
case (npred(_, ?args)) {
fn constraint_mentions(&fn_ctxt fcx, &norm_constraint c, node_id v) -> bool {
ret (alt (c.c.node) {
case (ninit(?id,_)) { v == id }
case (npred(_, _, ?args)) {
args_mention(args, any_eq, ~[v])
}
});
}
fn non_init_constraint_mentions(&fn_ctxt fcx, &norm_constraint c,
&def_id v) -> bool {
ret (alt (c.c.node.c) {
case (ninit(_)) {
&node_id v) -> bool {
ret (alt (c.c.node) {
case (ninit(_,_)) {
false
}
case (npred(_, ?args)) {
case (npred(_, _, ?args)) {
args_mention(args, any_eq, ~[v])
}
});
}
fn args_mention[T](&(@constr_arg_use)[] args, fn(&(T)[], def_id) -> bool q,
fn args_mention[T](&(@constr_arg_use)[] args, fn(&(T)[], node_id) -> bool q,
&(T)[] s) -> bool {
/*
FIXME

62
src/comp/middle/tstate/bitvectors.rs
View file

@ -1,29 +1,8 @@
import syntax::ast::*;
import syntax::walk;
import std::ivec;
import std::option::*;
import aux::constr_arg_use;
import aux::local_node_id_to_def;
import aux::fn_ctxt;
import aux::fn_info;
import aux::log_tritv;
import aux::log_tritv_err;
import aux::num_constraints;
import aux::cinit;
import aux::cpred;
import aux::ninit;
import aux::npred;
import aux::pred_desc;
import aux::match_args;
import aux::constr_;
import aux::block_precond;
import aux::stmt_precond;
import aux::expr_precond;
import aux::block_prestate;
import aux::expr_prestate;
import aux::stmt_prestate;
import tstate::aux::node_id_to_ts_ann;
import aux::*;
import tstate::ann::pre_and_post;
import tstate::ann::precond;
import tstate::ann::postcond;
@ -47,11 +26,12 @@ import tstate::ann::clear_in_prestate;
import tstate::ann::clear_in_poststate_;
import tritv::*;
fn bit_num(&fn_ctxt fcx, &constr_ c) -> uint {
assert (fcx.enclosing.constrs.contains_key(c.id));
auto rslt = fcx.enclosing.constrs.get(c.id);
alt (c.c) {
case (ninit(_)) {
fn bit_num(&fn_ctxt fcx, &tsconstr c) -> uint {
auto d = tsconstr_to_def_id(c);
assert (fcx.enclosing.constrs.contains_key(d));
auto rslt = fcx.enclosing.constrs.get(d);
alt (c) {
case (ninit(_,_)) {
alt (rslt) {
case (cinit(?n, _, _)) { ret n; }
case (_) {
@ -60,11 +40,10 @@ fn bit_num(&fn_ctxt fcx, &constr_ c) -> uint {
}
}
}
case (npred(_, ?args)) {
case (npred(_, _, ?args)) {
alt (rslt) {
case (cpred(_, ?descs)) {
auto d = *descs;
ret match_args(fcx, d, args);
ret match_args(fcx, descs, args);
}
case (_) {
fcx.ccx.tcx.sess.bug("bit_num: asked for pred constraint,"
@ -75,7 +54,7 @@ fn bit_num(&fn_ctxt fcx, &constr_ c) -> uint {
}
}
fn promises(&fn_ctxt fcx, &poststate p, &constr_ c) -> bool {
fn promises(&fn_ctxt fcx, &poststate p, &tsconstr c) -> bool {
ret promises_(bit_num(fcx, c), p);
}
@ -161,12 +140,12 @@ fn intersect_states(&prestate p, &prestate q) -> prestate {
ret rslt;
}
fn gen(&fn_ctxt fcx, node_id id, &constr_ c) -> bool {
fn gen(&fn_ctxt fcx, node_id id, &tsconstr c) -> bool {
ret set_in_postcond(bit_num(fcx, c),
node_id_to_ts_ann(fcx.ccx, id).conditions);
}
fn declare_var(&fn_ctxt fcx, &constr_ c, prestate pre) -> prestate {
fn declare_var(&fn_ctxt fcx, &tsconstr c, prestate pre) -> prestate {
auto rslt = clone(pre);
relax_prestate(bit_num(fcx, c), rslt);
// idea is this is scoped
@ -209,18 +188,18 @@ fn relax_precond_block(&fn_ctxt fcx, node_id i, &block b) {
walk::walk_block(v, b);
}
fn gen_poststate(&fn_ctxt fcx, node_id id, &constr_ c) -> bool {
fn gen_poststate(&fn_ctxt fcx, node_id id, &tsconstr c) -> bool {
log "gen_poststate";
ret set_in_poststate(bit_num(fcx, c),
node_id_to_ts_ann(fcx.ccx, id).states);
}
fn kill_prestate(&fn_ctxt fcx, node_id id, &constr_ c) -> bool {
fn kill_prestate(&fn_ctxt fcx, node_id id, &tsconstr c) -> bool {
ret clear_in_prestate(bit_num(fcx, c),
node_id_to_ts_ann(fcx.ccx, id).states);
}
fn kill_poststate(&fn_ctxt fcx, node_id id, &constr_ c) -> bool {
fn kill_poststate(&fn_ctxt fcx, node_id id, &tsconstr c) -> bool {
log "kill_poststate";
ret clear_in_poststate(bit_num(fcx, c),
node_id_to_ts_ann(fcx.ccx, id).states);
@ -233,9 +212,8 @@ fn clear_in_poststate_expr(&fn_ctxt fcx, &@expr e, &poststate t) {
case (some(?i)) {
alt (local_node_id_to_def(fcx, e.id)) {
case (some(def_local(?d_id))) {
clear_in_poststate_(bit_num(fcx,
rec(id=d_id._1,
c=ninit(i))), t);
clear_in_poststate_(
bit_num(fcx,ninit(d_id._1, i)), t);
}
case (some(_)) { /* ignore args (for now...) */ }
case (_) {
@ -252,17 +230,17 @@ fn clear_in_poststate_expr(&fn_ctxt fcx, &@expr e, &poststate t) {
fn set_in_poststate_ident(&fn_ctxt fcx, &node_id id, &ident ident,
&poststate t) -> bool {
ret set_in_poststate_(bit_num(fcx, rec(id=id, c=ninit(ident))), t);
ret set_in_poststate_(bit_num(fcx, ninit(id, ident)), t);
}
fn clear_in_poststate_ident(&fn_ctxt fcx, &node_id id, &ident ident,
&node_id parent) -> bool {
ret kill_poststate(fcx, parent, rec(id=id, c=ninit(ident)));
ret kill_poststate(fcx, parent, ninit(id, ident));
}
fn clear_in_prestate_ident(&fn_ctxt fcx, &node_id id, &ident ident,
&node_id parent) -> bool {
ret kill_prestate(fcx, parent, rec(id=id, c=ninit(ident)));
ret kill_prestate(fcx, parent, ninit(id, ident));
}
//

9
src/comp/middle/tstate/ck.rs
View file

@ -49,10 +49,9 @@ import states::find_pre_post_state_fn;
fn check_unused_vars(&fn_ctxt fcx) {
// FIXME: could be more efficient
for (norm_constraint c in constraints(fcx)) {
alt (c.c.node.c) {
case (ninit(?v)) {
if (!vec_contains(fcx.enclosing.used_vars,
c.c.node.id)) {
alt (c.c.node) {
case (ninit(?id, ?v)) {
if (!vec_contains(fcx.enclosing.used_vars, id)) {
fcx.ccx.tcx.sess.span_warn(c.c.span,
"Unused variable " + v);
}
@ -140,7 +139,7 @@ fn check_states_against_conditions(&fn_ctxt fcx, &_fn f,
/* Check that the return value is initialized */
auto post = aux::block_poststate(fcx.ccx, f.body);
let aux::constr_ ret_c = rec(id=fcx.id, c=aux::ninit(fcx.name));
let tsconstr ret_c = ninit(fcx.id, fcx.name);
if (f.proto == ast::proto_fn && !promises(fcx, post, ret_c) &&
!type_is_nil(fcx.ccx.tcx, ret_ty_of_fn(fcx.ccx.tcx, id)) &&
f.decl.cf == return) {

45
src/comp/middle/tstate/collect_locals.rs
View file

@ -14,12 +14,11 @@ import util::common::new_def_hash;
import syntax::codemap::span;
import syntax::ast::respan;
type ctxt = rec(@mutable (aux::constr[]) cs, ty::ctxt tcx);
type ctxt = rec(@mutable (sp_constr[]) cs, ty::ctxt tcx);
fn collect_local(&@local loc, &ctxt cx, &visit::vt[ctxt] v) {
log "collect_local: pushing " + loc.node.ident;
*cx.cs += ~[respan(loc.span, rec(id=loc.node.id,
c=ninit(loc.node.ident)))];
*cx.cs += ~[respan(loc.span, ninit(loc.node.id, loc.node.ident))];
visit::visit_local(loc, cx, v);
}
@ -34,11 +33,10 @@ fn collect_pred(&@expr e, &ctxt cx, &visit::vt[ctxt] v) {
// If it's a call, generate appropriate instances of the
// call's constraints.
case (expr_call(?operator, ?operands)) {
for (@ty::constr_def c in constraints_expr(cx.tcx, operator)) {
let aux::constr ct = respan(c.span,
rec(id=c.node.id._1,
c=aux::substitute_constr_args(cx.tcx, operands,
c)));
for (@ty::constr c in constraints_expr(cx.tcx, operator)) {
let sp_constr ct = respan(c.span,
aux::substitute_constr_args(cx.tcx, operands,
c));
*cx.cs += ~[ct];
}
}
@ -61,13 +59,14 @@ fn find_locals(&ty::ctxt tcx, &_fn f, &ty_param[] tps, &span sp, &fn_ident i,
ret cx;
}
fn add_constraint(&ty::ctxt tcx, aux::constr c, uint next, constr_map tbl) ->
fn add_constraint(&ty::ctxt tcx, sp_constr c, uint next, constr_map tbl) ->
uint {
log aux::constraint_to_str(tcx, c) + " |-> " + std::uint::str(next);
alt (c.node.c) {
case (ninit(?i)) { tbl.insert(c.node.id, cinit(next, c.span, i)); }
case (npred(?p, ?args)) {
alt (tbl.find(c.node.id)) {
log constraint_to_str(tcx, c) + " |-> " + std::uint::str(next);
alt (c.node) {
case (ninit(?id, ?i)) { tbl.insert(local_def(id),
cinit(next, c.span, i)); }
case (npred(?p, ?d_id, ?args)) {
alt (tbl.find(d_id)) {
case (some(?ct)) {
alt (ct) {
case (cinit(_, _, _)) {
@ -76,16 +75,15 @@ fn add_constraint(&ty::ctxt tcx, aux::constr c, uint next, constr_map tbl) ->
}
case (cpred(_, ?pds)) {
*pds += ~[respan(c.span,
rec(args=args, bit_num=next))];
rec(args=args, bit_num=next))];
}
}
}
case (none) {
tbl.insert(c.node.id,
cpred(p,
@mutable ~[respan(c.span,
rec(args=args,
bit_num=next))]));
let @mutable(pred_args[]) rslt = @mutable(~[respan(c.span,
rec(args=args,
bit_num=next))]);
tbl.insert(d_id, cpred(p, rslt));
}
}
}
@ -98,22 +96,21 @@ fn add_constraint(&ty::ctxt tcx, aux::constr c, uint next, constr_map tbl) ->
to a bit number in the precondition/postcondition vectors */
fn mk_fn_info(&crate_ctxt ccx, &_fn f, &ty_param[] tp,
&span f_sp, &fn_ident f_name, node_id id) {
auto res_map = @new_int_hash[constraint]();
auto res_map = @new_def_hash[constraint]();
let uint next = 0u;
let ctxt cx = find_locals(ccx.tcx, f, tp, f_sp, f_name, id);
/* now we have to add bit nums for both the constraints
and the variables... */
for (aux::constr c in { *cx.cs }) {
for (sp_constr c in { *cx.cs }) {
next = add_constraint(cx.tcx, c, next, res_map);
}
/* add a pseudo-entry for the function's return value
we can safely use the function's name itself for this purpose */
auto name = fn_ident_to_string(id, f_name);
add_constraint(cx.tcx, respan(f_sp, rec(id=id, c=ninit(name))), next,
res_map);
add_constraint(cx.tcx, respan(f_sp, ninit(id, name)), next, res_map);
let @mutable node_id[] v = @mutable ~[];
auto rslt =
rec(constrs=res_map,

43
src/comp/middle/tstate/pre_post_conditions.rs
View file

@ -76,7 +76,7 @@ fn find_pre_post_item(&crate_ctxt ccx, &item i) {
// make a fake fcx
let @mutable node_id[] v = @mutable ~[];
auto fake_fcx =
rec(enclosing=rec(constrs=@new_int_hash[constraint](),
rec(enclosing=rec(constrs=@new_def_hash[constraint](),
num_constraints=0u,
cf=return,
used_vars=v),
@ -135,7 +135,7 @@ fn find_pre_post_loop(&fn_ctxt fcx, &@local l, &@expr index, &block body,
node_id id) {
find_pre_post_expr(fcx, index);
find_pre_post_block(fcx, body);
auto v_init = rec(id=l.node.id, c=ninit(l.node.ident));
auto v_init = ninit(l.node.id, l.node.ident);
relax_precond_block(fcx, bit_num(fcx, v_init) as node_id, body);
// Hack: for-loop index variables are frequently ignored,
@ -160,7 +160,7 @@ fn join_then_else(&fn_ctxt fcx, &@expr antec, &block conseq,
case (none) {
alt (chck) {
case (if_check) {
let aux::constr c = expr_to_constr(fcx.ccx.tcx, antec);
let sp_constr c = expr_to_constr(fcx.ccx.tcx, antec);
gen(fcx, antec.id, c.node);
}
case (_) {}
@ -188,7 +188,7 @@ fn join_then_else(&fn_ctxt fcx, &@expr antec, &block conseq,
so that it's *not* set in the alternative. */
alt (chck) {
case (if_check) {
let aux::constr c = expr_to_constr(fcx.ccx.tcx, antec);
let sp_constr c = expr_to_constr(fcx.ccx.tcx, antec);
gen(fcx, antec.id, c.node);
}
case (_) {}
@ -219,8 +219,7 @@ fn gen_if_local(&fn_ctxt fcx, @expr lhs, @expr rhs, node_id larger_id,
set_pre_and_post(fcx.ccx, larger_id, p.precondition,
p.postcondition);
gen(fcx, larger_id,
rec(id=d_id._1,
c=ninit(path_to_ident(fcx.ccx.tcx, pth))));
ninit(d_id._1, path_to_ident(fcx.ccx.tcx, pth)));
}
case (_) { find_pre_post_exprs(fcx, ~[lhs, rhs], larger_id); }
}
@ -256,9 +255,8 @@ fn handle_update(&fn_ctxt fcx, &@expr parent,
alt (df) {
case (def_local(?d_id)) {
auto i =
bit_num(fcx,
rec(id=d_id._1,
c=ninit(path_to_ident(fcx.ccx.tcx, p))));
bit_num(fcx, ninit(d_id._1,
path_to_ident(fcx.ccx.tcx, p)));
require_and_preserve(i, expr_pp(fcx.ccx, lhs));
}
case (_) {}
@ -269,8 +267,8 @@ fn handle_update(&fn_ctxt fcx, &@expr parent,
gen_if_local(fcx, lhs, rhs, parent.id, lhs.id, p);
alt (rhs.node) {
case (expr_path(?p1)) {
auto d = local_node_id_to_def_id(fcx, lhs.id);
auto d1 = local_node_id_to_def_id(fcx, rhs.id);
auto d = local_node_id_to_local_def_id(fcx, lhs.id);
auto d1 = local_node_id_to_local_def_id(fcx, rhs.id);
alt (d) {
case (some(?id)) {
alt (d1) {
@ -312,13 +310,11 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) {
find_pre_post_exprs(fcx, args, e.id);
/* see if the call has any constraints on its type */
for (@ty::constr_def c in constraints_expr(fcx.ccx.tcx, operator))
for (@ty::constr c in constraints_expr(fcx.ccx.tcx, operator))
{
auto i =
bit_num(fcx,
rec(id=c.node.id._1,
c=substitute_constr_args(fcx.ccx.tcx,
args, c)));
bit_num(fcx, substitute_constr_args(fcx.ccx.tcx,
args, c));
require(i, expr_pp(fcx.ccx, e));
}
@ -347,8 +343,7 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) {
case (def_local(?d_id)) {
auto i =
bit_num(fcx,
rec(id=d_id._1,
c=ninit(path_to_ident(fcx.ccx.tcx, p))));
ninit(d_id._1, path_to_ident(fcx.ccx.tcx, p)));
use_var(fcx, d_id._1);
require_and_preserve(i, rslt);
}
@ -547,7 +542,7 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) {
copy_pre_post(fcx.ccx, e.id, p);
/* predicate p holds after this expression executes */
let aux::constr c = expr_to_constr(fcx.ccx.tcx, p);
let sp_constr c = expr_to_constr(fcx.ccx.tcx, p);
gen(fcx, e.id, c.node);
}
case (expr_if_check(?p, ?conseq, ?maybe_alt)) {
@ -608,17 +603,17 @@ fn find_pre_post_stmt(&fn_ctxt fcx, &stmt s) {
case (expr_path(?p)) {
copy_in_postcond(fcx, id,
tup(alocal.node.ident,
local_def(alocal.node.id)),
alocal.node.id),
tup(path_to_ident(fcx.ccx.tcx, p),
local_def(an_init.expr.id)),
op_to_oper_ty(an_init.op));
an_init.expr.id),
op_to_oper_ty(an_init.op));
}
case (_) {}
}
gen(fcx, id,
rec(id=alocal.node.id,
c=ninit(alocal.node.ident)));
ninit(alocal.node.id,
alocal.node.ident));
if (an_init.op == init_move &&
is_path(an_init.expr)) {

20
src/comp/middle/tstate/states.rs
View file

@ -63,8 +63,7 @@ fn seq_states(&fn_ctxt fcx, prestate pres, &(@expr)[] exprs) ->
}
fn find_pre_post_state_sub(&fn_ctxt fcx, &prestate pres, &@expr e,
node_id parent, option::t[aux::constr_] c)
-> bool {
node_id parent, option::t[tsconstr] c) -> bool {
auto changed = find_pre_post_state_expr(fcx, pres, e);
changed = set_prestate_ann(fcx.ccx, parent, pres) || changed;
@ -118,8 +117,8 @@ fn find_pre_post_state_two(&fn_ctxt fcx, &prestate pres, &@expr lhs,
gen_if_local(fcx, post, lhs);
alt (rhs.node) {
case (expr_path(?p1)) {
auto d = local_node_id_to_def_id(fcx, lhs.id);
auto d1 = local_node_id_to_def_id(fcx, rhs.id);
auto d = local_node_id_to_local_def_id(fcx, lhs.id);
auto d1 = local_node_id_to_local_def_id(fcx, rhs.id);
alt (d) {
case (some(?id)) {
alt (d1) {
@ -249,7 +248,7 @@ fn join_then_else(&fn_ctxt fcx, &@expr antec, &block conseq,
auto conseq_prestate = expr_poststate(fcx.ccx, antec);
alt (chk) {
case (if_check) {
let aux::constr c = expr_to_constr(fcx.ccx.tcx, antec);
let sp_constr c = expr_to_constr(fcx.ccx.tcx, antec);
conseq_prestate = tritv_clone(conseq_prestate);
tritv_set(bit_num(fcx, c.node), conseq_prestate, ttrue);
}
@ -387,8 +386,7 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
alt (fcx.enclosing.cf) {
case (noreturn) {
kill_poststate(fcx, e.id, rec(id=fcx.id,
c=ninit(fcx.name)));
kill_poststate(fcx, e.id, ninit(fcx.id, fcx.name));
}
case (_) { }
}
@ -555,7 +553,7 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
}
case (expr_check(_, ?p)) {
/* predicate p holds after this expression executes */
let aux::constr c = expr_to_constr(fcx.ccx.tcx, p);
let sp_constr c = expr_to_constr(fcx.ccx.tcx, p);
ret find_pre_post_state_sub(fcx, pres, p, e.id, some(c.node));
}
case (expr_if_check(?p, ?conseq, ?maybe_alt)) {
@ -608,9 +606,9 @@ fn find_pre_post_state_stmt(&fn_ctxt fcx, &prestate pres, @stmt s) -> bool {
auto instlhs =
tup(alocal.node.ident,
local_def(alocal.node.id));
auto rhs_d = local_node_id_to_def_id(fcx,
an_init.expr.id);
alocal.node.id);
auto rhs_d = local_node_id_to_local_def_id
(fcx, an_init.expr.id);
alt (rhs_d) {
case (some(?rhsid)) {
auto instrhs =

208
src/comp/middle/ty.rs
View file

@ -13,19 +13,15 @@ import std::option::some;
import std::smallintmap;
import driver::session;
import syntax::ast;
import ast::def_id;
import ast::constr_arg_general;
import ast::mutability;
import ast::controlflow;
import ast::path_to_str;
import ast::spanned;
import syntax::ast::*;
import syntax::codemap::span;
import metadata::csearch;
import util::common::*;
import syntax::util::interner;
import util::ppaux::ty_to_str;
import util::ppaux::ty_constr_to_str;
import util::ppaux::mode_str_1;
import syntax::print::pprust::*;
export node_id_to_monotype;
export node_id_to_type;
@ -37,7 +33,8 @@ export arg;
export args_eq;
export bind_params_in_type;
export block_ty;
export constr_def;
export constr;
export constr_;
export constr_general;
export constr_table;
export count_ty_params;
@ -67,6 +64,7 @@ export mk_bot;
export mk_box;
export mk_chan;
export mk_char;
export mk_constr;
export mk_ctxt;
export mk_float;
export mk_fn;
@ -123,6 +121,7 @@ export ty_bot;
export ty_box;
export ty_chan;
export ty_char;
export ty_constr;
export ty_float;
export ty_fn;
export ty_fn_abi;
@ -151,6 +150,7 @@ export ty_var_id;
export ty_vec;
export ty_param_substs_opt_and_ty_to_monotype;
export ty_fn_args;
export type_constr;
export type_contains_params;
export type_contains_vars;
export type_err;
@ -193,9 +193,9 @@ type method =
arg[] inputs,
t output,
controlflow cf,
(@constr_def)[] constrs);
(@constr)[] constrs);
type constr_table = hashmap[ast::node_id, constr_def[]];
type constr_table = hashmap[ast::node_id, constr[]];
type mt = rec(t ty, ast::mutability mut);
@ -212,7 +212,7 @@ type ctxt =
ast_map::map items,
freevars::freevar_map freevars,
constr_table fn_constrs,
// constr_table fn_constrs,
type_cache tcache,
creader_cache rcache,
hashmap[t, str] short_names_cache,
@ -265,7 +265,7 @@ tag sty {
ty_task;
ty_tup(mt[]);
ty_rec(field[]);
ty_fn(ast::proto, arg[], t, controlflow, (@constr_def)[]);
ty_fn(ast::proto, arg[], t, controlflow, (@constr)[]);
ty_native_fn(ast::native_abi, arg[], t);
ty_obj(method[]);
ty_res(def_id, t, t[]);
@ -273,14 +273,15 @@ tag sty {
ty_param(uint); // fn/tag type param
ty_type;
ty_native(def_id);
ty_constr(t, (@type_constr)[]);
// TODO: ty_fn_arg(t), for a possibly-aliased function argument
}
type constr_def = spanned[constr_general[uint]];
type constr_general[T] =
rec(ast::path path, (@constr_arg_general[T])[] args, def_id id);
// In the middle end, constraints have a def_id attached, referring
// to the definition of the operator in the constraint.
type constr_general[ARG] = spanned[constr_general_[ARG, def_id]];
type type_constr = constr_general[path];
type constr = constr_general[uint];
// Data structures used in type unification
tag type_err {
@ -297,6 +298,8 @@ tag type_err {
terr_obj_meths(ast::ident, ast::ident);
terr_arg_count;
terr_mode_mismatch(mode, mode);
terr_constr_len(uint, uint);
terr_constr_mismatch(@type_constr, @type_constr);
}
type ty_param_count_and_ty = tup(uint, t);
@ -392,7 +395,8 @@ fn mk_rcache() -> creader_cache {
ret map::mk_hashmap[tup(int, uint, uint), t](h, e);
}
fn mk_ctxt(session::session s, resolve::def_map dm, constr_table cs,
fn mk_ctxt(session::session s, resolve::def_map dm,
ast_map::map amap, freevars::freevar_map freevars) -> ctxt {
let node_type_table ntt =
@smallintmap::mk[ty::ty_param_substs_opt_and_ty]();
@ -405,7 +409,6 @@ fn mk_ctxt(session::session s, resolve::def_map dm, constr_table cs,
node_types=ntt,
items=amap,
freevars=freevars,
fn_constrs=cs,
tcache=tcache,
rcache=mk_rcache(),
short_names_cache=map::mk_hashmap[ty::t,
@ -501,6 +504,9 @@ fn mk_raw_ty(&ctxt cx, &sty st, &option::t[str] cname) -> raw_t {
derive_flags_t(cx, has_params, has_vars, tt);
}
}
case (ty_constr(?tt, _)) {
derive_flags_t(cx, has_params, has_vars, tt);
}
}
ret rec(struct=st,
cname=cname,
@ -594,8 +600,12 @@ fn mk_imm_tup(&ctxt cx, &t[] tys) -> t {
fn mk_rec(&ctxt cx, &field[] fs) -> t { ret gen_ty(cx, ty_rec(fs)); }
fn mk_constr(&ctxt cx, &t t, &(@type_constr)[] cs) -> t {
ret gen_ty(cx, ty_constr(t, cs));
}
fn mk_fn(&ctxt cx, &ast::proto proto, &arg[] args, &t ty, &controlflow cf,
&(@constr_def)[] constrs) -> t {
&(@constr)[] constrs) -> t {
ret gen_ty(cx, ty_fn(proto, args, ty, cf, constrs));
}
@ -1300,6 +1310,33 @@ fn hash_type_structure(&sty st) -> uint {
h += h << 5u + hash_ty(subty);
ret h;
}
fn hash_type_constr(uint id, &@type_constr c)
-> uint {
auto h = id;
h += h << 5u + hash_def(h, c.node.id);
ret hash_type_constr_args(h, c.node.args);
}
fn hash_type_constr_args(uint id, (@ty_constr_arg)[] args) -> uint {
auto h = id;
for (@ty_constr_arg a in args) {
alt (a.node) {
case (carg_base) {
h += h << 5u;
}
case (carg_lit(_)) {
// FIXME
fail "lit args not implemented yet";
}
case (carg_ident(?p)) {
// FIXME: Not sure what to do here.
h += h << 5u;
}
}
}
ret h;
}
fn hash_fn(uint id, &arg[] args, &t rty) -> uint {
auto h = id;
for (arg a in args) { h += h << 5u + hash_ty(a.ty); }
@ -1371,6 +1408,13 @@ fn hash_type_structure(&sty st) -> uint {
for (t tp in tps) { h += h << 5u + hash_ty(tp); }
ret h;
}
case (ty_constr(?t, ?cs)) {
auto h = 36u;
for (@type_constr c in cs) {
h += h << 5u + hash_type_constr(h, c);
}
ret h;
}
}
}
@ -1392,8 +1436,8 @@ fn hash_ty(&t typ) -> uint { ret typ; }
// users should use `eq_ty()` instead.
fn eq_int(&uint x, &uint y) -> bool { ret x == y; }
fn arg_eq[T](&fn(&T, &T) -> bool eq, @ast::constr_arg_general[T] a,
@ast::constr_arg_general[T] b) -> bool {
fn arg_eq[T](&fn(&T, &T) -> bool eq, @sp_constr_arg[T] a,
@sp_constr_arg[T] b) -> bool {
alt (a.node) {
case (ast::carg_base) {
alt (b.node) {
@ -1416,26 +1460,26 @@ fn arg_eq[T](&fn(&T, &T) -> bool eq, @ast::constr_arg_general[T] a,
}
}
fn args_eq[T](fn(&T, &T) -> bool eq, &(@ast::constr_arg_general[T])[] a,
&(@ast::constr_arg_general[T])[] b) -> bool {
fn args_eq[T](fn(&T, &T) -> bool eq,
&(@sp_constr_arg[T])[] a, &(@sp_constr_arg[T])[] b) -> bool {
let uint i = 0u;
for (@ast::constr_arg_general[T] arg in a) {
for (@sp_constr_arg[T] arg in a) {
if (!arg_eq(eq, arg, b.(i))) { ret false; }
i += 1u;
}
ret true;
}
fn constr_eq(&@constr_def c, &@constr_def d) -> bool {
fn constr_eq(&@constr c, &@constr d) -> bool {
ret path_to_str(c.node.path) == path_to_str(d.node.path) &&
// FIXME: hack
args_eq(eq_int, c.node.args, d.node.args);
}
fn constrs_eq(&(@constr_def)[] cs, &(@constr_def)[] ds) -> bool {
fn constrs_eq(&(@constr)[] cs, &(@constr)[] ds) -> bool {
if (ivec::len(cs) != ivec::len(ds)) { ret false; }
auto i = 0u;
for (@constr_def c in cs) {
for (@constr c in cs) {
if (!constr_eq(c, ds.(i))) { ret false; }
i += 1u;
}
@ -2053,6 +2097,76 @@ mod unify {
ret ures_err(terr_mismatch);
}
// Right now this just checks that the lists of constraints are
// pairwise equal.
fn unify_constrs(&t base_t, (@type_constr)[] expected,
&(@type_constr)[] actual) -> result {
auto expected_len = ivec::len(expected);
auto actual_len = ivec::len(actual);
if (expected_len != actual_len) {
ret ures_err(terr_constr_len(expected_len, actual_len));
}
auto i = 0u;
auto rslt;
for (@type_constr c in expected) {
rslt = unify_constr(base_t, c, actual.(i));
alt (rslt) {
case (ures_ok(_)) { }
case (ures_err(_)) { ret rslt; }
}
i += 1u;
}
ret ures_ok(base_t);
}
fn unify_constr(&t base_t, @type_constr expected,
&@type_constr actual_constr) -> result {
auto ok_res = ures_ok(base_t);
auto err_res = ures_err(terr_constr_mismatch(expected,
actual_constr));
if (expected.node.id != actual_constr.node.id) {
ret err_res;
}
auto expected_arg_len = ivec::len(expected.node.args);
auto actual_arg_len = ivec::len(actual_constr.node.args);
if (expected_arg_len != actual_arg_len) {
ret err_res;
}
auto i = 0u;
auto actual;
for (@ty_constr_arg a in expected.node.args) {
actual = actual_constr.node.args.(i);
alt (a.node) {
case (carg_base) {
alt (actual.node) {
case (carg_base) { }
case (_) { ret err_res; }
}
}
case (carg_lit(?l)) {
alt (actual.node) {
case (carg_lit(?m)) {
if (l != m) { ret err_res; }
}
case (_) { ret err_res; }
}
}
case (carg_ident(?p)) {
alt (actual.node) {
case (carg_ident(?q)) {
if (p.node != q.node) {
ret err_res;
}
}
case (_) { ret err_res; }
}
}
}
i += 1u;
}
ret ok_res;
}
// Unifies two mutability flags.
fn unify_mut(ast::mutability expected, ast::mutability actual) ->
option::t[ast::mutability] {
@ -2109,8 +2223,8 @@ mod unify {
&t expected, &t actual, &arg[] expected_inputs,
&t expected_output, &arg[] actual_inputs, &t actual_output,
&controlflow expected_cf, &controlflow actual_cf,
&(@constr_def)[] expected_constrs,
&(@constr_def)[] actual_constrs) -> result {
&(@constr)[] expected_constrs,
&(@constr)[] actual_constrs) -> result {
if (e_proto != a_proto) { ret ures_err(terr_mismatch); }
alt (expected_cf) {
case (ast::return) { }
@ -2612,6 +2726,31 @@ mod unify {
case (_) { ret ures_err(terr_mismatch); }
}
}
case (ty::ty_constr(?expected_t, ?expected_constrs)) {
// unify the base types...
alt (struct(cx.tcx, actual)) {
case (ty::ty_constr(?actual_t, ?actual_constrs)) {
auto rslt = unify_step(cx, expected_t, actual_t);
alt (rslt) {
case (ures_ok(?rty)) {
// FIXME: probably too restrictive --
// requires the constraints to be
// syntactically equal
ret unify_constrs(expected,
expected_constrs,
actual_constrs);
}
case (_) { ret rslt; }
}
}
case (_) {
// If the actual type is *not* a constrained type,
// then we go ahead and just ignore the constraints on
// the expected type. typestate handles the rest.
ret unify_step(cx, expected_t, actual);
}
}
}
}
}
fn unify(&t expected, &t actual, &@var_bindings vb, &ty_ctxt tcx) ->
@ -2730,6 +2869,15 @@ fn type_err_to_str(&ty::type_err err) -> str {
+ mode_str_1(a_mode);
fail;
}
case (terr_constr_len(?e_len, ?a_len)) {
ret "Expected a type with " + uint::str(e_len) + " constraints, \
but found one with " + uint::str(a_len) + " constraints";
}
case (terr_constr_mismatch(?e_constr, ?a_constr)) {
ret "Expected a type with constraint "
+ ty_constr_to_str(e_constr) + " but found one with constraint "
+ ty_constr_to_str(a_constr);
}
}
}

19
src/comp/middle/typeck.rs
View file

@ -2,7 +2,6 @@
import syntax::ast;
import ast::mutability;
import ast::local_def;
import ast::path_to_str;
import ast::respan;
import ast::spanned;
import syntax::walk;
@ -47,6 +46,7 @@ import std::option::some;
import std::option::from_maybe;
import std::smallintmap;
import middle::tstate::ann::ts_ann;
import syntax::print::pprust::*;
export check_crate;
@ -396,6 +396,13 @@ fn ast_ty_to_ty(&ty::ctxt tcx, &ty_getter getter, &@ast::ty ast_ty) -> ty::t {
}
typ = ty::mk_obj(tcx, ty::sort_methods(tmeths));
}
case (ast::ty_constr(?t, ?cs)) {
auto out_cs = ~[];
for (@ast::ty_constr constr in cs) {
out_cs += ~[ast_constr_to_constr(tcx, constr)];
}
typ = ty::mk_constr(tcx, ast_ty_to_ty(tcx, getter, t), out_cs);
}
}
alt (cname) {
case (none) {/* no-op */ }
@ -2519,8 +2526,8 @@ fn get_obj_info(&@crate_ctxt ccx) -> option::t[obj_info] {
ret ivec::last[obj_info](ccx.obj_infos);
}
fn ast_constr_to_constr(ty::ctxt tcx, &@ast::constr c)
-> @ty::constr_def {
fn ast_constr_to_constr[T](ty::ctxt tcx, &@ast::constr_general[T] c)
-> @ty::constr_general[T] {
alt (tcx.def_map.find(c.node.id)) {
case (some(ast::def_fn(?pred_id, ast::pure_fn))) {
ret @respan(c.span, rec(path=c.node.path, args=c.node.args,
@ -2528,9 +2535,9 @@ fn ast_constr_to_constr(ty::ctxt tcx, &@ast::constr c)
}
case (_) {
tcx.sess.span_fatal(c.span, "Predicate "
+ path_to_str(c.node.path)
+ " is unbound or bound to a non-function or an\
impure function");
+ path_to_str(c.node.path)
+ " is unbound or bound to a non-function or an \
impure function");
}
}
}