michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/kernel_bindings): add hott_environment Lua API

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-21 11:49:30 -07:00
parent 45d473d44e
commit 9f4bae6856
2 changed files with 50 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/library/kernel_bindings.cpp
View file

@ -21,6 +21,7 @@ Author: Leonardo de Moura
#include "kernel/type_checker.h"
#include "kernel/inductive/inductive.h"
#include "kernel/standard/standard.h"
#include "kernel/hott/hott.h"
#include "library/occurs.h"
#include "library/io_state_stream.h"
#include "library/expr_lt.h"
@ -1115,12 +1116,14 @@ static int mk_bare_environment(lua_State * L) {
list<name> const & cls_proof_irrel = get_list_name_named_param(L, 1, "cls_proof_irrel", list<name>());
return push_environment(L, environment(trust_lvl, prop_proof_irrel, eta, impredicative, cls_proof_irrel));
}
static int mk_environment(lua_State * L) {
static unsigned get_trust_lvl(lua_State * L, int i) {
unsigned trust_lvl = 0;
if (lua_gettop(L) > 0)
trust_lvl = lua_tonumber(L, 1);
return push_environment(L, mk_environment(trust_lvl));
if (i <= lua_gettop(L))
trust_lvl = lua_tonumber(L, 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_expr(L, type_checker(to_environment(L, 1)).whnf(to_expr(L, 2))); }
@ -1208,6 +1211,7 @@ 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");

42
tests/lua/env10.lua Normal file
View file

@ -0,0 +1,42 @@
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(function(d)
print(tostring(d:name()) .. " : " .. tostring(d:type()))
end
)