From 2cd2527d9f01d15b97fb1665fd52882b1eaa6f1e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 7 Jan 2014 16:56:22 -0800 Subject: [PATCH] refactor(shell): move read-eval-loop script to repl.lua Signed-off-by: Leonardo de Moura --- src/builtin/repl.lua | 36 ++++++++++++++++++++ src/shell/lean.cpp | 3 +- src/shell/lua_repl.h | 79 -------------------------------------------- 3 files changed, 37 insertions(+), 81 deletions(-) create mode 100644 src/builtin/repl.lua delete mode 100644 src/shell/lua_repl.h diff --git a/src/builtin/repl.lua b/src/builtin/repl.lua new file mode 100644 index 0000000000..cfaaeb1885 --- /dev/null +++ b/src/builtin/repl.lua @@ -0,0 +1,36 @@ +-- Simple read-eval-print loop for Lean Lua frontend +local function trim(s) + return s:gsub('^%s+', ''):gsub('%s+$', '') +end + +local function show_results(...) + if select('#', ...) > 1 then + print(select(2, ...)) + end +end + +print([[Type 'exit' to exit.]]) +repeat + io.write'lean > ' + local s = io.read() + if s == nil then print(); break end + if trim(s) == 'exit' then break end + local f, err = loadstring(s, 'stdin') + if err then + f = loadstring('return (' .. s .. ')', 'stdin') + end + if f then + local ok, err = pcall(f) + if not ok then + if is_exception(err) then + print(err:what()) + else + print(err) + end + else + if err then print(err) end + end + else + print(err) + end +until false diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index f8cbd005a2..4514cab124 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -27,7 +27,6 @@ Author: Leonardo de Moura #include "frontends/lean/shell.h" #include "frontends/lean/frontend.h" #include "frontends/lua/register_modules.h" -#include "shell/lua_repl.h" #include "version.h" #include "githash.h" // NOLINT @@ -183,7 +182,7 @@ int main(int argc, char ** argv) { } else { lean_assert(default_k == input_kind::Lua); script_state S; - S.dostring(g_lua_repl); + S.import("repl"); } } else { environment env; diff --git a/src/shell/lua_repl.h b/src/shell/lua_repl.h deleted file mode 100644 index 8ddda8434d..0000000000 --- a/src/shell/lua_repl.h +++ /dev/null @@ -1,79 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -// Very simple read-eval-print for Lua - -#if LUA_VERSION_NUM >= 520 -static char const * g_lua_repl = - "local function trim(s)\n" - " return s:gsub('^%s+', ''):gsub('%s+$', '')\n" - "end\n" - "local function show_results(...)\n" - " if select('#', ...) > 1 then\n" - " print(select(2, ...))\n" - " end\n" - "end\n" - "print([[Type 'Exit' to exit.]])\n" - "repeat\n" - " io.write'lean > '\n" - " local s = io.read()\n" - " if s == nil then print(""); break end\n" - " if trim(s) == 'Exit' then break end\n" - " local f, err = load(s, 'stdin')\n" - " if err then\n" - " f = load('return (' .. s .. ')', 'stdin')\n" - " end\n" - " if f then\n" - " local ok, err = pcall(f)\n" - " if not ok then\n" - " if is_exception(err) then\n" - " print(err:what())\n" - " else\n" - " print(err)\n" - " end\n" - " else\n" - " if err then print(err) end\n" - " end\n" - " else\n" - " print(err)\n" - " end\n" - "until false\n"; -#else /* For Lua 5.1, we uses loadstring instead of load */ -static char const * g_lua_repl = - "local function trim(s)\n" - " return s:gsub('^%s+', ''):gsub('%s+$', '')\n" - "end\n" - "local function show_results(...)\n" - " if select('#', ...) > 1 then\n" - " print(select(2, ...))\n" - " end\n" - "end\n" - "print([[Type 'Exit' to exit.]])\n" - "repeat\n" - " io.write'lean > '\n" - " local s = io.read()\n" - " if s == nil then print(""); break end\n" - " if trim(s) == 'Exit' then break end\n" - " local f, err = loadstring(s, 'stdin')\n" - " if err then\n" - " f = loadstring('return (' .. s .. ')', 'stdin')\n" - " end\n" - " if f then\n" - " local ok, err = pcall(f)\n" - " if not ok then\n" - " if is_exception(err) then\n" - " print(err:what())\n" - " else\n" - " print(err)\n" - " end\n" - " else\n" - " if err then print(err) end\n" - " end\n" - " else\n" - " print(err)\n" - " end\n" - "until false\n"; -#endif