Agda.Auto.NarrowingSearch

Documentation

newtype Prio

Constructors

Prio

Fields

• getPrio :: Int

Instances

Num Prio

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

Eq Prio

Defined in Agda.Auto.NarrowingSearch

Methods

(==) :: Prio -> Prio -> Bool

(/=) :: Prio -> Prio -> Bool

Ord Prio

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 where

Associated Types

type Block a

Methods

trav :: Monad m => (forall b. TravWith b (Block a) => MM b (Block b) -> m ()) -> a -> m ()

Instances

Trav (ArgList o)

Defined in Agda.Auto.SearchControl

Associated Types

type Block (ArgList o)

Methods

trav :: Monad m => (forall b. TravWith b (Block (ArgList o)) => MM b (Block b) -> m ()) -> ArgList o -> m ()

Trav (Exp o)

Defined in Agda.Auto.SearchControl

Associated Types

type Block (Exp o)

Methods

trav :: Monad m => (forall b. TravWith b (Block (Exp o)) => MM b (Block b) -> m ()) -> Exp o -> m ()

Trav a => Trav [a]

Defined in Agda.Auto.SearchControl

Associated Types

type Block [a]

Methods

trav :: Monad m => (forall b. TravWith b (Block [a]) => MM b (Block b) -> m ()) -> [a] -> m ()

TravWith a blk => Trav (MM a blk)

Defined in Agda.Auto.NarrowingSearch

Associated Types

type Block (MM a blk)

Methods

trav :: Monad m => (forall b. TravWith b (Block (MM a blk)) => MM b (Block b) -> m ()) -> MM a blk -> m ()

Trav (TrBr a o)

Defined in Agda.Auto.SearchControl

Associated Types

type Block (TrBr a o)

Methods

trav :: Monad m => (forall b. TravWith b (Block (TrBr a o)) => MM b (Block b) -> m ()) -> TrBr a o -> m ()

Trav (MId, CExp o)

Defined in Agda.Auto.SearchControl

Associated Types

type Block (MId, CExp o)

Methods

trav :: Monad m => (forall b. TravWith b (Block (MId, CExp o)) => MM b (Block b) -> m ()) -> (MId, CExp o) -> m ()

type TravWith a blk = (Trav a, Block a ~ blk)

Trav instance a with block type blk

data Term blk

Constructors

forall a.TravWith 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) (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

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)

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

forall a.Refinable a blk => PrioMeta Prio (Metavar a blk)

NoPrio Bool

Instances

Eq (PrioMeta blk)

Defined in Agda.Auto.NarrowingSearch

Methods

(==) :: PrioMeta blk -> PrioMeta blk -> Bool

(/=) :: PrioMeta blk -> PrioMeta blk -> Bool

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

newtype RefCreateEnv blk a

Constructors

RefCreateEnv

Fields

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

Instances

Applicative (RefCreateEnv blk)

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)

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)

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

newtype Cost

Constructors

Cost

Fields

• getCost :: Int

Instances

Num Cost

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

Eq Cost

Defined in Agda.Auto.NarrowingSearch

Methods

(==) :: Cost -> Cost -> Bool

(/=) :: Cost -> Cost -> Bool

Ord Cost

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

Methods

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

Instances

Refinable Choice blk

Defined in Agda.Auto.NarrowingSearch

Methods

refinements :: blk -> [blk] -> Metavar Choice blk -> IO [Move' blk Choice]

Refinable OKVal blk

Defined in Agda.Auto.NarrowingSearch

Methods

refinements :: blk -> [blk] -> Metavar OKVal blk -> IO [Move' blk OKVal]

Refinable (ArgList o) (RefInfo o)

Defined in Agda.Auto.SearchControl

Methods

refinements :: RefInfo o -> [RefInfo o] -> Metavar (ArgList o) (RefInfo o) -> IO [Move' (RefInfo o) (ArgList o)]

Refinable (ConstRef o) (RefInfo o)

Defined in Agda.Auto.SearchControl

Methods

refinements :: RefInfo o -> [RefInfo o] -> Metavar (ConstRef o) (RefInfo o) -> IO [Move' (RefInfo o) (ConstRef o)]

Refinable (Exp o) (RefInfo o)

Defined in Agda.Auto.SearchControl

Methods

refinements :: RefInfo o -> [RefInfo o] -> Metavar (Exp o) (RefInfo o) -> IO [Move' (RefInfo o) (Exp o)]

Refinable (ICExp o) (RefInfo o)

Defined in Agda.Auto.SearchControl

Methods

refinements :: RefInfo o -> [RefInfo o] -> Metavar (ICExp o) (RefInfo o) -> IO [Move' (RefInfo o) (ICExp 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))

Defined in Agda.Auto.Convert

Methods

convert :: Clause -> TOM (Maybe ([Pat O], MExp O))

Conversion TOM Term (MExp O)

Defined in Agda.Auto.Convert

Methods

convert :: Term -> TOM (MExp O)

Conversion TOM Type (MExp O)

Defined in Agda.Auto.Convert

Methods

convert :: Type -> TOM (MExp O)

Conversion TOM Args (MM (ArgList O) (RefInfo O))

Defined in Agda.Auto.Convert

Methods

convert :: Args -> TOM (MM (ArgList O) (RefInfo O))

Conversion TOM [Clause] [([Pat O], MExp O)]

Defined in Agda.Auto.Convert

Methods

convert :: [Clause] -> TOM [([Pat O], MExp O)]

Conversion MOT a b => Conversion MOT (MM a (RefInfo O)) b

Defined in Agda.Auto.Convert

Methods

convert :: MM a (RefInfo O) -> MOT b

LocalTerminationEnv (MArgList o)

Defined in Agda.Auto.CaseSplit

Methods

sizeAndBoundVars :: MArgList o -> (Sum Nat, [Nat])

LocalTerminationEnv (MExp o)

Defined in Agda.Auto.CaseSplit

Methods

sizeAndBoundVars :: MExp o -> (Sum Nat, [Nat])

Replace (Exp o) (MExp o)

Defined in Agda.Auto.CaseSplit

Associated Types

type ReplaceWith (Exp o) (MExp o)

Methods

replace' :: Nat -> MExp (ReplaceWith (Exp o) (MExp o)) -> Exp o -> Reader (Nat, Nat) (MExp o)

Refinable (ICExp o) (RefInfo o)

Defined in Agda.Auto.SearchControl

Methods

refinements :: RefInfo o -> [RefInfo o] -> Metavar (ICExp o) (RefInfo o) -> IO [Move' (RefInfo o) (ICExp o)]

Lift t => Lift (MM t r)

Defined in Agda.Auto.CaseSplit

Methods

lift' :: Nat -> Nat -> MM t r -> MM t r

(Unify t, o ~ UnifiesTo t) => Unify (MM t (RefInfo o))

Defined in Agda.Auto.CaseSplit

Associated Types

type UnifiesTo (MM t (RefInfo o))

Methods

unify' :: MM t (RefInfo o) -> MM t (RefInfo o) -> StateT (Assignments (UnifiesTo (MM t (RefInfo o)))) Maybe ()

notequal' :: MM t (RefInfo o) -> MM t (RefInfo o) -> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo (MM t (RefInfo o)))) IO) Bool

TravWith a blk => Trav (MM a blk)

Defined in Agda.Auto.NarrowingSearch

Associated Types

type Block (MM a blk)

Methods

trav :: Monad m => (forall b. TravWith b (Block (MM a blk)) => MM b (Block b) -> m ()) -> MM a blk -> m ()

Trav (MId, CExp o)

Defined in Agda.Auto.SearchControl

Associated Types

type Block (MId, CExp o)

Methods

trav :: Monad m => (forall b. TravWith b (Block (MId, CExp o)) => MM b (Block b) -> m ()) -> (MId, CExp o) -> m ()

ExpandMetas t => ExpandMetas (MM t a)

Defined in Agda.Auto.Syntax

Methods

expandMetas :: MM t a -> IO (MM t a)

FreeVars t => FreeVars (MM t a)

Defined in Agda.Auto.Syntax

Methods

freeVarsOffset :: Nat -> MM t a -> Set Nat

MetaliseOKH t => MetaliseOKH (MM t a)

Defined in Agda.Auto.Syntax

Methods

metaliseOKH :: MM t a -> IO (MM t a)

Renaming t => Renaming (MM t a)

Defined in Agda.Auto.Syntax

Methods

renameOffset :: Nat -> (Nat -> Nat) -> MM t a -> MM t a

Replace t u => Replace (MM t (RefInfo o)) u

Defined in Agda.Auto.CaseSplit

Associated Types

type ReplaceWith (MM t (RefInfo o)) u

Methods

replace' :: Nat -> MExp (ReplaceWith (MM t (RefInfo o)) u) -> MM t (RefInfo o) -> Reader (Nat, Nat) u

type ReplaceWith (Exp o) (MExp o)

Defined in Agda.Auto.CaseSplit

type ReplaceWith (Exp o) (MExp o) = o

type UnifiesTo (MM t (RefInfo o))

Defined in Agda.Auto.CaseSplit

type UnifiesTo (MM t (RefInfo o)) = o

type Block (MM a blk)

Defined in Agda.Auto.NarrowingSearch

type Block (MM a blk) = blk

type Block (MId, CExp o)

Defined in Agda.Auto.SearchControl

type Block (MId, CExp o) = RefInfo o

type ReplaceWith (MM t (RefInfo o)) u

Defined in Agda.Auto.CaseSplit

type ReplaceWith (MM t (RefInfo o)) u = ReplaceWith t u

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

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

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)