summaryrefslogtreecommitdiff
path: root/dhall
diff options
context:
space:
mode:
Diffstat (limited to 'dhall')
-rw-r--r--dhall/src/normalize.rs4
-rw-r--r--dhall/src/typecheck.rs95
2 files changed, 62 insertions, 37 deletions
diff --git a/dhall/src/normalize.rs b/dhall/src/normalize.rs
index 26b23c2..17996cf 100644
--- a/dhall/src/normalize.rs
+++ b/dhall/src/normalize.rs
@@ -954,11 +954,15 @@ mod thunk {
self.clone()
}
+ // WARNING: avoid normalizing any thunk while holding on to this ref
+ // or you will run into BorrowMut panics
pub(crate) fn normalize_whnf(&self) -> Ref<Value> {
self.0.borrow_mut().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
pub(crate) fn normalize_nf(&self) -> Ref<Value> {
self.0.borrow_mut().normalize_nf();
Ref::map(self.0.borrow(), ThunkInternal::as_nf)
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs
index 8691945..461f1cc 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -991,46 +991,67 @@ fn type_last_layer(
.normalize_to_type(),
))
}
- Field(r, x) => match r.get_type()?.internal_whnf().deref() {
- Some(Value::RecordType(kts)) => match kts.get(&x) {
- Some(tth) => Ok(RetType(tth.clone().normalize_to_type(ctx)?)),
- None => Err(mkerr(MissingRecordField(x, r.clone()))),
- },
- // TODO: branch here only when r.get_type() is a Const
- _ => {
- let r = r.normalize_to_type();
- let r_internal = r.internal_whnf();
- match r_internal.deref() {
- 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)) => Ok(RetType(
- TypeIntermediate::Pi(
- ctx.clone(),
- x.clone(),
- t.clone().normalize_to_type(ctx)?,
- r.clone(),
- )
- .typecheck()?
- .normalize_to_type(),
- )),
- Some(None) => Ok(RetType(r.clone())),
- None => Err(mkerr(MissingUnionField(
- x,
- r.clone().into_normalized()?,
- ))),
+ Field(r, x) => {
+ let tr = r.get_type()?;
+ let tr_internal = tr.internal_whnf();
+ match tr_internal.deref() {
+ Some(Value::RecordType(kts)) => match kts.get(&x) {
+ Some(tth) => {
+ let tth = tth.clone();
+ drop(tr_internal);
+ Ok(RetType(tth.normalize_to_type(ctx)?))
},
- _ => Err(mkerr(NotARecord(
- x,
- r.clone().into_normalized()?
- ))),
+ None => Err(mkerr(MissingRecordField(x, r.clone()))),
+ },
+ // TODO: branch here only when r.get_type() is a Const
+ _ => {
+ let r = r.normalize_to_type();
+ let r_internal = r.internal_whnf();
+ match r_internal.deref() {
+ 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.normalize_to_type(ctx)?,
+ r,
+ )
+ .typecheck()?
+ .normalize_to_type(),
+ ))
+ },
+ Some(None) => {
+ drop(r_internal);
+ Ok(RetType(r))
+ },
+ None => {
+ drop(r_internal);
+ Err(mkerr(MissingUnionField(
+ x,
+ r.into_normalized()?,
+ )))
+ },
+ },
+ _ => {
+ drop(r_internal);
+ Err(mkerr(NotARecord(
+ x,
+ r.into_normalized()?
+ )))
+ },
+ }
}
+ // _ => Err(mkerr(NotARecord(
+ // x,
+ // r.normalize_to_type()?.into_normalized()?,
+ // ))),
}
- // _ => Err(mkerr(NotARecord(
- // x,
- // r.normalize_to_type()?.into_normalized()?,
- // ))),
- },
+ }
Const(c) => Ok(RetType(type_of_const(c))),
Builtin(b) => Ok(RetExpr(type_of_builtin(b))),
BoolLit(_) => Ok(RetType(builtin_to_type(Bool)?)),