feat(library): add choice expressions

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

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})

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<expr> 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<expr> 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<unsigned>(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");
+}
+}

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 <tt>get_num_choices(mk_choice(n, es)) == n</tt> whenever <tt>n >= 2</tt>.
+
+   \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);
+}

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() {

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)