michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(frontends/lean/scanner): disallow superscripts in identifiers

Browse source 
See new test for motivating example.
This commit is contained in:
Leonardo de Moura 2016-01-26 18:24:12 -08:00
parent 6f6672eaaa
commit 4821af8685
3 changed files with 11 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/frontends/lean/scanner.cpp
View file

@ -59,14 +59,10 @@ bool is_letter_like_unicode(unsigned u) {
(0x1f00 <= u && u <= 0x1ffe) || // Polytonic Greek Extended Character Set (0x1f00 <= u && u <= 0x1ffe) || // Polytonic Greek Extended Character Set
(0x2100 <= u && u <= 0x214f); // Letter like block (0x2100 <= u && u <= 0x214f); // Letter like block
} }
bool is_super_sub_script_alnum_unicode(unsigned u) { bool is_sub_script_alnum_unicode(unsigned u) {
return return
(0x2070 <= u && u <= 0x2079) || // most (numeric) superscripts
(0x207f <= u && u <= 0x2089) || // n superscript and numberic subscripts (0x207f <= u && u <= 0x2089) || // n superscript and numberic subscripts
(0x2090 <= u && u <= 0x209c) || // letter-like subscripts (0x2090 <= u && u <= 0x209c); // letter-like subscripts
u == 0x00B2 || // 2 superscript
u == 0x00B3 || // 3 superscript
u == 0x00B9; // 1 superscript
} }
void scanner::next() { void scanner::next() {
@ -333,7 +329,7 @@ bool is_id_rest(char const * begin, char const * end) {
if (std::isalnum(*begin) || *begin == '_' || *begin == '\'') if (std::isalnum(*begin) || *begin == '_' || *begin == '\'')
return true; return true;
unsigned u = utf8_to_unicode(begin, end); unsigned u = utf8_to_unicode(begin, end);
return is_letter_like_unicode(u) || is_super_sub_script_alnum_unicode(u); return is_letter_like_unicode(u) || is_sub_script_alnum_unicode(u);
} }
static char const * g_error_key_msg = "unexpected token"; static char const * g_error_key_msg = "unexpected token";

8
tests/lean/626a.lean
View file

@ -1,9 +1,9 @@
namespace foo namespace foo
definition C¹ := nat definition C₁ := nat
definition foo (c : C¹) := nat.rec_on c _ _ definition foo (c : C₁) := nat.rec_on c _ _
end foo end foo
namespace boo namespace boo
notation `C¹` := nat notation `C₁` := nat
definition foo (c : C¹) := nat.rec_on c _ _ definition foo (c : C₁) := nat.rec_on c _ _
end boo end boo

4
tests/lean/run/super.lean Normal file
View file

@ -0,0 +1,4 @@
constant f : nat → nat
notation a `²` := f a
variable a : nat
check a²