diff options
author | Nadrieril | 2019-05-07 18:23:07 +0200 |
---|---|---|
committer | Nadrieril | 2019-05-07 18:23:07 +0200 |
commit | 8cb3046e0920bf24d66c578b1a2b184c741b73fe (patch) | |
tree | 2fd14f54a5d140cf62afa75cf6b37dab8b90536f /dhall | |
parent | 3da450aa3fae23214aa982643b9bc4dd0ea4eaa6 (diff) |
Move AlphaVar and AlphaLabel into a new module
Diffstat (limited to '')
-rw-r--r-- | dhall/src/core/context.rs | 3 | ||||
-rw-r--r-- | dhall/src/core/mod.rs | 1 | ||||
-rw-r--r-- | dhall/src/core/thunk.rs | 3 | ||||
-rw-r--r-- | dhall/src/core/value.rs | 105 | ||||
-rw-r--r-- | dhall/src/core/var.rs | 103 | ||||
-rw-r--r-- | dhall/src/phase/mod.rs | 3 |
6 files changed, 112 insertions, 106 deletions
diff --git a/dhall/src/core/context.rs b/dhall/src/core/context.rs index 9b5beed..0466058 100644 --- a/dhall/src/core/context.rs +++ b/dhall/src/core/context.rs @@ -5,7 +5,8 @@ use dhall_syntax::context::Context; use dhall_syntax::{Label, V}; use crate::core::thunk::Thunk; -use crate::core::value::{AlphaVar, Value}; +use crate::core::value::Value; +use crate::core::var::AlphaVar; use crate::phase::{Normalized, Type, Typed}; #[derive(Debug, Clone)] diff --git a/dhall/src/core/mod.rs b/dhall/src/core/mod.rs index 8f5c2ca..a202e72 100644 --- a/dhall/src/core/mod.rs +++ b/dhall/src/core/mod.rs @@ -1,3 +1,4 @@ pub(crate) mod context; pub(crate) mod thunk; pub(crate) mod value; +pub(crate) mod var; diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs index 2b013bb..14ef710 100644 --- a/dhall/src/core/thunk.rs +++ b/dhall/src/core/thunk.rs @@ -3,7 +3,8 @@ use std::rc::Rc; use crate::core::context::NormalizationContext; use crate::core::context::TypecheckContext; -use crate::core::value::{AlphaVar, Value}; +use crate::core::value::Value; +use crate::core::var::AlphaVar; use crate::error::TypeError; use crate::phase::normalize::{ apply_any, normalize_whnf, InputSubExpr, OutputSubExpr, 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 - } -} 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 + } +} diff --git a/dhall/src/phase/mod.rs b/dhall/src/phase/mod.rs index c8a8ffd..97b8083 100644 --- a/dhall/src/phase/mod.rs +++ b/dhall/src/phase/mod.rs @@ -6,7 +6,8 @@ use dhall_syntax::{Const, Import, Span, SubExpr, X}; use crate::core::context::TypecheckContext; use crate::core::thunk::Thunk; -use crate::core::value::{AlphaVar, Value}; +use crate::core::value::Value; +use crate::core::var::AlphaVar; use crate::error::{Error, ImportError, TypeError, TypeMessage}; use resolve::ImportRoot; |