924b4d3bdc
They were at src/library because we hoped we would be able to use them in the type_context unifier. However, the plan did not work for several reasons. We saved the partial implementation in the branch: https://github.com/leodemoura/lean/tree/type_context_with_refl_lemmas Here are the problems: 1) We have to be able to rewrite even when the type context is already in tmp-mode. This is an issue because the tmp metavariables in the refl lemma clash with the ones created in the type context. Solution: implemented lift operation for idx metavariables, and custom match. This solution is not perfect since the lifting is extra overhead. 2) The term being "unfolded" may be stuck. Example: nat.add n (@one nat ?m) will not match the pattern nat.add ?x_0 (nat.succ ?x_1) because ?m is not assigned yet. We can assign it during the matching process because it is a regular metavariable and the matching is performed in tmp_mode. Possible workaround a) try to instanciate type class instances before we try the refl lemmas. This is a potential performance problem because the term can be arbitrarily big. The current heuristics we use to speed up the process do not work for the example above. Possible workaround b) allow regular metavariables be assigned by type class resolution even when we are in tmp-mode. We have not tried to implement any of these workarounds. 3) There are many more lazy-delta steps. Before this feature, when we unfold `nat.add a (succ ... (succ b) ...)`, we are done with delta-reduction. It is just iota and beta after that. However, with refl-lemmas, the term `nat.add a (succ ... (succ b) ...)` produces one lazy-delta step per succ. This produces nasty side-effects because of the The heuristic (f t =?= f s) ==> (t =?= s). Examples such as (fib 8) =?= 34 will take a very long time because of this heuristic. Possible workaround: cache failures like we did in Lean2. However, failure are only easy to cache if there are no meta-variables. 4) The type context trace gets very confusing since we use is_def_eq for matching lhs while we are computing is_def_eq. Possible workaround: disable trace when trying refl_lemmas. 5) We must be able to temporarily disable the feature. Example: when proving a refl_lemma for a definition `f`, we may have to expand the nested definitions (e.g., for match-end blocks) 6) refl/simp lemmas were designed to rewrite elaborated terms. Using them during unification may produce a series of unexpected behaviors since terms usually contain many regular and universe meta-variables. 7) We need to define a notion of "refl stuck application". Right now, a metavar is stuck, a projection is stuck if the structure is stuck, a recursor is stuck is the major premise is stuck. An application (f ...) is refl-lemma stuck if f has refl-lemmas associated with it, AND metavariables occurring in arguments are preventing a refl-lemma from being applied.
149 lines
4.1 KiB
C++
149 lines
4.1 KiB
C++
/*
|
|
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/trace.h"
|
|
#include "library/constants.h"
|
|
#include "library/kernel_serializer.h"
|
|
#include "library/typed_expr.h"
|
|
#include "library/choice.h"
|
|
#include "library/class.h"
|
|
#include "library/num.h"
|
|
#include "library/string.h"
|
|
#include "library/annotation.h"
|
|
#include "library/quote.h"
|
|
#include "library/explicit.h"
|
|
#include "library/module.h"
|
|
#include "library/protected.h"
|
|
#include "library/private.h"
|
|
#include "library/scoped_ext.h"
|
|
#include "library/reducible.h"
|
|
#include "library/aliases.h"
|
|
#include "library/export_decl.h"
|
|
#include "library/io_state.h"
|
|
#include "library/idx_metavar.h"
|
|
#include "library/sorry.h"
|
|
#include "library/placeholder.h"
|
|
#include "library/print.h"
|
|
#include "library/fingerprint.h"
|
|
#include "library/util.h"
|
|
#include "library/pp_options.h"
|
|
#include "library/projection.h"
|
|
#include "library/relation_manager.h"
|
|
#include "library/user_recursors.h"
|
|
#include "library/noncomputable.h"
|
|
#include "library/aux_recursors.h"
|
|
#include "library/type_context.h"
|
|
#include "library/local_context.h"
|
|
#include "library/metavar_context.h"
|
|
#include "library/attribute_manager.h"
|
|
#include "library/unification_hint.h"
|
|
#include "library/delayed_abstraction.h"
|
|
#include "library/app_builder.h"
|
|
#include "library/fun_info.h"
|
|
#include "library/mpq_macro.h"
|
|
#include "library/arith_instance_manager.h"
|
|
#include "library/inverse.h"
|
|
#include "library/pattern_attribute.h"
|
|
|
|
namespace lean {
|
|
void initialize_library_core_module() {
|
|
initialize_constants();
|
|
initialize_trace();
|
|
initialize_module();
|
|
initialize_scoped_ext();
|
|
initialize_attribute_manager();
|
|
}
|
|
|
|
void finalize_library_core_module() {
|
|
finalize_attribute_manager();
|
|
finalize_scoped_ext();
|
|
finalize_module();
|
|
finalize_trace();
|
|
finalize_constants();
|
|
}
|
|
|
|
void initialize_library_module() {
|
|
initialize_local_context();
|
|
initialize_metavar_context();
|
|
initialize_fingerprint();
|
|
initialize_print();
|
|
initialize_placeholder();
|
|
initialize_idx_metavar();
|
|
initialize_io_state();
|
|
initialize_kernel_serializer();
|
|
initialize_typed_expr();
|
|
initialize_choice();
|
|
initialize_string();
|
|
initialize_num();
|
|
initialize_annotation();
|
|
initialize_quote();
|
|
initialize_explicit();
|
|
initialize_protected();
|
|
initialize_private();
|
|
initialize_reducible();
|
|
initialize_aliases();
|
|
initialize_export_decl();
|
|
initialize_sorry();
|
|
initialize_class();
|
|
initialize_library_util();
|
|
initialize_pp_options();
|
|
initialize_projection();
|
|
initialize_relation_manager();
|
|
initialize_user_recursors();
|
|
initialize_noncomputable();
|
|
initialize_aux_recursors();
|
|
initialize_app_builder();
|
|
initialize_fun_info();
|
|
initialize_unification_hint();
|
|
initialize_type_context();
|
|
initialize_delayed_abstraction();
|
|
initialize_mpq_macro();
|
|
initialize_arith_instance_manager();
|
|
initialize_inverse();
|
|
initialize_pattern_attribute();
|
|
}
|
|
|
|
void finalize_library_module() {
|
|
finalize_pattern_attribute();
|
|
finalize_inverse();
|
|
finalize_arith_instance_manager();
|
|
finalize_mpq_macro();
|
|
finalize_delayed_abstraction();
|
|
finalize_type_context();
|
|
finalize_unification_hint();
|
|
finalize_fun_info();
|
|
finalize_app_builder();
|
|
finalize_aux_recursors();
|
|
finalize_noncomputable();
|
|
finalize_user_recursors();
|
|
finalize_relation_manager();
|
|
finalize_projection();
|
|
finalize_pp_options();
|
|
finalize_library_util();
|
|
finalize_class();
|
|
finalize_sorry();
|
|
finalize_export_decl();
|
|
finalize_aliases();
|
|
finalize_reducible();
|
|
finalize_private();
|
|
finalize_protected();
|
|
finalize_explicit();
|
|
finalize_quote();
|
|
finalize_annotation();
|
|
finalize_num();
|
|
finalize_string();
|
|
finalize_choice();
|
|
finalize_typed_expr();
|
|
finalize_kernel_serializer();
|
|
finalize_io_state();
|
|
finalize_idx_metavar();
|
|
finalize_placeholder();
|
|
finalize_print();
|
|
finalize_fingerprint();
|
|
finalize_metavar_context();
|
|
finalize_local_context();
|
|
}
|
|
}
|