diff --git a/src/frontends/lean/scanner.cpp b/src/frontends/lean/scanner.cpp index 15af5cb6a..d13c34f7e 100644 --- a/src/frontends/lean/scanner.cpp +++ b/src/frontends/lean/scanner.cpp @@ -132,8 +132,6 @@ bool scanner::check_next_is_digit() { } void scanner::read_comment() { - lean_assert(curr() == '*'); - next(); int nest = 1; while (true) { if (curr() == '*') { @@ -337,53 +335,43 @@ scanner::token scanner::read_string() { } scanner::token scanner::read_script_block() { - lean_assert(curr() == '{'); - next(); m_script_line = m_line; m_script_pos = m_pos; m_buffer.clear(); - int num_open_blocks = 1; while (true) { - char c = curr(); - if (c == EOF) { + char c1 = curr(); + if (c1 == EOF) throw_exception("unexpected end of script"); - } else if (c == '{') { - m_buffer += '{'; - next(); - c = curr(); - if (c == '{') - num_open_blocks++; - else if (c == '\n') - new_line(); - else if (c == EOF) - throw_exception("unexpected end of script"); - m_buffer += c; - next(); - } else if (c == '}') { - next(); + next(); + if (c1 == '*') { char c2 = curr(); - if (c2 == '}') { - next(); - num_open_blocks--; - if (num_open_blocks == 0) - return token::ScriptBlock; - } else if (c2 == '\n') { - new_line(); - next(); - } else if (c2 == EOF) { + if (c2 == EOF) throw_exception("unexpected end of script"); - } else { + next(); + if (c2 == '*') { + char c3 = curr(); + if (c3 == EOF) + throw_exception("unexpected end of script"); next(); + if (c3 == ')') { + return token::ScriptBlock; + } else { + if (c3 == '\n') + new_line(); + m_buffer += c1; + m_buffer += c2; + m_buffer += c3; + } + } else { + if (c2 == '\n') + new_line(); + m_buffer += c1; + m_buffer += c2; } - m_buffer += c; - m_buffer += c2; - } else if (c == '\n') { - new_line(); - m_buffer += '\n'; - next(); } else { - m_buffer += c; - next(); + if (c1 == '\n') + new_line(); + m_buffer += c1; } } } @@ -407,18 +395,19 @@ scanner::token scanner::scan() { case '(': next(); if (curr() == '*') { - read_comment(); - break; + next(); + if (curr() == '*') { + next(); + return read_script_block(); + } else { + read_comment(); + break; + } } else { return token::LeftParen; } case ')': next(); return token::RightParen; - case '{': - next(); - if (curr() == '{') - return read_script_block(); - else - return token::LeftCurlyBracket; + case '{': next(); return token::LeftCurlyBracket; case '}': next(); return token::RightCurlyBracket; case 'a': return read_a_symbol(); case 'b': return read_b_symbol(); diff --git a/tests/lean/lua1.lean b/tests/lean/lua1.lean index 95b30ba9a..6dbac0ce6 100644 --- a/tests/lean/lua1.lean +++ b/tests/lean/lua1.lean @@ -1,7 +1,7 @@ Variable x : Int -{{ +(** print("hello world from Lua") -}} +**) Variable y : Int diff --git a/tests/lean/lua2.lean b/tests/lean/lua2.lean index e26ea9f33..faae048f8 100644 --- a/tests/lean/lua2.lean +++ b/tests/lean/lua2.lean @@ -1,6 +1,6 @@ Variable x : Bool -{{ +(** a = {} print("hello world") print ("ok") @@ -9,7 +9,7 @@ Variable x : Bool y = 20 } rint ("ok") -}} +**) Variable y : Bool diff --git a/tests/lean/lua3.lean b/tests/lean/lua3.lean index 606da73fa..2811ab391 100644 --- a/tests/lean/lua3.lean +++ b/tests/lean/lua3.lean @@ -1,6 +1,6 @@ Variable x : Int -{{ +(** dofile("script.lua") -}} \ No newline at end of file +**) \ No newline at end of file diff --git a/tests/lean/lua4.lean b/tests/lean/lua4.lean index c191eb006..d5a0ba7be 100644 --- a/tests/lean/lua4.lean +++ b/tests/lean/lua4.lean @@ -1,12 +1,12 @@ Variable x : Int -{{ +(** -- Add a variable to the environment using Lua -- The type of the new variable is equal to the type -- of x typeofx = env():check_type(Const("x")) print("type of x is " .. tostring(typeofx)) env():add_var("y", typeofx) -}} +**) Check x + y diff --git a/tests/lean/lua5.lean b/tests/lean/lua5.lean index 35ecc24ae..ae0e18ec8 100644 --- a/tests/lean/lua5.lean +++ b/tests/lean/lua5.lean @@ -1,13 +1,13 @@ Variable x : Int -{{ +(** local N = 100 -- Create N variables with the same type of x typeofx = env():check_type(Const("x")) for i = 1, N do env():add_var("y_" .. i, typeofx) end -}} +**) Show Environment 101 Check x + y_1 + y_2 \ No newline at end of file diff --git a/tests/lean/lua6.lean b/tests/lean/lua6.lean index 4e7b984fc..b061065c1 100644 --- a/tests/lean/lua6.lean +++ b/tests/lean/lua6.lean @@ -1,19 +1,19 @@ Variable x : Int Set pp::notation false -{{ +(** print(get_options()) -}} +**) Check x + 2 -{{ +(** o = get_options() o = o:update(name('lean', 'pp', 'notation'), true) set_options(o) print(get_options()) -}} +**) Check x + 2 -{{ +(** set_option(name('lean', 'pp', 'notation'), false) print(get_options()) -}} +**) Variable y : Int Check x + y