max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(kernel/declaration): untrusted constant declarations

Browse source 
This feature is useful for implementing the new tactic framework
This commit is contained in:
Leonardo de Moura 2016-04-28 15:16:24 -07:00
parent 54f68226f4
commit 7932872487
2 changed files with 7 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/kernel/declaration.cpp
View file

@ -31,9 +31,9 @@ struct declaration::cell {
bool m_trusted;
void dealloc() { delete this; }
cell(name const & n, level_param_names const & params, expr const & t, bool is_axiom):
cell(name const & n, level_param_names const & params, expr const & t, bool is_axiom, bool trusted):
m_rc(1), m_name(n), m_params(params), m_type(t), m_theorem(is_axiom),
m_height(0), m_use_conv_opt(false), m_trusted(true) {}
m_height(0), m_use_conv_opt(false), m_trusted(trusted) {}
cell(name const & n, level_param_names const & params, expr const & t, bool is_thm, expr const & v,
unsigned h, bool use_conv_opt, bool trusted):
m_rc(1), m_name(n), m_params(params), m_type(t), m_theorem(is_thm),
@ -96,10 +96,10 @@ declaration mk_theorem(name const & n, level_param_names const & params, expr co
return declaration(new declaration::cell(n, params, t, true, v, height, true, true));
}
declaration mk_axiom(name const & n, level_param_names const & params, expr const & t) {
return declaration(new declaration::cell(n, params, t, true));
return declaration(new declaration::cell(n, params, t, true, true));
}
declaration mk_constant_assumption(name const & n, level_param_names const & params, expr const & t) {
return declaration(new declaration::cell(n, params, t, false));
declaration mk_constant_assumption(name const & n, level_param_names const & params, expr const & t, bool trusted) {
return declaration(new declaration::cell(n, params, t, false, trusted));
}
void initialize_declaration() {

4
src/kernel/declaration.h
View file

@ -63,7 +63,7 @@ public:
friend declaration mk_theorem(environment const &, name const &, level_param_names const &, expr const &, expr const &);
friend declaration mk_theorem(name const &, level_param_names const &, expr const &, expr const &, unsigned);
friend declaration mk_axiom(name const & n, level_param_names const & params, expr const & t);
friend declaration mk_constant_assumption(name const & n, level_param_names const & params, expr const & t);
friend declaration mk_constant_assumption(name const & n, level_param_names const & params, expr const & t, bool trusted);
};
inline optional<declaration> none_declaration() { return optional<declaration>(); }
@ -77,7 +77,7 @@ declaration mk_definition(environment const & env, name const & n, level_param_n
declaration mk_theorem(environment const & env, name const & n, level_param_names const & params, expr const & t, expr const & v);
declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v, unsigned w);
declaration mk_axiom(name const & n, level_param_names const & params, expr const & t);
declaration mk_constant_assumption(name const & n, level_param_names const & params, expr const & t);
declaration mk_constant_assumption(name const & n, level_param_names const & params, expr const & t, bool trusted = false);
void initialize_declaration();
void finalize_declaration();