From 8cb3046e0920bf24d66c578b1a2b184c741b73fe Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Tue, 7 May 2019 18:23:07 +0200
Subject: Move AlphaVar and AlphaLabel into a new module

---
 dhall/src/core/value.rs | 105 +-----------------------------------------------
 1 file changed, 2 insertions(+), 103 deletions(-)

(limited to 'dhall/src/core/value.rs')

diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index 28fcb3e..4c71778 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -3,29 +3,16 @@ use std::collections::BTreeMap;
 use dhall_proc_macros as dhall;
 use dhall_syntax::{
     rc, Builtin, Const, ExprF, Integer, InterpolatedTextContents, Label,
-    Natural, V, X,
+    Natural, X,
 };
 
 use crate::core::thunk::{Thunk, TypeThunk};
+use crate::core::var::{AlphaLabel, AlphaVar};
 use crate::phase::normalize::{
     apply_builtin, normalize_one_layer, squash_textlit, OutputSubExpr,
 };
 use crate::phase::Typed;
 
-/// Stores a pair of variables: a normal one and if relevant one
-/// that corresponds to the alpha-normalized version of the first one.
-/// Equality is up to alpha-equivalence.
-#[derive(Debug, Clone, Eq)]
-pub(crate) struct AlphaVar {
-    normal: V<Label>,
-    alpha: Option<V<()>>,
-}
-
-// Exactly like a Label, but equality returns always true.
-// This is so that Value equality is exactly alpha-equivalence.
-#[derive(Debug, Clone, Eq)]
-pub(crate) struct AlphaLabel(Label);
-
 /// A semantic value. The invariants ensure this value represents a Weak-Head
 /// Normal Form (WHNF). This means that this first constructor is the first constructor of the
 /// final Normal Form (NF).
@@ -73,43 +60,6 @@ pub(crate) enum Value {
     PartialExpr(ExprF<Thunk, Label, X>),
 }
 
-impl AlphaVar {
-    pub(crate) fn to_var(&self, alpha: bool) -> V<Label> {
-        match (alpha, &self.alpha) {
-            (true, Some(x)) => V("_".into(), x.1),
-            _ => self.normal.clone(),
-        }
-    }
-    pub(crate) fn from_var(normal: V<Label>) -> Self {
-        AlphaVar {
-            normal,
-            alpha: None,
-        }
-    }
-    pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
-        AlphaVar {
-            normal: self.normal.shift(delta, &var.normal),
-            alpha: match (&self.alpha, &var.alpha) {
-                (Some(x), Some(v)) => Some(x.shift(delta, v)),
-                _ => None,
-            },
-        }
-    }
-}
-
-impl AlphaLabel {
-    fn to_label_maybe_alpha(&self, alpha: bool) -> Label {
-        if alpha {
-            "_".into()
-        } else {
-            self.to_label()
-        }
-    }
-    fn to_label(&self) -> Label {
-        self.clone().into()
-    }
-}
-
 impl Value {
     pub(crate) fn into_thunk(self) -> Thunk {
         Thunk::from_value(self)
@@ -574,54 +524,3 @@ impl Value {
         }
     }
 }
-
-impl std::cmp::PartialEq for AlphaVar {
-    fn eq(&self, other: &Self) -> bool {
-        match (&self.alpha, &other.alpha) {
-            (Some(x), Some(y)) => x == y,
-            (None, None) => self.normal == other.normal,
-            _ => false,
-        }
-    }
-}
-impl std::cmp::PartialEq for AlphaLabel {
-    fn eq(&self, _other: &Self) -> bool {
-        true
-    }
-}
-
-impl From<Label> for AlphaVar {
-    fn from(x: Label) -> AlphaVar {
-        AlphaVar {
-            normal: V(x, 0),
-            alpha: Some(V((), 0)),
-        }
-    }
-}
-impl<'a> From<&'a Label> for AlphaVar {
-    fn from(x: &'a Label) -> AlphaVar {
-        x.clone().into()
-    }
-}
-impl From<AlphaLabel> for AlphaVar {
-    fn from(x: AlphaLabel) -> AlphaVar {
-        let l: Label = x.into();
-        l.into()
-    }
-}
-impl<'a> From<&'a AlphaLabel> for AlphaVar {
-    fn from(x: &'a AlphaLabel) -> AlphaVar {
-        x.clone().into()
-    }
-}
-
-impl From<Label> for AlphaLabel {
-    fn from(x: Label) -> AlphaLabel {
-        AlphaLabel(x)
-    }
-}
-impl From<AlphaLabel> for Label {
-    fn from(x: AlphaLabel) -> Label {
-        x.0
-    }
-}
-- 
cgit v1.2.3