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

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

Refinable OKVal blk

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)

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