ftml_solver/rules/sequences/
map.rs

1use std::hint::unreachable_unchecked;
2
3use ftml_ontology::terms::{
4    ApplicationTerm, Argument, BindingTerm, BoundArgument, ComponentVar, MaybeSequence, Term,
5    Variable,
6};
7use ftml_solver_trace::SizedSolverRule;
8use ftml_uris::SymbolUri;
9
10use crate::{
11    rules::{
12        InferenceRule, InhabitableRule, SimplificationRule,
13        operators::numbers::{NumberRule, NumberType},
14        sequences::{Sequence, SequenceType},
15    },
16    split::SplitStrategy,
17};
18
19/*
20#[derive(Debug, Clone, PartialEq, Eq)]
21pub struct MapInferenceRule(pub SymbolUri);
22impl SizedSolverRule for MapSimplificationRule {
23    fn display(&self) -> Vec<crate::trace::Displayable> {
24        ftml_solver_trace::trace!("{ s:T1*, x:T1, f(x):T2 } ⊢ ",&self.0, "([x1,...,xn],f) :=> T2*")
25    }
26}
27impl<Split: SplitStrategy> InferenceRule<Split> for MapInferenceRule {
28
29}
30 */
31
32#[derive(Debug, Clone, PartialEq, Eq)]
33pub struct MapArgumentSimplificationRule(pub SymbolUri);
34impl SizedSolverRule for MapArgumentSimplificationRule {
35    fn display(&self) -> Vec<crate::trace::Displayable> {
36        ftml_solver_trace::trace!(&self.0, "([x1,...,xn],f) ==> [f(x1),..,f(xn)]")
37    }
38    fn priority(&self) -> isize {
39        1000
40    }
41}
42impl<Split: SplitStrategy> SimplificationRule<Split> for MapArgumentSimplificationRule {
43    fn applicable(&self, term: &Term) -> bool {
44        if let Term::Application(app) = term {
45            app.arguments.iter().any(|a| {
46                if let Argument::Sequence(MaybeSequence::One(t)) = a {
47                    MapSimplificationRule::applicable_i(&self.0, t)
48                } else {
49                    false
50                }
51            })
52        } else if let Term::Bound(app) = term {
53            app.arguments.iter().any(|a| {
54                if let BoundArgument::Sequence(MaybeSequence::One(t)) = a {
55                    MapSimplificationRule::applicable_i(&self.0, t)
56                } else {
57                    false
58                }
59            })
60        } else {
61            false
62        }
63    }
64    fn apply<'t>(
65        &self,
66        mut checker: crate::CheckRef<'t, '_, Split>,
67        term: &'t Term,
68    ) -> Result<Term, Option<ftml_ontology::terms::termpaths::TermPath>> {
69        if let Term::Application(app) = term {
70            Ok(Term::Application(ApplicationTerm::new(
71                app.head.clone(),
72                app.arguments
73                    .iter()
74                    .map(|a| match a {
75                        Argument::Sequence(MaybeSequence::One(t))
76                            if MapSimplificationRule::applicable_i(&self.0, t) =>
77                        {
78                            MapSimplificationRule::apply_i(&mut checker, t).map_or_else(
79                                |_| a.clone(),
80                                |v| Argument::Sequence(MaybeSequence::Seq(v.into_boxed_slice())),
81                            )
82                        }
83                        _ => a.clone(),
84                    })
85                    .collect(),
86                app.presentation.clone(),
87            )))
88        } else if let Term::Bound(app) = term {
89            Ok(Term::Bound(BindingTerm::new(
90                app.head.clone(),
91                app.arguments
92                    .iter()
93                    .map(|a| match a {
94                        BoundArgument::Sequence(MaybeSequence::One(t))
95                            if MapSimplificationRule::applicable_i(&self.0, t) =>
96                        {
97                            MapSimplificationRule::apply_i(&mut checker, t).map_or_else(
98                                |_| a.clone(),
99                                |v| {
100                                    BoundArgument::Sequence(MaybeSequence::Seq(
101                                        v.into_boxed_slice(),
102                                    ))
103                                },
104                            )
105                        }
106                        _ => a.clone(),
107                    })
108                    .collect(),
109                app.presentation.clone(),
110            )))
111        } else {
112            Err(None)
113        }
114    }
115}
116
117#[derive(Debug, Clone, PartialEq, Eq)]
118pub struct MapIndexSimplificationRule(pub SymbolUri);
119impl SizedSolverRule for MapIndexSimplificationRule {
120    fn display(&self) -> Vec<crate::trace::Displayable> {
121        ftml_solver_trace::trace!(&self.0, "(s,f)(i) ==> f(s(i))")
122    }
123}
124impl<Split: SplitStrategy> SimplificationRule<Split> for MapIndexSimplificationRule {
125    fn applicable(&self, term: &Term) -> bool {
126        if let Term::Application(app) = term
127            && let [Argument::Simple(_)] = &*app.arguments
128            && let Term::Application(map) = &app.head
129            && let Term::Symbol { uri, .. } = &map.head
130            && *uri == self.0
131            && let [_, Argument::Simple(_)] = &*map.arguments
132        {
133            true
134        } else {
135            false
136        }
137    }
138    fn apply<'t>(
139        &self,
140        _: crate::CheckRef<'t, '_, Split>,
141        term: &'t Term,
142    ) -> Result<Term, Option<ftml_ontology::terms::termpaths::TermPath>> {
143        let Term::Application(app) = term else {
144            return Err(None);
145        };
146        let [Argument::Simple(idx)] = &*app.arguments else {
147            return Err(None);
148        };
149        let Term::Application(map) = &app.head else {
150            return Err(None);
151        };
152        let [a, Argument::Simple(f)] = &*map.arguments else {
153            return Err(None);
154        };
155        let s = match a {
156            Argument::Simple(t) | Argument::Sequence(MaybeSequence::One(t)) => t.clone(),
157            Argument::Sequence(MaybeSequence::Seq(ts)) => Term::into_seq(ts.iter().cloned()),
158        };
159        Ok(Term::Application(ApplicationTerm::new(
160            f.clone(),
161            Box::new([Argument::Simple(Term::Application(ApplicationTerm::new(
162                s,
163                Box::new([Argument::Simple(idx.clone())]),
164                None,
165            )))]),
166            None,
167        )))
168    }
169}
170
171#[derive(Debug, Clone, PartialEq, Eq)]
172pub struct MapSimplificationRule(pub SymbolUri);
173impl SizedSolverRule for MapSimplificationRule {
174    fn display(&self) -> Vec<crate::trace::Displayable> {
175        ftml_solver_trace::trace!(&self.0, "([x1,...,xn],f) ==> [f(x1),..,f(xn)]")
176    }
177}
178impl MapSimplificationRule {
179    fn apply_i<'t, Split: SplitStrategy>(
180        checker: &mut crate::CheckRef<'t, '_, Split>,
181        term: &'t Term,
182    ) -> Result<Vec<Term>, Option<ftml_ontology::terms::termpaths::TermPath>> {
183        let Term::Application(app) = term else {
184            return Err(None);
185        };
186        let [a, Argument::Simple(f)] = &*app.arguments else {
187            return Err(None);
188        };
189        match a {
190            Argument::Simple(s) | Argument::Sequence(MaybeSequence::One(s)) => {
191                let Some(ts) = s.as_sequence().and_then(|s| s.to_concrete()) else {
192                    return Err(None);
193                };
194                Ok(ts
195                    .into_iter()
196                    .map(|arg| {
197                        let t = Term::Application(ApplicationTerm::new(
198                            f.clone(),
199                            Box::new([Argument::Simple(arg)]),
200                            None,
201                        ));
202                        /*checker
203                        .scoped(|checker| {
204                            checker.simplify_full(
205                                crate::impls::simplify::Expansion::NoDefinitionExpansion,
206                                &t,
207                            )
208                        })
209                        .unwrap_or(t)*/
210                        t
211                    })
212                    .collect())
213            }
214            Argument::Sequence(MaybeSequence::Seq(ts)) => Ok(ts
215                .iter()
216                .map(|arg| {
217                    let t = Term::Application(ApplicationTerm::new(
218                        f.clone(),
219                        Box::new([Argument::Simple(arg.clone())]),
220                        None,
221                    ));
222                    /*
223                    checker
224                        .scoped(|checker| {
225                            checker.simplify_full(
226                                crate::impls::simplify::Expansion::NoDefinitionExpansion,
227                                &t,
228                            )
229                        })
230                        .unwrap_or(t) */
231                    t
232                })
233                .collect()),
234        }
235    }
236    fn applicable_i(sym: &SymbolUri, term: &Term) -> bool {
237        if let Term::Application(app) = term
238            && let Term::Symbol { uri, .. } = &app.head
239            && *uri == *sym
240            && let [a, Argument::Simple(_)] = &*app.arguments
241        {
242            if let Argument::Simple(s) | Argument::Sequence(MaybeSequence::One(s)) = a {
243                s.as_sequence().is_some_and(|seq| seq.is_concrete())
244            } else {
245                true
246            }
247        } else {
248            false
249        }
250    }
251}
252impl<Split: SplitStrategy> SimplificationRule<Split> for MapSimplificationRule {
253    fn applicable(&self, term: &Term) -> bool {
254        Self::applicable_i(&self.0, term)
255    }
256    fn apply<'t>(
257        &self,
258        mut checker: crate::CheckRef<'t, '_, Split>,
259        term: &'t Term,
260    ) -> Result<Term, Option<ftml_ontology::terms::termpaths::TermPath>> {
261        Self::apply_i::<Split>(&mut checker, term).map(|ts| Term::into_seq(ts.into_iter()))
262    }
263}
264
265#[derive(Debug, Clone, PartialEq, Eq)]
266pub struct MapInhabitableRule(pub SymbolUri);
267impl SizedSolverRule for MapInhabitableRule {
268    fn display(&self) -> Vec<crate::trace::Displayable> {
269        ftml_solver_trace::trace!("{ x:A, INH f(x), s:A* } ⊢ INH ", &self.0, "(s,f)")
270    }
271}
272
273impl<Split: SplitStrategy> InhabitableRule<Split> for MapInhabitableRule {
274    fn applicable(&self, term: &ftml_ontology::terms::Term) -> bool {
275        if let Term::Application(app) = term
276            && let Term::Symbol { uri, .. } = &app.head
277        {
278            *uri == self.0 && app.arguments.len() == 2
279        } else {
280            false
281        }
282    }
283    fn apply<'t>(
284        &self,
285        mut checker: crate::CheckRef<'t, '_, Split>,
286        term: &'t ftml_ontology::terms::Term,
287    ) -> Option<bool> {
288        let Term::Application(app) = term else {
289            return None;
290        };
291        let [Argument::Sequence(seq), Argument::Simple(f)] = &*app.arguments else {
292            checker.failure("arguments don't match");
293            return None;
294        };
295        let seqtp = match seq {
296            MaybeSequence::One(t)
297                if matches!(t.as_sequence(), Some(Sequence::SequenceExpression(_))) =>
298            {
299                // SAFETY: pattern match
300                let Some(Sequence::SequenceExpression(args)) = t.as_sequence() else {
301                    unsafe { unreachable_unchecked() }
302                };
303                let mut curr = None;
304                for t in args {
305                    if !checker.scoped::<Option<bool>>(|checker| {
306                        let r = checker.infer_type(t)?;
307                        if let Some(c) = &curr {
308                            if !checker.scoped(|checker| checker.check_equality(c, &r))? {
309                                return None;
310                            }
311                        } else {
312                            curr = Some(r);
313                        }
314                        Some(true)
315                    })? {
316                        return None;
317                    }
318                }
319                curr?
320            }
321            MaybeSequence::One(t) => checker.infer_type(t)?,
322            MaybeSequence::Seq(ts) => {
323                let mut curr = None;
324                for t in ts {
325                    if !checker.scoped::<Option<bool>>(|checker| {
326                        let r = checker.infer_type(t)?;
327                        if let Some(c) = &curr {
328                            if !checker.scoped(|checker| checker.check_equality(c, &r))? {
329                                return None;
330                            }
331                        } else {
332                            curr = Some(r);
333                        }
334                        Some(true)
335                    })? {
336                        return None;
337                    }
338                }
339                curr?
340            }
341        };
342        let seqtp = match seqtp.as_sequence_type() {
343            Some(SequenceType::SeqType(t, _)) => t.clone(),
344            Some(SequenceType::Map(seq, f)) => {
345                let nat = checker.rules().marker().iter().rev().find_map(|rl| {
346                    rl.as_any().downcast_ref::<NumberRule>().and_then(|rl| {
347                        if rl.typ == NumberType::Naturals {
348                            Some(rl.sym.clone())
349                        } else {
350                            None
351                        }
352                    })
353                })?;
354                let vname = Variable::Name {
355                    name: unsafe { "index".parse().unwrap_unchecked() },
356                    notated: None,
357                };
358                let nv = ComponentVar {
359                    var: vname.clone(),
360                    tp: Some(nat.into()),
361                    df: None,
362                };
363                checker.extend_context(nv);
364                let arg = Term::Application(ApplicationTerm::new(
365                    seq.to_term(),
366                    Box::new([Argument::Simple(vname.into())]),
367                    None,
368                ));
369                Term::Application(ApplicationTerm::new(
370                    f.clone(),
371                    Box::new([Argument::Simple(arg)]),
372                    None,
373                ))
374            }
375            Some(_) => {
376                let nat = checker.rules().marker().iter().rev().find_map(|rl| {
377                    rl.as_any().downcast_ref::<NumberRule>().and_then(|rl| {
378                        if rl.typ == NumberType::Naturals {
379                            Some(rl.sym.clone())
380                        } else {
381                            None
382                        }
383                    })
384                })?;
385                let vname = Variable::Name {
386                    name: unsafe { "index".parse().unwrap_unchecked() },
387                    notated: None,
388                };
389                let nv = ComponentVar {
390                    var: vname.clone(),
391                    tp: Some(nat.into()),
392                    df: None,
393                };
394                checker.extend_context(nv);
395                Term::Application(ApplicationTerm::new(
396                    seqtp,
397                    Box::new([Argument::Simple(vname.into())]),
398                    None,
399                ))
400            }
401            _ => seqtp,
402        };
403        let (v, _) = f.fresh_variable(&crate::DUMMY, None);
404        checker.extend_context(ComponentVar {
405            var: v.clone(),
406            tp: Some(seqtp),
407            df: None,
408        });
409        let nt = Term::Application(ApplicationTerm::new(
410            f.clone(),
411            Box::new([Argument::Simple(Term::Var {
412                variable: v,
413                presentation: None,
414            })]),
415            None,
416        ));
417        checker.scoped(|checker| checker.check_inhabitable(&nt))
418    }
419}
420
421#[derive(Debug, Clone, PartialEq, Eq)]
422pub struct MapInferenceRule(pub SymbolUri);
423impl SizedSolverRule for MapInferenceRule {
424    fn display(&self) -> Vec<crate::trace::Displayable> {
425        ftml_solver_trace::trace!("{ x:A, f(x):T, s:A* } ⊢ ", &self.0, "(s,f): T*")
426    }
427}
428
429impl<Split: SplitStrategy> InferenceRule<Split> for MapInferenceRule {
430    fn applicable(&self, term: &ftml_ontology::terms::Term) -> bool {
431        if let Term::Application(app) = term
432            && let Term::Symbol { uri, .. } = &app.head
433        {
434            *uri == self.0 && app.arguments.len() == 2
435        } else {
436            false
437        }
438    }
439    fn infer<'t>(
440        &self,
441        mut checker: crate::CheckRef<'t, '_, Split>,
442        term: &'t Term,
443    ) -> Option<Term> {
444        let Term::Application(app) = term else {
445            return None;
446        };
447        let [Argument::Sequence(seq), Argument::Simple(f)] = &*app.arguments else {
448            checker.failure("arguments don't match");
449            return None;
450        };
451        let seqtp = match seq {
452            MaybeSequence::One(t)
453                if matches!(t.as_sequence(), Some(Sequence::SequenceExpression(_))) =>
454            {
455                // SAFETY: pattern match
456                let Some(Sequence::SequenceExpression(args)) = t.as_sequence() else {
457                    unsafe { unreachable_unchecked() }
458                };
459                let mut curr = None;
460                for t in args {
461                    if !checker.scoped::<Option<bool>>(|checker| {
462                        let r = checker.infer_type(t)?;
463                        if let Some(c) = &curr {
464                            if !checker.scoped(|checker| checker.check_equality(c, &r))? {
465                                return None;
466                            }
467                        } else {
468                            curr = Some(r);
469                        }
470                        Some(true)
471                    })? {
472                        return None;
473                    }
474                }
475                curr?
476            }
477            MaybeSequence::One(t) => checker.infer_type(t)?,
478            MaybeSequence::Seq(ts) => {
479                let mut curr = None;
480                for t in ts {
481                    if !checker.scoped::<Option<bool>>(|checker| {
482                        let r = checker.infer_type(t)?;
483                        if let Some(c) = &curr {
484                            if !checker.scoped(|checker| checker.check_equality(c, &r))? {
485                                return None;
486                            }
487                        } else {
488                            curr = Some(r);
489                        }
490                        Some(true)
491                    })? {
492                        return None;
493                    }
494                }
495                curr?
496            }
497        };
498        let seqtp = match seqtp.as_sequence_type() {
499            Some(SequenceType::SeqType(t, _)) => t.clone(),
500            Some(SequenceType::Map(seq, f)) => {
501                let nat = checker.rules().marker().iter().rev().find_map(|rl| {
502                    rl.as_any().downcast_ref::<NumberRule>().and_then(|rl| {
503                        if rl.typ == NumberType::Naturals {
504                            Some(rl.sym.clone())
505                        } else {
506                            None
507                        }
508                    })
509                })?;
510                let vname = Variable::Name {
511                    name: unsafe { "index".parse().unwrap_unchecked() },
512                    notated: None,
513                };
514                let nv = ComponentVar {
515                    var: vname.clone(),
516                    tp: Some(nat.into()),
517                    df: None,
518                };
519                checker.extend_context(nv);
520                let arg = Term::Application(ApplicationTerm::new(
521                    seq.to_term(),
522                    Box::new([Argument::Simple(vname.into())]),
523                    None,
524                ));
525                Term::Application(ApplicationTerm::new(
526                    f.clone(),
527                    Box::new([Argument::Simple(arg)]),
528                    None,
529                ))
530            }
531            Some(_) => {
532                let nat = checker.rules().marker().iter().rev().find_map(|rl| {
533                    rl.as_any().downcast_ref::<NumberRule>().and_then(|rl| {
534                        if rl.typ == NumberType::Naturals {
535                            Some(rl.sym.clone())
536                        } else {
537                            None
538                        }
539                    })
540                })?;
541                let vname = Variable::Name {
542                    name: unsafe { "index".parse().unwrap_unchecked() },
543                    notated: None,
544                };
545                let nv = ComponentVar {
546                    var: vname.clone(),
547                    tp: Some(nat.into()),
548                    df: None,
549                };
550                checker.extend_context(nv);
551                Term::Application(ApplicationTerm::new(
552                    seqtp,
553                    Box::new([Argument::Simple(vname.into())]),
554                    None,
555                ))
556            }
557            _ => seqtp,
558        };
559        let (v, _) = f.fresh_variable(&crate::DUMMY, None);
560        checker.extend_context(ComponentVar {
561            var: v.clone(),
562            tp: Some(seqtp),
563            df: None,
564        });
565        let nt = Term::Application(ApplicationTerm::new(
566            f.clone(),
567            Box::new([Argument::Simple(Term::Var {
568                variable: v,
569                presentation: None,
570            })]),
571            None,
572        ));
573        checker
574            .scoped(|checker| checker.infer_type(&nt))
575            .map(Term::into_seq_type)
576    }
577}
ftml_solver/rules/sequences/map.rs

ftml_solver/rules/sequences/
map.rs
