diff options
Diffstat (limited to 'dhall/src/semantics/core/context.rs')
-rw-r--r-- | dhall/src/semantics/core/context.rs | 33 |
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 { |