|
|
|---|
|
|
|
|---|
b* binder for checking and propagating error results of parsing functions and ensuring termination.
This is similar to patbind-pok, but it also checks that the parsize of the output token and remaining tokens is strictly below the one of the input token and remaining tokens. The test is put in an mbt, because it is always true, but we need to test for it explicitly in order to ensure termination of certain recursive functions; after the functions have been admitted, guard verification ensures that those tests are indeed true.