diff options
Diffstat (limited to 'dhall/src')
| -rw-r--r-- | dhall/src/typecheck.rs | 133 |
1 files changed, 133 insertions, 0 deletions
diff --git a/dhall/src/typecheck.rs b/dhall/src/typecheck.rs index 90809af..bca098f 100644 --- a/dhall/src/typecheck.rs +++ b/dhall/src/typecheck.rs @@ -1128,6 +1128,139 @@ 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] |