From c448698f797f2304dca0e0b8b833959de00ca079 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 20 Jan 2020 15:27:19 +0000 Subject: Reimplement basic tck/nze with proper environments Inspired from dhall_haskell --- dhall/src/tests.rs | 19 +++++++++++++------ 1 file changed, 13 insertions(+), 6 deletions(-) (limited to 'dhall/src/tests.rs') diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs index f1648cf..d86574a 100644 --- a/dhall/src/tests.rs +++ b/dhall/src/tests.rs @@ -158,9 +158,12 @@ pub fn run_test(test: Test<'_>) -> Result<()> { parse_file_str(&file_path)?.resolve().unwrap_err(); } TypeInferenceSuccess(expr_file_path, expected_file_path) => { - let expr = - parse_file_str(&expr_file_path)?.resolve()?.typecheck()?; - let ty = expr.get_type()?.to_expr(); + // let expr = + // parse_file_str(&expr_file_path)?.resolve()?.typecheck()?; + // let ty = expr.get_type()?.to_expr(); + let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr(); + let tyexpr = crate::semantics::nze::nzexpr::typecheck(expr)?; + let ty = tyexpr.get_type()?.to_expr(); let expected = parse_file_str(&expected_file_path)?.to_expr(); assert_eq_display!(ty, expected); } @@ -203,9 +206,13 @@ pub fn run_test(test: Test<'_>) -> Result<()> { } } Normalization(expr_file_path, expected_file_path) => { - let expr = parse_file_str(&expr_file_path)? - .resolve()? - .typecheck()? + // let expr = parse_file_str(&expr_file_path)? + // .resolve()? + // .typecheck()? + // .normalize() + // .to_expr(); + let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr(); + let expr = crate::semantics::nze::nzexpr::typecheck(expr)? .normalize() .to_expr(); let expected = parse_file_str(&expected_file_path)?.to_expr(); -- cgit v1.2.3 From 015b24b04128cbf5a60fbc8ac3f526306ca27378 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 21 Jan 2020 17:43:44 +0000 Subject: Simplify type error type --- dhall/src/tests.rs | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) (limited to 'dhall/src/tests.rs') diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs index d86574a..7795d17 100644 --- a/dhall/src/tests.rs +++ b/dhall/src/tests.rs @@ -158,12 +158,12 @@ pub fn run_test(test: Test<'_>) -> Result<()> { parse_file_str(&file_path)?.resolve().unwrap_err(); } TypeInferenceSuccess(expr_file_path, expected_file_path) => { - // let expr = - // parse_file_str(&expr_file_path)?.resolve()?.typecheck()?; - // let ty = expr.get_type()?.to_expr(); - let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr(); - let tyexpr = crate::semantics::nze::nzexpr::typecheck(expr)?; - let ty = tyexpr.get_type()?.to_expr(); + let expr = + parse_file_str(&expr_file_path)?.resolve()?.typecheck()?; + let ty = expr.get_type()?.to_expr(); + // let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr(); + // let tyexpr = crate::semantics::nze::nzexpr::typecheck(expr)?; + // let ty = tyexpr.get_type()?.to_expr(); let expected = parse_file_str(&expected_file_path)?.to_expr(); assert_eq_display!(ty, expected); } @@ -206,15 +206,15 @@ pub fn run_test(test: Test<'_>) -> Result<()> { } } Normalization(expr_file_path, expected_file_path) => { - // let expr = parse_file_str(&expr_file_path)? - // .resolve()? - // .typecheck()? - // .normalize() - // .to_expr(); - let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr(); - let expr = crate::semantics::nze::nzexpr::typecheck(expr)? + let expr = parse_file_str(&expr_file_path)? + .resolve()? + .typecheck()? .normalize() .to_expr(); + // let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr(); + // let expr = crate::semantics::nze::nzexpr::typecheck(expr)? + // .normalize() + // .to_expr(); let expected = parse_file_str(&expected_file_path)?.to_expr(); assert_eq_display!(expr, expected); -- cgit v1.2.3 From 9e7cc77b6a25569b61340f39a2058e23cdc4a437 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 23 Jan 2020 22:22:01 +0000 Subject: Implement basic env-based normalization for Value-based TyExpr --- dhall/src/tests.rs | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) (limited to 'dhall/src/tests.rs') diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs index 7795d17..4928c51 100644 --- a/dhall/src/tests.rs +++ b/dhall/src/tests.rs @@ -206,11 +206,21 @@ pub fn run_test(test: Test<'_>) -> Result<()> { } } Normalization(expr_file_path, expected_file_path) => { + // let expr = parse_file_str(&expr_file_path)? + // .resolve()? + // .typecheck()? + // .normalize() + // .to_expr(); let expr = parse_file_str(&expr_file_path)? .resolve()? .typecheck()? - .normalize() - .to_expr(); + .to_value() + .to_tyexpr_noenv() + .normalize_whnf_noenv() + .to_expr(crate::semantics::phase::ToExprOptions { + alpha: false, + normalize: true, + }); // let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr(); // let expr = crate::semantics::nze::nzexpr::typecheck(expr)? // .normalize() -- cgit v1.2.3 From b72f0968ac19058b9cc513ab0ed1785133232a3d Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Fri, 24 Jan 2020 21:33:21 +0000 Subject: Implement basic typecheck with new approach --- dhall/src/tests.rs | 25 ++++++++++++++++--------- 1 file changed, 16 insertions(+), 9 deletions(-) (limited to 'dhall/src/tests.rs') diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs index 4928c51..994a134 100644 --- a/dhall/src/tests.rs +++ b/dhall/src/tests.rs @@ -211,20 +211,27 @@ pub fn run_test(test: Test<'_>) -> Result<()> { // .typecheck()? // .normalize() // .to_expr(); - let expr = parse_file_str(&expr_file_path)? - .resolve()? - .typecheck()? - .to_value() - .to_tyexpr_noenv() + // let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr(); + // let expr = crate::semantics::nze::nzexpr::typecheck(expr)? + // .normalize() + // .to_expr(); + // let expr = parse_file_str(&expr_file_path)? + // .resolve()? + // .typecheck()? + // .to_value() + // .to_tyexpr_noenv() + // .normalize_whnf_noenv() + // .to_expr(crate::semantics::phase::ToExprOptions { + // alpha: false, + // normalize: true, + // }); + let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr(); + let expr = crate::semantics::tck::typecheck::typecheck(expr)? .normalize_whnf_noenv() .to_expr(crate::semantics::phase::ToExprOptions { alpha: false, normalize: true, }); - // let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr(); - // let expr = crate::semantics::nze::nzexpr::typecheck(expr)? - // .normalize() - // .to_expr(); let expected = parse_file_str(&expected_file_path)?.to_expr(); assert_eq_display!(expr, expected); -- cgit v1.2.3 From 70e6e3a06c05cfe7d8ca3d6f072e7182639c147f Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Sat, 25 Jan 2020 10:15:17 +0000 Subject: Typecheck more cases --- dhall/src/tests.rs | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) (limited to 'dhall/src/tests.rs') diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs index 994a134..f51f6a8 100644 --- a/dhall/src/tests.rs +++ b/dhall/src/tests.rs @@ -158,12 +158,19 @@ pub fn run_test(test: Test<'_>) -> Result<()> { parse_file_str(&file_path)?.resolve().unwrap_err(); } TypeInferenceSuccess(expr_file_path, expected_file_path) => { - let expr = - parse_file_str(&expr_file_path)?.resolve()?.typecheck()?; - let ty = expr.get_type()?.to_expr(); + // let expr = + // parse_file_str(&expr_file_path)?.resolve()?.typecheck()?; + // let ty = expr.get_type()?.to_expr(); // let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr(); // let tyexpr = crate::semantics::nze::nzexpr::typecheck(expr)?; // let ty = tyexpr.get_type()?.to_expr(); + let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr(); + let ty = crate::semantics::tck::typecheck::typecheck(&expr)? + .get_type()? + .to_expr(crate::semantics::phase::ToExprOptions { + alpha: false, + normalize: true, + }); let expected = parse_file_str(&expected_file_path)?.to_expr(); assert_eq_display!(ty, expected); } @@ -226,7 +233,7 @@ pub fn run_test(test: Test<'_>) -> Result<()> { // normalize: true, // }); let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr(); - let expr = crate::semantics::tck::typecheck::typecheck(expr)? + let expr = crate::semantics::tck::typecheck::typecheck(&expr)? .normalize_whnf_noenv() .to_expr(crate::semantics::phase::ToExprOptions { alpha: false, -- cgit v1.2.3 From 5a835d9db35bf76858e178e1bd66e60128879629 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Mon, 27 Jan 2020 18:45:09 +0000 Subject: Fix a bunch of bugs and more tck --- dhall/src/tests.rs | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) (limited to 'dhall/src/tests.rs') diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs index f51f6a8..88c09cc 100644 --- a/dhall/src/tests.rs +++ b/dhall/src/tests.rs @@ -232,13 +232,10 @@ pub fn run_test(test: Test<'_>) -> Result<()> { // alpha: false, // normalize: true, // }); - let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr(); - let expr = crate::semantics::tck::typecheck::typecheck(&expr)? - .normalize_whnf_noenv() - .to_expr(crate::semantics::phase::ToExprOptions { - alpha: false, - normalize: true, - }); + let expr = parse_file_str(&expr_file_path)? + .resolve()? + .tck_and_normalize_new_flow()? + .to_expr(); let expected = parse_file_str(&expected_file_path)?.to_expr(); assert_eq_display!(expr, expected); -- cgit v1.2.3 From 8ced62a2cdde95c4d67298289756c12f53656df0 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Tue, 28 Jan 2020 18:41:20 +0000 Subject: Fix all sorts of variable shenanigans --- dhall/src/tests.rs | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) (limited to 'dhall/src/tests.rs') diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs index 88c09cc..971c48d 100644 --- a/dhall/src/tests.rs +++ b/dhall/src/tests.rs @@ -164,6 +164,7 @@ pub fn run_test(test: Test<'_>) -> Result<()> { // let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr(); // let tyexpr = crate::semantics::nze::nzexpr::typecheck(expr)?; // let ty = tyexpr.get_type()?.to_expr(); + // let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr(); let ty = crate::semantics::tck::typecheck::typecheck(&expr)? .get_type()? @@ -173,6 +174,23 @@ pub fn run_test(test: Test<'_>) -> Result<()> { }); let expected = parse_file_str(&expected_file_path)?.to_expr(); assert_eq_display!(ty, expected); + // + // let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr(); + // let ty = crate::semantics::tck::typecheck::typecheck(&expr)? + // .get_type()?; + // let expected = parse_file_str(&expected_file_path)?.to_expr(); + // let expected = crate::semantics::tck::typecheck::typecheck(&expected)? + // .normalize_whnf_noenv(); + // // if ty != expected { + // // assert_eq_display!(ty.to_expr(crate::semantics::phase::ToExprOptions { + // // alpha: false, + // // normalize: true, + // // }), expected.to_expr(crate::semantics::phase::ToExprOptions { + // // alpha: false, + // // normalize: true, + // // })) + // // } + // assert_eq_pretty!(ty, expected); } TypeInferenceFailure(file_path) => { let mut res = -- cgit v1.2.3 From f31ccaa40df77b1ca8b37db46a819460c831006e Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 29 Jan 2020 18:17:12 +0000 Subject: Fix more bugs --- dhall/src/tests.rs | 18 ++++++++++++++---- 1 file changed, 14 insertions(+), 4 deletions(-) (limited to 'dhall/src/tests.rs') diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs index 971c48d..1c687f6 100644 --- a/dhall/src/tests.rs +++ b/dhall/src/tests.rs @@ -193,13 +193,23 @@ pub fn run_test(test: Test<'_>) -> Result<()> { // assert_eq_pretty!(ty, expected); } TypeInferenceFailure(file_path) => { - let mut res = - parse_file_str(&file_path)?.skip_resolve()?.typecheck(); + // let mut res = + // parse_file_str(&file_path)?.skip_resolve()?.typecheck(); + // if let Ok(e) = &res { + // // If e did typecheck, check that get_type fails + // res = e.get_type(); + // } + // res.unwrap_err(); + + let res = crate::semantics::tck::typecheck::typecheck( + &parse_file_str(&file_path)?.skip_resolve()?.to_expr(), + ); if let Ok(e) = &res { // If e did typecheck, check that get_type fails - res = e.get_type(); + e.get_type().unwrap_err(); + } else { + res.unwrap_err(); } - res.unwrap_err(); } // Checks the output of the type error against a text file. If the text file doesn't exist, // we instead write to it the output we got. This makes it easy to update those files: just -- cgit v1.2.3 From 1e466a20533d936f44430b1bc18508cd00e5ccd2 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Wed, 29 Jan 2020 18:48:19 +0000 Subject: Use TyExpr in Typed --- dhall/src/tests.rs | 85 +++++++++--------------------------------------------- 1 file changed, 14 insertions(+), 71 deletions(-) (limited to 'dhall/src/tests.rs') diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs index 1c687f6..08feadf 100644 --- a/dhall/src/tests.rs +++ b/dhall/src/tests.rs @@ -158,65 +158,24 @@ pub fn run_test(test: Test<'_>) -> Result<()> { parse_file_str(&file_path)?.resolve().unwrap_err(); } TypeInferenceSuccess(expr_file_path, expected_file_path) => { - // let expr = - // parse_file_str(&expr_file_path)?.resolve()?.typecheck()?; - // let ty = expr.get_type()?.to_expr(); - // let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr(); - // let tyexpr = crate::semantics::nze::nzexpr::typecheck(expr)?; - // let ty = tyexpr.get_type()?.to_expr(); - // - let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr(); - let ty = crate::semantics::tck::typecheck::typecheck(&expr)? - .get_type()? - .to_expr(crate::semantics::phase::ToExprOptions { - alpha: false, - normalize: true, - }); + let expr = + parse_file_str(&expr_file_path)?.resolve()?.typecheck()?; + let ty = expr.get_type()?.to_expr(); let expected = parse_file_str(&expected_file_path)?.to_expr(); assert_eq_display!(ty, expected); - // - // let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr(); - // let ty = crate::semantics::tck::typecheck::typecheck(&expr)? - // .get_type()?; - // let expected = parse_file_str(&expected_file_path)?.to_expr(); - // let expected = crate::semantics::tck::typecheck::typecheck(&expected)? - // .normalize_whnf_noenv(); - // // if ty != expected { - // // assert_eq_display!(ty.to_expr(crate::semantics::phase::ToExprOptions { - // // alpha: false, - // // normalize: true, - // // }), expected.to_expr(crate::semantics::phase::ToExprOptions { - // // alpha: false, - // // normalize: true, - // // })) - // // } - // assert_eq_pretty!(ty, expected); } TypeInferenceFailure(file_path) => { - // let mut res = - // parse_file_str(&file_path)?.skip_resolve()?.typecheck(); - // if let Ok(e) = &res { - // // If e did typecheck, check that get_type fails - // res = e.get_type(); - // } - // res.unwrap_err(); - - let res = crate::semantics::tck::typecheck::typecheck( - &parse_file_str(&file_path)?.skip_resolve()?.to_expr(), - ); + let res = parse_file_str(&file_path)?.skip_resolve()?.typecheck(); if let Ok(e) = &res { // If e did typecheck, check that get_type fails e.get_type().unwrap_err(); - } else { - res.unwrap_err(); } } // Checks the output of the type error against a text file. If the text file doesn't exist, // we instead write to it the output we got. This makes it easy to update those files: just // `rm -r dhall/tests/type-errors` and run the tests again. TypeError(file_path) => { - let mut res = - parse_file_str(&file_path)?.skip_resolve()?.typecheck(); + let res = parse_file_str(&file_path)?.skip_resolve()?.typecheck(); let file_path = PathBuf::from(file_path); let error_file_path = file_path .strip_prefix("../dhall-lang/tests/type-inference/failure/") @@ -224,11 +183,13 @@ pub fn run_test(test: Test<'_>) -> Result<()> { let error_file_path = PathBuf::from("tests/type-errors/").join(error_file_path); let error_file_path = error_file_path.with_extension("txt"); - if let Ok(e) = &res { - // If e did typecheck, check that get_type fails - res = e.get_type(); - } - let err: Error = res.unwrap_err().into(); + let err: Error = match res { + Ok(e) => { + // If e did typecheck, check that get_type fails + e.get_type().unwrap_err().into() + } + Err(e) => e.into(), + }; if error_file_path.is_file() { let expected_msg = std::fs::read_to_string(error_file_path)?; @@ -241,28 +202,10 @@ pub fn run_test(test: Test<'_>) -> Result<()> { } } Normalization(expr_file_path, expected_file_path) => { - // let expr = parse_file_str(&expr_file_path)? - // .resolve()? - // .typecheck()? - // .normalize() - // .to_expr(); - // let expr = parse_file_str(&expr_file_path)?.resolve()?.to_expr(); - // let expr = crate::semantics::nze::nzexpr::typecheck(expr)? - // .normalize() - // .to_expr(); - // let expr = parse_file_str(&expr_file_path)? - // .resolve()? - // .typecheck()? - // .to_value() - // .to_tyexpr_noenv() - // .normalize_whnf_noenv() - // .to_expr(crate::semantics::phase::ToExprOptions { - // alpha: false, - // normalize: true, - // }); let expr = parse_file_str(&expr_file_path)? .resolve()? - .tck_and_normalize_new_flow()? + .typecheck()? + .normalize() .to_expr(); let expected = parse_file_str(&expected_file_path)?.to_expr(); -- cgit v1.2.3 From 5197c26c23edd6c499f8e0f8a239fe4393b2e3d2 Mon Sep 17 00:00:00 2001 From: Nadrieril Date: Thu, 30 Jan 2020 17:09:16 +0000 Subject: Move main API to lib.rs --- dhall/src/tests.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'dhall/src/tests.rs') diff --git a/dhall/src/tests.rs b/dhall/src/tests.rs index 08feadf..8216243 100644 --- a/dhall/src/tests.rs +++ b/dhall/src/tests.rs @@ -48,7 +48,7 @@ use std::io::{Read, Write}; use std::path::PathBuf; use crate::error::{Error, Result}; -use crate::semantics::phase::Parsed; +use crate::Parsed; #[allow(dead_code)] #[derive(Clone)] -- cgit v1.2.3