diff options
| -rw-r--r-- | dhall/src/semantics/core/context.rs | 33 | ||||
| -rw-r--r-- | dhall/src/semantics/core/value.rs | 34 | ||||
| -rw-r--r-- | dhall/src/semantics/core/var.rs | 10 | ||||
| -rw-r--r-- | dhall/src/semantics/phase/mod.rs | 8 | ||||
| -rw-r--r-- | dhall/src/semantics/to_expr.rs | 30 |
5 files changed, 75 insertions, 40 deletions
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<RefCell<u64>>, } +#[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<usize> { + self.ctx + .iter() + .rev() + .enumerate() + .find(|(_, other)| binder.same_binder(other)) + .map(|(i, _)| i) + } + pub fn lookup_by_name(&self, binder: &Binder) -> Option<usize> { + 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<Self> { 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<Value> { self.as_whnf().clone() @@ -399,6 +399,7 @@ impl<V> ValueKind<V> { ) } + #[allow(dead_code)] pub(crate) fn map_ref<'a, V2>( &'a self, map_val: impl Fn(&'a V) -> V2, @@ -414,7 +415,7 @@ impl<V> ValueKind<V> { 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<Value>, ) -> ValueKind<ValueWithCtx<'v, 'c>> { 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<usize> { - 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<S> { } impl AlphaVar { - pub(crate) fn to_var(&self, alpha: bool) -> V<Label> { - if alpha { - V("_".into(), self.alpha.1) - } else { - self.normal.clone() - } - } pub(crate) fn binder(&self) -> Binder { Binder::new(self.normal.0.clone(), self.binder_uid) } @@ -81,6 +74,9 @@ impl Binder { pub(crate) fn new(name: Label, uid: BinderUID) -> Self { Binder { name, uid } } + pub(crate) fn name(&self) -> &Label { + &self.name + } pub(crate) fn same_binder(&self, other: &Binder) -> bool { self.uid == other.uid } diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs index 104a1ba..5d17338 100644 --- a/dhall/src/semantics/phase/mod.rs +++ b/dhall/src/semantics/phase/mod.rs @@ -4,7 +4,7 @@ use std::path::Path; use crate::error::{EncodeError, Error, ImportError, TypeError}; use crate::semantics::core::value::Value; use crate::semantics::core::value::ValueKind; -use crate::semantics::core::var::{AlphaVar, Shift, Subst}; +use crate::semantics::core::var::{AlphaVar, Shift}; use crate::semantics::to_expr::ToExprOptions; use crate::syntax::binary; use crate::syntax::{Builtin, Const, Expr}; @@ -203,12 +203,6 @@ impl Shift for Normalized { } } -impl Subst<Value> for Typed { - fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { - Typed(self.0.subst_shift(var, val)) - } -} - macro_rules! derive_traits_for_wrapper_struct { ($ty:ident) => { impl std::cmp::PartialEq for $ty { diff --git a/dhall/src/semantics/to_expr.rs b/dhall/src/semantics/to_expr.rs index 11e289f..1ece1cc 100644 --- a/dhall/src/semantics/to_expr.rs +++ b/dhall/src/semantics/to_expr.rs @@ -1,9 +1,9 @@ -use crate::semantics::core::value::Value; -use crate::semantics::core::value::ValueKind; +use crate::semantics::core::context::VarCtx; use crate::semantics::phase::typecheck::rc; use crate::semantics::phase::NormalizedExpr; +use crate::semantics::{Value, ValueKind}; use crate::syntax; -use crate::syntax::{Builtin, ExprKind}; +use crate::syntax::{Builtin, ExprKind, V}; /// Controls conversion from `Value` to `Expr` #[derive(Copy, Clone)] @@ -16,6 +16,7 @@ pub(crate) struct ToExprOptions { /// Converts a value back to the corresponding AST expression. pub(crate) fn value_to_expr( + ctx: &VarCtx, val: &Value, opts: ToExprOptions, ) -> NormalizedExpr { @@ -23,7 +24,27 @@ pub(crate) fn value_to_expr( val.normalize_whnf(); } - match val.as_kind().map_ref(|v| value_to_expr(v, opts)) { + let kind = val.as_kind(); + let kind = kind.map_ref_with_special_handling_of_binders( + |v| value_to_expr(ctx, v, opts), + |binder, v| value_to_expr(&ctx.insert(binder), v, opts), + ); + match kind { + ValueKind::Var(v) => { + let b = v.binder(); + let (idx, name) = if opts.alpha { + (ctx.lookup(&b), "_".into()) + } else { + (ctx.lookup_by_name(&b), b.name().clone()) + }; + match idx { + Some(idx) => rc(ExprKind::Var(V(name, idx))), + None => panic!( + "internal error: binder {:?} not found in environment", + b + ), + } + } ValueKind::Lam(x, t, e) => { rc(ExprKind::Lam(x.to_label_maybe_alpha(opts.alpha), t, e)) } @@ -33,7 +54,6 @@ pub(crate) fn value_to_expr( ValueKind::Pi(x, t, e) => { rc(ExprKind::Pi(x.to_label_maybe_alpha(opts.alpha), t, e)) } - ValueKind::Var(v) => rc(ExprKind::Var(v.to_var(opts.alpha))), ValueKind::Const(c) => rc(ExprKind::Const(c)), ValueKind::BoolLit(b) => rc(ExprKind::BoolLit(b)), ValueKind::NaturalLit(n) => rc(ExprKind::NaturalLit(n)), |