Safe Haskell	None
Language	Haskell2010

Agda.Auto.NarrowingSearch

Synopsis

newtype Prio = Prio {
- getPrio :: Int
}
class Trav a where
- type Block a
- trav :: Monad m => (forall b. TravWith b (Block a) => MM b (Block b) -> m ()) -> a -> m ()
type TravWith a blk = (Trav a, Block a ~ blk)
data Term blk = forall a.TravWith a blk => Term a
data Prop blk
- = OK
- | Error String
- | forall a. AddExtraRef String (Metavar a blk) (Move' blk a)
- | And (Maybe [Term blk]) (MetaEnv (PB blk)) (MetaEnv (PB blk))
- | Sidecondition (MetaEnv (PB blk)) (MetaEnv (PB blk))
- | Or Prio (MetaEnv (PB blk)) (MetaEnv (PB blk))
- | ConnectHandle (OKHandle blk) (MetaEnv (PB blk))
data OKVal = OKVal
type OKHandle blk = MM OKVal blk
type OKMeta blk = Metavar OKVal blk
data Metavar a blk = Metavar {
- mbind :: IORef (Maybe a)
- mprincipalpresent :: IORef Bool
- mobs :: IORef [(QPB a blk, Maybe (CTree blk))]
- mcompoint :: IORef [SubConstraints blk]
- mextrarefs :: IORef [Move' blk a]
}
hequalMetavar :: Metavar a1 blk1 -> Metavar a2 bkl2 -> Bool
newMeta :: IORef [SubConstraints blk] -> IO (Metavar a blk)
initMeta :: IO (Metavar a blk)
data CTree blk = CTree {
- ctpriometa :: IORef (PrioMeta blk)
- ctsub :: IORef (Maybe (SubConstraints blk))
- ctparent :: IORef (Maybe (CTree blk))
- cthandles :: IORef [OKMeta blk]
}
data SubConstraints blk = SubConstraints {
- scflip :: IORef Bool
- sccomcount :: IORef Int
- scsub1 :: CTree blk
- scsub2 :: CTree blk
}
newCTree :: Maybe (CTree blk) -> IO (CTree blk)
newSubConstraints :: CTree blk -> IO (SubConstraints blk)
data PrioMeta blk
- = forall a.Refinable a blk => PrioMeta Prio (Metavar a blk)
- | NoPrio Bool
data Restore = forall a. Restore (IORef a) a
type Undo = StateT [Restore] IO
ureadIORef :: IORef a -> Undo a
uwriteIORef :: IORef a -> a -> Undo ()
umodifyIORef :: IORef a -> (a -> a) -> Undo ()
ureadmodifyIORef :: IORef a -> (a -> a) -> Undo a
runUndo :: Undo a -> IO a
newtype RefCreateEnv blk a = RefCreateEnv {
- runRefCreateEnv :: StateT (IORef [SubConstraints blk], Int) IO a
}
newtype Cost = Cost {
- getCost :: Int
}
data Move' blk a = Move {
- moveCost :: Cost
- 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)
newOKHandle :: RefCreateEnv blk (OKHandle blk)
dryInstantiate :: RefCreateEnv blk a -> IO a
type BlkInfo blk = (Bool, Prio, Maybe blk)
data MM a blk
- = NotM a
- | Meta (Metavar a blk)
rm :: Empty -> MM a b -> a
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))
mmcase :: Refinable a blk => MM a blk -> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mmmcase :: MM a blk -> MetaEnv (MB b blk) -> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mmpcase :: Refinable a blk => BlkInfo blk -> MM a blk -> (a -> MetaEnv (PB blk)) -> MetaEnv (PB blk)
doubleblock :: (Refinable a blk, Refinable b blk) => MM a blk -> MM b blk -> MetaEnv (PB blk) -> MetaEnv (PB blk)
mbcase :: MetaEnv (MB a blk) -> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)
mbpcase :: Prio -> Maybe blk -> MetaEnv (MB a blk) -> (a -> MetaEnv (PB blk)) -> MetaEnv (PB blk)
mmbpcase :: MetaEnv (MB a blk) -> (forall b. Refinable b blk => MM b blk -> MetaEnv (PB blk)) -> (a -> MetaEnv (PB blk)) -> MetaEnv (PB blk)
waitok :: OKHandle blk -> MetaEnv (MB b blk) -> MetaEnv (MB b blk)
mbret :: a -> MetaEnv (MB a blk)
mbfailed :: String -> MetaEnv (MB a blk)
mpret :: Prop blk -> MetaEnv (PB blk)
expandbind :: MM a blk -> MetaEnv (MM a blk)
type HandleSol = IO ()
type SRes = Either Bool Int
topSearch :: forall blk. IORef Int -> IORef Int -> HandleSol -> blk -> MetaEnv (PB blk) -> Cost -> Cost -> IO Bool
extractblkinfos :: Metavar a blk -> IO [blk]
recalcs :: [(QPB a blk, Maybe (CTree blk))] -> Undo Bool
seqc :: Undo Bool -> Undo Bool -> Undo Bool
recalc :: (QPB a blk, Maybe (CTree blk)) -> Undo Bool
reccalc :: MetaEnv (PB blk) -> Maybe (CTree blk) -> Undo Bool
calc :: forall blk. MetaEnv (PB blk) -> Maybe (CTree blk) -> Undo (Maybe [OKMeta blk])
choosePrioMeta :: Bool -> PrioMeta blk -> PrioMeta blk -> PrioMeta blk
propagatePrio :: CTree blk -> Undo [OKMeta blk]
data Choice
- = LeftDisjunct
- | RightDisjunct
choose :: MM Choice blk -> Prio -> MetaEnv (PB blk) -> MetaEnv (PB blk) -> MetaEnv (PB blk)

Documentation

newtype Prio Source #

Constructors

Prio
Fields getPrio :: Int

Instances

Instances details

Eq Prio Source #
Instance details Defined in Agda.Auto.NarrowingSearch Methods (==) :: Prio -> Prio -> Bool # (/=) :: Prio -> Prio -> Bool #
Num Prio Source #
Instance details Defined in Agda.Auto.NarrowingSearch Methods (+) :: Prio -> Prio -> Prio # (-) :: Prio -> Prio -> Prio # (*) :: Prio -> Prio -> Prio # negate :: Prio -> Prio # abs :: Prio -> Prio # signum :: Prio -> Prio # fromInteger :: Integer -> Prio #
Ord Prio Source #
Instance details Defined in Agda.Auto.NarrowingSearch Methods compare :: Prio -> Prio -> Ordering # (<) :: Prio -> Prio -> Bool # (<=) :: Prio -> Prio -> Bool # (>) :: Prio -> Prio -> Bool # (>=) :: Prio -> Prio -> Bool # max :: Prio -> Prio -> Prio # min :: Prio -> Prio -> Prio #

class Trav a where Source #

Associated Types

type Block a Source #

Methods

trav :: Monad m => (forall b. TravWith b (Block a) => MM b (Block b) -> m ()) -> a -> m () Source #

Instances

Instances details

Trav a => Trav [a] Source #
Instance details Defined in Agda.Auto.SearchControl Associated Types type Block [a] Source # Methods trav :: Monad m => (forall b. TravWith b (Block [a]) => MM b (Block b) -> m ()) -> [a] -> m () Source #
Trav (ArgList o) Source #
Instance details Defined in Agda.Auto.SearchControl Associated Types type Block (ArgList o) Source # Methods trav :: Monad m => (forall b. TravWith b (Block (ArgList o)) => MM b (Block b) -> m ()) -> ArgList o -> m () Source #
Trav (Exp o) Source #
Instance details Defined in Agda.Auto.SearchControl Associated Types type Block (Exp o) Source # Methods trav :: Monad m => (forall b. TravWith b (Block (Exp o)) => MM b (Block b) -> m ()) -> Exp o -> m () Source #
Trav (MId, CExp o) Source #
Instance details Defined in Agda.Auto.SearchControl Associated Types type Block (MId, CExp o) Source # Methods trav :: Monad m => (forall b. TravWith b (Block (MId, CExp o)) => MM b (Block b) -> m ()) -> (MId, CExp o) -> m () Source #
TravWith a blk => Trav (MM a blk) Source #
Instance details Defined in Agda.Auto.NarrowingSearch Associated Types type Block (MM a blk) Source # Methods trav :: Monad m => (forall b. TravWith b (Block (MM a blk)) => MM b (Block b) -> m ()) -> MM a blk -> m () Source #
Trav (TrBr a o) Source #
Instance details Defined in Agda.Auto.SearchControl Associated Types type Block (TrBr a o) Source # Methods trav :: Monad m => (forall b. TravWith b (Block (TrBr a o)) => MM b (Block b) -> m ()) -> TrBr a o -> m () Source #

type TravWith a blk = (Trav a, Block a ~ blk) Source #

Trav instance a with block type blk

data Term blk Source #

Constructors

forall a.TravWith a blk => Term a

data Prop blk Source #

Result of type-checking.

Constructors

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 Source #

Constructors

OKVal

Instances

Instances details

Refinable OKVal blk Source #
Instance details Defined in Agda.Auto.NarrowingSearch Methods refinements :: blk -> [blk] -> Metavar OKVal blk -> IO [Move' blk OKVal] Source #

type OKHandle blk = MM OKVal blk Source #

type OKMeta blk = Metavar OKVal blk Source #

data Metavar a blk Source #

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).

Constructors

Metavar

Fields

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

Instances

Instances details

Eq (Metavar a blk) Source #
Instance details Defined in Agda.Auto.NarrowingSearch Methods (==) :: Metavar a blk -> Metavar a blk -> Bool # (/=) :: Metavar a blk -> Metavar a blk -> Bool #

hequalMetavar :: Metavar a1 blk1 -> Metavar a2 bkl2 -> Bool Source #

newMeta :: IORef [SubConstraints blk] -> IO (Metavar a blk) Source #

initMeta :: IO (Metavar a blk) Source #

data CTree blk Source #

Constructors

CTree
Fields ctpriometa :: IORef (PrioMeta blk) ctsub :: IORef (Maybe (SubConstraints blk)) ctparent :: IORef (Maybe (CTree blk)) cthandles :: IORef [OKMeta blk]

data SubConstraints blk Source #

Constructors

SubConstraints
Fields scflip :: IORef Bool sccomcount :: IORef Int scsub1 :: CTree blk scsub2 :: CTree blk

newCTree :: Maybe (CTree blk) -> IO (CTree blk) Source #

newSubConstraints :: CTree blk -> IO (SubConstraints blk) Source #

data PrioMeta blk Source #

Constructors

forall a.Refinable a blk => PrioMeta Prio (Metavar a blk)
NoPrio Bool

Instances

Instances details

Eq (PrioMeta blk) Source #
Instance details Defined in Agda.Auto.NarrowingSearch Methods (==) :: PrioMeta blk -> PrioMeta blk -> Bool # (/=) :: PrioMeta blk -> PrioMeta blk -> Bool #

data Restore Source #

Constructors

forall a. Restore (IORef a) a

type Undo = StateT [Restore] IO Source #

ureadIORef :: IORef a -> Undo a Source #

uwriteIORef :: IORef a -> a -> Undo () Source #

umodifyIORef :: IORef a -> (a -> a) -> Undo () Source #

ureadmodifyIORef :: IORef a -> (a -> a) -> Undo a Source #

runUndo :: Undo a -> IO a Source #

newtype RefCreateEnv blk a Source #

Constructors

RefCreateEnv
Fields runRefCreateEnv :: StateT (IORef [SubConstraints blk], Int) IO a

Instances

Instances details

Monad (RefCreateEnv blk) Source #
Instance details Defined in Agda.Auto.NarrowingSearch Methods (>>=) :: RefCreateEnv blk a -> (a -> RefCreateEnv blk b) -> RefCreateEnv blk b # (>>) :: RefCreateEnv blk a -> RefCreateEnv blk b -> RefCreateEnv blk b # return :: a -> RefCreateEnv blk a #
Functor (RefCreateEnv blk) Source #
Instance details Defined in Agda.Auto.NarrowingSearch Methods fmap :: (a -> b) -> RefCreateEnv blk a -> RefCreateEnv blk b # (<$) :: a -> RefCreateEnv blk b -> RefCreateEnv blk a #
Applicative (RefCreateEnv blk) Source #
Instance details Defined in Agda.Auto.NarrowingSearch Methods pure :: a -> RefCreateEnv blk a # (<>) :: RefCreateEnv blk (a -> b) -> RefCreateEnv blk a -> RefCreateEnv blk b # liftA2 :: (a -> b -> c) -> RefCreateEnv blk a -> RefCreateEnv blk b -> RefCreateEnv blk c # (>) :: RefCreateEnv blk a -> RefCreateEnv blk b -> RefCreateEnv blk b # (<*) :: RefCreateEnv blk a -> RefCreateEnv blk b -> RefCreateEnv blk a #

newtype Cost Source #

Constructors

Cost
Fields getCost :: Int

Instances

Instances details

Eq Cost Source #
Instance details Defined in Agda.Auto.NarrowingSearch Methods (==) :: Cost -> Cost -> Bool # (/=) :: Cost -> Cost -> Bool #
Num Cost Source #
Instance details Defined in Agda.Auto.NarrowingSearch Methods (+) :: Cost -> Cost -> Cost # (-) :: Cost -> Cost -> Cost # (*) :: Cost -> Cost -> Cost # negate :: Cost -> Cost # abs :: Cost -> Cost # signum :: Cost -> Cost # fromInteger :: Integer -> Cost #
Ord Cost Source #
Instance details Defined in Agda.Auto.NarrowingSearch Methods compare :: Cost -> Cost -> Ordering # (<) :: Cost -> Cost -> Bool # (<=) :: Cost -> Cost -> Bool # (>) :: Cost -> Cost -> Bool # (>=) :: Cost -> Cost -> Bool # max :: Cost -> Cost -> Cost # min :: Cost -> Cost -> Cost #

data Move' blk a Source #

Constructors

Move
Fields moveCost :: Cost moveNext :: RefCreateEnv blk a

class Refinable a blk where Source #

Methods

refinements :: blk -> [blk] -> Metavar a blk -> IO [Move' blk a] Source #

Instances

Instances details

Refinable Choice blk Source #
Instance details Defined in Agda.Auto.NarrowingSearch Methods refinements :: blk -> [blk] -> Metavar Choice blk -> IO [Move' blk Choice] Source #
Refinable OKVal blk Source #
Instance details Defined in Agda.Auto.NarrowingSearch Methods refinements :: blk -> [blk] -> Metavar OKVal blk -> IO [Move' blk OKVal] Source #
Refinable (ICExp o) (RefInfo o) Source #
Instance details Defined in Agda.Auto.SearchControl Methods refinements :: RefInfo o -> [RefInfo o] -> Metavar (ICExp o) (RefInfo o) -> IO [Move' (RefInfo o) (ICExp o)] Source #
Refinable (ArgList o) (RefInfo o) Source #
Instance details Defined in Agda.Auto.SearchControl Methods refinements :: RefInfo o -> [RefInfo o] -> Metavar (ArgList o) (RefInfo o) -> IO [Move' (RefInfo o) (ArgList o)] Source #
Refinable (Exp o) (RefInfo o) Source #
Instance details Defined in Agda.Auto.SearchControl Methods refinements :: RefInfo o -> [RefInfo o] -> Metavar (Exp o) (RefInfo o) -> IO [Move' (RefInfo o) (Exp o)] Source #
Refinable (ConstRef o) (RefInfo o) Source #
Instance details Defined in Agda.Auto.SearchControl Methods refinements :: RefInfo o -> [RefInfo o] -> Metavar (ConstRef o) (RefInfo o) -> IO [Move' (RefInfo o) (ConstRef o)] Source #

newPlaceholder :: RefCreateEnv blk (MM a blk) Source #

newOKHandle :: RefCreateEnv blk (OKHandle blk) Source #

dryInstantiate :: RefCreateEnv blk a -> IO a Source #

type BlkInfo blk = (Bool, Prio, Maybe blk) Source #

data MM a blk Source #

Constructors

NotM a
Meta (Metavar a blk)

Instances

Instances details

Conversion TOM Clause (Maybe ([Pat O], MExp O)) Source #
Instance details Defined in Agda.Auto.Convert Methods convert :: Clause -> TOM (Maybe ([Pat O], MExp O)) Source #
Conversion TOM Type (MExp O) Source #
Instance details Defined in Agda.Auto.Convert Methods convert :: Type -> TOM (MExp O) Source #
Conversion TOM Term (MExp O) Source #
Instance details Defined in Agda.Auto.Convert Methods convert :: Term -> TOM (MExp O) Source #
Conversion TOM Args (MM (ArgList O) (RefInfo O)) Source #
Instance details Defined in Agda.Auto.Convert Methods convert :: Args -> TOM (MM (ArgList O) (RefInfo O)) Source #
Conversion TOM [Clause] [([Pat O], MExp O)] Source #
Instance details Defined in Agda.Auto.Convert Methods convert :: [Clause] -> TOM [([Pat O], MExp O)] Source #
Conversion MOT a b => Conversion MOT (MM a (RefInfo O)) b Source #
Instance details Defined in Agda.Auto.Convert Methods convert :: MM a (RefInfo O) -> MOT b Source #
LocalTerminationEnv (MArgList o) Source #
Instance details Defined in Agda.Auto.CaseSplit Methods sizeAndBoundVars :: MArgList o -> (Sum Nat, [Nat]) Source #
LocalTerminationEnv (MExp o) Source #
Instance details Defined in Agda.Auto.CaseSplit Methods sizeAndBoundVars :: MExp o -> (Sum Nat, [Nat]) Source #
Refinable (ICExp o) (RefInfo o) Source #
Instance details Defined in Agda.Auto.SearchControl Methods refinements :: RefInfo o -> [RefInfo o] -> Metavar (ICExp o) (RefInfo o) -> IO [Move' (RefInfo o) (ICExp o)] Source #
Replace (Exp o) (MExp o) Source #
Instance details Defined in Agda.Auto.CaseSplit Associated Types type ReplaceWith (Exp o) (MExp o) Source # Methods replace' :: Nat -> MExp (ReplaceWith (Exp o) (MExp o)) -> Exp o -> Reader (Nat, Nat) (MExp o) Source #
Trav (MId, CExp o) Source #
Instance details Defined in Agda.Auto.SearchControl Associated Types type Block (MId, CExp o) Source # Methods trav :: Monad m => (forall b. TravWith b (Block (MId, CExp o)) => MM b (Block b) -> m ()) -> (MId, CExp o) -> m () Source #
TravWith a blk => Trav (MM a blk) Source #
Instance details Defined in Agda.Auto.NarrowingSearch Associated Types type Block (MM a blk) Source # Methods trav :: Monad m => (forall b. TravWith b (Block (MM a blk)) => MM b (Block b) -> m ()) -> MM a blk -> m () Source #
Renaming t => Renaming (MM t a) Source #
Instance details Defined in Agda.Auto.Syntax Methods renameOffset :: Nat -> (Nat -> Nat) -> MM t a -> MM t a Source #
FreeVars t => FreeVars (MM t a) Source #
Instance details Defined in Agda.Auto.Syntax Methods freeVarsOffset :: Nat -> MM t a -> Set Nat Source #
ExpandMetas t => ExpandMetas (MM t a) Source #
Instance details Defined in Agda.Auto.Syntax Methods expandMetas :: MM t a -> IO (MM t a) Source #
MetaliseOKH t => MetaliseOKH (MM t a) Source #
Instance details Defined in Agda.Auto.Syntax Methods metaliseOKH :: MM t a -> IO (MM t a) Source #
Lift t => Lift (MM t r) Source #
Instance details Defined in Agda.Auto.CaseSplit Methods lift' :: Nat -> Nat -> MM t r -> MM t r Source #
(Unify t, o ~ UnifiesTo t) => Unify (MM t (RefInfo o)) Source #
Instance details Defined in Agda.Auto.CaseSplit Associated Types type UnifiesTo (MM t (RefInfo o)) Source # Methods unify' :: MM t (RefInfo o) -> MM t (RefInfo o) -> StateT (Assignments (UnifiesTo (MM t (RefInfo o)))) Maybe () Source # notequal' :: MM t (RefInfo o) -> MM t (RefInfo o) -> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo (MM t (RefInfo o)))) IO) Bool Source #
Replace t u => Replace (MM t (RefInfo o)) u Source #
Instance details Defined in Agda.Auto.CaseSplit Associated Types type ReplaceWith (MM t (RefInfo o)) u Source # Methods replace' :: Nat -> MExp (ReplaceWith (MM t (RefInfo o)) u) -> MM t (RefInfo o) -> Reader (Nat, Nat) u Source #
type ReplaceWith (Exp o) (MExp o) Source #
Instance details Defined in Agda.Auto.CaseSplit type ReplaceWith (Exp o) (MExp o) = o
type Block (MId, CExp o) Source #
Instance details Defined in Agda.Auto.SearchControl type Block (MId, CExp o) = RefInfo o
type Block (MM a blk) Source #
Instance details Defined in Agda.Auto.NarrowingSearch type Block (MM a blk) = blk
type UnifiesTo (MM t (RefInfo o)) Source #
Instance details Defined in Agda.Auto.CaseSplit type UnifiesTo (MM t (RefInfo o)) = o
type ReplaceWith (MM t (RefInfo o)) u Source #
Instance details Defined in Agda.Auto.CaseSplit type ReplaceWith (MM t (RefInfo o)) u = ReplaceWith t u

rm :: Empty -> MM a b -> a Source #

type MetaEnv = IO Source #

data MB a blk Source #

Constructors

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

data PB blk Source #

Constructors

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 Source #

Constructors

QPBlocked (BlkInfo blk) (MetaEnv (PB blk))
QPDoubleBlocked (IORef Bool) (MetaEnv (PB blk))

mmcase :: Refinable a blk => MM a blk -> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk) Source #

mmmcase :: MM a blk -> MetaEnv (MB b blk) -> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk) Source #

mmpcase :: Refinable a blk => BlkInfo blk -> MM a blk -> (a -> MetaEnv (PB blk)) -> MetaEnv (PB blk) Source #

doubleblock :: (Refinable a blk, Refinable b blk) => MM a blk -> MM b blk -> MetaEnv (PB blk) -> MetaEnv (PB blk) Source #

mbcase :: MetaEnv (MB a blk) -> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk) Source #

mbpcase :: Prio -> Maybe blk -> MetaEnv (MB a blk) -> (a -> MetaEnv (PB blk)) -> MetaEnv (PB blk) Source #

mmbpcase :: MetaEnv (MB a blk) -> (forall b. Refinable b blk => MM b blk -> MetaEnv (PB blk)) -> (a -> MetaEnv (PB blk)) -> MetaEnv (PB blk) Source #

waitok :: OKHandle blk -> MetaEnv (MB b blk) -> MetaEnv (MB b blk) Source #

mbret :: a -> MetaEnv (MB a blk) Source #

mbfailed :: String -> MetaEnv (MB a blk) Source #

mpret :: Prop blk -> MetaEnv (PB blk) Source #

expandbind :: MM a blk -> MetaEnv (MM a blk) Source #

type HandleSol = IO () Source #

type SRes = Either Bool Int Source #

topSearch :: forall blk. IORef Int -> IORef Int -> HandleSol -> blk -> MetaEnv (PB blk) -> Cost -> Cost -> IO Bool Source #

extractblkinfos :: Metavar a blk -> IO [blk] Source #

recalcs :: [(QPB a blk, Maybe (CTree blk))] -> Undo Bool Source #

seqc :: Undo Bool -> Undo Bool -> Undo Bool Source #

recalc :: (QPB a blk, Maybe (CTree blk)) -> Undo Bool Source #

reccalc :: MetaEnv (PB blk) -> Maybe (CTree blk) -> Undo Bool Source #

calc :: forall blk. MetaEnv (PB blk) -> Maybe (CTree blk) -> Undo (Maybe [OKMeta blk]) Source #

choosePrioMeta :: Bool -> PrioMeta blk -> PrioMeta blk -> PrioMeta blk Source #

propagatePrio :: CTree blk -> Undo [OKMeta blk] Source #

data Choice Source #

Constructors

LeftDisjunct
RightDisjunct

Instances

Instances details

Refinable Choice blk Source #
Instance details Defined in Agda.Auto.NarrowingSearch Methods refinements :: blk -> [blk] -> Metavar Choice blk -> IO [Move' blk Choice] Source #

choose :: MM Choice blk -> Prio -> MetaEnv (PB blk) -> MetaEnv (PB blk) -> MetaEnv (PB blk) Source #