Require Import Options.
Require Import CBase.
Require Import CDestruct.

Class MLift (M M' : Type → Type) := mlift_in : ∀ A, M A → M' A.
Arguments mlift_in {_ _ _ _}.
Hint Mode MLift - ! : typeclass_instances.
Class MLiftT (M M' : Type → Type) := mlift : ∀ A, M A → M' A.
Arguments mlift {_ _ _ _}.
Hint Mode MLiftT ! ! : typeclass_instances.
Instance MLiftT_one `{MLift M M'} : MLiftT M M' := ltac:(assumption).
Instance MLiftT_trans `{MLift M' M'', MLiftT M M'} : MLiftT M M'' :=
  λ A x, mlift_in (mlift x).

Instance idM_lift_all `{MRet M} : MLift idM M := λ A x, mret x.

Class Functor F `{FMap F} := {
    functor_id {A} : fmap id =@{F A → F A} id;
    functor_assoc {A B C} (f : A → B) (g : B → C) :
    fmap (g ∘ f) =@{F A → F C} fmap g ∘ fmap f
  }.

Class Monad M `{MRet M, MBind M} := {
    monad_left_id {A B} (a : A) (f : A → M B): mret a ≫= f = f a;
    monad_right_id : ∀ {A} (f : M A), f ≫= mret = f;
    monad_assoc : ∀ {A B C} (a : M A) (f : A → M B) (g : B → M C),
      a ≫= (λ x, f x ≫= g) = (a ≫= f) ≫= g;
  }.
Class MonadFMap M `{Monad M, FMap M} :=
  monad_fmap : ∀ {A B} (f : A → B), fmap f =@{M A → M B} mbind (λ x, mret (f x)).

Instance csimp_mon_left_id `{Monad M} {A B} (a : A) (f : A → M B) :
  mret a ≫= f ⇒ f a. Proof. apply monad_left_id. Qed.

Instance csimp_mon_right_id `{Monad M} {A} (f : M A) : f ≫= mret ⇒ f.
Proof. apply monad_right_id. Qed.

Instance csimp_monad_assoc `{Monad M} {A B C} (a : M A) (f : A → M B) (g : B → M C):
  a ≫= (λ x : A, f x ≫= g) ⇒ (a ≫= f) ≫= g.
Proof. apply monad_assoc. Qed.

Instance Functor_MonadFMap `{MonadFMap M} : Functor M.
Proof.
  split.
  - intros A.
    rewrite monad_fmap.
    extensionality x.
    by csimp.
  - intros A B C f g.
    rewrite ?monad_fmap.
    extensionality x.
    cbn.
    rewrite <- monad_assoc.
    setoid_rewrite monad_left_id.
    reflexivity.
Qed.

Lemma fmap_mret `{MonadFMap M} `(x : A) `(f : A → B) : f <$> mret x =@{M B} mret (f x).
Proof. rewrite monad_fmap. by csimp. Qed.

Instance csimp_fmap_mret `{MonadFMap M} {A B} (a : A) (f : A → B) :
  f <$> mret (M := M) a ⇒ mret (f a).
Proof. apply fmap_mret. Qed.

Fixpoint foldlM {A B} `{MRet M, MBind M} (f : A → B → M A) (a : A) (l : list B) : M A :=
  if l is hd :: tl then
    v ← (f a hd);
    foldlM f v tl
  else mret a.

Fixpoint foldrM {A B} `{MRet M, MBind M} (f : B → A → M A) (l : list B) (a : A) : M A :=
  if l is hd :: tl then
    v ← foldrM f tl a;
    f hd v
  else mret a.