add more options to monomorphization

Auto/Translation/Monomorphization.lean

@@ -33,6 +33,17 @@ register_option auto.mono.recordInstInst : Bool := {
   descr := "Whether to record instances of constants with the `instance` attribute"
 }
 
+register_option auto.mono.ciInstDefEq.mode : Meta.TransparencyMode := {
+  defValue := .default
+  descr := "Transparency level used when collecting definitional equality" ++
+    " arising from instance relations between `ConstInst`s"
+}
+
+register_option auto.mono.tyCan.mode : Meta.TransparencyMode := {
+  defValue := .reducible
+  descr := "Transparency level used when canonicalizing types"
+}
+
 namespace Auto
 
 inductive MonoMode where
@@ -463,6 +474,7 @@ where
         return false
       leadingForallQuasiMonomorphicAux (fvars.push xid)  bodyi
   | _ => return true
+
 /--
   Test whether a lemma is type monomorphic && universe monomorphic
     By universe monomorphic we mean `lem.params = #[]`
@@ -682,8 +694,9 @@ where
       let newCis ← collectConstInsts li.params #[] li.type
       for newCi in newCis do
         processConstInst newCi
-  bidirectionalOfInstanceEq (ci₁ ci₂ : ConstInst) : MetaM (Option (Expr × Expr)) :=
-    Meta.withNewMCtxDepth <| Meta.withDefault <| do
+  bidirectionalOfInstanceEq (ci₁ ci₂ : ConstInst) : MetaM (Option (Expr × Expr)) := do
+    let mode := auto.mono.ciInstDefEq.mode.get (← getOptions)
+    Meta.withNewMCtxDepth <| Meta.withTransparency mode <| do
       return (← Expr.instanceOf? (← ci₁.toExpr) (← ci₂.toExpr)) <|>
         (← Expr.instanceOf? (← ci₂.toExpr) (← ci₁.toExpr))
   isTrigger (cih : CiHead) :=
@@ -745,7 +758,8 @@ namespace FVarRep
 
   /-- Return : (reduce(e), whether reduce(e) contain bfvars) -/
   def processType (e : Expr) : FVarRepM (Expr × Bool) := do
-    let e ← MetaState.runMetaM <| prepReduceExpr e
+    let mode := auto.mono.tyCan.mode.get (← getOptions)
+    let e ← MetaState.runMetaM <| prepReduceExprWithMode e mode
     let bfvarSet ← getBfvarSet
     -- If `e` contains no bound variables
     if !e.hasAnyFVar bfvarSet.contains then

Auto/Translation/Reduction.lean

@@ -41,19 +41,22 @@ def unfoldProj (e : Expr) : MetaM Expr :=
     Meta.mkAppOptM sfi.projFn ((Array.mk nones).push struct)
   | _ => return e
 
-/-- This function is expensive -/
-partial def prepReduceExpr (term : Expr) : MetaM Expr := do
+def prepReduceExprWithMode (term : Expr) (mode : TransparencyMode) : MetaM Expr := do
   let red (e : Expr) : MetaM TransformStep := do
     let e := e.consumeMData
     let e ← Meta.whnf e
     return .continue e
-  let trMode := auto.redMode.get (← getOptions)
   -- Reduce
-  let term ← Meta.withTransparency trMode <| Meta.transform term (pre := red) (usedLetOnly := false)
+  let term ← Meta.withTransparency mode <| Meta.transform term (pre := red) (usedLetOnly := false)
   -- Unfold projection
   let term ← Meta.transform term (pre := fun e => do return .continue (← unfoldProj e))
   return term
 
+/-- This function is expensive -/
+def prepReduceExpr (term : Expr) : MetaM Expr := do
+  let mode := auto.redMode.get (← getOptions)
+  prepReduceExprWithMode term mode
+
 /--
   We assume that all defeq facts have the form
     `∀ (x₁ : ⋯) ⋯ (xₙ : ⋯), c ... = ...`