summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorNadrieril2019-04-21 11:30:58 +0200
committerNadrieril2019-04-21 11:30:58 +0200
commitd1f828961bccf9627ef4fb76ca528f039d180ff7 (patch)
treef5dc49a621138b98c69537b850118c20107bcd7d
parentbbf8d68b0df3ca8b3b8cb7324169f0049736ed89 (diff)
Embrace TypeInternal as a semantic value
-rw-r--r--dhall/src/expr.rs9
-rw-r--r--dhall/src/normalize.rs1
-rw-r--r--dhall/src/tests.rs2
-rw-r--r--dhall/src/typecheck.rs22
4 files changed, 25 insertions, 9 deletions
diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs
index 03aa966..44d1612 100644
--- a/dhall/src/expr.rs
+++ b/dhall/src/expr.rs
@@ -72,6 +72,15 @@ pub(crate) use crate::typecheck::TypeInternal;
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct Type<'a>(pub(crate) TypeInternal<'a>);
+impl<'a> std::fmt::Display for Type<'a> {
+ fn fmt(&self, f: &mut std::fmt::Formatter) -> Result<(), std::fmt::Error> {
+ match self.0.clone().into_normalized() {
+ Ok(e) => e.fmt(f),
+ Err(_) => write!(f, "SuperType"),
+ }
+ }
+}
+
// Exposed for the macros
#[doc(hidden)]
impl<'a> From<SimpleType<'a>> for SubExpr<X, X> {
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index f092c4d..7aa8686 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -322,6 +322,7 @@ enum WHNF {
(NormalizationContext, BTreeMap<Label, Option<InputSubExpr>>),
),
TextLit(Vec<InterpolatedTextContents<Now>>),
+ /// This must not contain a value captured by one of the variants above.
Expr(OutputSubExpr),
}
diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs
index 7f85b5c..c945b23 100644
--- a/dhall/src/tests.rs
+++ b/dhall/src/tests.rs
@@ -140,7 +140,7 @@ pub fn run_test(
TypeInference => {
let expr = expr.typecheck()?;
let ty = expr.get_type()?;
- assert_eq_display!(ty.as_normalized()?.as_ref(), &expected);
+ assert_eq_display!(ty.as_ref(), &expected.into_type());
}
Normalization => {
let expr = expr.skip_typecheck().normalize();
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 99fb003..b0ea63e 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -61,9 +61,7 @@ impl Normalized<'static> {
}
}
impl<'a> Type<'a> {
- pub(crate) fn as_normalized(
- &self,
- ) -> Result<Cow<Normalized<'a>>, TypeError> {
+ fn as_normalized(&self) -> Result<Cow<Normalized<'a>>, TypeError> {
match &self.0 {
TypeInternal::Expr(e) => Ok(Cow::Borrowed(e)),
TypeInternal::Const(c) => Ok(Cow::Owned(const_to_normalized(*c))),
@@ -84,6 +82,9 @@ impl<'a> Type<'a> {
Cow::Owned(e) => Ok(Cow::Owned(e.into_expr().unroll())),
}
}
+ fn internal(&self) -> &TypeInternal {
+ &self.0
+ }
fn shift0(&self, delta: isize, label: &Label) -> Self {
use TypeInternal::*;
Type(match &self.0 {
@@ -109,16 +110,21 @@ impl Type<'static> {
}
}
+/// A semantic type. This is partially redundant with `dhall_core::Expr`, on purpose. `TypeInternal` should
+/// be limited to syntactic expressions: either written by the user or meant to be printed.
+/// The rule is the following: we must _not_ construct values of type `Expr` while typechecking,
+/// but only construct `TypeInternal`s.
#[derive(Debug, Clone, PartialEq, Eq)]
pub(crate) enum TypeInternal<'a> {
- Expr(Box<Normalized<'a>>),
- Const(dhall_core::Const),
+ Const(Const),
/// The type of `Sort`
SuperType,
+ /// This must not contain a value captured by one of the variants above.
+ Expr(Box<Normalized<'a>>),
}
impl<'a> TypeInternal<'a> {
- fn into_normalized(self) -> Result<Normalized<'a>, TypeError> {
+ pub(crate) fn into_normalized(self) -> Result<Normalized<'a>, TypeError> {
match self {
TypeInternal::Expr(e) => Ok(*e),
TypeInternal::Const(c) => Ok(const_to_normalized(c)),
@@ -348,8 +354,8 @@ macro_rules! ensure_simple_type {
macro_rules! ensure_is_const {
($x:expr, $err:expr $(,)*) => {
- match $x.unroll_ref()?.as_ref() {
- Const(k) => *k,
+ match $x.internal() {
+ TypeInternal::Const(k) => *k,
_ => return Err($err),
}
};