Library MetaCoq.Template.monad_utils

Class Monad@{d c} (m : Type@{d} → Type@{c}) : Type :=
{ ret : ∀ {t : Type@{d}}, t → m t
; bind : ∀ {t u : Type@{d}}, m t → (t → m u) → m u
}.

Class MonadExc E (m : Type → Type) : Type :=
{ raise : ∀ {T}, E → m T
; catch : ∀ {T}, m T → (E → m T) → m T
}.

Module MonadNotation.

  Notation "c >>= f" := (@bind _ _ _ _ c f) (at level 50, left associativity) : monad_scope.
  Notation "f =<< c" := (@bind _ _ _ _ c f) (at level 51, right associativity) : monad_scope.

  Notation "'mlet' x <- c1 ;; c2" := (@bind _ _ _ _ c1 (fun x ⇒ c2))
    (at level 100, c1 at next level, right associativity, x pattern) : monad_scope.

  Notation "x <- c1 ;; c2" := (@bind _ _ _ _ c1 (fun x ⇒ c2))
    (at level 100, c1 at next level, right associativity) : monad_scope.

  Notation "e1 ;; e2" := (_ <- e1%monad ;; e2%monad)%monad
    (at level 100, right associativity) : monad_scope.
End MonadNotation.


Instance option_monad : Monad option :=
  {| ret A a := Some a ;
     bind A B m f :=
       match m with
       | Some a ⇒ f a
       | None ⇒ None
       end
  |}.


Section MapOpt.
  Context {A} (f : A → option A).

  Fixpoint mapopt (l : list A) : option (list A) :=
    match l with
    | nil ⇒ ret nil
    | x :: xs ⇒ x' <- f x ;;
                xs' <- mapopt xs ;;
                ret (x' :: xs')
    end.
End MapOpt.

Section MonadOperations.
  Context {T} {M : Monad T}.
  Context {A B} (f : A → T B).
  Fixpoint monad_map (l : list A)
    : T (list B)
    := match l with
       | nil ⇒ ret nil
       | x :: l ⇒ x' <- f x ;;
                  l' <- monad_map l ;;
                  ret (x' :: l')
       end.

  Context (g : A → B → T A).
  Fixpoint monad_fold_left (l : list B) (x : A) : T A
    := match l with
       | nil ⇒ ret x
       | y :: l ⇒ x' <- g x y ;;
                   monad_fold_left l x'
       end.

  Context (h : nat → A → T B).
  Fixpoint monad_map_i_aux (n0 : nat) (l : list A) : T (list B)
    := match l with
       | nil ⇒ ret nil
       | x :: l ⇒ x' <- (h n0 x) ;;
                   l' <- (monad_map_i_aux (S n0) l) ;;
                   ret (x' :: l')
       end.

  Definition monad_map_i := @monad_map_i_aux 0.
End MonadOperations.

Definition monad_iter {T : Type → Type} {M A} (f : A → T unit) (l : list A) : T unit
  := @monad_fold_left T M _ _ (fun _ ⇒ f) l tt.