Make identifier strings accessible from Coq

common/AST.v

@@ -31,6 +31,22 @@ Definition ident := positive.
 
 Definition ident_eq := peq.
 
+(** The mapping between the external representation of identifiers as
+  [string]s and their internal representation as [ident]s is axiomatized
+  as a bijection, and constructed incrementally by Camlcoq.ml *)
+
+Parameter ident_of_string: string -> ident.
+Parameter string_of_ident: ident -> string.
+
+Axiom string_of_ident_of_string:
+  forall s, string_of_ident (ident_of_string s) = s.
+Axiom ident_of_string_of_ident:
+  forall i, ident_of_string (string_of_ident i) = i.
+
+(** We can also print out positive numbers as such. *)
+
+Parameter string_of_pos: positive -> 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.
-
 (** * Interfaces *)
 
 Module Type BlockType <: EQUALITY_TYPE.
@@ -217,8 +214,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

@@ -37,10 +37,9 @@ 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)))".
+Extract Inlined Constant AST.ident_of_string => "Camlcoq.ident_of_coqstring".
+Extract Inlined Constant AST.string_of_ident => "Camlcoq.coqstring_of_ident".
+Extract Inlined Constant AST.string_of_pos => "Camlcoq.coqstring_of_pos".
 
 (* Standard lib *)
 Require Import ExtrOcamlBasic.

lib/Camlcoq.ml

@@ -324,6 +324,24 @@ let coqstring_uppercase_ascii_of_camlstring s =
     cstring (d :: accu) (pos - 1)
   in cstring [] (String.length s - 1)
 
+let coqstring_of_pos p =
+  coqstring_of_camlstring (Printf.sprintf "%ld" (P.to_int32 p))
+
+(* The two functions below are used from within Coq to query the
+  strings-to-atoms table, which we axiomatize as a total, bijective
+  mapping. In actuality, an ident_of_string query may create a new
+  atom, but this will not be observable: as far as the Coq code knows,
+  the mapping existed all along and we just "discovered" it.
+
+  To make sure the side-effects are unobservable, we avoid using
+  extern_atom, which catches Not_found and returns a made-up string;
+  instead, we take the exception and crash. *)
+
+let ident_of_coqstring s =
+  intern_string (camlstring_of_coqstring s)
+let coqstring_of_ident a =
+  coqstring_of_camlstring (Hashtbl.find string_of_atom a)
+
 (* Floats *)
 
 let coqfloat_of_camlfloat f =