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| checker.simplify_full(false, &t))
204                            .unwrap_or(t)
205                    })
206                    .collect())
207            }
208            Argument::Sequence(MaybeSequence::Seq(ts)) => Ok(ts
209                .iter()
210                .map(|arg| {
211                    let t = Term::Application(ApplicationTerm::new(
212                        f.clone(),
213                        Box::new([Argument::Simple(arg.clone())]),
214                        None,
215                    ));
216                    checker
217                        .scoped(|checker| checker.simplify_full(false, &t))
218                        .unwrap_or(t)
219                })
220                .collect()),
221        }
222    }
223    fn applicable_i(sym: &SymbolUri, term: &Term) -> bool {
224        if let Term::Application(app) = term
225            && let Term::Symbol { uri, .. } = &app.head
226            && *uri == *sym
227            && let [a, Argument::Simple(_)] = &*app.arguments
228        {
229            if let Argument::Simple(s) | Argument::Sequence(MaybeSequence::One(s)) = a {
230                s.as_sequence().is_some_and(|seq| seq.is_concrete())
231            } else {
232                true
233            }
234        } else {
235            false
236        }
237    }
238}
239impl<Split: SplitStrategy> SimplificationRule<Split> for MapSimplificationRule {
240    fn applicable(&self, term: &Term) -> bool {
241        Self::applicable_i(&self.0, term)
242    }
243    fn apply<'t>(
244        &self,
245        mut checker: crate::CheckRef<'t, '_, Split>,
246        term: &'t Term,
247    ) -> Result<Term, Option<ftml_ontology::terms::termpaths::TermPath>> {
248        Self::apply_i::<Split>(&mut checker, term).map(|ts| Term::into_seq(ts.into_iter()))
249    }
250}
251
252#[derive(Debug, Clone, PartialEq, Eq)]
253pub struct MapInhabitableRule(pub SymbolUri);
254impl SizedSolverRule for MapInhabitableRule {
255    fn display(&self) -> Vec<crate::trace::Displayable> {
256        ftml_solver_trace::trace!("{ x:A, INH f(x), s:A* } ⊢ INH ", &self.0, "(s,f)")
257    }
258}
259
260impl<Split: SplitStrategy> InhabitableRule<Split> for MapInhabitableRule {
261    fn applicable(&self, term: &ftml_ontology::terms::Term) -> bool {
262        if let Term::Application(app) = term
263            && let Term::Symbol { uri, .. } = &app.head
264        {
265            *uri == self.0 && app.arguments.len() == 2
266        } else {
267            false
268        }
269    }
270    fn apply<'t>(
271        &self,
272        mut checker: crate::CheckRef<'t, '_, Split>,
273        term: &'t ftml_ontology::terms::Term,
274    ) -> Option<bool> {
275        let Term::Application(app) = term else {
276            return None;
277        };
278        let [Argument::Sequence(seq), Argument::Simple(f)] = &*app.arguments else {
279            checker.failure("arguments don't match");
280            return None;
281        };
282        let seqtp = match seq {
283            MaybeSequence::One(t)
284                if matches!(t.as_sequence(), Some(Sequence::SequenceExpression(_))) =>
285            {
286                // SAFETY: pattern match
287                let Some(Sequence::SequenceExpression(args)) = t.as_sequence() else {
288                    unsafe { unreachable_unchecked() }
289                };
290                let mut curr = None;
291                for t in args {
292                    if !checker.scoped::<Option<bool>>(|checker| {
293                        let r = checker.infer_type(t)?;
294                        if let Some(c) = &curr {
295                            if !checker.scoped(|checker| checker.check_equality(c, &r))? {
296                                return None;
297                            }
298                        } else {
299                            curr = Some(r);
300                        }
301                        Some(true)
302                    })? {
303                        return None;
304                    }
305                }
306                curr?
307            }
308            MaybeSequence::One(t) => checker.infer_type(t)?,
309            MaybeSequence::Seq(ts) => {
310                let mut curr = None;
311                for t in ts {
312                    if !checker.scoped::<Option<bool>>(|checker| {
313                        let r = checker.infer_type(t)?;
314                        if let Some(c) = &curr {
315                            if !checker.scoped(|checker| checker.check_equality(c, &r))? {
316                                return None;
317                            }
318                        } else {
319                            curr = Some(r);
320                        }
321                        Some(true)
322                    })? {
323                        return None;
324                    }
325                }
326                curr?
327            }
328        };
329        let seqtp = match seqtp.as_sequence_type() {
330            Some(SequenceType::SeqType(t, _)) => t.clone(),
331            Some(SequenceType::Map(seq, f)) => {
332                let nat = checker.rules().marker().iter().rev().find_map(|rl| {
333                    rl.as_any().downcast_ref::<NumberRule>().and_then(|rl| {
334                        if rl.typ == NumberType::Naturals {
335                            Some(rl.sym.clone())
336                        } else {
337                            None
338                        }
339                    })
340                })?;
341                let vname = Variable::Name {
342                    name: unsafe { "index".parse().unwrap_unchecked() },
343                    notated: None,
344                };
345                let nv = ComponentVar {
346                    var: vname.clone(),
347                    tp: Some(nat.into()),
348                    df: None,
349                };
350                checker.extend_context(nv);
351                let arg = Term::Application(ApplicationTerm::new(
352                    seq.to_term(),
353                    Box::new([Argument::Simple(vname.into())]),
354                    None,
355                ));
356                Term::Application(ApplicationTerm::new(
357                    f.clone(),
358                    Box::new([Argument::Simple(arg)]),
359                    None,
360                ))
361            }
362            Some(_) => {
363                let nat = checker.rules().marker().iter().rev().find_map(|rl| {
364                    rl.as_any().downcast_ref::<NumberRule>().and_then(|rl| {
365                        if rl.typ == NumberType::Naturals {
366                            Some(rl.sym.clone())
367                        } else {
368                            None
369                        }
370                    })
371                })?;
372                let vname = Variable::Name {
373                    name: unsafe { "index".parse().unwrap_unchecked() },
374                    notated: None,
375                };
376                let nv = ComponentVar {
377                    var: vname.clone(),
378                    tp: Some(nat.into()),
379                    df: None,
380                };
381                checker.extend_context(nv);
382                Term::Application(ApplicationTerm::new(
383                    seqtp,
384                    Box::new([Argument::Simple(vname.into())]),
385                    None,
386                ))
387            }
388            _ => seqtp,
389        };
390        let (v, _) = f.fresh_variable(&crate::DUMMY, None);
391        checker.extend_context(ComponentVar {
392            var: v.clone(),
393            tp: Some(seqtp),
394            df: None,
395        });
396        let nt = Term::Application(ApplicationTerm::new(
397            f.clone(),
398            Box::new([Argument::Simple(Term::Var {
399                variable: v,
400                presentation: None,
401            })]),
402            None,
403        ));
404        checker.scoped(|checker| checker.check_inhabitable(&nt))
405    }
406}
407
408#[derive(Debug, Clone, PartialEq, Eq)]
409pub struct MapInferenceRule(pub SymbolUri);
410impl SizedSolverRule for MapInferenceRule {
411    fn display(&self) -> Vec<crate::trace::Displayable> {
412        ftml_solver_trace::trace!("{ x:A, f(x):T, s:A* } ⊢ ", &self.0, "(s,f): T*")
413    }
414}
415
416impl<Split: SplitStrategy> InferenceRule<Split> for MapInferenceRule {
417    fn applicable(&self, term: &ftml_ontology::terms::Term) -> bool {
418        if let Term::Application(app) = term
419            && let Term::Symbol { uri, .. } = &app.head
420        {
421            *uri == self.0 && app.arguments.len() == 2
422        } else {
423            false
424        }
425    }
426    fn infer<'t>(
427        &self,
428        mut checker: crate::CheckRef<'t, '_, Split>,
429        term: &'t Term,
430    ) -> Option<Term> {
431        let Term::Application(app) = term else {
432            return None;
433        };
434        let [Argument::Sequence(seq), Argument::Simple(f)] = &*app.arguments else {
435            checker.failure("arguments don't match");
436            return None;
437        };
438        let seqtp = match seq {
439            MaybeSequence::One(t)
440                if matches!(t.as_sequence(), Some(Sequence::SequenceExpression(_))) =>
441            {
442                // SAFETY: pattern match
443                let Some(Sequence::SequenceExpression(args)) = t.as_sequence() else {
444                    unsafe { unreachable_unchecked() }
445                };
446                let mut curr = None;
447                for t in args {
448                    if !checker.scoped::<Option<bool>>(|checker| {
449                        let r = checker.infer_type(t)?;
450                        if let Some(c) = &curr {
451                            if !checker.scoped(|checker| checker.check_equality(c, &r))? {
452                                return None;
453                            }
454                        } else {
455                            curr = Some(r);
456                        }
457                        Some(true)
458                    })? {
459                        return None;
460                    }
461                }
462                curr?
463            }
464            MaybeSequence::One(t) => checker.infer_type(t)?,
465            MaybeSequence::Seq(ts) => {
466                let mut curr = None;
467                for t in ts {
468                    if !checker.scoped::<Option<bool>>(|checker| {
469                        let r = checker.infer_type(t)?;
470                        if let Some(c) = &curr {
471                            if !checker.scoped(|checker| checker.check_equality(c, &r))? {
472                                return None;
473                            }
474                        } else {
475                            curr = Some(r);
476                        }
477                        Some(true)
478                    })? {
479                        return None;
480                    }
481                }
482                curr?
483            }
484        };
485        let seqtp = match seqtp.as_sequence_type() {
486            Some(SequenceType::SeqType(t, _)) => t.clone(),
487            Some(SequenceType::Map(seq, f)) => {
488                let nat = checker.rules().marker().iter().rev().find_map(|rl| {
489                    rl.as_any().downcast_ref::<NumberRule>().and_then(|rl| {
490                        if rl.typ == NumberType::Naturals {
491                            Some(rl.sym.clone())
492                        } else {
493                            None
494                        }
495                    })
496                })?;
497                let vname = Variable::Name {
498                    name: unsafe { "index".parse().unwrap_unchecked() },
499                    notated: None,
500                };
501                let nv = ComponentVar {
502                    var: vname.clone(),
503                    tp: Some(nat.into()),
504                    df: None,
505                };
506                checker.extend_context(nv);
507                let arg = Term::Application(ApplicationTerm::new(
508                    seq.to_term(),
509                    Box::new([Argument::Simple(vname.into())]),
510                    None,
511                ));
512                Term::Application(ApplicationTerm::new(
513                    f.clone(),
514                    Box::new([Argument::Simple(arg)]),
515                    None,
516                ))
517            }
518            Some(_) => {
519                let nat = checker.rules().marker().iter().rev().find_map(|rl| {
520                    rl.as_any().downcast_ref::<NumberRule>().and_then(|rl| {
521                        if rl.typ == NumberType::Naturals {
522                            Some(rl.sym.clone())
523                        } else {
524                            None
525                        }
526                    })
527                })?;
528                let vname = Variable::Name {
529                    name: unsafe { "index".parse().unwrap_unchecked() },
530                    notated: None,
531                };
532                let nv = ComponentVar {
533                    var: vname.clone(),
534                    tp: Some(nat.into()),
535                    df: None,
536                };
537                checker.extend_context(nv);
538                Term::Application(ApplicationTerm::new(
539                    seqtp,
540                    Box::new([Argument::Simple(vname.into())]),
541                    None,
542                ))
543            }
544            _ => seqtp,
545        };
546        let (v, _) = f.fresh_variable(&crate::DUMMY, None);
547        checker.extend_context(ComponentVar {
548            var: v.clone(),
549            tp: Some(seqtp),
550            df: None,
551        });
552        let nt = Term::Application(ApplicationTerm::new(
553            f.clone(),
554            Box::new([Argument::Simple(Term::Var {
555                variable: v,
556                presentation: None,
557            })]),
558            None,
559        ));
560        checker
561            .scoped(|checker| checker.infer_type(&nt))
562            .map(Term::into_seq_type)
563    }
564}
ftml_solver/rules/sequences/map.rs

ftml_solver/rules/sequences/
map.rs
