From 6753a1f97bb674d91dd4d42f2ddb25a8119e070d Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 17 Aug 2019 19:00:43 +0200 Subject: s/Thunk/Value/ --- dhall/src/core/context.rs | 14 +- dhall/src/core/mod.rs | 2 +- dhall/src/core/thunk.rs | 406 ------------------------ dhall/src/core/value.rs | 723 ++++++++++++++++++++++--------------------- dhall/src/core/valuef.rs | 405 ++++++++++++++++++++++++ dhall/src/phase/mod.rs | 26 +- dhall/src/phase/normalize.rs | 208 +++++++------ dhall/src/phase/typecheck.rs | 68 ++-- serde_dhall/src/lib.rs | 17 +- 9 files changed, 936 insertions(+), 933 deletions(-) delete mode 100644 dhall/src/core/thunk.rs create mode 100644 dhall/src/core/valuef.rs 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 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), - /// 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, -} - -/// 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>); - -#[derive(Debug, Clone)] -pub struct TypedThunk(Thunk); - -impl ThunkInternal { - fn into_thunk(self, t: Option) -> 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 { - 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 { - 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 { - self.0.borrow() - } - fn as_tinternal_mut(&mut self) -> RefMut { - self.0.borrow_mut() - } - fn as_internal(&self) -> Ref { - Ref::map(self.as_tinternal(), TypedThunkInternal::as_internal) - } - fn as_internal_mut(&self) -> RefMut { - 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 { - 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 { - 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, 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 { - // TODO: avoid clone - match &self.to_valuef() { - ValueF::Const(c) => Some(*c), - _ => None, - } - } - - pub(crate) fn normalize_mut(&mut self) { - self.0.normalize_mut() - } - - pub(crate) fn get_type(&self) -> Result, TypeError> { - self.0.get_type() - } -} - -impl Shift for Thunk { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option { - Some(Thunk(self.0.shift(delta, var)?)) - } -} - -impl Shift for ThunkInternal { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option { - 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 { - Some(TypedThunk(self.0.shift(delta, var)?)) - } -} - -impl Shift for TypedThunkInternal { - fn shift(&self, delta: isize, var: &AlphaVar) -> Option { - Some(TypedThunkInternal { - internal: self.internal.shift(delta, var)?, - typ: self.typ.shift(delta, var)?, - }) - } -} - -impl Subst for Thunk { - fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { - Thunk(self.0.subst_shift(var, val)) - } -} - -impl Subst 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 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 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), - - Var(AlphaVar), - Const(Const), - BoolLit(bool), - NaturalLit(Natural), - IntegerLit(Integer), - DoubleLit(NaiveDouble), - EmptyOptionalLit(TypedThunk), - NEOptionalLit(Thunk), - // EmptyListLit(t) means `[] : List t`, not `[] : t` - EmptyListLit(TypedThunk), - NEListLit(Vec), - RecordLit(HashMap), - RecordType(HashMap), - UnionType(HashMap>), - UnionConstructor(Label, HashMap>), - UnionLit(Label, Thunk, HashMap>), - // Invariant: this must not contain interpolations that are themselves TextLits, and - // contiguous text values must be merged. - TextLit(Vec>), - Equivalence(TypedThunk, TypedThunk), - // Invariant: this must not contain a value captured by one of the variants above. - PartialExpr(ExprF), +use std::borrow::Cow; +use std::cell::{Ref, RefCell, RefMut}; +use std::rc::Rc; + +use dhall_syntax::{Const, ExprF}; + +use crate::core::context::TypecheckContext; +use crate::core::valuef::ValueF; +use crate::core::var::{AlphaVar, Shift, Subst}; +use crate::error::{TypeError, TypeMessage}; +use crate::phase::normalize::{apply_any, normalize_one_layer, OutputSubExpr}; +use crate::phase::typecheck::type_of_const; +use crate::phase::{Normalized, NormalizedSubExpr, Type, Typed}; + +#[derive(Debug, Clone, Copy)] +enum Marker { + /// Weak Head Normal Form, i.e. subexpressions may not be normalized + WHNF, + /// Normal form, i.e. completely normalized + NF, } +use Marker::{NF, WHNF}; -impl ValueF { - pub(crate) fn into_thunk(self) -> Thunk { - Thunk::from_valuef(self) - } +#[derive(Debug, Clone)] +enum ValueInternal { + /// Partially normalized value whose subexpressions have been thunked (this is returned from + /// typechecking). Note that this is different from `ValueF::PartialExpr` because there is no + /// requirement of WHNF here. + PartialExpr(ExprF), + /// Partially normalized value. + /// Invariant: if the marker is `NF`, the value must be fully normalized + ValueF(Marker, ValueF), +} - /// Convert the value to a fully normalized syntactic expression - pub(crate) fn normalize_to_expr(&self) -> OutputSubExpr { - self.normalize_to_expr_maybe_alpha(false) +#[derive(Debug)] +struct TypedValueInternal { + internal: ValueInternal, + typ: Option, +} + +/// Stores a possibly unevaluated value. Gets (partially) normalized on-demand, +/// sharing computation automatically. Uses a RefCell to share computation. +/// Can optionally store a Type from typechecking to preserve type information through +/// normalization. +#[derive(Clone)] +pub struct Value(Rc>); + +#[derive(Debug, Clone)] +pub struct TypedValue(Value); + +impl ValueInternal { + fn into_value(self, t: Option) -> Value { + TypedValueInternal { + internal: self, + typ: t, + } + .into_value() } - /// Convert the value to a fully normalized syntactic expression. Also alpha-normalize - /// if alpha is `true` - pub(crate) fn normalize_to_expr_maybe_alpha( - &self, - alpha: bool, - ) -> OutputSubExpr { + + fn normalize_whnf(&mut self) { match self { - ValueF::Lam(x, t, e) => rc(ExprF::Lam( - x.to_label_maybe_alpha(alpha), - t.normalize_to_expr_maybe_alpha(alpha), - e.normalize_to_expr_maybe_alpha(alpha), - )), - ValueF::AppliedBuiltin(b, args) => { - let mut e = rc(ExprF::Builtin(*b)); - for v in args { - e = rc(ExprF::App( - e, - v.normalize_to_expr_maybe_alpha(alpha), - )); - } - e + ValueInternal::PartialExpr(e) => { + *self = + ValueInternal::ValueF(WHNF, normalize_one_layer(e.clone())) } - ValueF::Pi(x, t, e) => rc(ExprF::Pi( - x.to_label_maybe_alpha(alpha), - t.normalize_to_expr_maybe_alpha(alpha), - e.normalize_to_expr_maybe_alpha(alpha), - )), - ValueF::Var(v) => rc(ExprF::Var(v.to_var(alpha))), - ValueF::Const(c) => rc(ExprF::Const(*c)), - ValueF::BoolLit(b) => rc(ExprF::BoolLit(*b)), - ValueF::NaturalLit(n) => rc(ExprF::NaturalLit(*n)), - ValueF::IntegerLit(n) => rc(ExprF::IntegerLit(*n)), - ValueF::DoubleLit(n) => rc(ExprF::DoubleLit(*n)), - ValueF::EmptyOptionalLit(n) => rc(ExprF::App( - rc(ExprF::Builtin(Builtin::OptionalNone)), - n.normalize_to_expr_maybe_alpha(alpha), - )), - ValueF::NEOptionalLit(n) => { - rc(ExprF::SomeLit(n.normalize_to_expr_maybe_alpha(alpha))) + // Already at least in WHNF + ValueInternal::ValueF(_, _) => {} + } + } + + fn normalize_nf(&mut self) { + match self { + ValueInternal::PartialExpr(_) => { + self.normalize_whnf(); + self.normalize_nf(); } - ValueF::EmptyListLit(n) => rc(ExprF::EmptyListLit(rc(ExprF::App( - rc(ExprF::Builtin(Builtin::List)), - n.normalize_to_expr_maybe_alpha(alpha), - )))), - ValueF::NEListLit(elts) => rc(ExprF::NEListLit( - elts.iter() - .map(|n| n.normalize_to_expr_maybe_alpha(alpha)) - .collect(), - )), - ValueF::RecordLit(kvs) => rc(ExprF::RecordLit( - kvs.iter() - .map(|(k, v)| { - (k.clone(), v.normalize_to_expr_maybe_alpha(alpha)) - }) - .collect(), - )), - ValueF::RecordType(kts) => rc(ExprF::RecordType( - kts.iter() - .map(|(k, v)| { - (k.clone(), v.normalize_to_expr_maybe_alpha(alpha)) - }) - .collect(), - )), - ValueF::UnionType(kts) => rc(ExprF::UnionType( - kts.iter() - .map(|(k, v)| { - ( - k.clone(), - v.as_ref().map(|v| { - v.normalize_to_expr_maybe_alpha(alpha) - }), - ) - }) - .collect(), - )), - ValueF::UnionConstructor(l, kts) => { - let kts = kts - .iter() - .map(|(k, v)| { - ( - k.clone(), - v.as_ref().map(|v| { - v.normalize_to_expr_maybe_alpha(alpha) - }), - ) - }) - .collect(); - rc(ExprF::Field(rc(ExprF::UnionType(kts)), l.clone())) + ValueInternal::ValueF(m @ WHNF, v) => { + v.normalize_mut(); + *m = NF; } - ValueF::UnionLit(l, v, kts) => rc(ExprF::App( - ValueF::UnionConstructor(l.clone(), kts.clone()) - .normalize_to_expr_maybe_alpha(alpha), - v.normalize_to_expr_maybe_alpha(alpha), - )), - ValueF::TextLit(elts) => { - use InterpolatedTextContents::{Expr, Text}; - rc(ExprF::TextLit( - elts.iter() - .map(|contents| match contents { - Expr(e) => { - Expr(e.normalize_to_expr_maybe_alpha(alpha)) - } - Text(s) => Text(s.clone()), - }) - .collect(), - )) + // Already in NF + ValueInternal::ValueF(NF, _) => {} + } + } + + // Always use normalize_whnf before + fn as_whnf(&self) -> &ValueF { + match self { + ValueInternal::PartialExpr(_) => unreachable!(), + ValueInternal::ValueF(_, v) => v, + } + } + + // Always use normalize_nf before + fn as_nf(&self) -> &ValueF { + match self { + ValueInternal::PartialExpr(_) | ValueInternal::ValueF(WHNF, _) => { + unreachable!() } - ValueF::Equivalence(x, y) => rc(ExprF::BinOp( - dhall_syntax::BinOp::Equivalence, - x.normalize_to_expr_maybe_alpha(alpha), - y.normalize_to_expr_maybe_alpha(alpha), + ValueInternal::ValueF(NF, v) => v, + } + } +} + +impl TypedValueInternal { + fn into_value(self) -> Value { + Value(Rc::new(RefCell::new(self))) + } + fn as_internal(&self) -> &ValueInternal { + &self.internal + } + fn as_internal_mut(&mut self) -> &mut ValueInternal { + &mut self.internal + } + + fn get_type(&self) -> Result { + match &self.typ { + Some(t) => Ok(t.clone()), + None => Err(TypeError::new( + &TypecheckContext::new(), + TypeMessage::Untyped, )), - ValueF::PartialExpr(e) => { - rc(e.map_ref(|v| v.normalize_to_expr_maybe_alpha(alpha))) - } } } +} +impl Value { + pub(crate) fn from_valuef(v: ValueF) -> Value { + ValueInternal::ValueF(WHNF, v).into_value(None) + } + pub(crate) fn from_valuef_and_type(v: ValueF, t: Type) -> Value { + ValueInternal::ValueF(WHNF, v).into_value(Some(t)) + } + pub(crate) fn from_partial_expr(e: ExprF) -> Value { + ValueInternal::PartialExpr(e).into_value(None) + } + pub(crate) fn with_type(self, t: Type) -> Value { + self.as_internal().clone().into_value(Some(t)) + } + + /// Mutates the contents. If no one else shares this thunk, + /// mutates directly, thus avoiding a RefCell lock. + fn mutate_internal(&mut self, f: impl FnOnce(&mut TypedValueInternal)) { + match Rc::get_mut(&mut self.0) { + // Mutate directly if sole owner + Some(refcell) => f(RefCell::get_mut(refcell)), + // Otherwise mutate through the refcell + None => f(&mut self.as_tinternal_mut()), + } + } + + /// Normalizes contents to normal form; faster than `normalize_nf` if + /// no one else shares this thunk pub(crate) fn normalize_mut(&mut self) { - match self { - ValueF::Var(_) - | ValueF::Const(_) - | ValueF::BoolLit(_) - | ValueF::NaturalLit(_) - | ValueF::IntegerLit(_) - | ValueF::DoubleLit(_) => {} - - ValueF::EmptyOptionalLit(tth) | ValueF::EmptyListLit(tth) => { - tth.normalize_mut(); - } + self.mutate_internal(|i| i.as_internal_mut().normalize_nf()) + } - ValueF::NEOptionalLit(th) => { - th.normalize_mut(); - } - ValueF::Lam(_, t, e) => { - t.normalize_mut(); - e.normalize_mut(); - } - ValueF::Pi(_, t, e) => { - t.normalize_mut(); - e.normalize_mut(); - } - ValueF::AppliedBuiltin(_, args) => { - for x in args.iter_mut() { - x.normalize_mut(); - } - } - ValueF::NEListLit(elts) => { - for x in elts.iter_mut() { - x.normalize_mut(); - } - } - ValueF::RecordLit(kvs) => { - for x in kvs.values_mut() { - x.normalize_mut(); - } - } - ValueF::RecordType(kvs) => { - for x in kvs.values_mut() { - x.normalize_mut(); - } - } - ValueF::UnionType(kts) | ValueF::UnionConstructor(_, kts) => { - for x in kts.values_mut().flat_map(|opt| opt) { - x.normalize_mut(); - } - } - ValueF::UnionLit(_, v, kts) => { - v.normalize_mut(); - for x in kts.values_mut().flat_map(|opt| opt) { - x.normalize_mut(); - } - } - ValueF::TextLit(elts) => { - for x in elts.iter_mut() { - use InterpolatedTextContents::{Expr, Text}; - match x { - Expr(n) => n.normalize_mut(), - Text(_) => {} - } - } - } - ValueF::Equivalence(x, y) => { - x.normalize_mut(); - y.normalize_mut(); - } - ValueF::PartialExpr(e) => { - // TODO: need map_mut - e.map_ref(|v| { - v.normalize_nf(); - }); - } + fn as_tinternal(&self) -> Ref { + self.0.borrow() + } + fn as_tinternal_mut(&mut self) -> RefMut { + self.0.borrow_mut() + } + fn as_internal(&self) -> Ref { + Ref::map(self.as_tinternal(), TypedValueInternal::as_internal) + } + fn as_internal_mut(&self) -> RefMut { + RefMut::map(self.0.borrow_mut(), TypedValueInternal::as_internal_mut) + } + + fn do_normalize_whnf(&self) { + let borrow = self.as_internal(); + match &*borrow { + ValueInternal::PartialExpr(_) => { + drop(borrow); + self.as_internal_mut().normalize_whnf(); + } + // Already at least in WHNF + ValueInternal::ValueF(_, _) => {} } } - /// Apply to a value - pub(crate) fn app(self, val: ValueF) -> ValueF { - self.app_val(val) + fn do_normalize_nf(&self) { + let borrow = self.as_internal(); + match &*borrow { + ValueInternal::PartialExpr(_) | ValueInternal::ValueF(WHNF, _) => { + drop(borrow); + self.as_internal_mut().normalize_nf(); + } + // Already in NF + ValueInternal::ValueF(NF, _) => {} + } } - /// Apply to a value - pub(crate) fn app_val(self, val: ValueF) -> ValueF { - self.app_thunk(val.into_thunk()) + // WARNING: avoid normalizing any thunk while holding on to this ref + // or you could run into BorrowMut panics + pub(crate) fn normalize_nf(&self) -> Ref { + self.do_normalize_nf(); + Ref::map(self.as_internal(), ValueInternal::as_nf) } - /// Apply to a thunk - pub fn app_thunk(self, th: Thunk) -> ValueF { - Thunk::from_valuef(self).app_thunk(th) + // WARNING: avoid normalizing any thunk while holding on to this ref + // or you could run into BorrowMut panics + pub(crate) fn as_valuef(&self) -> Ref { + self.do_normalize_whnf(); + Ref::map(self.as_internal(), ValueInternal::as_whnf) } - pub fn from_builtin(b: Builtin) -> ValueF { - ValueF::AppliedBuiltin(b, vec![]) + pub(crate) fn to_valuef(&self) -> ValueF { + self.as_valuef().clone() + } + + pub(crate) fn normalize_to_expr_maybe_alpha( + &self, + alpha: bool, + ) -> OutputSubExpr { + self.normalize_nf().normalize_to_expr_maybe_alpha(alpha) + } + + pub(crate) fn app_valuef(&self, val: ValueF) -> ValueF { + self.app_value(val.into_value()) + } + + pub(crate) fn app_value(&self, th: Value) -> ValueF { + apply_any(self.clone(), th) + } + + pub(crate) fn get_type(&self) -> Result, TypeError> { + Ok(Cow::Owned(self.as_tinternal().get_type()?)) } } -impl Shift for ValueF { +impl TypedValue { + pub(crate) fn from_valuef(v: ValueF) -> TypedValue { + TypedValue::from_value_untyped(Value::from_valuef(v)) + } + + pub(crate) fn from_type(t: Type) -> TypedValue { + t.into_typedvalue() + } + + pub(crate) fn normalize_nf(&self) -> ValueF { + self.0.normalize_nf().clone() + } + + pub(crate) fn to_typed(&self) -> Typed { + self.clone().into_typed() + } + + pub(crate) fn normalize_to_expr_maybe_alpha( + &self, + alpha: bool, + ) -> OutputSubExpr { + self.normalize_nf().normalize_to_expr_maybe_alpha(alpha) + } + + pub(crate) fn from_value_and_type(th: Value, t: Type) -> Self { + TypedValue(th.with_type(t)) + } + pub fn from_value_simple_type(th: Value) -> Self { + TypedValue::from_value_and_type(th, Type::const_type()) + } + pub(crate) fn from_value_untyped(th: Value) -> Self { + TypedValue(th) + } + pub(crate) fn from_const(c: Const) -> Self { + match type_of_const(c) { + Ok(t) => TypedValue::from_valuef_and_type(ValueF::Const(c), t), + Err(_) => TypedValue::from_valuef(ValueF::Const(c)), + } + } + pub(crate) fn from_valuef_and_type(v: ValueF, t: Type) -> Self { + TypedValue(Value::from_valuef_and_type(v, t)) + } + + pub(crate) fn to_valuef(&self) -> ValueF { + self.0.to_valuef() + } + pub(crate) fn to_expr(&self) -> NormalizedSubExpr { + self.to_valuef().normalize_to_expr() + } + pub(crate) fn to_expr_alpha(&self) -> NormalizedSubExpr { + self.to_valuef().normalize_to_expr_maybe_alpha(true) + } + pub(crate) fn to_value(&self) -> Value { + self.0.clone() + } + pub(crate) fn to_type(&self) -> Type { + self.clone().into_typed().into_type() + } + pub(crate) fn into_typed(self) -> Typed { + Typed::from_typedvalue(self) + } + pub(crate) fn as_const(&self) -> Option { + // TODO: avoid clone + match &self.to_valuef() { + ValueF::Const(c) => Some(*c), + _ => None, + } + } + + pub(crate) fn normalize_mut(&mut self) { + self.0.normalize_mut() + } + + pub(crate) fn get_type(&self) -> Result, TypeError> { + self.0.get_type() + } +} + +impl Shift for Value { + fn shift(&self, delta: isize, var: &AlphaVar) -> Option { + Some(Value(self.0.shift(delta, var)?)) + } +} + +impl Shift for ValueInternal { fn shift(&self, delta: isize, var: &AlphaVar) -> Option { Some(match self { - ValueF::Lam(x, t, e) => ValueF::Lam( - x.clone(), - t.shift(delta, var)?, - e.shift(delta, &var.under_binder(x))?, - ), - ValueF::AppliedBuiltin(b, args) => { - ValueF::AppliedBuiltin(*b, args.shift(delta, var)?) - } - ValueF::Pi(x, t, e) => ValueF::Pi( - x.clone(), - t.shift(delta, var)?, - e.shift(delta, &var.under_binder(x))?, - ), - ValueF::Var(v) => ValueF::Var(v.shift(delta, var)?), - ValueF::Const(c) => ValueF::Const(*c), - ValueF::BoolLit(b) => ValueF::BoolLit(*b), - ValueF::NaturalLit(n) => ValueF::NaturalLit(*n), - ValueF::IntegerLit(n) => ValueF::IntegerLit(*n), - ValueF::DoubleLit(n) => ValueF::DoubleLit(*n), - ValueF::EmptyOptionalLit(tth) => { - ValueF::EmptyOptionalLit(tth.shift(delta, var)?) - } - ValueF::NEOptionalLit(th) => { - ValueF::NEOptionalLit(th.shift(delta, var)?) + ValueInternal::PartialExpr(e) => { + ValueInternal::PartialExpr(e.shift(delta, var)?) } - ValueF::EmptyListLit(tth) => { - ValueF::EmptyListLit(tth.shift(delta, var)?) + ValueInternal::ValueF(m, v) => { + ValueInternal::ValueF(*m, v.shift(delta, var)?) } - ValueF::NEListLit(elts) => { - ValueF::NEListLit(elts.shift(delta, var)?) - } - ValueF::RecordLit(kvs) => ValueF::RecordLit(kvs.shift(delta, var)?), - ValueF::RecordType(kvs) => { - ValueF::RecordType(kvs.shift(delta, var)?) - } - ValueF::UnionType(kts) => ValueF::UnionType(kts.shift(delta, var)?), - ValueF::UnionConstructor(x, kts) => { - ValueF::UnionConstructor(x.clone(), kts.shift(delta, var)?) - } - ValueF::UnionLit(x, v, kts) => ValueF::UnionLit( - x.clone(), - v.shift(delta, var)?, - kts.shift(delta, var)?, - ), - ValueF::TextLit(elts) => ValueF::TextLit(elts.shift(delta, var)?), - ValueF::Equivalence(x, y) => { - ValueF::Equivalence(x.shift(delta, var)?, y.shift(delta, var)?) - } - ValueF::PartialExpr(e) => ValueF::PartialExpr(e.shift(delta, var)?), }) } } -impl Subst for ValueF { +impl Shift for TypedValue { + fn shift(&self, delta: isize, var: &AlphaVar) -> Option { + Some(TypedValue(self.0.shift(delta, var)?)) + } +} + +impl Shift for TypedValueInternal { + fn shift(&self, delta: isize, var: &AlphaVar) -> Option { + Some(TypedValueInternal { + internal: self.internal.shift(delta, var)?, + typ: self.typ.shift(delta, var)?, + }) + } +} + +impl Subst for Value { + fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { + Value(self.0.subst_shift(var, val)) + } +} + +impl Subst for ValueInternal { fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { match self { - // Retry normalizing since substituting may allow progress - ValueF::AppliedBuiltin(b, args) => { - apply_builtin(*b, args.subst_shift(var, val)) - } - // Retry normalizing since substituting may allow progress - ValueF::PartialExpr(e) => { - normalize_one_layer(e.subst_shift(var, val)) - } - // Retry normalizing since substituting may allow progress - ValueF::TextLit(elts) => ValueF::TextLit(squash_textlit( - elts.iter().map(|contents| contents.subst_shift(var, val)), - )), - ValueF::Lam(x, t, e) => ValueF::Lam( - x.clone(), - t.subst_shift(var, val), - e.subst_shift(&var.under_binder(x), &val.under_binder(x)), - ), - ValueF::Pi(x, t, e) => ValueF::Pi( - x.clone(), - t.subst_shift(var, val), - e.subst_shift(&var.under_binder(x), &val.under_binder(x)), - ), - ValueF::Var(v) if v == var => val.to_valuef(), - ValueF::Var(v) => ValueF::Var(v.shift(-1, var).unwrap()), - ValueF::Const(c) => ValueF::Const(*c), - ValueF::BoolLit(b) => ValueF::BoolLit(*b), - ValueF::NaturalLit(n) => ValueF::NaturalLit(*n), - ValueF::IntegerLit(n) => ValueF::IntegerLit(*n), - ValueF::DoubleLit(n) => ValueF::DoubleLit(*n), - ValueF::EmptyOptionalLit(tth) => { - ValueF::EmptyOptionalLit(tth.subst_shift(var, val)) - } - ValueF::NEOptionalLit(th) => { - ValueF::NEOptionalLit(th.subst_shift(var, val)) - } - ValueF::EmptyListLit(tth) => { - ValueF::EmptyListLit(tth.subst_shift(var, val)) + ValueInternal::PartialExpr(e) => { + ValueInternal::PartialExpr(e.subst_shift(var, val)) } - ValueF::NEListLit(elts) => { - ValueF::NEListLit(elts.subst_shift(var, val)) + ValueInternal::ValueF(_, v) => { + // The resulting value may not stay in normal form after substitution + ValueInternal::ValueF(WHNF, v.subst_shift(var, val)) } - ValueF::RecordLit(kvs) => { - ValueF::RecordLit(kvs.subst_shift(var, val)) - } - ValueF::RecordType(kvs) => { - ValueF::RecordType(kvs.subst_shift(var, val)) - } - ValueF::UnionType(kts) => { - ValueF::UnionType(kts.subst_shift(var, val)) + } + } +} + +impl Subst for TypedValueInternal { + fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { + TypedValueInternal { + internal: self.internal.subst_shift(var, val), + typ: self.typ.subst_shift(var, val), + } + } +} + +impl Subst for TypedValue { + fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self { + TypedValue(self.0.subst_shift(var, val)) + } +} + +impl std::cmp::PartialEq for Value { + fn eq(&self, other: &Self) -> bool { + *self.as_valuef() == *other.as_valuef() + } +} +impl std::cmp::Eq for Value {} + +impl std::cmp::PartialEq for TypedValue { + fn eq(&self, other: &Self) -> bool { + self.to_valuef() == other.to_valuef() + } +} +impl std::cmp::Eq for TypedValue {} + +impl std::fmt::Debug for Value { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + let b: &ValueInternal = &self.as_internal(); + match b { + ValueInternal::ValueF(m, v) => { + f.debug_tuple(&format!("Value@{:?}", m)).field(v).finish() } - ValueF::UnionConstructor(x, kts) => { - ValueF::UnionConstructor(x.clone(), kts.subst_shift(var, val)) + ValueInternal::PartialExpr(e) => { + f.debug_tuple("Value@PartialExpr").field(e).finish() } - ValueF::UnionLit(x, v, kts) => ValueF::UnionLit( - x.clone(), - v.subst_shift(var, val), - kts.subst_shift(var, val), - ), - ValueF::Equivalence(x, y) => ValueF::Equivalence( - x.subst_shift(var, val), - y.subst_shift(var, val), - ), } } } 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), + + 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), + RecordLit(HashMap), + RecordType(HashMap), + UnionType(HashMap>), + UnionConstructor(Label, HashMap>), + UnionLit(Label, Value, HashMap>), + // Invariant: this must not contain interpolations that are themselves TextLits, and + // contiguous text values must be merged. + TextLit(Vec>), + Equivalence(TypedValue, TypedValue), + // Invariant: this must not contain a value captured by one of the variants above. + PartialExpr(ExprF), +} + +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 { + Some(match self { + ValueF::Lam(x, t, e) => ValueF::Lam( + x.clone(), + t.shift(delta, var)?, + e.shift(delta, &var.under_binder(x))?, + ), + ValueF::AppliedBuiltin(b, args) => { + ValueF::AppliedBuiltin(*b, args.shift(delta, var)?) + } + ValueF::Pi(x, t, e) => ValueF::Pi( + x.clone(), + t.shift(delta, var)?, + e.shift(delta, &var.under_binder(x))?, + ), + ValueF::Var(v) => ValueF::Var(v.shift(delta, var)?), + ValueF::Const(c) => ValueF::Const(*c), + ValueF::BoolLit(b) => ValueF::BoolLit(*b), + ValueF::NaturalLit(n) => ValueF::NaturalLit(*n), + ValueF::IntegerLit(n) => ValueF::IntegerLit(*n), + ValueF::DoubleLit(n) => ValueF::DoubleLit(*n), + ValueF::EmptyOptionalLit(tth) => { + ValueF::EmptyOptionalLit(tth.shift(delta, var)?) + } + ValueF::NEOptionalLit(th) => { + ValueF::NEOptionalLit(th.shift(delta, var)?) + } + ValueF::EmptyListLit(tth) => { + ValueF::EmptyListLit(tth.shift(delta, var)?) + } + ValueF::NEListLit(elts) => { + ValueF::NEListLit(elts.shift(delta, var)?) + } + ValueF::RecordLit(kvs) => ValueF::RecordLit(kvs.shift(delta, var)?), + ValueF::RecordType(kvs) => { + ValueF::RecordType(kvs.shift(delta, var)?) + } + ValueF::UnionType(kts) => ValueF::UnionType(kts.shift(delta, var)?), + ValueF::UnionConstructor(x, kts) => { + ValueF::UnionConstructor(x.clone(), kts.shift(delta, var)?) + } + ValueF::UnionLit(x, v, kts) => ValueF::UnionLit( + x.clone(), + v.shift(delta, var)?, + kts.shift(delta, var)?, + ), + ValueF::TextLit(elts) => ValueF::TextLit(elts.shift(delta, var)?), + ValueF::Equivalence(x, y) => { + ValueF::Equivalence(x.shift(delta, var)?, y.shift(delta, var)?) + } + ValueF::PartialExpr(e) => ValueF::PartialExpr(e.shift(delta, var)?), + }) + } +} + +impl Subst for ValueF { + fn subst_shift(&self, var: &AlphaVar, val: &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) -> ValueF { +pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> ValueF { use dhall_syntax::Builtin::*; use ValueF::*; @@ -66,7 +66,7 @@ pub(crate) fn apply_builtin(b: Builtin, args: Vec) -> 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) -> 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) -> 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) -> 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) -> 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) -> 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) -> 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) -> 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) -> 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) -> 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) -> 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>, -) -> Vec> { + elts: impl Iterator>, +) -> Vec> { use std::mem::replace; use InterpolatedTextContents::{Expr, Text}; fn inner( - elts: impl Iterator>, + elts: impl Iterator>, crnt_str: &mut String, - ret: &mut Vec>, + ret: &mut Vec>, ) { 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), + Value(Value), + ValueRef(&'a Value), + Expr(ExprF), } /// 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> { +fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option> { 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> { 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> { } (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> { } (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> { } (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> { } (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) -> ValueF { +pub(crate) fn normalize_one_layer(expr: ExprF) -> 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) -> 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) -> 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) -> 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) -> 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) -> 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) -> 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) -> 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) -> 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) -> 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, - kts_r: HashMap, + kts_l: HashMap, + kts_r: HashMap, ) -> Result { 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 { match (inner_l.to_valuef(), inner_r.to_valuef()) { ( @@ -690,7 +690,7 @@ fn type_last_layer( let kts: HashMap> = 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, - kts_r: HashMap, + kts_l: HashMap, + kts_r: HashMap, ) -> Result { 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 { 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()) }), ) }) -- cgit v1.2.3