summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorNadrieril2019-08-17 19:00:43 +0200
committerNadrieril2019-08-17 19:06:06 +0200
commit6753a1f97bb674d91dd4d42f2ddb25a8119e070d (patch)
tree56ebbfb08d4e7ad41565fcd38507e7d8cd4f8739
parent8dec798929f35df15a7bc3a6caa4f0c7954c4ffc (diff)
s/Thunk/Value/
-rw-r--r--dhall/src/core/context.rs14
-rw-r--r--dhall/src/core/mod.rs2
-rw-r--r--dhall/src/core/thunk.rs406
-rw-r--r--dhall/src/core/value.rs723
-rw-r--r--dhall/src/core/valuef.rs405
-rw-r--r--dhall/src/phase/mod.rs26
-rw-r--r--dhall/src/phase/normalize.rs208
-rw-r--r--dhall/src/phase/typecheck.rs68
-rw-r--r--serde_dhall/src/lib.rs17
9 files changed, 936 insertions, 933 deletions
diff --git a/dhall/src/core/context.rs b/dhall/src/core/context.rs
index b1fbde9..e1a23a9 100644
--- a/dhall/src/core/context.rs
+++ b/dhall/src/core/context.rs
@@ -3,8 +3,8 @@ use std::rc::Rc;
use dhall_syntax::{Label, V};
-use crate::core::thunk::Thunk;
-use crate::core::value::ValueF;
+use crate::core::value::Value;
+use crate::core::valuef::ValueF;
use crate::core::var::{AlphaVar, Shift, Subst};
use crate::error::TypeError;
use crate::phase::{Type, Typed};
@@ -12,7 +12,7 @@ use crate::phase::{Type, Typed};
#[derive(Debug, Clone)]
enum CtxItem {
Kept(AlphaVar, Type),
- Replaced(Thunk, Type),
+ Replaced(Value, Type),
}
#[derive(Debug, Clone)]
@@ -31,7 +31,7 @@ impl TypecheckContext {
let mut vec = self.0.as_ref().clone();
vec.push((
x.clone(),
- CtxItem::Replaced(e.to_thunk(), e.get_type()?.into_owned()),
+ CtxItem::Replaced(e.to_value(), e.get_type()?.into_owned()),
));
Ok(TypecheckContext(Rc::new(vec)))
}
@@ -44,11 +44,11 @@ impl TypecheckContext {
let i = i.under_multiple_binders(&shift_map);
let (th, t) = match i {
CtxItem::Kept(newvar, t) => {
- (ValueF::Var(newvar).into_thunk(), t)
+ (ValueF::Var(newvar).into_value(), t)
}
CtxItem::Replaced(th, t) => (th, t),
};
- return Some(Typed::from_thunk_and_type(th, t));
+ return Some(Typed::from_value_and_type(th, t));
}
Some(newvar) => var = newvar,
};
@@ -133,7 +133,7 @@ impl Subst<Typed> for CtxItem {
),
CtxItem::Kept(v, t) => match v.shift(-1, var) {
None => {
- CtxItem::Replaced(val.to_thunk(), t.subst_shift(var, val))
+ CtxItem::Replaced(val.to_value(), t.subst_shift(var, val))
}
Some(newvar) => CtxItem::Kept(newvar, t.subst_shift(var, val)),
},
diff --git a/dhall/src/core/mod.rs b/dhall/src/core/mod.rs
index 0667df8..08213f7 100644
--- a/dhall/src/core/mod.rs
+++ b/dhall/src/core/mod.rs
@@ -1,4 +1,4 @@
pub mod context;
-pub mod thunk;
pub mod value;
+pub mod valuef;
pub mod var;
diff --git a/dhall/src/core/thunk.rs b/dhall/src/core/thunk.rs
deleted file mode 100644
index 325a410..0000000
--- a/dhall/src/core/thunk.rs
+++ /dev/null
@@ -1,406 +0,0 @@
-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::value::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};
-
-#[derive(Debug, Clone)]
-enum ThunkInternal {
- /// 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<Thunk, Normalized>),
- /// Partially normalized value.
- /// Invariant: if the marker is `NF`, the value must be fully normalized
- ValueF(Marker, ValueF),
-}
-
-#[derive(Debug)]
-struct TypedThunkInternal {
- internal: ThunkInternal,
- 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 the typechecking phase to preserve type information through
-/// the normalization phase.
-#[derive(Clone)]
-pub struct Thunk(Rc<RefCell<TypedThunkInternal>>);
-
-#[derive(Debug, Clone)]
-pub struct TypedThunk(Thunk);
-
-impl ThunkInternal {
- fn into_thunk(self, t: Option<Type>) -> Thunk {
- TypedThunkInternal {
- internal: self,
- typ: t,
- }
- .into_thunk()
- }
-
- fn normalize_whnf(&mut self) {
- match self {
- ThunkInternal::PartialExpr(e) => {
- *self =
- ThunkInternal::ValueF(WHNF, normalize_one_layer(e.clone()))
- }
- // Already at least in WHNF
- ThunkInternal::ValueF(_, _) => {}
- }
- }
-
- fn normalize_nf(&mut self) {
- match self {
- ThunkInternal::PartialExpr(_) => {
- self.normalize_whnf();
- self.normalize_nf();
- }
- ThunkInternal::ValueF(m @ WHNF, v) => {
- v.normalize_mut();
- *m = NF;
- }
- // Already in NF
- ThunkInternal::ValueF(NF, _) => {}
- }
- }
-
- // Always use normalize_whnf before
- fn as_whnf(&self) -> &ValueF {
- match self {
- ThunkInternal::PartialExpr(_) => unreachable!(),
- ThunkInternal::ValueF(_, v) => v,
- }
- }
-
- // Always use normalize_nf before
- fn as_nf(&self) -> &ValueF {
- match self {
- ThunkInternal::PartialExpr(_) | ThunkInternal::ValueF(WHNF, _) => {
- unreachable!()
- }
- ThunkInternal::ValueF(NF, v) => v,
- }
- }
-}
-
-impl TypedThunkInternal {
- fn into_thunk(self) -> Thunk {
- Thunk(Rc::new(RefCell::new(self)))
- }
- fn as_internal(&self) -> &ThunkInternal {
- &self.internal
- }
- fn as_internal_mut(&mut self) -> &mut ThunkInternal {
- &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,
- )),
- }
- }
-}
-
-impl Thunk {
- pub(crate) fn from_valuef(v: ValueF) -> Thunk {
- ThunkInternal::ValueF(WHNF, v).into_thunk(None)
- }
- pub(crate) fn from_valuef_and_type(v: ValueF, t: Type) -> Thunk {
- ThunkInternal::ValueF(WHNF, v).into_thunk(Some(t))
- }
- pub(crate) fn from_partial_expr(e: ExprF<Thunk, Normalized>) -> Thunk {
- ThunkInternal::PartialExpr(e).into_thunk(None)
- }
- pub(crate) fn with_type(self, t: Type) -> Thunk {
- self.as_internal().clone().into_thunk(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 TypedThunkInternal)) {
- 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) {
- self.mutate_internal(|i| i.as_internal_mut().normalize_nf())
- }
-
- fn as_tinternal(&self) -> Ref<TypedThunkInternal> {
- self.0.borrow()
- }
- fn as_tinternal_mut(&mut self) -> RefMut<TypedThunkInternal> {
- self.0.borrow_mut()
- }
- fn as_internal(&self) -> Ref<ThunkInternal> {
- Ref::map(self.as_tinternal(), TypedThunkInternal::as_internal)
- }
- fn as_internal_mut(&self) -> RefMut<ThunkInternal> {
- RefMut::map(self.0.borrow_mut(), TypedThunkInternal::as_internal_mut)
- }
-
- fn do_normalize_whnf(&self) {
- let borrow = self.as_internal();
- match &*borrow {
- ThunkInternal::PartialExpr(_) => {
- drop(borrow);
- self.as_internal_mut().normalize_whnf();
- }
- // Already at least in WHNF
- ThunkInternal::ValueF(_, _) => {}
- }
- }
-
- fn do_normalize_nf(&self) {
- let borrow = self.as_internal();
- match &*borrow {
- ThunkInternal::PartialExpr(_) | ThunkInternal::ValueF(WHNF, _) => {
- drop(borrow);
- self.as_internal_mut().normalize_nf();
- }
- // Already in NF
- ThunkInternal::ValueF(NF, _) => {}
- }
- }
-
- // WARNING: avoid normalizing any thunk while holding on to this ref
- // or you could run into BorrowMut panics
- pub(crate) fn normalize_nf(&self) -> Ref<ValueF> {
- self.do_normalize_nf();
- Ref::map(self.as_internal(), ThunkInternal::as_nf)
- }
-
- // WARNING: avoid normalizing any thunk while holding on to this ref
- // or you could run into BorrowMut panics
- pub(crate) fn as_valuef(&self) -> Ref<ValueF> {
- self.do_normalize_whnf();
- Ref::map(self.as_internal(), ThunkInternal::as_whnf)
- }
-
- 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_val(&self, val: ValueF) -> ValueF {
- self.app_thunk(val.into_thunk())
- }
-
- pub(crate) fn app_thunk(&self, th: Thunk) -> 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 TypedThunk {
- pub(crate) fn from_valuef(v: ValueF) -> TypedThunk {
- TypedThunk::from_thunk_untyped(Thunk::from_valuef(v))
- }
-
- pub(crate) fn from_type(t: Type) -> TypedThunk {
- t.into_typethunk()
- }
-
- pub(crate) fn normalize_nf(&self) -> 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_thunk_and_type(th: Thunk, t: Type) -> Self {
- TypedThunk(th.with_type(t))
- }
- pub fn from_thunk_simple_type(th: Thunk) -> Self {
- TypedThunk::from_thunk_and_type(th, Type::const_type())
- }
- pub(crate) fn from_thunk_untyped(th: Thunk) -> Self {
- TypedThunk(th)
- }
- pub(crate) fn from_const(c: Const) -> Self {
- match type_of_const(c) {
- Ok(t) => TypedThunk::from_valuef_and_type(ValueF::Const(c), t),
- Err(_) => TypedThunk::from_valuef(ValueF::Const(c)),
- }
- }
- pub(crate) fn from_valuef_and_type(v: ValueF, t: Type) -> Self {
- TypedThunk(Thunk::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_thunk(&self) -> Thunk {
- 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_typethunk(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 Thunk {
- fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
- Some(Thunk(self.0.shift(delta, var)?))
- }
-}
-
-impl Shift for ThunkInternal {
- fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
- Some(match self {
- ThunkInternal::PartialExpr(e) => {
- ThunkInternal::PartialExpr(e.shift(delta, var)?)
- }
- ThunkInternal::ValueF(m, v) => {
- ThunkInternal::ValueF(*m, v.shift(delta, var)?)
- }
- })
- }
-}
-
-impl Shift for TypedThunk {
- fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
- Some(TypedThunk(self.0.shift(delta, var)?))
- }
-}
-
-impl Shift for TypedThunkInternal {
- fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
- Some(TypedThunkInternal {
- internal: self.internal.shift(delta, var)?,
- typ: self.typ.shift(delta, var)?,
- })
- }
-}
-
-impl Subst<Typed> for Thunk {
- fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
- Thunk(self.0.subst_shift(var, val))
- }
-}
-
-impl Subst<Typed> for ThunkInternal {
- fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
- match self {
- ThunkInternal::PartialExpr(e) => {
- ThunkInternal::PartialExpr(e.subst_shift(var, val))
- }
- ThunkInternal::ValueF(_, v) => {
- // The resulting value may not stay in normal form after substitution
- ThunkInternal::ValueF(WHNF, v.subst_shift(var, val))
- }
- }
- }
-}
-
-impl Subst<Typed> for TypedThunkInternal {
- fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
- TypedThunkInternal {
- internal: self.internal.subst_shift(var, val),
- typ: self.typ.subst_shift(var, val),
- }
- }
-}
-
-impl Subst<Typed> for TypedThunk {
- fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
- TypedThunk(self.0.subst_shift(var, val))
- }
-}
-
-impl std::cmp::PartialEq for Thunk {
- fn eq(&self, other: &Self) -> bool {
- *self.as_valuef() == *other.as_valuef()
- }
-}
-impl std::cmp::Eq for Thunk {}
-
-impl std::cmp::PartialEq for TypedThunk {
- fn eq(&self, other: &Self) -> bool {
- self.to_valuef() == other.to_valuef()
- }
-}
-impl std::cmp::Eq for TypedThunk {}
-
-impl std::fmt::Debug for Thunk {
- fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
- let b: &ThunkInternal = &self.as_internal();
- match b {
- ThunkInternal::ValueF(m, v) => {
- f.debug_tuple(&format!("Thunk@{:?}", m)).field(v).finish()
- }
- ThunkInternal::PartialExpr(e) => {
- f.debug_tuple("Thunk@PartialExpr").field(e).finish()
- }
- }
- }
-}
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),
- ),
}
}
}
diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs
new file mode 100644
index 0000000..bea2e2e
--- /dev/null
+++ b/dhall/src/core/valuef.rs
@@ -0,0 +1,405 @@
+use std::collections::HashMap;
+
+use dhall_syntax::{
+ rc, Builtin, Const, ExprF, Integer, InterpolatedTextContents, Label,
+ NaiveDouble, Natural,
+};
+
+use crate::core::value::{TypedValue, Value};
+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 Values, which are partially evaluated expressions that are normalized
+/// on-demand. 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
+/// 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, TypedValue, Value),
+ Pi(AlphaLabel, TypedValue, TypedValue),
+ // Invariant: 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(TypedValue),
+ NEOptionalLit(Value),
+ // EmptyListLit(t) means `[] : List t`, not `[] : t`
+ EmptyListLit(TypedValue),
+ NEListLit(Vec<Value>),
+ RecordLit(HashMap<Label, Value>),
+ RecordType(HashMap<Label, TypedValue>),
+ UnionType(HashMap<Label, Option<TypedValue>>),
+ UnionConstructor(Label, HashMap<Label, Option<TypedValue>>),
+ UnionLit(Label, Value, HashMap<Label, Option<TypedValue>>),
+ // Invariant: this must not contain interpolations that are themselves TextLits, and
+ // contiguous text values must be merged.
+ TextLit(Vec<InterpolatedTextContents<Value>>),
+ Equivalence(TypedValue, TypedValue),
+ // Invariant: this must not contain a value captured by one of the variants above.
+ PartialExpr(ExprF<Value, Normalized>),
+}
+
+impl ValueF {
+ pub(crate) fn into_value(self) -> Value {
+ Value::from_valuef(self)
+ }
+
+ /// Convert the value to a fully normalized syntactic expression
+ pub(crate) fn normalize_to_expr(&self) -> OutputSubExpr {
+ self.normalize_to_expr_maybe_alpha(false)
+ }
+ /// 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 {
+ 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
+ }
+ 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)))
+ }
+ 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()))
+ }
+ 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(),
+ ))
+ }
+ 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),
+ )),
+ ValueF::PartialExpr(e) => {
+ rc(e.map_ref(|v| v.normalize_to_expr_maybe_alpha(alpha)))
+ }
+ }
+ }
+
+ 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() {
+ 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();
+ });
+ }
+ }
+ }
+
+ /// Apply to a value
+ pub(crate) fn app(self, val: ValueF) -> ValueF {
+ self.app_valuef(val)
+ }
+
+ /// Apply to a value
+ pub(crate) fn app_valuef(self, val: ValueF) -> ValueF {
+ self.app_value(val.into_value())
+ }
+
+ /// Apply to a thunk
+ pub fn app_value(self, th: Value) -> ValueF {
+ Value::from_valuef(self).app_value(th)
+ }
+
+ pub fn from_builtin(b: Builtin) -> ValueF {
+ ValueF::AppliedBuiltin(b, vec![])
+ }
+}
+
+impl Shift for ValueF {
+ 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)?)
+ }
+ 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<Typed> for ValueF {
+ 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))
+ }
+ 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/phase/mod.rs b/dhall/src/phase/mod.rs
index 7e74f95..c18f976 100644
--- a/dhall/src/phase/mod.rs
+++ b/dhall/src/phase/mod.rs
@@ -4,8 +4,8 @@ use std::path::Path;
use dhall_syntax::{Const, SubExpr};
-use crate::core::thunk::{Thunk, TypedThunk};
-use crate::core::value::ValueF;
+use crate::core::value::{TypedValue, Value};
+use crate::core::valuef::ValueF;
use crate::core::var::{AlphaVar, Shift, Subst};
use crate::error::{EncodeError, Error, ImportError, TypeError};
@@ -33,7 +33,7 @@ pub struct Resolved(ResolvedSubExpr);
/// A typed expression
#[derive(Debug, Clone)]
-pub struct Typed(TypedThunk);
+pub struct Typed(TypedValue);
/// A normalized expression.
///
@@ -92,19 +92,19 @@ impl Typed {
Normalized(self)
}
- pub(crate) fn from_thunk_and_type(th: Thunk, t: Type) -> Self {
- Typed(TypedThunk::from_thunk_and_type(th, t))
+ pub(crate) fn from_value_and_type(th: Value, t: Type) -> Self {
+ Typed(TypedValue::from_value_and_type(th, t))
}
- pub(crate) fn from_thunk_untyped(th: Thunk) -> Self {
- Typed(TypedThunk::from_thunk_untyped(th))
+ pub(crate) fn from_value_untyped(th: Value) -> Self {
+ Typed(TypedValue::from_value_untyped(th))
}
pub(crate) fn from_const(c: Const) -> Self {
- Typed(TypedThunk::from_const(c))
+ Typed(TypedValue::from_const(c))
}
pub fn from_valuef_and_type(v: ValueF, t: Type) -> Self {
- Typed(TypedThunk::from_valuef_and_type(v, t))
+ Typed(TypedValue::from_valuef_and_type(v, t))
}
- pub(crate) fn from_typethunk(th: TypedThunk) -> Self {
+ pub(crate) fn from_typedvalue(th: TypedValue) -> Self {
Typed(th)
}
pub fn const_type() -> Self {
@@ -120,8 +120,8 @@ impl Typed {
pub(crate) fn to_expr_alpha(&self) -> NormalizedSubExpr {
self.0.to_expr_alpha()
}
- pub fn to_thunk(&self) -> Thunk {
- self.0.to_thunk()
+ pub fn to_value(&self) -> Value {
+ self.0.to_value()
}
// Deprecated
pub fn to_type(&self) -> Type {
@@ -131,7 +131,7 @@ impl Typed {
pub(crate) fn into_type(self) -> Type {
self
}
- pub(crate) fn into_typethunk(self) -> TypedThunk {
+ pub(crate) fn into_typedvalue(self) -> TypedValue {
self.0
}
pub(crate) fn to_normalized(&self) -> Normalized {
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index da54726..93f2528 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -5,8 +5,8 @@ use dhall_syntax::{
NaiveDouble,
};
-use crate::core::thunk::{Thunk, TypedThunk};
-use crate::core::value::ValueF;
+use crate::core::value::{TypedValue, Value};
+use crate::core::valuef::ValueF;
use crate::core::var::{Shift, Subst};
use crate::phase::{Normalized, NormalizedSubExpr, Typed};
@@ -20,45 +20,45 @@ macro_rules! make_closure {
Label::from(stringify!($var)).into(),
$n
);
- ValueF::Var(var).into_thunk()
+ ValueF::Var(var).into_value()
}};
// Warning: assumes that $ty, as a dhall value, has type `Type`
(λ($var:ident : $($ty:tt)*) -> $($rest:tt)*) => {
ValueF::Lam(
Label::from(stringify!($var)).into(),
- TypedThunk::from_thunk_simple_type(
+ TypedValue::from_value_simple_type(
make_closure!($($ty)*),
),
make_closure!($($rest)*),
- ).into_thunk()
+ ).into_value()
};
- (Natural) => { ValueF::from_builtin(Builtin::Natural).into_thunk() };
+ (Natural) => { ValueF::from_builtin(Builtin::Natural).into_value() };
(List $($rest:tt)*) => {
ValueF::from_builtin(Builtin::List)
- .app_thunk(make_closure!($($rest)*))
- .into_thunk()
+ .app_value(make_closure!($($rest)*))
+ .into_value()
};
(Some $($rest:tt)*) => {
- ValueF::NEOptionalLit(make_closure!($($rest)*)).into_thunk()
+ ValueF::NEOptionalLit(make_closure!($($rest)*)).into_value()
};
(1 + $($rest:tt)*) => {
ValueF::PartialExpr(ExprF::BinOp(
dhall_syntax::BinOp::NaturalPlus,
make_closure!($($rest)*),
- Thunk::from_valuef(ValueF::NaturalLit(1)),
- )).into_thunk()
+ Value::from_valuef(ValueF::NaturalLit(1)),
+ )).into_value()
};
([ $($head:tt)* ] # $($tail:tt)*) => {
ValueF::PartialExpr(ExprF::BinOp(
dhall_syntax::BinOp::ListAppend,
- ValueF::NEListLit(vec![make_closure!($($head)*)]).into_thunk(),
+ ValueF::NEListLit(vec![make_closure!($($head)*)]).into_value(),
make_closure!($($tail)*),
- )).into_thunk()
+ )).into_value()
};
}
#[allow(clippy::cognitive_complexity)]
-pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> ValueF {
+pub(crate) fn apply_builtin(b: Builtin, args: Vec<Value>) -> ValueF {
use dhall_syntax::Builtin::*;
use ValueF::*;
@@ -66,7 +66,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> ValueF {
let ret = match (b, args.as_slice()) {
(OptionalNone, [t, r..]) => Ok((
r,
- EmptyOptionalLit(TypedThunk::from_thunk_simple_type(t.clone())),
+ EmptyOptionalLit(TypedValue::from_value_simple_type(t.clone())),
)),
(NaturalIsZero, [n, r..]) => match &*n.as_valuef() {
NaturalLit(n) => Ok((r, BoolLit(*n == 0))),
@@ -189,10 +189,10 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> ValueF {
let mut kts = HashMap::new();
kts.insert(
"index".into(),
- TypedThunk::from_valuef(ValueF::from_builtin(Natural)),
+ TypedValue::from_valuef(ValueF::from_builtin(Natural)),
);
kts.insert("value".into(), t.clone());
- Ok((r, EmptyListLit(TypedThunk::from_valuef(RecordType(kts)))))
+ Ok((r, EmptyListLit(TypedValue::from_valuef(RecordType(kts)))))
}
NEListLit(xs) => {
let xs = xs
@@ -201,9 +201,9 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> ValueF {
.map(|(i, e)| {
let i = NaturalLit(i);
let mut kvs = HashMap::new();
- kvs.insert("index".into(), Thunk::from_valuef(i));
+ kvs.insert("index".into(), Value::from_valuef(i));
kvs.insert("value".into(), e.clone());
- Thunk::from_valuef(RecordLit(kvs))
+ Value::from_valuef(RecordLit(kvs))
})
.collect();
Ok((r, NEListLit(xs)))
@@ -222,8 +222,8 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> ValueF {
}
_ => Ok((
r,
- f.app_val(ValueF::from_builtin(List).app_thunk(t.clone()))
- .app_thunk({
+ f.app_valuef(ValueF::from_builtin(List).app_value(t.clone()))
+ .app_value({
// Move `t` under new `x` variable
let t1 = t.under_binder(Label::from("x"));
make_closure!(
@@ -232,9 +232,9 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> ValueF {
[ var(x, 1) ] # var(xs, 0)
)
})
- .app_val(EmptyListLit(TypedThunk::from_thunk_simple_type(
- t.clone(),
- ))),
+ .app_valuef(EmptyListLit(
+ TypedValue::from_value_simple_type(t.clone()),
+ )),
)),
},
(ListFold, [_, l, _, cons, nil, r..]) => match &*l.as_valuef() {
@@ -244,9 +244,9 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> ValueF {
for x in xs.iter().rev() {
v = cons
.clone()
- .app_thunk(x.clone())
- .app_thunk(v)
- .into_thunk();
+ .app_value(x.clone())
+ .app_value(v)
+ .into_value();
}
Ok((r, v.to_valuef()))
}
@@ -264,17 +264,19 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> ValueF {
}
_ => Ok((
r,
- f.app_val(ValueF::from_builtin(Optional).app_thunk(t.clone()))
- .app_thunk(make_closure!(λ(x: #t) -> Some var(x, 0)))
- .app_val(EmptyOptionalLit(
- TypedThunk::from_thunk_simple_type(t.clone()),
- )),
+ f.app_valuef(
+ ValueF::from_builtin(Optional).app_value(t.clone()),
+ )
+ .app_value(make_closure!(λ(x: #t) -> Some var(x, 0)))
+ .app_valuef(EmptyOptionalLit(
+ TypedValue::from_value_simple_type(t.clone()),
+ )),
)),
},
(OptionalFold, [_, v, _, just, nothing, r..]) => {
match &*v.as_valuef() {
EmptyOptionalLit(_) => Ok((r, nothing.to_valuef())),
- NEOptionalLit(x) => Ok((r, just.app_thunk(x.clone()))),
+ NEOptionalLit(x) => Ok((r, just.app_value(x.clone()))),
_ => Err(()),
}
}
@@ -290,9 +292,9 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> ValueF {
}
_ => Ok((
r,
- f.app_val(ValueF::from_builtin(Natural))
- .app_thunk(make_closure!(λ(x : Natural) -> 1 + var(x, 0)))
- .app_val(NaturalLit(0)),
+ f.app_valuef(ValueF::from_builtin(Natural))
+ .app_value(make_closure!(λ(x : Natural) -> 1 + var(x, 0)))
+ .app_valuef(NaturalLit(0)),
)),
},
(NaturalFold, [n, t, succ, zero, r..]) => match &*n.as_valuef() {
@@ -300,10 +302,10 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> ValueF {
NaturalLit(n) => {
let fold = ValueF::from_builtin(NaturalFold)
.app(NaturalLit(n - 1))
- .app_thunk(t.clone())
- .app_thunk(succ.clone())
- .app_thunk(zero.clone());
- Ok((r, succ.app_val(fold)))
+ .app_value(t.clone())
+ .app_value(succ.clone())
+ .app_value(zero.clone());
+ Ok((r, succ.app_valuef(fold)))
}
_ => Err(()),
},
@@ -313,7 +315,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> ValueF {
Ok((unconsumed_args, mut v)) => {
let n_consumed_args = args.len() - unconsumed_args.len();
for x in args.into_iter().skip(n_consumed_args) {
- v = v.app_thunk(x);
+ v = v.app_value(x);
}
v
}
@@ -321,13 +323,13 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec<Thunk>) -> ValueF {
}
}
-pub(crate) fn apply_any(f: Thunk, a: Thunk) -> ValueF {
- let fallback = |f: Thunk, a: Thunk| ValueF::PartialExpr(ExprF::App(f, a));
+pub(crate) fn apply_any(f: Value, a: Value) -> ValueF {
+ let fallback = |f: Value, a: Value| ValueF::PartialExpr(ExprF::App(f, a));
let f_borrow = f.as_valuef();
match &*f_borrow {
ValueF::Lam(x, _, e) => {
- let val = Typed::from_thunk_untyped(a);
+ let val = Typed::from_value_untyped(a);
e.subst_shift(&x.into(), &val).to_valuef()
}
ValueF::AppliedBuiltin(b, args) => {
@@ -346,15 +348,15 @@ pub(crate) fn apply_any(f: Thunk, a: Thunk) -> ValueF {
}
pub(crate) fn squash_textlit(
- elts: impl Iterator<Item = InterpolatedTextContents<Thunk>>,
-) -> Vec<InterpolatedTextContents<Thunk>> {
+ elts: impl Iterator<Item = InterpolatedTextContents<Value>>,
+) -> Vec<InterpolatedTextContents<Value>> {
use std::mem::replace;
use InterpolatedTextContents::{Expr, Text};
fn inner(
- elts: impl Iterator<Item = InterpolatedTextContents<Thunk>>,
+ elts: impl Iterator<Item = InterpolatedTextContents<Value>>,
crnt_str: &mut String,
- ret: &mut Vec<InterpolatedTextContents<Thunk>>,
+ ret: &mut Vec<InterpolatedTextContents<Value>>,
) {
for contents in elts {
match contents {
@@ -390,9 +392,9 @@ pub(crate) fn squash_textlit(
// Small helper enum to avoid repetition
enum Ret<'a> {
ValueF(ValueF),
- Thunk(Thunk),
- ThunkRef(&'a Thunk),
- Expr(ExprF<Thunk, Normalized>),
+ Value(Value),
+ ValueRef(&'a Value),
+ Expr(ExprF<Value, Normalized>),
}
/// Performs an intersection of two HashMaps.
@@ -508,7 +510,7 @@ where
kvs
}
-fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option<Ret<'a>> {
+fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> {
use BinOp::{
BoolAnd, BoolEQ, BoolNE, BoolOr, Equivalence, ListAppend, NaturalPlus,
NaturalTimes, RecursiveRecordMerge, RecursiveRecordTypeMerge,
@@ -521,46 +523,46 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option<Ret<'a>> {
let x_borrow = x.as_valuef();
let y_borrow = y.as_valuef();
Some(match (o, &*x_borrow, &*y_borrow) {
- (BoolAnd, BoolLit(true), _) => Ret::ThunkRef(y),
- (BoolAnd, _, BoolLit(true)) => Ret::ThunkRef(x),
+ (BoolAnd, BoolLit(true), _) => Ret::ValueRef(y),
+ (BoolAnd, _, BoolLit(true)) => Ret::ValueRef(x),
(BoolAnd, BoolLit(false), _) => Ret::ValueF(BoolLit(false)),
(BoolAnd, _, BoolLit(false)) => Ret::ValueF(BoolLit(false)),
- (BoolAnd, _, _) if x == y => Ret::ThunkRef(x),
+ (BoolAnd, _, _) if x == y => Ret::ValueRef(x),
(BoolOr, BoolLit(true), _) => Ret::ValueF(BoolLit(true)),
(BoolOr, _, BoolLit(true)) => Ret::ValueF(BoolLit(true)),
- (BoolOr, BoolLit(false), _) => Ret::ThunkRef(y),
- (BoolOr, _, BoolLit(false)) => Ret::ThunkRef(x),
- (BoolOr, _, _) if x == y => Ret::ThunkRef(x),
- (BoolEQ, BoolLit(true), _) => Ret::ThunkRef(y),
- (BoolEQ, _, BoolLit(true)) => Ret::ThunkRef(x),
+ (BoolOr, BoolLit(false), _) => Ret::ValueRef(y),
+ (BoolOr, _, BoolLit(false)) => Ret::ValueRef(x),
+ (BoolOr, _, _) if x == y => Ret::ValueRef(x),
+ (BoolEQ, BoolLit(true), _) => Ret::ValueRef(y),
+ (BoolEQ, _, BoolLit(true)) => Ret::ValueRef(x),
(BoolEQ, BoolLit(x), BoolLit(y)) => Ret::ValueF(BoolLit(x == y)),
(BoolEQ, _, _) if x == y => Ret::ValueF(BoolLit(true)),
- (BoolNE, BoolLit(false), _) => Ret::ThunkRef(y),
- (BoolNE, _, BoolLit(false)) => Ret::ThunkRef(x),
+ (BoolNE, BoolLit(false), _) => Ret::ValueRef(y),
+ (BoolNE, _, BoolLit(false)) => Ret::ValueRef(x),
(BoolNE, BoolLit(x), BoolLit(y)) => Ret::ValueF(BoolLit(x != y)),
(BoolNE, _, _) if x == y => Ret::ValueF(BoolLit(false)),
- (NaturalPlus, NaturalLit(0), _) => Ret::ThunkRef(y),
- (NaturalPlus, _, NaturalLit(0)) => Ret::ThunkRef(x),
+ (NaturalPlus, NaturalLit(0), _) => Ret::ValueRef(y),
+ (NaturalPlus, _, NaturalLit(0)) => Ret::ValueRef(x),
(NaturalPlus, NaturalLit(x), NaturalLit(y)) => {
Ret::ValueF(NaturalLit(x + y))
}
(NaturalTimes, NaturalLit(0), _) => Ret::ValueF(NaturalLit(0)),
(NaturalTimes, _, NaturalLit(0)) => Ret::ValueF(NaturalLit(0)),
- (NaturalTimes, NaturalLit(1), _) => Ret::ThunkRef(y),
- (NaturalTimes, _, NaturalLit(1)) => Ret::ThunkRef(x),
+ (NaturalTimes, NaturalLit(1), _) => Ret::ValueRef(y),
+ (NaturalTimes, _, NaturalLit(1)) => Ret::ValueRef(x),
(NaturalTimes, NaturalLit(x), NaturalLit(y)) => {
Ret::ValueF(NaturalLit(x * y))
}
- (ListAppend, EmptyListLit(_), _) => Ret::ThunkRef(y),
- (ListAppend, _, EmptyListLit(_)) => Ret::ThunkRef(x),
+ (ListAppend, EmptyListLit(_), _) => Ret::ValueRef(y),
+ (ListAppend, _, EmptyListLit(_)) => Ret::ValueRef(x),
(ListAppend, NEListLit(xs), NEListLit(ys)) => Ret::ValueF(NEListLit(
xs.iter().chain(ys.iter()).cloned().collect(),
)),
- (TextAppend, TextLit(x), _) if x.is_empty() => Ret::ThunkRef(y),
- (TextAppend, _, TextLit(y)) if y.is_empty() => Ret::ThunkRef(x),
+ (TextAppend, TextLit(x), _) if x.is_empty() => Ret::ValueRef(y),
+ (TextAppend, _, TextLit(y)) if y.is_empty() => Ret::ValueRef(x),
(TextAppend, TextLit(x), TextLit(y)) => Ret::ValueF(TextLit(
squash_textlit(x.iter().chain(y.iter()).cloned()),
)),
@@ -580,10 +582,10 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option<Ret<'a>> {
}
(RightBiasedRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => {
- Ret::ThunkRef(x)
+ Ret::ValueRef(x)
}
(RightBiasedRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => {
- Ret::ThunkRef(y)
+ Ret::ValueRef(y)
}
(RightBiasedRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => {
let mut kvs = kvs2.clone();
@@ -595,14 +597,14 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option<Ret<'a>> {
}
(RecursiveRecordMerge, _, RecordLit(kvs)) if kvs.is_empty() => {
- Ret::ThunkRef(x)
+ Ret::ValueRef(x)
}
(RecursiveRecordMerge, RecordLit(kvs), _) if kvs.is_empty() => {
- Ret::ThunkRef(y)
+ Ret::ValueRef(y)
}
(RecursiveRecordMerge, RecordLit(kvs1), RecordLit(kvs2)) => {
let kvs = merge_maps(kvs1, kvs2, |v1, v2| {
- Thunk::from_partial_expr(ExprF::BinOp(
+ Value::from_partial_expr(ExprF::BinOp(
RecursiveRecordMerge,
v1.clone(),
v2.clone(),
@@ -612,18 +614,18 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option<Ret<'a>> {
}
(RecursiveRecordTypeMerge, _, RecordType(kvs)) if kvs.is_empty() => {
- Ret::ThunkRef(x)
+ Ret::ValueRef(x)
}
(RecursiveRecordTypeMerge, RecordType(kvs), _) if kvs.is_empty() => {
- Ret::ThunkRef(y)
+ Ret::ValueRef(y)
}
(RecursiveRecordTypeMerge, RecordType(kvs1), RecordType(kvs2)) => {
let kvs = merge_maps(kvs1, kvs2, |v1, v2| {
- TypedThunk::from_thunk_untyped(Thunk::from_partial_expr(
+ TypedValue::from_value_untyped(Value::from_partial_expr(
ExprF::BinOp(
RecursiveRecordTypeMerge,
- v1.to_thunk(),
- v2.to_thunk(),
+ v1.to_value(),
+ v2.to_value(),
),
))
});
@@ -631,15 +633,15 @@ fn apply_binop<'a>(o: BinOp, x: &'a Thunk, y: &'a Thunk) -> Option<Ret<'a>> {
}
(Equivalence, _, _) => Ret::ValueF(ValueF::Equivalence(
- TypedThunk::from_thunk_simple_type(x.clone()),
- TypedThunk::from_thunk_simple_type(y.clone()),
+ TypedValue::from_value_simple_type(x.clone()),
+ TypedValue::from_value_simple_type(y.clone()),
)),
_ => return None,
})
}
-pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> ValueF {
+pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF {
use ValueF::{
AppliedBuiltin, BoolLit, DoubleLit, EmptyListLit, IntegerLit, Lam,
NEListLit, NEOptionalLit, NaturalLit, Pi, RecordLit, RecordType,
@@ -652,21 +654,21 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> ValueF {
),
ExprF::Embed(_) => unreachable!(),
ExprF::Var(_) => unreachable!(),
- ExprF::Annot(x, _) => Ret::Thunk(x),
+ ExprF::Annot(x, _) => Ret::Value(x),
ExprF::Assert(_) => Ret::Expr(expr),
ExprF::Lam(x, t, e) => {
- Ret::ValueF(Lam(x.into(), TypedThunk::from_thunk_untyped(t), e))
+ Ret::ValueF(Lam(x.into(), TypedValue::from_value_untyped(t), e))
}
ExprF::Pi(x, t, e) => Ret::ValueF(Pi(
x.into(),
- TypedThunk::from_thunk_untyped(t),
- TypedThunk::from_thunk_untyped(e),
+ TypedValue::from_value_untyped(t),
+ TypedValue::from_value_untyped(e),
)),
ExprF::Let(x, _, v, b) => {
- let v = Typed::from_thunk_untyped(v);
- Ret::Thunk(b.subst_shift(&x.into(), &v))
+ let v = Typed::from_value_untyped(v);
+ Ret::Value(b.subst_shift(&x.into(), &v))
}
- ExprF::App(v, a) => Ret::ValueF(v.app_thunk(a)),
+ ExprF::App(v, a) => Ret::ValueF(v.app_value(a)),
ExprF::Builtin(b) => Ret::ValueF(ValueF::from_builtin(b)),
ExprF::Const(c) => Ret::ValueF(ValueF::Const(c)),
ExprF::BoolLit(b) => Ret::ValueF(BoolLit(b)),
@@ -680,7 +682,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> ValueF {
match &*t_borrow {
AppliedBuiltin(Builtin::List, args) if args.len() == 1 => {
Ret::ValueF(EmptyListLit(
- TypedThunk::from_thunk_simple_type(args[0].clone()),
+ TypedValue::from_value_simple_type(args[0].clone()),
))
}
_ => {
@@ -697,12 +699,12 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> ValueF {
}
ExprF::RecordType(kts) => Ret::ValueF(RecordType(
kts.into_iter()
- .map(|(k, t)| (k, TypedThunk::from_thunk_untyped(t)))
+ .map(|(k, t)| (k, TypedValue::from_value_untyped(t)))
.collect(),
)),
ExprF::UnionType(kts) => Ret::ValueF(UnionType(
kts.into_iter()
- .map(|(k, t)| (k, t.map(|t| TypedThunk::from_thunk_untyped(t))))
+ .map(|(k, t)| (k, t.map(|t| TypedValue::from_value_untyped(t))))
.collect(),
)),
ExprF::TextLit(elts) => {
@@ -710,7 +712,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> ValueF {
let elts: Vec<_> = squash_textlit(elts.into_iter());
// Simplify bare interpolation
if let [Expr(th)] = elts.as_slice() {
- Ret::Thunk(th.clone())
+ Ret::Value(th.clone())
} else {
Ret::ValueF(TextLit(elts))
}
@@ -718,15 +720,15 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> ValueF {
ExprF::BoolIf(ref b, ref e1, ref e2) => {
let b_borrow = b.as_valuef();
match &*b_borrow {
- BoolLit(true) => Ret::ThunkRef(e1),
- BoolLit(false) => Ret::ThunkRef(e2),
+ BoolLit(true) => Ret::ValueRef(e1),
+ BoolLit(false) => Ret::ValueRef(e2),
_ => {
let e1_borrow = e1.as_valuef();
let e2_borrow = e2.as_valuef();
match (&*e1_borrow, &*e2_borrow) {
// Simplify `if b then True else False`
- (BoolLit(true), BoolLit(false)) => Ret::ThunkRef(b),
- _ if e1 == e2 => Ret::ThunkRef(e1),
+ (BoolLit(true), BoolLit(false)) => Ret::ValueRef(b),
+ _ if e1 == e2 => Ret::ValueRef(e1),
_ => {
drop(b_borrow);
drop(e1_borrow);
@@ -765,7 +767,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> ValueF {
let v_borrow = v.as_valuef();
match &*v_borrow {
RecordLit(kvs) => match kvs.get(l) {
- Some(r) => Ret::Thunk(r.clone()),
+ Some(r) => Ret::Value(r.clone()),
None => {
drop(v_borrow);
Ret::Expr(expr)
@@ -786,7 +788,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> ValueF {
let variant_borrow = variant.as_valuef();
match (&*handlers_borrow, &*variant_borrow) {
(RecordLit(kvs), UnionConstructor(l, _)) => match kvs.get(l) {
- Some(h) => Ret::Thunk(h.clone()),
+ Some(h) => Ret::Value(h.clone()),
None => {
drop(handlers_borrow);
drop(variant_borrow);
@@ -794,7 +796,7 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> ValueF {
}
},
(RecordLit(kvs), UnionLit(l, v, _)) => match kvs.get(l) {
- Some(h) => Ret::ValueF(h.app_thunk(v.clone())),
+ Some(h) => Ret::ValueF(h.app_value(v.clone())),
None => {
drop(handlers_borrow);
drop(variant_borrow);
@@ -812,8 +814,8 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Thunk, Normalized>) -> ValueF {
match ret {
Ret::ValueF(v) => v,
- Ret::Thunk(th) => th.to_valuef(),
- Ret::ThunkRef(th) => th.to_valuef(),
+ Ret::Value(th) => th.to_valuef(),
+ Ret::ValueRef(th) => th.to_valuef(),
Ret::Expr(expr) => ValueF::PartialExpr(expr),
}
}
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index 8d7a3bc..4154afe 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -5,8 +5,8 @@ use dhall_syntax::{
};
use crate::core::context::TypecheckContext;
-use crate::core::thunk::{Thunk, TypedThunk};
-use crate::core::value::ValueF;
+use crate::core::value::{TypedValue, Value};
+use crate::core::valuef::ValueF;
use crate::core::var::{Shift, Subst};
use crate::error::{TypeError, TypeMessage};
use crate::phase::{Normalized, Resolved, Type, Typed};
@@ -42,13 +42,13 @@ fn tck_pi_type(
let k = function_check(ka, kb);
- Ok(Typed::from_thunk_and_type(
+ Ok(Typed::from_value_and_type(
ValueF::Pi(
x.into(),
- TypedThunk::from_type(tx),
- TypedThunk::from_type(te),
+ TypedValue::from_type(tx),
+ TypedValue::from_type(te),
)
- .into_thunk(),
+ .into_value(),
Type::from_const(k),
))
}
@@ -80,15 +80,15 @@ fn tck_record_type(
return Err(TypeError::new(ctx, RecordTypeDuplicateField))
}
Entry::Vacant(_) => {
- entry.or_insert_with(|| TypedThunk::from_type(t.clone()))
+ entry.or_insert_with(|| TypedValue::from_type(t.clone()))
}
};
}
// An empty record type has type Type
let k = k.unwrap_or(dhall_syntax::Const::Type);
- Ok(Typed::from_thunk_and_type(
- ValueF::RecordType(new_kts).into_thunk(),
+ Ok(Typed::from_value_and_type(
+ ValueF::RecordType(new_kts).into_value(),
Type::from_const(k),
))
}
@@ -122,7 +122,7 @@ fn tck_union_type(
return Err(TypeError::new(ctx, UnionTypeDuplicateField))
}
Entry::Vacant(_) => entry.or_insert_with(|| {
- t.as_ref().map(|t| TypedThunk::from_type(t.clone()))
+ t.as_ref().map(|t| TypedValue::from_type(t.clone()))
}),
};
}
@@ -131,8 +131,8 @@ fn tck_union_type(
// an union type with only unary variants also has type Type
let k = k.unwrap_or(dhall_syntax::Const::Type);
- Ok(Typed::from_thunk_and_type(
- ValueF::UnionType(new_kts).into_thunk(),
+ Ok(Typed::from_value_and_type(
+ ValueF::UnionType(new_kts).into_value(),
Type::from_const(k),
))
}
@@ -337,12 +337,12 @@ fn type_with(
let b = type_with(&ctx2, b.clone())?;
let v = ValueF::Lam(
x.clone().into(),
- TypedThunk::from_type(tx.clone()),
- b.to_thunk(),
+ TypedValue::from_type(tx.clone()),
+ b.to_value(),
);
let tb = b.get_type()?.into_owned();
let t = tck_pi_type(ctx, x.clone(), tx, tb)?.to_type();
- Typed::from_thunk_and_type(Thunk::from_valuef(v), t)
+ Typed::from_value_and_type(Value::from_valuef(v), t)
}
Pi(x, ta, tb) => {
let ta = mktype(ctx, ta.clone())?;
@@ -380,9 +380,9 @@ fn type_with(
let ret = type_last_layer(ctx, &expr)?;
match ret {
RetTypeOnly(typ) => {
- let expr = expr.map_ref(|typed| typed.to_thunk());
- Typed::from_thunk_and_type(
- Thunk::from_partial_expr(expr),
+ let expr = expr.map_ref(|typed| typed.to_value());
+ Typed::from_value_and_type(
+ Value::from_partial_expr(expr),
typ,
)
}
@@ -505,10 +505,10 @@ fn type_last_layer(
}
Ok(RetTypeOnly(
- Typed::from_thunk_and_type(
+ Typed::from_value_and_type(
ValueF::from_builtin(dhall_syntax::Builtin::List)
.app(t.to_valuef())
- .into_thunk(),
+ .into_value(),
Typed::from_const(Type),
)
.to_type(),
@@ -524,10 +524,10 @@ fn type_last_layer(
}
Ok(RetTypeOnly(
- Typed::from_thunk_and_type(
+ Typed::from_value_and_type(
ValueF::from_builtin(dhall_syntax::Builtin::Optional)
.app(t.to_valuef())
- .into_thunk(),
+ .into_value(),
Typed::from_const(Type).into_type(),
)
.to_type(),
@@ -662,8 +662,8 @@ fn type_last_layer(
// records of records when merging.
fn combine_record_types(
ctx: &TypecheckContext,
- kts_l: HashMap<Label, TypedThunk>,
- kts_r: HashMap<Label, TypedThunk>,
+ kts_l: HashMap<Label, TypedValue>,
+ kts_r: HashMap<Label, TypedValue>,
) -> Result<Typed, TypeError> {
use crate::phase::normalize::outer_join;
@@ -671,8 +671,8 @@ fn type_last_layer(
// are records themselves, then we hit the recursive case.
// Otherwise we have a field collision.
let combine = |k: &Label,
- inner_l: &TypedThunk,
- inner_r: &TypedThunk|
+ inner_l: &TypedValue,
+ inner_r: &TypedValue|
-> Result<Typed, TypeError> {
match (inner_l.to_valuef(), inner_r.to_valuef()) {
(
@@ -690,7 +690,7 @@ fn type_last_layer(
let kts: HashMap<Label, Result<Typed, TypeError>> = outer_join(
|l| Ok(l.to_type()),
|r| Ok(r.to_type()),
- |k: &Label, l: &TypedThunk, r: &TypedThunk| {
+ |k: &Label, l: &TypedValue, r: &TypedValue| {
combine(k, l, r)
},
&kts_l,
@@ -735,8 +735,8 @@ fn type_last_layer(
// records of records when merging.
fn combine_record_types(
ctx: &TypecheckContext,
- kts_l: HashMap<Label, TypedThunk>,
- kts_r: HashMap<Label, TypedThunk>,
+ kts_l: HashMap<Label, TypedValue>,
+ kts_r: HashMap<Label, TypedValue>,
) -> Result<Typed, TypeError> {
use crate::phase::normalize::intersection_with_key;
@@ -744,8 +744,8 @@ fn type_last_layer(
// are records themselves, then we hit the recursive case.
// Otherwise we have a field collision.
let combine = |k: &Label,
- kts_l_inner: &TypedThunk,
- kts_r_inner: &TypedThunk|
+ kts_l_inner: &TypedValue,
+ kts_r_inner: &TypedValue|
-> Result<Typed, TypeError> {
match (kts_l_inner.to_valuef(), kts_r_inner.to_valuef()) {
(
@@ -761,7 +761,7 @@ fn type_last_layer(
};
let kts = intersection_with_key(
- |k: &Label, l: &TypedThunk, r: &TypedThunk| {
+ |k: &Label, l: &TypedValue, r: &TypedValue| {
combine(k, l, r)
},
&kts_l,
@@ -989,8 +989,8 @@ fn type_last_layer(
}
Ok(RetTypeOnly(
- Typed::from_thunk_and_type(
- ValueF::RecordType(new_kts).into_thunk(),
+ Typed::from_value_and_type(
+ ValueF::RecordType(new_kts).into_value(),
trecord.get_type()?.into_owned(),
)
.to_type(),
diff --git a/serde_dhall/src/lib.rs b/serde_dhall/src/lib.rs
index 49fd40e..48f311e 100644
--- a/serde_dhall/src/lib.rs
+++ b/serde_dhall/src/lib.rs
@@ -124,8 +124,9 @@ pub use value::Value;
// A Dhall value.
pub mod value {
- use dhall::core::thunk::{Thunk, TypedThunk};
- use dhall::core::value::ValueF as DhallValue;
+ use dhall::core::value::TypedValue as TypedThunk;
+ use dhall::core::value::Value as Thunk;
+ use dhall::core::valuef::ValueF as DhallValue;
use dhall::phase::{NormalizedSubExpr, Parsed, Type, Typed};
use dhall_syntax::Builtin;
@@ -153,8 +154,8 @@ pub mod value {
pub(crate) fn to_expr(&self) -> NormalizedSubExpr {
self.0.to_expr()
}
- pub(crate) fn to_thunk(&self) -> Thunk {
- self.0.to_thunk()
+ pub(crate) fn to_value(&self) -> Thunk {
+ self.0.to_value()
}
pub(crate) fn to_type(&self) -> Type {
self.0.to_type()
@@ -170,12 +171,12 @@ pub mod value {
pub(crate) fn make_optional_type(t: Value) -> Self {
Self::make_simple_type(
DhallValue::from_builtin(Builtin::Optional)
- .app_thunk(t.to_thunk()),
+ .app_value(t.to_value()),
)
}
pub(crate) fn make_list_type(t: Value) -> Self {
Self::make_simple_type(
- DhallValue::from_builtin(Builtin::List).app_thunk(t.to_thunk()),
+ DhallValue::from_builtin(Builtin::List).app_value(t.to_value()),
)
}
// Made public for the StaticType derive macro
@@ -185,7 +186,7 @@ pub mod value {
) -> Self {
Self::make_simple_type(DhallValue::RecordType(
kts.map(|(k, t)| {
- (k.into(), TypedThunk::from_thunk_simple_type(t.to_thunk()))
+ (k.into(), TypedThunk::from_value_simple_type(t.to_value()))
})
.collect(),
))
@@ -199,7 +200,7 @@ pub mod value {
(
k.into(),
t.map(|t| {
- TypedThunk::from_thunk_simple_type(t.to_thunk())
+ TypedThunk::from_value_simple_type(t.to_value())
}),
)
})