summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
Diffstat (limited to 'dhall')
-rw-r--r--dhall/Cargo.toml1
-rw-r--r--dhall/src/core/value.rs103
-rw-r--r--dhall/src/core/valuef.rs30
-rw-r--r--dhall/src/phase/normalize.rs29
4 files changed, 85 insertions, 78 deletions
diff --git a/dhall/Cargo.toml b/dhall/Cargo.toml
index 0a257e4..16c1c78 100644
--- a/dhall/Cargo.toml
+++ b/dhall/Cargo.toml
@@ -9,6 +9,7 @@ build = "build.rs"
[dependencies]
bytecount = "0.5.1"
itertools = "0.8.0"
+take_mut = "0.2.2"
term-painter = "0.2.3"
serde = { version = "1.0" }
serde_cbor = "0.9.0"
diff --git a/dhall/src/core/value.rs b/dhall/src/core/value.rs
index 5c29bf0..19976af 100644
--- a/dhall/src/core/value.rs
+++ b/dhall/src/core/value.rs
@@ -8,28 +8,32 @@ 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::normalize::{apply_any, normalize_whnf, 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
+enum Form {
+ /// No constraints; expression may not be normalized at all.
+ Unevaled,
+ /// Weak Head Normal Form, i.e. normalized up to the first constructor, but subexpressions may
+ /// not be normalized. This means that the first constructor of the contained ValueF is the first
+ /// constructor of the final Normal Form (NF).
WHNF,
- /// Normal form, i.e. completely normalized
+ /// Normal Form, i.e. completely normalized.
+ /// When all the Values in a ValueF are at least in WHNF, and recursively so, then the
+ /// ValueF is in NF. This is because WHNF ensures that we have the first constructor of the NF; so
+ /// if we have the first constructor of the NF at all levels, we actually have the NF.
NF,
}
-use Marker::{NF, WHNF};
+use Form::{Unevaled, NF, WHNF};
#[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 `WHNF`, the value must be in Weak Head Normal Form
/// Invariant: if the marker is `NF`, the value must be fully normalized
- ValueF(Marker, ValueF),
+ ValueF(Form, ValueF),
}
#[derive(Debug)]
@@ -45,6 +49,8 @@ struct TypedValueInternal {
#[derive(Clone)]
pub struct Value(Rc<RefCell<TypedValueInternal>>);
+/// A value that needs to carry a type for typechecking to work.
+/// TODO: actually enforce this.
#[derive(Debug, Clone)]
pub struct TypedValue(Value);
@@ -58,25 +64,25 @@ impl ValueInternal {
}
fn normalize_whnf(&mut self) {
- match self {
- ValueInternal::PartialExpr(e) => {
- *self =
- ValueInternal::ValueF(WHNF, normalize_one_layer(e.clone()))
+ take_mut::take(self, |vint| match vint {
+ ValueInternal::ValueF(Unevaled, v) => {
+ ValueInternal::ValueF(WHNF, normalize_whnf(v))
}
- // Already at least in WHNF
- ValueInternal::ValueF(_, _) => {}
- }
+ // Already in WHNF
+ vint @ ValueInternal::ValueF(WHNF, _)
+ | vint @ ValueInternal::ValueF(NF, _) => vint,
+ })
}
fn normalize_nf(&mut self) {
match self {
- ValueInternal::PartialExpr(_) => {
+ ValueInternal::ValueF(Unevaled, _) => {
self.normalize_whnf();
self.normalize_nf();
}
- ValueInternal::ValueF(m @ WHNF, v) => {
+ ValueInternal::ValueF(f @ WHNF, v) => {
v.normalize_mut();
- *m = NF;
+ *f = NF;
}
// Already in NF
ValueInternal::ValueF(NF, _) => {}
@@ -86,7 +92,7 @@ impl ValueInternal {
// Always use normalize_whnf before
fn as_whnf(&self) -> &ValueF {
match self {
- ValueInternal::PartialExpr(_) => unreachable!(),
+ ValueInternal::ValueF(Unevaled, _) => unreachable!(),
ValueInternal::ValueF(_, v) => v,
}
}
@@ -94,9 +100,8 @@ impl ValueInternal {
// Always use normalize_nf before
fn as_nf(&self) -> &ValueF {
match self {
- ValueInternal::PartialExpr(_) | ValueInternal::ValueF(WHNF, _) => {
- unreachable!()
- }
+ ValueInternal::ValueF(Unevaled, _)
+ | ValueInternal::ValueF(WHNF, _) => unreachable!(),
ValueInternal::ValueF(NF, v) => v,
}
}
@@ -126,13 +131,13 @@ impl TypedValueInternal {
impl Value {
pub(crate) fn from_valuef(v: ValueF) -> Value {
- ValueInternal::ValueF(WHNF, v).into_value(None)
+ ValueInternal::ValueF(Unevaled, v).into_value(None)
}
pub(crate) fn from_valuef_and_type(v: ValueF, t: Type) -> Value {
- ValueInternal::ValueF(WHNF, v).into_value(Some(t))
+ ValueInternal::ValueF(Unevaled, v).into_value(Some(t))
}
pub(crate) fn from_partial_expr(e: ExprF<Value, Normalized>) -> Value {
- ValueInternal::PartialExpr(e).into_value(None)
+ Value::from_valuef(ValueF::PartialExpr(e))
}
pub(crate) fn with_type(self, t: Type) -> Value {
self.as_internal().clone().into_value(Some(t))
@@ -150,7 +155,7 @@ impl Value {
}
/// Normalizes contents to normal form; faster than `normalize_nf` if
- /// no one else shares this thunk
+ /// no one else shares this thunk.
pub(crate) fn normalize_mut(&mut self) {
self.mutate_internal(|i| i.as_internal_mut().normalize_nf())
}
@@ -171,19 +176,20 @@ impl Value {
fn do_normalize_whnf(&self) {
let borrow = self.as_internal();
match &*borrow {
- ValueInternal::PartialExpr(_) => {
+ ValueInternal::ValueF(Unevaled, _) => {
drop(borrow);
self.as_internal_mut().normalize_whnf();
}
// Already at least in WHNF
- ValueInternal::ValueF(_, _) => {}
+ ValueInternal::ValueF(WHNF, _) | ValueInternal::ValueF(NF, _) => {}
}
}
fn do_normalize_nf(&self) {
let borrow = self.as_internal();
match &*borrow {
- ValueInternal::PartialExpr(_) | ValueInternal::ValueF(WHNF, _) => {
+ ValueInternal::ValueF(Unevaled, _)
+ | ValueInternal::ValueF(WHNF, _) => {
drop(borrow);
self.as_internal_mut().normalize_nf();
}
@@ -199,13 +205,21 @@ impl Value {
Ref::map(self.as_internal(), ValueInternal::as_nf)
}
- // WARNING: avoid normalizing any thunk while holding on to this ref
- // or you could run into BorrowMut panics
+ /// WARNING: avoid normalizing any thunk while holding on to this ref
+ /// or you could run into BorrowMut panics
+ /// TODO: deprecated because of misleading name
pub(crate) fn as_valuef(&self) -> Ref<ValueF> {
+ self.as_whnf()
+ }
+
+ /// WARNING: avoid normalizing any thunk while holding on to this ref
+ /// or you could run into BorrowMut panics
+ pub(crate) fn as_whnf(&self) -> Ref<ValueF> {
self.do_normalize_whnf();
Ref::map(self.as_internal(), ValueInternal::as_whnf)
}
+ /// TODO: deprecated because of misleading name
pub(crate) fn to_valuef(&self) -> ValueF {
self.as_valuef().clone()
}
@@ -317,11 +331,8 @@ impl Shift for Value {
impl Shift for ValueInternal {
fn shift(&self, delta: isize, var: &AlphaVar) -> Option<Self> {
Some(match self {
- ValueInternal::PartialExpr(e) => {
- ValueInternal::PartialExpr(e.shift(delta, var)?)
- }
- ValueInternal::ValueF(m, v) => {
- ValueInternal::ValueF(*m, v.shift(delta, var)?)
+ ValueInternal::ValueF(f, v) => {
+ ValueInternal::ValueF(*f, v.shift(delta, var)?)
}
})
}
@@ -351,12 +362,9 @@ impl Subst<Typed> for Value {
impl Subst<Typed> for ValueInternal {
fn subst_shift(&self, var: &AlphaVar, val: &Typed) -> Self {
match self {
- ValueInternal::PartialExpr(e) => {
- ValueInternal::PartialExpr(e.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))
+ // The resulting value may not stay in wnhf after substitution
+ ValueInternal::ValueF(Unevaled, v.subst_shift(var, val))
}
}
}
@@ -392,14 +400,11 @@ impl std::cmp::PartialEq for TypedValue {
impl std::cmp::Eq for TypedValue {}
impl std::fmt::Debug for Value {
- fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+ fn fmt(&self, fmt: &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()
- }
- ValueInternal::PartialExpr(e) => {
- f.debug_tuple("Value@PartialExpr").field(e).finish()
+ ValueInternal::ValueF(f, v) => {
+ fmt.debug_tuple(&format!("Value@{:?}", f)).field(v).finish()
}
}
}
diff --git a/dhall/src/core/valuef.rs b/dhall/src/core/valuef.rs
index bea2e2e..9e6e8c8 100644
--- a/dhall/src/core/valuef.rs
+++ b/dhall/src/core/valuef.rs
@@ -7,22 +7,13 @@ use dhall_syntax::{
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::normalize::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.
+/// A semantic value. Subexpressions are Values, which are partially evaluated expressions that are
+/// normalized on-demand.
/// Equality is up to alpha-equivalence (renaming of bound variables) and beta-equivalence
-/// (normalization). Equality will normalize only as needed.
+/// (normalization). Equality will normalize as needed.
#[derive(Debug, Clone, PartialEq, Eq)]
pub enum ValueF {
/// Closures
@@ -338,18 +329,15 @@ impl Shift for ValueF {
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))
+ ValueF::AppliedBuiltin(*b, args.subst_shift(var, val))
}
- // Retry normalizing since substituting may allow progress
ValueF::PartialExpr(e) => {
- normalize_one_layer(e.subst_shift(var, val))
+ ValueF::PartialExpr(e.subst_shift(var, val))
+ }
+ ValueF::TextLit(elts) => {
+ ValueF::TextLit(elts.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),
diff --git a/dhall/src/phase/normalize.rs b/dhall/src/phase/normalize.rs
index 93f2528..6c65e43 100644
--- a/dhall/src/phase/normalize.rs
+++ b/dhall/src/phase/normalize.rs
@@ -389,14 +389,6 @@ pub(crate) fn squash_textlit(
ret
}
-// Small helper enum to avoid repetition
-enum Ret<'a> {
- ValueF(ValueF),
- Value(Value),
- ValueRef(&'a Value),
- Expr(ExprF<Value, Normalized>),
-}
-
/// Performs an intersection of two HashMaps.
///
/// # Arguments
@@ -510,6 +502,14 @@ where
kvs
}
+// Small helper enum to avoid repetition
+enum Ret<'a> {
+ ValueF(ValueF),
+ Value(Value),
+ ValueRef(&'a Value),
+ Expr(ExprF<Value, Normalized>),
+}
+
fn apply_binop<'a>(o: BinOp, x: &'a Value, y: &'a Value) -> Option<Ret<'a>> {
use BinOp::{
BoolAnd, BoolEQ, BoolNE, BoolOr, Equivalence, ListAppend, NaturalPlus,
@@ -819,3 +819,16 @@ pub(crate) fn normalize_one_layer(expr: ExprF<Value, Normalized>) -> ValueF {
Ret::Expr(expr) => ValueF::PartialExpr(expr),
}
}
+
+/// Normalize a ValueF into WHNF
+pub(crate) fn normalize_whnf(v: ValueF) -> ValueF {
+ match v {
+ ValueF::AppliedBuiltin(b, args) => apply_builtin(b, args),
+ ValueF::PartialExpr(e) => normalize_one_layer(e),
+ ValueF::TextLit(elts) => {
+ ValueF::TextLit(squash_textlit(elts.into_iter()))
+ }
+ // All other cases are already in WHNF
+ v => v,
+ }
+}
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 19:26:36 +0000