Update core layout

proof-libs/coq/coq/generated-core/_CoqProject

@@ -47,6 +47,10 @@
 
 ./src/Core_Ops_Range.v
 
+./src/Core_Iter_Traits_Iterator.v
+
+./src/Core_Ops_Index_range.v
+
 ./src/Core_Ops.v
 
 ./src/Core_Base_interface_Coerce.v
@@ -65,26 +69,37 @@
 # Bundles: Core_Primitive.v,
 ./src/Core_Array_Rec_bundle_579704328.v
 
-./src/Core_Primitive.v
+# ./src/Core_Primitive_Number_conversion.v
+# ./src/Core_Primitive_Number_conversion_i.v
 
-# ./src/Core_Num.v # Broken?
+./src/Core_Primitive.v
 
 ./phase_library/NumberNotation.v
 ./phase_library/TODO.v
 
+./src/Core_Intrinsics.v
+
+./src/Core_Num.v # Broken?
+
+./src/Core_Slice_Iter.v
+./src/Core_Slice.v
+
+./src/Core_Array_Iter.v
+./src/Core_Array.v
+
 ./src/Core.v
 
 # # Extra
 
 # Core_Slice_Iter_Macros.v
-# Core_Slice_Iter.v
+# ----- Core_Slice_Iter.v
 # Core_Slice_Index_Private_slice_index.v
 # Core_Slice_Index.v
-# Core_Slice.v
+# ----- Core_Slice.v
 # ----- Core_Result.v
-# Core_Primitive_Number_conversion_i.v
-# Core_Primitive_Number_conversion.v
-# Core_Primitive.v
+# ----- Core_Primitive_Number_conversion_i.v
+# ----- Core_Primitive_Number_conversion.v
+# ----- Core_Primitive.v
 # ----- Core_Panicking.v
 # ----- Core_Option.v
 # ----- Core_Ops_Range.v
@@ -98,7 +113,7 @@
 # ----- Core_Ops.v
 # ----- Core_Num_Uint_macros.v
 # ----- Core_Num_Int_macros.v
-# Core_Num.v
+# ----- Core_Num.v
 # ----- Core_Marker.v
 # Core_Iter_Traits_Marker.v
 # Core_Iter_Traits_Iterator.v
@@ -107,7 +122,7 @@
 # Core_Iter_Traits.v
 # Core_Iter_Range.v
 # Core_Iter.v
-# Core_Intrinsics.v
+# ----- Core_Intrinsics.v
 # Core_Fmt.v
 # ----- Core_Convert.v
 # ----- Core_Cmp.v
@@ -124,7 +139,7 @@
 # Core_Base_interface_Int_I128_proofs.v
 # ----- Core_Base_interface_Int.v
 # ----- Core_Base_interface_Coerce.v
-# Core_Base_interface.v
+# ----- Core_Base_interface.v
 # ----- Core_Base_Z.v
 # ----- Core_Base_Spec_Z.v
 # ----- Core_Base_Spec_Unary.v
@@ -140,7 +155,7 @@
 # Core_Base_Number_conversion.v
 # ----- Core_Base_Binary.v
 # ----- Core_Base.v
-# Core_Array_Rec_bundle_579704328.v
-# Core_Array_Iter.v
-# Core_Array.v
-# Core.v
+# ----- Core_Array_Rec_bundle_579704328.v
+# ----- Core_Array_Iter.v
+# ----- Core_Array.v
+# ----- Core.v

proof-libs/coq/coq/generated-core/phase_library/TODO.v

@@ -33,3 +33,11 @@ Definition assert (b : bool) (* `{H_assert : b = true} *) : unit := tt.
 (* Definition impl_1__push {A} l (x : A) := cons l x. *)
 (* Definition impl__to_vec {T} (x : t_Slice T) : t_Vec T t_Global := {| x |}. *)
 (* Definition from_elem {A} (x : A) (l : Z) := repeat x (Z.to_nat l). *)
+
+Fixpoint build_range (l : nat) (f : nat) (a : list t_usize) : list t_usize :=
+  match f with
+  | 0%nat => a
+  | (S n)%nat => build_range (S l) n (cons a (Build_t_usize (Build_t_U64 (unary_to_int l))))
+  end.
+
+Definition fold_range {A : Type} (l : t_usize) (u : t_usize) (_ : A -> t_usize -> bool) (x : A) (f : A -> t_usize -> A) : A := List.fold_left f (build_range (unary_from_int (U64_f_v (usize_0 l))) (unary_from_int (U64_f_v (usize_0 (Sub_f_sub u l)))) nil) x.

proof-libs/coq/coq/generated-core/src/Core.v

@@ -64,6 +64,15 @@ Export Core_Primitive.
 From Core Require Import Core_Option.
 Export Core_Option.
 
+From Core Require Import Core_Array_Rec_bundle_579704328.
+Export Core_Array_Rec_bundle_579704328.
+
+From Core Require Import Core_Ops.
+Export Core_Ops.
+
+From Core Require Import Core_Ops_Index.
+Export Core_Ops_Index.
+
 From Core Require Import NumberNotation.
 Export NumberNotation.
 

proof-libs/coq/coq/generated-core/src/Core_Array.v

@@ -12,75 +12,26 @@ Import RecordSetNotations.
 
 (* From Core Require Import Core. *)
 
-(* TODO: Replace this dummy lib with core lib *)
-Class t_Sized (T : Type) := { }.
-Definition t_u8 := Z.
-Definition t_u16 := Z.
-Definition t_u32 := Z.
-Definition t_u64 := Z.
-Definition t_u128 := Z.
-Definition t_usize := Z.
-Definition t_i8 := Z.
-Definition t_i16 := Z.
-Definition t_i32 := Z.
-Definition t_i64 := Z.
-Definition t_i128 := Z.
-Definition t_isize := Z.
-Definition t_Array T (x : t_usize) := list T.
-Definition t_String := string.
-Definition ToString_f_to_string (x : string) := x.
-Instance Sized_any : forall {t_A}, t_Sized t_A := {}.
-Class t_Clone (T : Type) := { Clone_f_clone : T -> T }.
-Instance Clone_any : forall {t_A}, t_Clone t_A := {Clone_f_clone := fun x => x}.
-Definition t_Slice (T : Type) := list T.
-Definition unsize {T : Type} : list T -> t_Slice T := id.
-Definition t_PartialEq_f_eq x y := x =? y.
-Definition t_Rem_f_rem (x y : Z) := x mod y.
-Definition assert (b : bool) (* `{H_assert : b = true} *) : unit := tt.
-Inductive globality := | t_Global.
-Definition t_Vec T (_ : globality) : Type := list T.
-Definition impl_1__append {T} l1 l2 : list T * list T := (app l1 l2, l2).
-Definition impl_1__len {A} (l : list A) := Z.of_nat (List.length l).
-Definition impl__new {A} (_ : Datatypes.unit) : list A := nil.
-Definition impl__with_capacity {A} (_ : Z)  : list A := nil.
-Definition impl_1__push {A} l (x : A) := cons x l.
-Class t_From (A B : Type) := { From_f_from : B -> A }.
-Definition impl__to_vec {T} (x : t_Slice T) : t_Vec T t_Global := x.
-Class t_Into (A B : Type) := { Into_f_into : A -> B }.
-Instance t_Into_from_t_From {A B : Type} `{H : t_From B A} : t_Into A B := { Into_f_into x := @From_f_from B A H x }.
-Definition from_elem {A} (x : A) (l : Z) := repeat x (Z.to_nat l).
-Definition t_Option := option.
-Definition impl__map {A B} (x : t_Option A) (f : A -> B) : t_Option B := match x with | Some x => Some (f x) | None => None end.
-Definition t_Add_f_add x y := x + y.
-Class Cast A B := { cast : A -> B }.
-Instance cast_t_u8_t_u32 : Cast t_u8 t_u32 := {| cast x := x |}.
-(* / dummy lib *)
+From Core Require Import Core_Ops_Index.
+Export Core_Ops_Index.
 
+(* From Core Require Import Core_Ops_IndexMut. *)
+(* Export Core_Ops (t_IndexMut). *)
 
+From Core Require Import Core_Primitive.
+Export Core_Primitive.
 
-From Core Require Import Core_Ops (t_Index).
-Export Core_Ops (t_Index).
-
-From Core Require Import Core_Ops (t_IndexMut).
-Export Core_Ops (t_IndexMut).
-
-From Core Require Import Core_Primitive (t_Slice).
-Export Core_Primitive (t_Slice).
-
-From Core Require Import Core_Primitive (t_Array).
-Export Core_Primitive (t_Array).
-
-From Core Require Import Self_Iter (t_IntoIter).
-Export Self_Iter (t_IntoIter).
+From Core Require Import Core_Array_Iter.
+Export Core_Array_Iter.
 
 Notation "'t_TryFromSliceError'" := (t_TryFromSliceError).
 
 Notation "'TryFromSliceError_0'" := (TryFromSliceError_0).
 
 (* NotImplementedYet *)
 
-Notation "'impl_2'" := (impl_2).
+(* Notation "'impl_2'" := (impl_2). *)
 
-Notation "'impl_1'" := (impl_1).
+(* Notation "'impl_1'" := (impl_1). *)
 
-Notation "'impl'" := (impl).
+(* Notation "'impl'" := (impl). *)

proof-libs/coq/coq/generated-core/src/Core_Array_Iter.v

@@ -12,75 +12,31 @@ Import RecordSetNotations.
 
 (* From Core Require Import Core. *)
 
-(* TODO: Replace this dummy lib with core lib *)
-Class t_Sized (T : Type) := { }.
-Definition t_u8 := Z.
-Definition t_u16 := Z.
-Definition t_u32 := Z.
-Definition t_u64 := Z.
-Definition t_u128 := Z.
-Definition t_usize := Z.
-Definition t_i8 := Z.
-Definition t_i16 := Z.
-Definition t_i32 := Z.
-Definition t_i64 := Z.
-Definition t_i128 := Z.
-Definition t_isize := Z.
-Definition t_Array T (x : t_usize) := list T.
-Definition t_String := string.
-Definition ToString_f_to_string (x : string) := x.
-Instance Sized_any : forall {t_A}, t_Sized t_A := {}.
-Class t_Clone (T : Type) := { Clone_f_clone : T -> T }.
-Instance Clone_any : forall {t_A}, t_Clone t_A := {Clone_f_clone := fun x => x}.
-Definition t_Slice (T : Type) := list T.
-Definition unsize {T : Type} : list T -> t_Slice T := id.
-Definition t_PartialEq_f_eq x y := x =? y.
-Definition t_Rem_f_rem (x y : Z) := x mod y.
-Definition assert (b : bool) (* `{H_assert : b = true} *) : unit := tt.
-Inductive globality := | t_Global.
-Definition t_Vec T (_ : globality) : Type := list T.
-Definition impl_1__append {T} l1 l2 : list T * list T := (app l1 l2, l2).
-Definition impl_1__len {A} (l : list A) := Z.of_nat (List.length l).
-Definition impl__new {A} (_ : Datatypes.unit) : list A := nil.
-Definition impl__with_capacity {A} (_ : Z)  : list A := nil.
-Definition impl_1__push {A} l (x : A) := cons x l.
-Class t_From (A B : Type) := { From_f_from : B -> A }.
-Definition impl__to_vec {T} (x : t_Slice T) : t_Vec T t_Global := x.
-Class t_Into (A B : Type) := { Into_f_into : A -> B }.
-Instance t_Into_from_t_From {A B : Type} `{H : t_From B A} : t_Into A B := { Into_f_into x := @From_f_from B A H x }.
-Definition from_elem {A} (x : A) (l : Z) := repeat x (Z.to_nat l).
-Definition t_Option := option.
-Definition impl__map {A B} (x : t_Option A) (f : A -> B) : t_Option B := match x with | Some x => Some (f x) | None => None end.
-Definition t_Add_f_add x y := x + y.
-Class Cast A B := { cast : A -> B }.
-Instance cast_t_u8_t_u32 : Cast t_u8 t_u32 := {| cast x := x |}.
-(* / dummy lib *)
+From Core Require Import Core_Num.
+Export Core_Num.
 
-From Core Require Import Core_Num (t_NonZero).
-Export Core_Num (t_NonZero).
 
 
+From Core Require Import Core_Ops_Index_range.
+Export Core_Ops_Index_range.
 
-From Core Require Import Core_Ops (t_IndexRange).
-Export Core_Ops (t_IndexRange).
+From Core Require Import Core_Ops_Range.
+Export Core_Ops_Range.
 
-From Core Require Import Core_Ops (t_Range).
-Export Core_Ops (t_Range).
+From Core Require Import Core_Primitive.
+Export Core_Primitive.
 
-From Core Require Import Core_Primitive (t_Array).
-Export Core_Primitive (t_Array).
+(* From Core Require Import Core_Iter (t_IntoIterator). *)
+(* Export Core_Iter (t_IntoIterator). *)
 
-From Core Require Import Core_Iter (t_IntoIterator).
-Export Core_Iter (t_IntoIterator).
+From Core Require Import Core_Clone.
+Export Core_Clone.
 
-From Core Require Import Core (t_clone).
-Export Core (t_clone).
+From Core Require Import Core_Base.
+Export Core_Base.
 
-From Core Require Import Core (t_base).
-Export Core (t_base).
-
-From Core Require Import hax_lib.
-Export hax_lib.
+(* From Core Require Import hax_lib. *)
+(* Export hax_lib. *)
 
 Record t_IntoIter (v_T : Type) (v_N : t_usize) `{t_Sized (v_T)} : Type :=
   {