Fix some issues at extraction and add builtins

7 files changed, 206 insertions, 23 deletions

diff --git a/backends/lean/Base/Primitives.lean b/backends/lean/Base/Primitives.lean
index 22378af7..613b6076 100644
--- a/backends/lean/Base/Primitives.lean
+++ b/backends/lean/Base/Primitives.lean
@@ -1,6 +1,6 @@
 import Base.Primitives.Base
 import Base.Primitives.Scalar
-import Base.Primitives.Array
+import Base.Primitives.ArraySlice
 import Base.Primitives.Vec
 import Base.Primitives.Alloc
-import Base.Primitives.CoreOpsDeref
+import Base.Primitives.CoreOps
diff --git a/backends/lean/Base/Primitives/Alloc.lean b/backends/lean/Base/Primitives/Alloc.lean
index 0580421f..34590499 100644
--- a/backends/lean/Base/Primitives/Alloc.lean
+++ b/backends/lean/Base/Primitives/Alloc.lean
@@ -1,6 +1,6 @@
 import Lean
 import Base.Primitives.Base
-import Base.Primitives.CoreOpsDeref
+import Base.Primitives.CoreOps
 
 open Primitives
 open Result
diff --git a/backends/lean/Base/Primitives/Array.lean b/backends/lean/Base/Primitives/ArraySlice.lean
index 49c84bee..47807a0d 100644
--- a/backends/lean/Base/Primitives/Array.lean
+++ b/backends/lean/Base/Primitives/ArraySlice.lean
@@ -1,4 +1,4 @@
-/- Arrays/slices -/
+/- Arrays/Slices -/
 import Lean
 import Lean.Meta.Tactic.Simp
 import Init.Data.List.Basic
@@ -7,6 +7,7 @@ import Mathlib.Tactic.Linarith
 import Base.IList
 import Base.Primitives.Scalar
 import Base.Primitives.Range
+import Base.Primitives.CoreOps
 import Base.Arith
 import Base.Progress.Base
 
@@ -400,4 +401,160 @@ theorem Slice.subslice_mut_back_spec {α : Type u} [Inhabited α] (a : Slice α)
     have := h2 i (by int_tac) (by int_tac)
     simp [*]
 
+/- Trait declaration: [core::slice::index::private_slice_index::Sealed] -/
+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
+  Output : Type
+  get : Self → T0 → Result (Option Output)
+  get_mut : Self → T0 → Result (Option Output)
+  get_mut_back : Self → T0 → Option Output → Result T0
+  get_unchecked : Self → ConstRawPtr T0 → Result (ConstRawPtr Output)
+  get_unchecked_mut : Self → MutRawPtr T0 → Result (MutRawPtr Output)
+  index : Self → T0 → Result Output
+  index_mut : Self → T0 → Result Output
+  index_mut_back : Self → T0 → Output → Result T0
+
+/- [core::slice::index::[T]::index]: forward function -/
+def core.slice.index.Slice.index
+  (T0 I : Type) (inst : core.slice.index.SliceIndex I (Slice T0))
+  (slice : Slice T0) (i : I) : Result inst.Output := do
+  let x ← inst.get i slice
+  match x with
+  | none => fail panic
+  | some x => ret x
+
+/- [core::slice::index::Range:::get]: forward function -/
+def core.slice.index.Range.get (T0 : Type) (i : Range Usize) (slice : Slice T0) :
+  Result (Option (Slice T0)) :=
+  sorry -- TODO
+
+/- [core::slice::index::Range::get_mut]: forward function -/
+def core.slice.index.Range.get_mut
+  (T0 : Type) : Range Usize → Slice T0 → Result (Option (Slice T0)) :=
+  sorry -- TODO
+
+/- [core::slice::index::Range::get_mut]: backward function 0 -/
+def core.slice.index.Range.get_mut_back
+  (T0 : Type) :
+  Range Usize → Slice T0 → Option (Slice T0) → Result (Slice T0) :=
+  sorry -- TODO
+
+/- [core::slice::index::Range::get_unchecked]: forward function -/
+def core.slice.index.Range.get_unchecked
+  (T0 : Type) :
+  Range Usize → ConstRawPtr (Slice T0) → Result (ConstRawPtr (Slice T0)) :=
+  -- Don't know what the model should be - for now we always fail to make
+  -- sure code which uses it fails
+  fun _ _ => fail panic
+
+/- [core::slice::index::Range::get_unchecked_mut]: forward function -/
+def core.slice.index.Range.get_unchecked_mut
+  (T0 : Type) :
+  Range Usize → MutRawPtr (Slice T0) → Result (MutRawPtr (Slice T0)) :=
+  -- Don't know what the model should be - for now we always fail to make
+  -- sure code which uses it fails
+  fun _ _ => fail panic
+
+/- [core::slice::index::Range::index]: forward function -/
+def core.slice.index.Range.index
+  (T0 : Type) : Range Usize → Slice T0 → Result (Slice T0) :=
+  sorry -- TODO
+
+/- [core::slice::index::Range::index_mut]: forward function -/
+def core.slice.index.Range.index_mut
+  (T0 : Type) : Range Usize → Slice T0 → Result (Slice T0) :=
+  sorry -- TODO
+
+/- [core::slice::index::Range::index_mut]: backward function 0 -/
+def core.slice.index.Range.index_mut_back
+  (T0 : Type) : Range Usize → Slice T0 → Slice T0 → Result (Slice T0) :=
+  sorry -- TODO
+
+/- [core::slice::index::[T]::index_mut]: forward function -/
+def core.slice.index.Slice.index_mut
+  (T0 I : Type) (inst : core.slice.index.SliceIndex I (Slice T0)) :
+  Slice T0 → I → Result inst.Output :=
+  sorry -- TODO
+
+/- [core::slice::index::[T]::index_mut]: backward function 0 -/
+def core.slice.index.Slice.index_mut_back
+  (T0 I : Type) (inst : core.slice.index.SliceIndex I (Slice T0)) :
+  Slice T0 → I → inst.Output → Result (Slice T0) :=
+  sorry -- TODO
+
+/- [core::array::[T; N]::index]: forward function -/
+def core.array.Array.index
+  (T0 I : Type) (N : Usize) (inst : core.ops.index.Index (Slice T0) I) :
+  Array T0 N → I → Result inst.Output :=
+  sorry -- TODO
+
+/- [core::array::[T; N]::index_mut]: forward function -/
+def core.array.Array.index_mut
+  (T0 I : Type) (N : Usize) (inst : core.ops.index.IndexMut (Slice T0) I) :
+  Array T0 N → I → Result inst.indexInst.Output :=
+  sorry -- TODO
+
+/- [core::array::[T; N]::index_mut]: backward function 0 -/
+def core.array.Array.index_mut_back
+  (T0 I : Type) (N : Usize) (inst : core.ops.index.IndexMut (Slice T0) I) :
+  Array T0 N → I → inst.indexInst.Output → Result (Array T0 N) :=
+  sorry -- TODO
+
+/- Trait implementation: [core::slice::index::[T]] -/
+def core.slice.index.Slice.coreopsindexIndexInst (T0 I : Type)
+  (inst : core.slice.index.SliceIndex I (Slice T0)) :
+  core.ops.index.Index (Slice T0) I := {
+  Output := inst.Output
+  index := core.slice.index.Slice.index T0 I inst
+}
+
+/- Trait implementation: [core::slice::index::private_slice_index::Range] -/
+def core.slice.index.private_slice_index.Range.coresliceindexprivate_slice_indexSealedInst
+  : core.slice.index.private_slice_index.Sealed (Range Usize) := {}
+
+/- Trait implementation: [core::slice::index::Range] -/
+def core.slice.index.Range.coresliceindexSliceIndexInst (T0 : Type) :
+  core.slice.index.SliceIndex (Range Usize) (Slice T0) := {
+  sealedInst :=
+    core.slice.index.private_slice_index.Range.coresliceindexprivate_slice_indexSealedInst
+  Output := Slice T0
+  get := core.slice.index.Range.get T0
+  get_mut := core.slice.index.Range.get_mut T0
+  get_mut_back := core.slice.index.Range.get_mut_back T0
+  get_unchecked := core.slice.index.Range.get_unchecked T0
+  get_unchecked_mut := core.slice.index.Range.get_unchecked_mut T0
+  index := core.slice.index.Range.index T0
+  index_mut := core.slice.index.Range.index_mut T0
+  index_mut_back := core.slice.index.Range.index_mut_back T0
+}
+
+/- Trait implementation: [core::slice::index::[T]] -/
+def core.slice.index.Slice.coreopsindexIndexMutInst (T0 I : Type)
+  (inst : core.slice.index.SliceIndex I (Slice T0)) :
+  core.ops.index.IndexMut (Slice T0) I := {
+  indexInst := core.slice.index.Slice.coreopsindexIndexInst T0 I inst
+  index_mut := core.slice.index.Slice.index_mut T0 I inst
+  index_mut_back := core.slice.index.Slice.index_mut_back T0 I inst
+}
+
+/- Trait implementation: [core::array::[T; N]] -/
+def core.array.Array.coreopsindexIndexInst (T0 I : Type) (N : Usize)
+  (inst : core.ops.index.Index (Slice T0) I) :
+  core.ops.index.Index (Array T0 N) I := {
+  Output := inst.Output
+  index := core.array.Array.index T0 I N inst
+}
+
+/- Trait implementation: [core::array::[T; N]] -/
+def core.array.Array.coreopsindexIndexMutInst (T0 I : Type) (N : Usize)
+  (inst : core.ops.index.IndexMut (Slice T0) I) :
+  core.ops.index.IndexMut (Array T0 N) I := {
+  indexInst := core.array.Array.coreopsindexIndexInst T0 I N inst.indexInst
+  index_mut := core.array.Array.index_mut T0 I N inst
+  index_mut_back := core.array.Array.index_mut_back T0 I N inst
+}
+
 end Primitives
diff --git a/backends/lean/Base/Primitives/Base.lean b/backends/lean/Base/Primitives/Base.lean
index 10af8f67..7fc33251 100644
--- a/backends/lean/Base/Primitives/Base.lean
+++ b/backends/lean/Base/Primitives/Base.lean
@@ -127,4 +127,11 @@ def Result.attach {α: Type} (o : Result α): Result { x : α // o = ret x } :=
  Use with `simp [ aeneas ]` -/
 register_simp_attr aeneas
 
+-- We don't really use raw pointers for now
+structure MutRawPtr (T : Type) where
+  v : T
+
+structure ConstRawPtr (T : Type) where
+  v : T
+
 end Primitives
diff --git a/backends/lean/Base/Primitives/CoreOps.lean b/backends/lean/Base/Primitives/CoreOps.lean
new file mode 100644
index 00000000..da458f66
--- /dev/null
+++ b/backends/lean/Base/Primitives/CoreOps.lean
@@ -0,0 +1,37 @@
+import Lean
+import Base.Primitives.Base
+
+open Primitives
+open Result
+
+namespace core.ops
+
+namespace index -- core.ops.index
+
+/- Trait declaration: [core::ops::index::Index] -/
+structure Index (Self Idx : Type) where
+  Output : Type
+  index : Self → Idx → Result Output
+
+/- 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
+
+end index -- core.ops.index
+
+namespace deref -- core.ops.deref
+
+structure Deref (Self : Type) where
+  Target : Type
+  deref : Self → Result Target
+
+structure DerefMut (Self : Type) where
+  derefInst : Deref Self
+  deref_mut : Self → Result derefInst.Target
+  deref_mut_back : Self → derefInst.Target → Result Self
+
+end deref -- core.ops.deref
+
+end core.ops
diff --git a/backends/lean/Base/Primitives/CoreOpsDeref.lean b/backends/lean/Base/Primitives/CoreOpsDeref.lean
deleted file mode 100644
index 2b540012..00000000
--- a/backends/lean/Base/Primitives/CoreOpsDeref.lean
+++ /dev/null
@@ -1,18 +0,0 @@
-import Lean
-import Base.Primitives.Base
-
-open Primitives
-open Result
-
-namespace core.ops.deref
-
-structure Deref (Self : Type) where
-  Target : Type
-  deref : Self → Result Target
-
-structure DerefMut (Self : Type) where
-  derefInst : Deref Self
-  deref_mut : Self → Result derefInst.Target
-  deref_mut_back : Self → derefInst.Target → Result Self
-
-end core.ops.deref
diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean
index c4c4d9f2..99fcedc6 100644
--- a/backends/lean/Base/Primitives/Vec.lean
+++ b/backends/lean/Base/Primitives/Vec.lean
@@ -6,7 +6,7 @@ import Mathlib.Tactic.RunCmd
 import Mathlib.Tactic.Linarith
 import Base.IList
 import Base.Primitives.Scalar
-import Base.Primitives.Array
+import Base.Primitives.ArraySlice
 import Base.Arith
 import Base.Progress.Base