diff options
Diffstat (limited to '')
-rw-r--r-- | dhall/src/semantics/core/context.rs | 95 |
1 files changed, 0 insertions, 95 deletions
diff --git a/dhall/src/semantics/core/context.rs b/dhall/src/semantics/core/context.rs index 9749c50..8b13789 100644 --- a/dhall/src/semantics/core/context.rs +++ b/dhall/src/semantics/core/context.rs @@ -1,96 +1 @@ -use crate::error::TypeError; -use crate::semantics::core::value::Value; -use crate::semantics::core::value::ValueKind; -use crate::semantics::core::var::{AlphaVar, Binder}; -use crate::semantics::nze::NzVar; -// use crate::semantics::phase::normalize::{NzEnv, NzEnvItem}; -use crate::syntax::{Label, V}; -#[derive(Debug, Clone)] -enum CtxItem { - // Variable is bound with given type - Kept(Value), - // Variable has been replaced by corresponding value - Replaced(Value), -} - -#[derive(Debug, Clone)] -pub(crate) struct TyCtx { - ctx: Vec<(Binder, CtxItem)>, -} - -impl TyCtx { - pub fn new() -> Self { - TyCtx { ctx: Vec::new() } - } - fn with_vec(&self, vec: Vec<(Binder, CtxItem)>) -> Self { - TyCtx { ctx: vec } - } - pub fn insert_type(&self, x: &Binder, t: Value) -> Self { - let mut vec = self.ctx.clone(); - vec.push((x.clone(), CtxItem::Kept(t.under_binder()))); - self.with_vec(vec) - } - pub fn insert_value( - &self, - x: &Binder, - e: Value, - ) -> Result<Self, TypeError> { - let mut vec = self.ctx.clone(); - vec.push((x.clone(), CtxItem::Replaced(e))); - Ok(self.with_vec(vec)) - } - pub fn lookup(&self, var: &V<Label>) -> Option<Value> { - let mut var = var.clone(); - let mut shift_delta: isize = 0; - let mut rev_ctx = self.ctx.iter().rev().map(|(b, i)| (b.to_label(), i)); - let found_item = loop { - if let Some((label, item)) = rev_ctx.next() { - var = match var.over_binder(&label) { - Some(newvar) => newvar, - None => break item, - }; - if let CtxItem::Kept(_) = item { - shift_delta += 1; - } - } else { - // Unbound variable - return None; - } - }; - let var_idx = rev_ctx - .filter(|(_, i)| match i { - CtxItem::Kept(_) => true, - CtxItem::Replaced(_) => false, - }) - .count(); - - let v = match found_item { - CtxItem::Kept(t) => Value::from_kind_and_type( - ValueKind::Var(AlphaVar::default(), NzVar::new(var_idx)), - t.clone(), - ), - CtxItem::Replaced(v) => v.clone() - // .normalize_whnf(&NzEnv::construct( - // self.ctx - // .iter() - // .filter_map(|(_, i)| match i { - // CtxItem::Kept(t) => { - // Some(NzEnvItem::Kept(t.clone())) - // } - // CtxItem::Replaced(_) => None, - // }) - // .collect(), - // )), - }; - // Can't fail because delta is positive - let v = v.shift(shift_delta, &AlphaVar::default()).unwrap(); - return Some(v); - } - // pub fn lookup_alpha(&self, var: &AlphaVar) -> Option<Value> { - // self.lookup(&var.normal) - // } - pub fn new_binder(&self, l: &Label) -> Binder { - Binder::new(l.clone()) - } -} |