Agda-2.2.10: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.Auto.NarrowingSearch
Documentation
type Prio = IntSource
class Trav a blk | a -> blk whereSource
Methods
traverse :: Monad m => (forall b. Trav b blk => MM b blk -> m ()) -> a -> m ()Source
data Term blk Source
Constructors
forall a . Trav a blk => Term a
data Prop blk Source
Constructors
OK
Error String
forall a . AddExtraRef String (Metavar a blk) (Int, RefCreateEnv 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 Source
Constructors
OKVal
type OKHandle blk = MM OKVal blkSource
type OKMeta blk = Metavar OKVal blkSource
data Metavar a blk Source
Constructors
Metavar
mbind :: IORef (Maybe a)
mprincipalpresent :: IORef Bool
mobs :: IORef [(QPB a blk, Maybe (CTree blk))]
mcompoint :: IORef [SubConstraints blk]
mextrarefs :: IORef [(Int, RefCreateEnv blk a)]
hequalMetavar :: Metavar a1 blk1 -> Metavar a2 bkl2 -> BoolSource
newMeta :: IORef [SubConstraints blk] -> IO (Metavar a blk)Source
initMeta :: IO (Metavar a blk)Source
data CTree blk Source
Constructors
CTree
ctpriometa :: IORef (PrioMeta blk)
ctsub :: IORef (Maybe (SubConstraints blk))
ctparent :: IORef (Maybe (CTree blk))
cthandles :: IORef [OKMeta blk]
data SubConstraints blk Source
Constructors
SubConstraints
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
data Restore Source
Constructors
forall a . Restore (IORef a) a
type Undo = StateT [Restore] IOSource
ureadIORef :: IORef a -> Undo aSource
uwriteIORef :: IORef a -> a -> Undo ()Source
umodifyIORef :: IORef a -> (a -> a) -> Undo ()Source
ureadmodifyIORef :: IORef a -> (a -> a) -> Undo aSource
runUndo :: Undo a -> IO aSource
type RefCreateEnv blk = StateT (IORef [SubConstraints blk], Int) IOSource
data Pair a b Source
Constructors
Pair a b
class Refinable a blk | a -> blk whereSource
Methods
refinements :: blk -> [blk] -> Metavar a blk -> IO [(Int, RefCreateEnv blk a)]Source
newPlaceholder :: RefCreateEnv blk (MM a blk)Source
newOKHandle :: RefCreateEnv blk (OKHandle blk)Source
dryInstantiate :: RefCreateEnv blk a -> IO aSource
type BlkInfo blk = (Bool, Prio, Maybe blk)Source
data MM a blk Source
Constructors
NotM a
Meta (Metavar a blk)
type MetaEnv = IOSource
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 :: Refinable a blk => 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 IntSource
topSearch :: forall blk. IORef Int -> IORef Int -> HandleSol -> blk -> MetaEnv (PB blk) -> Int -> Int -> IO BoolSource
extractblkinfos :: Metavar a blk -> IO [blk]Source
recalcs :: [(QPB a blk, Maybe (CTree blk))] -> Undo BoolSource
seqc :: Undo Bool -> Undo Bool -> Undo BoolSource
recalc :: (QPB a blk, Maybe (CTree blk)) -> Undo BoolSource
reccalc :: MetaEnv (PB blk) -> Maybe (CTree blk) -> Undo BoolSource
calc :: forall blk. MetaEnv (PB blk) -> Maybe (CTree blk) -> Undo (Maybe [OKMeta blk])Source
choosePrioMeta :: Bool -> PrioMeta blk -> PrioMeta blk -> PrioMeta blkSource
propagatePrio :: CTree blk -> Undo [OKMeta blk]Source
data Choice Source
Constructors
LeftDisjunct
RightDisjunct
choose :: MM Choice blk -> Prio -> MetaEnv (PB blk) -> MetaEnv (PB blk) -> MetaEnv (PB blk)Source
Produced by Haddock version 2.6.1