diff options
author | Nadrieril | 2019-04-21 11:30:58 +0200 |
---|---|---|
committer | Nadrieril | 2019-04-21 11:30:58 +0200 |
commit | d1f828961bccf9627ef4fb76ca528f039d180ff7 (patch) | |
tree | f5dc49a621138b98c69537b850118c20107bcd7d /dhall/src/typecheck.rs | |
parent | bbf8d68b0df3ca8b3b8cb7324169f0049736ed89 (diff) |
Embrace TypeInternal as a semantic value
Diffstat (limited to 'dhall/src/typecheck.rs')
-rw-r--r-- | dhall/src/typecheck.rs | 22 |
1 files changed, 14 insertions, 8 deletions
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), } }; |