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

Safe HaskellSafe-Inferred
LanguageHaskell98

Agda.Auto.NarrowingSearch

Synopsis

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

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

Constructors

OKVal 

Instances

type OKHandle blk = MM OKVal blk

type OKMeta blk = Metavar OKVal blk

data Metavar a blk

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