fix: export ast field info for <local>.<field> (#677)

This commit addresses leanprover-community/mathport#58 (comment) Note that the title and first comment in that issue are unrelated and were addressed by [61b4659b7bcbf2c61b09db8370487b6f78403701](leanprover-community/mathport@61b4659)

src/frontends/lean/parser.cpp

@@ -2077,7 +2077,38 @@ expr parser::patexpr_to_expr_core(expr const & pat_or_expr) {
     return patexpr_to_expr_fn(*this)(pat_or_expr);
 }
 
-optional<expr> parser::resolve_local(name const & id, pos_info const & p, list<name> const & extra_locals,
+static expr mk_constant(parser & p, const name & id, const levels & ls, const ast_data & id_data, ast_id levels_id) {
+    expr r = mk_constant(id, ls);
+    ast_id c = p.new_ast("const", id_data.m_start).push(id_data.m_id).push(levels_id).m_id;
+    p.finalize_ast(c, r);
+    return r;
+}
+
+static expr mk_field_notation_ast(parser & p, const expr & s, const expr & r, ast_id field_id) {
+    ast_id sid = p.get_id(s);
+    ast_id ast = p.new_ast("field", p.ast_pos(sid)).push(sid).push(field_id).m_id;
+    p.finalize_ast(ast, r);
+    return r;
+}
+
+static expr mk_field_notation_compact(parser & p, const expr & s, const pos_info & field_pos, const char * field) {
+    ast_id field_id = p.new_ast("ident", field_pos, field).m_id;
+    expr r = p.save_pos(mk_field_notation_compact(s, field), field_pos);
+    return mk_field_notation_ast(p, s, r, field_id);
+}
+
+static expr mk_field_notation(parser & p, const expr & s, const pos_info & field_pos, const name & field) {
+    ast_id field_id = p.new_ast("ident", field_pos, field).m_id;
+    expr r = p.save_pos(mk_field_notation(s, field), field_pos);
+    return mk_field_notation_ast(p, s, r, field_id);
+}
+
+static expr mk_field_notation(parser & p, const expr & s, const pos_info & field_pos, ast_id field_id, unsigned fidx) {
+    expr r = p.save_pos(mk_field_notation(s, fidx), field_pos);
+    return mk_field_notation_ast(p, s, r, field_id);
+}
+
+optional<expr> parser::resolve_local(name const & id, ast_data & id_data, pos_info const & p, list<name> const & extra_locals,
                                      bool allow_field_notation) {
     /* Remark: (auxiliary) local constants many not be atomic.
        Example: when elaborating
@@ -2092,21 +2123,27 @@ optional<expr> parser::resolve_local(name const & id, pos_info const & p, list<n
     // extra locals
     unsigned vidx = 0;
     for (name const & extra : extra_locals) {
-        if (id == extra)
-            return some_expr(save_pos(mk_var(vidx), p));
+        if (id == extra) {
+            expr r = save_pos(mk_var(vidx), p);
+            finalize_ast(id_data.m_id, r);
+            return some_expr(r);
+        }
         vidx++;
     }
 
     // locals
     if (auto it1 = m_local_decls.find(id)) {
-        return some_expr(copy_with_new_pos(*it1, p));
+        expr r = copy_with_new_pos(*it1, p);
+        finalize_ast(id_data.m_id, r);
+        return some_expr(r);
     }
 
     if (allow_field_notation && !id.is_atomic() && id.is_string()) {
-        if (auto r = resolve_local(id.get_prefix(), p, extra_locals)) {
+        name n = id_data.m_value = id.get_prefix();
+        if (auto s = resolve_local(n, id_data, p, extra_locals)) {
             auto field_pos = p;
             field_pos.second += id.get_prefix().utf8_size();
-            return some_expr(save_pos(mk_field_notation_compact(*r, id.get_string()), field_pos));
+            return some_expr(mk_field_notation_compact(*this, *s, field_pos, id.get_string()));
         } else {
             return none_expr();
         }
@@ -2115,37 +2152,6 @@ optional<expr> parser::resolve_local(name const & id, pos_info const & p, list<n
     }
 }
 
-static expr mk_constant(parser & p, const name & id, const levels & ls, const ast_data & id_data, ast_id levels_id) {
-    expr r = mk_constant(id, ls);
-    ast_id c = p.new_ast("const", id_data.m_start).push(id_data.m_id).push(levels_id).m_id;
-    p.finalize_ast(c, r);
-    return r;
-}
-
-static expr mk_field_notation_ast(parser & p, const expr & s, const expr & r, ast_id field_id) {
-    ast_id sid = p.get_id(s);
-    ast_id ast = p.new_ast("field", p.ast_pos(sid)).push(sid).push(field_id).m_id;
-    p.finalize_ast(ast, r);
-    return r;
-}
-
-static expr mk_field_notation_compact(parser & p, const expr & s, const pos_info & field_pos, const char * field) {
-    ast_id field_id = p.new_ast("ident", field_pos, field).m_id;
-    expr r = p.save_pos(mk_field_notation_compact(s, field), field_pos);
-    return mk_field_notation_ast(p, s, r, field_id);
-}
-
-static expr mk_field_notation(parser & p, const expr & s, const pos_info & field_pos, const name & field) {
-    ast_id field_id = p.new_ast("ident", field_pos, field).m_id;
-    expr r = p.save_pos(mk_field_notation(s, field), field_pos);
-    return mk_field_notation_ast(p, s, r, field_id);
-}
-
-static expr mk_field_notation(parser & p, const expr & s, const pos_info & field_pos, ast_id field_id, unsigned fidx) {
-    expr r = p.save_pos(mk_field_notation(s, fidx), field_pos);
-    return mk_field_notation_ast(p, s, r, field_id);
-}
-
 expr parser::id_to_expr(name const & id, ast_data & id_data,
                         bool resolve_only, bool allow_field_notation, list<name> const & extra_locals) {
     buffer<level> lvl_buffer;
@@ -2183,9 +2189,8 @@ expr parser::id_to_expr(name const & id, ast_data & id_data,
         return r;
     }
 
-    if (auto r = resolve_local(id, p, extra_locals, allow_field_notation)) {
+    if (auto r = resolve_local(id, id_data, p, extra_locals, allow_field_notation)) {
         check_no_levels(ls, p);
-        finalize_ast(id_data.m_id, *r);
         return *r;
     }
 

src/frontends/lean/parser.h

@@ -288,7 +288,7 @@ class parser : public abstract_parser, public parser_info {
 
     std::shared_ptr<snapshot> mk_snapshot();
 
-    optional<expr> resolve_local(name const & id, pos_info const & p, list<name> const & extra_locals,
+    optional<expr> resolve_local(name const & id, ast_data & id_data, pos_info const & p, list<name> const & extra_locals,
                                  bool allow_field_notation = true);
 
     friend class module_parser;