ftml_solver/rules/operators/
letin.rs

1use ftml_ontology::terms::{BindingTerm, BoundArgument, ComponentVar, MaybeSequence, Term};
2use ftml_solver_trace::SizedSolverRule;
3use ftml_uris::SymbolUri;
4
5use crate::{
6    rules::{PreparationRule, SimplificationRule},
7    split::SplitStrategy,
8};
9
10#[derive(Debug, Clone, PartialEq, Eq)]
11pub struct LetinComputation(pub SymbolUri);
12
13impl SizedSolverRule for LetinComputation {
14    fn display(&self) -> Vec<crate::trace::Displayable> {
15        ftml_solver_trace::trace!(&self.0, " x := t in s ==> s[x/t]")
16    }
17}
18impl<Split: SplitStrategy> PreparationRule<Split> for LetinComputation {
19    fn applicable(&self, checker: &crate::CheckRef<'_, '_, Split>, t: &Term) -> bool {
20        false
21    }
22    fn applicable_revert(&self, checker: &crate::CheckRef<'_, '_, Split>, t: &Term) -> bool {
23        if let Term::Bound(b) = t
24            && let Term::Symbol { uri, .. } = &b.head
25            && *uri == self.0
26            && let [
27                BoundArgument::Bound(_) | BoundArgument::BoundSeq(MaybeSequence::Seq(_)),
28                BoundArgument::Simple(body),
29            ] = &*b.arguments
30        {
31            <Self as SimplificationRule<Split>>::applicable(&self, body)
32        } else {
33            false
34        }
35    }
36    fn apply(
37        &self,
38        checker: &mut crate::CheckRef<'_, '_, Split>,
39        t: Term,
40        path: Option<(&mut smallvec::SmallVec<u8, 16>, usize)>,
41    ) -> std::ops::ControlFlow<Term, Term> {
42        std::ops::ControlFlow::Continue(t)
43    }
44    fn revert(
45        &self,
46        checker: &crate::CheckRef<'_, '_, Split>,
47        t: Term,
48    ) -> std::ops::ControlFlow<Term, Term> {
49        let Term::Bound(b) = t else {
50            return std::ops::ControlFlow::Continue(t);
51        };
52        let [
53            var @ (BoundArgument::Bound(_) | BoundArgument::BoundSeq(MaybeSequence::Seq(_))),
54            BoundArgument::Simple(body),
55        ] = &*b.arguments
56        else {
57            return std::ops::ControlFlow::Continue(Term::Bound(b));
58        };
59        let Term::Bound(b2) = body else {
60            return std::ops::ControlFlow::Continue(Term::Bound(b));
61        };
62        let [
63            var2 @ (BoundArgument::Bound(_) | BoundArgument::BoundSeq(MaybeSequence::Seq(_))),
64            BoundArgument::Simple(body),
65        ] = &*b2.arguments
66        else {
67            return std::ops::ControlFlow::Continue(Term::Bound(b));
68        };
69        let mut vars = Vec::new();
70        match var {
71            BoundArgument::Bound(v) => vars.push(v.clone()),
72            BoundArgument::BoundSeq(MaybeSequence::Seq(v)) => vars = v.clone().into_vec(),
73            _ => unreachable!(),
74        }
75        match var2 {
76            BoundArgument::Bound(v) => vars.push(v.clone()),
77            BoundArgument::BoundSeq(MaybeSequence::Seq(v)) => vars.extend(v.iter().cloned()),
78            _ => unreachable!(),
79        }
80        std::ops::ControlFlow::Continue(Term::Bound(BindingTerm::new(
81            Term::Symbol {
82                uri: self.0.clone(),
83                presentation: None,
84            },
85            Box::new([
86                BoundArgument::BoundSeq(MaybeSequence::Seq(vars.into_boxed_slice())),
87                BoundArgument::Simple(body.clone()),
88            ]),
89            None,
90        )))
91    }
92}
93
94impl<Split: SplitStrategy> SimplificationRule<Split> for LetinComputation {
95    fn applicable(&self, term: &Term) -> bool {
96        if let Term::Bound(b) = term
97            && let Term::Symbol { uri, .. } = &b.head
98            && *uri == self.0
99            && let [
100                BoundArgument::Bound(_) | BoundArgument::BoundSeq(MaybeSequence::Seq(_)),
101                BoundArgument::Simple(_),
102            ] = &*b.arguments
103        {
104            true
105        } else {
106            false
107        }
108    }
109    fn apply<'t>(
110        &self,
111        mut checker: crate::CheckRef<'t, '_, Split>,
112        term: &'t Term,
113    ) -> Result<Term, Option<ftml_ontology::terms::termpaths::TermPath>> {
114        let Term::Bound(b) = term else {
115            return Err(None);
116        };
117        let [
118            var @ (BoundArgument::Bound(_) | BoundArgument::BoundSeq(MaybeSequence::Seq(_))),
119            BoundArgument::Simple(body),
120        ] = &*b.arguments
121        else {
122            return Err(None);
123        };
124        match var {
125            BoundArgument::Bound(ComponentVar {
126                var, df: Some(d), ..
127            }) => Ok((body / (var.name(), d)).into_owned()),
128            BoundArgument::Bound(v) => Ok((body
129                / (
130                    v.var.name(),
131                    &checker.get_var_definiens(&v.var).ok_or(None)?,
132                ))
133                .into_owned()),
134            BoundArgument::BoundSeq(MaybeSequence::Seq(s)) => s
135                .iter()
136                .rev()
137                .try_fold(body.clone(), |b, v| match v {
138                    ComponentVar {
139                        var, df: Some(d), ..
140                    } => Some(b / (var.name(), d)),
141                    ComponentVar { var, .. } => {
142                        Some(b / (var.name(), &checker.get_var_definiens(&var)?))
143                    }
144                })
145                .ok_or(None),
146            _ => unreachable!(),
147        }
148    }
149}
ftml_solver/rules/operators/letin.rs

ftml_solver/rules/operators/
letin.rs
