feat(kernel/inductive): add datatype and introduction rules declarations to environment, and fix tests
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
f7bc5ac514
commit
d03e35aaac
3 changed files with 46 additions and 32 deletions
|
@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
||||||
|
|
||||||
Author: Leonardo de Moura
|
Author: Leonardo de Moura
|
||||||
*/
|
*/
|
||||||
|
#include "kernel/type_checker.h"
|
||||||
#include "kernel/inductive/inductive.h"
|
#include "kernel/inductive/inductive.h"
|
||||||
|
|
||||||
namespace lean {
|
namespace lean {
|
||||||
|
@ -13,7 +14,7 @@ environment add_inductive(environment const & env, name const & ind_name, level_
|
||||||
return add_inductive(env, level_params, num_params, list<inductive_decl>(inductive_decl(ind_name, type, intro_rules)));
|
return add_inductive(env, level_params, num_params, list<inductive_decl>(inductive_decl(ind_name, type, intro_rules)));
|
||||||
}
|
}
|
||||||
|
|
||||||
environment add_inductive(environment const & env,
|
environment add_inductive(environment env,
|
||||||
level_param_names const & level_params,
|
level_param_names const & level_params,
|
||||||
unsigned num_params,
|
unsigned num_params,
|
||||||
list<inductive_decl> const & decls) {
|
list<inductive_decl> const & decls) {
|
||||||
|
@ -31,6 +32,14 @@ environment add_inductive(environment const & env,
|
||||||
std::cout << " " << intro_rule_name(ir) << " : " << intro_rule_type(ir) << "\n";
|
std::cout << " " << intro_rule_name(ir) << " : " << intro_rule_type(ir) << "\n";
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
// Add all datatype declarations to environment
|
||||||
|
for (auto d : decls)
|
||||||
|
env = env.add(check(env, mk_var_decl(inductive_decl_name(d), level_params, inductive_decl_type(d))));
|
||||||
|
// Add all introduction rules (aka constructors) to environment
|
||||||
|
for (auto d : decls) {
|
||||||
|
for (auto ir : inductive_decl_intros(d))
|
||||||
|
env = env.add(check(env, mk_var_decl(intro_rule_name(ir), level_params, intro_rule_type(ir))));
|
||||||
|
}
|
||||||
return env;
|
return env;
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
|
@ -33,7 +33,7 @@ inline expr const & inductive_decl_type(inductive_decl const & d) { return std::
|
||||||
inline list<intro_rule> const & inductive_decl_intros(inductive_decl const & d) { return std::get<2>(d); }
|
inline list<intro_rule> const & inductive_decl_intros(inductive_decl const & d) { return std::get<2>(d); }
|
||||||
|
|
||||||
/** \brief Declare a finite set of mutually dependent inductive datatypes. */
|
/** \brief Declare a finite set of mutually dependent inductive datatypes. */
|
||||||
environment add_inductive(environment const & env,
|
environment add_inductive(environment env,
|
||||||
level_param_names const & level_params,
|
level_param_names const & level_params,
|
||||||
unsigned num_params,
|
unsigned num_params,
|
||||||
list<inductive_decl> const & decls);
|
list<inductive_decl> const & decls);
|
||||||
|
|
|
@ -4,47 +4,52 @@ local A = Const("A")
|
||||||
local U_l = mk_sort(l)
|
local U_l = mk_sort(l)
|
||||||
local U_l1 = mk_sort(mk_level_max(l, mk_level_one()))
|
local U_l1 = mk_sort(mk_level_max(l, mk_level_one()))
|
||||||
local list_l = Const("list", {l})
|
local list_l = Const("list", {l})
|
||||||
local Nat = Const("Nat")
|
local Nat = Const("nat")
|
||||||
local vec_l = Const("vec", {l})
|
local vec_l = Const("vec", {l})
|
||||||
local zero = Const("zero")
|
local zero = Const("zero")
|
||||||
local succ = Const("succ")
|
local succ = Const("succ")
|
||||||
local forest_l = Const("forest", {l})
|
local forest_l = Const("forest", {l})
|
||||||
local tree_l = Const("tree", {l})
|
local tree_l = Const("tree", {l})
|
||||||
local n = Const("n")
|
local n = Const("n")
|
||||||
add_inductive(env, "nat", Type, "zero", Nat, "succ", mk_arrow(Nat, Nat))
|
env = add_inductive(env, "nat", Type, "zero", Nat, "succ", mk_arrow(Nat, Nat))
|
||||||
add_inductive(env,
|
env = add_inductive(env,
|
||||||
"list", {l}, 1, mk_arrow(U_l, U_l1),
|
"list", {l}, 1, mk_arrow(U_l, U_l1),
|
||||||
"nil", Pi({{A, U_l, true}}, list_l(A)),
|
"nil", Pi({{A, U_l, true}}, list_l(A)),
|
||||||
"cons", Pi({{A, U_l, true}}, mk_arrow(A, list_l(A), list_l(A))))
|
"cons", Pi({{A, U_l, true}}, mk_arrow(A, list_l(A), list_l(A))))
|
||||||
add_inductive(env,
|
env = add_inductive(env,
|
||||||
"vec", {l}, 1,
|
"vec", {l}, 1,
|
||||||
mk_arrow(U_l, Nat, U_l1),
|
mk_arrow(U_l, Nat, U_l1),
|
||||||
"vnil", Pi({{A, U_l, true}}, vec_l(A, zero)),
|
"vnil", Pi({{A, U_l, true}}, vec_l(A, zero)),
|
||||||
"vcons", Pi({{A, U_l, true}, {n, Nat, true}}, mk_arrow(A, vec_l(A, n), vec_l(A, succ(n)))))
|
"vcons", Pi({{A, U_l, true}, {n, Nat, true}}, mk_arrow(A, vec_l(A, n), vec_l(A, succ(n)))))
|
||||||
|
|
||||||
local And = Const("and")
|
local And = Const("and")
|
||||||
local Or = Const("or")
|
local Or = Const("or")
|
||||||
local B = Const("B")
|
local B = Const("B")
|
||||||
add_inductive(env, "false", Bool)
|
env = add_inductive(env, "false", Bool)
|
||||||
add_inductive(env, "true", Bool, "trivial", Const("true"))
|
env = add_inductive(env, "true", Bool, "trivial", Const("true"))
|
||||||
add_inductive(env,
|
env = add_inductive(env,
|
||||||
"and", mk_arrow(Bool, Bool, Bool),
|
"and", mk_arrow(Bool, Bool, Bool),
|
||||||
"and_intro", Pi({{A, Bool, true}, {B, Bool, true}}, mk_arrow(A, B, And(A, B))))
|
"and_intro", Pi({{A, Bool, true}, {B, Bool, true}}, mk_arrow(A, B, And(A, B))))
|
||||||
add_inductive(env,
|
env = add_inductive(env,
|
||||||
"or", mk_arrow(Bool, Bool, Bool),
|
"or", mk_arrow(Bool, Bool, Bool),
|
||||||
"or_intro_left", Pi({{A, Bool, true}, {B, Bool, true}}, mk_arrow(A, Or(A, B))),
|
"or_intro_left", Pi({{A, Bool, true}, {B, Bool, true}}, mk_arrow(A, Or(A, B))),
|
||||||
"or_intro_right", Pi({{A, Bool, true}, {B, Bool, true}}, mk_arrow(B, Or(A, B))))
|
"or_intro_right", Pi({{A, Bool, true}, {B, Bool, true}}, mk_arrow(B, Or(A, B))))
|
||||||
local P = Const("P")
|
local P = Const("P")
|
||||||
local a = Const("a")
|
local a = Const("a")
|
||||||
local exists_l = Const("exists", {l})
|
local exists_l = Const("exists", {l})
|
||||||
add_inductive(env,
|
env = add_inductive(env,
|
||||||
"exists", {l}, 2, Pi({{A, U_l}}, mk_arrow(mk_arrow(A, Bool), Bool)),
|
"exists", {l}, 2, Pi({{A, U_l}}, mk_arrow(mk_arrow(A, Bool), Bool)),
|
||||||
"exists_intro", Pi({{A, U_l, true}, {P, mk_arrow(A, Bool), true}, {a, A}}, mk_arrow(P(a), exists_l(A, P))))
|
"exists_intro", Pi({{A, U_l, true}, {P, mk_arrow(A, Bool), true}, {a, A}}, mk_arrow(P(a), exists_l(A, P))))
|
||||||
|
|
||||||
add_inductive(env, {l}, 1,
|
env = add_inductive(env, {l}, 1,
|
||||||
{"tree", mk_arrow(U_l, U_l1),
|
{"tree", mk_arrow(U_l, U_l1),
|
||||||
"node", Pi({{A, U_l, true}}, mk_arrow(A, forest_l(A), tree_l(A)))
|
"node", Pi({{A, U_l, true}}, mk_arrow(A, forest_l(A), tree_l(A)))
|
||||||
},
|
},
|
||||||
{"forest", mk_arrow(U_l, U_l1),
|
{"forest", mk_arrow(U_l, U_l1),
|
||||||
"emptyf", Pi({{A, U_l, true}}, forest_l(A)),
|
"emptyf", Pi({{A, U_l, true}}, forest_l(A)),
|
||||||
"consf", Pi({{A, U_l, true}}, mk_arrow(tree_l(A), forest_l(A), forest_l(A)))})
|
"consf", Pi({{A, U_l, true}}, mk_arrow(tree_l(A), forest_l(A), forest_l(A)))})
|
||||||
|
|
||||||
|
local tc = type_checker(env)
|
||||||
|
print(tc:check(Const("forest", {mk_level_zero()})))
|
||||||
|
print(tc:check(Const("vcons", {mk_level_zero()})))
|
||||||
|
print(tc:check(Const("consf", {mk_level_zero()})))
|
||||||
|
|
Loading…
Reference in a new issue