michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(library/elaborator): remove synthesizer

Browse source 
Synthesizer is not part of the elaborator anymore.
The elaborator fills the "easy" holes.
The remaining holes are filled using different techniques (e.g., tactic framework) that are independent of the elaborator.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-10 15:55:46 -08:00
parent bbaa83e16a
commit b270fb0030
5 changed files with 14 additions and 156 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

22
src/library/elaborator/elaborator.cpp
View file

@ -103,19 +103,6 @@ class elaborator::imp {
}
};
struct synthesizer_case_split : public case_split {
expr m_metavar;
lazy_list<expr> m_alternatives;
synthesizer_case_split(expr const & m, lazy_list<expr> const & r, state const & prev_state):
case_split(prev_state),
m_metavar(m),
m_alternatives(r) {
}
virtual ~synthesizer_case_split() {}
};
struct plugin_case_split : public case_split {
unification_constraint m_constraint;
std::unique_ptr<elaborator_plugin::result> m_alternatives;
@ -138,7 +125,6 @@ class elaborator::imp {
normalizer m_normalizer;
state m_state;
std::vector<std::unique_ptr<case_split>> m_case_splits;
std::shared_ptr<synthesizer> m_synthesizer;
std::shared_ptr<elaborator_plugin> m_plugin;
unsigned m_next_id;
int m_quota;
@ -1410,12 +1396,11 @@ class elaborator::imp {
public:
imp(environment const & env, metavar_env const & menv, unsigned num_cnstrs, unification_constraint const * cnstrs,
options const & opts, std::shared_ptr<synthesizer> const & s, std::shared_ptr<elaborator_plugin> const & p):
options const & opts, std::shared_ptr<elaborator_plugin> const & p):
m_env(env),
m_type_inferer(env),
m_normalizer(env),
m_state(menv, num_cnstrs, cnstrs),
m_synthesizer(s),
m_plugin(p) {
set_options(opts);
m_next_id = 0;
@ -1446,7 +1431,7 @@ public:
check_interrupted();
cnstr_queue & q = m_state.m_queue;
if (q.empty() || m_quota < - static_cast<int>(q.size()) - 10) {
// TODO(Leo): implement interface with synthesizer
// TODO(Leo): improve exit condition
return m_state.m_menv;
} else {
unification_constraint c = q.front();
@ -1478,9 +1463,8 @@ elaborator::elaborator(environment const & env,
unsigned num_cnstrs,
unification_constraint const * cnstrs,
options const & opts,
std::shared_ptr<synthesizer> const & s,
std::shared_ptr<elaborator_plugin> const & p):
m_ptr(new imp(env, menv, num_cnstrs, cnstrs, opts, s, p)) {
m_ptr(new imp(env, menv, num_cnstrs, cnstrs, opts, p)) {
}
elaborator::elaborator(environment const & env,

26
src/library/elaborator/elaborator.h
View file

@ -11,24 +11,22 @@ Author: Leonardo de Moura
#include "kernel/metavar.h"
#include "kernel/unification_constraint.h"
#include "library/elaborator/elaborator_plugin.h"
#include "library/elaborator/synthesizer.h"
#include "library/elaborator/elaborator_exception.h"
namespace lean {
/**
\brief Elaborator is the main object used to fill "holes" in Lean.
\brief Elaborator fills "holes" in Lean using unification based
method. This is essentially a generalizationof the ML type inference
algorithm.
Each hole is represented using a metavariable. This object is
responsible for solving the easy "holes" and invoking external
plugins/synthesizers for filling the other ones. It is also
responsible for managing the search space (i.e., managing the
backtracking search).
plugins for filling the other ones. It is also responsible for
managing the search space (i.e., managing the backtracking search).
The elaborator can be customized using:
1) Elaborator plugins. They are invoked whenever the elaborator
does not know how to solve a unification constraint.
2) Synthesizers. They are invoked whenever the elaborator does not
have unification constraints for inferring a particular hole.
The elaborator can be customized using plugins that are invoked
whenever the elaborator does not know how to solve a unification
constraint.
The result is a sequence of substitutions. Each substitution
represents a different way of filling the holes.
@ -43,16 +41,14 @@ public:
unsigned num_cnstrs,
unification_constraint const * cnstrs,
options const & opts = options(),
std::shared_ptr<synthesizer> const & s = std::shared_ptr<synthesizer>(),
std::shared_ptr<elaborator_plugin> const & p = std::shared_ptr<elaborator_plugin>());
elaborator(environment const & env,
metavar_env const & menv,
std::initializer_list<unification_constraint> const & cnstrs,
options const & opts = options(),
std::shared_ptr<synthesizer> const & s = std::shared_ptr<synthesizer>(),
std::shared_ptr<elaborator_plugin> const & p = std::shared_ptr<elaborator_plugin>()):
elaborator(env, menv, cnstrs.size(), cnstrs.begin(), opts, s, p) {}
elaborator(env, menv, cnstrs.size(), cnstrs.begin(), opts, p) {}
elaborator(environment const & env,
metavar_env const & menv,

45
src/library/elaborator/elaborator_justification.cpp
View file

@ -97,51 +97,6 @@ void typeof_mvar_justification::get_children(buffer<justification_cell*> & r) co
push_back(r, m_justification);
}
// -------------------------
// Synthesis justification objects
// -------------------------
synthesis_justification::synthesis_justification(context const & ctx, expr const & mvar, expr const & type, unsigned num, justification const * substs):
m_context(ctx),
m_mvar(mvar),
m_type(type),
m_substitution_justifications(substs, substs + num) {
}
synthesis_justification::~synthesis_justification() {
}
format synthesis_justification::pp_header(formatter const & fmt, options const & opts) const {
format r;
r += format(get_label());
r += space();
r += fmt(m_context, m_mvar, false, opts);
unsigned indent = get_pp_indent(opts);
r += nest(indent, compose(line(), fmt(m_context, m_type, true, opts)));
return r;
}
void synthesis_justification::get_children(buffer<justification_cell*> & r) const {
append(r, m_substitution_justifications);
}
optional<expr> synthesis_justification::get_main_expr() const {
return some_expr(m_mvar);
}
char const * synthesis_failure_justification::get_label() const {
return "Failed to synthesize expression of type for";
}
synthesis_failure_justification::synthesis_failure_justification(context const & ctx, expr const & mvar, expr const & type, justification const & tr, unsigned num, justification const * substs):
synthesis_justification(ctx, mvar, type, num, substs),
m_justification(tr) {
}
synthesis_failure_justification::~synthesis_failure_justification() {
}
void synthesis_failure_justification::get_children(buffer<justification_cell*> & r) const {
synthesis_justification::get_children(r);
push_back(r, m_justification);
}
char const * synthesized_assignment_justification::get_label() const {
return "Synthesized assignment for";
}
// -------------------------
// Next solution justification
// -------------------------

49
src/library/elaborator/elaborator_justification.h
View file

@ -153,55 +153,6 @@ public:
virtual void get_children(buffer<justification_cell*> & r) const;
};
/**
\brief Base class for synthesis_failure_justification and synthesized_assignment_justification
*/
class synthesis_justification : public justification_cell {
context m_context;
expr m_mvar;
expr m_type;
std::vector<justification> m_substitution_justifications; // justification objects justifying the assignments used to instantiate \c m_type and \c m_context.
protected:
virtual char const * get_label() const = 0;
public:
synthesis_justification(context const & ctx, expr const & mvar, expr const & type, unsigned num, justification const * substs);
virtual ~synthesis_justification();
virtual format pp_header(formatter const &, options const &) const;
virtual void get_children(buffer<justification_cell*> & r) const;
virtual optional<expr> get_main_expr() const;
};
/**
\brief Justification object for justifying why a synthesis step failed.
A synthesis step is of the form
<tt>ctx |- ?mvar : type</tt>
Before invoking the synthesizer, the elaborator substitutes the
metavariables in \c ctx and \c type with their corresponding assignments.
*/
class synthesis_failure_justification : public synthesis_justification {
justification m_justification; // justification object produced by the synthesizer
protected:
virtual char const * get_label() const;
public:
synthesis_failure_justification(context const & ctx, expr const & mvar, expr const & type, justification const & tr, unsigned num, justification const * substs);
virtual ~synthesis_failure_justification();
virtual void get_children(buffer<justification_cell*> & r) const;
};
/**
\brief Justification object used to justify a metavar assignment produced by a synthesizer.
*/
class synthesized_assignment_justification : public synthesis_justification {
protected:
virtual char const * get_label() const;
public:
synthesized_assignment_justification(context const & ctx, expr const & mvar, expr const & type, unsigned num, justification const * substs):
synthesis_justification(ctx, mvar, type, num, substs) {
}
};
/**
\brief Justification object used to justify that we are moving to the next solution.
*/

28
src/library/elaborator/synthesizer.h
View file

@ -1,28 +0,0 @@
/*
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include <memory>
#include "util/lazy_list.h"
#include "kernel/environment.h"
#include "kernel/context.h"
#include "library/elaborator/elaborator_exception.h"
namespace lean {
/**
\brief A synthesizer generates a sequence of expressions of a given type.
*/
class synthesizer {
public:
virtual ~synthesizer() {}
/**
\brief Return a sequence of expressions
of type \c type in the given environment and context.
*/
virtual lazy_list<expr> operator()(environment const & env, context const & ctx, expr const & type) = 0;
};
}