summaryrefslogtreecommitdiff
path: root/backends/lean
diff options
context:
space:
mode:
authorSon HO2023-11-22 15:06:43 +0100
committerGitHub2023-11-22 15:06:43 +0100
commitbacf3f5f6f5f6a9aa650d5ae8d12a132fd747039 (patch)
tree9953d7af1fe406cdc750030a43a5e4d6245cd763 /backends/lean
parent587f1ebc0178acb19029d3fc9a729c197082aba7 (diff)
parent01cfd899119174ef7c5941c99dd251711f4ee701 (diff)
Merge pull request #45 from AeneasVerif/son_merge_types
Big cleanup
Diffstat (limited to '')
-rw-r--r--backends/lean/Base/Primitives/Alloc.lean6
-rw-r--r--backends/lean/Base/Primitives/ArraySlice.lean71
-rw-r--r--backends/lean/Base/Primitives/Vec.lean6
3 files changed, 41 insertions, 42 deletions
diff --git a/backends/lean/Base/Primitives/Alloc.lean b/backends/lean/Base/Primitives/Alloc.lean
index 34590499..6c89c6bb 100644
--- a/backends/lean/Base/Primitives/Alloc.lean
+++ b/backends/lean/Base/Primitives/Alloc.lean
@@ -16,16 +16,16 @@ def deref_mut (T : Type) (x : T) : Result T := ret x
def deref_mut_back (T : Type) (_ : T) (x : T) : Result T := ret x
/-- Trait instance -/
-def coreOpsDerefInst (Self : Type) :
+def coreopsDerefInst (Self : Type) :
core.ops.deref.Deref Self := {
Target := Self
deref := deref Self
}
/-- Trait instance -/
-def coreOpsDerefMutInst (Self : Type) :
+def coreopsDerefMutInst (Self : Type) :
core.ops.deref.DerefMut Self := {
- derefInst := coreOpsDerefInst Self
+ derefInst := coreopsDerefInst Self
deref_mut := deref_mut Self
deref_mut_back := deref_mut_back Self
}
diff --git a/backends/lean/Base/Primitives/ArraySlice.lean b/backends/lean/Base/Primitives/ArraySlice.lean
index cfc9a6b2..f68c0846 100644
--- a/backends/lean/Base/Primitives/ArraySlice.lean
+++ b/backends/lean/Base/Primitives/ArraySlice.lean
@@ -363,23 +363,23 @@ def core.slice.index.Slice.index
| some x => ret x
/- [core::slice::index::Range:::get]: forward function -/
-def core.slice.index.Range.get (T : Type) (i : Range Usize) (slice : Slice T) :
+def core.slice.index.RangeUsize.get (T : Type) (i : Range Usize) (slice : Slice T) :
Result (Option (Slice T)) :=
sorry -- TODO
/- [core::slice::index::Range::get_mut]: forward function -/
-def core.slice.index.Range.get_mut
+def core.slice.index.RangeUsize.get_mut
(T : Type) : Range Usize → Slice T → Result (Option (Slice T)) :=
sorry -- TODO
/- [core::slice::index::Range::get_mut]: backward function 0 -/
-def core.slice.index.Range.get_mut_back
+def core.slice.index.RangeUsize.get_mut_back
(T : Type) :
Range Usize → Slice T → Option (Slice T) → Result (Slice T) :=
sorry -- TODO
/- [core::slice::index::Range::get_unchecked]: forward function -/
-def core.slice.index.Range.get_unchecked
+def core.slice.index.RangeUsize.get_unchecked
(T : Type) :
Range Usize → ConstRawPtr (Slice T) → Result (ConstRawPtr (Slice T)) :=
-- Don't know what the model should be - for now we always fail to make
@@ -387,7 +387,7 @@ def core.slice.index.Range.get_unchecked
fun _ _ => fail panic
/- [core::slice::index::Range::get_unchecked_mut]: forward function -/
-def core.slice.index.Range.get_unchecked_mut
+def core.slice.index.RangeUsize.get_unchecked_mut
(T : Type) :
Range Usize → MutRawPtr (Slice T) → Result (MutRawPtr (Slice T)) :=
-- Don't know what the model should be - for now we always fail to make
@@ -395,17 +395,17 @@ def core.slice.index.Range.get_unchecked_mut
fun _ _ => fail panic
/- [core::slice::index::Range::index]: forward function -/
-def core.slice.index.Range.index
+def core.slice.index.RangeUsize.index
(T : Type) : Range Usize → Slice T → Result (Slice T) :=
sorry -- TODO
/- [core::slice::index::Range::index_mut]: forward function -/
-def core.slice.index.Range.index_mut
+def core.slice.index.RangeUsize.index_mut
(T : Type) : Range Usize → Slice T → Result (Slice T) :=
sorry -- TODO
/- [core::slice::index::Range::index_mut]: backward function 0 -/
-def core.slice.index.Range.index_mut_back
+def core.slice.index.RangeUsize.index_mut_back
(T : Type) : Range Usize → Slice T → Slice T → Result (Slice T) :=
sorry -- TODO
@@ -439,45 +439,44 @@ def core.array.Array.index_mut_back
(a : Array T N) (i : I) (x : inst.indexInst.Output) : Result (Array T N) :=
sorry -- TODO
-/- Trait implementation: [core::slice::index::[T]] -/
-def core.slice.index.Slice.coreopsindexIndexInst (T I : Type)
- (inst : core.slice.index.SliceIndex I (Slice T)) :
- core.ops.index.Index (Slice T) I := {
- Output := inst.Output
- index := core.slice.index.Slice.index T I inst
-}
-
/- Trait implementation: [core::slice::index::private_slice_index::Range] -/
-def core.slice.index.private_slice_index.Range.coresliceindexprivate_slice_indexSealedInst
+def core.slice.index.private_slice_index.SealedRangeUsizeInst
: core.slice.index.private_slice_index.Sealed (Range Usize) := {}
/- Trait implementation: [core::slice::index::Range] -/
-def core.slice.index.Range.coresliceindexSliceIndexInst (T : Type) :
+def core.slice.index.SliceIndexRangeUsizeSliceTInst (T : Type) :
core.slice.index.SliceIndex (Range Usize) (Slice T) := {
- sealedInst :=
- core.slice.index.private_slice_index.Range.coresliceindexprivate_slice_indexSealedInst
+ sealedInst := core.slice.index.private_slice_index.SealedRangeUsizeInst
Output := Slice T
- get := core.slice.index.Range.get T
- get_mut := core.slice.index.Range.get_mut T
- get_mut_back := core.slice.index.Range.get_mut_back T
- get_unchecked := core.slice.index.Range.get_unchecked T
- get_unchecked_mut := core.slice.index.Range.get_unchecked_mut T
- index := core.slice.index.Range.index T
- index_mut := core.slice.index.Range.index_mut T
- index_mut_back := core.slice.index.Range.index_mut_back T
+ get := core.slice.index.RangeUsize.get T
+ get_mut := core.slice.index.RangeUsize.get_mut T
+ get_mut_back := core.slice.index.RangeUsize.get_mut_back T
+ get_unchecked := core.slice.index.RangeUsize.get_unchecked T
+ get_unchecked_mut := core.slice.index.RangeUsize.get_unchecked_mut T
+ index := core.slice.index.RangeUsize.index T
+ index_mut := core.slice.index.RangeUsize.index_mut T
+ index_mut_back := core.slice.index.RangeUsize.index_mut_back T
+}
+
+/- Trait implementation: [core::slice::index::[T]] -/
+def core.ops.index.IndexSliceTIInst (T I : Type)
+ (inst : core.slice.index.SliceIndex I (Slice T)) :
+ core.ops.index.Index (Slice T) I := {
+ Output := inst.Output
+ index := core.slice.index.Slice.index T I inst
}
/- Trait implementation: [core::slice::index::[T]] -/
-def core.slice.index.Slice.coreopsindexIndexMutInst (T I : Type)
+def core.ops.index.IndexMutSliceTIInst (T I : Type)
(inst : core.slice.index.SliceIndex I (Slice T)) :
core.ops.index.IndexMut (Slice T) I := {
- indexInst := core.slice.index.Slice.coreopsindexIndexInst T I inst
+ indexInst := core.ops.index.IndexSliceTIInst T I inst
index_mut := core.slice.index.Slice.index_mut T I inst
index_mut_back := core.slice.index.Slice.index_mut_back T I inst
}
/- Trait implementation: [core::array::[T; N]] -/
-def core.array.Array.coreopsindexIndexInst (T I : Type) (N : Usize)
+def core.ops.index.IndexArrayIInst (T I : Type) (N : Usize)
(inst : core.ops.index.Index (Slice T) I) :
core.ops.index.Index (Array T N) I := {
Output := inst.Output
@@ -485,10 +484,10 @@ def core.array.Array.coreopsindexIndexInst (T I : Type) (N : Usize)
}
/- Trait implementation: [core::array::[T; N]] -/
-def core.array.Array.coreopsindexIndexMutInst (T I : Type) (N : Usize)
+def core.ops.index.IndexMutArrayIInst (T I : Type) (N : Usize)
(inst : core.ops.index.IndexMut (Slice T) I) :
core.ops.index.IndexMut (Array T N) I := {
- indexInst := core.array.Array.coreopsindexIndexInst T I N inst.indexInst
+ indexInst := core.ops.index.IndexArrayIInst T I N inst.indexInst
index_mut := core.array.Array.index_mut T I N inst
index_mut_back := core.array.Array.index_mut_back T I N inst
}
@@ -532,13 +531,13 @@ def core.slice.index.Usize.index_mut_back
sorry -- TODO
/- Trait implementation: [core::slice::index::private_slice_index::usize] -/
-def core.slice.index.private_slice_index.usize.coresliceindexprivate_slice_indexSealedInst
+def core.slice.index.private_slice_index.SealedUsizeInst
: core.slice.index.private_slice_index.Sealed Usize := {}
/- Trait implementation: [core::slice::index::usize] -/
-def core.slice.index.usize.coresliceindexSliceIndexInst (T : Type) :
+def core.slice.index.SliceIndexUsizeSliceTInst (T : Type) :
core.slice.index.SliceIndex Usize (Slice T) := {
- sealedInst := core.slice.index.private_slice_index.usize.coresliceindexprivate_slice_indexSealedInst
+ sealedInst := core.slice.index.private_slice_index.SealedUsizeInst
Output := T
get := core.slice.index.Usize.get T
get_mut := core.slice.index.Usize.get_mut T
diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean
index bbed6082..e600a151 100644
--- a/backends/lean/Base/Primitives/Vec.lean
+++ b/backends/lean/Base/Primitives/Vec.lean
@@ -153,19 +153,19 @@ def Vec.coreopsindexIndexMutInst (T I : Type)
@[simp]
theorem Vec.index_slice_index {α : Type} (v : Vec α) (i : Usize) :
- Vec.index α Usize (core.slice.index.usize.coresliceindexSliceIndexInst α) v i =
+ Vec.index α Usize (core.slice.index.SliceIndexUsizeSliceTInst α) v i =
Vec.index_usize v i :=
sorry
@[simp]
theorem Vec.index_mut_slice_index {α : Type} (v : Vec α) (i : Usize) :
- Vec.index_mut α Usize (core.slice.index.usize.coresliceindexSliceIndexInst α) v i =
+ Vec.index_mut α Usize (core.slice.index.SliceIndexUsizeSliceTInst α) v i =
Vec.index_usize v i :=
sorry
@[simp]
theorem Vec.index_mut_back_slice_index {α : Type} (v : Vec α) (i : Usize) (x : α) :
- Vec.index_mut_back α Usize (core.slice.index.usize.coresliceindexSliceIndexInst α) v i x =
+ Vec.index_mut_back α Usize (core.slice.index.SliceIndexUsizeSliceTInst α) v i x =
Vec.update_usize v i x :=
sorry