ftml_solver/rules/fixity/
reorder.rs

1use crate::{
2    CheckRef,
3    rules::{PreparationRule, SizedSolverRule},
4    split::SplitStrategy,
5};
6use ftml_ontology::{
7    terms::{ApplicationTerm, BindingTerm, Term},
8    utils::Permutation,
9};
10use ftml_uris::SymbolUri;
11use std::ops::ControlFlow;
12
13#[derive(Debug, Clone, PartialEq, Eq)]
14pub struct ReorderRule {
15    pub symbol: SymbolUri,
16    pub reorder: Permutation,
17}
18impl SizedSolverRule for ReorderRule {
19    fn priority(&self) -> isize {
20        100_000
21    }
22    fn display(&self) -> Vec<crate::trace::Displayable> {
23        ftml_solver_trace::trace!(
24            &self.symbol,
25            format!("reorders argument {:?}", self.reorder)
26        )
27    }
28}
29impl std::fmt::Display for ReorderRule {
30    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
31        write!(f, "{} reorder arguments {:?}", self.symbol, self.reorder)
32    }
33}
34
35impl<Split: SplitStrategy> PreparationRule<Split> for ReorderRule {
36    fn applicable(&self, _: &CheckRef<'_, '_, Split>, t: &Term) -> bool {
37        match t {
38            Term::Application(a) => {
39                matches!(&a.head,Term::Symbol { uri, .. } if *uri == self.symbol)
40                    && a.arguments.len() == self.reorder.len()
41            }
42            Term::Bound(b) => {
43                matches!(&b.head,Term::Symbol { uri, .. } if *uri == self.symbol)
44                    && b.arguments.len() == self.reorder.len()
45            }
46            _ => false,
47        }
48    }
49    fn apply(
50        &self,
51        _: &mut CheckRef<'_, '_, Split>,
52        t: Term,
53        path: Option<(&mut smallvec::SmallVec<u8, 16>, usize)>,
54    ) -> ControlFlow<Term, Term> {
55        if let Some(i) = path.and_then(|(v, i)| {
56            v.get_mut(i)
57                .and_then(|i| if *i > 0 { Some(i) } else { None })
58        }) {
59            *i = self.reorder.of(*i).unwrap_or(*i);
60        }
61
62        //tracing::debug!("Reordering {:?}", t.debug_short());
63        let r = match t {
64            Term::Application(app) => Term::Application(ApplicationTerm::new(
65                app.head.clone(),
66                // SAFETY: applicable checks `arguments.len() == self.reorder.len()`
67                unsafe {
68                    debug_assert_eq!(app.arguments.len(), self.reorder.len());
69                    self.reorder.apply_unchecked(&app.arguments)
70                }
71                .into_boxed_slice(),
72                app.presentation.clone(),
73            )),
74            Term::Bound(app) => Term::Bound(BindingTerm::new(
75                app.head.clone(),
76                // SAFETY: applicable checks `arguments.len() == self.reorder.len()`
77                unsafe {
78                    debug_assert_eq!(app.arguments.len(), self.reorder.len());
79                    self.reorder.apply_unchecked(&app.arguments)
80                }
81                .into_boxed_slice(),
82                app.presentation.clone(),
83            )),
84            t => t,
85        };
86        //tracing::debug!("Result: {:?}", r.debug_short());
87        ControlFlow::Continue(r)
88    }
89    fn applicable_revert(&self, checker: &CheckRef<'_, '_, Split>, t: &Term) -> bool {
90        <Self as PreparationRule<Split>>::applicable(self, checker, t)
91    }
92    fn revert(&self, _: &CheckRef<'_, '_, Split>, t: Term) -> ControlFlow<Term, Term> {
93        //tracing::debug!("Reverting Reordering {:?}", t.debug_short());
94        let r = match t {
95            Term::Application(app) => Term::Application(ApplicationTerm::new(
96                app.head.clone(),
97                // SAFETY: applicable checks `arguments.len() == self.reorder.len()`
98                unsafe {
99                    debug_assert_eq!(app.arguments.len(), self.reorder.len());
100                    self.reorder.revert_unchecked(&app.arguments)
101                }
102                .into_boxed_slice(),
103                app.presentation.clone(),
104            )),
105            Term::Bound(app) => Term::Bound(BindingTerm::new(
106                app.head.clone(),
107                // SAFETY: applicable checks `arguments.len() == self.reorder.len()`
108                unsafe {
109                    debug_assert_eq!(app.arguments.len(), self.reorder.len());
110                    self.reorder.revert_unchecked(&app.arguments)
111                }
112                .into_boxed_slice(),
113                app.presentation.clone(),
114            )),
115            t => t,
116        };
117        //tracing::debug!("Result: {:?}", r.debug_short());
118        ControlFlow::Continue(r)
119    }
120}
ftml_solver/rules/fixity/reorder.rs

ftml_solver/rules/fixity/
reorder.rs
