Typestate 2

.gitignore

@@ -34,6 +34,7 @@
 *.vr
 *.swp
 *.tmp
+*.pyc
 .hg/
 .hgignore
 .cproject
@@ -53,3 +54,5 @@ config.mk
 /build/
 src/.DS_Store
 /stage0/
+/dl/
+

doc/rust.texi

@@ -682,7 +682,9 @@ The keywords are:
 @tab @code{thread}
 @item @code{auth}
 @tab @code{unsafe}
+@tab @code{as}
 @tab @code{self}
+@tab @code{log}
 @item @code{bind}
 @tab @code{type}
 @tab @code{true}
@@ -710,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}
@@ -727,12 +729,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 +1397,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,
@@ -1784,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
@@ -1804,16 +1804,37 @@ 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 @{
     ret x + y;
 @}
 @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.
@@ -1887,7 +1908,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 +2253,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
 
 
@@ -2630,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;
 @}
 
@@ -2898,6 +2919,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 +3091,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
 
@@ -3540,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;
 @}
 
@@ -3592,6 +3615,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

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=$@ $<

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);
@@ -563,6 +569,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

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);

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);

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 */