From ec349d42703a8a31715cf97b44845ba3dd7a6805 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 20 Aug 2019 22:20:59 +0200 Subject: Propagate type information in Value::app() --- dhall/src/core/value.rs | 23 +++++++++++++++-------- 1 file changed, 15 insertions(+), 8 deletions(-) (limited to 'dhall/src/core') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index b44dad6..24e2803 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -214,8 +214,18 @@ impl Value { self.as_nf().normalize_to_expr_maybe_alpha(alpha) } - pub(crate) fn app(&self, v: Value) -> VoVF { - apply_any(self.clone(), v) + pub(crate) fn app(&self, v: Value) -> Value { + let vovf = apply_any(self.clone(), v.clone()); + match self.as_internal().get_type() { + Err(_) => vovf.into_value_untyped(), + Ok(t) => match &*t.as_whnf() { + ValueF::Pi(x, _, e) => { + let t = e.subst_shift(&x.into(), &v); + vovf.into_value_with_type(t) + } + _ => unreachable!("Internal type error"), + }, + } } pub(crate) fn get_type(&self) -> Result { @@ -248,15 +258,12 @@ impl VoVF { VoVF::ValueF { val, form } => Value::new(val, form, Some(t)), } } - pub(crate) fn into_value_simple_type(self) -> Value { - self.into_value_with_type(Value::from_const(Const::Type)) - } - pub(crate) fn app(self, x: Value) -> Self { - match self { + pub(crate) fn app(self, x: Value) -> VoVF { + VoVF::Value(match self { VoVF::Value(v) => v.app(x), VoVF::ValueF { val, .. } => val.into_value_untyped().app(x), - } + }) } } -- cgit v1.2.3