From dd31ed60b01e8e33dbbbcf0db6800f2f51959164 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 18 Sep 2014 20:03:24 -0700 Subject: [PATCH] refactor(library): remove unnecessary file hott_kernel, HoTT and standard library have been merged --- src/library/CMakeLists.txt | 2 +- src/library/hott_kernel.cpp | 27 --------------------- src/library/hott_kernel.h | 11 --------- src/library/kernel_bindings.cpp | 8 ------- tests/lua/env10.lua | 42 --------------------------------- tests/lua/ind1.lua | 13 ---------- 6 files changed, 1 insertion(+), 102 deletions(-) delete mode 100644 src/library/hott_kernel.cpp delete mode 100644 src/library/hott_kernel.h delete mode 100644 tests/lua/env10.lua diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 197d95b99d..ad658ebfcc 100644 --- a/src/library/CMakeLists.txt +++ b/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 diff --git a/src/library/hott_kernel.cpp b/src/library/hott_kernel.cpp deleted file mode 100644 index ec53b9c4e9..0000000000 --- a/src/library/hott_kernel.cpp +++ /dev/null @@ -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(new inductive_normalizer_extension()), - std::unique_ptr(new record_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 deleted file mode 100644 index 18c98be268..0000000000 --- a/src/library/hott_kernel.h +++ /dev/null @@ -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); -} diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index d94ab9a900..0947514668 100644 --- a/src/library/kernel_bindings.cpp +++ b/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"); } diff --git a/tests/lua/env10.lua b/tests/lua/env10.lua deleted file mode 100644 index d60e1299fd..0000000000 --- a/tests/lua/env10.lua +++ /dev/null @@ -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 -) diff --git a/tests/lua/ind1.lua b/tests/lua/ind1.lua index e30155cd86..76b5bbdde7 100644 --- a/tests/lua/ind1.lua +++ b/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}))