GaloisInc / daedalus

The Daedalus data description language
BSD 3-Clause "New" or "Revised" License
63 stars 11 forks source link

Restrict backtracking scope #329

Closed yav closed 1 year ago

yav commented 1 year ago

Consider a parser like this: { let a = P; Q } <| R, and we know that Q cannot fail. We can rewrite this to:

case Optional P of
   nothing -> R
   just a     -> Q

This is a form of "commit", and it is useful because it reduces the scope of backtracking. This is particularly important for fairly common cases like this:

def P = many (s = builder) { let x = UInt8; emit s x }

In this case, we'd like the builder s to be used linearly because then we can do the updates in place. Unfortunately, this is not the case at the moment, because while executing the body we cannot mutate the state builder in case the body failed, and we have to revert to it. Instead we want something like this:

def P_loop s =
  case Optional Uint8 of
      just  a -> P_loop (emit s a)
     nothing -> s