From 5df705ebe89fa8e9258a5837b138fc1de0a6d663 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 18 Sep 2016 17:20:52 -0700 Subject: [PATCH] fix(library/equations_compiler/compiler): nested match-exprs in meta_definitions --- src/library/equations_compiler/compiler.cpp | 7 +- tests/lean/run/assoc_flat.lean | 75 +++++++++++---------- 2 files changed, 43 insertions(+), 39 deletions(-) diff --git a/src/library/equations_compiler/compiler.cpp b/src/library/equations_compiler/compiler.cpp index d3216572b4..8a0184e2fd 100644 --- a/src/library/equations_compiler/compiler.cpp +++ b/src/library/equations_compiler/compiler.cpp @@ -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)) { diff --git a/tests/lean/run/assoc_flat.lean b/tests/lean/run/assoc_flat.lean index cc6245b1a2..144333ee74 100644 --- a/tests/lean/run/assoc_flat.lean +++ b/tests/lean/run/assoc_flat.lean @@ -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