diff --git a/library/init/control/combinators.lean b/library/init/control/combinators.lean index 27e983c6b3..664617e8e1 100644 --- a/library/init/control/combinators.lean +++ b/library/init/control/combinators.lean @@ -33,8 +33,8 @@ mcond c t (pure ()) namespace Nat @[specialize] def mforAux {m} [Applicative m] (f : Nat → m Unit) (n : Nat) : Nat → m Unit -| 0 => pure () -| i+1 => f (n-i-1) *> mforAux i +| 0 => pure () +| i+1 => f (n-i-1) *> mforAux i @[inline] def mfor {m} [Applicative m] (n : Nat) (f : Nat → m Unit) : m Unit := mforAux f n n @@ -59,18 +59,18 @@ namespace List @[specialize] def mmap {m : Type u → Type v} [Applicative m] {α : Type w} {β : Type u} (f : α → m β) : List α → m (List β) -| [] => pure [] -| a::as => List.cons <$> (f a) <*> mmap as +| [] => pure [] +| a::as => List.cons <$> (f a) <*> mmap as @[specialize] def mfor {m : Type u → Type v} [Applicative m] {α : Type w} {β : Type u} (f : α → m β) : List α → m PUnit -| [] => pure ⟨⟩ -| h :: t => f h *> mfor t +| [] => pure ⟨⟩ +| h :: t => f h *> mfor t @[specialize] def mfilter {m : Type → Type v} [Monad m] {α : Type} (f : α → m Bool) : List α → m (List α) -| [] => pure [] -| h :: t => do b ← f h; t' ← mfilter t; cond b (pure (h :: t')) (pure t') +| [] => pure [] +| h :: t => do b ← f h; t' ← mfilter t; cond b (pure (h :: t')) (pure t') @[specialize] def mfoldl {m : Type u → Type v} [Monad m] {s : Type u} {α : Type w} : (s → α → m s) → s → List α → m s @@ -88,20 +88,20 @@ def mfoldr {m : Type u → Type v} [Monad m] {s : Type u} {α : Type w} : (α @[specialize] def mfirst {m : Type u → Type v} [Monad m] [Alternative m] {α : Type w} {β : Type u} (f : α → m β) : List α → m β -| [] => failure -| a::as => f a <|> mfirst as +| [] => failure +| a::as => f a <|> mfirst as @[specialize] def mexists {m : Type → Type u} [Monad m] {α : Type v} (f : α → m Bool) : List α → m Bool -| [] => pure false -| a::as => do b ← f a; match b with +| [] => pure false +| a::as => do b ← f a; match b with | true => pure true | false => mexists as @[specialize] def mforall {m : Type → Type u} [Monad m] {α : Type v} (f : α → m Bool) : List α → m Bool -| [] => pure true -| a::as => do b ← f a; match b with +| [] => pure true +| a::as => do b ← f a; match b with | true => mforall as | false => pure false diff --git a/library/init/control/estate.lean b/library/init/control/estate.lean index e9ab233abe..3211becf04 100644 --- a/library/init/control/estate.lean +++ b/library/init/control/estate.lean @@ -34,12 +34,12 @@ abbrev resultOk (ε σ α : Type u) := {r : Result ε σ α // r.IsOk} ⟨Result.ok a s, Result.IsOk.mk a s⟩ protected def Result.toString [HasToString ε] [HasToString α] : Result ε σ α → String -| Result.ok a _ => "ok: " ++ toString a -| Result.error e _ => "error: " ++ toString e +| Result.ok a _ => "ok: " ++ toString a +| Result.error e _ => "error: " ++ toString e protected def Result.repr [HasRepr ε] [HasRepr α] : Result ε σ α → String -| Result.error e _ => "(error " ++ repr e ++ ")" -| Result.ok a _ => "(ok " ++ repr a ++ ")" +| Result.error e _ => "(error " ++ repr e ++ ")" +| Result.ok a _ => "(ok " ++ repr a ++ ")" instance [HasToString ε] [HasToString α] : HasToString (Result ε σ α) := ⟨Result.toString⟩ instance [HasRepr ε] [HasRepr α] : HasRepr (Result ε σ α) := ⟨Result.repr⟩ diff --git a/library/init/control/except.lean b/library/init/control/except.lean index d9ceec3bab..fd501c5a72 100644 --- a/library/init/control/except.lean +++ b/library/init/control/except.lean @@ -21,12 +21,12 @@ section variables {ε : Type u} {α : Type v} protected def Except.toString [HasToString ε] [HasToString α] : Except ε α → String -| Except.error e => "(error " ++ toString e ++ ")" -| Except.ok a => "(ok " ++ toString a ++ ")" +| Except.error e => "(error " ++ toString e ++ ")" +| Except.ok a => "(ok " ++ toString a ++ ")" protected def Except.repr [HasRepr ε] [HasRepr α] : Except ε α → String -| Except.error e => "(error " ++ repr e ++ ")" -| Except.ok a => "(ok " ++ repr a ++ ")" +| Except.error e => "(error " ++ repr e ++ ")" +| Except.ok a => "(ok " ++ repr a ++ ")" instance [HasToString ε] [HasToString α] : HasToString (Except ε α) := ⟨Except.toString⟩ @@ -42,12 +42,12 @@ variables {ε : Type u} Except.ok a @[inline] protected def map {α β : Type v} (f : α → β) : Except ε α → Except ε β -| Except.error err => Except.error err -| Except.ok v => Except.ok $ f v +| Except.error err => Except.error err +| Except.ok v => Except.ok $ f v @[inline] protected def mapError {ε' : Type u} {α : Type v} (f : ε → ε') : Except ε α → Except ε' α -| Except.error err => Except.error $ f err -| Except.ok v => Except.ok v +| Except.error err => Except.error $ f err +| Except.ok v => Except.ok v @[inline] protected def bind {α β : Type v} (ma : Except ε α) (f : α → Except ε β) : Except ε β := match ma with @@ -55,12 +55,12 @@ match ma with | (Except.ok v) => f v @[inline] protected def toBool {α : Type v} : Except ε α → Bool -| Except.ok _ => true -| Except.error _ => false +| Except.ok _ => true +| Except.error _ => false @[inline] protected def toOption {α : Type v} : Except ε α → Option α -| Except.ok a => some a -| Except.error _ => none +| Except.ok a => some a +| Except.error _ => none @[inline] protected def catch {α : Type u} (ma : Except ε α) (handle : ε → Except ε α) : Except ε α := match ma with @@ -87,8 +87,8 @@ variables {ε : Type u} {m : Type u → Type v} [Monad m] ExceptT.mk $ pure (Except.ok a) @[inline] protected def bindCont {α β : Type u} (f : α → ExceptT ε m β) : Except ε α → m (Except ε β) -| Except.ok a => f a -| Except.error e => pure (Except.error e) +| Except.ok a => f a +| Except.error e => pure (Except.error e) @[inline] protected def bind {α β : Type u} (ma : ExceptT ε m α) (f : α → ExceptT ε m β) : ExceptT ε m β := ExceptT.mk $ ma >>= ExceptT.bindCont f @@ -139,8 +139,8 @@ catch t₁ $ fun _ => t₂ catch t₁ $ fun e₁ => catch t₂ $ fun e₂ => throw (if useFirstEx then e₁ else e₂) @[inline] def liftExcept {ε' : Type u} [MonadExcept ε m] [HasLiftT ε' ε] [Monad m] {α : Type v} : Except ε' α → m α -| Except.error e => throw (coe e) -| Except.ok a => pure a +| Except.error e => throw (coe e) +| Except.ok a => pure a end MonadExcept export MonadExcept (throw catch) diff --git a/library/init/control/option.lean b/library/init/control/option.lean index 6e5b4c414d..3ae9419dfe 100644 --- a/library/init/control/option.lean +++ b/library/init/control/option.lean @@ -18,8 +18,8 @@ namespace OptionT variables {m : Type u → Type v} [Monad m] {α β : Type u} @[inline] protected def bindCont {α β : Type u} (f : α → OptionT m β) : Option α → m (Option β) - | some a => f a - | none => pure none + | some a => f a + | none => pure none @[inline] protected def bind (ma : OptionT m α) (f : α → OptionT m β) : OptionT m β := (ma >>= OptionT.bindCont f : m (Option β)) diff --git a/library/init/core.lean b/library/init/core.lean index 19357f5e1f..a7fc92014b 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. -/ @@ -474,15 +474,15 @@ instance (α : Type u) (β : Type v) [HasSizeof α] [HasSizeof β] : HasSizeof ( ⟨Prod.sizeof⟩ protected def Sum.sizeof {α : Type u} {β : Type v} [HasSizeof α] [HasSizeof β] : (Sum α β) → Nat -| Sum.inl a => 1 + sizeof a -| Sum.inr b => 1 + sizeof b +| Sum.inl a => 1 + sizeof a +| Sum.inr b => 1 + sizeof b instance (α : Type u) (β : Type v) [HasSizeof α] [HasSizeof β] : HasSizeof (Sum α β) := ⟨Sum.sizeof⟩ protected def PSum.sizeof {α : Type u} {β : Type v} [HasSizeof α] [HasSizeof β] : (PSum α β) → Nat -| PSum.inl a => 1 + sizeof a -| PSum.inr b => 1 + sizeof b +| PSum.inl a => 1 + sizeof a +| PSum.inr b => 1 + sizeof b instance (α : Type u) (β : Type v) [HasSizeof α] [HasSizeof β] : HasSizeof (PSum α β) := ⟨PSum.sizeof⟩ @@ -510,15 +510,15 @@ protected def Bool.sizeof : Bool → Nat instance : HasSizeof Bool := ⟨Bool.sizeof⟩ protected def Option.sizeof {α : Type u} [HasSizeof α] : Option α → Nat -| none => 1 -| some a => 1 + sizeof a +| none => 1 +| some a => 1 + sizeof a instance (α : Type u) [HasSizeof α] : HasSizeof (Option α) := ⟨Option.sizeof⟩ protected def List.sizeof {α : Type u} [HasSizeof α] : List α → Nat -| List.nil => 1 -| List.cons a l => 1 + sizeof a + List.sizeof l +| List.nil => 1 +| List.cons a l => 1 + sizeof a + List.sizeof l instance (α : Type u) [HasSizeof α] : HasSizeof (List α) := ⟨List.sizeof⟩ @@ -544,12 +544,12 @@ theorem optParamEq (α : Sort u) (default : α) : optParam α default = α := rf | false, x, y => y @[macroInline] def or : Bool → Bool → Bool -| true, _ => true -| false, b => b +| true, _ => true +| false, b => b @[macroInline] def and : Bool → Bool → Bool -| false, _ => false -| true, b => b +| false, _ => false +| true, b => b @[macroInline] def not : Bool → Bool | true => false @@ -988,7 +988,7 @@ up :: (down : α) namespace ULift /- Bijection between α and ULift.{v} α -/ theorem upDown {α : Type u} : ∀ (b : ULift.{v} α), up (down b) = b -| up a => rfl +| up a => rfl theorem downUp {α : Type u} (a : α) : down (up.{v} a) = a := rfl end ULift @@ -1000,7 +1000,7 @@ up :: (down : α) namespace PLift /- Bijection between α and PLift α -/ theorem upDown {α : Sort u} : ∀ (b : PLift α), up (down b) = b -| up a => rfl +| up a => rfl theorem downUp {α : Sort u} (a : α) : down (up a) = a := rfl end PLift diff --git a/library/init/data/array/basic.lean b/library/init/data/array/basic.lean index aa21ebe3dd..f3063d59bc 100644 --- a/library/init/data/array/basic.lean +++ b/library/init/data/array/basic.lean @@ -484,8 +484,8 @@ export Array (mkArray) | a::as, r => List.toArrayAux as (r.push a) @[inlineIfReduce] def List.redLength {α : Type u} : List α → Nat -| [] => 0 -| _::as => as.redLength + 1 +| [] => 0 +| _::as => as.redLength + 1 @[inline] def List.toArray {α : Type u} (as : List α) : Array α := as.toArrayAux (Array.mkEmpty as.redLength) diff --git a/library/init/data/assoclist.lean b/library/init/data/assoclist.lean index 954127636b..03f645386e 100644 --- a/library/init/data/assoclist.lean +++ b/library/init/data/assoclist.lean @@ -16,31 +16,31 @@ namespace AssocList variables {α : Type u} {β : Type v} {δ : Type w} {m : Type w → Type w} [Monad m] @[specialize] def mfoldl (f : δ → α → β → m δ) : δ → AssocList α β → m δ -| d, nil => pure d -| d, cons a b es => do d ← f d a b; mfoldl d es +| d, nil => pure d +| d, cons a b es => do d ← f d a b; mfoldl d es @[inline] def foldl (f : δ → α → β → δ) (d : δ) (as : AssocList α β) : δ := Id.run (mfoldl f d as) def find [HasBeq α] (a : α) : AssocList α β → Option β -| nil => none -| cons k v es => match k == a with +| nil => none +| cons k v es => match k == a with | true => some v | false => find es def contains [HasBeq α] (a : α) : AssocList α β → Bool -| nil => false -| cons k v es => k == a || contains es +| nil => false +| cons k v es => k == a || contains es def replace [HasBeq α] (a : α) (b : β) : AssocList α β → AssocList α β -| nil => nil -| cons k v es => match k == a with +| nil => nil +| cons k v es => match k == a with | true => cons a b es | false => cons k v (replace es) def erase [HasBeq α] (a : α) : AssocList α β → AssocList α β -| nil => nil -| cons k v es => match k == a with +| nil => nil +| cons k v es => match k == a with | true => es | false => cons k v (erase es) diff --git a/library/init/data/binomialheap/basic.lean b/library/init/data/binomialheap/basic.lean index 078595c45f..d61046142d 100644 --- a/library/init/data/binomialheap/basic.lean +++ b/library/init/data/binomialheap/basic.lean @@ -23,8 +23,8 @@ variables {α : Type u} instance : Inhabited (Heap α) := ⟨Heap.empty⟩ def hRank : List (HeapNode α) → Nat -| [] => 0 -| h::_ => h.rank +| [] => 0 +| h::_ => h.rank def isEmpty : Heap α → Bool | Heap.empty => true @@ -54,42 +54,42 @@ 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 -| Heap.heap h => h.foldl +| Heap.empty => none +| Heap.heap h => h.foldl (fun r n => match r with | none => n.val | some v => if lt v n.val then v else n.val) none /- O(log n) -/ @[specialize] def head [Inhabited α] (lt : α → α → Bool) : Heap α → α -| Heap.empty => default α -| Heap.heap [] => default α -| Heap.heap (h::hs) => hs.foldl (fun r n => if lt r n.val then r else n.val) h.val +| Heap.empty => default α +| Heap.heap [] => default α +| 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') def tail (lt : α → α → Bool) : Heap α → Heap α -| Heap.empty => Heap.empty -| Heap.heap [] => Heap.empty -| Heap.heap [h] => +| Heap.empty => Heap.empty +| Heap.heap [] => Heap.empty +| Heap.heap [h] => match h.children with | [] => Heap.empty | (h::hs) => hs.foldl (merge lt) h -| Heap.heap hhs@(h::hs) => +| Heap.heap hhs@(h::hs) => let (min, minIdx) := findMin lt hs 1 (h, 0); let rest := hhs.eraseIdx minIdx; min.children.foldl (merge lt) (Heap.heap rest) partial def toList (lt : α → α → Bool) : Heap α → List α -| Heap.empty => [] -| h => match headOpt lt h with +| Heap.empty => [] +| h => match headOpt lt h with | none => [] | some a => a :: toList (tail lt h) diff --git a/library/init/data/int/basic.lean b/library/init/data/int/basic.lean index 24b2b8e0ad..420e4b550b 100644 --- a/library/init/data/int/basic.lean +++ b/library/init/data/int/basic.lean @@ -28,8 +28,8 @@ instance : HasZero Int := ⟨Int.zero⟩ instance : HasOne Int := ⟨Int.one⟩ def negOfNat : Nat → Int -| 0 => 0 -| succ m => negSucc m +| 0 => 0 +| succ m => negSucc m @[extern cpp "lean::int_neg"] protected def neg (n : @& Int) : Int := @@ -115,8 +115,8 @@ match m with | negSucc m => m.succ protected def repr : Int → String -| ofNat m => Nat.repr m -| negSucc m => "-" ++ Nat.repr (succ m) +| ofNat m => Nat.repr m +| negSucc m => "-" ++ Nat.repr (succ m) instance : HasRepr Int := ⟨Int.repr⟩ @@ -126,24 +126,24 @@ 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⟩ def toNat : Int → Nat -| ofNat n => n -| negSucc n => 0 +| ofNat n => n +| negSucc n => 0 def natMod (m n : Int) : Nat := (m % n).toNat diff --git a/library/init/data/list/basic.lean b/library/init/data/list/basic.lean index 2352767076..429b5e4127 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 @@ -87,9 +87,9 @@ protected def erase {α} [HasBeq α] : List α → α → List α | 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 @@ -99,18 +99,18 @@ def length (as : List α) : Nat := lengthAux as 0 def isEmpty : List α → Bool -| [] => true -| _ :: _ => false +| [] => true +| _ :: _ => 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 @@ -118,29 +118,29 @@ def set : List α → Nat → α → List α | [], _, _ => [] def head [Inhabited α] : List α → α -| [] => default α -| a::_ => a +| [] => default α +| a::_ => a def tail : List α → List α -| [] => [] -| a::as => as +| [] => [] +| a::as => as @[specialize] def map (f : α → β) : List α → List β -| [] => [] -| a::as => f a :: map as +| [] => [] +| 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 α -| [] => [] -| a :: as => a ++ join as +| [] => [] +| a :: as => a ++ join as @[specialize] def filterMap (f : α → Option β) : List α → List β -| [] => [] -| a::as => +| [] => [] +| a::as => match f a with | none => filterMap as | some b => b :: filterMap as @@ -165,20 +165,20 @@ filterAux p as [] partitionAux p as ([], []) def dropWhile (p : α → Bool) : List α → List α -| [] => [] -| a::l => match p a with +| [] => [] +| a::l => match p a with | true => dropWhile l | false => a::l def find (p : α → Bool) : List α → Option α -| [] => none -| a::as => match p a with +| [] => none +| a::as => match p a with | true => some a | false => find as def elem [HasBeq α] (a : α) : List α → Bool -| [] => false -| b::bs => match a == b with +| [] => false +| b::bs => match a == b with | true => true | false => elem bs @@ -204,8 +204,8 @@ eraseDupsAux as [] spanAux p as [] def lookup [HasBeq α] : α → List (α × β) → Option β -| _, [] => none -| a, (k,b)::es => match a == k with +| _, [] => none +| a, (k,b)::es => match a == k with | true => some b | false => lookup a es @@ -213,22 +213,22 @@ 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 -| a, b :: l => foldl (f a b) l +| a, [] => a +| a, b :: l => foldl (f a b) l @[specialize] def foldr (f : α → β → β) (b : β) : List α → β -| [] => b -| a :: l => f a (foldr l) +| [] => b +| a :: l => f a (foldr l) @[specialize] def foldr1 (f : α → α → α) : ∀ (xs : List α), xs ≠ [] → α | [], h => absurd rfl h @@ -236,8 +236,8 @@ def take : Nat → List α → List α | a :: as@(_::_), _ => f a (foldr1 as (fun h => List.noConfusion h)) @[specialize] def foldr1Opt (f : α → α → α) : List α → Option α -| [] => none -| a :: as => some $ foldr1 f (a :: as) (fun h => List.noConfusion h) +| [] => none +| a :: as => some $ foldr1 f (a :: as) (fun h => List.noConfusion h) @[inline] def any (l : List α) (p : α → Bool) : Bool := foldr (fun a r => p a || r) false l @@ -250,15 +250,15 @@ 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 def unzip : List (α × β) → List α × List β -| [] => ([], []) -| (a, b) :: t => match unzip t with | (al, bl) => (a::al, b::bl) +| [] => ([], []) +| (a, b) :: t => match unzip t with | (al, bl) => (a::al, b::bl) def replicate (n : Nat) (a : α) : List α := n.repeat (fun xs => a :: xs) [] @@ -286,18 +286,18 @@ def getLastOfNonNil : ∀ (as : List α), as ≠ [] → α | a::b::as, h => getLastOfNonNil (b::as) (fun h => List.noConfusion h) def getLast [Inhabited α] : List α → α -| [] => arbitrary α -| a::as => getLastOfNonNil (a::as) (fun h => List.noConfusion h) +| [] => arbitrary α +| a::as => getLastOfNonNil (a::as) (fun h => List.noConfusion h) def init : List α → List α -| [] => [] -| [a] => [] -| a::l => a::init l +| [] => [] +| [a] => [] +| a::l => a::init l def intersperse (sep : α) : List α → List α -| [] => [] -| [x] => [x] -| x::xs => x::sep::intersperse xs +| [] => [] +| [x] => [x] +| x::xs => x::sep::intersperse xs def intercalate (sep : List α) (xs : List (List α)) : List α := join (intersperse sep xs) @@ -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,9 +346,9 @@ 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 := diff --git a/library/init/data/nat/basic.lean b/library/init/data/nat/basic.lean index aff4f1fedc..8fe433ddef 100644 --- a/library/init/data/nat/basic.lean +++ b/library/init/data/nat/basic.lean @@ -11,10 +11,10 @@ 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 @@ -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 @@ -63,18 +63,18 @@ instance : HasLess Nat := @[extern cpp inline "lean::nat_sub(#1, lean::box(1))"] def pred : Nat → Nat -| 0 => 0 -| a+1 => a +| 0 => 0 +| a+1 => a @[extern cpp "lean::nat_sub"] protected def sub : (@& Nat) → (@& Nat) → Nat -| a, 0 => a -| a, b+1 => pred (sub a b) +| a, 0 => a +| a, b+1 => pred (sub a b) @[extern cpp "lean::nat_mul"] protected def mul : (@& Nat) → (@& Nat) → Nat -| a, 0 => 0 -| a, b+1 => (mul a b) + a +| a, 0 => 0 +| a, b+1 => (mul a b) + a instance : HasSub Nat := ⟨Nat.sub⟩ @@ -90,8 +90,8 @@ instance : HasMul Nat := foldAux f n n a @[specialize] def anyAux (f : Nat → Bool) (s : Nat) : Nat → Bool -| 0 => false -| succ n => f (s - (succ n)) || anyAux n +| 0 => false +| succ n => f (s - (succ n)) || anyAux n /- `any f n = true` iff there is `i in [0, n-1]` s.t. `f i = true` -/ @[inline] def any (f : Nat → Bool) (n : Nat) : Bool := @@ -108,8 +108,8 @@ anyAux f n n repeatAux f n a protected def pow (m : Nat) : Nat → Nat -| 0 => 1 -| succ n => pow n * m +| 0 => 1 +| succ n => pow n * m instance : HasPow Nat Nat := ⟨Nat.pow⟩ @@ -117,12 +117,12 @@ instance : HasPow Nat Nat := /- Nat.add theorems -/ protected theorem zeroAdd : ∀ (n : Nat), 0 + n = n -| 0 => rfl -| n+1 => congrArg succ (zeroAdd n) +| 0 => rfl +| n+1 => congrArg succ (zeroAdd n) theorem succAdd : ∀ (n m : Nat), (succ n) + m = succ (n + m) -| n, 0 => rfl -| n, m+1 => congrArg succ (succAdd n m) +| n, 0 => rfl +| n, m+1 => congrArg succ (succAdd n m) theorem addSucc (n m : Nat) : n + succ m = succ (n + m) := rfl @@ -137,14 +137,14 @@ theorem succEqAddOne (n : Nat) : succ n = n + 1 := rfl protected theorem addComm : ∀ (n m : Nat), n + m = m + n -| n, 0 => Eq.symm (Nat.zeroAdd n) -| n, m+1 => +| n, 0 => Eq.symm (Nat.zeroAdd n) +| n, m+1 => suffices succ (n + m) = succ (m + n) from Eq.symm (succAdd m n) ▸ this; congrArg succ (addComm n m) protected theorem addAssoc : ∀ (n m k : Nat), (n + m) + k = n + (m + k) -| n, m, 0 => rfl -| n, m, succ k => congrArg succ (addAssoc n m k) +| n, m, 0 => rfl +| n, m, succ k => congrArg succ (addAssoc n m k) protected theorem addLeftComm : ∀ (n m k : Nat), n + (m + k) = m + (n + k) := leftComm Nat.add Nat.addComm Nat.addAssoc @@ -173,19 +173,19 @@ theorem mulSucc (n m : Nat) : n * succ m = n * m + n := rfl protected theorem zeroMul : ∀ (n : Nat), 0 * n = 0 -| 0 => rfl -| succ n => (mulSucc 0 n).symm ▸ (zeroMul n).symm ▸ rfl +| 0 => rfl +| succ n => (mulSucc 0 n).symm ▸ (zeroMul n).symm ▸ rfl theorem succMul : ∀ (n m : Nat), (succ n) * m = (n * m) + m -| n, 0 => rfl -| n, succ m => +| n, 0 => rfl +| n, succ m => have succ (n * m + m + n) = succ (n * m + n + m) from congrArg succ (Nat.addRightComm _ _ _); (mulSucc n m).symm ▸ (mulSucc (succ n) m).symm ▸ (succMul n m).symm ▸ this protected theorem mulComm : ∀ (n m : Nat), n * m = m * n -| n, 0 => (Nat.zeroMul n).symm ▸ (Nat.mulZero n).symm ▸ rfl -| n, succ m => (mulSucc n m).symm ▸ (succMul m n).symm ▸ (mulComm n m).symm ▸ rfl +| n, 0 => (Nat.zeroMul n).symm ▸ (Nat.mulZero n).symm ▸ rfl +| n, succ m => (mulSucc n m).symm ▸ (succMul m n).symm ▸ (mulComm n m).symm ▸ rfl protected theorem mulOne : ∀ (n : Nat), n * 1 = n := Nat.zeroAdd @@ -213,8 +213,8 @@ have h₄ : n * k + k * m = n * k + m * k from Nat.mulComm m k ▸ rfl; ((h₁.trans h₂).trans h₃).trans h₄ protected theorem mulAssoc : ∀ (n m k : Nat), (n * m) * k = n * (m * k) -| n, m, 0 => rfl -| n, m, succ k => +| n, m, 0 => rfl +| n, m, succ k => have h₁ : n * m * succ k = n * m * (k + 1) from rfl; have h₂ : n * m * (k + 1) = (n * m * k) + n * m * 1 from Nat.leftDistrib _ _ _; have h₃ : (n * m * k) + n * m * 1 = (n * m * k) + n * m from (Nat.mulOne (n*m)).symm ▸ rfl; @@ -226,12 +226,12 @@ protected theorem mulAssoc : ∀ (n m k : Nat), (n * m) * k = n * (m * k) /- Inequalities -/ protected def leRefl : ∀ (n : Nat), n ≤ n -| zero => rfl -| succ n => leRefl n +| zero => rfl +| succ n => leRefl n theorem leSucc : ∀ (n : Nat), n ≤ succ n -| zero => rfl -| succ n => leSucc n +| zero => rfl +| succ n => leSucc n theorem succLeSucc {n m : Nat} (h : n ≤ m) : succ n ≤ succ m := h @@ -249,8 +249,8 @@ theorem leStep : ∀ {n m : Nat}, n ≤ m → n ≤ succ m succLeSucc this theorem zeroLe : ∀ (n : Nat), 0 ≤ n -| zero => rfl -| succ n => rfl +| zero => rfl +| succ n => rfl theorem zeroLtSucc (n : Nat) : 0 < succ n := succLeSucc (zeroLe n) @@ -320,8 +320,8 @@ protected theorem leTrans : ∀ {n m k : Nat}, n ≤ m → m ≤ k → n ≤ k succLeSucc this theorem predLe : ∀ (n : Nat), pred n ≤ n -| zero => rfl -| succ n => leSucc _ +| zero => rfl +| succ n => leSucc _ theorem predLt : ∀ {n : Nat}, n ≠ 0 → pred n < n | zero, h => absurd rfl h @@ -356,8 +356,8 @@ leOfSuccLe h def lt.step {n m : Nat} : n < m → n < succ m := leStep theorem eqZeroOrPos : ∀ (n : Nat), n = 0 ∨ n > 0 -| 0 => Or.inl rfl -| n+1 => Or.inr (succPos _) +| 0 => Or.inl rfl +| n+1 => Or.inr (succPos _) protected theorem ltTrans {n m k : Nat} (h₁ : n < m) : m < k → n < k := Nat.leTrans (leStep h₁) @@ -380,8 +380,8 @@ protected theorem leAntisymm : ∀ {n m : Nat}, n ≤ m → m ≤ n → n = m congrArg succ this protected theorem ltOrGe : ∀ (n m : Nat), n < m ∨ n ≥ m -| n, 0 => Or.inr (zeroLe n) -| n, m+1 => +| n, 0 => Or.inr (zeroLe n) +| n, m+1 => match ltOrGe n m with | Or.inl h => Or.inl (leSuccOfLe h) | Or.inr h => @@ -421,8 +421,8 @@ Decidable.byCases Or.inl (leOfSuccLeSucc this)) theorem leAddRight : ∀ (n k : Nat), n ≤ n + k -| n, 0 => Nat.leRefl n -| n, k+1 => leSuccOfLe (leAddRight n k) +| n, 0 => Nat.leRefl n +| n, k+1 => leSuccOfLe (leAddRight n k) theorem leAddLeft (n m : Nat): n ≤ m + n := Nat.addComm n m ▸ leAddRight n m @@ -672,8 +672,8 @@ rfl theorem powZero (n : Nat) : n^0 = 1 := rfl theorem powLePowOfLeLeft {n m : Nat} (h : n ≤ m) : ∀ (i : Nat), n^i ≤ m^i -| 0 => Nat.leRefl _ -| succ i => Nat.mulLeMul (powLePowOfLeLeft i) h +| 0 => Nat.leRefl _ +| 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 => diff --git a/library/init/data/option/basic.lean b/library/init/data/option/basic.lean index c0bed31371..2d9a5436e5 100644 --- a/library/init/data/option/basic.lean +++ b/library/init/data/option/basic.lean @@ -20,20 +20,20 @@ def toMonad {m : Type → Type} [Monad m] [Alternative m] {A} : Option A → m A | none, e => e @[inline] def get {α : Type u} [Inhabited α] : Option α → α -| some x => x -| none => default α +| some x => x +| none => default α @[inline] def toBool {α : Type u} : Option α → Bool -| some _ => true -| none => false +| some _ => true +| none => false @[inline] def isSome {α : Type u} : Option α → Bool -| some _ => true -| none => false +| some _ => true +| none => false @[inline] def isNone {α : Type u} : Option α → Bool -| some _ => false -| none => true +| some _ => false +| none => true @[inline] protected def bind {α : Type u} {β : Type v} : Option α → (α → Option β) → Option β | none, b => none @@ -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]`. -/ @@ -60,15 +60,15 @@ instance : Alternative Option := ..Option.Monad } @[inline] protected def lt {α : Type u} (r : α → α → Prop) : Option α → Option α → Prop -| none, some x => True -| some x, some y => r x y -| _, _ => False +| none, some x => True +| some x, some y => r x y +| _, _ => 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/persistentarray/basic.lean b/library/init/data/persistentarray/basic.lean index f920b94942..1c3cc97199 100644 --- a/library/init/data/persistentarray/basic.lean +++ b/library/init/data/persistentarray/basic.lean @@ -186,8 +186,8 @@ variable {β : Type v} do b ← mfoldlAux f t.root b; t.tail.mfoldl f b @[specialize] partial def mfindAux (f : α → m (Option β)) : PersistentArrayNode α → m (Option β) -| node cs => cs.mfind (fun c => mfindAux c) -| leaf vs => vs.mfind f +| node cs => cs.mfind (fun c => mfindAux c) +| leaf vs => vs.mfind f @[specialize] def mfind (t : PersistentArray α) (f : α → m (Option β)) : m (Option β) := do b ← mfindAux f t.root; @@ -196,8 +196,8 @@ do b ← mfindAux f t.root; | some b => pure (some b) @[specialize] partial def mfindRevAux (f : α → m (Option β)) : PersistentArrayNode α → m (Option β) -| node cs => cs.mfindRev (fun c => mfindRevAux c) -| leaf vs => vs.mfindRev f +| node cs => cs.mfindRev (fun c => mfindRevAux c) +| leaf vs => vs.mfindRev f @[specialize] def mfindRev (t : PersistentArray α) (f : α → m (Option β)) : m (Option β) := do b ← t.tail.mfindRev f; @@ -220,8 +220,8 @@ else do t.tail.mfoldl f b @[specialize] partial def mforAux (f : α → m β) : PersistentArrayNode α → m PUnit -| node cs => cs.mfor (fun c => mforAux c) -| leaf vs => vs.mfor f +| node cs => cs.mfor (fun c => mforAux c) +| leaf vs => vs.mfor f @[specialize] def mfor (t : PersistentArray α) (f : α → m β) : m PUnit := mforAux f t.root *> t.tail.mfor f @@ -248,8 +248,8 @@ variables {m : Type u → Type v} [Monad m] variable {β : Type u} @[specialize] partial def mmapAux (f : α → m β) : PersistentArrayNode α → m (PersistentArrayNode β) -| node cs => node <$> cs.mmap (fun c => mmapAux c) -| leaf vs => leaf <$> vs.mmap f +| node cs => node <$> cs.mmap (fun c => mmapAux c) +| leaf vs => leaf <$> vs.mmap f @[specialize] def mmap (f : α → m β) (t : PersistentArray α) : m (PersistentArray β) := do diff --git a/library/init/data/persistenthashmap/basic.lean b/library/init/data/persistenthashmap/basic.lean index 311b2a0ae2..4fabc7650e 100644 --- a/library/init/data/persistenthashmap/basic.lean +++ b/library/init/data/persistenthashmap/basic.lean @@ -166,8 +166,8 @@ partial def isUnaryEntries (a : Array (Entry α β (Node α β))) : Nat → Opti else acc def isUnaryNode : Node α β → Option (α × β) -| Node.entries entries => isUnaryEntries entries 0 none -| Node.collision keys vals heq => +| Node.entries entries => isUnaryEntries entries 0 none +| Node.collision keys vals heq => if h : 1 = keys.size then have 0 < keys.size from h ▸ (Nat.zeroLtSucc _); some (keys.fget ⟨0, this⟩, vals.fget ⟨0, heq ▸ this⟩) diff --git a/library/init/data/rbmap/basic.lean b/library/init/data/rbmap/basic.lean index 336e39878c..d00b54ceaa 100644 --- a/library/init/data/rbmap/basic.lean +++ b/library/init/data/rbmap/basic.lean @@ -21,41 +21,41 @@ variables {α : Type u} {β : α → Type v} {σ : Type w} open Rbcolor Nat def depth (f : Nat → Nat → Nat) : RBNode α β → Nat -| leaf => 0 -| node _ l _ _ r => succ (f (depth l) (depth r)) +| leaf => 0 +| node _ l _ _ r => succ (f (depth l) (depth r)) protected def min : RBNode α β → Option (Sigma (fun k => β k)) -| leaf => none -| node _ leaf k v _ => some ⟨k, v⟩ -| node _ l k v _ => min l +| leaf => none +| node _ leaf k v _ => some ⟨k, v⟩ +| node _ l k v _ => min l protected def max : RBNode α β → Option (Sigma (fun k => β k)) -| leaf => none -| node _ _ k v leaf => some ⟨k, v⟩ -| node _ _ k v r => max r +| leaf => none +| node _ _ k v leaf => some ⟨k, v⟩ +| node _ _ k v r => max r @[specialize] def fold (f : σ → ∀ (k : α), β k → σ) : σ → RBNode α β → σ -| b, leaf => b -| b, node _ l k v r => fold (f (fold b l) k v) r +| b, leaf => b +| b, node _ l k v r => fold (f (fold b l) k v) r @[specialize] def mfold {m : Type w → Type w'} [Monad m] (f : σ → ∀ (k : α), β k → m σ) : σ → RBNode α β → m σ -| b, leaf => pure b -| b, node _ l k v r => do +| b, leaf => pure b +| b, node _ l k v r => do b ← mfold b l; b ← f b k v; mfold b r @[specialize] def revFold (f : σ → ∀ (k : α), β k → σ) : σ → RBNode α β → σ -| b, leaf => b -| b, node _ l k v r => revFold (f (revFold b r) k v) l +| b, leaf => b +| b, node _ l k v r => revFold (f (revFold b r) k v) l @[specialize] def all (p : ∀ k, β k → Bool) : RBNode α β → Bool -| leaf => true -| node _ l k v r => p k v && all l && all r +| leaf => true +| node _ l k v r => p k v && all l && all r @[specialize] def any (p : ∀ k, β k → Bool) : RBNode α β → Bool -| leaf => false -| node _ l k v r => p k v || any l || any r +| leaf => false +| node _ l k v r => p k v || any l || any r def singleton (k : α) (v : β k) : RBNode α β := node red leaf k v leaf @@ -67,18 +67,18 @@ node red leaf k v leaf | _, _, _, _ => leaf -- unreachable @[inline] def balance2 : RBNode α β → ∀ a, β a → RBNode α β → RBNode α β -| t, kv, vv, node _ (node red l kx₁ vx₁ r₁) ky vy r₂ => node red (node black t kv vv l) kx₁ vx₁ (node black r₁ ky vy r₂) -| t, kv, vv, node _ l₁ ky vy (node red l₂ kx₂ vx₂ r₂) => node red (node black t kv vv l₁) ky vy (node black l₂ kx₂ vx₂ r₂) -| t, kv, vv, node _ l ky vy r => node black t kv vv (node red l ky vy r) -| _, _, _, _ => leaf -- unreachable +| t, kv, vv, node _ (node red l kx₁ vx₁ r₁) ky vy r₂ => node red (node black t kv vv l) kx₁ vx₁ (node black r₁ ky vy r₂) +| t, kv, vv, node _ l₁ ky vy (node red l₂ kx₂ vx₂ r₂) => node red (node black t kv vv l₁) ky vy (node black l₂ kx₂ vx₂ r₂) +| t, kv, vv, node _ l ky vy r => node black t kv vv (node red l ky vy r) +| _, _, _, _ => leaf -- unreachable def isRed : RBNode α β → Bool -| node red _ _ _ _ => true -| _ => false +| node red _ _ _ _ => true +| _ => false def isBlack : RBNode α β → Bool -| node black _ _ _ _ => true -| _ => false +| node black _ _ _ _ => true +| _ => false section Insert @@ -101,8 +101,8 @@ variables (lt : α → α → Bool) node black a kx vx b def setBlack : RBNode α β → RBNode α β -| node _ l k v r => node black l k v r -| e => e +| node _ l k v r => node black l k v r +| e => e @[specialize] def insert (t : RBNode α β) (k : α) (v : β k) : RBNode α β := if isRed t then setBlack (ins lt t k v) @@ -118,14 +118,14 @@ def balance₃ : RBNode α β → ∀ k, β k → RBNode α β → RBNode α β | l, k, v, r => node black l k v r def setRed : RBNode α β → RBNode α β -| node _ a k v b => node red a k v b -| e => e +| node _ a k v b => node red a k v b +| e => e def balLeft : RBNode α β → ∀ k, β k → RBNode α β → RBNode α β -| node red a kx vx b, k, v, r => node red (node black a kx vx b) k v r -| l, k, v, node black a ky vy b => balance₃ l k v (node red a ky vy b) -| l, k, v, node red (node black a ky vy b) kz vz c => node red (node black l k v a) ky vy (balance₃ b kz vz (setRed c)) -| l, k, v, r => node red l k v r -- unreachable +| node red a kx vx b, k, v, r => node red (node black a kx vx b) k v r +| l, k, v, node black a ky vy b => balance₃ l k v (node red a ky vy b) +| l, k, v, node red (node black a ky vy b) kz vz c => node red (node black l k v a) ky vy (balance₃ b kz vz (setRed c)) +| l, k, v, r => node red l k v r -- unreachable def balRight (l : RBNode α β) (k : α) (v : β k) (r : RBNode α β) : RBNode α β := match r with @@ -155,8 +155,8 @@ section Erase variables (lt : α → α → Bool) @[specialize] def del (x : α) : RBNode α β → RBNode α β -| leaf => leaf -| node _ a y v b => +| leaf => leaf +| node _ a y v b => if lt x y then if a.isBlack then balLeft (del a) y v b else node red (del a) y v b @@ -267,8 +267,8 @@ instance [HasRepr α] [HasRepr β] : HasRepr (RBMap α β lt) := | ⟨t, w⟩, k => ⟨t.erase lt k, WellFormed.eraseWff w rfl⟩ @[specialize] def ofList : List (α × β) → RBMap α β lt -| [] => mkRBMap _ _ _ -| ⟨k,v⟩::xs => (ofList xs).insert k v +| [] => mkRBMap _ _ _ +| ⟨k,v⟩::xs => (ofList xs).insert k v @[inline] def findCore : RBMap α β lt → α → Option (Sigma (fun (k : α) => β)) | ⟨t, _⟩, x => t.findCore lt x diff --git a/library/init/data/rbtree/basic.lean b/library/init/data/rbtree/basic.lean index 889d3d9b4a..e0a4d657d5 100644 --- a/library/init/data/rbtree/basic.lean +++ b/library/init/data/rbtree/basic.lean @@ -63,8 +63,8 @@ RBMap.insert t a () RBMap.erase t a @[specialize] def ofList : List α → RBTree α lt -| [] => mkRBTree _ _ -| x::xs => (ofList xs).insert x +| [] => mkRBTree _ _ +| x::xs => (ofList xs).insert x @[inline] def find (t : RBTree α lt) (a : α) : Option α := match RBMap.findCore t a with diff --git a/library/init/data/repr.lean b/library/init/data/repr.lean index cf33f00f7f..2e76d01d9e 100644 --- a/library/init/data/repr.lean +++ b/library/init/data/repr.lean @@ -25,13 +25,13 @@ instance {p : Prop} : HasRepr (Decidable p) := ⟨fun b => @ite p b _ "true" "false"⟩ protected def List.reprAux {α : Type u} [HasRepr α] : Bool → List α → String -| b, [] => "" -| true, x::xs => repr x ++ List.reprAux false xs -| false, x::xs => ", " ++ repr x ++ List.reprAux false xs +| b, [] => "" +| true, x::xs => repr x ++ List.reprAux false xs +| false, x::xs => ", " ++ repr x ++ List.reprAux false xs protected def List.repr {α : Type u} [HasRepr α] : List α → String -| [] => "[]" -| x::xs => "[" ++ List.reprAux true (x::xs) ++ "]" +| [] => "[]" +| x::xs => "[" ++ List.reprAux true (x::xs) ++ "]" instance {α : Type u} [HasRepr α] : HasRepr (List α) := ⟨List.repr⟩ @@ -115,8 +115,8 @@ instance : HasRepr Char := ⟨fun c => "'" ++ Char.quoteCore c ++ "'"⟩ def String.quoteAux : List Char → String -| [] => "" -| x::xs => Char.quoteCore x ++ String.quoteAux xs +| [] => "" +| x::xs => Char.quoteCore x ++ String.quoteAux xs def String.quote (s : String) : String := if s.isEmpty = true then "\"\"" diff --git a/library/init/data/string/basic.lean b/library/init/data/string/basic.lean index 6bb894f718..42bd2bec23 100644 --- a/library/init/data/string/basic.lean +++ b/library/init/data/string/basic.lean @@ -41,7 +41,7 @@ List.hasDecidableLt s₁.data s₂.data @[extern cpp "lean::string_length"] def length : (@& String) → Nat -| ⟨s⟩ => s.length +| ⟨s⟩ => s.length /- The internal implementation uses dynamic arrays and will perform destructive updates if the String is not shared. -/ @@ -237,8 +237,8 @@ def extract : Iterator → Iterator → String else s₁.extract b e def forward : Iterator → Nat → Iterator -| it, 0 => it -| it, n+1 => forward it.next n +| it, 0 => it +| it, n+1 => forward it.next n def remainingToString : Iterator → String | ⟨s, i⟩ => s.extract i s.bsize @@ -249,12 +249,12 @@ def isPrefixOfRemaining : Iterator → Iterator → Bool | ⟨s₁, i₁⟩, ⟨s₂, i₂⟩ => s₁.extract i₁ s₁.bsize = s₂.extract i₂ (i₂ + (s₁.bsize - i₁)) def nextn : Iterator → Nat → Iterator -| it, 0 => it -| it, i+1 => nextn it.next i +| it, 0 => it +| it, i+1 => nextn it.next i def prevn : Iterator → Nat → Iterator -| it, 0 => it -| it, i+1 => prevn it.prev i +| it, 0 => it +| it, i+1 => prevn it.prev i end Iterator private partial def lineColumnAux (s : String) : Pos → Nat × Nat → Nat × Nat diff --git a/library/init/data/tostring.lean b/library/init/data/tostring.lean index 67a18c8550..14d8dd6db6 100644 --- a/library/init/data/tostring.lean +++ b/library/init/data/tostring.lean @@ -35,13 +35,13 @@ instance {p : Prop} : HasToString (Decidable p) := ⟨fun b => @ite p b _ "true" "false"⟩ protected def List.toStringAux {α : Type u} [HasToString α] : Bool → List α → String -| b, [] => "" -| true, x::xs => toString x ++ List.toStringAux false xs -| false, x::xs => ", " ++ toString x ++ List.toStringAux false xs +| b, [] => "" +| true, x::xs => toString x ++ List.toStringAux false xs +| false, x::xs => ", " ++ toString x ++ List.toStringAux false xs protected def List.toString {α : Type u} [HasToString α] : List α → String -| [] => "[]" -| x::xs => "[" ++ List.toStringAux true (x::xs) ++ "]" +| [] => "[]" +| x::xs => "[" ++ List.toStringAux true (x::xs) ++ "]" instance {α : Type u} [HasToString α] : HasToString (List α) := ⟨List.toString⟩ diff --git a/library/init/lean/class.lean b/library/init/lean/class.lean index ad591fa1f5..6a8db0a69f 100644 --- a/library/init/lean/class.lean +++ b/library/init/lean/class.lean @@ -15,8 +15,8 @@ inductive ClassEntry namespace ClassEntry @[inline] def getName : ClassEntry → Name -| «class» n _ => n -| «instance» n _ => n +| «class» n _ => n +| «instance» n _ => n def lt (a b : ClassEntry) : Bool := Name.quickLt a.getName b.getName @@ -84,8 +84,8 @@ private def isOutParam (e : Expr) : Bool := e.isAppOfArity `outParam 1 def Expr.hasOutParam : Expr → Bool -| Expr.pi _ _ d b => isOutParam d || Expr.hasOutParam b -| _ => false +| Expr.pi _ _ d b => isOutParam d || Expr.hasOutParam b +| _ => false def addClass (env : Environment) (clsName : Name) : Except String Environment := if isClass env clsName then Except.error ("class has already been declared '" ++ toString clsName ++ "'") @@ -94,13 +94,13 @@ 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 -| e => do +| Expr.pi _ _ _ d => getClassName d +| e => do Expr.const c _ ← pure e.getAppFn | none; info ← env.find c; match info.value with diff --git a/library/init/lean/compiler/constfolding.lean b/library/init/lean/compiler/constfolding.lean index 0533189d6c..b72cb9a5f2 100644 --- a/library/init/lean/compiler/constfolding.lean +++ b/library/init/lean/compiler/constfolding.lean @@ -37,8 +37,8 @@ def isToNat (fn : Name) : Bool := numScalarTypes.any (fun info => info.toNatFn = fn) def getInfoFromFn (fn : Name) : List NumScalarTypeInfo → Option NumScalarTypeInfo -| [] => none -| info::infos => +| [] => none +| info::infos => if info.ofNatFn = fn then some info else getInfoFromFn infos @@ -48,9 +48,9 @@ def getInfoFromVal : Expr → Option NumScalarTypeInfo @[export lean.get_num_lit_core] def getNumLit : Expr → Option Nat -| Expr.lit (Literal.natVal n) => some n -| Expr.app (Expr.const fn _) a => if isOfNat fn then getNumLit a else none -| _ => none +| Expr.lit (Literal.natVal n) => some n +| Expr.app (Expr.const fn _) a => if isOfNat fn then getNumLit a else none +| _ => none def mkUIntLit (info : NumScalarTypeInfo) (n : Nat) : Expr := Expr.app (Expr.const info.ofNatFn []) (Expr.lit (Literal.natVal (n%info.size))) @@ -126,9 +126,9 @@ def natFoldFns : List (Name × BinFoldFn) := (`Nat.decLe, foldNatDecLe)] def getBoolLit : Expr → Option Bool -| Expr.const `Bool.true _ => some true -| Expr.const `Bool.false _ => some false -| _ => none +| Expr.const `Bool.true _ => some true +| Expr.const `Bool.false _ => some false +| _ => none def foldStrictAnd (_ : Bool) (a₁ a₂ : Expr) : Option Expr := let v₁ := getBoolLit a₁; diff --git a/library/init/lean/compiler/externattr.lean b/library/init/lean/compiler/externattr.lean index a26e01e6a6..a21dcb9325 100644 --- a/library/init/lean/compiler/externattr.lean +++ b/library/init/lean/compiler/externattr.lean @@ -125,20 +125,20 @@ 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 -| ExternEntry.inline n _ => n -| ExternEntry.standard n _ => n -| ExternEntry.foreign n _ => n +| ExternEntry.adhoc n => n +| ExternEntry.inline n _ => n +| ExternEntry.standard n _ => n +| ExternEntry.foreign n _ => n def getExternEntryForAux (backend : Name) : List ExternEntry → Option ExternEntry -| [] => none -| e::es => +| [] => none +| e::es => if e.backend = `all then some e else if e.backend = backend then some e else getExternEntryForAux es diff --git a/library/init/lean/compiler/ir/basic.lean b/library/init/lean/compiler/ir/basic.lean index 96063ff16a..fd84881c55 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⟩ @@ -260,24 +260,24 @@ instance altInh : Inhabited Alt := ⟨Alt.default (default _)⟩ def FnBody.isTerminal : FnBody → Bool -| FnBody.case _ _ _ => true -| FnBody.ret _ => true -| FnBody.jmp _ _ => true -| FnBody.unreachable => true -| _ => false +| FnBody.case _ _ _ => true +| FnBody.ret _ => true +| FnBody.jmp _ _ => true +| FnBody.unreachable => true +| _ => false def FnBody.body : FnBody → FnBody -| FnBody.vdecl _ _ _ b => b -| FnBody.jdecl _ _ _ b => b -| FnBody.set _ _ _ b => b -| FnBody.uset _ _ _ b => b -| FnBody.sset _ _ _ _ _ b => b -| FnBody.setTag _ _ b => b -| FnBody.inc _ _ _ b => b -| FnBody.dec _ _ _ b => b -| FnBody.del _ b => b -| FnBody.mdata _ b => b -| other => other +| FnBody.vdecl _ _ _ b => b +| FnBody.jdecl _ _ _ b => b +| FnBody.set _ _ _ b => b +| FnBody.uset _ _ _ b => b +| FnBody.sset _ _ _ _ _ b => b +| FnBody.setTag _ _ b => b +| FnBody.inc _ _ _ b => b +| FnBody.dec _ _ _ b => b +| FnBody.del _ b => b +| FnBody.mdata _ b => b +| other => other def FnBody.setBody : FnBody → FnBody → FnBody | FnBody.vdecl x t v _, b => FnBody.vdecl x t v b @@ -303,24 +303,24 @@ let c := b.resetBody; (c, b') def AltCore.body : Alt → FnBody -| Alt.ctor _ b => b -| Alt.default b => b +| Alt.ctor _ b => b +| Alt.default b => b def AltCore.setBody : Alt → FnBody → Alt | 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) -| Alt.default b => Alt.default (f b) +| Alt.ctor c b => Alt.ctor c (f b) +| Alt.default b => Alt.default (f b) @[inline] def AltCore.mmodifyBody {m : Type → Type} [Monad m] (f : FnBody → m FnBody) : AltCore FnBody → m Alt -| Alt.ctor c b => Alt.ctor c <$> f b -| Alt.default b => Alt.default <$> f b +| Alt.ctor c b => Alt.ctor c <$> f b +| Alt.default b => Alt.default <$> f b def Alt.isDefault : Alt → Bool -| Alt.ctor _ _ => false -| Alt.default _ => true +| Alt.ctor _ _ => false +| Alt.default _ => true def push (bs : Array FnBody) (b : FnBody) : Array FnBody := let b := b.resetBody; @@ -368,16 +368,16 @@ instance : Inhabited Decl := ⟨fdecl (default _) (default _) IRType.irrelevant (default _)⟩ def name : Decl → FunId -| Decl.fdecl f _ _ _ => f -| Decl.extern f _ _ _ => f +| Decl.fdecl f _ _ _ => f +| Decl.extern f _ _ _ => f def params : Decl → Array Param -| Decl.fdecl _ xs _ _ => xs -| Decl.extern _ xs _ _ => xs +| Decl.fdecl _ xs _ _ => xs +| Decl.extern _ xs _ _ => xs def resultType : Decl → IRType -| Decl.fdecl _ _ t _ => t -| Decl.extern _ _ t _ => t +| Decl.fdecl _ _ t _ => t +| Decl.extern _ _ t _ => t end Decl @@ -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 97c92ef1d1..76f11247d8 100644 --- a/library/init/lean/compiler/ir/borrow.lean +++ b/library/init/lean/compiler/ir/borrow.lean @@ -24,15 +24,15 @@ 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⟩ def getHash : Key → USize -| decl n => hash n -| jp n id => mixHash (hash n) (hash id) +| decl n => hash n +| jp n id => mixHash (hash n) (hash id) instance : Hashable Key := ⟨getHash⟩ end Key @@ -226,16 +226,16 @@ xs.mfor $ fun x => | _ => pure () def collectExpr (z : VarId) : Expr → M Unit -| Expr.reset _ x => ownVar z *> ownVar x -| Expr.reuse x _ _ ys => ownVar z *> ownVar x *> ownArgsIfParam ys -| Expr.ctor _ xs => ownVar z *> ownArgsIfParam xs -| Expr.proj _ x => mwhen (isOwned z) $ ownVar x -| Expr.fap g xs => do ps ← getParamInfo (Key.decl g); +| Expr.reset _ x => ownVar z *> ownVar x +| Expr.reuse x _ _ ys => ownVar z *> ownVar x *> ownArgsIfParam ys +| Expr.ctor _ xs => ownVar z *> ownArgsIfParam xs +| Expr.proj _ x => mwhen (isOwned z) $ ownVar x +| Expr.fap g xs => do ps ← getParamInfo (Key.decl g); -- dbgTrace ("collectExpr: " ++ toString g ++ " " ++ toString (formatParams ps)) $ fun _ => ownVar z *> ownArgsUsingParams xs ps -| Expr.ap x ys => ownVar z *> ownVar x *> ownArgs ys -| Expr.pap _ xs => ownVar z *> ownArgs xs -| other => pure () +| Expr.ap x ys => ownVar z *> ownVar x *> ownArgs ys +| Expr.pap _ xs => ownVar z *> ownArgs xs +| other => pure () def preserveTailCall (x : VarId) (v : Expr) (b : FnBody) : M Unit := do ctx ← read; @@ -251,19 +251,19 @@ def updateParamSet (ctx : BorrowInfCtx) (ps : Array Param) : BorrowInfCtx := { paramSet := ps.foldl (fun s p => s.insert p.x.idx) ctx.paramSet, .. ctx } partial def collectFnBody : FnBody → M Unit -| FnBody.jdecl j ys v b => do +| FnBody.jdecl j ys v b => do adaptReader (fun ctx => updateParamSet ctx ys) (collectFnBody v); ctx ← read; updateParamMap (Key.jp ctx.currFn j); collectFnBody b -| FnBody.vdecl x _ v b => collectFnBody b *> collectExpr x v *> preserveTailCall x v b -| FnBody.jmp j ys => do +| FnBody.vdecl x _ v b => collectFnBody b *> collectExpr x v *> preserveTailCall x v b +| FnBody.jmp j ys => do ctx ← read; ps ← getParamInfo (Key.jp ctx.currFn j); ownArgsUsingParams ys ps; -- for making sure the join point can reuse ownParamsUsingArgs ys ps -- for making sure the tail call is preserved -| FnBody.case _ _ alts => alts.mfor $ fun alt => collectFnBody alt.body -| e => unless (e.isTerminal) $ collectFnBody e.body +| FnBody.case _ _ alts => alts.mfor $ fun alt => collectFnBody alt.body +| e => unless (e.isTerminal) $ collectFnBody e.body @[specialize] partial def whileModifingOwnedAux (x : M Unit) : Unit → M Unit | _ => do diff --git a/library/init/lean/compiler/ir/boxing.lean b/library/init/lean/compiler/ir/boxing.lean index 254fc6de47..9e7957d4bb 100644 --- a/library/init/lean/compiler/ir/boxing.lean +++ b/library/init/lean/compiler/ir/boxing.lean @@ -231,35 +231,35 @@ match e with pure $ FnBody.vdecl x ty e b partial def visitFnBody : FnBody → M FnBody -| FnBody.vdecl x t v b => do +| FnBody.vdecl x t v b => do b ← withVDecl x t v (visitFnBody b); visitVDeclExpr x t v b -| FnBody.jdecl j xs v b => do +| FnBody.jdecl j xs v b => do v ← withParams xs (visitFnBody v); b ← withJDecl j xs v (visitFnBody b); pure $ FnBody.jdecl j xs v b -| FnBody.uset x i y b => do +| FnBody.uset x i y b => do b ← visitFnBody b; castVarIfNeeded y IRType.usize $ fun y => pure $ FnBody.uset x i y b -| FnBody.sset x i o y ty b => do +| FnBody.sset x i o y ty b => do b ← visitFnBody b; castVarIfNeeded y ty $ fun y => pure $ FnBody.sset x i o y ty b -| FnBody.mdata d b => +| FnBody.mdata d b => FnBody.mdata d <$> visitFnBody b -| FnBody.case tid x alts => do +| FnBody.case tid x alts => do let expected := getScrutineeType alts; alts ← alts.mmap $ fun alt => alt.mmodifyBody visitFnBody; castVarIfNeeded x expected $ fun x => pure $ FnBody.case tid x alts -| FnBody.ret x => do +| FnBody.ret x => do expected ← getResultType; castArgIfNeeded x expected (fun x => pure $ FnBody.ret x) -| FnBody.jmp j ys => do +| FnBody.jmp j ys => do ps ← getJPParams j; castArgsIfNeeded ys ps (fun ys => pure $ FnBody.jmp j ys) -| other => +| other => pure other def run (env : Environment) (decls : Array Decl) : Array Decl := diff --git a/library/init/lean/compiler/ir/checker.lean b/library/init/lean/compiler/ir/checker.lean index 3f50616bc4..53ac0d91bc 100644 --- a/library/init/lean/compiler/ir/checker.lean +++ b/library/init/lean/compiler/ir/checker.lean @@ -70,21 +70,21 @@ unless (ys.size < decl.params.size) (throw ("too many arguments too partial appl checkArgs ys def checkExpr (ty : IRType) : Expr → M Unit -| Expr.pap f ys => checkPartialApp f ys *> checkObjType ty -- partial applications should always produce a closure object -| Expr.ap x ys => checkObjVar x *> checkArgs ys -| Expr.fap f ys => checkFullApp f ys -| Expr.ctor c ys => when c.isRef (checkObjType ty) *> checkArgs ys -| Expr.reset _ x => checkObjVar x *> checkObjType ty -| Expr.reuse x i u ys => checkObjVar x *> checkArgs ys *> checkObjType ty -| Expr.box xty x => checkObjType ty *> checkScalarVar x *> checkVarType x (fun t => t == xty) -| Expr.unbox x => checkScalarType ty *> checkObjVar x -| Expr.proj _ x => checkObjVar x *> checkObjType ty -| Expr.uproj _ x => checkObjVar x *> checkType ty (fun t => t == IRType.usize) -| Expr.sproj _ _ x => checkObjVar x *> checkScalarType ty -| Expr.isShared x => checkObjVar x *> checkType ty (fun t => t == IRType.uint8) -| Expr.isTaggedPtr x => checkObjVar x *> checkType ty (fun t => t == IRType.uint8) -| Expr.lit (LitVal.str _) => checkObjType ty -| Expr.lit _ => pure () +| Expr.pap f ys => checkPartialApp f ys *> checkObjType ty -- partial applications should always produce a closure object +| Expr.ap x ys => checkObjVar x *> checkArgs ys +| Expr.fap f ys => checkFullApp f ys +| Expr.ctor c ys => when c.isRef (checkObjType ty) *> checkArgs ys +| Expr.reset _ x => checkObjVar x *> checkObjType ty +| Expr.reuse x i u ys => checkObjVar x *> checkArgs ys *> checkObjType ty +| Expr.box xty x => checkObjType ty *> checkScalarVar x *> checkVarType x (fun t => t == xty) +| Expr.unbox x => checkScalarType ty *> checkObjVar x +| Expr.proj _ x => checkObjVar x *> checkObjType ty +| Expr.uproj _ x => checkObjVar x *> checkType ty (fun t => t == IRType.usize) +| Expr.sproj _ _ x => checkObjVar x *> checkScalarType ty +| Expr.isShared x => checkObjVar x *> checkType ty (fun t => t == IRType.uint8) +| Expr.isTaggedPtr x => checkObjVar x *> checkType ty (fun t => t == IRType.uint8) +| Expr.lit (LitVal.str _) => checkObjType ty +| Expr.lit _ => pure () @[inline] def withParams (ps : Array Param) (k : M Unit) : M Unit := do ctx ← read; @@ -94,32 +94,32 @@ do ctx ← read; adaptReader (fun _ => { localCtx := localCtx, .. ctx }) k partial def checkFnBody : FnBody → M Unit -| FnBody.vdecl x t v b => do +| FnBody.vdecl x t v b => do checkExpr t v; ctx ← read; when (ctx.localCtx.contains x.idx) $ throw ("invalid variable declaration, shadowing is not allowed"); adaptReader (fun (ctx : Context) => { localCtx := ctx.localCtx.addLocal x t v, .. ctx }) (checkFnBody b) -| FnBody.jdecl j ys v b => do +| FnBody.jdecl j ys v b => do withParams ys (checkFnBody v); ctx ← read; when (ctx.localCtx.contains j.idx) $ throw ("invalid join point declaration, shadowing is not allowed"); adaptReader (fun (ctx : Context) => { localCtx := ctx.localCtx.addJP j ys v, .. ctx }) (checkFnBody b) -| FnBody.set x _ y b => checkVar x *> checkArg y *> checkFnBody b -| FnBody.uset x _ y b => checkVar x *> checkVar y *> checkFnBody b -| FnBody.sset x _ _ y _ b => checkVar x *> checkVar y *> checkFnBody b -| FnBody.setTag x _ b => checkVar x *> checkFnBody b -| FnBody.inc x _ _ b => checkVar x *> checkFnBody b -| FnBody.dec x _ _ b => checkVar x *> checkFnBody b -| FnBody.del x b => checkVar x *> checkFnBody b -| FnBody.mdata _ b => checkFnBody b -| FnBody.jmp j ys => checkJP j *> checkArgs ys -| FnBody.ret x => checkArg x -| FnBody.case _ x alts => checkVar x *> alts.mfor (fun alt => checkFnBody alt.body) -| FnBody.unreachable => pure () +| FnBody.set x _ y b => checkVar x *> checkArg y *> checkFnBody b +| FnBody.uset x _ y b => checkVar x *> checkVar y *> checkFnBody b +| FnBody.sset x _ _ y _ b => checkVar x *> checkVar y *> checkFnBody b +| FnBody.setTag x _ b => checkVar x *> checkFnBody b +| FnBody.inc x _ _ b => checkVar x *> checkFnBody b +| FnBody.dec x _ _ b => checkVar x *> checkFnBody b +| FnBody.del x b => checkVar x *> checkFnBody b +| FnBody.mdata _ b => checkFnBody b +| FnBody.jmp j ys => checkJP j *> checkArgs ys +| FnBody.ret x => checkArg x +| FnBody.case _ x alts => checkVar x *> alts.mfor (fun alt => checkFnBody alt.body) +| FnBody.unreachable => pure () def checkDecl : Decl → M Unit -| Decl.fdecl f xs t b => withParams xs (checkFnBody b) -| Decl.extern f xs t _ => withParams xs (pure ()) +| Decl.fdecl f xs t b => withParams xs (checkFnBody b) +| Decl.extern f xs t _ => withParams xs (pure ()) end Checker diff --git a/library/init/lean/compiler/ir/compilerm.lean b/library/init/lean/compiler/ir/compilerm.lean index 069d03f7f8..f02abe90ad 100644 --- a/library/init/lean/compiler/ir/compilerm.lean +++ b/library/init/lean/compiler/ir/compilerm.lean @@ -18,8 +18,8 @@ inductive LogEntry namespace LogEntry protected def fmt : LogEntry → Format -| step cls decls => Format.bracket "[" (format cls) "]" ++ decls.foldl (fun fmt decl => fmt ++ Format.line ++ format decl) Format.nil -| message msg => msg +| step cls decls => Format.bracket "[" (format cls) "]" ++ decls.foldl (fun fmt decl => fmt ++ Format.line ++ format decl) Format.nil +| message msg => msg instance : HasFormat LogEntry := ⟨LogEntry.fmt⟩ end LogEntry diff --git a/library/init/lean/compiler/ir/elimdead.lean b/library/init/lean/compiler/ir/elimdead.lean index 2d8ec73237..70dcf44a31 100644 --- a/library/init/lean/compiler/ir/elimdead.lean +++ b/library/init/lean/compiler/ir/elimdead.lean @@ -44,8 +44,8 @@ partial def FnBody.elimDead : FnBody → FnBody /-- Eliminate dead let-declarations and join points -/ def Decl.elimDead : Decl → Decl -| Decl.fdecl f xs t b => Decl.fdecl f xs t b.elimDead -| other => other +| Decl.fdecl f xs t b => Decl.fdecl f xs t b.elimDead +| other => other end IR end Lean diff --git a/library/init/lean/compiler/ir/emitcpp.lean b/library/init/lean/compiler/ir/emitcpp.lean index 27c9282e3e..ef1d597b31 100644 --- a/library/init/lean/compiler/ir/emitcpp.lean +++ b/library/init/lean/compiler/ir/emitcpp.lean @@ -69,9 +69,9 @@ def toCppType : IRType → String | IRType.irrelevant => "obj*" def openNamespacesAux : Name → M Unit -| Name.anonymous => pure () -| Name.mkString p s => openNamespacesAux p *> emitLn ("namespace " ++ s ++ " {") -| n => throw ("invalid namespace '" ++ toString n ++ "'") +| Name.anonymous => pure () +| Name.mkString p s => openNamespacesAux p *> emitLn ("namespace " ++ s ++ " {") +| n => throw ("invalid namespace '" ++ toString n ++ "'") def openNamespaces (n : Name) : M Unit := openNamespacesAux n.getPrefix @@ -83,9 +83,9 @@ do env ← getEnv; | some n => openNamespaces n def closeNamespacesAux : Name → M Unit -| Name.anonymous => pure () -| Name.mkString p _ => emitLn "}" *> closeNamespacesAux p -| n => throw ("invalid namespace '" ++ toString n ++ "'") +| Name.anonymous => pure () +| Name.mkString p _ => emitLn "}" *> closeNamespacesAux p +| n => throw ("invalid namespace '" ++ toString n ++ "'") def closeNamespaces (n : Name) : M Unit := closeNamespacesAux n.getPrefix @@ -600,25 +600,25 @@ match v with | _ => throw "bug at emitTailCall" partial def emitBlock (emitBody : FnBody → M Unit) : FnBody → M Unit -| FnBody.jdecl j xs v b => emitBlock b -| d@(FnBody.vdecl x t v b) => +| FnBody.jdecl j xs v b => emitBlock b +| d@(FnBody.vdecl x t v b) => do ctx ← read; if isTailCallTo ctx.mainFn d then emitTailCall v else emitVDecl x t v *> emitBlock b -| FnBody.inc x n c b => emitInc x n c *> emitBlock b -| FnBody.dec x n c b => emitDec x n c *> emitBlock b -| FnBody.del x b => emitDel x *> emitBlock b -| FnBody.setTag x i b => emitSetTag x i *> emitBlock b -| FnBody.set x i y b => emitSet x i y *> emitBlock b -| FnBody.uset x i y b => emitUSet x i y *> emitBlock b -| FnBody.sset x i o y _ b => emitSSet x i o y *> emitBlock b -| FnBody.mdata _ b => emitBlock b -| FnBody.ret x => emit "return " *> emitArg x *> emitLn ";" -| FnBody.case _ x alts => emitCase emitBody x alts -| FnBody.jmp j xs => emitJmp j xs -| FnBody.unreachable => emitLn "lean_unreachable();" +| FnBody.inc x n c b => emitInc x n c *> emitBlock b +| FnBody.dec x n c b => emitDec x n c *> emitBlock b +| FnBody.del x b => emitDel x *> emitBlock b +| FnBody.setTag x i b => emitSetTag x i *> emitBlock b +| FnBody.set x i y b => emitSet x i y *> emitBlock b +| FnBody.uset x i y b => emitUSet x i y *> emitBlock b +| FnBody.sset x i o y _ b => emitSSet x i o y *> emitBlock b +| FnBody.mdata _ b => emitBlock b +| FnBody.ret x => emit "return " *> emitArg x *> emitLn ";" +| FnBody.case _ x alts => emitCase emitBody x alts +| FnBody.jmp j xs => emitJmp j xs +| FnBody.unreachable => emitLn "lean_unreachable();" partial def emitJPs (emitBody : FnBody → M Unit) : FnBody → M Unit -| FnBody.jdecl j xs v b => do emit j; emitLn ":"; emitBody v; emitJPs b -| e => unless e.isTerminal (emitJPs e.body) +| FnBody.jdecl j xs v b => do emit j; emitLn ":"; emitBody v; emitJPs b +| e => unless e.isTerminal (emitJPs e.body) partial def emitFnBody : FnBody → M Unit | b => do diff --git a/library/init/lean/compiler/ir/emitutil.lean b/library/init/lean/compiler/ir/emitutil.lean index 5446e697b4..9bf8e2b110 100644 --- a/library/init/lean/compiler/ir/emitutil.lean +++ b/library/init/lean/compiler/ir/emitutil.lean @@ -52,8 +52,8 @@ partial def visitFnBody : FnBody → M Bool end UsesLeanNamespace def usesLeanNamespace (env : Environment) : Decl → Bool -| Decl.fdecl _ _ _ b => (UsesLeanNamespace.visitFnBody b env).run' {} -| _ => false +| Decl.fdecl _ _ _ b => (UsesLeanNamespace.visitFnBody b env).run' {} +| _ => false namespace CollectUsedDecls @@ -80,8 +80,8 @@ do env ← read; | _ => pure () def collectDecl : Decl → M NameSet -| Decl.fdecl fn _ _ b => collectInitDecl fn *> CollectUsedDecls.collectFnBody b *> get -| Decl.extern fn _ _ _ => collectInitDecl fn *> get +| Decl.fdecl fn _ _ b => collectInitDecl fn *> CollectUsedDecls.collectFnBody b *> get +| Decl.extern fn _ _ _ => collectInitDecl fn *> get end CollectUsedDecls @@ -102,10 +102,10 @@ fun s => ps.foldl (fun s p => collectVar p.x p.ty s) s /- `collectFnBody` assumes the variables in -/ partial def collectFnBody : FnBody → Collector -| FnBody.vdecl x t _ b => collectVar x t ∘ collectFnBody b -| FnBody.jdecl j xs v b => collectJP j xs ∘ collectParams xs ∘ collectFnBody v ∘ collectFnBody b -| FnBody.case _ _ alts => fun s => alts.foldl (fun s alt => collectFnBody alt.body s) s -| e => if e.isTerminal then id else collectFnBody e.body +| FnBody.vdecl x t _ b => collectVar x t ∘ collectFnBody b +| FnBody.jdecl j xs v b => collectJP j xs ∘ collectParams xs ∘ collectFnBody v ∘ collectFnBody b +| FnBody.case _ _ alts => fun s => alts.foldl (fun s alt => collectFnBody alt.body s) s +| e => if e.isTerminal then id else collectFnBody e.body def collectDecl : Decl → Collector | Decl.fdecl _ xs _ b => collectParams xs ∘ collectFnBody b diff --git a/library/init/lean/compiler/ir/expandresetreuse.lean b/library/init/lean/compiler/ir/expandresetreuse.lean index e9c8256d4d..f0d34a2fb6 100644 --- a/library/init/lean/compiler/ir/expandresetreuse.lean +++ b/library/init/lean/compiler/ir/expandresetreuse.lean @@ -25,10 +25,10 @@ fun m => match v with | _ => m partial def collectFnBody : FnBody → Collector -| FnBody.vdecl x _ v b => collectVDecl x v ∘ collectFnBody b -| FnBody.jdecl _ _ v b => collectFnBody v ∘ collectFnBody b -| FnBody.case _ _ alts => fun s => alts.foldl (fun s alt => collectFnBody alt.body s) s -| e => if e.isTerminal then id else collectFnBody e.body +| FnBody.vdecl x _ v b => collectVDecl x v ∘ collectFnBody b +| FnBody.jdecl _ _ v b => collectFnBody v ∘ collectFnBody b +| FnBody.case _ _ alts => fun s => alts.foldl (fun s alt => collectFnBody alt.body s) s +| e => if e.isTerminal then id else collectFnBody e.body end CollectProjMap /- Create a mapping from variables to projections. diff --git a/library/init/lean/compiler/ir/format.lean b/library/init/lean/compiler/ir/format.lean index c861dcf827..8da56e8af8 100644 --- a/library/init/lean/compiler/ir/format.lean +++ b/library/init/lean/compiler/ir/format.lean @@ -19,8 +19,8 @@ private def formatArray {α : Type} [HasFormat α] (args : Array α) : Format := args.foldl (fun r a => r ++ " " ++ format a) Format.nil private def formatLitVal : LitVal → Format -| LitVal.num v => format v -| LitVal.str v => format (repr v) +| LitVal.num v => format v +| LitVal.str v => format (repr v) instance litValHasFormat : HasFormat LitVal := ⟨formatLitVal⟩ @@ -34,20 +34,20 @@ private def formatCtorInfo : CtorInfo → Format instance ctorInfoHasFormat : HasFormat CtorInfo := ⟨formatCtorInfo⟩ private def formatExpr : Expr → Format -| Expr.ctor i ys => format i ++ formatArray ys -| Expr.reset n x => "reset[" ++ format n ++ "] " ++ format x -| Expr.reuse x i u ys => "reuse" ++ (if u then "!" else "") ++ " " ++ format x ++ " in " ++ format i ++ formatArray ys -| Expr.proj i x => "proj[" ++ format i ++ "] " ++ format x -| Expr.uproj i x => "uproj[" ++ format i ++ "] " ++ format x -| Expr.sproj n o x => "sproj[" ++ format n ++ ", " ++ format o ++ "] " ++ format x -| Expr.fap c ys => format c ++ formatArray ys -| Expr.pap c ys => "pap " ++ format c ++ formatArray ys -| Expr.ap x ys => "app " ++ format x ++ formatArray ys -| Expr.box _ x => "box " ++ format x -| Expr.unbox x => "unbox " ++ format x -| Expr.lit v => format v -| Expr.isShared x => "isShared " ++ format x -| Expr.isTaggedPtr x => "isTaggedPtr " ++ format x +| Expr.ctor i ys => format i ++ formatArray ys +| Expr.reset n x => "reset[" ++ format n ++ "] " ++ format x +| Expr.reuse x i u ys => "reuse" ++ (if u then "!" else "") ++ " " ++ format x ++ " in " ++ format i ++ formatArray ys +| Expr.proj i x => "proj[" ++ format i ++ "] " ++ format x +| Expr.uproj i x => "uproj[" ++ format i ++ "] " ++ format x +| Expr.sproj n o x => "sproj[" ++ format n ++ ", " ++ format o ++ "] " ++ format x +| Expr.fap c ys => format c ++ formatArray ys +| Expr.pap c ys => "pap " ++ format c ++ formatArray ys +| Expr.ap x ys => "app " ++ format x ++ formatArray ys +| Expr.box _ x => "box " ++ format x +| Expr.unbox x => "unbox " ++ format x +| Expr.lit v => format v +| Expr.isShared x => "isShared " ++ format x +| Expr.isTaggedPtr x => "isTaggedPtr " ++ format x instance exprHasFormat : HasFormat Expr := ⟨formatExpr⟩ instance exprHasToString : HasToString Expr := ⟨fun e => Format.pretty (format e)⟩ @@ -71,34 +71,34 @@ private def formatParam : Param → Format instance paramHasFormat : HasFormat Param := ⟨formatParam⟩ def formatAlt (fmt : FnBody → Format) (indent : Nat) : Alt → Format -| Alt.ctor i b => format i.name ++ " →" ++ Format.nest indent (Format.line ++ fmt b) -| Alt.default b => "default →" ++ Format.nest indent (Format.line ++ fmt b) +| Alt.ctor i b => format i.name ++ " →" ++ Format.nest indent (Format.line ++ fmt b) +| Alt.default b => "default →" ++ Format.nest indent (Format.line ++ fmt b) def formatParams (ps : Array Param) : Format := formatArray ps partial def formatFnBody (indent : Nat := 2) : FnBody → Format -| FnBody.vdecl x ty e b => "let " ++ format x ++ " : " ++ format ty ++ " := " ++ format e ++ ";" ++ Format.line ++ formatFnBody b -| FnBody.jdecl j xs v b => format j ++ formatParams xs ++ " :=" ++ Format.nest indent (Format.line ++ formatFnBody v) ++ ";" ++ Format.line ++ formatFnBody b -| FnBody.set x i y b => "set " ++ format x ++ "[" ++ format i ++ "] := " ++ format y ++ ";" ++ Format.line ++ formatFnBody b -| FnBody.uset x i y b => "uset " ++ format x ++ "[" ++ format i ++ "] := " ++ format y ++ ";" ++ Format.line ++ formatFnBody b -| FnBody.sset x i o y ty b => "sset " ++ format x ++ "[" ++ format i ++ ", " ++ format o ++ "] : " ++ format ty ++ " := " ++ format y ++ ";" ++ Format.line ++ formatFnBody b -| FnBody.setTag x cidx b => "setTag " ++ format x ++ " := " ++ format cidx ++ ";" ++ Format.line ++ formatFnBody b -| FnBody.inc x n c b => "inc" ++ (if n != 1 then Format.sbracket (format n) else "") ++ " " ++ format x ++ ";" ++ Format.line ++ formatFnBody b -| FnBody.dec x n c b => "dec" ++ (if n != 1 then Format.sbracket (format n) else "") ++ " " ++ format x ++ ";" ++ Format.line ++ formatFnBody b -| FnBody.del x b => "del " ++ format x ++ ";" ++ Format.line ++ formatFnBody b -| FnBody.mdata d b => "mdata " ++ format d ++ ";" ++ Format.line ++ formatFnBody b -| FnBody.case tid x cs => "case " ++ format x ++ " of" ++ cs.foldl (fun r c => r ++ Format.line ++ formatAlt formatFnBody indent c) Format.nil -| FnBody.jmp j ys => "jmp " ++ format j ++ formatArray ys -| FnBody.ret x => "ret " ++ format x -| FnBody.unreachable => "⊥" +| FnBody.vdecl x ty e b => "let " ++ format x ++ " : " ++ format ty ++ " := " ++ format e ++ ";" ++ Format.line ++ formatFnBody b +| FnBody.jdecl j xs v b => format j ++ formatParams xs ++ " :=" ++ Format.nest indent (Format.line ++ formatFnBody v) ++ ";" ++ Format.line ++ formatFnBody b +| FnBody.set x i y b => "set " ++ format x ++ "[" ++ format i ++ "] := " ++ format y ++ ";" ++ Format.line ++ formatFnBody b +| FnBody.uset x i y b => "uset " ++ format x ++ "[" ++ format i ++ "] := " ++ format y ++ ";" ++ Format.line ++ formatFnBody b +| FnBody.sset x i o y ty b => "sset " ++ format x ++ "[" ++ format i ++ ", " ++ format o ++ "] : " ++ format ty ++ " := " ++ format y ++ ";" ++ Format.line ++ formatFnBody b +| FnBody.setTag x cidx b => "setTag " ++ format x ++ " := " ++ format cidx ++ ";" ++ Format.line ++ formatFnBody b +| FnBody.inc x n c b => "inc" ++ (if n != 1 then Format.sbracket (format n) else "") ++ " " ++ format x ++ ";" ++ Format.line ++ formatFnBody b +| FnBody.dec x n c b => "dec" ++ (if n != 1 then Format.sbracket (format n) else "") ++ " " ++ format x ++ ";" ++ Format.line ++ formatFnBody b +| FnBody.del x b => "del " ++ format x ++ ";" ++ Format.line ++ formatFnBody b +| FnBody.mdata d b => "mdata " ++ format d ++ ";" ++ Format.line ++ formatFnBody b +| FnBody.case tid x cs => "case " ++ format x ++ " of" ++ cs.foldl (fun r c => r ++ Format.line ++ formatAlt formatFnBody indent c) Format.nil +| FnBody.jmp j ys => "jmp " ++ format j ++ formatArray ys +| FnBody.ret x => "ret " ++ format x +| FnBody.unreachable => "⊥" instance fnBodyHasFormat : HasFormat FnBody := ⟨formatFnBody⟩ instance fnBodyHasToString : HasToString FnBody := ⟨fun b => (format b).pretty⟩ def formatDecl (indent : Nat := 2) : Decl → Format -| Decl.fdecl f xs ty b => "def " ++ format f ++ formatParams xs ++ format " : " ++ format ty ++ " :=" ++ Format.nest indent (Format.line ++ formatFnBody indent b) -| Decl.extern f xs ty _ => "extern " ++ format f ++ formatParams xs ++ format " : " ++ format ty +| Decl.fdecl f xs ty b => "def " ++ format f ++ formatParams xs ++ format " : " ++ format ty ++ " :=" ++ Format.nest indent (Format.line ++ formatFnBody indent b) +| Decl.extern f xs ty _ => "extern " ++ format f ++ formatParams xs ++ format " : " ++ format ty instance declHasFormat : HasFormat Decl := ⟨formatDecl⟩ diff --git a/library/init/lean/compiler/ir/freevars.lean b/library/init/lean/compiler/ir/freevars.lean index b014309f1b..3612884f26 100644 --- a/library/init/lean/compiler/ir/freevars.lean +++ b/library/init/lean/compiler/ir/freevars.lean @@ -28,8 +28,8 @@ abbrev Collector := Index → Index instance : HasAndthen Collector := ⟨seq⟩ private def collectArg : Arg → Collector -| Arg.var x => collectVar x -| irrelevant => skip +| Arg.var x => collectVar x +| irrelevant => skip @[specialize] private def collectArray {α : Type} (as : Array α) (f : α → Collector) : Collector := fun m => as.foldl (fun m a => f a m) m @@ -39,43 +39,43 @@ private def collectParam (p : Param) : Collector := collectVar p.x private def collectParams (ps : Array Param) : Collector := collectArray ps collectParam private def collectExpr : Expr → Collector -| Expr.ctor _ ys => collectArgs ys -| Expr.reset _ x => collectVar x -| Expr.reuse x _ _ ys => collectVar x >> collectArgs ys -| Expr.proj _ x => collectVar x -| Expr.uproj _ x => collectVar x -| Expr.sproj _ _ x => collectVar x -| Expr.fap _ ys => collectArgs ys -| Expr.pap _ ys => collectArgs ys -| Expr.ap x ys => collectVar x >> collectArgs ys -| Expr.box _ x => collectVar x -| Expr.unbox x => collectVar x -| Expr.lit v => skip -| Expr.isShared x => collectVar x -| Expr.isTaggedPtr x => collectVar x +| Expr.ctor _ ys => collectArgs ys +| Expr.reset _ x => collectVar x +| Expr.reuse x _ _ ys => collectVar x >> collectArgs ys +| Expr.proj _ x => collectVar x +| Expr.uproj _ x => collectVar x +| Expr.sproj _ _ x => collectVar x +| Expr.fap _ ys => collectArgs ys +| Expr.pap _ ys => collectArgs ys +| Expr.ap x ys => collectVar x >> collectArgs ys +| Expr.box _ x => collectVar x +| Expr.unbox x => collectVar x +| Expr.lit v => skip +| Expr.isShared x => collectVar x +| Expr.isTaggedPtr x => collectVar x private def collectAlts (f : FnBody → Collector) (alts : Array Alt) : Collector := collectArray alts $ fun alt => f alt.body partial def collectFnBody : FnBody → Collector -| FnBody.vdecl x _ v b => collectExpr v >> collectFnBody b -| FnBody.jdecl j ys v b => collectFnBody v >> collectParams ys >> collectFnBody b -| FnBody.set x _ y b => collectVar x >> collectArg y >> collectFnBody b -| FnBody.uset x _ y b => collectVar x >> collectVar y >> collectFnBody b -| FnBody.sset x _ _ y _ b => collectVar x >> collectVar y >> collectFnBody b -| FnBody.setTag x _ b => collectVar x >> collectFnBody b -| FnBody.inc x _ _ b => collectVar x >> collectFnBody b -| FnBody.dec x _ _ b => collectVar x >> collectFnBody b -| FnBody.del x b => collectVar x >> collectFnBody b -| FnBody.mdata _ b => collectFnBody b -| FnBody.case _ x alts => collectVar x >> collectAlts collectFnBody alts -| FnBody.jmp j ys => collectJP j >> collectArgs ys -| FnBody.ret x => collectArg x -| FnBody.unreachable => skip +| FnBody.vdecl x _ v b => collectExpr v >> collectFnBody b +| FnBody.jdecl j ys v b => collectFnBody v >> collectParams ys >> collectFnBody b +| FnBody.set x _ y b => collectVar x >> collectArg y >> collectFnBody b +| FnBody.uset x _ y b => collectVar x >> collectVar y >> collectFnBody b +| FnBody.sset x _ _ y _ b => collectVar x >> collectVar y >> collectFnBody b +| FnBody.setTag x _ b => collectVar x >> collectFnBody b +| FnBody.inc x _ _ b => collectVar x >> collectFnBody b +| FnBody.dec x _ _ b => collectVar x >> collectFnBody b +| FnBody.del x b => collectVar x >> collectFnBody b +| FnBody.mdata _ b => collectFnBody b +| FnBody.case _ x alts => collectVar x >> collectAlts collectFnBody alts +| FnBody.jmp j ys => collectJP j >> collectArgs ys +| FnBody.ret x => collectArg x +| FnBody.unreachable => skip partial def collectDecl : Decl → Collector -| Decl.fdecl _ xs _ b => collectParams xs >> collectFnBody b -| Decl.extern _ xs _ _ => collectParams xs +| Decl.fdecl _ xs _ b => collectParams xs >> collectFnBody b +| Decl.extern _ xs _ _ => collectParams xs end MaxIndex @@ -124,8 +124,8 @@ fun k₁ k₂ bv fv => k₂ bv (k₁ bv fv) instance : HasAndthen Collector := ⟨seq⟩ private def collectArg : Arg → Collector -| Arg.var x => collectVar x -| irrelevant => skip +| Arg.var x => collectVar x +| irrelevant => skip @[specialize] private def collectArray {α : Type} (as : Array α) (f : α → Collector) : Collector := fun bv fv => as.foldl (fun fv a => f a bv fv) fv @@ -134,39 +134,39 @@ private def collectArgs (as : Array Arg) : Collector := collectArray as collectArg private def collectExpr : Expr → Collector -| Expr.ctor _ ys => collectArgs ys -| Expr.reset _ x => collectVar x -| Expr.reuse x _ _ ys => collectVar x >> collectArgs ys -| Expr.proj _ x => collectVar x -| Expr.uproj _ x => collectVar x -| Expr.sproj _ _ x => collectVar x -| Expr.fap _ ys => collectArgs ys -| Expr.pap _ ys => collectArgs ys -| Expr.ap x ys => collectVar x >> collectArgs ys -| Expr.box _ x => collectVar x -| Expr.unbox x => collectVar x -| Expr.lit v => skip -| Expr.isShared x => collectVar x -| Expr.isTaggedPtr x => collectVar x +| Expr.ctor _ ys => collectArgs ys +| Expr.reset _ x => collectVar x +| Expr.reuse x _ _ ys => collectVar x >> collectArgs ys +| Expr.proj _ x => collectVar x +| Expr.uproj _ x => collectVar x +| Expr.sproj _ _ x => collectVar x +| Expr.fap _ ys => collectArgs ys +| Expr.pap _ ys => collectArgs ys +| Expr.ap x ys => collectVar x >> collectArgs ys +| Expr.box _ x => collectVar x +| Expr.unbox x => collectVar x +| Expr.lit v => skip +| Expr.isShared x => collectVar x +| Expr.isTaggedPtr x => collectVar x private def collectAlts (f : FnBody → Collector) (alts : Array Alt) : Collector := collectArray alts $ fun alt => f alt.body partial def collectFnBody : FnBody → Collector -| FnBody.vdecl x _ v b => collectExpr v >> withVar x (collectFnBody b) -| FnBody.jdecl j ys v b => withParams ys (collectFnBody v) >> withJP j (collectFnBody b) -| FnBody.set x _ y b => collectVar x >> collectArg y >> collectFnBody b -| FnBody.uset x _ y b => collectVar x >> collectVar y >> collectFnBody b -| FnBody.sset x _ _ y _ b => collectVar x >> collectVar y >> collectFnBody b -| FnBody.setTag x _ b => collectVar x >> collectFnBody b -| FnBody.inc x _ _ b => collectVar x >> collectFnBody b -| FnBody.dec x _ _ b => collectVar x >> collectFnBody b -| FnBody.del x b => collectVar x >> collectFnBody b -| FnBody.mdata _ b => collectFnBody b -| FnBody.case _ x alts => collectVar x >> collectAlts collectFnBody alts -| FnBody.jmp j ys => collectJP j >> collectArgs ys -| FnBody.ret x => collectArg x -| FnBody.unreachable => skip +| FnBody.vdecl x _ v b => collectExpr v >> withVar x (collectFnBody b) +| FnBody.jdecl j ys v b => withParams ys (collectFnBody v) >> withJP j (collectFnBody b) +| FnBody.set x _ y b => collectVar x >> collectArg y >> collectFnBody b +| FnBody.uset x _ y b => collectVar x >> collectVar y >> collectFnBody b +| FnBody.sset x _ _ y _ b => collectVar x >> collectVar y >> collectFnBody b +| FnBody.setTag x _ b => collectVar x >> collectFnBody b +| FnBody.inc x _ _ b => collectVar x >> collectFnBody b +| FnBody.dec x _ _ b => collectVar x >> collectFnBody b +| FnBody.del x b => collectVar x >> collectFnBody b +| FnBody.mdata _ b => collectFnBody b +| FnBody.case _ x alts => collectVar x >> collectAlts collectFnBody alts +| FnBody.jmp j ys => collectJP j >> collectArgs ys +| FnBody.ret x => collectArg x +| FnBody.unreachable => skip end FreeIndices @@ -185,8 +185,8 @@ def visitVar (w : Index) (x : VarId) : Bool := w == x.idx def visitJP (w : Index) (x : JoinPointId) : Bool := w == x.idx def visitArg (w : Index) : Arg → Bool -| Arg.var x => visitVar w x -| _ => false +| Arg.var x => visitVar w x +| _ => false def visitArgs (w : Index) (xs : Array Arg) : Bool := xs.any (visitArg w) @@ -195,36 +195,36 @@ def visitParams (w : Index) (ps : Array Param) : Bool := ps.any (fun p => w == p.x.idx) def visitExpr (w : Index) : Expr → Bool -| Expr.ctor _ ys => visitArgs w ys -| Expr.reset _ x => visitVar w x -| Expr.reuse x _ _ ys => visitVar w x || visitArgs w ys -| Expr.proj _ x => visitVar w x -| Expr.uproj _ x => visitVar w x -| Expr.sproj _ _ x => visitVar w x -| Expr.fap _ ys => visitArgs w ys -| Expr.pap _ ys => visitArgs w ys -| Expr.ap x ys => visitVar w x || visitArgs w ys -| Expr.box _ x => visitVar w x -| Expr.unbox x => visitVar w x -| Expr.lit v => false -| Expr.isShared x => visitVar w x -| Expr.isTaggedPtr x => visitVar w x +| Expr.ctor _ ys => visitArgs w ys +| Expr.reset _ x => visitVar w x +| Expr.reuse x _ _ ys => visitVar w x || visitArgs w ys +| Expr.proj _ x => visitVar w x +| Expr.uproj _ x => visitVar w x +| Expr.sproj _ _ x => visitVar w x +| Expr.fap _ ys => visitArgs w ys +| Expr.pap _ ys => visitArgs w ys +| Expr.ap x ys => visitVar w x || visitArgs w ys +| Expr.box _ x => visitVar w x +| Expr.unbox x => visitVar w x +| Expr.lit v => false +| Expr.isShared x => visitVar w x +| Expr.isTaggedPtr x => visitVar w x partial def visitFnBody (w : Index) : FnBody → Bool -| FnBody.vdecl x _ v b => visitExpr w v || visitFnBody b -| FnBody.jdecl j ys v b => visitFnBody v || visitFnBody b -| FnBody.set x _ y b => visitVar w x || visitArg w y || visitFnBody b -| FnBody.uset x _ y b => visitVar w x || visitVar w y || visitFnBody b -| FnBody.sset x _ _ y _ b => visitVar w x || visitVar w y || visitFnBody b -| FnBody.setTag x _ b => visitVar w x || visitFnBody b -| FnBody.inc x _ _ b => visitVar w x || visitFnBody b -| FnBody.dec x _ _ b => visitVar w x || visitFnBody b -| FnBody.del x b => visitVar w x || visitFnBody b -| FnBody.mdata _ b => visitFnBody b -| FnBody.jmp j ys => visitJP w j || visitArgs w ys -| FnBody.ret x => visitArg w x -| FnBody.case _ x alts => visitVar w x || alts.any (fun alt => visitFnBody alt.body) -| FnBody.unreachable => false +| FnBody.vdecl x _ v b => visitExpr w v || visitFnBody b +| FnBody.jdecl j ys v b => visitFnBody v || visitFnBody b +| FnBody.set x _ y b => visitVar w x || visitArg w y || visitFnBody b +| FnBody.uset x _ y b => visitVar w x || visitVar w y || visitFnBody b +| FnBody.sset x _ _ y _ b => visitVar w x || visitVar w y || visitFnBody b +| FnBody.setTag x _ b => visitVar w x || visitFnBody b +| FnBody.inc x _ _ b => visitVar w x || visitFnBody b +| FnBody.dec x _ _ b => visitVar w x || visitFnBody b +| FnBody.del x b => visitVar w x || visitFnBody b +| FnBody.mdata _ b => visitFnBody b +| FnBody.jmp j ys => visitJP w j || visitArgs w ys +| FnBody.ret x => visitArg w x +| FnBody.case _ x alts => visitVar w x || alts.any (fun alt => visitFnBody alt.body) +| FnBody.unreachable => false end HasIndex diff --git a/library/init/lean/compiler/ir/livevars.lean b/library/init/lean/compiler/ir/livevars.lean index 79e5d604bd..6abac43d24 100644 --- a/library/init/lean/compiler/ir/livevars.lean +++ b/library/init/lean/compiler/ir/livevars.lean @@ -47,17 +47,17 @@ abbrev M := State LocalContext @[inline] def visitExpr (w : Index) (e : Expr) : M Bool := pure (HasIndex.visitExpr w e) partial def visitFnBody (w : Index) : FnBody → M Bool -| FnBody.vdecl x _ v b => visitExpr w v <||> visitFnBody b -| FnBody.jdecl j ys v b => visitFnBody v <||> visitFnBody b -| FnBody.set x _ y b => visitVar w x <||> visitArg w y <||> visitFnBody b -| FnBody.uset x _ y b => visitVar w x <||> visitVar w y <||> visitFnBody b -| FnBody.sset x _ _ y _ b => visitVar w x <||> visitVar w y <||> visitFnBody b -| FnBody.setTag x _ b => visitVar w x <||> visitFnBody b -| FnBody.inc x _ _ b => visitVar w x <||> visitFnBody b -| FnBody.dec x _ _ b => visitVar w x <||> visitFnBody b -| FnBody.del x b => visitVar w x <||> visitFnBody b -| FnBody.mdata _ b => visitFnBody b -| FnBody.jmp j ys => visitArgs w ys <||> do { +| FnBody.vdecl x _ v b => visitExpr w v <||> visitFnBody b +| FnBody.jdecl j ys v b => visitFnBody v <||> visitFnBody b +| FnBody.set x _ y b => visitVar w x <||> visitArg w y <||> visitFnBody b +| FnBody.uset x _ y b => visitVar w x <||> visitVar w y <||> visitFnBody b +| FnBody.sset x _ _ y _ b => visitVar w x <||> visitVar w y <||> visitFnBody b +| FnBody.setTag x _ b => visitVar w x <||> visitFnBody b +| FnBody.inc x _ _ b => visitVar w x <||> visitFnBody b +| FnBody.dec x _ _ b => visitVar w x <||> visitFnBody b +| FnBody.del x b => visitVar w x <||> visitFnBody b +| FnBody.mdata _ b => visitFnBody b +| FnBody.jmp j ys => visitArgs w ys <||> do { ctx ← get; match ctx.getJPBody j with | some b => @@ -68,9 +68,9 @@ partial def visitFnBody (w : Index) : FnBody → M Bool -- `j` must be a local join point. So do nothing since we have already visite its body. pure false } -| FnBody.ret x => visitArg w x -| FnBody.case _ x alts => visitVar w x <||> alts.anyM (fun alt => visitFnBody alt.body) -| FnBody.unreachable => pure false +| FnBody.ret x => visitArg w x +| FnBody.case _ x alts => visitVar w x <||> alts.anyM (fun alt => visitFnBody alt.body) +| FnBody.unreachable => pure false end IsLive @@ -98,8 +98,8 @@ abbrev Collector := LiveVarSet → LiveVarSet @[inline] private def skip : Collector := fun s => s @[inline] private def collectVar (x : VarId) : Collector := fun s => s.insert x private def collectArg : Arg → Collector -| Arg.var x => collectVar x -| irrelevant => skip +| Arg.var x => collectVar x +| irrelevant => skip @[specialize] private def collectArray {α : Type} (as : Array α) (f : α → Collector) : Collector := fun s => as.foldl (fun s a => f a s) s private def collectArgs (as : Array Arg) : Collector := @@ -116,20 +116,20 @@ private def bindParams (ps : Array Param) : Collector := fun s => ps.foldl (fun s p => s.erase p.x) s def collectExpr : Expr → Collector -| Expr.ctor _ ys => collectArgs ys -| Expr.reset _ x => collectVar x -| Expr.reuse x _ _ ys => collectVar x ∘ collectArgs ys -| Expr.proj _ x => collectVar x -| Expr.uproj _ x => collectVar x -| Expr.sproj _ _ x => collectVar x -| Expr.fap _ ys => collectArgs ys -| Expr.pap _ ys => collectArgs ys -| Expr.ap x ys => collectVar x ∘ collectArgs ys -| Expr.box _ x => collectVar x -| Expr.unbox x => collectVar x -| Expr.lit v => skip -| Expr.isShared x => collectVar x -| Expr.isTaggedPtr x => collectVar x +| Expr.ctor _ ys => collectArgs ys +| Expr.reset _ x => collectVar x +| Expr.reuse x _ _ ys => collectVar x ∘ collectArgs ys +| Expr.proj _ x => collectVar x +| Expr.uproj _ x => collectVar x +| Expr.sproj _ _ x => collectVar x +| Expr.fap _ ys => collectArgs ys +| Expr.pap _ ys => collectArgs ys +| Expr.ap x ys => collectVar x ∘ collectArgs ys +| Expr.box _ x => collectVar x +| Expr.unbox x => collectVar x +| Expr.lit v => skip +| Expr.isShared x => collectVar x +| Expr.isTaggedPtr x => collectVar x partial def collectFnBody : FnBody → JPLiveVarMap → Collector | FnBody.vdecl x _ v b, m => collectExpr v ∘ collectFnBody b m ∘ bindVar x diff --git a/library/init/lean/compiler/ir/normids.lean b/library/init/lean/compiler/ir/normids.lean index eafa4a3371..f189b6e5ec 100644 --- a/library/init/lean/compiler/ir/normids.lean +++ b/library/init/lean/compiler/ir/normids.lean @@ -23,14 +23,14 @@ def checkParams (ps : Array Param) : M Bool := ps.allM $ fun p => checkId p.x.idx partial def checkFnBody : FnBody → M Bool -| FnBody.vdecl x _ _ b => checkId x.idx <&&> checkFnBody b -| FnBody.jdecl j ys _ b => checkId j.idx <&&> checkParams ys <&&> checkFnBody b -| FnBody.case _ _ alts => alts.allM $ fun alt => checkFnBody alt.body -| b => if b.isTerminal then pure true else checkFnBody b.body +| FnBody.vdecl x _ _ b => checkId x.idx <&&> checkFnBody b +| FnBody.jdecl j ys _ b => checkId j.idx <&&> checkParams ys <&&> checkFnBody b +| FnBody.case _ _ alts => alts.allM $ fun alt => checkFnBody alt.body +| b => if b.isTerminal then pure true else checkFnBody b.body partial def checkDecl : Decl → M Bool -| Decl.fdecl _ xs _ b => checkParams xs <&&> checkFnBody b -| Decl.extern _ xs _ _ => checkParams xs +| Decl.fdecl _ xs _ b => checkParams xs <&&> checkFnBody b +| Decl.extern _ xs _ _ => checkParams xs end UniqueIds @@ -54,8 +54,8 @@ def normJP (x : JoinPointId) : M JoinPointId := JoinPointId.mk <$> normIndex x.idx def normArg : Arg → M Arg -| Arg.var x => Arg.var <$> normVar x -| other => pure other +| Arg.var x => Arg.var <$> normVar x +| other => pure other def normArgs (as : Array Arg) : M (Array Arg) := fun m => as.map $ fun a => normArg a m @@ -98,29 +98,29 @@ instance MtoN {α} : HasCoe (M α) (N α) := ⟨fun x m => pure $ x m⟩ partial def normFnBody : FnBody → N FnBody -| FnBody.vdecl x t v b => do v ← normExpr v; withVar x $ fun x => FnBody.vdecl x t v <$> normFnBody b -| FnBody.jdecl j ys v b => do +| FnBody.vdecl x t v b => do v ← normExpr v; withVar x $ fun x => FnBody.vdecl x t v <$> normFnBody b +| FnBody.jdecl j ys v b => do (ys, v) ← withParams ys $ fun ys => do { v ← normFnBody v; pure (ys, v) }; withJP j $ fun j => FnBody.jdecl j ys v <$> normFnBody b -| FnBody.set x i y b => do x ← normVar x; y ← normArg y; FnBody.set x i y <$> normFnBody b -| FnBody.uset x i y b => do x ← normVar x; y ← normVar y; FnBody.uset x i y <$> normFnBody b -| FnBody.sset x i o y t b => do x ← normVar x; y ← normVar y; FnBody.sset x i o y t <$> normFnBody b -| FnBody.setTag x i b => do x ← normVar x; FnBody.setTag x i <$> normFnBody b -| FnBody.inc x n c b => do x ← normVar x; FnBody.inc x n c <$> normFnBody b -| FnBody.dec x n c b => do x ← normVar x; FnBody.dec x n c <$> normFnBody b -| FnBody.del x b => do x ← normVar x; FnBody.del x <$> normFnBody b -| FnBody.mdata d b => FnBody.mdata d <$> normFnBody b -| FnBody.case tid x alts => do +| FnBody.set x i y b => do x ← normVar x; y ← normArg y; FnBody.set x i y <$> normFnBody b +| FnBody.uset x i y b => do x ← normVar x; y ← normVar y; FnBody.uset x i y <$> normFnBody b +| FnBody.sset x i o y t b => do x ← normVar x; y ← normVar y; FnBody.sset x i o y t <$> normFnBody b +| FnBody.setTag x i b => do x ← normVar x; FnBody.setTag x i <$> normFnBody b +| FnBody.inc x n c b => do x ← normVar x; FnBody.inc x n c <$> normFnBody b +| FnBody.dec x n c b => do x ← normVar x; FnBody.dec x n c <$> normFnBody b +| FnBody.del x b => do x ← normVar x; FnBody.del x <$> normFnBody b +| FnBody.mdata d b => FnBody.mdata d <$> normFnBody b +| FnBody.case tid x alts => do x ← normVar x; alts ← alts.mmap $ fun alt => alt.mmodifyBody normFnBody; pure $ FnBody.case tid x alts -| FnBody.jmp j ys => FnBody.jmp <$> normJP j <*> normArgs ys -| FnBody.ret x => FnBody.ret <$> normArg x -| FnBody.unreachable => pure FnBody.unreachable +| FnBody.jmp j ys => FnBody.jmp <$> normJP j <*> normArgs ys +| FnBody.ret x => FnBody.ret <$> normArg x +| FnBody.unreachable => pure FnBody.unreachable def normDecl : Decl → N Decl -| Decl.fdecl f xs t b => withParams xs $ fun xs => Decl.fdecl f xs t <$> normFnBody b -| other => pure other +| Decl.fdecl f xs t b => withParams xs $ fun xs => Decl.fdecl f xs t <$> normFnBody b +| other => pure other end NormalizeIds @@ -133,43 +133,43 @@ def Decl.normalizeIds (d : Decl) : Decl := namespace MapVars @[inline] def mapArg (f : VarId → VarId) : Arg → Arg -| Arg.var x => Arg.var (f x) -| a => a +| Arg.var x => Arg.var (f x) +| a => a @[specialize] def mapArgs (f : VarId → VarId) (as : Array Arg) : Array Arg := as.map (mapArg f) @[specialize] def mapExpr (f : VarId → VarId) : Expr → Expr -| Expr.ctor c ys => Expr.ctor c (mapArgs f ys) -| Expr.reset n x => Expr.reset n (f x) -| Expr.reuse x c u ys => Expr.reuse (f x) c u (mapArgs f ys) -| Expr.proj i x => Expr.proj i (f x) -| Expr.uproj i x => Expr.uproj i (f x) -| Expr.sproj n o x => Expr.sproj n o (f x) -| Expr.fap c ys => Expr.fap c (mapArgs f ys) -| Expr.pap c ys => Expr.pap c (mapArgs f ys) -| Expr.ap x ys => Expr.ap (f x) (mapArgs f ys) -| Expr.box t x => Expr.box t (f x) -| Expr.unbox x => Expr.unbox (f x) -| Expr.isShared x => Expr.isShared (f x) -| Expr.isTaggedPtr x => Expr.isTaggedPtr (f x) -| e@(Expr.lit v) => e +| Expr.ctor c ys => Expr.ctor c (mapArgs f ys) +| Expr.reset n x => Expr.reset n (f x) +| Expr.reuse x c u ys => Expr.reuse (f x) c u (mapArgs f ys) +| Expr.proj i x => Expr.proj i (f x) +| Expr.uproj i x => Expr.uproj i (f x) +| Expr.sproj n o x => Expr.sproj n o (f x) +| Expr.fap c ys => Expr.fap c (mapArgs f ys) +| Expr.pap c ys => Expr.pap c (mapArgs f ys) +| Expr.ap x ys => Expr.ap (f x) (mapArgs f ys) +| Expr.box t x => Expr.box t (f x) +| Expr.unbox x => Expr.unbox (f x) +| Expr.isShared x => Expr.isShared (f x) +| Expr.isTaggedPtr x => Expr.isTaggedPtr (f x) +| e@(Expr.lit v) => e @[specialize] partial def mapFnBody (f : VarId → VarId) : FnBody → FnBody -| FnBody.vdecl x t v b => FnBody.vdecl x t (mapExpr f v) (mapFnBody b) -| FnBody.jdecl j ys v b => FnBody.jdecl j ys (mapFnBody v) (mapFnBody b) -| FnBody.set x i y b => FnBody.set (f x) i (mapArg f y) (mapFnBody b) -| FnBody.setTag x i b => FnBody.setTag (f x) i (mapFnBody b) -| FnBody.uset x i y b => FnBody.uset (f x) i (f y) (mapFnBody b) -| FnBody.sset x i o y t b => FnBody.sset (f x) i o (f y) t (mapFnBody b) -| FnBody.inc x n c b => FnBody.inc (f x) n c (mapFnBody b) -| FnBody.dec x n c b => FnBody.dec (f x) n c (mapFnBody b) -| FnBody.del x b => FnBody.del (f x) (mapFnBody b) -| FnBody.mdata d b => FnBody.mdata d (mapFnBody b) -| FnBody.case tid x alts => FnBody.case tid (f x) (alts.map (fun alt => alt.modifyBody mapFnBody)) -| FnBody.jmp j ys => FnBody.jmp j (mapArgs f ys) -| FnBody.ret x => FnBody.ret (mapArg f x) -| FnBody.unreachable => FnBody.unreachable +| FnBody.vdecl x t v b => FnBody.vdecl x t (mapExpr f v) (mapFnBody b) +| FnBody.jdecl j ys v b => FnBody.jdecl j ys (mapFnBody v) (mapFnBody b) +| FnBody.set x i y b => FnBody.set (f x) i (mapArg f y) (mapFnBody b) +| FnBody.setTag x i b => FnBody.setTag (f x) i (mapFnBody b) +| FnBody.uset x i y b => FnBody.uset (f x) i (f y) (mapFnBody b) +| FnBody.sset x i o y t b => FnBody.sset (f x) i o (f y) t (mapFnBody b) +| FnBody.inc x n c b => FnBody.inc (f x) n c (mapFnBody b) +| FnBody.dec x n c b => FnBody.dec (f x) n c (mapFnBody b) +| FnBody.del x b => FnBody.del (f x) (mapFnBody b) +| FnBody.mdata d b => FnBody.mdata d (mapFnBody b) +| FnBody.case tid x alts => FnBody.case tid (f x) (alts.map (fun alt => alt.modifyBody mapFnBody)) +| FnBody.jmp j ys => FnBody.jmp j (mapArgs f ys) +| FnBody.ret x => FnBody.ret (mapArg f x) +| FnBody.unreachable => FnBody.unreachable end MapVars diff --git a/library/init/lean/compiler/ir/pushproj.lean b/library/init/lean/compiler/ir/pushproj.lean index 40c8a9be8f..6b766eeb5a 100644 --- a/library/init/lean/compiler/ir/pushproj.lean +++ b/library/init/lean/compiler/ir/pushproj.lean @@ -53,8 +53,8 @@ partial def FnBody.pushProj : FnBody → FnBody /-- Push projections inside `case` branches. -/ def Decl.pushProj : Decl → Decl -| Decl.fdecl f xs t b => Decl.fdecl f xs t b.pushProj -| other => other +| Decl.fdecl f xs t b => Decl.fdecl f xs t b.pushProj +| other => other end IR end Lean diff --git a/library/init/lean/compiler/ir/rc.lean b/library/init/lean/compiler/ir/rc.lean index e213d09bf9..94c1425df0 100644 --- a/library/init/lean/compiler/ir/rc.lean +++ b/library/init/lean/compiler/ir/rc.lean @@ -160,8 +160,8 @@ ps.foldl b private def isPersistent : Expr → Bool -| Expr.fap c xs => xs.isEmpty -- all global constants are persistent objects -| _ => false +| Expr.fap c xs => xs.isEmpty -- all global constants are persistent objects +| _ => false /- We do not need to consume the projection of a variable that is not consumed -/ private def consumeExpr (m : VarMap) : Expr → Bool diff --git a/library/init/lean/compiler/ir/simpcase.lean b/library/init/lean/compiler/ir/simpcase.lean index dbf2f563d8..43a7c4efb1 100644 --- a/library/init/lean/compiler/ir/simpcase.lean +++ b/library/init/lean/compiler/ir/simpcase.lean @@ -62,8 +62,8 @@ partial def FnBody.simpCase : FnBody → FnBody - Remove `case` if there is only one branch. - Merge most common branches using `Alt.default`. -/ def Decl.simpCase : Decl → Decl -| Decl.fdecl f xs t b => Decl.fdecl f xs t b.simpCase -| other => other +| Decl.fdecl f xs t b => Decl.fdecl f xs t b.simpCase +| other => other end IR end Lean diff --git a/library/init/lean/compiler/namemangling.lean b/library/init/lean/compiler/namemangling.lean index fe0270bb33..a0d056de59 100644 --- a/library/init/lean/compiler/namemangling.lean +++ b/library/init/lean/compiler/namemangling.lean @@ -36,13 +36,13 @@ def String.mangle (s : String) : String := String.mangleAux s.length s.mkIterator "" private def Name.mangleAux : Name → String -| Name.anonymous => "" -| Name.mkString p s => +| Name.anonymous => "" +| Name.mkString p s => let m := String.mangle s; match p with | Name.anonymous => m | _ => Name.mangleAux p ++ "_" ++ m -| Name.mkNumeral p n => Name.mangleAux p ++ "_" ++ toString n ++ "_" +| Name.mkNumeral p n => Name.mangleAux p ++ "_" ++ toString n ++ "_" def Name.mangle (n : Name) (pre : String := "l_") : String := pre ++ Name.mangleAux n diff --git a/library/init/lean/compiler/util.lean b/library/init/lean/compiler/util.lean index f01ab98b32..8df6a18d75 100644 --- a/library/init/lean/compiler/util.lean +++ b/library/init/lean/compiler/util.lean @@ -38,14 +38,14 @@ instance : HasAndthen Visitor := | {found := true, result := true} => {found := true, result := x != y} def visit (x : Name) : Expr → Visitor -| Expr.fvar y => visitFVar y x -| Expr.app f a => visit a >> visit f -| Expr.lam _ _ d b => visit d >> visit b -| Expr.pi _ _ d b => visit d >> visit b -| Expr.elet _ t v b => visit t >> visit v >> visit b -| Expr.mdata _ e => visit e -| Expr.proj _ _ e => visit e -| _ => skip +| Expr.fvar y => visitFVar y x +| Expr.app f a => visit a >> visit f +| Expr.lam _ _ d b => visit d >> visit b +| Expr.pi _ _ d b => visit d >> visit b +| Expr.elet _ t v b => visit t >> visit v >> visit b +| Expr.mdata _ e => visit e +| Expr.proj _ _ e => visit e +| _ => skip end atMostOnce @@ -72,9 +72,9 @@ def isEagerLambdaLiftingName : Name → Bool We use this definition to implement `add_and_compile`. -/ @[export lean.get_decl_names_for_code_gen_core] private def getDeclNamesForCodeGen : Declaration → List Name -| Declaration.defnDecl { name := n, .. } => [n] -| Declaration.mutualDefnDecl defs => defs.map $ fun d => d.name -| _ => [] +| Declaration.defnDecl { name := n, .. } => [n] +| Declaration.mutualDefnDecl defs => defs.map $ fun d => d.name +| _ => [] def checkIsDefinition (env : Environment) (n : Name) : Except String Unit := match env.find n with diff --git a/library/init/lean/declaration.lean b/library/init/lean/declaration.lean index 9aad8c1f30..fb398a4dcb 100644 --- a/library/init/lean/declaration.lean +++ b/library/init/lean/declaration.lean @@ -134,14 +134,14 @@ inductive ConstantInfo namespace ConstantInfo def toConstantVal : ConstantInfo → ConstantVal -| defnInfo {toConstantVal := d, ..} => d -| axiomInfo {toConstantVal := d, ..} => d -| thmInfo {toConstantVal := d, ..} => d -| opaqueInfo {toConstantVal := d, ..} => d -| quotInfo {toConstantVal := d, ..} => d -| inductInfo {toConstantVal := d, ..} => d -| ctorInfo {toConstantVal := d, ..} => d -| recInfo {toConstantVal := d, ..} => d +| defnInfo {toConstantVal := d, ..} => d +| axiomInfo {toConstantVal := d, ..} => d +| thmInfo {toConstantVal := d, ..} => d +| opaqueInfo {toConstantVal := d, ..} => d +| quotInfo {toConstantVal := d, ..} => d +| inductInfo {toConstantVal := d, ..} => d +| ctorInfo {toConstantVal := d, ..} => d +| recInfo {toConstantVal := d, ..} => d def name (d : ConstantInfo) : Name := d.toConstantVal.name @@ -153,18 +153,18 @@ def type (d : ConstantInfo) : Expr := d.toConstantVal.type def value : ConstantInfo → Option Expr -| defnInfo {value := r, ..} => some r -| thmInfo {value := r, ..} => some r.get -| _ => none +| defnInfo {value := r, ..} => some r +| thmInfo {value := r, ..} => some r.get +| _ => none def hasValue : ConstantInfo → Bool -| defnInfo {value := r, ..} => true -| thmInfo {value := r, ..} => true -| _ => false +| defnInfo {value := r, ..} => true +| thmInfo {value := r, ..} => true +| _ => false def hints : ConstantInfo → ReducibilityHints -| defnInfo {hints := r, ..} => r -| _ => ReducibilityHints.opaque +| defnInfo {hints := r, ..} => r +| _ => ReducibilityHints.opaque end ConstantInfo end Lean diff --git a/library/init/lean/elaborator/basic.lean b/library/init/lean/elaborator/basic.lean index 790855082f..dae7529df6 100644 --- a/library/init/lean/elaborator/basic.lean +++ b/library/init/lean/elaborator/basic.lean @@ -98,8 +98,8 @@ do b ← Parser.isValidSyntaxNodeKind k; else throw (IO.userError "failed") def checkSyntaxNodeKindAtNamespaces (k : Name) : List Name → IO Name -| [] => throw (IO.userError "failed") -| n::ns => checkSyntaxNodeKind (n ++ k) <|> checkSyntaxNodeKindAtNamespaces ns +| [] => throw (IO.userError "failed") +| n::ns => checkSyntaxNodeKind (n ++ k) <|> checkSyntaxNodeKindAtNamespaces ns def syntaxNodeKindOfAttrParam (env : Environment) (parserNamespace : Name) (arg : Syntax) : IO SyntaxNodeKind := match attrParamSyntaxToIdentifier arg with @@ -239,10 +239,10 @@ do pos ← getPos stx; logErrorAt pos errorMsg def toMessage : ElabException → Elab Message -| ElabException.msg m => pure m -| ElabException.io e => mkMessage (toString e) -| ElabException.other e => mkMessage e -| ElabException.kernel e => +| ElabException.msg m => pure m +| ElabException.io e => mkMessage (toString e) +| ElabException.other e => mkMessage e +| ElabException.kernel e => match e with | KernelException.other msg => mkMessage msg | _ => mkMessage "kernel exception" -- TODO(pretty print them) @@ -423,9 +423,9 @@ def resolveNamespaceUsingScopes (env : Environment) (n : Name) : List ElabScope | { ns := ns, .. } :: scopes => if isNamespace env (ns ++ n) then some (ns ++ n) else resolveNamespaceUsingScopes scopes def resolveNamespaceUsingOpenDecls (env : Environment) (n : Name) : List OpenDecl → Option Name -| [] => none -| OpenDecl.simple ns :: ds => if isNamespace env (ns ++ n) then some (ns ++ n) else resolveNamespaceUsingOpenDecls ds -| _ :: ds => resolveNamespaceUsingOpenDecls ds +| [] => none +| OpenDecl.simple ns :: ds => if isNamespace env (ns ++ n) then some (ns ++ n) else resolveNamespaceUsingOpenDecls ds +| _ :: ds => resolveNamespaceUsingOpenDecls ds /- Given a name `n` try to find namespace it refers to. The resolution procedure works as follows diff --git a/library/init/lean/elaborator/command.lean b/library/init/lean/elaborator/command.lean index 449256da37..55971e4dc9 100644 --- a/library/init/lean/elaborator/command.lean +++ b/library/init/lean/elaborator/command.lean @@ -36,8 +36,8 @@ fun n => do | none => { scopes := { cmd := "section", header := Name.anonymous, ns := ns } :: s.scopes, .. s } private def getNumEndScopes : Option Name → Nat -| none => 1 -| some n => n.getNumParts +| none => 1 +| some n => n.getNumParts private def checkAnonymousScope : List ElabScope → Bool | { header := Name.anonymous, .. } :: _ => true diff --git a/library/init/lean/environment.lean b/library/init/lean/environment.lean index 0aa9726477..37905f5acb 100644 --- a/library/init/lean/environment.lean +++ b/library/init/lean/environment.lean @@ -514,13 +514,13 @@ namespacesExt.getState env namespace Environment private def isNamespaceName : Name → Bool -| Name.mkString Name.anonymous _ => true -| Name.mkString p _ => isNamespaceName p -| _ => false +| Name.mkString Name.anonymous _ => true +| Name.mkString p _ => isNamespaceName p +| _ => false private def registerNamePrefixes : Environment → Name → Environment -| env, Name.mkString p _ => if isNamespaceName p then registerNamePrefixes (registerNamespace env p) p else env -| env, _ => env +| env, Name.mkString p _ => if isNamespaceName p then registerNamePrefixes (registerNamespace env p) p else env +| env, _ => env @[export lean.environment_add_core] def add (env : Environment) (cinfo : ConstantInfo) : Environment := diff --git a/library/init/lean/expr.lean b/library/init/lean/expr.lean index 48410dc3a4..35f8689652 100644 --- a/library/init/lean/expr.lean +++ b/library/init/lean/expr.lean @@ -82,8 +82,8 @@ constant eqv (a : @& Expr) (b : @& Expr) : Bool := default _ instance : HasBeq Expr := ⟨Expr.eqv⟩ def getAppFn : Expr → Expr -| Expr.app f a => getAppFn f -| e => e +| Expr.app f a => getAppFn f +| e => e def getAppNumArgsAux : Expr → Nat → Nat | Expr.app f a, n => getAppNumArgsAux f (n+1) @@ -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 bf6609f18b..18e854bdb3 100644 --- a/library/init/lean/format.lean +++ b/library/init/lean/format.lean @@ -76,13 +76,13 @@ def spaceUptoLine' : List (Nat × Format) → Nat → SpaceResult | 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 -| w, k, out, (i, nil)::z => be w k out z -| w, k, out, (i, (compose _ f₁ f₂))::z => be w k out ((i, f₁)::(i, f₂)::z) -| w, k, out, (i, (nest n f))::z => be w k out ((i+n, f)::z) -| w, k, out, (i, text s)::z => be w (k + s.length) (out ++ s) z -| w, k, out, (i, line)::z => be w i ((out ++ "\n").pushn ' ' i) z -| w, k, out, (i, choice f₁ f₂)::z => +| w, k, out, [] => out +| w, k, out, (i, nil)::z => be w k out z +| w, k, out, (i, (compose _ f₁ f₂))::z => be w k out ((i, f₁)::(i, f₂)::z) +| w, k, out, (i, (nest n f))::z => be w k out ((i+n, f)::z) +| w, k, out, (i, text s)::z => be w (k + s.length) (out ++ s) z +| w, k, out, (i, line)::z => be w i ((out ++ "\n").pushn ' ' i) z +| w, k, out, (i, choice f₁ f₂)::z => let r := merge w (spaceUptoLine f₁ w) (spaceUptoLine' z w); if r.exceeded then be w k out ((i, f₂)::z) else be w k out ((i, f₁)::z) @@ -144,8 +144,8 @@ def Format.joinSep {α : Type u} [HasFormat α] : List α → Format → Format | 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 +| [] => nil +| a::as => pre ++ format a ++ Format.prefixJoin as def Format.joinSuffix {α : Type u} [HasFormat α] : List α → Format → Format | [], suffix => nil @@ -185,11 +185,11 @@ instance formatHasToString : HasToString Format := ⟨Format.pretty⟩ instance : HasRepr Format := ⟨Format.pretty ∘ Format.repr⟩ def formatDataValue : DataValue → Format -| DataValue.ofString v => format (repr v) -| DataValue.ofBool v => format v -| DataValue.ofName v => "`" ++ format v -| DataValue.ofNat v => format v -| DataValue.ofInt v => format v +| DataValue.ofString v => format (repr v) +| DataValue.ofBool v => format v +| DataValue.ofName v => "`" ++ format v +| DataValue.ofNat v => format v +| DataValue.ofInt v => format v instance dataValueHasFormat : HasFormat DataValue := ⟨formatDataValue⟩ diff --git a/library/init/lean/kvmap.lean b/library/init/lean/kvmap.lean index 2ed13ebbd9..f0f480b7bd 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⟩ diff --git a/library/init/lean/level.lean b/library/init/lean/level.lean index 1225ed9005..692d271030 100644 --- a/library/init/lean/level.lean +++ b/library/init/lean/level.lean @@ -28,48 +28,48 @@ instance levelIsInhabited : Inhabited Level := def Level.one : Level := Level.succ Level.zero def Level.hasParam : Level → Bool -| Level.Param _ => true -| Level.succ l => Level.hasParam l -| Level.max l₁ l₂ => Level.hasParam l₁ || Level.hasParam l₂ -| Level.imax l₁ l₂ => Level.hasParam l₁ || Level.hasParam l₂ -| _ => false +| Level.Param _ => true +| Level.succ l => Level.hasParam l +| Level.max l₁ l₂ => Level.hasParam l₁ || Level.hasParam l₂ +| Level.imax l₁ l₂ => Level.hasParam l₁ || Level.hasParam l₂ +| _ => false def Level.hasMvar : Level → Bool -| Level.mvar _ => true -| Level.succ l => Level.hasParam l -| Level.max l₁ l₂ => Level.hasParam l₁ || Level.hasParam l₂ -| Level.imax l₁ l₂ => Level.hasParam l₁ || Level.hasParam l₂ -| _ => false +| Level.mvar _ => true +| Level.succ l => Level.hasParam l +| Level.max l₁ l₂ => Level.hasParam l₁ || Level.hasParam l₂ +| Level.imax l₁ l₂ => Level.hasParam l₁ || Level.hasParam l₂ +| _ => false def Level.ofNat : Nat → Level -| 0 => Level.zero -| n+1 => Level.succ (Level.ofNat n) +| 0 => Level.zero +| n+1 => Level.succ (Level.ofNat n) def Nat.imax (n m : Nat) : Nat := if m = 0 then 0 else Nat.max n m def Level.toNat : Level → Option Nat -| Level.zero => some 0 -| Level.succ l => Nat.succ <$> Level.toNat l -| Level.max l₁ l₂ => Nat.max <$> Level.toNat l₁ <*> Level.toNat l₂ -| Level.imax l₁ l₂ => Nat.imax <$> Level.toNat l₁ <*> Level.toNat l₂ -| _ => none +| Level.zero => some 0 +| Level.succ l => Nat.succ <$> Level.toNat l +| Level.max l₁ l₂ => Nat.max <$> Level.toNat l₁ <*> Level.toNat l₂ +| Level.imax l₁ l₂ => Nat.imax <$> Level.toNat l₁ <*> Level.toNat l₂ +| _ => none def Level.toOffset : Level → Level × Nat -| Level.zero => (Level.zero, 0) -| Level.succ l => let (l', k) := Level.toOffset l; (l', k+1) -| l => (l, 0) +| Level.zero => (Level.zero, 0) +| Level.succ l => let (l', k) := Level.toOffset l; (l', k+1) +| l => (l, 0) def Level.instantiate (s : Name → Option Level) : Level → Level -| Level.zero => Level.zero -| Level.succ l => Level.succ (Level.instantiate l) -| Level.max l₁ l₂ => Level.max (Level.instantiate l₁) (Level.instantiate l₂) -| Level.imax l₁ l₂ => Level.imax (Level.instantiate l₁) (Level.instantiate l₂) -| l@(Level.Param n) => +| Level.zero => Level.zero +| Level.succ l => Level.succ (Level.instantiate l) +| Level.max l₁ l₂ => Level.max (Level.instantiate l₁) (Level.instantiate l₂) +| Level.imax l₁ l₂ => Level.imax (Level.instantiate l₁) (Level.instantiate l₂) +| l@(Level.Param n) => match s n with | some l' => l' | none => l -| l => l +| l => l @[extern "lean_level_hash"] constant Level.hash (n : @& Level) : USize := default USize @@ -84,25 +84,25 @@ inductive Result | imaxNode : List Result → Result def Result.succ : Result → Result -| Result.offset f k => Result.offset f (k+1) -| Result.num k => Result.num (k+1) -| f => Result.offset f 1 +| Result.offset f k => Result.offset f (k+1) +| Result.num k => Result.num (k+1) +| f => Result.offset f 1 def Result.max : Result → Result → Result -| f, Result.maxNode Fs => Result.maxNode (f::Fs) -| f₁, f₂ => Result.maxNode [f₁, f₂] +| f, Result.maxNode Fs => Result.maxNode (f::Fs) +| f₁, f₂ => Result.maxNode [f₁, f₂] def Result.imax : Result → Result → Result -| f, Result.imaxNode Fs => Result.imaxNode (f::Fs) -| f₁, f₂ => Result.imaxNode [f₁, f₂] +| f, Result.imaxNode Fs => Result.imaxNode (f::Fs) +| f₁, f₂ => Result.imaxNode [f₁, f₂] def parenIfFalse : Format → Bool → Format | f, true => f | f, false => f.paren @[specialize] private def formatLst (fmt : Result → Format) : List Result → Format -| [] => Format.nil -| r::rs => Format.line ++ fmt r ++ formatLst rs +| [] => Format.nil +| r::rs => Format.line ++ fmt r ++ formatLst rs partial def Result.format : Result → Bool → Format | Result.leaf f, _ => f @@ -115,12 +115,12 @@ partial def Result.format : Result → Bool → Format | 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 -| Level.succ l => Result.succ (Level.toResult l) -| Level.max l₁ l₂ => Result.max (Level.toResult l₁) (Level.toResult l₂) -| Level.imax l₁ l₂ => Result.imax (Level.toResult l₁) (Level.toResult l₂) -| Level.Param n => Result.leaf (fmt n) -| Level.mvar n => Result.leaf (fmt n) +| Level.zero => Result.num 0 +| Level.succ l => Result.succ (Level.toResult l) +| Level.max l₁ l₂ => Result.max (Level.toResult l₁) (Level.toResult l₂) +| Level.imax l₁ l₂ => Result.imax (Level.toResult l₁) (Level.toResult l₂) +| Level.Param n => Result.leaf (fmt n) +| Level.mvar n => Result.leaf (fmt n) def Level.format (l : Level) : Format := (Level.toResult l).format true diff --git a/library/init/lean/localcontext.lean b/library/init/lean/localcontext.lean index 5dbbd38a91..dd05e4d599 100644 --- a/library/init/lean/localcontext.lean +++ b/library/init/lean/localcontext.lean @@ -18,36 +18,36 @@ namespace LocalDecl instance : Inhabited LocalDecl := ⟨ldecl (default _) (default _) (default _) (default _) (default _)⟩ def isLet : LocalDecl → Bool -| cdecl _ _ _ _ _ => false -| ldecl _ _ _ _ _ => true +| cdecl _ _ _ _ _ => false +| ldecl _ _ _ _ _ => true def index : LocalDecl → Nat -| cdecl idx _ _ _ _ => idx -| ldecl idx _ _ _ _ => idx +| cdecl idx _ _ _ _ => idx +| ldecl idx _ _ _ _ => idx def name : LocalDecl → Name -| cdecl _ n _ _ _ => n -| ldecl _ n _ _ _ => n +| cdecl _ n _ _ _ => n +| ldecl _ n _ _ _ => n def userName : LocalDecl → Name -| cdecl _ _ n _ _ => n -| ldecl _ _ n _ _ => n +| cdecl _ _ n _ _ => n +| ldecl _ _ n _ _ => n def type : LocalDecl → Expr -| cdecl _ _ _ t _ => t -| ldecl _ _ _ t _ => t +| cdecl _ _ _ t _ => t +| ldecl _ _ _ t _ => t def binderInfo : LocalDecl → BinderInfo -| cdecl _ _ _ _ bi => bi -| ldecl _ _ _ _ _ => BinderInfo.default +| cdecl _ _ _ _ bi => bi +| ldecl _ _ _ _ _ => BinderInfo.default def valueOpt : LocalDecl → Option Expr -| cdecl _ _ _ _ _ => none -| ldecl _ _ _ _ v => some v +| cdecl _ _ _ _ _ => none +| ldecl _ _ _ _ v => some v def value : LocalDecl → Expr -| cdecl _ _ _ _ _ => default _ -| ldecl _ _ _ _ v => v +| cdecl _ _ _ _ _ => default _ +| ldecl _ _ _ _ v => v def updateUserName : LocalDecl → Name → LocalDecl | cdecl index name _ type bi, userName => cdecl index name userName type bi diff --git a/library/init/lean/modifiers.lean b/library/init/lean/modifiers.lean index 083dd2282a..609545c2bc 100644 --- a/library/init/lean/modifiers.lean +++ b/library/init/lean/modifiers.lean @@ -71,8 +71,8 @@ def isPrivateNameExport (n : Name) : Bool := isPrivateName n private def privateToUserNameAux : Name → Name -| Name.mkString p s => Name.mkString (privateToUserNameAux p) s -| _ => Name.anonymous +| Name.mkString p s => Name.mkString (privateToUserNameAux p) s +| _ => Name.anonymous @[export lean.private_to_user_name_core] def privateToUserName (n : Name) : Option Name := @@ -80,8 +80,8 @@ if isPrivateName n then privateToUserNameAux n else none private def privatePrefixAux : Name → Name -| Name.mkString p _ => privatePrefixAux p -| n => n +| Name.mkString p _ => privatePrefixAux p +| n => n @[export lean.private_prefix_core] def privatePrefix (n : Name) : Option Name := diff --git a/library/init/lean/name.lean b/library/init/lean/name.lean index b81c89f2ee..930712c909 100644 --- a/library/init/lean/name.lean +++ b/library/init/lean/name.lean @@ -39,14 +39,14 @@ instance : Hashable Name := ⟨Name.hash⟩ def getPrefix : Name → Name -| anonymous => anonymous -| mkString p s => p -| mkNumeral p s => p +| anonymous => anonymous +| mkString p s => p +| mkNumeral p s => p def getNumParts : Name → Nat -| anonymous => 0 -| mkString p _ => getNumParts p + 1 -| mkNumeral p _ => getNumParts p + 1 +| anonymous => 0 +| mkString p _ => getNumParts p + 1 +| mkNumeral p _ => getNumParts p + 1 def updatePrefix : Name → Name → Name | anonymous, newP => anonymous @@ -54,34 +54,34 @@ def updatePrefix : Name → Name → Name | mkNumeral p s, newP => mkNumeral newP s def components' : Name → List Name -| anonymous => [] -| mkString n s => mkString anonymous s :: components' n -| mkNumeral n v => mkNumeral anonymous v :: components' n +| anonymous => [] +| mkString n s => mkString anonymous s :: components' n +| mkNumeral n v => mkNumeral anonymous v :: components' n def components (n : Name) : List Name := 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 @@ -140,11 +140,11 @@ else quickLtCore n₁ n₂ inferInstanceAs (DecidableRel (fun a b => Name.quickLt a b = true)) def toStringWithSep (sep : String) : Name → String -| anonymous => "[anonymous]" -| mkString anonymous s => s -| mkNumeral anonymous v => toString v -| mkString n s => toStringWithSep n ++ sep ++ s -| mkNumeral n v => toStringWithSep n ++ sep ++ repr v +| anonymous => "[anonymous]" +| mkString anonymous s => s +| mkNumeral anonymous v => toString v +| mkString n s => toStringWithSep n ++ sep ++ s +| mkNumeral n v => toStringWithSep n ++ sep ++ repr v protected def toString : Name → String := toStringWithSep "." diff --git a/library/init/lean/parser/parser.lean b/library/init/lean/parser/parser.lean index 54696f51b1..2f57de1f56 100644 --- a/library/init/lean/parser/parser.lean +++ b/library/init/lean/parser/parser.lean @@ -216,29 +216,29 @@ 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 -| tks => tks +| tokens tks => optTokens tks +| tks => tks def toStr : FirstTokens → String -| epsilon => "epsilon" -| unknown => "unknown" -| tokens tks => toString tks -| optTokens tks => "?" ++ toString tks +| epsilon => "epsilon" +| unknown => "unknown" +| tokens tks => toString tks +| optTokens tks => "?" ++ toString tks instance : HasToString FirstTokens := ⟨toStr⟩ @@ -1179,8 +1179,8 @@ def longestMatchMkResult (startSize : Nat) (s : ParserState) : ParserState := if !s.hasError && s.stackSize > startSize + 1 then s.mkNode choiceKind startSize else s def longestMatchFnAux {k : ParserKind} (startSize : Nat) (startPos : String.Pos) : List (Parser k) → ParserFn k -| [] => fun _ _ s => longestMatchMkResult startSize s -| p::ps => fun a c s => +| [] => fun _ _ s => longestMatchMkResult startSize s +| p::ps => fun a c s => let s := longestMatchStep startSize startPos p.fn a c s; longestMatchFnAux ps a c s @@ -1191,9 +1191,9 @@ let s := p a c s; if s.hasError then s else s.mkLongestNodeAlt startSize def longestMatchFn {k : ParserKind} : List (Parser k) → ParserFn k -| [] => fun _ _ s => s.mkError "longestMatch: empty list" -| [p] => longestMatchFn₁ p.fn -| p::ps => fun a c s => +| [] => fun _ _ s => s.mkError "longestMatch: empty list" +| [p] => longestMatchFn₁ p.fn +| p::ps => fun a c s => let startSize := s.stackSize; let startPos := s.pos; let s := p.fn a c s; diff --git a/library/init/lean/parser/trie.lean b/library/init/lean/parser/trie.lean index 07ddf22d51..c016e7c1de 100644 --- a/library/init/lean/parser/trie.lean +++ b/library/init/lean/parser/trie.lean @@ -85,7 +85,7 @@ def matchPrefix (s : String) (t : Trie α) (i : String.Pos) : String.Pos × Opti matchPrefixAux s t i (i, none) private partial def toStringAux {α : Type} : Trie α → List Format -| Trie.Node val map => map.fold (fun Fs c t => +| Trie.Node val map => map.fold (fun Fs c t => format (repr c) :: (Format.group $ Format.nest 2 $ flip Format.joinSep Format.line $ toStringAux t) :: Fs) [] instance {α : Type} : HasToString (Trie α) := diff --git a/library/init/lean/path.lean b/library/init/lean/path.lean index f783d08284..83042257e4 100644 --- a/library/init/lean/path.lean +++ b/library/init/lean/path.lean @@ -79,14 +79,14 @@ do let fname := System.FilePath.normalizePath fname; | other => pure other def modNameToFileName : Name → String -| Name.mkString Name.anonymous h => h -| Name.mkString p h => modNameToFileName p ++ pathSep ++ h -| Name.anonymous => "" -| Name.mkNumeral p _ => modNameToFileName p +| Name.mkString Name.anonymous h => h +| Name.mkString p h => modNameToFileName p ++ pathSep ++ h +| Name.anonymous => "" +| Name.mkNumeral p _ => modNameToFileName p def addRel (baseDir : String) : Nat → String -| 0 => baseDir -| n+1 => addRel n ++ pathSep ++ ".." +| 0 => baseDir +| n+1 => addRel n ++ pathSep ++ ".." def findLeanFile (modName : Name) (ext : String) : IO String := do diff --git a/library/init/lean/syntax.lean b/library/init/lean/syntax.lean index 27b4ac0c03..495a44b9de 100644 --- a/library/init/lean/syntax.lean +++ b/library/init/lean/syntax.lean @@ -123,20 +123,20 @@ match stx with | _ => hno () def isIdent {α} : Syntax α → Bool -| ident _ _ _ _ => true -| _ => false +| ident _ _ _ _ => true +| _ => false def getId {α} : Syntax α → Name -| ident _ _ val _ => val -| _ => Name.anonymous +| ident _ _ val _ => val +| _ => Name.anonymous def isOfKind {α} : Syntax α → SyntaxNodeKind → Bool | node kind _, k => k == kind | _, _ => false def asNode {α} : Syntax α → SyntaxNode α -| Syntax.node kind args => ⟨Syntax.node kind args, IsNode.mk kind args⟩ -| _ => ⟨Syntax.node nullKind Array.empty, IsNode.mk nullKind Array.empty⟩ +| Syntax.node kind args => ⟨Syntax.node kind args, IsNode.mk kind args⟩ +| _ => ⟨Syntax.node nullKind Array.empty, IsNode.mk nullKind Array.empty⟩ def getNumArgs {α} (stx : Syntax α) : Nat := stx.asNode.getNumArgs @@ -238,19 +238,19 @@ partial def updateTrailing {α} (trailing : Substring) : Syntax α → Syntax α /-- Retrieve the left-most leaf's info in the Syntax tree. -/ partial def getHeadInfo {α} : Syntax α → Option SourceInfo -| atom info _ => info -| ident info _ _ _ => info -| node _ args => args.find getHeadInfo -| _ => none +| atom info _ => info +| ident info _ _ _ => info +| node _ args => args.find getHeadInfo +| _ => none def getPos {α} (stx : Syntax α) : Option String.Pos := SourceInfo.pos <$> stx.getHeadInfo partial def getTailInfo {α} : Syntax α → Option SourceInfo -| atom info _ => info -| ident info _ _ _ => info -| node _ args => args.findRev getTailInfo -| _ => none +| atom info _ => info +| ident info _ _ _ => info +| node _ args => args.findRev getTailInfo +| _ => none @[specialize] private partial def updateLast {α} [Inhabited α] (a : Array α) (f : α → Option α) : Nat → Option (Array α) | i => @@ -263,13 +263,13 @@ partial def getTailInfo {α} : Syntax α → Option SourceInfo | none => updateLast i partial def setTailInfoAux {α} (info : Option SourceInfo) : Syntax α → Option (Syntax α) -| atom _ val => some $ atom info val -| ident _ rawVal val pre => some $ ident info rawVal val pre -| node k args => +| atom _ val => some $ atom info val +| ident _ rawVal val pre => some $ ident info rawVal val pre +| node k args => match updateLast args setTailInfoAux args.size with | some args => some $ node k args | none => none -| stx => none +| stx => none def setTailInfo {α} (stx : Syntax α) (info : Option SourceInfo) : Syntax α := match setTailInfoAux info stx with @@ -295,16 +295,16 @@ partial def reprint {α} : Syntax α → Option String open Lean.Format protected partial def formatStx {α} : Syntax α → Format -| atom info val => format $ repr val -| ident _ _ val pre => format "`" ++ format val -| node kind args => +| atom info val => format $ repr val +| ident _ _ val pre => format "`" ++ format val +| node kind args => if kind = `Lean.Parser.noKind then sbracket $ joinSep (args.toList.map formatStx) line else let shorterName := kind.replacePrefix `Lean.Parser Name.anonymous; paren $ joinSep ((format shorterName) :: args.toList.map formatStx) line -| missing => "" -| other _ => "" +| missing => "" +| other _ => "" instance {α} : HasFormat (Syntax α) := ⟨Syntax.formatStx⟩ instance {α} : HasToString (Syntax α) := ⟨toString ∘ format⟩ diff --git a/library/init/lean/toexpr.lean b/library/init/lean/toexpr.lean index 68662efeb1..0a878ab123 100644 --- a/library/init/lean/toexpr.lean +++ b/library/init/lean/toexpr.lean @@ -21,9 +21,9 @@ instance natToExpr : ToExpr Nat := ⟨fun n => Expr.lit (Literal.natVal n)⟩ instance strToExpr : ToExpr String := ⟨fun s => Expr.lit (Literal.strVal s)⟩ def nameToExprAux : Name → Expr -| Name.anonymous => mkConst `Lean.Name.anonymous -| Name.mkString p s => mkBinCApp `Lean.Name.mkString (nameToExprAux p) (toExpr s) -| Name.mkNumeral p n => mkBinCApp `Lean.Name.mkNumeral (nameToExprAux p) (toExpr n) +| Name.anonymous => mkConst `Lean.Name.anonymous +| Name.mkString p s => mkBinCApp `Lean.Name.mkString (nameToExprAux p) (toExpr s) +| Name.mkNumeral p n => mkBinCApp `Lean.Name.mkNumeral (nameToExprAux p) (toExpr n) instance nameToExpr : ToExpr Name := ⟨nameToExprAux⟩ diff --git a/library/init/lean/trace.lean b/library/init/lean/trace.lean index 284154267d..fc8b6a0f23 100644 --- a/library/init/lean/trace.lean +++ b/library/init/lean/trace.lean @@ -20,7 +20,7 @@ inductive Trace | mk (msg : Message) (subtraces : List Trace) partial def Trace.pp : Trace → Format -| Trace.mk (Message.fromFormat fmt) subtraces => +| Trace.mk (Message.fromFormat fmt) subtraces => fmt ++ Format.nest 2 (Format.join $ subtraces.map (fun t => Format.line ++ t.pp)) namespace Trace diff --git a/tests/playground/patcheqnspace2.lean b/tests/playground/patcheqnspace2.lean new file mode 100644 index 0000000000..2e04b1d22d --- /dev/null +++ b/tests/playground/patcheqnspace2.lean @@ -0,0 +1,56 @@ +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 : Nat := + match p.getTailInfo with + | some info => info.trailing.stopPos - info.trailing.startPos + | none => 0; + 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 → Array Syntax +| ps, i => + let minSpace := getMinTrailingSpace ps i; + if minSpace <= 1 then + ps + else + let delta := minSpace - 1; + ps.map $ fun p => p.modifyArg i $ fun pat => + match pat.getTailInfo with + | some info => pat.setTailInfo (some { trailing := { stopPos := info.trailing.stopPos - delta, .. info.trailing } , .. info }) + | none => pat + +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 (patSize - 1); + 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")