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

Safe Haskell | Safe-Infered

Agda.Auto.NarrowingSearch

# Documentation

type Prio = Int

class Trav a blk | a -> blk where

Methods

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

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

Constructors

forall a . Trav a blk => Term a |

data Prop blk

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

Constructors

OKVal |

Instances

Refinable OKVal blk |

type OKHandle blk = MM OKVal blk

type OKMeta blk = Metavar OKVal blk

data Metavar a blk

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

newMeta :: IORef [SubConstraints blk] -> IO (Metavar a blk)

initMeta :: IO (Metavar a blk)

data CTree blk

Constructors

CTree |

Fields

ctpriometa :: IORef (PrioMeta blk)
ctsub :: IORef (Maybe (SubConstraints blk))
ctparent :: IORef (Maybe (CTree blk))
cthandles :: IORef [OKMeta blk]

data SubConstraints blk

Constructors

SubConstraints |

Fields

scflip :: IORef Bool
sccomcount :: IORef Int
scsub1 :: CTree blk
scsub2 :: CTree blk

newCTree :: Maybe (CTree blk) -> IO (CTree blk)

newSubConstraints :: CTree blk -> IO (SubConstraints blk)

data PrioMeta blk

Constructors

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

Instances

Eq (PrioMeta blk) |

data Restore

Constructors

forall a . Restore (IORef a) a |

type Undo = StateT [Restore] IO

ureadIORef :: IORef a -> Undo a

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

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

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

runUndo :: Undo a -> IO a

type RefCreateEnv blk = StateT (IORef [SubConstraints blk], Int) IO

data Pair a b

Constructors

Pair a b |

class Refinable a blk | a -> blk where

Methods

refinements :: blk -> [blk] -> Metavar a blk -> IO [(Int, RefCreateEnv blk a)]

Instances

Refinable Choice blk |
Refinable OKVal blk |
Refinable (ICExp o) (RefInfo o) |
Refinable (ArgList o) (RefInfo o) |
Refinable (Exp o) (RefInfo o) |
Refinable (ConstRef o) (RefInfo o) |

newPlaceholder :: RefCreateEnv blk (MM a blk)

newOKHandle :: RefCreateEnv blk (OKHandle blk)

dryInstantiate :: RefCreateEnv blk a -> IO a

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

data MM a blk

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

type MetaEnv = IO

data MB a blk

Constructors

NotB a |
forall b . Refinable b blk => Blocked (Metavar b blk) (MetaEnv (MB a blk)) |
Failed String |

data PB blk

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

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)

mmmcase :: Refinable a blk => MM a blk -> MetaEnv (MB b blk) -> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)

mmpcase :: Refinable a blk => BlkInfo blk -> MM a blk -> (a -> MetaEnv (PB blk)) -> MetaEnv (PB blk)

doubleblock :: (Refinable a blk, Refinable b blk) => MM a blk -> MM b blk -> MetaEnv (PB blk) -> MetaEnv (PB blk)

mbcase :: MetaEnv (MB a blk) -> (a -> MetaEnv (MB b blk)) -> MetaEnv (MB b blk)

mbpcase :: Prio -> Maybe blk -> MetaEnv (MB a blk) -> (a -> MetaEnv (PB blk)) -> MetaEnv (PB blk)

mmbpcase :: MetaEnv (MB a blk) -> (forall b. Refinable b blk => MM b blk -> MetaEnv (PB blk)) -> (a -> MetaEnv (PB blk)) -> MetaEnv (PB blk)

waitok :: OKHandle blk -> MetaEnv (MB b blk) -> MetaEnv (MB b blk)

mbret :: a -> MetaEnv (MB a blk)

mbfailed :: String -> MetaEnv (MB a blk)

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

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

type HandleSol = IO ()

type SRes = Either Bool Int

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

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

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

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

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

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

calc :: forall blk. MetaEnv (PB blk) -> Maybe (CTree blk) -> Undo (Maybe [OKMeta blk])

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

propagatePrio :: CTree blk -> Undo [OKMeta blk]

data Choice

Constructors

LeftDisjunct |
RightDisjunct |

Instances

Refinable Choice blk |

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