module Stdlib.Data.List;

import Stdlib.Data.List.Base open public;
import Stdlib.Data.Bool.Base open;
import Stdlib.Data.String.Base open;
import Stdlib.Function open;

import Stdlib.Trait.Eq open;
import Stdlib.Trait.Ord open;
import Stdlib.Trait.Show open;
import Stdlib.Trait open;
import Stdlib.Trait.Partial open;
import Stdlib.Trait.Foldable open using {Foldable; module Polymorphic; fromPolymorphicFoldable};

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

instance
eqListI {A} {{Eq A}} : Eq (List A) :=
  let
    go : List A -> List A -> Bool
      | nil nil := true
      | nil _ := false
      | _ nil := false
      | (x :: xs) (y :: ys) := ite (Eq.eq x y) (go xs ys) false;
  in mkEq go;

instance
ordListI {A} {{Ord A}} : Ord (List A) :=
  let
    go : List A -> List A -> Ordering
      | nil nil := EQ
      | nil _ := LT
      | _ nil := GT
      | (x :: xs) (y :: ys) :=
        case Ord.cmp x y of
          | LT := LT
          | GT := GT
          | EQ := go xs ys;
  in mkOrd go;

instance
showListI {A} {{Show A}} : Show (List A) :=
  let
    go : List A -> String
      | nil := "nil"
      | (x :: xs) := Show.show x ++str " :: " ++str go xs;
  in mkShow
    λ {
      | nil := "nil"
      | s := "(" ++str go s ++str ")"
    };

{-# specialize: true, inline: case #-}
instance
functorListI : Functor List :=
  mkFunctor@{
    map := listMap
  };

{-# specialize: true, inline: true #-}
instance
monomorphicFunctorListI {A} : Monomorphic.Functor (List A) A :=
  fromPolymorphicFunctor;

{-# specialize: true, inline: case #-}
instance
polymorphicFoldableListI : Polymorphic.Foldable List :=
  Polymorphic.mkFoldable@{
    for := listFor;
    rfor := listRfor
  };

{-# specialize: true, inline: true #-}
instance
foldableListI {A} : Foldable (List A) A := fromPolymorphicFoldable;

instance
applicativeListI : Applicative List :=
  mkApplicative@{
    pure {A} (a : A) : List A := [a];
    ap {A B} : List (A -> B) -> List A -> List B
      | [] _ := []
      | (f :: fs) l := map f l ++ ap fs l
  };

instance
monadListI : Monad List :=
  mkMonad@{
    bind := flip concatMap
  };