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

fix(library/equations_compiler/compiler): nested match-exprs in meta_definitions

Browse source
This commit is contained in:
Leonardo de Moura 2016-09-18 17:20:52 -07:00
parent 98da86eac0
commit 5df705ebe8
2 changed files with 43 additions and 39 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -33,10 +33,11 @@ static expr compile_equations_core(environment & env, options const & opts,
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";);
lean_assert(!has_nested_rec(eqns));
equations_header const & header = get_equations_header(eqns);
if (header.m_is_meta)
return unbounded_rec(env, opts, mctx, lctx, eqns);
lean_assert(header.m_is_meta || !has_nested_rec(eqns));
if (header.m_is_meta) {
return mk_equations_result(unbounded_rec(env, opts, mctx, lctx, eqns));
}
if (header.m_num_fns == 1) {
if (!is_recursive_eqns(ctx, eqns)) {

75
tests/lean/run/assoc_flat.lean
View file

@ -1,3 +1,4 @@
set_option new_elaborator true
open tactic expr
constant nat.add_assoc (a b c : nat) : (a + b) + c = a + (b + c)
@ -8,43 +9,45 @@ match e with
| e := none
end
meta_definition flat_with (op : expr) (assoc : expr) (e : expr) (rhs : expr) : tactic (expr × expr) :=
match (is_op_app op e) with
| (some (a1, a2)) := do
-- H₁ is a proof for a2 + rhs = rhs₁
(rhs₁, H₁) ← flat_with op assoc a2 rhs,
-- H₂ is a proof for a1 + rhs₁ = rhs₂
(new_app, H₂) ← flat_with op assoc a1 rhs₁,
-- We need to generate a proof that (a1 + a2) + rhs = a1 + (a2 + rhs)
-- H₃ is a proof for (a1 + a2) + rhs = a1 + (a2 + rhs)
H₃ : expr ← return (app (app (app assoc a1) a2) rhs),
-- H₃ is a proof for a1 + (a2 + rhs) = a1 + rhs1
H₄ : expr ← mk_app `congr_arg [app op a1, H₁],
H₅ ← mk_app `eq.trans [H₃, H₄],
H ← mk_app `eq.trans [H₅, H₂],
return (new_app, H)
| none := do
new_app ← return $ app (app op e) rhs,
H ← mk_app `eq.refl [new_app],
return (new_app, H)
end
meta_definition flat_with : expr → expr → expr → expr → tactic (expr × expr)
| op assoc e rhs :=
match (is_op_app op e) with
| (some (a1, a2)) := do
-- H₁ is a proof for a2 + rhs = rhs₁
(rhs₁, H₁) ← flat_with op assoc a2 rhs,
-- H₂ is a proof for a1 + rhs₁ = rhs₂
(new_app, H₂) ← flat_with op assoc a1 rhs₁,
-- We need to generate a proof that (a1 + a2) + rhs = a1 + (a2 + rhs)
-- H₃ is a proof for (a1 + a2) + rhs = a1 + (a2 + rhs)
H₃ : expr ← return (app (app (app assoc a1) a2) rhs),
-- H₃ is a proof for a1 + (a2 + rhs) = a1 + rhs1
H₄ : expr ← mk_app `congr_arg [app op a1, H₁],
H₅ ← mk_app `eq.trans [H₃, H₄],
H ← mk_app `eq.trans [H₅, H₂],
return (new_app, H)
| none := do
new_app ← return $ app (app op e) rhs,
H ← mk_app `eq.refl [new_app],
return (new_app, H)
end
meta_definition flat (op : expr) (assoc : expr) (e : expr) : tactic (expr × expr) :=
match (is_op_app op e) with
| (some (a1, a2)) := do
-- H₁ is a proof that a2 = new_a2
(new_a2, H₁) ← flat op assoc a2,
-- H₂ is a proof that a1 + new_a2 = new_app
(new_app, H₂) ← flat_with op assoc a1 new_a2,
-- We need a proof that (a1 + a2) = new_app
-- H₃ is a proof for a1 + a2 = a1 + new_a2
H₃ : expr ← mk_app `congr_arg [app op a1, H₁],
H ← mk_app `eq.trans [H₃, H₂],
return (new_app, H)
| none :=
do pr ← mk_app `eq.refl [e],
return (e, pr)
end
meta_definition flat : expr → expr → expr → tactic (expr × expr)
| op assoc e :=
match (is_op_app op e) with
| (some (a1, a2)) := do
-- H₁ is a proof that a2 = new_a2
(new_a2, H₁) ← flat op assoc a2,
-- H₂ is a proof that a1 + new_a2 = new_app
(new_app, H₂) ← flat_with op assoc a1 new_a2,
-- We need a proof that (a1 + a2) = new_app
-- H₃ is a proof for a1 + a2 = a1 + new_a2
H₃ : expr ← mk_app `congr_arg [app op a1, H₁],
H ← mk_app `eq.trans [H₃, H₂],
return (new_app, H)
| none :=
do pr ← mk_app `eq.refl [e],
return (e, pr)
end
local infix `+` := nat.add
set_option trace.app_builder true