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/core/context.rs | 17 +++++++++++++++--
dhall/src/semantics/core/value.rs | 18 +++++++++++-------
dhall/src/semantics/nze/nzexpr.rs | 8 ++++++++
dhall/src/semantics/phase/normalize.rs | 24 +++++++++++++++++++-----
4 files changed, 53 insertions(+), 14 deletions(-)
(limited to 'dhall/src/semantics')
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())?),
diff --git a/dhall/src/semantics/nze/nzexpr.rs b/dhall/src/semantics/nze/nzexpr.rs
index 723c895..49aa704 100644
--- a/dhall/src/semantics/nze/nzexpr.rs
+++ b/dhall/src/semantics/nze/nzexpr.rs
@@ -217,6 +217,9 @@ impl QuoteEnv {
pub fn new() -> Self {
QuoteEnv { size: 0 }
}
+ pub fn construct(size: usize) -> Self {
+ QuoteEnv { size }
+ }
pub fn insert(&self) -> Self {
QuoteEnv {
size: self.size + 1,
@@ -231,6 +234,11 @@ impl NzVar {
pub fn new(idx: usize) -> Self {
NzVar { idx }
}
+ pub fn shift(&self, delta: isize) -> Self {
+ NzVar {
+ idx: (self.idx as isize + delta) as usize,
+ }
+ }
}
impl TyExpr {
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<NzEnvItem>) -> 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