From 8dfd22e66cd9644fd336da0b5ab1c9465370f5d5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 30 Nov 2014 17:03:08 -0800 Subject: [PATCH] feat(frontends/lean): add 'prelude' command, and init directory --- library/init/default.lean | 7 +++++ src/emacs/lean-syntax.el | 2 +- src/frontends/lean/dependencies.cpp | 44 ++++++++++++++++++----------- src/frontends/lean/parser.cpp | 33 +++++++++++++++------- src/frontends/lean/token_table.cpp | 4 +-- src/frontends/lean/tokens.cpp | 4 +++ src/frontends/lean/tokens.h | 1 + 7 files changed, 66 insertions(+), 29 deletions(-) create mode 100644 library/init/default.lean diff --git a/library/init/default.lean b/library/init/default.lean new file mode 100644 index 0000000000..cdddf8b436 --- /dev/null +++ b/library/init/default.lean @@ -0,0 +1,7 @@ +/- +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Authors: Leonardo de Moura +-/ +prelude diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index 5efed6543f..b52d7457ea 100644 --- a/src/emacs/lean-syntax.el +++ b/src/emacs/lean-syntax.el @@ -8,7 +8,7 @@ (require 'rx) (defconst lean-keywords - '("import" "reducible" "irreducible" "tactic_hint" "protected" "private" "opaque" "definition" "renaming" + '("import" "prelude" "reducible" "irreducible" "tactic_hint" "protected" "private" "opaque" "definition" "renaming" "hiding" "exposing" "parameter" "parameters" "begin" "proof" "qed" "conjecture" "constant" "constants" "hypothesis" "lemma" "corollary" "variable" "variables" "print" "theorem" "example" "context" "open" "as" "export" "axiom" "inductive" "with" "structure" "record" "universe" "universes" diff --git a/src/frontends/lean/dependencies.cpp b/src/frontends/lean/dependencies.cpp index 944fb6ad43..47587ae8fd 100644 --- a/src/frontends/lean/dependencies.cpp +++ b/src/frontends/lean/dependencies.cpp @@ -12,8 +12,11 @@ Author: Leonardo de Moura #include "frontends/lean/scanner.h" namespace lean { + + bool display_deps(environment const & env, std::ostream & out, std::ostream & err, char const * fname) { name import("import"); + name prelude("prelude"); name period("."); std::ifstream in(fname); if (in.bad() || in.fail()) { @@ -26,6 +29,25 @@ bool display_deps(environment const & env, std::ostream & out, std::ostream & er bool import_prefix = false; bool import_args = false; bool ok = true; + bool is_prelude = false; + auto display_dep = [&](optional const & k, name const & f) { + import_args = true; + try { + std::string m_name = find_file(base, k, name_to_file(f), {".lean", ".olean", ".lua"}); + int last_idx = m_name.find_last_of("."); + std::string rawname = m_name.substr(0, last_idx); + std::string ext = m_name.substr(last_idx); + if (ext == ".lean") + m_name = rawname + ".olean"; + display_path(out, m_name); + import_prefix = true; + out << "\n"; + } catch (exception & new_ex) { + err << "error: file '" << name_to_file(s.get_name_val()) << "' not found in the LEAN_PATH" << std::endl; + ok = false; + } + }; + while (true) { scanner::token_kind t = scanner::token_kind::Identifier; try { @@ -34,7 +56,11 @@ bool display_deps(environment const & env, std::ostream & out, std::ostream & er continue; } if (t == scanner::token_kind::Eof) { + if (!is_prelude) + display_dep(optional(), name("init")); return ok; + } else if (t == scanner::token_kind::CommandKeyword && s.get_token_info().value() == prelude) { + is_prelude = true; } else if (t == scanner::token_kind::CommandKeyword && s.get_token_info().value() == import) { k = optional(); import_prefix = true; @@ -44,22 +70,8 @@ bool display_deps(environment const & env, std::ostream & out, std::ostream & er else k = *k + 1; } else if ((import_prefix || import_args) && t == scanner::token_kind::Identifier) { - import_args = true; - try { - std::string m_name = find_file(base, k, name_to_file(s.get_name_val()), {".lean", ".olean", ".lua"}); - int last_idx = m_name.find_last_of("."); - std::string rawname = m_name.substr(0, last_idx); - std::string ext = m_name.substr(last_idx); - if (ext == ".lean") - m_name = rawname + ".olean"; - display_path(out, m_name); - k = optional(); - import_prefix = true; - out << "\n"; - } catch (exception & new_ex) { - err << "error: file '" << name_to_file(s.get_name_val()) << "' not found in the LEAN_PATH" << std::endl; - ok = false; - } + display_dep(k, s.get_name_val()); + k = optional(); } else { import_args = false; import_prefix = false; diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 6181235937..62bbe23603 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -1304,8 +1304,30 @@ static void lua_module_reader(deserializer & d, module_idx, shared_environment & void parser::parse_imports() { buffer olean_files; buffer lua_files; + bool prelude = false; std::string base = dirname(get_stream_name().c_str()); bool imported = false; + if (curr_is_token(get_prelude_tk())) { + next(); + prelude = true; + } + auto import_olean = [&](optional const & k, name const & f) { + if (auto it = try_file(base, k, f, ".olean")) { + olean_files.push_back(module_name(k, f)); + } else { + m_found_errors = true; + if (!m_use_exceptions && m_show_errors) { + flycheck_error err(regular_stream()); + display_error_pos(pos()); + regular_stream() << " invalid import, unknown module '" << f << "'" << endl; + } + if (m_use_exceptions) + throw parser_error(sstream() << "invalid import, unknown module '" << f << "'", pos()); + } + }; + if (!prelude) { + import_olean(optional(), "init"); + } while (curr_is_token(get_import_tk())) { imported = true; m_last_cmd_pos = pos(); @@ -1327,17 +1349,8 @@ void parser::parse_imports() { throw parser_error(sstream() << "invalid import, failed to import '" << f << "', relative paths are not supported for .lua files", pos()); lua_files.push_back(f); - } else if (auto it = try_file(base, k, f, ".olean")) { - olean_files.push_back(module_name(k, f)); } else { - m_found_errors = true; - if (!m_use_exceptions && m_show_errors) { - flycheck_error err(regular_stream()); - display_error_pos(pos()); - regular_stream() << " invalid import, unknown module '" << f << "'" << endl; - } - if (m_use_exceptions) - throw parser_error(sstream() << "invalid import, unknown module '" << f << "'", pos()); + import_olean(k, f); } next(); } diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index 8ea9e9b0b3..27ac868d0b 100644 --- a/src/frontends/lean/token_table.cpp +++ b/src/frontends/lean/token_table.cpp @@ -82,8 +82,8 @@ void init_token_table(token_table & t) { {"theorem", "axiom", "variable", "protected", "private", "opaque", "definition", "example", "coercion", "variables", "parameter", "parameters", "constant", "constants", "[persistent]", "[visible]", "[instance]", "[off]", "[on]", "[none]", "[class]", "[coercion]", "[reducible]", "[parsing-only]", "reducible", "irreducible", - "evaluate", "check", "eval", "[whnf]", "[strict]", "[local]", "[priority", "print", "end", "namespace", "section", "import", - "inductive", "record", "structure", "module", "universe", "universes", + "evaluate", "check", "eval", "[whnf]", "[strict]", "[local]", "[priority", "print", "end", "namespace", "section", "prelude", + "import", "inductive", "record", "structure", "module", "universe", "universes", "precedence", "reserve", "infixl", "infixr", "infix", "postfix", "prefix", "notation", "context", "exit", "set_option", "open", "export", "calc_subst", "calc_refl", "calc_trans", "calc_symm", "tactic_hint", "add_begin_end_tactic", "set_begin_end_tactic", "instance", "class", "find_decl", diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp index b9e2d58a7e..359424552b 100644 --- a/src/frontends/lean/tokens.cpp +++ b/src/frontends/lean/tokens.cpp @@ -27,6 +27,7 @@ static name * g_max = nullptr; static name * g_imax = nullptr; static name * g_cup = nullptr; static name * g_import = nullptr; +static name * g_prelude = nullptr; static name * g_show = nullptr; static name * g_have = nullptr; static name * g_assume = nullptr; @@ -118,6 +119,7 @@ void initialize_tokens() { g_imax = new name("imax"); g_cup = new name("\u2294"); g_import = new name("import"); + g_prelude = new name("prelude"); g_show = new name("show"); g_have = new name("have"); g_assume = new name("assume"); @@ -260,6 +262,7 @@ void finalize_tokens() { delete g_have; delete g_show; delete g_import; + delete g_prelude; delete g_cup; delete g_imax; delete g_max; @@ -301,6 +304,7 @@ name const & get_max_tk() { return *g_max; } name const & get_imax_tk() { return *g_imax; } name const & get_cup_tk() { return *g_cup; } name const & get_import_tk() { return *g_import; } +name const & get_prelude_tk() { return *g_prelude; } name const & get_show_tk() { return *g_show; } name const & get_have_tk() { return *g_have; } name const & get_assume_tk() { return *g_assume; } diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h index b90022880f..2056b0154a 100644 --- a/src/frontends/lean/tokens.h +++ b/src/frontends/lean/tokens.h @@ -29,6 +29,7 @@ name const & get_max_tk(); name const & get_imax_tk(); name const & get_cup_tk(); name const & get_import_tk(); +name const & get_prelude_tk(); name const & get_show_tk(); name const & get_have_tk(); name const & get_assume_tk();