From 85dca9313efea9618dc4e3dd2e002ad4b5a02515 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 16 Apr 2019 15:53:22 +0200 Subject: Avoid some work duplication in typechecking --- dhall/src/expr.rs | 3 -- dhall/src/typecheck.rs | 104 ++++++++++++++++++++++++++----------------------- 2 files changed, 56 insertions(+), 51 deletions(-) (limited to 'dhall') diff --git a/dhall/src/expr.rs b/dhall/src/expr.rs index a84b41d..cda1d8d 100644 --- a/dhall/src/expr.rs +++ b/dhall/src/expr.rs @@ -116,9 +116,6 @@ impl<'a> Normalized<'a> { pub(crate) fn as_expr(&self) -> &SubExpr { &self.0 } - pub(crate) fn into_expr(self) -> SubExpr { - self.0.absurd() - } pub(crate) fn into_type(self) -> Type<'a> { crate::expr::Type(TypeInternal::Expr(Box::new(self))) } diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index 5162f4f..86c5ebd 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -48,6 +48,11 @@ impl<'a> Normalized<'a> { Normalized(shift(delta, var, &self.0), self.1.clone(), self.2) } } +impl Normalized<'static> { + fn embed(self) -> SubExpr> { + rc(ExprF::Embed(self)) + } +} impl<'a> Type<'a> { pub(crate) fn as_normalized(&self) -> Result<&Normalized<'a>, TypeError> { use TypeInternal::*; @@ -108,6 +113,11 @@ impl<'a> Type<'a> { .into_type() } } +impl Type<'static> { + fn embed(self) -> Result>, TypeError> { + Ok(self.into_normalized()?.embed()) + } +} fn function_check(a: Const, b: Const) -> Result { use dhall_core::Const::*; @@ -348,27 +358,27 @@ fn type_with( let b = type_with(&ctx2, b.clone())?; Ok(RetExpr(Pi( x.clone(), - t.into_normalized()?.into_expr(), - b.get_type_move()?.into_normalized()?.into_expr(), + t.embed()?, + b.get_type_move()?.embed()?, ))) } - Pi(x, tA, tB) => { - let tA = mktype(ctx, tA.clone())?; + Pi(x, ta, tb) => { + let ta = mktype(ctx, ta.clone())?; let kA = ensure_is_const!( - &tA.get_type()?, - mkerr(InvalidInputType(tA.into_normalized()?)), + &ta.get_type()?, + mkerr(InvalidInputType(ta.into_normalized()?)), ); let ctx2 = ctx - .insert(x.clone(), tA.clone()) + .insert(x.clone(), ta.clone()) .map(|e| e.shift(1, &V(x.clone(), 0))); - let tB = type_with(&ctx2, tB.clone())?; + let tb = type_with(&ctx2, tb.clone())?; let kB = ensure_is_const!( - &tB.get_type()?, + &tb.get_type()?, TypeError::new( &ctx2, e.clone(), - InvalidOutputType(tB.get_type_move()?.into_normalized()?), + InvalidOutputType(tb.get_type_move()?.into_normalized()?), ), ); @@ -376,8 +386,8 @@ fn type_with( Ok(k) => k, Err(()) => { return Err(mkerr(NoDependentTypes( - tA.clone().into_normalized()?, - tB.get_type_move()?.into_normalized()?, + ta.clone().into_normalized()?, + tb.get_type_move()?.into_normalized()?, ))) } }; @@ -395,7 +405,7 @@ fn type_with( let e = type_with( ctx, // TODO: Use a substitution context - subst_shift(&V(x.clone(), 0), &v.as_expr().absurd(), e), + subst_shift(&V(x.clone(), 0), &v.embed(), e), )?; Ok(RetType(e.get_type_move()?)) @@ -442,17 +452,20 @@ fn type_last_layer( }, App(f, args) => { let mut tf = f.get_type()?.into_owned(); + // Reconstruct the application `f a0 a1 ...` + // for error reporting + let mkf = |args: Vec<_>, i| { + rc(App( + f.into_expr(), + args.into_iter().take(i).map(Typed::into_expr).collect(), + )) + }; + for (i, a) in args.iter().enumerate() { let (x, tx, tb) = ensure_matches!(tf, Pi(x, tx, tb) => (x, tx, tb), mkerr(NotAFunction(Typed( - rc(App( - f.into_expr(), - args.into_iter() - .take(i) - .map(Typed::into_expr) - .collect() - )), + mkf(args, i), Some(tf), PhantomData ))) @@ -461,24 +474,19 @@ fn type_last_layer( ensure_equal!(&tx, a.get_type()?, { let a = a.clone(); mkerr(TypeMismatch( - Typed( - rc(App( - f.into_expr(), - args.into_iter() - .take(i + 1) - .map(Typed::into_expr) - .collect(), - )), - Some(tf), - PhantomData, - ), + Typed(mkf(args, i + 1), Some(tf), PhantomData), tx.into_normalized()?, a, )) }); tf = mktype( ctx, - rc(Let(x.clone(), None, a.as_expr().clone(), tb.absurd())), + rc(Let( + x.clone(), + None, + a.clone().normalize().embed(), + tb.absurd(), + )), )?; } Ok(RetType(tf)) @@ -523,7 +531,7 @@ fn type_last_layer( t, mkerr(InvalidListType(t.into_normalized()?)), ); - let t = t.into_normalized()?.into_expr(); + let t = t.embed()?; Ok(RetExpr(dhall::expr!(List t))) } NEListLit(xs) => { @@ -544,43 +552,41 @@ fn type_last_layer( )) ); } - let t = x.get_type_move()?.into_normalized()?.into_expr(); + let t = x.get_type_move()?; + let t = t.embed()?; Ok(RetExpr(dhall::expr!(List t))) } OldOptionalLit(None, t) => { - let t = t.into_expr(); + let t = t.normalize().embed(); let e = dhall::subexpr!(None t); Ok(RetType(type_with(ctx, e)?.get_type()?.into_owned())) } OldOptionalLit(Some(x), t) => { - let x = x.into_expr(); - let t = t.into_expr(); + let t = t.normalize().embed(); + let x = x.normalize().embed(); let e = dhall::subexpr!(Some x : Optional t); Ok(RetType(type_with(ctx, e)?.get_type()?.into_owned())) } EmptyOptionalLit(t) => { - let t = t.normalize().into_type(); - ensure_simple_type!( - t, - mkerr(InvalidOptionalType(t.into_normalized()?)), - ); - let t = t.into_normalized()?.into_expr(); + let t = t.normalize(); + ensure_simple_type!(t, mkerr(InvalidOptionalType(t))); + let t = t.embed(); Ok(RetExpr(dhall::expr!(Optional t))) } NEOptionalLit(x) => { let tx = x.get_type_move()?; ensure_simple_type!( tx, - mkerr(InvalidOptionalType(tx.into_normalized()?,)), + mkerr(InvalidOptionalType(tx.into_normalized()?)), ); - let t = tx.into_normalized()?.into_expr(); + let t = tx.embed()?; Ok(RetExpr(dhall::expr!(Optional t))) } RecordType(kts) => { for (k, t) in kts { - ensure_simple_type!(t, mkerr(InvalidFieldType(k, t)),); + ensure_simple_type!(t, mkerr(InvalidFieldType(k, t))); } - Ok(RetExpr(dhall::expr!(Type))) + Ok(RetType(crate::expr::Type::const_type())) } RecordLit(kvs) => { let kts = kvs @@ -590,7 +596,9 @@ fn type_last_layer( v.get_type()?, mkerr(InvalidField(k, v)), ); - Ok((k, v.get_type_move()?.into_normalized()?.into_expr())) + let t = v.get_type_move()?; + let t = t.embed()?; + Ok((k, t)) }) .collect::>()?; Ok(RetExpr(RecordType(kts))) -- cgit v1.2.3