Commits

Anonymous committed b40599e Draft

evars

  • Participants
  • Parent commits 07ce437

Comments (0)

Files changed (1)

File ErrorMonad.v

-Require Import Monads.
-
-Require Import FunctionalExtensionality.
-
-
-Inductive resG (e : Type) (a : Type) :=
-  | Ok : a -> resG e a
-  | Error : e -> resG e a
-.
-
-Definition resT e {m : Type -> Type} (M : Monad m) a :=
-  m (resG e a).
-
-Definition res e := resT e Identity.
-
-Implicit Arguments Ok [e a].
-Implicit Arguments Error [e a].
-
-
-Class ErrorMonadT
-(e : Type)
-{m : Type -> Type}
-(M : Monad m)
-:=
-  { throw : forall {a : Type},
-      e -> res e (m a)
-  ; catch : forall {a : Type},
-      res e (m a) -> (e -> res e (m a)) -> res e (m a)
-  }
-.
-
-Instance ErrorT
-(e : Type)
-{m : Type -> Type}
-(M : Monad m)
-: ErrorMonadT e M
-:=
-  {| throw := fun {a : Type} (err : e) =>
-       Error err
-   ; catch := fun
-       {a : Type}
-       (ra : res e (m a))
-       (handler : e -> res e (m a)) =>
-         match ra with
-         | Ok r => Ok r
-         | Error r => handler r
-         end
-   |}.
-
-
-Instance ErrorT_Monad_inst
-  (e : Type)
-  {m : Type -> Type}
-  (M : Monad m)
-: Monad (resT e M)
-:=
-  {| ret := fun {A} (a : A) => ret (Ok a)
-   ; bind := fun
-       {A B}
-       (ma : resT e M A)
-       (f : A -> resT e M B) =>
-         (ma : m (res e A)) >>= fun (a : res e A) =>
-         match a with
-         | Ok r => f r
-         | Error r => ret (Error r)
-         end
-   |}
-.
-(* 0 *)
-  intros. rewrite Monad0. reflexivity.
-(* 1 *)
-  intros. unfold resT in *. rewrite <- Monad1.
-  f_equal. extensionality q. destruct q; reflexivity.
-(* 2 *)
-  intros. unfold resT in *.
-  rewrite Monad2.
-  f_equal. extensionality q.
-  destruct q.
-  (* 2.1 *)
-    reflexivity.
-  (* 2.2 *)
-    rewrite Monad0.
-    reflexivity.
-Defined.
-
-
-Instance ErrorT_MonadTrans_inst
-  (e : Type)
-  {m : Type -> Type}
-  {M : Monad m}
-: MonadTrans (@resT e)
-:=
-  {| lift := fun {A} (ma : m A) =>
-       a <- ma;;
-       ret (Ok a)
-   |}
-.
-(* T0 *)
-  intros. extensionality q. rewrite Monad0. simpl. reflexivity.
-(* T1 *)
-  intros. simpl.
-  rewrite Monad2.
-  rewrite Monad2.
-  f_equal.
-  extensionality q.
-  rewrite Monad0.
-  reflexivity.
-Defined.
-
-
-Module Example.
-
-  Require Import StateMonad.
-
-  Inductive myerr :=
-    | Zero
-    | Empty
-  .
-
-  Require Import Eqdec.
-
-  Fixpoint test1_aux lst : res myerr nat :=
-    match lst with
-    | nil => ret 0
-    | cons h t =>
-        if eq_dec h 0
-        then throw Zero
-        else rest <- test1_aux t;; ret (h + rest)
-    end
-  .
-
-  Notation "f $ x" := (f x)
-    (at level 63, right associativity, only parsing).
-
-  Require Import List.
-
-  Definition test1 (lst : list nat) : res myerr (list nat) :=
-    if eq_dec lst nil
-    then throw Empty (M := Identity)
-    else
-      h <- test1_aux lst;;
-      ret $ h :: lst
-  .
-
-  Eval compute in test1 (1 :: 2 :: 3 :: nil).
-  Eval compute in test1 (1 :: 0 :: 3 :: nil).
-  Eval compute in test1 nil.
-
-Check test1.
-
-
-Typeclasses eauto := debug bfs.
-
-  Definition test2
- : resT myerr (@StateT_Monad_inst bool identity_type Identity) (list nat)
-   :=
-    lift $ (put true);;
-    r <-
-      (catch
-        (test1 nil)
-        (fun e =>
-           match e with
-           | Zero => ret (0 :: nil)
-           | _ => throw e
-           end
-        )
-      )
-      (fun e =>
-         match e with
-         | Empty =>
-             b <- lift $ get;;
-             if b:bool
-             then (100 :: nil)
-             else (200 :: nil)
-         | _ => throw e
-         end
-      );;
-    ret $ 123 :: r
-  .
-
-
-End Example.
-
-
+Require Import Monads.
+
+Require Import FunctionalExtensionality.
+
+
+Inductive resG (e : Type) (a : Type) :=
+  | Ok : a -> resG e a
+  | Error : e -> resG e a
+.
+
+Definition resT e {m : Type -> Type} (M : Monad m) a :=
+  m (resG e a).
+
+Definition res e := resT e Identity.
+
+Implicit Arguments Ok [e a].
+Implicit Arguments Error [e a].
+
+
+Class ErrorMonadT
+(e : Type)
+{m : Type -> Type}
+(M : Monad m)
+:=
+  { throw : forall {a : Type},
+      e -> res e (m a)
+  ; catch : forall {a : Type},
+      res e (m a) -> (e -> res e (m a)) -> res e (m a)
+  }
+.
+
+Instance ErrorT
+(e : Type)
+{m : Type -> Type}
+(M : Monad m)
+: ErrorMonadT e M
+:=
+  {| throw := fun {a : Type} (err : e) =>
+       Error err
+   ; catch := fun
+       {a : Type}
+       (ra : res e (m a))
+       (handler : e -> res e (m a)) =>
+         match ra with
+         | Ok r => Ok r
+         | Error r => handler r
+         end
+   |}.
+
+
+Instance ErrorT_Monad_inst
+  (e : Type)
+  {m : Type -> Type}
+  (M : Monad m)
+: Monad (resT e M)
+:=
+  {| ret := fun {A} (a : A) => ret (Ok a)
+   ; bind := fun
+       {A B}
+       (ma : resT e M A)
+       (f : A -> resT e M B) =>
+         (ma : m (res e A)) >>= fun (a : res e A) =>
+         match a with
+         | Ok r => f r
+         | Error r => ret (Error r)
+         end
+   |}
+.
+(* 0 *)
+  intros. rewrite Monad0. reflexivity.
+(* 1 *)
+  intros. unfold resT in *. rewrite <- Monad1.
+  f_equal. extensionality q. destruct q; reflexivity.
+(* 2 *)
+  intros. unfold resT in *.
+  rewrite Monad2.
+  f_equal. extensionality q.
+  destruct q.
+  (* 2.1 *)
+    reflexivity.
+  (* 2.2 *)
+    rewrite Monad0.
+    reflexivity.
+Defined.
+
+
+Instance ErrorT_MonadTrans_inst
+  (e : Type)
+  {m : Type -> Type}
+  {M : Monad m}
+: MonadTrans (@resT e)
+:=
+  {| lift := fun {A} ma =>
+       a <- ma;;
+       ret (Ok a)
+   |}
+.
+(* T0 *)
+  intros. extensionality q. rewrite Monad0. simpl. reflexivity.
+(* T1 *)
+  intros. simpl.
+  rewrite Monad2.
+  rewrite Monad2.
+  f_equal.
+  extensionality q.
+  rewrite Monad0.
+  reflexivity.
+Defined.
+
+
+Module Example.
+
+  Require Import StateMonad.
+
+  Inductive myerr :=
+    | Zero
+    | Empty
+  .
+
+  Require Import Eqdec.
+
+  Fixpoint test1_aux lst : res myerr nat :=
+    match lst with
+    | nil => ret 0
+    | cons h t =>
+        if eq_dec h 0
+        then throw Zero
+        else rest <- test1_aux t;; ret (h + rest)
+    end
+  .
+
+  Notation "f $ x" := (f x)
+    (at level 63, right associativity, only parsing).
+
+  Require Import List.
+
+  Definition test1 (lst : list nat) : res myerr (list nat) :=
+    if eq_dec lst nil
+    then throw Empty (M := Identity)
+    else
+      h <- test1_aux lst;;
+      ret $ h :: lst
+  .
+
+  Eval compute in test1 (1 :: 2 :: 3 :: nil).
+  Eval compute in test1 (1 :: 0 :: 3 :: nil).
+  Eval compute in test1 nil.
+
+Check test1.
+
+
+Typeclasses eauto := debug bfs.
+
+  Definition test2
+ : resT myerr (@StateT_Monad_inst bool identity_type Identity) (list nat)
+   :=
+    lift $ (put true);;
+    r <-
+      (catch
+        (test1 nil)
+        (fun e =>
+           match e with
+           | Zero => ret (0 :: nil)
+           | _ => throw e
+           end
+        )
+      )
+      (fun e =>
+         match e with
+         | Empty =>
+             b <- lift $ get;;
+             if b:bool
+             then (100 :: nil)
+             else (200 :: nil)
+         | _ => throw e
+         end
+      );;
+    ret $ 123 :: r
+  .
+
+
+End Example.
+
+