diff options
Diffstat (limited to 'dhall/src/core')
-rw-r--r-- | dhall/src/core/context.rs | 4 | ||||
-rw-r--r-- | dhall/src/core/thunk.rs | 90 | ||||
-rw-r--r-- | dhall/src/core/value.rs | 212 | ||||
-rw-r--r-- | dhall/src/core/var.rs | 2 |
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); |