feat(frontends/lean/inductive_cmds): scaffold for new inductive commands

src/frontends/lean/CMakeLists.txt

@@ -11,6 +11,7 @@ decl_attributes.cpp nested_declaration.cpp
 opt_cmd.cpp prenum.cpp
 print_cmd.cpp elaborator.cpp pattern_attribute.cpp
 match_expr.cpp local_context_adapter.cpp decl_util.cpp definition_cmds.cpp
+inductive_cmds.cpp
 # LEGACY
 old_elaborator.cpp
 old_attributes.cpp

src/frontends/lean/inductive_cmds.cpp

@@ -0,0 +1,61 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Daniel Selsam
+*/
+#include <algorithm>
+#include <library/attribute_manager.h>
+#include "util/sstream.h"
+#include "util/name_map.h"
+#include "util/fresh_name.h"
+#include "util/sexpr/option_declarations.h"
+#include "kernel/replace_fn.h"
+#include "kernel/instantiate.h"
+#include "kernel/inductive/inductive.h"
+#include "kernel/abstract.h"
+#include "kernel/free_vars.h"
+#include "library/scoped_ext.h"
+#include "library/locals.h"
+#include "library/deep_copy.h"
+#include "library/placeholder.h"
+#include "library/aliases.h"
+#include "library/protected.h"
+#include "library/explicit.h"
+#include "library/reducible.h"
+#include "library/class.h"
+#include "library/util.h"
+#include "library/app_builder.h"
+#include "library/type_context.h"
+#include "library/constructions/rec_on.h"
+#include "library/constructions/induction_on.h"
+#include "library/constructions/cases_on.h"
+#include "library/constructions/brec_on.h"
+#include "library/constructions/no_confusion.h"
+#include "frontends/lean/decl_cmds.h"
+#include "frontends/lean/util.h"
+#include "frontends/lean/parser.h"
+#include "frontends/lean/tokens.h"
+#include "frontends/lean/type_util.h"
+
+namespace lean {
+
+environment xinductive_cmd(parser & p) {
+    // TODO(dhs): implement
+    throw exception("xinductive_cmd not yet supported.");
+}
+
+environment xmutual_inductive_cmd(parser & p) {
+    // TODO(dhs): implement
+    throw exception("xmutual_inductive_cmd not yet supported.");
+}
+
+void register_inductive_cmds(cmd_table & r) {
+    add_cmd(r, cmd_info("xinductive",        "declare an inductive datatype",        xinductive_cmd));
+    add_cmd(r, cmd_info("xmutual_inductive", "declare mutually inductive datatypes", xmutual_inductive_cmd));
+}
+
+void initialize_inductive_cmds() {}
+void finalize_inductive_cmds() {}
+
+}

src/frontends/lean/inductive_cmds.h

@@ -0,0 +1,13 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Daniel Selsam
+*/
+#pragma once
+#include "frontends/lean/cmd_table.h"
+namespace lean {
+void register_inductive_cmds(cmd_table & r);
+void initialize_inductive_cmds();
+void finalize_inductive_cmds();
+}

src/frontends/lean/init_module.cpp

@@ -15,6 +15,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/builtin_cmds.h"
 #include "frontends/lean/builtin_exprs.h"
 #include "frontends/lean/inductive_cmd.h"
+#include "frontends/lean/inductive_cmds.h"
 #include "frontends/lean/structure_cmd.h"
 #include "frontends/lean/info_manager.h"
 #include "frontends/lean/parse_table.h"
@@ -48,6 +49,7 @@ void initialize_frontend_lean_module() {
     initialize_parser_config();
     initialize_calc();
     initialize_inductive_cmd();
+    initialize_inductive_cmds();
     initialize_structure_cmd();
     initialize_info_manager();
     initialize_pp();
@@ -69,6 +71,7 @@ void finalize_frontend_lean_module() {
     finalize_pp();
     finalize_info_manager();
     finalize_structure_cmd();
+    finalize_inductive_cmds();
     finalize_inductive_cmd();
     finalize_calc();
     finalize_parser_config();