kontroli 0.4.0

Type checking for the lambda-Pi calculus modulo rewriting
Documentation 
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

//! Maps from strings to (shared) symbols.

use super::{symbol, Symbol};
use alloc::{string::String, vec::Vec};
use core::borrow::Borrow;
use fnv::FnvHashMap;
use nested_modules::Context;

#[derive(Debug)]
pub enum Error {
    Reinsertion,
}

/// Map from strings to (shared) symbols.
#[derive(Default)]
pub struct Symbols<'s>(Context<String, FnvHashMap<String, &'s symbol::Owned>>);

impl<'s> Symbols<'s> {
    pub fn new() -> Self {
        Default::default()
    }

    pub fn get<S: Borrow<str> + Ord>(&self, path: &[S], name: &S) -> Option<Symbol<'s>> {
        self.0
            .find(path.iter().map(|p| p.borrow()))
            .filter_map(|module| module.data.get(name.borrow()))
            .next()
            .copied()
            .map(Symbol::new)
    }

    pub fn insert(&mut self, name: String, s: &'s symbol::Owned) -> Result<Symbol<'s>, Error> {
        // `insert` returns false if the symbol is already in the set
        if self.0.get_mut().data.insert(name, s).is_some() {
            return Err(Error::Reinsertion);
        }
        Ok(Symbol::new(s))
    }

    pub fn set_path(&mut self, path: Vec<String>) {
        while self.0.close() {}
        path.into_iter().for_each(|p| self.0.open_or_default(p))
    }
}