/* union <'a> list with nat { Nil(0); {n:nat} Cons(n+1) of 'a * <'a> list(n) } */ ('a){n:nat} int(n) length (xs: <'a> list(n)) { var: int x;; x = 0; invariant: [i:nat,j:nat | i+j=n] (xs: <'a> list(i), x: int(j)) while (true) { switch(xs) { case Nil: return x; case Cons(_, xs): x = x + 1; } } exit; } ('a){m:nat,n:nat} <'a> list(m+n) append (xs: <'a> list(m), ys: <'a> list(n)) { var: 'a x;; switch (xs) { case Nil: return ys; case Cons(x, xs): return Cons(x, append(xs, ys)); } } ('a){m:nat,n:nat} <'a> list(m+n) rev_append (xs: <'a> list(m), ys: <'a> list(n)) { var: 'a x;; invariant: [m1:nat,n1:nat | m1+n1 = m+n] (xs: <'a> list(m1), ys: <'a> list(n1)) while (true) { switch (xs) { case Nil: return ys; case Cons(x, xs): ys = Cons(x, ys); } } exit; } ('a){n:nat} <'a> list(n) reverse (xs: <'a> list(n)) { return rev_append(xs, Nil); } ('a,'b){n:nat} <'b> list(n) map (f: 'a -> 'b, xs: <'a> list(n)) { var: 'a x;; switch (xs) { case Nil: return Nil; case Cons(x, xs): return Cons(f(x), map(f, xs)); } } ('a,'b){n:nat} <'a> list(n) * <'b> list(n) split (xs: <'a *'b> list(n)) { var: 'a y; 'b z; <'a> list ys; <'b> list zs;; switch (xs) { case Nil: return (Nil, Nil); case Cons((y, z), xs): switch (split(xs)) { case (ys, zs): return(Cons(y, ys), Cons(z, zs)); } } } ('a,'b){n:nat} <'a * 'b> list(n) zip (xs: <'a> list(n), ys: <'b> list(n)) { var: 'a x; 'b y;; switch (xs, ys) { case (Nil, Nil): return Nil; case (Cons(x, xs), Cons(y, ys)): return Cons((x, y), zip (xs, ys)); } } ('a,'b){m:nat,n:nat} <'a * 'b> list(min(m,n)) zip1 (xs: <'a> list(m), ys: <'b> list(n)) { var: 'a x; 'b y;; switch (xs, ys) { case (Nil, _): return Nil; case (_, Nil): return Nil; case (Cons(x, xs), Cons(y, ys)): return Cons((x, y), zip1 (xs, ys)); } } ('a){n:nat} 'a head (xs: <'a> list(n+1)) { var: 'a x;; Cons(x, xs) = xs; return x; } ('a){n:nat} <'a> list(n) tail (xs: <'a> list(n+1)) { Cons(_, xs) = xs; return xs; } ('a){n:nat} int(n) length (xs: <'a> list(n)) { var: int x;; x = 0; invariant: [p:nat, q:nat | p + q = n] (xs: <'a> list(p), x: int(q)) while (true) { switch(xs) { case Nil: return x; case Cons(_, xs): x = x + 1; } } exit; } ('a){m:nat,n:nat | n < m} 'a nth (xs: <'a> list(m), n: int(n)) { var: 'a x;; invariant: [m:nat, n:nat | n < m] (xs: <'a> list(m), n: int(n)) while (true) { Cons(x, xs) = xs; if (n > 0) n = n - 1; else return x; } exit; } ('a){n:nat} unit iterate (f: 'a -> unit, xs: <'a> list(n)) { var: 'a x;; invariant: [n:nat] (xs: <'a> list(n)) while (true) { switch (xs) { case Nil: return; case Cons(x, xs): f(x); } } } ('a) bool exists(p: 'a -> bool, xs: <'a> list) { var: 'a x;; while (true) { switch (xs) { case Nil: break; case Cons(x, xs): if (p(x)) return true; } } return false; } ('a) bool forall(p: 'a -> bool, xs: <'a> list) { var: 'a x;; while (true) { switch (xs) { case Nil: break; case Cons(x, xs): if (p(x)) ; else return false; } } return true; } ('a) <'a> list flatten (xss: <<'a> list> list) { var: <'a> list xs, ys;; switch (xss) { case Nil: return Nil; case Cons(xs, xss): ys = flatten (xss); return append(xs, ys); } }