Safe Haskell | Safe-Inferred |
---|
Agda.Auto.NarrowingSearch
Documentation
class Trav a blk | a -> blk where
data Prop blk
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 Metavar a blk
Constructors
Metavar | |
Fields
|
hequalMetavar :: Metavar a1 blk1 -> Metavar a2 bkl2 -> Bool
newMeta :: IORef [SubConstraints blk] -> IO (Metavar a blk)
data CTree blk
data SubConstraints blk
newSubConstraints :: CTree blk -> IO (SubConstraints blk)
data PrioMeta blk
ureadIORef :: IORef a -> Undo a
uwriteIORef :: IORef a -> a -> Undo ()
umodifyIORef :: IORef a -> (a -> a) -> Undo ()
ureadmodifyIORef :: IORef a -> (a -> a) -> Undo a
type RefCreateEnv blk = StateT (IORef [SubConstraints blk], Int) IO
class Refinable a blk | a -> blk where
Methods
refinements :: blk -> [blk] -> Metavar a blk -> IO [(Int, RefCreateEnv blk a)]
newPlaceholder :: RefCreateEnv blk (MM a blk)
newOKHandle :: RefCreateEnv blk (OKHandle blk)
dryInstantiate :: RefCreateEnv blk a -> IO a
data MM a blk
data MB a blk
data PB blk
data QPB b blk
mmmcase :: Refinable a blk => 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)
mmbpcase :: MetaEnv (MB a blk) -> (forall b. Refinable b blk => MM b blk -> MetaEnv (PB blk)) -> (a -> MetaEnv (PB blk)) -> MetaEnv (PB blk)
expandbind :: MM a blk -> MetaEnv (MM a blk)
topSearch :: forall blk. IORef Int -> IORef Int -> HandleSol -> blk -> MetaEnv (PB blk) -> Int -> Int -> IO Bool
extractblkinfos :: Metavar a blk -> IO [blk]
choosePrioMeta :: Bool -> PrioMeta blk -> PrioMeta blk -> PrioMeta blk
propagatePrio :: CTree blk -> Undo [OKMeta blk]