diff options
author | Son Ho | 2023-09-03 10:04:14 +0200 |
---|---|---|
committer | Son Ho | 2023-09-03 10:04:14 +0200 |
commit | 4cf1217f593b46a17130403df85b5f39f9e3eb85 (patch) | |
tree | 83f6460c068c9f93f60969f012d35d2d1b427653 | |
parent | 0023f814ce638cd9b04ead9ec2e0c194d5efaefd (diff) |
Improve the collision detection
-rw-r--r-- | compiler/ExtractBase.ml | 70 |
1 files changed, 54 insertions, 16 deletions
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index 2c704d3e..02ff266e 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -458,21 +458,34 @@ type names_map = { *) } -let names_map_add (id_to_string : id -> string) (is_opaque : bool) (id : id) - (name : string) (nm : names_map) : names_map = - (* Check if there is a clash *) - (match StringMap.find_opt name nm.name_to_id with +(** Small helper to report name collision *) +let report_name_collision (id_to_string : id -> string) (id1 : id) (id2 : id) + (name : string) : unit = + let id1 = "\n- " ^ id_to_string id1 in + let id2 = "\n- " ^ id_to_string id2 in + let err = + "Name clash detected: the following identifiers are bound to the same name \ + \"" ^ name ^ "\":" ^ id1 ^ id2 + ^ "\nYou may want to rename some of your definitions, or report an issue." + in + log#serror err; + raise (Failure err) + +let names_map_get_id_from_name (name : string) (nm : names_map) : id option = + StringMap.find_opt name nm.name_to_id + +let names_map_check_collision (id_to_string : id -> string) (id : id) + (name : string) (nm : names_map) : unit = + match names_map_get_id_from_name name nm with | None -> () (* Ok *) | Some clash -> (* There is a clash: print a nice debugging message for the user *) - let id1 = "\n- " ^ id_to_string clash in - let id2 = "\n- " ^ id_to_string id in - let err = - "Name clash detected: the following identifiers are bound to the same \ - name \"" ^ name ^ "\":" ^ id1 ^ id2 - in - log#serror err; - raise (Failure err)); + report_name_collision id_to_string clash id name + +let names_map_add (id_to_string : id -> string) (is_opaque : bool) (id : id) + (name : string) (nm : names_map) : names_map = + (* Check if there is a clash *) + names_map_check_collision id_to_string id name nm; (* Sanity check *) assert (not (StringSet.mem name nm.names_set)); (* Insert *) @@ -743,17 +756,42 @@ let allow_collisions (id : id) : bool = let ctx_add (is_opaque : bool) (id : id) (name : string) (ctx : extraction_ctx) : extraction_ctx = - (* We do not use the same name map if we allow/disallow collisions *) + (* The id_to_string function to print nice debugging messages if there are + * collisions *) + let id_to_string (id : id) : string = id_to_string id ctx in + (* We do not use the same name map if we allow/disallow collisions. + We notably use it for field names: some backends like Lean can use the + type information to disambiguate field projections. + + Remark: what we do is actually subtle. Taking the example of fields: + - we allow fields from different ADT definitions to collide + - we do *not* allow field names to collide with other names + For instance, we don't allow naming a field "let". We enforce this by + not checking collision between ids for which we permit collisions (ex.: + between fields), but still checking collisions between those ids and the + others (ex.: fields and keywords). + *) if allow_collisions id then ( assert (not is_opaque); + (* Check with the other ids *) + names_map_check_collision id_to_string id name ctx.names_map; { ctx with unsafe_names_map = unsafe_names_map_add id name ctx.unsafe_names_map; }) else - (* The id_to_string function to print nice debugging messages if there are - * collisions *) - let id_to_string (id : id) : string = id_to_string id ctx in + (* Remark: we don't check that there are no collisions with the unsafe ids. + Importantly, we don't want some safe ids like keywords to clash with + unsafe ids like fields names. For this, we leverage the fact that we register + keywords *first*, then unsafe ids (meaning the clash will be detected with + the check in the other branch of the if ... then ... else ..., and we do + have to check for all possible collisions, which may be slightly too + restrictive). + + TODO: this is a bit hacky, we might want to improve the way we detect + clashes by being more precise. Overall, there is only an issue with + field names which are allowed to clash with each other. + *) let names_map = names_map_add id_to_string is_opaque id name ctx.names_map in |