CakeML/cakeml

Derive PMATCH thms for relevant parts of compiler definition

Open

#136 opened on Aug 7, 2016

View on GitHub
 (8 comments) (0 reactions) (1 assignee)Standard ML (98 forks)auto 404
help wantedlow rewardmedium effort

Repository metrics

Stars
 (1,169 stars)
PR merge metrics
 (PR metrics pending)

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 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

Contributor guide

Research direction
Examine the compiler definitions in the CakeML repository for large case expressions. For each suspicious pattern, derive a PMATCH theorem using HOL, store it with a name ending in ' pmatch', and modify the translator's lookup mechanism to prefer these theorems before the usual ' def' theorems.
Tech stack
None
Domain
compilers
Issue type
Refactor
DifficultyEstimated implementation difficulty for a new contributor, from 1 for very small changes to 5 for expert-level work.
3
Estimated timeA rough time range for an experienced contributor to investigate, implement, test, and prepare a pull request.
3-5 days
Activity statusHow available the issue appears right now: fresh, active, stale, blocked, or waiting on maintainer input.
Active
ClarityHow clearly the issue explains the expected change, acceptance criteria, and next step.
Clear
Prerequisites
Standard MLTheorem proving
Newbie friendlinessA 1-100 score estimating how approachable this issue is for first-time contributors.
30