Fix a minor issue and regenerate some F* test files

1 files changed, 20 insertions, 9 deletions

diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index 8ffbce41..dcd69f2b 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -622,11 +622,18 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
     | FStar | Lean | HOL4 -> name
     | Coq -> capitalize_first_letter name
   in
-  let type_name name =
+  let get_type_name_no_suffix name =
     match !backend with
-    | FStar | Coq | HOL4 -> type_name_to_snake_case name ^ "_t"
+    | FStar | Coq | HOL4 -> String.concat "_" (get_type_name name)
     | Lean -> String.concat "." (get_type_name name)
   in
+  let type_name name =
+    match !backend with
+    | FStar ->
+        StringUtils.lowercase_first_letter (get_type_name_no_suffix name ^ "_t")
+    | Coq | HOL4 -> get_type_name_no_suffix name ^ "_t"
+    | Lean -> get_type_name_no_suffix name
+  in
   let field_name (def_name : name) (field_id : FieldId.id)
       (field_name : string option) : string =
     let field_name_s =
@@ -641,15 +648,18 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
         "_" ^ field_name_s
       else field_name_s
     else
-      let def_name = type_name_to_snake_case def_name ^ "_" in
-      def_name ^ field_name_s
+      let def_name = get_type_name_no_suffix def_name ^ "_" ^ field_name_s in
+      match !backend with
+      | Lean | HOL4 -> def_name
+      | Coq | FStar -> StringUtils.lowercase_first_letter def_name
   in
   let variant_name (def_name : name) (variant : string) : string =
     match !backend with
     | FStar | Coq | HOL4 ->
         let variant = to_camel_case variant in
         if variant_concatenate_type_name then
-          type_name_to_camel_case def_name ^ variant
+          StringUtils.capitalize_first_letter
+            (get_type_name_no_suffix def_name ^ "_" ^ variant)
         else variant
     | Lean -> variant
   in
@@ -660,7 +670,10 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
   let get_fun_name fname =
     let fname = get_name fname in
     (* TODO: don't convert to snake case for Coq, HOL4, F* *)
-    flatten_name fname
+    let fname = flatten_name fname in
+    match !backend with
+    | FStar | Coq | HOL4 -> StringUtils.lowercase_first_letter fname
+    | Lean -> fname
   in
   let global_name (name : global_name) : string =
     (* Converting to snake case also lowercases the letters (in Rust, global
@@ -688,9 +701,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
        with the trait decl name *)
     let trait_decl =
       let name = trait_decl.name in
-      match !backend with
-      | FStar | Coq | HOL4 -> type_name_to_snake_case name ^ "_inst"
-      | Lean -> String.concat "" (get_type_name name) ^ "Inst"
+      get_type_name_no_suffix name ^ "Inst"
     in
     flatten_name (get_type_name trait_impl.name @ [ trait_decl ])
   in