summaryrefslogtreecommitdiff
path: root/dhall/src/core
diff options
context:
space:
mode:
authorNadrieril2019-08-20 22:20:59 +0200
committerNadrieril2019-08-20 22:20:59 +0200
commitec349d42703a8a31715cf97b44845ba3dd7a6805 (patch)
tree877f5fc4b2f6b6c5dff6090680bf8b4d51120d6d /dhall/src/core
parentf70e45daef2570259eccd227a0126493c015d7b0 (diff)
Propagate type information in Value::app()
Diffstat (limited to 'dhall/src/core')
-rw-r--r--dhall/src/core/value.rs23
1 files changed, 15 insertions, 8 deletions
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<Value, TypeError> {
@@ -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),
- }
+ })
}
}