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

ftml_solver/impls/
mod.rs
