From 1477036b36aa0bd0cb3051e9094fd6c751eebf08 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 28 Sep 2018 08:32:10 -0700 Subject: [PATCH] fix(library/compiler/csimp): we may have partially applied `cases_on` applications in the computationally irrelevant part --- src/library/compiler/csimp.cpp | 4 +++- src/library/compiler/util.cpp | 9 +++++++++ src/library/compiler/util.h | 10 ++++++++++ 3 files changed, 22 insertions(+), 1 deletion(-) diff --git a/src/library/compiler/csimp.cpp b/src/library/compiler/csimp.cpp index aaeb20c8e5..bb2394189f 100644 --- a/src/library/compiler/csimp.cpp +++ b/src/library/compiler/csimp.cpp @@ -233,7 +233,9 @@ class csimp_fn { if (is_proj(s) && proj_expr(s) == x) { found = true; return false; - } else if (is_cases_on_app(env(), s) && get_cases_on_app_major(env(), s) == x) { + } else if (is_cases_on_app(env(), s) && + get_app_num_args(s) == get_cases_on_arity(env(), const_name(get_app_fn(s))) && + get_cases_on_app_major(env(), s) == x) { found = true; return false; } diff --git a/src/library/compiler/util.cpp b/src/library/compiler/util.cpp index c20741345c..1715366317 100644 --- a/src/library/compiler/util.cpp +++ b/src/library/compiler/util.cpp @@ -125,6 +125,15 @@ bool is_cases_on_recursor(environment const & env, name const & n) { return ::lean::is_aux_recursor(env, n) && n.get_string() == "cases_on"; } +unsigned get_cases_on_arity(environment const & env, name const & c) { + lean_assert(is_cases_on_recursor(env, c)); + inductive_val I_val = get_cases_on_inductive_val(env, c); + unsigned nparams = I_val.get_nparams(); + unsigned nindices = I_val.get_nindices(); + unsigned nminors = I_val.get_ncnstrs(); + return nparams + 1 /* motive */ + nindices + 1 /* major */ + nminors; +} + expr get_cases_on_app_major(environment const & env, expr const & c) { lean_assert(is_cases_on_app(env, c)); buffer args; diff --git a/src/library/compiler/util.h b/src/library/compiler/util.h index 649687e825..7658af3422 100644 --- a/src/library/compiler/util.h +++ b/src/library/compiler/util.h @@ -30,6 +30,16 @@ expr unfold_macro_defs(environment const & env, expr const & e); inline bool is_lc_mdata(expr const &) { return false; } bool is_cases_on_recursor(environment const & env, name const & n); +/* We defined the "arity" of a cases_on application as the sum: + ``` + number of inductive parameters + + 1 + // motive + number of inductive indices + + 1 + // major premise + number of constructors // cases_on has a minor premise for each constructor + ``` + \pre is_cases_on_recursor(env, c) */ +unsigned get_cases_on_arity(environment const & env, name const & c); /* Return the `inductive_val` for the cases_on constant `c`. */ inline inductive_val get_cases_on_inductive_val(environment const & env, name const & c) { lean_assert(is_cases_on_recursor(env, c));