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

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

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)

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 

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

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

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

runUndo :: Undo a -> IO a

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

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

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

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

Instances

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