为什么 '\SO' 的行为与 Agda 中的其他转义码不同？答案

【问题标题】：Why is '\SO' behaving differently from the other escape codes in Agda?为什么 '\SO' 的行为与 Agda 中的其他转义码不同？
【发布时间】：2021-06-23 06:13:18
【问题描述】：

看来我可以通过转义码来定义一个字符，比如

mychar : Char
mychar = '\US'

但不是'\SO'，因为

mychar : Char
mychar = '\SO'

给予

字符串或字符文字中的词法错误：错误的转义码

即使Data.Char.show '\14' 回馈"'\\SO'"，所以我不明白为什么它不应该工作。

它与'\SOH'的存在有某种关系吗？以 Agda 也可以读取的方式打印任何字符的最佳方法是什么？

【问题讨论】：

标签： escaping ascii special-characters agda

【解决方案1】：

这看起来像是 Agda 解析器 so I've reported it as such 中的一个错误。特别是，the match function 不适用于非无前缀情况，例如 SO 与 SOH。为了说明，这里有一个简短的例子：

λ» M.parse defaultParseFlags [] (runLookAhead error $ match [("FO", pure 1), ("FOO", pure 2)] (pure 3)) "FOO"
ParseOk (PState {parseSrcFile = Nothing, parsePos = Pn {srcFile = (), posPos = 1, posLine = 1, posCol = 1}, parseLastPos = Pn {srcFile = (), posPos = 1, posLine = 1, posCol = 1}, parseInp = "FOO", parsePrevChar = '\n', parsePrevToken = "", parseLayout = [NoLayout], parseLexState = [], parseFlags = ParseFlags {parseKeepComments = False}}) 2
λ» M.parse defaultParseFlags [] (runLookAhead error $ match [("FO", pure 1), ("FOO", pure 2)] (pure 3)) "FOB"
ParseOk (PState {parseSrcFile = Nothing, parsePos = Pn {srcFile = (), posPos = 1, posLine = 1, posCol = 1}, parseLastPos = Pn {srcFile = (), posPos = 1, posLine = 1, posCol = 1}, parseInp = "FOB", parsePrevChar = '\n', parsePrevToken = "", parseLayout = [NoLayout], parseLexState = [], parseFlags = ParseFlags {parseKeepComments = False}}) 3
λ» M.parse defaultParseFlags [] (runLookAhead error $ match [("FO", pure 1), ("FOO", pure 2)] (pure 3)) "FO"
*** Exception: unexpected end of file
CallStack (from HasCallStack):
  error, called at <interactive>:31:44 in interactive:Ghci8

如我们所见，如果我们将"FO" 和"FOO" 作为两种情况，解析"FOO" 可以正常工作（返回2），解析"FOB" 可以正常工作（从默认情况返回3），但输入"FO" 会导致解析错误。

【讨论】：

感谢您的出色分析，这将在 2.6.2.1 中修复。