summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorNadrieril2020-02-02 18:27:00 +0000
committerNadrieril2020-02-02 18:36:06 +0000
commit488bce275f104384282a0867aeaad011ae8cf48c (patch)
tree8c9d117635ffe60781dfac31b7c612ee172e1b71
parentb7b5a0d27eb0cccdcd0c532a7042b3514eacbe40 (diff)
Add local test files on top of dhall-lang tests
-rw-r--r--dhall/build.rs102
-rw-r--r--dhall/src/semantics/tck/typecheck.rs1
-rw-r--r--dhall/src/tests.rs3
-rw-r--r--dhall/tests/type-errors/SortInLet.txt1
-rw-r--r--dhall/tests/type-inference/failure/SortInLet.dhall1
-rw-r--r--tests_buffer14
6 files changed, 68 insertions, 54 deletions
diff --git a/dhall/build.rs b/dhall/build.rs
index 8992f22..9cc07ea 100644
--- a/dhall/build.rs
+++ b/dhall/build.rs
@@ -2,7 +2,7 @@ use std::env;
use std::ffi::OsString;
use std::fs::{read_to_string, File};
use std::io::{BufRead, BufReader, Write};
-use std::path::{Path, PathBuf};
+use std::path::Path;
use walkdir::WalkDir;
use abnf_to_pest::render_rules_to_pest;
@@ -24,7 +24,7 @@ impl FileType {
fn dhall_files_in_dir<'a>(
dir: &'a Path,
- take_a_suffix: bool,
+ take_ab_suffix: bool,
filetype: FileType,
) -> impl Iterator<Item = (String, String)> + 'a {
WalkDir::new(dir)
@@ -38,14 +38,14 @@ fn dhall_files_in_dir<'a>(
}
let path = path.to_string_lossy();
let path = &path[..path.len() - 1 - ext.len()];
- let path = if take_a_suffix && &path[path.len() - 1..] != "A" {
+ let path = if take_ab_suffix && &path[path.len() - 1..] != "A" {
return None;
- } else if take_a_suffix {
+ } else if take_ab_suffix {
path[..path.len() - 1].to_owned()
} else {
path.to_owned()
};
- // Transform path into a valie Rust identifier
+ // Transform path into a valid Rust identifier
let name = path.replace("/", "_").replace("-", "_");
Some((name, path))
})
@@ -54,8 +54,8 @@ fn dhall_files_in_dir<'a>(
struct TestFeature {
/// Name of the module, used in the output of `cargo test`
module_name: &'static str,
- /// Directory containing the tests files
- directory: PathBuf,
+ /// Directory containing the tests files, relative to the base tests directory
+ directory: &'static str,
/// Relevant variant of `dhall::tests::Test`
variant: &'static str,
/// Given a file name, whether to exclude it
@@ -68,34 +68,43 @@ struct TestFeature {
fn make_test_module(
w: &mut impl Write, // Where to output the generated code
+ base_paths: &[&Path],
mut feature: TestFeature,
) -> std::io::Result<()> {
- let tests_dir = feature.directory;
writeln!(w, "mod {} {{", feature.module_name)?;
- let take_a_suffix = feature.output_type.is_some();
- for (name, path) in
- dhall_files_in_dir(&tests_dir, take_a_suffix, feature.input_type)
- {
- if (feature.path_filter)(&path) {
- continue;
- }
- let path = tests_dir.join(path);
- let path = path.to_string_lossy();
- let test = match feature.output_type {
- None => {
- let input_file =
- format!("\"{}.{}\"", path, feature.input_type.to_ext());
- format!("{}({})", feature.variant, input_file)
- }
- Some(output_type) => {
- let input_file =
- format!("\"{}A.{}\"", path, feature.input_type.to_ext());
- let output_file =
- format!("\"{}B.{}\"", path, output_type.to_ext());
- format!("{}({}, {})", feature.variant, input_file, output_file)
+ let take_ab_suffix = feature.output_type.is_some();
+ for base_path in base_paths {
+ let tests_dir = base_path.join(feature.directory);
+ for (name, path) in
+ dhall_files_in_dir(&tests_dir, take_ab_suffix, feature.input_type)
+ {
+ if (feature.path_filter)(&path) {
+ continue;
}
- };
- writeln!(w, "make_spec_test!({}, {});", test, name)?;
+ let path = tests_dir.join(path);
+ let path = path.to_string_lossy();
+ let test = match feature.output_type {
+ None => {
+ let input_file =
+ format!("\"{}.{}\"", path, feature.input_type.to_ext());
+ format!("{}({})", feature.variant, input_file)
+ }
+ Some(output_type) => {
+ let input_file = format!(
+ "\"{}A.{}\"",
+ path,
+ feature.input_type.to_ext()
+ );
+ let output_file =
+ format!("\"{}B.{}\"", path, output_type.to_ext());
+ format!(
+ "{}({}, {})",
+ feature.variant, input_file, output_file
+ )
+ }
+ };
+ writeln!(w, "make_spec_test!({}, {});", test, name)?;
+ }
}
writeln!(w, "}}")?;
Ok(())
@@ -111,12 +120,13 @@ fn generate_tests() -> std::io::Result<()> {
let out_dir = env::var("OUT_DIR").unwrap();
let parser_tests_path = Path::new(&out_dir).join("spec_tests.rs");
- let spec_tests_dir = Path::new("../dhall-lang/tests/");
+ let spec_tests_dirs =
+ vec![Path::new("../dhall-lang/tests/"), Path::new("tests/")];
let tests = vec![
TestFeature {
module_name: "parser_success",
- directory: spec_tests_dir.join("parser/success/"),
+ directory: "parser/success/",
variant: "ParserSuccess",
path_filter: Box::new(|path: &str| {
false
@@ -134,7 +144,7 @@ fn generate_tests() -> std::io::Result<()> {
},
TestFeature {
module_name: "parser_failure",
- directory: spec_tests_dir.join("parser/failure/"),
+ directory: "parser/failure/",
variant: "ParserFailure",
path_filter: Box::new(|_path: &str| false),
input_type: FileType::Text,
@@ -142,7 +152,7 @@ fn generate_tests() -> std::io::Result<()> {
},
TestFeature {
module_name: "printer",
- directory: spec_tests_dir.join("parser/success/"),
+ directory: "parser/success/",
variant: "Printer",
path_filter: Box::new(|path: &str| {
false
@@ -158,7 +168,7 @@ fn generate_tests() -> std::io::Result<()> {
},
TestFeature {
module_name: "binary_encoding",
- directory: spec_tests_dir.join("parser/success/"),
+ directory: "parser/success/",
variant: "BinaryEncoding",
path_filter: Box::new(|path: &str| {
false
@@ -180,7 +190,7 @@ fn generate_tests() -> std::io::Result<()> {
},
TestFeature {
module_name: "binary_decoding_success",
- directory: spec_tests_dir.join("binary-decode/success/"),
+ directory: "binary-decode/success/",
variant: "BinaryDecodingSuccess",
path_filter: Box::new(|path: &str| {
false
@@ -194,7 +204,7 @@ fn generate_tests() -> std::io::Result<()> {
},
TestFeature {
module_name: "binary_decoding_failure",
- directory: spec_tests_dir.join("binary-decode/failure/"),
+ directory: "binary-decode/failure/",
variant: "BinaryDecodingFailure",
path_filter: Box::new(|_path: &str| false),
input_type: FileType::Binary,
@@ -202,7 +212,7 @@ fn generate_tests() -> std::io::Result<()> {
},
TestFeature {
module_name: "import_success",
- directory: spec_tests_dir.join("import/success/"),
+ directory: "import/success/",
variant: "ImportSuccess",
path_filter: Box::new(|path: &str| {
false
@@ -221,7 +231,7 @@ fn generate_tests() -> std::io::Result<()> {
},
TestFeature {
module_name: "import_failure",
- directory: spec_tests_dir.join("import/failure/"),
+ directory: "import/failure/",
variant: "ImportFailure",
path_filter: Box::new(|path: &str| {
false
@@ -237,7 +247,7 @@ fn generate_tests() -> std::io::Result<()> {
},
TestFeature {
module_name: "beta_normalize",
- directory: spec_tests_dir.join("normalization/success/"),
+ directory: "normalization/success/",
variant: "Normalization",
path_filter: Box::new(|path: &str| {
// We don't support bignums
@@ -282,7 +292,7 @@ fn generate_tests() -> std::io::Result<()> {
},
TestFeature {
module_name: "alpha_normalize",
- directory: spec_tests_dir.join("alpha-normalization/success/"),
+ directory: "alpha-normalization/success/",
variant: "AlphaNormalization",
path_filter: Box::new(|path: &str| {
// This test doesn't typecheck
@@ -293,7 +303,7 @@ fn generate_tests() -> std::io::Result<()> {
},
TestFeature {
module_name: "type_inference_success",
- directory: spec_tests_dir.join("type-inference/success/"),
+ directory: "type-inference/success/",
variant: "TypeInferenceSuccess",
path_filter: Box::new(|path: &str| {
false
@@ -317,7 +327,7 @@ fn generate_tests() -> std::io::Result<()> {
},
TestFeature {
module_name: "type_inference_failure",
- directory: spec_tests_dir.join("type-inference/failure/"),
+ directory: "type-inference/failure/",
variant: "TypeInferenceFailure",
path_filter: Box::new(|path: &str| {
false
@@ -347,7 +357,7 @@ fn generate_tests() -> std::io::Result<()> {
},
TestFeature {
module_name: "type_error",
- directory: spec_tests_dir.join("type-inference/failure/"),
+ directory: "type-inference/failure/",
variant: "TypeError",
path_filter: Box::new(|path: &str| {
false
@@ -379,7 +389,7 @@ fn generate_tests() -> std::io::Result<()> {
let mut file = File::create(parser_tests_path)?;
for test in tests {
- make_test_module(&mut file, test)?;
+ make_test_module(&mut file, &spec_tests_dirs, test)?;
}
Ok(())
diff --git a/dhall/src/semantics/tck/typecheck.rs b/dhall/src/semantics/tck/typecheck.rs
index 9a1d0d8..11c07d8 100644
--- a/dhall/src/semantics/tck/typecheck.rs
+++ b/dhall/src/semantics/tck/typecheck.rs
@@ -680,6 +680,7 @@ pub(crate) fn type_with(
val.clone()
};
let val = type_with(env, &val)?;
+ val.get_type()?; // Ensure val is not Sort
let val_nf = val.eval(&env.as_nzenv());
let body_env = env.insert_value(&binder, val_nf);
let body = type_with(&body_env, body)?;
diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs
index 8216243..8136625 100644
--- a/dhall/src/tests.rs
+++ b/dhall/src/tests.rs
@@ -179,6 +179,9 @@ pub fn run_test(test: Test<'_>) -> Result<()> {
let file_path = PathBuf::from(file_path);
let error_file_path = file_path
.strip_prefix("../dhall-lang/tests/type-inference/failure/")
+ .or_else(|_| {
+ file_path.strip_prefix("tests/type-inference/failure/")
+ })
.unwrap();
let error_file_path =
PathBuf::from("tests/type-errors/").join(error_file_path);
diff --git a/dhall/tests/type-errors/SortInLet.txt b/dhall/tests/type-errors/SortInLet.txt
new file mode 100644
index 0000000..5b88ff7
--- /dev/null
+++ b/dhall/tests/type-errors/SortInLet.txt
@@ -0,0 +1 @@
+Type error: Unhandled error: Sort
diff --git a/dhall/tests/type-inference/failure/SortInLet.dhall b/dhall/tests/type-inference/failure/SortInLet.dhall
new file mode 100644
index 0000000..b19b882
--- /dev/null
+++ b/dhall/tests/type-inference/failure/SortInLet.dhall
@@ -0,0 +1 @@
+let x = Sort in 0
diff --git a/tests_buffer b/tests_buffer
index 87d73ef..e8eb3d7 100644
--- a/tests_buffer
+++ b/tests_buffer
@@ -14,7 +14,7 @@ success/
EmptyRecordLiteral {=}
ToMap toMap x
ToMapAnnot toMap x : T
- VariableQuotedSpace ` x `
+ VariableQuotedWithSpace ` x `
failure/
AssertNoAnnotation assert
@@ -47,19 +47,17 @@ success/
somehow test that ({ x = { z = 1 } } ∧ { x = { y = 2 } }).x has a type
somehow test that the recordtype from List/indexed has a type in both empty and nonempty cases
somehow test types added to the Foo/build closures
- λ(x : ∀(a : Type) → a) → x
- let X = 0 in λ(T : Type) → λ(x : T) → 1
- (λ(T : Type) → let foo = 0 in λ(x : T) → x) : ∀(T : Type) → ∀(x : T) → T
+ λ(todo : ∀(a : Type) → a) → todo
+ let T = 0 in λ(T : Type) → λ(x : T) → 1
+ (λ(T : Type) → let x = 0 in λ(x : T) → x) : ∀(T : Type) → ∀(x : T) → T
failure/
\(_: Bool) -> assert : (\(_: Bool) -> _) === (\(x: Bool) -> _)
- \(x: let x = 1 in Sort) -> 0
merge { x = λ(x : Bool) → x } (< x: Bool | y: Natural >.x True)
merge { x = λ(_ : Bool) → _, y = 1 } < x = True | y >
merge { x = True, y = 1 } < x | y >.x
merge {x=...,y=...} <x>.x
merge {x=...,y=...} <x:T>.x
- MergeBoolIsNotUnion merge x True
- MergeOptionalIsNotUnion merge x (Some 1)
- SortInLet let x = Sort in 1
+ MergeBool merge x True
+ LetInSort \(x: let x = 0 in Sort) -> 1
equivalence: