use crate::ast::*;
use crate::ast_util::{
    array_kind_of_typ, bool_typ, conjoin, disjoin, if_then_else, int_typ, mk_eq, mk_ineq,
    mk_int_lit_from_usize, place_to_spec_expr,
};
use crate::context::GlobalCtx;
use crate::def::Spanned;
use crate::messages::{Span, error};
use std::collections::HashMap;
use std::sync::Arc;

pub fn pattern_to_exprs(
    ctx: &GlobalCtx,
    place: &Place,
    pattern: &Pattern,
    has_guard: bool,
    decls: &mut Vec<Stmt>,
) -> Result<Expr, VirErr> {
    let mut pattern_bound_decls = vec![];
    let e = pattern_to_exprs_rec(ctx, pattern, place, &mut pattern_bound_decls, false)?;

    for pbd in pattern_bound_decls {
        if has_guard && pbd.mut_ref {
            return Err(error(
                &pattern.span,
                "Verus does not currently support a match guard when at least one bound variable is mutably borrowed",
            ));
        }

        let ComputedPatternBinding { name, mut_ref, place } = pbd;

        let place = if mut_ref {
            PlaceX::spec_temporary(SpannedTyped::new(
                &place.span,
                &Arc::new(TypX::MutRef(place.typ.clone())),
                ExprX::BorrowMut(place.clone()),
            ))
        } else {
            place
        };

        let pattern = PatternX::simple_var(name, &place.span, &place.typ);
        // Mode doesn't matter at this stage; arbitrarily set it to None
        let decl = StmtX::Decl {
            pattern,
            mode: None,
            init: Some(place.clone()),
            els: None,
            assert_irrefutable: false,
        };
        decls.push(Spanned::new(place.span.clone(), decl));
    }

    Ok(e)
}

struct ComputedPatternBinding {
    name: VarIdent,
    mut_ref: bool,
    place: Place,
}

fn computed(binding: &PatternBinding, place: &Place) -> Result<ComputedPatternBinding, VirErr> {
    Ok(ComputedPatternBinding {
        name: binding.name.clone(),
        place: place.clone(),
        mut_ref: matches!(binding.by_ref, ByRef::MutRef),
    })
}

fn read_place(place: &Place) -> Expr {
    SpannedTyped::new(
        &place.span,
        &place.typ,
        ExprX::ReadPlace(
            place.clone(),
            UnfinalizedReadKind { preliminary_kind: ReadKind::ImmutBor, id: 0 },
        ),
    )
}

fn err_if_bad_binding(span: &Span, in_immut: bool, by_ref: ByRef) -> Result<(), VirErr> {
    // extra sanity check, should be caught by lifetime checking, though
    if in_immut && matches!(by_ref, ByRef::MutRef) {
        return Err(error(
            span,
            "cannot borrow this place as mutable, as it is behind a `&` reference",
        ));
    }
    Ok(())
}

fn pattern_to_exprs_rec(
    ctx: &GlobalCtx,
    pattern: &Pattern,
    place: &Place,
    bindings: &mut Vec<ComputedPatternBinding>,
    in_immut: bool,
) -> Result<Expr, VirErr> {
    let t_bool = Arc::new(TypX::Bool);
    match &pattern.x {
        PatternX::Wildcard => {
            Ok(SpannedTyped::new(&pattern.span, &t_bool, ExprX::Const(Constant::Bool(true))))
        }
        PatternX::Var(binding) => {
            err_if_bad_binding(&pattern.span, in_immut, binding.by_ref)?;
            bindings.push(computed(binding, place)?);
            Ok(SpannedTyped::new(&pattern.span, &t_bool, ExprX::Const(Constant::Bool(true))))
        }
        PatternX::Binding { binding, sub_pat } => {
            err_if_bad_binding(&pattern.span, in_immut, binding.by_ref)?;
            let pattern_test = pattern_to_exprs_rec(ctx, sub_pat, place, bindings, in_immut)?;
            // This binding needs to go last in case we have something like this:
            //   `ref mut x @ Some(y)`
            // (which is ok if the y is bound via copy)
            // In this case we need to read `y` before taking the mut ref
            bindings.push(computed(binding, place)?);
            Ok(pattern_test)
        }
        PatternX::Constructor(dt, variant, patterns) => {
            let expr = read_place(&place);
            let is_variant_opr =
                UnaryOpr::IsVariant { datatype: dt.clone(), variant: variant.clone() };
            let test_variant = SpannedTyped::new(
                &pattern.span,
                &bool_typ(),
                ExprX::UnaryOpr(is_variant_opr, expr.clone()),
            );

            let mut test = test_variant;

            for binder in patterns.iter() {
                let field_opr = FieldOpr {
                    datatype: dt.clone(),
                    variant: variant.clone(),
                    field: binder.name.clone(),
                    get_variant: false,
                    check: VariantCheck::None,
                };
                let field_typ = &binder.a.typ;
                let field_place = SpannedTyped::new(
                    &binder.a.span,
                    field_typ,
                    PlaceX::Field(field_opr, place.clone()),
                );
                let pattern_test =
                    pattern_to_exprs_rec(ctx, &binder.a, &field_place, bindings, in_immut)?;
                let and = ExprX::Logical(LogicalOp::And, test, pattern_test);
                test = SpannedTyped::new(&pattern.span, &t_bool, and);
            }

            Ok(test)
        }
        PatternX::Or(pat1, pat2) => {
            let mut bindings1 = vec![];
            let mut bindings2 = vec![];

            let pat1_matches = pattern_to_exprs_rec(ctx, pat1, place, &mut bindings1, in_immut)?;
            let pat2_matches = pattern_to_exprs_rec(ctx, pat2, place, &mut bindings2, in_immut)?;

            let matches = disjoin(&pattern.span, &vec![pat1_matches.clone(), pat2_matches]);

            assert!(bindings1.len() == bindings2.len());
            for d1 in bindings1 {
                let d2 = bindings2
                    .iter()
                    .find(|d2| d2.name == d1.name)
                    .expect("both sides of 'or' pattern should bind the same variables");
                assert!(!d1.mut_ref);
                assert!(!d2.mut_ref);

                let e1 = place_to_spec_expr(&d1.place);
                let e2 = place_to_spec_expr(&d2.place);
                let ite = if_then_else(&pattern.span, &pat1_matches, &e1, &e2);

                let combined_binding = ComputedPatternBinding {
                    name: d1.name,
                    mut_ref: false,
                    place: PlaceX::spec_temporary(ite),
                };
                bindings.push(combined_binding);
            }

            Ok(matches)
        }
        PatternX::Expr(e) => {
            let expr = read_place(&place);
            Ok(mk_eq(&pattern.span, &expr, e))
        }
        PatternX::Range(lower, upper) => {
            let expr = read_place(&place);
            let mut v = vec![];
            if let Some(lower) = lower {
                v.push(mk_ineq(&pattern.span, lower, &expr, InequalityOp::Le));
            }
            if let Some((upper, upper_ineq)) = upper {
                v.push(mk_ineq(&pattern.span, &expr, upper, *upper_ineq));
            }
            Ok(conjoin(&pattern.span, &v))
        }
        PatternX::ImmutRef(sub_pat) => pattern_to_exprs_rec(ctx, sub_pat, place, bindings, true),
        PatternX::MutRef(sub_pat) => {
            let deref_place =
                SpannedTyped::new(&sub_pat.span, &sub_pat.typ, PlaceX::DerefMut(place.clone()));
            pattern_to_exprs_rec(ctx, sub_pat, &deref_place, bindings, in_immut)
        }
        PatternX::Slice(patterns) => {
            let (kind, elem_typ) = array_kind_of_typ(&pattern.typ);

            let mut conjuncts = vec![];

            // If it's a slice, we need to test the length
            if kind == ArrayKind::Slice {
                let actual_len = SpannedTyped::new(
                    &pattern.span,
                    &int_typ(),
                    ExprX::Unary(UnaryOp::Length(ArrayKind::Slice), read_place(&place)),
                );
                let expected_len = mk_int_lit_from_usize(&pattern.span, patterns.len());
                conjuncts.push(mk_eq(&pattern.span, &actual_len, &expected_len));
            }

            for (i, p) in patterns.iter().enumerate() {
                let idx = mk_int_lit_from_usize(&p.span, i);
                let index_place = SpannedTyped::new(
                    &p.span,
                    &elem_typ,
                    PlaceX::Index(place.clone(), idx, kind, BoundsCheck::Allow),
                );
                let pattern_test = pattern_to_exprs_rec(ctx, p, &index_place, bindings, in_immut)?;
                conjuncts.push(pattern_test);
            }

            Ok(conjoin(&pattern.span, &conjuncts))
        }
    }
}

pub fn pattern_find_mut_binding(pattern: &Pattern) -> Option<Span> {
    match &pattern.x {
        PatternX::Wildcard => None,
        PatternX::Var(binding) => {
            if matches!(binding.by_ref, ByRef::MutRef) {
                Some(pattern.span.clone())
            } else {
                None
            }
        }
        PatternX::Binding { binding, sub_pat } => {
            if matches!(binding.by_ref, ByRef::MutRef) {
                Some(pattern.span.clone())
            } else {
                pattern_find_mut_binding(sub_pat)
            }
        }
        PatternX::Constructor(_path, _variant, patterns) => {
            for binder in patterns.iter() {
                match pattern_find_mut_binding(&binder.a) {
                    s @ Some(_) => {
                        return s;
                    }
                    None => {}
                }
            }
            None
        }
        PatternX::Or(pat1, pat2) => {
            match pattern_find_mut_binding(pat1) {
                s @ Some(_) => {
                    return s;
                }
                None => {}
            }
            pattern_find_mut_binding(pat2)
        }
        PatternX::Expr(_e) => None,
        PatternX::Range(_lower, _upper) => None,
        PatternX::ImmutRef(p) | PatternX::MutRef(p) => pattern_find_mut_binding(p),
        PatternX::Slice(patterns) => {
            for p in patterns.iter() {
                match pattern_find_mut_binding(p) {
                    s @ Some(_) => {
                        return s;
                    }
                    None => {}
                }
            }
            None
        }
    }
}

pub(crate) fn pattern_has_mut(pattern: &Pattern) -> bool {
    pattern_find_mut_binding(pattern).is_some()
}

pub(crate) fn pattern_has_or(pattern: &Pattern) -> bool {
    match &pattern.x {
        PatternX::Wildcard => false,
        PatternX::Var(_binding) => false,
        PatternX::Binding { binding: _, sub_pat } => pattern_has_or(sub_pat),
        PatternX::Constructor(_path, _variant, patterns) => {
            patterns.iter().any(|p| pattern_has_or(&p.a))
        }
        PatternX::Or(_pat1, _pat2) => true,
        PatternX::Expr(_e) => false,
        PatternX::Range(_lower, _upper) => false,
        PatternX::ImmutRef(p) | PatternX::MutRef(p) => pattern_has_or(p),
        PatternX::Slice(patterns) => patterns.iter().any(|p| pattern_has_or(p)),
    }
}

/// Returns true ==> the pattern is irrefutable
pub(crate) fn definitely_irrefutable(
    pattern: &Pattern,
    datatypes: &HashMap<Path, Datatype>,
) -> bool {
    match &pattern.x {
        PatternX::Wildcard => true,
        PatternX::Var(_binding) => true,
        PatternX::Binding { binding: _, sub_pat } => definitely_irrefutable(sub_pat, datatypes),
        PatternX::Constructor(dt, _variant, patterns) => {
            let one_variant = match dt {
                Dt::Path(p) => datatypes[p].x.variants.len() == 1,
                Dt::Tuple(_) => true,
            };
            one_variant && patterns.iter().all(|p| definitely_irrefutable(&p.a, datatypes))
        }
        PatternX::Or(_pat1, _pat2) => false,
        PatternX::Expr(_e) => false,
        PatternX::Range(_lower, _upper) => false,
        PatternX::ImmutRef(p) | PatternX::MutRef(p) => definitely_irrefutable(p, datatypes),
        PatternX::Slice(patterns) => match array_kind_of_typ(&pattern.typ).0 {
            ArrayKind::Slice => false,
            ArrayKind::Array => patterns.iter().all(|p| definitely_irrefutable(p, datatypes)),
        },
    }
}