diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-10-04 15:37:36 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-10-05 08:38:45 +0200 |
commit | 40260a31cd197f655e6d3e0570a88d96fc1a9cac (patch) | |
tree | 0d0618bda35573e674b55a86364a5e39bf054442 | |
parent | 526791d917f9b0804376eae02a462a3b32dd7cba (diff) |
Fixing BZ#5769 (variable of type "_something" was named after invalid "_").
-rw-r--r-- | engine/namegen.ml | 14 | ||||
-rw-r--r-- | lib/unicode.ml | 28 | ||||
-rw-r--r-- | lib/unicode.mli | 4 | ||||
-rw-r--r-- | test-suite/bugs/closed/5769.v | 20 |
4 files changed, 65 insertions, 1 deletions
diff --git a/engine/namegen.ml b/engine/namegen.ml index a75fe721f..6c6a54127 100644 --- a/engine/namegen.ml +++ b/engine/namegen.ml @@ -43,6 +43,8 @@ let default_non_dependent_ident = Id.of_string default_non_dependent_string let default_dependent_ident = Id.of_string "x" +let default_generated_non_letter_string = "x" + (**********************************************************************) (* Globality of identifiers *) @@ -107,7 +109,17 @@ let head_name sigma c = (* Find the head constant of a constr if any *) hdrec c let lowercase_first_char id = (* First character of a constr *) - Unicode.lowercase_first_char (Id.to_string id) + let s = Id.to_string id in + match Unicode.split_at_first_letter s with + | None -> + (* General case: nat -> n *) + Unicode.lowercase_first_char s + | Some (s,s') -> + if String.length s' = 0 then + (* No letter, e.g. __, or __'_, etc. *) + default_generated_non_letter_string + else + s ^ Unicode.lowercase_first_char s' let sort_hdchar = function | Prop(_) -> "P" diff --git a/lib/unicode.ml b/lib/unicode.ml index 528d6434c..7f3743900 100644 --- a/lib/unicode.ml +++ b/lib/unicode.ml @@ -194,6 +194,14 @@ let is_unknown = function | Unknown -> true | Letter | IdentSep | IdentPart | Symbol -> false +let is_ident_part = function + | IdentPart -> true + | Letter | IdentSep | Symbol | Unknown -> false + +let is_ident_sep = function + | IdentSep -> true + | Letter | IdentPart | Symbol | Unknown -> false + let ident_refutation s = if s = ".." then None else try let j, n = next_utf8 s 0 in @@ -227,6 +235,26 @@ let lowercase_first_char s = let j, n = next_utf8 s 0 in utf8_of_unicode (lowercase_unicode n) +let split_at_first_letter s = + let n, v = next_utf8 s 0 in + if ((* optim *) n = 1 && s.[0] != '_') || not (is_ident_sep (classify v)) then None + else begin + let n = ref n in + let p = ref 0 in + while !n < String.length s && + let n', v = next_utf8 s !n in + p := n'; + (* Test if not letter *) + ((* optim *) n' = 1 && (s.[!n] = '_' || s.[!n] = '\'')) + || let st = classify v in + is_ident_sep st || is_ident_part st + do n := !n + !p + done; + let s1 = String.sub s 0 !n in + let s2 = String.sub s !n (String.length s - !n) in + Some (s1,s2) + end + (** For extraction, we need to encode unicode character into ascii ones *) let is_basic_ascii s = diff --git a/lib/unicode.mli b/lib/unicode.mli index a608d5f02..49b844493 100644 --- a/lib/unicode.mli +++ b/lib/unicode.mli @@ -30,6 +30,10 @@ val is_unknown : status -> bool @raise Assert_failure if the input string is empty. *) val lowercase_first_char : string -> string +(** Split a string supposed to be an ident at the first letter; + as an optimization, return None if the first character is a letter *) +val split_at_first_letter : string -> (string * string) option + (** Return [true] if all UTF-8 characters in the input string are just plain ASCII characters. Returns [false] otherwise. *) val is_basic_ascii : string -> bool diff --git a/test-suite/bugs/closed/5769.v b/test-suite/bugs/closed/5769.v new file mode 100644 index 000000000..42573aad8 --- /dev/null +++ b/test-suite/bugs/closed/5769.v @@ -0,0 +1,20 @@ +(* Check a few naming heuristics based on types *) +(* was buggy for types names _something *) + +Inductive _foo :=. +Lemma bob : (sigT (fun x : nat => _foo)) -> _foo. +destruct 1. +exact _f. +Abort. + +Inductive _'Foo :=. +Lemma bob : (sigT (fun x : nat => _'Foo)) -> _'Foo. +destruct 1. +exact _'f. +Abort. + +Inductive ____ :=. +Lemma bob : (sigT (fun x : nat => ____)) -> ____. +destruct 1. +exact x0. +Abort. |