From b9424975b398daa638e90a1094de02c6945a32dc Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 17 Feb 2017 22:02:05 +0100 Subject: [PATCH] refactor(init/meta): replace dynamically-checked quotes where possible --- library/init/data/sigma/lex.lean | 15 +++++++-------- library/init/meta/comp_value_tactics.lean | 2 +- library/init/meta/interactive.lean | 6 +++--- library/init/meta/mk_dec_eq_instance.lean | 2 +- library/init/meta/simp_tactic.lean | 4 ++-- library/init/meta/smt/ematch.lean | 12 ++++++------ library/init/meta/smt/interactive.lean | 4 ++-- library/init/meta/tactic.lean | 6 +++--- library/tools/super/datatypes.lean | 2 +- src/frontends/lean/builtin_exprs.cpp | 6 +----- src/frontends/lean/parser.cpp | 12 +++++++++--- 11 files changed, 36 insertions(+), 35 deletions(-) diff --git a/library/init/data/sigma/lex.lean b/library/init/data/sigma/lex.lean index edf95f56ed..b01ac062f5 100644 --- a/library/init/data/sigma/lex.lean +++ b/library/init/data/sigma/lex.lean @@ -36,15 +36,14 @@ section @sigma.lex.rec_on α β r s (λ p₁ p₂, p₂.1 = xa → p₂.2 == xb → acc (lex r s) p₁) p (sigma.mk xa xb) lt (λ (a₁ : α) (b₁ : β a₁) (a₂ : α) (b₂ : β a₂) (h : r a₁ a₂) (eq₂ : a₂ = xa) (eq₃ : b₂ == xb), - by do - get_local `eq₂ >>= subst, - to_expr `(iha a₁ h b₁) >>= exact) + begin subst eq₂, exact iha a₁ h b₁ end) (λ (a : α) (b₁ b₂ : β a) (h : s a b₁ b₂) (eq₂ : a = xa) (eq₃ : b₂ == xb), - by do - get_local `eq₂ >>= subst, - to_expr `(eq_of_heq eq₃) >>= note `new_eq₃, - get_local `new_eq₃ >>= subst, - to_expr `(ihb b₁ h) >>= exact), + begin + subst eq₂, + note new_eq₃ := eq_of_heq eq₃, + subst new_eq₃, + exact ihb b₁ h + end), aux rfl (heq.refl xb)))) -- The lexicographical order of well founded relations is well-founded diff --git a/library/init/meta/comp_value_tactics.lean b/library/init/meta/comp_value_tactics.lean index 6c6e294b31..cd98b98c35 100644 --- a/library/init/meta/comp_value_tactics.lean +++ b/library/init/meta/comp_value_tactics.lean @@ -63,5 +63,5 @@ do t ← target, exact pr) <|> (do (a, b) ← is_eq t, - unify a b, to_expr `(eq.refl %%a) >>= exact) + unify a b, to_expr ``(eq.refl %%a) >>= exact) end tactic diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean index 4b6e589c8c..d0fcf26413 100644 --- a/library/init/meta/interactive.lean +++ b/library/init/meta/interactive.lean @@ -161,7 +161,7 @@ term of the goal. Let `T` be our goal, let `p` be a term of type `U` then -/ meta def exact (q : parse texpr) : tactic unit := do tgt : expr ← target, - i_to_expr_strict `(%%q : %%tgt) >>= tactic.exact + i_to_expr_strict ``(%%q : %%tgt) >>= tactic.exact private meta def get_locals : list name → tactic (list expr) | [] := return [] @@ -329,12 +329,12 @@ This tactic applies to any goal. `assertv h : T := p` adds a new hypothesis of n -/ meta def assertv (h : parse ident) (q₁ : parse $ tk ":" *> texpr) (q₂ : parse $ tk ":=" *> texpr) : tactic unit := do t ← i_to_expr_strict q₁, - v ← i_to_expr_strict `(%%q₂ : %%t), + v ← i_to_expr_strict ``(%%q₂ : %%t), tactic.assertv h t v meta def definev (h : parse ident) (q₁ : parse $ tk ":" *> texpr) (q₂ : parse $ tk ":=" *> texpr) : tactic unit := do t ← i_to_expr_strict q₁, - v ← i_to_expr_strict `(%%q₂ : %%t), + v ← i_to_expr_strict ``(%%q₂ : %%t), tactic.definev h t v meta def note (h : parse ident) (q : parse $ tk ":=" *> texpr) : tactic unit := diff --git a/library/init/meta/mk_dec_eq_instance.lean b/library/init/meta/mk_dec_eq_instance.lean index 3ad973c8fb..a61a3a363d 100644 --- a/library/init/meta/mk_dec_eq_instance.lean +++ b/library/init/meta/mk_dec_eq_instance.lean @@ -118,7 +118,7 @@ do env ← get_env, do { d1' ← whnf d1, (app I_basic_const I_idx) ← return d1', I_idx_type ← infer_type I_idx, - new_goal ← to_expr `(∀ (_idx : %%I_idx_type), decidable_eq (%%I_basic_const _idx)), + new_goal ← to_expr ``(∀ (_idx : %%I_idx_type), decidable_eq (%%I_basic_const _idx)), assert `_basic_dec_eq new_goal, swap, to_expr `(_basic_dec_eq %%I_idx) >>= exact, diff --git a/library/init/meta/simp_tactic.lean b/library/init/meta/simp_tactic.lean index 14641eea16..8371d082e3 100644 --- a/library/init/meta/simp_tactic.lean +++ b/library/init/meta/simp_tactic.lean @@ -332,9 +332,9 @@ meta def to_simp_lemmas : simp_lemmas → list name → tactic simp_lemmas | S (n::ns) := do S' ← S^.add_simp n, to_simp_lemmas S' ns meta def mk_simp_attr (attr_name : name) : command := -do t ← to_expr `(caching_user_attribute simp_lemmas), +do t ← to_expr ``(caching_user_attribute simp_lemmas), a ← attr_name^.to_expr, - v ← to_expr `({ name := %%a, + v ← to_expr ``({name := %%a, descr := "simplifier attribute", mk_cache := λ ns, do {tactic.to_simp_lemmas simp_lemmas.mk ns}, dependencies := [`reducibility] } : caching_user_attribute simp_lemmas), diff --git a/library/init/meta/smt/ematch.lean b/library/init/meta/smt/ematch.lean index f772d31ad6..1a3bf463db 100644 --- a/library/init/meta/smt/ematch.lean +++ b/library/init/meta/smt/ematch.lean @@ -79,10 +79,10 @@ meta def to_hinst_lemmas_core (m : transparency) (ignore_errors : bool) : bool end meta def mk_hinst_lemma_attr_core (attr_name : name) (as_simp : bool) : command := -do t ← to_expr `(caching_user_attribute hinst_lemmas), +do t ← to_expr ``(caching_user_attribute hinst_lemmas), a ← attr_name^.to_expr, - b ← if as_simp then to_expr `(tt) else to_expr `(ff), - v ← to_expr `({ name := %%a, + b ← if as_simp then to_expr ``(tt) else to_expr ``(ff), + v ← to_expr ``({name := %%a, descr := "hinst_lemma attribute", mk_cache := λ ns, to_hinst_lemmas_core reducible ff %%b ns hinst_lemmas.mk, dependencies := [`reducibility] } : caching_user_attribute hinst_lemmas), @@ -95,7 +95,7 @@ meta def mk_hinst_lemma_attrs_core (as_simp : bool) : list name → command (mk_hinst_lemma_attr_core n as_simp >> mk_hinst_lemma_attrs_core ns) <|> (do type ← infer_type (expr.const n []), - expected ← to_expr `(caching_user_attribute hinst_lemmas), + expected ← to_expr ``(caching_user_attribute hinst_lemmas), (is_def_eq type expected <|> fail ("failed to create hinst_lemma attribute '" ++ n^.to_string ++ "', declaration already exists and has different type.")), mk_hinst_lemma_attrs_core ns) @@ -117,11 +117,11 @@ For the ones in simp_attr_names, we use the left-hand-side of the conclusion as meta def mk_hinst_lemma_attr_set (attr_name : name) (attr_names : list name) (simp_attr_names : list name) : command := do mk_hinst_lemma_attrs_core ff attr_names, mk_hinst_lemma_attrs_core tt simp_attr_names, - t ← to_expr `(caching_user_attribute hinst_lemmas), + t ← to_expr ``(caching_user_attribute hinst_lemmas), a ← attr_name^.to_expr, l1 ← list_name.to_expr attr_names, l2 ← list_name.to_expr simp_attr_names, - v ← to_expr `({ name := %%a, + v ← to_expr ``({name := %%a, descr := "hinst_lemma attribute set", mk_cache := λ ns, let aux1 : list name := %%l1, diff --git a/library/init/meta/smt/interactive.lean b/library/init/meta/smt/interactive.lean index 88f907e931..b5c48d988c 100644 --- a/library/init/meta/smt/interactive.lean +++ b/library/init/meta/smt/interactive.lean @@ -94,12 +94,12 @@ do e ← tactic.to_expr_strict q, meta def assertv (h : parse ident) (q₁ : parse $ tk ":" *> texpr) (q₂ : parse $ tk ":=" *> texpr) : smt_tactic unit := do t ← tactic.to_expr_strict q₁, - v ← tactic.to_expr_strict `(%%q₂ : %%t), + v ← tactic.to_expr_strict ``(%%q₂ : %%t), smt_tactic.assertv h t v meta def definev (h : parse ident) (q₁ : parse $ tk ":" *> texpr) (q₂ : parse $ tk ":=" *> texpr) : smt_tactic unit := do t ← tactic.to_expr_strict q₁, - v ← tactic.to_expr_strict `(%%q₂ : %%t), + v ← tactic.to_expr_strict ``(%%q₂ : %%t), smt_tactic.definev h t v meta def note (h : parse ident) (q : parse $ tk ":=" *> texpr) : smt_tactic unit := diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean index 8ded8ff5df..39ad994dbe 100644 --- a/library/init/meta/tactic.lean +++ b/library/init/meta/tactic.lean @@ -869,7 +869,7 @@ else do meta def refine (e : pexpr) (report_errors := ff) : tactic unit := do tgt : expr ← target, - to_expr `(%%e : %%tgt) tt report_errors >>= exact + to_expr ``(%%e : %%tgt) tt report_errors >>= exact private meta def get_undeclared_const (env : environment) (base : name) : ℕ → name | i := let n := base <.> ("_aux_" ++ to_string i) in @@ -957,8 +957,8 @@ end list run_command do l ← return $ level.param `l, Ty ← return $ expr.sort l, - type ← to_expr `(Π (α : %%Ty), α → α), - val ← to_expr `(λ (α : %%Ty) (a : α), a), + type ← to_expr ``(Π (α : %%Ty), α → α), + val ← to_expr ``(λ (α : %%Ty) (a : α), a), add_decl (declaration.defn `id_locked [`l] type val reducibility_hints.opaque tt) lemma id_locked_eq {α : Type u} (a : α) : id_locked α a = a := diff --git a/library/tools/super/datatypes.lean b/library/tools/super/datatypes.lean index 6f551b7a0e..3e95c8945c 100644 --- a/library/tools/super/datatypes.lean +++ b/library/tools/super/datatypes.lean @@ -36,7 +36,7 @@ on_right_at' c i $ λhyp, pr ← mk_app (lhs^.get_app_fn^.const_name^.get_prefix <.> "no_confusion") [false_, lhs, rhs, hyp], -- FIXME: change to local false ^^ ty ← infer_type pr, ty ← whnf ty, - pr ← to_expr `(@eq.mpr _ %%ty rfl %%pr), -- FIXME + pr ← to_expr ``(@eq.mpr _ %%ty rfl %%pr), -- FIXME return [([], pr)] | _ := failed end diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 5bb373216c..6ddee08309 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -463,11 +463,7 @@ static expr fix_do_action_lhs(parser_state & p, expr const & lhs, expr const & t static std::tuple, expr, expr, optional> parse_do_action(parser_state & p, buffer & new_locals) { auto lhs_pos = p.pos(); - optional lhs; - if (p.in_quote()) - lhs = p.parse_expr(); - else - lhs = p.parse_pattern_or_expr(); + optional lhs = some(p.parse_pattern_or_expr()); expr type, curr; optional else_case; if (p.curr_is_token(get_colon_tk())) { diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 1035125115..4e6a0cc576 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -118,7 +118,8 @@ parser::quote_scope::quote_scope(parser & p, bool q, id_behavior i): m_p.m_in_quote = true; m_p.push_local_scope(false); m_p.m_quote_stack = cons(m_p.mk_parser_scope(), m_p.m_quote_stack); - m_p.clear_expr_locals(); + if (i != id_behavior::ErrorIfUndef) + m_p.clear_expr_locals(); } else if (!m_in_quote && m_old_in_quote) { lean_assert(m_p.m_quote_stack); m_p.m_id_behavior = id_behavior::ErrorIfUndef; @@ -1717,9 +1718,14 @@ expr parser::patexpr_to_pattern(expr const & pat_or_expr, bool skip_main_fn, buf } expr parser::parse_pattern_or_expr(unsigned rbp) { - all_id_local_scope scope(*this); flet set_in_pattern(m_in_pattern, true); - return parse_expr(rbp); + if (m_id_behavior != id_behavior::AssumeLocalIfNotLocal) { + all_id_local_scope scope(*this); + return parse_expr(rbp); + } else { + // keep AssumeLocalIfNotLocal in quotes + return parse_expr(rbp); + } } expr parser::parse_pattern(std::function const & fn, buffer & new_locals) {