summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
authorNadrieril2019-04-20 23:52:09 +0200
committerNadrieril2019-04-20 23:52:09 +0200
commitbbf8d68b0df3ca8b3b8cb7324169f0049736ed89 (patch)
tree15f5498371968b5351c32fe110030d2a2a53b636 /dhall
parent9042db26ced0c56714c48bf2f6322e0a1c2a6973 (diff)
Move TypeInternal to typecheck
Diffstat (limited to 'dhall')
-rw-r--r--dhall/src/expr.rs16
-rw-r--r--dhall/src/typecheck.rs38
2 files changed, 31 insertions, 23 deletions
diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs
index bb1a4e4..03aa966 100644
--- a/dhall/src/expr.rs
+++ b/dhall/src/expr.rs
@@ -63,6 +63,8 @@ pub struct SimpleType<'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,14 +72,6 @@ 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,
-}
-
// Exposed for the macros
#[doc(hidden)]
impl<'a> From<SimpleType<'a>> for SubExpr<X, X> {
@@ -120,12 +114,6 @@ impl<'a> Normalized<'a> {
pub(crate) fn unnote<'b>(self) -> Normalized<'b> {
Normalized(self.0, self.1, PhantomData)
}
- 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)),
- })
- }
}
#[doc(hidden)]
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index b26f845..99fb003 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -48,6 +48,12 @@ impl<'a> Normalized<'a> {
// shift the type too ?
Normalized(shift0(delta, label, &self.0), self.1.clone(), self.2)
}
+ 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)),
+ })
+ }
}
impl Normalized<'static> {
fn embed<N>(self) -> SubExpr<N, Normalized<'static>> {
@@ -69,15 +75,7 @@ impl<'a> Type<'a> {
}
}
pub(crate) fn into_normalized(self) -> Result<Normalized<'a>, TypeError> {
- match self.0 {
- TypeInternal::Expr(e) => Ok(*e),
- TypeInternal::Const(c) => Ok(const_to_normalized(c)),
- TypeInternal::SuperType => Err(TypeError::new(
- &Context::new(),
- rc(ExprF::Const(Const::Sort)),
- TypeMessage::Untyped,
- )),
- }
+ self.0.into_normalized()
}
// Expose the outermost constructor
fn unroll_ref(&self) -> Result<Cow<Expr<X, X>>, TypeError> {
@@ -111,6 +109,28 @@ impl Type<'static> {
}
}
+#[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> TypeInternal<'a> {
+ fn into_normalized(self) -> Result<Normalized<'a>, TypeError> {
+ match self {
+ TypeInternal::Expr(e) => Ok(*e),
+ TypeInternal::Const(c) => Ok(const_to_normalized(c)),
+ TypeInternal::SuperType => Err(TypeError::new(
+ &Context::new(),
+ rc(ExprF::Const(Const::Sort)),
+ TypeMessage::Untyped,
+ )),
+ }
+ }
+}
+
fn function_check(a: Const, b: Const) -> Result<Const, ()> {
use dhall_core::Const::*;
match (a, b) {