feat: bettern parenthsing of patterns

CoqOfRust/blacklist.txt

@@ -3,7 +3,6 @@ examples/default/examples/ink_contracts/erc1155.v
 examples/default/examples/ink_contracts/erc721.v
 examples/default/examples/ink_contracts/mother.v
 examples/default/examples/ink_contracts/multisig.v
-examples/default/examples/ink_contracts/trait_erc20.v
 # blacklisting for changes that explicit M.Val
 examples/axiomatized/examples/conversion/try_from_and_try_into.v
 examples/axiomatized/examples/expressions/const_underscore_expression.v

CoqOfRust/examples/default/examples/cargo/concurrent_tests.v

@@ -28,7 +28,7 @@ Definition foo {A : Set} (o : core.option.Option.t A) : M unit :=
         let* α5 : unit := M.call (std.io.stdio._print α4) in
         M.alloc α5 in
       M.alloc tt
-    | core.option.Option.None  =>
+    | core.option.Option.None =>
       let* _ : M.Val unit :=
         let* α0 : ref str.t := M.read (mk_str "nothing
 ") in
@@ -101,7 +101,7 @@ Module tests.
                     (Trait := ltac:(refine _)))
                   (borrow_mut iter)) in
             match α0 with
-            | core.option.Option.None  =>
+            | core.option.Option.None =>
               let* α0 : M.Val never.t := Break in
               let* α1 := M.read α0 in
               let* α2 : unit := never_to_any α1 in
@@ -190,7 +190,7 @@ Module tests.
                     (Trait := ltac:(refine _)))
                   (borrow_mut iter)) in
             match α0 with
-            | core.option.Option.None  =>
+            | core.option.Option.None =>
               let* α0 : M.Val never.t := Break in
               let* α1 := M.read α0 in
               let* α2 : unit := never_to_any α1 in
@@ -280,7 +280,7 @@ Definition test_file : M unit :=
                   (Trait := ltac:(refine _)))
                 (borrow_mut iter)) in
           match α0 with
-          | core.option.Option.None  =>
+          | core.option.Option.None =>
             let* α0 : M.Val never.t := Break in
             let* α1 := M.read α0 in
             let* α2 : unit := never_to_any α1 in
@@ -367,7 +367,7 @@ Definition test_file_also : M unit :=
                   (Trait := ltac:(refine _)))
                 (borrow_mut iter)) in
           match α0 with
-          | core.option.Option.None  =>
+          | core.option.Option.None =>
             let* α0 : M.Val never.t := Break in
             let* α1 := M.read α0 in
             let* α2 : unit := never_to_any α1 in

CoqOfRust/examples/default/examples/custom_types/enums.v

@@ -39,7 +39,7 @@ Definition inspect (event : enums.WebEvent.t) : M unit :=
   let* α0 : enums.WebEvent.t := M.read event in
   let* α1 : M.Val unit :=
     match α0 with
-    | enums.WebEvent.PageLoad  =>
+    | enums.WebEvent.PageLoad =>
       let* _ : M.Val unit :=
         let* α0 : ref str.t :=
           M.read
@@ -56,7 +56,7 @@ Definition inspect (event : enums.WebEvent.t) : M unit :=
         let* α5 : unit := M.call (std.io.stdio._print α4) in
         M.alloc α5 in
       M.alloc tt
-    | enums.WebEvent.PageUnload  =>
+    | enums.WebEvent.PageUnload =>
       let* _ : M.Val unit :=
         let* α0 : ref str.t := M.read (mk_str "page unloaded
 ") in

CoqOfRust/examples/default/examples/custom_types/enums_testcase_linked_list.v

@@ -103,7 +103,7 @@ Section Impl_enums_testcase_linked_list_List_t.
             (enums_testcase_linked_list.List.t::["len"] (borrow (deref α1))) in
         let* α3 : u32.t := BinOp.Panic.add (Integer.of_Z 1) α2 in
         M.alloc α3
-      | enums_testcase_linked_list.List.Nil  => M.alloc (Integer.of_Z 0)
+      | enums_testcase_linked_list.List.Nil => M.alloc (Integer.of_Z 0)
       end in
     M.read α2.
 
@@ -172,7 +172,7 @@ Section Impl_enums_testcase_linked_list_List_t.
           let* α15 : alloc.string.String.t := M.call (alloc.fmt.format α14) in
           M.alloc α15 in
         M.pure res
-      | enums_testcase_linked_list.List.Nil  =>
+      | enums_testcase_linked_list.List.Nil =>
         let* res : M.Val alloc.string.String.t :=
           let* α0 : ref str.t := M.read (mk_str "Nil") in
           let* α1 : M.Val (array (ref str.t)) := M.alloc [ α0 ] in

CoqOfRust/examples/default/examples/custom_types/enums_type_aliases_v2.v

@@ -29,14 +29,12 @@ Section Impl_enums_type_aliases_v2_VeryVerboseEnumOfThingsToDoWithNumbers_t.
       M.read self in
     let* α1 : M.Val i32.t :=
       match α0 with
-      | enums_type_aliases_v2.VeryVerboseEnumOfThingsToDoWithNumbers.Add  =>
+      | enums_type_aliases_v2.VeryVerboseEnumOfThingsToDoWithNumbers.Add =>
         let* α0 : i32.t := M.read x in
         let* α1 : i32.t := M.read y in
         let* α2 : i32.t := BinOp.Panic.add α0 α1 in
         M.alloc α2
-      |
-          enums_type_aliases_v2.VeryVerboseEnumOfThingsToDoWithNumbers.Subtract 
-          =>
+      | enums_type_aliases_v2.VeryVerboseEnumOfThingsToDoWithNumbers.Subtract =>
         let* α0 : i32.t := M.read x in
         let* α1 : i32.t := M.read y in
         let* α2 : i32.t := BinOp.Panic.sub α0 α1 in

CoqOfRust/examples/default/examples/custom_types/enums_use.v

@@ -40,7 +40,7 @@ Definition main : M unit :=
   let* _ : M.Val unit :=
     let* α0 : enums_use.Status.t := M.read status in
     match α0 with
-    | enums_use.Status.Rich  =>
+    | enums_use.Status.Rich =>
       let* _ : M.Val unit :=
         let* α0 : ref str.t :=
           M.read (mk_str "The rich have lots of money!
@@ -54,7 +54,7 @@ Definition main : M unit :=
         let* α5 : unit := M.call (std.io.stdio._print α4) in
         M.alloc α5 in
       M.alloc tt
-    | enums_use.Status.Poor  =>
+    | enums_use.Status.Poor =>
       let* _ : M.Val unit :=
         let* α0 : ref str.t := M.read (mk_str "The poor have no money...
 ") in
@@ -71,7 +71,7 @@ Definition main : M unit :=
   let* α0 : enums_use.Work.t := M.read work in
   let* α0 : M.Val unit :=
     match α0 with
-    | enums_use.Work.Civilian  =>
+    | enums_use.Work.Civilian =>
       let* _ : M.Val unit :=
         let* α0 : ref str.t := M.read (mk_str "Civilians work!
 ") in
@@ -84,7 +84,7 @@ Definition main : M unit :=
         let* α5 : unit := M.call (std.io.stdio._print α4) in
         M.alloc α5 in
       M.alloc tt
-    | enums_use.Work.Soldier  =>
+    | enums_use.Work.Soldier =>
       let* _ : M.Val unit :=
         let* α0 : ref str.t := M.read (mk_str "Soldiers fight!
 ") in

CoqOfRust/examples/default/examples/error_handling/combinators_and_then.v

@@ -25,13 +25,13 @@ Section Impl_core_fmt_Debug_for_combinators_and_then_Food_t.
     let* α1 : ref combinators_and_then.Food.t := M.read self in
     let* α2 : M.Val (ref str.t) :=
       match α1 with
-      | combinators_and_then.Food.CordonBleu  =>
+      | combinators_and_then.Food.CordonBleu =>
         let* α0 : ref str.t := M.read (mk_str "CordonBleu") in
         M.alloc α0
-      | combinators_and_then.Food.Steak  =>
+      | combinators_and_then.Food.Steak =>
         let* α0 : ref str.t := M.read (mk_str "Steak") in
         M.alloc α0
-      | combinators_and_then.Food.Sushi  =>
+      | combinators_and_then.Food.Sushi =>
         let* α0 : ref str.t := M.read (mk_str "Sushi") in
         M.alloc α0
       end in
@@ -72,13 +72,13 @@ Section Impl_core_fmt_Debug_for_combinators_and_then_Day_t.
     let* α1 : ref combinators_and_then.Day.t := M.read self in
     let* α2 : M.Val (ref str.t) :=
       match α1 with
-      | combinators_and_then.Day.Monday  =>
+      | combinators_and_then.Day.Monday =>
         let* α0 : ref str.t := M.read (mk_str "Monday") in
         M.alloc α0
-      | combinators_and_then.Day.Tuesday  =>
+      | combinators_and_then.Day.Tuesday =>
         let* α0 : ref str.t := M.read (mk_str "Tuesday") in
         M.alloc α0
-      | combinators_and_then.Day.Wednesday  =>
+      | combinators_and_then.Day.Wednesday =>
         let* α0 : ref str.t := M.read (mk_str "Wednesday") in
         M.alloc α0
       end in
@@ -110,7 +110,7 @@ Definition have_ingredients
   let* α0 : combinators_and_then.Food.t := M.read food in
   let* α1 : M.Val (core.option.Option.t combinators_and_then.Food.t) :=
     match α0 with
-    | combinators_and_then.Food.Sushi  => M.alloc core.option.Option.None
+    | combinators_and_then.Food.Sushi => M.alloc core.option.Option.None
     | _ =>
       let* α0 : combinators_and_then.Food.t := M.read food in
       M.alloc (core.option.Option.Some α0)
@@ -132,7 +132,7 @@ Definition have_recipe
   let* α0 : combinators_and_then.Food.t := M.read food in
   let* α1 : M.Val (core.option.Option.t combinators_and_then.Food.t) :=
     match α0 with
-    | combinators_and_then.Food.CordonBleu  => M.alloc core.option.Option.None
+    | combinators_and_then.Food.CordonBleu => M.alloc core.option.Option.None
     | _ =>
       let* α0 : combinators_and_then.Food.t := M.read food in
       M.alloc (core.option.Option.Some α0)
@@ -159,14 +159,14 @@ Definition cookable_v1
     M.call (combinators_and_then.have_recipe α0) in
   let* α2 : M.Val (core.option.Option.t combinators_and_then.Food.t) :=
     match α1 with
-    | core.option.Option.None  => M.alloc core.option.Option.None
+    | core.option.Option.None => M.alloc core.option.Option.None
     | core.option.Option.Some food =>
       let* food := M.alloc food in
       let* α0 : combinators_and_then.Food.t := M.read food in
       let* α1 : core.option.Option.t combinators_and_then.Food.t :=
         M.call (combinators_and_then.have_ingredients α0) in
       match α1 with
-      | core.option.Option.None  => M.alloc core.option.Option.None
+      | core.option.Option.None => M.alloc core.option.Option.None
       | core.option.Option.Some food =>
         let* food := M.alloc food in
         let* α0 : combinators_and_then.Food.t := M.read food in
@@ -236,7 +236,7 @@ Definition eat
         let* α12 : unit := M.call (std.io.stdio._print α11) in
         M.alloc α12 in
       M.alloc tt
-    | core.option.Option.None  =>
+    | core.option.Option.None =>
       let* _ : M.Val unit :=
         let* α0 : ref str.t :=
           M.read (mk_str "Oh no. We don't get to eat on ") in

CoqOfRust/examples/default/examples/error_handling/combinators_map.v

@@ -25,13 +25,13 @@ Section Impl_core_fmt_Debug_for_combinators_map_Food_t.
     let* α1 : ref combinators_map.Food.t := M.read self in
     let* α2 : M.Val (ref str.t) :=
       match α1 with
-      | combinators_map.Food.Apple  =>
+      | combinators_map.Food.Apple =>
         let* α0 : ref str.t := M.read (mk_str "Apple") in
         M.alloc α0
-      | combinators_map.Food.Carrot  =>
+      | combinators_map.Food.Carrot =>
         let* α0 : ref str.t := M.read (mk_str "Carrot") in
         M.alloc α0
-      | combinators_map.Food.Potato  =>
+      | combinators_map.Food.Potato =>
         let* α0 : ref str.t := M.read (mk_str "Potato") in
         M.alloc α0
       end in
@@ -199,7 +199,7 @@ Definition peel
       let* food := M.alloc food in
       let* α0 : combinators_map.Food.t := M.read food in
       M.alloc (core.option.Option.Some (combinators_map.Peeled.Build_t α0))
-    | core.option.Option.None  => M.alloc core.option.Option.None
+    | core.option.Option.None => M.alloc core.option.Option.None
     end in
   M.read α1.
 
@@ -218,11 +218,11 @@ Definition chop
   let* α0 : core.option.Option.t combinators_map.Peeled.t := M.read peeled in
   let* α1 : M.Val (core.option.Option.t combinators_map.Chopped.t) :=
     match α0 with
-    | core.option.Option.Some combinators_map.Peeled.Build_t food =>
+    | core.option.Option.Some (combinators_map.Peeled.Build_t food) =>
       let* food := M.alloc food in
       let* α0 : combinators_map.Food.t := M.read food in
       M.alloc (core.option.Option.Some (combinators_map.Chopped.Build_t α0))
-    | core.option.Option.None  => M.alloc core.option.Option.None
+    | core.option.Option.None => M.alloc core.option.Option.None
     end in
   M.read α1.
 
@@ -321,7 +321,7 @@ Definition eat
         let* α10 : unit := M.call (std.io.stdio._print α9) in
         M.alloc α10 in
       M.alloc tt
-    | core.option.Option.None  =>
+    | core.option.Option.None =>
       let* _ : M.Val unit :=
         let* α0 : ref str.t := M.read (mk_str "Oh no! It wasn't edible.
 ") in

CoqOfRust/examples/default/examples/error_handling/option_and_unwrap.v

@@ -51,7 +51,7 @@ Definition give_adult (drink : core.option.Option.t (ref str.t)) : M unit :=
         let* α10 : unit := M.call (std.io.stdio._print α9) in
         M.alloc α10 in
       M.alloc tt
-    | core.option.Option.None  =>
+    | core.option.Option.None =>
       let* _ : M.Val unit :=
         let* α0 : ref str.t := M.read (mk_str "No drink? Oh well.
 ") in

CoqOfRust/examples/default/examples/error_handling/unpacking_options_and_defaults_via_get_or_insert.v

@@ -29,19 +29,19 @@ Section Impl_core_fmt_Debug_for_unpacking_options_and_defaults_via_get_or_insert
       M.read self in
     let* α2 : M.Val (ref str.t) :=
       match α1 with
-      | unpacking_options_and_defaults_via_get_or_insert.Fruit.Apple  =>
+      | unpacking_options_and_defaults_via_get_or_insert.Fruit.Apple =>
         let* α0 : ref str.t := M.read (mk_str "Apple") in
         M.alloc α0
-      | unpacking_options_and_defaults_via_get_or_insert.Fruit.Orange  =>
+      | unpacking_options_and_defaults_via_get_or_insert.Fruit.Orange =>
         let* α0 : ref str.t := M.read (mk_str "Orange") in
         M.alloc α0
-      | unpacking_options_and_defaults_via_get_or_insert.Fruit.Banana  =>
+      | unpacking_options_and_defaults_via_get_or_insert.Fruit.Banana =>
         let* α0 : ref str.t := M.read (mk_str "Banana") in
         M.alloc α0
-      | unpacking_options_and_defaults_via_get_or_insert.Fruit.Kiwi  =>
+      | unpacking_options_and_defaults_via_get_or_insert.Fruit.Kiwi =>
         let* α0 : ref str.t := M.read (mk_str "Kiwi") in
         M.alloc α0
-      | unpacking_options_and_defaults_via_get_or_insert.Fruit.Lemon  =>
+      | unpacking_options_and_defaults_via_get_or_insert.Fruit.Lemon =>
         let* α0 : ref str.t := M.read (mk_str "Lemon") in
         M.alloc α0
       end in

CoqOfRust/examples/default/examples/error_handling/unpacking_options_and_defaults_via_get_or_insert_with.v

@@ -30,19 +30,19 @@ Section Impl_core_fmt_Debug_for_unpacking_options_and_defaults_via_get_or_insert
       M.read self in
     let* α2 : M.Val (ref str.t) :=
       match α1 with
-      | unpacking_options_and_defaults_via_get_or_insert_with.Fruit.Apple  =>
+      | unpacking_options_and_defaults_via_get_or_insert_with.Fruit.Apple =>
         let* α0 : ref str.t := M.read (mk_str "Apple") in
         M.alloc α0
-      | unpacking_options_and_defaults_via_get_or_insert_with.Fruit.Orange  =>
+      | unpacking_options_and_defaults_via_get_or_insert_with.Fruit.Orange =>
         let* α0 : ref str.t := M.read (mk_str "Orange") in
         M.alloc α0
-      | unpacking_options_and_defaults_via_get_or_insert_with.Fruit.Banana  =>
+      | unpacking_options_and_defaults_via_get_or_insert_with.Fruit.Banana =>
         let* α0 : ref str.t := M.read (mk_str "Banana") in
         M.alloc α0
-      | unpacking_options_and_defaults_via_get_or_insert_with.Fruit.Kiwi  =>
+      | unpacking_options_and_defaults_via_get_or_insert_with.Fruit.Kiwi =>
         let* α0 : ref str.t := M.read (mk_str "Kiwi") in
         M.alloc α0
-      | unpacking_options_and_defaults_via_get_or_insert_with.Fruit.Lemon  =>
+      | unpacking_options_and_defaults_via_get_or_insert_with.Fruit.Lemon =>
         let* α0 : ref str.t := M.read (mk_str "Lemon") in
         M.alloc α0
       end in

CoqOfRust/examples/default/examples/error_handling/unpacking_options_and_defaults_via_or.v

@@ -28,19 +28,19 @@ Section Impl_core_fmt_Debug_for_unpacking_options_and_defaults_via_or_Fruit_t.
       M.read self in
     let* α2 : M.Val (ref str.t) :=
       match α1 with
-      | unpacking_options_and_defaults_via_or.Fruit.Apple  =>
+      | unpacking_options_and_defaults_via_or.Fruit.Apple =>
         let* α0 : ref str.t := M.read (mk_str "Apple") in
         M.alloc α0
-      | unpacking_options_and_defaults_via_or.Fruit.Orange  =>
+      | unpacking_options_and_defaults_via_or.Fruit.Orange =>
         let* α0 : ref str.t := M.read (mk_str "Orange") in
         M.alloc α0
-      | unpacking_options_and_defaults_via_or.Fruit.Banana  =>
+      | unpacking_options_and_defaults_via_or.Fruit.Banana =>
         let* α0 : ref str.t := M.read (mk_str "Banana") in
         M.alloc α0
-      | unpacking_options_and_defaults_via_or.Fruit.Kiwi  =>
+      | unpacking_options_and_defaults_via_or.Fruit.Kiwi =>
         let* α0 : ref str.t := M.read (mk_str "Kiwi") in
         M.alloc α0
-      | unpacking_options_and_defaults_via_or.Fruit.Lemon  =>
+      | unpacking_options_and_defaults_via_or.Fruit.Lemon =>
         let* α0 : ref str.t := M.read (mk_str "Lemon") in
         M.alloc α0
       end in

CoqOfRust/examples/default/examples/error_handling/unpacking_options_and_defaults_via_or_else.v

@@ -28,19 +28,19 @@ Section Impl_core_fmt_Debug_for_unpacking_options_and_defaults_via_or_else_Fruit
       M.read self in
     let* α2 : M.Val (ref str.t) :=
       match α1 with
-      | unpacking_options_and_defaults_via_or_else.Fruit.Apple  =>
+      | unpacking_options_and_defaults_via_or_else.Fruit.Apple =>
         let* α0 : ref str.t := M.read (mk_str "Apple") in
         M.alloc α0
-      | unpacking_options_and_defaults_via_or_else.Fruit.Orange  =>
+      | unpacking_options_and_defaults_via_or_else.Fruit.Orange =>
         let* α0 : ref str.t := M.read (mk_str "Orange") in
         M.alloc α0
-      | unpacking_options_and_defaults_via_or_else.Fruit.Banana  =>
+      | unpacking_options_and_defaults_via_or_else.Fruit.Banana =>
         let* α0 : ref str.t := M.read (mk_str "Banana") in
         M.alloc α0
-      | unpacking_options_and_defaults_via_or_else.Fruit.Kiwi  =>
+      | unpacking_options_and_defaults_via_or_else.Fruit.Kiwi =>
         let* α0 : ref str.t := M.read (mk_str "Kiwi") in
         M.alloc α0
-      | unpacking_options_and_defaults_via_or_else.Fruit.Lemon  =>
+      | unpacking_options_and_defaults_via_or_else.Fruit.Lemon =>
         let* α0 : ref str.t := M.read (mk_str "Lemon") in
         M.alloc α0
       end in