CakeML / CakeML/cakeml

Pancake __add_with_carry___ has unfortunate parser interactions

Open
#1,462 0 comments 1 reaction 0 assignees View on GitHub
low effort Pancake refactoring
Dominant language
Standard ML
Stars
1.2k
Forks
104
Avg merge
2d 21h
Merged PRs (30d)
16

Description

The `AddCarry` primitive was introduced to Pancake in #1398, and given concrete syntax that looked like this:

x = \_\_add_with_carry\_\_(y,z,w);

Because it looks so much like a function call, its parsing implementation piggybacks on the parsing of functions like this: during PEG parsing, nothing special is done so it becomes an ordinary `CallNT` node. Then during ptree conversion, the conversion of `CallNT` nodes has a ~~hack~~ special case for function calls of the precise form above, where they get replaced with the `AddCarry` primitive.

But function calls are allowed in many positions where `\_\_add_with_carry\_\_` is not: as stand-alone calls `f(args)`, as tail calls `return f(args)`, as calls with exception handlers, and so on. Ptree conversion needs to decide what do do when confronted with this. Prior to #1450, the behaviour in such cases was inconsistent: it would either fail during ptree conversion, or succeed and produce a `Call` to a function named `\_\_add_with_carry\_\_`. Both behaviours are bad: ptree conversion should never fail on the PEG parser's output, and it is confusing that nothing stops people from writing functions like this:

fun 1 \_\_add_with_carry\_\_(1 y, 1 w, 1 x) { ... }

...that is only callable on tuesdays.

In #1450 I made sure all out-of-place `__add_with_carry__` calls always fail ptree conversion, which is still bad, but at least consistent.

My proposed fix is to treat `__add_with_carry__` as a keyword during lexing, and handle it with its own kind of `NT` node in the PEG. Misusing the name would then produce (more) useful error messages.

Contributor guide

No contributing guide indexed for this repository

Research direction

Trace how the lexer, PEG parser, and ptree conversion handle the AddCarry primitive and out-of-place __add_with_carry__ calls. Start with the existing CallNT special case and the behavior described after #1450. Done means the name is handled as a keyword with its own PEG node, while misuse produces useful errors and ptree conversion does not fail unexpectedly.

Written by the indexing model from the issue text.

Assessment

Domain
compilers
Issue type
Bug
Difficulty
4/5
Estimated time
3-5 days
Activity status
Active
Clarity
Mostly clear
Newbie friendliness
48/100

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.