diff options
Diffstat (limited to 'dhall/src')
| -rw-r--r-- | dhall/src/typecheck.rs | 133 |
1 files changed, 0 insertions, 133 deletions
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index bca098f..90809af 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -1128,139 +1128,6 @@ impl fmt::Display for TypeMessage<'static> { } #[cfg(test)] -mod proptests { - use proptest::prelude::*; - - use crate::traits::DynamicType; - use dhall_core::*; - use dhall_generator as dhall; - - fn typecheck_using_external_dhall( - expr: &SubExpr<X, X>, - ) -> Result<SubExpr<X, X>, crate::error::Error> { - use std::io::Write; - use std::process::{Command, Stdio}; - - let expr_str = expr.to_string(); - let mut child = Command::new("dhall") - .arg("type") - .stdin(Stdio::piped()) - .stdout(Stdio::piped()) - .stderr(Stdio::piped()) - .spawn()?; - - { - let stdin = child.stdin.as_mut().unwrap(); - stdin.write_all(expr_str.as_bytes())?; - } - - let output = child.wait_with_output()?; - if !output.status.success() { - // I'm lazy - Err(crate::error::Error::Deserialize( - String::from_utf8_lossy(&output.stderr).into_owned(), - ))? - } - let output_str = String::from_utf8_lossy(&output.stdout); - let ty = crate::expr::Parsed::parse_str(&output_str)? - .skip_resolve()? - .skip_typecheck() - .skip_normalize() - .into_expr(); - Ok(ty) - } - - prop_compose! { - fn label_strategy()(id in 0usize..2usize) -> Label { - let name = match id { - 0 => "a", - _ => "b", - }; - name.into() - } - } - - fn type_strategy() -> impl Strategy<Value = SubExpr<X, X>> { - let leaf = prop_oneof![ - Just(rc(ExprF::Builtin(Builtin::Bool))), - Just(rc(ExprF::Const(Const::Type))), - Just(rc(ExprF::Const(Const::Kind))), - (label_strategy(), 0usize..3usize) - .prop_map(|(name, id)| { rc(ExprF::Var(V(name, id))) }), - ]; - leaf.prop_recursive( - 5, // 8 levels deep - 32, // Shoot for maximum size of 256 nodes - 2, // We put up to 4 items per collection - |inner| { - prop_oneof![ - (label_strategy(), inner.clone(), inner.clone()) - .prop_map(|(x, t, e)| rc(ExprF::Pi(x, t, e))), - inner.clone().prop_map(|e| dhall::subexpr!({ x: e })), - ] - }, - ) - } - - fn expr_strategy() -> impl Strategy<Value = SubExpr<X, X>> { - let leaf = prop_oneof![ - (label_strategy(), 0usize..3usize) - .prop_map(|(name, id)| { rc(ExprF::Var(V(name, id))) }), - any::<bool>().prop_map(|b| rc(ExprF::BoolLit(b))), - ]; - leaf.prop_recursive( - 8, // 8 levels deep - 256, // Shoot for maximum size of 256 nodes - 2, // We put up to 4 items per collection - |inner| { - prop_oneof![ - (label_strategy(), type_strategy(), inner.clone()) - .prop_map(|(x, t, e)| rc(ExprF::Lam(x, t, e))), - (inner.clone(), inner.clone()) - .prop_map(|(f, a)| rc(ExprF::App(f, a))), - inner.clone().prop_map(|e| rc(ExprF::Field(e, "x".into()))), - inner.clone().prop_map(|e| dhall::subexpr!({ x = e })), - ] - }, - ) - } - - // proptest! { - // #![proptest_config(ProptestConfig { - // max_global_rejects: 1000000, - // cases: 256, - // ..ProptestConfig::default() - // })] - // #[test] - // fn proptest_compare(expr in expr_strategy()) { - // let output_expr_err = typecheck_using_external_dhall(&expr); - // prop_assume!(output_expr_err.is_ok()); - // let output_expr = output_expr_err.unwrap(); - // let expected: SubExpr<X, X> = super::type_of(expr.embed_absurd()) - // .unwrap() - // .get_type() - // .unwrap() - // .into_owned() - // .into_normalized() - // .unwrap() - // .into_expr(); - // prop_assert_eq!(output_expr, expected); - // } - // } - - proptest! { - #![proptest_config(ProptestConfig { - cases: 256, - ..ProptestConfig::default() - })] - #[test] - fn proptest_alone(expr in expr_strategy()) { - super::type_of(expr.embed_absurd()); - } - } -} - -#[cfg(test)] mod spec_tests { #![rustfmt::skip] |