diff --git a/library/init/control/combinators.lean b/library/init/control/combinators.lean index b216228dac..86d45a0b49 100644 --- a/library/init/control/combinators.lean +++ b/library/init/control/combinators.lean @@ -95,14 +95,14 @@ def mfirst {m : Type u → Type v} [Monad m] [Alternative m] {α : Type w} {β : 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 - | true := pure true - | false := mexists as + | 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 - | true := mforall as - | false := pure false + | true => mforall as + | false => pure false end List diff --git a/library/init/control/conditional.lean b/library/init/control/conditional.lean index 598741e4e4..206cdad08f 100644 --- a/library/init/control/conditional.lean +++ b/library/init/control/conditional.lean @@ -17,20 +17,20 @@ instance {α} : HasToBool (Option α) := ⟨Option.toBool⟩ @[macroInline] def bool {β : Type u} {α : Type v} [HasToBool β] (f t : α) (b : β) : α := match toBool b with -| true := t -| false := f +| true => t +| false => f @[macroInline] def orM {m : Type u → Type v} {β : Type u} [Monad m] [HasToBool β] (x y : m β) : m β := do b ← x; match toBool b with - | true := pure b - | false := y + | true => pure b + | false => y @[macroInline] def andM {m : Type u → Type v} {β : Type u} [Monad m] [HasToBool β] (x y : m β) : m β := do b ← x; match toBool b with - | true := y - | false := pure b + | true => y + | false => pure b infixl ` <||> `:30 := orM infixl ` <&&> `:35 := andM diff --git a/library/init/control/estate.lean b/library/init/control/estate.lean index 1803c7259e..b26e42077f 100644 --- a/library/init/control/estate.lean +++ b/library/init/control/estate.lean @@ -54,73 +54,73 @@ variables {ε σ α β : Type u} instance [Inhabited ε] : Inhabited (EState ε σ α) := ⟨fun r => match r with - | ⟨Result.ok _ s, _⟩ := Result.error (default ε) s - | ⟨Result.error _ _, h⟩ := unreachableError h⟩ + | ⟨Result.ok _ s, _⟩ => Result.error (default ε) s + | ⟨Result.error _ _, h⟩ => unreachableError h⟩ @[inline] protected def pure (a : α) : EState ε σ α := fun r => match r with - | ⟨Result.ok _ s, _⟩ := Result.ok a s - | ⟨Result.error _ _, h⟩ := unreachableError h + | ⟨Result.ok _ s, _⟩ => Result.ok a s + | ⟨Result.error _ _, h⟩ => unreachableError h @[inline] protected def set (s : σ) : EState ε σ PUnit := fun r => match r with - | ⟨Result.ok _ _, _⟩ := Result.ok ⟨⟩ s - | ⟨Result.error _ _, h⟩ := unreachableError h + | ⟨Result.ok _ _, _⟩ => Result.ok ⟨⟩ s + | ⟨Result.error _ _, h⟩ => unreachableError h @[inline] protected def get : EState ε σ σ := fun r => match r with - | ⟨Result.ok _ s, _⟩ := Result.ok s s - | ⟨Result.error _ _, h⟩ := unreachableError h + | ⟨Result.ok _ s, _⟩ => Result.ok s s + | ⟨Result.error _ _, h⟩ => unreachableError h @[inline] protected def modify (f : σ → σ) : EState ε σ PUnit := fun r => match r with - | ⟨Result.ok _ s, _⟩ := Result.ok ⟨⟩ (f s) - | ⟨Result.error _ _, h⟩ := unreachableError h + | ⟨Result.ok _ s, _⟩ => Result.ok ⟨⟩ (f s) + | ⟨Result.error _ _, h⟩ => unreachableError h @[inline] protected def throw (e : ε) : EState ε σ α := fun r => match r with - | ⟨Result.ok _ s, _⟩ := Result.error e s - | ⟨Result.error _ _, h⟩ := unreachableError h + | ⟨Result.ok _ s, _⟩ => Result.error e s + | ⟨Result.error _ _, h⟩ => unreachableError h @[inline] protected def catch (x : EState ε σ α) (handle : ε → EState ε σ α) : EState ε σ α := fun r => match x r with - | Result.error e s := handle e (resultOk.mk ⟨⟩ s) - | ok := ok + | Result.error e s => handle e (resultOk.mk ⟨⟩ s) + | ok => ok @[inline] protected def orelse (x₁ x₂ : EState ε σ α) : EState ε σ α := fun r => match x₁ r with - | Result.error _ s := x₂ (resultOk.mk ⟨⟩ s) - | ok := ok + | Result.error _ s => x₂ (resultOk.mk ⟨⟩ s) + | ok => ok /-- Alternative orelse operator that allows to select which exception should be used. The default is to use the first exception since the standard `orelse` uses the second. -/ @[inline] protected def orelse' (x₁ x₂ : EState ε σ α) (useFirstEx := true) : EState ε σ α := fun r => match x₁ r with - | Result.error e₁ s₁ := + | Result.error e₁ s₁ => match x₂ (resultOk.mk ⟨⟩ s₁) with - | Result.error e₂ s₂ := Result.error (if useFirstEx then e₁ else e₂) s₂ - | ok := ok - | ok := ok + | Result.error e₂ s₂ => Result.error (if useFirstEx then e₁ else e₂) s₂ + | ok => ok + | ok => ok @[inline] def adaptExcept {ε' : Type u} [HasLift ε ε'] (x : EState ε σ α) : EState ε' σ α := fun r => match x r with - | Result.error e s := Result.error (lift e) s - | Result.ok a s := Result.ok a s + | Result.error e s => Result.error (lift e) s + | Result.ok a s => Result.ok a s @[inline] protected def bind (x : EState ε σ α) (f : α → EState ε σ β) : EState ε σ β := fun r => match x r with - | Result.ok a s := f a (resultOk.mk ⟨⟩ s) - | Result.error e s := Result.error e s + | Result.ok a s => f a (resultOk.mk ⟨⟩ s) + | Result.error e s => Result.error e s @[inline] protected def map (f : α → β) (x : EState ε σ α) : EState ε σ β := fun r => match x r with - | Result.ok a s := Result.ok (f a) s - | Result.error e s := Result.error e s + | Result.ok a s => Result.ok (f a) s + | Result.error e s => Result.error e s @[inline] protected def seqRight (x : EState ε σ α) (y : EState ε σ β) : EState ε σ β := fun r => match x r with - | Result.ok _ s := y (resultOk.mk ⟨⟩ s) - | Result.error e s := Result.error e s + | Result.ok _ s => y (resultOk.mk ⟨⟩ s) + | Result.error e s => Result.error e s instance : Monad (EState ε σ) := { bind := @EState.bind _ _, pure := @EState.pure _ _, map := @EState.map _ _, seqRight := @EState.seqRight _ _ } @@ -139,7 +139,7 @@ x (resultOk.mk ⟨⟩ s) @[inline] def run' (x : EState ε σ α) (s : σ) : Option α := match run x s with -| Result.ok v _ := some v -| Result.error _ _ := none +| Result.ok v _ => some v +| Result.error _ _ => none end EState diff --git a/library/init/control/except.lean b/library/init/control/except.lean index 7c0a763b87..fd629b496f 100644 --- a/library/init/control/except.lean +++ b/library/init/control/except.lean @@ -51,8 +51,8 @@ Except.ok a @[inline] protected def bind {α β : Type v} (ma : Except ε α) (f : α → Except ε β) : Except ε β := match ma with -| (Except.error err) := Except.error err -| (Except.ok v) := f v +| (Except.error err) => Except.error err +| (Except.ok v) => f v @[inline] protected def toBool {α : Type v} : Except ε α → Bool | (Except.ok _) := true @@ -64,8 +64,8 @@ match ma with @[inline] protected def catch {α : Type u} (ma : Except ε α) (handle : ε → Except ε α) : Except ε α := match ma with -| Except.ok a := Except.ok a -| Except.error e := handle e +| Except.ok a => Except.ok a +| Except.error e => handle e instance : Monad (Except ε) := { pure := @Except.return _, bind := @Except.bind _, map := @Except.map _ } @@ -95,8 +95,8 @@ ExceptT.mk $ ma >>= ExceptT.bindCont f @[inline] protected def map {α β : Type u} (f : α → β) (x : ExceptT ε m α) : ExceptT ε m β := ExceptT.mk $ x >>= fun a => match a with - | (Except.ok a) := pure $ Except.ok (f a) - | (Except.error e) := pure $ Except.error e + | (Except.ok a) => pure $ Except.ok (f a) + | (Except.error e) => pure $ Except.error e @[inline] protected def lift {α : Type u} (t : m α) : ExceptT ε m α := ExceptT.mk $ Except.ok <$> t @@ -109,8 +109,8 @@ instance : HasMonadLift m (ExceptT ε m) := @[inline] protected def catch {α : Type u} (ma : ExceptT ε m α) (handle : ε → ExceptT ε m α) : ExceptT ε m α := ExceptT.mk $ ma >>= fun res => match res with - | Except.ok a := pure (Except.ok a) - | Except.error e := (handle e) + | Except.ok a => pure (Except.ok a) + | Except.error e => (handle e) instance (m') [Monad m'] : MonadFunctor m m' (ExceptT ε m) (ExceptT ε m') := ⟨fun _ f x => f x⟩ diff --git a/library/init/core.lean b/library/init/core.lean index d653666dad..c1ac762b8f 100644 --- a/library/init/core.lean +++ b/library/init/core.lean @@ -917,8 +917,8 @@ Decidable.casesOn h (fun h => h₄) (fun h => False.rec _ (h₃ h)) @[macroInline] def byCases {q : Sort u} [s : Decidable p] (h1 : p → q) (h2 : ¬p → q) : q := match s with -| isTrue h := h1 h -| isFalse h := h2 h +| isTrue h => h1 h +| isFalse h => h2 h theorem em (p : Prop) [Decidable p] : p ∨ ¬p := byCases Or.inl Or.inr @@ -935,9 +935,9 @@ Iff.intro ofNotNot notNotIntro theorem notAndIffOrNot (p q : Prop) [d₁ : Decidable p] [d₂ : Decidable q] : ¬ (p ∧ q) ↔ ¬ p ∨ ¬ q := Iff.intro (fun h => match d₁, d₂ with - | isTrue h₁, isTrue h₂ := absurd (And.intro h₁ h₂) h - | _, isFalse h₂ := Or.inr h₂ - | isFalse h₁, _ := Or.inl h₁) + | isTrue h₁, isTrue h₂ => absurd (And.intro h₁ h₂) h + | _, isFalse h₂ => Or.inr h₂ + | isFalse h₁, _ => Or.inl h₁) (fun (h) ⟨hp, hq⟩ => Or.elim h (fun h => h hp) (fun h => h hq)) end Decidable @@ -995,46 +995,46 @@ end @[inline] instance {α : Sort u} [DecidableEq α] (a b : α) : Decidable (a ≠ b) := match decEq a b with -| isTrue h := isFalse $ fun h' => absurd h h' -| isFalse h := isTrue h +| isTrue h => isFalse $ fun h' => absurd h h' +| isFalse h => isTrue h theorem Bool.falseNeTrue (h : false = true) : False := Bool.noConfusion h instance : DecidableEq Bool := {decEq := fun a b => match a, b with - | false, false := isTrue rfl - | false, true := isFalse Bool.falseNeTrue - | true, false := isFalse (Ne.symm Bool.falseNeTrue) - | true, true := isTrue rfl} + | false, false => isTrue rfl + | false, true => isFalse Bool.falseNeTrue + | true, false => isFalse (Ne.symm Bool.falseNeTrue) + | true, true => isTrue rfl} /- if-then-else expression theorems -/ theorem ifPos {c : Prop} [h : Decidable c] (hc : c) {α : Sort u} {t e : α} : (ite c t e) = t := match h with -| (isTrue hc) := rfl -| (isFalse hnc) := absurd hc hnc +| (isTrue hc) => rfl +| (isFalse hnc) => absurd hc hnc theorem ifNeg {c : Prop} [h : Decidable c] (hnc : ¬c) {α : Sort u} {t e : α} : (ite c t e) = e := match h with -| (isTrue hc) := absurd hc hnc -| (isFalse hnc) := rfl +| (isTrue hc) => absurd hc hnc +| (isFalse hnc) => rfl -- Remark: dite and ite are "defally equal" when we ignore the proofs. theorem difEqIf (c : Prop) [h : Decidable c] {α : Sort u} (t : α) (e : α) : dite c (fun h => t) (fun h => e) = ite c t e := match h with -| (isTrue hc) := rfl -| (isFalse hnc) := rfl +| (isTrue hc) => rfl +| (isFalse hnc) => rfl instance {c t e : Prop} [dC : Decidable c] [dT : Decidable t] [dE : Decidable e] : Decidable (if c then t else e) := match dC with -| (isTrue hc) := dT -| (isFalse hc) := dE +| (isTrue hc) => dT +| (isFalse hc) => dE instance {c : Prop} {t : c → Prop} {e : ¬c → Prop} [dC : Decidable c] [dT : ∀ h, Decidable (t h)] [dE : ∀ h, Decidable (e h)] : Decidable (if h : c then t h else e h) := match dC with -| (isTrue hc) := dT hc -| (isFalse hc) := dE hc +| (isTrue hc) => dT hc +| (isFalse hc) => dE hc /-- Universe lifting operation -/ structure ULift.{r, s} (α : Type s) : Type (max s r) := @@ -1121,23 +1121,23 @@ instance subsingletonProp (p : Prop) : Subsingleton p := ⟨fun a b => proofIrrel a b⟩ instance (p : Prop) : Subsingleton (Decidable p) := -Subsingleton.intro (fun d₁ => +Subsingleton.intro $ fun d₁ => match d₁ with - | (isTrue t₁) := (fun d₂ => + | (isTrue t₁) => fun d₂ => match d₂ with - | (isTrue t₂) := Eq.recOn (proofIrrel t₁ t₂) rfl - | (isFalse f₂) := absurd t₁ f₂) - | (isFalse f₁) := (fun d₂ => + | (isTrue t₂) => Eq.recOn (proofIrrel t₁ t₂) rfl + | (isFalse f₂) => absurd t₁ f₂ + | (isFalse f₁) => fun d₂ => match d₂ with - | (isTrue t₂) := absurd t₂ f₁ - | (isFalse f₂) := Eq.recOn (proofIrrel f₁ f₂) rfl)) + | (isTrue t₂) => absurd t₂ f₁ + | (isFalse f₂) => Eq.recOn (proofIrrel f₁ f₂) rfl protected theorem recSubsingleton {p : Prop} [h : Decidable p] {h₁ : p → Sort u} {h₂ : ¬p → Sort u} [h₃ : ∀ (h : p), Subsingleton (h₁ h)] [h₄ : ∀ (h : ¬p), Subsingleton (h₂ h)] : Subsingleton (Decidable.casesOn h h₂ h₁) := match h with -| (isTrue h) := h₃ h -| (isFalse h) := h₄ h +| (isTrue h) => h₃ h +| (isFalse h) => h₄ h section relation variables {α : Sort u} {β : Sort v} (r : β → β → Prop) @@ -1254,12 +1254,14 @@ instance Sum.inhabitedRight [h : Inhabited β] : Inhabited (α ⊕ β) := instance {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] : DecidableEq (α ⊕ β) := {decEq := fun a b => match a, b with - | (Sum.inl a), (Sum.inl b) := if h : a = b then isTrue (h ▸ rfl) - else isFalse (fun h' => Sum.noConfusion h' (fun h' => absurd h' h)) - | (Sum.inr a), (Sum.inr b) := if h : a = b then isTrue (h ▸ rfl) - else isFalse (fun h' => Sum.noConfusion h' (fun h' => absurd h' h)) - | (Sum.inr a), (Sum.inl b) := isFalse (fun h => Sum.noConfusion h) - | (Sum.inl a), (Sum.inr b) := isFalse (fun h => Sum.noConfusion h)} + | (Sum.inl a), (Sum.inl b) => + if h : a = b then isTrue (h ▸ rfl) + else isFalse (fun h' => Sum.noConfusion h' (fun h' => absurd h' h)) + | (Sum.inr a), (Sum.inr b) => + if h : a = b then isTrue (h ▸ rfl) + else isFalse (fun h' => Sum.noConfusion h' (fun h' => absurd h' h)) + | (Sum.inr a), (Sum.inl b) => isFalse (fun h => Sum.noConfusion h) + | (Sum.inl a), (Sum.inr b) => isFalse (fun h => Sum.noConfusion h)} end /- Product -/ @@ -1273,11 +1275,11 @@ instance [Inhabited α] [Inhabited β] : Inhabited (Prod α β) := instance [DecidableEq α] [DecidableEq β] : DecidableEq (α × β) := {decEq := fun ⟨a, b⟩ ⟨a', b'⟩ => match (decEq a a') with - | (isTrue e₁) := + | (isTrue e₁) => (match (decEq b b') with - | (isTrue e₂) := isTrue (Eq.recOn e₁ (Eq.recOn e₂ rfl)) - | (isFalse n₂) := isFalse (fun h => Prod.noConfusion h (fun e₁' e₂' => absurd e₂' n₂))) - | (isFalse n₁) := isFalse (fun h => Prod.noConfusion h (fun e₁' e₂' => absurd e₁' n₁))} + | (isTrue e₂) => isTrue (Eq.recOn e₁ (Eq.recOn e₂ rfl)) + | (isFalse n₂) => isFalse (fun h => Prod.noConfusion h (fun e₁' e₂' => absurd e₂' n₂))) + | (isFalse n₁) => isFalse (fun h => Prod.noConfusion h (fun e₁' e₂' => absurd e₁' n₁))} instance [HasLess α] [HasLess β] : HasLess (α × β) := ⟨fun s t => s.1 < t.1 ∨ (s.1 = t.1 ∧ s.2 < t.2)⟩ @@ -1348,15 +1350,15 @@ variables {α : Sort u} [Setoid α] theorem refl (a : α) : a ≈ a := match Setoid.iseqv α with -| ⟨hRefl, hSymm, hTrans⟩ := hRefl a +| ⟨hRefl, hSymm, hTrans⟩ => hRefl a theorem symm {a b : α} (hab : a ≈ b) : b ≈ a := match Setoid.iseqv α with -| ⟨hRefl, hSymm, hTrans⟩ := hSymm hab +| ⟨hRefl, hSymm, hTrans⟩ => hSymm hab theorem trans {a b c : α} (hab : a ≈ b) (hbc : b ≈ c) : a ≈ c := match Setoid.iseqv α with -| ⟨hRefl, hSymm, hTrans⟩ := hTrans hab hbc +| ⟨hRefl, hSymm, hTrans⟩ => hTrans hab hbc end Setoid /- Propositional extensionality -/ @@ -1615,8 +1617,8 @@ instance {α : Sort u} {s : Setoid α} [d : ∀ a b : α, Decidable (a ≈ b)] : Quotient.recOnSubsingleton₂ q₁ q₂ (fun a₁ a₂ => match (d a₁ a₂) with - | (isTrue h₁) := isTrue (Quotient.sound h₁) - | (isFalse h₂) := isFalse (fun h => absurd (Quotient.exact h) h₂))} + | (isTrue h₁) => isTrue (Quotient.sound h₁) + | (isFalse h₂) => isFalse (fun h => absurd (Quotient.exact h) h₂))} /- Function extensionality -/ @@ -1761,8 +1763,8 @@ noncomputable def typeDecidableEq (α : Sort u) : DecidableEq α := noncomputable def typeDecidable (α : Sort u) : PSum α (α → False) := match (propDecidable (Nonempty α)) with -| (isTrue hp) := PSum.inl (@Inhabited.default _ (inhabitedOfNonempty hp)) -| (isFalse hn) := PSum.inr (fun a => absurd (Nonempty.intro a) hn) +| (isTrue hp) => PSum.inl (@Inhabited.default _ (inhabitedOfNonempty hp)) +| (isFalse hn) => PSum.inr (fun a => absurd (Nonempty.intro a) hn) noncomputable def strongIndefiniteDescription {α : Sort u} (p : α → Prop) (h : Nonempty α) : {x : α // Exists (fun y : α => p y) → p x} := diff --git a/library/init/data/array/basic.lean b/library/init/data/array/basic.lean index 009bca98f2..128f7423ce 100644 --- a/library/init/data/array/basic.lean +++ b/library/init/data/array/basic.lean @@ -179,8 +179,8 @@ miterate₂ a₁ a₂ b (fun _ a₁ a₂ b => f b a₁ a₂) let idx : Fin a.size := ⟨i, h⟩; do r ← f (a.fget idx); match r with - | some v := pure r - | none := mfindAux (i+1) + | some v => pure r + | none => mfindAux (i+1) else pure none @[inline] def mfind (a : Array α) (f : α → m (Option β)) : m (Option β) := @@ -218,8 +218,8 @@ variables {m : Type → Type v} [Monad m] let idx : Fin a.size := ⟨i, h⟩; do b ← p (a.fget idx); match b with - | true := pure true - | false := anyMAux (i+1) + | true => pure true + | false => anyMAux (i+1) else pure false @[inline] def anyM (a : Array α) (p : α → m Bool) : m Bool := @@ -342,8 +342,8 @@ partial def isEqvAux (a b : Array α) (hsz : a.size = b.size) (p : α → α → let aidx : Fin a.size := ⟨i, h⟩; let bidx : Fin b.size := ⟨i, hsz ▸ h⟩; match p (a.fget aidx) (b.fget bidx) with - | true := isEqvAux (i+1) - | false := false + | true => isEqvAux (i+1) + | false => false else true diff --git a/library/init/data/assoclist.lean b/library/init/data/assoclist.lean index b05bff2191..821ce81298 100644 --- a/library/init/data/assoclist.lean +++ b/library/init/data/assoclist.lean @@ -25,8 +25,8 @@ Id.run (mfoldl f d as) def find [HasBeq α] (a : α) : AssocList α β → Option β | nil := none | (cons k v es) := match k == a with - | true := some v - | false := find es + | true => some v + | false => find es def contains [HasBeq α] (a : α) : AssocList α β → Bool | nil := false @@ -35,13 +35,13 @@ def contains [HasBeq α] (a : α) : AssocList α β → Bool def replace [HasBeq α] (a : α) (b : β) : AssocList α β → AssocList α β | nil := nil | (cons k v es) := match k == a with - | true := cons a b es - | false := cons k v (replace es) + | 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 - | true := es - | false := cons k v (erase es) + | true => es + | false => cons k v (erase es) end AssocList diff --git a/library/init/data/hashmap/basic.lean b/library/init/data/hashmap/basic.lean index 82f98bdb66..01ecb8e519 100644 --- a/library/init/data/hashmap/basic.lean +++ b/library/init/data/hashmap/basic.lean @@ -28,8 +28,8 @@ let n := if nbuckets = 0 then 8 else nbuckets; have p₂ : n = (if nbuckets = 0 then 8 else nbuckets) from rfl; have p₃ : (if nbuckets = 0 then 8 else nbuckets) > 0 from match nbuckets with - | 0 := Nat.zeroLtSucc _ - | (Nat.succ x) := Nat.zeroLtSucc _; + | 0 => Nat.zeroLtSucc _ + | (Nat.succ x) => Nat.zeroLtSucc _; transRelRight Greater (Eq.trans p₁ p₂) p₃ ⟩ } namespace HashMapImp @@ -56,13 +56,13 @@ foldBuckets m.buckets d f def find [HasBeq α] [Hashable α] (m : HashMapImp α β) (a : α) : Option β := match m with -| ⟨_, buckets⟩ := +| ⟨_, buckets⟩ => let ⟨i, h⟩ := mkIdx buckets.property (hash a); (buckets.val.uget i h).find a def contains [HasBeq α] [Hashable α] (m : HashMapImp α β) (a : α) : Bool := match m with -| ⟨_, buckets⟩ := +| ⟨_, buckets⟩ => let ⟨i, h⟩ := mkIdx buckets.property (hash a); (buckets.val.uget i h).contains a @@ -88,7 +88,7 @@ let new_buckets : HashMapBucket α β := ⟨mkArray nbuckets AssocList.nil, aux def insert [HasBeq α] [Hashable α] (m : HashMapImp α β) (a : α) (b : β) : HashMapImp α β := match m with -| ⟨size, buckets⟩ := +| ⟨size, buckets⟩ => let ⟨i, h⟩ := mkIdx buckets.property (hash a); let bkt := buckets.val.uget i h; if bkt.contains a @@ -102,7 +102,7 @@ match m with def erase [HasBeq α] [Hashable α] (m : HashMapImp α β) (a : α) : HashMapImp α β := match m with -| ⟨ size, buckets ⟩ := +| ⟨ size, buckets ⟩ => let ⟨i, h⟩ := mkIdx buckets.property (hash a); let bkt := buckets.val.uget i h; if bkt.contains a then ⟨size - 1, buckets.update i (bkt.erase a) h⟩ @@ -134,31 +134,31 @@ instance : HasEmptyc (HashMap α β) := @[inline] def insert (m : HashMap α β) (a : α) (b : β) : HashMap α β := match m with -| ⟨ m, hw ⟩ := ⟨ m.insert a b, WellFormed.insertWff m a b hw ⟩ +| ⟨ m, hw ⟩ => ⟨ m.insert a b, WellFormed.insertWff m a b hw ⟩ @[inline] def erase (m : HashMap α β) (a : α) : HashMap α β := match m with -| ⟨ m, hw ⟩ := ⟨ m.erase a, WellFormed.eraseWff m a hw ⟩ +| ⟨ m, hw ⟩ => ⟨ m.erase a, WellFormed.eraseWff m a hw ⟩ @[inline] def find (m : HashMap α β) (a : α) : Option β := match m with -| ⟨ m, _ ⟩ := m.find a +| ⟨ m, _ ⟩ => m.find a @[inline] def contains (m : HashMap α β) (a : α) : Bool := match m with -| ⟨ m, _ ⟩ := m.contains a +| ⟨ m, _ ⟩ => m.contains a @[inline] def mfold {δ : Type w} {m : Type w → Type w} [Monad m] (f : δ → α → β → m δ) (d : δ) (h : HashMap α β) : m δ := match h with -| ⟨ h, _ ⟩ := h.mfold f d +| ⟨ h, _ ⟩ => h.mfold f d @[inline] def fold {δ : Type w} (f : δ → α → β → δ) (d : δ) (m : HashMap α β) : δ := match m with -| ⟨ m, _ ⟩ := m.fold f d +| ⟨ m, _ ⟩ => m.fold f d @[inline] def size (m : HashMap α β) : Nat := match m with -| ⟨ {size := sz, ..}, _ ⟩ := sz +| ⟨ {size := sz, ..}, _ ⟩ => sz @[inline] def empty (m : HashMap α β) : Bool := m.size = 0 diff --git a/library/init/data/int/basic.lean b/library/init/data/int/basic.lean index cb047036fa..f10bceaa98 100644 --- a/library/init/data/int/basic.lean +++ b/library/init/data/int/basic.lean @@ -34,29 +34,29 @@ def negOfNat : Nat → Int @[extern cpp "lean::int_neg"] protected def neg (n : @& Int) : Int := match n with -| ofNat n := negOfNat n -| negSucc n := succ n +| ofNat n => negOfNat n +| negSucc n => succ n def subNatNat (m n : Nat) : Int := match (n - m : Nat) with -| 0 := ofNat (m - n) -- m ≥ n -| (succ k) := negSucc k +| 0 => ofNat (m - n) -- m ≥ n +| (succ k) => negSucc k @[extern cpp "lean::int_add"] protected def add (m n : @& Int) : Int := match m, n with -| ofNat m, ofNat n := ofNat (m + n) -| ofNat m, negSucc n := subNatNat m (succ n) -| negSucc m, ofNat n := subNatNat n (succ m) -| negSucc m, negSucc n := negSucc (m + n) +| ofNat m, ofNat n => ofNat (m + n) +| ofNat m, negSucc n => subNatNat m (succ n) +| negSucc m, ofNat n => subNatNat n (succ m) +| negSucc m, negSucc n => negSucc (m + n) @[extern cpp "lean::int_mul"] protected def mul (m n : @& Int) : Int := match m, n with -| ofNat m, ofNat n := ofNat (m * n) -| ofNat m, negSucc n := negOfNat (m * succ n) -| negSucc m, ofNat n := negOfNat (succ m * n) -| negSucc m, negSucc n := ofNat (succ m * succ n) +| ofNat m, ofNat n => ofNat (m * n) +| ofNat m, negSucc n => negOfNat (m * succ n) +| negSucc m, ofNat n => negOfNat (succ m * n) +| negSucc m, negSucc n => ofNat (succ m * succ n) instance : HasNeg Int := ⟨Int.neg⟩ instance : HasAdd Int := ⟨Int.add⟩ @@ -82,14 +82,14 @@ instance : HasLess Int := ⟨Int.Less⟩ @[extern cpp "lean::int_dec_eq"] protected def decEq (a b : @& Int) : Decidable (a = b) := match a, b with - | ofNat a, ofNat b := match decEq a b with - | isTrue h := isTrue $ h ▸ rfl - | isFalse h := isFalse $ fun h' => Int.noConfusion h' (fun h' => absurd h' h) - | negSucc a, negSucc b := match decEq a b with - | isTrue h := isTrue $ h ▸ rfl - | isFalse h := isFalse $ fun h' => Int.noConfusion h' (fun h' => absurd h' h) - | ofNat a, negSucc b := isFalse $ fun h => Int.noConfusion h - | negSucc a, ofNat b := isFalse $ fun h => Int.noConfusion h + | ofNat a, ofNat b => match decEq a b with + | isTrue h => isTrue $ h ▸ rfl + | isFalse h => isFalse $ fun h' => Int.noConfusion h' (fun h' => absurd h' h) + | negSucc a, negSucc b => match decEq a b with + | isTrue h => isTrue $ h ▸ rfl + | isFalse h => isFalse $ fun h' => Int.noConfusion h' (fun h' => absurd h' h) + | ofNat a, negSucc b => isFalse $ fun h => Int.noConfusion h + | negSucc a, ofNat b => isFalse $ fun h => Int.noConfusion h instance Int.DecidableEq : DecidableEq Int := {decEq := Int.decEq} @@ -97,8 +97,8 @@ instance Int.DecidableEq : DecidableEq Int := @[extern cpp "lean::int_dec_nonneg"] private def decNonneg (m : @& Int) : Decidable (NonNeg m) := match m with -| ofNat m := isTrue $ NonNeg.mk m -| negSucc m := isFalse $ fun h => match h with end +| ofNat m => isTrue $ NonNeg.mk m +| negSucc m => isFalse $ fun h => match h with end @[extern cpp "lean::int_dec_le"] instance decLe (a b : @& Int) : Decidable (a ≤ b) := @@ -111,8 +111,8 @@ decNonneg _ @[extern cpp "lean::nat_abs"] def natAbs (m : @& Int) : Nat := match m with -| ofNat m := m -| negSucc m := m.succ +| ofNat m => m +| negSucc m => m.succ protected def repr : Int → String | (ofNat m) := Nat.repr m diff --git a/library/init/data/list/basic.lean b/library/init/data/list/basic.lean index b7f4f28b53..ae6e93aa62 100644 --- a/library/init/data/list/basic.lean +++ b/library/init/data/list/basic.lean @@ -22,11 +22,11 @@ protected def hasDecEq [DecidableEq α] : ∀ a b : List α, Decidable (a = b) | [] (b::bs) := isFalse (fun h => List.noConfusion h) | (a::as) (b::bs) := match decEq a b with - | isTrue hab := + | isTrue hab => match hasDecEq as bs with - | isTrue habs := isTrue (Eq.subst hab (Eq.subst habs rfl)) - | isFalse nabs := isFalse (fun h => List.noConfusion h (fun _ habs => absurd habs nabs)) - | isFalse nab := isFalse (fun h => List.noConfusion h (fun hab _ => absurd hab nab)) + | isTrue habs => isTrue (Eq.subst hab (Eq.subst habs rfl)) + | isFalse nabs => isFalse (fun h => List.noConfusion h (fun _ habs => absurd habs nabs)) + | isFalse nab => isFalse (fun h => List.noConfusion h (fun hab _ => absurd hab nab)) instance [DecidableEq α] : DecidableEq (List α) := {decEq := List.hasDecEq} @@ -93,8 +93,8 @@ instance decidableMem [DecidableEq α] (a : α) : ∀ (l : List α), Decidable ( | (b::bs) := if h₁ : a = b then isTrue (h₁.symm ▸ Mem.eqHead b bs) else match decidableMem bs with - | isTrue h₂ := isTrue (Mem.inTail _ h₂) - | isFalse h₂ := isFalse (notMem h₁ h₂) + | isTrue h₂ => isTrue (Mem.inTail _ h₂) + | isFalse h₂ => isFalse (notMem h₁ h₂) instance : HasEmptyc (List α) := ⟨List.nil⟩ @@ -154,14 +154,14 @@ def join : List (List α) → List α | [] := [] | (a::as) := match f a with - | none := filterMap as - | some b := b :: filterMap as + | none => filterMap as + | some b => b :: filterMap as @[specialize] def filterAux (p : α → Bool) : List α → List α → List α | [] rs := rs.reverse | (a::as) rs := match p a with - | true := filterAux as (a::rs) - | false := filterAux as rs + | true => filterAux as (a::rs) + | false => filterAux as rs @[inline] def filter (p : α → Bool) (as : List α) : List α := filterAux p as [] @@ -170,8 +170,8 @@ filterAux p as [] | [] (bs, cs) := (bs.reverse, cs.reverse) | (a::as) (bs, cs) := match p a with - | true := partitionAux as (a::bs, cs) - | false := partitionAux as (bs, a::cs) + | true => partitionAux as (a::bs, cs) + | false => partitionAux as (bs, a::cs) @[inline] def partition (p : α → Bool) (as : List α) : List α × List α := partitionAux p as ([], []) @@ -179,20 +179,20 @@ partitionAux p as ([], []) def dropWhile (p : α → Bool) : List α → List α | [] := [] | (a::l) := match p a with - | true := dropWhile l - | false := a::l + | true => dropWhile l + | false => a::l def find (p : α → Bool) : List α → Option α | [] := none | (a::as) := match p a with - | true := some a - | false := find as + | true => some a + | false => find as def elem [HasBeq α] (a : α) : List α → Bool | [] := false | (b::bs) := match a == b with - | true := true - | false := elem bs + | true => true + | false => elem bs def notElem [HasBeq α] (a : α) (as : List α) : Bool := !(as.elem a) @@ -200,8 +200,8 @@ def notElem [HasBeq α] (a : α) (as : List α) : Bool := @[specialize] def spanAux (p : α → Bool) : List α → List α → List α × List α | [] rs := (rs.reverse, []) | (a::as) rs := match p a with - | true := spanAux as (a::rs) - | false := (rs.reverse, a::as) + | true => spanAux as (a::rs) + | false => (rs.reverse, a::as) @[inline] def span (p : α → Bool) (as : List α) : List α × List α := spanAux p as [] @@ -209,8 +209,8 @@ spanAux p as [] def lookup [HasBeq α] : α → List (α × β) → Option β | _ [] := none | a ((k,b)::es) := match a == k with - | true := some b - | false := lookup a es + | true => some b + | false => lookup a es def removeAll [HasBeq α] (xs ys : List α) : List α := xs.filter (fun x => ys.notElem x) @@ -261,7 +261,7 @@ 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) protected def insert [DecidableEq α] (a : α) (l : List α) : List α := if a ∈ l then l else a :: l @@ -331,18 +331,18 @@ instance hasDecidableLt [HasLess α] [h : DecidableRel HasLess.Less] : ∀ l₁ | (a::as) [] := isFalse (fun h => match h with end) | (a::as) (b::bs) := match h a b with - | isTrue h₁ := isTrue (Less.head _ _ h₁) - | isFalse h₁ := + | isTrue h₁ => isTrue (Less.head _ _ h₁) + | isFalse h₁ => match h b a with - | isTrue h₂ := isFalse (fun h => match h with - | Less.head _ _ h₁' := absurd h₁' h₁ - | Less.tail _ h₂' _ := absurd h₂ h₂') - | isFalse h₂ := + | isTrue h₂ => isFalse (fun h => match h with + | Less.head _ _ h₁' => absurd h₁' h₁ + | Less.tail _ h₂' _ => absurd h₂ h₂') + | isFalse h₂ => match hasDecidableLt as bs with - | isTrue h₃ := isTrue (Less.tail h₁ h₂ h₃) - | isFalse h₃ := isFalse (fun h => match h with - | Less.head _ _ h₁' := absurd h₁' h₁ - | Less.tail _ _ h₃' := absurd h₃' h₃) + | isTrue h₃ => isTrue (Less.tail h₁ h₂ h₃) + | isFalse h₃ => isFalse (fun h => match h with + | Less.head _ _ h₁' => absurd h₁' h₁ + | Less.tail _ _ h₃' => absurd h₃' h₃) @[reducible] protected def LessEq [HasLess α] (a b : List α) : Prop := ¬ b < a diff --git a/library/init/data/nat/basic.lean b/library/init/data/nat/basic.lean index 951785e9fd..b843032b2b 100644 --- a/library/init/data/nat/basic.lean +++ b/library/init/data/nat/basic.lean @@ -382,11 +382,11 @@ protected theorem ltOrGe : ∀ (n m : Nat), n < m ∨ n ≥ m | n 0 := Or.inr (zeroLe n) | n (m+1) := match ltOrGe n m with - | Or.inl h := Or.inl (leSuccOfLe h) - | Or.inr h := + | Or.inl h => Or.inl (leSuccOfLe h) + | Or.inr h => match Nat.eqOrLtOfLe h with - | Or.inl h1 := Or.inl (h1 ▸ ltSuccSelf m) - | Or.inr h1 := Or.inr h1 + | Or.inl h1 => Or.inl (h1 ▸ ltSuccSelf m) + | Or.inr h1 => Or.inr h1 protected theorem leTotal (m n : Nat) : m ≤ n ∨ n ≤ m := Or.elim (Nat.ltOrGe m n) @@ -434,7 +434,7 @@ theorem le.dest : ∀ {n m : Nat}, n ≤ m → Exists (fun k => n + k = m) have n ≤ m from h; have Exists (fun k => n + k = m) from le.dest this; match this with - | ⟨k, h⟩ := ⟨k, show succ n + k = succ m from ((succAdd n k).symm ▸ h ▸ rfl)⟩ + | ⟨k, h⟩ => ⟨k, show succ n + k = succ m from ((succAdd n k).symm ▸ h ▸ rfl)⟩ theorem le.intro {n m k : Nat} (h : n + k = m) : n ≤ m := h ▸ leAddRight n k @@ -458,7 +458,7 @@ Or.elim (Nat.ltOrGe n m) protected theorem addLeAddLeft {n m : Nat} (h : n ≤ m) (k : Nat) : k + n ≤ k + m := match le.dest h with -| ⟨w, hw⟩ := +| ⟨w, hw⟩ => have h₁ : k + n + w = k + (n + w) from Nat.addAssoc _ _ _; have h₂ : k + (n + w) = k + m from congrArg _ hw; le.intro $ h₁.trans h₂ @@ -643,7 +643,7 @@ protected theorem oneLeBit0 : ∀ (n : Nat), n ≠ 0 → 1 ≤ bit0 n theorem mulLeMulLeft {n m : Nat} (k : Nat) (h : n ≤ m) : k * n ≤ k * m := match le.dest h with -| ⟨l, hl⟩ := +| ⟨l, hl⟩ => have k * n + k * l = k * m from Nat.leftDistrib k n l ▸ hl.symm ▸ rfl; le.intro this diff --git a/library/init/data/option/basic.lean b/library/init/data/option/basic.lean index a5336dce9e..263d869cfd 100644 --- a/library/init/data/option/basic.lean +++ b/library/init/data/option/basic.lean @@ -43,7 +43,7 @@ def toMonad {m : Type → Type} [Monad m] [Alternative m] {A} : Option A → m A Option.bind o (some ∘ f) theorem mapId {α} : (Option.map id : Option α → Option α) = id := -funext (fun o => match o with | none := rfl | some x := rfl) +funext (fun o => match o with | none => rfl | some x => rfl) instance : Monad Option := {pure := @some, bind := @Option.bind, map := @Option.map} @@ -77,12 +77,12 @@ instance (α : Type u) : Inhabited (Option α) := instance {α : Type u} [DecidableEq α] : DecidableEq (Option α) := {decEq := fun a b => match a, b with - | none, none := isTrue rfl - | none, (some v₂) := isFalse (fun h => Option.noConfusion h) - | (some v₁), none := isFalse (fun h => Option.noConfusion h) - | (some v₁), (some v₂) := + | none, none => isTrue rfl + | none, (some v₂) => isFalse (fun h => Option.noConfusion h) + | (some v₁), none => isFalse (fun h => Option.noConfusion h) + | (some v₁), (some v₂) => match decEq v₁ v₂ with - | (isTrue e) := isTrue (congrArg (@some α) e) - | (isFalse n) := isFalse (fun h => Option.noConfusion h (fun e => absurd e n))} + | (isTrue e) => isTrue (congrArg (@some α) e) + | (isFalse n) => isFalse (fun h => Option.noConfusion h (fun e => absurd e n))} instance {α : Type u} [HasLess α] : HasLess (Option α) := ⟨Option.lt HasLess.Less⟩ diff --git a/library/init/data/ordering/basic.lean b/library/init/data/ordering/basic.lean index 4c50dd3948..fc550154da 100644 --- a/library/init/data/ordering/basic.lean +++ b/library/init/data/ordering/basic.lean @@ -12,7 +12,7 @@ inductive Ordering | lt | Eq | gt instance : HasRepr Ordering := -⟨(fun s => match s with | Ordering.lt := "lt" | Ordering.Eq := "Eq" | Ordering.gt := "gt")⟩ +⟨(fun s => match s with | Ordering.lt => "lt" | Ordering.Eq => "Eq" | Ordering.gt => "gt")⟩ namespace Ordering def swap : Ordering → Ordering @@ -42,18 +42,18 @@ cmpUsing HasLess.Less a b instance : DecidableEq Ordering := {decEq := fun a b => match a with - | Ordering.lt := + | Ordering.lt => match b with - | Ordering.lt := isTrue rfl - | Ordering.Eq := isFalse (fun h => Ordering.noConfusion h) - | Ordering.gt := isFalse (fun h => Ordering.noConfusion h) - | Ordering.Eq := + | Ordering.lt => isTrue rfl + | Ordering.Eq => isFalse (fun h => Ordering.noConfusion h) + | Ordering.gt => isFalse (fun h => Ordering.noConfusion h) + | Ordering.Eq => match b with - | Ordering.lt := isFalse (fun h => Ordering.noConfusion h) - | Ordering.Eq := isTrue rfl - | Ordering.gt := isFalse (fun h => Ordering.noConfusion h) - | Ordering.gt := + | Ordering.lt => isFalse (fun h => Ordering.noConfusion h) + | Ordering.Eq => isTrue rfl + | Ordering.gt => isFalse (fun h => Ordering.noConfusion h) + | Ordering.gt => match b with - | Ordering.lt := isFalse (fun h => Ordering.noConfusion h) - | Ordering.Eq := isFalse (fun h => Ordering.noConfusion h) - | Ordering.gt := isTrue rfl} + | Ordering.lt => isFalse (fun h => Ordering.noConfusion h) + | Ordering.Eq => isFalse (fun h => Ordering.noConfusion h) + | Ordering.gt => isTrue rfl} diff --git a/library/init/data/rbmap/basic.lean b/library/init/data/rbmap/basic.lean index 5ef77494e4..ee7c821556 100644 --- a/library/init/data/rbmap/basic.lean +++ b/library/init/data/rbmap/basic.lean @@ -129,11 +129,11 @@ def balLeft : RBNode α β → ∀ k, β k → RBNode α β → RBNode α β def balRight (l : RBNode α β) (k : α) (v : β k) (r : RBNode α β) : RBNode α β := match r with -| (node red b ky vy c) := node red l k v (node black b ky vy c) -| _ := match l with - | node black a kx vx b := balance₃ (node red a kx vx b) k v r - | node red a kx vx (node black b ky vy c) := node red (balance₃ (setRed a) kx vx b) ky vy (node black c k v r) - | _ := node red l k v r -- unreachable +| (node red b ky vy c) => node red l k v (node black b ky vy c) +| _ => match l with + | node black a kx vx b => balance₃ (node red a kx vx b) k v r + | node red a kx vx (node black b ky vy c) => node red (balance₃ (setRed a) kx vx b) ky vy (node black c k v r) + | _ => node red l k v r -- unreachable -- TODO: use wellfounded recursion partial def appendTrees : RBNode α β → RBNode α β → RBNode α β @@ -141,12 +141,12 @@ partial def appendTrees : RBNode α β → RBNode α β → RBNode α β | x leaf := x | (node red a kx vx b) (node red c ky vy d) := match appendTrees b c with - | node red b' kz vz c' := node red (node red a kx vx b') kz vz (node red c' ky vy d) - | bc := node red a kx vx (node red bc ky vy d) + | node red b' kz vz c' => node red (node red a kx vx b') kz vz (node red c' ky vy d) + | bc => node red a kx vx (node red bc ky vy d) | (node black a kx vx b) (node black c ky vy d) := match appendTrees b c with - | node red b' kz vz c' := node red (node black a kx vx b') kz vz (node black c' ky vy d) - | bc := balLeft a kx vx (node black bc ky vy d) + | node red b' kz vz c' => node red (node black a kx vx b') kz vz (node black c' ky vy d) + | bc => balLeft a kx vx (node black bc ky vy d) | a (node red b kx vx c) := node red (appendTrees a b) kx vx c | (node red a kx vx b) c := node red a kx vx (appendTrees b c) @@ -248,14 +248,14 @@ t.mfold (fun _ k v => f k v *> pure ⟨⟩) ⟨⟩ @[inline] protected def min : RBMap α β lt → Option (α × β) | ⟨t, _⟩ := match t.min with - | some ⟨k, v⟩ := some (k, v) - | none := none + | some ⟨k, v⟩ => some (k, v) + | none => none @[inline] protected def max : RBMap α β lt → Option (α × β) | ⟨t, _⟩ := match t.max with - | some ⟨k, v⟩ := some (k, v) - | none := none + | some ⟨k, v⟩ => some (k, v) + | none => none instance [HasRepr α] [HasRepr β] : HasRepr (RBMap α β lt) := ⟨fun t => "rbmapOf " ++ repr t.toList⟩ diff --git a/library/init/data/rbtree/basic.lean b/library/init/data/rbtree/basic.lean index 431f8a7a09..52d3a940ed 100644 --- a/library/init/data/rbtree/basic.lean +++ b/library/init/data/rbtree/basic.lean @@ -42,13 +42,13 @@ t.revFold (fun as a => a::as) [] @[inline] protected def min (t : RBTree α lt) : Option α := match RBMap.min t with -| some ⟨a, _⟩ := some a -| none := none +| some ⟨a, _⟩ => some a +| none => none @[inline] protected def max (t : RBTree α lt) : Option α := match RBMap.max t with -| some ⟨a, _⟩ := some a -| none := none +| some ⟨a, _⟩ => some a +| none => none instance [HasRepr α] : HasRepr (RBTree α lt) := ⟨fun t => "rbtreeOf " ++ repr t.toList⟩ @@ -67,8 +67,8 @@ RBMap.erase t a @[inline] def find (t : RBTree α lt) (a : α) : Option α := match RBMap.findCore t a with -| some ⟨a, _⟩ := some a -| none := none +| some ⟨a, _⟩ => some a +| none => none @[inline] def contains (t : RBTree α lt) (a : α) : Bool := (t.find a).isSome diff --git a/library/init/data/repr.lean b/library/init/data/repr.lean index ed635bd29c..ad2977c716 100644 --- a/library/init/data/repr.lean +++ b/library/init/data/repr.lean @@ -40,10 +40,10 @@ instance : HasRepr Unit := ⟨fun u => "()"⟩ instance {α : Type u} [HasRepr α] : HasRepr (Option α) := -⟨fun o => match o with | none := "none" | (some a) := "(some " ++ repr a ++ ")"⟩ +⟨fun o => match o with | none => "none" | (some a) => "(some " ++ repr a ++ ")"⟩ instance {α : Type u} {β : Type v} [HasRepr α] [HasRepr β] : HasRepr (α ⊕ β) := -⟨fun s => match s with | (inl a) := "(inl " ++ repr a ++ ")" | (inr b) := "(inr " ++ repr b ++ ")"⟩ +⟨fun s => match s with | (inl a) => "(inl " ++ repr a ++ ")" | (inr b) => "(inr " ++ repr b ++ ")"⟩ instance {α : Type u} {β : Type v} [HasRepr α] [HasRepr β] : HasRepr (α × β) := ⟨fun ⟨a, b⟩ => "(" ++ repr a ++ ", " ++ repr b ++ ")"⟩ diff --git a/library/init/data/string/basic.lean b/library/init/data/string/basic.lean index d2cd2a1905..188c94e150 100644 --- a/library/init/data/string/basic.lean +++ b/library/init/data/string/basic.lean @@ -21,7 +21,7 @@ attribute [extern cpp "lean::string_data"] String.data @[extern cpp "lean::string_dec_eq"] def String.decEq (s₁ s₂ : @& String) : Decidable (s₁ = s₂) := match s₁, s₂ with -| ⟨s₁⟩, ⟨s₂⟩ := +| ⟨s₁⟩, ⟨s₂⟩ => if h : s₁ = s₂ then isTrue (congrArg _ h) else isFalse (fun h' => String.noConfusion h' (fun h' => absurd h' h)) @@ -353,7 +353,7 @@ s.get 0 @[inline] def posOf (s : Substring) (c : Char) : String.Pos := match s with -| ⟨s, b, e⟩ := (String.posOfAux s c e b) - b +| ⟨s, b, e⟩ => (String.posOfAux s c e b) - b @[inline] def drop : Substring → Nat → Substring | ⟨s, b, e⟩ n := @@ -398,15 +398,15 @@ if sep == "" then [s] else splitAux s.str sep s.stopPos s.startPos s.startPos 0 @[inline] def foldl {α : Type u} (f : α → Char → α) (a : α) (s : Substring) : α := match s with -| ⟨s, b, e⟩ := String.foldlAux f s e b a +| ⟨s, b, e⟩ => String.foldlAux f s e b a @[inline] def foldr {α : Type u} (f : Char → α → α) (a : α) (s : Substring) : α := match s with -| ⟨s, b, e⟩ := String.foldrAux f a s e b +| ⟨s, b, e⟩ => String.foldrAux f a s e b @[inline] def any (s : Substring) (p : Char → Bool) : Bool := match s with -| ⟨s, b, e⟩ := String.anyAux s e p b +| ⟨s, b, e⟩ => String.anyAux s e p b @[inline] def all (s : Substring) (p : Char → Bool) : Bool := !s.any (fun c => !p c) diff --git a/library/init/data/tostring.lean b/library/init/data/tostring.lean index 1d50163b46..4c2898d157 100644 --- a/library/init/data/tostring.lean +++ b/library/init/data/tostring.lean @@ -74,10 +74,10 @@ instance : HasToString USize := ⟨fun n => toString n.toNat⟩ instance {α : Type u} [HasToString α] : HasToString (Option α) := -⟨fun o => match o with | none := "none" | (some a) := "(some " ++ toString a ++ ")"⟩ +⟨fun o => match o with | none => "none" | (some a) => "(some " ++ toString a ++ ")"⟩ instance {α : Type u} {β : Type v} [HasToString α] [HasToString β] : HasToString (α ⊕ β) := -⟨fun s => match s with | (inl a) := "(inl " ++ toString a ++ ")" | (inr b) := "(inr " ++ toString b ++ ")"⟩ +⟨fun s => match s with | (inl a) => "(inl " ++ toString a ++ ")" | (inr b) => "(inr " ++ toString b ++ ")"⟩ instance {α : Type u} {β : Type v} [HasToString α] [HasToString β] : HasToString (α × β) := ⟨fun ⟨a, b⟩ => "(" ++ toString a ++ ", " ++ toString b ++ ")"⟩ diff --git a/library/init/io.lean b/library/init/io.lean index 81f2502842..f5c52c5ec9 100644 --- a/library/init/io.lean +++ b/library/init/io.lean @@ -69,8 +69,8 @@ namespace IO def ofExcept {ε α : Type} [HasToString ε] (e : Except ε α) : IO α := match e with -| Except.ok a := pure a -| Except.error e := throw (IO.userError (toString e)) +| Except.ok a => pure a +| Except.error e => throw (IO.userError (toString e)) def lazyPure {α : Type} (fn : Unit → α) : IO α := pure (fn ()) @@ -87,8 +87,8 @@ open Fs | a f := do v ← f a; match v with - | Sum.inl a := iterate a f - | Sum.inr b := pure b + | Sum.inl a => iterate a f + | Sum.inr b => pure b @[extern 2 "lean_io_prim_put_str"] constant putStr (s: @& String) : IO Unit := default _ diff --git a/library/init/lean/attributes.lean b/library/init/lean/attributes.lean index 9ccc1e60b0..c39c82bbad 100644 --- a/library/init/lean/attributes.lean +++ b/library/init/lean/attributes.lean @@ -52,8 +52,8 @@ env.getNamespaceSet.contains n @[export lean.in_section_core] def inSection (env : Environment) : Bool := match (scopeManagerExt.getState env).isNamespace with -| (b::_) := !b -| _ := false +| (b::_) => !b +| _ => false @[export lean.has_open_scopes_core] def hasOpenScopes (env : Environment) : Bool := @@ -62,14 +62,14 @@ def hasOpenScopes (env : Environment) : Bool := @[export lean.get_namespace_core] def getNamespace (env : Environment) : Name := match env.getNamespaces with -| (n::_) := n -| _ := Name.anonymous +| (n::_) => n +| _ => Name.anonymous @[export lean.get_scope_header_core] def getScopeHeader (env : Environment) : Name := match (scopeManagerExt.getState env).headers with -| (n::_) := n -| _ := Name.anonymous +| (n::_) => n +| _ => Name.anonymous @[export lean.to_valid_namespace_core] def toValidNamespace (env : Environment) (n : Name) : Option Name := @@ -77,8 +77,8 @@ let s := scopeManagerExt.getState env; if s.allNamespaces.contains n then some n else s.namespaces.foldl (fun r ns => match r with - | some _ := r - | none := + | some _ => r + | none => let c := ns ++ n; if s.allNamespaces.contains c then some c else none) none @@ -164,8 +164,8 @@ do m ← attributeMapRef.get; pure $ m.fold (fun r n _ => n::r) [] def getAttributeImpl (attrName : Name) : IO AttributeImpl := do m ← attributeMapRef.get; match m.find attrName with - | some attr := pure attr - | none := throw (IO.userError ("unknown attribute '" ++ toString attrName ++ "'")) + | some attr => pure attr + | none => throw (IO.userError ("unknown attribute '" ++ toString attrName ++ "'")) @[export lean.attribute_application_time_core] def attributeApplicationTime (n : Name) : IO AttributeApplicationTime := @@ -270,8 +270,8 @@ let attrImpl : AttributeImpl := { unless (env.getModuleIdxFor decl).isNone $ throw (IO.userError ("invalid attribute '" ++ toString name ++ "', declaration is in an imported module")); match validate env decl with - | Except.error msg := throw (IO.userError ("invalid attribute '" ++ toString name ++ "', " ++ msg)) - | _ := pure $ ext.addEntry env decl + | Except.error msg => throw (IO.userError ("invalid attribute '" ++ toString name ++ "', " ++ msg)) + | _ => pure $ ext.addEntry env decl }; registerAttribute attrImpl; pure { attr := attrImpl, ext := ext } @@ -282,8 +282,8 @@ instance : Inhabited TagAttribute := ⟨{attr := default _, ext := default _}⟩ def hasTag (attr : TagAttribute) (env : Environment) (decl : Name) : Bool := match env.getModuleIdxFor decl with -| some modIdx := (attr.ext.getModuleEntries env modIdx).binSearchContains decl Name.quickLt -| none := (attr.ext.getState env).contains decl +| some modIdx => (attr.ext.getModuleEntries env modIdx).binSearchContains decl Name.quickLt +| none => (attr.ext.getState env).contains decl end TagAttribute @@ -318,12 +318,12 @@ let attrImpl : AttributeImpl := { unless (env.getModuleIdxFor decl).isNone $ throw (IO.userError ("invalid attribute '" ++ toString name ++ "', declaration is in an imported module")); match getParam env decl args with - | Except.error msg := throw (IO.userError ("invalid attribute '" ++ toString name ++ "', " ++ msg)) - | Except.ok val := do + | Except.error msg => throw (IO.userError ("invalid attribute '" ++ toString name ++ "', " ++ msg)) + | Except.ok val => do let env := ext.addEntry env (decl, val); match afterSet env decl val with - | Except.error msg := throw (IO.userError ("invalid attribute '" ++ toString name ++ "', " ++ msg)) - | Except.ok env := pure env + | Except.error msg => throw (IO.userError ("invalid attribute '" ++ toString name ++ "', " ++ msg)) + | Except.ok env => pure env }; registerAttribute attrImpl; pure { attr := attrImpl, ext := ext } @@ -334,11 +334,11 @@ instance {α : Type} : Inhabited (ParametricAttribute α) := ⟨{attr := default def getParam {α : Type} [Inhabited α] (attr : ParametricAttribute α) (env : Environment) (decl : Name) : Option α := match env.getModuleIdxFor decl with -| some modIdx := +| some modIdx => match (attr.ext.getModuleEntries env modIdx).binSearch (decl, default _) (fun a b => Name.quickLt a.1 b.1) with - | some (_, val) := some val - | none := none -| none := (attr.ext.getState env).find decl + | some (_, val) => some val + | none => none +| none => (attr.ext.getState env).find decl def setParam {α : Type} (attr : ParametricAttribute α) (env : Environment) (decl : Name) (param : α) : Except String Environment := if (env.getModuleIdxFor decl).isSome then @@ -377,8 +377,8 @@ let attrs := attrDescrs.map $ fun ⟨name, descr, val⟩ => { AttributeImpl . unless (env.getModuleIdxFor decl).isNone $ throw (IO.userError ("invalid attribute '" ++ toString name ++ "', declaration is in an imported module")); match validate env decl val with - | Except.error msg := throw (IO.userError ("invalid attribute '" ++ toString name ++ "', " ++ msg)) - | _ := pure $ ext.addEntry env (decl, val) + | Except.error msg => throw (IO.userError ("invalid attribute '" ++ toString name ++ "', " ++ msg)) + | _ => pure $ ext.addEntry env (decl, val) }; attrs.mfor registerAttribute; pure { ext := ext, attrs := attrs } @@ -389,11 +389,11 @@ instance {α : Type} : Inhabited (EnumAttributes α) := ⟨{attrs := [], ext := def getValue {α : Type} [Inhabited α] (attr : EnumAttributes α) (env : Environment) (decl : Name) : Option α := match env.getModuleIdxFor decl with -| some modIdx := +| some modIdx => match (attr.ext.getModuleEntries env modIdx).binSearch (decl, default _) (fun a b => Name.quickLt a.1 b.1) with - | some (_, val) := some val - | none := none -| none := (attr.ext.getState env).find decl + | some (_, val) => some val + | none => none +| none => (attr.ext.getState env).find decl def setValue {α : Type} (attrs : EnumAttributes α) (env : Environment) (decl : Name) (val : α) : Except String Environment := if (env.getModuleIdxFor decl).isSome then @@ -412,12 +412,12 @@ end EnumAttributes decode the Syntax object. -/ def attrParamSyntaxToIdentifier (s : Syntax) : Option Name := match s with -| Syntax.node k args _ := +| Syntax.node k args _ => if k == nullKind && args.size == 1 then match args.get 0 with - | Syntax.ident _ _ id _ _ := some id - | _ := none + | Syntax.ident _ _ id _ _ => some id + | _ => none else none -| _ := none +| _ => none end Lean diff --git a/library/init/lean/class.lean b/library/init/lean/class.lean index 20d3f83963..4342066b6c 100644 --- a/library/init/lean/class.lean +++ b/library/init/lean/class.lean @@ -34,13 +34,13 @@ instance : Inhabited ClassState := ⟨{}⟩ def addEntry (s : ClassState) (entry : ClassEntry) : ClassState := match entry with -| ClassEntry.«class» clsName hasOutParam := +| ClassEntry.«class» clsName hasOutParam => { hasOutParam := s.hasOutParam.insert clsName hasOutParam, .. s } -| ClassEntry.«instance» instName clsName := +| ClassEntry.«instance» instName clsName => { instances := s.instances.insert instName (), classToInstances := match s.classToInstances.find clsName with - | some insts := s.classToInstances.insert clsName (instName :: insts) - | none := s.classToInstances.insert clsName [instName], + | some insts => s.classToInstances.insert clsName (instName :: insts) + | none => s.classToInstances.insert clsName [instName], .. s } def switch : ClassState → ClassState @@ -70,14 +70,14 @@ def isInstance (env : Environment) (n : Name) : Bool := @[export lean.get_class_instances_core] def getClassInstances (env : Environment) (n : Name) : List Name := match (classExtension.getState env).classToInstances.find n with -| some insts := insts -| none := [] +| some insts => insts +| none => [] @[export lean.has_out_params_core] def hasOutParams (env : Environment) (n : Name) : Bool := match (classExtension.getState env).hasOutParam.find n with -| some b := b -| none := false +| some b => b +| none => false @[export lean.is_out_param_core] private def isOutParam (e : Expr) : Bool := @@ -90,8 +90,8 @@ def Expr.hasOutParam : Expr → Bool def addClass (env : Environment) (clsName : Name) : Except String Environment := if isClass env clsName then Except.error ("class has already been declared '" ++ toString clsName ++ "'") else match env.find clsName with - | none := Except.error ("unknown declaration '" ++ toString clsName ++ "'") - | some decl := Except.ok (classExtension.addEntry env (ClassEntry.«class» clsName decl.type.hasOutParam)) + | none => Except.error ("unknown declaration '" ++ toString clsName ++ "'") + | some decl => Except.ok (classExtension.addEntry env (ClassEntry.«class» clsName decl.type.hasOutParam)) private def consumeNLambdas : Nat → Expr → Option Expr | 0 e := some e @@ -104,21 +104,21 @@ partial def getClassName (env : Environment) : Expr → Option Name Expr.const c _ ← pure e.getAppFn | none; info ← env.find c; match info.value with - | some val := do + | some val => do body ← consumeNLambdas e.getAppNumArgs val; getClassName body - | none := + | none => if isClass env c then some c else none @[export lean.add_instance_core] def addInstance (env : Environment) (instName : Name) : Except String Environment := match env.find instName with -| none := Except.error ("unknown declaration '" ++ toString instName ++ "'") -| some decl := +| none => Except.error ("unknown declaration '" ++ toString instName ++ "'") +| some decl => match getClassName env decl.type with - | none := Except.error ("invalid instance '" ++ toString instName ++ "', failed to retrieve class") - | some clsName := Except.ok (classExtension.addEntry env (ClassEntry.«instance» instName clsName)) + | none => Except.error ("invalid instance '" ++ toString instName ++ "', failed to retrieve class") + | some clsName => Except.ok (classExtension.addEntry env (ClassEntry.«instance» instName clsName)) @[init] def registerClassAttr : IO Unit := registerAttribute { diff --git a/library/init/lean/compiler/constfolding.lean b/library/init/lean/compiler/constfolding.lean index 3224d60c30..841625e047 100644 --- a/library/init/lean/compiler/constfolding.lean +++ b/library/init/lean/compiler/constfolding.lean @@ -98,10 +98,10 @@ mkBinApp (mkBinApp (Expr.const `HasLt.le [Level.zero]) (Expr.const `Nat []) (Exp def toDecidableExpr (beforeErasure : Bool) (pred : Expr) (r : Bool) : Expr := match beforeErasure, r with -| false, true := mkDecIsTrue neutralExpr neutralExpr -| false, false := mkDecIsFalse neutralExpr neutralExpr -| true, true := mkDecIsTrue pred (mkLcProof pred) -| true, false := mkDecIsFalse pred (mkLcProof pred) +| false, true => mkDecIsTrue neutralExpr neutralExpr +| false, false => mkDecIsFalse neutralExpr neutralExpr +| true, true => mkDecIsTrue pred (mkLcProof pred) +| true, false => mkDecIsFalse pred (mkLcProof pred) def foldNatBinPred (mkPred : Expr → Expr → Expr) (fn : Nat → Nat → Bool) (beforeErasure : Bool) (a₁ a₂ : Expr) : Option Expr := @@ -133,21 +133,21 @@ def foldStrictAnd (_ : Bool) (a₁ a₂ : Expr) : Option Expr := let v₁ := getBoolLit a₁; let v₂ := getBoolLit a₂; match v₁, v₂ with -| some true, _ := a₂ -| some false, _ := a₁ -| _, some true := a₁ -| _, some false := a₂ -| _, _ := none +| some true, _ => a₂ +| some false, _ => a₁ +| _, some true => a₁ +| _, some false => a₂ +| _, _ => none def foldStrictOr (_ : Bool) (a₁ a₂ : Expr) : Option Expr := let v₁ := getBoolLit a₁; let v₂ := getBoolLit a₂; match v₁, v₂ with -| some true, _ := a₁ -| some false, _ := a₂ -| _, some true := a₂ -| _, some false := a₁ -| _, _ := none +| some true, _ => a₁ +| some false, _ => a₂ +| _, some true => a₂ +| _, some false => a₁ +| _, _ => none def boolFoldFns : List (Name × BinFoldFn) := [(`strictOr, foldStrictOr), (`strictAnd, foldStrictAnd)] @@ -187,18 +187,18 @@ unFoldFns.lookup fn @[export lean.fold_bin_op_core] def foldBinOp (beforeErasure : Bool) (f : Expr) (a : Expr) (b : Expr) : Option Expr := match f with -| Expr.const fn _ := do +| Expr.const fn _ => do foldFn ← findBinFoldFn fn; foldFn beforeErasure a b -| _ := none +| _ => none @[export lean.fold_un_op_core] def foldUnOp (beforeErasure : Bool) (f : Expr) (a : Expr) : Option Expr := match f with -| Expr.const fn _ := do +| Expr.const fn _ => do foldFn ← findUnFoldFn fn; foldFn beforeErasure a -| _ := none +| _ => none end Compiler end Lean diff --git a/library/init/lean/compiler/exportattr.lean b/library/init/lean/compiler/exportattr.lean index 79d60dac3e..92b791dd25 100644 --- a/library/init/lean/compiler/exportattr.lean +++ b/library/init/lean/compiler/exportattr.lean @@ -20,10 +20,10 @@ private def isValidCppName : Name → Bool def mkExportAttr : IO (ParametricAttribute Name) := registerParametricAttribute `export "name to be used by code generators" $ fun _ _ stx => match attrParamSyntaxToIdentifier stx with - | some exportName := + | some exportName => if isValidCppName exportName then Except.ok exportName else Except.error "invalid 'export' function name, is not a valid C++ identifier" - | _ := Except.error "unexpected kind of argument" + | _ => Except.error "unexpected kind of argument" @[init mkExportAttr] constant exportAttr : ParametricAttribute Name := default _ diff --git a/library/init/lean/compiler/externattr.lean b/library/init/lean/compiler/externattr.lean index 2e12b6dba1..3e17b239fe 100644 --- a/library/init/lean/compiler/externattr.lean +++ b/library/init/lean/compiler/externattr.lean @@ -42,40 +42,40 @@ private partial def syntaxToExternEntries (a : Array Syntax) : Nat → List Exte | i entries := if i == a.size then Except.ok entries else match a.get i with - | Syntax.ident _ _ backend _ _ := + | Syntax.ident _ _ backend _ _ => let i := i + 1; if i == a.size then Except.error "string or identifier expected" else match (a.get i).isIdOrAtom with - | some "adhoc" := syntaxToExternEntries (i+1) (ExternEntry.adhoc backend :: entries) - | some "inline" := + | some "adhoc" => syntaxToExternEntries (i+1) (ExternEntry.adhoc backend :: entries) + | some "inline" => let i := i + 1; match (a.get i).isStrLit with - | some pattern := syntaxToExternEntries (i+1) (ExternEntry.inline backend pattern :: entries) - | none := Except.error "string literal expected" - | _ := match (a.get i).isStrLit with - | some fn := syntaxToExternEntries (i+1) (ExternEntry.standard backend fn :: entries) - | none := Except.error "string literal expected" - | _ := Except.error "identifier expected" + | some pattern => syntaxToExternEntries (i+1) (ExternEntry.inline backend pattern :: entries) + | none => Except.error "string literal expected" + | _ => match (a.get i).isStrLit with + | some fn => syntaxToExternEntries (i+1) (ExternEntry.standard backend fn :: entries) + | none => Except.error "string literal expected" + | _ => Except.error "identifier expected" private def syntaxToExternAttrData (s : Syntax) : ExceptT String Id ExternAttrData := match s with -| Syntax.missing := Except.ok { entries := [ ExternEntry.adhoc `all ] } -| Syntax.node _ args _ := +| Syntax.missing => Except.ok { entries := [ ExternEntry.adhoc `all ] } +| Syntax.node _ args _ => if args.size == 0 then Except.error "unexpected kind of argument" else let (arity, i) : Option Nat × Nat := match (args.get 0).isNatLit with - | some arity := (some arity, 1) - | none := (none, 0); + | some arity => (some arity, 1) + | none => (none, 0); match (args.get i).isStrLit with - | some str := + | some str => if args.size == i+1 then Except.ok { arity := arity, entries := [ ExternEntry.standard `all str ] } else Except.error "invalid extern attribute" - | none := match syntaxToExternEntries args i [] with - | Except.ok entries := Except.ok { arity := arity, entries := entries } - | Except.error msg := Except.error msg -| _ := Except.error "unexpected kind of argument" + | none => match syntaxToExternEntries args i [] with + | Except.ok entries => Except.ok { arity := arity, entries := entries } + | Except.error msg => Except.error msg +| _ => Except.error "unexpected kind of argument" @[extern "lean_add_extern"] constant addExtern (env : Environment) (n : Name) : ExceptT String Id Environment := default _ @@ -157,15 +157,15 @@ def isExtern (env : Environment) (fn : Name) : Bool := Thus, there is no name mangling. -/ def isExternC (env : Environment) (fn : Name) : Bool := match getExternAttrData env fn with -| some { entries := [ ExternEntry.standard `all _ ], .. } := true -| _ := false +| some { entries := [ ExternEntry.standard `all _ ], .. } => true +| _ => false def getExternNameFor (env : Environment) (backend : Name) (fn : Name) : Option String := do data ← getExternAttrData env fn; entry ← getExternEntryFor data backend; match entry with - | ExternEntry.standard _ n := pure n - | ExternEntry.foreign _ n := pure n - | _ := failure + | ExternEntry.standard _ n => pure n + | ExternEntry.foreign _ n => pure n + | _ => failure end Lean diff --git a/library/init/lean/compiler/implementedbyattr.lean b/library/init/lean/compiler/implementedbyattr.lean index 17df597e50..26749baa0a 100644 --- a/library/init/lean/compiler/implementedbyattr.lean +++ b/library/init/lean/compiler/implementedbyattr.lean @@ -12,16 +12,16 @@ namespace Compiler def mkImplementedByAttr : IO (ParametricAttribute Name) := registerParametricAttribute `implementedBy "name of the Lean (probably unsafe) function that implements opaque constant" $ fun env declName stx => match env.find declName with - | none := Except.error "unknown declaration" - | some decl := + | none => Except.error "unknown declaration" + | some decl => match attrParamSyntaxToIdentifier stx with - | some fnName := + | some fnName => match env.find fnName with - | none := Except.error ("unknown function '" ++ toString fnName ++ "'") - | some fnDecl := + | none => Except.error ("unknown function '" ++ toString fnName ++ "'") + | some fnDecl => if decl.type == fnDecl.type then Except.ok fnName else Except.error ("invalid function '" ++ toString fnName ++ "' type mismatch") - | _ := Except.error "expected identifier" + | _ => Except.error "expected identifier" @[init mkImplementedByAttr] constant implementedByAttr : ParametricAttribute Name := default _ diff --git a/library/init/lean/compiler/initattr.lean b/library/init/lean/compiler/initattr.lean index 9da6e6cc5e..5d5243def0 100644 --- a/library/init/lean/compiler/initattr.lean +++ b/library/init/lean/compiler/initattr.lean @@ -19,44 +19,44 @@ private def isUnitType : Expr → Bool private def isIOUnit (type : Expr) : Bool := match getIOTypeArg type with -| some type := isUnitType type -| _ := false +| some type => isUnitType type +| _ => false def mkInitAttr : IO (ParametricAttribute Name) := registerParametricAttribute `init "initialization procedure for global references" $ fun env declName stx => match env.find declName with - | none := Except.error "unknown declaration" - | some decl := + | none => Except.error "unknown declaration" + | some decl => match attrParamSyntaxToIdentifier stx with - | some initFnName := + | some initFnName => match env.find initFnName with - | none := Except.error ("unknown initialization function '" ++ toString initFnName ++ "'") - | some initDecl := + | none => Except.error ("unknown initialization function '" ++ toString initFnName ++ "'") + | some initDecl => match getIOTypeArg initDecl.type with - | none := Except.error ("initialization function '" ++ toString initFnName ++ "' must have type of the form `IO `") - | some initTypeArg := + | none => Except.error ("initialization function '" ++ toString initFnName ++ "' must have type of the form `IO `") + | some initTypeArg => if decl.type == initTypeArg then Except.ok initFnName else Except.error ("initialization function '" ++ toString initFnName ++ "' type mismatch") - | _ := match stx with - | Syntax.missing := + | _ => match stx with + | Syntax.missing => if isIOUnit decl.type then Except.ok Name.anonymous else Except.error "initialization function must have type `IO Unit`" - | _ := Except.error "unexpected kind of argument" + | _ => Except.error "unexpected kind of argument" @[init mkInitAttr] constant initAttr : ParametricAttribute Name := default _ def isIOUnitInitFn (env : Environment) (fn : Name) : Bool := match initAttr.getParam env fn with -| some Name.anonymous := true -| _ := false +| some Name.anonymous => true +| _ => false @[export lean.get_init_fn_name_for_core] def getInitFnNameFor (env : Environment) (fn : Name) : Option Name := match initAttr.getParam env fn with -| some Name.anonymous := none -| some n := some n -| _ := none +| some Name.anonymous => none +| some n => some n +| _ => none def hasInitAttr (env : Environment) (fn : Name) : Bool := (getInitFnNameFor env fn).isSome diff --git a/library/init/lean/compiler/inlineattrs.lean b/library/init/lean/compiler/inlineattrs.lean index 3c0f28f046..3a14aede87 100644 --- a/library/init/lean/compiler/inlineattrs.lean +++ b/library/init/lean/compiler/inlineattrs.lean @@ -44,8 +44,8 @@ private partial def hasInlineAttrAux (env : Environment) (kind : InlineAttribute /- We never inline auxiliary declarations created by eager lambda lifting -/ if isEagerLambdaLiftingName n then false else match inlineAttrs.getValue env n with - | some k := kind == k - | none := if n.isInternal then hasInlineAttrAux n.getPrefix else false + | some k => kind == k + | none => if n.isInternal then hasInlineAttrAux n.getPrefix else false @[export lean.has_inline_attribute_core] def hasInlineAttribute (env : Environment) (n : Name) : Bool := diff --git a/library/init/lean/compiler/ir/basic.lean b/library/init/lean/compiler/ir/basic.lean index da705f1402..a5ae79bdba 100644 --- a/library/init/lean/compiler/ir/basic.lean +++ b/library/init/lean/compiler/ir/basic.lean @@ -348,13 +348,13 @@ reshapeAux bs bs.size term @[inline] def modifyJPs (bs : Array FnBody) (f : FnBody → FnBody) : Array FnBody := bs.map $ fun b => match b with - | FnBody.jdecl j xs v k := FnBody.jdecl j xs (f v) k - | other := other + | FnBody.jdecl j xs v k => FnBody.jdecl j xs (f v) k + | other => other @[inline] def mmodifyJPs {m : Type → Type} [Monad m] (bs : Array FnBody) (f : FnBody → m FnBody) : m (Array FnBody) := bs.mmap $ fun b => match b with - | FnBody.jdecl j xs v k := do v ← f v; pure $ FnBody.jdecl j xs v k - | other := pure other + | FnBody.jdecl j xs v k => do v ← f v; pure $ FnBody.jdecl j xs v k + | other => pure other @[export lean.ir.mk_alt_core] def mkAlt (n : Name) (cidx : Nat) (size : Nat) (usize : Nat) (ssize : Nat) (b : FnBody) : Alt := Alt.ctor ⟨n, cidx, size, usize, ssize⟩ b @@ -411,28 +411,28 @@ ps.foldl LocalContext.addParam ctx def LocalContext.isJP (ctx : LocalContext) (idx : Index) : Bool := match ctx.find idx with -| some (LocalContextEntry.joinPoint _ _) := true -| other := false +| some (LocalContextEntry.joinPoint _ _) => true +| other => false def LocalContext.getJPBody (ctx : LocalContext) (j : JoinPointId) : Option FnBody := match ctx.find j.idx with -| some (LocalContextEntry.joinPoint _ b) := some b -| other := none +| some (LocalContextEntry.joinPoint _ b) => some b +| other => none def LocalContext.getJPParams (ctx : LocalContext) (j : JoinPointId) : Option (Array Param) := match ctx.find j.idx with -| some (LocalContextEntry.joinPoint ys _) := some ys -| other := none +| some (LocalContextEntry.joinPoint ys _) => some ys +| other => none def LocalContext.isParam (ctx : LocalContext) (idx : Index) : Bool := match ctx.find idx with -| some (LocalContextEntry.param _) := true -| other := false +| some (LocalContextEntry.param _) => true +| other => false def LocalContext.isLocalVar (ctx : LocalContext) (idx : Index) : Bool := match ctx.find idx with -| some (LocalContextEntry.localVar _ _) := true -| other := false +| some (LocalContextEntry.localVar _ _) => true +| other => false def LocalContext.contains (ctx : LocalContext) (idx : Index) : Bool := ctx.contains idx @@ -442,9 +442,9 @@ ctx.erase j.idx def LocalContext.getType (ctx : LocalContext) (x : VarId) : Option IRType := match ctx.find x.idx with -| some (LocalContextEntry.param t) := some t -| some (LocalContextEntry.localVar t _) := some t -| other := none +| some (LocalContextEntry.param t) => some t +| some (LocalContextEntry.localVar t _) => some t +| other => none abbrev IndexRenaming := RBMap Index Index Index.lt @@ -455,8 +455,8 @@ export HasAlphaEqv (aeqv) def VarId.alphaEqv (ρ : IndexRenaming) (v₁ v₂ : VarId) : Bool := match ρ.find v₁.idx with -| some v := v == v₂.idx -| none := v₁ == v₂ +| some v => v == v₂.idx +| none => v₁ == v₂ instance VarId.hasAeqv : HasAlphaEqv VarId := ⟨VarId.alphaEqv⟩ @@ -505,8 +505,8 @@ else Array.foldl₂ (fun ρ p₁ p₂ => do ρ ← ρ; addParamRename ρ p₁ p 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 - | some ρ' := FnBody.alphaEqv ρ' v₁ v₂ && FnBody.alphaEqv (addVarRename ρ j₁.idx j₂.idx) b₁ b₂ - | none := false + | 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₂) := @@ -518,9 +518,9 @@ partial def FnBody.alphaEqv : IndexRenaming → FnBody → FnBody → Bool | ρ (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) + | 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 diff --git a/library/init/lean/compiler/ir/borrow.lean b/library/init/lean/compiler/ir/borrow.lean index 7fc3fb0461..20a0d67b85 100644 --- a/library/init/lean/compiler/ir/borrow.lean +++ b/library/init/lean/compiler/ir/borrow.lean @@ -42,8 +42,8 @@ abbrev ParamMap := HashMap Key (Array Param) def ParamMap.fmt (map : ParamMap) : Format := let fmts := map.fold (fun fmt k ps => let k := match k with - | Key.decl n := format n - | Key.jp n id := format n ++ ":" ++ format id; + | Key.decl n => format n + | Key.jp n id => format n ++ ":" ++ format id; fmt ++ Format.line ++ k ++ " -> " ++ formatParams ps) Format.nil; "{" ++ (Format.nest 1 fmts) ++ "}" @@ -80,11 +80,11 @@ partial def visitFnBody (fnid : FunId) : FnBody → State ParamMap Unit def visitDecls (env : Environment) (decls : Array Decl) : State ParamMap Unit := decls.mfor $ fun decl => match decl with - | Decl.fdecl f xs _ b := do + | Decl.fdecl f xs _ b => do let exported := isExport env f; modify $ fun m => m.insert (Key.decl f) (initBorrowIfNotExported exported xs); visitFnBody f b - | _ := pure () + | _ => pure () end InitParamMap def mkInitParamMap (env : Environment) (decls : Array Decl) : ParamMap := @@ -99,8 +99,8 @@ partial def visitFnBody : FnBody → FunId → ParamMap → FnBody let v := visitFnBody v fnid map; let b := visitFnBody b fnid map; match map.find (Key.jp fnid j) with - | some ys := FnBody.jdecl j ys v b - | none := FnBody.jdecl j xs v b + | some ys => FnBody.jdecl j ys v b + | none => FnBody.jdecl j xs v b | e fnid map := if e.isTerminal then e else @@ -110,12 +110,12 @@ partial def visitFnBody : FnBody → FunId → ParamMap → FnBody def visitDecls (decls : Array Decl) (map : ParamMap) : Array Decl := decls.map $ fun decl => match decl with - | Decl.fdecl f xs ty b := + | Decl.fdecl f xs ty b => let b := visitFnBody b f map; match map.find (Key.decl f) with - | some xs := Decl.fdecl f xs ty b - | none := Decl.fdecl f xs ty b - | other := other + | some xs => Decl.fdecl f xs ty b + | none => Decl.fdecl f xs ty b + | other => other end ApplyParamMap @@ -149,8 +149,8 @@ modify $ fun s => def ownArg (x : Arg) : M Unit := match x with -| (Arg.var x) := ownVar x -| _ := pure () +| (Arg.var x) => ownVar x +| _ => pure () def ownArgs (xs : Array Arg) : M Unit := xs.mfor ownArg @@ -164,28 +164,28 @@ def updateParamMap (k : Key) : M Unit := do s ← get; match s.map.find k with -| some ps := do +| some ps => do ps ← ps.mmap $ fun (p : Param) => if p.borrow && s.owned.contains p.x.idx then do markModifiedParamMap; pure { borrow := false, .. p } else pure p; modify $ fun s => { map := s.map.insert k ps, .. s } -| none := pure () +| none => pure () def getParamInfo (k : Key) : M (Array Param) := do s ← get; match s.map.find k with -| some ps := pure ps -| none := +| some ps => pure ps +| none => match k with - | (Key.decl fn) := do + | (Key.decl fn) => do ctx ← read; match findEnvDecl ctx.env fn with - | some decl := pure decl.params - | none := pure Array.empty -- unreachable if well-formed input - | _ := pure Array.empty -- unreachable if well-formed input + | some decl => pure decl.params + | none => pure Array.empty -- unreachable if well-formed input + | _ => pure Array.empty -- unreachable if well-formed input /- For each ps[i], if ps[i] is owned, then mark xs[i] as owned. -/ def ownArgsUsingParams (xs : Array Arg) (ps : Array Param) : M Unit := @@ -204,8 +204,8 @@ xs.size.mfor $ fun i => do let x := xs.get i; let p := ps.get i; match x with - | Arg.var x := mwhen (isOwned x) $ ownVar p.x - | _ := pure () + | Arg.var x => mwhen (isOwned x) $ ownVar p.x + | _ => pure () /- Mark `xs[i]` as owned if it is one of the parameters `ps`. We use this action to mark function parameters that are being "packed" inside constructors. @@ -222,8 +222,8 @@ do ctx ← read; xs.mfor $ fun x => match x with - | Arg.var x := when (ctx.paramSet.contains x.idx) $ ownVar x - | _ := pure () + | Arg.var x => when (ctx.paramSet.contains x.idx) $ ownVar x + | _ => pure () def collectExpr (z : VarId) : Expr → M Unit | (Expr.reset _ x) := ownVar z *> ownVar x @@ -240,12 +240,12 @@ def collectExpr (z : VarId) : Expr → M Unit def preserveTailCall (x : VarId) (v : Expr) (b : FnBody) : M Unit := do ctx ← read; match v, b with -| (Expr.fap g ys), (FnBody.ret (Arg.var z)) := +| (Expr.fap g ys), (FnBody.ret (Arg.var z)) => when (ctx.currFn == g && x == z) $ do -- dbgTrace ("preserveTailCall " ++ toString b) $ fun _ => do ps ← getParamInfo (Key.decl g); ownParamsUsingArgs ys ps -| _, _ := pure () +| _, _ => pure () def updateParamSet (ctx : BorrowInfCtx) (ps : Array Param) : BorrowInfCtx := { paramSet := ps.foldl (fun s p => s.insert p.x.idx) ctx.paramSet, .. ctx } diff --git a/library/init/lean/compiler/ir/boxing.lean b/library/init/lean/compiler/ir/boxing.lean index cf96ffcb73..69a1e8fc1f 100644 --- a/library/init/lean/compiler/ir/boxing.lean +++ b/library/init/lean/compiler/ir/boxing.lean @@ -91,11 +91,11 @@ def getScrutineeType (alts : Array Alt) : IRType := let isScalar := alts.size > 1 && -- Recall that we encode Unit and PUnit using `object`. alts.all (fun alt => match alt with - | Alt.ctor c _ := c.isScalar - | Alt.default _ := false); + | Alt.ctor c _ => c.isScalar + | Alt.default _ => false); match isScalar with -| false := IRType.object -| true := +| false => IRType.object +| true => let n := alts.size; if n < 256 then IRType.uint8 else if n < 65536 then IRType.uint16 @@ -121,18 +121,18 @@ def getResultType : M IRType := BoxingContext.resultType <$> read def getVarType (x : VarId) : M IRType := do localCtx ← getLocalContext; match localCtx.getType x with - | some t := pure t - | none := pure IRType.object -- unreachable, we assume the code is well formed + | some t => pure t + | none => pure IRType.object -- unreachable, we assume the code is well formed def getJPParams (j : JoinPointId) : M (Array Param) := do localCtx ← getLocalContext; match localCtx.getJPParams j with - | some ys := pure ys - | none := pure Array.empty -- unreachable, we assume the code is well formed + | some ys => pure ys + | none => pure Array.empty -- unreachable, we assume the code is well formed def getDecl (fid : FunId) : M Decl := do ctx ← read; match findEnvDecl' ctx.env fid ctx.decls with - | some decl := pure decl - | none := pure (default _) -- unreachable if well-formed + | some decl => pure decl + | none => pure (default _) -- unreachable if well-formed @[inline] def withParams {α : Type} (xs : Array Param) (k : M α) : M α := adaptReader (fun ctx : BoxingContext => { localCtx := ctx.localCtx.addParams xs, .. ctx }) k @@ -159,16 +159,16 @@ do xType ← getVarType x; @[inline] def castArgIfNeeded (x : Arg) (expected : IRType) (k : Arg → M FnBody) : M FnBody := match x with -| Arg.var x := castVarIfNeeded x expected (fun x => k (Arg.var x)) -| _ := k x +| Arg.var x => castVarIfNeeded x expected (fun x => k (Arg.var x)) +| _ => k x @[specialize] def castArgsIfNeededAux (xs : Array Arg) (typeFromIdx : Nat → IRType) : M (Array Arg × Array FnBody) := xs.miterate (Array.empty, Array.empty) $ fun i (x : Arg) (r : Array Arg × Array FnBody) => let expected := typeFromIdx i.val; let (xs, bs) := r; match x with - | Arg.irrelevant := pure (xs.push x, bs) - | Arg.var x := do + | Arg.irrelevant => pure (xs.push x, bs) + | Arg.var x => do xType ← getVarType x; if eqvTypes xType expected then pure (xs.push (Arg.var x), bs) else do @@ -202,26 +202,26 @@ else do def visitVDeclExpr (x : VarId) (ty : IRType) (e : Expr) (b : FnBody) : M FnBody := match e with -| Expr.ctor c ys := +| Expr.ctor c ys => if c.isScalar && ty.isScalar then pure $ FnBody.vdecl x ty (Expr.lit (LitVal.num c.cidx)) b else boxArgsIfNeeded ys $ fun ys => pure $ FnBody.vdecl x ty (Expr.ctor c ys) b -| Expr.reuse w c u ys := +| Expr.reuse w c u ys => boxArgsIfNeeded ys $ fun ys => pure $ FnBody.vdecl x ty (Expr.reuse w c u ys) b -| Expr.fap f ys := do +| Expr.fap f ys => do decl ← getDecl f; castArgsIfNeeded ys decl.params $ fun ys => castResultIfNeeded x ty (Expr.fap f ys) decl.resultType b -| Expr.pap f ys := do +| Expr.pap f ys => do env ← getEnv; decl ← getDecl f; let f := if requiresBoxedVersion env decl then mkBoxedName f else f; boxArgsIfNeeded ys $ fun ys => pure $ FnBody.vdecl x ty (Expr.pap f ys) b -| Expr.ap f ys := +| Expr.ap f ys => boxArgsIfNeeded ys $ fun ys => unboxResultIfNeeded x ty (Expr.ap f ys) b -| other := +| other => pure $ FnBody.vdecl x ty e b partial def visitFnBody : FnBody → M FnBody @@ -259,11 +259,11 @@ partial def visitFnBody : FnBody → M FnBody def run (env : Environment) (decls : Array Decl) : Array Decl := let ctx : BoxingContext := { decls := decls, env := env }; let decls := decls.map (fun decl => match decl with - | Decl.fdecl f xs t b := + | Decl.fdecl f xs t b => let nextIdx := decl.maxIndex + 1; let b := (withParams xs (visitFnBody b) { resultType := t, .. ctx }).run' nextIdx; Decl.fdecl f xs t b - | d := d); + | d => d); addBoxedVersions env decls end ExplicitBoxing diff --git a/library/init/lean/compiler/ir/checker.lean b/library/init/lean/compiler/ir/checker.lean index 85e8869f83..994120ffbe 100644 --- a/library/init/lean/compiler/ir/checker.lean +++ b/library/init/lean/compiler/ir/checker.lean @@ -19,8 +19,8 @@ abbrev M := ExceptT String (ReaderT Context Id) def getDecl (c : Name) : M Decl := do ctx ← read; match findEnvDecl' ctx.env c ctx.decls with - | none := throw ("unknown declaration '" ++ toString c ++ "'") - | some d := pure d + | none => throw ("unknown declaration '" ++ toString c ++ "'") + | some d => pure d def checkVar (x : VarId) : M Unit := do ctx ← read; @@ -32,8 +32,8 @@ do ctx ← read; def checkArg (a : Arg) : M Unit := match a with -| Arg.var x := checkVar x -| other := pure () +| Arg.var x => checkVar x +| other => pure () def checkArgs (as : Array Arg) : M Unit := as.mfor checkArg @@ -48,8 +48,8 @@ def checkScalarType (ty : IRType) : M Unit := checkType ty IRType.isScalar @[inline] def checkVarType (x : VarId) (p : IRType → Bool) : M Unit := do ctx ← read; match ctx.localCtx.getType x with - | some ty := checkType ty p - | none := throw ("unknown variable '" ++ toString x ++ "'") + | some ty => checkType ty p + | none => throw ("unknown variable '" ++ toString x ++ "'") def checkObjVar (x : VarId) : M Unit := checkVarType x IRType.isObj @@ -127,8 +127,8 @@ def checkDecl (decls : Array Decl) (decl : Decl) : CompilerM Unit := do env ← getEnv; match Checker.checkDecl decl { env := env, decls := decls } with -| Except.error msg := throw ("IR check failed at '" ++ toString decl.name ++ "', error: " ++ msg) -| other := pure () +| Except.error msg => throw ("IR check failed at '" ++ toString decl.name ++ "', error: " ++ msg) +| other => pure () def checkDecls (decls : Array Decl) : CompilerM Unit := decls.mfor (checkDecl decls) diff --git a/library/init/lean/compiler/ir/compilerm.lean b/library/init/lean/compiler/ir/compilerm.lean index cab6a8c383..ae7b5e0ae5 100644 --- a/library/init/lean/compiler/ir/compilerm.lean +++ b/library/init/lean/compiler/ir/compilerm.lean @@ -45,8 +45,8 @@ def tracePrefixOptionName := `trace.compiler.ir private def isLogEnabledFor (opts : Options) (optName : Name) : Bool := match opts.find optName with -| some (DataValue.ofBool v) := v -| other := opts.getBool tracePrefixOptionName +| some (DataValue.ofBool v) => v +| other => opts.getBool tracePrefixOptionName private def logDeclsAux (optName : Name) (cls : Name) (decls : Array Decl) : CompilerM Unit := do opts ← read; @@ -124,8 +124,8 @@ decls.mfor addDecl def findEnvDecl' (env : Environment) (n : Name) (decls : Array Decl) : Option Decl := match decls.find (fun decl => if decl.name == n then some decl else none) with -| some decl := some decl -| none := (declMapExt.getState env).find n +| some decl => some decl +| none => (declMapExt.getState env).find n def findDecl' (n : Name) (decls : Array Decl) : CompilerM (Option Decl) := do s ← get; pure $ findEnvDecl' s.env n decls diff --git a/library/init/lean/compiler/ir/default.lean b/library/init/lean/compiler/ir/default.lean index f567a83616..739b39043c 100644 --- a/library/init/lean/compiler/ir/default.lean +++ b/library/init/lean/compiler/ir/default.lean @@ -53,8 +53,8 @@ pure () @[export lean.ir.compile_core] def compile (env : Environment) (opts : Options) (decls : Array Decl) : Log × (Except String Environment) := match (compileAux decls opts).run { env := env } with -| EState.Result.ok _ s := (s.log, Except.ok s.env) -| EState.Result.error msg s := (s.log, Except.error msg) +| EState.Result.ok _ s => (s.log, Except.ok s.env) +| EState.Result.error msg s => (s.log, Except.error msg) end IR end Lean diff --git a/library/init/lean/compiler/ir/elimdead.lean b/library/init/lean/compiler/ir/elimdead.lean index 5411bea880..471cd050be 100644 --- a/library/init/lean/compiler/ir/elimdead.lean +++ b/library/init/lean/compiler/ir/elimdead.lean @@ -24,9 +24,9 @@ partial def reshapeWithoutDeadAux : Array FnBody → FnBody → IndexSet → FnB if used.contains vidx then keep () else reshapeWithoutDeadAux bs b used; match curr with - | FnBody.vdecl x _ _ _ := keepIfUsed x.idx - | FnBody.jdecl j _ _ _ := keepIfUsed j.idx - | _ := keep () + | FnBody.vdecl x _ _ _ => keepIfUsed x.idx + | FnBody.jdecl j _ _ _ => keepIfUsed j.idx + | _ => keep () def reshapeWithoutDead (bs : Array FnBody) (term : FnBody) : FnBody := reshapeWithoutDeadAux bs term term.freeIndices @@ -36,10 +36,10 @@ partial def FnBody.elimDead : FnBody → FnBody let (bs, term) := b.flatten; let bs := modifyJPs bs FnBody.elimDead; let term := match term with - | FnBody.case tid x alts := + | FnBody.case tid x alts => let alts := alts.map $ fun alt => alt.modifyBody FnBody.elimDead; FnBody.case tid x alts - | other := other; + | other => other; reshapeWithoutDead bs term /-- Eliminate dead let-declarations and join points -/ diff --git a/library/init/lean/compiler/ir/emitcpp.lean b/library/init/lean/compiler/ir/emitcpp.lean index 8fa718903e..5b8aa23f0f 100644 --- a/library/init/lean/compiler/ir/emitcpp.lean +++ b/library/init/lean/compiler/ir/emitcpp.lean @@ -37,8 +37,8 @@ def getModName : M Name := Context.modName <$> read def getDecl (n : Name) : M Decl := do env ← getEnv; match findEnvDecl env n with - | some d := pure d - | none := throw ("unknown declaration '" ++ toString n ++ "'") + | some d => pure d + | none => throw ("unknown declaration '" ++ toString n ++ "'") @[inline] def emit {α : Type} [HasToString α] (a : α) : M Unit := modify (fun out => out ++ toString a) @@ -51,8 +51,8 @@ as.mfor $ fun a => emitLn a def argToCppString (x : Arg) : String := match x with -| Arg.var x := toString x -| _ := "lean::box(0)" +| Arg.var x => toString x +| _ => "lean::box(0)" def emitArg (x : Arg) : M Unit := emit (argToCppString x) @@ -79,8 +79,8 @@ openNamespacesAux n.getPrefix def openNamespacesFor (n : Name) : M Unit := do env ← getEnv; match getExportNameFor env n with - | none := pure () - | some n := openNamespaces n + | none => pure () + | some n => openNamespaces n def closeNamespacesAux : Name → M Unit | Name.anonymous := pure () @@ -93,8 +93,8 @@ closeNamespacesAux n.getPrefix def closeNamespacesFor (n : Name) : M Unit := do env ← getEnv; match getExportNameFor env n with - | none := pure () - | some n := closeNamespaces n + | none => pure () + | some n => closeNamespaces n def throwInvalidExportName {α : Type} (n : Name) : M α := throw ("invalid export name '" ++ toString n ++ "'") @@ -102,15 +102,15 @@ throw ("invalid export name '" ++ toString n ++ "'") def toBaseCppName (n : Name) : M String := do env ← getEnv; match getExportNameFor env n with - | some (Name.mkString _ s) := pure s - | some _ := throwInvalidExportName n - | none := if n == `main then pure leanMainFn else pure n.mangle + | some (Name.mkString _ s) => pure s + | some _ => throwInvalidExportName n + | none => if n == `main then pure leanMainFn else pure n.mangle def toCppName (n : Name) : M String := do env ← getEnv; match getExportNameFor env n with - | some s := pure (s.toStringWithSep "::") - | none := if n == `main then pure leanMainFn else pure n.mangle + | some s => pure (s.toStringWithSep "::") + | none => if n == `main then pure leanMainFn else pure n.mangle def emitCppName (n : Name) : M Unit := toCppName n >>= emit @@ -118,9 +118,9 @@ toCppName n >>= emit def toCppInitName (n : Name) : M String := do env ← getEnv; match getExportNameFor env n with - | some (Name.mkString p s) := pure $ (Name.mkString p ("_init_" ++ s)).toStringWithSep "::" - | some _ := throwInvalidExportName n - | none := pure ("_init_" ++ n.mangle) + | some (Name.mkString p s) => pure $ (Name.mkString p ("_init_" ++ s)).toStringWithSep "::" + | some _ => throwInvalidExportName n + | none => pure ("_init_" ++ n.mangle) def emitCppInitName (n : Name) : M Unit := toCppInitName n >>= emit @@ -171,14 +171,14 @@ let usedDecls := usedDecls.toList; usedDecls.mfor $ fun n => do decl ← getDecl n; match getExternNameFor env `cpp decl.name with - | some cppName := emitExternDeclAux decl cppName - | none := emitFnDecl decl (!modDecls.contains n) + | some cppName => emitExternDeclAux decl cppName + | none => emitFnDecl decl (!modDecls.contains n) def emitMainFn : M Unit := do d ← getDecl `main; match d with -| Decl.fdecl f xs t b := do +| Decl.fdecl f xs t b => do unless (xs.size == 2 || xs.size == 1) (throw "invalid main function, incorrect arity when generating code"); env ← getEnv; let usesLeanAPI := usesLeanNamespace env d; @@ -217,7 +217,7 @@ match d with " return 1;", "}"]; emitLn "}" -| other := throw "function declaration expected" +| other => throw "function declaration expected" def hasMainFn : M Bool := do env ← getEnv; @@ -258,14 +258,14 @@ throw ("unknown variable '" ++ toString x ++ "'") def isObj (x : VarId) : M Bool := do ctx ← read; match ctx.varMap.find x with - | some t := pure t.isObj - | none := throwUnknownVar x + | some t => pure t.isObj + | none => throwUnknownVar x def getJPParams (j : JoinPointId) : M (Array Param) := do ctx ← read; match ctx.jpMap.find j with - | some ps := pure ps - | none := throw "unknown join point" + | some ps => pure ps + | none => throw "unknown join point" def declareVar (x : VarId) (t : IRType) : M Unit := do emit (toCppType t); emit " "; emit x; emit "; " @@ -294,8 +294,8 @@ else def isIf (alts : Array Alt) : Option (Nat × FnBody × FnBody) := if alts.size != 2 then none else match alts.get 0 with - | Alt.ctor c b := some (c.cidx, b, (alts.get 1).body) - | _ := none + | Alt.ctor c b => some (c.cidx, b, (alts.get 1).body) + | _ => none def emitIf (emitBody : FnBody → M Unit) (x : VarId) (tag : Nat) (t : FnBody) (e : FnBody) : M Unit := do @@ -306,13 +306,13 @@ emitBody e def emitCase (emitBody : FnBody → M Unit) (x : VarId) (alts : Array Alt) : M Unit := match isIf alts with -| some (tag, t, e) := emitIf emitBody x tag t e -| _ := do +| some (tag, t, e) => emitIf emitBody x tag t e +| _ => do emit "switch ("; emitTag x; emitLn ") {"; let alts := ensureHasDefault alts; alts.mfor $ fun alt => match alt with - | Alt.ctor c b := emit "case " *> emit c.cidx *> emitLn ":" *> emitBody b - | Alt.default b := emitLn "default: " *> emitBody b; + | Alt.ctor c b => emit "case " *> emit c.cidx *> emitLn ":" *> emitBody b + | Alt.default b => emitLn "default: " *> emitBody b; emitLn "}" def emitInc (x : VarId) (n : Nat) (checkRef : Bool) : M Unit := @@ -431,11 +431,11 @@ do emitLhs z; decl ← getDecl f; match decl with -| Decl.extern _ _ _ extData := +| Decl.extern _ _ _ extData => match mkExternCall extData `cpp (toStringArgs ys) with - | some c := emit c *> emitLn ";" - | none := throw "failed to emit extern application" -| _ := do emitCppName f; when (ys.size > 0) (do emit "("; emitArgs ys; emit ")"); emitLn ";" + | some c => emit c *> emitLn ";" + | none => throw "failed to emit extern application" +| _ => do emitCppName f; when (ys.size > 0) (do emit "("; emitArgs ys; emit ")"); emitLn ";" def emitPartialApp (z : VarId) (f : FunId) (ys : Array Arg) : M Unit := do @@ -456,11 +456,11 @@ else do def emitBoxFn (xType : IRType) : M Unit := match xType with -| IRType.usize := emit "lean::box_size_t" -| IRType.uint32 := emit "lean::box_uint32" -| IRType.uint64 := emit "lean::box_uint64" -| IRType.float := throw "floats are not supported yet" -| other := emit "lean::box" +| IRType.usize => emit "lean::box_size_t" +| IRType.uint32 => emit "lean::box_uint32" +| IRType.uint64 => emit "lean::box_uint64" +| IRType.float => throw "floats are not supported yet" +| other => emit "lean::box" def emitBox (z : VarId) (x : VarId) (xType : IRType) : M Unit := do emitLhs z; emitBoxFn xType; emit "("; emit x; emitLn ");" @@ -469,11 +469,11 @@ def emitUnbox (z : VarId) (t : IRType) (x : VarId) : M Unit := do emitLhs z; match t with -| IRType.usize := emit "lean::unbox_size_t" -| IRType.uint32 := emit "lean::unbox_uint32" -| IRType.uint64 := emit "lean::unbox_uint64" -| IRType.float := throw "floats are not supported yet" -| other := emit "lean::unbox"; +| IRType.usize => emit "lean::unbox_size_t" +| IRType.uint32 => emit "lean::unbox_uint32" +| IRType.uint64 => emit "lean::unbox_uint64" +| IRType.float => throw "floats are not supported yet" +| other => emit "lean::unbox"; emit "("; emit x; emitLn ");" def emitIsShared (z : VarId) (x : VarId) : M Unit := @@ -512,37 +512,37 @@ else def emitLit (z : VarId) (t : IRType) (v : LitVal) : M Unit := emitLhs z *> match v with -| LitVal.num v := emitNumLit t v *> emitLn ";" -| LitVal.str v := do emit "lean::mk_string("; emit (quoteString v); emitLn ");" +| LitVal.num v => emitNumLit t v *> emitLn ";" +| LitVal.str v => do emit "lean::mk_string("; emit (quoteString v); emitLn ");" def emitVDecl (z : VarId) (t : IRType) (v : Expr) : M Unit := match v with -| Expr.ctor c ys := emitCtor z c ys -| Expr.reset n x := emitReset z n x -| Expr.reuse x c u ys := emitReuse z x c u ys -| Expr.proj i x := emitProj z i x -| Expr.uproj i x := emitUProj z i x -| Expr.sproj n o x := emitSProj z t n o x -| Expr.fap c ys := emitFullApp z c ys -| Expr.pap c ys := emitPartialApp z c ys -| Expr.ap x ys := emitApp z x ys -| Expr.box t x := emitBox z x t -| Expr.unbox x := emitUnbox z t x -| Expr.isShared x := emitIsShared z x -| Expr.isTaggedPtr x := emitIsTaggedPtr z x -| Expr.lit v := emitLit z t v +| Expr.ctor c ys => emitCtor z c ys +| Expr.reset n x => emitReset z n x +| Expr.reuse x c u ys => emitReuse z x c u ys +| Expr.proj i x => emitProj z i x +| Expr.uproj i x => emitUProj z i x +| Expr.sproj n o x => emitSProj z t n o x +| Expr.fap c ys => emitFullApp z c ys +| Expr.pap c ys => emitPartialApp z c ys +| Expr.ap x ys => emitApp z x ys +| Expr.box t x => emitBox z x t +| Expr.unbox x => emitUnbox z t x +| Expr.isShared x => emitIsShared z x +| Expr.isTaggedPtr x => emitIsTaggedPtr z x +| Expr.lit v => emitLit z t v def isTailCall (x : VarId) (v : Expr) (b : FnBody) : M Bool := do ctx ← read; match v, b with -| Expr.fap f _, FnBody.ret (Arg.var y) := pure $ f == ctx.mainFn && x == y -| _, _ := pure false +| Expr.fap f _, FnBody.ret (Arg.var y) => pure $ f == ctx.mainFn && x == y +| _, _ => pure false def paramEqArg (p : Param) (x : Arg) : Bool := match x with -| Arg.var x := p.x == x -| _ := false +| Arg.var x => p.x == x +| _ => false /- Given `[p_0, ..., p_{n-1}]`, `[y_0, ..., y_{n-1}]`, representing the assignments @@ -567,7 +567,7 @@ n.any $ fun i => def emitTailCall (v : Expr) : M Unit := match v with -| Expr.fap _ ys := do +| Expr.fap _ ys => do ctx ← read; let ps := ctx.mainParams; unless (ps.size == ys.size) (throw "invalid tail call"); @@ -594,7 +594,7 @@ match v with } }; emitLn "goto _start;" -| _ := throw "bug at emitTailCall" +| _ => throw "bug at emitTailCall" partial def emitBlock (emitBody : FnBody → M Unit) : FnBody → M Unit | (FnBody.jdecl j xs v b) := emitBlock b @@ -633,7 +633,7 @@ let (vMap, jpMap) := mkVarJPMaps d; adaptReader (fun ctx : Context => { varMap := vMap, jpMap := jpMap, .. ctx }) $ do unless (hasInitAttr env d.name) $ match d with - | Decl.fdecl f xs t b := do + | Decl.fdecl f xs t b => do openNamespacesFor f; baseName ← toBaseCppName f; emit (toCppType t); emit " "; @@ -654,7 +654,7 @@ unless (hasInitAttr env d.name) $ adaptReader (fun ctx : Context => { mainFn := f, mainParams := xs, .. ctx }) (emitFnBody b); emitLn "}"; closeNamespacesFor f - | _ := pure () + | _ => pure () def emitDecl (d : Decl) : M Unit := let d := d.normalizeIds; @@ -671,8 +671,8 @@ decls.reverse.mfor emitDecl def quoteNameAux : Name → Option String | (Name.mkString Name.anonymous s) := some $ "lean::mk_const_name(" ++ repr s ++ ")" | (Name.mkString p s) := match quoteNameAux p with - | some q := some $ "lean::mk_const_name(" ++ q ++ ", " ++ repr s ++ ")" - | _ := none + | some q => some $ "lean::mk_const_name(" ++ q ++ ", " ++ repr s ++ ")" + | _ => none | _ := none def quoteName (n : Name) : Option String := @@ -688,31 +688,31 @@ if isIOUnitInitFn env n then do { emitLn "if (io_result_is_error(w)) return w;" } else if (d.params.size == 0) then do { match getInitFnNameFor env d.name with - | some initFn := do { + | some initFn => do { emit "w = "; emitCppName initFn; emitLn "(w);"; emitLn "if (io_result_is_error(w)) return w;"; emitCppName n; emitLn " = io_result_get_value(w);" } - | _ := do { + | _ => do { emitCppName n; emit " = "; emitCppInitName n; emitLn "();" }; if d.resultType.isObj then do { emit "lean::mark_persistent("; emitCppName n; emitLn ");"; match quoteName n with - | some q := do emit ("lean::register_constant(" ++ q ++ ", "); emitCppName n; emitLn ");" - | none := pure () + | some q => do emit ("lean::register_constant(" ++ q ++ ", "); emitCppName n; emitLn ");" + | none => pure () } else unless d.resultType.isIrrelevant $ do { match quoteName n with - | some q := do emit ("lean::register_constant(" ++ q ++ ", "); emitBoxFn d.resultType; emit "("; emitCppName n; emitLn "));" - | none := pure () + | some q => do emit ("lean::register_constant(" ++ q ++ ", "); emitBoxFn d.resultType; emit "("; emitCppName n; emitLn "));" + | none => pure () } } else /- TODO(Leo): perhaps we should add a flag to disable closure registration. -/ match quoteName d.name with - | some q := do + | some q => do let clsName := if requiresBoxedVersion env d then mkBoxedName d.name else d.name; emit ("REGISTER_LEAN_FUNCTION(" ++ q ++ ", " ++ toString d.params.size ++ ", "); emitCppName clsName; emitLn ");" - | _ := pure () + | _ => pure () def emitInitFn : M Unit := do @@ -749,8 +749,8 @@ end EmitCpp @[export lean.ir.emit_cpp_core] def emitCpp (env : Environment) (modName : Name) : Except String String := match (EmitCpp.main { env := env, modName := modName }).run "" with -| EState.Result.ok _ s := Except.ok s -| EState.Result.error err _ := Except.error err +| EState.Result.ok _ s => Except.ok s +| EState.Result.error err _ => Except.error err end IR end Lean diff --git a/library/init/lean/compiler/ir/emitutil.lean b/library/init/lean/compiler/ir/emitutil.lean index 89f06a85d3..d41b3b07c2 100644 --- a/library/init/lean/compiler/ir/emitutil.lean +++ b/library/init/lean/compiler/ir/emitutil.lean @@ -15,8 +15,8 @@ namespace IR /- Return true iff `b` is of the form `let x := g ys; ret x` -/ def isTailCallTo (g : Name) (b : FnBody) : Bool := match b with -| FnBody.vdecl x _ (Expr.fap f _) (FnBody.ret (Arg.var y)) := x == y && f == g -| _ := false +| FnBody.vdecl x _ (Expr.fap f _) (FnBody.ret (Arg.var y)) => x == y && f == g +| _ => false namespace UsesLeanNamespace @@ -36,13 +36,13 @@ partial def visitFnBody : FnBody → M Bool modify (fun s => s.insert f); env ← read; match findEnvDecl env f with - | some (Decl.fdecl _ _ _ fbody) := visitFnBody fbody <||> visitFnBody b - | other := visitFnBody b + | some (Decl.fdecl _ _ _ fbody) => visitFnBody fbody <||> visitFnBody b + | other => visitFnBody b }; match v with - | Expr.fap f _ := checkFn f - | Expr.pap f _ := checkFn f - | other := visitFnBody b + | Expr.fap f _ => checkFn f + | Expr.pap f _ => checkFn f + | other => visitFnBody b | (FnBody.jdecl _ _ v b) := visitFnBody v <||> visitFnBody b | (FnBody.case _ _ alts) := alts.anyM $ fun alt => visitFnBody alt.body | e := @@ -66,9 +66,9 @@ modify (fun s => s.insert f) partial def collectFnBody : FnBody → M Unit | (FnBody.vdecl _ _ v b) := match v with - | Expr.fap f _ := collect f *> collectFnBody b - | Expr.pap f _ := collect f *> collectFnBody b - | other := collectFnBody b + | Expr.fap f _ => collect f *> collectFnBody b + | Expr.pap f _ => collect f *> collectFnBody b + | other => collectFnBody b | (FnBody.jdecl _ _ v b) := collectFnBody v *> collectFnBody b | (FnBody.case _ _ alts) := alts.mfor $ fun alt => collectFnBody alt.body | e := unless e.isTerminal $ collectFnBody e.body @@ -76,8 +76,8 @@ partial def collectFnBody : FnBody → M Unit def collectInitDecl (fn : Name) : M Unit := do env ← read; match getInitFnNameFor env fn with - | some initFn := collect initFn - | _ := pure () + | some initFn => collect initFn + | _ => pure () def collectDecl : Decl → M NameSet | (Decl.fdecl fn _ _ b) := collectInitDecl fn *> CollectUsedDecls.collectFnBody b *> get diff --git a/library/init/lean/compiler/ir/expandresetreuse.lean b/library/init/lean/compiler/ir/expandresetreuse.lean index a043785c72..5d3ee581ae 100644 --- a/library/init/lean/compiler/ir/expandresetreuse.lean +++ b/library/init/lean/compiler/ir/expandresetreuse.lean @@ -19,10 +19,10 @@ namespace CollectProjMap abbrev Collector := ProjMap → ProjMap @[inline] def collectVDecl (x : VarId) (v : Expr) : Collector := fun m => match v with - | Expr.proj _ _ := m.insert x v - | Expr.sproj _ _ _ := m.insert x v - | Expr.uproj _ _ := m.insert x v - | _ := m + | Expr.proj _ _ => m.insert x v + | Expr.sproj _ _ _ => m.insert x v + | Expr.uproj _ _ => m.insert x v + | _ => m partial def collectFnBody : FnBody → Collector | (FnBody.vdecl x _ v b) := collectVDecl x v ∘ collectFnBody b @@ -35,8 +35,8 @@ end CollectProjMap This function assumes variable ids have been normalized -/ def mkProjMap (d : Decl) : ProjMap := match d with -| Decl.fdecl _ _ _ b := CollectProjMap.collectFnBody b {} -| _ := {} +| Decl.fdecl _ _ _ b => CollectProjMap.collectFnBody b {} +| _ => {} structure Context := (projMap : ProjMap) @@ -46,8 +46,8 @@ structure Context := partial def consumed (x : VarId) : FnBody → Bool | (FnBody.vdecl _ _ v b) := match v with - | Expr.reuse y _ _ _ := x == y || consumed b - | _ := consumed b + | Expr.reuse y _ _ _ => x == y || consumed b + | _ => consumed b | (FnBody.dec y _ _ b) := x == y || consumed b | (FnBody.case _ _ alts) := alts.all $ fun alt => consumed alt.body | e := !e.isTerminal && consumed e.body @@ -63,13 +63,13 @@ partial def eraseProjIncForAux (y : VarId) : Array FnBody → Mask → Array FnB else let b := bs.back; match b with - | (FnBody.vdecl _ _ (Expr.sproj _ _ _) _) := keepInstr b - | (FnBody.vdecl _ _ (Expr.uproj _ _) _) := keepInstr b - | (FnBody.inc z n c _) := + | (FnBody.vdecl _ _ (Expr.sproj _ _ _) _) => keepInstr b + | (FnBody.vdecl _ _ (Expr.uproj _ _) _) => keepInstr b + | (FnBody.inc z n c _) => if n == 0 then done () else let b' := bs.get (bs.size - 2); match b' with - | (FnBody.vdecl w _ (Expr.proj i x) _) := + | (FnBody.vdecl w _ (Expr.proj i x) _) => if w == z && y == x then /- Found ``` @@ -84,8 +84,8 @@ partial def eraseProjIncForAux (y : VarId) : Array FnBody → Mask → Array FnB let keep := if n == 1 then keep else keep.push (FnBody.inc z (n-1) c FnBody.nil); eraseProjIncForAux bs mask keep else done () - | other := done () - | other := done () + | other => done () + | other => done () /- Try to erase `inc` instructions on projections of `y` occurring in the tail of `bs`. Return the updated `bs` and a bit mask specifying which `inc`s have been removed. -/ @@ -99,10 +99,10 @@ partial def reuseToCtor (x : VarId) : FnBody → FnBody else FnBody.dec y n c (reuseToCtor b) | (FnBody.vdecl z t v b) := match v with - | Expr.reuse y c u xs := + | Expr.reuse y c u xs => if x == y then FnBody.vdecl z t (Expr.ctor c xs) b else FnBody.vdecl z t v (reuseToCtor b) - | _ := + | _ => FnBody.vdecl z t v (reuseToCtor b) | (FnBody.case tid y alts) := let alts := alts.map $ fun alt => alt.modifyBody reuseToCtor; @@ -131,8 +131,8 @@ let b := reuseToCtor x b; let b := FnBody.dec y 1 true b; mask.foldl (fun b m => match m with - | some z := FnBody.inc z 1 true b - | none := b) + | some z => FnBody.inc z 1 true b + | none => b) b abbrev M := ReaderT Context (State Nat) @@ -143,8 +143,8 @@ def releaseUnreadFields (y : VarId) (mask : Mask) (b : FnBody) : M FnBody := mask.size.mfold (fun i b => match mask.get i with - | some _ := pure b -- code took ownership of this field - | none := do + | some _ => pure b -- code took ownership of this field + | none => do fld ← mkFresh; pure (FnBody.vdecl fld IRType.object (Expr.proj i y) (FnBody.dec fld 1 true b))) b @@ -157,23 +157,23 @@ zs.size.fold /- Given `set x[i] := y`, return true iff `y := proj[i] x` -/ def isSelfSet (ctx : Context) (x : VarId) (i : Nat) (y : Arg) : Bool := match y with -| Arg.var y := +| Arg.var y => match ctx.projMap.find y with - | some (Expr.proj j w) := j == i && w == x - | _ := false -| _ := false + | some (Expr.proj j w) => j == i && w == x + | _ => false +| _ => false /- Given `uset x[i] := y`, return true iff `y := uproj[i] x` -/ def isSelfUSet (ctx : Context) (x : VarId) (i : Nat) (y : VarId) : Bool := match ctx.projMap.find y with -| some (Expr.uproj j w) := j == i && w == x -| _ := false +| some (Expr.uproj j w) => j == i && w == x +| _ => false /- Given `sset x[n, i] := y`, return true iff `y := sproj[n, i] x` -/ def isSelfSSet (ctx : Context) (x : VarId) (n : Nat) (i : Nat) (y : VarId) : Bool := match ctx.projMap.find y with -| some (Expr.sproj m j w) := n == m && j == i && w == x -| _ := false +| some (Expr.sproj m j w) => n == m && j == i && w == x +| _ => false /- Remove unnecessary `set/uset/sset` operations -/ partial def removeSelfSet (ctx : Context) : FnBody → FnBody @@ -202,13 +202,13 @@ partial def reuseToSet (ctx : Context) (x y : VarId) : FnBody → FnBody else FnBody.dec z n c (reuseToSet b) | (FnBody.vdecl z t v b) := match v with - | Expr.reuse w c u zs := + | Expr.reuse w c u zs => if x == w then let b := setFields y zs (b.replaceVar z y); let b := if u then FnBody.setTag y c.cidx b else b; removeSelfSet ctx b else FnBody.vdecl z t v (reuseToSet b) - | _ := FnBody.vdecl z t v (reuseToSet b) + | _ => FnBody.vdecl z t v (reuseToSet b) | (FnBody.case tid y alts) := let alts := alts.map $ fun alt => alt.modifyBody reuseToSet; FnBody.case tid y alts @@ -277,12 +277,12 @@ partial def searchAndExpand : FnBody → Array FnBody → M FnBody def main (d : Decl) : Decl := let d := d.normalizeIds; match d with -| (Decl.fdecl f xs t b) := +| (Decl.fdecl f xs t b) => let m := mkProjMap d; let nextIdx := d.maxIndex + 1; let b := (searchAndExpand b Array.empty { projMap := m }).run' nextIdx; Decl.fdecl f xs t b -| d := d +| d => d end ExpandResetReuse diff --git a/library/init/lean/compiler/ir/livevars.lean b/library/init/lean/compiler/ir/livevars.lean index 06245c6cb6..26c8a53c83 100644 --- a/library/init/lean/compiler/ir/livevars.lean +++ b/library/init/lean/compiler/ir/livevars.lean @@ -60,11 +60,11 @@ partial def visitFnBody (w : Index) : FnBody → M Bool | (FnBody.jmp j ys) := visitArgs w ys <||> do { ctx ← get; match ctx.getJPBody j with - | some b := + | some b => -- `j` is not a local join point since we assume we cannot shadow join point declarations. -- Instead of marking the join points that we have already been visited, we permanently remove `j` from the context. set (ctx.eraseJoinPointDecl j) *> visitFnBody b - | none := + | none => -- `j` must be a local join point. So do nothing since we have already visite its body. pure false } @@ -105,8 +105,8 @@ private def accumulate (s' : LiveVarSet) : Collector := fun s => s'.fold (fun s x => s.insert x) s private def collectJP (m : JPLiveVarMap) (j : JoinPointId) : Collector := match m.find j with -| some xs := accumulate xs -| none := skip -- unreachable for well-formed code +| some xs => accumulate xs +| none => skip -- unreachable for well-formed code private def bindVar (x : VarId) : Collector := fun s => s.erase x private def bindParams (ps : Array Param) : Collector := diff --git a/library/init/lean/compiler/ir/normids.lean b/library/init/lean/compiler/ir/normids.lean index 70553c4efa..c271977c02 100644 --- a/library/init/lean/compiler/ir/normids.lean +++ b/library/init/lean/compiler/ir/normids.lean @@ -44,8 +44,8 @@ abbrev M := ReaderT IndexRenaming Id def normIndex (x : Index) : M Index := fun m => match m.find x with -| some y := y -| none := x +| some y => y +| none => x def normVar (x : VarId) : M VarId := VarId.mk <$> normIndex x.idx diff --git a/library/init/lean/compiler/ir/pushproj.lean b/library/init/lean/compiler/ir/pushproj.lean index 5dfa7d778d..0235e3d37b 100644 --- a/library/init/lean/compiler/ir/pushproj.lean +++ b/library/init/lean/compiler/ir/pushproj.lean @@ -28,28 +28,28 @@ partial def pushProjs : Array FnBody → Array Alt → Array IndexSet → Array else skip (); match b with - | FnBody.vdecl x t v _ := + | FnBody.vdecl x t v _ => match v with - | Expr.proj _ _ := push x t v - | Expr.uproj _ _ := push x t v - | Expr.sproj _ _ _ := push x t v - | Expr.isShared _ := skip () - | Expr.isTaggedPtr _ := skip () - | _ := done () - | _ := done () + | Expr.proj _ _ => push x t v + | Expr.uproj _ _ => push x t v + | Expr.sproj _ _ _ => push x t v + | Expr.isShared _ => skip () + | Expr.isTaggedPtr _ => skip () + | _ => done () + | _ => done () partial def FnBody.pushProj : FnBody → FnBody | b := let (bs, term) := b.flatten; let bs := modifyJPs bs FnBody.pushProj; match term with - | FnBody.case tid x alts := + | FnBody.case tid x alts => let altsF := alts.map $ fun alt => alt.body.freeIndices; let (bs, alts) := pushProjs bs alts altsF Array.empty {x.idx}; let alts := alts.map $ fun alt => alt.modifyBody FnBody.pushProj; let term := FnBody.case tid x alts; reshape bs term - | other := reshape bs term + | other => reshape bs term /-- Push projections inside `case` branches. -/ def Decl.pushProj : Decl → Decl diff --git a/library/init/lean/compiler/ir/rc.lean b/library/init/lean/compiler/ir/rc.lean index 3fb053a2fb..b982db0a00 100644 --- a/library/init/lean/compiler/ir/rc.lean +++ b/library/init/lean/compiler/ir/rc.lean @@ -32,23 +32,23 @@ structure Context := def getDecl (ctx : Context) (fid : FunId) : Decl := match findEnvDecl' ctx.env fid ctx.decls with -| some decl := decl -| none := default _ -- unreachable if well-formed +| some decl => decl +| none => default _ -- unreachable if well-formed def getVarInfo (ctx : Context) (x : VarId) : VarInfo := match ctx.varMap.find x with -| some info := info -| none := {} -- unreachable in well-formed code +| some info => info +| none => {} -- unreachable in well-formed code def getJPParams (ctx : Context) (j : JoinPointId) : Array Param := match ctx.localCtx.getJPParams j with -| some ps := ps -| none := Array.empty -- unreachable in well-formed code +| some ps => ps +| none => Array.empty -- unreachable in well-formed code def getJPLiveVars (ctx : Context) (j : JoinPointId) : LiveVarSet := match ctx.jpLiveVarMap.find j with -| some s := s -| none := {} +| some s => s +| none => {} def mustConsume (ctx : Context) (x : VarId) : Bool := let info := getVarInfo ctx x; @@ -64,8 +64,8 @@ private def updateRefUsingCtorInfo (ctx : Context) (x : VarId) (c : CtorInfo) : if c.isRef then ctx else let m := ctx.varMap; { varMap := match m.find x with - | some info := m.insert x { ref := false, .. info } -- I really want a Lenses library + notation - | none := m, + | some info => m.insert x { ref := false, .. info } -- I really want a Lenses library + notation + | none => m, .. ctx } private def addDecForAlt (ctx : Context) (caseLiveVars altLiveVars : LiveVarSet) (b : FnBody) : FnBody := @@ -85,8 +85,8 @@ private def isBorrowParamAux (x : VarId) (ys : Array Arg) (consumeParamPred : Na ys.size.any $ fun i => let y := ys.get i; match y with - | Arg.irrelevant := false - | Arg.var y := x == y && !consumeParamPred i + | Arg.irrelevant => false + | Arg.var y => x == y && !consumeParamPred i private def isBorrowParam (x : VarId) (ys : Array Arg) (ps : Array Param) : Bool := isBorrowParamAux x ys (fun i => !(ps.get i).borrow) @@ -102,8 +102,8 @@ ys.size.fold (fun i n => let y := ys.get i; match y with - | Arg.irrelevant := n - | Arg.var y := if x == y && consumeParamPred i then n+1 else n) + | Arg.irrelevant => n + | Arg.var y => if x == y && consumeParamPred i then n+1 else n) 0 @[specialize] @@ -112,8 +112,8 @@ xs.size.fold (fun i b => let x := xs.get i; match x with - | Arg.irrelevant := b - | Arg.var x := + | Arg.irrelevant => b + | Arg.var x => let info := getVarInfo ctx x; if !info.ref || info.persistent || !isFirstOcc xs i then b else @@ -138,8 +138,8 @@ private def addDecAfterFullApp (ctx : Context) (xs : Array Arg) (ps : Array Para xs.size.fold (fun i b => match xs.get i with - | Arg.irrelevant := b - | Arg.var x := + | Arg.irrelevant => b + | Arg.var x => /- We must add a `dec` if `x` must be consumed, it is alive after the application, and it has been borrowed by the application. Remark: `x` may occur multiple times in the application (e.g., `f x y x`). @@ -166,17 +166,17 @@ private def isPersistent : Expr → Bool /- We do not need to consume the projection of a variable that is not consumed -/ private def consumeExpr (m : VarMap) : Expr → Bool | (Expr.proj i x) := match m.find x with - | some info := info.consume - | none := true + | some info => info.consume + | none => true | other := true /- Return true iff `v` at runtime is a scalar value stored in a tagged pointer. We do not need RC operations for this kind of value. -/ private def isScalarBoxedInTaggedPtr (v : Expr) : Bool := match v with -| Expr.ctor c ys := c.size == 0 && c.ssize == 0 && c.usize == 0 -| Expr.lit (LitVal.num n) := n ≤ maxSmallNat -| _ := false +| Expr.ctor c ys => c.size == 0 && c.ssize == 0 && c.usize == 0 +| Expr.lit (LitVal.num n) => n ≤ maxSmallNat +| _ => false private def updateVarInfo (ctx : Context) (x : VarId) (t : IRType) (v : Expr) : Context := { varMap := ctx.varMap.insert x { @@ -191,26 +191,26 @@ if mustConsume ctx x && !bLiveVars.contains x then addDec x b else b private def processVDecl (ctx : Context) (z : VarId) (t : IRType) (v : Expr) (b : FnBody) (bLiveVars : LiveVarSet) : FnBody × LiveVarSet := -- dbgTrace ("processVDecl " ++ toString z ++ " " ++ toString (format v)) $ fun _ => let b := match v with - | (Expr.ctor _ ys) := addIncBeforeConsumeAll ctx ys (FnBody.vdecl z t v b) bLiveVars - | (Expr.reuse _ _ _ ys) := addIncBeforeConsumeAll ctx ys (FnBody.vdecl z t v b) bLiveVars - | (Expr.proj _ x) := + | (Expr.ctor _ ys) => addIncBeforeConsumeAll ctx ys (FnBody.vdecl z t v b) bLiveVars + | (Expr.reuse _ _ _ ys) => addIncBeforeConsumeAll ctx ys (FnBody.vdecl z t v b) bLiveVars + | (Expr.proj _ x) => let b := addDecIfNeeded ctx x b bLiveVars; let b := if (getVarInfo ctx x).consume then addInc z b else b; (FnBody.vdecl z t v b) - | (Expr.uproj _ x) := FnBody.vdecl z t v (addDecIfNeeded ctx x b bLiveVars) - | (Expr.sproj _ _ x) := FnBody.vdecl z t v (addDecIfNeeded ctx x b bLiveVars) - | (Expr.fap f ys) := + | (Expr.uproj _ x) => FnBody.vdecl z t v (addDecIfNeeded ctx x b bLiveVars) + | (Expr.sproj _ _ x) => FnBody.vdecl z t v (addDecIfNeeded ctx x b bLiveVars) + | (Expr.fap f ys) => -- dbgTrace ("processVDecl " ++ toString v) $ fun _ => let ps := (getDecl ctx f).params; let b := addDecAfterFullApp ctx ys ps b bLiveVars; let b := FnBody.vdecl z t v b; addIncBefore ctx ys ps b bLiveVars - | (Expr.pap _ ys) := addIncBeforeConsumeAll ctx ys (FnBody.vdecl z t v b) bLiveVars - | (Expr.ap x ys) := + | (Expr.pap _ ys) => addIncBeforeConsumeAll ctx ys (FnBody.vdecl z t v b) bLiveVars + | (Expr.ap x ys) => let ysx := ys.push (Arg.var x); -- TODO: avoid temporary array allocation addIncBeforeConsumeAll ctx ysx (FnBody.vdecl z t v b) bLiveVars - | (Expr.unbox x) := FnBody.vdecl z t v (addDecIfNeeded ctx x b bLiveVars) - | other := FnBody.vdecl z t v b; -- Expr.reset, Expr.box, Expr.lit are handled here + | (Expr.unbox x) => FnBody.vdecl z t v (addDecIfNeeded ctx x b bLiveVars) + | other => FnBody.vdecl z t v b; -- Expr.reset, Expr.box, Expr.lit are handled here let liveVars := updateLiveVars v bLiveVars; let liveVars := liveVars.erase z; (b, liveVars) @@ -246,22 +246,22 @@ partial def visitFnBody : FnBody → Context → (FnBody × LiveVarSet) | b@(FnBody.case tid x alts) ctx := let caseLiveVars := collectLiveVars b ctx.jpLiveVarMap; let alts := alts.map $ fun alt => match alt with - | Alt.ctor c b := + | Alt.ctor c b => let ctx := updateRefUsingCtorInfo ctx x c; let (b, altLiveVars) := visitFnBody b ctx; let b := addDecForAlt ctx caseLiveVars altLiveVars b; Alt.ctor c b - | Alt.default b := + | Alt.default b => let (b, altLiveVars) := visitFnBody b ctx; let b := addDecForAlt ctx caseLiveVars altLiveVars b; Alt.default b; (FnBody.case tid x alts, caseLiveVars) | b@(FnBody.ret x) ctx := match x with - | Arg.var x := + | Arg.var x => let info := getVarInfo ctx x; if info.ref && !info.persistent && !info.consume then (addInc x b, {x}) else (b, {x}) - | _ := (b, {}) + | _ => (b, {}) | b@(FnBody.jmp j xs) ctx := let jLiveVars := getJPLiveVars ctx j; let ps := getJPParams ctx j; diff --git a/library/init/lean/compiler/ir/resetreuse.lean b/library/init/lean/compiler/ir/resetreuse.lean index 0964e01b69..0b55f38660 100644 --- a/library/init/lean/compiler/ir/resetreuse.lean +++ b/library/init/lean/compiler/ir/resetreuse.lean @@ -74,13 +74,13 @@ private def Dfinalize (x : VarId) (c : CtorInfo) : FnBody × Bool → M FnBody private def argsContainsVar (ys : Array Arg) (x : VarId) : Bool := ys.any $ fun arg => match arg with - | Arg.var y := x == y - | _ := false + | Arg.var y => x == y + | _ => false private def isCtorUsing (b : FnBody) (x : VarId) : Bool := match b with -| (FnBody.vdecl _ _ (Expr.ctor _ ys) _) := argsContainsVar ys x -| _ := false +| (FnBody.vdecl _ _ (Expr.ctor _ ys) _) => argsContainsVar ys x +| _ => false /- Given `Dmain b`, the resulting pair `(new_b, flag)` contains the new body `new_b`, and `flag == true` if `x` is live in `b`. @@ -132,10 +132,10 @@ partial def R : FnBody → M FnBody alts ← alts.mmap $ fun alt => do { alt ← alt.mmodifyBody R; match alt with - | Alt.ctor c b := + | Alt.ctor c b => if c.isScalar then pure alt else Alt.ctor c <$> D x c b - | _ := pure alt + | _ => pure alt }; pure $ FnBody.case tid x alts | (FnBody.jdecl j ys v b) := do diff --git a/library/init/lean/compiler/ir/simpcase.lean b/library/init/lean/compiler/ir/simpcase.lean index d3505bbae7..1c875d0c56 100644 --- a/library/init/lean/compiler/ir/simpcase.lean +++ b/library/init/lean/compiler/ir/simpcase.lean @@ -52,10 +52,10 @@ partial def FnBody.simpCase : FnBody → FnBody let (bs, term) := b.flatten; let bs := modifyJPs bs FnBody.simpCase; match term with - | FnBody.case tid x alts := + | FnBody.case tid x alts => let alts := alts.map $ fun alt => alt.modifyBody FnBody.simpCase; reshape bs (mkSimpCase tid x alts) - | other := reshape bs term + | other => reshape bs term /-- Simplify `case` - Remove unreachable branches. diff --git a/library/init/lean/compiler/namemangling.lean b/library/init/lean/compiler/namemangling.lean index 873e6993e6..28909d5ce7 100644 --- a/library/init/lean/compiler/namemangling.lean +++ b/library/init/lean/compiler/namemangling.lean @@ -40,8 +40,8 @@ private def Name.mangleAux : Name → String | (Name.mkString p s) := let m := String.mangle s; match p with - | Name.anonymous := m - | _ := Name.mangleAux p ++ "_" ++ m + | Name.anonymous => m + | _ => Name.mangleAux p ++ "_" ++ m | (Name.mkNumeral p n) := Name.mangleAux p ++ "_" ++ toString n ++ "_" def Name.mangle (n : Name) (pre : String := "l_") : String := diff --git a/library/init/lean/compiler/specialize.lean b/library/init/lean/compiler/specialize.lean index ebbbfdce2f..2680b88311 100644 --- a/library/init/lean/compiler/specialize.lean +++ b/library/init/lean/compiler/specialize.lean @@ -37,8 +37,8 @@ constant specializeAttrs : EnumAttributes SpecializeAttributeKind := default _ private partial def hasSpecializeAttrAux (env : Environment) (kind : SpecializeAttributeKind) : Name → Bool | n := match specializeAttrs.getValue env n with - | some k := kind == k - | none := if n.isInternal then hasSpecializeAttrAux n.getPrefix else false + | some k => kind == k + | none => if n.isInternal then hasSpecializeAttrAux n.getPrefix else false @[export lean.has_specialize_attribute_core] def hasSpecializeAttribute (env : Environment) (n : Name) : Bool := @@ -72,8 +72,8 @@ instance : Inhabited SpecState := ⟨{}⟩ def addEntry (s : SpecState) (e : SpecEntry) : SpecState := match e with -| SpecEntry.info name info := { specInfo := s.specInfo.insert name info, .. s } -| SpecEntry.cache key fn := { cache := s.cache.insert key fn, .. s } +| SpecEntry.info name info => { specInfo := s.specInfo.insert name info, .. s } +| SpecEntry.cache key fn => { cache := s.cache.insert key fn, .. s } def switch : SpecState → SpecState | ⟨m₁, m₂⟩ := ⟨m₁.switch, m₂.switch⟩ diff --git a/library/init/lean/compiler/util.lean b/library/init/lean/compiler/util.lean index e7cb50b129..23a72b8b67 100644 --- a/library/init/lean/compiler/util.lean +++ b/library/init/lean/compiler/util.lean @@ -24,8 +24,8 @@ def Visitor := AtMostOnceData → AtMostOnceData @[inline] def seq (f g : Visitor) : Visitor := fun d => match f d with -| ⟨found, false⟩ := ⟨found, false⟩ -| other := g other +| ⟨found, false⟩ => ⟨found, false⟩ +| other => g other instance : HasAndthen Visitor := ⟨seq⟩ @@ -78,9 +78,9 @@ private def getDeclNamesForCodeGen : Declaration → List Name def checkIsDefinition (env : Environment) (n : Name) : Except String Unit := match env.find n with -| (some (ConstantInfo.defnInfo _)) := Except.ok () -| none := Except.error "unknow declaration" -| _ := Except.error "declaration is not a definition" +| (some (ConstantInfo.defnInfo _)) => Except.ok () +| none => Except.error "unknow declaration" +| _ => Except.error "declaration is not a definition" end Compiler end Lean diff --git a/library/init/lean/environment.lean b/library/init/lean/environment.lean index c188f3251c..df5b54321e 100644 --- a/library/init/lean/environment.lean +++ b/library/init/lean/environment.lean @@ -83,8 +83,8 @@ env.const2ModIdx.find c def isConstructor (env : Environment) (c : Name) : Bool := match env.find c with -| ConstantInfo.ctorInfo _ := true -| _ := false +| ConstantInfo.ctorInfo _ => true +| _ => false /-- Type check, add and compile the given declaration. @@ -279,7 +279,7 @@ registerPersistentEnvExtension { name := descr.name, addImportedFn := fun as => ([], descr.addImportedFn as), addEntryFn := fun s e => match s with - | (entries, s) := (e::entries, descr.addEntryFn s e), + | (entries, s) => (e::entries, descr.addEntryFn s e), exportEntriesFn := fun s => descr.toArrayFn s.1.reverse, statsFn := fun s => format "number of local entries: " ++ format s.1.length } diff --git a/library/init/lean/evalconst.lean b/library/init/lean/evalconst.lean index 2375df627c..17a80eef52 100644 --- a/library/init/lean/evalconst.lean +++ b/library/init/lean/evalconst.lean @@ -34,7 +34,7 @@ modifyConstTable (fun cs => cs.qsort (fun e₁ e₂ => Name.quickLt e₁.1 e₂. unsafe def evalConst (α : Type) [Inhabited α] (c : Name) : IO α := do cs ← getConstTable; match cs.binSearch (c, default _) (fun e₁ e₂ => Name.quickLt e₁.1 e₂.1) with - | some (_, v) := pure (unsafeCast v) - | none := throw (IO.userError ("unknow constant '" ++ toString c ++ "'")) + | some (_, v) => pure (unsafeCast v) + | none => throw (IO.userError ("unknow constant '" ++ toString c ++ "'")) end Lean diff --git a/library/init/lean/expr.lean b/library/init/lean/expr.lean index 1043e58ee8..bbf4ab1456 100644 --- a/library/init/lean/expr.lean +++ b/library/init/lean/expr.lean @@ -107,8 +107,8 @@ getAppNumArgsAux e 0 def isAppOf (e : Expr) (n : Name) : Bool := match e.getAppFn with -| Expr.const c _ := c == n -| _ := false +| Expr.const c _ => c == n +| _ => false def isAppOfArity : Expr → Name → Nat → Bool | (Expr.const c _) n 0 := c == n diff --git a/library/init/lean/kvmap.lean b/library/init/lean/kvmap.lean index d71791aaf8..65f8c8df55 100644 --- a/library/init/lean/kvmap.lean +++ b/library/init/lean/kvmap.lean @@ -55,28 +55,28 @@ def contains (m : KVMap) (n : Name) : Bool := def getString (m : KVMap) (k : Name) (defVal := "") : String := match m.find k with -| some (DataValue.ofString v) := v -| _ := defVal +| some (DataValue.ofString v) => v +| _ => defVal def getNat (m : KVMap) (k : Name) (defVal := 0) : Nat := match m.find k with -| some (DataValue.ofNat v) := v -| _ := defVal +| some (DataValue.ofNat v) => v +| _ => defVal def getInt (m : KVMap) (k : Name) (defVal : Int := 0) : Int := match m.find k with -| some (DataValue.ofInt v) := v -| _ := defVal +| some (DataValue.ofInt v) => v +| _ => defVal def getBool (m : KVMap) (k : Name) (defVal := false) : Bool := match m.find k with -| some (DataValue.ofBool v) := v -| _ := defVal +| some (DataValue.ofBool v) => v +| _ => defVal def getName (m : KVMap) (k : Name) (defVal := Name.anonymous) : Name := match m.find k with -| some (DataValue.ofName v) := v -| _ := defVal +| some (DataValue.ofName v) => v +| _ => defVal def setString (m : KVMap) (k : Name) (v : String) : KVMap := m.insert k (DataValue.ofString v) @@ -97,8 +97,8 @@ def subsetAux : List (Name × DataValue) → KVMap → Bool | [] m₂ := true | ((k, v₁)::m₁) m₂ := match m₂.find k with - | some v₂ := v₁ == v₂ && subsetAux m₁ m₂ - | none := false + | some v₂ => v₁ == v₂ && subsetAux m₁ m₂ + | none => false def subset : KVMap → KVMap → Bool | ⟨m₁⟩ m₂ := subsetAux m₁ m₂ diff --git a/library/init/lean/level.lean b/library/init/lean/level.lean index c2f213f0d1..a46408df5f 100644 --- a/library/init/lean/level.lean +++ b/library/init/lean/level.lean @@ -67,8 +67,8 @@ def Level.instantiate (s : Name → Option Level) : Level → Level | (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 + | some l' => l' + | none => l | l := l @[extern "lean_level_hash"] diff --git a/library/init/lean/message.lean b/library/init/lean/message.lean index b1bdbab9e1..0ec37f6a6e 100644 --- a/library/init/lean/message.lean +++ b/library/init/lean/message.lean @@ -25,9 +25,9 @@ namespace Message protected def toString (msg : Message) : String := msg.filename ++ ":" ++ toString msg.pos.line ++ ":" ++ toString msg.pos.column ++ ": " ++ (match msg.severity with - | MessageSeverity.information := "" - | MessageSeverity.warning := "warning: " - | MessageSeverity.error := "error: ") ++ + | MessageSeverity.information => "" + | MessageSeverity.warning => "warning: " + | MessageSeverity.error => "error: ") ++ (if msg.caption = "" then "" else msg.caption ++ ":\n") ++ msg.text @@ -57,8 +57,8 @@ instance : HasAppend MessageLog := def hasErrors (log : MessageLog) : Bool := log.revList.any $ fun m => match m.severity with -| MessageSeverity.error := true -| _ := false +| MessageSeverity.error => true +| _ => false def toList (log : MessageLog) : List Message := log.revList.reverse diff --git a/library/init/lean/modifiers.lean b/library/init/lean/modifiers.lean index 03e8b9a5e3..c27865403e 100644 --- a/library/init/lean/modifiers.lean +++ b/library/init/lean/modifiers.lean @@ -26,8 +26,8 @@ protectedExt.addEntry env n @[export lean.is_protected_core] def isProtected (env : Environment) (n : Name) : Bool := match env.getModuleIdxFor n with -| some modIdx := (protectedExt.getModuleEntries env modIdx).binSearchContains n Name.quickLt -| none := (protectedExt.getState env).contains n +| some modIdx => (protectedExt.getModuleEntries env modIdx).binSearchContains n Name.quickLt +| none => (protectedExt.getState env).contains n def mkPrivateExtension : IO (EnvExtension Nat) := registerEnvExtension 1 diff --git a/library/init/lean/name.lean b/library/init/lean/name.lean index 96ad470a15..c9396e1eea 100644 --- a/library/init/lean/name.lean +++ b/library/init/lean/name.lean @@ -62,14 +62,14 @@ protected def decEq : ∀ (a b : @& Name), Decidable (a = b) | (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₂ + | 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₂) := 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₂ + | 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 diff --git a/library/init/lean/options.lean b/library/init/lean/options.lean index ce80668d58..27b27a1190 100644 --- a/library/init/lean/options.lean +++ b/library/init/lean/options.lean @@ -54,16 +54,16 @@ do let ps := (entry.split "=").map String.trim; [key, val] ← pure ps | throw "invalid configuration option entry, it must be of the form ' = '"; defValue ← getOptionDefaulValue key.toName; match defValue with - | DataValue.ofString v := pure $ opts.setString key val - | DataValue.ofBool v := + | DataValue.ofString v => pure $ opts.setString key val + | DataValue.ofBool v => if key == "true" then pure $ opts.setBool key true else if key == "false" then pure $ opts.setBool key false else throw $ IO.userError ("invalid Bool option value '" ++ val ++ "'") - | DataValue.ofName v := pure $ opts.setName key val.toName - | DataValue.ofNat v := do + | DataValue.ofName v => pure $ opts.setName key val.toName + | DataValue.ofNat v => do unless val.isNat $ throw (IO.userError ("invalid Nat option value '" ++ val ++ "'")); pure $ opts.setNat key val.toNat - | DataValue.ofInt v := do + | DataValue.ofInt v => do unless val.isInt $ throw (IO.userError ("invalid Int option value '" ++ val ++ "'")); pure $ opts.setInt key val.toInt diff --git a/library/init/lean/parser/parser.lean b/library/init/lean/parser/parser.lean index 4621872b66..832921be6b 100644 --- a/library/init/lean/parser/parser.lean +++ b/library/init/lean/parser/parser.lean @@ -96,14 +96,14 @@ def next (s : ParserState) (input : String) (pos : Nat) : ParserState := def toErrorMsg (ctx : ParserContext) (s : ParserState) : String := match s.errorMsg with -| none := "" -| some msg := +| none => "" +| some msg => let pos := ctx.fileMap.toPosition s.pos; ctx.filename ++ ":" ++ toString pos.line ++ ":" ++ toString pos.column ++ " " ++ msg def mkNode (s : ParserState) (k : SyntaxNodeKind) (iniStackSz : Nat) : ParserState := match s with -| ⟨stack, pos, cache, err⟩ := +| ⟨stack, pos, cache, err⟩ => if err != none && stack.size == iniStackSz then -- If there is an error but there are no new nodes on the stack, we just return `d` s @@ -115,14 +115,14 @@ match s with def mkError (s : ParserState) (msg : String) : ParserState := match s with -| ⟨stack, pos, cache, _⟩ := ⟨stack, pos, cache, some msg⟩ +| ⟨stack, pos, cache, _⟩ => ⟨stack, pos, cache, some msg⟩ def mkEOIError (s : ParserState) : ParserState := s.mkError "end of input" def mkErrorAt (s : ParserState) (msg : String) (pos : String.Pos) : ParserState := match s with -| ⟨stack, _, cache, _⟩ := ⟨stack, pos, cache, some msg⟩ +| ⟨stack, _, cache, _⟩ => ⟨stack, pos, cache, some msg⟩ end ParserState @@ -264,8 +264,8 @@ instance hashOrelse {k : ParserKind} : HasOrelse (Parser k) := let iniSz := s.stackSize; let iniPos := s.pos; match p a c s with - | ⟨stack, _, cache, some msg⟩ := ⟨stack.shrink iniSz, iniPos, cache, some msg⟩ - | other := other + | ⟨stack, _, cache, some msg⟩ => ⟨stack.shrink iniSz, iniPos, cache, some msg⟩ + | other => other @[inline] def try {k : ParserKind} (p : Parser k) : Parser k := { info := noFirstTokenInfo p.info, @@ -581,8 +581,8 @@ def isIdCont : String → ParserState → Bool private def isToken (idStartPos idStopPos : Nat) (tk : Option TokenConfig) : Bool := match tk with -| none := false -| some tk := +| none => false +| some tk => -- if a token is both a symbol and a valid identifier (i.e. a keyword), -- we want it to be recognized as a symbol tk.val.bsize ≥ idStopPos - idStopPos @@ -590,8 +590,8 @@ match tk with def mkTokenAndFixPos (startPos : Nat) (tk : Option TokenConfig) : BasicParserFn := fun c s => match tk with -| none := s.mkErrorAt "token expected" startPos -| some tk := +| none => s.mkErrorAt "token expected" startPos +| some tk => let input := c.input; let leading := mkEmptySubstringAt input startPos; let val := tk.val; @@ -665,12 +665,12 @@ private def tokenFnAux : BasicParserFn private def updateCache (startPos : Nat) (s : ParserState) : ParserState := match s with -| ⟨stack, pos, cache, none⟩ := +| ⟨stack, pos, cache, none⟩ => if stack.size == 0 then s else let tk := stack.back; ⟨stack, pos, { tokenCache := { startPos := startPos, stopPos := pos, token := tk } }, none⟩ -| other := other +| other => other def tokenFn : BasicParserFn := fun c s => @@ -703,8 +703,8 @@ fun c s => s.mkErrorAt errorMsg startPos else match s.stxStack.back with - | Syntax.atom _ sym := if p sym then s else s.mkErrorAt errorMsg startPos - | _ := s.mkErrorAt errorMsg startPos + | Syntax.atom _ sym => if p sym then s else s.mkErrorAt errorMsg startPos + | _ => s.mkErrorAt errorMsg startPos def symbolFnAux (sym : String) (errorMsg : String) : BasicParserFn := satisfySymbolFn (fun s => s == sym) errorMsg @@ -712,12 +712,12 @@ satisfySymbolFn (fun s => s == sym) errorMsg def insertToken (sym : String) (lbp : Option Nat) (tks : Trie TokenConfig) : ExceptT String Id (Trie TokenConfig) := if sym == "" then throw "invalid empty symbol" else match tks.find sym, lbp with -| none, _ := pure (tks.insert sym { val := sym, lbp := lbp }) -| some _, none := pure tks -| some tk, some newLbp := +| none, _ => pure (tks.insert sym { val := sym, lbp := lbp }) +| some _, none => pure tks +| some tk, some newLbp => match tk.lbp with - | none := pure (tks.insert sym { val := sym, lbp := lbp }) - | some oldLbp := if newLbp == oldLbp then pure tks else throw ("precedence mismatch for '" ++ toString sym ++ "', previous: " ++ toString oldLbp ++ ", new: " ++ toString newLbp) + | none => pure (tks.insert sym { val := sym, lbp := lbp }) + | some oldLbp => if newLbp == oldLbp then pure tks else throw ("precedence mismatch for '" ++ toString sym ++ "', previous: " ++ toString oldLbp ++ ", new: " ++ toString newLbp) def symbolInfo (sym : String) (lbp : Option Nat) : ParserInfo := { updateTokens := insertToken sym lbp, @@ -785,20 +785,20 @@ namespace ParserState def keepNewError (s : ParserState) (oldStackSize : Nat) : ParserState := match s with -| ⟨stack, pos, cache, err⟩ := ⟨stack.shrink oldStackSize, pos, cache, err⟩ +| ⟨stack, pos, cache, err⟩ => ⟨stack.shrink oldStackSize, pos, cache, err⟩ def keepPrevError (s : ParserState) (oldStackSize : Nat) (oldStopPos : String.Pos) (oldError : Option String) : ParserState := match s with -| ⟨stack, _, cache, _⟩ := ⟨stack.shrink oldStackSize, oldStopPos, cache, oldError⟩ +| ⟨stack, _, cache, _⟩ => ⟨stack.shrink oldStackSize, oldStopPos, cache, oldError⟩ def mergeErrors (s : ParserState) (oldStackSize : Nat) (oldError : String) : ParserState := match s with -| ⟨stack, pos, cache, some err⟩ := ⟨stack.shrink oldStackSize, pos, cache, some (err ++ "; " ++ oldError)⟩ -| other := other +| ⟨stack, pos, cache, some err⟩ => ⟨stack.shrink oldStackSize, pos, cache, some (err ++ "; " ++ oldError)⟩ +| other => other def mkLongestNodeAlt (s : ParserState) (startSize : Nat) : ParserState := match s with -| ⟨stack, pos, cache, _⟩ := +| ⟨stack, pos, cache, _⟩ => if stack.size == startSize then ⟨stack.push Syntax.missing, pos, cache, none⟩ -- parser did not create any node, then we just add `Syntax.missing` else if stack.size == startSize + 1 then s else @@ -809,7 +809,7 @@ match s with def keepLatest (s : ParserState) (startStackSize : Nat) : ParserState := match s with -| ⟨stack, pos, cache, _⟩ := +| ⟨stack, pos, cache, _⟩ => let node := stack.back; let stack := stack.shrink startStackSize; let stack := stack.push node; @@ -829,17 +829,17 @@ let prevSize := s.stackSize; let s := s.restore prevSize startPos; let s := p a c s; match prevErrorMsg, s.errorMsg with -| none, none := -- both succeeded +| none, none => -- both succeeded if s.pos > prevStopPos then s.replaceLongest startSize prevSize -- replace else if s.pos < prevStopPos then s.restore prevSize prevStopPos -- keep prev else s.mkLongestNodeAlt prevSize -- keep both -| none, some _ := -- prev succeeded, current failed +| none, some _ => -- prev succeeded, current failed s.restore prevSize prevStopPos -| some oldError, some _ := -- both failed +| some oldError, some _ => -- both failed if s.pos > prevStopPos then s.keepNewError prevSize else if s.pos < prevStopPos then s.keepPrevError prevSize prevStopPos prevErrorMsg else s.mergeErrors prevSize oldError -| some _, none := -- prev failed, current succeeded +| some _, none => -- prev failed, current succeeded s.mkLongestNodeAlt startSize def longestMatchMkResult (startSize : Nat) (s : ParserState) : ParserState := @@ -883,8 +883,8 @@ namespace TokenMap def insert {α : Type} (map : TokenMap α) (k : Name) (v : α) : TokenMap α := match map.find k with -| none := map.insert k [v] -| some vs := map.insert k (v::vs) +| none => map.insert k [v] +| some vs => map.insert k (v::vs) instance {α : Type} : Inhabited (TokenMap α) := ⟨RBMap.empty⟩ @@ -901,25 +901,25 @@ structure ParsingTables := def currLbp (c : ParserContext) (s : ParserState) : ParserState × Nat := let (s, stx) := peekToken c s; match stx with -| some (Syntax.atom _ sym) := +| some (Syntax.atom _ sym) => match c.tokens.matchPrefix sym 0 with - | (_, some tk) := (s, tk.lbp.getOrElse 0) - | _ := (s, 0) -| some (Syntax.ident _ _ _ _ _) := (s, maxPrec) -| some (Syntax.node k _ _) := if k == numLitKind || k == strLitKind then (s, maxPrec) else (s, 0) -| _ := (s, 0) + | (_, some tk) => (s, tk.lbp.getOrElse 0) + | _ => (s, 0) +| some (Syntax.ident _ _ _ _ _) => (s, maxPrec) +| some (Syntax.node k _ _) => if k == numLitKind || k == strLitKind then (s, maxPrec) else (s, 0) +| _ => (s, 0) def indexed {α : Type} (map : TokenMap α) (c : ParserContext) (s : ParserState) : ParserState × List α := let (s, stx) := peekToken c s; let find (n : Name) : ParserState × List α := match map.find n with - | some as := (s, as) - | _ := (s, []); + | some as => (s, as) + | _ => (s, []); match stx with -| some (Syntax.atom _ sym) := find (mkSimpleName sym) -| some (Syntax.ident _ _ _ _ _) := find `ident -| some (Syntax.node k _ _) := find k -| _ := (s, []) +| some (Syntax.atom _ sym) => find (mkSimpleName sym) +| some (Syntax.ident _ _ _ _ _) => find `ident +| some (Syntax.node k _ _) => find k +| _ => (s, []) private def mkResult (s : ParserState) (iniSz : Nat) : ParserState := if s.stackSize == iniSz + 1 then s @@ -987,18 +987,18 @@ IO.mkRef {} private def updateTokens (tables : ParsingTables) (info : ParserInfo) (declName : Name) : IO ParsingTables := match info.updateTokens tables.tokens with -| Except.ok newTokens := pure { tokens := newTokens, .. tables } -| Except.error msg := throw (IO.userError ("invalid builtin parser '" ++ toString declName ++ "', " ++ msg)) +| Except.ok newTokens => pure { tokens := newTokens, .. tables } +| Except.error msg => throw (IO.userError ("invalid builtin parser '" ++ toString declName ++ "', " ++ msg)) def addBuiltinLeadingParser (tablesRef : IO.Ref ParsingTables) (declName : Name) (p : Parser) : IO Unit := do tables ← tablesRef.get; tablesRef.reset; tables ← updateTokens tables p.info declName; match p.info.firstTokens with - | FirstTokens.tokens tks := + | FirstTokens.tokens tks => let tables := tks.foldl (fun (tables : ParsingTables) tk => { leadingTable := tables.leadingTable.insert (mkSimpleName tk.val) p, .. tables }) tables; tablesRef.set tables - | _ := + | _ => throw (IO.userError ("invalid builtin parser '" ++ toString declName ++ "', initial token is not statically known")) def addBuiltinTrailingParser (tablesRef : IO.Ref ParsingTables) (declName : Name) (p : TrailingParser) : IO Unit := @@ -1006,10 +1006,10 @@ do tables ← tablesRef.get; tablesRef.reset; tables ← updateTokens tables p.info declName; match p.info.firstTokens with - | FirstTokens.tokens tks := + | FirstTokens.tokens tks => let tables := tks.foldl (fun (tables : ParsingTables) tk => { trailingTable := tables.trailingTable.insert (mkSimpleName tk.val) p, .. tables }) tables; tablesRef.set tables - | _ := + | _ => let tables := { trailingParsers := p :: tables.trailingParsers, .. tables }; tablesRef.set tables @@ -1019,8 +1019,8 @@ let type := Expr.app (mkConst `IO) (mkConst `Unit); let val := mkCApp addFnName [mkConst refDeclName, toExpr declName, mkConst declName]; let decl := Declaration.defnDecl { name := name, lparams := [], type := type, value := val, hints := ReducibilityHints.opaque, isUnsafe := false }; match env.addAndCompile {} decl with -| none := throw (IO.userError ("failed to emit registration code for builtin parser '" ++ toString declName ++ "'")) -| some env := IO.ofExcept (setInitAttr env name) +| none => throw (IO.userError ("failed to emit registration code for builtin parser '" ++ toString declName ++ "'")) +| some env => IO.ofExcept (setInitAttr env name) def declareLeadingBuiltinParser (env : Environment) (refDeclName : Name) (declName : Name) : IO Environment := declareBuiltinParser env `Lean.Parser.addBuiltinLeadingParser refDeclName declName @@ -1039,14 +1039,14 @@ registerAttribute { unless args.isMissing $ throw (IO.userError ("invalid attribute '" ++ toString attrName ++ "', unexpected argument")); unless persistent $ throw (IO.userError ("invalid attribute '" ++ toString attrName ++ "', must be persistent")); match env.find declName with - | none := throw "unknown declaration" - | some decl := + | none => throw "unknown declaration" + | some decl => match decl.type with - | Expr.const `Lean.Parser.TrailingParser _ := + | Expr.const `Lean.Parser.TrailingParser _ => declareTrailingBuiltinParser env refDeclName declName - | Expr.app (Expr.const `Lean.Parser.Parser _) (Expr.const `Lean.Parser.ParserKind.leading _) := + | Expr.app (Expr.const `Lean.Parser.Parser _) (Expr.const `Lean.Parser.ParserKind.leading _) => declareLeadingBuiltinParser env refDeclName declName - | _ := + | _ => throw (IO.userError ("unexpected parser type at '" ++ toString declName ++ "' (`Parser` or `TrailingParser` expected")) }, applicationTime := AttributeApplicationTime.afterCompilation @@ -1061,8 +1061,8 @@ registerBuiltinParserAttribute `builtinCommandParser `Lean.Parser.builtinCommand @[noinline] unsafe def runBuiltinParserUnsafe (kind : String) (ref : IO.Ref ParsingTables) : ParserFn leading := fun a c s => match unsafeIO (do tables ← ref.get; pure $ prattParser kind tables a c s) with -| some s := s -| none := s.mkError "failed to access builtin reference" +| some s => s +| none => s.mkError "failed to access builtin reference" @[implementedBy runBuiltinParserUnsafe] constant runBuiltinParser (kind : String) (ref : IO.Ref ParsingTables) : ParserFn leading := default _ diff --git a/library/init/lean/parser/trie.lean b/library/init/lean/parser/trie.lean index 79fdcf85c9..121907d971 100644 --- a/library/init/lean/parser/trie.lean +++ b/library/init/lean/parser/trie.lean @@ -29,8 +29,8 @@ instance : Inhabited (Trie α) := private partial def insertEmptyAux (s : String) (val : α) : String.Pos → Trie α | i := match s.atEnd i with - | true := Trie.Node (some val) RBNode.leaf - | false := + | true => Trie.Node (some val) RBNode.leaf + | false => let c := s.get i; let t := insertEmptyAux (s.next i); Trie.Node none (RBNode.singleton c t) @@ -38,13 +38,13 @@ private partial def insertEmptyAux (s : String) (val : α) : String.Pos → Trie private partial def insertAux (s : String) (val : α) : Trie α → String.Pos → Trie α | (Trie.Node v m) i := match s.atEnd i with - | true := Trie.Node (some val) m -- overrides old value - | false := + | true => Trie.Node (some val) m -- overrides old value + | false => let c := s.get i; let i := s.next i; let t := match RBNode.find Char.lt m c with - | none := insertEmptyAux s val i - | some t := insertAux t i; + | none => insertEmptyAux s val i + | some t => insertAux t i; Trie.Node v (RBNode.insert Char.lt m c t) def insert (t : Trie α) (s : String) (val : α) : Trie α := @@ -53,33 +53,33 @@ insertAux s val t 0 private partial def findAux (s : String) : Trie α → String.Pos → Option α | (Trie.Node val m) i := match s.atEnd i with - | true := val - | false := + | true => val + | false => let c := s.get i; let i := s.next i; match RBNode.find Char.lt m c with - | none := none - | some t := findAux t i + | none => none + | some t => findAux t i def find (t : Trie α) (s : String) : Option α := findAux s t 0 private def updtAcc (v : Option α) (i : String.Pos) (acc : String.Pos × Option α) : String.Pos × Option α := match v, acc with -| some v, (j, w) := (i, some v) -- we pattern match on `acc` to enable memory reuse -| none, acc := acc +| some v, (j, w) => (i, some v) -- we pattern match on `acc` to enable memory reuse +| none, acc => acc private partial def matchPrefixAux (s : String) : Trie α → String.Pos → (String.Pos × Option α) → String.Pos × Option α | (Trie.Node v m) i acc := match s.atEnd i with - | true := updtAcc v i acc - | false := + | true => updtAcc v i acc + | false => let acc := updtAcc v i acc; let c := s.get i; let i := s.next i; match RBNode.find Char.lt m c with - | some t := matchPrefixAux t i acc - | none := acc + | some t => matchPrefixAux t i acc + | none => acc def matchPrefix (s : String) (t : Trie α) (i : String.Pos) : String.Pos × Option α := matchPrefixAux s t i (i, none) diff --git a/library/init/lean/projfns.lean b/library/init/lean/projfns.lean index 1e122879ee..9df48487ff 100644 --- a/library/init/lean/projfns.lean +++ b/library/init/lean/projfns.lean @@ -39,16 +39,16 @@ namespace Environment @[export lean.get_projection_info_core] def getProjectionFnInfo (env : Environment) (projName : Name) : Option ProjectionFunctionInfo := match env.getModuleIdxFor projName with -| some modIdx := +| some modIdx => match (projectionFnInfoExt.getModuleEntries env modIdx).binSearch (projName, default _) (fun a b => Name.quickLt a.1 b.1) with - | some e := some e.2 - | none := none -| none := (projectionFnInfoExt.getState env).find projName + | some e => some e.2 + | none => none +| none => (projectionFnInfoExt.getState env).find projName def isProjectionFn (env : Environment) (n : Name) : Bool := match env.getModuleIdxFor n with -| some modIdx := (projectionFnInfoExt.getModuleEntries env modIdx).binSearchContains (n, default _) (fun a b => Name.quickLt a.1 b.1) -| none := (projectionFnInfoExt.getState env).contains n +| some modIdx => (projectionFnInfoExt.getModuleEntries env modIdx).binSearchContains (n, default _) (fun a b => Name.quickLt a.1 b.1) +| none => (projectionFnInfoExt.getState env).contains n end Environment end Lean diff --git a/library/init/lean/reducibilityattrs.lean b/library/init/lean/reducibilityattrs.lean index 54f7880a9e..ddf33032a6 100644 --- a/library/init/lean/reducibilityattrs.lean +++ b/library/init/lean/reducibilityattrs.lean @@ -25,13 +25,13 @@ constant reducibilityAttrs : EnumAttributes ReducibilityStatus := default _ @[export lean.get_reducibility_status_core] def getReducibilityStatus (env : Environment) (n : Name) : ReducibilityStatus := match reducibilityAttrs.getValue env n with -| some s := s -| none := ReducibilityStatus.semireducible +| some s => s +| none => ReducibilityStatus.semireducible @[export lean.set_reducibility_status_core] def setReducibilityStatus (env : Environment) (n : Name) (s : ReducibilityStatus) : Environment := match reducibilityAttrs.setValue env n s with -| Except.ok env := env -| _ := env -- TODO(Leo): we should extend EnumAttributes.setValue in the future and ensure it never fails +| Except.ok env => env +| _ => env -- TODO(Leo): we should extend EnumAttributes.setValue in the future and ensure it never fails end Lean diff --git a/library/init/lean/syntax.lean b/library/init/lean/syntax.lean index e1b4e53c6b..9d9194233c 100644 --- a/library/init/lean/syntax.lean +++ b/library/init/lean/syntax.lean @@ -67,25 +67,25 @@ False.elim (match h with end) @[inline] def withArgs {α : Type} (n : SyntaxNode) (fn : Array Syntax → α) : α := match n with -| ⟨Syntax.node _ args _, _⟩ := fn args -| ⟨Syntax.missing, h⟩ := unreachIsNodeMissing h -| ⟨Syntax.atom _ _, h⟩ := unreachIsNodeAtom h -| ⟨Syntax.ident _ _ _ _ _, h⟩ := unreachIsNodeIdent h +| ⟨Syntax.node _ args _, _⟩ => fn args +| ⟨Syntax.missing, h⟩ => unreachIsNodeMissing h +| ⟨Syntax.atom _ _, h⟩ => unreachIsNodeAtom h +| ⟨Syntax.ident _ _ _ _ _, h⟩ => unreachIsNodeIdent h @[inline] def updateArgs (n : SyntaxNode) (fn : Array Syntax → Array Syntax) : Syntax := match n with -| ⟨Syntax.node kind args scopes, _⟩ := Syntax.node kind (fn args) scopes -| ⟨Syntax.missing, h⟩ := unreachIsNodeMissing h -| ⟨Syntax.atom _ _, h⟩ := unreachIsNodeAtom h -| ⟨Syntax.ident _ _ _ _ _, h⟩ := unreachIsNodeIdent h +| ⟨Syntax.node kind args scopes, _⟩ => Syntax.node kind (fn args) scopes +| ⟨Syntax.missing, h⟩ => unreachIsNodeMissing h +| ⟨Syntax.atom _ _, h⟩ => unreachIsNodeAtom h +| ⟨Syntax.ident _ _ _ _ _, h⟩ => unreachIsNodeIdent h -- TODO(Sebastian): exhaustively argue why (if?) this is correct -- The basic idea is List concatenation with elimination of adjacent identical scopes def MacroScopes.flip : MacroScopes → MacroScopes → MacroScopes | ys [] := ys | ys (x::xs) := match MacroScopes.flip ys xs with - | y::ys := if x == y then ys else x::y::ys - | [] := [x] + | y::ys => if x == y then ys else x::y::ys + | [] => [x] namespace Syntax def isIdent : Syntax → Bool @@ -103,16 +103,16 @@ def flipScopes (scopes : MacroScopes) : Syntax → Syntax @[inline] def toSyntaxNode {α : Type} (s : Syntax) (base : α) (fn : SyntaxNode → α) : α := match s with -| Syntax.node kind args [] := fn ⟨Syntax.node kind args [], IsNode.mk _ _ _⟩ -| Syntax.node kind args scopes := fn ⟨Syntax.node kind (args.map (flipScopes scopes)) [], IsNode.mk _ _ _⟩ -| other := base +| Syntax.node kind args [] => fn ⟨Syntax.node kind args [], IsNode.mk _ _ _⟩ +| Syntax.node kind args scopes => fn ⟨Syntax.node kind (args.map (flipScopes scopes)) [], IsNode.mk _ _ _⟩ +| other => base @[specialize] partial def mreplace {m : Type → Type} [Monad m] (fn : Syntax → m (Option Syntax)) : Syntax → m Syntax | stx@(node kind args scopes) := do o ← fn stx; (match o with - | some stx := pure stx - | none := do args ← args.mmap mreplace; pure (node kind args scopes)) + | some stx => pure stx + | none => do args ← args.mmap mreplace; pure (node kind args scopes)) | stx := do o ← fn stx; pure (o.getOrElse stx) @[inline] def replace {m : Type → Type} [Monad m] (fn : Syntax → m (Option Syntax)) := @mreplace Id _ @@ -195,10 +195,10 @@ protected partial def formatStx : Syntax → Format | (atom info val) := format $ repr val | (ident _ _ val pre scopes) := let scopes := pre.map format ++ scopes.reverse.map format; - let scopes := match scopes with [] := format "" | _ := bracket "{" (joinSep scopes ", ") "}"; + let scopes := match scopes with [] => format "" | _ => bracket "{" (joinSep scopes ", ") "}"; format "`" ++ format val ++ scopes | (node kind args scopes) := - let scopes := match scopes with [] := format "" | _ := bracket "{" (joinSep scopes.reverse ", ") "}"; + let scopes := match scopes with [] => format "" | _ => bracket "{" (joinSep scopes.reverse ", ") "}"; if kind = `Lean.Parser.noKind then sbracket $ scopes ++ joinSep (args.toList.map formatStx) line else @@ -251,8 +251,8 @@ def isStrLit : Syntax → Option String | (Syntax.node k args _) := if k == strLitKind && args.size == 1 then match args.get 0 with - | (Syntax.atom _ val) := some val - | _ := none + | (Syntax.atom _ val) => some val + | _ => none else none | _ := none @@ -320,8 +320,8 @@ def isNatLit : Syntax → Option Nat | (Syntax.node k args _) := if k == numLitKind && args.size == 1 then match args.get 0 with - | (Syntax.atom _ val) := decodeNatLitVal val - | _ := none + | (Syntax.atom _ val) => decodeNatLitVal val + | _ => none else none | _ := none diff --git a/src/frontends/lean/match_expr.cpp b/src/frontends/lean/match_expr.cpp index 14bef718b2..3ce46f18a9 100644 --- a/src/frontends/lean/match_expr.cpp +++ b/src/frontends/lean/match_expr.cpp @@ -63,7 +63,7 @@ expr parse_match(parser & p, unsigned, expr const *, pos_info const & pos) { bool skip_main_fn = true; lhs = p.patexpr_to_pattern(lhs, skip_main_fn, locals); auto assign_pos = p.pos(); - p.check_token_next(get_assign_tk(), "invalid 'match' expression, ':=' expected"); + p.check_token_next(get_darrow_tk(), "invalid 'match' expression, '=>' expected"); { parser::local_scope scope2(p); for (expr const & local : locals) diff --git a/tests/bench/const_fold.lean b/tests/bench/const_fold.lean index c9aa002f96..5fe0fa2fa6 100644 --- a/tests/bench/const_fold.lean +++ b/tests/bench/const_fold.lean @@ -34,18 +34,18 @@ def constFolding : Expr → Expr let e₁ := constFolding e₁ in let e₂ := constFolding e₂ in (match e₁, e₂ with - | Val a, Val b := Val (a+b) - | Val a, Add e (Val b) := Add (Val (a+b)) e - | Val a, Add (Val b) e := Add (Val (a+b)) e - | _, _ := Add e₁ e₂) + | Val a, Val b => Val (a+b) + | Val a, Add e (Val b) => Add (Val (a+b)) e + | Val a, Add (Val b) e => Add (Val (a+b)) e + | _, _ => Add e₁ e₂) | (Mul e₁ e₂) := let e₁ := constFolding e₁ in let e₂ := constFolding e₂ in (match e₁, e₂ with - | Val a, Val b := Val (a*b) - | Val a, Mul e (Val b) := Mul (Val (a*b)) e - | Val a, Mul (Val b) e := Mul (Val (a*b)) e - | _, _ := Mul e₁ e₂) + | Val a, Val b => Val (a*b) + | Val a, Mul e (Val b) => Mul (Val (a*b)) e + | Val a, Mul (Val b) e => Mul (Val (a*b)) e + | _, _ => Mul e₁ e₂) | e := e def size : Expr → Nat diff --git a/tests/bench/rbmap.library.lean b/tests/bench/rbmap.library.lean index 3d534d6bde..f8d4a94cfd 100644 --- a/tests/bench/rbmap.library.lean +++ b/tests/bench/rbmap.library.lean @@ -1,4 +1,4 @@ -@[reducible] def Map : Type := RBMap Nat Bool (λ a b, a < b) +@[reducible] def Map : Type := RBMap Nat Bool (fun a b => a < b) def mkMapAux : Nat → Map → Map | 0 m := m @@ -8,7 +8,7 @@ def mkMap (n : Nat) := mkMapAux n {} def main (xs : List String) : IO UInt32 := -let m := mkMap xs.head.toNat in -let v := m.fold (λ (r : Nat) (k : Nat) (v : Bool), if v then r + 1 else r) 0 in +let m := mkMap xs.head.toNat; +let v := m.fold (fun (r : Nat) (k : Nat) (v : Bool) => if v then r + 1 else r) 0; IO.println (toString v) *> pure 0 diff --git a/tests/bench/rbmap2.lean b/tests/bench/rbmap2.lean index 9a191ee426..b90acd7802 100644 --- a/tests/bench/rbmap2.lean +++ b/tests/bench/rbmap2.lean @@ -68,7 +68,7 @@ def mkMap (n : Nat) := mkMapAux n Leaf def main (xs : List String) : IO UInt32 := -let m := mkMap xs.head.toNat in -let v := fold (λ (k : Nat) (v : Bool) (r : Nat), if v then r + 1 else r) m 0 in +let m := mkMap xs.head.toNat; +let v := fold (fun (k : Nat) (v : Bool) (r : Nat) => if v then r + 1 else r) m 0; IO.println (toString v) *> pure 0 diff --git a/tests/bench/rbmap3.lean b/tests/bench/rbmap3.lean index b13bcfbb01..591d95a324 100644 --- a/tests/bench/rbmap3.lean +++ b/tests/bench/rbmap3.lean @@ -11,9 +11,9 @@ inductive Rbnode (α : Type u) (β : α → Type v) | Node (c : Rbcolor) (lchild : Rbnode) (key : α) (val : β key) (rchild : Rbnode) : Rbnode instance Rbcolor.DecidableEq : DecidableEq Rbcolor := -{decEq := λ a b, Rbcolor.casesOn a - (Rbcolor.casesOn b (isTrue rfl) (isFalse (λ h, Rbcolor.noConfusion h))) - (Rbcolor.casesOn b (isFalse (λ h, Rbcolor.noConfusion h)) (isTrue rfl))} +{decEq := fun a b => Rbcolor.casesOn a + (Rbcolor.casesOn b (isTrue rfl) (isFalse (fun h => Rbcolor.noConfusion h))) + (Rbcolor.casesOn b (isFalse (fun h => Rbcolor.noConfusion h)) (isTrue rfl))} namespace Rbnode variables {α : Type u} {β : α → Type v} {σ : Type w} @@ -24,12 +24,12 @@ def depth (f : Nat → Nat → Nat) : Rbnode α β → Nat | leaf := 0 | (Node _ l _ _ r) := (f (depth l) (depth r)) + 1 -protected def min : Rbnode α β → Option (Sigma (λ k : α, β k)) +protected def min : Rbnode α β → Option (Sigma (fun k => β k)) | leaf := none | (Node _ leaf k v _) := some ⟨k, v⟩ | (Node _ l k v _) := min l -protected def max : Rbnode α β → Option (Sigma (λ k : α, β k)) +protected def max : Rbnode α β → Option (Sigma (fun k => β k)) | leaf := none | (Node _ _ k v leaf) := some ⟨k, v⟩ | (Node _ _ k v r) := max r @@ -63,10 +63,10 @@ def rotateLeft : Π (n : Rbnode α β), n ≠ leaf → Rbnode α β | e _ := e theorem ifNodeNodeNeLeaf {c : Prop} [Decidable c] {l1 l2 : Rbnode α β} {c1 k1 v1 r1 c2 k2 v2 r2} : (if c then Node c1 l1 k1 v1 r1 else Node c2 l2 k2 v2 r2) ≠ leaf := -λ h, if hc : c -then have h1 : (if c then Node c1 l1 k1 v1 r1 else Node c2 l2 k2 v2 r2) = Node c1 l1 k1 v1 r1, from ifPos hc, +fun h => if hc : c +then have h1 : (if c then Node c1 l1 k1 v1 r1 else Node c2 l2 k2 v2 r2) = Node c1 l1 k1 v1 r1 from ifPos hc; Rbnode.noConfusion (Eq.trans h1.symm h) -else have h1 : (if c then Node c1 l1 k1 v1 r1 else Node c2 l2 k2 v2 r2) = Node c2 l2 k2 v2 r2, from ifNeg hc, +else have h1 : (if c then Node c1 l1 k1 v1 r1 else Node c2 l2 k2 v2 r2) = Node c2 l2 k2 v2 r2 from ifNeg hc; Rbnode.noConfusion (Eq.trans h1.symm h) theorem rotateLeftNeLeaf : ∀ (n : Rbnode α β) (h : n ≠ leaf), rotateLeft n h ≠ leaf @@ -119,8 +119,8 @@ variables (lt : α → α → Prop) [DecidableRel lt] def ins (x : α) (vx : β x) : Rbnode α β → Rbnode α β | leaf := Node red leaf x vx leaf | (Node c l k v r) := - if lt x k then fixup (Node c (ins l) k v r) (λ h, Rbnode.noConfusion h) - else if lt k x then fixup (Node c l k v (ins r)) (λ h, Rbnode.noConfusion h) + if lt x k then fixup (Node c (ins l) k v r) (fun h => Rbnode.noConfusion h) + else if lt k x then fixup (Node c l k v (ins r)) (fun h => Rbnode.noConfusion h) else Node c l x vx r def insert (t : Rbnode α β) (k : α) (v : β k) : Rbnode α β := @@ -133,29 +133,29 @@ variable (lt : α → α → Prop) variable [DecidableRel lt] -def findCore : Rbnode α β → Π k : α, Option (Sigma (λ k : α, β k)) +def findCore : Rbnode α β → Π k : α, Option (Sigma (fun k => β k)) | leaf x := none | (Node _ a ky vy b) x := (match cmpUsing lt x ky with - | Ordering.lt := findCore a x - | Ordering.Eq := some ⟨ky, vy⟩ - | Ordering.gt := findCore b x) + | Ordering.lt => findCore a x + | Ordering.Eq => some ⟨ky, vy⟩ + | Ordering.gt => findCore b x) -def find {β : Type v} : Rbnode α (λ _, β) → α → Option β +def find {β : Type v} : Rbnode α (fun _ => β) → α → Option β | leaf x := none | (Node _ a ky vy b) x := (match cmpUsing lt x ky with - | Ordering.lt := find a x - | Ordering.Eq := some vy - | Ordering.gt := find b x) + | Ordering.lt => find a x + | Ordering.Eq => some vy + | Ordering.gt => find b x) def lowerBound : Rbnode α β → α → Option (Sigma β) → Option (Sigma β) | leaf x lb := lb | (Node _ a ky vy b) x lb := (match cmpUsing lt x ky with - | Ordering.lt := lowerBound a x lb - | Ordering.Eq := some ⟨ky, vy⟩ - | Ordering.gt := lowerBound b x (some ⟨ky, vy⟩)) + | Ordering.lt => lowerBound a x lb + | Ordering.Eq => some ⟨ky, vy⟩ + | Ordering.gt => lowerBound b x (some ⟨ky, vy⟩)) end membership @@ -170,7 +170,7 @@ open Rbnode /- TODO(Leo): define dRbmap -/ def Rbmap (α : Type u) (β : Type v) (lt : α → α → Prop) : Type (max u v) := -{t : Rbnode α (λ _, β) // t.WellFormed lt } +{t : Rbnode α (fun _ => β) // t.WellFormed lt } @[inline] def mkRbmap (α : Type u) (β : Type v) (lt : α → α → Prop) : Rbmap α β lt := ⟨leaf, WellFormed.leafWff lt⟩ @@ -192,22 +192,22 @@ t.val.depth f | _ := false @[specialize] def toList : Rbmap α β lt → List (α × β) -| ⟨t, _⟩ := t.revFold (λ k v ps, (k, v)::ps) [] +| ⟨t, _⟩ := t.revFold (fun k v ps => (k, v)::ps) [] @[inline] protected def min : Rbmap α β lt → Option (α × β) | ⟨t, _⟩ := match t.min with - | some ⟨k, v⟩ := some (k, v) - | none := none + | some ⟨k, v⟩ => some (k, v) + | none => none @[inline] protected def max : Rbmap α β lt → Option (α × β) | ⟨t, _⟩ := match t.max with - | some ⟨k, v⟩ := some (k, v) - | none := none + | some ⟨k, v⟩ => some (k, v) + | none => none instance [HasRepr α] [HasRepr β] : HasRepr (Rbmap α β lt) := -⟨λ t, "rbmapOf " ++ repr t.toList⟩ +⟨fun t => "rbmapOf " ++ repr t.toList⟩ variables [DecidableRel lt] @@ -218,7 +218,7 @@ def insert : Rbmap α β lt → α → β → Rbmap α β lt | [] := mkRbmap _ _ _ | (⟨k,v⟩::xs) := (ofList xs).insert k v -def findCore : Rbmap α β lt → α → Option (Sigma (λ k : α, β)) +def findCore : Rbmap α β lt → α → Option (Sigma (fun (k : α) => β)) | ⟨t, _⟩ x := t.findCore lt x def find : Rbmap α β lt → α → Option β @@ -226,14 +226,14 @@ def find : Rbmap α β lt → α → Option β /-- (lowerBound k) retrieves the kv pair of the largest key smaller than or equal to `k`, if it exists. -/ -def lowerBound : Rbmap α β lt → α → Option (Sigma (λ k : α, β)) +def lowerBound : Rbmap α β lt → α → Option (Sigma (fun (k : α) => β)) | ⟨t, _⟩ x := t.lowerBound lt x none @[inline] def contains (t : Rbmap α β lt) (a : α) : Bool := (t.find a).isSome def fromList (l : List (α × β)) (lt : α → α → Prop) [DecidableRel lt] : Rbmap α β lt := -l.foldl (λ r p, r.insert p.1 p.2) (mkRbmap α β lt) +l.foldl (fun r p => r.insert p.1 p.2) (mkRbmap α β lt) @[inline] def all : Rbmap α β lt → (α → β → Bool) → Bool | ⟨t, _⟩ p := t.all p @@ -248,17 +248,17 @@ Rbmap.fromList l lt /- Test -/ -@[reducible] def map : Type := Rbmap Nat Bool (<) +@[reducible] def map : Type := Rbmap Nat Bool HasLess.Less def mkMapAux : Nat → map → map | 0 m := m | (n+1) m := mkMapAux n (m.insert n (n % 10 = 0)) def mkMap (n : Nat) := -mkMapAux n (mkRbmap Nat Bool (<)) +mkMapAux n (mkRbmap Nat Bool HasLess.Less) def main (xs : List String) : IO UInt32 := -let m := mkMap xs.head.toNat in -let v := Rbmap.fold (λ (k : Nat) (v : Bool) (r : Nat), if v then r + 1 else r) m 0 in +let m := mkMap xs.head.toNat; +let v := Rbmap.fold (fun (k : Nat) (v : Bool) (r : Nat) => if v then r + 1 else r) m 0; IO.println (toString v) *> pure 0 diff --git a/tests/bench/rbmap4.lean b/tests/bench/rbmap4.lean index 8d6e77e4ea..7e58649cf3 100644 --- a/tests/bench/rbmap4.lean +++ b/tests/bench/rbmap4.lean @@ -70,7 +70,7 @@ def mkMap (n : Nat) := mkMapAux n Leaf def main (xs : List String) : IO UInt32 := -let m := mkMap xs.head.toNat in -let v := fold (λ (k : Nat) (v : Bool) (r : Nat), if v then r + 1 else r) m 0 in +let m := mkMap xs.head.toNat; +let v := fold (fun (k : Nat) (v : Bool) (r : Nat) => if v then r + 1 else r) m 0; IO.println (toString v) *> pure 0 diff --git a/tests/bench/rbmap_checkpoint2.lean b/tests/bench/rbmap_checkpoint2.lean index 8eeabd808a..dddd0ce493 100644 --- a/tests/bench/rbmap_checkpoint2.lean +++ b/tests/bench/rbmap_checkpoint2.lean @@ -86,6 +86,6 @@ let n := n.toNat; let freq := freq.toNat; let freq := if freq == 0 then 1 else freq; let mList := mkMap n freq; -let v := fold (λ (k : Nat) (v : Bool) (r : Nat), if v then r + 1 else r) mList.head 0; +let v := fold (fun (k : Nat) (v : Bool) (r : Nat) => if v then r + 1 else r) mList.head 0; IO.println (toString (myLen mList 0) ++ " " ++ toString v) *> pure 0 diff --git a/tests/bench/unionfind.lean b/tests/bench/unionfind.lean index 4dfde10555..446aa6ab69 100644 --- a/tests/bench/unionfind.lean +++ b/tests/bench/unionfind.lean @@ -16,8 +16,8 @@ variables {m : Type → Type} [Monad m] {ε : Type} {α β : Type} @[inline] protected def pure (a : α) : ExceptT' m ε α := (pure (Except.ok a) : m (Except ε α)) @[inline] protected def bind (x : ExceptT' m ε α) (f : α → ExceptT' m ε β) : ExceptT' m ε β := (do { v ← x; match v with - | Except.error e := pure (Except.error e) - | Except.ok a := f a } : m (Except ε β)) + | Except.error e => pure (Except.error e) + | Except.ok a => f a } : m (Except ε β)) @[inline] def error (e : ε) : ExceptT' m ε α := (pure (Except.error e) : m (Except ε α)) @[inline] def lift (x : m α) : ExceptT' m ε α := (do {a ← x; pure (Except.ok a) } : m (Except ε α)) instance : Monad (ExceptT' m ε) := @@ -122,5 +122,5 @@ else do def main (xs : List String) : IO UInt32 := let n := xs.head.toNat; match run (test n) with -| (Except.ok v, s) := IO.println ("ok " ++ toString v) *> pure 0 -| (Except.error e, s) := IO.println ("Error : " ++ e) *> pure 1 +| (Except.ok v, s) => IO.println ("ok " ++ toString v) *> pure 0 +| (Except.error e, s) => IO.println ("Error : " ++ e) *> pure 1 diff --git a/tests/bench/unionfind_clean.lean b/tests/bench/unionfind_clean.lean index 9223329b69..70bd8dc512 100644 --- a/tests/bench/unionfind_clean.lean +++ b/tests/bench/unionfind_clean.lean @@ -18,7 +18,7 @@ def findEntryAux : Nat → Node → M nodeData do { let e := s.fget ⟨n, h⟩; if e.find = n then pure e else do e₁ ← findEntryAux i e.find; - modify (λ s, s.set n e₁); + modify (fun s => s.set n e₁); pure e₁ } else throw "invalid Node" @@ -31,14 +31,14 @@ do e ← findEntry n; pure e.find def mk : M Node := do n ← capacity; - modify $ λ s, s.push {find := n, rank := 1}; + modify $ fun s => s.push {find := n, rank := 1}; pure n def union (n₁ n₂ : Node) : M Unit := do r₁ ← findEntry n₁; r₂ ← findEntry n₂; if r₁.find = r₂.find then pure () - else modify $ λ s, + else modify $ fun s => if r₁.rank < r₂.rank then s.set r₁.find { find := r₂.find } else if r₁.rank = r₂.rank then let s₁ := s.set r₁.find { find := r₂.find } in @@ -90,5 +90,5 @@ else do def main (xs : List String) : IO UInt32 := let n := xs.head.toNat in match (test n).run Array.empty with -| EState.Result.ok v s := IO.println ("ok " ++ toString v) *> pure 0 -| EState.Result.error e s := IO.println ("Error : " ++ e) *> pure 1 +| EState.Result.ok v s => IO.println ("ok " ++ toString v) *> pure 0 +| EState.Result.error e s => IO.println ("Error : " ++ e) *> pure 1 diff --git a/tests/lean/run/coroutine.lean b/tests/lean/run/coroutine.lean index 55cd1c4a02..fabd2fca3e 100644 --- a/tests/lean/run/coroutine.lean +++ b/tests/lean/run/coroutine.lean @@ -94,8 +94,8 @@ open wellFoundedTactics @[inlineIfReduce] protected unsafe def bind : coroutine α δ β → (β → coroutine α δ γ) → coroutine α δ γ | (mk k) f := mk $ fun a => match k a, rfl : ∀ (n : _), n = k a → _ with - | done b, _ := coroutine.resume (f b) a - | yielded d c, h := + | done b, _ => coroutine.resume (f b) a + | yielded d c, h => -- have directSubcoroutine c (mk k), { apply directSubcoroutine.mk k a d, rw h }, yielded d (bind c f) -- usingWellFounded { decTac := unfoldWfRel >> processLex (tactic.assumption) } @@ -103,11 +103,11 @@ open wellFoundedTactics unsafe def pipe : coroutine α δ β → coroutine δ γ β → coroutine α γ β | (mk k₁) (mk k₂) := mk $ fun a => match k₁ a, rfl : ∀ (n : _), n = k₁ a → _ with - | done b, h := done b - | yielded d k₁', h := + | done b, h => done b + | yielded d k₁', h => match k₂ d with - | done b := done b - | yielded r k₂' := + | done b => done b + | yielded r k₂' => -- have directSubcoroutine k₁' (mk k₁), { apply directSubcoroutine.mk k₁ a d, rw h }, yielded r (pipe k₁' k₂') -- usingWellFounded { decTac := unfoldWfRel >> processLex (tactic.assumption) } @@ -115,8 +115,8 @@ unsafe def pipe : coroutine α δ β → coroutine δ γ β → coroutine α γ private unsafe def finishAux (f : δ → α) : coroutine α δ β → α → List δ → List δ × β | (mk k) a ds := match k a with - | done b := (ds.reverse, b) - | yielded d k' := finishAux k' (f d) (d::ds) + | done b => (ds.reverse, b) + | yielded d k' => finishAux k' (f d) (d::ds) /-- Run a coroutine to completion, feeding back yielded items after transforming them with `f`. -/ unsafe def finish (f : δ → α) : coroutine α δ β → α → List δ × β := diff --git a/tests/lean/run/rc_tests.lean b/tests/lean/run/rc_tests.lean index 54cf107dcc..d841bf9d1e 100644 --- a/tests/lean/run/rc_tests.lean +++ b/tests/lean/run/rc_tests.lean @@ -9,8 +9,8 @@ namespace x1 def f (x : Bool) (y z : Nat) : Nat := match x with -| true := y -| false := z + y + y +| true => y +| false => z + y + y end x1 diff --git a/tests/lean/trust0/basic.lean b/tests/lean/trust0/basic.lean index 2a92343c2d..fb4d812644 100644 --- a/tests/lean/trust0/basic.lean +++ b/tests/lean/trust0/basic.lean @@ -58,8 +58,8 @@ def hasDecEq : Π a b : Nat, Decidable (a = b) | zero (succ y) := isFalse (fun h => Nat.noConfusion h) | (succ x) (succ y) := match hasDecEq x y with - | isTrue xeqy := isTrue (xeqy ▸ Eq.refl (succ x)) - | isFalse xney := isFalse (fun h => Nat.noConfusion h (fun xeqy => absurd xeqy xney)) + | isTrue xeqy => isTrue (xeqy ▸ Eq.refl (succ x)) + | isFalse xney => isFalse (fun h => Nat.noConfusion h (fun xeqy => absurd xeqy xney)) instance : DecidableEq ℕ := {decEq := hasDecEq} @@ -109,8 +109,8 @@ instance decidableLe : ∀ a b : ℕ, Decidable (a ≤ b) | (a+1) 0 := isFalse (notSuccLeZero a) | (a+1) (b+1) := match decidableLe a b with - | isTrue h := isTrue (succLeSucc h) - | isFalse h := isFalse (fun a => h (leOfSuccLeSucc a)) + | isTrue h => isTrue (succLeSucc h) + | isFalse h => isFalse (fun a => h (leOfSuccLeSucc a)) instance decidableLt : ∀ a b : ℕ, Decidable (a < b) := fun a b => Nat.decidableLe (succ a) b