Deducteam
Allowed characters in identifiers
The following line does not typecheck:
symbol foo/bar: TYPE;
and yield the following error message
[...] The proof is not finished.
It seems to me that the following does what we want
https://gist.github.com/gabrielhdt/e687e60f2eb14c14282e310f556e2230
it allows $, ? but still parses $foo as a pattern, it forbids / and allows *.
The problem is that foo/bar is parsed as 3 separate identifiers foo / bar because / is not allowed in identifiers except as a single-letter identifier. I agree that the message is not nice. A way to get a better message is to ask the lexer to output an error message in case an identifier containing / (but reduced to /) is parsed.
To solve this issue, I would rather suggest to do:
let separ_letter = [%sedlex.regexp? Chars " ,;.:\r\t\n(){}[]\""]
let special_letter = [%sedlex.regexp? Chars "`@/|$?"]
let forbidden_letter = [%sedlex.regexp? separ_letter | special_letter]
let allowed_letter = [%sedlex.regexp? Compl forbidden_letter]
let regid = [%sedlex.regexp? Plus allowed_letter]
let badid = [%sedlex.regexp? Plus allowed_letter, Plus (special_letter, Star allowed_letter)]
[...]
| '/' | regid -> UID(Utf8.lexeme lb)
| badid -> fail lb "Forbidden identifier"
My concern is rather that the syntax of identifiers is not really clear. It seems odd to me to allow / by itself but not in anything else. IMO nobody will remember or use that, even when writing translators.