Merge pull request #1392 from Lenny222/list

list: add "is_not_empty" requirement to "head" and "tail" (analogous to "vec")
This commit is contained in:
Brian Anderson 2012-01-03 12:18:53 -08:00
commit 513a263e81
6 changed files with 87 additions and 16 deletions

View File

@ -1,7 +1,7 @@
import syntax::{visit, ast_util};
import syntax::ast::*;
import syntax::codemap::span;
import std::list::{list, nil, cons, tail};
import std::list::{is_not_empty, list, nil, cons, tail};
import core::{vec, option};
import std::list;
@ -192,7 +192,9 @@ fn visit_block(tp: block_type, cx: ctx, visit: block()) {
visit();
local.second = true;
visit();
cx.blocks = tail(cx.blocks);
let cx_blocks = cx.blocks;
check is_not_empty(cx_blocks);
cx.blocks = tail(cx_blocks);
cx.current = join_branches(local.exits);
}

View File

@ -266,6 +266,7 @@ fn map_crate(e: @env, c: @ast::crate) {
let imp = follow_import(*e, sc, *path, vi.span);
if option::is_some(imp) {
let glob = {def: option::get(imp), item: vi};
check list::is_not_empty(sc);
alt list::head(sc) {
scope_item(i) {
e.mod_map.get(i.id).glob_imports += [glob];
@ -461,6 +462,7 @@ fn visit_block_with_scope(b: ast::blk, sc: scopes, v: vt<scopes>) {
}
fn visit_decl_with_scope(d: @decl, sc: scopes, v: vt<scopes>) {
check list::is_not_empty(sc);
let loc_pos = alt list::head(sc) {
scope_block(_, _, pos) { pos }
_ { @mutable 0u }

View File

@ -97,6 +97,27 @@ fn has<copy T>(ls: list<T>, elt: T) -> bool {
ret false;
}
/*
Function: is_empty
Returns true if the list is empty.
*/
pure fn is_empty<copy T>(ls: list<T>) -> bool {
alt ls {
nil. { true }
_ { false }
}
}
/*
Function: is_not_empty
Returns true if the list is not empty.
*/
pure fn is_not_empty<copy T>(ls: list<T>) -> bool {
ret !is_empty(ls);
}
/*
Function: len
@ -112,8 +133,11 @@ Function: tail
Returns all but the first element of a list
*/
pure fn tail<copy T>(ls: list<T>) -> list<T> {
alt ls { cons(_, tl) { ret *tl; } nil. { fail "list empty" } }
pure fn tail<copy T>(ls: list<T>) : is_not_empty(ls) -> list<T> {
alt ls {
cons(_, tl) { ret *tl; }
nil. { fail "list empty" }
}
}
/*
@ -121,8 +145,11 @@ Function: head
Returns the first element of a list
*/
pure fn head<copy T>(ls: list<T>) -> T {
alt ls { cons(hd, _) { ret hd; } nil. { fail "list empty" } }
pure fn head<copy T>(ls: list<T>) : is_not_empty(ls) -> T {
alt ls {
cons(hd, _) { ret hd; }
nil. { fail "list empty" }
}
}
/*

View File

@ -14,7 +14,10 @@ pure fn nonempty_list<copy T>(ls: list<T>) -> bool { pure_length(ls) > 0u }
// 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<copy T>(ls: list<T>) : nonempty_list(ls) -> T { head(ls) }
fn safe_head<copy T>(ls: list<T>) : nonempty_list(ls) -> T {
check is_not_empty(ls);
ret head(ls);
}
fn main() {
let mylist = cons(@1u, @nil);

View File

@ -1,4 +1,6 @@
// Uses foldl to exhibit the unchecked block syntax.
// TODO: since list's head/tail require the predicate "is_not_empty" now and
// we have unit tests for list, this test might me not necessary anymore?
use std;
import std::list::*;
@ -6,7 +8,10 @@ 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<copy T, copy 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)) } }
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
@ -22,7 +27,10 @@ pure fn nonempty_list<copy T>(ls: list<T>) -> bool { pure_length(ls) > 0u }
// 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<copy T>(ls: list<T>) : nonempty_list(ls) -> T { head(ls) }
fn safe_head<copy T>(ls: list<T>) : nonempty_list(ls) -> T {
check is_not_empty(ls);
ret head(ls)
}
fn main() {
let mylist = cons(@1u, @nil);

View File

@ -2,17 +2,38 @@ import core::*;
use std;
import std::list;
import std::list::head;
import std::list::tail;
import std::list::from_vec;
import std::list::{from_vec, head, is_empty, is_not_empty, tail};
import option;
#[test]
fn test_is_empty() {
let empty : list::list<int> = from_vec([]);
let full1 = from_vec([1]);
let full2 = from_vec(['r', 'u']);
assert is_empty(empty);
assert !is_empty(full1);
assert !is_empty(full2);
assert !is_not_empty(empty);
assert is_not_empty(full1);
assert is_not_empty(full2);
}
#[test]
fn test_from_vec() {
let l = from_vec([0, 1, 2]);
check is_not_empty(l);
assert (head(l) == 0);
assert (head(tail(l)) == 1);
assert (head(tail(tail(l))) == 2);
let tail_l = tail(l);
check is_not_empty(tail_l);
assert (head(tail_l) == 1);
let tail_tail_l = tail(tail_l);
check is_not_empty(tail_tail_l);
assert (head(tail_tail_l) == 2);
}
#[test]
@ -24,9 +45,17 @@ fn test_from_vec_empty() {
#[test]
fn test_from_vec_mut() {
let l = from_vec([mutable 0, 1, 2]);
check is_not_empty(l);
assert (head(l) == 0);
assert (head(tail(l)) == 1);
assert (head(tail(tail(l))) == 2);
let tail_l = tail(l);
check is_not_empty(tail_l);
assert (head(tail_l) == 1);
let tail_tail_l = tail(tail_l);
check is_not_empty(tail_tail_l);
assert (head(tail_tail_l) == 2);
}
#[test]