summaryrefslogtreecommitdiff
path: root/dhall/src/expr.rs
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/expr.rs')
-rw-r--r--dhall/src/expr.rs208
1 files changed, 157 insertions, 51 deletions
diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs
index bb1a4e4..4d55f4a 100644
--- a/dhall/src/expr.rs
+++ b/dhall/src/expr.rs
@@ -1,4 +1,5 @@
use crate::imports::ImportRoot;
+use crate::normalize::{Thunk, Value};
use dhall_core::*;
use std::marker::PhantomData;
@@ -10,6 +11,8 @@ macro_rules! derive_other_traits {
}
}
+ impl<'a> std::cmp::Eq for $ty<'a> {}
+
impl<'a> std::fmt::Display for $ty<'a> {
fn fmt(
&self,
@@ -21,34 +24,149 @@ macro_rules! derive_other_traits {
};
}
-#[derive(Debug, Clone, Eq)]
+#[derive(Debug, Clone)]
pub(crate) struct Parsed<'a>(
pub(crate) SubExpr<Span<'a>, Import>,
pub(crate) ImportRoot,
);
derive_other_traits!(Parsed);
-#[derive(Debug, Clone, Eq)]
+#[derive(Debug, Clone)]
pub(crate) struct Resolved<'a>(
pub(crate) SubExpr<Span<'a>, Normalized<'static>>,
);
derive_other_traits!(Resolved);
-#[derive(Debug, Clone, Eq)]
+pub(crate) use self::typed::TypedInternal;
+
+#[derive(Debug, Clone)]
pub(crate) struct Typed<'a>(
- pub(crate) SubExpr<X, Normalized<'static>>,
- pub(crate) Option<Type<'static>>,
+ pub(crate) TypedInternal,
pub(crate) PhantomData<&'a ()>,
);
-derive_other_traits!(Typed);
-#[derive(Debug, Clone, Eq)]
+#[derive(Debug, Clone)]
pub(crate) struct Normalized<'a>(
- pub(crate) SubExpr<X, X>,
- pub(crate) Option<Type<'static>>,
+ pub(crate) TypedInternal,
pub(crate) PhantomData<&'a ()>,
);
-derive_other_traits!(Normalized);
+
+impl<'a> std::cmp::PartialEq for Normalized<'a> {
+ fn eq(&self, other: &Self) -> bool {
+ self.to_expr() == other.to_expr()
+ }
+}
+
+impl<'a> std::cmp::Eq for Normalized<'a> {}
+
+impl<'a> std::fmt::Display for Normalized<'a> {
+ fn fmt(&self, f: &mut std::fmt::Formatter) -> Result<(), std::fmt::Error> {
+ self.to_expr().fmt(f)
+ }
+}
+
+mod typed {
+ use super::{Type, Typed};
+ use crate::normalize::{Thunk, Value};
+ use crate::typecheck::{
+ TypeError, TypeInternal, TypeMessage, TypecheckContext,
+ };
+ use dhall_core::{Const, Label, SubExpr, V, X};
+ use std::borrow::Cow;
+ use std::marker::PhantomData;
+
+ #[derive(Debug, Clone)]
+ pub(crate) enum TypedInternal {
+ // The `Sort` higher-kinded type doesn't have a type
+ Sort,
+ // Any other value, along with its type
+ Value(Thunk, Option<Type<'static>>),
+ }
+
+ impl TypedInternal {
+ pub(crate) fn from_thunk_and_type(th: Thunk, t: Type<'static>) -> Self {
+ TypedInternal::Value(th, Some(t))
+ }
+
+ pub(crate) fn from_thunk_untyped(th: Thunk) -> Self {
+ TypedInternal::Value(th, None)
+ }
+
+ // TODO: Avoid cloning if possible
+ pub(crate) fn to_value(&self) -> Value {
+ match self {
+ TypedInternal::Value(th, _) => th.normalize_whnf().clone(),
+ TypedInternal::Sort => Value::Const(Const::Sort),
+ }
+ }
+
+ pub(crate) fn to_expr(&self) -> SubExpr<X, X> {
+ self.to_value().normalize_to_expr()
+ }
+
+ pub(crate) fn to_thunk(&self) -> Thunk {
+ match self {
+ TypedInternal::Value(th, _) => th.clone(),
+ TypedInternal::Sort => {
+ Thunk::from_whnf(Value::Const(Const::Sort))
+ }
+ }
+ }
+
+ pub(crate) fn to_type(&self) -> Type<'static> {
+ match self {
+ TypedInternal::Sort => Type(TypeInternal::Const(Const::Sort)),
+ TypedInternal::Value(th, _) => match &*th.normalize_whnf() {
+ Value::Const(c) => Type(TypeInternal::Const(*c)),
+ _ => Type(TypeInternal::Typed(Box::new(Typed(
+ self.clone(),
+ PhantomData,
+ )))),
+ },
+ }
+ }
+
+ pub(crate) fn get_type(
+ &self,
+ ) -> Result<Cow<'_, Type<'static>>, TypeError> {
+ match self {
+ TypedInternal::Value(_, Some(t)) => Ok(Cow::Borrowed(t)),
+ TypedInternal::Value(_, None) => Err(TypeError::new(
+ &TypecheckContext::new(),
+ TypeMessage::Untyped,
+ )),
+ TypedInternal::Sort => Err(TypeError::new(
+ &TypecheckContext::new(),
+ TypeMessage::Sort,
+ )),
+ }
+ }
+
+ pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self {
+ match self {
+ TypedInternal::Value(th, t) => TypedInternal::Value(
+ th.shift(delta, var),
+ t.as_ref().map(|x| x.shift(delta, var)),
+ ),
+ TypedInternal::Sort => TypedInternal::Sort,
+ }
+ }
+
+ pub(crate) fn subst_shift(
+ &self,
+ var: &V<Label>,
+ val: &Typed<'static>,
+ ) -> Self {
+ match self {
+ TypedInternal::Value(th, t) => TypedInternal::Value(
+ th.subst_shift(var, val),
+ t.as_ref().map(|x| x.subst_shift(var, val)),
+ ),
+ TypedInternal::Sort => TypedInternal::Sort,
+ }
+ }
+ }
+}
/// A Dhall expression representing a simple type.
///
@@ -56,13 +174,15 @@ derive_other_traits!(Normalized);
/// `Bool`, `{ x: Integer }` or `Natural -> Text`.
///
/// For a more general notion of "type", see [Type].
-#[derive(Debug, Clone, Eq)]
+#[derive(Debug, Clone)]
pub struct SimpleType<'a>(
pub(crate) SubExpr<X, X>,
pub(crate) PhantomData<&'a ()>,
);
derive_other_traits!(SimpleType);
+pub(crate) use crate::typecheck::TypeInternal;
+
/// A Dhall expression representing a (possibly higher-kinded) type.
///
/// This includes [SimpleType]s but also higher-kinded expressions like
@@ -70,12 +190,10 @@ derive_other_traits!(SimpleType);
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct Type<'a>(pub(crate) TypeInternal<'a>);
-#[derive(Debug, Clone, PartialEq, Eq)]
-pub(crate) enum TypeInternal<'a> {
- Expr(Box<Normalized<'a>>),
- Const(dhall_core::Const),
- /// The type of `Sort`
- SuperType,
+impl<'a> std::fmt::Display for Type<'a> {
+ fn fmt(&self, f: &mut std::fmt::Formatter) -> Result<(), std::fmt::Error> {
+ self.to_normalized().fmt(f)
+ }
}
// Exposed for the macros
@@ -98,50 +216,38 @@ impl<'a> From<SubExpr<X, X>> for SimpleType<'a> {
#[doc(hidden)]
impl<'a> From<Normalized<'a>> for Typed<'a> {
fn from(x: Normalized<'a>) -> Typed<'a> {
- Typed(x.0.embed_absurd(), x.1, x.2)
+ Typed(x.0, x.1)
}
}
-#[doc(hidden)]
-impl<'a> Typed<'a> {
- pub(crate) fn as_expr(&self) -> &SubExpr<X, Normalized<'a>> {
- &self.0
- }
-}
-
-#[doc(hidden)]
impl<'a> Normalized<'a> {
- pub(crate) fn as_expr(&self) -> &SubExpr<X, X> {
- &self.0
+ pub(crate) fn from_thunk_and_type(th: Thunk, t: Type<'static>) -> Self {
+ Normalized(TypedInternal::from_thunk_and_type(th, t), PhantomData)
}
- pub(crate) fn into_expr(self) -> SubExpr<X, X> {
- self.0
+ // Deprecated
+ pub(crate) fn as_expr(&self) -> SubExpr<X, X> {
+ self.0.to_expr()
}
- pub(crate) fn unnote<'b>(self) -> Normalized<'b> {
- Normalized(self.0, self.1, PhantomData)
+ pub(crate) fn to_expr(&self) -> SubExpr<X, X> {
+ self.0.to_expr()
}
- pub(crate) fn into_type(self) -> Type<'a> {
- Type(match self.0.as_ref() {
- ExprF::Const(c) => TypeInternal::Const(*c),
- _ => TypeInternal::Expr(Box::new(self)),
- })
+ pub(crate) fn to_value(&self) -> Value {
+ self.0.to_value()
}
-}
-
-#[doc(hidden)]
-impl<'a> Type<'a> {
- pub(crate) fn unnote<'b>(self) -> Type<'b> {
- use TypeInternal::*;
- Type(match self.0 {
- Expr(e) => Expr(Box::new(e.unnote())),
- Const(c) => Const(c),
- SuperType => SuperType,
- })
+ #[allow(dead_code)]
+ pub(crate) fn unnote<'b>(self) -> Normalized<'b> {
+ Normalized(self.0, PhantomData)
}
}
-impl<'a> SimpleType<'a> {
- pub(crate) fn into_type(self) -> Type<'a> {
- Normalized(self.0, Some(Type::const_type()), PhantomData).into_type()
+impl<'a> Typed<'a> {
+ pub(crate) fn from_thunk_and_type(th: Thunk, t: Type<'static>) -> Self {
+ Typed(TypedInternal::from_thunk_and_type(th, t), PhantomData)
+ }
+ pub(crate) fn from_thunk_untyped(th: Thunk) -> Self {
+ Typed(TypedInternal::from_thunk_untyped(th), PhantomData)
+ }
+ pub(crate) fn const_sort() -> Self {
+ Typed(TypedInternal::Sort, PhantomData)
}
}