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/var.rs | 103 ++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 103 insertions(+)
 create mode 100644 dhall/src/core/var.rs

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

diff --git a/dhall/src/core/var.rs b/dhall/src/core/var.rs
new file mode 100644
index 0000000..e431fc2
--- /dev/null
+++ b/dhall/src/core/var.rs
@@ -0,0 +1,103 @@
+use dhall_syntax::{Label, V};
+
+/// 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);
+
+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 {
+    pub(crate) fn to_label_maybe_alpha(&self, alpha: bool) -> Label {
+        if alpha {
+            "_".into()
+        } else {
+            self.to_label()
+        }
+    }
+    pub(crate) fn to_label(&self) -> Label {
+        self.clone().into()
+    }
+}
+
+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