(* -*- coq-prog-args: ("-emacs-U" "-R" "." "Prelude") -*- *)
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(* Certified Haskell Prelude.
 * Author: Matthieu Sozeau
 * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
 *              91405 Orsay, France *)

(* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *)

Require Import Prelude.Monad.

Set Implicit Arguments.
Unset Strict Implicit.
  
Definition state (s a : Type) : Type := s -> (a * s).
  
Program Instance state_monad : Monad (state s) :=
  unit A a := fun s => (a, s) ;
  bind A B m f := fun s => prod_curry f (m s).

  Next Obligation.
  Proof.
    rewrite -> (eta_expansion (f x)).
    reflexivity.
  Qed.
  
  Next Obligation.
  Proof.
    extensionality y.
    elim (x y).
    reflexivity.
  Qed.
  
  Next Obligation.
  Proof.
    extensionality y.
    elim (x y) ; intros.
    reflexivity.
  Qed.

Definition eval_state {s a} (S : state s a) (init : s) : a :=
  fst (S init).

Definition exec_state {s a} (S : state s a) (init : s) : s :=
  snd (S init).

Definition map_state {s a b} (f : (a * s) -> (b * s)) (S : state s a) : state s b :=
  fun s => f (S s).

Definition with_state {s a} (f : s -> s) (S : state s a) : state s a := S ∘ f.

Require Import Datatypes.

Class [ Monad m ] => MonadState (s : Type) :=
  get : m s ;
  put : s -> m unit.

Definition modify [ MonadState m s ] (f : s -> s) : m unit :=
  x <- get ;; put (f x).

Definition gets [ MonadState m s ] {a} (f : s -> a) : m a :=
  x <- get ;; return (f x).

Program Instance state_state_monad : ! MonadState (state s) s :=
  get s := (s, s) ;
  put x s := (tt, x).

(** The State Monad transformer. *)

Definition stateT s (m : Type -> Type) (a : Type) : Type := 
  s -> m (a * s)%type.

Lemma eta_prod_return [ Monad m ] : forall a b (t : prod a b), (let (x,y) := t in return (x,y)) = return t.
Proof.
  destruct t ; reflexivity.
Qed.

Program Instance [ Monad m ] => stateT_monad : Monad (stateT s m) :=
  unit A a := fun s => return (a, s) ;
  bind A B m f := fun s => t <- m s ;; (prod_curry f) t.

  Next Obligation.
  Proof.
    unfold stateT in f.
    extensionality s'.
    rewrite bind_unit_left.
    reflexivity.
  Qed.
  
  Next Obligation.
  Proof.
    unfold stateT in x.
    extensionality s'.
    rewrite <- bind_unit_right.
    apply bind_eq_l.
    extensionality s''.
    destruct s'' ; simpl. 
    reflexivity.
  Qed.
  
  Next Obligation.
  Proof.
    unfold stateT in x, f, g.
    extensionality s'.
    rewrite <- bind_assoc.
    apply bind_eq_l.
    extensionality t.
    destruct t ; simpl. reflexivity.
  Qed.

Program Instance [ Monad m ] => stateT_monadstate : ! MonadState (stateT s m) s :=
  get := fun s => return (s, s) ;
  put x := fun _ => return (tt, x).
    
Definition eval_stateT {s} [ Monad m ] {a} (S : stateT s m a) (init : s) : m a :=
  x <- S init ;; return fst x.

Definition exec_stateT {s} [ Monad m ] {a} (S : stateT s m a) (init : s) : m s :=
  x <- S init ;; return snd x.

Definition map_stateT {s} {m n : Type -> Type} {a b} (f : m (a * s)%type -> n (b * s)%type) (S : stateT s m a) : stateT s n b :=
  fun s => f (S s).

Definition with_stateT {s m a} (f : s -> s) (S : stateT s m a) : stateT s m a := S ∘ f.

Require Import Prelude.MonadTransformer.

Program Instance stateT_monadtrans : MonadTrans (stateT s) :=
  lift := fun [ Monad m ] A t => fun s => x <- t ;; return (x, s).