refactor(library): remove unnecessary file hott_kernel, HoTT and

standard library have been merged

src/library/CMakeLists.txt

@@ -4,7 +4,7 @@ add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp
   normalize.cpp shared_environment.cpp module.cpp coercion.cpp
   private.cpp placeholder.cpp aliases.cpp level_names.cpp
   update_declaration.cpp choice.cpp scoped_ext.cpp locals.cpp
-  standard_kernel.cpp hott_kernel.cpp sorry.cpp
+  standard_kernel.cpp sorry.cpp
   unifier.cpp unifier_plugin.cpp inductive_unifier_plugin.cpp
   explicit.cpp num.cpp string.cpp opaque_hints.cpp head_map.cpp
   match.cpp definition_cache.cpp declaration_index.cpp

src/library/hott_kernel.cpp

@@ -1,27 +0,0 @@
-/*
-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 "kernel/record/record.h"
-#include "library/inductive_unifier_plugin.h"
-
-namespace lean {
-using inductive::inductive_normalizer_extension;
-using record::record_normalizer_extension;
-
-/** \brief Create a HoTT (Homotopy Type Theory) compatible environment */
-environment mk_hott_environment(unsigned trust_lvl) {
-    environment env = environment(trust_lvl,
-                                  false /* Type.{0} is proof relevant */,
-                                  true  /* Eta */,
-                                  false /* Type.{0} is predicative */,
-                                  to_list(name("Id")) /* Exact equality types are proof irrelevant */,
-                                  /* builtin support for inductive and record datatypes */
-                                  compose(std::unique_ptr<normalizer_extension>(new inductive_normalizer_extension()),
-                                          std::unique_ptr<normalizer_extension>(new record_normalizer_extension())));
-    return set_unifier_plugin(env, mk_inductive_unifier_plugin());
-}
-}

src/library/hott_kernel.h

@@ -1,11 +0,0 @@
-/*
-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 {
-environment mk_hott_environment(unsigned trust_lvl = 0);
-}

src/library/kernel_bindings.cpp

@@ -23,7 +23,6 @@ Author: Leonardo de Moura
 #include "kernel/replace_fn.h"
 #include "kernel/inductive/inductive.h"
 #include "library/standard_kernel.h"
-#include "library/hott_kernel.h"
 #include "library/occurs.h"
 #include "library/io_state_stream.h"
 #include "library/expr_lt.h"
@@ -1043,7 +1042,6 @@ static unsigned get_trust_lvl(lua_State * L, int i) {
     return trust_lvl;
 }
 static int mk_environment(lua_State * L)      { return push_environment(L, mk_environment(get_trust_lvl(L, 1))); }
-static int mk_hott_environment(lua_State * L) { return push_environment(L, mk_hott_environment(get_trust_lvl(L, 1))); }
 
 static int environment_forget(lua_State * L) { return push_environment(L, to_environment(L, 1).forget()); }
 static int environment_whnf(lua_State * L) { return push_ecs(L, type_checker(to_environment(L, 1)).whnf(to_expr(L, 2))); }
@@ -1110,10 +1108,6 @@ static int import_modules(lua_State * L) {
         return import_modules(mk_environment(), L, 1);
 }
 
-static int import_hott_modules(lua_State * L) {
-    return import_modules(mk_hott_environment(), L, 1);
-}
-
 static int export_module(lua_State * L) {
     std::ofstream out(lua_tostring(L, 2), std::ofstream::binary);
     export_module(out, to_environment(L, 1));
@@ -1199,14 +1193,12 @@ static void open_environment(lua_State * L) {
 
     SET_GLOBAL_FUN(mk_bare_environment,    "bare_environment");
     SET_GLOBAL_FUN(mk_environment,         "environment");
-    SET_GLOBAL_FUN(mk_hott_environment,    "hott_environment");
     SET_GLOBAL_FUN(environment_pred,       "is_environment");
     SET_GLOBAL_FUN(get_environment,        "get_environment");
     SET_GLOBAL_FUN(get_environment,        "get_env");
     SET_GLOBAL_FUN(set_environment,        "set_environment");
     SET_GLOBAL_FUN(set_environment,        "set_env");
     SET_GLOBAL_FUN(import_modules,         "import_modules");
-    SET_GLOBAL_FUN(import_hott_modules,    "import_hott_modules");
     SET_GLOBAL_FUN(export_module,          "export_module");
 }
 

tests/lua/env10.lua

@@ -1,42 +0,0 @@
-local env = hott_environment()
-assert(not env:impredicative())
-assert(not env:prop_proof_irrel())
-
-local l        = param_univ("l")
-local U_l      = mk_sort(l)
-local A        = Local("A", U_l)
-local list_l   = Const("list", {l})
-
--- In HoTT environments, we don't need to use max(l, 1) trick
--- in the following definition
-env = add_inductive(env,
-                    "list", {l}, 1, Pi(A, U_l),
-                    "nil", Pi(A, list_l(A)),
-                    "cons", Pi(A, mk_arrow(A, list_l(A), list_l(A))))
-
-local l1          = param_univ("l1")
-local l2          = param_univ("l2")
-local U_l1        = mk_sort(l1)
-local U_l2        = mk_sort(l2)
-local U_l1l2      = mk_sort(max_univ(l1, l2))
-local A           = Local("A", U_l1)
-local B           = Local("B", U_l2)
-local a           = Local("a", A)
-local b           = Local("b", B)
-local sigma_l1l2  = Const("sigma", {l1, l2})
-
-env = add_inductive(env,
-                    "sigma", {l1, l2}, 2, Pi(A, B, U_l1l2),
-                    "pair", Pi(A, B, a, b, sigma_l1l2(A, B)))
-
-local coproduct_l1l2 = Const("coproduct", {l1, l2})
-
-env = add_inductive(env,
-                    "coproduct", {l1, l2}, 2, Pi(A, B, U_l1l2),
-                    "inl", Pi(A, B, a, coproduct_l1l2(A, B)),
-                    "inr", Pi(A, B, b, coproduct_l1l2(A, B)))
-
-env:for_each_decl(function(d)
-                     print(tostring(d:name()) .. " : " .. tostring(d:type()))
-                  end
-)

tests/lua/ind1.lua

@@ -143,16 +143,3 @@ local tc = type_checker(env2)
 assert(tc:is_def_eq(length(nil_nat), zero))
 assert(tc:is_def_eq(length(cons_nat(zero, nil_nat)), succ(zero)))
 assert(tc:is_def_eq(length(cons_nat(zero, cons_nat(zero, nil_nat))), succ(succ(zero))))
-
--- Martin-Lof style identity type
-local env  = hott_environment()
-local Id_l = Const("Id", {l})
-local A = Local("A", U_l)
-local a = Local("a", A)
-local b = Local("b", A)
-env = env:add_universe("u")
-env = env:add_universe("v")
-env = add_inductive(env,
-                    "Id", {l}, 1, Pi(A, a, b, U_l),
-                    "Id_refl", Pi(A, b, Id_l(A, b, b)))
-display_type(env, Const({"Id", "rec"}, {v, u}))