ftml_solver/rules/fixity/
bin.rs

1use crate::{
2    CheckRef,
3    rules::{PreparationRule, SizedSolverRule},
4    split::SplitStrategy,
5};
6use ftml_ontology::terms::{ApplicationTerm, Argument, IsTerm, MaybeSequence, Term, VarOrSym};
7use ftml_uris::SymbolUri;
8use std::ops::ControlFlow;
9
10#[derive(Debug, Clone, PartialEq, Eq)]
11pub struct BinLRule(pub SymbolUri);
12
13impl SizedSolverRule for BinLRule {
14    fn priority(&self) -> isize {
15        10_000
16    }
17    fn display(&self) -> Vec<crate::trace::Displayable> {
18        ftml_solver_trace::trace!(&self.0, "is a left-associative binary operator")
19    }
20}
21impl BinLRule {
22    fn app_two(
23        head: Term,
24        pre: &[Argument],
25        a: Term,
26        b: Term,
27        post: &[Argument],
28        presentation: Option<VarOrSym>,
29    ) -> Term {
30        Term::Application(ApplicationTerm::new(
31            head,
32            pre.iter()
33                .cloned()
34                .chain([Argument::Simple(a), Argument::Simple(b)])
35                .chain(post.iter().cloned())
36                .collect(),
37            presentation,
38        ))
39    }
40
41    fn applicable<Split: SplitStrategy>(
42        uri: &SymbolUri,
43        checker: &CheckRef<'_, '_, Split>,
44        t: &Term,
45    ) -> bool {
46        let Some(head) = checker.get_head(t) else {
47            return false;
48        };
49        let head = head.as_ref().map_either(|e| &**e, |e| &**e);
50        super::is_sequence_binary(uri, t, head).is_some()
51    }
52    fn apply<Split: SplitStrategy>(
53        uri: &SymbolUri,
54        checker: &CheckRef<'_, '_, Split>,
55        t: Term,
56    ) -> ControlFlow<Term, Term> {
57        //tracing::trace!("binl!");
58        //println!("binl: {:?}", t.debug_short());
59        let Some(head) = checker.get_head(&t) else {
60            return ControlFlow::Continue(t);
61        };
62        let head = head.as_ref().map_either(|e| &**e, |e| &**e);
63
64        let Some((app, seq, idx)) = super::is_sequence_binary(uri, &t, head) else {
65            return ControlFlow::Continue(t);
66        };
67        let preargs = &app.arguments[..idx];
68        let postargs = &app.arguments[idx + 1..];
69        match seq {
70            MaybeSequence::Seq(seq) => {
71                if seq.len() < 2 {
72                    return ControlFlow::Continue(t);
73                }
74                //SAFETY: len() >= 2
75                unsafe {
76                    ControlFlow::Continue(
77                        seq.iter()
78                            .cloned()
79                            .reduce(|a, b| {
80                                Self::app_two(
81                                    app.head.clone(),
82                                    preargs,
83                                    a,
84                                    b,
85                                    postargs,
86                                    app.presentation.clone(),
87                                )
88                            })
89                            .unwrap_unchecked(),
90                    )
91                }
92            }
93            s @ MaybeSequence::One(_) => ControlFlow::Continue(
94                super::super::sequences::fold::Fold::apply(s.clone(), |a, b| {
95                    Self::app_two(
96                        app.head.clone(),
97                        preargs,
98                        a.into(),
99                        b.into(),
100                        postargs,
101                        app.presentation.clone(),
102                    )
103                }),
104            ),
105        }
106    }
107    pub fn app_rev<Split: SplitStrategy>(
108        uri: &SymbolUri,
109        checker: &CheckRef<'_, '_, Split>,
110        t: &Term,
111    ) -> bool {
112        let Some(head) = checker.get_head(t) else {
113            return false;
114        };
115        let head = head.as_ref().map_either(|e| &**e, |e| &**e);
116        super::was_sequence_binary(uri, t, head).is_some()
117    }
118
119    pub fn rev<Split: SplitStrategy>(
120        uri: &SymbolUri,
121        checker: &CheckRef<'_, '_, Split>,
122        t: Term,
123    ) -> ControlFlow<Term, Term> {
124        let Some(head) = checker.get_head(&t) else {
125            return ControlFlow::Continue(t);
126        };
127        let head = head.as_ref().map_either(|e| &**e, |e| &**e);
128        let Some((app, first, second, idx)) = super::was_sequence_binary(uri, &t, head) else {
129            return ControlFlow::Continue(t);
130        };
131        let pre = &app.arguments[..idx];
132        let post = &app.arguments[idx + 2..];
133        let mut nargs = vec![first.clone()];
134        //nargs.push(Argument::Simple(second.clone()));
135        let mut to_check = second;
136        while super::match_head(head, to_check.head()) {
137            let Some((napp, first, second, nidx)) = super::was_sequence_binary(uri, to_check, head)
138            else {
139                break;
140            };
141            if nidx != idx {
142                break;
143            }
144            let npre = &napp.arguments[..idx];
145            let npost = &napp.arguments[idx + 2..];
146            if npre != pre || npost != post {
147                break;
148            }
149            nargs.push(first.clone());
150            //nargs.push(Argument::Simple(second.clone()));
151            to_check = second;
152        }
153        nargs.push(to_check.clone());
154        let nargs = pre
155            .iter()
156            .cloned()
157            .chain(std::iter::once(Argument::Sequence(MaybeSequence::Seq(
158                nargs.into_boxed_slice(),
159            ))))
160            .chain(post.iter().cloned())
161            .collect();
162        ControlFlow::Continue(Term::Application(ApplicationTerm::new(
163            app.head.clone(),
164            nargs,
165            app.presentation.clone(),
166        )))
167    }
168}
169
170impl<Split: SplitStrategy> PreparationRule<Split> for BinLRule {
171    fn applicable(&self, checker: &CheckRef<'_, '_, Split>, t: &Term) -> bool {
172        Self::applicable(&self.0, checker, t)
173    }
174    fn apply(
175        &self,
176        checker: &mut CheckRef<'_, '_, Split>,
177        t: Term,
178        _: Option<(&mut smallvec::SmallVec<u8, 16>, usize)>,
179    ) -> ControlFlow<Term, Term> {
180        Self::apply(&self.0, checker, t)
181    }
182    fn applicable_revert(&self, checker: &CheckRef<'_, '_, Split>, t: &Term) -> bool {
183        Self::app_rev(&self.0, checker, t)
184    }
185
186    fn revert(&self, checker: &CheckRef<'_, '_, Split>, t: Term) -> ControlFlow<Term, Term> {
187        Self::rev(&self.0, checker, t)
188    }
189}
190
191#[derive(Debug, Clone, PartialEq, Eq)]
192pub struct BinRRule(pub SymbolUri);
193
194impl SizedSolverRule for BinRRule {
195    fn priority(&self) -> isize {
196        10_000
197    }
198    fn display(&self) -> Vec<crate::trace::Displayable> {
199        ftml_solver_trace::trace!(&self.0, "is a right-associative binary operator")
200    }
201}
202impl std::fmt::Display for BinRRule {
203    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
204        write!(f, "{} is a right-associative binary operator", self.0)
205    }
206}
207impl<Split: SplitStrategy> PreparationRule<Split> for BinRRule {
208    fn applicable(&self, checker: &CheckRef<'_, '_, Split>, t: &Term) -> bool {
209        let Some(head) = checker.get_head(t) else {
210            return false;
211        };
212        let head = head.as_ref().map_either(|e| &**e, |e| &**e);
213        super::is_sequence_binary(&self.0, t, head).is_some()
214    }
215    fn apply(
216        &self,
217        checker: &mut CheckRef<'_, '_, Split>,
218        t: Term,
219        _: Option<(&mut smallvec::SmallVec<u8, 16>, usize)>,
220    ) -> ControlFlow<Term, Term> {
221        //println!("binr: {:?}", t.debug_short());
222        let Some(head) = checker.get_head(&t) else {
223            return ControlFlow::Continue(t);
224        };
225        let head = head.as_ref().map_either(|e| &**e, |e| &**e);
226        let Some((app, seq, idx)) = super::is_sequence_binary(&self.0, &t, head) else {
227            return ControlFlow::Continue(t);
228        };
229        let preargs = &app.arguments[..idx];
230        let postargs = &app.arguments[idx + 1..];
231        match seq {
232            MaybeSequence::Seq(seq) => {
233                if seq.len() < 2 {
234                    return ControlFlow::Continue(t);
235                }
236                //SAFETY: len() >= 2
237                unsafe {
238                    ControlFlow::Continue(seq[..seq.len() - 1].iter().cloned().rfold(
239                        seq.last().unwrap_unchecked().clone(),
240                        |a, b| {
241                            Term::Application(ApplicationTerm::new(
242                                app.head.clone(),
243                                {
244                                    let mut args = preargs.to_vec();
245                                    args.extend([Argument::Simple(a), Argument::Simple(b)]);
246                                    args.extend_from_slice(postargs);
247                                    args.into_boxed_slice()
248                                },
249                                app.presentation.clone(),
250                            ))
251                        },
252                    ))
253                }
254            }
255            s @ MaybeSequence::One(_) => ControlFlow::Continue(
256                super::super::sequences::fold::Fold::apply(s.clone(), |a, b| {
257                    BinLRule::app_two(
258                        app.head.clone(),
259                        preargs,
260                        a.into(),
261                        b.into(),
262                        postargs,
263                        app.presentation.clone(),
264                    )
265                }),
266            ),
267        }
268    }
269
270    fn applicable_revert(&self, checker: &CheckRef<'_, '_, Split>, t: &Term) -> bool {
271        let Some(head) = checker.get_head(t) else {
272            return false;
273        };
274        let head = head.as_ref().map_either(|e| &**e, |e| &**e);
275        super::was_sequence_binary(&self.0, t, head).is_some()
276    }
277    fn revert(&self, checker: &CheckRef<'_, '_, Split>, t: Term) -> ControlFlow<Term, Term> {
278        let Some(head) = checker.get_head(&t) else {
279            return ControlFlow::Continue(t);
280        };
281        let head = head.as_ref().map_either(|e| &**e, |e| &**e);
282        let Some((app, first, second, idx)) = super::was_sequence_binary(&self.0, &t, head) else {
283            return ControlFlow::Continue(t);
284        };
285        let pre = &app.arguments[..idx];
286        let post = &app.arguments[idx + 2..];
287        let mut nargs = vec![second.clone()];
288
289        let mut to_check = first;
290        while super::match_head(head, to_check.head()) {
291            let Some((napp, first, second, nidx)) =
292                super::was_sequence_binary(&self.0, to_check, head)
293            else {
294                break;
295            };
296            if nidx != idx {
297                break;
298            }
299            let npre = &napp.arguments[..idx];
300            let npost = &napp.arguments[idx + 2..];
301            if npre != pre || npost != post {
302                break;
303            }
304            //nargs.push(Argument::Simple(first.clone()));
305            nargs.push(second.clone());
306            to_check = first;
307        }
308        nargs.push(to_check.clone());
309        nargs.reverse();
310        let nargs = pre
311            .iter()
312            .cloned()
313            .chain(std::iter::once(Argument::Sequence(MaybeSequence::Seq(
314                nargs.into_boxed_slice(),
315            ))))
316            .chain(post.iter().cloned())
317            .collect();
318        ControlFlow::Continue(Term::Application(ApplicationTerm::new(
319            app.head.clone(),
320            nargs,
321            app.presentation.clone(),
322        )))
323    }
324}
ftml_solver/rules/fixity/bin.rs

ftml_solver/rules/fixity/
bin.rs
