From 20f01b79378a41c6e063d33c584d04c756419a26 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 21 Apr 2019 19:38:09 +0200 Subject: Factor out context handling --- dhall/src/traits/dynamic_type.rs | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) (limited to 'dhall/src/traits') diff --git a/dhall/src/traits/dynamic_type.rs b/dhall/src/traits/dynamic_type.rs index d4faf45..479bed6 100644 --- a/dhall/src/traits/dynamic_type.rs +++ b/dhall/src/traits/dynamic_type.rs @@ -1,7 +1,8 @@ use crate::expr::*; use crate::traits::StaticType; -use crate::typecheck::{type_of_const, TypeError, TypeMessage}; -use dhall_core::context::Context; +use crate::typecheck::{ + type_of_const, TypeError, TypeMessage, TypecheckContext, +}; use dhall_core::{Const, ExprF}; use std::borrow::Cow; @@ -21,7 +22,7 @@ impl<'a> DynamicType for Type<'a> { TypeInternal::Expr(e) => e.get_type(), TypeInternal::Const(c) => Ok(Cow::Owned(type_of_const(*c))), TypeInternal::SuperType => Err(TypeError::new( - &Context::new(), + &TypecheckContext::new(), dhall_core::rc(ExprF::Const(Const::Sort)), TypeMessage::Untyped, )), @@ -34,7 +35,7 @@ impl<'a> DynamicType for Normalized<'a> { match &self.1 { Some(t) => Ok(Cow::Borrowed(t)), None => Err(TypeError::new( - &Context::new(), + &TypecheckContext::new(), self.0.embed_absurd(), TypeMessage::Untyped, )), @@ -47,7 +48,7 @@ impl<'a> DynamicType for Typed<'a> { match &self.1 { Some(t) => Ok(Cow::Borrowed(t)), None => Err(TypeError::new( - &Context::new(), + &TypecheckContext::new(), self.0.clone(), TypeMessage::Untyped, )), -- cgit v1.2.3 From 60df4ed07a752d256888e6b4449a48bfa43cf79f Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 22 Apr 2019 23:31:42 +0200 Subject: Temporarily simplify functions depending on TypeInternal --- dhall/src/traits/dynamic_type.rs | 21 ++++++++++++--------- 1 file changed, 12 insertions(+), 9 deletions(-) (limited to 'dhall/src/traits') diff --git a/dhall/src/traits/dynamic_type.rs b/dhall/src/traits/dynamic_type.rs index 479bed6..3b34363 100644 --- a/dhall/src/traits/dynamic_type.rs +++ b/dhall/src/traits/dynamic_type.rs @@ -18,15 +18,18 @@ impl DynamicType for T { impl<'a> DynamicType for Type<'a> { fn get_type(&self) -> Result>, TypeError> { - match &self.0 { - TypeInternal::Expr(e) => e.get_type(), - TypeInternal::Const(c) => Ok(Cow::Owned(type_of_const(*c))), - TypeInternal::SuperType => Err(TypeError::new( - &TypecheckContext::new(), - dhall_core::rc(ExprF::Const(Const::Sort)), - TypeMessage::Untyped, - )), - } + Ok(Cow::Owned( + self.clone().into_normalized()?.get_type()?.into_owned(), + )) + // match &self.0 { + // TypeInternal::Expr(e) => e.get_type(), + // TypeInternal::Const(c) => Ok(Cow::Owned(type_of_const(*c))), + // TypeInternal::SuperType => Err(TypeError::new( + // &TypecheckContext::new(), + // dhall_core::rc(ExprF::Const(Const::Sort)), + // TypeMessage::Untyped, + // )), + // } } } -- cgit v1.2.3 From 2f1fa26abd9c9f2b75d24b18877d3b278f7d2a01 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 23 Apr 2019 14:13:50 +0200 Subject: Avoid duplicating work when matching on Pi types --- dhall/src/traits/deserialize.rs | 2 +- dhall/src/traits/static_type.rs | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) (limited to 'dhall/src/traits') diff --git a/dhall/src/traits/deserialize.rs b/dhall/src/traits/deserialize.rs index 43eb2ac..9cc2147 100644 --- a/dhall/src/traits/deserialize.rs +++ b/dhall/src/traits/deserialize.rs @@ -48,6 +48,6 @@ impl<'de: 'a, 'a> Deserialize<'de> for Normalized<'a> { impl<'de: 'a, 'a> Deserialize<'de> for Type<'a> { fn from_str(s: &'de str, ty: Option<&Type>) -> Result { - Ok(Normalized::from_str(s, ty)?.into_type()) + Ok(Normalized::from_str(s, ty)?.into_type()?) } } diff --git a/dhall/src/traits/static_type.rs b/dhall/src/traits/static_type.rs index e92ce78..225eb32 100644 --- a/dhall/src/traits/static_type.rs +++ b/dhall/src/traits/static_type.rs @@ -44,6 +44,7 @@ impl StaticType for T { std::marker::PhantomData, ) .into_type() + .unwrap() } } -- cgit v1.2.3 From 4b1ad84cb2dad533069d685e212894d517d8fa57 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 23 Apr 2019 17:59:10 +0200 Subject: Silence warnings --- dhall/src/traits/dynamic_type.rs | 2 ++ 1 file changed, 2 insertions(+) (limited to 'dhall/src/traits') diff --git a/dhall/src/traits/dynamic_type.rs b/dhall/src/traits/dynamic_type.rs index 3b34363..f783950 100644 --- a/dhall/src/traits/dynamic_type.rs +++ b/dhall/src/traits/dynamic_type.rs @@ -1,8 +1,10 @@ use crate::expr::*; use crate::traits::StaticType; +#[allow(unused_imports)] use crate::typecheck::{ type_of_const, TypeError, TypeMessage, TypecheckContext, }; +#[allow(unused_imports)] use dhall_core::{Const, ExprF}; use std::borrow::Cow; -- cgit v1.2.3 From 5a3d63ecb46ee0b4ab3a7b49cf9feb286b164803 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 29 Apr 2019 16:34:13 +0200 Subject: Don't need to store original expression in TypeError --- dhall/src/traits/dynamic_type.rs | 11 ----------- 1 file changed, 11 deletions(-) (limited to 'dhall/src/traits') diff --git a/dhall/src/traits/dynamic_type.rs b/dhall/src/traits/dynamic_type.rs index f783950..c15b277 100644 --- a/dhall/src/traits/dynamic_type.rs +++ b/dhall/src/traits/dynamic_type.rs @@ -23,15 +23,6 @@ impl<'a> DynamicType for Type<'a> { Ok(Cow::Owned( self.clone().into_normalized()?.get_type()?.into_owned(), )) - // match &self.0 { - // TypeInternal::Expr(e) => e.get_type(), - // TypeInternal::Const(c) => Ok(Cow::Owned(type_of_const(*c))), - // TypeInternal::SuperType => Err(TypeError::new( - // &TypecheckContext::new(), - // dhall_core::rc(ExprF::Const(Const::Sort)), - // TypeMessage::Untyped, - // )), - // } } } @@ -41,7 +32,6 @@ impl<'a> DynamicType for Normalized<'a> { Some(t) => Ok(Cow::Borrowed(t)), None => Err(TypeError::new( &TypecheckContext::new(), - self.0.embed_absurd(), TypeMessage::Untyped, )), } @@ -54,7 +44,6 @@ impl<'a> DynamicType for Typed<'a> { Some(t) => Ok(Cow::Borrowed(t)), None => Err(TypeError::new( &TypecheckContext::new(), - self.0.clone(), TypeMessage::Untyped, )), } -- cgit v1.2.3 From 5465b7e2b8cc286e2e8b87556b3ec6a2476cf0cf Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 2 May 2019 12:54:35 +0200 Subject: Tweaks --- dhall/src/traits/static_type.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'dhall/src/traits') diff --git a/dhall/src/traits/static_type.rs b/dhall/src/traits/static_type.rs index 225eb32..8b5acbf 100644 --- a/dhall/src/traits/static_type.rs +++ b/dhall/src/traits/static_type.rs @@ -33,7 +33,7 @@ pub trait SimpleStaticType { } fn mktype<'a>(x: SubExpr) -> SimpleType<'a> { - SimpleType(x, std::marker::PhantomData) + x.into() } impl StaticType for T { -- cgit v1.2.3 From c13a4881b56bf2f5b2d5d4d0018a48927b45e7e0 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 2 May 2019 14:11:29 +0200 Subject: Store Thunk in Normalized --- dhall/src/traits/static_type.rs | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'dhall/src/traits') diff --git a/dhall/src/traits/static_type.rs b/dhall/src/traits/static_type.rs index 8b5acbf..4dd9961 100644 --- a/dhall/src/traits/static_type.rs +++ b/dhall/src/traits/static_type.rs @@ -39,7 +39,9 @@ fn mktype<'a>(x: SubExpr) -> SimpleType<'a> { impl StaticType for T { fn get_static_type() -> Type<'static> { crate::expr::Normalized( - T::get_simple_static_type().into(), + crate::normalize::Thunk::from_normalized_expr( + T::get_simple_static_type().into(), + ), Some(Type::const_type()), std::marker::PhantomData, ) -- cgit v1.2.3 From db3ca819283f9bd99d197de464717f0b58b52fe4 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 2 May 2019 17:07:11 +0200 Subject: Instead of possibly nonexistent Type, treat Sort specially --- dhall/src/traits/deserialize.rs | 2 +- dhall/src/traits/dynamic_type.rs | 24 ++++-------------------- dhall/src/traits/static_type.rs | 8 +++----- 3 files changed, 8 insertions(+), 26 deletions(-) (limited to 'dhall/src/traits') diff --git a/dhall/src/traits/deserialize.rs b/dhall/src/traits/deserialize.rs index 9cc2147..99ca5ee 100644 --- a/dhall/src/traits/deserialize.rs +++ b/dhall/src/traits/deserialize.rs @@ -48,6 +48,6 @@ impl<'de: 'a, 'a> Deserialize<'de> for Normalized<'a> { impl<'de: 'a, 'a> Deserialize<'de> for Type<'a> { fn from_str(s: &'de str, ty: Option<&Type>) -> Result { - Ok(Normalized::from_str(s, ty)?.into_type()?) + Ok(Normalized::from_str(s, ty)?.to_type()) } } diff --git a/dhall/src/traits/dynamic_type.rs b/dhall/src/traits/dynamic_type.rs index c15b277..74c2e0a 100644 --- a/dhall/src/traits/dynamic_type.rs +++ b/dhall/src/traits/dynamic_type.rs @@ -1,9 +1,7 @@ use crate::expr::*; use crate::traits::StaticType; #[allow(unused_imports)] -use crate::typecheck::{ - type_of_const, TypeError, TypeMessage, TypecheckContext, -}; +use crate::typecheck::{TypeError, TypeMessage, TypecheckContext}; #[allow(unused_imports)] use dhall_core::{Const, ExprF}; use std::borrow::Cow; @@ -20,32 +18,18 @@ impl DynamicType for T { impl<'a> DynamicType for Type<'a> { fn get_type(&self) -> Result>, TypeError> { - Ok(Cow::Owned( - self.clone().into_normalized()?.get_type()?.into_owned(), - )) + self.get_type() } } impl<'a> DynamicType for Normalized<'a> { fn get_type(&self) -> Result>, TypeError> { - match &self.1 { - Some(t) => Ok(Cow::Borrowed(t)), - None => Err(TypeError::new( - &TypecheckContext::new(), - TypeMessage::Untyped, - )), - } + self.0.get_type() } } impl<'a> DynamicType for Typed<'a> { fn get_type(&self) -> Result>, TypeError> { - match &self.1 { - Some(t) => Ok(Cow::Borrowed(t)), - None => Err(TypeError::new( - &TypecheckContext::new(), - TypeMessage::Untyped, - )), - } + self.0.get_type() } } diff --git a/dhall/src/traits/static_type.rs b/dhall/src/traits/static_type.rs index 4dd9961..df6a177 100644 --- a/dhall/src/traits/static_type.rs +++ b/dhall/src/traits/static_type.rs @@ -38,15 +38,13 @@ fn mktype<'a>(x: SubExpr) -> SimpleType<'a> { impl StaticType for T { fn get_static_type() -> Type<'static> { - crate::expr::Normalized( + crate::expr::Normalized::from_thunk_and_type( crate::normalize::Thunk::from_normalized_expr( T::get_simple_static_type().into(), ), - Some(Type::const_type()), - std::marker::PhantomData, + Type::const_type(), ) - .into_type() - .unwrap() + .to_type() } } -- cgit v1.2.3