summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Primitives
diff options
context:
space:
mode:
authorSon Ho2023-12-22 18:30:29 +0100
committerSon Ho2023-12-22 18:30:29 +0100
commite799ef503dda30b6dcbecb042ecb0fae1a71fa81 (patch)
tree25ec8f7eaa112972f4798ae9b20cb1b9336511d3 /backends/lean/Base/Primitives
parenta504199331e1b406d24067837a725085fb8f09e9 (diff)
Update the Lean standard library
Diffstat (limited to 'backends/lean/Base/Primitives')
-rw-r--r--backends/lean/Base/Primitives/Alloc.lean4
-rw-r--r--backends/lean/Base/Primitives/ArraySlice.lean68
-rw-r--r--backends/lean/Base/Primitives/Base.lean3
-rw-r--r--backends/lean/Base/Primitives/CoreOps.lean6
-rw-r--r--backends/lean/Base/Primitives/Vec.lean38
5 files changed, 38 insertions, 81 deletions
diff --git a/backends/lean/Base/Primitives/Alloc.lean b/backends/lean/Base/Primitives/Alloc.lean
index 6c89c6bb..1f470fe1 100644
--- a/backends/lean/Base/Primitives/Alloc.lean
+++ b/backends/lean/Base/Primitives/Alloc.lean
@@ -12,8 +12,7 @@ namespace boxed -- alloc.boxed
namespace Box -- alloc.boxed.Box
def deref (T : Type) (x : T) : Result T := ret x
-def deref_mut (T : Type) (x : T) : Result T := ret x
-def deref_mut_back (T : Type) (_ : T) (x : T) : Result T := ret x
+def deref_mut (T : Type) (x : T) : Result (T × (T → Result T)) := ret (x, λ x => ret x)
/-- Trait instance -/
def coreopsDerefInst (Self : Type) :
@@ -27,7 +26,6 @@ def coreopsDerefMutInst (Self : Type) :
core.ops.deref.DerefMut Self := {
derefInst := coreopsDerefInst Self
deref_mut := deref_mut Self
- deref_mut_back := deref_mut_back Self
}
end Box -- alloc.boxed.Box
diff --git a/backends/lean/Base/Primitives/ArraySlice.lean b/backends/lean/Base/Primitives/ArraySlice.lean
index f68c0846..59432a0b 100644
--- a/backends/lean/Base/Primitives/ArraySlice.lean
+++ b/backends/lean/Base/Primitives/ArraySlice.lean
@@ -149,13 +149,6 @@ theorem Slice.index_usize_spec {α : Type u} [Inhabited α] (v: Slice α) (i: Us
have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*])
simp [*]
--- This shouldn't be used
-def Slice.index_shared_back (α : Type u) (v: Slice α) (i: Usize) (_: α) : Result Unit :=
- if i.val < List.length v.val then
- .ret ()
- else
- .fail arrayOutOfBounds
-
def Slice.update_usize (α : Type u) (v: Slice α) (i: Usize) (x: α) : Result (Slice α) :=
match v.val.indexOpt i.val with
| none => fail .arrayOutOfBounds
@@ -243,7 +236,7 @@ def Array.update_subslice (α : Type u) (n : Usize) (a : Array α n) (r : Range
-- but: some symbols like `+` are already overloaded to be notations for monadic
-- operations/
-- We should introduce special symbols for the monadic arithmetic operations
--- (the use will never write those symbols directly).
+-- (the user will never write those symbols directly).
@[pspec]
theorem Array.update_subslice_spec {α : Type u} {n : Usize} [Inhabited α] (a : Array α n) (r : Range Usize) (s : Slice α)
(_ : r.start.val < r.end_.val) (_ : r.end_.val ≤ a.length) (_ : s.length = r.end_.val - r.start.val) :
@@ -345,13 +338,11 @@ structure core.slice.index.SliceIndex (Self T : Type) where
sealedInst : core.slice.index.private_slice_index.Sealed Self
Output : Type
get : Self → T → Result (Option Output)
- get_mut : Self → T → Result (Option Output)
- get_mut_back : Self → T → Option Output → Result T
+ get_mut : Self → T → Result (Option Output × (Option Output → Result T))
get_unchecked : Self → ConstRawPtr T → Result (ConstRawPtr Output)
get_unchecked_mut : Self → MutRawPtr T → Result (MutRawPtr Output)
index : Self → T → Result Output
- index_mut : Self → T → Result Output
- index_mut_back : Self → T → Output → Result T
+ index_mut : Self → T → Result (Output × (Output → Result T))
/- [core::slice::index::[T]::index]: forward function -/
def core.slice.index.Slice.index
@@ -369,13 +360,7 @@ def core.slice.index.RangeUsize.get (T : Type) (i : Range Usize) (slice : Slice
/- [core::slice::index::Range::get_mut]: forward function -/
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.RangeUsize.get_mut_back
- (T : Type) :
- Range Usize → Slice T → Option (Slice T) → Result (Slice T) :=
+ (T : Type) : Range Usize → Slice T → Result (Option (Slice T) × (Option (Slice T) → Result (Slice T))) :=
sorry -- TODO
/- [core::slice::index::Range::get_unchecked]: forward function -/
@@ -401,24 +386,13 @@ def core.slice.index.RangeUsize.index
/- [core::slice::index::Range::index_mut]: forward function -/
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.RangeUsize.index_mut_back
- (T : Type) : Range Usize → Slice T → Slice T → Result (Slice T) :=
+ (T : Type) : Range Usize → Slice T → Result (Slice T × (Slice T → Result (Slice T))) :=
sorry -- TODO
/- [core::slice::index::[T]::index_mut]: forward function -/
def core.slice.index.Slice.index_mut
(T I : Type) (inst : core.slice.index.SliceIndex I (Slice T)) :
- Slice T → I → Result inst.Output :=
- sorry -- TODO
-
-/- [core::slice::index::[T]::index_mut]: backward function 0 -/
-def core.slice.index.Slice.index_mut_back
- (T I : Type) (inst : core.slice.index.SliceIndex I (Slice T)) :
- Slice T → I → inst.Output → Result (Slice T) :=
+ Slice T → I → Result (inst.Output × (inst.Output → Result (Slice T))) :=
sorry -- TODO
/- [core::array::[T; N]::index]: forward function -/
@@ -430,13 +404,8 @@ def core.array.Array.index
/- [core::array::[T; N]::index_mut]: forward function -/
def core.array.Array.index_mut
(T I : Type) (N : Usize) (inst : core.ops.index.IndexMut (Slice T) I)
- (a : Array T N) (i : I) : Result inst.indexInst.Output :=
- sorry -- TODO
-
-/- [core::array::[T; N]::index_mut]: backward function 0 -/
-def core.array.Array.index_mut_back
- (T I : Type) (N : Usize) (inst : core.ops.index.IndexMut (Slice T) I)
- (a : Array T N) (i : I) (x : inst.indexInst.Output) : Result (Array T N) :=
+ (a : Array T N) (i : I) :
+ Result (inst.indexInst.Output × (inst.indexInst.Output → Result (Array T N))) :=
sorry -- TODO
/- Trait implementation: [core::slice::index::private_slice_index::Range] -/
@@ -450,12 +419,10 @@ def core.slice.index.SliceIndexRangeUsizeSliceTInst (T : Type) :
Output := Slice 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]] -/
@@ -472,7 +439,6 @@ def core.ops.index.IndexMutSliceTIInst (T I : Type)
core.ops.index.IndexMut (Slice T) I := {
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]] -/
@@ -489,7 +455,6 @@ def core.ops.index.IndexMutArrayIInst (T I : Type) (N : Usize)
core.ops.index.IndexMut (Array T N) I := {
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
}
/- [core::slice::index::usize::get]: forward function -/
@@ -499,12 +464,7 @@ def core.slice.index.Usize.get
/- [core::slice::index::usize::get_mut]: forward function -/
def core.slice.index.Usize.get_mut
- (T : Type) : Usize → Slice T → Result (Option T) :=
- sorry -- TODO
-
-/- [core::slice::index::usize::get_mut]: backward function 0 -/
-def core.slice.index.Usize.get_mut_back
- (T : Type) : Usize → Slice T → Option T → Result (Slice T) :=
+ (T : Type) : Usize → Slice T → Result (Option T × (Option T → Result (Slice T))) :=
sorry -- TODO
/- [core::slice::index::usize::get_unchecked]: forward function -/
@@ -522,12 +482,8 @@ def core.slice.index.Usize.index (T : Type) : Usize → Slice T → Result T :=
sorry -- TODO
/- [core::slice::index::usize::index_mut]: forward function -/
-def core.slice.index.Usize.index_mut (T : Type) : Usize → Slice T → Result T :=
- sorry -- TODO
-
-/- [core::slice::index::usize::index_mut]: backward function 0 -/
-def core.slice.index.Usize.index_mut_back
- (T : Type) : Usize → Slice T → T → Result (Slice T) :=
+def core.slice.index.Usize.index_mut (T : Type) :
+ Usize → Slice T → Result (T × (T → Result (Slice T))) :=
sorry -- TODO
/- Trait implementation: [core::slice::index::private_slice_index::usize] -/
@@ -541,12 +497,10 @@ def core.slice.index.SliceIndexUsizeSliceTInst (T : Type) :
Output := T
get := core.slice.index.Usize.get T
get_mut := core.slice.index.Usize.get_mut T
- get_mut_back := core.slice.index.Usize.get_mut_back T
get_unchecked := core.slice.index.Usize.get_unchecked T
get_unchecked_mut := core.slice.index.Usize.get_unchecked_mut T
index := core.slice.index.Usize.index T
index_mut := core.slice.index.Usize.index_mut T
- index_mut_back := core.slice.index.Usize.index_mut_back T
}
end Primitives
diff --git a/backends/lean/Base/Primitives/Base.lean b/backends/lean/Base/Primitives/Base.lean
index 7fc33251..321c39a8 100644
--- a/backends/lean/Base/Primitives/Base.lean
+++ b/backends/lean/Base/Primitives/Base.lean
@@ -120,8 +120,7 @@ def Result.attach {α: Type} (o : Result α): Result { x : α // o = ret x } :=
-- MISC --
----------
-@[simp] def core.mem.replace (a : Type) (x : a) (_ : a) : a := x
-@[simp] def core.mem.replace_back (a : Type) (_ : a) (y : a) : a := y
+@[simp] def core.mem.replace (a : Type) (x : a) (_ : a) : a × (a → a) := (x, λ x => x)
/-- Aeneas-translated function -- useful to reduce non-recursive definitions.
Use with `simp [ aeneas ]` -/
diff --git a/backends/lean/Base/Primitives/CoreOps.lean b/backends/lean/Base/Primitives/CoreOps.lean
index da458f66..1736bfa6 100644
--- a/backends/lean/Base/Primitives/CoreOps.lean
+++ b/backends/lean/Base/Primitives/CoreOps.lean
@@ -16,8 +16,7 @@ structure Index (Self Idx : Type) where
/- Trait declaration: [core::ops::index::IndexMut] -/
structure IndexMut (Self Idx : Type) where
indexInst : Index Self Idx
- index_mut : Self → Idx → Result indexInst.Output
- index_mut_back : Self → Idx → indexInst.Output → Result Self
+ index_mut : Self → Idx → Result (indexInst.Output × (indexInst.Output → Result Self))
end index -- core.ops.index
@@ -29,8 +28,7 @@ structure Deref (Self : Type) where
structure DerefMut (Self : Type) where
derefInst : Deref Self
- deref_mut : Self → Result derefInst.Target
- deref_mut_back : Self → derefInst.Target → Result Self
+ deref_mut : Self → Result (derefInst.Target × (Self → Result Self))
end deref -- core.ops.deref
diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean
index 2c3fce91..12733a34 100644
--- a/backends/lean/Base/Primitives/Vec.lean
+++ b/backends/lean/Base/Primitives/Vec.lean
@@ -122,6 +122,26 @@ theorem Vec.update_usize_spec {α : Type u} (v: Vec α) (i: Usize) (x : α)
. simp_all [length]; cases h <;> scalar_tac
. simp_all
+def Vec.index_mut_usize {α : Type u} (v: Vec α) (i: Usize) :
+ Result (α × (α → Result (Vec α))) :=
+ match Vec.index_usize v i with
+ | ret x =>
+ ret (x, Vec.update_usize v i)
+ | fail e => fail e
+ | div => div
+
+@[pspec]
+theorem Vec.index_mut_usize_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize)
+ (hbound : i.val < v.length) :
+ ∃ x back, v.index_mut_usize i = ret (x, back) ∧
+ x = v.val.index i.val ∧
+ -- Backward function
+ back = v.update_usize i
+ := by
+ simp only [index_mut_usize]
+ have ⟨ x, h ⟩ := index_usize_spec v i hbound
+ simp [h]
+
/- [alloc::vec::Vec::index]: forward function -/
def Vec.index (T I : Type) (inst : core.slice.index.SliceIndex I (Slice T))
(self : Vec T) (i : I) : Result inst.Output :=
@@ -129,13 +149,8 @@ def Vec.index (T I : Type) (inst : core.slice.index.SliceIndex I (Slice T))
/- [alloc::vec::Vec::index_mut]: forward function -/
def Vec.index_mut (T I : Type) (inst : core.slice.index.SliceIndex I (Slice T))
- (self : Vec T) (i : I) : Result inst.Output :=
- sorry -- TODO
-
-/- [alloc::vec::Vec::index_mut]: backward function 0 -/
-def Vec.index_mut_back
- (T I : Type) (inst : core.slice.index.SliceIndex I (Slice T))
- (self : Vec T) (i : I) (x : inst.Output) : Result (alloc.vec.Vec T) :=
+ (self : Vec T) (i : I) :
+ Result (inst.Output × (inst.Output → Result (Vec T))) :=
sorry -- TODO
/- Trait implementation: [alloc::vec::Vec] -/
@@ -152,7 +167,6 @@ def Vec.coreopsindexIndexMutInst (T I : Type)
core.ops.index.IndexMut (alloc.vec.Vec T) I := {
indexInst := Vec.coreopsindexIndexInst T I inst
index_mut := Vec.index_mut T I inst
- index_mut_back := Vec.index_mut_back T I inst
}
@[simp]
@@ -164,13 +178,7 @@ theorem Vec.index_slice_index {α : Type} (v : Vec α) (i : Usize) :
@[simp]
theorem Vec.index_mut_slice_index {α : Type} (v : Vec α) (i : Usize) :
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.SliceIndexUsizeSliceTInst α) v i x =
- Vec.update_usize v i x :=
+ index_mut_usize v i :=
sorry
end alloc.vec