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

feat(frontends/lua/parser): allow users to specify the precedence of macros

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-25 12:27:56 -08:00
parent f418491c70
commit a3dde29f3c
4 changed files with 46 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/extra/macros.lua
View file

@ -24,6 +24,7 @@
-- The _ are placeholders (aka) holes that will be filled by the Lean
-- elaborator.
function binder_macro(name, f, farity, typepos, lambdapos)
local precedence = 0
macro(name, { macro_arg.Bindings, macro_arg.Comma, macro_arg.Expr },
function (bindings, body)
local r = body
@ -44,7 +45,8 @@ function binder_macro(name, f, farity, typepos, lambdapos)
r = mk_app(unpack(args))
end
return r
end)
end,
precedence)
end
-- The following macro is used to create nary versions of operators such as MP and ForallElim.
@ -85,3 +87,4 @@ binder_macro("for", Const("ForallIntro"), 3, 1, 3)
binder_macro("assume", Const("Discharge"), 3, 1, 3)
nary_macro("instantiate", Const("ForallElim"), 4)
nary_macro("mp", Const("MP"), 4)
nary_macro("subst", Const("Subst"), 6)

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

@ -132,7 +132,12 @@ static unsigned g_level_cup_prec = 5;
static name g_unused = name::mk_internal_unique_name();
enum class macro_arg_kind { Expr, Exprs, Bindings, Id, Comma, Assign };
typedef std::pair<list<macro_arg_kind>, luaref> macro;
struct macro {
list<macro_arg_kind> m_arg_kinds;
luaref m_fn;
unsigned m_precedence;
macro(list<macro_arg_kind> const & as, luaref const & fn, unsigned prec):m_arg_kinds(as), m_fn(fn), m_precedence(prec) {}
};
typedef name_map<macro> macros;
macros & get_macros(lua_State * L);
@ -921,47 +926,47 @@ class parser::imp {
/**
\brief Parse a macro implemented in Lua
*/
expr parse_macro(list<macro_arg_kind> const & arg_kinds, luaref const & proc, macro_arg_stack & args, pos_info const & p) {
expr parse_macro(list<macro_arg_kind> const & arg_kinds, luaref const & fn, unsigned prec, macro_arg_stack & args, pos_info const & p) {
if (arg_kinds) {
auto k = head(arg_kinds);
switch (k) {
case macro_arg_kind::Expr: {
expr e = parse_expr(g_app_precedence);
expr e = parse_expr(prec);
args.emplace_back(k, &e);
return parse_macro(tail(arg_kinds), proc, args, p);
return parse_macro(tail(arg_kinds), fn, prec, args, p);
}
case macro_arg_kind::Exprs: {
buffer<expr> exprs;
while (is_curr_begin_expr()) {
exprs.push_back(parse_expr(g_app_precedence));
exprs.push_back(parse_expr(prec));
}
args.emplace_back(k, &exprs);
return parse_macro(tail(arg_kinds), proc, args, p);
return parse_macro(tail(arg_kinds), fn, prec, args, p);
}
case macro_arg_kind::Bindings: {
mk_scope scope(*this);
bindings_buffer bindings;
parse_expr_bindings(bindings);
args.emplace_back(k, &bindings);
return parse_macro(tail(arg_kinds), proc, args, p);
return parse_macro(tail(arg_kinds), fn, prec, args, p);
}
case macro_arg_kind::Comma:
check_comma_next("invalid macro, ',' expected");
return parse_macro(tail(arg_kinds), proc, args, p);
return parse_macro(tail(arg_kinds), fn, prec, args, p);
case macro_arg_kind::Assign:
check_comma_next("invalid macro, ':=' expected");
return parse_macro(tail(arg_kinds), proc, args, p);
return parse_macro(tail(arg_kinds), fn, prec, args, p);
case macro_arg_kind::Id: {
name n = curr_name();
args.emplace_back(k, &n);
return parse_macro(tail(arg_kinds), proc, args, p);
return parse_macro(tail(arg_kinds), fn, prec, args, p);
}}
lean_unreachable();
} else {
// All arguments have been parsed, then call Lua procedure proc.
// All arguments have been parsed, then call Lua procedure fn.
m_last_script_pos = p;
return m_script_state->apply([&](lua_State * L) {
proc.push();
fn.push();
for (auto p : args) {
macro_arg_kind k = p.first;
void * arg = p.second;
@ -1019,10 +1024,8 @@ class parser::imp {
expr parse_macro(name const & id, pos_info const & p) {
lean_assert(m_macros && m_macros->find(id) != m_macros->end());
auto m = m_macros->find(id)->second;
list<macro_arg_kind> arg_kinds = m.first;
luaref proc = m.second;
macro_arg_stack args;
return parse_macro(arg_kinds, proc, args, p);
return parse_macro(m.m_arg_kinds, m.m_fn, m.m_precedence, args, p);
}
/**
@ -2671,7 +2674,9 @@ macros & get_macros(lua_State * L) {
}
int mk_macro(lua_State * L) {
int nargs = lua_gettop(L);
name macro_name = to_name_ext(L, 1);
unsigned prec = nargs == 4 ? lua_tointeger(L, 4) : g_app_precedence;
luaL_checktype(L, 3, LUA_TFUNCTION); // user-fun
buffer<macro_arg_kind> arg_kind_buffer;
int n = objlen(L, 2);
@ -2681,7 +2686,7 @@ int mk_macro(lua_State * L) {
lua_pop(L, 1);
}
list<macro_arg_kind> arg_kinds = to_list(arg_kind_buffer.begin(), arg_kind_buffer.end());
get_macros(L).insert(mk_pair(macro_name, macro(arg_kinds, luaref(L, 3))));
get_macros(L).insert(mk_pair(macro_name, macro(arg_kinds, luaref(L, 3), prec)));
return 0;
}

7
tests/lean/subst3.lean Normal file
View file

@ -0,0 +1,7 @@
(** import("macros.lua") **)
Theorem T (A : Type) (p : A -> Bool) (f : A -> A -> A) : forall x y z, p (f x x) => x = y => x = z => p (f y z) :=
for x y z, assume (H1 : p (f x x)) (H2 : x = y) (H3 : x = z),
subst H1 H2 H3.
Show Environment 1.

14
tests/lean/subst3.lean.expected.out Normal file
View file

@ -0,0 +1,14 @@
Set: pp::colors
Set: pp::unicode
Proved: T
Theorem T (A : Type) (p : A → Bool) (f : A → A → A) : ∀ x y z : A,
p (f x x) ⇒ x = y ⇒ x = z ⇒ p (f y z) :=
ForallIntro
(λ x : A,
ForallIntro
(λ y : A,
ForallIntro
(λ z : A,
Discharge
(λ H1 : p (f x x),
Discharge (λ H2 : x = y, Discharge (λ H3 : x = z, Subst (Subst H1 H2) H3))))))