From e3640bdbbac76807457d50ac60e93192d137f3f9 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 11 Jul 2019 09:54:45 +0200 Subject: Hide ExtrOcamlStringPlus.v like the other extraction files --- doc/stdlib/hidden-files | 1 + 1 file changed, 1 insertion(+) (limited to 'doc') diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files index b816ef6210..97ff84dd8e 100644 --- a/doc/stdlib/hidden-files +++ b/doc/stdlib/hidden-files @@ -18,6 +18,7 @@ plugins/extraction/ExtrOcamlIntConv.v plugins/extraction/ExtrOcamlNatBigInt.v plugins/extraction/ExtrOcamlNatInt.v plugins/extraction/ExtrOcamlString.v +plugins/extraction/ExtrOcamlStringPlus.v plugins/extraction/ExtrOcamlZBigInt.v plugins/extraction/ExtrOcamlZInt.v plugins/extraction/Extraction.v -- cgit v1.2.3 From 887128c20edcc7d9a0e6d7387291fe0ba05a29e5 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Sun, 8 Dec 2019 19:01:04 +0100 Subject: Rename ExtrOcamlStringPlus into ExtrOcamlNativeString As suggested during review. That's a much better name. --- doc/stdlib/hidden-files | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc') diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files index 97ff84dd8e..3e53c05439 100644 --- a/doc/stdlib/hidden-files +++ b/doc/stdlib/hidden-files @@ -18,7 +18,7 @@ plugins/extraction/ExtrOcamlIntConv.v plugins/extraction/ExtrOcamlNatBigInt.v plugins/extraction/ExtrOcamlNatInt.v plugins/extraction/ExtrOcamlString.v -plugins/extraction/ExtrOcamlStringPlus.v +plugins/extraction/ExtrOcamlNativeString.v plugins/extraction/ExtrOcamlZBigInt.v plugins/extraction/ExtrOcamlZInt.v plugins/extraction/Extraction.v -- cgit v1.2.3 From ad3ece31bbb13b940d1a48f8fd694295f290fea3 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 8 Jan 2020 11:11:02 +0100 Subject: Add documentation for extraction of ascii and string literals --- doc/sphinx/addendum/extraction.rst | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) (limited to 'doc') diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst index 7136cc28d1..d909f98956 100644 --- a/doc/sphinx/addendum/extraction.rst +++ b/doc/sphinx/addendum/extraction.rst @@ -313,14 +313,21 @@ The system also provides a mechanism to specify ML terms for inductive types and constructors. For instance, the user may want to use the ML native boolean type instead of the |Coq| one. The syntax is the following: -.. cmd:: Extract Inductive @qualid => @string [ {+ @string } ] +.. cmd:: Extract Inductive @qualid => @string__1 [ {+ @string } ] Give an ML extraction for the given inductive type. You must specify - extractions for the type itself (first :token:`string`) and all its - constructors (all the :token:`string` between square brackets). In this form, + extractions for the type itself (:n:`@string__1`) and all its + constructors (all the :n:`@string` between square brackets). In this form, the ML extraction must be an ML inductive datatype, and the native pattern matching of the language will be used. + When :n:`@string__1` matches the name of the type of characters or strings + (``char`` and ``string`` for OCaml, ``Prelude.Char`` and ``Prelude.String`` + for Haskell), extraction of literals is handled in a specialized way, so as + to generate literals in the target language. This feature requires the type + designated by :n:`@qualid` to be registered as the standard char or string type, + using the :cmd:`Register` command. + .. cmdv:: Extract Inductive @qualid => @string [ {+ @string } ] @string Same as before, with a final extra :token:`string` that indicates how to -- cgit v1.2.3 From ef938a4ce2c03b1c4f23222a4542ad144a1f209b Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 8 Jan 2020 13:52:25 +0100 Subject: Factorize ascii extraction in ExtrOcamlChar.v --- doc/stdlib/hidden-files | 1 + 1 file changed, 1 insertion(+) (limited to 'doc') diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files index 3e53c05439..dbc3a42ee9 100644 --- a/doc/stdlib/hidden-files +++ b/doc/stdlib/hidden-files @@ -12,6 +12,7 @@ plugins/extraction/ExtrHaskellZInteger.v plugins/extraction/ExtrHaskellZNum.v plugins/extraction/ExtrOcamlBasic.v plugins/extraction/ExtrOcamlBigIntConv.v +plugins/extraction/ExtrOcamlChar.v plugins/extraction/ExtrOCamlInt63.v plugins/extraction/ExtrOCamlFloats.v plugins/extraction/ExtrOcamlIntConv.v -- cgit v1.2.3 From fcc3d7c64cc3d6f8f60e0e0f9469a78009b7fbd2 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 8 Jan 2020 15:06:38 +0100 Subject: Add changelog entry for native string extraction --- doc/changelog/12-misc/10486-native-string-extraction.rst | 7 +++++++ 1 file changed, 7 insertions(+) create mode 100644 doc/changelog/12-misc/10486-native-string-extraction.rst (limited to 'doc') diff --git a/doc/changelog/12-misc/10486-native-string-extraction.rst b/doc/changelog/12-misc/10486-native-string-extraction.rst new file mode 100644 index 0000000000..c6778403d4 --- /dev/null +++ b/doc/changelog/12-misc/10486-native-string-extraction.rst @@ -0,0 +1,7 @@ +- **Added:** + Support for better extraction of strings in OCaml and Haskell: + `ExtOcamlNativeString` provides bindings from the Coq `String` type to + the OCaml `string` type, and string literals can be extracted to literals, + both in OCaml and Haskell. (`#10486 + `_, by Xavier Leroy, with help from + Maxime Dénès, review by Hugo Herbelin). -- cgit v1.2.3