It seems that I can define a character by its escape code, such as
mychar : Char
mychar = '\US'
But not for '\SO', because
mychar : Char
mychar = '\SO'
gives
Lexical error in string or character literal: bad escape code
Even though Data.Char.show '\14' gives back "'\\SO'", so I don't see why it shouldn't work.
Is it somehow related to the existence of '\SOH'? What is the best way to print any character in a way that Agda can also read them in?
This looks like a bug in Agda's parser, so I've reported it as such. In particular, the match function doesn't work for non-prefix-free cases, such as SO vs. SOH. To illustrate, here's a short example:
λ» 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
As we can see, if we have "FO" and "FOO" as the two cases, parsing "FOO" works as expected (returning 2), parsing "FOB" works as expected (returning 3 from the default case), but the input "FO" leads to a parse error.