perf(to_dual): first try translating without inserting casts (#35131)

This PR addresses the performance regression introduced by #32438. The problem is that deciding where casts need to be inserted is an expensive operation (similarly expensive to kernel type checking). I expect that in category theory this will be particularly significant.

Most uses of `to_dual` don't need any casts to be inserted at all. So, it is more efficient to simply first try translating without inserting casts. And if that fails, we insert casts and then try again.

So after this PR, in the failure case, `to_dual` will check the term 4 times:
- first try the translation without casts
- then determine where casts should go
- then try the translation of this
- then use `Meta.check` to get a nicer error message.

This is OK, since the failure case is not the performance critical case.

Author: JovanGerb

Mathlib/Tactic/Translate/Core.lean

@@ -563,26 +563,68 @@ def applyReplacementLambda (t : TranslateData) (dontTranslate : List Nat) (e : E
 
 /-- Run `applyReplacementFun` on the given `srcDecl` to make a new declaration with name `tgt`. -/
 def updateDecl (t : TranslateData) (tgt : Name) (srcDecl : ConstantInfo)
-    (reorder : Reorder) (dont : List Nat) : MetaM ConstantInfo := do
+    (reorder : Reorder) (dont : List Nat)
+    (unfoldBoundaries? : Option UnfoldBoundary.UnfoldBoundaries) : MetaM ConstantInfo := do
   let mut decl := srcDecl.updateName tgt
   if reorder.any (·.contains 0) then
     decl := decl.updateLevelParams decl.levelParams.swapFirstTwo
   let mut value := decl.value! (allowOpaque := true)
-  if let some b := t.unfoldBoundaries? then
+  if let some b := unfoldBoundaries? then
     value ← b.cast (← b.insertBoundaries value t.attrName) decl.type t.attrName
   trace[translate] "Value before translation:{indentExpr value}"
   value ← reorderLambda reorder <| ← applyReplacementLambda t dont value
-  if let some b := t.unfoldBoundaries? then
+  if let some b := unfoldBoundaries? then
     value ← b.unfoldInsertions value
   decl := decl.updateValue value
   let mut type := decl.type
-  if let some b := t.unfoldBoundaries? then
+  if let some b := unfoldBoundaries? then
     type ← b.insertBoundaries decl.type t.attrName
   type ← reorderForall reorder <| ← applyReplacementForall t dont <| renameBinderNames t type
-  if let some b := t.unfoldBoundaries? then
+  if let some b := unfoldBoundaries? then
     type ← b.unfoldInsertions type
   return decl.updateType type
 
+/-- Translate the source declaration and then run `addDecl`. If the kernel throws an error,
+try to emit a better error message.
+
+For efficiency in `to_dual`, we first run `updateDecl` without any `UnfoldBoundaries`,
+and only if that fails do we try to include them.
+The reason is that in the most common case, `to_dual` succeeds without needing to insert
+unfold boundaries, and figuring out whether to insert them can be quite expensive. -/
+def updateAndAddDecl (t : TranslateData) (tgt : Name) (srcDecl : ConstantInfo)
+    (reorder : Reorder) (dont : List Nat) : MetaM ConstantInfo :=
+  -- Set `Elab.async` to `false` so that we can catch kernel errors.
+  withOptions (Elab.async.set · false) do
+  let decl ←
+    if let some unfoldBoundaries := t.unfoldBoundaries? then
+      let env ← getEnv
+      -- First attempt to generate the translation without unfold boundaries.
+      let declAttempt ← updateDecl t tgt srcDecl reorder dont none
+      try
+        addDecl declAttempt.toDeclaration!
+        trace[translate] "generating\n{tgt} : {declAttempt.type} :=\
+          {indentExpr <| declAttempt.value! (allowOpaque := true)}"
+        return declAttempt -- early return
+      catch _ =>
+        setEnv env
+        updateDecl t tgt srcDecl reorder dont (unfoldBoundaries.getState env)
+    else
+      updateDecl t tgt srcDecl reorder dont none
+  trace[translate] "generating\n{tgt} : {decl.type} :=\
+    {indentExpr <| decl.value! (allowOpaque := true)}"
+  try
+    addDecl decl.toDeclaration!
+    return decl
+  catch ex =>
+    try
+      withoutExporting <| check (decl.value! (allowOpaque := true))
+    catch ex =>
+      throwError "@[{t.attrName}] failed to add declaration `{decl.name}`.\n  \
+        The translated value is not type correct.\n  \
+        For help, see the docstring of `to_additive`, section `Troubleshooting`.\n\
+        {ex.toMessageData}"
+    throwError "@[{t.attrName}] failed. Nested error message:\n{ex.toMessageData}"
+
 /--
 Find the argument of `nm` that appears in the first translatable (type-class) argument.
 Returns 1 if there are no types with a translatable class as arguments.
@@ -702,26 +744,10 @@ partial def transformDeclRec (t : TranslateData) (ref : Syntax) (pre tgt_pre src
       let namesSrc := (← getConstInfo src).type.getForallBinderNames
       pure <| dontTranslate.filterMap (namesPre[·]? >>= namesSrc.idxOf?)
   -- now transform the source declaration
-  let trgDecl ← MetaM.run' <| updateDecl t tgt srcDecl reorder dontTranslate
-  if src == pre && srcDecl.isThm && trgDecl.type == srcDecl.type then
+  let tgtDecl ← MetaM.run' <| updateAndAddDecl t tgt srcDecl reorder dontTranslate
+  if src == pre && srcDecl.isThm && tgtDecl.type == srcDecl.type then
     Linter.logLintIf linter.translateRedundant ref m!"`{t.attrName}` did not change the type \
       of theorem `{.ofConstName src}`. Please remove the attribute."
-  let value := trgDecl.value! (allowOpaque := true)
-  trace[translate] "generating\n{tgt} : {trgDecl.type} :=\n  {value}"
-  try
-    -- set `Elab.async` to `false` in order to be able to catch kernel errors
-    withOptions (Elab.async.set · false) do
-      addDecl trgDecl.toDeclaration!
-  catch ex =>
-    -- Try to emit a better error message if the kernel throws an error.
-    try
-      withoutExporting <| MetaM.run' <| check value
-    catch ex =>
-      throwError "@[{t.attrName}] failed. \
-        The translated value is not type correct. For help, see the docstring \
-        of `to_additive`, section `Troubleshooting`. \
-        Failed to add declaration\n{tgt}:\n{ex.toMessageData}"
-    throwError "@[{t.attrName}] failed. Nested error message:\n{ex.toMessageData}"
   /- If `src` is explicitly marked as `noncomputable`, then add the new decl as a declaration but
   do not compile it, and mark is as noncomputable. Otherwise, only log errors in compiling if `src`
   has executable code.
@@ -740,8 +766,8 @@ partial def transformDeclRec (t : TranslateData) (ref : Syntax) (pre tgt_pre src
     if isMarkedMeta (← getEnv) src then
       -- We need to mark `tgt` as `meta` before running `compileDecl`
       modifyEnv (markMeta · tgt)
-    compileDecl trgDecl.toDeclaration! (logErrors := (IR.findEnvDecl (← getEnv) src).isSome)
-  if let .defnInfo { hints := .abbrev, .. } := trgDecl then
+    compileDecl tgtDecl.toDeclaration! (logErrors := (IR.findEnvDecl (← getEnv) src).isSome)
+  if let .defnInfo { hints := .abbrev, .. } := tgtDecl then
     if (← getReducibilityStatus src) == .reducible then
       setReducibilityStatus tgt .reducible
     if Compiler.getInlineAttribute? (← getEnv) src == some .inline then
@@ -917,7 +943,8 @@ partial def checkExistingType (t : TranslateData) (src tgt : Name) (cfg : Config
     throwError "`{t.attrName}` validation failed:\n  expected {srcDecl.levelParams.length} \
       universe levels, but '{tgt}' has {tgtDecl.levelParams.length} universe levels"
   let mut srcType := srcDecl.type
-  if let some b := t.unfoldBoundaries? then
+  let unfoldBoundaries? ← t.unfoldBoundaries?.mapM (return ·.getState (← getEnv))
+  if let some b := unfoldBoundaries? then
     srcType ← b.insertBoundaries srcType t.attrName
   srcType ← applyReplacementForall t cfg.dontTranslate srcType
   let reorder' := guessReorder srcType tgtDecl.type
@@ -942,7 +969,7 @@ partial def checkExistingType (t : TranslateData) (src tgt : Name) (cfg : Config
       If you need to give a hint to `{t.attrName}` to translate expressions involving `{src}`,\n\
       use `{t.attrName}_do_translate` instead"
   srcType ← reorderForall reorder srcType
-  if let some b := t.unfoldBoundaries? then
+  if let some b := unfoldBoundaries? then
     srcType ← b.unfoldInsertions srcType
   if reorder.any (·.contains 0) then
     srcDecl := srcDecl.updateLevelParams srcDecl.levelParams.swapFirstTwo

Mathlib/Tactic/Translate/UnfoldBoundary.lean

@@ -123,7 +123,7 @@ def mkAppWithCast (b : UnfoldBoundaries) (f a : Expr) : SimpM Expr :=
     return f.app (← mkCast b a d)
 
 /-- Modify `e` so that it has type `expectedType` if the constants in `b` cannot be unfolded. -/
-def UnfoldBoundaries.cast (b : UnfoldBoundaries) (e expectedType : Expr) (attr : Name) :
+public def UnfoldBoundaries.cast (b : UnfoldBoundaries) (e expectedType : Expr) (attr : Name) :
     MetaM Expr :=
   run b <|
   try
@@ -137,7 +137,7 @@ def UnfoldBoundaries.cast (b : UnfoldBoundaries) (e expectedType : Expr) (attr :
 Note: it may be that `e` contains some constant whose type is not well typed in this setting.
 We don't make an effort to replace such constants.
 It seems that this approximation works well enough. -/
-def UnfoldBoundaries.insertBoundaries (b : UnfoldBoundaries) (e : Expr) (attr : Name) :
+public def UnfoldBoundaries.insertBoundaries (b : UnfoldBoundaries) (e : Expr) (attr : Name) :
     MetaM Expr :=
   run b <| Meta.transform e (post := fun e ↦ e.withApp fun f args =>
     try
@@ -147,7 +147,7 @@ def UnfoldBoundaries.insertBoundaries (b : UnfoldBoundaries) (e : Expr) (attr :
         well typed\n\n{ex.toMessageData}")
 
 /-- Unfold all of the auxiliary functions that were inserted as unfold boundaries. -/
-def UnfoldBoundaries.unfoldInsertions (e : Expr) (b : UnfoldBoundaries) : CoreM Expr :=
+public def UnfoldBoundaries.unfoldInsertions (e : Expr) (b : UnfoldBoundaries) : CoreM Expr :=
   -- This is the same as `Meta.deltaExpand`, but with an extra beta reduction.
   Core.transform e fun e => do
     if let some e ← delta? e b.insertionFuns.contains then
@@ -182,19 +182,4 @@ public def registerUnfoldBoundaryExt : IO UnfoldBoundaryExt := do
     addImportedFn as := as.foldl (Array.foldl (·.insert ·)) {}
   }
 
-@[inherit_doc UnfoldBoundaries.cast]
-public def UnfoldBoundaryExt.cast (b : UnfoldBoundaryExt) (e expectedType : Expr) (attr : Name) :
-    MetaM Expr := do
-  (b.getState (← getEnv)).cast e expectedType attr
-
-@[inherit_doc UnfoldBoundaries.insertBoundaries]
-public def UnfoldBoundaryExt.insertBoundaries (b : UnfoldBoundaryExt) (e : Expr) (attr : Name) :
-    MetaM Expr := do
-  (b.getState (← getEnv)).insertBoundaries e attr
-
-@[inherit_doc UnfoldBoundaries.unfoldInsertions]
-public def UnfoldBoundaryExt.unfoldInsertions (e : Expr) (b : UnfoldBoundaryExt) : CoreM Expr := do
-  (b.getState (← getEnv)).unfoldInsertions e
-
-
 end Mathlib.Tactic.UnfoldBoundary

MathlibTest/ToDual.lean

@@ -32,8 +32,9 @@ attribute [to_dual existing] Lattice.toSemilatticeInf
 
 -- we still cannot reorder arguments of arguments, so `SemilatticeInf.mk` is not translatable
 /--
-error: @[to_dual] failed. The translated value is not type correct. For help, see the docstring of `to_additive`, section `Troubleshooting`. Failed to add declaration
-instSemilatticeSupOfForallLeForallMax:
+error: @[to_dual] failed to add declaration `instSemilatticeSupOfForallLeForallMax`.
+  The translated value is not type correct.
+  For help, see the docstring of `to_additive`, section `Troubleshooting`.
 Application type mismatch: The argument
   le_inf
 has type