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

feat(library/definitional/equations): add support for serializing equations

Browse source
This commit is contained in:
Leonardo de Moura 2014-12-04 14:43:43 -08:00
parent 1d401ad862
commit e267b2d120
1 changed files with 43 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

53
src/library/definitional/equations.cpp
View file

@ -5,22 +5,25 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura Author: Leonardo de Moura
*/ */
#include "kernel/expr.h" #include "kernel/expr.h"
#include "library/kernel_serializer.h"
namespace lean { namespace lean {
static name * g_equations_name = nullptr; static name * g_equations_name = nullptr;
static name * g_equation_name = nullptr; static name * g_equation_name = nullptr;
static name * g_decreasing_name = nullptr; static name * g_decreasing_name = nullptr;
static std::string * g_equations_opcode = nullptr;
static std::string * g_equation_opcode = nullptr;
static std::string * g_decreasing_opcode = nullptr;
[[ noreturn ]] static void throw_eqs_ex() { throw exception("unexpected occurrence of 'equations' expression"); } [[ noreturn ]] static void throw_eqs_ex() { throw exception("unexpected occurrence of 'equations' expression"); }
[[ noreturn ]] static void throw_eq_ex() { throw exception("unexpected occurrence of 'equation' expression"); } [[ noreturn ]] static void throw_eq_ex() { throw exception("unexpected occurrence of 'equation' expression"); }
[[ noreturn ]] static void throw_dec_ex() { throw exception("unexpected occurrence of 'decreasing' expression"); }
class equations_macro_cell : public macro_definition_cell { class equations_macro_cell : public macro_definition_cell {
public: public:
virtual name get_name() const { return *g_equations_name; } virtual name get_name() const { return *g_equations_name; }
virtual pair<expr, constraint_seq> get_type(expr const &, extension_context &) const { throw_eqs_ex(); } virtual pair<expr, constraint_seq> get_type(expr const &, extension_context &) const { throw_eqs_ex(); }
virtual optional<expr> expand(expr const &, extension_context &) const { throw_eqs_ex(); } virtual optional<expr> expand(expr const &, extension_context &) const { throw_eqs_ex(); }
virtual void write(serializer &) const { throw_eqs_ex(); } virtual void write(serializer & s) const { s.write_string(*g_equations_opcode); }
}; };
class equation_macro_cell : public macro_definition_cell { class equation_macro_cell : public macro_definition_cell {
@ -28,7 +31,7 @@ public:
virtual name get_name() const { return *g_equation_name; } virtual name get_name() const { return *g_equation_name; }
virtual pair<expr, constraint_seq> get_type(expr const &, extension_context &) const { throw_eq_ex(); } virtual pair<expr, constraint_seq> get_type(expr const &, extension_context &) const { throw_eq_ex(); }
virtual optional<expr> expand(expr const &, extension_context &) const { throw_eq_ex(); } virtual optional<expr> expand(expr const &, extension_context &) const { throw_eq_ex(); }
virtual void write(serializer &) const { throw_eq_ex(); } virtual void write(serializer & s) const { s.write_string(*g_equation_opcode); }
}; };
class decreasing_macro_cell : public macro_definition_cell { class decreasing_macro_cell : public macro_definition_cell {
@ -47,7 +50,7 @@ public:
check_macro(m); check_macro(m);
return some_expr(macro_arg(m, 0)); return some_expr(macro_arg(m, 0));
} }
virtual void write(serializer &) const { throw_dec_ex(); } virtual void write(serializer & s) const { s.write_string(*g_decreasing_opcode); }
}; };
static macro_definition * g_equations = nullptr; static macro_definition * g_equations = nullptr;
@ -107,15 +110,45 @@ expr mk_equations(unsigned num, expr const * eqns, expr const & Hwf) {
} }
void initialize_equations() { void initialize_equations() {
g_equations_name = new name("equations"); g_equations_name = new name("equations");
g_equation_name = new name("equation"); g_equation_name = new name("equation");
g_decreasing_name = new name("decreasing"); g_decreasing_name = new name("decreasing");
g_equations = new macro_definition(new equations_macro_cell()); g_equations = new macro_definition(new equations_macro_cell());
g_equation = new macro_definition(new equation_macro_cell()); g_equation = new macro_definition(new equation_macro_cell());
g_decreasing = new macro_definition(new decreasing_macro_cell()); g_decreasing = new macro_definition(new decreasing_macro_cell());
g_equations_opcode = new std::string("Eqns");
g_equation_opcode = new std::string("Eqn");
g_decreasing_opcode = new std::string("Decr");
register_macro_deserializer(*g_equations_opcode,
[](deserializer &, unsigned num, expr const * args) {
if (num == 0)
throw corrupted_stream_exception();
if (!is_equation(args[num-1])) {
if (num == 1)
throw corrupted_stream_exception();
return mk_equations(num-1, args, args[num-1]);
} else {
return mk_equations(num, args);
}
});
register_macro_deserializer(*g_equation_opcode,
[](deserializer &, unsigned num, expr const * args) {
if (num != 2)
throw corrupted_stream_exception();
return mk_equation(args[0], args[1]);
});
register_macro_deserializer(*g_decreasing_opcode,
[](deserializer &, unsigned num, expr const * args) {
if (num != 2)
throw corrupted_stream_exception();
return mk_decreasing(args[0], args[1]);
});
} }
void finalize_equations() { void finalize_equations() {
delete g_equation_opcode;
delete g_equations_opcode;
delete g_decreasing_opcode;
delete g_equations; delete g_equations;
delete g_equation; delete g_equation;
delete g_decreasing; delete g_decreasing;