From 3a19d9fee1fb1cf1d75dbcd47e5b7419fac27d74 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 15 May 2014 10:29:35 -0700
Subject: [PATCH] refactor(kernel): revise macro_definition API

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/kernel/converter.cpp    |  2 +-
 src/kernel/expr.h           | 14 ++++++--------
 src/kernel/type_checker.cpp |  8 ++------
 3 files changed, 9 insertions(+), 15 deletions(-)

diff --git a/src/kernel/converter.cpp b/src/kernel/converter.cpp
index 76d420041..ee9344dc2 100644
--- a/src/kernel/converter.cpp
+++ b/src/kernel/converter.cpp
@@ -54,7 +54,7 @@ struct default_converter : public converter {
     optional<expr> expand_macro(expr const & m, context & c) {
         lean_assert(is_macro(m));
         extended_context xctx(*this, c);
-        return macro_def(m).expand(macro_num_args(m), macro_args(m), xctx);
+        return macro_def(m).expand(m, xctx);
     }
 
     /** \brief Apply normalizer extensions to \c e. */
diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index f55c3daa7..876d11ab8 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -297,9 +297,9 @@ public:
     macro_definition_cell():m_rc(0) {}
     virtual ~macro_definition_cell() {}
     virtual name get_name() const = 0;
-    virtual expr get_type(unsigned num, expr const * args, expr const * arg_types, extension_context & ctx) const = 0;
-    virtual optional<expr> expand1(unsigned num, expr const * args, extension_context & ctx) const = 0;
-    virtual optional<expr> expand(unsigned num, expr const * args, extension_context & ctx) const = 0;
+    virtual expr get_type(expr const & m, expr const * arg_types, extension_context & ctx) const = 0;
+    virtual optional<expr> expand(expr const & m, extension_context & ctx) const = 0;
+    virtual optional<expr> expand1(expr const & m, extension_context & ctx) const { return expand(m, ctx); }
     virtual unsigned trust_level() const;
     virtual bool operator==(macro_definition_cell const & other) const;
     virtual void display(std::ostream & out) const;
@@ -330,11 +330,9 @@ public:
     macro_definition & operator=(macro_definition && s);
 
     name get_name() const { return m_ptr->get_name(); }
-    expr get_type(unsigned num, expr const * args, expr const * arg_types, extension_context & ctx) const {
-        return m_ptr->get_type(num, args, arg_types, ctx);
-    }
-    optional<expr> expand1(unsigned num, expr const * args, extension_context & ctx) const { return m_ptr->expand1(num, args, ctx); }
-    optional<expr> expand(unsigned num, expr const * args, extension_context & ctx) const { return m_ptr->expand(num, args, ctx); }
+    expr get_type(expr const & m, expr const * arg_types, extension_context & ctx) const { return m_ptr->get_type(m, arg_types, ctx); }
+    optional<expr> expand(expr const & m, extension_context & ctx) const { return m_ptr->expand(m, ctx); }
+    optional<expr> expand1(expr const & m, extension_context & ctx) const { return m_ptr->expand1(m, ctx); }
     unsigned trust_level() const { return m_ptr->trust_level(); }
     bool operator==(macro_definition const & other) const { return m_ptr->operator==(*other.m_ptr); }
     bool operator!=(macro_definition const & other) const { return !operator==(other); }
diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index 9e866af11..79cc99ae5 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -13,7 +13,6 @@ Author: Leonardo de Moura
 #include "kernel/type_checker.h"
 #include "kernel/expr_maps.h"
 #include "kernel/instantiate.h"
-#include "kernel/max_sharing.h"
 #include "kernel/free_vars.h"
 #include "kernel/metavar.h"
 #include "kernel/error_msgs.h"
@@ -78,10 +77,7 @@ struct type_checker::imp {
 
     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), m_tc_ctx))
-            return some_expr(max_sharing(*new_m));
-        else
-            return none_expr();
+        return macro_def(m).expand(m, m_tc_ctx);
     }
 
     /**
@@ -319,7 +315,7 @@ 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(), m_tc_ctx);
+            r = macro_def(e).get_type(e, arg_types.data(), m_tc_ctx);
             if (!infer_only && macro_def(e).trust_level() <= m_env.trust_lvl()) {
                 optional<expr> m = expand_macro(e);
                 if (!m)