From e3adfbe8d4be02a4bfbe301dbed9a4e32698dbdc Mon Sep 17 00:00:00 2001 From: Shrys Date: Sat, 17 Aug 2024 22:40:45 +0000 Subject: [PATCH 1/7] Basic file setup --- Batteries/Data/Vector.lean | 1 + Batteries/Data/Vector/Monadic.lean | 23 +++++++++++++++++++++++ 2 files changed, 24 insertions(+) create mode 100644 Batteries/Data/Vector/Monadic.lean diff --git a/Batteries/Data/Vector.lean b/Batteries/Data/Vector.lean index f543f121ef..f7cd4e2d07 100644 --- a/Batteries/Data/Vector.lean +++ b/Batteries/Data/Vector.lean @@ -1,2 +1,3 @@ import Batteries.Data.Vector.Basic import Batteries.Data.Vector.Lemmas +import Batteries.Data.Vector.Monadic diff --git a/Batteries/Data/Vector/Monadic.lean b/Batteries/Data/Vector/Monadic.lean new file mode 100644 index 0000000000..5f5f555c16 --- /dev/null +++ b/Batteries/Data/Vector/Monadic.lean @@ -0,0 +1,23 @@ +/- +Copyright (c) 2024 Shreyas Srinivas. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Shreyas Srinivas +-/ + +import Batteries.Data.Vector.Basic + + +/-! +## Monadic Definitions for Vectors +In this file we add monadic definitions for statically sized vectors. +-/ + +namespace Batteries + +namespace Vector + + + + +end Vector +end Batteries From a9101e6eac76dadf2111c742e5e5790d5e514c22 Mon Sep 17 00:00:00 2001 From: Shrys Date: Sat, 17 Aug 2024 23:31:04 +0000 Subject: [PATCH 2/7] Added and fixed definitions from Init.Data.Array.Basic --- Batteries/Data/Vector/Monadic.lean | 120 ++++++++++++++++++++++++++++- 1 file changed, 119 insertions(+), 1 deletion(-) diff --git a/Batteries/Data/Vector/Monadic.lean b/Batteries/Data/Vector/Monadic.lean index 5f5f555c16..071732d416 100644 --- a/Batteries/Data/Vector/Monadic.lean +++ b/Batteries/Data/Vector/Monadic.lean @@ -5,7 +5,7 @@ Authors: Shreyas Srinivas -/ import Batteries.Data.Vector.Basic - +import Init.Data.Array.Basic /-! ## Monadic Definitions for Vectors @@ -16,8 +16,126 @@ namespace Batteries namespace Vector +def modifyM [Monad m] (v : Vector α n) (i : Nat) + (f : α → m α) : m (Vector α n) := do + return ⟨←Array.modifyM v.toArray i f, by sorry⟩ + +@[inline] +def modify (v : Vector α n) (i : Nat) (f : α → α) : Vector α n := + Id.run <| modifyM v i f + +@[inline] +def modifyOp (self : Vector α n) (idx : Nat) (f : α → α) : Vector α n := + self.modify idx f + +protected def forIn {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] + (vs : Vector α n) (acc : β) (f : α → β → m (ForInStep β)) : m β := do + Array.forIn vs.toArray acc f + +instance : ForIn m (Vector α n) α where + forIn := Vector.forIn + +def foldlM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] + (f : β → α → m β) (init : β) + (v : Vector α n) (start := 0) (stop := n) : m β := do + Array.foldlM f init v.toArray start stop + +def foldrM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] + (f : α → β → m β) (init : β) (v : Vector α n) + (start := n) (stop := 0) : m β := + Array.foldrM f init v.toArray start stop + +def mapM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] + (f : α → m β) (v : Vector α n) : m (Vector β n) := do + return ⟨←Array.mapM f v.toArray, by sorry⟩ + +@[inline] +def mapIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] + (v : Vector α n) (f : Fin n → α → m β) : m (Vector β n) := do + return ⟨←Array.mapIdxM v.toArray (v.size_eq.symm ▸ f), by sorry⟩ + +@[inline] +def findSomeM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] + (v : Vector α n) (f : α → m (Option β)) : m (Option β) := + Array.findSomeM? v.toArray f + +@[inline] +def findM? {α : Type} {m : Type → Type} [Monad m] + (v : Vector α n) (p : α → m Bool) : m (Option α) := do + Array.findM? v.toArray p + +@[inline] +def findIdxM? [Monad m] (v : Vector α n) (p : α → m Bool) : m (Option Nat) := do + Array.findIdxM? v.toArray p + + +def anyM {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) + (v : Vector α n) (start := 0) (stop := n) : m Bool := + Array.anyM p v.toArray start stop + +@[inline] +def allM {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) + (v : Vector α n) (start := 0) (stop := n) : m Bool := + Array.allM p v.toArray start stop + +@[inline] +def findSomeRevM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] + (v : Vector α n) (f : α → m (Option β)) : m (Option β) := + Array.findSomeRevM? v.toArray f + +@[inline] +def findRevM? {α : Type} {m : Type → Type w} [Monad m] (v : Vector α n) + (p : α → m Bool) : m (Option α) := Array.findRevM? v.toArray p + +@[inline] +def forM {α : Type u} {m : Type v → Type w} [Monad m] (f : α → m PUnit) + (as : Array α) (start := 0) (stop := as.size) : m PUnit := + as.foldlM (fun _ => f) ⟨⟩ start stop + +@[inline] +def forRevM {α : Type u} {m : Type v → Type w} [Monad m] (f : α → m PUnit) (as : Array α) (start := as.size) (stop := 0) : m PUnit := + as.foldrM (fun a _ => f a) ⟨⟩ start stop + +@[inline] +def foldl {α : Type u} {β : Type v} (f : β → α → β) (init : β) + (v : Vector α n) (start := 0) (stop := n) : β := + Id.run <| v.foldlM f init start stop + +@[inline] +def foldr {α : Type u} {β : Type v} (f : α → β → β) (init : β) + (v : Vector α n) (start := n) (stop := 0) : β := + Id.run <| v.foldrM f init start stop + +@[inline] +def mapIdx {α : Type u} {β : Type v} (v : Vector α n) + (f : Fin n → α → β) : Vector β n := + Id.run <| v.mapIdxM f + +/-- Turns `#[a, b]` into `#[(a, 0), (b, 1)]`. -/ +def zipWithIndex (v : Vector α n) : Vector (α × Nat) n := + v.mapIdx fun i a => (a, i) + +@[inline] +def find? {α : Type} (v : Vector α n) (p : α → Bool) : Option α := + Id.run <| v.findM? p + +@[inline] +def findSome? {α : Type u} {β : Type v} (v : Vector α n) + (f : α → Option β) : Option β := + Id.run <| v.findSomeM? f + +@[inline] +def findSome! {α : Type u} {β : Type v} [Inhabited β] (v : Vector α n) + (f : α → Option β) : β := Array.findSome! v.toArray f +@[inline] +def findSomeRev? {α : Type u} {β : Type v} (v : Vector α n) (f : α → Option β) + : Option β := + Id.run <| v.findSomeRevM? f +@[inline] +def findRev? {α : Type} (v : Vector α n) (p : α → Bool) : Option α := + Id.run <| v.findRevM? p end Vector end Batteries From c658e2f01967bd1a5fbe9e6aba48e97ca4afbb1c Mon Sep 17 00:00:00 2001 From: Shrys Date: Sat, 17 Aug 2024 23:42:11 +0000 Subject: [PATCH 3/7] Fixes forRevM and adds a few docstrings --- Batteries/Data/Vector/Monadic.lean | 20 ++++++++++++++++---- 1 file changed, 16 insertions(+), 4 deletions(-) diff --git a/Batteries/Data/Vector/Monadic.lean b/Batteries/Data/Vector/Monadic.lean index 071732d416..fa62a7c386 100644 --- a/Batteries/Data/Vector/Monadic.lean +++ b/Batteries/Data/Vector/Monadic.lean @@ -16,17 +16,28 @@ namespace Batteries namespace Vector +/-- +`modifyM v i f` applies a monadic transformation `f` to `v[i]` +-/ def modifyM [Monad m] (v : Vector α n) (i : Nat) (f : α → m α) : m (Vector α n) := do return ⟨←Array.modifyM v.toArray i f, by sorry⟩ +/-- +`modify v i f` takes a vector `v`, index `i`, and a modification function `f` +and sets `v[i]` to `f`. +-/ @[inline] def modify (v : Vector α n) (i : Nat) (f : α → α) : Vector α n := Id.run <| modifyM v i f +/-- +`modifyOp self idx f` is identical to `modify v i f` It modifies `v[i]` by +applying `f`. +-/ @[inline] -def modifyOp (self : Vector α n) (idx : Nat) (f : α → α) : Vector α n := - self.modify idx f +def modifyOp (v : Vector α n) (idx : Nat) (f : α → α) : Vector α n := + v.modify idx f protected def forIn {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (vs : Vector α n) (acc : β) (f : α → β → m (ForInStep β)) : m β := do @@ -93,8 +104,9 @@ def forM {α : Type u} {m : Type v → Type w} [Monad m] (f : α → m PUnit) as.foldlM (fun _ => f) ⟨⟩ start stop @[inline] -def forRevM {α : Type u} {m : Type v → Type w} [Monad m] (f : α → m PUnit) (as : Array α) (start := as.size) (stop := 0) : m PUnit := - as.foldrM (fun a _ => f a) ⟨⟩ start stop +def forRevM {α : Type u} {m : Type v → Type w} [Monad m] (f : α → m PUnit) + (v : Vector α n) (start := n) (stop := 0) : m PUnit := + v.toArray.foldrM (fun a _ => f a) ⟨⟩ start stop @[inline] def foldl {α : Type u} {β : Type v} (f : β → α → β) (init : β) From e5058ca228b224ec79a0478bafd0730834885c54 Mon Sep 17 00:00:00 2001 From: Shrys Date: Sat, 17 Aug 2024 23:55:46 +0000 Subject: [PATCH 4/7] More docstrings added --- Batteries/Data/Vector/Monadic.lean | 26 ++++++++++++++++++++++++-- 1 file changed, 24 insertions(+), 2 deletions(-) diff --git a/Batteries/Data/Vector/Monadic.lean b/Batteries/Data/Vector/Monadic.lean index fa62a7c386..a1688d99c6 100644 --- a/Batteries/Data/Vector/Monadic.lean +++ b/Batteries/Data/Vector/Monadic.lean @@ -39,27 +39,49 @@ applying `f`. def modifyOp (v : Vector α n) (idx : Nat) (f : α → α) : Vector α n := v.modify idx f +/-- +`forIn v acc f` iterates over `v` applying `f` on each element and the +accumulated result. The final value of `acc` after the completion of the loop +is returned. +-/ protected def forIn {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] - (vs : Vector α n) (acc : β) (f : α → β → m (ForInStep β)) : m β := do - Array.forIn vs.toArray acc f + (v : Vector α n) (acc : β) (f : α → β → m (ForInStep β)) : m β := do + Array.forIn v.toArray acc f instance : ForIn m (Vector α n) α where forIn := Vector.forIn +/-- +`foldlM f init v start stop` is the monadic left fold function that folds `f` +over `v` from left to right. +-/ def foldlM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : β → α → m β) (init : β) (v : Vector α n) (start := 0) (stop := n) : m β := do Array.foldlM f init v.toArray start stop +/-- +`foldrM f init v start stop` is the monadic right fold function that folds `f` +over `v` from right to left. +-/ def foldrM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → β → m β) (init : β) (v : Vector α n) (start := n) (stop := 0) : m β := Array.foldrM f init v.toArray start stop +/-- +`mapM f v` maps a monadic function `f : α → m β` over `v` and returns +the resultant vector in the same monad `m`. +-/ def mapM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m β) (v : Vector α n) : m (Vector β n) := do return ⟨←Array.mapM f v.toArray, by sorry⟩ +/-- +`mapIdx f v` maps a monadic function `f : Fin n → α → m β` that takes vector +elements and their index, and maps them over `v`. It returns the resultant +vector in the same monad `m`. +-/ @[inline] def mapIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (v : Vector α n) (f : Fin n → α → m β) : m (Vector β n) := do From 4cc3bc01a3ee988af3ea594643d4ed7fd8ba68a3 Mon Sep 17 00:00:00 2001 From: Shrys Date: Sun, 18 Aug 2024 00:06:38 +0000 Subject: [PATCH 5/7] removed modifyOp --- Batteries/Data/Vector/Monadic.lean | 13 ++++--------- 1 file changed, 4 insertions(+), 9 deletions(-) diff --git a/Batteries/Data/Vector/Monadic.lean b/Batteries/Data/Vector/Monadic.lean index a1688d99c6..965180b0d9 100644 --- a/Batteries/Data/Vector/Monadic.lean +++ b/Batteries/Data/Vector/Monadic.lean @@ -6,6 +6,8 @@ Authors: Shreyas Srinivas import Batteries.Data.Vector.Basic import Init.Data.Array.Basic +import Init.Data.Array.Lemmas +import Batteries.Classes.SatisfiesM /-! ## Monadic Definitions for Vectors @@ -21,7 +23,8 @@ namespace Vector -/ def modifyM [Monad m] (v : Vector α n) (i : Nat) (f : α → m α) : m (Vector α n) := do - return ⟨←Array.modifyM v.toArray i f, by sorry⟩ + return ⟨←Array.modifyM v.toArray i f, + by rw[←v.size_eq]; sorry⟩ /-- `modify v i f` takes a vector `v`, index `i`, and a modification function `f` @@ -31,14 +34,6 @@ and sets `v[i]` to `f`. def modify (v : Vector α n) (i : Nat) (f : α → α) : Vector α n := Id.run <| modifyM v i f -/-- -`modifyOp self idx f` is identical to `modify v i f` It modifies `v[i]` by -applying `f`. --/ -@[inline] -def modifyOp (v : Vector α n) (idx : Nat) (f : α → α) : Vector α n := - v.modify idx f - /-- `forIn v acc f` iterates over `v` applying `f` on each element and the accumulated result. The final value of `acc` after the completion of the loop From 2a016daa978bcade07d7c442df6b2f9410aa258b Mon Sep 17 00:00:00 2001 From: Shrys Date: Sun, 18 Aug 2024 00:11:52 +0000 Subject: [PATCH 6/7] Some isolation of troubles --- Batteries/Data/Vector/Monadic.lean | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/Batteries/Data/Vector/Monadic.lean b/Batteries/Data/Vector/Monadic.lean index 965180b0d9..307a103c6d 100644 --- a/Batteries/Data/Vector/Monadic.lean +++ b/Batteries/Data/Vector/Monadic.lean @@ -70,7 +70,7 @@ the resultant vector in the same monad `m`. -/ def mapM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α → m β) (v : Vector α n) : m (Vector β n) := do - return ⟨←Array.mapM f v.toArray, by sorry⟩ + return ⟨←Array.mapM f v.toArray, by rw[←v.size_eq]; sorry⟩ /-- `mapIdx f v` maps a monadic function `f : Fin n → α → m β` that takes vector @@ -80,7 +80,8 @@ vector in the same monad `m`. @[inline] def mapIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (v : Vector α n) (f : Fin n → α → m β) : m (Vector β n) := do - return ⟨←Array.mapIdxM v.toArray (v.size_eq.symm ▸ f), by sorry⟩ + return ⟨←Array.mapIdxM v.toArray (v.size_eq.symm ▸ f), + by rw[←v.size_eq]; sorry⟩ @[inline] def findSomeM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] From 4cfe57bf7700c9ad7ff0fd8d8e693751f9077a3d Mon Sep 17 00:00:00 2001 From: Shrys Date: Sun, 18 Aug 2024 00:33:03 +0000 Subject: [PATCH 7/7] Added sensible definitions from Batteries --- Batteries/Data/Vector/Monadic.lean | 103 +++++++++++++++++++++++++++++ 1 file changed, 103 insertions(+) diff --git a/Batteries/Data/Vector/Monadic.lean b/Batteries/Data/Vector/Monadic.lean index 307a103c6d..8c6ba85507 100644 --- a/Batteries/Data/Vector/Monadic.lean +++ b/Batteries/Data/Vector/Monadic.lean @@ -167,5 +167,108 @@ def findSomeRev? {α : Type u} {β : Type v} (v : Vector α n) (f : α → Optio def findRev? {α : Type} (v : Vector α n) (p : α → Bool) : Option α := Id.run <| v.findRevM? p +/-- +Check whether vectors `xs` and `ys` are equal as sets, i.e. they +contain the same elements when disregarding order and duplicates. +-/ +def equalSet [BEq α] (xs ys : Vector α n) : Bool := + xs.toArray.all (ys.toArray.contains ·) + && ys.toArray.all (xs.toArray.contains ·) + +set_option linter.unusedVariables.funArgs false in +/-- +Returns the first minimal element among `d` and elements of the vector. +If `start` and `stop` are given, only the subarray `xs[start:stop]` is +considered (in addition to `d`). +-/ +@[inline] +protected def minWith [ord : Ord α] + (xs : Vector α n) (d : α) (start := 0) (stop := n) : α := + xs.foldl (init := d) (start := start) (stop := stop) fun min x => + if compare x min |>.isLT then x else min + +set_option linter.unusedVariables.funArgs false in +/-- +Find the first minimal element of a vector. If the array is empty, `d` is +returned. If `start` and `stop` are given, only the subarray `xs[start:stop]` is +considered. +-/ +@[inline] +protected def minD [ord : Ord α] + (xs : Vector α n) (d : α) (start := 0) (stop := xs.size) : α := + if h: start < xs.size ∧ start < stop then + xs.minWith (xs.get ⟨start, h.left⟩) (start + 1) stop + else + d + +set_option linter.unusedVariables.funArgs false in +/-- +Find the first minimal element of a vector. If the vector is empty, `none` is +returned. If `start` and `stop` are given, only the subarray `xs[start:stop]` is +considered. +-/ +@[inline] +protected def min? [ord : Ord α] + (xs : Vector α n) (start := 0) (stop := xs.size) : Option α := + if h : start < xs.size ∧ start < stop then + some $ xs.minD (xs.get ⟨start, h.left⟩) start stop + else + none + +set_option linter.unusedVariables.funArgs false in +/-- +Find the first minimal element of a vector. If the vector is empty, `default` is +returned. If `start` and `stop` are given, only the subvector `xs[start:stop]` +is considered. +-/ +@[inline] +protected def minI [ord : Ord α] [Inhabited α] + (xs : Vector α n) (start := 0) (stop := xs.size) : α := + xs.minD default start stop + +set_option linter.unusedVariables.funArgs false in +/-- +Returns the first maximal element among `d` and elements of the vector. +If `start` and `stop` are given, only the subvector `xs[start:stop]` is +considered (in addition to `d`). +-/ +@[inline] +protected def maxWith [ord : Ord α] + (xs : Vector α n) (d : α) (start := 0) (stop := xs.size) : α := + xs.minWith (ord := ord.opposite) d start stop + +set_option linter.unusedVariables.funArgs false in +/-- +Find the first maximal element of a vector. If the vector is empty, `d` is +returned. If `start` and `stop` are given, only the subvector `xs[start:stop]` +is considered. +-/ +@[inline] +protected def maxD [ord : Ord α] + (xs : Vector α n) (d : α) (start := 0) (stop := xs.size) : α := + xs.minD (ord := ord.opposite) d start stop + +set_option linter.unusedVariables.funArgs false in +/-- +Find the first maximal element of a vector. If the vector is empty, `none` is +returned. If `start` and `stop` are given, only the subvector `xs[start:stop]` +is considered. +-/ +@[inline] +protected def max? [ord : Ord α] + (xs : Vector α n) (start := 0) (stop := xs.size) : Option α := + xs.min? (ord := ord.opposite) start stop + +set_option linter.unusedVariables.funArgs false in +/-- +Find the first maximal element of a vector. If the vector is empty, `default` is +returned. If `start` and `stop` are given, only the subvector `xs[start:stop]` +is considered. +-/ +@[inline] +protected def maxI [ord : Ord α] [Inhabited α] + (xs : Array α) (start := 0) (stop := xs.size) : α := + xs.minI (ord := ord.opposite) start stop + end Vector end Batteries