Make forcing builtin functions pure and work-free

[zliu41]

and added a test.

[michaelpj]

why?

[michaelpj]

Forcing builtin functions is currently work-free. I don't know that there's any reason in principle why we couldn't have a builtin with only type arguments. If this is a constraint we should make sure we're checking it somewhere otherwise this could go wrong later.

[zliu41]

Forcing builtin functions is currently work-free

If it is currently work-free then I think we should do this.

The reason I want to do this is because it is needed by CSE. It's a bad idea to consider work-free items like force ifThenElse as a common expression. If isWorkFree doesn't work as it should, then I'd have to implement a totally separate one just for CSE.

[michaelpj]

If it is currently work-free then I think we should do this.

Or we could come up with a more precise version. Forcing a builtin is work-free if the builtin does not have a single type argument.

You also possibly need to handle repeated forcing. In fact, doesn't the work-free check already look at whether the builtin is saturated, which should subsume this?

[zliu41]

You also possibly need to handle repeated forcing.

This is already being checked. This is what splitForces is for.

In fact, doesn't the work-free check already look at whether the builtin is saturated, which should subsume this?

No - the additional check I added does this; it isn't done currently.

[michaelpj]

Ah, it's behind the PIR one. Seems better to bring it in line with the PIR one, which I think handles all builtin applications correctly? https://github.com/input-output-hk/plutus/blob/master/plutus-core/plutus-ir/src/PlutusIR/Purity.hs#L149

[zliu41]

Seems better to bring it in line with the PIR one, which I think handles all builtin applications correctly?

Yeah that seems the right thing to do

[zliu41]

Ok, I'll put this down as a good first task for newhires