Add local test files on top of dhall-lang tests

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: