refactor(kernel/type_checker): new API for type checker

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

src/kernel/type_checker.cpp

@@ -4,6 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include "kernel/type_checker.h"
+
+
+
 #if 0
 #include "util/freset.h"
 #include "util/flet.h"

src/kernel/type_checker.h

@@ -8,97 +8,81 @@ Author: Leonardo de Moura
 #include <memory>
 #include <utility>
 #include "util/name_generator.h"
-#include "kernel/expr.h"
+#include "kernel/environment.h"
 #include "kernel/constraint.h"
 
 namespace lean {
-class environment;
-class normalizer;
+class constraint_handler {
+public:
+    virtual ~constraint_handler();
+    void add_constr(constraint const & c);
+};
 
 /**
-   \brief Given pi == (Pi x : A, B x), return (B a)
+   \brief Lean Type Checker. It can also be used to infer types, check whether a
+   type \c A is convertible to a type \c B, etc.
 
-   \pre is_pi(pi)
-   \pre type of a is A
-*/
-expr pi_body_at(expr const & pi, expr const & a);
-
-/**
-   \brief Lean Type Checker. It can also be used to infer types, universes and check whether a
-   type \c A is convertible to a type \c B.
-
-   Remark: several methods take a \c name_generator as argument. The name generator is used
-   for creating fresh metavariables and local variables.
-
-   Remark: several methods return constraints. Three possible kinds of constraints a generated:
-   unification constraints, convertability constraints and universe level constraints.
-   See constraints.h for more details. The first two kinds of constraints are only generated
-   if the input expression contains meta-variables or meta-level-parameters.
+   The type checker produces constraints, and they are sent to the constraint handler.
 */
 class type_checker {
     class imp;
     std::unique_ptr<imp> m_ptr;
 public:
-    type_checker(ro_environment const & env);
+    /**
+       \brief Create a type checker for the given environment. The auxiliary names created by this
+       type checker are based on the given name generator.
+
+       The following set of options is supported:
+         - memoize:      inferred types are memoized/cached
+         - unique_expr:  hash consing is performed on input expressions, it improves the effectiveness of memoize
+         - extra_opaque: additional definitions that should be treated as opaque
+    */
+    type_checker(environment const & env, name_generator const & g, constraint_handler & h, options const & o = options());
+    /**
+       \brief Similar to the previous constructor, but if a method tries to create a constraint, then an
+       exception is thrown.
+    */
+    type_checker(environment const & env, name_generator const & g, options const & o = options());
     ~type_checker();
 
     /**
-       \brief Return the type of \c e.
+       \brief Return the type of \c t.
 
        It does not check whether the input expression is type correct or not.
        The contract is: IF the input expression is type correct, then the inferred
        type is correct.
        Throw an exception if a type error is found.
 
-       The result is meaningful only if the resultant set of constraints can be solved.
+       The result is meaningful only if the constraints sent to the
+       constraint handler can be solved.
    */
-    std::pair<expr, constraints> infer_type(expr const & e, name_generator & g);
+    expr infer(expr const & t);
 
     /**
-       \brief Type check the given expression, and return the type of \c e.
+       \brief Type check the given expression, and return the type of \c t.
        Throw an exception if a type error is found.
 
-       The result is meaningful only if the resultant set of constraints can be solved.
+       The result is meaningful only if the constraints sent to the
+       constraint handler can be solved.
     */
-    std::pair<expr, constraints> check(expr const & e, name_generator & g);
-
-    /**
-        \brief Return a set of constraints that need to be solved for \c t1 to be convertible to \c t2.
-
-        Return none if \c t1 is not convertible to \c t2.
-    */
-    optional<constraints> is_convertible(expr const & t1, expr const & t2, name_generator & g);
-
-    /**
-        \brief Return a set of constraints that need to be solved for \c t1 to be definitionally equal to \c t2.
-
-        Return none if \c t1 is not definitionally equal to \c t2.
-    */
-    optional<constraints> is_definitionally_equal(expr const & t1, expr const & t2, name_generator & g);
-
-    /**
-        \brief Return a set of constraints that need to be solved for \c e to be a proposition (i.e., it has type Bool)
-
-        Return none if \c e is not a proposition.
-    */
-    optional<constraints> is_proposition(expr const & e, name_generator & g);
-
-    /**
-        \brief Return a Pi if \c e is convertible to a Pi type.
-       Throw an exception if a type error is found.
-    */
-    std::pair<expr, constraints> ensure_pi(expr const & e, name_generator & g);
-
-    /**
-        \brief Return a Sigma if \c e is convertible to a Sigma type.
-       Throw an exception if a type error is found.
-    */
-    std::pair<expr, constraints> ensure_sigma(expr const & e, name_generator & g);
-
-    /** \brief Reset internal caches */
-    void clear();
-
-    /** \brief Return reference to the normalizer used by this type checker. */
-    normalizer & get_normalizer();
+    expr check(expr const & t);
+    /** \brief Return true iff t is convertible to s. */
+    bool is_conv(expr const & t, expr const & s);
+    /** \brief Return true iff t is definitionally equal to s. */
+    bool is_defeq(expr const & t, expr const & s);
+    /** \brief Return true iff t is a proposition. */
+    bool is_prop(expr const & t);
+    /** \brief Return the weak head normal form of \c t. */
+    expr whnf(expr const & t);
+    /** \brief Return a Pi if \c t is convertible to a Pi type. Throw an exception otherwise. */
+    expr ensure_pi(expr const & t);
+    /** \brief Return a Sort if \c t is convertible to Sort. Throw an exception otherwise. */
+    expr ensure_sort(expr const & t);
 };
+
+/**
+   \brief Type check the given definition, and return a certified definition if it is type correct.
+   Throw an exception if the definition is type incorrect.
+*/
+certified_definition check(environment const & env, name_generator const & g, options const & o, definition const & d);
 }