feat(kernel/expr): add has_expr_metavar_strict
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
d9ee994281
commit
5c5dea7c8e
2 changed files with 16 additions and 0 deletions
|
@ -19,6 +19,7 @@ Author: Leonardo de Moura
|
|||
#include "kernel/expr.h"
|
||||
#include "kernel/expr_eq_fn.h"
|
||||
#include "kernel/free_vars.h"
|
||||
#include "kernel/for_each_fn.h"
|
||||
|
||||
#ifndef LEAN_INITIAL_EXPR_CACHE_CAPACITY
|
||||
#define LEAN_INITIAL_EXPR_CACHE_CAPACITY 1024*16
|
||||
|
@ -594,6 +595,19 @@ bool is_arrow(expr const & t) {
|
|||
}
|
||||
}
|
||||
|
||||
bool has_expr_metavar_strict(expr const & e) {
|
||||
if (!has_expr_metavar(e))
|
||||
return false;
|
||||
bool found = false;
|
||||
for_each(e, [&](expr const & e, unsigned) {
|
||||
if (found || !has_expr_metavar(e)) return false;
|
||||
if (is_metavar(e)) { found = true; return false; }
|
||||
if (is_local(e)) return false; // do not visit type
|
||||
return true;
|
||||
});
|
||||
return found;
|
||||
}
|
||||
|
||||
static bool has_free_var_in_domain(expr const & b, unsigned vidx) {
|
||||
if (is_pi(b)) {
|
||||
return has_free_var(binding_domain(b), vidx) || has_free_var_in_domain(binding_body(b), vidx+1);
|
||||
|
|
|
@ -585,6 +585,8 @@ inline bool is_constant(expr const & e, name const & n) { return is_constant(e)
|
|||
inline bool has_metavar(expr const & e) { return e.has_metavar(); }
|
||||
inline bool has_expr_metavar(expr const & e) { return e.has_expr_metavar(); }
|
||||
inline bool has_univ_metavar(expr const & e) { return e.has_univ_metavar(); }
|
||||
/** \brief Similar to \c has_expr_metavar, but ignores metavariables occurring in local constant types. */
|
||||
bool has_expr_metavar_strict(expr const & e);
|
||||
inline bool has_local(expr const & e) { return e.has_local(); }
|
||||
inline bool has_param_univ(expr const & e) { return e.has_param_univ(); }
|
||||
unsigned get_depth(expr const & e);
|
||||
|
|
Loading…
Reference in a new issue