summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
Diffstat (limited to 'dhall')
-rw-r--r--dhall/src/normalize.rs39
-rw-r--r--dhall/src/typecheck.rs18
2 files changed, 37 insertions, 20 deletions
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index cff7fdc..5749989 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -1002,9 +1002,11 @@ mod thunk {
}
fn normalize_nf(&mut self) {
- self.normalize_whnf();
match self {
- ThunkInternal::Unnormalized(_, _) => unreachable!(),
+ ThunkInternal::Unnormalized(_, _) => {
+ self.normalize_whnf();
+ self.normalize_nf();
+ }
ThunkInternal::Value(m @ WHNF, v) => {
v.normalize_mut();
*m = NF;
@@ -1091,17 +1093,42 @@ mod thunk {
}
}
+ fn do_normalize_whnf(&self) {
+ let borrow = self.0.borrow();
+ match &*borrow {
+ ThunkInternal::Unnormalized(_, _) => {
+ drop(borrow);
+ self.0.borrow_mut().normalize_whnf();
+ }
+ // Already at least in WHNF
+ ThunkInternal::Value(_, _) => {}
+ }
+ }
+
+ fn do_normalize_nf(&self) {
+ let borrow = self.0.borrow();
+ match &*borrow {
+ ThunkInternal::Unnormalized(_, _)
+ | ThunkInternal::Value(WHNF, _) => {
+ drop(borrow);
+ self.0.borrow_mut().normalize_nf();
+ }
+ // Already in NF
+ ThunkInternal::Value(NF, _) => {}
+ }
+ }
+
// WARNING: avoid normalizing any thunk while holding on to this ref
- // or you will run into BorrowMut panics
+ // or you could run into BorrowMut panics
pub(crate) fn normalize_whnf(&self) -> Ref<Value> {
- self.0.borrow_mut().normalize_whnf();
+ self.do_normalize_whnf();
Ref::map(self.0.borrow(), ThunkInternal::as_whnf)
}
// WARNING: avoid normalizing any thunk while holding on to this ref
- // or you will run into BorrowMut panics
+ // or you could run into BorrowMut panics
pub(crate) fn normalize_nf(&self) -> Ref<Value> {
- self.0.borrow_mut().normalize_nf();
+ self.do_normalize_nf();
Ref::map(self.0.borrow(), ThunkInternal::as_nf)
}
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index c6f3645..d68d304 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -901,13 +901,9 @@ fn type_last_layer(
))
}
Field(r, x) => {
- let tr = r.get_type()?;
- let tr_internal = tr.internal_whnf();
- match &tr_internal {
+ match &r.get_type()?.internal_whnf() {
Some(Value::RecordType(kts)) => match kts.get(&x) {
Some(tth) => {
- let tth = tth.clone();
- drop(tr_internal);
Ok(RetType(tth.to_type(ctx)?))
},
None => Err(mkerr(MissingRecordField(x, r.clone()))),
@@ -915,31 +911,26 @@ fn type_last_layer(
// TODO: branch here only when r.get_type() is a Const
_ => {
let r = r.to_type();
- let r_internal = r.internal_whnf();
- match &r_internal {
+ match &r.internal_whnf() {
Some(Value::UnionType(kts)) => match kts.get(&x) {
// Constructor has type T -> < x: T, ... >
// TODO: use "_" instead of x (i.e. compare types using equivalence in tests)
Some(Some(t)) => {
- let t = t.clone();
- drop(r_internal);
Ok(RetType(
TypeIntermediate::Pi(
ctx.clone(),
x.clone(),
t.to_type(ctx)?,
- r,
+ r.clone(),
)
.typecheck()?
.to_type(),
))
},
Some(None) => {
- drop(r_internal);
- Ok(RetType(r))
+ Ok(RetType(r.clone()))
},
None => {
- drop(r_internal);
Err(mkerr(MissingUnionField(
x,
r.to_normalized(),
@@ -947,7 +938,6 @@ fn type_last_layer(
},
},
_ => {
- drop(r_internal);
Err(mkerr(NotARecord(
x,
r.to_normalized()