ftml_solver/
context.rs

1use std::borrow::Cow;
2
3use ftml_ontology::terms::ComponentVar;
4use smallvec::SmallVec;
5
6use crate::{
7    Checker,
8    facts::{Fact, GlobalOrLocal, LocalFacts},
9    hoas::HOASSymbols,
10    split::SplitStrategy,
11};
12
13pub(crate) const CONTEXT_LEN: usize = 4;
14
15pub trait CowLike<'a> {
16    fn into_cow(self) -> Cow<'a, ComponentVar>;
17}
18impl<'a> CowLike<'a> for ComponentVar {
19    #[inline]
20    fn into_cow(self) -> Cow<'a, ComponentVar> {
21        Cow::Owned(self)
22    }
23}
24impl<'a> CowLike<'a> for &'a ComponentVar {
25    #[inline]
26    fn into_cow(self) -> Cow<'a, ComponentVar> {
27        Cow::Borrowed(self)
28    }
29}
30
31#[derive(Clone)]
32pub(crate) struct ContextBase<'c> {
33    //hoas: Option<HOASSymbols>,
34    ctx: SmallVec<Cow<'c, ComponentVar>, { super::context::CONTEXT_LEN }>,
35    blocked: Vec<GlobalOrLocal>,
36    facts: LocalFacts,
37    goal_counter: std::sync::Arc<std::sync::atomic::AtomicUsize>,
38}
39impl<'c> ContextBase<'c> {
40    pub fn new() -> Self {
41        Self {
42            ctx: SmallVec::new(),
43            blocked: Vec::new(),
44            facts: LocalFacts::default(),
45            goal_counter: std::sync::Arc::new(std::sync::atomic::AtomicUsize::new(1)), //hoas: HOASSymbols::get(top),
46        }
47    }
48    #[inline]
49    pub const fn get_ref(&mut self) -> ContextWrap<'c, '_> {
50        ContextWrap(self)
51    }
52}
53impl<'c> AsRef<[Cow<'c, ComponentVar>]> for ContextBase<'c> {
54    #[inline]
55    fn as_ref(&self) -> &[Cow<'c, ComponentVar>] {
56        &self.ctx
57    }
58}
59
60pub struct ContextWrap<'c, 's>(&'s mut ContextBase<'c>);
61impl<'c> ContextWrap<'c, '_> {
62    pub(crate) fn clone_base(&self) -> ContextBase<'c> {
63        self.0.clone()
64    }
65    pub(crate) fn pop(&mut self, len: usize) {
66        for _ in 0..len {
67            self.0.ctx.pop();
68        }
69        let newlen = self.0.ctx.len();
70        while let Some((i, _)) = self.0.facts.facts.last()
71            && *i >= newlen
72        {
73            self.0.facts.facts.pop();
74        }
75    }
76
77    pub(crate) fn block_fact(&mut self, fact: GlobalOrLocal) {
78        self.0.blocked.push(fact);
79    }
80    pub(crate) fn blocked(&self) -> &[GlobalOrLocal] {
81        &self.0.blocked
82    }
83    pub(crate) const fn facts(&self) -> &LocalFacts {
84        &self.0.facts
85    }
86    pub(crate) fn goal_counter(&self) -> &std::sync::atomic::AtomicUsize {
87        &self.0.goal_counter
88    }
89    pub(crate) fn push<Split: SplitStrategy>(
90        &mut self,
91        top: &Checker<Split>,
92        var: Cow<'c, ComponentVar>,
93    ) {
94        /*
95        if let Some(tp) = var.tp.as_ref()
96            && let Some(hoas) = top.hoas()
97            && let Some(fact) = Fact::from_tp(hoas, tp, top)
98        {
99            self.0.facts.facts.push((self.0.ctx.len(), fact));
100        }
101        */
102        tracing::trace!("Adding");
103        self.0.ctx.push(var);
104    }
105    pub(crate) fn take(&mut self) -> ContextBase<'c> {
106        std::mem::replace(self.0, ContextBase::new())
107    }
108    pub(crate) fn set(&mut self, base: ContextBase<'c>) {
109        *self.0 = base;
110    }
111    pub(crate) const fn duplicate(&mut self) -> ContextWrap<'c, '_> {
112        ContextWrap(self.0)
113    }
114}
115impl<'c> AsRef<[Cow<'c, ComponentVar>]> for ContextWrap<'c, '_> {
116    #[inline]
117    fn as_ref(&self) -> &[Cow<'c, ComponentVar>] {
118        &self.0.ctx
119    }
120}
121impl std::fmt::Debug for ContextWrap<'_, '_> {
122    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
123        let mut ls = f.debug_list();
124        for cv in &self.0.ctx {
125            ls.entry(&**cv);
126        }
127        ls.finish()
128    }
129}
ftml_solver/context.rs

ftml_solver/
context.rs
