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

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

Instances

Trav a blk => Trav [a] blk 
Trav (CAction o) (RefInfo o) 
Trav (CArgList o) (RefInfo o) 
Trav (HNExp o) (RefInfo o) 
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 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 

Fields

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 

Fields

ctpriometa :: IORef (PrioMeta blk)
 
ctsub :: IORef (Maybe (SubConstraints blk))
 
ctparent :: IORef (Maybe (CTree 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

newSubConstraints :: CTree blk -> IO (SubConstraints 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 

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

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) 

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 

Instances

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

printCTree :: CTree blk -> IO ()Source