diff options
author | Nadrieril | 2019-08-25 16:33:12 +0200 |
---|---|---|
committer | Nadrieril | 2019-08-25 16:37:31 +0200 |
commit | 80fb5355ea90377492b9863f632c01a808f8aade (patch) | |
tree | e9de4459615e601da64862e26c56c68b4265999e | |
parent | 98399997cf289d802fbed674558665547cf73d59 (diff) |
Check consistency of type information
-rw-r--r-- | dhall/src/core/value.rs | 53 | ||||
-rw-r--r-- | dhall/src/phase/normalize.rs | 4 |
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( |