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<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)),
-- 
cgit v1.2.3