catlog/tt/
context.rs

1//! Contexts store the type and values of in-scope variables during elaboration.
2
3use derive_more::Constructor;
4
5use crate::tt::{prelude::*, val::*};
6
7/// Each variable in context is associated with a label and a type.
8///
9/// Multiple variables with the same name can show up in context; in this case
10/// the most recent one is selected, following the standard scope conventions.
11#[derive(Constructor)]
12pub struct VarInContext {
13    /// The name of the variable.
14    pub name: VarName,
15    /// The label for the variable.
16    pub label: LabelSegment,
17    /// The type of the variable.
18    ///
19    /// We allow the type to be null as a hack for the `self` variable before we
20    /// know the type of the `self` variable.
21    pub ty: Option<BaseTyV>,
22}
23
24/// Each *fiber* variable in context — a generator or sub-instance import
25/// introduced inside an instance body — with its label and fiber type.
26#[derive(Constructor)]
27pub struct FiberVarInContext {
28    /// The name of the fiber variable.
29    pub name: VarName,
30    /// The label for the fiber variable.
31    pub label: LabelSegment,
32    /// The fiber type of the variable.
33    pub ty: FiberTyV,
34}
35
36/// The variable context during elaboration.
37///
38/// Carries two scopes: the **base** context (`env`/`scope`) of ordinary
39/// terms typed by [`BaseTyV`], and a separate **fiber** context
40/// (`fiber_env`/`fiber_scope`) of instance generators and sub-instance
41/// imports typed by [`FiberTyV`]. The fiber scope is populated only while
42/// elaborating an instance body; the two never alias, so neither lookup
43/// can see the other's variables. See [`crate::tt::toplevel`] for why the
44/// two worlds are distinct.
45pub struct Context {
46    /// Stores the value of each of the base variables in context.
47    pub env: Env,
48    /// Stores the names and types of each of the base variables in context.
49    pub scope: Vec<VarInContext>,
50    /// Stores the value of each fiber variable in context.
51    pub fiber_env: FiberEnv,
52    /// Stores the names and fiber types of each fiber variable in context.
53    pub fiber_scope: Vec<FiberVarInContext>,
54}
55
56/// A checkpoint that we can return the context to.
57pub struct ContextCheckpoint {
58    env: Env,
59    scope: usize,
60    fiber_env: FiberEnv,
61    fiber_scope: usize,
62}
63
64impl Default for Context {
65    fn default() -> Self {
66        Self::new()
67    }
68}
69
70impl Context {
71    /// Create an empty context.
72    pub fn new() -> Self {
73        Self {
74            env: Env::Nil,
75            scope: Vec::new(),
76            fiber_env: FiberEnv::Nil,
77            fiber_scope: Vec::new(),
78        }
79    }
80
81    /// Create a checkpoint from the current state of the context.
82    pub fn checkpoint(&self) -> ContextCheckpoint {
83        ContextCheckpoint {
84            env: self.env.clone(),
85            scope: self.scope.len(),
86            fiber_env: self.fiber_env.clone(),
87            fiber_scope: self.fiber_scope.len(),
88        }
89    }
90
91    /// Reset the context to a previously-saved checkpoint.
92    pub fn reset_to(&mut self, c: ContextCheckpoint) {
93        self.env = c.env;
94        self.scope.truncate(c.scope);
95        self.fiber_env = c.fiber_env;
96        self.fiber_scope.truncate(c.fiber_scope);
97    }
98
99    /// Add a new base variable to scope (note: does not add it to the environment).
100    pub fn push_scope(&mut self, name: VarName, label: LabelSegment, ty: Option<BaseTyV>) {
101        self.scope.push(VarInContext::new(name, label, ty))
102    }
103
104    /// Lookup a base variable by name.
105    pub fn lookup(&self, name: VarName) -> Option<(BwdIdx, LabelSegment, Option<BaseTyV>)> {
106        self.scope
107            .iter()
108            .rev()
109            .enumerate()
110            .find(|(_, v)| v.name == name)
111            .map(|(i, v)| (i.into(), v.label, v.ty.clone()))
112    }
113
114    /// Add a new fiber variable to scope (note: does not add it to the
115    /// fiber environment).
116    pub fn push_fiber(&mut self, name: VarName, label: LabelSegment, ty: FiberTyV) {
117        self.fiber_scope.push(FiberVarInContext::new(name, label, ty))
118    }
119
120    /// Lookup a fiber variable by name.
121    pub fn lookup_fiber(&self, name: VarName) -> Option<(BwdIdx, LabelSegment, FiberTyV)> {
122        self.fiber_scope
123            .iter()
124            .rev()
125            .enumerate()
126            .find(|(_, v)| v.name == name)
127            .map(|(i, v)| (i.into(), v.label, v.ty.clone()))
128    }
129}
catlog/tt/context.rs

catlog/tt/
context.rs
