module Stdlib.Data.Maybe;

import Stdlib.Data.Maybe.Base open public;

import Stdlib.Trait.Eq open;
import Stdlib.Trait.Ord open;
import Stdlib.Trait.Show open;
import Stdlib.Trait.Functor open;
import Stdlib.Trait.Applicative open;
import Stdlib.Trait.Monad open;

import Stdlib.Data.Bool.Base open;
import Stdlib.Data.String.Base open;
import Stdlib.Data.Pair.Base open;

{-# specialize: true, inline: case #-}
deriving instance
eqMaybeI {A} {{Eq A}} : Eq (Maybe A);

instance
showMaybeI {A} {{Show A}} : Show (Maybe A) :=
  mkShow@{
    show (m : Maybe A) : String :=
      case m of
        | nothing := "nothing"
        | just a := "just " ++str Show.show a;
  };

{-# specialize: true, inline: case #-}
deriving instance
ordMaybeI {A} {{Ord A}} : Ord (Maybe A);

{-# specialize: true, inline: case #-}
instance
functorMaybeI : Functor Maybe :=
  mkFunctor@{
    map {A B} (f : A -> B) : Maybe A -> Maybe B
      | nothing := nothing
      | (just a) := just (f a);
  };

{-# specizalize: true, inline: true #-}
instance
monomorphicFunctorMaybeI {A} : Monomorphic.Functor (Maybe A) A :=
  fromPolymorphicFunctor;

instance
applicativeMaybeI : Applicative Maybe :=
  mkApplicative@{
    pure := just;
    ap {A B} (listOfFuns : Maybe (A -> B)) (list : Maybe A) : Maybe B :=
      case listOfFuns, list of
        | just f, just x := just (f x)
        | _, _ := nothing;
  };

instance
monadMaybeI : Monad Maybe :=
  mkMonad@{
    bind {A B} (maybe : Maybe A) (fun : A -> Maybe B) : Maybe B :=
      case maybe of
        | nothing := nothing
        | just a := fun a;
  };