From c9c58c695fe39ba94f07872b60fc87eb7bbe2b8f Mon Sep 17 00:00:00 2001
From: Claude Marche <Claude.Marche@inria.fr>
Date: Fri, 13 Sep 2024 11:05:21 +0200
Subject: [PATCH] Augment documentation of extraction to C

---
 doc/exec.rst                    | 69 +++++++++++++++++++++++++++++++++++++++++
 examples/tests/c_extraction.mlw | 19 ++++++++++++
 src/extract/c.ml                |  4 +--
 3 files changed, 90 insertions(+), 2 deletions(-)
 create mode 100644 examples/tests/c_extraction.mlw

diff --git a/doc/exec.rst b/doc/exec.rst
index 34b8259b1..140897257 100644
--- a/doc/exec.rst
+++ b/doc/exec.rst
@@ -381,3 +381,72 @@ This gives the following C code.
      }
      return idx;
    }
+
+Not any WhyML code can be extracted to C. Here is a list of supported features and a few rules that your code must follow for extraction to succeed.
+
+* Basic datatypes
+
+   * Integer types declared in ``mach.int`` library are supported for
+     sizes 16, 32 and 64 bits.
+
+   * The mathematical integer type ``int`` is not supported.
+
+   * The Boolean type and bitwise operators from ``bool.Bool`` are
+     supported
+
+   * Character and strings are partially supported via the functions
+     declared in ``mach.c.String`` library
+
+   * Floating-point types are not yet supported
+
+* Compound datatypes
+
+   * Record types are supported and translated to C structs.
+
+     Beware that records as such are passed by value and returned by
+     value. For example the WhyML code
+
+     .. code-block:: whyml
+
+        use mach.int.Int32
+        type r = { x : int32; y : int32 }
+        let swap (a : r) : r = { x = a.y ; y = a.x }
+
+     is extracted as
+
+     .. code-block:: c
+
+        #include <stdint.h>
+
+        struct r {
+          int32_t x;
+          int32_t y;
+        };
+
+        struct r swap(struct r a) {
+          struct r r;
+          r.x = a.y;
+          r.y = a.x;
+          return r;
+        }
+
+   * WhyML arrays are not supported
+
+   * Pointer types are supported via the type ``ptr`` declared in
+     library ``mach.c.C``. See above for an example of use.
+
+   * Algebraic datatypes are not supported (even enumerations)
+
+* Pointer aliasing constraints
+
+   The type ``ptr`` from ``mach.c.C`` must be seen as a WhyML mutable
+   type, and as such is subject to the WhyML restrictions regarding
+   aliasing. In particular, two pointers passed as argument to a
+   function are implicitly not aliased.
+
+* Control flow structures
+
+   * Sequences, conditionals, ``while`` loops and ``for`` loops are supported
+   * Pattern matching is not supported
+   * Exception raising and catching is not supported
+   * ``break``, ``continue`` and ``return`` are supported
diff --git a/examples/tests/c_extraction.mlw b/examples/tests/c_extraction.mlw
new file mode 100644
index 000000000..14da28033
--- /dev/null
+++ b/examples/tests/c_extraction.mlw
@@ -0,0 +1,19 @@
+
+module R
+
+  use mach.int.Int32
+  type r = { x : int32; y : int32 }
+  let swap (a : r) : r = { x = a.y ; y = a.x }
+
+end
+
+module S
+
+  use mach.int.UInt32
+  use mach.c.String
+
+  let hello () : string = "hello"
+
+  let hello_len () : uint32 = length "hello"
+
+end
diff --git a/src/extract/c.ml b/src/extract/c.ml
index f82c4a426..6db73573a 100644
--- a/src/extract/c.ml
+++ b/src/extract/c.ml
@@ -1528,9 +1528,9 @@ module MLToC = struct
                 if header || flat
                 then [C.Dstruct sd]
                 else [C.Dstruct_decl id.id_string]
-             | Some Ddata _ -> raise (Unsupported "Ddata@.")
+             | Some Ddata _ -> raise (Unsupported "Ddata")
              | Some (Drange _) | Some (Dfloat _) ->
-                raise (Unsupported "Drange/Dfloat@.")
+                raise (Unsupported "Drange/Dfloat")
              | None -> raise (Unsupported
                                 ("type declaration without syntax or alias: "
                                  ^id.id_string))
-- 
2.11.4.GIT