From ab672506fd45e33f60b1b962c4757f912b6e27be Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Fri, 17 Jan 2020 18:31:45 +0000
Subject: Use alpha variables everywhere

Don't bother keeping name around, it complicates matters
---
 dhall/src/semantics/core/value.rs |  2 +-
 dhall/src/semantics/core/var.rs   | 30 +++++++++---------------------
 dhall/src/semantics/to_expr.rs    | 29 ++++++++++++++++++++++++-----
 3 files changed, 34 insertions(+), 27 deletions(-)

(limited to 'dhall')

diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs
index 5aa337d..d843a1b 100644
--- a/dhall/src/semantics/core/value.rs
+++ b/dhall/src/semantics/core/value.rs
@@ -163,7 +163,7 @@ impl Value {
         &self,
         opts: to_expr::ToExprOptions,
     ) -> NormalizedExpr {
-        to_expr::value_to_expr(self, opts)
+        to_expr::value_to_expr(self, opts, &vec![])
     }
     pub(crate) fn to_whnf_ignore_type(&self) -> ValueKind<Value> {
         self.as_whnf().clone()
diff --git a/dhall/src/semantics/core/var.rs b/dhall/src/semantics/core/var.rs
index d7666e3..f3475e7 100644
--- a/dhall/src/semantics/core/var.rs
+++ b/dhall/src/semantics/core/var.rs
@@ -2,12 +2,9 @@ use std::collections::HashMap;
 
 use crate::syntax::{Label, V};
 
-/// Stores a pair of variables: a normal one and one
-/// that corresponds to the alpha-normalized version of the first one.
-/// Equality is up to alpha-equivalence (compares on the second one only).
+/// Stores an alpha-normalized variable.
 #[derive(Clone, Eq)]
 pub struct AlphaVar {
-    normal: V<Label>,
     alpha: V<()>,
 }
 
@@ -19,17 +16,12 @@ pub struct Binder {
 }
 
 impl AlphaVar {
-    pub(crate) fn to_var_maybe_alpha(&self, alpha: bool) -> V<Label> {
-        if alpha {
-            V("_".into(), self.alpha.idx())
-        } else {
-            self.normal.clone()
-        }
+    pub(crate) fn idx(&self) -> usize {
+        self.alpha.idx()
     }
 
     pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
         Some(AlphaVar {
-            normal: self.normal.shift(delta, &var.normal)?,
             alpha: self.alpha.shift(delta, &var.alpha)?,
         })
     }
@@ -48,7 +40,6 @@ impl AlphaVar {
         shift_map: &HashMap<Label, usize>,
     ) -> Self {
         AlphaVar {
-            normal: self.normal.under_multiple_binders(shift_map),
             alpha: self.alpha.under_multiple_binders(shift_map),
         }
     }
@@ -68,6 +59,9 @@ impl Binder {
     pub(crate) fn to_label(&self) -> Label {
         self.clone().into()
     }
+    pub(crate) fn name(&self) -> &Label {
+        &self.name
+    }
 }
 
 /// Equality up to alpha-equivalence
@@ -85,7 +79,7 @@ impl std::cmp::PartialEq for Binder {
 
 impl std::fmt::Debug for AlphaVar {
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
-        write!(f, "AlphaVar({}, {})", self.normal, self.alpha.1)
+        write!(f, "AlphaVar({})", self.alpha.1)
     }
 }
 
@@ -97,18 +91,12 @@ impl std::fmt::Debug for Binder {
 
 impl<'a> From<&'a Label> for AlphaVar {
     fn from(x: &'a Label) -> AlphaVar {
-        AlphaVar {
-            normal: V(x.clone(), 0),
-            alpha: V((), 0),
-        }
+        AlphaVar { alpha: V((), 0) }
     }
 }
 impl From<Binder> for AlphaVar {
     fn from(x: Binder) -> AlphaVar {
-        AlphaVar {
-            normal: V(x.into(), 0),
-            alpha: V((), 0),
-        }
+        AlphaVar { alpha: V((), 0) }
     }
 }
 impl<'a> From<&'a Binder> for AlphaVar {
diff --git a/dhall/src/semantics/to_expr.rs b/dhall/src/semantics/to_expr.rs
index 1adfd49..612f794 100644
--- a/dhall/src/semantics/to_expr.rs
+++ b/dhall/src/semantics/to_expr.rs
@@ -1,8 +1,9 @@
+use crate::semantics::core::var::Binder;
 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)]
@@ -14,19 +15,37 @@ pub(crate) struct ToExprOptions {
 }
 
 /// Converts a value back to the corresponding AST expression.
-pub(crate) fn value_to_expr(
-    val: &Value,
+pub(crate) fn value_to_expr<'a>(
+    val: &'a Value,
     opts: ToExprOptions,
+    ctx: &Vec<&'a Binder>,
 ) -> NormalizedExpr {
     if opts.normalize {
         val.normalize_whnf();
     }
 
     let kind = val.as_kind();
-    let kind = kind.map_ref(|v| value_to_expr(v, opts));
+    let kind = kind.map_ref_with_special_handling_of_binders(
+        |v| value_to_expr(v, opts, ctx),
+        |b, _, v| {
+            let mut ctx = ctx.clone();
+            ctx.push(b);
+            value_to_expr(v, opts, &ctx)
+        },
+    );
     match kind {
+        ValueKind::Var(v) if opts.alpha => {
+            rc(ExprKind::Var(V("_".into(), v.idx())))
+        }
         ValueKind::Var(v) => {
-            rc(ExprKind::Var(v.to_var_maybe_alpha(opts.alpha)))
+            let name = ctx[ctx.len() - 1 - v.idx()].to_label();
+            let mut idx = 0;
+            for b in ctx.iter().rev().take(v.idx()) {
+                if b.name() == &name {
+                    idx += 1;
+                }
+            }
+            rc(ExprKind::Var(V(name, idx)))
         }
         ValueKind::Lam(x, t, e) => {
             rc(ExprKind::Lam(x.to_label_maybe_alpha(opts.alpha), t, e))
-- 
cgit v1.2.3