struct Term<'a> {
    arguments: Vec<Term<'a>>,
    symbol: &'a str,
}

impl<'a> PartialEq for Term<'a> {
    fn eq(&self, other: &Term) -> bool {
        if self.symbol == other.symbol && self.arguments.len() == 0 && other.arguments.len() == 0 {
            return true;
        } else if self.symbol == other.symbol && self.arguments.len() == other.arguments.len() {
            for (idx, argument) in (self.arguments).iter().enumerate() {
                if *argument != other.arguments[idx] {
                    return false;
                }
            }
            return true;
        }
        false
    }
}

impl<'a> Term<'a> {
    fn new(symbol: &'a str, arguments: Vec<Term<'a>>) -> Term<'a> {
        Term {
            symbol: symbol,
            arguments: arguments,
        }
    }

    fn is_variable(self: &Term<'a>) -> bool {
        self.arguments.len() == 0 && self.symbol.chars().nth(0).unwrap().is_uppercase()
    }

    fn substitute_variable(self: &mut Term<'a>, with_term: Term<'a>) {}

    //    fn to_string(self : &Term<'a>) -> String {
    //        if self.arguments.len() == 0 {
    //            String::from(self.symbol)
    //        } else {
    //            let mut representation = String::new();
    //            representation += &(self.symbol.to_owned() + "(");
    //            for argument in self.arguments {
    //                representation += &(argument.to_string() + ",");
    //
    //            }
    //            representation
    //        }
    //    }
}

struct TESRule<'a> {
    // left_side -> right_side
    left_side: Term<'a>,
    right_side: Term<'a>,
}

fn check_termination(left_side: &Term, right_side: &Term) -> bool {
    for arguments in left_side.arguments.iter() {
        if arguments == right_side {
            return true;
        }
    }
    if left_side.symbol != right_side.symbol
        || left_side.arguments.len() != right_side.arguments.len()
    {
        return false;
    }
    let num_sub_terms = left_side.arguments.len();
    for i in 0..num_sub_terms {
        if !check_termination(&left_side.arguments[i], &right_side.arguments[i]) {
            return false;
        }
        for j in 0..num_sub_terms {
            if i != j
                && !check_termination(&left_side.arguments[i], &right_side.arguments[i])
                && left_side.arguments[i] != right_side.arguments[i]
            {
                return false;
            }
        }
        return true;
    }
    false
}

impl<'a> TESRule<'a> {
    fn new(left_side: Term<'a>, right_side: Term<'a>) -> TESRule<'a> {
        TESRule {
            left_side: left_side,
            right_side: right_side,
        }
    }

    //    fn check_termination(&self) -> bool {
    //        for arguments in self.left_side.arguments.iter() {
    //            if *arguments == self.right_side {
    //                return true;
    //            }
    //        }
    //        if self.left_side.symbol != self.right_side.symbol ||
    //        self.left_side.arguments.len() != self.right_side.arguments.len() {
    //            return false;
    //        }
    //        let num_sub_terms = self.left_side.arguments.len();
    //        for i in 0..num_sub_terms {
    //            let sub_rule = TESRule::new(self.left_side.arguments[i],self.right_side.arguments[i]);
    //            for j in 0..num_sub_terms {
    //                if i == j {
    //                    continue;
    //                }
    //            }
    //        }
    //        false
    //    }
}

//macro_rules! term {
//
//}

fn main() {
    let term_a = Term::new("f", vec![Term::new("X", vec![]), Term::new("a", vec![])]);
    println!("{}", term_a.arguments[0].is_variable());
    println!("{}", term_a.arguments[1].is_variable());
    //println!("{}",term_a.to_string());
    println!("{}", term_a == term_a);
    println!("{}", term_a == term_a.arguments[1]);

    let term_b = Term::new("X", vec![]);
    let term_c = Term::new("f", vec![Term::new("a", vec![]), Term::new("a", vec![])]);
    println!("{}", check_termination(&term_a, &term_b));
    println!("{}", check_termination(&term_a, &term_c));
}