diff options
author | Son Ho | 2023-12-22 18:30:29 +0100 |
---|---|---|
committer | Son Ho | 2023-12-22 18:30:29 +0100 |
commit | e799ef503dda30b6dcbecb042ecb0fae1a71fa81 (patch) | |
tree | 25ec8f7eaa112972f4798ae9b20cb1b9336511d3 /backends/lean/Base/Primitives/ArraySlice.lean | |
parent | a504199331e1b406d24067837a725085fb8f09e9 (diff) |
Update the Lean standard library
Diffstat (limited to '')
-rw-r--r-- | backends/lean/Base/Primitives/ArraySlice.lean | 68 |
1 files changed, 11 insertions, 57 deletions
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 |