diff options
| -rw-r--r-- | src/ExtractToFStar.ml | 8 | ||||
| -rw-r--r-- | src/Names.ml | 7 |
2 files changed, 12 insertions, 3 deletions
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index c5d078f9..b5190a45 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -224,11 +224,13 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) (* Prepare a name. * The first id elem is always the crate: if it is the local crate, * we remove it. - * We also remove all the disambiguators which are 0, then convert - * everything to strings. + * We also remove all the disambiguators, then convert everything to strings. + * **Rmk:** because we remove the disambiguators, there may be name collisions + * (which is ok, because we check for name collisions and fail if there is any). *) let get_name (name : name) : string list = - let name = Names.filter_disambiguators_zero name in + (* Rmk.: initially we only filtered the disambiguators equal to 0 *) + let name = Names.filter_disambiguators name in match name with | Ident crate :: name -> let name = if crate = crate_name then name else Ident crate :: name in diff --git a/src/Names.ml b/src/Names.ml index 5785d06f..a57f9aa1 100644 --- a/src/Names.ml +++ b/src/Names.ml @@ -61,6 +61,13 @@ let filter_disambiguators_zero (n : name) : name = in List.filter pred n +(** Filter the disambiguators in a name *) +let filter_disambiguators (n : name) : name = + let pred (pe : path_elem) : bool = + match pe with Ident _ -> true | Disambiguator _ -> false + in + List.filter pred n + let as_ident (pe : path_elem) : string = match pe with | Ident s -> s |