From af2d6dbd45cb5c4c9b8b4390f98f4e1e8a16a2e2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 24 Jun 2019 13:07:20 -0700 Subject: [PATCH] chore(library/init): avoid `local attribute` --- library/init/control/monad.lean | 7 +++---- library/init/core.lean | 16 ++++++++-------- library/init/data/array/basic.lean | 1 - library/init/data/persistentarray/basic.lean | 1 - library/init/lean/syntax.lean | 2 -- library/init/lean/trace.lean | 5 ++--- src/frontends/lean/builtin_cmds.cpp | 10 ---------- 7 files changed, 13 insertions(+), 29 deletions(-) diff --git a/library/init/control/monad.lean b/library/init/control/monad.lean index 34c4e85b19..cd9ad72cd1 100644 --- a/library/init/control/monad.lean +++ b/library/init/control/monad.lean @@ -27,9 +27,8 @@ class Monad (m : Type u → Type v) extends Applicative m, HasBind m : Type (max (seqLeft := λ α β x y, x >>= λ a, y >>= λ _, pure a) (seqRight := λ α β x y, x >>= λ _, y) +instance monadInhabited' {α : Type u} {m : Type u → Type v} [Monad m] : Inhabited (α → m α) := +⟨pure⟩ + instance monadInhabited {α : Type u} {m : Type u → Type v} [Monad m] [Inhabited α] : Inhabited (m α) := ⟨pure $ default _⟩ - -/- Alternative instance -/ -def monadInhabited' {α : Type u} {m : Type u → Type v} [Monad m] : Inhabited (α → m α) := -⟨pure⟩ diff --git a/library/init/core.lean b/library/init/core.lean index 76d29df549..172e05540e 100644 --- a/library/init/core.lean +++ b/library/init/core.lean @@ -1754,11 +1754,9 @@ noncomputable def propDecidable (a : Prop) : Decidable a := choice $ Or.elim (em a) (assume ha, ⟨isTrue ha⟩) (assume hna, ⟨isFalse hna⟩) -local attribute [instance] propDecidable noncomputable def decidableInhabited (a : Prop) : Inhabited (Decidable a) := ⟨propDecidable a⟩ -local attribute [instance] decidableInhabited noncomputable def typeDecidableEq (α : Sort u) : DecidableEq α := {decEq := λ x y, propDecidable (x = y)} @@ -1770,10 +1768,12 @@ match (propDecidable (Nonempty α)) with noncomputable def strongIndefiniteDescription {α : Sort u} (p : α → Prop) (h : Nonempty α) : {x : α // Exists (λ y : α, p y) → p x} := -if hp : Exists (λ x : α, p x) then - let xp := indefiniteDescription _ hp in - ⟨xp.val, λ h', xp.property⟩ -else ⟨choice h, λ h, absurd h hp⟩ +@dite (Exists (λ x : α, p x)) (propDecidable _) _ + (λ hp : Exists (λ x : α, p x), + show {x : α // Exists (λ y : α, p y) → p x}, from + let xp := indefiniteDescription _ hp in + ⟨xp.val, λ h', xp.property⟩) + (λ hp, ⟨choice h, λ h, absurd h hp⟩) /- the Hilbert epsilon Function -/ @@ -1808,10 +1808,10 @@ Or.elim (em a) -- this supercedes byCases in Decidable theorem byCases {p q : Prop} (hpq : p → q) (hnpq : ¬p → q) : q := -Decidable.byCases hpq hnpq +@Decidable.byCases _ _ (propDecidable _) hpq hnpq -- this supercedes byContradiction in Decidable theorem byContradiction {p : Prop} (h : ¬p → False) : p := -Decidable.byContradiction h +@Decidable.byContradiction _ (propDecidable _) h end Classical diff --git a/library/init/data/array/basic.lean b/library/init/data/array/basic.lean index 7b514bfc68..374ed821ff 100644 --- a/library/init/data/array/basic.lean +++ b/library/init/data/array/basic.lean @@ -137,7 +137,6 @@ partial def shrink : Array α → Nat → Array α section variables {m : Type v → Type v} [Monad m] -local attribute [instance] monadInhabited' -- TODO(Leo): justify termination using wf-rec @[specialize] partial def miterateAux (a : Array α) (f : Π i : Fin a.size, α → β → m β) : Nat → β → m β diff --git a/library/init/data/persistentarray/basic.lean b/library/init/data/persistentarray/basic.lean index fa77aa2aba..c9568f2e41 100644 --- a/library/init/data/persistentarray/basic.lean +++ b/library/init/data/persistentarray/basic.lean @@ -127,7 +127,6 @@ else section variables {m : Type v → Type v} [Monad m] -local attribute [instance] monadInhabited' @[specialize] partial def mfoldlAux (f : β → α → m β) : PersistentArrayNode α → β → m β | (node cs) b := cs.mfoldl (λ b c, mfoldlAux c b) b diff --git a/library/init/lean/syntax.lean b/library/init/lean/syntax.lean index 6a72fb9c8b..fa18cd6a1c 100644 --- a/library/init/lean/syntax.lean +++ b/library/init/lean/syntax.lean @@ -105,8 +105,6 @@ match s with | Syntax.node kind args scopes := fn ⟨Syntax.node kind (args.map (flipScopes scopes)) [], IsNode.mk _ _ _⟩ | other := base -local attribute [instance] monadInhabited - @[specialize] partial def mreplace {m : Type → Type} [Monad m] (fn : Syntax → m (Option Syntax)) : Syntax → m Syntax | stx@(node kind args scopes) := do o ← fn stx, diff --git a/library/init/lean/trace.lean b/library/init/lean/trace.lean index 72208e683e..e7913b30f8 100644 --- a/library/init/lean/trace.lean +++ b/library/init/lean/trace.lean @@ -33,10 +33,9 @@ structure TraceState := (curPos : Option Position) (curTraces : List Trace) -def TraceT (m : Type → Type u) := StateT TraceState m -local attribute [reducible] TraceT +abbrev TraceT (m : Type → Type u) := StateT TraceState m -instance (m) [Monad m] : Monad (TraceT m) := inferInstance +instance (m) [Monad m] : Monad (TraceT m) := inferInstanceAs (Monad (StateT TraceState m)) class MonadTracer (m : Type → Type u) := (traceRoot {α} : Position → Name → Message → Thunk (m α) → m α) diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 8807de1530..0e36833501 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -286,15 +286,6 @@ environment open_export_cmd(parser & p, bool open) { static environment open_cmd(parser & p) { return open_export_cmd(p, true); } static environment export_cmd(parser & p) { return open_export_cmd(p, false); } -static environment local_cmd(parser & p) { - if (p.curr_is_token_or_id(get_attribute_tk())) { - p.next(); - return local_attribute_cmd(p); - } else { - throw exception("invalid 'local' command, 'attribute' expected"); - } -} - static environment help_cmd(parser & p) { auto rep = p.mk_message(p.cmd_pos(), INFORMATION); if (p.curr_is_token_or_id(get_options_tk())) { @@ -494,7 +485,6 @@ void init_cmd_table(cmd_table & r) { add_cmd(r, cmd_info("namespace", "open a new namespace", namespace_cmd)); add_cmd(r, cmd_info("end", "close the current namespace/section", end_scoped_cmd)); add_cmd(r, cmd_info("#check", "type check given expression, and display its type", check_cmd)); - add_cmd(r, cmd_info("local", "define local attributes or notation", local_cmd)); add_cmd(r, cmd_info("#help", "brief description of available commands and options", help_cmd)); add_cmd(r, cmd_info("initQuot", "initialize `quot` type computational rules", init_quot_cmd)); add_cmd(r, cmd_info("import", "import module(s)", import_cmd));