From e3cb3646bbe3d50240aa0bf4763f8e816fb9a706 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 25 Oct 2023 15:36:06 +0200
Subject: Fix some issues at extraction and add builtins

---
 backends/lean/Base/Primitives/ArraySlice.lean | 560 ++++++++++++++++++++++++++
 1 file changed, 560 insertions(+)
 create mode 100644 backends/lean/Base/Primitives/ArraySlice.lean

(limited to 'backends/lean/Base/Primitives/ArraySlice.lean')

diff --git a/backends/lean/Base/Primitives/ArraySlice.lean b/backends/lean/Base/Primitives/ArraySlice.lean
new file mode 100644
index 00000000..47807a0d
--- /dev/null
+++ b/backends/lean/Base/Primitives/ArraySlice.lean
@@ -0,0 +1,560 @@
+/- Arrays/Slices -/
+import Lean
+import Lean.Meta.Tactic.Simp
+import Init.Data.List.Basic
+import Mathlib.Tactic.RunCmd
+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
+
+namespace Primitives
+
+open Result Error
+
+def Array (α : Type u) (n : Usize) := { l : List α // l.length = n.val }
+
+instance (a : Type u) (n : Usize) : Arith.HasIntProp (Array a n) where
+  prop_ty := λ v => v.val.len = n.val
+  prop := λ ⟨ _, l ⟩ => by simp[Scalar.max, List.len_eq_length, *]
+
+instance {α : Type u} {n : Usize} (p : Array α n → Prop) : Arith.HasIntProp (Subtype p) where
+  prop_ty := λ x => p x
+  prop := λ x => x.property
+
+@[simp]
+abbrev Array.length {α : Type u} {n : Usize} (v : Array α n) : Int := v.val.len
+
+@[simp]
+abbrev Array.v {α : Type u} {n : Usize} (v : Array α n) : List α := v.val
+
+example {α: Type u} {n : Usize} (v : Array α n) : v.length ≤ Scalar.max ScalarTy.Usize := by
+  scalar_tac
+
+def Array.make (α : Type u) (n : Usize) (init : List α) (hl : init.len = n.val := by decide) :
+  Array α n := ⟨ init, by simp [← List.len_eq_length]; apply hl ⟩
+
+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) : α :=
+  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 α :=
+  match v.val.indexOpt i.val with
+  | none => fail .arrayOutOfBounds
+  | some x => ret x
+
+-- For initialization
+def Array.repeat (α : Type u) (n : Usize) (x : α) : Array α n :=
+  ⟨ List.ireplicate n.val x, by have h := n.hmin; simp_all [Scalar.min] ⟩
+
+@[pspec]
+theorem Array.repeat_spec {α : Type u} (n : Usize) (x : α) :
+  ∃ a, Array.repeat α n x = a ∧ a.val = List.ireplicate n.val x := by
+  simp [Array.repeat]
+
+/- In the theorems below: we don't always need the `∃ ..`, but we use one
+   so that `progress` introduces an opaque variable and an equality. This
+   helps control the context.
+ -/
+
+@[pspec]
+theorem Array.index_shared_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]
+  -- 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) :=
+  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 : α)
+  (hbound : i.val < v.length) :
+  ∃ nv, v.index_mut_back α n i x = ret nv ∧
+  nv.val = v.val.update i.val x
+  := by
+  simp only [index_mut_back]
+  have h := List.indexOpt_bounds v.val i.val
+  split
+  . simp_all [length]; cases h <;> scalar_tac
+  . simp_all
+
+def Slice (α : Type u) := { l : List α // l.length ≤ Usize.max }
+
+instance (a : Type u) : Arith.HasIntProp (Slice a) where
+  prop_ty := λ v => 0 ≤ v.val.len ∧ v.val.len ≤ Scalar.max ScalarTy.Usize
+  prop := λ ⟨ _, l ⟩ => by simp[Scalar.max, List.len_eq_length, *]
+
+instance {α : Type u} (p : Slice α → Prop) : Arith.HasIntProp (Subtype p) where
+  prop_ty := λ x => p x
+  prop := λ x => x.property
+
+@[simp]
+abbrev Slice.length {α : Type u} (v : Slice α) : Int := v.val.len
+
+@[simp]
+abbrev Slice.v {α : Type u} (v : Slice α) : List α := v.val
+
+example {a: Type u} (v : Slice a) : v.length ≤ Scalar.max ScalarTy.Usize := by
+  scalar_tac
+
+def Slice.new (α : Type u): Slice α := ⟨ [], by apply Scalar.cMax_suffices .Usize; simp ⟩
+
+-- TODO: very annoying that the α is an explicit parameter
+def Slice.len (α : Type u) (v : Slice α) : Usize :=
+  Usize.ofIntCore v.val.len (by scalar_tac) (by scalar_tac)
+
+@[simp]
+theorem Slice.len_val {α : Type u} (v : Slice α) : (Slice.len α v).val = v.length :=
+  by rfl
+
+@[simp]
+abbrev Slice.index {α : 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 α :=
+  match v.val.indexOpt i.val with
+  | none => fail .arrayOutOfBounds
+  | some x => ret x
+
+/- In the theorems below: we don't always need the `∃ ..`, but we use one
+   so that `progress` introduces an opaque variable and an equality. This
+   helps control the context.
+ -/
+
+@[pspec]
+theorem Slice.index_shared_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]
+  -- 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 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.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 α) :=
+  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 : α)
+  (hbound : i.val < v.length) :
+  ∃ nv, v.index_mut_back α i x = ret nv ∧
+  nv.val = v.val.update i.val x
+  := by
+  simp only [index_mut_back]
+  have h := List.indexOpt_bounds v.val i.val
+  split
+  . simp_all [length]; cases h <;> scalar_tac
+  . simp_all
+
+/- 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.
+   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 α) :=
+  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
+
+@[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) :=
+  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, *]
+
+def Array.subslice_shared (α : 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,
+          by
+            simp [← List.len_eq_length]
+            have := a.val.slice_len_le r.start.val r.end_.val
+            scalar_tac ⟩
+  else
+    fail panic
+
+@[pspec]
+theorem Array.subslice_shared_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.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, *]
+  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) :=
+  -- 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
+    let s_end := a.val.idrop r.end_.val
+    have : s_beg.len = r.start.val := by
+      apply List.itake_len
+      . simp_all; scalar_tac
+      . scalar_tac
+    have : s_end.len = a.val.len - r.end_.val := by
+      apply List.idrop_len
+      . scalar_tac
+      . scalar_tac
+    let na := s_beg.append (s.val.append s_end)
+    have : na.len = a.val.len := by simp [*]
+    ret ⟨ na, by simp_all [← List.len_eq_length]; scalar_tac ⟩
+  else
+    fail panic
+
+-- TODO: it is annoying to write `.val` everywhere. We could leverage coercions,
+-- 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).
+@[pspec]
+theorem Array.subslice_mut_back_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, *]
+  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
+  have ⟨ h0, h1, h2 ⟩ := h
+  clear h
+  split_conjs
+  . intro i _ _
+    have := h0 i (by int_tac) (by int_tac)
+    simp [*]
+  . intro i _ _
+    have := h1 i (by int_tac) (by int_tac)
+    simp [*]
+  . intro i _ _
+    have := h2 i (by int_tac) (by int_tac)
+    simp [*]
+
+def Slice.subslice_shared (α : 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,
+          by
+            simp [← List.len_eq_length]
+            have := s.val.slice_len_le r.start.val r.end_.val
+            scalar_tac ⟩
+  else
+    fail panic
+
+@[pspec]
+theorem Slice.subslice_shared_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.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))
+  := by
+  simp [subslice_shared, *]
+  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 α) :=
+  -- 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
+    let s_end := s.val.idrop r.end_.val
+    have : s_beg.len = r.start.val := by
+      apply List.itake_len
+      . simp_all; scalar_tac
+      . scalar_tac
+    have : s_end.len = s.val.len - r.end_.val := by
+      apply List.idrop_len
+      . scalar_tac
+      . scalar_tac
+    let ns := s_beg.append (ss.val.append s_end)
+    have : ns.len = s.val.len := by simp [*]
+    ret ⟨ ns, by simp_all [← List.len_eq_length]; scalar_tac ⟩
+  else
+    fail panic
+
+@[pspec]
+theorem Slice.subslice_mut_back_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, *]
+  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
+  have ⟨ h0, h1, h2 ⟩ := h
+  clear h
+  split_conjs
+  . intro i _ _
+    have := h0 i (by int_tac) (by int_tac)
+    simp [*]
+  . intro i _ _
+    have := h1 i (by int_tac) (by int_tac)
+    simp [*]
+  . intro i _ _
+    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
-- 
cgit v1.2.3


From 81b7a7d706bc1a0f2f57bc254a8af158039a10cf Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 25 Oct 2023 18:44:28 +0200
Subject: Make the hashmap files typecheck again in Lean

---
 backends/lean/Base/Primitives/ArraySlice.lean | 61 ++++++++++++++++++++++++++-
 1 file changed, 59 insertions(+), 2 deletions(-)

(limited to 'backends/lean/Base/Primitives/ArraySlice.lean')

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
-- 
cgit v1.2.3


From ca24c351f97a3f8989a6866de0868ef54241b194 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 26 Oct 2023 12:07:50 +0200
Subject: Make progress on fixing the extraction for Lean

---
 backends/lean/Base/Primitives/ArraySlice.lean | 164 ++++++++------------------
 1 file changed, 50 insertions(+), 114 deletions(-)

(limited to 'backends/lean/Base/Primitives/ArraySlice.lean')

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
-- 
cgit v1.2.3


From 442f0aede5da127b4828a90bcbade73a345340e3 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 26 Oct 2023 14:10:57 +0200
Subject: Make progress on fixing the extraction

---
 backends/lean/Base/Primitives/ArraySlice.lean | 128 +++++++++++++-------------
 1 file changed, 64 insertions(+), 64 deletions(-)

(limited to 'backends/lean/Base/Primitives/ArraySlice.lean')

diff --git a/backends/lean/Base/Primitives/ArraySlice.lean b/backends/lean/Base/Primitives/ArraySlice.lean
index 2a080ca6..cfc9a6b2 100644
--- a/backends/lean/Base/Primitives/ArraySlice.lean
+++ b/backends/lean/Base/Primitives/ArraySlice.lean
@@ -341,110 +341,110 @@ theorem Slice.update_subslice_spec {α : Type u} [Inhabited α] (a : Slice α) (
 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
+structure core.slice.index.SliceIndex (Self T : 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
+  get : Self → T → Result (Option Output)
+  get_mut : Self → T → Result (Option Output)
+  get_mut_back : Self → T → 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
 
 /- [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
+  (T I : Type) (inst : core.slice.index.SliceIndex I (Slice T))
+  (slice : Slice T) (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)) :=
+def core.slice.index.Range.get (T : Type) (i : Range Usize) (slice : Slice T) :
+  Result (Option (Slice T)) :=
   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)) :=
+  (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.Range.get_mut_back
-  (T0 : Type) :
-  Range Usize → Slice T0 → Option (Slice T0) → Result (Slice T0) :=
+  (T : Type) :
+  Range Usize → Slice T → Option (Slice T) → Result (Slice T) :=
   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)) :=
+  (T : Type) :
+  Range Usize → ConstRawPtr (Slice T) → Result (ConstRawPtr (Slice T)) :=
   -- 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)) :=
+  (T : Type) :
+  Range Usize → MutRawPtr (Slice T) → Result (MutRawPtr (Slice T)) :=
   -- 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) :=
+  (T : Type) : Range Usize → Slice T → Result (Slice T) :=
   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) :=
+  (T : Type) : Range Usize → Slice T → Result (Slice T) :=
   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) :=
+  (T : Type) : Range Usize → Slice T → Slice T → Result (Slice T) :=
   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 :=
+  (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
-  (T0 I : Type) (inst : core.slice.index.SliceIndex I (Slice T0)) :
-  Slice T0 → I → inst.Output → Result (Slice T0) :=
+  (T I : Type) (inst : core.slice.index.SliceIndex I (Slice T)) :
+  Slice T → I → inst.Output → Result (Slice T) :=
   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 :=
+  (T I : Type) (N : Usize) (inst : core.ops.index.Index (Slice T) I)
+  (a : Array T N) (i : 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 :=
+  (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
-  (T0 I : Type) (N : Usize) (inst : core.ops.index.IndexMut (Slice T0) I) :
-  Array T0 N → I → inst.indexInst.Output → Result (Array T0 N) :=
+  (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) :=
   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 := {
+def core.slice.index.Slice.coreopsindexIndexInst (T I : Type)
+  (inst : core.slice.index.SliceIndex I (Slice T)) :
+  core.ops.index.Index (Slice T) I := {
   Output := inst.Output
-  index := core.slice.index.Slice.index T0 I inst
+  index := core.slice.index.Slice.index T I inst
 }
 
 /- Trait implementation: [core::slice::index::private_slice_index::Range] -/
@@ -452,45 +452,45 @@ def core.slice.index.private_slice_index.Range.coresliceindexprivate_slice_index
   : 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) := {
+def core.slice.index.Range.coresliceindexSliceIndexInst (T : Type) :
+  core.slice.index.SliceIndex (Range Usize) (Slice T) := {
   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
+  Output := Slice T
+  get := core.slice.index.Range.get T
+  get_mut := core.slice.index.Range.get_mut T
+  get_mut_back := core.slice.index.Range.get_mut_back T
+  get_unchecked := core.slice.index.Range.get_unchecked T
+  get_unchecked_mut := core.slice.index.Range.get_unchecked_mut T
+  index := core.slice.index.Range.index T
+  index_mut := core.slice.index.Range.index_mut T
+  index_mut_back := core.slice.index.Range.index_mut_back T
 }
 
 /- 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
+def core.slice.index.Slice.coreopsindexIndexMutInst (T I : Type)
+  (inst : core.slice.index.SliceIndex I (Slice T)) :
+  core.ops.index.IndexMut (Slice T) I := {
+  indexInst := core.slice.index.Slice.coreopsindexIndexInst 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]] -/
-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 := {
+def core.array.Array.coreopsindexIndexInst (T I : Type) (N : Usize)
+  (inst : core.ops.index.Index (Slice T) I) :
+  core.ops.index.Index (Array T N) I := {
   Output := inst.Output
-  index := core.array.Array.index T0 I N inst
+  index := core.array.Array.index T 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
+def core.array.Array.coreopsindexIndexMutInst (T I : Type) (N : Usize)
+  (inst : core.ops.index.IndexMut (Slice T) I) :
+  core.ops.index.IndexMut (Array T N) I := {
+  indexInst := core.array.Array.coreopsindexIndexInst 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 -/
-- 
cgit v1.2.3


From c3b6ad3685995b3b96dc88789e8512560d3257b3 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 21 Nov 2023 10:23:14 +0100
Subject: Update the standard libraries

---
 backends/lean/Base/Primitives/ArraySlice.lean | 39 +++++++++++++--------------
 1 file changed, 19 insertions(+), 20 deletions(-)

(limited to 'backends/lean/Base/Primitives/ArraySlice.lean')

diff --git a/backends/lean/Base/Primitives/ArraySlice.lean b/backends/lean/Base/Primitives/ArraySlice.lean
index cfc9a6b2..8bb9a855 100644
--- a/backends/lean/Base/Primitives/ArraySlice.lean
+++ b/backends/lean/Base/Primitives/ArraySlice.lean
@@ -439,23 +439,14 @@ def core.array.Array.index_mut_back
   (a : Array T N) (i : I) (x : inst.indexInst.Output) : Result (Array T N) :=
   sorry -- TODO
 
-/- Trait implementation: [core::slice::index::[T]] -/
-def core.slice.index.Slice.coreopsindexIndexInst (T I : Type)
-  (inst : core.slice.index.SliceIndex I (Slice T)) :
-  core.ops.index.Index (Slice T) I := {
-  Output := inst.Output
-  index := core.slice.index.Slice.index T I inst
-}
-
 /- Trait implementation: [core::slice::index::private_slice_index::Range] -/
-def core.slice.index.private_slice_index.Range.coresliceindexprivate_slice_indexSealedInst
+def core.slice.index.private_slice_index.SealedRangeUsizeInst
   : core.slice.index.private_slice_index.Sealed (Range Usize) := {}
 
 /- Trait implementation: [core::slice::index::Range] -/
-def core.slice.index.Range.coresliceindexSliceIndexInst (T : Type) :
+def core.slice.index.SliceIndexRangeUsizeSliceTInst (T : Type) :
   core.slice.index.SliceIndex (Range Usize) (Slice T) := {
-  sealedInst :=
-    core.slice.index.private_slice_index.Range.coresliceindexprivate_slice_indexSealedInst
+  sealedInst := core.slice.index.private_slice_index.SealedRangeUsizeInst
   Output := Slice T
   get := core.slice.index.Range.get T
   get_mut := core.slice.index.Range.get_mut T
@@ -468,16 +459,24 @@ def core.slice.index.Range.coresliceindexSliceIndexInst (T : Type) :
 }
 
 /- Trait implementation: [core::slice::index::[T]] -/
-def core.slice.index.Slice.coreopsindexIndexMutInst (T I : Type)
+def core.ops.index.IndexSliceTIInst (T I : Type)
+  (inst : core.slice.index.SliceIndex I (Slice T)) :
+  core.ops.index.Index (Slice T) I := {
+  Output := inst.Output
+  index := core.slice.index.Slice.index T I inst
+}
+
+/- Trait implementation: [core::slice::index::[T]] -/
+def core.ops.index.IndexMutSliceTIInst (T I : Type)
   (inst : core.slice.index.SliceIndex I (Slice T)) :
   core.ops.index.IndexMut (Slice T) I := {
-  indexInst := core.slice.index.Slice.coreopsindexIndexInst T I inst
+  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]] -/
-def core.array.Array.coreopsindexIndexInst (T I : Type) (N : Usize)
+def core.ops.index.IndexArrayIInst (T I : Type) (N : Usize)
   (inst : core.ops.index.Index (Slice T) I) :
   core.ops.index.Index (Array T N) I := {
   Output := inst.Output
@@ -485,10 +484,10 @@ def core.array.Array.coreopsindexIndexInst (T I : Type) (N : Usize)
 }
 
 /- Trait implementation: [core::array::[T; N]] -/
-def core.array.Array.coreopsindexIndexMutInst (T I : Type) (N : Usize)
+def core.ops.index.IndexMutArrayIInst (T I : Type) (N : Usize)
   (inst : core.ops.index.IndexMut (Slice T) I) :
   core.ops.index.IndexMut (Array T N) I := {
-  indexInst := core.array.Array.coreopsindexIndexInst T I N inst.indexInst
+  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
 }
@@ -532,13 +531,13 @@ def core.slice.index.Usize.index_mut_back
   sorry -- TODO
 
 /- Trait implementation: [core::slice::index::private_slice_index::usize] -/
-def core.slice.index.private_slice_index.usize.coresliceindexprivate_slice_indexSealedInst
+def core.slice.index.private_slice_index.SealedUsizeInst
   : core.slice.index.private_slice_index.Sealed Usize := {}
 
 /- Trait implementation: [core::slice::index::usize] -/
-def core.slice.index.usize.coresliceindexSliceIndexInst (T : Type) :
+def core.slice.index.SliceIndexUsizeSliceTInst (T : Type) :
   core.slice.index.SliceIndex Usize (Slice T) := {
-  sealedInst := core.slice.index.private_slice_index.usize.coresliceindexprivate_slice_indexSealedInst
+  sealedInst := core.slice.index.private_slice_index.SealedUsizeInst
   Output := T
   get := core.slice.index.Usize.get T
   get_mut := core.slice.index.Usize.get_mut T
-- 
cgit v1.2.3


From 1dbdd9e316e690e5c63de2e1923afad520c76e4d Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Tue, 21 Nov 2023 10:27:08 +0100
Subject: Update more names

---
 backends/lean/Base/Primitives/ArraySlice.lean | 32 +++++++++++++--------------
 1 file changed, 16 insertions(+), 16 deletions(-)

(limited to 'backends/lean/Base/Primitives/ArraySlice.lean')

diff --git a/backends/lean/Base/Primitives/ArraySlice.lean b/backends/lean/Base/Primitives/ArraySlice.lean
index 8bb9a855..f68c0846 100644
--- a/backends/lean/Base/Primitives/ArraySlice.lean
+++ b/backends/lean/Base/Primitives/ArraySlice.lean
@@ -363,23 +363,23 @@ def core.slice.index.Slice.index
   | some x => ret x
 
 /- [core::slice::index::Range:::get]: forward function -/
-def core.slice.index.Range.get (T : Type) (i : Range Usize) (slice : Slice T) :
+def core.slice.index.RangeUsize.get (T : Type) (i : Range Usize) (slice : Slice T) :
   Result (Option (Slice T)) :=
   sorry -- TODO
 
 /- [core::slice::index::Range::get_mut]: forward function -/
-def core.slice.index.Range.get_mut
+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.Range.get_mut_back
+def core.slice.index.RangeUsize.get_mut_back
   (T : Type) :
   Range Usize → Slice T → Option (Slice T) → Result (Slice T) :=
   sorry -- TODO
 
 /- [core::slice::index::Range::get_unchecked]: forward function -/
-def core.slice.index.Range.get_unchecked
+def core.slice.index.RangeUsize.get_unchecked
   (T : Type) :
   Range Usize → ConstRawPtr (Slice T) → Result (ConstRawPtr (Slice T)) :=
   -- Don't know what the model should be - for now we always fail to make
@@ -387,7 +387,7 @@ def core.slice.index.Range.get_unchecked
   fun _ _ => fail panic
 
 /- [core::slice::index::Range::get_unchecked_mut]: forward function -/
-def core.slice.index.Range.get_unchecked_mut
+def core.slice.index.RangeUsize.get_unchecked_mut
   (T : Type) :
   Range Usize → MutRawPtr (Slice T) → Result (MutRawPtr (Slice T)) :=
   -- Don't know what the model should be - for now we always fail to make
@@ -395,17 +395,17 @@ def core.slice.index.Range.get_unchecked_mut
   fun _ _ => fail panic
 
 /- [core::slice::index::Range::index]: forward function -/
-def core.slice.index.Range.index
+def core.slice.index.RangeUsize.index
   (T : Type) : Range Usize → Slice T → Result (Slice T) :=
   sorry -- TODO
 
 /- [core::slice::index::Range::index_mut]: forward function -/
-def core.slice.index.Range.index_mut
+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.Range.index_mut_back
+def core.slice.index.RangeUsize.index_mut_back
   (T : Type) : Range Usize → Slice T → Slice T → Result (Slice T) :=
   sorry -- TODO
 
@@ -448,14 +448,14 @@ def core.slice.index.SliceIndexRangeUsizeSliceTInst (T : Type) :
   core.slice.index.SliceIndex (Range Usize) (Slice T) := {
   sealedInst := core.slice.index.private_slice_index.SealedRangeUsizeInst
   Output := Slice T
-  get := core.slice.index.Range.get T
-  get_mut := core.slice.index.Range.get_mut T
-  get_mut_back := core.slice.index.Range.get_mut_back T
-  get_unchecked := core.slice.index.Range.get_unchecked T
-  get_unchecked_mut := core.slice.index.Range.get_unchecked_mut T
-  index := core.slice.index.Range.index T
-  index_mut := core.slice.index.Range.index_mut T
-  index_mut_back := core.slice.index.Range.index_mut_back 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]] -/
-- 
cgit v1.2.3