ftml_solver/rules/fixity/
pre.rs

1use crate::{
2    CheckRef,
3    rules::{PreparationRule, SizedSolverRule},
4    split::SplitStrategy,
5};
6use ftml_ontology::terms::{
7    ApplicationTerm, Argument, ArgumentMode, BindingTerm, BoundArgument, MaybeSequence, Term,
8};
9use ftml_uris::SymbolUri;
10use std::ops::ControlFlow;
11
12#[derive(Debug, Clone, PartialEq, Eq)]
13pub struct PrenexRule(pub SymbolUri);
14impl SizedSolverRule for PrenexRule {
15    fn priority(&self) -> isize {
16        10_000
17    }
18    fn display(&self) -> Vec<crate::trace::Displayable> {
19        ftml_solver_trace::trace!(&self.0, " is a prenex binder")
20    }
21}
22impl std::fmt::Display for PrenexRule {
23    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
24        write!(f, "{} is a prenex binder", self.0)
25    }
26}
27
28impl PrenexRule {
29    fn do_app(seq_index: usize, app: ApplicationTerm) -> std::ops::ControlFlow<Term, Term> {
30        let pre = &app.arguments[..seq_index];
31        let post = &app.arguments[seq_index + 1..];
32        let Some(Argument::Sequence(seq)) = app.arguments.get(seq_index) else {
33            return ControlFlow::Continue(Term::Application(app));
34        };
35        match seq {
36            MaybeSequence::One(v) => {
37                let mut joined = pre.to_vec();
38                joined.push(Argument::Simple(v.clone()));
39                joined.extend_from_slice(post);
40                ControlFlow::Continue(Term::Application(ApplicationTerm::new(
41                    app.head.clone(),
42                    joined.into_boxed_slice(),
43                    app.presentation.clone(),
44                )))
45            }
46            MaybeSequence::Seq(m) => {
47                let Some(Argument::Simple(last)) = post.last() else {
48                    return ControlFlow::Continue(Term::Application(app));
49                };
50                let post = &post[..post.len() - 1];
51                let t = m.iter().rfold(last.clone(), |t, v| {
52                    let mut joined = pre.to_vec();
53                    joined.push(Argument::Simple(v.clone()));
54                    joined.extend_from_slice(post);
55                    joined.push(Argument::Simple(t));
56                    Term::Application(ApplicationTerm::new(
57                        app.head.clone(),
58                        joined.into_boxed_slice(),
59                        app.presentation.clone(),
60                    ))
61                });
62                ControlFlow::Continue(t)
63            }
64        }
65    }
66
67    fn do_bound(bound_index: usize, b: BindingTerm) -> std::ops::ControlFlow<Term, Term> {
68        let pre = &b.arguments[..bound_index];
69        let post = &b.arguments[bound_index + 1..];
70        let Some(BoundArgument::BoundSeq(bound)) = b.arguments.get(bound_index) else {
71            return ControlFlow::Continue(Term::Bound(b));
72        };
73        match bound {
74            MaybeSequence::One(v) => {
75                let mut joined = pre.to_vec();
76                joined.push(BoundArgument::Bound(v.clone()));
77                joined.extend_from_slice(post);
78                ControlFlow::Continue(Term::Bound(BindingTerm::new(
79                    b.head.clone(),
80                    joined.into_boxed_slice(),
81                    b.presentation.clone(),
82                )))
83            }
84            MaybeSequence::Seq(m) => {
85                let Some(BoundArgument::Simple(last)) = post.last() else {
86                    return ControlFlow::Continue(Term::Bound(b));
87                };
88                let post = &post[..post.len() - 1];
89                let t = m.iter().rfold(last.clone(), |t, v| {
90                    let mut joined = pre.to_vec();
91                    joined.push(BoundArgument::Bound(v.clone()));
92                    joined.extend_from_slice(post);
93                    joined.push(BoundArgument::Simple(t));
94                    Term::Bound(BindingTerm::new(
95                        b.head.clone(),
96                        joined.into_boxed_slice(),
97                        b.presentation.clone(),
98                    ))
99                });
100                ControlFlow::Continue(t)
101            }
102        }
103    }
104}
105
106impl<Split: SplitStrategy> PreparationRule<Split> for PrenexRule {
107    fn applicable(&self, checker: &CheckRef<'_, '_, Split>, t: &Term) -> bool {
108        let Some(head) = checker.get_head(t) else {
109            return false;
110        };
111        let head = head.as_ref().map_either(|e| &**e, |e| &**e);
112        let either::Left(sym) = head else {
113            return false;
114        };
115        if sym.uri != self.0 {
116            return false;
117        }
118        if let Term::Bound(b) = t {
119            let Some(bound_index) = sym
120                .data
121                .arity
122                .iter()
123                .position(|m| matches!(m, ArgumentMode::BoundVariableSequence))
124            else {
125                tracing::trace!("No bound index");
126                return false;
127            };
128            matches!(
129                b.arguments.get(bound_index),
130                Some(BoundArgument::BoundSeq(_))
131            )
132        } else if let Term::Application(a) = t {
133            let Some(seq_index) = sym
134                .data
135                .arity
136                .iter()
137                .position(|m| matches!(m, ArgumentMode::Sequence))
138            else {
139                tracing::trace!("No sequence index");
140                return false;
141            };
142            matches!(
143                a.arguments.get(seq_index),
144                Some(Argument::Sequence(MaybeSequence::Seq(_)))
145            )
146        } else {
147            tracing::trace!("Not a binder or application");
148            false
149        }
150    }
151
152    fn apply(
153        &self,
154        checker: &mut CheckRef<'_, '_, Split>,
155        t: Term,
156        path: Option<(&mut smallvec::SmallVec<u8, 16>, usize)>,
157    ) -> std::ops::ControlFlow<Term, Term> {
158        tracing::trace!("Prenexing");
159        let Some(head) = checker.get_head(&t) else {
160            return ControlFlow::Continue(t);
161        };
162        let head = head.as_ref().map_either(|e| &**e, |e| &**e);
163        let either::Left(sym) = head else {
164            return ControlFlow::Continue(t);
165        };
166        match t {
167            Term::Bound(b) => {
168                if let Some(bound_index) = sym
169                    .data
170                    .arity
171                    .iter()
172                    .position(|m| matches!(m, ArgumentMode::BoundVariableSequence))
173                {
174                    Self::do_bound(bound_index, b)
175                } else {
176                    ControlFlow::Continue(Term::Bound(b))
177                }
178            }
179            Term::Application(a) => {
180                if let Some(seq_index) = sym
181                    .data
182                    .arity
183                    .iter()
184                    .position(|m| matches!(m, ArgumentMode::Sequence))
185                {
186                    Self::do_app(seq_index, a)
187                } else {
188                    ControlFlow::Continue(Term::Application(a))
189                }
190            }
191            o => ControlFlow::Continue(o),
192        }
193    }
194    fn applicable_revert(&self, _: &CheckRef<'_, '_, Split>, _: &Term) -> bool {
195        false
196    }
197    fn revert(&self, _: &CheckRef<'_, '_, Split>, t: Term) -> ControlFlow<Term, Term> {
198        ControlFlow::Continue(t)
199    }
200}
ftml_solver/rules/fixity/pre.rs

ftml_solver/rules/fixity/
pre.rs
