ftml_solver/rules/operators/
intersection.rs

1use ftml_ontology::terms::{Argument, BoundArgument, MaybeSequence, Term};
2use ftml_solver_trace::SizedSolverRule;
3use ftml_uris::SymbolUri;
4
5use crate::{
6    CheckRef,
7    rules::{InhabitableRule, MarkerRule, UniverseRule, operators::pi::PiExtensionRule},
8    split::SplitStrategy,
9};
10
11#[derive(Debug, Clone, PartialEq, Eq)]
12pub struct IntersectionTypeInhabitable(pub SymbolUri);
13impl SizedSolverRule for IntersectionTypeInhabitable {
14    fn display(&self) -> Vec<crate::trace::Displayable> {
15        ftml_solver_trace::trace!("intersection types inherit inhabitability and universality")
16    }
17}
18impl<Split: SplitStrategy> InhabitableRule<Split> for IntersectionTypeInhabitable {
19    fn applicable(&self, term: &Term) -> bool {
20        if let Term::Application(app) = term
21            && let Term::Symbol { uri, .. } = &app.head
22            && *uri == self.0
23            && let [Argument::Sequence(_)] = &*app.arguments
24        {
25            true
26        } else {
27            false
28        }
29    }
30    fn apply<'t>(&self, mut checker: CheckRef<'t, '_, Split>, term: &'t Term) -> Option<bool> {
31        let Term::Application(app) = term else {
32            return None;
33        };
34        let [Argument::Sequence(MaybeSequence::Seq(tps))] = &*app.arguments else {
35            return None;
36        };
37        for t in tps {
38            if !checker.check_inhabitable(t)? {
39                return None;
40            }
41        }
42        Some(true)
43    }
44}
45impl<Split: SplitStrategy> UniverseRule<Split> for IntersectionTypeInhabitable {
46    fn applicable(&self, term: &Term) -> bool {
47        <Self as InhabitableRule<Split>>::applicable(&self, term)
48    }
49    fn apply<'t>(&self, mut checker: CheckRef<'t, '_, Split>, term: &'t Term) -> Option<bool> {
50        let Term::Application(app) = term else {
51            return None;
52        };
53        let [Argument::Sequence(MaybeSequence::Seq(tps))] = &*app.arguments else {
54            return None;
55        };
56        for t in tps {
57            if !checker.check_universe(t)? {
58                return None;
59            }
60        }
61        Some(true)
62    }
63}
64
65pub fn intersect_pi_extension<Split: SplitStrategy>(
66    intersect: SymbolUri,
67    pi: SymbolUri,
68) -> super::pi::PiExtensionRule<Split> {
69    super::pi::PiExtensionRule {
70        extension: intersect,
71        pi,
72        applicable: |slf, tp, _| {
73            if let Term::Application(app) = tp
74                && let Term::Symbol { uri, .. } = &app.head
75                && *uri == slf.extension
76                && let [Argument::Sequence(MaybeSequence::Seq(tps))] = &*app.arguments
77            {
78                tps.iter().all(|t| {
79                    if let Term::Bound(b) = t {
80                        matches!(&b.head,Term::Symbol { uri, .. } if *uri == slf.pi)
81                            && b.arguments.len() == 2
82                            && matches!(&b.arguments[1], BoundArgument::Simple(_))
83                    } else {
84                        false
85                    }
86                })
87            } else {
88                false
89            }
90        },
91        infer: |slf, pi, checker, tp, args, index| {
92            let Argument::Simple(arg) = &args[*index] else {
93                return None;
94            };
95            let Term::Application(app) = tp else {
96                return None;
97            };
98            let [Argument::Sequence(MaybeSequence::Seq(tps))] = &*app.arguments else {
99                return None;
100            };
101            for tp in tps {
102                let Ok(b) = super::pi::PiInferenceRule::deconstruct_tp(&pi.0, checker, tp.clone())
103                else {
104                    continue;
105                };
106                let [_, BoundArgument::Simple(body)] = &*b.arguments else {
107                    // SAFETY: invariant of deconstruct_tp
108                    unsafe { std::hint::unreachable_unchecked() }
109                };
110                if let Some(r) = super::pi::PiInferenceRule::simple_apply(checker, &b, arg, body) {
111                    *index += 1;
112                    return Some(r);
113                }
114            }
115            None
116        },
117    }
118}
ftml_solver/rules/operators/intersection.rs

ftml_solver/rules/operators/
intersection.rs
