automatic_relations/convolution/
mod.rs

1use terms::{
2    Term,
3    Pattern,
4    variable::Family
5};
6use ta::{
7    Symbol,
8    State,
9    NoLabel,
10    Rank,
11    bottom_up::{
12        Automaton,
13        width_search::{LanguageState, Killed}
14    }
15};
16use crate::{
17    Convoluted
18};
19
20pub mod aligned;
21
22/// Convolution operations.
23pub trait Convolution<F: Symbol> {
24    /// Perform a term convolution.
25    fn convolute<T: AsRef<[Option<Term<F>>]>>(terms: T) -> Term<Rank<Convoluted<F>>>;
26
27    // /// Perform a pattern convolution.
28    // fn convolute_patterns<X: Clone, P: AsRef<[Option<Pattern<F, X>>]>>(patterns: P) -> ConvolutedPattern<F, X>;
29
30    /// Perform a term deconvolution.
31    fn deconvolute(term: Term<Rank<Convoluted<F>>>) -> Vec<Option<Term<F>>>;
32
33    /// Generic alternating-automaton out of a convoluted bottom-up automaton.
34    fn generic_automaton<Q: State>(aut: &Automaton<Rank<Convoluted<F>>, Q, NoLabel>) -> ta::alternating::Automaton<Convoluted<F>, Q, Convoluted<u32>>;
35
36    /// Compute the equality predicate over a domain between `n` variables.
37    fn equality<Q: State>(aut: &Automaton<F, Q, NoLabel>, n: usize) -> Automaton<Rank<Convoluted<F>>, Q, NoLabel>;
38
39    // /// Compute the natural comparison operator `<` for the given nat constructors.
40    // fn nat_less<Q: State>(s: F, zero: F) -> Automaton<Rank<Convoluted<F>>, Q, NoLabel>;
41    //
42    // /// Compute the natural comparison operator `<=` for the given nat constructors.
43    // fn nat_leq<Q: State>(s: F, zero: F) -> Automaton<Rank<Convoluted<F>>, Q, NoLabel>;
44
45    fn state_convolution<E, Q: LanguageState<F, E>>(initial_state: Convoluted<Q>, env: &E) -> Automaton<Rank<Convoluted<F>>, Convoluted<Q>, NoLabel>;
46
47    fn search<'a, 'e, Q: State, X: 'a + Family + Ord + Clone>(automata: &'a [&'e Automaton<Rank<Convoluted<F>>, Q, NoLabel>], patterns: Vec<Convoluted<Pattern<F, X>>>, kill_signal: Option<crossbeam_channel::Receiver<()>>) -> Box<dyn Iterator<Item = Result<Vec<Term<Rank<Convoluted<F>>>>, Killed>> + 'a>;
48}
automatic_relations/convolution/mod.rs

automatic_relations/convolution/
mod.rs
