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

feat(library/explicit): allow 'as-is', 'explicit' and 'implicit' annotations to be saved in .olean files

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-08-07 19:13:48 -07:00
parent 969afa8245
commit 24e8dca014
3 changed files with 15 additions and 31 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/kernel/annotation.cpp
View file

@ -76,7 +76,7 @@ bool is_annotation(expr const & e, name const & kind) {
return is_annotation(e) && static_cast<annotation_macro_definition_cell const*>(macro_def(e).raw())->get_annotation_kind() == kind;
}
expr get_annotation_arg(expr const & e) {
expr const & get_annotation_arg(expr const & e) {
lean_assert(is_annotation(e));
return macro_arg(e, 0);
}

2
src/kernel/annotation.h
View file

@ -33,7 +33,7 @@ bool is_annotation(expr const & e, name const & kind);
\post get_annotation_arg(mk_annotation(k, e)) == e
*/
expr get_annotation_arg(expr const & e);
expr const & get_annotation_arg(expr const & e);
/** \brief Tag \c e as a 'let'-expression. 'let' is a pre-registered annotation. */
expr mk_let_annotation(expr const & e);

42
src/library/explicit.cpp
View file

@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "util/sstream.h"
#include "kernel/annotation.h"
#include "library/explicit.h"
#include "library/kernel_bindings.h"
@ -12,37 +13,20 @@ namespace lean {
static name g_explicit_name("@");
static name g_implicit_name("@^-1");
static name g_as_is_name("as_is");
[[ noreturn ]] static void throw_ex(name const & n) { throw exception(sstream() << "unexpected occurrence of '" << n << "' expression"); }
// We encode the 'explicit' expression mark '@' using a macro.
// This is a trick to avoid creating a new kind of expression.
// 'Explicit' expressions are temporary objects used by the elaborator,
// and have no semantic significance.
class explicit_macro_cell : public macro_definition_cell {
public:
virtual bool operator==(macro_definition_cell const & other) const { return this == &other; }
virtual name get_name() const { return g_explicit_name; }
virtual expr get_type(expr const &, expr const *, extension_context &) const { throw_ex(get_name()); }
virtual optional<expr> expand(expr const &, extension_context &) const { throw_ex(get_name()); }
virtual void write(serializer &) const { throw_ex(get_name()); }
};
register_annotation_fn g_explicit_annotation(g_explicit_name);
register_annotation_fn g_implicit_annotation(g_implicit_name);
register_annotation_fn g_as_is_annotation(g_as_is_name);
struct as_is_macro_cell : public explicit_macro_cell { virtual name get_name() const { return g_as_is_name; } };
struct implicit_macro_cell : public explicit_macro_cell { virtual name get_name() const { return g_implicit_name; } };
static macro_definition g_explicit(new explicit_macro_cell());
static macro_definition g_as_is(new as_is_macro_cell());
static macro_definition g_implicit(new implicit_macro_cell());
expr mk_explicit(expr const & e) { return mk_macro(g_explicit, 1, &e); }
bool is_explicit(expr const & e) { return is_macro(e) && macro_def(e) == g_explicit; }
expr mk_as_is(expr const & e) { return mk_macro(g_as_is, 1, &e); }
bool is_as_is(expr const & e) { return is_macro(e) && macro_def(e) == g_as_is; }
expr mk_implicit(expr const & e) { return mk_macro(g_implicit, 1, &e); }
bool is_implicit(expr const & e) { return is_macro(e) && macro_def(e) == g_implicit; }
expr const & get_explicit_arg(expr const & e) { lean_assert(is_explicit(e)); return macro_arg(e, 0); }
expr const & get_as_is_arg(expr const & e) { lean_assert(is_as_is(e)); return macro_arg(e, 0); }
expr const & get_implicit_arg(expr const & e) { lean_assert(is_implicit(e)); return macro_arg(e, 0); }
expr mk_explicit(expr const & e) { return mk_annotation(g_explicit_name, e); }
bool is_explicit(expr const & e) { return is_annotation(e, g_explicit_name); }
expr mk_as_is(expr const & e) { return mk_annotation(g_as_is_name, e); }
bool is_as_is(expr const & e) { return is_annotation(e, g_as_is_name); }
expr mk_implicit(expr const & e) { return mk_annotation(g_implicit_name, e); }
bool is_implicit(expr const & e) { return is_annotation(e, g_implicit_name); }
expr const & get_explicit_arg(expr const & e) { lean_assert(is_explicit(e)); return get_annotation_arg(e); }
expr const & get_as_is_arg(expr const & e) { lean_assert(is_as_is(e)); return get_annotation_arg(e); }
expr const & get_implicit_arg(expr const & e) { lean_assert(is_implicit(e)); return get_annotation_arg(e); }
static int mk_explicit(lua_State * L) { return push_expr(L, mk_explicit(to_expr(L, 1))); }
static int is_explicit(lua_State * L) { return push_boolean(L, is_explicit(to_expr(L, 1))); }