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/value.rs | 723 ++++++++++++++++++++++++------------------------ 1 file changed, 362 insertions(+), 361 deletions(-) (limited to 'dhall/src/core/value.rs') diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs index da70118..5c29bf0 100644 --- a/dhall/src/core/value.rs +++ b/dhall/src/core/value.rs @@ -1,405 +1,406 @@ -use std::collections::HashMap; - -use dhall_syntax::{ - rc, Builtin, Const, ExprF, Integer, InterpolatedTextContents, Label, - NaiveDouble, Natural, -}; - -use crate::core::thunk::{Thunk, TypedThunk}; -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 Thunks, which are partially evaluated expressions that are normalized -/// 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 ValueF { - /// Closures - Lam(AlphaLabel, TypedThunk, Thunk), - Pi(AlphaLabel, TypedThunk, TypedThunk), - // 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(TypedThunk), - NEOptionalLit(Thunk), - // EmptyListLit(t) means `[] : List t`, not `[] : t` - EmptyListLit(TypedThunk), - NEListLit(Vec), - RecordLit(HashMap), - RecordType(HashMap), - UnionType(HashMap>), - UnionConstructor(Label, HashMap>), - UnionLit(Label, Thunk, HashMap>), - // Invariant: this must not contain interpolations that are themselves TextLits, and - // contiguous text values must be merged. - TextLit(Vec>), - Equivalence(TypedThunk, TypedThunk), - // Invariant: this must not contain a value captured by one of the variants above. - PartialExpr(ExprF), +use std::borrow::Cow; +use std::cell::{Ref, RefCell, RefMut}; +use std::rc::Rc; + +use dhall_syntax::{Const, ExprF}; + +use crate::core::context::TypecheckContext; +use crate::core::valuef::ValueF; +use crate::core::var::{AlphaVar, Shift, Subst}; +use crate::error::{TypeError, TypeMessage}; +use crate::phase::normalize::{apply_any, normalize_one_layer, OutputSubExpr}; +use crate::phase::typecheck::type_of_const; +use crate::phase::{Normalized, NormalizedSubExpr, Type, Typed}; + +#[derive(Debug, Clone, Copy)] +enum Marker { + /// Weak Head Normal Form, i.e. subexpressions may not be normalized + WHNF, + /// Normal form, i.e. completely normalized + NF, } +use Marker::{NF, WHNF}; -impl ValueF { - pub(crate) fn into_thunk(self) -> Thunk { - Thunk::from_valuef(self) - } +#[derive(Debug, Clone)] +enum ValueInternal { + /// Partially normalized value whose subexpressions have been thunked (this is returned from + /// typechecking). Note that this is different from `ValueF::PartialExpr` because there is no + /// requirement of WHNF here. + PartialExpr(ExprF), + /// Partially normalized value. + /// Invariant: if the marker is `NF`, the value must be fully normalized + ValueF(Marker, ValueF), +} - /// Convert the value to a fully normalized syntactic expression - pub(crate) fn normalize_to_expr(&self) -> OutputSubExpr { - self.normalize_to_expr_maybe_alpha(false) +#[derive(Debug)] +struct TypedValueInternal { + internal: ValueInternal, + typ: Option, +} + +/// Stores a possibly unevaluated value. Gets (partially) normalized on-demand, +/// sharing computation automatically. Uses a RefCell to share computation. +/// Can optionally store a Type from typechecking to preserve type information through +/// normalization. +#[derive(Clone)] +pub struct Value(Rc>); + +#[derive(Debug, Clone)] +pub struct TypedValue(Value); + +impl ValueInternal { + fn into_value(self, t: Option) -> Value { + TypedValueInternal { + internal: self, + typ: t, + } + .into_value() } - /// 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 { + + fn normalize_whnf(&mut self) { 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 + ValueInternal::PartialExpr(e) => { + *self = + ValueInternal::ValueF(WHNF, normalize_one_layer(e.clone())) } - 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))) + // Already at least in WHNF + ValueInternal::ValueF(_, _) => {} + } + } + + fn normalize_nf(&mut self) { + match self { + ValueInternal::PartialExpr(_) => { + self.normalize_whnf(); + self.normalize_nf(); } - 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())) + ValueInternal::ValueF(m @ WHNF, v) => { + v.normalize_mut(); + *m = NF; } - 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(), - )) + // Already in NF + ValueInternal::ValueF(NF, _) => {} + } + } + + // Always use normalize_whnf before + fn as_whnf(&self) -> &ValueF { + match self { + ValueInternal::PartialExpr(_) => unreachable!(), + ValueInternal::ValueF(_, v) => v, + } + } + + // Always use normalize_nf before + fn as_nf(&self) -> &ValueF { + match self { + ValueInternal::PartialExpr(_) | ValueInternal::ValueF(WHNF, _) => { + unreachable!() } - 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), + ValueInternal::ValueF(NF, v) => v, + } + } +} + +impl TypedValueInternal { + fn into_value(self) -> Value { + Value(Rc::new(RefCell::new(self))) + } + fn as_internal(&self) -> &ValueInternal { + &self.internal + } + fn as_internal_mut(&mut self) -> &mut ValueInternal { + &mut self.internal + } + + fn get_type(&self) -> Result { + match &self.typ { + Some(t) => Ok(t.clone()), + None => Err(TypeError::new( + &TypecheckContext::new(), + TypeMessage::Untyped, )), - ValueF::PartialExpr(e) => { - rc(e.map_ref(|v| v.normalize_to_expr_maybe_alpha(alpha))) - } } } +} +impl Value { + pub(crate) fn from_valuef(v: ValueF) -> Value { + ValueInternal::ValueF(WHNF, v).into_value(None) + } + pub(crate) fn from_valuef_and_type(v: ValueF, t: Type) -> Value { + ValueInternal::ValueF(WHNF, v).into_value(Some(t)) + } + pub(crate) fn from_partial_expr(e: ExprF) -> Value { + ValueInternal::PartialExpr(e).into_value(None) + } + pub(crate) fn with_type(self, t: Type) -> Value { + self.as_internal().clone().into_value(Some(t)) + } + + /// Mutates the contents. If no one else shares this thunk, + /// mutates directly, thus avoiding a RefCell lock. + fn mutate_internal(&mut self, f: impl FnOnce(&mut TypedValueInternal)) { + match Rc::get_mut(&mut self.0) { + // Mutate directly if sole owner + Some(refcell) => f(RefCell::get_mut(refcell)), + // Otherwise mutate through the refcell + None => f(&mut self.as_tinternal_mut()), + } + } + + /// Normalizes contents to normal form; faster than `normalize_nf` if + /// no one else shares this thunk 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(); - } + self.mutate_internal(|i| i.as_internal_mut().normalize_nf()) + } - 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(); - }); - } + fn as_tinternal(&self) -> Ref { + self.0.borrow() + } + fn as_tinternal_mut(&mut self) -> RefMut { + self.0.borrow_mut() + } + fn as_internal(&self) -> Ref { + Ref::map(self.as_tinternal(), TypedValueInternal::as_internal) + } + fn as_internal_mut(&self) -> RefMut { + RefMut::map(self.0.borrow_mut(), TypedValueInternal::as_internal_mut) + } + + fn do_normalize_whnf(&self) { + let borrow = self.as_internal(); + match &*borrow { + ValueInternal::PartialExpr(_) => { + drop(borrow); + self.as_internal_mut().normalize_whnf(); + } + // Already at least in WHNF + ValueInternal::ValueF(_, _) => {} } } - /// Apply to a value - pub(crate) fn app(self, val: ValueF) -> ValueF { - self.app_val(val) + fn do_normalize_nf(&self) { + let borrow = self.as_internal(); + match &*borrow { + ValueInternal::PartialExpr(_) | ValueInternal::ValueF(WHNF, _) => { + drop(borrow); + self.as_internal_mut().normalize_nf(); + } + // Already in NF + ValueInternal::ValueF(NF, _) => {} + } } - /// Apply to a value - pub(crate) fn app_val(self, val: ValueF) -> ValueF { - self.app_thunk(val.into_thunk()) + // 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 { + self.do_normalize_nf(); + Ref::map(self.as_internal(), ValueInternal::as_nf) } - /// Apply to a thunk - pub fn app_thunk(self, th: Thunk) -> ValueF { - Thunk::from_valuef(self).app_thunk(th) + // WARNING: avoid normalizing any thunk while holding on to this ref + // or you could run into BorrowMut panics + pub(crate) fn as_valuef(&self) -> Ref { + self.do_normalize_whnf(); + Ref::map(self.as_internal(), ValueInternal::as_whnf) } - pub fn from_builtin(b: Builtin) -> ValueF { - ValueF::AppliedBuiltin(b, vec![]) + pub(crate) fn to_valuef(&self) -> ValueF { + self.as_valuef().clone() + } + + pub(crate) fn normalize_to_expr_maybe_alpha( + &self, + alpha: bool, + ) -> OutputSubExpr { + self.normalize_nf().normalize_to_expr_maybe_alpha(alpha) + } + + pub(crate) fn app_valuef(&self, val: ValueF) -> ValueF { + self.app_value(val.into_value()) + } + + pub(crate) fn app_value(&self, th: Value) -> ValueF { + apply_any(self.clone(), th) + } + + pub(crate) fn get_type(&self) -> Result, TypeError> { + Ok(Cow::Owned(self.as_tinternal().get_type()?)) } } -impl Shift for ValueF { +impl TypedValue { + pub(crate) fn from_valuef(v: ValueF) -> TypedValue { + TypedValue::from_value_untyped(Value::from_valuef(v)) + } + + pub(crate) fn from_type(t: Type) -> TypedValue { + t.into_typedvalue() + } + + pub(crate) fn normalize_nf(&self) -> ValueF { + self.0.normalize_nf().clone() + } + + pub(crate) fn to_typed(&self) -> Typed { + self.clone().into_typed() + } + + pub(crate) fn normalize_to_expr_maybe_alpha( + &self, + alpha: bool, + ) -> OutputSubExpr { + self.normalize_nf().normalize_to_expr_maybe_alpha(alpha) + } + + pub(crate) fn from_value_and_type(th: Value, t: Type) -> Self { + TypedValue(th.with_type(t)) + } + pub fn from_value_simple_type(th: Value) -> Self { + TypedValue::from_value_and_type(th, Type::const_type()) + } + pub(crate) fn from_value_untyped(th: Value) -> Self { + TypedValue(th) + } + pub(crate) fn from_const(c: Const) -> Self { + match type_of_const(c) { + Ok(t) => TypedValue::from_valuef_and_type(ValueF::Const(c), t), + Err(_) => TypedValue::from_valuef(ValueF::Const(c)), + } + } + pub(crate) fn from_valuef_and_type(v: ValueF, t: Type) -> Self { + TypedValue(Value::from_valuef_and_type(v, t)) + } + + pub(crate) fn to_valuef(&self) -> ValueF { + self.0.to_valuef() + } + pub(crate) fn to_expr(&self) -> NormalizedSubExpr { + self.to_valuef().normalize_to_expr() + } + pub(crate) fn to_expr_alpha(&self) -> NormalizedSubExpr { + self.to_valuef().normalize_to_expr_maybe_alpha(true) + } + pub(crate) fn to_value(&self) -> Value { + self.0.clone() + } + pub(crate) fn to_type(&self) -> Type { + self.clone().into_typed().into_type() + } + pub(crate) fn into_typed(self) -> Typed { + Typed::from_typedvalue(self) + } + pub(crate) fn as_const(&self) -> Option { + // TODO: avoid clone + match &self.to_valuef() { + ValueF::Const(c) => Some(*c), + _ => None, + } + } + + pub(crate) fn normalize_mut(&mut self) { + self.0.normalize_mut() + } + + pub(crate) fn get_type(&self) -> Result, TypeError> { + self.0.get_type() + } +} + +impl Shift for Value { + fn shift(&self, delta: isize, var: &AlphaVar) -> Option { + Some(Value(self.0.shift(delta, var)?)) + } +} + +impl Shift for ValueInternal { 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)?) + ValueInternal::PartialExpr(e) => { + ValueInternal::PartialExpr(e.shift(delta, var)?) } - ValueF::EmptyListLit(tth) => { - ValueF::EmptyListLit(tth.shift(delta, var)?) + ValueInternal::ValueF(m, v) => { + ValueInternal::ValueF(*m, v.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 { +impl Shift for TypedValue { + fn shift(&self, delta: isize, var: &AlphaVar) -> Option { + Some(TypedValue(self.0.shift(delta, var)?)) + } +} + +impl Shift for TypedValueInternal { + fn shift(&self, delta: isize, var: &AlphaVar) -> Option { + Some(TypedValueInternal { + internal: self.internal.shift(delta, var)?, + typ: self.typ.shift(delta, var)?, + }) + } +} + +impl Subst for Value { + fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { + Value(self.0.subst_shift(var, val)) + } +} + +impl Subst for ValueInternal { 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)) + ValueInternal::PartialExpr(e) => { + ValueInternal::PartialExpr(e.subst_shift(var, val)) } - ValueF::NEListLit(elts) => { - ValueF::NEListLit(elts.subst_shift(var, val)) + ValueInternal::ValueF(_, v) => { + // The resulting value may not stay in normal form after substitution + ValueInternal::ValueF(WHNF, v.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)) + } + } +} + +impl Subst for TypedValueInternal { + fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { + TypedValueInternal { + internal: self.internal.subst_shift(var, val), + typ: self.typ.subst_shift(var, val), + } + } +} + +impl Subst for TypedValue { + fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { + TypedValue(self.0.subst_shift(var, val)) + } +} + +impl std::cmp::PartialEq for Value { + fn eq(&self, other: &Self) -> bool { + *self.as_valuef() == *other.as_valuef() + } +} +impl std::cmp::Eq for Value {} + +impl std::cmp::PartialEq for TypedValue { + fn eq(&self, other: &Self) -> bool { + self.to_valuef() == other.to_valuef() + } +} +impl std::cmp::Eq for TypedValue {} + +impl std::fmt::Debug for Value { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + let b: &ValueInternal = &self.as_internal(); + match b { + ValueInternal::ValueF(m, v) => { + f.debug_tuple(&format!("Value@{:?}", m)).field(v).finish() } - ValueF::UnionConstructor(x, kts) => { - ValueF::UnionConstructor(x.clone(), kts.subst_shift(var, val)) + ValueInternal::PartialExpr(e) => { + f.debug_tuple("Value@PartialExpr").field(e).finish() } - 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