feat(frontends/lean): add definition_cmds files

src/frontends/lean/CMakeLists.txt

@@ -10,7 +10,7 @@ type_util.cpp local_ref_info.cpp
 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
+match_expr.cpp local_context_adapter.cpp decl_util.cpp definition_cmds.cpp
 # LEGACY
 old_elaborator.cpp
 old_attributes.cpp

src/frontends/lean/decl_cmds.cpp

@@ -36,6 +36,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/update_environment_exception.h"
 #include "frontends/lean/nested_declaration.h"
 #include "frontends/lean/structure_cmd.h"
+#include "frontends/lean/definition_cmds.h"
 
 // We don't display profiling information for declarations that take less than 0.01 secs
 #ifndef LEAN_PROFILE_THRESHOLD
@@ -1139,6 +1140,9 @@ static environment definition_cmd(parser & p) {
         if (p.curr_is_token(get_structure_tk())) {
             p.next();
             return private_structure_cmd(p);
+        } else if (p.curr_is_token(get_mutual_definition_tk())) {
+            p.next();
+            return private_mutual_definition_cmd(p);
         }
     } else if (p.curr_is_token(get_protected_tk())) {
         is_protected = true;
@@ -1159,6 +1163,9 @@ static environment definition_cmd(parser & p) {
         } else if (p.curr_is_token_or_id(get_constants_tk())) {
             p.next();
             return variables_cmd_core(p, variable_kind::Constant, true);
+        } else if (p.curr_is_token_or_id(get_mutual_definition_tk())) {
+            p.next();
+            return protected_mutual_definition_cmd(p);
         }
     }
 
@@ -1186,6 +1193,16 @@ static environment definition_cmd(parser & p) {
     } else if (p.curr_is_token_or_id(get_theorem_tk())) {
         p.next();
         kind = Theorem;
+    } else if (p.curr_is_token_or_id(get_mutual_definition_tk())) {
+        if (is_private && is_noncomputable) {
+            return private_noncomputable_mutual_definition_cmd(p);
+        } else if (is_protected && is_noncomputable) {
+            return protected_noncomputable_mutual_definition_cmd(p);
+        } else if (is_noncomputable) {
+            return noncomputable_mutual_definition_cmd(p);
+        } else {
+            lean_unreachable();
+        }
     } else {
         throw parser_error("invalid definition/theorem, 'definition' or 'theorem' expected", p.pos());
     }
@@ -1286,6 +1303,7 @@ void register_decl_cmds(cmd_table & r) {
     add_cmd(r, cmd_info("attribute",       "set declaration attributes", attribute_cmd));
     add_cmd(r, cmd_info("abbreviation",    "declare a new abbreviation", definition_cmd, false));
     add_cmd(r, cmd_info("omit",            "undo 'include' command", omit_cmd));
+    add_cmd(r, cmd_info("mutual_definition", "declare a mutually recursive definition", mutual_definition_cmd));
 }
 
 void initialize_decl_cmds() {

src/frontends/lean/definition_cmds.cpp

@@ -0,0 +1,29 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "frontends/lean/parser.h"
+
+namespace lean {
+struct mutual_definition_cmd_fn {
+    parser & m_p;
+    bool     m_is_private;
+    bool     m_is_protected;
+    bool     m_is_noncomputable;
+
+    mutual_definition_cmd_fn(parser & p, bool is_private, bool is_protected, bool is_noncomputable):
+        m_p(p), m_is_private(is_private), m_is_protected(is_protected), m_is_noncomputable(is_noncomputable) {
+    }
+
+    environment operator()() {
+        // TODO(Leo)
+        lean_unreachable();
+    }
+};
+
+environment mutual_definition_cmd_core(parser & p, bool is_private, bool is_protected, bool is_noncomputable) {
+    return mutual_definition_cmd_fn(p, is_private, is_protected, is_noncomputable)();
+}
+}

src/frontends/lean/definition_cmds.h

@@ -0,0 +1,17 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "frontends/lean/parser.h"
+namespace lean {
+environment mutual_definition_cmd_core(parser & p, bool is_private, bool is_protected, bool is_noncomputable);
+inline environment mutual_definition_cmd(parser & p) { return mutual_definition_cmd_core(p, false, false, false); }
+inline environment private_mutual_definition_cmd(parser & p) { return mutual_definition_cmd_core(p, true, false, false); }
+inline environment protected_mutual_definition_cmd(parser & p) { return mutual_definition_cmd_core(p, false, true, false); }
+inline environment noncomputable_mutual_definition_cmd(parser & p) { return mutual_definition_cmd_core(p, false, false, true); }
+inline environment private_noncomputable_mutual_definition_cmd(parser & p) { return mutual_definition_cmd_core(p, true, false, true); }
+inline environment protected_noncomputable_mutual_definition_cmd(parser & p) { return mutual_definition_cmd_core(p, false, true, true); }
+}

src/frontends/lean/tokens.cpp

@@ -141,6 +141,7 @@ static name const * g_noncomputable_tk = nullptr;
 static name const * g_theory_tk = nullptr;
 static name const * g_key_equivalences_tk = nullptr;
 static name const * g_using_well_founded_tk = nullptr;
+static name const * g_mutual_definition_tk = nullptr;
 void initialize_tokens() {
     g_aliases_tk = new name{"aliases"};
     g_period_tk = new name{"."};
@@ -280,6 +281,7 @@ void initialize_tokens() {
     g_theory_tk = new name{"theory"};
     g_key_equivalences_tk = new name{"key_equivalences"};
     g_using_well_founded_tk = new name{"using_well_founded"};
+    g_mutual_definition_tk = new name{"mutual_definition"};
 }
 void finalize_tokens() {
     delete g_aliases_tk;
@@ -420,6 +422,7 @@ void finalize_tokens() {
     delete g_theory_tk;
     delete g_key_equivalences_tk;
     delete g_using_well_founded_tk;
+    delete g_mutual_definition_tk;
 }
 name const & get_aliases_tk() { return *g_aliases_tk; }
 name const & get_period_tk() { return *g_period_tk; }
@@ -559,4 +562,5 @@ name const & get_noncomputable_tk() { return *g_noncomputable_tk; }
 name const & get_theory_tk() { return *g_theory_tk; }
 name const & get_key_equivalences_tk() { return *g_key_equivalences_tk; }
 name const & get_using_well_founded_tk() { return *g_using_well_founded_tk; }
+name const & get_mutual_definition_tk() { return *g_mutual_definition_tk; }
 }

src/frontends/lean/tokens.h

@@ -143,4 +143,5 @@ name const & get_noncomputable_tk();
 name const & get_theory_tk();
 name const & get_key_equivalences_tk();
 name const & get_using_well_founded_tk();
+name const & get_mutual_definition_tk();
 }

src/frontends/lean/tokens.txt

@@ -136,3 +136,4 @@ noncomputable noncomputable
 theory       theory
 key_equivalences key_equivalences
 using_well_founded using_well_founded
+mutual_definition mutual_definition