extern crate terms;
extern crate tree_automata as ta;

use terms::{Term, Pattern};
use ta::Automaton;

#[test]
fn simple_common_configurations() {
    let mut a = Automaton::new();

    let conf = Pattern::cons((), &[]);

    a.add(conf.clone(), (), true);
    a.add(conf.clone(), (), false);

    let automata = [&a, &a];
    let positions = [true.into(), false.into()];
    let patterns = [(), ()];

    let mut it = Automaton::common_configurations(
        &automata,
        &positions,
        &patterns,
        ()
    );

    assert!(it.next().is_some())
}

// #[test]
// fn synchronized_runs_depth0() {
//     let mut a = Automaton::new();
//
//     let conf = Pattern::cons((), &[]);
//
//     a.add(conf.clone(), (), true);
//     a.add(conf.clone(), (), false);
//
//     let automata = [&a, &a];
//     let positions = [true.into(), false.into()];
//     let patterns = [(), ()];
//     let constraints = ();
//
//     let term = Term::new((), &[]);
//
//     let mut it = Automaton::synchronized_runs(
//         &automata,
//         &positions,
//         &patterns,
//         &constraints
//     );
//
//     assert!(it.find(|(terms, _)| {
//         for t in terms.iter() {
//             if *t != term {
//                 return false
//             }
//         }
//
//         true
//     }).is_some())
// }
//
// #[test]
// fn synchronized_runs_depth1() {
//     let mut a = Automaton::new();
//
//     a.add(Pattern::cons('a', &[]), (), "ab");
//     a.add(Pattern::cons('b', &[]), (), "ab");
//
//     a.add(Pattern::cons('b', &[]), (), "bc");
//     a.add(Pattern::cons('c', &[]), (), "bc");
//
//     a.add(Pattern::cons('f', &["ab".into()]), (), "f(ab)");
//     a.add(Pattern::cons('f', &["bc".into()]), (), "f(bc)");
//
//     let automata = [&a, &a];
//     let positions = ["f(ab)".into(), "f(bc)".into()];
//     let patterns = [(), ()];
//     let constraints = ();
//
//     let term = Term::new('f', &[Term::new('b', &[])]);
//
//     let mut it = Automaton::synchronized_runs(
//         &automata,
//         &positions,
//         &patterns,
//         &constraints
//     );
//
//     // we should find term "f(b)"
//     assert!(it.find(|(terms, _)| {
//         for t in terms.iter() {
//             if *t != term {
//                 return false
//             }
//         }
//
//         true
//     }).is_some())
// }
//
// #[test]
// fn synchronized_runs_depth2() {
//     let mut a = Automaton::new();
//
//     a.add(Pattern::cons('a', &[]), (), "ab");
//     a.add(Pattern::cons('b', &[]), (), "ab");
//     a.add(Pattern::cons('b', &[]), (), "bc");
//     a.add(Pattern::cons('c', &[]), (), "bc");
//
//     assert!(a.configurations_for(&Pattern::cons('a', &[])).next().is_some());
//     assert!(a.configurations_for(&Pattern::cons('a', &[])).next().is_some());
//     assert!(a.configurations_for(&Pattern::cons('a', &[])).next().is_some());
//     assert!(a.configurations_for(&Pattern::cons('a', &[])).next().is_some());
//
//     a.add(Pattern::cons('i', &["ab".into()]), (), "i(ab)");
//     a.add(Pattern::cons('j', &["ab".into()]), (), "j(ab)");
//     a.add(Pattern::cons('k', &["ab".into()]), (), "k(ab)");
//     a.add(Pattern::cons('l', &["ab".into()]), (), "l(ab)");
//     a.add(Pattern::cons('l', &["bc".into()]), (), "l(bc)");
//     a.add(Pattern::cons('m', &["bc".into()]), (), "m(bc)");
//     a.add(Pattern::cons('n', &["bc".into()]), (), "n(bc)");
//     a.add(Pattern::cons('o', &["bc".into()]), (), "o(bc)");
//
//     a.add(Pattern::cons('f', &["i(ab)".into()]), (), "f(ij)|g(kl)");
//     a.add(Pattern::cons('f', &["j(ab)".into()]), (), "f(ij)|g(kl)");
//     a.add(Pattern::cons('g', &["k(ab)".into()]), (), "f(ij)|g(kl)");
//     a.add(Pattern::cons('g', &["l(ab)".into()]), (), "f(ij)|g(kl)");
//     a.add(Pattern::cons('g', &["l(bc)".into()]), (), "g(lm)|h(no)");
//     a.add(Pattern::cons('g', &["m(bc)".into()]), (), "g(lm)|h(no)");
//     a.add(Pattern::cons('h', &["n(bc)".into()]), (), "g(lm)|h(no)");
//     a.add(Pattern::cons('h', &["o(bc)".into()]), (), "g(lm)|h(no)");
//
//     let automata = [&a, &a];
//     let positions = ["f(ij)|g(kl)".into(), "g(lm)|h(no)".into()];
//     let patterns = [(), ()];
//     let constraints = ();
//
//     // g(l(b))
//     let term = Term::new('g', &[Term::new('l', &[Term::new('b', &[])])]);
//
//     let mut it = Automaton::synchronized_runs(
//         &automata,
//         &positions,
//         &patterns,
//         &constraints
//     );
//
//     // we should find term "g(l(b))"
//     let mut empty = true;
//     for (run, _) in it {
//         empty = false;
//         let t = run.first().unwrap();
//         println!("term: {:?}", t);
//         assert!(*t == term)
//     }
//     assert!(!empty);
// }