refactor: add polymorphic methods for updating/querying reducibility status

src/Lean/Elab/Structure.lean

@@ -441,7 +441,7 @@ private def addDefaults (lctx : LocalContext) (defaultAuxDecls : Array (Name ×
       /- The identity function is used as "marker". -/
       let value ← mkId value
       mkAuxDefinition declName type value (zeta := true)
-      modifyEnv fun env => setReducibilityStatus env declName ReducibilityStatus.reducible
+      setReducibleAttribute declName
 
 private def elabStructureView (view : StructView) : TermElabM Unit := do
   let numExplicitParams := view.params.size

src/Lean/Meta/Basic.lean

@@ -269,11 +269,6 @@ def shouldReduceReducibleOnly : m Bool := liftMetaM do
 def getTransparency : m TransparencyMode := liftMetaM do
   return (← read).config.transparency
 
--- Remark: wanted to use `private`, but in the C++ parser, `private` declarations do not shadow outer public ones.
--- TODO: fix this bug
-def isReducible (constName : Name) : MetaM Bool := do
-  return Lean.isReducible (← getEnv) constName
-
 def getMVarDecl (mvarId : MVarId) : m MetavarDecl := liftMetaM do
   let mctx ← getMCtx
   match mctx.findDecl? mvarId with
@@ -420,11 +415,18 @@ def getConst? (constName : Name) : MetaM (Option ConstantInfo) := do
   let env ← getEnv
   match env.find? constName with
   | some (info@(ConstantInfo.thmInfo _)) =>
-    condM shouldReduceAll (pure (some info)) (pure none)
+    if (← shouldReduceAll) then
+      pure (some info)
+    else
+      pure none
   | some (info@(ConstantInfo.defnInfo _)) =>
-    condM shouldReduceReducibleOnly
-      (condM (isReducible constName) (pure (some info)) (pure none))
-      (pure (some info))
+    if (← shouldReduceReducibleOnly) then
+      if (← isReducible constName) then
+        pure (some info)
+      else
+        pure none
+    else
+      pure (some info)
   | some info => pure (some info)
   | none      => throwUnknownConstant constName
 

src/Lean/Meta/ExprDefEq.lean

@@ -865,8 +865,8 @@ private def unfoldReducibeDefEq (tInfo sInfo : ConstantInfo) (t s : Expr) : Meta
   if (← shouldReduceReducibleOnly) then
     unfoldDefEq tInfo sInfo t s
   else
-    let tReducible ← Meta.isReducible tInfo.name
-    let sReducible ← Meta.isReducible sInfo.name
+    let tReducible ← isReducible tInfo.name
+    let sReducible ← isReducible sInfo.name
     if tReducible && !sReducible then
       unfold t (unfoldDefEq tInfo sInfo t s) fun t => isDefEqLeft tInfo.name t s
     else if !tReducible && sReducible then

src/Lean/ReducibilityAttrs.lean

@@ -19,19 +19,28 @@ builtin_initialize reducibilityAttrs : EnumAttributes ReducibilityStatus ←
      (`irreducible, "irreducible", ReducibilityStatus.irreducible)]
 
 @[export lean_get_reducibility_status]
-def getReducibilityStatus (env : Environment) (n : Name) : ReducibilityStatus :=
-  match reducibilityAttrs.getValue env n with
+def getReducibilityStatusImp (env : Environment) (declName : Name) : ReducibilityStatus :=
+  match reducibilityAttrs.getValue env declName with
   | some s => s
   | none   => ReducibilityStatus.semireducible
 
 @[export lean_set_reducibility_status]
-def setReducibilityStatus (env : Environment) (n : Name) (s : ReducibilityStatus) : Environment :=
-  match reducibilityAttrs.setValue env n s with
+def setReducibilityStatusImp (env : Environment) (declName : Name) (s : ReducibilityStatus) : Environment :=
+  match reducibilityAttrs.setValue env declName s with
   | Except.ok env => env
   | _ => env -- TODO(Leo): we should extend EnumAttributes.setValue in the future and ensure it never fails
 
-def isReducible (env : Environment) (n : Name) : Bool :=
-  match getReducibilityStatus env n with
+def getReducibilityStatus {m} [Monad m] [MonadEnv m] (declName : Name) : m ReducibilityStatus := do
+  return getReducibilityStatusImp (← getEnv) declName
+
+def setReducibilityStatus {m} [Monad m] [MonadEnv m] (declName : Name) (s : ReducibilityStatus) : m Unit := do
+  modifyEnv fun env => setReducibilityStatusImp env declName s
+
+def setReducibleAttribute {m} [Monad m] [MonadEnv m] (declName : Name) : m Unit := do
+  setReducibilityStatus declName ReducibilityStatus.reducible
+
+def isReducible {m} [Monad m] [MonadEnv m] (declName : Name) : m Bool := do
+  match ← getReducibilityStatus declName with
   | ReducibilityStatus.reducible => true
   | _ => false
 

tests/lean/run/meta2.lean

@@ -156,8 +156,8 @@ do print "----- tst7 -----";
 def tst9 : MetaM Unit :=
 do print "----- tst9 -----";
    let env ← getEnv;
-   print (toString $ Lean.isReducible env `Prod.fst);
-   print (toString $ Lean.isReducible env `HasAdd.add);
+   print (toString (← isReducible `Prod.fst))
+   print (toString (← isReducible `HasAdd.add))
    pure ()
 
 #eval tst9