Update the generation of names

7 files changed, 57 insertions, 39 deletions

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index b9c6b1b0..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 =
@@ -1108,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
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 =
diff --git a/compiler/ExtractName.ml b/compiler/ExtractName.ml
index b53f4cdd..dfac6546 100644
--- a/compiler/ExtractName.ml
+++ b/compiler/ExtractName.ml
@@ -39,37 +39,46 @@ let pattern_to_extract_name (name : pattern) : string list =
     | GRegion (RVar _) -> true
     | _ -> false
   in
-  let all_vars = List.for_all is_var in
-  let elem_to_string (e : pattern_elem) : string =
-    match e with
-    | PIdent _ -> pattern_elem_to_string c e
-    | PImpl ty -> (
+  let all_distinct_vars = List.for_all is_var in
+
+  (* This is a bit of a hack: we want to simplify the occurrences of
+     tuples of two variables, arrays with only variables, slices with
+     only variables, etc.
+     We explore the pattern and replace such occurrences with a specific name.
+  *)
+  let visitor =
+    object
+      inherit [_] map_pattern as super
+
+      method! visit_PImpl _ ty =
+        (* TODO: Option *)
         match ty with
         | EComp id -> (
             (* Retrieve the last ident *)
             let id = Collections.List.last id in
             match id with
-            | PIdent (s, g) ->
-                if all_vars g then s else pattern_elem_to_string c id
+            | PIdent (s, g) as id ->
+                if all_distinct_vars g then PImpl (EComp [ PIdent (s, []) ])
+                else super#visit_PImpl () (EComp [ id ])
             | PImpl _ -> raise (Failure "Unreachable"))
-        | EPrimAdt (adt, g) ->
-            if all_vars g then
-              match adt with
-              | TTuple ->
-                  let l = List.length g in
-                  if l = 2 then "Pair" else expr_to_string c ty
-              | TArray -> "Array"
-              | TSlice -> "Slice"
-            else expr_to_string c ty
-        | ERef _ | EVar _ | EArrow _ | ERawPtr _ ->
-            (* We simply convert the pattern to a string. This is not very
-               satisfying but we should rarely get there. *)
-            expr_to_string c ty)
-  in
-  let rec pattern_to_string (n : pattern) : string list =
-    match n with [] -> [] | e :: n -> elem_to_string e :: pattern_to_string n
+        | _ -> super#visit_PImpl () ty
+
+      method! visit_EPrimAdt _ adt g =
+        if all_distinct_vars g then
+          match adt with
+          | TTuple ->
+              let l = List.length g in
+              if l = 2 then EComp [ PIdent ("Pair", []) ]
+              else super#visit_EPrimAdt () adt g
+          | TArray -> EComp [ PIdent ("Array", []) ]
+          | TSlice -> EComp [ PIdent ("Slice", []) ]
+          (*else if adt = TTuple && List.length g = 2 then
+            super#visit_EComp () [ PIdent ("Pair", g) ]*)
+        else super#visit_EPrimAdt () adt g
+    end
   in
-  pattern_to_string name
+  let name = visitor#visit_pattern () name in
+  List.map (pattern_elem_to_string c) name
 
 let pattern_to_type_extract_name = pattern_to_extract_name
 let pattern_to_fun_extract_name = pattern_to_extract_name
diff --git a/compiler/Interpreter.ml b/compiler/Interpreter.ml
index fd3e334b..ccae4588 100644
--- a/compiler/Interpreter.ml
+++ b/compiler/Interpreter.ml
@@ -68,12 +68,12 @@ let normalize_inst_fun_sig (ctx : eval_ctx) (sg : inst_fun_sig) : inst_fun_sig =
     normalize because a trait clause was instantiated with a specific trait ref).
  *)
 let symbolic_instantiate_fun_sig (ctx : eval_ctx) (sg : fun_sig)
-    (regions_hierarchy : region_var_groups) (kind : fun_kind) :
+    (regions_hierarchy : region_var_groups) (kind : item_kind) :
     eval_ctx * inst_fun_sig =
   let tr_self =
     match kind with
-    | RegularKind | TraitMethodImpl _ -> UnknownTrait __FUNCTION__
-    | TraitMethodDecl _ | TraitMethodProvided _ -> Self
+    | RegularKind | TraitItemImpl _ -> UnknownTrait __FUNCTION__
+    | TraitItemDecl _ | TraitItemProvided _ -> Self
   in
   let generics =
     let { regions; types; const_generics; trait_clauses } = sg.generics in
diff --git a/compiler/LlbcAstUtils.ml b/compiler/LlbcAstUtils.ml
index d3fac032..1053c9ab 100644
--- a/compiler/LlbcAstUtils.ml
+++ b/compiler/LlbcAstUtils.ml
@@ -44,7 +44,7 @@ let crate_get_opaque_non_builtin_decls (k : crate) (filter_assumed : bool) :
     d.body = None
     (* Something to pay attention to: we must ignore trait method *declarations*
        (which don't have a body but must not be considered as opaque) *)
-    && (match d.kind with TraitMethodDecl _ -> false | _ -> true)
+    && (match d.kind with TraitItemDecl _ -> false | _ -> true)
     && ((not filter_assumed)
        || (not (NameMatcherMap.mem ctx d.name builtin_globals_map))
           && not (NameMatcherMap.mem ctx d.name (builtin_funs_map ())))
diff --git a/compiler/Pure.ml b/compiler/Pure.ml
index dd7a4acf..33c23cc3 100644
--- a/compiler/Pure.ml
+++ b/compiler/Pure.ml
@@ -1063,13 +1063,13 @@ type fun_body = {
 }
 [@@deriving show]
 
-type fun_kind = A.fun_kind [@@deriving show]
+type item_kind = A.item_kind [@@deriving show]
 
 type fun_decl = {
   def_id : FunDeclId.id;
   is_local : bool;
   meta : meta;
-  kind : fun_kind;
+  kind : item_kind;
   num_loops : int;
       (** The number of loops in the parent forward function (basically the number
           of loops appearing in the original Rust functions, unless some loops are
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index c12de045..48a3685b 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -730,7 +730,7 @@ let extract_definitions (fmt : Format.formatter) (config : gen_config)
            the trait declarations themselves, there is no point in having
            separate type definitions) *)
         match pure_fun.f.Pure.kind with
-        | TraitMethodDecl _ -> ()
+        | TraitItemDecl _ -> ()
         | _ ->
             (* Translate *)
             export_functions_group [ pure_fun ])