From ab5c0301d657ead4d950f461d4bcdd36606c5e72 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 12 May 2020 14:58:11 -0700 Subject: [PATCH] chore: update stage0 --- stage0/src/Init/Coe.lean | 2 +- stage0/src/Init/Control/Alternative.lean | 3 +- stage0/src/Init/Control/Applicative.lean | 2 +- stage0/src/Init/Control/EState.lean | 4 +- stage0/src/Init/Control/Except.lean | 12 +++--- stage0/src/Init/Control/Lift.lean | 10 ++--- stage0/src/Init/Control/Reader.lean | 10 ++--- stage0/src/Init/Control/State.lean | 12 +++--- stage0/src/Init/Core.lean | 38 +++++++++---------- stage0/src/Init/Data/AssocList.lean | 2 +- stage0/src/Init/Data/BinomialHeap/Basic.lean | 10 ++--- .../Init/Data/PersistentHashMap/Basic.lean | 6 +-- stage0/src/Init/Data/RBMap/Basic.lean | 4 +- .../src/Init/Lean/Data/Json/FromToJson.lean | 2 +- stage0/src/Init/Lean/Data/Json/Parser.lean | 8 ++-- stage0/src/Init/Lean/Data/KVMap.lean | 2 +- stage0/src/Init/Lean/Data/LOption.lean | 6 +-- stage0/src/Init/Lean/Elab/Log.lean | 10 ++--- stage0/src/Init/Lean/Elab/StructInst.lean | 8 ++-- stage0/src/Init/Lean/Elab/Util.lean | 12 +++--- stage0/src/Init/Lean/Util/MonadCache.lean | 8 ++-- stage0/src/Init/Lean/Util/Trace.lean | 22 +++++------ stage0/src/Init/LeanInit.lean | 10 ++--- stage0/src/Init/ShareCommon.lean | 2 +- stage0/src/Init/Util.lean | 2 +- stage0/src/Init/WF.lean | 4 +- stage0/stdlib/Init/Control/Alternative.c | 21 ---------- 27 files changed, 105 insertions(+), 127 deletions(-) diff --git a/stage0/src/Init/Coe.lean b/stage0/src/Init/Coe.lean index a97ca477ec..4d65730d9e 100644 --- a/stage0/src/Init/Coe.lean +++ b/stage0/src/Init/Coe.lean @@ -119,4 +119,4 @@ instance subtypeCoe {α : Sort u} {p : α → Prop} : CoeHead { x // p x } α := Reason: `HasOfNat` is for implementing polymorphic numeric literals, and we may want to have numberic literals for a type α and **no** coercion from `Nat` to `α`. -/ instance hasOfNatOfCoe {α : Type u} {β : Type v} [HasOfNat α] [Coe α β] : HasOfNat β := -{ ofNat := fun (n : Nat) => coe (HasOfNat.ofNat α n) } +{ ofNat := fun (n : Nat) => coe (HasOfNat.ofNat n : α) } diff --git a/stage0/src/Init/Control/Alternative.lean b/stage0/src/Init/Control/Alternative.lean index 6b5754dfb8..0f6081a680 100644 --- a/stage0/src/Init/Control/Alternative.lean +++ b/stage0/src/Init/Control/Alternative.lean @@ -18,8 +18,7 @@ instance alternativeHasOrelse (f : Type u → Type v) (α : Type u) [Alternative section variables {f : Type u → Type v} [Alternative f] {α : Type u} -@[inline] def failure : f α := -Alternative.failure f +export Alternative (failure) @[inline] def guard {f : Type → Type v} [Alternative f] (p : Prop) [Decidable p] : f Unit := if p then pure () else failure diff --git a/stage0/src/Init/Control/Applicative.lean b/stage0/src/Init/Control/Applicative.lean index 8e80b9c5c9..28dd82a56d 100644 --- a/stage0/src/Init/Control/Applicative.lean +++ b/stage0/src/Init/Control/Applicative.lean @@ -9,7 +9,7 @@ open Function universes u v class HasPure (f : Type u → Type v) := -(pure {} {α : Type u} : α → f α) +(pure {α : Type u} : α → f α) export HasPure (pure) diff --git a/stage0/src/Init/Control/EState.lean b/stage0/src/Init/Control/EState.lean index bab6287d07..63a54be6ef 100644 --- a/stage0/src/Init/Control/EState.lean +++ b/stage0/src/Init/Control/EState.lean @@ -11,8 +11,8 @@ universes u v namespace EStateM inductive Result (ε σ α : Type u) -| ok {} : α → σ → Result -| error {} : ε → σ → Result +| ok : α → σ → Result +| error : ε → σ → Result variables {ε σ α : Type u} diff --git a/stage0/src/Init/Control/Except.lean b/stage0/src/Init/Control/Except.lean index 8cd89a207e..117492c987 100644 --- a/stage0/src/Init/Control/Except.lean +++ b/stage0/src/Init/Control/Except.lean @@ -12,8 +12,8 @@ import Init.Data.ToString universes u v w inductive Except (ε : Type u) (α : Type v) -| error {} : ε → Except -| ok {} : α → Except +| error : ε → Except +| ok : α → Except attribute [unbox] Except @@ -127,8 +127,8 @@ end ExceptT /-- An implementation of [MonadError](https://hackage.haskell.org/package/mtl-2.2.2/docs/Control-Monad-Except.html#t:MonadError) -/ class MonadExcept (ε : outParam (Type u)) (m : Type v → Type w) := -(throw {} {α : Type v} : ε → m α) -(catch {} {α : Type v} : m α → (ε → m α) → m α) +(throw {α : Type v} : ε → m α) +(catch {α : Type v} : m α → (ε → m α) → m α) namespace MonadExcept variables {ε : Type u} {m : Type v → Type w} @@ -160,11 +160,11 @@ instance (ε) : MonadExcept ε (Except ε) := Note: This class can be seen as a simplification of the more "principled" definition ``` class MonadExceptFunctor (ε ε' : outParam (Type u)) (n n' : Type u → Type u) := - (map {} {α : Type u} : (∀ {m : Type u → Type u} [Monad m], ExceptT ε m α → ExceptT ε' m α) → n α → n' α) + (map {α : Type u} : (∀ {m : Type u → Type u} [Monad m], ExceptT ε m α → ExceptT ε' m α) → n α → n' α) ``` -/ class MonadExceptAdapter (ε ε' : outParam (Type u)) (m m' : Type u → Type v) := -(adaptExcept {} {α : Type u} : (ε → ε') → m α → m' α) +(adaptExcept {α : Type u} : (ε → ε') → m α → m' α) export MonadExceptAdapter (adaptExcept) section diff --git a/stage0/src/Init/Control/Lift.lean b/stage0/src/Init/Control/Lift.lean index 1b7549edbb..64c904f3f3 100644 --- a/stage0/src/Init/Control/Lift.lean +++ b/stage0/src/Init/Control/Lift.lean @@ -19,13 +19,13 @@ universes u v w but `n` does not have to be a monad transformer. Alternatively, an implementation of [MonadLayer](https://hackage.haskell.org/package/layers-0.1/docs/Control-Monad-Layer.html#t:MonadLayer) without `layerInvmap` (so far). -/ class HasMonadLift (m : Type u → Type v) (n : Type u → Type w) := -(monadLift {} : ∀ {α}, m α → n α) +(monadLift : ∀ {α}, m α → n α) /-- The reflexive-transitive closure of `HasMonadLift`. `monadLift` is used to transitively lift monadic computations such as `StateT.get` or `StateT.put s`. Corresponds to [MonadLift](https://hackage.haskell.org/package/layers-0.1/docs/Control-Monad-Layer.html#t:MonadLift). -/ class HasMonadLiftT (m : Type u → Type v) (n : Type u → Type w) := -(monadLift {} : ∀ {α}, m α → n α) +(monadLift : ∀ {α}, m α → n α) export HasMonadLiftT (monadLift) @@ -53,13 +53,13 @@ theorem monadLiftRefl {m : Type u → Type v} {α} : (monadLift : m α → m α) Remark: other libraries equate `m` and `m'`, and `n` and `n'`. We need to distinguish them to be able to implement gadgets such as `MonadStateAdapter` and `MonadReaderAdapter`. -/ class MonadFunctor (m m' : Type u → Type v) (n n' : Type u → Type w) := -(monadMap {} {α : Type u} : (∀ {β}, m β → m' β) → n α → n' α) +(monadMap {α : Type u} : (∀ {β}, m β → m' β) → n α → n' α) /-- The reflexive-transitive closure of `MonadFunctor`. `monadMap` is used to transitively lift Monad morphisms such as `StateT.zoom`. A generalization of [MonadLiftFunctor](http://duairc.netsoc.ie/layers-docs/Control-Monad-Layer.html#t:MonadLiftFunctor), which can only lift endomorphisms (i.e. m = m', n = n'). -/ class MonadFunctorT (m m' : Type u → Type v) (n n' : Type u → Type w) := -(monadMap {} {α : Type u} : (∀ {β}, m β → m' β) → n α → n' α) +(monadMap {α : Type u} : (∀ {β}, m β → m' β) → n α → n' α) export MonadFunctorT (monadMap) @@ -82,6 +82,6 @@ theorem monadMapRefl {m m' : Type u → Type v} (f : ∀ {β}, m β → m' β) { ``` -/ class MonadRun (out : outParam $ Type u → Type v) (m : Type u → Type v) := -(run {} {α : Type u} : m α → out α) +(run {α : Type u} : m α → out α) export MonadRun (run) diff --git a/stage0/src/Init/Control/Reader.lean b/stage0/src/Init/Control/Reader.lean index 68f2fbac68..2ad3ea08fd 100644 --- a/stage0/src/Init/Control/Reader.lean +++ b/stage0/src/Init/Control/Reader.lean @@ -77,11 +77,11 @@ end ReaderT Note: This class can be seen as a simplification of the more "principled" definition ``` class MonadReader (ρ : outParam (Type u)) (n : Type u → Type u) := - (lift {} {α : Type u} : (∀ {m : Type u → Type u} [Monad m], ReaderT ρ m α) → n α) + (lift {α : Type u} : (∀ {m : Type u → Type u} [Monad m], ReaderT ρ m α) → n α) ``` -/ class MonadReader (ρ : outParam (Type u)) (m : Type u → Type v) := -(read {} : m ρ) +(read : m ρ) export MonadReader (read) @@ -100,11 +100,11 @@ instance {ρ : Type u} {m : Type u → Type v} [Monad m] : MonadReader ρ (Reade Note: This class can be seen as a simplification of the more "principled" definition ``` class MonadReaderFunctor (ρ ρ' : outParam (Type u)) (n n' : Type u → Type u) := - (map {} {α : Type u} : (∀ {m : Type u → Type u} [Monad m], ReaderT ρ m α → ReaderT ρ' m α) → n α → n' α) + (map {α : Type u} : (∀ {m : Type u → Type u} [Monad m], ReaderT ρ m α → ReaderT ρ' m α) → n α → n' α) ``` -/ class MonadReaderAdapter (ρ ρ' : outParam (Type u)) (m m' : Type u → Type v) := -(adaptReader {} {α : Type u} : (ρ' → ρ) → m α → m' α) +(adaptReader {α : Type u} : (ρ' → ρ) → m α → m' α) export MonadReaderAdapter (adaptReader) section @@ -121,7 +121,7 @@ instance (ρ : Type u) (m out) [MonadRun out m] : MonadRun (fun α => ρ → out ⟨fun α x => run ∘ x⟩ class MonadReaderRunner (ρ : Type u) (m m' : Type u → Type u) := -(runReader {} {α : Type u} : m α → ρ → m' α) +(runReader {α : Type u} : m α → ρ → m' α) export MonadReaderRunner (runReader) section diff --git a/stage0/src/Init/Control/State.lean b/stage0/src/Init/Control/State.lean index 0e60bb45d0..47bd5c8c64 100644 --- a/stage0/src/Init/Control/State.lean +++ b/stage0/src/Init/Control/State.lean @@ -91,14 +91,14 @@ end StateT automatically from `monadLift`. -/ class MonadState (σ : outParam (Type u)) (m : Type u → Type v) := /- Obtain the top-most State of a Monad stack. -/ -(get {} : m σ) +(get : m σ) /- Set the top-most State of a Monad stack. -/ -(set {} : σ → m PUnit) +(set : σ → m PUnit) /- Map the top-most State of a Monad stack. Note: `modifyGet f` may be preferable to `do s <- get; let (a, s) := f s; put s; pure a` because the latter does not use the State linearly (without sufficient inlining). -/ -(modifyGet {} {α : Type u} : (σ → α × σ) → m α) +(modifyGet {α : Type u} : (σ → α × σ) → m α) export MonadState (get set modifyGet) @@ -149,7 +149,7 @@ end Note: This class can be seen as a simplification of the more "principled" definition ``` class MonadStateFunctor (σ σ' : outParam (Type u)) (n n' : Type u → Type u) := - (map {} {α : Type u} : (∀ {m : Type u → Type u} [Monad m], StateT σ m α → StateT σ' m α) → n α → n' α) + (map {α : Type u} : (∀ {m : Type u → Type u} [Monad m], StateT σ m α → StateT σ' m α) → n α → n' α) ``` which better describes the intent of "we can map a `StateT` anywhere in the Monad stack". If we look at the unfolded Type of the first argument `∀ m [Monad m], (σ → m (α × σ)) → σ' → m (α × σ')`, we see that it has the lens Type `∀ f [Functor f], (α → f α) → β → f β` with `f` specialized to `fun σ => m (α × σ)` (exercise: show that this is a lawful Functor). We can build all lenses we are insterested in from the functions `split` and `join` as @@ -159,7 +159,7 @@ end ``` -/ class MonadStateAdapter (σ σ' : outParam (Type u)) (m m' : Type u → Type v) := -(adaptState {} {σ'' α : Type u} (split : σ' → σ × σ'') (join : σ → σ'' → σ') : m α → m' α) +(adaptState {σ'' α : Type u} (split : σ' → σ × σ'') (join : σ → σ'' → σ') : m α → m' α) export MonadStateAdapter (adaptState) section @@ -180,7 +180,7 @@ instance (σ : Type u) (m out : Type u → Type v) [MonadRun out m] [Functor m] ⟨fun α x => run ∘ StateT.run' x⟩ class MonadStateRunner (σ : Type u) (m m' : Type u → Type u) := -(runState {} {α : Type u} : m α → σ → m' α) +(runState {α : Type u} : m α → σ → m' α) export MonadStateRunner (runState) section diff --git a/stage0/src/Init/Core.lean b/stage0/src/Init/Core.lean index b29f991284..3ca4ab3393 100644 --- a/stage0/src/Init/Core.lean +++ b/stage0/src/Init/Core.lean @@ -180,7 +180,7 @@ def Not (a : Prop) : Prop := a → False prefix `¬` := Not inductive Eq {α : Sort u} (a : α) : α → Prop -| refl : Eq a +| refl {} : Eq a @[elabAsEliminator, inline, reducible] def Eq.ndrec.{u1, u2} {α : Sort u2} {a : α} {C : α → Sort u1} (m : C a) {b : α} (h : Eq a b) : C b := @@ -206,7 +206,7 @@ constant Quot.ind {α : Sort u} {r : α → α → Prop} {β : Quot r → Prop} init_quot inductive HEq {α : Sort u} (a : α) : ∀ {β : Sort u}, β → Prop -| refl : HEq a +| refl {} : HEq a structure Prod (α : Type u) (β : Type v) := (fst : α) (snd : β) @@ -254,16 +254,16 @@ show (Eq.ndrecOn (Eq.refl α) a : α) = a' from this α a' h (Eq.refl α) inductive Sum (α : Type u) (β : Type v) -| inl {} (val : α) : Sum -| inr {} (val : β) : Sum +| inl (val : α) : Sum +| inr (val : β) : Sum inductive PSum (α : Sort u) (β : Sort v) -| inl {} (val : α) : PSum -| inr {} (val : β) : PSum +| inl (val : α) : PSum +| inr (val : β) : PSum inductive Or (a b : Prop) : Prop -| inl {} (h : a) : Or -| inr {} (h : b) : Or +| inl (h : a) : Or +| inr (h : b) : Or def Or.introLeft {a : Prop} (b : Prop) (ha : a) : Or a b := Or.inl ha @@ -307,7 +307,7 @@ def decEq {α : Sort u} [s : DecidableEq α] (a b : α) : Decidable (a = b) := s a b inductive Option (α : Type u) -| none {} : Option +| none : Option | some (val : α) : Option attribute [unbox] Option @@ -316,7 +316,7 @@ export Option (none some) export Bool (false true) inductive List (T : Type u) -| nil {} : List +| nil : List | cons (hd : T) (tl : List) : List infixr `::` := List.cons @@ -332,8 +332,8 @@ axiom sorryAx (α : Sort u) (synthetic := true) : α /- Declare builtin and reserved notation -/ -class HasZero (α : Type u) := (zero : α) -class HasOne (α : Type u) := (one : α) +class HasZero (α : Type u) := mk {} :: (zero : α) +class HasOne (α : Type u) := mk {} :: (one : α) class HasAdd (α : Type u) := (add : α → α → α) class HasMul (α : Type u) := (mul : α → α → α) class HasNeg (α : Type u) := (neg : α → α) @@ -365,7 +365,7 @@ infix `≤` := HasLessEq.LessEq infix `<` := HasLess.Less infix `==` := HasBeq.beq infix `++` := HasAppend.append -notation `∅` := HasEmptyc.emptyc _ +notation `∅` := HasEmptyc.emptyc infix `≈` := HasEquiv.Equiv infixr `^` := HasPow.pow infixr `/\` := And @@ -1080,7 +1080,7 @@ structure PointedType := /- Inhabited -/ class Inhabited (α : Sort u) := -(default : α) +mk {} :: (default : α) constant arbitrary (α : Sort u) [Inhabited α] : α := Inhabited.default α @@ -1353,7 +1353,7 @@ fun a b => isTrue (punitEq a b) /- Setoid -/ class Setoid (α : Sort u) := -(r : α → α → Prop) (iseqv : Equivalence r) +(r : α → α → Prop) (iseqv {} : Equivalence r) instance setoidHasEquiv {α : Sort u} [Setoid α] : HasEquiv α := ⟨Setoid.r⟩ @@ -1600,10 +1600,10 @@ variable {α : Type u} variable (r : α → α → Prop) inductive EqvGen : α → α → Prop -| rel {} : ∀ x y, r x y → EqvGen x y -| refl {} : ∀ x, EqvGen x x -| symm {} : ∀ x y, EqvGen x y → EqvGen y x -| trans {} : ∀ x y z, EqvGen x y → EqvGen y z → EqvGen x z +| rel : ∀ x y, r x y → EqvGen x y +| refl : ∀ x, EqvGen x x +| symm : ∀ x y, EqvGen x y → EqvGen y x +| trans : ∀ x y z, EqvGen x y → EqvGen y z → EqvGen x z theorem EqvGen.isEquivalence : Equivalence (@EqvGen α r) := mkEquivalence _ EqvGen.refl EqvGen.symm EqvGen.trans diff --git a/stage0/src/Init/Data/AssocList.lean b/stage0/src/Init/Data/AssocList.lean index 445da38140..b66edb3ad4 100644 --- a/stage0/src/Init/Data/AssocList.lean +++ b/stage0/src/Init/Data/AssocList.lean @@ -9,7 +9,7 @@ universes u v w /- List-like type to avoid extra level of indirection -/ inductive AssocList (α : Type u) (β : Type v) -| nil {} : AssocList +| nil : AssocList | cons (key : α) (value : β) (tail : AssocList) : AssocList namespace AssocList diff --git a/stage0/src/Init/Data/BinomialHeap/Basic.lean b/stage0/src/Init/Data/BinomialHeap/Basic.lean index 48f9d9cd08..cb24558ce3 100644 --- a/stage0/src/Init/Data/BinomialHeap/Basic.lean +++ b/stage0/src/Init/Data/BinomialHeap/Basic.lean @@ -13,7 +13,7 @@ structure HeapNodeAux (α : Type u) (h : Type u) := (val : α) (rank : Nat) (children : List h) inductive Heap (α : Type u) : Type u -| empty {} : Heap +| empty : Heap | heap (ns : List (HeapNodeAux α Heap)) : Heap abbrev HeapNode (α) := HeapNodeAux α (Heap α) @@ -94,8 +94,8 @@ partial def toList (lt : α → α → Bool) : Heap α → List α | some a => a :: toList (tail lt h) inductive WellFormed (lt : α → α → Bool) : Heap α → Prop -| emptyWff : WellFormed Heap.empty -| singletonWff (a : α) : WellFormed (singleton a) +| emptyWff : WellFormed Heap.empty +| singletonWff (a : α) : WellFormed (singleton a) | mergeWff (h₁ h₂ : Heap α) : WellFormed h₁ → WellFormed h₂ → WellFormed (merge lt h₁ h₂) | tailWff (h : Heap α) : WellFormed h → WellFormed (tail lt h) @@ -106,7 +106,7 @@ open BinomialHeapImp def BinomialHeap (α : Type u) (lt : α → α → Bool) := { h : Heap α // WellFormed lt h } @[inline] def mkBinomialHeap (α : Type u) (lt : α → α → Bool) : BinomialHeap α lt := -⟨Heap.empty, WellFormed.emptyWff lt⟩ +⟨Heap.empty, WellFormed.emptyWff⟩ namespace BinomialHeap variables {α : Type u} {lt : α → α → Bool} @@ -119,7 +119,7 @@ mkBinomialHeap α lt /- O(1) -/ @[inline] def singleton (a : α) : BinomialHeap α lt := -⟨BinomialHeapImp.singleton a, WellFormed.singletonWff lt a⟩ +⟨BinomialHeapImp.singleton a, WellFormed.singletonWff a⟩ /- O(log n) -/ @[inline] def merge : BinomialHeap α lt → BinomialHeap α lt → BinomialHeap α lt diff --git a/stage0/src/Init/Data/PersistentHashMap/Basic.lean b/stage0/src/Init/Data/PersistentHashMap/Basic.lean index 0e638f8ac7..d14fb72312 100644 --- a/stage0/src/Init/Data/PersistentHashMap/Basic.lean +++ b/stage0/src/Init/Data/PersistentHashMap/Basic.lean @@ -11,9 +11,9 @@ universes u v w w' namespace PersistentHashMap inductive Entry (α : Type u) (β : Type v) (σ : Type w) -| entry {} (key : α) (val : β) : Entry -| ref {} (node : σ) : Entry -| null {} : Entry +| entry (key : α) (val : β) : Entry +| ref (node : σ) : Entry +| null : Entry instance Entry.inhabited {α β σ} : Inhabited (Entry α β σ) := ⟨Entry.null⟩ diff --git a/stage0/src/Init/Data/RBMap/Basic.lean b/stage0/src/Init/Data/RBMap/Basic.lean index ac3d99dda8..52af33ea02 100644 --- a/stage0/src/Init/Data/RBMap/Basic.lean +++ b/stage0/src/Init/Data/RBMap/Basic.lean @@ -13,7 +13,7 @@ inductive Rbcolor | red | black inductive RBNode (α : Type u) (β : α → Type v) -| leaf {} : RBNode +| leaf : RBNode | node (color : Rbcolor) (lchild : RBNode) (key : α) (val : β key) (rchild : RBNode) : RBNode namespace RBNode @@ -213,7 +213,7 @@ def RBMap (α : Type u) (β : Type v) (lt : α → α → Bool) : Type (max u v) {t : RBNode α (fun _ => β) // t.WellFormed lt } @[inline] def mkRBMap (α : Type u) (β : Type v) (lt : α → α → Bool) : RBMap α β lt := -⟨leaf, WellFormed.leafWff lt⟩ +⟨leaf, WellFormed.leafWff⟩ @[inline] def RBMap.empty {α : Type u} {β : Type v} {lt : α → α → Bool} : RBMap α β lt := mkRBMap _ _ _ diff --git a/stage0/src/Init/Lean/Data/Json/FromToJson.lean b/stage0/src/Init/Lean/Data/Json/FromToJson.lean index bc61c0f582..f17f0156fe 100644 --- a/stage0/src/Init/Lean/Data/Json/FromToJson.lean +++ b/stage0/src/Init/Lean/Data/Json/FromToJson.lean @@ -13,7 +13,7 @@ namespace Lean universes u class HasFromJson (α : Type u) := -(fromJson? {} : Json → Option α) +(fromJson? : Json → Option α) export HasFromJson (fromJson?) class HasToJson (α : Type u) := diff --git a/stage0/src/Init/Lean/Data/Json/Parser.lean b/stage0/src/Init/Lean/Data/Json/Parser.lean index d4967cbd08..5d6545480a 100644 --- a/stage0/src/Init/Lean/Data/Json/Parser.lean +++ b/stage0/src/Init/Lean/Data/Json/Parser.lean @@ -11,8 +11,8 @@ import Init.Control.Except namespace Lean inductive Quickparse.Result (α : Type) -| success {} (pos : String.Iterator) (res : α) : Quickparse.Result -| error {} (pos : String.Iterator) (err : String) : Quickparse.Result +| success (pos : String.Iterator) (res : α) : Quickparse.Result +| error (pos : String.Iterator) (err : String) : Quickparse.Result def Quickparse (α : Type) : Type := String.Iterator → Quickparse.Result α @@ -38,7 +38,7 @@ protected def pure {α : Type} (a : α) : Quickparse α | it => success it a @[inline] -protected def bind {α β : Type} (f : Quickparse α) (g : α → Quickparse β) : Quickparse β | it => +protected def bind {α β : Type} (f : Quickparse α) (g : α → Quickparse β) : Quickparse β | it => match f it with | success rem a => g a rem | error pos msg => error pos msg @@ -137,7 +137,7 @@ else do ec ← if c = '\\' then escapedChar - -- as to whether c.val > 0xffff should be split up and encoded with multiple \u, + -- as to whether c.val > 0xffff should be split up and encoded with multiple \u, -- the JSON standard is not definite: both directly printing the character -- and encoding it with multiple \u is allowed. we choose the former. else if 0x0020 ≤ c.val ∧ c.val ≤ 0x10ffff then diff --git a/stage0/src/Init/Lean/Data/KVMap.lean b/stage0/src/Init/Lean/Data/KVMap.lean index 283d0be6e4..17cdbcfb8e 100644 --- a/stage0/src/Init/Lean/Data/KVMap.lean +++ b/stage0/src/Init/Lean/Data/KVMap.lean @@ -155,7 +155,7 @@ class isKVMapVal (α : Type) := export isKVMapVal (set) -@[inline] def get {α : Type} [isKVMapVal α] (m : KVMap) (k : Name) (defVal := isKVMapVal.defVal α) : α := +@[inline] def get {α : Type} [isKVMapVal α] (m : KVMap) (k : Name) (defVal := isKVMapVal.defVal) : α := isKVMapVal.get m k defVal instance boolVal : isKVMapVal Bool := diff --git a/stage0/src/Init/Lean/Data/LOption.lean b/stage0/src/Init/Lean/Data/LOption.lean index ae29a55699..10928e92f6 100644 --- a/stage0/src/Init/Lean/Data/LOption.lean +++ b/stage0/src/Init/Lean/Data/LOption.lean @@ -10,9 +10,9 @@ universes u namespace Lean inductive LOption (α : Type u) -| none {} : LOption -| some : α → LOption -| undef {} : LOption +| none : LOption +| some : α → LOption +| undef : LOption namespace LOption variables {α : Type u} diff --git a/stage0/src/Init/Lean/Elab/Log.lean b/stage0/src/Init/Lean/Elab/Log.lean index f6cbe1159d..8811ff36e6 100644 --- a/stage0/src/Init/Lean/Elab/Log.lean +++ b/stage0/src/Init/Lean/Elab/Log.lean @@ -11,15 +11,15 @@ namespace Lean namespace Elab class MonadPosInfo (m : Type → Type) := -(getFileMap {} : m FileMap) -(getFileName {} : m String) -(getCmdPos {} : m String.Pos) -(addContext {} : MessageData → m MessageData) +(getFileMap : m FileMap) +(getFileName : m String) +(getCmdPos : m String.Pos) +(addContext : MessageData → m MessageData) export MonadPosInfo (getFileMap getFileName getCmdPos) class MonadLog (m : Type → Type) extends MonadPosInfo m := -(logMessage {} : Message → m Unit) +(logMessage : Message → m Unit) export MonadLog (logMessage) diff --git a/stage0/src/Init/Lean/Elab/StructInst.lean b/stage0/src/Init/Lean/Elab/StructInst.lean index 2aed9e89a7..8541dc7c28 100644 --- a/stage0/src/Init/Lean/Elab/StructInst.lean +++ b/stage0/src/Init/Lean/Elab/StructInst.lean @@ -220,12 +220,12 @@ instance FieldLHS.hasFormat : HasFormat FieldLHS := | FieldLHS.modifyOp _ i => "[" ++ i.prettyPrint ++ "]"⟩ inductive FieldVal (σ : Type) -| term {} (stx : Syntax) : FieldVal -| nested (s : σ) : FieldVal -| default {} : FieldVal -- mark that field must be synthesized using default value +| term (stx : Syntax) : FieldVal +| nested (s : σ) : FieldVal +| default : FieldVal -- mark that field must be synthesized using default value structure Field (σ : Type) := -mk {} :: (ref : Syntax) (lhs : List FieldLHS) (val : FieldVal σ) (expr? : Option Expr := none) +(ref : Syntax) (lhs : List FieldLHS) (val : FieldVal σ) (expr? : Option Expr := none) instance Field.inhabited {σ} : Inhabited (Field σ) := ⟨⟨arbitrary _, [], FieldVal.term (arbitrary _), arbitrary _⟩⟩ diff --git a/stage0/src/Init/Lean/Elab/Util.lean b/stage0/src/Init/Lean/Elab/Util.lean index cab1a6f614..c8670e0ffc 100644 --- a/stage0/src/Init/Lean/Elab/Util.lean +++ b/stage0/src/Init/Lean/Elab/Util.lean @@ -106,12 +106,12 @@ fun stx => | none => throw Macro.Exception.unsupportedSyntax class MonadMacroAdapter (m : Type → Type) := -(getEnv {} : m Environment) -(getCurrMacroScope {} : m MacroScope) -(getNextMacroScope {} : m MacroScope) -(setNextMacroScope {} : MacroScope → m Unit) -(throwError {} {α : Type} : Syntax → MessageData → m α) -(throwUnsupportedSyntax {} {α : Type} : m α) +(getEnv : m Environment) +(getCurrMacroScope : m MacroScope) +(getNextMacroScope : m MacroScope) +(setNextMacroScope : MacroScope → m Unit) +(throwError {α : Type} : Syntax → MessageData → m α) +(throwUnsupportedSyntax {α : Type} : m α) @[inline] def liftMacroM {α} {m : Type → Type} [Monad m] [MonadMacroAdapter m] (x : MacroM α) : m α := do scp ← MonadMacroAdapter.getCurrMacroScope; diff --git a/stage0/src/Init/Lean/Util/MonadCache.lean b/stage0/src/Init/Lean/Util/MonadCache.lean index c44585cc2d..0b5df73ae3 100644 --- a/stage0/src/Init/Lean/Util/MonadCache.lean +++ b/stage0/src/Init/Lean/Util/MonadCache.lean @@ -11,8 +11,8 @@ import Init.Data.HashMap namespace Lean /-- Interface for caching results. -/ class MonadCache (α β : Type) (m : Type → Type) := -(findCached? {} : α → m (Option β)) -(cache {} : α → β → m Unit) +(findCached? : α → m (Option β)) +(cache : α → β → m Unit) /-- If entry `a := b` is already in the cache, then return `b`. Otherwise, execute `b ← f a`, store `a := b` in the cache and return `b`. -/ @@ -36,8 +36,8 @@ instance exceptLift {α β ε : Type} {m : Type → Type} [MonadCache α β m] [ /-- Adapter for implementing `MonadCache` interface using `HashMap`s. We just have to specify how to extract/modify the `HashMap`. -/ class MonadHashMapCacheAdapter (α β : Type) (m : Type → Type) [HasBeq α] [Hashable α] := -(getCache {} : m (HashMap α β)) -(modifyCache {} : (HashMap α β → HashMap α β) → m Unit) +(getCache : m (HashMap α β)) +(modifyCache : (HashMap α β → HashMap α β) → m Unit) namespace MonadHashMapCacheAdapter diff --git a/stage0/src/Init/Lean/Util/Trace.lean b/stage0/src/Init/Lean/Util/Trace.lean index a2a5cd6a38..b865252997 100644 --- a/stage0/src/Init/Lean/Util/Trace.lean +++ b/stage0/src/Init/Lean/Util/Trace.lean @@ -11,15 +11,15 @@ namespace Lean class MonadTracer (m : Type → Type u) := (traceCtx {α} : Name → m α → m α) -(trace {} : Name → (Unit → MessageData) → m PUnit) -(traceM {} : Name → m MessageData → m PUnit) +(trace : Name → (Unit → MessageData) → m PUnit) +(traceM : Name → m MessageData → m PUnit) class MonadTracerAdapter (m : Type → Type) := -(isTracingEnabledFor {} : Name → m Bool) -(addContext {} : MessageData → m MessageData) -(enableTracing {} : Bool → m Bool) -(getTraces {} : m (PersistentArray MessageData)) -(modifyTraces {} : (PersistentArray MessageData → PersistentArray MessageData) → m Unit) +(isTracingEnabledFor : Name → m Bool) +(addContext : MessageData → m MessageData) +(enableTracing : Bool → m Bool) +(getTraces : m (PersistentArray MessageData)) +(modifyTraces : (PersistentArray MessageData → PersistentArray MessageData) → m Unit) private def checkTraceOptionAux (opts : Options) : Name → Bool | n@(Name.str p _ _) => opts.getBool n || (!opts.contains n && checkTraceOptionAux p) @@ -128,10 +128,10 @@ instance : HasToString TraceState := ⟨toString ∘ fmt⟩ end TraceState class SimpleMonadTracerAdapter (m : Type → Type) := -(getOptions {} : m Options) -(modifyTraceState {} : (TraceState → TraceState) → m Unit) -(getTraceState {} : m TraceState) -(addContext {} : MessageData → m MessageData) +(getOptions : m Options) +(modifyTraceState : (TraceState → TraceState) → m Unit) +(getTraceState : m TraceState) +(addContext : MessageData → m MessageData) namespace SimpleMonadTracerAdapter variables {m : Type → Type} [Monad m] [SimpleMonadTracerAdapter m] diff --git a/stage0/src/Init/LeanInit.lean b/stage0/src/Init/LeanInit.lean index 49f55a1d2b..115a600aa8 100644 --- a/stage0/src/Init/LeanInit.lean +++ b/stage0/src/Init/LeanInit.lean @@ -175,10 +175,10 @@ abbrev SyntaxNodeKind := Name /- Syntax AST -/ inductive Syntax -| missing {} : Syntax +| missing : Syntax | node (kind : SyntaxNodeKind) (args : Array Syntax) : Syntax -| atom {} (info : Option SourceInfo) (val : String) : Syntax -| ident {} (info : Option SourceInfo) (rawVal : Substring) (val : Name) (preresolved : List (Name × List String)) : Syntax +| atom (info : Option SourceInfo) (val : String) : Syntax +| ident (info : Option SourceInfo) (rawVal : Substring) (val : Name) (preresolved : List (Name × List String)) : Syntax instance Syntax.inhabited : Inhabited Syntax := ⟨Syntax.missing⟩ @@ -247,8 +247,8 @@ def firstFrontendMacroScope := reservedMacroScope + 1 elaboration). -/ class MonadQuotation (m : Type → Type) := -- Get the fresh scope of the current macro invocation -(getCurrMacroScope {} : m MacroScope) -(getMainModule {} : m Name) +(getCurrMacroScope : m MacroScope) +(getMainModule : m Name) /- Execute action in a new macro invocation context. This transformer should be used at all places that morally qualify as the beginning of a "macro call", e.g. `elabCommand` and `elabTerm` in the case of the elaborator. However, it diff --git a/stage0/src/Init/ShareCommon.lean b/stage0/src/Init/ShareCommon.lean index 7514c93f9b..faca73ca5e 100644 --- a/stage0/src/Init/ShareCommon.lean +++ b/stage0/src/Init/ShareCommon.lean @@ -116,7 +116,7 @@ def PersistentState.shareCommon {α} (s : PersistentState) (a : α) : α × Pers end ShareCommon class MonadShareCommon (m : Type u → Type v) := -(withShareCommon {} {α : Type u} : α → m α) +(withShareCommon {α : Type u} : α → m α) export MonadShareCommon (withShareCommon) diff --git a/stage0/src/Init/Util.lean b/stage0/src/Init/Util.lean index 3584dba211..716c0c0343 100644 --- a/stage0/src/Init/Util.lean +++ b/stage0/src/Init/Util.lean @@ -49,7 +49,7 @@ k (ptrAddrUnsafe a) if ptrAddrUnsafe a == ptrAddrUnsafe b then true else k () inductive PtrEqResult {α : Type u} (x y : α) : Type -| unknown {} : PtrEqResult +| unknown : PtrEqResult | yesEqual (h : x = y) : PtrEqResult @[inline] unsafe def withPtrEqResultUnsafe {α : Type u} {β : Type v} [Subsingleton β] (a b : α) (k : PtrEqResult a b → β) : β := diff --git a/stage0/src/Init/WF.lean b/stage0/src/Init/WF.lean index 1d1e1200af..60d6689fc4 100644 --- a/stage0/src/Init/WF.lean +++ b/stage0/src/Init/WF.lean @@ -189,7 +189,7 @@ def lexWf (ha : WellFounded ra) (hb : WellFounded rb) : WellFounded (Lex ra rb) -- relational product is a Subrelation of the Lex def rprodSubLex : ∀ a b, Rprod ra rb a b → Lex ra rb a b := -@Prod.Rprod.rec _ _ ra rb (fun a b _ => Lex ra rb a b) (fun a₁ b₁ a₂ b₂ h₁ h₂ => Lex.left rb b₁ b₂ h₁) +@Prod.Rprod.rec _ _ ra rb (fun a b _ => Lex ra rb a b) (fun a₁ b₁ a₂ b₂ h₁ h₂ => Lex.left b₁ b₂ h₁) -- The relational product of well founded relations is well-founded def rprodWf (ha : WellFounded ra) (hb : WellFounded rb) : WellFounded (Rprod ra rb) := @@ -301,7 +301,7 @@ def skipLeftWf (α : Type u) {β : Type v} {s : β → β → Prop} (hb : WellFo revLexWf emptyWf hb def mkSkipLeft {α : Type u} {β : Type v} {b₁ b₂ : β} {s : β → β → Prop} (a₁ a₂ : α) (h : s b₁ b₂) : skipLeft α s ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ := -RevLex.right _ _ _ h +RevLex.right _ _ h end instance HasWellFounded {α : Type u} {β : α → Type v} [s₁ : HasWellFounded α] [s₂ : ∀ a, HasWellFounded (β a)] : HasWellFounded (PSigma β) := diff --git a/stage0/stdlib/Init/Control/Alternative.c b/stage0/stdlib/Init/Control/Alternative.c index 4d3e152843..cda7d1f290 100644 --- a/stage0/stdlib/Init/Control/Alternative.c +++ b/stage0/stdlib/Init/Control/Alternative.c @@ -15,14 +15,12 @@ extern "C" { #endif lean_object* l_alternativeHasOrelse___rarg(lean_object*); lean_object* l_assert___rarg(lean_object*, lean_object*, uint8_t); -lean_object* l_failure___rarg(lean_object*, lean_object*); lean_object* l_guard___rarg(lean_object*, lean_object*, uint8_t); lean_object* l_guardb(lean_object*); lean_object* l_optional___rarg___closed__1; lean_object* l_guardb___rarg(lean_object*, uint8_t); lean_object* l_assert(lean_object*); lean_object* l_optional___rarg(lean_object*, lean_object*, lean_object*); -lean_object* l_failure(lean_object*); lean_object* l_guard___rarg___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_optional___rarg___lambda__1(lean_object*); lean_object* l_alternativeHasOrelse(lean_object*, lean_object*); @@ -49,25 +47,6 @@ x_3 = lean_alloc_closure((void*)(l_alternativeHasOrelse___rarg), 1, 0); return x_3; } } -lean_object* l_failure___rarg(lean_object* x_1, lean_object* x_2) { -_start: -{ -lean_object* x_3; lean_object* x_4; -x_3 = lean_ctor_get(x_1, 1); -lean_inc(x_3); -lean_dec(x_1); -x_4 = lean_apply_1(x_3, lean_box(0)); -return x_4; -} -} -lean_object* l_failure(lean_object* x_1) { -_start: -{ -lean_object* x_2; -x_2 = lean_alloc_closure((void*)(l_failure___rarg), 2, 0); -return x_2; -} -} lean_object* l_guard___rarg(lean_object* x_1, lean_object* x_2, uint8_t x_3) { _start: {