summaryrefslogtreecommitdiff
path: root/dhall/src/core/value.rs
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src/core/value.rs')
-rw-r--r--dhall/src/core/value.rs212
1 files changed, 106 insertions, 106 deletions
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<Thunk, Normalized>),
}
-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<Self> {
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::<Result<_, _>>()?,
),
- 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::<Result<_, _>>()?,
),
- Value::RecordLit(kvs) => Value::RecordLit(
+ ValueF::RecordLit(kvs) => ValueF::RecordLit(
kvs.iter()
.map(|(k, v)| Ok((k.clone(), v.shift(delta, var)?)))
.collect::<Result<_, _>>()?,
),
- Value::RecordType(kvs) => Value::RecordType(
+ ValueF::RecordType(kvs) => ValueF::RecordType(
kvs.iter()
.map(|(k, v)| Ok((k.clone(), v.shift(delta, var)?)))
.collect::<Result<_, _>>()?,
),
- 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::<Result<_, _>>()?,
),
- 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::<Result<_, _>>()?,
),
- 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::<Result<_, _>>()?,
),
- 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::<Result<_, _>>()?,
),
- 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<Typed> for Value {
+impl Subst<Typed> 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<Typed> 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<Typed> 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<Typed> 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<Typed> 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),
),
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-05 15:04:27 +0000