---

yaml
---
r: 27726
b: refs/heads/try
c: 8d26d86
h: refs/heads/master
v: v3

Author: megakorre

[refs]

@@ -2,7 +2,7 @@
 refs/heads/master: cd6f24f9d14ac90d167386a56e7a6ac1f0318195
 refs/heads/snap-stage1: e33de59e47c5076a89eadeb38f4934f58a3618a6
 refs/heads/snap-stage3: cd6f24f9d14ac90d167386a56e7a6ac1f0318195
-refs/heads/try: f9946f37aa14ae98f934c0f9cebffee97dc0d0da
+refs/heads/try: 8d26d86b708b4597e761034fe3a2cc8a7a08c85f
 refs/tags/release-0.1: 1f5c5126e96c79d22cb7862f75304136e204f105
 refs/heads/ndm: f3868061cd7988080c30d6d5bf352a5a5fe2460b
 refs/heads/try2: d0c6ce338884ee21843f4b40bf6bf18d222ce5df

branches/try/doc/rust.md

@@ -899,51 +899,58 @@ express that `f` requires no explicit `return`, as if it returns
 control to the caller, it returns a value (true because it never returns
 control).
 
-#### Pure functions
+#### Predicate functions
 
-A pure function declaration is identical to a function declaration, except that
-it is declared with the additional keyword `pure`. In addition, the typechecker
-checks the body of a pure function with a restricted set of typechecking rules.
-A pure function
+Any pure boolean function is called a *predicate function*, and may be used in
+a [constraint](#constraints), as part of the static [typestate
+system](#typestate-system). A predicate declaration is identical to a function
+declaration, except that it is declared with the additional keyword `pure`. In
+addition, the typechecker checks the body of a predicate with a restricted set
+of typechecking rules. A predicate
 
 * may not contain an assignment or self-call expression; and
-* may only call other pure functions, not general functions.
+* may only call other predicates, not general functions.
 
-An example of a pure function:
+An example of a predicate:
 
 ~~~~
 pure fn lt_42(x: int) -> bool {
     return (x < 42);
 }
 ~~~~
 
-Pure functions may call other pure functions:
+A non-boolean function may also be declared with `pure fn`. This allows
+predicates to call non-boolean functions as long as they are pure. For example:
 
 ~~~~{.xfail-test}
 pure fn pure_length<T>(ls: list<T>) -> uint { /* ... */ }
 
 pure fn nonempty_list<T>(ls: list<T>) -> bool { pure_length(ls) > 0u }
 ~~~~
 
+In this example, `nonempty_list` is a predicate---it can be used in a
+typestate constraint---but the auxiliary function `pure_length` is
+not.
+
 *TODO:* should actually define referential transparency.
 
 The effect checking rules previously enumerated are a restricted set of
 typechecking rules meant to approximate the universe of observably
 referentially transparent Rust procedures conservatively. Sometimes, these
 rules are *too* restrictive. Rust allows programmers to violate these rules by
-writing pure functions that the compiler cannot prove to be referentially
+writing predicates that the compiler cannot prove to be referentially
 transparent, using an escape-hatch feature called "unchecked blocks". When
 writing code that uses unchecked blocks, programmers should always be aware
 that they have an obligation to show that the code *behaves* referentially
 transparently at all times, even if the compiler cannot *prove* automatically
 that the code is referentially transparent. In the presence of unchecked
 blocks, the compiler provides no static guarantee that the code will behave as
 expected at runtime. Rather, the programmer has an independent obligation to
-verify the semantics of the pure functions they write.
+verify the semantics of the predicates they write.
 
 *TODO:* last two sentences are vague.
 
-An example of a pure function that uses an unchecked block:
+An example of a predicate that uses an unchecked block:
 
 ~~~~
 # import std::list::*;
@@ -965,7 +972,7 @@ pure fn pure_length<T>(ls: list<T>) -> uint {
 
 Despite its name, `pure_foldl` is a `fn`, not a `pure fn`, because there is no
 way in Rust to specify that the higher-order function argument `f` is a pure
-function. So, to use `foldl` in a pure list length function that a pure function
+function. So, to use `foldl` in a pure list length function that a predicate
 could then use, we must use an `unchecked` block wrapped around the call to
 `pure_foldl` in the definition of `pure_length`.
 
@@ -1129,8 +1136,8 @@ looks like:
 
 The only exception is that the body of the class constructor begins
 with all the class's fields uninitialized, and is allowed to -- in
-fact, must -- initialize all the fields. The compiler enforces this
-invariant.
+fact, must -- initialize all the fields. A special case in the
+typestate pass enforces this invariant.
 
 Usually, the class constructor stores its argument or arguments in the
 class's named fields. In this case, the `file_descriptor`'s data field
@@ -1299,7 +1306,7 @@ type.
 
 ~~~~
 # trait shape { }
-# impl int: shape { }
+# impl of shape for int { }
 # let mycircle = 0;
 
 let myshape: shape = mycircle as shape;
@@ -1325,7 +1332,7 @@ An _implementation item_ provides an implementation of a
 
 type circle = {radius: float, center: point};
 
-impl circle: shape {
+impl circle_shape of shape for circle {
     fn draw(s: surface) { do_draw_circle(s, self); }
     fn bounding_box() -> bounding_box {
         let r = self.radius;
@@ -1363,10 +1370,10 @@ specified, after the `impl` keyword.
 ~~~~
 # trait seq<T> { }
 
-impl<T> ~[T]: seq<T> {
+impl <T> of seq<T> for ~[T] {
     /* ... */
 }
-impl u32: seq<bool> {
+impl of seq<bool> for u32 {
    /* Treat the integer as a sequence of bits */
 }
 ~~~~
@@ -1927,15 +1934,13 @@ x <- copy y;
 
 The former is just more terse and familiar.
 
-#### Compound assignment expressions
+#### Operator-assignment expressions
 
 The `+`, `-`, `*`, `/`, `%`, `&`, `|`, `^`, `<<`, `>>`, and `>>>`
 operators may be composed with the `=` operator. The expression `lval
 OP= val` is equivalent to `lval = lval OP val`. For example, `x = x +
 1` may be written as `x += 1`.
 
-Any such expression always has the [`nil`](#primitive-types) type.
-
 #### Operator precedence
 
 The precedence of Rust binary operators is ordered as follows, going
@@ -2069,6 +2074,31 @@ A `loop` expression denotes an infinite loop:
 loop_expr : "loop" '{' block '}';
 ~~~~~~~~
 
+For a block `b`, the expression `loop b` is semantically equivalent to
+`while true b`. However, `loop`s differ from `while` loops in that the
+typestate analysis pass takes into account that `loop`s are infinite.
+
+For example, the following (contrived) function uses a `loop` with a
+`return` expression:
+
+~~~~
+fn count() -> bool {
+  let mut i = 0;
+  loop {
+    i += 1;
+    if i == 20 { return true; }
+  }
+}
+~~~~
+
+This function compiles, because typestate recognizes that the `loop`
+never terminates (except non-locally, with `return`), thus there is no
+need to insert a spurious `fail` or `return` after the `loop`. If `loop`
+were replaced with `while true`, the function would be rejected
+because from the compiler's perspective, there would be a control path
+along which `count` does not return a value (that is, if the loop
+condition is always false).
+
 ### Break expressions
 
 ~~~~~~~~{.ebnf .gram}
@@ -2510,7 +2540,7 @@ macro-generated and user-written code can cause unintentional capture.
 Future versions of Rust will address these issues.
 
 
-# Type system
+# Types and typestates
 
 ## Types
 
@@ -2728,7 +2758,7 @@ trait printable {
   fn to_str() -> ~str;
 }
 
-impl ~str: printable {
+impl of printable for ~str {
   fn to_str() -> ~str { self }
 }
 
@@ -2775,7 +2805,7 @@ trait printable {
   fn to_str() -> ~str;
 }
 
-impl ~str: printable {
+impl of printable for ~str {
   fn to_str() -> ~str { self }
 }
 ~~~~~~
@@ -2936,7 +2966,7 @@ Local variables are not initialized when allocated; the entire frame worth of
 local variables are allocated at once, on frame-entry, in an uninitialized
 state. Subsequent statements within a function may or may not initialize the
 local variables. Local variables can be used only after they have been
-initialized; this is enforced by the compiler.
+initialized; this condition is guaranteed by the typestate system.
 
 References are created for function arguments. If the compiler can not prove
 that the referred-to value will outlive the reference, it will try to set