ftml_solver/rules/operators/
universe.rs

1use crate::{
2    CheckRef,
3    impls::solving::TermExtSolvable,
4    rules::{
5        CheckingRule, InhabitableRule, MarkerRule, SizedSolverRule, SubtypeRule, UniverseRule,
6    },
7    split::SplitStrategy,
8};
9use ftml_ontology::terms::{Argument, Term, patterns::Pattern};
10use ftml_uris::SymbolUri;
11
12#[derive(Debug, Clone, PartialEq, Eq)]
13pub struct SimpleInhabitableRule(pub SymbolUri, pub u8);
14impl SizedSolverRule for SimpleInhabitableRule {
15    fn display(&self) -> Vec<crate::trace::Displayable> {
16        ftml_solver_trace::trace!(&self.0, " is inhabitable")
17    }
18}
19impl<Split: SplitStrategy> InhabitableRule<Split> for SimpleInhabitableRule {
20    fn applicable(&self, term: &Term) -> bool {
21        if self.1 == 0 {
22            //ftml_ontology::matchtm!(sym(= &self.0) = term)
23            matches!(term,Term::Symbol { uri, .. } if *uri == self.0)
24        } else {
25            /*ftml_ontology::matchtm!(app({sym(=self.0)},[args]) = term
26                => { args.len() == self.1 as usize} else {false}
27            )*/
28            matches!(term,Term::Application(a)
29                if matches!(&a.head,Term::Symbol { uri, .. } if *uri == self.0)
30                && a.arguments.len() == self.1 as usize
31            )
32        }
33    }
34    fn apply<'t>(&self, mut checker: CheckRef<'t, '_, Split>, t: &'t Term) -> Option<bool> {
35        if self.1 == 0 {
36            return Some(true);
37        }
38        let Term::Application(a) = t else { return None };
39        for (i, arg) in a.arguments.iter().enumerate() {
40            checker.comment(format!("Checking argument {}", i + 1));
41            match arg {
42                Argument::Simple(t) => {
43                    if !checker.check_inhabitable(t)? {
44                        return Some(false);
45                    }
46                }
47                Argument::Sequence(_) => return None,
48            }
49        }
50        Some(true)
51    }
52}
53
54#[derive(Debug, Clone, PartialEq, Eq)]
55pub struct ComplexInhabitableRule(pub Pattern);
56impl SizedSolverRule for ComplexInhabitableRule {
57    fn display(&self) -> Vec<crate::trace::Displayable> {
58        ftml_solver_trace::trace!(self.0.body.clone(), "is inhabitable")
59    }
60}
61impl<Split: SplitStrategy> InhabitableRule<Split> for ComplexInhabitableRule {
62    fn applicable(&self, term: &Term) -> bool {
63        self.0.matches(term).is_some()
64    }
65    fn apply<'t>(&self, mut checker: CheckRef<'t, '_, Split>, t: &'t Term) -> Option<bool> {
66        // To be sure:
67        checker.infer_type(t)?;
68        Some(true)
69    }
70}
71
72#[derive(Debug, Clone, PartialEq, Eq)]
73pub struct SimpleUniverseRule(pub SymbolUri);
74
75impl SizedSolverRule for SimpleUniverseRule {
76    fn display(&self) -> Vec<crate::trace::Displayable> {
77        ftml_solver_trace::trace!(&self.0, " is a universe")
78    }
79}
80impl std::fmt::Display for SimpleUniverseRule {
81    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
82        write!(f, "{} is a universe", self.0)
83    }
84}
85impl<Split: SplitStrategy> InhabitableRule<Split> for SimpleUniverseRule {
86    fn applicable(&self, term: &Term) -> bool {
87        matches!(term,Term::Symbol { uri, .. } if *uri == self.0)
88    }
89    fn apply<'t>(&self, _: CheckRef<'t, '_, Split>, _: &'t Term) -> Option<bool> {
90        Some(true)
91    }
92}
93impl<Split: SplitStrategy> UniverseRule<Split> for SimpleUniverseRule {
94    fn applicable(&self, term: &Term) -> bool {
95        matches!(term,Term::Symbol { uri, .. } if *uri == self.0)
96    }
97    fn apply<'t>(&self, _: CheckRef<'t, '_, Split>, _: &'t Term) -> Option<bool> {
98        Some(true)
99    }
100}
101
102#[derive(Debug, Clone, PartialEq, Eq)]
103pub struct ComplexUniverseRule(pub Pattern);
104impl SizedSolverRule for ComplexUniverseRule {
105    fn display(&self) -> Vec<crate::trace::Displayable> {
106        ftml_solver_trace::trace!(self.0.body.clone(), "is a universe")
107    }
108}
109impl<Split: SplitStrategy> InhabitableRule<Split> for ComplexUniverseRule {
110    fn applicable(&self, term: &Term) -> bool {
111        self.0.matches(term).is_some()
112    }
113    fn apply<'t>(&self, mut checker: CheckRef<'t, '_, Split>, t: &'t Term) -> Option<bool> {
114        // To be sure:
115        checker.infer_type(t)?;
116        Some(true)
117    }
118}
119impl<Split: SplitStrategy> UniverseRule<Split> for ComplexUniverseRule {
120    fn applicable(&self, term: &Term) -> bool {
121        self.0.matches(term).is_some()
122    }
123    fn apply<'t>(&self, mut checker: CheckRef<'t, '_, Split>, t: &'t Term) -> Option<bool> {
124        // To be sure:
125        checker.infer_type(t)?;
126        Some(true)
127    }
128}
129
130#[derive(Debug, Clone, PartialEq, Eq)]
131pub struct AnyRule(pub SymbolUri);
132
133impl SizedSolverRule for AnyRule {
134    fn display(&self) -> Vec<crate::trace::Displayable> {
135        ftml_solver_trace::trace!(&self.0, " is any-type")
136    }
137}
138
139impl std::fmt::Display for AnyRule {
140    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
141        write!(f, "{} is any-type", self.0)
142    }
143}
144impl<Split: SplitStrategy> MarkerRule<Split> for AnyRule {}
145impl<Split: SplitStrategy> SubtypeRule<Split> for AnyRule {
146    fn applicable(&self, _: &CheckRef<'_, '_, Split>, _: &Term, sup: &Term) -> bool {
147        matches!(sup,Term::Symbol { uri, .. } if *uri == self.0)
148    }
149    fn apply<'t>(
150        &self,
151        mut checker: CheckRef<'t, '_, Split>,
152        tm: &'t Term,
153        _: &'t Term,
154    ) -> Option<bool> {
155        checker.check_inhabitable(tm)
156    }
157}
158impl<Split: SplitStrategy> CheckingRule<Split> for AnyRule {
159    fn applicable(&self, _: &CheckRef<'_, '_, Split>, _: &Term, tp: &Term) -> bool {
160        matches!(tp,Term::Symbol { uri, .. } if *uri == self.0)
161    }
162    fn apply<'t>(
163        &self,
164        mut checker: CheckRef<'t, '_, Split>,
165        tm: &'t Term,
166        tp: &'t Term,
167    ) -> Option<bool> {
168        if let Some(ntp) = checker.infer_type(tm)
169            && let Some(unk) = ntp.is_solvable()
170        {
171            return checker.solve_upper_bound(unk, tp);
172        }
173        Some(true)
174    }
175}
ftml_solver/rules/operators/universe.rs

ftml_solver/rules/operators/
universe.rs
