| 369 | |
| 370 | #[test] |
| 371 | fn test_structural_unification() { |
| 372 | let mut arena = Arena::new(); |
| 373 | let env = Environment::new(); |
| 374 | let ctx = Context::new(); |
| 375 | let mut unifier = Unifier::new(); |
| 376 | |
| 377 | // App(?0, x) = App(y, x) => ?0 = y |
| 378 | let mvar0 = arena.mk_mvar(MetaVarId::new(0)); |
| 379 | let x = arena.mk_var(0); |
| 380 | let y = arena.mk_var(1); |
| 381 | |
| 382 | let app1 = arena.mk_app(mvar0, x); |
| 383 | let app2 = arena.mk_app(y, x); |
| 384 | |
| 385 | unifier.unify(app1, app2); |
| 386 | |
| 387 | unifier.solve(&mut arena, &env, &ctx).unwrap(); |
| 388 | |
| 389 | let assignment = unifier.substitution().lookup(MetaVarId::new(0)).unwrap(); |
| 390 | assert_eq!(assignment, y); |
| 391 | } |
| 392 | } |