feat: add a special case for equality on bools

CoqOfRust/blacklist.txt

@@ -1,12 +1,3 @@
-# recently added
-examples/default/examples/custom_types/enums_type_aliases_v2.v
-examples/default/examples/ink_contracts/erc20.v
-examples/default/examples/ink_contracts/lang_err_integration_tests/call_builder.v
-examples/default/examples/ink_contracts/payment_channel.v
-examples/default/examples/ink_contracts/Proofs/erc20.v
-examples/default/examples/ink_contracts/Simulations/erc20.v
-examples/default/examples/ink_contracts/trait_erc20.v
-examples/default/examples/ink_contracts/wildcard_selector.v
 # blacklisting ink smart contracts
 examples/default/examples/ink_contracts/erc1155.v
 examples/default/examples/ink_contracts/erc721.v

CoqOfRust/core/ops.v

@@ -603,6 +603,22 @@ Module control_flow.
     | Break : B -> t B C.
     Arguments Continue {_ _}.
     Arguments Break {_ _}.
+
+    Global Instance Get_Continue_0 {B C : Set} : Notations.Dot "Continue.0" := {
+      Notations.dot :=
+        Ref.map (Big := t B C)
+          (fun α => match α with | Continue α0 => Some α0 | _ => None end)
+          (fun β α =>
+            match α with | Continue _ => Some (Continue β) | _ => None end);
+    }.
+
+    Global Instance Get_Break_0 {B C : Set} : Notations.Dot "Break.0" := {
+      Notations.dot :=
+        Ref.map (Big := t B C)
+          (fun α => match α with | Break α0 => Some α0 | _ => None end)
+          (fun β α =>
+            match α with | Break _ => Some (Break β) | _ => None end);
+    }.
   End ControlFlow.
 End control_flow.
 

CoqOfRust/core/option.v

@@ -44,6 +44,21 @@ Module Option.
   | Some : T -> t T.
   Arguments None {_}.
   Arguments Some {_}.
+
+  Global Instance Get_Some_0 {T : Set} : Notations.Dot "Some.0" := {
+      Notations.dot :=
+        Ref.map (Big := t T)
+          (fun α =>
+            match α with
+            | Some α0 => Datatypes.Some α0
+            | _ => Datatypes.None
+            end)
+          (fun β α =>
+            match α with
+            | Some _ => Datatypes.Some (Some β)
+            | _ => Datatypes.None
+            end);
+    }.
 End Option.
 
 Module Impl_Option. Section Impl_Option.

CoqOfRust/core/result_types.v

@@ -48,4 +48,18 @@ Module Result.
   | Err : E -> t T E.
   Arguments Ok {T E} _.
   Arguments Err {T E} _.
+
+  Global Instance Get_Ok_0 {T E : Set} : Notations.Dot "Ok.0" := {
+    Notations.dot :=
+      Ref.map (Big := t T E)
+        (fun α => match α with Ok α0 => Some α0 | _ => None end)
+        (fun β α => match α with Ok _ => Some (Ok β) | _ => None end);
+  }.
+
+  Global Instance Get_Err_0 {T E : Set} : Notations.Dot "Err.0" := {
+    Notations.dot :=
+      Ref.map (Big := t T E)
+        (fun α => match α with Err α0 => Some α0 | _ => None end)
+        (fun β α => match α with Err _ => Some (Err β) | _ => None end);
+  }.
 End Result.

CoqOfRust/examples/default/examples/conversion/try_from_and_try_into.v

@@ -178,8 +178,8 @@ Definition main : M unit :=
           (let* α0 := M.read γ in
           match α0 with
           | (_, _) =>
-            let γ0 := γ.["(,)left"] in
-            let γ1 := γ.["(,)right"] in
+            let γ0 := Tuple.Access.left γ in
+            let γ1 := Tuple.Access.right γ in
             let* left_val := M.copy γ0 in
             let* right_val := M.copy γ1 in
             let* α0 :
@@ -267,8 +267,8 @@ Definition main : M unit :=
           (let* α0 := M.read γ in
           match α0 with
           | (_, _) =>
-            let γ0 := γ.["(,)left"] in
-            let γ1 := γ.["(,)right"] in
+            let γ0 := Tuple.Access.left γ in
+            let γ1 := Tuple.Access.right γ in
             let* left_val := M.copy γ0 in
             let* right_val := M.copy γ1 in
             let* α0 :
@@ -358,8 +358,8 @@ Definition main : M unit :=
           (let* α0 := M.read γ in
           match α0 with
           | (_, _) =>
-            let γ0 := γ.["(,)left"] in
-            let γ1 := γ.["(,)right"] in
+            let γ0 := Tuple.Access.left γ in
+            let γ1 := Tuple.Access.right γ in
             let* left_val := M.copy γ0 in
             let* right_val := M.copy γ1 in
             let* α0 :
@@ -447,8 +447,8 @@ Definition main : M unit :=
           (let* α0 := M.read γ in
           match α0 with
           | (_, _) =>
-            let γ0 := γ.["(,)left"] in
-            let γ1 := γ.["(,)right"] in
+            let γ0 := Tuple.Access.left γ in
+            let γ1 := Tuple.Access.right γ in
             let* left_val := M.copy γ0 in
             let* right_val := M.copy γ1 in
             let* α0 :

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

@@ -31,7 +31,7 @@ Section Impl_enums_type_aliases_v2_VeryVerboseEnumOfThingsToDoWithNumbers_t.
           fun γ =>
             (let* γ :=
               let* α0 := M.read γ in
-              M.alloc (deref α0) in
+              M.pure (deref α0) in
             let* α0 := M.read γ in
             match α0 with
             |
@@ -47,7 +47,7 @@ Section Impl_enums_type_aliases_v2_VeryVerboseEnumOfThingsToDoWithNumbers_t.
           fun γ =>
             (let* γ :=
               let* α0 := M.read γ in
-              M.alloc (deref α0) in
+              M.pure (deref α0) in
             let* α0 := M.read γ in
             match α0 with
             |

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

@@ -29,7 +29,7 @@ Section Impl_core_fmt_Debug_for_combinators_and_then_Food_t.
           fun γ =>
             (let* γ :=
               let* α0 := M.read γ in
-              M.alloc (deref α0) in
+              M.pure (deref α0) in
             let* α0 := M.read γ in
             match α0 with
             | combinators_and_then.Food.CordonBleu =>
@@ -41,7 +41,7 @@ Section Impl_core_fmt_Debug_for_combinators_and_then_Food_t.
           fun γ =>
             (let* γ :=
               let* α0 := M.read γ in
-              M.alloc (deref α0) in
+              M.pure (deref α0) in
             let* α0 := M.read γ in
             match α0 with
             | combinators_and_then.Food.Steak =>
@@ -53,7 +53,7 @@ Section Impl_core_fmt_Debug_for_combinators_and_then_Food_t.
           fun γ =>
             (let* γ :=
               let* α0 := M.read γ in
-              M.alloc (deref α0) in
+              M.pure (deref α0) in
             let* α0 := M.read γ in
             match α0 with
             | combinators_and_then.Food.Sushi =>
@@ -104,7 +104,7 @@ Section Impl_core_fmt_Debug_for_combinators_and_then_Day_t.
           fun γ =>
             (let* γ :=
               let* α0 := M.read γ in
-              M.alloc (deref α0) in
+              M.pure (deref α0) in
             let* α0 := M.read γ in
             match α0 with
             | combinators_and_then.Day.Monday =>
@@ -116,7 +116,7 @@ Section Impl_core_fmt_Debug_for_combinators_and_then_Day_t.
           fun γ =>
             (let* γ :=
               let* α0 := M.read γ in
-              M.alloc (deref α0) in
+              M.pure (deref α0) in
             let* α0 := M.read γ in
             match α0 with
             | combinators_and_then.Day.Tuesday =>
@@ -128,7 +128,7 @@ Section Impl_core_fmt_Debug_for_combinators_and_then_Day_t.
           fun γ =>
             (let* γ :=
               let* α0 := M.read γ in
-              M.alloc (deref α0) in
+              M.pure (deref α0) in
             let* α0 := M.read γ in
             match α0 with
             | combinators_and_then.Day.Wednesday =>
@@ -418,9 +418,9 @@ Definition main : M unit :=
           (let* α0 := M.read γ in
           match α0 with
           | (_, _, _) =>
-            let γ0 := γ.["(,)left"].["(,)left"] in
-            let γ1 := γ.["(,)left"].["(,)right"] in
-            let γ2 := γ.["(,)right"] in
+            let γ0 := Tuple.Access.left (Tuple.Access.left γ) in
+            let γ1 := Tuple.Access.right (Tuple.Access.left γ) in
+            let γ2 := Tuple.Access.right γ in
             let* cordon_bleu := M.copy γ0 in
             let* steak := M.copy γ1 in
             let* sushi := M.copy γ2 in

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

@@ -29,7 +29,7 @@ Section Impl_core_fmt_Debug_for_combinators_map_Food_t.
           fun γ =>
             (let* γ :=
               let* α0 := M.read γ in
-              M.alloc (deref α0) in
+              M.pure (deref α0) in
             let* α0 := M.read γ in
             match α0 with
             | combinators_map.Food.Apple =>
@@ -41,7 +41,7 @@ Section Impl_core_fmt_Debug_for_combinators_map_Food_t.
           fun γ =>
             (let* γ :=
               let* α0 := M.read γ in
-              M.alloc (deref α0) in
+              M.pure (deref α0) in
             let* α0 := M.read γ in
             match α0 with
             | combinators_map.Food.Carrot =>
@@ -53,7 +53,7 @@ Section Impl_core_fmt_Debug_for_combinators_map_Food_t.
           fun γ =>
             (let* γ :=
               let* α0 := M.read γ in
-              M.alloc (deref α0) in
+              M.pure (deref α0) in
             let* α0 := M.read γ in
             match α0 with
             | combinators_map.Food.Potato =>

CoqOfRust/examples/default/examples/error_handling/iterating_over_results_collect_valid_values_and_failures_via_partition.v

@@ -96,8 +96,8 @@ Definition main : M unit :=
           (let* α0 := M.read γ in
           match α0 with
           | (_, _) =>
-            let γ0 := γ.["(,)left"] in
-            let γ1 := γ.["(,)right"] in
+            let γ0 := Tuple.Access.left γ in
+            let γ1 := Tuple.Access.right γ in
             let* numbers := M.copy γ0 in
             let* errors := M.copy γ1 in
             let* _ : M.Val unit :=

CoqOfRust/examples/default/examples/error_handling/iterating_over_results_collect_valid_values_and_failures_via_partition_unwrapped.v

@@ -98,8 +98,8 @@ Definition main : M unit :=
           (let* α0 := M.read γ in
           match α0 with
           | (_, _) =>
-            let γ0 := γ.["(,)left"] in
-            let γ1 := γ.["(,)right"] in
+            let γ0 := Tuple.Access.left γ in
+            let γ1 := Tuple.Access.right γ in
             let* numbers := M.copy γ0 in
             let* errors := M.copy γ1 in
             let* numbers : M.Val (alloc.vec.Vec.t i32.t alloc.alloc.Global.t) :=

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

@@ -32,7 +32,7 @@ Section Impl_core_fmt_Debug_for_unpacking_options_and_defaults_via_get_or_insert
           fun γ =>
             (let* γ :=
               let* α0 := M.read γ in
-              M.alloc (deref α0) in
+              M.pure (deref α0) in
             let* α0 := M.read γ in
             match α0 with
             | unpacking_options_and_defaults_via_get_or_insert.Fruit.Apple =>
@@ -44,7 +44,7 @@ Section Impl_core_fmt_Debug_for_unpacking_options_and_defaults_via_get_or_insert
           fun γ =>
             (let* γ :=
               let* α0 := M.read γ in
-              M.alloc (deref α0) in
+              M.pure (deref α0) in
             let* α0 := M.read γ in
             match α0 with
             | unpacking_options_and_defaults_via_get_or_insert.Fruit.Orange =>
@@ -56,7 +56,7 @@ Section Impl_core_fmt_Debug_for_unpacking_options_and_defaults_via_get_or_insert
           fun γ =>
             (let* γ :=
               let* α0 := M.read γ in
-              M.alloc (deref α0) in
+              M.pure (deref α0) in
             let* α0 := M.read γ in
             match α0 with
             | unpacking_options_and_defaults_via_get_or_insert.Fruit.Banana =>
@@ -68,7 +68,7 @@ Section Impl_core_fmt_Debug_for_unpacking_options_and_defaults_via_get_or_insert
           fun γ =>
             (let* γ :=
               let* α0 := M.read γ in
-              M.alloc (deref α0) in
+              M.pure (deref α0) in
             let* α0 := M.read γ in
             match α0 with
             | unpacking_options_and_defaults_via_get_or_insert.Fruit.Kiwi =>
@@ -80,7 +80,7 @@ Section Impl_core_fmt_Debug_for_unpacking_options_and_defaults_via_get_or_insert
           fun γ =>
             (let* γ :=
               let* α0 := M.read γ in
-              M.alloc (deref α0) in
+              M.pure (deref α0) in
             let* α0 := M.read γ in
             match α0 with
             | unpacking_options_and_defaults_via_get_or_insert.Fruit.Lemon =>

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

@@ -32,7 +32,7 @@ Section Impl_core_fmt_Debug_for_unpacking_options_and_defaults_via_get_or_insert
           fun γ =>
             (let* γ :=
               let* α0 := M.read γ in
-              M.alloc (deref α0) in
+              M.pure (deref α0) in
             let* α0 := M.read γ in
             match α0 with
             |
@@ -46,7 +46,7 @@ Section Impl_core_fmt_Debug_for_unpacking_options_and_defaults_via_get_or_insert
           fun γ =>
             (let* γ :=
               let* α0 := M.read γ in
-              M.alloc (deref α0) in
+              M.pure (deref α0) in
             let* α0 := M.read γ in
             match α0 with
             |
@@ -60,7 +60,7 @@ Section Impl_core_fmt_Debug_for_unpacking_options_and_defaults_via_get_or_insert
           fun γ =>
             (let* γ :=
               let* α0 := M.read γ in
-              M.alloc (deref α0) in
+              M.pure (deref α0) in
             let* α0 := M.read γ in
             match α0 with
             |
@@ -74,7 +74,7 @@ Section Impl_core_fmt_Debug_for_unpacking_options_and_defaults_via_get_or_insert
           fun γ =>
             (let* γ :=
               let* α0 := M.read γ in
-              M.alloc (deref α0) in
+              M.pure (deref α0) in
             let* α0 := M.read γ in
             match α0 with
             |
@@ -88,7 +88,7 @@ Section Impl_core_fmt_Debug_for_unpacking_options_and_defaults_via_get_or_insert
           fun γ =>
             (let* γ :=
               let* α0 := M.read γ in
-              M.alloc (deref α0) in
+              M.pure (deref α0) in
             let* α0 := M.read γ in
             match α0 with
             |

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

@@ -31,7 +31,7 @@ Section Impl_core_fmt_Debug_for_unpacking_options_and_defaults_via_or_Fruit_t.
           fun γ =>
             (let* γ :=
               let* α0 := M.read γ in
-              M.alloc (deref α0) in
+              M.pure (deref α0) in
             let* α0 := M.read γ in
             match α0 with
             | unpacking_options_and_defaults_via_or.Fruit.Apple =>
@@ -43,7 +43,7 @@ Section Impl_core_fmt_Debug_for_unpacking_options_and_defaults_via_or_Fruit_t.
           fun γ =>
             (let* γ :=
               let* α0 := M.read γ in
-              M.alloc (deref α0) in
+              M.pure (deref α0) in
             let* α0 := M.read γ in
             match α0 with
             | unpacking_options_and_defaults_via_or.Fruit.Orange =>
@@ -55,7 +55,7 @@ Section Impl_core_fmt_Debug_for_unpacking_options_and_defaults_via_or_Fruit_t.
           fun γ =>
             (let* γ :=
               let* α0 := M.read γ in
-              M.alloc (deref α0) in
+              M.pure (deref α0) in
             let* α0 := M.read γ in
             match α0 with
             | unpacking_options_and_defaults_via_or.Fruit.Banana =>
@@ -67,7 +67,7 @@ Section Impl_core_fmt_Debug_for_unpacking_options_and_defaults_via_or_Fruit_t.
           fun γ =>
             (let* γ :=
               let* α0 := M.read γ in
-              M.alloc (deref α0) in
+              M.pure (deref α0) in
             let* α0 := M.read γ in
             match α0 with
             | unpacking_options_and_defaults_via_or.Fruit.Kiwi =>
@@ -79,7 +79,7 @@ Section Impl_core_fmt_Debug_for_unpacking_options_and_defaults_via_or_Fruit_t.
           fun γ =>
             (let* γ :=
               let* α0 := M.read γ in
-              M.alloc (deref α0) in
+              M.pure (deref α0) in
             let* α0 := M.read γ in
             match α0 with
             | unpacking_options_and_defaults_via_or.Fruit.Lemon =>