Freshly generated core code

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

@@ -0,0 +1,55 @@
+(* File automatically generated by Hacspec *)
+From Hacspec Require Import Hacspec_Lib MachineIntegers.
+From Coq Require Import ZArith.
+Import List.ListNotations.
+Open Scope Z_scope.
+Open Scope bool_scope.
+
+Require Import Primitive.
+Export Primitive.
+
+(*Not implemented yet? todo(item)*)
+
+(*Not implemented yet? todo(item)*)
+
+(*Not implemented yet? todo(item)*)
+
+(*Not implemented yet? todo(item)*)
+
+(*Not implemented yet? todo(item)*)
+
+(*Not implemented yet? todo(item)*)
+
+(*Not implemented yet? todo(item)*)
+
+(*Not implemented yet? todo(item)*)
+
+(*Not implemented yet? todo(item)*)
+
+(*Not implemented yet? todo(item)*)
+
+(*Not implemented yet? todo(item)*)
+
+(*Not implemented yet? todo(item)*)
+
+(*Not implemented yet? todo(item)*)
+
+(*Not implemented yet? todo(item)*)
+
+(*Not implemented yet? todo(item)*)
+
+(*Not implemented yet? todo(item)*)
+
+(*Not implemented yet? todo(item)*)
+
+(*Not implemented yet? todo(item)*)
+
+(*Not implemented yet? todo(item)*)
+
+(*Not implemented yet? todo(item)*)
+
+(*Not implemented yet? todo(item)*)
+
+(*Not implemented yet? todo(item)*)
+
+(*Not implemented yet? todo(item)*)

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

@@ -1,72 +1,33 @@
 (* File automatically generated by Hacspec *)
+From Hacspec Require Import Hacspec_Lib MachineIntegers.
 From Coq Require Import ZArith.
 Import List.ListNotations.
 Open Scope Z_scope.
 Open Scope bool_scope.
-Require Import String.
 
+Require Import Index.
+Export Index.
 
-From Core Require Import Core_Coerce (t_Abstraction).
-Export Core_Coerce (t_Abstraction).
+Require Import IndexMut.
+Export IndexMut.
 
-From Core Require Import Core_Coerce (t_Concretization).
-Export Core_Coerce (t_Concretization).
+Require Import Slice.
+Export Slice.
 
+Require Import Array.
+Export Array.
 
-From Core Require Import Core_Base_Int_Number_conversion.
-Export Core_Base_Int_Number_conversion.
+Require Import IntoIter.
+Export IntoIter.
 
-From Core Require Import Core_Base_Seq.
-Export Core_Base_Seq.
+(*Not implemented yet? todo(item)*)
 
-From Core Require Import Core_Int.
-Export Core_Int.
+Record t_TryFromSliceError : Type := {
+  0 : unit;
+}.
 
+(*item error backend*)
 
-From Core Require Import Core_Cmp.
-Export Core_Cmp.
+(*item error backend*)
 
-From Core Require Import Core_Clone.
-Export Core_Clone.
-
-
-From Core Require Import Core_Primitive.
-Export Core_Primitive.
-
-Instance t_Clone_427868774 `{v_T : Type} `{v_N : t_usize} `{t_Sized v_T} `{t_Clone v_T} : t_Clone (t_Array (v_T) (v_N)) :=
-  {
-    t_Clone_f_clone := fun (self : t_Array (v_T) (v_N)) =>
-      Build_t_Array (t_Clone_f_clone (t_Array_f_v self));
-  }.
-
-Instance t_PartialEq_670168337 `{v_T : Type} `{v_N : t_usize} `{t_Sized v_T} `{t_Clone v_T} `{t_PartialEq v_T v_T} : t_PartialEq (t_Array (v_T) (v_N)) (t_Array (v_T) (v_N)) :=
-  {
-    t_PartialEq_f_eq := fun (self : t_Array (v_T) (v_N)) (other : t_Array (v_T) (v_N)) =>
-      t_PartialEq_f_eq (t_Clone_f_clone (t_Array_f_v self)) (t_Array_f_v other);
-    t_PartialEq_f_ne := fun (self : t_Array (v_T) (v_N)) (other : t_Array (v_T) (v_N)) =>
-      negb (t_PartialEq_f_eq (t_Clone_f_clone (t_Array_f_v self)) (t_Array_f_v other));
-  }.
-
-Definition impl_2__reverse `{v_T : Type} `{v_N : t_usize} `{t_Sized v_T} `{t_Clone v_T} (self : t_Array (v_T) (v_N)) : t_Array (v_T) (v_N) :=
-  Build_t_Array (impl_2__rev (t_Array_f_v self)).
-
-Lemma lt_usize_implies_hax_int (x : t_usize) (y : t_usize) :
-  t_PartialOrd_f_lt (x) (y) = true ->
-  t_PartialOrd_f_lt (t_From_f_from (x)) (t_From_f_from (y)) = true.
-Proof. Admitted.
-
-Lemma lift_usize_equality (x : t_HaxInt) (y : t_usize) :
-  t_PartialEq_f_eq (x) (t_From_f_from  y) = true ->
-  t_PartialEq_f_eq (t_From_f_from (x)) (y) = true.
-Proof. Admitted.
-
-Program Definition impl_2__index `{v_T : Type} `{v_N : t_usize} `{t_Sized v_T} `{t_Clone v_T} (self : t_Array (v_T) (v_N)) (i : t_usize) `{andb (t_PartialEq_f_eq (impl_2__len (t_Array_f_v self)) (t_From_f_from (v_N))) (t_PartialOrd_f_lt (i) (v_N)) = true} : v_T :=
-    impl_2__get_index (H1 := _) (t_Array_f_v self) (t_From_f_from (i)).
-Admit Obligations.
-
-Definition impl_2__new `{v_T : Type} `{v_N : t_usize} `{t_Sized v_T} `{t_Clone v_T} (x : v_T) : t_Array (v_T) (v_N) :=
-  Build_t_Array (impl_2__repeat (t_From_f_from (v_N)) (x)).
-
-Program Definition impl_2__set_index `{v_T : Type} `{v_N : t_usize} `{t_Sized v_T} `{t_Clone v_T} (self : t_Array (v_T) (v_N)) (i : t_usize) (t : v_T) `{andb (t_PartialEq_f_eq (impl_2__len (t_Array_f_v self)) (t_From_f_from (v_N))) (t_PartialOrd_f_lt (i) (v_N)) = true} : t_Array (v_T) (v_N) :=
-  Build_t_Array (impl_2__set_index (H1 := _) (t_Array_f_v self) (t_From_f_from (i)) (t)).
-Admit Obligations.
+(*item error backend*)

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

@@ -0,0 +1,32 @@
+(* File automatically generated by Hacspec *)
+From Hacspec Require Import Hacspec_Lib MachineIntegers.
+From Coq Require Import ZArith.
+Import List.ListNotations.
+Open Scope Z_scope.
+Open Scope bool_scope.
+
+Require Import NonZero.
+Export NonZero.
+
+Require Import IndexRange.
+Export IndexRange.
+
+Require Import Range.
+Export Range.
+
+Require Import Array.
+Export Array.
+
+Require Import IntoIterator.
+Export IntoIterator.
+
+Require Import Core_Clone.
+Export Core_Clone.
+
+Require Import Crate_Base.
+Export Crate_Base.
+
+Require Import Hax_lib.
+Export Hax_lib.
+
+(*item error backend*)

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

@@ -0,0 +1,36 @@
+(* File automatically generated by Hacspec *)
+From Hacspec Require Import Hacspec_Lib MachineIntegers.
+From Coq Require Import ZArith.
+Import List.ListNotations.
+Open Scope Z_scope.
+Open Scope bool_scope.
+
+Require Import Spec.
+Export Spec.
+
+Require Import Binary.
+Export Binary.
+
+Require Import Pos.
+Export Pos.
+
+Require Import Z.
+Export Z.
+
+Require Import Number_conversion.
+Export Number_conversion.
+
+Require Import Seq.
+Export Seq.
+
+(*Not implemented yet? todo(item)*)
+
+(*Not implemented yet? todo(item)*)
+
+(*Not implemented yet? todo(item)*)
+
+(*Not implemented yet? todo(item)*)
+
+(*Not implemented yet? todo(item)*)
+
+(*Not implemented yet? todo(item)*)

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

@@ -0,0 +1,147 @@
+(* File automatically generated by Hacspec *)
+From Hacspec Require Import Hacspec_Lib MachineIntegers.
+From Coq Require Import ZArith.
+Import List.ListNotations.
+Open Scope Z_scope.
+Open Scope bool_scope.
+
+Require Import Super_Spec.
+Export Super_Spec.
+
+Require Import Ordering.
+Export Ordering.
+
+Definition positive_cmp__cmp_binary_cont (x : t_Positive_t) (y : t_Positive_t) (r : t_Ordering_t) : t_Ordering_t :=
+  match match_positive x with
+  | POSITIVE_XH  =>
+    match match_positive y with
+    | POSITIVE_XH  =>
+      r
+    | POSITIVE_XO q | POSITIVE_XI q =>
+      Ordering_Lesst_Ordering_t
+    end
+  | POSITIVE_XO p =>
+    match match_positive y with
+    | POSITIVE_XH  =>
+      Ordering_Greatert_Ordering_t
+    | POSITIVE_XO q =>
+      positive_cmp__cmp_binary_cont p q r
+    | POSITIVE_XI q =>
+      positive_cmp__cmp_binary_cont p q Ordering_Lesst_Ordering_t
+    end
+  | POSITIVE_XI p =>
+    match match_positive y with
+    | POSITIVE_XH  =>
+      Ordering_Greatert_Ordering_t
+    | POSITIVE_XO q =>
+      positive_cmp__cmp_binary_cont p q Ordering_Greatert_Ordering_t
+    | POSITIVE_XI q =>
+      positive_cmp__cmp_binary_cont p q r
+    end
+  end.
+
+Definition positive_cmp (lhs : t_Positive_t) (rhs : t_Positive_t) : t_Ordering_t :=
+  positive_cmp__cmp_binary_cont lhs rhs Ordering_Equalt_Ordering_t.
+
+Definition positive_le (lhs : t_Positive_t) (rhs : t_Positive_t) : bool :=
+  match Option_Some (positive_cmp lhs rhs) with
+  | Option_Some Ordering_Less  | Ordering_Equal  =>
+    true
+  | _ =>
+    false
+  end.
+
+Definition positive_pred_double (s : t_Positive_t) : t_Positive_t :=
+  match match_positive s with
+  | POSITIVE_XH  =>
+    xH
+  | POSITIVE_XO p =>
+    xI (positive_pred_double p)
+  | POSITIVE_XI p =>
+    xI (xO p)
+  end.
+
+Definition positive_succ (s : t_Positive_t) : t_Positive_t :=
+  match match_positive s with
+  | POSITIVE_XH  =>
+    xO xH
+  | POSITIVE_XO q =>
+    xI q
+  | POSITIVE_XI q =>
+    xO (positive_succ q)
+  end.
+
+Definition positive_add (lhs : t_Positive_t) (rhs : t_Positive_t) : t_Positive_t :=
+  positive_add__add lhs rhs.
+
+Definition positive_mul (lhs : t_Positive_t) (rhs : t_Positive_t) : t_Positive_t :=
+  match match_positive lhs with
+  | POSITIVE_XH  =>
+    rhs
+  | POSITIVE_XO p =>
+    xO (positive_mul p rhs)
+  | POSITIVE_XI p =>
+    positive_add (f_clone rhs) (xO (positive_mul p rhs))
+  end.
+
+Definition positive_add__add (lhs : t_Positive_t) (rhs : t_Positive_t) : t_Positive_t :=
+  match match_positive lhs with
+  | POSITIVE_XH  =>
+    match match_positive rhs with
+    | POSITIVE_XH  =>
+      xO xH
+    | POSITIVE_XO q =>
+      xI q
+    | POSITIVE_XI q =>
+      xO (positive_succ q)
+    end
+  | POSITIVE_XO p =>
+    match match_positive rhs with
+    | POSITIVE_XH  =>
+      xI p
+    | POSITIVE_XO q =>
+      xO (positive_add__add p q)
+    | POSITIVE_XI q =>
+      xI (positive_add__add p q)
+    end
+  | POSITIVE_XI p =>
+    match match_positive rhs with
+    | POSITIVE_XH  =>
+      xO (positive_succ p)
+    | POSITIVE_XO q =>
+      xI (positive_add__add p q)
+    | POSITIVE_XI q =>
+      xO (positive_add__add_carry p q)
+    end
+  end.
+
+Definition positive_add__add_carry (lhs : t_Positive_t) (rhs : t_Positive_t) : t_Positive_t :=
+  match match_positive lhs with
+  | POSITIVE_XH  =>
+    match match_positive rhs with
+    | POSITIVE_XH  =>
+      xI xH
+    | POSITIVE_XO q =>
+      xO (positive_succ q)
+    | POSITIVE_XI q =>
+      xI (positive_succ q)
+    end
+  | POSITIVE_XO p =>
+    match match_positive rhs with
+    | POSITIVE_XH  =>
+      xO (positive_succ p)
+    | POSITIVE_XO q =>
+      xI (positive_add__add p q)
+    | POSITIVE_XI q =>
+      xO (positive_add__add_carry p q)
+    end
+  | POSITIVE_XI p =>
+    match match_positive rhs with
+    | POSITIVE_XH  =>
+      xI (positive_succ p)
+    | POSITIVE_XO q =>
+      xO (positive_add__add_carry p q)
+    | POSITIVE_XI q =>
+      xI (positive_add__add_carry p q)
+    end
+  end.