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

Agda.Auto.NarrowingSearch

Documentation

class Trav a blk | a -> blk whereSource

Methods

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

Instances

Trav a blk => Trav [a] blk 
Trav (ArgList o) (RefInfo o) 
Trav (Exp o) (RefInfo o) 
Trav a blk => Trav (MM a blk) blk 
Trav (MId, CExp o) (RefInfo o) 
Trav (TrBr a o) (RefInfo o) 

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 

Instances

type OKHandle blk = MM OKVal blkSource

type OKMeta blk = Metavar OKVal blkSource

data Metavar a blk Source

Constructors

Metavar 

Fields

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)]
 

Instances

Eq (Metavar a blk) 

hequalMetavar :: Metavar a1 blk1 -> Metavar a2 bkl2 -> BoolSource

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

data PrioMeta blk Source

Constructors

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

Instances

Eq (PrioMeta blk) 

data Restore Source

Constructors

forall a . Restore (IORef a) a 

umodifyIORef :: IORef a -> (a -> a) -> Undo ()Source

ureadmodifyIORef :: IORef a -> (a -> a) -> Undo aSource

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

type BlkInfo blk = (Bool, Prio, Maybe blk)Source

data MM a blk Source

Constructors

NotM a 
Meta (Metavar a blk) 

Instances

Refinable (ICExp o) (RefInfo o) 
Trav a blk => Trav (MM a blk) blk 
Trav (MId, CExp o) (RefInfo o) 

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

mpret :: Prop blk -> MetaEnv (PB blk)Source

expandbind :: MM a blk -> MetaEnv (MM a blk)Source

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

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

data Choice Source

Instances

choose :: MM Choice blk -> Prio -> MetaEnv (PB blk) -> MetaEnv (PB blk) -> MetaEnv (PB blk)Source