Derive PMATCH thms for relevant parts of compiler definition

[myreen]

Certain case expressions are huge within HOL. For such case expressions, the translator produces huge CakeML output, which in turn is highly likely to cause problems for the compiler bootstrapping.

One way to make the translator produce better output is to introduce PMATCH-reformulations of the exploding case expressions and use the reformulations in the translator. This can make the CakeML output much smaller and hence easier for the bootstrapping process to digest.

The task for this issue is to look through the compiler definitions for suspicious looking case expressions, e.g. deeply nested matches and wildcards:

foo x =
  case x of 
  | SOME [x; SOME (NONE, [t1; t2; t3])] => SOME (x,t2)
  | _ => NONE

For each such:

• a PMATCH reformulation needs to be proved and stored with a predictable name, e.g. foo_pmatch
• the translator's look up mechanism in the bootstrap should be changed so that it first looks for theorems ending in _pmatch before it looks for the usual _def theorems

[xrchz]

How is this going? Is it in a mergable state (even if not finished)? It would be good to get partial progress merged in, to avoid forking changes to the translator too much.

[IlmariReissumies]

Agreed.

It's in decent shape and close to mergeable. There's some more functions I want to make pmatch versions of (the most horrible one from the parser in particular); I'll put that on ice for now. As soon as I can get through bootstrap translation and catch up with master, I'll make a pull request. I'll try to get it done over the weekend.

[xrchz]

How did you go?

[IlmariReissumies]

I failed to find time for this over the weekend, but now I have.

I am through bootstrap translation, save for the final append_main_call. This is baffling to me since I don't believe I have touched anything that should be relevant at this stage. For now, I have simply merged anyway, praying that some recent change to /characteristic will make it go through... but if master currently times out on bootstrap translation I guess we won't know straight away.

I'll do some final sanity checks, and if nothing surprising turns up, create a pull request later today.

[tanyongkiam]

Ramana reminded me to note here that the translation contains commented out PMATCH translations.

The translation mechanism was probably broken by env-refactor.

[xrchz]

Commits like c29355f6e60c8407fcb6a7a186a76fa1a158b1ae are undoing the work of this issue, leaving more to be done.

[xrchz]

@myreen Can you specify a concrete target for this issue to be closed?