feat(kernel): add combinator for combining normalizer_extensions

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

src/kernel/CMakeLists.txt

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

src/kernel/environment.cpp

@@ -12,15 +12,6 @@ Author: Leonardo de Moura
 #include "kernel/kernel_exception.h"
 
 namespace lean {
-/**
-   \brief "Do nothing" normalizer extension.
-*/
-class noop_normalizer_extension : public normalizer_extension {
-public:
-    virtual optional<expr> operator()(expr const &, extension_context &) const { return none_expr(); }
-    virtual bool may_reduce_later(expr const &, extension_context &) const { return false; }
-};
-
 environment_header::environment_header(unsigned trust_lvl, bool prop_proof_irrel, bool eta, bool impredicative,
                                        list<name> const & cls_proof_irrel, std::unique_ptr<normalizer_extension const> ext):
     m_trust_lvl(trust_lvl), m_prop_proof_irrel(prop_proof_irrel), m_eta(eta), m_impredicative(impredicative),
@@ -83,7 +74,7 @@ environment::environment(header const & h, environment_id const & ancestor, decl
     m_header(h), m_id(environment_id::mk_descendant(ancestor)), m_declarations(d), m_global_levels(g), m_extensions(exts) {}
 
 environment::environment(unsigned trust_lvl, bool prop_proof_irrel, bool eta, bool impredicative, list<name> const & cls_proof_irrel):
-    environment(trust_lvl, prop_proof_irrel, eta, impredicative, cls_proof_irrel, std::unique_ptr<normalizer_extension>(new noop_normalizer_extension()))
+    environment(trust_lvl, prop_proof_irrel, eta, impredicative, cls_proof_irrel, mk_id_normalizer_extension())
 {}
 
 environment::environment(unsigned trust_lvl, bool prop_proof_irrel, bool eta, bool impredicative, list<name> const & cls_proof_irrel,

src/kernel/environment.h

@@ -16,6 +16,7 @@ Author: Leonardo de Moura
 #include "kernel/expr.h"
 #include "kernel/constraint.h"
 #include "kernel/declaration.h"
+#include "kernel/normalizer_extension.h"
 
 #ifndef LEAN_BELIEVER_TRUST_LEVEL
 // If an environment E is created with a trust level > LEAN_BELIEVER_TRUST_LEVEL, then
@@ -28,20 +29,6 @@ class type_checker;
 class environment;
 class certified_declaration;
 
-/**
-   \brief The Lean kernel can be instantiated with different normalization extensions.
-   Each extension is part of the trusted code base. The extensions allow us to support
-   different flavors of the core type theory. We will use these extensions to implement
-   inductive datatype (ala Coq), HIT, record types, etc.
-*/
-class normalizer_extension {
-public:
-    virtual ~normalizer_extension() {}
-    virtual optional<expr> operator()(expr const & e, extension_context & ctx) const = 0;
-    /** \brief Return true if the extension may reduce \c e after metavariables are instantiated. */
-    virtual bool may_reduce_later(expr const & e, extension_context & ctx) const = 0;
-};
-
 /**
    \brief The header of an environment is created when we create the empty environment.
    Moreover if environment B is an extension of environment A, then A and B share the same header.

src/kernel/inductive/inductive.cpp

@@ -94,6 +94,7 @@ Author: Leonardo de Moura
 namespace lean {
 namespace inductive {
 static name g_tmp_prefix = name::mk_internal_unique_name();
+static name g_inductive_extension("inductive_extension");
 
 /** \brief Environment extension used to store the computational rules associated with inductive datatype declarations. */
 struct inductive_env_ext : public environment_extension {
@@ -224,7 +225,7 @@ struct add_inductive_fn {
     /** \brief Return type of the i-th global parameter. */
     expr get_param_type(unsigned i) { return mlocal_type(m_param_consts[i]); }
 
-    /**
+     /**
        \brief Check if the type of datatypes is well typed, all inductive datatypes have the same parameters,
        and the number of parameters match the argument num_params.
 
@@ -732,7 +733,7 @@ struct add_inductive_fn {
     }
 
     environment operator()() {
-        if (!dynamic_cast<inductive_normalizer_extension const*>(&m_env.norm_ext()))
+        if (!m_env.norm_ext().supports(g_inductive_extension))
             throw kernel_exception(m_env, "environment does not support inductive datatypes");
         if (get_num_its() == 0)
             throw kernel_exception(m_env, "at least one inductive datatype declaration expected");
@@ -753,6 +754,10 @@ environment add_inductive(environment                  env,
     return add_inductive_fn(env, level_params, num_params, decls)();
 }
 
+bool inductive_normalizer_extension::supports(name const & feature) const {
+    return feature == g_inductive_extension;
+}
+
 optional<expr> inductive_normalizer_extension::operator()(expr const & e, extension_context & ctx) const {
     // Reduce terms \c e of the form
     //    elim_k A C e p[A,b] (intro_k_i A b u)

src/kernel/inductive/inductive.h

@@ -18,6 +18,7 @@ class inductive_normalizer_extension : public normalizer_extension {
 public:
     virtual optional<expr> operator()(expr const & e, extension_context & ctx) const;
     virtual bool may_reduce_later(expr const & e, extension_context & ctx) const;
+    virtual bool supports(name const & feature) const;
 };
 
 /** \brief Introduction rule */

src/kernel/normalizer_extension.cpp

@@ -0,0 +1,47 @@
+/*
+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/normalizer_extension.h"
+
+namespace lean {
+class id_normalizer_extension : public normalizer_extension {
+public:
+    virtual optional<expr> operator()(expr const &, extension_context &) const { return none_expr(); }
+    virtual bool may_reduce_later(expr const &, extension_context &) const { return false; }
+    virtual bool supports(name const &) const { return false; }
+};
+
+std::unique_ptr<normalizer_extension> mk_id_normalizer_extension() {
+    return std::unique_ptr<normalizer_extension>(new id_normalizer_extension());
+}
+
+class comp_normalizer_extension : public normalizer_extension {
+    std::unique_ptr<normalizer_extension> m_ext1;
+    std::unique_ptr<normalizer_extension> m_ext2;
+public:
+    comp_normalizer_extension(std::unique_ptr<normalizer_extension> && ext1, std::unique_ptr<normalizer_extension> && ext2):
+        m_ext1(std::move(ext1)), m_ext2(std::move(ext2)) {}
+
+    virtual optional<expr> operator()(expr const & e, extension_context & ctx) const {
+        if (auto r = (*m_ext1)(e, ctx))
+            return r;
+        else
+            return (*m_ext2)(e, ctx);
+    }
+
+    virtual bool may_reduce_later(expr const & e, extension_context & ctx) const {
+        return m_ext1->may_reduce_later(e, ctx) || m_ext2->may_reduce_later(e, ctx);
+    }
+
+    virtual bool supports(name const & feature) const {
+        return m_ext1->supports(feature) || m_ext2->supports(feature);
+    }
+};
+
+std::unique_ptr<normalizer_extension> compose(std::unique_ptr<normalizer_extension> && ext1, std::unique_ptr<normalizer_extension> && ext2) {
+    return std::unique_ptr<normalizer_extension>(new comp_normalizer_extension(std::move(ext1), std::move(ext2)));
+}
+}

src/kernel/normalizer_extension.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 "kernel/expr.h"
+
+namespace lean {
+/**
+   \brief The Lean kernel can be instantiated with different normalization extensions.
+   Each extension is part of the trusted code base. The extensions allow us to support
+   different flavors of the core type theory. We will use these extensions to implement
+   inductive datatype (ala Coq), HIT, record types, etc.
+*/
+class normalizer_extension {
+public:
+    virtual ~normalizer_extension() {}
+    virtual optional<expr> operator()(expr const & e, extension_context & ctx) const = 0;
+    /** \brief Return true if the extension may reduce \c e after metavariables are instantiated. */
+    virtual bool may_reduce_later(expr const & e, extension_context & ctx) const = 0;
+    /** \brief Return true iff the extension supports a feature with the given name,
+        this method is only used for sanity checking. */
+    virtual bool supports(name const & feature) const = 0;
+};
+
+/** \brief Create the do-nothing normalizer extension */
+std::unique_ptr<normalizer_extension> mk_id_normalizer_extension();
+
+/** \brief Create the composition of two normalizer extensions */
+std::unique_ptr<normalizer_extension> compose(std::unique_ptr<normalizer_extension> && ext1, std::unique_ptr<normalizer_extension> && ext2);
+}

src/kernel/record/record.cpp

@@ -51,4 +51,16 @@ environment add_record(environment const & env, level_param_names const & level_
                        name const & intro_name, expr const & intro_type) {
     return add_record_fn(env, level_params, rec_name, rec_type, intro_name, intro_type)();
 }
+
+optional<expr> record_normalizer_extension::operator()(expr const &, extension_context &) const {
+    return optional<expr>();
+}
+
+bool record_normalizer_extension::may_reduce_later(expr const &, extension_context &) const {
+    return false;
+}
+
+bool record_normalizer_extension::supports(name const &) const {
+    return false;
+}
 }}

src/kernel/record/record.h

@@ -29,6 +29,7 @@ class record_normalizer_extension : public normalizer_extension {
 public:
     virtual optional<expr> operator()(expr const & e, extension_context & ctx) const;
     virtual bool may_reduce_later(expr const & e, extension_context & ctx) const;
+    virtual bool supports(name const & feature) const;
 };
 
 /** \brief If \c n is the name of a record in the environment \c env, then return the

src/library/hott_kernel.cpp

@@ -5,10 +5,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "kernel/inductive/inductive.h"
+#include "kernel/record/record.h"
 #include "library/inductive_unifier_plugin.h"
 
 namespace lean {
 using inductive::inductive_normalizer_extension;
+using record::record_normalizer_extension;
 
 /** \brief Create a HoTT (Homotopy Type Theory) compatible environment */
 environment mk_hott_environment(unsigned trust_lvl) {
@@ -17,8 +19,9 @@ environment mk_hott_environment(unsigned trust_lvl) {
                                   true  /* Eta */,
                                   false /* Type.{0} is predicative */,
                                   list<name>(name("Id")) /* Exact equality types are proof irrelevant */,
-                                  /* builtin support for inductive datatypes */
-                                  std::unique_ptr<normalizer_extension>(new inductive_normalizer_extension()));
+                                  /* builtin support for inductive and record datatypes */
+                                  compose(std::unique_ptr<normalizer_extension>(new inductive_normalizer_extension()),
+                                          std::unique_ptr<normalizer_extension>(new record_normalizer_extension())));
     return set_unifier_plugin(env, mk_inductive_unifier_plugin());
 }
 }

src/library/standard_kernel.cpp

@@ -5,10 +5,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "kernel/inductive/inductive.h"
+#include "kernel/record/record.h"
 #include "library/inductive_unifier_plugin.h"
 
 namespace lean {
 using inductive::inductive_normalizer_extension;
+using record::record_normalizer_extension;
 
 /** \brief Create standard Lean environment */
 environment mk_environment(unsigned trust_lvl) {
@@ -17,8 +19,9 @@ environment mk_environment(unsigned trust_lvl) {
                                   true /* Eta */,
                                   true /* Type.{0} is impredicative */,
                                   list<name>() /* No type class has proof irrelevance */,
-                                  /* builtin support for inductive datatypes */
-                                  std::unique_ptr<normalizer_extension>(new inductive_normalizer_extension()));
+                                  /* builtin support for inductive and record datatypes */
+                                  compose(std::unique_ptr<normalizer_extension>(new inductive_normalizer_extension()),
+                                          std::unique_ptr<normalizer_extension>(new record_normalizer_extension())));
     return set_unifier_plugin(env, mk_inductive_unifier_plugin());
 }
 }

src/tests/kernel/environment.cpp

@@ -129,6 +129,7 @@ public:
         return some_expr(app_arg(app_fn(a_n)));
     }
     virtual bool may_reduce_later(expr const &, extension_context &) const { return false; }
+    virtual bool supports(name const &) const { return false; }
 };
 
 static void tst3() {