#[derive(Debug, PartialEq, Eq, Hash, Clone)]
#[cfg_attr(kani, derive(kani::Arbitrary))]
pub enum BinaryOp {
    Eq,
    LessEq,
    Add,
}

#[derive(Debug, PartialEq, Eq, Hash, Clone)]
#[cfg_attr(kani, derive(kani::Arbitrary))]
pub enum Expr {
    Int(i32),
    Bool(bool),
    If {
        test_expr: Box<Expr>,
        then_expr: Box<Expr>,
        else_expr: Box<Expr>,
    },
    BinaryApp {
        op: BinaryOp,
        arg1: Box<Expr>,
        arg2: Box<Expr>,
    },
}

#[derive(Debug, PartialEq, Eq, Hash, Clone)]
#[cfg_attr(kani, derive(kani::Arbitrary))]
pub enum Value {
    Bool(bool),
    Int(i32),
}

pub struct Calculator {}

impl Calculator {
    pub fn new() -> Self { Self {} }

    pub fn calculate(&self, e: Expr) -> Result<Value, ()> {
        match e {
            Expr::Int(i) => Ok(Value::Int(i)),
            Expr::Bool(b) => Ok(Value::Bool(b)),
            Expr::If {
                test_expr,
                then_expr,
                else_expr,
            } => match self.calculate(*test_expr) {
                Ok(v) => match v {
                    Value::Int(_) => Err(()),
                    Value::Bool(b) => {
                        if b {
                            self.calculate(*then_expr)
                        } else {
                            self.calculate(*else_expr)
                        }
                    }
                },
                Err(e) => Err(e),
            },
            Expr::BinaryApp { op, arg1, arg2 } => {
                let v1 = self.calculate(*arg1);
                let v2 = self.calculate(*arg2);
                if let (Ok(v1), Ok(v2)) = (v1, v2) {
                    match op {
                        BinaryOp::Eq => Ok(Value::Bool(v1 == v2)),
                        BinaryOp::LessEq => match (v1, v2) {
                            (Value::Int(i1), Value::Int(i2)) => Ok(Value::Bool(i1 <= i2)),
                            (_, _) => Err(()),
                        },
                        BinaryOp::Add => match (v1, v2) {
                            (Value::Int(i1), Value::Int(i2)) => Ok(Value::Int(i1.wrapping_add(i2))),
                            (_, _) => Err(()),
                        },
                    }
                } else {
                    Err(())
                }
            }
        }
    }
}

#[kani::proof]
#[kani::unwind(2)]
fn test_calc_kani() {
    let calc = Calculator::new();
    assert_eq!(
        calc.calculate(Expr::BinaryApp {
            op: BinaryOp::Add,
            arg1: Box::new(Expr::Int(3)),
            arg2: Box::new(Expr::Int(4))
        }),
        Ok(Value::Int(7))
    );
}

pub fn main() {
    println!("Hello world!")
}