ftml_solver/impls/
inference.rs

1use ftml_ontology::terms::{ComponentVar, Term, Variable};
2
3use crate::{
4    CheckRef, impls::solving::is_solvable_var, rules::InferenceRule, split::SplitStrategy,
5    trace::CheckingTask,
6};
7
8impl<'t, Split: SplitStrategy> CheckRef<'t, '_, Split> {
9    pub fn infer_type(&mut self, t: &'t Term) -> Option<Term> {
10        tracing::debug!("Inferring type of {:?}", t.debug_short());
11        //crate::pause();
12        let r = self.wrap_check(CheckingTask::Inference(t), |slf| slf.infer_type_i(t));
13        if let Some(r) = &r {
14            tracing::debug!("Inferred: {:?}", r.debug_short());
15        } else {
16            tracing::debug!("Inferrence failed");
17        }
18        r
19    }
20    pub(crate) fn infer_type_i(&mut self, t: &'t Term) -> Option<Term> {
21        match t {
22            Term::Symbol { uri, .. } => {
23                self.comment("Looking up symbol");
24                let ret = self.get_symbol_type(uri);
25
26                if ret.is_none() {
27                    self.failure("Symbol has no type");
28                }
29                return ret;
30            }
31            Term::Var { variable, .. } => {
32                return self.infer_var_type_i(variable);
33            }
34            _ => (),
35        }
36        self.simplify_rules(
37            self.top.rules.inference(),
38            t,
39            InferenceRule::applicable,
40            |slf, rl, t| rl.infer(slf, t),
41        )
42        /*
43        let rules = self
44            .top
45            .rules
46            .inference()
47            .iter()
48            .filter_map(|rl| if rl.applicable(t) { Some(&**rl) } else { None })
49            .collect::<smallvec::SmallVec<_, 2>>();
50        let r = Split::split(self, true, rules, |slf, rl| rl.infer(slf, t));
51        r.map(|t| self.subst(t))
52        */
53        /*r.map(|t| {
54            let simp = self.scoped(|slf| slf.simplify_full(false, &t)).unwrap_or(t);
55            self.subst(simp)
56        })*/
57    }
58
59    pub fn infer_var_type(&mut self, var: &'t Variable) -> Option<Term> {
60        self.wrap_check(CheckingTask::VariableInference(var.name()), |slf| {
61            slf.infer_var_type_i(var)
62        })
63    }
64    pub(crate) fn infer_var_type_i(&mut self, var: &Variable) -> Option<Term> {
65        if let Some(id) = is_solvable_var(var) {
66            return Some(self.get_solvable_type(id));
67        }
68        let (ctx, mut msgs) = self.split();
69
70        for v in ctx.iter().rev().map(|v| &**v) {
71            match (v, var) {
72                (ComponentVar { var: v, tp, .. }, var) if v.name() == var.name() => {
73                    if tp.is_some() {
74                        msgs.comment("Found type in context");
75                    } else if let Variable::Ref { declaration, .. } = v {
76                        msgs.comment("Getting variable globally");
77                        let declaration = declaration.clone();
78                        let var = self.get_variable(&declaration).ok()?;
79                        return var.data.tp.checked_or_parsed().map(|(t, _)| {
80                            if var.data.is_seq && t.as_sequence_type().is_none() {
81                                t.into_seq_type()
82                            } else {
83                                t
84                            }
85                        });
86                    } else {
87                        msgs.failure("variable untyped in context");
88                    }
89                    return tp.clone().map(|t| self.subst(t));
90                }
91                _ => (),
92            }
93        }
94        if let Variable::Ref { declaration, .. } = var {
95            self.comment("Getting variable globally");
96            let var = self.get_variable(declaration).ok()?;
97            var.data.tp.checked_or_parsed().map(|(t, _)| {
98                if var.data.is_seq && t.as_sequence_type().is_none() {
99                    t.into_seq_type()
100                } else {
101                    t
102                }
103            })
104        } else {
105            Some(self.new_solvable())
106        }
107    }
108}
ftml_solver/impls/inference.rs

ftml_solver/impls/
inference.rs
