gdp_rs 0.0.3

use std::marker::PhantomData;

use frunk_core::{
    hlist::{HCons, HNil, Plucker, Sculptor},
    traits::IntoReverse,
};

use crate::{
    proposition::{
        list::{EvaluablePropositionList, PropositionList},
        Evaluable, Proposition,
    },
    proven::Proven,
};

/// A struct representing a compound proposition
/// that evaluates to logical conjunction of all list members.
pub struct AllOf<S, PL: PropositionList<S>> {
    _phantom: PhantomData<fn() -> (S, PL)>,
}

impl<S, PL: PropositionList<S>> Clone for AllOf<S, PL> {
    fn clone(&self) -> Self {
        Self {
            _phantom: self._phantom,
        }
    }
}

impl<S, PL: PropositionList<S>> std::fmt::Debug for AllOf<S, PL> {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        f.debug_struct("AllOf").finish()
    }
}

impl<S, PL> Proposition<S> for AllOf<S, PL> where PL: PropositionList<S> {}

impl<S, PLH, PLT> Proven<S, AllOf<S, HCons<PLH, PLT>>>
where
    PLH: Proposition<S>,
    PLT: PropositionList<S>,
{
    /// Convert into hlist-head proven proposition.
    #[inline]
    pub fn into_head_proven(self) -> Proven<S, PLH> {
        // Safety: if all of propositions hold, head proposition too holds.
        unsafe { Proven::new_unchecked(self.into_subject()) }
    }

    /// Convert into hlist-tail proven proposition.
    #[inline]
    pub fn into_tail_proven(self) -> Proven<S, AllOf<S, PLT>> {
        // Safety: if all of propositions hold, all propositions in tail too hold.
        unsafe { Proven::new_unchecked(self.into_subject()) }
    }

    /// Convert into hlist-plucked proven proposition.
    #[inline]
    pub fn into_plucked_proven<T, Index>(self) -> Proven<S, T>
    where
        T: Proposition<S>,
        HCons<PLH, PLT>: Plucker<T, Index>,
    {
        // Safety: if all of propositions hold, then any of plucked propositions too hold.
        unsafe { Proven::new_unchecked(self.into_subject()) }
    }
}

impl<S, PL> Proven<S, AllOf<S, PL>>
where
    PL: PropositionList<S>,
{
    /// Convert into hlist-sculpted proven proposition.
    #[inline]
    pub fn into_sculpted_proven<Ts, Indices>(self) -> Proven<S, AllOf<S, Ts>>
    where
        Ts: PropositionList<S>,
        PL: Sculptor<Ts, Indices>,
    {
        // Safety: if all of propositions hold, then all propositions in sculpted list also hold.
        unsafe { Proven::new_unchecked(self.into_subject()) }
    }

    /// Convert into hlist-sculpted proven proposition.
    #[inline]
    pub fn into_rev_list_proven(self) -> Proven<S, AllOf<S, <PL as IntoReverse>::Output>>
    where
        PL: IntoReverse,
        <PL as IntoReverse>::Output: PropositionList<S>,
    {
        // Safety: if all of propositions hold, then all propositions in sculpted list also hold.
        unsafe { Proven::new_unchecked(self.into_subject()) }
    }

    /// Try to extend all-of compound proposition with proposition of given proposition class about subject.
    #[allow(clippy::type_complexity)]
    pub fn try_extend_proposition<P>(
        self,
    ) -> Result<Proven<S, AllOf<S, HCons<P, PL>>>, <P as Evaluable<S>>::EvalError>
    where
        P: Proposition<S> + Evaluable<S>,
    {
        P::evaluate_for(self.as_ref())
            // Safety: All propositions hold.
            .map(|_| unsafe { Proven::new_unchecked(self.into_subject()) })
    }

    /// Extend all-of compound proposition with proposition of given proposition class about subject.
    ///
    /// # Safety
    ///
    /// Callers must ensure, extension proposition about the subject holds.
    pub unsafe fn extend_proposition_unchecked<P>(self) -> Proven<S, AllOf<S, HCons<P, PL>>>
    where
        P: Proposition<S>,
    {
        Proven::new_unchecked(self.into_subject())
    }
}

impl<S> Proven<S, AllOf<S, HNil>> {
    /// Get new proven proposition with given subject and empty list proposition type.
    pub fn new(subject: S) -> Self {
        // Safety: Conjunction of empty list of proposition always holds.
        unsafe { Self::new_unchecked(subject) }
    }
}

impl<S, PL> Evaluable<S> for AllOf<S, PL>
where
    PL: EvaluablePropositionList<S>,
{
    type EvalError = Box<dyn std::error::Error + Send + Sync + 'static>;

    #[inline]
    fn evaluate_for(sub: &S) -> Result<(), Self::EvalError> {
        PL::evaluate_all_for(sub)
    }
}