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

chore(*): fix some compilation warnings

Browse source
This commit is contained in:
Leonardo de Moura 2019-08-15 09:26:13 -07:00
parent f1fa528dbe
commit 61beb56a83
3 changed files with 6 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/frontends/lean/elaborator.cpp
View file

@ -2538,7 +2538,6 @@ expr elaborator::visit_equation(expr const & e, unsigned num_fns) {
}
expr elaborator::visit_equations(expr const & e) {
expr const & ref = e;
buffer<expr> eqs;
buffer<expr> new_eqs;
optional<expr> new_tacs;
@ -2849,7 +2848,7 @@ class visit_structure_instance_fn {
fval = mk_app(default_val, args);
fval = head_beta_reduce(fval);
}
reduce_and_check_deps(fval, full_S_fname);
reduce_and_check_deps(fval);
return fval;
}
});
@ -2975,7 +2974,7 @@ class visit_structure_instance_fn {
* Also reduce projections containing mvars, which may remove dependencies.
* Example: `functor.map (functor.mk ?p1 ?m1 ?m2...) => ?m1`
*/
void reduce_and_check_deps(expr & e, name const & full_S_fname) {
void reduce_and_check_deps(expr & e) {
if (m_use_subobjects)
e = reduce_projections_visitor(m_ctx)(e);
name_set deps;
@ -3053,7 +3052,7 @@ class visit_structure_instance_fn {
expr val;
try {
reduce_and_check_deps(reduced_expected_type, full_S_fname);
reduce_and_check_deps(reduced_expected_type);
/* note: we pass the reduced, mvar-free expected type. Otherwise auto params may fail with
* "result contains meta-variables". */
val = (*m_field2elab.find(S_fname))(reduced_expected_type);

7
src/frontends/lean/pp.cpp
View file

@ -463,13 +463,6 @@ auto pretty_fn::pp_child_core(expr const & e, unsigned bp, bool ignore_hide) ->
return add_paren_if_needed(pp(e, ignore_hide), bp);
}
static expr consume_ref_annotations(expr const & e) {
if (is_explicit(e))
return consume_ref_annotations(get_explicit_arg(e));
else
return e;
}
static bool is_coercion(expr const & e) {
return is_app_of(e, get_coe_name()) && get_app_num_args(e) >= 4;
}

7
src/library/compiler/specialize.cpp
View file

@ -460,7 +460,6 @@ class specialize_fn {
/* Auxiliary class for collecting specialization dependencies. */
class dep_collector {
type_checker::state & m_st;
local_ctx m_lctx;
name_set m_visited_not_in_binder;
name_set m_visited_in_binder;
@ -572,8 +571,8 @@ class specialize_fn {
}
public:
dep_collector(type_checker::state & st, local_ctx const & lctx, spec_ctx & ctx):
m_st(st), m_lctx(lctx), m_ctx(ctx) {}
dep_collector(local_ctx const & lctx, spec_ctx & ctx):
m_lctx(lctx), m_ctx(ctx) {}
void operator()(expr const & e) { return collect(e, false); }
};
@ -587,7 +586,7 @@ class specialize_fn {
buffer<spec_arg_kind> kinds;
get_arg_kinds(const_name(fn), kinds);
bool has_attr = has_specialize_attribute(env(), const_name(fn));
dep_collector collect(m_st, m_lctx, ctx);
dep_collector collect(m_lctx, ctx);
unsigned sz = std::min(kinds.size(), args.size());
unsigned i = sz;
bool found_inst = false;