feat(frontends/lean): allow the user to mark subterms that should be automatically abstracted into new definitions

closes #484

src/emacs/lean-syntax.el

@@ -11,7 +11,7 @@
   '("import" "prelude" "tactic_hint" "protected" "private" "definition" "renaming"
     "hiding" "exposing" "parameter" "parameters" "begin" "begin+" "proof" "qed" "conjecture" "constant" "constants"
     "hypothesis" "lemma" "corollary" "variable" "variables" "premise" "premises"
-    "print" "theorem" "example" "abbreviation"
+    "print" "theorem" "example" "abbreviation" "abstract"
     "open" "as" "export" "override" "axiom" "axioms" "inductive" "with" "structure" "record" "universe" "universes"
     "alias" "help" "environment" "options" "precedence" "reserve"
     "match" "infix" "infixl" "infixr" "notation" "postfix" "prefix"

src/frontends/lean/CMakeLists.txt

@@ -9,6 +9,6 @@ coercion_elaborator.cpp info_tactic.cpp
 init_module.cpp elaborator_context.cpp calc_proof_elaborator.cpp
 parse_tactic_location.cpp parse_rewrite_tactic.cpp builtin_tactics.cpp
 type_util.cpp elaborator_exception.cpp migrate_cmd.cpp local_ref_info.cpp
-obtain_expr.cpp decl_attributes.cpp)
+obtain_expr.cpp decl_attributes.cpp nested_declaration.cpp)
 
 target_link_libraries(lean_frontend ${LEAN_LIBS})

src/frontends/lean/builtin_exprs.cpp

@@ -33,6 +33,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/info_annotation.h"
 #include "frontends/lean/structure_cmd.h"
 #include "frontends/lean/obtain_expr.h"
+#include "frontends/lean/nested_declaration.h"
 
 namespace lean {
 namespace notation {
@@ -626,6 +627,7 @@ parse_table init_nud_table() {
     r = r.add({transition("assert", mk_ext_action(parse_assert))}, x0);
     r = r.add({transition("show", mk_ext_action(parse_show))}, x0);
     r = r.add({transition("obtain", mk_ext_action(parse_obtain))}, x0);
+    r = r.add({transition("abstract", mk_ext_action(parse_nested_declaration))}, x0);
     r = r.add({transition("if", mk_ext_action(parse_if_then_else))}, x0);
     r = r.add({transition("(", Expr), transition(")", mk_ext_action(parse_rparen))}, x0);
     r = r.add({transition("(", Expr), transition(":", Expr), transition(")", mk_ext_action(parse_typed_expr))}, x0);

src/frontends/lean/decl_attributes.cpp

@@ -246,4 +246,20 @@ environment decl_attributes::apply(environment env, io_state const & ios, name c
         env = mark_multiple_instances(env, d, m_persistent);
     return env;
 }
+
+void decl_attributes::write(serializer & s) const {
+    s << m_def_only << m_is_abbrev << m_persistent << m_is_instance << m_is_coercion
+      << m_is_reducible << m_is_irreducible << m_is_semireducible << m_is_quasireducible
+      << m_is_class << m_is_parsing_only << m_has_multiple_instances << m_unfold_f_hint
+      << m_constructor_hint << m_symm << m_trans << m_refl << m_subst << m_recursor
+      << m_rewrite << m_recursor_major_pos << m_priority << m_unfold_c_hint;
+}
+
+void decl_attributes::read(deserializer & d) {
+    d >> m_def_only >> m_is_abbrev >> m_persistent >> m_is_instance >> m_is_coercion
+      >> m_is_reducible >> m_is_irreducible >> m_is_semireducible >> m_is_quasireducible
+      >> m_is_class >> m_is_parsing_only >> m_has_multiple_instances >> m_unfold_f_hint
+      >> m_constructor_hint >> m_symm >> m_trans >> m_refl >> m_subst >> m_recursor
+      >> m_rewrite >> m_recursor_major_pos >> m_priority >> m_unfold_c_hint;
+}
 }

src/frontends/lean/decl_attributes.h

@@ -43,5 +43,7 @@ public:
     void parse(parser & p);
     environment apply(environment env, io_state const & ios, name const & d) const;
     bool is_parsing_only() const { return m_is_parsing_only; }
+    void write(serializer & s) const;
+    void read(deserializer & d);
 };
 }

src/frontends/lean/decl_cmds.cpp

@@ -27,6 +27,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/tokens.h"
 #include "frontends/lean/decl_attributes.h"
 #include "frontends/lean/update_environment_exception.h"
+#include "frontends/lean/nested_declaration.h"
 
 namespace lean {
 static environment declare_universe(parser & p, environment env, name const & n, bool local) {
@@ -671,6 +672,12 @@ class definition_cmd_fn {
             m_name = m_p.check_id_next("invalid declaration, identifier expected");
     }
 
+    expr extract_nested(expr const & v) {
+        expr new_v;
+        std::tie(m_env, new_v) = extract_nested_declarations(m_env, m_p.ios(), m_name, v);
+        return new_v;
+    }
+
     void parse_type_value() {
         // Parse universe parameters
         parser::local_scope scope1(m_p);
@@ -690,6 +697,7 @@ class definition_cmd_fn {
             m_type = m_p.parse_expr();
             save_checkpoint();
             if (is_curr_with_or_comma_or_bar(m_p)) {
+                allow_nested_decls_scope scope2(is_definition());
                 m_value = parse_equations(m_p, m_name, m_type, m_aux_decls,
                                           optional<local_environment>(), buffer<expr>(), m_pos);
             } else if (!is_definition() && !m_p.curr_is_token(get_assign_tk())) {
@@ -697,6 +705,7 @@ class definition_cmd_fn {
                 m_value = m_p.save_pos(mk_expr_placeholder(), pos);
             } else {
                 m_p.check_token_next(get_assign_tk(), "invalid declaration, ':=' expected");
+                allow_nested_decls_scope scope2(is_definition());
                 m_value = m_p.save_pos(m_p.parse_expr(), pos);
             }
         } else {
@@ -711,11 +720,13 @@ class definition_cmd_fn {
                 m_type     = Pi(ps, type, m_p);
                 save_checkpoint();
                 if (is_curr_with_or_comma_or_bar(m_p)) {
+                    allow_nested_decls_scope scope2(is_definition());
                     m_value = parse_equations(m_p, m_name, type, m_aux_decls, lenv, ps, m_pos);
                 } else if (!is_definition() && !m_p.curr_is_token(get_assign_tk())) {
                     check_end_of_theorem(m_p);
                     m_value = m_p.save_pos(mk_expr_placeholder(), pos);
                 } else {
+                    allow_nested_decls_scope scope2(is_definition());
                     m_p.check_token_next(get_assign_tk(), "invalid declaration, ':=' expected");
                     m_value = m_p.parse_scoped_expr(ps, *lenv);
                 }
@@ -730,6 +741,7 @@ class definition_cmd_fn {
                 m_type  = Pi(ps, m_type, m_p);
                 save_checkpoint();
                 m_p.check_token_next(get_assign_tk(), "invalid declaration, ':=' expected");
+                allow_nested_decls_scope scope2(is_definition());
                 m_value = m_p.parse_scoped_expr(ps, *lenv);
             }
             erase_local_binder_info(ps);
@@ -837,6 +849,7 @@ class definition_cmd_fn {
                         cd = check(mk_axiom(m_real_name, c_ls, c_type));
                         m_env = module::add(m_env, *cd);
                     } else {
+                        c_value = extract_nested(c_value);
                         cd = check(mk_definition(m_env, m_real_name, c_ls, c_type, c_value));
                         if (!m_is_private)
                             m_p.add_decl_index(m_real_name, m_pos, m_p.get_cmd_token(), c_type);
@@ -947,7 +960,7 @@ class definition_cmd_fn {
         if (aux_values.size() != m_real_aux_names.size())
             throw exception("invalid declaration, failed to compile auxiliary declarations");
         m_type  = postprocess(m_env, m_type);
-        m_value = postprocess(m_env, m_value);
+        m_value = extract_nested(postprocess(m_env, m_value));
         for (unsigned i = 0; i < aux_values.size(); i++) {
             m_aux_types[i] = postprocess(m_env, m_aux_types[i]);
             aux_values[i]  = postprocess(m_env, aux_values[i]);
@@ -1008,7 +1021,9 @@ class definition_cmd_fn {
                 new_ls       = append(m_ls, new_ls);
                 m_type       = postprocess(m_env, m_type);
                 m_value      = postprocess(m_env, m_value);
-                m_env = module::add(m_env, check(mk_definition(m_env, m_real_name, new_ls, m_type, m_value)));
+                expr new_val = extract_nested(m_value);
+                m_env = module::add(m_env, check(mk_definition(m_env, m_real_name, new_ls, m_type, new_val)));
+                // Remark: we cache the definition with the nested declarations.
                 m_p.cache_definition(m_real_name, pre_type, pre_value, new_ls, m_type, m_value);
             }
         }

src/frontends/lean/elaborator.cpp

@@ -52,6 +52,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/info_tactic.h"
 #include "frontends/lean/begin_end_ext.h"
 #include "frontends/lean/elaborator_exception.h"
+#include "frontends/lean/nested_declaration.h"
 #include "frontends/lean/calc.h"
 #include "frontends/lean/decl_cmds.h"
 

src/frontends/lean/init_module.cpp

@@ -31,6 +31,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/local_ref_info.h"
 #include "frontends/lean/obtain_expr.h"
 #include "frontends/lean/decl_cmds.h"
+#include "frontends/lean/nested_declaration.h"
 
 namespace lean {
 void initialize_frontend_lean_module() {
@@ -61,8 +62,10 @@ void initialize_frontend_lean_module() {
     initialize_local_ref_info();
     initialize_obtain_expr();
     initialize_decl_cmds();
+    initialize_nested_declaration();
 }
 void finalize_frontend_lean_module() {
+    finalize_nested_declaration();
     finalize_decl_cmds();
     finalize_obtain_expr();
     finalize_local_ref_info();

src/frontends/lean/nested_declaration.cpp

@@ -0,0 +1,221 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include <string>
+#include "util/sstream.h"
+#include "kernel/type_checker.h"
+#include "kernel/find_fn.h"
+#include "kernel/instantiate.h"
+#include "kernel/abstract.h"
+#include "library/locals.h"
+#include "library/scoped_ext.h"
+#include "library/kernel_serializer.h"
+#include "library/replace_visitor.h"
+#include "library/module.h"
+#include "library/aliases.h"
+#include "frontends/lean/decl_attributes.h"
+#include "frontends/lean/tokens.h"
+#include "frontends/lean/parser.h"
+#include "frontends/lean/util.h"
+#include "frontends/lean/nested_declaration.h"
+
+namespace lean {
+static name * g_nested_decl = nullptr;
+static std::string * g_nested_decl_opcode = nullptr;
+
+name const & get_nested_decl_name() { return *g_nested_decl; }
+std::string const & get_nested_decl_opcode() { return *g_nested_decl_opcode; }
+
+class nested_decl_macro_definition_cell : public macro_definition_cell {
+    optional<name>  m_name;
+    decl_attributes m_attributes;
+
+    void check_macro(expr const & m) const {
+        if (!is_macro(m) || macro_num_args(m) != 1)
+            throw exception(sstream() << "invalid nested declaration, incorrect number of arguments");
+    }
+public:
+    nested_decl_macro_definition_cell(optional<name> const & n, decl_attributes const & attrs):
+        m_name(n), m_attributes(attrs) {}
+    virtual name get_name() const { return get_nested_decl_name(); }
+    virtual pair<expr, constraint_seq> check_type(expr const & m, extension_context & ctx, bool infer_only) const {
+        check_macro(m);
+        return ctx.check_type(macro_arg(m, 0), infer_only);
+    }
+    virtual optional<expr> expand(expr const & m, extension_context &) const {
+        check_macro(m);
+        return some_expr(macro_arg(m, 0));
+    }
+    virtual void write(serializer & s) const {
+        s.write_string(get_nested_decl_opcode());
+        s << m_name;
+        m_attributes.write(s);
+    }
+    virtual unsigned hash() const {
+        return get_nested_decl_name().hash();
+    }
+    optional<name> const & get_decl_name() const { return m_name; }
+    decl_attributes const & get_decl_attributes() const { return m_attributes; }
+};
+
+expr mk_nested_declaration(optional<name> const & n, decl_attributes const & attrs, expr const & e) {
+    macro_definition def(new nested_decl_macro_definition_cell(n, attrs));
+    return mk_macro(def, 1, &e);
+}
+
+bool is_nested_declaration(expr const & e) {
+    return is_macro(e) && macro_def(e).get_name() == get_nested_decl_name();
+}
+
+expr update_nested_declaration(expr const & e, expr const & new_d) {
+    lean_assert(is_nested_declaration(e));
+    return mk_macro(macro_def(e), 1,  &new_d);
+}
+
+expr get_nested_declaration_arg(expr const & e) {
+    lean_assert(is_nested_declaration(e));
+    return macro_arg(e, 0);
+}
+
+optional<name> const & get_nested_declaration_name(expr const & d) {
+    lean_assert(is_nested_declaration(e));
+    return static_cast<nested_decl_macro_definition_cell const*>(macro_def(d).raw())->get_decl_name();
+}
+
+decl_attributes const & get_nested_declaration_attributes(expr const & d) {
+    lean_assert(is_nested_declaration(e));
+    return static_cast<nested_decl_macro_definition_cell const*>(macro_def(d).raw())->get_decl_attributes();
+}
+
+LEAN_THREAD_VALUE(bool, g_allow_nested_declarations, false);
+
+allow_nested_decls_scope::allow_nested_decls_scope(bool enable) {
+    m_saved = g_allow_nested_declarations;
+    g_allow_nested_declarations = enable;
+}
+
+allow_nested_decls_scope::~allow_nested_decls_scope() {
+    g_allow_nested_declarations = m_saved;
+}
+
+expr parse_nested_declaration(parser & p, unsigned, expr const *, pos_info const & pos) {
+    try {
+        optional<name> n;
+        decl_attributes attrs;
+        if (!g_allow_nested_declarations)
+            throw parser_error("invalid 'abstract' expression, it is only allowed inside definitions", pos);
+        if (p.curr_is_token(get_as_tk())) {
+            p.next();
+            n = p.check_id_next("invalid 'abstract' expression, identifier expected");
+        }
+        attrs.parse(p);
+        expr e = p.parse_expr();
+        p.check_token_next(get_end_tk(), "invalid 'abstract' expression, 'end' expected");
+        return p.save_pos(mk_nested_declaration(n, attrs, e), pos);
+    } catch (exception & ex) {
+        consume_until_end(p);
+        ex.rethrow();
+        lean_unreachable();
+    }
+}
+
+bool contains_nested_declarations(expr const & e) {
+    return static_cast<bool>(find(e, [&](expr const & n, unsigned) { return is_nested_declaration(n); }));
+}
+
+class extractor : public replace_visitor {
+    environment  m_env;
+    io_state     m_ios;
+    type_checker m_tc;
+    name         m_dname;
+    unsigned     m_idx;
+public:
+    extractor(environment const & env, io_state const & ios, name const & dname):
+        m_env(env), m_ios(ios), m_tc(m_env), m_dname(dname), m_idx(1) {}
+
+    name mk_name_for(expr const & e) {
+        lean_assert(is_nested_declaration(e));
+        if (auto n = get_nested_declaration_name(e)) {
+            return *n;
+        } else {
+            name ns  = get_namespace(m_env);
+            while (true) {
+                name aux = m_dname.append_after(m_idx);
+                m_idx++;
+                if (!m_env.find(ns + aux))
+                    return aux;
+            }
+        }
+    }
+
+    expr extract(expr const & e) {
+        lean_assert(is_nested_declaration(e));
+        expr const & d = visit(get_nested_declaration_arg(e));
+        name new_name      = mk_name_for(e);
+        name new_real_name = get_namespace(m_env) + new_name;
+        collected_locals locals;
+        collect_locals(d, locals);
+        buffer<name> uparams;
+        collect_univ_params(d).to_buffer(uparams);
+        expr new_value           = Fun(locals.get_collected(), d);
+        expr new_type            = m_tc.infer(new_value).first;
+        level_param_names new_ps = to_list(uparams);
+        levels ls                = param_names_to_levels(new_ps);
+        m_env = module::add(m_env, check(m_env, mk_definition(m_env, new_real_name, new_ps,
+                                                              new_type, new_value)));
+        if (new_name != new_real_name)
+            m_env = add_expr_alias_rec(m_env, new_name, new_real_name);
+        decl_attributes const & attrs = get_nested_declaration_attributes(e);
+        m_env = attrs.apply(m_env, m_ios, new_real_name);
+        return mk_app(mk_constant(new_real_name, ls), locals.get_collected());
+    }
+
+    expr visit_macro(expr const & e) {
+        if (is_nested_declaration(e)) {
+            return extract(e);
+        } else {
+            return replace_visitor::visit_macro(e);
+        }
+    }
+
+    expr visit_binding(expr const & b) {
+        expr new_domain = visit(binding_domain(b));
+        expr l          = mk_local(m_tc.mk_fresh_name(), new_domain);
+        expr new_body   = abstract(visit(instantiate(binding_body(b), l)), l);
+        return update_binding(b, new_domain, new_body);
+    }
+
+    environment const & get_env() const { return m_env; }
+};
+
+std::tuple<environment, expr> extract_nested_declarations(environment const & env, io_state const & ios,
+                                                          name const & dname, expr const & e) {
+    if (contains_nested_declarations(e)) {
+        extractor ex(env, ios, dname);
+        expr new_e = ex(e);
+        return std::make_tuple(ex.get_env(), new_e);
+    } else {
+        return std::make_tuple(env, e);
+    }
+}
+
+void initialize_nested_declaration() {
+    g_nested_decl        = new name("nested_decl");
+    g_nested_decl_opcode = new std::string("NDecl");
+    register_macro_deserializer(get_nested_decl_opcode(),
+                                [](deserializer & d, unsigned num, expr const * args) {
+                                    if (num != 1)
+                                        throw corrupted_stream_exception();
+                                    optional<name> n; decl_attributes attrs;
+                                    d >> n; attrs.read(d);
+                                    return mk_nested_declaration(n, attrs, args[0]);
+                                });
+}
+void finalize_nested_declaration() {
+    delete g_nested_decl;
+    delete g_nested_decl_opcode;
+}
+}

src/frontends/lean/nested_declaration.h

@@ -0,0 +1,24 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "util/flet.h"
+#include "kernel/expr.h"
+namespace lean {
+class parser;
+// auxiliary object used to temporarily enable nested declarations
+class allow_nested_decls_scope {
+    bool m_saved;
+public:
+    allow_nested_decls_scope(bool enable = true);
+    ~allow_nested_decls_scope();
+};
+expr parse_nested_declaration(parser & p, unsigned, expr const *, pos_info const & pos);
+std::tuple<environment, expr> extract_nested_declarations(environment const & env, io_state const & ios,
+                                                          name const & def_name, expr const & e);
+void initialize_nested_declaration();
+void finalize_nested_declaration();
+}

src/frontends/lean/token_table.cpp

@@ -97,7 +97,7 @@ void init_token_table(token_table & t) {
          {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {"rewrite", 0}, {"xrewrite", 0}, {"krewrite", 0},
          {"esimp", 0}, {"fold", 0}, {"unfold", 0},
          {"generalize", 0}, {"as", 0}, {":=", 0}, {"--", 0}, {"#", 0},
-         {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"begin+", g_max_prec},
+         {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"begin+", g_max_prec}, {"abstract", g_max_prec},
          {"proof", g_max_prec}, {"qed", 0}, {"@", g_max_prec},
          {"sorry", g_max_prec}, {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec},
          {"?(", g_max_prec}, {"⌞", g_max_prec}, {"⌟", 0}, {"match", 0},

tests/lean/nested1.lean

@@ -0,0 +1,19 @@
+import data.nat
+open nat
+
+namespace test
+
+constant foo (a : nat) : a > 0 → nat
+
+definition bla (a : nat) :=
+foo
+  (succ (succ a))
+  abstract as foo.prf [irreducible] lt.step (zero_lt_succ a) end
+
+print foo.prf
+print bla
+
+end test
+
+print test.bla
+print test.foo.prf

tests/lean/nested1.lean.expected.out

@@ -0,0 +1,8 @@
+definition test.foo.prf [irreducible] : ∀ (x : ℕ), 0 < succ (succ x)
+λ (x : ℕ), lt.step (zero_lt_succ x)
+definition test.bla : ℕ → ℕ
+λ (a : ℕ), foo (succ (succ a)) (foo.prf a)
+definition test.bla : ℕ → ℕ
+λ (a : ℕ), test.foo (succ (succ a)) (test.foo.prf a)
+definition test.foo.prf : ∀ (x : ℕ), 0 < succ (succ x)
+λ (x : ℕ), lt.step (zero_lt_succ x)

tests/lean/nested2.lean

@@ -0,0 +1,32 @@
+import data.nat data.list
+open nat
+
+constant foo (a : nat) : a > 0 → nat
+
+definition bla (a : nat) :=
+foo
+  (succ (succ a))
+  abstract lt.step abstract zero_lt_succ a end  end
+
+print bla
+print bla_1
+print bla_2
+
+definition test (a : nat) :=
+foo
+  (succ (succ a))
+  abstract [reducible] lt.step abstract [irreducible] zero_lt_succ a end  end
+
+print test_1
+print test_2
+
+constant voo {A : Type} (a b : A) : a ≠ b → bool
+
+set_option pp.universes true
+
+open list
+definition tst {A : Type} (a : A) (l : list A) :=
+voo (a::l) [] abstract by contradiction end
+
+print tst_1
+print tst

tests/lean/nested2.lean.expected.out

@@ -0,0 +1,15 @@
+definition bla : ℕ → ℕ
+λ (a : ℕ), foo (succ (succ a)) (bla_2 a)
+definition bla_1 : ∀ (x : ℕ), 0 < succ x
+λ (x : ℕ), zero_lt_succ x
+definition bla_2 : ∀ (x : ℕ), 0 < succ (succ x)
+λ (x : ℕ), lt.step (bla_1 x)
+definition test_1 [irreducible] : ∀ (x : ℕ), 0 < succ x
+λ (x : ℕ), zero_lt_succ x
+definition test_2 [reducible] : ∀ (x : ℕ), 0 < succ (succ x)
+λ (x : ℕ), lt.step (test_1 x)
+definition tst_1 : ∀ (x : Type.{l_1}) (x_1 : x) (x_2 : list.{l_1} x),
+  x_1 :: x_2 = nil.{l_1} → list.no_confusion_type.{0 l_1} false (x_1 :: x_2) nil.{l_1}
+λ (x : Type.{l_1}) (x_1 : x) (x_2 : list.{l_1} x), list.no_confusion.{0 l_1}
+definition tst : Π {A : Type.{l_1}}, A → list.{l_1} A → bool
+λ (A : Type.{l_1}) (a : A) (l : list.{l_1} A), voo.{(max 1 l_1)} (a :: l) nil.{l_1} (tst_1.{l_1} A a l)