summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/src/core/value.rs23
-rw-r--r--dhall/src/phase/normalize.rs35
-rw-r--r--dhall/src/phase/typecheck.rs10
3 files changed, 33 insertions, 35 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),
- }
+ })
}
}
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index a146ec7..e4a0c5b 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -34,7 +34,6 @@ macro_rules! make_closure {
(List $($rest:tt)*) => {
Value::from_builtin(Builtin::List)
.app(make_closure!($($rest)*))
- .into_value_simple_type()
};
(Some($($rest:tt)*)) => {
ValueF::NEOptionalLit(make_closure!($($rest)*))
@@ -251,9 +250,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
}
}
_ => {
- let list_t = Value::from_builtin(List)
- .app(t.clone())
- .into_value_simple_type();
+ let list_t = Value::from_builtin(List).app(t.clone());
Ok((
r,
f.app(list_t.clone())
@@ -269,18 +266,19 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
.app(
EmptyListLit(t.clone())
.into_value_with_type(list_t),
- ),
+ )
+ .into_vovf(),
))
}
},
(ListFold, [_, l, _, cons, nil, r..]) => match &*l.as_whnf() {
EmptyListLit(_) => Ok((r, nil.clone().into_vovf())),
NEListLit(xs) => {
- let mut v = nil.clone().into_vovf();
+ let mut v = nil.clone();
for x in xs.iter().cloned().rev() {
- v = cons.app(x).app(v.into_value_untyped());
+ v = cons.app(x).app(v);
}
- Ok((r, v))
+ Ok((r, v.into_vovf()))
}
_ => Err(()),
},
@@ -295,9 +293,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
}
}
_ => {
- let optional_t = Value::from_builtin(Optional)
- .app(t.clone())
- .into_value_simple_type();
+ let optional_t = Value::from_builtin(Optional).app(t.clone());
Ok((
r,
f.app(optional_t.clone())
@@ -305,13 +301,14 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
.app(
EmptyOptionalLit(t.clone())
.into_value_with_type(optional_t),
- ),
+ )
+ .into_vovf(),
))
}
},
(OptionalFold, [_, v, _, just, nothing, r..]) => match &*v.as_whnf() {
EmptyOptionalLit(_) => Ok((r, nothing.clone().into_vovf())),
- NEOptionalLit(x) => Ok((r, just.app(x.clone()))),
+ NEOptionalLit(x) => Ok((r, just.app(x.clone()).into_vovf())),
_ => Err(()),
},
(NaturalBuild, [f, r..]) => match &*f.as_whnf() {
@@ -331,7 +328,8 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
.app(
NaturalLit(0)
.into_value_with_type(Value::from_builtin(Natural)),
- ),
+ )
+ .into_vovf(),
)),
},
(NaturalFold, [n, t, succ, zero, r..]) => match &*n.as_whnf() {
@@ -344,9 +342,8 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> VoVF {
)
.app(t.clone())
.app(succ.clone())
- .app(zero.clone())
- .into_value_with_type(t.clone());
- Ok((r, succ.app(fold)))
+ .app(zero.clone());
+ Ok((r, succ.app(fold).into_vovf()))
}
_ => Err(()),
},
@@ -643,7 +640,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> VoVF {
ExprF::Lam(x, t, e) => Ret::ValueF(Lam(x.into(), t, e)),
ExprF::Pi(x, t, e) => Ret::ValueF(Pi(x.into(), t, e)),
ExprF::Let(x, _, v, b) => Ret::Value(b.subst_shift(&x.into(), &v)),
- ExprF::App(v, a) => Ret::VoVF(v.app(a)),
+ ExprF::App(v, a) => Ret::Value(v.app(a)),
ExprF::Builtin(b) => Ret::ValueF(ValueF::from_builtin(b)),
ExprF::Const(c) => Ret::ValueF(ValueF::Const(c)),
ExprF::BoolLit(b) => Ret::ValueF(BoolLit(b)),
@@ -765,7 +762,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> VoVF {
}
},
(RecordLit(kvs), UnionLit(l, v, _)) => match kvs.get(l) {
- Some(h) => Ret::VoVF(h.app(v.clone())),
+ Some(h) => Ret::Value(h.app(v.clone())),
None => {
drop(handlers_borrow);
drop(variant_borrow);
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index 4abc314..abe05a3 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -455,11 +455,7 @@ fn type_last_layer(
return mkerr(InvalidListType(t));
}
- RetTypeOnly(
- ValueF::from_builtin(dhall_syntax::Builtin::List)
- .app(t)
- .into_value_simple_type(),
- )
+ RetTypeOnly(Value::from_builtin(dhall_syntax::Builtin::List).app(t))
}
SomeLit(x) => {
let t = x.get_type()?;
@@ -468,9 +464,7 @@ fn type_last_layer(
}
RetTypeOnly(
- Value::from_builtin(dhall_syntax::Builtin::Optional)
- .app(t)
- .into_value_simple_type(),
+ Value::from_builtin(dhall_syntax::Builtin::Optional).app(t),
)
}
RecordType(kts) => RetWhole(tck_record_type(