Better compatibility with pull request AbsInt#222

In particular, use the name [AST.string_of_ident] and declare it in the
same places, so that a merge would be straightforward.

Author: jeremie-koenig

common/AST.v

@@ -31,6 +31,8 @@ Definition ident := positive.
 
 Definition ident_eq := peq.
 
+Parameter string_of_ident: ident -> string.
+
 (** The intermediate languages are weakly typed, using the following types: *)
 
 Inductive typ : Type :=

common/BlockNames.v

@@ -4,9 +4,6 @@ Require Import AST.
 Require Import Maps.
 Require Import String.
 
-Axiom ident_to_string: ident -> string.
-Axiom pos_to_string: positive -> string.
-
 (** * Interface *)
 
 (** This is the interface of the memory block namespace. There should
@@ -63,6 +60,11 @@ End BlockType.
 
 (** * Implementation *)
 
+(** We get some help from the Ocaml code to convert dynamic block
+  identifiers into strings. *)
+
+Parameter string_of_pos: positive -> string.
+
 (** Block names are implemented as the disjoint union of [AST.ident]
   and dynamically allocated [positive]. *)
 
@@ -218,8 +220,8 @@ Module Block : BlockType.
 
   Definition to_string (b: t): string :=
     match b with
-    | glob_def i => append "glob:" (ident_to_string i)
-    | dyn b => append "dyn:" (pos_to_string b)
+    | glob_def i => append "glob:" (string_of_ident i)
+    | dyn b => append "dyn:" (string_of_pos b)
     end.
 
   Lemma ident_of_glob i:

extraction/extraction.v

@@ -36,12 +36,6 @@ Require Parser.
 Require Initializers.
 Require Int31.
 
-
-Extract Inlined Constant BlockNames.ident_to_string =>
-  "(fun i -> Camlcoq.coqstring_of_camlstring (Camlcoq.extern_atom i))".
-Extract Inlined Constant BlockNames.pos_to_string =>
-  "(fun p -> Camlcoq.coqstring_of_camlstring (Printf.sprintf ""%ld"" (Camlcoq.P.to_int32 p)))".
-
 (* Standard lib *)
 Require Import ExtrOcamlBasic.
 Require Import ExtrOcamlString.
@@ -68,6 +62,14 @@ Extraction NoInline Memory.Mem.valid_pointer.
 (* Errors *)
 Extraction Inline Errors.bind Errors.bind2.
 
+(* AST *)
+Extract Inlined Constant AST.string_of_ident =>
+  "(fun i -> Camlcoq.coqstring_of_camlstring (Camlcoq.extern_atom i))".
+
+(* BlockNames *)
+Extract Inlined Constant BlockNames.string_of_pos =>
+  "(fun p -> Camlcoq.coqstring_of_camlstring (Printf.sprintf ""%ld"" (Camlcoq.P.to_int32 p)))".
+
 (* Iteration *)
 
 Extract Constant Iteration.GenIter.iterate =>