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;
open import Stdlib.Debug.Fail;

infixr 5 ::;
--- Inductive list.
type List (a : Type) :=
  | --- The empty list
    nil : List a
  | --- An element followed by a list
    :: : a → List a → List a;

--- 𝒪(𝓃). Returns ;true; if the given
--- object is in the ;List;.
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;

--- Right-associative fold.
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);

--- Left-associative and tail-recursive fold.
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;

--- 𝒪(𝓃). Maps a function over each element of a ;List;.
map : {A : Type} → {B : Type} → (A → B) → List A → List B;
map f nil := nil;
map f (h :: hs) := f h :: map f hs;

--- 𝒪(𝓃). Only keeps the elements for which the
--- given predicate returns ;true;.
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);

--- 𝒪(𝓃). Returns the length of the ;List;.
length : {A : Type} → List A → Nat;
length nil := zero;
length (_ :: l) := suc (length l);

--- 𝒪(𝓃). Returns the given ;List; in reverse order.
reverse : {A : Type} → List A → List A;
reverse := foldl (flip (::)) nil;

--- Returns a ;List; of length n where every element is the given value.
replicate : {A : Type} → Nat → A → List A;
replicate zero _ := nil;
replicate (suc n) x := x :: replicate n x;

--- Takes the first n elements of a ;List;.
take : {A : Type} → Nat → List A → List A;
take (suc n) (x :: xs) := x :: take n xs;
take _ _ := nil;

--- 𝒪(𝓃). splitAt n xs returns a tuple where first element is xs
--- prefix of length n and second element is the remainder of the ;List;.
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);

--- 𝒪(𝓃 + 𝓂). Merges two lists according the given ordering.
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;

--- 𝒪(𝓃). Returns a tuple where the first component has the items that
--- satisfy the predicate and the second component has the elements that don't.
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 ++;
--- Concatenates two ;List;s.
++ : {A : Type} → List A → List A → List A;
++ nil ys := ys;
++ (x :: xs) ys := x :: xs ++ ys;

--- Concatenates a ;List; of ;List;s.
flatten : {A : Type} → List (List A) → List A;
flatten := foldl (++) nil;

--- 𝒪(𝓃). Inserts the given element before every element in the given ;List;.
prependToAll : {A : Type} → A → List A → List A;
prependToAll _ nil := nil;
prependToAll sep (x :: xs) := sep :: x :: prependToAll sep xs;

--- 𝒪(𝓃). Inserts the given element inbetween every two elements in the given ;List;.
intersperse : {A : Type} → A → List A → List A;
intersperse _ nil := nil;
intersperse sep (x :: xs) := x :: prependToAll sep xs;

--- 𝒪(1). Partial function that returns the first element of a ;List;.
head : {A : Type} → List A → A;
head (x :: _) := x;
head nil := fail "head: empty list";

--- 𝒪(1). Drops the first element of a ;List;.
tail : {A : Type} → List A → List A;
tail (_ :: xs) := xs;
tail nil := nil;

--- 𝒪(𝓃 * 𝓂). Partial function that transposes a ;List; of ;List;s interpreted as a matrix.
terminating
transpose : {A : Type} → List (List A) → List (List A);
transpose (nil :: _) := nil;
transpose xss := map head xss :: transpose (map tail xss);

--- 𝒪(𝓃). Returns ;true; if at least one element of the ;List; satisfies the predicate.
any : {A : Type} → (A → Bool) → List A → Bool;
any f xs := foldl or false (map f xs);

--- 𝒪(1). Returns ;true; if the ;List; is empty.
null : {A : Type} → List A → Bool;
null nil := true;
null _ := false;