Skip to content

Commit

Permalink
Fix minor mistakes
Browse files Browse the repository at this point in the history
  • Loading branch information
@sonmarcho
sonmarcho committed Sep 9, 2024
1 parent 19e6953 commit 653092b
Show file tree
Hide file tree
Showing 17 changed files with 138 additions and 138 deletions.
24 changes: 12 additions & 12 deletions backends/coq/Primitives.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -67,7 +67,7 @@ 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 * a := (x, x) .
Definition core_mem_replace {a : Type} (x : a) (y : a) : a * a := (x, x) .

Record mut_raw_ptr (T : Type) := { mut_raw_ptr_v : T }.
Record const_raw_ptr (T : Type) := { const_raw_ptr_v : T }.
Expand Down Expand Up @@ -676,7 +676,7 @@ Qed.
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_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).
Expand Down Expand Up @@ -944,7 +944,7 @@ Definition core_slice_index_private_slice_index_SealedUsizeInst
: core_slice_index_private_slice_index_Sealed usize := tt.

(* Trait implementation: [core::slice::index::usize] *)
Definition core_slice_index_SliceIndexUsizeSliceTInst {T : Type} :
Definition core_slice_index_SliceIndexUsizeSliceTInst (T : Type) :
core_slice_index_SliceIndex usize (slice T) := {|
core_slice_index_SliceIndex_sealedInst := core_slice_index_private_slice_index_SealedUsizeInst;
core_slice_index_SliceIndex_Output := T;
Expand All @@ -957,39 +957,39 @@ Definition core_slice_index_SliceIndexUsizeSliceTInst {T : Type} :
|}.

(* [alloc::vec::Vec::index]: forward function *)
Axiom alloc_vec_Vec_index : forall (T Idx : Type) (inst : core_slice_index_SliceIndex Idx (slice T))
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))
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) *
(inst.(core_slice_index_SliceIndex_Output) -> result (alloc_vec_Vec T))).

(* Trait implementation: [alloc::vec::Vec] *)
Definition alloc_vec_Vec_coreopsindexIndexInst (T Idx : Type)
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;
core_ops_index_Index_index := alloc_vec_Vec_index inst;
|}.

(* Trait implementation: [alloc::vec::Vec] *)
Definition alloc_vec_Vec_coreopsindexIndexMutInst (T Idx : Type)
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_indexInst := alloc_vec_Vec_coreopsindexIndexInst inst;
core_ops_index_IndexMut_index_mut := alloc_vec_Vec_index_mut inst;
|}.

(*** Theorems *)

Axiom alloc_vec_Vec_index_eq : forall {a : Type} (v : alloc_vec_Vec a) (i : usize) (x : a),
alloc_vec_Vec_index a usize core_slice_index_SliceIndexUsizeSliceTInst v i =
alloc_vec_Vec_index (core_slice_index_SliceIndexUsizeSliceTInst a) v i =
alloc_vec_Vec_index_usize v i.

Axiom alloc_vec_Vec_index_mut_eq : forall {a : Type} (v : alloc_vec_Vec a) (i : usize) (x : a),
alloc_vec_Vec_index_mut a usize core_slice_index_SliceIndexUsizeSliceTInst v i =
alloc_vec_Vec_index_mut (core_slice_index_SliceIndexUsizeSliceTInst a) v i =
alloc_vec_Vec_index_mut_usize v i.

End Primitives.
10 changes: 5 additions & 5 deletions backends/fstar/Primitives.fst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -887,7 +887,7 @@ let core_slice_index_private_slice_index_SealedUsizeInst
: core_slice_index_private_slice_index_Sealed usize = ()

// Trait implementation: [core::slice::index::usize]
let core_slice_index_SliceIndexUsizeSliceTInst (#t : Type0) :
let core_slice_index_SliceIndexUsizeSliceTInst (t : Type0) :
core_slice_index_SliceIndex usize (slice t) = {
sealedInst = core_slice_index_private_slice_index_SealedUsizeInst;
output = t;
Expand Down Expand Up @@ -930,16 +930,16 @@ let alloc_vec_Vec_coreopsindexIndexMutInst (#t #idx : Type0)

let alloc_vec_Vec_index_eq (#a : Type0) (v : alloc_vec_Vec a) (i : usize) :
Lemma (
alloc_vec_Vec_index core_slice_index_SliceIndexUsizeSliceTInst v i ==
alloc_vec_Vec_index (core_slice_index_SliceIndexUsizeSliceTInst a) v i ==
alloc_vec_Vec_index_usize v i)
[SMTPat (alloc_vec_Vec_index core_slice_index_SliceIndexUsizeSliceTInst v i)]
[SMTPat (alloc_vec_Vec_index (core_slice_index_SliceIndexUsizeSliceTInst a) v i)]
=
admit()

let alloc_vec_Vec_index_mut_eq (#a : Type0) (v : alloc_vec_Vec a) (i : usize) :
Lemma (
alloc_vec_Vec_index_mut core_slice_index_SliceIndexUsizeSliceTInst v i ==
alloc_vec_Vec_index_mut (core_slice_index_SliceIndexUsizeSliceTInst a) v i ==
alloc_vec_Vec_index_mut_usize v i)
[SMTPat (alloc_vec_Vec_index_mut core_slice_index_SliceIndexUsizeSliceTInst v i)]
[SMTPat (alloc_vec_Vec_index_mut (core_slice_index_SliceIndexUsizeSliceTInst a) v i)]
=
admit()
24 changes: 12 additions & 12 deletions tests/coq/arrays/Primitives.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -67,7 +67,7 @@ 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 * a := (x, x) .
Definition core_mem_replace {a : Type} (x : a) (y : a) : a * a := (x, x) .

Record mut_raw_ptr (T : Type) := { mut_raw_ptr_v : T }.
Record const_raw_ptr (T : Type) := { const_raw_ptr_v : T }.
Expand Down Expand Up @@ -676,7 +676,7 @@ Qed.
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_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).
Expand Down Expand Up @@ -944,7 +944,7 @@ Definition core_slice_index_private_slice_index_SealedUsizeInst
: core_slice_index_private_slice_index_Sealed usize := tt.

(* Trait implementation: [core::slice::index::usize] *)
Definition core_slice_index_SliceIndexUsizeSliceTInst {T : Type} :
Definition core_slice_index_SliceIndexUsizeSliceTInst (T : Type) :
core_slice_index_SliceIndex usize (slice T) := {|
core_slice_index_SliceIndex_sealedInst := core_slice_index_private_slice_index_SealedUsizeInst;
core_slice_index_SliceIndex_Output := T;
Expand All @@ -957,39 +957,39 @@ Definition core_slice_index_SliceIndexUsizeSliceTInst {T : Type} :
|}.

(* [alloc::vec::Vec::index]: forward function *)
Axiom alloc_vec_Vec_index : forall (T Idx : Type) (inst : core_slice_index_SliceIndex Idx (slice T))
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))
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) *
(inst.(core_slice_index_SliceIndex_Output) -> result (alloc_vec_Vec T))).

(* Trait implementation: [alloc::vec::Vec] *)
Definition alloc_vec_Vec_coreopsindexIndexInst (T Idx : Type)
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;
core_ops_index_Index_index := alloc_vec_Vec_index inst;
|}.

(* Trait implementation: [alloc::vec::Vec] *)
Definition alloc_vec_Vec_coreopsindexIndexMutInst (T Idx : Type)
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_indexInst := alloc_vec_Vec_coreopsindexIndexInst inst;
core_ops_index_IndexMut_index_mut := alloc_vec_Vec_index_mut inst;
|}.

(*** Theorems *)

Axiom alloc_vec_Vec_index_eq : forall {a : Type} (v : alloc_vec_Vec a) (i : usize) (x : a),
alloc_vec_Vec_index a usize core_slice_index_SliceIndexUsizeSliceTInst v i =
alloc_vec_Vec_index (core_slice_index_SliceIndexUsizeSliceTInst a) v i =
alloc_vec_Vec_index_usize v i.

Axiom alloc_vec_Vec_index_mut_eq : forall {a : Type} (v : alloc_vec_Vec a) (i : usize) (x : a),
alloc_vec_Vec_index_mut a usize core_slice_index_SliceIndexUsizeSliceTInst v i =
alloc_vec_Vec_index_mut (core_slice_index_SliceIndexUsizeSliceTInst a) v i =
alloc_vec_Vec_index_mut_usize v i.

End Primitives.
24 changes: 12 additions & 12 deletions tests/coq/betree/Primitives.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -67,7 +67,7 @@ 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 * a := (x, x) .
Definition core_mem_replace {a : Type} (x : a) (y : a) : a * a := (x, x) .

Record mut_raw_ptr (T : Type) := { mut_raw_ptr_v : T }.
Record const_raw_ptr (T : Type) := { const_raw_ptr_v : T }.
Expand Down Expand Up @@ -676,7 +676,7 @@ Qed.
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_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).
Expand Down Expand Up @@ -944,7 +944,7 @@ Definition core_slice_index_private_slice_index_SealedUsizeInst
: core_slice_index_private_slice_index_Sealed usize := tt.

(* Trait implementation: [core::slice::index::usize] *)
Definition core_slice_index_SliceIndexUsizeSliceTInst {T : Type} :
Definition core_slice_index_SliceIndexUsizeSliceTInst (T : Type) :
core_slice_index_SliceIndex usize (slice T) := {|
core_slice_index_SliceIndex_sealedInst := core_slice_index_private_slice_index_SealedUsizeInst;
core_slice_index_SliceIndex_Output := T;
Expand All @@ -957,39 +957,39 @@ Definition core_slice_index_SliceIndexUsizeSliceTInst {T : Type} :
|}.

(* [alloc::vec::Vec::index]: forward function *)
Axiom alloc_vec_Vec_index : forall (T Idx : Type) (inst : core_slice_index_SliceIndex Idx (slice T))
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))
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) *
(inst.(core_slice_index_SliceIndex_Output) -> result (alloc_vec_Vec T))).

(* Trait implementation: [alloc::vec::Vec] *)
Definition alloc_vec_Vec_coreopsindexIndexInst (T Idx : Type)
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;
core_ops_index_Index_index := alloc_vec_Vec_index inst;
|}.

(* Trait implementation: [alloc::vec::Vec] *)
Definition alloc_vec_Vec_coreopsindexIndexMutInst (T Idx : Type)
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_indexInst := alloc_vec_Vec_coreopsindexIndexInst inst;
core_ops_index_IndexMut_index_mut := alloc_vec_Vec_index_mut inst;
|}.

(*** Theorems *)

Axiom alloc_vec_Vec_index_eq : forall {a : Type} (v : alloc_vec_Vec a) (i : usize) (x : a),
alloc_vec_Vec_index a usize core_slice_index_SliceIndexUsizeSliceTInst v i =
alloc_vec_Vec_index (core_slice_index_SliceIndexUsizeSliceTInst a) v i =
alloc_vec_Vec_index_usize v i.

Axiom alloc_vec_Vec_index_mut_eq : forall {a : Type} (v : alloc_vec_Vec a) (i : usize) (x : a),
alloc_vec_Vec_index_mut a usize core_slice_index_SliceIndexUsizeSliceTInst v i =
alloc_vec_Vec_index_mut (core_slice_index_SliceIndexUsizeSliceTInst a) v i =
alloc_vec_Vec_index_mut_usize v i.

End Primitives.
24 changes: 12 additions & 12 deletions tests/coq/demo/Primitives.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -67,7 +67,7 @@ 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 * a := (x, x) .
Definition core_mem_replace {a : Type} (x : a) (y : a) : a * a := (x, x) .

Record mut_raw_ptr (T : Type) := { mut_raw_ptr_v : T }.
Record const_raw_ptr (T : Type) := { const_raw_ptr_v : T }.
Expand Down Expand Up @@ -676,7 +676,7 @@ Qed.
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_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).
Expand Down Expand Up @@ -944,7 +944,7 @@ Definition core_slice_index_private_slice_index_SealedUsizeInst
: core_slice_index_private_slice_index_Sealed usize := tt.

(* Trait implementation: [core::slice::index::usize] *)
Definition core_slice_index_SliceIndexUsizeSliceTInst {T : Type} :
Definition core_slice_index_SliceIndexUsizeSliceTInst (T : Type) :
core_slice_index_SliceIndex usize (slice T) := {|
core_slice_index_SliceIndex_sealedInst := core_slice_index_private_slice_index_SealedUsizeInst;
core_slice_index_SliceIndex_Output := T;
Expand All @@ -957,39 +957,39 @@ Definition core_slice_index_SliceIndexUsizeSliceTInst {T : Type} :
|}.

(* [alloc::vec::Vec::index]: forward function *)
Axiom alloc_vec_Vec_index : forall (T Idx : Type) (inst : core_slice_index_SliceIndex Idx (slice T))
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))
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) *
(inst.(core_slice_index_SliceIndex_Output) -> result (alloc_vec_Vec T))).

(* Trait implementation: [alloc::vec::Vec] *)
Definition alloc_vec_Vec_coreopsindexIndexInst (T Idx : Type)
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;
core_ops_index_Index_index := alloc_vec_Vec_index inst;
|}.

(* Trait implementation: [alloc::vec::Vec] *)
Definition alloc_vec_Vec_coreopsindexIndexMutInst (T Idx : Type)
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_indexInst := alloc_vec_Vec_coreopsindexIndexInst inst;
core_ops_index_IndexMut_index_mut := alloc_vec_Vec_index_mut inst;
|}.

(*** Theorems *)

Axiom alloc_vec_Vec_index_eq : forall {a : Type} (v : alloc_vec_Vec a) (i : usize) (x : a),
alloc_vec_Vec_index a usize core_slice_index_SliceIndexUsizeSliceTInst v i =
alloc_vec_Vec_index (core_slice_index_SliceIndexUsizeSliceTInst a) v i =
alloc_vec_Vec_index_usize v i.

Axiom alloc_vec_Vec_index_mut_eq : forall {a : Type} (v : alloc_vec_Vec a) (i : usize) (x : a),
alloc_vec_Vec_index_mut a usize core_slice_index_SliceIndexUsizeSliceTInst v i =
alloc_vec_Vec_index_mut (core_slice_index_SliceIndexUsizeSliceTInst a) v i =
alloc_vec_Vec_index_mut_usize v i.

End Primitives.
Loading

0 comments on commit 653092b

Please sign in to comment.