summaryrefslogtreecommitdiff
path: root/dhall/src/semantics/core/context.rs
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/semantics/core/context.rs')
-rw-r--r--dhall/src/semantics/core/context.rs33
1 files changed, 33 insertions, 0 deletions
diff --git a/dhall/src/semantics/core/context.rs b/dhall/src/semantics/core/context.rs
index 25e4037..826ba15 100644
--- a/dhall/src/semantics/core/context.rs
+++ b/dhall/src/semantics/core/context.rs
@@ -22,6 +22,11 @@ pub(crate) struct TyCtx {
next_uid: Rc<RefCell<u64>>,
}
+#[derive(Debug, Clone)]
+pub(crate) struct VarCtx<'b> {
+ ctx: Vec<&'b Binder>,
+}
+
impl TyCtx {
pub fn new() -> Self {
TyCtx {
@@ -128,6 +133,34 @@ impl TyCtx {
}
}
+impl<'b> VarCtx<'b> {
+ pub fn new() -> Self {
+ VarCtx { ctx: Vec::new() }
+ }
+ pub fn insert(&self, binder: &'b Binder) -> Self {
+ VarCtx {
+ ctx: self.ctx.iter().copied().chain(Some(binder)).collect(),
+ }
+ }
+ pub fn lookup(&self, binder: &Binder) -> Option<usize> {
+ self.ctx
+ .iter()
+ .rev()
+ .enumerate()
+ .find(|(_, other)| binder.same_binder(other))
+ .map(|(i, _)| i)
+ }
+ pub fn lookup_by_name(&self, binder: &Binder) -> Option<usize> {
+ self.ctx
+ .iter()
+ .rev()
+ .filter(|other| binder.name() == other.name())
+ .enumerate()
+ .find(|(_, other)| binder.same_binder(other))
+ .map(|(i, _)| i)
+ }
+}
+
impl Shift for CtxItem {
fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
Some(match self {