diff options
author | Nadrieril | 2019-04-22 00:07:50 +0200 |
---|---|---|
committer | Nadrieril | 2019-04-22 00:07:50 +0200 |
commit | 316c6ea1c5512bcc9e0a07aa63fd086eb313abc5 (patch) | |
tree | 36529717ff0e36a11a1397b171e5e3006dd18d14 /dhall/src/normalize.rs | |
parent | ecff0ecd47bb38937fb43e60b8d78ea92e2af01c (diff) |
Avoid shift_subst in typecheck
Diffstat (limited to 'dhall/src/normalize.rs')
-rw-r--r-- | dhall/src/normalize.rs | 16 |
1 files changed, 15 insertions, 1 deletions
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs index c17ed78..0301e35 100644 --- a/dhall/src/normalize.rs +++ b/dhall/src/normalize.rs @@ -18,6 +18,20 @@ impl<'a> Typed<'a> { pub fn normalize(self) -> Normalized<'a> { Normalized(normalize(self.0), self.1, self.2) } + pub fn normalize_ctx( + self, + ctx: &crate::typecheck::TypecheckContext, + ) -> Normalized<'a> { + Normalized( + normalize_whnf( + NormalizationContext::from_typecheck_ctx(ctx), + self.0, + ) + .normalize_to_expr(), + self.1, + self.2, + ) + } /// Pretends this expression is normalized. Use with care. #[allow(dead_code)] pub fn skip_normalize(self) -> Normalized<'a> { @@ -279,7 +293,7 @@ impl NormalizationContext { use crate::typecheck::EnvItem::*; let mut ctx = Context::new(); for (k, vs) in tc_ctx.0.iter_keys() { - for v in vs.iter().rev() { + for v in vs.iter() { let new_item = match v { Type(var, _) => EnvItem::Skip(var.clone()), Value(e) => EnvItem::Expr(normalize_whnf( |