From e3a68e235cd077c35654f79013ad54da46d72fee Mon Sep 17 00:00:00 2001 From: Tim Chevalier Date: Wed, 4 May 2011 11:28:13 -0700 Subject: Bring back "pred" syntax for writing predicates for check This commit reinstates the requirement that the predicate in a "check" must be a manifest call to a special kind of function declared with the new "pred" keyword instead of "fn". Preds must have a boolean return type and can only call other preds; they can't have any effects (as enforced by the typechecker). The arguments to a predicate in a check expression must be slot variables or literals. --- src/comp/front/ast.rs | 8 +++- src/comp/front/lexer.rs | 1 + src/comp/front/parser.rs | 32 ++++++++----- src/comp/front/token.rs | 2 + src/comp/middle/fold.rs | 13 +++--- src/comp/middle/typeck.rs | 112 ++++++++++++++++++++++++++++++++++++++++++++-- src/comp/pretty/pprust.rs | 9 +++- 7 files changed, 155 insertions(+), 22 deletions(-) (limited to 'src/comp') diff --git a/src/comp/front/ast.rs b/src/comp/front/ast.rs index cc7569e1..574ebd4a 100644 --- a/src/comp/front/ast.rs +++ b/src/comp/front/ast.rs @@ -346,7 +346,13 @@ type constr = spanned[constr_]; type arg = rec(mode mode, @ty ty, ident ident, def_id id); type fn_decl = rec(vec[arg] inputs, - @ty output); + @ty output, + purity purity); +tag purity { + pure_fn; // declared with "pred" + impure_fn; // declared with "fn" +} + type _fn = rec(fn_decl decl, proto proto, block body); diff --git a/src/comp/front/lexer.rs b/src/comp/front/lexer.rs index 9ef6ea27..4153533a 100644 --- a/src/comp/front/lexer.rs +++ b/src/comp/front/lexer.rs @@ -141,6 +141,7 @@ fn keyword_table() -> std.map.hashmap[str, token.token] { keywords.insert("auto", token.AUTO); keywords.insert("fn", token.FN); + keywords.insert("pred", token.PRED); keywords.insert("iter", token.ITER); keywords.insert("import", token.IMPORT); diff --git a/src/comp/front/parser.rs b/src/comp/front/parser.rs index 3ef16c71..e355290d 100644 --- a/src/comp/front/parser.rs +++ b/src/comp/front/parser.rs @@ -242,6 +242,7 @@ fn parse_proto(parser p) -> ast.proto { alt (p.peek()) { case (token.ITER) { p.bump(); ret ast.proto_iter; } case (token.FN) { p.bump(); ret ast.proto_fn; } + case (token.PRED) { p.bump(); ret ast.proto_fn; } case (?t) { unexpected(p, t); } } fail; @@ -1767,7 +1768,7 @@ fn parse_ty_params(parser p) -> vec[ast.ty_param] { ret ty_params; } -fn parse_fn_decl(parser p) -> ast.fn_decl { +fn parse_fn_decl(parser p, ast.purity purity) -> ast.fn_decl { auto pf = parse_arg; let util.common.spanned[vec[ast.arg]] inputs = // FIXME: passing parse_arg as an lval doesn't work at the @@ -1790,11 +1791,12 @@ fn parse_fn_decl(parser p) -> ast.fn_decl { } else { output = @spanned(inputs.span.lo, inputs.span.hi, ast.ty_nil); } - ret rec(inputs=inputs.node, output=output); + // FIXME + ret rec(inputs=inputs.node, output=output, purity=purity); } -fn parse_fn(parser p, ast.proto proto) -> ast._fn { - auto decl = parse_fn_decl(p); +fn parse_fn(parser p, ast.proto proto, ast.purity purity) -> ast._fn { + auto decl = parse_fn_decl(p, purity); auto body = parse_block(p); ret rec(decl = decl, proto = proto, @@ -1808,11 +1810,11 @@ fn parse_fn_header(parser p) ret tup(id, ty_params); } -fn parse_item_fn_or_iter(parser p) -> @ast.item { +fn parse_item_fn_or_iter(parser p, ast.purity purity) -> @ast.item { auto lo = p.get_lo_pos(); auto proto = parse_proto(p); auto t = parse_fn_header(p); - auto f = parse_fn(p, proto); + auto f = parse_fn(p, proto, purity); auto item = ast.item_fn(t._0, f, t._1, p.next_def_id(), ast.ann_none); ret @spanned(lo, f.body.span.hi, item); @@ -1830,7 +1832,7 @@ fn parse_method(parser p) -> @ast.method { auto lo = p.get_lo_pos(); auto proto = parse_proto(p); auto ident = parse_ident(p); - auto f = parse_fn(p, proto); + auto f = parse_fn(p, proto, ast.impure_fn); auto meth = rec(ident=ident, meth=f, id=p.next_def_id(), ann=ast.ann_none); ret @spanned(lo, f.body.span.hi, meth); @@ -1843,7 +1845,8 @@ fn parse_dtor(parser p) -> @ast.method { let vec[ast.arg] inputs = vec(); let @ast.ty output = @spanned(lo, lo, ast.ty_nil); let ast.fn_decl d = rec(inputs=inputs, - output=output); + output=output, + purity=ast.impure_fn); let ast._fn f = rec(decl = d, proto = ast.proto_fn, body = b); @@ -1946,7 +1949,7 @@ fn parse_item_native_fn(parser p) -> @ast.native_item { auto lo = p.get_lo_pos(); expect(p, token.FN); auto t = parse_fn_header(p); - auto decl = parse_fn_decl(p); + auto decl = parse_fn_decl(p, ast.impure_fn); auto link_name = none[str]; if (p.peek() == token.EQ) { p.bump(); @@ -2155,6 +2158,7 @@ fn peeking_at_item(parser p) -> bool { case (token.GC) { ret true; } case (token.CONST) { ret true; } case (token.FN) { ret true; } + case (token.PRED) { ret true; } case (token.ITER) { ret true; } case (token.MOD) { ret true; } case (token.TYPE) { ret true; } @@ -2176,11 +2180,17 @@ fn parse_item(parser p) -> @ast.item { case (token.FN) { assert (lyr == ast.layer_value); - ret parse_item_fn_or_iter(p); + ret parse_item_fn_or_iter(p, ast.impure_fn); } + + case (token.PRED) { + assert (lyr == ast.layer_value); + ret parse_item_fn_or_iter(p, ast.pure_fn); + } + case (token.ITER) { assert (lyr == ast.layer_value); - ret parse_item_fn_or_iter(p); + ret parse_item_fn_or_iter(p, ast.impure_fn); } case (token.MOD) { assert (lyr == ast.layer_value); diff --git a/src/comp/front/token.rs b/src/comp/front/token.rs index 594515f2..b0fa0588 100644 --- a/src/comp/front/token.rs +++ b/src/comp/front/token.rs @@ -156,6 +156,7 @@ tag token { /* Callable type constructors */ FN; + PRED; ITER; /* Object type and related keywords */ @@ -340,6 +341,7 @@ fn to_str(token t) -> str { /* Callable type constructors */ case (FN) { ret "fn"; } + case (PRED) { ret "pred"; } case (ITER) { ret "iter"; } /* Object type */ diff --git a/src/comp/middle/fold.rs b/src/comp/middle/fold.rs index 49b6290c..b37f7be8 100644 --- a/src/comp/middle/fold.rs +++ b/src/comp/middle/fold.rs @@ -30,6 +30,7 @@ import front.ast.def; import front.ast.def_id; import front.ast.ann; import front.ast.mt; +import front.ast.purity; import std._uint; import std._vec; @@ -301,7 +302,8 @@ type ast_fold[ENV] = (fn(&ENV e, vec[arg] inputs, - @ty output) -> ast.fn_decl) fold_fn_decl, + @ty output, + purity p) -> ast.fn_decl) fold_fn_decl, (fn(&ENV e, &ast._mod m) -> ast._mod) fold_mod, @@ -900,7 +902,7 @@ fn fold_fn_decl[ENV](&ENV env, ast_fold[ENV] fld, inputs += vec(fold_arg(env, fld, a)); } auto output = fold_ty[ENV](env, fld, decl.output); - ret fld.fold_fn_decl(env, inputs, output); + ret fld.fold_fn_decl(env, inputs, output, decl.purity); } fn fold_fn[ENV](&ENV env, ast_fold[ENV] fld, &ast._fn f) -> ast._fn { @@ -1542,8 +1544,9 @@ fn identity_fold_block[ENV](&ENV e, &span sp, &ast.block_ blk) -> block { fn identity_fold_fn_decl[ENV](&ENV e, vec[arg] inputs, - @ty output) -> ast.fn_decl { - ret rec(inputs=inputs, output=output); + @ty output, + purity p) -> ast.fn_decl { + ret rec(inputs=inputs, output=output, purity=p); } fn identity_fold_fn[ENV](&ENV e, @@ -1732,7 +1735,7 @@ fn new_identity_fold[ENV]() -> ast_fold[ENV] { fold_ann = bind identity_fold_ann[ENV](_,_), fold_fn = bind identity_fold_fn[ENV](_,_,_,_), - fold_fn_decl = bind identity_fold_fn_decl[ENV](_,_,_), + fold_fn_decl = bind identity_fold_fn_decl[ENV](_,_,_,_), fold_mod = bind identity_fold_mod[ENV](_,_), fold_native_mod = bind identity_fold_native_mod[ENV](_,_), fold_crate = bind identity_fold_crate[ENV](_,_,_,_), diff --git a/src/comp/middle/typeck.rs b/src/comp/middle/typeck.rs index e693fdf7..4cea077f 100644 --- a/src/comp/middle/typeck.rs +++ b/src/comp/middle/typeck.rs @@ -8,7 +8,7 @@ import driver.session; import util.common; import util.common.span; import util.common.plain_ann; - +import util.common.new_def_hash; import util.common.log_expr_err; import middle.ty; @@ -40,6 +40,7 @@ import std.map.hashmap; import std.option; import std.option.none; import std.option.some; +import std.option.from_maybe; import pretty.pprust; @@ -53,6 +54,7 @@ tag any_item { } type ty_item_table = hashmap[ast.def_id,any_item]; +type fn_purity_table = hashmap[ast.def_id, ast.purity]; type unify_cache_entry = tup(ty.t,ty.t,vec[mutable ty.t]); type unify_cache = hashmap[unify_cache_entry,ty.Unify.result]; @@ -62,6 +64,7 @@ type crate_ctxt = rec(session.session sess, @ty_item_table item_items, vec[ast.obj_field] obj_fields, option.t[ast.def_id] this_obj, + @fn_purity_table fn_purity_table, mutable int next_var_id, unify_cache unify_cache, mutable uint cache_hits, @@ -69,6 +72,7 @@ type crate_ctxt = rec(session.session sess, ty.ctxt tcx); type fn_ctxt = rec(ty.t ret_ty, + ast.purity purity, @ty_table locals, @crate_ctxt ccx); @@ -1673,6 +1677,62 @@ fn check_pat(&@fn_ctxt fcx, @ast.pat pat) -> @ast.pat { ret @fold.respan[ast.pat_](pat.span, new_pat); } +fn require_impure(&session.session sess, + &ast.purity f_purity, &span sp) -> () { + alt (f_purity) { + case (ast.impure_fn) { + ret; + } + case (ast.pure_fn) { + sess.span_err(sp, + "Found impure expression in pure function decl"); + } + } +} + +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(_, some[ast.def](ast.def_fn(?d_id)), _)) { + alt (get_function_purity(ccx, d_id)) { + case (ast.pure_fn) { + ret; + } + case (_) { + ccx.sess.span_err(sp, + "Pure function calls impure function"); + + } + } + } + case (_) { + ccx.sess.span_err(sp, + "Pure function calls unknown function"); + } + } + } + } +} + +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.sess.span_err(sp, "Found non-predicate in check expression"); + } + case (_) { ret; } + } +} + fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr { //fcx.ccx.sess.span_warn(expr.span, "typechecking expr " + // pretty.pprust.expr_to_str(expr)); @@ -1916,6 +1976,8 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr { } case (ast.expr_put(?expr_opt, _)) { + require_impure(fcx.ccx.sess, fcx.purity, expr.span); + alt (expr_opt) { case (none[@ast.expr]) { auto nil = ty.mk_nil(fcx.ccx.tcx); @@ -1965,7 +2027,8 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr { alt (e.node) { case (ast.expr_call(?operator, ?operands, _)) { alt (operator.node) { - case (ast.expr_path(?oper_name, ?d_id, _)) { + case (ast.expr_path(?oper_name, + some[ast.def](ast.def_fn(?d_id)), _)) { for (@ast.expr operand in operands) { if (! ast.is_constraint_arg(operand)) { @@ -1975,8 +2038,8 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr { } } - /* operator must be a pure function */ - /* FIXME: need more checking */ + require_pure_function(fcx.ccx, d_id, expr.span); + ret @fold.respan[ast.expr_] (expr.span, ast.expr_check(expr_t, plain_ann(fcx.ccx.tcx))); @@ -2005,6 +2068,8 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr { } case (ast.expr_assign(?lhs, ?rhs, _)) { + require_impure(fcx.ccx.sess, fcx.purity, expr.span); + auto checked = check_assignment(fcx, lhs, rhs); auto newexpr = ast.expr_assign(checked._0, checked._1, @@ -2013,6 +2078,8 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr { } case (ast.expr_assign_op(?op, ?lhs, ?rhs, _)) { + require_impure(fcx.ccx.sess, fcx.purity, expr.span); + auto checked = check_assignment(fcx, lhs, rhs); auto newexpr = ast.expr_assign_op(op, checked._0, @@ -2022,6 +2089,8 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr { } case (ast.expr_send(?lhs, ?rhs, _)) { + require_impure(fcx.ccx.sess, fcx.purity, expr.span); + auto lhs_0 = check_expr(fcx, lhs); auto rhs_0 = check_expr(fcx, rhs); auto rhs_t = expr_ty(fcx.ccx.tcx, rhs_0); @@ -2045,6 +2114,8 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr { } case (ast.expr_recv(?lhs, ?rhs, _)) { + require_impure(fcx.ccx.sess, fcx.purity, expr.span); + auto lhs_0 = check_expr(fcx, lhs); auto rhs_0 = check_expr(fcx, rhs); auto lhs_t1 = expr_ty(fcx.ccx.tcx, lhs_0); @@ -2250,6 +2321,12 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr { } case (ast.expr_call(?f, ?args, _)) { + /* here we're kind of hosed, as f can be any expr + need to restrict it to being an explicit expr_path if we're + inside a pure function, and need an environment mapping from + function name onto purity-designation */ + require_pure_call(fcx.ccx, fcx.purity, f, expr.span); + auto result = check_call(fcx, f, args); auto f_1 = result._0; auto args_1 = result._1; @@ -2302,6 +2379,8 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr { auto ann = triv_ann(t); + require_impure(fcx.ccx.sess, fcx.purity, expr.span); + ret @fold.respan[ast.expr_](expr.span, ast.expr_self_method(id, ann)); } @@ -2725,6 +2804,7 @@ fn check_const(&@crate_ctxt ccx, &span sp, ast.ident ident, @ast.ty t, // for checking the initializer expression. auto rty = ann_to_type(ann); let @fn_ctxt fcx = @rec(ret_ty = rty, + purity = ast.pure_fn, locals = @common.new_def_hash[ty.t](), ccx = ccx); auto e_ = check_expr(fcx, e); @@ -2755,6 +2835,7 @@ fn check_fn(&@crate_ctxt ccx, &ast.fn_decl decl, ast.proto proto, } let @fn_ctxt fcx = @rec(ret_ty = ast_ty_to_ty_crate(ccx, decl.output), + purity = decl.purity, locals = local_ty_table, ccx = ccx); @@ -2834,6 +2915,26 @@ fn eq_unify_cache_entry(&unify_cache_entry a, &unify_cache_entry b) -> bool { ret true; } +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, _, ?d_id, _)) { + t.insert(d_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; +} type typecheck_result = tup(@ast.crate, ty.type_cache); @@ -2848,12 +2949,15 @@ fn check_crate(ty.ctxt tcx, @ast.crate crate) auto eqer = eq_unify_cache_entry; auto unify_cache = map.mk_hashmap[unify_cache_entry,ty.Unify.result](hasher, eqer); + auto fpt = + mk_fn_purity_table(crate); // use a variation on Collect auto ccx = @rec(sess=sess, type_cache=result._1, item_items=result._2, obj_fields=fields, this_obj=none[ast.def_id], + fn_purity_table = fpt, mutable next_var_id=0, unify_cache=unify_cache, mutable cache_hits=0u, diff --git a/src/comp/pretty/pprust.rs b/src/comp/pretty/pprust.rs index 62e6594b..c87a8679 100644 --- a/src/comp/pretty/pprust.rs +++ b/src/comp/pretty/pprust.rs @@ -790,7 +790,14 @@ fn print_pat(ps s, &@ast.pat pat) { fn print_fn(ps s, ast.fn_decl decl, str name, vec[ast.ty_param] typarams) { - wrd1(s, "fn"); + alt (decl.purity) { + case (ast.impure_fn) { + wrd1(s, "fn"); + } + case (_) { + wrd1(s, "pred"); + } + } wrd(s.s, name); print_type_params(s, typarams); popen(s); -- cgit v1.2.3