refactor: termination_by changes in stdlib

src/Init/Data/Array/Basic.lean

@@ -276,8 +276,8 @@ def mapM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α 
       map (i+1) (r.push (← f as[i]))
     else
       pure r
+  termination_by as.size - i
   map 0 (mkEmpty as.size)
-termination_by map => as.size - i
 
 @[inline]
 def mapIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : Fin as.size → α → m β) : m (Array β) :=
@@ -348,12 +348,12 @@ def anyM {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as :
           loop (j+1)
       else
         pure false
+      termination_by stop - j
     loop start
   if h : stop ≤ as.size then
     any stop h
   else
     any as.size (Nat.le_refl _)
-termination_by loop i j => stop - j
 
 @[inline]
 def allM {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as : Array α) (start := 0) (stop := as.size) : m Bool :=
@@ -523,7 +523,7 @@ def isEqvAux (a b : Array α) (hsz : a.size = b.size) (p : α → α → Bool) (
      p a[i] b[i] && isEqvAux a b hsz p (i+1)
   else
     true
-termination_by _ => a.size - i
+termination_by a.size - i
 
 @[inline] def isEqv (a b : Array α) (p : α → α → Bool) : Bool :=
   if h : a.size = b.size then
@@ -627,7 +627,7 @@ def indexOfAux [BEq α] (a : Array α) (v : α) (i : Nat) : Option (Fin a.size)
     if a.get idx == v then some idx
     else indexOfAux a v (i+1)
   else none
-termination_by _ => a.size - i
+termination_by a.size - i
 
 def indexOf? [BEq α] (a : Array α) (v : α) : Option (Fin a.size) :=
   indexOfAux a v 0
@@ -659,7 +659,7 @@ where
       loop as (i+1) ⟨j-1, this⟩
     else
       as
-termination_by _ => j - i
+termination_by j - i
 
 def popWhile (p : α → Bool) (as : Array α) : Array α :=
   if h : as.size > 0 then
@@ -669,7 +669,7 @@ def popWhile (p : α → Bool) (as : Array α) : Array α :=
       as
   else
     as
-termination_by popWhile as => as.size
+termination_by as.size
 
 def takeWhile (p : α → Bool) (as : Array α) : Array α :=
   let rec go (i : Nat) (r : Array α) : Array α :=
@@ -681,8 +681,8 @@ def takeWhile (p : α → Bool) (as : Array α) : Array α :=
         r
     else
       r
+    termination_by as.size - i
   go 0 #[]
-termination_by go i r => as.size - i
 
 def eraseIdxAux (i : Nat) (a : Array α) : Array α :=
   if h : i < a.size then
@@ -692,7 +692,7 @@ def eraseIdxAux (i : Nat) (a : Array α) : Array α :=
     eraseIdxAux (i+1) a'
   else
     a.pop
-termination_by _ => a.size - i
+termination_by a.size - i
 
 def feraseIdx (a : Array α) (i : Fin a.size) : Array α :=
   eraseIdxAux (i.val + 1) a
@@ -707,7 +707,7 @@ def eraseIdxSzAux (a : Array α) (i : Nat) (r : Array α) (heq : r.size = a.size
     eraseIdxSzAux a (i+1) (r.swap idx idx1) ((size_swap r idx idx1).trans heq)
   else
     ⟨r.pop, (size_pop r).trans (heq ▸ rfl)⟩
-termination_by _ => r.size - i
+termination_by r.size - i
 
 def eraseIdx' (a : Array α) (i : Fin a.size) : { r : Array α // r.size = a.size - 1 } :=
   eraseIdxSzAux a (i.val + 1) a rfl
@@ -726,10 +726,10 @@ def erase [BEq α] (as : Array α) (a : α) : Array α :=
       loop as ⟨j', by rw [size_swap]; exact j'.2⟩
     else
       as
+    termination_by j.1
   let j := as.size
   let as := as.push a
   loop as ⟨j, size_push .. ▸ j.lt_succ_self⟩
-termination_by loop j => j.1
 
 /-- Insert element `a` at position `i`. Panics if `i` is not `i ≤ as.size`. -/
 def insertAt! (as : Array α) (i : Nat) (a : α) : Array α :=
@@ -779,7 +779,7 @@ def isPrefixOfAux [BEq α] (as bs : Array α) (hle : as.size ≤ bs.size) (i : N
       false
   else
     true
-termination_by _ => as.size - i
+termination_by as.size - i
 
 /-- Return true iff `as` is a prefix of `bs`.
 That is, `bs = as ++ t` for some `t : List α`.-/
@@ -800,7 +800,7 @@ private def allDiffAux [BEq α] (as : Array α) (i : Nat) : Bool :=
     allDiffAuxAux as as[i] i h && allDiffAux as (i+1)
   else
     true
-termination_by _ => as.size - i
+termination_by as.size - i
 
 def allDiff [BEq α] (as : Array α) : Bool :=
   allDiffAux as 0
@@ -815,7 +815,7 @@ def allDiff [BEq α] (as : Array α) : Bool :=
       cs
   else
     cs
-termination_by _ => as.size - i
+termination_by as.size - i
 
 @[inline] def zipWith (as : Array α) (bs : Array β) (f : α → β → γ) : Array γ :=
   zipWithAux f as bs 0 #[]

src/Init/Data/Array/BasicAux.lean

@@ -47,7 +47,7 @@ where
       have hlt : i < as.size := Nat.lt_of_le_of_ne hle h
       let b ← f as[i]
       go (i+1) ⟨acc.val.push b, by simp [acc.property]⟩ hlt
-termination_by go i _ _ => as.size - i
+  termination_by as.size - i
 
 @[inline] private unsafe def mapMonoMImp [Monad m] (as : Array α) (f : α → m α) : m (Array α) :=
   go 0 as

src/Init/Data/Array/DecidableEq.lean

@@ -20,7 +20,7 @@ theorem eq_of_isEqvAux [DecidableEq α] (a b : Array α) (hsz : a.size = b.size)
   · have heq : i = a.size := Nat.le_antisymm hi (Nat.ge_of_not_lt h)
     subst heq
     exact absurd (Nat.lt_of_lt_of_le high low) (Nat.lt_irrefl j)
-termination_by _ => a.size - i
+termination_by a.size - i
 
 theorem eq_of_isEqv [DecidableEq α] (a b : Array α) : Array.isEqv a b (fun x y => x = y) → a = b := by
   simp [Array.isEqv]
@@ -36,7 +36,7 @@ theorem isEqvAux_self [DecidableEq α] (a : Array α) (i : Nat) : Array.isEqvAux
   split
   case inl h => simp [h, isEqvAux_self a (i+1)]
   case inr h => simp [h]
-termination_by _ => a.size - i
+termination_by a.size - i
 
 theorem isEqv_self [DecidableEq α] (a : Array α) : Array.isEqv a a (fun x y => x = y) = true := by
   simp [isEqv, isEqvAux_self]

src/Init/Data/Array/QSort.lean

@@ -26,8 +26,8 @@ def qpartition (as : Array α) (lt : α → α → Bool) (lo hi : Nat) : Nat ×
     else
       let as := as.swap! i hi
       (i, as)
+    termination_by hi - j
   loop as lo lo
-termination_by _ => hi - j
 
 @[inline] partial def qsort (as : Array α) (lt : α → α → Bool) (low := 0) (high := as.size - 1) : Array α :=
   let rec @[specialize] sort (as : Array α) (low high : Nat) :=

src/Init/Data/Nat/Power2.lean

@@ -21,8 +21,8 @@ where
       go (power * 2) (Nat.mul_pos h (by decide))
     else
       power
-termination_by go p h => n - p
-decreasing_by simp_wf; apply nextPowerOfTwo_dec <;> assumption
+  termination_by n - power
+  decreasing_by simp_wf; apply nextPowerOfTwo_dec <;> assumption
 
 def isPowerOfTwo (n : Nat) := ∃ k, n = 2 ^ k
 
@@ -48,7 +48,7 @@ where
     split
     . exact isPowerOfTwo_go (power*2) (Nat.mul_pos h₁ (by decide)) (Nat.mul2_isPowerOfTwo_of_isPowerOfTwo h₂)
     . assumption
-termination_by isPowerOfTwo_go p _ _ => n - p
-decreasing_by simp_wf; apply nextPowerOfTwo_dec <;> assumption
+  termination_by n - power
+  decreasing_by simp_wf; apply nextPowerOfTwo_dec <;> assumption
 
 end Nat

src/Init/Data/String/Basic.lean

@@ -159,7 +159,7 @@ def posOfAux (s : String) (c : Char) (stopPos : Pos) (pos : Pos) : Pos :=
       have := Nat.sub_lt_sub_left h (lt_next s pos)
       posOfAux s c stopPos (s.next pos)
   else pos
-termination_by _ => stopPos.1 - pos.1
+termination_by stopPos.1 - pos.1
 
 @[inline] def posOf (s : String) (c : Char) : Pos :=
   posOfAux s c s.endPos 0
@@ -171,7 +171,7 @@ def revPosOfAux (s : String) (c : Char) (pos : Pos) : Option Pos :=
     let pos := s.prev pos
     if s.get pos == c then some pos
     else revPosOfAux s c pos
-termination_by _ => pos.1
+termination_by pos.1
 
 def revPosOf (s : String) (c : Char) : Option Pos :=
   revPosOfAux s c s.endPos
@@ -183,7 +183,7 @@ def findAux (s : String) (p : Char → Bool) (stopPos : Pos) (pos : Pos) : Pos :
       have := Nat.sub_lt_sub_left h (lt_next s pos)
       findAux s p stopPos (s.next pos)
   else pos
-termination_by _ => stopPos.1 - pos.1
+termination_by stopPos.1 - pos.1
 
 @[inline] def find (s : String) (p : Char → Bool) : Pos :=
   findAux s p s.endPos 0
@@ -195,7 +195,7 @@ def revFindAux (s : String) (p : Char → Bool) (pos : Pos) : Option Pos :=
     let pos := s.prev pos
     if p (s.get pos) then some pos
     else revFindAux s p pos
-termination_by _ => pos.1
+termination_by pos.1
 
 def revFind (s : String) (p : Char → Bool) : Option Pos :=
   revFindAux s p s.endPos
@@ -213,8 +213,8 @@ def firstDiffPos (a b : String) : Pos :=
         have := Nat.sub_lt_sub_left h (lt_next a i)
         loop (a.next i)
     else i
+    termination_by stopPos.1 - i.1
   loop 0
-termination_by loop => stopPos.1 - i.1
 
 @[extern "lean_string_utf8_extract"]
 def extract : (@& String) → (@& Pos) → (@& Pos) → String
@@ -240,7 +240,7 @@ where
       splitAux s p i' i' (s.extract b i :: r)
     else
       splitAux s p b (s.next i) r
-termination_by _ => s.endPos.1 - i.1
+termination_by s.endPos.1 - i.1
 
 @[specialize] def split (s : String) (p : Char → Bool) : List String :=
   splitAux s p 0 0 []
@@ -260,7 +260,7 @@ def splitOnAux (s sep : String) (b : Pos) (i : Pos) (j : Pos) (r : List String)
         splitOnAux s sep b i j r
     else
       splitOnAux s sep b (s.next i) 0 r
-termination_by _ => s.endPos.1 - i.1
+termination_by s.endPos.1 - i.1
 
 def splitOn (s : String) (sep : String := " ") : List String :=
   if sep == "" then [s] else splitOnAux s sep 0 0 0 []
@@ -369,7 +369,7 @@ def offsetOfPosAux (s : String) (pos : Pos) (i : Pos) (offset : Nat) : Nat :=
   else
     have := Nat.sub_lt_sub_left (Nat.gt_of_not_le (mt decide_eq_true h)) (lt_next s _)
     offsetOfPosAux s pos (s.next i) (offset+1)
-termination_by _ => s.endPos.1 - i.1
+termination_by s.endPos.1 - i.1
 
 def offsetOfPos (s : String) (pos : Pos) : Nat :=
   offsetOfPosAux s pos 0 0
@@ -379,7 +379,7 @@ def offsetOfPos (s : String) (pos : Pos) : Nat :=
     have := Nat.sub_lt_sub_left h (lt_next s i)
     foldlAux f s stopPos (s.next i) (f a (s.get i))
   else a
-termination_by _ => stopPos.1 - i.1
+termination_by stopPos.1 - i.1
 
 @[inline] def foldl {α : Type u} (f : α → Char → α) (init : α) (s : String) : α :=
   foldlAux f s s.endPos 0 init
@@ -392,7 +392,7 @@ termination_by _ => stopPos.1 - i.1
     let a := f (s.get i) a
     foldrAux f a s i begPos
   else a
-termination_by _ => i.1
+termination_by i.1
 
 @[inline] def foldr {α : Type u} (f : Char → α → α) (init : α) (s : String) : α :=
   foldrAux f init s s.endPos 0
@@ -404,7 +404,7 @@ termination_by _ => i.1
       have := Nat.sub_lt_sub_left h (lt_next s i)
       anyAux s stopPos p (s.next i)
   else false
-termination_by _ => stopPos.1 - i.1
+termination_by stopPos.1 - i.1
 
 @[inline] def any (s : String) (p : Char → Bool) : Bool :=
   anyAux s s.endPos p 0
@@ -463,7 +463,7 @@ theorem mapAux_lemma (s : String) (i : Pos) (c : Char) (h : ¬s.atEnd i) :
     have := mapAux_lemma s i c h
     let s := s.set i c
     mapAux f (s.next i) s
-termination_by _ => s.endPos.1 - i.1
+termination_by s.endPos.1 - i.1
 
 @[inline] def map (f : Char → Char) (s : String) : String :=
   mapAux f 0 s
@@ -490,7 +490,7 @@ where
       have := Nat.sub_lt_sub_left h (Nat.add_lt_add_left (one_le_csize c₁) off1.1)
       c₁ == c₂ && loop (off1 + c₁) (off2 + c₂) stop1
     else true
-termination_by loop => stop1.1 - off1.1
+  termination_by stop1.1 - off1.1
 
 /-- Return true iff `p` is a prefix of `s` -/
 def isPrefixOf (p : String) (s : String) : Bool :=
@@ -512,8 +512,8 @@ def replace (s pattern replacement : String) : String :=
         else
           have := Nat.sub_lt_sub_left this (lt_next s pos)
           loop acc accStop (s.next pos)
+      termination_by s.endPos.1 - pos.1
     loop "" 0 0
-termination_by loop => s.endPos.1 - pos.1
 
 end String
 
@@ -612,8 +612,8 @@ def splitOn (s : Substring) (sep : String := " ") : List Substring :=
         else
           s.extract b i :: r
         r.reverse
+      termination_by s.bsize - i.1
     loop 0 0 0 []
-termination_by loop => s.bsize - i.1
 
 @[inline] def foldl {α : Type u} (f : α → Char → α) (init : α) (s : Substring) : α :=
   match s with
@@ -640,7 +640,7 @@ def contains (s : Substring) (c : Char) : Bool :=
       takeWhileAux s stopPos p (s.next i)
     else i
   else i
-termination_by _ => stopPos.1 - i.1
+termination_by stopPos.1 - i.1
 
 @[inline] def takeWhile : Substring → (Char → Bool) → Substring
   | ⟨s, b, e⟩, p =>
@@ -661,7 +661,7 @@ termination_by _ => stopPos.1 - i.1
     if !p c then i
     else takeRightWhileAux s begPos p i'
   else i
-termination_by _ => i.1
+termination_by i.1
 
 @[inline] def takeRightWhile : Substring → (Char → Bool) → Substring
   | ⟨s, b, e⟩, p =>

src/Init/Meta.lean

@@ -1039,7 +1039,7 @@ where
       go (i+1) (args.push (quote xs[i]))
     else
       Syntax.mkCApp (Name.mkStr2 "Array" ("mkArray" ++ toString xs.size)) args
-termination_by go i _ => xs.size - i
+  termination_by xs.size - i
 
 instance [Quote α `term] : Quote (Array α) `term where
   quote := quoteArray

src/Lean/Compiler/LCNF/AlphaEqv.lean

@@ -75,10 +75,10 @@ def eqvLetValue (e₁ e₂ : LetValue) : EqvM Bool := do
           go (i+1)
       else
         x
+      termination_by params₁.size - i
     go 0
   else
     return false
-termination_by go i => params₁.size - i
 
 def sortAlts (alts : Array Alt) : Array Alt :=
   alts.qsort fun
@@ -133,4 +133,4 @@ Return `true` if `c₁` and `c₂` are alpha equivalent.
 def Code.alphaEqv (c₁ c₂ : Code) : Bool :=
   AlphaEqv.eqv c₁ c₂ |>.run {}
 
-end Lean.Compiler.LCNF
+end Lean.Compiler.LCNF

src/Lean/Compiler/LCNF/Specialize.lean

@@ -181,8 +181,8 @@ def expandCodeDecls (decls : Array CodeDecl) (body : LetValue) : CompilerM Expr
       go (i+1) (subst.push value)
     else
       (body.toExpr.abstract xs).instantiateRev subst
+    termination_by values.size - i
   return go 0 #[]
-termination_by go => values.size - i
 
 /--
 Create the "key" that uniquely identifies a code specialization.

src/Lean/Compiler/LCNF/Types.lean

@@ -234,7 +234,7 @@ where
         throwError "invalid instantiateForall, too many parameters"
     else
       return type
-termination_by go i _ => ps.size - i
+  termination_by ps.size - i
 
 /--
 Return `true` if `type` is a predicate.

src/Lean/Data/HashMap.lean

@@ -89,7 +89,7 @@ def moveEntries [Hashable α] (i : Nat) (source : Array (AssocList α β)) (targ
      let target                := es.foldl (reinsertAux hash) target
      moveEntries (i+1) source target
   else target
-termination_by _ i source _ => source.size - i
+termination_by source.size - i
 
 def expand [Hashable α] (size : Nat) (buckets : HashMapBucket α β) : HashMapImp α β :=
   let bucketsNew : HashMapBucket α β := ⟨