diff options
Diffstat (limited to '')
-rw-r--r-- | dhall/src/typecheck.rs | 90 |
1 files changed, 45 insertions, 45 deletions
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index e04bf0d..8fbebf0 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -108,6 +108,11 @@ impl<'a> Type<'a> { fn normalize_whnf(self) -> Result<WHNF, TypeError> { self.0.normalize_whnf() } + pub(crate) fn partially_normalize( + self, + ) -> Result<PartiallyNormalized<'a>, TypeError> { + self.0.partially_normalize() + } fn internal(&self) -> &TypeInternal<'a> { &self.0 } @@ -120,37 +125,12 @@ impl<'a> Type<'a> { pub(crate) fn shift(&self, delta: isize, var: &V<Label>) -> Self { Type(self.0.shift(delta, var)) } - fn subst( - self, - ctx: &TypecheckContext, - x: &Label, - val: Normalized<'static>, - ) -> Result<Self, TypeError> { - let tval = val.get_type()?.into_owned(); - let ctx_type = ctx.insert_type(x, tval); - let ctx_val = ctx.insert_value(x, val); - - let pnzed = match self.0 { - TypeInternal::PNzed(e) => e, - internal => return Ok(Type(internal)), - }; - let nzed = pnzed.normalize(); - let pnzed = Typed(nzed.0.embed_absurd(), nzed.1, ctx_val, nzed.2) - .normalize_whnf(); - - Ok(match &pnzed.0 { - WHNF::Expr(e) => { - let e = e.clone(); - match e.as_ref() { - ExprF::Pi(_, _, _) | ExprF::RecordType(_) => { - type_with(&ctx_type, e.embed_absurd())? - .normalize_to_type() - } - _ => pnzed.normalize_to_type(), - } - } - _ => pnzed.normalize_to_type(), - }) + pub(crate) fn subst_shift( + &self, + var: &V<Label>, + val: &PartiallyNormalized<'static>, + ) -> Self { + Type(self.0.subst_shift(var, val)) } fn const_sort() -> Self { @@ -198,9 +178,15 @@ pub(crate) enum TypeInternal<'a> { impl<'a> TypeInternal<'a> { pub(crate) fn into_normalized(self) -> Result<Normalized<'a>, TypeError> { + Ok(self.partially_normalize()?.normalize()) + } + fn normalize_whnf(self) -> Result<WHNF, TypeError> { + Ok(self.partially_normalize()?.into_whnf()) + } + fn partially_normalize(self) -> Result<PartiallyNormalized<'a>, TypeError> { Ok(match self { - TypeInternal::PNzed(e) => e.normalize(), - TypeInternal::Const(c) => const_to_normalized(c), + TypeInternal::PNzed(e) => *e, + TypeInternal::Const(c) => const_to_pnormalized(c), TypeInternal::SuperType => { return Err(TypeError::new( &TypecheckContext::new(), @@ -210,10 +196,6 @@ impl<'a> TypeInternal<'a> { } }) } - fn normalize_whnf(self) -> Result<WHNF, TypeError> { - let typed: Typed = self.into_normalized()?.into(); - Ok(typed.normalize_whnf().0) - } fn whnf(&self) -> Option<&WHNF> { match self { TypeInternal::PNzed(e) => Some(&e.0), @@ -231,6 +213,18 @@ impl<'a> TypeInternal<'a> { SuperType => SuperType, } } + fn subst_shift( + &self, + var: &V<Label>, + val: &PartiallyNormalized<'static>, + ) -> Self { + use TypeInternal::*; + match self { + PNzed(e) => PNzed(Box::new(e.subst_shift(var, val))), + Const(c) => Const(*c), + SuperType => SuperType, + } + } } impl<'a> Eq for TypeInternal<'a> {} @@ -260,7 +254,9 @@ impl TypedOrType { } fn normalize_to_type(self) -> Type<'static> { match self { - TypedOrType::Typed(e) => e.normalize_whnf().normalize_to_type(), + TypedOrType::Typed(e) => { + e.partially_normalize().normalize_to_type() + } TypedOrType::Type(t) => t, } } @@ -276,10 +272,12 @@ impl TypedOrType { TypedOrType::Type(t) => Ok(t.get_type()?.into_owned()), } } - fn normalize(self) -> Result<Normalized<'static>, TypeError> { + fn partially_normalize( + self, + ) -> Result<PartiallyNormalized<'static>, TypeError> { match self { - TypedOrType::Typed(e) => Ok(e.normalize()), - TypedOrType::Type(t) => Ok(t.into_normalized()?), + TypedOrType::Typed(e) => Ok(e.partially_normalize()), + TypedOrType::Type(t) => Ok(t.partially_normalize()?), } } } @@ -443,8 +441,8 @@ where } } -fn const_to_normalized<'a>(c: Const) -> Normalized<'a> { - Normalized(rc(ExprF::Const(c)), Some(type_of_const(c)), PhantomData) +fn const_to_pnormalized<'a>(c: Const) -> PartiallyNormalized<'a> { + PartiallyNormalized(WHNF::Const(c), Some(type_of_const(c)), PhantomData) } fn const_to_type<'a>(c: Const) -> Type<'a> { @@ -897,7 +895,9 @@ fn type_last_layer( mkerr(TypeMismatch(f.clone(), tx.clone().into_normalized()?, a)) }); - Ok(RetType(tb.clone().subst(&ctx, x, a.normalize()?)?)) + Ok(RetType( + tb.subst_shift(&V(x.clone(), 0), &a.partially_normalize()?), + )) } Annot(x, t) => { let t = t.normalize_to_type(); @@ -1147,9 +1147,9 @@ pub(crate) enum TypeMessage<'a> { /// A structured type error that includes context #[derive(Debug)] pub struct TypeError { + type_message: TypeMessage<'static>, context: TypecheckContext, current: SubExpr<X, Normalized<'static>>, - type_message: TypeMessage<'static>, } impl TypeError { |