diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index d5f40eb892..af83288d68 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -15,14 +15,10 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp fun_info.cpp congr_lemma.cpp defeq_canonizer.cpp scope_pos_info_provider.cpp mpq_macro.cpp arith_instance_manager.cpp replace_visitor_with_tc.cpp aux_definition.cpp inverse.cpp library_system.cpp rfl_lemmas.cpp - pattern_attribute.cpp + pattern_attribute.cpp choice.cpp locals.cpp # Legacy -- The following files will be eventually deleted - normalize.cpp justification.cpp constraint.cpp metavar.cpp choice.cpp locals.cpp + normalize.cpp justification.cpp constraint.cpp metavar.cpp old_type_context.cpp legacy_type_context.cpp old_type_checker.cpp old_converter.cpp old_default_converter.cpp - old_util.cpp old_local_context.cpp choice_iterator.cpp - old_tmp_type_context.cpp - - # light_lt_manager.cpp - # proof_irrel_expr_manager.cpp + old_util.cpp ) diff --git a/src/library/choice_iterator.cpp b/src/library/choice_iterator.cpp deleted file mode 100644 index ec9558310b..0000000000 --- a/src/library/choice_iterator.cpp +++ /dev/null @@ -1,27 +0,0 @@ -/* -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/choice_iterator.h" - -namespace lean { -lazy_list choose(std::shared_ptr c, bool ignore_failure) { - return mk_lazy_list([=]() { - auto s = c->next(); - if (s) { - return some(mk_pair(*s, choose(c, false))); - } else if (ignore_failure) { - // return singleton empty list of constraints, and let tactic hints try to instantiate the metavariable. - return lazy_list::maybe_pair(constraints(), lazy_list()); - } else { - return lazy_list::maybe_pair(); - } - }); -} - -lazy_list choose(std::shared_ptr c) { - return choose(c, c->ignore_failure()); -} -} diff --git a/src/library/choice_iterator.h b/src/library/choice_iterator.h deleted file mode 100644 index 1d8af525e7..0000000000 --- a/src/library/choice_iterator.h +++ /dev/null @@ -1,28 +0,0 @@ -/* -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 "util/lazy_list.h" -#include "library/constraint.h" - -namespace lean { -/** \brief Abstract (helper) class for creating lazy_list */ -class choice_iterator { - bool m_ignore_failure; -public: - choice_iterator(bool ignore_failure = false):m_ignore_failure(ignore_failure) {} - virtual ~choice_iterator() {} - virtual optional next() = 0; - bool ignore_failure() const { return m_ignore_failure; } -}; - -/** \brief Convert a choice_iterator into a lazy_list - The lazy list is generated by invoking the method \c choice_iterator::next. - If c->ignore_failure() is true AND \c c does not produce any result, - then the singleton lazy_list is produced with an empty set of constraints. -*/ -lazy_list choose(std::shared_ptr c); -} diff --git a/src/library/old_local_context.cpp b/src/library/old_local_context.cpp deleted file mode 100644 index e6d896614a..0000000000 --- a/src/library/old_local_context.cpp +++ /dev/null @@ -1,123 +0,0 @@ -/* -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 "util/fresh_name.h" -#include "kernel/abstract.h" -#include "kernel/replace_fn.h" -#include "library/metavar.h" -#include "library/old_local_context.h" - -namespace lean { -/** \brief Given a list of local constants \c locals - (x_n : A_n) ... (x_0 : A_0) - and a term \c e - t[x_0, ..., x_n] - return - t[#n, ..., #0] -*/ -expr old_local_context::abstract_locals(expr const & e, list const & locals) { - lean_assert(std::all_of(locals.begin(), locals.end(), [](expr const & e) { return closed(e) && is_local(e); })); - if (!has_local(e)) - return e; - return replace(e, [=](expr const & m, unsigned offset) -> optional { - if (!has_local(m)) - return some_expr(m); // expression m does not contain local constants - if (is_local(m)) { - unsigned i = 0; - for (expr const & l : locals) { - if (mlocal_name(l) == mlocal_name(m)) - return some_expr(copy_tag(m, mk_var(offset + i))); - i++; - } - return none_expr(); - } - return none_expr(); - }); -} - -auto old_local_context::to_local_decl(expr const & l, list const & ctx) -> local_decl { - return local_decl(local_pp_name(l), abstract_locals(mlocal_type(l), ctx), local_info(l)); -} - -old_local_context::old_local_context() {} -old_local_context::old_local_context(list const & ctx) { - set_ctx(ctx); -} - -void old_local_context::set_ctx(list const & ctx) { - m_ctx = ctx; - buffer tmp; - list it = ctx; - while (it) { - tmp.push_back(to_local_decl(head(it), tail(it))); - it = tail(it); - } - m_ctx_abstracted = to_list(tmp.begin(), tmp.end()); -} - -expr old_local_context::pi_abstract_context(expr e, tag g) const { - e = abstract_locals(e, m_ctx); - for (local_decl const & l : m_ctx_abstracted) - e = mk_pi(std::get<0>(l), std::get<1>(l), e, std::get<2>(l), g); - return e; -} - -static expr apply_context_core(expr const & f, list const & ctx, tag g) { - if (ctx) - return mk_app(apply_context_core(f, tail(ctx), g), head(ctx), g); - else - return f; -} - -expr old_local_context::apply_context(expr const & f, tag g) const { - return apply_context_core(f, m_ctx, g); -} - -expr old_local_context::mk_type_metavar(tag g) const { - name n = mk_fresh_name(); - expr s = mk_sort(mk_meta_univ(mk_fresh_name()), g); - expr t = pi_abstract_context(s, g); - return ::lean::mk_metavar(n, t, g); -} - -expr old_local_context::mk_type_meta(tag g) const { - return apply_context(mk_type_metavar(g), g); -} - -expr old_local_context::mk_metavar(optional const & suffix, optional const & type, tag g) const { - name n = mk_fresh_name(); - if (suffix) - n = n + *suffix; - expr r_type = type ? *type : mk_type_meta(g); - expr t = pi_abstract_context(r_type, g); - return ::lean::mk_metavar(n, t, g); -} - -expr old_local_context::mk_meta(optional const & suffix, optional const & type, tag g) const { - expr mvar = mk_metavar(suffix, type, g); - expr meta = apply_context(mvar, g); - return meta; -} - -void old_local_context::add_local(expr const & l) { - lean_assert(is_local(l)); - m_ctx_abstracted = cons(to_local_decl(l, m_ctx), m_ctx_abstracted); - m_ctx = cons(l, m_ctx); - lean_assert(length(m_ctx) == length(m_ctx_abstracted)); -} - -list const & old_local_context::get_data() const { - return m_ctx; -} - -static list instantiate_locals(list const & ls, substitution & s) { - return map(ls, [&](expr const & l) { return update_mlocal(l, s.instantiate(mlocal_type(l))); }); -} - -old_local_context old_local_context::instantiate(substitution s) const { - return old_local_context(instantiate_locals(m_ctx, s)); -} -} diff --git a/src/library/old_local_context.h b/src/library/old_local_context.h deleted file mode 100644 index c5d19739c1..0000000000 --- a/src/library/old_local_context.h +++ /dev/null @@ -1,95 +0,0 @@ -/* -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 "util/name_map.h" -#include "kernel/expr.h" - -namespace lean { -/** \brief Auxiliary data-structure for storing the local context, - and creating metavariables in the scope of the local context efficiently -*/ -class old_local_context { - list m_ctx; // current local context: a list of local constants - typedef std::tuple local_decl; - list m_ctx_abstracted; // m_ctx where elements have been abstracted - static expr abstract_locals(expr const & e, list const & locals); - // convert a local constant into a local_decl - static local_decl to_local_decl(expr const & l, list const & ctx); -public: - old_local_context(); - old_local_context(list const & ctx); - - void set_ctx(list const & ctx); - - /** \brief Given e[l_1, ..., l_n] and assuming \c m_ctx is - [l_n : A_n[l_1, ..., l_{n-1}], ..., l_1 : A_1 ], - then the result is - (Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), e[x_1, ... x_n]). - */ - expr pi_abstract_context(expr e, tag g) const; - - /** \brief Assuming \c m_ctx is - [l_n : A_n[l_1, ..., l_{n-1}], ..., l_1 : A_1 ], - return (f l_1 ... l_n). - */ - expr apply_context(expr const & f, tag g) const; - - /** \brief Assuming \c m_ctx is - [l_n : A_n[l_1, ..., l_{n-1}], ..., l_1 : A_1 ], - return a fresh metavariable \c ?m with type - (Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), Type.{?u}), - where \c ?u is a fresh universe metavariable. - */ - expr mk_type_metavar(tag g) const; - - /** \brief Assuming \c m_ctx is - [l_n : A_n[l_1, ..., l_{n-1}], ..., l_1 : A_1 ], - return (?m l_1 ... l_n) where \c ?m is a fresh metavariable with type - (Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), Type.{?u}), - and \c ?u is a fresh universe metavariable. - - \remark The type of the resulting expression is Type.{?u} - */ - expr mk_type_meta(tag g) const; - - /** \brief Given type[l_1, ..., l_n] and assuming \c m_ctx is - [l_n : A_n[l_1, ..., l_{n-1}], ..., l_1 : A_1 ], - then the result is a fresh metavariable \c ?m with type - (Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), type[x_1, ... x_n]). - If type is none, then the result is a fresh metavariable \c ?m1 with type - (Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), ?m2 x1 .... xn), - where ?m2 is another fresh metavariable with type - (Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), Type.{?u}), - and \c ?u is a fresh universe metavariable. - - \remark If \c suffix is not none, then it is appended to the (fresh) metavariable name. - */ - expr mk_metavar(optional const & suffix, optional const & type, tag g) const; - - /** \brief Given type[l_1, ..., l_n] and assuming \c m_ctx is - [l_n : A_n[l_1, ..., l_{n-1}], ..., l_1 : A_1 ], - return (?m l_1 ... l_n), where ?m is a fresh metavariable - created using \c mk_metavar. - - \see mk_metavar - - \remark If \c suffix is not none, then it is appended to the (fresh) metavariable name. - */ - expr mk_meta(optional const & suffix, optional const & type, tag g) const; - expr mk_meta(optional const & type, tag g) const { - return mk_meta(optional(), type, g); - } - - /** \brief Return context as a list */ - list const & get_data() const; - - void add_local(expr const & l); - - /** \brief Instantiate metavariables occurring this local context using \c s, and return updated old_local_context */ - old_local_context instantiate(substitution s) const; -}; -} diff --git a/src/library/old_tmp_type_context.cpp b/src/library/old_tmp_type_context.cpp deleted file mode 100644 index e00ca822e0..0000000000 --- a/src/library/old_tmp_type_context.cpp +++ /dev/null @@ -1,144 +0,0 @@ -/* -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 "library/old_tmp_type_context.h" -#include "library/idx_metavar.h" - -namespace lean { -void old_tmp_type_context::init(environment const & env, reducible_behavior b) { - switch (b) { - case UnfoldReducible: m_opaque_pred = mk_not_reducible_pred(env); break; - case UnfoldSemireducible: m_opaque_pred = mk_irreducible_pred(env); break; - } -} - -old_tmp_type_context::old_tmp_type_context(environment const & env, options const & o, reducible_behavior b): - old_type_context(env, o) { - init(env, b); -} - -old_tmp_type_context::~old_tmp_type_context() { -} - -void old_tmp_type_context::clear() { - m_uassignment.clear(); - m_eassignment.clear(); - m_trail.clear(); - m_scopes.clear(); - clear_infer_cache(); -} - -void old_tmp_type_context::set_next_uvar_idx(unsigned next_idx) { - lean_assert(m_uassignment.empty()); - lean_assert(m_scopes.empty()); - m_uassignment.resize(next_idx); -} - -void old_tmp_type_context::set_next_mvar_idx(unsigned next_idx) { - lean_assert(m_eassignment.empty()); - lean_assert(m_scopes.empty()); - m_eassignment.resize(next_idx); -} - -bool old_tmp_type_context::is_uvar(level const & l) const { - return is_idx_metauniv(l); -} - -bool old_tmp_type_context::is_mvar(expr const & e) const { - return is_idx_metavar(e); -} - -optional old_tmp_type_context::get_assignment(level const & u) const { - unsigned idx = to_meta_idx(u); - // if the following assetion is violated, we have two options: - // 1- We should create the meta-variable using mk_uvar - // 2- We create using mk_idx_metauniv, and notify this object using - // set_next_uvar_idx - lean_assert(idx < m_uassignment.size()); - return m_uassignment[idx]; -} - -optional old_tmp_type_context::get_assignment(expr const & m) const { - unsigned idx = to_meta_idx(m); - // if the following assetion is violated, we have two options: - // 1- We should create the meta-variable using mk_mvar - // 2- We create using mk_idx_metavar, and notify this object using - // set_next_mvar_idx - lean_assert(idx < m_eassignment.size()); - return m_eassignment[idx]; -} - -void old_tmp_type_context::update_assignment(level const & u, level const & v) { - unsigned idx = to_meta_idx(u); - lean_assert(idx < m_uassignment.size()); // see comments above - lean_assert(!m_uassignment[idx]); - m_uassignment[idx] = v; - if (!m_scopes.empty()) - m_trail.emplace_back(trail_kind::Level, idx); -} - -void old_tmp_type_context::update_assignment(expr const & m, expr const & v) { - unsigned idx = to_meta_idx(m); - lean_assert(idx < m_eassignment.size()); // see comments above - // Remark: type class resolution may update an already assigned meta-variable with a - // definitionally equal, but the new assignment is "nicer", i.e., it has not been - // accidentally unfolded by the unifier. - // We only add the entry to the trail if it was not assigned before. - bool was_assigned = static_cast(m_eassignment[idx]); - m_eassignment[idx] = v; - if (!m_scopes.empty() && !was_assigned) - m_trail.emplace_back(trail_kind::Expr, idx); -} - -level old_tmp_type_context::mk_uvar() { - unsigned idx = m_uassignment.size(); - m_uassignment.push_back(none_level()); - return mk_idx_metauniv(idx); -} - -expr old_tmp_type_context::mk_mvar(expr const & type) { - unsigned idx = m_eassignment.size(); - m_eassignment.push_back(none_expr()); - return mk_idx_metavar(idx, type); -} - -void old_tmp_type_context::push_core() { - m_scopes.push_back(scope()); - scope & s = m_scopes.back(); - s.m_uassignment_sz = m_uassignment.size(); - s.m_eassignment_sz = m_eassignment.size(); - s.m_trail_sz = m_trail.size(); -} - -void old_tmp_type_context::pop_core() { - lean_assert(!m_scopes.empty()); - scope const & s = m_scopes.back(); - unsigned old_sz = s.m_trail_sz; - unsigned i = m_trail.size(); - while (i > old_sz) { - --i; - pair const & p = m_trail.back(); - switch (p.first) { - case trail_kind::Level: m_uassignment[p.second] = none_level(); break; - case trail_kind::Expr: m_eassignment[p.second] = none_expr(); break; - } - m_trail.pop_back(); - } - lean_assert(m_trail.size() == old_sz); - m_uassignment.resize(s.m_uassignment_sz); - m_eassignment.resize(s.m_eassignment_sz); - m_scopes.pop_back(); -} - -unsigned old_tmp_type_context::get_num_check_points() const { - return m_scopes.size(); -} - -void old_tmp_type_context::commit() { - lean_assert(!m_scopes.empty()); - m_scopes.pop_back(); -} -} diff --git a/src/library/old_tmp_type_context.h b/src/library/old_tmp_type_context.h deleted file mode 100644 index 3c4a4f4320..0000000000 --- a/src/library/old_tmp_type_context.h +++ /dev/null @@ -1,113 +0,0 @@ -/* -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 -#include "library/old_type_context.h" -#include "library/reducible.h" - -namespace lean { -/** \brief Type context for solving matching and simple unification problems. - It only supports meta-variables created with the module idx_metavar.h. - Internally, it stores the meta-variable assignments in an array. - So, it is assuming the metavariables have small indices. - - The assignment and backtracking stack can be reset using the clear method. - - \remark By default, this object assumes that non-reducible constants are opaque. - We can change that by providing a different reducible_behavior value when - creating the object. - - \remark The default implementations for infer_local(e) and - infer_metavar(e) just return mlocal_type(e). They must be - redefined if we want to use this class in modules that store the type - of local constants and meta-variables in a different place. - - \remark The local context is set using the method set_context from type_context. -*/ -class old_tmp_type_context : public old_type_context { - name_predicate m_opaque_pred; - std::vector> m_uassignment; - std::vector> m_eassignment; - enum class trail_kind { Level, Expr }; - std::vector> m_trail; // undo stack - struct scope { - unsigned m_old_next_local_idx; - unsigned m_uassignment_sz; - unsigned m_eassignment_sz; - unsigned m_trail_sz; - }; - std::vector m_scopes; - void init(environment const & env, reducible_behavior b); -public: - old_tmp_type_context(environment const & env, options const & o, reducible_behavior b = UnfoldReducible); - virtual ~old_tmp_type_context(); - - /** \brief Reset the state: backtracking stack, indices and assignment. */ - void clear(); - - /** \remark The following methods are useful when indexed meta-variables have been created outside - of this module. - \pre This method should only be invoked if not meta-variable has been created. - Use the method clear() to ensure this condition holds */ - void set_next_uvar_idx(unsigned next_idx); - - /** \remark The following methods are useful when indexed meta-variables have been created outside - of this module. - \pre This method should only be invoked if not meta-variable has been created. - Use the method clear() to ensure this condition holds */ - void set_next_mvar_idx(unsigned next_idx); - - virtual bool is_extra_opaque(name const & n) const { return m_opaque_pred(n); } - virtual bool is_uvar(level const & l) const; - virtual bool is_mvar(expr const & e) const; - virtual optional get_assignment(level const & u) const; - virtual optional get_assignment(expr const & m) const; - virtual void update_assignment(level const & u, level const & v); - virtual void update_assignment(expr const & m, expr const & v); - - virtual expr infer_local(expr const & e) const { return mlocal_type(e); } - virtual expr infer_metavar(expr const & e) const { return mlocal_type(e); } - - virtual level mk_uvar(); - virtual expr mk_mvar(expr const &); - - virtual void push_core(); - virtual void pop_core(); - virtual unsigned get_num_check_points() const; - virtual void commit(); - - bool is_uvar_assigned(unsigned idx) const { - lean_assert(idx < m_uassignment.size()); - return static_cast(m_uassignment[idx]); - } - - bool is_mvar_assigned(unsigned idx) const { - lean_assert(idx < m_eassignment.size()); - return static_cast(m_eassignment[idx]); - } -}; - -class old_tmp_type_context_pool { -public: - virtual old_tmp_type_context * mk_old_tmp_type_context() =0; - virtual void recycle_old_tmp_type_context(old_tmp_type_context * tmp_tctx) =0; - - virtual ~old_tmp_type_context_pool() {} -}; - -class default_old_tmp_type_context_pool : public old_tmp_type_context_pool { - environment m_env; - options m_options; -public: - default_old_tmp_type_context_pool(environment const & env, options const & o): - m_env(env), m_options(o) {} - - virtual old_tmp_type_context * mk_old_tmp_type_context() override { return new old_tmp_type_context(m_env, m_options); } - virtual void recycle_old_tmp_type_context(old_tmp_type_context * tmp_tctx) override { delete tmp_tctx; } -}; - -}