| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Auto.NarrowingSearch
Synopsis
- newtype Prio = Prio {}
- class Trav a where
- type TravWith a blk = (Trav a, Block a ~ blk)
- data Term blk = TravWith a blk => Term a
- data Prop blk
- data OKVal = OKVal
- type OKHandle blk = MM OKVal blk
- type OKMeta blk = Metavar OKVal blk
- data Metavar a blk = Metavar {}
- 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 {}
- data SubConstraints blk = SubConstraints {}
- newCTree :: Maybe (CTree blk) -> IO (CTree blk)
- newSubConstraints :: CTree blk -> IO (SubConstraints blk)
- data PrioMeta blk
- 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 {}
- data Move' blk a = Move {
- moveCost :: Cost
- moveNext :: RefCreateEnv blk a
- class Refinable a blk where
- refinements :: blk -> [blk] -> Metavar a blk -> IO [Move' blk a]
- 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
- rm :: Empty -> MM a b -> a
- type MetaEnv = IO
- data MB a blk
- data PB blk
- data QPB b 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 :: 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 :: 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
- choose :: MM Choice blk -> Prio -> MetaEnv (PB blk) -> MetaEnv (PB blk) -> MetaEnv (PB blk)
Documentation
Methods
trav :: Monad m => (forall b. TravWith b (Block a) => MM b (Block b) -> m ()) -> a -> m () Source #
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 |
| 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. |
Constructors
| OKVal |
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
| |
data SubConstraints blk Source #
newSubConstraints :: CTree blk -> IO (SubConstraints blk) Source #
ureadIORef :: IORef a -> Undo a Source #
uwriteIORef :: IORef a -> a -> Undo () Source #
umodifyIORef :: IORef a -> (a -> a) -> Undo () Source #
ureadmodifyIORef :: IORef a -> (a -> a) -> Undo a Source #
newtype RefCreateEnv blk a Source #
Constructors
| RefCreateEnv | |
Fields
| |
Instances
| Applicative (RefCreateEnv blk) Source # | |
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 # | |
| Functor (RefCreateEnv blk) Source # | |
Defined in Agda.Auto.NarrowingSearch Methods fmap :: (a -> b) -> RefCreateEnv blk a -> RefCreateEnv blk b # (<$) :: a -> RefCreateEnv blk b -> RefCreateEnv blk a # | |
| Monad (RefCreateEnv blk) Source # | |
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 # | |
class Refinable a blk where Source #
Instances
newPlaceholder :: RefCreateEnv blk (MM a blk) Source #
newOKHandle :: RefCreateEnv blk (OKHandle blk) Source #
dryInstantiate :: RefCreateEnv blk a -> IO a Source #
Instances
mmmcase :: 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 #
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 #
topSearch :: IORef Int -> IORef Int -> HandleSol -> blk -> MetaEnv (PB blk) -> Cost -> Cost -> IO Bool Source #
extractblkinfos :: Metavar a blk -> IO [blk] Source #
Constructors
| LeftDisjunct | |
| RightDisjunct |