veri_engine_lib/
termname.rs

1use cranelift_isle as isle;
2use isle::sema::{Pattern, TermEnv, TypeEnv};
3
4/// Check whether the pattern (the LHS term) contains a given term name,
5/// including in any subterms.
6pub fn pattern_contains_termname(
7    pat: &Pattern,
8    name: &str,
9    termenv: &TermEnv,
10    typeenv: &TypeEnv,
11) -> bool {
12    match pat {
13        Pattern::BindPattern(..)
14        | Pattern::Var(..)
15        | Pattern::ConstInt(..)
16        | Pattern::ConstBool(..)
17        | Pattern::ConstPrim(..)
18        | Pattern::Wildcard(..) => false,
19        Pattern::Term(_, termid, arg_patterns) => {
20            let term = &termenv.terms[termid.index()];
21            let term_name = &typeenv.syms[term.name.index()];
22            (term_name == name)
23                || arg_patterns
24                    .iter()
25                    .any(|p| pattern_contains_termname(p, name, termenv, typeenv))
26        }
27        Pattern::And(_, children) => children
28            .iter()
29            .any(|p| pattern_contains_termname(p, name, termenv, typeenv)),
30    }
31}
veri_engine_lib/termname.rs

veri_engine_lib/
termname.rs
