CakeML/cakeml
Voir sur GitHubDerive PMATCH thms for relevant parts of compiler definition
Open
#136 ouverte le 7 août 2016
help wantedlow rewardmedium effort
Métriques du dépôt
- Stars
- (1 169 stars)
- Métriques de merge PR
- (Métriques PR en attente)
Description
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
PMATCHreformulation 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
_pmatchbefore it looks for the usual_deftheorems