Agda.Auto.NarrowingSearch

Synopsis

• type Prio = 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) (Int, RefCreateEnv 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 [(Int, RefCreateEnv 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
• type RefCreateEnv blk = StateT (IORef [SubConstraints blk], Int) IO
• data Pair a b = Pair a b
• 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)
• 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) -> 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
  • = LeftDisjunct
  • | RightDisjunct
• choose :: MM Choice blk -> Prio -> MetaEnv (PB blk) -> MetaEnv (PB blk) -> MetaEnv (PB blk)

Documentation