Safe Haskell	None
Language	Haskell2010

Agda.Auto.NarrowingSearch

Synopsis

Documentation

newtype Prio #

Constructors

Prio
Fields getPrio :: Int

Instances

Eq Prio #
Methods (==) :: Prio -> Prio -> Bool # (/=) :: Prio -> Prio -> Bool #
Num Prio #
Methods (+) :: Prio -> Prio -> Prio # (-) :: Prio -> Prio -> Prio # (*) :: Prio -> Prio -> Prio # negate :: Prio -> Prio # abs :: Prio -> Prio # signum :: Prio -> Prio # fromInteger :: Integer -> Prio #
Ord Prio #
Methods compare :: Prio -> Prio -> Ordering # (<) :: Prio -> Prio -> Bool # (<=) :: Prio -> Prio -> Bool # (>) :: Prio -> Prio -> Bool # (>=) :: Prio -> Prio -> Bool # max :: Prio -> Prio -> Prio # min :: Prio -> Prio -> Prio #

class Trav a blk | a -> blk where #

Minimal complete definition

trav

Methods

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

Instances

Trav a blk => Trav (MM a blk) blk #
Methods trav :: Monad m => (forall b. Trav b blk => MM b blk -> m ()) -> MM a blk -> m () #

data Term blk #

Constructors

Trav a blk => Term a

data Prop blk #

Result of type-checking.

Constructors

OK	Success.
Error String	Definite failure.
AddExtraRef String (Metavar a blk) (Move' 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 #
Methods refinements :: blk -> [blk] -> Metavar OKVal blk -> IO [Move' blk OKVal] #

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 [Move' blk a]
Experimental.

Instances

Eq (Metavar a blk) #
Methods (==) :: Metavar a blk -> Metavar a blk -> Bool # (/=) :: Metavar a blk -> Metavar a blk -> Bool #

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

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

Instances

Eq (PrioMeta blk) #
Methods (==) :: PrioMeta blk -> PrioMeta blk -> Bool # (/=) :: PrioMeta blk -> PrioMeta blk -> Bool #

data Restore #

Constructors

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 #

newtype RefCreateEnv blk a #

Constructors

RefCreateEnv
Fields runRefCreateEnv :: StateT (IORef [SubConstraints blk], Int) IO a

Instances

Monad (RefCreateEnv blk) #
Methods (>>=) :: RefCreateEnv blk a -> (a -> RefCreateEnv blk b) -> RefCreateEnv blk b # (>>) :: RefCreateEnv blk a -> RefCreateEnv blk b -> RefCreateEnv blk b # return :: a -> RefCreateEnv blk a # fail :: String -> RefCreateEnv blk a #
Functor (RefCreateEnv blk) #
Methods fmap :: (a -> b) -> RefCreateEnv blk a -> RefCreateEnv blk b # (<$) :: a -> RefCreateEnv blk b -> RefCreateEnv blk a #
Applicative (RefCreateEnv blk) #
Methods pure :: a -> RefCreateEnv blk a # (<>) :: RefCreateEnv blk (a -> b) -> RefCreateEnv blk a -> RefCreateEnv blk b # liftA2 :: (a -> b -> c) -> RefCreateEnv blk a -> RefCreateEnv blk b -> RefCreateEnv blk c # (>) :: RefCreateEnv blk a -> RefCreateEnv blk b -> RefCreateEnv blk b # (<*) :: RefCreateEnv blk a -> RefCreateEnv blk b -> RefCreateEnv blk a #

newtype Cost #

Constructors

Cost
Fields getCost :: Int

Instances

Eq Cost #
Methods (==) :: Cost -> Cost -> Bool # (/=) :: Cost -> Cost -> Bool #
Num Cost #
Methods (+) :: Cost -> Cost -> Cost # (-) :: Cost -> Cost -> Cost # (*) :: Cost -> Cost -> Cost # negate :: Cost -> Cost # abs :: Cost -> Cost # signum :: Cost -> Cost # fromInteger :: Integer -> Cost #
Ord Cost #
Methods compare :: Cost -> Cost -> Ordering # (<) :: Cost -> Cost -> Bool # (<=) :: Cost -> Cost -> Bool # (>) :: Cost -> Cost -> Bool # (>=) :: Cost -> Cost -> Bool # max :: Cost -> Cost -> Cost # min :: Cost -> Cost -> Cost #

data Move' blk a #

Constructors

Move
Fields moveCost :: Cost moveNext :: RefCreateEnv blk a

class Refinable a blk where #

Minimal complete definition

refinements

Methods

refinements :: blk -> [blk] -> Metavar a blk -> IO [Move' blk a] #

Instances

Refinable Choice blk #
Methods refinements :: blk -> [blk] -> Metavar Choice blk -> IO [Move' blk Choice] #
Refinable OKVal blk #
Methods refinements :: blk -> [blk] -> Metavar OKVal blk -> IO [Move' blk OKVal] #

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

Conversion TOM Clause (Maybe ([Pat O], MExp O)) #
Methods convert :: Clause -> TOM (Maybe ([Pat O], MExp O)) #
Conversion TOM Type (MExp O) #
Methods convert :: Type -> TOM (MExp O) #
Conversion TOM Term (MExp O) #
Methods convert :: Term -> TOM (MExp O) #
Conversion TOM Args (MM (ArgList O) (RefInfo O)) #
Methods convert :: Args -> TOM (MM (ArgList O) (RefInfo O)) #
Replace o (Exp o) (MExp o) #
Methods replace' :: Nat -> MExp o -> Exp o -> Reader (Nat, Nat) (MExp o) #
Conversion TOM [Clause] [([Pat O], MExp O)] #
Methods convert :: [Clause] -> TOM [([Pat O], MExp O)] #
Unify o t => Unify o (MM t (RefInfo o)) #
Methods unify' :: MM t (RefInfo o) -> MM t (RefInfo o) -> StateT (Assignments o) Maybe () # notequal' :: MM t (RefInfo o) -> MM t (RefInfo o) -> ReaderT * (Nat, Nat) (StateT (Assignments o) IO) Bool #
Replace o t u => Replace o (MM t (RefInfo o)) u #
Methods replace' :: Nat -> MExp o -> MM t (RefInfo o) -> Reader (Nat, Nat) u #
Conversion MOT a b => Conversion MOT (MM a (RefInfo O)) b #
Methods convert :: MM a (RefInfo O) -> MOT b #
LocalTerminationEnv (MArgList o) #
Methods sizeAndBoundVars :: MArgList o -> (Sum Nat, [Nat]) #
LocalTerminationEnv (MExp o) #
Methods sizeAndBoundVars :: MExp o -> (Sum Nat, [Nat]) #
Renaming t => Renaming (MM t a) #
Methods renameOffset :: Nat -> (Nat -> Nat) -> MM t a -> MM t a #
FreeVars t => FreeVars (MM t a) #
Methods freeVarsOffset :: Nat -> MM t a -> Set Nat #
ExpandMetas t => ExpandMetas (MM t a) #
Methods expandMetas :: MM t a -> IO (MM t a) #
MetaliseOKH t => MetaliseOKH (MM t a) #
Methods metaliseOKH :: MM t a -> IO (MM t a) #
Lift t => Lift (MM t r) #
Methods lift' :: Nat -> Nat -> MM t r -> MM t r #
Trav a blk => Trav (MM a blk) blk #
Methods trav :: Monad m => (forall b. Trav b blk => MM b blk -> m ()) -> MM a blk -> m () #

rm :: Empty -> MM a b -> a #

type MetaEnv = IO #

data MB a blk #

Constructors

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

data PB blk #

Constructors

NotPB (Prop blk)
Refinable b blk => PBlocked (Metavar b blk) (BlkInfo blk) (MetaEnv (PB blk))
(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 :: 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) -> Cost -> Cost -> 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 #
Methods refinements :: blk -> [blk] -> Metavar Choice blk -> IO [Move' blk Choice] #

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