Safe Haskell	None
Language	Haskell2010

Agda.Auto.NarrowingSearch

Synopsis

newtype Prio = Prio {
- getPrio :: Int
}
class Trav a blk | a -> blk where
data Term blk = Trav a blk => Term a
data Prop blk
- = OK
- | Error String
- | AddExtraRef String (Metavar a blk) (Move' 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 = OKVal
type OKHandle blk = MM OKVal blk
type OKMeta blk = Metavar OKVal blk
data Metavar a blk = Metavar {
- mbind :: IORef (Maybe a)
- mprincipalpresent :: IORef Bool
- mobs :: IORef [(QPB a blk, Maybe (CTree blk))]
- mcompoint :: IORef [SubConstraints blk]
- mextrarefs :: IORef [Move' blk a]
}
hequalMetavar :: Metavar a1 blk1 -> Metavar a2 bkl2 -> Bool
newMeta :: IORef [SubConstraints blk] -> IO (Metavar a blk)
initMeta :: IO (Metavar a blk)
data CTree blk = CTree {
- ctpriometa :: IORef (PrioMeta blk)
- ctsub :: IORef (Maybe (SubConstraints blk))
- ctparent :: IORef (Maybe (CTree blk))
- cthandles :: IORef [OKMeta blk]
}
data SubConstraints blk = SubConstraints {
- 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
- = Refinable a blk => PrioMeta Prio (Metavar a blk)
- | NoPrio Bool
data Restore = 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 = RefCreateEnv {
- runRefCreateEnv :: StateT (IORef [SubConstraints blk], Int) IO a
}
newtype Cost = Cost {
- getCost :: Int
}
data Move' blk a = Move {
- moveCost :: Cost
- moveNext :: RefCreateEnv blk a
}
class Refinable a blk where
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
- = NotM a
- | Meta (Metavar a blk)
rm :: Empty -> MM a b -> a
type MetaEnv = IO
data MB a blk
- = NotB a
- | Refinable b blk => Blocked (Metavar b blk) (MetaEnv (MB a blk))
- | Failed String
data PB blk
- = 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
- = 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
- = LeftDisjunct
- | RightDisjunct
choose :: MM Choice blk -> Prio -> MetaEnv (PB blk) -> MetaEnv (PB blk) -> MetaEnv (PB blk)

Documentation

newtype Prio #

Constructors

Prio
Fields getPrio :: Int

Instances

Eq Prio #
Instance details Defined in Agda.Auto.NarrowingSearch Methods (==) :: Prio -> Prio -> Bool # (/=) :: Prio -> Prio -> Bool #
Num Prio #
Instance details Defined in Agda.Auto.NarrowingSearch Methods (+) :: Prio -> Prio -> Prio # (-) :: Prio -> Prio -> Prio # (*) :: Prio -> Prio -> Prio # negate :: Prio -> Prio # abs :: Prio -> Prio # signum :: Prio -> Prio # fromInteger :: Integer -> Prio #
Ord Prio #
Instance details Defined in Agda.Auto.NarrowingSearch 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 [a] blk #
Instance details Defined in Agda.Auto.SearchControl Methods trav :: Monad m => (forall b. Trav b blk => MM b blk -> m ()) -> [a] -> m () #
Trav (ArgList o) (RefInfo o) #
Instance details Defined in Agda.Auto.SearchControl Methods trav :: Monad m => (forall b. Trav b (RefInfo o) => MM b (RefInfo o) -> m ()) -> ArgList o -> m () #
Trav (Exp o) (RefInfo o) #
Instance details Defined in Agda.Auto.SearchControl Methods trav :: Monad m => (forall b. Trav b (RefInfo o) => MM b (RefInfo o) -> m ()) -> Exp o -> m () #
Trav a blk => Trav (MM a blk) blk #
Instance details Defined in Agda.Auto.NarrowingSearch Methods trav :: Monad m => (forall b. Trav b blk => MM b blk -> m ()) -> MM a blk -> m () #
Trav (MId, CExp o) (RefInfo o) #
Instance details Defined in Agda.Auto.SearchControl Methods trav :: Monad m => (forall b. Trav b (RefInfo o) => MM b (RefInfo o) -> m ()) -> (MId, CExp o) -> m () #
Trav (TrBr a o) (RefInfo o) #
Instance details Defined in Agda.Auto.SearchControl Methods trav :: Monad m => (forall b. Trav b (RefInfo o) => MM b (RefInfo o) -> m ()) -> TrBr a o -> 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 #
Instance details Defined in Agda.Auto.NarrowingSearch 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) #
Instance details Defined in Agda.Auto.NarrowingSearch 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) #
Instance details Defined in Agda.Auto.NarrowingSearch 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) #
Instance details Defined in Agda.Auto.NarrowingSearch 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) #
Instance details Defined in Agda.Auto.NarrowingSearch Methods fmap :: (a -> b) -> RefCreateEnv blk a -> RefCreateEnv blk b # (<$) :: a -> RefCreateEnv blk b -> RefCreateEnv blk a #
Applicative (RefCreateEnv blk) #
Instance details Defined in Agda.Auto.NarrowingSearch 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 #
Instance details Defined in Agda.Auto.NarrowingSearch Methods (==) :: Cost -> Cost -> Bool # (/=) :: Cost -> Cost -> Bool #
Num Cost #
Instance details Defined in Agda.Auto.NarrowingSearch Methods (+) :: Cost -> Cost -> Cost # (-) :: Cost -> Cost -> Cost # (*) :: Cost -> Cost -> Cost # negate :: Cost -> Cost # abs :: Cost -> Cost # signum :: Cost -> Cost # fromInteger :: Integer -> Cost #
Ord Cost #
Instance details Defined in Agda.Auto.NarrowingSearch 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 #
Instance details Defined in Agda.Auto.NarrowingSearch Methods refinements :: blk -> [blk] -> Metavar Choice blk -> IO [Move' blk Choice] #
Refinable OKVal blk #
Instance details Defined in Agda.Auto.NarrowingSearch Methods refinements :: blk -> [blk] -> Metavar OKVal blk -> IO [Move' blk OKVal] #
Refinable (ICExp o) (RefInfo o) #
Instance details Defined in Agda.Auto.SearchControl Methods refinements :: RefInfo o -> [RefInfo o] -> Metavar (ICExp o) (RefInfo o) -> IO [Move' (RefInfo o) (ICExp o)] #
Refinable (ArgList o) (RefInfo o) #
Instance details Defined in Agda.Auto.SearchControl Methods refinements :: RefInfo o -> [RefInfo o] -> Metavar (ArgList o) (RefInfo o) -> IO [Move' (RefInfo o) (ArgList o)] #
Refinable (Exp o) (RefInfo o) #
Instance details Defined in Agda.Auto.SearchControl Methods refinements :: RefInfo o -> [RefInfo o] -> Metavar (Exp o) (RefInfo o) -> IO [Move' (RefInfo o) (Exp o)] #
Refinable (ConstRef o) (RefInfo o) #
Instance details Defined in Agda.Auto.SearchControl Methods refinements :: RefInfo o -> [RefInfo o] -> Metavar (ConstRef o) (RefInfo o) -> IO [Move' (RefInfo o) (ConstRef 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

Conversion TOM Clause (Maybe ([Pat O], MExp O)) #
Instance details Defined in Agda.Auto.Convert Methods convert :: Clause -> TOM (Maybe ([Pat O], MExp O)) #
Conversion TOM Type (MExp O) #
Instance details Defined in Agda.Auto.Convert Methods convert :: Type -> TOM (MExp O) #
Conversion TOM Term (MExp O) #
Instance details Defined in Agda.Auto.Convert Methods convert :: Term -> TOM (MExp O) #
Conversion TOM Args (MM (ArgList O) (RefInfo O)) #
Instance details Defined in Agda.Auto.Convert Methods convert :: Args -> TOM (MM (ArgList O) (RefInfo O)) #
Replace o (Exp o) (MExp o) #
Instance details Defined in Agda.Auto.CaseSplit Methods replace' :: Nat -> MExp o -> Exp o -> Reader (Nat, Nat) (MExp o) #
Conversion TOM [Clause] [([Pat O], MExp O)] #
Instance details Defined in Agda.Auto.Convert Methods convert :: [Clause] -> TOM [([Pat O], MExp O)] #
Unify o t => Unify o (MM t (RefInfo o)) #
Instance details Defined in Agda.Auto.CaseSplit 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 #
Instance details Defined in Agda.Auto.CaseSplit Methods replace' :: Nat -> MExp o -> MM t (RefInfo o) -> Reader (Nat, Nat) u #
Conversion MOT a b => Conversion MOT (MM a (RefInfo O)) b #
Instance details Defined in Agda.Auto.Convert Methods convert :: MM a (RefInfo O) -> MOT b #
LocalTerminationEnv (MArgList o) #
Instance details Defined in Agda.Auto.CaseSplit Methods sizeAndBoundVars :: MArgList o -> (Sum Nat, [Nat]) #
LocalTerminationEnv (MExp o) #
Instance details Defined in Agda.Auto.CaseSplit Methods sizeAndBoundVars :: MExp o -> (Sum Nat, [Nat]) #
Refinable (ICExp o) (RefInfo o) #
Instance details Defined in Agda.Auto.SearchControl Methods refinements :: RefInfo o -> [RefInfo o] -> Metavar (ICExp o) (RefInfo o) -> IO [Move' (RefInfo o) (ICExp o)] #
Renaming t => Renaming (MM t a) #
Instance details Defined in Agda.Auto.Syntax Methods renameOffset :: Nat -> (Nat -> Nat) -> MM t a -> MM t a #
FreeVars t => FreeVars (MM t a) #
Instance details Defined in Agda.Auto.Syntax Methods freeVarsOffset :: Nat -> MM t a -> Set Nat #
ExpandMetas t => ExpandMetas (MM t a) #
Instance details Defined in Agda.Auto.Syntax Methods expandMetas :: MM t a -> IO (MM t a) #
MetaliseOKH t => MetaliseOKH (MM t a) #
Instance details Defined in Agda.Auto.Syntax Methods metaliseOKH :: MM t a -> IO (MM t a) #
Lift t => Lift (MM t r) #
Instance details Defined in Agda.Auto.CaseSplit Methods lift' :: Nat -> Nat -> MM t r -> MM t r #
Trav a blk => Trav (MM a blk) blk #
Instance details Defined in Agda.Auto.NarrowingSearch Methods trav :: Monad m => (forall b. Trav b blk => MM b blk -> m ()) -> MM a blk -> m () #
Trav (MId, CExp o) (RefInfo o) #
Instance details Defined in Agda.Auto.SearchControl Methods trav :: Monad m => (forall b. Trav b (RefInfo o) => MM b (RefInfo o) -> m ()) -> (MId, CExp o) -> 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 #
Instance details Defined in Agda.Auto.NarrowingSearch 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) #