//! Trait solving using Chalk.
use std::{panic, sync::Arc};

use chalk_ir::cast::Cast;
use hir_def::{expr::ExprId, DefWithBodyId, ImplId, TraitId, TypeAliasId};
use ra_db::{impl_intern_key, salsa, CrateId};
use ra_prof::profile;
use rustc_hash::FxHashSet;

use crate::db::HirDatabase;

use super::{Canonical, GenericPredicate, HirDisplay, ProjectionTy, TraitRef, Ty, TypeWalk};

use self::chalk::{from_chalk, Interner, ToChalk};

pub(crate) mod chalk;
mod builtin;

/// This controls the maximum size of types Chalk considers. If we set this too
/// high, we can run into slow edge cases; if we set it too low, Chalk won't
/// find some solutions.
const CHALK_SOLVER_MAX_SIZE: usize = 10;
/// This controls how much 'time' we give the Chalk solver before giving up.
const CHALK_SOLVER_FUEL: i32 = 100;

#[derive(Debug, Copy, Clone)]
struct ChalkContext<'a> {
    db: &'a dyn HirDatabase,
    krate: CrateId,
}

fn create_chalk_solver() -> chalk_solve::Solver<Interner> {
    let solver_choice =
        chalk_solve::SolverChoice::SLG { max_size: CHALK_SOLVER_MAX_SIZE, expected_answers: None };
    solver_choice.into_solver()
}

/// Collects impls for the given trait in the whole dependency tree of `krate`.
pub(crate) fn impls_for_trait_query(
    db: &dyn HirDatabase,
    krate: CrateId,
    trait_: TraitId,
) -> Arc<[ImplId]> {
    let mut impls = FxHashSet::default();
    // We call the query recursively here. On the one hand, this means we can
    // reuse results from queries for different crates; on the other hand, this
    // will only ever get called for a few crates near the root of the tree (the
    // ones the user is editing), so this may actually be a waste of memory. I'm
    // doing it like this mainly for simplicity for now.
    for dep in &db.crate_graph()[krate].dependencies {
        impls.extend(db.impls_for_trait(dep.crate_id, trait_).iter());
    }
    let crate_impl_defs = db.impls_in_crate(krate);
    impls.extend(crate_impl_defs.lookup_impl_defs_for_trait(trait_));
    impls.into_iter().collect()
}

/// A set of clauses that we assume to be true. E.g. if we are inside this function:
/// ```rust
/// fn foo<T: Default>(t: T) {}
/// ```
/// we assume that `T: Default`.
#[derive(Clone, Debug, PartialEq, Eq, Hash)]
pub struct TraitEnvironment {
    pub predicates: Vec<GenericPredicate>,
}

impl TraitEnvironment {
    /// Returns trait refs with the given self type which are supposed to hold
    /// in this trait env. E.g. if we are in `foo<T: SomeTrait>()`, this will
    /// find that `T: SomeTrait` if we call it for `T`.
    pub(crate) fn trait_predicates_for_self_ty<'a>(
        &'a self,
        ty: &'a Ty,
    ) -> impl Iterator<Item = &'a TraitRef> + 'a {
        self.predicates.iter().filter_map(move |pred| match pred {
            GenericPredicate::Implemented(tr) if tr.self_ty() == ty => Some(tr),
            _ => None,
        })
    }
}

/// Something (usually a goal), along with an environment.
#[derive(Clone, Debug, PartialEq, Eq, Hash)]
pub struct InEnvironment<T> {
    pub environment: Arc<TraitEnvironment>,
    pub value: T,
}

impl<T> InEnvironment<T> {
    pub fn new(environment: Arc<TraitEnvironment>, value: T) -> InEnvironment<T> {
        InEnvironment { environment, value }
    }
}

/// Something that needs to be proven (by Chalk) during type checking, e.g. that
/// a certain type implements a certain trait. Proving the Obligation might
/// result in additional information about inference variables.
#[derive(Clone, Debug, PartialEq, Eq, Hash)]
pub enum Obligation {
    /// Prove that a certain type implements a trait (the type is the `Self` type
    /// parameter to the `TraitRef`).
    Trait(TraitRef),
    Projection(ProjectionPredicate),
}

impl Obligation {
    pub fn from_predicate(predicate: GenericPredicate) -> Option<Obligation> {
        match predicate {
            GenericPredicate::Implemented(trait_ref) => Some(Obligation::Trait(trait_ref)),
            GenericPredicate::Projection(projection_pred) => {
                Some(Obligation::Projection(projection_pred))
            }
            GenericPredicate::Error => None,
        }
    }
}

#[derive(Clone, Debug, PartialEq, Eq, Hash)]
pub struct ProjectionPredicate {
    pub projection_ty: ProjectionTy,
    pub ty: Ty,
}

impl TypeWalk for ProjectionPredicate {
    fn walk(&self, f: &mut impl FnMut(&Ty)) {
        self.projection_ty.walk(f);
        self.ty.walk(f);
    }

    fn walk_mut_binders(&mut self, f: &mut impl FnMut(&mut Ty, usize), binders: usize) {
        self.projection_ty.walk_mut_binders(f, binders);
        self.ty.walk_mut_binders(f, binders);
    }
}

/// Solve a trait goal using Chalk.
pub(crate) fn trait_solve_query(
    db: &dyn HirDatabase,
    krate: CrateId,
    goal: Canonical<InEnvironment<Obligation>>,
) -> Option<Solution> {
    let _p = profile("trait_solve_query").detail(|| match &goal.value.value {
        Obligation::Trait(it) => db.trait_data(it.trait_).name.to_string(),
        Obligation::Projection(_) => "projection".to_string(),
    });
    log::debug!("trait_solve_query({})", goal.value.value.display(db));

    if let Obligation::Projection(pred) = &goal.value.value {
        if let Ty::Bound(_) = &pred.projection_ty.parameters[0] {
            // Hack: don't ask Chalk to normalize with an unknown self type, it'll say that's impossible
            return Some(Solution::Ambig(Guidance::Unknown));
        }
    }

    let canonical = goal.to_chalk(db).cast();

    // We currently don't deal with universes (I think / hope they're not yet
    // relevant for our use cases?)
    let u_canonical = chalk_ir::UCanonical { canonical, universes: 1 };
    let solution = solve(db, krate, &u_canonical);
    solution.map(|solution| solution_from_chalk(db, solution))
}

fn solve(
    db: &dyn HirDatabase,
    krate: CrateId,
    goal: &chalk_ir::UCanonical<chalk_ir::InEnvironment<chalk_ir::Goal<Interner>>>,
) -> Option<chalk_solve::Solution<Interner>> {
    let context = ChalkContext { db, krate };
    log::debug!("solve goal: {:?}", goal);
    let mut solver = create_chalk_solver();

    let fuel = std::cell::Cell::new(CHALK_SOLVER_FUEL);

    let solution = solver.solve_limited(&context, goal, || {
        context.db.check_canceled();
        let remaining = fuel.get();
        fuel.set(remaining - 1);
        if remaining == 0 {
            log::debug!("fuel exhausted");
        }
        remaining > 0
    });

    log::debug!("solve({:?}) => {:?}", goal, solution);
    solution
}

fn solution_from_chalk(
    db: &dyn HirDatabase,
    solution: chalk_solve::Solution<Interner>,
) -> Solution {
    let convert_subst = |subst: chalk_ir::Canonical<chalk_ir::Substitution<Interner>>| {
        let value = subst
            .value
            .into_iter()
            .map(|p| match p.ty() {
                Some(ty) => from_chalk(db, ty.clone()),
                None => unimplemented!(),
            })
            .collect();
        let result = Canonical { value, num_vars: subst.binders.len() };
        SolutionVariables(result)
    };
    match solution {
        chalk_solve::Solution::Unique(constr_subst) => {
            let subst = chalk_ir::Canonical {
                value: constr_subst.value.subst,
                binders: constr_subst.binders,
            };
            Solution::Unique(convert_subst(subst))
        }
        chalk_solve::Solution::Ambig(chalk_solve::Guidance::Definite(subst)) => {
            Solution::Ambig(Guidance::Definite(convert_subst(subst)))
        }
        chalk_solve::Solution::Ambig(chalk_solve::Guidance::Suggested(subst)) => {
            Solution::Ambig(Guidance::Suggested(convert_subst(subst)))
        }
        chalk_solve::Solution::Ambig(chalk_solve::Guidance::Unknown) => {
            Solution::Ambig(Guidance::Unknown)
        }
    }
}

#[derive(Clone, Debug, PartialEq, Eq)]
pub struct SolutionVariables(pub Canonical<Vec<Ty>>);

#[derive(Clone, Debug, PartialEq, Eq)]
/// A (possible) solution for a proposed goal.
pub enum Solution {
    /// The goal indeed holds, and there is a unique value for all existential
    /// variables.
    Unique(SolutionVariables),

    /// The goal may be provable in multiple ways, but regardless we may have some guidance
    /// for type inference. In this case, we don't return any lifetime
    /// constraints, since we have not "committed" to any particular solution
    /// yet.
    Ambig(Guidance),
}

#[derive(Clone, Debug, PartialEq, Eq)]
/// When a goal holds ambiguously (e.g., because there are multiple possible
/// solutions), we issue a set of *guidance* back to type inference.
pub enum Guidance {
    /// The existential variables *must* have the given values if the goal is
    /// ever to hold, but that alone isn't enough to guarantee the goal will
    /// actually hold.
    Definite(SolutionVariables),

    /// There are multiple plausible values for the existentials, but the ones
    /// here are suggested as the preferred choice heuristically. These should
    /// be used for inference fallback only.
    Suggested(SolutionVariables),

    /// There's no useful information to feed back to type inference
    Unknown,
}

#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)]
pub enum FnTrait {
    FnOnce,
    FnMut,
    Fn,
}

impl FnTrait {
    fn lang_item_name(self) -> &'static str {
        match self {
            FnTrait::FnOnce => "fn_once",
            FnTrait::FnMut => "fn_mut",
            FnTrait::Fn => "fn",
        }
    }
}

#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub struct ClosureFnTraitImplData {
    def: DefWithBodyId,
    expr: ExprId,
    fn_trait: FnTrait,
}

#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub struct UnsizeToSuperTraitObjectData {
    trait_: TraitId,
    super_trait: TraitId,
}

/// An impl. Usually this comes from an impl block, but some built-in types get
/// synthetic impls.
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub enum Impl {
    /// A normal impl from an impl block.
    ImplDef(ImplId),
    /// Closure types implement the Fn traits synthetically.
    ClosureFnTraitImpl(ClosureFnTraitImplData),
    /// [T; n]: Unsize<[T]>
    UnsizeArray,
    /// T: Unsize<dyn Trait> where T: Trait
    UnsizeToTraitObject(TraitId),
    /// dyn Trait: Unsize<dyn SuperTrait> if Trait: SuperTrait
    UnsizeToSuperTraitObject(UnsizeToSuperTraitObjectData),
}
/// This exists just for Chalk, because our ImplIds are only unique per module.
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub struct GlobalImplId(salsa::InternId);
impl_intern_key!(GlobalImplId);

/// An associated type value. Usually this comes from a `type` declaration
/// inside an impl block, but for built-in impls we have to synthesize it.
/// (We only need this because Chalk wants a unique ID for each of these.)
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
pub enum AssocTyValue {
    /// A normal assoc type value from an impl block.
    TypeAlias(TypeAliasId),
    /// The output type of the Fn trait implementation.
    ClosureFnTraitImplOutput(ClosureFnTraitImplData),
}
/// This exists just for Chalk, because it needs a unique ID for each associated
/// type value in an impl (even synthetic ones).
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub struct AssocTyValueId(salsa::InternId);
impl_intern_key!(AssocTyValueId);