summaryrefslogtreecommitdiff
path: root/dhall/src/semantics
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--dhall/src/semantics/core/context.rs2
-rw-r--r--dhall/src/semantics/core/mod.rs1
-rw-r--r--dhall/src/semantics/core/value.rs270
-rw-r--r--dhall/src/semantics/core/value_kind.rs267
-rw-r--r--dhall/src/semantics/phase/mod.rs2
-rw-r--r--dhall/src/semantics/phase/normalize.rs2
-rw-r--r--dhall/src/semantics/phase/typecheck.rs2
-rw-r--r--dhall/src/semantics/to_expr.rs2
8 files changed, 269 insertions, 279 deletions
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<RefCell<ValueInternal>>);
@@ -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<Value>),
+
+ 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<Value>),
+ RecordType(HashMap<Label, Value>),
+ RecordLit(HashMap<Label, Value>),
+ UnionType(HashMap<Label, Option<Value>>),
+ UnionConstructor(Label, HashMap<Label, Option<Value>>),
+ UnionLit(Label, Value, HashMap<Label, Option<Value>>),
+ // Invariant: in whnf, this must not contain interpolations that are themselves TextLits, and
+ // contiguous text values must be merged.
+ TextLit(Vec<InterpolatedTextContents<Value>>),
+ Equivalence(Value, Value),
+ // Invariant: in whnf, this must not contain a value captured by one of the variants above.
+ PartialExpr(ExprKind<Value, Normalized>),
+}
+
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<Self> {
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<Self> {
+ 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<Value> for Value {
fn subst_shift(&self, var: &AlphaVar, val: &Value) -> Self {
match &*self.as_kind() {
@@ -303,6 +494,73 @@ impl Subst<Value> for ValueInternal {
}
}
+impl Subst<Value> 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<Value>),
-
- 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<Value>),
- RecordType(HashMap<Label, Value>),
- RecordLit(HashMap<Label, Value>),
- UnionType(HashMap<Label, Option<Value>>),
- UnionConstructor(Label, HashMap<Label, Option<Value>>),
- UnionLit(Label, Value, HashMap<Label, Option<Value>>),
- // Invariant: in whnf, this must not contain interpolations that are themselves TextLits, and
- // contiguous text values must be merged.
- TextLit(Vec<InterpolatedTextContents<Value>>),
- Equivalence(Value, Value),
- // Invariant: in whnf, this must not contain a value captured by one of the variants above.
- PartialExpr(ExprKind<Value, Normalized>),
-}
-
-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<Self> {
- 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<Value> 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/phase/mod.rs b/dhall/src/semantics/phase/mod.rs
index 7c57c3f..b22120d 100644
--- a/dhall/src/semantics/phase/mod.rs
+++ b/dhall/src/semantics/phase/mod.rs
@@ -3,7 +3,7 @@ use std::path::Path;
use crate::error::{EncodeError, Error, ImportError, 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::semantics::to_expr::ToExprOptions;
use crate::syntax::binary;
diff --git a/dhall/src/semantics/phase/normalize.rs b/dhall/src/semantics/phase/normalize.rs
index 3e612aa..d81a910 100644
--- a/dhall/src/semantics/phase/normalize.rs
+++ b/dhall/src/semantics/phase/normalize.rs
@@ -1,7 +1,7 @@
use std::collections::HashMap;
use crate::semantics::core::value::Value;
-use crate::semantics::core::value_kind::ValueKind;
+use crate::semantics::core::value::ValueKind;
use crate::semantics::core::var::{AlphaLabel, AlphaVar, Shift, Subst};
use crate::semantics::phase::Normalized;
use crate::syntax;
diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs
index cf928d8..c439f74 100644
--- a/dhall/src/semantics/phase/typecheck.rs
+++ b/dhall/src/semantics/phase/typecheck.rs
@@ -4,7 +4,7 @@ use std::collections::HashMap;
use crate::error::{TypeError, TypeMessage};
use crate::semantics::core::context::TypecheckContext;
use crate::semantics::core::value::Value;
-use crate::semantics::core::value_kind::ValueKind;
+use crate::semantics::core::value::ValueKind;
use crate::semantics::core::var::{Shift, Subst};
use crate::semantics::phase::normalize::merge_maps;
use crate::semantics::phase::Normalized;
diff --git a/dhall/src/semantics/to_expr.rs b/dhall/src/semantics/to_expr.rs
index 6099976..b21fb29 100644
--- a/dhall/src/semantics/to_expr.rs
+++ b/dhall/src/semantics/to_expr.rs
@@ -1,5 +1,5 @@
use crate::semantics::core::value::Value;
-use crate::semantics::core::value_kind::ValueKind;
+use crate::semantics::core::value::ValueKind;
use crate::semantics::phase::typecheck::rc;
use crate::semantics::phase::NormalizedExpr;
use crate::syntax;
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-26 12:47:42 +0000