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

fix(frontends/lean/parser): fix deadlock in macro parser

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-19 21:36:17 -08:00
parent c77464703f
commit 3eb4de6760
5 changed files with 206 additions and 52 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

94
examples/lean/macros.lean Normal file
View file

@ -0,0 +1,94 @@
(**
-- This example demonstrates how to create Macros for automating proof
-- construction using Lua.
-- This macro creates the syntax-sugar
-- name bindings ',' expr
-- For a function f with signature
-- f : ... (A : Type) ... (Pi x : A, ...)
--
-- farity is the arity of f
-- typepos is the position of (A : Type) argument
-- lambdapos is the position of the (Pi x : A, ...) argument
--
-- Example: suppose we invoke
--
-- binder_macro("for", Const("ForallIntro"), 3, 1, 3)
--
-- Then, the macro expression
--
-- for x y : Int, H x y
--
-- produces the expression
--
-- ForallIntro Int _ (fun x : Int, ForallIntro Int _ (fun y : Int, H x y))
--
-- The _ are placeholders (aka) holes that will be filled by the Lean
-- elaborator.
function binder_macro(name, f, farity, typepos, lambdapos)
macro(name, { macro_arg.Bindings, macro_arg.Comma, macro_arg.Expr },
function (bindings, body)
local r = body
for i = #bindings, 1, -1 do
local bname = bindings[i][1]
local btype = bindings[i][2]
local args = {}
args[#args + 1] = f
for j = 1, farity, 1 do
if j == typepos then
args[#args + 1] = btype
elseif j == lambdapos then
args[#args + 1] = fun(bname, btype, r)
else
args[#args + 1] = mk_placeholder()
end
end
r = mk_app(unpack(args))
end
return r
end)
end
function nary_macro(name, f, farity)
local bin_app = function(e1, e2)
local args = {}
args[#args + 1] = f
for i = 1, farity - 2, 1 do
args[#args + 1] = mk_placeholder()
end
args[#args + 1] = e1
args[#args + 1] = e2
return mk_app(unpack(args))
end
macro(name, { macro_arg.Expr, macro_arg.Expr, macro_arg.Exprs },
function (e1, e2, rest)
local r = bin_app(e1, e2)
for i = 1, #rest do
r = bin_app(r, rest[i])
end
return r
end)
end
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)
**)
Definition Set (A : Type) : Type := A → Bool
Definition element {A : Type} (x : A) (s : Set A) := s x
Infix 60 ∈ : element
Definition subset {A : Type} (s1 : Set A) (s2 : Set A) := ∀ x, x ∈ s1 ⇒ x ∈ s2
Infix 50 ⊆ : subset
Theorem SubsetTrans (A : Type) : ∀ s1 s2 s3 : Set A, s1 ⊆ s2 ⇒ s2 ⊆ s3 ⇒ s1 ⊆ s3 :=
for s1 s2 s3, assume (H1 : s1 ⊆ s2) (H2 : s2 ⊆ s3),
show s1 ⊆ s3,
for x, assume Hin : x ∈ s1,
show x ∈ s3,
let L1 : x ∈ s2 := mp (instantiate H1 x) Hin
in mp (instantiate H2 x) L1

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

@ -280,6 +280,8 @@ class parser::imp {
bool curr_is_lcurly() const { return curr() == scanner::token::LeftCurlyBracket; }
/** \brief Return true iff the current token is a ':' */
bool curr_is_colon() const { return curr() == scanner::token::Colon; }
/** \brief Return true iff the current token is a ',' */
bool curr_is_comma() const { return curr() == scanner::token::Comma; }
/** \brief Return true iff the current token is a ':=' */
bool curr_is_assign() const { return curr() == scanner::token::Assign; }
/** \brief Return true iff the current token is an 'in' token */
@ -856,36 +858,79 @@ class parser::imp {
case scanner::token::CommandId:
case scanner::token::Eof:
case scanner::token::ScriptBlock:
case scanner::token::In:
return false;
default:
return true;
}
}
typedef buffer<std::pair<macro_arg_kind, void*>> macro_arg_stack;
/**
\brief Parse a macro implemented in Lua
*/
expr parse_macro(lua_State * L, list<macro_arg_kind> const & args, unsigned num_args, pos_info const & p) {
if (args) {
auto k = head(args);
expr parse_macro(list<macro_arg_kind> const & arg_kinds, luaref const & proc, macro_arg_stack & args, pos_info const & p) {
if (arg_kinds) {
auto k = head(arg_kinds);
switch (k) {
case macro_arg_kind::Expr:
push_expr(L, parse_expr());
return parse_macro(L, tail(args), num_args + 1, p);
case macro_arg_kind::Exprs: {
lua_newtable(L);
int i = 1;
while (is_curr_begin_expr()) {
push_expr(L, parse_expr(g_app_precedence));
lua_rawseti(L, -2, i);
i = i + 1;
case macro_arg_kind::Expr: {
expr e = parse_expr(g_app_precedence);
args.emplace_back(k, &e);
return parse_macro(tail(arg_kinds), proc, args, p);
}
return parse_macro(L, tail(args), num_args + 1, p);
case macro_arg_kind::Exprs: {
buffer<expr> exprs;
while (is_curr_begin_expr()) {
exprs.push_back(parse_expr(g_app_precedence));
}
args.emplace_back(k, &exprs);
return parse_macro(tail(arg_kinds), proc, 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);
}
case macro_arg_kind::Comma:
check_comma_next("invalid macro, ',' expected");
return parse_macro(tail(arg_kinds), proc, args, p);
case macro_arg_kind::Assign:
check_comma_next("invalid macro, ':=' expected");
return parse_macro(tail(arg_kinds), proc, 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);
}}
lean_unreachable();
} else {
// All arguments have been parsed, then call Lua procedure proc.
m_last_script_pos = p;
return m_script_state->apply([&](lua_State * L) {
proc.push();
for (auto p : args) {
macro_arg_kind k = p.first;
void * arg = p.second;
switch (k) {
case macro_arg_kind::Expr:
push_expr(L, *static_cast<expr*>(arg));
break;
case macro_arg_kind::Exprs: {
auto const & exprs = *static_cast<buffer<expr>*>(arg);
lua_newtable(L);
int i = 1;
for (auto e : exprs) {
push_expr(L, e);
lua_rawseti(L, -2, i);
i = i + 1;
}
break;
}
case macro_arg_kind::Bindings: {
bindings_buffer const & bindings = *static_cast<bindings_buffer*>(arg);
lua_newtable(L);
int i = 1;
for (auto const & b : bindings) {
@ -897,24 +942,16 @@ class parser::imp {
lua_rawseti(L, -2, i);
i = i + 1;
}
return parse_macro(L, tail(args), num_args + 1, p);
break;
}
case macro_arg_kind::Comma:
check_comma_next("invalid macro, ',' expected");
return parse_macro(L, tail(args), num_args, p);
case macro_arg_kind::Assign:
check_comma_next("invalid macro, ':=' expected");
return parse_macro(L, tail(args), num_args, p);
case macro_arg_kind::Id:
push_name(L, curr_name());
next();
return parse_macro(L, tail(args), num_args + 1, p);
}
push_name(L, *static_cast<name*>(arg));
break;
default:
lean_unreachable();
} else {
// All arguments have been parsed, then call Lua procedure proc.
m_last_script_pos = p;
pcall(L, num_args, 1, 0);
}
}
pcall(L, args.size(), 1, 0);
if (is_expr(L, -1)) {
expr r = to_expr(L, -1);
lua_pop(L, 1);
@ -923,18 +960,17 @@ class parser::imp {
lua_pop(L, 1);
throw parser_error("failed to execute macro", p);
}
});
}
}
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> args = m.first;
list<macro_arg_kind> arg_kinds = m.first;
luaref proc = m.second;
return m_script_state->apply([&](lua_State * L) {
proc.push();
return parse_macro(L, args, 0, p);
});
macro_arg_stack args;
return parse_macro(arg_kinds, proc, args, p);
}
/**
@ -1334,12 +1370,18 @@ class parser::imp {
auto p = pos();
next();
expr t = parse_expr();
check_next(scanner::token::By, "invalid 'show _ by _' expression, 'by' expected");
if (curr_is_comma()) {
next();
expr b = parse_expr();
return mk_let("H", t, b, Var(0));
} else {
check_next(scanner::token::By, "invalid 'show' expression, 'by' or ',' expected");
tactic tac = parse_tactic_expr();
expr r = mk_placeholder(some_expr(t));
m_tactic_hints.insert(mk_pair(r, tac));
return save(r, p);
}
}
/** \brief Parse <tt>'by' tactic</tt> */
expr parse_by_expr() {

13
src/library/placeholder.cpp
View file

@ -10,6 +10,7 @@ Author: Leonardo de Moura
#include "kernel/replace_visitor.h"
#include "library/expr_pair.h"
#include "library/placeholder.h"
#include "library/kernel_bindings.h"
namespace lean {
static name g_placeholder_name("_");
@ -54,4 +55,16 @@ expr replace_placeholders_with_metavars(expr const & e, metavar_env const & menv
replace_placeholders_with_metavars_proc proc(menv, new2old);
return proc(e);
}
static int mk_placeholder(lua_State * L) {
if (lua_gettop(L) == 0) {
return push_expr(L, mk_placeholder());
} else {
return push_expr(L, mk_placeholder(some_expr(to_expr(L, 1))));
}
}
void open_placeholder(lua_State * L) {
SET_GLOBAL_FUN(mk_placeholder, "mk_placeholder");
}
}

3
src/library/placeholder.h
View file

@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "util/lua.h"
#include "kernel/expr.h"
#include "kernel/expr_maps.h"
@ -33,4 +34,6 @@ bool has_placeholder(expr const & e);
\c s, we store <tt>(*new2old)[t] = s</tt>.
*/
expr replace_placeholders_with_metavars(expr const & e, metavar_env const & menv, expr_map<expr> * new2old = nullptr);
void open_placeholder(lua_State * L);
}

2
src/library/register_module.h
View file

@ -12,6 +12,7 @@ Author: Leonardo de Moura
#include "library/hidden_defs.h"
#include "library/substitution.h"
#include "library/fo_unify.h"
#include "library/placeholder.h"
namespace lean {
inline void open_core_module(lua_State * L) {
@ -21,6 +22,7 @@ inline void open_core_module(lua_State * L) {
open_hidden_defs(L);
open_substitution(L);
open_fo_unify(L);
open_placeholder(L);
}
inline void register_core_module() {
script_state::register_module(open_core_module);