CakeML/cakeml

Support custom failure exceptions in the translator

Open

#181 opened on Nov 24, 2016

View on GitHub
 (1 comment) (0 reactions) (0 assignees)Standard ML (98 forks)auto 404
help wantedlow efforttranslator

Repository metrics

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

Description

Currently, if you translate something with a side-condition from ARB, the translator produces the code raise Bind. It would be nice to tweak this a little to allow an arbitrary exception. For example:

val _ = register_exn ``Size``; (* made this up... not sure how it should work *)
val sub_def = Define`sub i ls = if i < LENGTH ls then EL i ls else FAIL Size ARB`;

to produce code that calls raise Size rather than raise Bind. This requires the translator to support defining exceptions too.

For sophisticated use of exceptions, one must use CF, but for exceptions that correspond to side-conditions we expect to always be true, it would be nicer to just use the translator.

Contributor guide

Research direction
Investigate how the translator currently generates exceptions (e.g., `Bind`) and how to allow custom exceptions to be defined and used in the translation process.
Tech stack
None
Domain
compilers
Issue type
Feature
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.
1-2 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.
Mostly clear
Prerequisites
Git
Newbie friendlinessA 1-100 score estimating how approachable this issue is for first-time contributors.
30