summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorNadrieril2019-08-16 12:35:34 +0200
committerNadrieril2019-08-16 18:02:26 +0200
commit51bb1d2da8e5874129d4b5cc5d0c60e23eee9f11 (patch)
treed1d1d106abff44ead33bcb4b3275f85e9afc8ae3
parent664c925186ecd587f46577715254b74b6264e4fe (diff)
Typecheck before normalizing in tests
-rw-r--r--dhall/build.rs5
-rw-r--r--dhall/src/phase/typecheck.rs5
-rw-r--r--dhall/src/tests.rs28
3 files changed, 21 insertions, 17 deletions
diff --git a/dhall/build.rs b/dhall/build.rs
index 2305208..166b036 100644
--- a/dhall/build.rs
+++ b/dhall/build.rs
@@ -213,7 +213,10 @@ fn main() -> std::io::Result<()> {
"alpha_normalize",
"alpha-normalization/",
"AlphaNormalization",
- |_| false,
+ |path| {
+ // This test doesn't typecheck
+ path == "success/unit/FunctionNestedBindingXXFree"
+ },
)?;
make_test_module(
diff --git a/dhall/src/phase/typecheck.rs b/dhall/src/phase/typecheck.rs
index 2030f21..7bbad38 100644
--- a/dhall/src/phase/typecheck.rs
+++ b/dhall/src/phase/typecheck.rs
@@ -1002,10 +1002,7 @@ fn type_last_layer(
/// will fail.
fn type_of(e: SubExpr<Normalized>) -> Result<Typed, TypeError> {
let ctx = TypecheckContext::new();
- let e = type_with(&ctx, e)?;
- // Ensure `e` has a type (i.e. `e` is not `Sort`)
- e.get_type()?;
- Ok(e)
+ type_with(&ctx, e)
}
pub(crate) fn typecheck(e: Resolved) -> Result<Typed, TypeError> {
diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs
index d269523..70cff46 100644
--- a/dhall/src/tests.rs
+++ b/dhall/src/tests.rs
@@ -169,7 +169,7 @@ pub fn run_test(
let expected_file_path = base_path + "B.dhall";
let expected = parse_file_str(&expected_file_path)?
.resolve()?
- .skip_typecheck()
+ .typecheck()?
.normalize();
match feature {
@@ -177,24 +177,23 @@ pub fn run_test(
unreachable!()
}
Import => {
- let expr = expr.skip_typecheck().normalize();
+ let expr = expr.typecheck()?.normalize();
assert_eq_display!(expr, expected);
}
Typecheck => {
- expr.typecheck_with(&expected.to_type())?;
+ expr.typecheck_with(&expected.to_type())?.get_type()?;
}
TypeInference => {
let expr = expr.typecheck()?;
- let ty = expr.get_type()?.into_owned();
- assert_eq_display!(ty.to_normalized(), expected);
+ let ty = expr.get_type()?.to_normalized();
+ assert_eq_display!(ty, expected);
}
Normalization => {
- let expr = expr.skip_typecheck().normalize();
+ let expr = expr.typecheck()?.normalize();
assert_eq_display!(expr, expected);
}
AlphaNormalization => {
- let expr =
- expr.skip_typecheck().normalize().to_expr_alpha();
+ let expr = expr.typecheck()?.normalize().to_expr_alpha();
assert_eq_display!(expr, expected.to_expr());
}
}
@@ -226,10 +225,15 @@ pub fn run_test(
}
Normalization | AlphaNormalization => unreachable!(),
Typecheck | TypeInference => {
- parse_file_str(&file_path)?
- .skip_resolve()?
- .typecheck()
- .unwrap_err();
+ let res =
+ parse_file_str(&file_path)?.skip_resolve()?.typecheck();
+ match res {
+ Err(_) => {}
+ // If e did typecheck, check that it doesn't have a type
+ Ok(e) => {
+ e.get_type().unwrap_err();
+ }
+ }
}
}
}