Lean4
/-- If a structure has a field that corresponds to a coercion to functions or sets, or corresponds
to notation, find the custom projection that uses this coercion or notation.
Returns the custom projection and the name of the projection used.
We catch most errors this function causes, so that we don't fail if an unrelated projection has
an applicable name. (e.g. `Iso.inv`)
Implementation note: getting rid of TermElabM is tricky, since `Expr.mkAppOptM` doesn't allow to
keep metavariables around, which are necessary for `OutParam`. -/
def findAutomaticProjectionsAux (str : Name) (proj : ParsedProjectionData) (args : Array Expr) :
TermElabM <| Option (Expr × Name) := do
if let some ⟨className, isNotation, findArgs⟩ := notationClassAttr.find? (← getEnv) proj.strName then
let findArgs ← unsafe evalConst findArgType findArgs
let classArgs ←
try
findArgs str className args
catch ex =>
trace[simps.debug]"Projection {proj.strName } is likely unrelated to the projection of \
{className }:\n{ex.toMessageData}"
return none
let classArgs ←
classArgs.mapM fun e =>
match e with
| none => mkFreshExprMVar none
| some e => pure e
let classArgs := classArgs.map Arg.expr
let projName := (getStructureFields (← getEnv) className)[0]!
let projName := className ++ projName
let eStr := mkAppN (← mkConstWithLevelParams str) args
let eInstType ←
try
withoutErrToSorry (elabAppArgs (← Term.mkConst className) #[] classArgs none true false)
catch ex =>
trace[simps.debug]"Projection doesn't have the right type for the automatic projection:\n\
{ex.toMessageData}"
return none
return
←
withLocalDeclD `self eStr fun instStr ↦ do
trace[simps.debug]"found projection {proj.strName }. Trying to synthesize {eInstType}."
let eInst ←
try
synthInstance eInstType
catch ex =>
trace[simps.debug]"Didn't find instance:\n{ex.toMessageData}"
return none
let projExpr ← elabAppArgs (← Term.mkConst projName) #[] (classArgs.push <| .expr eInst) none true false
let projExpr ← mkLambdaFVars (if isNotation then args.push instStr else args) projExpr
let projExpr ← instantiateMVars projExpr
return (projExpr, projName)
return none
