diff --git a/library/init/control/combinators.lean b/library/init/control/combinators.lean index 91d22717cb..27e983c6b3 100644 --- a/library/init/control/combinators.lean +++ b/library/init/control/combinators.lean @@ -40,8 +40,8 @@ namespace Nat mforAux f n n @[specialize] def mfoldAux {α : Type u} {m : Type u → Type v} [Monad m] (f : Nat → α → m α) (n : Nat) : Nat → α → m α -| 0, a => pure a -| i+1, a => f (n-i-1) a >>= mfoldAux i +| 0, a => pure a +| i+1, a => f (n-i-1) a >>= mfoldAux i @[inline] def mfold {α : Type u} {m : Type u → Type v} [Monad m] (f : Nat → α → m α) (a : α) (n : Nat) : m α := mfoldAux f n n a diff --git a/library/init/core.lean b/library/init/core.lean index 15267dbd20..19357f5e1f 100644 --- a/library/init/core.lean +++ b/library/init/core.lean @@ -395,8 +395,8 @@ attribute [matchPattern] HasZero.zero HasOne.one bit0 bit1 HasAdd.add HasNeg.neg /- Nat basic instances -/ @[extern cpp "lean::nat_add"] protected def Nat.add : (@& Nat) → (@& Nat) → Nat -| a, Nat.zero => a -| a, Nat.succ b => Nat.succ (Nat.add a b) +| a, Nat.zero => a +| a, Nat.succ b => Nat.succ (Nat.add a b) /- We mark the following definitions as pattern to make sure they can be used in recursive equations, and reduced by the equation Compiler. -/ diff --git a/library/init/data/array/basic.lean b/library/init/data/array/basic.lean index 3ce9e7e9e7..aa21ebe3dd 100644 --- a/library/init/data/array/basic.lean +++ b/library/init/data/array/basic.lean @@ -269,8 +269,8 @@ section variable {β:Type w} @[specialize] private def revIterateAux (a : Array α) (f : ∀ (i : Fin a.size), α → β → β) : ∀ (i : Nat), i ≤ a.size → β → β -| 0, h, b => b -| j+1, h, b => +| 0, h, b => b +| j+1, h, b => let i : Fin a.size := ⟨j, h⟩; revIterateAux j (Nat.leOfLt h) (f i (a.fget i) b) @@ -480,8 +480,8 @@ end Array export Array (mkArray) @[inlineIfReduce] def List.toArrayAux {α : Type u} : List α → Array α → Array α -| [], r => r -| a::as, r => List.toArrayAux as (r.push a) +| [], r => r +| a::as, r => List.toArrayAux as (r.push a) @[inlineIfReduce] def List.redLength {α : Type u} : List α → Nat | [] => 0 diff --git a/library/init/data/binomialheap/basic.lean b/library/init/data/binomialheap/basic.lean index ab8f0f6e38..078595c45f 100644 --- a/library/init/data/binomialheap/basic.lean +++ b/library/init/data/binomialheap/basic.lean @@ -54,9 +54,9 @@ else if r != hRank t₂ then mergeNodes t₁ (merged :: t₂) else merged :: mergeNodes t₁ t₂ @[specialize] def merge (lt : α → α → Bool) : Heap α → Heap α → Heap α -| Heap.empty, h => h -| h, Heap.empty => h -| Heap.heap h₁, Heap.heap h₂ => Heap.heap (mergeNodes lt h₁ h₂) +| Heap.empty, h => h +| h, Heap.empty => h +| Heap.heap h₁, Heap.heap h₂ => Heap.heap (mergeNodes lt h₁ h₂) @[specialize] def headOpt (lt : α → α → Bool) : Heap α → Option α | Heap.empty => none @@ -72,8 +72,8 @@ else | Heap.heap (h::hs) => hs.foldl (fun r n => if lt r n.val then r else n.val) h.val @[specialize] def findMin (lt : α → α → Bool) : List (HeapNode α) → Nat → HeapNode α × Nat → HeapNode α × Nat -| [], _, r => r -| h::hs, idx, (h', idx') => if lt h.val h'.val then findMin hs (idx+1) (h, idx) else findMin hs (idx+1) (h', idx') +| [], _, r => r +| h::hs, idx, (h', idx') => if lt h.val h'.val then findMin hs (idx+1) (h, idx) else findMin hs (idx+1) (h', idx') def tail (lt : α → α → Bool) : Heap α → Heap α | Heap.empty => Heap.empty diff --git a/library/init/data/bytearray/basic.lean b/library/init/data/bytearray/basic.lean index 4f64f813c0..f5e0977a1b 100644 --- a/library/init/data/bytearray/basic.lean +++ b/library/init/data/bytearray/basic.lean @@ -56,8 +56,8 @@ toListAux bs 0 [] end ByteArray def List.toByteArrayAux : List UInt8 → ByteArray → ByteArray -| [], r => r -| b::bs, r => List.toByteArrayAux bs (r.push b) +| [], r => r +| b::bs, r => List.toByteArrayAux bs (r.push b) def List.toByteArray (bs : List UInt8) : ByteArray := bs.toByteArrayAux ByteArray.empty diff --git a/library/init/data/fin/basic.lean b/library/init/data/fin/basic.lean index d382ddbf8e..9926d2a5c6 100644 --- a/library/init/data/fin/basic.lean +++ b/library/init/data/fin/basic.lean @@ -37,8 +37,8 @@ def ofNat' {n : Nat} (a : Nat) (h : n > 0) : Fin n := ⟨a % n, Nat.modLt _ h⟩ private theorem mlt {n b : Nat} : ∀ {a}, n > a → b % n < n -| 0, h => Nat.modLt _ h -| a+1, h => +| 0, h => Nat.modLt _ h +| a+1, h => have n > 0 from Nat.ltTrans (Nat.zeroLtSucc _) h; Nat.modLt _ this diff --git a/library/init/data/int/basic.lean b/library/init/data/int/basic.lean index 28256b7d88..24b2b8e0ad 100644 --- a/library/init/data/int/basic.lean +++ b/library/init/data/int/basic.lean @@ -126,17 +126,17 @@ instance : HasToString Int := @[extern cpp "lean::int_div"] def div : (@& Int) → (@& Int) → Int -| ofNat m, ofNat n => ofNat (m / n) -| ofNat m, negSucc n => -ofNat (m / succ n) -| negSucc m, ofNat n => -ofNat (succ m / n) -| negSucc m, negSucc n => ofNat (succ m / succ n) +| ofNat m, ofNat n => ofNat (m / n) +| ofNat m, negSucc n => -ofNat (m / succ n) +| negSucc m, ofNat n => -ofNat (succ m / n) +| negSucc m, negSucc n => ofNat (succ m / succ n) @[extern cpp "lean::int_mod"] def mod : (@& Int) → (@& Int) → Int -| ofNat m, ofNat n => ofNat (m % n) -| ofNat m, negSucc n => ofNat (m % succ n) -| negSucc m, ofNat n => -ofNat (succ m % n) -| negSucc m, negSucc n => -ofNat (succ m % succ n) +| ofNat m, ofNat n => ofNat (m % n) +| ofNat m, negSucc n => ofNat (m % succ n) +| negSucc m, ofNat n => -ofNat (succ m % n) +| negSucc m, negSucc n => -ofNat (succ m % succ n) instance : HasDiv Int := ⟨Int.div⟩ instance : HasMod Int := ⟨Int.mod⟩ diff --git a/library/init/data/list/basic.lean b/library/init/data/list/basic.lean index 98a67e3c6a..2352767076 100644 --- a/library/init/data/list/basic.lean +++ b/library/init/data/list/basic.lean @@ -17,10 +17,10 @@ variables {α : Type u} {β : Type v} {γ : Type w} namespace List protected def hasDecEq [DecidableEq α] : ∀ (a b : List α), Decidable (a = b) -| [], [] => isTrue rfl -| a::as, [] => isFalse (fun h => List.noConfusion h) -| [], b::bs => isFalse (fun h => List.noConfusion h) -| a::as, b::bs => +| [], [] => isTrue rfl +| a::as, [] => isFalse (fun h => List.noConfusion h) +| [], b::bs => isFalse (fun h => List.noConfusion h) +| a::as, b::bs => match decEq a b with | isTrue hab => match hasDecEq as bs with @@ -32,8 +32,8 @@ instance [DecidableEq α] : DecidableEq (List α) := {decEq := List.hasDecEq} def reverseAux : List α → List α → List α -| [], r => r -| a::l, r => reverseAux l (a::r) +| [], r => r +| a::l, r => reverseAux l (a::r) def reverse : List α → List α := fun l => reverseAux l [] @@ -45,8 +45,8 @@ instance : HasAppend (List α) := ⟨List.append⟩ theorem reverseAuxReverseAuxNil : ∀ (as bs : List α), reverseAux (reverseAux as bs) [] = reverseAux bs as -| [], bs => rfl -| a::as, bs => +| [], bs => rfl +| a::as, bs => show reverseAux (reverseAux as (a::bs)) [] = reverseAux bs (a::as) from reverseAuxReverseAuxNil as (a::bs) @@ -58,8 +58,8 @@ show reverseAux (reverseAux as []) [] = as from reverseAuxReverseAuxNil as [] theorem reverseAuxReverseAux : ∀ (as bs cs : List α), reverseAux (reverseAux as bs) cs = reverseAux bs (reverseAux (reverseAux as []) cs) -| [], bs, cs => rfl -| a::as, bs, cs => +| [], bs, cs => rfl +| a::as, bs, cs => Eq.trans (reverseAuxReverseAux as (a::bs) cs) (congrArg (fun b => reverseAux bs b) (reverseAuxReverseAux as [a] cs).symm) @@ -68,8 +68,8 @@ theorem consAppend (a : α) (as bs : List α) : (a::as) ++ bs = a::(as ++ bs) := reverseAuxReverseAux as [a] bs theorem appendAssoc : ∀ (as bs cs : List α), (as ++ bs) ++ cs = as ++ (bs ++ cs) -| [], bs, cs => rfl -| a::as, bs, cs => +| [], bs, cs => rfl +| a::as, bs, cs => show ((a::as) ++ bs) ++ cs = (a::as) ++ (bs ++ cs) from have h₁ : ((a::as) ++ bs) ++ cs = a::(as++bs) ++ cs from congrArg (fun ds => ds ++ cs) (consAppend a as bs); have h₂ : a::(as++bs) ++ cs = a::((as++bs) ++ cs) from consAppend a (as++bs) cs; @@ -81,19 +81,19 @@ instance : HasEmptyc (List α) := ⟨List.nil⟩ protected def erase {α} [HasBeq α] : List α → α → List α -| [], b => [] -| a::as, b => match a == b with +| [], b => [] +| a::as, b => match a == b with | true => as | false => a :: erase as b def eraseIdx : List α → Nat → List α -| [], _ => [] -| a::as, 0 => as -| a::as, n+1 => a :: eraseIdx as n +| [], _ => [] +| a::as, 0 => as +| a::as, n+1 => a :: eraseIdx as n def lengthAux : List α → Nat → Nat -| [], n => n -| a::as, n => lengthAux as (n+1) +| [], n => n +| a::as, n => lengthAux as (n+1) def length (as : List α) : Nat := lengthAux as 0 @@ -103,19 +103,19 @@ def isEmpty : List α → Bool | _ :: _ => false def get [Inhabited α] : Nat → List α → α -| 0, a::as => a -| n+1, a::as => get n as -| _, _ => default α +| 0, a::as => a +| n+1, a::as => get n as +| _, _ => default α def getOpt : Nat → List α → Option α -| 0, a::as => some a -| n+1, a::as => getOpt n as -| _, _ => none +| 0, a::as => some a +| n+1, a::as => getOpt n as +| _, _ => none def set : List α → Nat → α → List α -| a::as, 0, b => b::as -| a::as, n+1, b => a::(set as n b) -| [], _, _ => [] +| a::as, 0, b => b::as +| a::as, n+1, b => a::(set as n b) +| [], _, _ => [] def head [Inhabited α] : List α → α | [] => default α @@ -130,9 +130,9 @@ def tail : List α → List α | a::as => f a :: map as @[specialize] def map₂ (f : α → β → γ) : List α → List β → List γ -| [], _ => [] -| _, [] => [] -| a::as, b::bs => f a b :: map₂ as bs +| [], _ => [] +| _, [] => [] +| a::as, b::bs => f a b :: map₂ as bs def join : List (List α) → List α | [] => [] @@ -146,8 +146,8 @@ def join : List (List α) → List α | some b => b :: filterMap as @[specialize] def filterAux (p : α → Bool) : List α → List α → List α -| [], rs => rs.reverse -| a::as, rs => match p a with +| [], rs => rs.reverse +| a::as, rs => match p a with | true => filterAux as (a::rs) | false => filterAux as rs @@ -155,8 +155,8 @@ def join : List (List α) → List α filterAux p as [] @[specialize] def partitionAux (p : α → Bool) : List α → List α × List α → List α × List α -| [], (bs, cs) => (bs.reverse, cs.reverse) -| a::as, (bs, cs) => +| [], (bs, cs) => (bs.reverse, cs.reverse) +| a::as, (bs, cs) => match p a with | true => partitionAux as (a::bs, cs) | false => partitionAux as (bs, a::cs) @@ -186,8 +186,8 @@ def notElem [HasBeq α] (a : α) (as : List α) : Bool := !(as.elem a) def eraseDupsAux {α} [HasBeq α] : List α → List α → List α -| [], bs => bs.reverse -| a::as, bs => match bs.elem a with +| [], bs => bs.reverse +| a::as, bs => match bs.elem a with | true => eraseDupsAux as bs | false => eraseDupsAux as (a::bs) @@ -195,8 +195,8 @@ def eraseDups {α} [HasBeq α] (as : List α) : List α := eraseDupsAux as [] @[specialize] def spanAux (p : α → Bool) : List α → List α → List α × List α -| [], rs => (rs.reverse, []) -| a::as, rs => match p a with +| [], rs => (rs.reverse, []) +| a::as, rs => match p a with | true => spanAux as (a::rs) | false => (rs.reverse, a::as) @@ -213,14 +213,14 @@ def removeAll [HasBeq α] (xs ys : List α) : List α := xs.filter (fun x => ys.notElem x) def drop : Nat → List α → List α -| 0, a => a -| n+1, [] => [] -| n+1, a::as => drop n as +| 0, a => a +| n+1, [] => [] +| n+1, a::as => drop n as def take : Nat → List α → List α -| 0, a => [] -| n+1, [] => [] -| n+1, a::as => a :: take n as +| 0, a => [] +| n+1, [] => [] +| n+1, a::as => a :: take n as @[specialize] def foldl (f : α → β → α) : α → List β → α | a, [] => a @@ -231,9 +231,9 @@ def take : Nat → List α → List α | a :: l => f a (foldr l) @[specialize] def foldr1 (f : α → α → α) : ∀ (xs : List α), xs ≠ [] → α -| [], h => absurd rfl h -| [a], _ => a -| a :: as@(_::_), _ => f a (foldr1 as (fun h => List.noConfusion h)) +| [], h => absurd rfl h +| [a], _ => a +| a :: as@(_::_), _ => f a (foldr1 as (fun h => List.noConfusion h)) @[specialize] def foldr1Opt (f : α → α → α) : List α → Option α | [] => none @@ -250,8 +250,8 @@ def or (bs : List Bool) : Bool := bs.any id def and (bs : List Bool) : Bool := bs.all id def zipWith (f : α → β → γ) : List α → List β → List γ -| x::xs, y::ys => f x y :: zipWith xs ys -| _, _ => [] +| x::xs, y::ys => f x y :: zipWith xs ys +| _, _ => [] def zip : List α → List β → List (Prod α β) := zipWith Prod.mk @@ -264,8 +264,8 @@ def replicate (n : Nat) (a : α) : List α := n.repeat (fun xs => a :: xs) [] def rangeAux : Nat → List Nat → List Nat -| 0, ns => ns -| n+1, ns => rangeAux n (n::ns) +| 0, ns => ns +| n+1, ns => rangeAux n (n::ns) def range (n : Nat) : List Nat := rangeAux n [] @@ -281,9 +281,9 @@ def enumFrom : Nat → List α → List (Nat × α) def enum : List α → List (Nat × α) := enumFrom 0 def getLastOfNonNil : ∀ (as : List α), as ≠ [] → α -| [], h => absurd rfl h -| [a], h => a -| a::b::as, h => getLastOfNonNil (b::as) (fun h => List.noConfusion h) +| [], h => absurd rfl h +| [a], h => a +| a::b::as, h => getLastOfNonNil (b::as) (fun h => List.noConfusion h) def getLast [Inhabited α] : List α → α | [] => arbitrary α @@ -317,10 +317,10 @@ instance [HasLess α] : HasLess (List α) := ⟨List.Less⟩ instance hasDecidableLt [HasLess α] [h : DecidableRel HasLess.Less] : ∀ (l₁ l₂ : List α), Decidable (l₁ < l₂) -| [], [] => isFalse (fun h => nomatch h) -| [], b::bs => isTrue (Less.nil _ _) -| a::as, [] => isFalse (fun h => nomatch h) -| a::as, b::bs => +| [], [] => isFalse (fun h => nomatch h) +| [], b::bs => isTrue (Less.nil _ _) +| a::as, [] => isFalse (fun h => nomatch h) +| a::as, b::bs => match h a b with | isTrue h₁ => isTrue (Less.head _ _ h₁) | isFalse h₁ => @@ -346,16 +346,16 @@ fun a b => Not.Decidable /-- `isPrefixOf l₁ l₂` returns `true` Iff `l₁` is a prefix of `l₂`. -/ def isPrefixOf [HasBeq α] : List α → List α → Bool -| [], _ => true -| _, [] => false -| a::as, b::bs => a == b && isPrefixOf as bs +| [], _ => true +| _, [] => false +| a::as, b::bs => a == b && isPrefixOf as bs /-- `isSuffixOf l₁ l₂` returns `true` Iff `l₁` is a suffix of `l₂`. -/ def isSuffixOf [HasBeq α] (l₁ l₂ : List α) : Bool := isPrefixOf l₁.reverse l₂.reverse @[specialize] def isEqv : List α → List α → (α → α → Bool) → Bool -| [], [], _ => true -| a::as, b::bs, eqv => eqv a b && isEqv as bs eqv -| _, _, eqv => false +| [], [], _ => true +| a::as, b::bs, eqv => eqv a b && isEqv as bs eqv +| _, _, eqv => false end List diff --git a/library/init/data/nat/basic.lean b/library/init/data/nat/basic.lean index 610dd312a3..aff4f1fedc 100644 --- a/library/init/data/nat/basic.lean +++ b/library/init/data/nat/basic.lean @@ -11,25 +11,25 @@ namespace Nat @[extern cpp "lean::nat_dec_eq"] def beq : Nat → Nat → Bool -| zero, zero => true -| zero, succ m => false -| succ n, zero => false -| succ n, succ m => beq n m +| zero, zero => true +| zero, succ m => false +| succ n, zero => false +| succ n, succ m => beq n m theorem eqOfBeqEqTt : ∀ {n m : Nat}, beq n m = true → n = m -| zero, zero, h => rfl -| zero, succ m, h => Bool.noConfusion h -| succ n, zero, h => Bool.noConfusion h -| succ n, succ m, h => +| zero, zero, h => rfl +| zero, succ m, h => Bool.noConfusion h +| succ n, zero, h => Bool.noConfusion h +| succ n, succ m, h => have beq n m = true from h; have n = m from eqOfBeqEqTt this; congrArg succ this theorem neOfBeqEqFf : ∀ {n m : Nat}, beq n m = false → n ≠ m -| zero, zero, h₁, h₂ => Bool.noConfusion h₁ -| zero, succ m, h₁, h₂ => Nat.noConfusion h₂ -| succ n, zero, h₁, h₂ => Nat.noConfusion h₂ -| succ n, succ m, h₁, h₂ => +| zero, zero, h₁, h₂ => Bool.noConfusion h₁ +| zero, succ m, h₁, h₂ => Nat.noConfusion h₂ +| succ n, zero, h₁, h₂ => Nat.noConfusion h₂ +| succ n, succ m, h₁, h₂ => have beq n m = false from h₁; have n ≠ m from neOfBeqEqFf this; Nat.noConfusion h₂ (fun h₂ => absurd h₂ this) @@ -44,10 +44,10 @@ else isFalse (neOfBeqEqFf (eqFalseOfNeTrue h)) @[extern cpp "lean::nat_dec_le"] def ble : Nat → Nat → Bool -| zero, zero => true -| zero, succ m => true -| succ n, zero => false -| succ n, succ m => ble n m +| zero, zero => true +| zero, succ m => true +| succ n, zero => false +| succ n, succ m => ble n m protected def le (n m : Nat) : Prop := ble n m = true @@ -83,8 +83,8 @@ instance : HasMul Nat := ⟨Nat.mul⟩ @[specialize] def foldAux {α : Type u} (f : Nat → α → α) (s : Nat) : Nat → α → α -| 0, a => a -| succ n, a => foldAux n (f (s - (succ n)) a) +| 0, a => a +| succ n, a => foldAux n (f (s - (succ n)) a) @[inline] def fold {α : Type u} (f : Nat → α → α) (n : Nat) (a : α) : α := foldAux f n n a @@ -101,8 +101,8 @@ anyAux f n n !any (fun i => !f i) n @[specialize] def repeatAux {α : Type u} (f : α → α) : Nat → α → α -| 0, a => a -| succ n, a => repeatAux n (f a) +| 0, a => a +| succ n, a => repeatAux n (f a) @[inline] def repeat {α : Type u} (f : α → α) (n : Nat) (a : α) : α := repeatAux f n a @@ -153,8 +153,8 @@ protected theorem addRightComm : ∀ (n m k : Nat), (n + m) + k = (n + k) + m := rightComm Nat.add Nat.addComm Nat.addAssoc protected theorem addLeftCancel : ∀ {n m k : Nat}, n + m = n + k → m = k -| 0, m, k, h => Nat.zeroAdd m ▸ Nat.zeroAdd k ▸ h -| succ n, m, k, h => +| 0, m, k, h => Nat.zeroAdd m ▸ Nat.zeroAdd k ▸ h +| succ n, m, k, h => have n+m = n+k from have succ (n + m) = succ (n + k) from succAdd n m ▸ succAdd n k ▸ h; Nat.noConfusion this id; @@ -194,8 +194,8 @@ protected theorem oneMul (n : Nat) : 1 * n = n := Nat.mulComm n 1 ▸ Nat.mulOne n protected theorem leftDistrib : ∀ (n m k : Nat), n * (m + k) = n * m + n * k -| 0, m, k => (Nat.zeroMul (m + k)).symm ▸ (Nat.zeroMul m).symm ▸ (Nat.zeroMul k).symm ▸ rfl -| succ n, m, k => +| 0, m, k => (Nat.zeroMul (m + k)).symm ▸ (Nat.zeroMul m).symm ▸ (Nat.zeroMul k).symm ▸ rfl +| succ n, m, k => have h₁ : succ n * (m + k) = n * (m + k) + (m + k) from succMul _ _; have h₂ : n * (m + k) + (m + k) = (n * m + n * k) + (m + k) from leftDistrib n m k ▸ rfl; have h₃ : (n * m + n * k) + (m + k) = n * m + (n * k + (m + k)) from Nat.addAssoc _ _ _; @@ -240,10 +240,10 @@ theorem succLtSucc {n m : Nat} : n < m → succ n < succ m := succLeSucc theorem leStep : ∀ {n m : Nat}, n ≤ m → n ≤ succ m -| zero, zero, h => rfl -| zero, succ n, h => rfl -| succ n, zero, h => Bool.noConfusion h -| succ n, succ m, h => +| zero, zero, h => rfl +| zero, succ n, h => rfl +| succ n, zero, h => Bool.noConfusion h +| succ n, succ m, h => have n ≤ m from h; have n ≤ succ m from leStep this; succLeSucc this @@ -258,17 +258,17 @@ succLeSucc (zeroLe n) def succPos := zeroLtSucc theorem notSuccLeZero : ∀ (n : Nat), succ n ≤ 0 → False -| 0, h => nomatch h -| n+1, h => nomatch h +| 0, h => nomatch h +| n+1, h => nomatch h theorem notLtZero (n : Nat) : ¬ n < 0 := notSuccLeZero n theorem predLePred : ∀ {n m : Nat}, n ≤ m → pred n ≤ pred m -| zero, zero, h => rfl -| zero, succ n, h => zeroLe n -| succ n, zero, h => Bool.noConfusion h -| succ n, succ m, h => h +| zero, zero, h => rfl +| zero, succ n, h => zeroLe n +| succ n, zero, h => Bool.noConfusion h +| succ n, succ m, h => h theorem leOfSuccLeSucc {n m : Nat} : succ n ≤ succ m → n ≤ m := predLePred @@ -282,10 +282,10 @@ instance decLt (n m : @& Nat) : Decidable (n < m) := Nat.decLe (succ n) m protected theorem eqOrLtOfLe : ∀ {n m: Nat}, n ≤ m → n = m ∨ n < m -| zero, zero, h => Or.inl rfl -| zero, succ n, h => Or.inr $ zeroLe n -| succ n, zero, h => Bool.noConfusion h -| succ n, succ m, h => +| zero, zero, h => Or.inl rfl +| zero, succ n, h => Or.inr $ zeroLe n +| succ n, zero, h => Bool.noConfusion h +| succ n, succ m, h => have n ≤ m from h; have n = m ∨ n < m from eqOrLtOfLe this; Or.elim this @@ -310,10 +310,10 @@ protected theorem ltIrrefl (n : Nat) : ¬n < n := notSuccLeSelf n protected theorem leTrans : ∀ {n m k : Nat}, n ≤ m → m ≤ k → n ≤ k -| zero, m, k, h₁, h₂ => zeroLe _ -| succ n, zero, k, h₁, h₂ => Bool.noConfusion h₁ -| succ n, succ m, zero, h₁, h₂ => Bool.noConfusion h₂ -| succ n, succ m, succ k, h₁, h₂ => +| zero, m, k, h₁, h₂ => zeroLe _ +| succ n, zero, k, h₁, h₂ => Bool.noConfusion h₁ +| succ n, succ m, zero, h₁, h₂ => Bool.noConfusion h₂ +| succ n, succ m, succ k, h₁, h₂ => have h₁' : n ≤ m from h₁; have h₂' : m ≤ k from h₂; have n ≤ k from leTrans h₁' h₂'; @@ -324,16 +324,16 @@ theorem predLe : ∀ (n : Nat), pred n ≤ n | succ n => leSucc _ theorem predLt : ∀ {n : Nat}, n ≠ 0 → pred n < n -| zero, h => absurd rfl h -| succ n, h => ltSuccOfLe (Nat.leRefl _) +| zero, h => absurd rfl h +| succ n, h => ltSuccOfLe (Nat.leRefl _) theorem subLe (n m : Nat) : n - m ≤ n := Nat.recOn m (Nat.leRefl (n - 0)) (fun m => Nat.leTrans (predLe (n - m))) theorem subLt : ∀ {n m : Nat}, 0 < n → 0 < m → n - m < n -| 0, m, h1, h2 => absurd h1 (Nat.ltIrrefl 0) -| n+1, 0, h1, h2 => absurd h2 (Nat.ltIrrefl 0) -| n+1, m+1, h1, h2 => +| 0, m, h1, h2 => absurd h1 (Nat.ltIrrefl 0) +| n+1, 0, h1, h2 => absurd h2 (Nat.ltIrrefl 0) +| n+1, m+1, h1, h2 => Eq.symm (succSubSuccEqSub n m) ▸ show n - m < succ n from ltSuccOfLe (subLe n m) @@ -370,10 +370,10 @@ def lt.base (n : Nat) : n < succ n := Nat.leRefl (succ n) theorem ltSuccSelf (n : Nat) : n < succ n := lt.base n protected theorem leAntisymm : ∀ {n m : Nat}, n ≤ m → m ≤ n → n = m -| zero, zero, h₁, h₂ => rfl -| succ n, zero, h₁, h₂ => Bool.noConfusion h₁ -| zero, succ m, h₁, h₂ => Bool.noConfusion h₂ -| succ n, succ m, h₁, h₂ => +| zero, zero, h₁, h₂ => rfl +| succ n, zero, h₁, h₂ => Bool.noConfusion h₁ +| zero, succ m, h₁, h₂ => Bool.noConfusion h₂ +| succ n, succ m, h₁, h₂ => have h₁' : n ≤ m from h₁; have h₂' : m ≤ n from h₂; have n = m from leAntisymm h₁' h₂'; @@ -428,10 +428,10 @@ theorem leAddLeft (n m : Nat): n ≤ m + n := Nat.addComm n m ▸ leAddRight n m theorem le.dest : ∀ {n m : Nat}, n ≤ m → Exists (fun k => n + k = m) -| zero, zero, h => ⟨0, rfl⟩ -| zero, succ n, h => ⟨succ n, show 0 + succ n = succ n from (Nat.addComm 0 (succ n)).symm ▸ rfl⟩ -| succ n, zero, h => Bool.noConfusion h -| succ n, succ m, h => +| zero, zero, h => ⟨0, rfl⟩ +| zero, succ n, h => ⟨succ n, show 0 + succ n = succ n from (Nat.addComm 0 (succ n)).symm ▸ rfl⟩ +| succ n, zero, h => Bool.noConfusion h +| succ n, succ m, h => have n ≤ m from h; have Exists (fun k => n + k = m) from le.dest this; match this with @@ -507,8 +507,8 @@ show succ (succ n + n) = succ (succ (n + n)) from congrArg succ (succAdd n n) protected theorem zeroLtBit0 : ∀ {n : Nat}, n ≠ 0 → 0 < bit0 n -| 0, h => absurd rfl h -| succ n, h => +| 0, h => absurd rfl h +| succ n, h => have h₁ : 0 < succ (succ (bit0 n)) from zeroLtSucc _; have h₂ : succ (succ (bit0 n)) = bit0 (succ n) from (Nat.bit0SuccEq n).symm; transRelLeft (fun a b => a < b) h₁ h₂ @@ -517,8 +517,8 @@ protected theorem zeroLtBit1 (n : Nat) : 0 < bit1 n := zeroLtSucc _ protected theorem bit0NeZero : ∀ {n : Nat}, n ≠ 0 → bit0 n ≠ 0 -| 0, h => absurd rfl h -| n+1, h => +| 0, h => absurd rfl h +| n+1, h => suffices (n+1) + (n+1) ≠ 0 from this; suffices succ ((n+1) + n) ≠ 0 from this; fun h => Nat.noConfusion h @@ -534,28 +534,28 @@ protected theorem bit1SuccEq (n : Nat) : bit1 (succ n) = succ (succ (bit1 n)) := Eq.trans (Nat.bit1EqSuccBit0 (succ n)) (congrArg succ (Nat.bit0SuccEq n)) protected theorem bit1NeOne : ∀ {n : Nat}, n ≠ 0 → bit1 n ≠ 1 -| 0, h, h1 => absurd rfl h -| n+1, h, h1 => Nat.noConfusion h1 (fun h2 => absurd h2 (succNeZero _)) +| 0, h, h1 => absurd rfl h +| n+1, h, h1 => Nat.noConfusion h1 (fun h2 => absurd h2 (succNeZero _)) protected theorem bit0NeOne : ∀ (n : Nat), bit0 n ≠ 1 -| 0, h => absurd h (Ne.symm Nat.oneNeZero) -| n+1, h => +| 0, h => absurd h (Ne.symm Nat.oneNeZero) +| n+1, h => have h1 : succ (succ (n + n)) = 1 from succAdd n n ▸ h; Nat.noConfusion h1 (fun h2 => absurd h2 (succNeZero (n + n))) protected theorem addSelfNeOne : ∀ (n : Nat), n + n ≠ 1 -| 0, h => Nat.noConfusion h -| n+1, h => +| 0, h => Nat.noConfusion h +| n+1, h => have h1 : succ (succ (n + n)) = 1 from succAdd n n ▸ h; Nat.noConfusion h1 (fun h2 => absurd h2 (Nat.succNeZero (n + n))) protected theorem bit1NeBit0 : ∀ (n m : Nat), bit1 n ≠ bit0 m -| 0, m, h => absurd h (Ne.symm (Nat.addSelfNeOne m)) -| n+1, 0, h => +| 0, m, h => absurd h (Ne.symm (Nat.addSelfNeOne m)) +| n+1, 0, h => have h1 : succ (bit0 (succ n)) = 0 from h; absurd h1 (Nat.succNeZero _) -| n+1, m+1, h => +| n+1, m+1, h => have h1 : succ (succ (bit1 n)) = succ (succ (bit0 m)) from Nat.bit0SuccEq m ▸ Nat.bit1SuccEq n ▸ h; have h2 : bit1 n = bit0 m from @@ -566,10 +566,10 @@ protected theorem bit0NeBit1 : ∀ (n m : Nat), bit0 n ≠ bit1 m := fun n m => Ne.symm (Nat.bit1NeBit0 m n) protected theorem bit0Inj : ∀ {n m : Nat}, bit0 n = bit0 m → n = m -| 0, 0, h => rfl -| 0, m+1, h => absurd h.symm (succNeZero _) -| n+1, 0, h => absurd h (succNeZero _) -| n+1, m+1, h => +| 0, 0, h => rfl +| 0, m+1, h => absurd h.symm (succNeZero _) +| n+1, 0, h => absurd h (succNeZero _) +| n+1, m+1, h => have (n+1) + n = (m+1) + m from Nat.noConfusion h id; have n + (n+1) = m + (m+1) from Nat.addComm (m+1) m ▸ Nat.addComm (n+1) n ▸ this; have succ (n + n) = succ (m + m) from this; @@ -602,14 +602,14 @@ protected theorem oneNeBit1 {n : Nat} : n ≠ 0 → 1 ≠ bit1 n := fun h => Ne.symm (Nat.bit1NeOne h) protected theorem oneLtBit1 : ∀ {n : Nat}, n ≠ 0 → 1 < bit1 n -| 0, h => absurd rfl h -| succ n, h => +| 0, h => absurd rfl h +| succ n, h => suffices succ 0 < succ (succ (bit1 n)) from (Nat.bit1SuccEq n).symm ▸ this; succLtSucc (zeroLtSucc _) protected theorem oneLtBit0 : ∀ {n : Nat}, n ≠ 0 → 1 < bit0 n -| 0, h => absurd rfl h -| succ n, h => +| 0, h => absurd rfl h +| succ n, h => suffices succ 0 < succ (succ (bit0 n)) from (Nat.bit0SuccEq n).symm ▸ this; succLtSucc (zeroLtSucc _) @@ -623,8 +623,8 @@ protected theorem bit0LtBit1 {n m : Nat} (h : n ≤ m) : bit0 n < bit1 m := ltSuccOfLe (Nat.addLeAdd h h) protected theorem bit1LtBit0 : ∀ {n m : Nat}, n < m → bit1 n < bit0 m -| n, 0, h => absurd h (notLtZero _) -| n, succ m, h => +| n, 0, h => absurd h (notLtZero _) +| n, succ m, h => have n ≤ m from leOfLtSucc h; have succ (n + n) ≤ succ (m + m) from succLeSucc (addLeAdd this this); have succ (n + n) ≤ succ m + m from (succAdd m m).symm ▸ this; @@ -635,8 +635,8 @@ show 1 ≤ succ (bit0 n) from succLeSucc (zeroLe (bit0 n)) protected theorem oneLeBit0 : ∀ (n : Nat), n ≠ 0 → 1 ≤ bit0 n -| 0, h => absurd rfl h -| n+1, h => +| 0, h => absurd rfl h +| n+1, h => suffices 1 ≤ succ (succ (bit0 n)) from Eq.symm (Nat.bit0SuccEq n) ▸ this; succLeSucc (zeroLe (succ (bit0 n))) @@ -676,10 +676,10 @@ theorem powLePowOfLeLeft {n m : Nat} (h : n ≤ m) : ∀ (i : Nat), n^i ≤ m^i | succ i => Nat.mulLeMul (powLePowOfLeLeft i) h theorem powLePowOfLeRight {n : Nat} (hx : n > 0) {i : Nat} : ∀ {j}, i ≤ j → n^i ≤ n^j -| 0, h => +| 0, h => have i = 0 from eqZeroOfLeZero h; this.symm ▸ Nat.leRefl _ -| succ j, h => +| succ j, h => Or.elim (ltOrEqOrLeSucc h) (fun h => show n^i ≤ n^j * n from suffices n^i * 1 ≤ n^j * n from Nat.mulOne (n^i) ▸ this; diff --git a/library/init/data/option/basic.lean b/library/init/data/option/basic.lean index d1410b1169..c0bed31371 100644 --- a/library/init/data/option/basic.lean +++ b/library/init/data/option/basic.lean @@ -16,8 +16,8 @@ def toMonad {m : Type → Type} [Monad m] [Alternative m] {A} : Option A → m A | some a => pure a @[macroInline] def getOrElse {α : Type u} : Option α → α → α -| some x, _ => x -| none, e => e +| some x, _ => x +| none, e => e @[inline] def get {α : Type u} [Inhabited α] : Option α → α | some x => x @@ -36,8 +36,8 @@ def toMonad {m : Type → Type} [Monad m] [Alternative m] {A} : Option A → m A | none => true @[inline] protected def bind {α : Type u} {β : Type v} : Option α → (α → Option β) → Option β -| none, b => none -| some a, b => b a +| none, b => none +| some a, b => b a @[inline] protected def map {α β} (f : α → β) (o : Option α) : Option β := Option.bind o (some ∘ f) @@ -49,8 +49,8 @@ instance : Monad Option := {pure := @some, bind := @Option.bind, map := @Option.map} @[macroInline] protected def orelse {α : Type u} : Option α → Option α → Option α -| some a, _ => some a -| none, b => b +| some a, _ => some a +| none, b => b /- Remark: when using the polymorphic notation `a <|> b` is not a `[macroInline]`. Thus, `a <|> b` will make `Option.orelse` to behave like it was marked as `[inline]`. -/ @@ -65,10 +65,10 @@ instance : Alternative Option := | _, _ => False instance decidableRelLt {α : Type u} (r : α → α → Prop) [s : DecidableRel r] : DecidableRel (Option.lt r) -| none, some y => isTrue trivial -| some x, some y => s x y -| some x, none => isFalse notFalse -| none, none => isFalse notFalse +| none, some y => isTrue trivial +| some x, some y => s x y +| some x, none => isFalse notFalse +| none, none => isFalse notFalse end Option diff --git a/library/init/data/option/instances.lean b/library/init/data/option/instances.lean index 8d0f10b796..9bd25dca91 100644 --- a/library/init/data/option/instances.lean +++ b/library/init/data/option/instances.lean @@ -9,10 +9,10 @@ import init.data.option.basic universes u v theorem Option.eqOfEqSome {α : Type u} : ∀ {x y : Option α}, (∀z, x = some z ↔ y = some z) → x = y -| none, none, h => rfl -| none, some z, h => Option.noConfusion ((h z).2 rfl) -| some z, none, h => Option.noConfusion ((h z).1 rfl) -| some z, some w, h => Option.noConfusion ((h w).2 rfl) (congrArg some) +| none, none, h => rfl +| none, some z, h => Option.noConfusion ((h z).2 rfl) +| some z, none, h => Option.noConfusion ((h z).1 rfl) +| some z, some w, h => Option.noConfusion ((h w).2 rfl) (congrArg some) theorem Option.eqNoneOfIsNone {α : Type u} : ∀ {o : Option α}, o.isNone → o = none | none, h => rfl diff --git a/library/init/data/persistentarray/basic.lean b/library/init/data/persistentarray/basic.lean index 20aac42619..f920b94942 100644 --- a/library/init/data/persistentarray/basic.lean +++ b/library/init/data/persistentarray/basic.lean @@ -51,8 +51,8 @@ abbrev div2Shift (i : USize) (shift : USize) : USize := USize.shift_right i shif abbrev mod2Shift (i : USize) (shift : USize) : USize := USize.land i ((USize.shift_left 1 shift) - 1) partial def getAux [Inhabited α] : PersistentArrayNode α → USize → USize → α -| node cs, i, shift => getAux (cs.get (div2Shift i shift).toNat) (mod2Shift i shift) (shift - initShift) -| leaf cs, i, _ => cs.get i.toNat +| node cs, i, shift => getAux (cs.get (div2Shift i shift).toNat) (mod2Shift i shift) (shift - initShift) +| leaf cs, i, _ => cs.get i.toNat def get [Inhabited α] (t : PersistentArray α) (i : Nat) : α := if i >= t.tailOff then @@ -61,12 +61,12 @@ else getAux t.root (USize.ofNat i) t.shift partial def setAux : PersistentArrayNode α → USize → USize → α → PersistentArrayNode α -| node cs, i, shift, a => +| node cs, i, shift, a => let j := div2Shift i shift; let i := mod2Shift i shift; let shift := shift - initShift; node $ cs.modify j.toNat $ fun c => setAux c i shift a -| leaf cs, i, _, a => leaf (cs.set i.toNat a) +| leaf cs, i, _, a => leaf (cs.set i.toNat a) def set (t : PersistentArray α) (i : Nat) (a : α) : PersistentArray α := if i >= t.tailOff then @@ -75,12 +75,12 @@ else { root := setAux t.root (USize.ofNat i) t.shift a, .. t } @[specialize] partial def modifyAux [Inhabited α] (f : α → α) : PersistentArrayNode α → USize → USize → PersistentArrayNode α -| node cs, i, shift => +| node cs, i, shift => let j := div2Shift i shift; let i := mod2Shift i shift; let shift := shift - initShift; node $ cs.modify j.toNat $ fun c => modifyAux c i shift -| leaf cs, i, _ => leaf (cs.modify i.toNat f) +| leaf cs, i, _ => leaf (cs.modify i.toNat f) @[specialize] def modify [Inhabited α] (t : PersistentArray α) (i : Nat) (f : α → α) : PersistentArray α := if i >= t.tailOff then @@ -179,8 +179,8 @@ variables {m : Type v → Type w} [Monad m] variable {β : Type v} @[specialize] partial def mfoldlAux (f : β → α → m β) : PersistentArrayNode α → β → m β -| node cs, b => cs.mfoldl (fun b c => mfoldlAux c b) b -| leaf vs, b => vs.mfoldl f b +| node cs, b => cs.mfoldl (fun b c => mfoldlAux c b) b +| leaf vs, b => vs.mfoldl f b @[specialize] def mfoldl (t : PersistentArray α) (f : β → α → m β) (b : β) : m β := do b ← mfoldlAux f t.root b; t.tail.mfoldl f b @@ -206,11 +206,11 @@ do b ← t.tail.mfindRev f; | some b => pure (some b) partial def mfoldlFromAux (f : β → α → m β) : PersistentArrayNode α → USize → USize → β → m β -| node cs, i, shift, b => do +| node cs, i, shift, b => do let j := (div2Shift i shift).toNat; b ← mfoldlFromAux (cs.get j) (mod2Shift i shift) (shift - initShift) b; cs.mfoldlFrom (fun b c => mfoldlAux f c b) b (j+1) -| leaf vs, i, _, b => vs.mfoldlFrom f b i.toNat +| leaf vs, i, _, b => vs.mfoldlFrom f b i.toNat def mfoldlFrom (t : PersistentArray α) (f : β → α → m β) (b : β) (ini : Nat) : m β := if ini >= t.tailOff then @@ -266,11 +266,11 @@ structure Stats := (numNodes : Nat) (depth : Nat) (tailSize : Nat) partial def collectStats : PersistentArrayNode α → Stats → Nat → Stats -| node cs, s, d => +| node cs, s, d => cs.foldl (fun s c => collectStats c s (d+1)) { numNodes := s.numNodes + 1, depth := Nat.max d s.depth, .. s } -| leaf vs, s, d => { numNodes := s.numNodes + 1, depth := Nat.max d s.depth, .. s } +| leaf vs, s, d => { numNodes := s.numNodes + 1, depth := Nat.max d s.depth, .. s } def stats (r : PersistentArray α) : Stats := collectStats r.root { numNodes := 0, depth := 0, tailSize := r.tail.size } 0 @@ -283,8 +283,8 @@ instance : HasToString Stats := ⟨Stats.toString⟩ end PersistentArray def List.toPersistentArrayAux {α : Type u} : List α → PersistentArray α → PersistentArray α -| [], t => t -| x::xs, t => List.toPersistentArrayAux xs (t.push x) +| [], t => t +| x::xs, t => List.toPersistentArrayAux xs (t.push x) def List.toPersistentArray {α : Type u} (xs : List α) : PersistentArray α := xs.toPersistentArrayAux {} diff --git a/library/init/data/persistenthashmap/basic.lean b/library/init/data/persistenthashmap/basic.lean index 4be18f8c75..311b2a0ae2 100644 --- a/library/init/data/persistenthashmap/basic.lean +++ b/library/init/data/persistenthashmap/basic.lean @@ -106,7 +106,7 @@ let vs := (vs.push v₁).push v₂; Node.collision ks vs rfl partial def insertAux [HasBeq α] [Hashable α] : Node α β → USize → USize → α → β → Node α β -| Node.collision keys vals heq, _, depth, k, v => +| Node.collision keys vals heq, _, depth, k, v => let newNode := insertAtCollisionNode ⟨Node.collision keys vals heq, IsCollisionNode.mk _ _ _⟩ k v; if depth >= maxDepth || getCollisionNodeSize newNode < maxCollisions then newNode.val else match newNode with @@ -120,7 +120,7 @@ partial def insertAux [HasBeq α] [Hashable α] : Node α β → USize → USize -- toString (div2Shift h (shift * (depth - 1)))) $ fun _ => let h := div2Shift h (shift * (depth - 1)); insertAux entries h depth k v -| Node.entries entries, h, depth, k, v => +| Node.entries entries, h, depth, k, v => let j := (mod2Shift h shift).toNat; Node.entries $ entries.modify j $ fun entry => match entry with @@ -142,13 +142,13 @@ partial def findAtAux [HasBeq α] (keys : Array α) (vals : Array β) (heq : key else none partial def findAux [HasBeq α] : Node α β → USize → α → Option β -| Node.entries entries, h, k => +| Node.entries entries, h, k => let j := (mod2Shift h shift).toNat; match entries.get j with | Entry.null => none | Entry.ref node => findAux node (div2Shift h shift) k | Entry.entry k' v => if k == k' then some v else none -| Node.collision keys vals heq, _, k => findAtAux keys vals heq 0 k +| Node.collision keys vals heq, _, k => findAtAux keys vals heq 0 k def find [HasBeq α] [Hashable α] : PersistentHashMap α β → α → Option β | { root := n, .. }, k => findAux n (hash k) k @@ -209,8 +209,8 @@ variables {m : Type w → Type w'} [Monad m] variables {σ : Type w} @[specialize] partial def mfoldlAux (f : σ → α → β → m σ) : Node α β → σ → m σ -| Node.collision keys vals heq, acc => keys.miterate acc $ fun i k acc => f acc k (vals.fget ⟨i.val, heq ▸ i.isLt⟩) -| Node.entries entries, acc => entries.mfoldl (fun acc entry => +| Node.collision keys vals heq, acc => keys.miterate acc $ fun i k acc => f acc k (vals.fget ⟨i.val, heq ▸ i.isLt⟩) +| Node.entries entries, acc => entries.mfoldl (fun acc entry => match entry with | Entry.null => pure acc | Entry.entry k v => f acc k v @@ -234,12 +234,12 @@ structure Stats := (maxDepth : Nat := 0) partial def collectStats : Node α β → Stats → Nat → Stats -| Node.collision keys _ _, stats, depth => +| Node.collision keys _ _, stats, depth => { numNodes := stats.numNodes + 1, numCollisions := stats.numCollisions + keys.size - 1, maxDepth := Nat.max stats.maxDepth depth, .. stats } -| Node.entries entries, stats, depth => +| Node.entries entries, stats, depth => let stats := { numNodes := stats.numNodes + 1, maxDepth := Nat.max stats.maxDepth depth, diff --git a/library/init/data/rbmap/basic.lean b/library/init/data/rbmap/basic.lean index 7782c5752b..336e39878c 100644 --- a/library/init/data/rbmap/basic.lean +++ b/library/init/data/rbmap/basic.lean @@ -85,12 +85,12 @@ section Insert variables (lt : α → α → Bool) @[specialize] def ins : RBNode α β → ∀ k, β k → RBNode α β -| leaf, kx, vx => node red leaf kx vx leaf -| node red a ky vy b, kx, vx => +| leaf, kx, vx => node red leaf kx vx leaf +| node red a ky vy b, kx, vx => if lt kx ky then node red (ins a kx vx) ky vy b else if lt ky kx then node red a ky vy (ins b kx vx) else node red a kx vx b -| node black a ky vy b, kx, vx => +| node black a ky vy b, kx, vx => if lt kx ky then if isRed a then balance1 ky vy b (ins a kx vx) else node black (ins a kx vx) ky vy b @@ -175,22 +175,22 @@ section Membership variable (lt : α → α → Bool) @[specialize] def findCore : RBNode α β → ∀ (k : α), Option (Sigma (fun k => β k)) -| leaf, x => none -| node _ a ky vy b, x => +| leaf, x => none +| node _ a ky vy b, x => if lt x ky then findCore a x else if lt ky x then findCore b x else some ⟨ky, vy⟩ @[specialize] def find {β : Type v} : RBNode α (fun _ => β) → α → Option β -| leaf, x => none -| node _ a ky vy b, x => +| leaf, x => none +| node _ a ky vy b, x => if lt x ky then find a x else if lt ky x then find b x else some vy @[specialize] def lowerBound : RBNode α β → α → Option (Sigma β) → Option (Sigma β) -| leaf, x, lb => lb -| node _ a ky vy b, x, lb => +| leaf, x, lb => lb +| node _ a ky vy b, x, lb => if lt x ky then lowerBound a x lb else if lt ky x then lowerBound b x (some ⟨ky, vy⟩) else some ⟨ky, vy⟩ @@ -261,7 +261,7 @@ instance [HasRepr α] [HasRepr β] : HasRepr (RBMap α β lt) := ⟨fun t => "rbmapOf " ++ repr t.toList⟩ @[inline] def insert : RBMap α β lt → α → β → RBMap α β lt -| ⟨t, w⟩, k, v => ⟨t.insert lt k v, WellFormed.insertWff w rfl⟩ +| ⟨t, w⟩, k, v => ⟨t.insert lt k v, WellFormed.insertWff w rfl⟩ @[inline] def erase : RBMap α β lt → α → RBMap α β lt | ⟨t, w⟩, k => ⟨t.erase lt k, WellFormed.eraseWff w rfl⟩ diff --git a/library/init/data/repr.lean b/library/init/data/repr.lean index 7f847e74ef..cf33f00f7f 100644 --- a/library/init/data/repr.lean +++ b/library/init/data/repr.lean @@ -76,8 +76,8 @@ if n = 0xf then 'f' else '*' def toDigitsCore (base : Nat) : Nat → Nat → List Char → List Char -| 0, n, ds => ds -| fuel+1, n, ds => +| 0, n, ds => ds +| fuel+1, n, ds => let d := digitChar $ n % base; let n' := n / base; if n' = 0 then d::ds diff --git a/library/init/data/string/basic.lean b/library/init/data/string/basic.lean index af91957029..6bb894f718 100644 --- a/library/init/data/string/basic.lean +++ b/library/init/data/string/basic.lean @@ -63,8 +63,8 @@ private def csize (c : Char) : Nat := c.utf8Size.toNat private def utf8ByteSizeAux : List Char → Nat → Nat -| [], r => r -| c::cs, r => utf8ByteSizeAux cs (r + csize c) +| [], r => r +| c::cs, r => utf8ByteSizeAux cs (r + csize c) @[extern cpp "lean::string_utf8_byte_size"] def utf8ByteSize : (@& String) → Nat @@ -77,16 +77,16 @@ utf8ByteSize s {str := s, startPos := 0, stopPos := s.bsize} private def utf8GetAux : List Char → Pos → Pos → Char -| [], i, p => default Char -| c::cs, i, p => if i = p then c else utf8GetAux cs (i + csize c) p +| [], i, p => default Char +| c::cs, i, p => if i = p then c else utf8GetAux cs (i + csize c) p @[extern cpp "lean::string_utf8_get"] def get : (@& String) → (@& Pos) → Char | ⟨s⟩, p => utf8GetAux s 0 p private def utf8SetAux (c' : Char) : List Char → Pos → Pos → List Char -| [], i, p => [] -| c::cs, i, p => +| [], i, p => [] +| c::cs, i, p => if i = p then (c'::cs) else c::(utf8SetAux cs (i + csize c) p) @[extern cpp "lean::string_utf8_set"] @@ -99,8 +99,8 @@ let c := get s p; p + csize c private def utf8PrevAux : List Char → Pos → Pos → Pos -| [], i, p => 0 -| c::cs, i, p => +| [], i, p => 0 +| c::cs, i, p => let cz := csize c; let i' := i + cz; if i' = p then i else utf8PrevAux cs i' p @@ -142,8 +142,8 @@ if s.bsize == 0 then none else revPosOfAux s c (s.prev s.bsize) private def utf8ExtractAux₂ : List Char → Pos → Pos → List Char -| [], _, _ => [] -| c::cs, i, e => if i = e then [] else c :: utf8ExtractAux₂ cs (i + csize c) e +| [], _, _ => [] +| c::cs, i, e => if i = e then [] else c :: utf8ExtractAux₂ cs (i + csize c) e private def utf8ExtractAux₁ : List Char → Pos → Pos → Pos → List Char | [], _, _, _ => [] diff --git a/library/init/fix.lean b/library/init/fix.lean index 95876f58cc..aa496ca19b 100644 --- a/library/init/fix.lean +++ b/library/init/fix.lean @@ -8,8 +8,8 @@ import init.data.uint universe u def bfix1 {α β : Type u} (base : α → β) (rec : (α → β) → α → β) : Nat → α → β -| 0, a => base a -| n+1, a => rec (bfix1 n) a +| 0, a => base a +| n+1, a => rec (bfix1 n) a @[extern cpp inline "lean::fixpoint(#4, #5)"] def fixCore1 {α β : Type u} (base : @& (α → β)) (rec : (α → β) → α → β) : α → β := @@ -25,8 +25,8 @@ fixCore1 (fun _ => default β) rec fixCore1 (fun _ => default β) rec def bfix2 {α₁ α₂ β : Type u} (base : α₁ → α₂ → β) (rec : (α₁ → α₂ → β) → α₁ → α₂ → β) : Nat → α₁ → α₂ → β -| 0, a₁, a₂ => base a₁ a₂ -| n+1, a₁, a₂ => rec (bfix2 n) a₁ a₂ +| 0, a₁, a₂ => base a₁ a₂ +| n+1, a₁, a₂ => rec (bfix2 n) a₁ a₂ @[extern cpp inline "lean::fixpoint2(#5, #6, #7)"] def fixCore2 {α₁ α₂ β : Type u} (base : α₁ → α₂ → β) (rec : (α₁ → α₂ → β) → α₁ → α₂ → β) : α₁ → α₂ → β := @@ -36,8 +36,8 @@ bfix2 base rec usizeSz fixCore2 (fun _ _ => default β) rec def bfix3 {α₁ α₂ α₃ β : Type u} (base : α₁ → α₂ → α₃ → β) (rec : (α₁ → α₂ → α₃ → β) → α₁ → α₂ → α₃ → β) : Nat → α₁ → α₂ → α₃ → β -| 0, a₁, a₂, a₃ => base a₁ a₂ a₃ -| n+1, a₁, a₂, a₃ => rec (bfix3 n) a₁ a₂ a₃ +| 0, a₁, a₂, a₃ => base a₁ a₂ a₃ +| n+1, a₁, a₂, a₃ => rec (bfix3 n) a₁ a₂ a₃ @[extern cpp inline "lean::fixpoint3(#6, #7, #8, #9)"] def fixCore3 {α₁ α₂ α₃ β : Type u} (base : α₁ → α₂ → α₃ → β) (rec : (α₁ → α₂ → α₃ → β) → α₁ → α₂ → α₃ → β) : α₁ → α₂ → α₃ → β := @@ -47,8 +47,8 @@ bfix3 base rec usizeSz fixCore3 (fun _ _ _ => default β) rec def bfix4 {α₁ α₂ α₃ α₄ β : Type u} (base : α₁ → α₂ → α₃ → α₄ → β) (rec : (α₁ → α₂ → α₃ → α₄ → β) → α₁ → α₂ → α₃ → α₄ → β) : Nat → α₁ → α₂ → α₃ → α₄ → β -| 0, a₁, a₂, a₃, a₄ => base a₁ a₂ a₃ a₄ -| n+1, a₁, a₂, a₃, a₄ => rec (bfix4 n) a₁ a₂ a₃ a₄ +| 0, a₁, a₂, a₃, a₄ => base a₁ a₂ a₃ a₄ +| n+1, a₁, a₂, a₃, a₄ => rec (bfix4 n) a₁ a₂ a₃ a₄ @[extern cpp inline "lean::fixpoint4(#7, #8, #9, #10, #11)"] def fixCore4 {α₁ α₂ α₃ α₄ β : Type u} (base : α₁ → α₂ → α₃ → α₄ → β) (rec : (α₁ → α₂ → α₃ → α₄ → β) → α₁ → α₂ → α₃ → α₄ → β) : α₁ → α₂ → α₃ → α₄ → β := @@ -58,8 +58,8 @@ bfix4 base rec usizeSz fixCore4 (fun _ _ _ _ => default β) rec def bfix5 {α₁ α₂ α₃ α₄ α₅ β : Type u} (base : α₁ → α₂ → α₃ → α₄ → α₅ → β) (rec : (α₁ → α₂ → α₃ → α₄ → α₅ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → β) : Nat → α₁ → α₂ → α₃ → α₄ → α₅ → β -| 0, a₁, a₂, a₃, a₄, a₅ => base a₁ a₂ a₃ a₄ a₅ -| n+1, a₁, a₂, a₃, a₄, a₅ => rec (bfix5 n) a₁ a₂ a₃ a₄ a₅ +| 0, a₁, a₂, a₃, a₄, a₅ => base a₁ a₂ a₃ a₄ a₅ +| n+1, a₁, a₂, a₃, a₄, a₅ => rec (bfix5 n) a₁ a₂ a₃ a₄ a₅ @[extern cpp inline "lean::fixpoint5(#8, #9, #10, #11, #12, #13)"] def fixCore5 {α₁ α₂ α₃ α₄ α₅ β : Type u} (base : α₁ → α₂ → α₃ → α₄ → α₅ → β) (rec : (α₁ → α₂ → α₃ → α₄ → α₅ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → β) : α₁ → α₂ → α₃ → α₄ → α₅ → β := @@ -69,8 +69,8 @@ bfix5 base rec usizeSz fixCore5 (fun _ _ _ _ _ => default β) rec def bfix6 {α₁ α₂ α₃ α₄ α₅ α₆ β : Type u} (base : α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) (rec : (α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) : Nat → α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β -| 0, a₁, a₂, a₃, a₄, a₅, a₆ => base a₁ a₂ a₃ a₄ a₅ a₆ -| n+1, a₁, a₂, a₃, a₄, a₅, a₆ => rec (bfix6 n) a₁ a₂ a₃ a₄ a₅ a₆ +| 0, a₁, a₂, a₃, a₄, a₅, a₆ => base a₁ a₂ a₃ a₄ a₅ a₆ +| n+1, a₁, a₂, a₃, a₄, a₅, a₆ => rec (bfix6 n) a₁ a₂ a₃ a₄ a₅ a₆ @[extern cpp inline "lean::fixpoint6(#9, #10, #11, #12, #13, #14, #15)"] def fixCore6 {α₁ α₂ α₃ α₄ α₅ α₆ β : Type u} (base : α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) (rec : (α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) → α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β) : α₁ → α₂ → α₃ → α₄ → α₅ → α₆ → β := diff --git a/library/init/lean/class.lean b/library/init/lean/class.lean index dbda0488ae..ad591fa1f5 100644 --- a/library/init/lean/class.lean +++ b/library/init/lean/class.lean @@ -94,9 +94,9 @@ else match env.find clsName with | some decl => Except.ok (classExtension.addEntry env (ClassEntry.«class» clsName decl.type.hasOutParam)) private def consumeNLambdas : Nat → Expr → Option Expr -| 0, e => some e -| i+1, Expr.lam _ _ _ b => consumeNLambdas i b -| _, _ => none +| 0, e => some e +| i+1, Expr.lam _ _ _ b => consumeNLambdas i b +| _, _ => none partial def getClassName (env : Environment) : Expr → Option Name | Expr.pi _ _ _ d => getClassName d diff --git a/library/init/lean/compiler/externattr.lean b/library/init/lean/compiler/externattr.lean index 368d72d0d0..a26e01e6a6 100644 --- a/library/init/lean/compiler/externattr.lean +++ b/library/init/lean/compiler/externattr.lean @@ -97,8 +97,8 @@ def getExternAttrData (env : Environment) (n : Name) : Option ExternAttrData := externAttr.getParam env n private def parseOptNum : Nat → String.Iterator → Nat → String.Iterator × Nat -| 0, it, r => (it, r) -| n+1, it, r => +| 0, it, r => (it, r) +| n+1, it, r => if !it.hasNext then (it, r) else let c := it.curr; @@ -107,8 +107,8 @@ private def parseOptNum : Nat → String.Iterator → Nat → String.Iterator × else (it, r) def expandExternPatternAux (args : List String) : Nat → String.Iterator → String → String -| 0, it, r => r -| i+1, it, r => +| 0, it, r => r +| i+1, it, r => if ¬ it.hasNext then r else let c := it.curr; if c ≠ '#' then expandExternPatternAux i it.next (r.push c) @@ -125,10 +125,10 @@ def mkSimpleFnCall (fn : String) (args : List String) : String := fn ++ "(" ++ ((args.intersperse ", ").foldl HasAppend.append "") ++ ")" def expandExternEntry : ExternEntry → List String → Option String -| ExternEntry.adhoc _, args => none -- backend must expand it -| ExternEntry.standard _ fn, args => some (mkSimpleFnCall fn args) -| ExternEntry.inline _ pat, args => some (expandExternPattern pat args) -| ExternEntry.foreign _ fn, args => some (mkSimpleFnCall fn args) +| ExternEntry.adhoc _, args => none -- backend must expand it +| ExternEntry.standard _ fn, args => some (mkSimpleFnCall fn args) +| ExternEntry.inline _ pat, args => some (expandExternPattern pat args) +| ExternEntry.foreign _ fn, args => some (mkSimpleFnCall fn args) def ExternEntry.backend : ExternEntry → Name | ExternEntry.adhoc n => n diff --git a/library/init/lean/compiler/ir/basic.lean b/library/init/lean/compiler/ir/basic.lean index a6baf3bdda..96063ff16a 100644 --- a/library/init/lean/compiler/ir/basic.lean +++ b/library/init/lean/compiler/ir/basic.lean @@ -132,9 +132,9 @@ inductive LitVal | str (v : String) def LitVal.beq : LitVal → LitVal → Bool -| LitVal.num v₁, LitVal.num v₂ => v₁ == v₂ -| LitVal.str v₁, LitVal.str v₂ => v₁ == v₂ -| _, _ => false +| LitVal.num v₁, LitVal.num v₂ => v₁ == v₂ +| LitVal.str v₁, LitVal.str v₂ => v₁ == v₂ +| _, _ => false instance LitVal.HasBeq : HasBeq LitVal := ⟨LitVal.beq⟩ @@ -280,17 +280,17 @@ def FnBody.body : FnBody → FnBody | other => other def FnBody.setBody : FnBody → FnBody → FnBody -| FnBody.vdecl x t v _, b => FnBody.vdecl x t v b -| FnBody.jdecl j xs v _, b => FnBody.jdecl j xs v b -| FnBody.set x i y _, b => FnBody.set x i y b -| FnBody.uset x i y _, b => FnBody.uset x i y b -| FnBody.sset x i o y t _, b => FnBody.sset x i o y t b -| FnBody.setTag x i _, b => FnBody.setTag x i b -| FnBody.inc x n c _, b => FnBody.inc x n c b -| FnBody.dec x n c _, b => FnBody.dec x n c b -| FnBody.del x _, b => FnBody.del x b -| FnBody.mdata d _, b => FnBody.mdata d b -| other, b => other +| FnBody.vdecl x t v _, b => FnBody.vdecl x t v b +| FnBody.jdecl j xs v _, b => FnBody.jdecl j xs v b +| FnBody.set x i y _, b => FnBody.set x i y b +| FnBody.uset x i y _, b => FnBody.uset x i y b +| FnBody.sset x i o y t _, b => FnBody.sset x i o y t b +| FnBody.setTag x i _, b => FnBody.setTag x i b +| FnBody.inc x n c _, b => FnBody.inc x n c b +| FnBody.dec x n c _, b => FnBody.dec x n c b +| FnBody.del x _, b => FnBody.del x b +| FnBody.mdata d _, b => FnBody.mdata d b +| other, b => other @[inline] def FnBody.resetBody (b : FnBody) : FnBody := b.setBody FnBody.nil @@ -307,8 +307,8 @@ def AltCore.body : Alt → FnBody | Alt.default b => b def AltCore.setBody : Alt → FnBody → Alt -| Alt.ctor c _, b => Alt.ctor c b -| Alt.default _, b => Alt.default b +| Alt.ctor c _, b => Alt.ctor c b +| Alt.default _, b => Alt.default b @[inline] def AltCore.modifyBody (f : FnBody → FnBody) : AltCore FnBody → Alt | Alt.ctor c b => Alt.ctor c (f b) @@ -476,21 +476,21 @@ Array.isEqv args₁ args₂ (fun a b => aeqv ρ a b) instance args.hasAeqv : HasAlphaEqv (Array Arg) := ⟨args.alphaEqv⟩ def Expr.alphaEqv (ρ : IndexRenaming) : Expr → Expr → Bool -| Expr.ctor i₁ ys₁, Expr.ctor i₂ ys₂ => i₁ == i₂ && aeqv ρ ys₁ ys₂ -| Expr.reset n₁ x₁, Expr.reset n₂ x₂ => n₁ == n₂ && aeqv ρ x₁ x₂ -| Expr.reuse x₁ i₁ u₁ ys₁, Expr.reuse x₂ i₂ u₂ ys₂ => aeqv ρ x₁ x₂ && i₁ == i₂ && u₁ == u₂ && aeqv ρ ys₁ ys₂ -| Expr.proj i₁ x₁, Expr.proj i₂ x₂ => i₁ == i₂ && aeqv ρ x₁ x₂ -| Expr.uproj i₁ x₁, Expr.uproj i₂ x₂ => i₁ == i₂ && aeqv ρ x₁ x₂ -| Expr.sproj n₁ o₁ x₁, Expr.sproj n₂ o₂ x₂ => n₁ == n₂ && o₁ == o₂ && aeqv ρ x₁ x₂ -| Expr.fap c₁ ys₁, Expr.fap c₂ ys₂ => c₁ == c₂ && aeqv ρ ys₁ ys₂ -| Expr.pap c₁ ys₁, Expr.pap c₂ ys₂ => c₁ == c₂ && aeqv ρ ys₂ ys₂ -| Expr.ap x₁ ys₁, Expr.ap x₂ ys₂ => aeqv ρ x₁ x₂ && aeqv ρ ys₁ ys₂ -| Expr.box ty₁ x₁, Expr.box ty₂ x₂ => ty₁ == ty₂ && aeqv ρ x₁ x₂ -| Expr.unbox x₁, Expr.unbox x₂ => aeqv ρ x₁ x₂ -| Expr.lit v₁, Expr.lit v₂ => v₁ == v₂ -| Expr.isShared x₁, Expr.isShared x₂ => aeqv ρ x₁ x₂ -| Expr.isTaggedPtr x₁, Expr.isTaggedPtr x₂ => aeqv ρ x₁ x₂ -| _, _ => false +| Expr.ctor i₁ ys₁, Expr.ctor i₂ ys₂ => i₁ == i₂ && aeqv ρ ys₁ ys₂ +| Expr.reset n₁ x₁, Expr.reset n₂ x₂ => n₁ == n₂ && aeqv ρ x₁ x₂ +| Expr.reuse x₁ i₁ u₁ ys₁, Expr.reuse x₂ i₂ u₂ ys₂ => aeqv ρ x₁ x₂ && i₁ == i₂ && u₁ == u₂ && aeqv ρ ys₁ ys₂ +| Expr.proj i₁ x₁, Expr.proj i₂ x₂ => i₁ == i₂ && aeqv ρ x₁ x₂ +| Expr.uproj i₁ x₁, Expr.uproj i₂ x₂ => i₁ == i₂ && aeqv ρ x₁ x₂ +| Expr.sproj n₁ o₁ x₁, Expr.sproj n₂ o₂ x₂ => n₁ == n₂ && o₁ == o₂ && aeqv ρ x₁ x₂ +| Expr.fap c₁ ys₁, Expr.fap c₂ ys₂ => c₁ == c₂ && aeqv ρ ys₁ ys₂ +| Expr.pap c₁ ys₁, Expr.pap c₂ ys₂ => c₁ == c₂ && aeqv ρ ys₂ ys₂ +| Expr.ap x₁ ys₁, Expr.ap x₂ ys₂ => aeqv ρ x₁ x₂ && aeqv ρ ys₁ ys₂ +| Expr.box ty₁ x₁, Expr.box ty₂ x₂ => ty₁ == ty₂ && aeqv ρ x₁ x₂ +| Expr.unbox x₁, Expr.unbox x₂ => aeqv ρ x₁ x₂ +| Expr.lit v₁, Expr.lit v₂ => v₁ == v₂ +| Expr.isShared x₁, Expr.isShared x₂ => aeqv ρ x₁ x₂ +| Expr.isTaggedPtr x₁, Expr.isTaggedPtr x₂ => aeqv ρ x₁ x₂ +| _, _ => false instance Expr.hasAeqv : HasAlphaEqv Expr:= ⟨Expr.alphaEqv⟩ @@ -506,28 +506,28 @@ if ps₁.size != ps₂.size then none else Array.foldl₂ (fun ρ p₁ p₂ => do ρ ← ρ; addParamRename ρ p₁ p₂) (some ρ) ps₁ ps₂ partial def FnBody.alphaEqv : IndexRenaming → FnBody → FnBody → Bool -| ρ, FnBody.vdecl x₁ t₁ v₁ b₁, FnBody.vdecl x₂ t₂ v₂ b₂ => t₁ == t₂ && aeqv ρ v₁ v₂ && FnBody.alphaEqv (addVarRename ρ x₁.idx x₂.idx) b₁ b₂ -| ρ, FnBody.jdecl j₁ ys₁ v₁ b₁, FnBody.jdecl j₂ ys₂ v₂ b₂ => match addParamsRename ρ ys₁ ys₂ with +| ρ, FnBody.vdecl x₁ t₁ v₁ b₁, FnBody.vdecl x₂ t₂ v₂ b₂ => t₁ == t₂ && aeqv ρ v₁ v₂ && FnBody.alphaEqv (addVarRename ρ x₁.idx x₂.idx) b₁ b₂ +| ρ, FnBody.jdecl j₁ ys₁ v₁ b₁, FnBody.jdecl j₂ ys₂ v₂ b₂ => match addParamsRename ρ ys₁ ys₂ with | some ρ' => FnBody.alphaEqv ρ' v₁ v₂ && FnBody.alphaEqv (addVarRename ρ j₁.idx j₂.idx) b₁ b₂ | none => false -| ρ, FnBody.set x₁ i₁ y₁ b₁, FnBody.set x₂ i₂ y₂ b₂ => aeqv ρ x₁ x₂ && i₁ == i₂ && aeqv ρ y₁ y₂ && FnBody.alphaEqv ρ b₁ b₂ -| ρ, FnBody.uset x₁ i₁ y₁ b₁, FnBody.uset x₂ i₂ y₂ b₂ => aeqv ρ x₁ x₂ && i₁ == i₂ && aeqv ρ y₁ y₂ && FnBody.alphaEqv ρ b₁ b₂ -| ρ, FnBody.sset x₁ i₁ o₁ y₁ t₁ b₁, FnBody.sset x₂ i₂ o₂ y₂ t₂ b₂ => +| ρ, FnBody.set x₁ i₁ y₁ b₁, FnBody.set x₂ i₂ y₂ b₂ => aeqv ρ x₁ x₂ && i₁ == i₂ && aeqv ρ y₁ y₂ && FnBody.alphaEqv ρ b₁ b₂ +| ρ, FnBody.uset x₁ i₁ y₁ b₁, FnBody.uset x₂ i₂ y₂ b₂ => aeqv ρ x₁ x₂ && i₁ == i₂ && aeqv ρ y₁ y₂ && FnBody.alphaEqv ρ b₁ b₂ +| ρ, FnBody.sset x₁ i₁ o₁ y₁ t₁ b₁, FnBody.sset x₂ i₂ o₂ y₂ t₂ b₂ => aeqv ρ x₁ x₂ && i₁ = i₂ && o₁ = o₂ && aeqv ρ y₁ y₂ && t₁ == t₂ && FnBody.alphaEqv ρ b₁ b₂ -| ρ, FnBody.setTag x₁ i₁ b₁, FnBody.setTag x₂ i₂ b₂ => aeqv ρ x₁ x₂ && i₁ == i₂ && FnBody.alphaEqv ρ b₁ b₂ -| ρ, FnBody.inc x₁ n₁ c₁ b₁, FnBody.inc x₂ n₂ c₂ b₂ => aeqv ρ x₁ x₂ && n₁ == n₂ && c₁ == c₂ && FnBody.alphaEqv ρ b₁ b₂ -| ρ, FnBody.dec x₁ n₁ c₁ b₁, FnBody.dec x₂ n₂ c₂ b₂ => aeqv ρ x₁ x₂ && n₁ == n₂ && c₁ == c₂ && FnBody.alphaEqv ρ b₁ b₂ -| ρ, FnBody.del x₁ b₁, FnBody.del x₂ b₂ => aeqv ρ x₁ x₂ && FnBody.alphaEqv ρ b₁ b₂ -| ρ, FnBody.mdata m₁ b₁, FnBody.mdata m₂ b₂ => m₁ == m₂ && FnBody.alphaEqv ρ b₁ b₂ -| ρ, FnBody.case n₁ x₁ alts₁, FnBody.case n₂ x₂ alts₂ => n₁ == n₂ && aeqv ρ x₁ x₂ && Array.isEqv alts₁ alts₂ (fun alt₁ alt₂ => +| ρ, FnBody.setTag x₁ i₁ b₁, FnBody.setTag x₂ i₂ b₂ => aeqv ρ x₁ x₂ && i₁ == i₂ && FnBody.alphaEqv ρ b₁ b₂ +| ρ, FnBody.inc x₁ n₁ c₁ b₁, FnBody.inc x₂ n₂ c₂ b₂ => aeqv ρ x₁ x₂ && n₁ == n₂ && c₁ == c₂ && FnBody.alphaEqv ρ b₁ b₂ +| ρ, FnBody.dec x₁ n₁ c₁ b₁, FnBody.dec x₂ n₂ c₂ b₂ => aeqv ρ x₁ x₂ && n₁ == n₂ && c₁ == c₂ && FnBody.alphaEqv ρ b₁ b₂ +| ρ, FnBody.del x₁ b₁, FnBody.del x₂ b₂ => aeqv ρ x₁ x₂ && FnBody.alphaEqv ρ b₁ b₂ +| ρ, FnBody.mdata m₁ b₁, FnBody.mdata m₂ b₂ => m₁ == m₂ && FnBody.alphaEqv ρ b₁ b₂ +| ρ, FnBody.case n₁ x₁ alts₁, FnBody.case n₂ x₂ alts₂ => n₁ == n₂ && aeqv ρ x₁ x₂ && Array.isEqv alts₁ alts₂ (fun alt₁ alt₂ => match alt₁, alt₂ with | Alt.ctor i₁ b₁, Alt.ctor i₂ b₂ => i₁ == i₂ && FnBody.alphaEqv ρ b₁ b₂ | Alt.default b₁, Alt.default b₂ => FnBody.alphaEqv ρ b₁ b₂ | _, _ => false) -| ρ, FnBody.jmp j₁ ys₁, FnBody.jmp j₂ ys₂ => j₁ == j₂ && aeqv ρ ys₁ ys₂ -| ρ, FnBody.ret x₁, FnBody.ret x₂ => aeqv ρ x₁ x₂ -| _, FnBody.unreachable, FnBody.unreachable => true -| _, _, _ => false +| ρ, FnBody.jmp j₁ ys₁, FnBody.jmp j₂ ys₂ => j₁ == j₂ && aeqv ρ ys₁ ys₂ +| ρ, FnBody.ret x₁, FnBody.ret x₂ => aeqv ρ x₁ x₂ +| _, FnBody.unreachable, FnBody.unreachable => true +| _, _, _ => false def FnBody.beq (b₁ b₂ : FnBody) : Bool := FnBody.alphaEqv ∅ b₁ b₂ diff --git a/library/init/lean/compiler/ir/borrow.lean b/library/init/lean/compiler/ir/borrow.lean index fb602dd150..97c92ef1d1 100644 --- a/library/init/lean/compiler/ir/borrow.lean +++ b/library/init/lean/compiler/ir/borrow.lean @@ -24,9 +24,9 @@ inductive Key namespace Key def beq : Key → Key → Bool -| decl n₁, decl n₂ => n₁ == n₂ -| jp n₁ id₁, jp n₂ id₂ => n₁ == n₂ && id₁ == id₂ -| _, _ => false +| decl n₁, decl n₂ => n₁ == n₂ +| jp n₁ id₁, jp n₂ id₂ => n₁ == n₂ && id₁ == id₂ +| _, _ => false instance : HasBeq Key := ⟨beq⟩ diff --git a/library/init/lean/compiler/ir/emitcpp.lean b/library/init/lean/compiler/ir/emitcpp.lean index d2f75f3d2f..27c9282e3e 100644 --- a/library/init/lean/compiler/ir/emitcpp.lean +++ b/library/init/lean/compiler/ir/emitcpp.lean @@ -277,14 +277,14 @@ def declareParams (ps : Array Param) : M Unit := ps.mfor $ fun p => declareVar p.x p.ty partial def declareVars : FnBody → Bool → M Bool -| e@(FnBody.vdecl x t _ b), d => do +| e@(FnBody.vdecl x t _ b), d => do ctx ← read; if isTailCallTo ctx.mainFn e then pure d else declareVar x t *> declareVars b true -| FnBody.jdecl j xs _ b, d => declareParams xs *> declareVars b (d || xs.size > 0) -| e, d => if e.isTerminal then pure d else declareVars e.body d +| FnBody.jdecl j xs _ b, d => declareParams xs *> declareVars b (d || xs.size > 0) +| e, d => if e.isTerminal then pure d else declareVars e.body d def emitTag (x : VarId) : M Unit := do diff --git a/library/init/lean/compiler/ir/livevars.lean b/library/init/lean/compiler/ir/livevars.lean index 5c803a8d5e..79e5d604bd 100644 --- a/library/init/lean/compiler/ir/livevars.lean +++ b/library/init/lean/compiler/ir/livevars.lean @@ -132,23 +132,23 @@ def collectExpr : Expr → Collector | Expr.isTaggedPtr x => collectVar x partial def collectFnBody : FnBody → JPLiveVarMap → Collector -| FnBody.vdecl x _ v b, m => collectExpr v ∘ collectFnBody b m ∘ bindVar x -| FnBody.jdecl j ys v b, m => +| FnBody.vdecl x _ v b, m => collectExpr v ∘ collectFnBody b m ∘ bindVar x +| FnBody.jdecl j ys v b, m => let jLiveVars := (collectFnBody v m ∘ bindParams ys) {}; let m := m.insert j jLiveVars; collectFnBody b m -| FnBody.set x _ y b, m => collectVar x ∘ collectArg y ∘ collectFnBody b m -| FnBody.setTag x _ b, m => collectVar x ∘ collectFnBody b m -| FnBody.uset x _ y b, m => collectVar x ∘ collectVar y ∘ collectFnBody b m -| FnBody.sset x _ _ y _ b, m => collectVar x ∘ collectVar y ∘ collectFnBody b m -| FnBody.inc x _ _ b, m => collectVar x ∘ collectFnBody b m -| FnBody.dec x _ _ b, m => collectVar x ∘ collectFnBody b m -| FnBody.del x b, m => collectVar x ∘ collectFnBody b m -| FnBody.mdata _ b, m => collectFnBody b m -| FnBody.ret x, m => collectArg x -| FnBody.case _ x alts, m => collectVar x ∘ collectArray alts (fun alt => collectFnBody alt.body m) -| FnBody.unreachable, m => skip -| FnBody.jmp j xs, m => collectJP m j ∘ collectArgs xs +| FnBody.set x _ y b, m => collectVar x ∘ collectArg y ∘ collectFnBody b m +| FnBody.setTag x _ b, m => collectVar x ∘ collectFnBody b m +| FnBody.uset x _ y b, m => collectVar x ∘ collectVar y ∘ collectFnBody b m +| FnBody.sset x _ _ y _ b, m => collectVar x ∘ collectVar y ∘ collectFnBody b m +| FnBody.inc x _ _ b, m => collectVar x ∘ collectFnBody b m +| FnBody.dec x _ _ b, m => collectVar x ∘ collectFnBody b m +| FnBody.del x b, m => collectVar x ∘ collectFnBody b m +| FnBody.mdata _ b, m => collectFnBody b m +| FnBody.ret x, m => collectArg x +| FnBody.case _ x alts, m => collectVar x ∘ collectArray alts (fun alt => collectFnBody alt.body m) +| FnBody.unreachable, m => skip +| FnBody.jmp j xs, m => collectJP m j ∘ collectArgs xs def updateJPLiveVarMap (j : JoinPointId) (ys : Array Param) (v : FnBody) (m : JPLiveVarMap) : JPLiveVarMap := let jLiveVars := (collectFnBody v m ∘ bindParams ys) {}; diff --git a/library/init/lean/compiler/ir/normids.lean b/library/init/lean/compiler/ir/normids.lean index 6e887baeb1..eafa4a3371 100644 --- a/library/init/lean/compiler/ir/normids.lean +++ b/library/init/lean/compiler/ir/normids.lean @@ -61,20 +61,20 @@ def normArgs (as : Array Arg) : M (Array Arg) := fun m => as.map $ fun a => normArg a m def normExpr : Expr → M Expr -| Expr.ctor c ys, m => Expr.ctor c (normArgs ys m) -| Expr.reset n x, m => Expr.reset n (normVar x m) -| Expr.reuse x c u ys, m => Expr.reuse (normVar x m) c u (normArgs ys m) -| Expr.proj i x, m => Expr.proj i (normVar x m) -| Expr.uproj i x, m => Expr.uproj i (normVar x m) -| Expr.sproj n o x, m => Expr.sproj n o (normVar x m) -| Expr.fap c ys, m => Expr.fap c (normArgs ys m) -| Expr.pap c ys, m => Expr.pap c (normArgs ys m) -| Expr.ap x ys, m => Expr.ap (normVar x m) (normArgs ys m) -| Expr.box t x, m => Expr.box t (normVar x m) -| Expr.unbox x, m => Expr.unbox (normVar x m) -| Expr.isShared x, m => Expr.isShared (normVar x m) -| Expr.isTaggedPtr x, m => Expr.isTaggedPtr (normVar x m) -| e@(Expr.lit v), m => e +| Expr.ctor c ys, m => Expr.ctor c (normArgs ys m) +| Expr.reset n x, m => Expr.reset n (normVar x m) +| Expr.reuse x c u ys, m => Expr.reuse (normVar x m) c u (normArgs ys m) +| Expr.proj i x, m => Expr.proj i (normVar x m) +| Expr.uproj i x, m => Expr.uproj i (normVar x m) +| Expr.sproj n o x, m => Expr.sproj n o (normVar x m) +| Expr.fap c ys, m => Expr.fap c (normArgs ys m) +| Expr.pap c ys, m => Expr.pap c (normArgs ys m) +| Expr.ap x ys, m => Expr.ap (normVar x m) (normArgs ys m) +| Expr.box t x, m => Expr.box t (normVar x m) +| Expr.unbox x, m => Expr.unbox (normVar x m) +| Expr.isShared x, m => Expr.isShared (normVar x m) +| Expr.isTaggedPtr x, m => Expr.isTaggedPtr (normVar x m) +| e@(Expr.lit v), m => e abbrev N := ReaderT IndexRenaming (State Nat) diff --git a/library/init/lean/compiler/namemangling.lean b/library/init/lean/compiler/namemangling.lean index 24684a1402..fe0270bb33 100644 --- a/library/init/lean/compiler/namemangling.lean +++ b/library/init/lean/compiler/namemangling.lean @@ -8,8 +8,8 @@ import init.lean.name namespace Lean private def String.mangleAux : Nat → String.Iterator → String → String -| 0, it, r => r -| i+1, it, r => +| 0, it, r => r +| i+1, it, r => let c := it.curr; if c.isAlpha || c.isDigit then String.mangleAux i it.next (r.push c) diff --git a/library/init/lean/environment.lean b/library/init/lean/environment.lean index bf68386c0f..0aa9726477 100644 --- a/library/init/lean/environment.lean +++ b/library/init/lean/environment.lean @@ -425,8 +425,8 @@ def writeModule (env : Environment) (fname : String) : IO Unit := do modData ← mkModuleData env; saveModuleData fname modData partial def importModulesAux : List Name → (NameSet × Array ModuleData) → IO (NameSet × Array ModuleData) -| [], r => pure r -| m::ms, (s, mods) => +| [], r => pure r +| m::ms, (s, mods) => if s.contains m then importModulesAux ms (s, mods) else do diff --git a/library/init/lean/expr.lean b/library/init/lean/expr.lean index 3a5d31c11d..48410dc3a4 100644 --- a/library/init/lean/expr.lean +++ b/library/init/lean/expr.lean @@ -86,8 +86,8 @@ def getAppFn : Expr → Expr | e => e def getAppNumArgsAux : Expr → Nat → Nat -| Expr.app f a, n => getAppNumArgsAux f (n+1) -| e, n => n +| Expr.app f a, n => getAppNumArgsAux f (n+1) +| e, n => n def getAppNumArgs (e : Expr) : Nat := getAppNumArgsAux e 0 @@ -98,9 +98,9 @@ match e.getAppFn with | _ => false def isAppOfArity : Expr → Name → Nat → Bool -| Expr.const c _, n, 0 => c == n -| Expr.app f _, n, a+1 => isAppOfArity f n a -| _, _, _ => false +| Expr.const c _, n, 0 => c == n +| Expr.app f _, n, a+1 => isAppOfArity f n a +| _, _, _ => false end Expr diff --git a/library/init/lean/format.lean b/library/init/lean/format.lean index 149d0e6f77..bf6609f18b 100644 --- a/library/init/lean/format.lean +++ b/library/init/lean/format.lean @@ -64,16 +64,16 @@ else { space := newSpace, exceeded := newSpace > w } def spaceUptoLine : Format → Nat → SpaceResult -| nil, w => {} -| line, w => { found := true } -| text s, w => { space := s.length, exceeded := s.length > w } -| compose _ f₁ f₂, w => merge w (spaceUptoLine f₁ w) (spaceUptoLine f₂ w) -| nest _ f, w => spaceUptoLine f w -| choice f₁ f₂, w => spaceUptoLine f₂ w +| nil, w => {} +| line, w => { found := true } +| text s, w => { space := s.length, exceeded := s.length > w } +| compose _ f₁ f₂, w => merge w (spaceUptoLine f₁ w) (spaceUptoLine f₂ w) +| nest _ f, w => spaceUptoLine f w +| choice f₁ f₂, w => spaceUptoLine f₂ w def spaceUptoLine' : List (Nat × Format) → Nat → SpaceResult -| [], w => {} -| p::ps, w => merge w (spaceUptoLine p.2 w) (spaceUptoLine' ps w) +| [], w => {} +| p::ps, w => merge w (spaceUptoLine p.2 w) (spaceUptoLine' ps w) partial def be : Nat → Nat → String → List (Nat × Format) → String | w, k, out, [] => out @@ -139,17 +139,17 @@ instance formatHasFormat : HasFormat Format := instance stringHasFormat : HasFormat String := ⟨Format.text⟩ def Format.joinSep {α : Type u} [HasFormat α] : List α → Format → Format -| [], sep => nil -| [a], sep => format a -| a::as, sep => format a ++ sep ++ Format.joinSep as sep +| [], sep => nil +| [a], sep => format a +| a::as, sep => format a ++ sep ++ Format.joinSep as sep def Format.prefixJoin {α : Type u} [HasFormat α] (pre : Format) : List α → Format | [] => nil | a::as => pre ++ format a ++ Format.prefixJoin as def Format.joinSuffix {α : Type u} [HasFormat α] : List α → Format → Format -| [], suffix => nil -| a::as, suffix => format a ++ suffix ++ Format.joinSuffix as suffix +| [], suffix => nil +| a::as, suffix => format a ++ suffix ++ Format.joinSuffix as suffix def List.format {α : Type u} [HasFormat α] : List α → Format | [] => "[]" diff --git a/library/init/lean/kvmap.lean b/library/init/lean/kvmap.lean index 3a2d0586c0..2ed13ebbd9 100644 --- a/library/init/lean/kvmap.lean +++ b/library/init/lean/kvmap.lean @@ -16,10 +16,10 @@ inductive DataValue | ofInt (v : Int) def DataValue.beq : DataValue → DataValue → Bool -| DataValue.ofString s₁, DataValue.ofString s₂ => s₁ = s₂ -| DataValue.ofNat n₁, DataValue.ofNat n₂ => n₂ = n₂ -| DataValue.ofBool b₁, DataValue.ofBool b₂ => b₁ = b₂ -| _, _ => false +| DataValue.ofString s₁, DataValue.ofString s₂ => s₁ = s₂ +| DataValue.ofNat n₁, DataValue.ofNat n₂ => n₂ = n₂ +| DataValue.ofBool b₁, DataValue.ofBool b₂ => b₁ = b₂ +| _, _ => false instance DataValue.HasBeq : HasBeq DataValue := ⟨DataValue.beq⟩ @@ -37,15 +37,15 @@ structure KVMap := namespace KVMap def findCore : List (Name × DataValue) → Name → Option DataValue -| [], k' => none -| (k,v)::m, k' => if k = k' then some v else findCore m k' +| [], k' => none +| (k,v)::m, k' => if k = k' then some v else findCore m k' def find : KVMap → Name → Option DataValue | ⟨m⟩, k => findCore m k def insertCore : List (Name × DataValue) → Name → DataValue → List (Name × DataValue) -| [], k', v' => [(k',v')] -| (k,v)::m, k', v' => if k = k' then (k, v') :: m else (k, v) :: insertCore m k' v' +| [], k', v' => [(k',v')] +| (k,v)::m, k', v' => if k = k' then (k, v') :: m else (k, v) :: insertCore m k' v' def insert : KVMap → Name → DataValue → KVMap | ⟨m⟩, k, v => ⟨insertCore m k v⟩ @@ -94,8 +94,8 @@ def setName (m : KVMap) (k : Name) (v : Name) : KVMap := m.insert k (DataValue.ofName v) def subsetAux : List (Name × DataValue) → KVMap → Bool -| [], m₂ => true -| (k, v₁)::m₁, m₂ => +| [], m₂ => true +| (k, v₁)::m₁, m₂ => match m₂.find k with | some v₂ => v₁ == v₂ && subsetAux m₁ m₂ | none => false diff --git a/library/init/lean/level.lean b/library/init/lean/level.lean index 3bd8eed09b..1225ed9005 100644 --- a/library/init/lean/level.lean +++ b/library/init/lean/level.lean @@ -105,14 +105,14 @@ def parenIfFalse : Format → Bool → Format | r::rs => Format.line ++ fmt r ++ formatLst rs partial def Result.format : Result → Bool → Format -| Result.leaf f, _ => f -| Result.num k, _ => toString k -| Result.offset f 0, r => Result.format f r -| Result.offset f (k+1), r => +| Result.leaf f, _ => f +| Result.num k, _ => toString k +| Result.offset f 0, r => Result.format f r +| Result.offset f (k+1), r => let f' := Result.format f false; parenIfFalse (f' ++ "+" ++ fmt (k+1)) r -| Result.maxNode fs, r => parenIfFalse (Format.group $ "max" ++ formatLst (fun r => Result.format r false) fs) r -| Result.imaxNode fs, r => parenIfFalse (Format.group $ "imax" ++ formatLst (fun r => Result.format r false) fs) r +| Result.maxNode fs, r => parenIfFalse (Format.group $ "max" ++ formatLst (fun r => Result.format r false) fs) r +| Result.imaxNode fs, r => parenIfFalse (Format.group $ "imax" ++ formatLst (fun r => Result.format r false) fs) r def Level.toResult : Level → Result | Level.zero => Result.num 0 diff --git a/library/init/lean/localcontext.lean b/library/init/lean/localcontext.lean index 4780666c1d..5dbbd38a91 100644 --- a/library/init/lean/localcontext.lean +++ b/library/init/lean/localcontext.lean @@ -50,8 +50,8 @@ def value : LocalDecl → Expr | ldecl _ _ _ _ v => v def updateUserName : LocalDecl → Name → LocalDecl -| cdecl index name _ type bi, userName => cdecl index name userName type bi -| ldecl index name _ type val, userName => ldecl index name userName type val +| cdecl index name _ type bi, userName => cdecl index name userName type bi +| ldecl index name _ type val, userName => ldecl index name userName type val end LocalDecl diff --git a/library/init/lean/name.lean b/library/init/lean/name.lean index 4ec620d58a..b81c89f2ee 100644 --- a/library/init/lean/name.lean +++ b/library/init/lean/name.lean @@ -49,9 +49,9 @@ def getNumParts : Name → Nat | mkNumeral p _ => getNumParts p + 1 def updatePrefix : Name → Name → Name -| anonymous, newP => anonymous -| mkString p s, newP => mkString newP s -| mkNumeral p s, newP => mkNumeral newP s +| anonymous, newP => anonymous +| mkString p s, newP => mkString newP s +| mkNumeral p s, newP => mkNumeral newP s def components' : Name → List Name | anonymous => [] @@ -63,25 +63,25 @@ n.components'.reverse @[extern "lean_name_dec_eq"] protected def decEq : ∀ (a b : @& Name), Decidable (a = b) -| anonymous, anonymous => isTrue rfl -| mkString p₁ s₁, mkString p₂ s₂ => +| anonymous, anonymous => isTrue rfl +| mkString p₁ s₁, mkString p₂ s₂ => if h₁ : s₁ = s₂ then match decEq p₁ p₂ with | isTrue h₂ => isTrue $ h₁ ▸ h₂ ▸ rfl | isFalse h₂ => isFalse $ fun h => Name.noConfusion h $ fun hp hs => absurd hp h₂ else isFalse $ fun h => Name.noConfusion h $ fun hp hs => absurd hs h₁ -| mkNumeral p₁ n₁, mkNumeral p₂ n₂ => +| mkNumeral p₁ n₁, mkNumeral p₂ n₂ => if h₁ : n₁ = n₂ then match decEq p₁ p₂ with | isTrue h₂ => isTrue $ h₁ ▸ h₂ ▸ rfl | isFalse h₂ => isFalse $ fun h => Name.noConfusion h $ fun hp hs => absurd hp h₂ else isFalse $ fun h => Name.noConfusion h $ fun hp hs => absurd hs h₁ -| anonymous, mkString _ _ => isFalse $ fun h => Name.noConfusion h -| anonymous, mkNumeral _ _ => isFalse $ fun h => Name.noConfusion h -| mkString _ _, anonymous => isFalse $ fun h => Name.noConfusion h -| mkString _ _, mkNumeral _ _ => isFalse $ fun h => Name.noConfusion h -| mkNumeral _ _, anonymous => isFalse $ fun h => Name.noConfusion h -| mkNumeral _ _, mkString _ _ => isFalse $ fun h => Name.noConfusion h +| anonymous, mkString _ _ => isFalse $ fun h => Name.noConfusion h +| anonymous, mkNumeral _ _ => isFalse $ fun h => Name.noConfusion h +| mkString _ _, anonymous => isFalse $ fun h => Name.noConfusion h +| mkString _ _, mkNumeral _ _ => isFalse $ fun h => Name.noConfusion h +| mkNumeral _ _, anonymous => isFalse $ fun h => Name.noConfusion h +| mkNumeral _ _, mkString _ _ => isFalse $ fun h => Name.noConfusion h instance : DecidableEq Name := {decEq := Name.decEq} @@ -120,12 +120,12 @@ def isPrefixOf : Name → Name → Bool | p, n@(mkString p' _) => p == n || isPrefixOf p p' def quickLtCore : Name → Name → Bool -| anonymous, anonymous => false -| anonymous, _ => true -| mkNumeral n v, mkNumeral n' v' => v < v' || (v = v' && n.quickLtCore n') -| mkNumeral _ _, mkString _ _ => true -| mkString n s, mkString n' s' => s < s' || (s = s' && n.quickLtCore n') -| _, _ => false +| anonymous, anonymous => false +| anonymous, _ => true +| mkNumeral n v, mkNumeral n' v' => v < v' || (v = v' && n.quickLtCore n') +| mkNumeral _ _, mkString _ _ => true +| mkString n s, mkString n' s' => s < s' || (s = s' && n.quickLtCore n') +| _, _ => false def quickLt (n₁ n₂ : Name) : Bool := if n₁.hash < n₂.hash then true @@ -153,12 +153,12 @@ instance : HasToString Name := ⟨Name.toString⟩ def appendAfter : Name → String → Name -| mkString p s, suffix => mkString p (s ++ suffix) -| n, suffix => mkString n suffix +| mkString p s, suffix => mkString p (s ++ suffix) +| n, suffix => mkString n suffix def appendIndexAfter : Name → Nat → Name -| mkString p s, idx => mkString p (s ++ "_" ++ toString idx) -| n, idx => mkString n ("_" ++ toString idx) +| mkString p s, idx => mkString p (s ++ "_" ++ toString idx) +| n, idx => mkString n ("_" ++ toString idx) /- The frontend does not allow user declarations to start with `_` in any of its parts. We use name parts starting with `_` internally to create auxiliary names (e.g., `_private`). -/ diff --git a/library/init/lean/parser/parser.lean b/library/init/lean/parser/parser.lean index 36276d54f5..54696f51b1 100644 --- a/library/init/lean/parser/parser.lean +++ b/library/init/lean/parser/parser.lean @@ -216,19 +216,19 @@ inductive FirstTokens namespace FirstTokens def merge : FirstTokens → FirstTokens → FirstTokens -| epsilon, tks => tks -| tks, epsilon => tks -| tokens s₁, tokens s₂ => tokens (s₁ ++ s₂) -| optTokens s₁, optTokens s₂ => optTokens (s₁ ++ s₂) -| tokens s₁, optTokens s₂ => tokens (s₁ ++ s₂) -| optTokens s₁, tokens s₂ => tokens (s₁ ++ s₂) -| _, _ => unknown +| epsilon, tks => tks +| tks, epsilon => tks +| tokens s₁, tokens s₂ => tokens (s₁ ++ s₂) +| optTokens s₁, optTokens s₂ => optTokens (s₁ ++ s₂) +| tokens s₁, optTokens s₂ => tokens (s₁ ++ s₂) +| optTokens s₁, tokens s₂ => tokens (s₁ ++ s₂) +| _, _ => unknown def seq : FirstTokens → FirstTokens → FirstTokens -| epsilon, tks => tks -| optTokens s₁, optTokens s₂ => optTokens (s₁ ++ s₂) -| optTokens s₁, tokens s₂ => tokens (s₁ ++ s₂) -| tks, _ => tks +| epsilon, tks => tks +| optTokens s₁, optTokens s₂ => optTokens (s₁ ++ s₂) +| optTokens s₁, tokens s₂ => tokens (s₁ ++ s₂) +| tks, _ => tks def toOptional : FirstTokens → FirstTokens | tokens tks => optTokens tks @@ -1205,9 +1205,9 @@ def longestMatchFn {k : ParserKind} : List (Parser k) → ParserFn k longestMatchFnAux startSize startPos ps a c s def anyOfFn {k : ParserKind} : List (Parser k) → ParserFn k -| [], _, _, s => s.mkError "anyOf: empty list" -| [p], a, c, s => p.fn a c s -| p::ps, a, c, s => orelseFn p.fn (anyOfFn ps) a c s +| [], _, _, s => s.mkError "anyOf: empty list" +| [p], a, c, s => p.fn a c s +| p::ps, a, c, s => orelseFn p.fn (anyOfFn ps) a c s @[inline] def checkColGeFn (col : Nat) (errorMsg : String) : BasicParserFn := fun c s => diff --git a/library/init/lean/parser/trie.lean b/library/init/lean/parser/trie.lean index ce527f1ed4..07ddf22d51 100644 --- a/library/init/lean/parser/trie.lean +++ b/library/init/lean/parser/trie.lean @@ -36,7 +36,7 @@ private partial def insertEmptyAux (s : String) (val : α) : String.Pos → Trie Trie.Node none (RBNode.singleton c t) private partial def insertAux (s : String) (val : α) : Trie α → String.Pos → Trie α -| Trie.Node v m, i => +| Trie.Node v m, i => match s.atEnd i with | true => Trie.Node (some val) m -- overrides old value | false => @@ -51,7 +51,7 @@ def insert (t : Trie α) (s : String) (val : α) : Trie α := insertAux s val t 0 private partial def findAux (s : String) : Trie α → String.Pos → Option α -| Trie.Node val m, i => +| Trie.Node val m, i => match s.atEnd i with | true => val | false => @@ -70,7 +70,7 @@ match v, acc with | none, acc => acc private partial def matchPrefixAux (s : String) : Trie α → String.Pos → (String.Pos × Option α) → String.Pos × Option α -| Trie.Node v m, i, acc => +| Trie.Node v m, i, acc => match s.atEnd i with | true => updtAcc v i acc | false => diff --git a/library/init/lean/syntax.lean b/library/init/lean/syntax.lean index b706ef406a..27b4ac0c03 100644 --- a/library/init/lean/syntax.lean +++ b/library/init/lean/syntax.lean @@ -109,8 +109,8 @@ end SyntaxNode namespace Syntax def setAtomVal {α} : Syntax α → String → Syntax α -| atom info _, v => (atom info v) -| stx, _ => stx +| atom info _, v => (atom info v) +| stx, _ => stx @[inline] def ifNode {α β} (stx : Syntax α) (hyes : SyntaxNode α → β) (hno : Unit → β) : β := match stx with @@ -131,8 +131,8 @@ def getId {α} : Syntax α → Name | _ => Name.anonymous def isOfKind {α} : Syntax α → SyntaxNodeKind → Bool -| node kind _, k => k == kind -| _, _ => false +| node kind _, k => k == kind +| _, _ => false def asNode {α} : Syntax α → SyntaxNode α | Syntax.node kind args => ⟨Syntax.node kind args, IsNode.mk kind args⟩ @@ -277,8 +277,8 @@ match setTailInfoAux info stx with | none => stx private def reprintLeaf : Option SourceInfo → String → String -| none, val => val -| some info, val => info.leading.toString ++ val ++ info.trailing.toString +| none, val => val +| some info, val => info.leading.toString ++ val ++ info.trailing.toString partial def reprint {α} : Syntax α → Option String | atom info val => reprintLeaf info val diff --git a/tests/playground/patcheqnspace.lean b/tests/playground/patcheqnspace.lean new file mode 100644 index 0000000000..e860113cd2 --- /dev/null +++ b/tests/playground/patcheqnspace.lean @@ -0,0 +1,53 @@ +import init.lean.parser +import init.lean.parser.transform +open Lean +open Lean.Parser + +def getAtomTrailingSpace : Syntax → Nat +| Syntax.atom (some info) _ => info.trailing.stopPos - info.trailing.startPos +| _ => 0 + +def getMinTrailingSpace (ps : Array Syntax) (i : Nat) : Nat := +ps.foldl (fun acc (p : Syntax) => + let space := getAtomTrailingSpace (p.getArg i); + if space < acc then space else acc) + 100000 + +def reduceTrailingSpace : Syntax → Nat → Syntax +| Syntax.atom (some info) val, delta => Syntax.atom (some { trailing := { stopPos := info.trailing.stopPos - delta, .. info.trailing }, .. info }) val + +| stx, _ => stx + +partial def fixPats : Array Syntax → Nat → Nat → Array Syntax +| ps, i, sz => + if i < sz then + let minSpace := getMinTrailingSpace ps i; + if minSpace <= 1 then + fixPats ps (i+2) sz + else + let ps := ps.map $ fun p => p.modifyArg i $ fun comma => reduceTrailingSpace comma (minSpace - 1); + fixPats ps (i+2) sz + else + ps + +def fixEqnSyntax (stx : Syntax) : Syntax := +stx.rewriteBottomUp $ fun stx => + stx.ifNodeKind `Lean.Parser.Command.declValEqns + (fun stx => + stx.val.modifyArg 0 $ fun altsStx => + altsStx.modifyArgs $ fun alts => + let pats := alts.map $ fun alt => alt.getArg 1; + let patSize := (pats.get 0).getArgs.size; + let pats := fixPats pats 1 patSize; + alts.mapIdx $ fun i alt => alt.setArg 1 (pats.get i)) + (fun _ => stx) + +def main (xs : List String) : IO Unit := +do +[fname] ← pure xs | throw (IO.userError "usage `patch `"); +env ← mkEmptyEnvironment; +stx ← parseFile env fname; +let stx := fixEqnSyntax stx; +match stx.reprint with +| some out => IO.print out +| none => throw (IO.userError "failed to reprint")