X-Git-Url: http://git.megacz.com/?p=coinductive-monad.git;a=blobdiff_plain;f=Computation%2FMonad.v;fp=Computation%2FMonad.v;h=082a3dd2d8b0710184a41dbbb64cb105e0bc7faa;hp=0000000000000000000000000000000000000000;hb=ad8905d391e4e2015b6525a81a3b5e1ad607439e;hpb=7439e43c33a10817e19e7a5f26435d2097dc262d

diff --git a/Computation/Monad.v b/Computation/Monad.v
new file mode 100644
index 0000000..082a3dd
--- /dev/null
+++ b/Computation/Monad.v
@@ -0,0 +1,32 @@
+Reserved Notation "# A" (at level 30).
+Section Constructors.
+
+  (* a co-inductive type representing a possibly-nonterminating computation *)
+     CoInductive Computation (A:Set) : Type :=
+
+  (* terminate and return a value *)
+       | Return  : A                               -> #A
+         
+  (* monadic >>= (bind) operator *)
+       | Bind    : forall (B:Set),  (B->#A) ->  #B -> #A
+         where "# A" := (Computation A).
+     Implicit Arguments Return [A].
+     Implicit Arguments Bind [A B].
+     Notation "c >>= f" := (Bind f c) (at level 20).
+     
+End Constructors.
+
+Notation "# A" := (Computation A).
+Implicit Arguments Return [A].
+Implicit Arguments Bind [A B].
+Notation "c >>= f" := (Bind f c) (at level 20).
+
+Notation "'call' c" :=
+  (c >>= (fun x=>(Return x)))
+  (at level 60, right associativity)
+.
+
+Notation "var <- c ; rest" := 
+  (* I need this "fun" to tell the parser that "var" is bound *)
+  (c >>= (fun var => rest))
+  (at level 60, right associativity).