summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--dhall/src/semantics/builtins.rs7
-rw-r--r--dhall/src/semantics/nze/env.rs2
-rw-r--r--dhall/src/semantics/nze/normalize.rs25
-rw-r--r--dhall/src/semantics/nze/value.rs79
4 files changed, 55 insertions, 58 deletions
diff --git a/dhall/src/semantics/builtins.rs b/dhall/src/semantics/builtins.rs
index 1357adf..85ef294 100644
--- a/dhall/src/semantics/builtins.rs
+++ b/dhall/src/semantics/builtins.rs
@@ -12,7 +12,7 @@ use std::collections::HashMap;
use std::convert::TryInto;
/// A partially applied builtin.
-/// Invariant: TODO
+/// Invariant: the evaluation of the given args must not be able to progress further
#[derive(Debug, Clone)]
pub(crate) struct BuiltinClosure<Value> {
pub env: NzEnv,
@@ -41,9 +41,8 @@ impl BuiltinClosure<Value> {
let types = self.types.iter().cloned().chain(once(f_ty)).collect();
apply_builtin(self.b, args, ret_ty, types, self.env.clone())
}
- pub fn ensure_whnf(self, ret_ty: &Value) -> ValueKind {
- apply_builtin(self.b, self.args, ret_ty, self.types, self.env)
- }
+ /// This doesn't break the invariant because we already checked that the appropriate arguments
+ /// did not normalize to something that allows evaluation to proceed.
pub fn normalize_mut(&mut self) {
for x in self.args.iter_mut() {
x.normalize_mut();
diff --git a/dhall/src/semantics/nze/env.rs b/dhall/src/semantics/nze/env.rs
index a083076..073886e 100644
--- a/dhall/src/semantics/nze/env.rs
+++ b/dhall/src/semantics/nze/env.rs
@@ -62,7 +62,7 @@ impl NzEnv {
pub fn lookup_val(&self, var: &AlphaVar) -> Value {
let idx = self.items.len() - 1 - var.idx();
match &self.items[idx] {
- NzEnvItem::Kept(ty) => Value::from_kind_and_type_whnf(
+ NzEnvItem::Kept(ty) => Value::from_kind_and_type(
ValueKind::Var(NzVar::new(idx)),
ty.clone(),
),
diff --git a/dhall/src/semantics/nze/normalize.rs b/dhall/src/semantics/nze/normalize.rs
index 16c886e..7632d12 100644
--- a/dhall/src/semantics/nze/normalize.rs
+++ b/dhall/src/semantics/nze/normalize.rs
@@ -208,12 +208,12 @@ fn apply_binop<'a>(
_ => unreachable!("Internal type error"),
};
let kvs = merge_maps::<_, _, _, !>(kvs1, kvs2, |k, v1, v2| {
- Ok(Value::from_kind_and_type(
- ValueKind::PartialExpr(ExprKind::BinOp(
+ Ok(Value::from_partial_expr(
+ ExprKind::BinOp(
RecursiveRecordMerge,
v1.clone(),
v2.clone(),
- )),
+ ),
kts.get(k).expect("Internal type error").clone(),
))
})?;
@@ -226,12 +226,12 @@ fn apply_binop<'a>(
kts_y,
// If the Label exists for both records, then we hit the recursive case.
|_, l: &Value, r: &Value| {
- Ok(Value::from_kind_and_type(
- ValueKind::PartialExpr(ExprKind::BinOp(
+ Ok(Value::from_partial_expr(
+ ExprKind::BinOp(
RecursiveRecordTypeMerge,
l.clone(),
r.clone(),
- )),
+ ),
ty.clone(),
))
},
@@ -444,16 +444,6 @@ pub(crate) fn normalize_one_layer(
}
}
-/// Normalize a ValueKind into WHNF
-pub(crate) fn normalize_whnf(v: ValueKind, ty: &Value) -> ValueKind {
- match v {
- ValueKind::AppliedBuiltin(closure) => closure.ensure_whnf(ty),
- ValueKind::PartialExpr(e) => normalize_one_layer(e, ty, &NzEnv::new()),
- // All other cases are already in WHNF
- v => v,
- }
-}
-
/// Normalize a TyExpr into WHNF
pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> Value {
let ty = match tye.get_type() {
@@ -490,6 +480,5 @@ pub(crate) fn normalize_tyexpr_whnf(tye: &TyExpr, env: &NzEnv) -> Value {
}
};
- // dbg!(tye.kind(), env, &kind);
- Value::from_kind_and_type_whnf(kind, ty)
+ Value::from_kind_and_type(kind, ty)
}
diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs
index 8ae0939..108dc9c 100644
--- a/dhall/src/semantics/nze/value.rs
+++ b/dhall/src/semantics/nze/value.rs
@@ -5,7 +5,7 @@ use std::rc::Rc;
use crate::error::{TypeError, TypeMessage};
use crate::semantics::Binder;
use crate::semantics::{
- apply_any, normalize_tyexpr_whnf, normalize_whnf, squash_textlit,
+ apply_any, normalize_one_layer, normalize_tyexpr_whnf, squash_textlit,
};
use crate::semantics::{type_of_builtin, typecheck, TyExpr, TyExprKind};
use crate::semantics::{BuiltinClosure, NzEnv, NzVar, VarEnv};
@@ -16,34 +16,30 @@ use crate::syntax::{
use crate::{Normalized, NormalizedExpr, ToExprOptions};
/// Stores a possibly unevaluated value. Gets (partially) normalized on-demand, sharing computation
-/// automatically. Uses a RefCell to share computation.
-/// Can optionally store a type from typechecking to preserve type information.
-/// If you compare for equality two `Value`s in WHNF, then equality will be up to alpha-equivalence
+/// automatically. Uses a Rc<RefCell> to share computation.
+/// If you compare for equality two `Value`s, then equality will be up to alpha-equivalence
/// (renaming of bound variables) and beta-equivalence (normalization). It will recursively
/// normalize as needed.
#[derive(Clone)]
pub(crate) struct Value(Rc<RefCell<ValueInternal>>);
-/// Invariant: if `form` is `WHNF`, `value` must be in Weak Head Normal Form
#[derive(Debug)]
struct ValueInternal {
form: Form,
- /// This is None if and only if `value` is `Sort` (which doesn't have a type)
+ /// This is None if and only if `form` is `Sort` (which doesn't have a type)
ty: Option<Value>,
span: Span,
}
+/// A potentially un-evaluated expression. Once we get to WHNF we won't modify the form again, as
+/// explained in the doc for `ValueKind`.
#[derive(Debug, Clone)]
pub(crate) enum Form {
+ /// A totally unnormalized value.
Thunk(Thunk),
- /// No constraints; expression may not be normalized at all.
- Unevaled(ValueKind),
- /// 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 ValueKind is the first
- /// constructor of the final Normal Form (NF).
- /// When all the Values in a ValueKind are in WHNF, and recursively so, then the
- /// ValueKind is in NF. This is because WHNF ensures that we have the first constructor of the NF; so
- /// if we have the first constructor of the NF at all levels, we actually have the NF.
+ /// A partially normalized value that may need to go through `normalize_one_layer`.
+ PartialExpr(ExprKind<Value, Normalized>),
+ /// A value in WHNF.
WHNF(ValueKind),
}
@@ -73,6 +69,13 @@ pub(crate) enum Closure {
#[derive(Debug, Clone, PartialEq, Eq)]
pub(crate) struct TextLit(Vec<InterpolatedTextContents<Value>>);
+/// This represents a value in Weak Head Normal Form (WHNF). This means that the value is
+/// normalized up to the first constructor, but subexpressions may not be fully normalized.
+/// When all the Values in a ValueKind are in WHNF, and recursively so, then the ValueKind is in
+/// Normal Form (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.
+/// In particular, this means that once we get a `ValueKind`, it can be considered immutable, and
+/// we only need to recursively normalize its sub-`Value`s to get to the NF.
#[derive(Debug, Clone, PartialEq, Eq)]
pub(crate) enum ValueKind {
/// Closures
@@ -86,7 +89,6 @@ pub(crate) enum ValueKind {
annot: Value,
closure: Closure,
},
- // Invariant: in whnf, the evaluation must not be able to progress further.
AppliedBuiltin(BuiltinClosure<Value>),
Var(NzVar),
@@ -109,7 +111,7 @@ pub(crate) enum ValueKind {
UnionLit(Label, Value, HashMap<Label, Option<Value>>, Value, Value),
TextLit(TextLit),
Equivalence(Value, Value),
- // Invariant: in whnf, this must not contain a value captured by one of the variants above.
+ /// Invariant: evaluation must not be able to progress with `normalize_one_layer`?
PartialExpr(ExprKind<Value, Normalized>),
}
@@ -130,6 +132,7 @@ impl Value {
}
.into_value()
}
+ /// Construct a Value from a completely unnormalized expression.
pub(crate) fn new_thunk(env: &NzEnv, tye: TyExpr) -> Value {
ValueInternal {
form: Form::Thunk(Thunk::new(env, tye.clone())),
@@ -138,10 +141,15 @@ impl Value {
}
.into_value()
}
- pub(crate) fn from_kind_and_type(v: ValueKind, t: Value) -> Value {
- Value::new(Form::Unevaled(v), t, Span::Artificial)
+ /// Construct a Value from a partially normalized expression that's not in WHNF.
+ pub(crate) fn from_partial_expr(
+ e: ExprKind<Value, Normalized>,
+ t: Value,
+ ) -> Value {
+ Value::new(Form::PartialExpr(e), t, Span::Artificial)
}
- pub(crate) fn from_kind_and_type_whnf(v: ValueKind, t: Value) -> Value {
+ /// Make a Value from a ValueKind
+ pub(crate) fn from_kind_and_type(v: ValueKind, t: Value) -> Value {
Value::new(Form::WHNF(v), t, Span::Artificial)
}
pub(crate) fn from_const(c: Const) -> Self {
@@ -188,7 +196,7 @@ impl Value {
pub(crate) fn kind(&self) -> Ref<ValueKind> {
self.normalize_whnf();
Ref::map(self.as_internal(), |vint| match &vint.form {
- Form::Thunk(..) | Form::Unevaled(..) => unreachable!(),
+ Form::Thunk(..) | Form::PartialExpr(..) => unreachable!(),
Form::WHNF(k) => k,
})
}
@@ -228,7 +236,7 @@ impl Value {
pub(crate) fn normalize_whnf(&self) {
let borrow = self.as_internal();
match borrow.form {
- Form::Thunk(..) | Form::Unevaled(_) => {
+ Form::Thunk(..) | Form::PartialExpr(_) => {
drop(borrow);
self.as_internal_mut().normalize_whnf();
}
@@ -248,10 +256,7 @@ impl Value {
}
_ => unreachable!("Internal type error"),
};
- Value::from_kind_and_type_whnf(
- apply_any(self.clone(), v, &body_t),
- body_t,
- )
+ Value::from_kind_and_type(apply_any(self.clone(), v, &body_t), body_t)
}
/// In debug mode, panic if the provided type doesn't match the value's type.
@@ -398,12 +403,13 @@ impl ValueInternal {
fn normalize_whnf(&mut self) {
use std::mem::replace;
- let dummy = Form::Unevaled(ValueKind::Const(Const::Type));
+ let dummy = Form::PartialExpr(ExprKind::Const(Const::Type));
self.form = match replace(&mut self.form, dummy) {
Form::Thunk(th) => Form::WHNF(th.eval().kind().clone()),
- Form::Unevaled(kind) => {
+ Form::PartialExpr(e) => {
Form::WHNF(match &self.ty {
- Some(ty) => normalize_whnf(kind, &ty),
+ // TODO: env
+ Some(ty) => normalize_one_layer(e, &ty, &NzEnv::new()),
// `value` is `Sort`
None => ValueKind::Const(Const::Sort),
})
@@ -413,11 +419,11 @@ impl ValueInternal {
};
}
fn normalize_nf(&mut self) {
- if let Form::Thunk(..) | Form::Unevaled(_) = self.form {
+ if let Form::Thunk(..) | Form::PartialExpr(_) = self.form {
self.normalize_whnf();
}
match &mut self.form {
- Form::Thunk(..) | Form::Unevaled(_) => unreachable!(),
+ Form::Thunk(..) | Form::PartialExpr(_) => unreachable!(),
Form::WHNF(k) => k.normalize_mut(),
}
}
@@ -451,9 +457,10 @@ impl ValueKind {
ValueKind::NEOptionalLit(th) => {
th.normalize_mut();
}
- ValueKind::LamClosure { annot, .. }
- | ValueKind::PiClosure { annot, .. } => {
+ ValueKind::LamClosure { annot, closure, .. }
+ | ValueKind::PiClosure { annot, closure, .. } => {
annot.normalize_mut();
+ closure.normalize_mut();
}
ValueKind::AppliedBuiltin(closure) => closure.normalize_mut(),
ValueKind::NEListLit(elts) => {
@@ -553,6 +560,8 @@ impl Closure {
}
}
+ // TODO: somehow normalize the body. Might require to pass an env.
+ pub fn normalize_mut(&mut self) {}
/// Convert this closure to a TyExpr
pub fn to_tyexpr(&self, venv: VarEnv) -> TyExpr {
self.apply_var(NzVar::new(venv.size()))
@@ -665,9 +674,9 @@ impl std::fmt::Debug for Value {
x.field("thunk", th);
x
}
- Form::Unevaled(kind) => {
- let mut x = fmt.debug_struct(&format!("Value@Unevaled"));
- x.field("kind", kind);
+ Form::PartialExpr(e) => {
+ let mut x = fmt.debug_struct(&format!("Value@PartialExpr"));
+ x.field("expr", e);
x
}
Form::WHNF(kind) => {