From 79d32b768d7d36cc3796a79f26c659db93d297e6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 16 Jun 2014 15:50:27 -0700 Subject: [PATCH] feat(shell): add '--hott' command line option Signed-off-by: Leonardo de Moura --- library/hott/logic.lean | 2 ++ library/standard/logic.lean | 2 ++ src/shell/lean.cpp | 17 +++++++++-- src/util/lean_path.cpp | 58 +++++++++++++++++++------------------ src/util/lean_path.h | 6 ++-- 5 files changed, 51 insertions(+), 34 deletions(-) create mode 100644 library/hott/logic.lean create mode 100644 library/standard/logic.lean diff --git a/library/hott/logic.lean b/library/hott/logic.lean new file mode 100644 index 000000000..0dc9e6402 --- /dev/null +++ b/library/hott/logic.lean @@ -0,0 +1,2 @@ +definition id.{l} (A : Type.{l}) (a : A) : A := a +check ∀ x : Type.{0}, x \ No newline at end of file diff --git a/library/standard/logic.lean b/library/standard/logic.lean new file mode 100644 index 000000000..a5b7644bc --- /dev/null +++ b/library/standard/logic.lean @@ -0,0 +1,2 @@ +definition [inline] Bool : Type.{0} := Type.{1} + diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index afc8436f1..59d06c7c9 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -20,6 +20,7 @@ Author: Leonardo de Moura #include "kernel/kernel_exception.h" #include "kernel/formatter.h" #include "kernel/standard/standard.h" +#include "kernel/hott/hott.h" #include "library/module.h" #include "library/io_state_stream.h" #include "library/error_handling/error_handling.h" @@ -36,6 +37,7 @@ using lean::io_state; using lean::io_state_stream; using lean::regular; using lean::mk_environment; +using lean::mk_hott_environment; enum class input_kind { Unspecified, Lean, Lua }; @@ -65,6 +67,7 @@ static void display_help(std::ostream & out) { std::cout << " --trust=num -t trust level (default: 0) \n"; std::cout << " --quiet -q do not print verbose messages\n"; std::cout << " --interactive -i read blocks of commands from the input stream\n"; + std::cout << " --hott use Homotopy Type Theory kernel and libraries\n"; #if defined(LEAN_USE_BOOST) std::cout << " --tstack=num -s thread stack size in Kb\n"; #endif @@ -96,6 +99,7 @@ static struct option g_long_options[] = { {"trust", required_argument, 0, 't'}, {"interactive", no_argument, 0, 'i'}, {"quiet", no_argument, 0, 'q'}, + {"hott", no_argument, 0, 'H'}, #if defined(LEAN_USE_BOOST) {"tstack", required_argument, 0, 's'}, #endif @@ -103,11 +107,13 @@ static struct option g_long_options[] = { }; #if defined(LEAN_USE_BOOST) -static char const * g_opt_str = "iqlupgvhc:012s:012t:012o:"; +static char const * g_opt_str = "Hiqlupgvhc:012s:012t:012o:"; #else -static char const * g_opt_str = "iqlupgvhc:012t:012o:"; +static char const * g_opt_str = "Hiqlupgvhc:012t:012o:"; #endif +enum class lean_mode { Standard, HoTT }; + int main(int argc, char ** argv) { lean::save_stack_info(); lean::register_modules(); @@ -115,6 +121,7 @@ int main(int argc, char ** argv) { unsigned trust_lvl = 0; bool quiet = false; bool interactive = false; + lean_mode mode = lean_mode::Standard; std::string output; input_kind default_k = input_kind::Lean; // default while (true) { @@ -122,6 +129,10 @@ int main(int argc, char ** argv) { if (c == -1) break; // end of command line switch (c) { + case 'H': + mode = lean_mode::HoTT; + lean::init_lean_path("hott"); + break; case 'i': interactive = true; break; @@ -166,7 +177,7 @@ int main(int argc, char ** argv) { } } - environment env = mk_environment(trust_lvl); + environment env = mode == lean_mode::Standard ? mk_environment(trust_lvl) : mk_hott_environment(trust_lvl); io_state ios(lean::mk_simple_formatter()); if (quiet) ios.set_option("verbose", false); diff --git a/src/util/lean_path.cpp b/src/util/lean_path.cpp index ec1d5c477..9783263ad 100644 --- a/src/util/lean_path.cpp +++ b/src/util/lean_path.cpp @@ -128,36 +128,38 @@ std::string get_path(std::string f) { static std::string g_lean_path; static std::vector g_lean_path_vector; -struct init_lean_path { - init_lean_path() { - char * r = getenv("LEAN_PATH"); - if (r == nullptr) { - g_lean_path = "."; - std::string exe_path = get_path(get_exe_location()); - g_lean_path += g_path_sep; - g_lean_path += exe_path + g_sep + ".." + g_sep + "library"; - g_lean_path += g_path_sep; - g_lean_path += exe_path; - } else { - g_lean_path = r; - } - g_lean_path = normalize_path(g_lean_path); - unsigned i = 0; - unsigned j = 0; - unsigned sz = g_lean_path.size(); - for (; j < sz; j++) { - if (g_lean_path[j] == g_path_sep) { - if (j > i) - g_lean_path_vector.push_back(g_lean_path.substr(i, j - i)); - i = j + 1; - } - } - if (j > i) - g_lean_path_vector.push_back(g_lean_path.substr(i, j - i)); +void init_lean_path(char const * kernel_instance_name) { + char * r = getenv("LEAN_PATH"); + if (r == nullptr) { + g_lean_path = "."; + std::string exe_path = get_path(get_exe_location()); + g_lean_path += g_path_sep; + g_lean_path += exe_path + g_sep + ".." + g_sep + "library" + g_sep + kernel_instance_name; + g_lean_path += g_path_sep; + g_lean_path += exe_path; + } else { + g_lean_path = r; } + g_lean_path = normalize_path(g_lean_path); + unsigned i = 0; + unsigned j = 0; + unsigned sz = g_lean_path.size(); + for (; j < sz; j++) { + if (g_lean_path[j] == g_path_sep) { + if (j > i) + g_lean_path_vector.push_back(g_lean_path.substr(i, j - i)); + i = j + 1; + } + } + if (j > i) + g_lean_path_vector.push_back(g_lean_path.substr(i, j - i)); +} + +struct init_lean_path_fn { + init_lean_path_fn() { init_lean_path("standard"); } }; -static init_lean_path g_init_lean_path; -static std::string g_sep_str(1, g_sep); +static init_lean_path_fn g_init_lean_path_fn; +static std::string g_sep_str(1, g_sep); bool has_file_ext(std::string const & fname, char const * ext) { unsigned ext_len = strlen(ext); diff --git a/src/util/lean_path.h b/src/util/lean_path.h index 81caef57e..cf5c5f100 100644 --- a/src/util/lean_path.h +++ b/src/util/lean_path.h @@ -8,9 +8,9 @@ Author: Leonardo de Moura #include #include "util/name.h" namespace lean { -/** - \brief Return the LEAN_PATH string -*/ +/** \brief Initialize the lean_path for the given kernel instance */ +void init_lean_path(char const * kernel_instance_name); +/** \brief Return the LEAN_PATH string */ char const * get_lean_path(); /** \brief Search the file \c fname in the LEAN_PATH. Throw an