#
# Constant time concatenable list.
#
# -- Allen Leung
# Compiled by:
# src/lib/std/src/standard-core.sublib# See also the discussion in Chris Okasaki's "Purely Functional Data Structures",
# p 153 section 10.2.1: "Lists with efficient catenation".
package catlist: Catlist { # Catlist is from src/lib/std/src/catlist.api Catlist(X)
= EMPTY_LIST
| SINGLE X
| PAIR (Catlist(X), Catlist(X));
empty = EMPTY_LIST;
single = SINGLE;
fun null EMPTY_LIST => TRUE;
null _ => FALSE;
end;
fun length EMPTY_LIST => 0;
length (SINGLE _) => 1;
length (PAIR(a,b)) => length a + length b;
end;
fun head EMPTY_LIST => raise exception EMPTY;
head (SINGLE a) => a;
head (PAIR(a,b)) => head a;
end;
fun tail EMPTY_LIST => raise exception EMPTY;
tail (SINGLE a) => EMPTY_LIST;
tail (PAIR((SINGLE _), a)) => a;
tail (PAIR(PAIR(a,b),c)) => tail (PAIR(a,(PAIR(b,c))));
tail (PAIR(EMPTY_LIST,c)) => tail c;
end;
fun cons (a, EMPTY_LIST) => SINGLE a;
cons (a, b) => PAIR(SINGLE a,b);
end;
fun append (EMPTY_LIST, a) => a;
append (a, EMPTY_LIST) => a;
append (a, b) => PAIR(a, b);
end;
fun map f l
=
g l
where
fun g EMPTY_LIST => EMPTY_LIST;
g (SINGLE a) => SINGLE (f a);
g (PAIR(a, b)) => PAIR((g a), (g b));
end;
end;
fun apply f l
=
g l
where
fun g EMPTY_LIST => ();
g (SINGLE a) => f a;
g (PAIR(a, b)) => { g a; g b;};
end;
end;
fun from_list [] => EMPTY_LIST;
from_list (a ! b) => cons (a, from_list b);
end;
fun to_list l
=
g (l, [])
where
fun g (EMPTY_LIST, l) => l;
g (SINGLE a, l) => a ! l;
g (PAIR(a, b), l) => g (a, g (b, l));
end;
end;
};