From 04438824db21fb5d9d3a2abdb3fa167875bda892 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 20 Aug 2019 16:39:27 +0200 Subject: Add Value::from_builtin --- dhall/src/core/value.rs | 7 +++++-- dhall/src/core/valuef.rs | 10 ---------- 2 files changed, 5 insertions(+), 12 deletions(-) (limited to 'dhall/src/core') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 5367c86..f897f16 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -2,14 +2,14 @@ use std::borrow::Cow; use std::cell::{Ref, RefCell, RefMut}; use std::rc::Rc; -use dhall_syntax::Const; +use dhall_syntax::{Builtin, Const}; use crate::core::context::TypecheckContext; use crate::core::valuef::ValueF; use crate::core::var::{AlphaVar, Shift, Subst}; use crate::error::{TypeError, TypeMessage}; use crate::phase::normalize::{apply_any, normalize_whnf, OutputSubExpr}; -use crate::phase::typecheck::const_to_value; +use crate::phase::typecheck::{builtin_to_value, const_to_value}; use crate::phase::{NormalizedSubExpr, Typed}; #[derive(Debug, Clone, Copy)] @@ -115,6 +115,9 @@ impl Value { pub fn const_type() -> Self { Value::from_const(Const::Type) } + pub fn from_builtin(b: Builtin) -> Self { + builtin_to_value(b) + } pub(crate) fn as_const(&self) -> Option { match &*self.as_whnf() { diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs index 0c3058d..da03cbd 100644 --- a/dhall/src/core/valuef.rs +++ b/dhall/src/core/valuef.rs @@ -257,16 +257,6 @@ impl ValueF { } } - /// Apply to a valuef - pub(crate) fn app(self, val: ValueF) -> ValueF { - self.app_valuef(val) - } - - /// Apply to a valuef - pub(crate) fn app_valuef(self, val: ValueF) -> ValueF { - self.app_value(val.into_value_untyped()) - } - /// Apply to a value pub fn app_value(self, th: Value) -> ValueF { Value::from_valuef_untyped(self).app_value(th) -- cgit v1.2.3 From a506632b27b287d1bf898e2f77ae09a56902474c Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 20 Aug 2019 17:08:01 +0200 Subject: Naming tweaks --- dhall/src/core/value.rs | 6 +++--- dhall/src/core/valuef.rs | 11 +++++------ 2 files changed, 8 insertions(+), 9 deletions(-) (limited to 'dhall/src/core') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index f897f16..5055ac2 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -8,7 +8,7 @@ use crate::core::context::TypecheckContext; use crate::core::valuef::ValueF; use crate::core::var::{AlphaVar, Shift, Subst}; use crate::error::{TypeError, TypeMessage}; -use crate::phase::normalize::{apply_any, normalize_whnf, OutputSubExpr}; +use crate::phase::normalize::{apply_any, normalize_whnf}; use crate::phase::typecheck::{builtin_to_value, const_to_value}; use crate::phase::{NormalizedSubExpr, Typed}; @@ -208,11 +208,11 @@ impl Value { pub(crate) fn normalize_to_expr_maybe_alpha( &self, alpha: bool, - ) -> OutputSubExpr { + ) -> NormalizedSubExpr { self.as_nf().normalize_to_expr_maybe_alpha(alpha) } - pub(crate) fn app_value(&self, th: Value) -> ValueF { + pub(crate) fn app(&self, th: Value) -> ValueF { apply_any(self.clone(), th) } diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs index da03cbd..e9049c7 100644 --- a/dhall/src/core/valuef.rs +++ b/dhall/src/core/valuef.rs @@ -7,8 +7,7 @@ use dhall_syntax::{ use crate::core::value::Value; use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; -use crate::phase::normalize::OutputSubExpr; -use crate::phase::Normalized; +use crate::phase::{Normalized, NormalizedSubExpr}; /// A semantic value. Subexpressions are Values, which are partially evaluated expressions that are /// normalized on-demand. @@ -59,7 +58,7 @@ impl ValueF { } /// Convert the value to a fully normalized syntactic expression - pub(crate) fn normalize_to_expr(&self) -> OutputSubExpr { + pub(crate) fn normalize_to_expr(&self) -> NormalizedSubExpr { self.normalize_to_expr_maybe_alpha(false) } /// Convert the value to a fully normalized syntactic expression. Also alpha-normalize @@ -67,7 +66,7 @@ impl ValueF { pub(crate) fn normalize_to_expr_maybe_alpha( &self, alpha: bool, - ) -> OutputSubExpr { + ) -> NormalizedSubExpr { match self { ValueF::Lam(x, t, e) => rc(ExprF::Lam( x.to_label_maybe_alpha(alpha), @@ -258,8 +257,8 @@ impl ValueF { } /// Apply to a value - pub fn app_value(self, th: Value) -> ValueF { - Value::from_valuef_untyped(self).app_value(th) + pub fn app(self, th: Value) -> ValueF { + Value::from_valuef_untyped(self).app(th) } pub fn from_builtin(b: Builtin) -> ValueF { -- cgit v1.2.3 From 4f1f37cfc115510500e83d2dfbfa8ed7ddeae74a Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 20 Aug 2019 18:03:59 +0200 Subject: Introduce a new enum to store either a Value or a ValueF --- dhall/src/core/value.rs | 54 +++++++++++++++++++++++++++++++++++++++++++++--- dhall/src/core/valuef.rs | 9 +++++--- 2 files changed, 57 insertions(+), 6 deletions(-) (limited to 'dhall/src/core') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 5055ac2..25fcaae 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -44,6 +44,14 @@ struct ValueInternal { #[derive(Clone)] pub struct Value(Rc>); +/// When a function needs to return either a freshly created ValueF or an existing Value, but +/// doesn't want to convert both to the same thing, either to avoid unnecessary allocations or to +/// avoid loss of typ information. +pub enum VoVF { + Value(Value), + ValueF(ValueF), +} + impl ValueInternal { fn into_value(self) -> Value { Value(Rc::new(RefCell::new(self))) @@ -56,7 +64,8 @@ impl ValueInternal { take_mut::take(self, |vint| match &vint.form { Unevaled => ValueInternal { form: WHNF, - value: normalize_whnf(vint.value), + // TODO: thunk chaining + value: normalize_whnf(vint.value).into_whnf(), ty: vint.ty, }, // Already in WHNF @@ -166,6 +175,9 @@ impl Value { pub(crate) fn into_typed(self) -> Typed { Typed::from_value(self) } + pub(crate) fn into_vovf(self) -> VoVF { + VoVF::Value(self) + } /// Mutates the contents. If no one else shares this, this avoids a RefCell lock. fn mutate_internal(&mut self, f: impl FnOnce(&mut ValueInternal)) { @@ -212,8 +224,8 @@ impl Value { self.as_nf().normalize_to_expr_maybe_alpha(alpha) } - pub(crate) fn app(&self, th: Value) -> ValueF { - apply_any(self.clone(), th) + pub(crate) fn app(&self, v: Value) -> VoVF { + apply_any(self.clone(), v) } pub(crate) fn get_type(&self) -> Result, TypeError> { @@ -221,6 +233,42 @@ impl Value { } } +impl VoVF { + pub fn into_whnf(self) -> ValueF { + match self { + VoVF::Value(v) => v.to_whnf(), + VoVF::ValueF(v) => v, + } + } + pub(crate) fn into_value_untyped(self) -> Value { + match self { + VoVF::Value(v) => v, + VoVF::ValueF(v) => v.into_value_untyped(), + } + } + pub(crate) fn into_value_with_type(self, t: Value) -> Value { + match self { + // TODO: check type with debug_assert ? + VoVF::Value(v) => v, + VoVF::ValueF(v) => v.into_value_with_type(t), + } + } + pub(crate) fn into_value_simple_type(self) -> Value { + match self { + // TODO: check type with debug_assert ? + VoVF::Value(v) => v, + VoVF::ValueF(v) => v.into_value_simple_type(), + } + } + + pub(crate) fn app(self, x: Value) -> Self { + match self { + VoVF::Value(v) => v.app(x), + VoVF::ValueF(v) => v.into_value_untyped().app(x), + } + } +} + impl Shift for Value { fn shift(&self, delta: isize, var: &AlphaVar) -> Option { Some(Value(self.0.shift(delta, var)?)) diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs index e9049c7..80978a7 100644 --- a/dhall/src/core/valuef.rs +++ b/dhall/src/core/valuef.rs @@ -5,7 +5,7 @@ use dhall_syntax::{ NaiveDouble, Natural, }; -use crate::core::value::Value; +use crate::core::value::{Value, VoVF}; use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; use crate::phase::{Normalized, NormalizedSubExpr}; @@ -56,6 +56,9 @@ impl ValueF { pub(crate) fn into_value_simple_type(self) -> Value { Value::from_valuef_simple_type(self) } + pub(crate) fn into_vovf(self) -> VoVF { + VoVF::ValueF(self) + } /// Convert the value to a fully normalized syntactic expression pub(crate) fn normalize_to_expr(&self) -> NormalizedSubExpr { @@ -257,8 +260,8 @@ impl ValueF { } /// Apply to a value - pub fn app(self, th: Value) -> ValueF { - Value::from_valuef_untyped(self).app(th) + pub fn app(self, v: Value) -> VoVF { + self.into_vovf().app(v) } pub fn from_builtin(b: Builtin) -> ValueF { -- cgit v1.2.3 From c157df5e66fb80ff6184cb3934e5b0883f0fdbf0 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 20 Aug 2019 18:11:05 +0200 Subject: No need for Cow in return type of get_type --- dhall/src/core/value.rs | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'dhall/src/core') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 25fcaae..64a4842 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -1,4 +1,3 @@ -use std::borrow::Cow; use std::cell::{Ref, RefCell, RefMut}; use std::rc::Rc; @@ -228,8 +227,8 @@ impl Value { apply_any(self.clone(), v) } - pub(crate) fn get_type(&self) -> Result, TypeError> { - Ok(Cow::Owned(self.as_internal().get_type()?.clone())) + pub(crate) fn get_type(&self) -> Result { + Ok(self.as_internal().get_type()?.clone()) } } -- cgit v1.2.3 From f70e45daef2570259eccd227a0126493c015d7b0 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 20 Aug 2019 21:50:47 +0200 Subject: Track evaluation status alongside ValueF in VoVF --- dhall/src/core/value.rs | 44 ++++++++++++++++++-------------------------- dhall/src/core/valuef.rs | 32 ++++++++++++++++++++++---------- 2 files changed, 40 insertions(+), 36 deletions(-) (limited to 'dhall/src/core') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 64a4842..b44dad6 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -12,7 +12,7 @@ use crate::phase::typecheck::{builtin_to_value, const_to_value}; use crate::phase::{NormalizedSubExpr, Typed}; #[derive(Debug, Clone, Copy)] -enum Form { +pub enum Form { /// No constraints; expression may not be normalized at all. Unevaled, /// Weak Head Normal Form, i.e. normalized up to the first constructor, but subexpressions may @@ -46,9 +46,10 @@ pub struct Value(Rc>); /// When a function needs to return either a freshly created ValueF or an existing Value, but /// doesn't want to convert both to the same thing, either to avoid unnecessary allocations or to /// avoid loss of typ information. +#[derive(Debug, Clone)] pub enum VoVF { Value(Value), - ValueF(ValueF), + ValueF { val: ValueF, form: Form }, } impl ValueInternal { @@ -98,24 +99,14 @@ impl ValueInternal { } impl Value { + pub(crate) fn new(value: ValueF, form: Form, ty: Option) -> Value { + ValueInternal { form, value, ty }.into_value() + } pub(crate) fn from_valuef_untyped(v: ValueF) -> Value { - ValueInternal { - form: Unevaled, - value: v, - ty: None, - } - .into_value() + Value::new(v, Unevaled, None) } pub(crate) fn from_valuef_and_type(v: ValueF, t: Value) -> Value { - ValueInternal { - form: Unevaled, - value: v, - ty: Some(t), - } - .into_value() - } - pub(crate) fn from_valuef_simple_type(v: ValueF) -> Value { - Value::from_valuef_and_type(v, Value::from_const(Const::Type)) + Value::new(v, Unevaled, Some(t)) } pub(crate) fn from_const(c: Const) -> Self { const_to_value(c) @@ -236,34 +227,35 @@ impl VoVF { pub fn into_whnf(self) -> ValueF { match self { VoVF::Value(v) => v.to_whnf(), - VoVF::ValueF(v) => v, + VoVF::ValueF { + val, + form: Unevaled, + } => normalize_whnf(val).into_whnf(), + // Already at lest in WHNF + VoVF::ValueF { val, .. } => val, } } pub(crate) fn into_value_untyped(self) -> Value { match self { VoVF::Value(v) => v, - VoVF::ValueF(v) => v.into_value_untyped(), + VoVF::ValueF { val, form } => Value::new(val, form, None), } } pub(crate) fn into_value_with_type(self, t: Value) -> Value { match self { // TODO: check type with debug_assert ? VoVF::Value(v) => v, - VoVF::ValueF(v) => v.into_value_with_type(t), + VoVF::ValueF { val, form } => Value::new(val, form, Some(t)), } } pub(crate) fn into_value_simple_type(self) -> Value { - match self { - // TODO: check type with debug_assert ? - VoVF::Value(v) => v, - VoVF::ValueF(v) => v.into_value_simple_type(), - } + self.into_value_with_type(Value::from_const(Const::Type)) } pub(crate) fn app(self, x: Value) -> Self { match self { VoVF::Value(v) => v.app(x), - VoVF::ValueF(v) => v.into_value_untyped().app(x), + VoVF::ValueF { val, .. } => val.into_value_untyped().app(x), } } } diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs index 80978a7..db8a284 100644 --- a/dhall/src/core/valuef.rs +++ b/dhall/src/core/valuef.rs @@ -5,7 +5,7 @@ use dhall_syntax::{ NaiveDouble, Natural, }; -use crate::core::value::{Value, VoVF}; +use crate::core::value::{Form, Value, VoVF}; use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; use crate::phase::{Normalized, NormalizedSubExpr}; @@ -19,7 +19,7 @@ pub enum ValueF { /// Closures Lam(AlphaLabel, Value, Value), Pi(AlphaLabel, Value, Value), - // Invariant: the evaluation must not be able to progress further. + // Invariant: in whnf, the evaluation must not be able to progress further. AppliedBuiltin(Builtin, Vec), Var(AlphaVar), @@ -33,16 +33,16 @@ pub enum ValueF { // EmptyListLit(t) means `[] : List t`, not `[] : t` EmptyListLit(Value), NEListLit(Vec), - RecordLit(HashMap), RecordType(HashMap), + RecordLit(HashMap), UnionType(HashMap>), UnionConstructor(Label, HashMap>), UnionLit(Label, Value, HashMap>), - // Invariant: this must not contain interpolations that are themselves TextLits, and + // Invariant: in whnf, this must not contain interpolations that are themselves TextLits, and // contiguous text values must be merged. TextLit(Vec>), Equivalence(Value, Value), - // Invariant: this must not contain a value captured by one of the variants above. + // Invariant: in whnf, this must not contain a value captured by one of the variants above. PartialExpr(ExprF), } @@ -53,11 +53,23 @@ impl ValueF { pub(crate) fn into_value_with_type(self, t: Value) -> Value { Value::from_valuef_and_type(self, t) } - pub(crate) fn into_value_simple_type(self) -> Value { - Value::from_valuef_simple_type(self) + pub(crate) fn into_vovf_unevaled(self) -> VoVF { + VoVF::ValueF { + val: self, + form: Form::Unevaled, + } + } + pub(crate) fn into_vovf_whnf(self) -> VoVF { + VoVF::ValueF { + val: self, + form: Form::WHNF, + } } - pub(crate) fn into_vovf(self) -> VoVF { - VoVF::ValueF(self) + pub(crate) fn into_vovf_nf(self) -> VoVF { + VoVF::ValueF { + val: self, + form: Form::NF, + } } /// Convert the value to a fully normalized syntactic expression @@ -261,7 +273,7 @@ impl ValueF { /// Apply to a value pub fn app(self, v: Value) -> VoVF { - self.into_vovf().app(v) + self.into_vovf_unevaled().app(v) } pub fn from_builtin(b: Builtin) -> ValueF { -- cgit v1.2.3 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 From 8e68396e9fe3751bcf8bcfd68301ca7fea836787 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 20 Aug 2019 22:35:53 +0200 Subject: Use Ret in apply_builtin --- dhall/src/core/valuef.rs | 6 ------ 1 file changed, 6 deletions(-) (limited to 'dhall/src/core') diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs index db8a284..316238c 100644 --- a/dhall/src/core/valuef.rs +++ b/dhall/src/core/valuef.rs @@ -65,12 +65,6 @@ impl ValueF { form: Form::WHNF, } } - pub(crate) fn into_vovf_nf(self) -> VoVF { - VoVF::ValueF { - val: self, - form: Form::NF, - } - } /// Convert the value to a fully normalized syntactic expression pub(crate) fn normalize_to_expr(&self) -> NormalizedSubExpr { -- cgit v1.2.3 From 6c006e122a050ebbe76c8c566e559bbf9f2301a7 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 20 Aug 2019 23:06:14 +0200 Subject: Reduce API surface of dhall crate --- dhall/src/core/value.rs | 13 +++++-------- dhall/src/core/valuef.rs | 15 ++------------- 2 files changed, 7 insertions(+), 21 deletions(-) (limited to 'dhall/src/core') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 24e2803..e1623a8 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -12,7 +12,7 @@ use crate::phase::typecheck::{builtin_to_value, const_to_value}; use crate::phase::{NormalizedSubExpr, Typed}; #[derive(Debug, Clone, Copy)] -pub enum Form { +pub(crate) enum Form { /// No constraints; expression may not be normalized at all. Unevaled, /// Weak Head Normal Form, i.e. normalized up to the first constructor, but subexpressions may @@ -41,13 +41,13 @@ struct ValueInternal { /// sharing computation automatically. Uses a RefCell to share computation. /// Can optionally store a type from typechecking to preserve type information. #[derive(Clone)] -pub struct Value(Rc>); +pub(crate) struct Value(Rc>); /// When a function needs to return either a freshly created ValueF or an existing Value, but /// doesn't want to convert both to the same thing, either to avoid unnecessary allocations or to /// avoid loss of typ information. #[derive(Debug, Clone)] -pub enum VoVF { +pub(crate) enum VoVF { Value(Value), ValueF { val: ValueF, form: Form }, } @@ -111,10 +111,7 @@ impl Value { pub(crate) fn from_const(c: Const) -> Self { const_to_value(c) } - pub fn const_type() -> Self { - Value::from_const(Const::Type) - } - pub fn from_builtin(b: Builtin) -> Self { + pub(crate) fn from_builtin(b: Builtin) -> Self { builtin_to_value(b) } @@ -234,7 +231,7 @@ impl Value { } impl VoVF { - pub fn into_whnf(self) -> ValueF { + pub(crate) fn into_whnf(self) -> ValueF { match self { VoVF::Value(v) => v.to_whnf(), VoVF::ValueF { diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs index 316238c..42606a9 100644 --- a/dhall/src/core/valuef.rs +++ b/dhall/src/core/valuef.rs @@ -15,7 +15,7 @@ use crate::phase::{Normalized, NormalizedSubExpr}; /// alpha-equivalence (renaming of bound variables) and beta-equivalence (normalization). It will /// recursively normalize as needed. #[derive(Debug, Clone, PartialEq, Eq)] -pub enum ValueF { +pub(crate) enum ValueF { /// Closures Lam(AlphaLabel, Value, Value), Pi(AlphaLabel, Value, Value), @@ -53,12 +53,6 @@ impl ValueF { pub(crate) fn into_value_with_type(self, t: Value) -> Value { Value::from_valuef_and_type(self, t) } - pub(crate) fn into_vovf_unevaled(self) -> VoVF { - VoVF::ValueF { - val: self, - form: Form::Unevaled, - } - } pub(crate) fn into_vovf_whnf(self) -> VoVF { VoVF::ValueF { val: self, @@ -265,12 +259,7 @@ impl ValueF { } } - /// Apply to a value - pub fn app(self, v: Value) -> VoVF { - self.into_vovf_unevaled().app(v) - } - - pub fn from_builtin(b: Builtin) -> ValueF { + pub(crate) fn from_builtin(b: Builtin) -> ValueF { ValueF::AppliedBuiltin(b, vec![]) } } -- cgit v1.2.3 From e8a9178ebe4860a8a00a6ec8f77b661fdad84890 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 21 Aug 2019 17:40:56 +0200 Subject: Don't use take_mut::take lightly since normalize_whnf might panic --- dhall/src/core/value.rs | 27 ++++++++++++++++++--------- 1 file changed, 18 insertions(+), 9 deletions(-) (limited to 'dhall/src/core') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index e1623a8..69d372a 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -61,16 +61,25 @@ impl ValueInternal { } fn normalize_whnf(&mut self) { - take_mut::take(self, |vint| match &vint.form { - Unevaled => ValueInternal { - form: WHNF, - // TODO: thunk chaining - value: normalize_whnf(vint.value).into_whnf(), - ty: vint.ty, + take_mut::take_or_recover( + self, + // Dummy value in case the other closure panics + || ValueInternal { + form: Unevaled, + value: ValueF::Const(Const::Type), + ty: None, }, - // Already in WHNF - WHNF | NF => vint, - }) + |vint| match &vint.form { + Unevaled => ValueInternal { + form: WHNF, + // TODO: thunk chaining + value: normalize_whnf(vint.value).into_whnf(), + ty: vint.ty, + }, + // Already in WHNF + WHNF | NF => vint, + }, + ) } fn normalize_nf(&mut self) { match self.form { -- cgit v1.2.3 From 98399997cf289d802fbed674558665547cf73d59 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 25 Aug 2019 16:09:55 +0200 Subject: Keep type information through normalization --- dhall/src/core/value.rs | 39 ++++++++++++++++++++++++++++----------- 1 file changed, 28 insertions(+), 11 deletions(-) (limited to 'dhall/src/core') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 69d372a..6f9f78a 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -70,12 +70,25 @@ impl ValueInternal { ty: None, }, |vint| match &vint.form { - Unevaled => ValueInternal { - form: WHNF, - // TODO: thunk chaining - value: normalize_whnf(vint.value).into_whnf(), - ty: vint.ty, - }, + 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); + // } + ValueInternal { + form: WHNF, + value: new_val, + ty: ty, + } + } // Already in WHNF WHNF | NF => vint, }, @@ -221,7 +234,8 @@ impl Value { } pub(crate) fn app(&self, v: Value) -> Value { - let vovf = apply_any(self.clone(), v.clone()); + let ty = self.get_type().ok(); + let vovf = apply_any(self.clone(), v.clone(), ty.as_ref()); match self.as_internal().get_type() { Err(_) => vovf.into_value_untyped(), Ok(t) => match &*t.as_whnf() { @@ -240,15 +254,18 @@ impl Value { } impl VoVF { - pub(crate) fn into_whnf(self) -> ValueF { + pub(crate) fn into_whnf_and_type( + self, + ty: Option<&Value>, + ) -> (ValueF, Option) { match self { - VoVF::Value(v) => v.to_whnf(), VoVF::ValueF { val, form: Unevaled, - } => normalize_whnf(val).into_whnf(), + } => normalize_whnf(val, ty).into_whnf_and_type(ty), // Already at lest in WHNF - VoVF::ValueF { val, .. } => val, + VoVF::ValueF { val, .. } => (val, None), + VoVF::Value(v) => (v.to_whnf(), v.get_type().ok()), } } pub(crate) fn into_value_untyped(self) -> Value { -- cgit v1.2.3 From 80fb5355ea90377492b9863f632c01a808f8aade Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 25 Aug 2019 16:33:12 +0200 Subject: Check consistency of type information --- dhall/src/core/value.rs | 53 ++++++++++++++++++++++++++----------------------- 1 file changed, 28 insertions(+), 25 deletions(-) (limited to 'dhall/src/core') 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) { + 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)), } } -- cgit v1.2.3 From f9ec2cdf2803ed92fa404db989b786fc1dfac12e Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 25 Aug 2019 17:07:59 +0200 Subject: Enforce type information almost everywhere --- dhall/src/core/value.rs | 66 ++++++++++++++++++++++++++---------------------- dhall/src/core/valuef.rs | 3 --- 2 files changed, 36 insertions(+), 33 deletions(-) (limited to 'dhall/src/core') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 7f98826..4a78b05 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -27,13 +27,14 @@ pub(crate) enum Form { } use Form::{Unevaled, NF, WHNF}; -#[derive(Debug)] /// Partially normalized value. /// Invariant: if `form` is `WHNF`, `value` must be in Weak Head Normal Form /// Invariant: if `form` is `NF`, `value` must be fully normalized +#[derive(Debug)] struct ValueInternal { form: Form, value: ValueF, + /// This is None if and only if `value` is `Sort` (which doesn't have a type) ty: Option, } @@ -69,11 +70,15 @@ impl ValueInternal { value: ValueF::Const(Const::Type), ty: None, }, - |vint| match &vint.form { - Unevaled => { + |vint| match (&vint.form, &vint.ty) { + (Unevaled, None) => ValueInternal { + form: NF, + value: ValueF::Const(Const::Sort), + ty: None, + }, + (Unevaled, Some(ty)) => { let new_value = - normalize_whnf(vint.value, vint.ty.as_ref()) - .into_whnf(vint.ty.as_ref()); + normalize_whnf(vint.value, &ty).into_whnf(&ty); ValueInternal { form: WHNF, value: new_value, @@ -81,7 +86,7 @@ impl ValueInternal { } } // Already in WHNF - WHNF | NF => vint, + (WHNF, _) | (NF, _) => vint, }, ) } @@ -103,10 +108,9 @@ impl ValueInternal { fn get_type(&self) -> Result<&Value, TypeError> { match &self.ty { Some(t) => Ok(t), - None => Err(TypeError::new( - &TypecheckContext::new(), - TypeMessage::Untyped, - )), + None => { + Err(TypeError::new(&TypecheckContext::new(), TypeMessage::Sort)) + } } } } @@ -115,9 +119,13 @@ impl Value { pub(crate) fn new(value: ValueF, form: Form, ty: Option) -> Value { ValueInternal { form, value, ty }.into_value() } + // TODO: this is very wrong pub(crate) fn from_valuef_untyped(v: ValueF) -> Value { Value::new(v, Unevaled, None) } + pub(crate) fn const_sort() -> Value { + Value::new(ValueF::Const(Const::Sort), NF, None) + } pub(crate) fn from_valuef_and_type(v: ValueF, t: Value) -> Value { Value::new(v, Unevaled, Some(t)) } @@ -225,27 +233,30 @@ impl Value { } pub(crate) fn app(&self, v: Value) -> Value { - let ty = self.get_type().ok(); - let vovf = apply_any(self.clone(), v.clone(), ty.as_ref()); - 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"), - }, + let t = self.get_type_not_sort(); + let vovf = apply_any(self.clone(), v.clone(), &t); + let t_borrow = t.as_whnf(); + match &*t_borrow { + 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 { Ok(self.as_internal().get_type()?.clone()) } + /// When we know the value isn't `Sort`, this gets the type directly + pub(crate) fn get_type_not_sort(&self) -> Value { + self.get_type() + .expect("Internal type error: value is `Sort` but shouldn't be") + } } impl VoVF { - pub(crate) fn into_whnf(self, ty: Option<&Value>) -> ValueF { + pub(crate) fn into_whnf(self, ty: &Value) -> ValueF { match self { VoVF::ValueF { val, @@ -256,7 +267,7 @@ impl VoVF { VoVF::Value(v) => { let v_ty = v.get_type().ok(); debug_assert_eq!( - ty, + Some(ty), v_ty.as_ref(), "The type recovered from normalization doesn't match the stored type." ); @@ -264,12 +275,6 @@ impl VoVF { } } } - pub(crate) fn into_value_untyped(self) -> Value { - match self { - VoVF::Value(v) => v, - VoVF::ValueF { val, form } => Value::new(val, form, None), - } - } pub(crate) fn into_value_with_type(self, ty: Value) -> Value { match self { VoVF::Value(v) => { @@ -288,7 +293,8 @@ impl VoVF { 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), + // TODO: this is very wrong + VoVF::ValueF { val, .. } => Value::from_valuef_untyped(val).app(x), }) } } diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs index 42606a9..5638078 100644 --- a/dhall/src/core/valuef.rs +++ b/dhall/src/core/valuef.rs @@ -47,9 +47,6 @@ pub(crate) enum ValueF { } impl ValueF { - pub(crate) fn into_value_untyped(self) -> Value { - Value::from_valuef_untyped(self) - } pub(crate) fn into_value_with_type(self, t: Value) -> Value { Value::from_valuef_and_type(self, t) } -- cgit v1.2.3 From bf37fd9da3782134ca4bca9567c34bbee81784b9 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 25 Aug 2019 21:16:38 +0200 Subject: Rework apply_builtin to enforce preservation of type information --- dhall/src/core/value.rs | 32 +++++++++++++++----------------- 1 file changed, 15 insertions(+), 17 deletions(-) (limited to 'dhall/src/core') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 4a78b05..2554da1 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -116,18 +116,24 @@ impl ValueInternal { } impl Value { - pub(crate) fn new(value: ValueF, form: Form, ty: Option) -> Value { - ValueInternal { form, value, ty }.into_value() - } - // TODO: this is very wrong - pub(crate) fn from_valuef_untyped(v: ValueF) -> Value { - Value::new(v, Unevaled, None) + fn new(value: ValueF, form: Form, ty: Value) -> Value { + ValueInternal { + form, + value, + ty: Some(ty), + } + .into_value() } pub(crate) fn const_sort() -> Value { - Value::new(ValueF::Const(Const::Sort), NF, None) + ValueInternal { + form: NF, + value: ValueF::Const(Const::Sort), + ty: None, + } + .into_value() } pub(crate) fn from_valuef_and_type(v: ValueF, t: Value) -> Value { - Value::new(v, Unevaled, Some(t)) + Value::new(v, Unevaled, t) } pub(crate) fn from_const(c: Const) -> Self { const_to_value(c) @@ -286,17 +292,9 @@ impl VoVF { ); v } - VoVF::ValueF { val, form } => Value::new(val, form, Some(ty)), + VoVF::ValueF { val, form } => Value::new(val, form, ty), } } - - pub(crate) fn app(self, x: Value) -> VoVF { - VoVF::Value(match self { - VoVF::Value(v) => v.app(x), - // TODO: this is very wrong - VoVF::ValueF { val, .. } => Value::from_valuef_untyped(val).app(x), - }) - } } impl Shift for Value { -- cgit v1.2.3 From 906cbf5fc4c3bee65f24df1604497e33c6a20833 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 25 Aug 2019 21:52:59 +0200 Subject: Remove now unnecessary VoVF enum --- dhall/src/core/value.rs | 95 ++++++++++++++---------------------------------- dhall/src/core/valuef.rs | 10 +---- 2 files changed, 29 insertions(+), 76 deletions(-) (limited to 'dhall/src/core') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 2554da1..13f8e59 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -44,15 +44,6 @@ struct ValueInternal { #[derive(Clone)] pub(crate) struct Value(Rc>); -/// When a function needs to return either a freshly created ValueF or an existing Value, but -/// doesn't want to convert both to the same thing, either to avoid unnecessary allocations or to -/// avoid loss of typ information. -#[derive(Debug, Clone)] -pub(crate) enum VoVF { - Value(Value), - ValueF { val: ValueF, form: Form }, -} - impl ValueInternal { fn into_value(self) -> Value { Value(Rc::new(RefCell::new(self))) @@ -76,15 +67,11 @@ impl ValueInternal { value: ValueF::Const(Const::Sort), ty: None, }, - (Unevaled, Some(ty)) => { - let new_value = - normalize_whnf(vint.value, &ty).into_whnf(&ty); - ValueInternal { - form: WHNF, - value: new_value, - ty: vint.ty, - } - } + (Unevaled, Some(ty)) => ValueInternal { + form: WHNF, + value: normalize_whnf(vint.value, &ty), + ty: vint.ty, + }, // Already in WHNF (WHNF, _) | (NF, _) => vint, }, @@ -135,6 +122,9 @@ impl Value { pub(crate) fn from_valuef_and_type(v: ValueF, t: Value) -> Value { Value::new(v, Unevaled, t) } + pub(crate) fn from_valuef_and_type_whnf(v: ValueF, t: Value) -> Value { + Value::new(v, WHNF, t) + } pub(crate) fn from_const(c: Const) -> Self { const_to_value(c) } @@ -182,16 +172,22 @@ impl Value { pub(crate) fn to_expr_alpha(&self) -> NormalizedSubExpr { self.as_whnf().normalize_to_expr_maybe_alpha(true) } - /// TODO: cloning a valuef can often be avoided - pub(crate) fn to_whnf(&self) -> ValueF { + pub(crate) fn to_whnf_ignore_type(&self) -> ValueF { self.as_whnf().clone() } + /// Before discarding type information, check that it matches the expected return type. + pub(crate) fn to_whnf_check_type(&self, ty: &Value) -> ValueF { + let self_ty = self.get_type().ok(); + debug_assert_eq!( + Some(ty), + self_ty.as_ref(), + "The value returned from normalization doesn't have the expected type." + ); + self.to_whnf_ignore_type() + } pub(crate) fn into_typed(self) -> Typed { Typed::from_value(self) } - pub(crate) fn into_vovf(self) -> VoVF { - VoVF::Value(self) - } /// Mutates the contents. If no one else shares this, this avoids a RefCell lock. fn mutate_internal(&mut self, f: impl FnOnce(&mut ValueInternal)) { @@ -239,16 +235,14 @@ impl Value { } pub(crate) fn app(&self, v: Value) -> Value { - let t = self.get_type_not_sort(); - let vovf = apply_any(self.clone(), v.clone(), &t); - let t_borrow = t.as_whnf(); - match &*t_borrow { - ValueF::Pi(x, _, e) => { - let t = e.subst_shift(&x.into(), &v); - vovf.into_value_with_type(t) - } + let body_t = match &*self.get_type_not_sort().as_whnf() { + ValueF::Pi(x, _, e) => e.subst_shift(&x.into(), &v), _ => unreachable!("Internal type error"), - } + }; + Value::from_valuef_and_type_whnf( + apply_any(self.clone(), v, &body_t), + body_t, + ) } pub(crate) fn get_type(&self) -> Result { @@ -261,42 +255,6 @@ impl Value { } } -impl VoVF { - pub(crate) fn into_whnf(self, ty: &Value) -> ValueF { - match self { - VoVF::ValueF { - val, - form: Unevaled, - } => normalize_whnf(val, ty).into_whnf(ty), - // Already at lest in WHNF - VoVF::ValueF { val, .. } => val, - 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.to_whnf() - } - } - } - pub(crate) fn into_value_with_type(self, ty: Value) -> Value { - match self { - 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, ty), - } - } -} - impl Shift for Value { fn shift(&self, delta: isize, var: &AlphaVar) -> Option { Some(Value(self.0.shift(delta, var)?)) @@ -324,6 +282,7 @@ impl Subst for ValueInternal { ValueInternal { // The resulting value may not stay in wnhf after substitution form: Unevaled, + // TODO: check type info if self.value if Var(v) and v == var value: self.value.subst_shift(var, val), ty: self.ty.subst_shift(var, val), } diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs index 5638078..9ea2467 100644 --- a/dhall/src/core/valuef.rs +++ b/dhall/src/core/valuef.rs @@ -5,7 +5,7 @@ use dhall_syntax::{ NaiveDouble, Natural, }; -use crate::core::value::{Form, Value, VoVF}; +use crate::core::value::Value; use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; use crate::phase::{Normalized, NormalizedSubExpr}; @@ -50,12 +50,6 @@ impl ValueF { pub(crate) fn into_value_with_type(self, t: Value) -> Value { Value::from_valuef_and_type(self, t) } - pub(crate) fn into_vovf_whnf(self) -> VoVF { - VoVF::ValueF { - val: self, - form: Form::WHNF, - } - } /// Convert the value to a fully normalized syntactic expression pub(crate) fn normalize_to_expr(&self) -> NormalizedSubExpr { @@ -339,7 +333,7 @@ impl Subst for ValueF { t.subst_shift(var, val), e.subst_shift(&var.under_binder(x), &val.under_binder(x)), ), - ValueF::Var(v) if v == var => val.to_whnf(), + ValueF::Var(v) if v == var => val.to_whnf_ignore_type(), ValueF::Var(v) => ValueF::Var(v.shift(-1, var).unwrap()), ValueF::Const(c) => ValueF::Const(*c), ValueF::BoolLit(b) => ValueF::BoolLit(*b), -- cgit v1.2.3 From 829fff5bd3e2115c0a16d40a4dc266747d622b08 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 26 Aug 2019 18:54:29 +0200 Subject: Check correctness of type info in a few more places --- dhall/src/core/value.rs | 60 +++++++++++++++++++++++++++++++++++-------------- 1 file changed, 43 insertions(+), 17 deletions(-) (limited to 'dhall/src/core') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index 13f8e59..21ac288 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -62,16 +62,17 @@ impl ValueInternal { ty: None, }, |vint| match (&vint.form, &vint.ty) { - (Unevaled, None) => ValueInternal { - form: NF, - value: ValueF::Const(Const::Sort), - ty: None, - }, (Unevaled, Some(ty)) => ValueInternal { form: WHNF, value: normalize_whnf(vint.value, &ty), ty: vint.ty, }, + // `value` is `Sort` + (Unevaled, None) => ValueInternal { + form: NF, + value: ValueF::Const(Const::Sort), + ty: None, + }, // Already in WHNF (WHNF, _) | (NF, _) => vint, }, @@ -177,12 +178,7 @@ impl Value { } /// Before discarding type information, check that it matches the expected return type. pub(crate) fn to_whnf_check_type(&self, ty: &Value) -> ValueF { - let self_ty = self.get_type().ok(); - debug_assert_eq!( - Some(ty), - self_ty.as_ref(), - "The value returned from normalization doesn't have the expected type." - ); + self.check_type(ty); self.to_whnf_ignore_type() } pub(crate) fn into_typed(self) -> Typed { @@ -236,7 +232,10 @@ impl Value { pub(crate) fn app(&self, v: Value) -> Value { let body_t = match &*self.get_type_not_sort().as_whnf() { - ValueF::Pi(x, _, e) => e.subst_shift(&x.into(), &v), + ValueF::Pi(x, t, e) => { + v.check_type(t); + e.subst_shift(&x.into(), &v) + } _ => unreachable!("Internal type error"), }; Value::from_valuef_and_type_whnf( @@ -245,6 +244,15 @@ impl Value { ) } + /// In debug mode, panic if the provided type doesn't match the value's type. + /// Otherwise does nothing. + pub(crate) fn check_type(&self, ty: &Value) { + debug_assert_eq!( + Some(ty), + self.get_type().ok().as_ref(), + "Internal type error" + ); + } pub(crate) fn get_type(&self) -> Result { Ok(self.as_internal().get_type()?.clone()) } @@ -273,7 +281,17 @@ impl Shift for ValueInternal { impl Subst for Value { fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { - Value(self.0.subst_shift(var, val)) + match &*self.as_valuef() { + // If the var matches, we can just reuse the provided value instead of copying it. + // We also check that the types match, if in debug mode. + ValueF::Var(v) if v == var => { + if let Ok(self_ty) = self.get_type() { + val.check_type(&self_ty.subst_shift(var, val)); + } + val.clone() + } + _ => Value(self.0.subst_shift(var, val)), + } } } @@ -282,7 +300,6 @@ impl Subst for ValueInternal { ValueInternal { // The resulting value may not stay in wnhf after substitution form: Unevaled, - // TODO: check type info if self.value if Var(v) and v == var value: self.value.subst_shift(var, val), ty: self.ty.subst_shift(var, val), } @@ -300,8 +317,17 @@ impl std::cmp::Eq for Value {} impl std::fmt::Debug for Value { fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { let vint: &ValueInternal = &self.as_internal(); - fmt.debug_tuple(&format!("Value@{:?}", &vint.form)) - .field(&vint.value) - .finish() + if let ValueF::Const(c) = &vint.value { + write!(fmt, "{:?}", c) + } else { + let mut x = fmt.debug_struct(&format!("Value@{:?}", &vint.form)); + x.field("value", &vint.value); + if let Some(ty) = vint.ty.as_ref() { + x.field("type", &ty); + } else { + x.field("type", &None::<()>); + } + x.finish() + } } } -- cgit v1.2.3