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

chore(library/equations_compiler/compiler): generate error when using well founded recursion in meta definitions

Browse source
This commit is contained in:
Leonardo de Moura 2017-05-17 12:24:47 -07:00
parent 75786e9a6e
commit dea8a856dc
3 changed files with 22 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/library/equations_compiler/compiler.cpp
View file

@ -31,11 +31,16 @@ static expr compile_equations_core(environment & env, options const & opts,
expr const & eqns) {
type_context ctx(env, opts, mctx, lctx, transparency_mode::Semireducible);
trace_compiler(tout() << "compiling\n" << eqns << "\n";);
trace_compiler(tout() << "recursive: " << is_recursive_eqns(ctx, eqns) << "\n";);
trace_compiler(tout() << "nested recursion: " << has_nested_rec(eqns) << "\n";);
trace_compiler(tout() << "recursive: " << is_recursive_eqns(ctx, eqns) << "\n";);
trace_compiler(tout() << "nested recursion: " << has_nested_rec(eqns) << "\n";);
trace_compiler(tout() << "using_well_founded: " << is_wf_equations(eqns) << "\n";);
equations_header const & header = get_equations_header(eqns);
lean_assert(header.m_is_meta || !has_nested_rec(eqns));
if (header.m_is_meta) {
if (is_wf_equations(eqns)) {
throw exception("invalid use of 'using_well_founded', we do not need to use well founded recursion for meta definitions, since they can use unbounded recursion");
}
return mk_equations_result(unbounded_rec(env, opts, mctx, lctx, eqns));
}

14
tests/lean/meta_wf_error.lean Normal file
View file

@ -0,0 +1,14 @@
def R : (Σ _ : nat, nat) → (Σ _ : nat, nat) → Prop :=
sigma.lex nat.lt (λ _, empty_relation)
def Rwf : well_founded R :=
sigma.lex_wf nat.lt_wf (λ _, empty_wf)
meta def Div : nat → nat → nat
| x y :=
if h : 0 < y ∧ y ≤ x
then
have x - y < x, from nat.sub_lt (nat.lt_of_lt_of_le h.left h.right) h.left,
Div (x - y) y + 1
else 0
using_well_founded R Rwf

1
tests/lean/meta_wf_error.lean.expected.out Normal file
View file

@ -0,0 +1 @@
meta_wf_error.lean:7:9: error: invalid use of 'using_well_founded', we do not need to use well founded recursion for meta definitions, since they can use unbounded recursion