Allowed characters in identifiers

[gabrielhdt]

The following line does not typecheck:

symbol foo/bar: TYPE;

and yield the following error message

[...] The proof is not finished.

[gabrielhdt]

Perhaps, because of the comments, we must not allow / in identifiers.

[gabrielhdt]

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 *.

[gabrielhdt]

The pull request #818 solves the issue

[fblanqui]

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.

[fblanqui]

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"

[gabrielhdt]

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.