summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
Diffstat (limited to 'dhall')
-rw-r--r--dhall/src/core/context.rs3
-rw-r--r--dhall/src/core/mod.rs1
-rw-r--r--dhall/src/core/thunk.rs3
-rw-r--r--dhall/src/core/value.rs105
-rw-r--r--dhall/src/core/var.rs103
-rw-r--r--dhall/src/phase/mod.rs3
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;
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-24 12:15:11 +0000