40 lines
1.2 KiB
Rust
40 lines
1.2 KiB
Rust
|
// 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);
|
||
|
|
}
|