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.3.1 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/expr.rs | 15 +++++++++------ dhall/src/traits/dynamic_type.rs | 21 ++++++++++++--------- dhall/src/typecheck.rs | 40 ++++++++++++++-------------------------- 3 files changed, 35 insertions(+), 41 deletions(-) (limited to 'dhall/src/traits') diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs index 1840eba..94093a9 100644 --- a/dhall/src/expr.rs +++ b/dhall/src/expr.rs @@ -136,12 +136,15 @@ impl<'a> Normalized<'a> { #[doc(hidden)] impl<'a> Type<'a> { pub(crate) fn unnote<'b>(self) -> Type<'b> { - use TypeInternal::*; - Type(match self.0 { - Expr(e) => Expr(Box::new(e.unnote())), - Const(c) => Const(c), - SuperType => SuperType, - }) + // use TypeInternal::*; + // Type(match self.0 { + // Expr(e) => Expr(Box::new(e.unnote())), + // Const(c) => Const(c), + // SuperType => SuperType, + // }) + + // Yes, this is positively horrible. Please forgive me. + unsafe { std::mem::transmute::, Type<'b>>(self) } } } 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, + // )), + // } } } diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index 19d7eee..37c95c5 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -78,15 +78,16 @@ impl Normalized<'static> { } impl<'a> Type<'a> { fn as_normalized(&self) -> Result>, TypeError> { - match &self.0 { - TypeInternal::Expr(e) => Ok(Cow::Borrowed(e)), - TypeInternal::Const(c) => Ok(Cow::Owned(const_to_normalized(*c))), - TypeInternal::SuperType => Err(TypeError::new( - &TypecheckContext::new(), - rc(ExprF::Const(Const::Sort)), - TypeMessage::Untyped, - )), - } + Ok(Cow::Owned(self.0.clone().into_normalized()?)) + // match &self.0 { + // TypeInternal::Expr(e) => Ok(Cow::Borrowed(e)), + // TypeInternal::Const(c) => Ok(Cow::Owned(const_to_normalized(*c))), + // TypeInternal::SuperType => Err(TypeError::new( + // &TypecheckContext::new(), + // rc(ExprF::Const(Const::Sort)), + // TypeMessage::Untyped, + // )), + // } } pub(crate) fn into_normalized(self) -> Result, TypeError> { self.0.into_normalized() @@ -427,20 +428,6 @@ macro_rules! ensure_equal { }; } -// Do not use with Const because they will never match -macro_rules! ensure_matches { - ($x:expr, $pat:pat => $branch:expr, $err:expr $(,)*) => { - match $x.unroll_ref()? { - Cow::Borrowed(e) => match e { - $pat => $branch, - _ => return Err($err), - }, - // Can't pattern match because lifetimes - Cow::Owned(_) => return Err($err), - } - }; -} - // Ensure the provided type has type `Type` macro_rules! ensure_simple_type { ($x:expr, $err:expr $(,)*) => {{ @@ -610,10 +597,11 @@ fn type_last_layer( }, App(f, a) => { let tf = f.get_type()?; - let (x, tx, tb) = ensure_matches!(tf, + let tf_expr = tf.unroll_ref()?; + let (x, tx, tb) = match tf_expr.as_ref() { Pi(x, tx, tb) => (x, tx, tb), - mkerr(NotAFunction(f)) - ); + _ => return Err(mkerr(NotAFunction(f))), + }; let tx = mktype(ctx, tx.embed_absurd())?; ensure_equal!(a.get_type()?, &tx, { mkerr(TypeMismatch(f, tx.into_normalized()?, a)) -- cgit v1.3.1 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/expr.rs | 11 +++- dhall/src/tests.rs | 9 ++- dhall/src/traits/deserialize.rs | 2 +- dhall/src/traits/static_type.rs | 1 + dhall/src/typecheck.rs | 135 +++++++++++++++++++++++++++++----------- 5 files changed, 118 insertions(+), 40 deletions(-) (limited to 'dhall/src/traits') diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs index 94093a9..1c3ec53 100644 --- a/dhall/src/expr.rs +++ b/dhall/src/expr.rs @@ -139,6 +139,7 @@ impl<'a> Type<'a> { // use TypeInternal::*; // Type(match self.0 { // Expr(e) => Expr(Box::new(e.unnote())), + // Pi(ctx, c, x, t, e) => Pi(ctx, c, x, t, e), // Const(c) => Const(c), // SuperType => SuperType, // }) @@ -150,6 +151,14 @@ impl<'a> Type<'a> { impl<'a> SimpleType<'a> { pub(crate) fn into_type(self) -> Type<'a> { - Normalized(self.0, Some(Type::const_type()), PhantomData).into_type() + self.into_type_ctx(&crate::typecheck::TypecheckContext::new()) + } + pub(crate) fn into_type_ctx( + self, + ctx: &crate::typecheck::TypecheckContext, + ) -> Type<'a> { + Normalized(self.0, Some(Type::const_type()), PhantomData) + .into_type_ctx(ctx) + .unwrap() } } diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs index c945b23..4d8fabd 100644 --- a/dhall/src/tests.rs +++ b/dhall/src/tests.rs @@ -71,7 +71,7 @@ pub fn run_test_with_bigger_stack( ) -> std::result::Result<(), String> { // Many tests stack overflow in debug mode let base_path: String = base_path.to_string(); - stacker::grow(4 * 1024 * 1024, move || { + stacker::grow(6 * 1024 * 1024, move || { run_test(&base_path, feature, status) .map_err(|e| e.to_string()) .map(|_| ()) @@ -135,12 +135,15 @@ pub fn run_test( assert_eq_display!(expr, expected); } Typecheck => { - expr.typecheck_with(&expected.into_type())?; + expr.typecheck_with(&expected.into_type()?)?; } TypeInference => { let expr = expr.typecheck()?; let ty = expr.get_type()?; - assert_eq_display!(ty.as_ref(), &expected.into_type()); + assert_eq_display!( + ty.as_normalized()?.as_expr(), + expected.into_type()?.as_normalized()?.as_expr() + ); } Normalization => { let expr = expr.skip_typecheck().normalize(); 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() } } diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index 6fb7cac..38b3d68 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -32,8 +32,11 @@ impl<'a> Resolved<'a> { } } impl<'a> Typed<'a> { - fn normalize_to_type(self) -> Type<'a> { - self.normalize().into_type() + fn normalize_to_type( + self, + ctx: &TypecheckContext, + ) -> Result, TypeError> { + Ok(self.normalize().into_type_ctx(ctx)?) } fn get_type_move(self) -> Result, TypeError> { let (expr, ty) = (self.0, self.1); @@ -54,11 +57,21 @@ impl<'a> Normalized<'a> { self.2, ) } - pub(crate) fn into_type(self) -> Type<'a> { - Type(match self.0.as_ref() { + pub(crate) fn into_type(self) -> Result, TypeError> { + self.into_type_ctx(&TypecheckContext::new()) + } + pub(crate) fn into_type_ctx( + self, + ctx: &TypecheckContext, + ) -> Result, TypeError> { + Ok(Type(match self.0.as_ref() { ExprF::Const(c) => TypeInternal::Const(*c), + ExprF::Pi(_, _, _) => { + return Ok(type_with(ctx, self.0.embed_absurd())? + .normalize_to_type(ctx)?) + } _ => TypeInternal::Expr(Box::new(self)), - }) + })) } fn get_type_move(self) -> Result, TypeError> { let (expr, ty) = (self.0, self.1); @@ -77,7 +90,9 @@ impl Normalized<'static> { } } impl<'a> Type<'a> { - fn as_normalized(&self) -> Result>, TypeError> { + pub(crate) fn as_normalized( + &self, + ) -> Result>, TypeError> { Ok(Cow::Owned(self.0.clone().into_normalized()?)) // match &self.0 { // TypeInternal::Expr(e) => Ok(Cow::Borrowed(e)), @@ -106,6 +121,13 @@ impl<'a> Type<'a> { use TypeInternal::*; Type(match &self.0 { Expr(e) => Expr(Box::new(e.shift0(delta, label))), + Pi(ctx, c, x, t, e) => Pi( + ctx.clone(), + *c, + x.clone(), + Box::new(t.shift0(delta, label)), + Box::new(e.shift0(delta, label)), + ), Const(c) => Const(*c), SuperType => SuperType, }) @@ -134,6 +156,13 @@ impl Type<'static> { #[derive(Debug, Clone, PartialEq, Eq)] pub(crate) enum TypeInternal<'a> { Const(Const), + Pi( + TypecheckContext, + Const, + Label, + Box>, + Box>, + ), /// The type of `Sort` SuperType, /// This must not contain a value captured by one of the variants above. @@ -144,6 +173,17 @@ impl<'a> TypeInternal<'a> { pub(crate) fn into_normalized(self) -> Result, TypeError> { match self { TypeInternal::Expr(e) => Ok(*e), + TypeInternal::Pi(ctx, c, x, t, e) => Ok(Typed( + rc(ExprF::Pi( + x, + t.into_normalized()?.embed(), + e.into_normalized()?.embed(), + )), + Some(const_to_type(c)), + ctx, + PhantomData, + ) + .normalize()), TypeInternal::Const(c) => Ok(const_to_normalized(c)), TypeInternal::SuperType => Err(TypeError::new( &TypecheckContext::new(), @@ -156,13 +196,32 @@ impl<'a> TypeInternal<'a> { #[derive(Debug, Clone)] pub(crate) enum TypedImproved { - // Pi(TypecheckContext, Const, Label, Type<'static>, Type<'static>), + Pi(TypecheckContext, Const, Label, Type<'static>, Type<'static>), Expr(Typed<'static>), } impl TypedImproved { fn into_typed(self) -> Result, TypeError> { match self { + TypedImproved::Pi(ctx, c, x, t, e) => Ok(Typed( + rc(ExprF::Pi( + x, + t.into_normalized()?.embed(), + e.into_normalized()?.embed(), + )), + Some(const_to_type(c)), + ctx, + PhantomData, + )), + TypedImproved::Expr(e) => Ok(e), + } + } + fn normalize_to_type( + self, + ctx: &TypecheckContext, + ) -> Result, TypeError> { + match self { + TypedImproved::Expr(e) => Ok(e.normalize_to_type(ctx)?), // TypedImproved::Pi(ctx, c, x, t, e) => Ok(Typed( // rc(ExprF::Pi( // x, @@ -172,12 +231,14 @@ impl TypedImproved { // Some(const_to_type(c)), // ctx, // PhantomData, - // )), - TypedImproved::Expr(e) => Ok(e), + // ) + // .normalize() + // .into_type()?), + TypedImproved::Pi(ctx, c, x, t, e) => { + Ok(Type(TypeInternal::Pi(ctx, c, x, Box::new(t), Box::new(e)))) + } } - } - fn normalize_to_type(self) -> Result, TypeError> { - Ok(self.into_typed()?.normalize_to_type()) + // Ok(self.into_typed()?.normalize_to_type()) } fn get_type(&self) -> Result>, TypeError> { Ok(Cow::Owned(self.clone().get_type_move()?)) @@ -332,12 +393,19 @@ 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)) => { + (TypeInternal::SuperType, _) => false, + (_, TypeInternal::SuperType) => false, + // (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()) + go( + &mut ctx, + eL0.borrow().as_normalized().unwrap().as_expr(), + eR0.borrow().as_normalized().unwrap().as_expr(), + ) } - _ => false, + // _ => false, } } @@ -465,15 +533,15 @@ fn mktype( ctx: &TypecheckContext, e: SubExpr>, ) -> Result, TypeError> { - Ok(type_with(ctx, e)?.normalize_to_type()?) + Ok(type_with(ctx, e)?.normalize_to_type(ctx)?) } -fn into_simple_type<'a>(e: SubExpr) -> Type<'a> { - SimpleType(e, PhantomData).into_type() +fn into_simple_type<'a>(ctx: &TypecheckContext, e: SubExpr) -> Type<'a> { + SimpleType(e, PhantomData).into_type_ctx(ctx) } fn simple_type_from_builtin<'a>(b: Builtin) -> Type<'a> { - into_simple_type(rc(ExprF::Builtin(b))) + into_simple_type(&TypecheckContext::new(), rc(ExprF::Builtin(b))) } /// Intermediary return type @@ -540,8 +608,8 @@ fn type_with( } }; - // return Ok(TypedImproved::Pi(ctx.clone(), k, x.clone(), ta, tb)); - Ok(RetExpr(Const(k))) + return Ok(TypedImproved::Pi(ctx.clone(), k, x.clone(), ta, tb)); + // Ok(RetExpr(Const(k))) } Let(x, t, v, e) => { let v = if let Some(t) = t { @@ -560,9 +628,8 @@ fn type_with( _ => type_last_layer( ctx, // Typecheck recursively all subexpressions - e.as_ref().traverse_ref_simple(|e| { - Ok(type_with(ctx, e.clone())?) - })?, + e.as_ref() + .traverse_ref_simple(|e| Ok(type_with(ctx, e.clone())?))?, e.clone(), ), }?; @@ -608,25 +675,23 @@ fn type_last_layer( None => Err(mkerr(UnboundVariable(var.clone()))), }, App(f, a) => { - let tf = f.get_type()?; - let tf_expr = tf.unroll_ref()?; - let (x, tx, tb) = match tf_expr.as_ref() { - Pi(x, tx, tb) => (x, tx, tb), + let tf = f.get_type()?.into_owned(); + let (x, tx, tb) = match tf.0 { + TypeInternal::Pi(_, _, x, tx, tb) => (x, tx, tb), _ => return Err(mkerr(NotAFunction(f))), }; - let tx = mktype(ctx, tx.embed_absurd())?; - ensure_equal!(a.get_type()?, &tx, { + ensure_equal!(a.get_type()?, tx.as_ref(), { mkerr(TypeMismatch(f, tx.into_normalized()?, a)) }); Ok(RetExpr(Let( x.clone(), None, a.normalize()?.embed(), - tb.embed_absurd(), + tb.into_normalized()?.into_expr().embed_absurd(), ))) } Annot(x, t) => { - let t = t.normalize_to_type()?; + let t = t.normalize_to_type(ctx)?; ensure_equal!( &t, x.get_type()?, @@ -660,7 +725,7 @@ fn type_last_layer( Ok(RetType(y.get_type_move()?)) } EmptyListLit(t) => { - let t = t.normalize_to_type()?; + let t = t.normalize_to_type(ctx)?; ensure_simple_type!( t, mkerr(InvalidListType(t.into_normalized()?)), @@ -788,7 +853,7 @@ fn type_last_layer( None => Err(mkerr(MissingRecordField(x, r))), }, _ => { - let r = r.normalize_to_type()?; + let r = r.normalize_to_type(ctx)?; match r.as_normalized()?.as_expr().as_ref() { UnionType(kts) => match kts.get(&x) { // Constructor has type T -> < x: T, ... > -- cgit v1.3.1 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/expr.rs | 3 +++ dhall/src/traits/dynamic_type.rs | 2 ++ 2 files changed, 5 insertions(+) (limited to 'dhall/src/traits') diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs index 1c3ec53..a548d32 100644 --- a/dhall/src/expr.rs +++ b/dhall/src/expr.rs @@ -114,6 +114,7 @@ impl<'a> From> for Typed<'a> { } #[doc(hidden)] +#[allow(dead_code)] impl<'a> Typed<'a> { pub(crate) fn as_expr(&self) -> &SubExpr> { &self.0 @@ -128,6 +129,7 @@ impl<'a> Normalized<'a> { pub(crate) fn into_expr(self) -> SubExpr { self.0 } + #[allow(dead_code)] pub(crate) fn unnote<'b>(self) -> Normalized<'b> { Normalized(self.0, self.1, PhantomData) } @@ -150,6 +152,7 @@ impl<'a> Type<'a> { } impl<'a> SimpleType<'a> { + #[allow(dead_code)] pub(crate) fn into_type(self) -> Type<'a> { self.into_type_ctx(&crate::typecheck::TypecheckContext::new()) } 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.3.1 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 ------- dhall/src/typecheck.rs | 62 +++++++++------------------------------- 2 files changed, 14 insertions(+), 59 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, )), } diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index 8fbebf0..948372f 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -35,9 +35,8 @@ impl<'a> Resolved<'a> { } impl<'a> Typed<'a> { fn get_type_move(self) -> Result, TypeError> { - let (expr, ty) = (self.0, self.1); - ty.ok_or_else(|| { - TypeError::new(&TypecheckContext::new(), expr, TypeMessage::Untyped) + self.1.ok_or_else(|| { + TypeError::new(&TypecheckContext::new(), TypeMessage::Untyped) }) } } @@ -73,13 +72,8 @@ impl<'a> Normalized<'a> { }) } fn get_type_move(self) -> Result, TypeError> { - let (expr, ty) = (self.0, self.1); - ty.ok_or_else(|| { - TypeError::new( - &TypecheckContext::new(), - expr.embed_absurd(), - TypeMessage::Untyped, - ) + self.1.ok_or_else(|| { + TypeError::new(&TypecheckContext::new(), TypeMessage::Untyped) }) } } @@ -157,6 +151,7 @@ impl TypeThunk { match self { TypeThunk::Type(t) => Ok(t), TypeThunk::Thunk(th) => { + // TODO: rule out statically mktype(ctx, th.normalize().normalize_to_expr().embed_absurd()) } } @@ -190,7 +185,6 @@ impl<'a> TypeInternal<'a> { TypeInternal::SuperType => { return Err(TypeError::new( &TypecheckContext::new(), - rc(ExprF::Const(Const::Sort)), TypeMessage::Untyped, )) } @@ -553,8 +547,7 @@ pub(crate) enum TypeIntermediate { impl TypeIntermediate { fn typecheck(self) -> Result { - let mkerr = - |ctx, msg| Ok(TypeError::new(ctx, self.clone().into_expr()?, msg)); + let mkerr = |ctx, msg| TypeError::new(ctx, msg); match &self { TypeIntermediate::Pi(ctx, x, ta, tb) => { let ctx2 = ctx.insert_type(x, ta.clone()); @@ -565,7 +558,7 @@ impl TypeIntermediate { return Err(mkerr( ctx, InvalidInputType(ta.clone().into_normalized()?), - )?) + )) } }; @@ -580,7 +573,7 @@ impl TypeIntermediate { .get_type_move()? .into_normalized()?, ), - )?) + )) } }; @@ -596,7 +589,7 @@ impl TypeIntermediate { .get_type_move()? .into_normalized()?, ), - )?) + )) } }; @@ -627,7 +620,7 @@ impl TypeIntermediate { x.clone(), TypedOrType::Type(t.clone()), ), - )?) + )) } } } @@ -665,7 +658,7 @@ impl TypeIntermediate { x.clone(), TypedOrType::Type(t.clone()), ), - )?) + )) } } } @@ -698,7 +691,7 @@ impl TypeIntermediate { TypeIntermediate::ListType(ctx, t) => { ensure_simple_type!( t, - mkerr(ctx, InvalidListType(t.clone().into_normalized()?))?, + mkerr(ctx, InvalidListType(t.clone().into_normalized()?)), ); let pnormalized = PartiallyNormalized( WHNF::from_builtin(Builtin::List) @@ -716,7 +709,7 @@ impl TypeIntermediate { mkerr( ctx, InvalidOptionalType(t.clone().into_normalized()?) - )?, + ), ); let pnormalized = PartiallyNormalized( WHNF::from_builtin(Builtin::Optional) @@ -730,26 +723,6 @@ impl TypeIntermediate { } } } - fn into_expr(self) -> Result>, TypeError> { - Ok(rc(match self { - TypeIntermediate::Pi(_, x, t, e) => ExprF::Pi(x, t, e), - TypeIntermediate::RecordType(_, kts) => ExprF::RecordType(kts), - TypeIntermediate::UnionType(_, kts) => ExprF::UnionType(kts), - TypeIntermediate::ListType(_, t) => { - return Ok(rc(ExprF::App( - rc(ExprF::Builtin(Builtin::List)), - t.embed()?, - ))) - } - TypeIntermediate::OptionalType(_, t) => { - return Ok(rc(ExprF::App( - rc(ExprF::Builtin(Builtin::Optional)), - t.embed()?, - ))) - } - } - .traverse_ref_simple(|e| e.clone().embed())?)) - } } /// Takes an expression that is meant to contain a Type @@ -836,7 +809,6 @@ fn type_with( // Typecheck recursively all subexpressions e.as_ref() .traverse_ref_simple(|e| Ok(type_with(ctx, e.clone())?))?, - e.clone(), ), }?; match ret { @@ -861,14 +833,11 @@ fn type_with( fn type_last_layer( ctx: &TypecheckContext, e: ExprF>, - original_e: SubExpr>, ) -> Result { use dhall_core::BinOp::*; use dhall_core::Builtin::*; use dhall_core::ExprF::*; - let mkerr = |msg: TypeMessage<'static>| { - TypeError::new(ctx, original_e.clone(), msg) - }; + let mkerr = |msg: TypeMessage<'static>| TypeError::new(ctx, msg); use Ret::*; match e { @@ -1149,18 +1118,15 @@ pub(crate) enum TypeMessage<'a> { pub struct TypeError { type_message: TypeMessage<'static>, context: TypecheckContext, - current: SubExpr>, } impl TypeError { pub(crate) fn new( context: &TypecheckContext, - current: SubExpr>, type_message: TypeMessage<'static>, ) -> Self { TypeError { context: context.clone(), - current, type_message, } } -- cgit v1.3.1 From 5465b7e2b8cc286e2e8b87556b3ec6a2476cf0cf Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 2 May 2019 12:54:35 +0200 Subject: Tweaks --- dhall/src/normalize.rs | 84 +++++++++++++++++++---------------------- dhall/src/traits/static_type.rs | 2 +- dhall/src/typecheck.rs | 68 ++++++++++++++++++--------------- 3 files changed, 78 insertions(+), 76 deletions(-) (limited to 'dhall/src/traits') diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs index dbb6d95..7a69bea 100644 --- a/dhall/src/normalize.rs +++ b/dhall/src/normalize.rs @@ -383,8 +383,8 @@ impl Value { match self { Value::Lam(x, t, e) => rc(ExprF::Lam( x.clone(), - t.normalize_nf().normalize_to_expr(), - e.normalize_nf().normalize_to_expr(), + t.normalize_to_expr(), + e.normalize_to_expr(), )), Value::AppliedBuiltin(b, args) => { let mut e = rc(ExprF::Builtin(*b)); @@ -394,18 +394,18 @@ impl Value { e } Value::OptionalSomeClosure(n) => { - let a = n.normalize_nf().normalize_to_expr(); + let a = n.normalize_to_expr(); dhall::subexpr!(λ(x: a) -> Some x) } Value::ListConsClosure(n, None) => { - let a = n.normalize_nf().normalize_to_expr(); + let a = n.normalize_to_expr(); // Avoid accidental capture of the new `x` variable let a1 = a.shift0(1, &"x".into()); dhall::subexpr!(λ(x : a) -> λ(xs : List a1) -> [ x ] # xs) } Value::ListConsClosure(n, Some(v)) => { - let v = v.normalize_nf().normalize_to_expr(); - let a = n.normalize_nf().normalize_to_expr(); + let v = v.normalize_to_expr(); + let a = n.normalize_to_expr(); // Avoid accidental capture of the new `xs` variable let v = v.shift0(1, &"xs".into()); dhall::subexpr!(λ(xs : List a) -> [ v ] # xs) @@ -415,8 +415,8 @@ impl Value { } Value::Pi(x, t, e) => rc(ExprF::Pi( x.clone(), - t.normalize_nf().normalize_to_expr(), - e.normalize_nf().normalize_to_expr(), + t.normalize_to_expr(), + e.normalize_to_expr(), )), Value::Var(v) => rc(ExprF::Var(v.clone())), Value::Const(c) => rc(ExprF::Const(*c)), @@ -425,41 +425,31 @@ impl Value { Value::IntegerLit(n) => rc(ExprF::IntegerLit(*n)), Value::EmptyOptionalLit(n) => rc(ExprF::App( rc(ExprF::Builtin(Builtin::OptionalNone)), - n.normalize_nf().normalize_to_expr(), + n.normalize_to_expr(), )), Value::NEOptionalLit(n) => { - rc(ExprF::SomeLit(n.normalize_nf().normalize_to_expr())) + rc(ExprF::SomeLit(n.normalize_to_expr())) } Value::EmptyListLit(n) => { - rc(ExprF::EmptyListLit(n.normalize_nf().normalize_to_expr())) + rc(ExprF::EmptyListLit(n.normalize_to_expr())) } Value::NEListLit(elts) => rc(ExprF::NEListLit( - elts.into_iter() - .map(|n| n.normalize_nf().normalize_to_expr()) - .collect(), + elts.into_iter().map(|n| n.normalize_to_expr()).collect(), )), Value::RecordLit(kvs) => rc(ExprF::RecordLit( kvs.iter() - .map(|(k, v)| { - (k.clone(), v.normalize_nf().normalize_to_expr()) - }) + .map(|(k, v)| (k.clone(), v.normalize_to_expr())) .collect(), )), Value::RecordType(kts) => rc(ExprF::RecordType( kts.iter() - .map(|(k, v)| { - (k.clone(), v.normalize_nf().normalize_to_expr()) - }) + .map(|(k, v)| (k.clone(), v.normalize_to_expr())) .collect(), )), Value::UnionType(kts) => rc(ExprF::UnionType( kts.iter() .map(|(k, v)| { - ( - k.clone(), - v.as_ref() - .map(|v| v.normalize_nf().normalize_to_expr()), - ) + (k.clone(), v.as_ref().map(|v| v.normalize_to_expr())) }) .collect(), )), @@ -467,25 +457,17 @@ impl Value { let kts = kts .iter() .map(|(k, v)| { - ( - k.clone(), - v.as_ref() - .map(|v| v.normalize_nf().normalize_to_expr()), - ) + (k.clone(), v.as_ref().map(|v| v.normalize_to_expr())) }) .collect(); rc(ExprF::Field(rc(ExprF::UnionType(kts)), l.clone())) } Value::UnionLit(l, v, kts) => rc(ExprF::UnionLit( l.clone(), - v.normalize_nf().normalize_to_expr(), + v.normalize_to_expr(), kts.iter() .map(|(k, v)| { - ( - k.clone(), - v.as_ref() - .map(|v| v.normalize_nf().normalize_to_expr()), - ) + (k.clone(), v.as_ref().map(|v| v.normalize_to_expr())) }) .collect(), )), @@ -961,7 +943,10 @@ impl Value { } mod thunk { - use super::{normalize_whnf, InputSubExpr, NormalizationContext, Value}; + use super::{ + normalize_whnf, InputSubExpr, NormalizationContext, OutputSubExpr, + Value, + }; use crate::expr::Typed; use dhall_core::{Label, V}; use std::cell::{Ref, RefCell}; @@ -1108,6 +1093,10 @@ mod thunk { Ref::map(self.0.borrow(), ThunkInternal::as_nf) } + pub(crate) fn normalize_to_expr(&self) -> OutputSubExpr { + self.normalize_nf().normalize_to_expr() + } + pub(crate) fn shift(&self, delta: isize, var: &V