feat(frontends/lean): add 'print fields' command

src/emacs/lean-syntax.el

@@ -15,7 +15,7 @@
     "alias" "help" "environment" "options" "precedence" "reserve" "postfix" "prefix"
     "calc_trans" "calc_subst" "calc_refl" "calc_symm"
     "infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end"
-    "using" "namespace" "instance" "class" "section"
+    "using" "namespace" "instance" "class" "section" "fields"
     "set_option" "add_rewrite" "extends" "include" "omit" "classes" "instances" "coercions" "raw")
   "lean keywords")
 

src/frontends/lean/builtin_cmds.cpp

@@ -90,6 +90,20 @@ static void print_prefix(parser & p) {
         p.regular_stream() << "no declaration starting with prefix '" << prefix << "'" << endl;
 }
 
+static void print_fields(parser & p) {
+    auto pos = p.pos();
+    environment const & env = p.env();
+    name S = p.check_constant_next("invalid 'print fields' command, constant expected");
+    if (!is_structure(env, S))
+        throw parser_error(sstream() << "invalid 'print fields' command, '" << S << "' is not a structure", pos);
+    buffer<name> field_names;
+    get_structure_fields(env, S, field_names);
+    for (name const & field_name : field_names) {
+        declaration d = env.get(field_name);
+        p.regular_stream() << d.get_name() << " : " << d.get_type() << endl;
+    }
+}
+
 environment print_cmd(parser & p) {
     if (p.curr() == scanner::token_kind::String) {
         p.regular_stream() << p.get_str_val() << endl;
@@ -141,6 +155,9 @@ environment print_cmd(parser & p) {
     } else if (p.curr_is_token_or_id(get_axioms_tk())) {
         p.next();
         print_axioms(p);
+    } else if (p.curr_is_token_or_id(get_fields_tk())) {
+        p.next();
+        print_fields(p);
     } else {
         throw parser_error("invalid print command", p.pos());
     }

src/frontends/lean/structure_cmd.cpp

@@ -53,6 +53,31 @@ void finalize_structure_cmd() {
     delete g_tmp_prefix;
 }
 
+/** \brief Return true iff the type named \c S can be viewed as
+    a structure in the given environment.
+
+    If not, generate an error message using \c pos.
+*/
+bool is_structure(environment const & env, name const & S) {
+    optional<inductive::inductive_decls> idecls = inductive::is_inductive_decl(env, S);
+    if (!idecls || length(std::get<2>(*idecls)) != 1)
+        return false;
+    inductive::inductive_decl decl   = head(std::get<2>(*idecls));
+    return length(inductive::inductive_decl_intros(decl)) == 1 && *inductive::get_num_indices(env, S) == 0;
+}
+
+/** \brief Return the universe parameters, number of parameters and introduction rule for the given parent structure
+
+    \pre is_structure(env, S)
+*/
+static auto get_structure_info(environment const & env, name const & S)
+-> std::tuple<level_param_names, unsigned, inductive::intro_rule> {
+    lean_assert(is_structure(env, S));
+    inductive::inductive_decls idecls = *inductive::is_inductive_decl(env, S);
+    inductive::intro_rule intro = head(inductive::inductive_decl_intros(head(std::get<2>(idecls))));
+    return std::make_tuple(std::get<0>(idecls), std::get<1>(idecls), intro);
+}
+
 struct structure_cmd_fn {
     typedef std::unique_ptr<type_checker> type_checker_ptr;
     typedef std::vector<pair<name, name>> rename_vector;
@@ -123,19 +148,13 @@ struct structure_cmd_fn {
         if (!is_constant(fn))
             throw parser_error("invalid 'structure', expression must be a 'parent' structure", pos);
         name const & S = const_name(fn);
-        optional<inductive::inductive_decls> idecls = inductive::is_inductive_decl(m_env, S);
-        if (!idecls || length(std::get<2>(*idecls)) != 1)
-            throw parser_error(sstream() << "invalid 'structure' extends, '" << S << "' is not a structure", pos);
-        inductive::inductive_decl decl   = head(std::get<2>(*idecls));
-        if (length(inductive::inductive_decl_intros(decl)) != 1 || *inductive::get_num_indices(m_env, S) != 0)
+        if (!is_structure(m_env, S))
             throw parser_error(sstream() << "invalid 'structure' extends, '" << S << "' is not a structure", pos);
     }
 
     /** \brief Return the universe parameters, number of parameters and introduction rule for the given parent structure */
     std::tuple<level_param_names, unsigned, inductive::intro_rule> get_parent_info(name const & parent) {
-        inductive::inductive_decls idecls = *inductive::is_inductive_decl(m_env, parent);
-        inductive::intro_rule intro = head(inductive::inductive_decl_intros(head(std::get<2>(idecls))));
-        return std::make_tuple(std::get<0>(idecls), std::get<1>(idecls), intro);
+        return get_structure_info(m_env, parent);
     }
 
     /** \brief Sign an error if the constructor \c intro_type does not have a field named \c from_id */
@@ -792,6 +811,20 @@ environment structure_cmd(parser & p) {
     return structure_cmd_fn(p)();
 }
 
+void get_structure_fields(environment const & env, name const & S, buffer<name> & fields) {
+    lean_assert(is_structure(env, S));
+    level_param_names ls; unsigned nparams; inductive::intro_rule intro;
+    std::tie(ls, nparams, intro) = get_structure_info(env, S);
+    expr intro_type = inductive::intro_rule_type(intro);
+    unsigned i = 0;
+    while (is_pi(intro_type)) {
+        if (i >= nparams)
+            fields.push_back(S + binding_name(intro_type));
+        i++;
+        intro_type = binding_body(intro_type);
+    }
+}
+
 void register_structure_cmd(cmd_table & r) {
     add_cmd(r, cmd_info("structure",   "declare a new structure/record type", structure_cmd));
 }

src/frontends/lean/structure_cmd.h

@@ -7,6 +7,8 @@ Author: Leonardo de Moura
 #pragma once
 #include "frontends/lean/cmd_table.h"
 namespace lean {
+bool is_structure(environment const & env, name const & S);
+void get_structure_fields(environment const & env, name const & S, buffer<name> & fields);
 void register_structure_cmd(cmd_table & r);
 void initialize_structure_cmd();
 void finalize_structure_cmd();

src/frontends/lean/tokens.cpp

@@ -91,6 +91,7 @@ static name * g_notation     = nullptr;
 static name * g_call         = nullptr;
 static name * g_persistent   = nullptr;
 static name * g_root         = nullptr;
+static name * g_fields       = nullptr;
 
 void initialize_tokens() {
     g_period       = new name(".");
@@ -177,11 +178,13 @@ void initialize_tokens() {
     g_call         = new name("call");
     g_persistent   = new name("[persistent]");
     g_root         = new name("_root_");
+    g_fields       = new name("fields");
 }
 
 void finalize_tokens() {
     delete g_persistent;
     delete g_root;
+    delete g_fields;
     delete g_prev;
     delete g_scoped;
     delete g_foldr;
@@ -350,4 +353,5 @@ name const & get_notation_tk() { return *g_notation; }
 name const & get_call_tk() { return *g_call; }
 name const & get_persistent_tk() { return *g_persistent; }
 name const & get_root_tk() { return *g_root; }
+name const & get_fields_tk() { return *g_fields; }
 }

src/frontends/lean/tokens.h

@@ -93,4 +93,5 @@ name const & get_notation_tk();
 name const & get_call_tk();
 name const & get_persistent_tk();
 name const & get_root_tk();
+name const & get_fields_tk();
 }

tests/lean/run/algebra3.lean

@@ -27,6 +27,8 @@ structure monoid [class] (A : Type) extends semigroup A, has_one A :=
 -- We can suppress := and :: when we are not declaring any new field.
 structure comm_monoid [class] (A : Type) extends monoid A renaming mul→add, comm_semigroup A
 
+print fields comm_monoid
+
 structure group [class] (A : Type) extends monoid A, has_inv A :=
 (is_inv : ∀ a, mul a (inv a) = one)
 
@@ -49,6 +51,8 @@ structure ring [class] (A : Type)
 (dist_left  : ∀ a b c, mul a (add b c) = add (mul a b) (mul a c))
 (dist_right : ∀ a b c, mul (add a b) c = add (mul a c) (mul b c))
 
+print fields ring
+
 variable A : Type₁
 variables a b c d : A
 variable R : ring A