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

feat(frontends/lean/structure_cmd): add 'private' modifier for parent structures

Browse source 
When it is used coercions/instances to parent structure are to registered
This commit is contained in:
Leonardo de Moura 2014-11-03 23:15:15 -08:00
parent b24165dc7b
commit b6722a5d33
4 changed files with 32 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
src/frontends/lean/structure_cmd.cpp
View file

@ -72,6 +72,7 @@ struct structure_cmd_fn {
buffer<expr> m_params;
expr m_type;
buffer<expr> m_parents;
buffer<bool> m_private_parents;
name m_mk;
pos_info m_mk_pos;
implicit_infer_kind m_mk_infer;
@ -153,8 +154,14 @@ struct structure_cmd_fn {
m_p.next();
while (true) {
auto pos = m_p.pos();
bool is_private_parent = false;
if (m_p.curr_is_token(get_private_tk())) {
m_p.next();
is_private_parent = true;
}
expr parent = m_p.parse_expr();
m_parents.push_back(parent);
m_private_parents.push_back(is_private_parent);
check_parent(parent, pos);
name const & parent_name = const_name(get_app_fn(parent));
auto parent_info = get_parent_info(parent_name);
@ -656,10 +663,12 @@ struct structure_cmd_fn {
m_env = set_reducible(m_env, coercion_name, reducible_status::On);
save_def_info(coercion_name);
add_alias(coercion_name);
m_env = add_coercion(m_env, coercion_name, m_p.ios());
if (m_modifiers.is_class() && is_class(m_env, parent_name)) {
// if both are classes, then we also mark coercion_name as an instance
m_env = add_instance(m_env, coercion_name);
if (!m_private_parents[i]) {
m_env = add_coercion(m_env, coercion_name, m_p.ios());
if (m_modifiers.is_class() && is_class(m_env, parent_name)) {
// if both are classes, then we also mark coercion_name as an instance
m_env = add_instance(m_env, coercion_name);
}
}
}
}

4
src/frontends/lean/tokens.cpp
View file

@ -62,6 +62,7 @@ static name * g_proof = nullptr;
static name * g_qed = nullptr;
static name * g_begin = nullptr;
static name * g_end = nullptr;
static name * g_private = nullptr;
static name * g_definition = nullptr;
static name * g_theorem = nullptr;
static name * g_axiom = nullptr;
@ -147,6 +148,7 @@ void initialize_tokens() {
g_qed = new name("qed");
g_begin = new name("begin");
g_end = new name("end");
g_private = new name("private");
g_definition = new name("definition");
g_theorem = new name("theorem");
g_opaque = new name("opaque");
@ -195,6 +197,7 @@ void finalize_tokens() {
delete g_call;
delete g_with;
delete g_class;
delete g_private;
delete g_definition;
delete g_theorem;
delete g_opaque;
@ -318,6 +321,7 @@ name const & get_proof_tk() { return *g_proof; }
name const & get_qed_tk() { return *g_qed; }
name const & get_begin_tk() { return *g_begin; }
name const & get_end_tk() { return *g_end; }
name const & get_private_tk() { return *g_private; }
name const & get_definition_tk() { return *g_definition; }
name const & get_theorem_tk() { return *g_theorem; }
name const & get_axiom_tk() { return *g_axiom; }

1
src/frontends/lean/tokens.h
View file

@ -64,6 +64,7 @@ name const & get_proof_tk();
name const & get_begin_tk();
name const & get_qed_tk();
name const & get_end_tk();
name const & get_private_tk();
name const & get_definition_tk();
name const & get_theorem_tk();
name const & get_axiom_tk();

14
tests/lean/run/record6.lean Normal file
View file

@ -0,0 +1,14 @@
import logic data.unit
structure point (A : Type) (B : Type) :=
mk :: (x : A) (y : B)
structure point2 (A : Type) (B : Type) extends point A B :=
make
structure point3 extends point num num, private point2 num num renaming x→y y→z
check point3.mk
theorem tst : point3.mk 1 2 3 = point.mk 1 2 :=
rfl