trivial_kernel/context/
store.rs

1use crate::{Var, Var_};
2
3#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]
4pub struct PackedPtr(u32);
5
6impl PackedPtr {
7    pub fn expr(e: u32) -> PackedPtr {
8        PackedPtr(e << 2)
9    }
10
11    pub fn as_expr(self) -> Option<Ptr> {
12        if self.0 & 0x3 == 0x0 {
13            Some(self.into())
14        } else {
15            None
16        }
17    }
18
19    pub fn proof(e: u32) -> PackedPtr {
20        PackedPtr((e << 2) | 0x01)
21    }
22
23    pub fn as_proof(self) -> Option<Ptr> {
24        if self.0 & 0x03 == 0x01 {
25            Some(self.into())
26        } else {
27            None
28        }
29    }
30
31    pub fn conv(e: u32) -> PackedPtr {
32        PackedPtr((e << 2) | 0x02)
33    }
34
35    pub fn as_conv(self) -> Option<Ptr> {
36        if self.0 & 0x03 == 0x02 {
37            Some(self.into())
38        } else {
39            None
40        }
41    }
42
43    pub fn co_conv(e: u32) -> PackedPtr {
44        PackedPtr((e << 2) | 0x03)
45    }
46
47    pub fn as_co_conv(self) -> Option<Ptr> {
48        if self.0 & 0x03 == 0x03 {
49            Some(self.into())
50        } else {
51            None
52        }
53    }
54
55    pub fn to_display<'a, S: Store>(&self, store: &'a S) -> DisplayPackedPtr<'a, S> {
56        DisplayPackedPtr(*self, store)
57    }
58}
59
60impl From<&PackedPtr> for Ptr {
61    fn from(ptr: &PackedPtr) -> Ptr {
62        Ptr(ptr.0 >> 2)
63    }
64}
65
66impl From<PackedPtr> for Ptr {
67    fn from(ptr: PackedPtr) -> Ptr {
68        Ptr(ptr.0 >> 2)
69    }
70}
71
72use core::fmt::{self, Display, Formatter};
73
74pub struct DisplayPackedPtr<'a, S: Store>(PackedPtr, &'a S);
75
76impl<'a, S: Store> Display for DisplayPackedPtr<'a, S> {
77    fn fmt(&self, f: &mut Formatter) -> fmt::Result {
78        write!(f, "{}", Into::<Ptr>::into(self.0).0)
79    }
80}
81
82impl Display for PackedPtr {
83    fn fmt(&self, f: &mut Formatter) -> fmt::Result {
84        match self.0 & 0x03 {
85            0x00 => write!(f, "expr"),
86            0x01 => write!(f, "proof"),
87            0x02 => write!(f, "conv"),
88            0x03 => write!(f, "co-conv"),
89            _ => Ok(()),
90        }
91    }
92}
93
94#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash, PartialOrd, Ord)]
95pub struct Ptr(pub u32);
96
97impl Ptr {
98    #[inline(always)]
99    pub fn to_proof(self) -> PackedPtr {
100        PackedPtr::proof(self.0)
101    }
102
103    #[inline(always)]
104    pub fn to_expr(self) -> PackedPtr {
105        PackedPtr::expr(self.0)
106    }
107
108    #[inline(always)]
109    pub fn to_co_conv(self) -> PackedPtr {
110        PackedPtr::co_conv(self.0)
111    }
112
113    #[inline(always)]
114    pub fn to_conv(self) -> PackedPtr {
115        PackedPtr::conv(self.0)
116    }
117
118    #[inline(always)]
119    pub fn get_idx(self) -> usize {
120        self.0 as usize
121    }
122}
123
124#[derive(Debug)]
125pub enum ElementRef<'a, Ty> {
126    Variable {
127        ty: &'a Ty,
128        var: &'a u16,
129    },
130    Term {
131        ty: &'a Ty,
132        id: &'a u32,
133        args: &'a [PackedPtr],
134    },
135    /// Convertability proof
136    Conv {
137        e1: &'a PackedPtr,
138        e2: &'a PackedPtr,
139    },
140}
141
142impl<'a, Ty: Var> ElementRef<'a, Ty> {
143    pub fn to_display<'b, S: Store<Var = Ty>>(
144        &'b self,
145        store: &'b S,
146    ) -> DisplayElement<'a, 'b, Ty, S> {
147        DisplayElement(self, store)
148    }
149}
150
151pub struct DisplayElement<'a, 'b, Ty: Var, S: Store<Var = Ty>>(
152    pub &'b ElementRef<'a, Ty>,
153    pub &'b S,
154);
155
156impl<'a, 'b, Ty: Var, S: Store<Var = Ty>> Display for DisplayElement<'a, 'b, Ty, S> {
157    fn fmt(&self, f: &mut Formatter) -> fmt::Result {
158        match self.0 {
159            ElementRef::Variable { var, .. } => {
160                write!(f, "v{}", var)
161                //
162            }
163            ElementRef::Term { id, args, .. } => {
164                write!(f, "t{} (", id)?;
165
166                for i in *args {
167                    match self.1.get_element(i.into()) {
168                        Some(el) => write!(f, "{} ", el.to_display(self.1))?,
169                        None => write!(f, "invalid_ptr")?,
170                    }
171                }
172
173                write!(f, ")")
174            }
175            ElementRef::Conv { e1, e2 } => write!(f, "conv: {:?} {:?}", e1, e2),
176        }
177    }
178}
179
180#[derive(Debug)]
181pub struct Term<'a, Ty> {
182    pub ty: &'a Ty,
183    pub id: &'a u32,
184    pub args: &'a [PackedPtr],
185}
186
187use core::convert::TryFrom;
188use core::convert::TryInto;
189
190impl<'a, Ty> TryFrom<ElementRef<'a, Ty>> for Term<'a, Ty> {
191    type Error = Kind;
192
193    fn try_from(element: ElementRef<'a, Ty>) -> Result<Self, Self::Error> {
194        if let ElementRef::Term { ty, id, args } = element {
195            Ok(Term { ty, id, args })
196        } else {
197            Err(Kind::InvalidStoreType)
198        }
199    }
200}
201
202#[derive(Debug)]
203pub struct Conv {
204    pub e1: PackedPtr,
205    pub e2: PackedPtr,
206}
207
208impl<'a, Ty> TryFrom<ElementRef<'a, Ty>> for Conv {
209    type Error = Kind;
210
211    fn try_from(element: ElementRef<'a, Ty>) -> Result<Self, Self::Error> {
212        if let ElementRef::Conv { e1, e2 } = element {
213            Ok(Conv { e1: *e1, e2: *e2 })
214        } else {
215            Err(Kind::InvalidStoreType)
216        }
217    }
218}
219
220#[derive(Debug)]
221pub struct Variable<Ty> {
222    pub ty: Ty,
223    pub var: u16,
224}
225
226impl<'a, Ty: Copy> TryFrom<ElementRef<'a, Ty>> for Variable<Ty> {
227    type Error = Kind;
228
229    fn try_from(element: ElementRef<'a, Ty>) -> Result<Self, Self::Error> {
230        if let ElementRef::Variable { ty, var } = element {
231            Ok(Variable { ty: *ty, var: *var })
232        } else {
233            Err(Kind::InvalidStoreType)
234        }
235    }
236}
237
238#[derive(Debug, Clone, Eq, PartialEq, Ord, PartialOrd, Hash)]
239enum InternalStoreElement {
240    Variable {
241        ty: Var_,
242        var: u16,
243    },
244    Term {
245        ty: Var_,
246        num_args: u16,
247        id: u32,
248        ptr_args: usize,
249    },
250    Conv {
251        e1: PackedPtr,
252        e2: PackedPtr,
253    },
254}
255
256#[derive(Debug, Default, Clone, Eq, PartialEq, Ord, PartialOrd, Hash)]
257pub struct Store_ {
258    data: Vec<InternalStoreElement>,
259    args: Vec<PackedPtr>,
260}
261
262use crate::error::Kind;
263use crate::KResult;
264
265pub trait Store {
266    type Var: Var;
267
268    fn create_term<T>(
269        &mut self,
270        id: u32,
271        args: T,
272        types: &[Self::Var],
273        ret_type: &Self::Var,
274        sort: u8,
275        def: bool,
276    ) -> KResult<PackedPtr>
277    where
278        T: IntoIterator<Item = PackedPtr>,
279        T: Clone;
280
281    fn alloc_var(&mut self, ty: Self::Var, idx: u16) -> PackedPtr;
282
283    fn alloc_conv(&mut self, l: PackedPtr, r: PackedPtr) -> PackedPtr;
284
285    fn clear(&mut self);
286
287    fn get_type_of_expr(&self, ptr: Ptr) -> Option<&Self::Var>;
288
289    fn get_element(&self, ptr: Ptr) -> Option<ElementRef<Self::Var>>;
290
291    fn get<'a, T: TryFrom<ElementRef<'a, Self::Var>, Error = Kind>>(
292        &'a self,
293        ptr: Ptr,
294    ) -> KResult<T>;
295}
296
297impl Store for Store_ {
298    type Var = Var_;
299
300    fn create_term<T>(
301        &mut self,
302        id: u32,
303        args: T,
304        types: &[Self::Var],
305        ret_type: &Self::Var,
306        sort: u8,
307        def: bool,
308    ) -> KResult<PackedPtr>
309    where
310        T: IntoIterator<Item = PackedPtr>,
311        T: Clone,
312    {
313        let offset = self.args.len();
314        let mut accum = 0;
315        let mut g_deps = [0; 256];
316        let mut bound = 0;
317
318        for (arg, &target_type) in args.clone().into_iter().zip(types.iter()) {
319            let arg = arg.as_expr().ok_or(Kind::InvalidStoreType)?;
320
321            let ty = self.get_type_of_expr(arg).ok_or(Kind::InvalidStoreExpr)?;
322
323            if !ty.is_compatible_to(&target_type) {
324                return Err(Kind::IncompatibleTypes);
325            }
326
327            let mut deps = ty.dependencies();
328
329            if target_type.is_bound() {
330                *g_deps
331                    .get_mut(bound as usize)
332                    .ok_or(Kind::DependencyOverflow)? = deps;
333
334                bound += 1;
335            } else {
336                if def {
337                    for (_, &j) in g_deps
338                        .get(..(bound as usize))
339                        .ok_or(Kind::DependencyOverflow)?
340                        .iter()
341                        .enumerate()
342                        .filter(|(i, _)| target_type.depends_on(*i as u8))
343                    {
344                        deps &= !j;
345                    }
346                }
347
348                accum |= deps;
349            }
350        }
351
352        if def && ret_type.dependencies() != 0 {
353            for (_, &j) in g_deps
354                .get(..(bound as usize))
355                .ok_or(Kind::DependencyOverflow)?
356                .iter()
357                .enumerate()
358                .filter(|(i, _)| ret_type.depends_on(*i as u8))
359            {
360                accum |= j;
361            }
362        }
363
364        self.args.extend(args);
365
366        let ise = InternalStoreElement::Term {
367            ty: Var::new(sort, accum, false),
368            num_args: types.len() as u16,
369            id,
370            ptr_args: offset,
371        };
372
373        let size = self.data.len() as u32;
374
375        self.data.push(ise);
376
377        Ok(PackedPtr::expr(size))
378    }
379
380    fn alloc_var(&mut self, ty: Self::Var, idx: u16) -> PackedPtr {
381        let size = self.data.len() as u32;
382
383        self.data
384            .push(InternalStoreElement::Variable { ty, var: idx });
385
386        PackedPtr::expr(size)
387    }
388
389    fn alloc_conv(&mut self, l: PackedPtr, r: PackedPtr) -> PackedPtr {
390        let size = self.data.len() as u32;
391
392        self.data.push(InternalStoreElement::Conv { e1: l, e2: r });
393
394        PackedPtr::conv(size)
395    }
396
397    fn clear(&mut self) {
398        self.data.clear();
399        self.args.clear();
400    }
401
402    fn get_type_of_expr(&self, ptr: Ptr) -> Option<&Self::Var> {
403        let element = self.data.get(ptr.get_idx())?;
404
405        match element {
406            InternalStoreElement::Variable { ty, .. } => Some(ty),
407            InternalStoreElement::Term { ty, .. } => Some(ty),
408            _ => None,
409        }
410    }
411
412    fn get_element(&self, ptr: Ptr) -> Option<ElementRef<Self::Var>> {
413        let element = self.data.get(ptr.get_idx())?;
414
415        match element {
416            InternalStoreElement::Variable { ty, var } => Some(ElementRef::Variable { ty, var }),
417            InternalStoreElement::Term {
418                ty,
419                num_args,
420                id,
421                ptr_args,
422            } => {
423                let ptr_args = *ptr_args as usize;
424                let args = self
425                    .args
426                    .as_slice()
427                    .get(ptr_args..(ptr_args + *num_args as usize))?;
428
429                Some(ElementRef::Term { ty, id, args })
430            }
431            InternalStoreElement::Conv { e1, e2 } => Some(ElementRef::Conv { e1, e2 }),
432        }
433    }
434
435    fn get<'a, T: TryFrom<ElementRef<'a, Self::Var>, Error = Kind>>(
436        &'a self,
437        ptr: Ptr,
438    ) -> KResult<T> {
439        let element = self.get_element(ptr).ok_or(Kind::InvalidStoreIndex)?;
440
441        element.try_into()
442    }
443}
444
445impl Display for Store_ {
446    fn fmt(&self, f: &mut Formatter) -> fmt::Result {
447        for i in 0..self.data.len() {
448            match self.get_element(Ptr(i as u32)) {
449                Some(el) => writeln!(f, "> {}", el.to_display(self))?,
450                None => writeln!(f, "> Invalid ptr")?,
451            }
452        }
453        Ok(())
454    }
455}
trivial_kernel/context/store.rs

trivial_kernel/context/
store.rs
