diff --git a/CHANGES.md b/CHANGES.md index 2cfd193e0..85e13fd5c 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -3,6 +3,13 @@ All notable changes to this project will be documented in this file. The format is based on [Keep a Changelog](https://keepachangelog.com/), and this project adheres to [Semantic Versioning](https://semver.org/). +## Unreleased + +### Changed + +- Identifiers may contain `$` or `?` but may not begin with + them. They may contain `|` as well. Identifiers must not contain `/`. + ## 2.1.0 (2022-01-17) ### Added diff --git a/src/parsing/lpLexer.ml b/src/parsing/lpLexer.ml index 426789863..b1fde6054 100644 --- a/src/parsing/lpLexer.ml +++ b/src/parsing/lpLexer.ml @@ -153,8 +153,11 @@ let string = [%sedlex.regexp? '"', Star (Compl '"'), '"'] (** Unqualified regular identifiers are any non-empty sequence of characters not among: *) -let forbidden_letter = [%sedlex.regexp? Chars " ,;\r\t\n(){}[]:.`\"@$|/"] -let regid = [%sedlex.regexp? '/' | '*' | Plus (Compl forbidden_letter)] +let forbidden_letter = [%sedlex.regexp? Chars " ,;\r\t\n(){}[]:.`\"@/"] +let forbidden_first_letter = [%sedlex.regexp? (forbidden_letter | Chars "$?")] +let regid = + [%sedlex.regexp? + Compl forbidden_first_letter, Star (Compl forbidden_letter)] let is_regid : string -> bool = fun s -> let lb = Utf8.from_string s in @@ -280,7 +283,7 @@ let rec token lb = | '_' -> UNDERSCORE (* identifiers *) - | '/' | regid -> UID(Utf8.lexeme lb) + | regid -> UID(Utf8.lexeme lb) | escid -> UID(remove_useless_escape(Utf8.lexeme lb)) | '@', regid -> UID_EXPL(remove_first lb) | '@', escid -> UID_EXPL(remove_useless_escape(remove_first lb)) diff --git a/tests/KO/identifiers.lp b/tests/KO/identifiers.lp new file mode 100644 index 000000000..d59bbc99b --- /dev/null +++ b/tests/KO/identifiers.lp @@ -0,0 +1 @@ +symbol foo/bar: TYPE; diff --git a/tests/KO/identifiers_bar.lp b/tests/KO/identifiers_bar.lp new file mode 100644 index 000000000..b918dad63 --- /dev/null +++ b/tests/KO/identifiers_bar.lp @@ -0,0 +1 @@ +symbol | : TYPE; diff --git a/tests/KO/identifiers_start_dollar.lp b/tests/KO/identifiers_start_dollar.lp new file mode 100644 index 000000000..d42ca1205 --- /dev/null +++ b/tests/KO/identifiers_start_dollar.lp @@ -0,0 +1 @@ +symbol $foo: TYPE; diff --git a/tests/OK/comment_in_qid.lp b/tests/OK/comment_in_qid.lp index 763aee6db..3f7ca4d64 100644 --- a/tests/OK/comment_in_qid.lp +++ b/tests/OK/comment_in_qid.lp @@ -1,5 +1,4 @@ require tests.OK.bool; assert ⊢ tests./*comment*/OK.bool.true : tests.OK.bool.B; symbol A:TYPE; -symbol /:A → A → A; symbol *:A → A → A; diff --git a/tests/OK/identifiers.lp b/tests/OK/identifiers.lp index 394a5b9e7..efc685077 100644 --- a/tests/OK/identifiers.lp +++ b/tests/OK/identifiers.lp @@ -1,3 +1,5 @@ -symbol /:TYPE; symbol *:TYPE; symbol **:TYPE; +symbol foo*: TYPE; +symbol foo$: TYPE; +symbol foo|bar: TYPE;