Merge pull request #3981 from FStarLang/_taramana_prettify_types

Tactics.PrettifyTypes: some improvements on generated types

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} =
@@ -32,17 +32,17 @@ type named_ty =
     (named "Case1" ((named "x" int & int) & (named "y" int & string)))
     (named "Case2" (named "b" bool))
 
-// bijection record disabled for now
-(*
 %splice[
   named_ty_pretty;
-  Case1;
-  Case2;
-  named_ty_pretty_bij;
-] (entry "_pretty" (`%named_ty))
+  Mknamed_ty_pretty_Case1;
+  Mknamed_ty_pretty_Case2;
+// named_ty_pretty_bij; // bijection record disabled for now
+] (entry "named_ty_pretty" (`%named_ty))
 
 // test bijection
 
+// bijection record disabled for now
+(*
 let _ = assert (Inl ((1, 2), (3, "a")) >> named_ty_pretty_bij == Case1 1 2 3 "a")
 let _ = assert (Case2 false << named_ty_pretty_bij == Inr false)
 *)
@@ -51,22 +51,46 @@ let _ = assert (Case2 false << named_ty_pretty_bij == Inr false)
 type can't be called? *)
 // let test (i : named_ty_pretty) =
 //   match i with
-//   | Case1 _ _ _ _ ->
-//     let _ = Case1?.x i in
-//     let _ = Case1?.y i in
+//   | Mknamed_ty_pretty_Case1 _ _ _ _ ->
+//     let _ = Mknamed_ty_pretty_Case1?.x i in
+//     let _ = Mknamed_ty_pretty_Case1?.y i in
 //     ()
-//   | Case2 _ ->
-//     let _ = Case2?.b i in
+//   | Mknamed_ty_pretty_Case2 _ ->
+//     let _ = Mknamed_ty_pretty_Case2?.b i in
 //     ()
 
+let test_named_ty1 (i : named_ty_pretty) =
+  match i with
+  | Mknamed_ty_pretty_Case1 _ _ _ _
+  | Mknamed_ty_pretty_Case2 _ ->
+    ()
+
+(* Named test: *)
+type named_ty2 =
+  either
+    (named "Case1" ((named "x" int & int) & (named "y" int & string)))
+    (named "Case2" (named "b" bool))
+
+%splice[
+  named_ty2_pretty;
+  Mknamed_ty2_pretty_Case1;
+  Mknamed_ty2_pretty_Case2;
+] (entry "named_ty2_pretty" (`%named_ty2))
+
+let test_named_ty2 (i : named_ty2_pretty) =
+  match i with
+  | Mknamed_ty2_pretty_Case1 _ _ _ _
+  | Mknamed_ty2_pretty_Case2 _ ->
+    ()
+
 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
 
@@ -79,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 <|
@@ -126,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

@@ -113,7 +113,9 @@ let rec flatten_type (pretty_tynm : name) (ctr:nat) (t:parsed_type) : Tac (nat &
     ctr, Sum (aa @ bb)
   | Named s t ->
     let _, p = as_prod_type 0 t in
-    ctr, Sum [(s, p)]
+    assume (List.length pretty_tynm > 0);
+    let _, s0 = unsnoc pretty_tynm in
+    ctr, Sum [("Mk" ^ s0 ^ "_" ^ s, p)]
   | t ->
     let _, p = as_prod_type 0 t in
     assume (List.length pretty_tynm > 0);
@@ -451,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
@@ -462,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);