From 5a4bc331d2e3717eab72063f84821587d19a4837 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 15 Sep 2013 19:37:59 -0700 Subject: [PATCH] Make unification_problems a virtual class. Associate a 'standard' context with each metavariable in metavar_env Signed-off-by: Leonardo de Moura --- src/kernel/metavar.cpp | 22 +++++++++++----------- src/kernel/metavar.h | 33 +++++++++++++++++---------------- src/tests/kernel/metavar.cpp | 16 +++++++++++++++- 3 files changed, 43 insertions(+), 28 deletions(-) diff --git a/src/kernel/metavar.cpp b/src/kernel/metavar.cpp index cc2aac384..359da766c 100644 --- a/src/kernel/metavar.cpp +++ b/src/kernel/metavar.cpp @@ -12,9 +12,9 @@ Author: Leonardo de Moura #include "kernel/for_each.h" namespace lean { -expr metavar_env::mk_metavar() { +expr metavar_env::mk_metavar(context const & ctx) { unsigned midx = m_env.size(); - m_env.push_back(mk_pair(expr(), expr())); + m_env.push_back(data(ctx)); return ::lean::mk_metavar(midx); } @@ -23,34 +23,34 @@ bool metavar_env::contains(unsigned midx) const { } bool metavar_env::is_assigned(unsigned midx) const { - return m_env[midx].first; + return m_env[midx].m_subst; } expr metavar_env::get_subst(unsigned midx) const { - return m_env[midx].first; + return m_env[midx].m_subst; } expr metavar_env::get_type(unsigned midx, unification_problems & up) { auto p = m_env[midx]; - expr t = p->second; + expr t = p->m_type; if (t) { return t; } else { t = mk_metavar(); - expr s = p->first; - m_env[midx] = mk_pair(s, t); + expr s = p->m_subst; + m_env[midx] = data(s, t, p->m_ctx); if (s) - up.add_type_of_eq(s, t); + up.add_type_of_eq(p->m_ctx, s, t); else - up.add_type_of_eq(::lean::mk_metavar(midx), t); + up.add_type_of_eq(p->m_ctx, ::lean::mk_metavar(midx), t); return t; } } -void metavar_env::assign(unsigned midx, expr const & t) { +void metavar_env::assign(unsigned midx, expr const & v) { lean_assert(!is_assigned(midx)); auto p = m_env[midx]; - m_env[midx] = mk_pair(t, p->second); + m_env[midx] = data(v, p->m_type, p->m_ctx); } expr subst(expr const & a, unsigned i, expr const & c) { diff --git a/src/kernel/metavar.h b/src/kernel/metavar.h index b7b508d3a..e843a8271 100644 --- a/src/kernel/metavar.h +++ b/src/kernel/metavar.h @@ -5,35 +5,29 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once -#include -#include #include "util/pair.h" #include "util/pvector.h" #include "kernel/expr.h" +#include "kernel/context.h" namespace lean { /** \brief Set of unification problems that need to be solved. It store two kinds of problems: - 1. lhs == rhs - 2. typeof(n) == t + 1. ctx |- lhs == rhs + 2. ctx |- typeof(n) == t */ class unification_problems { - std::vector> m_eqs; - std::vector> m_type_of_eqs; public: + virtual ~unification_problems() {} /** - \brief Add a new unification problem of the form lhs == rhs + \brief Add a new unification problem of the form ctx |- lhs == rhs */ - void add_eq(expr const & lhs, expr const & rhs) { m_eqs.push_back(mk_pair(lhs, rhs)); } - + virtual void add_eq(context const & ctx, expr const & lhs, expr const & rhs) = 0; /** - \brief Add a new unification problem of the form typeof(n) == t + \brief Add a new unification problem of the form ctx |- typeof(n) == t */ - void add_type_of_eq(expr const & n, expr const & t) { m_type_of_eqs.push_back(mk_pair(n, t)); } - - std::vector> const & eqs() const { return m_eqs; } - std::vector> const & type_of_eqs() const { return m_type_of_eqs; } + virtual void add_type_of_eq(context const & ctx, expr const & n, expr const & t) = 0; }; /** @@ -41,12 +35,19 @@ public: from metavariables to assignments and types. */ class metavar_env { - pvector> m_env; + struct data { + expr m_subst; + expr m_type; + context m_ctx; + data(context const & ctx):m_ctx(ctx) {} + data(expr const & s, expr const & t, context const & ctx):m_subst(s), m_type(t), m_ctx(ctx) {} + }; + pvector m_env; public: /** \brief Create new metavariable in this environment. */ - expr mk_metavar(); + expr mk_metavar(context const & ctx = context()); /** \brief Return true if this environment contains a metavariable diff --git a/src/tests/kernel/metavar.cpp b/src/tests/kernel/metavar.cpp index 9df9e72f3..798b65c74 100644 --- a/src/tests/kernel/metavar.cpp +++ b/src/tests/kernel/metavar.cpp @@ -5,6 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include +#include +#include #include "util/test.h" #include "kernel/metavar.h" #include "kernel/instantiate.h" @@ -13,8 +15,20 @@ Author: Leonardo de Moura #include "library/printer.h" using namespace lean; +class unification_problems_dbg : public unification_problems { + std::vector> m_eqs; + std::vector> m_type_of_eqs; +public: + unification_problems_dbg() {} + virtual ~unification_problems_dbg() {} + virtual void add_eq(context const &, expr const & lhs, expr const & rhs) { m_eqs.push_back(mk_pair(lhs, rhs)); } + virtual void add_type_of_eq(context const &, expr const & n, expr const & t) { m_type_of_eqs.push_back(mk_pair(n, t)); } + std::vector> const & eqs() const { return m_eqs; } + std::vector> const & type_of_eqs() const { return m_type_of_eqs; } +}; + static void tst1() { - unification_problems u; + unification_problems_dbg u; metavar_env menv; expr m1 = menv.mk_metavar(); lean_assert(!menv.is_assigned(m1));