From d1f828961bccf9627ef4fb76ca528f039d180ff7 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 21 Apr 2019 11:30:58 +0200 Subject: Embrace TypeInternal as a semantic value --- dhall/src/expr.rs | 9 +++++++++ dhall/src/normalize.rs | 1 + dhall/src/tests.rs | 2 +- dhall/src/typecheck.rs | 22 ++++++++++++++-------- 4 files changed, 25 insertions(+), 9 deletions(-) (limited to 'dhall/src') 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> for SubExpr { 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>), ), TextLit(Vec>), + /// 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>, TypeError> { + fn as_normalized(&self) -> Result>, 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>), - 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>), } impl<'a> TypeInternal<'a> { - fn into_normalized(self) -> Result, TypeError> { + pub(crate) fn into_normalized(self) -> Result, 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), } }; -- cgit v1.2.3