From d960080ab1bf062335d95a46002760d0af4328ed Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Mon, 10 Jul 2023 19:58:09 -0400 Subject: [PATCH 1/7] feat: add alias tactic --- Std.lean | 1 + Std/Tactic/Alias.lean | 204 ++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 205 insertions(+) create mode 100644 Std/Tactic/Alias.lean diff --git a/Std.lean b/Std.lean index 94271223a5..77f63d624c 100644 --- a/Std.lean +++ b/Std.lean @@ -87,6 +87,7 @@ import Std.Linter import Std.Linter.UnnecessarySeqFocus import Std.Linter.UnreachableTactic import Std.Logic +import Std.Tactic.Alias import Std.Tactic.Basic import Std.Tactic.ByCases import Std.Tactic.CoeExt diff --git a/Std/Tactic/Alias.lean b/Std/Tactic/Alias.lean new file mode 100644 index 0000000000..682f737fd4 --- /dev/null +++ b/Std/Tactic/Alias.lean @@ -0,0 +1,204 @@ +/- +Copyright (c) 2017 Mario Carneiro. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Mario Carneiro, David Renshaw +-/ +import Lean + +/-! +# The `alias` command + +This file defines an `alias` command, which can be used to create copies +of a theorem or definition with different names. + +Syntax: + +```lean +/-- doc string -/ +alias my_theorem ← alias1 alias2 ... +``` + +This produces defs or theorems of the form: + +```lean +/-- doc string -/ +theorem alias1 : := my_theorem + +/-- doc string -/ +theorem alias2 : := my_theorem +``` + +Iff alias syntax: + +```lean +alias A_iff_B ↔ B_of_A A_of_B +alias A_iff_B ↔ .. +``` + +This gets an existing biconditional theorem `A_iff_B` and produces +the one-way implications `B_of_A` and `A_of_B` (with no change in +implicit arguments). A blank `_` can be used to avoid generating one direction. +The `..` notation attempts to generate the 'of'-names automatically when the +input theorem has the form `A_iff_B` or `A_iff_B_left` etc. +-/ + +namespace Tactic +namespace Alias + +open Lean Elab Parser.Command + +/-- Adds some copies of a theorem or definition. -/ +syntax (name := alias) (docComment)? "alias " ident " ←" (ppSpace ident)* : command + +/-- Adds one-way implication declarations. -/ +syntax (name := aliasLR) (docComment)? + "alias " ident " ↔ " binderIdent ppSpace binderIdent : command + +/-- Adds one-way implication declarations, inferring names for them. -/ +syntax (name := aliasLRDots) (docComment)? "alias " ident " ↔ " ".." : command + +/-- Like `++`, except that if the right argument starts with `_root_` the namespace will be +ignored. +``` +appendNamespace `a.b `c.d = `a.b.c.d +appendNamespace `a.b `_root_.c.d = `c.d +``` + +TODO: Move this declaration to a more central location. +-/ +def appendNamespace (ns : Name) : Name → Name + | .str .anonymous s => if s = "_root_" then Name.anonymous else Name.mkStr ns s + | .str p s => Name.mkStr (appendNamespace ns p) s + | .num p n => Name.mkNum (appendNamespace ns p) n + | .anonymous => ns + +set_option linter.missingDocs false in +/-- An alias can be in one of three forms -/ +inductive Target + | plain : Name → Target + | forward : Name → Target + | backwards : Name → Target + +/-- The name underlying an alias target -/ +def Target.toName : Target → Name + | Target.plain n => n + | Target.forward n => n + | Target.backwards n => n + +/-- The docstring for an alias. -/ +def Target.toString : Target → String + | Target.plain n => s!"**Alias** of `{n}`." + | Target.forward n => s!"**Alias** of the forward direction of `{n}`." + | Target.backwards n => s!"**Alias** of the reverse direction of `{n}`." + +/-- Elaborates an `alias ←` command. -/ +@[command_elab «alias»] def elabAlias : Command.CommandElab +| `($[$doc]? alias $name:ident ← $aliases:ident*) => do + let resolved ← resolveGlobalConstNoOverloadWithInfo name + let constant ← getConstInfo resolved + let ns ← getCurrNamespace + for a in aliases do withRef a do + let declName := appendNamespace ns a.getId + let decl ← match constant with + | Lean.ConstantInfo.defnInfo d => + pure $ .defnDecl { + d with name := declName + value := mkConst resolved (d.levelParams.map mkLevelParam) + } + | Lean.ConstantInfo.thmInfo t => + pure $ .thmDecl { + t with name := declName + value := mkConst resolved (t.levelParams.map mkLevelParam) + } + | _ => throwError "alias only works with def or theorem" + checkNotAlreadyDeclared declName + addDeclarationRanges declName { + range := ← getDeclarationRange (← getRef) + selectionRange := ← getDeclarationRange a + } + -- TODO add @alias attribute + Command.liftTermElabM do + if isNoncomputable (← getEnv) resolved then + addDecl decl + setEnv $ addNoncomputable (← getEnv) declName + else + addAndCompile decl + Term.addTermInfo' a (← mkConstWithLevelParams declName) (isBinder := true) + let target := Target.plain resolved + let docString := match doc with | none => target.toString + | some d => d.getDocString + addDocString declName docString +| _ => throwUnsupportedSyntax + +/-- + Given a possibly forall-quantified iff expression `prf`, produce a value for one + of the implication directions (determined by `mp`). +-/ +def mkIffMpApp (mp : Bool) (ty prf : Expr) : MetaM Expr := do + Meta.forallTelescope ty fun xs ty ↦ do + let some (lhs, rhs) := ty.iff? + | throwError "Target theorem must have the form `∀ x y z, a ↔ b`" + Meta.mkLambdaFVars xs <| + mkApp3 (mkConst (if mp then ``Iff.mp else ``Iff.mpr)) lhs rhs (mkAppN prf xs) + +/-- + Given a constant representing an iff decl, adds a decl for one of the implication + directions. +-/ +def aliasIff (doc : Option (TSyntax `Lean.Parser.Command.docComment)) (ci : ConstantInfo) + (ref : Syntax) (al : Name) (isForward : Bool) : + TermElabM Unit := do + let ls := ci.levelParams + let v ← mkIffMpApp isForward ci.type ci.value! + let t' ← Meta.inferType v + -- TODO add @alias attribute + addDeclarationRanges al { + range := ← getDeclarationRange (← getRef) + selectionRange := ← getDeclarationRange ref + } + addDecl $ .thmDecl { + name := al + value := v + type := t' + levelParams := ls + } + Term.addTermInfo' ref (← mkConstWithLevelParams al) (isBinder := true) + let target := if isForward then Target.forward ci.name else Target.backwards ci.name + let docString := match doc with | none => target.toString + | some d => d.getDocString + addDocString al docString + +/-- Elaborates an `alias ↔` command. -/ +@[command_elab aliasLR] def elabAliasLR : Command.CommandElab +| `($[$doc]? alias $name:ident ↔ $left:binderIdent $right:binderIdent) => do + let resolved ← resolveGlobalConstNoOverloadWithInfo name + let constant ← getConstInfo resolved + let ns ← getCurrNamespace + Command.liftTermElabM do + if let `(binderIdent| $x:ident) := left then + aliasIff doc constant x (appendNamespace ns x.getId) true + if let `(binderIdent| $x:ident) := right then + aliasIff doc constant x (appendNamespace ns x.getId) false +| _ => throwUnsupportedSyntax + +/-- Elaborates an `alias ↔ ..` command. -/ +@[command_elab aliasLRDots] def elabAliasLRDots : Command.CommandElab +| `($[$doc]? alias $name:ident ↔ ..%$tk) => do + let resolved ← resolveGlobalConstNoOverloadWithInfo name + let constant ← getConstInfo resolved + let (parent, base) ← match resolved with + | .str n s => pure (n, s) + | _ => throwError "alias only works for string names" + let components := base.splitOn "_iff_" + if components.length != 2 then throwError "LHS must be of the form *_iff_*" + let forward := String.intercalate "_of_" components.reverse + let backward := String.intercalate "_of_" components + let forwardName := Name.mkStr parent forward + let backwardName := Name.mkStr parent backward + Command.liftTermElabM do + aliasIff doc constant tk forwardName true + aliasIff doc constant tk backwardName false +| _ => throwUnsupportedSyntax + +end Alias +end Tactic From 96b1143be92cbb2907ce078653f266fc999e839c Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Mon, 10 Jul 2023 20:25:37 -0400 Subject: [PATCH 2/7] chore: add missing docs --- Std/Tactic/Alias.lean | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/Std/Tactic/Alias.lean b/Std/Tactic/Alias.lean index 682f737fd4..99d18ab0bd 100644 --- a/Std/Tactic/Alias.lean +++ b/Std/Tactic/Alias.lean @@ -72,12 +72,14 @@ def appendNamespace (ns : Name) : Name → Name | .num p n => Name.mkNum (appendNamespace ns p) n | .anonymous => ns -set_option linter.missingDocs false in /-- An alias can be in one of three forms -/ inductive Target - | plain : Name → Target - | forward : Name → Target - | backwards : Name → Target + | /-- Plain alias -/ + plain : Name → Target + | /-- Forward direction of an iff alias -/ + forward : Name → Target + | /-- Reverse direction of an iff alias -/ + backwards : Name → Target /-- The name underlying an alias target -/ def Target.toName : Target → Name From d8f5f584bcb5a55872092d82d1fdd8bda3f7fb24 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fran=C3=A7ois=20G=2E=20Dorais?= Date: Wed, 12 Jul 2023 21:10:15 -0400 Subject: [PATCH 3/7] chore: import tests for alias --- test/alias.lean | 81 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 81 insertions(+) create mode 100644 test/alias.lean diff --git a/test/alias.lean b/test/alias.lean new file mode 100644 index 0000000000..262786ece0 --- /dev/null +++ b/test/alias.lean @@ -0,0 +1,81 @@ +import Std.Tactic.Alias +import Std.Tactic.GuardExpr + +open Lean Meta +namespace Alias +namespace A + +/-- doc string for foo -/ +theorem foo : 1 + 1 = 2 := rfl + +/-- doc string for `alias foo` -/ +alias foo ← foo1 foo2 foo3 _root_.B.foo4 + +example : 1 + 1 = 2 := foo1 +example : 1 + 1 = 2 := foo2 +example : 1 + 1 = 2 := foo3 + +def bar : Nat := 5 +alias bar ← bar1 bar2 +example : bar1 = 5 := rfl +example : bar2 = 5 := rfl + +theorem baz (x : Nat) : x = x := rfl +alias baz ← baz1 +example : 3 = 3 := baz1 3 + +theorem ab_iff_ba {t : Type} {a b : t} : a = b ↔ b = a := Iff.intro Eq.symm Eq.symm +alias ab_iff_ba ↔ ba_of_ab ab_of_ba +example {a b : Nat} : a = b → b = a := ba_of_ab +example {t : Type} {a b : t} : b = a → a = b := ab_of_ba + +theorem a_iff_a_and_a (a : Prop) : a ↔ a ∧ a := + Iff.intro (λ x => ⟨x,x⟩) (λ x => x.1) + +alias a_iff_a_and_a ↔ forward _ +alias a_iff_a_and_a ↔ _ backward + +example : True → True ∧ True := forward True +example : True ∧ True → True := backward True + +/-- doc string for `alias a_iff_a_and_a` -/ +alias a_iff_a_and_a ↔ .. +example : True → True ∧ True := a_and_a_of_a True +example : True ∧ True → True := a_of_a_and_a True + +end A + +-- test namespacing +example : 1 + 1 = 2 := A.foo1 +example : 1 + 1 = 2 := B.foo4 +example : True → True ∧ True := A.a_and_a_of_a True +example : True → True ∧ True := A.forward True +example : True ∧ True → True := A.backward True + +namespace C + +alias A.a_iff_a_and_a ↔ _root_.B.forward2 _ +alias A.a_iff_a_and_a ↔ _ _root_.B.backward2 + +end C + +example : True → True ∧ True := B.forward2 True +example : True ∧ True → True := B.backward2 True + +theorem checkType : 1 + 1 = 2 ↔ 2 = 2 := .rfl +alias checkType ↔ forward backward + +example : True := by + have h1 := forward + have h2 := backward + guard_hyp h1 :ₛ 1 + 1 = 2 → 2 = 2 + guard_hyp h2 :ₛ 2 = 2 → 1 + 1 = 2 + trivial + +def foo : ℕ → ℕ := id + +alias foo ← bar + +def baz (n : ℕ) := bar n + +end Alias From 902f4e7aebad51d02ceb6e15a14cbf64d2e18a62 Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Tue, 18 Jul 2023 21:16:39 -0400 Subject: [PATCH 4/7] feat: simpler `appendNamespace` --- Std/Tactic/Alias.lean | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/Std/Tactic/Alias.lean b/Std/Tactic/Alias.lean index 99d18ab0bd..f8e28b9779 100644 --- a/Std/Tactic/Alias.lean +++ b/Std/Tactic/Alias.lean @@ -66,11 +66,8 @@ appendNamespace `a.b `_root_.c.d = `c.d TODO: Move this declaration to a more central location. -/ -def appendNamespace (ns : Name) : Name → Name - | .str .anonymous s => if s = "_root_" then Name.anonymous else Name.mkStr ns s - | .str p s => Name.mkStr (appendNamespace ns p) s - | .num p n => Name.mkNum (appendNamespace ns p) n - | .anonymous => ns +abbrev appendNamespace (ns : Name) (n : Name) : Name := + if rootNamespace.isPrefixOf n then removeRoot n else ns ++ n /-- An alias can be in one of three forms -/ inductive Target From 536c3d64b57f6a78fe486eb3ffc85a3f8986b462 Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Thu, 20 Jul 2023 23:38:52 -0400 Subject: [PATCH 5/7] chore: clearer name --- Std/Tactic/Alias.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/Std/Tactic/Alias.lean b/Std/Tactic/Alias.lean index f8e28b9779..48dbe298e4 100644 --- a/Std/Tactic/Alias.lean +++ b/Std/Tactic/Alias.lean @@ -60,13 +60,13 @@ syntax (name := aliasLRDots) (docComment)? "alias " ident " ↔ " ".." : command /-- Like `++`, except that if the right argument starts with `_root_` the namespace will be ignored. ``` -appendNamespace `a.b `c.d = `a.b.c.d -appendNamespace `a.b `_root_.c.d = `c.d +addNamespaceUnlessRoot `a.b `c.d = `a.b.c.d +addNamespaceUnlessRoot `a.b `_root_.c.d = `c.d ``` TODO: Move this declaration to a more central location. -/ -abbrev appendNamespace (ns : Name) (n : Name) : Name := +abbrev addNamespaceUnlessRoot (ns : Name) (n : Name) : Name := if rootNamespace.isPrefixOf n then removeRoot n else ns ++ n /-- An alias can be in one of three forms -/ @@ -97,7 +97,7 @@ def Target.toString : Target → String let constant ← getConstInfo resolved let ns ← getCurrNamespace for a in aliases do withRef a do - let declName := appendNamespace ns a.getId + let declName := addNamespaceUnlessRoot ns a.getId let decl ← match constant with | Lean.ConstantInfo.defnInfo d => pure $ .defnDecl { @@ -175,9 +175,9 @@ def aliasIff (doc : Option (TSyntax `Lean.Parser.Command.docComment)) (ci : Cons let ns ← getCurrNamespace Command.liftTermElabM do if let `(binderIdent| $x:ident) := left then - aliasIff doc constant x (appendNamespace ns x.getId) true + aliasIff doc constant x (addNamespaceUnlessRoot ns x.getId) true if let `(binderIdent| $x:ident) := right then - aliasIff doc constant x (appendNamespace ns x.getId) false + aliasIff doc constant x (addNamespaceUnlessRoot ns x.getId) false | _ => throwUnsupportedSyntax /-- Elaborates an `alias ↔ ..` command. -/ From c355f6454975572a0a66496064e4d5431dae36a3 Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Tue, 25 Jul 2023 02:21:07 -0400 Subject: [PATCH 6/7] style, docs --- Std/Tactic/Alias.lean | 171 ++++++++++++++++++++++-------------------- 1 file changed, 89 insertions(+), 82 deletions(-) diff --git a/Std/Tactic/Alias.lean b/Std/Tactic/Alias.lean index 48dbe298e4..ed9011499a 100644 --- a/Std/Tactic/Alias.lean +++ b/Std/Tactic/Alias.lean @@ -3,7 +3,9 @@ Copyright (c) 2017 Mario Carneiro. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Mario Carneiro, David Renshaw -/ -import Lean +import Lean.Elab.Command +import Lean.Elab.DeclarationRange +import Lean.Compiler.NoncomputableAttr /-! # The `alias` command @@ -42,21 +44,10 @@ The `..` notation attempts to generate the 'of'-names automatically when the input theorem has the form `A_iff_B` or `A_iff_B_left` etc. -/ -namespace Tactic -namespace Alias +namespace Std.Tactic.Alias open Lean Elab Parser.Command -/-- Adds some copies of a theorem or definition. -/ -syntax (name := alias) (docComment)? "alias " ident " ←" (ppSpace ident)* : command - -/-- Adds one-way implication declarations. -/ -syntax (name := aliasLR) (docComment)? - "alias " ident " ↔ " binderIdent ppSpace binderIdent : command - -/-- Adds one-way implication declarations, inferring names for them. -/ -syntax (name := aliasLRDots) (docComment)? "alias " ident " ↔ " ".." : command - /-- Like `++`, except that if the right argument starts with `_root_` the namespace will be ignored. ``` @@ -66,48 +57,81 @@ addNamespaceUnlessRoot `a.b `_root_.c.d = `c.d TODO: Move this declaration to a more central location. -/ -abbrev addNamespaceUnlessRoot (ns : Name) (n : Name) : Name := +@[inline] def addNamespaceUnlessRoot (ns : Name) (n : Name) : Name := if rootNamespace.isPrefixOf n then removeRoot n else ns ++ n /-- An alias can be in one of three forms -/ -inductive Target - | /-- Plain alias -/ - plain : Name → Target - | /-- Forward direction of an iff alias -/ - forward : Name → Target - | /-- Reverse direction of an iff alias -/ - backwards : Name → Target +inductive Target where + /-- Plain alias -/ + | plain : Name → Target + /-- Forward direction of an iff alias -/ + | forward : Name → Target + /-- Reverse direction of an iff alias -/ + | reverse : Name → Target /-- The name underlying an alias target -/ -def Target.toName : Target → Name +def Target.name : Target → Name | Target.plain n => n | Target.forward n => n - | Target.backwards n => n + | Target.reverse n => n /-- The docstring for an alias. -/ def Target.toString : Target → String | Target.plain n => s!"**Alias** of `{n}`." | Target.forward n => s!"**Alias** of the forward direction of `{n}`." - | Target.backwards n => s!"**Alias** of the reverse direction of `{n}`." + | Target.reverse n => s!"**Alias** of the reverse direction of `{n}`." + +/-- +The `alias` command can be used to create copies +of a theorem or definition with different names. + +Syntax: + +```lean +/-- doc string -/ +alias my_theorem ← alias1 alias2 ... +``` + +This produces defs or theorems of the form: + +```lean +/-- doc string -/ +theorem alias1 : := my_theorem + +/-- doc string -/ +theorem alias2 : := my_theorem +``` + +Iff alias syntax: + +```lean +alias A_iff_B ↔ B_of_A A_of_B +alias A_iff_B ↔ .. +``` -/-- Elaborates an `alias ←` command. -/ -@[command_elab «alias»] def elabAlias : Command.CommandElab -| `($[$doc]? alias $name:ident ← $aliases:ident*) => do +This gets an existing biconditional theorem `A_iff_B` and produces +the one-way implications `B_of_A` and `A_of_B` (with no change in +implicit arguments). A blank `_` can be used to avoid generating one direction. +The `..` notation attempts to generate the 'of'-names automatically when the +input theorem has the form `A_iff_B` or `A_iff_B_left` etc. +-/ +elab (name := alias) doc:(docComment)? + "alias " name:ident " ←" aliases:(ppSpace ident)* : command => do let resolved ← resolveGlobalConstNoOverloadWithInfo name - let constant ← getConstInfo resolved + let const ← getConstInfo resolved let ns ← getCurrNamespace for a in aliases do withRef a do let declName := addNamespaceUnlessRoot ns a.getId - let decl ← match constant with + let decl ← match const with | Lean.ConstantInfo.defnInfo d => - pure $ .defnDecl { - d with name := declName - value := mkConst resolved (d.levelParams.map mkLevelParam) + pure <| .defnDecl { d with + name := declName + value := mkConst resolved (d.levelParams.map mkLevelParam) } | Lean.ConstantInfo.thmInfo t => - pure $ .thmDecl { - t with name := declName - value := mkConst resolved (t.levelParams.map mkLevelParam) + pure <| .thmDecl { t with + name := declName + value := mkConst resolved (t.levelParams.map mkLevelParam) } | _ => throwError "alias only works with def or theorem" checkNotAlreadyDeclared declName @@ -119,19 +143,19 @@ def Target.toString : Target → String Command.liftTermElabM do if isNoncomputable (← getEnv) resolved then addDecl decl - setEnv $ addNoncomputable (← getEnv) declName + setEnv <| addNoncomputable (← getEnv) declName else addAndCompile decl Term.addTermInfo' a (← mkConstWithLevelParams declName) (isBinder := true) let target := Target.plain resolved - let docString := match doc with | none => target.toString - | some d => d.getDocString + let docString := match doc with + | none => target.toString + | some d => d.getDocString addDocString declName docString -| _ => throwUnsupportedSyntax /-- - Given a possibly forall-quantified iff expression `prf`, produce a value for one - of the implication directions (determined by `mp`). +Given a possibly forall-quantified iff expression `prf`, produce a value for one +of the implication directions (determined by `mp`). -/ def mkIffMpApp (mp : Bool) (ty prf : Expr) : MetaM Expr := do Meta.forallTelescope ty fun xs ty ↦ do @@ -140,51 +164,40 @@ def mkIffMpApp (mp : Bool) (ty prf : Expr) : MetaM Expr := do Meta.mkLambdaFVars xs <| mkApp3 (mkConst (if mp then ``Iff.mp else ``Iff.mpr)) lhs rhs (mkAppN prf xs) -/-- - Given a constant representing an iff decl, adds a decl for one of the implication - directions. --/ +/-- Given a constant representing an iff decl, adds a decl for one of the implication directions. -/ def aliasIff (doc : Option (TSyntax `Lean.Parser.Command.docComment)) (ci : ConstantInfo) - (ref : Syntax) (al : Name) (isForward : Bool) : - TermElabM Unit := do - let ls := ci.levelParams - let v ← mkIffMpApp isForward ci.type ci.value! - let t' ← Meta.inferType v + (ref : Syntax) (name : Name) (isForward : Bool) : TermElabM Unit := do + let value ← mkIffMpApp isForward ci.type ci.value! + let type ← Meta.inferType value -- TODO add @alias attribute - addDeclarationRanges al { + addDeclarationRanges name { range := ← getDeclarationRange (← getRef) selectionRange := ← getDeclarationRange ref } - addDecl $ .thmDecl { - name := al - value := v - type := t' - levelParams := ls - } - Term.addTermInfo' ref (← mkConstWithLevelParams al) (isBinder := true) - let target := if isForward then Target.forward ci.name else Target.backwards ci.name - let docString := match doc with | none => target.toString - | some d => d.getDocString - addDocString al docString - -/-- Elaborates an `alias ↔` command. -/ -@[command_elab aliasLR] def elabAliasLR : Command.CommandElab -| `($[$doc]? alias $name:ident ↔ $left:binderIdent $right:binderIdent) => do + addDecl <| .thmDecl { name, value, type, levelParams := ci.levelParams } + Term.addTermInfo' ref (← mkConstWithLevelParams name) (isBinder := true) + let target := if isForward then Target.forward ci.name else Target.reverse ci.name + let docString := match doc with + | none => target.toString + | some d => d.getDocString + addDocString name docString + +@[inherit_doc «alias»] +elab (name := aliasLR) doc:(docComment)? + "alias " name:ident " ↔ " left:binderIdent ppSpace right:binderIdent : command => do let resolved ← resolveGlobalConstNoOverloadWithInfo name - let constant ← getConstInfo resolved + let const ← getConstInfo resolved let ns ← getCurrNamespace Command.liftTermElabM do if let `(binderIdent| $x:ident) := left then - aliasIff doc constant x (addNamespaceUnlessRoot ns x.getId) true + aliasIff doc const x (addNamespaceUnlessRoot ns x.getId) (isForward := true) if let `(binderIdent| $x:ident) := right then - aliasIff doc constant x (addNamespaceUnlessRoot ns x.getId) false -| _ => throwUnsupportedSyntax + aliasIff doc const x (addNamespaceUnlessRoot ns x.getId) (isForward := false) -/-- Elaborates an `alias ↔ ..` command. -/ -@[command_elab aliasLRDots] def elabAliasLRDots : Command.CommandElab -| `($[$doc]? alias $name:ident ↔ ..%$tk) => do +@[inherit_doc «alias»] +elab (name := aliasLRDots) doc:(docComment)? "alias " name:ident " ↔ " tk:".." : command => do let resolved ← resolveGlobalConstNoOverloadWithInfo name - let constant ← getConstInfo resolved + let const ← getConstInfo resolved let (parent, base) ← match resolved with | .str n s => pure (n, s) | _ => throwError "alias only works for string names" @@ -192,12 +205,6 @@ def aliasIff (doc : Option (TSyntax `Lean.Parser.Command.docComment)) (ci : Cons if components.length != 2 then throwError "LHS must be of the form *_iff_*" let forward := String.intercalate "_of_" components.reverse let backward := String.intercalate "_of_" components - let forwardName := Name.mkStr parent forward - let backwardName := Name.mkStr parent backward Command.liftTermElabM do - aliasIff doc constant tk forwardName true - aliasIff doc constant tk backwardName false -| _ => throwUnsupportedSyntax - -end Alias -end Tactic + aliasIff doc const tk (.str parent forward) (isForward := true) + aliasIff doc const tk (.str parent backward) (isForward := false) From a6e48cacff02f7411a3d47eec3534da4742236ab Mon Sep 17 00:00:00 2001 From: "F. G. Dorais" Date: Tue, 25 Jul 2023 04:10:19 -0400 Subject: [PATCH 7/7] feat: allow protected aliases --- Std/Tactic/Alias.lean | 25 +++++++++++++++++-------- 1 file changed, 17 insertions(+), 8 deletions(-) diff --git a/Std/Tactic/Alias.lean b/Std/Tactic/Alias.lean index ed9011499a..8aa7356a0e 100644 --- a/Std/Tactic/Alias.lean +++ b/Std/Tactic/Alias.lean @@ -114,14 +114,17 @@ the one-way implications `B_of_A` and `A_of_B` (with no change in implicit arguments). A blank `_` can be used to avoid generating one direction. The `..` notation attempts to generate the 'of'-names automatically when the input theorem has the form `A_iff_B` or `A_iff_B_left` etc. + +The `protected` modifier can be used to add protected aliases. -/ elab (name := alias) doc:(docComment)? - "alias " name:ident " ←" aliases:(ppSpace ident)* : command => do + protect:("protected ")? "alias " name:ident " ←" aliases:(ppSpace ident)* : command => do + let visibility : Visibility := if protect.isSome then .protected else .regular let resolved ← resolveGlobalConstNoOverloadWithInfo name let const ← getConstInfo resolved let ns ← getCurrNamespace for a in aliases do withRef a do - let declName := addNamespaceUnlessRoot ns a.getId + let declName ← applyVisibility visibility <| addNamespaceUnlessRoot ns a.getId let decl ← match const with | Lean.ConstantInfo.defnInfo d => pure <| .defnDecl { d with @@ -184,18 +187,22 @@ def aliasIff (doc : Option (TSyntax `Lean.Parser.Command.docComment)) (ci : Cons @[inherit_doc «alias»] elab (name := aliasLR) doc:(docComment)? - "alias " name:ident " ↔ " left:binderIdent ppSpace right:binderIdent : command => do + protect:("protected ")? "alias " name:ident " ↔ " left:binderIdent ppSpace right:binderIdent : command => do + let visibility : Visibility := if protect.isSome then .protected else .regular let resolved ← resolveGlobalConstNoOverloadWithInfo name let const ← getConstInfo resolved let ns ← getCurrNamespace Command.liftTermElabM do if let `(binderIdent| $x:ident) := left then - aliasIff doc const x (addNamespaceUnlessRoot ns x.getId) (isForward := true) + let declName ← applyVisibility visibility <| addNamespaceUnlessRoot ns x.getId + aliasIff doc const x declName (isForward := true) if let `(binderIdent| $x:ident) := right then - aliasIff doc const x (addNamespaceUnlessRoot ns x.getId) (isForward := false) + let declName ← applyVisibility visibility <| addNamespaceUnlessRoot ns x.getId + aliasIff doc const x declName (isForward := false) @[inherit_doc «alias»] -elab (name := aliasLRDots) doc:(docComment)? "alias " name:ident " ↔ " tk:".." : command => do +elab (name := aliasLRDots) doc:(docComment)? protect:("protected ")? "alias " name:ident " ↔ " tk:".." : command => do + let visibility : Visibility := if protect.isSome then .protected else .regular let resolved ← resolveGlobalConstNoOverloadWithInfo name let const ← getConstInfo resolved let (parent, base) ← match resolved with @@ -206,5 +213,7 @@ elab (name := aliasLRDots) doc:(docComment)? "alias " name:ident " ↔ " tk:".." let forward := String.intercalate "_of_" components.reverse let backward := String.intercalate "_of_" components Command.liftTermElabM do - aliasIff doc const tk (.str parent forward) (isForward := true) - aliasIff doc const tk (.str parent backward) (isForward := false) + let declName ← applyVisibility visibility (.str parent forward) + aliasIff doc const tk declName (isForward := true) + let declName ← applyVisibility visibility (.str parent backward) + aliasIff doc const tk declName (isForward := false)