From 2df35360eeabeba199d7171a2ab97d94b0b6a5c3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 3 May 2024 15:44:42 +0200 Subject: [PATCH] feat: validate reducibility attribute setting (#4052) and new option `set_option allowUnsafeReductibility true` to override validation. --------- Co-authored-by: Mario Carneiro --- src/Lean/Meta/LazyDiscrTree.lean | 1 - src/Lean/ReducibilityAttrs.lean | 85 ++++++++++++++--- tests/lean/run/1123.lean | 2 - .../lean/run/reducibilityAttrValidation.lean | 93 +++++++++++++++++++ tests/lean/run/rewrite.lean | 3 +- tests/lean/run/scopedLocalReducibility.lean | 2 +- tests/pkg/builtin_attr/UserAttr/Tst.lean | 2 +- 7 files changed, 168 insertions(+), 20 deletions(-) create mode 100644 tests/lean/run/reducibilityAttrValidation.lean diff --git a/src/Lean/Meta/LazyDiscrTree.lean b/src/Lean/Meta/LazyDiscrTree.lean index 14be19da8e..0d51b7388a 100644 --- a/src/Lean/Meta/LazyDiscrTree.lean +++ b/src/Lean/Meta/LazyDiscrTree.lean @@ -745,7 +745,6 @@ instance : Append (PreDiscrTree α) where end PreDiscrTree /-- Initial entry in lazy discrimination tree -/ -@[reducible] structure InitEntry (α : Type) where /-- Return root key for an entry. -/ key : Key diff --git a/src/Lean/ReducibilityAttrs.lean b/src/Lean/ReducibilityAttrs.lean index 2b46b63291..f843f0e4fc 100644 --- a/src/Lean/ReducibilityAttrs.lean +++ b/src/Lean/ReducibilityAttrs.lean @@ -16,6 +16,11 @@ inductive ReducibilityStatus where | reducible | semireducible | irreducible deriving Inhabited, Repr, BEq +def ReducibilityStatus.toAttrString : ReducibilityStatus → String + | .reducible => "[reducible]" + | .irreducible => "[irreducible]" + | .semireducible => "[semireducible]" + builtin_initialize reducibilityCoreExt : PersistentEnvExtension (Name × ReducibilityStatus) (Name × ReducibilityStatus) (NameMap ReducibilityStatus) ← registerPersistentEnvExtension { name := `reducibilityCore @@ -48,7 +53,7 @@ def getReducibilityStatusCore (env : Environment) (declName : Name) : Reducibili | none => .semireducible | none => (reducibilityCoreExt.getState env).find? declName |>.getD .semireducible -def setReducibilityStatusCore (env : Environment) (declName : Name) (status : ReducibilityStatus) (attrKind : AttributeKind) (currNamespace : Name) : Environment := +private def setReducibilityStatusCore (env : Environment) (declName : Name) (status : ReducibilityStatus) (attrKind : AttributeKind) (currNamespace : Name) : Environment := if attrKind matches .global then match env.getModuleIdxFor? declName with | some _ => @@ -65,15 +70,75 @@ def setReducibilityStatusCore (env : Environment) (declName : Name) (status : Re private def setReducibilityStatusImp (env : Environment) (declName : Name) (status : ReducibilityStatus) : Environment := setReducibilityStatusCore env declName status .global .anonymous +/- +TODO: it would be great if we could distinguish between the following two situations + +1- +``` +@[reducible] def foo := ... +``` + +2- +``` +def foo := ... +... +attribute [reducible] foo +``` + +Reason: the second one is problematic if user has add simp theorems or TC instances that include `foo`. +Recall that the discrimination trees unfold `[reducible]` declarations while indexing new entries. +-/ + +register_builtin_option allowUnsafeReducibility : Bool := { + defValue := false + descr := "enables users to modify the reducibility settings for declarations even when such changes are deemed potentially hazardous. For example, `simp` and type class resolution maintain term indices where reducible declarations are expanded." +} + +private def validate (declName : Name) (status : ReducibilityStatus) (attrKind : AttributeKind) : CoreM Unit := do + let suffix := "use `set_option allowUnsafeReducibility true` to override reducibility status validation" + unless allowUnsafeReducibility.get (← getOptions) do + match (← getConstInfo declName) with + | .defnInfo _ => + let statusOld := getReducibilityStatusCore (← getEnv) declName + match attrKind with + | .scoped => + throwError "failed to set reducibility status for `{declName}`, the `scoped` modifier is not recommended for this kind of attribute\n{suffix}" + | .global => + if (← getEnv).getModuleIdxFor? declName matches some _ then + throwError "failed to set reducibility status, `{declName}` has not been defined in this file, consider using the `local` modifier\n{suffix}" + match status with + | .reducible => + unless statusOld matches .semireducible do + throwError "failed to set `[reducible]`, `{declName}` is not currently `[semireducible]`, but `{statusOld.toAttrString}`\n{suffix}" + | .irreducible => + unless statusOld matches .semireducible do + throwError "failed to set `[irreducible]`, `{declName}` is not currently `[semireducible]`, but `{statusOld.toAttrString}`\n{suffix}" + | .semireducible => + throwError "failed to set `[semireducible]` for `{declName}`, declarations are `[semireducible]` by default\n{suffix}" + | .local => + match status with + | .reducible => + throwError "failed to set `[local reducible]` for `{declName}`, recall that `[reducible]` affects the term indexing datastructures used by `simp` and type class resolution\n{suffix}" + | .irreducible => + unless statusOld matches .semireducible do + throwError "failed to set `[local irreducible]`, `{declName}` is currently `{statusOld.toAttrString}`, `[semireducible]` expected\n{suffix}" + | .semireducible => + unless statusOld matches .irreducible do + throwError "failed to set `[local semireducible]`, `{declName}` is currently `{statusOld.toAttrString}`, `[irreducible]` expected\n{suffix}" + | _ => throwError "failed to set reducibility status, `{declName}` is not a definition\n{suffix}" + +private def addAttr (status : ReducibilityStatus) (declName : Name) (stx : Syntax) (attrKind : AttributeKind) : AttrM Unit := do + Attribute.Builtin.ensureNoArgs stx + validate declName status attrKind + let ns ← getCurrNamespace + modifyEnv fun env => setReducibilityStatusCore env declName status attrKind ns + builtin_initialize registerBuiltinAttribute { ref := by exact decl_name% name := `irreducible descr := "irreducible declaration" - add := fun declName stx attrKind => do - Attribute.Builtin.ensureNoArgs stx - let ns ← getCurrNamespace - modifyEnv fun env => setReducibilityStatusCore env declName .irreducible attrKind ns + add := addAttr .irreducible applicationTime := .afterTypeChecking } @@ -82,10 +147,7 @@ builtin_initialize ref := by exact decl_name% name := `reducible descr := "reducible declaration" - add := fun declName stx attrKind => do - Attribute.Builtin.ensureNoArgs stx - let ns ← getCurrNamespace - modifyEnv fun env => setReducibilityStatusCore env declName .reducible attrKind ns + add := addAttr .reducible applicationTime := .afterTypeChecking } @@ -94,10 +156,7 @@ builtin_initialize ref := by exact decl_name% name := `semireducible descr := "semireducible declaration" - add := fun declName stx attrKind => do - Attribute.Builtin.ensureNoArgs stx - let ns ← getCurrNamespace - modifyEnv fun env => setReducibilityStatusCore env declName .reducible attrKind ns + add := addAttr .semireducible applicationTime := .afterTypeChecking } diff --git a/tests/lean/run/1123.lean b/tests/lean/run/1123.lean index 0a3849f3eb..865c6691db 100644 --- a/tests/lean/run/1123.lean +++ b/tests/lean/run/1123.lean @@ -3,11 +3,9 @@ class OpAssoc (op : α → α → α) : Prop where abbrev op_assoc (op : α → α → α) [self : OpAssoc op] := self.op_assoc -@[reducible] structure SemigroupSig (α) where op : α → α → α -@[reducible] structure SemiringSig (α) where add : α → α → α mul : α → α → α diff --git a/tests/lean/run/reducibilityAttrValidation.lean b/tests/lean/run/reducibilityAttrValidation.lean new file mode 100644 index 0000000000..1c3d2d0e74 --- /dev/null +++ b/tests/lean/run/reducibilityAttrValidation.lean @@ -0,0 +1,93 @@ +def f (x : Nat) := x + 1 + +/-- +error: failed to set `[semireducible]` for `f`, declarations are `[semireducible]` by default +use `set_option allowUnsafeReducibility true` to override reducibility status validation +-/ +#guard_msgs in +attribute [semireducible] f + +attribute [reducible] f + +/-- +error: failed to set `[reducible]`, `f` is not currently `[semireducible]`, but `[reducible]` +use `set_option allowUnsafeReducibility true` to override reducibility status validation +-/ +#guard_msgs in +attribute [reducible] f -- should fail because of double reducible setting + +-- "Reset" `f` +set_option allowUnsafeReducibility true in +attribute [semireducible] f + +attribute [irreducible] f + +/-- +error: failed to set `[irreducible]`, `f` is not currently `[semireducible]`, but `[irreducible]` +use `set_option allowUnsafeReducibility true` to override reducibility status validation +-/ +#guard_msgs in +attribute [irreducible] f + +attribute [local semireducible] f + +/-- +error: failed to set `[local semireducible]`, `f` is currently `[semireducible]`, `[irreducible]` expected +use `set_option allowUnsafeReducibility true` to override reducibility status validation +-/ +#guard_msgs in +attribute [local semireducible] f + +attribute [local irreducible] f + +/-- +error: failed to set `[local irreducible]`, `f` is currently `[irreducible]`, `[semireducible]` expected +use `set_option allowUnsafeReducibility true` to override reducibility status validation +-/ +#guard_msgs in +attribute [local irreducible] f + +/-- +error: failed to set `[local reducible]` for `f`, recall that `[reducible]` affects the term indexing datastructures used by `simp` and type class resolution +use `set_option allowUnsafeReducibility true` to override reducibility status validation +-/ +#guard_msgs in +attribute [local reducible] f + +/-- +error: failed to set reducibility status, `Nat.add` has not been defined in this file, consider using the `local` modifier +use `set_option allowUnsafeReducibility true` to override reducibility status validation +-/ +#guard_msgs in +attribute [semireducible] Nat.add + +/-- +error: failed to set reducibility status, `Nat.add` has not been defined in this file, consider using the `local` modifier +use `set_option allowUnsafeReducibility true` to override reducibility status validation +-/ +#guard_msgs in +attribute [reducible] Nat.add + +/-- +error: failed to set reducibility status, `Nat.add` has not been defined in this file, consider using the `local` modifier +use `set_option allowUnsafeReducibility true` to override reducibility status validation +-/ +#guard_msgs in +attribute [irreducible] Nat.add + +/-- error: scoped attributes must be used inside namespaces -/ +#guard_msgs in +attribute [scoped reducible] Nat.add + +namespace Foo +/-- +error: failed to set reducibility status for `Nat.add`, the `scoped` modifier is not recommended for this kind of attribute +use `set_option allowUnsafeReducibility true` to override reducibility status validation +-/ +#guard_msgs in +attribute [scoped reducible] Nat.add + +set_option allowUnsafeReducibility true in +attribute [scoped reducible] Nat.add + +end Foo diff --git a/tests/lean/run/rewrite.lean b/tests/lean/run/rewrite.lean index dbee4e7b86..5802a27ea4 100644 --- a/tests/lean/run/rewrite.lean +++ b/tests/lean/run/rewrite.lean @@ -40,6 +40,7 @@ example : f 1 = f 2 := by example : f 1 = f 2 := by rw [s 1 3, s 3 4] -- Closes the goal via `rfl` +set_option allowUnsafeReducibility true -- For the remaining tests we prevent `rfl` from closing the goal. attribute [irreducible] f @@ -109,5 +110,3 @@ example : f 2 = f 0 := by -- we can return the problem to the user. rw [@t' 2 ?_] constructor - - diff --git a/tests/lean/run/scopedLocalReducibility.lean b/tests/lean/run/scopedLocalReducibility.lean index 48d31e40c1..3475b80b56 100644 --- a/tests/lean/run/scopedLocalReducibility.lean +++ b/tests/lean/run/scopedLocalReducibility.lean @@ -1,5 +1,5 @@ @[irreducible] def f (x : Nat) := x + 1 - +set_option allowUnsafeReducibility true /-- error: type mismatch rfl diff --git a/tests/pkg/builtin_attr/UserAttr/Tst.lean b/tests/pkg/builtin_attr/UserAttr/Tst.lean index 0df772ae7d..721e43b111 100644 --- a/tests/pkg/builtin_attr/UserAttr/Tst.lean +++ b/tests/pkg/builtin_attr/UserAttr/Tst.lean @@ -3,7 +3,7 @@ import UserAttr.BlaAttr @[bar] def f (x : Nat) := x + 2 @[bar] def g (x : Nat) := x + 1 -attribute [irreducible] myFun +attribute [local irreducible] myFun /-- error: type mismatch