diff options
Diffstat (limited to '')
| -rw-r--r-- | dhall/src/core/context.rs | 113 |
1 files changed, 38 insertions, 75 deletions
diff --git a/dhall/src/core/context.rs b/dhall/src/core/context.rs index 3c07c1c..36542d2 100644 --- a/dhall/src/core/context.rs +++ b/dhall/src/core/context.rs @@ -10,46 +10,46 @@ use crate::error::TypeError; use crate::phase::{Type, Typed}; #[derive(Debug, Clone)] -enum CtxItem<T> { - Kept(AlphaVar, T), - Replaced(Thunk, T), +enum CtxItem { + Kept(AlphaVar, Type), + Replaced(Thunk, Type), } #[derive(Debug, Clone)] -struct Context<T>(Rc<Vec<(Label, CtxItem<T>)>>); +pub(crate) struct TypecheckContext(Rc<Vec<(Label, CtxItem)>>); -#[derive(Debug, Clone)] -pub(crate) struct TypecheckContext(Context<Type>); - -impl<T> Context<T> { +impl TypecheckContext { pub fn new() -> Self { - Context(Rc::new(Vec::new())) + TypecheckContext(Rc::new(Vec::new())) } - pub fn insert_kept(&self, x: &Label, t: T) -> Self - where - T: Shift + Clone, - { + pub fn insert_type(&self, x: &Label, t: Type) -> Self { let mut vec = self.0.as_ref().clone(); vec.push((x.clone(), CtxItem::Kept(x.into(), t.under_binder(x)))); - Context(Rc::new(vec)) + TypecheckContext(Rc::new(vec)) } - pub fn insert_replaced(&self, x: &Label, th: Thunk, t: T) -> Self - where - T: Clone, - { + pub fn insert_value(&self, x: &Label, e: Typed) -> Result<Self, TypeError> { let mut vec = self.0.as_ref().clone(); - vec.push((x.clone(), CtxItem::Replaced(th, t))); - Context(Rc::new(vec)) + vec.push(( + x.clone(), + CtxItem::Replaced(e.to_thunk(), e.get_type()?.into_owned()), + )); + Ok(TypecheckContext(Rc::new(vec))) } - pub fn lookup(&self, var: &V<Label>) -> Result<CtxItem<T>, V<Label>> - where - T: Clone + Shift, - { + pub fn lookup(&self, var: &V<Label>) -> Option<Typed> { 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 => return Ok(i.under_multiple_binders(&shift_map)), + None => { + let i = i.under_multiple_binders(&shift_map); + let (th, t) = match i { + CtxItem::Kept(newvar, t) => { + (Value::Var(newvar).into_thunk(), t) + } + CtxItem::Replaced(th, t) => (th, t), + }; + return Some(Typed::from_thunk_and_type(th, t)); + } Some(newvar) => var = newvar, }; if let CtxItem::Kept(_, _) = i { @@ -57,7 +57,7 @@ impl<T> Context<T> { } } // Free variable - Err(var) + 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. @@ -66,11 +66,8 @@ impl<T> Context<T> { fn do_with_var<E>( &self, var: &AlphaVar, - mut f: impl FnMut(&AlphaVar, &CtxItem<T>) -> Result<CtxItem<T>, E>, - ) -> Result<Self, E> - where - T: Clone, - { + 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(); @@ -88,16 +85,13 @@ impl<T> Context<T> { vec.push((l.clone(), (*i).clone())); } vec.reverse(); - Ok(Context(Rc::new(vec))) + Ok(TypecheckContext(Rc::new(vec))) } - fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> - where - T: Clone + Shift, - { + 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(Context(Rc::new( + Some(TypecheckContext(Rc::new( self.0 .iter() .map(|(l, i)| Ok((l.clone(), i.shift(delta, &var)?))) @@ -105,44 +99,13 @@ impl<T> Context<T> { ))) } } - fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self - where - T: Clone + Subst<Typed>, - { + fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { self.do_with_var(var, |var, i| Ok::<_, !>(i.subst_shift(&var, val))) .unwrap() } } -impl TypecheckContext { - pub fn new() -> Self { - TypecheckContext(Context::new()) - } - pub fn insert_type(&self, x: &Label, t: Type) -> Self { - TypecheckContext(self.0.insert_kept(x, t)) - } - pub fn insert_value(&self, x: &Label, e: Typed) -> Result<Self, TypeError> { - Ok(TypecheckContext(self.0.insert_replaced( - x, - e.to_thunk(), - e.get_type()?.into_owned(), - ))) - } - pub fn lookup(&self, var: &V<Label>) -> Option<Typed> { - match self.0.lookup(var) { - Ok(CtxItem::Kept(newvar, t)) => Some(Typed::from_thunk_and_type( - Thunk::from_value(Value::Var(newvar.clone())), - t.clone(), - )), - Ok(CtxItem::Replaced(th, t)) => { - Some(Typed::from_thunk_and_type(th.clone(), t.clone())) - } - Err(_) => None, - } - } -} - -impl<T: Shift> Shift for CtxItem<T> { +impl Shift for CtxItem { fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { Some(match self { CtxItem::Kept(v, t) => { @@ -155,13 +118,13 @@ impl<T: Shift> Shift for CtxItem<T> { } } -impl<T: Clone + Shift> Shift for Context<T> { +impl Shift for TypecheckContext { fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { self.shift(delta, var) } } -impl<T: Subst<Typed>> Subst<Typed> for CtxItem<T> { +impl Subst<Typed> for CtxItem { fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { match self { CtxItem::Replaced(e, t) => CtxItem::Replaced( @@ -178,16 +141,16 @@ impl<T: Subst<Typed>> Subst<Typed> for CtxItem<T> { } } -impl<T: Clone + Subst<Typed>> Subst<Typed> for Context<T> { +impl Subst<Typed> for TypecheckContext { fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> 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 { - // don't count contexts when comparing stuff - // this is dirty but needed for now true } } |