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

chore(library/equations_compiler): remove old equation compiler

Browse source
This commit is contained in:
Leonardo de Moura 2016-09-19 17:13:30 -07:00
parent f6aba503ff
commit c66dbf202b
8 changed files with 2 additions and 3020 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/frontends/lean/CMakeLists.txt
View file

@ -9,10 +9,4 @@ type_util.cpp local_ref_info.cpp decl_attributes.cpp nested_declaration.cpp
opt_cmd.cpp prenum.cpp print_cmd.cpp elaborator.cpp
match_expr.cpp local_context_adapter.cpp decl_util.cpp definition_cmds.cpp
# LEGACY
old_attributes.cpp
# begin_end_annotation.cpp tactic_hint.cpp
# info_tactic.cpp
# parse_tactic_location.cpp parse_rewrite_tactic.cpp builtin_tactics.cpp
# parse_with_options_tactic.cpp
#parse_with_attributes_tactic.cpp
)
old_attributes.cpp)

4
src/library/equations_compiler/CMakeLists.txt
View file

@ -1,6 +1,4 @@
add_library(equations_compiler OBJECT
equations.cpp util.cpp pack_domain.cpp
structural_rec.cpp unbounded_rec.cpp
elim_match.cpp compiler.cpp init_module.cpp
#LEGACY
old_compiler.cpp old_goal.cpp old_inversion.cpp)
elim_match.cpp compiler.cpp init_module.cpp)

1539
src/library/equations_compiler/old_compiler.cpp
View file

File diff suppressed because it is too large Load diff

12
src/library/equations_compiler/old_compiler.h
View file

@ -1,12 +0,0 @@
/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "library/equations_compiler/equations.h"
namespace lean {
expr compile_equations(old_type_checker & tc, io_state const & ios, expr const & eqns,
expr const & meta, expr const & meta_type);
}

182
src/library/equations_compiler/old_goal.cpp
View file

@ -1,182 +0,0 @@
/*
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <utility>
#include <algorithm>
#include "util/buffer.h"
#include "util/sstream.h"
#include "util/sexpr/option_declarations.h"
#include "kernel/replace_fn.h"
#include "kernel/for_each_fn.h"
#include "kernel/abstract.h"
#include "kernel/type_checker.h"
#include "library/metavar.h"
#include "library/util.h"
#include "library/old_util.h"
#include "library/equations_compiler/old_goal.h"
namespace lean {
old_local_context old_goal::to_local_context() const {
buffer<expr> hyps;
get_hyps(hyps);
std::reverse(hyps.begin(), hyps.end());
return old_local_context(to_list(hyps));
}
format old_goal::pp(formatter const & fmt) const {
return pp(fmt, substitution());
}
format old_goal::pp(formatter const & fmt, substitution const & s) const {
buffer<expr> hyps;
get_app_args(m_meta, hyps);
return format_goal(fmt, hyps, m_type, s);
}
expr old_goal::abstract(expr const & v) const {
buffer<expr> locals;
get_app_args(m_meta, locals);
return Fun(locals, v);
}
expr old_goal::mk_meta(name const & n, expr const & type) const {
buffer<expr> locals;
expr this_mvar = get_app_args(m_meta, locals);
expr mvar = copy_tag(this_mvar, mk_metavar(n, Pi(locals, type)));
return copy_tag(m_meta, mk_app(mvar, locals));
}
old_goal old_goal::instantiate(substitution const & s) const {
substitution s1(s);
return old_goal(s1.instantiate_all(m_meta), s1.instantiate_all(m_type));
}
static bool validate_locals(expr const & r, unsigned num_locals, expr const * locals) {
bool failed = false;
for_each(r, [&](expr const & e, unsigned) {
if (!has_local(e) || failed) return false;
if (is_local(e) &&
!std::any_of(locals, locals + num_locals,
[&](expr const & l) { return mlocal_name(l) == mlocal_name(e); })) {
failed = true;
return false;
}
return true;
});
return !failed;
}
bool old_goal::validate_locals() const {
buffer<expr> locals;
get_app_args(m_meta, locals);
if (!::lean::validate_locals(m_type, locals.size(), locals.data()))
return false;
unsigned i = locals.size();
while (i > 0) {
--i;
if (!::lean::validate_locals(mlocal_type(locals[i]), i, locals.data()))
return false;
}
return true;
}
bool old_goal::validate(environment const & env) const {
if (validate_locals()) {
old_type_checker tc(env);
return tc.is_def_eq(tc.check(m_meta).first, m_type).first;
} else {
return false;
}
}
list<expr> old_goal::to_context() const {
buffer<expr> locals;
get_app_rev_args(m_meta, locals);
return to_list(locals.begin(), locals.end());
}
template<typename F>
static optional<pair<expr, unsigned>> find_hyp_core(expr const & meta, F && pred) {
expr const * it = &meta;
unsigned i = 0;
while (is_app(*it)) {
expr const & h = app_arg(*it);
if (pred(h))
return some(mk_pair(h, i));
i++;
it = &app_fn(*it);
}
return optional<pair<expr, unsigned>>();
}
optional<pair<expr, unsigned>> old_goal::find_hyp(name const & uname) const {
return find_hyp_core(m_meta, [&](expr const & h) { return local_pp_name(h) == uname; });
}
optional<pair<expr, unsigned>> old_goal::find_hyp_from_internal_name(name const & n) const {
return find_hyp_core(m_meta, [&](expr const & h) { return mlocal_name(h) == n; });
}
void old_goal::get_hyps(buffer<expr> & r) const {
get_app_args(m_meta, r);
}
void assign(substitution & s, old_goal const & g, expr const & v) {
buffer<expr> hyps;
expr const & mvar = get_app_args(g.get_meta(), hyps);
s.assign(mvar, hyps, v);
}
static bool uses_name(name const & n, buffer<expr> const & locals) {
for (expr const & local : locals) {
if (is_local(local) && local_pp_name(local) == n)
return true;
}
return false;
}
name get_unused_name(name const & prefix, unsigned & idx, buffer<expr> const & locals) {
while (true) {
name curr = prefix.append_after(idx);
idx++;
if (!uses_name(curr, locals))
return curr;
}
}
name get_unused_name(name const & prefix, buffer<expr> const & locals) {
if (!uses_name(prefix, locals))
return prefix;
unsigned idx = 1;
return get_unused_name(prefix, idx, locals);
}
name get_unused_name(name const & prefix, unsigned & idx, expr const & meta) {
buffer<expr> locals;
get_app_rev_args(meta, locals);
return get_unused_name(prefix, idx, locals);
}
name get_unused_name(name const & prefix, expr const & meta) {
buffer<expr> locals;
get_app_rev_args(meta, locals);
return get_unused_name(prefix, locals);
}
name old_goal::get_unused_name(name const & prefix, unsigned & idx) const {
return ::lean::get_unused_name(prefix, idx, m_meta);
}
name old_goal::get_unused_name(name const & prefix) const {
return ::lean::get_unused_name(prefix, m_meta);
}
io_state_stream const & operator<<(io_state_stream const & out, old_goal const & g) {
options const & opts = out.get_options();
out.get_stream() << mk_pair(g.pp(out.get_formatter()), opts);
return out;
}
}

113
src/library/equations_compiler/old_goal.h
View file

@ -1,113 +0,0 @@
/*
Copyright (c) 2016 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 "util/list.h"
#include "util/name.h"
#include "kernel/formatter.h"
#include "kernel/environment.h"
#include "library/io_state_stream.h"
#include "library/old_local_context.h"
namespace lean {
/**
\brief A goal is just encoding the synthesis problem <tt>(?m l_1 .... l_n) : t</tt>
That is, we want to find a term \c ?m s.t. <tt>(?m l_1 ... l_n)</tt> has type \c t
The terms \c l_i are just local constants.
We can convert any metavariable
<tt>?m : Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), B[x_1, ..., x_n]</tt>
into a goal by simply creating the local constants
<tt>l_1 : A_1, ..., l_n : A_n[l_1, ..., l_{n-1}]</tt>
and then, create the goal
<tt>?m l_1 ... l_n : B[l_1, ..., l_n]</tt>
Now, suppose we find a term \c b with type <tt>B[l_1, ... l_n]</tt>, then we can simply
find \c ?m by abstracting <tt>l_1, ..., l_n</tt>
We can check whether a goal is well formed in an environment by type checking.
*/
class old_goal {
expr m_meta;
expr m_type;
public:
old_goal() {}
old_goal(expr const & m, expr const & t):m_meta(m), m_type(t) {}
expr const & get_meta() const { return m_meta; }
expr const & get_type() const { return m_type; }
name get_name() const { return mlocal_name(get_app_fn(m_meta)); }
expr get_mvar() const { return get_app_fn(m_meta); }
/** \brief Given a term \c v with type get_type(), build a lambda abstraction
that is the solution for the metavariable associated with this old_goal.
*/
expr abstract(expr const & v) const;
/** \brief Create a metavariable application <tt>(?m l_1 ... l_n)</tt> with the given type,
and the locals from this old_goal.
*/
expr mk_meta(name const & m, expr const & type) const;
/** \brief Return true iff get_type() only contains local constants that arguments
of get_meta(), and each argument of get_meta() only contains local constants
that are previous arguments.
*/
bool validate_locals() const;
/** \brief Return true iff \c validate_locals() return true and type of \c get_meta() in
\c env is get_type()
*/
bool validate(environment const & env) const;
/** \brief Return the old_goal's "context".
That is, given <tt>?m l_1 ... l_n</tt>, return the list
<tt>[l_n, ..., l_1]</tt>
*/
list<expr> to_context() const;
old_local_context to_local_context() const;
/** \brief Apply given substitution to old_goal */
old_goal instantiate(substitution const & s) const;
/** \brief Return hypothesis (and its position) with "user name" uname (i.e., local_pp_name).
\remark The position is right to left. In the following old_goal (Ha is 2), (Hb is 1) and (Hc is 0):
Ha : a, Hb : b, Hc : c |- P
*/
optional<pair<expr, unsigned>> find_hyp(name const & uname) const;
/** \brief Similar to find_hyp but use internal name */
optional<pair<expr, unsigned>> find_hyp_from_internal_name(name const & hname) const;
/** \brief Store hypotheses in the given buffer.
\remark The hypotheses are stored from left to right.
*/
void get_hyps(buffer<expr> & r) const;
/** \brief Return a "user" name that is not used by any local constant in the given old_goal */
name get_unused_name(name const & prefix, unsigned & idx) const;
name get_unused_name(name const & prefix) const;
format pp(formatter const & fmt, substitution const & s) const;
format pp(formatter const & fmt) const;
};
void assign(substitution & s, old_goal const & g, expr const & v);
name get_unused_name(name const & prefix, unsigned & idx, buffer<expr> const & locals);
name get_unused_name(name const & prefix, buffer<expr> const & locals);
name get_unused_name(name const & prefix, unsigned & idx, expr const & meta);
name get_unused_name(name const & prefix, expr const & meta);
io_state_stream const & operator<<(io_state_stream const & out, old_goal const & g);
}

1102
src/library/equations_compiler/old_inversion.cpp
View file

File diff suppressed because it is too large Load diff

62
src/library/equations_compiler/old_inversion.h
View file

@ -1,62 +0,0 @@
/*
Copyright (c) 2016 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/expr.h"
#include "library/metavar.h"
#include "library/equations_compiler/old_goal.h"
namespace lean {
namespace inversion {
/**
\brief When we apply the inversion tactic/procedure on a hypothesis (h : I A j), where
I is an inductive datatpe, the hypothesis is "broken" into cases: one for each constructor.
Some cases may be in conflict with the type (I A j) and may be suppressed.
Example of conflict: given the vector type
inductive vector (A : Type) : nat → Type :=
nil {} : vector A zero,
cons : Π {n : nat}, A → vector A n → vector A (succ n)
Then, (h : vector A (succ n)) is in conflict with constructor nil.
The user may provide possible implementations (example: in the form of equations).
Each possible implementation is associated with a case/constructor.
The inversion tactic/procedure distributes the implementations over cases.
The implementations may depend on hypotheses that may be modifed by the inversion procedure.
The method update_exprs of each implementation is invoked to update the expressions of
a given implementation.
*/
class implementation {
public:
virtual ~implementation() {}
virtual name const & get_constructor_name() const = 0;
virtual void update_exprs(std::function<expr(expr const &)> const & fn) = 0;
};
typedef std::shared_ptr<implementation> implementation_ptr;
typedef list<implementation_ptr> implementation_list;
struct result {
list<old_goal> m_goals;
list<list<expr>> m_args; // arguments of the constructor/intro rule
list<implementation_list> m_implementation_lists;
list<rename_map> m_renames;
// invariant: length(m_goals) == length(m_args);
// invariant: length(m_goals) == length(m_implementation_lists);
// invariant: length(m_goals) == length(m_renames);
substitution m_subst;
result(list<old_goal> const & gs, list<list<expr>> const & args, list<implementation_list> const & imps,
list<rename_map> const & rs, substitution const & subst);
};
optional<result> apply(environment const & env, io_state const & ios, old_type_checker & tc,
old_goal const & g, expr const & h, implementation_list const & imps,
bool clear_elim);
}
}