Serialize constraints in types (literal arguments still not supported)

This involved, in part, changing the ast::def type so that a def_fn
has a "purity" field. This lets the typechecker determine whether
functions defined in other crates are pure.

It also required updating some error messages in tests. As a test
for cross-crate constrained functions, I added a safe_slice function
to std::str (slice(), with one of the asserts replaced with a
function precondition) and some test cases (various versions of
fn-constraint.rs) that call it. Also, I changed "fn" to "pred" for
some of the boolean functions in std::uint.
This commit is contained in:
Tim Chevalier 2011-06-20 17:29:54 -07:00
parent 3b6d94d489
commit 7fb35ecf84
15 changed files with 147 additions and 113 deletions

View file

@ -27,7 +27,7 @@ fn local_def(node_id id) -> def_id {
type ty_param = ident;
tag def {
def_fn(def_id);
def_fn(def_id, purity);
def_obj(def_id);
def_obj_field(def_id);
def_mod(def_id);
@ -54,7 +54,7 @@ fn variant_def_ids(&def d) -> tup(def_id, def_id) {
fn def_id_of_def(def d) -> def_id {
alt (d) {
case (def_fn(?id)) { ret id; }
case (def_fn(?id,_)) { ret id; }
case (def_obj(?id)) { ret id; }
case (def_obj_field(?id)) { ret id; }
case (def_mod(?id)) { ret id; }

View file

@ -56,13 +56,22 @@ fn next(@pstate st) -> u8 {
}
fn parse_ident(@pstate st, str_def sd, char last) -> ast::ident {
fn is_last(char b, char c) -> bool {
ret c == b;
}
ret parse_ident_(st, sd, bind is_last(last, _));
}
fn parse_ident_(@pstate st, str_def sd, fn(char) -> bool is_last)
-> ast::ident {
auto res = "";
while (peek(st) as char != last) {
while (! is_last(peek(st) as char)) {
res += str::unsafe_from_byte(next(st));
}
ret res;
}
fn parse_ty_data(vec[u8] data, int crate_num, uint pos, uint len, str_def sd,
ty::ctxt tcx) -> ty::t {
auto st =
@ -85,40 +94,59 @@ fn parse_constrs(@pstate st, str_def sd) -> vec[@ty::constr_def] {
do {
auto ignore = next(st);
vec::push(res, parse_constr(st, sd));
} while (peek(st) as char == ',')
} while (peek(st) as char == ';')
}
case (_) { }
}
ret res;
}
fn parse_path(@pstate st, str_def sd) -> ast::path {
let vec[ast::ident] idents = [];
fn is_last(char c) -> bool {
ret (c == '(' || c == ':');
}
idents += [parse_ident_(st, sd, is_last)];
while (true) {
alt (peek(st) as char) {
case (':') {
auto ignore = next(st);
ignore = next(st);
}
case (?c) {
if (c == '(') {
ret respan(rec(lo=0u, hi=0u),
rec(idents=idents, types=[]));
}
else {
idents += [parse_ident_(st, sd, is_last)];
}
}
}
}
fail "parse_path: ill-formed path";
}
fn parse_constr(@pstate st, str_def sd) -> @ty::constr_def {
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 = [];
let vec[@ast::ty] tys = [];
let ast::path pth = respan(sp,
rec(idents=ids, types=tys)); // FIXME
let ast::ident p1 = parse_ident(st, sd, '(');
log_err("ignore=");
log_err(p1);
auto sp = rec(lo=0u,hi=0u); // FIXME: use a real span
let ast::path pth = parse_path(st, sd);
let char ignore = next(st) as char;
assert(ignore as char == '(');
auto def = parse_def(st, sd);
do {
alt (peek(st) as char) {
case ('*') {
auto ignore = next(st);
st.pos += 1u;
args += [@respan(sp, ast::carg_base)];
}
case (?c) {
log_err("c =");
log_err(str::from_bytes([c as u8]));
if (may_begin_ident(c)) {
auto id = parse_ident(st, sd, ',');
args += [@respan(sp, ast::carg_ident(id))];
/* how will we disambiguate between
an arg index and a lit argument? */
if (c >= '0' && c <= '9') {
// FIXME
args += [@respan(sp, ast::carg_ident((c as uint) - 48u))];
ignore = next(st) as char;
}
else {
log_err("Lit args are unimplemented");
@ -132,10 +160,10 @@ fn parse_constr(@pstate st, str_def sd) -> @ty::constr_def {
*/
}
}
} while (next(st) as char == ',');
ignore = next(st) as char;
*/
ignore = next(st) as char;
} while (ignore == ';');
assert(ignore == ')');
ret @respan(sp, rec(path=pth, args=args, id=def));
}
fn parse_ty(@pstate st, str_def sd) -> ty::t {
@ -333,7 +361,7 @@ fn parse_ty_fn(@pstate st, str_def sd) ->
}
inputs += [rec(mode=mode, ty=parse_ty(st, sd))];
}
st.pos = st.pos + 1u;
st.pos += 1u; // eat the ']'
auto cs = parse_constrs(st, sd);
auto res = parse_ty_or_bang(st, sd);
alt (res) {
@ -641,6 +669,7 @@ fn kind_has_type_params(u8 kind_ch) -> bool {
ret alt (kind_ch as char) {
case ('c') { false }
case ('f') { true }
case ('p') { true }
case ('F') { true }
case ('y') { true }
case ('o') { true }
@ -669,7 +698,8 @@ fn lookup_def(int cnum, vec[u8] data, &ast::def_id did_) -> ast::def {
auto def =
alt (kind_ch as char) {
case ('c') { ast::def_const(did) }
case ('f') { ast::def_fn(did) }
case ('f') { ast::def_fn(did, ast::impure_fn) }
case ('p') { ast::def_fn(did, ast::pure_fn) }
case ('F') { ast::def_native_fn(did) }
case ('y') { ast::def_ty(did) }
case ('o') { ast::def_obj(did) }
@ -781,6 +811,7 @@ fn item_kind_to_str(u8 kind) -> str {
alt (kind as char) {
case ('c') { ret "const"; }
case ('f') { ret "fn"; }
case ('p') { ret "pred"; }
case ('F') { ret "native fn"; }
case ('y') { ret "type"; }
case ('o') { ret "obj"; }

View file

@ -264,34 +264,37 @@ mod Encode {
enc_ty(w, cx, arg.ty);
}
w.write_char(']');
alt (cf) {
case (noreturn) { w.write_char('!'); }
case (_) { enc_ty(w, cx, out); }
}
auto colon = true;
for (@ty::constr_def c in constrs) {
if (colon) {
w.write_char(':');
colon = false;
} else { w.write_char(','); }
} else { w.write_char(';'); }
enc_constr(w, cx, c);
}
alt (cf) {
case (noreturn) { w.write_char('!'); }
case (_) { enc_ty(w, cx, out); }
}
}
fn enc_constr(&io::writer w, &@ctxt cx, &@ty::constr_def 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;
w.write_str(cx.ds(c.node.id));
w.write_char('|');
auto semi = false;
for (@constr_arg a in c.node.args) {
if (comma) { w.write_char(','); } else { comma = true; }
if (semi) { w.write_char(';'); } else { semi = true; }
alt (a.node) {
case (carg_base) { w.write_char('*'); }
case (carg_ident(?i)) { w.write_uint(i); }
case (carg_ident(?i)) {
w.write_uint(i);
}
case (carg_lit(?l)) { w.write_str(lit_to_str(l)); }
}
}
w.write_char(')');
}
}
@ -506,10 +509,12 @@ fn encode_info_for_item(@trans::crate_ctxt cx, &ebml::writer ebml_w,
encode_symbol(cx, ebml_w, item.id);
ebml::end_tag(ebml_w);
}
case (item_fn(_, ?tps)) {
case (item_fn(?fd, ?tps)) {
ebml::start_tag(ebml_w, tag_items_data_item);
encode_def_id(ebml_w, local_def(item.id));
encode_kind(ebml_w, 'f' as u8);
encode_kind(ebml_w, alt (fd.decl.purity) {
case (pure_fn) { 'p' }
case (impure_fn) { 'f' } } as u8);
encode_type_param_count(ebml_w, tps);
encode_type(cx, ebml_w, trans::node_id_type(cx, item.id));
encode_symbol(cx, ebml_w, item.id);

View file

@ -412,7 +412,7 @@ fn resolve_constr(@env e, node_id id, &@ast::constr c, &scopes sc,
lookup_path_strict(*e, sc, c.span, c.node.path.node.idents, ns_value);
if (option::is_some(new_def)) {
alt (option::get(new_def)) {
case (ast::def_fn(?pred_id)) {
case (ast::def_fn(?pred_id, _)) {
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_);
@ -799,9 +799,9 @@ fn found_def_item(&@ast::item i, namespace ns) -> option::t[def] {
ret some(ast::def_const(local_def(i.id)));
}
}
case (ast::item_fn(_, _)) {
case (ast::item_fn(?f, _)) {
if (ns == ns_value) {
ret some(ast::def_fn(local_def(i.id)));
ret some(ast::def_fn(local_def(i.id), f.decl.purity));
}
}
case (ast::item_mod(_)) {
@ -1122,7 +1122,7 @@ fn index_nmod(&ast::native_mod md) -> mod_index {
// External lookups
fn ns_for_def(def d) -> namespace {
ret alt (d) {
case (ast::def_fn(?id)) { ns_value }
case (ast::def_fn(?id, _)) { ns_value }
case (ast::def_obj(?id)) { ns_value }
case (ast::def_obj_field(?id)) { ns_value }
case (ast::def_mod(?id)) { ns_module }

View file

@ -4681,7 +4681,7 @@ fn trans_path(&@block_ctxt cx, &ast::path p, ast::node_id id) -> lval_result {
assert (cx.fcx.llobjfields.contains_key(did._1));
ret lval_mem(cx, cx.fcx.llobjfields.get(did._1));
}
case (ast::def_fn(?did)) {
case (ast::def_fn(?did, _)) {
auto tyt = ty::lookup_item_type(cx.fcx.lcx.ccx.tcx, did);
ret lval_generic_fn(cx, tyt, did, id);
}

View file

@ -537,7 +537,7 @@ fn node_id_for_constr(ty::ctxt tcx, node_id t) -> node_id {
case (none) {
tcx.sess.bug("node_id_for_constr: bad node_id " + istr(t));
}
case (some(def_fn(?i))) { ret i._1; }
case (some(def_fn(?i,_))) { ret i._1; }
case (_) {
tcx.sess.bug("node_id_for_constr: pred is not a function");
}

View file

@ -2610,7 +2610,7 @@ fn substitute_type_params(&ctxt cx, vec[ty::t] substs, t typ) -> t {
fn def_has_ty_params(&ast::def def) -> bool {
alt (def) {
case (ast::def_fn(_)) { ret true; }
case (ast::def_fn(_,_)) { ret true; }
case (ast::def_obj(_)) { ret true; }
case (ast::def_obj_field(_)) { ret false; }
case (ast::def_mod(_)) { ret false; }

View file

@ -48,13 +48,10 @@ import middle::tstate::ann::ts_ann;
type ty_table = hashmap[ast::def_id, ty::t];
type fn_purity_table = hashmap[ast::def_id, ast::purity];
type obj_info = rec(vec[ast::obj_field] obj_fields, ast::node_id this_obj);
type crate_ctxt =
rec(mutable vec[obj_info] obj_infos,
@fn_purity_table fn_purity_table,
ty::ctxt tcx);
type fn_ctxt =
@ -91,7 +88,9 @@ fn ty_param_count_and_ty_for_def(&@fn_ctxt fcx, &span sp, &ast::def defn) ->
auto typ = ty::mk_var(fcx.ccx.tcx, fcx.locals.get(id._1));
ret tup(0u, typ);
}
case (ast::def_fn(?id)) { ret ty::lookup_item_type(fcx.ccx.tcx, id); }
case (ast::def_fn(?id, _)) {
ret ty::lookup_item_type(fcx.ccx.tcx, id);
}
case (ast::def_native_fn(?id)) {
ret ty::lookup_item_type(fcx.ccx.tcx, id);
}
@ -1271,51 +1270,24 @@ fn require_impure(&session::session sess, &ast::purity f_purity, &span sp) {
}
}
fn get_function_purity(@crate_ctxt ccx, &ast::def_id d_id) -> ast::purity {
let option::t[ast::purity] o = ccx.fn_purity_table.find(d_id);
ret from_maybe[ast::purity](ast::impure_fn, o);
}
fn require_pure_call(@crate_ctxt ccx, &ast::purity caller_purity,
&@ast::expr callee, &span sp) {
alt (caller_purity) {
case (ast::impure_fn) { ret; }
case (ast::pure_fn) {
alt (callee.node) {
case (ast::expr_path(_)) {
auto d_id;
alt (ccx.tcx.def_map.get(callee.id)) {
case (ast::def_fn(?_d_id)) { d_id = _d_id; }
}
alt (get_function_purity(ccx, d_id)) {
case (ast::pure_fn) { ret; }
case (_) {
ccx.tcx.sess.span_fatal(sp,
"Pure function calls \
impure function");
}
}
alt (ccx.tcx.def_map.get(callee.id)) {
case (ast::def_fn(_, ast::pure_fn)) {
ret;
}
case (_) {
ccx.tcx.sess.span_fatal(sp,
"Pure function calls \
unknown function");
"Pure function calls function not known to be pure");
}
}
}
}
}
fn require_pure_function(@crate_ctxt ccx, &ast::def_id d_id, &span sp) {
alt (get_function_purity(ccx, d_id)) {
case (ast::impure_fn) {
ccx.tcx.sess.span_fatal(sp,
"Found non-predicate in check expression");
}
case (_) { ret; }
}
}
fn check_expr(&@fn_ctxt fcx, &@ast::expr expr) {
// fcx.ccx.tcx.sess.span_warn(expr.span, "typechecking expr " +
// pretty::pprust::expr_to_str(expr));
@ -1428,9 +1400,15 @@ fn check_expr(&@fn_ctxt fcx, &@ast::expr expr) {
case (ast::expr_call(?operator, ?operands)) {
alt (operator.node) {
case (ast::expr_path(?oper_name)) {
auto d_id;
alt (fcx.ccx.tcx.def_map.get(operator.id)) {
case (ast::def_fn(?_d_id)) { d_id = _d_id; }
case (ast::def_fn(?_d_id, ast::pure_fn)) {
// do nothing
}
case (_) {
fcx.ccx.tcx.sess.span_fatal(operator.span,
"non-predicate as operator \
in constraint");
}
}
for (@ast::expr operand in operands) {
if (!ast::is_constraint_arg(operand)) {
@ -1439,7 +1417,6 @@ fn check_expr(&@fn_ctxt fcx, &@ast::expr expr) {
fcx.ccx.tcx.sess.span_fatal(e.span, s);
}
}
require_pure_function(fcx.ccx, d_id, e.span);
}
case (_) {
auto s = "In a constraint, expected the \
@ -2193,14 +2170,15 @@ fn get_obj_info(&@crate_ctxt ccx) -> option::t[obj_info] {
fn ast_constr_to_constr(ty::ctxt tcx, &@ast::constr c)
-> @ty::constr_def {
alt (tcx.def_map.find(c.node.id)) {
case (some(ast::def_fn(?pred_id))) {
case (some(ast::def_fn(?pred_id, ast::pure_fn))) {
ret @respan(c.span, rec(path=c.node.path, args=c.node.args,
id=pred_id));
}
case (_) {
tcx.sess.span_fatal(c.span, "Predicate "
+ path_to_str(c.node.path)
+ " is unbound or bound to a non-function");
+ " is unbound or bound to a non-function or an\
impure function");
}
}
}
@ -2372,30 +2350,12 @@ fn check_item(@crate_ctxt ccx, &@ast::item it) {
}
}
fn mk_fn_purity_table(&@ast::crate crate) -> @fn_purity_table {
auto res = @new_def_hash[ast::purity]();
fn do_one(@fn_purity_table t, &@ast::item i) {
alt (i.node) {
case (ast::item_fn(?f, _)) {
t.insert(local_def(i.id), f.decl.purity);
}
case (_) { }
}
}
auto do_one_fn = bind do_one(res, _);
auto v = walk::default_visitor();
auto add_fn_entry_visitor = rec(visit_item_post=do_one_fn with v);
walk::walk_crate(add_fn_entry_visitor, *crate);
ret res;
}
fn check_crate(&ty::ctxt tcx, &@ast::crate crate) {
collect::collect_item_types(tcx, crate);
let vec[obj_info] obj_infos = [];
auto fpt = mk_fn_purity_table(crate); // use a variation on collect
auto ccx =
@rec(mutable obj_infos=obj_infos, fn_purity_table=fpt, tcx=tcx);
@rec(mutable obj_infos=obj_infos, tcx=tcx);
auto visit =
rec(visit_item_pre=bind check_item(ccx, _)
with walk::default_visitor());

View file

@ -1,6 +1,7 @@
import rustrt::sbuf;
import vec::rustrt::vbuf;
import uint::le;
export sbuf;
export rustrt;
export eq;
@ -45,6 +46,7 @@ export split;
export concat;
export connect;
export to_upper;
export safe_slice;
native "rust" mod rustrt {
type sbuf;
@ -381,6 +383,12 @@ fn slice(str s, uint begin, uint end) -> str {
ret rustrt::str_slice(s, begin, end);
}
fn safe_slice(str s, uint begin, uint end) : le(begin, end) -> str {
assert (end <= str::byte_len(s)); // would need some magic to
// make this a precondition
ret rustrt::str_slice(s, begin, end);
}
fn shift_byte(&mutable str s) -> u8 {
auto len = byte_len(s);
assert (len > 0u);

View file

@ -10,17 +10,17 @@ fn div(uint x, uint y) -> uint { ret x / y; }
fn rem(uint x, uint y) -> uint { ret x % y; }
fn lt(uint x, uint y) -> bool { ret x < y; }
pred lt(uint x, uint y) -> bool { ret x < y; }
fn le(uint x, uint y) -> bool { ret x <= y; }
pred le(uint x, uint y) -> bool { ret x <= y; }
fn eq(uint x, uint y) -> bool { ret x == y; }
pred eq(uint x, uint y) -> bool { ret x == y; }
fn ne(uint x, uint y) -> bool { ret x != y; }
pred ne(uint x, uint y) -> bool { ret x != y; }
fn ge(uint x, uint y) -> bool { ret x >= y; }
pred ge(uint x, uint y) -> bool { ret x >= y; }
fn gt(uint x, uint y) -> bool { ret x > y; }
pred gt(uint x, uint y) -> bool { ret x > y; }
fn max(uint x, uint y) -> uint { if (x > y) { ret x; } ret y; }

View file

@ -0,0 +1,9 @@
// error-pattern: Unsatisfied precondition constraint (for example, le(a, b)
use std;
import std::str::*;
fn main() {
let uint a = 4u;
let uint b = 1u;
log_err (safe_slice("kitties", a, b));
}

View file

@ -1,5 +1,5 @@
// -*- rust -*-
// error-pattern: impure function
// error-pattern: Pure function calls function not known to be pure
fn g() -> () {}

View file

@ -2,7 +2,7 @@
// error-pattern: Constraint args must be
fn f(int q) -> bool { ret true; }
pred f(int q) -> bool { ret true; }
fn main() {
// should fail to typecheck, as pred args must be slot variables or literals

View file

@ -0,0 +1,11 @@
// error-pattern:Predicate le(a, b) failed
use std;
import std::str::*;
import std::uint::le;
fn main() {
let uint a = 4u;
let uint b = 1u;
check le(a, b);
log_err (safe_slice("kitties", a, b));
}

View file

@ -0,0 +1,10 @@
use std;
import std::str::*;
import std::uint::*;
fn main() {
let uint a = 1u;
let uint b = 4u;
check le(a, b);
log (safe_slice("kitties", a, b));
}