From eb87c1869330fa51b08c8ccb43adaf0d87d8a898 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 5 Dec 2014 14:34:02 -0800 Subject: [PATCH] feat(*): add support for separate HoTT library --- hott/.project | 4 +++ hott/init/datatypes.hlean | 23 ++++++++++++++ hott/init/default.hlean | 8 +++++ src/frontends/lean/dependencies.cpp | 4 +-- src/frontends/lean/inductive_cmd.cpp | 18 +++++++---- src/frontends/lean/structure_cmd.cpp | 10 +++--- src/library/CMakeLists.txt | 2 +- src/library/hott_kernel.cpp | 22 +++++++++++++ src/library/hott_kernel.h | 13 ++++++++ src/shell/lean.cpp | 47 +++++++++++++++++++++++++--- src/util/lean_path.cpp | 23 ++++++++++---- src/util/lean_path.h | 2 +- 12 files changed, 152 insertions(+), 24 deletions(-) create mode 100644 hott/.project create mode 100644 hott/init/datatypes.hlean create mode 100644 hott/init/default.hlean create mode 100644 src/library/hott_kernel.cpp create mode 100644 src/library/hott_kernel.h diff --git a/hott/.project b/hott/.project new file mode 100644 index 000000000..01cefdf13 --- /dev/null +++ b/hott/.project @@ -0,0 +1,4 @@ ++ *.hlean +- flycheck*.lean +- flycheck*.hlean +- .#*.hlean \ No newline at end of file diff --git a/hott/init/datatypes.hlean b/hott/init/datatypes.hlean new file mode 100644 index 000000000..ccab2ba01 --- /dev/null +++ b/hott/init/datatypes.hlean @@ -0,0 +1,23 @@ +/- +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Authors: Leonardo de Moura + +Basic datatypes +-/ +prelude +notation [parsing-only] `Type'` := Type.{_+1} +notation [parsing-only] `Type₊` := Type.{_+1} +notation `Type₀` := Type.{0} +notation `Type₁` := Type.{1} +notation `Type₂` := Type.{2} +notation `Type₃` := Type.{3} + +inductive unit : Type := +star : unit + +inductive empty : Type + +structure prod (A B : Type) := +mk :: (pr1 : A) (pr2 : B) diff --git a/hott/init/default.hlean b/hott/init/default.hlean new file mode 100644 index 000000000..981b2aaf0 --- /dev/null +++ b/hott/init/default.hlean @@ -0,0 +1,8 @@ +/- +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 +import init.datatypes diff --git a/src/frontends/lean/dependencies.cpp b/src/frontends/lean/dependencies.cpp index 47587ae8f..340e1631f 100644 --- a/src/frontends/lean/dependencies.cpp +++ b/src/frontends/lean/dependencies.cpp @@ -33,11 +33,11 @@ bool display_deps(environment const & env, std::ostream & out, std::ostream & er 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"}); + std::string m_name = find_file(base, k, name_to_file(f), {".lean", ".hlean", ".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") + if (ext == ".lean" || ext == ".hlean") m_name = rawname + ".olean"; display_path(out, m_name); import_prefix = true; diff --git a/src/frontends/lean/inductive_cmd.cpp b/src/frontends/lean/inductive_cmd.cpp index 96d007e33..62bbf553d 100644 --- a/src/frontends/lean/inductive_cmd.cpp +++ b/src/frontends/lean/inductive_cmd.cpp @@ -727,9 +727,11 @@ struct inductive_cmd_fn { name const & n = inductive_decl_name(d); pos_info pos = *m_decl_pos_map.find(n); env = mk_rec_on(env, n); - env = mk_induction_on(env, n); save_def_info(name(n, "rec_on"), pos); - save_def_info(name(n, "induction_on"), pos); + if (env.impredicative()) { + env = mk_induction_on(env, n); + save_def_info(name(n, "induction_on"), pos); + } if (has_unit) { env = mk_cases_on(env, n); save_def_info(name(n, "cases_on"), pos); @@ -740,9 +742,11 @@ struct inductive_cmd_fn { } if (has_prod) { env = mk_below(env, n); - env = mk_ibelow(env, n); save_if_defined(name{n, "below"}, pos); - save_if_defined(name(n, "ibelow"), pos); + if (env.impredicative()) { + env = mk_ibelow(env, n); + save_if_defined(name(n, "ibelow"), pos); + } } } } @@ -751,9 +755,11 @@ struct inductive_cmd_fn { pos_info pos = *m_decl_pos_map.find(n); if (has_unit && has_prod) { env = mk_brec_on(env, n); - env = mk_binduction_on(env, n); save_if_defined(name{n, "brec_on"}, pos); - save_if_defined(name(n, "binduction_on"), pos); + if (env.impredicative()) { + env = mk_binduction_on(env, n); + save_if_defined(name(n, "binduction_on"), pos); + } } } return env; diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp index 23d41da49..896053136 100644 --- a/src/frontends/lean/structure_cmd.cpp +++ b/src/frontends/lean/structure_cmd.cpp @@ -658,13 +658,15 @@ struct structure_cmd_fn { void declare_auxiliary() { m_env = mk_rec_on(m_env, m_name); - m_env = mk_induction_on(m_env, m_name); name rec_on_name(m_name, "rec_on"); - name induction_on_name(m_name, "induction_on"); add_rec_alias(rec_on_name); - add_rec_alias(induction_on_name); save_def_info(rec_on_name); - save_def_info(induction_on_name); + if (m_env.impredicative()) { + m_env = mk_induction_on(m_env, m_name); + name induction_on_name(m_name, "induction_on"); + add_rec_alias(induction_on_name); + save_def_info(induction_on_name); + } add_rec_on_alias(name(m_name, "destruct")); add_rec_on_alias(name(m_name, "cases_on")); } diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 7c499fe67..514c84097 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -10,6 +10,6 @@ add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp definition_cache.cpp declaration_index.cpp print.cpp annotation.cpp typed_expr.cpp let.cpp type_util.cpp protected.cpp metavar_closure.cpp reducible.cpp init_module.cpp - fingerprint.cpp flycheck.cpp) + fingerprint.cpp flycheck.cpp hott_kernel.cpp) target_link_libraries(library ${LEAN_LIBS}) diff --git a/src/library/hott_kernel.cpp b/src/library/hott_kernel.cpp new file mode 100644 index 000000000..95f719f60 --- /dev/null +++ b/src/library/hott_kernel.cpp @@ -0,0 +1,22 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "kernel/inductive/inductive.h" +#include "library/inductive_unifier_plugin.h" + +namespace lean { +using inductive::inductive_normalizer_extension; +/** \brief Create Lean environment for Homotopy Type Theory */ +environment mk_hott_environment(unsigned trust_lvl) { + environment env = environment(trust_lvl, + false /* Type.{0} is not proof irrelevant */, + true /* Eta */, + false /* Type.{0} is not impredicative */, + /* builtin support for inductive */ + std::unique_ptr(new inductive_normalizer_extension())); + return set_unifier_plugin(env, mk_inductive_unifier_plugin()); +} +} diff --git a/src/library/hott_kernel.h b/src/library/hott_kernel.h new file mode 100644 index 000000000..7b7f119a7 --- /dev/null +++ b/src/library/hott_kernel.h @@ -0,0 +1,13 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "kernel/environment.h" + +namespace lean { +/** \brief Create Lean environment for Homotopy Type Theory */ +environment mk_hott_environment(unsigned trust_lvl = 0); +} diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index b0c950a27..bdf23aedb 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -25,6 +25,7 @@ Author: Leonardo de Moura #include "kernel/kernel_exception.h" #include "kernel/formatter.h" #include "library/standard_kernel.h" +#include "library/hott_kernel.h" #include "library/module.h" #include "library/io_state_stream.h" #include "library/definition_cache.h" @@ -45,6 +46,7 @@ using lean::io_state; using lean::io_state_stream; using lean::regular; using lean::mk_environment; +using lean::mk_hott_environment; using lean::set_environment; using lean::set_io_state; using lean::definition_cache; @@ -57,7 +59,7 @@ using lean::declaration_index; using lean::keep_theorem_mode; using lean::module_name; -enum class input_kind { Unspecified, Lean, Lua, Trace }; +enum class input_kind { Unspecified, Lean, HLean, Lua, Trace }; static void on_ctrl_c(int ) { lean::request_interrupt(); @@ -81,6 +83,8 @@ static void display_help(std::ostream & out) { std::cout << "Input format:\n"; std::cout << " --lean use parser for Lean default input format for files,\n"; std::cout << " with unknown extension (default)\n"; + std::cout << " --hlean use parser for Lean default input format \n"; + std::cout << " and use HoTT compatible kernel for files, with unknown extension\n"; std::cout << " --lua use Lua parser for files with unknown extension\n"; std::cout << " --server-trace use lean server trace parser for files with unknown extension\n"; std::cout << "Miscellaneous:\n"; @@ -130,6 +134,7 @@ static struct option g_long_options[] = { {"version", no_argument, 0, 'v'}, {"help", no_argument, 0, 'h'}, {"lean", no_argument, 0, 'l'}, + {"hlean", no_argument, 0, 'H'}, {"lua", no_argument, 0, 'u'}, {"server-trace", no_argument, 0, 'R'}, {"path", no_argument, 0, 'p'}, @@ -155,7 +160,7 @@ static struct option g_long_options[] = { {0, 0, 0, 0} }; -#define BASIC_OPT_STR "RXTFC:dD:qlupgvhk:012t:012o:c:i:" +#define BASIC_OPT_STR "HRXTFC:dD:qlupgvhk:012t:012o:c:i:" #if defined(LEAN_USE_BOOST) && defined(LEAN_MULTI_THREAD) static char const * g_opt_str = BASIC_OPT_STR "Sj:012s:012"; @@ -327,7 +332,7 @@ int main(int argc, char ** argv) { std::string cpp_output; std::string cache_name; std::string index_name; - input_kind default_k = input_kind::Lean; // default + input_kind default_k = input_kind::Unspecified; while (true) { int c = getopt_long(argc, argv, g_opt_str, g_long_options, NULL); if (c == -1) @@ -351,6 +356,9 @@ int main(int argc, char ** argv) { case 'l': default_k = input_kind::Lean; break; + case 'H': + default_k = input_kind::HLean; + break; case 'u': default_k = input_kind::Lua; break; @@ -419,7 +427,35 @@ int main(int argc, char ** argv) { lean_assert(num_threads == 1); #endif - environment env = mk_environment(trust_lvl); + bool has_lean = (default_k == input_kind::Lean); + bool has_hlean = (default_k == input_kind::HLean); + for (int i = optind; i < argc; i++) { + char const * ext = get_file_extension(argv[i]); + if (strcmp(ext, "lean") == 0) { + has_lean = true; + if (has_hlean) { + std::cerr << ".hlean file cannot be mixed with .lean files\n"; + return 1; + } + if (default_k == input_kind::Unspecified) + default_k = input_kind::Lean; + } else if (strcmp(ext, "hlean") == 0) { + has_hlean = true; + if (has_lean) { + std::cerr << ".lean file cannot be mixed with .hlean files\n"; + return 1; + } + if (default_k == input_kind::Unspecified) + default_k = input_kind::HLean; + } + } + if (default_k == input_kind::Unspecified) + default_k = input_kind::Lean; + + if (has_hlean) + lean::initialize_lean_path(true); + + environment env = has_hlean ? mk_hott_environment(trust_lvl) : mk_environment(trust_lvl); io_state ios(opts, lean::mk_pretty_formatter_factory()); script_state S = lean::get_thread_script_state(); set_environment set1(S, env); @@ -446,12 +482,15 @@ int main(int argc, char ** argv) { if (ext) { if (strcmp(ext, "lean") == 0) { k = input_kind::Lean; + } else if (strcmp(ext, "hlean") == 0) { + k = input_kind::HLean; } else if (strcmp(ext, "lua") == 0) { k = input_kind::Lua; } } switch (k) { case input_kind::Lean: + case input_kind::HLean: if (only_deps) { if (!display_deps(env, std::cout, std::cerr, argv[i])) ok = false; diff --git a/src/util/lean_path.cpp b/src/util/lean_path.cpp index bf0e64002..15742768b 100644 --- a/src/util/lean_path.cpp +++ b/src/util/lean_path.cpp @@ -118,15 +118,22 @@ std::string get_path(std::string f) { static std::string * g_lean_path = nullptr; static std::vector * g_lean_path_vector = nullptr; -void init_lean_path() { +void init_lean_path(bool use_hott) { #if defined(LEAN_EMSCRIPTEN) *g_lean_path = "/library"; g_lean_path_vector->push_back(*g_lean_path); #else - char * r = getenv("LEAN_PATH"); + char * r = nullptr; + if (use_hott) + r = getenv("LEAN_PATH"); + else + r = getenv("HLEAN_PATH"); if (r == nullptr) { std::string exe_path = get_path(get_exe_location()); - *g_lean_path = exe_path + g_sep + ".." + g_sep + "library"; + if (use_hott) + *g_lean_path = exe_path + g_sep + ".." + g_sep + "hott"; + else + *g_lean_path = exe_path + g_sep + ".." + g_sep + "library"; *g_lean_path += g_path_sep; *g_lean_path += exe_path + g_sep + ".." + g_sep + "lib" + g_sep + "lean"; *g_lean_path += g_path_sep; @@ -153,13 +160,13 @@ void init_lean_path() { static char g_sep_str[2]; -void initialize_lean_path() { +void initialize_lean_path(bool use_hott) { g_default_file_name = new std::string(LEAN_DEFAULT_MODULE_FILE_NAME); g_lean_path = new std::string(); g_lean_path_vector = new std::vector(); g_sep_str[0] = g_sep; g_sep_str[1] = 0; - init_lean_path(); + init_lean_path(use_hott); } void finalize_lean_path() { @@ -173,6 +180,10 @@ bool has_file_ext(std::string const & fname, char const * ext) { return fname.size() > ext_len && fname.substr(fname.size() - ext_len, ext_len) == ext; } +bool is_hlean_file(std::string const & fname) { + return has_file_ext(fname, ".hlean"); +} + bool is_lean_file(std::string const & fname) { return has_file_ext(fname, ".lean"); } @@ -186,7 +197,7 @@ bool is_lua_file(std::string const & fname) { } bool is_known_file_ext(std::string const & fname) { - return is_lean_file(fname) || is_olean_file(fname) || is_lua_file(fname); + return is_lean_file(fname) || is_hlean_file(fname) || is_olean_file(fname) || is_lua_file(fname); } optional check_file_core(std::string file, char const * ext) { diff --git a/src/util/lean_path.h b/src/util/lean_path.h index 16711e735..aa40742c1 100644 --- a/src/util/lean_path.h +++ b/src/util/lean_path.h @@ -55,6 +55,6 @@ void display_path(std::ostream & out, std::string const & fname); std::string dirname(char const * fname); std::string path_append(char const * path1, char const * path2); -void initialize_lean_path(); +void initialize_lean_path(bool use_hott = false); void finalize_lean_path(); }