Add MRaise typeclass

This is an alternative to MFail in #488. It allows a monad to present a general error raising mechanism. This includes an example instantiation for option. I didn't do the work of #488 to completely replace MGuard, but if we decide to use this instead of MFail, we can merge the two patches.

stdpp/base.v

@@ -1204,6 +1204,42 @@ Notation "'guard' P ; z" := (mguard P (λ _, z))
 Notation "'guard' P 'as' H ; z" := (mguard P (λ H, z))
   (at level 20, z at level 200, only parsing, right associativity) : stdpp_scope.
 
+(** For any monad that had a builtin way to raise an exception *)
+Class MRaise (E : Type) (M : Type → Type) := mraise : ∀ {A}, E → M A.
+Global Arguments mraise {_ _ _ _} _ : assert.
+Global Instance: Params (@mraise) 4 := {}.
+Global Hint Mode MRaise ! ! : typeclass_instances.
+
+(** We use unit as the error content for monads that can report an error without
+    payload like an option *)
+Definition mfail `{MRaise () M} {A} : M A := mraise ().
+
+(** mguard or, like mguard but one can specify the error in case of failure *)
+Definition mguard_or `{MRaise E M} P {dec : Decision P} {A}
+    (e : E) (f : P → M A) : M A :=
+  match decide P with
+  | left p => f p
+  | right _ => mraise e
+  end.
+Notation "'guard' P 'or' e ; z" := (mguard_or P e (λ _, z))
+  (at level 20, z at level 200, only parsing, right associativity) : stdpp_scope.
+Notation "'guard' P 'or' e 'as' H ; z" := (mguard_or P e (λ H, z))
+  (at level 20, z at level 200, only parsing, right associativity) : stdpp_scope.
+
+(* mfail replaces MGuard *)
+Global Instance mguard_mfail `{MRaise () M} : MGuard M :=
+  {mguard P _ _ f := mguard_or P () f}.
+
+Global Instance option_raise : MRaise () option := {mraise _ _ := None}.
+
+(** Unpack an option by raising an specified error if None *)
+Definition oraise `{MRaise E M} `{MRet M} {A} (err : E) (v : option A) : M A :=
+  match v with
+  | None => mraise err
+  | Some x => mret x
+  end.
+
+
 (** * Operations on maps *)
 (** In this section we define operational type classes for the operations
 on maps. In the file [fin_maps] we will axiomatize finite maps.