diff options
| -rw-r--r-- | dhall/src/expr.rs | 9 | ||||
| -rw-r--r-- | dhall/src/tests.rs | 2 | ||||
| -rw-r--r-- | dhall/src/traits/dynamic_type.rs | 8 | ||||
| -rw-r--r-- | dhall/src/typecheck.rs | 90 |
4 files changed, 67 insertions, 42 deletions
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<Normalized<'a>>), + Const(dhall_core::Const), /// The type of `Sort` SuperType, } @@ -116,8 +117,14 @@ impl<'a> Normalized<'a> { pub(crate) fn as_expr(&self) -> &SubExpr<X, X> { &self.0 } + pub(crate) fn into_expr(self) -> SubExpr<X, X> { + 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<T: StaticType> DynamicType for T { impl<'a> DynamicType for Type<'a> { fn get_type(&self) -> Result<Cow<'_, Type<'static>>, 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<Cow<Normalized<'a>>, 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<Normalized<'a>, 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<X, X>, 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<X, X>, TypeError> { - Ok(self.as_normalized()?.unroll_ref()) + fn unroll_ref(&self) -> Result<Cow<Expr<X, X>>, 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<Label>) -> Self { use TypeInternal::*; - crate::expr::Type(match &self.0 { + Type(match &self.0 { Expr(e) => Expr(Box::new(e.shift(delta, var))), + Const(c) => Const(*c), SuperType => SuperType, }) } fn const_sort() -> Self { - Normalized( - rc(ExprF::Const(Const::Sort)), - Some(Type(TypeInternal::SuperType)), - PhantomData, - ) - .into_type() + Type(TypeInternal::Const(Const::Sort)) } fn const_kind() -> Self { - Normalized( - rc(ExprF::Const(Const::Kind)), - Some(Type::const_sort()), - PhantomData, - ) - .into_type() + Type(TypeInternal::Const(Const::Kind)) } pub(crate) fn const_type() -> Self { - Normalized( - rc(ExprF::Const(Const::Type)), - Some(Type::const_kind()), - PhantomData, - ) - .into_type() + Type(TypeInternal::Const(Const::Type)) } } impl Type<'static> { @@ -200,6 +199,7 @@ where } match (&eL0.borrow().0, &eR0.borrow().0) { (TypeInternal::SuperType, TypeInternal::SuperType) => true, + (TypeInternal::Const(cl), TypeInternal::Const(cr)) => cl == cr, (TypeInternal::Expr(l), TypeInternal::Expr(r)) => { let mut ctx = vec![]; go(&mut ctx, l.as_expr(), r.as_expr()) @@ -208,7 +208,19 @@ where } } -fn type_of_const<'a>(c: Const) -> Type<'a> { +fn const_to_normalized<'a>(c: Const) -> Normalized<'a> { + Normalized( + rc(ExprF::Const(c)), + Some(Type(match c { + Const::Type => TypeInternal::Const(Const::Kind), + Const::Kind => TypeInternal::Const(Const::Sort), + Const::Sort => TypeInternal::SuperType, + })), + PhantomData, + ) +} + +pub(crate) fn type_of_const<'a>(c: Const) -> Type<'a> { match c { Const::Type => Type::const_kind(), Const::Kind => Type::const_sort(), @@ -216,7 +228,7 @@ fn type_of_const<'a>(c: Const) -> Type<'a> { } } -fn type_of_builtin<S>(b: Builtin) -> Expr<S, Normalized<'static>> { +fn type_of_builtin<N, E>(b: Builtin) -> Expr<N, E> { use dhall_core::Builtin::*; match b { Bool | Natural | Integer | Double | Text => dhall::expr!(Type), @@ -293,7 +305,7 @@ macro_rules! ensure_equal { macro_rules! ensure_matches { ($x:expr, $pat:pat => $branch:expr, $err:expr $(,)*) => { - match $x.unroll_ref()? { + match $x.unroll_ref_no_const()? { $pat => $branch, _ => return Err($err), } @@ -302,14 +314,20 @@ macro_rules! ensure_matches { // Ensure the provided type has type `Type` macro_rules! ensure_simple_type { - ($x:expr, $err:expr $(,)*) => { - ensure_matches!($x.get_type()?, Const(Type) => {}, $err) - }; + ($x:expr, $err:expr $(,)*) => {{ + let k = ensure_is_const!($x.get_type()?, $err); + if k != Type { + return Err($err); + } + }}; } macro_rules! ensure_is_const { ($x:expr, $err:expr $(,)*) => { - ensure_matches!($x, Const(k) => *k, $err) + match $x.unroll_ref()?.as_ref() { + Const(k) => *k, + _ => return Err($err), + } }; } @@ -619,7 +637,7 @@ fn type_last_layer( // TODO: check type of interpolations TextLit(_) => Ok(RetType(simple_type_from_builtin(Text))), BinOp(o @ ListAppend, l, r) => { - match l.get_type()?.as_normalized()?.as_expr().as_ref() { + match l.get_type()?.unroll_ref()?.as_ref() { App(f, args) if args.len() == 1 => match f.as_ref() { Builtin(List) => {} _ => return Err(mkerr(BinOpTypeMismatch(o, l))), |