max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(library): remove old unifier

Browse source
This commit is contained in:
Leonardo de Moura 2016-09-19 17:18:47 -07:00
parent c66dbf202b
commit d2b400ac2c
8 changed files with 1 additions and 3008 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/api/exception.cpp
View file

@ -6,7 +6,6 @@ Author: Leonardo de Moura
*/
#include "kernel/kernel_exception.h"
#include "kernel/type_checker.h"
#include "library/unifier.h"
#include "library/print.h"
#include "library/error_handling.h"
#include "api/exception.h"
@ -73,10 +72,6 @@ lean_exception_kind lean_exception_get_kind(lean_exception e) {
return LEAN_KERNEL_EXCEPTION;
if (dynamic_cast<lean::interrupted*>(ex))
return LEAN_INTERRUPTED;
if (dynamic_cast<lean::unifier_exception*>(ex))
return LEAN_UNIFIER_EXCEPTION;
// if (dynamic_cast<lean::tactic_exception*>(ex))
// return LEAN_TACTIC_EXCEPTION;
if (dynamic_cast<lean::parser_exception*>(ex))
return LEAN_PARSER_EXCEPTION;
return LEAN_OTHER_EXCEPTION;

2
src/api/lean_exception.h
View file

@ -49,8 +49,6 @@ typedef enum {
LEAN_OUT_OF_MEMORY, // out of memory exception
LEAN_INTERRUPTED, // execution was interrupted by user request
LEAN_KERNEL_EXCEPTION, // type checking error
LEAN_UNIFIER_EXCEPTION, // unification exception
LEAN_TACTIC_EXCEPTION, // tactic exception
LEAN_PARSER_EXCEPTION, // parser exception
LEAN_OTHER_EXCEPTION // other (TODO) lean exceptions
} lean_exception_kind;

1
src/frontends/lean/server.cpp
View file

@ -15,7 +15,6 @@ Author: Leonardo de Moura
#include "util/bitap_fuzzy_search.h"
#include "kernel/instantiate.h"
#include "library/aliases.h"
#include "library/unifier.h"
#include "library/protected.h"
#include "library/reducible.h"
#include "library/projection.h"

2
src/library/CMakeLists.txt
View file

@ -19,7 +19,7 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp
# Legacy -- The following files will be eventually deleted
normalize.cpp justification.cpp constraint.cpp metavar.cpp choice.cpp locals.cpp
unifier.cpp class_instance_resolution.cpp old_type_context.cpp
class_instance_resolution.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

11
src/library/error_handling.cpp
View file

@ -10,7 +10,6 @@ Author: Leonardo de Moura
#include "kernel/ext_exception.h"
#include "kernel/for_each_fn.h"
#include "library/io_state_stream.h"
#include "library/unifier.h"
#include "library/exception.h"
#include "library/flycheck.h"
#include "library/pp_options.h"
@ -129,14 +128,6 @@ static void display_error_warning(bool is_error, io_state_stream const & ios, po
ios << " " << ex << endl;
}
static void display_error_warning(bool is_error, io_state_stream const & ios, pos_info_provider const * p, unifier_exception const & ex) {
formatter fmt = ios.get_formatter();
options opts = ios.get_options();
auto j = ex.get_justification();
display_error_warning_pos(is_error, ios, p, j.get_main_expr());
ios << " " << mk_pair(j.pp(fmt, p, ex.get_substitution()), opts) << endl;
}
static void display_error_warning(bool is_error, io_state_stream const & ios, pos_info_provider const * p, formatted_exception const & ex) {
display_error_warning_pos(is_error, ios, p, ex.get_main_expr());
ios << " " << ex << endl;
@ -148,8 +139,6 @@ static void display_error_warning(bool is_error, io_state_stream const & ios, po
display_error_warning(is_error, ios, p, *k_ex);
} else if (auto f_ex = dynamic_cast<formatted_exception const *>(&ex)) {
display_error_warning(is_error, ios, p, *f_ex);
} else if (auto e_ex = dynamic_cast<unifier_exception const *>(&ex)) {
display_error_warning(is_error, ios, p, *e_ex);
} else if (p) {
display_error_warning_pos(is_error, ios, p->get_file_name(), p->get_some_pos().first, p->get_some_pos().second);
ios << " " << ex.what() << endl;

3
src/library/init_module.cpp
View file

@ -6,7 +6,6 @@ Author: Leonardo de Moura
*/
#include "library/trace.h"
#include "library/constants.h"
#include "library/unifier.h"
#include "library/kernel_serializer.h"
#include "library/typed_expr.h"
#include "library/choice.h"
@ -93,7 +92,6 @@ void initialize_library_module() {
initialize_placeholder();
initialize_idx_metavar();
initialize_io_state();
initialize_unifier();
initialize_kernel_serializer();
initialize_typed_expr();
initialize_choice();
@ -171,7 +169,6 @@ void finalize_library_module() {
finalize_choice();
finalize_typed_expr();
finalize_kernel_serializer();
finalize_unifier();
finalize_io_state();
finalize_idx_metavar();
finalize_placeholder();

2864
src/library/unifier.cpp
View file

File diff suppressed because it is too large Load diff

121
src/library/unifier.h
View file

@ -1,121 +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 <utility>
#include <functional>
#include "util/lazy_list.h"
#include "util/sexpr/options.h"
#include "kernel/environment.h"
#include "library/metavar.h"
#include "library/constraint.h"
namespace lean {
unsigned get_unifier_max_steps(options const & opts);
bool is_simple_meta(expr const & e);
expr mk_aux_metavar_for(expr const & t);
enum class unify_status { Solved, Failed, Unsupported };
/**
\brief Handle the easy-cases: first-order unification, higher-order patterns, identical terms, and terms without metavariables.
This function assumes that all assigned metavariables have been substituted.
*/
unify_status unify_simple(substitution & s, expr const & lhs, expr const & rhs, justification const & j);
unify_status unify_simple(substitution & s, level const & lhs, level const & rhs, justification const & j);
unify_status unify_simple(substitution & s, constraint const & c);
enum class unifier_kind { Cheap, Conservative, Liberal };
struct unifier_config {
bool m_use_exceptions;
unsigned m_max_steps;
unsigned m_normalizer_max_steps;
bool m_expensive_classes;
// If m_discard is true, then constraints that cannot be solved are discarded (or incomplete methods are used)
// If m_discard is false, unify returns the set of constraints that could not be handled.
bool m_discard;
// If m_mind == Conservative, then the following restrictions are imposed:
// - All constants that are not at least marked as Semireducible are treated as
// opaque.
// - Disables case-split on delta-delta constraints.
// - Disables reduction case-split on flex-rigid constraints.
//
// If m_kind == Cheap is true, then expensive case-analysis is not performed (e.g., delta).
// It is more restrictive than VeryConservative
//
// Default is Liberal
unifier_kind m_kind;
// If m_pattern is true, then we restrict the number of cases splits on
// flex-rigid constraints that are *not* in the higher-order pattern case.
bool m_pattern;
// If m_ignore_context_check == true, then occurs-check is skipped.
// Default is m_ignore_context_check == false
bool m_ignore_context_check;
// If m_nonchronological is true, then nonchronological backtracking is used in the unifier.
// Default is true
bool m_nonchronological;
unifier_config(bool use_exceptions = false, bool discard = false);
explicit unifier_config(options const & o, bool use_exceptions = false, bool discard = false);
};
/** \brief The unification procedures produce a lazy list of pair substitution + constraints that could not be solved. */
typedef lazy_list<pair<substitution, constraints>> unify_result_seq;
unify_result_seq unify(environment const & env, unsigned num_cs, constraint const * cs,
substitution const & s = substitution(), unifier_config const & c = unifier_config());
unify_result_seq unify(environment const & env, expr const & lhs, expr const & rhs,
substitution const & s = substitution(), unifier_config const & c = unifier_config());
/**
The unifier divides the constraints in 9 groups: Simple, Basic, FlexRigid, PluginDelayed, DelayedChoice, ClassInstance,
Epilogue, FlexFlex, MaxDelayed
1) Simple: constraints that never create case-splits. Example: pattern matching constraints (?M l_1 ... l_n) =?= t.
The are not even inserted in the constraint priority queue.
2) Basic: contains user choice constraints used to model coercions and overloaded constraints, and constraints
that cannot be solved, and the unification plugin must be invoked.
3) FlexRigid constraints (?M t_1 ... t_n) =?= t, where t_n is not an introduction application
4) PluginDelayed: contraints delayed by the unifier_plugin. Examples: (elim ... (?m ...)) and (?m ... (intro ...)),
where elim is an eliminator/recursor and intro is an introduction/constructor.
This constraints are delayed because after ?m is assigned we may be able to reduce them.
5) DelayedChoice: for delayed choice constraints (we use this group for the maximally delayed coercions constraints).
6) ClassInstance: for delayed choice constraints (we use this group for class-instance).
7) Epilogue: constraints that must be solved before FlexFlex are discarded/postponed.
8) Checkpoint: unifier performs a prolog-like cut for any constraint in this group.
9) FlexFlex: (?m1 ...) =?= (?m2 ...) we don't try to solve this constraint, we delay them and hope the other
ones instantiate ?m1 or ?m2. If this kind of constraint is the next to be processed in the queue, then
we simply discard it (or save it and return to the caller as residue).
10) MaxDelayed: maximally delayed constraint group
*/
enum class cnstr_group { Basic = 0, FlexRigid, PluginDelayed, DelayedChoice, ClassInstance,
Epilogue, Checkpoint, FlexFlex, MaxDelayed };
inline unsigned to_delay_factor(cnstr_group g) { return static_cast<unsigned>(g); }
class unifier_exception : public exception {
justification m_jst;
substitution m_subst;
public:
unifier_exception(justification const & j, substitution const & s):exception("unifier exception"), m_jst(j), m_subst(s) {}
virtual throwable * clone() const { return new unifier_exception(m_jst, m_subst); }
virtual void rethrow() const { throw *this; }
justification const & get_justification() const { return m_jst; }
substitution const & get_substitution() const { return m_subst; }
};
void initialize_unifier();
void finalize_unifier();
}