Skip to content

Commit

Permalink
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
chore: merge main
Browse files Browse the repository at this point in the history
fgdorais committed Dec 20, 2024

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
2 parents 77eb2a2 + 9e583ef commit 5347980
Showing 48 changed files with 1,039 additions and 1,124 deletions.
2 changes: 2 additions & 0 deletions .github/workflows/docs-release.yml
Original file line number Diff line number Diff line change
@@ -40,6 +40,8 @@ jobs:
- name: Release Docs
uses: softprops/action-gh-release@v2
with:
prerelease: ${{ contains(github.ref, 'rc') }}
make_latest: ${{ !contains(github.ref, 'rc') }}
files: |
docs/docs-${{ github.ref_name }}.tar.gz
docs/docs-${{ github.ref_name }}.zip
3 changes: 3 additions & 0 deletions .github/workflows/labels-from-status.yml
Original file line number Diff line number Diff line change
@@ -34,6 +34,7 @@ jobs:
if: github.event.pull_request.state == 'closed'
uses: actions-ecosystem/action-remove-labels@v1
with:
github_token: ${{ secrets.GITHUB_TOKEN }}
labels: |
WIP
awaiting-author
@@ -48,6 +49,7 @@ jobs:
! contains(github.event.pull_request.labels.*.name, 'WIP')
uses: actions-ecosystem/action-add-labels@v1
with:
github_token: ${{ secrets.GITHUB_TOKEN }}
labels: WIP

- name: Label unlabeled other PR as awaiting-review
@@ -59,4 +61,5 @@ jobs:
! contains(github.event.pull_request.labels.*.name, 'WIP')
uses: actions-ecosystem/action-add-labels@v1
with:
github_token: ${{ secrets.GITHUB_TOKEN }}
labels: awaiting-review
1 change: 0 additions & 1 deletion Batteries.lean
Original file line number Diff line number Diff line change
@@ -56,7 +56,6 @@ import Batteries.Lean.Meta.SavedState
import Batteries.Lean.Meta.Simp
import Batteries.Lean.Meta.UnusedNames
import Batteries.Lean.MonadBacktrack
import Batteries.Lean.NameMap
import Batteries.Lean.NameMapAttribute
import Batteries.Lean.PersistentHashMap
import Batteries.Lean.PersistentHashSet
15 changes: 5 additions & 10 deletions Batteries/Classes/SatisfiesM.lean
Original file line number Diff line number Diff line change
@@ -185,14 +185,15 @@ theorem SatisfiesM_EStateM_eq :
rw [EStateM.run_map, EStateM.run]
split <;> simp_all

@[simp] theorem SatisfiesM_ReaderT_eq [Monad m] :
theorem SatisfiesM_ReaderT_eq [Monad m] :
SatisfiesM (m := ReaderT ρ m) p x ↔ ∀ s, SatisfiesM p (x.run s) :=
(exists_congr fun a => by exact ⟨fun eq _ => eq ▸ rfl, funext⟩).trans Classical.skolem.symm

theorem SatisfiesM_StateRefT_eq [Monad m] :
SatisfiesM (m := StateRefT' ω σ m) p x ↔ ∀ s, SatisfiesM p (x s) := by simp [ReaderT.run]
SatisfiesM (m := StateRefT' ω σ m) p x ↔ ∀ s, SatisfiesM p (x s) := by
simp [SatisfiesM_ReaderT_eq, ReaderT.run]

@[simp] theorem SatisfiesM_StateT_eq [Monad m] [LawfulMonad m] :
theorem SatisfiesM_StateT_eq [Monad m] [LawfulMonad m] :
SatisfiesM (m := StateT ρ m) (α := α) p x ↔ ∀ s, SatisfiesM (m := m) (p ·.1) (x.run s) := by
change SatisfiesM (m := StateT ρ m) (α := α) p x ↔ ∀ s, SatisfiesM (m := m) (p ·.1) (x s)
refine .trans ⟨fun ⟨f, eq⟩ => eq ▸ ?_, fun ⟨f, h⟩ => ?_⟩ Classical.skolem.symm
@@ -201,7 +202,7 @@ theorem SatisfiesM_StateRefT_eq [Monad m] :
· refine ⟨fun s => (fun ⟨⟨a, s'⟩, h⟩ => ⟨⟨a, h⟩, s'⟩) <$> f s, funext fun s => ?_⟩
show _ >>= _ = _; simp [← h]

@[simp] theorem SatisfiesM_ExceptT_eq [Monad m] [LawfulMonad m] :
theorem SatisfiesM_ExceptT_eq [Monad m] [LawfulMonad m] :
SatisfiesM (m := ExceptT ρ m) (α := α) p x ↔
SatisfiesM (m := m) (∀ a, · = .ok a → p a) x.run := by
change _ ↔ SatisfiesM (m := m) (∀ a, · = .ok a → p a) x
@@ -247,9 +248,6 @@ instance : MonadSatisfying (Except ε) where
| .error e => .error e
val_eq {α p x?} h := by cases x? <;> simp

-- This will be redundant after nightly-2024-11-08.
attribute [ext] ReaderT.ext

instance [Monad m] [LawfulMonad m][MonadSatisfying m] : MonadSatisfying (ReaderT ρ m) where
satisfying {α p x} h :=
have h' := SatisfiesM_ReaderT_eq.mp h
@@ -263,9 +261,6 @@ instance [Monad m] [LawfulMonad m][MonadSatisfying m] : MonadSatisfying (ReaderT
instance [Monad m] [LawfulMonad m] [MonadSatisfying m] : MonadSatisfying (StateRefT' ω σ m) :=
inferInstanceAs <| MonadSatisfying (ReaderT _ _)

-- This will be redundant after nightly-2024-11-08.
attribute [ext] StateT.ext

instance [Monad m] [LawfulMonad m] [MonadSatisfying m] : MonadSatisfying (StateT ρ m) where
satisfying {α p x} h :=
have h' := SatisfiesM_StateT_eq.mp h
46 changes: 7 additions & 39 deletions Batteries/Data/Array/Basic.lean
Original file line number Diff line number Diff line change
@@ -46,7 +46,7 @@ considered.
protected def minD [ord : Ord α]
(xs : Array α) (d : α) (start := 0) (stop := xs.size) : α :=
if h: start < xs.size ∧ start < stop then
xs.minWith (xs.get ⟨start, h.left⟩) (start + 1) stop
xs.minWith xs[start] (start + 1) stop
else
d

@@ -60,7 +60,7 @@ considered.
protected def min? [ord : Ord α]
(xs : Array α) (start := 0) (stop := xs.size) : Option α :=
if h : start < xs.size ∧ start < stop then
some $ xs.minD (xs.get ⟨start, h.left⟩) start stop
some $ xs.minD xs[start] start stop
else
none

@@ -135,45 +135,13 @@ A proof by `get_elem_tactic` is provided as a default argument for `h`.
This will perform the update destructively provided that `a` has a reference count of 1 when called.
-/
abbrev setN (a : Array α) (i : Nat) (x : α) (h : i < a.size := by get_elem_tactic) : Array α :=
a.set ⟨i, h⟩ x
a.set i x

/--
`swapN a i j hi hj` swaps two `Nat` indexed entries in an `Array α`.
Uses `get_elem_tactic` to supply a proof that the indices are in range.
`hi` and `hj` are both given a default argument `by get_elem_tactic`.
This will perform the update destructively provided that `a` has a reference count of 1 when called.
-/
abbrev swapN (a : Array α) (i j : Nat)
(hi : i < a.size := by get_elem_tactic) (hj : j < a.size := by get_elem_tactic) : Array α :=
Array.swap a ⟨i,hi⟩ ⟨j, hj⟩
@[deprecated (since := "2024-11-24")] alias swapN := swap

/--
`swapAtN a i h x` swaps the entry with index `i : Nat` in the vector for a new entry `x`.
The old entry is returned alongwith the modified vector.
Automatically generates proof of `i < a.size` with `get_elem_tactic` where feasible.
-/
abbrev swapAtN (a : Array α) (i : Nat) (x : α) (h : i < a.size := by get_elem_tactic) :
α × Array α := swapAt a ⟨i,h⟩ x
@[deprecated (since := "2024-11-24")] alias swapAtN := swapAt

/--
`eraseIdxN a i h` Removes the element at position `i` from a vector of length `n`.
`h : i < a.size` has a default argument `by get_elem_tactic` which tries to supply a proof
that the index is valid.
This function takes worst case O(n) time because it has to backshift all elements at positions
greater than i.
-/
abbrev eraseIdxN (a : Array α) (i : Nat) (h : i < a.size := by get_elem_tactic) : Array α :=
a.feraseIdx ⟨i, h⟩

/--
Remove the element at a given index from an array, panics if index is out of bounds.
-/
def eraseIdx! (a : Array α) (i : Nat) : Array α :=
if h : i < a.size then
a.feraseIdx ⟨i, h⟩
else
have : Inhabited (Array α) := ⟨a⟩
panic! s!"index {i} out of bounds"
@[deprecated (since := "2024-11-20")] alias eraseIdxN := eraseIdx

end Array

@@ -201,7 +169,7 @@ subarray, or `none` if the subarray is empty.
def popHead? (as : Subarray α) : Option (α × Subarray α) :=
if h : as.start < as.stop
then
let head := as.array.get ⟨as.start, Nat.lt_of_lt_of_le h as.stop_le_array_size
let head := as.array[as.start]'(Nat.lt_of_lt_of_le h as.stop_le_array_size)
let tail :=
{ as with
start := as.start + 1
Loading

0 comments on commit 5347980

Please sign in to comment.