summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorNadrieril2019-08-25 16:33:12 +0200
committerNadrieril2019-08-25 16:37:31 +0200
commit80fb5355ea90377492b9863f632c01a808f8aade (patch)
treee9de4459615e601da64862e26c56c68b4265999e
parent98399997cf289d802fbed674558665547cf73d59 (diff)
Check consistency of type information
-rw-r--r--dhall/src/core/value.rs53
-rw-r--r--dhall/src/phase/normalize.rs4
2 files changed, 30 insertions, 27 deletions
diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index 6f9f78a..7f98826 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -71,22 +71,13 @@ impl ValueInternal {
},
|vint| match &vint.form {
Unevaled => {
- let (value, ty) = (vint.value, vint.ty);
- let vovf = normalize_whnf(value, ty.as_ref());
- // let was_value = if let VoVF::Value(_) = &vovf {
- // true
- // } else {
- // false
- // };
- let (new_val, _new_ty) =
- vovf.into_whnf_and_type(ty.as_ref());
- // if was_value {
- // debug_assert_eq!(ty, new_ty);
- // }
+ let new_value =
+ normalize_whnf(vint.value, vint.ty.as_ref())
+ .into_whnf(vint.ty.as_ref());
ValueInternal {
form: WHNF,
- value: new_val,
- ty: ty,
+ value: new_value,
+ ty: vint.ty,
}
}
// Already in WHNF
@@ -254,18 +245,23 @@ impl Value {
}
impl VoVF {
- pub(crate) fn into_whnf_and_type(
- self,
- ty: Option<&Value>,
- ) -> (ValueF, Option<Value>) {
+ pub(crate) fn into_whnf(self, ty: Option<&Value>) -> ValueF {
match self {
VoVF::ValueF {
val,
form: Unevaled,
- } => normalize_whnf(val, ty).into_whnf_and_type(ty),
+ } => normalize_whnf(val, ty).into_whnf(ty),
// Already at lest in WHNF
- VoVF::ValueF { val, .. } => (val, None),
- VoVF::Value(v) => (v.to_whnf(), v.get_type().ok()),
+ VoVF::ValueF { val, .. } => val,
+ VoVF::Value(v) => {
+ let v_ty = v.get_type().ok();
+ debug_assert_eq!(
+ ty,
+ v_ty.as_ref(),
+ "The type recovered from normalization doesn't match the stored type."
+ );
+ v.to_whnf()
+ }
}
}
pub(crate) fn into_value_untyped(self) -> Value {
@@ -274,11 +270,18 @@ impl VoVF {
VoVF::ValueF { val, form } => Value::new(val, form, None),
}
}
- pub(crate) fn into_value_with_type(self, t: Value) -> Value {
+ pub(crate) fn into_value_with_type(self, ty: Value) -> Value {
match self {
- // TODO: check type with debug_assert ?
- VoVF::Value(v) => v,
- VoVF::ValueF { val, form } => Value::new(val, form, Some(t)),
+ VoVF::Value(v) => {
+ let v_ty = v.get_type().ok();
+ debug_assert_eq!(
+ Some(&ty),
+ v_ty.as_ref(),
+ "The type recovered from normalization doesn't match the stored type."
+ );
+ v
+ }
+ VoVF::ValueF { val, form } => Value::new(val, form, Some(ty)),
}
}
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index 5743b0d..fe99696 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -61,8 +61,8 @@ macro_rules! make_closure {
(Some($($rest:tt)*)) => {{
let v = make_closure!($($rest)*);
let v_type = v.get_type().expect("Internal type error");
- ValueF::NEOptionalLit(v)
- .into_value_with_type(v_type)
+ let opt_v_type = Value::from_builtin(Builtin::Optional).app(v_type);
+ ValueF::NEOptionalLit(v).into_value_with_type(opt_v_type)
}};
(1 + $($rest:tt)*) => {
ValueF::PartialExpr(ExprF::BinOp(