prism_compiler/lang/
env.rs

1use crate::lang::TcEnv;
2use crate::lang::UnionIndex;
3use rpds::Vector;
4
5#[derive(Copy, Clone, Eq, PartialEq, Debug, Hash)]
6pub struct UniqueVariableId(usize);
7
8#[derive(Clone, Eq, PartialEq, Debug)]
9pub enum EnvEntry {
10    // Definitions used during type checking
11    /// We know the type of this variable, but not its value. The type is the second `UnionIndex`
12    CType(UniqueVariableId, UnionIndex),
13
14    CSubst(UnionIndex, UnionIndex),
15
16    // Definitions used during beta reduction
17    RType(UniqueVariableId),
18    RSubst(UnionIndex, Env),
19}
20
21#[derive(Clone, Eq, PartialEq, Debug)]
22pub struct GenericEnv<T>(Vector<T>);
23
24impl<T> Default for GenericEnv<T> {
25    fn default() -> Self {
26        Self(Vector::default())
27    }
28}
29
30pub type Env = GenericEnv<EnvEntry>;
31
32impl<T> GenericEnv<T> {
33    pub fn new() -> Self {
34        Self::default()
35    }
36
37    #[must_use]
38    pub fn cons(&self, e: T) -> Self {
39        Self(self.0.push_back(e))
40    }
41
42    /// Drops the last `count` elements from the Environment
43    #[must_use]
44    pub fn shift(&self, count: usize) -> Self {
45        let mut s = self.0.clone();
46        assert!(s.len() >= count);
47        for _ in 0..count {
48            s.drop_last_mut();
49        }
50        Self(s)
51    }
52
53    pub fn len(&self) -> usize {
54        self.0.len()
55    }
56
57    pub fn is_empty(&self) -> bool {
58        self.0.is_empty()
59    }
60
61    pub fn get(&self, index: usize) -> Option<&T> {
62        if index >= self.len() {
63            None
64        } else {
65            self.0.get(self.0.len() - 1 - index)
66        }
67    }
68
69    pub fn iter(&self) -> impl Iterator<Item = &T> {
70        self.0.iter().rev()
71    }
72}
73
74impl<T> std::ops::Index<usize> for GenericEnv<T> {
75    type Output = T;
76
77    fn index(&self, index: usize) -> &Self::Output {
78        self.get(index).unwrap()
79    }
80}
81
82impl TcEnv {
83    pub fn new_tc_id(&mut self) -> UniqueVariableId {
84        let id = UniqueVariableId(self.tc_id);
85        self.tc_id += 1;
86        id
87    }
88}
prism_compiler/lang/env.rs

prism_compiler/lang/
env.rs
