From 42a0a49621f661e19137236f32a9ee212e4343a5 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 21 Nov 2023 17:38:14 +0100
Subject: Update the generation of names for the parent trait clauses

---
 compiler/ExtractBase.ml | 33 +++++++++++++++++++++++++++++----
 1 file changed, 29 insertions(+), 4 deletions(-)

diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 0b9908b2..6f227003 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -1510,10 +1510,35 @@ let ctx_compute_trait_decl_constructor (ctx : extraction_ctx)
 
 let ctx_compute_trait_parent_clause_name (ctx : extraction_ctx)
     (trait_decl : trait_decl) (clause : trait_clause) : string =
-  (* TODO: improve - it would be better to not use indices *)
-  let clause = "parent_clause_" ^ TraitClauseId.to_string clause.clause_id in
-  if !Config.record_fields_short_names then clause
-  else ctx_compute_trait_decl_name ctx trait_decl ^ "_" ^ clause
+  (* We derive the name of the clause from the trait instance.
+     For instance, if the clause gives us an instance of `Foo<u32>`,
+     we generate a name along the lines of "fooU32Inst".
+  *)
+  (* We need to lookup the LLBC definitions, to have the original instantiation *)
+  let clause =
+    let trait_decl =
+      TraitDeclId.Map.find trait_decl.def_id ctx.crate.trait_decls
+    in
+    let clause =
+      List.find
+        (fun (c : Types.trait_clause) -> c.clause_id = clause.clause_id)
+        trait_decl.parent_clauses
+    in
+    let trait_id = clause.trait_id in
+    let impl_trait_decl = TraitDeclId.Map.find trait_id ctx.crate.trait_decls in
+    let params = trait_decl.generics in
+    let args = clause.clause_generics in
+    name_with_generics_to_simple_name ctx.trans_ctx impl_trait_decl.name params
+      args
+  in
+  let clause = String.concat "" clause in
+  let clause =
+    if !Config.record_fields_short_names then clause
+    else ctx_compute_trait_decl_name ctx trait_decl ^ "_" ^ clause
+  in
+  match !backend with
+  | FStar -> StringUtils.lowercase_first_letter clause
+  | Coq | HOL4 | Lean -> clause
 
 let ctx_compute_trait_type_name (ctx : extraction_ctx) (trait_decl : trait_decl)
     (item : string) : string =
-- 
cgit v1.2.3