summaryrefslogtreecommitdiff
path: root/sec
diff options
context:
space:
mode:
authorChloe Brown <chloe.brown.00@outlook.com>2025-06-26 18:23:23 +0100
committerChloe Brown <chloe.brown.00@outlook.com>2025-06-26 18:23:23 +0100
commit0bbbc5620203fea175c01a0ad86742d345bc6aee (patch)
treef44360c4913e25e2c236842e3e58b377e5047ca4 /sec
parent1500d2775307f855d17c483caabcdf1c2924b562 (diff)
Fix 960--966.
Diffstat (limited to 'sec')
-rw-r--r--sec/compiler.ltx13
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