summaryrefslogtreecommitdiff
path: root/backends/lean/Base
diff options
context:
space:
mode:
authorSon Ho2023-10-25 18:44:28 +0200
committerSon Ho2023-10-25 18:44:28 +0200
commit81b7a7d706bc1a0f2f57bc254a8af158039a10cf (patch)
tree64ac32b95e61f12d54be54827a3efc66f829106f /backends/lean/Base
parent862c6f939b001e4fe0556cc73af71210e7b96ea2 (diff)
Make the hashmap files typecheck again in Lean
Diffstat (limited to '')
-rw-r--r--backends/lean/Base/Primitives/ArraySlice.lean61
-rw-r--r--backends/lean/Base/Primitives/Range.lean2
-rw-r--r--backends/lean/Base/Primitives/Vec.lean74
-rw-r--r--backends/lean/Base/Progress/Progress.lean3
4 files changed, 107 insertions, 33 deletions
diff --git a/backends/lean/Base/Primitives/ArraySlice.lean b/backends/lean/Base/Primitives/ArraySlice.lean
index 47807a0d..615e0783 100644
--- a/backends/lean/Base/Primitives/ArraySlice.lean
+++ b/backends/lean/Base/Primitives/ArraySlice.lean
@@ -13,7 +13,7 @@ import Base.Progress.Base
namespace Primitives
-open Result Error
+open Result Error core.ops.range
def Array (α : Type u) (n : Usize) := { l : List α // l.length = n.val }
@@ -406,7 +406,7 @@ structure core.slice.index.private_slice_index.Sealed (Self : Type) where
/- Trait declaration: [core::slice::index::SliceIndex] -/
structure core.slice.index.SliceIndex (Self T0 : Type) where
- sealedInst :core.slice.index.private_slice_index.Sealed Self
+ sealedInst : core.slice.index.private_slice_index.Sealed Self
Output : Type
get : Self → T0 → Result (Option Output)
get_mut : Self → T0 → Result (Option Output)
@@ -557,4 +557,61 @@ def core.array.Array.coreopsindexIndexMutInst (T0 I : Type) (N : Usize)
index_mut_back := core.array.Array.index_mut_back T0 I N inst
}
+/- [core::slice::index::usize::get]: forward function -/
+def core.slice.index.Usize.get
+ (T : Type) : Usize → Slice T → Result (Option T) :=
+ sorry -- TODO
+
+/- [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) :=
+ sorry -- TODO
+
+/- [core::slice::index::usize::get_unchecked]: forward function -/
+def core.slice.index.Usize.get_unchecked
+ (T : Type) : Usize → ConstRawPtr (Slice T) → Result (ConstRawPtr T) :=
+ sorry -- TODO
+
+/- [core::slice::index::usize::get_unchecked_mut]: forward function -/
+def core.slice.index.Usize.get_unchecked_mut
+ (T : Type) : Usize → MutRawPtr (Slice T) → Result (MutRawPtr T) :=
+ sorry -- TODO
+
+/- [core::slice::index::usize::index]: forward function -/
+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) :=
+ sorry -- TODO
+
+/- Trait implementation: [core::slice::index::private_slice_index::usize] -/
+def core.slice.index.private_slice_index.usize.coresliceindexprivate_slice_indexSealedInst
+ : core.slice.index.private_slice_index.Sealed Usize := {}
+
+/- Trait implementation: [core::slice::index::usize] -/
+def core.slice.index.usize.coresliceindexSliceIndexInst (T : Type) :
+ core.slice.index.SliceIndex Usize (Slice T) := {
+ sealedInst := core.slice.index.private_slice_index.usize.coresliceindexprivate_slice_indexSealedInst
+ 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/Range.lean b/backends/lean/Base/Primitives/Range.lean
index 26cbee42..a268bcba 100644
--- a/backends/lean/Base/Primitives/Range.lean
+++ b/backends/lean/Base/Primitives/Range.lean
@@ -11,7 +11,7 @@ import Base.Progress.Base
namespace Primitives
-structure Range (α : Type u) where
+structure core.ops.range.Range (α : Type u) where
mk ::
start: α
end_: α
diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean
index 99fcedc6..e1b7e87b 100644
--- a/backends/lean/Base/Primitives/Vec.lean
+++ b/backends/lean/Base/Primitives/Vec.lean
@@ -14,6 +14,8 @@ namespace Primitives
open Result Error
+namespace alloc.vec
+
def Vec (α : Type u) := { l : List α // l.length ≤ Usize.max }
instance (a : Type u) : Arith.HasIntProp (Vec a) where
@@ -79,7 +81,7 @@ theorem Vec.insert_spec {α : Type u} (v: Vec α) (i: Usize) (x: α)
∃ nv, v.insert α i x = ret nv ∧ nv.val = v.val.update i.val x := by
simp [insert, *]
-def Vec.index_shared (α : Type u) (v: Vec α) (i: Usize) : Result α :=
+def Vec.index_usize (α : Type u) (v: Vec α) (i: Usize) : Result α :=
match v.val.indexOpt i.val with
| none => fail .arrayOutOfBounds
| some x => ret x
@@ -90,51 +92,65 @@ def Vec.index_shared (α : Type u) (v: Vec α) (i: Usize) : Result α :=
-/
@[pspec]
-theorem Vec.index_shared_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize)
+theorem Vec.index_usize_spec {α : Type u} [Inhabited α] (v: Vec α) (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 [*]
--- This shouldn't be used
-def Vec.index_back (α : Type u) (v: Vec α) (i: Usize) (_: α) : Result Unit :=
- if i.val < List.length v.val then
- .ret ()
- else
- .fail arrayOutOfBounds
-
-def Vec.index_mut (α : Type u) (v: Vec α) (i: Usize) : Result α :=
- match v.val.indexOpt i.val with
- | none => fail .arrayOutOfBounds
- | some x => ret x
-
-@[pspec]
-theorem Vec.index_mut_spec {α : Type u} [Inhabited α] (v: Vec α) (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 Vec.index_mut_back (α : Type u) (v: Vec α) (i: Usize) (x: α) : Result (Vec α) :=
+def Vec.update_usize (α : Type u) (v: Vec α) (i: Usize) (x: α) : Result (Vec α) :=
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 Vec.index_mut_back_spec {α : Type u} (v: Vec α) (i: Usize) (x : α)
+theorem Vec.update_usize_spec {α : Type u} (v: Vec α) (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
. simp_all
+/- [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 :=
+ sorry -- TODO
+
+/- [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) :=
+ sorry -- TODO
+
+/- Trait implementation: [alloc::vec::Vec] -/
+def Vec.coreopsindexIndexInst (T I : Type)
+ (inst : core.slice.index.SliceIndex I (Slice T)) :
+ core.ops.index.Index (alloc.vec.Vec T) I := {
+ Output := inst.Output
+ index := Vec.index T I inst
+}
+
+/- Trait implementation: [alloc::vec::Vec] -/
+def Vec.coreopsindexIndexMutInst (T I : Type)
+ (inst : core.slice.index.SliceIndex I (Slice T)) :
+ 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
+}
+
+end alloc.vec
+
end Primitives
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index ecf05dab..24c6f912 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -383,6 +383,7 @@ namespace Test
-- #eval showStoredPSpec
-- #eval showStoredPSpecClass
-- #eval showStoredPSpecExprClass
+ open alloc.vec
example {ty} {x y : Scalar ty}
(hmin : Scalar.min ty ≤ x.val + y.val)
@@ -408,7 +409,7 @@ namespace Test
`α : Type u` where u is quantified, while here we use `α : Type 0` -/
example {α : Type} (v: Vec α) (i: Usize) (x : α)
(hbounds : 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
progress
simp [*]