Reject programs with unsatisfied predicate constraints

Generate appropriate constraints for calls to functions with
preconditions, and reject calls where those constraints don't
hold true in the prestate.

...by which I mean that it works for one test case :-)

src/comp/front/ast.rs

@@ -355,14 +355,31 @@ tag ty_ {
     ty_constr(@ty, vec[@constr]);
 }
 
-tag constr_arg_ {
+/*
+A constraint arg that's a function argument is referred to by its position
+rather than name.  This is so we could have higher-order functions that have
+constraints (potentially -- right now there's no way to write that), and also
+so that the typestate pass doesn't have to map a function name onto its decl.
+So, the constr_arg type is parameterized: it's instantiated with uint for
+declarations, and ident for uses.
+*/
+tag constr_arg_general_[T] {
     carg_base;
-    carg_ident(ident);
+    carg_ident(T); 
     carg_lit(@lit);
 }
-type constr_arg = spanned[constr_arg_];
+type constr_arg = constr_arg_general[uint];
-type constr_ = rec(path path, vec[@constr_arg] args);
+type constr_arg_use = constr_arg_general[ident];
-type constr = spanned[constr_];
+type constr_arg_general[T] = spanned[constr_arg_general_[T]];
+
+// The ann field is there so that using the def_map in the type
+// context, we can get the def_id for the path.
+type constr_general[T] = rec(path path,
+                             vec[@constr_arg_general[T]] args,
+                             ann ann);
+
+type constr = spanned[constr_general[uint]];
+type constr_use = spanned[constr_general[ident]];
 
 type arg = rec(mode mode, @ty ty, ident ident, def_id id);
 type fn_decl = rec(vec[arg] inputs,

src/comp/front/creader.rs

@@ -94,6 +94,9 @@ fn parse_constrs(@pstate st, str_def sd) -> vec[@ast::constr] {
 }
 
 fn parse_constr(@pstate st, str_def sd) -> @ast::constr {
+    st.tcx.sess.unimpl("Reading constraints "
+                   + " isn't implemented");
+    /*
     let vec[@ast::constr_arg] args = [];
     auto sp = rec(lo=0u,hi=0u); // FIXME
     let vec[ast::ident] ids = [];
@@ -105,6 +108,7 @@ fn parse_constr(@pstate st, str_def sd) -> @ast::constr {
     log_err(p1);
     let char ignore = next(st) as char;
     assert(ignore as char == '(');
+    auto def = parse_def(st, sd);
     do {
         alt (peek(st) as char) {
             case ('*') {
@@ -132,7 +136,7 @@ fn parse_constr(@pstate st, str_def sd) -> @ast::constr {
         }
     } while (next(st) as char == ',');
     ignore = next(st) as char;
-    ret @respan(sp, rec(path=pth, args=args));
+    */
 }
 
 fn parse_ty(@pstate st, str_def sd) -> ty::t {

src/comp/front/parser.rs

@@ -339,7 +339,7 @@ fn parse_ty_fn(ast::proto proto, &parser p, uint lo)
     auto inputs = parse_seq(token::LPAREN, token::RPAREN,
                             some(token::COMMA), parse_fn_input_ty, p);
 
-    auto constrs = parse_constrs(p);
+    auto constrs = parse_constrs([], p);
 
     let @ast::ty output;
     auto cf = ast::return;
@@ -409,35 +409,57 @@ fn parse_ty_field(&parser p) -> ast::ty_field {
     ret spanned(lo, mt.ty.span.hi, rec(ident=id, mt=mt));
 }
 
-fn parse_constr_arg(&parser p) -> @ast::constr_arg {
+// if i is the jth ident in args, return j
+// otherwise, fail
+fn ident_index(&parser p, &vec[ast::arg] args, &ast::ident i) -> uint {
+    auto j = 0u;
+    for (ast::arg a in args) {
+        if (a.ident == i) {
+            ret j;
+        }
+        j += 1u;
+    }
+    p.get_session().span_err(p.get_span(),
+      "Unbound variable " + i + " in constraint arg");
+}
+
+fn parse_constr_arg(vec[ast::arg] args, &parser p) -> @ast::constr_arg {
     auto sp = p.get_span();
     auto carg = ast::carg_base;
     if (p.peek() == token::BINOP(token::STAR)) {
         p.bump();
     } else {
-        carg = ast::carg_ident(parse_value_ident(p));
+        let ast::ident i = parse_value_ident(p);
+        carg = ast::carg_ident(ident_index(p, args, i));
     }
     ret @rec(node=carg, span=sp);
 }
 
-fn parse_ty_constr(&parser p) -> @ast::constr {
+fn parse_ty_constr(&vec[ast::arg] fn_args, &parser p) -> @ast::constr {
     auto lo = p.get_lo_pos();
     auto path = parse_path(p);
-    auto pf = parse_constr_arg;
+    auto pf = bind parse_constr_arg(fn_args, _);
-    auto args = parse_seq[@ast::constr_arg](token::LPAREN,
+    let rec(vec[@ast::constr_arg] node, span span) args =
+         parse_seq[@ast::constr_arg](token::LPAREN,
                                          token::RPAREN,
                                          some(token::COMMA), pf, p);
-    ret @spanned(lo, args.span.hi, rec(path=path, args=args.node));
+    // FIXME fix the def_id
+    ret @spanned(lo, args.span.hi,
+                 rec(path=path, args=args.node, ann=p.get_ann()));
 }
 
-fn parse_constrs(&parser p) -> common::spanned[vec[@ast::constr]] {
+// Use the args list to translate each bound variable 
+// mentioned in a constraint to an arg index.
+// Seems weird to do this in the parser, but I'm not sure how else to.
+fn parse_constrs(&vec[ast::arg] args, 
+                 &parser p) -> common::spanned[vec[@ast::constr]] {
     auto lo = p.get_lo_pos();
     auto hi = p.get_hi_pos();
     let vec[@ast::constr] constrs = [];
     if (p.peek() == token::COLON) {
         p.bump();
         while (true) {
-            auto constr = parse_ty_constr(p);
+            auto constr = parse_ty_constr(args, p);
             hi = constr.span.hi;
             vec::push[@ast::constr](constrs, constr);
             if (p.peek() == token::COMMA) {
@@ -452,7 +474,7 @@ fn parse_constrs(&parser p) -> common::spanned[vec[@ast::constr]] {
 
 fn parse_ty_constrs(@ast::ty t, &parser p) -> @ast::ty {
    if (p.peek() == token::COLON) {
-       auto constrs = parse_constrs(p);
+       auto constrs = parse_constrs([], p);
        ret @spanned(t.span.lo, constrs.span.hi,
                     ast::ty_constr(t, constrs.node));
    }
@@ -1768,7 +1790,7 @@ fn parse_fn_decl(&parser p, ast::purity purity) -> ast::fn_decl {
 
     let ty_or_bang res;
 
-    auto constrs = parse_constrs(p).node;
+    auto constrs = parse_constrs(inputs.node, p).node;
 
     if (p.peek() == token::RARROW) {
         p.bump();

src/comp/middle/metadata.rs

@@ -286,6 +286,8 @@ mod Encode {
     fn enc_constr(&io::writer w, &@ctxt cx, &@ast::constr c) {
         w.write_str(path_to_str(c.node.path));
         w.write_char('(');
+        // FIXME
+        //   w.write_str(cx.ds(c.node.id));
         auto comma = false;
         for (@constr_arg a in c.node.args) {
             if (comma) {
@@ -299,7 +301,7 @@ mod Encode {
                     w.write_char('*');
                 }
                 case (carg_ident(?i)) {
-                    w.write_str(i);
+                    w.write_uint(i);
                 }
                 case (carg_lit(?l)) {
                     w.write_str(lit_to_str(l));

src/comp/middle/resolve.rs

@@ -254,7 +254,8 @@ 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_fn = visit_fn_with_scope
+                  visit_fn = visit_fn_with_scope,
+                  visit_constr = bind walk_constr(e, _, _, _)
                   with *visit::default_visitor());
     visit::visit_crate(*c, cons(scope_crate(c), @nil),
                        visit::vtor(v));
@@ -270,6 +271,14 @@ fn resolve_names(&@env e, &@ast::crate c) {
             case (_) {}
         }
     }
+
+    fn walk_constr(@env e, &@ast::constr c, &scopes sc, &vt[scopes] v) {
+        auto new_def = lookup_path_strict(*e, sc, c.span,
+                                          c.node.path.node.idents,
+                                          ns_value);
+        e.def_map.insert(c.node.ann.id, new_def);
+    }
+
     fn walk_ty(@env e, &@ast::ty t, &scopes sc, &vt[scopes] v) {
         visit::visit_ty(t, sc, v);
         alt (t.node) {

src/comp/middle/tstate/auxiliary.rs

@@ -51,10 +51,10 @@ fn def_id_to_str(def_id d) -> str {
    ret (istr(d._0) + "," + istr(d._1));
 }
 
-fn comma_str(vec[@constr_arg] args) -> str {
+fn comma_str(vec[@constr_arg_use] args) -> str {
     auto res = "";
     auto comma = false;
-    for (@constr_arg a in args) {
+    for (@constr_arg_use a in args) {
         if (comma) {
             res += ", ";
         }
@@ -78,10 +78,10 @@ fn comma_str(vec[@constr_arg] args) -> str {
 
 fn constraint_to_str(ty::ctxt tcx, constr c) -> str {
     alt (c.node) {
-        case (ninit(?i)) {
+        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) + "]";
         }
@@ -211,16 +211,18 @@ fn print_idents(vec[ident] idents) -> () {
 /* mapping from def_id to bit number and other data
    (ident/path/span are there for error-logging purposes) */
 
-type pred_desc_ = rec(vec[@constr_arg] args,
+/* FIXME very confused about why we have all these different types. */
+
+type pred_desc_ = rec(vec[@constr_arg_use] args,
                       uint bit_num);
 type pred_desc = spanned[pred_desc_];
 tag constraint {
-    cinit(uint, span, ident);
+    cinit(uint, span, def_id, ident);
-    cpred(path, @mutable vec[pred_desc]);
+    cpred(path, def_id, @mutable vec[pred_desc]);
 }
 tag constr_ {
-    ninit(ident);
+    ninit(ident, def_id);
-    npred(path, vec[@constr_arg]);
+    npred(path, def_id, vec[@constr_arg_use]);
 }
 type constr = spanned[constr_];
 type norm_constraint = rec(uint bit_num,
@@ -231,11 +233,18 @@ type norm_constraint = rec(uint bit_num,
    a pred. */
 tag constr_occ {
     occ_init;
-    occ_args(vec[@constr_arg]);
+    occ_args(vec[@constr_arg_use]);
 }
    
 type constr_map = @std::map::hashmap[def_id, constraint];
 
+fn constr_id(&constr c) -> def_id {
+    ret (alt (c.node) {
+            case (ninit(_, ?i))    { i }
+            case (npred(_, ?i, _)) { i }
+        })
+}
+
 type fn_info  = rec(constr_map constrs, uint num_constraints, controlflow cf);
 
 /* mapping from node ID to typestate annotation */
@@ -495,8 +504,8 @@ fn controlflow_expr(&crate_ctxt ccx, @expr e) -> controlflow {
     }
 }
 
-fn constraints_expr(&crate_ctxt ccx, @expr e) -> vec[@ast::constr] {
+fn constraints_expr(&ty::ctxt cx, @expr e) -> vec[@ast::constr] {
-    alt (ty::struct(ccx.tcx, ty::ann_to_type(ccx.tcx, expr_ann(e)))) {
+    alt (ty::struct(cx, ty::ann_to_type(cx, expr_ann(e)))) {
         case (ty::ty_fn(_,_,_,_,?cs)) {
             ret cs;
         }
@@ -506,8 +515,8 @@ fn constraints_expr(&crate_ctxt ccx, @expr e) -> vec[@ast::constr] {
     }
 }
 
-fn ann_to_def_strict(&crate_ctxt ccx, &ann a) -> def {
+fn ann_to_def_strict(&ty::ctxt cx, &ann a) -> def {
-    alt (ccx.tcx.def_map.find(a.id)) {
+    alt (cx.def_map.find(a.id)) {
         case (none) { 
             log_err("ann_to_def: node_id " + uistr(a.id) + " has no def");
             fail;
@@ -522,14 +531,14 @@ fn ann_to_def(&crate_ctxt ccx, &ann a) -> option::t[def] {
 
 fn norm_a_constraint(&constraint c) -> vec[norm_constraint] {
     alt (c) {
-        case (cinit(?n, ?sp, ?i)) {
+        case (cinit(?n, ?sp, ?id, ?i)) {
-            ret [rec(bit_num=n, c=respan(sp, ninit(i)))];
+            ret [rec(bit_num=n, c=respan(sp, ninit(i, id)))];
         }
-        case (cpred(?p, ?descs)) {
+        case (cpred(?p, ?id, ?descs)) {
             let vec[norm_constraint] res = [];
             for (pred_desc pd in *descs) {
                 vec::push(res, rec(bit_num=pd.node.bit_num,
-                  c=respan(pd.span, npred(p, pd.node.args))));
+                  c=respan(pd.span, npred(p, id, pd.node.args))));
             }
             ret res;
         }
@@ -547,29 +556,26 @@ fn constraints(&fn_ctxt fcx) -> vec[norm_constraint] {
     ret res;
 }
 
-
 // FIXME:
 // this probably doesn't handle name shadowing well (or at all)
 // variables should really always be id'd by def_id and not ident
 fn match_args(&fn_ctxt fcx, vec[pred_desc] occs,
-              vec[@constr_arg] occ) -> uint {
+              vec[@constr_arg_use] occ) -> uint {
-    log ("match_args: looking at " + constr_args_to_str(occ));
+    log ("match_args: looking at " +
+             pretty::ppaux::constr_args_to_str_1(occ));
     for (pred_desc pd in occs) {
         log ("match_args: candidate " + pred_desc_to_str(pd));
-        if (ty::args_eq(pd.node.args, occ)) {
+        if (ty::args_eq(str::eq, pd.node.args, occ)) {
             ret pd.node.bit_num;
         }
     }
     fcx.ccx.tcx.sess.bug("match_args: no match for occurring args");  
 }
 
-
-type constraint_info = rec(def_id id, constr c);
-
 fn constr_to_constr_occ(&ty::ctxt tcx, &constr_ c) -> constr_occ {
     alt (c) {
-        case (ninit(_)) { ret occ_init; }
+        case (ninit(_, _)) { ret occ_init; }
-        case (npred(_, ?args)) { ret occ_args(args); }
+        case (npred(_, _, ?args)) { ret occ_args(args); }
     }
 }
 
@@ -587,41 +593,42 @@ fn def_id_for_constr(ty::ctxt tcx, uint t) -> def_id {
     }
 }
 
-
+fn expr_to_constr_arg(ty::ctxt tcx, &@expr e) -> @constr_arg_use {
-fn exprs_to_constr_args(ty::ctxt tcx, vec[@expr] args) -> vec[@constr_arg] {
+    alt (e.node) {
-    fn one(ty::ctxt tcx, &@expr e) -> @constr_arg {
+        case (expr_path(?p, _)) {
-        alt (e.node) {
+            if (vec::len(p.node.idents) == 1u) {
-            case (expr_path(?p, _)) {
+                ret @respan(p.span, carg_ident[ident](p.node.idents.(0)));
-                if (vec::len(p.node.idents) == 1u) {
-                    ret @respan(p.span, carg_ident(p.node.idents.(0)));
-                }
-                else {
-                    tcx.sess.bug("exprs_to_constr_args: non-local variable "
-                                 + "as pred arg");
-                }
             }
-            case (expr_lit(?l, _)) {
+            else {
-                ret @respan(e.span, carg_lit(l));
+                tcx.sess.bug("exprs_to_constr_args: non-local variable "
-            }
+                             + "as pred arg");
-            case (_) {
-                tcx.sess.bug("exprs_to_constr_args: ill-formed pred arg");
             }
         }
+        case (expr_lit(?l, _)) {
+            ret @respan(e.span, carg_lit(l));
+        }
+        case (_) {
+            tcx.sess.bug("exprs_to_constr_args: ill-formed pred arg");
+        }
     }
-    auto f = bind one(tcx, _);
+}
+
+fn exprs_to_constr_args(ty::ctxt tcx, vec[@expr] args)
+    -> vec[@constr_arg_use] {
+    auto f = bind expr_to_constr_arg(tcx, _);
     ret vec::map(f, args); 
 }
 
-fn expr_to_constr(ty::ctxt tcx, &@expr e) -> constraint_info {
+fn expr_to_constr(ty::ctxt tcx, &@expr e) -> constr {
     alt (e.node) {
         // FIXME
         // change the first pattern to expr_path to test a typechecker bug
         case (expr_call(?operator, ?args, _)) {
             alt (operator.node) {
                 case (expr_path(?p, ?a)) {
-                    ret rec(id=def_id_for_constr(tcx, a.id),
+                    ret respan(e.span,
-                            c=respan(e.span,
+                               npred(p, def_id_for_constr(tcx, a.id),
-                                npred(p, exprs_to_constr_args(tcx, args)))); 
+                                     exprs_to_constr_args(tcx, args))); 
                 }
                 case (_) {
                     tcx.sess.span_err(operator.span, "Internal error: " +
@@ -638,55 +645,42 @@ fn expr_to_constr(ty::ctxt tcx, &@expr e) -> constraint_info {
 
 fn pred_desc_to_str(&pred_desc p) -> str {
     ret ("<" + uistr(p.node.bit_num) + ", " + 
-         constr_args_to_str(p.node.args) + ">");
+         pretty::ppaux::constr_args_to_str_1(p.node.args) + ">");
+}
+
+fn substitute_constr_args_(&ty::ctxt cx,
+                          &vec[@expr] actuals, &@ast::constr c)
+    -> vec[@constr_arg_use] {
+    let vec[@constr_arg_use] res = [];
+    for (@constr_arg a in c.node.args) {
+        res += [substitute_arg(cx, actuals, a)];
+    }
+    ret res;
+
 }
 
 fn substitute_constr_args(&ty::ctxt cx,
-                          &vec[@expr] actuals,
+      &vec[@expr] actuals, &@ast::constr c) -> constr_occ {
-                          &vec[arg] formals, &@ast::constr c) -> constr_occ {
+    ret occ_args(substitute_constr_args_(cx, actuals, c));
-    let vec[@constr_arg] res = [];
-    auto subst = vec::zip(formals, actuals);
-    for (@constr_arg a in c.node.args) {
-        res += [substitute_arg(cx, subst, a)];
-    }
-    ret occ_args(res);
 }
 
 type subst = vec[tup(arg, @expr)];
 
-fn substitute_arg(&ty::ctxt cx, &subst subst, @ast::constr_arg a)
+fn substitute_arg(&ty::ctxt cx, &vec[@expr] actuals, @ast::constr_arg a)
-     -> @constr_arg {
+     -> @constr_arg_use {
+    auto num_actuals = vec::len(actuals);
     alt (a.node) {
         case (carg_ident(?i)) {
-            ret find_arg(a.span, cx, i, subst);
+            if (i < num_actuals) {
-        }
+                ret expr_to_constr_arg(cx, actuals.(i));
-        case (_) { ret a; }
+            }
-    }
+            else {
-
+                cx.sess.span_err(a.span, "Constraint argument out of bounds");
-}
-
-fn find_arg(&span sp, ty::ctxt cx, ident i, subst subst) -> @constr_arg {
-    for (tup(arg, @expr) p in subst) {
-        if (p._0.ident == i) {
-            alt (p._1.node) {
-                case (expr_path(?pt, _)) {
-                    // ??? maybe should check that pt is a local?
-                    let option::t[ident] thing = vec::last(pt.node.idents);
-                    assert (! option::is_none(thing));
-                    ret @respan(p._1.span, carg_ident(option::get(thing)));
-                }
-                case (expr_lit(?l, _)) {
-                    ret @respan(p._1.span, carg_lit(l));
-                }
-                case (_) {
-                    cx.sess.span_err(p._1.span,
-                                     "Unsupported form of argument " +
-                                     "in a call to a constrained function");
-                }
             }
         }
+        case (carg_base) { ret @respan(a.span, carg_base); }
+        case (carg_lit(?l))  { ret @respan(a.span, carg_lit(l)); }
     }
-    cx.sess.span_err(sp, "Constraint contains an unbound variable " + i);
 }
 
 //

src/comp/middle/tstate/bitvectors.rs

@@ -41,7 +41,7 @@ fn bit_num(&fn_ctxt fcx, &def_id v, &constr_occ o) -> uint {
     alt (o) {
         case (occ_init) {
             alt (res) {
-                case (cinit(?n,_,_)) {
+                case (cinit(?n,_,_,_)) {
                     ret n;
                 }
                 case (_) {
@@ -52,7 +52,7 @@ fn bit_num(&fn_ctxt fcx, &def_id v, &constr_occ o) -> uint {
         }
         case (occ_args(?args)) {
             alt (res) {
-                case (cpred(_, ?descs)) {
+                case (cpred(_, _, ?descs)) {
                     ret match_args(fcx, *descs, args);
                 }
                 case (_) {

src/comp/middle/tstate/collect_locals.rs

@@ -1,6 +1,7 @@
 import std::vec;
 import std::vec::plus_option;
 
+import front::ast;
 import front::ast::*;
 import option::*;
 
@@ -12,30 +13,30 @@ import aux::cinit;
 import aux::ninit;
 import aux::npred;
 import aux::cpred;
+import aux::constr;
 import aux::constraint;
 import aux::fn_info;
 import aux::crate_ctxt;
 import aux::num_constraints;
 import aux::constr_map;
-import aux::constraint_info;
 import aux::expr_to_constr;
+import aux::constraints_expr;
+import aux::ann_to_def_strict;
 
 import util::common::new_def_hash;
 import util::common::uistr;
 import util::common::span;
 import util::common::respan;
 
-type ctxt = rec(@mutable vec[constraint_info] cs,
+type ctxt = rec(@mutable vec[constr] cs,
                 ty::ctxt tcx);
 
 fn collect_local(&ctxt cx, &@decl d) -> () {
     alt (d.node) {
       case (decl_local(?loc)) {
         log("collect_local: pushing " + loc.ident);
-        vec::push[constraint_info](*cx.cs,
+        vec::push[constr](*cx.cs, respan(d.span,
-                                   rec(id=loc.id,
+                                         ninit(loc.ident, loc.id)));
-                                       c=respan(d.span,
-                                                ninit(loc.ident))));
       }
       case (_) { ret; }
     }
@@ -44,7 +45,29 @@ fn collect_local(&ctxt cx, &@decl d) -> () {
 fn collect_pred(&ctxt cx, &@expr e) -> () {
     alt (e.node) {
         case (expr_check(?e, _)) {
-            vec::push[constraint_info](*cx.cs, expr_to_constr(cx.tcx, e));
+            vec::push[constr](*cx.cs, expr_to_constr(cx.tcx, e));
+        }
+        // If it's a call, generate appropriate instances of the
+        // call's constraints.
+        case (expr_call(?operator, ?operands, ?a)) {
+            for (@ast::constr c in constraints_expr(cx.tcx, operator)) {
+                auto d_id = ann_to_def_strict(cx.tcx, c.node.ann);
+                alt (d_id) {
+                    case (def_fn(?an_id)) {
+                        let constr an_occ = respan(c.span,
+                              npred(c.node.path, an_id, 
+                                    aux::substitute_constr_args_(cx.tcx,
+                                                                 operands,
+                                                                 c)));
+                        vec::push[constr](*cx.cs, an_occ);
+                    }
+                    case (_) {
+                        cx.tcx.sess.span_err(c.span,
+                                             "Non-pred in constraint");
+                    }
+                }
+            }
+            // FIXME: constraints on result type
         }
         case (_) { }
     }
@@ -52,7 +75,7 @@ fn collect_pred(&ctxt cx, &@expr e) -> () {
 
 fn find_locals(&ty::ctxt tcx, &_fn f, &span sp, &ident i, &def_id d, &ann a)
     -> ctxt {
-    let ctxt cx = rec(cs=@mutable vec::alloc[constraint_info](0u), tcx=tcx);
+    let ctxt cx = rec(cs=@mutable vec::alloc[constr](0u), tcx=tcx);
     auto visitor = walk::default_visitor();
     visitor = rec(visit_decl_pre=bind collect_local(cx,_),
                   visit_expr_pre=bind collect_pred(cx,_)
@@ -61,32 +84,33 @@ fn find_locals(&ty::ctxt tcx, &_fn f, &span sp, &ident i, &def_id d, &ann a)
     ret cx;
 }
 
-fn add_constraint(&ty::ctxt tcx, constraint_info c, uint next, constr_map tbl)
+fn add_constraint(&ty::ctxt tcx, constr c, uint next, constr_map tbl)
     -> uint {
-    log(aux::constraint_to_str(tcx, c.c) + " |-> "
+    log(aux::constraint_to_str(tcx, c) + " |-> "
         + util::common::uistr(next));
-    let aux::constr cn = c.c;
+    alt (c.node) {
-    alt (cn.node) {
+        case (ninit(?i, ?id)) {
-        case (ninit(?i)) {
+            tbl.insert(id, cinit(next, c.span, id, i));
-            tbl.insert(c.id, cinit(next, cn.span, i));
         }
-        case (npred(?p, ?args)) {
+        case (npred(?p, ?id, ?args)) {
-            alt (tbl.find(c.id)) {
+            alt (tbl.find(id)) {
                 case (some[constraint](?ct)) {
                     alt (ct) {
-                        case (cinit(_,_,_)) {
+                        case (cinit(_,_,_,_)) {
                             tcx.sess.bug("add_constraint: same def_id used"
                                          + " as a variable and a pred");
                         }
-                        case (cpred(_, ?pds)) {
+                        case (cpred(_, _, ?pds)) {
-                             vec::push(*pds, respan(cn.span,
+                             vec::push(*pds, respan(c.span,
                               rec(args=args, bit_num=next)));
                         }
                     }
                 }
+                // FIXME: this suggests a cpred shouldn't really have a
+                // def_id as a field...
                 case (none[constraint]) {
-                     tbl.insert(c.id, cpred(p,
+                    tbl.insert(id, cpred(p, id,
-                      @mutable [respan(cn.span, rec(args=args,
+                      @mutable [respan(c.span, rec(args=args,
                                                     bit_num=next))]));
                 }
             }
@@ -111,13 +135,12 @@ fn mk_fn_info(&crate_ctxt ccx, &_fn f, &span f_sp,
     /* now we have to add bit nums for both the constraints
        and the variables... */
 
-    for (constraint_info c in {*cx.cs}) {
+    for (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 */
-    add_constraint(cx.tcx, rec(id=f_id,
+    add_constraint(cx.tcx, respan(f_sp, ninit(f_name, f_id)), next, res_map);
-                               c=respan(f_sp, ninit(f_name))), next, res_map);
     
     auto res = rec(constrs=res_map,
                             num_constraints=vec::len(*cx.cs) + 1u,

src/comp/middle/tstate/pre_post_conditions.rs

@@ -46,10 +46,10 @@ import aux::ann_to_ts_ann;
 import aux::set_postcond_false;
 import aux::controlflow_expr;
 import aux::expr_to_constr;
-import aux::constraint_info;
 import aux::constr_to_constr_occ;
 import aux::constraints_expr;
 import aux::substitute_constr_args;
+import aux::constr_id;
 
 import bitvectors::seq_preconds;
 import bitvectors::union_postconds;
@@ -61,7 +61,6 @@ import bitvectors::gen;
 import front::ast::*;
 
 import middle::ty::expr_ann;
-import middle::ty::lookup_fn_decl;
 
 import util::common::new_def_hash;
 import util::common::decl_lhs;
@@ -220,36 +219,29 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) -> () {
             auto args = vec::clone[@expr](operands);
             vec::push[@expr](args, operator);
             find_pre_post_exprs(fcx, args, a);
-            
+          
+            /* should test higher-order constrained functions */
+            /* FIXME */
+
             /* see if the call has any constraints on its in type */
-            let option::t[tup(fn_decl, def_id)] decl_and_id =
+            log("a function: " );
-                lookup_fn_decl(fcx.ccx.tcx, expr_ann(operator));
+            log_expr(*operator);
-            alt (decl_and_id) {
+            auto pp = expr_pp(fcx.ccx, e);
-                case (some(?p)) {
+            for (@constr c in constraints_expr(fcx.ccx.tcx, operator)) {
-                    log("known function: " );
+                auto id = ann_to_def(fcx.ccx, c.node.ann);
-                    log_expr(*operator);
+                alt (id) {
-                    let def_id f_id = p._1;
+                    case (some(def_fn(?d_id))) {
-                    let fn_decl f_decl = p._0;
+                        auto i = bit_num(fcx, d_id,
-                    auto pp = expr_pp(fcx.ccx, e);
+                          substitute_constr_args(fcx.ccx.tcx, operands, c));
-                    for (@constr c in constraints_expr(fcx.ccx, operator)) {
-                        auto i = bit_num(fcx, f_id,
-                           substitute_constr_args(fcx.ccx.tcx, operands,
-                                                  f_decl.inputs, c));
                         require(i, pp);
                     }
+                    case (_) {
+                        fcx.ccx.tcx.sess.span_err(c.span, "Unbound pred "
+                          + " or pred that's not bound to a function");
+                    }
                 }
-                // FIXME: Soundness? If a function is constrained...
-                // shouldn't be able to pass it as an argument
-                // But typechecking guarantees that. However, we could
-                // have an unknown function w/ a constrained type =>
-                // no decl... but need to know the argument names.
-                // Fix that and then make a test w/ a higher-order
-                // constrained function.
-                case (_) { 
-                    log("unknown function: " );
-                    log_expr(*operator);
-                    /* unknown function -- do nothing */ }
             }
+             
             // FIXME: constraints on result type
             
             /* if this is a failing call, its postcondition sets everything */
@@ -275,7 +267,7 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) -> () {
             auto res = expr_pp(fcx.ccx, e);
             clear_pp(res);
 
-            auto df = ann_to_def_strict(fcx.ccx, a);
+            auto df = ann_to_def_strict(fcx.ccx.tcx, a);
             alt (df) {
                 case (def_local(?d_id)) {
                     auto i = bit_num(fcx, d_id, occ_init);
@@ -518,9 +510,9 @@ fn find_pre_post_expr(&fn_ctxt fcx, @expr e) -> () {
             find_pre_post_expr(fcx, p);
             copy_pre_post(fcx.ccx, a, p);
             /* predicate p holds after this expression executes */
-            let constraint_info c = expr_to_constr(fcx.ccx.tcx, p);
+            let aux::constr c = expr_to_constr(fcx.ccx.tcx, p);
-            let constr_occ o = constr_to_constr_occ(fcx.ccx.tcx, c.c.node);
+            let constr_occ o = constr_to_constr_occ(fcx.ccx.tcx, c.node);
-            gen(fcx, a, c.id, o);
+            gen(fcx, a, constr_id(c), o);
         }
         case(expr_bind(?operator, ?maybe_args, ?a)) {
             auto args = vec::cat_options[@expr](maybe_args);

src/comp/middle/tstate/states.rs

@@ -50,9 +50,9 @@ import aux::controlflow_expr;
 import aux::ann_to_def;
 import aux::occ_init;
 import aux::expr_to_constr;
-import aux::constraint_info;
 import aux::constr_to_constr_occ;
 import aux::constr_occ;
+import aux::constr_id;
 
 import bitvectors::seq_preconds;
 import bitvectors::union_postconds;
@@ -527,9 +527,9 @@ fn find_pre_post_state_expr(&fn_ctxt fcx, &prestate pres, @expr e) -> bool {
         changed = find_pre_post_state_expr(fcx, pres, p) || changed;
         changed = extend_poststate_ann(fcx.ccx, a, pres) || changed;
         /* predicate p holds after this expression executes */
-        let constraint_info c = expr_to_constr(fcx.ccx.tcx, p);
+        let aux::constr c = expr_to_constr(fcx.ccx.tcx, p);
-        let constr_occ o = constr_to_constr_occ(fcx.ccx.tcx, c.c.node);
+        let constr_occ o = constr_to_constr_occ(fcx.ccx.tcx, c.node);
-        changed = gen_poststate(fcx, a, c.id, o) || changed;
+        changed = gen_poststate(fcx, a, constr_id(c), o) || changed;
         ret changed;
     }
     case (expr_break(?a)) {

src/comp/middle/ty.rs

@@ -69,7 +69,7 @@ type ctxt = rec(@type_store ts,
                 session::session sess,
                 resolve::def_map def_map,
                 node_type_table node_types,
-                item_table items,
+                item_table items, // Only contains type items
                 type_cache tcache,
                 creader_cache rcache,
                 hashmap[t,str] short_names_cache,
@@ -1100,7 +1100,11 @@ fn hash_ty(&t typ) -> uint { ret typ; }
 // Type equality. This function is private to this module (and slow); external
 // users should use `eq_ty()` instead.
 
-fn arg_eq(@ast::constr_arg a, @ast::constr_arg b) -> bool {
+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 {
     alt (a.node) {
         case (ast::carg_base) {
             alt (b.node) {
@@ -1115,7 +1119,7 @@ fn arg_eq(@ast::constr_arg a, @ast::constr_arg b) -> bool {
         case (ast::carg_ident(?s)) {
             alt (b.node) {
                 case (ast::carg_ident(?t)) {
-                    ret (s == t);
+                    ret eq(s, t);
                 }
                 case (_) {
                     ret false;
@@ -1134,10 +1138,13 @@ fn arg_eq(@ast::constr_arg a, @ast::constr_arg b) -> bool {
         }
     }
 }
-fn args_eq(vec[@ast::constr_arg] a, vec[@ast::constr_arg] b) -> bool {
+
+fn args_eq[T](fn (&T, &T) -> bool eq,
+           vec[@ast::constr_arg_general[T]] a,
+           vec[@ast::constr_arg_general[T]] b) -> bool {
     let uint i = 0u;
-    for (@ast::constr_arg arg in a) {
+    for (@ast::constr_arg_general[T] arg in a) {
-        if (!arg_eq(arg, b.(i))) {
+        if (!arg_eq(eq, arg, b.(i))) {
             ret false;
         }
         i += 1u;
@@ -1148,7 +1155,7 @@ fn args_eq(vec[@ast::constr_arg] a, vec[@ast::constr_arg] b) -> bool {
 
 fn constr_eq(&@ast::constr c, &@ast::constr d) -> bool {
     ret path_to_str(c.node.path) == path_to_str(d.node.path) // FIXME: hack
-        && args_eq(c.node.args, d.node.args);
+        && args_eq(eq_int, c.node.args, d.node.args);
 }
 
 fn constrs_eq(&vec[@ast::constr] cs, &vec[@ast::constr] ds) -> bool {
@@ -2660,6 +2667,7 @@ fn substitute_type_params(&ctxt cx, vec[ty::t] substs, t typ) -> t {
     if (!type_contains_params(cx, typ)) { ret typ; }
 
     fn substituter(ctxt cx, vec[ty::t] substs, uint idx) -> t {
+        // FIXME: bounds check can fail
         ret substs.(idx);
     }
 
@@ -2775,27 +2783,6 @@ fn ret_ty_of_fn(ctxt cx, ast::ann ann) -> t {
     ret ret_ty_of_fn_ty(cx, ann_to_type(cx, ann));
 }
 
-fn lookup_fn_decl(ty_ctxt tcx, ast::ann ann)
-    -> option::t[tup(ast::fn_decl, ast::def_id)] {
-    auto nada = none[tup(ast::fn_decl, ast::def_id)];
-    alt (tcx.def_map.find(ann.id)) {
-        case (some(ast::def_fn(?d))) {
-            alt (tcx.items.find(d)) {
-                case (some(any_item_rust(?it))) {
-                    alt (it.node) {
-                        case (ast::item_fn(_,?f,_,_,_)) {
-                            ret some(tup(f.decl, d));
-                        }
-                        case (_) { ret nada; }
-                    }
-                }
-                case (_) { ret nada; }
-            }
-        }
-        case (_) { ret nada; }
-    }
-}
-
 // Local Variables:
 // mode: rust
 // fill-column: 78;

src/comp/middle/visit.rs

@@ -30,6 +30,7 @@ type visitor[E] =
          fn(&@decl d, &E e, &vt[E] v)          visit_decl,
          fn(&@expr ex, &E e, &vt[E] v)         visit_expr,
          fn(&@ty t, &E e, &vt[E] v)            visit_ty,
+         fn(&@constr c, &E e, &vt[E] v)        visit_constr,
          fn(&_fn f, &vec[ty_param] tp, &span sp, &ident name, &def_id d_id,
             &ann a, &E e, &vt[E] v)            visit_fn);
 
@@ -45,6 +46,7 @@ fn default_visitor[E]() -> visitor[E] {
              visit_decl = bind visit_decl[E](_, _, _),
              visit_expr = bind visit_expr[E](_, _, _),
              visit_ty = bind visit_ty[E](_, _, _),
+             visit_constr = bind visit_constr[E](_, _, _),
              visit_fn = bind visit_fn[E](_, _, _, _, _, _, _, _));
 }
 
@@ -153,10 +155,13 @@ fn visit_ty[E](&@ty t, &E e, &vt[E] v) {
                 vt(v).visit_ty(f.node.mt.ty, e, v);
             }
         }
-        case (ty_fn(_, ?args, ?out, _, _)) {
+        case (ty_fn(_, ?args, ?out, _, ?constrs)) {
             for (ty_arg a in args) {
                 vt(v).visit_ty(a.node.ty, e, v);
             }
+            for (@constr c in constrs) {
+                vt(v).visit_constr(c, e, v);
+            }
             vt(v).visit_ty(out, e, v);
         }
         case (ty_obj(?tmeths)) {
@@ -177,6 +182,10 @@ fn visit_ty[E](&@ty t, &E e, &vt[E] v) {
     }
 }
 
+fn visit_constr[E](&@constr c, &E e, &vt[E] v) {
+    // default
+}
+
 fn visit_pat[E](&@pat p, &E e, &vt[E] v) {
     alt (p.node) {
         case (pat_tag(?path, ?children, _)) {
@@ -200,6 +209,9 @@ fn visit_fn_decl[E](&fn_decl fd, &E e, &vt[E] v) {
     for (arg a in fd.inputs) {
         vt(v).visit_ty(a.ty, e, v);
     }
+    for (@constr c in fd.constraints) {
+        vt(v).visit_constr(c, e, v);
+    }
     vt(v).visit_ty(fd.output, e, v);
 }
 

src/comp/middle/walk.rs

@@ -36,6 +36,7 @@ type ast_visitor =
         fn (&@ast::expr e)              visit_expr_post,
         fn (&@ast::ty t)                visit_ty_pre,
         fn (&@ast::ty t)                visit_ty_post,
+        fn (&@ast::constr c)            visit_constr,
         fn (&ast::_fn f, &span sp, &ast::ident name, 
             &ast::def_id d_id, &ast::ann a)  visit_fn_pre,
         fn (&ast::_fn f, &span sp, &ast::ident name,
@@ -172,10 +173,13 @@ fn walk_ty(&ast_visitor v, @ast::ty t) {
                 walk_ty(v, f.node.mt.ty);
             }
         }
-        case (ast::ty_fn(_, ?args, ?out, _, _)) {
+        case (ast::ty_fn(_, ?args, ?out, _, ?constrs)) {
             for (ast::ty_arg a in args) {
                 walk_ty(v, a.node.ty);
             }
+            for (@ast::constr c in constrs) {
+                v.visit_constr(c);
+            }
             walk_ty(v, out);
         }
         case (ast::ty_obj(?tmeths)) {
@@ -240,6 +244,9 @@ fn walk_fn_decl(&ast_visitor v, &ast::fn_decl fd) {
     for (ast::arg a in fd.inputs) {
         walk_ty(v, a.ty);
     }
+    for (@ast::constr c in fd.constraints) {
+        v.visit_constr(c);
+    }
     walk_ty(v, fd.output);
 }
 
@@ -511,6 +518,7 @@ fn def_visit_pat(&@ast::pat p) { }
 fn def_visit_decl(&@ast::decl d) { }
 fn def_visit_expr(&@ast::expr e) { }
 fn def_visit_ty(&@ast::ty t) { }
+fn def_visit_constr(&@ast::constr c) { }
 fn def_visit_fn(&ast::_fn f, &span sp, &ast::ident i, &ast::def_id d,
                 &ast::ann a) { }
 
@@ -543,6 +551,7 @@ fn default_visitor() -> ast_visitor {
             visit_expr_post=def_visit_expr,
             visit_ty_pre=def_visit_ty,
             visit_ty_post=def_visit_ty,
+            visit_constr=def_visit_constr,
             visit_fn_pre=def_visit_fn,
             visit_fn_post=def_visit_fn);
 }

src/comp/pretty/ppaux.rs

@@ -181,7 +181,22 @@ fn ty_to_short_str(&ctxt cx, t typ) -> str {
     ret s;
 }
 
-fn constr_arg_to_str(&ast::constr_arg_ c) -> str {
+fn constr_arg_to_str[T](fn (&T) -> str f,
+                        &ast::constr_arg_general_[T] c) -> str {
+    alt (c) {
+        case (ast::carg_base) {
+            ret "*";
+        }
+        case (ast::carg_ident(?i)) {
+            ret f(i);
+        }
+        case (ast::carg_lit(?l)) {
+            ret lit_to_str(l);
+        }
+    }
+}
+
+fn constr_arg_to_str_1(&ast::constr_arg_general_[str] c) -> str {
     alt (c) {
         case (ast::carg_base) {
             ret "*";
@@ -195,18 +210,34 @@ fn constr_arg_to_str(&ast::constr_arg_ c) -> str {
     }
 }
 
-
+fn constr_args_to_str[T](fn (&T) -> str f, 
-fn constr_args_to_str(&vec[@constr_arg] args) -> str {
+                         &vec[@ast::constr_arg_general[T]] args) -> str {
     auto comma = false;
     auto s   = "(";
-    for (@constr_arg a in args) {
+    for (@ast::constr_arg_general[T] a in args) {
         if (comma) {
             s += ", ";
         }
         else {
             comma = true;
         }
-        s += constr_arg_to_str(a.node);
+        s += constr_arg_to_str[T](f, a.node);
+    }
+    s += ")";
+    ret s;
+}
+
+fn constr_args_to_str_1(&vec[@ast::constr_arg_use] args) -> str {
+    auto comma = false;
+    auto s   = "(";
+    for (@ast::constr_arg_use a in args) {
+        if (comma) {
+            s += ", ";
+        }
+        else {
+            comma = true;
+        }
+        s += constr_arg_to_str_1(a.node);
     }
     s += ")";
     ret s;
@@ -410,9 +441,16 @@ fn rust_printer(io::writer writer) -> ps {
 const uint indent_unit = 4u;
 const uint default_columns = 78u;
 
+// needed b/c constr_args_to_str needs
+// something that takes an alias
+// (argh)
+fn uint_to_str(&uint i) -> str {
+    ret util::common::uistr(i);
+}
+
 fn constr_to_str(&@ast::constr c) -> str {
   ret path_to_str(c.node.path)
-    + constr_args_to_str(c.node.args);
+      + constr_args_to_str(uint_to_str, c.node.args);
 }
 
 fn constrs_str(&vec[@ast::constr] constrs) -> str {