From 4f83b1a50b624c0ecf0f0124ffe15ab6bf4f73b1 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 11 Jun 2014 13:32:23 -0700 Subject: [PATCH] feat(library): add choice expressions Signed-off-by: Leonardo de Moura --- src/library/CMakeLists.txt | 2 +- src/library/choice.cpp | 85 +++++++++++++++++++++++++++++++++++ src/library/choice.h | 38 ++++++++++++++++ src/library/register_module.h | 4 +- tests/lua/choice.lua | 14 ++++++ 5 files changed, 140 insertions(+), 3 deletions(-) create mode 100644 src/library/choice.cpp create mode 100644 src/library/choice.h create mode 100644 tests/lua/choice.lua diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index f4fdcf38a..5054b9b0d 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -3,7 +3,7 @@ add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp resolve_macro.cpp kernel_serializer.cpp max_sharing.cpp normalize.cpp shared_environment.cpp module.cpp coercion.cpp private.cpp placeholder.cpp aliases.cpp scope.cpp level_names.cpp - update_declaration.cpp) + update_declaration.cpp choice.cpp) # hop_match.cpp) target_link_libraries(library ${LEAN_LIBS}) diff --git a/src/library/choice.cpp b/src/library/choice.cpp new file mode 100644 index 000000000..9128ad600 --- /dev/null +++ b/src/library/choice.cpp @@ -0,0 +1,85 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "util/sstream.h" +#include "library/choice.h" +#include "library/kernel_bindings.h" + +namespace lean { +static name g_choice_name("choice"); +// We encode a 'choice' expression using a macro. +// This is a trick to avoid creating a new kind of expression. +// 'Choice' expressions are temporary objects used by the elaborator, +// and have no semantic significance. +class choice_macro_cell : public macro_definition_cell { +public: + virtual name get_name() const { return g_choice_name; } + // Choice expressions must be replaced with metavariables before invoking the type checker. + // Choice expressions cannot be exported. They are transient/auxiliary objects. + virtual expr get_type(expr const &, expr const *, extension_context &) const { lean_unreachable(); } + virtual optional expand(expr const &, extension_context &) const { lean_unreachable(); } + virtual void write(serializer &) const { lean_unreachable(); } +}; + +static macro_definition g_choice(new choice_macro_cell()); +expr mk_choice(unsigned num_es, expr const * es) { + lean_assert(num_es > 0); + if (num_es == 1) + return es[0]; + else + return mk_macro(g_choice, num_es, es); +} + +bool is_choice(expr const & e) { + return is_macro(e) && macro_def(e) == g_choice; +} + +unsigned get_num_choices(expr const & e) { + lean_assert(is_choice(e)); + return macro_num_args(e); +} + +expr const & get_choice(expr const & e, unsigned i) { + lean_assert(is_choice(e)); + return macro_arg(e, i); +} + +static int mk_choice(lua_State * L) { + check_atleast_num_args(L, 1); + int nargs = lua_gettop(L); + buffer args; + for (int i = 1; i <= nargs; i++) + args.push_back(to_expr(L, i)); + return push_expr(L, mk_choice(args.size(), args.data())); +} + +static int is_choice(lua_State * L) { + return push_boolean(L, is_choice(to_expr(L, 1))); +} +static void check_choice(lua_State * L, int idx) { + if (!is_choice(to_expr(L, idx))) + throw exception(sstream() << "arg #" << idx << " is not a choice-expression"); +} +static int get_num_choices(lua_State * L) { + check_choice(L, 1); + return push_integer(L, get_num_choices(to_expr(L, 1))); +} +static int get_choice(lua_State * L) { + check_choice(L, 1); + expr const & c = to_expr(L, 1); + int i = lua_tointeger(L, 2); + if (i < 0 || static_cast(i) >= get_num_choices(c)) + throw exception("arg #2 is an invalid choice index"); + return push_expr(L, get_choice(c, i)); +} + +void open_choice(lua_State * L) { + SET_GLOBAL_FUN(mk_choice, "mk_choice"); + SET_GLOBAL_FUN(is_choice, "is_choice"); + SET_GLOBAL_FUN(get_num_choices, "get_num_choices"); + SET_GLOBAL_FUN(get_choice, "get_choice"); +} +} diff --git a/src/library/choice.h b/src/library/choice.h new file mode 100644 index 000000000..d111e36e4 --- /dev/null +++ b/src/library/choice.h @@ -0,0 +1,38 @@ +/* +Copyright (c) 2014 Microsoft Corporation. All rights reserved. +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" + +namespace lean { +/** + \brief Create a choice expression for the given expressions. + The elaborator decides which one should be used based on the type of the arguments. + + \remark if num_fs == 1, then return fs[0] + + \pre num_fs >= 1 +*/ +expr mk_choice(unsigned num_es, expr const * es); +/** \brief Return true iff \c e is an expression created using \c mk_choice. */ +bool is_choice(expr const & e); +/** + \brief Return the number of alternatives in a choice expression. + We have that get_num_choices(mk_choice(n, es)) == n whenever n >= 2. + + \pre is_choice(e) +*/ +unsigned get_num_choices(expr const & e); +/** + \brief Return the (i+1)-th alternative of a choice expression. + + \pre is_choice(e) + \pre i < get_num_choices(e) +*/ +expr const & get_choice(expr const & e, unsigned i); +void open_choice(lua_State * L); +} diff --git a/src/library/register_module.h b/src/library/register_module.h index c3e43f5a3..a1965a951 100644 --- a/src/library/register_module.h +++ b/src/library/register_module.h @@ -12,7 +12,7 @@ Author: Leonardo de Moura #include "library/private.h" #include "library/placeholder.h" #include "library/aliases.h" -// #include "library/fo_unify.h" +#include "library/choice.h" // #include "library/hop_match.h" namespace lean { @@ -23,7 +23,7 @@ inline void open_core_module(lua_State * L) { open_private(L); open_placeholder(L); open_aliases(L); - // open_fo_unify(L); + open_choice(L); // open_hop_match(L); } inline void register_core_module() { diff --git a/tests/lua/choice.lua b/tests/lua/choice.lua new file mode 100644 index 000000000..803fe31ae --- /dev/null +++ b/tests/lua/choice.lua @@ -0,0 +1,14 @@ +local f = Const("f") +local a = Const("a") +local c = mk_choice(f(a), a, f(f(a))) +print(c) +assert(is_choice(c)) +assert(get_num_choices(c) == 3) +assert(get_choice(c, 0) == f(a)) +assert(get_choice(c, 1) == a) +assert(get_choice(c, 2) == f(f(a))) +assert(mk_choice(f(a)) == f(a)) +check_error(function() mk_choice() end) +check_error(function() get_num_choices(f(a)) end) +check_error(function() get_choice(f(a)) end) +check_error(function() get_choice(c, 3) end)