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/to_expr.rs | 29 ++++++++++++++++++++++++-----
 1 file changed, 24 insertions(+), 5 deletions(-)

(limited to 'dhall/src/semantics/to_expr.rs')

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