diff options
| -rw-r--r-- | compiler/Extract.ml | 28 | ||||
| -rw-r--r-- | compiler/ExtractBase.ml | 24 |
2 files changed, 39 insertions, 13 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 864d513f..60455cd9 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -655,6 +655,11 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) | _ -> raise (Failure ("Unexpected name shape: " ^ Print.name_to_string name)) in + let flatten_name (name : string list) : string = + match !backend with + | FStar | Coq | HOL4 -> String.concat "_" name + | Lean -> String.concat "." name + in let get_type_name = get_name in let type_name_to_camel_case name = let name = get_type_name name in @@ -708,9 +713,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) let get_fun_name fname = let fname = get_name fname in (* TODO: don't convert to snake case for Coq, HOL4, F* *) - match !backend with - | FStar | Coq | HOL4 -> String.concat "_" (List.map to_snake_case fname) - | Lean -> String.concat "." fname + flatten_name fname in let global_name (name : global_name) : string = (* Converting to snake case also lowercases the letters (in Rust, global @@ -732,8 +735,18 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string) type_name_to_snake_case trait_decl.name in - let trait_impl_name (trait_impl : trait_impl) : string = - get_fun_name trait_impl.name + let trait_impl_name (trait_decl : trait_decl) (trait_impl : trait_impl) : + string = + (* TODO: provisional: we concatenate the trait impl name (which is its type) + with the trait decl name *) + let inst_keyword = + match !backend with + | HOL4 | FStar | Coq -> "_instance" + | Lean -> "Instance" + in + flatten_name + (get_type_name trait_impl.name + @ [ trait_decl_name trait_decl ^ inst_keyword ]) in let trait_parent_clause_name (trait_decl : trait_decl) (clause : trait_clause) @@ -4017,8 +4030,9 @@ let extract_trait_impl_register_names (ctx : extraction_ctx) (trait_impl : trait_impl) : extraction_ctx = (* For now we do not support overriding provided methods *) assert (trait_impl.provided_methods = []); - (* Everything is actually taken care of by {!extract_trait_decl_register_names} *) - ctx + (* Everything is taken care of by {!extract_trait_decl_register_names} *but* + the name of the implementation itself *) + ctx_add_trait_impl trait_impl ctx (** Small helper. 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) |