From 6753a1f97bb674d91dd4d42f2ddb25a8119e070d Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 17 Aug 2019 19:00:43 +0200 Subject: s/Thunk/Value/ --- dhall/src/core/valuef.rs | 405 +++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 405 insertions(+) create mode 100644 dhall/src/core/valuef.rs (limited to 'dhall/src/core/valuef.rs') diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs new file mode 100644 index 0000000..bea2e2e --- /dev/null +++ b/dhall/src/core/valuef.rs @@ -0,0 +1,405 @@ +use std::collections::HashMap; + +use dhall_syntax::{ + rc, Builtin, Const, ExprF, Integer, InterpolatedTextContents, Label, + NaiveDouble, Natural, +}; + +use crate::core::value::{TypedValue, Value}; +use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; +use crate::phase::normalize::{ + apply_builtin, normalize_one_layer, squash_textlit, OutputSubExpr, +}; +use crate::phase::{Normalized, Typed}; + +/// A semantic value. The invariants ensure this value represents a Weak-Head +/// Normal Form (WHNF). This means that this first constructor is the first constructor of the +/// final Normal Form (NF). +/// This WHNF must be preserved by operations on `ValueF`s. In particular, `subst_shift` could break +/// the invariants so need to be careful to reevaluate as needed. +/// Subexpressions are Values, which are partially evaluated expressions that are normalized +/// on-demand. When all the Values in a ValueF are at least in WHNF, and recursively so, then the +/// ValueF is in NF. This is because WHNF ensures that we have the first constructor of the NF; so +/// if we have the first constructor of the NF at all levels, we actually have the NF. +/// Equality is up to alpha-equivalence (renaming of bound variables) and beta-equivalence +/// (normalization). Equality will normalize only as needed. +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum ValueF { + /// Closures + Lam(AlphaLabel, TypedValue, Value), + Pi(AlphaLabel, TypedValue, TypedValue), + // Invariant: the evaluation must not be able to progress further. + AppliedBuiltin(Builtin, Vec), + + Var(AlphaVar), + Const(Const), + BoolLit(bool), + NaturalLit(Natural), + IntegerLit(Integer), + DoubleLit(NaiveDouble), + EmptyOptionalLit(TypedValue), + NEOptionalLit(Value), + // EmptyListLit(t) means `[] : List t`, not `[] : t` + EmptyListLit(TypedValue), + NEListLit(Vec), + RecordLit(HashMap), + RecordType(HashMap), + UnionType(HashMap>), + UnionConstructor(Label, HashMap>), + UnionLit(Label, Value, HashMap>), + // Invariant: this must not contain interpolations that are themselves TextLits, and + // contiguous text values must be merged. + TextLit(Vec>), + Equivalence(TypedValue, TypedValue), + // Invariant: this must not contain a value captured by one of the variants above. + PartialExpr(ExprF), +} + +impl ValueF { + pub(crate) fn into_value(self) -> Value { + Value::from_valuef(self) + } + + /// Convert the value to a fully normalized syntactic expression + pub(crate) fn normalize_to_expr(&self) -> OutputSubExpr { + self.normalize_to_expr_maybe_alpha(false) + } + /// Convert the value to a fully normalized syntactic expression. Also alpha-normalize + /// if alpha is `true` + pub(crate) fn normalize_to_expr_maybe_alpha( + &self, + alpha: bool, + ) -> OutputSubExpr { + match self { + ValueF::Lam(x, t, e) => rc(ExprF::Lam( + x.to_label_maybe_alpha(alpha), + t.normalize_to_expr_maybe_alpha(alpha), + e.normalize_to_expr_maybe_alpha(alpha), + )), + ValueF::AppliedBuiltin(b, args) => { + let mut e = rc(ExprF::Builtin(*b)); + for v in args { + e = rc(ExprF::App( + e, + v.normalize_to_expr_maybe_alpha(alpha), + )); + } + e + } + ValueF::Pi(x, t, e) => rc(ExprF::Pi( + x.to_label_maybe_alpha(alpha), + t.normalize_to_expr_maybe_alpha(alpha), + e.normalize_to_expr_maybe_alpha(alpha), + )), + ValueF::Var(v) => rc(ExprF::Var(v.to_var(alpha))), + ValueF::Const(c) => rc(ExprF::Const(*c)), + ValueF::BoolLit(b) => rc(ExprF::BoolLit(*b)), + ValueF::NaturalLit(n) => rc(ExprF::NaturalLit(*n)), + ValueF::IntegerLit(n) => rc(ExprF::IntegerLit(*n)), + ValueF::DoubleLit(n) => rc(ExprF::DoubleLit(*n)), + ValueF::EmptyOptionalLit(n) => rc(ExprF::App( + rc(ExprF::Builtin(Builtin::OptionalNone)), + n.normalize_to_expr_maybe_alpha(alpha), + )), + ValueF::NEOptionalLit(n) => { + rc(ExprF::SomeLit(n.normalize_to_expr_maybe_alpha(alpha))) + } + ValueF::EmptyListLit(n) => rc(ExprF::EmptyListLit(rc(ExprF::App( + rc(ExprF::Builtin(Builtin::List)), + n.normalize_to_expr_maybe_alpha(alpha), + )))), + ValueF::NEListLit(elts) => rc(ExprF::NEListLit( + elts.iter() + .map(|n| n.normalize_to_expr_maybe_alpha(alpha)) + .collect(), + )), + ValueF::RecordLit(kvs) => rc(ExprF::RecordLit( + kvs.iter() + .map(|(k, v)| { + (k.clone(), v.normalize_to_expr_maybe_alpha(alpha)) + }) + .collect(), + )), + ValueF::RecordType(kts) => rc(ExprF::RecordType( + kts.iter() + .map(|(k, v)| { + (k.clone(), v.normalize_to_expr_maybe_alpha(alpha)) + }) + .collect(), + )), + ValueF::UnionType(kts) => rc(ExprF::UnionType( + kts.iter() + .map(|(k, v)| { + ( + k.clone(), + v.as_ref().map(|v| { + v.normalize_to_expr_maybe_alpha(alpha) + }), + ) + }) + .collect(), + )), + ValueF::UnionConstructor(l, kts) => { + let kts = kts + .iter() + .map(|(k, v)| { + ( + k.clone(), + v.as_ref().map(|v| { + v.normalize_to_expr_maybe_alpha(alpha) + }), + ) + }) + .collect(); + rc(ExprF::Field(rc(ExprF::UnionType(kts)), l.clone())) + } + ValueF::UnionLit(l, v, kts) => rc(ExprF::App( + ValueF::UnionConstructor(l.clone(), kts.clone()) + .normalize_to_expr_maybe_alpha(alpha), + v.normalize_to_expr_maybe_alpha(alpha), + )), + ValueF::TextLit(elts) => { + use InterpolatedTextContents::{Expr, Text}; + rc(ExprF::TextLit( + elts.iter() + .map(|contents| match contents { + Expr(e) => { + Expr(e.normalize_to_expr_maybe_alpha(alpha)) + } + Text(s) => Text(s.clone()), + }) + .collect(), + )) + } + ValueF::Equivalence(x, y) => rc(ExprF::BinOp( + dhall_syntax::BinOp::Equivalence, + x.normalize_to_expr_maybe_alpha(alpha), + y.normalize_to_expr_maybe_alpha(alpha), + )), + ValueF::PartialExpr(e) => { + rc(e.map_ref(|v| v.normalize_to_expr_maybe_alpha(alpha))) + } + } + } + + pub(crate) fn normalize_mut(&mut self) { + match self { + ValueF::Var(_) + | ValueF::Const(_) + | ValueF::BoolLit(_) + | ValueF::NaturalLit(_) + | ValueF::IntegerLit(_) + | ValueF::DoubleLit(_) => {} + + ValueF::EmptyOptionalLit(tth) | ValueF::EmptyListLit(tth) => { + tth.normalize_mut(); + } + + ValueF::NEOptionalLit(th) => { + th.normalize_mut(); + } + ValueF::Lam(_, t, e) => { + t.normalize_mut(); + e.normalize_mut(); + } + ValueF::Pi(_, t, e) => { + t.normalize_mut(); + e.normalize_mut(); + } + ValueF::AppliedBuiltin(_, args) => { + for x in args.iter_mut() { + x.normalize_mut(); + } + } + ValueF::NEListLit(elts) => { + for x in elts.iter_mut() { + x.normalize_mut(); + } + } + ValueF::RecordLit(kvs) => { + for x in kvs.values_mut() { + x.normalize_mut(); + } + } + ValueF::RecordType(kvs) => { + for x in kvs.values_mut() { + x.normalize_mut(); + } + } + ValueF::UnionType(kts) | ValueF::UnionConstructor(_, kts) => { + for x in kts.values_mut().flat_map(|opt| opt) { + x.normalize_mut(); + } + } + ValueF::UnionLit(_, v, kts) => { + v.normalize_mut(); + for x in kts.values_mut().flat_map(|opt| opt) { + x.normalize_mut(); + } + } + ValueF::TextLit(elts) => { + for x in elts.iter_mut() { + use InterpolatedTextContents::{Expr, Text}; + match x { + Expr(n) => n.normalize_mut(), + Text(_) => {} + } + } + } + ValueF::Equivalence(x, y) => { + x.normalize_mut(); + y.normalize_mut(); + } + ValueF::PartialExpr(e) => { + // TODO: need map_mut + e.map_ref(|v| { + v.normalize_nf(); + }); + } + } + } + + /// Apply to a value + pub(crate) fn app(self, val: ValueF) -> ValueF { + self.app_valuef(val) + } + + /// Apply to a value + pub(crate) fn app_valuef(self, val: ValueF) -> ValueF { + self.app_value(val.into_value()) + } + + /// Apply to a thunk + pub fn app_value(self, th: Value) -> ValueF { + Value::from_valuef(self).app_value(th) + } + + pub fn from_builtin(b: Builtin) -> ValueF { + ValueF::AppliedBuiltin(b, vec![]) + } +} + +impl Shift for ValueF { + fn shift(&self, delta: isize, var: &AlphaVar) -> Option { + Some(match self { + ValueF::Lam(x, t, e) => ValueF::Lam( + x.clone(), + t.shift(delta, var)?, + e.shift(delta, &var.under_binder(x))?, + ), + ValueF::AppliedBuiltin(b, args) => { + ValueF::AppliedBuiltin(*b, args.shift(delta, var)?) + } + ValueF::Pi(x, t, e) => ValueF::Pi( + x.clone(), + t.shift(delta, var)?, + e.shift(delta, &var.under_binder(x))?, + ), + ValueF::Var(v) => ValueF::Var(v.shift(delta, var)?), + ValueF::Const(c) => ValueF::Const(*c), + ValueF::BoolLit(b) => ValueF::BoolLit(*b), + ValueF::NaturalLit(n) => ValueF::NaturalLit(*n), + ValueF::IntegerLit(n) => ValueF::IntegerLit(*n), + ValueF::DoubleLit(n) => ValueF::DoubleLit(*n), + ValueF::EmptyOptionalLit(tth) => { + ValueF::EmptyOptionalLit(tth.shift(delta, var)?) + } + ValueF::NEOptionalLit(th) => { + ValueF::NEOptionalLit(th.shift(delta, var)?) + } + ValueF::EmptyListLit(tth) => { + ValueF::EmptyListLit(tth.shift(delta, var)?) + } + ValueF::NEListLit(elts) => { + ValueF::NEListLit(elts.shift(delta, var)?) + } + ValueF::RecordLit(kvs) => ValueF::RecordLit(kvs.shift(delta, var)?), + ValueF::RecordType(kvs) => { + ValueF::RecordType(kvs.shift(delta, var)?) + } + ValueF::UnionType(kts) => ValueF::UnionType(kts.shift(delta, var)?), + ValueF::UnionConstructor(x, kts) => { + ValueF::UnionConstructor(x.clone(), kts.shift(delta, var)?) + } + ValueF::UnionLit(x, v, kts) => ValueF::UnionLit( + x.clone(), + v.shift(delta, var)?, + kts.shift(delta, var)?, + ), + ValueF::TextLit(elts) => ValueF::TextLit(elts.shift(delta, var)?), + ValueF::Equivalence(x, y) => { + ValueF::Equivalence(x.shift(delta, var)?, y.shift(delta, var)?) + } + ValueF::PartialExpr(e) => ValueF::PartialExpr(e.shift(delta, var)?), + }) + } +} + +impl Subst for ValueF { + fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { + match self { + // Retry normalizing since substituting may allow progress + ValueF::AppliedBuiltin(b, args) => { + apply_builtin(*b, args.subst_shift(var, val)) + } + // Retry normalizing since substituting may allow progress + ValueF::PartialExpr(e) => { + normalize_one_layer(e.subst_shift(var, val)) + } + // Retry normalizing since substituting may allow progress + ValueF::TextLit(elts) => ValueF::TextLit(squash_textlit( + elts.iter().map(|contents| contents.subst_shift(var, val)), + )), + ValueF::Lam(x, t, e) => ValueF::Lam( + x.clone(), + t.subst_shift(var, val), + e.subst_shift(&var.under_binder(x), &val.under_binder(x)), + ), + ValueF::Pi(x, t, e) => ValueF::Pi( + x.clone(), + t.subst_shift(var, val), + e.subst_shift(&var.under_binder(x), &val.under_binder(x)), + ), + ValueF::Var(v) if v == var => val.to_valuef(), + ValueF::Var(v) => ValueF::Var(v.shift(-1, var).unwrap()), + ValueF::Const(c) => ValueF::Const(*c), + ValueF::BoolLit(b) => ValueF::BoolLit(*b), + ValueF::NaturalLit(n) => ValueF::NaturalLit(*n), + ValueF::IntegerLit(n) => ValueF::IntegerLit(*n), + ValueF::DoubleLit(n) => ValueF::DoubleLit(*n), + ValueF::EmptyOptionalLit(tth) => { + ValueF::EmptyOptionalLit(tth.subst_shift(var, val)) + } + ValueF::NEOptionalLit(th) => { + ValueF::NEOptionalLit(th.subst_shift(var, val)) + } + ValueF::EmptyListLit(tth) => { + ValueF::EmptyListLit(tth.subst_shift(var, val)) + } + ValueF::NEListLit(elts) => { + ValueF::NEListLit(elts.subst_shift(var, val)) + } + ValueF::RecordLit(kvs) => { + ValueF::RecordLit(kvs.subst_shift(var, val)) + } + ValueF::RecordType(kvs) => { + ValueF::RecordType(kvs.subst_shift(var, val)) + } + ValueF::UnionType(kts) => { + ValueF::UnionType(kts.subst_shift(var, val)) + } + ValueF::UnionConstructor(x, kts) => { + ValueF::UnionConstructor(x.clone(), kts.subst_shift(var, val)) + } + ValueF::UnionLit(x, v, kts) => ValueF::UnionLit( + x.clone(), + v.subst_shift(var, val), + kts.subst_shift(var, val), + ), + ValueF::Equivalence(x, y) => ValueF::Equivalence( + x.subst_shift(var, val), + y.subst_shift(var, val), + ), + } + } +} -- cgit v1.2.3 From c7d9a8659214a228963ea40d76e361bbc08129bb Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sun, 18 Aug 2019 15:24:13 +0200 Subject: Rework ValueInternal and clarify invariants around ValueF --- dhall/src/core/valuef.rs | 30 +++++++++--------------------- 1 file changed, 9 insertions(+), 21 deletions(-) (limited to 'dhall/src/core/valuef.rs') diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs index bea2e2e..9e6e8c8 100644 --- a/dhall/src/core/valuef.rs +++ b/dhall/src/core/valuef.rs @@ -7,22 +7,13 @@ use dhall_syntax::{ use crate::core::value::{TypedValue, Value}; use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; -use crate::phase::normalize::{ - apply_builtin, normalize_one_layer, squash_textlit, OutputSubExpr, -}; +use crate::phase::normalize::OutputSubExpr; use crate::phase::{Normalized, Typed}; -/// A semantic value. The invariants ensure this value represents a Weak-Head -/// Normal Form (WHNF). This means that this first constructor is the first constructor of the -/// final Normal Form (NF). -/// This WHNF must be preserved by operations on `ValueF`s. In particular, `subst_shift` could break -/// the invariants so need to be careful to reevaluate as needed. -/// Subexpressions are Values, which are partially evaluated expressions that are normalized -/// on-demand. When all the Values in a ValueF are at least in WHNF, and recursively so, then the -/// ValueF is in NF. This is because WHNF ensures that we have the first constructor of the NF; so -/// if we have the first constructor of the NF at all levels, we actually have the NF. +/// A semantic value. Subexpressions are Values, which are partially evaluated expressions that are +/// normalized on-demand. /// Equality is up to alpha-equivalence (renaming of bound variables) and beta-equivalence -/// (normalization). Equality will normalize only as needed. +/// (normalization). Equality will normalize as needed. #[derive(Debug, Clone, PartialEq, Eq)] pub enum ValueF { /// Closures @@ -338,18 +329,15 @@ impl Shift for ValueF { impl Subst for ValueF { fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { match self { - // Retry normalizing since substituting may allow progress ValueF::AppliedBuiltin(b, args) => { - apply_builtin(*b, args.subst_shift(var, val)) + ValueF::AppliedBuiltin(*b, args.subst_shift(var, val)) } - // Retry normalizing since substituting may allow progress ValueF::PartialExpr(e) => { - normalize_one_layer(e.subst_shift(var, val)) + ValueF::PartialExpr(e.subst_shift(var, val)) + } + ValueF::TextLit(elts) => { + ValueF::TextLit(elts.subst_shift(var, val)) } - // Retry normalizing since substituting may allow progress - ValueF::TextLit(elts) => ValueF::TextLit(squash_textlit( - elts.iter().map(|contents| contents.subst_shift(var, val)), - )), ValueF::Lam(x, t, e) => ValueF::Lam( x.clone(), t.subst_shift(var, val), -- cgit v1.2.3 From 29016b78736dca857e4e7f7c4dc68ed5e30c28bb Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 19 Aug 2019 12:25:09 +0200 Subject: s/to_valuef/to_whnf/ and avoid cloning ValueFs when possible --- dhall/src/core/valuef.rs | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'dhall/src/core/valuef.rs') diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs index 9e6e8c8..0ba1d59 100644 --- a/dhall/src/core/valuef.rs +++ b/dhall/src/core/valuef.rs @@ -12,8 +12,9 @@ use crate::phase::{Normalized, Typed}; /// A semantic value. Subexpressions are Values, which are partially evaluated expressions that are /// normalized on-demand. -/// Equality is up to alpha-equivalence (renaming of bound variables) and beta-equivalence -/// (normalization). Equality will normalize as needed. +/// If you compare for equality two `ValueF`s in WHNF, then equality will be up to +/// alpha-equivalence (renaming of bound variables) and beta-equivalence (normalization). It will +/// recursively normalize as needed. #[derive(Debug, Clone, PartialEq, Eq)] pub enum ValueF { /// Closures @@ -348,7 +349,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_valuef(), + ValueF::Var(v) if v == var => val.to_whnf(), 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 26a1fd0f0861038a76a0f9b09eaef16d808d4139 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 19 Aug 2019 21:52:26 +0200 Subject: Use TypedValue instead of Typed in normalize and typecheck Now Typed is only used in dhall::phase, similarly to Parsed/Resolved/Normalized --- dhall/src/core/valuef.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'dhall/src/core/valuef.rs') diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs index 0ba1d59..b948eb1 100644 --- a/dhall/src/core/valuef.rs +++ b/dhall/src/core/valuef.rs @@ -8,7 +8,7 @@ use dhall_syntax::{ use crate::core::value::{TypedValue, Value}; use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; use crate::phase::normalize::OutputSubExpr; -use crate::phase::{Normalized, Typed}; +use crate::phase::Normalized; /// A semantic value. Subexpressions are Values, which are partially evaluated expressions that are /// normalized on-demand. @@ -327,8 +327,8 @@ impl Shift for ValueF { } } -impl Subst for ValueF { - fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { +impl Subst for ValueF { + fn subst_shift(&self, var: &AlphaVar, val: &TypedValue) -> Self { match self { ValueF::AppliedBuiltin(b, args) => { ValueF::AppliedBuiltin(*b, args.subst_shift(var, val)) -- cgit v1.2.3 From 07a276c1d6ee892b93abbd7a73c78c96d56f4fe7 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 19 Aug 2019 22:26:17 +0200 Subject: Reduce untyped construction of Values --- dhall/src/core/valuef.rs | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) (limited to 'dhall/src/core/valuef.rs') diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs index b948eb1..de55d2f 100644 --- a/dhall/src/core/valuef.rs +++ b/dhall/src/core/valuef.rs @@ -48,8 +48,14 @@ pub enum ValueF { } impl ValueF { - pub(crate) fn into_value(self) -> Value { - Value::from_valuef(self) + pub(crate) fn into_value_untyped(self) -> Value { + Value::from_valuef_untyped(self) + } + pub(crate) fn into_value_with_type(self, t: TypedValue) -> Value { + Value::from_valuef_and_type(self, t) + } + pub(crate) fn into_value_simple_type(self) -> Value { + Value::from_valuef_simple_type(self) } /// Convert the value to a fully normalized syntactic expression @@ -258,12 +264,12 @@ impl ValueF { /// Apply to a value pub(crate) fn app_valuef(self, val: ValueF) -> ValueF { - self.app_value(val.into_value()) + self.app_value(val.into_value_untyped()) } /// Apply to a thunk pub fn app_value(self, th: Value) -> ValueF { - Value::from_valuef(self).app_value(th) + Value::from_valuef_untyped(self).app_value(th) } pub fn from_builtin(b: Builtin) -> ValueF { -- cgit v1.2.3 From 730f2ebb146792994c7492b6c05f7d09d42cbccf Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 19 Aug 2019 23:00:49 +0200 Subject: Merge TypedValue and Value --- dhall/src/core/valuef.rs | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) (limited to 'dhall/src/core/valuef.rs') diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs index de55d2f..0d2655e 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::{TypedValue, Value}; +use crate::core::value::Value; use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; use crate::phase::normalize::OutputSubExpr; use crate::phase::Normalized; @@ -18,8 +18,8 @@ use crate::phase::Normalized; #[derive(Debug, Clone, PartialEq, Eq)] pub enum ValueF { /// Closures - Lam(AlphaLabel, TypedValue, Value), - Pi(AlphaLabel, TypedValue, TypedValue), + Lam(AlphaLabel, Value, Value), + Pi(AlphaLabel, Value, Value), // Invariant: the evaluation must not be able to progress further. AppliedBuiltin(Builtin, Vec), @@ -29,20 +29,20 @@ pub enum ValueF { NaturalLit(Natural), IntegerLit(Integer), DoubleLit(NaiveDouble), - EmptyOptionalLit(TypedValue), + EmptyOptionalLit(Value), NEOptionalLit(Value), // EmptyListLit(t) means `[] : List t`, not `[] : t` - EmptyListLit(TypedValue), + EmptyListLit(Value), NEListLit(Vec), RecordLit(HashMap), - RecordType(HashMap), - UnionType(HashMap>), - UnionConstructor(Label, HashMap>), - UnionLit(Label, Value, HashMap>), + RecordType(HashMap), + UnionType(HashMap>), + UnionConstructor(Label, HashMap>), + UnionLit(Label, Value, HashMap>), // Invariant: this must not contain interpolations that are themselves TextLits, and // contiguous text values must be merged. TextLit(Vec>), - Equivalence(TypedValue, TypedValue), + Equivalence(Value, Value), // Invariant: this must not contain a value captured by one of the variants above. PartialExpr(ExprF), } @@ -51,7 +51,7 @@ impl ValueF { pub(crate) fn into_value_untyped(self) -> Value { Value::from_valuef_untyped(self) } - pub(crate) fn into_value_with_type(self, t: TypedValue) -> Value { + 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 { @@ -333,8 +333,8 @@ impl Shift for ValueF { } } -impl Subst for ValueF { - fn subst_shift(&self, var: &AlphaVar, val: &TypedValue) -> Self { +impl Subst for ValueF { + fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { match self { ValueF::AppliedBuiltin(b, args) => { ValueF::AppliedBuiltin(*b, args.subst_shift(var, val)) -- cgit v1.2.3 From caf36246a517b884d7cfcf7c31e1b5d8fce60dfa Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 20 Aug 2019 13:49:13 +0200 Subject: Cleanup --- dhall/src/core/valuef.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'dhall/src/core/valuef.rs') diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs index 0d2655e..0c3058d 100644 --- a/dhall/src/core/valuef.rs +++ b/dhall/src/core/valuef.rs @@ -257,17 +257,17 @@ impl ValueF { } } - /// Apply to a value + /// Apply to a valuef pub(crate) fn app(self, val: ValueF) -> ValueF { self.app_valuef(val) } - /// Apply to a value + /// Apply to a valuef pub(crate) fn app_valuef(self, val: ValueF) -> ValueF { self.app_value(val.into_value_untyped()) } - /// Apply to a thunk + /// 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 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/valuef.rs | 10 ---------- 1 file changed, 10 deletions(-) (limited to 'dhall/src/core/valuef.rs') 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/valuef.rs | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) (limited to 'dhall/src/core/valuef.rs') 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/valuef.rs | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) (limited to 'dhall/src/core/valuef.rs') 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 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/valuef.rs | 32 ++++++++++++++++++++++---------- 1 file changed, 22 insertions(+), 10 deletions(-) (limited to 'dhall/src/core/valuef.rs') 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 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/valuef.rs') 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/valuef.rs | 15 ++------------- 1 file changed, 2 insertions(+), 13 deletions(-) (limited to 'dhall/src/core/valuef.rs') 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 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/valuef.rs | 3 --- 1 file changed, 3 deletions(-) (limited to 'dhall/src/core/valuef.rs') 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 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/valuef.rs | 10 ++-------- 1 file changed, 2 insertions(+), 8 deletions(-) (limited to 'dhall/src/core/valuef.rs') 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 a7363042a16364a6dafdd545f4069dcf04a4197e Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 27 Aug 2019 23:18:13 +0200 Subject: Rename SubExpr to Expr, and Expr to RawExpr For clarity, and consistency with Value --- dhall/src/core/valuef.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'dhall/src/core/valuef.rs') diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs index 9ea2467..959f299 100644 --- a/dhall/src/core/valuef.rs +++ b/dhall/src/core/valuef.rs @@ -7,7 +7,7 @@ use dhall_syntax::{ use crate::core::value::Value; use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; -use crate::phase::{Normalized, NormalizedSubExpr}; +use crate::phase::{Normalized, NormalizedExpr}; /// A semantic value. Subexpressions are Values, which are partially evaluated expressions that are /// normalized on-demand. @@ -52,7 +52,7 @@ impl ValueF { } /// Convert the value to a fully normalized syntactic expression - pub(crate) fn normalize_to_expr(&self) -> NormalizedSubExpr { + pub(crate) fn normalize_to_expr(&self) -> NormalizedExpr { self.normalize_to_expr_maybe_alpha(false) } /// Convert the value to a fully normalized syntactic expression. Also alpha-normalize @@ -60,7 +60,7 @@ impl ValueF { pub(crate) fn normalize_to_expr_maybe_alpha( &self, alpha: bool, - ) -> NormalizedSubExpr { + ) -> NormalizedExpr { match self { ValueF::Lam(x, t, e) => rc(ExprF::Lam( x.to_label_maybe_alpha(alpha), -- cgit v1.2.3 From 55c127e70eb484df486a45b25bcf03479eebda10 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 28 Aug 2019 13:49:27 +0200 Subject: Cleanup conversion of `Value` to `Expr` --- dhall/src/core/valuef.rs | 103 ++++++++++++++--------------------------------- 1 file changed, 30 insertions(+), 73 deletions(-) (limited to 'dhall/src/core/valuef.rs') diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs index 959f299..7ecec86 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::{ToExprOptions, Value}; use crate::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; use crate::phase::{Normalized, NormalizedExpr}; @@ -51,38 +51,23 @@ impl ValueF { Value::from_valuef_and_type(self, t) } - /// Convert the value to a fully normalized syntactic expression - pub(crate) fn normalize_to_expr(&self) -> NormalizedExpr { - self.normalize_to_expr_maybe_alpha(false) - } - /// Convert the value to a fully normalized syntactic expression. Also alpha-normalize - /// if alpha is `true` - pub(crate) fn normalize_to_expr_maybe_alpha( - &self, - alpha: bool, - ) -> NormalizedExpr { + pub(crate) fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr { match self { ValueF::Lam(x, t, e) => rc(ExprF::Lam( - x.to_label_maybe_alpha(alpha), - t.normalize_to_expr_maybe_alpha(alpha), - e.normalize_to_expr_maybe_alpha(alpha), + x.to_label_maybe_alpha(opts.alpha), + t.to_expr(opts), + e.to_expr(opts), )), - ValueF::AppliedBuiltin(b, args) => { - let mut e = rc(ExprF::Builtin(*b)); - for v in args { - e = rc(ExprF::App( - e, - v.normalize_to_expr_maybe_alpha(alpha), - )); - } - e - } + ValueF::AppliedBuiltin(b, args) => args + .iter() + .map(|v| v.to_expr(opts)) + .fold(rc(ExprF::Builtin(*b)), |acc, v| rc(ExprF::App(acc, v))), ValueF::Pi(x, t, e) => rc(ExprF::Pi( - x.to_label_maybe_alpha(alpha), - t.normalize_to_expr_maybe_alpha(alpha), - e.normalize_to_expr_maybe_alpha(alpha), + x.to_label_maybe_alpha(opts.alpha), + t.to_expr(opts), + e.to_expr(opts), )), - ValueF::Var(v) => rc(ExprF::Var(v.to_var(alpha))), + ValueF::Var(v) => rc(ExprF::Var(v.to_var(opts.alpha))), ValueF::Const(c) => rc(ExprF::Const(*c)), ValueF::BoolLit(b) => rc(ExprF::BoolLit(*b)), ValueF::NaturalLit(n) => rc(ExprF::NaturalLit(*n)), @@ -90,73 +75,47 @@ impl ValueF { ValueF::DoubleLit(n) => rc(ExprF::DoubleLit(*n)), ValueF::EmptyOptionalLit(n) => rc(ExprF::App( rc(ExprF::Builtin(Builtin::OptionalNone)), - n.normalize_to_expr_maybe_alpha(alpha), + n.to_expr(opts), )), - ValueF::NEOptionalLit(n) => { - rc(ExprF::SomeLit(n.normalize_to_expr_maybe_alpha(alpha))) - } + ValueF::NEOptionalLit(n) => rc(ExprF::SomeLit(n.to_expr(opts))), ValueF::EmptyListLit(n) => rc(ExprF::EmptyListLit(rc(ExprF::App( rc(ExprF::Builtin(Builtin::List)), - n.normalize_to_expr_maybe_alpha(alpha), + n.to_expr(opts), )))), ValueF::NEListLit(elts) => rc(ExprF::NEListLit( - elts.iter() - .map(|n| n.normalize_to_expr_maybe_alpha(alpha)) - .collect(), + elts.iter().map(|n| n.to_expr(opts)).collect(), )), ValueF::RecordLit(kvs) => rc(ExprF::RecordLit( kvs.iter() - .map(|(k, v)| { - (k.clone(), v.normalize_to_expr_maybe_alpha(alpha)) - }) + .map(|(k, v)| (k.clone(), v.to_expr(opts))) .collect(), )), ValueF::RecordType(kts) => rc(ExprF::RecordType( kts.iter() - .map(|(k, v)| { - (k.clone(), v.normalize_to_expr_maybe_alpha(alpha)) - }) + .map(|(k, v)| (k.clone(), v.to_expr(opts))) .collect(), )), ValueF::UnionType(kts) => rc(ExprF::UnionType( kts.iter() .map(|(k, v)| { - ( - k.clone(), - v.as_ref().map(|v| { - v.normalize_to_expr_maybe_alpha(alpha) - }), - ) + (k.clone(), v.as_ref().map(|v| v.to_expr(opts))) }) .collect(), )), - ValueF::UnionConstructor(l, kts) => { - let kts = kts - .iter() - .map(|(k, v)| { - ( - k.clone(), - v.as_ref().map(|v| { - v.normalize_to_expr_maybe_alpha(alpha) - }), - ) - }) - .collect(); - rc(ExprF::Field(rc(ExprF::UnionType(kts)), l.clone())) - } + ValueF::UnionConstructor(l, kts) => rc(ExprF::Field( + ValueF::UnionType(kts.clone()).to_expr(opts), + l.clone(), + )), ValueF::UnionLit(l, v, kts) => rc(ExprF::App( - ValueF::UnionConstructor(l.clone(), kts.clone()) - .normalize_to_expr_maybe_alpha(alpha), - v.normalize_to_expr_maybe_alpha(alpha), + ValueF::UnionConstructor(l.clone(), kts.clone()).to_expr(opts), + v.to_expr(opts), )), ValueF::TextLit(elts) => { use InterpolatedTextContents::{Expr, Text}; rc(ExprF::TextLit( elts.iter() .map(|contents| match contents { - Expr(e) => { - Expr(e.normalize_to_expr_maybe_alpha(alpha)) - } + Expr(e) => Expr(e.to_expr(opts)), Text(s) => Text(s.clone()), }) .collect(), @@ -164,12 +123,10 @@ impl ValueF { } ValueF::Equivalence(x, y) => rc(ExprF::BinOp( dhall_syntax::BinOp::Equivalence, - x.normalize_to_expr_maybe_alpha(alpha), - y.normalize_to_expr_maybe_alpha(alpha), + x.to_expr(opts), + y.to_expr(opts), )), - ValueF::PartialExpr(e) => { - rc(e.map_ref(|v| v.normalize_to_expr_maybe_alpha(alpha))) - } + ValueF::PartialExpr(e) => rc(e.map_ref(|v| v.to_expr(opts))), } } -- cgit v1.2.3