From ff1bee1b115a5b9528be621502719cc4faeffaee Mon Sep 17 00:00:00 2001
From: Nadrieril
Date: Thu, 25 Apr 2019 14:26:19 +0200
Subject: Try property testing against reference implementation

---
 dhall/Cargo.toml       |   1 +
 dhall/src/typecheck.rs | 133 +++++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 134 insertions(+)

(limited to 'dhall')

diff --git a/dhall/Cargo.toml b/dhall/Cargo.toml
index de2ab7c..e2f3f6b 100644
--- a/dhall/Cargo.toml
+++ b/dhall/Cargo.toml
@@ -19,6 +19,7 @@ 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 90809af..bca098f 100644
--- a/dhall/src/typecheck.rs
+++ b/dhall/src/typecheck.rs
@@ -1127,6 +1127,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]
-- 
cgit v1.2.3