[ elab ] Support more applicative traversals of TTImp

[buzden]

Description

I propose to allow a bit more applicable, applicative mapping of TTImps, which generalises existing mapMTTImp way.

Proposed way allows you to do, for example, the following. Since traversal goes bottom up, from leaves up to the root, there might be not enough information of whether some transformation should be done, or not. Consider you want some transformation happen, but want to cancel it if some condition happens. You may need an original value at this point. The proposed addition of mapMMTTImp (along with existing mapMTTImp) allows this:

record WithOrig a where
  constructor W
  orig : a
  main : Lazy a

Functor WithOrig where
  map f = {orig $= f, main $= f}

Applicative WithOrig where
  pure x = W x x
  W fo fm <*> W xo xm = W (fo xo) (fm xm)

whateverTransformation : TTImp -> TTImp

condTrans : WithOrig TTImp -> WithOrig TTImp
condTrans wo = if cond wo.orig then wo else {main $= whateverTransformation} wo

Running mapMMTTImp condTrans expr, you have both original subexpression and the transformed one inside the condTrans function, allowing you to control precisely whether or not any particular change should be done.

Should this change go in the CHANGELOG?

• If this is a fix, user-facing change, a compiler change, or a new paper
  implementation, I have updated CHANGELOG.md (and potentially also
  CONTRIBUTORS.md).

[buzden]

I also updated one test to reduce the need of constant updates of its golden value on every standard library change, the second commit is for that.

[gallais]

Looks good to me. Can we call it mapATTImp instead though?

[buzden]

Looks good to me. Can we call it mapATTImp instead though?

Sure, done.