(************************************************************************)
(*  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.

Class [ Monad m ] => MonadCont :=
  callCC : forall {a b}, ((a -> m b) -> m a) -> m a.

Definition cont (R A : Type) := (A -> R) -> R.

Definition map_cont {R A} (f : R -> R) (c : cont R A) : cont R A := f ∘ c.

Definition with_cont {R A B} (f : (B -> R) -> A -> R) (c : cont R A) : cont R B := c ∘ f.

Program Instance continuation_monad : Monad (cont R) :=
  unit A a := fun k => k a ;
  bind A B x f := fun k => x (fun a => f a k).

  Next Obligation.
  Proof.
    generalize (f x) ; intros.
    rewrite eta_expansion ; auto.
  Qed.

  Next Obligation.
  Proof.
    unfold cont in x.
    rewrite eta_expansion.
    extensionality k.
    f_equal.
    rewrite eta_expansion ; auto.
  Qed.

Program Instance continuation_monadcont : ! MonadCont (cont R) :=
  callCC A B f := fun k : A -> R => f (fun a _ => k a) k.

(** Continuation monad transformer. *)

Definition contT R (m : Type -> Type) (A : Type) := (A -> m R) -> m R.

Program Instance [ Monad m ] => contT_monad : Monad (contT R m) :=
  unit A a := fun k => k a ;
  bind A B x f := fun k => x (fun a => f a k).

  Next Obligation.
  Proof.
    extensionality k ; reflexivity.
  Qed.
  
  Next Obligation.
  Proof.
    rewrite eta_expansion.
    extensionality k.  f_equal. rewrite eta_expansion ; reflexivity.
  Qed.

Program Instance [ Monad m ] => contT_monadcont : ! MonadCont (contT R m) :=
  callCC A B f := fun k => f (fun a _ => k a) k.

Require Import Prelude.MonadTransformer.

Program Instance contT_monad_trans : MonadTrans (contT R) :=
  lift m mon A := bind.