max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(library/init): fix whitspaces before =>

Browse source
This commit is contained in:
Leonardo de Moura 2019-08-09 09:13:49 -07:00
parent 4d913370a7
commit d00019f57e
58 changed files with 970 additions and 914 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

28
library/init/control/combinators.lean
View file

@ -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

8
library/init/control/estate.lean
View file

@ -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⟩

32
library/init/control/except.lean
View file

@ -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)

4
library/init/control/option.lean
View file

@ -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 β))

32
library/init/core.lean
View file

@ -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

4
library/init/data/array/basic.lean
View file

@ -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)

20
library/init/data/assoclist.lean
View file

@ -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)

32
library/init/data/binomialheap/basic.lean
View file

@ -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)

28
library/init/data/int/basic.lean
View file

@ -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

134
library/init/data/list/basic.lean
View file

@ -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 :=

100
library/init/data/nat/basic.lean
View file

@ -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 =>

34
library/init/data/option/basic.lean
View file

@ -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

16
library/init/data/persistentarray/basic.lean
View file

@ -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

4
library/init/data/persistenthashmap/basic.lean
View file

@ -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⟩)

76
library/init/data/rbmap/basic.lean
View file

@ -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

4
library/init/data/rbtree/basic.lean
View file

@ -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

14
library/init/data/repr.lean
View file

@ -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 "\"\""

14
library/init/data/string/basic.lean
View file

@ -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

10
library/init/data/tostring.lean
View file

@ -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⟩

18
library/init/lean/class.lean
View file

@ -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

16
library/init/lean/compiler/constfolding.lean
View file

@ -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₁;

20
library/init/lean/compiler/externattr.lean
View file

@ -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

126
library/init/lean/compiler/ir/basic.lean
View file

@ -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₂

36
library/init/lean/compiler/ir/borrow.lean
View file

@ -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

18
library/init/lean/compiler/ir/boxing.lean
View file

@ -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 :=

62
library/init/lean/compiler/ir/checker.lean
View file

@ -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

4
library/init/lean/compiler/ir/compilerm.lean
View file

@ -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

4
library/init/lean/compiler/ir/elimdead.lean
View file

@ -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

44
library/init/lean/compiler/ir/emitcpp.lean
View file

@ -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

16
library/init/lean/compiler/ir/emitutil.lean
View file

@ -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

8
library/init/lean/compiler/ir/expandresetreuse.lean
View file

@ -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.

68
library/init/lean/compiler/ir/format.lean
View file

@ -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⟩

184
library/init/lean/compiler/ir/freevars.lean
View file

@ -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

60
library/init/lean/compiler/ir/livevars.lean
View file

@ -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

108
library/init/lean/compiler/ir/normids.lean
View file

@ -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

4
library/init/lean/compiler/ir/pushproj.lean
View file

@ -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

4
library/init/lean/compiler/ir/rc.lean
View file

@ -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

4
library/init/lean/compiler/ir/simpcase.lean
View file

@ -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

6
library/init/lean/compiler/namemangling.lean
View file

@ -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

22
library/init/lean/compiler/util.lean
View file

@ -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

32
library/init/lean/declaration.lean
View file

@ -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

18
library/init/lean/elaborator/basic.lean
View file

@ -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

4
library/init/lean/elaborator/command.lean
View file

@ -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

10
library/init/lean/environment.lean
View file

@ -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 :=

10
library/init/lean/expr.lean
View file

@ -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

28
library/init/lean/format.lean
View file

@ -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⟩

8
library/init/lean/kvmap.lean
View file

@ -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⟩

82
library/init/lean/level.lean
View file

@ -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

32
library/init/lean/localcontext.lean
View file

@ -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

8
library/init/lean/modifiers.lean
View file

@ -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 :=

58
library/init/lean/name.lean
View file

@ -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 "."

44
library/init/lean/parser/parser.lean
View file

@ -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;

2
library/init/lean/parser/trie.lean
View file

@ -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 α) :=

12
library/init/lean/path.lean
View file

@ -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

46
library/init/lean/syntax.lean
View file

@ -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 => "<missing>"
| other _ => "<other>"
| missing => "<missing>"
| other _ => "<other>"
instance {α} : HasFormat (Syntax α) := ⟨Syntax.formatStx⟩
instance {α} : HasToString (Syntax α) := ⟨toString ∘ format⟩

6
library/init/lean/toexpr.lean
View file

@ -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⟩

2
library/init/lean/trace.lean
View file

@ -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

56
tests/playground/patcheqnspace2.lean Normal file
View file

@ -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 <file-name>`");
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")