From 70b7e519f8aae25fc7fe999318f7e6ca78876bd0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 14 Dec 2013 15:54:49 -0800 Subject: [PATCH] feat(library/type_inferer): provide the metavar_env to instantiate and lift_free_vars in the type_inferer, it will minimize the number of local_entries needed Signed-off-by: Leonardo de Moura --- src/library/type_inferer.cpp | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/src/library/type_inferer.cpp b/src/library/type_inferer.cpp index 01345a618..29cb6da8b 100644 --- a/src/library/type_inferer.cpp +++ b/src/library/type_inferer.cpp @@ -32,7 +32,18 @@ class type_inferer::imp { cache m_cache; expr normalize(expr const & e, context const & ctx) { - return m_normalizer(e, ctx); + return m_normalizer(e, ctx, m_menv.to_some_menv()); + } + expr lift_free_vars(expr const & e, unsigned s, unsigned d) { + return ::lean::lift_free_vars(e, s, d, m_menv.to_some_menv()); + } + + expr lift_free_vars(expr const & e, unsigned d) { + return ::lean::lift_free_vars(e, d, m_menv.to_some_menv()); + } + + expr instantiate(expr const & e, unsigned n, expr const * s) { + return ::lean::instantiate(e, n, s, m_menv.to_some_menv()); } expr check_type(expr const & e, expr const & s, context const & ctx) {