summaryrefslogtreecommitdiff
path: root/dhall/src
diff options
context:
space:
mode:
authorNadrieril2019-12-24 21:46:29 +0000
committerNadrieril2019-12-24 21:46:29 +0000
commitf5a588defc0ad22ce2f0d3b32ef8f0e22e43e672 (patch)
tree405bcef717b1a7ab0ec8de898ca5264698c39362 /dhall/src
parent611d4ced3a5ffca8b9765971001995a216dbbb54 (diff)
Ensure inferred type is always in normal form
Diffstat (limited to 'dhall/src')
-rw-r--r--dhall/src/semantics/core/value.rs3
-rw-r--r--dhall/src/semantics/phase/mod.rs11
-rw-r--r--dhall/src/semantics/phase/typecheck.rs5
-rw-r--r--dhall/src/tests.rs7
4 files changed, 19 insertions, 7 deletions
diff --git a/dhall/src/semantics/core/value.rs b/dhall/src/semantics/core/value.rs
index ca7c4bc..6fa00ac 100644
--- a/dhall/src/semantics/core/value.rs
+++ b/dhall/src/semantics/core/value.rs
@@ -200,6 +200,9 @@ impl Value {
WHNF | NF => {}
}
}
+ pub(crate) fn normalize_nf(&self) {
+ self.as_internal_mut().normalize_nf();
+ }
pub(crate) fn app(&self, v: Value) -> Value {
let body_t = match &*self.get_type_not_sort().as_whnf() {
diff --git a/dhall/src/semantics/phase/mod.rs b/dhall/src/semantics/phase/mod.rs
index b22120d..5332eb3 100644
--- a/dhall/src/semantics/phase/mod.rs
+++ b/dhall/src/semantics/phase/mod.rs
@@ -63,6 +63,11 @@ impl Parsed {
pub fn encode(&self) -> Result<Vec<u8>, EncodeError> {
binary::encode(&self.0)
}
+
+ /// Converts a value back to the corresponding AST expression.
+ pub fn to_expr(&self) -> ParsedExpr {
+ self.0.clone()
+ }
}
impl Resolved {
@@ -73,6 +78,10 @@ impl Resolved {
Ok(typecheck::typecheck_with(self.0, ty.normalize_to_expr())?
.into_typed())
}
+ /// Converts a value back to the corresponding AST expression.
+ pub fn to_expr(&self) -> ResolvedExpr {
+ self.0.clone()
+ }
}
impl Typed {
@@ -96,7 +105,7 @@ impl Typed {
}
/// Converts a value back to the corresponding AST expression.
- pub(crate) fn to_expr(&self) -> NormalizedExpr {
+ pub fn to_expr(&self) -> ResolvedExpr {
self.0.to_expr(ToExprOptions {
alpha: false,
normalize: false,
diff --git a/dhall/src/semantics/phase/typecheck.rs b/dhall/src/semantics/phase/typecheck.rs
index e9836e8..3960146 100644
--- a/dhall/src/semantics/phase/typecheck.rs
+++ b/dhall/src/semantics/phase/typecheck.rs
@@ -315,6 +315,7 @@ fn type_with(
Ok(match e.as_ref() {
Lam(var, annot, body) => {
let annot = type_with(ctx, annot.clone())?;
+ annot.normalize_nf();
let ctx2 = ctx.insert_type(var, annot.clone());
let body = type_with(&ctx2, body.clone())?;
let body_type = body.get_type()?;
@@ -401,7 +402,9 @@ fn type_last_layer(
return mkerr(TypeMismatch(f.clone(), tx.clone(), a.clone()));
}
- RetTypeOnly(tb.subst_shift(&x.into(), a))
+ let ret = tb.subst_shift(&x.into(), a);
+ ret.normalize_nf();
+ RetTypeOnly(ret)
}
Annot(x, t) => {
if &x.get_type()? != t {
diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs
index 7a3a540..0163c4d 100644
--- a/dhall/src/tests.rs
+++ b/dhall/src/tests.rs
@@ -160,11 +160,8 @@ pub fn run_test(test: Test<'_>) -> Result<()> {
TypeInferenceSuccess(expr_file_path, expected_file_path) => {
let expr =
parse_file_str(&expr_file_path)?.resolve()?.typecheck()?;
- let ty = expr.get_type()?.normalize_to_expr();
- let expected = parse_file_str(&expected_file_path)?
- .resolve()?
- .typecheck()?
- .normalize_to_expr();
+ let ty = expr.get_type()?.to_expr();
+ let expected = parse_file_str(&expected_file_path)?.to_expr();
assert_eq_display!(ty, expected);
}
TypeInferenceFailure(file_path) => {