Merge pull request #1064 from hacspec/coq-generic-printer-annotated-c…

…ore-lib

Move to annotated core lib

proof-libs/coq/coq/.gitignore

@@ -0,0 +1,7 @@
+*.vo*
+*.aux
+*.glob
+*.cache
+.Makefile.d
+Makefile
+Makefile.conf

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

@@ -0,0 +1,161 @@
+-R src/ Core
+-R spec/ Core
+-R phase_library/ Core
+-arg -w
+-arg all
+
+./src/Core_Clone.v
+./src/Core_Marker.v
+
+./src/Core_Panicking.v
+
+./src/Core_Ops_Function.v
+
+./src/Core_Option.v
+./src/Core_Cmp.v
+
+./spec/Core_Base_Spec_Haxint.v
+./spec/Core_Base_Spec_Unary.v
+
+./spec/Core_Base_Spec_Binary_Positive.v
+./spec/Core_Base_Spec_Binary_Pos.v
+
+./spec/Core_Base_Spec_Binary.v
+
+./spec/Core_Base_Spec_Z.v
+
+./spec/Core_Base_Spec_Seq.v
+
+./spec/Core_Base_Spec_Constants.v
+
+./spec/Core_Base_Spec.v
+
+./src/Core_Base_Binary.v
+./src/Core_Base_Pos.v
+./src/Core_Base_Z.v
+
+./src/Core_Base_Seq.v
+
+./src/Core_Base.v
+
+./src/Core_Convert.v
+
+./src/Core_Ops_Index.v
+
+./src/Core_Ops_Bit.v
+./src/Core_Ops_Arith.v
+
+./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
+
+./src/Core_Base_interface_Int.v
+
+./src/Core_Base_interface.v
+
+./src/Core_Num_Uint_macros.v # Empty
+./src/Core_Num_Int_macros.v # Empty
+
+./src/Core_Result.v
+
+./phase_library/ControlFlow.v
+
+# Bundles: Core_Primitive.v,
+./src/Core_Array_Rec_bundle_579704328.v
+
+# ./src/Core_Primitive_Number_conversion.v
+# ./src/Core_Primitive_Number_conversion_i.v
+
+./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_Index_Private_slice_index.v
+# Core_Slice_Index.v
+# ----- Core_Slice.v
+# ----- Core_Result.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
+# Core_Ops_Index_range.v
+# ----- Core_Ops_Index.v
+# Core_Ops_Function.v
+# Core_Ops_Bit_Impls_for_prims.v
+# ----- Core_Ops_Bit.v
+# Core_Ops_Arith_Impls_for_prims.v
+# ----- Core_Ops_Arith.v
+# ----- Core_Ops.v
+# ----- Core_Num_Uint_macros.v
+# ----- Core_Num_Int_macros.v
+# ----- Core_Num.v
+# ----- Core_Marker.v
+# Core_Iter_Traits_Marker.v
+# Core_Iter_Traits_Iterator.v
+# Core_Iter_Traits_Exact_size.v
+# Core_Iter_Traits_Collect.v
+# Core_Iter_Traits.v
+# Core_Iter_Range.v
+# Core_Iter.v
+# ----- Core_Intrinsics.v
+# Core_Fmt.v
+# ----- Core_Convert.v
+# ----- Core_Cmp.v
+# ----- Core_Clone.v
+# Core_Base_interface_Int_U8_proofs.v
+# Core_Base_interface_Int_U64_proofs.v
+# Core_Base_interface_Int_U32_proofs.v
+# Core_Base_interface_Int_U16_proofs.v
+# Core_Base_interface_Int_U128_proofs.v
+# Core_Base_interface_Int_I8_proofs.v
+# Core_Base_interface_Int_I64_proofs.v
+# Core_Base_interface_Int_I32_proofs.v
+# Core_Base_interface_Int_I16_proofs.v
+# Core_Base_interface_Int_I128_proofs.v
+# ----- Core_Base_interface_Int.v
+# ----- Core_Base_interface_Coerce.v
+# ----- Core_Base_interface.v
+# ----- Core_Base_Z.v
+# ----- Core_Base_Spec_Z.v
+# ----- Core_Base_Spec_Unary.v
+# ----- Core_Base_Spec_Seq.v
+# ----- Core_Base_Spec_Haxint.v
+# ----- Core_Base_Spec_Constants.v
+# ----- Core_Base_Spec_Binary_Positive.v
+# ----- Core_Base_Spec_Binary_Pos.v
+# ----- Core_Base_Spec_Binary.v
+# ----- Core_Base_Spec.v
+# ----- Core_Base_Seq.v
+# ----- Core_Base_Pos.v
+# 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

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

@@ -0,0 +1,45 @@
+(* File automatically generated by Hacspec *)
+From Coq Require Import ZArith.
+Require Import List.
+Import List.ListNotations.
+Open Scope Z_scope.
+Open Scope bool_scope.
+Require Import Ascii.
+Require Import String.
+Require Import Coq.Floats.Floats.
+From RecordUpdate Require Import RecordSet.
+Import RecordSetNotations.
+
+(* From Core Require Import Core. *)
+
+From Core Require Import Core_Marker.
+
+From Core Require Import Core_Convert.
+
+From Core Require Import Core_Base_interface_Int.
+
+From Core Require Import Core_Result.
+
+Inductive t_ControlFlow a b :=
+| ControlFlow_Continue : a -> t_ControlFlow a b
+| ControlFlow_Break : b -> t_ControlFlow a b.
+Arguments ControlFlow_Continue {a} {b}.
+Arguments ControlFlow_Break {a} {b}.
+
+(* Run exception *)
+Definition run {a} (x : t_ControlFlow a a) : a :=
+  match x with
+  | ControlFlow_Continue x => x
+  | ControlFlow_Break x => x
+  end.
+
+Definition bind_exception {a c}
+  (x : t_ControlFlow a c)
+  (f : forall (k : a) `{x = ControlFlow_Continue k}, t_ControlFlow a c) : t_ControlFlow a c :=
+  match x as k return x = k -> _ with
+  | ControlFlow_Continue o => fun k => f (H := k) o
+  | ControlFlow_Break o => fun _ => ControlFlow_Break o
+  end eq_refl.
+
+Notation "'letb' p ':=' e 'in' rhs" :=
+  (bind_exception e (fun p _ => rhs)) (at level 100).

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

@@ -0,0 +1,52 @@
+(* File automatically generated by Hacspec *)
+From Coq Require Import ZArith.
+Require Import List.
+Import List.ListNotations.
+Open Scope Z_scope.
+Open Scope bool_scope.
+Require Import Ascii.
+Require Import String.
+Require Import Coq.Floats.Floats.
+From RecordUpdate Require Import RecordSet.
+Import RecordSetNotations.
+
+Require Import Core_Primitive.
+Export Core_Primitive.
+
+(* Handwritten *)
+
+Coercion Build_t_i8 : t_I8 >-> t_i8.
+Coercion Build_t_I8 : Z >-> t_I8.
+
+Coercion Build_t_i16 : t_I16 >-> t_i16.
+Coercion Build_t_I16 : Z >-> t_I16.
+
+Coercion Build_t_i32 : t_I32 >-> t_i32.
+Coercion Build_t_I32 : Z >-> t_I32.
+
+Coercion Build_t_i64 : t_I64 >-> t_i64.
+Coercion Build_t_I64 : Z >-> t_I64.
+
+Coercion Build_t_i128 : t_I128 >-> t_i128.
+Coercion Build_t_I128 : Z >-> t_I128.
+
+Coercion Build_t_isize : t_I64 >-> t_isize.
+
+Coercion Build_t_u8 : t_U8 >-> t_u8.
+Coercion Build_t_U8 : N >-> t_U8.
+
+Coercion Build_t_u16 : t_U16 >-> t_u16.
+Coercion Build_t_U16 : N >-> t_U16.
+
+Coercion Build_t_u32 : t_U32 >-> t_u32.
+Coercion Build_t_U32 : N >-> t_U32.
+
+Coercion Build_t_u64 : t_U64 >-> t_u64.
+Coercion Build_t_U64 : N >-> t_U64.
+
+Coercion Build_t_u128 : t_U128 >-> t_u128.
+Coercion Build_t_U128 : N >-> t_U128.
+
+Coercion Build_t_usize : t_U64 >-> t_usize.
+
+Coercion Z.to_N : Z >-> N.

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

@@ -0,0 +1,43 @@
+(* File automatically generated by Hacspec *)
+From Coq Require Import ZArith.
+Require Import List.
+Import List.ListNotations.
+Open Scope Z_scope.
+Open Scope bool_scope.
+Require Import Ascii.
+Require Import String.
+Require Import Coq.Floats.Floats.
+From RecordUpdate Require Import RecordSet.
+Import RecordSetNotations.
+
+Require Import Core_Primitive.
+Export Core_Primitive.
+
+(* Array coercions *)
+Coercion Build_t_Array : t_Slice >-> t_Array.
+Coercion Build_t_Slice : list >-> t_Slice.
+
+Definition unsize {A} (x : A) := x.
+Definition repeat {v_T} (a : v_T) b : t_Array v_T b := List.repeat a (N.to_nat (U64_f_v (usize_0 b))).
+
+Definition t_String := string.
+Definition ToString_f_to_string (x : string) : string := x.
+
+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 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/spec/Core_Base_Spec.v

@@ -0,0 +1,43 @@
+(* File automatically generated by Hacspec *)
+From Coq Require Import ZArith.
+Require Import List.
+Import List.ListNotations.
+Open Scope Z_scope.
+Open Scope bool_scope.
+Require Import Ascii.
+Require Import String.
+Require Import Coq.Floats.Floats.
+From RecordUpdate Require Import RecordSet.
+Import RecordSetNotations.
+
+(* From Core Require Import Core. *)
+
+From Core Require Import Core_Base_Spec_Haxint.
+Export Core_Base_Spec_Haxint.
+
+From Core Require Import Core_Base_Spec_Unary.
+Export Core_Base_Spec_Unary.
+
+From Core Require Import Core_Base_Spec_Binary.
+Export Core_Base_Spec_Binary.
+
+From Core Require Import Core_Base_Spec_Z.
+Export Core_Base_Spec_Z.
+
+From Core Require Import Core_Base_Spec_Seq.
+Export Core_Base_Spec_Seq.
+
+From Core Require Import Core_Base_Spec_Constants.
+Export Core_Base_Spec_Constants.
+
+(* NotImplementedYet *)
+
+(* NotImplementedYet *)
+
+(* NotImplementedYet *)
+
+(* NotImplementedYet *)
+
+(* NotImplementedYet *)
+
+(* NotImplementedYet *)

proof-libs/coq/coq/generated-core/spec/Core_Base_Spec_Binary.v

@@ -0,0 +1,23 @@
+(* File automatically generated by Hacspec *)
+From Coq Require Import ZArith.
+Require Import List.
+Import List.ListNotations.
+Open Scope Z_scope.
+Open Scope bool_scope.
+Require Import Ascii.
+Require Import String.
+Require Import Coq.Floats.Floats.
+From RecordUpdate Require Import RecordSet.
+Import RecordSetNotations.
+
+(* From Core Require Import Core. *)
+
+From Core Require Import Core_Base_Spec_Binary_Pos.
+Export Core_Base_Spec_Binary_Pos.
+
+From Core Require Import Core_Base_Spec_Binary_Positive.
+Export Core_Base_Spec_Binary_Positive.
+
+(* NotImplementedYet *)
+
+(* NotImplementedYet *)