ftml_solver/impls/
mod.rs

1#![allow(clippy::absurd_extreme_comparisons)]
2
3pub mod backend;
4pub mod equality;
5mod inference;
6pub mod preparation;
7pub mod proving;
8pub mod records;
9pub mod simplify;
10pub mod solving;
11mod typing;
12
13use crate::{
14    CheckRef, Checker,
15    context::{ContextBase, CowLike},
16    impls::solving::Solutions,
17    judgment_cache::{JudgmentCache, JudgmentCacheBase, Judgments},
18    split::{CancelToken, SplitStrategy},
19    trace::{CheckLogCow, CheckingTask, PreCheckLog, RefCheckLog},
20    utils::{Merge, MutableRefList},
21};
22use ftml_ontology::terms::ComponentVar;
23use ftml_solver_trace::traceref;
24use proving::ProverState;
25use smallvec::SmallVec;
26use std::borrow::Cow;
27
28const DEPTH_LIMIT: usize = 64;
29
30impl<Split: SplitStrategy> Checker<Split> {
31    pub(crate) fn wrap_task<'t, R: std::fmt::Debug + Clone + 'static, F>(
32        &'t self,
33        task: CheckingTask<'t>,
34        unknowns: Option<Solutions>,
35        then: F,
36    ) -> (Option<R>, Solutions, PreCheckLog)
37    where
38        F: FnOnce(CheckRef<'t, '_, Split>) -> Option<R>,
39    {
40        let mut context = ContextBase::new();
41        let mut solutions = unknowns.unwrap_or_default();
42        let mut messages = SmallVec::new();
43        let cancel = CancelToken::default();
44        let proof_state = ProverState::default();
45        let mut judgment_cache = JudgmentCacheBase::default();
46        let rf = CheckRef {
47            top: self,
48            messages: &mut messages,
49            cancel: &cancel,
50            context: context.get_ref(),
51            judgment_cache: judgment_cache.make_ref(),
52            proof_state: &proof_state,
53            added: 0,
54            solutions: MutableRefList::new(&mut solutions),
55            traced: true,
56        };
57        let r = then(rf);
58        let rl = MutableRefList::new(&mut solutions);
59        let line = task
60            .close(r.as_ref(), messages.into_boxed_slice(), context.as_ref())
61            .into_owned(&|t| rl.subst(t));
62        tracing::trace!("Solutions:{solutions:#?}");
63        (r, solutions, line)
64    }
65
66    pub(crate) fn wrap_none<'t, R: std::fmt::Debug + Clone + 'static, F>(
67        &'t self,
68        unknowns: Option<Solutions>,
69        then: F,
70    ) -> (Solutions, R)
71    where
72        F: FnOnce(CheckRef<'t, '_, Split>) -> R,
73    {
74        let mut context = ContextBase::new();
75        let mut solutions = unknowns.unwrap_or_default();
76        let mut messages = SmallVec::new();
77        let cancel = CancelToken::default();
78        let proof_state = ProverState::default();
79        let mut judgment_cache = JudgmentCacheBase::default();
80        let rf = CheckRef {
81            top: self,
82            messages: &mut messages,
83            cancel: &cancel,
84            judgment_cache: judgment_cache.make_ref(),
85            context: context.get_ref(),
86            proof_state: &proof_state,
87            added: 0,
88            solutions: MutableRefList::new(&mut solutions),
89            traced: true,
90        };
91        let r = then(rf);
92        (solutions, r)
93    }
94}
95
96impl<'c, 'i, Split: SplitStrategy> CheckRef<'c, 'i, Split> {
97    pub fn extend_context<C: CowLike<'c>>(&mut self, var: C) {
98        self.added += 1;
99        self.context.push(self.top, var.into_cow());
100    }
101
102    pub fn add_msg(&mut self, line: CheckLogCow<'c>) {
103        self.messages.push(line);
104    }
105    pub fn comment(&mut self, msg: impl Into<Cow<'static, str>>) {
106        self.messages.push(CheckLogCow::Owned(PreCheckLog::Msg(
107            vec![msg.into().into_owned().into()],
108            crate::trace::MessageLevel::Comment,
109        )));
110    }
111    pub fn counter(&mut self, msg: &'static str, num: usize) {
112        self.messages.push(CheckLogCow::Owned(PreCheckLog::Msg(
113            vec![msg.into(), num.into()],
114            crate::trace::MessageLevel::Comment,
115        )));
116    }
117    pub fn failure(&mut self, msg: impl Into<Cow<'static, str>>) {
118        self.messages.push(CheckLogCow::Owned(PreCheckLog::Msg(
119            vec![msg.into().into_owned().into()],
120            crate::trace::MessageLevel::Failure,
121        )));
122    }
123    #[inline]
124    pub(crate) fn split(&mut self) -> (&[Cow<'c, ComponentVar>], Trace<'c, '_>) {
125        (self.context.as_ref(), Trace(self.messages))
126    }
127
128    #[must_use]
129    pub fn iter_context(&self) -> impl ExactSizeIterator<Item = &ComponentVar> {
130        self.context.as_ref().iter().rev().map(|c| &**c)
131    }
132
133    pub(crate) fn traced<R: Clone>(
134        &mut self,
135        tsk: CheckingTask<'c>,
136        f: impl FnOnce(&mut Self) -> Option<R>,
137    ) -> Result<R, RefCheckLog<'c>> {
138        if self.depth() >= DEPTH_LIMIT {
139            //self.failure("Depth Limit Reached!");
140            return Err(traceref!(FAIL "Depth Limit Reached!"));
141        }
142        let (r, l) = self.traced_inner(tsk, f);
143        if let Some(r) = r {
144            self.messages.push(CheckLogCow::Borrowed(l));
145            Ok(r)
146        } else {
147            Err(l)
148        }
149    }
150
151    pub(crate) fn untraced<R: Clone>(
152        &mut self,
153        task: CheckingTask<'c>,
154        f: impl FnOnce(&mut Self) -> Option<R>,
155    ) -> Option<R> {
156        if self.depth() >= DEPTH_LIMIT {
157            self.failure("Depth Limit Reached!");
158            return None;
159        }
160        let old_msg = std::mem::replace(self.messages, SmallVec::new());
161        let ret = f(self);
162        *self.messages = old_msg;
163        let ctx = self.context.as_ref();
164        let ctx = &ctx[ctx.len() - self.added as usize..ctx.len()];
165        let line = task.close(ret.as_ref(), Box::new([]), ctx);
166        ret
167    }
168
169    pub(crate) fn traced_inner<R: Clone>(
170        &mut self,
171        task: CheckingTask<'c>,
172        f: impl FnOnce(&mut Self) -> Option<R>,
173    ) -> (Option<R>, RefCheckLog<'c>) {
174        if self.depth() >= DEPTH_LIMIT {
175            //self.failure("Depth Limit Reached!");
176            return (None, traceref!(FAIL "Depth Limit Reached!"));
177        }
178
179        if self.judgment_cache.running(&task) {
180            return (None, traceref!(FAIL "Recursion in Task check"));
181        }
182        if let Some(r) = self.judgment_cache.has::<R>(&task, &self.context) {
183            let l = task.close(
184                r.as_ref(),
185                Box::new([if r.is_some() {
186                    traceref!("previously proven")
187                } else {
188                    traceref!(FAIL "previously failed already")
189                }
190                .into()]),
191                &[],
192            );
193            return (r, l);
194        }
195        self.judgment_cache.push(task);
196        let old_msg = std::mem::replace(self.messages, SmallVec::new());
197        let ret = f(self);
198        let msgs = std::mem::replace(self.messages, old_msg);
199        let ctx = self.context.as_ref();
200        let ctx = &ctx[ctx.len() - self.added as usize..ctx.len()];
201        let task = self
202            .judgment_cache
203            .pop(&ret, self.context.as_ref(), &self.solutions)
204            .expect("wut");
205        let line = if crate::TRUNCATE_PROOFS && ret.is_some() {
206            task.close(ret.as_ref(), Box::new([]), ctx)
207        } else {
208            task.close(ret.as_ref(), msgs.into_boxed_slice(), ctx)
209        };
210        (ret, line)
211    }
212
213    #[inline]
214    pub const fn depth(&self) -> usize {
215        self.solutions.depth()
216    }
217
218    pub(crate) fn branch_traced<R: Clone>(
219        &mut self,
220        task: CheckingTask<'c>,
221        f: impl FnOnce(CheckRef<'c, '_, Split>) -> Option<R>,
222    ) -> Result<R, RefCheckLog<'c>> {
223        if self.depth() >= DEPTH_LIMIT {
224            //self.failure("Depth Limit Reached!");
225            return Err(traceref!(FAIL "Depth Limit Reached!"));
226        }
227        if self.judgment_cache.running(&task) {
228            return Err(traceref!(FAIL "Recursion in Task check"));
229        }
230        if let Some(r) = self.judgment_cache.has::<R>(&task, &self.context) {
231            return match r {
232                Some(r) => {
233                    self.messages.push(
234                        task.close(
235                            Some(&r),
236                            Box::new([traceref!("previously proven").into()]),
237                            &[],
238                        )
239                        .into(),
240                    );
241                    Ok(r)
242                }
243                None => Err(traceref!(FAIL "previously failed already")),
244            };
245        }
246
247        self.judgment_cache.push(task);
248
249        let mut messages = SmallVec::<CheckLogCow<'c>, _>::new();
250        let mut solutions = Solutions::default();
251        let inner = CheckRef {
252            messages: &mut messages,
253            context: self.context.duplicate(),
254            proof_state: self.proof_state,
255            judgment_cache: self.judgment_cache.copied(),
256            solutions: MutableRefList::new_with_parent(&mut solutions, &self.solutions),
257            top: self.top,
258            cancel: self.cancel,
259            added: 0,
260            traced: self.traced,
261        };
262        let ret = f(inner);
263        let ctx = self.context.as_ref();
264        let ctx = &ctx[ctx.len() - self.added as usize..ctx.len()];
265
266        let task = self
267            .judgment_cache
268            .pop(&ret, self.context.as_ref(), &solutions)
269            .expect("wut");
270
271        let line = if crate::TRUNCATE_PROOFS && ret.is_some() {
272            task.close(ret.as_ref(), Box::new([]), ctx)
273        } else {
274            task.close(ret.as_ref(), messages.into_boxed_slice(), ctx)
275        };
276        if let Some(r) = ret {
277            self.merge_solutions(solutions);
278            self.messages.push(line.into());
279            Ok(r)
280        } else {
281            Err(line)
282        }
283    }
284
285    pub fn scoped<'nt, R: Send + Sync + 'static>(
286        &'nt mut self,
287        f: impl FnOnce(&mut CheckRef<'nt, '_, Split>) -> R,
288    ) -> R {
289        let old_added = std::mem::take(&mut self.added);
290        let old_msgs = std::mem::take(self.messages);
291
292        // SAFETY:
293        // - all variables added in `f` with lifetime 'nt are popped again before we return
294        // - all messages added in `f` with lifetime 'nt are turned into owned ones
295        //   before readding
296        let muted = unsafe {
297            std::mem::transmute::<&mut CheckRef<'c, '_, Split>, &mut CheckRef<'nt, '_, Split>>(self)
298        };
299        let r = f(muted);
300        self.context
301            .pop(std::mem::replace(&mut self.added, old_added) as usize);
302        for m in std::mem::replace(self.messages, old_msgs) {
303            self.messages.push(m.into_owned(&|t| self.subst(t)).into());
304        }
305        r
306    }
307
308    pub(crate) fn cancellable<R: Send>(&mut self, f: impl FnOnce(&mut Self) -> R) -> R {
309        let old = self.cancel;
310        let cancel = old.derive();
311        let rf = &cancel;
312        let rf: &'c CancelToken<'c, Split::CancelToken> = unsafe { std::mem::transmute(rf) };
313        self.cancel = rf;
314        let r = f(self);
315        self.cancel = old;
316        drop(cancel);
317        r
318    }
319
320    pub(crate) fn wrap_check<R: Clone>(
321        &mut self,
322        task: CheckingTask<'c>,
323        f: impl FnOnce(&mut Self) -> Option<R>,
324    ) -> Option<R> {
325        if self.depth() >= DEPTH_LIMIT {
326            self.failure("Depth Limit Reached!");
327            return None;
328        }
329        if self.cancel.is_cancelled() {
330            self.failure("CANCELLED!");
331            return None;
332        }
333        match self.traced(task, f) {
334            Ok(r) => Some(r),
335            Err(l) => {
336                self.add_msg(l.into());
337                None
338            }
339        }
340    }
341
342    pub(crate) fn copied(&self) -> CheckRefBranch<'c, 'i, Split> {
343        CheckRefBranch {
344            context: self.context.clone_base(),
345            proof_state: self.proof_state,
346            messages: SmallVec::new(),
347            // --------------
348            top: self.top,
349            cache_base: self.judgment_cache.new_base(),
350            solutions: Solutions::default(),
351            // SAFETY: will not live longer than 'i; only immutable borrows, 'i is only stack reference
352            // to parent
353            parent_solutions: unsafe { std::mem::transmute(&self.solutions) },
354            cancel: self.cancel,
355            traced: self.traced,
356        }
357    }
358}
359
360pub struct CheckRefBranch<'c, 'i, Split: SplitStrategy> {
361    top: &'c Checker<Split>,
362    context: ContextBase<'c>,
363    proof_state: &'i ProverState,
364    cache_base: JudgmentCacheBase<'c>,
365    solutions: Solutions,
366    parent_solutions: &'i MutableRefList<'i, Solutions>,
367    cancel: &'i CancelToken<'i, Split::CancelToken>,
368    messages: SmallVec<CheckLogCow<'c>, 2>,
369    traced: bool,
370}
371impl<'c, Split: SplitStrategy> CheckRefBranch<'c, '_, Split> {
372    pub fn get_ref(&mut self) -> CheckRef<'c, '_, Split> {
373        CheckRef {
374            top: self.top,
375            cancel: self.cancel,
376            messages: &mut self.messages,
377            proof_state: self.proof_state,
378            judgment_cache: self.cache_base.make_ref(),
379            context: self.context.get_ref(),
380            added: 0,
381            solutions: MutableRefList::new_with_parent(&mut self.solutions, self.parent_solutions),
382            traced: self.traced,
383        }
384    }
385    pub fn close(self, checker: &mut CheckRef<'c, '_, Split>) {
386        checker.merge_solutions(self.solutions);
387        checker.messages.extend(self.messages);
388    }
389}
390
391impl<Split: SplitStrategy> Drop for CheckRef<'_, '_, Split> {
392    fn drop(&mut self) {
393        self.context.pop(self.added as usize);
394    }
395}
396
397pub struct Trace<'c, 'i>(&'i mut SmallVec<CheckLogCow<'c>, 2>);
398impl<'c> Trace<'c, '_> {
399    pub fn add_msg(&mut self, line: CheckLogCow<'c>) {
400        self.0.push(line);
401    }
402    pub fn comment(&mut self, msg: impl Into<Cow<'static, str>>) {
403        self.0.push(CheckLogCow::Owned(PreCheckLog::Msg(
404            vec![msg.into().into_owned().into()],
405            crate::trace::MessageLevel::Comment,
406        )));
407    }
408    pub fn failure(&mut self, msg: impl Into<Cow<'static, str>>) {
409        self.0.push(CheckLogCow::Owned(PreCheckLog::Msg(
410            vec![msg.into().into_owned().into()],
411            crate::trace::MessageLevel::Failure,
412        )));
413    }
414}
ftml_solver/impls/mod.rs

ftml_solver/impls/
mod.rs
