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.lean | 4 +- backends/lean/Base/Primitives/Alloc.lean | 2 +- backends/lean/Base/Primitives/Array.lean | 403 ----------------- backends/lean/Base/Primitives/ArraySlice.lean | 560 ++++++++++++++++++++++++ backends/lean/Base/Primitives/Base.lean | 7 + backends/lean/Base/Primitives/CoreOps.lean | 37 ++ backends/lean/Base/Primitives/CoreOpsDeref.lean | 18 - backends/lean/Base/Primitives/Vec.lean | 2 +- compiler/Extract.ml | 45 +- compiler/ExtractBuiltin.ml | 304 ++++++++++++- compiler/LlbcAstUtils.ml | 19 +- compiler/Translate.ml | 10 +- 12 files changed, 948 insertions(+), 463 deletions(-) delete mode 100644 backends/lean/Base/Primitives/Array.lean create mode 100644 backends/lean/Base/Primitives/ArraySlice.lean create mode 100644 backends/lean/Base/Primitives/CoreOps.lean delete mode 100644 backends/lean/Base/Primitives/CoreOpsDeref.lean 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/Array.lean deleted file mode 100644 index 49c84bee..00000000 --- a/backends/lean/Base/Primitives/Array.lean +++ /dev/null @@ -1,403 +0,0 @@ -/- 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.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 [*] - -end Primitives 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 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 diff --git a/compiler/Extract.ml b/compiler/Extract.ml index afd722e5..6b6a2686 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -234,26 +234,20 @@ let assumed_adts () : (assumed_ty * string) list = (Array, "Array"); (Slice, "Slice"); (Str, "Str"); + (RawPtr Mut, "MutRawPtr"); + (RawPtr Const, "ConstRawPtr"); ] - | Coq | FStar -> + | Coq | FStar | HOL4 -> [ (State, "state"); (Result, "result"); (Error, "error"); - (Fuel, "nat"); - (Array, "array"); - (Slice, "slice"); - (Str, "str"); - ] - | HOL4 -> - [ - (State, "state"); - (Result, "result"); - (Error, "error"); - (Fuel, "num"); + (Fuel, if !backend = HOL4 then "num" else "nat"); (Array, "array"); (Slice, "slice"); (Str, "str"); + (RawPtr Mut, "mut_raw_ptr"); + (RawPtr Const, "const_raw_ptr"); ] let assumed_struct_constructors () : (assumed_ty * string) list = @@ -1378,7 +1372,7 @@ let extract_type_decl_register_names (ctx : extraction_ctx) (def : type_decl) : let def_name = match info with | None -> ctx.fmt.type_name def.name - | Some info -> String.concat "." info.rust_name + | Some info -> info.extract_name in let ctx = ctx_add (TypeId (AdtId def.def_id)) def_name ctx in (* Compute and register: @@ -4281,16 +4275,9 @@ let extract_trait_decl_method_names (ctx : extraction_ctx) string * (RegionGroupId.id option * string) list = let compute_fun_name (f : fun_decl) : RegionGroupId.id option * string = - (* We do something special: we use the base name but remove everything - but the crate (because [get_name] removes it) and the last ident. - This allows us to reuse the [ctx_compute_fun_decl] function. - *) - let basename : name = - match (f.basename : name) with - | Ident crate :: name -> - Ident crate :: [ Collections.List.last name ] - | _ -> raise (Failure "Unexpected") - in + (* We do something special to reuse the [ctx_compute_fun_decl] + function. TODO: make it cleaner. *) + let basename : name = [ Ident item_name ] in let f = { f with basename } in let trans = A.FunDeclId.Map.find f.def_id ctx.trans_funs in let name = ctx_compute_fun_name trans f ctx in @@ -4503,6 +4490,17 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter) extract_generic_params ctx fmt TypeDeclId.Set.empty generics type_params cg_params trait_clauses; + (* Add the parent clauses as local clauses, so that we can refer to them *) + let ctx = + List.fold_left + (fun ctx clause -> + let item_name = + ctx_get_trait_parent_clause decl.def_id clause.clause_id ctx + in + ctx_add (LocalTraitClauseId clause.clause_id) item_name ctx) + ctx decl.generics.trait_clauses + in + F.pp_print_space fmt (); (match !backend with | Lean -> F.pp_print_string fmt "where" @@ -4522,6 +4520,7 @@ let extract_trait_decl (ctx : extraction_ctx) (fmt : F.formatter) ctx_get_trait_parent_clause decl.def_id clause.clause_id ctx in let ty () = + F.pp_print_space fmt (); extract_trait_clause_type ctx fmt TypeDeclId.Set.empty clause in extract_trait_decl_item ctx fmt item_name ty) diff --git a/compiler/ExtractBuiltin.ml b/compiler/ExtractBuiltin.ml index 4c6fe014..c781463e 100644 --- a/compiler/ExtractBuiltin.ml +++ b/compiler/ExtractBuiltin.ml @@ -121,7 +121,7 @@ let builtin_types () : builtin_type_info list = rust_name = [ "alloc"; "alloc"; "Global" ]; extract_name = (match !backend with - | Lean -> "AllocGlobal" + | Lean -> "alloc.alloc.Global" | Coq | FStar | HOL4 -> "alloc_global"); keep_params = None; body_info = None; @@ -335,7 +335,7 @@ let builtin_funs () : rg = None; extract_name = (match !backend with - | FStar | Coq | HOL4 -> "alloc_boxed_box_deref" + | FStar | Coq | HOL4 -> "alloc_boxed_Box_deref" | Lean -> "alloc.boxed.Box.deref"); }; (* The backward function shouldn't be used *) @@ -343,7 +343,7 @@ let builtin_funs () : rg = rg0; extract_name = (match !backend with - | FStar | Coq | HOL4 -> "alloc_boxed_box_deref_back" + | FStar | Coq | HOL4 -> "alloc_boxed_Box_deref_back" | Lean -> "alloc.boxed.Box.deref_back"); }; ] ); @@ -354,7 +354,7 @@ let builtin_funs () : rg = None; extract_name = (match !backend with - | FStar | Coq | HOL4 -> "alloc_boxed_box_deref_mut" + | FStar | Coq | HOL4 -> "alloc_boxed_Box_deref_mut" | Lean -> "alloc.boxed.Box.deref_mut"); }; { @@ -365,6 +365,179 @@ let builtin_funs () : | Lean -> "alloc.boxed.Box.deref_mut_back"); }; ] ); + (* TODO: fix the same like "[T]" below *) + ( [ "core"; "slice"; "index"; "[T]"; "index" ], + None, + [ + { + rg = None; + extract_name = + (match !backend with + | FStar | Coq | HOL4 -> "core_slice_index_Slice_index" + | Lean -> "core.slice.index.Slice.index"); + }; + (* The backward function shouldn't be used *) + { + rg = rg0; + extract_name = + (match !backend with + | FStar | Coq | HOL4 -> "core_slice_index_Slice_index_back" + | Lean -> "core.slice.index.Slice.index_back"); + }; + ] ); + ( [ "core"; "slice"; "index"; "[T]"; "index_mut" ], + None, + [ + { + rg = None; + extract_name = + (match !backend with + | FStar | Coq | HOL4 -> "core_slice_index_Slice_index_mut" + | Lean -> "core.slice.index.Slice.index_mut"); + }; + (* The backward function shouldn't be used *) + { + rg = rg0; + extract_name = + (match !backend with + | FStar | Coq | HOL4 -> "core_slice_index_Slice_index_mut_back" + | Lean -> "core.slice.index.Slice.index_mut_back"); + }; + ] ); + ( [ "core"; "array"; "[T; N]"; "index" ], + None, + [ + { + rg = None; + extract_name = + (match !backend with + | FStar | Coq | HOL4 -> "core_array_Array_index" + | Lean -> "core.array.Array.index"); + }; + (* The backward function shouldn't be used *) + { + rg = rg0; + extract_name = + (match !backend with + | FStar | Coq | HOL4 -> "core_array_Array_index_back" + | Lean -> "core.array.Array.index_back"); + }; + ] ); + ( [ "core"; "array"; "[T; N]"; "index_mut" ], + None, + [ + { + rg = None; + extract_name = + (match !backend with + | FStar | Coq | HOL4 -> "core_array_Array_index_mut" + | Lean -> "core.array.Array.index_mut"); + }; + (* The backward function shouldn't be used *) + { + rg = rg0; + extract_name = + (match !backend with + | FStar | Coq | HOL4 -> "core_array_Array_index_mut_back" + | Lean -> "core.array.Array.index_mut_back"); + }; + ] ); + ( [ "core"; "slice"; "index"; "Range"; "get" ], + None, + [ + { + rg = None; + extract_name = + (match !backend with + | FStar | Coq | HOL4 -> "core_slice_index_Range_get" + | Lean -> "core.slice.index.Range.get"); + }; + (* The backward function shouldn't be used *) + { + rg = rg0; + extract_name = + (match !backend with + | FStar | Coq | HOL4 -> "core_slice_index_Range_get_back" + | Lean -> "core.slice.index.Range.get_back"); + }; + ] ); + ( [ "core"; "slice"; "index"; "Range"; "get_mut" ], + None, + [ + { + rg = None; + extract_name = + (match !backend with + | FStar | Coq | HOL4 -> "core_slice_index_Range_get_mut" + | Lean -> "core.slice.index.Range.get_mut"); + }; + { + rg = rg0; + extract_name = + (match !backend with + | FStar | Coq | HOL4 -> "core_slice_index_Range_get_mut_back" + | Lean -> "core.slice.index.Range.get_mut_back"); + }; + ] ); + ( [ "core"; "slice"; "index"; "Range"; "index" ], + None, + [ + { + rg = None; + extract_name = + (match !backend with + | FStar | Coq | HOL4 -> "core_slice_index_Range_index" + | Lean -> "core.slice.index.Range.index"); + }; + (* The backward function shouldn't be used *) + { + rg = rg0; + extract_name = + (match !backend with + | FStar | Coq | HOL4 -> "core_slice_index_Range_index_back" + | Lean -> "core.slice.index.Range.index_back"); + }; + ] ); + ( [ "core"; "slice"; "index"; "Range"; "index_mut" ], + None, + [ + { + rg = None; + extract_name = + (match !backend with + | FStar | Coq | HOL4 -> "core_slice_index_Range_index_mut" + | Lean -> "core.slice.index.Range.index_mut"); + }; + { + rg = rg0; + extract_name = + (match !backend with + | FStar | Coq | HOL4 -> "core_slice_index_Range_index_mut_back" + | Lean -> "core.slice.index.Range.index_mut_back"); + }; + ] ); + ( [ "core"; "slice"; "index"; "Range"; "get_unchecked" ], + None, + [ + { + rg = None; + extract_name = + (match !backend with + | FStar | Coq | HOL4 -> "core_slice_index_Range_get_unchecked" + | Lean -> "core.slice.index.Range.get_unchecked"); + }; + ] ); + ( [ "core"; "slice"; "index"; "Range"; "get_unchecked_mut" ], + None, + [ + { + rg = None; + extract_name = + (match !backend with + | FStar | Coq | HOL4 -> "core_slice_index_Range_get_unchecked_mut" + | Lean -> "core.slice.index.Range.get_unchecked_mut"); + }; + ] ); ] let mk_builtin_funs_map () = @@ -528,7 +701,7 @@ let builtin_trait_decls_info () = [ (match !backend with | Coq | FStar | HOL4 -> "index_inst" - | Lean -> "IndexInst"); + | Lean -> "indexInst"); ]; consts = []; types = []; @@ -547,6 +720,104 @@ let builtin_trait_decls_info () = ] ); ]; }; + { + (* Sealed *) + rust_name = "core::slice::index::private_slice_index::Sealed"; + extract_name = + (match !backend with + | Coq | FStar | HOL4 -> "core_slice_index_sealed" + | Lean -> "core.slice.index.private_slice_index.Sealed"); + parent_clauses = []; + consts = []; + types = []; + funs = []; + }; + { + (* SliceIndex *) + rust_name = "core::slice::index::SliceIndex"; + extract_name = + (match !backend with + | Coq | FStar | HOL4 -> "core_SliceIndex" + | Lean -> "core.slice.index.SliceIndex"); + parent_clauses = + [ + (match !backend with + | Coq | FStar | HOL4 -> "sealed_inst" + | Lean -> "sealedInst"); + ]; + consts = []; + types = + [ + ( "Output", + ( (match !backend with + | Coq | FStar | HOL4 -> "core_SliceIndex_Output" + | Lean -> "Output"), + [] ) ); + ]; + funs = + [ + ( "get", + [ + ( None, + match !backend with + | Coq | FStar | HOL4 -> "core_SliceIndex_get" + | Lean -> "get" ); + (* The backward function shouldn't be used *) + ( rg0, + match !backend with + | Coq | FStar | HOL4 -> "core_SliceIndex_get_back" + | Lean -> "get_back" ); + ] ); + ( "get_mut", + [ + ( None, + match !backend with + | Coq | FStar | HOL4 -> "core_SliceIndex_get_mut" + | Lean -> "get_mut" ); + ( rg0, + match !backend with + | Coq | FStar | HOL4 -> "core_SliceIndex_get_mut_back" + | Lean -> "get_mut_back" ); + ] ); + ( "get_unchecked", + [ + ( None, + match !backend with + | Coq | FStar | HOL4 -> "core_SliceIndex_get_unchecked" + | Lean -> "get_unchecked" ); + ] ); + ( "get_unchecked_mut", + [ + ( None, + match !backend with + | Coq | FStar | HOL4 -> "core_SliceIndex_get_unchecked_mut" + | Lean -> "get_unchecked_mut" ); + ] ); + ( "index", + [ + ( None, + match !backend with + | Coq | FStar | HOL4 -> "core_SliceIndex_index" + | Lean -> "index" ); + (* The backward function shouldn't be used *) + ( rg0, + match !backend with + | Coq | FStar | HOL4 -> "core_SliceIndex_index_back" + | Lean -> "index_back" ); + ] ); + ( "index_mut", + [ + ( None, + match !backend with + | Coq | FStar | HOL4 -> "core_SliceIndex_index_mut" + | Lean -> "index_mut" ); + ( rg0, + match !backend with + | Coq | FStar | HOL4 -> "core_SliceIndex_index_mut_back" + | Lean -> "index_mut_back" ); + ] ); + ]; + }; ] let mk_builtin_trait_decls_map () = @@ -577,6 +848,7 @@ end module SimpleNamePairMap = Collections.MakeMap (SimpleNamePairOrd) let builtin_trait_impls_info () : ((string list * string list) * string) list = + (* TODO: fix the names like "[T]" below *) [ (* core::ops::Deref> *) ( ([ "alloc"; "boxed"; "Box" ], [ "core"; "ops"; "deref"; "Deref" ]), @@ -584,6 +856,28 @@ let builtin_trait_impls_info () : ((string list * string list) * string) list = (* core::ops::DerefMut> *) ( ([ "alloc"; "boxed"; "Box" ], [ "core"; "ops"; "deref"; "DerefMut" ]), "alloc.boxed.Box.coreOpsDerefMutInst" ); + (* core::ops::index::Index<[T], I> *) + ( ([ "core"; "slice"; "index"; "[T]" ], [ "core"; "ops"; "index"; "Index" ]), + "core.slice.index.Slice.coreopsindexIndexInst" ); + (* core::slice::index::private_slice_index::Sealed> *) + ( ( [ "core"; "slice"; "index"; "private_slice_index"; "Range" ], + [ "core"; "slice"; "index"; "private_slice_index"; "Sealed" ] ), + "core.slice.index.private_slice_index.Range.coresliceindexprivate_slice_indexSealedInst" + ); + (* core::slice::index::SliceIndex, [T]> *) + ( ( [ "core"; "slice"; "index"; "Range" ], + [ "core"; "slice"; "index"; "SliceIndex" ] ), + "core.slice.index.Range.coresliceindexSliceIndexInst" ); + (* core::ops::index::IndexMut<[T], I> *) + ( ( [ "core"; "slice"; "index"; "[T]" ], + [ "core"; "ops"; "index"; "IndexMut" ] ), + "core.slice.index.Slice.coreopsindexIndexMutInst" ); + (* core::ops::index::Index<[T; N], I> *) + ( ([ "core"; "array"; "[T; N]" ], [ "core"; "ops"; "index"; "Index" ]), + "core.array.Array.coreopsindexIndexInst" ); + (* core::ops::index::IndexMut<[T; N], I> *) + ( ([ "core"; "array"; "[T; N]" ], [ "core"; "ops"; "index"; "IndexMut" ]), + "core.array.Array.coreopsindexIndexMutInst" ); ] let mk_builtin_trait_impls_map () = diff --git a/compiler/LlbcAstUtils.ml b/compiler/LlbcAstUtils.ml index 2553127a..0ab4ed94 100644 --- a/compiler/LlbcAstUtils.ml +++ b/compiler/LlbcAstUtils.ml @@ -13,14 +13,14 @@ let lookup_fun_name (fun_id : fun_id) (fun_decls : fun_decl FunDeclId.Map.t) : | Regular id -> (FunDeclId.Map.find id fun_decls).name | Assumed aid -> Assumed.get_assumed_fun_name aid -(** Return the opaque declarations found in the crate. +(** Return the opaque declarations found in the crate, which are also *not builtin*. [filter_assumed]: if [true], do not consider as opaque the external definitions that we will map to definitions from the standard library. Remark: the list of functions also contains the list of opaque global bodies. *) -let crate_get_opaque_decls (k : crate) (filter_assumed : bool) : +let crate_get_opaque_non_builtin_decls (k : crate) (filter_assumed : bool) : T.type_decl list * fun_decl list = let open ExtractBuiltin in let is_opaque_fun (d : fun_decl) : bool = @@ -30,14 +30,21 @@ let crate_get_opaque_decls (k : crate) (filter_assumed : bool) : (which don't have a body but must not be considered as opaque) *) && (match d.kind with TraitMethodDecl _ -> false | _ -> true) && ((not filter_assumed) - || not (SimpleNameMap.mem sname builtin_globals_map)) + || (not (SimpleNameMap.mem sname builtin_globals_map)) + && not (SimpleNameMap.mem sname (builtin_funs_map ()))) + in + let is_opaque_type (d : T.type_decl) : bool = + let sname = name_to_simple_name d.name in + d.kind = T.Opaque + && ((not filter_assumed) + || not (SimpleNameMap.mem sname (builtin_types_map ()))) in - let is_opaque_type (d : T.type_decl) : bool = d.kind = T.Opaque in (* Note that by checking the function bodies we also the globals *) ( List.filter is_opaque_type (T.TypeDeclId.Map.values k.types), List.filter is_opaque_fun (FunDeclId.Map.values k.functions) ) (** Return true if the crate contains opaque declarations, ignoring the assumed definitions. *) -let crate_has_opaque_decls (k : crate) (filter_assumed : bool) : bool = - crate_get_opaque_decls k filter_assumed <> ([], []) +let crate_has_opaque_non_builtin_decls (k : crate) (filter_assumed : bool) : + bool = + crate_get_opaque_non_builtin_decls k filter_assumed <> ([], []) diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 35dff9e6..019a5c35 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -390,10 +390,10 @@ type gen_config = { [filter_assumed]: if [true], do not consider as opaque the external definitions that we will map to definitions from the standard library. *) -let crate_has_opaque_decls (ctx : gen_ctx) (filter_assumed : bool) : bool * bool - = +let crate_has_opaque_non_builtin_decls (ctx : gen_ctx) (filter_assumed : bool) : + bool * bool = let types, funs = - LlbcAstUtils.crate_get_opaque_decls ctx.crate filter_assumed + LlbcAstUtils.crate_get_opaque_non_builtin_decls ctx.crate filter_assumed in log#ldebug (lazy @@ -1257,7 +1257,9 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : (* Check if there are opaque types and functions - in which case we need * to split *) - let has_opaque_types, has_opaque_funs = crate_has_opaque_decls ctx true in + let has_opaque_types, has_opaque_funs = + crate_has_opaque_non_builtin_decls ctx true + in let has_opaque_types = has_opaque_types || !Config.use_state in (* Extract the types *) -- cgit v1.2.3