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

Add coercion support in the elaborator and pretty printer

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-09-01 19:08:49 -07:00
parent e8c09015ad
commit c97e669f0c
9 changed files with 134 additions and 37 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

50
src/frontends/lean/lean_elaborator.cpp
View file

@ -90,7 +90,7 @@ class elaborator::imp {
normalizer m_normalizer;
bool m_add_constraints;
bool m_processing_root;
// The following mapping is used to store the relationship
// between elaborated expressions and non-elaborated expressions.
@ -194,12 +194,6 @@ class elaborator::imp {
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) {
@ -213,15 +207,21 @@ class elaborator::imp {
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;
}
expr expected = abst_domain(f_t);
expr given = types[i];
if (!has_metavar(expected) && !has_metavar(given)) {
if (!is_convertible(expected, given, ctx) &&
!m_frontend.get_coercion(given, expected))
break; // failed to use this overload
}
f_t = instantiate_free_var_mmv(abst_body(f_t), 0, args[i]);
}
if (i == num_args) {
if (good_choices.empty()) {
// first good choice
args[0] = f_choices[j];
types[0] = f_choice_types[j];
}
good_choices.push_back(j);
}
} catch (exception & ex) {
@ -233,8 +233,7 @@ class elaborator::imp {
// 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]];
// found overload
} else {
// TODO add information to the exception
throw exception("ambiguous overload");
@ -310,8 +309,23 @@ class elaborator::imp {
expr f_t = types[0];
for (unsigned i = 1; i < num; i++) {
f_t = check_pi(f_t, ctx, e, ctx);
if (m_add_constraints)
add_constraint(abst_domain(f_t), types[i], ctx, e, i);
if (m_processing_root) {
expr expected = abst_domain(f_t);
expr given = types[i];
if (has_metavar(expected) || has_metavar(given)) {
m_constraints.push_back(constraint(expected, given, ctx, e, ctx, i));
} else {
if (!is_convertible(expected, given, ctx)) {
expr coercion = m_frontend.get_coercion(given, expected);
if (coercion) {
modified = true;
args[i] = mk_app(coercion, args[i]);
} else {
throw app_type_mismatch_exception(m_env, ctx, e, i, expected, given);
}
}
}
}
f_t = instantiate_free_var_mmv(abst_body(f_t), 0, args[i]);
}
if (modified) {
@ -589,7 +603,7 @@ class elaborator::imp {
void solve() {
unsigned num_meta = m_metavars.size();
m_add_constraints = false;
m_processing_root = false;
while (true) {
solve_core();
bool cont = false;
@ -673,7 +687,7 @@ public:
m_constraints.clear();
m_metavars.clear();
m_owner = &elb;
m_add_constraints = true;
m_processing_root = true;
m_root = process(e, context()).first;
if (has_metavar(m_root)) {
solve();

24
src/frontends/lean/lean_frontend.cpp
View file

@ -173,6 +173,7 @@ struct frontend::imp {
// overload
if (defined_here(old_op, led)) {
old_op.add_expr(d);
insert(m_expr_to_operator, d, old_op);
} else {
// we must copy the operator because it was defined in
// a parent frontend.
@ -180,12 +181,15 @@ struct frontend::imp {
register_new_op(new_op, d, led);
}
} else {
diagnostic(m_state) << "The denotation(s) for the existing notation:\n " << old_op << "\nhave been replaced with the new denotation:\n " << d << "\nbecause they conflict on how implicit arguments are used.\n";
diagnostic(m_state) << "The denotation(s) for the existing notation:\n " << old_op
<< "\nhave been replaced with the new denotation:\n " << d
<< "\nbecause they conflict on how implicit arguments are used.\n";
remove_bindings(old_op);
register_new_op(new_op, d, led);
}
} else {
diagnostic(m_state) << "Notation has been redefined, the existing notation:\n " << old_op << "\nhas been replaced with:\n " << new_op << "\nbecause they conflict with each other.\n";
diagnostic(m_state) << "Notation has been redefined, the existing notation:\n " << old_op
<< "\nhas been replaced with:\n " << new_op << "\nbecause they conflict with each other.\n";
remove_bindings(old_op);
register_new_op(new_op, d, led);
}
@ -290,24 +294,30 @@ struct frontend::imp {
expr to = abst_body(norm_type);
if (from == to)
throw exception("invalid coercion declaration, 'from' and 'to' types are the same");
if (get_coercion(from, to))
if (get_coercion_core(from, to))
throw exception("invalid coercion declaration, frontend already has a coercion for the given types");
m_coercion_map[expr_pair(from, to)] = f;
m_coercion_set.insert(f);
m_env.add_neutral_object(new coercion_declaration(f));
}
expr get_coercion(expr const & given_type, expr const & expected_type) {
expr get_coercion_core(expr const & given_type, expr const & expected_type) {
expr_pair p(given_type, expected_type);
auto it = m_coercion_map.find(p);
if (it != m_coercion_map.end())
return it->second;
else if (has_parent())
return m_parent->get_coercion(given_type, expected_type);
return m_parent->get_coercion_core(given_type, expected_type);
else
return expr();
}
expr get_coercion(expr const & given_type, expr const & expected_type) {
expr norm_given_type = m_env.normalize(given_type);
expr norm_expected_type = m_env.normalize(expected_type);
return get_coercion_core(norm_given_type, norm_expected_type);
}
bool is_coercion(expr const & f) {
return m_coercion_set.find(f) != m_coercion_set.end();
}
@ -392,8 +402,8 @@ std::vector<bool> const & frontend::get_implicit_arguments(name const & n) const
name const & frontend::get_explicit_version(name const & n) const { return m_imp->get_explicit_version(n); }
void frontend::add_coercion(expr const & f) { m_imp->add_coercion(f); }
expr frontend::get_coercion(expr const & given_type, expr const & expected_type) { return m_imp->get_coercion(given_type, expected_type); }
bool frontend::is_coercion(expr const & f) { return m_imp->is_coercion(f); }
expr frontend::get_coercion(expr const & given_type, expr const & expected_type) const { return m_imp->get_coercion(given_type, expected_type); }
bool frontend::is_coercion(expr const & f) const { return m_imp->is_coercion(f); }
state const & frontend::get_state() const { return m_imp->m_state; }
state & frontend::get_state_core() { return m_imp->m_state; }

6
src/frontends/lean/lean_frontend.h
View file

@ -160,15 +160,13 @@ public:
\brief Return a coercion from given_type to expected_type if it exists.
Return the null expression if there is no coercion from \c given_type to
\c expected_type.
\pre The expressions \c given_type and \c expected_type are normalized
*/
expr get_coercion(expr const & given_type, expr const & expected_type);
expr get_coercion(expr const & given_type, expr const & expected_type) const;
/**
\brief Return true iff the given expression is a coercion. That is, it was added using
\c add_coercion.
*/
bool is_coercion(expr const & f);
bool is_coercion(expr const & f) const;
/*@}*/
/**

17
src/frontends/lean/lean_pp.cpp
View file

@ -32,12 +32,16 @@ Author: Leonardo de Moura
#define LEAN_DEFAULT_PP_MAX_STEPS std::numeric_limits<unsigned>::max()
#endif
#ifndef LEAN_DEFAULT_PP_NOTATION
#define LEAN_DEFAULT_PP_NOTATION true
#endif
#ifndef LEAN_DEFAULT_PP_IMPLICIT
#define LEAN_DEFAULT_PP_IMPLICIT false
#endif
#ifndef LEAN_DEFAULT_PP_NOTATION
#define LEAN_DEFAULT_PP_NOTATION true
#ifndef LEAN_DEFAULT_PP_COERCION
#define LEAN_DEFAULT_PP_COERCION false
#endif
#ifndef LEAN_DEFAULT_PP_EXTRA_LETS
@ -78,11 +82,13 @@ static name g_pp_implicit {"lean", "pp", "implicit"};
static name g_pp_notation {"lean", "pp", "notation"};
static name g_pp_extra_lets {"lean", "pp", "extra_lets"};
static name g_pp_alias_min_weight{"lean", "pp", "alias_min_weight"};
static name g_pp_coercion {"lean", "pp", "coercion"};
RegisterUnsignedOption(g_pp_max_depth, LEAN_DEFAULT_PP_MAX_DEPTH, "(lean pretty printer) maximum expression depth, after that it will use ellipsis");
RegisterUnsignedOption(g_pp_max_steps, LEAN_DEFAULT_PP_MAX_STEPS, "(lean pretty printer) maximum number of visited expressions, after that it will use ellipsis");
RegisterBoolOption(g_pp_implicit, LEAN_DEFAULT_PP_IMPLICIT, "(lean pretty printer) display implicit parameters");
RegisterBoolOption(g_pp_notation, LEAN_DEFAULT_PP_NOTATION, "(lean pretty printer) disable/enable notation (infix, mixfix, postfix operators and unicode characters)");
RegisterBoolOption(g_pp_coercion, LEAN_DEFAULT_PP_COERCION, "(lean pretty printer) display coercions");
RegisterBoolOption(g_pp_extra_lets, LEAN_DEFAULT_PP_EXTRA_LETS, "(lean pretty printer) introduce extra let expressions when displaying shared terms");
RegisterUnsignedOption(g_pp_alias_min_weight, LEAN_DEFAULT_PP_ALIAS_MIN_WEIGHT, "(lean pretty printer) mimimal weight (approx. size) of a term to be considered a shared term");
@ -90,6 +96,7 @@ unsigned get_pp_max_depth(options const & opts) { return opts.get_unsigne
unsigned get_pp_max_steps(options const & opts) { return opts.get_unsigned(g_pp_max_steps, LEAN_DEFAULT_PP_MAX_STEPS); }
bool get_pp_implicit(options const & opts) { return opts.get_bool(g_pp_implicit, LEAN_DEFAULT_PP_IMPLICIT); }
bool get_pp_notation(options const & opts) { return opts.get_bool(g_pp_notation, LEAN_DEFAULT_PP_NOTATION); }
bool get_pp_coercion(options const & opts) { return opts.get_bool(g_pp_coercion, LEAN_DEFAULT_PP_COERCION); }
bool get_pp_extra_lets(options const & opts) { return opts.get_bool(g_pp_extra_lets, LEAN_DEFAULT_PP_EXTRA_LETS); }
unsigned get_pp_alias_min_weight(options const & opts) { return opts.get_unsigned(g_pp_alias_min_weight, LEAN_DEFAULT_PP_ALIAS_MIN_WEIGHT); }
@ -136,7 +143,8 @@ class pp_fn {
unsigned m_indent;
unsigned m_max_depth;
unsigned m_max_steps;
bool m_implict;
bool m_implict; //!< if true show implicit arguments
bool m_coercion; //!< if true show coercions
bool m_notation; //!< if true use notation
bool m_extra_lets; //!< introduce extra let-expression to cope with sharing.
unsigned m_alias_min_weight; //!< minimal weight for creating an alias
@ -535,6 +543,8 @@ class pp_fn {
\brief Pretty print an application.
*/
result pp_app(expr const & e, unsigned depth) {
if (!m_coercion && num_args(e) == 2 && m_frontend.is_coercion(arg(e,0)))
return pp(arg(e,1), depth);
application app(e, *this, m_implict);
operator_info op;
if (m_notation && app.notation_enabled() && (op = get_operator(e)) && has_expected_num_args(app, op)) {
@ -930,6 +940,7 @@ class pp_fn {
m_max_depth = get_pp_max_depth(opts);
m_max_steps = get_pp_max_steps(opts);
m_implict = get_pp_implicit(opts);
m_coercion = get_pp_coercion(opts);
m_notation = get_pp_notation(opts);
m_extra_lets = get_pp_extra_lets(opts);
m_alias_min_weight = get_pp_alias_min_weight(opts);

33
tests/lean/coercion2.lean Normal file
View file

@ -0,0 +1,33 @@
Set pp::colors false
Variable T : Type
Variable R : Type
Variable t2r : T -> R
Coercion t2r
Variable g : R -> R -> R
Variable a : T
Show g a a
Variable b : R
Show g a b
Show g b a
Set lean::pp::coercion true
Show g a a
Show g a b
Show g b a
Set lean::pp::coercion false
Variable S : Type
Variable s : S
Variable r : S
Variable h : S -> S -> S
Infixl 10 ++ : g
Infixl 10 ++ : h
Set lean::pp::notation false
Show a ++ b ++ a
Show r ++ s ++ r
Check a ++ b ++ a
Check r ++ s ++ r
Set lean::pp::coercion true
Show a ++ b ++ a
Show r ++ s ++ r
Set lean::pp::notation true
Show a ++ b ++ a
Show r ++ s ++ r

31
tests/lean/coercion2.lean.expected.out Normal file
View file

@ -0,0 +1,31 @@
Set option: pp::colors
Assumed: T
Assumed: R
Assumed: t2r
Coercion t2r
Assumed: g
Assumed: a
g a a
Assumed: b
g a b
g b a
Set option: lean::pp::coercion
g (t2r a) (t2r a)
g (t2r a) b
g b (t2r a)
Set option: lean::pp::coercion
Assumed: S
Assumed: s
Assumed: r
Assumed: h
Set option: lean::pp::notation
g (g a b) a
h (h r s) r
R
S
Set option: lean::pp::coercion
g (g (t2r a) b) (t2r a)
h (h r s) r
Set option: lean::pp::notation
(t2r a) ++ b ++ (t2r a)
r ++ s ++ r

4
tests/lean/tst3.lean
View file

@ -19,9 +19,9 @@ Set lean::pp::notation true.
Show c |- d ; e.
Variable fact : A -> A.
Notation 20 _ ! : fact.
Show a! !.
Show c! !.
Set lean::pp::notation false.
Show a! !.
Show c! !.
Set lean::pp::notation true.
Variable g : A -> A -> A.
Notation 30 [ _ ; _ ] : g

4
tests/lean/tst3.lean.expected.out
View file

@ -6,8 +6,8 @@ implies true (implies a false)
Notation 100 _ |- _ ; _ : f
f c d e
c |- d ; e
(a !) !
fact (fact a)
(c !) !
fact (fact c)
[ c ; d ]
[ c ; ([ d ; e ]) ]
g c (g d e)

2
tests/lean/tst9.lean.expected.out
View file

@ -3,7 +3,7 @@
Assumed: g
Assumed: a
Error (line: 5, pos: 6) type mismatch at application argument 1 of
g ⊤ (f N a a)
g ⊤ (f _ a a)
expected type
N
given type