summaryrefslogtreecommitdiff
path: root/dhall/src/typecheck.rs
diff options
context:
space:
mode:
authorNadrieril2019-04-21 11:30:58 +0200
committerNadrieril2019-04-21 11:30:58 +0200
commitd1f828961bccf9627ef4fb76ca528f039d180ff7 (patch)
treef5dc49a621138b98c69537b850118c20107bcd7d /dhall/src/typecheck.rs
parentbbf8d68b0df3ca8b3b8cb7324169f0049736ed89 (diff)
Embrace TypeInternal as a semantic value
Diffstat (limited to 'dhall/src/typecheck.rs')
-rw-r--r--dhall/src/typecheck.rs22
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),
}
};