1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145

/// Index
/// The index contains information about items in the proof file that are useful
/// for printing and debugging purposes.
#[derive(Debug)]
pub struct Index<'a> {
    /// The root pointer of the index BST (binary search tree)
    pub(crate) root_bst_ptr: u64,
    /// A pointer to the proof file, used to resolve file relative pointers
    pub(crate) file: &'a [u8],
    pub(crate) sorts: &'a [u8],
    pub(crate) terms: &'a [u8],
    pub(crate) theorems: &'a [u8],
}

use crate::{error, parser};

impl<'a> Index<'a> {
    /// Return a pointer to the root of the index binary search tree (BST)
    pub fn root_bst_ptr(&self) -> u64 {
        self.root_bst_ptr
    }

    /// Return the slice of the data containing the pointers to the sort index
    /// entries
    pub fn sorts(&self) -> &[u8] {
        self.sorts
    }

    /// Return the pointer to the sort index entry by index number
    pub fn sort_pointer(&self, idx: usize) -> Option<u64> {
        let num_sorts = self.sorts.len() / 8;

        if idx < num_sorts {
            parser::parse_index_pointer(self.sorts, idx)
                .ok()
                .map(|ptr| ptr.1)
        } else {
            None
        }
    }

    /// Return the slice of the data containing the pointers to the term index
    /// entries
    pub fn terms(&self) -> &[u8] {
        self.terms
    }

    /// Return the pointer to the sort index entry by index number
    pub fn term_pointer(&self, idx: usize) -> Option<u64> {
        let num_terms = self.terms.len() / 8;

        if idx < num_terms {
            parser::parse_index_pointer(self.terms, idx)
                .ok()
                .map(|ptr| ptr.1)
        } else {
            None
        }
    }

    /// Return the slice of the data containing the pointers to the theorem index
    /// entries
    pub fn theorems(&self) -> &[u8] {
        self.theorems
    }

    /// Return the pointer to the theorem index entry by index number
    pub fn theorem_pointer(&self, idx: usize) -> Option<u64> {
        let num_theorems = self.theorems.len() / 8;

        if idx < num_theorems {
            parser::parse_index_pointer(self.theorems, idx)
                .ok()
                .map(|ptr| ptr.1)
        } else {
            None
        }
    }

    /// Visit all sorts in the index using the supplied `visitor`
    pub fn visit_sorts<V: Visitor>(&self, visitor: &mut V) {
        let num_sorts = self.sorts.len() / 8;
        parser::parse_index(self.file, self.sorts, num_sorts, visitor).unwrap();
    }

    /// Visit all terms in the index using the supplied `visitor`
    pub fn visit_terms<V: Visitor>(&self, visitor: &mut V) {
        let num_terms = self.terms.len() / 8;
        parser::parse_index(self.file, self.terms, num_terms, visitor).unwrap();
    }

    /// Visit all theorems in the index using the supplied `visitor`
    pub fn visit_theorems<V: Visitor>(&self, visitor: &mut V) {
        let num_theorems = self.theorems.len() / 8;
        parser::parse_index(self.file, self.theorems, num_theorems, visitor).unwrap();
    }

    /// Get the pointer to a sort index entry, and the entry data itself
    pub fn sort(&self, idx: usize) -> Result<IndexEntry, nom::Err<error::ParseError>> {
        let (_, entry) = parser::parse_index_by_idx(self.file, self.sorts, idx)?;

        Ok(entry)
    }

    /// Get the pointer to a term index entry, and the entry data itself
    pub fn term(&self, idx: usize) -> Result<IndexEntry, nom::Err<error::ParseError>> {
        let (_, entry) = parser::parse_index_by_idx(self.file, self.terms, idx)?;

        Ok(entry)
    }

    /// Get the pointer to a theorem index entry, and the entry data itself
    pub fn theorem(&self, idx: usize) -> Result<IndexEntry, nom::Err<error::ParseError>> {
        let (_, entry) = parser::parse_index_by_idx(self.file, self.theorems, idx)?;

        Ok(entry)
    }
}

/// An index entry
#[derive(Debug, Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash)]
pub struct IndexEntry<'a> {
    /// Pointer to this entry in the index
    pub ptr: u64,
    /// Pointer (file-relative) to the left subtree of this item in the BST
    pub left: u64,
    /// Pointer (file-relative) to the right subtree of this item in the BST
    pub right: u64,
    /// Row number in source file
    pub row: u32,
    /// Column number in source file
    pub col: u32,
    /// Pointer to the command statement that defines this item
    pub proof: u64,
    /// Index to the item in the relevant table
    pub idx: u32,
    /// To identify the item type
    pub kind: u8,
    /// A null-terminated character string with the name
    pub name: &'a [u8],
}

pub trait Visitor {
    fn visit<'a>(&mut self, entry: IndexEntry);
}