From 3abfad7a88f86c922d9f73f1a54b3d0c9f83c553 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 26 Dec 2013 18:51:37 -0800 Subject: [PATCH] feat(frontends/lean/parser): add support for integer arguments in macros Signed-off-by: Leonardo de Moura --- src/frontends/lean/parser.cpp | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 154062dec..3172db7ae 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -131,7 +131,7 @@ static unsigned g_level_cup_prec = 5; // are syntax sugar for (Pi (_ : A), B) static name g_unused = name::mk_internal_unique_name(); -enum class macro_arg_kind { Expr, Exprs, Bindings, Id, String, Comma, Assign, Tactic, Tactics }; +enum class macro_arg_kind { Expr, Exprs, Bindings, Id, Int, String, Comma, Assign, Tactic, Tactics }; struct macro { list m_arg_kinds; luaref m_fn; @@ -1023,6 +1023,11 @@ class parser::imp { args.emplace_back(k, &str); return parse_macro(tail(arg_kinds), fn, prec, args, p); } + case macro_arg_kind::Int: { + unsigned i = parse_unsigned("invalid macro argument, value does not fit in a machine integer"); + args.emplace_back(k, &i); + return parse_macro(tail(arg_kinds), fn, prec, args, p); + } case macro_arg_kind::Id: { name n = curr_name(); next(); @@ -1088,6 +1093,9 @@ class parser::imp { case macro_arg_kind::String: lua_pushstring(L, static_cast(arg)->c_str()); break; + case macro_arg_kind::Int: + lua_pushinteger(L, *static_cast(arg)); + break; case macro_arg_kind::Tactic: push_tactic(L, *static_cast(arg)); break; @@ -2868,6 +2876,7 @@ void open_macros(lua_State * L) { SET_ENUM("Bindings", macro_arg_kind::Bindings); SET_ENUM("Id", macro_arg_kind::Id); SET_ENUM("String", macro_arg_kind::String); + SET_ENUM("Int", macro_arg_kind::Int); SET_ENUM("Comma", macro_arg_kind::Comma); SET_ENUM("Assign", macro_arg_kind::Assign); SET_ENUM("Tactic", macro_arg_kind::Tactic);