summaryrefslogtreecommitdiff
path: root/tests/coq/hashmap
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/coq/hashmap/Hashmap_Funs.v2
-rw-r--r--tests/coq/hashmap/Hashmap_Types.v2
-rw-r--r--tests/coq/hashmap/Primitives.v55
-rw-r--r--tests/coq/hashmap_on_disk/HashmapMain_Funs.v2
-rw-r--r--tests/coq/hashmap_on_disk/HashmapMain_Opaque.v2
-rw-r--r--tests/coq/hashmap_on_disk/HashmapMain_Types.v2
-rw-r--r--tests/coq/hashmap_on_disk/Primitives.v55
7 files changed, 108 insertions, 12 deletions
diff --git a/tests/coq/hashmap/Hashmap_Funs.v b/tests/coq/hashmap/Hashmap_Funs.v
index c8630eb6..c412abcd 100644
--- a/tests/coq/hashmap/Hashmap_Funs.v
+++ b/tests/coq/hashmap/Hashmap_Funs.v
@@ -3,6 +3,8 @@
Require Import Primitives.
Import Primitives.
Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
Local Open Scope Primitives_scope.
Require Export Hashmap_Types.
Import Hashmap_Types.
diff --git a/tests/coq/hashmap/Hashmap_Types.v b/tests/coq/hashmap/Hashmap_Types.v
index ce6e7dab..dbde6be9 100644
--- a/tests/coq/hashmap/Hashmap_Types.v
+++ b/tests/coq/hashmap/Hashmap_Types.v
@@ -3,6 +3,8 @@
Require Import Primitives.
Import Primitives.
Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
Local Open Scope Primitives_scope.
Module Hashmap_Types.
diff --git a/tests/coq/hashmap/Primitives.v b/tests/coq/hashmap/Primitives.v
index ae961ac2..71a2d9c3 100644
--- a/tests/coq/hashmap/Primitives.v
+++ b/tests/coq/hashmap/Primitives.v
@@ -394,13 +394,15 @@ 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.
-(*** Vectors *)
-
-Definition vec T := { l: list T | Z.of_nat (length l) <= usize_max }.
+(*** Range *)
+Record range (T : Type) := mk_range {
+ start: T;
+ end_: T;
+}.
+Arguments mk_range {_}.
-Definition vec_to_list {T: Type} (v: vec T) : list T := proj1_sig v.
-
-Definition vec_length {T: Type} (v: vec T) : Z := Z.of_nat (length (vec_to_list v)).
+(*** 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.
@@ -409,6 +411,47 @@ Proof.
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.
+
+Axiom array_index_shared : forall (T : Type) (n : usize) (x : array T n) (i : usize), result T.
+Axiom array_index_mut_fwd : forall (T : Type) (n : usize) (x : array T n) (i : usize), result T.
+Axiom array_index_mut_back : 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_shared : forall (T : Type) (x : slice T) (i : usize), result T.
+Axiom slice_index_mut_fwd : forall (T : Type) (x : slice T) (i : usize), result T.
+Axiom slice_index_mut_back : forall (T : Type) (x : slice T) (i : usize) (nx : T), result (slice T).
+
+(*** Subslices *)
+
+Axiom array_to_slice_shared : forall (T : Type) (n : usize) (x : array T n), result (slice T).
+Axiom array_to_slice_mut_fwd : forall (T : Type) (n : usize) (x : array T n), result (slice T).
+Axiom array_to_slice_mut_back : forall (T : Type) (n : usize) (x : array T n) (s : slice T), result (array T n).
+
+Axiom array_subslice_shared: forall (T : Type) (n : usize) (x : array T n) (r : range usize), result (slice T).
+Axiom array_subslice_mut_fwd: forall (T : Type) (n : usize) (x : array T n) (r : range usize), result (slice T).
+Axiom array_subslice_mut_back: forall (T : Type) (n : usize) (x : array T n) (r : range usize) (ns : slice T), result (array T n).
+Axiom slice_subslice_shared: forall (T : Type) (x : slice T) (r : range usize), result (slice T).
+Axiom slice_subslice_mut_fwd: forall (T : Type) (x : slice T) (r : range usize), result (slice T).
+Axiom slice_subslice_mut_back: forall (T : Type) (x : slice T) (r : range usize) (ns : slice T), result (slice T).
+
+(*** Vectors *)
+
+Definition vec T := { l: list T | Z.of_nat (length l) <= usize_max }.
+
+Definition vec_to_list {T: Type} (v: vec T) : list T := proj1_sig v.
+
+Definition vec_length {T: Type} (v: vec T) : Z := Z.of_nat (length (vec_to_list v)).
+
Definition vec_new (T: Type) : vec T := (exist _ [] le_0_usize_max).
Lemma vec_len_in_usize {T} (v: vec T) : usize_min <= vec_length v <= usize_max.
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
index 1b7304cc..e6095fe1 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Funs.v
@@ -3,6 +3,8 @@
Require Import Primitives.
Import Primitives.
Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
Local Open Scope Primitives_scope.
Require Export HashmapMain_Types.
Import HashmapMain_Types.
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Opaque.v b/tests/coq/hashmap_on_disk/HashmapMain_Opaque.v
index 1ad9c697..2d17cc29 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Opaque.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Opaque.v
@@ -3,6 +3,8 @@
Require Import Primitives.
Import Primitives.
Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
Local Open Scope Primitives_scope.
Require Export HashmapMain_Types.
Import HashmapMain_Types.
diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Types.v b/tests/coq/hashmap_on_disk/HashmapMain_Types.v
index b92cbf3a..36aaaf25 100644
--- a/tests/coq/hashmap_on_disk/HashmapMain_Types.v
+++ b/tests/coq/hashmap_on_disk/HashmapMain_Types.v
@@ -3,6 +3,8 @@
Require Import Primitives.
Import Primitives.
Require Import Coq.ZArith.ZArith.
+Require Import List.
+Import ListNotations.
Local Open Scope Primitives_scope.
Module HashmapMain_Types.
diff --git a/tests/coq/hashmap_on_disk/Primitives.v b/tests/coq/hashmap_on_disk/Primitives.v
index ae961ac2..71a2d9c3 100644
--- a/tests/coq/hashmap_on_disk/Primitives.v
+++ b/tests/coq/hashmap_on_disk/Primitives.v
@@ -394,13 +394,15 @@ 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.
-(*** Vectors *)
-
-Definition vec T := { l: list T | Z.of_nat (length l) <= usize_max }.
+(*** Range *)
+Record range (T : Type) := mk_range {
+ start: T;
+ end_: T;
+}.
+Arguments mk_range {_}.
-Definition vec_to_list {T: Type} (v: vec T) : list T := proj1_sig v.
-
-Definition vec_length {T: Type} (v: vec T) : Z := Z.of_nat (length (vec_to_list v)).
+(*** 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.
@@ -409,6 +411,47 @@ Proof.
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.
+
+Axiom array_index_shared : forall (T : Type) (n : usize) (x : array T n) (i : usize), result T.
+Axiom array_index_mut_fwd : forall (T : Type) (n : usize) (x : array T n) (i : usize), result T.
+Axiom array_index_mut_back : 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_shared : forall (T : Type) (x : slice T) (i : usize), result T.
+Axiom slice_index_mut_fwd : forall (T : Type) (x : slice T) (i : usize), result T.
+Axiom slice_index_mut_back : forall (T : Type) (x : slice T) (i : usize) (nx : T), result (slice T).
+
+(*** Subslices *)
+
+Axiom array_to_slice_shared : forall (T : Type) (n : usize) (x : array T n), result (slice T).
+Axiom array_to_slice_mut_fwd : forall (T : Type) (n : usize) (x : array T n), result (slice T).
+Axiom array_to_slice_mut_back : forall (T : Type) (n : usize) (x : array T n) (s : slice T), result (array T n).
+
+Axiom array_subslice_shared: forall (T : Type) (n : usize) (x : array T n) (r : range usize), result (slice T).
+Axiom array_subslice_mut_fwd: forall (T : Type) (n : usize) (x : array T n) (r : range usize), result (slice T).
+Axiom array_subslice_mut_back: forall (T : Type) (n : usize) (x : array T n) (r : range usize) (ns : slice T), result (array T n).
+Axiom slice_subslice_shared: forall (T : Type) (x : slice T) (r : range usize), result (slice T).
+Axiom slice_subslice_mut_fwd: forall (T : Type) (x : slice T) (r : range usize), result (slice T).
+Axiom slice_subslice_mut_back: forall (T : Type) (x : slice T) (r : range usize) (ns : slice T), result (slice T).
+
+(*** Vectors *)
+
+Definition vec T := { l: list T | Z.of_nat (length l) <= usize_max }.
+
+Definition vec_to_list {T: Type} (v: vec T) : list T := proj1_sig v.
+
+Definition vec_length {T: Type} (v: vec T) : Z := Z.of_nat (length (vec_to_list v)).
+
Definition vec_new (T: Type) : vec T := (exist _ [] le_0_usize_max).
Lemma vec_len_in_usize {T} (v: vec T) : usize_min <= vec_length v <= usize_max.
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-27 12:13:16 +0000