diff --git a/crates/sempai/src/tests/property_tests.rs b/crates/sempai/src/tests/property_tests.rs index 1fb99d4b..08a1f2dc 100644 --- a/crates/sempai/src/tests/property_tests.rs +++ b/crates/sempai/src/tests/property_tests.rs @@ -12,6 +12,7 @@ use crate::semantic_check::validate_formula; const MAX_DEPTH: u32 = 5; const MAX_SIZE: u32 = 32; const MAX_BRANCHES: u32 = 3; +const MIN_PROPERTY_DEPTH: usize = 4; fn decorated(node: Formula, span: Option) -> Decorated { Decorated { @@ -50,6 +51,75 @@ fn atom_strategy() -> BoxedStrategy> { .boxed() } +fn unary_node(variant: u8, child: Decorated) -> Formula { + match variant { + 0 => Formula::Not(Box::new(child)), + 1 => Formula::Inside(Box::new(child)), + _ => Formula::Anywhere(Box::new(child)), + } +} + +fn valid_unary_node(is_inside: bool, child: Decorated) -> Formula { + if is_inside { + Formula::Inside(Box::new(child)) + } else { + Formula::Anywhere(Box::new(child)) + } +} + +fn deep_atom(min_depth: usize) -> BoxedStrategy> { + if min_depth <= 1 { + return atom_strategy(); + } + + (any::(), deep_atom(min_depth - 1), span_strategy()) + .prop_map(|(is_inside, child, span)| decorated(valid_unary_node(is_inside, child), span)) + .boxed() +} + +fn deep_constraint_atom(min_depth: usize) -> BoxedStrategy> { + if min_depth <= 1 { + return atom_strategy(); + } + + ( + any::(), + deep_constraint_atom(min_depth - 1), + span_strategy(), + ) + .prop_map(|(is_not, child, span)| { + let node = if is_not { + Formula::Not(Box::new(child)) + } else { + Formula::Inside(Box::new(child)) + }; + decorated(node, span) + }) + .boxed() +} + +fn deep_positive_atom(min_depth: usize) -> BoxedStrategy> { + if min_depth <= 1 { + return atom_strategy(); + } + + (deep_positive_atom(min_depth - 1), span_strategy()) + .prop_map(|(child, span)| decorated(Formula::Or(vec![child]), span)) + .boxed() +} + +fn deep_atomless(min_depth: usize) -> BoxedStrategy> { + if min_depth <= 1 { + return span_strategy() + .prop_map(|span| decorated(Formula::And(vec![]), span)) + .boxed(); + } + + (0_u8..3, deep_atomless(min_depth - 1), span_strategy()) + .prop_map(|(variant, child, span)| decorated(unary_node(variant, child), span)) + .boxed() +} + fn formula_tree() -> BoxedStrategy> { atom_strategy() .prop_recursive(MAX_DEPTH, MAX_SIZE, MAX_BRANCHES, |inner| { @@ -81,26 +151,39 @@ fn formula_tree() -> BoxedStrategy> { } fn tree_with_not() -> BoxedStrategy> { - (formula_tree(), span_strategy()) + (deep_atom(MIN_PROPERTY_DEPTH - 1), span_strategy()) .prop_map(|(child, span)| decorated(Formula::Not(Box::new(child)), span)) .boxed() } -fn or_with_not_descendant() -> BoxedStrategy> { +fn nary_with_required_branch( + sibling: S, + required: R, + wrap: W, +) -> BoxedStrategy> +where + S: Strategy> + Clone + 'static, + R: Strategy> + 'static, + W: Fn(Vec>) -> Formula + Send + Sync + Clone + 'static, +{ ( - vec(formula_tree(), 0..=2), - tree_with_not(), - vec(formula_tree(), 0..=2), + vec(sibling.clone(), 0..=2), + required, + vec(sibling, 0..=2), span_strategy(), ) - .prop_map(|(mut before, not_branch, after, span)| { - before.push(not_branch); + .prop_map(move |(mut before, required_branch, after, span)| { + before.push(required_branch); before.extend(after); - decorated(Formula::Or(before), span) + decorated(wrap(before), span) }) .boxed() } +fn or_with_not_descendant() -> BoxedStrategy> { + nary_with_required_branch(formula_tree(), tree_with_not(), Formula::Or) +} + fn atomless_tree_without_not_in_or() -> BoxedStrategy> { let leaf = span_strategy() .prop_map(|span| decorated(Formula::And(vec![]), span)) @@ -123,16 +206,15 @@ fn atomless_tree_without_not_in_or() -> BoxedStrategy> { } fn and_without_positive_descendant() -> BoxedStrategy> { - ( - vec(atomless_tree_without_not_in_or(), 0..=MAX_BRANCHES as usize), - span_strategy(), + nary_with_required_branch( + atomless_tree_without_not_in_or(), + deep_atomless(MIN_PROPERTY_DEPTH - 1), + Formula::And, ) - .prop_map(|(branches, span)| decorated(Formula::And(branches), span)) - .boxed() } fn valid_no_not_tree() -> BoxedStrategy> { - atom_strategy() + deep_atom(MIN_PROPERTY_DEPTH) .prop_recursive(MAX_DEPTH, MAX_SIZE, MAX_BRANCHES, |inner| { let unary = (any::(), inner.clone(), span_strategy()).prop_map( |(is_inside, child, span)| { @@ -152,17 +234,18 @@ fn valid_no_not_tree() -> BoxedStrategy> { } fn positive_tree() -> BoxedStrategy> { - atom_strategy() + deep_positive_atom(MIN_PROPERTY_DEPTH) .prop_recursive(MAX_DEPTH, MAX_SIZE, MAX_BRANCHES, |inner| { - let constraint = - (0_u8..3, atom_strategy(), span_strategy()).prop_map(|(variant, child, span)| { + let constraint = (0_u8..3, deep_constraint_atom(2), span_strategy()).prop_map( + |(variant, child, span)| { let node = match variant { 0 => Formula::Not(Box::new(child)), 1 => Formula::Inside(Box::new(child)), _ => Formula::Anywhere(Box::new(child)), }; decorated(node, span) - }); + }, + ); let and = ( vec(prop_oneof![inner.clone(), constraint], 0..=2), inner.clone(), @@ -176,7 +259,7 @@ fn positive_tree() -> BoxedStrategy> { }); let or = ( vec(valid_no_not_tree(), 0..=2), - atom_strategy(), + deep_positive_atom(MIN_PROPERTY_DEPTH - 1), vec(valid_no_not_tree(), 0..=2), span_strategy(), ) @@ -190,6 +273,18 @@ fn positive_tree() -> BoxedStrategy> { .boxed() } +fn tree_depth(formula: &Decorated) -> usize { + match &formula.node { + Formula::Atom(_) => 1, + Formula::Not(inner) | Formula::Inside(inner) | Formula::Anywhere(inner) => { + 1 + tree_depth(inner) + } + Formula::And(branches) | Formula::Or(branches) => { + 1 + branches.iter().map(tree_depth).max().unwrap_or_default() + } + } +} + fn first_diagnostic_code(formula: &Decorated) -> DiagnosticCode { let err = validate_formula(formula).expect_err("formula should fail validation"); err.diagnostics() @@ -207,6 +302,8 @@ proptest! { #[test] fn prop_or_branch_containing_negation_is_rejected(formula in or_with_not_descendant()) { + prop_assert!(tree_depth(&formula) >= MIN_PROPERTY_DEPTH); + prop_assert_eq!( first_diagnostic_code(&formula), DiagnosticCode::ESempaiInvalidNotInOr @@ -215,6 +312,8 @@ proptest! { #[test] fn prop_and_with_no_positive_term_is_rejected(formula in and_without_positive_descendant()) { + prop_assert!(tree_depth(&formula) >= MIN_PROPERTY_DEPTH); + let expected_span = formula .span .clone() @@ -234,6 +333,8 @@ proptest! { #[test] fn prop_valid_tree_with_positive_in_every_and_is_ok(formula in positive_tree()) { + prop_assert!(tree_depth(&formula) >= MIN_PROPERTY_DEPTH); + prop_assert!(validate_formula(&formula).is_ok()); } }