From a24f2d1367b2848779014c7bb3ecfe6bfbcff7d7 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 24 Jan 2020 18:38:30 +0000 Subject: Fix some variable shifting failures --- dhall/src/semantics/phase/normalize.rs | 24 +++++++++++++++++++----- 1 file changed, 19 insertions(+), 5 deletions(-) (limited to 'dhall/src/semantics/phase') diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs index ac60ce0..3ddfb84 100644 --- a/dhall/src/semantics/phase/normalize.rs +++ b/dhall/src/semantics/phase/normalize.rs @@ -12,8 +12,8 @@ use crate::semantics::{ use crate::syntax; use crate::syntax::Const::Type; use crate::syntax::{ - BinOp, Builtin, ExprKind, InterpolatedText, InterpolatedTextContents, - Label, NaiveDouble, + BinOp, Builtin, Const, ExprKind, InterpolatedText, + InterpolatedTextContents, Label, NaiveDouble, }; // Ad-hoc macro to help construct closures @@ -822,7 +822,7 @@ pub(crate) fn normalize_whnf( } #[derive(Debug, Clone)] -enum NzEnvItem { +pub(crate) enum NzEnvItem { // Variable is bound with given type Kept(Value), // Variable has been replaced by corresponding value @@ -838,6 +838,9 @@ impl NzEnv { pub fn new() -> Self { NzEnv { items: Vec::new() } } + pub fn construct(items: Vec) -> Self { + NzEnv { items } + } pub fn insert_type(&self, t: Value) -> Self { let mut env = self.clone(); @@ -851,9 +854,16 @@ impl NzEnv { } pub fn lookup_val(&self, var: &AlphaVar) -> Value { let idx = self.items.len() - 1 - var.idx(); + let var_idx = self.items[..idx] + .iter() + .filter(|i| match i { + NzEnvItem::Kept(_) => true, + NzEnvItem::Replaced(_) => false, + }) + .count(); match &self.items[idx] { NzEnvItem::Kept(ty) => Value::from_kind_and_type_whnf( - ValueKind::Var(var.clone(), NzVar::new(idx)), + ValueKind::Var(var.clone(), NzVar::new(var_idx)), ty.clone(), ), NzEnvItem::Replaced(x) => x.clone(), @@ -863,7 +873,11 @@ impl NzEnv { /// Normalize a TyExpr into WHNF pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> Value { - let ty = tye.get_type().unwrap(); + let ty = match tye.get_type() { + Ok(ty) => ty, + Err(_) => return Value::from_const(Const::Sort), + }; + let kind = match tye.kind() { TyExprKind::Var(var) => return env.lookup_val(var), TyExprKind::Expr(ExprKind::Lam(binder, annot, body)) => { -- cgit v1.2.3