diff options
Diffstat (limited to 'compiler/Extract.ml')
| -rw-r--r-- | compiler/Extract.ml | 64 |
1 files changed, 46 insertions, 18 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 794a1bfa..46f6a1ca 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -19,7 +19,7 @@ let extract_fun_decl_register_names (ctx : extraction_ctx) only use their type for the fields of the records we generate for the trait declarations *) match def.f.kind with - | TraitMethodDecl _ -> ctx + | TraitItemDecl _ -> ctx | _ -> ( (* Check if the function is builtin *) let builtin = @@ -48,6 +48,9 @@ let extract_fun_decl_register_names (ctx : extraction_ctx) ctx_add (FunId (FromLlbc fun_id)) fun_info.extract_name ctx | None -> (* Not builtin *) + (* If this is a trait method implementation, we prefix the name with the + name of the trait implementation. We need to do so because there + can be clashes otherwise. *) (* Register the decrease clauses, if necessary *) let register_decreases ctx def = if has_decreases_clause def then @@ -1105,7 +1108,7 @@ let extract_fun_parameters (space : bool ref) (ctx : extraction_ctx) *) let ctx, trait_decl = match def.kind with - | TraitMethodProvided (decl_id, _) -> + | TraitItemProvided (decl_id, _) -> let trait_decl = T.TraitDeclId.Map.find decl_id ctx.trans_trait_decls in let ctx, _ = ctx_add_trait_self_clause ctx in let ctx = { ctx with is_provided_method = true } in @@ -1204,9 +1207,14 @@ let extract_template_fstar_decreases_clause (ctx : extraction_ctx) (* Add a break before *) F.pp_print_break fmt 0 0; (* Print a comment to link the extracted type to its original rust definition *) - extract_comment_with_span fmt - [ "[" ^ name_to_string ctx def.llbc_name ^ "]: decreases clause" ] - def.meta.span; + (let name = + if !Config.extract_external_name_patterns && not def.is_local then + Some def.llbc_name + else None + in + extract_comment_with_span ctx fmt + [ "[" ^ name_to_string ctx def.llbc_name ^ "]: decreases clause" ] + name def.meta.span); F.pp_print_space fmt (); (* Open a box for the definition, so that whenever possible it gets printed on * one line *) @@ -1267,9 +1275,9 @@ let extract_template_lean_termination_and_decreasing (ctx : extraction_ctx) (* Add a break before *) F.pp_print_break fmt 0 0; (* Print a comment to link the extracted type to its original rust definition *) - extract_comment_with_span fmt + extract_comment_with_span ctx fmt [ "[" ^ name_to_string ctx def.llbc_name ^ "]: termination measure" ] - def.meta.span; + None def.meta.span; F.pp_print_space fmt (); (* Open a box for the definition, so that whenever possible it gets printed on * one line *) @@ -1322,9 +1330,9 @@ let extract_template_lean_termination_and_decreasing (ctx : extraction_ctx) let def_name = ctx_get_decreases_proof def.def_id def.loop_id ctx in (* syntax <def_name> term ... term : tactic *) F.pp_print_break fmt 0 0; - extract_comment_with_span fmt + extract_comment_with_span ctx fmt [ "[" ^ name_to_string ctx def.llbc_name ^ "]: decreases_by tactic" ] - def.meta.span; + None def.meta.span; F.pp_print_space fmt (); F.pp_open_hvbox fmt 0; F.pp_print_string fmt "syntax \""; @@ -1364,7 +1372,12 @@ let extract_fun_comment (ctx : extraction_ctx) (fmt : F.formatter) in [ comment_pre ^ loop_comment ] in - extract_comment_with_span fmt comment def.meta.span + let name = + if !Config.extract_external_name_patterns && not def.is_local then + Some def.llbc_name + else None + in + extract_comment_with_span ctx fmt comment name def.meta.span (** Extract a function declaration. @@ -1813,9 +1826,14 @@ let extract_global_decl (ctx : extraction_ctx) (fmt : F.formatter) (* Add a break then the name of the corresponding LLBC declaration *) F.pp_print_break fmt 0 0; - extract_comment_with_span fmt + let name = + if !Config.extract_external_name_patterns && not global.is_local then + Some global.name + else None + in + extract_comment_with_span ctx fmt [ "[" ^ name_to_string ctx global.name ^ "]" ] - global.meta.span; + name global.meta.span; F.pp_print_space fmt (); let decl_name = ctx_get_global global.def_id ctx in @@ -2207,9 +2225,14 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter) (* Add a break before *) F.pp_print_break fmt 0 0; (* Print a comment to link the extracted type to its original rust definition *) - extract_comment_with_span fmt - [ "Trait declaration: [" ^ name_to_string ctx decl.llbc_name ^ "]" ] - decl.meta.span; + (let name = + if !Config.extract_external_name_patterns && not decl.is_local then + Some decl.llbc_name + else None + in + extract_comment_with_span ctx fmt + [ "Trait declaration: [" ^ name_to_string ctx decl.llbc_name ^ "]" ] + name decl.meta.span); F.pp_print_break fmt 0 0; (* Open two outer boxes for the definition, so that whenever possible it gets printed on one line and indents are correct. @@ -2490,9 +2513,14 @@ let extract_trait_impl (ctx : extraction_ctx) (fmt : F.formatter) (* Add a break before *) F.pp_print_break fmt 0 0; (* Print a comment to link the extracted type to its original rust definition *) - extract_comment_with_span fmt - [ "Trait implementation: [" ^ name_to_string ctx impl.llbc_name ^ "]" ] - impl.meta.span; + (let name = + if !Config.extract_external_name_patterns && not impl.is_local then + Some impl.llbc_name + else None + in + extract_comment_with_span ctx fmt + [ "Trait implementation: [" ^ name_to_string ctx impl.llbc_name ^ "]" ] + name impl.meta.span); F.pp_print_break fmt 0 0; (* Open two outer boxes for the definition, so that whenever possible it gets printed on |