Commits

Anonymous committed 5a1d410

ErrorMonad renames: err -> error, Eok -> Ok, Eerr -> Error

Comments (0)

Files changed (1)

   - throw {A} : E -> m A
   - catch : m A -> (E -> m A) -> m A
   - run_error : m A -> InnerMonad.m (err E A)
-    where Inductive err E A := | Eok a | Eerr e.
+    where Inductive error E A := | Ok a | Error e.
 *)
 
 
 Require Import Monads.
 
-Inductive err E A :=
-| Eok : A -> err E A
-| Eerr : E -> err E A
+Inductive error E A :=
+| Ok : A -> error E A
+| Error : E -> error E A
 .
 
-Implicit Arguments Eok [E A].
-Implicit Arguments Eerr [E A].
+Implicit Arguments Ok [E A].
+Implicit Arguments Error [E A].
 
 
 Module Type ERR_TYPE.
 
 (* for MapError: *)
 Module Type ERROR_T (Et : ERR_TYPE) (M : MONAD).
-  Definition m A := M.m (err Et.E A).
+  Definition m A := M.m (error Et.E A).
 End ERROR_T.
 
 
 <: ERROR_T (Et) (M).
 
   Module Mo.
-  Definition tm A := M.m (err Et.E A).
+  Definition tm A := M.m (error Et.E A).
 
   Definition ret A (a : A) : tm A :=
-    M.ret (Eok a)
+    M.ret (Ok a)
   .
   Global Implicit Arguments ret [[A]].
 
     M.bind
       (fun ea =>
          match ea with
-         | Eok a => f a
-         | Eerr e => M.ret (Eerr e)
+         | Ok a => f a
+         | Error e => M.ret (Error e)
          end
       )
       tma
     M.bind
       (fun ea =>
          match ea with
-         | Eok _ => M.ret ea
-         | Eerr e => M.ret (Eerr (mapper e))
+         | Ok _ => M.ret ea
+         | Error e => M.ret (Error (mapper e))
          end
       )
       tma
 
   (* specific functions *)
 
-  Definition throw {A} (e : Et.E) : m A := M.ret (@Eerr Et.E A e).
+  Definition throw {A} (e : Et.E) : m A := M.ret (@Error Et.E A e).
 
   Definition catch {A} (ma : m A)
     (handler : Et.E -> m A)
     M.bind
       (fun ea =>
          match ea with
-         | Eok _ => M.ret ea
-         | Eerr e => handler e
+         | Ok _ => M.ret ea
+         | Error e => handler e
          end
       )
       ma
   .
 
-  Definition run_error {A} (tma : tm A) : M.m (err Et.E A) :=
+  Definition run_error {A} (tma : tm A) : M.m (error Et.E A) :=
     tma
   .
 
     M.bind
       (fun ea =>
          match ea with
-         | Eok a => M.ret (Eok a)
-         | Eerr e => M.ret (Eerr (mapper e))
+         | Ok a => M.ret (Ok a)
+         | Error e => M.ret (Error (mapper e))
          end
       )
       m1