Lean4
/-- Execute the projection renamings (and turning off projections) as specified by `rules`. -/
def applyProjectionRules (projs : Array ParsedProjectionData) (rules : Array ProjectionRule) :
CoreM (Array ParsedProjectionData) := do
let projs : Array ParsedProjectionData :=
rules.foldl (init := projs) fun projs rule ↦
match rule with
| .rename strName strStx newName newStx =>
if (projs.map (·.newName)).contains strName then
projs.map fun proj ↦
if proj.newName == strName then
{ proj with newName, newStx, strStx := if proj.strStx.isMissing then strStx else proj.strStx }
else proj
else projs.push { strName, strStx, newName, newStx }
| .erase nm stx =>
if (projs.map (·.newName)).contains nm then
projs.map fun proj ↦
if proj.newName = nm then
{ proj with isDefault := false, strStx := if proj.strStx.isMissing then stx else proj.strStx }
else proj
else projs.push { strName := nm, newName := nm, strStx := stx, newStx := stx, isDefault := false }
| .add nm stx =>
if (projs.map (·.newName)).contains nm then
projs.map fun proj ↦
if proj.newName = nm then
{ proj with isDefault := true, strStx := if proj.strStx.isMissing then stx else proj.strStx }
else proj
else projs.push { strName := nm, newName := nm, strStx := stx, newStx := stx }
| .prefix nm stx =>
if (projs.map (·.newName)).contains nm then
projs.map fun proj ↦
if proj.newName = nm then
{ proj with isPrefix := true, strStx := if proj.strStx.isMissing then stx else proj.strStx }
else proj
else projs.push { strName := nm, newName := nm, strStx := stx, newStx := stx, isPrefix := true }
trace[simps.debug]"Projection info after applying the rules: {projs}."
unless (projs.map (·.newName)).toList.Nodup do
throwError"\
Invalid projection names. Two projections have the same name.\n\
This is likely because a custom composition of projections was given the same name as an \
existing projection. Solution: rename the existing projection (before naming the \
custom projection)."
pure projs
