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

Safe HaskellSafe-Inferred

Agda.Auto.NarrowingSearch

Synopsis

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

Constructors

forall a . Trav a blk => Term a 

data Prop blk Source

Result of type-checking.

Constructors

OK

Success.

Error String

Definite failure.

forall a . AddExtraRef String (Metavar a blk) (Int, RefCreateEnv blk a)

Experimental.

And (Maybe [Term blk]) (MetaEnv (PB blk)) (MetaEnv (PB blk))

Parallel conjunction of constraints.

Sidecondition (MetaEnv (PB blk)) (MetaEnv (PB blk))

Experimental, related to mcompoint. First arg is sidecondition.

Or Prio (MetaEnv (PB blk)) (MetaEnv (PB blk))

Forking proof on something that is not part of the term language. E.g. whether a term will reduce or not.

ConnectHandle (OKHandle blk) (MetaEnv (PB blk))

Obsolete.

data OKVal Source

Constructors

OKVal 

Instances

type OKHandle blk = MM OKVal blkSource

type OKMeta blk = Metavar OKVal blkSource

data Metavar a blk Source

Agsy's meta variables.

a the type of the metavariable (what it can be instantiated with). blk the search control information (e.g. the scope of the meta).

Constructors

Metavar 

Fields

mbind :: IORef (Maybe a)

Maybe an instantiation (refinement). It is usually shallow, i.e., just one construct(or) with arguments again being metas.

mprincipalpresent :: IORef Bool

Does this meta block a principal constraint (i.e., a type-checking constraint).

mobs :: IORef [(QPB a blk, Maybe (CTree blk))]

List of observers, i.e., constraints blocked by this meta.

mcompoint :: IORef [SubConstraints blk]

Used for experiments with independence of subproofs.

mextrarefs :: IORef [(Int, RefCreateEnv blk a)]

Experimental.

Instances

Eq (Metavar a blk) 

hequalMetavar :: Metavar a1 blk1 -> Metavar a2 bkl2 -> BoolSource

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

initMeta :: 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))
 
cthandles :: IORef [OKMeta 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

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 

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 (IORef [SubConstraints blk], Int) IOSource

data Pair a b Source

Constructors

Pair a b 

class Refinable a blk whereSource

Methods

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

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

data MM a blk Source

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

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

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)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 -> (a -> MetaEnv (PB blk)) -> MetaEnv (PB blk)Source

doubleblock :: (Refinable a blk, Refinable b blk) => MM a blk -> MM b 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 -> Maybe blk -> MetaEnv (MB a blk) -> (a -> MetaEnv (PB blk)) -> MetaEnv (PB blk)Source

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

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

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

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

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

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

type HandleSol = IO ()Source

type SRes = Either Bool IntSource

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

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

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

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

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

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

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

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

data Choice Source

Instances

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