From a030560e60c4ff1c724216f4a5640722eb89b227 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 27 Dec 2019 21:38:34 +0000 Subject: Use binder ids to reconstruct variables in expr output --- dhall/src/semantics/core/context.rs | 33 +++++++++++++++++++++++++++++++++ dhall/src/semantics/core/value.rs | 34 +++++++++++++--------------------- dhall/src/semantics/core/var.rs | 10 +++------- dhall/src/semantics/phase/mod.rs | 8 +------- dhall/src/semantics/to_expr.rs | 30 +++++++++++++++++++++++++----- 5 files changed, 75 insertions(+), 40 deletions(-) (limited to 'dhall/src/semantics') diff --git a/dhall/src/semantics/core/context.rs b/dhall/src/semantics/core/context.rs index 25e4037..826ba15 100644 --- a/dhall/src/semantics/core/context.rs +++ b/dhall/src/semantics/core/context.rs @@ -22,6 +22,11 @@ pub(crate) struct TyCtx { next_uid: Rc>, } +#[derive(Debug, Clone)] +pub(crate) struct VarCtx<'b> { + ctx: Vec<&'b Binder>, +} + impl TyCtx { pub fn new() -> Self { TyCtx { @@ -128,6 +133,34 @@ impl TyCtx { } } +impl<'b> VarCtx<'b> { + pub fn new() -> Self { + VarCtx { ctx: Vec::new() } + } + pub fn insert(&self, binder: &'b Binder) -> Self { + VarCtx { + ctx: self.ctx.iter().copied().chain(Some(binder)).collect(), + } + } + pub fn lookup(&self, binder: &Binder) -> Option { + self.ctx + .iter() + .rev() + .enumerate() + .find(|(_, other)| binder.same_binder(other)) + .map(|(i, _)| i) + } + pub fn lookup_by_name(&self, binder: &Binder) -> Option { + self.ctx + .iter() + .rev() + .filter(|other| binder.name() == other.name()) + .enumerate() + .find(|(_, other)| binder.same_binder(other)) + .map(|(i, _)| i) + } +} + impl Shift for CtxItem { fn shift(&self, delta: isize, var: &AlphaVar) -> Option { Some(match self { diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index f8146f5..26b8672 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -4,7 +4,7 @@ use std::collections::HashMap; use std::rc::Rc; use crate::error::{TypeError, TypeMessage}; -use crate::semantics::core::context::TyCtx; +use crate::semantics::core::context::{TyCtx, VarCtx}; use crate::semantics::core::var::{AlphaVar, Binder, Shift, Subst}; use crate::semantics::phase::normalize::{apply_any, normalize_whnf}; use crate::semantics::phase::typecheck::{builtin_to_value, const_to_value}; @@ -164,7 +164,7 @@ impl Value { &self, opts: to_expr::ToExprOptions, ) -> NormalizedExpr { - to_expr::value_to_expr(self, opts) + to_expr::value_to_expr(&VarCtx::new(), self, opts) } pub(crate) fn to_whnf_ignore_type(&self) -> ValueKind { self.as_whnf().clone() @@ -399,6 +399,7 @@ impl ValueKind { ) } + #[allow(dead_code)] pub(crate) fn map_ref<'a, V2>( &'a self, map_val: impl Fn(&'a V) -> V2, @@ -414,7 +415,7 @@ impl ValueKind { fn equiv(val1: &Value, val2: &Value) -> bool { struct ValueWithCtx<'v, 'c> { val: &'v Value, - ctx: Cow<'c, Vec<&'v Binder>>, + ctx: Cow<'c, VarCtx<'v>>, } impl<'v, 'c> PartialEq for ValueWithCtx<'v, 'c> { fn eq(&self, other: &ValueWithCtx<'v, 'c>) -> bool { @@ -423,8 +424,8 @@ fn equiv(val1: &Value, val2: &Value) -> bool { } // Push the given context into every subnode of the ValueKind. That way, normal equality of the // resulting value will take into account the context. - fn push_context<'v, 'c>( - ctx: &'c Vec<&'v Binder>, + fn push_context_through<'v, 'c>( + ctx: &'c VarCtx<'v>, kind: &'v ValueKind, ) -> ValueKind> { kind.map_ref_with_special_handling_of_binders( @@ -434,25 +435,15 @@ fn equiv(val1: &Value, val2: &Value) -> bool { }, |binder, val| ValueWithCtx { val, - ctx: Cow::Owned( - ctx.iter().cloned().chain(Some(binder)).collect(), - ), + ctx: Cow::Owned(ctx.insert(binder)), }, ) } - fn lookup(ctx: &Vec<&Binder>, binder: &Binder) -> Option { - ctx.iter() - .rev() - .enumerate() - .find(|(_, other)| binder.same_binder(other)) - .map(|(i, _)| i) - } - fn equiv_with_ctx<'v, 'c>( - ctx1: &'c Vec<&'v Binder>, + ctx1: &'c VarCtx<'v>, val1: &'v Value, - ctx2: &'c Vec<&'v Binder>, + ctx2: &'c VarCtx<'v>, val2: &'v Value, ) -> bool { use ValueKind::Var; @@ -465,16 +456,17 @@ fn equiv(val1: &Value, val2: &Value) -> bool { if b1.same_binder(&b2) { return true; } - match (lookup(ctx1, &b1), lookup(ctx2, &b2)) { + match (ctx1.lookup(&b1), ctx2.lookup(&b2)) { (Some(i), Some(j)) => i == j, _ => false, } } else { - push_context(ctx1, &*kind1) == push_context(ctx2, &*kind2) + push_context_through(ctx1, &*kind1) + == push_context_through(ctx2, &*kind2) } } - equiv_with_ctx(&Vec::new(), val1, &Vec::new(), val2) + equiv_with_ctx(&VarCtx::new(), val1, &VarCtx::new(), val2) } impl Shift for Value { diff --git a/dhall/src/semantics/core/var.rs b/dhall/src/semantics/core/var.rs index 4245e40..d21fa80 100644 --- a/dhall/src/semantics/core/var.rs +++ b/dhall/src/semantics/core/var.rs @@ -65,13 +65,6 @@ pub(crate) trait Subst { } impl AlphaVar { - pub(crate) fn to_var(&self, alpha: bool) -> V