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

feat(kernel): add strict implicit arguments

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-25 17:47:38 -07:00
parent 1da4ed5d80
commit acf8c13619
10 changed files with 166 additions and 26 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
src/frontends/lean/decl_cmds.cpp
View file

@ -20,6 +20,8 @@ namespace lean {
static name g_llevel_curly(".{");
static name g_lcurly("{");
static name g_rcurly("}");
static name g_ldcurly("⦃");
static name g_rdcurly("⦄");
static name g_lbracket("[");
static name g_rbracket("]");
static name g_colon(":");
@ -47,11 +49,20 @@ binder_info parse_open_binder_info(parser & p) {
if (p.curr_is_token(g_lcurly)) {
check_in_section(p);
p.next();
return mk_implicit_binder_info();
if (p.curr_is_token(g_lcurly)) {
p.next();
return mk_strict_implicit_binder_info();
} else {
return mk_implicit_binder_info();
}
} else if (p.curr_is_token(g_lbracket)) {
check_in_section(p);
p.next();
return mk_cast_binder_info();
} else if (p.curr_is_token(g_ldcurly)) {
check_in_section(p);
p.next();
return mk_strict_implicit_binder_info();
} else {
return binder_info();
}
@ -62,6 +73,13 @@ void parse_close_binder_info(parser & p, binder_info const & bi) {
p.check_token_next(g_rcurly, "invalid declaration, '}' expected");
} else if (bi.is_cast()) {
p.check_token_next(g_rbracket, "invalid declaration, ']' expected");
} else if (bi.is_strict_implicit()) {
if (p.curr_is_token(g_lcurly)) {
p.next();
p.check_token_next(g_rdcurly, "invalid declaration, '}' expected");
} else {
p.check_token_next(g_rdcurly, "invalid declaration, '⦄' expected");
}
}
}

14
src/frontends/lean/elaborator.cpp
View file

@ -348,14 +348,22 @@ public:
expr f = visit(app_fn(e));
auto f_t = ensure_fun(f);
f = f_t.first;
expr d_type = binding_domain(f_t.second);
expr f_type = f_t.second;
lean_assert(is_pi(f_type));
while (is_pi(f_type) && binding_info(f_type).is_strict_implicit()) {
tag g = f.get_tag();
expr imp_arg = mk_meta(some_expr(binding_domain(f_type)), g);
f = mk_app(f, imp_arg, g);
f_type = whnf(instantiate(binding_body(f_type), imp_arg));
}
expr d_type = binding_domain(f_type);
expr a = visit_expecting_type_of(app_arg(e), d_type);
expr a_type = instantiate_metavars(infer_type(a));
expr r = mk_app(f, a, e.get_tag());
app_delayed_justification j(m_env, r, f_t.second, a_type);
app_delayed_justification j(m_env, r, f_type, a_type);
if (!m_tc.is_def_eq(a_type, d_type, j)) {
// try coercions
optional<expr> c = get_coercion(a_type, d_type, binding_info(f_t.second).is_cast());
optional<expr> c = get_coercion(a_type, d_type, binding_info(f_type).is_cast());
bool coercion_worked = false;
expr new_a;
if (c) {

40
src/frontends/lean/parser.cpp
View file

@ -396,6 +396,8 @@ static name g_rparen(")");
static name g_llevel_curly(".{");
static name g_lcurly("{");
static name g_rcurly("}");
static name g_ldcurly("⦃");
static name g_rdcurly("⦄");
static name g_lbracket("[");
static name g_rbracket("]");
static name g_add("+");
@ -578,16 +580,29 @@ parameter parser::parse_binder() {
return p;
} else if (curr_is_token(g_lcurly)) {
next();
auto p = parse_binder_core(mk_implicit_binder_info());
check_token_next(g_rcurly, "invalid binder, '}' expected");
return p;
if (curr_is_token(g_lcurly)) {
next();
auto p = parse_binder_core(mk_strict_implicit_binder_info());
check_token_next(g_rcurly, "invalid binder, '}' expected");
check_token_next(g_rcurly, "invalid binder, '}' expected");
return p;
} else {
auto p = parse_binder_core(mk_implicit_binder_info());
check_token_next(g_rcurly, "invalid binder, '}' expected");
return p;
}
} else if (curr_is_token(g_lbracket)) {
next();
auto p = parse_binder_core(mk_cast_binder_info());
check_token_next(g_rbracket, "invalid binder, ']' expected");
return p;
} else if (curr_is_token(g_ldcurly)) {
next();
auto p = parse_binder_core(mk_strict_implicit_binder_info());
check_token_next(g_rdcurly, "invalid binder, '⦄' expected");
return p;
} else {
throw parser_error("invalid binder, '(', '{', '[' or identifier expected", pos());
throw parser_error("invalid binder, '(', '{', '[', '{{', '⦃' or identifier expected", pos());
}
}
@ -623,12 +638,23 @@ void parser::parse_binders_core(buffer<parameter> & r) {
check_token_next(g_rparen, "invalid binder, ')' expected");
} else if (curr_is_token(g_lcurly)) {
next();
parse_binder_block(r, mk_implicit_binder_info());
check_token_next(g_rcurly, "invalid binder, '}' expected");
if (curr_is_token(g_lcurly)) {
next();
parse_binder_block(r, mk_strict_implicit_binder_info());
check_token_next(g_rcurly, "invalid binder, '}' expected");
check_token_next(g_rcurly, "invalid binder, '}' expected");
} else {
parse_binder_block(r, mk_implicit_binder_info());
check_token_next(g_rcurly, "invalid binder, '}' expected");
}
} else if (curr_is_token(g_lbracket)) {
next();
parse_binder_block(r, mk_cast_binder_info());
check_token_next(g_rbracket, "invalid binder, ']' expected");
} else if (curr_is_token(g_ldcurly)) {
next();
parse_binder_block(r, mk_strict_implicit_binder_info());
check_token_next(g_rdcurly, "invalid binder, '⦄' expected");
} else {
return;
}
@ -641,7 +667,7 @@ local_environment parser::parse_binders(buffer<parameter> & r) {
unsigned old_sz = r.size();
parse_binders_core(r);
if (old_sz == r.size())
throw parser_error("invalid binder, '(', '{', '[' or identifier expected", pos());
throw parser_error("invalid binder, '(', '{', '[', '{{', '⦃' or identifier expected", pos());
return local_environment(m_env);
}

2
src/frontends/lean/token_table.cpp
View file

@ -57,7 +57,7 @@ token_table init_token_table() {
std::pair<char const *, unsigned> builtin[] =
{{"fun", 0}, {"Pi", 0}, {"let", 0}, {"in", 0}, {"have", 0}, {"show", 0}, {"by", 0}, {"then", 0},
{"from", 0}, {"(", g_max_prec}, {")", 0}, {"{", g_max_prec}, {"}", 0}, {"_", g_max_prec},
{"[", g_max_prec}, {"]", 0}, {".{", 0}, {"Type", g_max_prec}, {"|", 0}, {"with", 0},
{"[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0}, {"Type", g_max_prec}, {"|", 0}, {"with", 0},
{"...", 0}, {",", 0}, {".", 0}, {":", 0}, {"calc", 0}, {":=", 0}, {"--", 0}, {"#", 0},
{"(*", 0}, {"(--", 0}, {"proof", 0}, {"qed", 0}, {"@", 0},
{"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, {nullptr, 0}};

6
src/kernel/expr.cpp
View file

@ -149,7 +149,11 @@ void expr_app::dealloc(buffer<expr_cell*> & todelete) {
static unsigned dec(unsigned k) { return k == 0 ? 0 : k - 1; }
bool operator==(binder_info const & i1, binder_info const & i2) {
return i1.is_implicit() == i2.is_implicit() && i1.is_cast() == i2.is_cast() && i1.is_contextual() == i2.is_contextual();
return
i1.is_implicit() == i2.is_implicit() &&
i1.is_cast() == i2.is_cast() &&
i1.is_contextual() == i2.is_contextual() &&
i1.is_strict_implicit() == i2.is_strict_implicit();
}
// Expr binders (Lambda, Pi)

13
src/kernel/expr.h
View file

@ -241,18 +241,21 @@ public:
is only used for elaboration.
*/
class binder_info {
unsigned m_implicit:1; //! if true, binder argument is an implicit argument
unsigned m_cast:1; //! if true, binder argument is a target for using cast
unsigned m_contextual:1; //! if true, binder argument is assumed to be part of the context, and may be argument for metavariables.
unsigned m_implicit:1; //! if true, binder argument is an implicit argument
unsigned m_cast:1; //! if true, binder argument is a target for using cast
unsigned m_contextual:1; //! if true, binder argument is assumed to be part of the context, and may be argument for metavariables.
unsigned m_strict_implicit:1; //! if true, binder argument is assumed to be a strict implicit argument
public:
binder_info(bool implicit = false, bool cast = false, bool contextual = true):
m_implicit(implicit), m_cast(cast), m_contextual(contextual) {}
binder_info(bool implicit = false, bool cast = false, bool contextual = true, bool strict_implicit = false):
m_implicit(implicit), m_cast(cast), m_contextual(contextual), m_strict_implicit(strict_implicit) {}
bool is_implicit() const { return m_implicit; }
bool is_cast() const { return m_cast; }
bool is_contextual() const { return m_contextual; }
bool is_strict_implicit() const { return m_strict_implicit; }
};
inline binder_info mk_implicit_binder_info() { return binder_info(true); }
inline binder_info mk_strict_implicit_binder_info() { return binder_info(false, false, true, true); }
inline binder_info mk_cast_binder_info() { return binder_info(false, true); }
inline binder_info mk_contextual_info(bool f) { return binder_info(false, false, f); }

4
src/kernel/formatter.cpp
View file

@ -134,6 +134,8 @@ struct print_expr_fn {
out() << "[";
else if (!binding_info(e).is_contextual())
out() << "[[";
else if (binding_info(e).is_strict_implicit())
out() << "{{";
else
out() << "(";
out() << n << " : ";
@ -144,6 +146,8 @@ struct print_expr_fn {
out() << "]";
else if (!binding_info(e).is_contextual())
out() << "]]";
else if (binding_info(e).is_strict_implicit())
out() << "}}";
else
out() << ")";
e = p.first;

14
src/library/kernel_bindings.cpp
View file

@ -275,17 +275,21 @@ static int mk_binder_info(lua_State * L) {
return push_binder_info(L, binder_info(lua_toboolean(L, 1)));
else if (nargs == 2)
return push_binder_info(L, binder_info(lua_toboolean(L, 1), lua_toboolean(L, 2)));
else
else if (nargs == 3)
return push_binder_info(L, binder_info(lua_toboolean(L, 1), lua_toboolean(L, 2), lua_toboolean(L, 3)));
else
return push_binder_info(L, binder_info(lua_toboolean(L, 1), lua_toboolean(L, 2), lua_toboolean(L, 3), lua_toboolean(L, 4)));
}
static int binder_info_is_implicit(lua_State * L) { return push_boolean(L, to_binder_info(L, 1).is_implicit()); }
static int binder_info_is_cast(lua_State * L) { return push_boolean(L, to_binder_info(L, 1).is_cast()); }
static int binder_info_is_contextual(lua_State * L) { return push_boolean(L, to_binder_info(L, 1).is_contextual()); }
static int binder_info_is_strict_implicit(lua_State * L) { return push_boolean(L, to_binder_info(L, 1).is_strict_implicit()); }
static const struct luaL_Reg binder_info_m[] = {
{"__gc", binder_info_gc},
{"is_implicit", safe_function<binder_info_is_implicit>},
{"is_cast", safe_function<binder_info_is_cast>},
{"is_contextual", safe_function<binder_info_is_contextual>},
{"__gc", binder_info_gc},
{"is_implicit", safe_function<binder_info_is_implicit>},
{"is_cast", safe_function<binder_info_is_cast>},
{"is_contextual", safe_function<binder_info_is_contextual>},
{"is_strict_implicit", safe_function<binder_info_is_strict_implicit>},
{0, 0}
};
static void open_binder_info(lua_State * L) {

10
src/library/kernel_serializer.cpp
View file

@ -119,13 +119,17 @@ static expr read_macro_definition(deserializer & d, unsigned num, expr const * a
serializer & operator<<(serializer & s, binder_info const & i) {
s.write_bool(i.is_implicit());
s.write_bool(i.is_cast());
s.write_bool(i.is_contextual());
s.write_bool(i.is_strict_implicit());
return s;
}
static binder_info read_binder_info(deserializer & d) {
bool imp = d.read_bool();
bool cast = d.read_bool();
return binder_info(imp, cast);
bool imp = d.read_bool();
bool cast = d.read_bool();
bool ctx = d.read_bool();
bool s_imp = d.read_bool();
return binder_info(imp, cast, ctx, s_imp);
}
class expr_serializer : public object_serializer<expr, expr_hash_alloc, expr_eqp> {

69
tests/lean/run/e5.lean Normal file
View file

@ -0,0 +1,69 @@
definition Bool [inline] := Type.{0}
definition false : Bool := ∀x : Bool, x
check false
theorem false_elim (C : Bool) (H : false) : C
:= H C
definition eq {A : Type} (a b : A)
:= ∀ P : A → Bool, P a → P b
check eq
infix `=` 50 := eq
theorem refl {A : Type} (a : A) : a = a
:= λ P H, H
definition true : Bool
:= false = false
theorem trivial : true
:= refl false
theorem subst {A : Type} {P : A -> Bool} {a b : A} (H1 : a = b) (H2 : P a) : P b
:= H1 _ H2
theorem symm {A : Type} {a b : A} (H : a = b) : b = a
:= subst H (refl a)
theorem trans {A : Type} {a b c : A} (H1 : a = b) (H2 : b = c) : a = c
:= subst H2 H1
inductive nat : Type :=
| zero : nat
| succ : nat → nat
print "using strict implicit arguments"
abbreviation symmetric {A : Type} (R : A → A → Bool) := ∀ ⦃a b⦄, R a b → R b a
check symmetric
variable p : nat → nat → Bool
check symmetric p
axiom H1 : symmetric p
axiom H2 : p zero (succ zero)
check H1
check H1 H2
print "------------"
print "using implicit arguments"
abbreviation symmetric2 {A : Type} (R : A → A → Bool) := ∀ {a b}, R a b → R b a
check symmetric2
check symmetric2 p
axiom H3 : symmetric2 p
axiom H4 : p zero (succ zero)
check H3
check H3 H4
print "-----------------"
print "using strict implicit arguments (ASCII notation)"
abbreviation symmetric3 {A : Type} (R : A → A → Bool) := ∀ {{a b}}, R a b → R b a
check symmetric3
check symmetric3 p
axiom H5 : symmetric3 p
axiom H6 : p zero (succ zero)
check H5
check H5 H6