diff options
author | Nadrieril | 2019-05-07 21:53:00 +0200 |
---|---|---|
committer | Nadrieril | 2019-05-07 21:53:00 +0200 |
commit | e3054cbbeb84bbaec626689c53584e54ca515d3e (patch) | |
tree | 72924a3e88e12e55dd6b3ab5ffcbe58a272a2c1c /dhall/src/core/context.rs | |
parent | 372c78ab875c8aa1e967ffb594f26df8beb43bea (diff) |
Don't discard normalization work done by typechecking
Diffstat (limited to 'dhall/src/core/context.rs')
-rw-r--r-- | dhall/src/core/context.rs | 33 |
1 files changed, 8 insertions, 25 deletions
diff --git a/dhall/src/core/context.rs b/dhall/src/core/context.rs index aeec7fb..56dec03 100644 --- a/dhall/src/core/context.rs +++ b/dhall/src/core/context.rs @@ -1,4 +1,3 @@ -use std::borrow::Cow; use std::rc::Rc; use dhall_syntax::context::Context as SimpleContext; @@ -25,28 +24,10 @@ pub(crate) struct NormalizationContext(Context<()>); #[derive(Debug, Clone)] pub(crate) struct TypecheckContext(Context<Type>); -impl<T> CtxItem<T> { - fn forget(&self) -> CtxItem<()> { - match self { - CtxItem::Kept(var, _) => CtxItem::Kept(var.clone(), ()), - CtxItem::Replaced(e, _) => CtxItem::Replaced(e.clone(), ()), - } - } -} - impl<T> Context<T> { pub(crate) fn new() -> Self { Context(Rc::new(SimpleContext::new())) } - pub(crate) fn forget(&self) -> Context<()> { - let mut ctx = SimpleContext::new(); - for (k, vs) in self.0.iter_keys() { - for v in vs.iter() { - ctx = ctx.insert(k.clone(), v.forget()); - } - } - Context(Rc::new(ctx)) - } pub(crate) fn insert_kept(&self, x: &Label, t: T) -> Self where T: Shift + Clone, @@ -103,16 +84,18 @@ impl TypecheckContext { e.get_type()?.into_owned(), ))) } - pub(crate) fn lookup(&self, var: &V<Label>) -> Option<Cow<'_, Type>> { + pub(crate) fn lookup(&self, var: &V<Label>) -> Option<Typed> { match self.0.lookup(var) { - Some(CtxItem::Kept(_, t)) => Some(Cow::Borrowed(&t)), - Some(CtxItem::Replaced(_, t)) => Some(Cow::Borrowed(&t)), + Some(CtxItem::Kept(newvar, t)) => Some(Typed::from_thunk_and_type( + Thunk::from_value(Value::Var(newvar.clone())), + t.clone(), + )), + Some(CtxItem::Replaced(th, t)) => { + Some(Typed::from_thunk_and_type(th.clone(), t.clone())) + } None => None, } } - pub(crate) fn to_normalization_ctx(&self) -> NormalizationContext { - NormalizationContext(self.0.forget()) - } } impl<T: Shift> Shift for CtxItem<T> { |