gistfile1.v

From ExtLib.Structures Require Import Monad MonadWriter MonadExc Monoid.
From ExtLib.Data Require Import Monads.WriterMonad List.
Require Import ZArith.

Import MonadNotation.

Open Scope monad.

Section Error.

Context {E : Type}.
Context {T : Type}.
Context {MT : Monoid T}.

Definition errW A := T -> E + (T * A).

Global Instance Monad_errW : Monad errW := {
  ret := fun _ x => fun w => inr (w, x) ;
  bind := fun _ _ m f => fun w => match m w with
                            | inl v => inl v
                            | inr (w', x) => f x w'
                            end
}.

Global Instance Exception_errW : MonadExc E errW := {
  raise := fun _ v => fun w => inl v ;
  catch := fun _ c h => fun w => match c w with
                           | inl v => h v w
                           | inr x => inr x
                           end
}.

Global Instance Writer_errW : MonadWriter MT errW := {
  tell := fun w => fun _ => inr (w, tt) ;
  listen := fun _ m => fun w => match m w with 
                          | inl v => inl v 
                          | inr (w', x) => inr (w', (x, w'))
                          end ;
  pass := fun _ m => fun w => match m w with
                        | inl v => inl v
                        | inr (w', (x, f)) => inr (f w', x)
                        end ;
}.

Definition evalErrW {A : Type} (e : errW A) (init : T) : option A := 
  match e init with
  | inl _ => None
  | inr (_, v) => Some v
  end.

Definition execErrW {A : Type} (e : errW A) (init : T) : option T :=
  match e init with
  | inl _ => None
  | inr (w, _) => Some w
  end.

End Error.


Section Test.

Definition errW1 := @errW nat (list Z).

(*
Existing Class Monoid.
Existing Instance Monoid_list_app.
*)

Definition test : errW1 unit := tell (cons 1%Z nil).

End Test.