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.rs53
1 files changed, 3 insertions, 50 deletions
diff --git a/dhall/src/semantics/core/context.rs b/dhall/src/semantics/core/context.rs
index 826ba15..3a7930e 100644
--- a/dhall/src/semantics/core/context.rs
+++ b/dhall/src/semantics/core/context.rs
@@ -1,6 +1,4 @@
-use std::cell::RefCell;
use std::collections::HashMap;
-use std::rc::Rc;
use crate::error::TypeError;
use crate::semantics::core::value::Value;
@@ -17,28 +15,14 @@ enum CtxItem {
#[derive(Debug, Clone)]
pub(crate) struct TyCtx {
ctx: Vec<(Binder, CtxItem)>,
- /// Keeps track of the next free binder id to assign. Shared among all the contexts to ensure
- /// unicity across the expression.
- next_uid: Rc<RefCell<u64>>,
-}
-
-#[derive(Debug, Clone)]
-pub(crate) struct VarCtx<'b> {
- ctx: Vec<&'b Binder>,
}
impl TyCtx {
pub fn new() -> Self {
- TyCtx {
- ctx: Vec::new(),
- next_uid: Rc::new(RefCell::new(0)),
- }
+ TyCtx { ctx: Vec::new() }
}
fn with_vec(&self, vec: Vec<(Binder, CtxItem)>) -> Self {
- TyCtx {
- ctx: vec,
- next_uid: self.next_uid.clone(),
- }
+ TyCtx { ctx: vec }
}
pub fn insert_type(&self, x: &Binder, t: Value) -> Self {
let mut vec = self.ctx.clone();
@@ -79,10 +63,7 @@ impl TyCtx {
None
}
pub fn new_binder(&self, l: &Label) -> Binder {
- let mut next_uid = self.next_uid.borrow_mut();
- let uid = *next_uid;
- *next_uid += 1;
- Binder::new(l.clone(), uid)
+ Binder::new(l.clone())
}
/// Given a var that makes sense in the current context, map the given function in such a way
@@ -133,34 +114,6 @@ 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 {