Tactics.Prettify: allow the user to define the full name of a new type

Author: tahina-pro

tests/tactics/Prettify.fst

@@ -13,7 +13,7 @@ type myty =
   myty_pretty_right;
   Mkmyty_pretty0;
   Mkmyty_pretty1
-] (entry "_pretty" (`%myty))
+] (entry "myty_pretty" (`%myty))
 
 (* Sanity check *)
 let right (x : myty) : r:myty_pretty{myty_pretty_right x == r} =
@@ -37,7 +37,7 @@ type named_ty =
   Mknamed_ty_pretty_Case1;
   Mknamed_ty_pretty_Case2;
 // named_ty_pretty_bij; // bijection record disabled for now
-] (entry "_pretty" (`%named_ty))
+] (entry "named_ty_pretty" (`%named_ty))
 
 // test bijection
 
@@ -75,7 +75,7 @@ type named_ty2 =
   named_ty2_pretty;
   Mknamed_ty2_pretty_Case1;
   Mknamed_ty2_pretty_Case2;
-] (entry "_pretty" (`%named_ty2))
+] (entry "named_ty2_pretty" (`%named_ty2))
 
 let test_named_ty2 (i : named_ty2_pretty) =
   match i with
@@ -84,13 +84,13 @@ let test_named_ty2 (i : named_ty2_pretty) =
     ()
 
 type t2 = tuple2 int int
-%splice[t2_pretty] (entry "_pretty" (`%t2))
+%splice[t2_pretty] (entry "t2_pretty" (`%t2))
 
 type t3 = tuple2 int (either bool string)
-%splice[t3_pretty] (entry "_pretty" (`%t3))
+%splice[t3_pretty] (entry "t3_pretty" (`%t3))
 
 type t4 = either t3 (tuple2 int (either bool string))
-%splice[t4_pretty; t4_pretty_left_right] (entry "_pretty" (`%t4))
+%splice[t4_pretty; t4_pretty_left_right] (entry "t4_pretty" (`%t4))
 
 let inv (x:t4) = t4_pretty_left_right x
 
@@ -103,7 +103,7 @@ type t5 =
 noextract
 noeq (* will only go to the generated type. *)
 unfold
-%splice[t5_quals; t5_quals_left_right] (entry "_quals" (`%t5))
+%splice[t5_quals; t5_quals_left_right] (entry "t5_quals" (`%t5))
 
 type big =
   either int <|
@@ -150,4 +150,6 @@ type bigger =
   ) bool
 
 [@@no_auto_projectors] // makes it a bit faster
-%splice[] (entry "_pretty" (`%bigger))
+%splice[huger] (entry "huger" (`%bigger))
+
+let _ = huger

ulib/FStar.Tactics.PrettifyType.fst

@@ -453,7 +453,7 @@ let mk_bij cfg : Tac decls =
   [pack_sigelt sv]
 
 [@@plugin]
-let entry (suf nm : string) : Tac decls =
+let entry (pretty_tynm nm : string) : Tac decls =
   // print ("ENTRY, n quals = " ^ string_of_int (List.length (splice_quals ())));
   // print ("ENTRY, n attrs = " ^ string_of_int (List.length (splice_attrs ())));
   let quals = splice_quals () in
@@ -464,7 +464,9 @@ let entry (suf nm : string) : Tac decls =
   // print ("def: " ^ term_to_string def);
   let at = parse_type def in
   // print ("at: " ^ parsed_type_to_string at);
-  let pretty_tynm = add_suffix suf nm in
+  assume (List.length nm > 0);
+  let qns, _ = unsnoc nm in
+  let pretty_tynm = qns @ [pretty_tynm] in
   let _, fat = flatten_type pretty_tynm 0 at in
   // print ("fat: " ^ flat_type_to_string fat);