Agda-2.2.6: A dependently typed functional programming language and proof assistant Source code Contents Index

Agda.Auto.NarrowingSearch

Documentation

type Prio = Int Source

class Trav a blk | a -> blk where Source

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 -> Bool Source

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] IO Source

ureadIORef :: IORef a -> Undo a Source

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

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

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

runUndo :: Undo a -> IO a Source

type RefCreateEnv blk = StateT (Maybe (SubConstraints blk), Int) IO Source

class Refinable a blk | a -> blk where Source

Methods refinements :: blk -> [blk] -> IO [(Int, RefCreateEnv blk a)] Source printref :: a -> IO String Source

newPlaceholder :: RefCreateEnv blk (MM a blk) Source

dryInstantiate :: RefCreateEnv blk a -> IO a Source

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

data MM a blk Source

Constructors NotM a Meta (Metavar a blk)

type MetaEnv = IO Source

type PrintConstr = MetaEnv String Source

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 Int Source

topSearch :: forall blk. IORef Int -> IORef Int -> HandleSol -> HandlePartSol -> Bool -> blk -> MetaEnv (PB blk) -> Int -> Int -> IO Bool Source

extractblkinfos :: Metavar a blk -> IO [blk] Source

recalcs :: [(QPB a blk, CTree blk)] -> Undo Bool Source

seqc :: Undo Bool -> Undo Bool -> Undo Bool Source

recalc :: (QPB a blk, CTree blk) -> Undo Bool Source

reccalc :: MetaEnv (PB blk) -> CTree blk -> Undo Bool Source

calc :: forall blk. MetaEnv (PB blk) -> CTree blk -> Undo Bool Source

choosePrioMeta :: Bool -> PrioMeta blk -> PrioMeta blk -> PrioMeta blk Source

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