From fa85324c2cbf9539ab2138c117f1f8c3b372488b Mon Sep 17 00:00:00 2001 From: Tim Chevalier Date: Mon, 2 May 2011 12:16:29 -0700 Subject: [PATCH 01/10] Un-XFAILed not-a-pred in stage0 (it fails correctly) --- src/test/compile-fail/not-a-pred.rs | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/test/compile-fail/not-a-pred.rs b/src/test/compile-fail/not-a-pred.rs index fe58114a69bc4..4a899512e31ea 100644 --- a/src/test/compile-fail/not-a-pred.rs +++ b/src/test/compile-fail/not-a-pred.rs @@ -1,6 +1,3 @@ -// xfail-stage0 -// xfail-stage1 -// xfail-stage2 // -*- rust -*- // error-pattern: mismatched types From 7878e6f89f99d6ff2618a411bf8fed522e387937 Mon Sep 17 00:00:00 2001 From: Tim Chevalier Date: Mon, 2 May 2011 13:47:41 -0700 Subject: [PATCH 02/10] Check that the operand in a check is a call In addition, fix bug in fold that was turning asserts into checks. More typechecking still needs to be done. --- src/comp/middle/fold.rs | 2 +- src/comp/middle/typeck.rs | 25 ++++++++++++++++++------- src/test/compile-fail/not-a-pred-2.rs | 9 +++++++++ 3 files changed, 28 insertions(+), 8 deletions(-) create mode 100644 src/test/compile-fail/not-a-pred-2.rs diff --git a/src/comp/middle/fold.rs b/src/comp/middle/fold.rs index e932fd9af497c..49b6290cfba5b 100644 --- a/src/comp/middle/fold.rs +++ b/src/comp/middle/fold.rs @@ -1396,7 +1396,7 @@ fn identity_fold_expr_check[ENV](&ENV e, &span sp, @expr x, ann a) fn identity_fold_expr_assert[ENV](&ENV e, &span sp, @expr x, ann a) -> @expr { - ret @respan(sp, ast.expr_check(x, a)); + ret @respan(sp, ast.expr_assert(x, a)); } fn identity_fold_expr_port[ENV](&ENV e, &span sp, ann a) -> @expr { diff --git a/src/comp/middle/typeck.rs b/src/comp/middle/typeck.rs index 094b7e1f0ee99..5c4fc574e1e39 100644 --- a/src/comp/middle/typeck.rs +++ b/src/comp/middle/typeck.rs @@ -9,6 +9,8 @@ import util.common; import util.common.span; import util.common.plain_ann; +import util.common.log_expr_err; + import middle.ty; import middle.ty.ann_to_type; import middle.ty.arg; @@ -1955,16 +1957,25 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr { } case (ast.expr_check(?e, _)) { - /* FIXME */ - /* presumably, here is where we should check that e is - actually a call to a predicate, where all the arguments - are literals or slot variables? */ auto expr_t = check_expr(fcx, e); Demand.simple(fcx, expr.span, ty.mk_bool(fcx.ccx.tcx), expr_ty(fcx.ccx.tcx, expr_t)); - ret @fold.respan[ast.expr_] - (expr.span, ast.expr_check(expr_t, - plain_ann(fcx.ccx.tcx))); + /* e must be a call expr where all arguments are either + literals or slots */ + alt (e.node) { + case (ast.expr_call(?operator, ?operands, _)) { + /* operator must be a pure function */ + /* FIXME: need more checking */ + ret @fold.respan[ast.expr_] + (expr.span, ast.expr_check(expr_t, + plain_ann(fcx.ccx.tcx))); + + } + case (_) { + fcx.ccx.sess.span_err(expr.span, + "Check on non-predicate"); + } + } } case (ast.expr_assert(?e, _)) { diff --git a/src/test/compile-fail/not-a-pred-2.rs b/src/test/compile-fail/not-a-pred-2.rs new file mode 100644 index 0000000000000..c8ac4a08adb3c --- /dev/null +++ b/src/test/compile-fail/not-a-pred-2.rs @@ -0,0 +1,9 @@ +// -*- rust -*- +// xfail-boot + +// error-pattern: non-predicate + +fn main() { + check (1 == 2); // should fail to typecheck, as (a == b) + // is not a manifest call +} From b11df3e5b3f6ea60d720ccf5bf226d5bc887f2e3 Mon Sep 17 00:00:00 2001 From: Tim Chevalier Date: Mon, 2 May 2011 13:50:34 -0700 Subject: [PATCH 03/10] Change checks to asserts in test/bench files --- src/test/bench/shootout/ackermann.rs | 8 ++++---- src/test/bench/shootout/fibo.rs | 4 ++-- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/test/bench/shootout/ackermann.rs b/src/test/bench/shootout/ackermann.rs index 27b4c3c05a7b7..7eaf84ce2f11d 100644 --- a/src/test/bench/shootout/ackermann.rs +++ b/src/test/bench/shootout/ackermann.rs @@ -13,13 +13,13 @@ fn ack(int m, int n) -> int { } fn main() { - check (ack(0,0) == 1); - check (ack(3,2) == 29); - check (ack(3,4) == 125); + assert (ack(0,0) == 1); + assert (ack(3,2) == 29); + assert (ack(3,4) == 125); // This takes a while; but a comparison may amuse: on win32 at least, the // posted C version of the 'benchmark' running ack(4,1) overruns its stack // segment and crashes. We just grow our stack (to 4mb) as we go. - // check (ack(4,1) == 65533); + // assert (ack(4,1) == 65533); } \ No newline at end of file diff --git a/src/test/bench/shootout/fibo.rs b/src/test/bench/shootout/fibo.rs index 9045f3815b3f2..8fc95f895c2ba 100644 --- a/src/test/bench/shootout/fibo.rs +++ b/src/test/bench/shootout/fibo.rs @@ -15,8 +15,8 @@ fn fib(int n) -> int { } fn main() { - check (fib(8) == 21); - check (fib(15) == 610); + assert (fib(8) == 21); + assert (fib(15) == 610); log fib(8); log fib(15); } From 49e6203aee2a3b98586353bb9c99eb3fa8ecfe05 Mon Sep 17 00:00:00 2001 From: Tim Chevalier Date: Mon, 2 May 2011 14:28:35 -0700 Subject: [PATCH 04/10] Check well-formedness of constraints Check that the operand in a constraint is an explicit name, and that the operands are all local variables or literals. Still need to check that the name refers to a pure function. --- src/comp/front/ast.rs | 14 +++++++++++++ src/comp/middle/typeck.rs | 29 ++++++++++++++++++++------ src/test/compile-fail/not-a-pred-3.rs | 15 +++++++++++++ src/test/compile-fail/not-pred-args.rs | 11 ++++++++++ 4 files changed, 63 insertions(+), 6 deletions(-) create mode 100644 src/test/compile-fail/not-a-pred-3.rs create mode 100644 src/test/compile-fail/not-pred-args.rs diff --git a/src/comp/front/ast.rs b/src/comp/front/ast.rs index 1f123f748647c..cc7569e16b769 100644 --- a/src/comp/front/ast.rs +++ b/src/comp/front/ast.rs @@ -563,6 +563,20 @@ fn is_call_expr(@expr e) -> bool { } } +fn is_constraint_arg(@expr e) -> bool { + alt (e.node) { + case (expr_lit(_,_)) { + ret true; + } + case (expr_path(_, option.some[def](def_local(_)), _)) { + ret true; + } + case (_) { + ret false; + } + } +} + // // Local Variables: // mode: rust diff --git a/src/comp/middle/typeck.rs b/src/comp/middle/typeck.rs index 5c4fc574e1e39..27cdfc3476585 100644 --- a/src/comp/middle/typeck.rs +++ b/src/comp/middle/typeck.rs @@ -1964,12 +1964,29 @@ fn check_expr(&@fn_ctxt fcx, @ast.expr expr) -> @ast.expr { literals or slots */ alt (e.node) { case (ast.expr_call(?operator, ?operands, _)) { - /* operator must be a pure function */ - /* FIXME: need more checking */ - ret @fold.respan[ast.expr_] - (expr.span, ast.expr_check(expr_t, - plain_ann(fcx.ccx.tcx))); - + alt (operator.node) { + case (ast.expr_path(?oper_name, ?d_id, _)) { + + for (@ast.expr operand in operands) { + if (! ast.is_constraint_arg(operand)) { + fcx.ccx.sess.span_err(expr.span, + "Constraint args must be " + + "slot variables or literals"); + } + } + + /* operator must be a pure function */ + /* FIXME: need more checking */ + ret @fold.respan[ast.expr_] + (expr.span, ast.expr_check(expr_t, + plain_ann(fcx.ccx.tcx))); + } + case (_) { + fcx.ccx.sess.span_err(expr.span, + "In a constraint, expected the constraint name " + + "to be an explicit name"); + } + } } case (_) { fcx.ccx.sess.span_err(expr.span, diff --git a/src/test/compile-fail/not-a-pred-3.rs b/src/test/compile-fail/not-a-pred-3.rs new file mode 100644 index 0000000000000..ea1b6cc096571 --- /dev/null +++ b/src/test/compile-fail/not-a-pred-3.rs @@ -0,0 +1,15 @@ +// -*- rust -*- +// xfail-boot + +// error-pattern: expected the constraint name + +obj f () { + fn g (int q) -> bool { + ret true; + } +} + +fn main() { + auto z = f (); + check (z.g)(42); // should fail to typecheck, as z.g isn't an explicit name +} diff --git a/src/test/compile-fail/not-pred-args.rs b/src/test/compile-fail/not-pred-args.rs new file mode 100644 index 0000000000000..c92b4ff9cae4d --- /dev/null +++ b/src/test/compile-fail/not-pred-args.rs @@ -0,0 +1,11 @@ +// -*- rust -*- +// xfail-boot + +// error-pattern: Constraint args must be + +fn f(int q) -> bool { ret true; } + +fn main() { +// should fail to typecheck, as pred args must be slot variables or literals + check f(42 * 17); +} From 1715910db1617031fdfb7ae67585eea67502ef7d Mon Sep 17 00:00:00 2001 From: Tim Chevalier Date: Wed, 4 May 2011 10:55:32 -0700 Subject: [PATCH 05/10] add dl/ and .pyc files to .gitignore --- .gitignore | 3 +++ 1 file changed, 3 insertions(+) diff --git a/.gitignore b/.gitignore index 184f140273cfd..bb34977fd203f 100644 --- a/.gitignore +++ b/.gitignore @@ -34,6 +34,7 @@ *.vr *.swp *.tmp +*.pyc .hg/ .hgignore .cproject @@ -53,3 +54,5 @@ config.mk /build/ src/.DS_Store /stage0/ +/dl/ + From a5ffdb40217fbbaa5c3a954741688d4c2aec799c Mon Sep 17 00:00:00 2001 From: Tim Chevalier Date: Wed, 4 May 2011 11:01:47 -0700 Subject: [PATCH 06/10] Update docs to reflect assert vs. check Also added the --batch flag to texi2pdf, as it doesn't really ever seem useful to drop to the TeX prompt during a build. --- doc/rust.texi | 29 +++++++++++++++++++++-------- mk/docs.mk | 2 +- 2 files changed, 22 insertions(+), 9 deletions(-) diff --git a/doc/rust.texi b/doc/rust.texi index e7860a9305e98..1404e9ca5b38c 100644 --- a/doc/rust.texi +++ b/doc/rust.texi @@ -683,6 +683,7 @@ The keywords are: @item @code{auth} @tab @code{unsafe} @tab @code{self} +@tab @code{log} @item @code{bind} @tab @code{type} @tab @code{true} @@ -727,12 +728,12 @@ The keywords are: @tab @code{while} @tab @code{break} @tab @code{cont} -@tab @code{fail} -@item @code{log} @tab @code{note} +@item @code{assert} @tab @code{claim} @tab @code{check} @tab @code{prove} +@tab @code{fail} @item @code{for} @tab @code{each} @tab @code{ret} @@ -1395,7 +1396,7 @@ An example of an implicit-dereference operation performed on box values: @example let @@int x = @@10; let @@int y = @@12; -check (x + y == 22); +assert (x + y == 22); @end example Other operations act on box values as single-word-sized address values, @@ -1887,7 +1888,7 @@ let counter c = counter(1); c.incr(); c.incr(); -check (c.get() == 3); +assert (c.get() == 3); @end example There is no @emph{this} or @emph{self} available inside an object's @@ -2232,9 +2233,9 @@ An example of a tuple type and its use: @example type pair = tup(int,str); let pair p = tup(10,"hello"); -check (p._0 == 10); +assert (p._0 == 10); p._1 = "world"; -check (p._1 == "world"); +assert (p._1 == "world"); @end example @@ -2898,6 +2899,8 @@ effects of the expression's evaluation. * Ref.Expr.Alt:: Expression for complex conditional branching. * Ref.Expr.Prove:: Expression for static assertion of typestate. * Ref.Expr.Check:: Expression for dynamic assertion of typestate. +* Ref.Expr.Assert:: Expression for halting the program if a + boolean condition fails to hold. * Ref.Expr.IfCheck:: Expression for dynamic testing of typestate. @end menu @@ -3068,8 +3071,8 @@ let single_param_fn add4 = bind add(4, _); let single_param_fn add5 = bind add(_, 5); -check (add(4,5) == add4(5)); -check (add(4,5) == add5(4)); +assert (add(4,5) == add4(5)); +assert (add(4,5) == add5(4)); @end example @@ -3592,6 +3595,16 @@ if check even(x) @{ @} @end example +@node Ref.Expr.Assert +@subsection Ref.Expr.Assert +@c * Ref.Expr.Assert:: Expression that halts the program if a boolean condition fails to hold. +@cindex Assertions + +An @code{assert} expression is similar to a @code{check} expression, except +the condition may be any boolean-typed expression, and the compiler makes no +use of the knowledge that the condition holds if the program continues to +execute after the @code{assert}. + @page @node Ref.Run @section Ref.Run diff --git a/mk/docs.mk b/mk/docs.mk index ba00f57cdf63a..6e78ebe4352d2 100644 --- a/mk/docs.mk +++ b/mk/docs.mk @@ -7,7 +7,7 @@ doc/version.texi: $(MKFILES) rust.texi --pretty=format:'@macro gitversion%n%h %ci%n@end macro%n') >$@ doc/%.pdf: %.texi doc/version.texi - texi2pdf -I doc -o $@ --clean $< + texi2pdf --batch -I doc -o $@ --clean $< doc/%.html: %.texi doc/version.texi makeinfo -I doc --html --ifhtml --force --no-split --output=$@ $< From 25893f2c77333f780fe97048a199d8c9d725f5ba Mon Sep 17 00:00:00 2001 From: Tim Chevalier Date: Wed, 4 May 2011 11:28:13 -0700 Subject: [PATCH 07/10] 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(-) diff --git a/src/comp/front/ast.rs b/src/comp/front/ast.rs index cc7569e16b769..574ebd4a63c54 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 dabdee1c7389a..c78a0593da14c 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 e7a86d6efed1d..005f85c513517 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; @@ -1760,7 +1761,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 @@ -1783,11 +1784,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, @@ -1801,11 +1803,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); @@ -1823,7 +1825,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); @@ -1836,7 +1838,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); @@ -1939,7 +1942,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(); @@ -2148,6 +2151,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; } @@ -2169,11 +2173,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 594515f22141e..b0fa0588cfaae 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 49b6290cfba5b..b37f7be835ec6 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 27cdfc3476585..b0b223ab6e5fd 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 62e6594b62748..c87a86796ff48 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); From acb7131e2c0127f069f65fe1ab189dd842fb6804 Mon Sep 17 00:00:00 2001 From: Tim Chevalier Date: Wed, 4 May 2011 11:32:06 -0700 Subject: [PATCH 08/10] Test cases for pred / check stuff --- src/test/compile-fail/impure-pred.rs | 17 +++++++++++++++++ src/test/compile-fail/not-a-pred-2.rs | 1 + src/test/compile-fail/not-a-pred-3.rs | 1 + src/test/compile-fail/not-a-pred-check.rs | 12 ++++++++++++ src/test/compile-fail/not-pred-args.rs | 1 + src/test/compile-fail/pred-not-bool.rs | 13 +++++++++++++ src/test/run-pass/pred-check.rs | 11 +++++++++++ src/test/run-pass/pred.rs | 4 +--- 8 files changed, 57 insertions(+), 3 deletions(-) create mode 100644 src/test/compile-fail/impure-pred.rs create mode 100644 src/test/compile-fail/not-a-pred-check.rs create mode 100644 src/test/compile-fail/pred-not-bool.rs create mode 100644 src/test/run-pass/pred-check.rs diff --git a/src/test/compile-fail/impure-pred.rs b/src/test/compile-fail/impure-pred.rs new file mode 100644 index 0000000000000..b5ebc10e72f2e --- /dev/null +++ b/src/test/compile-fail/impure-pred.rs @@ -0,0 +1,17 @@ +// -*- rust -*- +// xfail-boot +// xfail-stage0 +// error-pattern: impure function + +fn g() -> () {} + +pred f(int q) -> bool { + g(); + ret true; +} + +fn main() { + auto x = 0; + + check f(x); +} diff --git a/src/test/compile-fail/not-a-pred-2.rs b/src/test/compile-fail/not-a-pred-2.rs index c8ac4a08adb3c..07ea13b35eb4e 100644 --- a/src/test/compile-fail/not-a-pred-2.rs +++ b/src/test/compile-fail/not-a-pred-2.rs @@ -1,5 +1,6 @@ // -*- rust -*- // xfail-boot +// xfail-stage0 // error-pattern: non-predicate diff --git a/src/test/compile-fail/not-a-pred-3.rs b/src/test/compile-fail/not-a-pred-3.rs index ea1b6cc096571..f4dafd204d797 100644 --- a/src/test/compile-fail/not-a-pred-3.rs +++ b/src/test/compile-fail/not-a-pred-3.rs @@ -1,5 +1,6 @@ // -*- rust -*- // xfail-boot +// xfail-stage0 // error-pattern: expected the constraint name diff --git a/src/test/compile-fail/not-a-pred-check.rs b/src/test/compile-fail/not-a-pred-check.rs new file mode 100644 index 0000000000000..55698ad26414d --- /dev/null +++ b/src/test/compile-fail/not-a-pred-check.rs @@ -0,0 +1,12 @@ +// -*- rust -*- +// xfail-boot +// xfail-stage0 +// error-pattern: non-predicate + +fn f(int q) -> bool { ret true; } + +fn main() { + auto x = 0; + + check f(x); +} diff --git a/src/test/compile-fail/not-pred-args.rs b/src/test/compile-fail/not-pred-args.rs index c92b4ff9cae4d..7fe6220ad98f3 100644 --- a/src/test/compile-fail/not-pred-args.rs +++ b/src/test/compile-fail/not-pred-args.rs @@ -1,5 +1,6 @@ // -*- rust -*- // xfail-boot +// xfail-stage0 // error-pattern: Constraint args must be diff --git a/src/test/compile-fail/pred-not-bool.rs b/src/test/compile-fail/pred-not-bool.rs new file mode 100644 index 0000000000000..c0d19ef2c9fc1 --- /dev/null +++ b/src/test/compile-fail/pred-not-bool.rs @@ -0,0 +1,13 @@ +// -*- rust -*- + +// error-pattern: mismatched types + +// this checks that a pred with a non-bool return +// type is rejected, even if the pred is never used + +pred bad(int a) -> int { + ret 37; +} + +fn main() { +} diff --git a/src/test/run-pass/pred-check.rs b/src/test/run-pass/pred-check.rs new file mode 100644 index 0000000000000..e099756469baa --- /dev/null +++ b/src/test/run-pass/pred-check.rs @@ -0,0 +1,11 @@ +// -*- rust -*- +// xfail-boot +// xfail-stage0 + +pred f(int q) -> bool { ret true; } + +fn main() { + auto x = 0; + + check f(x); +} diff --git a/src/test/run-pass/pred.rs b/src/test/run-pass/pred.rs index 022e1fc4f8a2e..b4d003a877407 100644 --- a/src/test/run-pass/pred.rs +++ b/src/test/run-pass/pred.rs @@ -1,12 +1,10 @@ // xfail-stage0 -// xfail-stage1 -// xfail-stage2 // -*- rust -*- fn f(int a, int b) : lt(a,b) { } -fn lt(int a, int b) -> bool { +pred lt(int a, int b) -> bool { ret a < b; } From 08ed05a1c0a157b398ea7b3754b023a6f64314e7 Mon Sep 17 00:00:00 2001 From: Tim Chevalier Date: Wed, 4 May 2011 14:28:52 -0700 Subject: [PATCH 09/10] Update docs to reflect preds --- doc/rust.texi | 38 +++++++++++++++++++++++++++++--------- 1 file changed, 29 insertions(+), 9 deletions(-) diff --git a/doc/rust.texi b/doc/rust.texi index 1404e9ca5b38c..1c6b88eb11f11 100644 --- a/doc/rust.texi +++ b/doc/rust.texi @@ -682,6 +682,7 @@ The keywords are: @tab @code{thread} @item @code{auth} @tab @code{unsafe} +@tab @code{as} @tab @code{self} @tab @code{log} @item @code{bind} @@ -711,8 +712,8 @@ The keywords are: @tab @code{str} @item @code{fn} @tab @code{iter} +@tab @code{pred} @tab @code{obj} -@tab @code{as} @tab @code{drop} @item @code{task} @tab @code{port} @@ -1785,8 +1786,6 @@ fn main() @{ @c * Ref.Item.Fn:: Items defining functions. @cindex Functions @cindex Slots, function input and output -@cindex Predicate - A @dfn{function item} defines a sequence of statements associated with a name and a set of parameters. Functions are declared with the keyword @@ -1805,9 +1804,6 @@ expression. If a control path lacks a @code{ret} expression in source code, an implicit @code{ret} expression is appended to the end of the control path during compilation, returning the implicit @code{()} value. -Any pure boolean function is also called a @emph{predicate}, and may be used -as part of the static typestate system. @xref{Ref.Typestate.Constr}. - An example of a function: @example fn add(int x, int y) -> int @{ @@ -1815,6 +1811,30 @@ fn add(int x, int y) -> int @{ @} @end example +@node Ref.Item.Pred +@subsection Ref.Item.Pred +@c * Ref.Item.Pred:: Items defining predicates. +@cindex Predicate + +Any pure boolean function is called a @emph{predicate}, and may be used +as part of the static typestate system. @xref{Ref.Typestate.Constr}. A +predicate declaration is identical to a function declaration, except that it +is declared with the keyword @code{pred} instead of @code{fn}. In addition, +the typechecker checks the body of a predicate with a restricted set of +typechecking rules. A predicate +@itemize +@item may not contain a @code{put}, @code{send}, @code{recv}, assignment, or +self-call expression; and +@item may only call other predicates, not general functions. +@end itemize + +An example of a predicate: +@example +pred lt_42(int x) -> bool @{ + ret (x < 42); +@} +@end example + @node Ref.Item.Iter @subsection Ref.Item.Iter @c * Ref.Item.Iter:: Items defining iterators. @@ -2631,14 +2651,14 @@ This implicit graph is called the @dfn{control-flow graph}, or @dfn{CFG}. @cindex Predicate @cindex Constraint -A @dfn{predicate} is any pure boolean function. @xref{Ref.Item.Fn}. +A @dfn{predicate} is a pure boolean function declared with the keyword @code{pred}. @xref{Ref.Item.Pred}. A @dfn{constraint} is a predicate applied to specific slots. For example, consider the following code: @example -fn is_less_than(int a, int b) -> bool @{ +pred is_less_than(int a, int b) -> bool @{ ret a < b; @} @@ -3543,7 +3563,7 @@ and statically comparing implied states and their specifications. @xref{Ref.Typestate}. @example -fn even(&int x) -> bool @{ +pred even(&int x) -> bool @{ ret x & 1 == 0; @} From 736a4493884ea2dbcc433d4c28b3a164dbc3cc2d Mon Sep 17 00:00:00 2001 From: Tim Chevalier Date: Wed, 4 May 2011 15:24:07 -0700 Subject: [PATCH 10/10] Enforce in typechecker that preds return a bool as well as a test case --- src/comp/middle/typeck.rs | 11 +++++++++++ src/test/compile-fail/pred-not-bool.rs | 4 +++- 2 files changed, 14 insertions(+), 1 deletion(-) diff --git a/src/comp/middle/typeck.rs b/src/comp/middle/typeck.rs index b0b223ab6e5fd..348353a74f94b 100644 --- a/src/comp/middle/typeck.rs +++ b/src/comp/middle/typeck.rs @@ -2841,6 +2841,17 @@ fn check_fn(&@crate_ctxt ccx, &ast.fn_decl decl, ast.proto proto, // TODO: Make sure the type of the block agrees with the function type. auto block_t = check_block(fcx, body); + alt (decl.purity) { + case (ast.pure_fn) { + // per the previous comment, this just checks that the declared + // type is bool, and trusts that that's the actual return type. + if (!ty.type_is_bool(ccx.tcx, fcx.ret_ty)) { + ccx.sess.span_err(body.span, "Non-boolean return type in pred"); + } + } + case (_) {} + } + auto block_wb = resolve_local_types_in_block(fcx, block_t); auto fn_t = rec(decl=decl, diff --git a/src/test/compile-fail/pred-not-bool.rs b/src/test/compile-fail/pred-not-bool.rs index c0d19ef2c9fc1..7c7fa3d175962 100644 --- a/src/test/compile-fail/pred-not-bool.rs +++ b/src/test/compile-fail/pred-not-bool.rs @@ -1,6 +1,8 @@ // -*- rust -*- +// xfail-boot +// xfail-stage0 -// error-pattern: mismatched types +// error-pattern: Non-boolean return type // this checks that a pred with a non-bool return // type is rejected, even if the pred is never used