diff --git a/example/Example.v b/example/Example.v
new file mode 100644
index 0000000000000000000000000000000000000000..1d122032e96365e3f9d2b786d118aa1b8dc746e9
--- /dev/null
+++ b/example/Example.v
@@ -0,0 +1,51 @@
+(* This software is governed by the CeCILL license under French law and
+ * abiding by the rules of distribution of free software. You can use,
+ * modify and/ or redistribute the software under the terms of the CeCILL
+ * license as circulated by CEA, CNRS and INRIA at the following URL
+ * "http://www.cecill.info".
+
+ * As a counterpart to the access to the source code and rights to copy,
+ * modify and redistribute granted by the license, users are provided only
+ * with a limited warranty and the software's author, the holder of the
+ * economic rights, and the successive licensors have only limited
+ * liability.
+
+ * In this respect, the user's attention is drawn to the risks associated
+ * with loading, using, modifying and/or developing or reproducing the
+ * software by the user in light of its specific status of free software,
+ * that may mean that it is complicated to manipulate, and that also
+ * therefore means that it is reserved for developers and experienced
+ * professionals having in-depth computer knowledge. Users are therefore
+ * encouraged to load and test the software's suitability as regards their
+ * requirements in conditions enabling the security of their systems and/or
+ * data to be ensured and, more generally, to use and operate it in the
+ * same conditions as regards security.
+
+ * The fact that you are presently reading this means that you have had
+ * knowledge of the CeCILL license and that you accept its terms.
+ *)
+
+(* This Coq module uses the monad defined in the Monad module to
+ describe sequential computations. *)
+
+Require Import Monad Internals.
+Open Scope monad_scope.
+
+Definition id (b : bool) : M bool := returnM b.
+
+Definition neg (b : bool) : M bool := if b then returnM false else returnM true.
+
+Fixpoint prepare recBound : M unit :=
+ match recBound with
+ | O => emptyM
+ | S b => do r <- ready ;
+ if r
+ then returnM tt
+ else do _ <- getReady ;
+ prepare b
+ end.
+
+Eval compute in runM (id true) 12.
+Eval compute in runM (neg true) 12.
+Eval compute in runM (prepare 1) 1.
+Eval compute in runM (prepare 2) 1.
\ No newline at end of file
diff --git a/example/Extraction.v b/example/Extraction.v
new file mode 100644
index 0000000000000000000000000000000000000000..c77e62609d62e87351331431496cc81743fe9a0c
--- /dev/null
+++ b/example/Extraction.v
@@ -0,0 +1,34 @@
+(* This software is governed by the CeCILL license under French law and
+ * abiding by the rules of distribution of free software. You can use,
+ * modify and/ or redistribute the software under the terms of the CeCILL
+ * license as circulated by CEA, CNRS and INRIA at the following URL
+ * "http://www.cecill.info".
+
+ * As a counterpart to the access to the source code and rights to copy,
+ * modify and redistribute granted by the license, users are provided only
+ * with a limited warranty and the software's author, the holder of the
+ * economic rights, and the successive licensors have only limited
+ * liability.
+
+ * In this respect, the user's attention is drawn to the risks associated
+ * with loading, using, modifying and/or developing or reproducing the
+ * software by the user in light of its specific status of free software,
+ * that may mean that it is complicated to manipulate, and that also
+ * therefore means that it is reserved for developers and experienced
+ * professionals having in-depth computer knowledge. Users are therefore
+ * encouraged to load and test the software's suitability as regards their
+ * requirements in conditions enabling the security of their systems and/or
+ * data to be ensured and, more generally, to use and operate it in the
+ * same conditions as regards security.
+
+ * The fact that you are presently reading this means that you have had
+ * knowledge of the CeCILL license and that you accept its terms.
+ *)
+
+(* This Coq module uses the monad defined in the Monad module to
+ describe sequential computations. *)
+
+Require Import Internals Example.
+Extraction Language JSON.
+Extraction Library Internals.
+Extraction Library Example.
diff --git a/example/Internals.c b/example/Internals.c
new file mode 100644
index 0000000000000000000000000000000000000000..41482d5ef224328ee06bb8816df9a0dd95e096b4
--- /dev/null
+++ b/example/Internals.c
@@ -0,0 +1,39 @@
+/* This software is governed by the CeCILL license under French law and
+ * abiding by the rules of distribution of free software. You can use,
+ * modify and/ or redistribute the software under the terms of the CeCILL
+ * license as circulated by CEA, CNRS and INRIA at the following URL
+ * "http://www.cecill.info".
+
+ * As a counterpart to the access to the source code and rights to copy,
+ * modify and redistribute granted by the license, users are provided only
+ * with a limited warranty and the software's author, the holder of the
+ * economic rights, and the successive licensors have only limited
+ * liability.
+
+ * In this respect, the user's attention is drawn to the risks associated
+ * with loading, using, modifying and/or developing or reproducing the
+ * software by the user in light of its specific status of free software,
+ * that may mean that it is complicated to manipulate, and that also
+ * therefore means that it is reserved for developers and experienced
+ * professionals having in-depth computer knowledge. Users are therefore
+ * encouraged to load and test the software's suitability as regards their
+ * requirements in conditions enabling the security of their systems and/or
+ * data to be ensured and, more generally, to use and operate it in the
+ * same conditions as regards security.
+
+ * The fact that you are presently reading this means that you have had
+ * knowledge of the CeCILL license and that you accept its terms.
+ */
+
+/* This C source provides possible implementations for the "primitive" functions */
+
+#include "base.h"
+#include "Monad.h"
+
+bool ready() {
+ return state % 2 == 0;
+}
+
+void getReady() {
+ state += state % 2;
+}
diff --git a/example/Internals.h b/example/Internals.h
new file mode 100644
index 0000000000000000000000000000000000000000..efb7cbf3531d78e87e7a3eee199378da49132935
--- /dev/null
+++ b/example/Internals.h
@@ -0,0 +1,31 @@
+/* This software is governed by the CeCILL license under French law and
+ * abiding by the rules of distribution of free software. You can use,
+ * modify and/ or redistribute the software under the terms of the CeCILL
+ * license as circulated by CEA, CNRS and INRIA at the following URL
+ * "http://www.cecill.info".
+
+ * As a counterpart to the access to the source code and rights to copy,
+ * modify and redistribute granted by the license, users are provided only
+ * with a limited warranty and the software's author, the holder of the
+ * economic rights, and the successive licensors have only limited
+ * liability.
+
+ * In this respect, the user's attention is drawn to the risks associated
+ * with loading, using, modifying and/or developing or reproducing the
+ * software by the user in light of its specific status of free software,
+ * that may mean that it is complicated to manipulate, and that also
+ * therefore means that it is reserved for developers and experienced
+ * professionals having in-depth computer knowledge. Users are therefore
+ * encouraged to load and test the software's suitability as regards their
+ * requirements in conditions enabling the security of their systems and/or
+ * data to be ensured and, more generally, to use and operate it in the
+ * same conditions as regards security.
+
+ * The fact that you are presently reading this means that you have had
+ * knowledge of the CeCILL license and that you accept its terms.
+ */
+
+/* This C header provides the prototypes for the "primitive" functions */
+
+bool ready();
+void getReady();
diff --git a/example/Internals.v b/example/Internals.v
new file mode 100644
index 0000000000000000000000000000000000000000..f5653a37d681a7a410c5a45b587e3d672a7d5ef1
--- /dev/null
+++ b/example/Internals.v
@@ -0,0 +1,43 @@
+(* This software is governed by the CeCILL license under French law and
+ * abiding by the rules of distribution of free software. You can use,
+ * modify and/ or redistribute the software under the terms of the CeCILL
+ * license as circulated by CEA, CNRS and INRIA at the following URL
+ * "http://www.cecill.info".
+
+ * As a counterpart to the access to the source code and rights to copy,
+ * modify and redistribute granted by the license, users are provided only
+ * with a limited warranty and the software's author, the holder of the
+ * economic rights, and the successive licensors have only limited
+ * liability.
+
+ * In this respect, the user's attention is drawn to the risks associated
+ * with loading, using, modifying and/or developing or reproducing the
+ * software by the user in light of its specific status of free software,
+ * that may mean that it is complicated to manipulate, and that also
+ * therefore means that it is reserved for developers and experienced
+ * professionals having in-depth computer knowledge. Users are therefore
+ * encouraged to load and test the software's suitability as regards their
+ * requirements in conditions enabling the security of their systems and/or
+ * data to be ensured and, more generally, to use and operate it in the
+ * same conditions as regards security.
+
+ * The fact that you are presently reading this means that you have had
+ * knowledge of the CeCILL license and that you accept its terms.
+ *)
+
+(* This Coq module defines a simple state monad with failure, as an
+ example of use of digger to extract some monadic code into C code *)
+
+Require Import Nat Monad.
+Open Scope monad_scope.
+
+Definition ready : M bool :=
+ do s <- get ;
+ returnM (even s).
+
+Definition getReady : M unit :=
+ do s <- get ;
+ if even s
+ then returnM tt
+ else do _ <- put (S s) ;
+ returnM tt.
\ No newline at end of file
diff --git a/example/Makefile b/example/Makefile
new file mode 100644
index 0000000000000000000000000000000000000000..025caca580ce5bd48a629311ad47b36a1befa88e
--- /dev/null
+++ b/example/Makefile
@@ -0,0 +1,28 @@
+DIGGER := ../digger
+
+_: Example.o
+
+.PRECIOUS: Example.c
+
+-include .Makefile.deps
+
+Example.json: Extraction.vo
+
+.Makefile.deps: $(wildcard *.v)
+ coqdep $^ > $@
+
+%.vo: %.v
+ coqc $<
+
+%.c: %.json
+ $(DIGGER) -m Monad -M coq_M -R returnM -B bindM \
+ -m Datatypes -r Coq_true:true -r Coq_false:false -r Coq_tt:tt \
+ -q base.h -q Monad.h -q Internals.h \
+ -m Internals -d :Internals.json \
+ -o $@ $<
+
+%.o: %.c
+ cc -Wall -Wextra -c $<
+
+clean:
+ rm -f .Makefile.deps *.vo *.aux .*.vo.aux *.glob *.o *.json Example.c
diff --git a/example/Monad.c b/example/Monad.c
new file mode 100644
index 0000000000000000000000000000000000000000..92bedeb4273b4074ff66603c762fdec8c0073d2b
--- /dev/null
+++ b/example/Monad.c
@@ -0,0 +1,37 @@
+/* This software is governed by the CeCILL license under French law and
+ * abiding by the rules of distribution of free software. You can use,
+ * modify and/ or redistribute the software under the terms of the CeCILL
+ * license as circulated by CEA, CNRS and INRIA at the following URL
+ * "http://www.cecill.info".
+
+ * As a counterpart to the access to the source code and rights to copy,
+ * modify and redistribute granted by the license, users are provided only
+ * with a limited warranty and the software's author, the holder of the
+ * economic rights, and the successive licensors have only limited
+ * liability.
+
+ * In this respect, the user's attention is drawn to the risks associated
+ * with loading, using, modifying and/or developing or reproducing the
+ * software by the user in light of its specific status of free software,
+ * that may mean that it is complicated to manipulate, and that also
+ * therefore means that it is reserved for developers and experienced
+ * professionals having in-depth computer knowledge. Users are therefore
+ * encouraged to load and test the software's suitability as regards their
+ * requirements in conditions enabling the security of their systems and/or
+ * data to be ensured and, more generally, to use and operate it in the
+ * same conditions as regards security.
+
+ * The fact that you are presently reading this means that you have had
+ * knowledge of the CeCILL license and that you accept its terms.
+ */
+
+/* This C source provides possible implementations for the monad functions */
+
+#include <assert.h>
+#include "Monad.h"
+
+unsigned int state;
+
+void emptyM() {
+ assert(0);
+}
diff --git a/example/Monad.h b/example/Monad.h
new file mode 100644
index 0000000000000000000000000000000000000000..98bbadb55327ed375a9b69a80885e28c43dde654
--- /dev/null
+++ b/example/Monad.h
@@ -0,0 +1,33 @@
+/* This software is governed by the CeCILL license under French law and
+ * abiding by the rules of distribution of free software. You can use,
+ * modify and/ or redistribute the software under the terms of the CeCILL
+ * license as circulated by CEA, CNRS and INRIA at the following URL
+ * "http://www.cecill.info".
+
+ * As a counterpart to the access to the source code and rights to copy,
+ * modify and redistribute granted by the license, users are provided only
+ * with a limited warranty and the software's author, the holder of the
+ * economic rights, and the successive licensors have only limited
+ * liability.
+
+ * In this respect, the user's attention is drawn to the risks associated
+ * with loading, using, modifying and/or developing or reproducing the
+ * software by the user in light of its specific status of free software,
+ * that may mean that it is complicated to manipulate, and that also
+ * therefore means that it is reserved for developers and experienced
+ * professionals having in-depth computer knowledge. Users are therefore
+ * encouraged to load and test the software's suitability as regards their
+ * requirements in conditions enabling the security of their systems and/or
+ * data to be ensured and, more generally, to use and operate it in the
+ * same conditions as regards security.
+
+ * The fact that you are presently reading this means that you have had
+ * knowledge of the CeCILL license and that you accept its terms.
+ */
+
+/* This C header provides the prototypes for the monad functions that
+ * are needed in Internals or applications */
+
+extern unsigned int state;
+
+void emptyM();
diff --git a/example/Monad.v b/example/Monad.v
new file mode 100644
index 0000000000000000000000000000000000000000..8e4bfd5918e870c234a233be9373a37f4f852310
--- /dev/null
+++ b/example/Monad.v
@@ -0,0 +1,52 @@
+(* This software is governed by the CeCILL license under French law and
+ * abiding by the rules of distribution of free software. You can use,
+ * modify and/ or redistribute the software under the terms of the CeCILL
+ * license as circulated by CEA, CNRS and INRIA at the following URL
+ * "http://www.cecill.info".
+
+ * As a counterpart to the access to the source code and rights to copy,
+ * modify and redistribute granted by the license, users are provided only
+ * with a limited warranty and the software's author, the holder of the
+ * economic rights, and the successive licensors have only limited
+ * liability.
+
+ * In this respect, the user's attention is drawn to the risks associated
+ * with loading, using, modifying and/or developing or reproducing the
+ * software by the user in light of its specific status of free software,
+ * that may mean that it is complicated to manipulate, and that also
+ * therefore means that it is reserved for developers and experienced
+ * professionals having in-depth computer knowledge. Users are therefore
+ * encouraged to load and test the software's suitability as regards their
+ * requirements in conditions enabling the security of their systems and/or
+ * data to be ensured and, more generally, to use and operate it in the
+ * same conditions as regards security.
+
+ * The fact that you are presently reading this means that you have had
+ * knowledge of the CeCILL license and that you accept its terms.
+ *)
+
+(* This Coq module defines a simple state monad with failure, as an
+ example of use of digger to extract some monadic code into C code *)
+
+(* A simple notion of state *)
+Definition state := nat.
+
+Definition M (A: Type) := state -> option (A * state).
+
+Definition runM {A: Type} (x: M A) (s: state) := x s.
+Definition returnM {A: Type} (a: A) : M A := fun s => Some (a, s).
+Definition emptyM {A: Type} : M A := fun s => None.
+Definition bindM {A B: Type} (x: M A) (f: A -> M B) : M B :=
+ fun s =>
+ match runM x s with
+ | None => None
+ | Some (x', s') => runM (f x') s'
+ end.
+
+Definition get : M state := fun s => Some (s, s).
+Definition put (s: state) : M unit := fun s' => Some (tt, s).
+
+Notation "'do' x <- a ; b" :=
+ (bindM a (fun x => b))
+ (at level 200, x ident, a at level 100, b at level 200)
+ : monad_scope.
\ No newline at end of file
diff --git a/example/base.h b/example/base.h
new file mode 100644
index 0000000000000000000000000000000000000000..d8cec3f5ecee1a585478134f8fc1b14f4f3636f2
--- /dev/null
+++ b/example/base.h
@@ -0,0 +1,33 @@
+/* This software is governed by the CeCILL license under French law and
+ * abiding by the rules of distribution of free software. You can use,
+ * modify and/ or redistribute the software under the terms of the CeCILL
+ * license as circulated by CEA, CNRS and INRIA at the following URL
+ * "http://www.cecill.info".
+
+ * As a counterpart to the access to the source code and rights to copy,
+ * modify and redistribute granted by the license, users are provided only
+ * with a limited warranty and the software's author, the holder of the
+ * economic rights, and the successive licensors have only limited
+ * liability.
+
+ * In this respect, the user's attention is drawn to the risks associated
+ * with loading, using, modifying and/or developing or reproducing the
+ * software by the user in light of its specific status of free software,
+ * that may mean that it is complicated to manipulate, and that also
+ * therefore means that it is reserved for developers and experienced
+ * professionals having in-depth computer knowledge. Users are therefore
+ * encouraged to load and test the software's suitability as regards their
+ * requirements in conditions enabling the security of their systems and/or
+ * data to be ensured and, more generally, to use and operate it in the
+ * same conditions as regards security.
+
+ * The fact that you are presently reading this means that you have had
+ * knowledge of the CeCILL license and that you accept its terms.
+ */
+
+/* This C header provides the basic typedefs and #define */
+
+typedef int bool;
+
+#define true (1)
+#define false (0)