diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/12-misc/10486-native-string-extraction.rst | 7 | ||||
| -rw-r--r-- | doc/sphinx/addendum/extraction.rst | 13 | ||||
| -rw-r--r-- | doc/stdlib/hidden-files | 2 |
3 files changed, 19 insertions, 3 deletions
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 + <https://github.com/coq/coq/pull/10486>`_, by Xavier Leroy, with help from + Maxime Dénès, review by Hugo Herbelin). 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 diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files index b816ef6210..dbc3a42ee9 100644 --- a/doc/stdlib/hidden-files +++ b/doc/stdlib/hidden-files @@ -12,12 +12,14 @@ 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 plugins/extraction/ExtrOcamlNatBigInt.v plugins/extraction/ExtrOcamlNatInt.v plugins/extraction/ExtrOcamlString.v +plugins/extraction/ExtrOcamlNativeString.v plugins/extraction/ExtrOcamlZBigInt.v plugins/extraction/ExtrOcamlZInt.v plugins/extraction/Extraction.v |