Test case for unchecked blocks

src/test/run-pass/unchecked-predicates.rs

@@ -0,0 +1,41 @@
+// xfail-stage0
+// Uses foldl to exhibit the unchecked block syntax.
+use std;
+
+import std::list::*;
+
+// Can't easily be written as a "pure fn" because there's
+// no syntax for specifying that f is pure.
+fn pure_foldl<@T, @U>(ls: &list<T>, u: &U, f: &block(&T, &U) -> U) -> U {
+    alt ls {
+      nil. { u }
+      cons(hd, tl) { f(hd, pure_foldl(*tl, f(hd, u), f)) }
+    }
+}
+
+// Shows how to use an "unchecked" block to call a general
+// fn from a pure fn
+pure fn pure_length<@T>(ls: &list<T>) -> uint {
+    fn count<T>(_t: &T, u: &uint) -> uint { u + 1u }
+    unchecked {
+        pure_foldl(ls, 0u, count)
+    }
+}
+
+pure fn nonempty_list<@T>(ls: &list<T>) -> bool {
+    pure_length(ls) > 0u
+}
+
+ // Of course, the compiler can't take advantage of the
+    // knowledge that ls is a cons node. Future work.
+    // Also, this is pretty contrived since nonempty_list
+    // could be a "tag refinement", if we implement those.
+fn safe_head<@T>(ls: &list<T>) : nonempty_list(ls) -> T { car(ls) }
+
+fn main() {
+    let mylist = cons(@1u, @nil);
+    // Again, a way to eliminate such "obvious" checks seems
+    // desirable. (Tags could have postconditions.)
+    check(nonempty_list(mylist));
+    assert (*(safe_head(mylist)) == 1u);
+}