| 426 | num_nested: Nat::from(0u64), |
| 427 | is_rec: false, |
| 428 | is_unsafe: false, |
| 429 | is_reflexive: false, |
| 430 | }), |
| 431 | ); |
| 432 | } |
| 433 | |
| 434 | let graph = build_ref_graph(&env); |
| 435 | assert!(!graph.out_refs[&n("A")].contains(&n("B"))); |
| 436 | assert!(!graph.out_refs[&n("B")].contains(&n("A"))); |
| 437 | } |
| 438 | |
| 439 | #[test] |
| 440 | fn ctor_includes_induct() { |
| 441 | // Constructor T.mk references its parent T |
| 442 | let mut env = Env::default(); |
| 443 | env.insert( |
| 444 | n("T"), |
| 445 | ConstantInfo::AxiomInfo(AxiomVal { cnst: mk_cv("T"), is_unsafe: false }), |
| 446 | ); |
| 447 | env.insert( |
| 448 | n("T.mk"), |
| 449 | ConstantInfo::CtorInfo(ConstructorVal { |
| 450 | cnst: mk_cv("T.mk"), |
| 451 | induct: n("T"), |
| 452 | cidx: Nat::from(0u64), |
| 453 | num_params: Nat::from(0u64), |
| 454 | num_fields: Nat::from(0u64), |
| 455 | is_unsafe: false, |
| 456 | }), |
| 457 | ); |
| 458 | let graph = build_ref_graph(&env); |
| 459 | assert!(graph.out_refs[&n("T.mk")].contains(&n("T"))); |
| 460 | } |
| 461 | |
| 462 | #[test] |
| 463 | fn in_refs_bidirectional() { |
| 464 | // A -> B, C -> B |
| 465 | let mut env = Env::default(); |
| 466 | let b_ref = Expr::cnst(n("B"), vec![]); |
| 467 | env.insert( |
| 468 | n("B"), |
| 469 | ConstantInfo::AxiomInfo(AxiomVal { cnst: mk_cv("B"), is_unsafe: false }), |
| 470 | ); |