catlog/tt/
context.rs

1//! Contexts store the type and values of in-scope variables during elaboration.
2use crate::tt::{prelude::*, val::*};
3
4/// Each variable in context is associated with a label and a type.
5///
6/// Multiple variables with the same name can show up in context; in this case
7/// the most recent one is selected, as follows the standard scope conventions.
8pub struct VarInContext {
9    /// The name of the variable.
10    pub name: VarName,
11    /// The label for the variable.
12    pub label: LabelSegment,
13    /// The type of the variable.
14    pub ty: Option<TyV>,
15}
16
17impl VarInContext {
18    /// Constructor for VarInContext.
19    pub fn new(name: VarName, label: LabelSegment, ty: Option<TyV>) -> Self {
20        Self { name, label, ty }
21    }
22}
23
24/// The variable context during elaboration
25pub struct Context {
26    /// Stores the value of each of the variables in context
27    pub env: Env,
28    /// Stores the names and types of each of the variables in context.
29    ///
30    /// We allow the type to be "none" as a hack for the `self` variable before we
31    /// know the type of the `self` variable.
32    pub scope: Vec<VarInContext>,
33}
34
35/// A checkpoint that we can return the context to.
36pub struct ContextCheckpoint {
37    env: Env,
38    scope: usize,
39}
40
41// Clippy wants this for some reason
42impl Default for Context {
43    fn default() -> Self {
44        Self::new()
45    }
46}
47
48impl Context {
49    /// Create an empty context.
50    pub fn new() -> Self {
51        Self {
52            env: Env::Nil,
53            scope: Vec::new(),
54        }
55    }
56
57    /// Create a checkpoint from the current state of the context.
58    pub fn checkpoint(&self) -> ContextCheckpoint {
59        ContextCheckpoint {
60            env: self.env.clone(),
61            scope: self.scope.len(),
62        }
63    }
64
65    /// Reset the context to a previously-saved checkpoint.
66    pub fn reset_to(&mut self, c: ContextCheckpoint) {
67        self.env = c.env;
68        self.scope.truncate(c.scope);
69    }
70
71    /// Add a new variable to scope (note: does not add it to the environment)
72    pub fn push_scope(&mut self, name: VarName, label: LabelSegment, ty: Option<TyV>) {
73        self.scope.push(VarInContext::new(name, label, ty))
74    }
75
76    /// Lookup a variable by name
77    pub fn lookup(&self, name: VarName) -> Option<(BwdIdx, LabelSegment, Option<TyV>)> {
78        self.scope
79            .iter()
80            .rev()
81            .enumerate()
82            .find(|(_, v)| v.name == name)
83            .map(|(i, v)| (i.into(), v.label, v.ty.clone()))
84    }
85}
catlog/tt/context.rs

catlog/tt/
context.rs
