ftml_solver/rules/fixity/
conj.rs

1use crate::{
2    CheckRef,
3    rules::{MarkerRule, PreparationRule, SizedSolverRule},
4    split::SplitStrategy,
5};
6use ftml_ontology::terms::{ApplicationTerm, Argument, MaybeSequence, Term};
7use ftml_uris::SymbolUri;
8use std::ops::ControlFlow;
9
10#[derive(Debug, Clone, PartialEq, Eq)]
11pub struct IsConjunctionRule(pub SymbolUri);
12impl SizedSolverRule for IsConjunctionRule {
13    fn display(&self) -> Vec<crate::trace::Displayable> {
14        ftml_solver_trace::trace!(&self.0, "is a conjunction")
15    }
16}
17impl<Split: SplitStrategy> MarkerRule<Split> for IsConjunctionRule {}
18
19#[derive(Debug, Clone, PartialEq, Eq)]
20pub struct ConjunctiveRule(pub SymbolUri);
21impl SizedSolverRule for ConjunctiveRule {
22    fn priority(&self) -> isize {
23        10_000
24    }
25    fn display(&self) -> Vec<crate::trace::Displayable> {
26        ftml_solver_trace::trace!(&self.0, " is conjunctive")
27    }
28}
29impl std::fmt::Display for ConjunctiveRule {
30    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
31        write!(f, "{} is conjunctive", self.0)
32    }
33}
34impl<Split: SplitStrategy> PreparationRule<Split> for ConjunctiveRule {
35    fn applicable(&self, checker: &CheckRef<'_, '_, Split>, t: &Term) -> bool {
36        let Some(head) = checker.get_head(t) else {
37            return false;
38        };
39        let head = head.as_ref().map_either(|e| &**e, |e| &**e);
40        super::is_sequence_binary(&self.0, t, head).is_some()
41    }
42    fn apply(
43        &self,
44        checker: &mut CheckRef<'_, '_, Split>,
45        t: Term,
46        path: Option<(&mut smallvec::SmallVec<u8, 16>, usize)>,
47    ) -> ControlFlow<Term, Term> {
48        let Some(head) = checker.get_head(&t) else {
49            return ControlFlow::Continue(t);
50        };
51        let head = head.as_ref().map_either(|e| &**e, |e| &**e);
52        let Some((app, args, index)) = super::is_sequence_binary(&self.0, &t, head) else {
53            return ControlFlow::Continue(t);
54        };
55        let Some(conj): Option<&IsConjunctionRule> = checker
56            .rules()
57            .marker()
58            .iter()
59            .rev()
60            .find_map(|rl| rl.as_any().downcast_ref())
61        else {
62            return ControlFlow::Continue(t);
63        };
64        let pre = &app.arguments[..index];
65        let post = &app.arguments[index + 1..];
66        let args: &[Term] = match args {
67            MaybeSequence::Seq(s) => s,
68            MaybeSequence::One(o) => std::slice::from_ref(o),
69        };
70        if args.is_empty() {
71            return ControlFlow::Continue(t);
72        }
73        let conjuncts = args.iter().map(|a| {
74            Term::Application(ApplicationTerm::new(
75                app.head.clone(),
76                {
77                    let mut args = pre.to_vec();
78                    args.push(Argument::Simple(a.clone()));
79                    args.extend_from_slice(post);
80                    args.into_boxed_slice()
81                },
82                app.presentation.clone(),
83            ))
84        });
85        // SAFETY: !args.is_empty()
86        let t = unsafe {
87            conjuncts
88                .reduce(|a, b| {
89                    Term::Application(ApplicationTerm::new(
90                        Term::Symbol {
91                            uri: conj.0.clone(),
92                            presentation: None,
93                        },
94                        Box::new([Argument::Simple(a), Argument::Simple(b)]),
95                        None,
96                    ))
97                })
98                .unwrap_unchecked()
99        };
100        ControlFlow::Continue(t)
101    }
102
103    fn applicable_revert(&self, _: &CheckRef<'_, '_, Split>, _: &Term) -> bool {
104        false
105    }
106    fn revert(&self, _: &CheckRef<'_, '_, Split>, t: Term) -> ControlFlow<Term, Term> {
107        ControlFlow::Continue(t)
108    }
109}
110
111#[derive(Debug, Clone, PartialEq, Eq)]
112pub struct PairwiseConjunctiveRule(pub SymbolUri);
113impl SizedSolverRule for PairwiseConjunctiveRule {
114    fn priority(&self) -> isize {
115        10_000
116    }
117    fn display(&self) -> Vec<crate::trace::Displayable> {
118        ftml_solver_trace::trace!(&self.0, " is pairwise conjunctive")
119    }
120}
121impl std::fmt::Display for PairwiseConjunctiveRule {
122    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
123        write!(f, "{} is pairwise conjunctive", self.0)
124    }
125}
126impl<Split: SplitStrategy> PreparationRule<Split> for PairwiseConjunctiveRule {
127    fn applicable(&self, checker: &CheckRef<'_, '_, Split>, t: &Term) -> bool {
128        let Some(head) = checker.get_head(t) else {
129            return false;
130        };
131        let head = head.as_ref().map_either(|e| &**e, |e| &**e);
132        super::is_sequence_binary(&self.0, t, head).is_some()
133    }
134    fn apply(
135        &self,
136        checker: &mut CheckRef<'_, '_, Split>,
137        t: Term,
138        path: Option<(&mut smallvec::SmallVec<u8, 16>, usize)>,
139    ) -> ControlFlow<Term, Term> {
140        let Some(head) = checker.get_head(&t) else {
141            return ControlFlow::Continue(t);
142        };
143        let head = head.as_ref().map_either(|e| &**e, |e| &**e);
144        let Some((app, args, index)) = super::is_sequence_binary(&self.0, &t, head) else {
145            return ControlFlow::Continue(t);
146        };
147        let Some(conj): Option<&IsConjunctionRule> = checker
148            .rules()
149            .marker()
150            .iter()
151            .rev()
152            .find_map(|rl| rl.as_any().downcast_ref())
153        else {
154            return ControlFlow::Continue(t);
155        };
156        let pre = &app.arguments[..index];
157        let post = &app.arguments[index + 1..];
158        let args: &[Term] = match args {
159            MaybeSequence::Seq(s) => s,
160            MaybeSequence::One(o) => std::slice::from_ref(o),
161        };
162        if args.len() < 2 {
163            return ControlFlow::Continue(t);
164        }
165        //tracing::debug!("In: {:?}", t.debug_short());
166        let mut conjuncts = (0..args.len() - 1).map(|i| {
167            let (a, b) = (&args[i], &args[i + 1]);
168            Term::Application(ApplicationTerm::new(
169                app.head.clone(),
170                {
171                    let mut args = pre.to_vec();
172                    args.push(Argument::Simple(a.clone()));
173                    args.push(Argument::Simple(b.clone()));
174                    args.extend_from_slice(post);
175                    args.into_boxed_slice()
176                },
177                app.presentation.clone(),
178            ))
179        });
180        let t = if args.len() == 2 {
181            // Safety: args.len() == 2 => conjuncts.len() == 1
182            unsafe { conjuncts.next().unwrap_unchecked() }
183        } else {
184            // SAFETY: args.len() > 2 => conjuncts.len() >= 2
185            unsafe {
186                conjuncts
187                    .reduce(|a, b| {
188                        Term::Application(ApplicationTerm::new(
189                            Term::Symbol {
190                                uri: conj.0.clone(),
191                                presentation: None,
192                            },
193                            Box::new([Argument::Simple(a), Argument::Simple(b)]),
194                            None,
195                        ))
196                    })
197                    .unwrap_unchecked()
198            }
199        };
200        //tracing::debug!("Out: {:?}", t.debug_short());
201        ControlFlow::Continue(t)
202    }
203    fn applicable_revert(&self, checker: &CheckRef<'_, '_, Split>, t: &Term) -> bool {
204        super::bin::BinLRule::app_rev(&self.0, checker, t)
205    }
206    fn revert(&self, checker: &CheckRef<'_, '_, Split>, t: Term) -> ControlFlow<Term, Term> {
207        super::bin::BinLRule::rev(&self.0, checker, t)
208    }
209}
ftml_solver/rules/fixity/conj.rs

ftml_solver/rules/fixity/
conj.rs
