Skip to content

Commit

Permalink
Add support for notations with symbols starting with a number.
Browse files Browse the repository at this point in the history
E.g.
Notation "0+" := None.

Printing was working but not parsing.
  • Loading branch information
herbelin committed Aug 3, 2021
1 parent a41c99a commit 69d0f05
Show file tree
Hide file tree
Showing 3 changed files with 15 additions and 2 deletions.
6 changes: 4 additions & 2 deletions parsing/cLexer.ml
Original file line number Diff line number Diff line change
Expand Up @@ -737,9 +737,11 @@ let rec next_token ~diff_mode loc s =
IDENT id, set_loc_pos loc bp ep end
| Some ('0'..'9') ->
let n = NumTok.Unsigned.parse s in
let ep = Stream.count s in
comment_stop bp;
(NUMBER n, set_loc_pos loc bp ep)
begin try find_keyword loc (NumTok.Unsigned.sprint n) bp s
with Not_found ->
let ep = Stream.count s in
NUMBER n, set_loc_pos loc bp ep end
| Some '\"' ->
Stream.junk s;
let (loc, len) =
Expand Down
4 changes: 4 additions & 0 deletions test-suite/output/Notations4.out
Original file line number Diff line number Diff line change
Expand Up @@ -215,3 +215,7 @@ Some MyNone+
: option (option ?A)
where
?A : [ |- Type]
0+
: option ?A
where
?A : [ |- Type]
7 changes: 7 additions & 0 deletions test-suite/output/Notations4.v
Original file line number Diff line number Diff line change
Expand Up @@ -483,3 +483,10 @@ Check MyNone+.
Check Some MyNone+.

End LeadingIdent.

Module SymbolsStartingWithNumbers.

Notation "0+" := None.
Check 0+.

End SymbolsStartingWithNumbers.

0 comments on commit 69d0f05

Please sign in to comment.