From 3ecca99a25369fecf990d922e6ccbaa31f71190a Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 4 Mar 2022 13:15:16 +0100
Subject: Make minor modifications to the variable names generation

---
 src/ExtractToFStar.ml        | 10 +++++++---
 src/Names.ml                 |  5 +++++
 tests/misc/External.Funs.fst |  2 +-
 3 files changed, 13 insertions(+), 4 deletions(-)

diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index 9ec74ff0..1f59075a 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -321,11 +321,15 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
                   TypeDeclId.Map.find adt_id ctx.type_context.type_decls
                 in
                 (* We do the following:
-                 * - compute the type name converted_to_snake_case
+                 * - compute the type name, and retrieve the last ident
+                 * - convert this to snake case
                  * - take the first letter of every "letter group"
-                 * Ex.: "TypeVar" -> "type_var" -> "tv"
+                 * Ex.: ["hashmap"; "HashMap"] ~~> "HashMap" -> "hash_map" -> "hm"
                  *)
-                let cl = type_name_to_snake_case def.name in
+                (* Thename shouldn't be empty, and its last element should
+                 * be an ident *)
+                let cl = List.nth def.name (List.length def.name - 1) in
+                let cl = to_snake_case (Names.as_ident cl) in
                 let cl = String.split_on_char '_' cl in
                 let cl = List.filter (fun s -> String.length s > 0) cl in
                 assert (List.length cl > 0);
diff --git a/src/Names.ml b/src/Names.ml
index 41177c37..5785d06f 100644
--- a/src/Names.ml
+++ b/src/Names.ml
@@ -60,3 +60,8 @@ let filter_disambiguators_zero (n : name) : name =
     match pe with Ident _ -> true | Disambiguator d -> d <> Disambiguator.zero
   in
   List.filter pred n
+
+let as_ident (pe : path_elem) : string =
+  match pe with
+  | Ident s -> s
+  | Disambiguator _ -> raise (Failure "Improper variant")
diff --git a/tests/misc/External.Funs.fst b/tests/misc/External.Funs.fst
index 8030b838..927dad9c 100644
--- a/tests/misc/External.Funs.fst
+++ b/tests/misc/External.Funs.fst
@@ -36,7 +36,7 @@ let test_new_non_zero_u32_fwd
       core_option_option_unwrap_fwd core_num_nonzero_non_zero_u32_t opt st0
       with
     | Fail -> Fail
-    | Return (st1, cnnnzu) -> Return (st1, cnnnzu)
+    | Return (st1, nzu) -> Return (st1, nzu)
     end
   end
 
-- 
cgit v1.2.3