From c882c7751c399f3eddd2342f18556e0c1cfea63e Mon Sep 17 00:00:00 2001 From: Jad Ghalayini Date: Fri, 31 Jan 2025 19:30:59 +0000 Subject: [PATCH 1/3] Updated to use latest Lean 4, batteries --- YatimaStdLib/AddChain.lean | 52 ++++++------ YatimaStdLib/Arithmetic.lean | 10 +-- YatimaStdLib/Array.lean | 10 +-- YatimaStdLib/Benchmark.lean | 83 +++++++++---------- YatimaStdLib/Bit.lean | 2 +- YatimaStdLib/ByteArray.lean | 19 ++--- YatimaStdLib/ByteVector.lean | 22 ++--- YatimaStdLib/Cached.lean | 2 +- YatimaStdLib/Cronos.lean | 4 +- YatimaStdLib/Either.lean | 4 +- YatimaStdLib/HashMap.lean | 10 +-- YatimaStdLib/HashSet.lean | 9 +- YatimaStdLib/Int.lean | 7 +- YatimaStdLib/Lean.lean | 6 -- YatimaStdLib/List.lean | 2 +- .../MLE/MultilinearLagrangePolynomial.lean | 8 +- YatimaStdLib/Matrix.lean | 6 +- YatimaStdLib/MultilinearPolynomial.lean | 8 +- YatimaStdLib/Nat.lean | 30 +------ YatimaStdLib/Polynomial.lean | 28 +++---- YatimaStdLib/RBMap.lean | 8 +- YatimaStdLib/RBNode.lean | 14 ++-- YatimaStdLib/Rat.lean | 10 +-- YatimaStdLib/SparseMatrix.lean | 32 +++---- .../StringInterner/Backend/Buffer.lean | 2 +- YatimaStdLib/StringInterner/Interner.lean | 4 +- YatimaStdLib/Tree.lean | 18 ++-- YatimaStdLib/UInt.lean | 13 ++- lake-manifest.json | 22 ++--- lakefile.lean | 20 +---- lean-toolchain | 2 +- 31 files changed, 207 insertions(+), 260 deletions(-) diff --git a/YatimaStdLib/AddChain.lean b/YatimaStdLib/AddChain.lean index b9f154a..9ab31dd 100644 --- a/YatimaStdLib/AddChain.lean +++ b/YatimaStdLib/AddChain.lean @@ -4,13 +4,13 @@ import YatimaStdLib.Nat /-! # AddChain -This module implements an efficient representation of numbers in terms of the double-and-add +This module implements an efficient representation of numbers in terms of the double-and-add algorithm. The finding an `AddChain` with `minChain` can be used to pre-calculate the function which implements a double-and-add or square-and-multiply represention of a natural number. -The types are left polymorphic to allow for more efficient implementations of `double` in the +The types are left polymorphic to allow for more efficient implementations of `double` in the case of `Chainable`, or `square` for `Square`. ## References @@ -22,13 +22,13 @@ case of `Chainable`, or `square` for `Square`. /-- The typeclass which implements efficient `add`, `mul`, `double`, and `doubleAdd` methods -/ class Chainable (α : Type _) extends BEq α, OfNat α (nat_lit 1) where - add : α → α → α - mul : α → α → α + add : α → α → α + mul : α → α → α double : α → α := fun x => add x x - doubleAdd : α → α → α := fun x y => add (double x) y + doubleAdd : α → α → α := fun x y => add (double x) y /- -In this section we include the basic instances for `Chainable` that exist in the core +In this section we include the basic instances for `Chainable` that exist in the core numerical libraries of Lean -/ section instances @@ -53,7 +53,7 @@ inductive ChainStep | add (idx₁ idx₂ : Nat) | double (idx : Nat) deriving Repr /-- -The chain of operations that can be used to represent a `Chainable` n in terms of the +The chain of operations that can be used to represent a `Chainable` n in terms of the double-and-add algorithm -/ def AddChain (α : Type _) [Chainable α] := Array α @@ -62,23 +62,23 @@ instance [Chainable α] : Inhabited (AddChain α) where default := #[1] instance [Chainable α] : HAdd (AddChain α) α (AddChain α) where - hAdd ch n := ch.push (n + ch.back) + hAdd ch n := ch.push (n + ch.back!) instance [Chainable α] : Mul (AddChain α) where - mul ch₁ ch₂ := - let last := ch₁.back - let ch₂' := ch₂.last.map (fun x => x * last) + mul ch₁ ch₂ := + let last := ch₁.back! + let ch₂' := ch₂.last.map (fun x => x * last) ch₁.append ch₂' -/- -In this section we implement an efficient algorithm to calculate the minimal AddChain for a natural +/- +In this section we implement an efficient algorithm to calculate the minimal AddChain for a natural number -/ namespace Nat -mutual +mutual -private partial def addChain (n k : Nat) : AddChain Nat := +private partial def addChain (n k : Nat) : AddChain Nat := let (q, r) := n.quotRem k if r == 0 || r == 1 then minChain k * minChain q + r else @@ -88,7 +88,7 @@ private partial def addChain (n k : Nat) : AddChain Nat := partial def minChain (n : Nat) : AddChain Nat := let logN := n.log2 if n == (1 <<< logN) then - Array.iota logN |>.map fun k => 2^k + Array.iota logN |>.map fun k => 2^k else if n == 3 then #[1, 2, 3] else let k := n / (1 <<< (logN/2)) @@ -124,8 +124,8 @@ def buildSteps [Chainable α] (ch : AddChain α) : Array ChainStep := Id.run do end AddChain -/-- -The function which returns the `AddChain` and the `Array ChainStep` to represent the natural number +/-- +The function which returns the `AddChain` and the `Array ChainStep` to represent the natural number `n` in terms of the double-and-add representation -/ def Nat.buildAddChain (n : Nat) : AddChain Nat × Array ChainStep := @@ -137,7 +137,7 @@ class Square (α : Type _) extends OfNat α (nat_lit 1) where mul : α → α → α square : α → α -namespace Square +namespace Square instance [Square α] : Inhabited α where default := 1 @@ -155,12 +155,12 @@ instance [Square α] : Mul α where for step in steps.toList do match step with - | .add left right => + | .add left right => answer := answer.push (answer[left]! * answer[right]!) - | .double idx => + | .double idx => answer := answer.push (square answer[idx]!) - - answer.back + + answer.back! end Square @@ -168,7 +168,7 @@ namespace Exp open Square in /-- Returns the function `n ↦ n ^ exp` by pre-calculating the `AddChain` for `exp`. -/ -@[specialize] def fastExpFunc [Square α] (exp : Nat) : α → α := +@[specialize] def fastExpFunc [Square α] (exp : Nat) : α → α := let (_ , steps) := exp.buildAddChain chainExp steps @@ -176,6 +176,6 @@ open Square in @[specialize] def fastExp [Square α] (n : α) (exp : Nat) : α := fastExpFunc exp n instance (priority := low) [Square α] : HPow α Nat α where - hPow n pow := fastExp n pow + hPow n pow := fastExp n pow -end Exp \ No newline at end of file +end Exp diff --git a/YatimaStdLib/Arithmetic.lean b/YatimaStdLib/Arithmetic.lean index 0505b7c..3fa8369 100644 --- a/YatimaStdLib/Arithmetic.lean +++ b/YatimaStdLib/Arithmetic.lean @@ -5,7 +5,7 @@ open Nat (powMod) /-- An implementation of the probabilistic Miller-Rabin primality test. Returns `false` if it can be -verified that `n` is not prime, and returns `true` if `n` is probably prime after `k` loops, which +verified that `n` is not prime, and returns `true` if `n` is probably prime after `k` loops, which may return a false positive with probability `1 / 4^k` assuming the ψRNG `gen` doesn't conspire against us in some unexpected way -/ @@ -14,7 +14,7 @@ def millerRabinTest (n k : Nat) : Bool := -- let exp : Nat → Nat := Exp.fastExpFunc d -- TODO: Use AddChains once we have an efficient Zmod Id.run do let mut a := 0 - let mut gen := mkStdGen (n + k) -- Using Lean's built in ψRNG + let mut gen := mkStdGen (n + k) -- Using Lean's built in ψRNG for _ in [:k] do (a, gen) := randNat gen 2 (n - 2) let mut x := powMod n a d @@ -29,9 +29,9 @@ def millerRabinTest (n k : Nat) : Bool := return true open Std in -/-- +/-- Calculates the discrete logarithm of using the Babystep-Giantstep algorithm, should have `O(√n)` -runtime +runtime -/ def dLog (base result mod : Nat) : Option Nat := do let mut basePowers : HashMap Nat Nat := .empty @@ -47,7 +47,7 @@ def dLog (base result mod : Nat) : Option Nat := do let mut target := result for quot in [:lim] do - match basePowers.find? target with + match basePowers.get? target with | some rem => return quot * lim + rem | none => target := target * basePowInv % mod diff --git a/YatimaStdLib/Array.lean b/YatimaStdLib/Array.lean index 1178535..a7c65a2 100644 --- a/YatimaStdLib/Array.lean +++ b/YatimaStdLib/Array.lean @@ -1,4 +1,4 @@ -import Std.Data.Array.Basic +import Batteries.Data.Array.Basic import YatimaStdLib.List namespace Array @@ -10,7 +10,7 @@ def iota (n : Nat) : Array Nat := instance : Monad Array where map := Array.map pure x := #[x] - bind l f := Array.join $ Array.map f l + bind l f := Array.flatten $ Array.map f l def shuffle (ar : Array α) (seed : Option Nat := none) [Inhabited α] : IO $ Array α := do @@ -29,17 +29,17 @@ def pad (ar : Array α) (a : α) (n : Nat) : Array α := ar ++ (.mkArray diff a) instance [Ord α] : Ord (Array α) where - compare x y := compare x.data y.data + compare x y := compare x.toList y.toList def last (ar : Array α) : Array α := ar.toSubarray.popFront.toArray -theorem append_size (arr₁ arr₂ : Array α) (h1 : arr₁.size = n) (h2 : arr₂.size = m) +theorem append_size (arr₁ arr₂ : Array α) (h1 : arr₁.size = n) (h2 : arr₂.size = m) : (arr₁ ++ arr₂).size = n + m := by unfold Array.size at * simp [h1, h2] def stdSizes (maxSize : Nat) := Array.iota maxSize |>.map (2 ^ ·) -def average (arr : Array Nat) : Nat := +def average (arr : Array Nat) : Nat := let sum := arr.foldl (init := 0) fun acc a => acc + a sum / arr.size diff --git a/YatimaStdLib/Benchmark.lean b/YatimaStdLib/Benchmark.lean index 95f9dd1..e1b9c32 100644 --- a/YatimaStdLib/Benchmark.lean +++ b/YatimaStdLib/Benchmark.lean @@ -8,10 +8,10 @@ import YatimaStdLib.RBMap Some basic utilities for benchmarking. See the `Benchmarks` folder for examples of use. There are current 4 benchmarking modes implemented: -- `FunctionAsymptotics`: Takes in a single function `f : α → β` where `α` implemented `FixedSize` +- `FunctionAsymptotics`: Takes in a single function `f : α → β` where `α` implemented `FixedSize` and a list of input sizes, and runs a benchmark on an array of randomly generated inputs. - `FixedInput`: Takes in a function `f : α → β` and a array of inputs `inputs : Array α`, and - benchmarks the time to run `f` on the list of inputs + benchmarks the time to run `f` on the list of inputs - `Comparison`: Takes in two functions `f g : α → β` and an array of inputs `inputs : Array α` and benchmarks the relative times for `f` and `g` on the fixed array of inputs - `RandomComparison`: Similar to the above, but works on a type `a` which implements `FixedSize` and @@ -29,7 +29,7 @@ section fixed_size open SlimCheck /-- -The class that represents a type `α` that has a measurable size, represented in terms of the +The class that represents a type `α` that has a measurable size, represented in terms of the generator that creates instances of type `α` of given size, and its measure. -/ class FixedSize (α : Type u) where @@ -46,16 +46,16 @@ end fixed_size namespace Benchmark -/-- +/-- Logging mode for the benchmark logger. `stdOut` prints to `stdOut` and `fsOut` prints to the -filesystem to a file named `name?` (or `benchmark` if no name is provided) +filesystem to a file named `name?` (or `benchmark` if no name is provided) -/ inductive LoggingMode | stdOut | fsOut (name? : Option String) -/-- -The mode in which the benchmark is being run based off the arguments given to the binary +/-- +The mode in which the benchmark is being run based off the arguments given to the binary `loggingMode` is as aboe and `rounds` determines the number of repetitions are averaged to generate the timing results -/ @@ -63,9 +63,9 @@ structure TestMode where rounds : Nat loggingMode : LoggingMode -open Std in +open Batteries in /-- -The type that contains all the resulting data from a benchmark run. +The type that contains all the resulting data from a benchmark run. Note: `keys`, `values`, and `keyOrd` can in many cases be left out when defining an instance of `Result` by having Lean solve them via unification from information coming from `data`. @@ -75,12 +75,12 @@ class Result where values : Type _ keyOrd : Ord keys data : IO $ RBMap keys values compare - printKeys : keys → String - printVal : values → String + printKeys : keys → String + printVal : values → String open Result in -def Result.print (result : Result) : IO $ Array String := - return (← result.data).foldl (init := #[]) +def Result.print (result : Result) : IO $ Array String := + return (← result.data).foldl (init := #[]) (fun acc key res => acc.push s!"{printKeys key}: {printVal res}") open Std in @@ -91,35 +91,36 @@ structure Runner where run (rounds : Nat) : Result open Std in -def unorderedRunnerAux {χ : Type _} [Ord χ] (inputs : Array α) (f : α → β) (numIter : Nat) - (order : α → χ) : IO $ RBMap χ Nat compare := do - let mut cron : Std.RBMap χ Nat compare := .empty +def unorderedRunnerAux {χ : Type _} [Ord χ] (inputs : Array α) (f : α → β) (numIter : Nat) + (order : α → χ) : IO $ Batteries.RBMap χ Nat compare := do + let mut cron : Batteries.RBMap χ Nat compare := .empty let mut answers := Array.mkEmpty inputs.size for input in inputs do let mut times : Array Nat := .mkEmpty numIter for _ in [:numIter] do let before ← IO.monoNanosNow - answers := answers.push $ f input + answers := answers.push $ f input let after ← IO.monoNanosNow let diff := after - before times := times.push diff - cron := cron.insert (order input) times.average + cron := cron.insert (order input) times.average return cron open Std in -def orderedRunnerAux [Ord α] (inputs : Array α) (f : α → β) (numIter : Nat) : IO $ RBMap α Nat +def orderedRunnerAux [Ord α] (inputs : Array α) (f : α → β) (numIter : Nat) + : IO $ Batteries.RBMap α Nat compare := unorderedRunnerAux inputs f numIter id structure FunctionAsymptotics {α : Type _} (f : α → β) where - inputSizes : Array Nat + inputSizes : Array Nat open SlimCheck in -def FunctionAsymptotics.generateInputs [cmd : FixedSize α] {f : α → β} +def FunctionAsymptotics.generateInputs [cmd : FixedSize α] {f : α → β} (K : FunctionAsymptotics f) : IO $ Array α := do let mut answer : Array α := #[] for size in K.inputSizes do answer := answer.push (← IO.runRand $ cmd.random size) - return answer + return answer def FunctionAsymptotics.benchmark {f : α → β} [FixedSize α] (K : FunctionAsymptotics f) : Runner where run rounds := { @@ -133,25 +134,25 @@ def FunctionAsymptotics.benchmark {f : α → β} [FixedSize α] (K : FunctionAs structure FixedInput {α : Type _} (f : α → β) where inputs : Array α -def FixedInput.benchmark {f : α → β} [Ord α] [ToString α] (K : FixedInput f) +def FixedInput.benchmark {f : α → β} [Ord α] [ToString α] (K : FixedInput f) : Runner where run rounds := { - data := return ← orderedRunnerAux K.inputs f rounds + data := return ← orderedRunnerAux K.inputs f rounds printKeys := ToString.toString printVal := ToString.toString } structure Comparison {α : Type _} (f g : α → β) where - inputs : Array α + inputs : Array α -def Comparison.benchmark {f g : α → β} [Ord α] [ToString α] (K : Comparison f g) +def Comparison.benchmark {f g : α → β} [Ord α] [ToString α] (K : Comparison f g) : Runner where run rounds := { data := do let fData ← orderedRunnerAux K.inputs f rounds let gData ← orderedRunnerAux K.inputs g rounds let answer := fData.zipD gData 0 - return answer + return answer printKeys := ToString.toString printVal := fun (n₁, n₂) => s!"f:{n₁} vs g:{n₂}" } @@ -160,33 +161,33 @@ structure RandomComparison {α : Type _} (f g : α → β) where inputSizes : Array Nat open SlimCheck in -def RandomComparison.generateInputs [cmd : FixedSize α] {f g : α → β} +def RandomComparison.generateInputs [cmd : FixedSize α] {f g : α → β} (K : RandomComparison f g) : IO $ Array α := do let mut answer : Array α := #[] for size in K.inputSizes do answer := answer.push (← IO.runRand $ cmd.random size) - return answer + return answer -def RandomComparison.benchmark {f g : α → β} [Ord α] [FixedSize α] (K : RandomComparison f g) +def RandomComparison.benchmark {f g : α → β} [Ord α] [FixedSize α] (K : RandomComparison f g) : Runner where run rounds := { data := do - let inputs ← K.generateInputs + let inputs ← K.generateInputs let fData ← orderedRunnerAux inputs f rounds let gData ← orderedRunnerAux inputs g rounds let answer := fData.zipD gData 0 - return answer + return answer printKeys := fun key => s!"{FixedSize.size key}" printVal := fun (n₁, n₂) => s!"f:{n₁} vs g:{n₂}" } /-- Parse arguments coming from `main` -/ -private def parseArgs (args : List String) : Except String TestMode := +private def parseArgs (args : List String) : Except String TestMode := let numIdx? := args.findIdx? (fun str => str == "-n" || str == "--num") let logIdx? := args.findIdx? (fun str => str == "-l" || str == "--log") - match numIdx?, logIdx? with + match numIdx?, logIdx? with | none, none => .ok {rounds := 1, loggingMode := .stdOut} - | some numIdx, none => + | some numIdx, none => if let some numIterStr := args.get? (numIdx + 1) then if let some numIter := numIterStr.toNat? then .ok {rounds := numIter, loggingMode := .stdOut} @@ -217,7 +218,7 @@ private def parseArgs (args : List String) : Except String TestMode := else .error "-n or --num must be followed by a number of iterations" -/-- +/-- This should be the main function used in a benchmark. In general the workflow will be: * Define the function(s) you wish to benchmark @@ -228,19 +229,17 @@ This should be the main function used in a benchmark. In general the workflow wi -/ def benchMain (args : List String) (bench : Runner) : IO UInt32 := do match parseArgs args with - | .ok mode => + | .ok mode => let result ← Runner.run bench mode.rounds |>.print match mode.loggingMode with - | .stdOut => + | .stdOut => for line in result do IO.println line return 0 - | .fsOut name? => + | .fsOut name? => let filename := match name? with | some name => name | none => "benchmark" IO.FS.writeFile filename <| result.foldl (init := "") (fun acc line => acc ++ line ++ "\n") return 0 - | .error str => + | .error str => IO.eprintln str return 1 - - \ No newline at end of file diff --git a/YatimaStdLib/Bit.lean b/YatimaStdLib/Bit.lean index c54857d..c4deef7 100644 --- a/YatimaStdLib/Bit.lean +++ b/YatimaStdLib/Bit.lean @@ -127,7 +127,7 @@ def UInt8.toBits (u : UInt8) : List Bit := Bit.listPad 8 $ Nat.toBits $ UInt8.toNat u def ByteArray.toBits (ba : ByteArray) : List Bit := - List.join $ List.map UInt8.toBits $ ByteArray.toList ba + List.flatten $ List.map UInt8.toBits $ ByteArray.toList ba /-- Generates the array of binary expansions between `0` and `2^n` -/ def getBits (n : Nat) : Array (Array Bit) := Id.run do diff --git a/YatimaStdLib/ByteArray.lean b/YatimaStdLib/ByteArray.lean index bfe0948..e0d17b0 100644 --- a/YatimaStdLib/ByteArray.lean +++ b/YatimaStdLib/ByteArray.lean @@ -5,12 +5,12 @@ namespace ByteArray /-- Read Nat from Little-Endian ByteArray -/ def asLEtoNat (b : ByteArray) : Nat := - b.data.data.enum.foldl (init := 0) + b.data.toList.enum.foldl (init := 0) fun acc (i, bᵢ) => acc + bᵢ.toNat.shiftLeft (i * 8) /-- Read Nat from Big-Endian ByteArray -/ def asBEtoNat (b : ByteArray) : Nat := - b.data.data.foldl (init := 0) fun acc bᵢ => acc.shiftLeft 8 + bᵢ.toNat + b.data.toList.foldl (init := 0) fun acc bᵢ => acc.shiftLeft 8 + bᵢ.toNat /-- Returns the index of -/ def leadingZeroBits (bytes : ByteArray) : Nat := Id.run do @@ -34,7 +34,7 @@ def beq : @& ByteArray → @& ByteArray → Bool := beqL def ordL (a b : ByteArray) : Ordering := - compare a.data.data b.data.data + compare a.data.toList b.data.toList @[extern "lean_byte_array_ord"] def ord : @& ByteArray → @& ByteArray → Ordering := @@ -49,7 +49,7 @@ instance : DecidableEq ByteArray | isFalse h₂ => isFalse $ fun h => by cases h; exact (h₂ rfl) def Subarray.asBA (s : Subarray UInt8) : ByteArray := - s.as.data.toByteArray + s.array.toList.toByteArray def toString (bs : ByteArray) : String := Id.run do if bs.isEmpty then "b[]" else @@ -102,7 +102,7 @@ def sliceL (bs : ByteArray) (i n : Nat) : ByteArray := | 0, _ => acc | n, [] => acc ++ (.mkArray n 0) | n + 1, b :: bs => aux (acc.push b) n bs - .mk $ aux #[] n (bs.data.data.drop i) + .mk $ aux #[] n (bs.data.toList.drop i) @[extern "lean_byte_array_slice"] def slice : @& ByteArray → Nat → Nat → ByteArray := @@ -110,22 +110,21 @@ def slice : @& ByteArray → Nat → Nat → ByteArray := theorem sliceL.aux_size : (sliceL.aux acc n bs).size = acc.size + n := by induction bs generalizing acc n - · induction n <;> simp [sliceL.aux, ByteArray.size, Array.size] + · induction n <;> simp [sliceL.aux] rename_i ih cases n · simp [sliceL.aux] simp [sliceL.aux, ByteArray.size, ih] - rw [Nat.succ_eq_add_one, Nat.add_assoc, Nat.add_comm 1 _] + rw [Nat.add_assoc, Nat.add_comm 1 _] theorem slice_size : (slice bytes i n).size = n := by simp [slice, sliceL, sliceL.aux, sliceL.aux_size, ByteArray.size] -theorem set_size : (set arr i u).size = arr.size := by +theorem set_size : (set arr i u (h := h)).size = arr.size := by simp [size, set] theorem set!_size : (set! arr i u).size = arr.size := by - simp [size, set!, Array.set!, Array.setD] - by_cases h : i < arr.data.size <;> simp [h] + simp [size, set!, Array.set!] /- In this section we define Arithmetic on ByteArrays viewed as natural numbers encoded in diff --git a/YatimaStdLib/ByteVector.lean b/YatimaStdLib/ByteVector.lean index bd42aff..bfb606b 100644 --- a/YatimaStdLib/ByteVector.lean +++ b/YatimaStdLib/ByteVector.lean @@ -1,5 +1,5 @@ import YatimaStdLib.ByteArray -import Std.Data.Nat.Lemmas +import Batteries.Data.Nat.Lemmas structure ByteVector (n : Nat) where data : ByteArray @@ -15,7 +15,7 @@ instance : BEq (ByteVector n) where beq x y := x.data == y.data def toString (vec : ByteVector n) : String := - let str := s!"⟨{", ".intercalate (vec.data.data.data.map ToString.toString)}⟩" + let str := s!"⟨{", ".intercalate (vec.data.data.toList.map ToString.toString)}⟩" s!"{n.toSubscriptString}{str}" instance : ToString (ByteVector n) := ⟨toString⟩ @@ -24,20 +24,20 @@ def ofByteArray (bytes : ByteArray) : ByteVector bytes.size := ⟨bytes, rfl⟩ def get (vec : ByteVector n) (i : Nat) (h : i < n) : UInt8 := - vec.data.get ⟨i, by simp only [vec.valid, h]⟩ + vec.data.get i (h := by simp only [vec.valid, h]) def get' (vec : ByteVector n) (i : Fin n) : UInt8 := - vec.data.get ⟨i, by simp only [vec.valid, i.isLt]⟩ + vec.data.get i (h := by simp only [vec.valid, i.isLt]) def get! (vec : ByteVector n) (i : Nat) : UInt8 := vec.data.get! i def set (vec : ByteVector n) (i : Nat) (h : i < n) (u : UInt8) : ByteVector n := - let data := vec.data.set ⟨i, by simp only [vec.valid, h]⟩ u + let data := vec.data.set i (h := by simp only [vec.valid, h]) u ⟨data, by rw [ByteArray.set_size, vec.valid]⟩ def set' (vec : ByteVector n) (i : Fin n) (u : UInt8) : ByteVector n := - let data := vec.data.set ⟨i, by simp only [vec.valid, i.isLt]⟩ u + let data := vec.data.set i (h := by simp only [vec.valid, i.isLt]) u ⟨data, by rw [ByteArray.set_size, vec.valid]⟩ def set! (vec : ByteVector n) (i : Nat) (u : UInt8) : ByteVector n := @@ -49,7 +49,7 @@ def genWith (f : Fin n → UInt8) : ByteVector n := Id.run do for h : i in [0 : n] do have := Membership.mem.upper h res := res.set i this (f $ Fin.mk i this) - return res + return res def ofNat (n capacity : Nat) : ByteVector capacity := ⟨n.toByteArrayLE.slice 0 capacity, ByteArray.slice_size⟩ @@ -83,12 +83,12 @@ def split (x : ByteVector n) (size₁ size₂ : Nat) : ByteVector size₁ × Byt (⟨left, ByteArray.slice_size⟩, ⟨right, ByteArray.slice_size⟩) open Array in -def append (x : ByteVector n) (y : ByteVector m) : ByteVector (n + m) := +def append (x : ByteVector n) (y : ByteVector m) : ByteVector (n + m) := let ⟨xData, xSize⟩ := x let ⟨yData, ySize⟩ := y ⟨⟨xData.data ++ yData.data⟩, append_size xData.data yData.data xSize ySize⟩ -def shiftRight1 (x : ByteVector n) : ByteVector n := +def shiftRight1 (x : ByteVector n) : ByteVector n := ⟨x.data.slice 1 n, ByteArray.slice_size⟩ def shiftRight (x : ByteVector n) : Nat → ByteVector n @@ -109,7 +109,7 @@ def xor (x : ByteVector n) (y : ByteVector n) : ByteVector n := def not (x : ByteVector n) : ByteVector n := x.map (255 - ·) -def add (x y : ByteVector n) : ByteVector n := +def add (x y : ByteVector n) : ByteVector n := ⟨x.data + y.data |>.slice 0 n, ByteArray.slice_size⟩ instance : Add (ByteVector n) where @@ -125,7 +125,7 @@ instance : HMul (ByteVector n) UInt8 (ByteVector n) where private def naiiveMul (x y : ByteVector n) : ByteVector n := ⟨x.data * y.data |>.slice 0 n, ByteArray.slice_size⟩ -def karatsubaMul (x y : ByteVector n) : ByteVector n := +def karatsubaMul (x y : ByteVector n) : ByteVector n := ⟨x.data * y.data |>.slice 0 n, ByteArray.slice_size⟩ instance : Mul (ByteVector n) where diff --git a/YatimaStdLib/Cached.lean b/YatimaStdLib/Cached.lean index ed9191c..72251c8 100644 --- a/YatimaStdLib/Cached.lean +++ b/YatimaStdLib/Cached.lean @@ -1,6 +1,6 @@ namespace Cached -structure Cached {α : Type u} {β : Type v} (f : α → β) (x : α) := +structure Cached {α : Type u} {β : Type v} (f : α → β) (x : α) where val : β isFX : f x = val deriving Repr diff --git a/YatimaStdLib/Cronos.lean b/YatimaStdLib/Cronos.lean index 5e76964..2ec5364 100644 --- a/YatimaStdLib/Cronos.lean +++ b/YatimaStdLib/Cronos.lean @@ -1,8 +1,8 @@ import YatimaStdLib.RBMap structure Cronos where - refs : Std.RBMap String Nat compare - data : Std.RBMap String Nat compare + refs : Batteries.RBMap String Nat compare + data : Batteries.RBMap String Nat compare deriving Inhabited namespace Cronos diff --git a/YatimaStdLib/Either.lean b/YatimaStdLib/Either.lean index 775cbf1..099c486 100644 --- a/YatimaStdLib/Either.lean +++ b/YatimaStdLib/Either.lean @@ -51,7 +51,7 @@ def leftsArray (l : List $ Either α β) : Array α := | _ => acc def lefts (l : List $ Either α β) : List α := - leftsArray l |>.data + leftsArray l |>.toList /-- Faster version of `lefts`, but the resulting order is reversed. -/ def leftsReverse (l : List $ Either α β) : List α := @@ -71,7 +71,7 @@ def rightsReverse (l : List $ Either α β) : List β := | _ => acc def rights (l : List $ Either α β) : List β := - rightsArray l |>.data + rightsArray l |>.toList @[specialize] def either (f : α → χ) (g : β → χ) : Either α β → χ | .left a => f a diff --git a/YatimaStdLib/HashMap.lean b/YatimaStdLib/HashMap.lean index deba00c..8138b33 100644 --- a/YatimaStdLib/HashMap.lean +++ b/YatimaStdLib/HashMap.lean @@ -3,8 +3,8 @@ import YatimaStdLib.HashSet namespace Std -def HashMap.unionWith {α β : Type _} [BEq α] [Hashable α] [Inhabited β] (combine : β → β → β) - (s₁ s₂ : HashMap α β) : HashMap α β := - s₁.fold - (fun map key value => - map.insert key (combine value <| map.findD key default)) s₂ +def HashMap.unionWith {α β : Type _} [BEq α] [Hashable α] [Inhabited β] (combine : β → β → β) + (s₁ s₂ : HashMap α β) : HashMap α β := + s₁.fold + (fun map key value => + map.insert key (combine value <| map.getD key default)) s₂ diff --git a/YatimaStdLib/HashSet.lean b/YatimaStdLib/HashSet.lean index c3ad5df..488f02f 100644 --- a/YatimaStdLib/HashSet.lean +++ b/YatimaStdLib/HashSet.lean @@ -1,4 +1,4 @@ -import Lean.Data.HashSet +import Std.Data.HashSet syntax "⦃" term,* "⦄" : term @@ -12,12 +12,9 @@ macro_rules acc ← `(HashSet.insert $acc $x) return ← `($acc) -instance [ToString α] [BEq α] [Hashable α] : ToString (HashSet α) where - toString set := +instance [ToString α] [BEq α] [Hashable α] : ToString (Std.HashSet α) where + toString set := let content := ", ".intercalate (set |>.toList |>.reverse |>.map fun k => s!"{k}") s!"⦃{content}⦄" namespace Std.HashSet - -def union {α : Type _} [BEq α] [Hashable α] (s t : HashSet α) : HashSet α := - s.fold (HashSet.insert) t diff --git a/YatimaStdLib/Int.lean b/YatimaStdLib/Int.lean index 3d43aca..4f0c806 100644 --- a/YatimaStdLib/Int.lean +++ b/YatimaStdLib/Int.lean @@ -1,11 +1,11 @@ import YatimaStdLib.Bit import YatimaStdLib.Nat -import Std.Data.Int.Basic +import Batteries.Data.Int import YatimaStdLib.Bitwise namespace Int -open Nat hiding bitwise +open Nat --hiding bitwise def toUInt8 (x : Int) : UInt8 := Bit.bitsToUInt8 x.toBits @@ -22,7 +22,7 @@ def gcdExtNat (a : Nat) (b : Nat) : Int × Int × Int := match h : b with | 0 => (1, 0, a) | k + 1 => - let p := quotRem a b + let p := Nat.quotRem a b let q := p.1 let r := p.2 have : r < k.succ := by @@ -32,7 +32,6 @@ def gcdExtNat (a : Nat) (b : Nat) : Int × Int × Int := exact Nat.zero_lt_of_ne_zero h2 let (s, t, g) := gcdExtNat b r (t, s - q * t, g) - termination_by _ => b def gcdExt (a : Int) (b : Int) : Int × Int × Int := gcdExtNat (Int.natAbs a) (Int.natAbs b) diff --git a/YatimaStdLib/Lean.lean b/YatimaStdLib/Lean.lean index 6a35c46..819c4f2 100644 --- a/YatimaStdLib/Lean.lean +++ b/YatimaStdLib/Lean.lean @@ -2,12 +2,6 @@ import Lean namespace Lean.Expr -def constName (e : Expr) : Name := - e.constName?.getD Name.anonymous - -def getAppFnArgs (e : Expr) : Name × Array Expr := - withApp e fun e a => (e.constName, a) - /-- Converts a `Expr` of a list to a list of `Expr`s -/ partial def toListExpr (e : Expr) : List Expr := match e.getAppFnArgs with diff --git a/YatimaStdLib/List.lean b/YatimaStdLib/List.lean index e66fb42..696664a 100644 --- a/YatimaStdLib/List.lean +++ b/YatimaStdLib/List.lean @@ -1,7 +1,7 @@ import YatimaStdLib.Applicative import YatimaStdLib.Foldable import YatimaStdLib.Traversable -import Std.Data.List.Basic +import Batteries.Data.List.Basic namespace List diff --git a/YatimaStdLib/MLE/MultilinearLagrangePolynomial.lean b/YatimaStdLib/MLE/MultilinearLagrangePolynomial.lean index 9b38a65..a331311 100644 --- a/YatimaStdLib/MLE/MultilinearLagrangePolynomial.lean +++ b/YatimaStdLib/MLE/MultilinearLagrangePolynomial.lean @@ -8,18 +8,18 @@ scoped instance : Coe (List (Nat × Int)) (List (Nat × Zmod n)) where /-- Reads cached polynomials from a JSON file -/ def polynomialsFromCache : - IO $ Std.RBMap (Nat × Nat) (MultilinearPolynomial $ Zmod n) compare := + IO $ Batteries.RBMap (Nat × Nat) (MultilinearPolynomial $ Zmod n) compare := return cachedMLPData.foldl (fun acc (k, v) => acc.insert k (.ofPairs v)) default def pallasFSize := 0x40000000000000000000000000000000224698fc094cf91b992d30ed00000001 def vestaFSize := 0x40000000000000000000000000000000224698fc0994a8dd8c46eb2100000001 initialize pallasCache : - Std.RBMap (Nat × Nat) (MultilinearPolynomial $ Zmod pallasFSize) compare + Batteries.RBMap (Nat × Nat) (MultilinearPolynomial $ Zmod pallasFSize) compare ← polynomialsFromCache initialize vestaCache : - Std.RBMap (Nat × Nat) (MultilinearPolynomial $ Zmod vestaFSize) compare + Batteries.RBMap (Nat × Nat) (MultilinearPolynomial $ Zmod vestaFSize) compare ← polynomialsFromCache inductive Curve @@ -31,7 +31,7 @@ def Curve.fSize : Curve → Nat | .vesta => vestaFSize def Curve.cache : (c : Curve) → - Std.RBMap (Nat × Nat) (MultilinearPolynomial $ Zmod c.fSize) compare + Batteries.RBMap (Nat × Nat) (MultilinearPolynomial $ Zmod c.fSize) compare | .pallas => pallasCache | .vesta => vestaCache diff --git a/YatimaStdLib/Matrix.lean b/YatimaStdLib/Matrix.lean index 47214fa..7922c4b 100644 --- a/YatimaStdLib/Matrix.lean +++ b/YatimaStdLib/Matrix.lean @@ -8,6 +8,8 @@ Note we do not use any dependent types or any useful features of Lean. This was will hopefully improve with time and more lemmas about arrays available in `std4` -/ +namespace YatimaStdLib + variable (R : Type) [Ring R] section vector @@ -20,7 +22,7 @@ variable {R} [OfNat R (nat_lit 0)] /- NOTE : All these definitions only make sense when we know that the two arrays representing the -vectors have the same dimension. Otherwise you'll get nonsense. +vectors have the same dimension. Otherwise you'll get nonsense. Look at `AbstractMatrix.lean` for a comment on the prefered solution where vectors carry their length, which is currently blocked by some formalization of Array lemmas that still needs to be done in the standard library. @@ -85,4 +87,4 @@ def twoInv [Field R] (M : Matrix R) : Matrix R := (Field.inv det) * #[#[M[1]![1]!, -M[0]![1]!], #[-M[1]![0]!, M[0]![0]!]] end Matrix -end matrix \ No newline at end of file +end matrix diff --git a/YatimaStdLib/MultilinearPolynomial.lean b/YatimaStdLib/MultilinearPolynomial.lean index 479dcd1..fed651e 100644 --- a/YatimaStdLib/MultilinearPolynomial.lean +++ b/YatimaStdLib/MultilinearPolynomial.lean @@ -1,4 +1,4 @@ -import Std.Data.RBMap +import Batteries.Data.RBMap import YatimaStdLib.Nat import LSpec @@ -15,12 +15,12 @@ For example, `(6, 9)` encodes `9x₁x₂` because * `9` is the coefficient * `6₁₀ = 110₂`, so the variables on indexes `1` and `2` are present -/ -abbrev MultilinearPolynomial α := Std.RBMap Nat α compare +abbrev MultilinearPolynomial α := Batteries.RBMap Nat α compare namespace MultilinearPolynomial /-- The indices of variables in a summand -/ -abbrev Indices := Std.RBSet Nat compare +abbrev Indices := Batteries.RBSet Nat compare /-- Extracts the variable indices encoded on a base -/ def Indices.ofBase (b : Nat) : Indices := @@ -116,7 +116,7 @@ the range of the array are considered to have value 0. Evaluates a MLP on a map that indicates the value of the variables indexed from 0. Variables whose indexes aren't in the map are considered to have value 0. -/ -@[specialize] def eval' (input : Std.RBMap Nat α compare) : α := +@[specialize] def eval' (input : Batteries.RBMap Nat α compare) : α := mlp.foldl (init := 0) fun acc b c => HAdd.hAdd acc $ Indices.ofBase b |>.foldl (init := c) fun acc i => acc * (input.find? i |>.getD 0) diff --git a/YatimaStdLib/Nat.lean b/YatimaStdLib/Nat.lean index 9e64bd0..33f9171 100644 --- a/YatimaStdLib/Nat.lean +++ b/YatimaStdLib/Nat.lean @@ -1,4 +1,4 @@ -import Std.Data.Nat.Basic +import Batteries.Data.Nat.Basic namespace Nat @@ -135,7 +135,7 @@ def get2Adicity (n : Nat) : Nat × Nat := let rec loop (m acc : Nat) := match h : m with | 0 | 1 => (acc, 1) - | _ + 1 => + | _ + 1 => have : m / 2 < m := Nat.bitwise_rec_lemma (h ▸ Nat.succ_ne_zero _) if m % 2 ==0 then loop (m / 2) (acc + 1) else (acc, m) loop n 0 @@ -184,30 +184,4 @@ def asHex (n : Nat) (length : Nat) : String := let pad := List.replicate (length - tail.length) '0' "0x" ++ List.asString (pad ++ tail) -def subDigitChar (n : Nat) : Char := - if n = 0 then '₀' else - if n = 1 then '₁' else - if n = 2 then '₂' else - if n = 3 then '₃' else - if n = 4 then '₄' else - if n = 5 then '₅' else - if n = 6 then '₆' else - if n = 7 then '₇' else - if n = 8 then '₈' else - if n = 9 then '₉' else - '*' - -partial def toSubDigitsAux : Nat → List Char → List Char - | n, ds => - let d := subDigitChar <| n % 10; - let n' := n / 10; - if n' = 0 then d::ds - else toSubDigitsAux n' (d::ds) - -def toSubDigits (n : Nat) : List Char := - toSubDigitsAux n [] - -def toSubscriptString (n : Nat) : String := - (toSubDigits n).asString - end Nat diff --git a/YatimaStdLib/Polynomial.lean b/YatimaStdLib/Polynomial.lean index e479d81..0445a27 100644 --- a/YatimaStdLib/Polynomial.lean +++ b/YatimaStdLib/Polynomial.lean @@ -5,8 +5,8 @@ In this module we define univariate polynomials over a type `R`, together with b defining their evaluation, arithmetic, and divisibility. -/ -/-- -The type of a polynomial with coefficients in `R`. +/-- +The type of a polynomial with coefficients in `R`. NOTE : We encode polynomials in such a way so that the `i`th entry of the array corresponds to the degree `i-1` coefficient. For example `#[a,b,c]` <--> `a + b x + c x^2` @@ -29,13 +29,13 @@ instance [Inhabited R] : Inhabited (Polynomial R) where instance : Append (Polynomial A) where append := .append -private def tail (ar : Polynomial A) : Polynomial A := ar.eraseIdx 0 +private def tail (ar : Polynomial A) : Polynomial A := ar.eraseIdxIfInBounds 0 -variable {A : Type _ } [Add A] [Mul A] [HPow A Nat A] [OfNat A (nat_lit 1)] [OfNat A (nat_lit 0)] +variable {A : Type _ } [Add A] [Mul A] [HPow A Nat A] [OfNat A (nat_lit 1)] [OfNat A (nat_lit 0)] [BEq A] [Div A] [Neg A] /-- Returns a "normalized" form for a polynomial, dropping the leading zeroes -/ -def norm (f : Polynomial A) : Polynomial A := +def norm (f : Polynomial A) : Polynomial A := let ans := f.popWhile (· == 0) if ans.size == 0 then #[0] else ans @@ -70,7 +70,7 @@ def makeMonic (f : Polynomial A) : Polynomial A := (1 / f.lead) * f def eval (f : Polynomial A) (a : A) : A := let f := f.norm let action (i : Fin f.size) c := c * a ^ (i : Nat) - Array.foldr (. + .) 0 (f.mapIdx action) + Array.foldr (. + .) 0 (f.mapFinIdx action) private def zeros (n : Nat) : Polynomial A := mkArray n 0 @@ -78,7 +78,7 @@ private def zeros (n : Nat) : Polynomial A := mkArray n 0 def zero : Polynomial A := #[0] private def padZeroes (f : Polynomial A) (n : Nat) : Polynomial A := - f ++ zeros n + f ++ zeros n /-- Returns the addition addition of two polynomials -/ def polyAdd (f : Polynomial A) (g : Polynomial A) : Polynomial A := @@ -111,7 +111,7 @@ def polyMul (f : Polynomial A) : Polynomial A → Polynomial A := instance : Mul (Polynomial A) where mul := polyMul -/-- +/-- Returns `(q, r)` where `q` is the quotient of division of polynomial `f` by `g` and `r` is the remainder -/ @@ -119,7 +119,7 @@ def polyQuotRem (f : Polynomial A) (g : Polynomial A) : Polynomial A × Polynomi let rec polyQRAux (f' g' : Polynomial A) (n : Nat) : Polynomial A × Polynomial A := match n with | 0 => (#[], #[]) - | k + 1 => + | k + 1 => if k + 1 < g'.size then (#[],f') else let x := f'.getD 0 0 @@ -138,7 +138,7 @@ def polyDiv (f g : Polynomial A) : Polynomial A := polyQuotRem f g |>.fst /-- Returns the remainder of the division of the polynomial `f` by `g` -/ def polyMod (f g : Polynomial A) : Polynomial A := polyQuotRem f g |>.snd -/-- +/-- Returns `(a, b, d)` where `d` is the greatest common divisor of `f` and `g` and `a`, `b` satisfy `a * f + b * g = d ` @@ -146,20 +146,20 @@ Returns `(a, b, d)` where `d` is the greatest common divisor of `f` and `g` and TODO : Eliminate `partial` using `termination_by _ => g.degree` and a proof that `polyQuotRem` reduces degree. -/ -partial def polyEuc [Inhabited A] [Div A] (f g : Polynomial A) : Polynomial A × Polynomial A × Polynomial A - := if g.isZero then +partial def polyEuc [Inhabited A] [Div A] (f g : Polynomial A) : Polynomial A × Polynomial A × Polynomial A + := if g.isZero then (#[1 / f.lead], #[0], f.makeMonic) else let (q, r) := polyQuotRem f g let (s, t, d) := polyEuc g r (t, s - q * t, d) -/-- +/-- Returns the monic polynomial with the roots taken from the list `a`. -/ def rootsToPoly (as : List A) : Polynomial A := match as with | [] => #[1] - | (root :: roots) => + | (root :: roots) => let monom : Polynomial A := #[-root,1] monom * (rootsToPoly roots) diff --git a/YatimaStdLib/RBMap.lean b/YatimaStdLib/RBMap.lean index 2512205..d9aff91 100644 --- a/YatimaStdLib/RBMap.lean +++ b/YatimaStdLib/RBMap.lean @@ -1,6 +1,6 @@ -import Std.Data.RBMap +import Batteries.Data.RBMap -namespace Std.RBMap +namespace Batteries.RBMap variable {cmp : α → α → Ordering} @@ -17,7 +17,7 @@ def filterOut [BEq α] [Ord α] (map : RBMap α β cmp) (t : RBSet α cmp) : def fromArray (x : Array (α × β)) : RBMap α β cmp := x.foldl (fun r p => r.insert p.1 p.2) (mkRBMap α β cmp) -/- +/- Merge two RBMaps, always taking the first value in case of a key being present in both maps. Intended for set simulation. -/ @@ -35,4 +35,4 @@ def mapKeys [Ord χ] (m : RBMap α β cmp) (f : α → χ) : RBMap χ β compare def zipD (m₁ : RBMap α β₁ cmp) (m₂ : RBMap α β₂ cmp) (b₂ : β₂) : RBMap α (β₁ × β₂) cmp := m₁.foldl (init := default) fun acc a b₁ => acc.insert a (b₁, m₂.findD a b₂) -end Std.RBMap +end Batteries.RBMap diff --git a/YatimaStdLib/RBNode.lean b/YatimaStdLib/RBNode.lean index 2d97f71..3d00e3a 100644 --- a/YatimaStdLib/RBNode.lean +++ b/YatimaStdLib/RBNode.lean @@ -1,6 +1,6 @@ -import Std.Data.RBMap +import Batteries.Data.RBMap -open Std Lean +open Batteries Lean namespace Lean.RBNode @@ -12,16 +12,16 @@ instance [BEq α] [BEq β] : BEq (Lean.RBNode α fun _ => β) where end Lean.RBNode -namespace Std.RBMap +namespace Batteries.RBMap -@[inline] def findM {ordering : α → α → Ordering} [Monad m] [MonadExcept ε m] +@[inline] def findM {ordering : α → α → Ordering} [Monad m] [MonadExcept ε m] (rbmap : RBMap α β ordering) (a : α) (e : ε) : m β := - match rbmap.find? a with + match rbmap.find? a with | some b => pure b | none => throw e -instance [ToString α] [ToString β] {ordering : α → α → Ordering} : +instance [ToString α] [ToString β] {ordering : α → α → Ordering} : ToString (RBMap α β ordering) := { toString := fun rbmap => s!"{rbmap.toList}" } -end Std.RBMap +end Batteries.RBMap diff --git a/YatimaStdLib/Rat.lean b/YatimaStdLib/Rat.lean index f2e2cb5..30dbb49 100644 --- a/YatimaStdLib/Rat.lean +++ b/YatimaStdLib/Rat.lean @@ -1,22 +1,22 @@ import YatimaStdLib.Ring -import Std.Data.Rat.Basic +import Batteries.Data.Rat.Basic namespace Rat -def powAux (base : Rat) (exp : Nat) : Rat := +def powAux (base : Rat) (exp : Nat) : Rat := let rec go (power acc : Rat) (n : Nat) : Rat := match h : n with | 0 => acc | _ + 1 => let n' := n / 2 - have : n' < n := Nat.bitwise_rec_lemma (h ▸ Nat.succ_ne_zero _) + have : n' < n := Nat.bitwise_rec_lemma (h ▸ Nat.succ_ne_zero _) if n % 2 == 0 then go (power * power) acc n' else go (power * power) (acc * power) n' go base 1 exp instance : Field Rat where - hPow r n := powAux r n + hPow r n := powAux r n coe a := { num := a, reduced := by simp only [Nat.Coprime, Nat.coprime_one_right]} zero := 0 one := 1 @@ -24,7 +24,7 @@ instance : Field Rat where def abs (r : Rat) : Rat := {r with num := r.num.natAbs} -def round (r : Rat) : Int := +def round (r : Rat) : Int := let floor := r.floor if abs (r - floor) ≤ (1 : Rat)/2 then floor else r.ceil diff --git a/YatimaStdLib/SparseMatrix.lean b/YatimaStdLib/SparseMatrix.lean index fafde4f..1ef427b 100644 --- a/YatimaStdLib/SparseMatrix.lean +++ b/YatimaStdLib/SparseMatrix.lean @@ -2,10 +2,10 @@ import YatimaStdLib.Array import YatimaStdLib.Ord import YatimaStdLib.Ring import YatimaStdLib.RBMap -import Std.Data.RBMap +import Batteries.Data.RBMap structure SparseMatrix (R : Type _) where - entries : Std.RBMap (Nat × Nat) R compare + entries : Batteries.RBMap (Nat × Nat) R compare rows : Nat cols : Nat @@ -13,18 +13,18 @@ instance [ToString R] : ToString (SparseMatrix R) where toString m := let print (p : (Nat × Nat) × R) := match p with - | ((i,j), v) => - "row:" ++ + | ((i,j), v) => + "row:" ++ toString i ++ " col:" ++ toString j ++ " " ++ toString v ++ "\n" let triples := - print <$> Std.RBMap.toList m.entries + print <$> Batteries.RBMap.toList m.entries List.foldr (. ++ .) "" triples -open Std.RBMap +open Batteries.RBMap namespace SparseMatrix @@ -32,14 +32,14 @@ namespace SparseMatrix Empty matrix -/ def empty (col : Nat) (row : Nat) : SparseMatrix R := - SparseMatrix.mk Std.RBMap.empty col row + SparseMatrix.mk Batteries.RBMap.empty col row /-- Insert a triple -/ def insert (m : SparseMatrix R) (col row : Nat) (a : R) : SparseMatrix R := SparseMatrix.mk - (Std.RBMap.insert m.entries (col,row) a) + (Batteries.RBMap.insert m.entries (col,row) a) m.rows m.cols @@ -49,7 +49,7 @@ Creates a sparse matrix from a list def ofListWithDims (rows : Nat) (cols : Nat) (l : List ((Nat × Nat) × R)) : SparseMatrix R := SparseMatrix.mk - (Std.RBMap.ofList l compare) + (Batteries.RBMap.ofList l compare) rows cols @@ -59,14 +59,14 @@ Creates a sparse matrix from an array def ofArrayWithDims (rows : Nat) (cols : Nat) (l : Array ((Nat × Nat) × R)) : SparseMatrix R := SparseMatrix.mk - (Std.RBMap.ofArray l compare) + (Batteries.RBMap.ofArray l compare) rows cols instance : Functor SparseMatrix where map f m := SparseMatrix.mk - (Std.RBMap.mapVal (fun _ x => f x) m.entries) + (Batteries.RBMap.mapVal (fun _ x => f x) m.entries) m.rows m.cols @@ -84,7 +84,7 @@ Transpose a sparse matrix -/ def transpose (m : SparseMatrix R) : SparseMatrix R := SparseMatrix.mk - (Std.RBMap.mapKeys m.entries $ fun (a,b) => (b,a)) + (Batteries.RBMap.mapKeys m.entries $ fun (a,b) => (b,a)) m.cols m.rows @@ -107,7 +107,7 @@ def addition (m₁ m₂ : SparseMatrix R) : SparseMatrix R := instance : Add (SparseMatrix R) where add := SparseMatrix.addition -abbrev SparseArray R := Std.RBMap Nat R compare +abbrev SparseArray R := Batteries.RBMap Nat R compare def SparseArray.zipProd (x y : SparseArray R) : SparseArray R := y.foldl (init := default) fun acc k v => match x.find? k with @@ -126,14 +126,14 @@ instance : BEq (SparseArray R) where beq x y := x.prune == y.prune def Array.toSparse (x : Array R) : SparseArray R := - SparseArray.prune $ Std.RBMap.fromArray $ Array.zip (Array.iota x.size) (x : Array R) + SparseArray.prune $ Batteries.RBMap.fromArray $ Array.zip (Array.iota x.size) (x : Array R) -def collectRows (m : SparseMatrix R) : Std.RBMap Nat (SparseArray R) compare := +def collectRows (m : SparseMatrix R) : Batteries.RBMap Nat (SparseArray R) compare := m.entries.foldl (init := default) fun acc (i, j) v => match acc.find? i with | some arr => acc.insert i (arr.insert j v) | none => acc.insert i (.single j v) -def collectCols (m : SparseMatrix R) : Std.RBMap Nat (SparseArray R) compare := +def collectCols (m : SparseMatrix R) : Batteries.RBMap Nat (SparseArray R) compare := m.entries.foldl (init := default) fun acc (i, j) v => match acc.find? j with | some arr => acc.insert j (arr.insert i v) | none => acc.insert j (.single i v) diff --git a/YatimaStdLib/StringInterner/Backend/Buffer.lean b/YatimaStdLib/StringInterner/Backend/Buffer.lean index 878f20a..daf3ff9 100644 --- a/YatimaStdLib/StringInterner/Backend/Buffer.lean +++ b/YatimaStdLib/StringInterner/Backend/Buffer.lean @@ -72,7 +72,7 @@ def resolveIndexToStr (index : Nat) : BufferM String := do let (strLen, strLenBytes) ← decodeVarSize! index let start := index + strLenBytes let strBytes := (← get).data.extract start (start + strLen) - return .fromUTF8Unchecked strBytes + return .fromUTF8! strBytes end BufferM diff --git a/YatimaStdLib/StringInterner/Interner.lean b/YatimaStdLib/StringInterner/Interner.lean index 5ab17de..b995679 100644 --- a/YatimaStdLib/StringInterner/Interner.lean +++ b/YatimaStdLib/StringInterner/Interner.lean @@ -50,7 +50,7 @@ def run' (state : StringInterner α) (b : Buffer := default) def getOrIntern (str : String) : StringInterner Symbol := do let hash := str.hash - match (← get).find? hash with + match (← get).get? hash with | some sym => return sym | none => let symbol ← MonadBackend.intern str @@ -58,7 +58,7 @@ def getOrIntern (str : String) : StringInterner Symbol := do return symbol def get (str : String) : StringInterner (Option Symbol) := do - return (← StateT.get).find? str.hash + return (← StateT.get).get? str.hash def resolve! (symbol : Symbol) : StringInterner String := MonadBackend.resolve! symbol diff --git a/YatimaStdLib/Tree.lean b/YatimaStdLib/Tree.lean index 268c06d..9b2f944 100644 --- a/YatimaStdLib/Tree.lean +++ b/YatimaStdLib/Tree.lean @@ -1,6 +1,6 @@ import YatimaStdLib.String -inductive Tree (α : Type) where +inductive Tree (α : Type) where | empty : Tree α | node : α → List (Tree α) → Tree α deriving BEq, Repr @@ -34,10 +34,10 @@ partial def size : Tree α → Nat node a [] @[inline] partial def bind : Tree α → (α → Tree β) → Tree β := - fun x b => match x with - | empty => empty - | node x ts => - match b x with + fun x b => match x with + | empty => empty + | node x ts => + match b x with | empty => empty | node x' ts' => node x' (ts' ++ List.map (fun ta => bind ta b) ts) @@ -50,9 +50,9 @@ mutual partial def preorder : Tree α → List α | empty => [] | node x ts => x :: preorderF ts - + partial def preorderF (ts : List $ Tree α) : List α := - (ts.map preorder).join + (ts.map preorder).flatten end @@ -61,9 +61,9 @@ mutual partial def postorder : Tree α → List α | empty => [] | node x ts => postorderF ts ++ [x] - + partial def postorderF (ts : List $ Tree α) : List α := - (ts.map postorder).join + (ts.map postorder).flatten end diff --git a/YatimaStdLib/UInt.lean b/YatimaStdLib/UInt.lean index a94e144..6285062 100644 --- a/YatimaStdLib/UInt.lean +++ b/YatimaStdLib/UInt.lean @@ -33,14 +33,13 @@ def sum3 (i a b : UInt8) : UInt8 × UInt8 := end UInt8 def UInt16.toByteArrayL (n : UInt16) : ByteArray := - ⟨#[n.toUInt8, (n / 256) % 65536 |>.toUInt8]⟩ + ⟨#[n.toUInt8, (n / 256) |>.toUInt8]⟩ @[extern "lean_uint16_to_byte_array"] def UInt16.toByteArray : UInt16 → ByteArray := UInt16.toByteArrayL -theorem UInt16.toByteArray_size_2 : (UInt16.toByteArray n).size = 2 := by - simp [ByteArray.size, Array.size, List.length] +theorem UInt16.toByteArray_size_2 : (UInt16.toByteArray n).size = 2 := by rfl def UInt32.toByteArrayL (n : UInt32) : ByteArray := let a₀ := n.toUInt8 @@ -49,15 +48,14 @@ def UInt32.toByteArrayL (n : UInt32) : ByteArray := let n := n / 256 let a₂ := n % 16777216 |>.toUInt8 let n := n / 256 - let a₃ := n % 4294967296 |>.toUInt8 + let a₃ := n |>.toUInt8 ⟨#[a₀, a₁, a₂, a₃]⟩ @[extern "lean_uint32_to_byte_array"] def UInt32.toByteArray : UInt32 → ByteArray := UInt32.toByteArrayL -theorem UInt32.toByteArray_size_4 : (UInt32.toByteArray n).size = 4 := by - simp [ByteArray.size, Array.size, List.length] +theorem UInt32.toByteArray_size_4 : (UInt32.toByteArray n).size = 4 := by rfl def UInt64.toByteArrayL (n : UInt64) : ByteArray := let a₀ := n.toUInt8 @@ -81,5 +79,4 @@ def UInt64.toByteArrayL (n : UInt64) : ByteArray := def UInt64.toByteArray : UInt64 → ByteArray := UInt64.toByteArrayL -theorem UInt64.toByteArray_size_8 : (UInt64.toByteArray n).size = 8 := by - simp [ByteArray.size, Array.size, List.length] +theorem UInt64.toByteArray_size_8 : (UInt64.toByteArray n).size = 8 := by rfl diff --git a/lake-manifest.json b/lake-manifest.json index 7067c7d..0db6b40 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,23 +1,25 @@ -{"version": 7, +{"version": "1.1.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/leanprover/std4/", + [{"url": "https://github.com/argumentcomputer/LSpec", "type": "git", "subDir": null, - "rev": "9e37a01f8590f81ace095b56710db694b5bf8ca0", - "name": "std", + "scope": "lurk-lab", + "rev": "b7d4dc67a5171dee9352506394fa155ba8e3956f", + "name": "LSpec", "manifestFile": "lake-manifest.json", - "inputRev": "9e37a01f8590f81ace095b56710db694b5bf8ca0", + "inputRev": "b7d4dc6", "inherited": false, "configFile": "lakefile.lean"}, - {"url": "https://github.com/lurk-lab/LSpec", + {"url": "https://github.com/leanprover-community/batteries", "type": "git", "subDir": null, - "rev": "3388be5a1d1390594a74ec469fd54a5d84ff6114", - "name": "LSpec", + "scope": "leanprover-community", + "rev": "9089cee37a32d51bc4aeea6506719a21b7a2d011", + "name": "batteries", "manifestFile": "lake-manifest.json", - "inputRev": "3388be5a1d1390594a74ec469fd54a5d84ff6114", + "inputRev": "main", "inherited": false, - "configFile": "lakefile.lean"}], + "configFile": "lakefile.toml"}], "name": "YatimaStdLib", "lakeDir": ".lake"} diff --git a/lakefile.lean b/lakefile.lean index 0bd4a99..99315eb 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -7,25 +7,9 @@ package YatimaStdLib lean_lib YatimaStdLib where precompileModules := true -def ffiC := "ffi.c" -def ffiO := "ffi.o" +require "leanprover-community" / "batteries" @ git "main" -target ffi.o pkg : FilePath := do - let oFile := pkg.buildDir / ffiO - let srcJob ← inputFile $ pkg.dir / ffiC - let flags := #["-I", (← getLeanIncludeDir).toString, "-fPIC"] - buildO ffiC oFile srcJob flags - -extern_lib ffi pkg := do - let name := nameToStaticLib "ffi" - let job ← fetch <| pkg.target ``ffi.o - buildStaticLib (pkg.nativeLibDir / name) #[job] - -require std from git - "https://github.com/leanprover/std4/" @ "9e37a01f8590f81ace095b56710db694b5bf8ca0" - -require LSpec from git - "https://github.com/lurk-lab/LSpec" @ "3388be5a1d1390594a74ec469fd54a5d84ff6114" +require "lurk-lab" / "LSpec" @ git "b7d4dc6" section ImportAll diff --git a/lean-toolchain b/lean-toolchain index 91ccf6a..2ffc30c 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.4.0-rc1 +leanprover/lean4:v4.16.0-rc2 \ No newline at end of file From 3dde3b09b65abf8a4c376f5c8b9ffc674177c29e Mon Sep 17 00:00:00 2001 From: Jad Ghalayini Date: Fri, 31 Jan 2025 19:33:09 +0000 Subject: [PATCH 2/3] Bump LSpec version --- lake-manifest.json | 4 ++-- lakefile.lean | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index 0db6b40..fb52356 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "lurk-lab", - "rev": "b7d4dc67a5171dee9352506394fa155ba8e3956f", + "rev": "7f2c46ba960a24447eb0a0974ba7541892f8524c", "name": "LSpec", "manifestFile": "lake-manifest.json", - "inputRev": "b7d4dc6", + "inputRev": "7f2c46b", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/batteries", diff --git a/lakefile.lean b/lakefile.lean index 99315eb..8f67565 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -9,7 +9,7 @@ lean_lib YatimaStdLib where require "leanprover-community" / "batteries" @ git "main" -require "lurk-lab" / "LSpec" @ git "b7d4dc6" +require "lurk-lab" / "LSpec" @ git "7f2c46b" section ImportAll From f7cccbb3f70465d82c0e37db9301995771ff9c83 Mon Sep 17 00:00:00 2001 From: Jad Ghalayini Date: Fri, 31 Jan 2025 20:05:06 +0000 Subject: [PATCH 3/3] Added FFI back in --- lakefile.lean | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/lakefile.lean b/lakefile.lean index 8f67565..f15c0d7 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -7,11 +7,24 @@ package YatimaStdLib lean_lib YatimaStdLib where precompileModules := true +def ffiC := "ffi.c" +def ffiO := "ffi.o" + +target ffi.o pkg : System.FilePath := do + let oFile := pkg.buildDir / ffiO + let srcJob ← inputFile (pkg.dir / ffiC) true + let flags := #["-I", (← getLeanIncludeDir).toString, "-fPIC"] + buildO (oFile := oFile) (srcJob := srcJob) flags + +extern_lib ffi pkg := do + let name := nameToStaticLib "ffi" + let job ← fetch <| pkg.target ``ffi.o + buildStaticLib (pkg.nativeLibDir / name) #[job] + require "leanprover-community" / "batteries" @ git "main" require "lurk-lab" / "LSpec" @ git "7f2c46b" - section ImportAll open System