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 (OKHandle blk)
-> RefCreateEnv blk (OKHandle blk)
forall blk a.
StateT (IORef [SubConstraints blk], Int) IO a -> RefCreateEnv blk a
RefCreateEnv (StateT (IORef [SubConstraints blk], Int) IO (OKHandle blk)
 -> RefCreateEnv blk (OKHandle blk))
-> StateT (IORef [SubConstraints blk], Int) IO (OKHandle blk)
-> RefCreateEnv blk (OKHandle 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))
 OKHandle blk
-> StateT (IORef [SubConstraints blk], Int) IO (OKHandle blk)
forall (m :: * -> *) a. Monad m => a -> m a
return (OKHandle blk
 -> StateT (IORef [SubConstraints blk], Int) IO (OKHandle blk))
-> OKHandle blk
-> StateT (IORef [SubConstraints blk], Int) IO (OKHandle blk)
forall a b. (a -> b) -> a -> b
$ Metavar OKVal blk -> OKHandle 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


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