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, 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]