chore(library/coercion): remove lua bindings for coercion module
Reason: we will refactor the coercion module. See issue #668
This commit is contained in:
Leonardo de Moura
parent
667f647b27
commit
0f5b7a36f5
9 changed files with 0 additions and 359 deletions
|
|
@ -535,114 +535,4 @@ void for_each_coercion_fun(environment const & env, coercion_fun_fn const & f) {
|
||||||
f(C, info.m_fun, info.m_level_params, info.m_num_args);
|
f(C, info.m_fun, info.m_level_params, info.m_num_args);
|
||||||
});
|
});
|
||||||
}
|
}
|
||||||
|
|
||||||
static int add_coercion(lua_State * L) {
|
|
||||||
int nargs = lua_gettop(L);
|
|
||||||
if (nargs == 2)
|
|
||||||
return push_environment(L, add_coercion(to_environment(L, 1), to_name_ext(L, 2), get_io_state(L)));
|
|
||||||
else if (nargs == 3 && is_io_state(L, 3))
|
|
||||||
return push_environment(L, add_coercion(to_environment(L, 1), to_name_ext(L, 2), to_io_state(L, 3)));
|
|
||||||
else if (nargs == 3)
|
|
||||||
return push_environment(L, add_coercion(to_environment(L, 1), to_name_ext(L, 2), to_name_ext(L, 3), get_io_state(L)));
|
|
||||||
else
|
|
||||||
return push_environment(L, add_coercion(to_environment(L, 1), to_name_ext(L, 2), to_name_ext(L, 3), to_io_state(L, 4)));
|
|
||||||
}
|
|
||||||
|
|
||||||
static int is_coercion(lua_State * L) {
|
|
||||||
optional<pair<name, unsigned>> r;
|
|
||||||
if (is_expr(L, 2))
|
|
||||||
r = is_coercion(to_environment(L, 1), to_expr(L, 2));
|
|
||||||
else
|
|
||||||
r = is_coercion(to_environment(L, 1), to_name_ext(L, 2));
|
|
||||||
if (r) {
|
|
||||||
push_name(L, r->first);
|
|
||||||
push_integer(L, r->second);
|
|
||||||
return 2;
|
|
||||||
} else {
|
|
||||||
return 0;
|
|
||||||
}
|
|
||||||
}
|
|
||||||
|
|
||||||
static int has_coercions_from(lua_State * L) {
|
|
||||||
if (is_expr(L, 2))
|
|
||||||
return push_boolean(L, has_coercions_from(to_environment(L, 1), to_expr(L, 2)));
|
|
||||||
else
|
|
||||||
return push_boolean(L, has_coercions_from(to_environment(L, 1), to_name_ext(L, 2)));
|
|
||||||
}
|
|
||||||
|
|
||||||
static int get_coercions(lua_State * L) {
|
|
||||||
return push_list_expr(L, get_coercions(to_environment(L, 1), to_expr(L, 2), to_name_ext(L, 3)));
|
|
||||||
}
|
|
||||||
|
|
||||||
static int get_coercions_to_sort(lua_State * L) {
|
|
||||||
return push_list_expr(L, get_coercions_to_sort(to_environment(L, 1), to_expr(L, 2)));
|
|
||||||
}
|
|
||||||
|
|
||||||
static int get_coercions_to_fun(lua_State * L) {
|
|
||||||
return push_list_expr(L, get_coercions_to_fun(to_environment(L, 1), to_expr(L, 2)));
|
|
||||||
}
|
|
||||||
|
|
||||||
static int get_coercions_from(lua_State * L) {
|
|
||||||
buffer<std::tuple<coercion_class, expr, expr>> r;
|
|
||||||
get_coercions_from(to_environment(L, 1), to_expr(L, 2), r);
|
|
||||||
lua_newtable(L);
|
|
||||||
int i = 1;
|
|
||||||
for (auto p : r) {
|
|
||||||
lua_newtable(L);
|
|
||||||
coercion_class c = std::get<0>(p);
|
|
||||||
push_integer(L, static_cast<unsigned>(c.kind()));
|
|
||||||
lua_rawseti(L, -2, 1);
|
|
||||||
if (c.kind() == coercion_class_kind::User) {
|
|
||||||
push_name(L, c.get_name());
|
|
||||||
} else {
|
|
||||||
push_nil(L);
|
|
||||||
}
|
|
||||||
lua_rawseti(L, -2, 2);
|
|
||||||
push_expr(L, std::get<1>(p));
|
|
||||||
lua_rawseti(L, -2, 3);
|
|
||||||
push_expr(L, std::get<2>(p));
|
|
||||||
lua_rawseti(L, -2, 4);
|
|
||||||
lua_rawseti(L, -2, i);
|
|
||||||
i = i + 1;
|
|
||||||
}
|
|
||||||
return 1;
|
|
||||||
}
|
|
||||||
|
|
||||||
static int for_each_coercion(lua_State * L, coercion_class_kind k) {
|
|
||||||
environment env = to_environment(L, 1);
|
|
||||||
luaL_checktype(L, 2, LUA_TFUNCTION); // user-fun
|
|
||||||
for_each_coercion(env, [&](name const & C, coercion_info const & info) {
|
|
||||||
if (info.m_to.kind() != k)
|
|
||||||
return;
|
|
||||||
lua_pushvalue(L, 2); // push user-fun
|
|
||||||
push_name(L, C);
|
|
||||||
int nargs = 4;
|
|
||||||
if (info.m_to.kind() == coercion_class_kind::User) {
|
|
||||||
push_name(L, info.m_to.get_name());
|
|
||||||
nargs++;
|
|
||||||
}
|
|
||||||
push_expr(L, info.m_fun);
|
|
||||||
push_list_name(L, info.m_level_params);
|
|
||||||
push_integer(L, info.m_num_args);
|
|
||||||
pcall(L, nargs, 0, 0);
|
|
||||||
});
|
|
||||||
return 0;
|
|
||||||
}
|
|
||||||
|
|
||||||
static int for_each_coercion_user(lua_State * L) { return for_each_coercion(L, coercion_class_kind::User); }
|
|
||||||
static int for_each_coercion_sort(lua_State * L) { return for_each_coercion(L, coercion_class_kind::Sort); }
|
|
||||||
static int for_each_coercion_fun(lua_State * L) { return for_each_coercion(L, coercion_class_kind::Fun); }
|
|
||||||
|
|
||||||
void open_coercion(lua_State * L) {
|
|
||||||
SET_GLOBAL_FUN(add_coercion, "add_coercion");
|
|
||||||
SET_GLOBAL_FUN(is_coercion, "is_coercion");
|
|
||||||
SET_GLOBAL_FUN(has_coercions_from, "has_coercions_from");
|
|
||||||
SET_GLOBAL_FUN(get_coercions, "get_coercions");
|
|
||||||
SET_GLOBAL_FUN(get_coercions_to_sort, "get_coercions_to_sort");
|
|
||||||
SET_GLOBAL_FUN(get_coercions_to_fun, "get_coercions_to_fun");
|
|
||||||
SET_GLOBAL_FUN(get_coercions_from, "get_coercions_from");
|
|
||||||
SET_GLOBAL_FUN(for_each_coercion_user, "for_each_coercion_user");
|
|
||||||
SET_GLOBAL_FUN(for_each_coercion_sort, "for_each_coercion_sort");
|
|
||||||
SET_GLOBAL_FUN(for_each_coercion_fun, "for_each_coercion_fun");
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -96,7 +96,6 @@ typedef std::function<void(name const &, expr const &, level_param_names const &
|
||||||
void for_each_coercion_user(environment const & env, coercion_user_fn const & f);
|
void for_each_coercion_user(environment const & env, coercion_user_fn const & f);
|
||||||
void for_each_coercion_sort(environment const & env, coercion_sort_fn const & f);
|
void for_each_coercion_sort(environment const & env, coercion_sort_fn const & f);
|
||||||
void for_each_coercion_fun(environment const & env, coercion_fun_fn const & f);
|
void for_each_coercion_fun(environment const & env, coercion_fun_fn const & f);
|
||||||
void open_coercion(lua_State * L);
|
|
||||||
void initialize_coercion();
|
void initialize_coercion();
|
||||||
void finalize_coercion();
|
void finalize_coercion();
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -8,7 +8,6 @@ Author: Leonardo de Moura
|
||||||
#include "util/script_state.h"
|
#include "util/script_state.h"
|
||||||
#include "library/kernel_bindings.h"
|
#include "library/kernel_bindings.h"
|
||||||
#include "library/resolve_macro.h"
|
#include "library/resolve_macro.h"
|
||||||
#include "library/coercion.h"
|
|
||||||
#include "library/private.h"
|
#include "library/private.h"
|
||||||
#include "library/placeholder.h"
|
#include "library/placeholder.h"
|
||||||
#include "library/aliases.h"
|
#include "library/aliases.h"
|
||||||
|
|
@ -24,7 +23,6 @@ namespace lean {
|
||||||
inline void open_core_module(lua_State * L) {
|
inline void open_core_module(lua_State * L) {
|
||||||
open_kernel_module(L);
|
open_kernel_module(L);
|
||||||
open_resolve_macro(L);
|
open_resolve_macro(L);
|
||||||
open_coercion(L);
|
|
||||||
open_private(L);
|
open_private(L);
|
||||||
open_placeholder(L);
|
open_placeholder(L);
|
||||||
open_aliases(L);
|
open_aliases(L);
|
||||||
|
|
|
||||||
|
|
@ -1,90 +0,0 @@
|
||||||
local env = environment()
|
|
||||||
local l = param_univ("l")
|
|
||||||
local nat = Const("nat")
|
|
||||||
local real = Const("real")
|
|
||||||
local one = Const("one")
|
|
||||||
local Ul = mk_sort(l)
|
|
||||||
local lst_l = Const("lst", {l})
|
|
||||||
local vec_l = Const("vec", {l})
|
|
||||||
local mat_l = Const("mat", {l})
|
|
||||||
local A = Local("A", Ul)
|
|
||||||
local n = Local("n", nat)
|
|
||||||
local ll = Local("ll", lst_l(A))
|
|
||||||
local len_l = Const("len", {l})
|
|
||||||
local lst_1 = Const("lst", {1})
|
|
||||||
local l1 = param_univ("l1")
|
|
||||||
local l2 = param_univ("l2")
|
|
||||||
local m = Local("m", nat)
|
|
||||||
env = add_decl(env, mk_constant_assumption("nat", Type))
|
|
||||||
env = add_decl(env, mk_constant_assumption("real", Type))
|
|
||||||
env = add_decl(env, mk_constant_assumption("one", nat))
|
|
||||||
env = add_decl(env, mk_constant_assumption("lst", {l}, mk_arrow(Ul, Ul)))
|
|
||||||
env = add_decl(env, mk_constant_assumption("len", {l}, Pi(A, mk_arrow(lst_l(A), nat))))
|
|
||||||
env = add_decl(env, mk_constant_assumption("vec", {l}, mk_arrow(Ul, nat, Ul)))
|
|
||||||
env = add_decl(env, mk_constant_assumption("mat", {l}, mk_arrow(Ul, nat, nat, Ul)))
|
|
||||||
env = add_decl(env, mk_constant_assumption("dlst", {l1, l2}, mk_arrow(mk_sort(l1), mk_sort(l2), mk_sort(max_univ(l1, l2)))))
|
|
||||||
env = add_decl(env, mk_constant_assumption("vec2lst", {l}, Pi(A, n, mk_arrow(vec_l(A, n), lst_l(A)))))
|
|
||||||
env = add_decl(env, mk_constant_assumption("lst2vec", {l}, Pi(A, ll, vec_l(A, len_l(A, ll)))))
|
|
||||||
env = add_decl(env, mk_constant_assumption("vec2mat", {l}, Pi(A, n, mk_arrow(vec_l(A, n), mat_l(A, n, one)))))
|
|
||||||
env = add_decl(env, mk_constant_assumption("mat2dlst", {l}, Pi(A, n, m, mk_arrow(mat_l(A, n, m), Const("dlst", {l, 1})(A, nat)))))
|
|
||||||
env = add_decl(env, mk_constant_assumption("nat2lst", mk_arrow(nat, lst_1(nat))))
|
|
||||||
env = add_coercion(env, "lst2vec")
|
|
||||||
assert(is_coercion(env, Const("lst2vec", {l})))
|
|
||||||
assert(has_coercions_from(env, "lst"))
|
|
||||||
local lst_nat = lst_1(nat)
|
|
||||||
|
|
||||||
function display_coercions(coes)
|
|
||||||
if not coes:is_nil() then
|
|
||||||
print(coes:head())
|
|
||||||
display_coercions(coes:tail())
|
|
||||||
end
|
|
||||||
end
|
|
||||||
|
|
||||||
display_coercions(get_coercions(env, lst_nat, "vec"))
|
|
||||||
env = add_coercion(env, "vec2mat")
|
|
||||||
display_coercions(get_coercions(env, lst_nat, "mat"))
|
|
||||||
assert(env:type_check(get_coercions(env, lst_nat, "mat"):head()))
|
|
||||||
for_each_coercion_user(env, function(C, D, f) print(tostring(C) .. " >-> " .. tostring(D) .. " : " .. tostring(f)) end)
|
|
||||||
env = add_coercion(env, "nat2lst")
|
|
||||||
print("---------")
|
|
||||||
for_each_coercion_user(env, function(C, D, f) print(tostring(C) .. " >-> " .. tostring(D) .. " : " .. tostring(f)) end)
|
|
||||||
print(get_coercions(env, nat, "mat"):head())
|
|
||||||
assert(env:type_check(get_coercions(env, nat, "mat"):head()))
|
|
||||||
env = add_coercion(env, "mat2dlst")
|
|
||||||
print("---------")
|
|
||||||
for_each_coercion_user(env, function(C, D, f) print(tostring(C) .. " >-> " .. tostring(D) .. " : " .. tostring(f)) end)
|
|
||||||
print(get_coercions(env, lst_nat, "dlst"):head())
|
|
||||||
assert(env:type_check(get_coercions(env, lst_nat, "dlst"):head()))
|
|
||||||
|
|
||||||
env:export("coe1_mod.olean")
|
|
||||||
local env2 = import_modules("coe1_mod")
|
|
||||||
print(get_coercions(env2, lst_nat, "dlst"):head())
|
|
||||||
assert(env2:type_check(get_coercions(env2, lst_nat, "dlst"):head()))
|
|
||||||
assert(is_coercion(env2, "vec2mat"))
|
|
||||||
assert(is_coercion(env2, "lst2vec"))
|
|
||||||
env2 = add_decl(env2, mk_constant_assumption("lst2vec2", {l}, Pi(A, ll, vec_l(A, len_l(A, ll)))))
|
|
||||||
print("======")
|
|
||||||
env2 = add_coercion(env2, "lst2vec2")
|
|
||||||
print("======")
|
|
||||||
print(get_coercions(env2, lst_nat, "dlst"):head())
|
|
||||||
print("---------")
|
|
||||||
for_each_coercion_user(env2, function(C, D, f) print(tostring(C) .. " >-> " .. tostring(D) .. " : " .. tostring(f)) end)
|
|
||||||
env2 = add_coercion(env2, "vec2lst")
|
|
||||||
env2 = add_decl(env2, mk_constant_assumption("lst2nat", {l}, Pi(A, mk_arrow(lst_l(A), nat))))
|
|
||||||
env2 = add_coercion(env2, "lst2nat")
|
|
||||||
print("---------")
|
|
||||||
for_each_coercion_user(env2, function(C, D, f) print(tostring(C) .. " >-> " .. tostring(D)) end)
|
|
||||||
for_each_coercion_user(env2, function(C, D, f) print(tostring(C) .. " >-> " .. tostring(D) .. " : " .. tostring(f)) end)
|
|
||||||
|
|
||||||
assert(has_coercions_from(env2, lst_nat))
|
|
||||||
assert(not has_coercions_from(env2, Const("foo")))
|
|
||||||
assert(not has_coercions_from(env2, Const("lst", {1})))
|
|
||||||
assert(has_coercions_from(env2, Const("vec", {1})(nat, one)))
|
|
||||||
assert(not has_coercions_from(env2, Const("vec", {1})(nat)))
|
|
||||||
assert(not has_coercions_from(env2, Const("vec")(nat, one)))
|
|
||||||
|
|
||||||
print("Coercions (vec nat one): ")
|
|
||||||
cs = get_coercions_from(env2, Const("vec", {1})(nat, one))
|
|
||||||
for i = 1, #cs do
|
|
||||||
print(tostring(cs[i][2]) .. " : " .. tostring(cs[i][4]) .. " : " .. tostring(cs[i][3]))
|
|
||||||
end
|
|
||||||
|
|
@ -1,21 +0,0 @@
|
||||||
local env = environment()
|
|
||||||
local l1 = param_univ("l1")
|
|
||||||
local l2 = param_univ("l2")
|
|
||||||
env = add_decl(env, mk_constant_assumption("functor", {l1, l2}, mk_arrow(mk_sort(l1), mk_sort(l2), mk_sort(imax_univ(l1, l2)))))
|
|
||||||
local A = Local("A", mk_sort(l1))
|
|
||||||
local B = Local("B", mk_sort(l2))
|
|
||||||
local functor = Const("functor", {l1, l2})
|
|
||||||
env = add_decl(env, mk_constant_assumption("to_fun", {l1, l2}, Pi(A, B, mk_arrow(functor(A, B), mk_arrow(A, B)))))
|
|
||||||
env = add_coercion(env, "to_fun", "functor")
|
|
||||||
for_each_coercion_fun(env, function(C, f) print(tostring(C) .. " >-> function : " .. tostring(f)) end)
|
|
||||||
env = add_decl(env, mk_constant_assumption("nat", Type))
|
|
||||||
env = add_decl(env, mk_constant_assumption("real", Type))
|
|
||||||
local nat = Const("nat")
|
|
||||||
local real = Const("real")
|
|
||||||
env = add_decl(env, mk_constant_assumption("f1", Const("functor", {1, 1})(nat, real)))
|
|
||||||
print(get_coercions_to_fun(env, Const("functor", {1, 1})(nat, real)):head())
|
|
||||||
env = add_decl(env, mk_constant_assumption("sfunctor", {l1}, mk_arrow(mk_sort(l1), mk_sort(l1))))
|
|
||||||
env = add_decl(env, mk_constant_assumption("sf2f", {l1}, Pi(A, mk_arrow(Const("sfunctor", {l1})(A), Const("functor", {l1, l1})(A, A)))))
|
|
||||||
env = add_coercion(env, "sf2f")
|
|
||||||
print(get_coercions_to_fun(env, Const("sfunctor", {1})(nat)):head())
|
|
||||||
assert(env:type_check(get_coercions_to_fun(env, Const("sfunctor", {1})(nat)):head()))
|
|
||||||
|
|
@ -1,13 +0,0 @@
|
||||||
local env = environment()
|
|
||||||
local l = param_univ("l")
|
|
||||||
env = add_decl(env, mk_constant_assumption("group", {l}, mk_sort(l+1)))
|
|
||||||
env = add_decl(env, mk_constant_assumption("abelian_group", {l}, mk_sort(l+1)))
|
|
||||||
local group = Const("group", {l})
|
|
||||||
local ab_group = Const("abelian_group", {l})
|
|
||||||
env = add_decl(env, mk_constant_assumption("carrier", {l}, mk_arrow(group, mk_sort(l))))
|
|
||||||
env = add_coercion(env, "carrier")
|
|
||||||
env = add_decl(env, mk_constant_assumption("abg2g", {l}, mk_arrow(ab_group, group)))
|
|
||||||
env = add_coercion(env, "abg2g")
|
|
||||||
for_each_coercion_sort(env, function(C, f) print(tostring(C) .. " >-> sort : " .. tostring(f)) end)
|
|
||||||
print(get_coercions_to_sort(env, Const("abelian_group", {1})):head())
|
|
||||||
assert(env:type_check(get_coercions_to_sort(env, Const("abelian_group", {1})):head()))
|
|
||||||
|
|
@ -1,23 +0,0 @@
|
||||||
local env = environment()
|
|
||||||
local l = param_univ("l")
|
|
||||||
local Ul = mk_sort(l)
|
|
||||||
local lst_l = Const("lst", {l})
|
|
||||||
local A = Local("A", Ul)
|
|
||||||
env = add_decl(env, mk_constant_assumption("lst", {l}, mk_arrow(Ul, Ul)))
|
|
||||||
env = add_decl(env, mk_constant_assumption("lst2lst", {l}, Pi(A, mk_arrow(lst_l(A), lst_l(A)))))
|
|
||||||
env = add_decl(env, mk_constant_assumption("head", {l}, Pi(A, mk_arrow(lst_l(A), A))))
|
|
||||||
env = add_decl(env, mk_constant_assumption("id", {l}, Pi(A, mk_arrow(A, A))))
|
|
||||||
function add_bad_coercion(env, c)
|
|
||||||
ok, msg = pcall(function() add_coercion(env, c) end)
|
|
||||||
assert(not ok)
|
|
||||||
print("Expected error: " .. tostring(msg:what()))
|
|
||||||
end
|
|
||||||
function add_bad_coercion2(env, c, cls)
|
|
||||||
ok, msg = pcall(function() add_coercion(env, c, cls) end)
|
|
||||||
assert(not ok)
|
|
||||||
print("Expected error: " .. tostring(msg:what()))
|
|
||||||
end
|
|
||||||
add_bad_coercion(env, "lst2lst")
|
|
||||||
add_bad_coercion(env, "head")
|
|
||||||
add_bad_coercion(env, "id")
|
|
||||||
add_bad_coercion2(env, "head", "lst")
|
|
||||||
|
|
@ -1,31 +0,0 @@
|
||||||
local env = environment()
|
|
||||||
local l = param_univ("l")
|
|
||||||
env = add_decl(env, mk_constant_assumption("group", {l}, mk_sort(l+1)))
|
|
||||||
env = add_decl(env, mk_constant_assumption("abelian_group", {l}, mk_sort(l+1)))
|
|
||||||
env = add_decl(env, mk_constant_assumption("ring", {l}, mk_sort(l+1)))
|
|
||||||
env = add_decl(env, mk_constant_assumption("abelian_ring", {l}, mk_sort(l+1)))
|
|
||||||
local group = Const("group", {l})
|
|
||||||
local ring = Const("ring", {l})
|
|
||||||
local ab_group = Const("abelian_group", {l})
|
|
||||||
local ab_ring = Const("abelian_ring", {l})
|
|
||||||
env = add_decl(env, mk_constant_assumption("carrier", {l}, mk_arrow(group, mk_sort(l))))
|
|
||||||
env = add_coercion(env, "carrier")
|
|
||||||
|
|
||||||
env = add_decl(env, mk_constant_assumption("ag2g", {l}, mk_arrow(ab_group, group)))
|
|
||||||
env = add_decl(env, mk_constant_assumption("r2g", {l}, mk_arrow(ring, group)))
|
|
||||||
env = add_decl(env, mk_constant_assumption("ar2r", {l}, mk_arrow(ab_ring, ring)))
|
|
||||||
env = add_decl(env, mk_constant_assumption("ar2ag", {l}, mk_arrow(ab_ring, ab_group)))
|
|
||||||
env = add_coercion(env, "ag2g")
|
|
||||||
env = add_coercion(env, "r2g")
|
|
||||||
env = add_coercion(env, "ar2r")
|
|
||||||
env = add_coercion(env, "ar2ag")
|
|
||||||
for_each_coercion_sort(env, function(C, f) print(tostring(C) .. " >-> sort : " .. tostring(f)) end)
|
|
||||||
for_each_coercion_user(env, function(C, D, f) print(tostring(C) .. " >-> " .. tostring(D) .. " : " .. tostring(f)) end)
|
|
||||||
|
|
||||||
print(get_coercions_to_sort(env, Const("abelian_ring", {1})):head())
|
|
||||||
assert(env:type_check(get_coercions_to_sort(env, Const("abelian_ring", {1})):head()))
|
|
||||||
print("Coercions (abelian ring): ")
|
|
||||||
cs = get_coercions_from(env, ab_ring)
|
|
||||||
for i = 1, #cs do
|
|
||||||
print(tostring(cs[i][2]) .. " : " .. tostring(cs[i][4]) .. " : " .. tostring(cs[i][3]))
|
|
||||||
end
|
|
||||||
|
|
@ -1,68 +0,0 @@
|
||||||
local env = environment()
|
|
||||||
local l = param_univ("l")
|
|
||||||
local nat = Const("nat")
|
|
||||||
local real = Const("real")
|
|
||||||
local one = Const("one")
|
|
||||||
local Ul = mk_sort(l)
|
|
||||||
local lst_l = Const("lst", {l})
|
|
||||||
local vec_l = Const("vec", {l})
|
|
||||||
local mat_l = Const("mat", {l})
|
|
||||||
local A = Local("A", Ul)
|
|
||||||
local n = Local("n", nat)
|
|
||||||
local ll = Local("ll", lst_l(A))
|
|
||||||
local len_l = Const("len", {l})
|
|
||||||
local lst_1 = Const("lst", {1})
|
|
||||||
local l1 = param_univ("l1")
|
|
||||||
local l2 = param_univ("l2")
|
|
||||||
local m = Local("m", nat)
|
|
||||||
env = add_decl(env, mk_constant_assumption("nat", Type))
|
|
||||||
env = add_decl(env, mk_constant_assumption("real", Type))
|
|
||||||
env = add_decl(env, mk_constant_assumption("one", nat))
|
|
||||||
env = add_decl(env, mk_constant_assumption("lst", {l}, mk_arrow(Ul, Ul)))
|
|
||||||
env = add_decl(env, mk_constant_assumption("len", {l}, Pi(A, mk_arrow(lst_l(A), nat))))
|
|
||||||
env = add_decl(env, mk_constant_assumption("vec", {l}, mk_arrow(Ul, nat, Ul)))
|
|
||||||
env = add_decl(env, mk_constant_assumption("mat", {l}, mk_arrow(Ul, nat, nat, Ul)))
|
|
||||||
env = add_decl(env, mk_constant_assumption("dlst", {l1, l2}, mk_arrow(mk_sort(l1), mk_sort(l2), mk_sort(max_univ(l1, l2)))))
|
|
||||||
env = add_decl(env, mk_constant_assumption("vec2lst", {l}, Pi(A, n, mk_arrow(vec_l(A, n), lst_l(A)))))
|
|
||||||
env = add_decl(env, mk_constant_assumption("lst2vec", {l}, Pi(A, ll, vec_l(A, len_l(A, ll)))))
|
|
||||||
env = add_decl(env, mk_constant_assumption("vec2mat", {l}, Pi(A, n, mk_arrow(vec_l(A, n), mat_l(A, n, one)))))
|
|
||||||
env = add_decl(env, mk_constant_assumption("mat2dlst", {l}, Pi(A, n, m, mk_arrow(mat_l(A, n, m), Const("dlst", {l, 1})(A, nat)))))
|
|
||||||
env = add_decl(env, mk_constant_assumption("nat2lst", mk_arrow(nat, lst_1(nat))))
|
|
||||||
env = add_coercion(env, "lst2vec")
|
|
||||||
env = push_scope(env, "tst")
|
|
||||||
local lst_nat = lst_1(nat)
|
|
||||||
print(get_coercions(env, lst_nat, "vec"):head())
|
|
||||||
env = add_coercion(env, "vec2mat")
|
|
||||||
print(get_coercions(env, lst_nat, "mat"):head())
|
|
||||||
assert(env:type_check(get_coercions(env, lst_nat, "mat"):head()))
|
|
||||||
function get_num_coercions(env)
|
|
||||||
local r = 0
|
|
||||||
for_each_coercion_user(env, function(C, D, f) r = r + 1 end)
|
|
||||||
return r
|
|
||||||
end
|
|
||||||
for_each_coercion_user(env, function(C, D, f) print(tostring(C) .. " >-> " .. tostring(D) .. " : " .. tostring(f)) end)
|
|
||||||
assert(get_num_coercions(env) == 3)
|
|
||||||
env = pop_scope(env, "tst")
|
|
||||||
print("---------")
|
|
||||||
for_each_coercion_user(env, function(C, D, f) print(tostring(C) .. " >-> " .. tostring(D) .. " : " .. tostring(f)) end)
|
|
||||||
assert(get_num_coercions(env) == 1)
|
|
||||||
print("---------")
|
|
||||||
env = push_scope(env)
|
|
||||||
env = using_namespace_objects(env, "tst")
|
|
||||||
for_each_coercion_user(env, function(C, D, f) print(tostring(C) .. " >-> " .. tostring(D) .. " : " .. tostring(f)) end)
|
|
||||||
assert(get_num_coercions(env) == 3)
|
|
||||||
env = pop_scope(env)
|
|
||||||
print("---------")
|
|
||||||
for_each_coercion_user(env, function(C, D, f) print(tostring(C) .. " >-> " .. tostring(D) .. " : " .. tostring(f)) end)
|
|
||||||
assert(get_num_coercions(env) == 1)
|
|
||||||
print("---------")
|
|
||||||
env = push_scope(env, "tst")
|
|
||||||
for_each_coercion_user(env, function(C, D, f) print(tostring(C) .. " >-> " .. tostring(D) .. " : " .. tostring(f)) end)
|
|
||||||
assert(get_num_coercions(env) == 3)
|
|
||||||
print("---------")
|
|
||||||
env = push_scope(env)
|
|
||||||
env = add_coercion(env, "nat2lst")
|
|
||||||
for_each_coercion_user(env, function(C, D, f) print(tostring(C) .. " >-> " .. tostring(D) .. " : " .. tostring(f)) end)
|
|
||||||
assert(get_num_coercions(env) == 6)
|
|
||||||
print("---------")
|
|
||||||
env = pop_scope(env)
|
|
||||||
Loading…
Reference in a new issue