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
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
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
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 = forall b. TravWith b (Block (MM a blk)) => MM b (Block b) -> m ()
f MM a blk
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 = forall a blk. Metavar a blk -> IORef Bool
mprincipalpresent Metavar a1 blk1
m1 forall a. Eq a => a -> a -> 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 = 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 <- forall a. a -> IO (IORef a)
newIORef forall a. Maybe a
Nothing
 IORef Bool
pp <- forall a. a -> IO (IORef a)
newIORef Bool
False
 IORef [(QPB a blk, Maybe (CTree blk))]
obs <- forall a. a -> IO (IORef a)
newIORef []
 IORef [Move' blk a]
erefs <- forall a. a -> IO (IORef a)
newIORef []
 forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 <- forall a. a -> IO (IORef a)
newIORef []
 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 <- forall a. a -> IO (IORef a)
newIORef (forall blk. Bool -> PrioMeta blk
NoPrio Bool
False)
 IORef (Maybe (SubConstraints blk))
sub <- forall a. a -> IO (IORef a)
newIORef forall a. Maybe a
Nothing
 IORef (Maybe (CTree blk))
rparent <- forall a. a -> IO (IORef a)
newIORef Maybe (CTree blk)
parent
 IORef [OKMeta blk]
handles <- forall a. a -> IO (IORef a)
newIORef []
 forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 <- 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 <- forall a. a -> IO (IORef a)
newIORef Int
0
 CTree blk
sub1 <- forall blk. Maybe (CTree blk) -> IO (CTree blk)
newCTree forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just CTree blk
node
 CTree blk
sub2 <- forall blk. Maybe (CTree blk) -> IO (CTree blk)
newCTree forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just CTree blk
node
 forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 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 forall a. Eq a => a -> a -> Bool
== Prio
p2 Bool -> Bool -> 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 = forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ 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 <- forall a. IORef a -> Undo a
ureadIORef IORef a
ptr
 forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (forall a. IORef a -> a -> Restore
Restore IORef a
ptr a
oldval forall a. a -> [a] -> [a]
:)
 forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ 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 <- forall a. IORef a -> Undo a
ureadIORef IORef a
ptr
 forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (forall a. IORef a -> a -> Restore
Restore IORef a
ptr a
oldval forall a. a -> [a] -> [a]
:)
 forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ 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 <- forall a. IORef a -> Undo a
ureadIORef IORef a
ptr
 forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify (forall a. IORef a -> a -> Restore
Restore IORef a
ptr a
oldval forall a. a -> [a] -> [a]
:)
 forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> a -> IO ()
NoUndo.writeIORef IORef a
ptr (a -> a
f a
oldval)
 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) <- forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT Undo a
x []
 forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(Restore IORef a
ptr a
oldval) -> forall a. IORef a -> a -> IO ()
NoUndo.writeIORef IORef a
ptr a
oldval) [Restore]
restores
 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 = forall blk a.
StateT (IORef [SubConstraints blk], Int) IO a -> RefCreateEnv blk a
RefCreateEnv forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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    = forall blk a.
StateT (IORef [SubConstraints blk], Int) IO a -> RefCreateEnv blk a
RefCreateEnv forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall blk a.
StateT (IORef [SubConstraints blk], Int) IO a -> RefCreateEnv blk a
RefCreateEnv forall a b. (a -> b) -> a -> b
$ forall blk a.
RefCreateEnv blk a -> StateT (IORef [SubConstraints blk], Int) IO a
runRefCreateEnv RefCreateEnv blk (a -> b)
f forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> 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 = 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 = forall blk a.
StateT (IORef [SubConstraints blk], Int) IO a -> RefCreateEnv blk a
RefCreateEnv forall a b. (a -> b) -> a -> b
$ forall blk a.
RefCreateEnv blk a -> StateT (IORef [SubConstraints blk], Int) IO a
runRefCreateEnv RefCreateEnv blk a
t forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall blk a.
RefCreateEnv blk a -> StateT (IORef [SubConstraints blk], Int) IO a
runRefCreateEnv 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
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
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
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 = forall blk a.
StateT (IORef [SubConstraints blk], Int) IO a -> RefCreateEnv blk a
RefCreateEnv forall a b. (a -> b) -> a -> b
$ do
 (IORef [SubConstraints blk]
mcompoint, Int
c) <- forall s (m :: * -> *). MonadState s m => m s
get
 Metavar a blk
m <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall blk a. IORef [SubConstraints blk] -> IO (Metavar a blk)
newMeta IORef [SubConstraints blk]
mcompoint
 forall s (m :: * -> *). MonadState s m => s -> m ()
put (IORef [SubConstraints blk]
mcompoint, (Int
c forall a. Num a => a -> a -> a
+ Int
1))
 forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 = forall blk a.
StateT (IORef [SubConstraints blk], Int) IO a -> RefCreateEnv blk a
RefCreateEnv forall a b. (a -> b) -> a -> b
$ do
 (IORef [SubConstraints blk]
e, Int
c) <- forall s (m :: * -> *). MonadState s m => m s
get
 IORef [SubConstraints blk]
cp <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall a. a -> IO (IORef a)
newIORef []
 Metavar OKVal blk
m  <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall blk a. IORef [SubConstraints blk] -> IO (Metavar a blk)
newMeta IORef [SubConstraints blk]
cp
 forall s (m :: * -> *). MonadState s m => s -> m ()
put (IORef [SubConstraints blk]
e, (Int
c forall a. Num a => a -> a -> a
+ Int
1))
 forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 = forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (forall blk a.
RefCreateEnv blk a -> StateT (IORef [SubConstraints blk], Int) IO a
runRefCreateEnv RefCreateEnv blk a
bind) (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{}   = 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 <- forall a. IORef a -> IO a
readIORef forall a b. (a -> b) -> a -> b
$ 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a blk b.
Refinable b blk =>
Metavar b blk -> MetaEnv (MB a blk) -> MB a blk
Blocked Metavar a blk
m (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 <- forall a. IORef a -> IO a
readIORef forall a b. (a -> b) -> a -> b
$ forall a blk. Metavar a blk -> IORef (Maybe a)
mbind Metavar a blk
m
  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 <- forall a. IORef a -> IO a
readIORef forall a b. (a -> b) -> a -> b
$ 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall blk b.
Refinable b blk =>
Metavar b blk -> BlkInfo blk -> MetaEnv (PB blk) -> PB blk
PBlocked Metavar a blk
m BlkInfo blk
blkinfo (forall a blk.
Refinable a blk =>
BlkInfo blk
-> MM a blk -> (a -> MetaEnv (PB blk)) -> MetaEnv (PB blk)
mmpcase 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 = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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)
_ = 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a blk b.
Refinable b blk =>
Metavar b blk -> MetaEnv (MB a blk) -> MB a blk
Blocked Metavar b blk
m (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 -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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) (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 -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall blk. Prop blk -> PB blk
NotPB forall a b. (a -> b) -> a -> b
$ 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)
_ -> forall b. Refinable b blk => MM b blk -> MetaEnv (PB blk)
fm (forall a blk. Metavar a blk -> MM a blk
Meta Metavar b blk
m)
  Failed String
msg -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall blk. Prop blk -> PB blk
NotPB forall a b. (a -> b) -> a -> b
$ 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 =
 forall a blk b.
Refinable a blk =>
MM a blk -> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mmcase OKHandle blk
okh 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 = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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{} -> forall (m :: * -> *) a. Monad m => a -> m a
return MM a blk
x
 Meta Metavar a blk
m -> do
  Maybe a
bind <- forall a. IORef a -> IO a
readIORef forall a b. (a -> b) -> a -> b
$ forall a blk. Metavar a blk -> IORef (Maybe a)
mbind Metavar a blk
m
  case Maybe a
bind of
   Just a
x -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a blk. a -> MM a blk
NotM a
x
   Maybe a
Nothing -> 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 <- forall a. a -> IO (IORef a)
newIORef Bool
False


 CTree blk
mainroot <- forall blk. Maybe (CTree blk) -> IO (CTree blk)
newCTree 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
   forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Cost
depth forall a. Ord a => a -> a -> Bool
< Cost
depthinterval) forall a b. (a -> b) -> a -> b
$ do


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


   forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 <- forall a. IORef a -> IO a
readIORef forall a b. (a -> b) -> a -> b
$ forall blk. CTree blk -> IORef (PrioMeta blk)
ctpriometa CTree blk
root
     case PrioMeta blk
pm of
      NoPrio Bool
False -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 = forall a. Refinable a blk => Metavar a blk -> Cost -> IO SRes
fork Metavar a blk
m Cost
depth
       Maybe (SubConstraints blk)
sub <- forall a. IORef a -> IO a
readIORef forall a b. (a -> b) -> a -> b
$ 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 = forall blk. SubConstraints blk -> CTree blk
scsub1 SubConstraints blk
sc
             sub2 :: CTree blk
sub2 = forall blk. SubConstraints blk -> CTree blk
scsub2 SubConstraints blk
sc
         PrioMeta blk
pm1 <- forall a. IORef a -> IO a
readIORef forall a b. (a -> b) -> a -> b
$ forall blk. CTree blk -> IORef (PrioMeta blk)
ctpriometa CTree blk
sub1
         PrioMeta blk
pm2 <- forall a. IORef a -> IO a
readIORef forall a b. (a -> b) -> a -> b
$ 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 <- forall a. IORef a -> IO a
readIORef forall a b. (a -> b) -> a -> b
$ 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 <- forall a blk. Metavar a blk -> IO [blk]
extractblkinfos Metavar a blk
m
      [Move' blk a]
refs <- 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 <- forall a. IORef a -> IO a
readIORef forall a b. (a -> b) -> a -> b
$ forall a blk. Metavar a blk -> IORef [Move' blk a]
mextrarefs Metavar a blk
m
       case [Move' blk a]
erefs of
        [] -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. a -> Either a b
Left Bool
False)
        [Move' blk a]
_ -> do
         forall a. IORef a -> a -> IO ()
NoUndo.writeIORef (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 (forall a. Metavar a blk -> RefCreateEnv blk a -> Cost -> IO SRes
refine Metavar a blk
m RefCreateEnv blk a
bind (Cost
depth 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
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return SRes
res
      Left Bool
found -> do
       Int
n <- forall a. IORef a -> IO a
readIORef IORef Int
nsol
       if Int
n forall a. Eq a => a -> a -> Bool
== Int
0 then
         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 forall a. HasCallStack => a
__IMPOSSIBLE__ else forall (m :: * -> *) a. Monad m => a -> m a
return SRes
res2
          Left Bool
found2 -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 forall a. Ord a => a -> a -> Bool
< Cost
0 = do
     forall a. IORef a -> a -> IO ()
NoUndo.writeIORef IORef Bool
depthreached Bool
True
     forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left Bool
False


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


        (a
bind, (IORef [SubConstraints blk]
_, Int
nnewmeta)) <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (forall blk a.
RefCreateEnv blk a -> StateT (IORef [SubConstraints blk], Int) IO a
runRefCreateEnv RefCreateEnv blk a
bind) (forall a blk. Metavar a blk -> IORef [SubConstraints blk]
mcompoint Metavar a blk
m, Int
0)
        forall a. IORef a -> a -> Undo ()
uwriteIORef (forall a blk. Metavar a blk -> IORef (Maybe a)
mbind Metavar a blk
m) (forall a. a -> Maybe a
Just a
bind)
        [SubConstraints blk]
mcomptr <- forall a. IORef a -> Undo a
ureadIORef forall a b. (a -> b) -> a -> b
$ forall a blk. Metavar a blk -> IORef [SubConstraints blk]
mcompoint Metavar a blk
m
        forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\SubConstraints blk
comptr ->
          forall a. IORef a -> (a -> a) -> Undo ()
umodifyIORef (forall blk. SubConstraints blk -> IORef Int
sccomcount SubConstraints blk
comptr) (forall a. Num a => a -> a -> a
+ (Int
nnewmeta 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 <- forall a. IORef a -> Undo a
ureadIORef (forall a blk.
Metavar a blk -> IORef [(QPB a blk, Maybe (CTree blk))]
mobs Metavar a blk
m)
        Bool
res <- forall a blk. [(QPB a blk, Maybe (CTree blk))] -> Undo Bool
recalcs [(QPB a blk, Maybe (CTree blk))]
obs
        if Bool
res
          then
            forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left Bool
False     -- failed
          else
            forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift 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
     forall (m :: * -> *) a. Monad m => a -> m a
return 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 forall a. Eq a => a -> a -> Bool
== Int
0 then
          forall a b. a -> Either a b
Left Bool
False
         else
          forall a b. b -> Either a b
Right (Int
n forall a. Num a => a -> a -> a
- Int
1)
        Just IORef Bool
_ ->
         forall a b. b -> Either a b
Right (Int
n 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
_ -> 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 <- 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
        forall a. IORef a -> a -> IO ()
NoUndo.writeIORef IORef Bool
rdone Bool
True
        IO SRes
doit

 forall a. Undo a -> IO a
runUndo forall a b. (a -> b) -> a -> b
$ do
  Bool
res <- forall blk. MetaEnv (PB blk) -> Maybe (CTree blk) -> Undo Bool
reccalc MetaEnv (PB blk)
p (forall a. a -> Maybe a
Just CTree blk
mainroot)
  if Bool
res -- failed immediately
    then
        forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
    else
      do
        Left Bool
_solFound <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ [(CTree blk, Maybe (IORef Bool))] -> Cost -> IO SRes
searchSubProb [(CTree blk
mainroot, forall a. Maybe a
Nothing)] Cost
searchdepth
        forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ 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 <- forall a. IORef a -> IO a
readIORef forall a b. (a -> b) -> a -> b
$ forall a blk.
Metavar a blk -> IORef [(QPB a blk, Maybe (CTree blk))]
mobs Metavar a blk
m
 forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ 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 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 = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Undo Bool -> Undo Bool -> Undo Bool
seqc forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a blk. (QPB a blk, Maybe (CTree blk)) -> Undo Bool
recalc) (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 -> 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 -> 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 <- forall a. IORef a -> Undo a
ureadIORef IORef Bool
flag
    if Bool
fl
      then forall (m :: * -> *) a. Monad m => a -> m a
return Bool
False
      else do
        forall a. IORef a -> a -> Undo ()
uwriteIORef IORef Bool
flag Bool
True
        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 <- 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return Bool
True
    Just [OKMeta blk]
pendhandles ->
      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 forall (m :: * -> *) a. Monad m => a -> m a
return Bool
res1
              else do
                forall a. IORef a -> a -> Undo ()
uwriteIORef (forall a blk. Metavar a blk -> IORef (Maybe a)
mbind OKMeta blk
h) forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just OKVal
OKVal
                [(QPB OKVal blk, Maybe (CTree blk))]
obs <- forall a. IORef a -> Undo a
ureadIORef (forall a blk.
Metavar a blk -> IORef [(QPB a blk, Maybe (CTree blk))]
mobs OKMeta blk
h)
                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 -> forall blk. CTree blk -> Undo [OKMeta blk]
propagatePrio CTree blk
node
     Maybe (CTree blk)
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return []
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just ([OKMeta blk]
pendhandles forall a. [a] -> [a] -> [a]
++ [OKMeta blk]
pendhandles2)
   Maybe (PrioMeta blk, [OKMeta blk])
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return 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 <- forall a. IORef a -> Undo a
ureadIORef (forall blk. CTree blk -> IORef [OKMeta blk]
cthandles CTree blk
node)
     forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [OKMeta blk]
handles forall a. [a] -> [a] -> [a]
++ [OKMeta blk]
pendhandles
    PrioMeta blk
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return [OKMeta blk]
pendhandles
   forall a. IORef a -> a -> Undo ()
uwriteIORef (forall blk. CTree blk -> IORef (PrioMeta blk)
ctpriometa CTree blk
node) PrioMeta blk
pm
   forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just (PrioMeta blk
pm, [OKMeta blk]
pendhandles')
  storeprio Maybe (CTree blk)
Nothing PrioMeta blk
_ [OKMeta blk]
_ =
   forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just (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 <- 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 <- forall a. IORef a -> (a -> a) -> Undo a
ureadmodifyIORef (forall a blk.
Metavar a blk -> IORef [(QPB a blk, Maybe (CTree blk))]
mobs Metavar b blk
m) ((forall b blk. BlkInfo blk -> MetaEnv (PB blk) -> QPB b blk
QPBlocked BlkInfo blk
blkinfo MetaEnv (PB blk)
cont, Maybe (CTree blk)
node) forall a. a -> [a] -> [a]
:)
     let (Bool
princ, Prio
prio, Maybe blk
_) = BlkInfo blk
blkinfo
     Bool
pp <- forall a. IORef a -> Undo a
ureadIORef (forall a blk. Metavar a blk -> IORef Bool
mprincipalpresent Metavar b blk
m)
     forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool
princ Bool -> Bool -> Bool
&& Bool -> Bool
not Bool
pp) forall a b. (a -> b) -> a -> b
$ do
      forall a. IORef a -> a -> Undo ()
uwriteIORef (forall a blk. Metavar a blk -> IORef Bool
mprincipalpresent Metavar b blk
m) Bool
True
      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


            forall a. IORef a -> a -> Undo ()
uwriteIORef (forall blk. CTree blk -> IORef (PrioMeta blk)
ctpriometa CTree blk
node) (forall blk a.
Refinable a blk =>
Prio -> Metavar a blk -> PrioMeta blk
PrioMeta Prio
prio Metavar b blk
m)
            forall blk. CTree blk -> Undo [OKMeta blk]
propagatePrio CTree blk
node
           QPDoubleBlocked IORef Bool
_flag MetaEnv (PB blk)
_ ->
            forall (m :: * -> *) a. Monad m => a -> m a
return []
         Maybe (CTree blk)
Nothing -> 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
       forall {blk}.
Maybe (CTree blk)
-> PrioMeta blk
-> [OKMeta blk]
-> StateT [Restore] IO (Maybe (PrioMeta blk, [OKMeta blk]))
storeprio Maybe (CTree blk)
node (forall blk a.
Refinable a blk =>
Prio -> Metavar a blk -> PrioMeta blk
PrioMeta Prio
prio Metavar b blk
m) []
      else
       forall {blk}.
Maybe (CTree blk)
-> PrioMeta blk
-> [OKMeta blk]
-> StateT [Restore] IO (Maybe (PrioMeta blk, [OKMeta blk]))
storeprio Maybe (CTree blk)
node (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 <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ 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 = ((forall b blk. IORef Bool -> MetaEnv (PB blk) -> QPB b blk
QPDoubleBlocked IORef Bool
flag MetaEnv (PB blk)
cont, Maybe (CTree blk)
node) forall a. a -> [a] -> [a]
:)
     forall a. IORef a -> (a -> a) -> Undo ()
umodifyIORef (forall a blk.
Metavar a blk -> IORef [(QPB a blk, Maybe (CTree blk))]
mobs Metavar b1 blk
m1) forall b.
[(QPB b blk, Maybe (CTree blk))]
-> [(QPB b blk, Maybe (CTree blk))]
newobs
     forall a. IORef a -> (a -> a) -> Undo ()
umodifyIORef (forall a blk.
Metavar a blk -> IORef [(QPB a blk, Maybe (CTree blk))]
mobs Metavar b2 blk
m2) forall b.
[(QPB b blk, Maybe (CTree blk))]
-> [(QPB b blk, Maybe (CTree blk))]
newobs
     forall {blk}.
Maybe (CTree blk)
-> PrioMeta blk
-> [OKMeta blk]
-> StateT [Restore] IO (Maybe (PrioMeta blk, [OKMeta blk]))
storeprio Maybe (CTree blk)
node (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 -> forall {blk}.
Maybe (CTree blk)
-> PrioMeta blk
-> [OKMeta blk]
-> StateT [Restore] IO (Maybe (PrioMeta blk, [OKMeta blk]))
storeprio Maybe (CTree blk)
node (forall blk. Bool -> PrioMeta blk
NoPrio Bool
True) []
    Error String
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing


    AddExtraRef String
_ Metavar a blk
m Move' blk a
eref -> do
     forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> (a -> a) -> IO ()
NoUndo.modifyIORef (forall a blk. Metavar a blk -> IORef [Move' blk a]
mextrarefs Metavar a blk
m) (Move' blk a
eref forall a. a -> [a] -> [a]
:)
     forall (m :: * -> *) a. Monad m => a -> m a
return 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 <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall blk. CTree blk -> IO (SubConstraints blk)
newSubConstraints CTree blk
jnode


     forall a. IORef a -> a -> Undo ()
uwriteIORef (forall blk. CTree blk -> IORef (Maybe (SubConstraints blk))
ctsub CTree blk
jnode) forall a b. (a -> b) -> a -> b
$ forall a. a -> Maybe a
Just SubConstraints blk
sc
     Int
ndep <- case Maybe [Term blk]
coms of
      Maybe [Term blk]
Nothing -> 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  -> forall (m :: * -> *) a. Monad m => a -> m a
return Int
1 -- dito
     forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> a -> IO ()
NoUndo.writeIORef (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 (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ 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 (forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ 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) ->
         forall {blk}.
Maybe (CTree blk)
-> PrioMeta blk
-> [OKMeta blk]
-> StateT [Restore] IO (Maybe (PrioMeta blk, [OKMeta blk]))
storeprio Maybe (CTree blk)
node (forall blk. Bool -> PrioMeta blk -> PrioMeta blk -> PrioMeta blk
choosePrioMeta Bool
False PrioMeta blk
pm1 PrioMeta blk
pm2) ([OKMeta blk]
phs1 forall a. [a] -> [a] -> [a]
++ [OKMeta blk]
phs2)
        resp2 :: Maybe (PrioMeta blk, [OKMeta blk])
resp2@Maybe (PrioMeta blk, [OKMeta blk])
Nothing -> 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 -> 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 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) ->
         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 -> 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 -> 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 <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ 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 (forall blk.
MM Choice blk
-> Prio -> MetaEnv (PB blk) -> MetaEnv (PB blk) -> MetaEnv (PB blk)
choose (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
     forall a. IORef a -> (a -> a) -> Undo ()
umodifyIORef (forall blk. CTree blk -> IORef [OKMeta blk]
cthandles CTree blk
jnode) (OKMeta blk
handle 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)
_ -> 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 forall a. Ord a => a -> a -> Bool
> Prio
p2 = PrioMeta blk
pm1
  | Prio
p2 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) = 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 <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall a. IORef a -> IO a
readIORef forall a b. (a -> b) -> a -> b
$ forall blk. CTree blk -> IORef (Maybe (CTree blk))
ctparent CTree blk
node
  case Maybe (CTree blk)
parent of
    Maybe (CTree blk)
Nothing     -> forall (m :: * -> *) a. Monad m => a -> m a
return []
    Just CTree blk
parent -> do
      Just SubConstraints blk
sc <- forall a. IORef a -> Undo a
ureadIORef (forall blk. CTree blk -> IORef (Maybe (SubConstraints blk))
ctsub CTree blk
parent)
      PrioMeta blk
pm1     <- forall a. IORef a -> Undo a
ureadIORef forall a b. (a -> b) -> a -> b
$ forall blk. CTree blk -> IORef (PrioMeta blk)
ctpriometa forall a b. (a -> b) -> a -> b
$ forall blk. SubConstraints blk -> CTree blk
scsub1 SubConstraints blk
sc
      PrioMeta blk
pm2     <- forall a. IORef a -> Undo a
ureadIORef forall a b. (a -> b) -> a -> b
$ forall blk. CTree blk -> IORef (PrioMeta blk)
ctpriometa forall a b. (a -> b) -> a -> b
$ forall blk. SubConstraints blk -> CTree blk
scsub2 SubConstraints blk
sc
      Bool
flip    <- forall a. IORef a -> Undo a
ureadIORef forall a b. (a -> b) -> a -> b
$ forall blk. SubConstraints blk -> IORef Bool
scflip SubConstraints blk
sc
      let pm :: PrioMeta blk
pm = forall blk. Bool -> PrioMeta blk -> PrioMeta blk -> PrioMeta blk
choosePrioMeta Bool
flip PrioMeta blk
pm1 PrioMeta blk
pm2
      PrioMeta blk
opm <- forall a. IORef a -> Undo a
ureadIORef (forall blk. CTree blk -> IORef (PrioMeta blk)
ctpriometa CTree blk
parent)
      if (PrioMeta blk
pm forall a. Eq a => a -> a -> Bool
/= PrioMeta blk
opm)
        then do
          forall a. IORef a -> a -> Undo ()
uwriteIORef (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 -> forall a. IORef a -> Undo a
ureadIORef (forall blk. CTree blk -> IORef [OKMeta blk]
cthandles CTree blk
parent)
            PrioMeta blk
_           -> forall (m :: * -> *) a. Monad m => a -> m a
return []
          [OKMeta blk]
phs2 <- forall blk. CTree blk -> Undo [OKMeta blk]
propagatePrio CTree blk
parent
          forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [OKMeta blk]
phs forall a. [a] -> [a] -> [a]
++ [OKMeta blk]
phs2
        else
          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 =
 forall a blk.
Refinable a blk =>
BlkInfo blk
-> MM a blk -> (a -> MetaEnv (PB blk)) -> MetaEnv (PB blk)
mmpcase (Bool
True, Prio
prio, forall a. Maybe a
Nothing) MM Choice blk
c 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
_ = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall blk a. Cost -> RefCreateEnv blk a -> Move' blk a
Move Cost
0 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (m :: * -> *) a. Monad m => a -> m a
return 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
_ = forall a. HasCallStack => a
__IMPOSSIBLE__ -- OKVal should never be refined


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