summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dhall/src/expr.rs72
-rw-r--r--dhall/src/normalize.rs26
-rw-r--r--dhall/src/traits/dynamic_type.rs2
-rw-r--r--dhall/src/typecheck.rs9
4 files changed, 34 insertions, 75 deletions
diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs
index 7dbbf1c..896753c 100644
--- a/dhall/src/expr.rs
+++ b/dhall/src/expr.rs
@@ -34,13 +34,10 @@ derive_other_traits!(Parsed);
pub(crate) struct Resolved(pub(crate) SubExpr<Span, Normalized>);
derive_other_traits!(Resolved);
-pub(crate) use self::typed::TypedInternal;
+pub(crate) use self::typed::Typed;
#[derive(Debug, Clone)]
-pub(crate) struct Typed(pub(crate) TypedInternal);
-
-#[derive(Debug, Clone)]
-pub(crate) struct Normalized(pub(crate) TypedInternal);
+pub(crate) struct Normalized(pub(crate) Typed);
impl std::cmp::PartialEq for Normalized {
fn eq(&self, other: &Self) -> bool {
@@ -57,7 +54,7 @@ impl std::fmt::Display for Normalized {
}
mod typed {
- use super::{Type, Typed};
+ use super::Type;
use crate::normalize::{AlphaVar, Thunk, Value};
use crate::typecheck::{
TypeError, TypeInternal, TypeMessage, TypecheckContext,
@@ -66,27 +63,27 @@ mod typed {
use std::borrow::Cow;
#[derive(Debug, Clone)]
- pub(crate) enum TypedInternal {
+ pub(crate) enum Typed {
// The `Sort` higher-kinded type doesn't have a type
Sort,
// Any other value, along with its type
Value(Thunk, Option<Type>),
}
- impl TypedInternal {
+ impl Typed {
pub(crate) fn from_thunk_and_type(th: Thunk, t: Type) -> Self {
- TypedInternal::Value(th, Some(t))
+ Typed::Value(th, Some(t))
}
pub(crate) fn from_thunk_untyped(th: Thunk) -> Self {
- TypedInternal::Value(th, None)
+ Typed::Value(th, None)
}
// TODO: Avoid cloning if possible
pub(crate) fn to_value(&self) -> Value {
match self {
- TypedInternal::Value(th, _) => th.to_value(),
- TypedInternal::Sort => Value::Const(Const::Sort),
+ Typed::Value(th, _) => th.to_value(),
+ Typed::Sort => Value::Const(Const::Sort),
}
}
@@ -100,33 +97,29 @@ mod typed {
pub(crate) fn to_thunk(&self) -> Thunk {
match self {
- TypedInternal::Value(th, _) => th.clone(),
- TypedInternal::Sort => {
- Thunk::from_value(Value::Const(Const::Sort))
- }
+ Typed::Value(th, _) => th.clone(),
+ Typed::Sort => Thunk::from_value(Value::Const(Const::Sort)),
}
}
pub(crate) fn to_type(&self) -> Type {
match self {
- TypedInternal::Sort => Type(TypeInternal::Const(Const::Sort)),
- TypedInternal::Value(th, _) => match &*th.as_value() {
+ Typed::Sort => Type(TypeInternal::Const(Const::Sort)),
+ Typed::Value(th, _) => match &*th.as_value() {
Value::Const(c) => Type(TypeInternal::Const(*c)),
- _ => {
- Type(TypeInternal::Typed(Box::new(Typed(self.clone()))))
- }
+ _ => Type(TypeInternal::Typed(Box::new(self.clone()))),
},
}
}
pub(crate) fn get_type(&self) -> Result<Cow<'_, Type>, TypeError> {
match self {
- TypedInternal::Value(_, Some(t)) => Ok(Cow::Borrowed(t)),
- TypedInternal::Value(_, None) => Err(TypeError::new(
+ Typed::Value(_, Some(t)) => Ok(Cow::Borrowed(t)),
+ Typed::Value(_, None) => Err(TypeError::new(
&TypecheckContext::new(),
TypeMessage::Untyped,
)),
- TypedInternal::Sort => Err(TypeError::new(
+ Typed::Sort => Err(TypeError::new(
&TypecheckContext::new(),
TypeMessage::Sort,
)),
@@ -135,32 +128,35 @@ mod typed {
pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
match self {
- TypedInternal::Value(th, t) => TypedInternal::Value(
+ Typed::Value(th, t) => Typed::Value(
th.shift(delta, var),
t.as_ref().map(|x| x.shift(delta, var)),
),
- TypedInternal::Sort => TypedInternal::Sort,
+ Typed::Sort => Typed::Sort,
}
}
pub(crate) fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
match self {
- TypedInternal::Value(th, t) => TypedInternal::Value(
+ Typed::Value(th, t) => Typed::Value(
th.subst_shift(var, val),
t.as_ref().map(|x| x.subst_shift(var, val)),
),
- TypedInternal::Sort => TypedInternal::Sort,
+ Typed::Sort => Typed::Sort,
}
}
+ pub(crate) fn const_sort() -> Self {
+ Typed::Sort
+ }
}
- impl std::cmp::PartialEq for TypedInternal {
+ impl std::cmp::PartialEq for Typed {
fn eq(&self, other: &Self) -> bool {
self.to_value() == other.to_value()
}
}
- impl std::cmp::Eq for TypedInternal {}
+ impl std::cmp::Eq for Typed {}
}
/// A Dhall expression representing a simple type.
@@ -208,13 +204,13 @@ impl From<SubExpr<X, X>> for SimpleType {
#[doc(hidden)]
impl From<Normalized> for Typed {
fn from(x: Normalized) -> Typed {
- Typed(x.0)
+ x.0
}
}
impl Normalized {
pub(crate) fn from_thunk_and_type(th: Thunk, t: Type) -> Self {
- Normalized(TypedInternal::from_thunk_and_type(th, t))
+ Normalized(Typed::from_thunk_and_type(th, t))
}
pub(crate) fn to_expr(&self) -> SubExpr<X, X> {
self.0.to_expr()
@@ -230,15 +226,3 @@ impl Normalized {
self.0.to_thunk()
}
}
-
-impl Typed {
- pub(crate) fn from_thunk_and_type(th: Thunk, t: Type) -> Self {
- Typed(TypedInternal::from_thunk_and_type(th, t))
- }
- pub(crate) fn from_thunk_untyped(th: Thunk) -> Self {
- Typed(TypedInternal::from_thunk_untyped(th))
- }
- pub(crate) fn const_sort() -> Self {
- Typed(TypedInternal::Sort)
- }
-}
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 35ab45d..1d306bc 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -9,7 +9,7 @@ use dhall_syntax::{
Natural, Span, SubExpr, V, X,
};
-use crate::expr::{Normalized, Type, Typed, TypedInternal};
+use crate::expr::{Normalized, Type, Typed};
type InputSubExpr = SubExpr<Span, Normalized>;
type OutputSubExpr = SubExpr<X, X>;
@@ -25,29 +25,13 @@ impl Typed {
/// leave ill-typed sub-expressions unevaluated.
///
pub fn normalize(self) -> Normalized {
- match &self.0 {
- TypedInternal::Sort => {}
- TypedInternal::Value(thunk, _) => {
+ match &self {
+ Typed::Sort => {}
+ Typed::Value(thunk, _) => {
thunk.normalize_nf();
}
}
- Normalized(self.0)
- }
-
- pub(crate) fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
- Typed(self.0.shift(delta, var))
- }
-
- pub(crate) fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
- Typed(self.0.subst_shift(var, val))
- }
-
- pub(crate) fn to_value(&self) -> Value {
- self.0.to_value()
- }
-
- pub(crate) fn to_thunk(&self) -> Thunk {
- self.0.to_thunk()
+ Normalized(self)
}
}
diff --git a/dhall/src/traits/dynamic_type.rs b/dhall/src/traits/dynamic_type.rs
index 858642e..4c8e1fd 100644
--- a/dhall/src/traits/dynamic_type.rs
+++ b/dhall/src/traits/dynamic_type.rs
@@ -30,6 +30,6 @@ impl DynamicType for Normalized {
impl DynamicType for Typed {
fn get_type(&self) -> Result<Cow<'_, Type>, TypeError> {
- self.0.get_type()
+ self.get_type()
}
}
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 8d6b6eb..4dde883 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -35,15 +35,6 @@ impl Resolved {
}
}
-impl Typed {
- fn to_type(&self) -> Type {
- match &self.to_value() {
- Value::Const(c) => Type(TypeInternal::Const(*c)),
- _ => Type(TypeInternal::Typed(Box::new(self.clone()))),
- }
- }
-}
-
impl Normalized {
fn shift(&self, delta: isize, var: &AlphaVar) -> Self {
Normalized(self.0.shift(delta, var))
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-25 08:45:15 +0000