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

Add support for overloads in the elaborator

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-09-01 14:52:17 -07:00
parent a3bbd9fbb5
commit d27680d7fc
4 changed files with 105 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

72
src/library/elaborator.cpp
View file

@ -6,6 +6,7 @@ Author: Leonardo de Moura
*/
#include <deque>
#include "elaborator.h"
#include "normalize.h"
#include "metavar.h"
#include "printer.h"
#include "context.h"
@ -83,6 +84,8 @@ class elaborator::imp {
constraint_queue m_constraints;
metavars m_metavars;
normalizer m_normalizer;
bool m_add_constraints;
// The following mapping is used to store the relationship
@ -177,12 +180,57 @@ class elaborator::imp {
}
}
bool is_convertible(expr const & t1, expr const & t2, context const & ctx) {
return m_normalizer.is_convertible(t1, t2, ctx);
}
void add_constraint(expr const & t1, expr const & t2, context const & ctx, expr const & s, unsigned arg_pos) {
if (has_metavar(t1) || has_metavar(t2)) {
m_constraints.push_back(constraint(t1, t2, ctx, s, ctx, arg_pos));
}
}
void choose(buffer<expr> const & f_choices, buffer<expr> const & f_choice_types,
buffer<expr> & args, buffer<expr> & types,
context const & ctx, expr const & src) {
lean_assert(f_choices.size() == f_choice_types.size());
buffer<unsigned> good_choices;
unsigned num_choices = f_choices.size();
unsigned num_args = args.size();
for (unsigned j = 0; j < num_choices; j++) {
expr f_t = f_choice_types[j];
try {
unsigned i = 1;
for (; i < num_args; i++) {
f_t = check_pi(f_t, ctx, src, ctx);
expr const & expected = abst_domain(f_t);
if (!has_metavar(expected) && !has_metavar(types[i])) {
if (!is_convertible(expected, types[i], ctx)) {
break;
}
}
f_t = instantiate_free_var_mmv(abst_body(f_t), 0, args[i]);
}
if (i == num_args) {
good_choices.push_back(j);
}
} catch (exception & ex) {
// candidate failed
// do nothing
}
}
if (good_choices.size() == 0) {
// TODO add information to the exception
throw exception("none of the overloads are good");
} else if (good_choices.size() == 1) {
args[0] = f_choices[good_choices[0]];
types[0] = f_choice_types[good_choices[0]];
} else {
// TODO add information to the exception
throw exception("ambiguous overload");
}
}
typedef std::pair<expr, expr> expr_pair;
/**
@ -247,7 +295,10 @@ class elaborator::imp {
args.push_back(p.first);
types.push_back(p.second);
}
// TODO: choose an f from f_choices
if (!f_choices.empty()) {
// choose one of the functions (overloads) based on the types in types
choose(f_choices, f_choice_types, args, types, ctx, e);
}
expr f_t = types[0];
for (unsigned i = 1; i < num; i++) {
f_t = check_pi(f_t, ctx, e, ctx);
@ -589,17 +640,20 @@ class elaborator::imp {
public:
imp(environment const & env, name_set const * defs):
m_env(env),
m_available_defs(defs) {
m_available_defs(defs),
m_normalizer(env) {
m_interrupted = false;
m_owner = nullptr;
}
void clear() {
m_trace.clear();
m_normalizer.clear();
}
void set_interrupt(bool flag) {
m_interrupted = flag;
m_normalizer.set_interrupt(flag);
}
void display(std::ostream & out) {
@ -625,16 +679,16 @@ public:
}
expr operator()(expr const & e, elaborator const & elb) {
if (has_placeholder(e)) {
m_constraints.clear();
m_metavars.clear();
m_owner = &elb;
m_add_constraints = true;
m_root = process(e, context()).first;
m_constraints.clear();
m_metavars.clear();
m_owner = &elb;
m_add_constraints = true;
m_root = process(e, context()).first;
if (has_metavar(m_root)) {
solve();
return instantiate(m_root);
} else {
return e;
return m_root;
}
}

26
src/library/metavar.cpp
View file

@ -307,6 +307,15 @@ expr instantiate_metavar(expr const & a, unsigned midx, expr const & v) {
return replace_fn<decltype(f)>(f)(a);
}
static expr get_def_value(name const & n, environment const & env, name_set const * defs) {
if (defs == nullptr || defs->find(n) != defs->end()) {
object const & obj = env.find_object(n);
if (obj && obj.is_definition() && !obj.is_opaque())
return obj.get_value();
}
return expr();
}
expr head_reduce_mmv(expr const & e, environment const & env, name_set const * defs) {
if (is_app(e) && is_lambda(arg(e, 0))) {
expr r = arg(e,0);
@ -326,15 +335,20 @@ expr head_reduce_mmv(expr const & e, environment const & env, name_set const * d
r = mk_app(args.size(), args.data());
}
return r;
} else if (is_app(e) && is_constant(arg(e, 0))) {
expr def = get_def_value(const_name(arg(e, 0)), env, defs);
if (def) {
buffer<expr> new_args;
new_args.push_back(def);
new_args.append(num_args(e)-1, &arg(e,1));
return mk_app(new_args.size(), new_args.data());
}
} else if (is_let(e)) {
return instantiate_free_var_mmv(let_body(e), 0, let_value(e));
} else if (is_constant(e)) {
name const & n = const_name(e);
if (defs == nullptr || defs->find(n) != defs->end()) {
object const & obj = env.find_object(n);
if (obj && obj.is_definition() && !obj.is_opaque())
return obj.get_value();
}
expr def = get_def_value(const_name(e), env, defs);
if (def)
return def;
}
return e;
}

12
tests/lean/overload1.lean Normal file
View file

@ -0,0 +1,12 @@
Variable N : Type
Variable f : Bool -> Bool -> Bool
Variable g : N -> N -> N
Infixl 10 ++ : f
Infixl 10 ++ : g
Show true ++ false ++ true
Set lean::pp::notation false
Show true ++ false ++ true
Variable a : N
Variable b : N
Show a ++ b ++ a
Show true ++ false ++ false

10
tests/lean/overload1.lean.expected.out Normal file
View file

@ -0,0 +1,10 @@
Assumed: N
Assumed: f
Assumed: g
⊤ ++ ⊥ ++ ⊤
Set option: lean::pp::notation
f (f true false) true
Assumed: a
Assumed: b
g (g a b) a
f (f true false) false