module Stdlib.Data.List;

open import Stdlib.Data.List.Base public;
open import Stdlib.Data.Bool.Base;
open import Stdlib.Data.String.Base;
open import Stdlib.Debug.Fail;

import Stdlib.Trait.Eq as Eq;
open Eq using {Eq};

import Stdlib.Trait.Ord as Ord;
open Ord using {Ord};

import Stdlib.Trait.Show as Show;
open Show using {Show};

--- 𝒪(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";

--- 𝒪(𝓃 * 𝓂). 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);

module ListTraits;
  
  Eq : {A : Type} -> Eq A -> Eq (List A);
  Eq {A} (Eq.mkEq eq-a) :=
    let
      go : List A -> List A -> Bool;
      go nil nil := true;
      go nil _ := false;
      go _ nil := false;
      go (x :: xs) (y :: ys) := if (eq-a x y) (go xs ys) false;
    in Eq.mkEq go;
  
  Ord : {A : Type} -> Ord A -> Ord (List A);
  Ord {A} (Ord.mkOrd cmp-a) :=
    let
      go : List A -> List A -> Ord.Ordering;
      go nil nil := Ord.EQ;
      go nil _ := Ord.LT;
      go _ nil := Ord.GT;
      go (x :: xs) (y :: ys) :=
        case cmp-a x y
          | Ord.LT := Ord.LT
          | Ord.GT := Ord.GT
          | Ord.EQ := go xs ys;
    in Ord.mkOrd go;
  
  Show : {A : Type} -> Show A -> Show (List A);
  Show {A} (Show.mkShow to-str) :=
    let
      go : List A -> String;
      go nil := "nil";
      go (x :: xs) := to-str x ++str " :: " ++str go xs;
    in Show.mkShow
      λ {
        | nil := "nil"
        | s := "(" ++str go s ++str ")"
      };
end;