Lean4
/-- Transform the declaration `src` and all declarations `pre._proof_i` occurring in `src`
using the transforms dictionary.
`replace_all`, `trace`, `ignore` and `reorder` are configuration options.
`pre` is the declaration that got the `@[to_additive]` attribute and `tgt_pre` is the target of this
declaration. -/
partial def transformDeclAux (cfg : Config) (pre tgt_pre : Name) : Name → CoreM Unit := fun src ↦ do
let env ← getEnv
trace[to_additive_detail]"visiting {src}"
if (findTranslation? env src).isSome && src != pre then
return
-- if this declaration is not `pre` and not an internal declaration, we return an error,
-- since we should have already translated this declaration.
if src != pre && !src.isInternalDetail then
throwError "The declaration {pre } depends on the declaration {src } which is in the namespace \
{pre }, but does not have the `@[to_additive]` attribute. This is not supported.\n\
Workaround: move {src} to a different namespace."
let tgt ← findTargetName env src pre tgt_pre
if env.contains tgt then
if tgt == src then
-- Note: this can happen for equation lemmas of declarations without `@[to_additive]`.
trace[to_additive_detail]"Auxiliary declaration {src} will be translated to itself."
else
trace[to_additive_detail]"Already visited {tgt } as translation of {src}."
return
let srcDecl ← getConstInfo src
let srcDecl ←
MetaM.run' do
declUnfoldAuxLemmas srcDecl
for n in findAuxDecls srcDecl.type pre do
transformDeclAux cfg pre tgt_pre n
if let some value := srcDecl.value? then
for n in findAuxDecls value pre do
transformDeclAux cfg pre tgt_pre n
if let .opaqueInfo { value, .. } := srcDecl then
for n in findAuxDecls value pre do
transformDeclAux cfg pre tgt_pre n
if !pre.isPrefixOf src then
insertTranslation src tgt
let trgDecl : ConstantInfo ←
MetaM.run' <|
if src == pre then updateDecl tgt srcDecl cfg.reorder cfg.dontTranslate else updateDecl tgt srcDecl [] []
let value ←
match trgDecl with
| .thmInfo { value, .. } | .defnInfo { value, .. } | .opaqueInfo { value, .. } =>
pure value
| _ =>
throwError "Expected {tgt} to have a value."
trace[to_additive]"generating\n{tgt } : {trgDecl.type } :=\n {value}"
try
-- make sure that the type is correct,
-- and emit a more helpful error message if it fails
MetaM.run' <| check value
catch
| Exception.error _ msg =>
throwError "@[to_additive] failed. \
The translated value is not type correct. For help, see the docstring \
of `to_additive.attr`, section `Troubleshooting`. \
Failed to add declaration\n{tgt }:\n{msg}"
| _ =>
panic!
"unreachable"
-- "Refold" all the aux lemmas that we unfolded.
let trgDecl ← MetaM.run' <| declAbstractNestedProofs trgDecl
if isNoncomputable env src then
addDecl trgDecl.toDeclaration!
setEnv <| addNoncomputable (← getEnv) tgt
else
addAndCompile trgDecl.toDeclaration! (logCompileErrors := (IR.findEnvDecl env src).isSome)
if let .defnDecl { hints := .abbrev, .. } := trgDecl.toDeclaration! then
if (← getReducibilityStatus src) == .reducible then
setReducibilityStatus tgt .reducible
if Compiler.getInlineAttribute? (← getEnv) src == some .inline then
MetaM.run' <| Meta.setInlineAttribute tgt
addDeclarationRangesFromSyntax tgt (← getRef) cfg.ref
if isProtected (← getEnv) src then
setEnv <| addProtected (← getEnv) tgt
if defeqAttr.hasTag (← getEnv) src then
defeqAttr.setTag tgt
if let some matcherInfo← getMatcherInfo? src then
/-
Use `Match.addMatcherInfo tgt matcherInfo`
once https://github.com/leanprover/lean4/pull/5068 is in
-/
modifyEnv fun env => Match.Extension.addMatcherInfo env tgt matcherInfo
enableRealizationsForConst tgt
