diff options
Diffstat (limited to 'dhall/src/semantics/core')
| -rw-r--r-- | dhall/src/semantics/core/context.rs | 17 | ||||
| -rw-r--r-- | dhall/src/semantics/core/value.rs | 18 |
2 files changed, 26 insertions, 9 deletions
diff --git a/dhall/src/semantics/core/context.rs b/dhall/src/semantics/core/context.rs index 7972a20..0e62fef 100644 --- a/dhall/src/semantics/core/context.rs +++ b/dhall/src/semantics/core/context.rs @@ -2,7 +2,8 @@ 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::nze::{NzVar, QuoteEnv}; +use crate::semantics::phase::normalize::{NzEnv, NzEnvItem}; use crate::syntax::{Label, V}; #[derive(Debug, Clone)] @@ -69,7 +70,19 @@ impl TyCtx { ValueKind::Var(AlphaVar::default(), NzVar::new(var_idx)), t.clone(), ), - CtxItem::Replaced(v) => v.clone(), + CtxItem::Replaced(v) => v.clone() + // .to_tyexpr(QuoteEnv::construct(var_idx)) + // .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(); diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index 96bb99a..11d8bd8 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -185,7 +185,7 @@ impl Value { self.normalize_nf(); } - self.to_tyexpr(QuoteEnv::new()).to_expr(opts) + self.to_tyexpr_noenv().to_expr(opts) } pub(crate) fn to_whnf_ignore_type(&self) -> ValueKind<Value> { self.as_whnf().clone() @@ -292,11 +292,9 @@ impl Value { pub fn to_tyexpr(&self, qenv: QuoteEnv) -> TyExpr { let tye = match &*self.as_kind() { - ValueKind::Var(v, _w) => { - TyExprKind::Var(*v) - // TODO: Only works when we don't normalize under lambdas - // TyExprKind::Var(qenv.lookup(w)) - } + // ValueKind::Var(v, _w) => TyExprKind::Var(*v), + // TODO: Only works when we don't normalize under lambdas + ValueKind::Var(_v, w) => TyExprKind::Var(qenv.lookup(w)), ValueKind::LamClosure { binder, annot, @@ -611,7 +609,13 @@ impl ValueKind<Value> { fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> { Some(match self { - ValueKind::Var(v, w) => ValueKind::Var(v.shift(delta, var)?, *w), + ValueKind::Var(v, w) if var.idx() <= v.idx() => { + ValueKind::Var(v.shift(delta, var)?, *w) + } + ValueKind::Var(v, w) => { + ValueKind::Var(v.shift(delta, var)?, w.shift(delta)) + } + // ValueKind::Var(v, w) => ValueKind::Var(v.shift(delta, var)?, *w), _ => self.traverse_ref_with_special_handling_of_binders( |x| Ok(x.shift(delta, var)?), |_, _, x| Ok(x.shift(delta, &var.under_binder())?), |