diff options
Diffstat (limited to 'sec/compiler.ltx')
| -rw-r--r-- | sec/compiler.ltx | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/sec/compiler.ltx b/sec/compiler.ltx index 8f18adc..27705b6 100644 --- a/sec/compiler.ltx +++ b/sec/compiler.ltx @@ -67,12 +67,13 @@ as an identifier, the parser can look up the name in the environment and convert it into a deBruijn index. The state is not stored globally, but is local to the current parser -combinator. We can imagine this as a stack of states. Before parsing -the first item in a sequence, we push a copy of the current state on -top of the stack. After parsing that item, we pop the local state off -the stack. We can then modify the original state using the first -item's value. We then copy this modified state onto the stack before -parsing the second item, and so on. +combinator. Imagine this as a stack of states. Before parsing the +first combinator in a sequence, we push a copy of the current state on +top of the stack. After parsing that combinator, we pop the local +state off the stack. We then update the original state using the first +combinator's result and copy this modified state onto the stack. We +then parse the second combinator and pop, update and copy the state +before the third combinator and so on. The parser returns an intrinsically well-scoped term~\cite{iwss}. Terms are a dependent data type with signature |