diff options
Diffstat (limited to '')
-rw-r--r-- | dhall/src/semantics/core/context.rs | 144 |
1 files changed, 0 insertions, 144 deletions
diff --git a/dhall/src/semantics/core/context.rs b/dhall/src/semantics/core/context.rs deleted file mode 100644 index f755f72..0000000 --- a/dhall/src/semantics/core/context.rs +++ /dev/null @@ -1,144 +0,0 @@ -use std::collections::HashMap; -use std::rc::Rc; - -use crate::error::TypeError; -use crate::semantics::core::value::Value; -use crate::semantics::core::value::ValueKind; -use crate::semantics::core::var::{AlphaVar, Shift, Subst}; -use crate::syntax::{Label, V}; - -#[derive(Debug, Clone)] -enum CtxItem { - Kept(AlphaVar, Value), - Replaced(Value), -} - -#[derive(Debug, Clone)] -pub(crate) struct TypecheckContext(Rc<Vec<(Label, CtxItem)>>); - -impl TypecheckContext { - pub fn new() -> Self { - TypecheckContext(Rc::new(Vec::new())) - } - pub fn insert_type(&self, x: &Label, t: Value) -> Self { - let mut vec = self.0.as_ref().clone(); - vec.push((x.clone(), CtxItem::Kept(x.into(), t.under_binder(x)))); - TypecheckContext(Rc::new(vec)) - } - pub fn insert_value(&self, x: &Label, e: Value) -> Result<Self, TypeError> { - let mut vec = self.0.as_ref().clone(); - vec.push((x.clone(), CtxItem::Replaced(e))); - Ok(TypecheckContext(Rc::new(vec))) - } - pub fn lookup(&self, var: &V<Label>) -> Option<Value> { - let mut var = var.clone(); - let mut shift_map: HashMap<Label, _> = HashMap::new(); - for (l, i) in self.0.iter().rev() { - match var.over_binder(l) { - None => { - let i = i.under_multiple_binders(&shift_map); - return Some(match i { - CtxItem::Kept(newvar, t) => { - Value::from_kind_and_type(ValueKind::Var(newvar), t) - } - CtxItem::Replaced(v) => v, - }); - } - Some(newvar) => var = newvar, - }; - if let CtxItem::Kept(_, _) = i { - *shift_map.entry(l.clone()).or_insert(0) += 1; - } - } - // Unbound variable - None - } - /// Given a var that makes sense in the current context, map the given function in such a way - /// that the passed variable always makes sense in the context of the passed item. - /// Once we pass the variable definition, the variable doesn't make sense anymore so we just - /// copy the remaining items. - fn do_with_var<E>( - &self, - var: &AlphaVar, - mut f: impl FnMut(&AlphaVar, &CtxItem) -> Result<CtxItem, E>, - ) -> Result<Self, E> { - let mut vec = Vec::new(); - vec.reserve(self.0.len()); - let mut var = var.clone(); - let mut iter = self.0.iter().rev(); - for (l, i) in iter.by_ref() { - vec.push((l.clone(), f(&var, i)?)); - if let CtxItem::Kept(_, _) = i { - match var.over_binder(l) { - None => break, - Some(newvar) => var = newvar, - }; - } - } - for (l, i) in iter { - vec.push((l.clone(), (*i).clone())); - } - vec.reverse(); - Ok(TypecheckContext(Rc::new(vec))) - } - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { - if delta < 0 { - Some(self.do_with_var(var, |var, i| Ok(i.shift(delta, &var)?))?) - } else { - Some(TypecheckContext(Rc::new( - self.0 - .iter() - .map(|(l, i)| Ok((l.clone(), i.shift(delta, &var)?))) - .collect::<Result<_, _>>()?, - ))) - } - } - fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { - self.do_with_var(var, |var, i| Ok::<_, !>(i.subst_shift(&var, val))) - .unwrap() - } -} - -impl Shift for CtxItem { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { - Some(match self { - CtxItem::Kept(v, t) => { - CtxItem::Kept(v.shift(delta, var)?, t.shift(delta, var)?) - } - CtxItem::Replaced(e) => CtxItem::Replaced(e.shift(delta, var)?), - }) - } -} - -impl Shift for TypecheckContext { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { - self.shift(delta, var) - } -} - -impl Subst<Value> for CtxItem { - fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { - match self { - CtxItem::Replaced(e) => CtxItem::Replaced(e.subst_shift(var, val)), - CtxItem::Kept(v, t) => match v.shift(-1, var) { - None => CtxItem::Replaced(val.clone()), - Some(newvar) => CtxItem::Kept(newvar, t.subst_shift(var, val)), - }, - } - } -} - -impl Subst<Value> for TypecheckContext { - fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { - self.subst_shift(var, val) - } -} - -/// Don't count contexts when comparing stuff. -/// This is dirty but needed. -impl PartialEq for TypecheckContext { - fn eq(&self, _: &Self) -> bool { - true - } -} -impl Eq for TypecheckContext {} |