summaryrefslogtreecommitdiff
path: root/dhall/src
diff options
context:
space:
mode:
Diffstat (limited to 'dhall/src')
-rw-r--r--dhall/src/typecheck.rs133
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]