Trace removal re-implemented as a IR rewrite rule

[Unisay]

• Rename: PlutusIR.Transform.RewriteRules.Rules to PlutusIR.Transform.RewriteRules.Internal
  • Removed exported RewriteRules constructor in favor of unRewriteRules.
• Depending on the "remove-trace" flag a rewrite rule is added to the list of default rules;
• Removed a special case inside Builtin module responsible for rewriting traces;
• Re-implemented "remove-trace" functionality as an IR rewrite rule;

[michaelpj]

Removed exported RewriteRules constructor in favor of unRewriteRules

I'm not sure what this gets us?

[Unisay]

I'm not sure what this gets us?

I want to keep RewriteRules implementation hidden, so that we can change it, say, from a one big step to a list of small steps, e.g. each one having a name, without breaking call sites.

[michaelpj]

We control all the use sites, so I'm not sure that the abstraction buys us much here. I certainly agree with exposing more limited APIs to consumers that you don't control, but in this case I don't really see the point.

[bezirg]

We control all the use sites, so I'm not sure that the abstraction buys us much here. I certainly agree with exposing more limited APIs to consumers that you don't control, but in this case I don't really see the point.

I also don't see the point

[bezirg]

This rewrite rule seems to do the job, except a small peculiarity (which I think @michaelpj does not care about :)):

We should make sure that the _msg is evaluated for its effects.
For example:

trace (appenString "_msg" (error ()) arg will become => arg ,where the correct thing is to throw instead.

To make sure that the _msg is evaluated before continuing to arg, take a look at UnConstrConstrData rewrite rule.
I think you have to change your implementation to something like

B Builtin.Trace `I` _ty `A` _msg `A` arg ->  (stringtype,msg) `seQ` arg

The seQ (and other helpers from Common), should generate Haskell.seq-like code iff not-isPure , so the generated code will not look that bad.

Also, if you decide to do what I suggest above, can you add 1,2 tests that exercise this rewrite-rule ?

[michaelpj]

No, it's deliberate that it throws away the message, indeed that's a major point of the remove-trace option: it removes trace entirely, such that all the message strings become dead and can also be removed. If we still evaluate the message arguments then we may not be able to remove them (if we think the evaluation might have an effect).

[michaelpj]

Worth a comment, though!

[bezirg]

You see, I knew @michaelpj would not like it :D.

I am fine with it, let's add a comment though that we are deviating slightly here where we strip completely even if the _msg is not pure

[michaelpj]

I guess I don't hate the idea of keeping the semantics and evaluating the message. If someone writes trace (error) 1, it probably should still blow up. The problem is that we are not going to do well at noticing that string manipulation is pure, and I do think a lot of the utility of this option comes from it enabling a lot of string stripping.