use super::*;
#[test]
fn test_be_arg_da_with_universal_stays_innermost() {
let predicates = vec![
Predicate::Root("goes".into()), Predicate::WithArgs((0, vec![1])), Predicate::Root("dog".into()), ];
let arguments = vec![
Argument::Description((Determiner::Every, 2)), Argument::Variable("$da".into()), ];
let proposition = Proposition {
relation: 1,
terms: vec![0],
x1_present: true,
negated: false,
tense: None,
deontic: None,
};
let (form, compiler) = compile_one(predicates, arguments, proposition);
assert!(compiler.errors.is_empty(), "errors: {:?}", compiler.errors);
assert_eq!(
binder_spine(&form, &compiler).first(),
Some(&Binder::ForAll),
"root must stay ForAll (nibli-reason rule shape)"
);
assert!(
!exists_outscopes_forall(&form, "$da", &compiler),
"a be-arg `da` is closed innermost, under the universal"
);
assert_eq!(count_exists_binding(&form, "$da", &compiler), 1);
assert!(free_vars(&form, &compiler).is_empty());
}