From 68c1ff62199a2db4a3471de19645c76ee163b648 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 27 Mar 2017 14:46:45 +0200 Subject: [PATCH] feat(frontends/lean/builtin_exprs): use local field inference for info too --- src/frontends/lean/builtin_exprs.cpp | 4 ++-- src/frontends/lean/info_manager.h | 3 ++- src/frontends/lean/interactive.cpp | 9 ++++++++- tests/lean/interactive/field_info.lean | 9 +++++++++ tests/lean/interactive/field_info.lean.expected.out | 3 +++ 5 files changed, 24 insertions(+), 4 deletions(-) diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 97392a3e2d..cb1acf8a48 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -1066,10 +1066,10 @@ static expr parse_proj(parser_state & p, unsigned, expr const * args, pos_info c /* failed to elaborate or infer type */ throw ex; } - expr fn = get_app_fn(lhs_type); + expr fn = get_app_fn(lhs_type); if (is_constant(fn)) { - ex.m_token_info.m_struct = const_name(fn); ex.m_token_info.m_context = break_at_pos_exception::token_context::field; + ex.m_token_info.m_struct = const_name(fn); } throw; } diff --git a/src/frontends/lean/info_manager.h b/src/frontends/lean/info_manager.h index c2192a12b2..087b9434ed 100644 --- a/src/frontends/lean/info_manager.h +++ b/src/frontends/lean/info_manager.h @@ -73,7 +73,6 @@ class info_manager : public log_entry_cell { std::string m_file_name; rb_map m_line_data; - line_info_data_set get_line_info_set(unsigned l) const; void add_info(pos_info pos, info_data data); public: info_manager() {} @@ -89,6 +88,8 @@ public: void add_const_info(environment const & env, pos_info pos, name const & full_id); void add_vm_obj_format_info(pos_info pos, environment const & env, vm_obj const & thunk); + line_info_data_set get_line_info_set(unsigned l) const; + void instantiate_mvars(metavar_context const & mctx); void merge(info_manager const & info); diff --git a/src/frontends/lean/interactive.cpp b/src/frontends/lean/interactive.cpp index da90d21529..7efd6aff4d 100644 --- a/src/frontends/lean/interactive.cpp +++ b/src/frontends/lean/interactive.cpp @@ -129,7 +129,14 @@ void report_info(environment const & env, options const & opts, io_state const & record["tactic_param_idx"] = *idx; has_token_info = true; break; - default: + 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); + if (auto doc = get_doc_string(env, name)) + record["doc"] = *doc; + interactive_report_type(env, opts, env.get(name).get_type(), record); + } default: break; } } diff --git a/tests/lean/interactive/field_info.lean b/tests/lean/interactive/field_info.lean index e6fb9edd44..831005b55d 100644 --- a/tests/lean/interactive/field_info.lean +++ b/tests/lean/interactive/field_info.lean @@ -2,3 +2,12 @@ def f (n : ℕ) := n^.to_string --^ "command": "info" def g (l : list ℕ) := l^.all --^ "command": "info" + +-- elaborated, not locally inferable +def h : list ℕ → (ℕ → bool) → bool := +λ l, (l ++ l)^.all + --^ "command": "info" + +-- not elaborated, locally inferable +def j := (list.nil^.all + --^ "command": "info" diff --git a/tests/lean/interactive/field_info.lean.expected.out b/tests/lean/interactive/field_info.lean.expected.out index f0f8af5995..1eeec1c550 100644 --- a/tests/lean/interactive/field_info.lean.expected.out +++ b/tests/lean/interactive/field_info.lean.expected.out @@ -1,3 +1,6 @@ +{"msgs":[{"caption":"","file_name":"f","pos_col":40,"pos_line":13,"severity":"error","text":"invalid expression, `)` expected"}],"response":"all_messages"} {"message":"file invalidated","response":"ok","seq_num":0} {"record":{"full-id":"nat.to_string","source":,"type":"ℕ → string"},"response":"ok","seq_num":2} {"record":{"full-id":"list.all","source":,"type":"Π {α : Type}, list α → (α → bool) → bool"},"response":"ok","seq_num":4} +{"record":{"full-id":"list.all","source":,"type":"Π {α : Type}, list α → (α → bool) → bool"},"response":"ok","seq_num":9} +{"record":{"full-id":"list.all","source":,"type":"Π {α : Type u}, list α → (α → bool) → bool"},"response":"ok","seq_num":13}