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

feat(kernel): add is_def_eq predicate in the extension_context API

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-15 09:31:11 -07:00
parent a6dc6060e2
commit 08ac9c1f05
3 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/kernel/converter.cpp
View file

@ -45,6 +45,7 @@ struct default_converter : public converter {
extended_context(default_converter & conv, context & ctx):m_conv(conv), m_ctx(ctx) {}
virtual environment const & env() const { return m_conv.m_env; }
virtual expr whnf(expr const & e) { return m_conv.whnf(e, m_ctx); }
virtual bool is_def_eq(expr const & e1, expr const & e2, delayed_justification & j) { return m_conv.is_def_eq(e1, e2, m_ctx, j); }
virtual expr infer_type(expr const & e) { return m_ctx.infer_type(e); }
virtual name mk_fresh_name() { return m_ctx.mk_fresh_name(); }
virtual void add_cnstr(constraint const & c) { m_ctx.add_cnstr(c); }

2
src/kernel/extension_context.h
View file

@ -11,6 +11,7 @@ namespace lean {
class expr;
class constraint;
class environment;
class delayed_justification;
/**
\brief Extension context (aka API provided to macro_definitions and normalizer_extensions).
@ -26,6 +27,7 @@ public:
virtual ~extension_context() {}
virtual environment const & env() const = 0;
virtual expr whnf(expr const & e) = 0;
virtual bool is_def_eq(expr const & e1, expr const & e2, delayed_justification & j) = 0;
virtual expr infer_type(expr const & e) = 0;
virtual name mk_fresh_name() = 0;
virtual void add_cnstr(constraint const & c) = 0;

1
src/kernel/type_checker.cpp
View file

@ -51,6 +51,7 @@ struct type_checker::imp {
type_checker_context(imp & i):m_imp(i) {}
virtual environment const & env() const { return m_imp.m_env; }
virtual expr whnf(expr const & e) { return m_imp.whnf(e); }
virtual bool is_def_eq(expr const & e1, expr const & e2, delayed_justification & j) { return m_imp.is_def_eq(e1, e2, j); }
virtual expr infer_type(expr const & e) { return m_imp.infer_type(e); }
virtual name mk_fresh_name() { return m_imp.m_gen.next(); }
virtual void add_cnstr(constraint const & c) { m_imp.add_cnstr(c); }