refactor(kernel): define extension_context API for normalizer_extesions and macro_definitions

A particular macro definition may use the extra information to retrieve information necessary to expand/type a given macro application. Example: it may need to invoke whnf.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/kernel/environment.h

@@ -29,26 +29,7 @@ class certified_definition;
 */
 class normalizer_extension {
 public:
-    /**
+    virtual optional<expr> operator()(expr const & e, extension_context const & ctx) const;
-        \brief Normalization extension context (aka API provided to the normalizer_extension procedure).
-        The extension can request
-         1) the environment being used.
-         2) the weak head normal form of an expression.
-         3) the type of an expression.
-         4) a new fresh name
-         A normalizer extension can also add a new constraint.
-    */
-    class context {
-    public:
-        virtual ~context() {}
-        virtual environment const & env() const = 0;
-        virtual expr whnf(expr const & e) = 0;
-        virtual expr infer_type(expr const & e) = 0;
-        virtual name mk_fresh_name() = 0;
-        virtual void add_cnstr(constraint const & c) = 0;
-    };
-
-    virtual optional<expr> operator()(expr const & e, context const & ctx) const;
 };
 
 /**

src/kernel/expr.cpp

@@ -1,5 +1,5 @@
 /*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Copyright (c) 2013-2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura

src/kernel/expr.h

@@ -1,5 +1,5 @@
 /*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Copyright (c) 2013-2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
@@ -22,6 +22,7 @@ Author: Leonardo de Moura
 #include "util/serializer.h"
 #include "util/sexpr/format.h"
 #include "kernel/level.h"
+#include "kernel/extension_context.h"
 
 namespace lean {
 class expr;
@@ -260,9 +261,9 @@ public:
     macro_definition():m_rc(0) {}
     virtual ~macro_definition() {}
     virtual name get_name() const = 0;
-    virtual expr get_type(unsigned num, expr const * args, expr const * arg_types) const = 0;
+    virtual expr get_type(unsigned num, expr const * args, expr const * arg_types, extension_context const & ctx) const = 0;
-    virtual optional<expr> expand1(unsigned num, expr const * args) const = 0;
+    virtual optional<expr> expand1(unsigned num, expr const * args, extension_context const & ctx) const = 0;
-    virtual optional<expr> expand(unsigned num, expr const * args) const = 0;
+    virtual optional<expr> expand(unsigned num, expr const * args, extension_context const & ctx) const = 0;
     virtual unsigned trust_level() const = 0;
     virtual int push_lua(lua_State * L) const;
     virtual bool operator==(macro_definition const & other) const;

src/kernel/extension_context.h

@@ -0,0 +1,33 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "util/name.h"
+
+namespace lean {
+class expr;
+class constraint;
+class environment;
+
+/**
+   \brief Extension context (aka API provided to macro_definitions and normalizer_extensions).
+   The extension can request
+   1) the environment being used.
+   2) the weak head normal form of an expression.
+   3) the type of an expression.
+   4) a new fresh name.
+   5) registration of a new constraint.
+*/
+class extension_context {
+public:
+    virtual ~extension_context() {}
+    virtual environment const & env() const = 0;
+    virtual expr whnf(expr const & e) = 0;
+    virtual expr infer_type(expr const & e) = 0;
+    virtual name mk_fresh_name() = 0;
+    virtual void add_cnstr(constraint const & c) = 0;
+};
+}

src/kernel/type_checker.cpp

@@ -40,10 +40,10 @@ struct type_checker::imp {
         optional<module_idx> mod_idx, bool memoize, name_set const & extra_opaque):
         m_env(env), m_gen(g), m_chandler(h), m_module_idx(mod_idx), m_memoize(memoize), m_extra_opaque(extra_opaque) {}
 
-    class normalizer_context : public normalizer_extension::context {
+    class type_checker_context : public extension_context {
         imp & m_imp;
     public:
-        normalizer_context(imp & i):m_imp(i) {}
+        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 expr infer_type(expr const & e) { return m_imp.infer_type(e); }
@@ -58,7 +58,8 @@ struct type_checker::imp {
     expr mk_rev_app(expr const & f, unsigned num, expr const * args) { return max_sharing(lean::mk_rev_app(f, num, args)); }
     optional<expr> expand_macro(expr const & m) {
         lean_assert(is_macro(m));
-        if (auto new_m = macro_def(m).expand(macro_num_args(m), macro_args(m)))
+        type_checker_context ctx(*this);
+        if (auto new_m = macro_def(m).expand(macro_num_args(m), macro_args(m), ctx))
             return some_expr(max_sharing(*new_m));
         else
             return none_expr();
@@ -68,7 +69,7 @@ struct type_checker::imp {
     }
     /** \brief Apply normalizer extensions to \c e. */
     optional<expr> norm_ext(expr const & e) {
-        normalizer_context ctx(*this);
+        type_checker_context ctx(*this);
         if (auto new_e = m_env.norm_ext()(e, ctx))
             return some_expr(max_sharing(*new_e));
         else
@@ -662,7 +663,8 @@ struct type_checker::imp {
             buffer<expr> arg_types;
             for (unsigned i = 0; i < macro_num_args(e); i++)
                 arg_types.push_back(infer_type_core(macro_arg(e, i), infer_only));
-            r = macro_def(e).get_type(macro_num_args(e), macro_args(e), arg_types.data());
+            type_checker_context ctx(*this);
+            r = macro_def(e).get_type(macro_num_args(e), macro_args(e), arg_types.data(), ctx);
             if (!infer_only && macro_def(e).trust_level() <= m_env.trust_lvl()) {
                 optional<expr> m = expand_macro(e);
                 if (!m)