From 5b17c3cbd9100b95bc5602ab0e702ec2e180bd35 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sat, 22 Apr 2017 17:25:48 +0200 Subject: [PATCH] fix(frontends/lean/interactive): fall back to elaborator info when not an interactive tactic Fixes #1530 --- src/frontends/lean/interactive.cpp | 17 +++++++++-------- tests/lean/interactive/info_tactic.lean | 4 ++++ .../interactive/info_tactic.lean.expected.out | 11 ++++++----- 3 files changed, 19 insertions(+), 13 deletions(-) diff --git a/src/frontends/lean/interactive.cpp b/src/frontends/lean/interactive.cpp index 5fa9ffbd7f..a62148087c 100644 --- a/src/frontends/lean/interactive.cpp +++ b/src/frontends/lean/interactive.cpp @@ -122,15 +122,16 @@ void report_info(environment const & env, options const & opts, io_state const & if (auto it = get_option_declarations().find(tk)) record["doc"] = it->get_description(); break; - case break_at_pos_exception::token_context::interactive_tactic: - record = serialize_decl(e.m_token_info.m_token, - get_interactive_tactic_full_name(e.m_token_info.m_tac_class, e.m_token_info.m_token), - env, opts); - if (auto idx = e.m_token_info.m_tac_param_idx) - record["tactic_param_idx"] = *idx; - has_token_info = true; + case break_at_pos_exception::token_context::interactive_tactic: { + auto n = get_interactive_tactic_full_name(e.m_token_info.m_tac_class, e.m_token_info.m_token); + if (env.find(n)) { + record = serialize_decl(e.m_token_info.m_token, n, env, opts); + if (auto idx = e.m_token_info.m_tac_param_idx) + record["tactic_param_idx"] = *idx; + has_token_info = true; + } break; - case break_at_pos_exception::token_context::field: { + } case break_at_pos_exception::token_context::field: { auto name = e.m_token_info.m_struct + e.m_token_info.m_token; record["full-id"] = name.to_string(); add_source_info(env, name, record); diff --git a/tests/lean/interactive/info_tactic.lean b/tests/lean/interactive/info_tactic.lean index 0f9ac8603a..16fcb347ac 100644 --- a/tests/lean/interactive/info_tactic.lean +++ b/tests/lean/interactive/info_tactic.lean @@ -1,3 +1,5 @@ +open tactic + example : false := begin simp, @@ -8,4 +10,6 @@ begin --^ "command": "info" simp [d] , --^ "command": "info" + get_env +--^ "command": "info" end diff --git a/tests/lean/interactive/info_tactic.lean.expected.out b/tests/lean/interactive/info_tactic.lean.expected.out index 75c90549df..4b1c4bcbfb 100644 --- a/tests/lean/interactive/info_tactic.lean.expected.out +++ b/tests/lean/interactive/info_tactic.lean.expected.out @@ -1,6 +1,7 @@ -{"msgs":[{"caption":"","file_name":"f","pos_col":2,"pos_line":3,"severity":"error","text":"simplify tactic failed to simplify\nstate:\n⊢ false"}],"response":"all_messages"} +{"msgs":[{"caption":"","file_name":"f","pos_col":2,"pos_line":5,"severity":"error","text":"simplify tactic failed to simplify\nstate:\n⊢ false"}],"response":"all_messages"} {"message":"file invalidated","response":"ok","seq_num":0} -{"record":{"doc":"This tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses.\nIt has many variants.\n\n- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.\n\n- `simp [h_1, ..., h_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and the given `h_i`s.\n The `h_i`'s are terms. If a `h_i` is a definition `f`, then the equational lemmas associated with `f` are used.\n This is a convenient way to \"unfold\" `f`.\n\n- `simp without id_1 ... id_n` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`,\n but removes the ones named `id_i`s.\n\n- `simp at h` simplifies the non dependent hypothesis `h : T`. The tactic fails if the target or another hypothesis depends on `h`.\n\n- `simp with attr` simplifies the main goal target using the lemmas tagged with the attribute `[attr]`.","source":,"state":"⊢ false","tactic_params":["[expr, ...]?","(with id*)?","(without id*)?","(at id*)?","tactic.simp_config?"],"text":"simp","type":"interactive.parse interactive.types.opt_qexpr_list → interactive.parse interactive.types.with_ident_list → interactive.parse interactive.types.without_ident_list → interactive.parse interactive.types.location → opt_param tactic.simp_config {max_steps := tactic.simp_config.max_steps._default, contextual := tactic.simp_config.contextual._default, lift_eq := tactic.simp_config.lift_eq._default, canonize_instances := tactic.simp_config.canonize_instances._default, canonize_proofs := tactic.simp_config.canonize_proofs._default, use_axioms := tactic.simp_config.use_axioms._default, zeta := tactic.simp_config.zeta._default, beta := tactic.simp_config.beta._default, eta := tactic.simp_config.eta._default, proj := tactic.simp_config.proj._default} → tactic unit"},"response":"ok","seq_num":4} -{"record":{"doc":"This tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses.\nIt has many variants.\n\n- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.\n\n- `simp [h_1, ..., h_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and the given `h_i`s.\n The `h_i`'s are terms. If a `h_i` is a definition `f`, then the equational lemmas associated with `f` are used.\n This is a convenient way to \"unfold\" `f`.\n\n- `simp without id_1 ... id_n` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`,\n but removes the ones named `id_i`s.\n\n- `simp at h` simplifies the non dependent hypothesis `h : T`. The tactic fails if the target or another hypothesis depends on `h`.\n\n- `simp with attr` simplifies the main goal target using the lemmas tagged with the attribute `[attr]`.","source":,"tactic_param_idx":0,"tactic_params":["[expr, ...]?","(with id*)?","(without id*)?","(at id*)?","tactic.simp_config?"],"text":"simp","type":"interactive.parse interactive.types.opt_qexpr_list → interactive.parse interactive.types.with_ident_list → interactive.parse interactive.types.without_ident_list → interactive.parse interactive.types.location → opt_param tactic.simp_config {max_steps := tactic.simp_config.max_steps._default, contextual := tactic.simp_config.contextual._default, lift_eq := tactic.simp_config.lift_eq._default, canonize_instances := tactic.simp_config.canonize_instances._default, canonize_proofs := tactic.simp_config.canonize_proofs._default, use_axioms := tactic.simp_config.use_axioms._default, zeta := tactic.simp_config.zeta._default, beta := tactic.simp_config.beta._default, eta := tactic.simp_config.eta._default, proj := tactic.simp_config.proj._default} → tactic unit"},"response":"ok","seq_num":6} -{"record":{"doc":"This tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses.\nIt has many variants.\n\n- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.\n\n- `simp [h_1, ..., h_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and the given `h_i`s.\n The `h_i`'s are terms. If a `h_i` is a definition `f`, then the equational lemmas associated with `f` are used.\n This is a convenient way to \"unfold\" `f`.\n\n- `simp without id_1 ... id_n` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`,\n but removes the ones named `id_i`s.\n\n- `simp at h` simplifies the non dependent hypothesis `h : T`. The tactic fails if the target or another hypothesis depends on `h`.\n\n- `simp with attr` simplifies the main goal target using the lemmas tagged with the attribute `[attr]`.","source":,"tactic_param_idx":0,"tactic_params":["[expr, ...]?","(with id*)?","(without id*)?","(at id*)?","tactic.simp_config?"],"text":"simp","type":"interactive.parse interactive.types.opt_qexpr_list → interactive.parse interactive.types.with_ident_list → interactive.parse interactive.types.without_ident_list → interactive.parse interactive.types.location → opt_param tactic.simp_config {max_steps := tactic.simp_config.max_steps._default, contextual := tactic.simp_config.contextual._default, lift_eq := tactic.simp_config.lift_eq._default, canonize_instances := tactic.simp_config.canonize_instances._default, canonize_proofs := tactic.simp_config.canonize_proofs._default, use_axioms := tactic.simp_config.use_axioms._default, zeta := tactic.simp_config.zeta._default, beta := tactic.simp_config.beta._default, eta := tactic.simp_config.eta._default, proj := tactic.simp_config.proj._default} → tactic unit"},"response":"ok","seq_num":8} -{"record":{"doc":"This tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses.\nIt has many variants.\n\n- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.\n\n- `simp [h_1, ..., h_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and the given `h_i`s.\n The `h_i`'s are terms. If a `h_i` is a definition `f`, then the equational lemmas associated with `f` are used.\n This is a convenient way to \"unfold\" `f`.\n\n- `simp without id_1 ... id_n` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`,\n but removes the ones named `id_i`s.\n\n- `simp at h` simplifies the non dependent hypothesis `h : T`. The tactic fails if the target or another hypothesis depends on `h`.\n\n- `simp with attr` simplifies the main goal target using the lemmas tagged with the attribute `[attr]`.","source":,"tactic_param_idx":1,"tactic_params":["[expr, ...]?","(with id*)?","(without id*)?","(at id*)?","tactic.simp_config?"],"text":"simp","type":"interactive.parse interactive.types.opt_qexpr_list → interactive.parse interactive.types.with_ident_list → interactive.parse interactive.types.without_ident_list → interactive.parse interactive.types.location → opt_param tactic.simp_config {max_steps := tactic.simp_config.max_steps._default, contextual := tactic.simp_config.contextual._default, lift_eq := tactic.simp_config.lift_eq._default, canonize_instances := tactic.simp_config.canonize_instances._default, canonize_proofs := tactic.simp_config.canonize_proofs._default, use_axioms := tactic.simp_config.use_axioms._default, zeta := tactic.simp_config.zeta._default, beta := tactic.simp_config.beta._default, eta := tactic.simp_config.eta._default, proj := tactic.simp_config.proj._default} → tactic unit"},"response":"ok","seq_num":10} +{"record":{"doc":"This tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses.\nIt has many variants.\n\n- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.\n\n- `simp [h_1, ..., h_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and the given `h_i`s.\n The `h_i`'s are terms. If a `h_i` is a definition `f`, then the equational lemmas associated with `f` are used.\n This is a convenient way to \"unfold\" `f`.\n\n- `simp without id_1 ... id_n` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`,\n but removes the ones named `id_i`s.\n\n- `simp at h` simplifies the non dependent hypothesis `h : T`. The tactic fails if the target or another hypothesis depends on `h`.\n\n- `simp with attr` simplifies the main goal target using the lemmas tagged with the attribute `[attr]`.","source":,"state":"⊢ false","tactic_params":["[expr, ...]?","(with id*)?","(without id*)?","(at id*)?","simp_config?"],"text":"simp","type":"interactive.parse interactive.types.opt_qexpr_list → interactive.parse interactive.types.with_ident_list → interactive.parse interactive.types.without_ident_list → interactive.parse interactive.types.location → opt_param simp_config {max_steps := simp_config.max_steps._default, contextual := simp_config.contextual._default, lift_eq := simp_config.lift_eq._default, canonize_instances := simp_config.canonize_instances._default, canonize_proofs := simp_config.canonize_proofs._default, use_axioms := simp_config.use_axioms._default, zeta := simp_config.zeta._default, beta := simp_config.beta._default, eta := simp_config.eta._default, proj := simp_config.proj._default} → tactic unit"},"response":"ok","seq_num":6} +{"record":{"doc":"This tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses.\nIt has many variants.\n\n- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.\n\n- `simp [h_1, ..., h_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and the given `h_i`s.\n The `h_i`'s are terms. If a `h_i` is a definition `f`, then the equational lemmas associated with `f` are used.\n This is a convenient way to \"unfold\" `f`.\n\n- `simp without id_1 ... id_n` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`,\n but removes the ones named `id_i`s.\n\n- `simp at h` simplifies the non dependent hypothesis `h : T`. The tactic fails if the target or another hypothesis depends on `h`.\n\n- `simp with attr` simplifies the main goal target using the lemmas tagged with the attribute `[attr]`.","source":,"tactic_param_idx":0,"tactic_params":["[expr, ...]?","(with id*)?","(without id*)?","(at id*)?","simp_config?"],"text":"simp","type":"interactive.parse interactive.types.opt_qexpr_list → interactive.parse interactive.types.with_ident_list → interactive.parse interactive.types.without_ident_list → interactive.parse interactive.types.location → opt_param simp_config {max_steps := simp_config.max_steps._default, contextual := simp_config.contextual._default, lift_eq := simp_config.lift_eq._default, canonize_instances := simp_config.canonize_instances._default, canonize_proofs := simp_config.canonize_proofs._default, use_axioms := simp_config.use_axioms._default, zeta := simp_config.zeta._default, beta := simp_config.beta._default, eta := simp_config.eta._default, proj := simp_config.proj._default} → tactic unit"},"response":"ok","seq_num":8} +{"record":{"doc":"This tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses.\nIt has many variants.\n\n- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.\n\n- `simp [h_1, ..., h_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and the given `h_i`s.\n The `h_i`'s are terms. If a `h_i` is a definition `f`, then the equational lemmas associated with `f` are used.\n This is a convenient way to \"unfold\" `f`.\n\n- `simp without id_1 ... id_n` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`,\n but removes the ones named `id_i`s.\n\n- `simp at h` simplifies the non dependent hypothesis `h : T`. The tactic fails if the target or another hypothesis depends on `h`.\n\n- `simp with attr` simplifies the main goal target using the lemmas tagged with the attribute `[attr]`.","source":,"tactic_param_idx":0,"tactic_params":["[expr, ...]?","(with id*)?","(without id*)?","(at id*)?","simp_config?"],"text":"simp","type":"interactive.parse interactive.types.opt_qexpr_list → interactive.parse interactive.types.with_ident_list → interactive.parse interactive.types.without_ident_list → interactive.parse interactive.types.location → opt_param simp_config {max_steps := simp_config.max_steps._default, contextual := simp_config.contextual._default, lift_eq := simp_config.lift_eq._default, canonize_instances := simp_config.canonize_instances._default, canonize_proofs := simp_config.canonize_proofs._default, use_axioms := simp_config.use_axioms._default, zeta := simp_config.zeta._default, beta := simp_config.beta._default, eta := simp_config.eta._default, proj := simp_config.proj._default} → tactic unit"},"response":"ok","seq_num":10} +{"record":{"doc":"This tactic uses lemmas and hypotheses to simplify the main goal target or non-dependent hypotheses.\nIt has many variants.\n\n- `simp` simplifies the main goal target using lemmas tagged with the attribute `[simp]`.\n\n- `simp [h_1, ..., h_n]` simplifies the main goal target using the lemmas tagged with the attribute `[simp]` and the given `h_i`s.\n The `h_i`'s are terms. If a `h_i` is a definition `f`, then the equational lemmas associated with `f` are used.\n This is a convenient way to \"unfold\" `f`.\n\n- `simp without id_1 ... id_n` simplifies the main goal target using the lemmas tagged with the attribute `[simp]`,\n but removes the ones named `id_i`s.\n\n- `simp at h` simplifies the non dependent hypothesis `h : T`. The tactic fails if the target or another hypothesis depends on `h`.\n\n- `simp with attr` simplifies the main goal target using the lemmas tagged with the attribute `[attr]`.","source":,"tactic_param_idx":1,"tactic_params":["[expr, ...]?","(with id*)?","(without id*)?","(at id*)?","simp_config?"],"text":"simp","type":"interactive.parse interactive.types.opt_qexpr_list → interactive.parse interactive.types.with_ident_list → interactive.parse interactive.types.without_ident_list → interactive.parse interactive.types.location → opt_param simp_config {max_steps := simp_config.max_steps._default, contextual := simp_config.contextual._default, lift_eq := simp_config.lift_eq._default, canonize_instances := simp_config.canonize_instances._default, canonize_proofs := simp_config.canonize_proofs._default, use_axioms := simp_config.use_axioms._default, zeta := simp_config.zeta._default, beta := simp_config.beta._default, eta := simp_config.eta._default, proj := simp_config.proj._default} → tactic unit"},"response":"ok","seq_num":12} +{"record":{"full-id":"tactic.get_env","source":,"tactic_params":[],"type":"tactic environment"},"response":"ok","seq_num":14}