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

feat(frontends/lean/definition_cmds): allow meta recursive definitions without recursive equations

Browse source
This commit is contained in:
Leonardo de Moura 2017-02-04 13:44:05 -08:00
parent 160011b80e
commit b28ed2453e
5 changed files with 19 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/init/meta/converter.lean
View file

@ -80,7 +80,7 @@ meta instance : alternative conv :=
orelse := @conv.orelse }
meta def whnf_core (m : transparency) : conv unit :=
λ r e, do n ← whnf_core m e, return ⟨(), n, none⟩
λ r e, do n ← tactic.whnf_core m e, return ⟨(), n, none⟩
meta def whnf : conv unit :=
conv.whnf_core reducible

2
library/init/meta/tactic.lean
View file

@ -211,7 +211,7 @@ do fmt ← pp a,
return $ _root_.trace_fmt fmt (λ u, ())
meta def trace_call_stack : tactic unit :=
take state, trace_call_stack (success () state)
take state, _root_.trace_call_stack (success () state)
meta def trace_state : tactic unit :=
do s ← read,

2
library/tools/super/prover.lean
View file

@ -120,6 +120,6 @@ meta def super (extra_clause_names : types.raw_ident_list)
(extra_lemma_names : types.with_ident_list) : tactic unit := do
with_lemmas extra_clause_names,
extra_lemmas ← monad.for extra_lemma_names mk_const,
super extra_lemmas
_root_.super extra_lemmas
end tactic.interactive

2
library/tools/super/prover_state.lean
View file

@ -145,7 +145,7 @@ meta instance (α : Type) : has_coe (tactic α) (prover α) :=
⟨monad.monad_lift⟩
meta def fail {α β : Type} [has_to_format β] (msg : β) : prover α :=
fail msg
tactic.fail msg
meta def orelse (A : Type) (p1 p2 : prover A) : prover A :=
take state, p1 state <|> p2 state

18
src/frontends/lean/definition_cmds.cpp
View file

@ -170,7 +170,7 @@ environment mutual_definition_cmd_core(parser & p, def_cmd_kind kind, decl_modif
}
static expr_pair parse_definition(parser & p, buffer<name> & lp_names, buffer<expr> & params,
bool is_example, bool is_instance) {
bool is_example, bool is_instance, bool is_meta) {
parser::local_scope scope1(p);
auto header_pos = p.pos();
bool allow_default = true;
@ -179,7 +179,19 @@ static expr_pair parse_definition(parser & p, buffer<name> & lp_names, buffer<ex
expr val;
if (p.curr_is_token(get_assign_tk())) {
p.next();
val = p.parse_expr();
if (is_meta) {
declaration_name_scope scope2("_main");
fn = mk_local(mlocal_name(fn), local_pp_name(fn), mlocal_type(fn), mk_rec_info(true));
p.add_local(fn);
val = p.parse_expr();
/* add fake equation */
expr eqn = mk_equation(fn, val);
buffer<expr> eqns;
eqns.push_back(eqn);
val = mk_equations(p, fn, scope2.get_name(), eqns, {}, header_pos);
} else {
val = p.parse_expr();
}
} else if (p.curr_is_token(get_bar_tk()) || p.curr_is_token(get_period_tk())) {
declaration_name_scope scope2("_main");
fn = mk_local(mlocal_name(fn), local_pp_name(fn), mlocal_type(fn), mk_rec_info(true));
@ -772,7 +784,7 @@ environment single_definition_cmd_core(parser & p, def_cmd_kind kind, decl_modif
bool is_rfl = false;
if (is_instance)
attrs.set_attribute(p.env(), "instance");
std::tie(fn, val) = parse_definition(p, lp_names, params, is_example, is_instance);
std::tie(fn, val) = parse_definition(p, lp_names, params, is_example, is_instance, modifiers.m_is_meta);
p.declare_sorry_if_used();
// skip elaboration of definitions during reparsing