From ba26169d47d42a8f50d30f29f699edb61a4b3759 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 16 Apr 2019 18:03:12 +0200 Subject: Remove higher-kinded type noise in Type --- dhall/src/expr.rs | 9 +++- dhall/src/tests.rs | 2 +- dhall/src/traits/dynamic_type.rs | 8 ++-- dhall/src/typecheck.rs | 90 ++++++++++++++++++++++++---------------- 4 files changed, 67 insertions(+), 42 deletions(-) (limited to 'dhall/src') diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs index cda1d8d..9e89e3a 100644 --- a/dhall/src/expr.rs +++ b/dhall/src/expr.rs @@ -73,6 +73,7 @@ pub struct Type<'a>(pub(crate) TypeInternal<'a>); #[derive(Debug, Clone, PartialEq, Eq)] pub(crate) enum TypeInternal<'a> { Expr(Box>), + Const(dhall_core::Const), /// The type of `Sort` SuperType, } @@ -116,8 +117,14 @@ impl<'a> Normalized<'a> { pub(crate) fn as_expr(&self) -> &SubExpr { &self.0 } + pub(crate) fn into_expr(self) -> SubExpr { + self.0 + } pub(crate) fn into_type(self) -> Type<'a> { - crate::expr::Type(TypeInternal::Expr(Box::new(self))) + Type(match self.0.as_ref() { + ExprF::Const(c) => TypeInternal::Const(*c), + _ => TypeInternal::Expr(Box::new(self)), + }) } } diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs index ce24bfc..5cea6aa 100644 --- a/dhall/src/tests.rs +++ b/dhall/src/tests.rs @@ -139,7 +139,7 @@ pub fn run_test( TypeInference => { let expr = expr.typecheck()?; let ty = expr.get_type()?; - assert_eq_display!(ty.as_normalized()?, &expected); + assert_eq_display!(ty.as_normalized()?.as_ref(), &expected); } Normalization => { let expr = expr.skip_typecheck().normalize(); diff --git a/dhall/src/traits/dynamic_type.rs b/dhall/src/traits/dynamic_type.rs index 28ed76d..d2a5414 100644 --- a/dhall/src/traits/dynamic_type.rs +++ b/dhall/src/traits/dynamic_type.rs @@ -1,6 +1,6 @@ use crate::expr::*; use crate::traits::StaticType; -use crate::typecheck::{TypeError, TypeMessage}; +use crate::typecheck::{type_of_const, TypeError, TypeMessage}; use dhall_core::context::Context; use dhall_core::{Const, ExprF}; use std::borrow::Cow; @@ -17,10 +17,10 @@ impl DynamicType for T { impl<'a> DynamicType for Type<'a> { fn get_type(&self) -> Result>, TypeError> { - use TypeInternal::*; match &self.0 { - Expr(e) => e.get_type(), - SuperType => Err(TypeError::new( + TypeInternal::Expr(e) => e.get_type(), + TypeInternal::Const(c) => Ok(Cow::Owned(type_of_const(*c))), + TypeInternal::SuperType => Err(TypeError::new( &Context::new(), dhall_core::rc(ExprF::Const(Const::Sort)), TypeMessage::Untyped, diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index 86c5ebd..195628b 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -1,5 +1,6 @@ #![allow(non_snake_case)] use std::borrow::Borrow; +use std::borrow::Cow; use std::fmt; use std::marker::PhantomData; @@ -54,11 +55,13 @@ impl Normalized<'static> { } } impl<'a> Type<'a> { - pub(crate) fn as_normalized(&self) -> Result<&Normalized<'a>, TypeError> { - use TypeInternal::*; + pub(crate) fn as_normalized( + &self, + ) -> Result>, TypeError> { match &self.0 { - Expr(e) => Ok(e), - SuperType => Err(TypeError::new( + TypeInternal::Expr(e) => Ok(Cow::Borrowed(e)), + TypeInternal::Const(c) => Ok(Cow::Owned(const_to_normalized(*c))), + TypeInternal::SuperType => Err(TypeError::new( &Context::new(), rc(ExprF::Const(Const::Sort)), TypeMessage::Untyped, @@ -66,51 +69,47 @@ impl<'a> Type<'a> { } } pub(crate) fn into_normalized(self) -> Result, TypeError> { - use TypeInternal::*; match self.0 { - Expr(e) => Ok(*e), - SuperType => Err(TypeError::new( + 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, )), } } + // Expose the outermost constructor, except if it is Const + fn unroll_ref_no_const(&self) -> Result<&Expr, TypeError> { + match self.as_normalized()? { + Cow::Borrowed(e) => Ok(e.unroll_ref()), + Cow::Owned(_) => unimplemented!(), + } + } // Expose the outermost constructor - fn unroll_ref(&self) -> Result<&Expr, TypeError> { - Ok(self.as_normalized()?.unroll_ref()) + fn unroll_ref(&self) -> Result>, TypeError> { + match self.as_normalized()? { + Cow::Borrowed(e) => Ok(Cow::Borrowed(e.unroll_ref())), + Cow::Owned(e) => Ok(Cow::Owned(e.into_expr().unroll())), + } } fn shift(&self, delta: isize, var: &V