ftml_solver/
judgment_cache.rs

1use std::borrow::Cow;
2
3use ftml_ontology::terms::{ComponentVar, Term};
4use ftml_solver_trace::CheckingTask;
5
6use crate::{
7    context::ContextWrap,
8    impls::solving::{Solutions, is_solvable_var},
9};
10
11pub type Judgments<'c> = rustc_hash::FxHashSet<(Vec<ComponentVar>, CachedJudgment)>;
12pub type Simplifications = rustc_hash::FxHashMap<Term, Vec<(Vec<ComponentVar>, Term)>>;
13
14#[derive(Default, Debug)]
15pub struct JudgmentCacheBase<'c> {
16    current: Vec<CheckingTask<'c>>,
17    cached: std::sync::Arc<parking_lot::Mutex<Judgments<'c>>>,
18    simplifications: std::sync::Arc<parking_lot::Mutex<Simplifications>>,
19}
20impl<'c> JudgmentCacheBase<'c> {
21    pub fn make_ref(&mut self) -> JudgmentCache<'c, '_> {
22        JudgmentCache {
23            current: &mut self.current,
24            cached: self.cached.clone(),
25            simplifications: self.simplifications.clone(),
26        }
27    }
28}
29
30#[derive(Debug)]
31pub struct JudgmentCache<'c, 'i> {
32    current: &'i mut Vec<CheckingTask<'c>>,
33    pub(crate) cached: std::sync::Arc<parking_lot::Mutex<Judgments<'c>>>,
34    simplifications: std::sync::Arc<parking_lot::Mutex<Simplifications>>,
35}
36impl<'c> JudgmentCache<'c, '_> {
37    pub fn copied(&mut self) -> JudgmentCache<'c, '_> {
38        JudgmentCache {
39            current: &mut self.current,
40            cached: self.cached.clone(),
41            simplifications: self.simplifications.clone(),
42        }
43    }
44    pub fn new_base(&self) -> JudgmentCacheBase<'c> {
45        JudgmentCacheBase {
46            current: self.current.clone(),
47            cached: self.cached.clone(),
48            simplifications: self.simplifications.clone(),
49        }
50    }
51    pub fn add_simplification(&self, from: &Term, to: &Term, ctx: &[Cow<ComponentVar>]) {
52        return ();
53        let mut vars = from.free_variables();
54
55        let mut nctx = Vec::new();
56        while let Some(v) = vars.pop() {
57            if is_solvable_var(v).is_some() {
58                return;
59            }
60            if let Some(v) = ctx.iter().rev().find(|vd| vd.var.name() == v.name()) {
61                nctx.push(v.clone().into_owned());
62                //vars.push(&v.var);
63                if let Some(tp) = v.tp.as_ref() {
64                    for v in tp.free_variables() {
65                        if !vars.contains(&v) && !nctx.iter().any(|nv| nv.var.name() == v.name()) {
66                            vars.push(v);
67                        }
68                    }
69                }
70                if let Some(df) = v.df.as_ref() {
71                    for v in df.free_variables() {
72                        if !vars.contains(&v) && !nctx.iter().any(|nv| nv.var.name() == v.name()) {
73                            vars.push(v);
74                        }
75                    }
76                }
77            }
78        }
79        nctx.reverse();
80        let mut simps = self.simplifications.lock();
81        match simps.entry(from.clone()) {
82            std::collections::hash_map::Entry::Vacant(v) => {
83                v.insert_entry(vec![(nctx, to.clone())]);
84            }
85            std::collections::hash_map::Entry::Occupied(mut o) => {
86                let o = o.get_mut();
87                o.push((nctx, to.clone()));
88            }
89        }
90    }
91    pub fn get_simplification(&self, from: &Term, ctx: &[Cow<ComponentVar>]) -> Option<Term> {
92        return None;
93        let simps = self.simplifications.lock();
94        simps.get(from).and_then(|v| {
95            v.iter().rev().find_map(|(c, t)| {
96                if c.iter().all(|v| {
97                    ctx.iter()
98                        .rev()
99                        .find(|w| w.var.name() == v.var.name())
100                        .is_some_and(|w| w.tp == v.tp && w.df == v.df)
101                }) {
102                    Some(t.clone())
103                } else {
104                    None
105                }
106            })
107        })
108    }
109
110    pub fn push(&mut self, task: CheckingTask<'c>) {
111        self.current.push(task);
112    }
113    pub fn pop<R: Clone>(
114        &mut self,
115        ret: &Option<R>,
116        ctx: &[Cow<ComponentVar>],
117        solutions: &Solutions,
118    ) -> Option<CheckingTask<'c>> {
119        fn filter_context(
120            ctx: &[Cow<ComponentVar>],
121            task: &CheckingTask,
122        ) -> Option<Vec<ComponentVar>> {
123            let mut vars: Vec<_> = match task {
124                CheckingTask::Equality(a, b)
125                | CheckingTask::HasType(a, b)
126                | CheckingTask::Subtype(a, b) => a
127                    .free_variables()
128                    .into_iter()
129                    .chain(b.free_variables())
130                    .collect(),
131                CheckingTask::Inference(t)
132                | CheckingTask::Inhabitable(t)
133                | CheckingTask::Proving(t)
134                | CheckingTask::Universe(t) => t.free_variables().into_iter().collect(),
135                CheckingTask::Rule(_)
136                | CheckingTask::Simplify(_)
137                | CheckingTask::Strategy(_)
138                | CheckingTask::VariableInference(_) => {
139                    return None;
140                }
141            };
142            let mut ret = Vec::new();
143            while let Some(v) = vars.pop() {
144                if is_solvable_var(v).is_some() {
145                    return None;
146                }
147                if let Some(v) = ctx.iter().find(|vd| vd.var.name() == v.name()) {
148                    ret.push(v.clone().into_owned());
149                    //vars.push(&v.var);
150                    if let Some(tp) = v.tp.as_ref() {
151                        for v in tp.free_variables() {
152                            if is_solvable_var(v).is_some() {
153                                return None;
154                            }
155                            if !vars.contains(&v) && !ret.iter().any(|nv| nv.var.name() == v.name())
156                            {
157                                vars.push(v);
158                            }
159                        }
160                    }
161                    if let Some(df) = v.df.as_ref() {
162                        for v in df.free_variables() {
163                            if is_solvable_var(v).is_some() {
164                                return None;
165                            }
166                            if !vars.contains(&v) && !ret.iter().any(|nv| nv.var.name() == v.name())
167                            {
168                                vars.push(v);
169                            }
170                        }
171                    }
172                }
173            }
174            ret.reverse();
175            Some(ret)
176        }
177        fn has_unsolveds(ctx: &[Cow<ComponentVar>], task: &CheckingTask) -> bool {
178            let vars = match task {
179                CheckingTask::Equality(a, b)
180                | CheckingTask::HasType(a, b)
181                | CheckingTask::Subtype(a, b) => {
182                    either::Left(a.free_variables().into_iter().chain(b.free_variables()))
183                }
184                CheckingTask::Inference(t)
185                | CheckingTask::Inhabitable(t)
186                | CheckingTask::Proving(t)
187                | CheckingTask::Universe(t) => either::Right(t.free_variables().into_iter()),
188                CheckingTask::Rule(_)
189                | CheckingTask::Simplify(_)
190                | CheckingTask::Strategy(_)
191                | CheckingTask::VariableInference(_) => {
192                    return true;
193                }
194            };
195            for v in vars {
196                if is_solvable_var(v).is_some() {
197                    return true;
198                }
199                if let Some(v) = ctx.iter().find(|vd| vd.var.name() == v.name())
200                    && (v
201                        .tp
202                        .as_ref()
203                        .is_some_and(|t| t.has_free_such_that(|v| is_solvable_var(v).is_some()))
204                        || v.df.as_ref().is_some_and(|t| {
205                            t.has_free_such_that(|v| is_solvable_var(v).is_some())
206                        }))
207                {
208                    return true;
209                }
210            }
211            false
212        }
213        let task = self.current.pop()?;
214        //return Some(task);
215        if !solutions.0.is_empty()
216        //|| ret.is_none()
217        //|| has_unsolveds(ctx, &task)
218        /*|| !filter_context(ctx, &task)
219        || {
220            std::mem::size_of::<R>() == std::mem::size_of::<Term>() && {
221                let ot: &Option<Term> = unsafe {
222                    std::ptr::from_ref(ret)
223                        .cast::<Option<Term>>()
224                        .as_ref_unchecked()
225                };
226                ot.as_ref()
227                    .is_some_and(|t| t.has_free_such_that(|v| is_solvable_var(v).is_some()))
228            }
229        } */
230        {
231            return Some(task);
232        }
233
234        let Some(ctx) = filter_context(ctx, &task) else {
235            return Some(task);
236        };
237
238        macro_rules! insert {
239            ($e:expr) => {{
240                let mut store = self.cached.lock();
241                //let ctx = ctx.iter().map(|vd| vd.clone().into_owned()).collect();
242                store.insert((ctx, $e));
243            }};
244        }
245        match task {
246            CheckingTask::Rule(_)
247            | CheckingTask::Strategy(_)
248            | CheckingTask::Simplify(_)
249            | CheckingTask::VariableInference(_) => (),
250            CheckingTask::Inference(t) => {
251                //println!("Here: {:?}\n in context {:?}", t.debug_short(), ctx);
252                //println!("");
253                insert!(CachedJudgment::Inference {
254                    term: t.clone(),
255                    result: mutate(ret),
256                });
257            }
258            CheckingTask::Proving(t) => {
259                insert!(CachedJudgment::Proof {
260                    goal: t.clone(),
261                    result: mutate(ret),
262                });
263            }
264            CheckingTask::Inhabitable(t) => {
265                insert!(CachedJudgment::Inhabitable {
266                    term: t.clone(),
267                    result: mutate(ret),
268                });
269            }
270            CheckingTask::Universe(t) => {
271                insert!(CachedJudgment::Universe {
272                    term: t.clone(),
273                    result: mutate(ret),
274                });
275            }
276            CheckingTask::Equality(lhs, rhs) => {
277                insert!(CachedJudgment::Equal {
278                    lhs: lhs.clone(),
279                    rhs: rhs.clone(),
280                    result: mutate(ret),
281                });
282            }
283            CheckingTask::Subtype(sub, sup) => {
284                insert!(CachedJudgment::Subtype {
285                    sub: sub.clone(),
286                    sup: sup.clone(),
287                    result: mutate(ret),
288                });
289            }
290            CheckingTask::HasType(tm, tp) => {
291                insert!(CachedJudgment::HasType {
292                    tm: tm.clone(),
293                    tp: tp.clone(),
294                    result: mutate(ret),
295                });
296            }
297        }
298        //
299
300        Some(task)
301    }
302
303    pub fn running(&self, task: &CheckingTask<'c>) -> bool {
304        self.current.contains(task)
305    }
306    pub fn has<R: Clone>(&self, task: &CheckingTask, context: &ContextWrap) -> Option<Option<R>> {
307        //return None;
308        let curr = &*self.cached.lock();
309        for c in curr {
310            if let Some(r) = c.1.is(task, context, &c.0) {
311                /*println!(
312                    "Here:\n - Task: {task:?}\n - Context: {context:?}\n - Cached context: {:?}\n - Cached Judgment: {:?}",
313                    c.0, c.1
314                );*/
315                return Some(r);
316            }
317        }
318        None
319    }
320}
321
322#[derive(Debug, Clone, Hash, PartialEq, Eq)]
323pub enum CachedJudgment {
324    Proof {
325        // ctx:SmallVec<Cow<'c, ComponentVar>, { CONTEXT_LEN }>,
326        goal: Term,
327        result: Option<Term>,
328    },
329    Inference {
330        term: Term,
331        result: Option<Term>,
332    },
333    Inhabitable {
334        term: Term,
335        result: Option<bool>,
336    },
337    Universe {
338        term: Term,
339        result: Option<bool>,
340    },
341    Subtype {
342        sub: Term,
343        sup: Term,
344        result: Option<bool>,
345    },
346    HasType {
347        tm: Term,
348        tp: Term,
349        result: Option<bool>,
350    },
351    Equal {
352        lhs: Term,
353        rhs: Term,
354        result: Option<bool>,
355    },
356}
357impl CachedJudgment {
358    pub fn is<R: Clone>(
359        &self,
360        task: &CheckingTask,
361        ctx: &ContextWrap,
362        cached_ctx: &[ComponentVar],
363    ) -> Option<Option<R>> {
364        fn contexts(ctx: &ContextWrap, cached_ctx: &[ComponentVar]) -> bool {
365            cached_ctx.iter().all(|v| {
366                ctx.as_ref()
367                    .iter()
368                    .rev()
369                    .find(|w| w.var.name() == v.var.name())
370                    .is_some_and(|w| w.tp == v.tp && w.df == v.df)
371            })
372        }
373        match (task, self) {
374            (CheckingTask::Proving(t), Self::Proof { goal, result })
375                if goal.alpha_equal(t) && contexts(ctx, cached_ctx) =>
376            {
377                Some(mutate(result))
378            }
379            (CheckingTask::Inference(t), Self::Inference { term, result })
380                if t.alpha_equal(term) && contexts(ctx, cached_ctx) =>
381            {
382                Some(mutate(result))
383            }
384            (CheckingTask::Inhabitable(t), Self::Inhabitable { term, result })
385                if t.alpha_equal(term) && contexts(ctx, cached_ctx) =>
386            {
387                Some(mutate(result))
388            }
389            (CheckingTask::Universe(t), Self::Universe { term, result })
390                if t.alpha_equal(term) && contexts(ctx, cached_ctx) =>
391            {
392                Some(mutate(result))
393            }
394            (CheckingTask::Subtype(asub, asup), Self::Subtype { sub, sup, result })
395                if asub.alpha_equal(sub) && asup.alpha_equal(sup) && contexts(ctx, cached_ctx) =>
396            {
397                Some(mutate(result))
398            }
399            (CheckingTask::HasType(a, b), Self::HasType { tm, tp, result })
400                if a.alpha_equal(tm) && b.alpha_equal(tp) && contexts(ctx, cached_ctx) =>
401            {
402                Some(mutate(result))
403            }
404            (CheckingTask::Equality(l, r), Self::Equal { lhs, rhs, result })
405                if l.alpha_equal(lhs) && r.alpha_equal(rhs) && contexts(ctx, cached_ctx) =>
406            {
407                Some(mutate(result))
408            }
409            _ => None,
410        }
411    }
412}
413
414#[allow(clippy::ref_option)]
415fn mutate<R: Clone, T>(res: &Option<T>) -> Option<R> {
416    assert_eq!(std::mem::size_of::<R>(), std::mem::size_of::<T>());
417    unsafe {
418        std::ptr::from_ref(res)
419            .cast::<Option<R>>()
420            .as_ref()
421            .expect("wut")
422            .clone()
423    }
424}
ftml_solver/judgment_cache.rs

ftml_solver/
judgment_cache.rs
