Avoid hardcoded paths in extraction

6 files changed, 57 insertions, 29 deletions

diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 219afcf408..e2cde8e0d3 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 =
@@ -654,7 +661,18 @@ let pp_native_char c = str ("'"^Char.escaped (get_native_char c)^"'")
     [Extract Inductive string => string] has been declared, then
     the constants are directly turned into string literals *)
 
-let ind_string = mk_ind "Coq.Strings.String" "string"
+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
@@ -662,32 +680,35 @@ let check_extract_string () =
       | Ocaml -> "string"
       | _ -> raise Not_found
     in
-    String.equal (find_custom (GlobRef.IndRef (ind_string, 0))) string_type
+    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 = function
+let rec is_native_string_rec empty_string_ref string_constructor_ref = function
   (* "EmptyString" constructor *)
-  | MLcons(_, GlobRef.ConstructRef(_, 1), []) -> true
+  | MLcons(_, gr, []) -> GlobRef.equal gr empty_string_ref
   (* "String" constructor *)
-  | MLcons(_, GlobRef.ConstructRef(_, 2), [hd; tl]) ->
-      is_native_char hd && is_native_string_rec tl
+  | 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 of type Coq.Strings.String.string
+(* Here we first check that the argument is has a 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((kn,0), j), l) ->
-      MutInd.equal kn ind_string
+  | MLcons(_, GlobRef.ConstructRef(ind, j), l) ->
+      is_string_registered ()
+      && GlobRef.equal (GlobRef.IndRef ind) (string_type_ref ())
       && check_extract_string ()
-      && is_native_string_rec c
+      && is_native_string_rec (empty_string_ref ()) (string_constructor_ref ()) c
   | _ -> false
 
 (* Extract the underlying string. *)
@@ -696,10 +717,10 @@ let get_native_string c =
   let buf = Buffer.create 64 in
   let rec get = function
     (* "EmptyString" constructor *)
-    | MLcons(_, GlobRef.ConstructRef(_, 1), []) ->
+    | MLcons(_, gr, []) when GlobRef.equal gr (empty_string_ref ()) ->
         Buffer.contents buf
     (* "String" constructor *)
-    | MLcons(_, GlobRef.ConstructRef(_, 2), [hd; tl]) ->
+    | MLcons(_, gr, [hd; tl]) when GlobRef.equal gr (string_constructor_ref ()) ->
         Buffer.add_char buf (get_native_char hd);
         get tl
     (* others *)
@@ -710,3 +731,7 @@ let get_native_string c =
 
 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 d13ac7926a..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 *)
@@ -89,3 +85,6 @@ val pp_native_char : ml_ast -> Pp.t
 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..bde37bcae7 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
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index ab37bd2d76..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
diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v
index 79ec67b633..6a849bb0b1 100644
--- a/theories/Strings/Ascii.v
+++ b/theories/Strings/Ascii.v
@@ -24,6 +24,9 @@ Declare Scope char_scope.
 Delimit Scope char_scope with char.
 Bind Scope char_scope with ascii.
 
+Register ascii as core.ascii.type.
+Register Ascii as core.ascii.ascii.
+
 Definition zero := Ascii false false false false false false false false.
 
 Definition one := Ascii true false false false false false false false.
diff --git a/theories/Strings/String.v b/theories/Strings/String.v
index 9d0d2f854d..b736f41a08 100644
--- a/theories/Strings/String.v
+++ b/theories/Strings/String.v
@@ -30,8 +30,9 @@ Delimit Scope string_scope with string.
 Bind Scope string_scope with string.
 Local Open Scope string_scope.
 
-Register EmptyString as plugins.syntax.EmptyString.
-Register String as plugins.syntax.String.
+Register string as core.string.type.
+Register EmptyString as core.string.empty.
+Register String as core.string.string.
 
 (** Equality is decidable *)