| 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

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

Instances

Eq (PrioMeta blk)

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

Instances

Refinable Choice blk
Refinable (ArgList o) (RefInfo o)
Refinable (ArgList o) (RefInfo o)
Refinable (Exp o) (RefInfo o)
Refinable (Exp o) (RefInfo o)

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

Instances

Trav a blk => Trav (MM a blk) 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 |

Instances

Refinable Choice blk

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