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        let r = self.wrap_check(CheckingTask::Inference(t), |slf| slf.infer_type_i(t));
12        if let Some(r) = &r {
13            tracing::debug!("Inferred: {:?}", r.debug_short());
14        } else {
15            tracing::debug!("Inferrence failed");
16        }
17        r
18    }
19    pub(crate) fn infer_type_i(&mut self, t: &'t Term) -> Option<Term> {
20        match t {
21            Term::Symbol { uri, .. } => {
22                self.comment("Looking up symbol");
23                let ret = self.get_symbol_type(uri);
24
25                if ret.is_none() {
26                    self.failure("Symbol has no type");
27                }
28                return ret;
29            }
30            Term::Var { variable, .. } => {
31                return self.infer_var_type_i(variable);
32            }
33            _ => (),
34        }
35        self.simplify_rules(
36            self.top.rules.inference(),
37            t,
38            InferenceRule::applicable,
39            |slf, rl, t| rl.infer(slf, t),
40        )
41        /*
42        let rules = self
43            .top
44            .rules
45            .inference()
46            .iter()
47            .filter_map(|rl| if rl.applicable(t) { Some(&**rl) } else { None })
48            .collect::<smallvec::SmallVec<_, 2>>();
49        let r = Split::split(self, true, rules, |slf, rl| rl.infer(slf, t));
50        r.map(|t| self.subst(t))
51        */
52        /*r.map(|t| {
53            let simp = self.scoped(|slf| slf.simplify_full(false, &t)).unwrap_or(t);
54            self.subst(simp)
55        })*/
56    }
57
58    pub fn infer_var_type(&mut self, var: &'t Variable) -> Option<Term> {
59        self.wrap_check(CheckingTask::VariableInference(var.name()), |slf| {
60            slf.infer_var_type_i(var)
61        })
62    }
63    pub(crate) fn infer_var_type_i(&mut self, var: &Variable) -> Option<Term> {
64        if let Some(id) = is_solvable_var(var) {
65            return Some(self.get_solvable_type(id));
66        }
67        let (ctx, mut msgs) = self.split();
68        for v in ctx.iter().rev().map(|v| &**v) {
69            match (v, var) {
70                (
71                    ComponentVar {
72                        var: Variable::Name { name, .. },
73                        tp,
74                        ..
75                    },
76                    Variable::Name { name: n2, .. },
77                ) if *name == *n2 => {
78                    if tp.is_some() {
79                        msgs.comment("Found type in context");
80                    } else {
81                        msgs.failure("variable untyped in context");
82                    }
83                    return tp.clone().map(|t| self.subst(t));
84                }
85                (
86                    ComponentVar {
87                        var: Variable::Name { name, .. },
88                        tp,
89                        ..
90                    },
91                    Variable::Ref { declaration, .. },
92                ) if name.as_ref() == declaration.name().last() && tp.is_some() => {
93                    if tp.is_some() {
94                        msgs.comment("Found type in context");
95                    } else {
96                        msgs.failure("Variable untyped in context");
97                    }
98                    return tp.clone().map(|t| self.subst(t));
99                }
100                (
101                    ComponentVar {
102                        var: Variable::Ref { declaration, .. },
103                        tp,
104                        ..
105                    },
106                    Variable::Name { name, .. },
107                ) if name.as_ref() == declaration.name().last() => {
108                    return if tp.is_some() {
109                        msgs.comment("Found type in context");
110                        tp.clone().map(|t| self.subst(t))
111                    } else {
112                        msgs.comment("Getting variable globally");
113                        let declaration = declaration.clone();
114                        let var = self.get_variable(&declaration).ok()?;
115                        var.data.tp.checked_or_parsed().map(|(t, _)| {
116                            if var.data.is_seq && t.as_sequence_type().is_none() {
117                                t.into_seq_type()
118                            } else {
119                                t
120                            }
121                        })
122                    };
123                }
124                (
125                    ComponentVar {
126                        var: Variable::Ref { declaration, .. },
127                        tp,
128                        ..
129                    },
130                    Variable::Ref {
131                        declaration: d2, ..
132                    },
133                ) if *declaration == *d2 => {
134                    return if tp.is_some() {
135                        msgs.comment("Found type in context");
136                        tp.clone().map(|t| self.subst(t))
137                    } else {
138                        msgs.comment("Getting variable globally");
139                        let declaration = declaration.clone();
140                        let var = self.get_variable(&declaration).ok()?;
141                        var.data.tp.checked_or_parsed().map(|(t, _)| {
142                            if var.data.is_seq && t.as_sequence_type().is_none() {
143                                t.into_seq_type()
144                            } else {
145                                t
146                            }
147                        })
148                    };
149                }
150                _ => (),
151            }
152        }
153        if let Variable::Ref { declaration, .. } = var {
154            self.comment("Getting variable globally");
155            let var = self.get_variable(declaration).ok()?;
156            var.data.tp.checked_or_parsed().map(|(t, _)| {
157                if var.data.is_seq && t.as_sequence_type().is_none() {
158                    t.into_seq_type()
159                } else {
160                    t
161                }
162            })
163        } else {
164            Some(self.new_solvable())
165        }
166    }
167}
ftml_solver/impls/inference.rs

ftml_solver/impls/
inference.rs
