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

Set Implicit Arguments.
Unset Strict Implicit. 

Require Import Prelude.Basics.
Require Export Prelude.Applicative.

Open Local Scope applicative.

Reserved Notation " x <|> y " (at level 60, right associativity).

Class Alternative `{app : Applicative f} := {
  (* Operations *)
  empty : Π {α}, f α ;
  alternative : Π {α}, f α ---> f α ---> f α where "x <|> y" := (alternative x y) ;

  (* Properties *)
  alternative_empty_left : Π {α} (x : f α), empty <|> x == x ;

  alternative_empty_right : Π {α} (x : f α), x <|> empty == x ;

  alternative_assoc : Π {α} (x y z : f α), 
    (x <|> y) <|> z == x <|> y <|> z }.

(* Binds less than <$>. *)
Notation " x <|> y " := (alternative x y).

Definition optional `{Alternative f} {a} (v : f a) : f (option_setoid a) :=
  SomeS <$> v <|> pure NoneS.

Program Definition optionalS `{Alternative f} {a} : f a ---> f (option_setoid a) :=
  mkMap optional.

  Next Obligation. simpl_morph. 
    unfold optional. rewrite Hxy. reflexivity.
  Qed.