diff options
Diffstat (limited to 'dhall/src/core/value.rs')
-rw-r--r-- | dhall/src/core/value.rs | 105 |
1 files changed, 2 insertions, 103 deletions
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 - } -} |