ftml_solver/rules/sequences/
fold.rs

1use ftml_ontology::terms::{
2    BindingTerm, BoundArgument, ComponentVar, MaybeSequence, Term, Variable,
3};
4use ftml_solver_trace::SizedSolverRule;
5use ftml_uris::Id;
6
7use crate::{
8    rules::{InferenceRule, sequences::SequenceType},
9    split::SplitStrategy,
10};
11
12static X: std::sync::LazyLock<Id> =
13    std::sync::LazyLock::new(|| unsafe { "x".parse().unwrap_unchecked() });
14static Y: std::sync::LazyLock<Id> =
15    std::sync::LazyLock::new(|| unsafe { "y".parse().unwrap_unchecked() });
16
17pub struct Fold;
18impl Fold {
19    pub fn apply_init(
20        seq: MaybeSequence<Term>,
21        init: Term,
22        then: impl FnOnce(Variable, Variable) -> Term,
23    ) -> Term {
24        Term::Bound(BindingTerm::new(
25            ftml_uris::metatheory::FOLD_RIGHT.clone().into(),
26            Box::new([
27                BoundArgument::Sequence(seq),
28                BoundArgument::Simple(init),
29                BoundArgument::Bound(ComponentVar {
30                    var: X.clone().into(),
31                    tp: None,
32                    df: None,
33                }),
34                BoundArgument::Bound(ComponentVar {
35                    var: Y.clone().into(),
36                    tp: None,
37                    df: None,
38                }),
39                BoundArgument::Simple(then(X.clone().into(), Y.clone().into())),
40            ]),
41            None,
42        ))
43    }
44    pub fn unapply_init(
45        term: &Term,
46    ) -> Option<(
47        &MaybeSequence<Term>,
48        &Term,
49        &ComponentVar,
50        &ComponentVar,
51        &Term,
52    )> {
53        let Term::Bound(b) = term else { return None };
54        if !b.head.is(&*ftml_uris::metatheory::FOLD_RIGHT) {
55            return None;
56        }
57        let [
58            BoundArgument::Sequence(seq),
59            BoundArgument::Simple(init),
60            BoundArgument::Bound(cv1),
61            BoundArgument::Bound(cv2),
62            BoundArgument::Simple(ret),
63        ] = &*b.arguments
64        else {
65            return None;
66        };
67        Some((seq, init, cv1, cv2, ret))
68    }
69
70    pub fn apply(seq: MaybeSequence<Term>, then: impl FnOnce(Variable, Variable) -> Term) -> Term {
71        Term::Bound(BindingTerm::new(
72            ftml_uris::metatheory::FOLD.clone().into(),
73            Box::new([
74                BoundArgument::Sequence(seq),
75                BoundArgument::Bound(ComponentVar {
76                    var: X.clone().into(),
77                    tp: None,
78                    df: None,
79                }),
80                BoundArgument::Bound(ComponentVar {
81                    var: Y.clone().into(),
82                    tp: None,
83                    df: None,
84                }),
85                BoundArgument::Simple(then(X.clone().into(), Y.clone().into())),
86            ]),
87            None,
88        ))
89    }
90    pub fn unapply(
91        term: &Term,
92    ) -> Option<(&MaybeSequence<Term>, &ComponentVar, &ComponentVar, &Term)> {
93        let Term::Bound(b) = term else { return None };
94        if !b.head.is(&*ftml_uris::metatheory::FOLD) {
95            return None;
96        }
97        let [
98            BoundArgument::Sequence(seq),
99            BoundArgument::Bound(cv1),
100            BoundArgument::Bound(cv2),
101            BoundArgument::Simple(ret),
102        ] = &*b.arguments
103        else {
104            return None;
105        };
106        Some((seq, cv1, cv2, ret))
107    }
108}
109
110#[derive(Debug, Copy, Clone, PartialEq, Eq)]
111pub struct FoldInferenceRule;
112impl SizedSolverRule for FoldInferenceRule {
113    fn display(&self) -> Vec<ftml_solver_trace::Displayable> {
114        ftml_solver_trace::trace!(&*ftml_uris::metatheory::FOLD_RIGHT)
115    }
116}
117impl FoldInferenceRule {
118    fn infer_init<'t, Split: SplitStrategy>(
119        mut checker: crate::CheckRef<'t, '_, Split>,
120        term: &'t Term,
121    ) -> Option<Term> {
122        let (seq, init, cv1, cv2, ret) = Fold::unapply_init(term)?;
123        let seqtp = match seq {
124            MaybeSequence::One(t) => checker.infer_type(t)?,
125            MaybeSequence::Seq(ts) => {
126                let seq = Term::into_seq(ts.iter().cloned());
127                checker.scoped(|checker| checker.infer_type(&seq))?
128            }
129        };
130        let Some(SequenceType::SeqType(seqtp, _)) = seqtp.as_sequence_type() else {
131            checker.failure("not a sequence type");
132            return None;
133        };
134        let inittp = checker.infer_type(init)?;
135        let ncv1 = ComponentVar {
136            var: cv1.var.clone(),
137            tp: Some(seqtp.clone()),
138            df: None,
139        };
140        let ncv2 = ComponentVar {
141            var: cv2.var.clone(),
142            tp: Some(inittp),
143            df: None,
144        };
145        checker.extend_context(ncv1);
146        checker.extend_context(ncv2);
147        checker.infer_type(ret)
148    }
149}
150impl<Split: SplitStrategy> InferenceRule<Split> for FoldInferenceRule {
151    fn applicable(&self, term: &Term) -> bool {
152        Fold::unapply_init(term).is_some() || Fold::unapply(term).is_some()
153    }
154    fn infer<'t>(
155        &self,
156        mut checker: crate::CheckRef<'t, '_, Split>,
157        term: &'t Term,
158    ) -> Option<Term> {
159        let Some((seq, cv1, cv2, ret)) = Fold::unapply(term) else {
160            return Self::infer_init(checker, term);
161        };
162        let seqtp = match seq {
163            MaybeSequence::One(t) => checker.infer_type(t)?,
164            MaybeSequence::Seq(ts) => {
165                let seq = Term::into_seq(ts.iter().cloned());
166                checker.scoped(|checker| checker.infer_type(&seq))?
167            }
168        };
169        let Some(SequenceType::SeqType(seqtp, _)) = seqtp.as_sequence_type() else {
170            checker.failure("not a sequence type");
171            return None;
172        };
173        if let Some(tp) = cv1.tp.as_ref()
174            && checker.scoped(|c| c.check_subtype(seqtp, tp)) != Some(true)
175        {
176            return None;
177        }
178        if let Some(tp) = cv2.tp.as_ref()
179            && checker.scoped(|c| c.check_subtype(seqtp, tp)) != Some(true)
180        {
181            return None;
182        }
183        let ncv1 = ComponentVar {
184            var: cv1.var.clone(),
185            tp: Some(seqtp.clone()),
186            df: None,
187        };
188        let ncv2 = ComponentVar {
189            var: cv2.var.clone(),
190            tp: Some(seqtp.clone()),
191            df: None,
192        };
193        checker.extend_context(ncv1);
194        checker.extend_context(ncv2);
195        checker.infer_type(ret)
196    }
197}
ftml_solver/rules/sequences/fold.rs

ftml_solver/rules/sequences/
fold.rs
