module Stdlib.Data.List;
  open import Stdlib.Data.Bool;
  open import Stdlib.Function;
  open import Stdlib.Data.Nat;
  open import Stdlib.Data.Ord;
  open import Stdlib.Data.Product;

  infixr 5 ;
  inductive List (a : Type) {
    nil : List a;
     : a  List a  List a;
  };

  elem : {A : Type}  (A  A  Bool)  A  List A  Bool;
  elem _ _ nil := false;
  elem eq s (x  xs) := eq s x || elem eq s xs;

  foldr : {A : Type}  {B : Type}  (A  B  B)  B  List
    A  B;
  foldr _ z nil := z;
  foldr f z (h  hs) := f h (foldr f z hs);

  foldl : {A : Type}  {B : Type}  (B  A  B)  B  List
    A  B;
  foldl f z nil := z;
  foldl f z (h  hs) := foldl f (f z h) hs;

  map : {A : Type}  {B : Type}  (A  B)  List A  List B;
  map f nil := nil;
  map f (h  hs) := f h  map f hs;

  filter : {A : Type}  (A  Bool)  List A  List A;
  filter _ nil := nil;
  filter f (h  hs) := if
    (f h)
    (h  filter f hs)
    (filter f hs);

  length : {A : Type}  List A  Nat;
  length nil := zero;
  length (_  l) := suc (length l);

  reverse : {A : Type}  List A  List A;
  reverse := foldl (flip ()) nil;

  replicate : {A : Type}  Nat  A  List A;
  replicate zero _ := nil;
  replicate (suc n) x := x  replicate n x;

  take : {A : Type}  Nat  List A  List A;
  take (suc n) (x  xs) := x  take n xs;
  take _ _ := nil;

  splitAt : {A : Type}  Nat  List A  List A × List A;
  splitAt _ nil := nil , nil;
  splitAt zero xs := nil , xs;
  splitAt (suc zero) (x  xs) := x  nil , xs;
  splitAt (suc (suc m)) (x  xs) := first
    (() x)
    (splitAt m xs);

  merge : {A : Type}  (A  A  Ordering)  List A  List
    A  List A;
  merge cmp (x  xs) (y  ys) := if
    (isLT (cmp x y))
    (x  merge cmp xs (y  ys))
    (y  merge cmp (x  xs) ys);
  merge _ nil ys := ys;
  merge _ xs nil := xs;

  partition : {A : Type}  (A  Bool)  List A  List A
    × List A;
  partition _ nil := nil , nil;
  partition f (x  xs) := if
    (f x)
    first
    second
    (() x)
    (partition f xs);

  infixr 5 ++;
  ++ : {A : Type}  List A  List A  List A;
  ++ nil ys := ys;
  ++ (x  xs) ys := x  xs ++ ys;

  flatten : {A : Type}  List (List A)  List A;
  flatten := foldl (++) nil;

  prependToAll : {A : Type}  A  List A  List A;
  prependToAll _ nil := nil;
  prependToAll sep (x  xs) := sep  x  prependToAll sep xs;

  intersperse : {A : Type}  A  List A  List A;
  intersperse _ nil := nil;
  intersperse sep (x  xs) := x  prependToAll sep xs;

  head : {A : Type}  List A  A;
  head (x  _) := x;

  tail : {A : Type}  List A  List A;
  tail (_  xs) := xs;

  terminating
  transpose : {A : Type}  List (List A)  List (List A);
  transpose (nil  _) := nil;
  transpose xss := map head xss  transpose (map tail xss);

  any : {A : Type}  (A  Bool)  List A  Bool;
  any f xs := foldl (||) false (map f xs);

  null : {A : Type}  List A  Bool;
  null nil := true;
  null _ := false;
end;