From 53f886c0f5044e4bfe7de756b8c47d992f91b03e Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 22 Apr 2019 23:14:20 +0200 Subject: Pass through new TypedImproved type --- dhall/src/typecheck.rs | 117 ++++++++++++++++++++++++++++++++++++++----------- 1 file changed, 92 insertions(+), 25 deletions(-) diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index a53e88a..19d7eee 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -32,6 +32,9 @@ impl<'a> Resolved<'a> { } } impl<'a> Typed<'a> { + fn normalize_to_type(self) -> Type<'a> { + self.normalize().into_type() + } fn get_type_move(self) -> Result, TypeError> { let (expr, ty) = (self.0, self.1); ty.ok_or_else(|| { @@ -57,6 +60,16 @@ impl<'a> Normalized<'a> { _ => TypeInternal::Expr(Box::new(self)), }) } + 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, + ) + }) + } } impl Normalized<'static> { fn embed(self) -> SubExpr> { @@ -140,6 +153,30 @@ impl<'a> TypeInternal<'a> { } } +#[derive(Debug, Clone)] +pub(crate) enum TypedImproved { + // 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), + } + } +} + #[derive(Debug, Clone)] pub(crate) enum EnvItem { Type(V