summaryrefslogtreecommitdiff
path: root/dhall/src/semantics
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/src/semantics/core/context.rs33
-rw-r--r--dhall/src/semantics/core/value.rs34
-rw-r--r--dhall/src/semantics/core/var.rs10
-rw-r--r--dhall/src/semantics/phase/mod.rs8
-rw-r--r--dhall/src/semantics/to_expr.rs30
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)),
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-28 13:11:27 +0000