diff options
Diffstat (limited to 'dhall')
| -rw-r--r-- | dhall/src/normalize.rs | 39 | ||||
| -rw-r--r-- | dhall/src/typecheck.rs | 18 |
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() |