List.fm

// The polymorphic List type can hold a number of elements.
T List <A: Type>
| List.nil;
| List.cons(head: A, tail: List(A));

// Basic Theorems
// ===============

// A proposition that a list is not the empty list
List.not_empty<A: Type>(xs: List(A)) : Type
  case xs:
  | Empty;
  | Unit;

// A theorem that List.cons isn't List.nil
List.cons_isnt_nil<A: Type>(x:A, xs: List(A))
  : Not(Equal(List(A),List.cons<A>(x,xs), List.nil<A>))
  def P = ((x) case x: | Empty; | Unit;) :: List(A) -> Type
  (e) Equal.rewrite<List(A), List.cons<A>(x,xs), List.nil<A>,P>(e, Unit.new)

// A theorem that a list made with List.cons is not the empty list
List.cons_isnt_empty<A: Type>(
  x:A,
  xs: List(A)
): List.not_empty<A>(List.cons<A>(x,xs))
  def y = List.cons<A>(x,xs)
  case y:
  with e : Equal(List(A),y,y.self) = Equal.to<List(A),y>;
  | Empty.absurd<>(List.cons_isnt_nil<A>(x,xs,e));
  | Unit.new;

// Basic Functions
// ===============

// Concatenates two lists.
List.concat<A: Type>(as: List(A), bs: List(A)): List(A)
  case as:
  | bs;
  | List.cons<>(as.head, List.concat<>(as.tail,bs));

// Get the head of a nonempty list
List.head<A: Type>(xs: List(A), not_empty: List.not_empty<A>(xs)) : A
  case xs:
  with ne : List.not_empty<A>(xs.self) = not_empty;
  | Empty.absurd<>(ne);
  | xs.head;

// Get the tail of a nonempty list
List.tail<A: Type>(xs: List(A), not_empty: List.not_empty<A>(xs)) : List(A)
  case xs:
  with ne : List.not_empty<A>(xs.self) = not_empty;
  | Empty.absurd<>(ne);
  | xs.tail;

// Get the all elements of a nonempty list except the last one
List.init<A: Type>(xs: List(A), not_empty: List.not_empty<A>(xs)) : List(A)
  case xs:
  with ne : List.not_empty<A>(xs.self) = not_empty;
  | Empty.absurd<>(ne);
  | case xs.tail:
    with e : Equal(_, xs.tail.self,xs.tail) = Equal.to<List(A),xs.tail>;
    | List.nil<>;
    | def cne = List.cons_isnt_empty<A>(xs.tail.head,xs.tail.tail)
      def xne = Equal.rewrite<_,_,_,(x) List.not_empty<A>(x)>(e,cne)
      List.cons<>(xs.head,List.init<>(xs.tail,xne));;

// Get the last element of a nonempty list
List.last<A: Type>(xs: List(A), not_empty: List.not_empty<A>(xs)) : A
  case xs:
  with ne : List.not_empty<A>(xs.self) = not_empty;
  | Empty.absurd<>(ne);
  | case xs.tail:
    with e : Equal(_, xs.tail.self,xs.tail) = Equal.to<List(A),xs.tail>;
    | xs.head;
    | def cne = List.cons_isnt_empty<A>(xs.tail.head,xs.tail.tail)
      def xne = Equal.rewrite<_,_,_,(x) List.not_empty<A>(x)>(e,cne)
      List.last<>(xs.tail,xne);;

List.uncons<A: Type>(xs: List(A)): Maybe(Pair(A,List(A)))
  case xs:
  | Maybe.none<>;
  | Maybe.some<>(Pair.new<,>(xs.head,xs.tail));

List.null<A: Type>(xs: List(A)) : Bool
  case xs:
  | Bool.true;
  | Bool.false;

// Computes the length of the list.
List.length<A: Type>(xs: List(A), n: Nat): Nat
  case xs:
  | n;
  | List.length<A>(xs.tail,Nat.succ(n));

// Appends element to the end of the list.
List.append<A: Type>(as: List(A), a: A): List(A)
  case as:
  | List.pure<>(a);
  | List.cons<>(as.head,List.append<>(as.tail, a));


// List transformations
// ====================

// Applies a function to all elements of the list.
List.map<A: Type, B: Type>(f: A -> B, as: List(A)): List(B)
  case as:
  | List.nil<>;
  | List.cons<>(f(as.head),List.map<,>(f,as.tail));

// Map over a list with the index
List.imap<A: Type,B: Type>(f: Nat -> A -> B, xs: List(A)): List(B)
  case xs:
  | List.nil<>;
  | List.cons<>(f(0,xs.head),List.imap<,>((n) f(Nat.succ(n)),xs.tail));

// Reverse the order of the elements of the list
List.reverse<A: Type>(xs: List(A)) : List(A)
  List.reverse.go<>(xs,List.nil<>)

List.reverse.go<A: Type>(xs: List(A), res: List(A)): List(A)
  case xs:
  | res;
  | List.reverse.go<>(xs.tail,List.cons<>(xs.head,res));

// insert separators between elements, i.e. `[A,B,C] ~> [A,sep,B,sep,C]`
List.intersperse<A: Type>(sep: A, xs: List(A)): List(A)
  case xs:
  | List.nil<>;
  | case xs.tail:
    | List.pure<>(xs.head);
    | List.cons<>(xs.head,List.cons<>(sep,List.intersperse<A>(sep,xs.tail)));;

// insert separators between elements, i.e. `[A,B,C] ~> [A,sep,B,sep,C]`
List.intercalate<A: Type>(sep: List(A), xs: List(List(A))): List(A)
  List.flatten<A>(List.intersperse<List(A)>(sep,xs))

List.subsequences<A: Type>(xs: List(A)): List(List(A))
  List.cons<>(List.nil<>,List.subsequences.go<>(xs))

List.subsequences.go<A: Type>(xs: List(A)): List(List(A))
  case xs:
  | List.nil<>;
  | let f = ((ys,r) List.cons<>(ys,List.cons<>(List.cons<>(xs.head,ys),r)))
        :: List(A) -> List(List(A)) -> List(List(A))
    List.cons<>
    | List.pure<>(xs.head);
    | List.foldr<,>(List.nil<>,f,List.subsequences.go<>(xs.tail));;

// List transformation proofs
// ==========================

// Proof that List.cons(f(x)) & List.map(f, xs) commute
List.commute_cons_map<A: Type, B: Type>(a :A, ls: List(A), f: A -> B)
  : Equal(List(B),
          List.cons<B>(f(a), List.map<A, B>(f, ls)),
          List.map<A, B>(f, List.cons<A>(a, ls)))
  case ls:
  | _;
  | _;
  : Equal(_, List.cons<>(f(a), List.map<,>(f, ls.self)), List.map<,>(f, List.cons<>(a, ls.self)));

// Reducing Lists
// ==============

// Converts a list to its non-inductive Church encoding
List.fold<A: Type>(list: List(A)): <P: Type> -> P -> (A -> P -> P) -> P
  <P> (nil, cons)
  case list:
  | nil;
  | cons(list.head, List.fold<A>(list.tail)<P>(nil, cons));

List.fold1<A: Type>(xs: List(A))<ne: List.not_empty<A>(xs)>
  : <P: Type> -> P -> (A -> P -> P) -> P
  <P> (nil, cons)
  case xs:
  with ne : List.not_empty<>(xs.self) = ne;
  | Empty.absurd<>(ne);
  | List.fold<>(xs)<P>(nil,cons);

// Folds over a list, right associative
List.foldr<A: Type,B: Type>(b: B, f: A -> B -> B, xs: List(A)): B
  List.fold<>(xs)<>(b,f)

// Folds over a list, left associative
List.foldl<A: Type,B: Type>(b: B, f: B -> A -> B, xs: List(A)): B
  case xs:
  | b;
  | List.foldl<,>(f(b,xs.head),f,xs.tail);

List.foldl1<A: Type>(f: A -> A -> A, xs: List(A), ne: List.not_empty<A>(xs)): A
  case xs:
  with ne : List.not_empty<>(xs.self) = ne;
  | Empty.absurd<>(ne);
  | List.foldl<A,A>(xs.head,f,xs.tail);

// Special folds
// =============

// Flattens a list of lists into a single list.
List.flatten<A: Type>(xs: List(List(A))): List(A)
  case xs:
  | List.nil<>;
  | List.concat<>(xs.head, List.flatten<>(xs.tail));

// Do all elements satisfy a condition?
List.all<A: Type>(cond: A -> Bool, list: List(A)): Bool
  case list:
  | Bool.true;
  | case cond(list.head):
    | List.all<>(cond)(list.tail);
    | Bool.false;;

// Are all elements true?
List.and(list: List(Bool)): Bool
  List.all<>((x) x)(list)

/// Do any element satisfy a condition?
List.any <A: Type>(cond: A -> Bool, list: List(A)): Bool
  case list:
  | Bool.false;
  | case cond(list.head):
    | Bool.true;
    | List.any<>(cond)(list.tail);;

// Is any element true?
List.or(list: List(Bool)): Bool
  List.any<>((x) x)(list)

// Add the total of a list of natural numbers
List.sum(xs: List(Nat)) : Nat
  List.sum.go(xs, Nat.zero)

List.sum.go(xs: List(Nat), n: Nat) : Nat
  case xs:
  | Nat.zero;
  | List.sum.go(xs.tail,Nat.add(xs.head,n));

List.product(xs: List(Nat)) : Nat
  List.product.go(xs, Nat.zero)

List.product.go(xs: List(Nat), n: Nat) : Nat
  case xs:
  | Nat.zero;
  | List.product.go(xs.tail,Nat.mul(xs.head,n));

// Print a list
List.show<A: Type>(f: A -> String, xs: List(A)): String
  String.flatten(["[",String.intercalate(",", List.map<,>(f,xs)),"]"])

// List functor
// ============

// The functor instance for list
List.functor: Functor(List)
  Functor.new<List>(List.map)

// Proof that List.functor conforms to the functor laws
List.functor.verified: VerifiedFunctor(List, List.functor)
  VerifiedFunctor.new<List, List.functor>(List.map.id, List.map.comp)

List.map.id<A: Type>(ls: List(A)): Equal(List(A), List.map<A, A>(Function.id<A>, ls), ls)
  case ls:
  | Equal.to<_, List.map<,>(Function.id<>, List.nil<>)>;
  | let tail_eq = List.map.id<>(ls.tail)
    Equal.apply<_, _,
                List.map<,>(Function.id<>, ls.tail),
                ls.tail,
                List.cons<>(ls.head)>(tail_eq);
  : Equal(_, List.map<,>(Function.id<>, ls.self), ls.self);

List.map.comp<A: Type, B: Type, C: Type>(ls: List(A), g: (B -> C), h: (A -> B))
  : Equal(List(C),
          List.map<A, C>(Function.comp<A, B, C>(g, h), ls),
          Function.comp<List(A), List(B), List(C)>(List.map<B, C>(g), List.map<A, B>(h))(ls))
  case ls:
  | Equal.to<_, List.map<,>(Function.comp<,,>(g, h), List.nil<>)>;
  | let tail_eq = List.map.comp<,,>(ls.tail, g, h)
    Equal.apply<_, _,
                List.map<,>(Function.comp<,,>(g, h), ls.tail),
                Function.comp<,,>(List.map<,>(g), List.map<,>(h), ls.tail), List.cons<>(Function.comp<,,>(g, h, ls.head))>(tail_eq);
  : Equal(_, List.map<,>(Function.comp<,,>(g, h), ls.self), Function.comp<,,>(List.map<,>(g), List.map<,>(h))(ls.self));

// List monad
// ==========

// The monad instance for list
List.monad: Monad(List)
  Monad.new<List>(List.bind, List.pure)

// A list with only one element.
List.pure<A : Type>(x : A) : List(A)
  List.cons<A>(x)(List.nil<A>)

// The bind function of the list Monad.
List.bind<A: Type,B: Type>(xs: List(A), f: A -> List(B)): List(B)
  List.flatten<>(List.map<,>(f)(xs))

// Sublists
// ========

// Removes the first elements of a list.
List.drop<A: Type>(n: Nat, xs: List(A)):  List(A)
  case n:
  | xs;
  | case xs:
    | List.nil<>;
    | List.drop<>(n.pred,xs.tail);;

// Returns the first elements of a list, discards the rest.
List.take<A: Type>(n: Nat, xs: List(A)): List(A)
  case xs:
  | List.nil<>;
  | case n:
    | List.nil<>;
    | List.cons<>(xs.head,List.take<>(n.pred, xs.tail));;

// Remove elements while a condition is true
List.drop_while<A: Type>(f: A -> Bool, xs: List(A)): List(A)
  case xs:
  | List.nil<>;
  | case f(xs.head):
    | List.drop_while<>(f,xs.tail);
    | xs;;

List.take_while<A: Type>(f: A -> Bool, xs: List(A)) : List(A)
  case xs:
  | List.nil<>;
  | case f(xs.head):
    | List.cons<>(xs.head,List.take_while<>(f,xs.tail));
    | List.nil<>;;

List.split_at<A: Type>(n : Nat, xs: List(A)) : Pair(List(A),List(A))
  case xs:
  | Pair.new<,>(List.nil<>, List.nil<>);
  | case n:
    | Pair.new<,>(List.nil<>, xs);
    | get fst snd = List.split_at<>(n.pred, xs.tail)
      Pair.new<,>(List.cons<>(xs.head, fst), snd);;

List.drop_until<A: Type>(f: A -> Bool, xs: List(A)): List(A)
  List.drop_while<>((c) Bool.not(f(c)), xs)

// Removes all elements that do not satisfy a condition.
List.filter<A: Type>(f: A -> Bool, xs: List(A)): List(A)
  case xs:
  | List.nil<>;
  | case f(xs.head):
    | List.cons<>(xs.head,List.filter<>(f, xs.tail));
    | List.filter<>(f, xs.tail);;

List.span<A: Type>(f: A -> Bool, xs: List(A)): Pair(List(A),List(A))
  case xs:
  | Pair.new<,>(List.nil<>,List.nil<>);
  | case f(xs.head):
    | get y z = List.span<>(f,xs.tail)
      Pair.new<,>(List.cons<>(xs.head,y),z);
    | Pair.new<,>(List.nil<>,xs);;

// List.Builder
// ============

// A lazy List constructor, useful for efficient concatenation
List.Builder(A: Type): Type
  List(A) -> List(A)

// construct a new builder (it's just the identity function)
List.Builder.new<A: Type> : List.Builder(A)
  (x) x

// turn a builder into a List
List.run_builder<A: Type>(lb: List.Builder(A)): List(A)
  lb(List.nil<>)

// concatenate two list builders
List.Builder.concat<A: Type>(a: List.Builder(A), b: List.Builder(A)): List.Builder(A)
   (x) a(b(x))

// prepend an element
List.Builder.cons<A: Type>(c: A, lb: List.Builder(A)) : List.Builder(A)
  (x) List.cons<>(c,lb(x))

// append an element
List.Builder.snoc<A: Type>(c: A, lb: List.Builder(A)) : List.Builder(A)
  (x) lb(List.cons<>(c,x))

// convert a list to a builder
List.to_builder<A: Type>(list: List(A)) : List.Builder(A)
  List.to_builder.go<>(list, List.Builder.new<>)

List.to_builder.go<A: Type>(list: List(A), lb: List.Builder(A)) : List.Builder(A)
  case list:
  | lb;
  | List.to_builder.go<>(list.tail)(List.Builder.snoc<>(list.head, lb));

// Returns the element at given position.
List.at<A: Type>(list: List(A), index: Nat): Maybe(A)
  case list:
  | Maybe.none<>;
  | case index:
    | Maybe.some<>(list.head);
    | List.at<>(list.tail)(index.pred);;

List.chunk<A: Type>(n: Nat, xs: List(A)): Maybe(List(A))
  case n:
  | Maybe.some<>(List.nil<>);
  | case xs:
    | Maybe.none<>;
    | Maybe.bind<,>(List.chunk<>(n.pred,xs.tail))
      | (x) Maybe.some<>(List.cons<>(xs.head,x));;;

// Indexing Lists
// ==============

//Finds the first occurrence that satisfies a condition
List.find<A: Type>(cond: A -> Bool, xs: List(A)): Maybe(A)
  case xs:
  | Maybe.none<>;
  | case cond(xs.head):
    | Maybe.some<>(xs.head);
    | List.find<>(cond)(xs.tail);;

// Finds the last element that satisfies a condition and its index.
List.find_last<A: Type>(xs: List(A), f: A -> Nat -> Bool): Maybe(Pair(A)(Nat))
  List.find_last.go<A>(xs,f,Nat.zero,Maybe.none<>)

List.find_last.go<A: Type>(
  xs: List(A),
  f: A -> Nat -> Bool,
  n: Nat,
  res: Maybe(Pair(A,Nat))
): Maybe(Pair(A,Nat))
  case xs:
  | res;
  | let res = case f(xs.head,n):
      | Maybe.some<>(Pair.new<,>(xs.head,n));
      | res;
    List.find_last.go<>(xs.tail,f,Nat.succ(n),res);

// Finds the first element that satisfies a condition and its index.
List.ifind<A: Type>(xs: List(A), f: A -> Nat -> Bool): Maybe(Pair(A,Nat))
  List.ifind.go<A>(xs,f,Nat.zero)

List.ifind.go<A: Type>(xs: List(A), f: A -> Nat -> Bool, i: Nat): Maybe(Pair(A,Nat))
  case xs:
  | Maybe.none<>;
  | case f(xs.head,i):
    | Maybe.some<>(Pair.new<,>(xs.head)(i));
    | List.ifind.go<>(xs.tail,f,Nat.succ(i));;

// Zipping lists
// =============

// Given two lists `xs` and `ys`, applies `f(xs[i],ys[i])` for all `i`.
List.zip_with<A: Type, B: Type, C: Type>(f: A -> B -> C, as: List(A), bs: List(B))
  : List(C)
  case as:
  | List.nil<>;
  | case bs:
    | List.nil<>;
    | List.cons<>(f(as.head,bs.head),List.zip_with<,,>(f,as.tail,bs.tail));;