summaryrefslogtreecommitdiff
path: root/backends/lean/Base
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--backends/lean/Base/Primitives/ArraySlice.lean164
1 files changed, 50 insertions, 114 deletions
diff --git a/backends/lean/Base/Primitives/ArraySlice.lean b/backends/lean/Base/Primitives/ArraySlice.lean
index 615e0783..2a080ca6 100644
--- a/backends/lean/Base/Primitives/ArraySlice.lean
+++ b/backends/lean/Base/Primitives/ArraySlice.lean
@@ -40,14 +40,14 @@ def Array.make (α : Type u) (n : Usize) (init : List α) (hl : init.len = n.val
example : Array Int (Usize.ofInt 2) := Array.make Int (Usize.ofInt 2) [0, 1]
@[simp]
-abbrev Array.index {α : Type u} {n : Usize} [Inhabited α] (v : Array α n) (i : Int) : α :=
+abbrev Array.index_s {α : Type u} {n : Usize} [Inhabited α] (v : Array α n) (i : Int) : α :=
v.val.index i
@[simp]
abbrev Array.slice {α : Type u} {n : Usize} [Inhabited α] (v : Array α n) (i j : Int) : List α :=
v.val.slice i j
-def Array.index_shared (α : Type u) (n : Usize) (v: Array α n) (i: Usize) : Result α :=
+def Array.index_usize (α : Type u) (n : Usize) (v: Array α n) (i: Usize) : Result α :=
match v.val.indexOpt i.val with
| none => fail .arrayOutOfBounds
| some x => ret x
@@ -67,48 +67,27 @@ theorem Array.repeat_spec {α : Type u} (n : Usize) (x : α) :
-/
@[pspec]
-theorem Array.index_shared_spec {α : Type u} {n : Usize} [Inhabited α] (v: Array α n) (i: Usize)
+theorem Array.index_usize_spec {α : Type u} {n : Usize} [Inhabited α] (v: Array α n) (i: Usize)
(hbound : i.val < v.length) :
- ∃ x, v.index_shared α n i = ret x ∧ x = v.val.index i.val := by
- simp only [index_shared]
+ ∃ x, v.index_usize α n i = ret x ∧ x = v.val.index i.val := by
+ simp only [index_usize]
-- TODO: dependent rewrite
have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*])
simp [*]
--- This shouldn't be used
-def Array.index_shared_back (α : Type u) (n : Usize) (v: Array α n) (i: Usize) (_: α) : Result Unit :=
- if i.val < List.length v.val then
- .ret ()
- else
- .fail arrayOutOfBounds
-
-def Array.index_mut (α : Type u) (n : Usize) (v: Array α n) (i: Usize) : Result α :=
- match v.val.indexOpt i.val with
- | none => fail .arrayOutOfBounds
- | some x => ret x
-
-@[pspec]
-theorem Array.index_mut_spec {α : Type u} {n : Usize} [Inhabited α] (v: Array α n) (i: Usize)
- (hbound : i.val < v.length) :
- ∃ x, v.index_mut α n i = ret x ∧ x = v.val.index i.val := by
- simp only [index_mut]
- -- TODO: dependent rewrite
- have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*])
- simp [*]
-
-def Array.index_mut_back (α : Type u) (n : Usize) (v: Array α n) (i: Usize) (x: α) : Result (Array α n) :=
+def Array.update_usize (α : Type u) (n : Usize) (v: Array α n) (i: Usize) (x: α) : Result (Array α n) :=
match v.val.indexOpt i.val with
| none => fail .arrayOutOfBounds
| some _ =>
.ret ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩
@[pspec]
-theorem Array.index_mut_back_spec {α : Type u} {n : Usize} (v: Array α n) (i: Usize) (x : α)
+theorem Array.update_usize_spec {α : Type u} {n : Usize} (v: Array α n) (i: Usize) (x : α)
(hbound : i.val < v.length) :
- ∃ nv, v.index_mut_back α n i x = ret nv ∧
+ ∃ nv, v.update_usize α n i x = ret nv ∧
nv.val = v.val.update i.val x
:= by
- simp only [index_mut_back]
+ simp only [update_usize]
have h := List.indexOpt_bounds v.val i.val
split
. simp_all [length]; cases h <;> scalar_tac
@@ -144,14 +123,14 @@ theorem Slice.len_val {α : Type u} (v : Slice α) : (Slice.len α v).val = v.le
by rfl
@[simp]
-abbrev Slice.index {α : Type u} [Inhabited α] (v: Slice α) (i: Int) : α :=
+abbrev Slice.index_s {α : Type u} [Inhabited α] (v: Slice α) (i: Int) : α :=
v.val.index i
@[simp]
abbrev Slice.slice {α : Type u} [Inhabited α] (s : Slice α) (i j : Int) : List α :=
s.val.slice i j
-def Slice.index_shared (α : Type u) (v: Slice α) (i: Usize) : Result α :=
+def Slice.index_usize (α : Type u) (v: Slice α) (i: Usize) : Result α :=
match v.val.indexOpt i.val with
| none => fail .arrayOutOfBounds
| some x => ret x
@@ -162,10 +141,10 @@ def Slice.index_shared (α : Type u) (v: Slice α) (i: Usize) : Result α :=
-/
@[pspec]
-theorem Slice.index_shared_spec {α : Type u} [Inhabited α] (v: Slice α) (i: Usize)
+theorem Slice.index_usize_spec {α : Type u} [Inhabited α] (v: Slice α) (i: Usize)
(hbound : i.val < v.length) :
- ∃ x, v.index_shared α i = ret x ∧ x = v.val.index i.val := by
- simp only [index_shared]
+ ∃ x, v.index_usize α i = ret x ∧ x = v.val.index i.val := by
+ simp only [index_usize]
-- TODO: dependent rewrite
have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*])
simp [*]
@@ -177,33 +156,19 @@ def Slice.index_shared_back (α : Type u) (v: Slice α) (i: Usize) (_: α) : Res
else
.fail arrayOutOfBounds
-def Slice.index_mut (α : Type u) (v: Slice α) (i: Usize) : Result α :=
- match v.val.indexOpt i.val with
- | none => fail .arrayOutOfBounds
- | some x => ret x
-
-@[pspec]
-theorem Slice.index_mut_spec {α : Type u} [Inhabited α] (v: Slice α) (i: Usize)
- (hbound : i.val < v.length) :
- ∃ x, v.index_mut α i = ret x ∧ x = v.val.index i.val := by
- simp only [index_mut]
- -- TODO: dependent rewrite
- have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*])
- simp [*]
-
-def Slice.index_mut_back (α : Type u) (v: Slice α) (i: Usize) (x: α) : Result (Slice α) :=
+def Slice.update_usize (α : Type u) (v: Slice α) (i: Usize) (x: α) : Result (Slice α) :=
match v.val.indexOpt i.val with
| none => fail .arrayOutOfBounds
| some _ =>
.ret ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩
@[pspec]
-theorem Slice.index_mut_back_spec {α : Type u} (v: Slice α) (i: Usize) (x : α)
+theorem Slice.update_usize_spec {α : Type u} (v: Slice α) (i: Usize) (x : α)
(hbound : i.val < v.length) :
- ∃ nv, v.index_mut_back α i x = ret nv ∧
+ ∃ nv, v.update_usize α i x = ret nv ∧
nv.val = v.val.update i.val x
:= by
- simp only [index_mut_back]
+ simp only [update_usize]
have h := List.indexOpt_bounds v.val i.val
split
. simp_all [length]; cases h <;> scalar_tac
@@ -212,34 +177,27 @@ theorem Slice.index_mut_back_spec {α : Type u} (v: Slice α) (i: Usize) (x : α
/- Array to slice/subslices -/
/- We could make this function not use the `Result` type. By making it monadic, we
- push the user to use the `Array.to_slice_shared_spec` spec theorem below (through the
- `progress` tactic), meaning `Array.to_slice_shared` should be considered as opaque.
+ push the user to use the `Array.to_slice_spec` spec theorem below (through the
+ `progress` tactic), meaning `Array.to_slice` should be considered as opaque.
All what the spec theorem reveals is that the "representative" lists are the same. -/
-def Array.to_slice_shared (α : Type u) (n : Usize) (v : Array α n) : Result (Slice α) :=
+def Array.to_slice (α : Type u) (n : Usize) (v : Array α n) : Result (Slice α) :=
ret ⟨ v.val, by simp [← List.len_eq_length]; scalar_tac ⟩
@[pspec]
-theorem Array.to_slice_shared_spec {α : Type u} {n : Usize} (v : Array α n) :
- ∃ s, to_slice_shared α n v = ret s ∧ v.val = s.val := by simp [to_slice_shared]
-
-def Array.to_slice_mut (α : Type u) (n : Usize) (v : Array α n) : Result (Slice α) :=
- to_slice_shared α n v
+theorem Array.to_slice_spec {α : Type u} {n : Usize} (v : Array α n) :
+ ∃ s, to_slice α n v = ret s ∧ v.val = s.val := by simp [to_slice]
-@[pspec]
-theorem Array.to_slice_mut_spec {α : Type u} {n : Usize} (v : Array α n) :
- ∃ s, Array.to_slice_shared α n v = ret s ∧ v.val = s.val := to_slice_shared_spec v
-
-def Array.to_slice_mut_back (α : Type u) (n : Usize) (_ : Array α n) (s : Slice α) : Result (Array α n) :=
+def Array.from_slice (α : Type u) (n : Usize) (_ : Array α n) (s : Slice α) : Result (Array α n) :=
if h: s.val.len = n.val then
ret ⟨ s.val, by simp [← List.len_eq_length, *] ⟩
else fail panic
@[pspec]
-theorem Array.to_slice_mut_back_spec {α : Type u} {n : Usize} (a : Array α n) (ns : Slice α) (h : ns.val.len = n.val) :
- ∃ na, to_slice_mut_back α n a ns = ret na ∧ na.val = ns.val
- := by simp [to_slice_mut_back, *]
+theorem Array.from_slice_spec {α : Type u} {n : Usize} (a : Array α n) (ns : Slice α) (h : ns.val.len = n.val) :
+ ∃ na, from_slice α n a ns = ret na ∧ na.val = ns.val
+ := by simp [from_slice, *]
-def Array.subslice_shared (α : Type u) (n : Usize) (a : Array α n) (r : Range Usize) : Result (Slice α) :=
+def Array.subslice (α : Type u) (n : Usize) (a : Array α n) (r : Range Usize) : Result (Slice α) :=
-- TODO: not completely sure here
if r.start.val < r.end_.val ∧ r.end_.val ≤ a.val.len then
ret ⟨ a.val.slice r.start.val r.end_.val,
@@ -251,29 +209,18 @@ def Array.subslice_shared (α : Type u) (n : Usize) (a : Array α n) (r : Range
fail panic
@[pspec]
-theorem Array.subslice_shared_spec {α : Type u} {n : Usize} [Inhabited α] (a : Array α n) (r : Range Usize)
+theorem Array.subslice_spec {α : Type u} {n : Usize} [Inhabited α] (a : Array α n) (r : Range Usize)
(h0 : r.start.val < r.end_.val) (h1 : r.end_.val ≤ a.val.len) :
- ∃ s, subslice_shared α n a r = ret s ∧
+ ∃ s, subslice α n a r = ret s ∧
s.val = a.val.slice r.start.val r.end_.val ∧
(∀ i, 0 ≤ i → i + r.start.val < r.end_.val → s.val.index i = a.val.index (r.start.val + i))
:= by
- simp [subslice_shared, *]
+ simp [subslice, *]
intro i _ _
have := List.index_slice r.start.val r.end_.val i a.val (by scalar_tac) (by scalar_tac) (by trivial) (by scalar_tac)
simp [*]
-def Array.subslice_mut (α : Type u) (n : Usize) (a : Array α n) (r : Range Usize) : Result (Slice α) :=
- Array.subslice_shared α n a r
-
-@[pspec]
-theorem Array.subslice_mut_spec {α : Type u} {n : Usize} [Inhabited α] (a : Array α n) (r : Range Usize)
- (h0 : r.start.val < r.end_.val) (h1 : r.end_.val ≤ a.val.len) :
- ∃ s, subslice_mut α n a r = ret s ∧
- s.val = a.slice r.start.val r.end_.val ∧
- (∀ i, 0 ≤ i → i + r.start.val < r.end_.val → s.val.index i = a.val.index (r.start.val + i))
- := subslice_shared_spec a r h0 h1
-
-def Array.subslice_mut_back (α : Type u) (n : Usize) (a : Array α n) (r : Range Usize) (s : Slice α) : Result (Array α n) :=
+def Array.update_subslice (α : Type u) (n : Usize) (a : Array α n) (r : Range Usize) (s : Slice α) : Result (Array α n) :=
-- TODO: not completely sure here
if h: r.start.val < r.end_.val ∧ r.end_.val ≤ a.length ∧ s.val.len = r.end_.val - r.start.val then
let s_beg := a.val.itake r.start.val
@@ -298,13 +245,13 @@ def Array.subslice_mut_back (α : Type u) (n : Usize) (a : Array α n) (r : Rang
-- We should introduce special symbols for the monadic arithmetic operations
-- (the use will never write those symbols directly).
@[pspec]
-theorem Array.subslice_mut_back_spec {α : Type u} {n : Usize} [Inhabited α] (a : Array α n) (r : Range Usize) (s : Slice α)
+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) :
- ∃ na, subslice_mut_back α n a r s = ret na ∧
- (∀ i, 0 ≤ i → i < r.start.val → na.index i = a.index i) ∧
- (∀ i, r.start.val ≤ i → i < r.end_.val → na.index i = s.index (i - r.start.val)) ∧
- (∀ i, r.end_.val ≤ i → i < n.val → na.index i = a.index i) := by
- simp [subslice_mut_back, *]
+ ∃ na, update_subslice α n a r s = ret na ∧
+ (∀ i, 0 ≤ i → i < r.start.val → na.index_s i = a.index_s i) ∧
+ (∀ i, r.start.val ≤ i → i < r.end_.val → na.index_s i = s.index_s (i - r.start.val)) ∧
+ (∀ i, r.end_.val ≤ i → i < n.val → na.index_s i = a.index_s i) := by
+ simp [update_subslice, *]
have h := List.replace_slice_index r.start.val r.end_.val a.val s.val
(by scalar_tac) (by scalar_tac) (by scalar_tac) (by scalar_tac)
simp [List.replace_slice] at h
@@ -321,7 +268,7 @@ theorem Array.subslice_mut_back_spec {α : Type u} {n : Usize} [Inhabited α] (a
have := h2 i (by int_tac) (by int_tac)
simp [*]
-def Slice.subslice_shared (α : Type u) (s : Slice α) (r : Range Usize) : Result (Slice α) :=
+def Slice.subslice (α : Type u) (s : Slice α) (r : Range Usize) : Result (Slice α) :=
-- TODO: not completely sure here
if r.start.val < r.end_.val ∧ r.end_.val ≤ s.length then
ret ⟨ s.val.slice r.start.val r.end_.val,
@@ -333,32 +280,21 @@ def Slice.subslice_shared (α : Type u) (s : Slice α) (r : Range Usize) : Resul
fail panic
@[pspec]
-theorem Slice.subslice_shared_spec {α : Type u} [Inhabited α] (s : Slice α) (r : Range Usize)
+theorem Slice.subslice_spec {α : Type u} [Inhabited α] (s : Slice α) (r : Range Usize)
(h0 : r.start.val < r.end_.val) (h1 : r.end_.val ≤ s.val.len) :
- ∃ ns, subslice_shared α s r = ret ns ∧
+ ∃ ns, subslice α s r = ret ns ∧
ns.val = s.slice r.start.val r.end_.val ∧
- (∀ i, 0 ≤ i → i + r.start.val < r.end_.val → ns.index i = s.index (r.start.val + i))
+ (∀ i, 0 ≤ i → i + r.start.val < r.end_.val → ns.index_s i = s.index_s (r.start.val + i))
:= by
- simp [subslice_shared, *]
+ simp [subslice, *]
intro i _ _
have := List.index_slice r.start.val r.end_.val i s.val (by scalar_tac) (by scalar_tac) (by trivial) (by scalar_tac)
simp [*]
-def Slice.subslice_mut (α : Type u) (s : Slice α) (r : Range Usize) : Result (Slice α) :=
- Slice.subslice_shared α s r
-
-@[pspec]
-theorem Slice.subslice_mut_spec {α : Type u} [Inhabited α] (s : Slice α) (r : Range Usize)
- (h0 : r.start.val < r.end_.val) (h1 : r.end_.val ≤ s.val.len) :
- ∃ ns, subslice_mut α s r = ret ns ∧
- ns.val = s.slice r.start.val r.end_.val ∧
- (∀ i, 0 ≤ i → i + r.start.val < r.end_.val → ns.index i = s.index (r.start.val + i))
- := subslice_shared_spec s r h0 h1
-
attribute [pp_dot] List.len List.length List.index -- use the dot notation when printing
set_option pp.coercions false -- do not print coercions with ↑ (this doesn't parse)
-def Slice.subslice_mut_back (α : Type u) (s : Slice α) (r : Range Usize) (ss : Slice α) : Result (Slice α) :=
+def Slice.update_subslice (α : Type u) (s : Slice α) (r : Range Usize) (ss : Slice α) : Result (Slice α) :=
-- TODO: not completely sure here
if h: r.start.val < r.end_.val ∧ r.end_.val ≤ s.length ∧ ss.val.len = r.end_.val - r.start.val then
let s_beg := s.val.itake r.start.val
@@ -378,13 +314,13 @@ def Slice.subslice_mut_back (α : Type u) (s : Slice α) (r : Range Usize) (ss :
fail panic
@[pspec]
-theorem Slice.subslice_mut_back_spec {α : Type u} [Inhabited α] (a : Slice α) (r : Range Usize) (ss : Slice α)
+theorem Slice.update_subslice_spec {α : Type u} [Inhabited α] (a : Slice α) (r : Range Usize) (ss : Slice α)
(_ : r.start.val < r.end_.val) (_ : r.end_.val ≤ a.length) (_ : ss.length = r.end_.val - r.start.val) :
- ∃ na, subslice_mut_back α a r ss = ret na ∧
- (∀ i, 0 ≤ i → i < r.start.val → na.index i = a.index i) ∧
- (∀ i, r.start.val ≤ i → i < r.end_.val → na.index i = ss.index (i - r.start.val)) ∧
- (∀ i, r.end_.val ≤ i → i < a.length → na.index i = a.index i) := by
- simp [subslice_mut_back, *]
+ ∃ na, update_subslice α a r ss = ret na ∧
+ (∀ i, 0 ≤ i → i < r.start.val → na.index_s i = a.index_s i) ∧
+ (∀ i, r.start.val ≤ i → i < r.end_.val → na.index_s i = ss.index_s (i - r.start.val)) ∧
+ (∀ i, r.end_.val ≤ i → i < a.length → na.index_s i = a.index_s i) := by
+ simp [update_subslice, *]
have h := List.replace_slice_index r.start.val r.end_.val a.val ss.val
(by scalar_tac) (by scalar_tac) (by scalar_tac) (by scalar_tac)
simp [List.replace_slice, *] at h