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
show/hide Instances
Trav a blk => Trav ([] a) blk
Trav (CAction o) (RefInfo o)
Trav (CAction o) (RefInfo o)
Trav (CArgList o) (RefInfo o)
Trav (CArgList o) (RefInfo o)
Trav (HNExp o) (RefInfo o)
Trav (HNExp o) (RefInfo o)
Trav (ArgList o) (RefInfo o)
Trav (ArgList o) (RefInfo o)
Trav (Exp o) (RefInfo o)
Trav (Exp o) (RefInfo o)
Trav a blk => Trav (MM a blk) blk
Trav ((,) MId (CExp o)) (RefInfo o)
Trav ((,) MId (CExp o)) (RefInfo o)
Trav a (RefInfo o) => Trav (Clos a o) (RefInfo o)
Trav a (RefInfo o) => Trav (Clos a o) (RefInfo o)
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
show/hide Instances
Eq (PrioMeta blk)
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
show/hide Instances
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)
show/hide Instances
Trav a blk => Trav (MM a blk) 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
show/hide Instances
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.4.2