From 30bbf22fbfaead80322888eba7b7acdf908c3f3e Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 17 Dec 2019 15:00:44 +0000 Subject: Rename ValueF to ValueKind --- dhall/src/semantics/core/context.rs | 4 +- dhall/src/semantics/core/mod.rs | 2 +- dhall/src/semantics/core/value.rs | 70 +++---- dhall/src/semantics/core/value_kind.rs | 333 +++++++++++++++++++++++++++++++++ dhall/src/semantics/core/valuef.rs | 323 -------------------------------- dhall/src/semantics/core/var.rs | 2 +- 6 files changed, 372 insertions(+), 362 deletions(-) create mode 100644 dhall/src/semantics/core/value_kind.rs delete mode 100644 dhall/src/semantics/core/valuef.rs (limited to 'dhall/src/semantics/core') diff --git a/dhall/src/semantics/core/context.rs b/dhall/src/semantics/core/context.rs index d150e56..8861378 100644 --- a/dhall/src/semantics/core/context.rs +++ b/dhall/src/semantics/core/context.rs @@ -2,7 +2,7 @@ use std::collections::HashMap; use std::rc::Rc; use crate::semantics::core::value::Value; -use crate::semantics::core::valuef::ValueF; +use crate::semantics::core::value_kind::ValueKind; use crate::semantics::core::var::{AlphaVar, Shift, Subst}; use crate::semantics::error::TypeError; use crate::syntax::{Label, V}; @@ -39,7 +39,7 @@ impl TypecheckContext { let i = i.under_multiple_binders(&shift_map); return Some(match i { CtxItem::Kept(newvar, t) => { - Value::from_valuef_and_type(ValueF::Var(newvar), t) + Value::from_kind_and_type(ValueKind::Var(newvar), t) } CtxItem::Replaced(v) => v, }); diff --git a/dhall/src/semantics/core/mod.rs b/dhall/src/semantics/core/mod.rs index 08213f7..bf3d390 100644 --- a/dhall/src/semantics/core/mod.rs +++ b/dhall/src/semantics/core/mod.rs @@ -1,4 +1,4 @@ pub mod context; pub mod value; -pub mod valuef; +pub mod value_kind; pub mod var; diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index 6e6739f..7403742 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -2,7 +2,7 @@ use std::cell::{Ref, RefCell, RefMut}; use std::rc::Rc; use crate::semantics::core::context::TypecheckContext; -use crate::semantics::core::valuef::ValueF; +use crate::semantics::core::value_kind::ValueKind; use crate::semantics::core::var::{AlphaVar, Shift, Subst}; use crate::semantics::error::{TypeError, TypeMessage}; use crate::semantics::phase::normalize::{apply_any, normalize_whnf}; @@ -15,12 +15,12 @@ pub(crate) enum Form { /// No constraints; expression may not be normalized at all. Unevaled, /// Weak Head Normal Form, i.e. normalized up to the first constructor, but subexpressions may - /// not be normalized. This means that the first constructor of the contained ValueF is the first + /// not be normalized. This means that the first constructor of the contained ValueKind is the first /// constructor of the final Normal Form (NF). WHNF, /// Normal Form, i.e. completely normalized. - /// When all the Values 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 + /// When all the Values in a ValueKind are at least in WHNF, and recursively so, then the + /// ValueKind 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. NF, } @@ -32,7 +32,7 @@ use Form::{Unevaled, NF, WHNF}; #[derive(Debug)] struct ValueInternal { form: Form, - value: ValueF, + kind: ValueKind, /// This is None if and only if `value` is `Sort` (which doesn't have a type) ty: Option, span: Span, @@ -57,8 +57,8 @@ impl ValueInternal { fn into_value(self) -> Value { Value(Rc::new(RefCell::new(self))) } - fn as_valuef(&self) -> &ValueF { - &self.value + fn as_kind(&self) -> &ValueKind { + &self.kind } fn normalize_whnf(&mut self) { @@ -67,21 +67,21 @@ impl ValueInternal { // Dummy value in case the other closure panics || ValueInternal { form: Unevaled, - value: ValueF::Const(Const::Type), + kind: ValueKind::Const(Const::Type), ty: None, span: Span::Artificial, }, |vint| match (&vint.form, &vint.ty) { (Unevaled, Some(ty)) => ValueInternal { form: WHNF, - value: normalize_whnf(vint.value, &ty), + kind: normalize_whnf(vint.kind, &ty), ty: vint.ty, span: vint.span, }, // `value` is `Sort` (Unevaled, None) => ValueInternal { form: NF, - value: ValueF::Const(Const::Sort), + kind: ValueKind::Const(Const::Sort), ty: None, span: vint.span, }, @@ -97,7 +97,7 @@ impl ValueInternal { self.normalize_nf(); } WHNF => { - self.value.normalize_mut(); + self.kind.normalize_mut(); self.form = NF; } // Already in NF @@ -116,10 +116,10 @@ impl ValueInternal { } impl Value { - fn new(value: ValueF, form: Form, ty: Value, span: Span) -> Value { + fn new(kind: ValueKind, form: Form, ty: Value, span: Span) -> Value { ValueInternal { form, - value, + kind, ty: Some(ty), span, } @@ -128,23 +128,23 @@ impl Value { pub(crate) fn const_sort() -> Value { ValueInternal { form: NF, - value: ValueF::Const(Const::Sort), + kind: ValueKind::Const(Const::Sort), ty: None, span: Span::Artificial, } .into_value() } - pub(crate) fn from_valuef_and_type(v: ValueF, t: Value) -> Value { + pub(crate) fn from_kind_and_type(v: ValueKind, t: Value) -> Value { Value::new(v, Unevaled, t, Span::Artificial) } - pub(crate) fn from_valuef_and_type_and_span( - v: ValueF, + pub(crate) fn from_kind_and_type_and_span( + v: ValueKind, t: Value, span: Span, ) -> Value { Value::new(v, Unevaled, t, span) } - pub(crate) fn from_valuef_and_type_whnf(v: ValueF, t: Value) -> Value { + pub(crate) fn from_kind_and_type_whnf(v: ValueKind, t: Value) -> Value { Value::new(v, WHNF, t, Span::Artificial) } pub(crate) fn from_const(c: Const) -> Self { @@ -160,7 +160,7 @@ impl Value { pub(crate) fn as_const(&self) -> Option { match &*self.as_whnf() { - ValueF::Const(c) => Some(*c), + ValueKind::Const(c) => Some(*c), _ => None, } } @@ -174,30 +174,30 @@ impl Value { fn as_internal_mut(&self) -> RefMut { self.0.borrow_mut() } - /// WARNING: The returned ValueF may be entirely unnormalized, in aprticular it may just be an + /// WARNING: The returned ValueKind may be entirely unnormalized, in aprticular it may just be an /// unevaled PartialExpr. You probably want to use `as_whnf`. - fn as_valuef(&self) -> Ref { - Ref::map(self.as_internal(), ValueInternal::as_valuef) + fn as_kind(&self) -> Ref { + Ref::map(self.as_internal(), ValueInternal::as_kind) } /// This is what you want if you want to pattern-match on the value. /// WARNING: drop this ref before normalizing the same value or you will run into BorrowMut /// panics. - pub(crate) fn as_whnf(&self) -> Ref { + pub(crate) fn as_whnf(&self) -> Ref { self.normalize_whnf(); - self.as_valuef() + self.as_kind() } pub(crate) fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr { if opts.normalize { self.normalize_whnf(); } - self.as_valuef().to_expr(opts) + self.as_kind().to_expr(opts) } - pub(crate) fn to_whnf_ignore_type(&self) -> ValueF { + pub(crate) fn to_whnf_ignore_type(&self) -> ValueKind { self.as_whnf().clone() } /// Before discarding type information, check that it matches the expected return type. - pub(crate) fn to_whnf_check_type(&self, ty: &Value) -> ValueF { + pub(crate) fn to_whnf_check_type(&self, ty: &Value) -> ValueKind { self.check_type(ty); self.to_whnf_ignore_type() } @@ -234,13 +234,13 @@ impl Value { pub(crate) fn app(&self, v: Value) -> Value { let body_t = match &*self.get_type_not_sort().as_whnf() { - ValueF::Pi(x, t, e) => { + ValueKind::Pi(x, t, e) => { v.check_type(t); e.subst_shift(&x.into(), &v) } _ => unreachable!("Internal type error"), }; - Value::from_valuef_and_type_whnf( + Value::from_kind_and_type_whnf( apply_any(self.clone(), v, &body_t), body_t, ) @@ -275,7 +275,7 @@ impl Shift for ValueInternal { fn shift(&self, delta: isize, var: &AlphaVar) -> Option { Some(ValueInternal { form: self.form, - value: self.value.shift(delta, var)?, + kind: self.kind.shift(delta, var)?, ty: self.ty.shift(delta, var)?, span: self.span.clone(), }) @@ -284,10 +284,10 @@ impl Shift for ValueInternal { impl Subst for Value { fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { - match &*self.as_valuef() { + match &*self.as_kind() { // If the var matches, we can just reuse the provided value instead of copying it. // We also check that the types match, if in debug mode. - ValueF::Var(v) if v == var => { + ValueKind::Var(v) if v == var => { if let Ok(self_ty) = self.get_type() { val.check_type(&self_ty.subst_shift(var, val)); } @@ -303,7 +303,7 @@ impl Subst for ValueInternal { ValueInternal { // The resulting value may not stay in wnhf after substitution form: Unevaled, - value: self.value.subst_shift(var, val), + kind: self.kind.subst_shift(var, val), ty: self.ty.subst_shift(var, val), span: self.span.clone(), } @@ -321,11 +321,11 @@ impl std::cmp::Eq for Value {} impl std::fmt::Debug for Value { fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { let vint: &ValueInternal = &self.as_internal(); - if let ValueF::Const(c) = &vint.value { + if let ValueKind::Const(c) = &vint.kind { write!(fmt, "{:?}", c) } else { let mut x = fmt.debug_struct(&format!("Value@{:?}", &vint.form)); - x.field("value", &vint.value); + x.field("value", &vint.kind); if let Some(ty) = vint.ty.as_ref() { x.field("type", &ty); } else { diff --git a/dhall/src/semantics/core/value_kind.rs b/dhall/src/semantics/core/value_kind.rs new file mode 100644 index 0000000..36ba068 --- /dev/null +++ b/dhall/src/semantics/core/value_kind.rs @@ -0,0 +1,333 @@ +use std::collections::HashMap; + +use crate::semantics::core::value::{ToExprOptions, Value}; +use crate::semantics::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; +use crate::semantics::phase::typecheck::rc; +use crate::semantics::phase::{Normalized, NormalizedExpr}; +use crate::syntax; +use crate::syntax::{ + Builtin, Const, ExprF, Integer, InterpolatedTextContents, Label, + NaiveDouble, Natural, +}; + +/// A semantic value. Subexpressions are Values, which are partially evaluated expressions that are +/// normalized on-demand. +/// If you compare for equality two `ValueKind`s in WHNF, then equality will be up to +/// alpha-equivalence (renaming of bound variables) and beta-equivalence (normalization). It will +/// recursively normalize as needed. +#[derive(Debug, Clone, PartialEq, Eq)] +pub(crate) enum ValueKind { + /// Closures + Lam(AlphaLabel, Value, Value), + Pi(AlphaLabel, Value, Value), + // Invariant: in whnf, 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(Value), + NEOptionalLit(Value), + // EmptyListLit(t) means `[] : List t`, not `[] : t` + EmptyListLit(Value), + NEListLit(Vec), + RecordType(HashMap), + RecordLit(HashMap), + UnionType(HashMap>), + UnionConstructor(Label, HashMap>), + UnionLit(Label, Value, HashMap>), + // Invariant: in whnf, this must not contain interpolations that are themselves TextLits, and + // contiguous text values must be merged. + TextLit(Vec>), + Equivalence(Value, Value), + // Invariant: in whnf, this must not contain a value captured by one of the variants above. + PartialExpr(ExprF), +} + +impl ValueKind { + pub(crate) fn into_value_with_type(self, t: Value) -> Value { + Value::from_kind_and_type(self, t) + } + + pub(crate) fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr { + match self { + ValueKind::Lam(x, t, e) => rc(ExprF::Lam( + x.to_label_maybe_alpha(opts.alpha), + t.to_expr(opts), + e.to_expr(opts), + )), + ValueKind::AppliedBuiltin(b, args) => args + .iter() + .map(|v| v.to_expr(opts)) + .fold(rc(ExprF::Builtin(*b)), |acc, v| rc(ExprF::App(acc, v))), + ValueKind::Pi(x, t, e) => rc(ExprF::Pi( + x.to_label_maybe_alpha(opts.alpha), + t.to_expr(opts), + e.to_expr(opts), + )), + ValueKind::Var(v) => rc(ExprF::Var(v.to_var(opts.alpha))), + ValueKind::Const(c) => rc(ExprF::Const(*c)), + ValueKind::BoolLit(b) => rc(ExprF::BoolLit(*b)), + ValueKind::NaturalLit(n) => rc(ExprF::NaturalLit(*n)), + ValueKind::IntegerLit(n) => rc(ExprF::IntegerLit(*n)), + ValueKind::DoubleLit(n) => rc(ExprF::DoubleLit(*n)), + ValueKind::EmptyOptionalLit(n) => rc(ExprF::App( + rc(ExprF::Builtin(Builtin::OptionalNone)), + n.to_expr(opts), + )), + ValueKind::NEOptionalLit(n) => rc(ExprF::SomeLit(n.to_expr(opts))), + ValueKind::EmptyListLit(n) => rc(ExprF::EmptyListLit(rc( + ExprF::App(rc(ExprF::Builtin(Builtin::List)), n.to_expr(opts)), + ))), + ValueKind::NEListLit(elts) => rc(ExprF::NEListLit( + elts.iter().map(|n| n.to_expr(opts)).collect(), + )), + ValueKind::RecordLit(kvs) => rc(ExprF::RecordLit( + kvs.iter() + .map(|(k, v)| (k.clone(), v.to_expr(opts))) + .collect(), + )), + ValueKind::RecordType(kts) => rc(ExprF::RecordType( + kts.iter() + .map(|(k, v)| (k.clone(), v.to_expr(opts))) + .collect(), + )), + ValueKind::UnionType(kts) => rc(ExprF::UnionType( + kts.iter() + .map(|(k, v)| { + (k.clone(), v.as_ref().map(|v| v.to_expr(opts))) + }) + .collect(), + )), + ValueKind::UnionConstructor(l, kts) => rc(ExprF::Field( + ValueKind::UnionType(kts.clone()).to_expr(opts), + l.clone(), + )), + ValueKind::UnionLit(l, v, kts) => rc(ExprF::App( + ValueKind::UnionConstructor(l.clone(), kts.clone()) + .to_expr(opts), + v.to_expr(opts), + )), + ValueKind::TextLit(elts) => rc(ExprF::TextLit( + elts.iter() + .map(|contents| contents.map_ref(|e| e.to_expr(opts))) + .collect(), + )), + ValueKind::Equivalence(x, y) => rc(ExprF::BinOp( + syntax::BinOp::Equivalence, + x.to_expr(opts), + y.to_expr(opts), + )), + ValueKind::PartialExpr(e) => rc(e.map_ref(|v| v.to_expr(opts))), + } + } + + pub(crate) fn normalize_mut(&mut self) { + match self { + ValueKind::Var(_) + | ValueKind::Const(_) + | ValueKind::BoolLit(_) + | ValueKind::NaturalLit(_) + | ValueKind::IntegerLit(_) + | ValueKind::DoubleLit(_) => {} + + ValueKind::EmptyOptionalLit(tth) | ValueKind::EmptyListLit(tth) => { + tth.normalize_mut(); + } + + ValueKind::NEOptionalLit(th) => { + th.normalize_mut(); + } + ValueKind::Lam(_, t, e) => { + t.normalize_mut(); + e.normalize_mut(); + } + ValueKind::Pi(_, t, e) => { + t.normalize_mut(); + e.normalize_mut(); + } + ValueKind::AppliedBuiltin(_, args) => { + for x in args.iter_mut() { + x.normalize_mut(); + } + } + ValueKind::NEListLit(elts) => { + for x in elts.iter_mut() { + x.normalize_mut(); + } + } + ValueKind::RecordLit(kvs) => { + for x in kvs.values_mut() { + x.normalize_mut(); + } + } + ValueKind::RecordType(kvs) => { + for x in kvs.values_mut() { + x.normalize_mut(); + } + } + ValueKind::UnionType(kts) | ValueKind::UnionConstructor(_, kts) => { + for x in kts.values_mut().flat_map(|opt| opt) { + x.normalize_mut(); + } + } + ValueKind::UnionLit(_, v, kts) => { + v.normalize_mut(); + for x in kts.values_mut().flat_map(|opt| opt) { + x.normalize_mut(); + } + } + ValueKind::TextLit(elts) => { + for x in elts.iter_mut() { + x.map_mut(Value::normalize_mut); + } + } + ValueKind::Equivalence(x, y) => { + x.normalize_mut(); + y.normalize_mut(); + } + ValueKind::PartialExpr(e) => { + e.map_mut(Value::normalize_mut); + } + } + } + + pub(crate) fn from_builtin(b: Builtin) -> ValueKind { + ValueKind::AppliedBuiltin(b, vec![]) + } +} + +impl Shift for ValueKind { + fn shift(&self, delta: isize, var: &AlphaVar) -> Option { + Some(match self { + ValueKind::Lam(x, t, e) => ValueKind::Lam( + x.clone(), + t.shift(delta, var)?, + e.shift(delta, &var.under_binder(x))?, + ), + ValueKind::AppliedBuiltin(b, args) => { + ValueKind::AppliedBuiltin(*b, args.shift(delta, var)?) + } + ValueKind::Pi(x, t, e) => ValueKind::Pi( + x.clone(), + t.shift(delta, var)?, + e.shift(delta, &var.under_binder(x))?, + ), + ValueKind::Var(v) => ValueKind::Var(v.shift(delta, var)?), + ValueKind::Const(c) => ValueKind::Const(*c), + ValueKind::BoolLit(b) => ValueKind::BoolLit(*b), + ValueKind::NaturalLit(n) => ValueKind::NaturalLit(*n), + ValueKind::IntegerLit(n) => ValueKind::IntegerLit(*n), + ValueKind::DoubleLit(n) => ValueKind::DoubleLit(*n), + ValueKind::EmptyOptionalLit(tth) => { + ValueKind::EmptyOptionalLit(tth.shift(delta, var)?) + } + ValueKind::NEOptionalLit(th) => { + ValueKind::NEOptionalLit(th.shift(delta, var)?) + } + ValueKind::EmptyListLit(tth) => { + ValueKind::EmptyListLit(tth.shift(delta, var)?) + } + ValueKind::NEListLit(elts) => { + ValueKind::NEListLit(elts.shift(delta, var)?) + } + ValueKind::RecordLit(kvs) => { + ValueKind::RecordLit(kvs.shift(delta, var)?) + } + ValueKind::RecordType(kvs) => { + ValueKind::RecordType(kvs.shift(delta, var)?) + } + ValueKind::UnionType(kts) => { + ValueKind::UnionType(kts.shift(delta, var)?) + } + ValueKind::UnionConstructor(x, kts) => { + ValueKind::UnionConstructor(x.clone(), kts.shift(delta, var)?) + } + ValueKind::UnionLit(x, v, kts) => ValueKind::UnionLit( + x.clone(), + v.shift(delta, var)?, + kts.shift(delta, var)?, + ), + ValueKind::TextLit(elts) => { + ValueKind::TextLit(elts.shift(delta, var)?) + } + ValueKind::Equivalence(x, y) => ValueKind::Equivalence( + x.shift(delta, var)?, + y.shift(delta, var)?, + ), + ValueKind::PartialExpr(e) => { + ValueKind::PartialExpr(e.shift(delta, var)?) + } + }) + } +} + +impl Subst for ValueKind { + fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { + match self { + ValueKind::AppliedBuiltin(b, args) => { + ValueKind::AppliedBuiltin(*b, args.subst_shift(var, val)) + } + ValueKind::PartialExpr(e) => { + ValueKind::PartialExpr(e.subst_shift(var, val)) + } + ValueKind::TextLit(elts) => { + ValueKind::TextLit(elts.subst_shift(var, val)) + } + ValueKind::Lam(x, t, e) => ValueKind::Lam( + x.clone(), + t.subst_shift(var, val), + e.subst_shift(&var.under_binder(x), &val.under_binder(x)), + ), + ValueKind::Pi(x, t, e) => ValueKind::Pi( + x.clone(), + t.subst_shift(var, val), + e.subst_shift(&var.under_binder(x), &val.under_binder(x)), + ), + ValueKind::Var(v) if v == var => val.to_whnf_ignore_type(), + ValueKind::Var(v) => ValueKind::Var(v.shift(-1, var).unwrap()), + ValueKind::Const(c) => ValueKind::Const(*c), + ValueKind::BoolLit(b) => ValueKind::BoolLit(*b), + ValueKind::NaturalLit(n) => ValueKind::NaturalLit(*n), + ValueKind::IntegerLit(n) => ValueKind::IntegerLit(*n), + ValueKind::DoubleLit(n) => ValueKind::DoubleLit(*n), + ValueKind::EmptyOptionalLit(tth) => { + ValueKind::EmptyOptionalLit(tth.subst_shift(var, val)) + } + ValueKind::NEOptionalLit(th) => { + ValueKind::NEOptionalLit(th.subst_shift(var, val)) + } + ValueKind::EmptyListLit(tth) => { + ValueKind::EmptyListLit(tth.subst_shift(var, val)) + } + ValueKind::NEListLit(elts) => { + ValueKind::NEListLit(elts.subst_shift(var, val)) + } + ValueKind::RecordLit(kvs) => { + ValueKind::RecordLit(kvs.subst_shift(var, val)) + } + ValueKind::RecordType(kvs) => { + ValueKind::RecordType(kvs.subst_shift(var, val)) + } + ValueKind::UnionType(kts) => { + ValueKind::UnionType(kts.subst_shift(var, val)) + } + ValueKind::UnionConstructor(x, kts) => ValueKind::UnionConstructor( + x.clone(), + kts.subst_shift(var, val), + ), + ValueKind::UnionLit(x, v, kts) => ValueKind::UnionLit( + x.clone(), + v.subst_shift(var, val), + kts.subst_shift(var, val), + ), + ValueKind::Equivalence(x, y) => ValueKind::Equivalence( + x.subst_shift(var, val), + y.subst_shift(var, val), + ), + } + } +} diff --git a/dhall/src/semantics/core/valuef.rs b/dhall/src/semantics/core/valuef.rs deleted file mode 100644 index 73c715a..0000000 --- a/dhall/src/semantics/core/valuef.rs +++ /dev/null @@ -1,323 +0,0 @@ -use std::collections::HashMap; - -use crate::semantics::core::value::{ToExprOptions, Value}; -use crate::semantics::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; -use crate::semantics::phase::typecheck::rc; -use crate::semantics::phase::{Normalized, NormalizedExpr}; -use crate::syntax; -use crate::syntax::{ - Builtin, Const, ExprF, Integer, InterpolatedTextContents, Label, - NaiveDouble, Natural, -}; - -/// A semantic value. Subexpressions are Values, which are partially evaluated expressions that are -/// normalized on-demand. -/// If you compare for equality two `ValueF`s in WHNF, then equality will be up to -/// alpha-equivalence (renaming of bound variables) and beta-equivalence (normalization). It will -/// recursively normalize as needed. -#[derive(Debug, Clone, PartialEq, Eq)] -pub(crate) enum ValueF { - /// Closures - Lam(AlphaLabel, Value, Value), - Pi(AlphaLabel, Value, Value), - // Invariant: in whnf, 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(Value), - NEOptionalLit(Value), - // EmptyListLit(t) means `[] : List t`, not `[] : t` - EmptyListLit(Value), - NEListLit(Vec), - RecordType(HashMap), - RecordLit(HashMap), - UnionType(HashMap>), - UnionConstructor(Label, HashMap>), - UnionLit(Label, Value, HashMap>), - // Invariant: in whnf, this must not contain interpolations that are themselves TextLits, and - // contiguous text values must be merged. - TextLit(Vec>), - Equivalence(Value, Value), - // Invariant: in whnf, this must not contain a value captured by one of the variants above. - PartialExpr(ExprF), -} - -impl ValueF { - pub(crate) fn into_value_with_type(self, t: Value) -> Value { - Value::from_valuef_and_type(self, t) - } - - pub(crate) fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr { - match self { - ValueF::Lam(x, t, e) => rc(ExprF::Lam( - x.to_label_maybe_alpha(opts.alpha), - t.to_expr(opts), - e.to_expr(opts), - )), - ValueF::AppliedBuiltin(b, args) => args - .iter() - .map(|v| v.to_expr(opts)) - .fold(rc(ExprF::Builtin(*b)), |acc, v| rc(ExprF::App(acc, v))), - ValueF::Pi(x, t, e) => rc(ExprF::Pi( - x.to_label_maybe_alpha(opts.alpha), - t.to_expr(opts), - e.to_expr(opts), - )), - ValueF::Var(v) => rc(ExprF::Var(v.to_var(opts.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.to_expr(opts), - )), - ValueF::NEOptionalLit(n) => rc(ExprF::SomeLit(n.to_expr(opts))), - ValueF::EmptyListLit(n) => rc(ExprF::EmptyListLit(rc(ExprF::App( - rc(ExprF::Builtin(Builtin::List)), - n.to_expr(opts), - )))), - ValueF::NEListLit(elts) => rc(ExprF::NEListLit( - elts.iter().map(|n| n.to_expr(opts)).collect(), - )), - ValueF::RecordLit(kvs) => rc(ExprF::RecordLit( - kvs.iter() - .map(|(k, v)| (k.clone(), v.to_expr(opts))) - .collect(), - )), - ValueF::RecordType(kts) => rc(ExprF::RecordType( - kts.iter() - .map(|(k, v)| (k.clone(), v.to_expr(opts))) - .collect(), - )), - ValueF::UnionType(kts) => rc(ExprF::UnionType( - kts.iter() - .map(|(k, v)| { - (k.clone(), v.as_ref().map(|v| v.to_expr(opts))) - }) - .collect(), - )), - ValueF::UnionConstructor(l, kts) => rc(ExprF::Field( - ValueF::UnionType(kts.clone()).to_expr(opts), - l.clone(), - )), - ValueF::UnionLit(l, v, kts) => rc(ExprF::App( - ValueF::UnionConstructor(l.clone(), kts.clone()).to_expr(opts), - v.to_expr(opts), - )), - ValueF::TextLit(elts) => rc(ExprF::TextLit( - elts.iter() - .map(|contents| contents.map_ref(|e| e.to_expr(opts))) - .collect(), - )), - ValueF::Equivalence(x, y) => rc(ExprF::BinOp( - syntax::BinOp::Equivalence, - x.to_expr(opts), - y.to_expr(opts), - )), - ValueF::PartialExpr(e) => rc(e.map_ref(|v| v.to_expr(opts))), - } - } - - 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(); - } - - 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() { - x.map_mut(Value::normalize_mut); - } - } - ValueF::Equivalence(x, y) => { - x.normalize_mut(); - y.normalize_mut(); - } - ValueF::PartialExpr(e) => { - e.map_mut(Value::normalize_mut); - } - } - } - - pub(crate) fn from_builtin(b: Builtin) -> ValueF { - ValueF::AppliedBuiltin(b, vec![]) - } -} - -impl Shift for ValueF { - 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)?) - } - ValueF::EmptyListLit(tth) => { - ValueF::EmptyListLit(tth.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 { - fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { - match self { - ValueF::AppliedBuiltin(b, args) => { - ValueF::AppliedBuiltin(*b, args.subst_shift(var, val)) - } - ValueF::PartialExpr(e) => { - ValueF::PartialExpr(e.subst_shift(var, val)) - } - ValueF::TextLit(elts) => { - ValueF::TextLit(elts.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_whnf_ignore_type(), - 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)) - } - ValueF::NEListLit(elts) => { - ValueF::NEListLit(elts.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)) - } - ValueF::UnionConstructor(x, kts) => { - ValueF::UnionConstructor(x.clone(), kts.subst_shift(var, val)) - } - 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), - ), - } - } -} diff --git a/dhall/src/semantics/core/var.rs b/dhall/src/semantics/core/var.rs index 184a372..77473f6 100644 --- a/dhall/src/semantics/core/var.rs +++ b/dhall/src/semantics/core/var.rs @@ -12,7 +12,7 @@ pub struct AlphaVar { } // Exactly like a Label, but equality returns always true. -// This is so that ValueF equality is exactly alpha-equivalence. +// This is so that ValueKind equality is exactly alpha-equivalence. #[derive(Clone, Eq)] pub struct AlphaLabel(Label); -- cgit v1.2.3 From fd665388b6f1fd80ded9010640ac65cfebca7bc6 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 17 Dec 2019 16:00:51 +0000 Subject: Move out conversion from value back to ast to its own file --- dhall/src/semantics/core/value.rs | 25 ++++------- dhall/src/semantics/core/value_kind.rs | 82 ++++------------------------------ 2 files changed, 17 insertions(+), 90 deletions(-) (limited to 'dhall/src/semantics/core') diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index 7403742..ad0861b 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -8,6 +8,7 @@ use crate::semantics::error::{TypeError, TypeMessage}; use crate::semantics::phase::normalize::{apply_any, normalize_whnf}; use crate::semantics::phase::typecheck::{builtin_to_value, const_to_value}; use crate::semantics::phase::{NormalizedExpr, Typed}; +use crate::semantics::to_expr; use crate::syntax::{Builtin, Const, Span}; #[derive(Debug, Clone, Copy)] @@ -44,15 +45,6 @@ struct ValueInternal { #[derive(Clone)] pub(crate) struct Value(Rc>); -#[derive(Copy, Clone)] -/// Controls conversion from `Value` to `Expr` -pub(crate) struct ToExprOptions { - /// Whether to convert all variables to `_` - pub(crate) alpha: bool, - /// Whether to normalize before converting - pub(crate) normalize: bool, -} - impl ValueInternal { fn into_value(self) -> Value { Value(Rc::new(RefCell::new(self))) @@ -174,9 +166,9 @@ impl Value { fn as_internal_mut(&self) -> RefMut { self.0.borrow_mut() } - /// WARNING: The returned ValueKind may be entirely unnormalized, in aprticular it may just be an + /// WARNING: The returned ValueKind may be entirely unnormalized, in particular it may just be an /// unevaled PartialExpr. You probably want to use `as_whnf`. - fn as_kind(&self) -> Ref { + pub(crate) fn as_kind(&self) -> Ref { Ref::map(self.as_internal(), ValueInternal::as_kind) } /// This is what you want if you want to pattern-match on the value. @@ -187,11 +179,12 @@ impl Value { self.as_kind() } - pub(crate) fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr { - if opts.normalize { - self.normalize_whnf(); - } - self.as_kind().to_expr(opts) + /// Converts a value back to the corresponding AST expression. + pub(crate) fn to_expr( + &self, + opts: to_expr::ToExprOptions, + ) -> NormalizedExpr { + to_expr::value_to_expr(self, opts) } pub(crate) fn to_whnf_ignore_type(&self) -> ValueKind { self.as_whnf().clone() diff --git a/dhall/src/semantics/core/value_kind.rs b/dhall/src/semantics/core/value_kind.rs index 36ba068..47df39d 100644 --- a/dhall/src/semantics/core/value_kind.rs +++ b/dhall/src/semantics/core/value_kind.rs @@ -1,10 +1,9 @@ use std::collections::HashMap; -use crate::semantics::core::value::{ToExprOptions, Value}; +use crate::semantics::core::value::Value; use crate::semantics::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; -use crate::semantics::phase::typecheck::rc; use crate::semantics::phase::{Normalized, NormalizedExpr}; -use crate::syntax; +use crate::semantics::to_expr; use crate::syntax::{ Builtin, Const, ExprF, Integer, InterpolatedTextContents, Label, NaiveDouble, Natural, @@ -52,77 +51,12 @@ impl ValueKind { Value::from_kind_and_type(self, t) } - pub(crate) fn to_expr(&self, opts: ToExprOptions) -> NormalizedExpr { - match self { - ValueKind::Lam(x, t, e) => rc(ExprF::Lam( - x.to_label_maybe_alpha(opts.alpha), - t.to_expr(opts), - e.to_expr(opts), - )), - ValueKind::AppliedBuiltin(b, args) => args - .iter() - .map(|v| v.to_expr(opts)) - .fold(rc(ExprF::Builtin(*b)), |acc, v| rc(ExprF::App(acc, v))), - ValueKind::Pi(x, t, e) => rc(ExprF::Pi( - x.to_label_maybe_alpha(opts.alpha), - t.to_expr(opts), - e.to_expr(opts), - )), - ValueKind::Var(v) => rc(ExprF::Var(v.to_var(opts.alpha))), - ValueKind::Const(c) => rc(ExprF::Const(*c)), - ValueKind::BoolLit(b) => rc(ExprF::BoolLit(*b)), - ValueKind::NaturalLit(n) => rc(ExprF::NaturalLit(*n)), - ValueKind::IntegerLit(n) => rc(ExprF::IntegerLit(*n)), - ValueKind::DoubleLit(n) => rc(ExprF::DoubleLit(*n)), - ValueKind::EmptyOptionalLit(n) => rc(ExprF::App( - rc(ExprF::Builtin(Builtin::OptionalNone)), - n.to_expr(opts), - )), - ValueKind::NEOptionalLit(n) => rc(ExprF::SomeLit(n.to_expr(opts))), - ValueKind::EmptyListLit(n) => rc(ExprF::EmptyListLit(rc( - ExprF::App(rc(ExprF::Builtin(Builtin::List)), n.to_expr(opts)), - ))), - ValueKind::NEListLit(elts) => rc(ExprF::NEListLit( - elts.iter().map(|n| n.to_expr(opts)).collect(), - )), - ValueKind::RecordLit(kvs) => rc(ExprF::RecordLit( - kvs.iter() - .map(|(k, v)| (k.clone(), v.to_expr(opts))) - .collect(), - )), - ValueKind::RecordType(kts) => rc(ExprF::RecordType( - kts.iter() - .map(|(k, v)| (k.clone(), v.to_expr(opts))) - .collect(), - )), - ValueKind::UnionType(kts) => rc(ExprF::UnionType( - kts.iter() - .map(|(k, v)| { - (k.clone(), v.as_ref().map(|v| v.to_expr(opts))) - }) - .collect(), - )), - ValueKind::UnionConstructor(l, kts) => rc(ExprF::Field( - ValueKind::UnionType(kts.clone()).to_expr(opts), - l.clone(), - )), - ValueKind::UnionLit(l, v, kts) => rc(ExprF::App( - ValueKind::UnionConstructor(l.clone(), kts.clone()) - .to_expr(opts), - v.to_expr(opts), - )), - ValueKind::TextLit(elts) => rc(ExprF::TextLit( - elts.iter() - .map(|contents| contents.map_ref(|e| e.to_expr(opts))) - .collect(), - )), - ValueKind::Equivalence(x, y) => rc(ExprF::BinOp( - syntax::BinOp::Equivalence, - x.to_expr(opts), - y.to_expr(opts), - )), - ValueKind::PartialExpr(e) => rc(e.map_ref(|v| v.to_expr(opts))), - } + /// Converts a value back to the corresponding AST expression. + pub(crate) fn to_expr( + &self, + opts: to_expr::ToExprOptions, + ) -> NormalizedExpr { + to_expr::kind_to_expr(self, opts) } pub(crate) fn normalize_mut(&mut self) { -- cgit v1.2.3 From 78d066a44c5598794602effa4c10a09f80ed1e72 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 20 Dec 2019 17:57:49 +0000 Subject: Move error module to root of crate --- dhall/src/semantics/core/context.rs | 2 +- dhall/src/semantics/core/value.rs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'dhall/src/semantics/core') diff --git a/dhall/src/semantics/core/context.rs b/dhall/src/semantics/core/context.rs index 8861378..9dfd22b 100644 --- a/dhall/src/semantics/core/context.rs +++ b/dhall/src/semantics/core/context.rs @@ -1,10 +1,10 @@ use std::collections::HashMap; use std::rc::Rc; +use crate::error::TypeError; use crate::semantics::core::value::Value; use crate::semantics::core::value_kind::ValueKind; use crate::semantics::core::var::{AlphaVar, Shift, Subst}; -use crate::semantics::error::TypeError; use crate::syntax::{Label, V}; #[derive(Debug, Clone)] diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index ad0861b..9511cc2 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -1,10 +1,10 @@ use std::cell::{Ref, RefCell, RefMut}; use std::rc::Rc; +use crate::error::{TypeError, TypeMessage}; use crate::semantics::core::context::TypecheckContext; use crate::semantics::core::value_kind::ValueKind; use crate::semantics::core::var::{AlphaVar, Shift, Subst}; -use crate::semantics::error::{TypeError, TypeMessage}; use crate::semantics::phase::normalize::{apply_any, normalize_whnf}; use crate::semantics::phase::typecheck::{builtin_to_value, const_to_value}; use crate::semantics::phase::{NormalizedExpr, Typed}; -- cgit v1.2.3 From e355984c3c83f8288eac36023c361db869643367 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 20 Dec 2019 18:12:10 +0000 Subject: s/ExprF/ExprKind/ --- dhall/src/semantics/core/value_kind.rs | 4 ++-- dhall/src/semantics/core/var.rs | 6 +++--- 2 files changed, 5 insertions(+), 5 deletions(-) (limited to 'dhall/src/semantics/core') diff --git a/dhall/src/semantics/core/value_kind.rs b/dhall/src/semantics/core/value_kind.rs index 47df39d..35b2b23 100644 --- a/dhall/src/semantics/core/value_kind.rs +++ b/dhall/src/semantics/core/value_kind.rs @@ -5,7 +5,7 @@ use crate::semantics::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; use crate::semantics::phase::{Normalized, NormalizedExpr}; use crate::semantics::to_expr; use crate::syntax::{ - Builtin, Const, ExprF, Integer, InterpolatedTextContents, Label, + Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label, NaiveDouble, Natural, }; @@ -43,7 +43,7 @@ pub(crate) enum ValueKind { TextLit(Vec>), Equivalence(Value, Value), // Invariant: in whnf, this must not contain a value captured by one of the variants above. - PartialExpr(ExprF), + PartialExpr(ExprKind), } impl ValueKind { diff --git a/dhall/src/semantics/core/var.rs b/dhall/src/semantics/core/var.rs index 77473f6..1548713 100644 --- a/dhall/src/semantics/core/var.rs +++ b/dhall/src/semantics/core/var.rs @@ -1,6 +1,6 @@ use std::collections::HashMap; -use crate::syntax::{ExprF, InterpolatedTextContents, Label, V}; +use crate::syntax::{ExprKind, InterpolatedTextContents, Label, V}; /// Stores a pair of variables: a normal one and one /// that corresponds to the alpha-normalized version of the first one. @@ -190,7 +190,7 @@ impl Shift for std::cell::RefCell { } } -impl Shift for ExprF { +impl Shift for ExprKind { fn shift(&self, delta: isize, var: &AlphaVar) -> Option { Some(self.traverse_ref_with_special_handling_of_binders( |v| Ok(v.shift(delta, var)?), @@ -262,7 +262,7 @@ impl> Subst for std::cell::RefCell { } } -impl, E: Clone> Subst for ExprF { +impl, E: Clone> Subst for ExprKind { fn subst_shift(&self, var: &AlphaVar, val: &S) -> Self { self.map_ref_with_special_handling_of_binders( |v| v.subst_shift(var, val), -- cgit v1.2.3 From bc51d829f8b725531159a190f0096061df30b2cb Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 20 Dec 2019 19:18:40 +0000 Subject: Reorder value.rs --- dhall/src/semantics/core/value.rs | 162 +++++++++++++++++++------------------- 1 file changed, 81 insertions(+), 81 deletions(-) (limited to 'dhall/src/semantics/core') diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index 9511cc2..1e3b965 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -11,6 +11,25 @@ use crate::semantics::phase::{NormalizedExpr, Typed}; use crate::semantics::to_expr; use crate::syntax::{Builtin, Const, Span}; +use self::Form::{Unevaled, NF, WHNF}; + +/// 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. +#[derive(Clone)] +pub(crate) struct Value(Rc>); + +/// Invariant: if `form` is `WHNF`, `value` must be in Weak Head Normal Form +/// Invariant: if `form` is `NF`, `value` must be fully normalized +#[derive(Debug)] +struct ValueInternal { + form: Form, + kind: ValueKind, + /// This is None if and only if `value` is `Sort` (which doesn't have a type) + ty: Option, + span: Span, +} + #[derive(Debug, Clone, Copy)] pub(crate) enum Form { /// No constraints; expression may not be normalized at all. @@ -25,87 +44,6 @@ pub(crate) enum Form { /// if we have the first constructor of the NF at all levels, we actually have the NF. NF, } -use Form::{Unevaled, NF, WHNF}; - -/// Partially normalized value. -/// Invariant: if `form` is `WHNF`, `value` must be in Weak Head Normal Form -/// Invariant: if `form` is `NF`, `value` must be fully normalized -#[derive(Debug)] -struct ValueInternal { - form: Form, - kind: ValueKind, - /// This is None if and only if `value` is `Sort` (which doesn't have a type) - ty: Option, - span: Span, -} - -/// 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. -#[derive(Clone)] -pub(crate) struct Value(Rc>); - -impl ValueInternal { - fn into_value(self) -> Value { - Value(Rc::new(RefCell::new(self))) - } - fn as_kind(&self) -> &ValueKind { - &self.kind - } - - fn normalize_whnf(&mut self) { - take_mut::take_or_recover( - self, - // Dummy value in case the other closure panics - || ValueInternal { - form: Unevaled, - kind: ValueKind::Const(Const::Type), - ty: None, - span: Span::Artificial, - }, - |vint| match (&vint.form, &vint.ty) { - (Unevaled, Some(ty)) => ValueInternal { - form: WHNF, - kind: normalize_whnf(vint.kind, &ty), - ty: vint.ty, - span: vint.span, - }, - // `value` is `Sort` - (Unevaled, None) => ValueInternal { - form: NF, - kind: ValueKind::Const(Const::Sort), - ty: None, - span: vint.span, - }, - // Already in WHNF - (WHNF, _) | (NF, _) => vint, - }, - ) - } - fn normalize_nf(&mut self) { - match self.form { - Unevaled => { - self.normalize_whnf(); - self.normalize_nf(); - } - WHNF => { - self.kind.normalize_mut(); - self.form = NF; - } - // Already in NF - NF => {} - } - } - - fn get_type(&self) -> Result<&Value, TypeError> { - match &self.ty { - Some(t) => Ok(t), - None => { - Err(TypeError::new(&TypecheckContext::new(), TypeMessage::Sort)) - } - } - } -} impl Value { fn new(kind: ValueKind, form: Form, ty: Value, span: Span) -> Value { @@ -258,6 +196,68 @@ impl Value { } } +impl ValueInternal { + fn into_value(self) -> Value { + Value(Rc::new(RefCell::new(self))) + } + fn as_kind(&self) -> &ValueKind { + &self.kind + } + + fn normalize_whnf(&mut self) { + take_mut::take_or_recover( + self, + // Dummy value in case the other closure panics + || ValueInternal { + form: Unevaled, + kind: ValueKind::Const(Const::Type), + ty: None, + span: Span::Artificial, + }, + |vint| match (&vint.form, &vint.ty) { + (Unevaled, Some(ty)) => ValueInternal { + form: WHNF, + kind: normalize_whnf(vint.kind, &ty), + ty: vint.ty, + span: vint.span, + }, + // `value` is `Sort` + (Unevaled, None) => ValueInternal { + form: NF, + kind: ValueKind::Const(Const::Sort), + ty: None, + span: vint.span, + }, + // Already in WHNF + (WHNF, _) | (NF, _) => vint, + }, + ) + } + fn normalize_nf(&mut self) { + match self.form { + Unevaled => { + self.normalize_whnf(); + self.normalize_nf(); + } + WHNF => { + self.kind.normalize_mut(); + self.form = NF; + } + // Already in NF + NF => {} + } + } + + fn get_type(&self) -> Result<&Value, TypeError> { + match &self.ty { + Some(t) => Ok(t), + None => { + Err(TypeError::new(&TypecheckContext::new(), TypeMessage::Sort)) + } + } + } +} + impl Shift for Value { fn shift(&self, delta: isize, var: &AlphaVar) -> Option { Some(Value(self.0.shift(delta, var)?)) -- cgit v1.2.3 From 64cca1837cc97b7679c4e2ffd54a22ad50f05cfd Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 20 Dec 2019 19:26:08 +0000 Subject: Move ValueKind into value.rs --- dhall/src/semantics/core/context.rs | 2 +- dhall/src/semantics/core/mod.rs | 1 - dhall/src/semantics/core/value.rs | 270 ++++++++++++++++++++++++++++++++- dhall/src/semantics/core/value_kind.rs | 267 -------------------------------- 4 files changed, 265 insertions(+), 275 deletions(-) delete mode 100644 dhall/src/semantics/core/value_kind.rs (limited to 'dhall/src/semantics/core') diff --git a/dhall/src/semantics/core/context.rs b/dhall/src/semantics/core/context.rs index 9dfd22b..f755f72 100644 --- a/dhall/src/semantics/core/context.rs +++ b/dhall/src/semantics/core/context.rs @@ -3,7 +3,7 @@ use std::rc::Rc; use crate::error::TypeError; use crate::semantics::core::value::Value; -use crate::semantics::core::value_kind::ValueKind; +use crate::semantics::core::value::ValueKind; use crate::semantics::core::var::{AlphaVar, Shift, Subst}; use crate::syntax::{Label, V}; diff --git a/dhall/src/semantics/core/mod.rs b/dhall/src/semantics/core/mod.rs index bf3d390..90d74ea 100644 --- a/dhall/src/semantics/core/mod.rs +++ b/dhall/src/semantics/core/mod.rs @@ -1,4 +1,3 @@ pub mod context; pub mod value; -pub mod value_kind; pub mod var; diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs index 1e3b965..ca7c4bc 100644 --- a/dhall/src/semantics/core/value.rs +++ b/dhall/src/semantics/core/value.rs @@ -1,21 +1,27 @@ use std::cell::{Ref, RefCell, RefMut}; +use std::collections::HashMap; use std::rc::Rc; use crate::error::{TypeError, TypeMessage}; use crate::semantics::core::context::TypecheckContext; -use crate::semantics::core::value_kind::ValueKind; -use crate::semantics::core::var::{AlphaVar, Shift, Subst}; +use crate::semantics::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; use crate::semantics::phase::normalize::{apply_any, normalize_whnf}; use crate::semantics::phase::typecheck::{builtin_to_value, const_to_value}; -use crate::semantics::phase::{NormalizedExpr, Typed}; +use crate::semantics::phase::{Normalized, NormalizedExpr, Typed}; use crate::semantics::to_expr; -use crate::syntax::{Builtin, Const, Span}; +use crate::syntax::{ + Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label, + NaiveDouble, Natural, Span, +}; use self::Form::{Unevaled, NF, WHNF}; -/// Stores a possibly unevaluated value. Gets (partially) normalized on-demand, -/// sharing computation automatically. Uses a RefCell to share computation. +/// 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. +/// If you compare for equality two `Value`s in WHNF, then equality will be up to alpha-equivalence +/// (renaming of bound variables) and beta-equivalence (normalization). It will recursively +/// normalize as needed. #[derive(Clone)] pub(crate) struct Value(Rc>); @@ -45,6 +51,38 @@ pub(crate) enum Form { NF, } +#[derive(Debug, Clone, PartialEq, Eq)] +pub(crate) enum ValueKind { + /// Closures + Lam(AlphaLabel, Value, Value), + Pi(AlphaLabel, Value, Value), + // Invariant: in whnf, 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(Value), + NEOptionalLit(Value), + // EmptyListLit(t) means `[] : List t`, not `[] : t` + EmptyListLit(Value), + NEListLit(Vec), + RecordType(HashMap), + RecordLit(HashMap), + UnionType(HashMap>), + UnionConstructor(Label, HashMap>), + UnionLit(Label, Value, HashMap>), + // Invariant: in whnf, this must not contain interpolations that are themselves TextLits, and + // contiguous text values must be merged. + TextLit(Vec>), + Equivalence(Value, Value), + // Invariant: in whnf, this must not contain a value captured by one of the variants above. + PartialExpr(ExprKind), +} + impl Value { fn new(kind: ValueKind, form: Form, ty: Value, span: Span) -> Value { ValueInternal { @@ -258,6 +296,94 @@ impl ValueInternal { } } +impl ValueKind { + pub(crate) fn into_value_with_type(self, t: Value) -> Value { + Value::from_kind_and_type(self, t) + } + + /// Converts a value back to the corresponding AST expression. + pub(crate) fn to_expr( + &self, + opts: to_expr::ToExprOptions, + ) -> NormalizedExpr { + to_expr::kind_to_expr(self, opts) + } + + pub(crate) fn normalize_mut(&mut self) { + match self { + ValueKind::Var(_) + | ValueKind::Const(_) + | ValueKind::BoolLit(_) + | ValueKind::NaturalLit(_) + | ValueKind::IntegerLit(_) + | ValueKind::DoubleLit(_) => {} + + ValueKind::EmptyOptionalLit(tth) | ValueKind::EmptyListLit(tth) => { + tth.normalize_mut(); + } + + ValueKind::NEOptionalLit(th) => { + th.normalize_mut(); + } + ValueKind::Lam(_, t, e) => { + t.normalize_mut(); + e.normalize_mut(); + } + ValueKind::Pi(_, t, e) => { + t.normalize_mut(); + e.normalize_mut(); + } + ValueKind::AppliedBuiltin(_, args) => { + for x in args.iter_mut() { + x.normalize_mut(); + } + } + ValueKind::NEListLit(elts) => { + for x in elts.iter_mut() { + x.normalize_mut(); + } + } + ValueKind::RecordLit(kvs) => { + for x in kvs.values_mut() { + x.normalize_mut(); + } + } + ValueKind::RecordType(kvs) => { + for x in kvs.values_mut() { + x.normalize_mut(); + } + } + ValueKind::UnionType(kts) | ValueKind::UnionConstructor(_, kts) => { + for x in kts.values_mut().flat_map(|opt| opt) { + x.normalize_mut(); + } + } + ValueKind::UnionLit(_, v, kts) => { + v.normalize_mut(); + for x in kts.values_mut().flat_map(|opt| opt) { + x.normalize_mut(); + } + } + ValueKind::TextLit(elts) => { + for x in elts.iter_mut() { + x.map_mut(Value::normalize_mut); + } + } + ValueKind::Equivalence(x, y) => { + x.normalize_mut(); + y.normalize_mut(); + } + ValueKind::PartialExpr(e) => { + e.map_mut(Value::normalize_mut); + } + } + } + + pub(crate) fn from_builtin(b: Builtin) -> ValueKind { + ValueKind::AppliedBuiltin(b, vec![]) + } +} + impl Shift for Value { fn shift(&self, delta: isize, var: &AlphaVar) -> Option { Some(Value(self.0.shift(delta, var)?)) @@ -275,6 +401,71 @@ impl Shift for ValueInternal { } } +impl Shift for ValueKind { + fn shift(&self, delta: isize, var: &AlphaVar) -> Option { + Some(match self { + ValueKind::Lam(x, t, e) => ValueKind::Lam( + x.clone(), + t.shift(delta, var)?, + e.shift(delta, &var.under_binder(x))?, + ), + ValueKind::AppliedBuiltin(b, args) => { + ValueKind::AppliedBuiltin(*b, args.shift(delta, var)?) + } + ValueKind::Pi(x, t, e) => ValueKind::Pi( + x.clone(), + t.shift(delta, var)?, + e.shift(delta, &var.under_binder(x))?, + ), + ValueKind::Var(v) => ValueKind::Var(v.shift(delta, var)?), + ValueKind::Const(c) => ValueKind::Const(*c), + ValueKind::BoolLit(b) => ValueKind::BoolLit(*b), + ValueKind::NaturalLit(n) => ValueKind::NaturalLit(*n), + ValueKind::IntegerLit(n) => ValueKind::IntegerLit(*n), + ValueKind::DoubleLit(n) => ValueKind::DoubleLit(*n), + ValueKind::EmptyOptionalLit(tth) => { + ValueKind::EmptyOptionalLit(tth.shift(delta, var)?) + } + ValueKind::NEOptionalLit(th) => { + ValueKind::NEOptionalLit(th.shift(delta, var)?) + } + ValueKind::EmptyListLit(tth) => { + ValueKind::EmptyListLit(tth.shift(delta, var)?) + } + ValueKind::NEListLit(elts) => { + ValueKind::NEListLit(elts.shift(delta, var)?) + } + ValueKind::RecordLit(kvs) => { + ValueKind::RecordLit(kvs.shift(delta, var)?) + } + ValueKind::RecordType(kvs) => { + ValueKind::RecordType(kvs.shift(delta, var)?) + } + ValueKind::UnionType(kts) => { + ValueKind::UnionType(kts.shift(delta, var)?) + } + ValueKind::UnionConstructor(x, kts) => { + ValueKind::UnionConstructor(x.clone(), kts.shift(delta, var)?) + } + ValueKind::UnionLit(x, v, kts) => ValueKind::UnionLit( + x.clone(), + v.shift(delta, var)?, + kts.shift(delta, var)?, + ), + ValueKind::TextLit(elts) => { + ValueKind::TextLit(elts.shift(delta, var)?) + } + ValueKind::Equivalence(x, y) => ValueKind::Equivalence( + x.shift(delta, var)?, + y.shift(delta, var)?, + ), + ValueKind::PartialExpr(e) => { + ValueKind::PartialExpr(e.shift(delta, var)?) + } + }) + } +} + impl Subst for Value { fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { match &*self.as_kind() { @@ -303,6 +494,73 @@ impl Subst for ValueInternal { } } +impl Subst for ValueKind { + fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { + match self { + ValueKind::AppliedBuiltin(b, args) => { + ValueKind::AppliedBuiltin(*b, args.subst_shift(var, val)) + } + ValueKind::PartialExpr(e) => { + ValueKind::PartialExpr(e.subst_shift(var, val)) + } + ValueKind::TextLit(elts) => { + ValueKind::TextLit(elts.subst_shift(var, val)) + } + ValueKind::Lam(x, t, e) => ValueKind::Lam( + x.clone(), + t.subst_shift(var, val), + e.subst_shift(&var.under_binder(x), &val.under_binder(x)), + ), + ValueKind::Pi(x, t, e) => ValueKind::Pi( + x.clone(), + t.subst_shift(var, val), + e.subst_shift(&var.under_binder(x), &val.under_binder(x)), + ), + ValueKind::Var(v) if v == var => val.to_whnf_ignore_type(), + ValueKind::Var(v) => ValueKind::Var(v.shift(-1, var).unwrap()), + ValueKind::Const(c) => ValueKind::Const(*c), + ValueKind::BoolLit(b) => ValueKind::BoolLit(*b), + ValueKind::NaturalLit(n) => ValueKind::NaturalLit(*n), + ValueKind::IntegerLit(n) => ValueKind::IntegerLit(*n), + ValueKind::DoubleLit(n) => ValueKind::DoubleLit(*n), + ValueKind::EmptyOptionalLit(tth) => { + ValueKind::EmptyOptionalLit(tth.subst_shift(var, val)) + } + ValueKind::NEOptionalLit(th) => { + ValueKind::NEOptionalLit(th.subst_shift(var, val)) + } + ValueKind::EmptyListLit(tth) => { + ValueKind::EmptyListLit(tth.subst_shift(var, val)) + } + ValueKind::NEListLit(elts) => { + ValueKind::NEListLit(elts.subst_shift(var, val)) + } + ValueKind::RecordLit(kvs) => { + ValueKind::RecordLit(kvs.subst_shift(var, val)) + } + ValueKind::RecordType(kvs) => { + ValueKind::RecordType(kvs.subst_shift(var, val)) + } + ValueKind::UnionType(kts) => { + ValueKind::UnionType(kts.subst_shift(var, val)) + } + ValueKind::UnionConstructor(x, kts) => ValueKind::UnionConstructor( + x.clone(), + kts.subst_shift(var, val), + ), + ValueKind::UnionLit(x, v, kts) => ValueKind::UnionLit( + x.clone(), + v.subst_shift(var, val), + kts.subst_shift(var, val), + ), + ValueKind::Equivalence(x, y) => ValueKind::Equivalence( + x.subst_shift(var, val), + y.subst_shift(var, val), + ), + } + } +} + // TODO: use Rc comparison to shortcut on identical pointers impl std::cmp::PartialEq for Value { fn eq(&self, other: &Self) -> bool { diff --git a/dhall/src/semantics/core/value_kind.rs b/dhall/src/semantics/core/value_kind.rs deleted file mode 100644 index 35b2b23..0000000 --- a/dhall/src/semantics/core/value_kind.rs +++ /dev/null @@ -1,267 +0,0 @@ -use std::collections::HashMap; - -use crate::semantics::core::value::Value; -use crate::semantics::core::var::{AlphaLabel, AlphaVar, Shift, Subst}; -use crate::semantics::phase::{Normalized, NormalizedExpr}; -use crate::semantics::to_expr; -use crate::syntax::{ - Builtin, Const, ExprKind, Integer, InterpolatedTextContents, Label, - NaiveDouble, Natural, -}; - -/// A semantic value. Subexpressions are Values, which are partially evaluated expressions that are -/// normalized on-demand. -/// If you compare for equality two `ValueKind`s in WHNF, then equality will be up to -/// alpha-equivalence (renaming of bound variables) and beta-equivalence (normalization). It will -/// recursively normalize as needed. -#[derive(Debug, Clone, PartialEq, Eq)] -pub(crate) enum ValueKind { - /// Closures - Lam(AlphaLabel, Value, Value), - Pi(AlphaLabel, Value, Value), - // Invariant: in whnf, 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(Value), - NEOptionalLit(Value), - // EmptyListLit(t) means `[] : List t`, not `[] : t` - EmptyListLit(Value), - NEListLit(Vec), - RecordType(HashMap), - RecordLit(HashMap), - UnionType(HashMap>), - UnionConstructor(Label, HashMap>), - UnionLit(Label, Value, HashMap>), - // Invariant: in whnf, this must not contain interpolations that are themselves TextLits, and - // contiguous text values must be merged. - TextLit(Vec>), - Equivalence(Value, Value), - // Invariant: in whnf, this must not contain a value captured by one of the variants above. - PartialExpr(ExprKind), -} - -impl ValueKind { - pub(crate) fn into_value_with_type(self, t: Value) -> Value { - Value::from_kind_and_type(self, t) - } - - /// Converts a value back to the corresponding AST expression. - pub(crate) fn to_expr( - &self, - opts: to_expr::ToExprOptions, - ) -> NormalizedExpr { - to_expr::kind_to_expr(self, opts) - } - - pub(crate) fn normalize_mut(&mut self) { - match self { - ValueKind::Var(_) - | ValueKind::Const(_) - | ValueKind::BoolLit(_) - | ValueKind::NaturalLit(_) - | ValueKind::IntegerLit(_) - | ValueKind::DoubleLit(_) => {} - - ValueKind::EmptyOptionalLit(tth) | ValueKind::EmptyListLit(tth) => { - tth.normalize_mut(); - } - - ValueKind::NEOptionalLit(th) => { - th.normalize_mut(); - } - ValueKind::Lam(_, t, e) => { - t.normalize_mut(); - e.normalize_mut(); - } - ValueKind::Pi(_, t, e) => { - t.normalize_mut(); - e.normalize_mut(); - } - ValueKind::AppliedBuiltin(_, args) => { - for x in args.iter_mut() { - x.normalize_mut(); - } - } - ValueKind::NEListLit(elts) => { - for x in elts.iter_mut() { - x.normalize_mut(); - } - } - ValueKind::RecordLit(kvs) => { - for x in kvs.values_mut() { - x.normalize_mut(); - } - } - ValueKind::RecordType(kvs) => { - for x in kvs.values_mut() { - x.normalize_mut(); - } - } - ValueKind::UnionType(kts) | ValueKind::UnionConstructor(_, kts) => { - for x in kts.values_mut().flat_map(|opt| opt) { - x.normalize_mut(); - } - } - ValueKind::UnionLit(_, v, kts) => { - v.normalize_mut(); - for x in kts.values_mut().flat_map(|opt| opt) { - x.normalize_mut(); - } - } - ValueKind::TextLit(elts) => { - for x in elts.iter_mut() { - x.map_mut(Value::normalize_mut); - } - } - ValueKind::Equivalence(x, y) => { - x.normalize_mut(); - y.normalize_mut(); - } - ValueKind::PartialExpr(e) => { - e.map_mut(Value::normalize_mut); - } - } - } - - pub(crate) fn from_builtin(b: Builtin) -> ValueKind { - ValueKind::AppliedBuiltin(b, vec![]) - } -} - -impl Shift for ValueKind { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option { - Some(match self { - ValueKind::Lam(x, t, e) => ValueKind::Lam( - x.clone(), - t.shift(delta, var)?, - e.shift(delta, &var.under_binder(x))?, - ), - ValueKind::AppliedBuiltin(b, args) => { - ValueKind::AppliedBuiltin(*b, args.shift(delta, var)?) - } - ValueKind::Pi(x, t, e) => ValueKind::Pi( - x.clone(), - t.shift(delta, var)?, - e.shift(delta, &var.under_binder(x))?, - ), - ValueKind::Var(v) => ValueKind::Var(v.shift(delta, var)?), - ValueKind::Const(c) => ValueKind::Const(*c), - ValueKind::BoolLit(b) => ValueKind::BoolLit(*b), - ValueKind::NaturalLit(n) => ValueKind::NaturalLit(*n), - ValueKind::IntegerLit(n) => ValueKind::IntegerLit(*n), - ValueKind::DoubleLit(n) => ValueKind::DoubleLit(*n), - ValueKind::EmptyOptionalLit(tth) => { - ValueKind::EmptyOptionalLit(tth.shift(delta, var)?) - } - ValueKind::NEOptionalLit(th) => { - ValueKind::NEOptionalLit(th.shift(delta, var)?) - } - ValueKind::EmptyListLit(tth) => { - ValueKind::EmptyListLit(tth.shift(delta, var)?) - } - ValueKind::NEListLit(elts) => { - ValueKind::NEListLit(elts.shift(delta, var)?) - } - ValueKind::RecordLit(kvs) => { - ValueKind::RecordLit(kvs.shift(delta, var)?) - } - ValueKind::RecordType(kvs) => { - ValueKind::RecordType(kvs.shift(delta, var)?) - } - ValueKind::UnionType(kts) => { - ValueKind::UnionType(kts.shift(delta, var)?) - } - ValueKind::UnionConstructor(x, kts) => { - ValueKind::UnionConstructor(x.clone(), kts.shift(delta, var)?) - } - ValueKind::UnionLit(x, v, kts) => ValueKind::UnionLit( - x.clone(), - v.shift(delta, var)?, - kts.shift(delta, var)?, - ), - ValueKind::TextLit(elts) => { - ValueKind::TextLit(elts.shift(delta, var)?) - } - ValueKind::Equivalence(x, y) => ValueKind::Equivalence( - x.shift(delta, var)?, - y.shift(delta, var)?, - ), - ValueKind::PartialExpr(e) => { - ValueKind::PartialExpr(e.shift(delta, var)?) - } - }) - } -} - -impl Subst for ValueKind { - fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self { - match self { - ValueKind::AppliedBuiltin(b, args) => { - ValueKind::AppliedBuiltin(*b, args.subst_shift(var, val)) - } - ValueKind::PartialExpr(e) => { - ValueKind::PartialExpr(e.subst_shift(var, val)) - } - ValueKind::TextLit(elts) => { - ValueKind::TextLit(elts.subst_shift(var, val)) - } - ValueKind::Lam(x, t, e) => ValueKind::Lam( - x.clone(), - t.subst_shift(var, val), - e.subst_shift(&var.under_binder(x), &val.under_binder(x)), - ), - ValueKind::Pi(x, t, e) => ValueKind::Pi( - x.clone(), - t.subst_shift(var, val), - e.subst_shift(&var.under_binder(x), &val.under_binder(x)), - ), - ValueKind::Var(v) if v == var => val.to_whnf_ignore_type(), - ValueKind::Var(v) => ValueKind::Var(v.shift(-1, var).unwrap()), - ValueKind::Const(c) => ValueKind::Const(*c), - ValueKind::BoolLit(b) => ValueKind::BoolLit(*b), - ValueKind::NaturalLit(n) => ValueKind::NaturalLit(*n), - ValueKind::IntegerLit(n) => ValueKind::IntegerLit(*n), - ValueKind::DoubleLit(n) => ValueKind::DoubleLit(*n), - ValueKind::EmptyOptionalLit(tth) => { - ValueKind::EmptyOptionalLit(tth.subst_shift(var, val)) - } - ValueKind::NEOptionalLit(th) => { - ValueKind::NEOptionalLit(th.subst_shift(var, val)) - } - ValueKind::EmptyListLit(tth) => { - ValueKind::EmptyListLit(tth.subst_shift(var, val)) - } - ValueKind::NEListLit(elts) => { - ValueKind::NEListLit(elts.subst_shift(var, val)) - } - ValueKind::RecordLit(kvs) => { - ValueKind::RecordLit(kvs.subst_shift(var, val)) - } - ValueKind::RecordType(kvs) => { - ValueKind::RecordType(kvs.subst_shift(var, val)) - } - ValueKind::UnionType(kts) => { - ValueKind::UnionType(kts.subst_shift(var, val)) - } - ValueKind::UnionConstructor(x, kts) => ValueKind::UnionConstructor( - x.clone(), - kts.subst_shift(var, val), - ), - ValueKind::UnionLit(x, v, kts) => ValueKind::UnionLit( - x.clone(), - v.subst_shift(var, val), - kts.subst_shift(var, val), - ), - ValueKind::Equivalence(x, y) => ValueKind::Equivalence( - x.subst_shift(var, val), - y.subst_shift(var, val), - ), - } - } -} -- cgit v1.2.3