Concrete ident for coq

hacspec · Oct 30, 2024 · 96e7a0e · 96e7a0e
1 parent abdcd67
commit 96e7a0e
Showing 1 changed file with 13 additions and 8 deletions.
diff --git a/engine/lib/concrete_ident/concrete_ident.ml b/engine/lib/concrete_ident/concrete_ident.ml
@@ -346,7 +346,10 @@ module View = struct
         path
     in
     let sep = "__" in
-    let subst = String.substr_replace_all ~pattern:sep ~with_:(sep ^ "_") in
+    let subst =
+      String.substr_replace_all ~pattern:sep ~with_:(sep ^ "_")
+      >> String.substr_replace_all ~pattern:"___" ~with_:""
+    in
     let fake_path, real_path =
       (* Detects paths of nested items *)
       List.rev def_id.path |> List.tl_exn
@@ -472,7 +475,7 @@ module MakeViewAPI (NP : NAME_POLICY) : VIEW_API = struct
         else escape name
     | Constructor { is_struct } ->
         let name =
-          if start_lowercase name || is_reserved_word name then "C_" ^ name
+          if start_lowercase name || is_reserved_word name then "t_" ^ name
           else escape name
         in
         if is_struct then NP.struct_constructor_name_transform name
@@ -498,17 +501,19 @@ module MakeViewAPI (NP : NAME_POLICY) : VIEW_API = struct
         |> Option.some
       with _ -> None
     in
-    let path, definition =
+    let path, definition, extra =
       match kind with
       | Constructor { is_struct = false } ->
           ( List.drop_last_exn path,
-            Option.value_exn type_name ^ "_" ^ definition )
+            Option.value_exn type_name ^ "_" ^ definition,
+            "t_" (* ^ List.last_exn path ^ "_" *) )
       | Field when List.last path |> [%equal: string option] type_name ->
-          (List.drop_last_exn path, definition)
-      | AssociatedItem _ -> (List.drop_last_exn path, definition)
-      | _ -> (path, definition)
+          (List.drop_last_exn path, definition, "t_" ^ List.last_exn path ^ "_")
+      | AssociatedItem _ ->
+          (List.drop_last_exn path, definition, "t_" ^ List.last_exn path ^ "_")
+      | _ -> (path, definition, "")
     in
-    let definition = rename_definition path definition kind type_name in
+    let definition = extra ^ rename_definition path definition kind type_name in
     View.{ crate; path; definition }
 
   and to_view ({ def_id; kind } : t) : view =