From 7241d4014675cc684a04850bc2cd62893f3a84ac Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 27 Oct 2020 18:29:54 -0700 Subject: [PATCH] chore: update stage0 --- stage0/src/Init/Coe.lean | 10 +- stage0/src/Init/Control/Alternative.lean | 2 +- stage0/src/Init/Control/Applicative.lean | 18 +- stage0/src/Init/Control/Conditional.lean | 15 +- stage0/src/Init/Control/EState.lean | 12 +- stage0/src/Init/Control/Except.lean | 2 +- stage0/src/Init/Control/Id.lean | 4 +- stage0/src/Init/Control/Monad.lean | 9 +- stage0/src/Init/Control/MonadControl.lean | 6 +- stage0/src/Init/Core.lean | 125 ++++------ stage0/src/Init/Data/Array/Basic.lean | 30 +-- stage0/src/Init/Data/ByteArray/Basic.lean | 2 +- stage0/src/Init/Data/Char/Basic.lean | 6 +- stage0/src/Init/Data/Fin/Basic.lean | 16 +- stage0/src/Init/Data/Float.lean | 18 +- stage0/src/Init/Data/Int/Basic.lean | 18 +- stage0/src/Init/Data/List/Basic.lean | 60 ++--- stage0/src/Init/Data/Nat/Basic.lean | 12 +- stage0/src/Init/Data/Nat/Div.lean | 4 +- stage0/src/Init/Data/Option/Basic.lean | 4 +- stage0/src/Init/Data/String/Basic.lean | 8 +- stage0/src/Init/Data/UInt.lean | 90 +++---- stage0/src/Init/LeanInit.lean | 33 ++- stage0/src/Init/System/IO.lean | 20 +- stage0/src/Init/WF.lean | 18 +- stage0/src/Lean/Attributes.lean | 2 +- stage0/src/Lean/Compiler/ConstFolding.lean | 16 +- stage0/src/Lean/Compiler/ExternAttr.lean | 2 +- stage0/src/Lean/Compiler/IR/Basic.lean | 27 +-- stage0/src/Lean/Compiler/IR/Borrow.lean | 4 +- .../Lean/Compiler/IR/ElimDeadBranches.lean | 2 +- stage0/src/Lean/Compiler/IR/FreeVars.lean | 4 +- stage0/src/Lean/Compiler/InlineAttrs.lean | 2 +- stage0/src/Lean/Compiler/Specialize.lean | 2 +- stage0/src/Lean/Compiler/Util.lean | 2 +- stage0/src/Lean/CoreM.lean | 4 +- stage0/src/Lean/Data/Format.lean | 6 +- stage0/src/Lean/Data/Json/FromToJson.lean | 46 ++-- stage0/src/Lean/Data/JsonRpc.lean | 18 +- stage0/src/Lean/Data/KVMap.lean | 4 +- stage0/src/Lean/Data/LBool.lean | 2 +- stage0/src/Lean/Data/LOption.lean | 4 +- stage0/src/Lean/Data/Lsp/Basic.lean | 72 +++--- stage0/src/Lean/Data/Lsp/Capabilities.lean | 4 +- stage0/src/Lean/Data/Lsp/Communication.lean | 8 +- stage0/src/Lean/Data/Lsp/Diagnostics.lean | 24 +- stage0/src/Lean/Data/Lsp/Hover.lean | 8 +- stage0/src/Lean/Data/Lsp/InitShutdown.lean | 12 +- stage0/src/Lean/Data/Lsp/TextSync.lean | 20 +- stage0/src/Lean/Data/Lsp/Workspace.lean | 4 +- stage0/src/Lean/Data/Name.lean | 10 +- stage0/src/Lean/Data/Occurrences.lean | 2 +- stage0/src/Lean/Data/SMap.lean | 4 +- stage0/src/Lean/Data/Trie.lean | 2 +- stage0/src/Lean/Delaborator.lean | 42 ++-- stage0/src/Lean/Elab/Tactic/Basic.lean | 2 +- stage0/src/Lean/Elab/Term.lean | 4 +- stage0/src/Lean/Eval.lean | 14 +- stage0/src/Lean/Expr.lean | 12 +- stage0/src/Lean/HeadIndex.lean | 2 +- stage0/src/Lean/InternalExceptionId.lean | 2 +- stage0/src/Lean/Level.lean | 4 +- stage0/src/Lean/Message.lean | 4 +- stage0/src/Lean/Meta/AbstractMVars.lean | 2 +- stage0/src/Lean/Meta/AppBuilder.lean | 4 +- stage0/src/Lean/Meta/Basic.lean | 12 +- stage0/src/Lean/Meta/DiscrTree.lean | 23 +- stage0/src/Lean/Meta/DiscrTreeTypes.lean | 2 +- stage0/src/Lean/Meta/ReduceEval.lean | 15 +- stage0/src/Lean/Meta/TransparencyMode.lean | 2 +- stage0/src/Lean/MetavarContext.lean | 8 +- stage0/src/Lean/Parser/Basic.lean | 8 +- stage0/src/Lean/ParserCompiler.lean | 2 +- stage0/src/Lean/PrettyPrinter/Formatter.lean | 2 +- .../src/Lean/PrettyPrinter/Parenthesizer.lean | 2 +- stage0/src/Lean/Server.lean | 14 +- stage0/src/Lean/Syntax.lean | 2 +- stage0/src/Lean/Util/MonadCache.lean | 12 +- stage0/src/Lean/Util/SCC.lean | 4 +- stage0/src/Std/Data/AssocList.lean | 12 +- stage0/src/Std/Data/DList.lean | 6 +- stage0/src/Std/Data/HashMap.lean | 20 +- stage0/src/Std/Data/HashSet.lean | 18 +- stage0/src/Std/Data/PersistentArray.lean | 4 +- stage0/src/Std/Data/PersistentHashMap.lean | 56 ++--- stage0/src/Std/Data/PersistentHashSet.lean | 8 +- stage0/src/Std/Data/RBMap.lean | 2 +- stage0/src/Std/Data/RBTree.lean | 2 +- stage0/stdlib/Init/Control/EState.c | 58 ++--- stage0/stdlib/Init/Core.c | 22 +- stage0/stdlib/Lean/Delaborator.c | 223 ++++++------------ stage0/stdlib/Lean/Elab/Do.c | 97 ++------ stage0/stdlib/Lean/Meta/DiscrTree.c | 2 +- 93 files changed, 692 insertions(+), 897 deletions(-) diff --git a/stage0/src/Init/Coe.lean b/stage0/src/Init/Coe.lean index e3833d90bd..85a68a4bb4 100644 --- a/stage0/src/Init/Coe.lean +++ b/stage0/src/Init/Coe.lean @@ -130,12 +130,12 @@ instance subtypeCoe {α : Sort u} {p : α → Prop} : CoeHead { x // p x } α := coe := fun v => v.val } -/- Coe & HasOfNat bridge -/ +/- Coe & OfNat bridge -/ /- - Remark: one may question why we use `HasOfNat α` instead of `Coe Nat α`. - Reason: `HasOfNat` is for implementing polymorphic numeric literals, and we may + Remark: one may question why we use `OfNat α` instead of `Coe Nat α`. + Reason: `OfNat` 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 : α) +instance hasOfNatOfCoe {α : Type u} {β : Type v} [OfNat α] [Coe α β] : OfNat β := { + ofNat := fun (n : Nat) => coe (OfNat.ofNat n : α) } diff --git a/stage0/src/Init/Control/Alternative.lean b/stage0/src/Init/Control/Alternative.lean index 91c0b89589..91a94fdb71 100644 --- a/stage0/src/Init/Control/Alternative.lean +++ b/stage0/src/Init/Control/Alternative.lean @@ -12,7 +12,7 @@ class Alternative (f : Type u → Type v) extends Applicative f : Type (max (u+1 (failure : {α : Type u} → f α) (orelse : {α : Type u} → f α → f α → f α) -instance (f : Type u → Type v) (α : Type u) [Alternative f] : HasOrelse (f α) := ⟨Alternative.orelse⟩ +instance (f : Type u → Type v) (α : Type u) [Alternative f] : OrElse (f α) := ⟨Alternative.orelse⟩ variables {f : Type u → Type v} [Alternative f] {α : Type u} diff --git a/stage0/src/Init/Control/Applicative.lean b/stage0/src/Init/Control/Applicative.lean index c46005fcd4..8280ad08ca 100644 --- a/stage0/src/Init/Control/Applicative.lean +++ b/stage0/src/Init/Control/Applicative.lean @@ -8,23 +8,11 @@ import Init.Control.Functor open Function universes u v -class HasPure (f : Type u → Type v) := - (pure {α : Type u} : α → f α) - -export HasPure (pure) - -class HasSeq (f : Type u → Type v) : Type (max (u+1) v) := - (seq : {α β : Type u} → f (α → β) → f α → f β) - -class HasSeqLeft (f : Type u → Type v) : Type (max (u+1) v) := - (seqLeft : {α : Type u} → f α → f PUnit → f α) - -class HasSeqRight (f : Type u → Type v) : Type (max (u+1) v) := - (seqRight : {β : Type u} → f PUnit → f β → f β) - class Pure (f : Type u → Type v) := (pure {α : Type u} : α → f α) +export Pure (pure) + class Seq (f : Type u → Type v) : Type (max (u+1) v) := (seq : {α β : Type u} → f (α → β) → f α → f β) @@ -34,7 +22,7 @@ class SeqLeft (f : Type u → Type v) : Type (max (u+1) v) := class SeqRight (f : Type u → Type v) : Type (max (u+1) v) := (seqRight : {β : Type u} → f PUnit → f β → f β) -class Applicative (f : Type u → Type v) extends Functor f, HasPure f, HasSeq f, HasSeqLeft f, HasSeqRight f := +class Applicative (f : Type u → Type v) extends Functor f, Pure f, Seq f, SeqLeft f, SeqRight f := (map := fun x y => pure x <*> y) (seqLeft := fun a b => const _ <$> a <*> b) (seqRight := fun a b => const _ id <$> a <*> b) diff --git a/stage0/src/Init/Control/Conditional.lean b/stage0/src/Init/Control/Conditional.lean index 4a72b58ce9..1576477315 100644 --- a/stage0/src/Init/Control/Conditional.lean +++ b/stage0/src/Init/Control/Conditional.lean @@ -8,29 +8,26 @@ import Init.Control.Monad import Init.Data.Option.Basic universes u v -class HasToBool (α : Type u) := - (toBool : α → Bool) - class ToBool (α : Type u) := (toBool : α → Bool) -export HasToBool (toBool) +export ToBool (toBool) -instance : HasToBool Bool := ⟨id⟩ -instance {α} : HasToBool (Option α) := ⟨Option.toBool⟩ +instance : ToBool Bool := ⟨id⟩ +instance {α} : ToBool (Option α) := ⟨Option.toBool⟩ -@[macroInline] def bool {β : Type u} {α : Type v} [HasToBool β] (f t : α) (b : β) : α := +@[macroInline] def bool {β : Type u} {α : Type v} [ToBool β] (f t : α) (b : β) : α := match toBool b with | true => t | false => f -@[macroInline] def orM {m : Type u → Type v} {β : Type u} [Monad m] [HasToBool β] (x y : m β) : m β := do +@[macroInline] def orM {m : Type u → Type v} {β : Type u} [Monad m] [ToBool β] (x y : m β) : m β := do let b ← x match toBool b with | true => pure b | false => y -@[macroInline] def andM {m : Type u → Type v} {β : Type u} [Monad m] [HasToBool β] (x y : m β) : m β := do +@[macroInline] def andM {m : Type u → Type v} {β : Type u} [Monad m] [ToBool β] (x y : m β) : m β := do let b ← x match toBool b with | true => y diff --git a/stage0/src/Init/Control/EState.lean b/stage0/src/Init/Control/EState.lean index e948df4223..3c37d635a4 100644 --- a/stage0/src/Init/Control/EState.lean +++ b/stage0/src/Init/Control/EState.lean @@ -69,15 +69,15 @@ class Backtrackable (δ : outParam $ Type u) (σ : Type u) := | Result.error e s => handle e (Backtrackable.restore s d) | ok => ok -@[inline] protected def orelse {δ} [Backtrackable δ σ] (x₁ x₂ : EStateM ε σ α) : EStateM ε σ α := fun s => +@[inline] protected def orElse {δ} [Backtrackable δ σ] (x₁ x₂ : EStateM ε σ α) : EStateM ε σ α := fun s => let d := Backtrackable.save s; match x₁ s with | Result.error _ s => x₂ (Backtrackable.restore s d) | 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' {δ} [Backtrackable δ σ] (x₁ x₂ : EStateM ε σ α) (useFirstEx := true) : EStateM ε σ α := fun s => +/-- 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' {δ} [Backtrackable δ σ] (x₁ x₂ : EStateM ε σ α) (useFirstEx := true) : EStateM ε σ α := fun s => let d := Backtrackable.save s; match x₁ s with | Result.error e₁ s₁ => @@ -113,8 +113,8 @@ instance : Monad (EStateM ε σ) := { seqRight := EStateM.seqRight } -instance {δ} [Backtrackable δ σ] : HasOrelse (EStateM ε σ α) := { - orelse := EStateM.orelse +instance {δ} [Backtrackable δ σ] : OrElse (EStateM ε σ α) := { + orElse := EStateM.orElse } instance : MonadStateOf σ (EStateM ε σ) := { diff --git a/stage0/src/Init/Control/Except.lean b/stage0/src/Init/Control/Except.lean index bea8f2379b..74af61d693 100644 --- a/stage0/src/Init/Control/Except.lean +++ b/stage0/src/Init/Control/Except.lean @@ -171,7 +171,7 @@ variables {ε : Type u} {m : Type v → Type w} @[inline] protected def orelse [MonadExcept ε m] {α : Type v} (t₁ t₂ : m α) : m α := tryCatch t₁ fun _ => t₂ -instance [MonadExcept ε m] {α : Type v} : HasOrelse (m α) := ⟨MonadExcept.orelse⟩ +instance [MonadExcept ε m] {α : Type v} : OrElse (m α) := ⟨MonadExcept.orelse⟩ /-- 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. -/ diff --git a/stage0/src/Init/Control/Id.lean b/stage0/src/Init/Control/Id.lean index a80de1d88f..79e41da7bd 100644 --- a/stage0/src/Init/Control/Id.lean +++ b/stage0/src/Init/Control/Id.lean @@ -26,7 +26,7 @@ instance : Monad Id := { @[inline] protected def run {α : Type u} (x : Id α) : α := x -instance {α} [HasOfNat α] : HasOfNat (Id α) := -inferInstanceAs (HasOfNat α) +instance {α} [OfNat α] : OfNat (Id α) := +inferInstanceAs (OfNat α) end Id diff --git a/stage0/src/Init/Control/Monad.lean b/stage0/src/Init/Control/Monad.lean index 2ab86ef0ab..2a7f1f3300 100644 --- a/stage0/src/Init/Control/Monad.lean +++ b/stage0/src/Init/Control/Monad.lean @@ -10,18 +10,15 @@ universes u v w open Function -class HasBind (m : Type u → Type v) := - (bind : {α β : Type u} → m α → (α → m β) → m β) - class Bind (m : Type u → Type v) := (bind : {α β : Type u} → m α → (α → m β) → m β) -export HasBind (bind) +export Bind (bind) -@[inline] def mcomp {α : Type u} {β δ : Type v} {m : Type v → Type w} [HasBind m] (f : α → m β) (g : β → m δ) : α → m δ := +@[inline] def mcomp {α : Type u} {β δ : Type v} {m : Type v → Type w} [Bind m] (f : α → m β) (g : β → m δ) : α → m δ := fun a => f a >>= g -class Monad (m : Type u → Type v) extends Applicative m, HasBind m : Type (max (u+1) v) := +class Monad (m : Type u → Type v) extends Applicative m, Bind m : Type (max (u+1) v) := (map := fun f x => x >>= pure ∘ f) (seq := fun f x => f >>= (fun y => y <$> x)) (seqLeft := fun x y => x >>= fun a => y >>= fun _ => pure a) diff --git a/stage0/src/Init/Control/MonadControl.lean b/stage0/src/Init/Control/MonadControl.lean index f695092c90..fd8a6811c9 100644 --- a/stage0/src/Init/Control/MonadControl.lean +++ b/stage0/src/Init/Control/MonadControl.lean @@ -28,18 +28,18 @@ instance (m n o) [MonadControlT m n] [MonadControl n o] : MonadControlT m o := { restoreM := MonadControl.restoreM ∘ restoreM } -instance (m : Type u → Type v) [HasPure m] : MonadControlT m m := { +instance (m : Type u → Type v) [Pure m] : MonadControlT m m := { stM := fun α => α, liftWith := fun f => f fun x => x, restoreM := fun x => pure x } @[inline] -def controlAt (m : Type u → Type v) {n : Type u → Type w} [s1 : MonadControlT m n] [s2 : HasBind n] {α : Type u} +def controlAt (m : Type u → Type v) {n : Type u → Type w} [s1 : MonadControlT m n] [s2 : Bind n] {α : Type u} (f : ({β : Type u} → n β → m (stM m n β)) → m (stM m n α)) : n α := liftWith f >>= restoreM @[inline] -def control {m : Type u → Type v} {n : Type u → Type w} [MonadControlT m n] [HasBind n] {α : Type u} +def control {m : Type u → Type v} {n : Type u → Type w} [MonadControlT m n] [Bind n] {α : Type u} (f : ({β : Type u} → n β → m (stM m n β)) → m (stM m n α)) : n α := controlAt m f diff --git a/stage0/src/Init/Core.lean b/stage0/src/Init/Core.lean index 018e17aaa8..739fb3dd6d 100644 --- a/stage0/src/Init/Core.lean +++ b/stage0/src/Init/Core.lean @@ -270,15 +270,12 @@ inductive Nat | succ (n : Nat) : Nat /- For numeric literals notation -/ -class HasOfNat (α : Type u) := - (ofNat : Nat → α) - -export HasOfNat (ofNat) - class OfNat (α : Type u) := (ofNat : Nat → α) -instance : HasOfNat Nat := ⟨id⟩ +export OfNat (ofNat) + +instance : OfNat Nat := ⟨id⟩ /- Auxiliary axiom used to implement `sorry`. TODO: add this theorem on-demand. That is, @@ -286,23 +283,6 @@ instance : HasOfNat Nat := ⟨id⟩ axiom sorryAx (α : Sort u) (synthetic := true) : α /- Declare builtin and reserved notation -/ -class HasAdd (α : Type u) := (add : α → α → α) -class HasMul (α : Type u) := (mul : α → α → α) -class HasNeg (α : Type u) := (neg : α → α) -class HasSub (α : Type u) := (sub : α → α → α) -class HasDiv (α : Type u) := (div : α → α → α) -class HasMod (α : Type u) := (mod : α → α → α) -class HasModN (α : Type u) := (modn : α → Nat → α) -class HasLessEq (α : Type u) := (LessEq : α → α → Prop) -class HasLess (α : Type u) := (Less : α → α → Prop) -class HasBeq (α : Type u) := (beq : α → α → Bool) -class HasAppend (α : Type u) := (append : α → α → α) -class HasOrelse (α : Type u) := (orelse : α → α → α) -class HasAndthen (α : Type u) := (andthen : α → α → α) -class HasEquiv (α : Sort u) := (Equiv : α → α → Prop) -class HasEmptyc (α : Type u) := (emptyc : α) -class HasPow (α : Type u) (β : Type v) := (pow : α → β → α) - class Add (α : Type u) := (add : α → α → α) class Mul (α : Type u) := (mul : α → α → α) class Neg (α : Type u) := (neg : α → α) @@ -312,7 +292,7 @@ class Mod (α : Type u) := (mod : α → α → α) class ModN (α : Type u) := (modn : α → Nat → α) class LessEq (α : Type u) := (LessEq : α → α → Prop) class Less (α : Type u) := (Less : α → α → Prop) -class Beq (α : Type u) := (beq : α → α → Bool) +class BEq (α : Type u) := (beq : α → α → Bool) class Append (α : Type u) := (append : α → α → α) class OrElse (α : Type u) := (orElse : α → α → α) class AndThen (α : Type u) := (andThen : α → α → α) @@ -320,8 +300,8 @@ class Equiv (α : Sort u) := (Equiv : α → α → Prop) class EmptyCollection (α : Type u) := (emptyCollection : α) class Pow (α : Type u) (β : Type v) := (pow : α → β → α) -@[reducible] def GreaterEq {α : Type u} [HasLessEq α] (a b : α) : Prop := HasLessEq.LessEq b a -@[reducible] def Greater {α : Type u} [HasLess α] (a b : α) : Prop := HasLess.Less b a +@[reducible] def GreaterEq {α : Type u} [LessEq α] (a b : α) : Prop := LessEq.LessEq b a +@[reducible] def Greater {α : Type u} [Less α] (a b : α) : Prop := Less.Less b a /- Nat basic instances -/ @@ -333,9 +313,9 @@ protected def Nat.add : (@& Nat) → (@& Nat) → Nat /- We mark the following definitions as pattern to make sure they can be used in recursive equations, and reduced by the equation Compiler. -/ -attribute [matchPattern] Nat.add HasAdd.add HasNeg.neg +attribute [matchPattern] Nat.add Add.add Neg.neg -instance : HasAdd Nat := ⟨Nat.add⟩ +instance : Add Nat := ⟨Nat.add⟩ def std.priority.default : Nat := 1000 def std.priority.max : Nat := 0xFFFFFFFF @@ -403,78 +383,75 @@ inductive PNonScalar : Type u /- sizeof -/ -class HasSizeof (α : Sort u) := - (sizeof : α → Nat) - -export HasSizeof (sizeof) - class SizeOf (α : Sort u) := (sizeOf : α → Nat) +export SizeOf (sizeOf) + /- -Declare sizeof instances and theorems for types declared before HasSizeof. -From now on, the inductive Compiler will automatically generate sizeof instances and theorems. +Declare sizeOf instances and theorems for types declared before SizeOf. +From now on, the inductive Compiler will automatically generate sizeOf instances and theorems. -/ -/- Every Type `α` has a default HasSizeof instance that just returns 0 for every element of `α` -/ -protected def default.sizeof (α : Sort u) : α → Nat +/- Every Type `α` has a default SizeOf instance that just returns 0 for every element of `α` -/ +protected def default.sizeOf (α : Sort u) : α → Nat | a => 0 -instance (α : Sort u) : HasSizeof α := - ⟨default.sizeof α⟩ +instance (α : Sort u) : SizeOf α := + ⟨default.sizeOf α⟩ -instance : HasSizeof Nat := { - sizeof := fun n => n +instance : SizeOf Nat := { + sizeOf := fun n => n } -instance (α : Type u) (β : Type v) [HasSizeof α] [HasSizeof β] : HasSizeof (Prod α β) := { - sizeof := fun (a, b) => 1 + sizeof a + sizeof b +instance (α : Type u) (β : Type v) [SizeOf α] [SizeOf β] : SizeOf (Prod α β) := { + sizeOf := fun (a, b) => 1 + sizeOf a + sizeOf b } -instance (α : Type u) (β : Type v) [HasSizeof α] [HasSizeof β] : HasSizeof (Sum α β) := { - sizeof := fun - | Sum.inl a => 1 + sizeof a - | Sum.inr b => 1 + sizeof b +instance (α : Type u) (β : Type v) [SizeOf α] [SizeOf β] : SizeOf (Sum α β) := { + sizeOf := fun + | Sum.inl a => 1 + sizeOf a + | Sum.inr b => 1 + sizeOf b } -instance (α : Type u) (β : Type v) [HasSizeof α] [HasSizeof β] : HasSizeof (PSum α β) := { - sizeof := fun - | PSum.inl a => 1 + sizeof a - | PSum.inr b => 1 + sizeof b +instance (α : Type u) (β : Type v) [SizeOf α] [SizeOf β] : SizeOf (PSum α β) := { + sizeOf := fun + | PSum.inl a => 1 + sizeOf a + | PSum.inr b => 1 + sizeOf b } -instance (α : Type u) (β : α → Type v) [HasSizeof α] [∀ a, HasSizeof (β a)] : HasSizeof (Sigma β) := { - sizeof := fun ⟨a, b⟩ => 1 + sizeof a + sizeof b +instance (α : Type u) (β : α → Type v) [SizeOf α] [∀ a, SizeOf (β a)] : SizeOf (Sigma β) := { + sizeOf := fun ⟨a, b⟩ => 1 + sizeOf a + sizeOf b } -instance (α : Type u) (β : α → Type v) [HasSizeof α] [(a : α) → HasSizeof (β a)] : HasSizeof (PSigma β) := { - sizeof := fun ⟨a, b⟩ => 1 + sizeof a + sizeof b +instance (α : Type u) (β : α → Type v) [SizeOf α] [(a : α) → SizeOf (β a)] : SizeOf (PSigma β) := { + sizeOf := fun ⟨a, b⟩ => 1 + sizeOf a + sizeOf b } -instance : HasSizeof PUnit := { - sizeof := fun _ => 1 +instance : SizeOf PUnit := { + sizeOf := fun _ => 1 } -instance : HasSizeof Bool := { - sizeof := fun _ => 1 +instance : SizeOf Bool := { + sizeOf := fun _ => 1 } -instance (α : Type u) [HasSizeof α] : HasSizeof (Option α) := { - sizeof := fun +instance (α : Type u) [SizeOf α] : SizeOf (Option α) := { + sizeOf := fun | none => 1 - | some a => 1 + sizeof a + | some a => 1 + sizeOf a } -instance (α : Type u) [HasSizeof α] : HasSizeof (List α) := { - sizeof := fun as => +instance (α : Type u) [SizeOf α] : SizeOf (List α) := { + sizeOf := fun as => let rec loop | List.nil => 1 - | List.cons x xs => 1 + sizeof x + loop xs + | List.cons x xs => 1 + sizeOf x + loop xs loop as } -instance {α : Type u} [HasSizeof α] (p : α → Prop) : HasSizeof (Subtype p) := { - sizeof := fun ⟨a, _⟩ => sizeof a +instance {α : Type u} [SizeOf α] (p : α → Prop) : SizeOf (Subtype p) := { + sizeOf := fun ⟨a, _⟩ => sizeOf a } theorem natAddZero (n : Nat) : n + 0 = n := rfl @@ -513,7 +490,7 @@ theorem optParamEq (α : Sort u) (default : α) : optParam α default = α := rf @[extern c inline "#1 || #2"] def strictOr (b₁ b₂ : Bool) := b₁ || b₂ @[extern c inline "#1 && #2"] def strictAnd (b₁ b₂ : Bool) := b₁ && b₂ -@[inline] def bne {α : Type u} [HasBeq α] (a b : α) : Bool := +@[inline] def bne {α : Type u} [BEq α] (a b : α) : Bool := !(a == b) /- Logical connectives an equality -/ @@ -792,7 +769,7 @@ theorem Exists.elim {α : Sort u} {p : α → Prop} {b : Prop} export Decidable (isTrue isFalse decide) -instance {α : Type u} [DecidableEq α] : HasBeq α := +instance {α : Type u} [DecidableEq α] : BEq α := ⟨fun a b => decide (a = b)⟩ theorem decideTrueEqTrue (h : Decidable True) : @decide True h = true := @@ -1273,21 +1250,21 @@ instance [DecidableEq α] [DecidableEq β] : DecidableEq (α × β) := | (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 [HasBeq α] [HasBeq β] : HasBeq (α × β) := { +instance [BEq α] [BEq β] : BEq (α × β) := { beq := fun ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ => a₁ == a₂ && b₁ == b₂ } -instance [HasLess α] [HasLess β] : HasLess (α × β) := { +instance [Less α] [Less β] : Less (α × β) := { Less := fun s t => s.1 < t.1 ∨ (s.1 = t.1 ∧ s.2 < t.2) } instance prodHasDecidableLt - [HasLess α] [HasLess β] [DecidableEq α] [DecidableEq β] + [Less α] [Less β] [DecidableEq α] [DecidableEq β] [(a b : α) → Decidable (a < b)] [(a b : β) → Decidable (a < b)] : (s t : α × β) → Decidable (s < t) := fun t s => inferInstanceAs (Decidable (_ ∨ _)) -theorem Prod.ltDef [HasLess α] [HasLess β] (s t : α × β) : (s < t) = (s.1 < t.1 ∨ (s.1 = t.1 ∧ s.2 < t.2)) := +theorem Prod.ltDef [Less α] [Less β] (s t : α × β) : (s < t) = (s.1 < t.1 ∨ (s.1 = t.1 ∧ s.2 < t.2)) := rfl end @@ -1330,7 +1307,7 @@ class Setoid (α : Sort u) := (r : α → α → Prop) (iseqv {} : Equivalence r) -instance {α : Sort u} [Setoid α] : HasEquiv α := +instance {α : Sort u} [Setoid α] : Equiv α := ⟨Setoid.r⟩ namespace Setoid diff --git a/stage0/src/Init/Data/Array/Basic.lean b/stage0/src/Init/Data/Array/Basic.lean index 7481e2468d..c544b2f24a 100644 --- a/stage0/src/Init/Data/Array/Basic.lean +++ b/stage0/src/Init/Data/Array/Basic.lean @@ -59,7 +59,7 @@ theorem szMkArrayEq (n : Nat) (v : α) : (mkArray n v).sz = n := def empty : Array α := mkEmpty 0 -instance : HasEmptyc (Array α) := ⟨Array.empty⟩ +instance : EmptyCollection (Array α) := ⟨Array.empty⟩ instance : Inhabited (Array α) := ⟨Array.empty⟩ def isEmpty (a : Array α) : Bool := @@ -324,7 +324,7 @@ match findIdxAux a p 0 with | some i => i | none => panic! "failed to find element" -def getIdx? [HasBeq α] (a : Array α) (v : α) : Option Nat := +def getIdx? [BEq α] (a : Array α) (v : α) : Option Nat := a.findIdx? $ fun a => a == v end @@ -541,7 +541,7 @@ end protected def append (a : Array α) (b : Array α) : Array α := b.foldl (fun a v => a.push v) a -instance : HasAppend (Array α) := ⟨Array.append⟩ +instance : Append (Array α) := ⟨Array.append⟩ -- TODO(Leo): justify termination using wf-rec @[specialize] partial def isEqvAux (a b : Array α) (hsz : a.size = b.size) (p : α → α → Bool) : Nat → Bool @@ -561,8 +561,8 @@ if h : a.size = b.size then else false -instance [HasBeq α] : HasBeq (Array α) := -⟨fun a b => isEqv a b HasBeq.beq⟩ +instance [BEq α] : BEq (Array α) := +⟨fun a b => isEqv a b BEq.beq⟩ -- TODO(Leo): justify termination using wf-rec, and use `swap` partial def reverseAux : Array α → Nat → Array α @@ -628,7 +628,7 @@ filterMapMAux f as 0 Array.empty @[inline] def filterMap {α β : Type u} (f : α → Option β) (as : Array α) : Array β := Id.run $ filterMapM f as -partial def indexOfAux {α} [HasBeq α] (a : Array α) (v : α) : Nat → Option (Fin a.size) +partial def indexOfAux {α} [BEq α] (a : Array α) (v : α) : Nat → Option (Fin a.size) | i => if h : i < a.size then let idx : Fin a.size := ⟨i, h⟩; @@ -636,7 +636,7 @@ partial def indexOfAux {α} [HasBeq α] (a : Array α) (v : α) : Nat → Option else indexOfAux a v (i+1) else none -def indexOf? {α} [HasBeq α] (a : Array α) (v : α) : Option (Fin a.size) := +def indexOf? {α} [BEq α] (a : Array α) (v : α) : Option (Fin a.size) := indexOfAux a v 0 partial def eraseIdxAux {α} : Nat → Array α → Array α @@ -679,13 +679,13 @@ end def eraseIdx' {α} (a : Array α) (i : Fin a.size) : { r : Array α // r.size = a.size - 1 } := eraseIdxSzAux a (i.val + 1) a rfl -def contains [HasBeq α] (as : Array α) (a : α) : Bool := +def contains [BEq α] (as : Array α) (a : α) : Bool := as.any $ fun b => a == b -def elem [HasBeq α] (a : α) (as : Array α) : Bool := +def elem [BEq α] (a : α) (as : Array α) : Bool := as.contains a -def erase [HasBeq α] (as : Array α) (a : α) : Array α := +def erase [BEq α] (as : Array α) (a : α) : Array α := match as.indexOf? a with | none => as | some i => as.feraseIdx i @@ -807,7 +807,7 @@ else @[inline] def partition {α : Type u} (p : α → Bool) (as : Array α) : Array α × Array α := partitionAux p as 0 #[] #[] -partial def isPrefixOfAux {α : Type u} [HasBeq α] (as bs : Array α) (hle : as.size ≤ bs.size) : Nat → Bool +partial def isPrefixOfAux {α : Type u} [BEq α] (as bs : Array α) (hle : as.size ≤ bs.size) : Nat → Bool | i => if h : i < as.size then let a := as.get ⟨i, h⟩; @@ -820,26 +820,26 @@ partial def isPrefixOfAux {α : Type u} [HasBeq α] (as bs : Array α) (hle : as true /- Return true iff `as` is a prefix of `bs` -/ -def isPrefixOf {α : Type u} [HasBeq α] (as bs : Array α) : Bool := +def isPrefixOf {α : Type u} [BEq α] (as bs : Array α) : Bool := if h : as.size ≤ bs.size then isPrefixOfAux as bs h 0 else false -private def allDiffAuxAux {α} [HasBeq α] (as : Array α) (a : α) : forall (i : Nat), i < as.size → Bool +private def allDiffAuxAux {α} [BEq α] (as : Array α) (a : α) : forall (i : Nat), i < as.size → Bool | 0, h => true | i+1, h => have i < as.size from Nat.ltTrans (Nat.ltSuccSelf _) h; a != as.get ⟨i, this⟩ && allDiffAuxAux as a i this -private partial def allDiffAux {α} [HasBeq α] (as : Array α) : Nat → Bool +private partial def allDiffAux {α} [BEq α] (as : Array α) : Nat → Bool | i => if h : i < as.size then allDiffAuxAux as (as.get ⟨i, h⟩) i h && allDiffAux as (i+1) else true -def allDiff {α} [HasBeq α] (as : Array α) : Bool := +def allDiff {α} [BEq α] (as : Array α) : Bool := allDiffAux as 0 @[specialize] partial def zipWithAux {α β γ} (f : α → β → γ) (as : Array α) (bs : Array β) : Nat → Array γ → Array γ diff --git a/stage0/src/Init/Data/ByteArray/Basic.lean b/stage0/src/Init/Data/ByteArray/Basic.lean index 941c21d047..c7be7abff8 100644 --- a/stage0/src/Init/Data/ByteArray/Basic.lean +++ b/stage0/src/Init/Data/ByteArray/Basic.lean @@ -58,7 +58,7 @@ protected def append (a : ByteArray) (b : ByteArray) : ByteArray := -- we assume that `append`s may be repeated, so use asymptotic growing; use `copySlice` directly to customize b.copySlice 0 a a.size b.size false -instance : HasAppend ByteArray := ⟨ByteArray.append⟩ +instance : Append ByteArray := ⟨ByteArray.append⟩ partial def toList (bs : ByteArray) : List UInt8 := let rec loop (i : Nat) (r : List UInt8) := diff --git a/stage0/src/Init/Data/Char/Basic.lean b/stage0/src/Init/Data/Char/Basic.lean index fbcb45fdc3..f661617084 100644 --- a/stage0/src/Init/Data/Char/Basic.lean +++ b/stage0/src/Init/Data/Char/Basic.lean @@ -15,7 +15,7 @@ structure Char := (val : UInt32) (valid : isValidChar val) -instance : HasSizeof Char := ⟨fun c => c.val.toNat⟩ +instance : SizeOf Char := ⟨fun c => c.val.toNat⟩ namespace Char def utf8Size (c : Char) : UInt32 := @@ -28,8 +28,8 @@ def utf8Size (c : Char) : UInt32 := protected def Less (a b : Char) : Prop := a.val < b.val protected def LessEq (a b : Char) : Prop := a.val ≤ b.val -instance : HasLess Char := ⟨Char.Less⟩ -instance : HasLessEq Char := ⟨Char.LessEq⟩ +instance : Less Char := ⟨Char.Less⟩ +instance : LessEq Char := ⟨Char.LessEq⟩ protected def lt (a b : Char) : Bool := a.val < b.val diff --git a/stage0/src/Init/Data/Fin/Basic.lean b/stage0/src/Init/Data/Fin/Basic.lean index 0a0ae784c9..47ec2365e5 100644 --- a/stage0/src/Init/Data/Fin/Basic.lean +++ b/stage0/src/Init/Data/Fin/Basic.lean @@ -24,8 +24,8 @@ protected def lt {n} (a b : Fin n) : Prop := protected def le {n} (a b : Fin n) : Prop := a.val ≤ b.val -instance {n} : HasLess (Fin n) := ⟨Fin.lt⟩ -instance {n} : HasLessEq (Fin n) := ⟨Fin.le⟩ +instance {n} : Less (Fin n) := ⟨Fin.lt⟩ +instance {n} : LessEq (Fin n) := ⟨Fin.le⟩ instance decLt {n} (a b : Fin n) : Decidable (a < b) := Nat.decLt .. @@ -80,12 +80,12 @@ def land : Fin n → Fin n → Fin n def lor : Fin n → Fin n → Fin n | ⟨a, h⟩, ⟨b, _⟩ => ⟨(Nat.lor a b) % n, mlt h⟩ -instance : HasAdd (Fin n) := ⟨Fin.add⟩ -instance : HasSub (Fin n) := ⟨Fin.sub⟩ -instance : HasMul (Fin n) := ⟨Fin.mul⟩ -instance : HasMod (Fin n) := ⟨Fin.mod⟩ -instance : HasDiv (Fin n) := ⟨Fin.div⟩ -instance : HasModN (Fin n) := ⟨Fin.modn⟩ +instance : Add (Fin n) := ⟨Fin.add⟩ +instance : Sub (Fin n) := ⟨Fin.sub⟩ +instance : Mul (Fin n) := ⟨Fin.mul⟩ +instance : Mod (Fin n) := ⟨Fin.mod⟩ +instance : Div (Fin n) := ⟨Fin.div⟩ +instance : ModN (Fin n) := ⟨Fin.modn⟩ theorem eqOfVeq : ∀ {i j : Fin n}, (val i) = (val j) → i = j | ⟨iv, ilt₁⟩, ⟨_, _⟩, rfl => rfl diff --git a/stage0/src/Init/Data/Float.lean b/stage0/src/Init/Data/Float.lean index 60ea966a8e..0f69dd5145 100644 --- a/stage0/src/Init/Data/Float.lean +++ b/stage0/src/Init/Data/Float.lean @@ -44,17 +44,17 @@ def Float.lt : Float → Float → Prop := fun a b => def Float.le : Float → Float → Prop := fun a b => floatSpec.le a.val b.val -instance : HasOfNat Float := ⟨Float.ofNat⟩ -instance : HasAdd Float := ⟨Float.add⟩ -instance : HasSub Float := ⟨Float.sub⟩ -instance : HasMul Float := ⟨Float.mul⟩ -instance : HasDiv Float := ⟨Float.div⟩ -instance : HasLess Float := ⟨Float.lt⟩ -instance : HasLessEq Float := ⟨Float.le⟩ +instance : OfNat Float := ⟨Float.ofNat⟩ +instance : Add Float := ⟨Float.add⟩ +instance : Sub Float := ⟨Float.sub⟩ +instance : Mul Float := ⟨Float.mul⟩ +instance : Div Float := ⟨Float.div⟩ +instance : Less Float := ⟨Float.lt⟩ +instance : LessEq Float := ⟨Float.le⟩ @[extern c inline "#1 == #2"] constant Float.beq (a b : Float) : Bool -instance : HasBeq Float := ⟨Float.beq⟩ +instance : BEq Float := ⟨Float.beq⟩ @[extern c inline "#1 < #2"] constant Float.decLt (a b : Float) : Decidable (a < b) := match a, b with @@ -96,4 +96,4 @@ abbrev Nat.toFloat (n : Nat) : Float := @[extern "sqrt"] constant Float.sqrt : Float → Float @[extern "cbrt"] constant Float.cbrt : Float → Float -instance : HasPow Float Float := ⟨Float.pow⟩ +instance : Pow Float Float := ⟨Float.pow⟩ diff --git a/stage0/src/Init/Data/Int/Basic.lean b/stage0/src/Init/Data/Int/Basic.lean index a8e082eb0e..31390cae58 100644 --- a/stage0/src/Init/Data/Int/Basic.lean +++ b/stage0/src/Init/Data/Int/Basic.lean @@ -60,26 +60,26 @@ protected def mul (m n : @& Int) : Int := | 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⟩ -instance : HasMul Int := ⟨Int.mul⟩ +instance : Neg Int := ⟨Int.neg⟩ +instance : Add Int := ⟨Int.add⟩ +instance : Mul Int := ⟨Int.mul⟩ @[extern "lean_int_sub"] protected def sub (m n : @& Int) : Int := m + (- n) -instance : HasSub Int := ⟨Int.sub⟩ +instance : Sub Int := ⟨Int.sub⟩ inductive NonNeg : Int → Prop | mk (n : Nat) : NonNeg (ofNat n) protected def LessEq (a b : Int) : Prop := NonNeg (b - a) -instance : HasLessEq Int := ⟨Int.LessEq⟩ +instance : LessEq Int := ⟨Int.LessEq⟩ protected def Less (a b : Int) : Prop := (a + 1) ≤ b -instance : HasLess Int := ⟨Int.Less⟩ +instance : Less Int := ⟨Int.Less⟩ set_option bootstrap.gen_matcher_code false in @[extern "lean_int_dec_eq"] @@ -124,7 +124,7 @@ protected def repr : Int → String instance : Repr Int := ⟨Int.repr⟩ instance : ToString Int := ⟨Int.repr⟩ -instance : HasOfNat Int := ⟨Int.ofNat⟩ +instance : OfNat Int := ⟨Int.ofNat⟩ @[extern "lean_int_div"] def div : (@& Int) → (@& Int) → Int @@ -140,8 +140,8 @@ def mod : (@& Int) → (@& Int) → Int | negSucc m, ofNat n => -ofNat (succ m % n) | negSucc m, negSucc n => -ofNat (succ m % succ n) -instance : HasDiv Int := ⟨Int.div⟩ -instance : HasMod Int := ⟨Int.mod⟩ +instance : Div Int := ⟨Int.div⟩ +instance : Mod Int := ⟨Int.mod⟩ def toNat : Int → Nat | ofNat n => n diff --git a/stage0/src/Init/Data/List/Basic.lean b/stage0/src/Init/Data/List/Basic.lean index 36b7b62615..3fddf905e7 100644 --- a/stage0/src/Init/Data/List/Basic.lean +++ b/stage0/src/Init/Data/List/Basic.lean @@ -40,7 +40,7 @@ def reverse (as : List α) :List α := protected def append (as bs : List α) : List α := reverseAux as.reverse bs -instance : HasAppend (List α) := ⟨List.append⟩ +instance : Append (List α) := ⟨List.append⟩ theorem reverseAuxReverseAuxNil : ∀ (as bs : List α), reverseAux (reverseAux as bs) [] = reverseAux bs as | [], bs => rfl @@ -70,9 +70,9 @@ theorem appendAssoc : ∀ (as bs cs : List α), (as ++ bs) ++ cs = as ++ (bs ++ rw [consAppend, consAppend, appendAssoc, consAppend] exact rfl -instance : HasEmptyc (List α) := ⟨List.nil⟩ +instance : EmptyCollection (List α) := ⟨List.nil⟩ -protected def erase {α} [HasBeq α] : List α → α → List α +protected def erase {α} [BEq α] : List α → α → List α | [], b => [] | a::as, b => match a == b with | true => as @@ -156,41 +156,41 @@ def findSome? (f : α → Option β) : List α → Option β | some b => some b | none => findSome? f as -def replace [HasBeq α] : List α → α → α → List α +def replace [BEq α] : List α → α → α → List α | [], _, _ => [] | a::as, b, c => match a == b with | true => c::as | flase => a :: (replace as b c) -def elem [HasBeq α] (a : α) : List α → Bool +def elem [BEq α] (a : α) : List α → Bool | [] => false | b::bs => match a == b with | true => true | false => elem a bs -def notElem [HasBeq α] (a : α) (as : List α) : Bool := +def notElem [BEq α] (a : α) (as : List α) : Bool := !(as.elem a) -abbrev contains [HasBeq α] (as : List α) (a : α) : Bool := +abbrev contains [BEq α] (as : List α) (a : α) : Bool := elem a as -def eraseDupsAux {α} [HasBeq α] : List α → List α → List α +def eraseDupsAux {α} [BEq α] : List α → List α → List α | [], bs => bs.reverse | a::as, bs => match bs.elem a with | true => eraseDupsAux as bs | false => eraseDupsAux as (a::bs) -def eraseDups {α} [HasBeq α] (as : List α) : List α := +def eraseDups {α} [BEq α] (as : List α) : List α := eraseDupsAux as [] -def eraseRepsAux {α} [HasBeq α] : α → List α → List α → List α +def eraseRepsAux {α} [BEq α] : α → List α → List α → List α | a, [], rs => (a::rs).reverse | a, a'::as, rs => match a == a' with | true => eraseRepsAux a as rs | false => eraseRepsAux a' as (a::rs) /-- Erase repeated adjacent elements. -/ -def eraseReps {α} [HasBeq α] : List α → List α +def eraseReps {α} [BEq α] : List α → List α | [] => [] | a::as => eraseRepsAux a as [] @@ -213,13 +213,13 @@ def eraseReps {α} [HasBeq α] : List α → List α | [] => [] | a::as => groupByAux p as [[a]] -def lookup [HasBeq α] : α → List (α × β) → Option β +def lookup [BEq α] : α → List (α × β) → Option β | _, [] => none | a, (k,b)::es => match a == k with | true => some b | false => lookup a es -def removeAll [HasBeq α] (xs ys : List α) : List α := +def removeAll [BEq α] (xs ys : List α) : List α := xs.filter (fun x => ys.notElem x) def drop : Nat → List α → List α @@ -298,47 +298,47 @@ def intercalate (sep : List α) (xs : List (List α)) : List α := @[inline] protected def pure {α : Type u} (a : α) : List α := [a] -inductive Less [HasLess α] : List α → List α → Prop +inductive List.Less [Less α] : List α → List α → Prop | nil (b : α) (bs : List α) : Less [] (b::bs) | head {a : α} (as : List α) {b : α} (bs : List α) : a < b → Less (a::as) (b::bs) | tail {a : α} {as : List α} {b : α} {bs : List α} : ¬ a < b → ¬ b < a → Less as bs → Less (a::as) (b::bs) -instance less [HasLess α] : HasLess (List α) := ⟨List.Less⟩ +instance less [Less α] : Less (List α) := ⟨List.Less⟩ -instance hasDecidableLt [HasLess α] [h : DecidableRel (α:=α) (·<·)] : (l₁ l₂ : List α) → Decidable (l₁ < l₂) +instance hasDecidableLt [Less α] [h : DecidableRel (α:=α) (·<·)] : (l₁ l₂ : List α) → Decidable (l₁ < l₂) | [], [] => isFalse (fun h => nomatch h) - | [], b::bs => isTrue (Less.nil _ _) + | [], b::bs => isTrue (List.Less.nil _ _) | a::as, [] => isFalse (fun h => nomatch h) | a::as, b::bs => match h a b with - | isTrue h₁ => isTrue (Less.head _ _ h₁) + | isTrue h₁ => isTrue (List.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₂') + | List.Less.head _ _ h₁' => absurd h₁' h₁ + | List.Less.tail _ h₂' _ => absurd h₂ h₂') | isFalse h₂ => match hasDecidableLt as bs with - | isTrue h₃ => isTrue (Less.tail h₁ h₂ h₃) + | isTrue h₃ => isTrue (List.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₃) + | List.Less.head _ _ h₁' => absurd h₁' h₁ + | List.Less.tail _ _ h₃' => absurd h₃' h₃) -@[reducible] protected def LessEq [HasLess α] (a b : List α) : Prop := ¬ b < a +@[reducible] protected def LessEq [Less α] (a b : List α) : Prop := ¬ b < a -instance lessEq [HasLess α] : HasLessEq (List α) := ⟨List.LessEq⟩ +instance lessEq [Less α] : LessEq (List α) := ⟨List.LessEq⟩ -instance [HasLess α] [h : DecidableRel (HasLess.Less : α → α → Prop)] : (l₁ l₂ : List α) → Decidable (l₁ ≤ l₂) := +instance [Less α] [h : DecidableRel (Less.Less : α → α → Prop)] : (l₁ l₂ : List α) → Decidable (l₁ ≤ l₂) := fun a b => inferInstanceAs (Decidable (Not _)) /-- `isPrefixOf l₁ l₂` returns `true` Iff `l₁` is a prefix of `l₂`. -/ -def isPrefixOf [HasBeq α] : List α → List α → Bool +def isPrefixOf [BEq α] : List α → List α → Bool | [], _ => true | _, [] => false | a::as, b::bs => a == b && isPrefixOf as bs /-- `isSuffixOf l₁ l₂` returns `true` Iff `l₁` is a suffix of `l₂`. -/ -def isSuffixOf [HasBeq α] (l₁ l₂ : List α) : Bool := +def isSuffixOf [BEq α] (l₁ l₂ : List α) : Bool := isPrefixOf l₁.reverse l₂.reverse @[specialize] def isEqv : List α → List α → (α → α → Bool) → Bool @@ -346,11 +346,11 @@ def isSuffixOf [HasBeq α] (l₁ l₂ : List α) : Bool := | a::as, b::bs, eqv => eqv a b && isEqv as bs eqv | _, _, eqv => false -protected def beq [HasBeq α] : List α → List α → Bool +protected def beq [BEq α] : List α → List α → Bool | [], [] => true | a::as, b::bs => a == b && List.beq as bs | _, _ => false -instance [HasBeq α] : HasBeq (List α) := ⟨List.beq⟩ +instance [BEq α] : BEq (List α) := ⟨List.beq⟩ end List diff --git a/stage0/src/Init/Data/Nat/Basic.lean b/stage0/src/Init/Data/Nat/Basic.lean index 3d1d359d4a..7f20a81edf 100644 --- a/stage0/src/Init/Data/Nat/Basic.lean +++ b/stage0/src/Init/Data/Nat/Basic.lean @@ -53,12 +53,12 @@ def ble : Nat → Nat → Bool protected def le (n m : Nat) : Prop := ble n m = true -instance : HasLessEq Nat := ⟨Nat.le⟩ +instance : LessEq Nat := ⟨Nat.le⟩ protected def lt (n m : Nat) : Prop := Nat.le (succ n) m -instance : HasLess Nat := ⟨Nat.lt⟩ +instance : Less Nat := ⟨Nat.lt⟩ set_option bootstrap.gen_matcher_code false in @[extern c inline "lean_nat_sub(#1, lean_box(1))"] @@ -78,8 +78,8 @@ protected def mul : (@& Nat) → (@& Nat) → Nat | a, 0 => 0 | a, b+1 => (Nat.mul a b) + a -instance : HasSub Nat := ⟨Nat.sub⟩ -instance : HasMul Nat := ⟨Nat.mul⟩ +instance : Sub Nat := ⟨Nat.sub⟩ +instance : Mul Nat := ⟨Nat.mul⟩ @[specialize] def foldAux {α : Type u} (f : Nat → α → α) (s : Nat) : Nat → α → α | 0, a => a @@ -117,7 +117,7 @@ protected def pow (m : @& Nat) : (@& Nat) → Nat | 0 => 1 | succ n => Nat.pow m n * m -instance : HasPow Nat Nat := ⟨Nat.pow⟩ +instance : Pow Nat Nat := ⟨Nat.pow⟩ /- Nat.add theorems -/ @@ -444,7 +444,7 @@ theorem leAddLeft (n m : Nat): n ≤ m + n := theorem le.dest : ∀ {n m : Nat}, n ≤ m → Exists (fun k => n + k = m) | zero, zero, h => ⟨0, rfl⟩ - | zero, succ n, h => ⟨succ n, show 0 + succ n = succ n from (Nat.addComm 0 (succ n)).symm ▸ rfl⟩ + | zero, succ n, h => ⟨succ n, Nat.addComm 0 (succ n) ▸ rfl⟩ | succ n, zero, h => Bool.noConfusion h | succ n, succ m, h => have n ≤ m from h diff --git a/stage0/src/Init/Data/Nat/Div.lean b/stage0/src/Init/Data/Nat/Div.lean index 6f193a71ad..0cc37d18c3 100644 --- a/stage0/src/Init/Data/Nat/Div.lean +++ b/stage0/src/Init/Data/Nat/Div.lean @@ -18,7 +18,7 @@ private def div.F (x : Nat) (f : ∀ x₁, x₁ < x → Nat → Nat) (y : Nat) : protected def div (a b : @& Nat) : Nat := WellFounded.fix ltWf div.F a b -instance : HasDiv Nat := ⟨Nat.div⟩ +instance : Div Nat := ⟨Nat.div⟩ private theorem divDefAux (x y : Nat) : x / y = if h : 0 < y ∧ y ≤ x then (x - y) / y + 1 else 0 := congrFun (WellFounded.fixEq ltWf div.F x) y @@ -49,7 +49,7 @@ private def mod.F (x : Nat) (f : ∀ x₁, x₁ < x → Nat → Nat) (y : Nat) : protected def mod (a b : @& Nat) : Nat := WellFounded.fix ltWf mod.F a b -instance : HasMod Nat := ⟨Nat.mod⟩ +instance : Mod Nat := ⟨Nat.mod⟩ private theorem modDefAux (x y : Nat) : x % y = if h : 0 < y ∧ y ≤ x then (x - y) % y else x := congrFun (WellFounded.fixEq ltWf mod.F x) y diff --git a/stage0/src/Init/Data/Option/Basic.lean b/stage0/src/Init/Data/Option/Basic.lean index bee6df533d..43f3958c04 100644 --- a/stage0/src/Init/Data/Option/Basic.lean +++ b/stage0/src/Init/Data/Option/Basic.lean @@ -98,11 +98,11 @@ instance {α : Type u} [DecidableEq α] : DecidableEq (Option α) := fun a b => | (isTrue e) => isTrue (congrArg (@some α) e) | (isFalse n) => isFalse (fun h => Option.noConfusion h (fun e => absurd e n)) -instance {α : Type u} [HasBeq α] : HasBeq (Option α) := ⟨fun a b => +instance {α : Type u} [BEq α] : BEq (Option α) := ⟨fun a b => match a, b with | none, none => true | none, (some v₂) => false | (some v₁), none => false | (some v₁), (some v₂) => v₁ == v₂⟩ -instance {α : Type u} [HasLess α] : HasLess (Option α) := ⟨Option.lt HasLess.Less⟩ +instance {α : Type u} [Less α] : Less (Option α) := ⟨Option.lt Less.Less⟩ diff --git a/stage0/src/Init/Data/String/Basic.lean b/stage0/src/Init/Data/String/Basic.lean index 8b95f73ab9..8116dfff30 100644 --- a/stage0/src/Init/Data/String/Basic.lean +++ b/stage0/src/Init/Data/String/Basic.lean @@ -40,7 +40,7 @@ def List.asString (s : List Char) : String := ⟨s⟩ namespace String -instance : HasLess String := +instance : Less String := ⟨fun s₁ s₂ => s₁.data < s₂.data⟩ @[extern "lean_string_dec_lt"] @@ -197,9 +197,9 @@ def splitOn (s : String) (sep : String := " ") : List String := instance : Inhabited String := ⟨""⟩ -instance : HasSizeof String := ⟨String.length⟩ +instance : SizeOf String := ⟨String.length⟩ -instance : HasAppend String := ⟨String.append⟩ +instance : Append String := ⟨String.append⟩ def str : String → Char → String := push @@ -508,7 +508,7 @@ def toNat? (s : Substring) : Option Nat := def beq (ss1 ss2 : Substring) : Bool := ss1.toString == ss2.toString -instance hasBeq : HasBeq Substring := ⟨beq⟩ +instance hasBeq : BEq Substring := ⟨beq⟩ end Substring diff --git a/stage0/src/Init/Data/UInt.lean b/stage0/src/Init/Data/UInt.lean index 8c4df7730d..3afbb0379a 100644 --- a/stage0/src/Init/Data/UInt.lean +++ b/stage0/src/Init/Data/UInt.lean @@ -37,15 +37,15 @@ def UInt8.lor (a b : UInt8) : UInt8 := ⟨Fin.lor a.val b.val⟩ def UInt8.lt (a b : UInt8) : Prop := a.val < b.val def UInt8.le (a b : UInt8) : Prop := a.val ≤ b.val -instance : HasOfNat UInt8 := ⟨UInt8.ofNat⟩ -instance : HasAdd UInt8 := ⟨UInt8.add⟩ -instance : HasSub UInt8 := ⟨UInt8.sub⟩ -instance : HasMul UInt8 := ⟨UInt8.mul⟩ -instance : HasMod UInt8 := ⟨UInt8.mod⟩ -instance : HasModN UInt8 := ⟨UInt8.modn⟩ -instance : HasDiv UInt8 := ⟨UInt8.div⟩ -instance : HasLess UInt8 := ⟨UInt8.lt⟩ -instance : HasLessEq UInt8 := ⟨UInt8.le⟩ +instance : OfNat UInt8 := ⟨UInt8.ofNat⟩ +instance : Add UInt8 := ⟨UInt8.add⟩ +instance : Sub UInt8 := ⟨UInt8.sub⟩ +instance : Mul UInt8 := ⟨UInt8.mul⟩ +instance : Mod UInt8 := ⟨UInt8.mod⟩ +instance : ModN UInt8 := ⟨UInt8.modn⟩ +instance : Div UInt8 := ⟨UInt8.div⟩ +instance : Less UInt8 := ⟨UInt8.lt⟩ +instance : LessEq UInt8 := ⟨UInt8.le⟩ instance : Inhabited UInt8 := ⟨0⟩ set_option bootstrap.gen_matcher_code false in @@ -99,15 +99,15 @@ def UInt16.lt (a b : UInt16) : Prop := a.val < b.val def UInt16.le (a b : UInt16) : Prop := a.val ≤ b.val -instance : HasOfNat UInt16 := ⟨UInt16.ofNat⟩ -instance : HasAdd UInt16 := ⟨UInt16.add⟩ -instance : HasSub UInt16 := ⟨UInt16.sub⟩ -instance : HasMul UInt16 := ⟨UInt16.mul⟩ -instance : HasMod UInt16 := ⟨UInt16.mod⟩ -instance : HasModN UInt16 := ⟨UInt16.modn⟩ -instance : HasDiv UInt16 := ⟨UInt16.div⟩ -instance : HasLess UInt16 := ⟨UInt16.lt⟩ -instance : HasLessEq UInt16 := ⟨UInt16.le⟩ +instance : OfNat UInt16 := ⟨UInt16.ofNat⟩ +instance : Add UInt16 := ⟨UInt16.add⟩ +instance : Sub UInt16 := ⟨UInt16.sub⟩ +instance : Mul UInt16 := ⟨UInt16.mul⟩ +instance : Mod UInt16 := ⟨UInt16.mod⟩ +instance : ModN UInt16 := ⟨UInt16.modn⟩ +instance : Div UInt16 := ⟨UInt16.div⟩ +instance : Less UInt16 := ⟨UInt16.lt⟩ +instance : LessEq UInt16 := ⟨UInt16.le⟩ instance : Inhabited UInt16 := ⟨0⟩ set_option bootstrap.gen_matcher_code false in @@ -168,15 +168,15 @@ def UInt32.toUInt16 (a : UInt32) : UInt16 := a.toNat.toUInt16 @[extern c inline "((uint32_t)#1)"] def UInt8.toUInt32 (a : UInt8) : UInt32 := a.toNat.toUInt32 -instance : HasOfNat UInt32 := ⟨UInt32.ofNat⟩ -instance : HasAdd UInt32 := ⟨UInt32.add⟩ -instance : HasSub UInt32 := ⟨UInt32.sub⟩ -instance : HasMul UInt32 := ⟨UInt32.mul⟩ -instance : HasMod UInt32 := ⟨UInt32.mod⟩ -instance : HasModN UInt32 := ⟨UInt32.modn⟩ -instance : HasDiv UInt32 := ⟨UInt32.div⟩ -instance : HasLess UInt32 := ⟨UInt32.lt⟩ -instance : HasLessEq UInt32 := ⟨UInt32.le⟩ +instance : OfNat UInt32 := ⟨UInt32.ofNat⟩ +instance : Add UInt32 := ⟨UInt32.add⟩ +instance : Sub UInt32 := ⟨UInt32.sub⟩ +instance : Mul UInt32 := ⟨UInt32.mul⟩ +instance : Mod UInt32 := ⟨UInt32.mod⟩ +instance : ModN UInt32 := ⟨UInt32.modn⟩ +instance : Div UInt32 := ⟨UInt32.div⟩ +instance : Less UInt32 := ⟨UInt32.lt⟩ +instance : LessEq UInt32 := ⟨UInt32.le⟩ instance : Inhabited UInt32 := ⟨0⟩ set_option bootstrap.gen_matcher_code false in @@ -248,15 +248,15 @@ constant UInt64.shiftLeft (a b : UInt64) : UInt64 := (arbitrary Nat).toUInt64 @[extern c inline "#1 >> #2"] constant UInt64.shiftRight (a b : UInt64) : UInt64 := (arbitrary Nat).toUInt64 -instance : HasOfNat UInt64 := ⟨UInt64.ofNat⟩ -instance : HasAdd UInt64 := ⟨UInt64.add⟩ -instance : HasSub UInt64 := ⟨UInt64.sub⟩ -instance : HasMul UInt64 := ⟨UInt64.mul⟩ -instance : HasMod UInt64 := ⟨UInt64.mod⟩ -instance : HasModN UInt64 := ⟨UInt64.modn⟩ -instance : HasDiv UInt64 := ⟨UInt64.div⟩ -instance : HasLess UInt64 := ⟨UInt64.lt⟩ -instance : HasLessEq UInt64 := ⟨UInt64.le⟩ +instance : OfNat UInt64 := ⟨UInt64.ofNat⟩ +instance : Add UInt64 := ⟨UInt64.add⟩ +instance : Sub UInt64 := ⟨UInt64.sub⟩ +instance : Mul UInt64 := ⟨UInt64.mul⟩ +instance : Mod UInt64 := ⟨UInt64.mod⟩ +instance : ModN UInt64 := ⟨UInt64.modn⟩ +instance : Div UInt64 := ⟨UInt64.div⟩ +instance : Less UInt64 := ⟨UInt64.lt⟩ +instance : LessEq UInt64 := ⟨UInt64.le⟩ instance : Inhabited UInt64 := ⟨0⟩ @[extern c inline "(uint64_t)#1"] @@ -327,15 +327,15 @@ constant USize.shiftRight (a b : USize) : USize := (arbitrary Nat).toUSize def USize.lt (a b : USize) : Prop := a.val < b.val def USize.le (a b : USize) : Prop := a.val ≤ b.val -instance : HasOfNat USize := ⟨USize.ofNat⟩ -instance : HasAdd USize := ⟨USize.add⟩ -instance : HasSub USize := ⟨USize.sub⟩ -instance : HasMul USize := ⟨USize.mul⟩ -instance : HasMod USize := ⟨USize.mod⟩ -instance : HasModN USize := ⟨USize.modn⟩ -instance : HasDiv USize := ⟨USize.div⟩ -instance : HasLess USize := ⟨USize.lt⟩ -instance : HasLessEq USize := ⟨USize.le⟩ +instance : OfNat USize := ⟨USize.ofNat⟩ +instance : Add USize := ⟨USize.add⟩ +instance : Sub USize := ⟨USize.sub⟩ +instance : Mul USize := ⟨USize.mul⟩ +instance : Mod USize := ⟨USize.mod⟩ +instance : ModN USize := ⟨USize.modn⟩ +instance : Div USize := ⟨USize.div⟩ +instance : Less USize := ⟨USize.lt⟩ +instance : LessEq USize := ⟨USize.le⟩ instance : Inhabited USize := ⟨0⟩ set_option bootstrap.gen_matcher_code false in diff --git a/stage0/src/Init/LeanInit.lean b/stage0/src/Init/LeanInit.lean index 72e73b7bf5..29d26b5018 100644 --- a/stage0/src/Init/LeanInit.lean +++ b/stage0/src/Init/LeanInit.lean @@ -88,7 +88,7 @@ protected def beq : (@& Name) → (@& Name) → Bool | num p₁ n₁ _, num p₂ n₂ _ => n₁ == n₂ && Name.beq p₁ p₂ | _, _ => false -instance : HasBeq Name := ⟨Name.beq⟩ +instance : BEq Name := ⟨Name.beq⟩ def toStringWithSep (sep : String) : Name → String | anonymous => "[anonymous]" @@ -107,7 +107,7 @@ protected def append : Name → Name → Name | n, str p s _ => mkNameStr (Name.append n p) s | n, num p d _ => mkNameNum (Name.append n p) d -instance : HasAppend Name := ⟨Name.append⟩ +instance : Append Name := ⟨Name.append⟩ def capitalize : Name → Name | Name.str p s _ => mkNameStr p s.capitalize @@ -844,43 +844,40 @@ def find? (stx : Syntax) (p : Syntax → Bool) : Option Syntax := end Syntax /-- Reflect a runtime datum back to surface syntax (best-effort). -/ -class HasQuote (α : Type) := - (quote : α → Syntax) - -export HasQuote (quote) - class Quote (α : Type) := (quote : α → Syntax) -instance : HasQuote Syntax := ⟨id⟩ -instance : HasQuote String := ⟨mkStxStrLit⟩ -instance : HasQuote Nat := ⟨fun n => mkStxNumLit $ toString n⟩ -instance : HasQuote Substring := ⟨fun s => mkCAppStx `String.toSubstring #[quote s.toString]⟩ +export Quote (quote) + +instance : Quote Syntax := ⟨id⟩ +instance : Quote String := ⟨mkStxStrLit⟩ +instance : Quote Nat := ⟨fun n => mkStxNumLit $ toString n⟩ +instance : Quote Substring := ⟨fun s => mkCAppStx `String.toSubstring #[quote s.toString]⟩ private def quoteName : Name → Syntax | Name.anonymous => mkCIdent `Lean.Name.anonymous | Name.str n s _ => mkCAppStx `Lean.mkNameStr #[quoteName n, quote s] | Name.num n i _ => mkCAppStx `Lean.mkNameNum #[quoteName n, quote i] -instance : HasQuote Name := ⟨quoteName⟩ +instance : Quote Name := ⟨quoteName⟩ -instance {α β : Type} [HasQuote α] [HasQuote β] : HasQuote (α × β) := +instance {α β : Type} [Quote α] [Quote β] : Quote (α × β) := ⟨fun ⟨a, b⟩ => mkCAppStx `Prod.mk #[quote a, quote b]⟩ -private def quoteList {α : Type} [HasQuote α] : List α → Syntax +private def quoteList {α : Type} [Quote α] : List α → Syntax | [] => mkCIdent `List.nil | (x::xs) => mkCAppStx `List.cons #[quote x, quoteList xs] -instance {α : Type} [HasQuote α] : HasQuote (List α) := ⟨quoteList⟩ +instance {α : Type} [Quote α] : Quote (List α) := ⟨quoteList⟩ -instance {α : Type} [HasQuote α] : HasQuote (Array α) := +instance {α : Type} [Quote α] : Quote (Array α) := ⟨fun xs => mkCAppStx `List.toArray #[quote xs.toList]⟩ -private def quoteOption {α : Type} [HasQuote α] : Option α → Syntax +private def quoteOption {α : Type} [Quote α] : Option α → Syntax | none => mkIdent `Option.none | (some x) => mkCAppStx `Option.some #[quote x] -instance Option.hasQuote {α : Type} [HasQuote α] : HasQuote (Option α) := ⟨quoteOption⟩ +instance Option.hasQuote {α : Type} [Quote α] : Quote (Option α) := ⟨quoteOption⟩ end Lean diff --git a/stage0/src/Init/System/IO.lean b/stage0/src/Init/System/IO.lean index 23c5d444a3..5d66eada39 100644 --- a/stage0/src/Init/System/IO.lean +++ b/stage0/src/Init/System/IO.lean @@ -35,7 +35,7 @@ def EIO (ε : Type) : Type → Type := EStateM ε IO.RealWorld instance (ε : Type) : Monad (EIO ε) := inferInstanceAs (Monad (EStateM ε IO.RealWorld)) instance (ε : Type) : MonadFinally (EIO ε) := inferInstanceAs (MonadFinally (EStateM ε IO.RealWorld)) instance (ε : Type) : MonadExceptOf ε (EIO ε) := inferInstanceAs (MonadExceptOf ε (EStateM ε IO.RealWorld)) -instance (α ε : Type) : HasOrelse (EIO ε α) := ⟨MonadExcept.orelse⟩ +instance (α ε : Type) : OrElse (EIO ε α) := ⟨MonadExcept.orelse⟩ instance {ε : Type} {α : Type} [Inhabited ε] : Inhabited (EIO ε α) := inferInstanceAs (Inhabited (EStateM ε IO.RealWorld α)) open IO (Error) in @@ -462,28 +462,22 @@ universe u namespace Lean /-- Typeclass used for presenting the output of an `#eval` command. -/ -class HasEval (α : Type u) := - -- We default `hideUnit` to `true`, but set it to `false` in the direct call from `#eval` - -- so that `()` output is hidden in chained instances such as for some `m Unit`. - -- We take `Unit → α` instead of `α` because ‵α` may contain effectful debugging primitives (e.g., `dbgTrace!`) - (eval : (Unit → α) → forall (hideUnit : optParam Bool true), IO Unit) - class Eval (α : Type u) := -- We default `hideUnit` to `true`, but set it to `false` in the direct call from `#eval` -- so that `()` output is hidden in chained instances such as for some `m Unit`. -- We take `Unit → α` instead of `α` because ‵α` may contain effectful debugging primitives (e.g., `dbgTrace!`) (eval : (Unit → α) → forall (hideUnit : optParam Bool true), IO Unit) -instance {α : Type u} [Repr α] : HasEval α := +instance {α : Type u} [Repr α] : Eval α := ⟨fun a _ => IO.println (repr (a ()))⟩ -instance : HasEval Unit := +instance : Eval Unit := ⟨fun u hideUnit => if hideUnit then pure () else IO.println (repr (u ()))⟩ -instance {α : Type} [HasEval α] : HasEval (IO α) := - ⟨fun x _ => do let a ← x (); HasEval.eval (fun _ => a)⟩ +instance {α : Type} [Eval α] : Eval (IO α) := + ⟨fun x _ => do let a ← x (); Eval.eval (fun _ => a)⟩ -@[noinline, nospecialize] def runEval {α : Type u} [HasEval α] (a : Unit → α) : IO (String × Except IO.Error Unit) := - IO.FS.withIsolatedStreams (HasEval.eval a false) +@[noinline, nospecialize] def runEval {α : Type u} [Eval α] (a : Unit → α) : IO (String × Except IO.Error Unit) := + IO.FS.withIsolatedStreams (Eval.eval a false) end Lean diff --git a/stage0/src/Init/WF.lean b/stage0/src/Init/WF.lean index aa15be8b88..c0a55fb084 100644 --- a/stage0/src/Init/WF.lean +++ b/stage0/src/Init/WF.lean @@ -38,10 +38,6 @@ end Acc inductive WellFounded {α : Sort u} (r : α → α → Prop) : Prop | intro (h : ∀ a, Acc r a) : WellFounded r -class HasWellFounded (α : Sort u) : Type u := - (r : α → α → Prop) - (wf : WellFounded r) - class WellFoundedRelation (α : Sort u) : Type u := (r : α → α → Prop) (wf : WellFounded r) @@ -174,13 +170,13 @@ def measure {α : Sort u} : (α → Nat) → α → α → Prop := def measureWf {α : Sort u} (f : α → Nat) : WellFounded (measure f) := InvImage.wf f Nat.ltWf -def sizeofMeasure (α : Sort u) [HasSizeof α] : α → α → Prop := - measure sizeof +def sizeofMeasure (α : Sort u) [SizeOf α] : α → α → Prop := + measure sizeOf -def sizeofMeasureWf (α : Sort u) [HasSizeof α] : WellFounded (sizeofMeasure α) := - measureWf sizeof +def sizeofMeasureWf (α : Sort u) [SizeOf α] : WellFounded (sizeofMeasure α) := + measureWf sizeOf -instance hasWellFoundedOfHasSizeof (α : Sort u) [HasSizeof α] : HasWellFounded α := { +instance hasWellFoundedOfSizeOf (α : Sort u) [SizeOf α] : WellFoundedRelation α := { r := sizeofMeasure α, wf := sizeofMeasureWf α } @@ -237,7 +233,7 @@ def rprodWf (ha : WellFounded ra) (hb : WellFounded rb) : WellFounded (Rprod ra end -instance {α : Type u} {β : Type v} [s₁ : HasWellFounded α] [s₂ : HasWellFounded β] : HasWellFounded (α × β) := { +instance {α : Type u} {β : Type v} [s₁ : WellFoundedRelation α] [s₂ : WellFoundedRelation β] : WellFoundedRelation (α × β) := { r := Lex s₁.r s₂.r, wf := lexWf s₁.wf s₂.wf } @@ -329,7 +325,7 @@ def mkSkipLeft {α : Type u} {β : Type v} {b₁ b₂ : β} {s : β → β → P RevLex.right _ _ h end -instance HasWellFounded {α : Type u} {β : α → Type v} [s₁ : HasWellFounded α] [s₂ : ∀ a, HasWellFounded (β a)] : HasWellFounded (PSigma β) := { +instance WellFoundedRelation {α : Type u} {β : α → Type v} [s₁ : WellFoundedRelation α] [s₂ : ∀ a, WellFoundedRelation (β a)] : WellFoundedRelation (PSigma β) := { r := Lex s₁.r (fun a => (s₂ a).r), wf := lexWf s₁.wf (fun a => (s₂ a).wf) } diff --git a/stage0/src/Lean/Attributes.lean b/stage0/src/Lean/Attributes.lean index 4a0041e535..d43cb89a0b 100644 --- a/stage0/src/Lean/Attributes.lean +++ b/stage0/src/Lean/Attributes.lean @@ -18,7 +18,7 @@ def AttributeApplicationTime.beq : AttributeApplicationTime → AttributeApplica | AttributeApplicationTime.beforeElaboration, AttributeApplicationTime.beforeElaboration => true | _, _ => false -instance : HasBeq AttributeApplicationTime := ⟨AttributeApplicationTime.beq⟩ +instance : BEq AttributeApplicationTime := ⟨AttributeApplicationTime.beq⟩ structure Attr.Context := (currNamespace : Name) diff --git a/stage0/src/Lean/Compiler/ConstFolding.lean b/stage0/src/Lean/Compiler/ConstFolding.lean index 354d549e2c..f9e0623ac5 100644 --- a/stage0/src/Lean/Compiler/ConstFolding.lean +++ b/stage0/src/Lean/Compiler/ConstFolding.lean @@ -61,10 +61,10 @@ def foldBinUInt (fn : NumScalarTypeInfo → Bool → Nat → Nat → Nat) (befor let info ← getInfoFromVal a₁ pure $ mkUIntLit info (fn info beforeErasure n₁ n₂) -def foldUIntAdd := foldBinUInt $ fun _ _ => HasAdd.add -def foldUIntMul := foldBinUInt $ fun _ _ => HasMul.mul -def foldUIntDiv := foldBinUInt $ fun _ _ => HasDiv.div -def foldUIntMod := foldBinUInt $ fun _ _ => HasMod.mod +def foldUIntAdd := foldBinUInt $ fun _ _ => Add.add +def foldUIntMul := foldBinUInt $ fun _ _ => Mul.mul +def foldUIntDiv := foldBinUInt $ fun _ _ => Div.div +def foldUIntMod := foldBinUInt $ fun _ _ => Mod.mod def foldUIntSub := foldBinUInt $ fun info _ a b => (a + (info.size - b)) def preUIntBinFoldFns : List (Name × BinFoldFn) := @@ -79,10 +79,10 @@ def foldNatBinOp (fn : Nat → Nat → Nat) (a₁ a₂ : Expr) : Option Expr := let n₂ ← getNumLit a₂ pure $ mkNatLit (fn n₁ n₂) -def foldNatAdd (_ : Bool) := foldNatBinOp HasAdd.add -def foldNatMul (_ : Bool) := foldNatBinOp HasMul.mul -def foldNatDiv (_ : Bool) := foldNatBinOp HasDiv.div -def foldNatMod (_ : Bool) := foldNatBinOp HasMod.mod +def foldNatAdd (_ : Bool) := foldNatBinOp Add.add +def foldNatMul (_ : Bool) := foldNatBinOp Mul.mul +def foldNatDiv (_ : Bool) := foldNatBinOp Div.div +def foldNatMod (_ : Bool) := foldNatBinOp Mod.mod -- TODO: add option for controlling the limit def natPowThreshold := 256 diff --git a/stage0/src/Lean/Compiler/ExternAttr.lean b/stage0/src/Lean/Compiler/ExternAttr.lean index 3f857e5443..81d9b554da 100644 --- a/stage0/src/Lean/Compiler/ExternAttr.lean +++ b/stage0/src/Lean/Compiler/ExternAttr.lean @@ -122,7 +122,7 @@ def expandExternPattern (pattern : String) (args : List String) : String := expandExternPatternAux args pattern.length pattern.mkIterator "" def mkSimpleFnCall (fn : String) (args : List String) : String := - fn ++ "(" ++ ((args.intersperse ", ").foldl HasAppend.append "") ++ ")" + fn ++ "(" ++ ((args.intersperse ", ").foldl Append.append "") ++ ")" def ExternEntry.backend : ExternEntry → Name | ExternEntry.adhoc n => n diff --git a/stage0/src/Lean/Compiler/IR/Basic.lean b/stage0/src/Lean/Compiler/IR/Basic.lean index 13a7c57fd9..031e4ed594 100644 --- a/stage0/src/Lean/Compiler/IR/Basic.lean +++ b/stage0/src/Lean/Compiler/IR/Basic.lean @@ -27,12 +27,12 @@ structure JoinPointId := (idx : Index) abbrev Index.lt (a b : Index) : Bool := a < b -instance : HasBeq VarId := ⟨fun a b => a.idx == b.idx⟩ +instance : BEq VarId := ⟨fun a b => a.idx == b.idx⟩ instance : ToString VarId := ⟨fun a => "x_" ++ toString a.idx⟩ instance : ToFormat VarId := ⟨fun a => toString a⟩ instance : Hashable VarId := ⟨fun a => hash a.idx⟩ -instance : HasBeq JoinPointId := ⟨fun a b => a.idx == b.idx⟩ +instance : BEq JoinPointId := ⟨fun a b => a.idx == b.idx⟩ instance : ToString JoinPointId := ⟨fun a => "block_" ++ toString a.idx⟩ instance : ToFormat JoinPointId := ⟨fun a => toString a⟩ instance : Hashable JoinPointId := ⟨fun a => hash a.idx⟩ @@ -94,7 +94,7 @@ partial def beq : IRType → IRType → Bool | union n₁ tys₁, union n₂ tys₂ => n₁ == n₂ && Array.isEqv tys₁ tys₂ beq | _, _ => false -instance : HasBeq IRType := ⟨beq⟩ +instance : BEq IRType := ⟨beq⟩ def isScalar : IRType → Bool | float => true @@ -137,7 +137,7 @@ protected def Arg.beq : Arg → Arg → Bool | irrelevant, irrelevant => true | _, _ => false -instance : HasBeq Arg := ⟨Arg.beq⟩ +instance : BEq Arg := ⟨Arg.beq⟩ instance : Inhabited Arg := ⟨Arg.irrelevant⟩ @[export lean_ir_mk_var_arg] def mkVarArg (id : VarId) : Arg := Arg.var id @@ -151,7 +151,7 @@ def LitVal.beq : LitVal → LitVal → Bool | str v₁, str v₂ => v₁ == v₂ | _, _ => false -instance : HasBeq LitVal := ⟨LitVal.beq⟩ +instance : BEq LitVal := ⟨LitVal.beq⟩ /- Constructor information. @@ -175,7 +175,7 @@ def CtorInfo.beq : CtorInfo → CtorInfo → Bool | ⟨n₁, cidx₁, size₁, usize₁, ssize₁⟩, ⟨n₂, cidx₂, size₂, usize₂, ssize₂⟩ => n₁ == n₂ && cidx₁ == cidx₂ && size₁ == size₂ && usize₁ == usize₂ && ssize₁ == ssize₂ -instance : HasBeq CtorInfo := ⟨CtorInfo.beq⟩ +instance : BEq CtorInfo := ⟨CtorInfo.beq⟩ def CtorInfo.isRef (info : CtorInfo) : Bool := info.size > 0 || info.usize > 0 || info.ssize > 0 @@ -491,32 +491,29 @@ def LocalContext.getValue (ctx : LocalContext) (x : VarId) : Option Expr := abbrev IndexRenaming := RBMap Index Index Index.lt -class HasAlphaEqv (α : Type) := - (aeqv : IndexRenaming → α → α → Bool) - class AlphaEqv (α : Type) := (aeqv : IndexRenaming → α → α → Bool) -export HasAlphaEqv (aeqv) +export AlphaEqv (aeqv) def VarId.alphaEqv (ρ : IndexRenaming) (v₁ v₂ : VarId) : Bool := match ρ.find? v₁.idx with | some v => v == v₂.idx | none => v₁ == v₂ -instance : HasAlphaEqv VarId := ⟨VarId.alphaEqv⟩ +instance : AlphaEqv VarId := ⟨VarId.alphaEqv⟩ def Arg.alphaEqv (ρ : IndexRenaming) : Arg → Arg → Bool | Arg.var v₁, Arg.var v₂ => aeqv ρ v₁ v₂ | Arg.irrelevant, Arg.irrelevant => true | _, _ => false -instance : HasAlphaEqv Arg := ⟨Arg.alphaEqv⟩ +instance : AlphaEqv Arg := ⟨Arg.alphaEqv⟩ def args.alphaEqv (ρ : IndexRenaming) (args₁ args₂ : Array Arg) : Bool := Array.isEqv args₁ args₂ (fun a b => aeqv ρ a b) -instance: HasAlphaEqv (Array Arg) := ⟨args.alphaEqv⟩ +instance: AlphaEqv (Array Arg) := ⟨args.alphaEqv⟩ def Expr.alphaEqv (ρ : IndexRenaming) : Expr → Expr → Bool | Expr.ctor i₁ ys₁, Expr.ctor i₂ ys₂ => i₁ == i₂ && aeqv ρ ys₁ ys₂ @@ -535,7 +532,7 @@ def Expr.alphaEqv (ρ : IndexRenaming) : Expr → Expr → Bool | Expr.isTaggedPtr x₁, Expr.isTaggedPtr x₂ => aeqv ρ x₁ x₂ | _, _ => false -instance : HasAlphaEqv Expr:= ⟨Expr.alphaEqv⟩ +instance : AlphaEqv Expr:= ⟨Expr.alphaEqv⟩ def addVarRename (ρ : IndexRenaming) (x₁ x₂ : Nat) := if x₁ == x₂ then ρ else ρ.insert x₁ x₂ @@ -575,7 +572,7 @@ partial def FnBody.alphaEqv : IndexRenaming → FnBody → FnBody → Bool def FnBody.beq (b₁ b₂ : FnBody) : Bool := FnBody.alphaEqv ∅ b₁ b₂ -instance : HasBeq FnBody := ⟨FnBody.beq⟩ +instance : BEq FnBody := ⟨FnBody.beq⟩ abbrev VarIdSet := RBTree VarId (fun x y => x.idx < y.idx) instance : Inhabited VarIdSet := ⟨{}⟩ diff --git a/stage0/src/Lean/Compiler/IR/Borrow.lean b/stage0/src/Lean/Compiler/IR/Borrow.lean index 5beea44202..b229ecd0c2 100644 --- a/stage0/src/Lean/Compiler/IR/Borrow.lean +++ b/stage0/src/Lean/Compiler/IR/Borrow.lean @@ -16,7 +16,7 @@ abbrev Key := FunId × Index def beq : Key → Key → Bool | (f₁, x₁), (f₂, x₂) => f₁ == f₂ && x₁ == x₂ -instance : HasBeq Key := ⟨beq⟩ +instance : BEq Key := ⟨beq⟩ def getHash : Key → USize | (f, x) => mixHash (hash f) (hash x) @@ -43,7 +43,7 @@ def beq : Key → Key → Bool | Key.jp n₁ id₁, Key.jp n₂ id₂ => n₁ == n₂ && id₁ == id₂ | _, _ => false -instance : HasBeq Key := ⟨beq⟩ +instance : BEq Key := ⟨beq⟩ def getHash : Key → USize | Key.decl n => hash n diff --git a/stage0/src/Lean/Compiler/IR/ElimDeadBranches.lean b/stage0/src/Lean/Compiler/IR/ElimDeadBranches.lean index c97f527864..640c153915 100644 --- a/stage0/src/Lean/Compiler/IR/ElimDeadBranches.lean +++ b/stage0/src/Lean/Compiler/IR/ElimDeadBranches.lean @@ -30,7 +30,7 @@ protected partial def beq : Value → Value → Bool vs₂.all (fun v₂ => vs₁.any fun v₁ => Value.beq v₁ v₂) | _, _ => false -instance : HasBeq Value := ⟨Value.beq⟩ +instance : BEq Value := ⟨Value.beq⟩ partial def addChoice (merge : Value → Value → Value) : List Value → Value → List Value | [], v => [v] diff --git a/stage0/src/Lean/Compiler/IR/FreeVars.lean b/stage0/src/Lean/Compiler/IR/FreeVars.lean index 84658dfcf8..4b5eeb11d3 100644 --- a/stage0/src/Lean/Compiler/IR/FreeVars.lean +++ b/stage0/src/Lean/Compiler/IR/FreeVars.lean @@ -23,7 +23,7 @@ abbrev Collector := Index → Index @[inline] private def collectVar (x : VarId) : Collector := collect x.idx @[inline] private def collectJP (j : JoinPointId) : Collector := collect j.idx @[inline] private def seq (k₁ k₂ : Collector) : Collector := k₂ ∘ k₁ -instance : HasAndthen Collector := ⟨seq⟩ +instance : AndThen Collector := ⟨seq⟩ private def collectArg : Arg → Collector | Arg.var x => collectVar x @@ -119,7 +119,7 @@ fun k bv fv => k (insertParams bv ys) fv @[inline] private def seq : Collector → Collector → Collector := fun k₁ k₂ bv fv => k₂ bv (k₁ bv fv) -instance : HasAndthen Collector := ⟨seq⟩ +instance : AndThen Collector := ⟨seq⟩ private def collectArg : Arg → Collector | Arg.var x => collectVar x diff --git a/stage0/src/Lean/Compiler/InlineAttrs.lean b/stage0/src/Lean/Compiler/InlineAttrs.lean index 0eb0eb28e0..73015a245e 100644 --- a/stage0/src/Lean/Compiler/InlineAttrs.lean +++ b/stage0/src/Lean/Compiler/InlineAttrs.lean @@ -22,7 +22,7 @@ protected def beq : InlineAttributeKind → InlineAttributeKind → Bool | inlineIfReduce, inlineIfReduce => true | _, _ => false -instance : HasBeq InlineAttributeKind := ⟨InlineAttributeKind.beq⟩ +instance : BEq InlineAttributeKind := ⟨InlineAttributeKind.beq⟩ end InlineAttributeKind diff --git a/stage0/src/Lean/Compiler/Specialize.lean b/stage0/src/Lean/Compiler/Specialize.lean index 32cce2fd49..c649110e16 100644 --- a/stage0/src/Lean/Compiler/Specialize.lean +++ b/stage0/src/Lean/Compiler/Specialize.lean @@ -20,7 +20,7 @@ protected def beq : SpecializeAttributeKind → SpecializeAttributeKind → Bool | nospecialize, nospecialize => true | _, _ => false -instance : HasBeq SpecializeAttributeKind := ⟨SpecializeAttributeKind.beq⟩ +instance : BEq SpecializeAttributeKind := ⟨SpecializeAttributeKind.beq⟩ end SpecializeAttributeKind diff --git a/stage0/src/Lean/Compiler/Util.lean b/stage0/src/Lean/Compiler/Util.lean index be76565c66..cc675ffeba 100644 --- a/stage0/src/Lean/Compiler/Util.lean +++ b/stage0/src/Lean/Compiler/Util.lean @@ -25,7 +25,7 @@ def Visitor := AtMostOnceData → AtMostOnceData | ⟨found, false⟩ => ⟨found, false⟩ | other => g other -instance : HasAndthen Visitor := ⟨seq⟩ +instance : AndThen Visitor := ⟨seq⟩ @[inline] def skip : Visitor := id diff --git a/stage0/src/Lean/CoreM.lean b/stage0/src/Lean/CoreM.lean index eeb5895eb1..eecf595b5b 100644 --- a/stage0/src/Lean/CoreM.lean +++ b/stage0/src/Lean/CoreM.lean @@ -93,11 +93,11 @@ def mkFreshUserName {m} [MonadLiftT CoreM m] (n : Name) : m Name := | Except.error (Exception.internal id) => throw $ IO.userError $ "internal exception #" ++ toString id.idx | Except.ok a => pure a -instance {α} [MetaHasEval α] : MetaHasEval (CoreM α) := { +instance {α} [MetaEval α] : MetaEval (CoreM α) := { eval := fun env opts x _ => do let x : CoreM α := do try x finally printTraces let (a, s) ← x.toIO { maxRecDepth := getMaxRecDepth opts, options := opts } { env := env } - MetaHasEval.eval s.env opts a (hideUnit := true) + MetaEval.eval s.env opts a (hideUnit := true) } end Core diff --git a/stage0/src/Lean/Data/Format.lean b/stage0/src/Lean/Data/Format.lean index db517c4dbd..e9eb24d841 100644 --- a/stage0/src/Lean/Data/Format.lean +++ b/stage0/src/Lean/Data/Format.lean @@ -14,7 +14,7 @@ inductive FlattenBehavior | fill namespace FlattenBehavior -instance : HasBeq FlattenBehavior := ⟨fun b₁ b₂ => +instance : BEq FlattenBehavior := ⟨fun b₁ b₂ => match b₁, b₂ with | allOrNone, allOrNone => true | fill, fill => true @@ -45,12 +45,12 @@ protected def appendEx (a b : Format) : Format := protected def groupEx : Format → Format := group -instance : HasAppend Format := ⟨Format.append⟩ +instance : Append Format := ⟨Format.append⟩ instance : Coe String Format := ⟨text⟩ instance : Inhabited Format := ⟨nil⟩ def join (xs : List Format) : Format := - xs.foldl HasAppend.append "" + xs.foldl Append.append "" def isNil : Format → Bool | nil => true diff --git a/stage0/src/Lean/Data/Json/FromToJson.lean b/stage0/src/Lean/Data/Json/FromToJson.lean index 74621fb3da..798d15a331 100644 --- a/stage0/src/Lean/Data/Json/FromToJson.lean +++ b/stage0/src/Lean/Data/Json/FromToJson.lean @@ -10,63 +10,57 @@ namespace Lean universes u -class HasFromJson (α : Type u) := - (fromJson? : Json → Option α) - class FromJson (α : Type u) := (fromJson? : Json → Option α) -export HasFromJson (fromJson?) +export FromJson (fromJson?) class ToJson (α : Type u) := (toJson : α → Json) -class HasToJson (α : Type u) := - (toJson : α → Json) +export ToJson (toJson) -export HasToJson (toJson) +instance : FromJson Json := ⟨some⟩ +instance : ToJson Json := ⟨id⟩ -instance : HasFromJson Json := ⟨some⟩ -instance : HasToJson Json := ⟨id⟩ - -instance : HasFromJson JsonNumber := ⟨Json.getNum?⟩ -instance : HasToJson JsonNumber := ⟨Json.num⟩ +instance : FromJson JsonNumber := ⟨Json.getNum?⟩ +instance : ToJson JsonNumber := ⟨Json.num⟩ -- looks like id, but there are coercions happening -instance : HasFromJson Bool := ⟨Json.getBool?⟩ -instance : HasToJson Bool := ⟨fun b => b⟩ -instance : HasFromJson Nat := ⟨Json.getNat?⟩ -instance : HasToJson Nat := ⟨fun n => n⟩ -instance : HasFromJson Int := ⟨Json.getInt?⟩ -instance : HasToJson Int := ⟨fun n => Json.num n⟩ -instance : HasFromJson String := ⟨Json.getStr?⟩ -instance : HasToJson String := ⟨fun s => s⟩ +instance : FromJson Bool := ⟨Json.getBool?⟩ +instance : ToJson Bool := ⟨fun b => b⟩ +instance : FromJson Nat := ⟨Json.getNat?⟩ +instance : ToJson Nat := ⟨fun n => n⟩ +instance : FromJson Int := ⟨Json.getInt?⟩ +instance : ToJson Int := ⟨fun n => Json.num n⟩ +instance : FromJson String := ⟨Json.getStr?⟩ +instance : ToJson String := ⟨fun s => s⟩ -instance {α : Type u} [HasFromJson α] : HasFromJson (Array α) := ⟨fun j => +instance {α : Type u} [FromJson α] : FromJson (Array α) := ⟨fun j => match j with | Json.arr a => a.mapM fromJson? | _ => none⟩ -instance {α : Type u} [HasToJson α] : HasToJson (Array α) := +instance {α : Type u} [ToJson α] : ToJson (Array α) := ⟨fun a => Json.arr (a.map toJson)⟩ namespace Json -instance : HasFromJson Structured := ⟨fun j => +instance : FromJson Structured := ⟨fun j => match j with | arr a => Structured.arr a | obj o => Structured.obj o | _ => none⟩ -instance : HasToJson Structured := ⟨fun s => +instance : ToJson Structured := ⟨fun s => match s with | Structured.arr a => arr a | Structured.obj o => obj o⟩ -def getObjValAs? (j : Json) (α : Type u) [HasFromJson α] (k : String) : Option α := +def getObjValAs? (j : Json) (α : Type u) [FromJson α] (k : String) : Option α := (j.getObjVal? k).bind fromJson? -def opt {α : Type u} [HasToJson α] (k : String) : Option α → List (String × Json) +def opt {α : Type u} [ToJson α] (k : String) : Option α → List (String × Json) | some o => [⟨k, toJson o⟩] | none => [] diff --git a/stage0/src/Lean/Data/JsonRpc.lean b/stage0/src/Lean/Data/JsonRpc.lean index e83cad59bb..45b61ea434 100644 --- a/stage0/src/Lean/Data/JsonRpc.lean +++ b/stage0/src/Lean/Data/JsonRpc.lean @@ -38,7 +38,7 @@ inductive ErrorCode | requestCancelled | contentModified -instance : HasFromJson ErrorCode := ⟨fun j => +instance : FromJson ErrorCode := ⟨fun j => match j with | num (-32700 : Int) => ErrorCode.parseError | num (-32600 : Int) => ErrorCode.invalidRequest @@ -53,7 +53,7 @@ instance : HasFromJson ErrorCode := ⟨fun j => | num (-32801 : Int) => ErrorCode.contentModified | _ => none⟩ -instance : HasToJson ErrorCode := ⟨fun e => +instance : ToJson ErrorCode := ⟨fun e => match e with | ErrorCode.parseError => (-32700 : Int) | ErrorCode.invalidRequest => (-32600 : Int) @@ -85,19 +85,19 @@ structure Error := (id : RequestID) (code : JsonNumber) (message : String) (data instance : Coe String RequestID := ⟨RequestID.str⟩ instance : Coe JsonNumber RequestID := ⟨RequestID.num⟩ -instance : HasFromJson RequestID := ⟨fun j => +instance : FromJson RequestID := ⟨fun j => match j with | str s => RequestID.str s | num n => RequestID.num n | _ => none⟩ -instance : HasToJson RequestID := ⟨fun rid => +instance : ToJson RequestID := ⟨fun rid => match rid with | RequestID.str s => s | RequestID.num n => num n | RequestID.null => null⟩ -instance : HasToJson Message := ⟨fun m => +instance : ToJson Message := ⟨fun m => mkObj $ ⟨"jsonrpc", "2.0"⟩ :: match m with | Message.request id method params? => [ ⟨"id", toJson id⟩, @@ -143,7 +143,7 @@ def aux4 (j : Json) : Option Message := do -- HACK: The implementation must be made up of several `auxN`s instead -- of one large block because of a bug in the compiler. -instance : HasFromJson Message := ⟨fun j => do +instance : FromJson Message := ⟨fun j => do let "2.0" ← j.getObjVal? "jsonrpc" | none aux1 j <|> aux2 j <|> aux3 j <|> aux4 j⟩ @@ -162,7 +162,7 @@ def readMessage (h : FS.Stream) (nBytes : Nat) : IO Message := do | some m => pure m | none => throw (userError ("JSON '" ++ j.compress ++ "' did not have the format of a JSON-RPC message")) -def readRequestAs (h : FS.Stream) (nBytes : Nat) (expectedMethod : String) (α : Type) [HasFromJson α] : IO (Request α) := do +def readRequestAs (h : FS.Stream) (nBytes : Nat) (expectedMethod : String) (α : Type) [FromJson α] : IO (Request α) := do let m ← h.readMessage nBytes match m with | Message.request id method params? => @@ -178,7 +178,7 @@ def readRequestAs (h : FS.Stream) (nBytes : Nat) (expectedMethod : String) (α : throw (userError ("expected method '" ++ expectedMethod ++ "', got method '" ++ method ++ "'")) | _ => throw (userError "expected request, got other type of message") -def readNotificationAs (h : FS.Stream) (nBytes : Nat) (expectedMethod : String) (α : Type) [HasFromJson α] : IO α := do +def readNotificationAs (h : FS.Stream) (nBytes : Nat) (expectedMethod : String) (α : Type) [FromJson α] : IO α := do let m ← h.readMessage nBytes match m with | Message.notification method params? => @@ -197,7 +197,7 @@ def readNotificationAs (h : FS.Stream) (nBytes : Nat) (expectedMethod : String) def writeMessage (h : FS.Stream) (m : Message) : IO Unit := h.writeJson (toJson m) -def writeResponse {α} [HasToJson α] (h : FS.Stream) (id : RequestID) (r : α) : IO Unit := +def writeResponse {α} [ToJson α] (h : FS.Stream) (id : RequestID) (r : α) : IO Unit := h.writeMessage (Message.response id (toJson r)) end IO.FS.Stream diff --git a/stage0/src/Lean/Data/KVMap.lean b/stage0/src/Lean/Data/KVMap.lean index b904b7af78..dc1b820a63 100644 --- a/stage0/src/Lean/Data/KVMap.lean +++ b/stage0/src/Lean/Data/KVMap.lean @@ -33,7 +33,7 @@ def DataValue.sameCtor : DataValue → DataValue → Bool | DataValue.ofInt _, DataValue.ofInt _ => true | _, _ => false -instance : HasBeq DataValue := ⟨DataValue.beq⟩ +instance : BEq DataValue := ⟨DataValue.beq⟩ @[export lean_data_value_to_string] def DataValue.str : DataValue → String @@ -143,7 +143,7 @@ def subset : KVMap → KVMap → Bool def eqv (m₁ m₂ : KVMap) : Bool := subset m₁ m₂ && subset m₂ m₁ -instance : HasBeq KVMap := ⟨eqv⟩ +instance : BEq KVMap := ⟨eqv⟩ class KVMapVal (α : Type) := (defVal : α) diff --git a/stage0/src/Lean/Data/LBool.lean b/stage0/src/Lean/Data/LBool.lean index 1aae19673c..68496d9602 100644 --- a/stage0/src/Lean/Data/LBool.lean +++ b/stage0/src/Lean/Data/LBool.lean @@ -30,7 +30,7 @@ def beq : LBool → LBool → Bool | undef, undef => Bool.true | _, _ => Bool.false -instance : HasBeq LBool := ⟨beq⟩ +instance : BEq LBool := ⟨beq⟩ def toString : LBool → String | true => "true" diff --git a/stage0/src/Lean/Data/LOption.lean b/stage0/src/Lean/Data/LOption.lean index c5e4e5f988..e5fd2df3ba 100644 --- a/stage0/src/Lean/Data/LOption.lean +++ b/stage0/src/Lean/Data/LOption.lean @@ -20,13 +20,13 @@ instance : Inhabited (LOption α) := ⟨none⟩ instance [ToString α] : ToString (LOption α) := ⟨fun o => match o with | none => "none" | undef => "undef" | (some a) => "(some " ++ toString a ++ ")"⟩ -def beq [HasBeq α] : LOption α → LOption α → Bool +def beq [BEq α] : LOption α → LOption α → Bool | none, none => true | undef, undef => true | some a, some b => a == b | _, _ => false -instance [HasBeq α] : HasBeq (LOption α) := ⟨beq⟩ +instance [BEq α] : BEq (LOption α) := ⟨beq⟩ end LOption end Lean diff --git a/stage0/src/Lean/Data/Lsp/Basic.lean b/stage0/src/Lean/Data/Lsp/Basic.lean index cd68a6ddfe..2a704ee99d 100644 --- a/stage0/src/Lean/Data/Lsp/Basic.lean +++ b/stage0/src/Lean/Data/Lsp/Basic.lean @@ -27,12 +27,12 @@ structure Position := (line : Nat) (character : Nat) instance : Inhabited Position := ⟨⟨0, 0⟩⟩ -instance : HasFromJson Position := ⟨fun j => do +instance : FromJson Position := ⟨fun j => do let line ← j.getObjValAs? Nat "line" let character ← j.getObjValAs? Nat "character" pure ⟨line, character⟩⟩ -instance : HasToJson Position := ⟨fun o => +instance : ToJson Position := ⟨fun o => mkObj [ ⟨"line", o.line⟩, ⟨"character", o.character⟩]⟩ @@ -42,24 +42,24 @@ instance : ToString Position := ⟨fun p => structure Range := (start : Position) («end» : Position) -instance : HasFromJson Range := ⟨fun j => do +instance : FromJson Range := ⟨fun j => do let start ← j.getObjValAs? Position "start" let «end» ← j.getObjValAs? Position "end" pure ⟨start, «end»⟩⟩ -instance : HasToJson Range := ⟨fun o => +instance : ToJson Range := ⟨fun o => mkObj [ ⟨"start", toJson o.start⟩, ⟨"end", toJson o.«end»⟩]⟩ structure Location := (uri : DocumentUri) (range : Range) -instance : HasFromJson Location := ⟨fun j => do +instance : FromJson Location := ⟨fun j => do let uri ← j.getObjValAs? DocumentUri "uri" let range ← j.getObjValAs? Range "range" pure ⟨uri, range⟩⟩ -instance : HasToJson Location := ⟨fun o => +instance : ToJson Location := ⟨fun o => mkObj [ ⟨"uri", toJson o.uri⟩, ⟨"range", toJson o.range⟩]⟩ @@ -70,14 +70,14 @@ structure LocationLink := (targetRange : Range) (targetSelectionRange : Range) -instance : HasFromJson LocationLink := ⟨fun j => do +instance : FromJson LocationLink := ⟨fun j => do let originSelectionRange? := j.getObjValAs? Range "originSelectionRange" let targetUri ← j.getObjValAs? DocumentUri "targetUri" let targetRange ← j.getObjValAs? Range "targetRange" let targetSelectionRange ← j.getObjValAs? Range "targetSelectionRange" pure ⟨originSelectionRange?, targetUri, targetRange, targetSelectionRange⟩⟩ -instance : HasToJson LocationLink := ⟨fun o => mkObj $ +instance : ToJson LocationLink := ⟨fun o => mkObj $ opt "originSelectionRange" o.originSelectionRange? ++ [ ⟨"targetUri", toJson o.targetUri⟩, ⟨"targetRange", toJson o.targetRange⟩, @@ -92,13 +92,13 @@ structure Command := (command : String) (arguments? : Option (Array Json) := none) -instance : HasFromJson Command := ⟨fun j => do +instance : FromJson Command := ⟨fun j => do let title ← j.getObjValAs? String "title" let command ← j.getObjValAs? String "command" let arguments? := j.getObjValAs? (Array Json) "arguments" pure ⟨title, command, arguments?⟩⟩ -instance : HasToJson Command := ⟨fun o => mkObj $ +instance : ToJson Command := ⟨fun o => mkObj $ opt "arguments" o.arguments? ++ [ ⟨"title", o.title⟩, ⟨"command", o.command⟩]⟩ @@ -107,42 +107,42 @@ structure TextEdit := (range : Range) (newText : String) -instance : HasFromJson TextEdit := ⟨fun j => do +instance : FromJson TextEdit := ⟨fun j => do let range ← j.getObjValAs? Range "range" let newText ← j.getObjValAs? String "newText" pure ⟨range, newText⟩⟩ -instance : HasToJson TextEdit := ⟨fun o => +instance : ToJson TextEdit := ⟨fun o => mkObj [ ⟨"range", toJson o.range⟩, ⟨"newText", o.newText⟩]⟩ def TextEditBatch := Array TextEdit -instance : HasFromJson TextEditBatch := +instance : FromJson TextEditBatch := ⟨@fromJson? (Array TextEdit) _⟩ -instance : HasToJson TextEditBatch := +instance : ToJson TextEditBatch := ⟨@toJson (Array TextEdit) _⟩ structure TextDocumentIdentifier := (uri : DocumentUri) -instance : HasFromJson TextDocumentIdentifier := ⟨fun j => +instance : FromJson TextDocumentIdentifier := ⟨fun j => TextDocumentIdentifier.mk <$> j.getObjValAs? DocumentUri "uri"⟩ -instance : HasToJson TextDocumentIdentifier := +instance : ToJson TextDocumentIdentifier := ⟨fun o => mkObj [⟨"uri", o.uri⟩]⟩ structure VersionedTextDocumentIdentifier := (uri : DocumentUri) (version? : Option Nat := none) -instance : HasFromJson VersionedTextDocumentIdentifier := ⟨fun j => do +instance : FromJson VersionedTextDocumentIdentifier := ⟨fun j => do let uri ← j.getObjValAs? DocumentUri "uri" let version? := j.getObjValAs? Nat "version" pure ⟨uri, version?⟩⟩ -instance : HasToJson VersionedTextDocumentIdentifier := ⟨fun o => mkObj $ +instance : ToJson VersionedTextDocumentIdentifier := ⟨fun o => mkObj $ opt "version" o.version? ++ [⟨"uri", o.uri⟩]⟩ @@ -150,12 +150,12 @@ structure TextDocumentEdit := (textDocument : VersionedTextDocumentIdentifier) (edits : TextEditBatch) -instance : HasFromJson TextDocumentEdit := ⟨fun j => do +instance : FromJson TextDocumentEdit := ⟨fun j => do let textDocument ← j.getObjValAs? VersionedTextDocumentIdentifier "textDocument" let edits ← j.getObjValAs? TextEditBatch "edits" pure ⟨textDocument, edits⟩⟩ -instance : HasToJson TextDocumentEdit := ⟨fun o => +instance : ToJson TextDocumentEdit := ⟨fun o => mkObj [ ⟨"textDocument", toJson o.textDocument⟩, ⟨"edits", toJson o.edits⟩]⟩ @@ -171,14 +171,14 @@ structure TextDocumentItem := (version : Nat) (text : String) -instance : HasFromJson TextDocumentItem := ⟨fun j => do +instance : FromJson TextDocumentItem := ⟨fun j => do let uri ← j.getObjValAs? DocumentUri "uri" let languageId ← j.getObjValAs? String "languageId" let version ← j.getObjValAs? Nat "version" let text ← j.getObjValAs? String "text" pure ⟨uri, languageId, version, text⟩⟩ -instance : HasToJson TextDocumentItem := ⟨fun o => +instance : ToJson TextDocumentItem := ⟨fun o => mkObj [ ⟨"uri", o.uri⟩, ⟨"languageId", o.languageId⟩, @@ -189,12 +189,12 @@ structure TextDocumentPositionParams := (textDocument : TextDocumentIdentifier) (position : Position) -instance : HasFromJson TextDocumentPositionParams := ⟨fun j => do +instance : FromJson TextDocumentPositionParams := ⟨fun j => do let textDocument ← j.getObjValAs? TextDocumentIdentifier "textDocument" let position ← j.getObjValAs? Position "position" pure ⟨textDocument, position⟩⟩ -instance : HasToJson TextDocumentPositionParams := ⟨fun o => +instance : ToJson TextDocumentPositionParams := ⟨fun o => mkObj [ ⟨"textDocument", toJson o.textDocument⟩, ⟨"position", toJson o.position⟩]⟩ @@ -204,62 +204,62 @@ structure DocumentFilter := (scheme? : Option String := none) (pattern? : Option String := none) -instance : HasFromJson DocumentFilter := ⟨fun j => do +instance : FromJson DocumentFilter := ⟨fun j => do let language? := j.getObjValAs? String "language" let scheme? := j.getObjValAs? String "scheme" let pattern? := j.getObjValAs? String "pattern" pure ⟨language?, scheme?, pattern?⟩⟩ -instance : HasToJson DocumentFilter := ⟨fun o => mkObj $ +instance : ToJson DocumentFilter := ⟨fun o => mkObj $ opt "language" o.language? ++ opt "scheme" o.scheme? ++ opt "pattern" o.pattern?⟩ def DocumentSelector := Array DocumentFilter -instance : HasFromJson DocumentSelector := +instance : FromJson DocumentSelector := ⟨@fromJson? (Array DocumentFilter) _⟩ -instance : HasToJson DocumentSelector := +instance : ToJson DocumentSelector := ⟨@toJson (Array DocumentFilter) _⟩ structure StaticRegistrationOptions := (id? : Option String := none) -instance : HasFromJson StaticRegistrationOptions := +instance : FromJson StaticRegistrationOptions := ⟨fun j => some ⟨j.getObjValAs? String "id"⟩⟩ -instance : HasToJson StaticRegistrationOptions := +instance : ToJson StaticRegistrationOptions := ⟨fun o => mkObj $ opt "id" o.id?⟩ structure TextDocumentRegistrationOptions := (documentSelector? : Option DocumentSelector := none) -instance : HasFromJson TextDocumentRegistrationOptions := +instance : FromJson TextDocumentRegistrationOptions := ⟨fun j => some ⟨j.getObjValAs? DocumentSelector "documentSelector"⟩⟩ -instance : HasToJson TextDocumentRegistrationOptions := +instance : ToJson TextDocumentRegistrationOptions := ⟨fun o => mkObj $ opt "documentSelector" o.documentSelector?⟩ inductive MarkupKind | plaintext | markdown -instance : HasFromJson MarkupKind := ⟨fun j => +instance : FromJson MarkupKind := ⟨fun j => match j with | str "plaintext" => some MarkupKind.plaintext | str "markdown" => some MarkupKind.markdown | _ => none⟩ -instance : HasToJson MarkupKind := ⟨fun k => +instance : ToJson MarkupKind := ⟨fun k => match k with | MarkupKind.plaintext => str "plaintext" | MarkupKind.markdown => str "markdown"⟩ structure MarkupContent := (kind : MarkupKind) (value : String) -instance : HasFromJson MarkupContent := ⟨fun j => do +instance : FromJson MarkupContent := ⟨fun j => do let kind ← j.getObjValAs? MarkupKind "kind" let value ← j.getObjValAs? String "value" pure ⟨kind, value⟩⟩ -instance : HasToJson MarkupContent := ⟨fun o => +instance : ToJson MarkupContent := ⟨fun o => mkObj [ ⟨"kind", toJson o.kind⟩, ⟨"value", o.value⟩]⟩ diff --git a/stage0/src/Lean/Data/Lsp/Capabilities.lean b/stage0/src/Lean/Data/Lsp/Capabilities.lean index 749c1ee75a..396675ffe0 100644 --- a/stage0/src/Lean/Data/Lsp/Capabilities.lean +++ b/stage0/src/Lean/Data/Lsp/Capabilities.lean @@ -19,7 +19,7 @@ open Json -- TODO: right now we ignore the client's capabilities inductive ClientCapabilities | mk -instance : HasFromJson ClientCapabilities := +instance : FromJson ClientCapabilities := ⟨fun j => ClientCapabilities.mk⟩ -- TODO largely unimplemented @@ -27,7 +27,7 @@ structure ServerCapabilities := (textDocumentSync? : Option TextDocumentSyncOptions := none) (hoverProvider : Bool := false) -instance : HasToJson ServerCapabilities := ⟨fun o => mkObj $ +instance : ToJson ServerCapabilities := ⟨fun o => mkObj $ opt "textDocumentSync" o.textDocumentSync? ++ [⟨"hoverProvider", o.hoverProvider⟩]⟩ diff --git a/stage0/src/Lean/Data/Lsp/Communication.lean b/stage0/src/Lean/Data/Lsp/Communication.lean index 58019cd35b..7a944a4b06 100644 --- a/stage0/src/Lean/Data/Lsp/Communication.lean +++ b/stage0/src/Lean/Data/Lsp/Communication.lean @@ -51,11 +51,11 @@ def readLspMessage (h : FS.Stream) : IO Message := do let nBytes ← readLspHeader h h.readMessage nBytes -def readLspRequestAs (h : FS.Stream) (expectedMethod : String) (α : Type) [HasFromJson α] : IO (Request α) := do +def readLspRequestAs (h : FS.Stream) (expectedMethod : String) (α : Type) [FromJson α] : IO (Request α) := do let nBytes ← readLspHeader h h.readRequestAs nBytes expectedMethod α -def readLspNotificationAs (h : FS.Stream) (expectedMethod : String) (α : Type) [HasFromJson α] : IO α := do +def readLspNotificationAs (h : FS.Stream) (expectedMethod : String) (α : Type) [FromJson α] : IO α := do let nBytes ← readLspHeader h h.readNotificationAs nBytes expectedMethod α @@ -67,10 +67,10 @@ def writeLspMessage (h : FS.Stream) (m : Message) : IO Unit := do h.putStr (header ++ j) h.flush -def writeLspResponse {α : Type} [HasToJson α] (h : FS.Stream) (id : RequestID) (r : α) : IO Unit := +def writeLspResponse {α : Type} [ToJson α] (h : FS.Stream) (id : RequestID) (r : α) : IO Unit := writeLspMessage h (Message.response id (toJson r)) -def writeLspNotification {α : Type} [HasToJson α] (h : FS.Stream) (method : String) (r : α) : IO Unit := +def writeLspNotification {α : Type} [ToJson α] (h : FS.Stream) (method : String) (r : α) : IO Unit := match toJson r with | Json.obj o => writeLspMessage h (Message.notification method o) | Json.arr a => writeLspMessage h (Message.notification method a) diff --git a/stage0/src/Lean/Data/Lsp/Diagnostics.lean b/stage0/src/Lean/Data/Lsp/Diagnostics.lean index 83c1ee1c1d..21ab1ae1e9 100644 --- a/stage0/src/Lean/Data/Lsp/Diagnostics.lean +++ b/stage0/src/Lean/Data/Lsp/Diagnostics.lean @@ -21,7 +21,7 @@ open Json inductive DiagnosticSeverity | error | warning | information | hint -instance : HasFromJson DiagnosticSeverity := ⟨fun j => +instance : FromJson DiagnosticSeverity := ⟨fun j => match j.getNat? with | some 1 => DiagnosticSeverity.error | some 2 => DiagnosticSeverity.warning @@ -29,7 +29,7 @@ instance : HasFromJson DiagnosticSeverity := ⟨fun j => | some 4 => DiagnosticSeverity.hint | _ => none⟩ -instance : HasToJson DiagnosticSeverity := ⟨fun o => +instance : ToJson DiagnosticSeverity := ⟨fun o => match o with | DiagnosticSeverity.error => 1 | DiagnosticSeverity.warning => 2 @@ -40,13 +40,13 @@ inductive DiagnosticCode | int (i : Int) | string (s : String) -instance : HasFromJson DiagnosticCode := ⟨fun j => +instance : FromJson DiagnosticCode := ⟨fun j => match j with | num (i : Int) => DiagnosticCode.int i | str s => DiagnosticCode.string s | _ => none⟩ -instance : HasToJson DiagnosticCode := ⟨fun o => +instance : ToJson DiagnosticCode := ⟨fun o => match o with | DiagnosticCode.int i => i | DiagnosticCode.string s => s⟩ @@ -55,13 +55,13 @@ inductive DiagnosticTag | unnecessary | deprecated -instance : HasFromJson DiagnosticTag := ⟨fun j => +instance : FromJson DiagnosticTag := ⟨fun j => match j.getNat? with | some 1 => DiagnosticTag.unnecessary | some 2 => DiagnosticTag.deprecated | _ => none⟩ -instance : HasToJson DiagnosticTag := ⟨fun o => +instance : ToJson DiagnosticTag := ⟨fun o => match o with | DiagnosticTag.unnecessary => (1 : Nat) | DiagnosticTag.deprecated => (2 : Nat)⟩ @@ -70,12 +70,12 @@ structure DiagnosticRelatedInformation := (location : Location) (message : String) -instance : HasFromJson DiagnosticRelatedInformation := ⟨fun j => do +instance : FromJson DiagnosticRelatedInformation := ⟨fun j => do let location ← j.getObjValAs? Location "location" let message ← j.getObjValAs? String "message" pure ⟨location, message⟩⟩ -instance : HasToJson DiagnosticRelatedInformation := ⟨fun o => +instance : ToJson DiagnosticRelatedInformation := ⟨fun o => mkObj [ ⟨"location", toJson o.location⟩, ⟨"message", o.message⟩]⟩ @@ -89,7 +89,7 @@ structure Diagnostic := (tags? : Option (Array DiagnosticTag) := none) (relatedInformation? : Option (Array DiagnosticRelatedInformation) := none) -instance : HasFromJson Diagnostic := ⟨fun j => do +instance : FromJson Diagnostic := ⟨fun j => do let range ← j.getObjValAs? Range "range" let severity? := j.getObjValAs? DiagnosticSeverity "severity" let code? := j.getObjValAs? DiagnosticCode "code" @@ -99,7 +99,7 @@ instance : HasFromJson Diagnostic := ⟨fun j => do let relatedInformation? := j.getObjValAs? (Array DiagnosticRelatedInformation) "relatedInformation" pure ⟨range, severity?, code?, source?, message, tags?, relatedInformation?⟩⟩ -instance : HasToJson Diagnostic := ⟨fun o => mkObj $ +instance : ToJson Diagnostic := ⟨fun o => mkObj $ opt "severity" o.severity? ++ opt "code" o.code? ++ opt "source" o.source? ++ @@ -113,13 +113,13 @@ structure PublishDiagnosticsParams := (version? : Option Int := none) (diagnostics: Array Diagnostic) -instance : HasFromJson PublishDiagnosticsParams := ⟨fun j => do +instance : FromJson PublishDiagnosticsParams := ⟨fun j => do let uri ← j.getObjValAs? DocumentUri "uri" let version? := j.getObjValAs? Int "version" let diagnostics ← j.getObjValAs? (Array Diagnostic) "diagnostics" pure ⟨uri, version?, diagnostics⟩⟩ -instance : HasToJson PublishDiagnosticsParams := ⟨fun o => mkObj $ +instance : ToJson PublishDiagnosticsParams := ⟨fun o => mkObj $ opt "version" o.version? ++ [ ⟨"uri", toJson o.uri⟩, ⟨"diagnostics", toJson o.diagnostics⟩]⟩ diff --git a/stage0/src/Lean/Data/Lsp/Hover.lean b/stage0/src/Lean/Data/Lsp/Hover.lean index c6891fecce..87cbf7c322 100644 --- a/stage0/src/Lean/Data/Lsp/Hover.lean +++ b/stage0/src/Lean/Data/Lsp/Hover.lean @@ -20,22 +20,22 @@ structure Hover := (contents : MarkupContent) (range? : Option Range := none) -instance : HasFromJson Hover := ⟨fun j => do +instance : FromJson Hover := ⟨fun j => do let contents ← j.getObjValAs? MarkupContent "contents" let range? := j.getObjValAs? Range "range" pure ⟨contents, range?⟩⟩ -instance : HasToJson Hover := ⟨fun o => mkObj $ +instance : ToJson Hover := ⟨fun o => mkObj $ ⟨"contents", toJson o.contents⟩ :: opt "range" o.range?⟩ structure HoverParams extends TextDocumentPositionParams -instance : HasFromJson HoverParams := ⟨fun j => do +instance : FromJson HoverParams := ⟨fun j => do let tdpp ← @fromJson? TextDocumentPositionParams _ j pure ⟨tdpp⟩⟩ -instance : HasToJson HoverParams := +instance : ToJson HoverParams := ⟨fun o => toJson o.toTextDocumentPositionParams⟩ end Lsp diff --git a/stage0/src/Lean/Data/Lsp/InitShutdown.lean b/stage0/src/Lean/Data/Lsp/InitShutdown.lean index 08fce78384..8d073fed74 100644 --- a/stage0/src/Lean/Data/Lsp/InitShutdown.lean +++ b/stage0/src/Lean/Data/Lsp/InitShutdown.lean @@ -20,7 +20,7 @@ structure ClientInfo := (name : String) (version? : Option String := none) -instance : HasFromJson ClientInfo := ⟨fun j => do +instance : FromJson ClientInfo := ⟨fun j => do let name ← j.getObjValAs? String "name" let version? := j.getObjValAs? String "version" pure ⟨name, version?⟩⟩ @@ -30,7 +30,7 @@ inductive Trace | messages | verbose -instance : HasFromJson Trace := ⟨fun j => +instance : FromJson Trace := ⟨fun j => match j.getStr? with | some "off" => Trace.off | some "messages" => Trace.messages @@ -49,7 +49,7 @@ structure InitializeParams := (trace : Trace := Trace.off) (workspaceFolders? : Option (Array WorkspaceFolder) := none) -instance : HasFromJson InitializeParams := ⟨fun j => do +instance : FromJson InitializeParams := ⟨fun j => do /- Many of these params can be null instead of not present. For ease of implementation, we're liberal: missing params, wrong json types and null all map to none, @@ -68,14 +68,14 @@ instance : HasFromJson InitializeParams := ⟨fun j => do inductive InitializedParams | mk -instance : HasFromJson InitializedParams := +instance : FromJson InitializedParams := ⟨fun j => InitializedParams.mk⟩ structure ServerInfo := (name : String) (version? : Option String := none) -instance : HasToJson ServerInfo := ⟨fun o => mkObj $ +instance : ToJson ServerInfo := ⟨fun o => mkObj $ ⟨"name", o.name⟩ :: opt "version" o.version?⟩ @@ -83,7 +83,7 @@ structure InitializeResult := (capabilities : ServerCapabilities) (serverInfo? : Option ServerInfo := none) -instance : HasToJson InitializeResult := ⟨fun o => +instance : ToJson InitializeResult := ⟨fun o => mkObj $ ⟨"capabilities", toJson o.capabilities⟩ :: opt "serverInfo" o.serverInfo?⟩ diff --git a/stage0/src/Lean/Data/Lsp/TextSync.lean b/stage0/src/Lean/Data/Lsp/TextSync.lean index 680af51b04..b1c910b97e 100644 --- a/stage0/src/Lean/Data/Lsp/TextSync.lean +++ b/stage0/src/Lean/Data/Lsp/TextSync.lean @@ -19,14 +19,14 @@ inductive TextDocumentSyncKind | full | incremental -instance : HasFromJson TextDocumentSyncKind := ⟨fun j => +instance : FromJson TextDocumentSyncKind := ⟨fun j => match j.getNat? with | some 0 => TextDocumentSyncKind.none | some 1 => TextDocumentSyncKind.full | some 2 => TextDocumentSyncKind.incremental | _ => none⟩ -instance : HasToJson TextDocumentSyncKind := ⟨fun o => +instance : ToJson TextDocumentSyncKind := ⟨fun o => match o with | TextDocumentSyncKind.none => 0 | TextDocumentSyncKind.full => 1 @@ -35,17 +35,17 @@ instance : HasToJson TextDocumentSyncKind := ⟨fun o => structure DidOpenTextDocumentParams := (textDocument : TextDocumentItem) -instance : HasFromJson DidOpenTextDocumentParams := ⟨fun j => +instance : FromJson DidOpenTextDocumentParams := ⟨fun j => DidOpenTextDocumentParams.mk <$> j.getObjValAs? TextDocumentItem "textDocument"⟩ -instance : HasToJson DidOpenTextDocumentParams := ⟨fun o => +instance : ToJson DidOpenTextDocumentParams := ⟨fun o => mkObj $ [⟨"textDocument", toJson o.textDocument⟩]⟩ structure TextDocumentChangeRegistrationOptions := (documentSelector? : Option DocumentSelector := none) (syncKind : TextDocumentSyncKind) -instance : HasFromJson TextDocumentChangeRegistrationOptions := ⟨fun j => do +instance : FromJson TextDocumentChangeRegistrationOptions := ⟨fun j => do let documentSelector? := j.getObjValAs? DocumentSelector "documentSelector"; let syncKind ← j.getObjValAs? TextDocumentSyncKind "syncKind"; pure ⟨documentSelector?, syncKind⟩⟩ @@ -55,7 +55,7 @@ inductive TextDocumentContentChangeEvent | rangeChange (range : Range) (text : String) | fullChange (text : String) -instance : HasFromJson TextDocumentContentChangeEvent := ⟨fun j => +instance : FromJson TextDocumentContentChangeEvent := ⟨fun j => (do let range ← j.getObjValAs? Range "range" let text ← j.getObjValAs? String "text" @@ -66,7 +66,7 @@ structure DidChangeTextDocumentParams := (textDocument : VersionedTextDocumentIdentifier) (contentChanges : Array TextDocumentContentChangeEvent) -instance : HasFromJson DidChangeTextDocumentParams := ⟨fun j => do +instance : FromJson DidChangeTextDocumentParams := ⟨fun j => do let textDocument ← j.getObjValAs? VersionedTextDocumentIdentifier "textDocument" let contentChanges ← j.getObjValAs? (Array TextDocumentContentChangeEvent) "contentChanges" pure ⟨textDocument, contentChanges⟩⟩ @@ -77,12 +77,12 @@ instance : HasFromJson DidChangeTextDocumentParams := ⟨fun j => do structure SaveOptions := (includeText : Bool) -instance : HasToJson SaveOptions := ⟨fun o => +instance : ToJson SaveOptions := ⟨fun o => mkObj $ [⟨"includeText", o.includeText⟩]⟩ structure DidCloseTextDocumentParams := (textDocument : TextDocumentIdentifier) -instance : HasFromJson DidCloseTextDocumentParams := ⟨fun j => +instance : FromJson DidCloseTextDocumentParams := ⟨fun j => DidCloseTextDocumentParams.mk <$> j.getObjValAs? TextDocumentIdentifier "textDocument"⟩ -- TODO: TextDocumentSyncClientCapabilities @@ -95,7 +95,7 @@ structure TextDocumentSyncOptions := (willSaveWaitUntil : Bool) (save? : Option SaveOptions := none) -instance : HasToJson TextDocumentSyncOptions := ⟨fun o => +instance : ToJson TextDocumentSyncOptions := ⟨fun o => mkObj $ opt "save" o.save? ++ [ ⟨"openClose", toJson o.openClose⟩, diff --git a/stage0/src/Lean/Data/Lsp/Workspace.lean b/stage0/src/Lean/Data/Lsp/Workspace.lean index 4b4e2ce23c..c58a1e1b86 100644 --- a/stage0/src/Lean/Data/Lsp/Workspace.lean +++ b/stage0/src/Lean/Data/Lsp/Workspace.lean @@ -16,12 +16,12 @@ structure WorkspaceFolder := (uri : DocumentUri) (name : String) -instance : HasFromJson WorkspaceFolder := ⟨fun j => do +instance : FromJson WorkspaceFolder := ⟨fun j => do let uri ← j.getObjValAs? DocumentUri "uri" let name ← j.getObjValAs? String "name" pure ⟨uri, name⟩⟩ -instance : HasToJson WorkspaceFolder := ⟨fun o => +instance : ToJson WorkspaceFolder := ⟨fun o => mkObj [ ⟨"uri", toJson o.uri⟩, ⟨"name", toJson o.name⟩]⟩ diff --git a/stage0/src/Lean/Data/Name.lean b/stage0/src/Lean/Data/Name.lean index 69bcb7b934..19ca39b9a5 100644 --- a/stage0/src/Lean/Data/Name.lean +++ b/stage0/src/Lean/Data/Name.lean @@ -93,10 +93,10 @@ else if n₁.hash > n₂.hash then false else quickLtAux n₁ n₂ /- Alternative HasLt instance. -/ -@[inline] protected def hasLtQuick : HasLess Name := +@[inline] protected def hasLtQuick : Less Name := ⟨fun a b => Name.quickLt a b = true⟩ -@[inline] instance : DecidableRel (@HasLess.Less Name Name.hasLtQuick) := +@[inline] instance : DecidableRel (@Less.Less Name Name.hasLtQuick) := inferInstanceAs (DecidableRel (fun a b => Name.quickLt a b = true)) /- The frontend does not allow user declarations to start with `_` in any of its parts. @@ -135,7 +135,7 @@ def NameMap (α : Type) := Std.RBMap Name α Name.quickLt namespace NameMap variable {α : Type} -instance (α : Type) : HasEmptyc (NameMap α) := ⟨mkNameMap α⟩ +instance (α : Type) : EmptyCollection (NameMap α) := ⟨mkNameMap α⟩ instance (α : Type) : Inhabited (NameMap α) := ⟨{}⟩ @@ -151,7 +151,7 @@ def NameSet := RBTree Name Name.quickLt namespace NameSet def empty : NameSet := mkRBTree Name Name.quickLt -instance : HasEmptyc NameSet := ⟨empty⟩ +instance : EmptyCollection NameSet := ⟨empty⟩ instance : Inhabited NameSet := ⟨{}⟩ def insert (s : NameSet) (n : Name) : NameSet := Std.RBTree.insert s n def contains (s : NameSet) (n : Name) : Bool := Std.RBMap.contains s n @@ -162,7 +162,7 @@ def NameHashSet := Std.HashSet Name namespace NameHashSet @[inline] def empty : NameHashSet := Std.HashSet.empty -instance : HasEmptyc NameHashSet := ⟨empty⟩ +instance : EmptyCollection NameHashSet := ⟨empty⟩ instance : Inhabited NameHashSet := ⟨{}⟩ def insert (s : NameHashSet) (n : Name) := Std.HashSet.insert s n def contains (s : NameHashSet) (n : Name) : Bool := Std.HashSet.contains s n diff --git a/stage0/src/Lean/Data/Occurrences.lean b/stage0/src/Lean/Data/Occurrences.lean index 91e5680500..3ce01ab1e9 100644 --- a/stage0/src/Lean/Data/Occurrences.lean +++ b/stage0/src/Lean/Data/Occurrences.lean @@ -30,7 +30,7 @@ def beq : Occurrences → Occurrences → Bool | neg is₁, neg is₂ => is₁ == is₂ | _, _ => false -instance : HasBeq Occurrences := ⟨beq⟩ +instance : BEq Occurrences := ⟨beq⟩ end Occurrences diff --git a/stage0/src/Lean/Data/SMap.lean b/stage0/src/Lean/Data/SMap.lean index 5bf1f18b35..40efe770d4 100644 --- a/stage0/src/Lean/Data/SMap.lean +++ b/stage0/src/Lean/Data/SMap.lean @@ -27,13 +27,13 @@ open Std (HashMap PHashMap) that an entry was "removed" from the hashtable. - We do not need additional bookkeeping for extracting the local entries. -/ -structure SMap (α : Type u) (β : Type v) [HasBeq α] [Hashable α] := +structure SMap (α : Type u) (β : Type v) [BEq α] [Hashable α] := (stage₁ : Bool := true) (map₁ : HashMap α β := {}) (map₂ : PHashMap α β := {}) namespace SMap -variables {α : Type u} {β : Type v} [HasBeq α] [Hashable α] +variables {α : Type u} {β : Type v} [BEq α] [Hashable α] instance : Inhabited (SMap α β) := ⟨{}⟩ def empty : SMap α β := {} diff --git a/stage0/src/Lean/Data/Trie.lean b/stage0/src/Lean/Data/Trie.lean index 209931b00f..23890469d5 100644 --- a/stage0/src/Lean/Data/Trie.lean +++ b/stage0/src/Lean/Data/Trie.lean @@ -21,7 +21,7 @@ variables {α : Type} def empty : Trie α := ⟨none, RBNode.leaf⟩ -instance : HasEmptyc (Trie α) := +instance : EmptyCollection (Trie α) := ⟨empty⟩ instance : Inhabited (Trie α) := diff --git a/stage0/src/Lean/Delaborator.lean b/stage0/src/Lean/Delaborator.lean index a5b2ffb4d6..0f9c0da77c 100644 --- a/stage0/src/Lean/Delaborator.lean +++ b/stage0/src/Lean/Delaborator.lean @@ -48,7 +48,7 @@ protected partial def quote : Level → Syntax -- HACK: approximation | mvar n _ => Unhygienic.run `(level|_) -instance : HasQuote Level := ⟨Level.quote⟩ +instance : Quote Level := ⟨Level.quote⟩ end Level def getPPBinderTypes (o : Options) : Bool := o.get `pp.binder_types true @@ -104,7 +104,7 @@ instance : Alternative DelabM := { failure := Delaborator.failure } -- HACK: necessary since it would otherwise prefer the instance from MonadExcept -instance {α} : HasOrelse (DelabM α) := ⟨Delaborator.orelse⟩ +instance {α} : OrElse (DelabM α) := ⟨Delaborator.orelse⟩ -- Macro scopes in the delaborator output are ultimately ignored by the pretty printer, -- so give a trivial implementation. @@ -507,7 +507,7 @@ def delabLit : Delab := do | Literal.strVal s => pure $ quote s -- `ofNat 0` ~> `0` -@[builtinDelab app.HasOfNat.ofNat] +@[builtinDelab app.OfNat.ofNat] def delabOfNat : Delab := whenPPOption getPPCoercions do let e@(Expr.app _ (Expr.lit (Literal.natVal n) _) _) ← getExpr | failure pure $ quote n @@ -627,24 +627,24 @@ def delabPrefixOp (op : Bool → Syntax → Delab) : Delab := whenPPOption getPP @[builtinDelab app.Prod] def delabProd : Delab := delabInfixOp fun _ x y => `($x × $y) @[builtinDelab app.Function.comp] def delabFComp : Delab := delabInfixOp fun _ x y => `($x ∘ $y) -@[builtinDelab app.HasAdd.add] def delabAdd : Delab := delabInfixOp fun _ x y => `($x + $y) -@[builtinDelab app.HasSub.sub] def delabSub : Delab := delabInfixOp fun _ x y => `($x - $y) -@[builtinDelab app.HasMul.mul] def delabMul : Delab := delabInfixOp fun _ x y => `($x * $y) -@[builtinDelab app.HasDiv.div] def delabDiv : Delab := delabInfixOp fun _ x y => `($x / $y) -@[builtinDelab app.HasMod.mod] def delabMod : Delab := delabInfixOp fun _ x y => `($x % $y) -@[builtinDelab app.HasModN.modn] def delabModN : Delab := delabInfixOp fun _ x y => `($x %ₙ $y) -@[builtinDelab app.HasPow.pow] def delabPow : Delab := delabInfixOp fun _ x y => `($x ^ $y) +@[builtinDelab app.Add.add] def delabAdd : Delab := delabInfixOp fun _ x y => `($x + $y) +@[builtinDelab app.Sub.sub] def delabSub : Delab := delabInfixOp fun _ x y => `($x - $y) +@[builtinDelab app.Mul.mul] def delabMul : Delab := delabInfixOp fun _ x y => `($x * $y) +@[builtinDelab app.Div.div] def delabDiv : Delab := delabInfixOp fun _ x y => `($x / $y) +@[builtinDelab app.Mod.mod] def delabMod : Delab := delabInfixOp fun _ x y => `($x % $y) +@[builtinDelab app.ModN.modn] def delabModN : Delab := delabInfixOp fun _ x y => `($x %ₙ $y) +@[builtinDelab app.Pow.pow] def delabPow : Delab := delabInfixOp fun _ x y => `($x ^ $y) -@[builtinDelab app.HasLessEq.LessEq] def delabLE : Delab := delabInfixOp fun b x y => cond b `($x ≤ $y) `($x <= $y) +@[builtinDelab app.LessEq.LessEq] def delabLE : Delab := delabInfixOp fun b x y => cond b `($x ≤ $y) `($x <= $y) @[builtinDelab app.GreaterEq] def delabGE : Delab := delabInfixOp fun b x y => cond b `($x ≥ $y) `($x >= $y) -@[builtinDelab app.HasLess.Less] def delabLT : Delab := delabInfixOp fun _ x y => `($x < $y) +@[builtinDelab app.Less.Less] def delabLT : Delab := delabInfixOp fun _ x y => `($x < $y) @[builtinDelab app.Greater] def delabGT : Delab := delabInfixOp fun _ x y => `($x > $y) @[builtinDelab app.Eq] def delabEq : Delab := delabInfixOp fun _ x y => `($x = $y) @[builtinDelab app.Ne] def delabNe : Delab := delabInfixOp fun _ x y => `($x ≠ $y) -@[builtinDelab app.HasBeq.beq] def delabBEq : Delab := delabInfixOp fun _ x y => `($x == $y) +@[builtinDelab app.BEq.beq] def delabBEq : Delab := delabInfixOp fun _ x y => `($x == $y) @[builtinDelab app.bne] def delabBNe : Delab := delabInfixOp fun _ x y => `($x != $y) @[builtinDelab app.HEq] def delabHEq : Delab := delabInfixOp fun b x y => cond b `($x ≅ $y) `($x ~= $y) -@[builtinDelab app.HasEquiv.Equiv] def delabEquiv : Delab := delabInfixOp fun _ x y => `($x ≈ $y) +@[builtinDelab app.Equiv.Equiv] def delabEquiv : Delab := delabInfixOp fun _ x y => `($x ≈ $y) @[builtinDelab app.And] def delabAnd : Delab := delabInfixOp fun b x y => cond b `($x ∧ $y) `($x /\ $y) @[builtinDelab app.Or] def delabOr : Delab := delabInfixOp fun b x y => cond b `($x ∨ $y) `($x || $y) @@ -653,20 +653,20 @@ def delabPrefixOp (op : Bool → Syntax → Delab) : Delab := whenPPOption getPP @[builtinDelab app.and] def delabBAnd : Delab := delabInfixOp fun _ x y => `($x && $y) @[builtinDelab app.or] def delabBOr : Delab := delabInfixOp fun _ x y => `($x || $y) -@[builtinDelab app.HasAppend.append] def delabAppend : Delab := delabInfixOp fun _ x y => `($x ++ $y) +@[builtinDelab app.Append.append] def delabAppend : Delab := delabInfixOp fun _ x y => `($x ++ $y) @[builtinDelab app.List.cons] def delabCons : Delab := delabInfixOp fun _ x y => `($x :: $y) -@[builtinDelab app.HasAndthen.andthen] def delabAndThen : Delab := delabInfixOp fun _ x y => `($x >> $y) -@[builtinDelab app.HasBind.bind] def delabBind : Delab := delabInfixOp fun _ x y => `($x >>= $y) +@[builtinDelab app.AndThen.andthen] def delabAndThen : Delab := delabInfixOp fun _ x y => `($x >> $y) +@[builtinDelab app.Bind.bind] def delabBind : Delab := delabInfixOp fun _ x y => `($x >>= $y) -@[builtinDelab app.HasSeq.seq] def delabseq : Delab := delabInfixOp fun _ x y => `($x <*> $y) -@[builtinDelab app.HasSeqLeft.seqLeft] def delabseqLeft : Delab := delabInfixOp fun _ x y => `($x <* $y) -@[builtinDelab app.HasSeqRight.seqRight] def delabseqRight : Delab := delabInfixOp fun _ x y => `($x *> $y) +@[builtinDelab app.Seq.seq] def delabseq : Delab := delabInfixOp fun _ x y => `($x <*> $y) +@[builtinDelab app.SeqLeft.seqLeft] def delabseqLeft : Delab := delabInfixOp fun _ x y => `($x <* $y) +@[builtinDelab app.SeqRight.seqRight] def delabseqRight : Delab := delabInfixOp fun _ x y => `($x *> $y) @[builtinDelab app.Functor.map] def delabMap : Delab := delabInfixOp fun _ x y => `($x <$> $y) @[builtinDelab app.Functor.mapRev] def delabMapRev : Delab := delabInfixOp fun _ x y => `($x <&> $y) -@[builtinDelab app.HasOrelse.orelse] def delabOrElse : Delab := delabInfixOp fun _ x y => `($x <|> $y) +@[builtinDelab app.OrElse.orelse] def delabOrElse : Delab := delabInfixOp fun _ x y => `($x <|> $y) @[builtinDelab app.orM] def delabOrM : Delab := delabInfixOp fun _ x y => `($x <||> $y) @[builtinDelab app.andM] def delabAndM : Delab := delabInfixOp fun _ x y => `($x <&&> $y) diff --git a/stage0/src/Lean/Elab/Tactic/Basic.lean b/stage0/src/Lean/Elab/Tactic/Basic.lean index a8641ee851..e7caecee7a 100644 --- a/stage0/src/Lean/Elab/Tactic/Basic.lean +++ b/stage0/src/Lean/Elab/Tactic/Basic.lean @@ -59,7 +59,7 @@ instance : MonadExcept Exception TacticM := { tryCatch := Tactic.tryCatch } -instance {α} : HasOrelse (TacticM α) := ⟨Tactic.orelse⟩ +instance {α} : OrElse (TacticM α) := ⟨Tactic.orelse⟩ structure SavedState := (core : Core.State) diff --git a/stage0/src/Lean/Elab/Term.lean b/stage0/src/Lean/Elab/Term.lean index 5ae33ae098..5a1e0b366a 100644 --- a/stage0/src/Lean/Elab/Term.lean +++ b/stage0/src/Lean/Elab/Term.lean @@ -1276,13 +1276,13 @@ private def mkSomeContext : Context := { let ((a, s), sCore, sMeta) ← (x.run ctx s).toIO ctxCore sCore ctxMeta sMeta pure (a, sCore, sMeta, s) -instance {α} [MetaHasEval α] : MetaHasEval (TermElabM α) := +instance {α} [MetaEval α] : MetaEval (TermElabM α) := ⟨fun env opts x _ => let x : TermElabM α := do try x finally let s ← get liftIO $ s.messages.forM fun msg => msg.toString >>= IO.println - MetaHasEval.eval env opts (hideUnit := true) $ x.run' mkSomeContext⟩ + MetaEval.eval env opts (hideUnit := true) $ x.run' mkSomeContext⟩ end Term diff --git a/stage0/src/Lean/Eval.lean b/stage0/src/Lean/Eval.lean index 4ee4482161..24b2ab5c83 100644 --- a/stage0/src/Lean/Eval.lean +++ b/stage0/src/Lean/Eval.lean @@ -9,16 +9,16 @@ namespace Lean universe u -/-- `HasEval` extension that gives access to the current environment & options. - The basic `HasEval` class is in the prelude and should not depend on these +/-- `Eval` extension that gives access to the current environment & options. + The basic `Eval` class is in the prelude and should not depend on these types. -/ -class MetaHasEval (α : Type u) := +class MetaEval (α : Type u) := (eval : Environment → Options → α → (hideUnit : Bool) → IO Environment) -instance {α : Type u} [HasEval α] : MetaHasEval α := -⟨fun env opts a hideUnit => do HasEval.eval (fun _ => a) hideUnit; pure env⟩ +instance {α : Type u} [Eval α] : MetaEval α := +⟨fun env opts a hideUnit => do Eval.eval (fun _ => a) hideUnit; pure env⟩ -def runMetaEval {α : Type u} [MetaHasEval α] (env : Environment) (opts : Options) (a : α) : IO (String × Except IO.Error Environment) := -IO.FS.withIsolatedStreams (MetaHasEval.eval env opts a false) +def runMetaEval {α : Type u} [MetaEval α] (env : Environment) (opts : Options) (a : α) : IO (String × Except IO.Error Environment) := +IO.FS.withIsolatedStreams (MetaEval.eval env opts a false) end Lean diff --git a/stage0/src/Lean/Expr.lean b/stage0/src/Lean/Expr.lean index c0226e7a9f..a549393f75 100644 --- a/stage0/src/Lean/Expr.lean +++ b/stage0/src/Lean/Expr.lean @@ -25,7 +25,7 @@ def Literal.beq : Literal → Literal → Bool | Literal.strVal v₁, Literal.strVal v₂ => v₁ == v₂ | _, _ => false -instance : HasBeq Literal := ⟨Literal.beq⟩ +instance : BEq Literal := ⟨Literal.beq⟩ def Literal.lt : Literal → Literal → Bool | Literal.natVal _, Literal.strVal _ => true @@ -33,7 +33,7 @@ def Literal.lt : Literal → Literal → Bool | Literal.strVal v₁, Literal.strVal v₂ => v₁ < v₂ | _, _ => false -instance : HasLess Literal := ⟨fun a b => a.lt b⟩ +instance : Less Literal := ⟨fun a b => a.lt b⟩ instance (a b : Literal) : Decidable (a < b) := inferInstanceAs (Decidable (a.lt b)) @@ -74,7 +74,7 @@ protected def BinderInfo.beq : BinderInfo → BinderInfo → Bool | BinderInfo.auxDecl, BinderInfo.auxDecl => true | _, _ => false -instance : HasBeq BinderInfo := ⟨BinderInfo.beq⟩ +instance : BEq BinderInfo := ⟨BinderInfo.beq⟩ abbrev MData := KVMap abbrev MData.empty : MData := {} @@ -97,7 +97,7 @@ instance: Inhabited Expr.Data := def Expr.Data.hash (c : Expr.Data) : USize := c.toUInt32.toUSize -instance : HasBeq Expr.Data := +instance : BEq Expr.Data := ⟨fun (a b : UInt64) => a == b⟩ def Expr.Data.looseBVarRange (c : Expr.Data) : UInt32 := @@ -388,7 +388,7 @@ constant lt (a : @& Expr) (b : @& Expr) : Bool @[extern "lean_expr_eqv"] constant eqv (a : @& Expr) (b : @& Expr) : Bool -instance : HasBeq Expr := ⟨Expr.eqv⟩ +instance : BEq Expr := ⟨Expr.eqv⟩ /- Return true iff `a` and `b` are equal. Binder names and annotations are taking into account. -/ @@ -735,7 +735,7 @@ protected def hash : ExprStructEq → USize | ⟨e⟩ => e.hash instance : Inhabited ExprStructEq := ⟨{ val := arbitrary _ }⟩ -instance : HasBeq ExprStructEq := ⟨ExprStructEq.beq⟩ +instance : BEq ExprStructEq := ⟨ExprStructEq.beq⟩ instance : Hashable ExprStructEq := ⟨ExprStructEq.hash⟩ instance : ToString ExprStructEq := ⟨fun e => toString e.val⟩ instance : Repr ExprStructEq := ⟨fun e => repr e.val⟩ diff --git a/stage0/src/Lean/HeadIndex.lean b/stage0/src/Lean/HeadIndex.lean index 0db4e6550e..4b60ed03a0 100644 --- a/stage0/src/Lean/HeadIndex.lean +++ b/stage0/src/Lean/HeadIndex.lean @@ -44,7 +44,7 @@ protected def HeadIndex.beq : HeadIndex → HeadIndex → Bool | forallE, forallE => true | _, _ => false -instance : HasBeq HeadIndex := ⟨HeadIndex.beq⟩ +instance : BEq HeadIndex := ⟨HeadIndex.beq⟩ end HeadIndex diff --git a/stage0/src/Lean/InternalExceptionId.lean b/stage0/src/Lean/InternalExceptionId.lean index a73da9a5d3..5e6f6d92c0 100644 --- a/stage0/src/Lean/InternalExceptionId.lean +++ b/stage0/src/Lean/InternalExceptionId.lean @@ -9,7 +9,7 @@ structure InternalExceptionId := (idx : Nat := 0) instance : Inhabited InternalExceptionId := ⟨{}⟩ -instance : HasBeq InternalExceptionId := +instance : BEq InternalExceptionId := ⟨fun id₁ id₂ => id₁.idx == id₂.idx⟩ builtin_initialize internalExceptionsRef : IO.Ref (Array Name) ← IO.mkRef #[] diff --git a/stage0/src/Lean/Level.lean b/stage0/src/Lean/Level.lean index 3af4210380..9f1233af51 100644 --- a/stage0/src/Lean/Level.lean +++ b/stage0/src/Lean/Level.lean @@ -29,7 +29,7 @@ instance : Inhabited Level.Data := def Level.Data.hash (c : Level.Data) : USize := c.toUInt32.toUSize -instance : HasBeq Level.Data := +instance : BEq Level.Data := ⟨fun (a b : UInt64) => a == b⟩ def Level.Data.depth (c : Level.Data) : UInt32 := @@ -201,7 +201,7 @@ def toNat (lvl : Level) : Option Nat := @[extern "lean_level_eq"] protected constant beq (a : @& Level) (b : @& Level) : Bool := arbitrary _ -instance : HasBeq Level := ⟨Level.beq⟩ +instance : BEq Level := ⟨Level.beq⟩ /-- `occurs u l` return `true` iff `u` occurs in `l`. -/ def occurs : Level → Level → Bool diff --git a/stage0/src/Lean/Message.lean b/stage0/src/Lean/Message.lean index babb08bb52..c35a39f704 100644 --- a/stage0/src/Lean/Message.lean +++ b/stage0/src/Lean/Message.lean @@ -94,7 +94,7 @@ protected def toString (msgData : MessageData) : IO String := do let fmt ← msgData.format pure $ toString fmt -instance : HasAppend MessageData := ⟨compose⟩ +instance : Append MessageData := ⟨compose⟩ instance : Coe String MessageData := ⟨ofFormat ∘ format⟩ instance : Coe Format MessageData := ⟨ofFormat⟩ @@ -182,7 +182,7 @@ def add (msg : Message) (log : MessageLog) : MessageLog := protected def append (l₁ l₂ : MessageLog) : MessageLog := ⟨l₁.msgs ++ l₂.msgs⟩ -instance : HasAppend MessageLog := +instance : Append MessageLog := ⟨MessageLog.append⟩ def hasErrors (log : MessageLog) : Bool := diff --git a/stage0/src/Lean/Meta/AbstractMVars.lean b/stage0/src/Lean/Meta/AbstractMVars.lean index e87e5b2344..cfe0314546 100644 --- a/stage0/src/Lean/Meta/AbstractMVars.lean +++ b/stage0/src/Lean/Meta/AbstractMVars.lean @@ -17,7 +17,7 @@ instance : Inhabited AbstractMVarsResult := ⟨⟨#[], 0, arbitrary _⟩⟩ def AbstractMVarsResult.beq (r₁ r₂ : AbstractMVarsResult) : Bool := r₁.paramNames == r₂.paramNames && r₁.numMVars == r₂.numMVars && r₁.expr == r₂.expr -instance : HasBeq AbstractMVarsResult := ⟨AbstractMVarsResult.beq⟩ +instance : BEq AbstractMVarsResult := ⟨AbstractMVarsResult.beq⟩ namespace AbstractMVars diff --git a/stage0/src/Lean/Meta/AppBuilder.lean b/stage0/src/Lean/Meta/AppBuilder.lean index 638f0d4c8c..b44c2e2965 100644 --- a/stage0/src/Lean/Meta/AppBuilder.lean +++ b/stage0/src/Lean/Meta/AppBuilder.lean @@ -270,11 +270,11 @@ private partial def mkAppOptMAux (f : Expr) (xs : Array (Option Expr)) : Nat → /-- Similar to `mkAppM`, but it allows us to specify which arguments are provided explicitly using `Option` type. Example: - Given `Pure.pure {m : Type u → Type v} [HasPure m] {α : Type u} (a : α) : m α`, + Given `Pure.pure {m : Type u → Type v} [Pure m] {α : Type u} (a : α) : m α`, ``` mkAppOptM `Pure.pure #[m, none, none, a] ``` - returns a `Pure.pure` application if the instance `HasPure m` can be synthesized, and the universes match. + returns a `Pure.pure` application if the instance `Pure m` can be synthesized, and the universes match. Note that, ``` mkAppM `Pure.pure #[a] diff --git a/stage0/src/Lean/Meta/Basic.lean b/stage0/src/Lean/Meta/Basic.lean index 24b2f0fbd4..e9cfce0bcb 100644 --- a/stage0/src/Lean/Meta/Basic.lean +++ b/stage0/src/Lean/Meta/Basic.lean @@ -78,7 +78,7 @@ namespace InfoCacheKey instance : Inhabited InfoCacheKey := ⟨⟨arbitrary _, arbitrary _, arbitrary _⟩⟩ instance : Hashable InfoCacheKey := ⟨fun ⟨transparency, expr, nargs⟩ => mixHash (hash transparency) $ mixHash (hash expr) (hash nargs)⟩ -instance : HasBeq InfoCacheKey := +instance : BEq InfoCacheKey := ⟨fun ⟨t₁, e₁, n₁⟩ ⟨t₂, e₂, n₂⟩ => t₁ == t₂ && n₁ == n₂ && e₁ == e₂⟩ end InfoCacheKey @@ -144,8 +144,8 @@ instance : AddMessageContext MetaM := { let ((a, s), sCore) ← (x.run ctx s).toIO ctxCore sCore pure (a, sCore, s) -instance {α} [MetaHasEval α] : MetaHasEval (MetaM α) := - ⟨fun env opts x _ => MetaHasEval.eval env opts x.run' true⟩ +instance {α} [MetaEval α] : MetaEval (MetaM α) := + ⟨fun env opts x _ => MetaEval.eval env opts x.run' true⟩ protected def throwIsDefEqStuck {α} : MetaM α := throw $ Exception.internal isDefEqStuckExceptionId @@ -920,10 +920,10 @@ def withMCtx {α} (mctx : MetavarContext) : n α → n α := /-- Similar to `approxDefEq`, but uses all available approximations. We don't use `constApprox` by default at `approxDefEq` because it often produces undesirable solution for monadic code. - For example, suppose we have `pure (x > 0)` which has type `?m Prop`. We also have the goal `[HasPure ?m]`. + For example, suppose we have `pure (x > 0)` which has type `?m Prop`. We also have the goal `[Pure ?m]`. Now, assume the expected type is `IO Bool`. Then, the unification constraint `?m Prop =?= IO Bool` could be solved as `?m := fun _ => IO Bool` using `constApprox`, but this spurious solution would generate a failure when we try to - solve `[HasPure (fun _ => IO Bool)]` -/ + solve `[Pure (fun _ => IO Bool)]` -/ @[inline] def fullApproxDefEq {α} : n α → n α := mapMetaM fullApproxDefEqImp @@ -991,7 +991,7 @@ def ppExpr (e : Expr) : m Format := let mctx ← getMCtx try x catch _ => setEnv env; setMCtx mctx; y -instance {α} : HasOrelse (MetaM α) := ⟨Meta.orelse⟩ +instance {α} : OrElse (MetaM α) := ⟨Meta.orelse⟩ @[inline] private def orelseMergeErrorsImp {α} (x y : MetaM α) (mergeRef : Syntax → Syntax → Syntax := fun r₁ r₂ => r₁) diff --git a/stage0/src/Lean/Meta/DiscrTree.lean b/stage0/src/Lean/Meta/DiscrTree.lean index 1180a56df3..172ab5b3cc 100644 --- a/stage0/src/Lean/Meta/DiscrTree.lean +++ b/stage0/src/Lean/Meta/DiscrTree.lean @@ -29,13 +29,14 @@ namespace Lean.Meta.DiscrTree discrimination tree. Recall that projections from classes are **NOT** reducible. - For example, the expressions `Add.add α (ringHasAdd ?α ?s) ?x ?x` + For example, the expressions `Add.add α (ringAdd ?α ?s) ?x ?x` and `Add.add Nat Nat.hasAdd a b` generates paths with the following keys respctively ``` - ⟨HasAdd.add, 4⟩, *, *, *, * - ⟨HasAdd.add, 4⟩, *, *, ⟨a,0⟩, ⟨b,0⟩ + ⟨Add.add, 4⟩, *, *, *, * + ⟨Add.add, 4⟩, *, *, ⟨a,0⟩, ⟨b,0⟩ ``` + That is, we don't reduce `Add.add Nat inst a b` into `Nat.add a b`. We say the `Add.add` applications are the de-facto canonical forms in the metaprogramming framework. @@ -61,7 +62,7 @@ def Key.lt : Key → Key → Bool | Key.const n₁ a₁, Key.const n₂ a₂ => Name.quickLt n₁ n₂ || (n₁ == n₂ && a₁ < a₂) | k₁, k₂ => k₁.ctorIdx < k₂.ctorIdx -instance : HasLess Key := ⟨fun a b => Key.lt a b⟩ +instance : Less Key := ⟨fun a b => Key.lt a b⟩ instance (a b : Key) : Decidable (a < b) := inferInstanceAs (Decidable (Key.lt a b)) def Key.format : Key → Format @@ -96,7 +97,7 @@ instance {α} : Inhabited (DiscrTree α) := ⟨{}⟩ - We ignore proofs because of proof irrelevance. It doesn't make sense to try to index their structure. - - We ignore instance implicit arguments (e.g., `[HasAdd α]`) because they are "morally" canonical. + - We ignore instance implicit arguments (e.g., `[Add α]`) because they are "morally" canonical. Moreover, we may have many definitionally equal terms floating around. Example: `Ring.hasAdd Int Int.isRing` and `Int.hasAdd`. @@ -206,10 +207,10 @@ private partial def createNodes {α} (keys : Array Key) (v : α) (i : Nat) : Tri else Trie.node #[v] #[] -private def insertVal {α} [HasBeq α] (vs : Array α) (v : α) : Array α := +private def insertVal {α} [BEq α] (vs : Array α) (v : α) : Array α := if vs.contains v then vs else vs.push v -private partial def insertAux {α} [HasBeq α] (keys : Array Key) (v : α) : Nat → Trie α → Trie α +private partial def insertAux {α} [BEq α] (keys : Array Key) (v : α) : Nat → Trie α → Trie α | i, Trie.node vs cs => if h : i < keys.size then let k := keys.get ⟨i, h⟩ @@ -222,7 +223,7 @@ private partial def insertAux {α} [HasBeq α] (keys : Array Key) (v : α) : Nat else Trie.node (insertVal vs v) cs -def insertCore {α} [HasBeq α] (d : DiscrTree α) (keys : Array Key) (v : α) : DiscrTree α := +def insertCore {α} [BEq α] (d : DiscrTree α) (keys : Array Key) (v : α) : DiscrTree α := if keys.isEmpty then panic! "invalid key sequence" else let k := keys[0] @@ -234,7 +235,7 @@ def insertCore {α} [HasBeq α] (d : DiscrTree α) (keys : Array Key) (v : α) : let c := insertAux keys v 1 c { root := d.root.insert k c } -def insert {α} [HasBeq α] (d : DiscrTree α) (e : Expr) (v : α) : MetaM (DiscrTree α) := do +def insert {α} [BEq α] (d : DiscrTree α) (e : Expr) (v : α) : MetaM (DiscrTree α) := do let keys ← mkPath e pure $ d.insertCore keys v @@ -278,9 +279,9 @@ private def getKeyArgs (e : Expr) (isMatch? : Bool) : MetaM (Key × Array Expr) we may want to notify the caller that the TC problem may be solveable later after it assigns `?m`. The method `DiscrTree.getUnify e` returns candidates `c` that may "unify" with `e`. - That is, `isDefEq c e` may return true. Now, consider `DiscrTree.getUnify d (HasAdd ?m)` + That is, `isDefEq c e` may return true. Now, consider `DiscrTree.getUnify d (Add ?m)` where `?m` is a read-only metavariable, and the discrimination tree contains the keys - `HadAdd Nat` and `HasAdd Int`. If `isDefEqStuckEx` is set to true, we must treat `?m` as + `HadAdd Nat` and `Add Int`. If `isDefEqStuckEx` is set to true, we must treat `?m` as a regular metavariable here, otherwise we return the empty set of candidates. This is incorrect because it is equivalent to saying that there is no solution even if the caller assigns `?m` and try again. -/ diff --git a/stage0/src/Lean/Meta/DiscrTreeTypes.lean b/stage0/src/Lean/Meta/DiscrTreeTypes.lean index 1365276597..74a977b652 100644 --- a/stage0/src/Lean/Meta/DiscrTreeTypes.lean +++ b/stage0/src/Lean/Meta/DiscrTreeTypes.lean @@ -37,7 +37,7 @@ protected def Key.beq : Key → Key → Bool | Key.other, Key.other => true | _, _ => false -instance : HasBeq Key := ⟨Key.beq⟩ +instance : BEq Key := ⟨Key.beq⟩ inductive Trie (α : Type) | node (vs : Array α) (children : Array (Key × Trie α)) : Trie α diff --git a/stage0/src/Lean/Meta/ReduceEval.lean b/stage0/src/Lean/Meta/ReduceEval.lean index f32804644b..73262c2948 100644 --- a/stage0/src/Lean/Meta/ReduceEval.lean +++ b/stage0/src/Lean/Meta/ReduceEval.lean @@ -10,25 +10,22 @@ import Lean.Meta.Offset namespace Lean.Meta -class HasReduceEval (α : Type) := - (reduceEval : Expr → MetaM α) - class ReduceEval (α : Type) := (reduceEval : Expr → MetaM α) -def reduceEval {α : Type} [HasReduceEval α] (e : Expr) : MetaM α := +def reduceEval {α : Type} [ReduceEval α] (e : Expr) : MetaM α := withAtLeastTransparency TransparencyMode.default $ - HasReduceEval.reduceEval e + ReduceEval.reduceEval e private def throwFailedToEval {α} (e : Expr) : MetaM α := throwError! "reduceEval: failed to evaluate argument{indentExpr e}" -instance : HasReduceEval Nat := ⟨fun e => do +instance : ReduceEval Nat := ⟨fun e => do let e ← whnf e let some n ← pure $ evalNat e | throwFailedToEval e pure n⟩ -instance {α : Type} [HasReduceEval α] : HasReduceEval (Option α) := ⟨fun e => do +instance {α : Type} [ReduceEval α] : ReduceEval (Option α) := ⟨fun e => do let e ← whnf e let Expr.const c .. ← pure e.getAppFn | throwFailedToEval e let nargs := e.getAppNumArgs @@ -36,7 +33,7 @@ instance {α : Type} [HasReduceEval α] : HasReduceEval (Option α) := ⟨fun e else if c == `Option.some && nargs == 1 then some <$> reduceEval e.appArg! else throwFailedToEval e⟩ -instance : HasReduceEval String := ⟨fun e => do +instance : ReduceEval String := ⟨fun e => do let Expr.lit (Literal.strVal s) _ ← whnf e | throwFailedToEval e pure s⟩ @@ -56,6 +53,6 @@ private partial def evalName (e : Expr) : MetaM Name := do else throwFailedToEval e -instance : HasReduceEval Name := ⟨evalName⟩ +instance : ReduceEval Name := ⟨evalName⟩ end Lean.Meta diff --git a/stage0/src/Lean/Meta/TransparencyMode.lean b/stage0/src/Lean/Meta/TransparencyMode.lean index 8d17a39da3..22f602b8d6 100644 --- a/stage0/src/Lean/Meta/TransparencyMode.lean +++ b/stage0/src/Lean/Meta/TransparencyMode.lean @@ -17,7 +17,7 @@ def beq : TransparencyMode → TransparencyMode → Bool | reducible, reducible => true | _, _ => false -instance : HasBeq TransparencyMode := ⟨beq⟩ +instance : BEq TransparencyMode := ⟨beq⟩ def hash : TransparencyMode → USize | all => 7 diff --git a/stage0/src/Lean/MetavarContext.lean b/stage0/src/Lean/MetavarContext.lean index aaf930193c..08cc8a6dbf 100644 --- a/stage0/src/Lean/MetavarContext.lean +++ b/stage0/src/Lean/MetavarContext.lean @@ -17,14 +17,14 @@ the requirements imposed by these modules. - We may invoke TC while executing `isDefEq`. We need this feature to be able to solve unification problems such as: ``` -f ?a (ringHasAdd ?s) ?x ?y =?= f Int intHasAdd n m +f ?a (ringAdd ?s) ?x ?y =?= f Int intAdd n m ``` where `(?a : Type) (?s : Ring ?a) (?x ?y : ?a)` During `isDefEq` (i.e., unification), it will need to solve the constrain ``` -ringHasAdd ?s =?= intHasAdd +ringAdd ?s =?= intAdd ``` -We say `ringHasAdd ?s` is stuck because it cannot be reduced until we +We say `ringAdd ?s` is stuck because it cannot be reduced until we synthesize the term `?s : Ring ?a` using TC. This can be done since we have assigned `?a := Int` when solving `?a =?= Int`. @@ -227,7 +227,7 @@ abbrev LocalInstances := Array LocalInstance def LocalInstance.beq (i₁ i₂ : LocalInstance) : Bool := i₁.fvar == i₂.fvar -instance : HasBeq LocalInstance := ⟨LocalInstance.beq⟩ +instance : BEq LocalInstance := ⟨LocalInstance.beq⟩ /-- Remove local instance with the given `fvarId`. Do nothing if `localInsts` does not contain any free variable with id `fvarId`. -/ def LocalInstances.erase (localInsts : LocalInstances) (fvarId : FVarId) : LocalInstances := diff --git a/stage0/src/Lean/Parser/Basic.lean b/stage0/src/Lean/Parser/Basic.lean index c24ff6b8fb..2bf7d6c6c5 100644 --- a/stage0/src/Lean/Parser/Basic.lean +++ b/stage0/src/Lean/Parser/Basic.lean @@ -158,7 +158,7 @@ instance : ToString Error := ⟨Error.toString⟩ protected def beq (e₁ e₂ : Error) : Bool := e₁.unexpected == e₂.unexpected && e₁.expected == e₂.expected -instance : HasBeq Error := ⟨Error.beq⟩ +instance : BEq Error := ⟨Error.beq⟩ def merge (e₁ e₂ : Error) : Error := match e₂ with @@ -335,7 +335,7 @@ abbrev TrailingParser := Parser fn := andthenFn p.fn q.fn } -instance : HasAndthen Parser := ⟨andthen⟩ +instance : AndThen Parser := ⟨andthen⟩ @[inline] def nodeFn (n : SyntaxNodeKind) (p : ParserFn) : ParserFn := fun c s => let iniSz := s.stackSize @@ -461,7 +461,7 @@ def orelseFnCore (p q : ParserFn) (mergeErrors : Bool) : ParserFn := fun c s => fn := orelseFn p.fn q.fn } -instance : HasOrelse Parser := ⟨orelse⟩ +instance : OrElse Parser := ⟨orelse⟩ @[noinline] def noFirstTokenInfo (info : ParserInfo) : ParserInfo := { collectTokens := info.collectTokens, @@ -1407,7 +1407,7 @@ def insert {α : Type} (map : TokenMap α) (k : Name) (v : α) : TokenMap α := instance {α : Type} : Inhabited (TokenMap α) := ⟨RBMap.empty⟩ -instance {α : Type} : HasEmptyc (TokenMap α) := ⟨RBMap.empty⟩ +instance {α : Type} : EmptyCollection (TokenMap α) := ⟨RBMap.empty⟩ end TokenMap diff --git a/stage0/src/Lean/ParserCompiler.lean b/stage0/src/Lean/ParserCompiler.lean index c828b2dbeb..240207037b 100644 --- a/stage0/src/Lean/ParserCompiler.lean +++ b/stage0/src/Lean/ParserCompiler.lean @@ -86,7 +86,7 @@ match e with setEnv $ ctx.combinatorAttr.setDeclFor env c c' mkCall c' else - -- if this is a generic function, e.g. `HasAndthen.andthen`, it's easier to just unfold it until we are + -- if this is a generic function, e.g. `AndThen.andthen`, it's easier to just unfold it until we are -- back to parser combinators let some e' ← unfoldDefinition? e | throwError! "don't know how to generate {ctx.varName} for non-parser combinator '{e}'" diff --git a/stage0/src/Lean/PrettyPrinter/Formatter.lean b/stage0/src/Lean/PrettyPrinter/Formatter.lean index 84cf8f9db9..6db8729b80 100644 --- a/stage0/src/Lean/PrettyPrinter/Formatter.lean +++ b/stage0/src/Lean/PrettyPrinter/Formatter.lean @@ -46,7 +46,7 @@ abbrev FormatterM := ReaderT Formatter.Context $ StateRefT Formatter.State CoreM p₁ (fun _ => do set s; p₂) -instance {α} : HasOrelse (FormatterM α) := ⟨FormatterM.orelse⟩ +instance {α} : OrElse (FormatterM α) := ⟨FormatterM.orelse⟩ abbrev Formatter := FormatterM Unit diff --git a/stage0/src/Lean/PrettyPrinter/Parenthesizer.lean b/stage0/src/Lean/PrettyPrinter/Parenthesizer.lean index 14f1729ab5..2d51f0fe85 100644 --- a/stage0/src/Lean/PrettyPrinter/Parenthesizer.lean +++ b/stage0/src/Lean/PrettyPrinter/Parenthesizer.lean @@ -109,7 +109,7 @@ abbrev Parenthesizer := ParenthesizerM Unit p₁ (fun _ => do set s; p₂) -instance {α} : HasOrelse (ParenthesizerM α) := ⟨ParenthesizerM.orelse⟩ +instance {α} : OrElse (ParenthesizerM α) := ⟨ParenthesizerM.orelse⟩ unsafe def mkParenthesizerAttribute : IO (KeyedDeclsAttribute Parenthesizer) := KeyedDeclsAttribute.init { diff --git a/stage0/src/Lean/Server.lean b/stage0/src/Lean/Server.lean index 77f56064c8..63999a5726 100644 --- a/stage0/src/Lean/Server.lean +++ b/stage0/src/Lean/Server.lean @@ -97,16 +97,16 @@ def updateOpenDocuments (key : DocumentUri) (val : EditableDocument) : ServerM U def readLspMessage : ServerM JsonRpc.Message := fun st => Lsp.readLspMessage st.hIn -def readLspRequestAs (expectedMethod : String) (α : Type) [HasFromJson α] : ServerM (Request α) := fun st => +def readLspRequestAs (expectedMethod : String) (α : Type) [FromJson α] : ServerM (Request α) := fun st => Lsp.readLspRequestAs st.hIn expectedMethod α -def readLspNotificationAs (expectedMethod : String) (α : Type) [HasFromJson α] : ServerM α := fun st => +def readLspNotificationAs (expectedMethod : String) (α : Type) [FromJson α] : ServerM α := fun st => Lsp.readLspNotificationAs st.hIn expectedMethod α -def writeLspNotification {α : Type} [HasToJson α] (method : String) (params : α) : ServerM Unit := fun st => +def writeLspNotification {α : Type} [ToJson α] (method : String) (params : α) : ServerM Unit := fun st => Lsp.writeLspNotification st.hOut method params -def writeLspResponse {α : Type} [HasToJson α] (id : RequestID) (params : α) : ServerM Unit := fun st => +def writeLspResponse {α : Type} [ToJson α] (id : RequestID) (params : α) : ServerM Unit := fun st => Lsp.writeLspResponse st.hOut id params /-- Clears diagnostics for the document version 'version'. -/ @@ -172,13 +172,13 @@ def handleDidClose (p : DidCloseTextDocumentParams) : ServerM Unit := fun st => def handleHover (p : HoverParams) : ServerM Json := pure Json.null -def parseParams (paramType : Type) [HasFromJson paramType] (params : Json) : ServerM paramType := +def parseParams (paramType : Type) [FromJson paramType] (params : Json) : ServerM paramType := match fromJson? params with | some parsed => pure parsed | none => throw (userError "got param with wrong structure") def handleNotification (method : String) (params : Json) : ServerM Unit := do - let h := (fun paramType [HasFromJson paramType] (handler : paramType → ServerM Unit) => + let h := (fun paramType [FromJson paramType] (handler : paramType → ServerM Unit) => parseParams paramType params >>= handler) match method with | "textDocument/didOpen" => h DidOpenTextDocumentParams handleDidOpen @@ -188,7 +188,7 @@ def handleNotification (method : String) (params : Json) : ServerM Unit := do | _ => throw (userError "got unsupported notification method") def handleRequest (id : RequestID) (method : String) (params : Json) : ServerM Unit := do - let h := (fun paramType responseType [HasFromJson paramType] [HasToJson responseType] + let h := (fun paramType responseType [FromJson paramType] [ToJson responseType] (handler : paramType → ServerM responseType) => parseParams paramType params >>= handler >>= writeLspResponse id) match method with diff --git a/stage0/src/Lean/Syntax.lean b/stage0/src/Lean/Syntax.lean index 22fd3eb69d..60316a8c0e 100644 --- a/stage0/src/Lean/Syntax.lean +++ b/stage0/src/Lean/Syntax.lean @@ -331,7 +331,7 @@ partial def structEq : Syntax → Syntax → Bool | Syntax.ident _ rawVal val preresolved, Syntax.ident _ rawVal' val' preresolved' => rawVal == rawVal' && val == val' && preresolved == preresolved' | _, _ => false -instance : HasBeq Lean.Syntax := ⟨structEq⟩ +instance : BEq Lean.Syntax := ⟨structEq⟩ /-- Represents a cursor into a syntax tree that can be read, written, and advanced down/up/left/right. diff --git a/stage0/src/Lean/Util/MonadCache.lean b/stage0/src/Lean/Util/MonadCache.lean index 319de8d267..eb3d12b783 100644 --- a/stage0/src/Lean/Util/MonadCache.lean +++ b/stage0/src/Lean/Util/MonadCache.lean @@ -33,30 +33,30 @@ open Std (HashMap) /-- 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 α] := +class MonadHashMapCacheAdapter (α β : Type) (m : Type → Type) [BEq α] [Hashable α] := (getCache : m (HashMap α β)) (modifyCache : (HashMap α β → HashMap α β) → m Unit) namespace MonadHashMapCacheAdapter -@[inline] def findCached? {α β : Type} {m : Type → Type} [HasBeq α] [Hashable α] [Monad m] [MonadHashMapCacheAdapter α β m] (a : α) : m (Option β) := do +@[inline] def findCached? {α β : Type} {m : Type → Type} [BEq α] [Hashable α] [Monad m] [MonadHashMapCacheAdapter α β m] (a : α) : m (Option β) := do let c ← getCache pure (c.find? a) -@[inline] def cache {α β : Type} {m : Type → Type} [HasBeq α] [Hashable α] [MonadHashMapCacheAdapter α β m] (a : α) (b : β) : m Unit := +@[inline] def cache {α β : Type} {m : Type → Type} [BEq α] [Hashable α] [MonadHashMapCacheAdapter α β m] (a : α) (b : β) : m Unit := modifyCache fun s => s.insert a b -instance {α β : Type} {m : Type → Type} [HasBeq α] [Hashable α] [Monad m] [MonadHashMapCacheAdapter α β m] : MonadCache α β m := +instance {α β : Type} {m : Type → Type} [BEq α] [Hashable α] [Monad m] [MonadHashMapCacheAdapter α β m] : MonadCache α β m := { findCached? := MonadHashMapCacheAdapter.findCached?, cache := MonadHashMapCacheAdapter.cache } end MonadHashMapCacheAdapter -def MonadCacheT {ω} (α β : Type) (m : Type → Type) [STWorld ω m] [HasBeq α] [Hashable α] := StateRefT (HashMap α β) m +def MonadCacheT {ω} (α β : Type) (m : Type → Type) [STWorld ω m] [BEq α] [Hashable α] := StateRefT (HashMap α β) m namespace MonadCacheT -variables {ω α β : Type} {m : Type → Type} [STWorld ω m] [HasBeq α] [Hashable α] [MonadLiftT (ST ω) m] [Monad m] +variables {ω α β : Type} {m : Type → Type} [STWorld ω m] [BEq α] [Hashable α] [MonadLiftT (ST ω) m] [Monad m] instance : MonadHashMapCacheAdapter α β (MonadCacheT α β m) := { getCache := (get : StateRefT' ..), diff --git a/stage0/src/Lean/Util/SCC.lean b/stage0/src/Lean/Util/SCC.lean index ca0ef010f8..1775b4b564 100644 --- a/stage0/src/Lean/Util/SCC.lean +++ b/stage0/src/Lean/Util/SCC.lean @@ -14,7 +14,7 @@ namespace Lean.SCC open Std section -variables (α : Type) [HasBeq α] [Hashable α] +variables (α : Type) [BEq α] [Hashable α] structure Data := (index? : Option Nat := none) @@ -30,7 +30,7 @@ structure State := abbrev M := StateM (State α) end -variables {α : Type} [HasBeq α] [Hashable α] +variables {α : Type} [BEq α] [Hashable α] private def getDataOf (a : α) : M α Data := do let s ← get diff --git a/stage0/src/Std/Data/AssocList.lean b/stage0/src/Std/Data/AssocList.lean index 00deeb9296..453292b524 100644 --- a/stage0/src/Std/Data/AssocList.lean +++ b/stage0/src/Std/Data/AssocList.lean @@ -17,7 +17,7 @@ variables {α : Type u} {β : Type v} {δ : Type w} {m : Type w → Type w} [Mon abbrev empty : AssocList α β := nil -instance : HasEmptyc (AssocList α β) := ⟨empty⟩ +instance : EmptyCollection (AssocList α β) := ⟨empty⟩ abbrev insert (m : AssocList α β) (k : α) (v : β) : AssocList α β := m.cons k v @@ -41,29 +41,29 @@ def mapVal (f : β → δ) : AssocList α β → AssocList α δ | nil => nil | cons k v t => cons k (f v) (mapVal f t) -def findEntry? [HasBeq α] (a : α) : AssocList α β → Option (α × β) +def findEntry? [BEq α] (a : α) : AssocList α β → Option (α × β) | nil => none | cons k v es => match k == a with | true => some (k, v) | false => findEntry? a es -def find? [HasBeq α] (a : α) : AssocList α β → Option β +def find? [BEq α] (a : α) : AssocList α β → Option β | nil => none | cons k v es => match k == a with | true => some v | false => find? a es -def contains [HasBeq α] (a : α) : AssocList α β → Bool +def contains [BEq α] (a : α) : AssocList α β → Bool | nil => false | cons k v es => k == a || contains a es -def replace [HasBeq α] (a : α) (b : β) : AssocList α β → AssocList α β +def replace [BEq α] (a : α) (b : β) : AssocList α β → AssocList α β | nil => nil | cons k v es => match k == a with | true => cons a b es | false => cons k v (replace a b es) -def erase [HasBeq α] (a : α) : AssocList α β → AssocList α β +def erase [BEq α] (a : α) : AssocList α β → AssocList α β | nil => nil | cons k v es => match k == a with | true => es diff --git a/stage0/src/Std/Data/DList.lean b/stage0/src/Std/Data/DList.lean index 6cf4fe0a4d..a794e63d2f 100644 --- a/stage0/src/Std/Data/DList.lean +++ b/stage0/src/Std/Data/DList.lean @@ -20,12 +20,12 @@ variables {α : Type u} open List def ofList (l : List α) : DList α := -⟨HasAppend.append l, fun t => by rw appendNil; exact rfl⟩ +⟨Append.append l, fun t => by rw appendNil; exact rfl⟩ def empty : DList α := ⟨id, fun t => rfl⟩ -instance : HasEmptyc (DList α) := +instance : EmptyCollection (DList α) := ⟨DList.empty⟩ def toList : DList α → List α @@ -61,7 +61,7 @@ def push : DList α → α → DList α rw [h [a], h (a::t), appendAssoc (f []) [a] t] exact rfl⟩ -instance : HasAppend (DList α) := +instance : Append (DList α) := ⟨DList.append⟩ end DList diff --git a/stage0/src/Std/Data/HashMap.lean b/stage0/src/Std/Data/HashMap.lean index 837245d06d..6ce71ca45e 100644 --- a/stage0/src/Std/Data/HashMap.lean +++ b/stage0/src/Std/Data/HashMap.lean @@ -53,19 +53,19 @@ foldBucketsM h.buckets d f @[inline] def fold {δ : Type w} (f : δ → α → β → δ) (d : δ) (m : HashMapImp α β) : δ := foldBuckets m.buckets d f -def findEntry? [HasBeq α] [Hashable α] (m : HashMapImp α β) (a : α) : Option (α × β) := +def findEntry? [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : Option (α × β) := match m with | ⟨_, buckets⟩ => let ⟨i, h⟩ := mkIdx buckets.property (hash a) (buckets.val.uget i h).findEntry? a -def find? [HasBeq α] [Hashable α] (m : HashMapImp α β) (a : α) : Option β := +def find? [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : Option β := match m with | ⟨_, buckets⟩ => let ⟨i, h⟩ := mkIdx buckets.property (hash a) (buckets.val.uget i h).find? a -def contains [HasBeq α] [Hashable α] (m : HashMapImp α β) (a : α) : Bool := +def contains [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : Bool := match m with | ⟨_, buckets⟩ => let ⟨i, h⟩ := mkIdx buckets.property (hash a) @@ -92,7 +92,7 @@ let new_buckets : HashMapBucket α β := ⟨mkArray nbuckets AssocList.nil, this { size := size, buckets := moveEntries 0 buckets.val new_buckets } -def insert [HasBeq α] [Hashable α] (m : HashMapImp α β) (a : α) (b : β) : HashMapImp α β := +def insert [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) (b : β) : HashMapImp α β := match m with | ⟨size, buckets⟩ => let ⟨i, h⟩ := mkIdx buckets.property (hash a) @@ -106,7 +106,7 @@ match m with then { size := size', buckets := buckets' } else expand size' buckets' -def erase [HasBeq α] [Hashable α] (m : HashMapImp α β) (a : α) : HashMapImp α β := +def erase [BEq α] [Hashable α] (m : HashMapImp α β) (a : α) : HashMapImp α β := match m with | ⟨ size, buckets ⟩ => let ⟨i, h⟩ := mkIdx buckets.property (hash a) @@ -114,28 +114,28 @@ match m with if bkt.contains a then ⟨size - 1, buckets.update i (bkt.erase a) h⟩ else m -inductive WellFormed [HasBeq α] [Hashable α] : HashMapImp α β → Prop +inductive WellFormed [BEq α] [Hashable α] : HashMapImp α β → Prop | mkWff : ∀ n, WellFormed (mkHashMapImp n) | insertWff : ∀ m a b, WellFormed m → WellFormed (insert m a b) | eraseWff : ∀ m a, WellFormed m → WellFormed (erase m a) end HashMapImp -def HashMap (α : Type u) (β : Type v) [HasBeq α] [Hashable α] := +def HashMap (α : Type u) (β : Type v) [BEq α] [Hashable α] := { m : HashMapImp α β // m.WellFormed } open Std.HashMapImp -def mkHashMap {α : Type u} {β : Type v} [HasBeq α] [Hashable α] (nbuckets := 8) : HashMap α β := +def mkHashMap {α : Type u} {β : Type v} [BEq α] [Hashable α] (nbuckets := 8) : HashMap α β := ⟨ mkHashMapImp nbuckets, WellFormed.mkWff nbuckets ⟩ namespace HashMap -variables {α : Type u} {β : Type v} [HasBeq α] [Hashable α] +variables {α : Type u} {β : Type v} [BEq α] [Hashable α] instance inhabited : Inhabited (HashMap α β) := ⟨mkHashMap⟩ -instance hasEmptyc : HasEmptyc (HashMap α β) := +instance hasEmptyc : EmptyCollection (HashMap α β) := ⟨mkHashMap⟩ @[inline] def insert (m : HashMap α β) (a : α) (b : β) : HashMap α β := diff --git a/stage0/src/Std/Data/HashSet.lean b/stage0/src/Std/Data/HashSet.lean index a2576c7930..c20cc19571 100644 --- a/stage0/src/Std/Data/HashSet.lean +++ b/stage0/src/Std/Data/HashSet.lean @@ -52,13 +52,13 @@ foldBucketsM h.buckets d f @[inline] def fold {δ : Type w} (f : δ → α → δ) (d : δ) (m : HashSetImp α) : δ := foldBuckets m.buckets d f -def find? [HasBeq α] [Hashable α] (m : HashSetImp α) (a : α) : Option α := +def find? [BEq α] [Hashable α] (m : HashSetImp α) (a : α) : Option α := match m with | ⟨_, buckets⟩ => let ⟨i, h⟩ := mkIdx buckets.property (hash a) (buckets.val.uget i h).find? (fun a' => a == a') -def contains [HasBeq α] [Hashable α] (m : HashSetImp α) (a : α) : Bool := +def contains [BEq α] [Hashable α] (m : HashSetImp α) (a : α) : Bool := match m with | ⟨_, buckets⟩ => let ⟨i, h⟩ := mkIdx buckets.property (hash a) @@ -85,7 +85,7 @@ let new_buckets : HashSetBucket α := ⟨mkArray nbuckets [], this⟩; { size := size, buckets := moveEntries 0 buckets.val new_buckets } -def insert [HasBeq α] [Hashable α] (m : HashSetImp α) (a : α) : HashSetImp α := +def insert [BEq α] [Hashable α] (m : HashSetImp α) (a : α) : HashSetImp α := match m with | ⟨size, buckets⟩ => let ⟨i, h⟩ := mkIdx buckets.property (hash a) @@ -99,7 +99,7 @@ match m with then { size := size', buckets := buckets' } else expand size' buckets' -def erase [HasBeq α] [Hashable α] (m : HashSetImp α) (a : α) : HashSetImp α := +def erase [BEq α] [Hashable α] (m : HashSetImp α) (a : α) : HashSetImp α := match m with | ⟨ size, buckets ⟩ => let ⟨i, h⟩ := mkIdx buckets.property (hash a) @@ -107,28 +107,28 @@ match m with if bkt.contains a then ⟨size - 1, buckets.update i (bkt.erase a) h⟩ else m -inductive WellFormed [HasBeq α] [Hashable α] : HashSetImp α → Prop +inductive WellFormed [BEq α] [Hashable α] : HashSetImp α → Prop | mkWff : ∀ n, WellFormed (mkHashSetImp n) | insertWff : ∀ m a, WellFormed m → WellFormed (insert m a) | eraseWff : ∀ m a, WellFormed m → WellFormed (erase m a) end HashSetImp -def HashSet (α : Type u) [HasBeq α] [Hashable α] := +def HashSet (α : Type u) [BEq α] [Hashable α] := { m : HashSetImp α // m.WellFormed } open HashSetImp -def mkHashSet {α : Type u} [HasBeq α] [Hashable α] (nbuckets := 8) : HashSet α := +def mkHashSet {α : Type u} [BEq α] [Hashable α] (nbuckets := 8) : HashSet α := ⟨ mkHashSetImp nbuckets, WellFormed.mkWff nbuckets ⟩ namespace HashSet -variables {α : Type u} [HasBeq α] [Hashable α] +variables {α : Type u} [BEq α] [Hashable α] instance : Inhabited (HashSet α) := ⟨mkHashSet⟩ -instance : HasEmptyc (HashSet α) := +instance : EmptyCollection (HashSet α) := ⟨mkHashSet⟩ @[inline] def insert (m : HashSet α) (a : α) : HashSet α := diff --git a/stage0/src/Std/Data/PersistentArray.lean b/stage0/src/Std/Data/PersistentArray.lean index c9ed9d910f..0f9389c540 100644 --- a/stage0/src/Std/Data/PersistentArray.lean +++ b/stage0/src/Std/Data/PersistentArray.lean @@ -229,7 +229,7 @@ match n with @[specialize] def forIn (t : PersistentArray α) (init : β) (f : α → β → m (ForInStep β)) : m β := do match (← forInAux (inh := ⟨init⟩) f t.root init) with -| ForInStep.done b => b +| ForInStep.done b => pure b | ForInStep.yield b => for v in t.tail do match (← f v b) with @@ -279,7 +279,7 @@ def append (t₁ t₂ : PersistentArray α) : PersistentArray α := if t₁.isEmpty then t₂ else t₂.foldl PersistentArray.push t₁ -instance : HasAppend (PersistentArray α) := ⟨append⟩ +instance : Append (PersistentArray α) := ⟨append⟩ @[inline] def findSome? {β} (t : PersistentArray α) (f : α → (Option β)) : Option β := Id.run (t.findSomeM? f) diff --git a/stage0/src/Std/Data/PersistentHashMap.lean b/stage0/src/Std/Data/PersistentHashMap.lean index 3a7f9ea8d1..52acada563 100644 --- a/stage0/src/Std/Data/PersistentHashMap.lean +++ b/stage0/src/Std/Data/PersistentHashMap.lean @@ -31,21 +31,21 @@ def mkEmptyEntriesArray {α β} : Array (Entry α β (Node α β)) := end PersistentHashMap -structure PersistentHashMap (α : Type u) (β : Type v) [HasBeq α] [Hashable α] := +structure PersistentHashMap (α : Type u) (β : Type v) [BEq α] [Hashable α] := (root : PersistentHashMap.Node α β := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray) (size : Nat := 0) -abbrev PHashMap (α : Type u) (β : Type v) [HasBeq α] [Hashable α] := PersistentHashMap α β +abbrev PHashMap (α : Type u) (β : Type v) [BEq α] [Hashable α] := PersistentHashMap α β namespace PersistentHashMap variables {α : Type u} {β : Type v} -def empty [HasBeq α] [Hashable α] : PersistentHashMap α β := {} +def empty [BEq α] [Hashable α] : PersistentHashMap α β := {} -def isEmpty [HasBeq α] [Hashable α] (m : PersistentHashMap α β) : Bool := +def isEmpty [BEq α] [Hashable α] (m : PersistentHashMap α β) : Bool := m.size == 0 -instance [HasBeq α] [Hashable α] : Inhabited (PersistentHashMap α β) := ⟨{}⟩ +instance [BEq α] [Hashable α] : Inhabited (PersistentHashMap α β) := ⟨{}⟩ def mkEmptyEntries {α β} : Node α β := Node.entries mkEmptyEntriesArray @@ -76,7 +76,7 @@ have h₂ : (vs.push v).size = vs.size + 1 by apply Array.szPushEq have h₃ : ks.size + 1 = vs.size + 1 by rw h; exact rfl (h₁.trans h₃).trans h₂.symm -partial def insertAtCollisionNodeAux [HasBeq α] : CollisionNode α β → Nat → α → β → CollisionNode α β +partial def insertAtCollisionNodeAux [BEq α] : CollisionNode α β → Nat → α → β → CollisionNode α β | n@⟨Node.collision keys vals heq, _⟩, i, k, v => if h : i < keys.size then let idx : Fin keys.size := ⟨i, h⟩; @@ -89,7 +89,7 @@ partial def insertAtCollisionNodeAux [HasBeq α] : CollisionNode α β → Nat ⟨Node.collision (keys.push k) (vals.push v) (pushSizeEq heq k v), IsCollisionNode.mk _ _ _⟩ | ⟨Node.entries _, h⟩, _, _, _ => False.elim (nomatch h) -def insertAtCollisionNode [HasBeq α] : CollisionNode α β → α → β → CollisionNode α β := +def insertAtCollisionNode [BEq α] : CollisionNode α β → α → β → CollisionNode α β := fun n k v => insertAtCollisionNodeAux n 0 k v def getCollisionNodeSize : CollisionNode α β → Nat @@ -103,7 +103,7 @@ let vs : Array β := Array.mkEmpty maxCollisions let vs := (vs.push v₁).push v₂ Node.collision ks vs rfl -partial def insertAux [HasBeq α] [Hashable α] : Node α β → USize → USize → α → β → Node α β +partial def insertAux [BEq α] [Hashable α] : Node α β → USize → USize → α → β → Node α β | Node.collision keys vals heq, _, depth, k, v => let newNode := insertAtCollisionNode ⟨Node.collision keys vals heq, IsCollisionNode.mk _ _ _⟩ k v if depth >= maxDepth || getCollisionNodeSize newNode < maxCollisions then newNode.val @@ -130,10 +130,10 @@ partial def insertAux [HasBeq α] [Hashable α] : Node α β → USize → USize if k == k' then Entry.entry k v else Entry.ref $ mkCollisionNode k' v' k v -def insert [HasBeq α] [Hashable α] : PersistentHashMap α β → α → β → PersistentHashMap α β +def insert [BEq α] [Hashable α] : PersistentHashMap α β → α → β → PersistentHashMap α β | { root := n, size := sz }, k, v => { root := insertAux n (hash k) 1 k v, size := sz + 1 } -partial def findAtAux [HasBeq α] (keys : Array α) (vals : Array β) (heq : keys.size = vals.size) : Nat → α → Option β +partial def findAtAux [BEq α] (keys : Array α) (vals : Array β) (heq : keys.size = vals.size) : Nat → α → Option β | i, k => if h : i < keys.size then let k' := keys.get ⟨i, h⟩ @@ -141,7 +141,7 @@ partial def findAtAux [HasBeq α] (keys : Array α) (vals : Array β) (heq : key else findAtAux keys vals heq (i+1) k else none -partial def findAux [HasBeq α] : Node α β → USize → α → Option β +partial def findAux [BEq α] : Node α β → USize → α → Option β | Node.entries entries, h, k => let j := (mod2Shift h shift).toNat match entries.get! j with @@ -150,21 +150,21 @@ partial def findAux [HasBeq α] : Node α β → USize → α → Option β | Entry.entry k' v => if k == k' then some v else none | Node.collision keys vals heq, _, k => findAtAux keys vals heq 0 k -def find? [HasBeq α] [Hashable α] : PersistentHashMap α β → α → Option β +def find? [BEq α] [Hashable α] : PersistentHashMap α β → α → Option β | { root := n, .. }, k => findAux n (hash k) k -@[inline] def getOp [HasBeq α] [Hashable α] (self : PersistentHashMap α β) (idx : α) : Option β := +@[inline] def getOp [BEq α] [Hashable α] (self : PersistentHashMap α β) (idx : α) : Option β := self.find? idx -@[inline] def findD [HasBeq α] [Hashable α] (m : PersistentHashMap α β) (a : α) (b₀ : β) : β := +@[inline] def findD [BEq α] [Hashable α] (m : PersistentHashMap α β) (a : α) (b₀ : β) : β := (m.find? a).getD b₀ -@[inline] def find! [HasBeq α] [Hashable α] [Inhabited β] (m : PersistentHashMap α β) (a : α) : β := +@[inline] def find! [BEq α] [Hashable α] [Inhabited β] (m : PersistentHashMap α β) (a : α) : β := match m.find? a with | some b => b | none => panic! "key is not in the map" -partial def findEntryAtAux [HasBeq α] (keys : Array α) (vals : Array β) (heq : keys.size = vals.size) : Nat → α → Option (α × β) +partial def findEntryAtAux [BEq α] (keys : Array α) (vals : Array β) (heq : keys.size = vals.size) : Nat → α → Option (α × β) | i, k => if h : i < keys.size then let k' := keys.get ⟨i, h⟩ @@ -172,7 +172,7 @@ partial def findEntryAtAux [HasBeq α] (keys : Array α) (vals : Array β) (heq else findEntryAtAux keys vals heq (i+1) k else none -partial def findEntryAux [HasBeq α] : Node α β → USize → α → Option (α × β) +partial def findEntryAux [BEq α] : Node α β → USize → α → Option (α × β) | Node.entries entries, h, k => let j := (mod2Shift h shift).toNat match entries.get! j with @@ -181,10 +181,10 @@ partial def findEntryAux [HasBeq α] : Node α β → USize → α → Option ( | Entry.entry k' v => if k == k' then some (k', v) else none | Node.collision keys vals heq, _, k => findEntryAtAux keys vals heq 0 k -def findEntry? [HasBeq α] [Hashable α] : PersistentHashMap α β → α → Option (α × β) +def findEntry? [BEq α] [Hashable α] : PersistentHashMap α β → α → Option (α × β) | { root := n, .. }, k => findEntryAux n (hash k) k -partial def containsAtAux [HasBeq α] (keys : Array α) (vals : Array β) (heq : keys.size = vals.size) : Nat → α → Bool +partial def containsAtAux [BEq α] (keys : Array α) (vals : Array β) (heq : keys.size = vals.size) : Nat → α → Bool | i, k => if h : i < keys.size then let k' := keys.get ⟨i, h⟩ @@ -192,7 +192,7 @@ partial def containsAtAux [HasBeq α] (keys : Array α) (vals : Array β) (heq : else containsAtAux keys vals heq (i+1) k else false -partial def containsAux [HasBeq α] : Node α β → USize → α → Bool +partial def containsAux [BEq α] : Node α β → USize → α → Bool | Node.entries entries, h, k => let j := (mod2Shift h shift).toNat match entries.get! j with @@ -201,7 +201,7 @@ partial def containsAux [HasBeq α] : Node α β → USize → α → Bool | Entry.entry k' v => k == k' | Node.collision keys vals heq, _, k => containsAtAux keys vals heq 0 k -def contains [HasBeq α] [Hashable α] : PersistentHashMap α β → α → Bool +def contains [BEq α] [Hashable α] : PersistentHashMap α β → α → Bool | { root := n, .. }, k => containsAux n (hash k) k partial def isUnaryEntries (a : Array (Entry α β (Node α β))) : Nat → Option (α × β) → Option (α × β) @@ -225,7 +225,7 @@ def isUnaryNode : Node α β → Option (α × β) else none -partial def eraseAux [HasBeq α] : Node α β → USize → α → Node α β × Bool +partial def eraseAux [BEq α] : Node α β → USize → α → Node α β × Bool | n@(Node.collision keys vals heq), _, k => match keys.indexOf? k with | some idx => @@ -249,7 +249,7 @@ partial def eraseAux [HasBeq α] : Node α β → USize → α → Node α β × | none => (Node.entries (entries.set! j (Entry.ref newNode)), true) | some (k, v) => (Node.entries (entries.set! j (Entry.entry k v)), true) -def erase [HasBeq α] [Hashable α] : PersistentHashMap α β → α → PersistentHashMap α β +def erase [BEq α] [Hashable α] : PersistentHashMap α β → α → PersistentHashMap α β | { root := n, size := sz }, k => let h := hash k let (n, del) := eraseAux n h k @@ -276,17 +276,17 @@ variables {σ : Type w} | Entry.ref node => foldlMAux f node acc) acc -@[specialize] def foldlM [HasBeq α] [Hashable α] (map : PersistentHashMap α β) (f : σ → α → β → m σ) (acc : σ) : m σ := +@[specialize] def foldlM [BEq α] [Hashable α] (map : PersistentHashMap α β) (f : σ → α → β → m σ) (acc : σ) : m σ := foldlMAux f map.root acc -@[specialize] def forM [HasBeq α] [Hashable α] (map : PersistentHashMap α β) (f : α → β → m PUnit) : m PUnit := +@[specialize] def forM [BEq α] [Hashable α] (map : PersistentHashMap α β) (f : α → β → m PUnit) : m PUnit := map.foldlM (fun _ => f) ⟨⟩ -@[specialize] def foldl [HasBeq α] [Hashable α] (map : PersistentHashMap α β) (f : σ → α → β → σ) (acc : σ) : σ := +@[specialize] def foldl [BEq α] [Hashable α] (map : PersistentHashMap α β) (f : σ → α → β → σ) (acc : σ) : σ := Id.run $ map.foldlM f acc end -def toList [HasBeq α] [Hashable α] (m : PersistentHashMap α β) : List (α × β) := +def toList [BEq α] [Hashable α] (m : PersistentHashMap α β) : List (α × β) := m.foldl (fun ps k v => (k, v) :: ps) [] structure Stats := @@ -313,7 +313,7 @@ partial def collectStats : Node α β → Stats → Nat → Stats | Entry.entry _ _ => stats) stats -def stats [HasBeq α] [Hashable α] (m : PersistentHashMap α β) : Stats := +def stats [BEq α] [Hashable α] (m : PersistentHashMap α β) : Stats := collectStats m.root {} 1 def Stats.toString (s : Stats) : String := diff --git a/stage0/src/Std/Data/PersistentHashSet.lean b/stage0/src/Std/Data/PersistentHashSet.lean index ed2947da7d..2eb9831149 100644 --- a/stage0/src/Std/Data/PersistentHashSet.lean +++ b/stage0/src/Std/Data/PersistentHashSet.lean @@ -8,14 +8,14 @@ import Std.Data.PersistentHashMap namespace Std universes u v -structure PersistentHashSet (α : Type u) [HasBeq α] [Hashable α] := +structure PersistentHashSet (α : Type u) [BEq α] [Hashable α] := (set : PersistentHashMap α Unit) -abbrev PHashSet (α : Type u) [HasBeq α] [Hashable α] := PersistentHashSet α +abbrev PHashSet (α : Type u) [BEq α] [Hashable α] := PersistentHashSet α namespace PersistentHashSet -variables {α : Type u} [HasBeq α] [Hashable α] +variables {α : Type u} [BEq α] [Hashable α] @[inline] def isEmpty (s : PersistentHashSet α) : Bool := s.set.isEmpty @@ -26,7 +26,7 @@ s.set.isEmpty instance : Inhabited (PersistentHashSet α) := ⟨empty⟩ -instance : HasEmptyc (PersistentHashSet α) := +instance : EmptyCollection (PersistentHashSet α) := ⟨empty⟩ @[inline] def insert (s : PersistentHashSet α) (a : α) : PersistentHashSet α := diff --git a/stage0/src/Std/Data/RBMap.lean b/stage0/src/Std/Data/RBMap.lean index 73315a2c43..7c6d06c7b0 100644 --- a/stage0/src/Std/Data/RBMap.lean +++ b/stage0/src/Std/Data/RBMap.lean @@ -217,7 +217,7 @@ def RBMap (α : Type u) (β : Type v) (lt : α → α → Bool) : Type (max u v) @[inline] def RBMap.empty {α : Type u} {β : Type v} {lt : α → α → Bool} : RBMap α β lt := mkRBMap .. -instance (α : Type u) (β : Type v) (lt : α → α → Bool) : HasEmptyc (RBMap α β lt) := +instance (α : Type u) (β : Type v) (lt : α → α → Bool) : EmptyCollection (RBMap α β lt) := ⟨RBMap.empty⟩ namespace RBMap diff --git a/stage0/src/Std/Data/RBTree.lean b/stage0/src/Std/Data/RBTree.lean index a7353085a3..fcaae70e79 100644 --- a/stage0/src/Std/Data/RBTree.lean +++ b/stage0/src/Std/Data/RBTree.lean @@ -13,7 +13,7 @@ def RBTree (α : Type u) (lt : α → α → Bool) : Type u := @[inline] def mkRBTree (α : Type u) (lt : α → α → Bool) : RBTree α lt := mkRBMap α Unit lt -instance (α : Type u) (lt : α → α → Bool) : HasEmptyc (RBTree α lt) := +instance (α : Type u) (lt : α → α → Bool) : EmptyCollection (RBTree α lt) := ⟨mkRBTree α lt⟩ namespace RBTree diff --git a/stage0/stdlib/Init/Control/EState.c b/stage0/stdlib/Init/Control/EState.c index 10e00fbf5b..eb448a12a8 100644 --- a/stage0/stdlib/Init/Control/EState.c +++ b/stage0/stdlib/Init/Control/EState.c @@ -21,7 +21,6 @@ lean_object* l_EStateM_run_x27_match__1(lean_object*, lean_object*, lean_object* lean_object* l_EStateM_tryCatch(lean_object*, lean_object*, lean_object*); lean_object* l_EStateM_Init_Control_EState___instance__9_match__3___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_EStateM_Init_Control_EState___instance__5___closed__9; -lean_object* l_EStateM_orelse_x27___rarg(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*); lean_object* l_EStateM_seqRight___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_EStateM_Init_Control_EState___instance__5___closed__6; lean_object* l_EStateM_Init_Control_EState___instance__7___closed__3; @@ -30,7 +29,6 @@ lean_object* l_EStateM_modifyGet_match__1___rarg(lean_object*, lean_object*); lean_object* l_EStateM_Init_Control_EState___instance__9_match__1(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_EStateM_Init_Control_EState___instance__5(lean_object*, lean_object*); lean_object* l_EStateM_run(lean_object*, lean_object*, lean_object*); -lean_object* l_EStateM_orelse_x27_match__1___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_EStateM_seqRight_match__1(lean_object*, lean_object*, lean_object*); lean_object* l_EStateM_fromStateM___rarg(lean_object*, lean_object*); lean_object* l_EStateM_Init_Control_EState___instance__5___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -38,20 +36,21 @@ lean_object* l_EStateM_dummyRestore___rarg(lean_object*, lean_object*); lean_object* l_EStateM_Init_Control_EState___instance__5___lambda__3(lean_object*, lean_object*, lean_object*); lean_object* l_EStateM_bind_match__1___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_EStateM_Init_Control_EState___instance__5___lambda__5(lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_EStateM_orelse_x27_match__1(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_EStateM_dummySave(lean_object*, lean_object*); lean_object* lean_string_append(lean_object*, lean_object*); lean_object* l_EStateM_seqRight_match__1___rarg(lean_object*, lean_object*, lean_object*); +lean_object* l_EStateM_orElse_match__1___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_EStateM_Init_Control_EState___instance__8___rarg(lean_object*); +lean_object* l_EStateM_orElse_x27___rarg(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*); lean_object* l_EStateM_adaptExcept(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_EStateM_Init_Control_EState___instance__9___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_EStateM_dummySave___boxed(lean_object*, lean_object*); lean_object* l_EStateM_dummyRestore(lean_object*); lean_object* l_EStateM_Init_Control_EState___instance__2___rarg(lean_object*, lean_object*, lean_object*); +lean_object* l_EStateM_orElse_match__1(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_EStateM_Init_Control_EState___instance__5___lambda__7(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_EStateM_modifyGet_match__1(lean_object*, lean_object*, lean_object*); lean_object* l_EStateM_adaptExcept_match__1(lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_EStateM_orelse(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_EStateM_map_match__1(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_EStateM_Init_Control_EState___instance__8___rarg___closed__1; lean_object* l_EStateM_dummyRestore___rarg___boxed(lean_object*, lean_object*); @@ -69,13 +68,13 @@ lean_object* l_EStateM_bind___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_EStateM_Init_Control_EState___instance__5___lambda__6(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_EStateM_Init_Control_EState___instance__1(lean_object*, lean_object*, lean_object*); lean_object* l_EStateM_fromStateM_match__1___rarg(lean_object*, lean_object*); -lean_object* l_EStateM_orelse_match__1___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_EStateM_Init_Control_EState___instance__4___rarg(lean_object*, lean_object*); lean_object* l_EStateM_modifyGet___rarg(lean_object*, lean_object*); lean_object* l_EStateM_map(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_EStateM_Init_Control_EState___instance__3(lean_object*, lean_object*, lean_object*); extern lean_object* l_Except_toString___rarg___closed__2; lean_object* l_EStateM_Init_Control_EState___instance__5___closed__10; +lean_object* l_EStateM_orElse_x27___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_EStateM_Init_Control_EState___instance__9(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_EStateM_bind_match__1(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_EStateM_map_match__1___rarg(lean_object*, lean_object*, lean_object*); @@ -83,11 +82,12 @@ lean_object* l_EStateM_Init_Control_EState___instance__9_match__1___rarg(lean_ob lean_object* l_EStateM_modifyGet(lean_object*, lean_object*, lean_object*); lean_object* l_EStateM_nonBacktrackable___closed__1; lean_object* l_EStateM_Init_Control_EState___instance__5___lambda__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_EStateM_orelse_x27_match__2___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_EStateM_nonBacktrackable___closed__2; lean_object* l_EStateM_Init_Control_EState___instance__8___rarg___lambda__1(lean_object*, lean_object*, lean_object*); +lean_object* l_EStateM_orElse_x27_match__2___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_EStateM_Init_Control_EState___instance__7___closed__2; lean_object* l_EStateM_fromStateM(lean_object*, lean_object*, lean_object*); +lean_object* l_EStateM_orElse_x27_match__2(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_EStateM_Init_Control_EState___instance__8___rarg___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_EStateM_seqRight(lean_object*, lean_object*, lean_object*); lean_object* l_EStateM_Init_Control_EState___instance__1_match__1(lean_object*, lean_object*, lean_object*, lean_object*); @@ -101,15 +101,16 @@ lean_object* l_EStateM_Init_Control_EState___instance__1___rarg___closed__2; lean_object* l_EStateM_adaptExcept___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_EStateM_Init_Control_EState___instance__7___closed__4; lean_object* l_EStateM_Init_Control_EState___instance__7(lean_object*, lean_object*); -lean_object* l_EStateM_orelse___rarg(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_EStateM_set(lean_object*, lean_object*); lean_object* l_EStateM_pure(lean_object*, lean_object*, lean_object*); lean_object* l_EStateM_Init_Control_EState___instance__9_match__2(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_EStateM_Init_Control_EState___instance__8(lean_object*, lean_object*, lean_object*); lean_object* l_EStateM_run_x27(lean_object*, lean_object*, lean_object*); lean_object* l_EStateM_Init_Control_EState___instance__9_match__2___rarg(lean_object*, lean_object*, lean_object*); +lean_object* l_EStateM_orElse_x27_match__1___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_EStateM_set___rarg(lean_object*, lean_object*); lean_object* l_EStateM_Init_Control_EState___instance__9_match__3(lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_EStateM_orElse(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_EStateM_Init_Control_EState___instance__3___rarg(lean_object*, lean_object*); lean_object* l_EStateM_Init_Control_EState___instance__5___closed__7; lean_object* l_EStateM_Init_Control_EState___instance__4(lean_object*, lean_object*, lean_object*); @@ -118,7 +119,6 @@ lean_object* l_EStateM_Init_Control_EState___instance__5___closed__3; lean_object* l_EStateM_Init_Control_EState___instance__6___rarg(lean_object*); lean_object* l_EStateM_Init_Control_EState___instance__1_match__1___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_EStateM_Init_Control_EState___instance__7___closed__1; -lean_object* l_EStateM_orelse_x27_match__2(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_EStateM_bind(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_EStateM_throw(lean_object*, lean_object*, lean_object*); lean_object* l_EStateM_Init_Control_EState___instance__2_match__1(lean_object*, lean_object*, lean_object*, lean_object*); @@ -127,11 +127,11 @@ lean_object* l_EStateM_pure___rarg(lean_object*, lean_object*); lean_object* l_EStateM_Init_Control_EState___instance__5___closed__1; lean_object* l_EStateM_Init_Control_EState___instance__2_match__1___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_EStateM_Init_Control_EState___instance__5___closed__2; +lean_object* l_EStateM_orElse_x27(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_EStateM_run_x27_match__1___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_EStateM_Init_Control_EState___instance__5___closed__8; -lean_object* l_EStateM_orelse_x27___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_EStateM_orelse_match__1(lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_EStateM_orelse_x27(lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_EStateM_orElse___rarg(lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_EStateM_orElse_x27_match__1(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_EStateM_tryCatch___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_EStateM_Init_Control_EState___instance__1_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: @@ -542,7 +542,7 @@ x_4 = lean_alloc_closure((void*)(l_EStateM_tryCatch___rarg), 5, 0); return x_4; } } -lean_object* l_EStateM_orelse_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +lean_object* l_EStateM_orElse_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { if (lean_obj_tag(x_1) == 0) @@ -566,15 +566,15 @@ return x_7; } } } -lean_object* l_EStateM_orelse_match__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { +lean_object* l_EStateM_orElse_match__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { _start: { lean_object* x_5; -x_5 = lean_alloc_closure((void*)(l_EStateM_orelse_match__1___rarg), 3, 0); +x_5 = lean_alloc_closure((void*)(l_EStateM_orElse_match__1___rarg), 3, 0); return x_5; } } -lean_object* l_EStateM_orelse___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { +lean_object* l_EStateM_orElse___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { _start: { lean_object* x_5; lean_object* x_6; lean_object* x_7; @@ -605,15 +605,15 @@ return x_11; } } } -lean_object* l_EStateM_orelse(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { +lean_object* l_EStateM_orElse(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { _start: { lean_object* x_5; -x_5 = lean_alloc_closure((void*)(l_EStateM_orelse___rarg), 4, 0); +x_5 = lean_alloc_closure((void*)(l_EStateM_orElse___rarg), 4, 0); return x_5; } } -lean_object* l_EStateM_orelse_x27_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +lean_object* l_EStateM_orElse_x27_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { if (lean_obj_tag(x_1) == 0) @@ -637,15 +637,15 @@ return x_7; } } } -lean_object* l_EStateM_orelse_x27_match__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { +lean_object* l_EStateM_orElse_x27_match__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { _start: { lean_object* x_5; -x_5 = lean_alloc_closure((void*)(l_EStateM_orelse_x27_match__1___rarg), 3, 0); +x_5 = lean_alloc_closure((void*)(l_EStateM_orElse_x27_match__1___rarg), 3, 0); return x_5; } } -lean_object* l_EStateM_orelse_x27_match__2___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +lean_object* l_EStateM_orElse_x27_match__2___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { if (lean_obj_tag(x_1) == 0) @@ -669,15 +669,15 @@ return x_7; } } } -lean_object* l_EStateM_orelse_x27_match__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { +lean_object* l_EStateM_orElse_x27_match__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { _start: { lean_object* x_5; -x_5 = lean_alloc_closure((void*)(l_EStateM_orelse_x27_match__2___rarg), 3, 0); +x_5 = lean_alloc_closure((void*)(l_EStateM_orElse_x27_match__2___rarg), 3, 0); return x_5; } } -lean_object* l_EStateM_orelse_x27___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, uint8_t x_4, lean_object* x_5) { +lean_object* l_EStateM_orElse_x27___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, uint8_t x_4, lean_object* x_5) { _start: { lean_object* x_6; lean_object* x_7; lean_object* x_8; @@ -764,21 +764,21 @@ return x_21; } } } -lean_object* l_EStateM_orelse_x27(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { +lean_object* l_EStateM_orElse_x27(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { _start: { lean_object* x_5; -x_5 = lean_alloc_closure((void*)(l_EStateM_orelse_x27___rarg___boxed), 5, 0); +x_5 = lean_alloc_closure((void*)(l_EStateM_orElse_x27___rarg___boxed), 5, 0); return x_5; } } -lean_object* l_EStateM_orelse_x27___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) { +lean_object* l_EStateM_orElse_x27___rarg___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) { _start: { uint8_t x_6; lean_object* x_7; x_6 = lean_unbox(x_4); lean_dec(x_4); -x_7 = l_EStateM_orelse_x27___rarg(x_1, x_2, x_3, x_6, x_5); +x_7 = l_EStateM_orElse_x27___rarg(x_1, x_2, x_3, x_6, x_5); return x_7; } } @@ -1644,7 +1644,7 @@ lean_object* l_EStateM_Init_Control_EState___instance__6___rarg(lean_object* x_1 _start: { lean_object* x_2; -x_2 = lean_alloc_closure((void*)(l_EStateM_orelse___rarg), 4, 1); +x_2 = lean_alloc_closure((void*)(l_EStateM_orElse___rarg), 4, 1); lean_closure_set(x_2, 0, x_1); return x_2; } diff --git a/stage0/stdlib/Init/Core.c b/stage0/stdlib/Init/Core.c index ef1abea093..6d92c5ae34 100644 --- a/stage0/stdlib/Init/Core.c +++ b/stage0/stdlib/Init/Core.c @@ -100,14 +100,12 @@ lean_object* l_Classical_typeDecidable_match__1___rarg___boxed(lean_object*, lea lean_object* l_Init_Core___instance__1; lean_object* l_Init_Core___instance__3(lean_object*); lean_object* l_Init_Core___instance__14_match__1___rarg(lean_object*, lean_object*); -lean_object* l_default_sizeof(lean_object*, lean_object*); lean_object* l_cond___rarg(uint8_t, lean_object*, lean_object*); lean_object* l_Quotient_recOnSubsingleton___rarg(lean_object*, lean_object*); lean_object* l_Task_get___boxed(lean_object*, lean_object*); lean_object* l_Init_Core___instance__24_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_False_elim(lean_object*, uint8_t); lean_object* l_Init_Core___instance__45_match__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l_default_sizeof___boxed(lean_object*, lean_object*); lean_object* l_Task_map___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Nat_prio; lean_object* l_Init_Core___instance__45_match__2___rarg___boxed(lean_object*, lean_object*, lean_object*); @@ -165,7 +163,6 @@ lean_object* l_ite(lean_object*, lean_object*); lean_object* l_Quot_hrecOn(lean_object*, lean_object*, lean_object*); lean_object* l_not___boxed(lean_object*); lean_object* l_Task_Priority_dedicated; -lean_object* l_default_sizeof_match__1___rarg(lean_object*, lean_object*); uint8_t l_Init_Core___instance__31; lean_object* l_std_prec_arrow; uint8_t l_Init_Core___instance__22___rarg(uint8_t, uint8_t); @@ -214,7 +211,6 @@ lean_object* l_decEq(lean_object*); lean_object* l_Subtype_Init_Core___instance__42_match__1(lean_object*, lean_object*, lean_object*); lean_object* l_or___boxed(lean_object*, lean_object*); uint8_t l_strictOr(uint8_t, uint8_t); -lean_object* l_default_sizeof_match__1(lean_object*, lean_object*); lean_object* l_Eq_mpr___rarg(lean_object*); lean_object* l_decEq___rarg(lean_object*, lean_object*, lean_object*); lean_object* l_inferInstance(lean_object*); @@ -313,6 +309,7 @@ lean_object* l_Function_const(lean_object*, lean_object*); lean_object* l_Lean_reduceNat___boxed(lean_object*); lean_object* l_and_match__1(lean_object*); lean_object* l_and_match__1___rarg(uint8_t, uint8_t, lean_object*, lean_object*); +lean_object* l_default_sizeOf___boxed(lean_object*, lean_object*); lean_object* l_Eq_ndrecOn___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Function_combine(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Init_Core___instance__25_match__1(lean_object*); @@ -349,8 +346,10 @@ lean_object* l_id(lean_object*); lean_object* l_Subtype_Init_Core___instance__41(lean_object*, lean_object*); lean_object* l_inline___rarg(lean_object*); lean_object* l_dite___rarg___boxed(lean_object*, lean_object*, lean_object*); +lean_object* l_default_sizeOf_match__1(lean_object*, lean_object*); lean_object* l_id___rarg(lean_object*); lean_object* l_Init_Core___instance__32; +lean_object* l_default_sizeOf(lean_object*, lean_object*); lean_object* l_arbitrary(lean_object*); lean_object* l_Eq_ndrec___boxed(lean_object*, lean_object*, lean_object*); lean_object* l_Init_Core___instance__24(lean_object*); @@ -390,6 +389,7 @@ lean_object* l_Eq_ndrecOn(lean_object*, lean_object*, lean_object*, lean_object* lean_object* l_Init_Core___instance__44___rarg(lean_object*, lean_object*); lean_object* lean_task_get_own(lean_object*); uint8_t l_decidableOfDecidableOfIff___rarg(uint8_t, lean_object*); +lean_object* l_default_sizeOf_match__1___rarg(lean_object*, lean_object*); lean_object* l_cast___rarg(lean_object*); lean_object* l_Function_onFun___rarg(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* lean_thunk_bind(lean_object*, lean_object*); @@ -902,7 +902,7 @@ x_6 = lean_task_bind(x_3, x_4, x_5); return x_6; } } -lean_object* l_default_sizeof_match__1___rarg(lean_object* x_1, lean_object* x_2) { +lean_object* l_default_sizeOf_match__1___rarg(lean_object* x_1, lean_object* x_2) { _start: { lean_object* x_3; @@ -910,15 +910,15 @@ x_3 = lean_apply_1(x_2, x_1); return x_3; } } -lean_object* l_default_sizeof_match__1(lean_object* x_1, lean_object* x_2) { +lean_object* l_default_sizeOf_match__1(lean_object* x_1, lean_object* x_2) { _start: { lean_object* x_3; -x_3 = lean_alloc_closure((void*)(l_default_sizeof_match__1___rarg), 2, 0); +x_3 = lean_alloc_closure((void*)(l_default_sizeOf_match__1___rarg), 2, 0); return x_3; } } -lean_object* l_default_sizeof(lean_object* x_1, lean_object* x_2) { +lean_object* l_default_sizeOf(lean_object* x_1, lean_object* x_2) { _start: { lean_object* x_3; @@ -926,11 +926,11 @@ x_3 = lean_unsigned_to_nat(0u); return x_3; } } -lean_object* l_default_sizeof___boxed(lean_object* x_1, lean_object* x_2) { +lean_object* l_default_sizeOf___boxed(lean_object* x_1, lean_object* x_2) { _start: { lean_object* x_3; -x_3 = l_default_sizeof(x_1, x_2); +x_3 = l_default_sizeOf(x_1, x_2); lean_dec(x_2); return x_3; } @@ -939,7 +939,7 @@ static lean_object* _init_l_Init_Core___instance__3___closed__1() { _start: { lean_object* x_1; -x_1 = lean_alloc_closure((void*)(l_default_sizeof___boxed), 2, 1); +x_1 = lean_alloc_closure((void*)(l_default_sizeOf___boxed), 2, 1); lean_closure_set(x_1, 0, lean_box(0)); return x_1; } diff --git a/stage0/stdlib/Lean/Delaborator.c b/stage0/stdlib/Lean/Delaborator.c index 5d79022c16..7239465331 100644 --- a/stage0/stdlib/Lean/Delaborator.c +++ b/stage0/stdlib/Lean/Delaborator.c @@ -343,6 +343,7 @@ lean_object* l___regBuiltin_Lean_Delaborator_delabDiv___closed__4; lean_object* l___regBuiltin_Lean_Delaborator_delabBind(lean_object*); lean_object* l_Lean_Delaborator_delabMap___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Delaborator_delabBAnd___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +extern lean_object* l_Lean_Meta_evalNat___closed__9; extern lean_object* l_Lean_mkAppStx___closed__8; lean_object* l_Std_PersistentHashMap_findAux___at_Lean_Delaborator_delabFor___spec__3___boxed(lean_object*, lean_object*, lean_object*); lean_object* l___regBuiltin_Lean_Delaborator_delabCoe___closed__1; @@ -426,6 +427,7 @@ lean_object* l_Array_anyRangeMAux___at_Lean_Delaborator_delabAppExplicit___spec_ lean_object* l_Lean_Delaborator_delabSort___closed__10; lean_object* l___regBuiltin_Lean_Delaborator_delabCons(lean_object*); lean_object* l_Lean_Delaborator_delabTuple___lambda__1___closed__4; +extern lean_object* l___private_Lean_Meta_DiscrTree_0__Lean_Meta_DiscrTree_shouldAddAsStar___closed__7; lean_object* l_Lean_Delaborator_delabBOr___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Delaborator_orelse(lean_object*); lean_object* l_Lean_Delaborator_delabBNe___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -582,6 +584,7 @@ lean_object* l_Lean_Delaborator_delabPrefixOp___lambda__1(lean_object*, lean_obj lean_object* l_Lean_Delaborator_getPPOption(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___private_Lean_Delaborator_0__Lean_Delaborator_unresolveUsingNamespace___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___regBuiltin_Lean_Delaborator_delabTuple___closed__3; +extern lean_object* l_Lean_Meta_evalNat___closed__12; lean_object* l_Lean_Delaborator_annotatePos_match__2(lean_object*); lean_object* l_Lean_Delaborator_delabProd___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); uint8_t l_Lean_getPPUnicode(lean_object*); @@ -613,7 +616,6 @@ lean_object* l_Lean_Delaborator_delabModN___lambda__1___closed__4; extern lean_object* l_Lean_mkAppStx___closed__6; lean_object* l_Lean_Delaborator_withBindingBody___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Delaborator_delabEq___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); -lean_object* l___regBuiltin_Lean_Delaborator_delabLT___closed__4; lean_object* l___regBuiltin_Lean_Delaborator_delabOrElse___closed__1; lean_object* l_Lean_getRevAliases(lean_object*, lean_object*); lean_object* l___regBuiltin_Lean_Delaborator_delabOrElse___closed__2; @@ -688,6 +690,7 @@ lean_object* l_Lean_Delaborator_delabProjectionApp_match__2___rarg(lean_object*, lean_object* l___regBuiltin_Lean_Delaborator_delabGE___closed__2; lean_object* l_Lean_Delaborator_delabModN___lambda__1___closed__1; lean_object* l_Lean_getPPCoercions___closed__2; +extern lean_object* l_Lean_Meta_evalNat___closed__5; lean_object* l___regBuiltin_Lean_Delaborator_delabseq___closed__2; lean_object* l_Lean_Delaborator_delabGT___lambda__1___closed__3; lean_object* l_Lean_Delaborator_delabProjectionApp_match__1___rarg(lean_object*, lean_object*, lean_object*); @@ -761,7 +764,6 @@ lean_object* l_Lean_Delaborator_delabProd___lambda__1___closed__4; lean_object* l_Lean_LocalDecl_type(lean_object*); uint8_t l_Lean_getPPNotation(lean_object*); lean_object* l___regBuiltin_Lean_Delaborator_delabAdd___closed__2; -lean_object* l___regBuiltin_Lean_Delaborator_delabMul___closed__4; lean_object* l_Lean_Delaborator_failure___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_Init_LeanInit___instance__19___rarg___closed__1; lean_object* l_Lean_Delaborator_delabStructureInstance_match__2(lean_object*); @@ -863,7 +865,6 @@ lean_object* l_Lean_Delaborator_delabAppExplicit___lambda__2___closed__2; lean_object* lean_panic_fn(lean_object*, lean_object*); extern lean_object* l_Lean_setOptionFromString___closed__1; lean_object* l_Lean_getPPUniverses___closed__2; -lean_object* l___regBuiltin_Lean_Delaborator_delabEquiv___closed__5; lean_object* l_Lean_Delaborator_delabLT___lambda__1(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Std_PersistentHashMap_mkCollisionNode___rarg___closed__1; extern lean_object* l_Lean_Init_LeanInit___instance__8___closed__1; @@ -928,7 +929,6 @@ lean_object* l_Lean_Delaborator_getExprKind_match__1___rarg(lean_object*, lean_o lean_object* l_Lean_getPPStructureInstanceType___closed__2; lean_object* l_Lean_Delaborator_Lean_Delaborator___instance__3___closed__2; lean_object* l_Lean_Delaborator_delabGE___lambda__1___closed__3; -lean_object* l___regBuiltin_Lean_Delaborator_delabLE___closed__4; lean_object* l_Lean_getPPExplicit___boxed(lean_object*); lean_object* l___regBuiltin_Lean_Delaborator_delabNot(lean_object*); lean_object* l___regBuiltin_Lean_Delaborator_elabMData___closed__1; @@ -1018,7 +1018,6 @@ lean_object* l_Lean_Delaborator_delabProjectionApp_match__3___rarg(lean_object*, lean_object* l___regBuiltin_Lean_Delaborator_delabAndM___closed__1; lean_object* l_Lean_Delaborator_delabHEq___lambda__1___closed__6; lean_object* l_Lean_Delaborator_delabLetE___closed__4; -lean_object* l___regBuiltin_Lean_Delaborator_delabAdd___closed__4; lean_object* l___regBuiltin_Lean_Delaborator_delabBVar___closed__1; lean_object* l_Lean_Delaborator_delabModN(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Delaborator_delabPow___lambda__1(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -1081,7 +1080,6 @@ lean_object* l___regBuiltin_Lean_Delaborator_delabTuple___closed__1; lean_object* l_Lean_Delaborator_delabStructureInstance_match__3___rarg(lean_object*, lean_object*, lean_object*); uint8_t l_List_isEmpty___rarg(lean_object*); lean_object* l_Lean_getPPBinderTypes___closed__2; -lean_object* l___regBuiltin_Lean_Delaborator_delabOfNat___closed__4; lean_object* l_Lean_Delaborator_liftMetaM(lean_object*); lean_object* l_Lean_Delaborator_Lean_Delaborator___instance__3___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Delaborator_delabseq___lambda__1(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -1174,7 +1172,6 @@ lean_object* l_Lean_Delaborator_delabMapRev___lambda__1___boxed(lean_object*, le lean_object* l___regBuiltin_Lean_Delaborator_delabLE___closed__2; lean_object* l___regBuiltin_Lean_Delaborator_delabBNe___closed__2; lean_object* l_Lean_Delaborator_delabseqRight___lambda__1___closed__3; -lean_object* l___regBuiltin_Lean_Delaborator_delabSub___closed__4; lean_object* l_Lean_Delaborator_delabAndM___lambda__1___closed__1; lean_object* l_Lean_Delaborator_delabAppExplicit___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_mkAppStx___closed__1; @@ -19104,32 +19101,24 @@ return x_7; static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabOfNat___closed__1() { _start: { -lean_object* x_1; -x_1 = lean_mk_string("HasOfNat"); -return x_1; +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Delaborator_getExprKind___closed__5; +x_2 = l_Lean_Meta_evalNat___closed__9; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; } } static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabOfNat___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Delaborator_getExprKind___closed__5; -x_2 = l___regBuiltin_Lean_Delaborator_delabOfNat___closed__1; -x_3 = lean_name_mk_string(x_1, x_2); -return x_3; -} -} -static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabOfNat___closed__3() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l___regBuiltin_Lean_Delaborator_delabOfNat___closed__2; +x_1 = l___regBuiltin_Lean_Delaborator_delabOfNat___closed__1; x_2 = l_Lean_Expr_isCharLit___closed__3; x_3 = lean_name_mk_string(x_1, x_2); return x_3; } } -static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabOfNat___closed__4() { +static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabOfNat___closed__3() { _start: { lean_object* x_1; @@ -19142,8 +19131,8 @@ _start: { lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; x_2 = l_Lean_Delaborator_delabAttribute; -x_3 = l___regBuiltin_Lean_Delaborator_delabOfNat___closed__3; -x_4 = l___regBuiltin_Lean_Delaborator_delabOfNat___closed__4; +x_3 = l___regBuiltin_Lean_Delaborator_delabOfNat___closed__2; +x_4 = l___regBuiltin_Lean_Delaborator_delabOfNat___closed__3; x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1); return x_5; } @@ -22931,32 +22920,24 @@ return x_11; static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabAdd___closed__1() { _start: { -lean_object* x_1; -x_1 = lean_mk_string("HasAdd"); -return x_1; +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Delaborator_getExprKind___closed__5; +x_2 = l___private_Lean_Meta_DiscrTree_0__Lean_Meta_DiscrTree_shouldAddAsStar___closed__7; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; } } static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabAdd___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Delaborator_getExprKind___closed__5; -x_2 = l___regBuiltin_Lean_Delaborator_delabAdd___closed__1; -x_3 = lean_name_mk_string(x_1, x_2); -return x_3; -} -} -static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabAdd___closed__3() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l___regBuiltin_Lean_Delaborator_delabAdd___closed__2; +x_1 = l___regBuiltin_Lean_Delaborator_delabAdd___closed__1; x_2 = l___private_Lean_Meta_DiscrTree_0__Lean_Meta_DiscrTree_shouldAddAsStar___closed__5; x_3 = lean_name_mk_string(x_1, x_2); return x_3; } } -static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabAdd___closed__4() { +static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabAdd___closed__3() { _start: { lean_object* x_1; @@ -22969,8 +22950,8 @@ _start: { lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; x_2 = l_Lean_Delaborator_delabAttribute; -x_3 = l___regBuiltin_Lean_Delaborator_delabAdd___closed__3; -x_4 = l___regBuiltin_Lean_Delaborator_delabAdd___closed__4; +x_3 = l___regBuiltin_Lean_Delaborator_delabAdd___closed__2; +x_4 = l___regBuiltin_Lean_Delaborator_delabAdd___closed__3; x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1); return x_5; } @@ -23051,32 +23032,24 @@ return x_11; static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabSub___closed__1() { _start: { -lean_object* x_1; -x_1 = lean_mk_string("HasSub"); -return x_1; +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Delaborator_getExprKind___closed__5; +x_2 = l_Lean_Meta_evalNat___closed__12; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; } } static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabSub___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Delaborator_getExprKind___closed__5; -x_2 = l___regBuiltin_Lean_Delaborator_delabSub___closed__1; -x_3 = lean_name_mk_string(x_1, x_2); -return x_3; -} -} -static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabSub___closed__3() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l___regBuiltin_Lean_Delaborator_delabSub___closed__2; +x_1 = l___regBuiltin_Lean_Delaborator_delabSub___closed__1; x_2 = l_Lean_Meta_evalNat___closed__14; x_3 = lean_name_mk_string(x_1, x_2); return x_3; } } -static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabSub___closed__4() { +static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabSub___closed__3() { _start: { lean_object* x_1; @@ -23089,8 +23062,8 @@ _start: { lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; x_2 = l_Lean_Delaborator_delabAttribute; -x_3 = l___regBuiltin_Lean_Delaborator_delabSub___closed__3; -x_4 = l___regBuiltin_Lean_Delaborator_delabSub___closed__4; +x_3 = l___regBuiltin_Lean_Delaborator_delabSub___closed__2; +x_4 = l___regBuiltin_Lean_Delaborator_delabSub___closed__3; x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1); return x_5; } @@ -23171,32 +23144,24 @@ return x_11; static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabMul___closed__1() { _start: { -lean_object* x_1; -x_1 = lean_mk_string("HasMul"); -return x_1; +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Delaborator_getExprKind___closed__5; +x_2 = l_Lean_Meta_evalNat___closed__5; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; } } static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabMul___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Delaborator_getExprKind___closed__5; -x_2 = l___regBuiltin_Lean_Delaborator_delabMul___closed__1; -x_3 = lean_name_mk_string(x_1, x_2); -return x_3; -} -} -static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabMul___closed__3() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l___regBuiltin_Lean_Delaborator_delabMul___closed__2; +x_1 = l___regBuiltin_Lean_Delaborator_delabMul___closed__1; x_2 = l_Lean_Meta_evalNat___closed__7; x_3 = lean_name_mk_string(x_1, x_2); return x_3; } } -static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabMul___closed__4() { +static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabMul___closed__3() { _start: { lean_object* x_1; @@ -23209,8 +23174,8 @@ _start: { lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; x_2 = l_Lean_Delaborator_delabAttribute; -x_3 = l___regBuiltin_Lean_Delaborator_delabMul___closed__3; -x_4 = l___regBuiltin_Lean_Delaborator_delabMul___closed__4; +x_3 = l___regBuiltin_Lean_Delaborator_delabMul___closed__2; +x_4 = l___regBuiltin_Lean_Delaborator_delabMul___closed__3; x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1); return x_5; } @@ -23300,7 +23265,7 @@ static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabDiv___closed__1() _start: { lean_object* x_1; -x_1 = lean_mk_string("HasDiv"); +x_1 = lean_mk_string("Div"); return x_1; } } @@ -23428,7 +23393,7 @@ static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabMod___closed__1() _start: { lean_object* x_1; -x_1 = lean_mk_string("HasMod"); +x_1 = lean_mk_string("Mod"); return x_1; } } @@ -23564,7 +23529,7 @@ static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabModN___closed__1( _start: { lean_object* x_1; -x_1 = lean_mk_string("HasModN"); +x_1 = lean_mk_string("ModN"); return x_1; } } @@ -23708,7 +23673,7 @@ static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabPow___closed__1() _start: { lean_object* x_1; -x_1 = lean_mk_string("HasPow"); +x_1 = lean_mk_string("Pow"); return x_1; } } @@ -23883,32 +23848,24 @@ return x_11; static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabLE___closed__1() { _start: { -lean_object* x_1; -x_1 = lean_mk_string("HasLessEq"); -return x_1; +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Delaborator_getExprKind___closed__5; +x_2 = l_Lean_Meta_mkLe___rarg___closed__1; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; } } static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabLE___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Delaborator_getExprKind___closed__5; -x_2 = l___regBuiltin_Lean_Delaborator_delabLE___closed__1; -x_3 = lean_name_mk_string(x_1, x_2); -return x_3; -} -} -static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabLE___closed__3() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l___regBuiltin_Lean_Delaborator_delabLE___closed__2; +x_1 = l___regBuiltin_Lean_Delaborator_delabLE___closed__1; x_2 = l_Lean_Meta_mkLe___rarg___closed__1; x_3 = lean_name_mk_string(x_1, x_2); return x_3; } } -static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabLE___closed__4() { +static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabLE___closed__3() { _start: { lean_object* x_1; @@ -23921,8 +23878,8 @@ _start: { lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; x_2 = l_Lean_Delaborator_delabAttribute; -x_3 = l___regBuiltin_Lean_Delaborator_delabLE___closed__3; -x_4 = l___regBuiltin_Lean_Delaborator_delabLE___closed__4; +x_3 = l___regBuiltin_Lean_Delaborator_delabLE___closed__2; +x_4 = l___regBuiltin_Lean_Delaborator_delabLE___closed__3; x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1); return x_5; } @@ -24185,32 +24142,24 @@ return x_11; static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabLT___closed__1() { _start: { -lean_object* x_1; -x_1 = lean_mk_string("HasLess"); -return x_1; +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Delaborator_getExprKind___closed__5; +x_2 = l_Lean_Meta_mkLt___rarg___closed__1; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; } } static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabLT___closed__2() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Delaborator_getExprKind___closed__5; -x_2 = l___regBuiltin_Lean_Delaborator_delabLT___closed__1; -x_3 = lean_name_mk_string(x_1, x_2); -return x_3; -} -} -static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabLT___closed__3() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l___regBuiltin_Lean_Delaborator_delabLT___closed__2; +x_1 = l___regBuiltin_Lean_Delaborator_delabLT___closed__1; x_2 = l_Lean_Meta_mkLt___rarg___closed__1; x_3 = lean_name_mk_string(x_1, x_2); return x_3; } } -static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabLT___closed__4() { +static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabLT___closed__3() { _start: { lean_object* x_1; @@ -24223,8 +24172,8 @@ _start: { lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; x_2 = l_Lean_Delaborator_delabAttribute; -x_3 = l___regBuiltin_Lean_Delaborator_delabLT___closed__3; -x_4 = l___regBuiltin_Lean_Delaborator_delabLT___closed__4; +x_3 = l___regBuiltin_Lean_Delaborator_delabLT___closed__2; +x_4 = l___regBuiltin_Lean_Delaborator_delabLT___closed__3; x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1); return x_5; } @@ -24676,7 +24625,7 @@ static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabBEq___closed__1() _start: { lean_object* x_1; -x_1 = lean_mk_string("HasBeq"); +x_1 = lean_mk_string("BEq"); return x_1; } } @@ -25088,7 +25037,7 @@ static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabEquiv___closed__1 _start: { lean_object* x_1; -x_1 = lean_mk_string("HasEquiv"); +x_1 = lean_mk_string("Equiv"); return x_1; } } @@ -25105,22 +25054,14 @@ return x_3; static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabEquiv___closed__3() { _start: { -lean_object* x_1; -x_1 = lean_mk_string("Equiv"); -return x_1; -} -} -static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabEquiv___closed__4() { -_start: -{ lean_object* x_1; lean_object* x_2; lean_object* x_3; x_1 = l___regBuiltin_Lean_Delaborator_delabEquiv___closed__2; -x_2 = l___regBuiltin_Lean_Delaborator_delabEquiv___closed__3; +x_2 = l___regBuiltin_Lean_Delaborator_delabEquiv___closed__1; x_3 = lean_name_mk_string(x_1, x_2); return x_3; } } -static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabEquiv___closed__5() { +static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabEquiv___closed__4() { _start: { lean_object* x_1; @@ -25133,8 +25074,8 @@ _start: { lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; x_2 = l_Lean_Delaborator_delabAttribute; -x_3 = l___regBuiltin_Lean_Delaborator_delabEquiv___closed__4; -x_4 = l___regBuiltin_Lean_Delaborator_delabEquiv___closed__5; +x_3 = l___regBuiltin_Lean_Delaborator_delabEquiv___closed__3; +x_4 = l___regBuiltin_Lean_Delaborator_delabEquiv___closed__4; x_5 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_1); return x_5; } @@ -25900,7 +25841,7 @@ static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabAppend___closed__ _start: { lean_object* x_1; -x_1 = lean_mk_string("HasAppend"); +x_1 = lean_mk_string("Append"); return x_1; } } @@ -26156,7 +26097,7 @@ static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabAndThen___closed_ _start: { lean_object* x_1; -x_1 = lean_mk_string("HasAndthen"); +x_1 = lean_mk_string("AndThen"); return x_1; } } @@ -26292,7 +26233,7 @@ static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabBind___closed__1( _start: { lean_object* x_1; -x_1 = lean_mk_string("HasBind"); +x_1 = lean_mk_string("Bind"); return x_1; } } @@ -26436,7 +26377,7 @@ static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabseq___closed__1() _start: { lean_object* x_1; -x_1 = lean_mk_string("HasSeq"); +x_1 = lean_mk_string("Seq"); return x_1; } } @@ -26572,7 +26513,7 @@ static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabseqLeft___closed_ _start: { lean_object* x_1; -x_1 = lean_mk_string("HasSeqLeft"); +x_1 = lean_mk_string("SeqLeft"); return x_1; } } @@ -26708,7 +26649,7 @@ static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabseqRight___closed _start: { lean_object* x_1; -x_1 = lean_mk_string("HasSeqRight"); +x_1 = lean_mk_string("SeqRight"); return x_1; } } @@ -27098,7 +27039,7 @@ static lean_object* _init_l___regBuiltin_Lean_Delaborator_delabOrElse___closed__ _start: { lean_object* x_1; -x_1 = lean_mk_string("HasOrelse"); +x_1 = lean_mk_string("OrElse"); return x_1; } } @@ -28213,8 +28154,6 @@ l___regBuiltin_Lean_Delaborator_delabOfNat___closed__2 = _init_l___regBuiltin_Le lean_mark_persistent(l___regBuiltin_Lean_Delaborator_delabOfNat___closed__2); l___regBuiltin_Lean_Delaborator_delabOfNat___closed__3 = _init_l___regBuiltin_Lean_Delaborator_delabOfNat___closed__3(); lean_mark_persistent(l___regBuiltin_Lean_Delaborator_delabOfNat___closed__3); -l___regBuiltin_Lean_Delaborator_delabOfNat___closed__4 = _init_l___regBuiltin_Lean_Delaborator_delabOfNat___closed__4(); -lean_mark_persistent(l___regBuiltin_Lean_Delaborator_delabOfNat___closed__4); res = l___regBuiltin_Lean_Delaborator_delabOfNat(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); @@ -28346,8 +28285,6 @@ l___regBuiltin_Lean_Delaborator_delabAdd___closed__2 = _init_l___regBuiltin_Lean lean_mark_persistent(l___regBuiltin_Lean_Delaborator_delabAdd___closed__2); l___regBuiltin_Lean_Delaborator_delabAdd___closed__3 = _init_l___regBuiltin_Lean_Delaborator_delabAdd___closed__3(); lean_mark_persistent(l___regBuiltin_Lean_Delaborator_delabAdd___closed__3); -l___regBuiltin_Lean_Delaborator_delabAdd___closed__4 = _init_l___regBuiltin_Lean_Delaborator_delabAdd___closed__4(); -lean_mark_persistent(l___regBuiltin_Lean_Delaborator_delabAdd___closed__4); res = l___regBuiltin_Lean_Delaborator_delabAdd(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); @@ -28363,8 +28300,6 @@ l___regBuiltin_Lean_Delaborator_delabSub___closed__2 = _init_l___regBuiltin_Lean lean_mark_persistent(l___regBuiltin_Lean_Delaborator_delabSub___closed__2); l___regBuiltin_Lean_Delaborator_delabSub___closed__3 = _init_l___regBuiltin_Lean_Delaborator_delabSub___closed__3(); lean_mark_persistent(l___regBuiltin_Lean_Delaborator_delabSub___closed__3); -l___regBuiltin_Lean_Delaborator_delabSub___closed__4 = _init_l___regBuiltin_Lean_Delaborator_delabSub___closed__4(); -lean_mark_persistent(l___regBuiltin_Lean_Delaborator_delabSub___closed__4); res = l___regBuiltin_Lean_Delaborator_delabSub(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); @@ -28380,8 +28315,6 @@ l___regBuiltin_Lean_Delaborator_delabMul___closed__2 = _init_l___regBuiltin_Lean lean_mark_persistent(l___regBuiltin_Lean_Delaborator_delabMul___closed__2); l___regBuiltin_Lean_Delaborator_delabMul___closed__3 = _init_l___regBuiltin_Lean_Delaborator_delabMul___closed__3(); lean_mark_persistent(l___regBuiltin_Lean_Delaborator_delabMul___closed__3); -l___regBuiltin_Lean_Delaborator_delabMul___closed__4 = _init_l___regBuiltin_Lean_Delaborator_delabMul___closed__4(); -lean_mark_persistent(l___regBuiltin_Lean_Delaborator_delabMul___closed__4); res = l___regBuiltin_Lean_Delaborator_delabMul(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); @@ -28487,8 +28420,6 @@ l___regBuiltin_Lean_Delaborator_delabLE___closed__2 = _init_l___regBuiltin_Lean_ lean_mark_persistent(l___regBuiltin_Lean_Delaborator_delabLE___closed__2); l___regBuiltin_Lean_Delaborator_delabLE___closed__3 = _init_l___regBuiltin_Lean_Delaborator_delabLE___closed__3(); lean_mark_persistent(l___regBuiltin_Lean_Delaborator_delabLE___closed__3); -l___regBuiltin_Lean_Delaborator_delabLE___closed__4 = _init_l___regBuiltin_Lean_Delaborator_delabLE___closed__4(); -lean_mark_persistent(l___regBuiltin_Lean_Delaborator_delabLE___closed__4); res = l___regBuiltin_Lean_Delaborator_delabLE(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); @@ -28531,8 +28462,6 @@ l___regBuiltin_Lean_Delaborator_delabLT___closed__2 = _init_l___regBuiltin_Lean_ lean_mark_persistent(l___regBuiltin_Lean_Delaborator_delabLT___closed__2); l___regBuiltin_Lean_Delaborator_delabLT___closed__3 = _init_l___regBuiltin_Lean_Delaborator_delabLT___closed__3(); lean_mark_persistent(l___regBuiltin_Lean_Delaborator_delabLT___closed__3); -l___regBuiltin_Lean_Delaborator_delabLT___closed__4 = _init_l___regBuiltin_Lean_Delaborator_delabLT___closed__4(); -lean_mark_persistent(l___regBuiltin_Lean_Delaborator_delabLT___closed__4); res = l___regBuiltin_Lean_Delaborator_delabLT(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); @@ -28664,8 +28593,6 @@ l___regBuiltin_Lean_Delaborator_delabEquiv___closed__3 = _init_l___regBuiltin_Le lean_mark_persistent(l___regBuiltin_Lean_Delaborator_delabEquiv___closed__3); l___regBuiltin_Lean_Delaborator_delabEquiv___closed__4 = _init_l___regBuiltin_Lean_Delaborator_delabEquiv___closed__4(); lean_mark_persistent(l___regBuiltin_Lean_Delaborator_delabEquiv___closed__4); -l___regBuiltin_Lean_Delaborator_delabEquiv___closed__5 = _init_l___regBuiltin_Lean_Delaborator_delabEquiv___closed__5(); -lean_mark_persistent(l___regBuiltin_Lean_Delaborator_delabEquiv___closed__5); res = l___regBuiltin_Lean_Delaborator_delabEquiv(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); diff --git a/stage0/stdlib/Lean/Elab/Do.c b/stage0/stdlib/Lean/Elab/Do.c index a8f208ccb1..88296b35f7 100644 --- a/stage0/stdlib/Lean/Elab/Do.c +++ b/stage0/stdlib/Lean/Elab/Do.c @@ -123,7 +123,6 @@ extern lean_object* l___private_Lean_Elab_Binders_0__Lean_Elab_Term_expandMatchA lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_doSeqToCode(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_resolveLocalName(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Std_Range_myMacro____x40_Init_Data_Range___hyg_299____closed__20; -lean_object* l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__58; uint8_t l_Array_anyRangeMAux___at_Lean_Elab_Term_Do_hasTerminalAction___spec__2(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___lambda__5___closed__2; lean_object* l_Lean_Elab_Term_Do_ToTerm_continueToTermCore(lean_object*, lean_object*, lean_object*, lean_object*); @@ -220,7 +219,6 @@ lean_object* l_Lean_Elab_throwUnsupportedSyntax___at___private_Lean_Elab_Term_0_ lean_object* l_Lean_Elab_Term_Do_ToTerm_breakToTermCore___closed__16; lean_object* l_Lean_Elab_Term_Do_mkAuxDeclFor___rarg___lambda__5___closed__8; lean_object* l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTermCore___closed__12; -lean_object* l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__56; lean_object* l_Lean_Elab_Term_Do_ToTerm_returnToTerm(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Array_umapMAux___at_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___spec__1___closed__8; lean_object* l_Lean_Elab_Term_Do_extendUpdatedVarsAux_update(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -486,7 +484,6 @@ lean_object* l_Lean_Elab_Term_Do_ToTerm_actionTerminalToTermCore(lean_object*, l lean_object* l_Array_forInUnsafe_loop___at_Lean_Elab_Term_Do_getDoLetRecVars___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_Do_getDoLetArrowVars___closed__3; extern lean_object* l___private_Lean_Elab_Quotation_0__Lean_Elab_Term_Quotation_quoteSyntax___closed__41; -lean_object* l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__54; lean_object* l_Lean_Elab_Term_Do_ToTerm_breakToTermCore___closed__12; extern lean_object* l_Lean_Elab_Term_Quotation_stxQuot_expand___closed__3; lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Term_Do_ToCodeBlock_doSeqToCode___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); @@ -612,7 +609,6 @@ size_t lean_usize_of_nat(lean_object*); lean_object* l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__53; lean_object* l_Lean_Elab_Term_Do_concat___closed__3; lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_doSeqToCode___closed__6; -lean_object* l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__55; lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_concatWith(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__42; lean_object* l_Lean_Elab_Term_Do_CodeBlock_uvars___default; @@ -793,7 +789,6 @@ lean_object* l_Lean_Elab_Term_Do_ToTerm_seqToTermCore___closed__7; lean_object* l_Array_iterateMAux___at_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___spec__2___closed__7; lean_object* l_Lean_Elab_throwUnsupportedSyntax___at_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); uint8_t l_Std_RBNode_any___at_Lean_Elab_Term_Do_extendUpdatedVars___spec__1(lean_object*, lean_object*); -lean_object* l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__57; lean_object* l_Array_umapMAux___at_Lean_Elab_Term_Do_ToTerm_mkJoinPointCore___spec__1___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Array_anyRangeMAux___at_Lean_Elab_Term_Do_extendUpdatedVarsAux_update___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Array_iterateMAux___at_Lean_Elab_Term_Do_eraseVars___spec__3(lean_object*, lean_object*, lean_object*, lean_object*); @@ -27803,71 +27798,19 @@ return x_3; static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__51() { _start: { -lean_object* x_1; -x_1 = lean_mk_string("HasPure"); -return x_1; -} -} -static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__52() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__51; -x_3 = lean_name_mk_string(x_1, x_2); -return x_3; -} -} -static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__53() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__52; -x_2 = l_Lean_Meta_mkPure___rarg___closed__3; -x_3 = lean_name_mk_string(x_1, x_2); -return x_3; -} -} -static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__54() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__53; -x_3 = lean_alloc_ctor(0, 2, 0); -lean_ctor_set(x_3, 0, x_2); -lean_ctor_set(x_3, 1, x_1); -return x_3; -} -} -static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__55() { -_start: -{ -lean_object* x_1; lean_object* x_2; lean_object* x_3; -x_1 = lean_box(0); -x_2 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__54; -x_3 = lean_alloc_ctor(1, 2, 0); -lean_ctor_set(x_3, 0, x_2); -lean_ctor_set(x_3, 1, x_1); -return x_3; -} -} -static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__56() { -_start: -{ lean_object* x_1; lean_object* x_2; x_1 = l_IO_Prim_fopenFlags___closed__4; x_2 = lean_string_utf8_byte_size(x_1); return x_2; } } -static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__57() { +static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__52() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; x_1 = l_IO_Prim_fopenFlags___closed__4; x_2 = lean_unsigned_to_nat(0u); -x_3 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__56; +x_3 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__51; x_4 = lean_alloc_ctor(0, 3, 0); lean_ctor_set(x_4, 0, x_1); lean_ctor_set(x_4, 1, x_2); @@ -27875,7 +27818,7 @@ lean_ctor_set(x_4, 2, x_3); return x_4; } } -static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__58() { +static lean_object* _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__53() { _start: { lean_object* x_1; lean_object* x_2; lean_object* x_3; @@ -29501,7 +29444,7 @@ x_930 = lean_array_push(x_909, x_929); x_931 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__50; x_932 = l_Lean_addMacroScope(x_881, x_931, x_880); x_933 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__49; -x_934 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__55; +x_934 = l_Lean_Elab_Term_Quotation_stxQuot_expand___closed__30; x_935 = lean_alloc_ctor(3, 4, 0); lean_ctor_set(x_935, 0, x_885); lean_ctor_set(x_935, 1, x_933); @@ -29688,7 +29631,7 @@ x_1036 = lean_array_push(x_1015, x_1035); x_1037 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__50; x_1038 = l_Lean_addMacroScope(x_987, x_1037, x_986); x_1039 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__49; -x_1040 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__55; +x_1040 = l_Lean_Elab_Term_Quotation_stxQuot_expand___closed__30; x_1041 = lean_alloc_ctor(3, 4, 0); lean_ctor_set(x_1041, 0, x_991); lean_ctor_set(x_1041, 1, x_1039); @@ -29936,7 +29879,7 @@ lean_inc(x_1093); lean_inc(x_1094); x_1175 = l_Lean_addMacroScope(x_1094, x_1174, x_1093); x_1176 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__49; -x_1177 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__55; +x_1177 = l_Lean_Elab_Term_Quotation_stxQuot_expand___closed__30; x_1178 = lean_alloc_ctor(3, 4, 0); lean_ctor_set(x_1178, 0, x_1098); lean_ctor_set(x_1178, 1, x_1176); @@ -30243,7 +30186,7 @@ lean_inc(x_1266); lean_inc(x_1267); x_1348 = l_Lean_addMacroScope(x_1267, x_1347, x_1266); x_1349 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__49; -x_1350 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__55; +x_1350 = l_Lean_Elab_Term_Quotation_stxQuot_expand___closed__30; x_1351 = lean_alloc_ctor(3, 4, 0); lean_ctor_set(x_1351, 0, x_1271); lean_ctor_set(x_1351, 1, x_1349); @@ -30557,7 +30500,7 @@ lean_inc(x_1440); lean_inc(x_1441); x_1522 = l_Lean_addMacroScope(x_1441, x_1521, x_1440); x_1523 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__49; -x_1524 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__55; +x_1524 = l_Lean_Elab_Term_Quotation_stxQuot_expand___closed__30; x_1525 = lean_alloc_ctor(3, 4, 0); lean_ctor_set(x_1525, 0, x_1445); lean_ctor_set(x_1525, 1, x_1523); @@ -30610,9 +30553,9 @@ lean_ctor_set(x_1550, 1, x_1548); lean_ctor_set(x_1550, 2, x_1547); lean_ctor_set(x_1550, 3, x_1549); x_1551 = lean_array_push(x_1448, x_1550); -x_1552 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__58; +x_1552 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__53; x_1553 = l_Lean_addMacroScope(x_1441, x_1552, x_1440); -x_1554 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__57; +x_1554 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__52; x_1555 = lean_alloc_ctor(3, 4, 0); lean_ctor_set(x_1555, 0, x_1445); lean_ctor_set(x_1555, 1, x_1554); @@ -30850,7 +30793,7 @@ lean_inc(x_1604); lean_inc(x_1605); x_1686 = l_Lean_addMacroScope(x_1605, x_1685, x_1604); x_1687 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__49; -x_1688 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__55; +x_1688 = l_Lean_Elab_Term_Quotation_stxQuot_expand___closed__30; x_1689 = lean_alloc_ctor(3, 4, 0); lean_ctor_set(x_1689, 0, x_1609); lean_ctor_set(x_1689, 1, x_1687); @@ -30903,9 +30846,9 @@ lean_ctor_set(x_1714, 1, x_1712); lean_ctor_set(x_1714, 2, x_1711); lean_ctor_set(x_1714, 3, x_1713); x_1715 = lean_array_push(x_1612, x_1714); -x_1716 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__58; +x_1716 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__53; x_1717 = l_Lean_addMacroScope(x_1605, x_1716, x_1604); -x_1718 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__57; +x_1718 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__52; x_1719 = lean_alloc_ctor(3, 4, 0); lean_ctor_set(x_1719, 0, x_1609); lean_ctor_set(x_1719, 1, x_1718); @@ -31147,7 +31090,7 @@ lean_inc(x_1769); lean_inc(x_1770); x_1851 = l_Lean_addMacroScope(x_1770, x_1850, x_1769); x_1852 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__49; -x_1853 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__55; +x_1853 = l_Lean_Elab_Term_Quotation_stxQuot_expand___closed__30; x_1854 = lean_alloc_ctor(3, 4, 0); lean_ctor_set(x_1854, 0, x_1774); lean_ctor_set(x_1854, 1, x_1852); @@ -31504,7 +31447,7 @@ lean_inc(x_1969); lean_inc(x_1970); x_2051 = l_Lean_addMacroScope(x_1970, x_2050, x_1969); x_2052 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__49; -x_2053 = l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__55; +x_2053 = l_Lean_Elab_Term_Quotation_stxQuot_expand___closed__30; x_2054 = lean_alloc_ctor(3, 4, 0); lean_ctor_set(x_2054, 0, x_1974); lean_ctor_set(x_2054, 1, x_2052); @@ -46278,16 +46221,6 @@ l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__52 = _init_l_Lean_Ela lean_mark_persistent(l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__52); l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__53 = _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__53(); lean_mark_persistent(l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__53); -l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__54 = _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__54(); -lean_mark_persistent(l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__54); -l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__55 = _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__55(); -lean_mark_persistent(l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__55); -l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__56 = _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__56(); -lean_mark_persistent(l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__56); -l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__57 = _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__57(); -lean_mark_persistent(l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__57); -l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__58 = _init_l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__58(); -lean_mark_persistent(l_Lean_Elab_Term_Do_ToTerm_matchNestedTermResult___closed__58); l_Lean_Elab_Term_Do_ToCodeBlock_Context_varSet___default = _init_l_Lean_Elab_Term_Do_ToCodeBlock_Context_varSet___default(); lean_mark_persistent(l_Lean_Elab_Term_Do_ToCodeBlock_Context_varSet___default); l_Lean_Elab_Term_Do_ToCodeBlock_Context_insideFor___default = _init_l_Lean_Elab_Term_Do_ToCodeBlock_Context_insideFor___default(); diff --git a/stage0/stdlib/Lean/Meta/DiscrTree.c b/stage0/stdlib/Lean/Meta/DiscrTree.c index e8298fb188..41aa4937a4 100644 --- a/stage0/stdlib/Lean/Meta/DiscrTree.c +++ b/stage0/stdlib/Lean/Meta/DiscrTree.c @@ -5166,7 +5166,7 @@ _start: lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; x_1 = l_Lean_Meta_DiscrTree_insertCore___rarg___closed__2; x_2 = l_Lean_Meta_DiscrTree_insertCore___rarg___closed__3; -x_3 = lean_unsigned_to_nat(226u); +x_3 = lean_unsigned_to_nat(227u); x_4 = lean_unsigned_to_nat(23u); x_5 = l_Lean_Meta_DiscrTree_insertCore___rarg___closed__4; x_6 = l___private_Init_Util_0__mkPanicMessageWithDecl(x_1, x_2, x_3, x_4, x_5);