list.timl

(* List and its operations *)

structure List = struct

(* length-indexed list *)
datatype list 'a : {Nat} =
         Nil of list 'a {0} 
       | Cons {n : Nat} of 'a * list 'a {n} --> list 'a {n + 1} 

absidx T_map : BigO (fn m n => $m * $n) with
fun map ['a 'b] {m n : Nat} (f : 'a -- $m --> 'b) (ls : list (* 'a *)_ {n}) return list (* 'b *)_ {n} using T_map m n =
          case ls of
              Nil => Nil
            | Cons (x, xs) => Cons (f x, map f xs)
end

(* fold-left *)                   
fun foldl ['a 'b] {m n : Nat} (f : 'a * 'b -- $m --> 'b) acc (l : list 'a {n}) return (* 'b *) using $(m + 4) * $n =
  case l of
      [] => acc
    | x :: xs => foldl f (f (x, acc)) xs

(* another version of [foldl] that uses big-O spec *)                     
absidx T_foldl : BigO (fn m n => $m * $n) with
fun foldl ['a 'b] {m n : Nat} (f : 'a * 'b -- $m --> 'b) y (xs : list 'a {n}) return (* 'b *) using T_foldl m n =
        case xs of
            [] => y
          | x :: xs => foldl f (f (x, y)) xs
end

(* [hd] is a total function that requires its input list to be non-empty *)
fun hd {n: Nat | n > 0} (ls: list _ {n}) =
    case ls of
        x :: _ => x
      | _ => never

(* reverse and append *)
fun rev_append {n m : Nat} (l : list _ {n}, acc : list _ {m}) return list _ {n + m} using $n =
    case l of
        [] => acc
      | hd :: tl => rev_append (tl, hd :: acc)

(* another version with Big-O complexity *)
absidx T_rev_append : BigO (fn n => $n) (* = fn n => 2.0 * $n *) with
fun rev_append_2 {n1 n2 : Nat} (xs : list _ {n1}) (ys : list _ {n2}) return list _ {n1 + n2} using T_rev_append n1 =
    case xs of
        [] => ys
      | x :: xs => rev_append_2 xs (x :: ys)
end

(* reverse *)
absidx T_rev : BigO (fn n => $n) with
fun rev {n : Nat} (xs : list _ {n}) return list _ {n} using T_rev n = rev_append_2 xs []
end

end