feat(kernel/extension_context): add auxiliary methods

src/kernel/CMakeLists.txt

@@ -3,6 +3,6 @@ replace_fn.cpp free_vars.cpp abstract.cpp instantiate.cpp
 formatter.cpp declaration.cpp environment.cpp
 justification.cpp pos_info_provider.cpp metavar.cpp converter.cpp
 constraint.cpp type_checker.cpp error_msgs.cpp kernel_exception.cpp
-normalizer_extension.cpp init_module.cpp)
+normalizer_extension.cpp init_module.cpp extension_context.cpp)
 
 target_link_libraries(kernel ${LEAN_LIBS})

src/kernel/extension_context.cpp

@@ -0,0 +1,17 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "kernel/extension_context.h"
+#include "kernel/expr.h"
+
+namespace lean {
+expr extension_context::whnf(expr const & e, constraint_seq & cs) {
+    auto p = whnf(e); cs += p.second; return p.first;
+}
+expr extension_context::infer_type(expr const & e, constraint_seq & cs) {
+    auto p = infer_type(e); cs += p.second; return p.first;
+}
+}

src/kernel/extension_context.h

@@ -29,5 +29,7 @@ public:
     virtual pair<bool, constraint_seq> is_def_eq(expr const & e1, expr const & e2, delayed_justification & j) = 0;
     virtual pair<expr, constraint_seq> infer_type(expr const & e) = 0;
     virtual name mk_fresh_name() = 0;
+    expr whnf(expr const & e, constraint_seq & cs);
+    expr infer_type(expr const & e, constraint_seq & cs);
 };
 }