From 44a31dd8fbca397f4392c7e896d8e632c05de4b0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 28 Dec 2013 12:04:56 -0800 Subject: [PATCH] feat(frontends/lean/parser): improve Import command - The extension does not have to be provided. - It can also import Lua files. - Hierachical names can be used instead of strings. Signed-off-by: Leonardo de Moura --- src/frontends/lean/parser.cpp | 27 ++++++++++++++--- src/util/lean_path.cpp | 57 +++++++++++++++++++++++++++++++---- src/util/lean_path.h | 13 +++++++- src/util/name.cpp | 14 ++++----- src/util/name.h | 2 +- src/util/script_state.cpp | 21 ++++++++++--- src/util/script_state.h | 7 ++++- tests/lean/cast4.lean | 2 +- tests/lean/discharge.lean | 2 +- tests/lean/disj1.lean | 2 +- tests/lean/mod1.lean | 4 +-- tests/lean/norm_tac.lean | 2 +- 12 files changed, 122 insertions(+), 31 deletions(-) diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 2c4cf5a35..29802868b 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -2373,10 +2373,7 @@ class parser::imp { regular(m_io_state) << " Set: " << id << endl; } - void parse_import() { - next(); - std::string fname = check_string_next("invalid import command, string (i.e., file name) expected"); - fname = find_file(fname.c_str()); + void import_lean_file(std::string const & fname) { std::ifstream in(fname); if (!in.is_open()) throw parser_error(sstream() << "invalid import command, failed to open file '" << fname << "'", m_last_cmd_pos); @@ -2395,6 +2392,28 @@ class parser::imp { } } + void parse_import() { + next(); + std::string fname; + if (curr_is_identifier()) { + fname = name_to_file(curr_name()); + next(); + } else { + fname = check_string_next("invalid import command, string (i.e., file name) or identifier expected"); + } + fname = find_file(fname); + if (is_lean_file(fname)) { + import_lean_file(fname); + } else if (is_lua_file(fname)) { + if (!m_script_state) + throw parser_error(sstream() << "failed to import Lua file '" << fname << "', parser does not have an intepreter", m_last_cmd_pos); + m_script_state->import_explicit(fname.c_str()); + } else { + // assume is a Lean file + import_lean_file(fname); + } + } + void parse_help() { next(); if (curr() == scanner::token::CommandId) { diff --git a/src/util/lean_path.cpp b/src/util/lean_path.cpp index 7010f674f..15346eccc 100644 --- a/src/util/lean_path.cpp +++ b/src/util/lean_path.cpp @@ -10,6 +10,8 @@ Author: Leonardo de Moura #include #include "util/exception.h" #include "util/sstream.h" +#include "util/name.h" +#include "util/optional.h" namespace lean { #if defined(LEAN_WINDOWS) @@ -115,14 +117,57 @@ struct init_lean_path { } }; static init_lean_path g_init_lean_path; +static std::string g_sep_str(1, g_sep); -std::string find_file(char const * fname) { - std::string nfname = normalize_path(std::string(fname)); +bool has_file_ext(std::string const & fname, char const * ext) { + unsigned ext_len = strlen(ext); + return fname.size() > ext_len && fname.substr(fname.size() - ext_len, ext_len) == ext; +} + +bool is_lean_file(std::string const & fname) { + return has_file_ext(fname, ".lean"); +} + +bool is_olean_file(std::string const & fname) { + return has_file_ext(fname, ".olean"); +} + +bool is_lua_file(std::string const & fname) { + return has_file_ext(fname, ".lua"); +} + +bool is_known_file_ext(std::string const & fname) { + return is_lean_file(fname) || is_olean_file(fname) || is_lua_file(fname); +} + +optional check_file(std::string const & path, std::string const & fname, char const * ext = nullptr) { + std::string file = path + g_sep + fname; + if (ext) + file += ext; + std::ifstream ifile(file); + if (ifile) + return optional(file); + else + return optional(); +} + +std::string name_to_file(name const & fname) { + return fname.to_string(g_sep_str.c_str()); +} + +std::string find_file(std::string fname) { + bool is_known = is_known_file_ext(fname); + fname = normalize_path(fname); for (auto path : g_lean_path_vector) { - std::string file = path + g_sep + nfname; - std::ifstream ifile(file); - if (ifile) - return file; + if (is_known) { + if (auto r = check_file(path, fname)) + return *r; + } else { + for (auto ext : { ".olean", ".lean", ".lua" }) { + if (auto r = check_file(path, fname, ext)) + return *r; + } + } } throw exception(sstream() << "file '" << fname << "' not found in the LEAN_PATH"); } diff --git a/src/util/lean_path.h b/src/util/lean_path.h index aec574593..786cf301e 100644 --- a/src/util/lean_path.h +++ b/src/util/lean_path.h @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #pragma once #include +#include "util/name.h" namespace lean { /** \brief Return the LEAN_PATH string @@ -15,5 +16,15 @@ char const * get_lean_path(); \brief Search the file \c fname in the LEAN_PATH. Throw an exception if the file was not found. */ -std::string find_file(char const * fname); +std::string find_file(std::string fname); + +/** \brief Return true iff fname ends with ".lean" */ +bool is_lean_file(std::string const & fname); +/** \brief Return true iff fname ends with ".olean" */ +bool is_olean_file(std::string const & fname); +/** \brief Return true iff fname ends with ".lua" */ +bool is_lua_file(std::string const & fname); + +/** \brief Return a string that replaces hierachical name separator '::' with a path separator. */ +std::string name_to_file(name const & fname); } diff --git a/src/util/name.cpp b/src/util/name.cpp index b782a8fef..0991ce6c2 100644 --- a/src/util/name.cpp +++ b/src/util/name.cpp @@ -53,11 +53,11 @@ struct name::imp { imp(bool s, imp * p):m_rc(1), m_is_string(s), m_hash(0), m_prefix(p) { if (p) p->inc_ref(); } - static void display_core(std::ostream & out, imp * p) { + static void display_core(std::ostream & out, imp * p, char const * sep) { lean_assert(p != nullptr); if (p->m_prefix) { - display_core(out, p->m_prefix); - out << lean_name_separator; + display_core(out, p->m_prefix, sep); + out << sep; } if (p->m_is_string) out << p->m_str; @@ -65,11 +65,11 @@ struct name::imp { out << p->m_k; } - static void display(std::ostream & out, imp * p) { + static void display(std::ostream & out, imp * p, char const * sep = lean_name_separator) { if (p == nullptr) out << anonymous_str; else - display_core(out, p); + display_core(out, p, sep); } friend void copy_limbs(imp * p, buffer & limbs) { @@ -330,9 +330,9 @@ bool name::is_safe_ascii() const { return true; } -std::string name::to_string() const { +std::string name::to_string(char const * sep) const { std::ostringstream s; - imp::display(s, m_ptr); + imp::display(s, m_ptr, sep); return s.str(); } diff --git a/src/util/name.h b/src/util/name.h index 0f39e4cf6..577ee2610 100644 --- a/src/util/name.h +++ b/src/util/name.h @@ -90,7 +90,7 @@ public: */ name get_prefix() const; /** \brief Convert this hierarchical name into a string. */ - std::string to_string() const; + std::string to_string(char const * sep = lean_name_separator) const; /** \brief Size of the this name (in characters). */ size_t size() const; unsigned hash() const; diff --git a/src/util/script_state.cpp b/src/util/script_state.cpp index 56b9e5db6..3d9c86fc8 100644 --- a/src/util/script_state.cpp +++ b/src/util/script_state.cpp @@ -119,13 +119,20 @@ struct script_state::imp { ::lean::dostring(m_state, str); } - void import(char const * fname) { - std::string fname_str(find_file(fname)); - if (m_imported_modules.find(fname_str) == m_imported_modules.end()) { - dofile(fname_str.c_str()); - m_imported_modules.insert(fname_str); + void import_explicit(std::string const & fname) { + if (m_imported_modules.find(fname) == m_imported_modules.end()) { + dofile(fname.c_str()); + m_imported_modules.insert(fname); } } + + void import_explicit(char const * fname) { + import_explicit(std::string(fname)); + } + + void import(char const * fname) { + return import_explicit(find_file(fname)); + } }; script_state to_script_state(lua_State * L) { @@ -158,6 +165,10 @@ void script_state::import(char const * str) { m_ptr->import(str); } +void script_state::import_explicit(char const * str) { + m_ptr->import_explicit(str); +} + mutex & script_state::get_mutex() { return m_ptr->m_mutex; } diff --git a/src/util/script_state.h b/src/util/script_state.h index efd6edb68..9e31fbb4e 100644 --- a/src/util/script_state.h +++ b/src/util/script_state.h @@ -46,9 +46,14 @@ public: void dostring(char const * str); /** \brief Import file \c fname from the LEAN_PATH. - If the file was already included, then it nothing happens. + If the file was already included, then nothing happens. */ void import(char const * fname); + /** + \brief Import file \c fname. \c fname is the explicit path to the file. + If the file was already included, then nothing happens. + */ + void import_explicit(char const * fname); /** \brief Execute \c f in the using the internal Lua State. diff --git a/tests/lean/cast4.lean b/tests/lean/cast4.lean index 0db23b860..9e4761899 100644 --- a/tests/lean/cast4.lean +++ b/tests/lean/cast4.lean @@ -1,4 +1,4 @@ -Import "cast.lean" +Import cast SetOption pp::colors false Definition TypeM := (Type M) diff --git a/tests/lean/discharge.lean b/tests/lean/discharge.lean index 1d4beb116..e877dd9ab 100644 --- a/tests/lean/discharge.lean +++ b/tests/lean/discharge.lean @@ -1,4 +1,4 @@ -(** import("tactic.lua") **) +Import tactic Check @Discharge Theorem T (a b : Bool) : a => b => b => a. apply Discharge. diff --git a/tests/lean/disj1.lean b/tests/lean/disj1.lean index d9edf53cd..1f1592e80 100644 --- a/tests/lean/disj1.lean +++ b/tests/lean/disj1.lean @@ -1,4 +1,4 @@ -(** import("tactic.lua") **) +Import tactic Theorem T1 (a b : Bool) : a \/ b => b \/ a. apply Discharge. diff --git a/tests/lean/mod1.lean b/tests/lean/mod1.lean index b91430f7e..d949bfad1 100644 --- a/tests/lean/mod1.lean +++ b/tests/lean/mod1.lean @@ -1,5 +1,5 @@ -Import "simple.lean" -Import "simple.lean" +Import simple +Import simple (** local env = environment() -- create new environment parse_lean_cmds([[ diff --git a/tests/lean/norm_tac.lean b/tests/lean/norm_tac.lean index 5c1172bb5..c29d7e392 100644 --- a/tests/lean/norm_tac.lean +++ b/tests/lean/norm_tac.lean @@ -1,4 +1,4 @@ -(** import("tactic.lua") **) +Import tactic SetOption pp::implicit true SetOption pp::coercion true SetOption pp::notation false