ftml_solver/rules/sequences/
mod.rs

1use ftml_ontology::terms::{
2    ApplicationTerm, Argument, MaybeSequence, Numeric, Term, Variable,
3    sequences::{Sequence, SequenceType},
4};
5use ftml_solver_trace::SizedSolverRule;
6
7use crate::{
8    CheckRef,
9    rules::{
10        EqualityRule, InferenceRule, InhabitableRule, UniverseRule,
11        operators::numbers::{NumberRule, NumberType},
12    },
13    split::SplitStrategy,
14};
15
16pub mod fold;
17pub mod map;
18
19/*
20pub enum Sequence<'t> {
21    Var(&'t Variable),
22    SequenceExpression(&'t [Term]),
23    Map(Box<Self>, &'t Term),
24    Concatenation(Vec<Self>),
25}
26impl Sequence<'_> {
27    pub fn to_term(&self) -> Term {
28        match self {
29            Self::Var(v) => Term::Var {
30                variable: (*v).clone(),
31                presentation: None,
32            },
33            Self::SequenceExpression(ts) => Term::into_seq(ts.iter().cloned()),
34            Self::Map(s, f) => Term::Application(ApplicationTerm::new(
35                ftml_uris::metatheory::SEQUENCE_MAP.clone().into(),
36                Box::new([
37                    Argument::Simple(s.to_term()),
38                    Argument::Simple((*f).clone()),
39                ]),
40                None,
41            )),
42            Self::Concatenation(ts) => Term::Application(ApplicationTerm::new(
43                ftml_uris::metatheory::SEQUENCE_CONC.clone().into(),
44                Box::new([Argument::Sequence(MaybeSequence::Seq(
45                    ts.iter().map(Self::to_term).collect(),
46                ))]),
47                None,
48            )),
49        }
50    }
51    #[must_use]
52    pub fn is_concrete(&self) -> bool {
53        match self {
54            Self::Var(_) => false,
55            Self::SequenceExpression(_) => true,
56            Self::Map(s, _) => s.is_concrete(),
57            Self::Concatenation(v) => v.iter().all(Self::is_concrete),
58        }
59    }
60    #[must_use]
61    pub fn to_concrete(&self) -> Option<Vec<Term>> {
62        match self {
63            Self::Var(_) => None,
64            Self::SequenceExpression(es) => Some(es.to_vec()),
65            Self::Map(seq, f) => seq.to_concrete().map(|seq| {
66                seq.into_iter()
67                    .map(|a| {
68                        Term::Application(ApplicationTerm::new(
69                            (*f).clone(),
70                            Box::new([Argument::Simple(a)]),
71                            None,
72                        ))
73                    })
74                    .collect()
75            }),
76            Self::Concatenation(v) => {
77                let mut ret = Vec::new();
78                for v in v {
79                    ret.extend(v.to_concrete()?);
80                }
81                Some(ret)
82            }
83        }
84    }
85}
86
87pub enum SequenceType<'t> {
88    Var(&'t Variable),
89    SequenceExpression(&'t [Term]),
90    Map(Sequence<'t>, &'t Term),
91    SeqType(&'t Term, Option<&'t [Term]>),
92}
93
94pub trait TermExtSeq: Sized {
95    fn is_sequence_variable(&self) -> bool;
96    fn is_sequence(&self) -> bool;
97    fn as_sequence(&self) -> Option<Sequence<'_>>;
98    fn into_seq(seqs: impl Iterator<Item = Self>) -> Self;
99    fn as_sequence_type(&self) -> Option<SequenceType<'_>>;
100    #[must_use]
101    fn into_seq_type(self) -> Self;
102    #[must_use]
103    fn into_ranged_seq_type(self, range: impl IntoIterator<Item = Term>) -> Self;
104    /*
105    fn as_sequence(&self) -> Option<&[Self]>;
106    fn is_concrete_sequence(&self) -> bool;
107    fn make_concrete_sequence(&self) -> Option<Vec<Self>>;
108     */
109}
110impl TermExtSeq for Term {
111    fn is_sequence_variable(&self) -> bool {
112        matches!(
113            self,
114            Self::Var {
115                variable: Variable::Ref {
116                    is_sequence: Some(true),
117                    ..
118                },
119                ..
120            }
121        )
122    }
123    fn is_sequence(&self) -> bool {
124        if self.is_sequence_variable() {
125            return true;
126        }
127        let Self::Application(app) = self else {
128            return false;
129        };
130        let Self::Symbol { uri, .. } = &app.head else {
131            return false;
132        };
133        if *uri == *ftml_uris::metatheory::SEQUENCE_EXPRESSION
134            && let [Argument::Sequence(MaybeSequence::Seq(_))] = &*app.arguments
135        {
136            true
137        } else if *uri == *ftml_uris::metatheory::SEQUENCE_MAP {
138            if let [
139                Argument::Simple(seq) | Argument::Sequence(MaybeSequence::One(seq)),
140                Argument::Simple(_),
141            ] = &*app.arguments
142                && seq.is_sequence()
143            {
144                true
145            } else {
146                false
147            }
148        } else if *uri == *ftml_uris::metatheory::SEQUENCE_CONC {
149            if let [Argument::Sequence(MaybeSequence::Seq(seq))] = &*app.arguments
150                && seq.iter().all(Self::is_sequence)
151            {
152                true
153            } else {
154                false
155            }
156        } else {
157            false
158        }
159    }
160    fn as_sequence(&self) -> Option<Sequence<'_>> {
161        if let Self::Var {
162            variable:
163                v @ Variable::Ref {
164                    is_sequence: Some(true),
165                    ..
166                },
167            ..
168        } = self
169        {
170            return Some(Sequence::Var(v));
171        }
172        let Self::Application(app) = self else {
173            return None;
174        };
175        let Self::Symbol { uri, .. } = &app.head else {
176            return None;
177        };
178        if *uri == *ftml_uris::metatheory::SEQUENCE_EXPRESSION
179            && let [Argument::Sequence(MaybeSequence::Seq(seq))] = &*app.arguments
180        {
181            Some(Sequence::SequenceExpression(seq))
182        } else if *uri == *ftml_uris::metatheory::SEQUENCE_MAP {
183            if let [
184                Argument::Simple(seq) | Argument::Sequence(MaybeSequence::One(seq)),
185                Argument::Simple(f),
186            ] = &*app.arguments
187                && let Some(seq) = seq.as_sequence()
188            {
189                Some(Sequence::Map(Box::new(seq), f))
190            } else {
191                None
192            }
193        } else if *uri == *ftml_uris::metatheory::SEQUENCE_CONC {
194            if let [Argument::Sequence(MaybeSequence::Seq(seq))] = &*app.arguments
195                && seq.iter().all(Self::is_sequence)
196            {
197                Some(Sequence::Concatenation(
198                    seq.iter().filter_map(Term::as_sequence).collect(),
199                ))
200            } else {
201                None
202            }
203        } else {
204            None
205        }
206    }
207    fn into_seq(seqs: impl Iterator<Item = Self>) -> Self {
208        Self::Application(ApplicationTerm::new(
209            Self::Symbol {
210                uri: ftml_uris::metatheory::SEQUENCE_EXPRESSION.clone(),
211                presentation: None,
212            },
213            Box::new([Argument::Sequence(MaybeSequence::Seq(seqs.collect()))]),
214            None,
215        ))
216    }
217
218    fn as_sequence_type(&self) -> Option<SequenceType<'_>> {
219        if let Self::Application(app) = self
220            && let Self::Symbol { uri, .. } = &app.head
221        {
222            if *uri == *ftml_uris::metatheory::SEQUENCE_TYPE
223                && let [Argument::Simple(t)] = &*app.arguments
224            {
225                Some(SequenceType::SeqType(t, None))
226            } else if *uri == *ftml_uris::metatheory::RANGED_SEQUENCE_TYPE
227                && let [
228                    Argument::Simple(t),
229                    Argument::Sequence(MaybeSequence::Seq(range)),
230                ] = &*app.arguments
231            {
232                Some(SequenceType::SeqType(t, Some(&**range)))
233            } else if *uri == *ftml_uris::metatheory::SEQUENCE_MAP
234                && let [
235                    Argument::Simple(seq) | Argument::Sequence(MaybeSequence::One(seq)),
236                    Argument::Simple(f),
237                ] = &*app.arguments
238            {
239                Some(SequenceType::Map(seq.as_sequence()?, f))
240            } else {
241                None
242            }
243        } else if let Self::Var {
244            variable:
245                v @ Variable::Ref {
246                    is_sequence: Some(true),
247                    ..
248                },
249            ..
250        } = self
251        {
252            // TODO check that variable is inhabitable?
253            Some(SequenceType::Var(v))
254        } else {
255            None
256        }
257    }
258
259    fn into_seq_type(self) -> Self {
260        Self::Application(ApplicationTerm::new(
261            Self::Symbol {
262                uri: ftml_uris::metatheory::SEQUENCE_TYPE.clone(),
263                presentation: None,
264            },
265            Box::new([Argument::Simple(self)]),
266            None,
267        ))
268    }
269
270    fn into_ranged_seq_type(self, range: impl IntoIterator<Item = Self>) -> Self {
271        Self::Application(ApplicationTerm::new(
272            Self::Symbol {
273                uri: ftml_uris::metatheory::RANGED_SEQUENCE_TYPE.clone(),
274                presentation: None,
275            },
276            Box::new([
277                Argument::Simple(self),
278                Argument::Sequence(MaybeSequence::Seq(range.into_iter().collect())),
279            ]),
280            None,
281        ))
282    }
283
284    /*
285    fn is_concrete_sequence(&self) -> bool {
286        let Self::Application(app) = self else {
287            return false;
288        };
289        let Self::Symbol { uri, .. } = &app.head else {
290            return false;
291        };
292        if *uri == *ftml_uris::metatheory::SEQUENCE_EXPRESSION {
293            return matches!(&*app.arguments, [Argument::Sequence(MaybeSequence::Seq(_))]);
294        }
295        if *uri == *ftml_uris::metatheory::SEQUENCE_MAP {
296            let [
297                Argument::Simple(seq) | Argument::Sequence(MaybeSequence::One(seq)),
298                Argument::Simple(_),
299            ] = &*app.arguments
300            else {
301                return false;
302            };
303            seq.is_concrete_sequence()
304        } else {
305            false
306        }
307    }
308    fn make_concrete_sequence(&self) -> Option<Vec<Self>> {
309        let Self::Application(app) = self else {
310            return None;
311        };
312        let Self::Symbol { uri, .. } = &app.head else {
313            return None;
314        };
315        if *uri == *ftml_uris::metatheory::SEQUENCE_EXPRESSION {
316            let [Argument::Sequence(MaybeSequence::Seq(ts))] = &*app.arguments else {
317                return None;
318            };
319            return Some(ts.to_vec());
320        }
321        if *uri == *ftml_uris::metatheory::SEQUENCE_MAP {
322            let [
323                Argument::Simple(seq) | Argument::Sequence(MaybeSequence::One(seq)),
324                Argument::Simple(f),
325            ] = &*app.arguments
326            else {
327                return None;
328            };
329            Some(
330                seq.make_concrete_sequence()?
331                    .into_iter()
332                    .map(|a| {
333                        Self::Application(ApplicationTerm::new(
334                            f.clone(),
335                            Box::new([Argument::Simple(a)]),
336                            None,
337                        ))
338                    })
339                    .collect(),
340            )
341        } else {
342            None
343        }
344    }
345     */
346}
347 */
348
349#[allow(clippy::match_like_matches_macro)]
350const fn is_index(t: &Argument) -> bool {
351    match t {
352        Argument::Simple(Term::Number(Numeric::Int(_))) => true,
353        _ => false,
354    }
355}
356
357#[derive(Debug, Clone, Copy, PartialEq, Eq)]
358pub struct SeqConcatInferenceRule;
359impl SizedSolverRule for SeqConcatInferenceRule {
360    fn priority(&self) -> isize {
361        1000
362    }
363    fn display(&self) -> Vec<crate::trace::Displayable> {
364        ftml_solver_trace::trace!("sequence concatenation inference")
365    }
366}
367impl<Split: SplitStrategy> InferenceRule<Split> for SeqConcatInferenceRule {
368    fn applicable(&self, term: &Term) -> bool {
369        if let Term::Application(app) = term
370            && app.head.is(&*ftml_uris::metatheory::SEQUENCE_CONC)
371            && let [Argument::Sequence(MaybeSequence::Seq(seq))] = &*app.arguments
372            && seq.iter().all(|s| s.is_sequence())
373        {
374            true
375        } else {
376            false
377        }
378    }
379    fn infer<'t>(&self, mut checker: CheckRef<'t, '_, Split>, term: &'t Term) -> Option<Term> {
380        let Term::Application(app) = term else {
381            return None;
382        };
383        let [Argument::Sequence(MaybeSequence::Seq(seq))] = &*app.arguments else {
384            return None;
385        };
386        let mut curr = None;
387        for s in seq {
388            let tp = checker.infer_type(s)?;
389            if let Some(otp) = curr.as_ref() {
390                if checker.scoped(|c| c.check_equality(otp, &tp)) != Some(true) {
391                    return None;
392                }
393            } else {
394                curr = Some(tp);
395            }
396        }
397        curr
398    }
399}
400
401#[derive(Debug, Clone, Copy, PartialEq, Eq)]
402pub struct SeqIndexRule;
403impl SizedSolverRule for SeqIndexRule {
404    fn priority(&self) -> isize {
405        1000
406    }
407    fn display(&self) -> Vec<crate::trace::Displayable> {
408        ftml_solver_trace::trace!("sequence index")
409    }
410}
411impl<Split: SplitStrategy> InferenceRule<Split> for SeqIndexRule {
412    fn applicable(&self, term: &Term) -> bool {
413        matches!(term,Term::Application(app) if app.head.is_sequence_variable() && app.arguments.len() == 1
414            && matches!(app.arguments.first(),Some(Argument::Simple(_)))
415            //&& app.arguments.first().is_some_and(is_index)
416        )
417    }
418    fn infer<'t>(&self, mut checker: CheckRef<'t, '_, Split>, term: &'t Term) -> Option<Term> {
419        let Term::Application(app) = term else {
420            return None;
421        };
422        let tp = checker.infer_type(&app.head)?;
423        if let SequenceType::SeqType(t, _) = tp.as_sequence_type()? {
424            Some(t.clone())
425        } else {
426            let Some(Argument::Simple(index)) = app.arguments.first() else {
427                checker.failure("First argument is not simple");
428                return None;
429            }; //.clone();
430            let indextp = checker.infer_type(index)?;
431            if NumberRule::is_number_term(&indextp, &checker)
432                .is_none_or(|t| !(t <= NumberType::Integers))
433            {
434                checker.failure("index is not an ordinal type");
435                return None;
436            }
437            Some(Term::Application(ApplicationTerm::new(
438                tp,
439                Box::new([Argument::Simple(index.clone())]),
440                None,
441            )))
442        }
443    }
444}
445
446#[derive(Debug, Clone, Copy, PartialEq, Eq)]
447pub struct SeqUniverseRule;
448impl SizedSolverRule for SeqUniverseRule {
449    fn display(&self) -> Vec<crate::trace::Displayable> {
450        ftml_solver_trace::trace!("sequences of inhabitables/universes are inhabitable/universes")
451    }
452}
453impl<Split: SplitStrategy> UniverseRule<Split> for SeqUniverseRule {
454    fn applicable(&self, term: &Term) -> bool {
455        term.as_sequence_type().is_some()
456    }
457    fn apply<'t>(&self, mut checker: CheckRef<'t, '_, Split>, term: &'t Term) -> Option<bool> {
458        match term.as_sequence_type()? {
459            SequenceType::SeqType(univ, _) => checker.check_universe(univ),
460            SequenceType::SequenceExpression(expr) => {
461                for e in expr {
462                    if checker.check_universe(e) != Some(true) {
463                        return None;
464                    }
465                }
466                Some(true)
467            }
468            _ => None, // TODO?
469        }
470    }
471}
472impl<Split: SplitStrategy> InhabitableRule<Split> for SeqUniverseRule {
473    fn applicable(&self, term: &Term) -> bool {
474        term.as_sequence_type().is_some()
475    }
476    fn apply<'t>(&self, mut checker: CheckRef<'t, '_, Split>, term: &'t Term) -> Option<bool> {
477        //let univ = term.as_sequence_type()?;
478        match term.as_sequence_type()? {
479            SequenceType::SeqType(inh, _) => checker.check_inhabitable(inh),
480            SequenceType::SequenceExpression(expr) => {
481                for e in expr {
482                    if checker.check_inhabitable(e) != Some(true) {
483                        return None;
484                    }
485                }
486                Some(true)
487            }
488            _ => None, // TODO?
489        }
490    }
491}
492
493#[derive(Debug, Clone, Copy, PartialEq, Eq)]
494pub struct SeqInferenceRule;
495impl SizedSolverRule for SeqInferenceRule {
496    fn display(&self) -> Vec<crate::trace::Displayable> {
497        ftml_solver_trace::trace!("sequences have sequence types")
498    }
499}
500impl<Split: SplitStrategy> InferenceRule<Split> for SeqInferenceRule {
501    fn applicable(&self, term: &Term) -> bool {
502        matches!(term.as_sequence(), Some(Sequence::SequenceExpression(_)))
503    }
504    fn infer<'t>(&self, mut checker: CheckRef<'t, '_, Split>, term: &'t Term) -> Option<Term> {
505        //checker.comment(format!("Here: {:?}", term.debug_short()));
506        let Some(Sequence::SequenceExpression(elems)) = term.as_sequence() else {
507            return None;
508        };
509        let mut curr = None;
510        for e in elems {
511            if let Some(tp) = &curr {
512                if checker.scoped(|checker| checker.check_type(e, tp)) != Some(true) {
513                    return None;
514                }
515            } else {
516                curr = Some(checker.infer_type(e)?);
517            }
518        }
519        curr.map(Term::into_seq_type)
520    }
521}
522
523/*
524#[derive(Debug, Clone, Copy, PartialEq, Eq)]
525pub struct SeqTypeEqRule;
526impl SizedSolverRule for SeqTypeEqRule {
527    fn display(&self) -> Vec<crate::trace::Displayable> {
528        ftml_solver_trace::trace!("sequences of types are sequence types")
529    }
530}
531impl<Split: SplitStrategy> EqualityRule<Split> for SeqTypeEqRule {
532    fn applicable(&self, lhs: &Term, rhs: &Term) -> bool {
533        (lhs.as_sequence_type().is_some() && rhs.as_sequence().is_some_and(|r| r.is_concrete()))
534            || (rhs.as_sequence_type().is_some()
535                && lhs.as_sequence().is_some_and(|r| r.is_concrete()))
536    }
537    fn apply<'t>(
538        &self,
539        mut checker: CheckRef<'t, '_, Split>,
540        lhs: &'t Term,
541        rhs: &'t Term,
542    ) -> Option<bool> {
543        if rhs.as_sequence_type().is_some() && lhs.as_sequence().is_some_and(|r| r.is_concrete()) {
544            return self.apply(checker, rhs, lhs);
545        }
546        let Some(SequenceType::SeqType(seqtp, _)) = lhs.as_sequence_type() else {
547            return None;
548        };
549        let seq = rhs.as_sequence()?.to_concrete()?;
550        checker.comment(format!(
551            "Here: {seq:#?}\n    Type: {:?}",
552            seqtp.debug_short()
553        ));
554        for t in seq {
555            if checker.scoped(|c| c.check_equality(&t, seqtp)) != Some(true) {
556                return None;
557            }
558        }
559        Some(true)
560    }
561}
562 */
ftml_solver/rules/sequences/mod.rs

ftml_solver/rules/sequences/
mod.rs
