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.rs723
1 files changed, 362 insertions, 361 deletions
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<Thunk>),
-
- 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<Thunk>),
- RecordLit(HashMap<Label, Thunk>),
- RecordType(HashMap<Label, TypedThunk>),
- UnionType(HashMap<Label, Option<TypedThunk>>),
- UnionConstructor(Label, HashMap<Label, Option<TypedThunk>>),
- UnionLit(Label, Thunk, HashMap<Label, Option<TypedThunk>>),
- // Invariant: this must not contain interpolations that are themselves TextLits, and
- // contiguous text values must be merged.
- TextLit(Vec<InterpolatedTextContents<Thunk>>),
- Equivalence(TypedThunk, TypedThunk),
- // Invariant: this must not contain a value captured by one of the variants above.
- PartialExpr(ExprF<Thunk, Normalized>),
+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<Value, Normalized>),
+ /// 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<Type>,
+}
+
+/// 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<RefCell<TypedValueInternal>>);
+
+#[derive(Debug, Clone)]
+pub struct TypedValue(Value);
+
+impl ValueInternal {
+ fn into_value(self, t: Option<Type>) -> 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<Type, TypeError> {
+ 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, Normalized>) -> 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<TypedValueInternal> {
+ self.0.borrow()
+ }
+ fn as_tinternal_mut(&mut self) -> RefMut<TypedValueInternal> {
+ self.0.borrow_mut()
+ }
+ fn as_internal(&self) -> Ref<ValueInternal> {
+ Ref::map(self.as_tinternal(), TypedValueInternal::as_internal)
+ }
+ fn as_internal_mut(&self) -> RefMut<ValueInternal> {
+ 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<ValueF> {
+ 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<ValueF> {
+ 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<Cow<'_, Type>, 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<Const> {
+ // 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<Cow<'_, Type>, TypeError> {
+ self.0.get_type()
+ }
+}
+
+impl Shift for Value {
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+ Some(Value(self.0.shift(delta, var)?))
+ }
+}
+
+impl Shift for ValueInternal {
fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
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<Typed> for ValueF {
+impl Shift for TypedValue {
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+ Some(TypedValue(self.0.shift(delta, var)?))
+ }
+}
+
+impl Shift for TypedValueInternal {
+ fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
+ Some(TypedValueInternal {
+ internal: self.internal.shift(delta, var)?,
+ typ: self.typ.shift(delta, var)?,
+ })
+ }
+}
+
+impl Subst<Typed> for Value {
+ fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
+ Value(self.0.subst_shift(var, val))
+ }
+}
+
+impl Subst<Typed> 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<Typed> 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<Typed> 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),
- ),
}
}
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-03 13:49:22 +0000