diff options
Diffstat (limited to '')
| -rw-r--r-- | compiler/ExtractBase.ml | 24 |
1 files changed, 18 insertions, 6 deletions
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index 612cf359..1996d38f 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -245,7 +245,7 @@ type formatter = { - loop identifier, if this is for a loop *) trait_decl_name : trait_decl -> string; - trait_impl_name : trait_impl -> string; + trait_impl_name : trait_decl -> trait_impl -> string; trait_parent_clause_name : trait_decl -> trait_clause -> string; trait_const_name : trait_decl -> string -> string; trait_type_name : trait_decl -> string -> string; @@ -523,7 +523,8 @@ let report_name_collision (id_to_string : id -> string) (id1 : id) (id2 : id) ^ "\nYou may want to rename some of your definitions, or report an issue." in log#serror err; - raise (Failure err) + (* If we fail hard on errors, raise an exception *) + if !Config.extract_fail_hard then 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 @@ -534,15 +535,21 @@ let names_map_check_collision (id_to_string : id -> string) (id : id) | None -> () (* Ok *) | Some clash -> (* There is a clash: print a nice debugging message for the user *) - if !Config.extract_fail_hard then - report_name_collision id_to_string clash id name + 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)); + if StringSet.mem name nm.names_set then ( + let err = + "Error when registering the name for id: " ^ id_to_string id + ^ ":\nThe chosen name is already in the names set: " ^ name + in + log#serror err; + (* If we fail hard on errors, raise an exception *) + if !Config.extract_fail_hard then raise (Failure err)); (* Insert *) let id_to_name = IdMap.add id name nm.id_to_name in let name_to_id = StringMap.add name id nm.name_to_id in @@ -1284,8 +1291,13 @@ let ctx_add_trait_decl (d : trait_decl) (ctx : extraction_ctx) : extraction_ctx let ctx_add_trait_impl (d : trait_impl) (ctx : extraction_ctx) : extraction_ctx = + (* We need to lookup the trait decl that is implemented by the trait impl *) + let decl = + Pure.TraitDeclId.Map.find d.impl_trait.trait_decl_id ctx.trans_trait_decls + in + (* Compute the name *) let is_opaque = false in - let name = ctx.fmt.trait_impl_name d in + let name = ctx.fmt.trait_impl_name decl d in ctx_add is_opaque (TraitImplId d.def_id) name ctx let ctx_add_trait_const (d : trait_decl) (item : string) (ctx : extraction_ctx) |