我对Coq解析器的实现方式感到非常惊讶.例如
https://www.cis.upenn.edu/~bcpierce/sf/current/Imp.html#lab321
通过给出notation命令并且后续解析器能够解析任何表达式,解析器似乎可以接受任何lexeme.所以这意味着语法必须是上下文敏感的.但这非常灵活,绝对超出了我的理解范围.
关于这种解析器在理论上如何可行的任何指针？它应该如何工作？任何材料或知识都可行.我只是试着了解一下这种类型的解析器.谢谢.
请不要让我自己阅读Coq的来源.我想检查一般的想法,但不是具体的实现.
在 Kenneth Iverson 的A Programming Language 中，归约操作op/定义为foldl（左折叠）：
The ?-reduction of a vector is denoted by ?/ and defined as
z??/ ? z = (?((? ? ?) ? ?) ? ? ?)
然而在现代 APL 中，它显然是一个正确的折叠 ( foldr )
{??}/'abcd'
????????????
?a ?????????
? ?b ??????
? ? ?cd???
? ? ??????
? ?????????
????????????
我想知道这种变化是什么时候发生的（动机是什么）？
也许（？）?/v仅定义为v? ? v? ? ? ? v?，其中（给定 APL 规则）将解析为foldr确实有意义。另一方面，实现高效的foldl更容易。