max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor(kernel): remove dead code from type_checker

Browse source
This commit is contained in:
Leonardo de Moura 2016-03-19 15:25:38 -07:00
parent 6406d7cf8b
commit 856889a08d
3 changed files with 16 additions and 110 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

47
src/kernel/type_checker.cpp
View file

@ -23,53 +23,6 @@ Author: Leonardo de Moura
#include "kernel/replace_fn.h"
namespace lean {
expr replace_range(expr const & type, expr const & new_range) {
if (is_pi(type))
return update_binding(type, binding_domain(type), replace_range(binding_body(type), new_range));
else
return new_range;
}
/** \brief Return the "arity" of the given type. The arity is the number of nested pi-expressions. */
unsigned get_arity(expr type) {
unsigned r = 0;
while (is_pi(type)) {
type = binding_body(type);
r++;
}
return r;
}
expr mk_aux_type_metavar_for(expr const & t) {
expr new_type = replace_range(t, mk_sort(mk_meta_univ(mk_fresh_name())));
name n = mk_fresh_name();
return mk_metavar(n, new_type);
}
expr mk_aux_metavar_for(expr const & t) {
unsigned num = get_arity(t);
expr r = mk_app_vars(mk_aux_type_metavar_for(t), num);
expr new_type = replace_range(t, r);
name n = mk_fresh_name();
return mk_metavar(n, new_type);
}
expr mk_pi_for(expr const & meta) {
lean_assert(is_meta(meta));
buffer<expr> margs;
expr const & m = get_app_args(meta, margs);
expr const & mtype = mlocal_type(m);
expr maux1 = mk_aux_type_metavar_for(mtype);
expr dontcare;
expr tmp_pi = mk_pi(mk_fresh_name(), mk_app_vars(maux1, margs.size()), dontcare); // trick for "extending" the context
expr mtype2 = replace_range(mtype, tmp_pi); // trick for "extending" the context
expr maux2 = mk_aux_type_metavar_for(mtype2);
expr A = mk_app(maux1, margs);
margs.push_back(Var(0));
expr B = mk_app(maux2, margs);
return mk_pi(mk_fresh_name(), A, B);
}
optional<expr> type_checker::expand_macro(expr const & m) {
lean_assert(is_macro(m));
return macro_def(m).expand(m, *this);

76
src/kernel/type_checker.h
View file

@ -17,57 +17,18 @@ Author: Leonardo de Moura
#include "kernel/abstract_type_context.h"
namespace lean {
/** \brief Return the "arity" of the given type. The arity is the number of nested pi-expressions. */
unsigned get_arity(expr type);
/** \brief Given \c type of the form <tt>(Pi ctx, r)</tt>, return <tt>(Pi ctx, new_range)</tt> */
expr replace_range(expr const & type, expr const & new_range);
/**
\brief Given a type \c t of the form
<tt>Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), B[x_1, ..., x_n]</tt>
return a new metavariable \c m1 with type
<tt>Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), Type.{u}</tt>
where \c u is a new universe metavariable.
*/
expr mk_aux_type_metavar_for(expr const & t);
/**
\brief Given a type \c t of the form
<tt>Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), B[x_1, ..., x_n]</tt>
return a new metavariable \c m1 with type
<tt>Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), (?m2 x_1 ... x_n)</tt>
where \c ?m2 is a new metavariable with type
<tt>Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), Type.{u}</tt>
where \c u is a new universe metavariable.
*/
expr mk_aux_metavar_for(expr const & t);
/**
\brief Given a meta (?m t_1 ... t_n) where ?m has type
<tt>Pi (x_1 : A_1) ... (x_n : A_n[x_1, ..., x_{n-1}]), B[x_1, ..., x_n]</tt>
return a Pi term
<tt>Pi (x : ?m1 t_1 ... t_n), (?m2 t_1 ... t_n x) </tt>
where ?m1 and ?m2 are fresh metavariables
*/
expr mk_pi_for(expr const & meta);
/**
\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.
*/
/** \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. */
class type_checker : public abstract_type_context {
/* In the type checker cache, we must take into account binder information.
Examples:
The type of (lambda x : A, t) is (Pi x : A, typeof(t))
The type of (lambda {x : A}, t) is (Pi {x : A}, typeof(t)) */
typedef expr_bi_struct_map<expr> cache;
environment m_env;
std::unique_ptr<converter> m_conv;
// In the type checker cache, we must take into account binder information.
// Examples:
// The type of (lambda x : A, t) is (Pi x : A, typeof(t))
// The type of (lambda {x : A}, t) is (Pi {x : A}, typeof(t))
cache m_infer_type_cache[2];
bool m_memoize;
// temp flag
level_param_names const * m_params;
friend class converter; // allow converter to access the following methods
@ -84,12 +45,10 @@ class type_checker : public abstract_type_context {
expr infer_type_core(expr const & e, bool infer_only);
expr infer_type(expr const & e);
public:
/**
\brief Create a type checker for the given environment. The auxiliary names created by this
/** \brief Create a type checker for the given environment. The auxiliary names created by this
type checker are based on the given name generator.
memoize: if true, then inferred types are memoized/cached
*/
memoize: if true, then inferred types are memoized/cached */
type_checker(environment const & env, std::unique_ptr<converter> && conv, bool memoize = true);
type_checker(environment const & env, bool memoize = true);
~type_checker();
@ -97,15 +56,14 @@ public:
virtual environment const & env() const { return m_env; }
/** \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. */
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. */
virtual expr infer(expr const & t) { return infer_type(t); }
/**
\brief Type check the given expression, and return the type of \c t.
Throw an exception if a type error is found. */
/** \brief Type check the given expression, and return the type of \c t.
Throw an exception if a type error is found. */
virtual expr check(expr const & t, level_param_names const & ps = level_param_names());
/** \brief Like \c check, but ignores undefined universes */
expr check_ignore_undefined_universes(expr const & e);
@ -161,10 +119,8 @@ typedef std::shared_ptr<type_checker> type_checker_ref;
void check_no_metavar(environment const & env, name const & n, expr const & e, bool is_type);
/**
\brief Type check the given declaration, and return a certified declaration if it is type correct.
Throw an exception if the declaration is type incorrect.
*/
/** \brief Type check the given declaration, and return a certified declaration if it is type correct.
Throw an exception if the declaration is type incorrect. */
certified_declaration check(environment const & env, declaration const & d);
certified_declaration check(environment const & env, declaration const & d, name_predicate const & opaque_hints);

3
src/library/old_type_checker.cpp
View file

@ -24,7 +24,6 @@ Author: Leonardo de Moura
#include "library/old_type_checker.h"
namespace lean {
#if 0
expr replace_range(expr const & type, expr const & new_range) {
if (is_pi(type))
return update_binding(type, binding_domain(type), replace_range(binding_body(type), new_range));
@ -72,8 +71,6 @@ expr mk_pi_for(expr const & meta) {
return mk_pi(mk_fresh_name(), A, B);
}
#endif
optional<expr> old_type_checker::expand_macro(expr const & m) {
lean_assert(is_macro(m));
return macro_def(m).expand(m, get_type_context());