diff options
Diffstat (limited to '')
-rw-r--r-- | compiler/ExtractBase.ml | 21 |
1 files changed, 15 insertions, 6 deletions
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index e0614af1..5e97cd21 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -1374,10 +1374,11 @@ let ctx_compute_fun_name_no_suffix (ctx : extraction_ctx) (fname : llbc_name) : (** Provided a basename, compute the name of a global declaration. *) let ctx_compute_global_name (ctx : extraction_ctx) (name : llbc_name) : string = - (* Converting to snake case also lowercases the letters (in Rust, global - * names are written in capital letters). *) - let parts = List.map to_snake_case (ctx_compute_simple_name ctx name) in - String.concat "_" parts + match !Config.backend with + | Coq | FStar | HOL4 -> + let parts = List.map to_snake_case (ctx_compute_simple_name ctx name) in + String.concat "_" parts + | Lean -> flatten_name (ctx_compute_simple_name ctx name) (** Helper function: generate a suffix for a function name, i.e., generates a suffix like "_loop", "loop1", etc. to append to a function name. @@ -1511,6 +1512,7 @@ let ctx_compute_trait_parent_clause_name (ctx : extraction_ctx) if !Config.record_fields_short_names then clause else ctx_compute_trait_decl_name ctx trait_decl ^ "_" ^ clause in + let clause = clause ^ "Inst" in match !backend with | FStar -> StringUtils.lowercase_first_letter clause | Coq | HOL4 | Lean -> clause @@ -1888,8 +1890,15 @@ let ctx_add_global_decl_and_body (def : A.global_decl) (ctx : extraction_ctx) : (* Not the case: "standard" registration *) let name = ctx_compute_global_name ctx def.name in let body = FunId (FromLlbc (FunId (FRegular def.body), None)) in - let ctx = ctx_add decl (name ^ "_c") ctx in - let ctx = ctx_add body (name ^ "_body") ctx in + (* If this is a provided constant (i.e., the default value for a constant + in a trait declaration) we add a suffix. Otherwise there is a clash + between the name for the default constant and the name for the field + in the trait declaration *) + let suffix = + match def.kind with TraitItemProvided _ -> "_default" | _ -> "" + in + let ctx = ctx_add decl (name ^ suffix) ctx in + let ctx = ctx_add body (name ^ suffix ^ "_body") ctx in ctx let ctx_compute_fun_name (def : fun_decl) (ctx : extraction_ctx) : string = |