summaryrefslogtreecommitdiff
path: root/dhall/src/core
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/src/core/context.rs4
-rw-r--r--dhall/src/core/thunk.rs90
-rw-r--r--dhall/src/core/value.rs212
-rw-r--r--dhall/src/core/var.rs2
4 files changed, 155 insertions, 153 deletions
diff --git a/dhall/src/core/context.rs b/dhall/src/core/context.rs
index cc25749..b1fbde9 100644
--- a/dhall/src/core/context.rs
+++ b/dhall/src/core/context.rs
@@ -4,7 +4,7 @@ use std::rc::Rc;
use dhall_syntax::{Label, V};
use crate::core::thunk::Thunk;
-use crate::core::value::Value;
+use crate::core::value::ValueF;
use crate::core::var::{AlphaVar, Shift, Subst};
use crate::error::TypeError;
use crate::phase::{Type, Typed};
@@ -44,7 +44,7 @@ impl TypecheckContext {
let i = i.under_multiple_binders(&shift_map);
let (th, t) = match i {
CtxItem::Kept(newvar, t) => {
- (Value::Var(newvar).into_thunk(), t)
+ (ValueF::Var(newvar).into_thunk(), t)
}
CtxItem::Replaced(th, t) => (th, t),
};
diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs
index 5f96ec8..cf7c097 100644
--- a/dhall/src/core/thunk.rs
+++ b/dhall/src/core/thunk.rs
@@ -5,7 +5,7 @@ use std::rc::Rc;
use dhall_syntax::{Const, ExprF};
use crate::core::context::TypecheckContext;
-use crate::core::value::Value;
+use crate::core::value::ValueF;
use crate::core::var::{AlphaVar, Shift, Subst};
use crate::error::{TypeError, TypeMessage};
use crate::phase::normalize::{apply_any, normalize_one_layer, OutputSubExpr};
@@ -24,12 +24,12 @@ use Marker::{NF, WHNF};
#[derive(Debug)]
enum ThunkInternal {
/// Partially normalized value whose subexpressions have been thunked (this is returned from
- /// typechecking). Note that this is different from `Value::PartialExpr` because there is no
+ /// typechecking). Note that this is different from `ValueF::PartialExpr` because there is no
/// requirement of WHNF here.
PartialExpr(ExprF<Thunk, Normalized>),
/// Partially normalized value.
/// Invariant: if the marker is `NF`, the value must be fully normalized
- Value(Marker, Value),
+ ValueF(Marker, ValueF),
}
/// Stores a possibly unevaluated value. Gets (partially) normalized on-demand,
@@ -61,10 +61,10 @@ impl ThunkInternal {
match self {
ThunkInternal::PartialExpr(e) => {
*self =
- ThunkInternal::Value(WHNF, normalize_one_layer(e.clone()))
+ ThunkInternal::ValueF(WHNF, normalize_one_layer(e.clone()))
}
// Already at least in WHNF
- ThunkInternal::Value(_, _) => {}
+ ThunkInternal::ValueF(_, _) => {}
}
}
@@ -74,37 +74,37 @@ impl ThunkInternal {
self.normalize_whnf();
self.normalize_nf();
}
- ThunkInternal::Value(m @ WHNF, v) => {
+ ThunkInternal::ValueF(m @ WHNF, v) => {
v.normalize_mut();
*m = NF;
}
// Already in NF
- ThunkInternal::Value(NF, _) => {}
+ ThunkInternal::ValueF(NF, _) => {}
}
}
// Always use normalize_whnf before
- fn as_whnf(&self) -> &Value {
+ fn as_whnf(&self) -> &ValueF {
match self {
ThunkInternal::PartialExpr(_) => unreachable!(),
- ThunkInternal::Value(_, v) => v,
+ ThunkInternal::ValueF(_, v) => v,
}
}
// Always use normalize_nf before
- fn as_nf(&self) -> &Value {
+ fn as_nf(&self) -> &ValueF {
match self {
- ThunkInternal::PartialExpr(_) | ThunkInternal::Value(WHNF, _) => {
+ ThunkInternal::PartialExpr(_) | ThunkInternal::ValueF(WHNF, _) => {
unreachable!()
}
- ThunkInternal::Value(NF, v) => v,
+ ThunkInternal::ValueF(NF, v) => v,
}
}
}
impl Thunk {
- pub(crate) fn from_value(v: Value) -> Thunk {
- ThunkInternal::Value(WHNF, v).into_thunk()
+ pub(crate) fn from_valuef(v: ValueF) -> Thunk {
+ ThunkInternal::ValueF(WHNF, v).into_thunk()
}
pub(crate) fn from_partial_expr(e: ExprF<Thunk, Normalized>) -> Thunk {
@@ -130,38 +130,38 @@ impl Thunk {
self.0.borrow_mut().normalize_whnf();
}
// Already at least in WHNF
- ThunkInternal::Value(_, _) => {}
+ ThunkInternal::ValueF(_, _) => {}
}
}
fn do_normalize_nf(&self) {
let borrow = self.0.borrow();
match &*borrow {
- ThunkInternal::PartialExpr(_) | ThunkInternal::Value(WHNF, _) => {
+ ThunkInternal::PartialExpr(_) | ThunkInternal::ValueF(WHNF, _) => {
drop(borrow);
self.0.borrow_mut().normalize_nf();
}
// Already in NF
- ThunkInternal::Value(NF, _) => {}
+ ThunkInternal::ValueF(NF, _) => {}
}
}
// WARNING: avoid normalizing any thunk while holding on to this ref
// or you could run into BorrowMut panics
- pub(crate) fn normalize_nf(&self) -> Ref<Value> {
+ pub(crate) fn normalize_nf(&self) -> Ref<ValueF> {
self.do_normalize_nf();
Ref::map(self.0.borrow(), ThunkInternal::as_nf)
}
// WARNING: avoid normalizing any thunk while holding on to this ref
// or you could run into BorrowMut panics
- pub(crate) fn as_value(&self) -> Ref<Value> {
+ pub(crate) fn as_valuef(&self) -> Ref<ValueF> {
self.do_normalize_whnf();
Ref::map(self.0.borrow(), ThunkInternal::as_whnf)
}
- pub(crate) fn to_value(&self) -> Value {
- self.as_value().clone()
+ pub(crate) fn to_valuef(&self) -> ValueF {
+ self.as_valuef().clone()
}
pub(crate) fn normalize_to_expr_maybe_alpha(
@@ -171,27 +171,27 @@ impl Thunk {
self.normalize_nf().normalize_to_expr_maybe_alpha(alpha)
}
- pub(crate) fn app_val(&self, val: Value) -> Value {
+ pub(crate) fn app_val(&self, val: ValueF) -> ValueF {
self.app_thunk(val.into_thunk())
}
- pub(crate) fn app_thunk(&self, th: Thunk) -> Value {
+ pub(crate) fn app_thunk(&self, th: Thunk) -> ValueF {
apply_any(self.clone(), th)
}
}
impl TypedThunk {
- pub(crate) fn from_value(v: Value) -> TypedThunk {
- TypedThunk::from_thunk_untyped(Thunk::from_value(v))
+ pub(crate) fn from_valuef(v: ValueF) -> TypedThunk {
+ TypedThunk::from_thunk_untyped(Thunk::from_valuef(v))
}
pub(crate) fn from_type(t: Type) -> TypedThunk {
t.into_typethunk()
}
- pub(crate) fn normalize_nf(&self) -> Value {
+ pub(crate) fn normalize_nf(&self) -> ValueF {
match self {
- TypedThunk::Const(c) => Value::Const(*c),
+ TypedThunk::Const(c) => ValueF::Const(*c),
TypedThunk::Untyped(thunk) | TypedThunk::Typed(thunk, _) => {
thunk.normalize_nf().clone()
}
@@ -221,27 +221,29 @@ impl TypedThunk {
pub(crate) fn from_const(c: Const) -> Self {
TypedThunk::Const(c)
}
- pub(crate) fn from_value_and_type(v: Value, t: Type) -> Self {
- TypedThunk::from_thunk_and_type(Thunk::from_value(v), t)
+ pub(crate) fn from_valuef_and_type(v: ValueF, t: Type) -> Self {
+ TypedThunk::from_thunk_and_type(Thunk::from_valuef(v), t)
}
// TODO: Avoid cloning if possible
- pub(crate) fn to_value(&self) -> Value {
+ pub(crate) fn to_valuef(&self) -> ValueF {
match self {
- TypedThunk::Untyped(th) | TypedThunk::Typed(th, _) => th.to_value(),
- TypedThunk::Const(c) => Value::Const(*c),
+ TypedThunk::Untyped(th) | TypedThunk::Typed(th, _) => {
+ th.to_valuef()
+ }
+ TypedThunk::Const(c) => ValueF::Const(*c),
}
}
pub(crate) fn to_expr(&self) -> NormalizedSubExpr {
- self.to_value().normalize_to_expr()
+ self.to_valuef().normalize_to_expr()
}
pub(crate) fn to_expr_alpha(&self) -> NormalizedSubExpr {
- self.to_value().normalize_to_expr_maybe_alpha(true)
+ self.to_valuef().normalize_to_expr_maybe_alpha(true)
}
pub(crate) fn to_thunk(&self) -> Thunk {
match self {
TypedThunk::Untyped(th) | TypedThunk::Typed(th, _) => th.clone(),
- TypedThunk::Const(c) => Thunk::from_value(Value::Const(*c)),
+ TypedThunk::Const(c) => Thunk::from_valuef(ValueF::Const(*c)),
}
}
pub(crate) fn to_type(&self) -> Type {
@@ -252,8 +254,8 @@ impl TypedThunk {
}
pub(crate) fn as_const(&self) -> Option<Const> {
// TODO: avoid clone
- match &self.to_value() {
- Value::Const(c) => Some(*c),
+ match &self.to_valuef() {
+ ValueF::Const(c) => Some(*c),
_ => None,
}
}
@@ -294,8 +296,8 @@ impl Shift for ThunkInternal {
|x, v| Ok(v.shift(delta, &var.under_binder(x))?),
)?,
),
- ThunkInternal::Value(m, v) => {
- ThunkInternal::Value(*m, v.shift(delta, var)?)
+ ThunkInternal::ValueF(m, v) => {
+ ThunkInternal::ValueF(*m, v.shift(delta, var)?)
}
})
}
@@ -336,9 +338,9 @@ impl Subst<Typed> for ThunkInternal {
},
),
),
- ThunkInternal::Value(_, v) => {
+ ThunkInternal::ValueF(_, v) => {
// The resulting value may not stay in normal form after substitution
- ThunkInternal::Value(WHNF, v.subst_shift(var, val))
+ ThunkInternal::ValueF(WHNF, v.subst_shift(var, val))
}
}
}
@@ -361,14 +363,14 @@ impl Subst<Typed> for TypedThunk {
impl std::cmp::PartialEq for Thunk {
fn eq(&self, other: &Self) -> bool {
- *self.as_value() == *other.as_value()
+ *self.as_valuef() == *other.as_valuef()
}
}
impl std::cmp::Eq for Thunk {}
impl std::cmp::PartialEq for TypedThunk {
fn eq(&self, other: &Self) -> bool {
- self.to_value() == other.to_value()
+ self.to_valuef() == other.to_valuef()
}
}
impl std::cmp::Eq for TypedThunk {}
@@ -377,7 +379,7 @@ impl std::fmt::Debug for Thunk {
fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
let b: &ThunkInternal = &self.0.borrow();
match b {
- ThunkInternal::Value(m, v) => {
+ ThunkInternal::ValueF(m, v) => {
f.debug_tuple(&format!("Thunk@{:?}", m)).field(v).finish()
}
ThunkInternal::PartialExpr(e) => {
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),
),
diff --git a/dhall/src/core/var.rs b/dhall/src/core/var.rs
index becd653..296e968 100644
--- a/dhall/src/core/var.rs
+++ b/dhall/src/core/var.rs
@@ -12,7 +12,7 @@ pub struct AlphaVar {
}
// Exactly like a Label, but equality returns always true.
-// This is so that Value equality is exactly alpha-equivalence.
+// This is so that ValueF equality is exactly alpha-equivalence.
#[derive(Clone, Eq)]
pub struct AlphaLabel(Label);
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-06 00:24:48 +0000