From 98e4b2882f643efc86bfbfc75a8973188412a048 Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Mon, 7 Jul 2025 14:41:53 +0200 Subject: [PATCH] refactor: migrate to new ranges (#8841) This PR migrates usages of `Std.Range` to the new polymorphic ranges. This PR unfortunately increases the transitive imports for frequently-used parts of `Init` because the ranges now rely on iterators in order to provide their functionality for types other than `Nat`. However, iteration over ranges in compiled code is as efficient as before in the examples I checked. This is because of a special `IteratorLoop` implementation provided in the PR for this purpose. There were two issues that were uncovered during migration: * In `IndPredBelow.lean`, migrating the last remaining range causes `compilerTest1.lean` to break. I have minimized the issue and came to the conclusion it's a compiler bug. Therefore, I have not replaced said old range usage yet (see #9186). * In `BRecOn.lean`, we are publicly importing the ranges. Making this import private should theoretically work, but there seems to be a problem with the module system, causing the build to panic later in `Init.Data.Grind.Poly` (see #9185). * In `FuzzyMatching.lean`, inlining fails with the new ranges, which would have led to significant slowdown. Therefore, I have not migrated this file either. --- src/Init/Data/Array/Lex/Basic.lean | 15 +- src/Init/Data/Array/Lex/Lemmas.lean | 50 +++- .../Iterators/Consumers/Monadic/Loop.lean | 100 ++++--- .../Internal/LawfulMonadLiftFunction.lean | 37 +++ .../Data/Iterators/Lemmas/Consumers/Loop.lean | 14 +- .../Lemmas/Consumers/Monadic/Loop.lean | 68 ++--- .../Data/Range/Polymorphic/Iterators.lean | 44 ---- .../Data/Range/Polymorphic/NatLemmas.lean | 4 +- .../Data/Range/Polymorphic/RangeIterator.lean | 231 ++++++++++++++++- src/Init/Data/Vector/Basic.lean | 7 +- src/Init/Data/Vector/Lex.lean | 3 +- src/Lean/Compiler/IR/Basic.lean | 2 +- src/Lean/Compiler/IR/EmitLLVM.lean | 4 +- src/Lean/Compiler/IR/SimpCase.lean | 4 +- src/Lean/Compiler/IR/ToIR.lean | 2 +- src/Lean/Compiler/LCNF/Check.lean | 2 +- src/Lean/Compiler/LCNF/ElimDeadBranches.lean | 2 +- src/Lean/Compiler/LCNF/FixedParams.lean | 8 +- src/Lean/Compiler/LCNF/InferType.lean | 6 +- src/Lean/Compiler/LCNF/MonoTypes.lean | 2 +- src/Lean/Compiler/LCNF/PassManager.lean | 2 +- src/Lean/Compiler/LCNF/PhaseExt.lean | 2 +- src/Lean/Compiler/LCNF/Probing.lean | 2 +- src/Lean/Compiler/LCNF/PullFunDecls.lean | 4 +- src/Lean/Compiler/LCNF/Simp/DefaultAlt.lean | 4 +- src/Lean/Compiler/LCNF/Simp/JpCases.lean | 2 +- src/Lean/Compiler/LCNF/SpecInfo.lean | 8 +- src/Lean/Compiler/LCNF/StructProjCases.lean | 4 +- src/Lean/Compiler/LCNF/ToLCNF.lean | 2 +- src/Lean/Compiler/LCNF/ToMono.lean | 4 +- src/Lean/Compiler/LCNF/Util.lean | 4 +- src/Lean/Data/Array.lean | 7 +- src/Lean/Data/FuzzyMatching.lean | 8 +- src/Lean/Data/Json/Basic.lean | 2 +- src/Lean/Elab/App.lean | 4 +- src/Lean/Elab/BuiltinCommand.lean | 2 +- src/Lean/Elab/BuiltinNotation.lean | 2 +- src/Lean/Elab/Command.lean | 3 +- src/Lean/Elab/DeclNameGen.lean | 2 +- src/Lean/Elab/Deriving/BEq.lean | 10 +- src/Lean/Elab/Deriving/DecEq.lean | 8 +- src/Lean/Elab/Deriving/FromToJson.lean | 12 +- src/Lean/Elab/Deriving/Hashable.lean | 8 +- src/Lean/Elab/Deriving/Inhabited.lean | 8 +- src/Lean/Elab/Deriving/Ord.lean | 8 +- src/Lean/Elab/Deriving/Repr.lean | 8 +- src/Lean/Elab/Deriving/ToExpr.lean | 8 +- src/Lean/Elab/Deriving/Util.lean | 8 +- src/Lean/Elab/Inductive.lean | 2 +- src/Lean/Elab/LetRec.lean | 2 +- src/Lean/Elab/Match.lean | 12 +- src/Lean/Elab/MutualDef.lean | 6 +- src/Lean/Elab/MutualInductive.lean | 12 +- src/Lean/Elab/PatternVar.lean | 5 +- src/Lean/Elab/PreDefinition/Basic.lean | 4 +- src/Lean/Elab/PreDefinition/Eqns.lean | 6 +- src/Lean/Elab/PreDefinition/FixedParams.lean | 34 +-- .../Elab/PreDefinition/Structural/Basic.lean | 2 +- .../Elab/PreDefinition/Structural/Eqns.lean | 2 +- .../PreDefinition/Structural/FindRecArg.lean | 4 +- .../PreDefinition/Structural/RecArgInfo.lean | 2 +- src/Lean/Elab/PreDefinition/WF/GuessLex.lean | 28 +- src/Lean/Elab/PreDefinition/WF/Rel.lean | 4 +- src/Lean/Elab/Quotation.lean | 2 +- src/Lean/Elab/StructInst.lean | 2 +- src/Lean/Elab/Structure.lean | 4 +- src/Lean/Elab/SyntheticMVars.lean | 4 +- .../BVDecide/Frontend/Normalize/AC.lean | 2 +- .../Frontend/Normalize/Structures.lean | 2 +- .../Frontend/Normalize/TypeAnalysis.lean | 8 +- src/Lean/Elab/Tactic/BVDecide/LRAT/Trim.lean | 2 +- src/Lean/Elab/Tactic/BuiltinTactic.lean | 2 +- src/Lean/Elab/Tactic/Conv/Basic.lean | 2 +- src/Lean/Elab/Tactic/Conv/Congr.lean | 8 +- src/Lean/Elab/Tactic/Do/ProofMode/MGoal.lean | 2 +- src/Lean/Elab/Tactic/ElabTerm.lean | 2 +- src/Lean/Elab/Tactic/Induction.lean | 4 +- src/Lean/Elab/Tactic/Lets.lean | 2 +- src/Lean/Elab/Tactic/Monotonicity.lean | 2 +- src/Lean/Elab/Tactic/Omega/Core.lean | 4 +- src/Lean/Elab/Tactic/Omega/Frontend.lean | 2 +- src/Lean/Elab/Tactic/Rewrite.lean | 2 +- src/Lean/Elab/Tactic/Simp.lean | 2 +- src/Lean/Elab/Tactic/Try.lean | 4 +- src/Lean/Environment.lean | 6 +- src/Lean/Linter/UnusedSimpArgs.lean | 4 +- src/Lean/Meta/ACLt.lean | 8 +- src/Lean/Meta/ArgsPacker.lean | 4 +- src/Lean/Meta/Basic.lean | 4 +- src/Lean/Meta/Canonicalizer.lean | 2 +- src/Lean/Meta/Check.lean | 2 +- src/Lean/Meta/CongrTheorems.lean | 10 +- src/Lean/Meta/Constructions/BRecOn.lean | 7 +- src/Lean/Meta/Constructions/NoConfusion.lean | 2 +- src/Lean/Meta/DiscrTree.lean | 2 +- src/Lean/Meta/ExprDefEq.lean | 10 +- src/Lean/Meta/ForEachExpr.lean | 2 +- src/Lean/Meta/FunInfo.lean | 4 +- src/Lean/Meta/Hint.lean | 2 +- src/Lean/Meta/IndPredBelow.lean | 3 +- src/Lean/Meta/InferType.lean | 4 +- src/Lean/Meta/Instances.lean | 7 +- src/Lean/Meta/LetToHave.lean | 2 +- src/Lean/Meta/Match/MatchEqs.lean | 12 +- src/Lean/Meta/Match/MatcherApp/Transform.lean | 4 +- src/Lean/Meta/Match/MatcherInfo.lean | 8 +- src/Lean/Meta/PProdN.lean | 4 +- src/Lean/Meta/RecursorInfo.lean | 6 +- src/Lean/Meta/Reduce.lean | 2 +- src/Lean/Meta/SizeOf.lean | 2 +- src/Lean/Meta/Structure.lean | 4 +- src/Lean/Meta/SynthInstance.lean | 2 +- src/Lean/Meta/Tactic/Apply.lean | 14 +- src/Lean/Meta/Tactic/Assert.lean | 2 +- src/Lean/Meta/Tactic/ElimInfo.lean | 6 +- src/Lean/Meta/Tactic/FunInd.lean | 14 +- .../Tactic/Grind/Arith/CommRing/EqCnstr.lean | 2 +- .../Meta/Tactic/Grind/Arith/CommRing/Inv.lean | 2 +- .../Tactic/Grind/Arith/CommRing/Proof.lean | 4 +- .../Meta/Tactic/Grind/Arith/Linear/Inv.lean | 2 +- .../Tactic/Grind/Arith/Linear/Search.lean | 2 +- .../Meta/Tactic/Grind/Arith/Offset/Main.lean | 4 +- .../Meta/Tactic/Grind/Arith/Offset/Model.lean | 8 +- src/Lean/Meta/Tactic/Grind/Canon.lean | 2 +- src/Lean/Meta/Tactic/Grind/Cases.lean | 2 +- src/Lean/Meta/Tactic/Grind/EMatch.lean | 2 +- src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean | 6 +- src/Lean/Meta/Tactic/Grind/Internalize.lean | 4 +- src/Lean/Meta/Tactic/Grind/Inv.lean | 4 +- .../Meta/Tactic/Grind/MarkNestedProofs.lean | 2 +- src/Lean/Meta/Tactic/Grind/MatchCond.lean | 4 +- src/Lean/Meta/Tactic/Injection.lean | 2 +- src/Lean/Meta/Tactic/Lets.lean | 2 +- src/Lean/Meta/Tactic/LibrarySearch.lean | 4 +- src/Lean/Meta/Tactic/NormCast.lean | 2 +- src/Lean/Meta/Tactic/Simp/Main.lean | 2 +- src/Lean/Meta/Tactic/Simp/Rewrite.lean | 6 +- src/Lean/Meta/Tactic/Simp/SimpAll.lean | 2 +- src/Lean/Meta/Tactic/Simp/SimpTheorems.lean | 2 +- src/Lean/Meta/Tactic/Simp/Simproc.lean | 4 +- src/Lean/Meta/Tactic/Simp/Types.lean | 2 +- src/Lean/Meta/Tactic/Split.lean | 2 +- src/Lean/Meta/Tactic/SplitIf.lean | 4 +- src/Lean/Meta/Tactic/TryThis.lean | 2 +- src/Lean/Meta/WHNF.lean | 2 +- src/Lean/ParserCompiler.lean | 2 +- .../PrettyPrinter/Delaborator/Builtins.lean | 4 +- .../Delaborator/FieldNotation.lean | 2 +- .../Delaborator/TopDownAnalyze.lean | 18 +- src/Lean/Server/CodeActions/Provider.lean | 8 +- src/Lean/Server/FileWorker/ExampleHover.lean | 2 +- src/Lean/Server/FileWorker/SignatureHelp.lean | 2 +- src/Lean/Server/References.lean | 2 +- src/Lean/Structure.lean | 4 +- src/Lean/Syntax.lean | 2 +- src/Lean/Util/Diff.lean | 8 +- src/Lean/Util/Profiler.lean | 2 +- src/Lean/Widget/Diff.lean | 2 +- src/Std/Time/Zoned/Database/Basic.lean | 4 +- src/Std/Time/Zoned/Database/TzIf.lean | 7 +- tests/bench/binarytrees.st.lean | 5 +- tests/bench/channel.lean | 20 +- tests/bench/identifier_completion_runner.lean | 2 +- tests/bench/ilean_roundtrip.lean | 2 +- tests/bench/inundation/lakefile.lean | 8 +- tests/bench/liasolver.lean | 6 +- tests/bench/nat_repr.lean | 4 +- tests/bench/parser.lean | 2 +- tests/bench/reduceMatch.lean | 2 +- tests/bench/simp_arith1.lean | 4 +- tests/bench/speedcenter.exec.velcom.yaml | 6 + tests/bench/workspaceSymbolsNewRanges.lean | 244 ++++++++++++++++++ tests/lean/run/1420.lean | 2 +- tests/lean/run/2137.lean | 2 +- tests/lean/run/646.lean | 4 +- tests/lean/run/bv_popcount.lean | 2 +- tests/lean/run/forInRangeWF.lean | 2 +- tests/lean/run/forIn_phashset.lean | 2 +- tests/lean/run/forOutParamIssue.lean | 4 +- tests/lean/run/lcnfInferProjTypeIssue.lean | 4 +- tests/lean/run/letToHaveCleanup.lean | 4 +- tests/lean/run/sarray.lean | 4 +- tests/lean/run/structure_recursive.lean | 4 +- tests/lean/run/sync_barrier.lean | 4 +- tests/lean/run/sync_channel.lean | 2 +- tests/lean/run/sync_mutex.lean | 4 +- tests/lean/run/sync_recursive_mutex.lean | 2 +- tests/lean/run/sync_shared_mutex.lean | 2 +- tests/lean/run/tempfile.lean | 8 +- tests/lean/run/timeLocalDateTime.lean | 2 +- 190 files changed, 1069 insertions(+), 556 deletions(-) create mode 100644 tests/bench/workspaceSymbolsNewRanges.lean diff --git a/src/Init/Data/Array/Lex/Basic.lean b/src/Init/Data/Array/Lex/Basic.lean index 7277a44b5a..5661bf4917 100644 --- a/src/Init/Data/Array/Lex/Basic.lean +++ b/src/Init/Data/Array/Lex/Basic.lean @@ -6,9 +6,12 @@ Author: Kim Morrison module prelude -public import Init.Data.Array.Basic -public import Init.Data.Nat.Lemmas -public import Init.Data.Range +public import Init.Core +import Init.Data.Array.Basic +import Init.Data.Nat.Lemmas +import Init.Data.Range.Polymorphic.Iterators +import Init.Data.Range.Polymorphic.Nat +import Init.Data.Iterators.Consumers public section @@ -26,9 +29,9 @@ Specifically, `Array.lex as bs lt` is true if * there is an index `i` such that `lt as[i] bs[i]`, and for all `j < i`, `as[j] == bs[j]`. -/ def lex [BEq α] (as bs : Array α) (lt : α → α → Bool := by exact (· < ·)) : Bool := Id.run do - for h : i in [0 : min as.size bs.size] do - -- TODO: `omega` should be able to find this itself. - have : i < min as.size bs.size := Membership.get_elem_helper h rfl + for h : i in 0...(min as.size bs.size) do + -- TODO: `get_elem_tactic` should be able to find this itself. + have : i < min as.size bs.size := Std.PRange.lt_upper_of_mem h if lt as[i] bs[i] then return true else if as[i] != bs[i] then diff --git a/src/Init/Data/Array/Lex/Lemmas.lean b/src/Init/Data/Array/Lex/Lemmas.lean index f6610c0644..853231c894 100644 --- a/src/Init/Data/Array/Lex/Lemmas.lean +++ b/src/Init/Data/Array/Lex/Lemmas.lean @@ -6,9 +6,12 @@ Author: Kim Morrison module prelude -public import all Init.Data.Array.Lex.Basic +import all Init.Data.Array.Lex.Basic +public import Init.Data.Array.Lex.Basic public import Init.Data.Array.Lemmas public import Init.Data.List.Lex +import Init.Data.Range.Polymorphic.Lemmas +import Init.Data.Range.Polymorphic.NatLemmas public section @@ -36,16 +39,38 @@ protected theorem not_le_iff_gt [LT α] {xs ys : Array α} : Classical.not_not @[simp] theorem lex_empty [BEq α] {lt : α → α → Bool} {xs : Array α} : xs.lex #[] lt = false := by - simp [lex] + rw [lex, Std.PRange.forIn'_eq_match] + simp [Std.PRange.SupportsUpperBound.IsSatisfied] + +private theorem cons_lex_cons.forIn'_congr_aux [Monad m] {as bs : ρ} {_ : Membership α ρ} + [ForIn' m ρ α inferInstance] (w : as = bs) + {b b' : β} (hb : b = b') + {f : (a' : α) → a' ∈ as → β → m (ForInStep β)} + {g : (a' : α) → a' ∈ bs → β → m (ForInStep β)} + (h : ∀ a m b, f a (by simpa [w] using m) b = g a m b) : + forIn' as b f = forIn' bs b' g := by + cases hb + cases w + have : f = g := by + ext a ha acc + apply h + cases this + rfl private theorem cons_lex_cons [BEq α] {lt : α → α → Bool} {a b : α} {xs ys : Array α} : (#[a] ++ xs).lex (#[b] ++ ys) lt = (lt a b || a == b && xs.lex ys lt) := by - simp only [lex] - simp only [Std.Range.forIn'_eq_forIn'_range', size_append, List.size_toArray, List.length_singleton, - Nat.add_comm 1] - simp [Nat.add_min_add_right, List.range'_succ, getElem_append_left, List.range'_succ_left, - getElem_append_right] + simp only [lex, size_append, List.size_toArray, List.length_cons, List.length_nil, Nat.zero_add, + Nat.add_min_add_left, Nat.add_lt_add_iff_left, Std.PRange.forIn'_eq_forIn'_toList] + conv => + lhs; congr; congr + rw [cons_lex_cons.forIn'_congr_aux Std.PRange.toList_eq_match rfl (fun _ _ _ => rfl)] + simp only [Std.PRange.SupportsUpperBound.IsSatisfied, bind_pure_comp, map_pure] + rw [cons_lex_cons.forIn'_congr_aux (if_pos (by omega)) rfl (fun _ _ _ => rfl)] + simp only [Std.PRange.toList_open_eq_toList_closed_of_isSome_succ? (lo := 0) (h := rfl), + Std.PRange.UpwardEnumerable.succ?, Nat.add_comm 1, Std.PRange.Nat.ClosedOpen.toList_succ_succ, + Option.get_some, List.forIn'_cons, List.size_toArray, List.length_cons, List.length_nil, + Nat.lt_add_one, getElem_append_left, List.getElem_toArray, List.getElem_cons_zero] cases lt a b · rw [bne] cases a == b <;> simp @@ -54,10 +79,17 @@ private theorem cons_lex_cons [BEq α] {lt : α → α → Bool} {a b : α} {xs @[simp, grind =] theorem _root_.List.lex_toArray [BEq α] {lt : α → α → Bool} {l₁ l₂ : List α} : l₁.toArray.lex l₂.toArray lt = l₁.lex l₂ lt := by induction l₁ generalizing l₂ with - | nil => cases l₂ <;> simp [lex] + | nil => + cases l₂ + · rw [lex, Std.PRange.forIn'_eq_match] + simp [Std.PRange.SupportsUpperBound.IsSatisfied] + · rw [lex, Std.PRange.forIn'_eq_match] + simp [Std.PRange.SupportsUpperBound.IsSatisfied] | cons x l₁ ih => cases l₂ with - | nil => simp [lex] + | nil => + rw [lex, Std.PRange.forIn'_eq_match] + simp [Std.PRange.SupportsUpperBound.IsSatisfied] | cons y l₂ => rw [List.toArray_cons, List.toArray_cons y, cons_lex_cons, List.lex, ih] diff --git a/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean b/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean index 48bcbecd91..b7a8bddc0c 100644 --- a/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean +++ b/src/Init/Data/Iterators/Consumers/Monadic/Loop.lean @@ -9,6 +9,7 @@ prelude public import Init.RCases public import Init.Data.Iterators.Basic public import Init.Data.Iterators.Consumers.Monadic.Partial +public import Init.Data.Iterators.Internal.LawfulMonadLiftFunction public section @@ -32,6 +33,8 @@ asserts that an `IteratorLoop` instance equals the default implementation. namespace Std.Iterators +open Std.Internal + section Typeclasses /-- @@ -39,6 +42,7 @@ Relation that needs to be well-formed in order for a loop over an iterator to te It is assumed that the `plausible_forInStep` predicate relates the input and output of the stepper function. -/ +@[expose] def IteratorLoop.rel (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] {γ : Type x} (plausible_forInStep : β → γ → ForInStep γ → Prop) (p' p : IterM (α := α) m β × γ) : Prop := @@ -48,6 +52,7 @@ def IteratorLoop.rel (α : Type w) (m : Type w → Type w') {β : Type w} [Itera /-- Asserts that `IteratorLoop.rel` is well-founded. -/ +@[expose] def IteratorLoop.WellFounded (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] {γ : Type x} (plausible_forInStep : β → γ → ForInStep γ → Prop) : Prop := _root_.WellFounded (IteratorLoop.rel α m plausible_forInStep) @@ -61,6 +66,7 @@ This class is experimental and users of the iterator API should not explicitly d They can, however, assume that consumers that require an instance will work for all iterators provided by the standard library. -/ +@[ext] class IteratorLoop (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] (n : Type x → Type x') where forIn : ∀ (_liftBind : (γ : Type w) → (δ : Type x) → (γ → n δ) → m γ → n δ) (γ : Type x), @@ -108,29 +114,24 @@ class IteratorSizePartial (α : Type w) (m : Type w → Type w') {β : Type w} [ end Typeclasses /-- Internal implementation detail of the iterator library. -/ -def IteratorLoop.WFRel {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] - {γ : Type x} {plausible_forInStep : β → γ → ForInStep γ → Prop} - (_wf : WellFounded α m plausible_forInStep) := - IterM (α := α) m β × γ +structure IteratorLoop.WithWF (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] + {γ : Type x} (PlausibleForInStep : β → γ → ForInStep γ → Prop) + (hwf : IteratorLoop.WellFounded α m PlausibleForInStep) where + it : IterM (α := α) m β + acc : γ -/-- Internal implementation detail of the iterator library. -/ -def IteratorLoop.WFRel.mk {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] - {γ : Type x} {plausible_forInStep : β → γ → ForInStep γ → Prop} - (wf : WellFounded α m plausible_forInStep) (it : IterM (α := α) m β) (c : γ) : - IteratorLoop.WFRel wf := - (it, c) - -private instance {α : Type w} {m : Type w → Type w'} {β : Type w} [Iterator α m β] - {γ : Type x} {plausible_forInStep : β → γ → ForInStep γ → Prop} - (wf : IteratorLoop.WellFounded α m plausible_forInStep) : - WellFoundedRelation (IteratorLoop.WFRel wf) where - rel := IteratorLoop.rel α m plausible_forInStep - wf := wf +instance IteratorLoop.WithWF.instWellFoundedRelation + (α : Type w) (m : Type w → Type w') {β : Type w} [Iterator α m β] + {γ : Type x} (PlausibleForInStep : β → γ → ForInStep γ → Prop) + (hwf : IteratorLoop.WellFounded α m PlausibleForInStep) : + WellFoundedRelation (WithWF α m PlausibleForInStep hwf) where + rel := InvImage (IteratorLoop.rel α m PlausibleForInStep) (fun x => (x.it, x.acc)) + wf := by exact InvImage.wf _ hwf /-- This is the loop implementation of the default instance `IteratorLoop.defaultImplementation`. -/ -@[specialize] +@[specialize, expose] def IterM.DefaultConsumers.forIn' {m : Type w → Type w'} {α : Type w} {β : Type w} [Iterator α m β] {n : Type x → Type x'} [Monad n] @@ -142,27 +143,59 @@ def IterM.DefaultConsumers.forIn' {m : Type w → Type w'} {α : Type w} {β : T (f : (b : β) → P b → (c : γ) → n (Subtype (plausible_forInStep b c))) : n γ := haveI : WellFounded _ := wf (lift _ _ · it.step) fun - | .yield it' out h => do - match ← f out (hP _ <| .direct ⟨_, h⟩) init with - | ⟨.yield c, _⟩ => - IterM.DefaultConsumers.forIn' lift _ plausible_forInStep wf it' c P - (fun _ h' => hP _ <| .indirect ⟨_, rfl, h⟩ h') f - | ⟨.done c, _⟩ => return c - | .skip it' h => - IterM.DefaultConsumers.forIn' lift _ plausible_forInStep wf it' init P - (fun _ h' => hP _ <| .indirect ⟨_, rfl, h⟩ h') f - | .done _ => return init -termination_by IteratorLoop.WFRel.mk wf it init + | .yield it' out h => do + match ← f out (hP _ <| .direct ⟨_, h⟩) init with + | ⟨.yield c, _⟩ => + IterM.DefaultConsumers.forIn' lift _ plausible_forInStep wf it' c P + (fun _ h' => hP _ <| .indirect ⟨_, rfl, h⟩ h') f + | ⟨.done c, _⟩ => return c + | .skip it' h => + IterM.DefaultConsumers.forIn' lift _ plausible_forInStep wf it' init P + (fun _ h' => hP _ <| .indirect ⟨_, rfl, h⟩ h') f + | .done _ => return init +termination_by IteratorLoop.WithWF.mk it init (hwf := wf) decreasing_by · exact Or.inl ⟨out, ‹_›, ‹_›⟩ · exact Or.inr ⟨‹_›, rfl⟩ +theorem IterM.DefaultConsumers.forIn'_eq_forIn' {m : Type w → Type w'} {α : Type w} {β : Type w} + [Iterator α m β] + {n : Type x → Type x'} [Monad n] + {lift : ∀ γ δ, (γ → n δ) → m γ → n δ} {γ : Type x} + {Pl : β → γ → ForInStep γ → Prop} + {wf : IteratorLoop.WellFounded α m Pl} + {it : IterM (α := α) m β} {init : γ} + {P : β → Prop} {hP : ∀ b, it.IsPlausibleIndirectOutput b → P b} + {Q : β → Prop} {hQ : ∀ b, it.IsPlausibleIndirectOutput b → Q b} + {f : (b : β) → P b → (c : γ) → n (Subtype (Pl b c))} + {g : (b : β) → Q b → (c : γ) → n (Subtype (Pl b c))} + (hfg : ∀ b c, (hPb : P b) → (hQb : Q b) → f b hPb c = g b hQb c) : + IterM.DefaultConsumers.forIn' lift γ Pl wf it init P hP f = + IterM.DefaultConsumers.forIn' lift γ Pl wf it init Q hQ g := by + rw [forIn', forIn'] + congr; ext step + split + · congr + · apply hfg + · ext + split + · apply IterM.DefaultConsumers.forIn'_eq_forIn' + assumption + · rfl + · apply IterM.DefaultConsumers.forIn'_eq_forIn' + assumption + · rfl +termination_by IteratorLoop.WithWF.mk it init (hwf := wf) +decreasing_by + · exact Or.inl ⟨_, ‹_›, ‹_›⟩ + · exact Or.inr ⟨‹_›, rfl⟩ + /-- This is the default implementation of the `IteratorLoop` class. It simply iterates through the iterator using `IterM.step`. For certain iterators, more efficient implementations are possible and should be used instead. -/ -@[always_inline, inline] +@[always_inline, inline, expose] def IteratorLoop.defaultImplementation {α : Type w} {m : Type w → Type w'} {n : Type x → Type x'} [Monad n] [Iterator α m β] : IteratorLoop α m n where @@ -173,8 +206,9 @@ Asserts that a given `IteratorLoop` instance is equal to `IteratorLoop.defaultIm (Even though equal, the given instance might be vastly more efficient.) -/ class LawfulIteratorLoop (α : Type w) (m : Type w → Type w') (n : Type x → Type x') - [Monad n] [Iterator α m β] [Finite α m] [i : IteratorLoop α m n] where - lawful : i = .defaultImplementation + [Monad m] [Monad n] [Iterator α m β] [i : IteratorLoop α m n] where + lawful : ∀ lift [LawfulMonadLiftBindFunction lift], i.forIn lift = + IteratorLoop.defaultImplementation.forIn lift /-- This is the loop implementation of the default instance `IteratorLoopPartial.defaultImplementation`. @@ -214,7 +248,7 @@ instance (α : Type w) (m : Type w → Type w') (n : Type x → Type x') letI : IteratorLoop α m n := .defaultImplementation LawfulIteratorLoop α m n := letI : IteratorLoop α m n := .defaultImplementation - ⟨rfl⟩ + ⟨fun _ => rfl⟩ theorem IteratorLoop.wellFounded_of_finite {m : Type w → Type w'} {α β : Type w} {γ : Type x} [Iterator α m β] [Finite α m] : diff --git a/src/Init/Data/Iterators/Internal/LawfulMonadLiftFunction.lean b/src/Init/Data/Iterators/Internal/LawfulMonadLiftFunction.lean index e03702fe03..2020ddb15f 100644 --- a/src/Init/Data/Iterators/Internal/LawfulMonadLiftFunction.lean +++ b/src/Init/Data/Iterators/Internal/LawfulMonadLiftFunction.lean @@ -24,6 +24,12 @@ the requirement that the `MonadLift(T)` instance induced by `f` admits a namespace Std.Internal +class LawfulMonadLiftBindFunction {m : Type u → Type v} {n : Type w → Type x} [Monad m] + [Monad n] (liftBind : ∀ γ δ, (γ → n δ) → m γ → n δ) where + liftBind_pure {γ δ} (f : γ → n δ) (a : γ) : liftBind γ δ f (pure a) = f a + liftBind_bind {β γ δ} (f : γ → n δ) (x : m β) (g : β → m γ) : + liftBind γ δ f (x >>= g) = liftBind β δ (fun b => liftBind γ δ f (g b)) x + class LawfulMonadLiftFunction {m : Type u → Type v} {n : Type u → Type w} [Monad m] [Monad n] (lift : ⦃α : Type u⦄ → m α → n α) where lift_pure {α : Type u} (a : α) : lift (pure a) = pure a @@ -79,4 +85,35 @@ instance [LawfulMonadLiftFunction lift] : { monadLift_pure := LawfulMonadLiftFunction.lift_pure monadLift_bind := LawfulMonadLiftFunction.lift_bind } +section LiftBind + +variable {liftBind : ∀ γ δ, (γ → m δ) → m γ → m δ} + +instance [LawfulMonadLiftBindFunction (n := n) (fun _ _ f x => lift x >>= f)] [LawfulMonad n] : + LawfulMonadLiftFunction lift where + lift_pure {γ} a := by + simpa using LawfulMonadLiftBindFunction.liftBind_pure (n := n) + (liftBind := fun _ _ f x => lift x >>= f) (γ := γ) (δ := γ) pure a + lift_bind {β γ} x g := by + simpa using LawfulMonadLiftBindFunction.liftBind_bind (n := n) + (liftBind := fun _ _ f x => lift x >>= f) (β := β) (γ := γ) (δ := γ) pure x g + +def LawfulMonadLiftBindFunction.id [Monad m] [LawfulMonad m] : + LawfulMonadLiftBindFunction (m := Id) (n := m) (fun _ _ f x => f x.run) where + liftBind_pure := by simp + liftBind_bind := by simp + +instance {m : Type u → Type v} [Monad m] {n : Type u → Type w} [Monad n] [MonadLiftT m n] + [LawfulMonadLiftT m n] [LawfulMonad n] : + LawfulMonadLiftBindFunction (fun γ δ (f : γ → n δ) (x : m γ) => monadLift x >>= f) where + liftBind_pure := by simp + liftBind_bind := by simp + +instance {n : Type u → Type w} [Monad n] [LawfulMonad n] : + LawfulMonadLiftBindFunction (fun γ δ (f : γ → n δ) (x : Id γ) => f x.run) where + liftBind_pure := by simp + liftBind_bind := by simp + +end LiftBind + end Std.Internal diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean index 77d2b49b2b..81b9699dc1 100644 --- a/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean +++ b/src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean @@ -6,6 +6,7 @@ Authors: Paul Reichert module prelude +public import Init.Control.Lawful.MonadLift.Instances public import Init.Data.Iterators.Lemmas.Consumers.Collect public import all Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop public import all Init.Data.Iterators.Consumers.Loop @@ -16,7 +17,7 @@ public section namespace Std.Iterators theorem Iter.forIn'_eq {α β : Type w} [Iterator α Id β] [Finite α Id] - {m : Type x → Type x'} [Monad m] [IteratorLoop α Id m] [hl : LawfulIteratorLoop α Id m] + {m : Type x → Type x'} [Monad m] [LawfulMonad m] [IteratorLoop α Id m] [hl : LawfulIteratorLoop α Id m] {γ : Type x} {it : Iter (α := α) β} {init : γ} {f : (b : β) → it.IsPlausibleIndirectOutput b → γ → m (ForInStep γ)} : letI : ForIn' m (Iter (α := α) β) β _ := Iter.instForIn' @@ -25,21 +26,22 @@ theorem Iter.forIn'_eq {α β : Type w} [Iterator α Id β] [Finite α Id] IteratorLoop.wellFounded_of_finite it.toIterM init _ (fun _ => id) (fun out h acc => (⟨·, .intro⟩) <$> f out (Iter.isPlausibleIndirectOutput_iff_isPlausibleIndirectOutput_toIterM.mpr h) acc) := by - cases hl.lawful; rfl + simp [instForIn', ForIn'.forIn', IteratorLoop.finiteForIn', hl.lawful (fun γ δ f x => f x.run), + IteratorLoop.defaultImplementation] theorem Iter.forIn_eq {α β : Type w} [Iterator α Id β] [Finite α Id] - {m : Type x → Type x'} [Monad m] [IteratorLoop α Id m] [hl : LawfulIteratorLoop α Id m] - {γ : Type x} {it : Iter (α := α) β} {init : γ} + {m : Type x → Type x'} [Monad m] [LawfulMonad m] [IteratorLoop α Id m] + [hl : LawfulIteratorLoop α Id m] {γ : Type x} {it : Iter (α := α) β} {init : γ} {f : (b : β) → γ → m (ForInStep γ)} : ForIn.forIn it init f = IterM.DefaultConsumers.forIn' (fun _ _ f c => f c.run) γ (fun _ _ _ => True) IteratorLoop.wellFounded_of_finite it.toIterM init _ (fun _ => id) (fun out _ acc => (⟨·, .intro⟩) <$> f out acc) := by - cases hl.lawful; rfl + simp [ForIn.forIn, forIn'_eq, -forIn'_eq_forIn] theorem Iter.forIn'_eq_forIn'_toIterM {α β : Type w} [Iterator α Id β] - [Finite α Id] {m : Type w → Type w'} [Monad m] [LawfulMonad m] + [Finite α Id] {m : Type w → Type w''} [Monad m] [LawfulMonad m] [IteratorLoop α Id m] [LawfulIteratorLoop α Id m] {γ : Type w} {it : Iter (α := α) β} {init : γ} {f : (out : β) → _ → γ → m (ForInStep γ)} : diff --git a/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean index 07f55394f7..9a31db0671 100644 --- a/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean +++ b/src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean @@ -38,60 +38,31 @@ theorem IterM.DefaultConsumers.forIn'_eq_match_step {α β : Type w} {m : Type w cases step using PlausibleIterStep.casesOn <;> rfl theorem IterM.forIn'_eq {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] - {n : Type w → Type w''} [Monad n] [IteratorLoop α m n] [hl : LawfulIteratorLoop α m n] - [MonadLiftT m n] {γ : Type w} {it : IterM (α := α) m β} {init : γ} + {n : Type w → Type w''} [Monad m] [Monad n] [LawfulMonad n] [IteratorLoop α m n] + [hl : LawfulIteratorLoop α m n] + [MonadLiftT m n] [LawfulMonadLiftT m n] {γ : Type w} {it : IterM (α := α) m β} {init : γ} {f : (b : β) → it.IsPlausibleIndirectOutput b → γ → n (ForInStep γ)} : letI : ForIn' n (IterM (α := α) m β) β _ := IterM.instForIn' ForIn'.forIn' it init f = IterM.DefaultConsumers.forIn' (n := n) (fun _ _ f x => monadLift x >>= f) γ (fun _ _ _ => True) IteratorLoop.wellFounded_of_finite it init _ (fun _ => id) ((⟨·, .intro⟩) <$> f · · ·) := by - cases hl.lawful; rfl + simp [instForIn', ForIn'.forIn', IteratorLoop.finiteForIn', + hl.lawful (fun _ _ f x => monadLift x >>= f), IteratorLoop.defaultImplementation] theorem IterM.forIn_eq {α β : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] - {n : Type w → Type w''} [Monad n] [IteratorLoop α m n] [hl : LawfulIteratorLoop α m n] - [MonadLiftT m n] {γ : Type w} {it : IterM (α := α) m β} {init : γ} + {n : Type w → Type w''} [Monad m] [Monad n] [LawfulMonad n] [IteratorLoop α m n] + [hl : LawfulIteratorLoop α m n] + [MonadLiftT m n] [LawfulMonadLiftT m n] {γ : Type w} {it : IterM (α := α) m β} {init : γ} {f : β → γ → n (ForInStep γ)} : ForIn.forIn it init f = IterM.DefaultConsumers.forIn' (n := n) (fun _ _ f x => monadLift x >>= f) γ (fun _ _ _ => True) IteratorLoop.wellFounded_of_finite it init _ (fun _ => id) (fun out _ acc => (⟨·, .intro⟩) <$> f out acc) := by - cases hl.lawful; rfl - -theorem IterM.DefaultConsumers.forIn'_eq_forIn' {m : Type w → Type w'} {α : Type w} {β : Type w} - [Iterator α m β] - {n : Type x → Type x'} [Monad n] - {liftBind : ∀ γ δ, (γ → n δ) → m γ → n δ} {γ : Type x} - {Pl : β → γ → ForInStep γ → Prop} - {wf : IteratorLoop.WellFounded α m Pl} - {it : IterM (α := α) m β} {init : γ} - {P : β → Prop} {hP : ∀ b, it.IsPlausibleIndirectOutput b → P b} - {Q : β → Prop} {hQ : ∀ b, it.IsPlausibleIndirectOutput b → Q b} - {f : (b : β) → P b → (c : γ) → n (Subtype (Pl b c))} - {g : (b : β) → Q b → (c : γ) → n (Subtype (Pl b c))} - (hfg : ∀ b c, (hPb : P b) → (hQb : Q b) → f b hPb c = g b hQb c) : - IterM.DefaultConsumers.forIn' liftBind γ Pl wf it init P hP f = - IterM.DefaultConsumers.forIn' liftBind γ Pl wf it init Q hQ g := by - rw [forIn', forIn'] - congr; ext step - split - · congr - · apply hfg - · ext - split - · apply IterM.DefaultConsumers.forIn'_eq_forIn' - assumption - · rfl - · apply IterM.DefaultConsumers.forIn'_eq_forIn' - assumption - · rfl -termination_by IteratorLoop.WFRel.mk wf it init -decreasing_by - · exact Or.inl ⟨_, ‹_›, ‹_›⟩ - · exact Or.inr ⟨‹_›, rfl⟩ + simp only [ForIn.forIn, forIn'_eq] theorem IterM.forIn'_eq_match_step {α β : Type w} {m : Type w → Type w'} [Iterator α m β] - [Finite α m] {n : Type w → Type w''} [Monad n] [LawfulMonad n] + [Finite α m] {n : Type w → Type w''} [Monad m] [Monad n] [LawfulMonad n] [IteratorLoop α m n] [LawfulIteratorLoop α m n] - [MonadLiftT m n] {γ : Type w} {it : IterM (α := α) m β} {init : γ} + [MonadLiftT m n] [LawfulMonadLiftT m n] {γ : Type w} {it : IterM (α := α) m β} {init : γ} {f : (out : β) → _ → γ → n (ForInStep γ)} : letI : ForIn' n (IterM (α := α) m β) β _ := IterM.instForIn' ForIn'.forIn' it init f = (do @@ -124,9 +95,9 @@ theorem IterM.forIn'_eq_match_step {α β : Type w} {m : Type w → Type w'} [It · simp theorem IterM.forIn_eq_match_step {α β : Type w} {m : Type w → Type w'} [Iterator α m β] - [Finite α m] {n : Type w → Type w''} [Monad n] [LawfulMonad n] + [Finite α m] {n : Type w → Type w''} [Monad m] [Monad n] [LawfulMonad n] [IteratorLoop α m n] [LawfulIteratorLoop α m n] - [MonadLiftT m n] {γ : Type w} {it : IterM (α := α) m β} {init : γ} + [MonadLiftT m n] [LawfulMonadLiftT m n] {γ : Type w} {it : IterM (α := α) m β} {init : γ} {f : β → γ → n (ForInStep γ)} : ForIn.forIn it init f = (do match ← it.step with @@ -140,7 +111,7 @@ theorem IterM.forIn_eq_match_step {α β : Type w} {m : Type w → Type w'} [Ite exact forIn'_eq_match_step theorem IterM.forM_eq_forIn {α β : Type w} {m : Type w → Type w'} [Iterator α m β] - [Finite α m] {n : Type w → Type w''} [Monad n] [LawfulMonad n] + [Finite α m] {n : Type w → Type w''} [Monad m] [Monad n] [LawfulMonad n] [IteratorLoop α m n] [LawfulIteratorLoop α m n] [MonadLiftT m n] {it : IterM (α := α) m β} {f : β → n PUnit} : @@ -148,9 +119,9 @@ theorem IterM.forM_eq_forIn {α β : Type w} {m : Type w → Type w'} [Iterator rfl theorem IterM.forM_eq_match_step {α β : Type w} {m : Type w → Type w'} [Iterator α m β] - [Finite α m] {n : Type w → Type w''} [Monad n] [LawfulMonad n] + [Finite α m] {n : Type w → Type w''} [Monad m] [Monad n] [LawfulMonad n] [IteratorLoop α m n] [LawfulIteratorLoop α m n] - [MonadLiftT m n] {it : IterM (α := α) m β} + [MonadLiftT m n] [LawfulMonadLiftT m n] {it : IterM (α := α) m β} {f : β → n PUnit} : ForM.forM it f = (do match ← it.step with @@ -171,7 +142,7 @@ theorem IterM.foldM_eq_forIn {α β γ : Type w} {m : Type w → Type w'} [Itera (rfl) theorem IterM.forIn_yield_eq_foldM {α β γ δ : Type w} {m : Type w → Type w'} [Iterator α m β] - [Finite α m] {n : Type w → Type w''} [Monad n] [LawfulMonad n] [IteratorLoop α m n] + [Finite α m] {n : Type w → Type w''} [Monad m] [Monad n] [LawfulMonad n] [IteratorLoop α m n] [LawfulIteratorLoop α m n] [MonadLiftT m n] {f : β → γ → n δ} {g : β → γ → δ → γ} {init : γ} {it : IterM (α := α) m β} : ForIn.forIn it init (fun c b => (fun d => .yield (g c b d)) <$> f c b) = @@ -179,8 +150,9 @@ theorem IterM.forIn_yield_eq_foldM {α β γ δ : Type w} {m : Type w → Type w simp [IterM.foldM_eq_forIn] theorem IterM.foldM_eq_match_step {α β γ : Type w} {m : Type w → Type w'} [Iterator α m β] [Finite α m] - {n : Type w → Type w''} [Monad n] [LawfulMonad n] [IteratorLoop α m n] [LawfulIteratorLoop α m n] - [MonadLiftT m n] {f : γ → β → n γ} {init : γ} {it : IterM (α := α) m β} : + {n : Type w → Type w''} [Monad m] [Monad n] [LawfulMonad n] [IteratorLoop α m n] + [LawfulIteratorLoop α m n] [MonadLiftT m n] [LawfulMonadLiftT m n] + {f : γ → β → n γ} {init : γ} {it : IterM (α := α) m β} : it.foldM (init := init) f = (do match ← it.step with | .yield it' out _ => it'.foldM (init := ← f init out) f diff --git a/src/Init/Data/Range/Polymorphic/Iterators.lean b/src/Init/Data/Range/Polymorphic/Iterators.lean index ad4ba7def1..4e041224d6 100644 --- a/src/Init/Data/Range/Polymorphic/Iterators.lean +++ b/src/Init/Data/Range/Polymorphic/Iterators.lean @@ -58,50 +58,6 @@ def size {sl su α} [UpwardEnumerable α] [BoundedUpwardEnumerable sl α] section Iterator -theorem RangeIterator.isPlausibleIndirectOutput_iff {su α} - [UpwardEnumerable α] [SupportsUpperBound su α] - [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableUpperBound su α] - {it : Iter (α := RangeIterator su α) α} {out : α} : - it.IsPlausibleIndirectOutput out ↔ - ∃ n, it.internalState.next.bind (UpwardEnumerable.succMany? n ·) = some out ∧ - SupportsUpperBound.IsSatisfied it.internalState.upperBound out := by - constructor - · intro h - induction h - case direct h => - rw [RangeIterator.isPlausibleOutput_iff] at h - refine ⟨0, by simp [h, LawfulUpwardEnumerable.succMany?_zero]⟩ - case indirect h _ ih => - rw [RangeIterator.isPlausibleSuccessorOf_iff] at h - obtain ⟨n, hn⟩ := ih - obtain ⟨a, ha, h₁, h₂, h₃⟩ := h - refine ⟨n + 1, ?_⟩ - simp [ha, ← h₃, hn.2, LawfulUpwardEnumerable.succMany?_succ_eq_succ?_bind_succMany?, h₂, hn] - · rintro ⟨n, hn, hu⟩ - induction n generalizing it - case zero => - apply Iter.IsPlausibleIndirectOutput.direct - rw [RangeIterator.isPlausibleOutput_iff] - exact ⟨by simpa [LawfulUpwardEnumerable.succMany?_zero] using hn, hu⟩ - case succ ih => - cases hn' : it.internalState.next - · simp [hn'] at hn - rename_i a - simp only [hn', Option.bind_some] at hn - have hle : UpwardEnumerable.LE a out := ⟨_, hn⟩ - rw [LawfulUpwardEnumerable.succMany?_succ_eq_succ?_bind_succMany?] at hn - cases hn' : UpwardEnumerable.succ? a - · simp only [hn', Option.bind_none, reduceCtorEq] at hn - rename_i a' - simp only [hn', Option.bind_some] at hn - specialize ih (it := ⟨some a', it.internalState.upperBound⟩) hn hu - refine Iter.IsPlausibleIndirectOutput.indirect ?_ ih - rw [RangeIterator.isPlausibleSuccessorOf_iff] - refine ⟨a, ‹_›, ?_, hn', rfl⟩ - apply LawfulUpwardEnumerableUpperBound.isSatisfied_of_le _ a out - · exact hu - · exact hle - theorem Internal.isPlausibleIndirectOutput_iter_iff {sl su α} [UpwardEnumerable α] [BoundedUpwardEnumerable sl α] [SupportsLowerBound sl α] [SupportsUpperBound su α] diff --git a/src/Init/Data/Range/Polymorphic/NatLemmas.lean b/src/Init/Data/Range/Polymorphic/NatLemmas.lean index b1bdfa5a1d..5894eb83d7 100644 --- a/src/Init/Data/Range/Polymorphic/NatLemmas.lean +++ b/src/Init/Data/Range/Polymorphic/NatLemmas.lean @@ -17,8 +17,8 @@ theorem succ_eq {n : Nat} : UpwardEnumerable.succ n = n + 1 := rfl theorem ClosedOpen.toList_succ_succ {m n : Nat} : - (PRange.mk (shape := ⟨.closed, .open⟩) (m+1) (n+1)).toList = - (PRange.mk (shape := ⟨.closed, .open⟩) m n).toList.map (· + 1) := by + ((m+1)...(n+1)).toList = + (m...n).toList.map (· + 1) := by simp only [← succ_eq] rw [Std.PRange.ClosedOpen.toList_succ_succ_eq_map] diff --git a/src/Init/Data/Range/Polymorphic/RangeIterator.lean b/src/Init/Data/Range/Polymorphic/RangeIterator.lean index 1cdb0d4b78..e10691d519 100644 --- a/src/Init/Data/Range/Polymorphic/RangeIterator.lean +++ b/src/Init/Data/Range/Polymorphic/RangeIterator.lean @@ -110,16 +110,6 @@ theorem RangeIterator.step_eq_step {su} [UpwardEnumerable α] [SupportsUpperBoun it.step = ⟨RangeIterator.step it, isPlausibleStep_iff.mpr rfl⟩ := by simp [Iter.step, step_eq_monadicStep, Monadic.step_eq_step, IterM.Step.toPure] -@[always_inline, inline] -instance RangeIterator.instIteratorLoop {su} [UpwardEnumerable α] [SupportsUpperBound su α] - {n : Type v → Type w} [Monad n] : - IteratorLoop (RangeIterator su α) Id n := - .defaultImplementation - -instance RangeIterator.instIteratorLoopPartial {su} [UpwardEnumerable α] [SupportsUpperBound su α] - {n : Type v → Type w} [Monad n] : IteratorLoopPartial (RangeIterator su α) Id n := - .defaultImplementation - instance RangeIterator.instIteratorCollect {su} [UpwardEnumerable α] [SupportsUpperBound su α] {n : Type u → Type w} [Monad n] : IteratorCollect (RangeIterator su α) Id n := .defaultImplementation @@ -370,4 +360,223 @@ instance RangeIterator.instLawfulDeterministicIterator {su} [UpwardEnumerable α LawfulDeterministicIterator (RangeIterator su α) Id where isPlausibleStep_eq_eq it := ⟨Monadic.step it, rfl⟩ -end Std.PRange +theorem RangeIterator.Monadic.isPlausibleIndirectOutput_iff {su α} + [UpwardEnumerable α] [SupportsUpperBound su α] + [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableUpperBound su α] + {it : IterM (α := RangeIterator su α) Id α} {out : α} : + it.IsPlausibleIndirectOutput out ↔ + ∃ n, it.internalState.next.bind (UpwardEnumerable.succMany? n ·) = some out ∧ + SupportsUpperBound.IsSatisfied it.internalState.upperBound out := by + constructor + · intro h + induction h + case direct h => + rw [RangeIterator.Monadic.isPlausibleOutput_iff] at h + refine ⟨0, by simp [h, LawfulUpwardEnumerable.succMany?_zero]⟩ + case indirect h _ ih => + rw [RangeIterator.Monadic.isPlausibleSuccessorOf_iff] at h + obtain ⟨n, hn⟩ := ih + obtain ⟨a, ha, h₁, h₂, h₃⟩ := h + refine ⟨n + 1, ?_⟩ + simp [ha, ← h₃, hn.2, LawfulUpwardEnumerable.succMany?_succ_eq_succ?_bind_succMany?, h₂, hn] + · rintro ⟨n, hn, hu⟩ + induction n generalizing it + case zero => + apply IterM.IsPlausibleIndirectOutput.direct + rw [RangeIterator.Monadic.isPlausibleOutput_iff] + exact ⟨by simpa [LawfulUpwardEnumerable.succMany?_zero] using hn, hu⟩ + case succ ih => + cases hn' : it.internalState.next + · simp [hn'] at hn + rename_i a + simp only [hn', Option.bind_some] at hn + have hle : UpwardEnumerable.LE a out := ⟨_, hn⟩ + rw [LawfulUpwardEnumerable.succMany?_succ_eq_succ?_bind_succMany?] at hn + cases hn' : UpwardEnumerable.succ? a + · simp only [hn', Option.bind_none, reduceCtorEq] at hn + rename_i a' + simp only [hn', Option.bind_some] at hn + specialize ih (it := ⟨some a', it.internalState.upperBound⟩) hn hu + refine IterM.IsPlausibleIndirectOutput.indirect ?_ ih + rw [RangeIterator.Monadic.isPlausibleSuccessorOf_iff] + refine ⟨a, ‹_›, ?_, hn', rfl⟩ + apply LawfulUpwardEnumerableUpperBound.isSatisfied_of_le _ a out + · exact hu + · exact hle + +theorem RangeIterator.isPlausibleIndirectOutput_iff {su α} + [UpwardEnumerable α] [SupportsUpperBound su α] + [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableUpperBound su α] + {it : Iter (α := RangeIterator su α) α} {out : α} : + it.IsPlausibleIndirectOutput out ↔ + ∃ n, it.internalState.next.bind (UpwardEnumerable.succMany? n ·) = some out ∧ + SupportsUpperBound.IsSatisfied it.internalState.upperBound out := by + simp only [Iter.isPlausibleIndirectOutput_iff_isPlausibleIndirectOutput_toIterM, + Monadic.isPlausibleIndirectOutput_iff, Iter.toIterM] + +section IteratorLoop + +/-! +## Efficient `IteratorLoop` instance +As long as the compiler cannot optimize away the `Option` in the internal state, we use a special +loop implementation. +-/ + +@[always_inline, inline] +instance RangeIterator.instIteratorLoop {su} [UpwardEnumerable α] [SupportsUpperBound su α] + [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableUpperBound su α] + {n : Type u → Type w} [Monad n] : + IteratorLoop (RangeIterator su α) Id n where + forIn _ γ Pl wf it init f := + match it with + | ⟨⟨some next, upperBound⟩⟩ => + if hu : SupportsUpperBound.IsSatisfied upperBound next then + loop γ Pl wf upperBound next init (fun a ha₁ ha₂ c => f a ?hf c) next ?hle hu + else + return init + | ⟨⟨none, _⟩⟩ => return init + where + @[specialize] + loop γ Pl wf (upperBound : Bound su α) least acc + (f : (out : α) → UpwardEnumerable.LE least out → SupportsUpperBound.IsSatisfied upperBound out → (c : γ) → n (Subtype (fun s : ForInStep γ => Pl out c s))) + (next : α) (hl : UpwardEnumerable.LE least next) (hu : SupportsUpperBound.IsSatisfied upperBound next) : n γ := do + match ← f next hl hu acc with + | ⟨.yield acc', h⟩ => + match hs : UpwardEnumerable.succ? next with + | some next' => + if hu : SupportsUpperBound.IsSatisfied upperBound next' then + loop γ Pl wf upperBound least acc' f next' ?hle' hu + else + return acc' + | none => return acc' + | ⟨.done acc', _⟩ => return acc' + termination_by IteratorLoop.WithWF.mk ⟨⟨some next, upperBound⟩⟩ acc (hwf := wf) + decreasing_by + simp [IteratorLoop.rel, RangeIterator.Monadic.isPlausibleStep_iff, + RangeIterator.Monadic.step, *] + finally + case hf => + rw [RangeIterator.Monadic.isPlausibleIndirectOutput_iff] + obtain ⟨n, hn⟩ := ha₁ + exact ⟨n, hn, ha₂⟩ + case hle => + exact UpwardEnumerable.le_refl _ + case hle' => + refine UpwardEnumerable.le_trans hl ⟨1, ?_⟩ + simp [UpwardEnumerable.succMany?_one, hs] + +partial instance RepeatIterator.instIteratorLoopPartial {su} [UpwardEnumerable α] + [SupportsUpperBound su α] [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableUpperBound su α] + {n : Type u → Type w} [Monad n] : IteratorLoopPartial (RangeIterator su α) Id n where + forInPartial _ γ it init f := + match it with + | ⟨⟨some next, upperBound⟩⟩ => + if hu : SupportsUpperBound.IsSatisfied upperBound next then + loop γ upperBound next init (fun a ha₁ ha₂ c => f a ?hf c) next ?hle hu + else + return init + | ⟨⟨none, _⟩⟩ => return init + where + @[specialize] + loop γ (upperBound : Bound su α) least acc + (f : (out : α) → UpwardEnumerable.LE least out → SupportsUpperBound.IsSatisfied upperBound out → (c : γ) → n (ForInStep γ)) + (next : α) (hl : UpwardEnumerable.LE least next) (hu : SupportsUpperBound.IsSatisfied upperBound next) : n γ := do + match ← f next hl hu acc with + | .yield acc' => + match hs : UpwardEnumerable.succ? next with + | some next' => + if hu : SupportsUpperBound.IsSatisfied upperBound next' then + loop γ upperBound least acc' f next' ?hle' hu + else + return acc' + | none => return acc' + | .done acc' => return acc' + finally + case hf => + rw [RangeIterator.Monadic.isPlausibleIndirectOutput_iff] + obtain ⟨n, hn⟩ := ha₁ + exact ⟨n, hn, ha₂⟩ + case hle => + exact UpwardEnumerable.le_refl _ + case hle' => + refine UpwardEnumerable.le_trans hl ⟨1, ?_⟩ + simp [UpwardEnumerable.succMany?_one, hs] + +theorem RangeIterator.instIteratorLoop.loop_eq {su} [UpwardEnumerable α] [SupportsUpperBound su α] + [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableUpperBound su α] + {n : Type u → Type w} [Monad n] [LawfulMonad n] {γ : Type u} + {lift} [Internal.LawfulMonadLiftBindFunction lift] + {PlausibleForInStep} {upperBound} {next} {hl} {hu} {f} {acc} {wf} : + loop (α := α) (su := su) (n := n) γ PlausibleForInStep wf upperBound least acc f next hl hu = + (do + match ← f next hl hu acc with + | ⟨.yield c, _⟩ => + letI it' : IterM (α := RangeIterator su α) Id α := ⟨⟨UpwardEnumerable.succ? next, upperBound⟩⟩ + IterM.DefaultConsumers.forIn' (m := Id) lift γ + PlausibleForInStep wf it' c it'.IsPlausibleIndirectOutput (fun _ => id) + (fun b h c => f b + (by + refine UpwardEnumerable.le_trans hl ?_ + simp only [RangeIterator.Monadic.isPlausibleIndirectOutput_iff, it', + ← LawfulUpwardEnumerable.succMany?_succ_eq_succ?_bind_succMany?] at h + exact ⟨h.choose + 1, h.choose_spec.1⟩) + (by simp only [RangeIterator.Monadic.isPlausibleIndirectOutput_iff, it'] at h; exact h.choose_spec.2) c) + | ⟨.done c, _⟩ => return c) := by + rw [loop] + apply bind_congr + intro step + split + · split + · split + · simp only [*] + rw [IterM.DefaultConsumers.forIn'] + simp only [Monadic.step_eq_step, Monadic.step, ↓reduceIte, *, + Internal.LawfulMonadLiftBindFunction.liftBind_pure] + rw [loop_eq (lift := lift)] + apply bind_congr + intro step + split + · apply IterM.DefaultConsumers.forIn'_eq_forIn' + intros; rfl + · simp + · simp only [*] + rw [IterM.DefaultConsumers.forIn'] + simp [Monadic.step_eq_step, Monadic.step, *, + Internal.LawfulMonadLiftBindFunction.liftBind_pure] + · simp only [*] + rw [IterM.DefaultConsumers.forIn'] + simp [Monadic.step_eq_step, Monadic.step, Internal.LawfulMonadLiftBindFunction.liftBind_pure] + · simp +termination_by IteratorLoop.WithWF.mk ⟨⟨some next, upperBound⟩⟩ acc (hwf := wf) +decreasing_by + simp [IteratorLoop.rel, RangeIterator.Monadic.isPlausibleStep_iff, + RangeIterator.Monadic.step, *] + +instance RangeIterator.instLawfulIteratorLoop {su} [UpwardEnumerable α] [SupportsUpperBound su α] + [LawfulUpwardEnumerable α] [LawfulUpwardEnumerableUpperBound su α] + {n : Type u → Type w} [Monad n] [LawfulMonad n] : + LawfulIteratorLoop (RangeIterator su α) Id n where + lawful := by + intro lift instLawfulMonadLiftFunction + ext γ PlausibleForInStep hwf it init f + simp only [IteratorLoop.forIn, IteratorLoop.defaultImplementation] + rw [IterM.DefaultConsumers.forIn'] + simp only [RangeIterator.Monadic.step_eq_step, RangeIterator.Monadic.step] + simp only [Internal.LawfulMonadLiftBindFunction.liftBind_pure] + split + · rename_i it f next upperBound f' + simp + split + · simp only + rw [instIteratorLoop.loop_eq (lift := lift)] + apply bind_congr + intro step + split + · apply IterM.DefaultConsumers.forIn'_eq_forIn' + intro b c hPb hQb + congr + · simp + · simp + · simp + +end Std.PRange.IteratorLoop diff --git a/src/Init/Data/Vector/Basic.lean b/src/Init/Data/Vector/Basic.lean index 3701197b8b..3471559b17 100644 --- a/src/Init/Data/Vector/Basic.lean +++ b/src/Init/Data/Vector/Basic.lean @@ -8,13 +8,14 @@ module prelude public meta import Init.Coe +public import Init.Data.Stream public import Init.Data.Array.Lemmas public import Init.Data.Array.MapIdx public import Init.Data.Array.InsertIdx public import Init.Data.Array.Range public import Init.Data.Range -import Init.Data.Slice.Array.Basic -public import Init.Data.Stream +-- TODO: Making this private leads to a panic in Init.Grind.Ring.Poly. +public import Init.Data.Slice.Array.Iterator public section @@ -562,7 +563,7 @@ Lexicographic comparator for vectors. - there is an index `i` such that `lt v[i] w[i]`, and for all `j < i`, `v[j] == w[j]`. -/ def lex [BEq α] (xs ys : Vector α n) (lt : α → α → Bool := by exact (· < ·)) : Bool := Id.run do - for h : i in [0 : n] do + for h : i in 0...n do if lt xs[i] ys[i] then return true else if xs[i] != ys[i] then diff --git a/src/Init/Data/Vector/Lex.lean b/src/Init/Data/Vector/Lex.lean index 882f9a80af..6f3b856a62 100644 --- a/src/Init/Data/Vector/Lex.lean +++ b/src/Init/Data/Vector/Lex.lean @@ -10,6 +10,7 @@ public import all Init.Data.Vector.Basic public import Init.Data.Vector.Lemmas public import all Init.Data.Array.Lex.Basic public import Init.Data.Array.Lex.Lemmas +import Init.Data.Range.Polymorphic.Lemmas public section @@ -43,7 +44,7 @@ protected theorem not_le_iff_gt [LT α] {xs ys : Vector α n} : @[simp] theorem mk_lex_mk [BEq α] {lt : α → α → Bool} {xs ys : Array α} {n₁ : xs.size = n} {n₂ : ys.size = n} : (Vector.mk xs n₁).lex (Vector.mk ys n₂) lt = xs.lex ys lt := by - simp [Vector.lex, Array.lex, n₁, n₂] + simp [Vector.lex, Array.lex, n₁, n₂, Std.PRange.forIn'_eq_forIn'_toList] rfl @[simp, grind =] theorem lex_toArray [BEq α] {lt : α → α → Bool} {xs ys : Vector α n} : diff --git a/src/Lean/Compiler/IR/Basic.lean b/src/Lean/Compiler/IR/Basic.lean index c643c6ba9a..3ec4f64e21 100644 --- a/src/Lean/Compiler/IR/Basic.lean +++ b/src/Lean/Compiler/IR/Basic.lean @@ -523,7 +523,7 @@ def addParamsRename (ρ : IndexRenaming) (ps₁ ps₂ : Array Param) : Option In failure else let mut ρ := ρ - for i in [:ps₁.size] do + for i in *...ps₁.size do ρ ← addParamRename ρ ps₁[i]! ps₂[i]! pure ρ diff --git a/src/Lean/Compiler/IR/EmitLLVM.lean b/src/Lean/Compiler/IR/EmitLLVM.lean index 4ae99e930a..f38b71a630 100644 --- a/src/Lean/Compiler/IR/EmitLLVM.lean +++ b/src/Lean/Compiler/IR/EmitLLVM.lean @@ -1176,7 +1176,7 @@ def emitFnArgs (builder : LLVM.Builder llvmctx) (needsPackedArgs? : Bool) (llvmfn : LLVM.Value llvmctx) (params : Array Param) : M llvmctx Unit := do if needsPackedArgs? then do let argsp ← LLVM.getParam llvmfn 0 -- lean_object **args - for h : i in [:params.size] do + for h : i in *...params.size do let param := params[i] -- argsi := (args + i) let argsi ← LLVM.buildGEP2 builder (← LLVM.voidPtrType llvmctx) argsp #[← constIntUnsigned i] s!"packed_arg_{i}_slot" @@ -1189,7 +1189,7 @@ def emitFnArgs (builder : LLVM.Builder llvmctx) addVartoState param.x alloca llvmty else let n ← LLVM.countParams llvmfn - for i in [:n.toNat] do + for i in *...n.toNat do let param := params[i]! let llvmty ← toLLVMType param.ty let alloca ← buildPrologueAlloca builder llvmty s!"arg_{i}" diff --git a/src/Lean/Compiler/IR/SimpCase.lean b/src/Lean/Compiler/IR/SimpCase.lean index e1519f8412..95ab37c44b 100644 --- a/src/Lean/Compiler/IR/SimpCase.lean +++ b/src/Lean/Compiler/IR/SimpCase.lean @@ -20,7 +20,7 @@ def ensureHasDefault (alts : Array Alt) : Array Alt := private def getOccsOf (alts : Array Alt) (i : Nat) : Nat := Id.run do let aBody := alts[i]!.body let mut n := 1 - for h : j in [i+1:alts.size] do + for h : j in (i+1)...alts.size do if alts[j].body == aBody then n := n+1 return n @@ -28,7 +28,7 @@ private def getOccsOf (alts : Array Alt) (i : Nat) : Nat := Id.run do private def maxOccs (alts : Array Alt) : Alt × Nat := Id.run do let mut maxAlt := alts[0]! let mut max := getOccsOf alts 0 - for h : i in [1:alts.size] do + for h : i in 1...alts.size do let curr := getOccsOf alts i if curr > max then maxAlt := alts[i] diff --git a/src/Lean/Compiler/IR/ToIR.lean b/src/Lean/Compiler/IR/ToIR.lean index 4767e0afca..e395f49203 100644 --- a/src/Lean/Compiler/IR/ToIR.lean +++ b/src/Lean/Compiler/IR/ToIR.lean @@ -184,7 +184,7 @@ partial def lowerLet (decl : LCNF.LetDecl) (k : LCNF.Code) : M FnBody := do let args := args.extract (start := ctorVal.numParams) let objArgs : Array Arg ← do let mut result : Array Arg := #[] - for i in [0:fields.size] do + for i in *...fields.size do match args[i]! with | .fvar fvarId => if let some (.var varId) := (← get).fvars[fvarId]? then diff --git a/src/Lean/Compiler/LCNF/Check.lean b/src/Lean/Compiler/LCNF/Check.lean index 419d4236ba..2b3a927e50 100644 --- a/src/Lean/Compiler/LCNF/Check.lean +++ b/src/Lean/Compiler/LCNF/Check.lean @@ -110,7 +110,7 @@ def isCtorParam (f : Expr) (i : Nat) : CoreM Bool := do def checkAppArgs (f : Expr) (args : Array Arg) : CheckM Unit := do let mut fType ← inferType f let mut j := 0 - for h : i in [:args.size] do + for h : i in *...args.size do let arg := args[i] if fType.isErased then return () diff --git a/src/Lean/Compiler/LCNF/ElimDeadBranches.lean b/src/Lean/Compiler/LCNF/ElimDeadBranches.lean index 06e459578b..90c440dcbb 100644 --- a/src/Lean/Compiler/LCNF/ElimDeadBranches.lean +++ b/src/Lean/Compiler/LCNF/ElimDeadBranches.lean @@ -527,7 +527,7 @@ ones. Return whether any `Value` got updated in the process. -/ def inferStep : InterpM Bool := do let ctx ← read - for h : idx in [0:ctx.decls.size] do + for h : idx in *...ctx.decls.size do let decl := ctx.decls[idx] if !decl.safe then continue diff --git a/src/Lean/Compiler/LCNF/FixedParams.lean b/src/Lean/Compiler/LCNF/FixedParams.lean index a8b35bb3d6..62df67d888 100644 --- a/src/Lean/Compiler/LCNF/FixedParams.lean +++ b/src/Lean/Compiler/LCNF/FixedParams.lean @@ -136,9 +136,9 @@ partial def evalApp (declName : Name) (args : Array Arg) : FixParamM Unit := do let main := (← read).main if declName == main.name then -- Recursive call to the function being analyzed - for h : i in [:main.params.size] do + for h : i in *...main.params.size do if _h : i < args.size then - have : i < main.params.size := h.upper + have : i < main.params.size := h.2 let param := main.params[i] let val ← evalArg args[i] unless val == .val i || (val == .erased && param.type.isErased) do @@ -154,7 +154,7 @@ partial def evalApp (declName : Name) (args : Array Arg) : FixParamM Unit := do if declName == decl.name then -- Call to another function in the same mutual block. let mut values := #[] - for i in [:decl.params.size] do + for i in *...decl.params.size do if h : i < args.size then values := values.push (← evalArg args[i]) else @@ -170,7 +170,7 @@ end def mkInitialValues (numParams : Nat) : Array AbsValue := Id.run do let mut values := #[] - for i in [:numParams] do + for i in *...numParams do values := values.push <| .val i return values diff --git a/src/Lean/Compiler/LCNF/InferType.lean b/src/Lean/Compiler/LCNF/InferType.lean index 4d51ee6911..6247621ea7 100644 --- a/src/Lean/Compiler/LCNF/InferType.lean +++ b/src/Lean/Compiler/LCNF/InferType.lean @@ -139,7 +139,7 @@ mutual partial def inferAppTypeCore (fType : Expr) (args : Array Arg) : InferTypeM Expr := do let mut j := 0 let mut fType := fType - for i in [:args.size] do + for i in *...args.size do fType := fType.headBeta match fType with | .forallE _ _ b _ => fType := b @@ -154,7 +154,7 @@ mutual let mut j := 0 let mut fType ← inferType e.getAppFn let args := e.getAppArgs - for i in [:args.size] do + for i in *...args.size do fType := fType.headBeta match fType with | .forallE _ _ b _ => fType := b @@ -181,7 +181,7 @@ mutual failed () else do let mut ctorType ← inferAppType (mkAppN (mkConst ctorVal.name structLvls) structTypeArgs[*...structVal.numParams]) - for _ in [:idx] do + for _ in *...idx do match ctorType with | .forallE _ _ body _ => if body.hasLooseBVars then diff --git a/src/Lean/Compiler/LCNF/MonoTypes.lean b/src/Lean/Compiler/LCNF/MonoTypes.lean index f5dfa4eed0..a6a0ef571e 100644 --- a/src/Lean/Compiler/LCNF/MonoTypes.lean +++ b/src/Lean/Compiler/LCNF/MonoTypes.lean @@ -60,7 +60,7 @@ where fillCache : CoreM (Option TrivialStructureInfo) := do if ctorType.isErased then return none let mask ← getRelevantCtorFields ctorName let mut result := none - for h : i in [:mask.size] do + for h : i in *...mask.size do if mask[i] then if result.isSome then return none result := some { ctorName, fieldIdx := i, numParams := info.numParams } diff --git a/src/Lean/Compiler/LCNF/PassManager.lean b/src/Lean/Compiler/LCNF/PassManager.lean index 5c4a740a4f..076695b3bc 100644 --- a/src/Lean/Compiler/LCNF/PassManager.lean +++ b/src/Lean/Compiler/LCNF/PassManager.lean @@ -131,7 +131,7 @@ def withEachOccurrence (targetName : Name) (f : Nat → PassInstaller) : PassIns install passes := do let highestOccurrence ← PassManager.findHighestOccurrence targetName passes let mut passes := passes - for occurrence in [0:highestOccurrence+1] do + for occurrence in *...=highestOccurrence do passes ← f occurrence |>.install passes return passes diff --git a/src/Lean/Compiler/LCNF/PhaseExt.lean b/src/Lean/Compiler/LCNF/PhaseExt.lean index 3a0c83e74d..cf9f2e221a 100644 --- a/src/Lean/Compiler/LCNF/PhaseExt.lean +++ b/src/Lean/Compiler/LCNF/PhaseExt.lean @@ -103,7 +103,7 @@ def getExt (phase : Phase) : DeclExt := def forEachDecl (f : Decl → CoreM Unit) (phase := Phase.base) : CoreM Unit := do let ext := getExt phase let env ← getEnv - for modIdx in [:env.allImportedModuleNames.size] do + for modIdx in *...env.allImportedModuleNames.size do for decl in ext.getModuleEntries env modIdx do f decl ext.getState env |>.forM fun _ decl => f decl diff --git a/src/Lean/Compiler/LCNF/Probing.lean b/src/Lean/Compiler/LCNF/Probing.lean index 659e843b52..dfbd548b93 100644 --- a/src/Lean/Compiler/LCNF/Probing.lean +++ b/src/Lean/Compiler/LCNF/Probing.lean @@ -189,7 +189,7 @@ def runGlobally (probe : Probe Decl β) (phase : Phase := Phase.base) : CoreM (A let ext := getExt phase let env ← getEnv let mut decls := #[] - for modIdx in [:env.allImportedModuleNames.size] do + for modIdx in *...env.allImportedModuleNames.size do decls := decls.append <| ext.getModuleEntries env modIdx probe decls |>.run (phase := phase) diff --git a/src/Lean/Compiler/LCNF/PullFunDecls.lean b/src/Lean/Compiler/LCNF/PullFunDecls.lean index 2635469403..f1f201921d 100644 --- a/src/Lean/Compiler/LCNF/PullFunDecls.lean +++ b/src/Lean/Compiler/LCNF/PullFunDecls.lean @@ -86,7 +86,7 @@ partial def attach (ps : Array ToPull) (k : Code) : Code := Id.run do return k where go : StateM (Code × Array Bool) Unit := do - for i in [:ps.size] do + for i in *...ps.size do visit i visited (i : Nat) : StateM (Code × Array Bool) Bool := @@ -96,7 +96,7 @@ where unless (← visited i) do modify fun (k, visited) => (k, visited.set! i true) let pi := ps[i]! - for h : j in [:ps.size] do + for h : j in *...ps.size do unless (← visited j) do let pj := ps[j] if pj.used.contains pi.decl.fvarId then diff --git a/src/Lean/Compiler/LCNF/Simp/DefaultAlt.lean b/src/Lean/Compiler/LCNF/Simp/DefaultAlt.lean index 2c12155672..0b2a5ea39d 100644 --- a/src/Lean/Compiler/LCNF/Simp/DefaultAlt.lean +++ b/src/Lean/Compiler/LCNF/Simp/DefaultAlt.lean @@ -18,7 +18,7 @@ or not. private def getMaxOccs (alts : Array Alt) : Alt × Nat := Id.run do let mut maxAlt := alts[0]! let mut max := getNumOccsOf alts 0 - for h : i in [1:alts.size] do + for h : i in 1...alts.size do let curr := getNumOccsOf alts i if curr > max then maxAlt := alts[i] @@ -34,7 +34,7 @@ where getNumOccsOf (alts : Array Alt) (i : Nat) : Nat := Id.run do let code := alts[i]!.getCode let mut n := 1 - for h : j in [i+1:alts.size] do + for h : j in (i+1)...alts.size do if Code.alphaEqv alts[j].getCode code then n := n+1 return n diff --git a/src/Lean/Compiler/LCNF/Simp/JpCases.lean b/src/Lean/Compiler/LCNF/Simp/JpCases.lean index c82a9ed593..2a19e97bcb 100644 --- a/src/Lean/Compiler/LCNF/Simp/JpCases.lean +++ b/src/Lean/Compiler/LCNF/Simp/JpCases.lean @@ -121,7 +121,7 @@ where let mut paramsNew := #[] let singleton : FVarIdSet := ({} : FVarIdSet).insert params[targetParamIdx]!.fvarId let dependsOnDiscr := k.dependsOn singleton || decls.any (·.dependsOn singleton) - for h : i in [:params.size] do + for h : i in *...params.size do let param := params[i] if targetParamIdx == i then if dependsOnDiscr then diff --git a/src/Lean/Compiler/LCNF/SpecInfo.lean b/src/Lean/Compiler/LCNF/SpecInfo.lean index e3786aeb46..b9a7970e25 100644 --- a/src/Lean/Compiler/LCNF/SpecInfo.lean +++ b/src/Lean/Compiler/LCNF/SpecInfo.lean @@ -132,7 +132,7 @@ See comment at `.fixedNeutral`. -/ private def hasFwdDeps (decl : Decl) (paramsInfo : Array SpecParamInfo) (j : Nat) : Bool := Id.run do let param := decl.params[j]! - for h : k in [j+1 : decl.params.size] do + for h : k in (j+1)...decl.params.size do if paramsInfo[k]! matches .user | .fixedHO | .fixedInst then let param' := decl.params[k] if param'.type.containsFVar param.fvarId then @@ -155,7 +155,7 @@ def saveSpecParamInfo (decls : Array Decl) : CompilerM Unit := do let specArgs? := getSpecializationArgs? (← getEnv) decl.name let contains (i : Nat) : Bool := specArgs?.getD #[] |>.contains i let mut paramsInfo : Array SpecParamInfo := #[] - for h :i in [:decl.params.size] do + for h :i in *...decl.params.size do let param := decl.params[i] let info ← if contains i then @@ -184,7 +184,7 @@ def saveSpecParamInfo (decls : Array Decl) : CompilerM Unit := do declsInfo := declsInfo.push paramsInfo if declsInfo.any fun paramsInfo => paramsInfo.any (· matches .user | .fixedInst | .fixedHO) then let m := mkFixedParamsMap decls - for hi : i in [:decls.size] do + for hi : i in *...decls.size do let decl := decls[i] let mut paramsInfo := declsInfo[i]! let some mask := m.find? decl.name | unreachable! @@ -194,7 +194,7 @@ def saveSpecParamInfo (decls : Array Decl) : CompilerM Unit := do info else .other - for j in [:paramsInfo.size] do + for j in *...paramsInfo.size do let mut info := paramsInfo[j]! if info matches .fixedNeutral && !hasFwdDeps decl paramsInfo j then paramsInfo := paramsInfo.set! j .other diff --git a/src/Lean/Compiler/LCNF/StructProjCases.lean b/src/Lean/Compiler/LCNF/StructProjCases.lean index 984938b66e..2c3600eb50 100644 --- a/src/Lean/Compiler/LCNF/StructProjCases.lean +++ b/src/Lean/Compiler/LCNF/StructProjCases.lean @@ -22,13 +22,13 @@ def findStructCtorInfo? (typeName : Name) : CoreM (Option ConstructorVal) := do def mkFieldParamsForCtorType (ctorType : Expr) (numParams : Nat) (numFields : Nat) : CompilerM (Array Param) := do let mut type := ctorType - for _ in [0:numParams] do + for _ in *...numParams do match type with | .forallE _ _ body _ => type := body | _ => unreachable! let mut fields := Array.emptyWithCapacity numFields - for _ in [0:numFields] do + for _ in *...numFields do match type with | .forallE name fieldType body _ => let param ← mkParam name (← toMonoType fieldType) false diff --git a/src/Lean/Compiler/LCNF/ToLCNF.lean b/src/Lean/Compiler/LCNF/ToLCNF.lean index 2dcd0ef7be..2b1907b86e 100644 --- a/src/Lean/Compiler/LCNF/ToLCNF.lean +++ b/src/Lean/Compiler/LCNF/ToLCNF.lean @@ -510,7 +510,7 @@ where match app with | .fvar f => let mut argsNew := #[] - for h :i in [arity : args.size] do + for h : i in arity...args.size do argsNew := argsNew.push (← visitAppArg args[i]) letValueToArg <| .fvar f argsNew | .erased | .type .. => return .erased diff --git a/src/Lean/Compiler/LCNF/ToMono.lean b/src/Lean/Compiler/LCNF/ToMono.lean index ed310c168b..6296183812 100644 --- a/src/Lean/Compiler/LCNF/ToMono.lean +++ b/src/Lean/Compiler/LCNF/ToMono.lean @@ -134,13 +134,13 @@ def LetDecl.toMono (decl : LetDecl) : ToMonoM LetDecl := do def mkFieldParamsForComputedFields (ctorType : Expr) (numParams : Nat) (numNewFields : Nat) (oldFields : Array Param) : ToMonoM (Array Param) := do let mut type := ctorType - for _ in [0:numParams] do + for _ in *...numParams do match type with | .forallE _ _ body _ => type := body | _ => unreachable! let mut newFields := Array.emptyWithCapacity (oldFields.size + numNewFields) - for _ in [0:numNewFields] do + for _ in *...numNewFields do match type with | .forallE name fieldType body _ => let param ← mkParam name (← toMonoType fieldType) false diff --git a/src/Lean/Compiler/LCNF/Util.lean b/src/Lean/Compiler/LCNF/Util.lean index f81bf22250..ee3625b9f7 100644 --- a/src/Lean/Compiler/LCNF/Util.lean +++ b/src/Lean/Compiler/LCNF/Util.lean @@ -37,7 +37,7 @@ structure CasesInfo where arity : Nat numParams : Nat discrPos : Nat - altsRange : Std.Range + altsRange : Std.PRange ⟨.closed, .open⟩ Nat altNumParams : Array Nat motivePos : Nat @@ -56,7 +56,7 @@ def getCasesInfo? (declName : Name) : CoreM (Option CasesInfo) := do let arity := numParams + 1 /- motive -/ + val.numIndices + 1 /- major -/ + val.numCtors let discrPos := numParams + 1 /- motive -/ + val.numIndices -- We view indices as discriminants - let altsRange := [discrPos + 1:arity] + let altsRange := (discrPos + 1)...arity let altNumParams ← val.ctors.toArray.mapM fun ctor => do let .ctorInfo ctorVal ← getConstInfo ctor | unreachable! return ctorVal.numFields diff --git a/src/Lean/Data/Array.lean b/src/Lean/Data/Array.lean index e65c958899..705eb93fc3 100644 --- a/src/Lean/Data/Array.lean +++ b/src/Lean/Data/Array.lean @@ -4,7 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Joachim Breitner -/ prelude -import Init.Data.Range +import Init.Data.Range.Polymorphic.Nat +import Init.Data.Range.Polymorphic.Iterators namespace Array @@ -36,7 +37,7 @@ def filterPairsM {m} [Monad m] {α} (a : Array α) (f : α → α → m (Bool × m (Array α) := do let mut removed := Array.replicate a.size false let mut numRemoved := 0 - for h1 : i in [:a.size] do for h2 : j in [i+1:a.size] do + for h1 : i in *...a.size do for h2 : j in (i+1)...a.size do unless removed[i]! || removed[j]! do let xi := a[i] let xj := a[j] @@ -48,7 +49,7 @@ def filterPairsM {m} [Monad m] {α} (a : Array α) (f : α → α → m (Bool × numRemoved := numRemoved + 1 removed := removed.set! j true let mut a' := Array.mkEmpty numRemoved - for h : i in [:a.size] do + for h : i in *...a.size do unless removed[i]! do a' := a'.push a[i] return a' diff --git a/src/Lean/Data/FuzzyMatching.lean b/src/Lean/Data/FuzzyMatching.lean index 26b50ab542..62f22bad1c 100644 --- a/src/Lean/Data/FuzzyMatching.lean +++ b/src/Lean/Data/FuzzyMatching.lean @@ -9,9 +9,11 @@ code's client side filtering algorithm. For the LLVM implementation see https://clang.llvm.org/extra//doxygen/FuzzyMatch_8cpp_source.html -/ prelude -import Init.Data.Range +import Init.Data.Range.Polymorphic.Iterators +import Init.Data.Range.Polymorphic.Nat import Init.Data.OfScientific import Init.Data.Option.Coe +import Init.Data.Range namespace Lean namespace FuzzyMatching @@ -36,7 +38,7 @@ private def containsInOrderLower (a b : String) : Bool := Id.run do return true let mut aIt := a.mkIterator -- TODO: the following code is assuming all characters are ASCII - for i in [:b.endPos.byteIdx] do + for i in *...b.endPos.byteIdx do if aIt.curr.toLower == (b.get ⟨i⟩).toLower then aIt := aIt.next if !aIt.hasNext then @@ -124,7 +126,7 @@ private def fuzzyMatchCore (pattern word : String) (patternRoles wordRoles : Arr /- For this dynamic program to be correct, it's only necessary to populate a range of length `word.length - pattern.length` at each index (because at the very end, we can only consider fuzzy matches of `pattern` with a longer substring of `word`). -/ - for wordIdx in [patternIdx:word.length-(pattern.length - patternIdx - 1)] do + for wordIdx in [patternIdx:(word.length-(pattern.length - patternIdx - 1))] do let missScore? := if wordIdx >= 1 then selectBest diff --git a/src/Lean/Data/Json/Basic.lean b/src/Lean/Data/Json/Basic.lean index 86e17ee263..47e5966d4d 100644 --- a/src/Lean/Data/Json/Basic.lean +++ b/src/Lean/Data/Json/Basic.lean @@ -45,7 +45,7 @@ protected def normalize : JsonNumber → Int × Nat × Int let mut mAbs := m.natAbs let nDigits := countDigits mAbs -- eliminate trailing zeros - for _ in [0:nDigits] do + for _ in *...nDigits do if mAbs % 10 = 0 then mAbs := mAbs / 10 else diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean index d958e6ef6e..1b89adb764 100644 --- a/src/Lean/Elab/App.lean +++ b/src/Lean/Elab/App.lean @@ -432,7 +432,7 @@ private def findNamedArgDependsOnCurrent? : M (Option NamedArg) := do else forallTelescopeReducing s.fType fun xs _ => do let curr := xs[0]! - for h : i in [1:xs.size] do + for h : i in 1...xs.size do let xDecl ← xs[i].fvarId!.getDecl if let some arg := s.namedArgs.find? fun arg => arg.name == xDecl.userName then /- Remark: a default value at `optParam` does not count as a dependency -/ @@ -826,7 +826,7 @@ def getElabElimExprInfo (elimExpr : Expr) : MetaM ElabElimInfo := do return s /- Collect the major parameter positions -/ let mut majorsPos := #[] - for h : i in [:xs.size] do + for h : i in *...xs.size do let x := xs[i] unless motivePos == i do let xType ← x.fvarId!.getType diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean index d508660084..d18429e42a 100644 --- a/src/Lean/Elab/BuiltinCommand.lean +++ b/src/Lean/Elab/BuiltinCommand.lean @@ -63,7 +63,7 @@ def withNamespace {α} (ns : Name) (elabFn : CommandElabM α) : CommandElabM α pure a private def popScopes (numScopes : Nat) : CommandElabM Unit := - for _ in [0:numScopes] do + for _ in *...numScopes do popScope private def innermostScopeName? : List Scope → Option Name diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean index 57ec08bd4f..0243a21995 100644 --- a/src/Lean/Elab/BuiltinNotation.lean +++ b/src/Lean/Elab/BuiltinNotation.lean @@ -55,7 +55,7 @@ open Meta let cinfo ← getConstInfoCtor ctor let numExplicitFields ← forallTelescopeReducing cinfo.type fun xs _ => do let mut n := 0 - for h : i in [cinfo.numParams:xs.size] do + for h : i in cinfo.numParams...xs.size do if (← getFVarLocalDecl xs[i]).binderInfo.isExplicit then n := n + 1 return n diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean index 9078e74e8d..3255cdb60e 100644 --- a/src/Lean/Elab/Command.lean +++ b/src/Lean/Elab/Command.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura, Gabriel Ebner -/ prelude +import Init.Data.Range.Polymorphic.Stream import Lean.Meta.Diagnostics import Lean.Elab.Binders import Lean.Elab.SyntheticMVars @@ -564,7 +565,7 @@ where go := do let opts ← getOptions -- For each command, associate it with new promise and old snapshot, if any, and -- elaborate recursively - for cmd in cmds, cmdPromise in cmdPromises, i in [0:cmds.size] do + for cmd in cmds, cmdPromise in cmdPromises, i in *...cmds.size do let oldCmd? := oldCmds?.bind (·[i]?) withReader ({ · with snap? := some { new := cmdPromise diff --git a/src/Lean/Elab/DeclNameGen.lean b/src/Lean/Elab/DeclNameGen.lean index 550ee9cbc8..589436cee4 100644 --- a/src/Lean/Elab/DeclNameGen.lean +++ b/src/Lean/Elab/DeclNameGen.lean @@ -64,7 +64,7 @@ private partial def winnowExpr (e : Expr) : MetaM Expr := do let mut fty ← inferType f let mut j := 0 let mut e' ← visit f - for h : i in [0:args.size] do + for h : i in *...args.size do unless fty.isForall do fty ← withTransparency .all <| whnf <| fty.instantiateRevRange j i args j := i diff --git a/src/Lean/Elab/Deriving/BEq.lean b/src/Lean/Elab/Deriving/BEq.lean index d13dc4f0c1..809b4cc0fd 100644 --- a/src/Lean/Elab/Deriving/BEq.lean +++ b/src/Lean/Elab/Deriving/BEq.lean @@ -23,7 +23,7 @@ where mkElseAlt : TermElabM (TSyntax ``matchAltExpr) := do let mut patterns := #[] -- add `_` pattern for indices - for _ in [:indVal.numIndices] do + for _ in *...indVal.numIndices do patterns := patterns.push (← `(_)) patterns := patterns.push (← `(_)) patterns := patterns.push (← `(_)) @@ -38,13 +38,13 @@ where let type ← Core.betaReduce type -- we 'beta-reduce' to eliminate "artificial" dependencies let mut patterns := #[] -- add `_` pattern for indices - for _ in [:indVal.numIndices] do + for _ in *...indVal.numIndices do patterns := patterns.push (← `(_)) let mut ctorArgs1 := #[] let mut ctorArgs2 := #[] let mut rhs ← `(true) let mut rhs_empty := true - for i in [:ctorInfo.numFields] do + for i in *...ctorInfo.numFields do let pos := indVal.numParams + ctorInfo.numFields - i - 1 let x := xs[pos]! if type.containsFVar x.fvarId! then @@ -81,7 +81,7 @@ where else rhs ← `($a:ident == $b:ident && $rhs) -- add `_` for inductive parameters, they are inaccessible - for _ in [:indVal.numParams] do + for _ in *...indVal.numParams do ctorArgs1 := ctorArgs1.push (← `(_)) ctorArgs2 := ctorArgs2.push (← `(_)) patterns := patterns.push (← `(@$(mkIdent ctorName):ident $ctorArgs1.reverse:term*)) @@ -107,7 +107,7 @@ def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM Command := do def mkMutualBlock (ctx : Context) : TermElabM Syntax := do let mut auxDefs := #[] - for i in [:ctx.typeInfos.size] do + for i in *...ctx.typeInfos.size do auxDefs := auxDefs.push (← mkAuxFunction ctx i) `(mutual set_option match.ignoreUnusedAlts true diff --git a/src/Lean/Elab/Deriving/DecEq.lean b/src/Lean/Elab/Deriving/DecEq.lean index 552de6b91a..d4f487ea53 100644 --- a/src/Lean/Elab/Deriving/DecEq.lean +++ b/src/Lean/Elab/Deriving/DecEq.lean @@ -45,7 +45,7 @@ where for ctorName₂ in indVal.ctors do let mut patterns := #[] -- add `_` pattern for indices - for _ in [:indVal.numIndices] do + for _ in *...indVal.numIndices do patterns := patterns.push (← `(_)) if ctorName₁ == ctorName₂ then let alt ← forallTelescopeReducing ctorInfo.type fun xs type => do @@ -54,11 +54,11 @@ where let mut ctorArgs1 := #[] let mut ctorArgs2 := #[] -- add `_` for inductive parameters, they are inaccessible - for _ in [:indVal.numParams] do + for _ in *...indVal.numParams do ctorArgs1 := ctorArgs1.push (← `(_)) ctorArgs2 := ctorArgs2.push (← `(_)) let mut todo := #[] - for i in [:ctorInfo.numFields] do + for i in *...ctorInfo.numFields do let x := xs[indVal.numParams + i]! if type.containsFVar x.fvarId! then -- If resulting type depends on this field, we don't need to compare @@ -102,7 +102,7 @@ def mkAuxFunction (ctx : Context) (auxFunName : Name) (indVal : InductiveVal): T def mkAuxFunctions (ctx : Context) : TermElabM (TSyntax `command) := do let mut res : Array (TSyntax `command) := #[] - for i in [:ctx.auxFunNames.size] do + for i in *...ctx.auxFunNames.size do let auxFunName := ctx.auxFunNames[i]! let indVal := ctx.typeInfos[i]! res := res.push (← mkAuxFunction ctx auxFunName indVal) diff --git a/src/Lean/Elab/Deriving/FromToJson.lean b/src/Lean/Elab/Deriving/FromToJson.lean index 70989ac45d..21693241ca 100644 --- a/src/Lean/Elab/Deriving/FromToJson.lean +++ b/src/Lean/Elab/Deriving/FromToJson.lean @@ -71,16 +71,16 @@ where let alt ← forallTelescopeReducing ctorInfo.type fun xs _ => do let mut patterns := #[] -- add `_` pattern for indices - for _ in [:indVal.numIndices] do + for _ in *...indVal.numIndices do patterns := patterns.push (← `(_)) let mut ctorArgs := #[] -- add `_` for inductive parameters, they are inaccessible - for _ in [:indVal.numParams] do + for _ in *...indVal.numParams do ctorArgs := ctorArgs.push (← `(_)) -- bound constructor arguments and their types let mut binders := #[] let mut userNames := #[] - for i in [:ctorInfo.numFields] do + for i in *...ctorInfo.numFields do let x := xs[indVal.numParams + i]! let localDecl ← x.fvarId!.getDecl if !localDecl.userName.hasMacroScopes then @@ -119,7 +119,7 @@ where let alt ← do forallTelescopeReducing ctorInfo.type fun xs _ => do let mut binders := #[] let mut userNames := #[] - for i in [:ctorInfo.numFields] do + for i in *...ctorInfo.numFields do let x := xs[indVal.numParams + i]! let localDecl ← x.fvarId!.getDecl if !localDecl.userName.hasMacroScopes then @@ -195,7 +195,7 @@ def mkFromJsonAuxFunction (ctx : Context) (i : Nat) : TermElabM Command := do def mkToJsonMutualBlock (ctx : Context) : TermElabM Command := do let mut auxDefs := #[] - for i in [:ctx.typeInfos.size] do + for i in *...ctx.typeInfos.size do auxDefs := auxDefs.push (← mkToJsonAuxFunction ctx i) `(mutual $auxDefs:command* @@ -203,7 +203,7 @@ def mkToJsonMutualBlock (ctx : Context) : TermElabM Command := do def mkFromJsonMutualBlock (ctx : Context) : TermElabM Command := do let mut auxDefs := #[] - for i in [:ctx.typeInfos.size] do + for i in *...ctx.typeInfos.size do auxDefs := auxDefs.push (← mkFromJsonAuxFunction ctx i) `(mutual $auxDefs:command* diff --git a/src/Lean/Elab/Deriving/Hashable.lean b/src/Lean/Elab/Deriving/Hashable.lean index b39cc0f99e..0fe992a5e7 100644 --- a/src/Lean/Elab/Deriving/Hashable.lean +++ b/src/Lean/Elab/Deriving/Hashable.lean @@ -31,14 +31,14 @@ where let alt ← forallTelescopeReducing ctorInfo.type fun xs _ => do let mut patterns := #[] -- add `_` pattern for indices - for _ in [:indVal.numIndices] do + for _ in *...indVal.numIndices do patterns := patterns.push (← `(_)) let mut ctorArgs := #[] let mut rhs ← `($(quote ctorIdx)) -- add `_` for inductive parameters, they are inaccessible - for _ in [:indVal.numParams] do + for _ in *...indVal.numParams do ctorArgs := ctorArgs.push (← `(_)) - for i in [:ctorInfo.numFields] do + for i in *...ctorInfo.numFields do let x := xs[indVal.numParams + i]! let a := mkIdent (← mkFreshUserName `a) ctorArgs := ctorArgs.push a @@ -72,7 +72,7 @@ def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM Command := do def mkHashFuncs (ctx : Context) : TermElabM Syntax := do let mut auxDefs := #[] - for i in [:ctx.typeInfos.size] do + for i in *...ctx.typeInfos.size do auxDefs := auxDefs.push (← mkAuxFunction ctx i) `(mutual $auxDefs:command* end) diff --git a/src/Lean/Elab/Deriving/Inhabited.lean b/src/Lean/Elab/Deriving/Inhabited.lean index f78546518e..11c032dbe8 100644 --- a/src/Lean/Elab/Deriving/Inhabited.lean +++ b/src/Lean/Elab/Deriving/Inhabited.lean @@ -63,7 +63,7 @@ where let ctorVal ← getConstInfoCtor ctorName let mut indArgs := #[] let mut binders := #[] - for i in [:indVal.numParams + indVal.numIndices] do + for i in *...indVal.numParams + indVal.numIndices do let arg := mkIdent (← mkFreshUserName `a) indArgs := indArgs.push arg let binder ← `(bracketedBinderF| { $arg:ident }) @@ -73,9 +73,9 @@ where binders := binders.push binder let type ← `(Inhabited (@$(mkIdent inductiveTypeName):ident $indArgs:ident*)) let mut ctorArgs := #[] - for _ in [:ctorVal.numParams] do + for _ in *...ctorVal.numParams do ctorArgs := ctorArgs.push (← `(_)) - for _ in [:ctorVal.numFields] do + for _ in *...ctorVal.numFields do ctorArgs := ctorArgs.push (← ``(Inhabited.default)) let val ← `(⟨@$(mkIdent ctorName):ident $ctorArgs*⟩) `(instance $binders:bracketedBinder* : $type := $val) @@ -86,7 +86,7 @@ where addLocalInstancesForParams xs[*...ctorVal.numParams] fun localInst2Index => do let mut usedInstIdxs := {} let mut ok := true - for h : i in [ctorVal.numParams:xs.size] do + for h : i in ctorVal.numParams...xs.size do let x := xs[i] let instType ← mkAppM `Inhabited #[(← inferType x)] trace[Elab.Deriving.inhabited] "checking {instType} for '{ctorName}'" diff --git a/src/Lean/Elab/Deriving/Ord.lean b/src/Lean/Elab/Deriving/Ord.lean index 8f9fbab033..34575c4202 100644 --- a/src/Lean/Elab/Deriving/Ord.lean +++ b/src/Lean/Elab/Deriving/Ord.lean @@ -28,17 +28,17 @@ where let type ← Core.betaReduce type -- we 'beta-reduce' to eliminate "artificial" dependencies let mut indPatterns := #[] -- add `_` pattern for indices - for _ in [:indVal.numIndices] do + for _ in *...indVal.numIndices do indPatterns := indPatterns.push (← `(_)) let mut ctorArgs1 := #[] let mut ctorArgs2 := #[] -- construct RHS top-down as continuation over the remaining comparison let mut rhsCont : Term → TermElabM Term := fun rhs => pure rhs -- add `_` for inductive parameters, they are inaccessible - for _ in [:indVal.numParams] do + for _ in *...indVal.numParams do ctorArgs1 := ctorArgs1.push (← `(_)) ctorArgs2 := ctorArgs2.push (← `(_)) - for i in [:ctorInfo.numFields] do + for i in *...ctorInfo.numFields do let x := xs[indVal.numParams + i]! if type.containsFVar x.fvarId! || (←isProp (←inferType x)) then -- If resulting type depends on this field or is a proof, we don't need to compare @@ -78,7 +78,7 @@ def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM Command := do def mkMutualBlock (ctx : Context) : TermElabM Syntax := do let mut auxDefs := #[] - for i in [:ctx.typeInfos.size] do + for i in *...ctx.typeInfos.size do auxDefs := auxDefs.push (← mkAuxFunction ctx i) `(mutual set_option match.ignoreUnusedAlts true diff --git a/src/Lean/Elab/Deriving/Repr.lean b/src/Lean/Elab/Deriving/Repr.lean index 076a74ebcc..9b6a24e736 100644 --- a/src/Lean/Elab/Deriving/Repr.lean +++ b/src/Lean/Elab/Deriving/Repr.lean @@ -29,7 +29,7 @@ def mkBodyForStruct (header : Header) (indVal : InductiveVal) : TermElabM Term : let mut fields ← `(Format.nil) if xs.size != numParams + fieldNames.size then throwError "'deriving Repr' failed, unexpected number of fields in structure" - for h : i in [:fieldNames.size] do + for h : i in *...fieldNames.size do let fieldName := fieldNames[i] let fieldNameLit := Syntax.mkStrLit (toString fieldName) let x := xs[numParams + i]! @@ -54,12 +54,12 @@ where let alt ← forallTelescopeReducing ctorInfo.type fun xs _ => do let mut patterns := #[] -- add `_` pattern for indices - for _ in [:indVal.numIndices] do + for _ in *...indVal.numIndices do patterns := patterns.push (← `(_)) let mut ctorArgs := #[] let mut rhs : Term := Syntax.mkStrLit (toString ctorInfo.name) rhs ← `(Format.text $rhs) - for h : i in [:xs.size] do + for h : i in *...xs.size do -- Note: some inductive parameters are explicit if they were promoted from indices, -- so we process all constructor arguments in the same loop. let x := xs[i] @@ -103,7 +103,7 @@ def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM Command := do def mkMutualBlock (ctx : Context) : TermElabM Syntax := do let mut auxDefs := #[] - for i in [:ctx.typeInfos.size] do + for i in *...ctx.typeInfos.size do auxDefs := auxDefs.push (← mkAuxFunction ctx i) `(mutual $auxDefs:command* diff --git a/src/Lean/Elab/Deriving/ToExpr.lean b/src/Lean/Elab/Deriving/ToExpr.lean index 21f7aaf85c..bca54e85f1 100644 --- a/src/Lean/Elab/Deriving/ToExpr.lean +++ b/src/Lean/Elab/Deriving/ToExpr.lean @@ -81,7 +81,7 @@ where let alt ← forallTelescopeReducing ctorInfo.type fun xs _ => do let mut patterns := #[] -- add `_` pattern for indices, before the constructor's pattern - for _ in [:indVal.numIndices] do + for _ in *...indVal.numIndices do patterns := patterns.push (← `(_)) let mut ctorArgs := #[] let mut rhsArgs : Array Term := #[] @@ -93,11 +93,11 @@ where else ``(toExpr $a) -- add `_` pattern for inductive parameters, which are inaccessible - for i in [:ctorInfo.numParams] do + for i in *...ctorInfo.numParams do let a := mkIdent header.argNames[i]! ctorArgs := ctorArgs.push (← `(_)) rhsArgs := rhsArgs.push <| ← mkArg xs[i]! a - for i in [:ctorInfo.numFields] do + for i in *...ctorInfo.numFields do let a := mkIdent (← mkFreshUserName `a) ctorArgs := ctorArgs.push a rhsArgs := rhsArgs.push <| ← mkArg xs[ctorInfo.numParams + i]! a @@ -178,7 +178,7 @@ Wraps the resulting definition commands in `mutual ... end`. -/ def mkAuxFunctions (ctx : Deriving.Context) : TermElabM Syntax := do let mut auxDefs := #[] - for i in [:ctx.typeInfos.size] do + for i in *...ctx.typeInfos.size do auxDefs := auxDefs.push (← mkAuxFunction ctx i) `(mutual $auxDefs:command* end) diff --git a/src/Lean/Elab/Deriving/Util.lean b/src/Lean/Elab/Deriving/Util.lean index 214d556f9d..90ebe929cf 100644 --- a/src/Lean/Elab/Deriving/Util.lean +++ b/src/Lean/Elab/Deriving/Util.lean @@ -49,7 +49,7 @@ invoking ``mkInstImplicitBinders `BarClass foo #[`α, `n, `β]`` gives `` `([Bar def mkInstImplicitBinders (className : Name) (indVal : InductiveVal) (argNames : Array Name) : TermElabM (Array Syntax) := forallBoundedTelescope indVal.type indVal.numParams fun xs _ => do let mut binders := #[] - for h : i in [:xs.size] do + for h : i in *...xs.size do try let x := xs[i] let c ← mkAppM className #[x] @@ -86,7 +86,7 @@ def mkContext (fnPrefix : String) (typeName : Name) : TermElabM Context := do def mkLocalInstanceLetDecls (ctx : Context) (className : Name) (argNames : Array Name) : TermElabM (Array (TSyntax ``Parser.Term.letDecl)) := do let mut letDecls := #[] - for h : i in [:ctx.typeInfos.size] do + for h : i in *...ctx.typeInfos.size do let indVal := ctx.typeInfos[i] let auxFunName := ctx.auxFunNames[i]! let currArgNames ← mkInductArgNames indVal @@ -109,7 +109,7 @@ def mkLet (letDecls : Array (TSyntax ``Parser.Term.letDecl)) (body : Term) : Ter open TSyntax.Compat in def mkInstanceCmds (ctx : Context) (className : Name) (typeNames : Array Name) (useAnonCtor := true) : TermElabM (Array Command) := do let mut instances := #[] - for i in [:ctx.typeInfos.size] do + for i in *...ctx.typeInfos.size do let indVal := ctx.typeInfos[i]! if typeNames.contains indVal.name then let auxFunName := ctx.auxFunNames[i]! @@ -140,7 +140,7 @@ def mkHeader (className : Name) (arity : Nat) (indVal : InductiveVal) : TermElab let binders ← mkImplicitBinders argNames let targetType ← mkInductiveApp indVal argNames let mut targetNames := #[] - for _ in [:arity] do + for _ in *...arity do targetNames := targetNames.push (← mkFreshUserName `x) let binders := binders ++ (← mkInstImplicitBinders className indVal argNames) let binders := binders ++ (← targetNames.mapM fun targetName => `(explicitBinderF| ($(mkIdent targetName) : $targetType))) diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean index e92517a8f3..8f5cfffbd4 100644 --- a/src/Lean/Elab/Inductive.lean +++ b/src/Lean/Elab/Inductive.lean @@ -240,7 +240,7 @@ where if indFVars.contains f then let mut args := e.getAppArgs -- Prefer throwing an "argument mismatch" error rather than a "missing parameter" one - for i in [:min args.size params.size] do + for i in *...min args.size params.size do let param := params[i]! let arg := args[i]! unless (← isDefEq param arg) do diff --git a/src/Lean/Elab/LetRec.lean b/src/Lean/Elab/LetRec.lean index 2d7d536f3d..16328235c4 100644 --- a/src/Lean/Elab/LetRec.lean +++ b/src/Lean/Elab/LetRec.lean @@ -89,7 +89,7 @@ private def elabLetRecDeclValues (view : LetRecView) : TermElabM (Array Expr) := view.decls.mapM fun view => do forallBoundedTelescope view.type view.binderIds.size fun xs type => do -- Add new info nodes for new fvars. The server will detect all fvars of a binder by the binder's source location. - for h : i in [0:view.binderIds.size] do + for h : i in *...view.binderIds.size do addLocalVarInfo view.binderIds[i] xs[i]! withDeclName view.declName do withInfoContext' view.valStx diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean index 4e94721ea7..dd2d6c06e1 100644 --- a/src/Lean/Elab/Match.lean +++ b/src/Lean/Elab/Match.lean @@ -295,12 +295,12 @@ where matchConstInduct t.getAppFn (fun _ => failure) fun info _ => do let tArgs := t.getAppArgs let dArgs := d.getAppArgs - for i in [:info.numParams] do + for i in *...info.numParams do let tArg := tArgs[i]! let dArg := dArgs[i]! unless (← isDefEq tArg dArg) do return i :: (← goType tArg dArg) - for h : i in [info.numParams : tArgs.size] do + for h : i in info.numParams...tArgs.size do let tArg := tArgs[i] let dArg := dArgs[i]! unless (← isDefEq tArg dArg) do @@ -318,12 +318,12 @@ where matchConstCtor t.getAppFn (fun _ => failure) fun info _ => do let tArgs := t.getAppArgs let dArgs := d.getAppArgs - for i in [:info.numParams] do + for i in *...info.numParams do let tArg := tArgs[i]! let dArg := dArgs[i]! unless (← isDefEq tArg dArg) do failure - for i in [info.numParams : tArgs.size] do + for i in info.numParams...tArgs.size do let tArg := tArgs[i]! let dArg := dArgs[i]! unless (← isDefEq tArg dArg) do @@ -356,13 +356,13 @@ private def elabPatterns (patternStxs : Array Syntax) (numDiscrs : Nat) (matchTy logIncorrectNumberOfPatternsAt (← getRef) "Not enough" numDiscrs patternStxs.size patternStxs.toList let numHoles := numDiscrs - patternStxs.size let mut extraStxs := Array.emptyWithCapacity numHoles - for _ in [:numHoles] do + for _ in *...numHoles do extraStxs := extraStxs.push (← `(_)) patternStxs := patternStxs ++ extraStxs else if patternStxs.size > numDiscrs then throwIncorrectNumberOfPatternsAt (← getRef) "Too many" numDiscrs patternStxs.size patternStxs.toList - for h : idx in [:patternStxs.size] do + for h : idx in *...patternStxs.size do let patternStx := patternStxs[idx] matchType ← whnf matchType match matchType with diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index 60abd4e746..e5c13fe20b 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/src/Lean/Elab/MutualDef.lean @@ -508,7 +508,7 @@ private def elabFunValues (headers : Array DefViewElabHeader) (vars : Array Expr (if header.kind.isTheorem && !deprecated.oldSectionVars.get (← getOptions) then withHeaderSecVars vars sc #[header] else fun x => x #[]) fun vars => do forallBoundedTelescope header.type header.numParams fun xs type => do -- Add new info nodes for new fvars. The server will detect all fvars of a binder by the binder's source location. - for h : i in [0:header.binderIds.size] do + for h : i in *...header.binderIds.size do -- skip auto-bound prefix in `xs` addLocalVarInfo header.binderIds[i] xs[header.numParams - header.binderIds.size + i]! let val ← if (← useProofAsSorry header.kind) then @@ -945,7 +945,7 @@ private def mkLetRecClosures (sectionVars : Array Expr) (mainFVarIds : Array FVa let mut letRecsToLift := letRecsToLift let mut freeVarMap ← mkFreeVarMap sectionVars mainFVarIds recFVarIds letRecsToLift let mut result := #[] - for i in [:letRecsToLift.size] do + for i in *...letRecsToLift.size do if letRecsToLift[i]!.val.hasExprMVar then -- This can happen when this particular let-rec has nested let-rec that have been resolved in previous iterations. -- This code relies on the fact that nested let-recs occur before the outer most let-recs at `letRecsToLift`. @@ -1352,7 +1352,7 @@ def elabMutualDef (ds : Array Syntax) : CommandElabM Unit := do let mut views := #[] let mut defs := #[] let mut reusedAllHeaders := true - for h : i in [0:ds.size], headerPromise in headerPromises do + for h : i in *...ds.size, headerPromise in headerPromises do let d := ds[i] let modifiers ← elabModifiers ⟨d[0]⟩ if ds.size > 1 && modifiers.isNonrec then diff --git a/src/Lean/Elab/MutualInductive.lean b/src/Lean/Elab/MutualInductive.lean index f4f0ca78bf..25b46e96dd 100644 --- a/src/Lean/Elab/MutualInductive.lean +++ b/src/Lean/Elab/MutualInductive.lean @@ -386,7 +386,7 @@ private def computeFixedIndexBitMask (numParams : Nat) (indType : InductiveType) | ctor :: ctors => forallTelescopeReducing ctor.type fun xs type => do let typeArgs := type.getAppArgs - for i in [numParams:arity] do + for i in numParams...arity do unless i < xs.size && xs[i]! == typeArgs[i]! do -- Remark: if we want to allow arguments to be rearranged, this test should be xs.contains typeArgs[i] maskRef.modify fun mask => mask.set! i false for x in xs[numParams...*] do @@ -394,7 +394,7 @@ private def computeFixedIndexBitMask (numParams : Nat) (indType : InductiveType) let cond (e : Expr) := indFVars.any (fun indFVar => e.getAppFn == indFVar) xType.forEachWhere (stopWhenVisited := true) cond fun e => do let eArgs := e.getAppArgs - for i in [numParams:eArgs.size] do + for i in numParams...eArgs.size do if i >= typeArgs.size then maskRef.modify (resetMaskAt · i) else @@ -411,7 +411,7 @@ private def computeFixedIndexBitMask (numParams : Nat) (indType : InductiveType) ``` because `i` doesn't appear in `All Iμ []`, the index shouldn't be fixed. -/ - for i in [eArgs.size:arity] do + for i in eArgs.size...arity do maskRef.modify (resetMaskAt · i) go ctors go indType.ctors @@ -762,7 +762,7 @@ private def checkResultingUniverses (views : Array InductiveView) (elabs' : Arra let u := (← instantiateLevelMVars (← getResultingUniverse indTypes)).normalize checkResultingUniversePolymorphism views u numParams indTypes unless u.isZero do - for h : i in [0:indTypes.length] do + for h : i in *...indTypes.length do let indType := indTypes[i] -- See if there is a custom error. If so, this should throw an error first: elabs'[i]!.checkUniverses numParams u @@ -813,7 +813,7 @@ private def collectLevelParamsInInductive (indTypes : List InductiveType) : Arra private def mkIndFVar2Const (views : Array InductiveView) (indFVars : Array Expr) (levelNames : List Name) : ExprMap Expr := Id.run do let levelParams := levelNames.map mkLevelParam; let mut m : ExprMap Expr := {} - for h : i in [:views.size] do + for h : i in *...views.size do let view := views[i] let indFVar := indFVars[i]! m := m.insert indFVar (mkConst view.declName levelParams) @@ -865,7 +865,7 @@ private def mkInductiveDecl (vars : Array Expr) (elabs : Array InductiveElabStep let rs := Array.zipWith (fun r indFVar => { r with indFVar : ElabHeaderResult }) rs indFVars let mut indTypesArray : Array InductiveType := #[] let mut elabs' := #[] - for h : i in [:views.size] do + for h : i in *...views.size do Term.addLocalVarInfo views[i].declId indFVars[i]! let r := rs[i]! let elab' ← elabs[i]!.elabCtors rs r params diff --git a/src/Lean/Elab/PatternVar.lean b/src/Lean/Elab/PatternVar.lean index f0887b4dc5..07a1093526 100644 --- a/src/Lean/Elab/PatternVar.lean +++ b/src/Lean/Elab/PatternVar.lean @@ -180,8 +180,9 @@ private def processVar (idStx : Syntax) : M Syntax := do private def samePatternsVariables (startingAt : Nat) (s₁ s₂ : State) : Bool := Id.run do if h₁ : s₁.vars.size = s₂.vars.size then - for h₂ : i in [startingAt:s₁.vars.size] do - if s₁.vars[i] != s₂.vars[i]'(by obtain ⟨_, y⟩ := h₂; simp_all +zetaDelta) then return false + for h₂ : i in startingAt...s₁.vars.size do + if s₁.vars[i] != s₂.vars[i]'(by have y := Std.PRange.lt_upper_of_mem h₂; simp_all +zetaDelta) then + return false true else false diff --git a/src/Lean/Elab/PreDefinition/Basic.lean b/src/Lean/Elab/PreDefinition/Basic.lean index e4b131c6b2..52b474ea4d 100644 --- a/src/Lean/Elab/PreDefinition/Basic.lean +++ b/src/Lean/Elab/PreDefinition/Basic.lean @@ -290,7 +290,7 @@ def checkCodomainsLevel (preDefs : Array PreDefinition) : MetaM Unit := do lambdaTelescope preDef.value fun xs _ => return xs.size forallBoundedTelescope preDefs[0]!.type arities[0]! fun _ type₀ => do let u₀ ← getLevel type₀ - for h : i in [1:preDefs.size] do + for h : i in 1...preDefs.size do forallBoundedTelescope preDefs[i].type arities[i]! fun _ typeᵢ => unless ← isLevelDefEq u₀ (← getLevel typeᵢ) do withOptions (fun o => pp.sanitizeNames.set o false) do @@ -307,7 +307,7 @@ def shareCommonPreDefs (preDefs : Array PreDefinition) : CoreM (Array PreDefinit es := es.push preDef.type |>.push preDef.value es := ShareCommon.shareCommon' es let mut result := #[] - for h : i in [:preDefs.size] do + for h : i in *...preDefs.size do let preDef := preDefs[i] result := result.push { preDef with type := es[2*i]!, value := es[2*i+1]! } return result diff --git a/src/Lean/Elab/PreDefinition/Eqns.lean b/src/Lean/Elab/PreDefinition/Eqns.lean index 651510bb7d..f35384f1c1 100644 --- a/src/Lean/Elab/PreDefinition/Eqns.lean +++ b/src/Lean/Elab/PreDefinition/Eqns.lean @@ -57,7 +57,7 @@ private def findMatchToSplit? (deepRecursiveSplit : Bool) (env : Environment) (e let args := e.getAppArgs -- If none of the discriminants is a free variable, then it is not worth splitting the match let mut hasFVarDiscr := false - for i in [info.getFirstDiscrPos : info.getFirstDiscrPos + info.numDiscrs] do + for i in info.getFirstDiscrPos...(info.getFirstDiscrPos + info.numDiscrs) do let discr := args[i]! if discr.isFVar then hasFVarDiscr := true @@ -72,7 +72,7 @@ private def findMatchToSplit? (deepRecursiveSplit : Bool) (env : Environment) (e return Expr.FindStep.found -- Else, the “old” behavior is split only when at least one alternative contains a `declNames` -- application with loose bound variables. - for i in [info.getFirstAltPos : info.getFirstAltPos + info.numAlts] do + for i in info.getFirstAltPos...(info.getFirstAltPos + info.numAlts) do let alt := args[i]! if Option.isSome <| alt.find? fun e => declNames.any e.isAppOf && e.hasLooseBVars then return Expr.FindStep.found @@ -409,7 +409,7 @@ def mkEqns (declName : Name) (declNames : Array Name) (tryRefl := true): MetaM ( withReducible do mkEqnTypes declNames goal.mvarId! let mut thmNames := #[] - for h : i in [: eqnTypes.size] do + for h : i in *...eqnTypes.size do let type := eqnTypes[i] trace[Elab.definition.eqns] "eqnType[{i}]: {eqnTypes[i]}" let name := mkEqLikeNameFor (← getEnv) declName s!"{eqnThmSuffixBasePrefix}{i+1}" diff --git a/src/Lean/Elab/PreDefinition/FixedParams.lean b/src/Lean/Elab/PreDefinition/FixedParams.lean index 7123551673..eb42a7b92f 100644 --- a/src/Lean/Elab/PreDefinition/FixedParams.lean +++ b/src/Lean/Elab/PreDefinition/FixedParams.lean @@ -105,8 +105,8 @@ partial def Info.setVarying (funIdx paramIdx : Nat) (info : Info) : Info := Id.r -- Set this as varying info := { info with graph := info.graph.modify funIdx (·.set! paramIdx none) } -- Propagate along edges for already observed calls - for otherFunIdx in [:info.graph.size] do - for otherParamIdx in [:info.graph[otherFunIdx]!.size] do + for otherFunIdx in *...info.graph.size do + for otherParamIdx in *...info.graph[otherFunIdx]!.size do if let some otherParamInfo := info.graph[otherFunIdx]![otherParamIdx]! then if otherParamInfo[funIdx]! = some paramIdx then info := Info.setVarying otherFunIdx otherParamIdx info @@ -139,12 +139,12 @@ partial def Info.setCallerParam (calleeIdx argIdx callerIdx paramIdx : Nat) (inf -- Propagate information about the caller let mut info : Info := info if let some callerParamInfo := info.graph[callerIdx]![paramIdx]! then - for h : otherFunIdx in [:callerParamInfo.size] do + for h : otherFunIdx in *...callerParamInfo.size do if let some otherParamIdx := callerParamInfo[otherFunIdx] then info := info.setCallerParam calleeIdx argIdx otherFunIdx otherParamIdx -- Propagate information about the callee - for otherFunIdx in [:info.graph.size] do - for otherArgIdx in [:info.graph[otherFunIdx]!.size] do + for otherFunIdx in *...info.graph.size do + for otherArgIdx in *...info.graph[otherFunIdx]!.size do if let some otherArgsInfo := info.graph[otherFunIdx]![otherArgIdx]! then if let some paramIdx' := otherArgsInfo[calleeIdx]! then if paramIdx' = argIdx then @@ -175,9 +175,9 @@ open Lean Meta FixedParams def getParamRevDeps (value : Expr) : MetaM (Array (Array Nat)) := do lambdaTelescope value (cleanupAnnotations := true) fun xs _ => do let mut revDeps := #[] - for h : i in [:xs.size] do + for h : i in *...xs.size do let mut deps := #[] - for h : j in [i+1:xs.size] do + for h : j in (i+1)...xs.size do if (← dependsOn (← inferType xs[j]) xs[i].fvarId!) then deps := deps.push j revDeps := revDeps.push deps @@ -190,7 +190,7 @@ def getFixedParamsInfo (preDefs : Array PreDefinition) : MetaM FixedParams.Info ref.modify .addSelfCalls - for h : callerIdx in [:preDefs.size] do + for h : callerIdx in *...preDefs.size do let preDef := preDefs[callerIdx] lambdaTelescope preDef.value fun params body => do assert! params.size = arities[callerIdx]! @@ -202,7 +202,7 @@ def getFixedParamsInfo (preDefs : Array PreDefinition) : MetaM FixedParams.Info return .continue let n := f.constName! let some calleeIdx := preDefs.findIdx? (·.declName = n) | return .continue - for argIdx in [:arities[calleeIdx]!] do + for argIdx in *...arities[calleeIdx]! do if (← ref.get).mayBeFixed calleeIdx argIdx then if h : argIdx < args.size then let arg := args[argIdx] @@ -215,7 +215,7 @@ def getFixedParamsInfo (preDefs : Array PreDefinition) : MetaM FixedParams.Info else -- Try all parameters let mut any := false - for h : paramIdx in [:params.size] do + for h : paramIdx in *...params.size do if (← ref.get).mayBeFixed callerIdx paramIdx then let param := params[paramIdx] if (← withoutProofIrrelevance <| withReducible <| isDefEq param arg) then @@ -271,7 +271,7 @@ def getFixedParamPerms (preDefs : Array PreDefinition) : MetaM FixedParamPerms : let mut firstPerm := #[] let mut numFixed := 0 - for paramIdx in [:xs.size], x in xs, paramInfo? in paramInfos do + for paramIdx in *...xs.size, x in xs, paramInfo? in paramInfos do if let some paramInfo := paramInfo? then assert! paramInfo[0]! = some paramIdx firstPerm := firstPerm.push (some numFixed) @@ -280,7 +280,7 @@ def getFixedParamPerms (preDefs : Array PreDefinition) : MetaM FixedParamPerms : firstPerm := firstPerm.push none let mut perms := #[firstPerm] - for h : funIdx in [1:info.graph.size] do + for h : funIdx in 1...info.graph.size do let paramInfos := info.graph[funIdx] let mut perm := #[] for paramInfo? in paramInfos do @@ -397,7 +397,7 @@ Unlike `pickFixed`, this function can handle over- or under-application. -/ def FixedParamPerm.pickVarying (perm : FixedParamPerm) (xs : Array α) : Array α := Id.run do let mut ys := #[] - for h : i in [:xs.size] do + for h : i in *...xs.size do if perm[i]?.join.isNone then ys := ys.push xs[i] pure ys @@ -453,7 +453,7 @@ def FixedParamPerms.erase (fixedParamPerms : FixedParamPerms) (xs : Array Expr) assert! toErase.size = fixedParamPerms.perms.size -- Calculate a mask on the fixed parameters of variables to erase let mut mask := Array.replicate fixedParamPerms.numFixed false - for funIdx in [:toErase.size], paramIdxs in toErase, mapping in fixedParamPerms.perms do + for funIdx in *...toErase.size, paramIdxs in toErase, mapping in fixedParamPerms.perms do for paramIdx in paramIdxs do assert! paramIdx < mapping.size if let some fixedParamIdx := mapping[paramIdx]! then @@ -462,8 +462,8 @@ def FixedParamPerms.erase (fixedParamPerms : FixedParamPerms) (xs : Array Expr) let mut changed := true while changed do changed := false - for h : funIdx in [:fixedParamPerms.perms.size] do - for h : paramIdx₁ in [:fixedParamPerms.perms[funIdx].size] do + for h : funIdx in *...fixedParamPerms.perms.size do + for h : paramIdx₁ in *...fixedParamPerms.perms[funIdx].size do if let some fixedParamIdx₁ := fixedParamPerms.perms[funIdx][paramIdx₁] then if mask[fixedParamIdx₁]! then for paramIdx₂ in fixedParamPerms.revDeps[funIdx]![paramIdx₁]! do @@ -475,7 +475,7 @@ def FixedParamPerms.erase (fixedParamPerms : FixedParamPerms) (xs : Array Expr) let mut reindex := #[] let mut fvarsToErase :=#[] let mut toKeep :=#[] - for i in [:mask.size], erase in mask, x in xs do + for i in *...mask.size, erase in mask, x in xs do if erase then reindex := reindex.push none fvarsToErase := fvarsToErase.push x.fvarId! diff --git a/src/Lean/Elab/PreDefinition/Structural/Basic.lean b/src/Lean/Elab/PreDefinition/Structural/Basic.lean index ff21d94f45..904f4e3cc2 100644 --- a/src/Lean/Elab/PreDefinition/Structural/Basic.lean +++ b/src/Lean/Elab/PreDefinition/Structural/Basic.lean @@ -71,7 +71,7 @@ def Positions.numIndices (positions : Positions) : Nat := -/ def Positions.inverse (positions : Positions) : Array Nat := Id.run do let mut r := .replicate positions.numIndices 0 - for _h : i in [:positions.size] do + for _h : i in *...positions.size do for k in positions[i] do r := r.set! k i return r diff --git a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean b/src/Lean/Elab/PreDefinition/Structural/Eqns.lean index 8f71a84802..31ba9a5a3b 100644 --- a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean +++ b/src/Lean/Elab/PreDefinition/Structural/Eqns.lean @@ -80,7 +80,7 @@ def mkEqns (info : EqnInfo) : MetaM (Array Name) := let goal ← mkFreshExprSyntheticOpaqueMVar target mkEqnTypes info.declNames goal.mvarId! let mut thmNames := #[] - for h : i in [: eqnTypes.size] do + for h : i in *...eqnTypes.size do let type := eqnTypes[i] trace[Elab.definition.structural.eqns] "eqnType {i+1}: {type}" let name := mkEqLikeNameFor (← getEnv) info.declName s!"{eqnThmSuffixBasePrefix}{i+1}" diff --git a/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean b/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean index 85c18f0ee4..a87a830075 100644 --- a/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean +++ b/src/Lean/Elab/PreDefinition/Structural/FindRecArg.lean @@ -127,7 +127,7 @@ def getRecArgInfos (fnName : Name) (fixedParamPerm : FixedParamPerm) (xs : Array let mut recArgInfos := #[] let mut report : MessageData := m!"" -- No `termination_by`, so try all, and remember the errors - for idx in [:args.size] do + for idx in *...args.size do try let recArgInfo ← getRecArgInfo fnName fixedParamPerm args idx recArgInfos := recArgInfos.push recArgInfo @@ -192,7 +192,7 @@ def argsInGroup (group : IndGroupInst) (xs : Array Expr) (value : Expr) if nestedTypeFormers.isEmpty then return .none lambdaTelescope value fun ys _ => do let x := (xs++ys)[recArgInfo.recArgPos]! - for nestedTypeFormer in nestedTypeFormers, indIdx in [group.all.size : group.numMotives] do + for nestedTypeFormer in nestedTypeFormers, indIdx in group.all.size...group.numMotives do let xType ← whnfD (← inferType x) let (indIndices, _, type) ← forallMetaTelescope nestedTypeFormer if (← isDefEqGuarded type xType) then diff --git a/src/Lean/Elab/PreDefinition/Structural/RecArgInfo.lean b/src/Lean/Elab/PreDefinition/Structural/RecArgInfo.lean index 4e073eda4d..10225d0b78 100644 --- a/src/Lean/Elab/PreDefinition/Structural/RecArgInfo.lean +++ b/src/Lean/Elab/PreDefinition/Structural/RecArgInfo.lean @@ -55,7 +55,7 @@ def RecArgInfo.pickIndicesMajor (info : RecArgInfo) (xs : Array Expr) : (Array E indexMajorArgs := indexMajorArgs.push xs[j]! -- Then the other arguments, in the order they appear in `xs` let mut otherVaryingArgs := #[] - for h : i in [:xs.size] do + for h : i in *...xs.size do unless indexMajorPos.contains i do unless info.fixedParamPerm.isFixed i do otherVaryingArgs := otherVaryingArgs.push xs[i] diff --git a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean index 09c41aa21a..d9f8e23e8e 100644 --- a/src/Lean/Elab/PreDefinition/WF/GuessLex.lean +++ b/src/Lean/Elab/PreDefinition/WF/GuessLex.lean @@ -107,7 +107,7 @@ case, the user gets to keep both pieces (and may have to rename variables). partial def naryVarNames (xs : Array Name) : MetaM (Array Name) := do let mut ns : Array Name := #[] - for h : i in [:xs.size] do + for h : i in *...xs.size do let n := xs[i] let n ← if n.hasMacroScopes then freshen ns (.mkSimple s!"x{i+1}") @@ -561,7 +561,7 @@ where go (fidx : Nat) : OptionT (ReaderT (Array Nat) (StateM (Array (Array Nat)))) Unit := do if h : fidx < numMeasures.size then let n := numMeasures[fidx] - for idx in [:n] do withReader (·.push idx) (go (fidx + 1)) + for idx in *...n do withReader (·.push idx) (go (fidx + 1)) else let comb ← read unless comb.all (· == comb[0]!) do @@ -604,7 +604,7 @@ partial def solve {m} {α} [Monad m] (measures : Array α) if calls.isEmpty then return .some acc -- Find the first measure that has at least one < and otherwise only = or <= - for h : measureIdx in [:measures.size] do + for h : measureIdx in *...measures.size do let measure := measures[measureIdx] let mut has_lt := false let mut all_le := true @@ -633,20 +633,20 @@ Single space as column separator. -/ def formatTable : Array (Array String) → String := fun xss => Id.run do let mut colWidths := xss[0]!.map (fun _ => 0) - for hi : i in [:xss.size] do - for hj : j in [:xss[i].size] do + for hi : i in *...xss.size do + for hj : j in *...xss[i].size do if xss[i][j].length > colWidths[j]! then colWidths := colWidths.set! j xss[i][j].length let mut str := "" - for hi : i in [:xss.size] do - for hj : j in [:xss[i].size] do + for hi : i in *...xss.size do + for hj : j in *...xss[i].size do let s := xss[i][j] if j > 0 then -- right-align - for _ in [:colWidths[j]! - s.length] do + for _ in *...(colWidths[j]! - s.length) do str := str ++ " " str := str ++ s if j = 0 then -- left-align - for _ in [:colWidths[j]! - s.length] do + for _ in *...(colWidths[j]! - s.length) do str := str ++ " " if j + 1 < xss[i].size then str := str ++ " " @@ -691,9 +691,9 @@ def collectHeaders {α} (a : StateT (Nat × String) MetaM α) : MetaM (α × Str def explainNonMutualFailure (measures : Array BasicMeasure) (rcs : Array RecCallCache) : MetaM Format := do let (header, footer) ← collectHeaders (measures.mapM measureHeader) let mut table : Array (Array String) := #[#[""] ++ header] - for i in [:rcs.size], rc in rcs do + for i in *...rcs.size, rc in rcs do let mut row := #[s!"{i+1}) {← rc.rcc.posString}"] - for argIdx in [:measures.size] do + for argIdx in *...measures.size do row := row.push (← rc.prettyEntry argIdx argIdx) table := table.push row let out := formatTable table @@ -719,14 +719,14 @@ def explainMutualFailure (declNames : Array Name) (measuress : Array (Array Basi if caller = callee then -- For self-calls, only the diagonal is interesting, so put it into one row let mut row := #[""] - for argIdx in [:measuress[caller]!.size] do + for argIdx in *...measuress[caller]!.size do row := row.push (← rc.prettyEntry argIdx argIdx) table := table.push row else - for argIdx in [:measuress[callee]!.size] do + for argIdx in *...measuress[callee]!.size do let mut row := #[] row := row.push headerss[callee]![argIdx]! - for paramIdx in [:measuress[caller]!.size] do + for paramIdx in *...measuress[caller]!.size do row := row.push (← rc.prettyEntry paramIdx argIdx) table := table.push row r := r ++ formatTable table ++ "\n" diff --git a/src/Lean/Elab/PreDefinition/WF/Rel.lean b/src/Lean/Elab/PreDefinition/WF/Rel.lean index 3ce99c914b..aca5a9faeb 100644 --- a/src/Lean/Elab/PreDefinition/WF/Rel.lean +++ b/src/Lean/Elab/PreDefinition/WF/Rel.lean @@ -26,7 +26,7 @@ This ensures the preconditions for `ArgsPacker.uncurryND`. def checkCodomains (names : Array Name) (fixedParamPerms : FixedParamPerms) (fixedArgs : Array Expr) (arities : Array Nat) (termMeasures : TerminationMeasures) : TermElabM Expr := do let mut codomains := #[] - for name in names, funIdx in [:names.size], arity in arities, termMeasure in termMeasures do + for name in names, funIdx in *...names.size, arity in arities, termMeasure in termMeasures do let measureType ← inferType termMeasure.fn let measureType ← fixedParamPerms.perms[funIdx]!.instantiateForall measureType fixedArgs let codomain ← forallBoundedTelescope measureType arity fun xs codomain => do @@ -40,7 +40,7 @@ def checkCodomains (names : Array Name) (fixedParamPerms : FixedParamPerms) (fix codomains := codomains.push codomain let codomain0 := codomains[0]! - for h : i in [1 : codomains.size] do + for h : i in 1...codomains.size do unless ← isDefEqGuarded codomain0 codomains[i] do throwErrorAt termMeasures[i]!.ref m!"The termination measures of mutually recursive functions " ++ m!"must have the same return type, but the termination measure of {names[0]!} has type" ++ diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean index af8d7ed157..9e1cbf1a75 100644 --- a/src/Lean/Elab/Quotation.lean +++ b/src/Lean/Elab/Quotation.lean @@ -655,7 +655,7 @@ The parameter `alts` provides position information for alternatives. -/ private def checkUnusedAlts (stx : Syntax) (alts : Array Syntax) (altIdxMap : NameMap Nat) (ignoreIfUnused : IdxSet) : TermElabM Syntax := do let (stx, used) ← findUsedAlts stx altIdxMap - for h : i in [:alts.size] do + for h : i in *...alts.size do unless used.contains i || ignoreIfUnused.contains i do logErrorAt alts[i] s!"redundant alternative #{i+1}" return stx diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean index afec44d7ec..ead52a5bea 100644 --- a/src/Lean/Elab/StructInst.lean +++ b/src/Lean/Elab/StructInst.lean @@ -407,7 +407,7 @@ private def mkCtorHeader (ctorVal : ConstructorVal) (structureType? : Option Exp let mut type ← instantiateTypeLevelParams cinfo.toConstantVal us let mut params : Array Expr := #[] let mut instMVars : Array MVarId := #[] - for _ in [0 : ctorVal.numParams] do + for _ in *...ctorVal.numParams do let .forallE _ d b bi := type | throwError "unexpected constructor type" let param ← diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean index 8c0c0e7521..66fb6c8491 100644 --- a/src/Lean/Elab/Structure.lean +++ b/src/Lean/Elab/Structure.lean @@ -909,7 +909,7 @@ Returns the binder list without these updates along with the new binder infos fo -/ private def elabParamInfoUpdates (structParams : Array Expr) (binders : Array Syntax) : StructElabM (Array Syntax × ExprMap (Syntax × BinderInfo)) := do let mut overrides : ExprMap (Syntax × BinderInfo) := {} - for i in [0:binders.size] do + for i in *...binders.size do match typelessBinder? binders[i]! with | none => return (binders.extract i, overrides) | some (ids, bi) => @@ -1225,7 +1225,7 @@ private def resolveFieldDefaults (structName : Name) : StructElabM Unit := do -- We will do that in `checkResolutionOrder`, which is after the structure is registered. let { resolutionOrder, .. } ← mergeStructureResolutionOrders structName ((← get).parents.map (·.structName)) (relaxed := true) let mut resOrderMap : NameMap Nat := {} - for h : i in [0:resolutionOrder.size] do + for h : i in *...resolutionOrder.size do resOrderMap := resOrderMap.insert resolutionOrder[i] i for fieldInfo in (← get).fields do if fieldInfo.default?.isSome then diff --git a/src/Lean/Elab/SyntheticMVars.lean b/src/Lean/Elab/SyntheticMVars.lean index 02effa1401..6c4be75574 100644 --- a/src/Lean/Elab/SyntheticMVars.lean +++ b/src/Lean/Elab/SyntheticMVars.lean @@ -150,7 +150,7 @@ where -- Succeeded. Collect new TC problems trace[Elab.defaultInstance] "isDefEq worked {mkMVar mvarId} : {← inferType (mkMVar mvarId)} =?= {candidate} : {← inferType candidate}" let mut pending := [] - for h : i in [:bis.size] do + for h : i in *...bis.size do if bis[i] == BinderInfo.instImplicit then pending := mvars[i]!.mvarId! :: pending synthesizePending pending @@ -266,7 +266,7 @@ private def throwStuckAtUniverseCnstr : TermElabM Unit := do unless found.contains (lhs, rhs) do found := found.insert (lhs, rhs) uniqueEntries := uniqueEntries.push entry - for h : i in [1:uniqueEntries.size] do + for h : i in 1...uniqueEntries.size do logErrorAt uniqueEntries[i].ref (← mkLevelStuckErrorMessage uniqueEntries[i]!) throwErrorAt uniqueEntries[0]!.ref (← mkLevelStuckErrorMessage uniqueEntries[0]!) diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/AC.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/AC.lean index 3cd5d0738a..6c5cdd88e9 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/AC.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/AC.lean @@ -220,7 +220,7 @@ def CoefficientsMap.toExpr (coeff : CoefficientsMap) (op : Op) : VarStateM (Opti let mut acc : Option Expr := none for (var, coeff) in coeffArr do let expr := (← get).varToExpr[var]! - for _ in [0:coeff] do + for _ in *...coeff do acc := match acc with | none => expr | some acc => some <| mkApp2 op.toExpr acc expr diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Structures.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Structures.lean index a40e78b5e9..03a169ca1f 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Structures.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Structures.lean @@ -49,7 +49,7 @@ def addStructureSimpLemmas (simprocs : Simprocs) (lemmas : SimpTheoremsArray) : lemmas ← lemmas.addTheorem (.decl lemmaName) (mkConst lemmaName) let fields := (getStructureInfo env const).fieldNames.size let numParams := constInfo.numParams - for proj in [0:fields] do + for proj in *...fields do -- We use the simprocs with pre such that we push in projections eagerly in order to -- potentially not have to simplify complex structure expressions that we only project one -- element out of. diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/TypeAnalysis.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/TypeAnalysis.lean index d39ce5a4d9..a24d9cacfa 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/TypeAnalysis.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/TypeAnalysis.lean @@ -77,7 +77,7 @@ def isSupportedMatch (declName : Name) : MetaM (Option MatchKind) := do -- Check that all parameters except the last are `h_n EnumInductive.ctor` let numConcreteCases := xs.size - 3 -- minus motive, discr and default case let mut handledCtors := Array.mkEmpty (xs.size - 3) - for i in [0:numConcreteCases] do + for i in *...numConcreteCases do let argType ← inferType xs[i + 2]! let some (.const ``Unit [], (.app m (.const c ..))) := argType.arrow? | return none if m != motive then return none @@ -103,7 +103,7 @@ where (numCtors : Nat) (motive : Expr) : MetaM (Option MatchKind) := do -- Check that all parameters are `h_n EnumInductive.ctor` let mut handledCtors := Array.mkEmpty numCtors - for i in [0:numCtors] do + for i in *...numCtors do let argType ← inferType xs[i + 2]! let some (.const ``Unit [], (.app m (.const c ..))) := argType.arrow? | return none if m != motive then return none @@ -138,7 +138,7 @@ where if !(← verifySimpleCasesOnApp inductiveInfo fn args params) then return false -- remaining arguments are of the form `(h_n Unit.unit)` - for i in [0:inductiveInfo.numCtors] do + for i in *...inductiveInfo.numCtors do let .app fn (.const ``Unit.unit []) := args[i + 2]! | return false let some (_, .app _ (.const relevantCtor ..)) := (← inferType fn).arrow? | unreachable! let some ctorIdx := ctors.findIdx? (·.name == relevantCtor) | unreachable! @@ -157,7 +157,7 @@ where - `(h_n Unit.unit)` if the constructor is handled explicitly - `(h_n InductiveEnum.ctor)` if the constructor is handled as part of the default case -/ - for i in [0:inductiveInfo.numCtors] do + for i in *...inductiveInfo.numCtors do let .app fn (.const argName ..) := args[i + 2]! | return false if argName == ``Unit.unit then let some (_, .app _ (.const relevantCtor ..)) := (← inferType fn).arrow? | unreachable! diff --git a/src/Lean/Elab/Tactic/BVDecide/LRAT/Trim.lean b/src/Lean/Elab/Tactic/BVDecide/LRAT/Trim.lean index d8b84e111b..cd7f3f0ba0 100644 --- a/src/Lean/Elab/Tactic/BVDecide/LRAT/Trim.lean +++ b/src/Lean/Elab/Tactic/BVDecide/LRAT/Trim.lean @@ -196,7 +196,7 @@ def mapping : M (Array IntAction) := do let initialId ← M.getInitialId let mut nextMapped := initialId let mut newProof := #[] - for id in [initialId:emptyId+1] do + for id in initialId...=emptyId do if ← M.isUsed id then M.registerIdMap id nextMapped -- This should never panic as the use def analysis has already marked this step as being used diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean index f572d27238..b8de6dcd5b 100644 --- a/src/Lean/Elab/Tactic/BuiltinTactic.lean +++ b/src/Lean/Elab/Tactic/BuiltinTactic.lean @@ -469,7 +469,7 @@ def renameInaccessibles (mvarId : MVarId) (hs : TSyntaxArray ``binderIdent) : Ta | `(binderIdent| $h:ident) => some <| extractMacroScopes h.getId | _ => none) | return mvarId - for i in [:n] do + for i in *...n do let j := n - i - 1 match lctx.getAt? j with | none => pure () diff --git a/src/Lean/Elab/Tactic/Conv/Basic.lean b/src/Lean/Elab/Tactic/Conv/Basic.lean index 8a5879e002..409a70d2a0 100644 --- a/src/Lean/Elab/Tactic/Conv/Basic.lean +++ b/src/Lean/Elab/Tactic/Conv/Basic.lean @@ -100,7 +100,7 @@ def changeLhs (lhs' : Expr) : TacticM Unit := do /-- Evaluate `sepByIndent conv "; " -/ def evalSepByIndentConv (stx : Syntax) : TacticM Unit := do - for arg in stx.getArgs, i in [:stx.getArgs.size] do + for arg in stx.getArgs, i in *...stx.getArgs.size do if i % 2 == 0 then evalTactic arg else diff --git a/src/Lean/Elab/Tactic/Conv/Congr.lean b/src/Lean/Elab/Tactic/Conv/Congr.lean index 0794d864ba..d2fe022a58 100644 --- a/src/Lean/Elab/Tactic/Conv/Congr.lean +++ b/src/Lean/Elab/Tactic/Conv/Congr.lean @@ -34,7 +34,7 @@ private partial def mkCongrThm (origTag : Name) (f : Expr) (args : Array Expr) ( let mut proof := congrThm.proof let mut mvarIdsNew := #[] let mut mvarIdsNewInsts := #[] - for h : i in [:congrThm.argKinds.size] do + for h : i in *...congrThm.argKinds.size do let arg := args[i]! let argInfo := funInfo.paramInfo[i]! match congrThm.argKinds[i] with @@ -124,7 +124,7 @@ private partial def mkCongrArgZeroThm (tacticName : String) (origTag : Name) (f let mut proof := congrThm.proof let mut mvarIdNew? := none let mut mvarIdsNewInsts := #[] - for h : i in [:congrThm.argKinds.size] do + for h : i in *...congrThm.argKinds.size do let arg := args[i]! let argInfo := funInfo.paramInfo[i]! match congrThm.argKinds[i] with @@ -207,7 +207,7 @@ where let mut fType ← inferType f let mut j := 0 let mut explicitIdxs := #[] - for k in [0:xs.size] do + for k in *...xs.size do unless fType.isForall do fType ← withTransparency .all <| whnf (fType.instantiateRevRange j k xs) j := k @@ -332,7 +332,7 @@ private def ext (userName? : Option Name) : TacticM Unit := do -- show initial state up to (incl.) `[` withTacticInfoContext (mkNullNode #[token, lbrak]) (pure ()) let numEnterArgs := (enterArgsAndSeps.size + 1) / 2 - for i in [:numEnterArgs] do + for i in *...numEnterArgs do let enterArg := enterArgsAndSeps[2 * i]! let sep := enterArgsAndSeps.getD (2 * i + 1) .missing -- show state up to (incl.) next `,` and show errors on `enterArg` diff --git a/src/Lean/Elab/Tactic/Do/ProofMode/MGoal.lean b/src/Lean/Elab/Tactic/Do/ProofMode/MGoal.lean index a18459b7ff..5bd491c9a5 100644 --- a/src/Lean/Elab/Tactic/Do/ProofMode/MGoal.lean +++ b/src/Lean/Elab/Tactic/Do/ProofMode/MGoal.lean @@ -135,7 +135,7 @@ def betaPreservingHypNames (σs' e : Expr) (args : Array Expr) : Expr := def dropStateList (σs : Expr) (n : Nat) : MetaM Expr := do let mut σs := σs - for _ in [:n] do + for _ in *...n do let some (_type, _σ, σs') := (← whnfR σs).app3? ``List.cons | throwError "Ambient state list not a cons {σs}" σs := σs' return σs diff --git a/src/Lean/Elab/Tactic/ElabTerm.lean b/src/Lean/Elab/Tactic/ElabTerm.lean index a3282f98fe..2d8ae05810 100644 --- a/src/Lean/Elab/Tactic/ElabTerm.lean +++ b/src/Lean/Elab/Tactic/ElabTerm.lean @@ -379,7 +379,7 @@ private partial def blameDecideReductionFailure (inst : Expr) : MetaM Expr := wi if let some info ← getMatcherInfo? c then if inst.getAppNumArgs == info.arity then let args := inst.getAppArgs - for i in [0:info.numDiscrs] do + for i in *...info.numDiscrs do let inst' := args[info.numParams + 1 + i]! if (← Meta.isClass? (← inferType inst')) == ``Decidable then let inst'' ← whnf inst' diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean index 1551280bba..2b19bb1735 100644 --- a/src/Lean/Elab/Tactic/Induction.lean +++ b/src/Lean/Elab/Tactic/Induction.lean @@ -266,7 +266,7 @@ private def isWildcard (altStx : Syntax) : Bool := private def checkAltNames (alts : Array Alt) (altsSyntax : Array Syntax) : TacticM Unit := do let mut seenNames : Array Name := #[] - for h : i in [:altsSyntax.size] do + for h : i in *...altsSyntax.size do let altStx := altsSyntax[i] if getAltName altStx == `_ && i != altsSyntax.size - 1 then withRef altStx <| throwError "Invalid occurrence of the wildcard alternative `| _ => ...`: It must be the last alternative" @@ -399,7 +399,7 @@ where 2- The errors are produced in the same order the appear in the code above. This is not super important when using IDEs. -/ - for h : altStxIdx in [0:altStxs.size] do + for h : altStxIdx in *...altStxs.size do let altStx := altStxs[altStxIdx] let altName := getAltName altStx if let some i := alts.findFinIdx? (·.1 == altName) then diff --git a/src/Lean/Elab/Tactic/Lets.lean b/src/Lean/Elab/Tactic/Lets.lean index 5bc00990fc..f72be9c011 100644 --- a/src/Lean/Elab/Tactic/Lets.lean +++ b/src/Lean/Elab/Tactic/Lets.lean @@ -26,7 +26,7 @@ register_builtin_option linter.tactic.unusedName : Bool := { def extractLetsAddVarInfo (ids : Array Syntax) (fvars : Array FVarId) : TacticM Unit := withMainContext do - for h : i in [0:ids.size] do + for h : i in *...ids.size do if h' : i < fvars.size then Term.addLocalVarInfo ids[i] (mkFVar fvars[i]) else diff --git a/src/Lean/Elab/Tactic/Monotonicity.lean b/src/Lean/Elab/Tactic/Monotonicity.lean index 3f3757246b..2111d00aef 100644 --- a/src/Lean/Elab/Tactic/Monotonicity.lean +++ b/src/Lean/Elab/Tactic/Monotonicity.lean @@ -188,7 +188,7 @@ def solveMonoStep (failK : ∀ {α}, Expr → Array Name → MetaM α := @defaul if let some info := isMatcherAppCore? (← getEnv) e then let candidate ← id do let args := e.getAppArgs - for i in [info.getFirstDiscrPos : info.getFirstDiscrPos + info.numDiscrs] do + for i in info.getFirstDiscrPos...(info.getFirstDiscrPos + info.numDiscrs) do if args[i]!.hasLooseBVars then return false return true diff --git a/src/Lean/Elab/Tactic/Omega/Core.lean b/src/Lean/Elab/Tactic/Omega/Core.lean index ea45d5828d..08f97c2a21 100644 --- a/src/Lean/Elab/Tactic/Omega/Core.lean +++ b/src/Lean/Elab/Tactic/Omega/Core.lean @@ -480,7 +480,7 @@ def fourierMotzkinData (p : Problem) : Array FourierMotzkinData := Id.run do let mut data : Array FourierMotzkinData := (List.range p.numVars).foldl (fun a i => a.push { var := i}) #[] for (_, f@⟨xs, s, _⟩) in p.constraints do - for i in [0:n] do + for i in *...n do let x := Coeffs.get xs i data := data.modify i fun d => if x = 0 then @@ -515,7 +515,7 @@ def fourierMotzkinSelect (data : Array FourierMotzkinData) : MetaM FourierMotzki if bestSize = 0 then trace[omega] "Selected variable {data[0]!.var}." return data[0]! - for h : i in [1:data.size] do + for h : i in 1...data.size do let exact := data[i].exact let size := data[i].size if size = 0 || !bestExact && exact || (bestExact == exact) && size < bestSize then diff --git a/src/Lean/Elab/Tactic/Omega/Frontend.lean b/src/Lean/Elab/Tactic/Omega/Frontend.lean index 2a489ddec5..fb130aa31a 100644 --- a/src/Lean/Elab/Tactic/Omega/Frontend.lean +++ b/src/Lean/Elab/Tactic/Omega/Frontend.lean @@ -559,7 +559,7 @@ where varNames (mask : Array Bool) : MetaM (Array String) := do let mut names := #[] let mut next := 0 - for h : i in [:mask.size] do + for h : i in *...mask.size do if mask[i] then while ← inScope (varNameOf next) do next := next + 1 names := names.push (varNameOf next) diff --git a/src/Lean/Elab/Tactic/Rewrite.lean b/src/Lean/Elab/Tactic/Rewrite.lean index ecb83fefef..a77ef9b38e 100644 --- a/src/Lean/Elab/Tactic/Rewrite.lean +++ b/src/Lean/Elab/Tactic/Rewrite.lean @@ -40,7 +40,7 @@ def withRWRulesSeq (token : Syntax) (rwRulesSeqStx : Syntax) (x : (symm : Bool) -- show initial state up to (incl.) `[` withTacticInfoContext (mkNullNode #[token, lbrak]) (pure ()) let numRules := (rules.size + 1) / 2 - for i in [:numRules] do + for i in *...numRules do let rule := rules[i * 2]! let sep := rules.getD (i * 2 + 1) Syntax.missing -- show rule state up to (incl.) next `,` diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean index 54c8d944a7..0d00a623e4 100644 --- a/src/Lean/Elab/Tactic/Simp.lean +++ b/src/Lean/Elab/Tactic/Simp.lean @@ -574,7 +574,7 @@ and different simp arguments may be used in each step.) def warnUnusedSimpArgs (simpArgs : Array (Syntax × ElabSimpArgResult)) (usedSimps : Simp.UsedSimps) : MetaM Unit := do if simpArgs.isEmpty then return let mut mask : Array Bool := #[] - for h : i in [:simpArgs.size] do + for h : i in *...simpArgs.size do let (ref, arg) := simpArgs[i] let used ← match arg with diff --git a/src/Lean/Elab/Tactic/Try.lean b/src/Lean/Elab/Tactic/Try.lean index a6cb16ac98..acb1b61b7e 100644 --- a/src/Lean/Elab/Tactic/Try.lean +++ b/src/Lean/Elab/Tactic/Try.lean @@ -285,7 +285,7 @@ private def mergeAll? (tacs : Array (TSyntax `tactic)) : TryTacticM (Option (TSy if tacs.any fun tac => tac.raw.getKind != tac0.raw.getKind then return none let mut tac := tac0 - for h : i in [1:tacs.size] do + for h : i in 1...tacs.size do let some tac' := merge? tac tacs[i] | return none tac := tac' @@ -432,7 +432,7 @@ private def evalSuggestChain (tac1 tac2 : TSyntax `tactic) : TryTacticM (TSyntax private def evalSuggestSeq (tacs : Array (TSyntax `tactic)) : TryTacticM (TSyntax `tactic) := do if (← read).terminal then let mut result := #[] - for i in [:tacs.size - 1] do + for i in *...(tacs.size - 1 : Nat) do result := appendSeq result (← withNonTerminal <| evalSuggest tacs[i]!) let suggestions ← getSuggestionOfTactic (← evalSuggest tacs.back!) |>.mapM fun tac => mkSeq (appendSeq result tac) (terminal := true) diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index 871eae7e0b..b74c37972c 100644 --- a/src/Lean/Environment.lean +++ b/src/Lean/Environment.lean @@ -1800,7 +1800,7 @@ We only consider extensions starting with index `>= startingAt`. def mkExtNameMap (startingAt : Nat) : IO (Std.HashMap Name Nat) := do let descrs ← persistentEnvExtensionsRef.get let mut result := {} - for h : i in [startingAt : descrs.size] do + for h : i in startingAt...descrs.size do let descr := descrs[i] result := result.insert descr.name i return result @@ -1816,7 +1816,7 @@ private def setImportedEntries (states : Array EnvExtensionState) (mods : Array { s with importedEntries := .replicate mods.size #[] } /- For each module `mod`, and `mod.entries`, if the extension name is one of the extensions after `startingAt`, set `entries` -/ let extNameIdx ← mkExtNameMap startingAt - for h : modIdx in [:mods.size] do + for h : modIdx in *...mods.size do let mod := mods[modIdx] for (extName, entries) in mod.entries do if let some entryIdx := extNameIdx[extName]? then @@ -2078,7 +2078,7 @@ def finalizeImport (s : ImportState) (imports : Array Import) (opts : Options) ( let mut const2ModIdx : Std.HashMap Name ModuleIdx := Std.HashMap.emptyWithCapacity (capacity := numPrivateConsts + numPublicConsts) let mut privateConstantMap : Std.HashMap Name ConstantInfo := Std.HashMap.emptyWithCapacity (capacity := numPrivateConsts) let mut publicConstantMap : Std.HashMap Name ConstantInfo := Std.HashMap.emptyWithCapacity (capacity := numPublicConsts) - for h : modIdx in [0:moduleData.size] do + for h : modIdx in *...moduleData.size do let data := moduleData[modIdx] for cname in data.constNames, cinfo in data.constants do match privateConstantMap.getThenInsertIfNew? cname cinfo with diff --git a/src/Lean/Linter/UnusedSimpArgs.lean b/src/Lean/Linter/UnusedSimpArgs.lean index 8ed3f2b135..9e585b9c3e 100644 --- a/src/Lean/Linter/UnusedSimpArgs.lean +++ b/src/Lean/Linter/UnusedSimpArgs.lean @@ -21,7 +21,7 @@ private def warnUnused (stx : Syntax) (i : Nat) : CoreM Unit := do let argStx := simpArgs[i]! let msg := m!"This simp argument is unused:{indentD argStx}" let mut otherArgs : Array Syntax := #[] - for h : j in [:simpArgs.size] do if j != i then + for h : j in *...simpArgs.size do if j != i then otherArgs := otherArgs.push simpArgs[j] let stx' := Tactic.setSimpParams stx otherArgs let suggestion : Meta.Hint.Suggestion := stx' @@ -63,7 +63,7 @@ def unusedSimpArgs : Linter where -- Sort the outputs by position for (_range, tacticStx, mask) in (← masksMap.get).toArray.qsort (·.1.start < ·.1.start) do - for i in [:mask.size] do + for i in *...mask.size do unless mask[i]! do liftCoreM <| warnUnused tacticStx i diff --git a/src/Lean/Meta/ACLt.lean b/src/Lean/Meta/ACLt.lean index 554384520a..365e5a04d8 100644 --- a/src/Lean/Meta/ACLt.lean +++ b/src/Lean/Meta/ACLt.lean @@ -115,14 +115,14 @@ where return false else let infos ← getParamsInfo aFn aArgs.size - for i in [:infos.size] do + for i in *...infos.size do -- We ignore instance implicit arguments during comparison if !infos[i]!.isInstImplicit then if (← lt aArgs[i]! bArgs[i]!) then return true else if (← lt bArgs[i]! aArgs[i]!) then return false - for i in [infos.size:aArgs.size] do + for i in infos.size...aArgs.size do if (← lt aArgs[i]! bArgs[i]!) then return true else if (← lt bArgs[i]! aArgs[i]!) then @@ -153,12 +153,12 @@ where | .app .. => a.withApp fun f args => do let infos ← getParamsInfo f args.size - for i in [:infos.size] do + for i in *...infos.size do -- We ignore instance implicit arguments during comparison if !infos[i]!.isInstImplicit then if !(← lt args[i]! b) then return false - for h : i in [infos.size:args.size] do + for h : i in infos.size...args.size do if !(← lt args[i] b) then return false return true diff --git a/src/Lean/Meta/ArgsPacker.lean b/src/Lean/Meta/ArgsPacker.lean index d6bee45ff4..185f0dea52 100644 --- a/src/Lean/Meta/ArgsPacker.lean +++ b/src/Lean/Meta/ArgsPacker.lean @@ -115,7 +115,7 @@ private def mkTupleElems (t : Expr) (arity : Nat) : Array Expr := Id.run do if arity = 0 then return #[] let mut result := #[] let mut t := t - for _ in [:arity - 1] do + for _ in *...(arity - 1 : Nat) do result := result.push (mkProj ``PSigma 0 t) t := mkProj ``PSigma 1 t result.push t @@ -559,7 +559,7 @@ to produce an expression of the isomorphic type -/ def curry (argsPacker : ArgsPacker) (e : Expr) : MetaM Expr := do let mut es := #[] - for i in [:argsPacker.numFuncs] do + for i in *...argsPacker.numFuncs do es := es.push (← argsPacker.curryProj e i) PProdN.mk 0 es diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean index 4d3fb875f1..4580e222f1 100644 --- a/src/Lean/Meta/Basic.lean +++ b/src/Lean/Meta/Basic.lean @@ -2088,7 +2088,7 @@ def instantiateForallWithParamInfos (e : Expr) (args : Array Expr) (cleanupAnnot let mut e := e let mut res := Array.mkEmpty args.size let mut j := 0 - for i in [0:args.size] do + for i in *...args.size do unless e.isForall do e ← whnf (e.instantiateRevRange j i args) j := i @@ -2117,7 +2117,7 @@ def instantiateLambdaWithParamInfos (e : Expr) (args : Array Expr) (cleanupAnnot let mut e := e let mut res := Array.mkEmpty args.size let mut j := 0 - for i in [0:args.size] do + for i in *...args.size do unless e.isLambda do e ← whnf (e.instantiateRevRange j i args) j := i diff --git a/src/Lean/Meta/Canonicalizer.lean b/src/Lean/Meta/Canonicalizer.lean index dc7b1c9e72..f4b46e1409 100644 --- a/src/Lean/Meta/Canonicalizer.lean +++ b/src/Lean/Meta/Canonicalizer.lean @@ -100,7 +100,7 @@ private partial def mkKey (e : Expr) : CanonM UInt64 := do else getFunInfo f let mut k ← mkKey f - for i in [:e.getAppNumArgs] do + for i in *...e.getAppNumArgs do if h : i < info.paramInfo.size then let info := info.paramInfo[i] if info.isExplicit && !info.isProp then diff --git a/src/Lean/Meta/Check.lean b/src/Lean/Meta/Check.lean index 1d76954880..c761feb2d1 100644 --- a/src/Lean/Meta/Check.lean +++ b/src/Lean/Meta/Check.lean @@ -116,7 +116,7 @@ where let mut bFnType ← inferType b.getAppFn let mut firstExplicitDiff? := none let mut firstImplicitDiff? := none - for i in [0:as.size] do + for i in *...as.size do unless aFnType.isForall do aFnType ← withTransparency .all <| whnf aFnType unless bFnType.isForall do bFnType ← withTransparency .all <| whnf bFnType -- These pattern matches are expected to succeed: diff --git a/src/Lean/Meta/CongrTheorems.lean b/src/Lean/Meta/CongrTheorems.lean index 2670e5ac0b..0f107af1ef 100644 --- a/src/Lean/Meta/CongrTheorems.lean +++ b/src/Lean/Meta/CongrTheorems.lean @@ -124,8 +124,8 @@ def mkHCongr (f : Expr) : MetaM CongrTheorem := do -/ private def fixKindsForDependencies (info : FunInfo) (kinds : Array CongrArgKind) : Array CongrArgKind := Id.run do let mut kinds := kinds - for i in [:info.paramInfo.size] do - for hj : j in [i+1:info.paramInfo.size] do + for i in *...info.paramInfo.size do + for hj : j in (i+1)...info.paramInfo.size do if info.paramInfo[j].backDeps.contains i then if kinds[j]! matches CongrArgKind.eq || kinds[j]! matches CongrArgKind.fixed then -- We must fix `i` because there is a `j` that depends on `i` and `j` is not cast-fixed. @@ -188,7 +188,7 @@ private def getClassSubobjectMask? (f : Expr) : MetaM (Option (Array Bool)) := d forallTelescopeReducing val.type (cleanupAnnotations := true) fun xs _ => do let env ← getEnv let mut mask := #[] - for h : i in [:xs.size] do + for h : i in *...xs.size do if i < val.numParams then mask := mask.push false else @@ -214,7 +214,7 @@ def getCongrSimpKinds (f : Expr) (info : FunInfo) : MetaM (Array CongrArgKind) : -/ let mut result := #[] let mask? ← getClassSubobjectMask? f - for h : i in [:info.paramInfo.size] do + for h : i in *...info.paramInfo.size do if info.resultDeps.contains i then result := result.push .fixed else if info.paramInfo[i].isProp then @@ -241,7 +241,7 @@ and otherwise it is `CongrArgKind.fixed`. This is used for the `arg` conv tactic -/ def getCongrSimpKindsForArgZero (info : FunInfo) : MetaM (Array CongrArgKind) := do let mut result := #[] - for h : i in [:info.paramInfo.size] do + for h : i in *...info.paramInfo.size do if info.resultDeps.contains i then result := result.push .fixed else if i == 0 then diff --git a/src/Lean/Meta/Constructions/BRecOn.lean b/src/Lean/Meta/Constructions/BRecOn.lean index c3c06c9246..29f8054f60 100644 --- a/src/Lean/Meta/Constructions/BRecOn.lean +++ b/src/Lean/Meta/Constructions/BRecOn.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura, Joachim Breitner -/ prelude +import Init.Data.Range.Polymorphic.Stream import Lean.Meta.InferType import Lean.AuxRecursor import Lean.AddDecl @@ -123,7 +124,7 @@ def mkBelow (indName : Name) : MetaM Unit := do -- If this is the first inductive in a mutual group with nested inductives, -- generate the constructions for the nested inductives now if indVal.all[0]! = indName then - for i in [:indVal.numNested] do + for i in *...indVal.numNested do let recName := recName.appendIndexAfter (i + 1) let belowName := belowName.appendIndexAfter (i + 1) mkBelowFromRec recName indVal.numParams belowName @@ -227,7 +228,7 @@ private def mkBRecOnFromRec (recName : Name) (nParams : Nat) -- (F_1 : (t : List α) → (f : List.below t) → motive t) -- and bring parameters of that type into scope let mut fDecls : Array (Name × (Array Expr -> MetaM Expr)) := #[] - for motive in motives, below in belows, i in [:motives.size] do + for motive in motives, below in belows, i in *...motives.size do let fType ← forallTelescope (← inferType motive) fun targs _ => do withLocalDeclD `f (mkAppN below targs) fun f => mkForallFVars (targs.push f) (mkAppN motive targs) @@ -280,7 +281,7 @@ def mkBRecOn (indName : Name) : MetaM Unit := do -- If this is the first inductive in a mutual group with nested inductives, -- generate the constructions for the nested inductives now. if indVal.all[0]! = indName then - for i in [:indVal.numNested] do + for i in *...indVal.numNested do let recName := recName.appendIndexAfter (i + 1) let brecOnName := brecOnName.appendIndexAfter (i + 1) mkBRecOnFromRec recName indVal.numParams indVal.all.toArray brecOnName diff --git a/src/Lean/Meta/Constructions/NoConfusion.lean b/src/Lean/Meta/Constructions/NoConfusion.lean index 27e11eedc4..de28bb2bff 100644 --- a/src/Lean/Meta/Constructions/NoConfusion.lean +++ b/src/Lean/Meta/Constructions/NoConfusion.lean @@ -71,7 +71,7 @@ where let natType := mkConst ``Nat let declType ← mkArrow enumType natType let mut minors := #[] - for i in [:numCtors] do + for i in *...numCtors do minors := minors.push <| mkNatLit i withLocalDeclD `x enumType fun x => do let motive ← mkLambdaFVars #[x] natType diff --git a/src/Lean/Meta/DiscrTree.lean b/src/Lean/Meta/DiscrTree.lean index afe2a9ce24..225bc65111 100644 --- a/src/Lean/Meta/DiscrTree.lean +++ b/src/Lean/Meta/DiscrTree.lean @@ -123,7 +123,7 @@ where goN (num : Nat) : StateRefT (List Key) CoreM (Array MessageData) := do let mut r := #[] - for _ in [: num] do + for _ in *...num do r := r.push (← go) return r diff --git a/src/Lean/Meta/ExprDefEq.lean b/src/Lean/Meta/ExprDefEq.lean index 2c32ac00b1..6163893251 100644 --- a/src/Lean/Meta/ExprDefEq.lean +++ b/src/Lean/Meta/ExprDefEq.lean @@ -80,7 +80,7 @@ where checkpointDefEq do let args := b.getAppArgs let params := args[*...ctorVal.numParams].toArray - for h : i in [ctorVal.numParams : args.size] do + for h : i in ctorVal.numParams...args.size do let j := i - ctorVal.numParams let proj ← mkProjFn ctorVal us params j a if ← isProof proj then @@ -255,7 +255,7 @@ private def isDefEqArgsFirstPass (paramInfo : Array ParamInfo) (args₁ args₂ : Array Expr) : MetaM DefEqArgsFirstPassResult := do let mut postponedImplicit := #[] let mut postponedHO := #[] - for h : i in [:paramInfo.size] do + for h : i in *...paramInfo.size do let info := paramInfo[i] let a₁ := args₁[i]! let a₂ := args₂[i]! @@ -291,7 +291,7 @@ private partial def isDefEqArgs (f : Expr) (args₁ args₂ : Array Expr) : Meta let finfo ← getFunInfoNArgs f args₁.size let .ok postponedImplicit postponedHO ← isDefEqArgsFirstPass finfo.paramInfo args₁ args₂ | pure false -- finfo.paramInfo.size may be smaller than args₁.size - for i in [finfo.paramInfo.size:args₁.size] do + for i in finfo.paramInfo.size...args₁.size do unless (← Meta.isExprDefEqAux args₁[i]! args₂[i]!) do return false for i in postponedImplicit do @@ -432,7 +432,7 @@ where let check (lctx : LocalContext) : Bool := Id.run do let start := lctx.getFVar! xs[0]! |>.index let stop := lctx.getFVar! xs.back! |>.index - for i in [start+1:stop] do + for i in (start+1)...stop do match lctx.getAt? i with | some localDecl => if localDecl.isLet then @@ -503,7 +503,7 @@ where let start := lctx.getFVar! xs[0]! |>.index let stop := lctx.getFVar! xs.back! |>.index let mut ys := #[] - for i in [start:stop+1] do + for i in start...=stop do match lctx.getAt? i with | none => pure () | some localDecl => diff --git a/src/Lean/Meta/ForEachExpr.lean b/src/Lean/Meta/ForEachExpr.lean index 7617dfc710..f93d5f6ced 100644 --- a/src/Lean/Meta/ForEachExpr.lean +++ b/src/Lean/Meta/ForEachExpr.lean @@ -93,7 +93,7 @@ def setMVarUserNamesAt (e : Expr) (isTarget : Array Expr) : MetaM (Array MVarId) forEachExpr (← instantiateMVars e) fun e => do if e.isApp then let args := e.getAppArgs - for h : i in [:args.size] do + for h : i in *...args.size do let arg := args[i] if arg.isMVar && isTarget.contains arg then let mvarId := arg.mvarId! diff --git a/src/Lean/Meta/FunInfo.lean b/src/Lean/Meta/FunInfo.lean index be9f618409..7509c0bbf2 100644 --- a/src/Lean/Meta/FunInfo.lean +++ b/src/Lean/Meta/FunInfo.lean @@ -59,7 +59,7 @@ private def getFunInfoAux (fn : Expr) (maxArgs? : Option Nat) : MetaM FunInfo := forallBoundedTelescope fnType maxArgs? fun fvars type => do let mut paramInfo := #[] let mut higherOrderOutParams : FVarIdSet := {} - for h : i in [:fvars.size] do + for h : i in *...fvars.size do let fvar := fvars[i] let decl ← getFVarLocalDecl fvar let backDeps := collectDeps fvars decl.type @@ -79,7 +79,7 @@ private def getFunInfoAux (fn : Expr) (maxArgs? : Option Nat) : MetaM FunInfo := if let some outParamPositions := getOutParamPositions? (← getEnv) className then unless outParamPositions.isEmpty do let args := decl.type.getAppArgs - for h2 : i in [:args.size] do + for h2 : i in *...args.size do if outParamPositions.contains i then let arg := args[i] if let some idx := fvars.idxOf? arg then diff --git a/src/Lean/Meta/Hint.lean b/src/Lean/Meta/Hint.lean index ee0005f995..5cd944120b 100644 --- a/src/Lean/Meta/Hint.lean +++ b/src/Lean/Meta/Hint.lean @@ -190,7 +190,7 @@ where let mut withWs := #[] let mut (wssIdx, wss'Idx) := (0, 0) let mut inSubst := false - for h : diffIdx in [:diff.size] do + for h : diffIdx in *...diff.size do let (a₁, s₁) := diff[diffIdx] withWs := withWs.push (a₁, s₁) if let some (a₂, s₂) := diff[diffIdx + 1]? then diff --git a/src/Lean/Meta/IndPredBelow.lean b/src/Lean/Meta/IndPredBelow.lean index db2d66ca58..c2939b309b 100644 --- a/src/Lean/Meta/IndPredBelow.lean +++ b/src/Lean/Meta/IndPredBelow.lean @@ -493,7 +493,7 @@ where -- `belowIndices` is a mapping from non-`below` to the `below` version of each field. let mut belowFieldOpts := .replicate belowCtor.numFields none let fields := fields.toArray - for fieldIdx in [:fields.size] do + for fieldIdx in *...fields.size do belowFieldOpts := belowFieldOpts.set! belowIndices[fieldIdx]! (some fields[fieldIdx]!) let belowParams := params.toArray.push belowMotive @@ -591,6 +591,7 @@ def mkBelow (declName : Name) : MetaM Unit := do addDecl decl trace[Meta.IndPredBelow] "added {ctx.belowNames}" ctx.belowNames.forM Lean.mkCasesOn + -- TODO: use new ranges as soon as it does not break compilerTest1.lean anymore for i in [:ctx.typeInfos.size] do try let decl ← IndPredBelow.mkBrecOnDecl ctx i diff --git a/src/Lean/Meta/InferType.lean b/src/Lean/Meta/InferType.lean index c992409d34..66283ed0cb 100644 --- a/src/Lean/Meta/InferType.lean +++ b/src/Lean/Meta/InferType.lean @@ -75,7 +75,7 @@ private def inferAppType (f : Expr) (args : Array Expr) : MetaM Expr := do let mut j := 0 /- TODO: check whether `instantiateBetaRevRange` is too expensive, and use it only when `args` contains a lambda expression. -/ - for i in [:args.size] do + for i in *...args.size do match fType with | Expr.forallE _ _ b _ => fType := b | _ => @@ -107,7 +107,7 @@ private def inferProjType (structName : Name) (idx : Nat) (e : Expr) : MetaM Exp failed () else do let mut ctorType ← inferAppType (mkConst ctorVal.name structLvls) structTypeArgs[*... diff --git a/src/Lean/Meta/Instances.lean b/src/Lean/Meta/Instances.lean index 2bdaecd091..276b8153b0 100644 --- a/src/Lean/Meta/Instances.lean +++ b/src/Lean/Meta/Instances.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ prelude +import Init.Data.Range.Polymorphic.Stream import Lean.ScopedEnvExtension import Lean.Meta.GlobalInstances import Lean.Meta.DiscrTree @@ -147,7 +148,7 @@ private partial def computeSynthOrder (inst : Expr) (projInfo? : Option Projecti if let .const className .. := classTy.getAppFn then forallTelescopeReducing (← inferType classTy.getAppFn) fun args _ => do let mut pos := (getOutParamPositions? (← getEnv) className).getD #[] - for arg in args, i in [:args.size] do + for arg in args, i in *...args.size do if (← inferType arg).isAppOf ``semiOutParam then pos := pos.push i return pos @@ -173,7 +174,7 @@ private partial def computeSynthOrder (inst : Expr) (projInfo? : Option Projecti -- These are assumed to not be mvars during TC search (or at least not assignable) let tyOutParams ← getSemiOutParamPositionsOf ty let tyArgs := ty.getAppArgs - for tyArg in tyArgs, i in [:tyArgs.size] do + for tyArg in tyArgs, i in *...tyArgs.size do unless tyOutParams.contains i do assignMVarsIn tyArg @@ -193,7 +194,7 @@ private partial def computeSynthOrder (inst : Expr) (projInfo? : Option Projecti let argTy ← whnf argTy let argOutParams ← getSemiOutParamPositionsOf argTy let argTyArgs := argTy.getAppArgs - for i in [:argTyArgs.size], argTyArg in argTyArgs do + for i in *...argTyArgs.size, argTyArg in argTyArgs do if !argOutParams.contains i && argTyArg.hasExprMVar then return false return true diff --git a/src/Lean/Meta/LetToHave.lean b/src/Lean/Meta/LetToHave.lean index 677852c5ba..3a9f5d8f7d 100644 --- a/src/Lean/Meta/LetToHave.lean +++ b/src/Lean/Meta/LetToHave.lean @@ -376,7 +376,7 @@ private partial def visitProj (e : Expr) (structName : Name) (idx : Nat) (struct let mut args := #[] let mut j := 0 let mut lastFieldTy : Expr := default - for i in [:idx+1] do + for i in *...=idx do unless ctorType.isForall do ctorType ← whnf <| ctorType.instantiateRevRange j i args j := i diff --git a/src/Lean/Meta/Match/MatchEqs.lean b/src/Lean/Meta/Match/MatchEqs.lean index 56e850a562..9b468b4c17 100644 --- a/src/Lean/Meta/Match/MatchEqs.lean +++ b/src/Lean/Meta/Match/MatchEqs.lean @@ -389,7 +389,7 @@ partial def proveCondEqThm (matchDeclName : Name) (type : Expr) let mut mvarId := mvar0.mvarId! if heqNum > 0 then mvarId := (← mvarId.introN heqPos).2 - for _ in [:heqNum] do + for _ in *...heqNum do let (h, mvarId') ← mvarId.intro1 mvarId ← subst mvarId' h trace[Meta.Match.matchEqs] "proveCondEqThm after subst{mvarId}" @@ -571,7 +571,7 @@ where e.withApp fun f args => do let mut argsNew := args let mut isAlt := #[] - for i in [6:args.size] do + for i in 6...args.size do let arg := argsNew[i]! if arg.isFVar then match (← read).find? arg.fvarId! with @@ -607,7 +607,7 @@ where -- Replace `rhs` with `x` (the lambda binder in the motive) let mut altTypeNewAbst := (← kabstract altTypeNew rhs).instantiate1 x -- Replace args[6...(6+i)] with `motiveTypeArgsNew` - for j in [:i] do + for j in *...i do altTypeNewAbst := (← kabstract altTypeNewAbst argsNew[6+j]!).instantiate1 motiveTypeArgsNew[j]! let localDecl ← motiveTypeArg.fvarId!.getDecl withLocalDecl localDecl.userName localDecl.binderInfo altTypeNewAbst fun motiveTypeArgNew => @@ -631,7 +631,7 @@ where let mut minorBodyNew := minor -- We have to extend the mapping to make sure `convertTemplate` can "fix" occurrences of the refined minor premises let mut m ← read - for h : i in [:isAlt.size] do + for h : i in *...isAlt.size do if isAlt[i] then -- `convertTemplate` will correct occurrences of the alternative let alt := args[6+i]! -- Recall that `Eq.ndrec` has 6 arguments @@ -760,7 +760,7 @@ where go baseName splitterName := withConfig (fun c => { c with etaStruct := .no let mut splitterAltTypes := #[] let mut splitterAltNumParams := #[] let mut altArgMasks := #[] -- masks produced by `forallAltTelescope` - for i in [:alts.size] do + for i in *...alts.size do let altNumParams := matchInfo.altNumParams[i]! let thmName := Name.str baseName eqnThmSuffixBase |>.appendIndexAfter idx eqnNames := eqnNames.push thmName @@ -878,7 +878,7 @@ where go baseName := withConfig (fun c => { c with etaStruct := .none }) do let discrs := xs[firstDiscrIdx...(firstDiscrIdx + matchInfo.numDiscrs)] let mut notAlts := #[] let mut idx := 1 - for i in [:alts.size] do + for i in *...alts.size do let altNumParams := matchInfo.altNumParams[i]! let thmName := (Name.str baseName congrEqnThmSuffixBase).appendIndexAfter idx eqnNames := eqnNames.push thmName diff --git a/src/Lean/Meta/Match/MatcherApp/Transform.lean b/src/Lean/Meta/Match/MatcherApp/Transform.lean index 1d7198c0e7..70545a720d 100644 --- a/src/Lean/Meta/Match/MatcherApp/Transform.lean +++ b/src/Lean/Meta/Match/MatcherApp/Transform.lean @@ -299,7 +299,7 @@ def transform let altTypes ← inferArgumentTypesN matcherApp.alts.size aux2 let mut alts' := #[] - for altIdx in [:matcherApp.alts.size], + for altIdx in *...matcherApp.alts.size, alt in matcherApp.alts, numParams in matcherApp.altNumParams, splitterNumParams in matchEqns.splitterAltNumParams, @@ -340,7 +340,7 @@ def transform let altTypes ← inferArgumentTypesN matcherApp.alts.size aux let mut alts' := #[] - for altIdx in [:matcherApp.alts.size], + for altIdx in *...matcherApp.alts.size, alt in matcherApp.alts, numParams in matcherApp.altNumParams, altType in altTypes do diff --git a/src/Lean/Meta/Match/MatcherInfo.lean b/src/Lean/Meta/Match/MatcherInfo.lean index a59b21553f..adf041105f 100644 --- a/src/Lean/Meta/Match/MatcherInfo.lean +++ b/src/Lean/Meta/Match/MatcherInfo.lean @@ -42,14 +42,14 @@ def MatcherInfo.arity (info : MatcherInfo) : Nat := def MatcherInfo.getFirstDiscrPos (info : MatcherInfo) : Nat := info.numParams + 1 -def MatcherInfo.getDiscrRange (info : MatcherInfo) : Std.Range := - [info.getFirstDiscrPos : info.getFirstDiscrPos + info.numDiscrs] +def MatcherInfo.getDiscrRange (info : MatcherInfo) : Std.PRange ⟨.closed, .open⟩ Nat := + info.getFirstDiscrPos...(info.getFirstDiscrPos + info.numDiscrs) def MatcherInfo.getFirstAltPos (info : MatcherInfo) : Nat := info.numParams + 1 + info.numDiscrs -def MatcherInfo.getAltRange (info : MatcherInfo) : Std.Range := - [info.getFirstAltPos : info.getFirstAltPos + info.numAlts] +def MatcherInfo.getAltRange (info : MatcherInfo) : Std.PRange ⟨.closed, .open⟩ Nat := + info.getFirstAltPos...(info.getFirstAltPos + info.numAlts) def MatcherInfo.getMotivePos (info : MatcherInfo) : Nat := info.numParams diff --git a/src/Lean/Meta/PProdN.lean b/src/Lean/Meta/PProdN.lean index ae76da66b2..ee791253b6 100644 --- a/src/Lean/Meta/PProdN.lean +++ b/src/Lean/Meta/PProdN.lean @@ -104,7 +104,7 @@ def proj (n i : Nat) (t e : Expr) : Expr := Id.run <| do unless i < n do panic! "PProdN.proj: {i} not less than {n}" let mut t := t let mut value := e - for _ in [:i] do + for _ in *...i do value := mkPProdSnd t value t := mkTypeSnd t if i+1 < n then @@ -119,7 +119,7 @@ def projs (n : Nat) (t e : Expr) : Array Expr := /-- Given a value of type `t₁ ×' … ×' tᵢ ×' … ×' tₙ`, return a value of type `tᵢ` -/ def projM (n i : Nat) (e : Expr) : MetaM Expr := do let mut value := e - for _ in [:i] do + for _ in *...i do value ← mkPProdSndM value if i+1 < n then mkPProdFstM value diff --git a/src/Lean/Meta/RecursorInfo.lean b/src/Lean/Meta/RecursorInfo.lean index 6c5c14adac..eb1ecf14ea 100644 --- a/src/Lean/Meta/RecursorInfo.lean +++ b/src/Lean/Meta/RecursorInfo.lean @@ -113,7 +113,7 @@ private def getMajorPosDepElim (declName : Name) (majorPos? : Option Nat) (xs : private def getParamsPos (declName : Name) (xs : Array Expr) (numParams : Nat) (Iargs : Array Expr) : MetaM (List (Option Nat)) := do let mut paramsPos := #[] - for i in [:numParams] do + for i in *...numParams do let x := xs[i]! match (← Iargs.findIdxM? fun Iarg => isDefEq Iarg x) with | some j => paramsPos := paramsPos.push (some j) @@ -127,7 +127,7 @@ private def getParamsPos (declName : Name) (xs : Array Expr) (numParams : Nat) ( private def getIndicesPos (declName : Name) (xs : Array Expr) (majorPos numIndices : Nat) (Iargs : Array Expr) : MetaM (List Nat) := do let mut indicesPos := #[] - for i in [:numIndices] do + for i in *...numIndices do let i := majorPos - numIndices + i let x := xs[i]! match (← Iargs.findIdxM? fun Iarg => isDefEq Iarg x) with @@ -158,7 +158,7 @@ private def getUnivLevelPos (declName : Name) (lparams : List Name) (motiveLvl : private def getProduceMotiveAndRecursive (xs : Array Expr) (numParams numIndices majorPos : Nat) (motive : Expr) : MetaM (List Bool × Bool) := do let mut produceMotive := #[] let mut recursor := false - for h : i in [:xs.size] do + for h : i in *...xs.size do if i < numParams + 1 then continue --skip parameters and motive if majorPos - numIndices ≤ i && i ≤ majorPos then diff --git a/src/Lean/Meta/Reduce.lean b/src/Lean/Meta/Reduce.lean index ff6c67785b..fac88d7188 100644 --- a/src/Lean/Meta/Reduce.lean +++ b/src/Lean/Meta/Reduce.lean @@ -25,7 +25,7 @@ partial def reduce (e : Expr) (explicitOnly skipTypes skipProofs := true) : Meta let nargs := e.getAppNumArgs let finfo ← getFunInfoNArgs f nargs let mut args := e.getAppArgs - for i in [:args.size] do + for i in *...args.size do if h : i < finfo.paramInfo.size then let info := finfo.paramInfo[i] if !explicitOnly || info.isExplicit then diff --git a/src/Lean/Meta/SizeOf.lean b/src/Lean/Meta/SizeOf.lean index 396f65ebef..3a23521c4e 100644 --- a/src/Lean/Meta/SizeOf.lean +++ b/src/Lean/Meta/SizeOf.lean @@ -178,7 +178,7 @@ def mkSizeOfFns (typeName : Name) : MetaM (Array Name × NameMap Name) := do recMap := recMap.insert recName sizeOfName result := result.push sizeOfName i := i + 1 - for j in [:indInfo.numNested] do + for j in *...indInfo.numNested do let recName := (mkRecName indInfo.all.head!).appendIndexAfter (j+1) let sizeOfName := baseName.appendIndexAfter i mkSizeOfFn recName sizeOfName diff --git a/src/Lean/Meta/Structure.lean b/src/Lean/Meta/Structure.lean index f3df9e1179..062283f9e0 100644 --- a/src/Lean/Meta/Structure.lean +++ b/src/Lean/Meta/Structure.lean @@ -74,7 +74,7 @@ def mkProjections (n : Name) (projDecls : Array StructProjDecl) (instImplicit : lctx := lctx.setBinderInfo fvarId .implicit -- Construct the projection functions: let mut ctorType := ctorType - for h : i in [0:projDecls.size] do + for h : i in *...projDecls.size do let {ref, projName, paramInfoOverrides} := projDecls[i] unless ctorType.isForall do throwErrorAt ref "\ @@ -130,7 +130,7 @@ def etaStruct? (e : Expr) (p : Name → Bool) : MetaM (Option Expr) := do let args := e.getAppArgs let params := args.extract 0 fVal.numParams let some x ← getProjectedExpr ctor fVal.induct params 0 args[fVal.numParams]! none | return none - for i in [1 : fVal.numFields] do + for i in 1...fVal.numFields do let arg := args[fVal.numParams + i]! let some x' ← getProjectedExpr ctor fVal.induct params i arg x | return none unless x' == x do return none diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean index 0414b261c2..d436ace3ec 100644 --- a/src/Lean/Meta/SynthInstance.lean +++ b/src/Lean/Meta/SynthInstance.lean @@ -227,7 +227,7 @@ def getInstances (type : Expr) : MetaM (Array Instance) := do let synthOrder ← forallTelescopeReducing (← inferType linst.fvar) fun xs _ => do if xs.isEmpty then return #[] let mut order := #[] - for i in [:xs.size], x in xs do + for i in *...xs.size, x in xs do if (← getFVarLocalDecl x).binderInfo == .instImplicit then order := order.push i return order diff --git a/src/Lean/Meta/Tactic/Apply.lean b/src/Lean/Meta/Tactic/Apply.lean index 8ced2dac2c..7c6790eb27 100644 --- a/src/Lean/Meta/Tactic/Apply.lean +++ b/src/Lean/Meta/Tactic/Apply.lean @@ -189,16 +189,16 @@ def _root_.Lean.MVarId.apply (mvarId : MVarId) (e : Expr) (cfg : ApplyConfig := ``` -/ let rangeNumArgs ← if hasMVarHead then - pure [numArgs : numArgs+1] + pure numArgs...(numArgs+1) else let targetTypeNumArgs ← getExpectedNumArgs targetType - pure [numArgs - targetTypeNumArgs : numArgs+1] + pure (numArgs - targetTypeNumArgs)...(numArgs+1) /- Auxiliary function for trying to add `n` underscores where `n ∈ [i: rangeNumArgs.stop)` See comment above -/ let rec go (i : Nat) : MetaM (Array Expr × Array BinderInfo) := do - if i < rangeNumArgs.stop then + if i < rangeNumArgs.upper then let s ← saveState let (newMVars, binderInfos, eType) ← forallMetaTelescopeReducing eType i if (← isDefEqApply cfg.approx eType targetType) then @@ -208,14 +208,14 @@ def _root_.Lean.MVarId.apply (mvarId : MVarId) (e : Expr) (cfg : ApplyConfig := go (i+1) else - let conclusionType? ← if rangeNumArgs.start = 0 then + let conclusionType? ← if rangeNumArgs.lower = 0 then pure none else - let (_, _, r) ← forallMetaTelescopeReducing eType (some rangeNumArgs.start) + let (_, _, r) ← forallMetaTelescopeReducing eType (some rangeNumArgs.lower) pure (some r) throwApplyError mvarId eType conclusionType? targetType term? - termination_by rangeNumArgs.stop - i - let (newMVars, binderInfos) ← go rangeNumArgs.start + termination_by rangeNumArgs.upper - i + let (newMVars, binderInfos) ← go rangeNumArgs.lower postprocessAppMVars `apply mvarId newMVars binderInfos cfg.synthAssignedInstances cfg.allowSynthFailures let e ← instantiateMVars e mvarId.assign (mkAppN e newMVars) diff --git a/src/Lean/Meta/Tactic/Assert.lean b/src/Lean/Meta/Tactic/Assert.lean index b22348025f..5d0d0a00bc 100644 --- a/src/Lean/Meta/Tactic/Assert.lean +++ b/src/Lean/Meta/Tactic/Assert.lean @@ -105,7 +105,7 @@ def _root_.Lean.MVarId.assertHypotheses (mvarId : MVarId) (hs : Array Hypothesis let (fvarIds, mvarId) ← mvarNew.mvarId!.introNP hs.size mvarId.modifyLCtx fun lctx => Id.run do let mut lctx := lctx - for h : i in [:hs.size] do + for h : i in *...hs.size do let h := hs[i] if h.kind != .default then lctx := lctx.setKind fvarIds[i]! h.kind diff --git a/src/Lean/Meta/Tactic/ElimInfo.lean b/src/Lean/Meta/Tactic/ElimInfo.lean index 01eedf52d9..cb0631dbfd 100644 --- a/src/Lean/Meta/Tactic/ElimInfo.lean +++ b/src/Lean/Meta/Tactic/ElimInfo.lean @@ -73,7 +73,7 @@ def getElimExprInfo (elimExpr : Expr) (baseDeclName? : Option Name := none) : Me | some targetPos => pure targetPos let mut altsInfo := #[] let env ← getEnv - for h : i in [:xs.size] do + for h : i in *...xs.size do let x := xs[i] if x != motive && !targets.contains x then let xDecl ← x.fvarId!.getDecl @@ -155,12 +155,12 @@ def mkCustomEliminator (elimName : Name) (induction : Bool) : MetaM CustomElimin let info ← getConstInfo elimName forallTelescopeReducing info.type fun xs _ => do let mut typeNames := #[] - for hi : i in [:elimInfo.targetsPos.size] do + for hi : i in *...elimInfo.targetsPos.size do let targetPos := elimInfo.targetsPos[i] let x := xs[targetPos]! /- Return true if there is another target that depends on `x`. -/ let isImplicitTarget : MetaM Bool := do - for hj : j in [i+1:elimInfo.targetsPos.size] do + for hj : j in (i+1)...elimInfo.targetsPos.size do let y := xs[elimInfo.targetsPos[j]]! let yType ← inferType y if (← dependsOn yType x.fvarId!) then diff --git a/src/Lean/Meta/Tactic/FunInd.lean b/src/Lean/Meta/Tactic/FunInd.lean index 696fb6898c..4ce7dc8225 100644 --- a/src/Lean/Meta/Tactic/FunInd.lean +++ b/src/Lean/Meta/Tactic/FunInd.lean @@ -426,7 +426,7 @@ def deduplicateIHs (vals : Array Expr) : MetaM (Array Expr) := do def assertIHs (vals : Array Expr) (mvarid : MVarId) : MetaM MVarId := do let mut mvarid := mvarid - for v in vals.reverse, i in [0:vals.size] do + for v in vals.reverse, i in *...vals.size do mvarid ← mvarid.assert (.mkSimple s!"ih{i+1}") (← inferType v) v return mvarid @@ -1058,7 +1058,7 @@ Given a realizer for `foo.mutual_induct`, defines `foo.induct`, `bar.induct` etc Used for well-founded and structural recursion. -/ def projectMutualInduct (unfolding : Bool) (names : Array Name) (mutualInduct : MetaM Name) (finalizeFirstInd : MetaM Unit) : MetaM Unit := do - for name in names, idx in [:names.size] do + for name in names, idx in *...names.size do let inductName := getFunInductName (unfolding := unfolding) name realizeConst names[0]! inductName do let ci ← getConstInfo (← mutualInduct) @@ -1087,7 +1087,7 @@ def setNaryFunIndInfo (unfolding : Bool) (fixedParamPerms : FixedParamPerms) (fu let fixedParamPerm := fixedParamPerms.perms[0]! let mut params := #[] let mut j := 0 - for h : i in [:fixedParamPerm.size] do + for h : i in *...fixedParamPerm.size do if fixedParamPerm[i].isSome then assert! j + 1 < unaryFunIndInfo.params.size params := params.push unaryFunIndInfo.params[j]! @@ -1370,7 +1370,7 @@ where doRealize inductName := do -- Motives with parameters reordered, to put indices and major first, -- and (when unfolding) the result field instantiated let mut brecMotives := #[] - for motive in motives, recArgInfo in recArgInfos, info in infos, funIdx in [:motives.size] do + for motive in motives, recArgInfo in recArgInfos, info in infos, funIdx in *...motives.size do let brecMotive ← forallTelescope (← inferType motive) fun ys _ => do let ys := if unfolding then ys.pop else ys let (indicesMajor, rest) := recArgInfo.pickIndicesMajor ys @@ -1422,7 +1422,7 @@ where doRealize inductName := do -- terms when we have mutual induction. let e' ← withLetDecls `minor minorTypes minors' fun minors' => do let mut brecOnApps := #[] - for info in infos, recArgInfo in recArgInfos, idx in [:infos.size] do + for info in infos, recArgInfo in recArgInfos, idx in *...infos.size do -- Take care to pick the `ys` from the type, to get the variable names expected -- by the user, but use the value arity let arity ← lambdaTelescope (← fixedParamPerms.perms[idx]!.instantiateLambda info.value xs) fun ys _ => pure ys.size @@ -1474,7 +1474,7 @@ where doRealize inductName := do if names.size = 1 then let mut params := #[] - for h : i in [:fixedParamPerms.perms[0]!.size] do + for h : i in *...fixedParamPerms.perms[0]!.size do if let some idx := fixedParamPerms.perms[0]![i] then if paramMask[idx]! then params := params.push .param @@ -1503,7 +1503,7 @@ partial def refinedArguments (e : Expr) : MetaM (Array Bool) := do let mut mask := mask let revDeps ← getParamRevDeps e assert! revDeps.size = mask.size - for i in [:mask.size] do + for i in *...mask.size do if mask[i]! then for j in revDeps[i]! do mask := mask.set! j true diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean index 7e2079a6c1..5ef26737ea 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean @@ -505,7 +505,7 @@ def check : GoalM Bool := do let mut progress := false checkInvariants try - for ringId in [:(← get').rings.size] do + for ringId in *...(← get').rings.size do let r ← RingM.run ringId checkRing progress := progress || r if (← isInconsistent) then diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Inv.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Inv.lean index 209d366ab2..960b8ae3b2 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Inv.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Inv.lean @@ -49,7 +49,7 @@ private def checkRingInvs : RingM Unit := do def checkInvariants : GoalM Unit := do unless grind.debug.get (← getOptions) do return () - for ringId in [: (← get').rings.size] do + for ringId in *...(← get').rings.size do RingM.run ringId do assert! (← getRingId) == ringId checkRingInvs diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean index 5b965b0844..9d0cbe48e3 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean @@ -112,7 +112,7 @@ def PreNullCert.combine (k₁ : Int) (m₁ : Mon) (c₁ : PreNullCert) (k₂ : I let qs₂ := c₂.qs let n := Nat.max qs₁.size qs₂.size let mut qs : Vector Poly n := Vector.replicate n (.num 0) - for h : i in [:n] do + for h : i in *...n do if h₁ : i < qs₁.size then let q₁ ← qs₁[i].mulMonM k₁ m₁ if h₂ : i < qs₂.size then @@ -121,7 +121,7 @@ def PreNullCert.combine (k₁ : Int) (m₁ : Mon) (c₁ : PreNullCert) (k₂ : I else qs := qs.set i q₁ else - have : i < n := h.upper + have : i < n := Std.PRange.lt_upper_of_mem h have : qs₁.size = n ∨ qs₂.size = n := by simp +zetaDelta only [Nat.max_def, right_eq_ite_iff]; split <;> simp [*] have : i < qs₂.size := by omega let q₂ ← qs₂[i].mulMonM k₂ m₂ diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Linear/Inv.lean b/src/Lean/Meta/Tactic/Grind/Arith/Linear/Inv.lean index 56c4dedfd7..909a640e05 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Linear/Inv.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Linear/Inv.lean @@ -98,7 +98,7 @@ def checkStructInvs : LinearM Unit := do def checkInvariants : GoalM Unit := do unless grind.debug.get (← getOptions) do return () - for structId in [: (← get').structs.size] do + for structId in *...(← get').structs.size do LinearM.run structId do assert! (← getStructId) == structId checkStructInvs diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Linear/Search.lean b/src/Lean/Meta/Tactic/Grind/Arith/Linear/Search.lean index 39e4977cea..68b0621804 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Linear/Search.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Linear/Search.lean @@ -266,7 +266,7 @@ The result is `false` if module for every structure already has an assignment. -/ def check : GoalM Bool := do let mut progress := false - for structId in [:(← get').structs.size] do + for structId in *...(← get').structs.size do let r ← LinearM.run structId do if (← hasAssignment) then return false diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Offset/Main.lean b/src/Lean/Meta/Tactic/Grind/Arith/Offset/Main.lean index 7f792be9d1..958a1e01e6 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Offset/Main.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Offset/Main.lean @@ -235,7 +235,7 @@ def Cnstr.toExpr (c : Cnstr NodeId) : GoalM Expr := do def checkInvariants : GoalM Unit := do unless (← isInconsistent) do let s ← get' - for u in [:s.targets.size], es in s.targets.toArray do + for u in *...s.targets.size, es in s.targets.toArray do for (v, k) in es do let c : Cnstr NodeId := { u, v, k } trace[grind.debug.offset] "{c}" @@ -353,7 +353,7 @@ def processNewEqImpl (a b : Expr) : GoalM Unit := do def traceDists : GoalM Unit := do let s ← get' - for u in [:s.targets.size], es in s.targets.toArray do + for u in *...s.targets.size, es in s.targets.toArray do for (v, k) in es do trace[grind.offset.dist] "#{u} -({k})-> #{v}" diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Offset/Model.lean b/src/Lean/Meta/Tactic/Grind/Arith/Offset/Model.lean index ffefc71bde..82ed1846cc 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Offset/Model.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Offset/Model.lean @@ -23,7 +23,7 @@ def mkModel (goal : Goal) : MetaM (Array (Expr × Nat)) := do -/ let mut needAdjust : Array Bool := .replicate nodes.size true -- Initialize `needAdjust` - for u in [: nodes.size] do + for u in *...nodes.size do if isInterpreted u then -- Interpreted values have a fixed value. needAdjust := needAdjust.set! u false @@ -32,12 +32,12 @@ def mkModel (goal : Goal) : MetaM (Array (Expr × Nat)) := do else if s.targets[u]!.any fun v _ => isInterpreted v then needAdjust := needAdjust.set! u false -- Set interpreted values - for h : u in [:nodes.size] do + for h : u in *...nodes.size do let e := nodes[u] if let some v ← getNatValue? e then pre := pre.set! u (Int.ofNat v) -- Set remaining values - for u in [:nodes.size] do + for u in *...nodes.size do let lower? := s.sources[u]!.foldl (init := none) fun val? v k => Id.run do let some va := pre[v]! | return val? let val' := va - k @@ -62,7 +62,7 @@ def mkModel (goal : Goal) : MetaM (Array (Expr × Nat)) := do let some val := val? | return min if val < min then val else min let mut r := {} - for u in [:nodes.size] do + for u in *...nodes.size do let some val := pre[u]! | unreachable! let val := if needAdjust[u]! then (val - min).toNat else val.toNat let e := nodes[u]! diff --git a/src/Lean/Meta/Tactic/Grind/Canon.lean b/src/Lean/Meta/Tactic/Grind/Canon.lean index c079a52fa2..f59dc12655 100644 --- a/src/Lean/Meta/Tactic/Grind/Canon.lean +++ b/src/Lean/Meta/Tactic/Grind/Canon.lean @@ -179,7 +179,7 @@ where let pinfos := (← getFunInfo f).paramInfo let mut modified := false let mut args := args.toVector - for h : i in [:args.size] do + for h : i in *...args.size do let arg := args[i] trace_goal[grind.debug.canon] "[{repr (← shouldCanon pinfos i arg)}]: {arg} : {← inferType arg}" let arg' ← match (← shouldCanon pinfos i arg) with diff --git a/src/Lean/Meta/Tactic/Grind/Cases.lean b/src/Lean/Meta/Tactic/Grind/Cases.lean index a28fa48c2d..bd256d9201 100644 --- a/src/Lean/Meta/Tactic/Grind/Cases.lean +++ b/src/Lean/Meta/Tactic/Grind/Cases.lean @@ -158,7 +158,7 @@ def cases (mvarId : MVarId) (e : Expr) : MetaM (List MVarId) := mvarId.withConte let mut recursorType ← inferType recursor let mut mvarIdsNew := #[] let mut idx := 1 - for _ in [:recursorInfo.numMinors] do + for _ in *...recursorInfo.numMinors do let .forallE _ targetNew recursorTypeNew _ ← whnf recursorType | throwTacticEx `grind.cases mvarId "unexpected recursor type" recursorType := recursorTypeNew diff --git a/src/Lean/Meta/Tactic/Grind/EMatch.lean b/src/Lean/Meta/Tactic/Grind/EMatch.lean index e46676a38d..33ffe5ab4b 100644 --- a/src/Lean/Meta/Tactic/Grind/EMatch.lean +++ b/src/Lean/Meta/Tactic/Grind/EMatch.lean @@ -372,7 +372,7 @@ private def assignGeneralizedPatternProof (mvarId : MVarId) (eqProof : Expr) (or private def applyAssignment (mvars : Array Expr) : OptionT (StateT Choice M) Unit := do let thm := (← read).thm let numParams := thm.numParams - for h : i in [:mvars.size] do + for h : i in *...mvars.size do let bidx := numParams - i - 1 let mut v := (← get).assignment[bidx]! if isSameExpr v delayedEqProof then diff --git a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean index de9c86dd49..a0a72ccac8 100644 --- a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean +++ b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean @@ -696,7 +696,7 @@ private partial def go (pattern : Expr) (inSupport : Bool) (root : Bool) : M Exp saveSymbol f.toHeadIndex let mut args := pattern.getAppArgs.toVector let patternArgKinds ← getPatternArgKinds f args.size - for h : i in [:args.size] do + for h : i in *...args.size do let arg := args[i] let argKind := patternArgKinds[i]?.getD .relevant args := args.set i (← goArg arg (inSupport || argKind.isSupport) argKind) @@ -831,7 +831,7 @@ private def checkCoverage (thmProof : Expr) (numParams : Nat) (bvarsFound : Std. if !modified then break let mut pos := #[] - for h : i in [:xs.size] do + for h : i in *...xs.size do let fvarId := xs[i].fvarId! unless fvarsFound.contains fvarId do pos := pos.push i @@ -845,7 +845,7 @@ private def ppParamsAt (proof : Expr) (numParams : Nat) (paramPos : List Nat) : forallBoundedTelescope (← inferType proof) numParams fun xs _ => do let mut msg := m!"" let mut first := true - for h : i in [:xs.size] do + for h : i in *...xs.size do if paramPos.contains i then let x := xs[i] if first then first := false else msg := msg ++ "\n" diff --git a/src/Lean/Meta/Tactic/Grind/Internalize.lean b/src/Lean/Meta/Tactic/Grind/Internalize.lean index dc0f8003fe..e83344dd34 100644 --- a/src/Lean/Meta/Tactic/Grind/Internalize.lean +++ b/src/Lean/Meta/Tactic/Grind/Internalize.lean @@ -238,7 +238,7 @@ private def propagateEtaStruct (a : Expr) (generation : Nat) : GoalM Unit := do if (← isExtTheorem inductVal.name) || ctorVal.numFields == 0 then let params := aType.getAppArgs[*...inductVal.numParams] let mut ctorApp := mkAppN (mkConst ctorVal.name us) params - for j in [: ctorVal.numFields] do + for j in *...ctorVal.numFields do let mut proj ← mkProjFn ctorVal us params j a if (← isProof proj) then proj ← markProof proj @@ -410,7 +410,7 @@ where else internalizeImpl f generation e registerParent e f - for h : i in [: args.size] do + for h : i in *...args.size do let arg := args[i] internalize arg generation e registerParent e arg diff --git a/src/Lean/Meta/Tactic/Grind/Inv.lean b/src/Lean/Meta/Tactic/Grind/Inv.lean index 66fc809758..d4683ce33e 100644 --- a/src/Lean/Meta/Tactic/Grind/Inv.lean +++ b/src/Lean/Meta/Tactic/Grind/Inv.lean @@ -95,9 +95,9 @@ private def checkParents (e : Expr) : GoalM Unit := do private def checkPtrEqImpliesStructEq : GoalM Unit := do let exprs ← getExprs - for h₁ : i in [: exprs.size] do + for h₁ : i in *...exprs.size do let e₁ := exprs[i] - for h₂ : j in [i+1 : exprs.size] do + for h₂ : j in (i+1)...exprs.size do let e₂ := exprs[j] -- We don't have multiple nodes for the same expression assert! !isSameExpr e₁ e₂ diff --git a/src/Lean/Meta/Tactic/Grind/MarkNestedProofs.lean b/src/Lean/Meta/Tactic/Grind/MarkNestedProofs.lean index b9a9fe42a1..5daa341592 100644 --- a/src/Lean/Meta/Tactic/Grind/MarkNestedProofs.lean +++ b/src/Lean/Meta/Tactic/Grind/MarkNestedProofs.lean @@ -56,7 +56,7 @@ where | .app .. => e.withApp fun f args => do let mut modified := false let mut args := args - for i in [:args.size] do + for i in *...args.size do let arg := args[i]! let arg' ← visit arg unless ptrEq arg arg' do diff --git a/src/Lean/Meta/Tactic/Grind/MatchCond.lean b/src/Lean/Meta/Tactic/Grind/MatchCond.lean index 31d19342f0..81b800a9ed 100644 --- a/src/Lean/Meta/Tactic/Grind/MatchCond.lean +++ b/src/Lean/Meta/Tactic/Grind/MatchCond.lean @@ -212,7 +212,7 @@ where if ctorLhs.name ≠ ctorRhs.name then return true let lhsArgs := root.self.getAppArgs let rhsArgs := rhs.getAppArgs - for i in [ctorLhs.numParams : ctorLhs.numParams + ctorLhs.numFields] do + for i in ctorLhs.numParams...(ctorLhs.numParams + ctorLhs.numFields) do if (← isFalse lhsArgs[i]! rhsArgs[i]!) then return true return false @@ -392,7 +392,7 @@ where let some ctorInfo ← isConstructorApp? ctor | return ctor let mut ctorArgs := ctor.getAppArgs let mut modified := false - for i in [ctorInfo.numParams : ctorInfo.numParams + ctorInfo.numFields] do + for i in ctorInfo.numParams...(ctorInfo.numParams + ctorInfo.numFields) do let arg := ctorArgs[i]! let arg' ← go arg unless isSameExpr arg arg' do diff --git a/src/Lean/Meta/Tactic/Injection.lean b/src/Lean/Meta/Tactic/Injection.lean index 0b61cd29f1..35a1a757e1 100644 --- a/src/Lean/Meta/Tactic/Injection.lean +++ b/src/Lean/Meta/Tactic/Injection.lean @@ -16,7 +16,7 @@ namespace Lean.Meta def getCtorNumPropFields (ctorInfo : ConstructorVal) : MetaM Nat := do forallTelescopeReducing ctorInfo.type fun xs _ => do let mut numProps := 0 - for i in [:ctorInfo.numFields] do + for i in *...ctorInfo.numFields do if (← isProp (← inferType xs[ctorInfo.numParams + i]!)) then numProps := numProps + 1 return numProps diff --git a/src/Lean/Meta/Tactic/Lets.lean b/src/Lean/Meta/Tactic/Lets.lean index e85228b2ec..e52d12398e 100644 --- a/src/Lean/Meta/Tactic/Lets.lean +++ b/src/Lean/Meta/Tactic/Lets.lean @@ -272,7 +272,7 @@ where else let (paramInfos, _) ← instantiateForallWithParamInfos (← inferType f) args let mut args := args - for i in [0:args.size] do + for i in *...args.size do if paramInfos[i]!.binderInfo.isExplicit then args := args.set! i (← extractCore fvars args[i]!) return mkAppN f' args diff --git a/src/Lean/Meta/Tactic/LibrarySearch.lean b/src/Lean/Meta/Tactic/LibrarySearch.lean index 796b3417e7..62636e9dce 100644 --- a/src/Lean/Meta/Tactic/LibrarySearch.lean +++ b/src/Lean/Meta/Tactic/LibrarySearch.lean @@ -144,8 +144,8 @@ def interleaveWith {α β γ} (f : α → γ) (x : Array α) (g : β → γ) (y Id.run do let mut res := Array.mkEmpty (x.size + y.size) let n := min x.size y.size - for h : i in [0:n] do - have p : i < min x.size y.size := h.2.1 + for h : i in *...n do + have p : i < min x.size y.size := Std.PRange.lt_upper_of_mem h have q : i < x.size := Nat.le_trans p (Nat.min_le_left ..) have r : i < y.size := Nat.le_trans p (Nat.min_le_right ..) res := res.push (f x[i]) diff --git a/src/Lean/Meta/Tactic/NormCast.lean b/src/Lean/Meta/Tactic/NormCast.lean index d727d309c8..8e3a377045 100644 --- a/src/Lean/Meta/Tactic/NormCast.lean +++ b/src/Lean/Meta/Tactic/NormCast.lean @@ -51,7 +51,7 @@ partial def countCoes (e : Expr) : MetaM Nat := if let some info ← getCoeFnInfo? fn then if e.getAppNumArgs >= info.numArgs then let mut coes := (← countHeadCoes (e.getArg! info.coercee)) + 1 - for i in [info.numArgs:e.getAppNumArgs] do + for i in info.numArgs...e.getAppNumArgs do coes := coes + (← countCoes (e.getArg! i)) return coes return (← (← getSimpArgs e).mapM countCoes).foldl (·+·) 0 diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean index 898e8ec228..39bc99f5ac 100644 --- a/src/Lean/Meta/Tactic/Simp/Main.lean +++ b/src/Lean/Meta/Tactic/Simp/Main.lean @@ -498,7 +498,7 @@ def HaveTelescopeInfo.computeFixedUsed (info : HaveTelescopeInfo) (keepUnused : -- There is no need to consider `info.bodyTypeDeps` in this computation. used := updateArrayFromBackDeps used info.bodyDeps -- For each used `have`, in reverse order, update `used`. - for i in [0:numHaves] do + for i in *...numHaves do let idx := numHaves - i - 1 if used[idx]! then let hinfo := info.haveInfo[idx]! diff --git a/src/Lean/Meta/Tactic/Simp/Rewrite.lean b/src/Lean/Meta/Tactic/Simp/Rewrite.lean index c215d31322..6e39d5a536 100644 --- a/src/Lean/Meta/Tactic/Simp/Rewrite.lean +++ b/src/Lean/Meta/Tactic/Simp/Rewrite.lean @@ -162,7 +162,7 @@ private def tryTheoremCore (lhs : Expr) (xs : Array Expr) (bis : Array BinderInf This simple approach was good enough for Mathlib 3 -/ let mut extraArgs := #[] let mut e := e - for _ in [:numExtraArgs] do + for _ in *...numExtraArgs do extraArgs := extraArgs.push e.appArg! e := e.appFn! extraArgs := extraArgs.reverse @@ -337,7 +337,7 @@ def simpMatchDiscrs? (info : MatcherInfo) (e : Expr) : SimpM (Option Result) := let args := e.getAppArgsN n let mut r : Result := { expr := f } let mut modified := false - for i in [0 : info.numDiscrs] do + for i in *...info.numDiscrs do let arg := args[i]! if i < infos.size && !infos[i]!.hasFwdDeps then let argNew ← simp arg @@ -353,7 +353,7 @@ def simpMatchDiscrs? (info : MatcherInfo) (e : Expr) : SimpM (Option Result) := r ← mkCongrFun r argNew unless modified do return none - for h : i in [info.numDiscrs : args.size] do + for h : i in info.numDiscrs...args.size do let arg := args[i] r ← mkCongrFun r arg return some r diff --git a/src/Lean/Meta/Tactic/Simp/SimpAll.lean b/src/Lean/Meta/Tactic/Simp/SimpAll.lean index cefc68f570..84f00785d5 100644 --- a/src/Lean/Meta/Tactic/Simp/SimpAll.lean +++ b/src/Lean/Meta/Tactic/Simp/SimpAll.lean @@ -59,7 +59,7 @@ private partial def loop : M Bool := do let simprocs := (← get).simprocs -- simplify entries let entries := (← get).entries - for h : i in [:entries.size] do + for h : i in *...entries.size do let entry := entries[i] let ctx := (← get).ctx -- We disable the current entry to prevent it to be simplified to `True` diff --git a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean index 7f9afa4b29..30dea1efd1 100644 --- a/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean +++ b/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean @@ -464,7 +464,7 @@ def mkSimpEntryOfDeclToUnfold (declName : Name) : MetaM (Array SimpEntry) := do if (← Simp.ignoreEquations declName) then entries := entries.push (.toUnfold declName) else if let some eqns ← getEqnsFor? declName then - for h : i in [:eqns.size] do + for h : i in *...eqns.size do let eqn := eqns[i] /- We assign priorities to the equational lemmas so that more specific ones diff --git a/src/Lean/Meta/Tactic/Simp/Simproc.lean b/src/Lean/Meta/Tactic/Simp/Simproc.lean index 204ad1907a..ac6c1002f9 100644 --- a/src/Lean/Meta/Tactic/Simp/Simproc.lean +++ b/src/Lean/Meta/Tactic/Simp/Simproc.lean @@ -188,7 +188,7 @@ def Simprocs.add (s : Simprocs) (declName : Name) (post : Bool) : CoreM Simprocs def SimprocEntry.try (s : SimprocEntry) (numExtraArgs : Nat) (e : Expr) : SimpM Step := do let mut extraArgs := #[] let mut e := e - for _ in [:numExtraArgs] do + for _ in *...numExtraArgs do extraArgs := extraArgs.push e.appArg! e := e.appFn! extraArgs := extraArgs.reverse @@ -204,7 +204,7 @@ def SimprocEntry.try (s : SimprocEntry) (numExtraArgs : Nat) (e : Expr) : SimpM def SimprocEntry.tryD (s : SimprocEntry) (numExtraArgs : Nat) (e : Expr) : SimpM DStep := do let mut extraArgs := #[] let mut e := e - for _ in [:numExtraArgs] do + for _ in *...numExtraArgs do extraArgs := extraArgs.push e.appArg! e := e.appFn! extraArgs := extraArgs.reverse diff --git a/src/Lean/Meta/Tactic/Simp/Types.lean b/src/Lean/Meta/Tactic/Simp/Types.lean index 65d64ed09d..fe3568c858 100644 --- a/src/Lean/Meta/Tactic/Simp/Types.lean +++ b/src/Lean/Meta/Tactic/Simp/Types.lean @@ -582,7 +582,7 @@ def mkImpCongr (src : Expr) (r₁ r₂ : Result) : MetaM Result := do partial def removeUnnecessaryCasts (e : Expr) : MetaM Expr := do let mut args := e.getAppArgs let mut modified := false - for i in [:args.size] do + for i in *...args.size do let arg := args[i]! if isDummyEqRec arg then args := args.set! i (elimDummyEqRec arg) diff --git a/src/Lean/Meta/Tactic/Split.lean b/src/Lean/Meta/Tactic/Split.lean index bcf442ef97..845f17558f 100644 --- a/src/Lean/Meta/Tactic/Split.lean +++ b/src/Lean/Meta/Tactic/Split.lean @@ -140,7 +140,7 @@ private partial def generalizeMatchDiscrs (mvarId : MVarId) (matcherDeclName : N let matcherApp := { matcherApp with discrs := discrVars } foundRef.set true let mut altsNew := #[] - for h : i in [:matcherApp.alts.size] do + for h : i in *...matcherApp.alts.size do let alt := matcherApp.alts[i] let altNumParams := matcherApp.altNumParams[i]! let altNew ← lambdaTelescope alt fun xs body => do diff --git a/src/Lean/Meta/Tactic/SplitIf.lean b/src/Lean/Meta/Tactic/SplitIf.lean index 549155c8d1..e8ff6093b2 100644 --- a/src/Lean/Meta/Tactic/SplitIf.lean +++ b/src/Lean/Meta/Tactic/SplitIf.lean @@ -45,7 +45,7 @@ private def isCandidate? (env : Environment) (ctx : Context) (e : Expr) : Option if ctx.kind.considerMatch then if let some info := isMatcherAppCore? env e then let args := e.getAppArgs - for i in [info.getFirstDiscrPos : info.getFirstDiscrPos + info.numDiscrs] do + for i in info.getFirstDiscrPos...(info.getFirstDiscrPos + info.numDiscrs) do if args[i]!.hasLooseBVars then return none return ret (e.getBoundedAppFn (args.size - info.arity)) @@ -81,7 +81,7 @@ where pure {} else getFunInfo f - for u : i in [0:args.size] do + for u : i in *...args.size do let arg := args[i] if h : i < info.paramInfo.size then let info := info.paramInfo[i] diff --git a/src/Lean/Meta/Tactic/TryThis.lean b/src/Lean/Meta/Tactic/TryThis.lean index 88a0708125..4a276aa80f 100644 --- a/src/Lean/Meta/Tactic/TryThis.lean +++ b/src/Lean/Meta/Tactic/TryThis.lean @@ -106,7 +106,7 @@ apply the replacement. unless stxRange.start.line ≤ params.range.end.line do return result unless params.range.start.line ≤ stxRange.end.line do return result let mut result := result - for h : i in [:suggestionTexts.size] do + for h : i in *...suggestionTexts.size do let (newText, title?) := suggestionTexts[i] let title := title?.getD <| (codeActionPrefix?.getD "Try this: ") ++ newText result := result.push { diff --git a/src/Lean/Meta/WHNF.lean b/src/Lean/Meta/WHNF.lean index d9cd949a0d..e42ef2a79e 100644 --- a/src/Lean/Meta/WHNF.lean +++ b/src/Lean/Meta/WHNF.lean @@ -182,7 +182,7 @@ private def toCtorWhenStructure (inductName : Name) (major : Expr) : MetaM Expr let ctorInfo ← getConstInfoCtor ctorName let params := majorType.getAppArgs.shrink ctorInfo.numParams let mut result := mkAppN (mkConst ctorName us) params - for i in [:ctorInfo.numFields] do + for i in *...ctorInfo.numFields do result := mkApp result (← mkProjFn ctorInfo us params i major) return result | _ => return major diff --git a/src/Lean/ParserCompiler.lean b/src/Lean/ParserCompiler.lean index 5330b8741d..2d26de1c0a 100644 --- a/src/Lean/ParserCompiler.lean +++ b/src/Lean/ParserCompiler.lean @@ -73,7 +73,7 @@ partial def compileParserExpr (e : Expr) : MetaM Expr := do forallTelescope ty fun params _ => do let mut p := mkConst p let args := e.getAppArgs - for i in [:Nat.min params.size args.size] do + for i in *...(Nat.min params.size args.size) do let param := params[i]! let arg := args[i]! let paramTy ← inferType param diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean index 2a3757eb40..a672eae2f1 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean @@ -184,7 +184,7 @@ def getParamKinds (f : Expr) (args : Array Expr) : MetaM (Array ParamKind) := do let mut result : Array ParamKind := Array.mkEmpty args.size let mut fnType ← inferType f let mut j := 0 - for i in [0:args.size] do + for i in *...args.size do unless fnType.isForall do fnType ← withTransparency .all <| whnf (fnType.instantiateRevRange j i args) j := i @@ -776,7 +776,7 @@ partial def delabAppMatch : Delab := whenNotPPOption getPPExplicit <| whenPPOpti let st ← withDummyBinders (st.info.discrInfos.map (·.hName?)) (← getExpr) fun hNames? => do let hNames := hNames?.filterMap id let mut st := {st with hNames? := hNames?} - for i in [0:st.alts.size] do + for i in *...st.alts.size do st ← withTheReader SubExpr (fun _ => st.alts[i]!) do -- We save the variables names here to be able to implement safe shadowing. -- The pattern delaboration must use the names saved here. diff --git a/src/Lean/PrettyPrinter/Delaborator/FieldNotation.lean b/src/Lean/PrettyPrinter/Delaborator/FieldNotation.lean index 1b5a65258f..1d7e0fa7d9 100644 --- a/src/Lean/PrettyPrinter/Delaborator/FieldNotation.lean +++ b/src/Lean/PrettyPrinter/Delaborator/FieldNotation.lean @@ -72,7 +72,7 @@ private def generalizedFieldInfo (c : Name) (args : Array Expr) : MetaM (Name × -- Search for the first argument that could be used for field notation -- and make sure it is the first explicit argument. forallBoundedTelescope info.type args.size fun params _ => do - for h : i in [0:params.size] do + for h : i in *...params.size do let fvarId := params[i].fvarId! -- If there is a motive, we will treat this as a sort of control flow structure and so we won't use field notation. -- Plus, recursors tend to be riskier when using dot notation. diff --git a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean index 2d38450f33..028905a205 100644 --- a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean +++ b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean @@ -308,7 +308,7 @@ partial def canBottomUp (e : Expr) (mvar? : Option Expr := none) (fuel : Nat := let args := e.getAppArgs let fType ← replaceLPsWithVars (← inferType e.getAppFn) let (mvars, bInfos, resultType) ← forallMetaBoundedTelescope fType e.getAppArgs.size - for h : i in [:mvars.size] do + for h : i in *...mvars.size do if bInfos[i]! == BinderInfo.instImplicit then inspectOutParams args[i]! mvars[i] else if bInfos[i]! == BinderInfo.default then @@ -480,14 +480,14 @@ mutual discard <| processPostponed (mayPostpone := true) applyFunBinderHeuristic analyzeFn - for i in [:(← read).args.size] do analyzeArg i + for i in *...(← read).args.size do analyzeArg i maybeSetExplicit where collectBottomUps := do let { args, mvars, bInfos, ..} ← read for target in [fun _ => none, fun i => some mvars[i]!] do - for h : i in [:args.size] do + for h : i in *...args.size do if bInfos[i]! == BinderInfo.default then if ← typeUnknown mvars[i]! <&&> canBottomUp args[i] (target i) then tryUnify args[i]! mvars[i]! @@ -495,12 +495,12 @@ mutual checkOutParams := do let { args, mvars, bInfos, ..} ← read - for h : i in [:args.size] do + for h : i in *...args.size do if bInfos[i]! == BinderInfo.instImplicit then inspectOutParams args[i] mvars[i]! collectHigherOrders := do let { args, mvars, bInfos, ..} ← read - for h : i in [:args.size] do + for h : i in *...args.size do if !(bInfos[i]! == BinderInfo.implicit || bInfos[i]! == BinderInfo.strictImplicit) then continue if !(← isHigherOrder (← inferType args[i])) then continue if getPPAnalyzeTrustId (← getOptions) && isIdLike args[i]! then continue @@ -520,7 +520,7 @@ mutual -- motivation: prevent levels from printing in -- Boo.mk : {α : Type u_1} → {β : Type u_2} → α → β → Boo.{u_1, u_2} α β let { args, mvars, bInfos, ..} ← read - for h : i in [:args.size] do + for h : i in *...args.size do if bInfos[i]! == BinderInfo.default then if ← valUnknown mvars[i]! <&&> isTrivialBottomUp args[i] then tryUnify args[i]! mvars[i]! @@ -533,7 +533,7 @@ mutual match ← getExpr, mvarType with | Expr.lam .., Expr.forallE _ t b .. => let mut annotated := false - for i in [:argIdx] do + for i in *...argIdx do if ← pure (bInfos[i]! == BinderInfo.implicit) <&&> valUnknown mvars[i]! <&&> withNewMCtxDepth (checkpointDefEq t mvars[i]!) then annotateBool `pp.funBinderTypes tryUnify args[i]! mvars[i]! @@ -546,7 +546,7 @@ mutual | _, _ => return false - for i in [:args.size] do + for i in *...args.size do if bInfos[i]! == BinderInfo.default then let b ← withNaryArg i (core i (← inferType mvars[i]!)) if b then modify fun s => { s with funBinders := s.funBinders.set! i true } @@ -609,7 +609,7 @@ mutual let { f, args, bInfos, ..} ← read if (← get).namedArgs.any nameNotRoundtrippable then annotateBool `pp.explicit - for i in [:args.size] do + for i in *...args.size do if !(← get).provideds[i]! then withNaryArg (f.getAppNumArgs + i) do annotateBool `pp.analysis.hole if bInfos[i]! == BinderInfo.instImplicit && getPPInstanceTypes (← getOptions) then diff --git a/src/Lean/Server/CodeActions/Provider.lean b/src/Lean/Server/CodeActions/Provider.lean index 976069f5db..c060e86110 100644 --- a/src/Lean/Server/CodeActions/Provider.lean +++ b/src/Lean/Server/CodeActions/Provider.lean @@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Mario Carneiro -/ prelude +import Std.Data.Iterators.Producers.Range +import Std.Data.Iterators.Combinators.StepSize import Lean.Elab.BuiltinTerm import Lean.Elab.BuiltinNotation import Lean.Server.InfoUtils @@ -111,14 +113,14 @@ where let (stack, stx) := ((stx[0], argIdx) :: (stx, 0) :: stack, stx[0][argIdx]) let mainRes := stx[0].getPos?.map fun pos => let i := Id.run do - for i in [0:stx.getNumArgs] do + for i in *...stx.getNumArgs do if let some pos' := stx[2*i].getPos? then if range.stop < pos' then return i (stx.getNumArgs + 1) / 2 .tacticSeq (bracket || preferred pos) i ((stx, 0) :: stack) let mut childRes := none - for i in [0:stx.getNumArgs:2] do + for i in (*...stx.getNumArgs).iter.stepSize 2 do if let some inner := visit stx[i] then let stack := (stx, i) :: stack if let some child := (← go stack stx[i]) <|> @@ -130,7 +132,7 @@ where else let mut childRes := none let mut prev? := prev? - for i in [0:stx.getNumArgs] do + for i in *...stx.getNumArgs do if let some _ := visit stx[i] prev? then if let some child ← go ((stx, i) :: stack) stx[i] prev? then if childRes.isSome then failure diff --git a/src/Lean/Server/FileWorker/ExampleHover.lean b/src/Lean/Server/FileWorker/ExampleHover.lean index 63302677b3..3e413ce881 100644 --- a/src/Lean/Server/FileWorker/ExampleHover.lean +++ b/src/Lean/Server/FileWorker/ExampleHover.lean @@ -27,7 +27,7 @@ line comment marker. private def addCommentAt (indent : Nat) (line : String) : String := Id.run do let s := "".pushn ' ' indent ++ "-- " let mut iter := line.iter - for _i in [0:indent] do + for _i in *...indent do if h : iter.hasNext then if iter.curr' h == ' ' then iter := iter.next' h diff --git a/src/Lean/Server/FileWorker/SignatureHelp.lean b/src/Lean/Server/FileWorker/SignatureHelp.lean index cfc1835792..f415277ec2 100644 --- a/src/Lean/Server/FileWorker/SignatureHelp.lean +++ b/src/Lean/Server/FileWorker/SignatureHelp.lean @@ -119,7 +119,7 @@ def findSignatureHelp? (text : FileMap) (ctx? : Option Lsp.SignatureHelpContext) | return none let stack := stack.toArray.map (·.1) let mut candidates : Array Candidate := #[] - for h:i in [0:stack.size] do + for h:i in *...stack.size do let stx := stack[i] let parent := stack[i+1]?.getD .missing let (kind?, control) := determineCandidateKind stx parent diff --git a/src/Lean/Server/References.lean b/src/Lean/Server/References.lean index 748ba58a71..17a14d6ad0 100644 --- a/src/Lean/Server/References.lean +++ b/src/Lean/Server/References.lean @@ -413,7 +413,7 @@ has a name or uri that is not identical to the others. -/ def ModuleImport.collapseIdenticalImports? (identicalImports : Array ModuleImport) : Option ModuleImport := do let mut acc ← identicalImports[0]? - for h:i in [1:identicalImports.size] do + for h:i in 1...identicalImports.size do let «import» := identicalImports[i] guard <| acc.module == «import».module guard <| acc.uri == «import».uri diff --git a/src/Lean/Structure.lean b/src/Lean/Structure.lean index d5f68c6088..10b0af3dcd 100644 --- a/src/Lean/Structure.lean +++ b/src/Lean/Structure.lean @@ -491,9 +491,9 @@ where selectParent (resOrders : Array (Array Name)) : m (Bool × Name) := do -- Assumption: every resOrder is nonempty. -- `n'` is for relaxation, to stop paying attention to end of `resOrders` when finding a good parent. - for n' in [0 : resOrders.size] do + for n' in *...resOrders.size do let hi := resOrders.size - n' - for i in [0 : hi] do + for i in *...hi do let parent := resOrders[i]![0]! let consistent resOrder := resOrder[1...*].all (· != parent) if resOrders[*....2 where collideSamples : StateM ThreadWithCollideMaps Unit := do - for oldSampleIdx in [0:add.samples.length] do + for oldSampleIdx in *...add.samples.length do let oldStackIdx := add.samples.stack[oldSampleIdx]! let stackIdx ← collideStacks oldStackIdx modify fun thread => diff --git a/src/Lean/Widget/Diff.lean b/src/Lean/Widget/Diff.lean index 29195ba6b2..44c7465524 100644 --- a/src/Lean/Widget/Diff.lean +++ b/src/Lean/Widget/Diff.lean @@ -171,7 +171,7 @@ partial def exprDiffCore (before after : SubExpr) : MetaM ExprDiff := do ⟨body₀.instantiateRev fvars.toArray, before.pos.pushNthBindingBody s.length⟩ after ) <|> (pure ∅) - for i in [0:s.length] do + for i in *...s.length do δ := δ.insertBeforeChange (before.pos.pushNthBindingDomain i) .delete -- [todo] maybe here insert a tag on the after case indicating an expression was deleted above the expression? return δ diff --git a/src/Std/Time/Zoned/Database/Basic.lean b/src/Std/Time/Zoned/Database/Basic.lean index e90d36c33b..c03a08b350 100644 --- a/src/Std/Time/Zoned/Database/Basic.lean +++ b/src/Std/Time/Zoned/Database/Basic.lean @@ -77,14 +77,14 @@ Converts a `TZif.TZifV1` structure to a `ZoneRules` structure. def convertTZifV1 (tz : TZif.TZifV1) (id : String) : Except String ZoneRules := do let mut times : Array LocalTimeType := #[] - for i in [0:tz.header.typecnt.toNat] do + for i in *...tz.header.typecnt.toNat do if let some result := convertLocalTimeType i tz id then times := times.push result else .error s!"cannot convert local time {i} of the file" let mut transitions := #[] - for i in [0:tz.transitionTimes.size] do + for i in *...tz.transitionTimes.size do if let some result := convertTransition times i tz then transitions := transitions.push result else .error s!"cannot convert transition {i} of the file" diff --git a/src/Std/Time/Zoned/Database/TzIf.lean b/src/Std/Time/Zoned/Database/TzIf.lean index 00fe6fda61..514749fe97 100644 --- a/src/Std/Time/Zoned/Database/TzIf.lean +++ b/src/Std/Time/Zoned/Database/TzIf.lean @@ -4,7 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Sofia Rodrigues -/ prelude -import Init.Data.Range +import Init.Data.Range.Polymorphic.Nat +import Init.Data.Range.Polymorphic.Iterators import Std.Internal.Parsec import Std.Internal.Parsec.ByteArray @@ -194,7 +195,7 @@ private def toInt64 (bs : ByteArray) : Int64 := private def manyN (n : Nat) (p : Parser α) : Parser (Array α) := do let mut result := #[] - for _ in [0:n] do + for _ in *...n do let x ← p result := result.push x return result @@ -242,7 +243,7 @@ private def parseAbbreviations (times : Array LocalTimeType) (n : UInt32) : Pars let mut chars ← manyN n.toNat pu8 for time in times do - for indx in [time.abbreviationIndex.toNat:n.toNat] do + for indx in time.abbreviationIndex.toNat...n.toNat do let char := chars[indx]! if char = 0 then strings := strings.push current diff --git a/tests/bench/binarytrees.st.lean b/tests/bench/binarytrees.st.lean index f28a73e3af..cfac2ae7d9 100644 --- a/tests/bench/binarytrees.st.lean +++ b/tests/bench/binarytrees.st.lean @@ -1,3 +1,6 @@ +import Std.Data.Iterators.Producers.Range +import Std.Data.Iterators.Combinators.StepSize + inductive Tree | nil | node (l r : Tree) @@ -42,7 +45,7 @@ def main : List String → IO UInt32 let long := make $ UInt32.ofNat maxN -- allocate, walk, and deallocate many bottom-up binary trees - for d in [minN:maxN+1:2] do + for d in (minN...=maxN).iter.stepSize 2 do let n := 2 ^ (maxN - d + minN) let i := sumT (.ofNat d) (.ofNat n) 0 out s!"{n}\t trees" d i diff --git a/tests/bench/channel.lean b/tests/bench/channel.lean index 99ad375600..110a1ca516 100644 --- a/tests/bench/channel.lean +++ b/tests/bench/channel.lean @@ -25,19 +25,19 @@ def MESSAGES : Nat := 100_000 def THREADS : Nat := 4 def seq (ch : Std.CloseableChannel.Sync Nat) (amount : Nat) : IO Unit := do - for i in [:amount] do + for i in *...amount do ch.send i - for _ in [:amount] do + for _ in *...amount do discard <| ch.recv def spsc (ch : Std.CloseableChannel.Sync Nat) (amount : Nat) : IO Unit := do let t1 ← IO.asTask (prio := .dedicated) do - for i in [:amount] do + for i in *...amount do ch.send i let t2 ← BaseIO.asTask (prio := .dedicated) do - for _ in [:amount] do + for _ in *...amount do discard <| ch.recv IO.ofExcept (← IO.wait t1) @@ -45,14 +45,14 @@ def spsc (ch : Std.CloseableChannel.Sync Nat) (amount : Nat) : IO Unit := do def mpsc (ch : Std.CloseableChannel.Sync Nat) (amount : Nat) : IO Unit := do let mut producers := Array.emptyWithCapacity THREADS - for _ in [:THREADS] do + for _ in *...THREADS do let t ← IO.asTask (prio := .dedicated) do - for i in [:(amount/THREADS)] do + for i in *...(amount/THREADS) do ch.send i producers := producers.push t let consumer ← BaseIO.asTask (prio := .dedicated) do - for _ in [:amount] do + for _ in *...amount do discard <| ch.recv IO.wait consumer @@ -61,14 +61,14 @@ def mpsc (ch : Std.CloseableChannel.Sync Nat) (amount : Nat) : IO Unit := do def mpmc (ch : Std.CloseableChannel.Sync Nat) (amount : Nat) : IO Unit := do let mut producers := Array.emptyWithCapacity THREADS - for _ in [:THREADS] do + for _ in *...THREADS do let t ← IO.asTask (prio := .dedicated) do - for i in [:(amount/THREADS)] do + for i in *...(amount/THREADS) do ch.send i producers := producers.push t let mut consumers := Array.emptyWithCapacity THREADS - for _ in [:THREADS] do + for _ in *...THREADS do let t ← IO.asTask (prio := .dedicated) do while true do if let some _ ← ch.recv then diff --git a/tests/bench/identifier_completion_runner.lean b/tests/bench/identifier_completion_runner.lean index 8201c244f6..14ce1aed37 100644 --- a/tests/bench/identifier_completion_runner.lean +++ b/tests/bench/identifier_completion_runner.lean @@ -21,7 +21,7 @@ def main : IO Unit := do Ipc.writeRequest <| mkCompletionRequest 1 let _ ← Ipc.readResponseAs 1 CompletionList let startTime ← IO.monoMsNow - for i in [2:5] do + for i in 2...(5 : Nat) do Ipc.writeRequest <| mkCompletionRequest i let _ ← Ipc.readResponseAs i CompletionList let endTime ← IO.monoMsNow diff --git a/tests/bench/ilean_roundtrip.lean b/tests/bench/ilean_roundtrip.lean index 53fe36983d..a843e5db45 100644 --- a/tests/bench/ilean_roundtrip.lean +++ b/tests/bench/ilean_roundtrip.lean @@ -20,7 +20,7 @@ def genModuleRefs (n : Nat) : IO Lean.Lsp.ModuleRefs := do } let mut refs : Lean.Lsp.ModuleRefs := .empty - for i in [0:n] do + for i in *...n do let someIdent := Lean.Lsp.RefIdent.const s!"A.Reasonably.Long.Module.Name{i}" s!"A.Reasonably.Long.Declaration.Name.foobar{i}" refs := refs.insert someIdent someInfo diff --git a/tests/bench/inundation/lakefile.lean b/tests/bench/inundation/lakefile.lean index b34ac25798..113bdf3129 100644 --- a/tests/bench/inundation/lakefile.lean +++ b/tests/bench/inundation/lakefile.lean @@ -33,7 +33,7 @@ script mkTree (args : List String) := do let treeDir := wsDir / "test" / "tree" let config ← IO.FS.readFile (wsDir / "lakefile.lean") let mut depsConfig := config ++ "\n" - for i in [:numPkgs] do + for i in *...numPkgs do let pkgName := num2letters i let config := config.replace "inundation" pkgName let pkgDir := treeDir / pkgName @@ -58,7 +58,7 @@ script mkBuild (args : List String) := do let mkImportsFor (layer : Nat) := Id.run do let mut out := "" - for idx in [:width] do + for idx in *...width do out := out ++ s!"import {test}.{num2letters layer}{idx}\n" return out let mkImportsAt (layer : Nat) := @@ -71,8 +71,8 @@ script mkBuild (args : List String) := do | .noFileOrDirectory .. => pure () | e => throw e IO.FS.createDirAll (testDir / test) - for layer in [:layers] do - for idx in [:width] do + for layer in *...layers do + for idx in *...width do IO.FS.writeFile (testDir / test / s!"{num2letters layer}{idx}.lean") <| mkImportsAt layer IO.FS.writeFile (testDir / s!"{test}.lean") (mkImportsAt layers) diff --git a/tests/bench/liasolver.lean b/tests/bench/liasolver.lean index e522256277..df9fe6815f 100644 --- a/tests/bench/liasolver.lean +++ b/tests/bench/liasolver.lean @@ -5,6 +5,8 @@ Author: Marc Huisinga -/ import Lean.Data.AssocList import Std.Data.HashMap +import Std.Data.Iterators.Producers.Range +import Std.Data.Iterators.Combinators.StepSize open Lean @@ -274,7 +276,7 @@ partial def readSolution? (p : Problem) : Option Solution := Id.run <| do if p.equations.any (fun _ eq => eq.const ≠ 0) then return some Solution.unsat let mut assignment : Array (Option Int) := mkArray p.nVars none - for i in [0:p.nVars] do + for i in *...p.nVars do assignment := readSolution i assignment return Solution.sat <| assignment.map (·.get!) where @@ -348,7 +350,7 @@ def main (args : List String) : IO UInt32 := do | error "Non-zero end of line symbol" let const ← elems.ithVal (elems.size - 2) "constant value" let mut coeffs := ∅ - for i in [1:elems.size-2:2] do + for i in ((1 : Nat)...(elems.size-2)).iter.stepSize 2 do let coeff ← elems.ithVal i "coefficient" let varIdx ← elems.ithVal (i + 1) "variable index" if varIdx < 1 then diff --git a/tests/bench/nat_repr.lean b/tests/bench/nat_repr.lean index 76c2dabb3d..c71c9378c3 100644 --- a/tests/bench/nat_repr.lean +++ b/tests/bench/nat_repr.lean @@ -1,8 +1,8 @@ def main : List String → IO Unit | [n] => do let mut s := 0 - for i in [0:n.toNat!] do - for j in [:i] do + for i in *...n.toNat! do + for j in *...i do s := s + j.repr.length IO.println s | _ => throw $ IO.userError "give upper bound" diff --git a/tests/bench/parser.lean b/tests/bench/parser.lean index 9d6807bddd..86f931230a 100644 --- a/tests/bench/parser.lean +++ b/tests/bench/parser.lean @@ -7,6 +7,6 @@ import Lean.Parser.Module def main : List String → IO Unit | [fname, n] => do let env ← Lean.mkEmptyEnvironment - for _ in [0:n.toNat!] do + for _ in *...n.toNat! do discard $ Lean.Parser.testParseFile env fname | _ => throw $ IO.userError "give file and iteration count" diff --git a/tests/bench/reduceMatch.lean b/tests/bench/reduceMatch.lean index 3f997c6a04..2f11d51d9e 100644 --- a/tests/bench/reduceMatch.lean +++ b/tests/bench/reduceMatch.lean @@ -32,6 +32,6 @@ def parts : List (List Nat) := List.insert ([1, 1, 0, 0]) <| List.insert ([0, 0, List.insert [1, 2, 3, 4] <| List.insert [5, 6, 7, 8] [] #eval show Lean.Elab.Command.CommandElabM _ from - for _ in [0:10] do + for _ in *...(10 : Nat) do Lean.Elab.Command.elabCommand (← `(example : ∀ (x) (_ : x ∈ parts) (y) (_ : y ∈ parts), x ++ y ∉ parts := by decide)) diff --git a/tests/bench/simp_arith1.lean b/tests/bench/simp_arith1.lean index 7f80c9ebfc..09407cf0e8 100644 --- a/tests/bench/simp_arith1.lean +++ b/tests/bench/simp_arith1.lean @@ -11,8 +11,8 @@ elab "largeGoal%" : term => withLocalDeclsD decls fun xs => do let mut e₁ : Expr := mkNatLit 42 let mut e₂ : Expr := mkNatLit 23 - for _ in [:r] do - for i in [:xs.size] do + for _ in *...r do + for i in *...xs.size do e₁ := mkAdd (mkMul (mkNatLit i) e₁) xs[i]! e₂ := mkAdd xs[i]! (mkMul e₂ (mkNatLit (xs.size - i))) let goal ← mkEq e₁ e₂ diff --git a/tests/bench/speedcenter.exec.velcom.yaml b/tests/bench/speedcenter.exec.velcom.yaml index 809a92ed22..8f1d30ad03 100644 --- a/tests/bench/speedcenter.exec.velcom.yaml +++ b/tests/bench/speedcenter.exec.velcom.yaml @@ -509,3 +509,9 @@ run_config: <<: *time cmd: lean iterators.lean +- attributes: + description: workspaceSymbols with new ranges + tags: [fast] + run_config: + <<: *time + cmd: lean workspaceSymbolsNewRanges.lean diff --git a/tests/bench/workspaceSymbolsNewRanges.lean b/tests/bench/workspaceSymbolsNewRanges.lean new file mode 100644 index 0000000000..3afcebc829 --- /dev/null +++ b/tests/bench/workspaceSymbolsNewRanges.lean @@ -0,0 +1,244 @@ +/- +Copyright (c) 2022 Lars König. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Lars König + +This benchmark evaluates the performance of fuzzy matching when using the new ranges. +-/ +import Lean + +@[specialize] private def iterateLookaround (f : (Option Char × Char × Option Char) → α) (string : String) : Array α := + if string.isEmpty then + #[] + else if string.length == 1 then + #[f (none, string.get 0, none)] + else Id.run do + let mut result := Array.mkEmpty string.length + result := result.push <| f (none, string.get 0, string.get ⟨1⟩) + -- TODO: the following code is assuming all characters are ASCII + for i in 2...string.length do + result := result.push <| f (string.get ⟨i - 2⟩, string.get ⟨i - 1⟩, string.get ⟨i⟩) + result.push <| f (string.get ⟨string.length - 2⟩, string.get ⟨string.length - 1⟩, none) + +private def containsInOrderLower (a b : String) : Bool := Id.run do + if a.isEmpty then + return true + let mut aIt := a.mkIterator + -- TODO: the following code is assuming all characters are ASCII + for i in *...b.endPos.byteIdx do + if aIt.curr.toLower == (b.get ⟨i⟩).toLower then + aIt := aIt.next + if !aIt.hasNext then + return true + return false + +/-- Represents the type of a single character. -/ +inductive CharType where + | lower | upper | separator + +def charType (c : Char) : CharType := + if c.isAlphanum then + if c.isUpper + then CharType.upper + else CharType.lower + else + CharType.separator + + +/-- Represents the role of a character inside a word. -/ +inductive CharRole where + | head | tail | separator + deriving Inhabited + +@[inline] def charRole (prev? : Option CharType) (curr : CharType) (next?: Option CharType) : CharRole := + if curr matches CharType.separator then + CharRole.separator + else if prev?.isNone || prev? matches some CharType.separator then + CharRole.head + else if curr matches CharType.lower then + CharRole.tail + else if prev? matches some CharType.upper && !(next? matches some CharType.lower) then + CharRole.tail + else + CharRole.head + +/-- Add additional information to each character in a string. -/ +private def stringInfo (s : String) : Array CharRole := + iterateLookaround (string := s) fun (prev?, curr, next?) => + charRole (prev?.map charType) (charType curr) (next?.map charType) + + +private def selectBest (missScore? matchScore? : Option Int) : Option Int := + match (missScore?, matchScore?) with + | (missScore, none) => missScore + | (none, matchScore) => matchScore + | (some missScore, some matchScore) => + some <| max missScore matchScore + +private def fuzzyMatchCore (pattern word : String) (patternRoles wordRoles : Array CharRole) : Option Int := Id.run do + /- Flattened array where the value at index (i, j, k) represents the best possible score of a fuzzy match + between the substrings pattern[*...=i] and word[*...j] assuming that pattern[i] misses at word[j] (k = 0, i.e. + it was matched earlier), or matches at word[j] (k = 1). A value of `none` corresponds to a score of -∞, and is used + where no such match/miss is possible or for unneeded parts of the table. -/ + let mut result : Array (Option Int) := Array.replicate (pattern.length * word.length * 2) none + let mut runLengths : Array Int := Array.replicate (pattern.length * word.length) 0 + + -- penalty for starting a consecutive run at each index + let mut startPenalties : Array Int := Array.replicate word.length 0 + + let mut lastSepIdx := 0 + let mut penaltyNs : Int := 0 + let mut penaltySkip : Int := 0 + for wordIdx in *...word.length do + if (wordIdx != 0) && wordRoles[wordIdx]! matches .separator then + -- reset skip penalty at namespace separator + penaltySkip := 0 + -- add constant penalty for each namespace to prefer shorter namespace nestings + penaltyNs := penaltyNs + 1 + lastSepIdx := wordIdx + penaltySkip := penaltySkip + skipPenalty wordRoles[wordIdx]! (wordIdx == 0) + startPenalties := startPenalties.set! wordIdx $ penaltySkip + penaltyNs + + -- TODO: the following code is assuming all characters are ASCII + for patternIdx in *...pattern.length do + /- For this dynamic program to be correct, it's only necessary to populate a range of length + `word.length - pattern.length` at each index (because at the very end, we can only consider fuzzy matches + of `pattern` with a longer substring of `word`). -/ + for wordIdx in patternIdx...(word.length-(pattern.length - patternIdx - 1)) do + let missScore? := + if wordIdx >= 1 then + selectBest + (getMiss result patternIdx (wordIdx - 1)) + (getMatch result patternIdx (wordIdx - 1)) + else none + + let mut matchScore? := none + + if allowMatch (pattern.get ⟨patternIdx⟩) (word.get ⟨wordIdx⟩) patternRoles[patternIdx]! wordRoles[wordIdx]! then + if patternIdx >= 1 then + let runLength := runLengths[getIdx (patternIdx - 1) (wordIdx - 1)]! + 1 + runLengths := runLengths.set! (getIdx patternIdx wordIdx) runLength + + matchScore? := selectBest + (getMiss result (patternIdx - 1) (wordIdx - 1) |>.map (· + matchResult + patternIdx wordIdx + patternRoles[patternIdx]! wordRoles[wordIdx]! + none + - startPenalties[wordIdx]!)) + (getMatch result (patternIdx - 1) (wordIdx - 1) |>.map (· + matchResult + patternIdx wordIdx + patternRoles[patternIdx]! wordRoles[wordIdx]! + (.some runLength) + )) |>.map fun score => if wordIdx >= lastSepIdx then score + 1 else score -- main identifier bonus + else + runLengths := runLengths.set! (getIdx patternIdx wordIdx) 1 + matchScore? := .some $ matchResult + patternIdx wordIdx + patternRoles[patternIdx]! wordRoles[wordIdx]! + none + - startPenalties[wordIdx]! + + result := set result patternIdx wordIdx missScore? matchScore? + + return selectBest (getMiss result (pattern.length - 1) (word.length - 1)) (getMatch result (pattern.length - 1) (word.length - 1)) + + where + getDoubleIdx (patternIdx wordIdx : Nat) := patternIdx * word.length * 2 + wordIdx * 2 + + getIdx (patternIdx wordIdx : Nat) := patternIdx * word.length + wordIdx + + getMiss (result : Array (Option Int)) (patternIdx wordIdx : Nat) : Option Int := + result[getDoubleIdx patternIdx wordIdx]! + + getMatch (result : Array (Option Int)) (patternIdx wordIdx : Nat) : Option Int := + result[getDoubleIdx patternIdx wordIdx + 1]! + + set (result : Array (Option Int)) (patternIdx wordIdx : Nat) (missValue matchValue : Option Int) : Array (Option Int) := + let idx := getDoubleIdx patternIdx wordIdx + result |>.set! idx missValue |>.set! (idx + 1) matchValue + + /-- Heuristic to penalize skipping characters in the word. -/ + skipPenalty (wordRole : CharRole) (wordStart : Bool) : Int := Id.run do + /- Skipping the beginning of the word. -/ + if wordStart then + return 3 + /- Skipping the beginning of a segment. -/ + if wordRole matches CharRole.head then + return 1 + + return 0 + + /-- Whether characters from the pattern and the word match. -/ + allowMatch (patternChar wordChar : Char) (patternRole wordRole : CharRole) : Bool := Id.run do + /- Different characters do not match. -/ + if patternChar.toLower != wordChar.toLower then + return false + /- The beginning of a segment in the pattern must align with the beginning of a segment in the word. -/ + if patternRole matches CharRole.head && !(wordRole matches CharRole.head) then + return false + + return true + + /-- Heuristic to rate a match. -/ + matchResult (patternIdx wordIdx : Nat) (patternRole wordRole : CharRole) (consecutive : Option Int) : Int := Id.run do + let mut score : Int := 1 + /- Case-sensitive equality or beginning of a segment in pattern and word. -/ + if (pattern.get ⟨patternIdx⟩) == (word.get ⟨wordIdx⟩) || (patternRole matches CharRole.head && wordRole matches CharRole.head) then + score := score + 1 + /- Matched end of word with end of pattern -/ + if wordIdx == word.length - 1 && patternIdx == pattern.length - 1 then + score := score + 2 + /- Matched beginning of the word. -/ + if (wordIdx == 0) then + score := score + 3 + /- Consecutive character match. -/ + if let some bonus := consecutive then + /- consecutive run bonus -/ + score := score + bonus + return score + +/-- Match the given pattern with the given word using a fuzzy matching +algorithm. The resulting scores are in the interval `[0, 1]` or `none` if no +match was found. -/ +def fuzzyMatchScore? (pattern word : String) : Option Float := Id.run do + /- Some fast and simple checks. -/ + if pattern.isEmpty then + return some 1 + if pattern.length > word.length then + return none + if !(containsInOrderLower pattern word) then + return none + + let some score := fuzzyMatchCore pattern word (stringInfo pattern) (stringInfo word) + | none + let mut score := score + + /- Bonus if every character is matched. -/ + if pattern.length == word.length then + score := score * 2 + + /- Perfect score per character. -/ + let perfect := 4 + /- Perfect score for full match given the heuristic in `matchResult`; + the latter term represents the bonus of a perfect consecutive run. -/ + let perfectMatch := (perfect * pattern.length + ((pattern.length * (pattern.length + 1) / 2) - 1)) + let normScore := Float.ofInt score / Float.ofInt perfectMatch + + return some <| min 1 (max 0 normScore) + +def fuzzyMatchScoreWithThreshold? (pattern word : String) (threshold := 0.1) : Option Float := + fuzzyMatchScore? pattern word |>.filter (· > threshold) + +/-- Match the given pattern with the given word using a fuzzy matching +algorithm. Return `false` if no match was found or the found match received a +score below the given threshold. -/ +def fuzzyMatch (pattern word : String) (threshold := 0.2) : Bool := + fuzzyMatchScoreWithThreshold? pattern word threshold |>.isSome + +open Lean Elab + +def orderFuzzyMatches (names : Array Name) (pattern : String) : Array Name := + names.filterMap (fun n => (n, ·) <$> fuzzyMatchScoreWithThreshold? pattern n.toString) |>.qsort (·.2 ≥ ·.2) |>.map (·.1) + +-- patterns matching at the end of a name should get a bonus +#eval orderFuzzyMatches #[`Array.extract, `Lean.extractMainModule] "extract" diff --git a/tests/lean/run/1420.lean b/tests/lean/run/1420.lean index edea369c4f..7c915ae6e7 100644 --- a/tests/lean/run/1420.lean +++ b/tests/lean/run/1420.lean @@ -1,5 +1,5 @@ example : Nat := Id.run do - for _ in [1:10] do + for _ in 1...(10 : Nat) do assert! true if false then return 0 return 0 diff --git a/tests/lean/run/2137.lean b/tests/lean/run/2137.lean index b039eb5ea5..96647cfc12 100644 --- a/tests/lean/run/2137.lean +++ b/tests/lean/run/2137.lean @@ -12,7 +12,7 @@ def main (_ : List String) : IO UInt32 := do makeProc IO.println "done test" - for _ in [0:6] do + for _ in *...(6 : Nat) do let _ ← IO.asTask makeProc return 0 diff --git a/tests/lean/run/646.lean b/tests/lean/run/646.lean index 5438956705..cf974771b3 100644 --- a/tests/lean/run/646.lean +++ b/tests/lean/run/646.lean @@ -1,6 +1,6 @@ def build (n : Nat) : Array Unit := Id.run <| do let mut out := #[] - for _ in [0:n] do + for _ in *...n do out := out.push () out @@ -10,7 +10,7 @@ def bench (f : ∀ {α : Type}, α → IO Unit := fun _ => pure ()) : IO Unit := let n ← size let arr := build n timeit "time" $ - for _ in [:1000] do + for _ in *...(1000 : Nat) do f $ #[1, 2, 3, 4].map fun ty => arr[ty]! #eval bench diff --git a/tests/lean/run/bv_popcount.lean b/tests/lean/run/bv_popcount.lean index 0b38ead139..cb710a9c8e 100644 --- a/tests/lean/run/bv_popcount.lean +++ b/tests/lean/run/bv_popcount.lean @@ -21,7 +21,7 @@ int pop_spec(uint32_t x) { def pop_spec (x : BitVec 32) : BitVec 32 := Id.run do let mut pop : BitVec 32 := 0 let mut mask : BitVec 32 := 1 - for _ in [0:32] do + for _ in *...(32 : Nat) do if (x &&& mask != 0) then pop := pop + 1 mask := mask <<< 1 diff --git a/tests/lean/run/forInRangeWF.lean b/tests/lean/run/forInRangeWF.lean index 4096f36173..fa0c91253b 100644 --- a/tests/lean/run/forInRangeWF.lean +++ b/tests/lean/run/forInRangeWF.lean @@ -5,7 +5,7 @@ def Expr.size (e : Expr) : Nat := Id.run do match e with | app f args => let mut sz := 1 - for h : i in [: args.size] do + for h : i in *...args.size do sz := sz + size args[i] return sz diff --git a/tests/lean/run/forIn_phashset.lean b/tests/lean/run/forIn_phashset.lean index d2f27a51f3..235c3f29b0 100644 --- a/tests/lean/run/forIn_phashset.lean +++ b/tests/lean/run/forIn_phashset.lean @@ -18,7 +18,7 @@ def sumIf (s : PHashSet Nat) (p : Nat → Bool) : Nat := Id.run do def mk [Hashable α] [BEq α] (f : Nat → α) (n : Nat) : PHashSet α := Id.run do let mut s := {} - for i in [:n] do + for i in *...n do s := s.insert (f i) return s diff --git a/tests/lean/run/forOutParamIssue.lean b/tests/lean/run/forOutParamIssue.lean index 18eff72240..5e3909347c 100644 --- a/tests/lean/run/forOutParamIssue.lean +++ b/tests/lean/run/forOutParamIssue.lean @@ -10,12 +10,12 @@ instance : GetElem (Array α) Nat α where opaque f : Option Bool → Id Unit def bad2 (bs : Array Bool) (n : Nat) : Id Unit := do - for idx in [:n] do + for idx in *...n do let b := getElem bs idx f b def bad3 (bs : Array Bool) (n : Nat) : Id Unit := do - for h : idx in [:n] do + for h : idx in *...n do let b := getElem bs idx f b diff --git a/tests/lean/run/lcnfInferProjTypeIssue.lean b/tests/lean/run/lcnfInferProjTypeIssue.lean index 53376a671a..704e99b370 100644 --- a/tests/lean/run/lcnfInferProjTypeIssue.lean +++ b/tests/lean/run/lcnfInferProjTypeIssue.lean @@ -14,14 +14,14 @@ def NFloatArray (n : Nat) := {a : FloatArray // a.size = n} instance {n} : Add (NFloatArray n) := ⟨λ x y => Id.run do let mut x := x.1 - for i in [0:n] do + for i in *...n do x := x.set i (x[i]'sorry+y.1[i]'sorry) sorry ⟨x,sorry⟩⟩ instance {n} : HMul Float (NFloatArray n) (NFloatArray n) := ⟨λ s x => Id.run do let mut x := x.1 - for i in [0:n] do + for i in *...n do x := x.set i (s*x[i]'sorry) sorry ⟨x,sorry⟩⟩ diff --git a/tests/lean/run/letToHaveCleanup.lean b/tests/lean/run/letToHaveCleanup.lean index dd13cf1d67..1215e785c9 100644 --- a/tests/lean/run/letToHaveCleanup.lean +++ b/tests/lean/run/letToHaveCleanup.lean @@ -260,7 +260,7 @@ def fnDo (x : MetaM Bool) (y : Nat → MetaM α) : MetaM (Array α) := do let a := (← x) if a then let mut arr := #[] - for i in [0:10] do + for i in *...(10 : Nat) do let b := (← y i) arr := arr.push b return arr @@ -275,7 +275,7 @@ fun {α} x y => do have arr : Array α := #[]; do let r ← - forIn { stop := 10, step_pos := Nat.zero_lt_one } arr fun i r => + forIn { lower := PUnit.unit, upper := 10 } arr fun i r => have arr : Array α := r; do let __do_lift ← y i diff --git a/tests/lean/run/sarray.lean b/tests/lean/run/sarray.lean index 8fa645b410..62586c45dd 100644 --- a/tests/lean/run/sarray.lean +++ b/tests/lean/run/sarray.lean @@ -1,6 +1,6 @@ def mkByteArray (n : Nat) : ByteArray := Id.run <| do let mut r := {} - for i in [:n] do + for i in *...n do r := r.push (UInt8.ofNat i) return r @@ -29,7 +29,7 @@ def tst2 (n : Nat) (expected : UInt32) : IO Unit := do def tst3 (n : Nat) (expected : UInt32) : IO Unit := do let bs := mkByteArray n let mut sum := 0 - for i in [:bs.size] do + for i in *...bs.size do sum := sum + bs[i]!.toUInt32 assert! sum == expected IO.println sum diff --git a/tests/lean/run/structure_recursive.lean b/tests/lean/run/structure_recursive.lean index a2c9f5775f..0a07e33829 100644 --- a/tests/lean/run/structure_recursive.lean +++ b/tests/lean/run/structure_recursive.lean @@ -94,8 +94,8 @@ structure Foo' where def Foo'.preorder : Foo' → String | {name, n, children} => Id.run do let mut acc := name - for h : i in [0:n] do - acc := acc ++ (children ⟨i, h.2.1⟩).preorder + for h : i in *...n do + acc := acc ++ (children ⟨i, h.2⟩).preorder return acc /-- info: Foo'.preorder : Foo' → String -/ diff --git a/tests/lean/run/sync_barrier.lean b/tests/lean/run/sync_barrier.lean index 4d26e8844e..a650b16375 100644 --- a/tests/lean/run/sync_barrier.lean +++ b/tests/lean/run/sync_barrier.lean @@ -1,10 +1,10 @@ import Std.Sync.Barrier def consBarrier (b : Std.Barrier) (list : IO.Ref (List Nat)) : IO Bool := do - for _ in [0:1000] do + for _ in *...(1000 : Nat) do list.modify fun l => 1 :: l let isLeader ← b.wait - for _ in [0:1000] do + for _ in *...(1000 : Nat) do list.modify fun l => 2 :: l return isLeader diff --git a/tests/lean/run/sync_channel.lean b/tests/lean/run/sync_channel.lean index add4e6c39d..e2ad29ce83 100644 --- a/tests/lean/run/sync_channel.lean +++ b/tests/lean/run/sync_channel.lean @@ -33,7 +33,7 @@ def trySend (ch : CloseableChannel Nat) (capacity : Option Nat) : IO Unit := do -- the unbounded CloseableChannel cannot go out of space so it is pointless to fill it up let some capacity := capacity | return () - for i in [:capacity] do + for i in *...capacity do assertBEq (← ch.trySend i) true assertBEq (← ch.trySend (capacity + 1)) false diff --git a/tests/lean/run/sync_mutex.lean b/tests/lean/run/sync_mutex.lean index 4fae95a9ad..a2a2e3369b 100644 --- a/tests/lean/run/sync_mutex.lean +++ b/tests/lean/run/sync_mutex.lean @@ -1,7 +1,7 @@ import Std.Sync.Mutex def countIt (mutex : Std.Mutex Nat) : IO Unit := do - for _ in [0:1000] do + for _ in *...(1000 : Nat) do mutex.atomically do modify fun s => s + 1 @@ -51,7 +51,7 @@ def tryAtomically : IO Unit := do throw <| .userError s!"Should be 3 but was {val}" def workIt (mutex : Std.Mutex Nat) (cond : Std.Condvar) : IO Unit := do - for _ in [0:1000] do + for _ in *...(1000 : Nat) do mutex.atomically do (modify fun s => s + 1) cond.notifyAll diff --git a/tests/lean/run/sync_recursive_mutex.lean b/tests/lean/run/sync_recursive_mutex.lean index e36a2be0fc..ebf19799c0 100644 --- a/tests/lean/run/sync_recursive_mutex.lean +++ b/tests/lean/run/sync_recursive_mutex.lean @@ -1,7 +1,7 @@ import Std.Sync.RecursiveMutex def countIt (mutex : Std.RecursiveMutex Nat) : IO Unit := do - for _ in [0:1000] do + for _ in *...(1000 : Nat) do mutex.atomically do modify fun s => s + 1 diff --git a/tests/lean/run/sync_shared_mutex.lean b/tests/lean/run/sync_shared_mutex.lean index ddb040dd0d..3a6e1b8721 100644 --- a/tests/lean/run/sync_shared_mutex.lean +++ b/tests/lean/run/sync_shared_mutex.lean @@ -1,7 +1,7 @@ import Std.Sync.SharedMutex def countIt (mutex : Std.SharedMutex Nat) : IO Unit := do - for _ in [0:1000] do + for _ in *...(1000 : Nat) do mutex.atomically do modify fun s => s + 1 diff --git a/tests/lean/run/tempfile.lean b/tests/lean/run/tempfile.lean index 6387c0a826..5ec931fda2 100644 --- a/tests/lean/run/tempfile.lean +++ b/tests/lean/run/tempfile.lean @@ -53,11 +53,11 @@ def testDir : IO Unit := do assert! (fileList.isEmpty) let toWrite := "Hello World" - for i in [0:3] do + for i in *...(3 : Nat) do IO.FS.withFile (path / s!"{i}.txt") .write fun h => do h.putStr toWrite h.putStr (toString i) - for i in [0:3] do + for i in *...(3 : Nat) do IO.FS.withFile (path / s!"{i}.txt") .read fun h => do let content ← h.getLine assert! (content == toWrite ++ toString i) @@ -82,11 +82,11 @@ def testWithDir : IO Unit := do assert! (fileList.isEmpty) let toWrite := "Hello World" - for i in [0:3] do + for i in *...(3 : Nat) do IO.FS.withFile (path / s!"{i}.txt") .write fun h => do h.putStr toWrite h.putStr (toString i) - for i in [0:3] do + for i in *...(3 : Nat) do IO.FS.withFile (path / s!"{i}.txt") .read fun h => do let content ← h.getLine assert! (content == toWrite ++ toString i) diff --git a/tests/lean/run/timeLocalDateTime.lean b/tests/lean/run/timeLocalDateTime.lean index 4863a63872..3ee7341a83 100644 --- a/tests/lean/run/timeLocalDateTime.lean +++ b/tests/lean/run/timeLocalDateTime.lean @@ -77,7 +77,7 @@ info: #[] #eval Id.run do let mut res := #[] - for i in [0:10000] do + for i in *...(10000 : Nat) do let i := Int.ofNat i - 999975 let date := PlainDate.ofDaysSinceUNIXEpoch (Day.Offset.ofInt i) let num := date.toDaysSinceUNIXEpoch