automatic_relations/convolution/aligned/
mod.rs

1use terms::{
2    Term,
3    Pattern,
4    variable::Family
5};
6use ta::{
7    Symbol,
8    State,
9    NoLabel,
10    Ranked,
11    Rank,
12    bottom_up::{
13        Automaton,
14        Configuration,
15        width_search::{LanguageState, Killed}
16    }
17};
18use crate::{
19    Convoluted,
20    MaybeBottom
21};
22
23pub mod automaton;
24mod search;
25pub use search::{search, multi_search};
26
27///
28pub struct Convolution {
29    // ...
30}
31
32// /// Indexed symbols.
33// pub trait Indexed: Symbol + Ranked {
34//     /// Get the index of the n-th position.
35//     fn index(n: usize) -> usize;
36// }
37
38pub struct ConvolutedPatternBuilder<F: Symbol, X: Clone> {
39    sub_patterns_to_convolute: Vec<Convoluted<Pattern<F, X>>>,
40    arity: usize
41}
42
43impl<F: Symbol, X: Clone> ConvolutedPatternBuilder<F, X> {
44    pub fn new() -> ConvolutedPatternBuilder<F, X> {
45        ConvolutedPatternBuilder {
46            sub_patterns_to_convolute: Vec::new(),
47            arity: 0
48        }
49    }
50
51    /// Set the sub-pattern i of the pattern k.
52    pub fn set(&mut self, k: usize, i: usize, pattern: Pattern<F, X>) {
53        if self.sub_patterns_to_convolute.len() <= i {
54            let mut list = Vec::new();
55            list.resize(self.arity+1, MaybeBottom::Bottom);
56            self.sub_patterns_to_convolute.resize(i+1, Convoluted(list));
57        }
58
59        if self.arity <= k {
60            for sub_pattern in self.sub_patterns_to_convolute.iter_mut() {
61                sub_pattern.0.resize(k+1, MaybeBottom::Bottom);
62            }
63
64            self.arity = k;
65        }
66
67        self.sub_patterns_to_convolute[i].0[k] = MaybeBottom::Some(pattern)
68    }
69
70    pub fn unwrap(self) -> Vec<Convoluted<Pattern<F, X>>> {
71        self.sub_patterns_to_convolute
72    }
73}
74
75impl<F: Symbol + Ranked> crate::Convolution<F> for Convolution {
76    /// Perform a term convolution.
77    fn convolute<T: AsRef<[Option<Term<F>>]>>(terms: T) -> Term<Rank<Convoluted<F>>> {
78        let terms = terms.as_ref();
79
80        let mut convoluted_symbol = Vec::with_capacity(terms.len());
81        let mut sub_terms_to_convolute = Vec::new();
82
83        for (k, term) in terms.iter().enumerate() {
84            if let Some(term) = term {
85                convoluted_symbol.push(MaybeBottom::Some(term.symbol().clone()));
86
87                for (i, sub_term) in term.sub_terms().iter().enumerate() {
88                    if sub_terms_to_convolute.len() <= i {
89                        let mut vec = Vec::with_capacity(k);
90                        vec.resize(k, None);
91                        sub_terms_to_convolute.resize(i+1, vec);
92                    }
93                    sub_terms_to_convolute[i].push(Some(sub_term.clone()));
94                }
95
96                for i in term.sub_terms().len()..sub_terms_to_convolute.len() {
97                    sub_terms_to_convolute[i].push(None);
98                }
99            } else {
100                convoluted_symbol.push(MaybeBottom::Bottom);
101                for i in 0..sub_terms_to_convolute.len() {
102                    sub_terms_to_convolute[i].push(None);
103                }
104            }
105        }
106
107        let convoluted_sub_terms = sub_terms_to_convolute.iter().map(|sub_terms| {
108            Self::convolute(&sub_terms)
109        }).collect();
110
111        Term::new(Rank(Convoluted(convoluted_symbol), sub_terms_to_convolute.len()), convoluted_sub_terms)
112    }
113
114    /// Perform a term deconvolution.
115    fn deconvolute(_term: Term<Rank<Convoluted<F>>>) -> Vec<Option<Term<F>>> {
116        panic!("TODO deconvolution");
117    }
118
119    /// Create the equality relation between n terms.
120    fn equality<Q: State>(aut: &Automaton<F, Q, NoLabel>, n: usize) -> Automaton<Rank<Convoluted<F>>, Q, NoLabel> {
121        let mut eq_aut = Automaton::new();
122
123        for (Configuration(f, sub_states), _, q) in aut.transitions() {
124            let mut convoluted_f = Vec::with_capacity(n);
125            convoluted_f.resize(n, MaybeBottom::Some(f.clone()));
126
127            eq_aut.add(Configuration(Rank(Convoluted(convoluted_f), sub_states.len()), sub_states.clone()), NoLabel, q.clone());
128        }
129
130        for final_q in aut.final_states() {
131            eq_aut.set_final(final_q.clone());
132        }
133
134        eq_aut
135    }
136
137    // fn nat_less<Q: State>(s: F, zero: F) -> Automaton<Rank<Convoluted<F>>, Q, NoLabel> {
138    //     let mut eq_aut = Automaton::new();
139    //
140    //     // ...
141    // }
142
143    fn generic_automaton<Q: State>(aut: &Automaton<Rank<Convoluted<F>>, Q, NoLabel>) -> ta::alternating::Automaton<Convoluted<F>, Q, Convoluted<u32>> {
144        let mut alt = ta::alternating::Automaton::new();
145
146        for (Configuration(convoluted_f, subs), _, convoluted_q) in aut.transitions() {
147            let conjunction = subs.iter().enumerate().map(|(i, convoluted_sub)| {
148                let indexes = convoluted_f.0.iter().map(|f| {
149                    if let MaybeBottom::Some(f) = f {
150                        if i < f.arity() {
151                            MaybeBottom::Some(i as u32)
152                        } else {
153                            MaybeBottom::Bottom
154                        }
155                    } else {
156                        MaybeBottom::Bottom
157                    }
158                }).collect();
159                (Convoluted(indexes), convoluted_sub.clone())
160            }).collect();
161            alt.add(convoluted_q, &convoluted_f.0, conjunction);
162        }
163
164        for convoluted_q in aut.final_states() {
165            alt.set_initial(convoluted_q.clone());
166        }
167
168        alt
169    }
170
171    fn state_convolution<E, Q: LanguageState<F, E>>(initial_state: Convoluted<Q>, env: &E) -> Automaton<Rank<Convoluted<F>>, Convoluted<Q>, NoLabel> {
172        automaton::state_convolution(initial_state, env)
173    }
174
175    fn search<'a, 'e, Q: State, X: 'a + Family + Ord>(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> {
176        Box::new(multi_search(automata, patterns, kill_signal))
177    }
178}
179
180//
181
182// #[derive(Clone, Debug)]
183// pub struct Convoluted<Pattern<F, X>>(pub Vec<MaybeBottom<Pattern<F, X>>>);
184//
185// impl<F: fmt::Display, X: fmt::Display> fmt::Display for Convoluted<Pattern<F, X>> {
186//     fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
187//         match self.0.split_first() {
188//             Some((head, tail)) => {
189//                 head.fmt(f)?;
190//                 for e in tail.iter() {
191//                     write!(f, "⊗{}", e)?;
192//                 }
193//
194//                 Ok(())
195//             },
196//             None => Ok(())
197//         }
198//     }
199// }
automatic_relations/convolution/aligned/mod.rs

automatic_relations/convolution/aligned/
mod.rs
