Agda-2.6.0.1: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.Auto.NarrowingSearch

Synopsis

- newtype Prio = Prio {
  - getPrio :: Int
  }
- class Trav a blk | a -> blk where
  - trav :: Monad m => (forall b. Trav b blk => MM b blk -> m ()) -> a -> m ()
- data Term blk = Trav a blk => Term a
- data Prop blk
  - = OK
  - | Error String
  - | 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
  - = Refinable a blk => PrioMeta Prio (Metavar a blk)
  - | NoPrio Bool
- data Restore = 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
  - | Refinable b blk => Blocked (Metavar b blk) (MetaEnv (MB a blk))
  - | Failed String
- data PB blk
  - = NotPB (Prop blk)
  - | Refinable b blk => PBlocked (Metavar b blk) (BlkInfo blk) (MetaEnv (PB blk))
  - | (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

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

class Trav a blk | a -> blk where Source #

Methods

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

Instances

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

data Term blk Source #

Constructors

Trav a blk => Term a |

data Prop blk Source #

Result of type-checking.

Constructors

OK | Success.
Error String | Definite failure.
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

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

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

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

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

Instances

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

data Restore Source #

Constructors

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

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

Instance details

Defined in Agda.Auto.NarrowingSearch

Methods

pure :: a -> RefCreateEnv blk a Source #

(<*>) :: RefCreateEnv blk (a -> b) -> RefCreateEnv blk a -> RefCreateEnv blk b Source #

liftA2 :: (a -> b -> c) -> RefCreateEnv blk a -> RefCreateEnv blk b -> RefCreateEnv blk c Source #

(*>) :: RefCreateEnv blk a -> RefCreateEnv blk b -> RefCreateEnv blk b Source #

(<*) :: RefCreateEnv blk a -> RefCreateEnv blk b -> RefCreateEnv blk a Source #

newtype Cost Source #

Constructors

Cost |

Fields

- getCost :: Int

Instances

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

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

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

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 #
Replace o (Exp o) (MExp o) Source # |
Instance details Defined in Agda.Auto.CaseSplit Methods replace' :: Nat -> MExp o -> Exp o -> Reader (Nat, Nat) (MExp 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 #
Unify o t => Unify o (MM t (RefInfo o)) Source # |
Instance details Defined in Agda.Auto.CaseSplit Methods unify' :: MM t (RefInfo o) -> MM t (RefInfo o) -> StateT (Assignments o) Maybe () Source # notequal' :: MM t (RefInfo o) -> MM t (RefInfo o) -> ReaderT (Nat, Nat) (StateT (Assignments o) IO) Bool Source #
Replace o t u => Replace o (MM t (RefInfo o)) u Source # |
Instance details Defined in Agda.Auto.CaseSplit Methods replace' :: Nat -> MExp o -> MM t (RefInfo o) -> Reader (Nat, Nat) u 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 #
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 #
Trav a blk => Trav (MM a blk) blk Source # |
Instance details Defined in Agda.Auto.NarrowingSearch Methods trav :: Monad m => (forall b. Trav b blk => MM b blk -> m ()) -> MM a blk -> m () Source #
Trav (MId, CExp o) (RefInfo o) Source # |
Instance details Defined in Agda.Auto.SearchControl Methods trav :: Monad m => (forall b. Trav b (RefInfo o) => MM b (RefInfo o) -> m ()) -> (MId, CExp o) -> m () Source #

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

type MetaEnv = IO Source #

data MB a blk Source #

Constructors

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

data PB blk Source #

Constructors

NotPB (Prop blk) |
Refinable b blk => PBlocked (Metavar b blk) (BlkInfo blk) (MetaEnv (PB blk)) |
(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

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 #