diff options
Diffstat (limited to 'dhall/src')
| -rw-r--r-- | dhall/src/semantics/core/context.rs | 17 | ||||
| -rw-r--r-- | dhall/src/semantics/core/value.rs | 18 | ||||
| -rw-r--r-- | dhall/src/semantics/nze/nzexpr.rs | 8 | ||||
| -rw-r--r-- | dhall/src/semantics/phase/normalize.rs | 24 |
4 files changed, 53 insertions, 14 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())?), 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)) => { |