Add coercion declarations

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

src/frontends/lean/lean_coercion.h

@@ -0,0 +1,23 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "object.h"
+
+namespace lean {
+/**
+    \brief Object for tracking coercion declarations.
+    This object is mainly used for recording the declaration.
+*/
+class coercion_declaration : public neutral_object_cell {
+    expr          m_coercion;
+public:
+    coercion_declaration(expr const & c):m_coercion(c) {}
+    virtual ~coercion_declaration() {}
+    virtual char const * keyword() const { return "Coercion"; }
+    expr const & get_coercion() const { return m_coercion; }
+};
+}

src/frontends/lean/lean_frontend.cpp

@@ -5,13 +5,16 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <atomic>
+#include <unordered_set>
 #include "environment.h"
 #include "toplevel.h"
 #include "map.h"
 #include "state.h"
 #include "sstream.h"
 #include "exception.h"
+#include "expr_pair.h"
 #include "lean_operator_info.h"
+#include "lean_coercion.h"
 #include "lean_frontend.h"
 #include "lean_notation.h"
 #include "lean_pp.h"
@@ -25,6 +28,9 @@ struct frontend::imp {
     typedef std::unordered_map<name, operator_info, name_hash, name_eq> operator_table;
     typedef std::unordered_map<name, implicit_info, name_hash, name_eq> implicit_table;
     typedef std::unordered_map<expr, operator_info, expr_hash, std::equal_to<expr>> expr_to_operator;
+    typedef std::unordered_map<expr_pair, expr, expr_pair_hash, expr_pair_eq> coercion_map;
+    typedef std::unordered_set<expr, expr_hash, std::equal_to<expr>> coercion_set;
+
     std::atomic<unsigned> m_num_children;
     std::shared_ptr<imp>  m_parent;
     environment           m_env;
@@ -32,6 +38,8 @@ struct frontend::imp {
     operator_table        m_led; // led table for Pratt's parser
     expr_to_operator      m_expr_to_operator; // map denotations to operators (this is used for pretty printing)
     implicit_table        m_implicit_table; // track the number of implicit arguments for a symbol.
+    coercion_map          m_coercion_map; // mapping from (given_type, expected_type) -> coercion
+    coercion_set          m_coercion_set; // Set of coercions
     state                 m_state;
 
     bool has_children() const { return m_num_children > 0; }
@@ -273,6 +281,37 @@ struct frontend::imp {
         }
     }
 
+    void add_coercion(expr const & f) {
+        expr type      = m_env.infer_type(f);
+        expr norm_type = m_env.normalize(type);
+        if (!is_arrow(norm_type))
+            throw exception("invalid coercion declaration, a coercion must have an arrow type (i.e., a non-dependent functional type)");
+        expr from      = abst_domain(norm_type);
+        expr to        = abst_body(norm_type);
+        if (from == to)
+            throw exception("invalid coercion declaration, 'from' and 'to' types are the same");
+        if (get_coercion(from, to))
+            throw exception("invalid coercion declaration, frontend already has a coercion for the given types");
+        m_coercion_map[expr_pair(from, to)] = f;
+        m_coercion_set.insert(f);
+        m_env.add_neutral_object(new coercion_declaration(f));
+    }
+
+    expr get_coercion(expr const & given_type, expr const & expected_type) {
+        expr_pair p(given_type, expected_type);
+        auto it = m_coercion_map.find(p);
+        if (it != m_coercion_map.end())
+            return it->second;
+        else if (has_parent())
+            return m_parent->get_coercion(given_type, expected_type);
+        else
+            return expr();
+    }
+
+    bool is_coercion(expr const & f) {
+        return m_coercion_set.find(f) != m_coercion_set.end();
+    }
+
     void set_interrupt(bool flag) {
         m_env.set_interrupt(flag);
         m_state.set_interrupt(flag);
@@ -352,6 +391,10 @@ bool frontend::has_implicit_arguments(name const & n) const { return m_imp->has_
 std::vector<bool> const & frontend::get_implicit_arguments(name const & n) const { return m_imp->get_implicit_arguments(n); }
 name const & frontend::get_explicit_version(name const & n) const { return m_imp->get_explicit_version(n); }
 
+void frontend::add_coercion(expr const & f) { m_imp->add_coercion(f); }
+expr frontend::get_coercion(expr const & given_type, expr const & expected_type) { return m_imp->get_coercion(given_type, expected_type); }
+bool frontend::is_coercion(expr const & f) { return m_imp->is_coercion(f); }
+
 state const & frontend::get_state() const { return m_imp->m_state; }
 state & frontend::get_state_core() { return m_imp->m_state; }
 void frontend::set_options(options const & opts) { return m_imp->m_state.set_options(opts); }

src/frontends/lean/lean_frontend.h

@@ -142,6 +142,35 @@ public:
     name const & get_explicit_version(name const & n) const;
     /*@}*/
 
+    /**
+       @name Coercions
+
+       We support a very basic form of coercion. It is an expression
+       with type T1 -> T2. This expression can be used to convert
+       an expression of type T1 into an expression of type T2 whenever
+       T2 is expected, but T1 was provided.
+    */
+    /**
+       \brief Add a new coercion to the frontend.
+       It throws an exception if f does not have type T1 -> T2, or if there is already a
+       coercion from T1 to T2.
+    */
+    void add_coercion(expr const & f);
+    /**
+        \brief Return a coercion from given_type to expected_type if it exists.
+        Return the null expression if there is no coercion from \c given_type to
+        \c expected_type.
+
+        \pre The expressions \c given_type and \c expected_type are normalized
+    */
+    expr get_coercion(expr const & given_type, expr const & expected_type);
+    /**
+       \brief Return true iff the given expression is a coercion. That is, it was added using
+       \c add_coercion.
+    */
+    bool is_coercion(expr const & f);
+    /*@}*/
+
     /**
        @name State management.
     */

src/frontends/lean/lean_parser.cpp

@@ -75,10 +75,11 @@ static name g_options_kwd("Options");
 static name g_env_kwd("Environment");
 static name g_import_kwd("Import");
 static name g_help_kwd("Help");
+static name g_coercion_kwd("Coercion");
 /** \brief Table/List with all builtin command keywords */
 static list<name> g_command_keywords = {g_definition_kwd, g_variable_kwd, g_theorem_kwd, g_axiom_kwd, g_universe_kwd, g_eval_kwd,
                                         g_show_kwd, g_check_kwd, g_infix_kwd, g_infixl_kwd, g_infixr_kwd, g_notation_kwd, g_echo_kwd,
-                                        g_set_kwd, g_env_kwd, g_options_kwd, g_import_kwd, g_help_kwd};
+                                        g_set_kwd, g_env_kwd, g_options_kwd, g_import_kwd, g_help_kwd, g_coercion_kwd};
 // ==========================================
 
 // ==========================================
@@ -1369,6 +1370,15 @@ class parser::imp {
         }
     }
 
+    /** \brief Parse 'Coercion' expr */
+    void parse_coercion() {
+        next();
+        expr coercion = parse_expr();
+        m_frontend.add_coercion(coercion);
+        if (m_verbose)
+            regular(m_frontend) << "  Coercion " << coercion << endl;
+    }
+
     /** \brief Parse a Lean command. */
     void parse_command() {
         m_elaborator.clear();
@@ -1390,6 +1400,7 @@ class parser::imp {
         else if (cmd_id == g_set_kwd)      parse_set();
         else if (cmd_id == g_import_kwd)   parse_import();
         else if (cmd_id == g_help_kwd)     parse_help();
+        else if (cmd_id == g_coercion_kwd) parse_coercion();
         else { next(); throw parser_error(sstream() << "invalid command '" << cmd_id << "'", m_last_cmd_pos); }
     }
     /*@}*/

src/frontends/lean/lean_pp.cpp

@@ -22,6 +22,7 @@ Author: Leonardo de Moura
 #include "lean_notation.h"
 #include "lean_pp.h"
 #include "lean_frontend.h"
+#include "lean_coercion.h"
 
 #ifndef LEAN_DEFAULT_PP_MAX_DEPTH
 #define LEAN_DEFAULT_PP_MAX_DEPTH std::numeric_limits<unsigned>::max()
@@ -1109,12 +1110,19 @@ class pp_formatter_cell : public formatter_cell {
     }
 
     format pp_notation_decl(object const & obj, options const & opts) {
-        notation_declaration const & n = *(static_cast<notation_declaration const *>(obj.cell()));
+        notation_declaration const & n = *static_cast<notation_declaration const *>(obj.cell());
         expr const & d = n.get_expr();
         format d_fmt   = is_constant(d) ? format(const_name(d)) : pp(d, opts);
         return format{::lean::pp(n.get_op()), space(), colon(), space(), d_fmt};
     }
 
+    format pp_coercion_decl(object const & obj, options const & opts) {
+        unsigned indent = get_pp_indent(opts);
+        coercion_declaration const & n = *static_cast<coercion_declaration const *>(obj.cell());
+        expr const & c = n.get_coercion();
+        return group(format{highlight_command(format(n.keyword())), nest(indent, format({line(), pp(c, opts)}))});
+    }
+
 public:
     pp_formatter_cell(frontend const & fe):
         m_frontend(fe) {
@@ -1157,10 +1165,13 @@ public:
         case object_kind::Definition:       return pp_definition(obj, opts);
         case object_kind::Neutral:
             if (dynamic_cast<notation_declaration const *>(obj.cell())) {
-                // If the object is not notation, then the object was
-                // created in different frontend, and we ignore it.
                 return pp_notation_decl(obj, opts);
+            } else if (dynamic_cast<coercion_declaration const *>(obj.cell())) {
+                return pp_coercion_decl(obj, opts);
             } else {
+                // If the object is not notation or coercion
+                // declaration, then the object was created in
+                // different frontend, and we ignore it.
                 return format("Unknown neutral object");
             }
         }

src/kernel/environment.cpp

@@ -290,6 +290,14 @@ struct environment::imp {
         }
     }
 
+    expr infer_type(expr const & e, context const & ctx) {
+        return m_type_checker.infer_type(e, ctx);
+    }
+
+    expr normalize(expr const & e, context const & ctx) {
+        return m_type_checker.get_normalizer()(e, ctx);
+    }
+
     /** \brief Display universal variable constraints and objects stored in this environment and its parents. */
     void display(std::ostream & out, environment const & env) const {
         if (has_parent())
@@ -410,6 +418,14 @@ object const & environment::get_object(unsigned i, bool local) const {
     return m_imp->get_object(i, local);
 }
 
+expr environment::infer_type(expr const & e, context const & ctx) {
+    return m_imp->infer_type(e, ctx);
+}
+
+expr environment::normalize(expr const & e, context const & ctx) {
+    return m_imp->normalize(e, ctx);
+}
+
 void environment::display(std::ostream & out) const {
     m_imp->display(out, *this);
 }

src/kernel/environment.h

@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #pragma once
 #include <iostream>
 #include <memory>
+#include "context.h"
 #include "object.h"
 #include "level.h"
 
@@ -120,6 +121,16 @@ public:
     /** \brief Return true iff the environment has an object with the given name */
     bool has_object(name const & n) const { return find_object(n); }
 
+    /**
+       \brief Return the type of \c e in the given context and this environment.
+    */
+    expr infer_type(expr const & e, context const & ctx = context());
+
+    /**
+       \brief Normalize \c e in the given context and this environment.
+    */
+    expr normalize(expr const & e, context const & ctx = context());
+
     /** \brief Iterator for Lean environment objects. */
     class object_iterator {
         environment const & m_env;

src/kernel/type_check.cpp

@@ -163,6 +163,10 @@ public:
         m_cache.clear();
         m_normalizer.clear();
     }
+
+    normalizer & get_normalizer() {
+        return m_normalizer;
+    }
 };
 
 type_checker::type_checker(environment const & env):m_ptr(new imp(env)) {}
@@ -171,9 +175,8 @@ expr type_checker::infer_type(expr const & e, context const & ctx) { return m_pt
 level type_checker::infer_universe(expr const & e, context const & ctx) { return m_ptr->infer_universe(e, ctx); }
 void type_checker::clear() { m_ptr->clear(); }
 void type_checker::set_interrupt(bool flag) { m_ptr->set_interrupt(flag); }
-bool type_checker::is_convertible(expr const & t1, expr const & t2, context const & ctx) {
-    return m_ptr->is_convertible(t1, t2, ctx);
-}
+bool type_checker::is_convertible(expr const & t1, expr const & t2, context const & ctx) { return m_ptr->is_convertible(t1, t2, ctx); }
+normalizer & type_checker::get_normalizer() { return m_ptr->get_normalizer(); }
 
 expr  infer_type(expr const & e, environment const & env, context const & ctx) {
     return type_checker(env).infer_type(e, ctx);

src/kernel/type_check.h

@@ -11,6 +11,7 @@ Author: Leonardo de Moura
 
 namespace lean {
 class environment;
+class normalizer;
 class type_checker {
     class imp;
     std::unique_ptr<imp> m_ptr;
@@ -28,6 +29,8 @@ public:
     void set_interrupt(bool flag);
     void interrupt() { set_interrupt(true); }
     void reset_interrupt() { set_interrupt(false); }
+
+    normalizer & get_normalizer();
 };
 
 expr infer_type(expr const & e, environment const & env, context const & ctx = context());

src/library/elaborator.cpp

@@ -15,6 +15,7 @@ Author: Leonardo de Moura
 #include "for_each.h"
 #include "update_expr.h"
 #include "replace.h"
+#include "expr_pair.h"
 #include "flet.h"
 #include "elaborator_exception.h"
 
@@ -238,8 +239,6 @@ class elaborator::imp {
         }
     }
 
-    typedef std::pair<expr, expr> expr_pair;
-
     /**
        \brief Traverse the expression \c e, and compute
 

src/library/expr_pair.h

@@ -0,0 +1,25 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "expr.h"
+#include "hash.h"
+
+namespace lean {
+typedef std::pair<expr, expr> expr_pair;
+/** \brief Functional object for hashing expression pairs. */
+struct expr_pair_hash {
+    unsigned operator()(expr_pair const & p) const { return hash(p.first.hash(), p.second.hash()); }
+};
+/** \brief Functional object for comparing expression pairs. */
+struct expr_pair_eq {
+    unsigned operator()(expr_pair const & p1, expr_pair const & p2) const { return p1.first == p2.first && p1.second == p2.second; }
+};
+/** \brief Functional object for comparing expression pairs using pointer equality. */
+struct expr_pair_eqp {
+    unsigned operator()(expr_pair const & p1, expr_pair const & p2) const { return is_eqp(p1.first, p2.first) && is_eqp(p1.second, p2.second); }
+};
+}

tests/lean/coercion1.lean

@@ -0,0 +1,16 @@
+Set pp::colors false
+Variable T : Type
+Variable R : Type
+Variable f : T -> R
+Coercion f
+Show Environment 2
+Variable g : T -> R
+Coercion g
+Variable h : Pi (x : Type), x
+Coercion h
+Definition T2 : Type := T
+Definition R2 : Type := R
+Variable f2 : T2 -> R2
+Coercion f2
+Variable id : T -> T
+Coercion id

tests/lean/coercion1.lean.expected.out

@@ -0,0 +1,17 @@
+  Set option: pp::colors
+  Assumed: T
+  Assumed: R
+  Assumed: f
+  Coercion f
+Variable f : T → R
+Coercion f
+  Assumed: g
+Error (line: 9, pos: 0) invalid coercion declaration, frontend already has a coercion for the given types
+  Assumed: h
+Error (line: 11, pos: 0) invalid coercion declaration, a coercion must have an arrow type (i.e., a non-dependent functional type)
+  Defined: T2
+  Defined: R2
+  Assumed: f2
+Error (line: 15, pos: 0) invalid coercion declaration, frontend already has a coercion for the given types
+  Assumed: id
+Error (line: 17, pos: 0) invalid coercion declaration, 'from' and 'to' types are the same