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

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2020-05-12 14:58:11 -07:00
parent 50990b99d6
commit ab5c0301d6
27 changed files with 105 additions and 127 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
stage0/src/Init/Coe.lean
View file

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

3
stage0/src/Init/Control/Alternative.lean
View file

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

2
stage0/src/Init/Control/Applicative.lean
View file

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

4
stage0/src/Init/Control/EState.lean
View file

@ -11,8 +11,8 @@ universes u v
namespace EStateM
inductive Result (ε σ α : Type u)
| ok {} : α → σ → Result
| error {} : ε → σ → Result
| ok : α → σ → Result
| error : ε → σ → Result
variables {ε σ α : Type u}

12
stage0/src/Init/Control/Except.lean
View file

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

10
stage0/src/Init/Control/Lift.lean
View file

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

10
stage0/src/Init/Control/Reader.lean
View file

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

12
stage0/src/Init/Control/State.lean
View file

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

38
stage0/src/Init/Core.lean
View file

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

2
stage0/src/Init/Data/AssocList.lean
View file

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

10
stage0/src/Init/Data/BinomialHeap/Basic.lean
View file

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

6
stage0/src/Init/Data/PersistentHashMap/Basic.lean
View file

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

4
stage0/src/Init/Data/RBMap/Basic.lean
View file

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

2
stage0/src/Init/Lean/Data/Json/FromToJson.lean
View file

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

8
stage0/src/Init/Lean/Data/Json/Parser.lean
View file

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

2
stage0/src/Init/Lean/Data/KVMap.lean
View file

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

6
stage0/src/Init/Lean/Data/LOption.lean
View file

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

10
stage0/src/Init/Lean/Elab/Log.lean
View file

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

8
stage0/src/Init/Lean/Elab/StructInst.lean
View file

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

12
stage0/src/Init/Lean/Elab/Util.lean
View file

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

8
stage0/src/Init/Lean/Util/MonadCache.lean
View file

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

22
stage0/src/Init/Lean/Util/Trace.lean
View file

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

10
stage0/src/Init/LeanInit.lean
View file

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

2
stage0/src/Init/ShareCommon.lean
View file

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

2
stage0/src/Init/Util.lean
View file

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

4
stage0/src/Init/WF.lean
View file

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

21
stage0/stdlib/Init/Control/Alternative.c
View file

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