Revert "Try property testing against reference implementation"

This reverts commit ff1bee1b115a5b9528be621502719cc4faeffaee.

2 files changed, 0 insertions, 134 deletions

diff --git a/dhall/Cargo.toml b/dhall/Cargo.toml
index e2f3f6b..de2ab7c 100644
--- a/dhall/Cargo.toml
+++ b/dhall/Cargo.toml
@@ -19,7 +19,6 @@ dhall_generator = { path = "../dhall_generator" }
 [dev-dependencies]
 pretty_assertions = "0.6.1"
 stacker = "0.1.5"
-proptest = "0.9.2"
 
 [build-dependencies]
 walkdir = "2"
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]