Extraction: no more ascii blob in type variables (fix #3227)

 Since type variables are local to the definition, we simply rename
 them in case of unicode chars. We also get rid of any ' to avoid
 Ocaml illegal 'a' type var (clash with char litteral).

4 files changed, 24 insertions, 12 deletions

diff --git a/lib/unicode.ml b/lib/unicode.ml
index 0764531c1a..1765e93dcd 100644
--- a/lib/unicode.ml
+++ b/lib/unicode.ml
@@ -222,13 +222,13 @@ let lowercase_first_char s =
 
 (** For extraction, we need to encode unicode character into ascii ones *)
 
+let is_basic_ascii s =
+  let ok = ref true in
+  String.iter (fun c -> if Char.code c >= 128 then ok := false) s;
+  !ok
+
 let ascii_of_ident s =
-  let check_ascii s =
-    let ok = ref true in
-    String.iter (fun c -> if Char.code c >= 128 then ok := false) s;
-    !ok
-  in
-  if check_ascii s then s else
+  if is_basic_ascii s then s else
     let i = ref 0 and out = ref "" in
     begin try while true do
       let j, n = next_utf8 s !i in
diff --git a/lib/unicode.mli b/lib/unicode.mli
index 763123306f..2c6b0a7963 100644
--- a/lib/unicode.mli
+++ b/lib/unicode.mli
@@ -24,4 +24,5 @@ val ident_refutation : string -> (bool * string) option
 val lowercase_first_char : string -> string
 
 (** For extraction, turn a unicode string into an ascii-only one *)
+val is_basic_ascii : string -> bool
 val ascii_of_ident : string -> string
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index a0e61c3b3f..a1a2c9db25 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -118,12 +118,27 @@ let _ = Hook.set type_scheme_nb_args_hook type_scheme_nb_args
 
 (*s [type_sign_vl] does the same, plus a type var list. *)
 
+(* When generating type variables, we avoid any ' in their names
+   (otherwise this may cause a lexer conflict in ocaml with 'a').
+   We also get rid of unicode characters. Anyway, since type variables
+   are local, the created name is just a matter of taste...
+   See also Bug #3227 *)
+
+let make_typvar n vl =
+  let id = id_of_name n in
+  let id' =
+    let s = Id.to_string id in
+    if not (String.contains s '\'') && Unicode.is_basic_ascii s then id
+    else id_of_name Anonymous
+  in
+  next_ident_away id' vl
+
 let rec type_sign_vl env c =
   match kind_of_term (whd_betadeltaiota env none c) with
     | Prod (n,t,d) ->
 	let s,vl = type_sign_vl (push_rel_assum (n,t) env) d in
 	if not (is_info_scheme env t) then Kill Kother::s, vl
-	else Keep::s, (next_ident_away (id_of_name n) vl) :: vl
+	else Keep::s, (make_typvar n vl) :: vl
     | _ -> [],[]
 
 let rec nb_default_params env c =
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index d762358970..ef81d03228 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -23,11 +23,7 @@ open Common
 
 (*s Some utility functions. *)
 
-let pp_tvar id =
-  let s = Id.to_string id in
-  if String.length s < 2 || s.[1] != '\''
-  then str ("'"^s)
-  else str ("' "^s)
+let pp_tvar id = str ("'" ^ Id.to_string id)
 
 let pp_abst = function
   | [] -> mt ()