    module Agda.Auto.NarrowingSearch where

    import Control.Monad       ( foldM, when )
    import Control.Monad.State ( MonadState(..), modify, StateT, evalStateT, runStateT )
    import Control.Monad.Trans ( lift )

    import Data.IORef hiding (writeIORef, modifyIORef)
    import qualified Data.IORef as NoUndo (writeIORef, modifyIORef)

    import Agda.Utils.Impossible
    import Agda.Utils.Empty

    newtype Prio = Prio { Prio -> Int
    getPrio :: Int }
     deriving (Prio -> Prio -> Bool
    (Prio -> Prio -> Bool) -> (Prio -> Prio -> Bool) -> Eq Prio
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: Prio -> Prio -> Bool
    $c/= :: Prio -> Prio -> Bool
    == :: Prio -> Prio -> Bool
    $c== :: Prio -> Prio -> Bool
    Eq, Eq Prio
    Eq Prio
    -> (Prio -> Prio -> Ordering)
    -> (Prio -> Prio -> Bool)
    -> (Prio -> Prio -> Bool)
    -> (Prio -> Prio -> Bool)
    -> (Prio -> Prio -> Bool)
    -> (Prio -> Prio -> Prio)
    -> (Prio -> Prio -> Prio)
    -> Ord Prio
    Prio -> Prio -> Bool
    Prio -> Prio -> Ordering
    Prio -> Prio -> Prio
    forall a.
    Eq a
    -> (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    min :: Prio -> Prio -> Prio
    $cmin :: Prio -> Prio -> Prio
    max :: Prio -> Prio -> Prio
    $cmax :: Prio -> Prio -> Prio
    >= :: Prio -> Prio -> Bool
    $c>= :: Prio -> Prio -> Bool
    > :: Prio -> Prio -> Bool
    $c> :: Prio -> Prio -> Bool
    <= :: Prio -> Prio -> Bool
    $c<= :: Prio -> Prio -> Bool
    < :: Prio -> Prio -> Bool
    $c< :: Prio -> Prio -> Bool
    compare :: Prio -> Prio -> Ordering
    $ccompare :: Prio -> Prio -> Ordering
    Ord, Integer -> Prio
    Prio -> Prio
    Prio -> Prio -> Prio
    (Prio -> Prio -> Prio)
    -> (Prio -> Prio -> Prio)
    -> (Prio -> Prio -> Prio)
    -> (Prio -> Prio)
    -> (Prio -> Prio)
    -> (Prio -> Prio)
    -> (Integer -> Prio)
    -> Num Prio
    forall a.
    (a -> a -> a)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> (a -> a)
    -> (a -> a)
    -> (a -> a)
    -> (Integer -> a)
    -> Num a
    fromInteger :: Integer -> Prio
    $cfromInteger :: Integer -> Prio
    signum :: Prio -> Prio
    $csignum :: Prio -> Prio
    abs :: Prio -> Prio
    $cabs :: Prio -> Prio
    negate :: Prio -> Prio
    $cnegate :: Prio -> Prio
    * :: Prio -> Prio -> Prio
    $c* :: Prio -> Prio -> Prio
    - :: Prio -> Prio -> Prio
    $c- :: Prio -> Prio -> Prio
    + :: Prio -> Prio -> Prio
    $c+ :: Prio -> Prio -> Prio
    Num)

    class Trav a where
      type Block a
      trav :: Monad m => (forall b. TravWith b (Block a) => MM b (Block b) -> m ()) -> a -> m ()

    -- | Trav instance 'a' with block type 'blk'
    type TravWith a blk = (Trav a, Block a ~ blk)

    instance TravWith a blk => Trav (MM a blk) where
      type Block (MM a blk) = blk
      trav :: forall (m :: * -> *).
    Monad m =>
    (forall b. TravWith b (Block (MM a blk)) => MM b (Block b) -> m ())
    -> MM a blk -> m ()
    trav forall b. TravWith b (Block (MM a blk)) => MM b (Block b) -> m ()
    f MM a blk
    me = MM a (Block a) -> m ()
    forall b. TravWith b (Block (MM a blk)) => MM b (Block b) -> m ()
    f MM a blk
    MM a (Block a)
    me

    data Term blk = forall a. TravWith a blk => Term a

    -- | Result of type-checking.
    data Prop blk
      = OK
        -- ^ Success.
      | Error String
        -- ^ Definite failure.
      | forall a . AddExtraRef String (Metavar a blk) (Move' blk a)
        -- ^ Experimental.
      | And (Maybe [Term blk]) (MetaEnv (PB blk)) (MetaEnv (PB blk))
        -- ^ Parallel conjunction of constraints.
      | Sidecondition (MetaEnv (PB blk)) (MetaEnv (PB blk))
        -- ^ Experimental, related to 'mcompoint'.
        -- First arg is sidecondition.
      | Or Prio (MetaEnv (PB blk)) (MetaEnv (PB blk))
        -- ^ Forking proof on something that is not part of the term language.
        --   E.g. whether a term will reduce or not.
      | ConnectHandle (OKHandle blk) (MetaEnv (PB blk))
        -- ^ Obsolete.

    data OKVal = OKVal
    type OKHandle blk = MM OKVal blk
    type OKMeta blk = Metavar OKVal blk

    -- | Agsy's meta variables.
    --
    --   @a@ the type of the metavariable (what it can be instantiated with).
    --   @blk@ the search control information (e.g. the scope of the meta).

    data Metavar a blk = Metavar
      { forall a blk. Metavar a blk -> IORef (Maybe a)
    mbind :: IORef (Maybe a)
        -- ^ Maybe an instantiation (refinement).  It is usually shallow,
        --   i.e., just one construct(or) with arguments again being metas.
      , forall a blk. Metavar a blk -> IORef Bool
    mprincipalpresent :: IORef Bool
        -- ^ Does this meta block a principal constraint
        --   (i.e., a type-checking constraint).
      , forall a blk.
    Metavar a blk -> IORef [(QPB a blk, Maybe (CTree blk))]
    mobs :: IORef [(QPB a blk, Maybe (CTree blk))]
        -- ^ List of observers, i.e., constraints blocked by this meta.
      , forall a blk. Metavar a blk -> IORef [SubConstraints blk]
    mcompoint :: IORef [SubConstraints blk]
        -- ^ Used for experiments with independence of subproofs.
      , forall a blk. Metavar a blk -> IORef [Move' blk a]
    mextrarefs :: IORef [Move' blk a]
        -- ^ Experimental.
      }

    hequalMetavar :: Metavar a1 blk1 -> Metavar a2 bkl2 -> Bool
    hequalMetavar :: forall a1 blk1 a2 bkl2. Metavar a1 blk1 -> Metavar a2 bkl2 -> Bool
    hequalMetavar Metavar a1 blk1
    m1 Metavar a2 bkl2
    m2 = Metavar a1 blk1 -> IORef Bool
    forall a blk. Metavar a blk -> IORef Bool
    mprincipalpresent Metavar a1 blk1
    m1 IORef Bool -> IORef Bool -> Bool
    forall a. Eq a => a -> a -> Bool
    == Metavar a2 bkl2 -> IORef Bool
    forall a blk. Metavar a blk -> IORef Bool
    mprincipalpresent Metavar a2 bkl2
    m2

    instance Eq (Metavar a blk) where
     Metavar a blk
    x == :: Metavar a blk -> Metavar a blk -> Bool
    == Metavar a blk
    y = Metavar a blk -> Metavar a blk -> Bool
    forall a1 blk1 a2 bkl2. Metavar a1 blk1 -> Metavar a2 bkl2 -> Bool
    hequalMetavar Metavar a blk
    x Metavar a blk
    y

    newMeta :: IORef [SubConstraints blk] -> IO (Metavar a blk)
    newMeta :: forall blk a. IORef [SubConstraints blk] -> IO (Metavar a blk)
    newMeta IORef [SubConstraints blk]
    mcompoint = do
     IORef (Maybe a)
    bind <- Maybe a -> IO (IORef (Maybe a))
    forall a. a -> IO (IORef a)
    newIORef Maybe a
    forall a. Maybe a
    Nothing
     IORef Bool
    pp <- Bool -> IO (IORef Bool)
    forall a. a -> IO (IORef a)
    newIORef Bool
    False
     IORef [(QPB a blk, Maybe (CTree blk))]
    obs <- [(QPB a blk, Maybe (CTree blk))]
    -> IO (IORef [(QPB a blk, Maybe (CTree blk))])
    forall a. a -> IO (IORef a)
    newIORef []
     IORef [Move' blk a]
    erefs <- [Move' blk a] -> IO (IORef [Move' blk a])
    forall a. a -> IO (IORef a)
    newIORef []
     Metavar a blk -> IO (Metavar a blk)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Metavar a blk -> IO (Metavar a blk))
    -> Metavar a blk -> IO (Metavar a blk)
    forall a b. (a -> b) -> a -> b
    $ IORef (Maybe a)
    -> IORef Bool
    -> IORef [(QPB a blk, Maybe (CTree blk))]
    -> IORef [SubConstraints blk]
    -> IORef [Move' blk a]
    -> Metavar a blk
    forall a blk.
    IORef (Maybe a)
    -> IORef Bool
    -> IORef [(QPB a blk, Maybe (CTree blk))]
    -> IORef [SubConstraints blk]
    -> IORef [Move' blk a]
    -> Metavar a blk
    Metavar IORef (Maybe a)
    bind IORef Bool
    pp IORef [(QPB a blk, Maybe (CTree blk))]
    obs IORef [SubConstraints blk]
    mcompoint IORef [Move' blk a]
    erefs

    initMeta :: IO (Metavar a blk)
    initMeta :: forall a blk. IO (Metavar a blk)
    initMeta = do
     IORef [SubConstraints blk]
    cp <- [SubConstraints blk] -> IO (IORef [SubConstraints blk])
    forall a. a -> IO (IORef a)
    newIORef []
     IORef [SubConstraints blk] -> IO (Metavar a blk)
    forall blk a. IORef [SubConstraints blk] -> IO (Metavar a blk)
    newMeta IORef [SubConstraints blk]
    cp

    data CTree blk = CTree
     {forall blk. CTree blk -> IORef (PrioMeta blk)
    ctpriometa :: IORef (PrioMeta blk),
      forall blk. CTree blk -> IORef (Maybe (SubConstraints blk))
    ctsub :: IORef (Maybe (SubConstraints blk)),
      forall blk. CTree blk -> IORef (Maybe (CTree blk))
    ctparent :: IORef (Maybe (CTree blk)), -- Nothing - root
      forall blk. CTree blk -> IORef [OKMeta blk]
    cthandles :: IORef [OKMeta blk]
     }

    data SubConstraints blk = SubConstraints
     {forall blk. SubConstraints blk -> IORef Bool
    scflip :: IORef Bool,
      forall blk. SubConstraints blk -> IORef Int
    sccomcount :: IORef Int,
      forall blk. SubConstraints blk -> CTree blk
    scsub1 :: CTree blk,
      forall blk. SubConstraints blk -> CTree blk
    scsub2 :: CTree blk
     }

    newCTree :: Maybe (CTree blk) -> IO (CTree blk)
    newCTree :: forall blk. Maybe (CTree blk) -> IO (CTree blk)
    newCTree Maybe (CTree blk)
    parent = do
     IORef (PrioMeta blk)
    priometa <- PrioMeta blk -> IO (IORef (PrioMeta blk))
    forall a. a -> IO (IORef a)
    newIORef (Bool -> PrioMeta blk
    forall blk. Bool -> PrioMeta blk
    NoPrio Bool
    False)
     IORef (Maybe (SubConstraints blk))
    sub <- Maybe (SubConstraints blk)
    -> IO (IORef (Maybe (SubConstraints blk)))
    forall a. a -> IO (IORef a)
    newIORef Maybe (SubConstraints blk)
    forall a. Maybe a
    Nothing
     IORef (Maybe (CTree blk))
    rparent <- Maybe (CTree blk) -> IO (IORef (Maybe (CTree blk)))
    forall a. a -> IO (IORef a)
    newIORef Maybe (CTree blk)
    parent
     IORef [OKMeta blk]
    handles <- [OKMeta blk] -> IO (IORef [OKMeta blk])
    forall a. a -> IO (IORef a)
    newIORef []
     CTree blk -> IO (CTree blk)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (CTree blk -> IO (CTree blk)) -> CTree blk -> IO (CTree blk)
    forall a b. (a -> b) -> a -> b
    $ IORef (PrioMeta blk)
    -> IORef (Maybe (SubConstraints blk))
    -> IORef (Maybe (CTree blk))
    -> IORef [OKMeta blk]
    -> CTree blk
    forall blk.
    IORef (PrioMeta blk)
    -> IORef (Maybe (SubConstraints blk))
    -> IORef (Maybe (CTree blk))
    -> IORef [OKMeta blk]
    -> CTree blk
    CTree IORef (PrioMeta blk)
    priometa IORef (Maybe (SubConstraints blk))
    sub IORef (Maybe (CTree blk))
    rparent IORef [OKMeta blk]
    handles

    newSubConstraints :: CTree blk -> IO (SubConstraints blk)
    newSubConstraints :: forall blk. CTree blk -> IO (SubConstraints blk)
    newSubConstraints CTree blk
    node = do
     IORef Bool
    flip <- Bool -> IO (IORef Bool)
    forall a. a -> IO (IORef a)
    newIORef Bool
    True -- False -- initially (and always) True, trying out prefer rightmost subterm when none have priority
     IORef Int
    comcount <- Int -> IO (IORef Int)
    forall a. a -> IO (IORef a)
    newIORef Int
    0
     CTree blk
    sub1 <- Maybe (CTree blk) -> IO (CTree blk)
    forall blk. Maybe (CTree blk) -> IO (CTree blk)
    newCTree (Maybe (CTree blk) -> IO (CTree blk))
    -> Maybe (CTree blk) -> IO (CTree blk)
    forall a b. (a -> b) -> a -> b
    $ CTree blk -> Maybe (CTree blk)
    forall a. a -> Maybe a
    Just CTree blk
    node
     CTree blk
    sub2 <- Maybe (CTree blk) -> IO (CTree blk)
    forall blk. Maybe (CTree blk) -> IO (CTree blk)
    newCTree (Maybe (CTree blk) -> IO (CTree blk))
    -> Maybe (CTree blk) -> IO (CTree blk)
    forall a b. (a -> b) -> a -> b
    $ CTree blk -> Maybe (CTree blk)
    forall a. a -> Maybe a
    Just CTree blk
    node
     SubConstraints blk -> IO (SubConstraints blk)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SubConstraints blk -> IO (SubConstraints blk))
    -> SubConstraints blk -> IO (SubConstraints blk)
    forall a b. (a -> b) -> a -> b
    $ IORef Bool
    -> IORef Int -> CTree blk -> CTree blk -> SubConstraints blk
    forall blk.
    IORef Bool
    -> IORef Int -> CTree blk -> CTree blk -> SubConstraints blk
    SubConstraints IORef Bool
    flip IORef Int
    comcount CTree blk
    sub1 CTree blk
    sub2

    data PrioMeta blk = forall a . Refinable a blk => PrioMeta Prio (Metavar a blk)
                      | NoPrio Bool -- True if subconstraint is done (all OK)

    instance Eq (PrioMeta blk) where
     NoPrio Bool
    d1 == :: PrioMeta blk -> PrioMeta blk -> Bool
    == NoPrio Bool
    d2 = Bool
    d1 Bool -> Bool -> Bool
    forall a. Eq a => a -> a -> Bool
    == Bool
    d2
     PrioMeta Prio
    p1 Metavar a blk
    m1 == PrioMeta Prio
    p2 Metavar a blk
    m2 = Prio
    p1 Prio -> Prio -> Bool
    forall a. Eq a => a -> a -> Bool
    == Prio
    p2 Bool -> Bool -> Bool
    && Metavar a blk -> Metavar a blk -> Bool
    forall a1 blk1 a2 bkl2. Metavar a1 blk1 -> Metavar a2 bkl2 -> Bool
    hequalMetavar Metavar a blk
    m1 Metavar a blk
    m2
     PrioMeta blk
    _ == PrioMeta blk
    _ = Bool
    False

    -- -----------------------

    data Restore = forall a . Restore (IORef a) a

    type Undo = StateT [Restore] IO

    ureadIORef :: IORef a -> Undo a
    ureadIORef :: forall a. IORef a -> Undo a
    ureadIORef IORef a
    ptr = IO a -> StateT [Restore] IO a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (IO a -> StateT [Restore] IO a) -> IO a -> StateT [Restore] IO a
    forall a b. (a -> b) -> a -> b
    $ IORef a -> IO a
    forall a. IORef a -> IO a
    readIORef IORef a
    ptr

    uwriteIORef :: IORef a -> a -> Undo ()
    uwriteIORef :: forall a. IORef a -> a -> Undo ()
    uwriteIORef IORef a
    ptr a
    newval = do
     a
    oldval <- IORef a -> Undo a
    forall a. IORef a -> Undo a
    ureadIORef IORef a
    ptr
     ([Restore] -> [Restore]) -> Undo ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify (IORef a -> a -> Restore
    forall a. IORef a -> a -> Restore
    Restore IORef a
    ptr a
    oldval Restore -> [Restore] -> [Restore]
    forall a. a -> [a] -> [a]
    :)
     IO () -> Undo ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (IO () -> Undo ()) -> IO () -> Undo ()
    forall a b. (a -> b) -> a -> b
    $ IORef a -> a -> IO ()
    forall a. IORef a -> a -> IO ()
    NoUndo.writeIORef IORef a
    ptr a
    newval

    umodifyIORef :: IORef a -> (a -> a) -> Undo ()
    umodifyIORef :: forall a. IORef a -> (a -> a) -> Undo ()
    umodifyIORef IORef a
    ptr a -> a
    f = do
     a
    oldval <- IORef a -> Undo a
    forall a. IORef a -> Undo a
    ureadIORef IORef a
    ptr
     ([Restore] -> [Restore]) -> Undo ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify (IORef a -> a -> Restore
    forall a. IORef a -> a -> Restore
    Restore IORef a
    ptr a
    oldval Restore -> [Restore] -> [Restore]
    forall a. a -> [a] -> [a]
    :)
     IO () -> Undo ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (IO () -> Undo ()) -> IO () -> Undo ()
    forall a b. (a -> b) -> a -> b
    $ IORef a -> a -> IO ()
    forall a. IORef a -> a -> IO ()
    NoUndo.writeIORef IORef a
    ptr (a -> a
    f a
    oldval)

    ureadmodifyIORef :: IORef a -> (a -> a) -> Undo a
    ureadmodifyIORef :: forall a. IORef a -> (a -> a) -> Undo a
    ureadmodifyIORef IORef a
    ptr a -> a
    f = do
     a
    oldval <- IORef a -> Undo a
    forall a. IORef a -> Undo a
    ureadIORef IORef a
    ptr
     ([Restore] -> [Restore]) -> Undo ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify (IORef a -> a -> Restore
    forall a. IORef a -> a -> Restore
    Restore IORef a
    ptr a
    oldval Restore -> [Restore] -> [Restore]
    forall a. a -> [a] -> [a]
    :)
     IO () -> Undo ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (IO () -> Undo ()) -> IO () -> Undo ()
    forall a b. (a -> b) -> a -> b
    $ IORef a -> a -> IO ()
    forall a. IORef a -> a -> IO ()
    NoUndo.writeIORef IORef a
    ptr (a -> a
    f a
    oldval)
     a -> Undo a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    oldval

    runUndo :: Undo a -> IO a
    runUndo :: forall a. Undo a -> IO a
    runUndo Undo a
    x = do
     (a
    res, [Restore]
    restores) <- Undo a -> [Restore] -> IO (a, [Restore])
    forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
    runStateT Undo a
    x []
     (Restore -> IO ()) -> [Restore] -> IO ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (\(Restore IORef a
    ptr a
    oldval) -> IORef a -> a -> IO ()
    forall a. IORef a -> a -> IO ()
    NoUndo.writeIORef IORef a
    ptr a
    oldval) [Restore]
    restores
     a -> IO a
    forall (m :: * -> *) a. Monad m => a -> m a
    return a
    res

    -- -----------------------

    newtype RefCreateEnv blk a = RefCreateEnv
      { forall blk a.
    RefCreateEnv blk a -> StateT (IORef [SubConstraints blk], Int) IO a
    runRefCreateEnv :: StateT ((IORef [SubConstraints blk]), Int) IO a }

    instance Functor (RefCreateEnv blk) where
      fmap :: forall a b. (a -> b) -> RefCreateEnv blk a -> RefCreateEnv blk b
    fmap a -> b
    f = StateT (IORef [SubConstraints blk], Int) IO b -> RefCreateEnv blk b
    forall blk a.
    StateT (IORef [SubConstraints blk], Int) IO a -> RefCreateEnv blk a
    RefCreateEnv (StateT (IORef [SubConstraints blk], Int) IO b
     -> RefCreateEnv blk b)
    -> (RefCreateEnv blk a
        -> StateT (IORef [SubConstraints blk], Int) IO b)
    -> RefCreateEnv blk a
    -> RefCreateEnv blk b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (a -> b)
    -> StateT (IORef [SubConstraints blk], Int) IO a
    -> StateT (IORef [SubConstraints blk], Int) IO b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap a -> b
    f (StateT (IORef [SubConstraints blk], Int) IO a
     -> StateT (IORef [SubConstraints blk], Int) IO b)
    -> (RefCreateEnv blk a
        -> StateT (IORef [SubConstraints blk], Int) IO a)
    -> RefCreateEnv blk a
    -> StateT (IORef [SubConstraints blk], Int) IO b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . RefCreateEnv blk a -> StateT (IORef [SubConstraints blk], Int) IO a
    forall blk a.
    RefCreateEnv blk a -> StateT (IORef [SubConstraints blk], Int) IO a
    runRefCreateEnv

    instance Applicative (RefCreateEnv blk) where
      pure :: forall a. a -> RefCreateEnv blk a
    pure    = StateT (IORef [SubConstraints blk], Int) IO a -> RefCreateEnv blk a
    forall blk a.
    StateT (IORef [SubConstraints blk], Int) IO a -> RefCreateEnv blk a
    RefCreateEnv (StateT (IORef [SubConstraints blk], Int) IO a
     -> RefCreateEnv blk a)
    -> (a -> StateT (IORef [SubConstraints blk], Int) IO a)
    -> a
    -> RefCreateEnv blk a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> StateT (IORef [SubConstraints blk], Int) IO a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure
      RefCreateEnv blk (a -> b)
    f <*> :: forall a b.
    RefCreateEnv blk (a -> b)
    -> RefCreateEnv blk a -> RefCreateEnv blk b
    <*> RefCreateEnv blk a
    t = StateT (IORef [SubConstraints blk], Int) IO b -> RefCreateEnv blk b
    forall blk a.
    StateT (IORef [SubConstraints blk], Int) IO a -> RefCreateEnv blk a
    RefCreateEnv (StateT (IORef [SubConstraints blk], Int) IO b
     -> RefCreateEnv blk b)
    -> StateT (IORef [SubConstraints blk], Int) IO b
    -> RefCreateEnv blk b
    forall a b. (a -> b) -> a -> b
    $ RefCreateEnv blk (a -> b)
    -> StateT (IORef [SubConstraints blk], Int) IO (a -> b)
    forall blk a.
    RefCreateEnv blk a -> StateT (IORef [SubConstraints blk], Int) IO a
    runRefCreateEnv RefCreateEnv blk (a -> b)
    f StateT (IORef [SubConstraints blk], Int) IO (a -> b)
    -> StateT (IORef [SubConstraints blk], Int) IO a
    -> StateT (IORef [SubConstraints blk], Int) IO b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> RefCreateEnv blk a -> StateT (IORef [SubConstraints blk], Int) IO a
    forall blk a.
    RefCreateEnv blk a -> StateT (IORef [SubConstraints blk], Int) IO a
    runRefCreateEnv RefCreateEnv blk a
    t

    instance Monad (RefCreateEnv blk) where
      return :: forall a. a -> RefCreateEnv blk a
    return = a -> RefCreateEnv blk a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure
      RefCreateEnv blk a
    t >>= :: forall a b.
    RefCreateEnv blk a
    -> (a -> RefCreateEnv blk b) -> RefCreateEnv blk b
    >>= a -> RefCreateEnv blk b
    f = StateT (IORef [SubConstraints blk], Int) IO b -> RefCreateEnv blk b
    forall blk a.
    StateT (IORef [SubConstraints blk], Int) IO a -> RefCreateEnv blk a
    RefCreateEnv (StateT (IORef [SubConstraints blk], Int) IO b
     -> RefCreateEnv blk b)
    -> StateT (IORef [SubConstraints blk], Int) IO b
    -> RefCreateEnv blk b
    forall a b. (a -> b) -> a -> b
    $ RefCreateEnv blk a -> StateT (IORef [SubConstraints blk], Int) IO a
    forall blk a.
    RefCreateEnv blk a -> StateT (IORef [SubConstraints blk], Int) IO a
    runRefCreateEnv RefCreateEnv blk a
    t StateT (IORef [SubConstraints blk], Int) IO a
    -> (a -> StateT (IORef [SubConstraints blk], Int) IO b)
    -> StateT (IORef [SubConstraints blk], Int) IO b
    forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
    >>= RefCreateEnv blk b -> StateT (IORef [SubConstraints blk], Int) IO b
    forall blk a.
    RefCreateEnv blk a -> StateT (IORef [SubConstraints blk], Int) IO a
    runRefCreateEnv (RefCreateEnv blk b
     -> StateT (IORef [SubConstraints blk], Int) IO b)
    -> (a -> RefCreateEnv blk b)
    -> a
    -> StateT (IORef [SubConstraints blk], Int) IO b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> RefCreateEnv blk b
    f

    newtype Cost = Cost { Cost -> Int
    getCost :: Int }
      deriving (Integer -> Cost
    Cost -> Cost
    Cost -> Cost -> Cost
    (Cost -> Cost -> Cost)
    -> (Cost -> Cost -> Cost)
    -> (Cost -> Cost -> Cost)
    -> (Cost -> Cost)
    -> (Cost -> Cost)
    -> (Cost -> Cost)
    -> (Integer -> Cost)
    -> Num Cost
    forall a.
    (a -> a -> a)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> (a -> a)
    -> (a -> a)
    -> (a -> a)
    -> (Integer -> a)
    -> Num a
    fromInteger :: Integer -> Cost
    $cfromInteger :: Integer -> Cost
    signum :: Cost -> Cost
    $csignum :: Cost -> Cost
    abs :: Cost -> Cost
    $cabs :: Cost -> Cost
    negate :: Cost -> Cost
    $cnegate :: Cost -> Cost
    * :: Cost -> Cost -> Cost
    $c* :: Cost -> Cost -> Cost
    - :: Cost -> Cost -> Cost
    $c- :: Cost -> Cost -> Cost
    + :: Cost -> Cost -> Cost
    $c+ :: Cost -> Cost -> Cost
    Num, Cost -> Cost -> Bool
    (Cost -> Cost -> Bool) -> (Cost -> Cost -> Bool) -> Eq Cost
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: Cost -> Cost -> Bool
    $c/= :: Cost -> Cost -> Bool
    == :: Cost -> Cost -> Bool
    $c== :: Cost -> Cost -> Bool
    Eq, Eq Cost
    Eq Cost
    -> (Cost -> Cost -> Ordering)
    -> (Cost -> Cost -> Bool)
    -> (Cost -> Cost -> Bool)
    -> (Cost -> Cost -> Bool)
    -> (Cost -> Cost -> Bool)
    -> (Cost -> Cost -> Cost)
    -> (Cost -> Cost -> Cost)
    -> Ord Cost
    Cost -> Cost -> Bool
    Cost -> Cost -> Ordering
    Cost -> Cost -> Cost
    forall a.
    Eq a
    -> (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    min :: Cost -> Cost -> Cost
    $cmin :: Cost -> Cost -> Cost
    max :: Cost -> Cost -> Cost
    $cmax :: Cost -> Cost -> Cost
    >= :: Cost -> Cost -> Bool
    $c>= :: Cost -> Cost -> Bool
    > :: Cost -> Cost -> Bool
    $c> :: Cost -> Cost -> Bool
    <= :: Cost -> Cost -> Bool
    $c<= :: Cost -> Cost -> Bool
    < :: Cost -> Cost -> Bool
    $c< :: Cost -> Cost -> Bool
    compare :: Cost -> Cost -> Ordering
    $ccompare :: Cost -> Cost -> Ordering
    Ord)

    data Move' blk a = Move
      { forall blk a. Move' blk a -> Cost
    moveCost :: Cost
      , forall blk a. Move' blk a -> RefCreateEnv blk a
    moveNext :: RefCreateEnv blk a
      }

    class Refinable a blk where
     refinements :: blk -> [blk] -> Metavar a blk -> IO [Move' blk a]

    newPlaceholder :: RefCreateEnv blk (MM a blk)
    newPlaceholder :: forall blk a. RefCreateEnv blk (MM a blk)
    newPlaceholder = StateT (IORef [SubConstraints blk], Int) IO (MM a blk)
    -> RefCreateEnv blk (MM a blk)
    forall blk a.
    StateT (IORef [SubConstraints blk], Int) IO a -> RefCreateEnv blk a
    RefCreateEnv (StateT (IORef [SubConstraints blk], Int) IO (MM a blk)
     -> RefCreateEnv blk (MM a blk))
    -> StateT (IORef [SubConstraints blk], Int) IO (MM a blk)
    -> RefCreateEnv blk (MM a blk)
    forall a b. (a -> b) -> a -> b
    $ do
     (IORef [SubConstraints blk]
    mcompoint, Int
    c) <- StateT
      (IORef [SubConstraints blk], Int)
      IO
      (IORef [SubConstraints blk], Int)
    forall s (m :: * -> *). MonadState s m => m s
    get
     Metavar a blk
    m <- IO (Metavar a blk)
    -> StateT (IORef [SubConstraints blk], Int) IO (Metavar a blk)
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (IO (Metavar a blk)
     -> StateT (IORef [SubConstraints blk], Int) IO (Metavar a blk))
    -> IO (Metavar a blk)
    -> StateT (IORef [SubConstraints blk], Int) IO (Metavar a blk)
    forall a b. (a -> b) -> a -> b
    $ IORef [SubConstraints blk] -> IO (Metavar a blk)
    forall blk a. IORef [SubConstraints blk] -> IO (Metavar a blk)
    newMeta IORef [SubConstraints blk]
    mcompoint
     (IORef [SubConstraints blk], Int)
    -> StateT (IORef [SubConstraints blk], Int) IO ()
    forall s (m :: * -> *). MonadState s m => s -> m ()
    put (IORef [SubConstraints blk]
    mcompoint, (Int
    c Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1))
     MM a blk -> StateT (IORef [SubConstraints blk], Int) IO (MM a blk)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (MM a blk
     -> StateT (IORef [SubConstraints blk], Int) IO (MM a blk))
    -> MM a blk
    -> StateT (IORef [SubConstraints blk], Int) IO (MM a blk)
    forall a b. (a -> b) -> a -> b
    $ Metavar a blk -> MM a blk
    forall a blk. Metavar a blk -> MM a blk
    Meta Metavar a blk
    m

    newOKHandle :: RefCreateEnv blk (OKHandle blk)
    newOKHandle :: forall blk. RefCreateEnv blk (OKHandle blk)
    newOKHandle = StateT (IORef [SubConstraints blk], Int) IO (MM OKVal blk)
    -> RefCreateEnv blk (MM OKVal blk)
    forall blk a.
    StateT (IORef [SubConstraints blk], Int) IO a -> RefCreateEnv blk a
    RefCreateEnv (StateT (IORef [SubConstraints blk], Int) IO (MM OKVal blk)
     -> RefCreateEnv blk (MM OKVal blk))
    -> StateT (IORef [SubConstraints blk], Int) IO (MM OKVal blk)
    -> RefCreateEnv blk (MM OKVal blk)
    forall a b. (a -> b) -> a -> b
    $ do
     (IORef [SubConstraints blk]
    e, Int
    c) <- StateT
      (IORef [SubConstraints blk], Int)
      IO
      (IORef [SubConstraints blk], Int)
    forall s (m :: * -> *). MonadState s m => m s
    get
     IORef [SubConstraints blk]
    cp <- IO (IORef [SubConstraints blk])
    -> StateT
         (IORef [SubConstraints blk], Int) IO (IORef [SubConstraints blk])
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (IO (IORef [SubConstraints blk])
     -> StateT
          (IORef [SubConstraints blk], Int) IO (IORef [SubConstraints blk]))
    -> IO (IORef [SubConstraints blk])
    -> StateT
         (IORef [SubConstraints blk], Int) IO (IORef [SubConstraints blk])
    forall a b. (a -> b) -> a -> b
    $ [SubConstraints blk] -> IO (IORef [SubConstraints blk])
    forall a. a -> IO (IORef a)
    newIORef []
     Metavar OKVal blk
    m  <- IO (Metavar OKVal blk)
    -> StateT (IORef [SubConstraints blk], Int) IO (Metavar OKVal blk)
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (IO (Metavar OKVal blk)
     -> StateT (IORef [SubConstraints blk], Int) IO (Metavar OKVal blk))
    -> IO (Metavar OKVal blk)
    -> StateT (IORef [SubConstraints blk], Int) IO (Metavar OKVal blk)
    forall a b. (a -> b) -> a -> b
    $ IORef [SubConstraints blk] -> IO (Metavar OKVal blk)
    forall blk a. IORef [SubConstraints blk] -> IO (Metavar a blk)
    newMeta IORef [SubConstraints blk]
    cp
     (IORef [SubConstraints blk], Int)
    -> StateT (IORef [SubConstraints blk], Int) IO ()
    forall s (m :: * -> *). MonadState s m => s -> m ()
    put (IORef [SubConstraints blk]
    e, (Int
    c Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1))
     MM OKVal blk
    -> StateT (IORef [SubConstraints blk], Int) IO (MM OKVal blk)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (MM OKVal blk
     -> StateT (IORef [SubConstraints blk], Int) IO (MM OKVal blk))
    -> MM OKVal blk
    -> StateT (IORef [SubConstraints blk], Int) IO (MM OKVal blk)
    forall a b. (a -> b) -> a -> b
    $ Metavar OKVal blk -> MM OKVal blk
    forall a blk. Metavar a blk -> MM a blk
    Meta Metavar OKVal blk
    m

    dryInstantiate :: RefCreateEnv blk a -> IO a
    dryInstantiate :: forall blk a. RefCreateEnv blk a -> IO a
    dryInstantiate RefCreateEnv blk a
    bind = StateT (IORef [SubConstraints blk], Int) IO a
    -> (IORef [SubConstraints blk], Int) -> IO a
    forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
    evalStateT (RefCreateEnv blk a -> StateT (IORef [SubConstraints blk], Int) IO a
    forall blk a.
    RefCreateEnv blk a -> StateT (IORef [SubConstraints blk], Int) IO a
    runRefCreateEnv RefCreateEnv blk a
    bind) (IORef [SubConstraints blk]
    forall a. HasCallStack => a
    __IMPOSSIBLE__, Int
    0)

    type BlkInfo blk = (Bool, Prio, Maybe blk) -- Bool - is principal

    data MM a blk = NotM a
                  | Meta (Metavar a blk)

    rm :: Empty -> MM a b -> a
    rm :: forall a b. Empty -> MM a b -> a
    rm Empty
    _ (NotM a
    x) = a
    x
    rm Empty
    e Meta{}   = Empty -> a
    forall a. Empty -> a
    absurd Empty
    e

    type MetaEnv = IO

    data MB a blk = NotB a
                  | forall b . Refinable b blk => Blocked (Metavar b blk) (MetaEnv (MB a blk))
                  | Failed String

    data PB blk = NotPB (Prop blk)
                | forall b . Refinable b blk => PBlocked (Metavar b blk) (BlkInfo blk) (MetaEnv (PB blk))
                | forall b1 b2 . (Refinable b1 blk, Refinable b2 blk) => PDoubleBlocked (Metavar b1 blk) (Metavar b2 blk) (MetaEnv (PB blk))

    data QPB b blk = QPBlocked (BlkInfo blk) (MetaEnv (PB blk))
                   | QPDoubleBlocked (IORef Bool) (MetaEnv (PB blk)) -- flag set True by first observer that continues

    mmcase :: Refinable a blk => MM a blk -> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
    mmcase :: forall a blk b.
    Refinable a blk =>
    MM a blk -> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
    mmcase MM a blk
    x a -> MetaEnv (MB b blk)
    f = case MM a blk
    x of
     NotM a
    x -> a -> MetaEnv (MB b blk)
    f a
    x
     x :: MM a blk
    x@(Meta Metavar a blk
    m) -> do
      Maybe a
    bind <- IORef (Maybe a) -> IO (Maybe a)
    forall a. IORef a -> IO a
    readIORef (IORef (Maybe a) -> IO (Maybe a))
    -> IORef (Maybe a) -> IO (Maybe a)
    forall a b. (a -> b) -> a -> b
    $ Metavar a blk -> IORef (Maybe a)
    forall a blk. Metavar a blk -> IORef (Maybe a)
    mbind Metavar a blk
    m
      case Maybe a
    bind of
       Just a
    x -> a -> MetaEnv (MB b blk)
    f a
    x
       Maybe a
    Nothing -> MB b blk -> MetaEnv (MB b blk)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (MB b blk -> MetaEnv (MB b blk)) -> MB b blk -> MetaEnv (MB b blk)
    forall a b. (a -> b) -> a -> b
    $ Metavar a blk -> MetaEnv (MB b blk) -> MB b blk
    forall a blk b.
    Refinable b blk =>
    Metavar b blk -> MetaEnv (MB a blk) -> MB a blk
    Blocked Metavar a blk
    m (MM a blk -> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
    forall a blk b.
    Refinable a blk =>
    MM a blk -> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
    mmcase MM a blk
    x a -> MetaEnv (MB b blk)
    f)

    mmmcase :: MM a blk -> MetaEnv (MB b blk) -> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
    mmmcase :: forall a blk b.
    MM a blk
    -> MetaEnv (MB b blk)
    -> (a -> MetaEnv (MB b blk))
    -> MetaEnv (MB b blk)
    mmmcase MM a blk
    x MetaEnv (MB b blk)
    fm a -> MetaEnv (MB b blk)
    f = case MM a blk
    x of
     NotM a
    x -> a -> MetaEnv (MB b blk)
    f a
    x
     Meta Metavar a blk
    m -> do
      Maybe a
    bind <- IORef (Maybe a) -> IO (Maybe a)
    forall a. IORef a -> IO a
    readIORef (IORef (Maybe a) -> IO (Maybe a))
    -> IORef (Maybe a) -> IO (Maybe a)
    forall a b. (a -> b) -> a -> b
    $ Metavar a blk -> IORef (Maybe a)
    forall a blk. Metavar a blk -> IORef (Maybe a)
    mbind Metavar a blk
    m
      MetaEnv (MB b blk)
    -> (a -> MetaEnv (MB b blk)) -> Maybe a -> MetaEnv (MB b blk)
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe MetaEnv (MB b blk)
    fm a -> MetaEnv (MB b blk)
    f Maybe a
    bind

    mmpcase :: Refinable a blk => BlkInfo blk -> MM a blk -> (a -> MetaEnv (PB blk)) -> MetaEnv (PB blk)
    mmpcase :: forall a blk.
    Refinable a blk =>
    BlkInfo blk
    -> MM a blk -> (a -> MetaEnv (PB blk)) -> MetaEnv (PB blk)
    mmpcase BlkInfo blk
    blkinfo MM a blk
    x a -> MetaEnv (PB blk)
    f = case MM a blk
    x of
     NotM a
    x -> a -> MetaEnv (PB blk)
    f a
    x
     x :: MM a blk
    x@(Meta Metavar a blk
    m) -> do
      Maybe a
    bind <- IORef (Maybe a) -> IO (Maybe a)
    forall a. IORef a -> IO a
    readIORef (IORef (Maybe a) -> IO (Maybe a))
    -> IORef (Maybe a) -> IO (Maybe a)
    forall a b. (a -> b) -> a -> b
    $ Metavar a blk -> IORef (Maybe a)
    forall a blk. Metavar a blk -> IORef (Maybe a)
    mbind Metavar a blk
    m
      case Maybe a
    bind of
       Just a
    x -> a -> MetaEnv (PB blk)
    f a
    x
       Maybe a
    Nothing -> PB blk -> MetaEnv (PB blk)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (PB blk -> MetaEnv (PB blk)) -> PB blk -> MetaEnv (PB blk)
    forall a b. (a -> b) -> a -> b
    $ Metavar a blk -> BlkInfo blk -> MetaEnv (PB blk) -> PB blk
    forall blk b.
    Refinable b blk =>
    Metavar b blk -> BlkInfo blk -> MetaEnv (PB blk) -> PB blk
    PBlocked Metavar a blk
    m BlkInfo blk
    blkinfo (BlkInfo blk
    -> MM a blk -> (a -> MetaEnv (PB blk)) -> MetaEnv (PB blk)
    forall a blk.
    Refinable a blk =>
    BlkInfo blk
    -> MM a blk -> (a -> MetaEnv (PB blk)) -> MetaEnv (PB blk)
    mmpcase BlkInfo blk
    forall a. HasCallStack => a
    __IMPOSSIBLE__ MM a blk
    x a -> MetaEnv (PB blk)
    f) -- blkinfo not needed because will be notb next time

    doubleblock :: (Refinable a blk, Refinable b blk) => MM a blk -> MM b blk -> MetaEnv (PB blk) -> MetaEnv (PB blk)
    doubleblock :: forall a blk b.
    (Refinable a blk, Refinable b blk) =>
    MM a blk -> MM b blk -> MetaEnv (PB blk) -> MetaEnv (PB blk)
    doubleblock (Meta Metavar a blk
    m1) (Meta Metavar b blk
    m2) MetaEnv (PB blk)
    cont = PB blk -> MetaEnv (PB blk)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (PB blk -> MetaEnv (PB blk)) -> PB blk -> MetaEnv (PB blk)
    forall a b. (a -> b) -> a -> b
    $ Metavar a blk -> Metavar b blk -> MetaEnv (PB blk) -> PB blk
    forall blk b1 b2.
    (Refinable b1 blk, Refinable b2 blk) =>
    Metavar b1 blk -> Metavar b2 blk -> MetaEnv (PB blk) -> PB blk
    PDoubleBlocked Metavar a blk
    m1 Metavar b blk
    m2 MetaEnv (PB blk)
    cont
    doubleblock MM a blk
    _ MM b blk
    _ MetaEnv (PB blk)
    _ = MetaEnv (PB blk)
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    mbcase :: MetaEnv (MB a blk) -> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
    mbcase :: forall a blk b.
    MetaEnv (MB a blk)
    -> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
    mbcase MetaEnv (MB a blk)
    x a -> MetaEnv (MB b blk)
    f = do
     MB a blk
    x' <- MetaEnv (MB a blk)
    x
     case MB a blk
    x' of
      NotB a
    x -> a -> MetaEnv (MB b blk)
    f a
    x
      Blocked Metavar b blk
    m MetaEnv (MB a blk)
    x -> MB b blk -> MetaEnv (MB b blk)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (MB b blk -> MetaEnv (MB b blk)) -> MB b blk -> MetaEnv (MB b blk)
    forall a b. (a -> b) -> a -> b
    $ Metavar b blk -> MetaEnv (MB b blk) -> MB b blk
    forall a blk b.
    Refinable b blk =>
    Metavar b blk -> MetaEnv (MB a blk) -> MB a blk
    Blocked Metavar b blk
    m (MetaEnv (MB a blk)
    -> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
    forall a blk b.
    MetaEnv (MB a blk)
    -> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
    mbcase MetaEnv (MB a blk)
    x a -> MetaEnv (MB b blk)
    f)
      Failed String
    msg -> MB b blk -> MetaEnv (MB b blk)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (MB b blk -> MetaEnv (MB b blk)) -> MB b blk -> MetaEnv (MB b blk)
    forall a b. (a -> b) -> a -> b
    $ String -> MB b blk
    forall a blk. String -> MB a blk
    Failed String
    msg

    mbpcase :: Prio -> Maybe blk -> MetaEnv (MB a blk) -> (a -> MetaEnv (PB blk)) -> MetaEnv (PB blk)
    mbpcase :: forall blk a.
    Prio
    -> Maybe blk
    -> MetaEnv (MB a blk)
    -> (a -> MetaEnv (PB blk))
    -> MetaEnv (PB blk)
    mbpcase Prio
    prio Maybe blk
    bi MetaEnv (MB a blk)
    x a -> MetaEnv (PB blk)
    f = do
     MB a blk
    x' <- MetaEnv (MB a blk)
    x
     case MB a blk
    x' of
      NotB a
    x -> a -> MetaEnv (PB blk)
    f a
    x
      Blocked Metavar b blk
    m MetaEnv (MB a blk)
    x -> PB blk -> MetaEnv (PB blk)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (PB blk -> MetaEnv (PB blk)) -> PB blk -> MetaEnv (PB blk)
    forall a b. (a -> b) -> a -> b
    $ Metavar b blk -> BlkInfo blk -> MetaEnv (PB blk) -> PB blk
    forall blk b.
    Refinable b blk =>
    Metavar b blk -> BlkInfo blk -> MetaEnv (PB blk) -> PB blk
    PBlocked Metavar b blk
    m (Bool
    False, Prio
    prio, Maybe blk
    bi) (Prio
    -> Maybe blk
    -> MetaEnv (MB a blk)
    -> (a -> MetaEnv (PB blk))
    -> MetaEnv (PB blk)
    forall blk a.
    Prio
    -> Maybe blk
    -> MetaEnv (MB a blk)
    -> (a -> MetaEnv (PB blk))
    -> MetaEnv (PB blk)
    mbpcase Prio
    prio Maybe blk
    bi MetaEnv (MB a blk)
    x a -> MetaEnv (PB blk)
    f)
      Failed String
    msg -> PB blk -> MetaEnv (PB blk)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (PB blk -> MetaEnv (PB blk)) -> PB blk -> MetaEnv (PB blk)
    forall a b. (a -> b) -> a -> b
    $ Prop blk -> PB blk
    forall blk. Prop blk -> PB blk
    NotPB (Prop blk -> PB blk) -> Prop blk -> PB blk
    forall a b. (a -> b) -> a -> b
    $ String -> Prop blk
    forall blk. String -> Prop blk
    Error String
    msg

    mmbpcase :: MetaEnv (MB a blk) -> (forall b . Refinable b blk => MM b blk -> MetaEnv (PB blk)) -> (a -> MetaEnv (PB blk)) -> MetaEnv (PB blk)
    mmbpcase :: forall a blk.
    MetaEnv (MB a blk)
    -> (forall b. Refinable b blk => MM b blk -> MetaEnv (PB blk))
    -> (a -> MetaEnv (PB blk))
    -> MetaEnv (PB blk)
    mmbpcase MetaEnv (MB a blk)
    x forall b. Refinable b blk => MM b blk -> MetaEnv (PB blk)
    fm a -> MetaEnv (PB blk)
    f = do
     MB a blk
    x' <- MetaEnv (MB a blk)
    x
     case MB a blk
    x' of
      NotB a
    x -> a -> MetaEnv (PB blk)
    f a
    x
      Blocked Metavar b blk
    m MetaEnv (MB a blk)
    _ -> MM b blk -> MetaEnv (PB blk)
    forall b. Refinable b blk => MM b blk -> MetaEnv (PB blk)
    fm (Metavar b blk -> MM b blk
    forall a blk. Metavar a blk -> MM a blk
    Meta Metavar b blk
    m)
      Failed String
    msg -> PB blk -> MetaEnv (PB blk)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (PB blk -> MetaEnv (PB blk)) -> PB blk -> MetaEnv (PB blk)
    forall a b. (a -> b) -> a -> b
    $ Prop blk -> PB blk
    forall blk. Prop blk -> PB blk
    NotPB (Prop blk -> PB blk) -> Prop blk -> PB blk
    forall a b. (a -> b) -> a -> b
    $ String -> Prop blk
    forall blk. String -> Prop blk
    Error String
    msg

    waitok :: OKHandle blk -> MetaEnv (MB b blk) -> MetaEnv (MB b blk)
    waitok :: forall blk b.
    OKHandle blk -> MetaEnv (MB b blk) -> MetaEnv (MB b blk)
    waitok OKHandle blk
    okh MetaEnv (MB b blk)
    f =
     OKHandle blk -> (OKVal -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
    forall a blk b.
    Refinable a blk =>
    MM a blk -> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
    mmcase OKHandle blk
    okh ((OKVal -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk))
    -> (OKVal -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
    forall a b. (a -> b) -> a -> b
    $ \ OKVal
    OKVal -> MetaEnv (MB b blk)
    f -- principle constraint is never present for okhandle so it will not be refined

    mbret :: a -> MetaEnv (MB a blk)
    mbret :: forall a blk. a -> MetaEnv (MB a blk)
    mbret a
    x = MB a blk -> IO (MB a blk)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (MB a blk -> IO (MB a blk)) -> MB a blk -> IO (MB a blk)
    forall a b. (a -> b) -> a -> b
    $ a -> MB a blk
    forall a blk. a -> MB a blk
    NotB a
    x

    mbfailed :: String -> MetaEnv (MB a blk)
    mbfailed :: forall a blk. String -> MetaEnv (MB a blk)
    mbfailed String
    msg = MB a blk -> IO (MB a blk)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (MB a blk -> IO (MB a blk)) -> MB a blk -> IO (MB a blk)
    forall a b. (a -> b) -> a -> b
    $ String -> MB a blk
    forall a blk. String -> MB a blk
    Failed String
    msg

    mpret :: Prop blk -> MetaEnv (PB blk)
    mpret :: forall blk. Prop blk -> MetaEnv (PB blk)
    mpret Prop blk
    p = PB blk -> IO (PB blk)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (PB blk -> IO (PB blk)) -> PB blk -> IO (PB blk)
    forall a b. (a -> b) -> a -> b
    $ Prop blk -> PB blk
    forall blk. Prop blk -> PB blk
    NotPB Prop blk
    p

    expandbind :: MM a blk -> MetaEnv (MM a blk)
    expandbind :: forall a blk. MM a blk -> MetaEnv (MM a blk)
    expandbind MM a blk
    x = case MM a blk
    x of
     NotM{} -> MM a blk -> MetaEnv (MM a blk)
    forall (m :: * -> *) a. Monad m => a -> m a
    return MM a blk
    x
     Meta Metavar a blk
    m -> do
      Maybe a
    bind <- IORef (Maybe a) -> IO (Maybe a)
    forall a. IORef a -> IO a
    readIORef (IORef (Maybe a) -> IO (Maybe a))
    -> IORef (Maybe a) -> IO (Maybe a)
    forall a b. (a -> b) -> a -> b
    $ Metavar a blk -> IORef (Maybe a)
    forall a blk. Metavar a blk -> IORef (Maybe a)
    mbind Metavar a blk
    m
      case Maybe a
    bind of
       Just a
    x -> MM a blk -> MetaEnv (MM a blk)
    forall (m :: * -> *) a. Monad m => a -> m a
    return (MM a blk -> MetaEnv (MM a blk)) -> MM a blk -> MetaEnv (MM a blk)
    forall a b. (a -> b) -> a -> b
    $ a -> MM a blk
    forall a blk. a -> MM a blk
    NotM a
    x
       Maybe a
    Nothing -> MM a blk -> MetaEnv (MM a blk)
    forall (m :: * -> *) a. Monad m => a -> m a
    return MM a blk
    x

    -- -----------------------

    type HandleSol = IO ()

    type SRes = Either Bool Int

    topSearch :: forall blk . IORef Int -> IORef Int -> HandleSol -> blk -> MetaEnv (PB blk) -> Cost -> Cost -> IO Bool
    topSearch :: forall blk.
    IORef Int
    -> IORef Int
    -> IO ()
    -> blk
    -> MetaEnv (PB blk)
    -> Cost
    -> Cost
    -> IO Bool
    topSearch IORef Int
    ticks IORef Int
    nsol IO ()
    hsol blk
    envinfo MetaEnv (PB blk)
    p Cost
    searchdepth Cost
    depthinterval = do
     IORef Bool
    depthreached <- Bool -> IO (IORef Bool)
    forall a. a -> IO (IORef a)
    newIORef Bool
    False

     CTree blk
    mainroot <- Maybe (CTree blk) -> IO (CTree blk)
    forall blk. Maybe (CTree blk) -> IO (CTree blk)
    newCTree Maybe (CTree blk)
    forall a. Maybe a
    Nothing

     let
      searchSubProb :: [(CTree blk, Maybe (IORef Bool))] -> Cost -> IO SRes
      searchSubProb :: [(CTree blk, Maybe (IORef Bool))] -> Cost -> IO SRes
    searchSubProb [] Cost
    depth = do
       Bool -> IO () -> IO ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (Cost
    depth Cost -> Cost -> Bool
    forall a. Ord a => a -> a -> Bool
    < Cost
    depthinterval) (IO () -> IO ()) -> IO () -> IO ()
    forall a b. (a -> b) -> a -> b
    $ do

        IO ()
    hsol
        Int
    n <- IORef Int -> IO Int
    forall a. IORef a -> IO a
    readIORef IORef Int
    nsol
        IORef Int -> Int -> IO ()
    forall a. IORef a -> a -> IO ()
    NoUndo.writeIORef IORef Int
    nsol (Int -> IO ()) -> Int -> IO ()
    forall a b. (a -> b) -> a -> b
    $! Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1

       SRes -> IO SRes
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SRes -> IO SRes) -> SRes -> IO SRes
    forall a b. (a -> b) -> a -> b
    $ Bool -> SRes
    forall a b. a -> Either a b
    Left Bool
    True
      searchSubProb ((CTree blk
    root, Maybe (IORef Bool)
    firstdone) : [(CTree blk, Maybe (IORef Bool))]
    restprobs) Cost
    depth =
       let
        search :: Cost -> IO SRes
        search :: Cost -> IO SRes
    search Cost
    depth = do
         PrioMeta blk
    pm <- IORef (PrioMeta blk) -> IO (PrioMeta blk)
    forall a. IORef a -> IO a
    readIORef (IORef (PrioMeta blk) -> IO (PrioMeta blk))
    -> IORef (PrioMeta blk) -> IO (PrioMeta blk)
    forall a b. (a -> b) -> a -> b
    $ CTree blk -> IORef (PrioMeta blk)
    forall blk. CTree blk -> IORef (PrioMeta blk)
    ctpriometa CTree blk
    root
         case PrioMeta blk
    pm of
          NoPrio Bool
    False -> SRes -> IO SRes
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SRes -> IO SRes) -> SRes -> IO SRes
    forall a b. (a -> b) -> a -> b
    $ Bool -> SRes
    forall a b. a -> Either a b
    Left Bool
    False -- nothing to refine but not done, this can happen when eq constraints are passed along with main constraint in agdaplugin
          NoPrio Bool
    True ->
           [(CTree blk, Maybe (IORef Bool))] -> Cost -> IO SRes
    searchSubProb [(CTree blk, Maybe (IORef Bool))]
    restprobs Cost
    depth -- ?? what should depth be
          PrioMeta Prio
    _ Metavar a blk
    m -> do
           let carryon :: IO SRes
    carryon = Metavar a blk -> Cost -> IO SRes
    forall a. Refinable a blk => Metavar a blk -> Cost -> IO SRes
    fork Metavar a blk
    m Cost
    depth
           Maybe (SubConstraints blk)
    sub <- IORef (Maybe (SubConstraints blk))
    -> IO (Maybe (SubConstraints blk))
    forall a. IORef a -> IO a
    readIORef (IORef (Maybe (SubConstraints blk))
     -> IO (Maybe (SubConstraints blk)))
    -> IORef (Maybe (SubConstraints blk))
    -> IO (Maybe (SubConstraints blk))
    forall a b. (a -> b) -> a -> b
    $ CTree blk -> IORef (Maybe (SubConstraints blk))
    forall blk. CTree blk -> IORef (Maybe (SubConstraints blk))
    ctsub CTree blk
    root
           case Maybe (SubConstraints blk)
    sub of
            Maybe (SubConstraints blk)
    Nothing -> IO SRes
    carryon
            Just SubConstraints blk
    sc -> do
             let sub1 :: CTree blk
    sub1 = SubConstraints blk -> CTree blk
    forall blk. SubConstraints blk -> CTree blk
    scsub1 SubConstraints blk
    sc
                 sub2 :: CTree blk
    sub2 = SubConstraints blk -> CTree blk
    forall blk. SubConstraints blk -> CTree blk
    scsub2 SubConstraints blk
    sc
             PrioMeta blk
    pm1 <- IORef (PrioMeta blk) -> IO (PrioMeta blk)
    forall a. IORef a -> IO a
    readIORef (IORef (PrioMeta blk) -> IO (PrioMeta blk))
    -> IORef (PrioMeta blk) -> IO (PrioMeta blk)
    forall a b. (a -> b) -> a -> b
    $ CTree blk -> IORef (PrioMeta blk)
    forall blk. CTree blk -> IORef (PrioMeta blk)
    ctpriometa CTree blk
    sub1
             PrioMeta blk
    pm2 <- IORef (PrioMeta blk) -> IO (PrioMeta blk)
    forall a. IORef a -> IO a
    readIORef (IORef (PrioMeta blk) -> IO (PrioMeta blk))
    -> IORef (PrioMeta blk) -> IO (PrioMeta blk)
    forall a b. (a -> b) -> a -> b
    $ CTree blk -> IORef (PrioMeta blk)
    forall blk. CTree blk -> IORef (PrioMeta blk)
    ctpriometa CTree blk
    sub2
             let split :: IO SRes
    split = IO SRes
    carryon -- split disabled
             case PrioMeta blk
    pm1 of
              NoPrio Bool
    True -> IO SRes
    split
              PrioMeta blk
    _ ->
               case PrioMeta blk
    pm2 of
                NoPrio Bool
    True -> IO SRes
    split
                PrioMeta blk
    _ -> do
                 Int
    comc <- IORef Int -> IO Int
    forall a. IORef a -> IO a
    readIORef (IORef Int -> IO Int) -> IORef Int -> IO Int
    forall a b. (a -> b) -> a -> b
    $ SubConstraints blk -> IORef Int
    forall blk. SubConstraints blk -> IORef Int
    sccomcount SubConstraints blk
    sc
                 case Int
    comc of
                  Int
    0 -> IO SRes
    split
                  Int
    _ -> IO SRes
    carryon

        fork :: forall a. Refinable a blk => Metavar a blk -> Cost -> IO SRes
        fork :: forall a. Refinable a blk => Metavar a blk -> Cost -> IO SRes
    fork Metavar a blk
    m Cost
    depth = do
          [blk]
    blkinfos <- Metavar a blk -> IO [blk]
    forall a blk. Metavar a blk -> IO [blk]
    extractblkinfos Metavar a blk
    m
          [Move' blk a]
    refs <- blk -> [blk] -> Metavar a blk -> IO [Move' blk a]
    forall a blk.
    Refinable a blk =>
    blk -> [blk] -> Metavar a blk -> IO [Move' blk a]
    refinements blk
    envinfo [blk]
    blkinfos Metavar a blk
    m
          [Move' blk a] -> IO SRes
    f [Move' blk a]
    refs
         where
          f :: [Move' blk a] -> IO SRes
          f :: [Move' blk a] -> IO SRes
    f [] = do
           [Move' blk a]
    erefs <- IORef [Move' blk a] -> IO [Move' blk a]
    forall a. IORef a -> IO a
    readIORef (IORef [Move' blk a] -> IO [Move' blk a])
    -> IORef [Move' blk a] -> IO [Move' blk a]
    forall a b. (a -> b) -> a -> b
    $ Metavar a blk -> IORef [Move' blk a]
    forall a blk. Metavar a blk -> IORef [Move' blk a]
    mextrarefs Metavar a blk
    m
           case [Move' blk a]
    erefs of
            [] -> SRes -> IO SRes
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Bool -> SRes
    forall a b. a -> Either a b
    Left Bool
    False)
            [Move' blk a]
    _ -> do
             IORef [Move' blk a] -> [Move' blk a] -> IO ()
    forall a. IORef a -> a -> IO ()
    NoUndo.writeIORef (Metavar a blk -> IORef [Move' blk a]
    forall a blk. Metavar a blk -> IORef [Move' blk a]
    mextrarefs Metavar a blk
    m) []
             [Move' blk a] -> IO SRes
    f [Move' blk a]
    erefs
          f (Move Cost
    cost RefCreateEnv blk a
    bind : [Move' blk a]
    binds) = IO SRes -> IO SRes -> IO SRes
    hsres (Metavar a blk -> RefCreateEnv blk a -> Cost -> IO SRes
    forall a. Metavar a blk -> RefCreateEnv blk a -> Cost -> IO SRes
    refine Metavar a blk
    m RefCreateEnv blk a
    bind (Cost
    depth Cost -> Cost -> Cost
    forall a. Num a => a -> a -> a
    - Cost
    cost)) ([Move' blk a] -> IO SRes
    f [Move' blk a]
    binds)
        hsres :: IO SRes -> IO SRes -> IO SRes
        hsres :: IO SRes -> IO SRes -> IO SRes
    hsres IO SRes
    x1 IO SRes
    x2 = do
         SRes
    res <- IO SRes
    x1
         case SRes
    res of
          Right Int
    _ -> SRes -> IO SRes
    forall (m :: * -> *) a. Monad m => a -> m a
    return SRes
    res
          Left Bool
    found -> do
           Int
    n <- IORef Int -> IO Int
    forall a. IORef a -> IO a
    readIORef IORef Int
    nsol
           if Int
    n Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    0 then
             SRes -> IO SRes
    forall (m :: * -> *) a. Monad m => a -> m a
    return SRes
    res
            else do
             SRes
    res2 <- IO SRes
    x2
             case SRes
    res2 of
              Right Int
    _ -> if Bool
    found then IO SRes
    forall a. HasCallStack => a
    __IMPOSSIBLE__ else SRes -> IO SRes
    forall (m :: * -> *) a. Monad m => a -> m a
    return SRes
    res2
              Left Bool
    found2 -> SRes -> IO SRes
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SRes -> IO SRes) -> SRes -> IO SRes
    forall a b. (a -> b) -> a -> b
    $ Bool -> SRes
    forall a b. a -> Either a b
    Left (Bool
    found Bool -> Bool -> Bool
    || Bool
    found2)

        refine :: Metavar a blk -> RefCreateEnv blk a -> Cost -> IO SRes

        refine :: forall a. Metavar a blk -> RefCreateEnv blk a -> Cost -> IO SRes
    refine Metavar a blk
    _ RefCreateEnv blk a
    _ Cost
    depthleft | Cost
    depthleft Cost -> Cost -> Bool
    forall a. Ord a => a -> a -> Bool
    < Cost
    0 = do
         IORef Bool -> Bool -> IO ()
    forall a. IORef a -> a -> IO ()
    NoUndo.writeIORef IORef Bool
    depthreached Bool
    True
         SRes -> IO SRes
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SRes -> IO SRes) -> SRes -> IO SRes
    forall a b. (a -> b) -> a -> b
    $ Bool -> SRes
    forall a b. a -> Either a b
    Left Bool
    False

        refine Metavar a blk
    m RefCreateEnv blk a
    bind Cost
    depthleft = Undo SRes -> IO SRes
    forall a. Undo a -> IO a
    runUndo (Undo SRes -> IO SRes) -> Undo SRes -> IO SRes
    forall a b. (a -> b) -> a -> b
    $
         do Int
    t <- IORef Int -> Undo Int
    forall a. IORef a -> Undo a
    ureadIORef IORef Int
    ticks
            IO () -> Undo ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (IO () -> Undo ()) -> IO () -> Undo ()
    forall a b. (a -> b) -> a -> b
    $ IORef Int -> Int -> IO ()
    forall a. IORef a -> a -> IO ()
    NoUndo.writeIORef IORef Int
    ticks (Int -> IO ()) -> Int -> IO ()
    forall a b. (a -> b) -> a -> b
    $! Int
    t Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1

            (a
    bind, (IORef [SubConstraints blk]
    _, Int
    nnewmeta)) <- IO (a, (IORef [SubConstraints blk], Int))
    -> StateT [Restore] IO (a, (IORef [SubConstraints blk], Int))
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (IO (a, (IORef [SubConstraints blk], Int))
     -> StateT [Restore] IO (a, (IORef [SubConstraints blk], Int)))
    -> IO (a, (IORef [SubConstraints blk], Int))
    -> StateT [Restore] IO (a, (IORef [SubConstraints blk], Int))
    forall a b. (a -> b) -> a -> b
    $ StateT (IORef [SubConstraints blk], Int) IO a
    -> (IORef [SubConstraints blk], Int)
    -> IO (a, (IORef [SubConstraints blk], Int))
    forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
    runStateT (RefCreateEnv blk a -> StateT (IORef [SubConstraints blk], Int) IO a
    forall blk a.
    RefCreateEnv blk a -> StateT (IORef [SubConstraints blk], Int) IO a
    runRefCreateEnv RefCreateEnv blk a
    bind) (Metavar a blk -> IORef [SubConstraints blk]
    forall a blk. Metavar a blk -> IORef [SubConstraints blk]
    mcompoint Metavar a blk
    m, Int
    0)
            IORef (Maybe a) -> Maybe a -> Undo ()
    forall a. IORef a -> a -> Undo ()
    uwriteIORef (Metavar a blk -> IORef (Maybe a)
    forall a blk. Metavar a blk -> IORef (Maybe a)
    mbind Metavar a blk
    m) (a -> Maybe a
    forall a. a -> Maybe a
    Just a
    bind)
            [SubConstraints blk]
    mcomptr <- IORef [SubConstraints blk] -> Undo [SubConstraints blk]
    forall a. IORef a -> Undo a
    ureadIORef (IORef [SubConstraints blk] -> Undo [SubConstraints blk])
    -> IORef [SubConstraints blk] -> Undo [SubConstraints blk]
    forall a b. (a -> b) -> a -> b
    $ Metavar a blk -> IORef [SubConstraints blk]
    forall a blk. Metavar a blk -> IORef [SubConstraints blk]
    mcompoint Metavar a blk
    m
            (SubConstraints blk -> Undo ()) -> [SubConstraints blk] -> Undo ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (\SubConstraints blk
    comptr ->
              IORef Int -> (Int -> Int) -> Undo ()
    forall a. IORef a -> (a -> a) -> Undo ()
    umodifyIORef (SubConstraints blk -> IORef Int
    forall blk. SubConstraints blk -> IORef Int
    sccomcount SubConstraints blk
    comptr) (Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + (Int
    nnewmeta Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1))
              -- umodifyIORef (scflip comptr) not -- don't flip now since trying prefer rightmost subterm if non have prio
             ) [SubConstraints blk]
    mcomptr
            [(QPB a blk, Maybe (CTree blk))]
    obs <- IORef [(QPB a blk, Maybe (CTree blk))]
    -> Undo [(QPB a blk, Maybe (CTree blk))]
    forall a. IORef a -> Undo a
    ureadIORef (Metavar a blk -> IORef [(QPB a blk, Maybe (CTree blk))]
    forall a blk.
    Metavar a blk -> IORef [(QPB a blk, Maybe (CTree blk))]
    mobs Metavar a blk
    m)
            Bool
    res <- [(QPB a blk, Maybe (CTree blk))] -> Undo Bool
    forall a blk. [(QPB a blk, Maybe (CTree blk))] -> Undo Bool
    recalcs [(QPB a blk, Maybe (CTree blk))]
    obs
            if Bool
    res
              then
                SRes -> Undo SRes
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SRes -> Undo SRes) -> SRes -> Undo SRes
    forall a b. (a -> b) -> a -> b
    $ Bool -> SRes
    forall a b. a -> Either a b
    Left Bool
    False     -- failed
              else
                IO SRes -> Undo SRes
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (IO SRes -> Undo SRes) -> IO SRes -> Undo SRes
    forall a b. (a -> b) -> a -> b
    $ Cost -> IO SRes
    search Cost
    depthleft -- succeeded

        doit :: IO SRes
    doit = do
         SRes
    res <- Cost -> IO SRes
    search Cost
    depth
         SRes -> IO SRes
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SRes -> IO SRes) -> SRes -> IO SRes
    forall a b. (a -> b) -> a -> b
    $ case SRes
    res of
          Right Int
    n ->
           case Maybe (IORef Bool)
    firstdone of
            Maybe (IORef Bool)
    Nothing ->
             if Int
    n Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == Int
    0 then
              Bool -> SRes
    forall a b. a -> Either a b
    Left Bool
    False
             else
              Int -> SRes
    forall a b. b -> Either a b
    Right (Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    - Int
    1)
            Just IORef Bool
    _ ->
             Int -> SRes
    forall a b. b -> Either a b
    Right (Int
    n Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1)
          res :: SRes
    res@(Left Bool
    True) -> SRes
    res
          res :: SRes
    res@(Left Bool
    False) ->
           case Maybe (IORef Bool)
    firstdone of
            Maybe (IORef Bool)
    Nothing -> SRes
    res
            Just IORef Bool
    _ -> Int -> SRes
    forall a b. b -> Either a b
    Right Int
    0
       in
        case Maybe (IORef Bool)
    firstdone of
         Maybe (IORef Bool)
    Nothing -> IO SRes
    doit
         Just IORef Bool
    rdone -> do
          Bool
    done <- IORef Bool -> IO Bool
    forall a. IORef a -> IO a
    readIORef IORef Bool
    rdone
          if Bool
    done then
            [(CTree blk, Maybe (IORef Bool))] -> Cost -> IO SRes
    searchSubProb [(CTree blk, Maybe (IORef Bool))]
    restprobs Cost
    depth
           else do
            IORef Bool -> Bool -> IO ()
    forall a. IORef a -> a -> IO ()
    NoUndo.writeIORef IORef Bool
    rdone Bool
    True
            IO SRes
    doit

     Undo Bool -> IO Bool
    forall a. Undo a -> IO a
    runUndo (Undo Bool -> IO Bool) -> Undo Bool -> IO Bool
    forall a b. (a -> b) -> a -> b
    $ do
      Bool
    res <- MetaEnv (PB blk) -> Maybe (CTree blk) -> Undo Bool
    forall blk. MetaEnv (PB blk) -> Maybe (CTree blk) -> Undo Bool
    reccalc MetaEnv (PB blk)
    p (CTree blk -> Maybe (CTree blk)
    forall a. a -> Maybe a
    Just CTree blk
    mainroot)
      if Bool
    res -- failed immediately
        then
            Bool -> Undo Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
        else
          do
            Left Bool
    _solFound <- IO SRes -> Undo SRes
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (IO SRes -> Undo SRes) -> IO SRes -> Undo SRes
    forall a b. (a -> b) -> a -> b
    $ [(CTree blk, Maybe (IORef Bool))] -> Cost -> IO SRes
    searchSubProb [(CTree blk
    mainroot, Maybe (IORef Bool)
    forall a. Maybe a
    Nothing)] Cost
    searchdepth
            IO Bool -> Undo Bool
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (IO Bool -> Undo Bool) -> IO Bool -> Undo Bool
    forall a b. (a -> b) -> a -> b
    $ IORef Bool -> IO Bool
    forall a. IORef a -> IO a
    readIORef IORef Bool
    depthreached

    extractblkinfos :: Metavar a blk -> IO [blk]
    extractblkinfos :: forall a blk. Metavar a blk -> IO [blk]
    extractblkinfos Metavar a blk
    m = do
     [(QPB a blk, Maybe (CTree blk))]
    obs <- IORef [(QPB a blk, Maybe (CTree blk))]
    -> IO [(QPB a blk, Maybe (CTree blk))]
    forall a. IORef a -> IO a
    readIORef (IORef [(QPB a blk, Maybe (CTree blk))]
     -> IO [(QPB a blk, Maybe (CTree blk))])
    -> IORef [(QPB a blk, Maybe (CTree blk))]
    -> IO [(QPB a blk, Maybe (CTree blk))]
    forall a b. (a -> b) -> a -> b
    $ Metavar a blk -> IORef [(QPB a blk, Maybe (CTree blk))]
    forall a blk.
    Metavar a blk -> IORef [(QPB a blk, Maybe (CTree blk))]
    mobs Metavar a blk
    m
     [blk] -> IO [blk]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([blk] -> IO [blk]) -> [blk] -> IO [blk]
    forall a b. (a -> b) -> a -> b
    $ [(QPB a blk, Maybe (CTree blk))] -> [blk]
    forall {b} {a} {b}. [(QPB b a, b)] -> [a]
    f [(QPB a blk, Maybe (CTree blk))]
    obs
     where
      f :: [(QPB b a, b)] -> [a]
    f [] = []
      f ((QPBlocked (Bool
    _,Prio
    _,Maybe a
    mblkinfo) MetaEnv (PB a)
    _, b
    _) : [(QPB b a, b)]
    cs) =
       case Maybe a
    mblkinfo of
        Maybe a
    Nothing -> [(QPB b a, b)] -> [a]
    f [(QPB b a, b)]
    cs
        Just a
    blkinfo -> a
    blkinfo a -> [a] -> [a]
    forall a. a -> [a] -> [a]
    : [(QPB b a, b)] -> [a]
    f [(QPB b a, b)]
    cs
      f ((QPDoubleBlocked{}, b
    _) : [(QPB b a, b)]
    cs) = [(QPB b a, b)] -> [a]
    f [(QPB b a, b)]
    cs

    recalcs :: [(QPB a blk, Maybe (CTree blk))] -> Undo Bool
    recalcs :: forall a blk. [(QPB a blk, Maybe (CTree blk))] -> Undo Bool
    recalcs [(QPB a blk, Maybe (CTree blk))]
    cs = ((QPB a blk, Maybe (CTree blk)) -> Undo Bool -> Undo Bool)
    -> Undo Bool -> [(QPB a blk, Maybe (CTree blk))] -> Undo Bool
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr (Undo Bool -> Undo Bool -> Undo Bool
    seqc (Undo Bool -> Undo Bool -> Undo Bool)
    -> ((QPB a blk, Maybe (CTree blk)) -> Undo Bool)
    -> (QPB a blk, Maybe (CTree blk))
    -> Undo Bool
    -> Undo Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (QPB a blk, Maybe (CTree blk)) -> Undo Bool
    forall a blk. (QPB a blk, Maybe (CTree blk)) -> Undo Bool
    recalc) (Bool -> Undo Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False) [(QPB a blk, Maybe (CTree blk))]
    cs

    seqc :: Undo Bool -> Undo Bool -> Undo Bool
    seqc :: Undo Bool -> Undo Bool -> Undo Bool
    seqc Undo Bool
    x Undo Bool
    y = do
     Bool
    res1 <- Undo Bool
    x
     case Bool
    res1 of
      res1 :: Bool
    res1@Bool
    True -> Bool -> Undo Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    res1
      Bool
    False -> Undo Bool
    y

    recalc :: (QPB a blk, Maybe (CTree blk)) -> Undo Bool
    recalc :: forall a blk. (QPB a blk, Maybe (CTree blk)) -> Undo Bool
    recalc (QPB a blk
    con, Maybe (CTree blk)
    node) = case QPB a blk
    con of
      QPBlocked       BlkInfo blk
    _    MetaEnv (PB blk)
    cont -> MetaEnv (PB blk) -> Maybe (CTree blk) -> Undo Bool
    forall blk. MetaEnv (PB blk) -> Maybe (CTree blk) -> Undo Bool
    reccalc MetaEnv (PB blk)
    cont Maybe (CTree blk)
    node
      QPDoubleBlocked IORef Bool
    flag MetaEnv (PB blk)
    cont -> do
        Bool
    fl <- IORef Bool -> Undo Bool
    forall a. IORef a -> Undo a
    ureadIORef IORef Bool
    flag
        if Bool
    fl
          then Bool -> Undo Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    False
          else do
            IORef Bool -> Bool -> Undo ()
    forall a. IORef a -> a -> Undo ()
    uwriteIORef IORef Bool
    flag Bool
    True
            MetaEnv (PB blk) -> Maybe (CTree blk) -> Undo Bool
    forall blk. MetaEnv (PB blk) -> Maybe (CTree blk) -> Undo Bool
    reccalc MetaEnv (PB blk)
    cont Maybe (CTree blk)
    node

    reccalc :: MetaEnv (PB blk) -> Maybe (CTree blk) -> Undo Bool
    reccalc :: forall blk. MetaEnv (PB blk) -> Maybe (CTree blk) -> Undo Bool
    reccalc MetaEnv (PB blk)
    cont Maybe (CTree blk)
    node = do
      Maybe [OKMeta blk]
    res <- MetaEnv (PB blk) -> Maybe (CTree blk) -> Undo (Maybe [OKMeta blk])
    forall blk.
    MetaEnv (PB blk) -> Maybe (CTree blk) -> Undo (Maybe [OKMeta blk])
    calc MetaEnv (PB blk)
    cont Maybe (CTree blk)
    node
      case Maybe [OKMeta blk]
    res of
        Maybe [OKMeta blk]
    Nothing -> Bool -> Undo Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    True
        Just [OKMeta blk]
    pendhandles ->
          (Bool -> OKMeta blk -> Undo Bool)
    -> Bool -> [OKMeta blk] -> Undo Bool
    forall (t :: * -> *) (m :: * -> *) b a.
    (Foldable t, Monad m) =>
    (b -> a -> m b) -> b -> t a -> m b
    foldM
            ( \Bool
    res1 OKMeta blk
    h ->
                if Bool
    res1
                  then Bool -> Undo Bool
    forall (m :: * -> *) a. Monad m => a -> m a
    return Bool
    res1
                  else do
                    IORef (Maybe OKVal) -> Maybe OKVal -> Undo ()
    forall a. IORef a -> a -> Undo ()
    uwriteIORef (OKMeta blk -> IORef (Maybe OKVal)
    forall a blk. Metavar a blk -> IORef (Maybe a)
    mbind OKMeta blk
    h) (Maybe OKVal -> Undo ()) -> Maybe OKVal -> Undo ()
    forall a b. (a -> b) -> a -> b
    $ OKVal -> Maybe OKVal
    forall a. a -> Maybe a
    Just OKVal
    OKVal
                    [(QPB OKVal blk, Maybe (CTree blk))]
    obs <- IORef [(QPB OKVal blk, Maybe (CTree blk))]
    -> Undo [(QPB OKVal blk, Maybe (CTree blk))]
    forall a. IORef a -> Undo a
    ureadIORef (OKMeta blk -> IORef [(QPB OKVal blk, Maybe (CTree blk))]
    forall a blk.
    Metavar a blk -> IORef [(QPB a blk, Maybe (CTree blk))]
    mobs OKMeta blk
    h)
                    [(QPB OKVal blk, Maybe (CTree blk))] -> Undo Bool
    forall a blk. [(QPB a blk, Maybe (CTree blk))] -> Undo Bool
    recalcs [(QPB OKVal blk, Maybe (CTree blk))]
    obs
            )
            Bool
    False
            [OKMeta blk]
    pendhandles

    calc :: forall blk . MetaEnv (PB blk) -> Maybe (CTree blk) -> Undo (Maybe [OKMeta blk])
    calc :: forall blk.
    MetaEnv (PB blk) -> Maybe (CTree blk) -> Undo (Maybe [OKMeta blk])
    calc MetaEnv (PB blk)
    cont Maybe (CTree blk)
    node = do
      Maybe (PrioMeta blk, [OKMeta blk])
    res <- Maybe (CTree blk)
    -> MetaEnv (PB blk)
    -> StateT [Restore] IO (Maybe (PrioMeta blk, [OKMeta blk]))
    donewp Maybe (CTree blk)
    node MetaEnv (PB blk)
    cont
      case Maybe (PrioMeta blk, [OKMeta blk])
    res of
       Just (PrioMeta blk
    _, [OKMeta blk]
    pendhandles) -> do
        [OKMeta blk]
    pendhandles2 <- case Maybe (CTree blk)
    node of
         Just CTree blk
    node -> CTree blk -> StateT [Restore] IO [OKMeta blk]
    forall blk. CTree blk -> Undo [OKMeta blk]
    propagatePrio CTree blk
    node
         Maybe (CTree blk)
    Nothing -> [OKMeta blk] -> StateT [Restore] IO [OKMeta blk]
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
        Maybe [OKMeta blk] -> Undo (Maybe [OKMeta blk])
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe [OKMeta blk] -> Undo (Maybe [OKMeta blk]))
    -> Maybe [OKMeta blk] -> Undo (Maybe [OKMeta blk])
    forall a b. (a -> b) -> a -> b
    $ [OKMeta blk] -> Maybe [OKMeta blk]
    forall a. a -> Maybe a
    Just ([OKMeta blk]
    pendhandles [OKMeta blk] -> [OKMeta blk] -> [OKMeta blk]
    forall a. [a] -> [a] -> [a]
    ++ [OKMeta blk]
    pendhandles2)
       Maybe (PrioMeta blk, [OKMeta blk])
    Nothing -> Maybe [OKMeta blk] -> Undo (Maybe [OKMeta blk])
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe [OKMeta blk]
    forall a. Maybe a
    Nothing
     where
      storeprio :: Maybe (CTree blk)
    -> PrioMeta blk
    -> [OKMeta blk]
    -> StateT [Restore] IO (Maybe (PrioMeta blk, [OKMeta blk]))
    storeprio (Just CTree blk
    node) PrioMeta blk
    pm [OKMeta blk]
    pendhandles = do
       [OKMeta blk]
    pendhandles' <- case PrioMeta blk
    pm of
        NoPrio Bool
    True -> do
         [OKMeta blk]
    handles <- IORef [OKMeta blk] -> StateT [Restore] IO [OKMeta blk]
    forall a. IORef a -> Undo a
    ureadIORef (CTree blk -> IORef [OKMeta blk]
    forall blk. CTree blk -> IORef [OKMeta blk]
    cthandles CTree blk
    node)
         [OKMeta blk] -> StateT [Restore] IO [OKMeta blk]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([OKMeta blk] -> StateT [Restore] IO [OKMeta blk])
    -> [OKMeta blk] -> StateT [Restore] IO [OKMeta blk]
    forall a b. (a -> b) -> a -> b
    $ [OKMeta blk]
    handles [OKMeta blk] -> [OKMeta blk] -> [OKMeta blk]
    forall a. [a] -> [a] -> [a]
    ++ [OKMeta blk]
    pendhandles
        PrioMeta blk
    _ -> [OKMeta blk] -> StateT [Restore] IO [OKMeta blk]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [OKMeta blk]
    pendhandles
       IORef (PrioMeta blk) -> PrioMeta blk -> Undo ()
    forall a. IORef a -> a -> Undo ()
    uwriteIORef (CTree blk -> IORef (PrioMeta blk)
    forall blk. CTree blk -> IORef (PrioMeta blk)
    ctpriometa CTree blk
    node) PrioMeta blk
    pm
       Maybe (PrioMeta blk, [OKMeta blk])
    -> StateT [Restore] IO (Maybe (PrioMeta blk, [OKMeta blk]))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe (PrioMeta blk, [OKMeta blk])
     -> StateT [Restore] IO (Maybe (PrioMeta blk, [OKMeta blk])))
    -> Maybe (PrioMeta blk, [OKMeta blk])
    -> StateT [Restore] IO (Maybe (PrioMeta blk, [OKMeta blk]))
    forall a b. (a -> b) -> a -> b
    $ (PrioMeta blk, [OKMeta blk]) -> Maybe (PrioMeta blk, [OKMeta blk])
    forall a. a -> Maybe a
    Just (PrioMeta blk
    pm, [OKMeta blk]
    pendhandles')
      storeprio Maybe (CTree blk)
    Nothing PrioMeta blk
    _ [OKMeta blk]
    _ =
       Maybe (PrioMeta blk, [OKMeta blk])
    -> StateT [Restore] IO (Maybe (PrioMeta blk, [OKMeta blk]))
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe (PrioMeta blk, [OKMeta blk])
     -> StateT [Restore] IO (Maybe (PrioMeta blk, [OKMeta blk])))
    -> Maybe (PrioMeta blk, [OKMeta blk])
    -> StateT [Restore] IO (Maybe (PrioMeta blk, [OKMeta blk]))
    forall a b. (a -> b) -> a -> b
    $ (PrioMeta blk, [OKMeta blk]) -> Maybe (PrioMeta blk, [OKMeta blk])
    forall a. a -> Maybe a
    Just (Bool -> PrioMeta blk
    forall blk. Bool -> PrioMeta blk
    NoPrio Bool
    False, [])
      donewp :: Maybe (CTree blk)
    -> MetaEnv (PB blk)
    -> StateT [Restore] IO (Maybe (PrioMeta blk, [OKMeta blk]))
    donewp Maybe (CTree blk)
    node MetaEnv (PB blk)
    p = do
       PB blk
    bp <- MetaEnv (PB blk) -> StateT [Restore] IO (PB blk)
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift MetaEnv (PB blk)
    p
       case PB blk
    bp of
        NotPB Prop blk
    p ->
         Maybe (CTree blk)
    -> Prop blk
    -> StateT [Restore] IO (Maybe (PrioMeta blk, [OKMeta blk]))
    doprop Maybe (CTree blk)
    node Prop blk
    p
        PBlocked Metavar b blk
    m BlkInfo blk
    blkinfo MetaEnv (PB blk)
    cont -> do
         [(QPB b blk, Maybe (CTree blk))]
    oldobs <- IORef [(QPB b blk, Maybe (CTree blk))]
    -> ([(QPB b blk, Maybe (CTree blk))]
        -> [(QPB b blk, Maybe (CTree blk))])
    -> Undo [(QPB b blk, Maybe (CTree blk))]
    forall a. IORef a -> (a -> a) -> Undo a
    ureadmodifyIORef (Metavar b blk -> IORef [(QPB b blk, Maybe (CTree blk))]
    forall a blk.
    Metavar a blk -> IORef [(QPB a blk, Maybe (CTree blk))]
    mobs Metavar b blk
    m) ((BlkInfo blk -> MetaEnv (PB blk) -> QPB b blk
    forall b blk. BlkInfo blk -> MetaEnv (PB blk) -> QPB b blk
    QPBlocked BlkInfo blk
    blkinfo MetaEnv (PB blk)
    cont, Maybe (CTree blk)
    node) (QPB b blk, Maybe (CTree blk))
    -> [(QPB b blk, Maybe (CTree blk))]
    -> [(QPB b blk, Maybe (CTree blk))]
    forall a. a -> [a] -> [a]
    :)
         let (Bool
    princ, Prio
    prio, Maybe blk
    _) = BlkInfo blk
    blkinfo
         Bool
    pp <- IORef Bool -> Undo Bool
    forall a. IORef a -> Undo a
    ureadIORef (Metavar b blk -> IORef Bool
    forall a blk. Metavar a blk -> IORef Bool
    mprincipalpresent Metavar b blk
    m)
         Bool -> Undo () -> Undo ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (Bool
    princ Bool -> Bool -> Bool
    && Bool -> Bool
    not Bool
    pp) (Undo () -> Undo ()) -> Undo () -> Undo ()
    forall a b. (a -> b) -> a -> b
    $ do
          IORef Bool -> Bool -> Undo ()
    forall a. IORef a -> a -> Undo ()
    uwriteIORef (Metavar b blk -> IORef Bool
    forall a blk. Metavar a blk -> IORef Bool
    mprincipalpresent Metavar b blk
    m) Bool
    True
          ((QPB b blk, Maybe (CTree blk))
     -> StateT [Restore] IO [OKMeta blk])
    -> [(QPB b blk, Maybe (CTree blk))] -> Undo ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (\(QPB b blk
    qpb, Maybe (CTree blk)
    node) -> case Maybe (CTree blk)
    node of
             Just CTree blk
    node ->
              case QPB b blk
    qpb of
               QPBlocked (Bool
    _, Prio
    prio, Maybe blk
    _) MetaEnv (PB blk)
    _ -> do

                IORef (PrioMeta blk) -> PrioMeta blk -> Undo ()
    forall a. IORef a -> a -> Undo ()
    uwriteIORef (CTree blk -> IORef (PrioMeta blk)
    forall blk. CTree blk -> IORef (PrioMeta blk)
    ctpriometa CTree blk
    node) (Prio -> Metavar b blk -> PrioMeta blk
    forall blk a.
    Refinable a blk =>
    Prio -> Metavar a blk -> PrioMeta blk
    PrioMeta Prio
    prio Metavar b blk
    m)
                CTree blk -> StateT [Restore] IO [OKMeta blk]
    forall blk. CTree blk -> Undo [OKMeta blk]
    propagatePrio CTree blk
    node
               QPDoubleBlocked IORef Bool
    _flag MetaEnv (PB blk)
    _ ->
                [OKMeta blk] -> StateT [Restore] IO [OKMeta blk]
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
             Maybe (CTree blk)
    Nothing -> [OKMeta blk] -> StateT [Restore] IO [OKMeta blk]
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
           ) [(QPB b blk, Maybe (CTree blk))]
    oldobs
         if Bool
    pp Bool -> Bool -> Bool
    || Bool
    princ then
           Maybe (CTree blk)
    -> PrioMeta blk
    -> [OKMeta blk]
    -> StateT [Restore] IO (Maybe (PrioMeta blk, [OKMeta blk]))
    forall {blk}.
    Maybe (CTree blk)
    -> PrioMeta blk
    -> [OKMeta blk]
    -> StateT [Restore] IO (Maybe (PrioMeta blk, [OKMeta blk]))
    storeprio Maybe (CTree blk)
    node (Prio -> Metavar b blk -> PrioMeta blk
    forall blk a.
    Refinable a blk =>
    Prio -> Metavar a blk -> PrioMeta blk
    PrioMeta Prio
    prio Metavar b blk
    m) []
          else
           Maybe (CTree blk)
    -> PrioMeta blk
    -> [OKMeta blk]
    -> StateT [Restore] IO (Maybe (PrioMeta blk, [OKMeta blk]))
    forall {blk}.
    Maybe (CTree blk)
    -> PrioMeta blk
    -> [OKMeta blk]
    -> StateT [Restore] IO (Maybe (PrioMeta blk, [OKMeta blk]))
    storeprio Maybe (CTree blk)
    node (Bool -> PrioMeta blk
    forall blk. Bool -> PrioMeta blk
    NoPrio Bool
    False) []
        PDoubleBlocked Metavar b1 blk
    m1 Metavar b2 blk
    m2 MetaEnv (PB blk)
    cont -> do
         IORef Bool
    flag <- IO (IORef Bool) -> StateT [Restore] IO (IORef Bool)
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (IO (IORef Bool) -> StateT [Restore] IO (IORef Bool))
    -> IO (IORef Bool) -> StateT [Restore] IO (IORef Bool)
    forall a b. (a -> b) -> a -> b
    $ Bool -> IO (IORef Bool)
    forall a. a -> IO (IORef a)
    newIORef Bool
    False

         let newobs :: forall b. [(QPB b blk, Maybe (CTree blk))]
                              -> [(QPB b blk, Maybe (CTree blk))]
             newobs :: forall b.
    [(QPB b blk, Maybe (CTree blk))]
    -> [(QPB b blk, Maybe (CTree blk))]
    newobs = ((IORef Bool -> MetaEnv (PB blk) -> QPB b blk
    forall b blk. IORef Bool -> MetaEnv (PB blk) -> QPB b blk
    QPDoubleBlocked IORef Bool
    flag MetaEnv (PB blk)
    cont, Maybe (CTree blk)
    node) (QPB b blk, Maybe (CTree blk))
    -> [(QPB b blk, Maybe (CTree blk))]
    -> [(QPB b blk, Maybe (CTree blk))]
    forall a. a -> [a] -> [a]
    :)
         IORef [(QPB b1 blk, Maybe (CTree blk))]
    -> ([(QPB b1 blk, Maybe (CTree blk))]
        -> [(QPB b1 blk, Maybe (CTree blk))])
    -> Undo ()
    forall a. IORef a -> (a -> a) -> Undo ()
    umodifyIORef (Metavar b1 blk -> IORef [(QPB b1 blk, Maybe (CTree blk))]
    forall a blk.
    Metavar a blk -> IORef [(QPB a blk, Maybe (CTree blk))]
    mobs Metavar b1 blk
    m1) [(QPB b1 blk, Maybe (CTree blk))]
    -> [(QPB b1 blk, Maybe (CTree blk))]
    forall b.
    [(QPB b blk, Maybe (CTree blk))]
    -> [(QPB b blk, Maybe (CTree blk))]
    newobs
         IORef [(QPB b2 blk, Maybe (CTree blk))]
    -> ([(QPB b2 blk, Maybe (CTree blk))]
        -> [(QPB b2 blk, Maybe (CTree blk))])
    -> Undo ()
    forall a. IORef a -> (a -> a) -> Undo ()
    umodifyIORef (Metavar b2 blk -> IORef [(QPB b2 blk, Maybe (CTree blk))]
    forall a blk.
    Metavar a blk -> IORef [(QPB a blk, Maybe (CTree blk))]
    mobs Metavar b2 blk
    m2) [(QPB b2 blk, Maybe (CTree blk))]
    -> [(QPB b2 blk, Maybe (CTree blk))]
    forall b.
    [(QPB b blk, Maybe (CTree blk))]
    -> [(QPB b blk, Maybe (CTree blk))]
    newobs
         Maybe (CTree blk)
    -> PrioMeta blk
    -> [OKMeta blk]
    -> StateT [Restore] IO (Maybe (PrioMeta blk, [OKMeta blk]))
    forall {blk}.
    Maybe (CTree blk)
    -> PrioMeta blk
    -> [OKMeta blk]
    -> StateT [Restore] IO (Maybe (PrioMeta blk, [OKMeta blk]))
    storeprio Maybe (CTree blk)
    node (Bool -> PrioMeta blk
    forall blk. Bool -> PrioMeta blk
    NoPrio Bool
    False) []
      doprop :: Maybe (CTree blk)
    -> Prop blk
    -> StateT [Restore] IO (Maybe (PrioMeta blk, [OKMeta blk]))
    doprop Maybe (CTree blk)
    node Prop blk
    p =
       case Prop blk
    p of
        Prop blk
    OK -> Maybe (CTree blk)
    -> PrioMeta blk
    -> [OKMeta blk]
    -> StateT [Restore] IO (Maybe (PrioMeta blk, [OKMeta blk]))
    forall {blk}.
    Maybe (CTree blk)
    -> PrioMeta blk
    -> [OKMeta blk]
    -> StateT [Restore] IO (Maybe (PrioMeta blk, [OKMeta blk]))
    storeprio Maybe (CTree blk)
    node (Bool -> PrioMeta blk
    forall blk. Bool -> PrioMeta blk
    NoPrio Bool
    True) []
        Error String
    _ -> Maybe (PrioMeta blk, [OKMeta blk])
    -> StateT [Restore] IO (Maybe (PrioMeta blk, [OKMeta blk]))
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (PrioMeta blk, [OKMeta blk])
    forall a. Maybe a
    Nothing

        AddExtraRef String
    _ Metavar a blk
    m Move' blk a
    eref -> do
         IO () -> Undo ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (IO () -> Undo ()) -> IO () -> Undo ()
    forall a b. (a -> b) -> a -> b
    $ IORef [Move' blk a] -> ([Move' blk a] -> [Move' blk a]) -> IO ()
    forall a. IORef a -> (a -> a) -> IO ()
    NoUndo.modifyIORef (Metavar a blk -> IORef [Move' blk a]
    forall a blk. Metavar a blk -> IORef [Move' blk a]
    mextrarefs Metavar a blk
    m) (Move' blk a
    eref Move' blk a -> [Move' blk a] -> [Move' blk a]
    forall a. a -> [a] -> [a]
    :)
         Maybe (PrioMeta blk, [OKMeta blk])
    -> StateT [Restore] IO (Maybe (PrioMeta blk, [OKMeta blk]))
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (PrioMeta blk, [OKMeta blk])
    forall a. Maybe a
    Nothing
        And Maybe [Term blk]
    coms MetaEnv (PB blk)
    p1 MetaEnv (PB blk)
    p2 -> do
         let Just CTree blk
    jnode = Maybe (CTree blk)
    node
         SubConstraints blk
    sc <- IO (SubConstraints blk) -> StateT [Restore] IO (SubConstraints blk)
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (IO (SubConstraints blk)
     -> StateT [Restore] IO (SubConstraints blk))
    -> IO (SubConstraints blk)
    -> StateT [Restore] IO (SubConstraints blk)
    forall a b. (a -> b) -> a -> b
    $ CTree blk -> IO (SubConstraints blk)
    forall blk. CTree blk -> IO (SubConstraints blk)
    newSubConstraints CTree blk
    jnode

         IORef (Maybe (SubConstraints blk))
    -> Maybe (SubConstraints blk) -> Undo ()
    forall a. IORef a -> a -> Undo ()
    uwriteIORef (CTree blk -> IORef (Maybe (SubConstraints blk))
    forall blk. CTree blk -> IORef (Maybe (SubConstraints blk))
    ctsub CTree blk
    jnode) (Maybe (SubConstraints blk) -> Undo ())
    -> Maybe (SubConstraints blk) -> Undo ()
    forall a b. (a -> b) -> a -> b
    $ SubConstraints blk -> Maybe (SubConstraints blk)
    forall a. a -> Maybe a
    Just SubConstraints blk
    sc
         Int
    ndep <- case Maybe [Term blk]
    coms of
          Maybe [Term blk]
    Nothing -> Int -> Undo Int
    forall (m :: * -> *) a. Monad m => a -> m a
    return Int
    1 -- no metas pointing to it so will never decrement to 0
          Just [Term blk]
    _coms  -> Int -> Undo Int
    forall (m :: * -> *) a. Monad m => a -> m a
    return Int
    1 -- dito
         IO () -> Undo ()
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (IO () -> Undo ()) -> IO () -> Undo ()
    forall a b. (a -> b) -> a -> b
    $ IORef Int -> Int -> IO ()
    forall a. IORef a -> a -> IO ()
    NoUndo.writeIORef (SubConstraints blk -> IORef Int
    forall blk. SubConstraints blk -> IORef Int
    sccomcount SubConstraints blk
    sc) Int
    ndep -- OK since sc was just created
         Maybe (PrioMeta blk, [OKMeta blk])
    resp1 <- Maybe (CTree blk)
    -> MetaEnv (PB blk)
    -> StateT [Restore] IO (Maybe (PrioMeta blk, [OKMeta blk]))
    donewp (CTree blk -> Maybe (CTree blk)
    forall a. a -> Maybe a
    Just (CTree blk -> Maybe (CTree blk)) -> CTree blk -> Maybe (CTree blk)
    forall a b. (a -> b) -> a -> b
    $ SubConstraints blk -> CTree blk
    forall blk. SubConstraints blk -> CTree blk
    scsub1 SubConstraints blk
    sc) MetaEnv (PB blk)
    p1
         case Maybe (PrioMeta blk, [OKMeta blk])
    resp1 of
          Just (PrioMeta blk
    pm1, [OKMeta blk]
    phs1) -> do
           Maybe (PrioMeta blk, [OKMeta blk])
    resp2 <- Maybe (CTree blk)
    -> MetaEnv (PB blk)
    -> StateT [Restore] IO (Maybe (PrioMeta blk, [OKMeta blk]))
    donewp (CTree blk -> Maybe (CTree blk)
    forall a. a -> Maybe a
    Just (CTree blk -> Maybe (CTree blk)) -> CTree blk -> Maybe (CTree blk)
    forall a b. (a -> b) -> a -> b
    $ SubConstraints blk -> CTree blk
    forall blk. SubConstraints blk -> CTree blk
    scsub2 SubConstraints blk
    sc) MetaEnv (PB blk)
    p2
           case Maybe (PrioMeta blk, [OKMeta blk])
    resp2 of
            Just (PrioMeta blk
    pm2, [OKMeta blk]
    phs2) ->
             Maybe (CTree blk)
    -> PrioMeta blk
    -> [OKMeta blk]
    -> StateT [Restore] IO (Maybe (PrioMeta blk, [OKMeta blk]))
    forall {blk}.
    Maybe (CTree blk)
    -> PrioMeta blk
    -> [OKMeta blk]
    -> StateT [Restore] IO (Maybe (PrioMeta blk, [OKMeta blk]))
    storeprio Maybe (CTree blk)
    node (Bool -> PrioMeta blk -> PrioMeta blk -> PrioMeta blk
    forall blk. Bool -> PrioMeta blk -> PrioMeta blk -> PrioMeta blk
    choosePrioMeta Bool
    False PrioMeta blk
    pm1 PrioMeta blk
    pm2) ([OKMeta blk]
    phs1 [OKMeta blk] -> [OKMeta blk] -> [OKMeta blk]
    forall a. [a] -> [a] -> [a]
    ++ [OKMeta blk]
    phs2)
            resp2 :: Maybe (PrioMeta blk, [OKMeta blk])
    resp2@Maybe (PrioMeta blk, [OKMeta blk])
    Nothing -> Maybe (PrioMeta blk, [OKMeta blk])
    -> StateT [Restore] IO (Maybe (PrioMeta blk, [OKMeta blk]))
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (PrioMeta blk, [OKMeta blk])
    resp2
          resp1 :: Maybe (PrioMeta blk, [OKMeta blk])
    resp1@Maybe (PrioMeta blk, [OKMeta blk])
    Nothing -> Maybe (PrioMeta blk, [OKMeta blk])
    -> StateT [Restore] IO (Maybe (PrioMeta blk, [OKMeta blk]))
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (PrioMeta blk, [OKMeta blk])
    resp1
        Sidecondition MetaEnv (PB blk)
    sidep MetaEnv (PB blk)
    mainp -> do
         Maybe (PrioMeta blk, [OKMeta blk])
    resp1 <- Maybe (CTree blk)
    -> MetaEnv (PB blk)
    -> StateT [Restore] IO (Maybe (PrioMeta blk, [OKMeta blk]))
    donewp Maybe (CTree blk)
    forall a. Maybe a
    Nothing MetaEnv (PB blk)
    sidep
         case Maybe (PrioMeta blk, [OKMeta blk])
    resp1 of
          Just{} -> do
           Maybe (PrioMeta blk, [OKMeta blk])
    resp2 <- Maybe (CTree blk)
    -> MetaEnv (PB blk)
    -> StateT [Restore] IO (Maybe (PrioMeta blk, [OKMeta blk]))
    donewp Maybe (CTree blk)
    node MetaEnv (PB blk)
    mainp
           case Maybe (PrioMeta blk, [OKMeta blk])
    resp2 of
            Just (PrioMeta blk
    pm2, [OKMeta blk]
    phs2) ->
             Maybe (CTree blk)
    -> PrioMeta blk
    -> [OKMeta blk]
    -> StateT [Restore] IO (Maybe (PrioMeta blk, [OKMeta blk]))
    forall {blk}.
    Maybe (CTree blk)
    -> PrioMeta blk
    -> [OKMeta blk]
    -> StateT [Restore] IO (Maybe (PrioMeta blk, [OKMeta blk]))
    storeprio Maybe (CTree blk)
    node PrioMeta blk
    pm2 [OKMeta blk]
    phs2
            resp2 :: Maybe (PrioMeta blk, [OKMeta blk])
    resp2@Maybe (PrioMeta blk, [OKMeta blk])
    Nothing -> Maybe (PrioMeta blk, [OKMeta blk])
    -> StateT [Restore] IO (Maybe (PrioMeta blk, [OKMeta blk]))
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (PrioMeta blk, [OKMeta blk])
    resp2
          resp1 :: Maybe (PrioMeta blk, [OKMeta blk])
    resp1@Maybe (PrioMeta blk, [OKMeta blk])
    Nothing -> Maybe (PrioMeta blk, [OKMeta blk])
    -> StateT [Restore] IO (Maybe (PrioMeta blk, [OKMeta blk]))
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (PrioMeta blk, [OKMeta blk])
    resp1
        Or Prio
    prio MetaEnv (PB blk)
    p1 MetaEnv (PB blk)
    p2 -> do
         Metavar Choice blk
    cm <- IO (Metavar Choice blk) -> StateT [Restore] IO (Metavar Choice blk)
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (IO (Metavar Choice blk)
     -> StateT [Restore] IO (Metavar Choice blk))
    -> IO (Metavar Choice blk)
    -> StateT [Restore] IO (Metavar Choice blk)
    forall a b. (a -> b) -> a -> b
    $ IO (Metavar Choice blk)
    forall a blk. IO (Metavar a blk)
    initMeta
         Maybe (CTree blk)
    -> MetaEnv (PB blk)
    -> StateT [Restore] IO (Maybe (PrioMeta blk, [OKMeta blk]))
    donewp Maybe (CTree blk)
    node (MM Choice blk
    -> Prio -> MetaEnv (PB blk) -> MetaEnv (PB blk) -> MetaEnv (PB blk)
    forall blk.
    MM Choice blk
    -> Prio -> MetaEnv (PB blk) -> MetaEnv (PB blk) -> MetaEnv (PB blk)
    choose (Metavar Choice blk -> MM Choice blk
    forall a blk. Metavar a blk -> MM a blk
    Meta Metavar Choice blk
    cm) Prio
    prio MetaEnv (PB blk)
    p1 MetaEnv (PB blk)
    p2)
        ConnectHandle (Meta OKMeta blk
    handle) MetaEnv (PB blk)
    p' -> do
         let Just CTree blk
    jnode = Maybe (CTree blk)
    node
         IORef [OKMeta blk] -> ([OKMeta blk] -> [OKMeta blk]) -> Undo ()
    forall a. IORef a -> (a -> a) -> Undo ()
    umodifyIORef (CTree blk -> IORef [OKMeta blk]
    forall blk. CTree blk -> IORef [OKMeta blk]
    cthandles CTree blk
    jnode) (OKMeta blk
    handle OKMeta blk -> [OKMeta blk] -> [OKMeta blk]
    forall a. a -> [a] -> [a]
    :)
         Maybe (CTree blk)
    -> MetaEnv (PB blk)
    -> StateT [Restore] IO (Maybe (PrioMeta blk, [OKMeta blk]))
    donewp Maybe (CTree blk)
    node MetaEnv (PB blk)
    p'
        ConnectHandle (NotM OKVal
    _) MetaEnv (PB blk)
    _ -> StateT [Restore] IO (Maybe (PrioMeta blk, [OKMeta blk]))
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    choosePrioMeta :: Bool -> PrioMeta blk -> PrioMeta blk -> PrioMeta blk
    choosePrioMeta :: forall blk. Bool -> PrioMeta blk -> PrioMeta blk -> PrioMeta blk
    choosePrioMeta Bool
    flip pm1 :: PrioMeta blk
    pm1@(PrioMeta Prio
    p1 Metavar a blk
    _) pm2 :: PrioMeta blk
    pm2@(PrioMeta Prio
    p2 Metavar a blk
    _)
      | Prio
    p1 Prio -> Prio -> Bool
    forall a. Ord a => a -> a -> Bool
    > Prio
    p2 = PrioMeta blk
    pm1
      | Prio
    p2 Prio -> Prio -> Bool
    forall a. Ord a => a -> a -> Bool
    > Prio
    p1 = PrioMeta blk
    pm2
      | Bool
    flip = PrioMeta blk
    pm2
      | Bool
    otherwise = PrioMeta blk
    pm1
    choosePrioMeta Bool
    _ pm :: PrioMeta blk
    pm@(PrioMeta Prio
    _ Metavar a blk
    _) (NoPrio Bool
    _) = PrioMeta blk
    pm
    choosePrioMeta Bool
    _ (NoPrio Bool
    _) pm :: PrioMeta blk
    pm@(PrioMeta Prio
    _ Metavar a blk
    _) = PrioMeta blk
    pm
    choosePrioMeta Bool
    _ (NoPrio Bool
    d1) (NoPrio Bool
    d2) = Bool -> PrioMeta blk
    forall blk. Bool -> PrioMeta blk
    NoPrio (Bool
    d1 Bool -> Bool -> Bool
    && Bool
    d2)

    propagatePrio :: CTree blk -> Undo [OKMeta blk]
    propagatePrio :: forall blk. CTree blk -> Undo [OKMeta blk]
    propagatePrio CTree blk
    node = do
      Maybe (CTree blk)
    parent <- IO (Maybe (CTree blk)) -> StateT [Restore] IO (Maybe (CTree blk))
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (IO (Maybe (CTree blk)) -> StateT [Restore] IO (Maybe (CTree blk)))
    -> IO (Maybe (CTree blk))
    -> StateT [Restore] IO (Maybe (CTree blk))
    forall a b. (a -> b) -> a -> b
    $ IORef (Maybe (CTree blk)) -> IO (Maybe (CTree blk))
    forall a. IORef a -> IO a
    readIORef (IORef (Maybe (CTree blk)) -> IO (Maybe (CTree blk)))
    -> IORef (Maybe (CTree blk)) -> IO (Maybe (CTree blk))
    forall a b. (a -> b) -> a -> b
    $ CTree blk -> IORef (Maybe (CTree blk))
    forall blk. CTree blk -> IORef (Maybe (CTree blk))
    ctparent CTree blk
    node
      case Maybe (CTree blk)
    parent of
        Maybe (CTree blk)
    Nothing     -> [OKMeta blk] -> Undo [OKMeta blk]
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
        Just CTree blk
    parent -> do
          Just SubConstraints blk
    sc <- IORef (Maybe (SubConstraints blk))
    -> Undo (Maybe (SubConstraints blk))
    forall a. IORef a -> Undo a
    ureadIORef (CTree blk -> IORef (Maybe (SubConstraints blk))
    forall blk. CTree blk -> IORef (Maybe (SubConstraints blk))
    ctsub CTree blk
    parent)
          PrioMeta blk
    pm1     <- IORef (PrioMeta blk) -> Undo (PrioMeta blk)
    forall a. IORef a -> Undo a
    ureadIORef (IORef (PrioMeta blk) -> Undo (PrioMeta blk))
    -> IORef (PrioMeta blk) -> Undo (PrioMeta blk)
    forall a b. (a -> b) -> a -> b
    $ CTree blk -> IORef (PrioMeta blk)
    forall blk. CTree blk -> IORef (PrioMeta blk)
    ctpriometa (CTree blk -> IORef (PrioMeta blk))
    -> CTree blk -> IORef (PrioMeta blk)
    forall a b. (a -> b) -> a -> b
    $ SubConstraints blk -> CTree blk
    forall blk. SubConstraints blk -> CTree blk
    scsub1 SubConstraints blk
    sc
          PrioMeta blk
    pm2     <- IORef (PrioMeta blk) -> Undo (PrioMeta blk)
    forall a. IORef a -> Undo a
    ureadIORef (IORef (PrioMeta blk) -> Undo (PrioMeta blk))
    -> IORef (PrioMeta blk) -> Undo (PrioMeta blk)
    forall a b. (a -> b) -> a -> b
    $ CTree blk -> IORef (PrioMeta blk)
    forall blk. CTree blk -> IORef (PrioMeta blk)
    ctpriometa (CTree blk -> IORef (PrioMeta blk))
    -> CTree blk -> IORef (PrioMeta blk)
    forall a b. (a -> b) -> a -> b
    $ SubConstraints blk -> CTree blk
    forall blk. SubConstraints blk -> CTree blk
    scsub2 SubConstraints blk
    sc
          Bool
    flip    <- IORef Bool -> Undo Bool
    forall a. IORef a -> Undo a
    ureadIORef (IORef Bool -> Undo Bool) -> IORef Bool -> Undo Bool
    forall a b. (a -> b) -> a -> b
    $ SubConstraints blk -> IORef Bool
    forall blk. SubConstraints blk -> IORef Bool
    scflip SubConstraints blk
    sc
          let pm :: PrioMeta blk
    pm = Bool -> PrioMeta blk -> PrioMeta blk -> PrioMeta blk
    forall blk. Bool -> PrioMeta blk -> PrioMeta blk -> PrioMeta blk
    choosePrioMeta Bool
    flip PrioMeta blk
    pm1 PrioMeta blk
    pm2
          PrioMeta blk
    opm <- IORef (PrioMeta blk) -> Undo (PrioMeta blk)
    forall a. IORef a -> Undo a
    ureadIORef (CTree blk -> IORef (PrioMeta blk)
    forall blk. CTree blk -> IORef (PrioMeta blk)
    ctpriometa CTree blk
    parent)
          if (PrioMeta blk
    pm PrioMeta blk -> PrioMeta blk -> Bool
    forall a. Eq a => a -> a -> Bool
    /= PrioMeta blk
    opm)
            then do
              IORef (PrioMeta blk) -> PrioMeta blk -> Undo ()
    forall a. IORef a -> a -> Undo ()
    uwriteIORef (CTree blk -> IORef (PrioMeta blk)
    forall blk. CTree blk -> IORef (PrioMeta blk)
    ctpriometa CTree blk
    parent) PrioMeta blk
    pm
              [OKMeta blk]
    phs <- case PrioMeta blk
    pm of
                NoPrio Bool
    True -> IORef [OKMeta blk] -> Undo [OKMeta blk]
    forall a. IORef a -> Undo a
    ureadIORef (CTree blk -> IORef [OKMeta blk]
    forall blk. CTree blk -> IORef [OKMeta blk]
    cthandles CTree blk
    parent)
                PrioMeta blk
    _           -> [OKMeta blk] -> Undo [OKMeta blk]
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
              [OKMeta blk]
    phs2 <- CTree blk -> Undo [OKMeta blk]
    forall blk. CTree blk -> Undo [OKMeta blk]
    propagatePrio CTree blk
    parent
              [OKMeta blk] -> Undo [OKMeta blk]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([OKMeta blk] -> Undo [OKMeta blk])
    -> [OKMeta blk] -> Undo [OKMeta blk]
    forall a b. (a -> b) -> a -> b
    $ [OKMeta blk]
    phs [OKMeta blk] -> [OKMeta blk] -> [OKMeta blk]
    forall a. [a] -> [a] -> [a]
    ++ [OKMeta blk]
    phs2
            else
              [OKMeta blk] -> Undo [OKMeta blk]
    forall (m :: * -> *) a. Monad m => a -> m a
    return []

    data Choice = LeftDisjunct | RightDisjunct

    choose :: MM Choice blk -> Prio -> MetaEnv (PB blk) -> MetaEnv (PB blk) -> MetaEnv (PB blk)
    choose :: forall blk.
    MM Choice blk
    -> Prio -> MetaEnv (PB blk) -> MetaEnv (PB blk) -> MetaEnv (PB blk)
    choose MM Choice blk
    c Prio
    prio MetaEnv (PB blk)
    p1 MetaEnv (PB blk)
    p2 =
     BlkInfo blk
    -> MM Choice blk
    -> (Choice -> MetaEnv (PB blk))
    -> MetaEnv (PB blk)
    forall a blk.
    Refinable a blk =>
    BlkInfo blk
    -> MM a blk -> (a -> MetaEnv (PB blk)) -> MetaEnv (PB blk)
    mmpcase (Bool
    True, Prio
    prio, Maybe blk
    forall a. Maybe a
    Nothing) MM Choice blk
    c ((Choice -> MetaEnv (PB blk)) -> MetaEnv (PB blk))
    -> (Choice -> MetaEnv (PB blk)) -> MetaEnv (PB blk)
    forall a b. (a -> b) -> a -> b
    $ \Choice
    c -> case Choice
    c of
      Choice
    LeftDisjunct -> MetaEnv (PB blk)
    p1
      Choice
    RightDisjunct -> MetaEnv (PB blk)
    p2

    instance Refinable Choice blk where
     refinements :: blk -> [blk] -> Metavar Choice blk -> IO [Move' blk Choice]
    refinements blk
    _ [blk]
    _ Metavar Choice blk
    _ = [Move' blk Choice] -> IO [Move' blk Choice]
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Move' blk Choice] -> IO [Move' blk Choice])
    -> [Move' blk Choice] -> IO [Move' blk Choice]
    forall a b. (a -> b) -> a -> b
    $ Cost -> RefCreateEnv blk Choice -> Move' blk Choice
    forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
    Move Cost
    0 (RefCreateEnv blk Choice -> Move' blk Choice)
    -> (Choice -> RefCreateEnv blk Choice)
    -> Choice
    -> Move' blk Choice
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Choice -> RefCreateEnv blk Choice
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Choice -> Move' blk Choice) -> [Choice] -> [Move' blk Choice]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> [Choice
    LeftDisjunct, Choice
    RightDisjunct]

    instance Refinable OKVal blk where
     refinements :: blk -> [blk] -> Metavar OKVal blk -> IO [Move' blk OKVal]
    refinements blk
    _ [blk]
    _ Metavar OKVal blk
    _ = IO [Move' blk OKVal]
    forall a. HasCallStack => a
    __IMPOSSIBLE__ -- OKVal should never be refined

    -- ------------------------------------