From e0f5216215ccb7a4df85d80e11dd265cdb52a44f Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 16 Aug 2019 19:47:36 +0200 Subject: s/Value/ValueF/ --- dhall/src/core/value.rs | 212 ++++++++++++++++++++++++------------------------ 1 file changed, 106 insertions(+), 106 deletions(-) (limited to 'dhall/src/core/value.rs') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index d3d017d..0f2ef00 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -15,16 +15,16 @@ 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 `Value`s. In particular, `subst_shift` could break +/// 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 Thunks, which are partially evaluated expressions that are normalized -/// on-demand. When all the Thunks in a Value are at least in WHNF, and recursively so, then the -/// Value is in NF. This is because WHNF ensures that we have the first constructor of the NF; so +/// on-demand. When all the Thunks 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 Value { +pub enum ValueF { /// Closures Lam(AlphaLabel, TypedThunk, Thunk), Pi(AlphaLabel, TypedThunk, TypedThunk), @@ -55,9 +55,9 @@ pub enum Value { PartialExpr(ExprF), } -impl Value { +impl ValueF { pub(crate) fn into_thunk(self) -> Thunk { - Thunk::from_value(self) + Thunk::from_valuef(self) } /// Convert the value to a fully normalized syntactic expression @@ -71,12 +71,12 @@ impl Value { alpha: bool, ) -> OutputSubExpr { match self { - Value::Lam(x, t, e) => rc(ExprF::Lam( + 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), )), - Value::AppliedBuiltin(b, args) => { + ValueF::AppliedBuiltin(b, args) => { let mut e = rc(ExprF::Builtin(*b)); for v in args { e = rc(ExprF::App( @@ -86,48 +86,48 @@ impl Value { } e } - Value::Pi(x, t, e) => rc(ExprF::Pi( + 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), )), - Value::Var(v) => rc(ExprF::Var(v.to_var(alpha))), - Value::Const(c) => rc(ExprF::Const(*c)), - Value::BoolLit(b) => rc(ExprF::BoolLit(*b)), - Value::NaturalLit(n) => rc(ExprF::NaturalLit(*n)), - Value::IntegerLit(n) => rc(ExprF::IntegerLit(*n)), - Value::DoubleLit(n) => rc(ExprF::DoubleLit(*n)), - Value::EmptyOptionalLit(n) => rc(ExprF::App( + 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), )), - Value::NEOptionalLit(n) => { + ValueF::NEOptionalLit(n) => { rc(ExprF::SomeLit(n.normalize_to_expr_maybe_alpha(alpha))) } - Value::EmptyListLit(n) => rc(ExprF::EmptyListLit(rc(ExprF::App( + ValueF::EmptyListLit(n) => rc(ExprF::EmptyListLit(rc(ExprF::App( rc(ExprF::Builtin(Builtin::List)), n.normalize_to_expr_maybe_alpha(alpha), )))), - Value::NEListLit(elts) => rc(ExprF::NEListLit( + ValueF::NEListLit(elts) => rc(ExprF::NEListLit( elts.iter() .map(|n| n.normalize_to_expr_maybe_alpha(alpha)) .collect(), )), - Value::RecordLit(kvs) => rc(ExprF::RecordLit( + ValueF::RecordLit(kvs) => rc(ExprF::RecordLit( kvs.iter() .map(|(k, v)| { (k.clone(), v.normalize_to_expr_maybe_alpha(alpha)) }) .collect(), )), - Value::RecordType(kts) => rc(ExprF::RecordType( + ValueF::RecordType(kts) => rc(ExprF::RecordType( kts.iter() .map(|(k, v)| { (k.clone(), v.normalize_to_expr_maybe_alpha(alpha)) }) .collect(), )), - Value::UnionType(kts) => rc(ExprF::UnionType( + ValueF::UnionType(kts) => rc(ExprF::UnionType( kts.iter() .map(|(k, v)| { ( @@ -139,7 +139,7 @@ impl Value { }) .collect(), )), - Value::UnionConstructor(l, kts) => { + ValueF::UnionConstructor(l, kts) => { let kts = kts .iter() .map(|(k, v)| { @@ -153,12 +153,12 @@ impl Value { .collect(); rc(ExprF::Field(rc(ExprF::UnionType(kts)), l.clone())) } - Value::UnionLit(l, v, kts) => rc(ExprF::App( - Value::UnionConstructor(l.clone(), kts.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), )), - Value::TextLit(elts) => { + ValueF::TextLit(elts) => { use InterpolatedTextContents::{Expr, Text}; rc(ExprF::TextLit( elts.iter() @@ -171,12 +171,12 @@ impl Value { .collect(), )) } - Value::Equivalence(x, y) => rc(ExprF::BinOp( + 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), )), - Value::PartialExpr(e) => { + ValueF::PartialExpr(e) => { rc(e.map_ref(|v| v.normalize_to_expr_maybe_alpha(alpha))) } } @@ -184,60 +184,60 @@ impl Value { pub(crate) fn normalize_mut(&mut self) { match self { - Value::Var(_) - | Value::Const(_) - | Value::BoolLit(_) - | Value::NaturalLit(_) - | Value::IntegerLit(_) - | Value::DoubleLit(_) => {} + ValueF::Var(_) + | ValueF::Const(_) + | ValueF::BoolLit(_) + | ValueF::NaturalLit(_) + | ValueF::IntegerLit(_) + | ValueF::DoubleLit(_) => {} - Value::EmptyOptionalLit(tth) | Value::EmptyListLit(tth) => { + ValueF::EmptyOptionalLit(tth) | ValueF::EmptyListLit(tth) => { tth.normalize_mut(); } - Value::NEOptionalLit(th) => { + ValueF::NEOptionalLit(th) => { th.normalize_mut(); } - Value::Lam(_, t, e) => { + ValueF::Lam(_, t, e) => { t.normalize_mut(); e.normalize_mut(); } - Value::Pi(_, t, e) => { + ValueF::Pi(_, t, e) => { t.normalize_mut(); e.normalize_mut(); } - Value::AppliedBuiltin(_, args) => { + ValueF::AppliedBuiltin(_, args) => { for x in args.iter_mut() { x.normalize_mut(); } } - Value::NEListLit(elts) => { + ValueF::NEListLit(elts) => { for x in elts.iter_mut() { x.normalize_mut(); } } - Value::RecordLit(kvs) => { + ValueF::RecordLit(kvs) => { for x in kvs.values_mut() { x.normalize_mut(); } } - Value::RecordType(kvs) => { + ValueF::RecordType(kvs) => { for x in kvs.values_mut() { x.normalize_mut(); } } - Value::UnionType(kts) | Value::UnionConstructor(_, kts) => { + ValueF::UnionType(kts) | ValueF::UnionConstructor(_, kts) => { for x in kts.values_mut().flat_map(|opt| opt) { x.normalize_mut(); } } - Value::UnionLit(_, v, kts) => { + ValueF::UnionLit(_, v, kts) => { v.normalize_mut(); for x in kts.values_mut().flat_map(|opt| opt) { x.normalize_mut(); } } - Value::TextLit(elts) => { + ValueF::TextLit(elts) => { for x in elts.iter_mut() { use InterpolatedTextContents::{Expr, Text}; match x { @@ -246,11 +246,11 @@ impl Value { } } } - Value::Equivalence(x, y) => { + ValueF::Equivalence(x, y) => { x.normalize_mut(); y.normalize_mut(); } - Value::PartialExpr(e) => { + ValueF::PartialExpr(e) => { // TODO: need map_mut e.map_ref(|v| { v.normalize_nf(); @@ -260,75 +260,75 @@ impl Value { } /// Apply to a value - pub(crate) fn app(self, val: Value) -> Value { + pub(crate) fn app(self, val: ValueF) -> ValueF { self.app_val(val) } /// Apply to a value - pub(crate) fn app_val(self, val: Value) -> Value { + pub(crate) fn app_val(self, val: ValueF) -> ValueF { self.app_thunk(val.into_thunk()) } /// Apply to a thunk - pub fn app_thunk(self, th: Thunk) -> Value { - Thunk::from_value(self).app_thunk(th) + pub fn app_thunk(self, th: Thunk) -> ValueF { + Thunk::from_valuef(self).app_thunk(th) } - pub fn from_builtin(b: Builtin) -> Value { - Value::AppliedBuiltin(b, vec![]) + pub fn from_builtin(b: Builtin) -> ValueF { + ValueF::AppliedBuiltin(b, vec![]) } } -impl Shift for Value { +impl Shift for ValueF { fn shift(&self, delta: isize, var: &AlphaVar) -> Option { Some(match self { - Value::Lam(x, t, e) => Value::Lam( + ValueF::Lam(x, t, e) => ValueF::Lam( x.clone(), t.shift(delta, var)?, e.shift(delta, &var.under_binder(x))?, ), - Value::AppliedBuiltin(b, args) => Value::AppliedBuiltin( + ValueF::AppliedBuiltin(b, args) => ValueF::AppliedBuiltin( *b, args.iter() .map(|v| Ok(v.shift(delta, var)?)) .collect::>()?, ), - Value::Pi(x, t, e) => Value::Pi( + ValueF::Pi(x, t, e) => ValueF::Pi( x.clone(), t.shift(delta, var)?, e.shift(delta, &var.under_binder(x))?, ), - Value::Var(v) => Value::Var(v.shift(delta, var)?), - Value::Const(c) => Value::Const(*c), - Value::BoolLit(b) => Value::BoolLit(*b), - Value::NaturalLit(n) => Value::NaturalLit(*n), - Value::IntegerLit(n) => Value::IntegerLit(*n), - Value::DoubleLit(n) => Value::DoubleLit(*n), - Value::EmptyOptionalLit(tth) => { - Value::EmptyOptionalLit(tth.shift(delta, var)?) + 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)?) } - Value::NEOptionalLit(th) => { - Value::NEOptionalLit(th.shift(delta, var)?) + ValueF::NEOptionalLit(th) => { + ValueF::NEOptionalLit(th.shift(delta, var)?) } - Value::EmptyListLit(tth) => { - Value::EmptyListLit(tth.shift(delta, var)?) + ValueF::EmptyListLit(tth) => { + ValueF::EmptyListLit(tth.shift(delta, var)?) } - Value::NEListLit(elts) => Value::NEListLit( + ValueF::NEListLit(elts) => ValueF::NEListLit( elts.iter() .map(|v| Ok(v.shift(delta, var)?)) .collect::>()?, ), - Value::RecordLit(kvs) => Value::RecordLit( + ValueF::RecordLit(kvs) => ValueF::RecordLit( kvs.iter() .map(|(k, v)| Ok((k.clone(), v.shift(delta, var)?))) .collect::>()?, ), - Value::RecordType(kvs) => Value::RecordType( + ValueF::RecordType(kvs) => ValueF::RecordType( kvs.iter() .map(|(k, v)| Ok((k.clone(), v.shift(delta, var)?))) .collect::>()?, ), - Value::UnionType(kts) => Value::UnionType( + ValueF::UnionType(kts) => ValueF::UnionType( kts.iter() .map(|(k, v)| { Ok(( @@ -340,7 +340,7 @@ impl Shift for Value { }) .collect::>()?, ), - Value::UnionConstructor(x, kts) => Value::UnionConstructor( + ValueF::UnionConstructor(x, kts) => ValueF::UnionConstructor( x.clone(), kts.iter() .map(|(k, v)| { @@ -353,7 +353,7 @@ impl Shift for Value { }) .collect::>()?, ), - Value::UnionLit(x, v, kts) => Value::UnionLit( + ValueF::UnionLit(x, v, kts) => ValueF::UnionLit( x.clone(), v.shift(delta, var)?, kts.iter() @@ -367,7 +367,7 @@ impl Shift for Value { }) .collect::>()?, ), - Value::TextLit(elts) => Value::TextLit( + ValueF::TextLit(elts) => ValueF::TextLit( elts.iter() .map(|contents| { use InterpolatedTextContents::{Expr, Text}; @@ -378,10 +378,10 @@ impl Shift for Value { }) .collect::>()?, ), - Value::Equivalence(x, y) => { - Value::Equivalence(x.shift(delta, var)?, y.shift(delta, var)?) + ValueF::Equivalence(x, y) => { + ValueF::Equivalence(x.shift(delta, var)?, y.shift(delta, var)?) } - Value::PartialExpr(e) => Value::PartialExpr( + ValueF::PartialExpr(e) => ValueF::PartialExpr( e.traverse_ref_with_special_handling_of_binders( |v| Ok(v.shift(delta, var)?), |x, v| Ok(v.shift(delta, &var.under_binder(x))?), @@ -391,16 +391,16 @@ impl Shift for Value { } } -impl Subst for Value { +impl Subst for ValueF { fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { match self { // Retry normalizing since substituting may allow progress - Value::AppliedBuiltin(b, args) => apply_builtin( + ValueF::AppliedBuiltin(b, args) => apply_builtin( *b, args.iter().map(|v| v.subst_shift(var, val)).collect(), ), // Retry normalizing since substituting may allow progress - Value::PartialExpr(e) => { + ValueF::PartialExpr(e) => { normalize_one_layer(e.map_ref_with_special_handling_of_binders( |v| v.subst_shift(var, val), |x, v| { @@ -412,8 +412,8 @@ impl Subst for Value { )) } // Retry normalizing since substituting may allow progress - Value::TextLit(elts) => { - Value::TextLit(squash_textlit(elts.iter().map(|contents| { + ValueF::TextLit(elts) => { + ValueF::TextLit(squash_textlit(elts.iter().map(|contents| { use InterpolatedTextContents::{Expr, Text}; match contents { Expr(th) => Expr(th.subst_shift(var, val)), @@ -421,53 +421,53 @@ impl Subst for Value { } }))) } - Value::Lam(x, t, e) => Value::Lam( + 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)), ), - Value::Pi(x, t, e) => Value::Pi( + 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)), ), - Value::Var(v) if v == var => val.to_value(), - Value::Var(v) => Value::Var(v.shift(-1, var).unwrap()), - Value::Const(c) => Value::Const(*c), - Value::BoolLit(b) => Value::BoolLit(*b), - Value::NaturalLit(n) => Value::NaturalLit(*n), - Value::IntegerLit(n) => Value::IntegerLit(*n), - Value::DoubleLit(n) => Value::DoubleLit(*n), - Value::EmptyOptionalLit(tth) => { - Value::EmptyOptionalLit(tth.subst_shift(var, val)) + 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)) } - Value::NEOptionalLit(th) => { - Value::NEOptionalLit(th.subst_shift(var, val)) + ValueF::NEOptionalLit(th) => { + ValueF::NEOptionalLit(th.subst_shift(var, val)) } - Value::EmptyListLit(tth) => { - Value::EmptyListLit(tth.subst_shift(var, val)) + ValueF::EmptyListLit(tth) => { + ValueF::EmptyListLit(tth.subst_shift(var, val)) } - Value::NEListLit(elts) => Value::NEListLit( + ValueF::NEListLit(elts) => ValueF::NEListLit( elts.iter().map(|v| v.subst_shift(var, val)).collect(), ), - Value::RecordLit(kvs) => Value::RecordLit( + ValueF::RecordLit(kvs) => ValueF::RecordLit( kvs.iter() .map(|(k, v)| (k.clone(), v.subst_shift(var, val))) .collect(), ), - Value::RecordType(kvs) => Value::RecordType( + ValueF::RecordType(kvs) => ValueF::RecordType( kvs.iter() .map(|(k, v)| (k.clone(), v.subst_shift(var, val))) .collect(), ), - Value::UnionType(kts) => Value::UnionType( + ValueF::UnionType(kts) => ValueF::UnionType( kts.iter() .map(|(k, v)| { (k.clone(), v.as_ref().map(|v| v.subst_shift(var, val))) }) .collect(), ), - Value::UnionConstructor(x, kts) => Value::UnionConstructor( + ValueF::UnionConstructor(x, kts) => ValueF::UnionConstructor( x.clone(), kts.iter() .map(|(k, v)| { @@ -475,7 +475,7 @@ impl Subst for Value { }) .collect(), ), - Value::UnionLit(x, v, kts) => Value::UnionLit( + ValueF::UnionLit(x, v, kts) => ValueF::UnionLit( x.clone(), v.subst_shift(var, val), kts.iter() @@ -484,7 +484,7 @@ impl Subst for Value { }) .collect(), ), - Value::Equivalence(x, y) => Value::Equivalence( + ValueF::Equivalence(x, y) => ValueF::Equivalence( x.subst_shift(var, val), y.subst_shift(var, val), ), -- cgit v1.2.3