From cb248bddb5940e0d86d8ffdbe6b2313ae8c76b2c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 28 Sep 2016 21:56:11 -0700 Subject: [PATCH] feat(library/init/meta/interactive): improve rewrite tactic interface in "interactive" mode --- library/init/meta/interactive.lean | 22 ++++++++++++++++++++-- 1 file changed, 20 insertions(+), 2 deletions(-) diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean index 6d258a74ba..15225333e5 100644 --- a/library/init/meta/interactive.lean +++ b/library/init/meta/interactive.lean @@ -109,12 +109,30 @@ match pexpr.to_raw_expr p with | _ := none end +private meta def resolve_name (n : name) : tactic expr := +get_local n +<|> +mk_const n +<|> +fail ("failed to resolve name '" ++ to_string n ++ "'") + +/- Version of to_expr that tries to bypass the elaborator if `p` is just a constant or local constant. + This is not an optimization, by skipping the elaborator we make sure that unwanted resolution is used. + Example: the elaborator will force any unassigned ?A that must have be an instance of (has_one ?A) to nat. + Remark: another benefit is that auxiliary temporary metavariables do not appear in error messages. -/ +private meta def to_expr' (p : pexpr) : tactic expr := +match pexpr.to_raw_expr p with +| (const c []) := resolve_name c +| (local_const c _ _ _) := resolve_name c +| _ := to_expr p +end + private meta def to_symm_expr_list : list pexpr → tactic (list (bool × expr)) | [] := return [] | (p::ps) := match is_neg p with - | some a := do r ← to_expr a, rs ← to_symm_expr_list ps, return ((tt, r) :: rs) - | none := do r ← to_expr p, rs ← to_symm_expr_list ps, return ((ff, r) :: rs) + | some a := do r ← to_expr' a, rs ← to_symm_expr_list ps, return ((tt, r) :: rs) + | none := do r ← to_expr' p, rs ← to_symm_expr_list ps, return ((ff, r) :: rs) end private meta def rw_goal : list (bool × expr) → tactic unit