diff options
Diffstat (limited to '')
| -rw-r--r-- | tests/coq/array/Array.v (renamed from tests/coq/array/Array_Funs.v) | 36 | ||||
| -rw-r--r-- | tests/coq/array/Array_Types.v | 14 | ||||
| -rw-r--r-- | tests/coq/array/_CoqProject | 3 | ||||
| -rw-r--r-- | tests/coq/betree/BetreeMain_Types.v | 4 | ||||
| -rw-r--r-- | tests/coq/hashmap/Hashmap_Types.v | 14 | ||||
| -rw-r--r-- | tests/coq/hashmap_on_disk/HashmapMain_Types.v | 14 | ||||
| -rw-r--r-- | tests/coq/misc/Constants.v | 10 | ||||
| -rw-r--r-- | tests/coq/misc/Loops.v | 4 | ||||
| -rw-r--r-- | tests/coq/misc/NoNestedBorrows.v | 32 | ||||
| -rw-r--r-- | tests/coq/misc/Paper.v | 4 | ||||
| -rw-r--r-- | tests/coq/misc/PoloniusList.v | 4 | ||||
| -rw-r--r-- | tests/coq/traits/Primitives.v | 822 | ||||
| -rw-r--r-- | tests/coq/traits/Traits.v | 520 | ||||
| -rw-r--r-- | tests/coq/traits/_CoqProject | 2 |
14 files changed, 1403 insertions, 80 deletions
diff --git a/tests/coq/array/Array_Funs.v b/tests/coq/array/Array.v index 9980a6e8..825f73e0 100644 --- a/tests/coq/array/Array_Funs.v +++ b/tests/coq/array/Array.v @@ -1,14 +1,15 @@ (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [array]: function definitions *) +(** [array] *) Require Import Primitives. Import Primitives. Require Import Coq.ZArith.ZArith. Require Import List. Import ListNotations. Local Open Scope Primitives_scope. -Require Export Array_Types. -Import Array_Types. -Module Array_Funs. +Module Array. + +(** [array::AB] *) +Inductive AB_t := | AB_A : AB_t | AB_B : AB_t. (** [array::incr]: merged forward/backward function (there is a single backward function, and the forward function returns ()) *) @@ -98,7 +99,7 @@ Definition index_mut_slice_back (** [array::slice_subslice_shared_]: forward function *) Definition slice_subslice_shared_ - (n : nat) (x : slice u32) (y : usize) (z : usize) : result (slice u32) := + (x : slice u32) (y : usize) (z : usize) : result (slice u32) := core_slice_index_Slice_index u32 (core_ops_range_Range usize) (core_slice_index_Range_coresliceindexSliceIndexInst u32) x {| core_ops_range_Range_start := y; core_ops_range_Range_end_ := z |} @@ -106,7 +107,7 @@ Definition slice_subslice_shared_ (** [array::slice_subslice_mut_]: forward function *) Definition slice_subslice_mut_ - (n : nat) (x : slice u32) (y : usize) (z : usize) : result (slice u32) := + (x : slice u32) (y : usize) (z : usize) : result (slice u32) := core_slice_index_Slice_index_mut u32 (core_ops_range_Range usize) (core_slice_index_Range_coresliceindexSliceIndexInst u32) x {| core_ops_range_Range_start := y; core_ops_range_Range_end_ := z |} @@ -114,7 +115,7 @@ Definition slice_subslice_mut_ (** [array::slice_subslice_mut_]: backward function 0 *) Definition slice_subslice_mut__back - (n : nat) (x : slice u32) (y : usize) (z : usize) (ret : slice u32) : + (x : slice u32) (y : usize) (z : usize) (ret : slice u32) : result (slice u32) := core_slice_index_Slice_index_mut_back u32 (core_ops_range_Range usize) @@ -141,9 +142,7 @@ Definition array_to_slice_mut__back (** [array::array_subslice_shared_]: forward function *) Definition array_subslice_shared_ - (n : nat) (x : array u32 32%usize) (y : usize) (z : usize) : - result (slice u32) - := + (x : array u32 32%usize) (y : usize) (z : usize) : result (slice u32) := core_array_Array_index u32 (core_ops_range_Range usize) 32%usize (core_slice_index_Slice_coreopsindexIndexInst u32 (core_ops_range_Range usize) (core_slice_index_Range_coresliceindexSliceIndexInst u32)) x @@ -152,9 +151,7 @@ Definition array_subslice_shared_ (** [array::array_subslice_mut_]: forward function *) Definition array_subslice_mut_ - (n : nat) (x : array u32 32%usize) (y : usize) (z : usize) : - result (slice u32) - := + (x : array u32 32%usize) (y : usize) (z : usize) : result (slice u32) := core_array_Array_index_mut u32 (core_ops_range_Range usize) 32%usize (core_slice_index_Slice_coreopsindexIndexMutInst u32 (core_ops_range_Range usize) (core_slice_index_Range_coresliceindexSliceIndexInst u32)) x @@ -163,8 +160,7 @@ Definition array_subslice_mut_ (** [array::array_subslice_mut_]: backward function 0 *) Definition array_subslice_mut__back - (n : nat) (x : array u32 32%usize) (y : usize) (z : usize) (ret : slice u32) - : + (x : array u32 32%usize) (y : usize) (z : usize) (ret : slice u32) : result (array u32 32%usize) := core_array_Array_index_mut_back u32 (core_ops_range_Range usize) 32%usize @@ -310,7 +306,7 @@ Definition update_all : result unit := . (** [array::range_all]: forward function *) -Definition range_all (n : nat) : result unit := +Definition range_all : result unit := s <- core_array_Array_index_mut u32 (core_ops_range_Range usize) 4%usize (core_slice_index_Slice_coreopsindexIndexMutInst u32 @@ -432,9 +428,7 @@ Definition f2 (i : u32) : result unit := (** [array::f4]: forward function *) Definition f4 - (n : nat) (x : array u32 32%usize) (y : usize) (z : usize) : - result (slice u32) - := + (x : array u32 32%usize) (y : usize) (z : usize) : result (slice u32) := core_array_Array_index u32 (core_ops_range_Range usize) 32%usize (core_slice_index_Slice_coreopsindexIndexInst u32 (core_ops_range_Range usize) (core_slice_index_Range_coresliceindexSliceIndexInst u32)) x @@ -449,7 +443,7 @@ Definition f3 (n : nat) : result u32 := _ <- f2 i; let b := array_repeat u32 32%usize 0%u32 in s <- array_to_slice u32 2%usize (mk_array u32 2%usize [ 1%u32; 2%u32 ]); - s0 <- f4 n b 16%usize 18%usize; + s0 <- f4 b 16%usize 18%usize; sum2 n s s0 . @@ -473,4 +467,4 @@ Definition ite : result unit := Return tt . -End Array_Funs . +End Array . diff --git a/tests/coq/array/Array_Types.v b/tests/coq/array/Array_Types.v deleted file mode 100644 index a13d64e6..00000000 --- a/tests/coq/array/Array_Types.v +++ /dev/null @@ -1,14 +0,0 @@ -(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [array]: type definitions *) -Require Import Primitives. -Import Primitives. -Require Import Coq.ZArith.ZArith. -Require Import List. -Import ListNotations. -Local Open Scope Primitives_scope. -Module Array_Types. - -(** [array::AB] *) -Inductive AB_t := | AB_A : AB_t | AB_B : AB_t. - -End Array_Types . diff --git a/tests/coq/array/_CoqProject b/tests/coq/array/_CoqProject index f33cefe6..87d8fc3d 100644 --- a/tests/coq/array/_CoqProject +++ b/tests/coq/array/_CoqProject @@ -3,6 +3,5 @@ -arg -w -arg all -Array_Funs.v Primitives.v -Array_Types.v +Array.v diff --git a/tests/coq/betree/BetreeMain_Types.v b/tests/coq/betree/BetreeMain_Types.v index ee26622e..933a670c 100644 --- a/tests/coq/betree/BetreeMain_Types.v +++ b/tests/coq/betree/BetreeMain_Types.v @@ -14,8 +14,8 @@ Inductive betree_List_t (T : Type) := | Betree_List_Nil : betree_List_t T . -Arguments Betree_List_Cons {T} _ _. -Arguments Betree_List_Nil {T}. +Arguments Betree_List_Cons { _ }. +Arguments Betree_List_Nil { _ }. (** [betree_main::betree::UpsertFunState] *) Inductive betree_UpsertFunState_t := diff --git a/tests/coq/hashmap/Hashmap_Types.v b/tests/coq/hashmap/Hashmap_Types.v index 63d30eeb..8529803d 100644 --- a/tests/coq/hashmap/Hashmap_Types.v +++ b/tests/coq/hashmap/Hashmap_Types.v @@ -14,8 +14,8 @@ Inductive List_t (T : Type) := | List_Nil : List_t T . -Arguments List_Cons {T} _ _ _. -Arguments List_Nil {T}. +Arguments List_Cons { _ }. +Arguments List_Nil { _ }. (** [hashmap::HashMap] *) Record HashMap_t (T : Type) := @@ -27,10 +27,10 @@ mkHashMap_t { } . -Arguments mkHashMap_t {T} _ _ _ _. -Arguments hashMap_num_entries {T}. -Arguments hashMap_max_load_factor {T}. -Arguments hashMap_max_load {T}. -Arguments hashMap_slots {T}. +Arguments mkHashMap_t { _ }. +Arguments hashMap_num_entries { _ }. +Arguments hashMap_max_load_factor { _ }. +Arguments hashMap_max_load { _ }. +Arguments hashMap_slots { _ }. End Hashmap_Types . diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Types.v b/tests/coq/hashmap_on_disk/HashmapMain_Types.v index 466119f8..95e5f35b 100644 --- a/tests/coq/hashmap_on_disk/HashmapMain_Types.v +++ b/tests/coq/hashmap_on_disk/HashmapMain_Types.v @@ -14,8 +14,8 @@ Inductive hashmap_List_t (T : Type) := | Hashmap_List_Nil : hashmap_List_t T . -Arguments Hashmap_List_Cons {T} _ _ _. -Arguments Hashmap_List_Nil {T}. +Arguments Hashmap_List_Cons { _ }. +Arguments Hashmap_List_Nil { _ }. (** [hashmap_main::hashmap::HashMap] *) Record hashmap_HashMap_t (T : Type) := @@ -27,11 +27,11 @@ mkhashmap_HashMap_t { } . -Arguments mkhashmap_HashMap_t {T} _ _ _ _. -Arguments hashmap_HashMap_num_entries {T}. -Arguments hashmap_HashMap_max_load_factor {T}. -Arguments hashmap_HashMap_max_load {T}. -Arguments hashmap_HashMap_slots {T}. +Arguments mkhashmap_HashMap_t { _ }. +Arguments hashmap_HashMap_num_entries { _ }. +Arguments hashmap_HashMap_max_load_factor { _ }. +Arguments hashmap_HashMap_max_load { _ }. +Arguments hashmap_HashMap_slots { _ }. (** The state type used in the state-error monad *) Axiom state : Type. diff --git a/tests/coq/misc/Constants.v b/tests/coq/misc/Constants.v index 7cb1a642..03653f69 100644 --- a/tests/coq/misc/Constants.v +++ b/tests/coq/misc/Constants.v @@ -35,9 +35,9 @@ Definition mk_pair0 (x : u32) (y : u32) : result (u32 * u32) := (** [constants::Pair] *) Record Pair_t (T1 T2 : Type) := mkPair_t { pair_x : T1; pair_y : T2; }. -Arguments mkPair_t {T1} {T2} _ _. -Arguments pair_x {T1} {T2}. -Arguments pair_y {T1} {T2}. +Arguments mkPair_t { _ _ }. +Arguments pair_x { _ _ }. +Arguments pair_y { _ _ }. (** [constants::mk_pair1]: forward function *) Definition mk_pair1 (x : u32) (y : u32) : result (Pair_t u32 u32) := @@ -65,8 +65,8 @@ Definition p3_c : Pair_t u32 u32 := p3_body%global. (** [constants::Wrap] *) Record Wrap_t (T : Type) := mkWrap_t { wrap_value : T; }. -Arguments mkWrap_t {T} _. -Arguments wrap_value {T}. +Arguments mkWrap_t { _ }. +Arguments wrap_value { _ }. (** [constants::Wrap::{0}::new]: forward function *) Definition wrap_new (T : Type) (value : T) : result (Wrap_t T) := diff --git a/tests/coq/misc/Loops.v b/tests/coq/misc/Loops.v index 180a1d68..1c0eab17 100644 --- a/tests/coq/misc/Loops.v +++ b/tests/coq/misc/Loops.v @@ -96,8 +96,8 @@ Inductive List_t (T : Type) := | List_Nil : List_t T . -Arguments List_Cons {T} _ _. -Arguments List_Nil {T}. +Arguments List_Cons { _ }. +Arguments List_Nil { _ }. (** [loops::list_mem]: loop 0: forward function *) Fixpoint list_mem_loop (n : nat) (x : u32) (ls : List_t u32) : result bool := diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v index e916ca4a..c7af496f 100644 --- a/tests/coq/misc/NoNestedBorrows.v +++ b/tests/coq/misc/NoNestedBorrows.v @@ -11,9 +11,9 @@ Module NoNestedBorrows. (** [no_nested_borrows::Pair] *) Record Pair_t (T1 T2 : Type) := mkPair_t { pair_x : T1; pair_y : T2; }. -Arguments mkPair_t {T1} {T2} _ _. -Arguments pair_x {T1} {T2}. -Arguments pair_y {T1} {T2}. +Arguments mkPair_t { _ _ }. +Arguments pair_x { _ _ }. +Arguments pair_y { _ _ }. (** [no_nested_borrows::List] *) Inductive List_t (T : Type) := @@ -21,13 +21,13 @@ Inductive List_t (T : Type) := | List_Nil : List_t T . -Arguments List_Cons {T} _ _. -Arguments List_Nil {T}. +Arguments List_Cons { _ }. +Arguments List_Nil { _ }. (** [no_nested_borrows::One] *) Inductive One_t (T1 : Type) := | One_One : T1 -> One_t T1. -Arguments One_One {T1} _. +Arguments One_One { _ }. (** [no_nested_borrows::EmptyEnum] *) Inductive EmptyEnum_t := | EmptyEnum_Empty : EmptyEnum_t. @@ -44,8 +44,8 @@ Inductive Sum_t (T1 T2 : Type) := | Sum_Right : T2 -> Sum_t T1 T2 . -Arguments Sum_Left {T1} {T2} _. -Arguments Sum_Right {T1} {T2} _. +Arguments Sum_Left { _ _ }. +Arguments Sum_Right { _ _ }. (** [no_nested_borrows::neg_test]: forward function *) Definition neg_test (x : i32) : result i32 := @@ -258,11 +258,11 @@ with NodeElem_t (T : Type) := | NodeElem_Nil : NodeElem_t T . -Arguments Tree_Leaf {T} _. -Arguments Tree_Node {T} _ _ _. +Arguments Tree_Leaf { _ }. +Arguments Tree_Node { _ }. -Arguments NodeElem_Cons {T} _ _. -Arguments NodeElem_Nil {T}. +Arguments NodeElem_Cons { _ }. +Arguments NodeElem_Nil { _ }. (** [no_nested_borrows::list_length]: forward function *) Fixpoint list_length (T : Type) (l : List_t T) : result u32 := @@ -425,8 +425,8 @@ mkStructWithTuple_t { } . -Arguments mkStructWithTuple_t {T1} {T2} _. -Arguments structWithTuple_p {T1} {T2}. +Arguments mkStructWithTuple_t { _ _ }. +Arguments structWithTuple_p { _ _ }. (** [no_nested_borrows::new_tuple1]: forward function *) Definition new_tuple1 : result (StructWithTuple_t u32 u32) := @@ -450,8 +450,8 @@ mkStructWithPair_t { } . -Arguments mkStructWithPair_t {T1} {T2} _. -Arguments structWithPair_p {T1} {T2}. +Arguments mkStructWithPair_t { _ _ }. +Arguments structWithPair_p { _ _ }. (** [no_nested_borrows::new_pair1]: forward function *) Definition new_pair1 : result (StructWithPair_t u32 u32) := diff --git a/tests/coq/misc/Paper.v b/tests/coq/misc/Paper.v index d397995b..d3852e6b 100644 --- a/tests/coq/misc/Paper.v +++ b/tests/coq/misc/Paper.v @@ -55,8 +55,8 @@ Inductive List_t (T : Type) := | List_Nil : List_t T . -Arguments List_Cons {T} _ _. -Arguments List_Nil {T}. +Arguments List_Cons { _ }. +Arguments List_Nil { _ }. (** [paper::list_nth_mut]: forward function *) Fixpoint list_nth_mut (T : Type) (l : List_t T) (i : u32) : result T := diff --git a/tests/coq/misc/PoloniusList.v b/tests/coq/misc/PoloniusList.v index 4f804b55..4848444f 100644 --- a/tests/coq/misc/PoloniusList.v +++ b/tests/coq/misc/PoloniusList.v @@ -14,8 +14,8 @@ Inductive List_t (T : Type) := | List_Nil : List_t T . -Arguments List_Cons {T} _ _. -Arguments List_Nil {T}. +Arguments List_Cons { _ }. +Arguments List_Nil { _ }. (** [polonius_list::get_list_at_x]: forward function *) Fixpoint get_list_at_x (ls : List_t u32) (x : u32) : result (List_t u32) := diff --git a/tests/coq/traits/Primitives.v b/tests/coq/traits/Primitives.v new file mode 100644 index 00000000..85e38f01 --- /dev/null +++ b/tests/coq/traits/Primitives.v @@ -0,0 +1,822 @@ +Require Import Lia. +Require Coq.Strings.Ascii. +Require Coq.Strings.String. +Require Import Coq.Program.Equality. +Require Import Coq.ZArith.ZArith. +Require Import Coq.ZArith.Znat. +Require Import List. +Import ListNotations. + +Module Primitives. + + (* TODO: use more *) +Declare Scope Primitives_scope. + +(*** Result *) + +Inductive error := + | Failure + | OutOfFuel. + +Inductive result A := + | Return : A -> result A + | Fail_ : error -> result A. + +Arguments Return {_} a. +Arguments Fail_ {_}. + +Definition bind {A B} (m: result A) (f: A -> result B) : result B := + match m with + | Fail_ e => Fail_ e + | Return x => f x + end. + +Definition return_ {A: Type} (x: A) : result A := Return x. +Definition fail_ {A: Type} (e: error) : result A := Fail_ e. + +Notation "x <- c1 ; c2" := (bind c1 (fun x => c2)) + (at level 61, c1 at next level, right associativity). + +(** Monadic assert *) +Definition massert (b: bool) : result unit := + if b then Return tt else Fail_ Failure. + +(** Normalize and unwrap a successful result (used for globals) *) +Definition eval_result_refl {A} {x} (a: result A) (p: a = Return x) : A := + match a as r return (r = Return x -> A) with + | Return a' => fun _ => a' + | Fail_ e => fun p' => + False_rect _ (eq_ind (Fail_ e) + (fun e : result A => + match e with + | Return _ => False + | Fail_ e => True + end) + I (Return x) p') + end p. + +Notation "x %global" := (eval_result_refl x eq_refl) (at level 40). +Notation "x %return" := (eval_result_refl x eq_refl) (at level 40). + +(* Sanity check *) +Check (if true then Return (1 + 2) else Fail_ Failure)%global = 3. + +(*** Misc *) + +Definition string := Coq.Strings.String.string. +Definition char := Coq.Strings.Ascii.ascii. +Definition char_of_byte := Coq.Strings.Ascii.ascii_of_byte. + +Definition core_mem_replace (a : Type) (x : a) (y : a) : a := x . +Definition core_mem_replace_back (a : Type) (x : a) (y : a) : a := y . + +Record mut_raw_ptr (T : Type) := { mut_raw_ptr_v : T }. +Record const_raw_ptr (T : Type) := { const_raw_ptr_v : T }. + +(*** Scalars *) + +Definition i8_min : Z := -128%Z. +Definition i8_max : Z := 127%Z. +Definition i16_min : Z := -32768%Z. +Definition i16_max : Z := 32767%Z. +Definition i32_min : Z := -2147483648%Z. +Definition i32_max : Z := 2147483647%Z. +Definition i64_min : Z := -9223372036854775808%Z. +Definition i64_max : Z := 9223372036854775807%Z. +Definition i128_min : Z := -170141183460469231731687303715884105728%Z. +Definition i128_max : Z := 170141183460469231731687303715884105727%Z. +Definition u8_min : Z := 0%Z. +Definition u8_max : Z := 255%Z. +Definition u16_min : Z := 0%Z. +Definition u16_max : Z := 65535%Z. +Definition u32_min : Z := 0%Z. +Definition u32_max : Z := 4294967295%Z. +Definition u64_min : Z := 0%Z. +Definition u64_max : Z := 18446744073709551615%Z. +Definition u128_min : Z := 0%Z. +Definition u128_max : Z := 340282366920938463463374607431768211455%Z. + +(** The bounds of [isize] and [usize] vary with the architecture. *) +Axiom isize_min : Z. +Axiom isize_max : Z. +Definition usize_min : Z := 0%Z. +Axiom usize_max : Z. + +Open Scope Z_scope. + +(** We provide those lemmas to reason about the bounds of [isize] and [usize] *) +Axiom isize_min_bound : isize_min <= i32_min. +Axiom isize_max_bound : i32_max <= isize_max. +Axiom usize_max_bound : u32_max <= usize_max. + +Inductive scalar_ty := + | Isize + | I8 + | I16 + | I32 + | I64 + | I128 + | Usize + | U8 + | U16 + | U32 + | U64 + | U128 +. + +Definition scalar_min (ty: scalar_ty) : Z := + match ty with + | Isize => isize_min + | I8 => i8_min + | I16 => i16_min + | I32 => i32_min + | I64 => i64_min + | I128 => i128_min + | Usize => usize_min + | U8 => u8_min + | U16 => u16_min + | U32 => u32_min + | U64 => u64_min + | U128 => u128_min +end. + +Definition scalar_max (ty: scalar_ty) : Z := + match ty with + | Isize => isize_max + | I8 => i8_max + | I16 => i16_max + | I32 => i32_max + | I64 => i64_max + | I128 => i128_max + | Usize => usize_max + | U8 => u8_max + | U16 => u16_max + | U32 => u32_max + | U64 => u64_max + | U128 => u128_max +end. + +(** We use the following conservative bounds to make sure we can compute bound + checks in most situations *) +Definition scalar_min_cons (ty: scalar_ty) : Z := + match ty with + | Isize => i32_min + | Usize => u32_min + | _ => scalar_min ty +end. + +Definition scalar_max_cons (ty: scalar_ty) : Z := + match ty with + | Isize => i32_max + | Usize => u32_max + | _ => scalar_max ty +end. + +Lemma scalar_min_cons_valid : forall ty, scalar_min ty <= scalar_min_cons ty . +Proof. + destruct ty; unfold scalar_min_cons, scalar_min; try lia. + - pose isize_min_bound; lia. + - apply Z.le_refl. +Qed. + +Lemma scalar_max_cons_valid : forall ty, scalar_max ty >= scalar_max_cons ty . +Proof. + destruct ty; unfold scalar_max_cons, scalar_max; try lia. + - pose isize_max_bound; lia. + - pose usize_max_bound. lia. +Qed. + +Definition scalar (ty: scalar_ty) : Type := + { x: Z | scalar_min ty <= x <= scalar_max ty }. + +Definition to_Z {ty} (x: scalar ty) : Z := proj1_sig x. + +(** Bounds checks: we start by using the conservative bounds, to make sure we + can compute in most situations, then we use the real bounds (for [isize] + and [usize]). *) +Definition scalar_ge_min (ty: scalar_ty) (x: Z) : bool := + Z.leb (scalar_min_cons ty) x || Z.leb (scalar_min ty) x. + +Definition scalar_le_max (ty: scalar_ty) (x: Z) : bool := + Z.leb x (scalar_max_cons ty) || Z.leb x (scalar_max ty). + +Lemma scalar_ge_min_valid (ty: scalar_ty) (x: Z) : + scalar_ge_min ty x = true -> scalar_min ty <= x . +Proof. + unfold scalar_ge_min. + pose (scalar_min_cons_valid ty). + lia. +Qed. + +Lemma scalar_le_max_valid (ty: scalar_ty) (x: Z) : + scalar_le_max ty x = true -> x <= scalar_max ty . +Proof. + unfold scalar_le_max. + pose (scalar_max_cons_valid ty). + lia. +Qed. + +Definition scalar_in_bounds (ty: scalar_ty) (x: Z) : bool := + scalar_ge_min ty x && scalar_le_max ty x . + +Lemma scalar_in_bounds_valid (ty: scalar_ty) (x: Z) : + scalar_in_bounds ty x = true -> scalar_min ty <= x <= scalar_max ty . +Proof. + unfold scalar_in_bounds. + intros H. + destruct (scalar_ge_min ty x) eqn:Hmin. + - destruct (scalar_le_max ty x) eqn:Hmax. + + pose (scalar_ge_min_valid ty x Hmin). + pose (scalar_le_max_valid ty x Hmax). + lia. + + inversion H. + - inversion H. +Qed. + +Import Sumbool. + +Definition mk_scalar (ty: scalar_ty) (x: Z) : result (scalar ty) := + match sumbool_of_bool (scalar_in_bounds ty x) with + | left H => Return (exist _ x (scalar_in_bounds_valid _ _ H)) + | right _ => Fail_ Failure + end. + +Definition scalar_add {ty} (x y: scalar ty) : result (scalar ty) := mk_scalar ty (to_Z x + to_Z y). + +Definition scalar_sub {ty} (x y: scalar ty) : result (scalar ty) := mk_scalar ty (to_Z x - to_Z y). + +Definition scalar_mul {ty} (x y: scalar ty) : result (scalar ty) := mk_scalar ty (to_Z x * to_Z y). + +Definition scalar_div {ty} (x y: scalar ty) : result (scalar ty) := + if to_Z y =? 0 then Fail_ Failure else + mk_scalar ty (to_Z x / to_Z y). + +Definition scalar_rem {ty} (x y: scalar ty) : result (scalar ty) := mk_scalar ty (Z.rem (to_Z x) (to_Z y)). + +Definition scalar_neg {ty} (x: scalar ty) : result (scalar ty) := mk_scalar ty (-(to_Z x)). + +(** Cast an integer from a [src_ty] to a [tgt_ty] *) +(* TODO: check the semantics of casts in Rust *) +Definition scalar_cast (src_ty tgt_ty : scalar_ty) (x : scalar src_ty) : result (scalar tgt_ty) := + mk_scalar tgt_ty (to_Z x). + +(** Comparisons *) +Definition scalar_leb {ty : scalar_ty} (x : scalar ty) (y : scalar ty) : bool := + Z.leb (to_Z x) (to_Z y) . + +Definition scalar_ltb {ty : scalar_ty} (x : scalar ty) (y : scalar ty) : bool := + Z.ltb (to_Z x) (to_Z y) . + +Definition scalar_geb {ty : scalar_ty} (x : scalar ty) (y : scalar ty) : bool := + Z.geb (to_Z x) (to_Z y) . + +Definition scalar_gtb {ty : scalar_ty} (x : scalar ty) (y : scalar ty) : bool := + Z.gtb (to_Z x) (to_Z y) . + +Definition scalar_eqb {ty : scalar_ty} (x : scalar ty) (y : scalar ty) : bool := + Z.eqb (to_Z x) (to_Z y) . + +Definition scalar_neqb {ty : scalar_ty} (x : scalar ty) (y : scalar ty) : bool := + negb (Z.eqb (to_Z x) (to_Z y)) . + + +(** The scalar types *) +Definition isize := scalar Isize. +Definition i8 := scalar I8. +Definition i16 := scalar I16. +Definition i32 := scalar I32. +Definition i64 := scalar I64. +Definition i128 := scalar I128. +Definition usize := scalar Usize. +Definition u8 := scalar U8. +Definition u16 := scalar U16. +Definition u32 := scalar U32. +Definition u64 := scalar U64. +Definition u128 := scalar U128. + +(** Negaion *) +Definition isize_neg := @scalar_neg Isize. +Definition i8_neg := @scalar_neg I8. +Definition i16_neg := @scalar_neg I16. +Definition i32_neg := @scalar_neg I32. +Definition i64_neg := @scalar_neg I64. +Definition i128_neg := @scalar_neg I128. + +(** Division *) +Definition isize_div := @scalar_div Isize. +Definition i8_div := @scalar_div I8. +Definition i16_div := @scalar_div I16. +Definition i32_div := @scalar_div I32. +Definition i64_div := @scalar_div I64. +Definition i128_div := @scalar_div I128. +Definition usize_div := @scalar_div Usize. +Definition u8_div := @scalar_div U8. +Definition u16_div := @scalar_div U16. +Definition u32_div := @scalar_div U32. +Definition u64_div := @scalar_div U64. +Definition u128_div := @scalar_div U128. + +(** Remainder *) +Definition isize_rem := @scalar_rem Isize. +Definition i8_rem := @scalar_rem I8. +Definition i16_rem := @scalar_rem I16. +Definition i32_rem := @scalar_rem I32. +Definition i64_rem := @scalar_rem I64. +Definition i128_rem := @scalar_rem I128. +Definition usize_rem := @scalar_rem Usize. +Definition u8_rem := @scalar_rem U8. +Definition u16_rem := @scalar_rem U16. +Definition u32_rem := @scalar_rem U32. +Definition u64_rem := @scalar_rem U64. +Definition u128_rem := @scalar_rem U128. + +(** Addition *) +Definition isize_add := @scalar_add Isize. +Definition i8_add := @scalar_add I8. +Definition i16_add := @scalar_add I16. +Definition i32_add := @scalar_add I32. +Definition i64_add := @scalar_add I64. +Definition i128_add := @scalar_add I128. +Definition usize_add := @scalar_add Usize. +Definition u8_add := @scalar_add U8. +Definition u16_add := @scalar_add U16. +Definition u32_add := @scalar_add U32. +Definition u64_add := @scalar_add U64. +Definition u128_add := @scalar_add U128. + +(** Substraction *) +Definition isize_sub := @scalar_sub Isize. +Definition i8_sub := @scalar_sub I8. +Definition i16_sub := @scalar_sub I16. +Definition i32_sub := @scalar_sub I32. +Definition i64_sub := @scalar_sub I64. +Definition i128_sub := @scalar_sub I128. +Definition usize_sub := @scalar_sub Usize. +Definition u8_sub := @scalar_sub U8. +Definition u16_sub := @scalar_sub U16. +Definition u32_sub := @scalar_sub U32. +Definition u64_sub := @scalar_sub U64. +Definition u128_sub := @scalar_sub U128. + +(** Multiplication *) +Definition isize_mul := @scalar_mul Isize. +Definition i8_mul := @scalar_mul I8. +Definition i16_mul := @scalar_mul I16. +Definition i32_mul := @scalar_mul I32. +Definition i64_mul := @scalar_mul I64. +Definition i128_mul := @scalar_mul I128. +Definition usize_mul := @scalar_mul Usize. +Definition u8_mul := @scalar_mul U8. +Definition u16_mul := @scalar_mul U16. +Definition u32_mul := @scalar_mul U32. +Definition u64_mul := @scalar_mul U64. +Definition u128_mul := @scalar_mul U128. + +(** Small utility *) +Definition usize_to_nat (x: usize) : nat := Z.to_nat (to_Z x). + +(** Notations *) +Notation "x %isize" := ((mk_scalar Isize x)%return) (at level 9). +Notation "x %i8" := ((mk_scalar I8 x)%return) (at level 9). +Notation "x %i16" := ((mk_scalar I16 x)%return) (at level 9). +Notation "x %i32" := ((mk_scalar I32 x)%return) (at level 9). +Notation "x %i64" := ((mk_scalar I64 x)%return) (at level 9). +Notation "x %i128" := ((mk_scalar I128 x)%return) (at level 9). +Notation "x %usize" := ((mk_scalar Usize x)%return) (at level 9). +Notation "x %u8" := ((mk_scalar U8 x)%return) (at level 9). +Notation "x %u16" := ((mk_scalar U16 x)%return) (at level 9). +Notation "x %u32" := ((mk_scalar U32 x)%return) (at level 9). +Notation "x %u64" := ((mk_scalar U64 x)%return) (at level 9). +Notation "x %u128" := ((mk_scalar U128 x)%return) (at level 9). + +Notation "x s= y" := (scalar_eqb x y) (at level 80) : Primitives_scope. +Notation "x s<> y" := (scalar_neqb x y) (at level 80) : Primitives_scope. +Notation "x s<= y" := (scalar_leb x y) (at level 80) : Primitives_scope. +Notation "x s< y" := (scalar_ltb x y) (at level 80) : Primitives_scope. +Notation "x s>= y" := (scalar_geb x y) (at level 80) : Primitives_scope. +Notation "x s> y" := (scalar_gtb x y) (at level 80) : Primitives_scope. + +(** Constants *) +Definition core_u8_max := u8_max %u32. +Definition core_u16_max := u16_max %u32. +Definition core_u32_max := u32_max %u32. +Definition core_u64_max := u64_max %u64. +Definition core_u128_max := u64_max %u128. +Axiom core_usize_max : usize. (** TODO *) +Definition core_i8_max := i8_max %i32. +Definition core_i16_max := i16_max %i32. +Definition core_i32_max := i32_max %i32. +Definition core_i64_max := i64_max %i64. +Definition core_i128_max := i64_max %i128. +Axiom core_isize_max : isize. (** TODO *) + +(*** core::ops *) + +(* Trait declaration: [core::ops::index::Index] *) +Record core_ops_index_Index (Self Idx : Type) := mk_core_ops_index_Index { + core_ops_index_Index_Output : Type; + core_ops_index_Index_index : Self -> Idx -> result core_ops_index_Index_Output; +}. +Arguments mk_core_ops_index_Index {_ _}. +Arguments core_ops_index_Index_Output {_ _}. +Arguments core_ops_index_Index_index {_ _}. + +(* Trait declaration: [core::ops::index::IndexMut] *) +Record core_ops_index_IndexMut (Self Idx : Type) := mk_core_ops_index_IndexMut { + core_ops_index_IndexMut_indexInst : core_ops_index_Index Self Idx; + core_ops_index_IndexMut_index_mut : Self -> Idx -> result core_ops_index_IndexMut_indexInst.(core_ops_index_Index_Output); + core_ops_index_IndexMut_index_mut_back : Self -> Idx -> core_ops_index_IndexMut_indexInst.(core_ops_index_Index_Output) -> result Self; +}. +Arguments mk_core_ops_index_IndexMut {_ _}. +Arguments core_ops_index_IndexMut_indexInst {_ _}. +Arguments core_ops_index_IndexMut_index_mut {_ _}. +Arguments core_ops_index_IndexMut_index_mut_back {_ _}. + +(* Trait declaration [core::ops::deref::Deref] *) +Record core_ops_deref_Deref (Self : Type) := mk_core_ops_deref_Deref { + core_ops_deref_Deref_target : Type; + core_ops_deref_Deref_deref : Self -> result core_ops_deref_Deref_target; +}. +Arguments mk_core_ops_deref_Deref {_}. +Arguments core_ops_deref_Deref_target {_}. +Arguments core_ops_deref_Deref_deref {_}. + +(* Trait declaration [core::ops::deref::DerefMut] *) +Record core_ops_deref_DerefMut (Self : Type) := mk_core_ops_deref_DerefMut { + core_ops_deref_DerefMut_derefInst : core_ops_deref_Deref Self; + core_ops_deref_DerefMut_deref_mut : Self -> result core_ops_deref_DerefMut_derefInst.(core_ops_deref_Deref_target); + core_ops_deref_DerefMut_deref_mut_back : Self -> core_ops_deref_DerefMut_derefInst.(core_ops_deref_Deref_target) -> result Self; +}. +Arguments mk_core_ops_deref_DerefMut {_}. +Arguments core_ops_deref_DerefMut_derefInst {_}. +Arguments core_ops_deref_DerefMut_deref_mut {_}. +Arguments core_ops_deref_DerefMut_deref_mut_back {_}. + +Record core_ops_range_Range (T : Type) := mk_core_ops_range_Range { + core_ops_range_Range_start : T; + core_ops_range_Range_end_ : T; +}. +Arguments mk_core_ops_range_Range {_}. +Arguments core_ops_range_Range_start {_}. +Arguments core_ops_range_Range_end_ {_}. + +(*** [alloc] *) + +Definition alloc_boxed_Box_deref (T : Type) (x : T) : result T := Return x. +Definition alloc_boxed_Box_deref_mut (T : Type) (x : T) : result T := Return x. +Definition alloc_boxed_Box_deref_mut_back (T : Type) (_ : T) (x : T) : result T := Return x. + +(* Trait instance *) +Definition alloc_boxed_Box_coreOpsDerefInst (Self : Type) : core_ops_deref_Deref Self := {| + core_ops_deref_Deref_target := Self; + core_ops_deref_Deref_deref := alloc_boxed_Box_deref Self; +|}. + +(* Trait instance *) +Definition alloc_boxed_Box_coreOpsDerefMutInst (Self : Type) : core_ops_deref_DerefMut Self := {| + core_ops_deref_DerefMut_derefInst := alloc_boxed_Box_coreOpsDerefInst Self; + core_ops_deref_DerefMut_deref_mut := alloc_boxed_Box_deref_mut Self; + core_ops_deref_DerefMut_deref_mut_back := alloc_boxed_Box_deref_mut_back Self; +|}. + + +(*** Arrays *) +Definition array T (n : usize) := { l: list T | Z.of_nat (length l) = to_Z n}. + +Lemma le_0_usize_max : 0 <= usize_max. +Proof. + pose (H := usize_max_bound). + unfold u32_max in H. + lia. +Qed. + +Lemma eqb_imp_eq (x y : Z) : Z.eqb x y = true -> x = y. +Proof. + lia. +Qed. + +(* TODO: finish the definitions *) +Axiom mk_array : forall (T : Type) (n : usize) (l : list T), array T n. + +(* For initialization *) +Axiom array_repeat : forall (T : Type) (n : usize) (x : T), array T n. + +Axiom array_index_usize : forall (T : Type) (n : usize) (x : array T n) (i : usize), result T. +Axiom array_update_usize : forall (T : Type) (n : usize) (x : array T n) (i : usize) (nx : T), result (array T n). + +(*** Slice *) +Definition slice T := { l: list T | Z.of_nat (length l) <= usize_max}. + +Axiom slice_len : forall (T : Type) (s : slice T), usize. +Axiom slice_index_usize : forall (T : Type) (x : slice T) (i : usize), result T. +Axiom slice_update_usize : forall (T : Type) (x : slice T) (i : usize) (nx : T), result (slice T). + +(*** Subslices *) + +Axiom array_to_slice : forall (T : Type) (n : usize) (x : array T n), result (slice T). +Axiom array_from_slice : forall (T : Type) (n : usize) (x : array T n) (s : slice T), result (array T n). + +Axiom array_subslice: forall (T : Type) (n : usize) (x : array T n) (r : core_ops_range_Range usize), result (slice T). +Axiom array_update_subslice: forall (T : Type) (n : usize) (x : array T n) (r : core_ops_range_Range usize) (ns : slice T), result (array T n). + +Axiom slice_subslice: forall (T : Type) (x : slice T) (r : core_ops_range_Range usize), result (slice T). +Axiom slice_update_subslice: forall (T : Type) (x : slice T) (r : core_ops_range_Range usize) (ns : slice T), result (slice T). + +(*** Vectors *) + +Definition alloc_vec_Vec T := { l: list T | Z.of_nat (length l) <= usize_max }. + +Definition alloc_vec_Vec_to_list {T: Type} (v: alloc_vec_Vec T) : list T := proj1_sig v. + +Definition alloc_vec_Vec_length {T: Type} (v: alloc_vec_Vec T) : Z := Z.of_nat (length (alloc_vec_Vec_to_list v)). + +Definition alloc_vec_Vec_new (T: Type) : alloc_vec_Vec T := (exist _ [] le_0_usize_max). + +Lemma alloc_vec_Vec_len_in_usize {T} (v: alloc_vec_Vec T) : usize_min <= alloc_vec_Vec_length v <= usize_max. +Proof. + unfold alloc_vec_Vec_length, usize_min. + split. + - lia. + - apply (proj2_sig v). +Qed. + +Definition alloc_vec_Vec_len (T: Type) (v: alloc_vec_Vec T) : usize := + exist _ (alloc_vec_Vec_length v) (alloc_vec_Vec_len_in_usize v). + +Fixpoint list_update {A} (l: list A) (n: nat) (a: A) + : list A := + match l with + | [] => [] + | x :: t => match n with + | 0%nat => a :: t + | S m => x :: (list_update t m a) +end end. + +Definition alloc_vec_Vec_bind {A B} (v: alloc_vec_Vec A) (f: list A -> result (list B)) : result (alloc_vec_Vec B) := + l <- f (alloc_vec_Vec_to_list v) ; + match sumbool_of_bool (scalar_le_max Usize (Z.of_nat (length l))) with + | left H => Return (exist _ l (scalar_le_max_valid _ _ H)) + | right _ => Fail_ Failure + end. + +(* The **forward** function shouldn't be used *) +Definition alloc_vec_Vec_push_fwd (T: Type) (v: alloc_vec_Vec T) (x: T) : unit := tt. + +Definition alloc_vec_Vec_push (T: Type) (v: alloc_vec_Vec T) (x: T) : result (alloc_vec_Vec T) := + alloc_vec_Vec_bind v (fun l => Return (l ++ [x])). + +(* The **forward** function shouldn't be used *) +Definition alloc_vec_Vec_insert_fwd (T: Type) (v: alloc_vec_Vec T) (i: usize) (x: T) : result unit := + if to_Z i <? alloc_vec_Vec_length v then Return tt else Fail_ Failure. + +Definition alloc_vec_Vec_insert (T: Type) (v: alloc_vec_Vec T) (i: usize) (x: T) : result (alloc_vec_Vec T) := + alloc_vec_Vec_bind v (fun l => + if to_Z i <? Z.of_nat (length l) + then Return (list_update l (usize_to_nat i) x) + else Fail_ Failure). + +(* Helper *) +Axiom alloc_vec_Vec_index_usize : forall {T : Type} (v : alloc_vec_Vec T) (i : usize) (x : T), result T. + +(* Helper *) +Axiom alloc_vec_Vec_update_usize : forall {T : Type} (v : alloc_vec_Vec T) (i : usize) (x : T), result (alloc_vec_Vec T). + +(* Trait declaration: [core::slice::index::private_slice_index::Sealed] *) +Definition core_slice_index_private_slice_index_Sealed (self : Type) := unit. + +(* Trait declaration: [core::slice::index::SliceIndex] *) +Record core_slice_index_SliceIndex (Self T : Type) := mk_core_slice_index_SliceIndex { + core_slice_index_SliceIndex_sealedInst : core_slice_index_private_slice_index_Sealed Self; + core_slice_index_SliceIndex_Output : Type; + core_slice_index_SliceIndex_get : Self -> T -> result (option core_slice_index_SliceIndex_Output); + core_slice_index_SliceIndex_get_mut : Self -> T -> result (option core_slice_index_SliceIndex_Output); + core_slice_index_SliceIndex_get_mut_back : Self -> T -> option core_slice_index_SliceIndex_Output -> result T; + core_slice_index_SliceIndex_get_unchecked : Self -> const_raw_ptr T -> result (const_raw_ptr core_slice_index_SliceIndex_Output); + core_slice_index_SliceIndex_get_unchecked_mut : Self -> mut_raw_ptr T -> result (mut_raw_ptr core_slice_index_SliceIndex_Output); + core_slice_index_SliceIndex_index : Self -> T -> result core_slice_index_SliceIndex_Output; + core_slice_index_SliceIndex_index_mut : Self -> T -> result core_slice_index_SliceIndex_Output; + core_slice_index_SliceIndex_index_mut_back : Self -> T -> core_slice_index_SliceIndex_Output -> result T; +}. +Arguments mk_core_slice_index_SliceIndex {_ _}. +Arguments core_slice_index_SliceIndex_sealedInst {_ _}. +Arguments core_slice_index_SliceIndex_Output {_ _}. +Arguments core_slice_index_SliceIndex_get {_ _}. +Arguments core_slice_index_SliceIndex_get_mut {_ _}. +Arguments core_slice_index_SliceIndex_get_mut_back {_ _}. +Arguments core_slice_index_SliceIndex_get_unchecked {_ _}. +Arguments core_slice_index_SliceIndex_get_unchecked_mut {_ _}. +Arguments core_slice_index_SliceIndex_index {_ _}. +Arguments core_slice_index_SliceIndex_index_mut {_ _}. +Arguments core_slice_index_SliceIndex_index_mut_back {_ _}. + +(* [core::slice::index::[T]::index]: forward function *) +Definition core_slice_index_Slice_index + (T Idx : Type) (inst : core_slice_index_SliceIndex Idx (slice T)) + (s : slice T) (i : Idx) : result inst.(core_slice_index_SliceIndex_Output) := + x <- inst.(core_slice_index_SliceIndex_get) i s; + match x with + | None => Fail_ Failure + | Some x => Return x + end. + +(* [core::slice::index::Range:::get]: forward function *) +Axiom core_slice_index_Range_get : forall (T : Type) (i : core_ops_range_Range usize) (s : slice T), result (option (slice T)). + +(* [core::slice::index::Range::get_mut]: forward function *) +Axiom core_slice_index_Range_get_mut : + forall (T : Type), core_ops_range_Range usize -> slice T -> result (option (slice T)). + +(* [core::slice::index::Range::get_mut]: backward function 0 *) +Axiom core_slice_index_Range_get_mut_back : + forall (T : Type), core_ops_range_Range usize -> slice T -> option (slice T) -> result (slice T). + +(* [core::slice::index::Range::get_unchecked]: forward function *) +Definition core_slice_index_Range_get_unchecked + (T : Type) : + core_ops_range_Range usize -> const_raw_ptr (slice T) -> result (const_raw_ptr (slice T)) := + (* Don't know what the model should be - for now we always fail to make + sure code which uses it fails *) + fun _ _ => Fail_ Failure. + +(* [core::slice::index::Range::get_unchecked_mut]: forward function *) +Definition core_slice_index_Range_get_unchecked_mut + (T : Type) : + core_ops_range_Range usize -> mut_raw_ptr (slice T) -> result (mut_raw_ptr (slice T)) := + (* Don't know what the model should be - for now we always fail to make + sure code which uses it fails *) + fun _ _ => Fail_ Failure. + +(* [core::slice::index::Range::index]: forward function *) +Axiom core_slice_index_Range_index : + forall (T : Type), core_ops_range_Range usize -> slice T -> result (slice T). + +(* [core::slice::index::Range::index_mut]: forward function *) +Axiom core_slice_index_Range_index_mut : + forall (T : Type), core_ops_range_Range usize -> slice T -> result (slice T). + +(* [core::slice::index::Range::index_mut]: backward function 0 *) +Axiom core_slice_index_Range_index_mut_back : + forall (T : Type), core_ops_range_Range usize -> slice T -> slice T -> result (slice T). + +(* [core::slice::index::[T]::index_mut]: forward function *) +Axiom core_slice_index_Slice_index_mut : + forall (T Idx : Type) (inst : core_slice_index_SliceIndex Idx (slice T)), + slice T -> Idx -> result inst.(core_slice_index_SliceIndex_Output). + +(* [core::slice::index::[T]::index_mut]: backward function 0 *) +Axiom core_slice_index_Slice_index_mut_back : + forall (T Idx : Type) (inst : core_slice_index_SliceIndex Idx (slice T)), + slice T -> Idx -> inst.(core_slice_index_SliceIndex_Output) -> result (slice T). + +(* [core::array::[T; N]::index]: forward function *) +Axiom core_array_Array_index : + forall (T Idx : Type) (N : usize) (inst : core_ops_index_Index (slice T) Idx) + (a : array T N) (i : Idx), result inst.(core_ops_index_Index_Output). + +(* [core::array::[T; N]::index_mut]: forward function *) +Axiom core_array_Array_index_mut : + forall (T Idx : Type) (N : usize) (inst : core_ops_index_IndexMut (slice T) Idx) + (a : array T N) (i : Idx), result inst.(core_ops_index_IndexMut_indexInst).(core_ops_index_Index_Output). + +(* [core::array::[T; N]::index_mut]: backward function 0 *) +Axiom core_array_Array_index_mut_back : + forall (T Idx : Type) (N : usize) (inst : core_ops_index_IndexMut (slice T) Idx) + (a : array T N) (i : Idx) (x : inst.(core_ops_index_IndexMut_indexInst).(core_ops_index_Index_Output)), result (array T N). + +(* Trait implementation: [core::slice::index::[T]] *) +Definition core_slice_index_Slice_coreopsindexIndexInst (T Idx : Type) + (inst : core_slice_index_SliceIndex Idx (slice T)) : + core_ops_index_Index (slice T) Idx := {| + core_ops_index_Index_Output := inst.(core_slice_index_SliceIndex_Output); + core_ops_index_Index_index := core_slice_index_Slice_index T Idx inst; +|}. + +(* Trait implementation: [core::slice::index::private_slice_index::Range] *) +Definition core_slice_index_private_slice_index_Range_coresliceindexprivate_slice_indexSealedInst + : core_slice_index_private_slice_index_Sealed (core_ops_range_Range usize) := tt. + +(* Trait implementation: [core::slice::index::Range] *) +Definition core_slice_index_Range_coresliceindexSliceIndexInst (T : Type) : + core_slice_index_SliceIndex (core_ops_range_Range usize) (slice T) := {| + core_slice_index_SliceIndex_sealedInst := core_slice_index_private_slice_index_Range_coresliceindexprivate_slice_indexSealedInst; + core_slice_index_SliceIndex_Output := slice T; + core_slice_index_SliceIndex_get := core_slice_index_Range_get T; + core_slice_index_SliceIndex_get_mut := core_slice_index_Range_get_mut T; + core_slice_index_SliceIndex_get_mut_back := core_slice_index_Range_get_mut_back T; + core_slice_index_SliceIndex_get_unchecked := core_slice_index_Range_get_unchecked T; + core_slice_index_SliceIndex_get_unchecked_mut := core_slice_index_Range_get_unchecked_mut T; + core_slice_index_SliceIndex_index := core_slice_index_Range_index T; + core_slice_index_SliceIndex_index_mut := core_slice_index_Range_index_mut T; + core_slice_index_SliceIndex_index_mut_back := core_slice_index_Range_index_mut_back T; +|}. + +(* Trait implementation: [core::slice::index::[T]] *) +Definition core_slice_index_Slice_coreopsindexIndexMutInst (T Idx : Type) + (inst : core_slice_index_SliceIndex Idx (slice T)) : + core_ops_index_IndexMut (slice T) Idx := {| + core_ops_index_IndexMut_indexInst := core_slice_index_Slice_coreopsindexIndexInst T Idx inst; + core_ops_index_IndexMut_index_mut := core_slice_index_Slice_index_mut T Idx inst; + core_ops_index_IndexMut_index_mut_back := core_slice_index_Slice_index_mut_back T Idx inst; +|}. + +(* Trait implementation: [core::array::[T; N]] *) +Definition core_array_Array_coreopsindexIndexInst (T Idx : Type) (N : usize) + (inst : core_ops_index_Index (slice T) Idx) : + core_ops_index_Index (array T N) Idx := {| + core_ops_index_Index_Output := inst.(core_ops_index_Index_Output); + core_ops_index_Index_index := core_array_Array_index T Idx N inst; +|}. + +(* Trait implementation: [core::array::[T; N]] *) +Definition core_array_Array_coreopsindexIndexMutInst (T Idx : Type) (N : usize) + (inst : core_ops_index_IndexMut (slice T) Idx) : + core_ops_index_IndexMut (array T N) Idx := {| + core_ops_index_IndexMut_indexInst := core_array_Array_coreopsindexIndexInst T Idx N inst.(core_ops_index_IndexMut_indexInst); + core_ops_index_IndexMut_index_mut := core_array_Array_index_mut T Idx N inst; + core_ops_index_IndexMut_index_mut_back := core_array_Array_index_mut_back T Idx N inst; +|}. + +(* [core::slice::index::usize::get]: forward function *) +Axiom core_slice_index_usize_get : forall (T : Type), usize -> slice T -> result (option T). + +(* [core::slice::index::usize::get_mut]: forward function *) +Axiom core_slice_index_usize_get_mut : forall (T : Type), usize -> slice T -> result (option T). + +(* [core::slice::index::usize::get_mut]: backward function 0 *) +Axiom core_slice_index_usize_get_mut_back : + forall (T : Type), usize -> slice T -> option T -> result (slice T). + +(* [core::slice::index::usize::get_unchecked]: forward function *) +Axiom core_slice_index_usize_get_unchecked : + forall (T : Type), usize -> const_raw_ptr (slice T) -> result (const_raw_ptr T). + +(* [core::slice::index::usize::get_unchecked_mut]: forward function *) +Axiom core_slice_index_usize_get_unchecked_mut : + forall (T : Type), usize -> mut_raw_ptr (slice T) -> result (mut_raw_ptr T). + +(* [core::slice::index::usize::index]: forward function *) +Axiom core_slice_index_usize_index : forall (T : Type), usize -> slice T -> result T. + +(* [core::slice::index::usize::index_mut]: forward function *) +Axiom core_slice_index_usize_index_mut : forall (T : Type), usize -> slice T -> result T. + +(* [core::slice::index::usize::index_mut]: backward function 0 *) +Axiom core_slice_index_usize_index_mut_back : + forall (T : Type), usize -> slice T -> T -> result (slice T). + +(* Trait implementation: [core::slice::index::private_slice_index::usize] *) +Definition core_slice_index_private_slice_index_usize_coresliceindexprivate_slice_indexSealedInst + : core_slice_index_private_slice_index_Sealed usize := tt. + +(* Trait implementation: [core::slice::index::usize] *) +Definition core_slice_index_usize_coresliceindexSliceIndexInst (T : Type) : + core_slice_index_SliceIndex usize (slice T) := {| + core_slice_index_SliceIndex_sealedInst := core_slice_index_private_slice_index_usize_coresliceindexprivate_slice_indexSealedInst; + core_slice_index_SliceIndex_Output := T; + core_slice_index_SliceIndex_get := core_slice_index_usize_get T; + core_slice_index_SliceIndex_get_mut := core_slice_index_usize_get_mut T; + core_slice_index_SliceIndex_get_mut_back := core_slice_index_usize_get_mut_back T; + core_slice_index_SliceIndex_get_unchecked := core_slice_index_usize_get_unchecked T; + core_slice_index_SliceIndex_get_unchecked_mut := core_slice_index_usize_get_unchecked_mut T; + core_slice_index_SliceIndex_index := core_slice_index_usize_index T; + core_slice_index_SliceIndex_index_mut := core_slice_index_usize_index_mut T; + core_slice_index_SliceIndex_index_mut_back := core_slice_index_usize_index_mut_back T; +|}. + +(* [alloc::vec::Vec::index]: forward function *) +Axiom alloc_vec_Vec_index : forall (T Idx : Type) (inst : core_slice_index_SliceIndex Idx (slice T)) + (Self : alloc_vec_Vec T) (i : Idx), result inst.(core_slice_index_SliceIndex_Output). + +(* [alloc::vec::Vec::index_mut]: forward function *) +Axiom alloc_vec_Vec_index_mut : forall (T Idx : Type) (inst : core_slice_index_SliceIndex Idx (slice T)) + (Self : alloc_vec_Vec T) (i : Idx), result inst.(core_slice_index_SliceIndex_Output). + +(* [alloc::vec::Vec::index_mut]: backward function 0 *) +Axiom alloc_vec_Vec_index_mut_back : + forall (T Idx : Type) (inst : core_slice_index_SliceIndex Idx (slice T)) + (Self : alloc_vec_Vec T) (i : Idx) (x : inst.(core_slice_index_SliceIndex_Output)), result (alloc_vec_Vec T). + +(* Trait implementation: [alloc::vec::Vec] *) +Definition alloc_vec_Vec_coreopsindexIndexInst (T Idx : Type) + (inst : core_slice_index_SliceIndex Idx (slice T)) : + core_ops_index_Index (alloc_vec_Vec T) Idx := {| + core_ops_index_Index_Output := inst.(core_slice_index_SliceIndex_Output); + core_ops_index_Index_index := alloc_vec_Vec_index T Idx inst; +|}. + +(* Trait implementation: [alloc::vec::Vec] *) +Definition alloc_vec_Vec_coreopsindexIndexMutInst (T Idx : Type) + (inst : core_slice_index_SliceIndex Idx (slice T)) : + core_ops_index_IndexMut (alloc_vec_Vec T) Idx := {| + core_ops_index_IndexMut_indexInst := alloc_vec_Vec_coreopsindexIndexInst T Idx inst; + core_ops_index_IndexMut_index_mut := alloc_vec_Vec_index_mut T Idx inst; + core_ops_index_IndexMut_index_mut_back := alloc_vec_Vec_index_mut_back T Idx inst; +|}. + +(*** Theorems *) + +Axiom alloc_vec_Vec_index_mut_back_eq : forall {a : Type} (v : alloc_vec_Vec a) (i : usize) (x : a), + alloc_vec_Vec_index_mut_back a usize (core_slice_index_usize_coresliceindexSliceIndexInst a) v i x = + alloc_vec_Vec_update_usize v i x. + +End Primitives. diff --git a/tests/coq/traits/Traits.v b/tests/coq/traits/Traits.v new file mode 100644 index 00000000..e104fb66 --- /dev/null +++ b/tests/coq/traits/Traits.v @@ -0,0 +1,520 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [traits] *) +Require Import Primitives. +Import Primitives. +Require Import Coq.ZArith.ZArith. +Require Import List. +Import ListNotations. +Local Open Scope Primitives_scope. +Module Traits. + +(** Trait declaration: [traits::BoolTrait] *) +Record BoolTrait_t (Self : Type) := mkBoolTrait_t { + BoolTrait_t_get_bool : Self -> result bool; +}. + +Arguments mkBoolTrait_t { _ }. +Arguments BoolTrait_t_get_bool { _ }. + +(** [traits::Bool::{0}::get_bool]: forward function *) +Definition bool_get_bool (self : bool) : result bool := + Return self. + +(** Trait implementation: [traits::Bool::{0}] *) +Definition Bool_BoolTraitInst : BoolTrait_t bool := {| + BoolTrait_t_get_bool := bool_get_bool; +|}. + +(** [traits::BoolTrait::ret_true]: forward function *) +Definition boolTrait_ret_true + {Self : Type} (self_clause : BoolTrait_t Self) (self : Self) : result bool := + Return true +. + +(** [traits::test_bool_trait_bool]: forward function *) +Definition test_bool_trait_bool (x : bool) : result bool := + b <- bool_get_bool x; + if b then boolTrait_ret_true Bool_BoolTraitInst x else Return false +. + +(** [traits::Option::{1}::get_bool]: forward function *) +Definition option_get_bool (T : Type) (self : option T) : result bool := + match self with | None => Return false | Some t => Return true end +. + +(** Trait implementation: [traits::Option::{1}] *) +Definition Option_BoolTraitInst (T : Type) : BoolTrait_t (option T) := {| + BoolTrait_t_get_bool := option_get_bool T; +|}. + +(** [traits::test_bool_trait_option]: forward function *) +Definition test_bool_trait_option (T : Type) (x : option T) : result bool := + b <- option_get_bool T x; + if b then boolTrait_ret_true (Option_BoolTraitInst T) x else Return false +. + +(** [traits::test_bool_trait]: forward function *) +Definition test_bool_trait + (T : Type) (inst : BoolTrait_t T) (x : T) : result bool := + inst.(BoolTrait_t_get_bool) x +. + +(** Trait declaration: [traits::ToU64] *) +Record ToU64_t (Self : Type) := mkToU64_t { + ToU64_t_to_u64 : Self -> result u64; +}. + +Arguments mkToU64_t { _ }. +Arguments ToU64_t_to_u64 { _ }. + +(** [traits::u64::{2}::to_u64]: forward function *) +Definition u64_to_u64 (self : u64) : result u64 := + Return self. + +(** Trait implementation: [traits::u64::{2}] *) +Definition u64_ToU64Inst : ToU64_t u64 := {| ToU64_t_to_u64 := u64_to_u64; |}. + +(** [traits::Tuple2::{3}::to_u64]: forward function *) +Definition tuple2_to_u64 + (A : Type) (inst : ToU64_t A) (self : (A * A)) : result u64 := + let (t, t0) := self in + i <- inst.(ToU64_t_to_u64) t; + i0 <- inst.(ToU64_t_to_u64) t0; + u64_add i i0 +. + +(** Trait implementation: [traits::Tuple2::{3}] *) +Definition Tuple2_ToU64Inst (A : Type) (inst : ToU64_t A) : ToU64_t (A * A) + := {| + ToU64_t_to_u64 := tuple2_to_u64 A inst; +|}. + +(** [traits::f]: forward function *) +Definition f (T : Type) (inst : ToU64_t T) (x : (T * T)) : result u64 := + tuple2_to_u64 T inst x +. + +(** [traits::g]: forward function *) +Definition g (T : Type) (inst : ToU64_t (T * T)) (x : (T * T)) : result u64 := + inst.(ToU64_t_to_u64) x +. + +(** [traits::h0]: forward function *) +Definition h0 (x : u64) : result u64 := + u64_to_u64 x. + +(** [traits::Wrapper] *) +Record Wrapper_t (T : Type) := mkWrapper_t { wrapper_x : T; }. + +Arguments mkWrapper_t { _ }. +Arguments wrapper_x { _ }. + +(** [traits::Wrapper::{4}::to_u64]: forward function *) +Definition wrapper_to_u64 + (T : Type) (inst : ToU64_t T) (self : Wrapper_t T) : result u64 := + inst.(ToU64_t_to_u64) self.(wrapper_x) +. + +(** Trait implementation: [traits::Wrapper::{4}] *) +Definition Wrapper_ToU64Inst (T : Type) (inst : ToU64_t T) : ToU64_t (Wrapper_t + T) := {| + ToU64_t_to_u64 := wrapper_to_u64 T inst; +|}. + +(** [traits::h1]: forward function *) +Definition h1 (x : Wrapper_t u64) : result u64 := + wrapper_to_u64 u64 u64_ToU64Inst x +. + +(** [traits::h2]: forward function *) +Definition h2 (T : Type) (inst : ToU64_t T) (x : Wrapper_t T) : result u64 := + wrapper_to_u64 T inst x +. + +(** Trait declaration: [traits::ToType] *) +Record ToType_t (Self T : Type) := mkToType_t { + ToType_t_to_type : Self -> result T; +}. + +Arguments mkToType_t { _ _ }. +Arguments ToType_t_to_type { _ _ }. + +(** [traits::u64::{5}::to_type]: forward function *) +Definition u64_to_type (self : u64) : result bool := + Return (self s> 0%u64). + +(** Trait implementation: [traits::u64::{5}] *) +Definition u64_ToTypeInst : ToType_t u64 bool := {| + ToType_t_to_type := u64_to_type; +|}. + +(** Trait declaration: [traits::OfType] *) +Record OfType_t (Self : Type) := mkOfType_t { + OfType_t_of_type : forall (T : Type) (inst : ToType_t T Self), T -> result + Self; +}. + +Arguments mkOfType_t { _ }. +Arguments OfType_t_of_type { _ }. + +(** [traits::h3]: forward function *) +Definition h3 + (T1 T2 : Type) (inst : OfType_t T1) (inst0 : ToType_t T2 T1) (y : T2) : + result T1 + := + inst.(OfType_t_of_type) T2 inst0 y +. + +(** Trait declaration: [traits::OfTypeBis] *) +Record OfTypeBis_t (Self T : Type) := mkOfTypeBis_t { + OfTypeBis_tOfTypeBis_t_parent_clause_0 : ToType_t T Self; + OfTypeBis_t_of_type : T -> result Self; +}. + +Arguments mkOfTypeBis_t { _ _ }. +Arguments OfTypeBis_tOfTypeBis_t_parent_clause_0 { _ _ }. +Arguments OfTypeBis_t_of_type { _ _ }. + +(** [traits::h4]: forward function *) +Definition h4 + (T1 T2 : Type) (inst : OfTypeBis_t T1 T2) (inst0 : ToType_t T2 T1) (y : T2) : + result T1 + := + inst.(OfTypeBis_t_of_type) y +. + +(** [traits::TestType] *) +Record TestType_t (T : Type) := mkTestType_t { testType_0 : T; }. + +Arguments mkTestType_t { _ }. +Arguments testType_0 { _ }. + +(** [traits::TestType::{6}::test::TestType1] *) +Record TestType_test_TestType1_t := +mkTestType_test_TestType1_t { + testType_test_TestType1_0 : u64; +} +. + +(** Trait declaration: [traits::TestType::{6}::test::TestTrait] *) +Record TestType_test_TestTrait_t (Self : Type) := mkTestType_test_TestTrait_t { + TestType_test_TestTrait_t_test : Self -> result bool; +}. + +Arguments mkTestType_test_TestTrait_t { _ }. +Arguments TestType_test_TestTrait_t_test { _ }. + +(** [traits::TestType::{6}::test::TestType1::{0}::test]: forward function *) +Definition testType_test_TestType1_test + (self : TestType_test_TestType1_t) : result bool := + Return (self.(testType_test_TestType1_0) s> 1%u64) +. + +(** Trait implementation: [traits::TestType::{6}::test::TestType1::{0}] *) +Definition TestType_test_TestType1_TestType_test_TestTraitInst : + TestType_test_TestTrait_t TestType_test_TestType1_t := {| + TestType_test_TestTrait_t_test := testType_test_TestType1_test; +|}. + +(** [traits::TestType::{6}::test]: forward function *) +Definition testType_test + (T : Type) (inst : ToU64_t T) (self : TestType_t T) (x : T) : result bool := + x0 <- inst.(ToU64_t_to_u64) x; + if x0 s> 0%u64 + then testType_test_TestType1_test {| testType_test_TestType1_0 := 0%u64 |} + else Return false +. + +(** [traits::BoolWrapper] *) +Record BoolWrapper_t := mkBoolWrapper_t { boolWrapper_0 : bool; }. + +(** [traits::BoolWrapper::{7}::to_type]: forward function *) +Definition boolWrapper_to_type + (T : Type) (inst : ToType_t bool T) (self : BoolWrapper_t) : result T := + inst.(ToType_t_to_type) self.(boolWrapper_0) +. + +(** Trait implementation: [traits::BoolWrapper::{7}] *) +Definition BoolWrapper_ToTypeInst (T : Type) (inst : ToType_t bool T) : + ToType_t BoolWrapper_t T := {| + ToType_t_to_type := boolWrapper_to_type T inst; +|}. + +(** [traits::WithConstTy::LEN2] *) +Definition with_const_ty_len2_body : result usize := Return 32%usize. +Definition with_const_ty_len2_c : usize := with_const_ty_len2_body%global. + +(** Trait declaration: [traits::WithConstTy] *) +Record WithConstTy_t (Self : Type) (LEN : usize) := mkWithConstTy_t { + WithConstTy_tWithConstTy_t_LEN1 : usize; + WithConstTy_tWithConstTy_t_LEN2 : usize; + WithConstTy_tWithConstTy_t_V : Type; + WithConstTy_tWithConstTy_t_W : Type; + WithConstTy_tWithConstTy_t_W_clause_0 : ToU64_t WithConstTy_tWithConstTy_t_W; + WithConstTy_t_f : WithConstTy_tWithConstTy_t_W -> array u8 LEN -> result + WithConstTy_tWithConstTy_t_W; +}. + +Arguments mkWithConstTy_t { _ _ }. +Arguments WithConstTy_tWithConstTy_t_LEN1 { _ _ }. +Arguments WithConstTy_tWithConstTy_t_LEN2 { _ _ }. +Arguments WithConstTy_tWithConstTy_t_V { _ _ }. +Arguments WithConstTy_tWithConstTy_t_W { _ _ }. +Arguments WithConstTy_tWithConstTy_t_W_clause_0 { _ _ }. +Arguments WithConstTy_t_f { _ _ }. + +(** [traits::Bool::{8}::LEN1] *) +Definition bool_len1_body : result usize := Return 12%usize. +Definition bool_len1_c : usize := bool_len1_body%global. + +(** [traits::Bool::{8}::f]: merged forward/backward function + (there is a single backward function, and the forward function returns ()) *) +Definition bool_f (i : u64) (a : array u8 32%usize) : result u64 := + Return i. + +(** Trait implementation: [traits::Bool::{8}] *) +Definition Bool_WithConstTyInst : WithConstTy_t bool 32%usize := {| + WithConstTy_tWithConstTy_t_LEN1 := bool_len1_c; + WithConstTy_tWithConstTy_t_LEN2 := with_const_ty_len2_c; + WithConstTy_tWithConstTy_t_V := u8; + WithConstTy_tWithConstTy_t_W := u64; + WithConstTy_tWithConstTy_t_W_clause_0 := u64_ToU64Inst; + WithConstTy_t_f := bool_f; +|}. + +(** [traits::use_with_const_ty1]: forward function *) +Definition use_with_const_ty1 + (H : Type) (LEN : usize) (inst : WithConstTy_t H LEN) : result usize := + let i := inst.(WithConstTy_tWithConstTy_t_LEN1) in Return i +. + +(** [traits::use_with_const_ty2]: forward function *) +Definition use_with_const_ty2 + (H : Type) (LEN : usize) (inst : WithConstTy_t H LEN) + (w : inst.(WithConstTy_tWithConstTy_t_W)) : + result unit + := + Return tt +. + +(** [traits::use_with_const_ty3]: forward function *) +Definition use_with_const_ty3 + (H : Type) (LEN : usize) (inst : WithConstTy_t H LEN) + (x : inst.(WithConstTy_tWithConstTy_t_W)) : + result u64 + := + inst.(WithConstTy_tWithConstTy_t_W_clause_0).(ToU64_t_to_u64) x +. + +(** [traits::test_where1]: forward function *) +Definition test_where1 (T : Type) (_x : T) : result unit := + Return tt. + +(** [traits::test_where2]: forward function *) +Definition test_where2 + (T : Type) (inst : WithConstTy_t T 32%usize) (_x : u32) : result unit := + Return tt +. + +(** [alloc::string::String] *) +Axiom alloc_string_String_t : Type. + +(** Trait declaration: [traits::ParentTrait0] *) +Record ParentTrait0_t (Self : Type) := mkParentTrait0_t { + ParentTrait0_tParentTrait0_t_W : Type; + ParentTrait0_t_get_name : Self -> result alloc_string_String_t; + ParentTrait0_t_get_w : Self -> result ParentTrait0_tParentTrait0_t_W; +}. + +Arguments mkParentTrait0_t { _ }. +Arguments ParentTrait0_tParentTrait0_t_W { _ }. +Arguments ParentTrait0_t_get_name { _ }. +Arguments ParentTrait0_t_get_w { _ }. + +(** Trait declaration: [traits::ParentTrait1] *) +Record ParentTrait1_t (Self : Type) := mkParentTrait1_t{}. + +Arguments mkParentTrait1_t { _ }. + +(** Trait declaration: [traits::ChildTrait] *) +Record ChildTrait_t (Self : Type) := mkChildTrait_t { + ChildTrait_tChildTrait_t_parent_clause_0 : ParentTrait0_t Self; + ChildTrait_tChildTrait_t_parent_clause_1 : ParentTrait1_t Self; +}. + +Arguments mkChildTrait_t { _ }. +Arguments ChildTrait_tChildTrait_t_parent_clause_0 { _ }. +Arguments ChildTrait_tChildTrait_t_parent_clause_1 { _ }. + +(** [traits::test_child_trait1]: forward function *) +Definition test_child_trait1 + (T : Type) (inst : ChildTrait_t T) (x : T) : result alloc_string_String_t := + inst.(ChildTrait_tChildTrait_t_parent_clause_0).(ParentTrait0_t_get_name) x +. + +(** [traits::test_child_trait2]: forward function *) +Definition test_child_trait2 + (T : Type) (inst : ChildTrait_t T) (x : T) : + result + inst.(ChildTrait_tChildTrait_t_parent_clause_0).(ParentTrait0_tParentTrait0_t_W) + := + inst.(ChildTrait_tChildTrait_t_parent_clause_0).(ParentTrait0_t_get_w) x +. + +(** [traits::order1]: forward function *) +Definition order1 + (T U : Type) (inst : ParentTrait0_t T) (inst0 : ParentTrait0_t U) : + result unit + := + Return tt +. + +(** Trait declaration: [traits::ChildTrait1] *) +Record ChildTrait1_t (Self : Type) := mkChildTrait1_t { + ChildTrait1_tChildTrait1_t_parent_clause_0 : ParentTrait1_t Self; +}. + +Arguments mkChildTrait1_t { _ }. +Arguments ChildTrait1_tChildTrait1_t_parent_clause_0 { _ }. + +(** Trait implementation: [traits::usize::{9}] *) +Definition usize_ParentTrait1Inst : ParentTrait1_t usize := mkParentTrait1_t. + +(** Trait implementation: [traits::usize::{10}] *) +Definition usize_ChildTrait1Inst : ChildTrait1_t usize := {| + ChildTrait1_tChildTrait1_t_parent_clause_0 := usize_ParentTrait1Inst; +|}. + +(** Trait declaration: [traits::Iterator] *) +Record Iterator_t (Self : Type) := mkIterator_t { + Iterator_tIterator_t_Item : Type; +}. + +Arguments mkIterator_t { _ }. +Arguments Iterator_tIterator_t_Item { _ }. + +(** Trait declaration: [traits::IntoIterator] *) +Record IntoIterator_t (Self : Type) := mkIntoIterator_t { + IntoIterator_tIntoIterator_t_Item : Type; + IntoIterator_tIntoIterator_t_IntoIter : Type; + IntoIterator_tIntoIterator_t_IntoIter_clause_0 : Iterator_t + IntoIterator_tIntoIterator_t_IntoIter; + IntoIterator_t_into_iter : Self -> result + IntoIterator_tIntoIterator_t_IntoIter; +}. + +Arguments mkIntoIterator_t { _ }. +Arguments IntoIterator_tIntoIterator_t_Item { _ }. +Arguments IntoIterator_tIntoIterator_t_IntoIter { _ }. +Arguments IntoIterator_tIntoIterator_t_IntoIter_clause_0 { _ }. +Arguments IntoIterator_t_into_iter { _ }. + +(** Trait declaration: [traits::FromResidual] *) +Record FromResidual_t (Self T : Type) := mkFromResidual_t{}. + +Arguments mkFromResidual_t { _ _ }. + +(** Trait declaration: [traits::Try] *) +Record Try_t (Self : Type) := mkTry_t { + Try_tTry_t_Residual : Type; + Try_tTry_t_parent_clause_0 : FromResidual_t Self Try_tTry_t_Residual; +}. + +Arguments mkTry_t { _ }. +Arguments Try_tTry_t_Residual { _ }. +Arguments Try_tTry_t_parent_clause_0 { _ }. + +(** Trait declaration: [traits::WithTarget] *) +Record WithTarget_t (Self : Type) := mkWithTarget_t { + WithTarget_tWithTarget_t_Target : Type; +}. + +Arguments mkWithTarget_t { _ }. +Arguments WithTarget_tWithTarget_t_Target { _ }. + +(** Trait declaration: [traits::ParentTrait2] *) +Record ParentTrait2_t (Self : Type) := mkParentTrait2_t { + ParentTrait2_tParentTrait2_t_U : Type; + ParentTrait2_tParentTrait2_t_U_clause_0 : WithTarget_t + ParentTrait2_tParentTrait2_t_U; +}. + +Arguments mkParentTrait2_t { _ }. +Arguments ParentTrait2_tParentTrait2_t_U { _ }. +Arguments ParentTrait2_tParentTrait2_t_U_clause_0 { _ }. + +(** Trait declaration: [traits::ChildTrait2] *) +Record ChildTrait2_t (Self : Type) := mkChildTrait2_t { + ChildTrait2_tChildTrait2_t_parent_clause_0 : ParentTrait2_t Self; + ChildTrait2_t_convert : + (ChildTrait2_tChildTrait2_t_parent_clause_0).(ParentTrait2_tParentTrait2_t_U) + -> result + (ChildTrait2_tChildTrait2_t_parent_clause_0).(ParentTrait2_tParentTrait2_t_U_clause_0).(WithTarget_tWithTarget_t_Target); +}. + +Arguments mkChildTrait2_t { _ }. +Arguments ChildTrait2_tChildTrait2_t_parent_clause_0 { _ }. +Arguments ChildTrait2_t_convert { _ }. + +(** Trait implementation: [traits::u32::{11}] *) +Definition u32_WithTargetInst : WithTarget_t u32 := {| + WithTarget_tWithTarget_t_Target := u32; +|}. + +(** Trait implementation: [traits::u32::{12}] *) +Definition u32_ParentTrait2Inst : ParentTrait2_t u32 := {| + ParentTrait2_tParentTrait2_t_U := u32; + ParentTrait2_tParentTrait2_t_U_clause_0 := u32_WithTargetInst; +|}. + +(** [traits::u32::{13}::convert]: forward function *) +Definition u32_convert (x : u32) : result u32 := + Return x. + +(** Trait implementation: [traits::u32::{13}] *) +Definition u32_ChildTrait2Inst : ChildTrait2_t u32 := {| + ChildTrait2_tChildTrait2_t_parent_clause_0 := u32_ParentTrait2Inst; + ChildTrait2_t_convert := u32_convert; +|}. + +(** [traits::incr_u32]: forward function *) +Definition incr_u32 (x : u32) : result u32 := + u32_add x 1%u32. + +(** Trait declaration: [traits::CFnOnce] *) +Record CFnOnce_t (Self Args : Type) := mkCFnOnce_t { + CFnOnce_tCFnOnce_t_Output : Type; + CFnOnce_t_call_once : Self -> Args -> result CFnOnce_tCFnOnce_t_Output; +}. + +Arguments mkCFnOnce_t { _ _ }. +Arguments CFnOnce_tCFnOnce_t_Output { _ _ }. +Arguments CFnOnce_t_call_once { _ _ }. + +(** Trait declaration: [traits::CFnMut] *) +Record CFnMut_t (Self Args : Type) := mkCFnMut_t { + CFnMut_tCFnMut_t_parent_clause_0 : CFnOnce_t Self Args; + CFnMut_t_call_mut : Self -> Args -> result + (CFnMut_tCFnMut_t_parent_clause_0).(CFnOnce_tCFnOnce_t_Output); + CFnMut_t_call_mut_back : Self -> Args -> + (CFnMut_tCFnMut_t_parent_clause_0).(CFnOnce_tCFnOnce_t_Output) -> result + Self; +}. + +Arguments mkCFnMut_t { _ _ }. +Arguments CFnMut_tCFnMut_t_parent_clause_0 { _ _ }. +Arguments CFnMut_t_call_mut { _ _ }. +Arguments CFnMut_t_call_mut_back { _ _ }. + +(** Trait declaration: [traits::CFn] *) +Record CFn_t (Self Args : Type) := mkCFn_t { + CFn_tCFn_t_parent_clause_0 : CFnMut_t Self Args; + CFn_t_call_mut : Self -> Args -> result + (CFn_tCFn_t_parent_clause_0).(CFnMut_tCFnMut_t_parent_clause_0).(CFnOnce_tCFnOnce_t_Output); +}. + +Arguments mkCFn_t { _ _ }. +Arguments CFn_tCFn_t_parent_clause_0 { _ _ }. +Arguments CFn_t_call_mut { _ _ }. + +End Traits . diff --git a/tests/coq/traits/_CoqProject b/tests/coq/traits/_CoqProject index d573657e..5b6199fc 100644 --- a/tests/coq/traits/_CoqProject +++ b/tests/coq/traits/_CoqProject @@ -3,3 +3,5 @@ -arg -w -arg all +Traits.v +Primitives.v |