Merge PR #10486: [extraction] Support extraction of Coq's string type to OCaml's string type

Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: herbelin
Ack-by: maximedenes
Reviewed-by: pi8027

7 files changed, 245 insertions, 53 deletions

diff --git a/plugins/extraction/ExtrOcamlChar.v b/plugins/extraction/ExtrOcamlChar.v
new file mode 100644
index 0000000000..1e68365dd3
--- /dev/null
+++ b/plugins/extraction/ExtrOcamlChar.v
@@ -0,0 +1,45 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* Extraction to Ocaml : extract ascii to OCaml's char type *)
+
+Require Coq.extraction.Extraction.
+
+Require Import Ascii String Coq.Strings.Byte.
+
+Extract Inductive ascii => char
+[
+"(* If this appears, you're using Ascii internals. Please don't *)
+ (fun (b0,b1,b2,b3,b4,b5,b6,b7) ->
+  let f b i = if b then 1 lsl i else 0 in
+  Char.chr (f b0 0 + f b1 1 + f b2 2 + f b3 3 + f b4 4 + f b5 5 + f b6 6 + f b7 7))"
+]
+"(* If this appears, you're using Ascii internals. Please don't *)
+ (fun f c ->
+  let n = Char.code c in
+  let h i = (n land (1 lsl i)) <> 0 in
+  f (h 0) (h 1) (h 2) (h 3) (h 4) (h 5) (h 6) (h 7))".
+
+Extract Constant zero => "'\000'".
+Extract Constant one => "'\001'".
+Extract Constant shift =>
+ "fun b c -> Char.chr (((Char.code c) lsl 1) land 255 + if b then 1 else 0)".
+
+Extract Inlined Constant ascii_dec => "(=)".
+Extract Inlined Constant Ascii.eqb => "(=)".
+
+(* python -c 'print(" ".join(r""" "%s" """.strip() % (r"'"'\''"'" if chr(i) == "'"'"'" else repr(""" "" """.strip()) if chr(i) == """ " """.strip() else repr(chr(i))) for i in range(256)))' # " to satisfy Coq's comment parser *)
+Extract Inductive byte => char
+["'\x00'" "'\x01'" "'\x02'" "'\x03'" "'\x04'" "'\x05'" "'\x06'" "'\x07'" "'\x08'" "'\t'" "'\n'" "'\x0b'" "'\x0c'" "'\r'" "'\x0e'" "'\x0f'" "'\x10'" "'\x11'" "'\x12'" "'\x13'" "'\x14'" "'\x15'" "'\x16'" "'\x17'" "'\x18'" "'\x19'" "'\x1a'" "'\x1b'" "'\x1c'" "'\x1d'" "'\x1e'" "'\x1f'" "' '" "'!'" "'""'" "'#'" "'$'" "'%'" "'&'" "'\''" "'('" "')'" "'*'" "'+'" "','" "'-'" "'.'" "'/'" "'0'" "'1'" "'2'" "'3'" "'4'" "'5'" "'6'" "'7'" "'8'" "'9'" "':'" "';'" "'<'" "'='" "'>'" "'?'" "'@'" "'A'" "'B'" "'C'" "'D'" "'E'" "'F'" "'G'" "'H'" "'I'" "'J'" "'K'" "'L'" "'M'" "'N'" "'O'" "'P'" "'Q'" "'R'" "'S'" "'T'" "'U'" "'V'" "'W'" "'X'" "'Y'" "'Z'" "'['" "'\\'" "']'" "'^'" "'_'" "'`'" "'a'" "'b'" "'c'" "'d'" "'e'" "'f'" "'g'" "'h'" "'i'" "'j'" "'k'" "'l'" "'m'" "'n'" "'o'" "'p'" "'q'" "'r'" "'s'" "'t'" "'u'" "'v'" "'w'" "'x'" "'y'" "'z'" "'{'" "'|'" "'}'" "'~'" "'\x7f'" "'\x80'" "'\x81'" "'\x82'" "'\x83'" "'\x84'" "'\x85'" "'\x86'" "'\x87'" "'\x88'" "'\x89'" "'\x8a'" "'\x8b'" "'\x8c'" "'\x8d'" "'\x8e'" "'\x8f'" "'\x90'" "'\x91'" "'\x92'" "'\x93'" "'\x94'" "'\x95'" "'\x96'" "'\x97'" "'\x98'" "'\x99'" "'\x9a'" "'\x9b'" "'\x9c'" "'\x9d'" "'\x9e'" "'\x9f'" "'\xa0'" "'\xa1'" "'\xa2'" "'\xa3'" "'\xa4'" "'\xa5'" "'\xa6'" "'\xa7'" "'\xa8'" "'\xa9'" "'\xaa'" "'\xab'" "'\xac'" "'\xad'" "'\xae'" "'\xaf'" "'\xb0'" "'\xb1'" "'\xb2'" "'\xb3'" "'\xb4'" "'\xb5'" "'\xb6'" "'\xb7'" "'\xb8'" "'\xb9'" "'\xba'" "'\xbb'" "'\xbc'" "'\xbd'" "'\xbe'" "'\xbf'" "'\xc0'" "'\xc1'" "'\xc2'" "'\xc3'" "'\xc4'" "'\xc5'" "'\xc6'" "'\xc7'" "'\xc8'" "'\xc9'" "'\xca'" "'\xcb'" "'\xcc'" "'\xcd'" "'\xce'" "'\xcf'" "'\xd0'" "'\xd1'" "'\xd2'" "'\xd3'" "'\xd4'" "'\xd5'" "'\xd6'" "'\xd7'" "'\xd8'" "'\xd9'" "'\xda'" "'\xdb'" "'\xdc'" "'\xdd'" "'\xde'" "'\xdf'" "'\xe0'" "'\xe1'" "'\xe2'" "'\xe3'" "'\xe4'" "'\xe5'" "'\xe6'" "'\xe7'" "'\xe8'" "'\xe9'" "'\xea'" "'\xeb'" "'\xec'" "'\xed'" "'\xee'" "'\xef'" "'\xf0'" "'\xf1'" "'\xf2'" "'\xf3'" "'\xf4'" "'\xf5'" "'\xf6'" "'\xf7'" "'\xf8'" "'\xf9'" "'\xfa'" "'\xfb'" "'\xfc'" "'\xfd'" "'\xfe'" "'\xff'"].
+
+Extract Inlined Constant Byte.eqb => "(=)".
+Extract Inlined Constant Byte.byte_eq_dec => "(=)".
+Extract Inlined Constant Ascii.ascii_of_byte => "(fun x -> x)".
+Extract Inlined Constant Ascii.byte_of_ascii => "(fun x -> x)".
diff --git a/plugins/extraction/ExtrOcamlNativeString.v b/plugins/extraction/ExtrOcamlNativeString.v
new file mode 100644
index 0000000000..ec3da1e444
--- /dev/null
+++ b/plugins/extraction/ExtrOcamlNativeString.v
@@ -0,0 +1,87 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(* Extraction to Ocaml : extract ascii to OCaml's char type
+   and string to OCaml's string type. *)
+
+Require Coq.extraction.Extraction.
+
+Require Import Ascii String Coq.Strings.Byte.
+Require Export ExtrOcamlChar.
+
+(* python -c 'print(" ".join(r""" "%s" """.strip() % (r"'"'\''"'" if chr(i) == "'"'"'" else repr(""" "" """.strip()) if chr(i) == """ " """.strip() else repr(chr(i))) for i in range(256)))' # " to satisfy Coq's comment parser *)
+Extract Inductive byte => char
+["'\x00'" "'\x01'" "'\x02'" "'\x03'" "'\x04'" "'\x05'" "'\x06'" "'\x07'" "'\x08'" "'\t'" "'\n'" "'\x0b'" "'\x0c'" "'\r'" "'\x0e'" "'\x0f'" "'\x10'" "'\x11'" "'\x12'" "'\x13'" "'\x14'" "'\x15'" "'\x16'" "'\x17'" "'\x18'" "'\x19'" "'\x1a'" "'\x1b'" "'\x1c'" "'\x1d'" "'\x1e'" "'\x1f'" "' '" "'!'" "'""'" "'#'" "'$'" "'%'" "'&'" "'\''" "'('" "')'" "'*'" "'+'" "','" "'-'" "'.'" "'/'" "'0'" "'1'" "'2'" "'3'" "'4'" "'5'" "'6'" "'7'" "'8'" "'9'" "':'" "';'" "'<'" "'='" "'>'" "'?'" "'@'" "'A'" "'B'" "'C'" "'D'" "'E'" "'F'" "'G'" "'H'" "'I'" "'J'" "'K'" "'L'" "'M'" "'N'" "'O'" "'P'" "'Q'" "'R'" "'S'" "'T'" "'U'" "'V'" "'W'" "'X'" "'Y'" "'Z'" "'['" "'\\'" "']'" "'^'" "'_'" "'`'" "'a'" "'b'" "'c'" "'d'" "'e'" "'f'" "'g'" "'h'" "'i'" "'j'" "'k'" "'l'" "'m'" "'n'" "'o'" "'p'" "'q'" "'r'" "'s'" "'t'" "'u'" "'v'" "'w'" "'x'" "'y'" "'z'" "'{'" "'|'" "'}'" "'~'" "'\x7f'" "'\x80'" "'\x81'" "'\x82'" "'\x83'" "'\x84'" "'\x85'" "'\x86'" "'\x87'" "'\x88'" "'\x89'" "'\x8a'" "'\x8b'" "'\x8c'" "'\x8d'" "'\x8e'" "'\x8f'" "'\x90'" "'\x91'" "'\x92'" "'\x93'" "'\x94'" "'\x95'" "'\x96'" "'\x97'" "'\x98'" "'\x99'" "'\x9a'" "'\x9b'" "'\x9c'" "'\x9d'" "'\x9e'" "'\x9f'" "'\xa0'" "'\xa1'" "'\xa2'" "'\xa3'" "'\xa4'" "'\xa5'" "'\xa6'" "'\xa7'" "'\xa8'" "'\xa9'" "'\xaa'" "'\xab'" "'\xac'" "'\xad'" "'\xae'" "'\xaf'" "'\xb0'" "'\xb1'" "'\xb2'" "'\xb3'" "'\xb4'" "'\xb5'" "'\xb6'" "'\xb7'" "'\xb8'" "'\xb9'" "'\xba'" "'\xbb'" "'\xbc'" "'\xbd'" "'\xbe'" "'\xbf'" "'\xc0'" "'\xc1'" "'\xc2'" "'\xc3'" "'\xc4'" "'\xc5'" "'\xc6'" "'\xc7'" "'\xc8'" "'\xc9'" "'\xca'" "'\xcb'" "'\xcc'" "'\xcd'" "'\xce'" "'\xcf'" "'\xd0'" "'\xd1'" "'\xd2'" "'\xd3'" "'\xd4'" "'\xd5'" "'\xd6'" "'\xd7'" "'\xd8'" "'\xd9'" "'\xda'" "'\xdb'" "'\xdc'" "'\xdd'" "'\xde'" "'\xdf'" "'\xe0'" "'\xe1'" "'\xe2'" "'\xe3'" "'\xe4'" "'\xe5'" "'\xe6'" "'\xe7'" "'\xe8'" "'\xe9'" "'\xea'" "'\xeb'" "'\xec'" "'\xed'" "'\xee'" "'\xef'" "'\xf0'" "'\xf1'" "'\xf2'" "'\xf3'" "'\xf4'" "'\xf5'" "'\xf6'" "'\xf7'" "'\xf8'" "'\xf9'" "'\xfa'" "'\xfb'" "'\xfc'" "'\xfd'" "'\xfe'" "'\xff'"].
+
+Extract Inlined Constant Byte.eqb => "(=)".
+Extract Inlined Constant Byte.byte_eq_dec => "(=)".
+Extract Inlined Constant Ascii.ascii_of_byte => "(fun x -> x)".
+Extract Inlined Constant Ascii.byte_of_ascii => "(fun x -> x)".
+
+(* This differs from ExtrOcamlString.v: the latter extracts "string"
+   to "char list", and we extract "string" to "string" *)
+
+Extract Inductive string => "string"
+[
+(* EmptyString *)
+"(* If this appears, you're using String internals. Please don't *)
+  """"
+"
+(* String *)
+"(* If this appears, you're using String internals. Please don't *)
+  (fun (c, s) -> String.make 1 c ^ s)
+"
+]
+"(* If this appears, you're using String internals. Please don't *)
+ (fun f0 f1 s ->
+    let l = String.length s in
+    if l = 0 then f0 else f1 (String.get s 0) (String.sub s 1 (l-1)))
+".
+
+Extract Inlined Constant String.string_dec => "(=)".
+Extract Inlined Constant String.eqb => "(=)".
+Extract Inlined Constant String.append => "(^)".
+Extract Inlined Constant String.concat => "String.concat".
+Extract Inlined Constant String.prefix =>
+  "(fun s1 s2 ->
+     let l1 = String.length s1 and l2 = String.length s2 in
+     l1 <= l2 && String.sub s2 0 l1 = s1)".
+Extract Inlined Constant String.string_of_list_ascii =>
+  "(fun l ->
+      let a = Array.of_list l in
+      String.init (Array.length a) (fun i -> a.(i)))".
+Extract Inlined Constant String.list_ascii_of_string =>
+  "(fun s ->
+      Array.to_list (Array.init (String.length s) (fun i -> s.[i])))".
+Extract Inlined Constant String.string_of_list_byte =>
+  "(fun l ->
+      let a = Array.of_list l in
+      String.init (Array.length a) (fun i -> a.(i)))".
+Extract Inlined Constant String.list_byte_of_string =>
+  "(fun s ->
+      Array.to_list (Array.init (String.length s) (fun i -> s.[i])))".
+
+(* Other operations in module String (at the time of this writing):
+      String.length
+      String.get
+      String.substring
+      String.index
+      String.findex
+   They all use type "nat".  If we know that "nat" extracts
+   to O | S of nat, we can provide OCaml implementations
+   for these functions that work directly on OCaml's strings.
+   However "nat" could be extracted to other OCaml types...
+*)
+
+(*
+Definition test := "ceci est un test"%string.
+
+Recursive Extraction test Ascii.zero Ascii.one.
+*)
diff --git a/plugins/extraction/ExtrOcamlString.v b/plugins/extraction/ExtrOcamlString.v
index 6265a67577..18c5ed3fe4 100644
--- a/plugins/extraction/ExtrOcamlString.v
+++ b/plugins/extraction/ExtrOcamlString.v
@@ -13,43 +13,6 @@
 Require Coq.extraction.Extraction.
 
 Require Import Ascii String Coq.Strings.Byte.
-
-Extract Inductive ascii => char
-[
-"(* If this appears, you're using Ascii internals. Please don't *)
- (fun (b0,b1,b2,b3,b4,b5,b6,b7) ->
-  let f b i = if b then 1 lsl i else 0 in
-  Char.chr (f b0 0 + f b1 1 + f b2 2 + f b3 3 + f b4 4 + f b5 5 + f b6 6 + f b7 7))"
-]
-"(* If this appears, you're using Ascii internals. Please don't *)
- (fun f c ->
-  let n = Char.code c in
-  let h i = (n land (1 lsl i)) <> 0 in
-  f (h 0) (h 1) (h 2) (h 3) (h 4) (h 5) (h 6) (h 7))".
-
-Extract Constant zero => "'\000'".
-Extract Constant one => "'\001'".
-Extract Constant shift =>
- "fun b c -> Char.chr (((Char.code c) lsl 1) land 255 + if b then 1 else 0)".
-
-Extract Inlined Constant ascii_dec => "(=)".
-Extract Inlined Constant Ascii.eqb => "(=)".
+Require Export ExtrOcamlChar.
 
 Extract Inductive string => "char list" [ "[]" "(::)" ].
-
-(* python -c 'print(" ".join(r""" "%s" """.strip() % (r"'"'\''"'" if chr(i) == "'"'"'" else repr(""" "" """.strip()) if chr(i) == """ " """.strip() else repr(chr(i))) for i in range(256)))' # " to satisfy Coq's comment parser *)
-Extract Inductive byte => char
-["'\x00'" "'\x01'" "'\x02'" "'\x03'" "'\x04'" "'\x05'" "'\x06'" "'\x07'" "'\x08'" "'\t'" "'\n'" "'\x0b'" "'\x0c'" "'\r'" "'\x0e'" "'\x0f'" "'\x10'" "'\x11'" "'\x12'" "'\x13'" "'\x14'" "'\x15'" "'\x16'" "'\x17'" "'\x18'" "'\x19'" "'\x1a'" "'\x1b'" "'\x1c'" "'\x1d'" "'\x1e'" "'\x1f'" "' '" "'!'" "'""'" "'#'" "'$'" "'%'" "'&'" "'\''" "'('" "')'" "'*'" "'+'" "','" "'-'" "'.'" "'/'" "'0'" "'1'" "'2'" "'3'" "'4'" "'5'" "'6'" "'7'" "'8'" "'9'" "':'" "';'" "'<'" "'='" "'>'" "'?'" "'@'" "'A'" "'B'" "'C'" "'D'" "'E'" "'F'" "'G'" "'H'" "'I'" "'J'" "'K'" "'L'" "'M'" "'N'" "'O'" "'P'" "'Q'" "'R'" "'S'" "'T'" "'U'" "'V'" "'W'" "'X'" "'Y'" "'Z'" "'['" "'\\'" "']'" "'^'" "'_'" "'`'" "'a'" "'b'" "'c'" "'d'" "'e'" "'f'" "'g'" "'h'" "'i'" "'j'" "'k'" "'l'" "'m'" "'n'" "'o'" "'p'" "'q'" "'r'" "'s'" "'t'" "'u'" "'v'" "'w'" "'x'" "'y'" "'z'" "'{'" "'|'" "'}'" "'~'" "'\x7f'" "'\x80'" "'\x81'" "'\x82'" "'\x83'" "'\x84'" "'\x85'" "'\x86'" "'\x87'" "'\x88'" "'\x89'" "'\x8a'" "'\x8b'" "'\x8c'" "'\x8d'" "'\x8e'" "'\x8f'" "'\x90'" "'\x91'" "'\x92'" "'\x93'" "'\x94'" "'\x95'" "'\x96'" "'\x97'" "'\x98'" "'\x99'" "'\x9a'" "'\x9b'" "'\x9c'" "'\x9d'" "'\x9e'" "'\x9f'" "'\xa0'" "'\xa1'" "'\xa2'" "'\xa3'" "'\xa4'" "'\xa5'" "'\xa6'" "'\xa7'" "'\xa8'" "'\xa9'" "'\xaa'" "'\xab'" "'\xac'" "'\xad'" "'\xae'" "'\xaf'" "'\xb0'" "'\xb1'" "'\xb2'" "'\xb3'" "'\xb4'" "'\xb5'" "'\xb6'" "'\xb7'" "'\xb8'" "'\xb9'" "'\xba'" "'\xbb'" "'\xbc'" "'\xbd'" "'\xbe'" "'\xbf'" "'\xc0'" "'\xc1'" "'\xc2'" "'\xc3'" "'\xc4'" "'\xc5'" "'\xc6'" "'\xc7'" "'\xc8'" "'\xc9'" "'\xca'" "'\xcb'" "'\xcc'" "'\xcd'" "'\xce'" "'\xcf'" "'\xd0'" "'\xd1'" "'\xd2'" "'\xd3'" "'\xd4'" "'\xd5'" "'\xd6'" "'\xd7'" "'\xd8'" "'\xd9'" "'\xda'" "'\xdb'" "'\xdc'" "'\xdd'" "'\xde'" "'\xdf'" "'\xe0'" "'\xe1'" "'\xe2'" "'\xe3'" "'\xe4'" "'\xe5'" "'\xe6'" "'\xe7'" "'\xe8'" "'\xe9'" "'\xea'" "'\xeb'" "'\xec'" "'\xed'" "'\xee'" "'\xef'" "'\xf0'" "'\xf1'" "'\xf2'" "'\xf3'" "'\xf4'" "'\xf5'" "'\xf6'" "'\xf7'" "'\xf8'" "'\xf9'" "'\xfa'" "'\xfb'" "'\xfc'" "'\xfd'" "'\xfe'" "'\xff'"].
-
-Extract Inlined Constant Byte.eqb => "(=)".
-Extract Inlined Constant Byte.byte_eq_dec => "(=)".
-Extract Inlined Constant Ascii.ascii_of_byte => "(fun x -> x)".
-Extract Inlined Constant Ascii.byte_of_ascii => "(fun x -> x)".
-
-(*
-Definition test := "ceci est un test"%string.
-Definition test2 := List.map (option_map Byte.to_nat) (List.map Byte.of_nat (List.seq 0 256)).
-Definition test3 := List.map ascii_of_nat (List.seq 0 256).
-
-Recursive Extraction test Ascii.zero Ascii.one test2 test3 byte_rect.
-*)
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 2f3f42c5f6..29da12de40 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -14,7 +14,6 @@ open Names
 open ModPath
 open Namegen
 open Nameops
-open Libnames
 open Table
 open Miniml
 open Mlutil
@@ -616,10 +615,15 @@ let pp_module mp =
     [Extract Inductive ascii => char] has been declared, then
     the constants are directly turned into chars *)
 
-let mk_ind path s =
-  MutInd.make2 (MPfile (dirpath_of_string path)) (Label.make s)
+let ascii_type_name = "core.ascii.type"
+let ascii_constructor_name = "core.ascii.ascii"
 
-let ind_ascii = mk_ind "Coq.Strings.Ascii" "ascii"
+let is_ascii_registered () =
+  Coqlib.has_ref ascii_type_name
+  && Coqlib.has_ref ascii_constructor_name
+
+let ascii_type_ref () = Coqlib.lib_ref ascii_type_name
+let ascii_constructor_ref () = Coqlib.lib_ref ascii_constructor_name
 
 let check_extract_ascii () =
   try
@@ -628,15 +632,18 @@ let check_extract_ascii () =
       | Haskell -> "Prelude.Char"
       | _ -> raise Not_found
     in
-    String.equal (find_custom (GlobRef.IndRef (ind_ascii, 0))) (char_type)
+    String.equal (find_custom @@ ascii_type_ref ()) (char_type)
   with Not_found -> false
 
 let is_list_cons l =
  List.for_all (function MLcons (_,GlobRef.ConstructRef(_,_),[]) -> true | _ -> false) l
 
 let is_native_char = function
-  | MLcons(_,GlobRef.ConstructRef ((kn,0),1),l) ->
-    MutInd.equal kn ind_ascii && check_extract_ascii () && is_list_cons l
+  | MLcons(_,gr,l) ->
+    is_ascii_registered ()
+    && GlobRef.equal gr (ascii_constructor_ref ())
+    && check_extract_ascii ()
+    && is_list_cons l
   | _ -> false
 
 let get_native_char c =
@@ -649,3 +656,84 @@ let get_native_char c =
   Char.chr (cumul l)
 
 let pp_native_char c = str ("'"^Char.escaped (get_native_char c)^"'")
+
+(** Special hack for constants of type String.string : if an
+    [Extract Inductive string => string] has been declared, then
+    the constants are directly turned into string literals *)
+
+let string_type_name = "core.string.type"
+let empty_string_name = "core.string.empty"
+let string_constructor_name = "core.string.string"
+
+let is_string_registered () =
+  Coqlib.has_ref string_type_name
+  && Coqlib.has_ref empty_string_name
+  && Coqlib.has_ref string_constructor_name
+
+let string_type_ref () = Coqlib.lib_ref string_type_name
+let empty_string_ref () = Coqlib.lib_ref empty_string_name
+let string_constructor_ref () = Coqlib.lib_ref string_constructor_name
+
+let check_extract_string () =
+  try
+    let string_type = match lang () with
+      | Ocaml -> "string"
+      | Haskell -> "Prelude.String"
+      | _ -> raise Not_found
+    in
+    String.equal (find_custom @@ string_type_ref ()) string_type
+  with Not_found -> false
+
+(* The argument is known to be of type Coq.Strings.String.string.
+   Check that it is built from constructors EmptyString and String
+   with constant ascii arguments. *)
+
+let rec is_native_string_rec empty_string_ref string_constructor_ref = function
+  (* "EmptyString" constructor *)
+  | MLcons(_, gr, []) -> GlobRef.equal gr empty_string_ref
+  (* "String" constructor *)
+  | MLcons(_, gr, [hd; tl]) ->
+      GlobRef.equal gr string_constructor_ref
+      && is_native_char hd
+      && is_native_string_rec empty_string_ref string_constructor_ref tl
+  (* others *)
+  | _ -> false
+
+(* Here we first check that the argument is the type registered as
+   core.string.type and that extraction to native strings was
+   requested.  Then we check every character via
+   [is_native_string_rec]. *)
+
+let is_native_string c =
+  match c with
+  | MLcons(_, GlobRef.ConstructRef(ind, j), l) ->
+      is_string_registered ()
+      && GlobRef.equal (GlobRef.IndRef ind) (string_type_ref ())
+      && check_extract_string ()
+      && is_native_string_rec (empty_string_ref ()) (string_constructor_ref ()) c
+  | _ -> false
+
+(* Extract the underlying string. *)
+
+let get_native_string c =
+  let buf = Buffer.create 64 in
+  let rec get = function
+    (* "EmptyString" constructor *)
+    | MLcons(_, gr, []) when GlobRef.equal gr (empty_string_ref ()) ->
+        Buffer.contents buf
+    (* "String" constructor *)
+    | MLcons(_, gr, [hd; tl]) when GlobRef.equal gr (string_constructor_ref ()) ->
+        Buffer.add_char buf (get_native_char hd);
+        get tl
+    (* others *)
+    | _ -> assert false
+  in get c
+
+(* Printing the underlying string. *)
+
+let pp_native_string c =
+  str ("\"" ^ String.escaped (get_native_string c) ^ "\"")
+
+(* Registered sig type *)
+
+let sig_type_ref () = Coqlib.lib_ref "core.sig.type"
diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli
index e4e9c4c527..9dbc09dd06 100644
--- a/plugins/extraction/common.mli
+++ b/plugins/extraction/common.mli
@@ -70,10 +70,6 @@ val reset_renaming_tables : reset_kind -> unit
 
 val set_keywords : Id.Set.t -> unit
 
-(** For instance: [mk_ind "Coq.Init.Datatypes" "nat"] *)
-
-val mk_ind : string -> string -> MutInd.t
-
 (** Special hack for constants of type Ascii.ascii : if an
     [Extract Inductive ascii => char] has been declared, then
     the constants are directly turned into chars *)
@@ -81,3 +77,14 @@ val mk_ind : string -> string -> MutInd.t
 val is_native_char : ml_ast -> bool
 val get_native_char : ml_ast -> char
 val pp_native_char : ml_ast -> Pp.t
+
+(** Special hack for constants of type String.string : if an
+    [Extract Inductive string => string] has been declared, then
+    the constants are directly turned into string literals *)
+
+val is_native_string : ml_ast -> bool
+val get_native_string : ml_ast -> string
+val pp_native_string : ml_ast -> Pp.t
+
+(* Registered sig type *)
+val sig_type_ref : unit -> GlobRef.t
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index f0053ba6b5..eef050efbd 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -109,8 +109,8 @@ let rec pp_type par vl t =
       (try Id.print (List.nth vl (pred i))
        with Failure _ -> (str "a" ++ int i))
     | Tglob (r,[]) -> pp_global Type r
-    | Tglob (GlobRef.IndRef(kn,0),l)
-        when not (keep_singleton ()) && MutInd.equal kn (mk_ind "Coq.Init.Specif" "sig") ->
+    | Tglob (gr,l)
+        when not (keep_singleton ()) && GlobRef.equal gr (sig_type_ref ()) ->
           pp_type true vl (List.hd l)
     | Tglob (r,l) ->
           pp_par par
@@ -171,6 +171,7 @@ let rec pp_expr par env args =
         assert (List.is_empty args);
         begin match a with
           | _ when is_native_char c -> pp_native_char c
+          | _ when is_native_string c -> pp_native_string c
           | [] -> pp_global Cons r
           | [a] ->
             pp_par par (pp_global Cons r ++ spc () ++ pp_expr true env [] a)
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 66429833b9..97cad87825 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -165,8 +165,8 @@ let pp_type par vl t =
     | Tglob (r,[a1;a2]) when is_infix r ->
         pp_par par (pp_rec true a1 ++ str (get_infix r) ++ pp_rec true a2)
     | Tglob (r,[]) -> pp_global Type r
-    | Tglob (GlobRef.IndRef(kn,0),l)
-        when not (keep_singleton ()) && MutInd.equal kn (mk_ind "Coq.Init.Specif" "sig") ->
+    | Tglob (gr,l)
+        when not (keep_singleton ()) && GlobRef.equal gr (sig_type_ref ()) ->
         pp_tuple_light pp_rec l
     | Tglob (r,l) ->
         pp_tuple_light pp_rec l ++ spc () ++ pp_global Type r
@@ -249,6 +249,7 @@ let rec pp_expr par env args =
         assert (List.is_empty args);
         begin match a with
           | _ when is_native_char c -> pp_native_char c
+          | _ when is_native_string c -> pp_native_string c
           | [a1;a2] when is_infix r ->
             let pp = pp_expr true env [] in
             pp_par par (pp a1 ++ str (get_infix r) ++ pp a2)