Merge pull request #659 from formal-land/guillaume-claret@generate-mo…

…re-links-types

Add more automation for the generation of link types

CoqOfRust/M.v

@@ -412,6 +412,12 @@ Parameter IsProvidedMethod :
     (method : Ty.t -> PolymorphicFunction.t),
   Prop.
 
+Parameter IsDiscriminant :
+  forall
+    (variant_name : string)
+    (discriminant : Z),
+  Prop.
+
 Module IsTraitMethod.
   Inductive t
       (trait_name : string)
@@ -758,13 +764,17 @@ Module SubPointer.
   Parameter get_slice_rest : Value.t -> Z -> Z -> M.
 End SubPointer.
 
+(** Explicit definition to simplify the links later *)
+Definition if_then_else_bool (condition : Value.t) (then_ else_ : M) : M :=
+  match condition with
+  | Value.Bool true => then_
+  | Value.Bool false => else_
+  | _ => impossible "if_then_else_bool: expected a boolean"
+  end.
+
 Definition is_constant_or_break_match (value expected_value : Value.t) : M :=
   let* are_equal := are_equal value expected_value in
-  match are_equal with
-  | Value.Bool true => pure (Value.Tuple [])
-  | Value.Bool false => break_match
-  | _ => impossible "expected a boolean"
-  end.
+  if_then_else_bool are_equal (pure (Value.Tuple [])) break_match.
 
 Definition is_struct_tuple (value : Value.t) (constructor : string) : M :=
   let* value := read value in

CoqOfRust/alloc/borrow.v

@@ -166,17 +166,18 @@ Module borrow.
         {
           name := "Borrowed";
           item := StructTuple [ Ty.apply (Ty.path "&") [] [ B ] ];
-          discriminant := None;
         };
         {
           name := "Owned";
           item := StructTuple [ Ty.associated ];
-          discriminant := None;
         }
       ];
   }
   *)
 
+  Axiom IsDiscriminant_Cow_Borrowed : M.IsDiscriminant "alloc::borrow::Cow::Borrowed" 0.
+  Axiom IsDiscriminant_Cow_Owned : M.IsDiscriminant "alloc::borrow::Cow::Owned" 1.
+
   Module Impl_core_clone_Clone_where_core_marker_Sized_B_where_alloc_borrow_ToOwned_B_for_alloc_borrow_Cow_B.
     Definition Self (B : Ty.t) : Ty.t := Ty.apply (Ty.path "alloc::borrow::Cow") [] [ B ].
 

CoqOfRust/alloc/collections/btree/map/entry.v

@@ -22,7 +22,6 @@ Module collections.
                         []
                         [ K; V; A ]
                     ];
-                discriminant := None;
               };
               {
                 name := "Occupied";
@@ -34,12 +33,16 @@ Module collections.
                         []
                         [ K; V; A ]
                     ];
-                discriminant := None;
               }
             ];
         }
         *)
 
+        Axiom IsDiscriminant_Entry_Vacant :
+          M.IsDiscriminant "alloc::collections::btree::map::entry::Entry::Vacant" 0.
+        Axiom IsDiscriminant_Entry_Occupied :
+          M.IsDiscriminant "alloc::collections::btree::map::entry::Entry::Occupied" 1.
+
         Module Impl_core_fmt_Debug_where_core_fmt_Debug_K_where_core_cmp_Ord_K_where_core_fmt_Debug_V_where_core_alloc_Allocator_A_where_core_clone_Clone_A_for_alloc_collections_btree_map_entry_Entry_K_V_A.
           Definition Self (K V A : Ty.t) : Ty.t :=
             Ty.apply (Ty.path "alloc::collections::btree::map::entry::Entry") [] [ K; V; A ].

CoqOfRust/alloc/collections/btree/merge_iter.v

@@ -31,17 +31,20 @@ Module collections.
             {
               name := "A";
               item := StructTuple [ Ty.associated ];
-              discriminant := None;
             };
             {
               name := "B";
               item := StructTuple [ Ty.associated ];
-              discriminant := None;
             }
           ];
       }
       *)
 
+      Axiom IsDiscriminant_Peeked_A :
+        M.IsDiscriminant "alloc::collections::btree::merge_iter::Peeked::A" 0.
+      Axiom IsDiscriminant_Peeked_B :
+        M.IsDiscriminant "alloc::collections::btree::merge_iter::Peeked::B" 1.
+
       Module Impl_core_clone_Clone_where_core_clone_Clone_I_where_core_iter_traits_iterator_Iterator_I_where_core_clone_Clone_associated_type_where_core_clone_Clone_associated_type_for_alloc_collections_btree_merge_iter_Peeked_I.
         Definition Self (I : Ty.t) : Ty.t :=
           Ty.apply (Ty.path "alloc::collections::btree::merge_iter::Peeked") [] [ I ].

CoqOfRust/alloc/collections/btree/navigate.v

@@ -2725,7 +2725,6 @@ Module collections.
                         Ty.path "alloc::collections::btree::node::marker::LeafOrInternal"
                       ]
                   ];
-              discriminant := None;
             };
             {
               name := "Edge";
@@ -2748,12 +2747,16 @@ Module collections.
                         Ty.path "alloc::collections::btree::node::marker::Edge"
                       ]
                   ];
-              discriminant := None;
             }
           ];
       }
       *)
 
+      Axiom IsDiscriminant_LazyLeafHandle_Root :
+        M.IsDiscriminant "alloc::collections::btree::navigate::LazyLeafHandle::Root" 0.
+      Axiom IsDiscriminant_LazyLeafHandle_Edge :
+        M.IsDiscriminant "alloc::collections::btree::navigate::LazyLeafHandle::Edge" 1.
+
       Module Impl_core_clone_Clone_for_alloc_collections_btree_navigate_LazyLeafHandle_alloc_collections_btree_node_marker_Immut_K_V.
         Definition Self (K V : Ty.t) : Ty.t :=
           Ty.apply
@@ -13661,7 +13664,6 @@ Module collections.
                       []
                       [ BorrowType; K; V; Ty.path "alloc::collections::btree::node::marker::Leaf" ]
                   ];
-              discriminant := None;
             };
             {
               name := "Internal";
@@ -13678,17 +13680,22 @@ Module collections.
                         Ty.path "alloc::collections::btree::node::marker::Internal"
                       ]
                   ];
-              discriminant := None;
             };
             {
               name := "InternalKV";
               item := StructTuple [];
-              discriminant := None;
             }
           ];
       }
       *)
 
+      Axiom IsDiscriminant_Position_Leaf :
+        M.IsDiscriminant "alloc::collections::btree::navigate::Position::Leaf" 0.
+      Axiom IsDiscriminant_Position_Internal :
+        M.IsDiscriminant "alloc::collections::btree::navigate::Position::Internal" 1.
+      Axiom IsDiscriminant_Position_InternalKV :
+        M.IsDiscriminant "alloc::collections::btree::navigate::Position::InternalKV" 2.
+
 
       Module Impl_alloc_collections_btree_node_Handle_alloc_collections_btree_node_NodeRef_BorrowType_K_V_alloc_collections_btree_node_marker_LeafOrInternal_alloc_collections_btree_node_marker_KV.
         Definition Self (BorrowType K V : Ty.t) : Ty.t :=

CoqOfRust/alloc/collections/btree/node.v

@@ -9207,17 +9207,20 @@ Module collections.
             {
               name := "Left";
               item := StructTuple [ T ];
-              discriminant := None;
             };
             {
               name := "Right";
               item := StructTuple [ T ];
-              discriminant := None;
             }
           ];
       }
       *)
 
+      Axiom IsDiscriminant_LeftOrRight_Left :
+        M.IsDiscriminant "alloc::collections::btree::node::LeftOrRight::Left" 0.
+      Axiom IsDiscriminant_LeftOrRight_Right :
+        M.IsDiscriminant "alloc::collections::btree::node::LeftOrRight::Right" 1.
+
       (*
       fn splitpoint(edge_idx: usize) -> (usize, LeftOrRight<usize>) {
           debug_assert!(edge_idx <= CAPACITY);
@@ -24233,17 +24236,20 @@ Module collections.
             {
               name := "Leaf";
               item := StructTuple [ Leaf ];
-              discriminant := None;
             };
             {
               name := "Internal";
               item := StructTuple [ Internal ];
-              discriminant := None;
             }
           ];
       }
       *)
 
+      Axiom IsDiscriminant_ForceResult_Leaf :
+        M.IsDiscriminant "alloc::collections::btree::node::ForceResult::Leaf" 0.
+      Axiom IsDiscriminant_ForceResult_Internal :
+        M.IsDiscriminant "alloc::collections::btree::node::ForceResult::Internal" 1.
+
       (* StructRecord
         {
           name := "SplitResult";
@@ -24503,6 +24509,7 @@ Module collections.
         }
         *)
 
+
         (*
         Enum Internal
         {
@@ -24512,6 +24519,7 @@ Module collections.
         }
         *)
 
+
         (*
         Enum LeafOrInternal
         {
@@ -24521,6 +24529,7 @@ Module collections.
         }
         *)
 
+
         (*
         Enum Owned
         {
@@ -24530,6 +24539,7 @@ Module collections.
         }
         *)
 
+
         (*
         Enum Dying
         {
@@ -24539,6 +24549,7 @@ Module collections.
         }
         *)
 
+
         (*
         Enum DormantMut
         {
@@ -24548,6 +24559,7 @@ Module collections.
         }
         *)
 
+
         (* StructTuple
           {
             name := "Immut";
@@ -24674,6 +24686,7 @@ Module collections.
         }
         *)
 
+
         (*
         Enum Edge
         {
@@ -24682,6 +24695,7 @@ Module collections.
           variants := [];
         }
         *)
+
       End marker.
 
       (*

CoqOfRust/alloc/collections/btree/search.v

@@ -14,27 +14,32 @@ Module collections.
             {
               name := "Included";
               item := StructTuple [ T ];
-              discriminant := None;
             };
             {
               name := "Excluded";
               item := StructTuple [ T ];
-              discriminant := None;
             };
             {
               name := "AllIncluded";
               item := StructTuple [];
-              discriminant := None;
             };
             {
               name := "AllExcluded";
               item := StructTuple [];
-              discriminant := None;
             }
           ];
       }
       *)
 
+      Axiom IsDiscriminant_SearchBound_Included :
+        M.IsDiscriminant "alloc::collections::btree::search::SearchBound::Included" 0.
+      Axiom IsDiscriminant_SearchBound_Excluded :
+        M.IsDiscriminant "alloc::collections::btree::search::SearchBound::Excluded" 1.
+      Axiom IsDiscriminant_SearchBound_AllIncluded :
+        M.IsDiscriminant "alloc::collections::btree::search::SearchBound::AllIncluded" 2.
+      Axiom IsDiscriminant_SearchBound_AllExcluded :
+        M.IsDiscriminant "alloc::collections::btree::search::SearchBound::AllExcluded" 3.
+
       Module Impl_alloc_collections_btree_search_SearchBound_T.
         Definition Self (T : Ty.t) : Ty.t :=
           Ty.apply (Ty.path "alloc::collections::btree::search::SearchBound") [] [ T ].
@@ -134,7 +139,6 @@ Module collections.
                         Ty.path "alloc::collections::btree::node::marker::KV"
                       ]
                   ];
-              discriminant := None;
             };
             {
               name := "GoDown";
@@ -152,12 +156,16 @@ Module collections.
                         Ty.path "alloc::collections::btree::node::marker::Edge"
                       ]
                   ];
-              discriminant := None;
             }
           ];
       }
       *)
 
+      Axiom IsDiscriminant_SearchResult_Found :
+        M.IsDiscriminant "alloc::collections::btree::search::SearchResult::Found" 0.
+      Axiom IsDiscriminant_SearchResult_GoDown :
+        M.IsDiscriminant "alloc::collections::btree::search::SearchResult::GoDown" 1.
+
       (*
       Enum IndexResult
       {
@@ -168,17 +176,20 @@ Module collections.
             {
               name := "KV";
               item := StructTuple [ Ty.path "usize" ];
-              discriminant := None;
             };
             {
               name := "Edge";
               item := StructTuple [ Ty.path "usize" ];
-              discriminant := None;
             }
           ];
       }
       *)
 
+      Axiom IsDiscriminant_IndexResult_KV :
+        M.IsDiscriminant "alloc::collections::btree::search::IndexResult::KV" 0.
+      Axiom IsDiscriminant_IndexResult_Edge :
+        M.IsDiscriminant "alloc::collections::btree::search::IndexResult::Edge" 1.
+
       Module Impl_alloc_collections_btree_node_NodeRef_BorrowType_K_V_alloc_collections_btree_node_marker_LeafOrInternal.
         Definition Self (BorrowType K V : Ty.t) : Ty.t :=
           Ty.apply