feat(*): add support for separate HoTT library

hott/.project

@@ -0,0 +1,4 @@
++ *.hlean
+- flycheck*.lean
+- flycheck*.hlean
+- .#*.hlean

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)

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

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<unsigned> 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;

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;

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"));
     }

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})

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<normalizer_extension>(new inductive_normalizer_extension()));
+    return set_unifier_plugin(env, mk_inductive_unifier_plugin());
+}
+}

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);
+}

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;

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<std::string> * 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<std::string>();
     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<std::string> check_file_core(std::string file, char const * ext) {

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();
 }