From f374ef154e352cedd60d19d9c8fb233a873c16c2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 17 Jan 2025 10:43:10 -0800 Subject: [PATCH] refactor: move `ext` environment extension to `Lean.Meta.Tactic` --- src/Lean/Elab/Tactic/Ext.lean | 62 ++-------------------------- src/Lean/Meta/Tactic.lean | 1 + src/Lean/Meta/Tactic/Ext.lean | 76 +++++++++++++++++++++++++++++++++++ 3 files changed, 80 insertions(+), 59 deletions(-) create mode 100644 src/Lean/Meta/Tactic/Ext.lean diff --git a/src/Lean/Elab/Tactic/Ext.lean b/src/Lean/Elab/Tactic/Ext.lean index 837c8d61dc..0e94c18c6f 100644 --- a/src/Lean/Elab/Tactic/Ext.lean +++ b/src/Lean/Elab/Tactic/Ext.lean @@ -5,6 +5,7 @@ Authors: Gabriel Ebner, Mario Carneiro -/ prelude import Init.Ext +import Lean.Meta.Tactic.Ext import Lean.Elab.DeclarationRange import Lean.Elab.Tactic.RCases import Lean.Elab.Tactic.Repeat @@ -174,65 +175,8 @@ def realizeExtIffTheorem (extName : Name) : Elab.Command.CommandElabM Name := do ### Attribute -/ -/-- Information about an extensionality theorem, stored in the environment extension. -/ -structure ExtTheorem where - /-- Declaration name of the extensionality theorem. -/ - declName : Name - /-- Priority of the extensionality theorem. -/ - priority : Nat - /-- - Key in the discrimination tree, - for the type in which the extensionality theorem holds. - -/ - keys : Array DiscrTree.Key - deriving Inhabited, Repr, BEq, Hashable - -/-- The state of the `ext` extension environment -/ -structure ExtTheorems where - /-- The tree of `ext` extensions. -/ - tree : DiscrTree ExtTheorem := {} - /-- Erased `ext`s via `attribute [-ext]`. -/ - erased : PHashSet Name := {} - deriving Inhabited - -/-- The environment extension to track `@[ext]` theorems. -/ -builtin_initialize extExtension : - SimpleScopedEnvExtension ExtTheorem ExtTheorems ← - registerSimpleScopedEnvExtension { - addEntry := fun { tree, erased } thm => - { tree := tree.insertCore thm.keys thm, erased := erased.erase thm.declName } - initial := {} - } - -/-- Gets the list of `@[ext]` theorems corresponding to the key `ty`, -ordered from high priority to low. -/ -@[inline] def getExtTheorems (ty : Expr) : MetaM (Array ExtTheorem) := do - let extTheorems := extExtension.getState (← getEnv) - let arr ← extTheorems.tree.getMatch ty - let erasedArr := arr.filter fun thm => !extTheorems.erased.contains thm.declName - -- Using insertion sort because it is stable and the list of matches should be mostly sorted. - -- Most ext theorems have default priority. - return erasedArr.insertionSort (·.priority < ·.priority) |>.reverse - -/-- -Erases a name marked `ext` by adding it to the state's `erased` field and -removing it from the state's list of `Entry`s. - -This is triggered by `attribute [-ext] name`. --/ -def ExtTheorems.eraseCore (d : ExtTheorems) (declName : Name) : ExtTheorems := - { d with erased := d.erased.insert declName } - -/-- -Erases a name marked as a `ext` attribute. -Check that it does in fact have the `ext` attribute by making sure it names a `ExtTheorem` -found somewhere in the state's tree, and is not erased. --/ -def ExtTheorems.erase [Monad m] [MonadError m] (d : ExtTheorems) (declName : Name) : - m ExtTheorems := do - unless d.tree.containsValueP (·.declName == declName) && !d.erased.contains declName do - throwError "'{declName}' does not have [ext] attribute" - return d.eraseCore declName +abbrev extExtension := Meta.Ext.extExtension +abbrev getExtTheorems := Meta.Ext.getExtTheorems builtin_initialize registerBuiltinAttribute { name := `ext diff --git a/src/Lean/Meta/Tactic.lean b/src/Lean/Meta/Tactic.lean index e372e6aeff..604576f54c 100644 --- a/src/Lean/Meta/Tactic.lean +++ b/src/Lean/Meta/Tactic.lean @@ -41,3 +41,4 @@ import Lean.Meta.Tactic.FunInd import Lean.Meta.Tactic.Rfl import Lean.Meta.Tactic.Rewrites import Lean.Meta.Tactic.Grind +import Lean.Meta.Tactic.Ext diff --git a/src/Lean/Meta/Tactic/Ext.lean b/src/Lean/Meta/Tactic/Ext.lean new file mode 100644 index 0000000000..bb6ce28b0b --- /dev/null +++ b/src/Lean/Meta/Tactic/Ext.lean @@ -0,0 +1,76 @@ +/- +Copyright (c) 2021 Gabriel Ebner. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Gabriel Ebner, Mario Carneiro +-/ +prelude +import Init.Data.Array.InsertionSort +import Lean.Meta.DiscrTree + +namespace Lean.Meta.Ext + +/-! +### Environment extension for `ext` theorems +-/ + +/-- Information about an extensionality theorem, stored in the environment extension. -/ +structure ExtTheorem where + /-- Declaration name of the extensionality theorem. -/ + declName : Name + /-- Priority of the extensionality theorem. -/ + priority : Nat + /-- + Key in the discrimination tree, + for the type in which the extensionality theorem holds. + -/ + keys : Array DiscrTree.Key + deriving Inhabited, Repr, BEq, Hashable + +/-- The state of the `ext` extension environment -/ +structure ExtTheorems where + /-- The tree of `ext` extensions. -/ + tree : DiscrTree ExtTheorem := {} + /-- Erased `ext`s via `attribute [-ext]`. -/ + erased : PHashSet Name := {} + deriving Inhabited + +/-- The environment extension to track `@[ext]` theorems. -/ +builtin_initialize extExtension : + SimpleScopedEnvExtension ExtTheorem ExtTheorems ← + registerSimpleScopedEnvExtension { + addEntry := fun { tree, erased } thm => + { tree := tree.insertCore thm.keys thm, erased := erased.erase thm.declName } + initial := {} + } + +/-- Gets the list of `@[ext]` theorems corresponding to the key `ty`, +ordered from high priority to low. -/ +@[inline] def getExtTheorems (ty : Expr) : MetaM (Array ExtTheorem) := do + let extTheorems := extExtension.getState (← getEnv) + let arr ← extTheorems.tree.getMatch ty + let erasedArr := arr.filter fun thm => !extTheorems.erased.contains thm.declName + -- Using insertion sort because it is stable and the list of matches should be mostly sorted. + -- Most ext theorems have default priority. + return erasedArr.insertionSort (·.priority < ·.priority) |>.reverse + +/-- +Erases a name marked `ext` by adding it to the state's `erased` field and +removing it from the state's list of `Entry`s. + +This is triggered by `attribute [-ext] name`. +-/ +def ExtTheorems.eraseCore (d : ExtTheorems) (declName : Name) : ExtTheorems := + { d with erased := d.erased.insert declName } + +/-- +Erases a name marked as a `ext` attribute. +Check that it does in fact have the `ext` attribute by making sure it names a `ExtTheorem` +found somewhere in the state's tree, and is not erased. +-/ +def ExtTheorems.erase [Monad m] [MonadError m] (d : ExtTheorems) (declName : Name) : + m ExtTheorems := do + unless d.tree.containsValueP (·.declName == declName) && !d.erased.contains declName do + throwError "'{declName}' does not have [ext] attribute" + return d.eraseCore declName + +end Lean.Meta.Ext