max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: exception while tracing in the old frontend

Browse source
This commit is contained in:
Sebastian Ullrich 2020-10-22 14:43:54 +02:00
parent 00a3c2ac56
commit b562cb8a2a
8 changed files with 18 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/parser.cpp
View file

@ -2058,6 +2058,8 @@ public:
lazy_type_context(environment const & env, options const & opts):m_env(env), m_opts(opts) {}
virtual ~lazy_type_context() {}
virtual environment const & env() const override { return const_cast<lazy_type_context*>(this)->ctx().env(); }
virtual local_context const & lctx() const override { return const_cast<lazy_type_context*>(this)->ctx().lctx(); }
virtual metavar_context const & mctx() const override { return const_cast<lazy_type_context*>(this)->ctx().mctx(); }
virtual expr whnf(expr const & e) override { return ctx().whnf(e); }
virtual bool is_def_eq(expr const & e1, expr const & e2) override { return ctx().is_def_eq(e1, e2); }
virtual expr infer(expr const & e) override { return ctx().infer(e); }

3
src/frontends/lean/pp.cpp
View file

@ -17,8 +17,7 @@ formatter_factory mk_pretty_formatter_factory() {
return [](environment const & env, options const & o, abstract_type_context & ctx) { // NOLINT
return formatter(o, [&](expr const & e, options const & new_o) {
// what could ever go wrong
type_context_old & tctx = dynamic_cast<type_context_old &>(ctx);
return get_io_result<format>(lean_pp_expr(env.to_obj_arg(), tctx.mctx().to_obj_arg(), tctx.lctx().to_obj_arg(), new_o.to_obj_arg(), e.to_obj_arg(), box(0)));
return get_io_result<format>(lean_pp_expr(env.to_obj_arg(), ctx.mctx().to_obj_arg(), ctx.lctx().to_obj_arg(), new_o.to_obj_arg(), e.to_obj_arg(), box(0)));
});
};
}

4
src/library/abstract_type_context.h
View file

@ -6,12 +6,16 @@ Author: Leonardo de Moura
*/
#pragma once
#include "kernel/expr.h"
#include "library/local_context.h"
#include "library/metavar_context.h"
namespace lean {
class abstract_type_context {
public:
virtual ~abstract_type_context() {}
virtual environment const & env() const = 0;
virtual local_context const & lctx() const = 0;
virtual metavar_context const & mctx() const = 0;
virtual expr whnf(expr const & e) = 0;
virtual name next_name() = 0;
virtual expr relaxed_whnf(expr const & e) { return whnf(e); }

4
src/library/type_context.h
View file

@ -575,8 +575,8 @@ public:
}
local_context const & lctx() const { return m_lctx; }
metavar_context const & mctx() const { return m_mctx; }
virtual local_context const & lctx() const override { return m_lctx; }
virtual metavar_context const & mctx() const override { return m_mctx; }
expr mk_metavar_decl(local_context const & ctx, expr const & type) { return m_mctx.mk_metavar_decl(ctx, type); }
expr mk_metavar_decl(name const & pp_n, local_context const & ctx, expr const & type) { return m_mctx.mk_metavar_decl(pp_n, ctx, type); }
optional<metavar_decl> find_metavar_decl(expr const & mvar) const { return m_mctx.find_metavar_decl(mvar); }

2
stage0/src/frontends/lean/parser.cpp generated
View file

@ -2058,6 +2058,8 @@ public:
lazy_type_context(environment const & env, options const & opts):m_env(env), m_opts(opts) {}
virtual ~lazy_type_context() {}
virtual environment const & env() const override { return const_cast<lazy_type_context*>(this)->ctx().env(); }
virtual local_context const & lctx() const override { return const_cast<lazy_type_context*>(this)->ctx().lctx(); }
virtual metavar_context const & mctx() const override { return const_cast<lazy_type_context*>(this)->ctx().mctx(); }
virtual expr whnf(expr const & e) override { return ctx().whnf(e); }
virtual bool is_def_eq(expr const & e1, expr const & e2) override { return ctx().is_def_eq(e1, e2); }
virtual expr infer(expr const & e) override { return ctx().infer(e); }

3
stage0/src/frontends/lean/pp.cpp generated
View file

@ -17,8 +17,7 @@ formatter_factory mk_pretty_formatter_factory() {
return [](environment const & env, options const & o, abstract_type_context & ctx) { // NOLINT
return formatter(o, [&](expr const & e, options const & new_o) {
// what could ever go wrong
type_context_old & tctx = dynamic_cast<type_context_old &>(ctx);
return get_io_result<format>(lean_pp_expr(env.to_obj_arg(), tctx.mctx().to_obj_arg(), tctx.lctx().to_obj_arg(), new_o.to_obj_arg(), e.to_obj_arg(), box(0)));
return get_io_result<format>(lean_pp_expr(env.to_obj_arg(), ctx.mctx().to_obj_arg(), ctx.lctx().to_obj_arg(), new_o.to_obj_arg(), e.to_obj_arg(), box(0)));
});
};
}

4
stage0/src/library/abstract_type_context.h generated
View file

@ -6,12 +6,16 @@ Author: Leonardo de Moura
*/
#pragma once
#include "kernel/expr.h"
#include "library/local_context.h"
#include "library/metavar_context.h"
namespace lean {
class abstract_type_context {
public:
virtual ~abstract_type_context() {}
virtual environment const & env() const = 0;
virtual local_context const & lctx() const = 0;
virtual metavar_context const & mctx() const = 0;
virtual expr whnf(expr const & e) = 0;
virtual name next_name() = 0;
virtual expr relaxed_whnf(expr const & e) { return whnf(e); }

4
stage0/src/library/type_context.h generated
View file

@ -575,8 +575,8 @@ public:
}
local_context const & lctx() const { return m_lctx; }
metavar_context const & mctx() const { return m_mctx; }
virtual local_context const & lctx() const override { return m_lctx; }
virtual metavar_context const & mctx() const override { return m_mctx; }
expr mk_metavar_decl(local_context const & ctx, expr const & type) { return m_mctx.mk_metavar_decl(ctx, type); }
expr mk_metavar_decl(name const & pp_n, local_context const & ctx, expr const & type) { return m_mctx.mk_metavar_decl(pp_n, ctx, type); }
optional<metavar_decl> find_metavar_decl(expr const & mvar) const { return m_mctx.find_metavar_decl(mvar); }