feat(library): add helper functions for 'updating' declarations

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/library/CMakeLists.txt

@@ -2,7 +2,8 @@ add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp
   kernel_bindings.cpp io_state_stream.cpp bin_app.cpp
   resolve_macro.cpp kernel_serializer.cpp max_sharing.cpp
   normalize.cpp shared_environment.cpp module.cpp coercion.cpp
-  private.cpp placeholder.cpp aliases.cpp scope.cpp)
+  private.cpp placeholder.cpp aliases.cpp scope.cpp
+  update_declaration.cpp)
 # fo_unify.cpp hop_match.cpp)
 
 target_link_libraries(library ${LEAN_LIBS})

src/library/scope.cpp

@@ -16,6 +16,7 @@ Author: Leonardo de Moura
 #include "kernel/inductive/inductive.h"
 #include "library/scope.h"
 #include "library/module.h"
+#include "library/update_declaration.h"
 
 namespace lean {
 namespace scope {
@@ -181,14 +182,8 @@ public:
         new_type  = Pi(new_type, var_deps);
         new_value = Fun(new_value, var_deps);
         add_decl_info(d.get_name(), level_deps, var_deps, new_type);
-        if (d.is_definition()) {
-            declaration new_d = mk_definition(d.get_name(), new_ls, new_type, new_value, d.is_opaque(),
-                                              d.get_weight(), d.get_module_idx(), d.use_conv_opt());
+        declaration new_d = update_declaration(d, new_ls, new_type, new_value);
         m_env = add(m_env, check(m_env, new_d));
-        } else {
-            declaration new_d = mk_theorem(d.get_name(), new_ls, new_type, new_value);
-            m_env = add(m_env, check(m_env, new_d));
-        }
     }
 };
 

src/library/update_declaration.cpp

@@ -0,0 +1,56 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "library/update_declaration.h"
+
+namespace lean {
+static declaration update_declaration(declaration d, optional<level_param_names> const & ps,
+                                      optional<expr> const & type, optional<expr> const & value) {
+    level_param_names _ps = ps ? *ps : d.get_params();
+    expr _type = type ? *type : d.get_type();
+    expr _value;
+    if (d.is_definition()) {
+        _value = value ? *value : d.get_value();
+    } else {
+        lean_assert(!value);
+    }
+    if (d.is_var_decl()) {
+        if (is_eqp(d.get_type(), _type) && is_eqp(d.get_params(), _ps))
+            return d;
+        if (d.is_axiom())
+            return mk_axiom(d.get_name(), _ps, _type);
+        else
+            return mk_var_decl(d.get_name(), _ps, _type);
+    } else {
+        if (is_eqp(d.get_type(), _type) && is_eqp(d.get_value(), _value) && is_eqp(d.get_params(), _ps))
+            return d;
+        if (d.is_theorem())
+            return mk_theorem(d.get_name(), _ps, _type, _value);
+        else
+            return mk_definition(d.get_name(), _ps, _type, _value, d.is_opaque(),
+                                 d.get_weight(), d.get_module_idx(), d.use_conv_opt());
+    }
+}
+
+declaration update_declaration_univ_params(declaration const & d, level_param_names const & ps) {
+    return update_declaration(d, optional<level_param_names>(ps), none_expr(), none_expr());
+}
+
+declaration update_declaration_type(declaration const & d, expr const & type) {
+    return update_declaration(d, optional<level_param_names>(), some_expr(type), none_expr());
+}
+
+declaration update_declaration_value(declaration const & d, expr const & value) {
+    return update_declaration(d, optional<level_param_names>(), none_expr(), some_expr(value));
+}
+
+declaration update_declaration(declaration const & d, level_param_names const & ps, expr const & type, expr const & value) {
+    return update_declaration(d, optional<level_param_names>(ps), some_expr(type), some_expr(value));
+}
+declaration update_declaration(declaration const & d, level_param_names const & ps, expr const & type) {
+    return update_declaration(d, optional<level_param_names>(ps), some_expr(type), none_expr());
+}
+}

src/library/update_declaration.h

@@ -0,0 +1,16 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "kernel/declaration.h"
+namespace lean {
+// Helper function for updating "declaration fields"
+declaration update_declaration_univ_params(declaration const & d, level_param_names const & ps);
+declaration update_declaration_type(declaration const & d, expr const & type);
+declaration update_declaration_value(declaration const & d, expr const & value);
+declaration update_declaration(declaration const & d, level_param_names const & ps, expr const & type, expr const & value);
+declaration update_declaration(declaration const & d, level_param_names const & ps, expr const & type);
+}