Lean4
/-- Auxiliary function for `getRawProjections`.
Generates the default projection, and looks for a custom projection declared by the user,
and replaces the default projection with the custom one, if it can find it. -/
def findProjection (str : Name) (proj : ParsedProjectionData) (rawUnivs : List Level) : CoreM ParsedProjectionData := do
let env ← getEnv
let (rawExpr, nrs) ← MetaM.run' <| getCompositeOfProjections str proj.strName.lastComponentAsString
if !proj.strStx.isMissing then
_ ← MetaM.run' <| TermElabM.run' <| addTermInfo proj.strStx rawExpr
trace[simps.debug]"Projection {proj.newName } has default projection {rawExpr } and
uses projection indices {nrs}"
let customName := str ++ `Simps ++ proj.newName
match env.find? customName with
| some d@(.defnInfo _) =>
let customProj := d.instantiateValueLevelParams! rawUnivs
trace[simps.verbose]"found custom projection for {proj.newName }:{indentExpr customProj}"
match (← MetaM.run' <| isDefEq customProj rawExpr) with
| true =>
_ ← MetaM.run' <| TermElabM.run' <| addTermInfo proj.newStx <| ← mkConstWithLevelParams customName
pure { proj with expr? := some customProj, projNrs := nrs, isCustom := true }
| false =>
-- if the type of the Expression is different, we show a different error message, because
-- (in Lean 3) just stating that the expressions are different is quite unhelpful
let customProjType ← MetaM.run' (inferType customProj)
let rawExprType ← MetaM.run' (inferType rawExpr)
if (← MetaM.run' (isDefEq customProjType rawExprType)) then
throwError "Invalid custom projection:{(indentExpr customProj)}\n\
Expression is not definitionally equal to {indentExpr rawExpr}"
else
throwError "Invalid custom projection:{(indentExpr customProj)}\n\
Expression has different type than {(str ++ proj.strName)}. Given type:\
{(indentExpr customProjType)}\nExpected type:{indentExpr rawExprType}\n\
Note: make sure order of implicit arguments is exactly the same."
| _ =>
_ ← MetaM.run' <| TermElabM.run' <| addTermInfo proj.newStx rawExpr
pure { proj with expr? := some rawExpr, projNrs := nrs }
