{-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable #-}
module Distribution.Solver.Modular.Tree
    ( POption(..)
    , Tree(..)
    , TreeF(..)
    , Weight
    , FailReason(..)
    , ConflictingDep(..)
    , ana
    , cata
    , inn
    , innM
    , para
    , trav
    , zeroOrOneChoices
    , active
    , TreeTrav
    , EndoTreeTrav
    ) where

import Control.Monad hiding (mapM, sequence)
import Data.Foldable
import Data.Traversable
import Prelude hiding (foldr, mapM, sequence)

import Distribution.Solver.Modular.Dependency
import Distribution.Solver.Modular.Flag
import Distribution.Solver.Modular.Package
import Distribution.Solver.Modular.PSQ (PSQ)
import Distribution.Solver.Modular.Version
import Distribution.Solver.Modular.WeightedPSQ (WeightedPSQ)
import qualified Distribution.Solver.Modular.WeightedPSQ as W
import Distribution.Solver.Types.ConstraintSource
import Distribution.Solver.Types.Flag
import Distribution.Solver.Types.PackagePath
import Distribution.Types.PkgconfigVersionRange
import Distribution.Types.UnitId (UnitId)
import Language.Haskell.Extension (Extension, Language)

type Weight = Double

-- | Type of the search tree. Inlining the choice nodes for now. Weights on
-- package, flag, and stanza choices control the traversal order.
--
-- The tree can hold additional data on 'Done' nodes (type 'd') and choice nodes
-- (type 'c'). For example, during the final traversal, choice nodes contain the
-- variables that introduced the choices, and 'Done' nodes contain the
-- assignments for all variables.
--
-- TODO: The weight type should be changed from [Double] to Double to avoid
-- giving too much weight to preferences that are applied later.
data Tree d c =
    -- | Choose a version for a package (or choose to link)
    PChoice QPN RevDepMap c (WeightedPSQ [Weight] POption (Tree d c))

    -- | Choose a value for a flag
    --
    -- The Bool is the default value.
  | FChoice QFN RevDepMap c WeakOrTrivial FlagType Bool (WeightedPSQ [Weight] Bool (Tree d c))

    -- | Choose whether or not to enable a stanza
  | SChoice QSN RevDepMap c WeakOrTrivial (WeightedPSQ [Weight] Bool (Tree d c))

    -- | Choose which choice to make next
    --
    -- Invariants:
    --
    -- * PSQ should never be empty
    -- * For each choice we additionally record the 'QGoalReason' why we are
    --   introducing that goal into tree. Note that most of the time we are
    --   working with @Tree QGoalReason@; in that case, we must have the
    --   invariant that the 'QGoalReason' cached in the 'PChoice', 'FChoice'
    --   or 'SChoice' directly below a 'GoalChoice' node must equal the reason
    --   recorded on that 'GoalChoice' node.
  | GoalChoice RevDepMap (PSQ (Goal QPN) (Tree d c))

    -- | We're done -- we found a solution!
  | Done RevDepMap d

    -- | We failed to find a solution in this path through the tree
  | Fail ConflictSet FailReason

-- | A package option is a package instance with an optional linking annotation
--
-- The modular solver has a number of package goals to solve for, and can only
-- pick a single package version for a single goal. In order to allow to
-- install multiple versions of the same package as part of a single solution
-- the solver uses qualified goals. For example, @0.P@ and @1.P@ might both
-- be qualified goals for @P@, allowing to pick a difference version of package
-- @P@ for @0.P@ and @1.P@.
--
-- Linking is an essential part of this story. In addition to picking a specific
-- version for @1.P@, the solver can also decide to link @1.P@ to @0.P@ (or
-- vice versa). It means that @1.P@ and @0.P@ really must be the very same package
-- (and hence must have the same build time configuration, and their
-- dependencies must also be the exact same).
--
-- See <http://www.well-typed.com/blog/2015/03/qualified-goals/> for details.
data POption = POption I (Maybe PackagePath)
  deriving (POption -> POption -> Bool
(POption -> POption -> Bool)
-> (POption -> POption -> Bool) -> Eq POption
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: POption -> POption -> Bool
== :: POption -> POption -> Bool
$c/= :: POption -> POption -> Bool
/= :: POption -> POption -> Bool
Eq, Int -> POption -> ShowS
[POption] -> ShowS
POption -> String
(Int -> POption -> ShowS)
-> (POption -> String) -> ([POption] -> ShowS) -> Show POption
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> POption -> ShowS
showsPrec :: Int -> POption -> ShowS
$cshow :: POption -> String
show :: POption -> String
$cshowList :: [POption] -> ShowS
showList :: [POption] -> ShowS
Show)

data FailReason = UnsupportedExtension Extension
                | UnsupportedLanguage Language
                | MissingPkgconfigPackage PkgconfigName PkgconfigVersionRange
                | MissingPkgconfigProgram PkgconfigName PkgconfigVersionRange
                | NewPackageDoesNotMatchExistingConstraint ConflictingDep
                | ConflictingConstraints ConflictingDep ConflictingDep
                | NewPackageIsMissingRequiredComponent ExposedComponent (DependencyReason QPN)
                | NewPackageHasPrivateRequiredComponent ExposedComponent (DependencyReason QPN)
                | NewPackageHasUnbuildableRequiredComponent ExposedComponent (DependencyReason QPN)
                | PackageRequiresMissingComponent QPN ExposedComponent
                | PackageRequiresPrivateComponent QPN ExposedComponent
                | PackageRequiresUnbuildableComponent QPN ExposedComponent
                | CannotReinstall
                | NotExplicit
                | Shadowed
                | Broken UnitId
                | UnknownPackage
                | GlobalConstraintVersion VR ConstraintSource
                | GlobalConstraintInstalled ConstraintSource
                | GlobalConstraintSource ConstraintSource
                | GlobalConstraintFlag ConstraintSource
                | ManualFlag
                | MalformedFlagChoice QFN
                | MalformedStanzaChoice QSN
                | EmptyGoalChoice
                | Backjump
                | MultipleInstances
                | DependenciesNotLinked String
                | CyclicDependencies
                | UnsupportedSpecVer Ver
  deriving (FailReason -> FailReason -> Bool
(FailReason -> FailReason -> Bool)
-> (FailReason -> FailReason -> Bool) -> Eq FailReason
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: FailReason -> FailReason -> Bool
== :: FailReason -> FailReason -> Bool
$c/= :: FailReason -> FailReason -> Bool
/= :: FailReason -> FailReason -> Bool
Eq, Int -> FailReason -> ShowS
[FailReason] -> ShowS
FailReason -> String
(Int -> FailReason -> ShowS)
-> (FailReason -> String)
-> ([FailReason] -> ShowS)
-> Show FailReason
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> FailReason -> ShowS
showsPrec :: Int -> FailReason -> ShowS
$cshow :: FailReason -> String
show :: FailReason -> String
$cshowList :: [FailReason] -> ShowS
showList :: [FailReason] -> ShowS
Show)

-- | Information about a dependency involved in a conflict, for error messages.
data ConflictingDep = ConflictingDep (DependencyReason QPN) (PkgComponent QPN) CI
  deriving (ConflictingDep -> ConflictingDep -> Bool
(ConflictingDep -> ConflictingDep -> Bool)
-> (ConflictingDep -> ConflictingDep -> Bool) -> Eq ConflictingDep
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ConflictingDep -> ConflictingDep -> Bool
== :: ConflictingDep -> ConflictingDep -> Bool
$c/= :: ConflictingDep -> ConflictingDep -> Bool
/= :: ConflictingDep -> ConflictingDep -> Bool
Eq, Int -> ConflictingDep -> ShowS
[ConflictingDep] -> ShowS
ConflictingDep -> String
(Int -> ConflictingDep -> ShowS)
-> (ConflictingDep -> String)
-> ([ConflictingDep] -> ShowS)
-> Show ConflictingDep
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ConflictingDep -> ShowS
showsPrec :: Int -> ConflictingDep -> ShowS
$cshow :: ConflictingDep -> String
show :: ConflictingDep -> String
$cshowList :: [ConflictingDep] -> ShowS
showList :: [ConflictingDep] -> ShowS
Show)

-- | Functor for the tree type. 'a' is the type of nodes' children. 'd' and 'c'
-- have the same meaning as in 'Tree'.
data TreeF d c a =
    PChoiceF    QPN RevDepMap c                             (WeightedPSQ [Weight] POption a)
  | FChoiceF    QFN RevDepMap c WeakOrTrivial FlagType Bool (WeightedPSQ [Weight] Bool    a)
  | SChoiceF    QSN RevDepMap c WeakOrTrivial               (WeightedPSQ [Weight] Bool    a)
  | GoalChoiceF     RevDepMap                               (PSQ (Goal QPN) a)
  | DoneF           RevDepMap d
  | FailF       ConflictSet FailReason
  deriving ((forall a b. (a -> b) -> TreeF d c a -> TreeF d c b)
-> (forall a b. a -> TreeF d c b -> TreeF d c a)
-> Functor (TreeF d c)
forall a b. a -> TreeF d c b -> TreeF d c a
forall a b. (a -> b) -> TreeF d c a -> TreeF d c b
forall d c a b. a -> TreeF d c b -> TreeF d c a
forall d c a b. (a -> b) -> TreeF d c a -> TreeF d c b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall d c a b. (a -> b) -> TreeF d c a -> TreeF d c b
fmap :: forall a b. (a -> b) -> TreeF d c a -> TreeF d c b
$c<$ :: forall d c a b. a -> TreeF d c b -> TreeF d c a
<$ :: forall a b. a -> TreeF d c b -> TreeF d c a
Functor, (forall m. Monoid m => TreeF d c m -> m)
-> (forall m a. Monoid m => (a -> m) -> TreeF d c a -> m)
-> (forall m a. Monoid m => (a -> m) -> TreeF d c a -> m)
-> (forall a b. (a -> b -> b) -> b -> TreeF d c a -> b)
-> (forall a b. (a -> b -> b) -> b -> TreeF d c a -> b)
-> (forall b a. (b -> a -> b) -> b -> TreeF d c a -> b)
-> (forall b a. (b -> a -> b) -> b -> TreeF d c a -> b)
-> (forall a. (a -> a -> a) -> TreeF d c a -> a)
-> (forall a. (a -> a -> a) -> TreeF d c a -> a)
-> (forall a. TreeF d c a -> [a])
-> (forall a. TreeF d c a -> Bool)
-> (forall a. TreeF d c a -> Int)
-> (forall a. Eq a => a -> TreeF d c a -> Bool)
-> (forall a. Ord a => TreeF d c a -> a)
-> (forall a. Ord a => TreeF d c a -> a)
-> (forall a. Num a => TreeF d c a -> a)
-> (forall a. Num a => TreeF d c a -> a)
-> Foldable (TreeF d c)
forall a. Eq a => a -> TreeF d c a -> Bool
forall a. Num a => TreeF d c a -> a
forall a. Ord a => TreeF d c a -> a
forall m. Monoid m => TreeF d c m -> m
forall a. TreeF d c a -> Bool
forall a. TreeF d c a -> Int
forall a. TreeF d c a -> [a]
forall a. (a -> a -> a) -> TreeF d c a -> a
forall m a. Monoid m => (a -> m) -> TreeF d c a -> m
forall b a. (b -> a -> b) -> b -> TreeF d c a -> b
forall a b. (a -> b -> b) -> b -> TreeF d c a -> b
forall d c a. Eq a => a -> TreeF d c a -> Bool
forall d c a. Num a => TreeF d c a -> a
forall d c a. Ord a => TreeF d c a -> a
forall d c m. Monoid m => TreeF d c m -> m
forall d c a. TreeF d c a -> Bool
forall d c a. TreeF d c a -> Int
forall d c a. TreeF d c a -> [a]
forall d c a. (a -> a -> a) -> TreeF d c a -> a
forall d c m a. Monoid m => (a -> m) -> TreeF d c a -> m
forall d c b a. (b -> a -> b) -> b -> TreeF d c a -> b
forall d c a b. (a -> b -> b) -> b -> TreeF d c a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall d c m. Monoid m => TreeF d c m -> m
fold :: forall m. Monoid m => TreeF d c m -> m
$cfoldMap :: forall d c m a. Monoid m => (a -> m) -> TreeF d c a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> TreeF d c a -> m
$cfoldMap' :: forall d c m a. Monoid m => (a -> m) -> TreeF d c a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> TreeF d c a -> m
$cfoldr :: forall d c a b. (a -> b -> b) -> b -> TreeF d c a -> b
foldr :: forall a b. (a -> b -> b) -> b -> TreeF d c a -> b
$cfoldr' :: forall d c a b. (a -> b -> b) -> b -> TreeF d c a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> TreeF d c a -> b
$cfoldl :: forall d c b a. (b -> a -> b) -> b -> TreeF d c a -> b
foldl :: forall b a. (b -> a -> b) -> b -> TreeF d c a -> b
$cfoldl' :: forall d c b a. (b -> a -> b) -> b -> TreeF d c a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> TreeF d c a -> b
$cfoldr1 :: forall d c a. (a -> a -> a) -> TreeF d c a -> a
foldr1 :: forall a. (a -> a -> a) -> TreeF d c a -> a
$cfoldl1 :: forall d c a. (a -> a -> a) -> TreeF d c a -> a
foldl1 :: forall a. (a -> a -> a) -> TreeF d c a -> a
$ctoList :: forall d c a. TreeF d c a -> [a]
toList :: forall a. TreeF d c a -> [a]
$cnull :: forall d c a. TreeF d c a -> Bool
null :: forall a. TreeF d c a -> Bool
$clength :: forall d c a. TreeF d c a -> Int
length :: forall a. TreeF d c a -> Int
$celem :: forall d c a. Eq a => a -> TreeF d c a -> Bool
elem :: forall a. Eq a => a -> TreeF d c a -> Bool
$cmaximum :: forall d c a. Ord a => TreeF d c a -> a
maximum :: forall a. Ord a => TreeF d c a -> a
$cminimum :: forall d c a. Ord a => TreeF d c a -> a
minimum :: forall a. Ord a => TreeF d c a -> a
$csum :: forall d c a. Num a => TreeF d c a -> a
sum :: forall a. Num a => TreeF d c a -> a
$cproduct :: forall d c a. Num a => TreeF d c a -> a
product :: forall a. Num a => TreeF d c a -> a
Foldable, Functor (TreeF d c)
Foldable (TreeF d c)
(Functor (TreeF d c), Foldable (TreeF d c)) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> TreeF d c a -> f (TreeF d c b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    TreeF d c (f a) -> f (TreeF d c a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> TreeF d c a -> m (TreeF d c b))
-> (forall (m :: * -> *) a.
    Monad m =>
    TreeF d c (m a) -> m (TreeF d c a))
-> Traversable (TreeF d c)
forall d c. Functor (TreeF d c)
forall d c. Foldable (TreeF d c)
forall d c (m :: * -> *) a.
Monad m =>
TreeF d c (m a) -> m (TreeF d c a)
forall d c (f :: * -> *) a.
Applicative f =>
TreeF d c (f a) -> f (TreeF d c a)
forall d c (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TreeF d c a -> m (TreeF d c b)
forall d c (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> TreeF d c a -> f (TreeF d c b)
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a.
Monad m =>
TreeF d c (m a) -> m (TreeF d c a)
forall (f :: * -> *) a.
Applicative f =>
TreeF d c (f a) -> f (TreeF d c a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TreeF d c a -> m (TreeF d c b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> TreeF d c a -> f (TreeF d c b)
$ctraverse :: forall d c (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> TreeF d c a -> f (TreeF d c b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> TreeF d c a -> f (TreeF d c b)
$csequenceA :: forall d c (f :: * -> *) a.
Applicative f =>
TreeF d c (f a) -> f (TreeF d c a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
TreeF d c (f a) -> f (TreeF d c a)
$cmapM :: forall d c (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TreeF d c a -> m (TreeF d c b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> TreeF d c a -> m (TreeF d c b)
$csequence :: forall d c (m :: * -> *) a.
Monad m =>
TreeF d c (m a) -> m (TreeF d c a)
sequence :: forall (m :: * -> *) a.
Monad m =>
TreeF d c (m a) -> m (TreeF d c a)
Traversable)

out :: Tree d c -> TreeF d c (Tree d c)
out :: forall d c. Tree d c -> TreeF d c (Tree d c)
out (PChoice    QPN
p RevDepMap
s c
i       WeightedPSQ [Weight] POption (Tree d c)
ts) = QPN
-> RevDepMap
-> c
-> WeightedPSQ [Weight] POption (Tree d c)
-> TreeF d c (Tree d c)
forall d c a.
QPN
-> RevDepMap -> c -> WeightedPSQ [Weight] POption a -> TreeF d c a
PChoiceF    QPN
p RevDepMap
s c
i       WeightedPSQ [Weight] POption (Tree d c)
ts
out (FChoice    QFN
p RevDepMap
s c
i WeakOrTrivial
b FlagType
m Bool
d WeightedPSQ [Weight] Bool (Tree d c)
ts) = QFN
-> RevDepMap
-> c
-> WeakOrTrivial
-> FlagType
-> Bool
-> WeightedPSQ [Weight] Bool (Tree d c)
-> TreeF d c (Tree d c)
forall d c a.
QFN
-> RevDepMap
-> c
-> WeakOrTrivial
-> FlagType
-> Bool
-> WeightedPSQ [Weight] Bool a
-> TreeF d c a
FChoiceF    QFN
p RevDepMap
s c
i WeakOrTrivial
b FlagType
m Bool
d WeightedPSQ [Weight] Bool (Tree d c)
ts
out (SChoice    QSN
p RevDepMap
s c
i WeakOrTrivial
b     WeightedPSQ [Weight] Bool (Tree d c)
ts) = QSN
-> RevDepMap
-> c
-> WeakOrTrivial
-> WeightedPSQ [Weight] Bool (Tree d c)
-> TreeF d c (Tree d c)
forall d c a.
QSN
-> RevDepMap
-> c
-> WeakOrTrivial
-> WeightedPSQ [Weight] Bool a
-> TreeF d c a
SChoiceF    QSN
p RevDepMap
s c
i WeakOrTrivial
b     WeightedPSQ [Weight] Bool (Tree d c)
ts
out (GoalChoice   RevDepMap
s         PSQ (Goal QPN) (Tree d c)
ts) = RevDepMap -> PSQ (Goal QPN) (Tree d c) -> TreeF d c (Tree d c)
forall d c a. RevDepMap -> PSQ (Goal QPN) a -> TreeF d c a
GoalChoiceF   RevDepMap
s         PSQ (Goal QPN) (Tree d c)
ts
out (Done       RevDepMap
x d
s           ) = RevDepMap -> d -> TreeF d c (Tree d c)
forall d c a. RevDepMap -> d -> TreeF d c a
DoneF       RevDepMap
x d
s
out (Fail       ConflictSet
c FailReason
x           ) = ConflictSet -> FailReason -> TreeF d c (Tree d c)
forall d c a. ConflictSet -> FailReason -> TreeF d c a
FailF       ConflictSet
c FailReason
x

inn :: TreeF d c (Tree d c) -> Tree d c
inn :: forall d c. TreeF d c (Tree d c) -> Tree d c
inn (PChoiceF    QPN
p RevDepMap
s c
i       WeightedPSQ [Weight] POption (Tree d c)
ts) = QPN
-> RevDepMap
-> c
-> WeightedPSQ [Weight] POption (Tree d c)
-> Tree d c
forall d c.
QPN
-> RevDepMap
-> c
-> WeightedPSQ [Weight] POption (Tree d c)
-> Tree d c
PChoice    QPN
p RevDepMap
s c
i       WeightedPSQ [Weight] POption (Tree d c)
ts
inn (FChoiceF    QFN
p RevDepMap
s c
i WeakOrTrivial
b FlagType
m Bool
d WeightedPSQ [Weight] Bool (Tree d c)
ts) = QFN
-> RevDepMap
-> c
-> WeakOrTrivial
-> FlagType
-> Bool
-> WeightedPSQ [Weight] Bool (Tree d c)
-> Tree d c
forall d c.
QFN
-> RevDepMap
-> c
-> WeakOrTrivial
-> FlagType
-> Bool
-> WeightedPSQ [Weight] Bool (Tree d c)
-> Tree d c
FChoice    QFN
p RevDepMap
s c
i WeakOrTrivial
b FlagType
m Bool
d WeightedPSQ [Weight] Bool (Tree d c)
ts
inn (SChoiceF    QSN
p RevDepMap
s c
i WeakOrTrivial
b     WeightedPSQ [Weight] Bool (Tree d c)
ts) = QSN
-> RevDepMap
-> c
-> WeakOrTrivial
-> WeightedPSQ [Weight] Bool (Tree d c)
-> Tree d c
forall d c.
QSN
-> RevDepMap
-> c
-> WeakOrTrivial
-> WeightedPSQ [Weight] Bool (Tree d c)
-> Tree d c
SChoice    QSN
p RevDepMap
s c
i WeakOrTrivial
b     WeightedPSQ [Weight] Bool (Tree d c)
ts
inn (GoalChoiceF   RevDepMap
s         PSQ (Goal QPN) (Tree d c)
ts) = RevDepMap -> PSQ (Goal QPN) (Tree d c) -> Tree d c
forall d c. RevDepMap -> PSQ (Goal QPN) (Tree d c) -> Tree d c
GoalChoice   RevDepMap
s         PSQ (Goal QPN) (Tree d c)
ts
inn (DoneF       RevDepMap
x d
s           ) = RevDepMap -> d -> Tree d c
forall d c. RevDepMap -> d -> Tree d c
Done       RevDepMap
x d
s
inn (FailF       ConflictSet
c FailReason
x           ) = ConflictSet -> FailReason -> Tree d c
forall d c. ConflictSet -> FailReason -> Tree d c
Fail       ConflictSet
c FailReason
x

innM :: Monad m => TreeF d c (m (Tree d c)) -> m (Tree d c)
innM :: forall (m :: * -> *) d c.
Monad m =>
TreeF d c (m (Tree d c)) -> m (Tree d c)
innM (PChoiceF    QPN
p RevDepMap
s c
i       WeightedPSQ [Weight] POption (m (Tree d c))
ts) = (WeightedPSQ [Weight] POption (Tree d c) -> Tree d c)
-> m (WeightedPSQ [Weight] POption (Tree d c)) -> m (Tree d c)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (QPN
-> RevDepMap
-> c
-> WeightedPSQ [Weight] POption (Tree d c)
-> Tree d c
forall d c.
QPN
-> RevDepMap
-> c
-> WeightedPSQ [Weight] POption (Tree d c)
-> Tree d c
PChoice    QPN
p RevDepMap
s c
i      ) (WeightedPSQ [Weight] POption (m (Tree d c))
-> m (WeightedPSQ [Weight] POption (Tree d c))
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a.
Monad m =>
WeightedPSQ [Weight] POption (m a)
-> m (WeightedPSQ [Weight] POption a)
sequence WeightedPSQ [Weight] POption (m (Tree d c))
ts)
innM (FChoiceF    QFN
p RevDepMap
s c
i WeakOrTrivial
b FlagType
m Bool
d WeightedPSQ [Weight] Bool (m (Tree d c))
ts) = (WeightedPSQ [Weight] Bool (Tree d c) -> Tree d c)
-> m (WeightedPSQ [Weight] Bool (Tree d c)) -> m (Tree d c)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (QFN
-> RevDepMap
-> c
-> WeakOrTrivial
-> FlagType
-> Bool
-> WeightedPSQ [Weight] Bool (Tree d c)
-> Tree d c
forall d c.
QFN
-> RevDepMap
-> c
-> WeakOrTrivial
-> FlagType
-> Bool
-> WeightedPSQ [Weight] Bool (Tree d c)
-> Tree d c
FChoice    QFN
p RevDepMap
s c
i WeakOrTrivial
b FlagType
m Bool
d) (WeightedPSQ [Weight] Bool (m (Tree d c))
-> m (WeightedPSQ [Weight] Bool (Tree d c))
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a.
Monad m =>
WeightedPSQ [Weight] Bool (m a) -> m (WeightedPSQ [Weight] Bool a)
sequence WeightedPSQ [Weight] Bool (m (Tree d c))
ts)
innM (SChoiceF    QSN
p RevDepMap
s c
i WeakOrTrivial
b     WeightedPSQ [Weight] Bool (m (Tree d c))
ts) = (WeightedPSQ [Weight] Bool (Tree d c) -> Tree d c)
-> m (WeightedPSQ [Weight] Bool (Tree d c)) -> m (Tree d c)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (QSN
-> RevDepMap
-> c
-> WeakOrTrivial
-> WeightedPSQ [Weight] Bool (Tree d c)
-> Tree d c
forall d c.
QSN
-> RevDepMap
-> c
-> WeakOrTrivial
-> WeightedPSQ [Weight] Bool (Tree d c)
-> Tree d c
SChoice    QSN
p RevDepMap
s c
i WeakOrTrivial
b    ) (WeightedPSQ [Weight] Bool (m (Tree d c))
-> m (WeightedPSQ [Weight] Bool (Tree d c))
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a.
Monad m =>
WeightedPSQ [Weight] Bool (m a) -> m (WeightedPSQ [Weight] Bool a)
sequence WeightedPSQ [Weight] Bool (m (Tree d c))
ts)
innM (GoalChoiceF   RevDepMap
s         PSQ (Goal QPN) (m (Tree d c))
ts) = (PSQ (Goal QPN) (Tree d c) -> Tree d c)
-> m (PSQ (Goal QPN) (Tree d c)) -> m (Tree d c)
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (RevDepMap -> PSQ (Goal QPN) (Tree d c) -> Tree d c
forall d c. RevDepMap -> PSQ (Goal QPN) (Tree d c) -> Tree d c
GoalChoice   RevDepMap
s        ) (PSQ (Goal QPN) (m (Tree d c)) -> m (PSQ (Goal QPN) (Tree d c))
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a.
Monad m =>
PSQ (Goal QPN) (m a) -> m (PSQ (Goal QPN) a)
sequence PSQ (Goal QPN) (m (Tree d c))
ts)
innM (DoneF       RevDepMap
x d
s           ) = Tree d c -> m (Tree d c)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Tree d c -> m (Tree d c)) -> Tree d c -> m (Tree d c)
forall a b. (a -> b) -> a -> b
$ RevDepMap -> d -> Tree d c
forall d c. RevDepMap -> d -> Tree d c
Done     RevDepMap
x d
s
innM (FailF       ConflictSet
c FailReason
x           ) = Tree d c -> m (Tree d c)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Tree d c -> m (Tree d c)) -> Tree d c -> m (Tree d c)
forall a b. (a -> b) -> a -> b
$ ConflictSet -> FailReason -> Tree d c
forall d c. ConflictSet -> FailReason -> Tree d c
Fail     ConflictSet
c FailReason
x

-- | Determines whether a tree is active, i.e., isn't a failure node.
active :: Tree d c -> Bool
active :: forall d c. Tree d c -> Bool
active (Fail ConflictSet
_ FailReason
_) = Bool
False
active Tree d c
_          = Bool
True

-- | Approximates the number of active choices that are available in a node.
-- Note that we count goal choices as having one choice, always.
zeroOrOneChoices :: Tree d c -> Bool
zeroOrOneChoices :: forall d c. Tree d c -> Bool
zeroOrOneChoices (PChoice    QPN
_ RevDepMap
_ c
_       WeightedPSQ [Weight] POption (Tree d c)
ts) = WeightedPSQ [Weight] POption (Tree d c) -> Bool
forall w k v. WeightedPSQ w k v -> Bool
W.isZeroOrOne ((Tree d c -> Bool)
-> WeightedPSQ [Weight] POption (Tree d c)
-> WeightedPSQ [Weight] POption (Tree d c)
forall v k w. (v -> Bool) -> WeightedPSQ k w v -> WeightedPSQ k w v
W.filter Tree d c -> Bool
forall d c. Tree d c -> Bool
active WeightedPSQ [Weight] POption (Tree d c)
ts)
zeroOrOneChoices (FChoice    QFN
_ RevDepMap
_ c
_ WeakOrTrivial
_ FlagType
_ Bool
_ WeightedPSQ [Weight] Bool (Tree d c)
ts) = WeightedPSQ [Weight] Bool (Tree d c) -> Bool
forall w k v. WeightedPSQ w k v -> Bool
W.isZeroOrOne ((Tree d c -> Bool)
-> WeightedPSQ [Weight] Bool (Tree d c)
-> WeightedPSQ [Weight] Bool (Tree d c)
forall v k w. (v -> Bool) -> WeightedPSQ k w v -> WeightedPSQ k w v
W.filter Tree d c -> Bool
forall d c. Tree d c -> Bool
active WeightedPSQ [Weight] Bool (Tree d c)
ts)
zeroOrOneChoices (SChoice    QSN
_ RevDepMap
_ c
_ WeakOrTrivial
_     WeightedPSQ [Weight] Bool (Tree d c)
ts) = WeightedPSQ [Weight] Bool (Tree d c) -> Bool
forall w k v. WeightedPSQ w k v -> Bool
W.isZeroOrOne ((Tree d c -> Bool)
-> WeightedPSQ [Weight] Bool (Tree d c)
-> WeightedPSQ [Weight] Bool (Tree d c)
forall v k w. (v -> Bool) -> WeightedPSQ k w v -> WeightedPSQ k w v
W.filter Tree d c -> Bool
forall d c. Tree d c -> Bool
active WeightedPSQ [Weight] Bool (Tree d c)
ts)
zeroOrOneChoices (GoalChoice RevDepMap
_           PSQ (Goal QPN) (Tree d c)
_ ) = Bool
True
zeroOrOneChoices (Done       RevDepMap
_ d
_           ) = Bool
True
zeroOrOneChoices (Fail       ConflictSet
_ FailReason
_           ) = Bool
True

-- | Catamorphism on trees.
cata :: (TreeF d c a -> a) -> Tree d c -> a
cata :: forall d c a. (TreeF d c a -> a) -> Tree d c -> a
cata TreeF d c a -> a
phi Tree d c
x = (TreeF d c a -> a
phi (TreeF d c a -> a) -> (Tree d c -> TreeF d c a) -> Tree d c -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Tree d c -> a) -> TreeF d c (Tree d c) -> TreeF d c a
forall a b. (a -> b) -> TreeF d c a -> TreeF d c b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((TreeF d c a -> a) -> Tree d c -> a
forall d c a. (TreeF d c a -> a) -> Tree d c -> a
cata TreeF d c a -> a
phi) (TreeF d c (Tree d c) -> TreeF d c a)
-> (Tree d c -> TreeF d c (Tree d c)) -> Tree d c -> TreeF d c a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tree d c -> TreeF d c (Tree d c)
forall d c. Tree d c -> TreeF d c (Tree d c)
out) Tree d c
x

type TreeTrav d c a = TreeF d c (Tree d a) -> TreeF d a (Tree d a)
type EndoTreeTrav d c = TreeTrav d c c

trav :: TreeTrav d c a -> Tree d c -> Tree d a
trav :: forall d c a. TreeTrav d c a -> Tree d c -> Tree d a
trav TreeTrav d c a
psi Tree d c
x = (TreeF d c (Tree d a) -> Tree d a) -> Tree d c -> Tree d a
forall d c a. (TreeF d c a -> a) -> Tree d c -> a
cata (TreeF d a (Tree d a) -> Tree d a
forall d c. TreeF d c (Tree d c) -> Tree d c
inn (TreeF d a (Tree d a) -> Tree d a)
-> TreeTrav d c a -> TreeF d c (Tree d a) -> Tree d a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TreeTrav d c a
psi) Tree d c
x

-- | Paramorphism on trees.
para :: (TreeF d c (a, Tree d c) -> a) -> Tree d c -> a
para :: forall d c a. (TreeF d c (a, Tree d c) -> a) -> Tree d c -> a
para TreeF d c (a, Tree d c) -> a
phi = TreeF d c (a, Tree d c) -> a
phi (TreeF d c (a, Tree d c) -> a)
-> (Tree d c -> TreeF d c (a, Tree d c)) -> Tree d c -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Tree d c -> (a, Tree d c))
-> TreeF d c (Tree d c) -> TreeF d c (a, Tree d c)
forall a b. (a -> b) -> TreeF d c a -> TreeF d c b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ Tree d c
x -> ((TreeF d c (a, Tree d c) -> a) -> Tree d c -> a
forall d c a. (TreeF d c (a, Tree d c) -> a) -> Tree d c -> a
para TreeF d c (a, Tree d c) -> a
phi Tree d c
x, Tree d c
x)) (TreeF d c (Tree d c) -> TreeF d c (a, Tree d c))
-> (Tree d c -> TreeF d c (Tree d c))
-> Tree d c
-> TreeF d c (a, Tree d c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Tree d c -> TreeF d c (Tree d c)
forall d c. Tree d c -> TreeF d c (Tree d c)
out

-- | Anamorphism on trees.
ana :: (a -> TreeF d c a) -> a -> Tree d c
ana :: forall a d c. (a -> TreeF d c a) -> a -> Tree d c
ana a -> TreeF d c a
psi = TreeF d c (Tree d c) -> Tree d c
forall d c. TreeF d c (Tree d c) -> Tree d c
inn (TreeF d c (Tree d c) -> Tree d c)
-> (a -> TreeF d c (Tree d c)) -> a -> Tree d c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Tree d c) -> TreeF d c a -> TreeF d c (Tree d c)
forall a b. (a -> b) -> TreeF d c a -> TreeF d c b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> TreeF d c a) -> a -> Tree d c
forall a d c. (a -> TreeF d c a) -> a -> Tree d c
ana a -> TreeF d c a
psi) (TreeF d c a -> TreeF d c (Tree d c))
-> (a -> TreeF d c a) -> a -> TreeF d c (Tree d c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> TreeF d c a
psi