Extraction: replace unicode characters in ident by ascii encodings (fix #2158,#2179)

 Any unicode character above 128 is replaced by __Uxxxx_ where xxxx is
 the hexa code for the unicode index of this character. For instance
 <alpha> is turned into __U03b1_. I know, this is ugly. Better
 solutions are welcome, but I'm afraid we can't do much better as long
 as ocaml and haskell don't accept unicode letters in idents. At
 least, this way we're pretty sure this translating won't create name
 conflit, as long as extraction users avoid __ in their names,
 something that they should already do btw (see for instance
 extraction of coinductive types in ocaml). Yes, I should add a test
 and a warning/error in case of use of __ someday.

 NB: this commit belongs proudly to the quick'n'dirty category

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13173 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 7 insertions, 1 deletions

diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 18b3642e28..bde54e1d80 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -20,6 +20,8 @@ open Mlutil
 open Modutil
 open Mod_subst
 
+let string_of_id id = ascii_of_ident (Names.string_of_id id)
+
 (*s Some pretty-print utility functions. *)
 
 let pp_par par st = if par then str "(" ++ st ++ str ")" else st
@@ -72,7 +74,11 @@ let is_upper s = match s.[0] with 'A' .. 'Z' -> true | _ -> false
 let is_lower s = match s.[0] with 'a' .. 'z' | '_' -> true | _ -> false
 
 let lowercase_id id = id_of_string (String.uncapitalize (string_of_id id))
-let uppercase_id id = id_of_string (String.capitalize (string_of_id id))
+let uppercase_id id =
+  let s = string_of_id id in
+  assert (s<>"");
+  if s.[0] = '_' then id_of_string ("Coq_"^s)
+  else id_of_string (String.capitalize s)
 
 type kind = Term | Type | Cons | Mod