From bb79e42c11a847c992acf82a48fd5bf5e0796d59 Mon Sep 17 00:00:00 2001
From: Samuel Hym <samuel.hym@univ-lille.fr>
Date: Wed, 17 Oct 2018 18:19:58 +0200
Subject: [PATCH] Add a simple example to show how to use digger
Show how to define a monad to provide support, how to write code in that
monad, how to use Coq extraction and how to call digger to convert the
code
---
example/Example.v | 51 +++++++++++++++++++++++++++++++++++++++++++
example/Extraction.v | 34 +++++++++++++++++++++++++++++
example/Internals.c | 39 +++++++++++++++++++++++++++++++++
example/Internals.h | 31 ++++++++++++++++++++++++++
example/Internals.v | 43 ++++++++++++++++++++++++++++++++++++
example/Makefile | 28 ++++++++++++++++++++++++
example/Monad.c | 37 +++++++++++++++++++++++++++++++
example/Monad.h | 33 ++++++++++++++++++++++++++++
example/Monad.v | 52 ++++++++++++++++++++++++++++++++++++++++++++
example/base.h | 33 ++++++++++++++++++++++++++++
10 files changed, 381 insertions(+)
create mode 100644 example/Example.v
create mode 100644 example/Extraction.v
create mode 100644 example/Internals.c
create mode 100644 example/Internals.h
create mode 100644 example/Internals.v
create mode 100644 example/Makefile
create mode 100644 example/Monad.c
create mode 100644 example/Monad.h
create mode 100644 example/Monad.v
create mode 100644 example/base.h
diff --git a/example/Example.v b/example/Example.v
new file mode 100644
index 0000000..1d12203
--- /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 0000000..c77e626
--- /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 0000000..41482d5
--- /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 0000000..efb7cbf
--- /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 0000000..f5653a3
--- /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 0000000..025caca
--- /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 0000000..92bedeb
--- /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 0000000..98bbadb
--- /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 0000000..8e4bfd5
--- /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 0000000..d8cec3f
--- /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)
--
GitLab