simproc test for whether expression changed

Stream: mathlib4

[Heather Macbeth]

I'm writing my first simproc and there are many gaps in my knowlege. Here's a particular issue I am currently encountering: When the simproc runs on an expression and returns .visit, it is supposed to check whether the simproc run actually changed the expression: if unchanged we continue, if changed then we send the expression back to the main loop, e.g. to see if some simp-lemmas now apply.

I believe this is the line where simp checks whether the simproc changed the expression. The check is done at the level of literal equality (==) of expressions.

In some of my tests, the simproc gets run twice on seemingly identical impressions, apparently because they are not literally equal (e.g. the simproc has changed an occurrence of exponentiation to a different Monoid ℚ instance).

Is this a common issue? Is it expected that simprocs be lightweight enough that running them repeatedly is harmless?

[Heather Macbeth]

BTW, the simproc is (experimentally) a replacement for field_simp! The context is that @Arend Mellendijk @Michael Rothgang and I have been rewriting field_simp to follow a (hopefully smarter, faster and more flexible) algorithm.

The old field_simp doesn't just clear denominators: it's implemented on top of simp and it does regular simp-ing, too. For example,

-- no denominators cleared here, just simp-ing
example {R} [Ring R] (f : ℚ →+* R) (a b c : ℚ) :
    f (a * b + c) = f a * f b + f c := by
  field_simp

To preserve this behaviour, which users have come to expect, I was thinking of implementing the new field_simp as a simproc; that way it too can be wrapped into a normal simp call.