From 3182c121815857c0b2b3c057f1d2944c51332cdc Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 21 Jan 2020 18:51:00 +0000 Subject: Prepare Value for reverse variables I thought it would work ><. It's a bit too early --- dhall/src/semantics/core/context.rs | 10 ++++++++-- dhall/src/semantics/core/value.rs | 40 ++++++++++++++++++++++++------------- dhall/src/semantics/core/visitor.rs | 2 +- dhall/src/semantics/nze/mod.rs | 2 +- dhall/src/semantics/nze/nzexpr.rs | 14 ++++++++++++- 5 files changed, 49 insertions(+), 19 deletions(-) diff --git a/dhall/src/semantics/core/context.rs b/dhall/src/semantics/core/context.rs index 8c64c26..7972a20 100644 --- a/dhall/src/semantics/core/context.rs +++ b/dhall/src/semantics/core/context.rs @@ -2,6 +2,7 @@ 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::syntax::{Label, V}; #[derive(Debug, Clone)] @@ -42,7 +43,6 @@ impl TyCtx { let mut var = var.clone(); let mut shift_delta: isize = 0; let mut rev_ctx = self.ctx.iter().rev().map(|(b, i)| (b.to_label(), i)); - let found_item = loop { if let Some((label, item)) = rev_ctx.next() { var = match var.over_binder(&label) { @@ -57,10 +57,16 @@ impl TyCtx { return None; } }; + let var_idx = rev_ctx + .filter(|(_, i)| match i { + CtxItem::Kept(_) => true, + CtxItem::Replaced(_) => false, + }) + .count(); let v = match found_item { CtxItem::Kept(t) => Value::from_kind_and_type( - ValueKind::Var(AlphaVar::default()), + ValueKind::Var(AlphaVar::default(), NzVar::new(var_idx)), t.clone(), ), CtxItem::Replaced(v) => v.clone(), diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index dc6a116..a7c207d 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -4,6 +4,7 @@ use std::rc::Rc; use crate::error::{TypeError, TypeMessage}; use crate::semantics::core::var::{AlphaVar, Binder}; +use crate::semantics::nze::{NzVar, QuoteEnv}; use crate::semantics::phase::normalize::{apply_any, normalize_whnf}; use crate::semantics::phase::typecheck::{builtin_to_value, const_to_value}; use crate::semantics::phase::{ @@ -60,7 +61,7 @@ pub(crate) enum ValueKind { // Invariant: in whnf, the evaluation must not be able to progress further. AppliedBuiltin(Builtin, Vec), - Var(AlphaVar), + Var(AlphaVar, NzVar), Const(Const), BoolLit(bool), NaturalLit(Natural), @@ -167,7 +168,7 @@ impl Value { self.normalize_nf(); } - self.to_tyexpr().to_expr(opts) + self.to_tyexpr(QuoteEnv::new()).to_expr(opts) } pub(crate) fn to_whnf_ignore_type(&self) -> ValueKind { self.as_whnf().clone() @@ -257,7 +258,7 @@ impl Value { match &*self.as_kind() { // If the var matches, we can just reuse the provided value instead of copying it. // We also check that the types match, if in debug mode. - ValueKind::Var(v) if v == var => { + ValueKind::Var(v, _) if v == var => { if let Ok(self_ty) = self.get_type() { val.check_type(&self_ty.subst_shift(var, val)); } @@ -288,18 +289,27 @@ impl Value { // } // } - pub fn to_tyexpr(&self) -> TyExpr { + pub fn to_tyexpr(&self, qenv: QuoteEnv) -> TyExpr { let self_kind = self.as_kind(); let self_ty = self.as_internal().ty.clone(); let self_span = self.as_internal().span.clone(); - if let ValueKind::Var(v) = &*self_kind { - return TyExpr::new(TyExprKind::Var(*v), self_ty, self_span); + if let ValueKind::Var(v, _w) = &*self_kind { + return TyExpr::new( + // TODO: Only works when we don't normalize under lambdas + // TyExprKind::Var(qenv.lookup(w)), + TyExprKind::Var(*v), + self_ty, + self_span, + ); } // TODO: properly recover intermediate types; `None` is a time-bomb here. - let self_kind = self_kind.map_ref(|v| v.to_tyexpr()); + let self_kind = self_kind.map_ref_with_special_handling_of_binders( + |v| v.to_tyexpr(qenv), + |_, _, v| v.to_tyexpr(qenv.insert()), + ); let expr = match self_kind { - ValueKind::Var(_) => unreachable!(), + ValueKind::Var(..) => unreachable!(), ValueKind::Lam(x, t, e) => ExprKind::Lam(x.to_label(), t, e), ValueKind::Pi(x, t, e) => ExprKind::Pi(x.to_label(), t, e), ValueKind::AppliedBuiltin(b, args) => { @@ -320,13 +330,13 @@ impl Value { ValueKind::IntegerLit(n) => ExprKind::IntegerLit(n), ValueKind::DoubleLit(n) => ExprKind::DoubleLit(n), ValueKind::EmptyOptionalLit(n) => ExprKind::App( - builtin_to_value(Builtin::OptionalNone).to_tyexpr(), + builtin_to_value(Builtin::OptionalNone).to_tyexpr(qenv), n, ), ValueKind::NEOptionalLit(n) => ExprKind::SomeLit(n), ValueKind::EmptyListLit(n) => ExprKind::EmptyListLit(TyExpr::new( TyExprKind::Expr(ExprKind::App( - builtin_to_value(Builtin::List).to_tyexpr(), + builtin_to_value(Builtin::List).to_tyexpr(qenv), n, )), Some(const_to_value(Const::Type)), @@ -470,7 +480,7 @@ impl ValueKind { pub(crate) fn normalize_mut(&mut self) { match self { - ValueKind::Var(_) + ValueKind::Var(..) | ValueKind::Const(_) | ValueKind::BoolLit(_) | ValueKind::NaturalLit(_) @@ -545,7 +555,7 @@ impl ValueKind { fn shift(&self, delta: isize, var: &AlphaVar) -> Option { Some(match self { - ValueKind::Var(v) => ValueKind::Var(v.shift(delta, var)?), + 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())?), @@ -554,8 +564,10 @@ impl ValueKind { } fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { match self { - ValueKind::Var(v) if v == var => val.to_whnf_ignore_type(), - ValueKind::Var(v) => ValueKind::Var(v.shift(-1, var).unwrap()), + ValueKind::Var(v, _) if v == var => val.to_whnf_ignore_type(), + ValueKind::Var(v, w) => { + ValueKind::Var(v.shift(-1, var).unwrap(), *w) + } _ => self.map_ref_with_special_handling_of_binders( |x| x.subst_shift(var, val), |_, _, x| { diff --git a/dhall/src/semantics/core/visitor.rs b/dhall/src/semantics/core/visitor.rs index a449f6c..5a04747 100644 --- a/dhall/src/semantics/core/visitor.rs +++ b/dhall/src/semantics/core/visitor.rs @@ -81,7 +81,7 @@ where Pi(l.clone(), t, e) } AppliedBuiltin(b, xs) => AppliedBuiltin(*b, v.visit_vec(xs)?), - Var(v) => Var(v.clone()), + Var(v, w) => Var(v.clone(), *w), Const(k) => Const(*k), BoolLit(b) => BoolLit(*b), NaturalLit(n) => NaturalLit(*n), diff --git a/dhall/src/semantics/nze/mod.rs b/dhall/src/semantics/nze/mod.rs index ef8918f..213404c 100644 --- a/dhall/src/semantics/nze/mod.rs +++ b/dhall/src/semantics/nze/mod.rs @@ -1,2 +1,2 @@ pub mod nzexpr; -// pub(crate) use nzexpr::*; +pub(crate) use nzexpr::*; diff --git a/dhall/src/semantics/nze/nzexpr.rs b/dhall/src/semantics/nze/nzexpr.rs index 3a5a1f9..1256ea0 100644 --- a/dhall/src/semantics/nze/nzexpr.rs +++ b/dhall/src/semantics/nze/nzexpr.rs @@ -82,10 +82,16 @@ pub(crate) struct QuoteEnv { } // Reverse-debruijn index: counts number of binders from the bottom of the stack. -#[derive(Debug, Clone, Copy)] +#[derive(Debug, Clone, Copy, Eq)] pub(crate) struct NzVar { idx: usize, } +// TODO: temporary hopefully +impl std::cmp::PartialEq for NzVar { + fn eq(&self, _other: &Self) -> bool { + true + } +} impl TyEnv { pub fn new() -> Self { @@ -219,6 +225,12 @@ impl QuoteEnv { } } +impl NzVar { + pub fn new(idx: usize) -> Self { + NzVar { idx } + } +} + impl TyExpr { pub fn new(kind: TyExprKind, ty: Option) -> Self { TyExpr { -- cgit v1.2.3