fix(frontends/lean/builtin_cmds): fixes #630

src/frontends/lean/elaborator.cpp

@@ -36,6 +36,7 @@ Author: Leonardo de Moura
 #include "library/constants.h"
 #include "library/util.h"
 #include "library/choice_iterator.h"
+#include "library/projection.h"
 #include "library/pp_options.h"
 #include "library/tactic/expr_to_tactic.h"
 #include "library/tactic/class_instance_synth.h"
@@ -1297,12 +1298,9 @@ expr elaborator::visit_decreasing(expr const & e, constraint_seq & cs) {
     return mk_decreasing(dec_app, dec_proof);
 }
 
-bool elaborator::is_structure(expr const & S) {
+bool elaborator::is_structure_like(expr const & S) {
     expr const & I = get_app_fn(S);
-    return is_constant(I) &&
-        inductive::is_inductive_decl(env(), const_name(I)) &&
-        *inductive::get_num_intro_rules(env(), const_name(I)) == 1 &&
-        *inductive::get_num_indices(env(), const_name(I)) == 0;
+    return is_constant(I) && ::lean::is_structure_like(env(), const_name(I));
 }
 
 expr elaborator::visit_structure_instance(expr const & e, constraint_seq & cs) {
@@ -1312,7 +1310,7 @@ expr elaborator::visit_structure_instance(expr const & e, constraint_seq & cs) {
     destruct_structure_instance(e, S, field_names, field_values, using_exprs);
     lean_assert(field_names.size() == field_values.size());
     expr new_S     = visit(S, cs);
-    if (!is_structure(new_S))
+    if (!is_structure_like(new_S))
         throw_elaborator_exception("invalid structure instance, given type is not a structure", S);
     buffer<expr> new_S_args;
     expr I = get_app_args(new_S, new_S_args);
@@ -1337,7 +1335,7 @@ expr elaborator::visit_structure_instance(expr const & e, constraint_seq & cs) {
     for (expr const & u : using_exprs) {
         expr new_u = visit(u, cs);
         expr new_u_type = whnf(infer_type(new_u, cs), cs);
-        if (!is_structure(new_u_type))
+        if (!is_structure_like(new_u_type))
             throw_elaborator_exception("invalid structure instance, type of 'using' argument is not a structure", u);
         new_using_exprs.push_back(new_u);
         new_using_types.push_back(new_u_type);

src/frontends/lean/elaborator.h

@@ -174,7 +174,7 @@ class elaborator : public coercion_info_manager {
     expr visit_decreasing(expr const & e, constraint_seq & cs);
     constraint mk_equations_cnstr(expr const & m, expr const & eqns);
 
-    bool is_structure(expr const & S);
+    bool is_structure_like(expr const & S);
     expr visit_structure_instance(expr const & e, constraint_seq & cs);
 
     expr process_obtain_expr(list<obtain_struct> const & s_list, list<expr> const & from_list,

src/frontends/lean/structure_cmd.cpp

@@ -67,11 +67,11 @@ bool get_structure_proj_mk_thm(options const & o) { return o.get_bool(*g_gen_pro
 
 /** \brief Return the universe parameters, number of parameters and introduction rule for the given parent structure
 
-    \pre is_structure(env, S)
+    \pre is_structure_like(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));
+    lean_assert(is_structure_like(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);
@@ -154,7 +154,7 @@ 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);
-        if (!is_structure(m_env, S))
+        if (!is_structure_like(m_env, S))
             throw parser_error(sstream() << "invalid 'structure' extends, '" << S << "' is not a structure", pos);
     }
 
@@ -952,7 +952,7 @@ environment structure_cmd(parser & p) {
 }
 
 void get_structure_fields(environment const & env, name const & S, buffer<name> & fields) {
-    lean_assert(is_structure(env, S));
+    lean_assert(is_structure_like(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);
@@ -965,6 +965,23 @@ void get_structure_fields(environment const & env, name const & S, buffer<name>
     }
 }
 
+bool is_structure(environment const & env, name const & S) {
+    if (!is_structure_like(env, S))
+        return false;
+    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);
+    for (unsigned i = 0; i < nparams; i++) {
+        if (!is_pi(intro_type))
+            return false;
+        intro_type = binding_body(intro_type);
+    }
+    if (!is_pi(intro_type))
+        return false;
+    name field_name = S + binding_name(intro_type);
+    return get_projection_info(env, field_name) != nullptr;
+}
+
 static name * g_structure_instance_name          = nullptr;
 static std::string * g_structure_instance_opcode = nullptr;
 

src/frontends/lean/structure_cmd.h

@@ -12,9 +12,10 @@ void init_structure_instance_parsing_rules(parse_table & r);
 bool is_structure_instance(expr const & e);
 void destruct_structure_instance(expr const & e, expr & t, buffer<name> & field_names,
                                  buffer<expr> & field_values, buffer<expr> & using_exprs);
-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);
+/** \brief Return true iff \c S is a structure created with the structure command */
+bool is_structure(environment const & env, name const & S);
 void initialize_structure_cmd();
 void finalize_structure_cmd();
 }

src/library/definitional/projection.cpp

@@ -19,19 +19,6 @@ Author: Leonardo de Moura
 #include "library/definitional/projection.h"
 
 namespace lean {
-/** \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;
-}
-
 [[ noreturn ]] static void throw_ill_formed(name const & n) {
     throw exception(sstream() << "projection generation, '" << n << "' is an ill-formed inductive datatype");
 }

src/library/definitional/projection.h

@@ -22,11 +22,4 @@ environment mk_projections(environment const & env, name const & n, buffer<name>
                            implicit_infer_kind infer_k = implicit_infer_kind::Implicit, bool inst_implicit = false);
 environment mk_projections(environment const & env, name const & n,
                            implicit_infer_kind infer_k = implicit_infer_kind::Implicit, bool inst_implicit = false);
-
-/** \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);
 }

src/library/projection.cpp

@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include "util/sstream.h"
 #include "kernel/kernel_exception.h"
 #include "kernel/instantiate.h"
+#include "kernel/inductive/inductive.h"
 #include "library/util.h"
 #include "library/projection.h"
 #include "library/module.h"
@@ -169,6 +170,19 @@ public:
     }
 };
 
+/** \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_like(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;
+}
+
 expr mk_projection_macro(name const & proj_name, expr const & e) {
     macro_definition def(new projection_macro_definition_cell(proj_name));
     return mk_macro(def, 1, &e);

src/library/projection.h

@@ -55,6 +55,13 @@ inline bool is_projection(environment const & env, name const & n) {
 */
 expr mk_projection_macro(name const & proj_name, expr const & e);
 
+/** \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_like(environment const & env, name const & S);
+
 void initialize_projection();
 void finalize_projection();
 }

tests/lean/630.lean

@@ -0,0 +1,4 @@
+import data.real
+print pnat
+
+print prod

tests/lean/630.lean.expected.out

@@ -0,0 +1,7 @@
+inductive pnat : Type₁
+constructors:
+pnat.pos : Π (n : ℕ), nat.gt n (nat.of_num 0) → ℕ+
+structure prod : Type → Type → Type
+fields:
+prod.pr1 : Π {A : Type} {B : Type}, A × B → A
+prod.pr2 : Π {A : Type} {B : Type}, A × B → B