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.Trait.Eq open;
import Stdlib.Trait.Ord open;
import Stdlib.Trait.Show open;
import Stdlib.Trait.Partial open;

--- 𝒪(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) := if (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 ")"
    };