Agda-2.2.6: 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
And (Maybe [Term blk]) (MetaEnv (PB blk)) (MetaEnv (PB blk))
Or Prio (MetaEnv (PB blk)) (MetaEnv (PB blk))
runProp :: MetaEnv (PB blk) -> MetaEnv ()Source
data Metavar a blk Source
Constructors
Metavar
mbind :: IORef (Maybe a)
mprincipalpresent :: IORef Bool
mobs :: IORef [(QPB a blk, CTree blk)]
mcompoint :: IORef (Maybe (SubConstraints blk))
hequalMetavar :: Metavar a1 blk1 -> Metavar a2 bkl2 -> BoolSource
newMeta :: Maybe (SubConstraints blk) -> 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))
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 (Maybe (SubConstraints blk), Int) IOSource
class Refinable a blk | a -> blk whereSource
Methods
refinements :: blk -> [blk] -> IO [(Int, RefCreateEnv blk a)]Source
printref :: a -> IO StringSource
newPlaceholder :: RefCreateEnv blk (MM a 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
type PrintConstr = MetaEnv StringSource
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) PrintConstr (MetaEnv (PB blk))
forall b . Refinable b blk => PDoubleBlocked (Metavar b blk) (Metavar b blk) (MetaEnv (PB blk))
data QPB b blk Source
Constructors
QPBlocked (BlkInfo blk) PrintConstr (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 -> PrintConstr -> (a -> MetaEnv (PB blk)) -> MetaEnv (PB blk)Source
doubleblock :: Refinable a blk => MM a blk -> MM a 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 -> MetaEnv (MB a blk) -> PrintConstr -> (a -> MetaEnv (PB blk)) -> MetaEnv (PB blk)Source
mmbpcase :: MetaEnv (MB a blk) -> MetaEnv (PB blk) -> (a -> MetaEnv (PB blk)) -> MetaEnv (PB blk)Source
mbret :: a -> MetaEnv (MB a blk)Source
mbfailed :: String -> MetaEnv (MB a blk)Source
mpret :: Prop blk -> MetaEnv (PB blk)Source
type HandleSol = IO ()Source
type HandlePartSol = IO ()Source
type SRes = Either Bool IntSource
topSearch :: forall blk. IORef Int -> IORef Int -> HandleSol -> HandlePartSol -> Bool -> blk -> MetaEnv (PB blk) -> Int -> Int -> IO BoolSource
extractblkinfos :: Metavar a blk -> IO [blk]Source
recalcs :: [(QPB a blk, CTree blk)] -> Undo BoolSource
seqc :: Undo Bool -> Undo Bool -> Undo BoolSource
recalc :: (QPB a blk, CTree blk) -> Undo BoolSource
reccalc :: MetaEnv (PB blk) -> CTree blk -> Undo BoolSource
calc :: forall blk. MetaEnv (PB blk) -> CTree blk -> Undo BoolSource
choosePrioMeta :: Bool -> PrioMeta blk -> PrioMeta blk -> PrioMeta blkSource
propagatePrio :: CTree blk -> Undo ()Source
data Choice Source
Constructors
LeftDisjunct
RightDisjunct
choose :: MM Choice blk -> Prio -> MetaEnv (PB blk) -> MetaEnv (PB blk) -> MetaEnv (PB blk)Source
printCTree :: CTree blk -> IO ()Source
Produced by Haddock version 2.6.0