content: {-# LANGUAGE OverloadedStrings #-}
  {-# LANGUAGE QuasiQuotes #-}
  {-# LANGUAGE LambdaCase #-}
  {-# LANGUAGE DeriveFunctor #-}
  {-# LANGUAGE TypeFamilies #-}
  {-# LANGUAGE ViewPatterns #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE DeriveFunctor #-}
  {-# LANGUAGE DeriveTraversable #-}
  module Props.Internal.Props (solve, solveAll) where
  
  import qualified Props.Internal.Graph as G
  import Control.Lens hiding (Context)
  import Props.Internal.Backtracking
  import Props.Internal.Graph
  import qualified Props.Internal.MinTracker as MT
  import Data.Dynamic
  import Data.Foldable
  import Control.Monad.State
  
  solve :: Graph
        -> Maybe Graph
  solve graph' = fmap snd $ runBacktrack (initMinTracker graph') graph' solve'
  
  solveAll :: Graph -> [Graph]
  solveAll graph' = snd <$> runBacktrackAll (initMinTracker graph') graph' solve'
  
  solve' :: Backtrack ()
  solve' = MT.popMinNode >>= \case
      Nothing -> return ()
      Just n  -> collapse n *> solve'
  {-# INLINABLE solve' #-}
  
  collapse :: G.Vertex
           -> Backtrack ()
  collapse n = do
      focused <- use (singular (graph . valueAt n))
      choicesOfQ' focused n
  {-# INLINE collapse #-}
  
  choicesOfQ' :: Quantum -> Vertex -> Backtrack ()
  choicesOfQ' (Quantum (Observed{})) _ = error "Can't collapse an already collapsed node!"
  choicesOfQ' (Quantum (Unknown xs :: SuperPos f a)) n = do
      choice <- select xs
      graph . valueAt n . superPos .= (Observed choice :: SuperPos f a)
      propagate (n, toDyn choice)
  {-# INLINE choicesOfQ' #-}
  
  initMinTracker :: Graph -> MT.MinTracker
  initMinTracker graph' = MT.fromList (allEntropies ^.. traversed . below _Just)
      where
        allEntropies :: [(G.Vertex, Maybe Int)]
        allEntropies = allNodes ^.. traversed . alongside id (to entropyOfQ)
        allNodes :: [(G.Vertex, Quantum)]
        allNodes =  graph' ^.. values
  
  propagate :: (Vertex, DChoice) -> Backtrack ()
  propagate (from', choice) = do
      allEdges <- gets (toListOf (graph . edgesFrom from'))
      for_ allEdges step'
      where
        step' :: (Vertex, DFilter) -> Backtrack ()
        step' e = propagateSingle choice e
  {-# INLINE propagate #-}
  
  propagateSingle :: DChoice -> (Vertex, DFilter) -> Backtrack ()
  propagateSingle v (to', dfilter) = do
      graph . valueAt to' %%= alterQ >>= \case
        Nothing -> return ()
        Just newEnt -> MT.setNodeEntropy to' newEnt
      return ()
    where
      alterQ :: Quantum -> (Maybe Int, Quantum)
      alterQ (Quantum (Unknown xs :: SuperPos f a)) = do
          let filteredDown = (forceDyn $ dynApp (dynApp dfilter v) (toDyn xs) :: f a)
           in (Just $ length filteredDown, Quantum (Unknown filteredDown))
      alterQ q = (Nothing, q)
  {-# INLINE propagateSingle #-}
  