summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorNadrieril2020-01-30 19:13:37 +0000
committerNadrieril2020-01-30 19:13:37 +0000
commit3c4895a06a4910184203d8531e7ab318db71fb15 (patch)
tree565f72d011f4e734b54f574297004d33a70e9faf
parentdc01ef2030e1177e4f247f4ddc0a3f69241d5cfc (diff)
Prepare ValueInternal with new `Form`s
-rw-r--r--dhall/src/semantics/nze/value.rs103
1 files changed, 50 insertions, 53 deletions
diff --git a/dhall/src/semantics/nze/value.rs b/dhall/src/semantics/nze/value.rs
index 06d8df8..31acb11 100644
--- a/dhall/src/semantics/nze/value.rs
+++ b/dhall/src/semantics/nze/value.rs
@@ -30,23 +30,22 @@ pub(crate) struct Value(Rc<RefCell<ValueInternal>>);
#[derive(Debug)]
struct ValueInternal {
form: Form,
- kind: ValueKind,
/// This is None if and only if `value` is `Sort` (which doesn't have a type)
ty: Option<Value>,
span: Span,
}
-#[derive(Debug, Clone, Copy)]
+#[derive(Debug, Clone)]
pub(crate) enum Form {
/// No constraints; expression may not be normalized at all.
- Unevaled,
+ 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.
- WHNF,
+ WHNF(ValueKind),
}
/// An unevaluated subexpression
@@ -118,10 +117,9 @@ pub(crate) enum ValueKind {
}
impl Value {
- fn new(kind: ValueKind, form: Form, ty: Value, span: Span) -> Value {
+ fn new(form: Form, ty: Value, span: Span) -> Value {
ValueInternal {
form,
- kind,
ty: Some(ty),
span,
}
@@ -129,8 +127,7 @@ impl Value {
}
pub(crate) fn const_sort() -> Value {
ValueInternal {
- form: WHNF,
- kind: ValueKind::Const(Const::Sort),
+ form: WHNF(ValueKind::Const(Const::Sort)),
ty: None,
span: Span::Artificial,
}
@@ -138,18 +135,17 @@ impl Value {
}
pub(crate) fn new_thunk(env: &NzEnv, tye: TyExpr) -> Value {
ValueInternal {
- form: Unevaled,
- kind: ValueKind::Thunk(Thunk::new(env, tye.clone())),
+ form: Unevaled(ValueKind::Thunk(Thunk::new(env, tye.clone()))),
ty: tye.get_type().ok(),
span: tye.span().clone(),
}
.into_value()
}
pub(crate) fn from_kind_and_type(v: ValueKind, t: Value) -> Value {
- Value::new(v, Unevaled, t, Span::Artificial)
+ Value::new(Unevaled(v), t, Span::Artificial)
}
pub(crate) fn from_kind_and_type_whnf(v: ValueKind, t: Value) -> Value {
- Value::new(v, WHNF, t, Span::Artificial)
+ Value::new(WHNF(v), t, Span::Artificial)
}
pub(crate) fn from_const(c: Const) -> Self {
let v = ValueKind::Const(c);
@@ -194,7 +190,10 @@ impl Value {
/// panics.
pub(crate) fn kind(&self) -> Ref<ValueKind> {
self.normalize_whnf();
- Ref::map(self.as_internal(), ValueInternal::as_kind)
+ Ref::map(self.as_internal(), |vint| match &vint.form {
+ Unevaled(..) => unreachable!(),
+ WHNF(k) => k,
+ })
}
/// Converts a value back to the corresponding AST expression.
@@ -232,12 +231,12 @@ impl Value {
pub(crate) fn normalize_whnf(&self) {
let borrow = self.as_internal();
match borrow.form {
- Unevaled => {
+ Unevaled(_) => {
drop(borrow);
self.as_internal_mut().normalize_whnf();
}
// Already in WHNF
- WHNF => {}
+ WHNF(_) => {}
}
}
pub(crate) fn normalize_nf(&self) {
@@ -400,41 +399,29 @@ impl ValueInternal {
fn into_value(self) -> Value {
Value(Rc::new(RefCell::new(self)))
}
- fn as_kind(&self) -> &ValueKind {
- &self.kind
- }
fn normalize_whnf(&mut self) {
- let dummy = ValueInternal {
- form: Unevaled,
- kind: ValueKind::Const(Const::Type),
- ty: None,
- span: Span::Artificial,
- };
- let vint = std::mem::replace(self, dummy);
- *self = match (&vint.form, &vint.ty) {
- (Unevaled, Some(ty)) => ValueInternal {
- form: WHNF,
- kind: normalize_whnf(vint.kind, &ty),
- ty: vint.ty,
- span: vint.span,
- },
- // `value` is `Sort`
- (Unevaled, None) => ValueInternal {
- form: WHNF,
- kind: ValueKind::Const(Const::Sort),
- ty: None,
- span: vint.span,
- },
+ use std::mem::replace;
+ let dummy = Unevaled(ValueKind::Const(Const::Type));
+ self.form = match replace(&mut self.form, dummy) {
+ Unevaled(kind) => {
+ WHNF(match &self.ty {
+ Some(ty) => normalize_whnf(kind, &ty),
+ // `value` is `Sort`
+ None => ValueKind::Const(Const::Sort),
+ })
+ }
// Already in WHNF
- (WHNF, _) => vint,
- }
+ form @ WHNF(_) => form,
+ };
}
fn normalize_nf(&mut self) {
- if let Unevaled = self.form {
+ if let Unevaled(_) = self.form {
self.normalize_whnf();
}
- self.kind.normalize_mut();
+ match &mut self.form {
+ Unevaled(k) | WHNF(k) => k.normalize_mut(),
+ }
}
fn get_type(&self) -> Result<&Value, TypeError> {
@@ -679,17 +666,27 @@ impl std::cmp::Eq for Closure {}
impl std::fmt::Debug for Value {
fn fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
let vint: &ValueInternal = &self.as_internal();
- if let ValueKind::Const(c) = &vint.kind {
- write!(fmt, "{:?}", c)
- } else {
- let mut x = fmt.debug_struct(&format!("Value@{:?}", &vint.form));
- x.field("value", &vint.kind);
- if let Some(ty) = vint.ty.as_ref() {
- x.field("type", &ty);
- } else {
- x.field("type", &None::<()>);
+ let mut x = match &vint.form {
+ WHNF(kind) => {
+ if let ValueKind::Const(c) = kind {
+ return write!(fmt, "{:?}", c);
+ } else {
+ let mut x = fmt.debug_struct(&format!("Value@WHNF"));
+ x.field("kind", kind);
+ x
+ }
}
- x.finish()
+ Unevaled(kind) => {
+ let mut x = fmt.debug_struct(&format!("Value@Unevaled"));
+ x.field("kind", kind);
+ x
+ }
+ };
+ if let Some(ty) = vint.ty.as_ref() {
+ x.field("type", &ty);
+ } else {
+ x.field("type", &None::<()>);
}
+ x.finish()
}
}