Agda.Auto.SearchControl

Documentation

data ExpRefInfo o

Constructors

ExpRefInfo

Fields

• eriMain :: Maybe (RefInfo o)
• eriUnifs :: [RefInfo o]
• eriInfTypeUnknown :: Bool
• eriIsEliminand :: Bool
• eriUsedVars :: Maybe ([UId o], [Elr o])
• eriIotaStep :: Maybe Bool
• eriPickSubsVar :: Bool
• eriEqRState :: Maybe EqReasoningState

initExpRefInfo :: ExpRefInfo o

getinfo :: [RefInfo o] -> ExpRefInfo o

univar :: [CAction o] -> Nat -> Maybe Nat

univar sub v figures out what the name of v "outside" of the substitution sub ought to be, if anything.

subsvars :: [CAction o] -> [Nat]

List of the variables instantiated by the substitution

type Move o = Move' (RefInfo o) (Exp o)

Moves A move is composed of a Cost together with an action computing the refined problem.

newAbs :: MId -> RefCreateEnv blk (Abs (MM a blk))

New constructors Taking a step towards a solution consists in picking a constructor and filling in the missing parts with placeholders to be discharged later on.

newLam :: Hiding -> MId -> RefCreateEnv (RefInfo o) (Exp o)

newPi :: UId o -> Bool -> Hiding -> RefCreateEnv (RefInfo o) (Exp o)

foldArgs :: [(Hiding, MExp o)] -> MArgList o

newArgs' :: [Hiding] -> [MExp o] -> RefCreateEnv (RefInfo o) (MArgList o)

New spine of arguments potentially using placeholders

newArgs :: [Hiding] -> RefCreateEnv (RefInfo o) (MArgList o)

newApp' :: UId o -> ConstRef o -> [Hiding] -> [MExp o] -> RefCreateEnv (RefInfo o) (Exp o)

New Application node using a new spine of arguments respecting the Hiding annotation

newApp :: UId o -> ConstRef o -> [Hiding] -> RefCreateEnv (RefInfo o) (Exp o)

eqStep :: UId o -> EqReasoningConsts o -> Move o

Equality reasoning steps The begin token is accompanied by two steps because it does not make sense to have a derivation any shorter than that.

eqEnd :: UId o -> EqReasoningConsts o -> Move o

eqCong :: UId o -> EqReasoningConsts o -> Move o

eqSym :: UId o -> EqReasoningConsts o -> Move o

eqBeginStep2 :: UId o -> EqReasoningConsts o -> Move o

pickUid :: forall o. [UId o] -> [Maybe (UId o)] -> (Maybe (UId o), Bool)

Pick the first unused UId amongst the ones you have seen (GA: ??) Defaults to the head of the seen ones.

extraref :: UId o -> [Maybe (UId o)] -> ConstRef o -> Move o

costIncrease :: Cost

costUnificationOccurs :: Cost

costUnification :: Cost

costAppVar :: Cost

costAppVarUsed :: Cost

costAppHint :: Cost

costAppHintUsed :: Cost

costAppRecCall :: Cost

costAppRecCallUsed :: Cost

costAppConstructor :: Cost

costAppConstructorSingle :: Cost

costAppExtraRef :: Cost

costLam :: Cost

costLamUnfold :: Cost

costPi :: Cost

costSort :: Cost

costIotaStep :: Cost

costInferredTypeUnkown :: Cost

costAbsurdLam :: Cost

costUnificationIf :: Bool -> Cost

costEqStep :: Cost

costEqEnd :: Cost

costEqSym :: Cost

costEqCong :: Cost

prioNo :: Prio

prioTypeUnknown :: Prio

prioTypecheckArgList :: Prio

prioInferredTypeUnknown :: Prio

prioCompBeta :: Prio

prioCompBetaStructured :: Prio

prioCompareArgList :: Prio

prioCompIota :: Prio

prioCompChoice :: Prio

prioCompUnif :: Prio

prioCompCopy :: Prio

prioNoIota :: Prio

prioAbsurdLambda :: Prio

prioProjIndex :: Prio

prioTypecheck :: Bool -> Prio

Orphan instances

Trav (ArgList o)

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)

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]

Associated Types

type Block [a]

Methods

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

Refinable (ArgList o) (RefInfo o)

Methods

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

Refinable (ConstRef o) (RefInfo o)

Methods

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

Refinable (Exp o) (RefInfo o)

Methods

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

Refinable (ICExp o) (RefInfo o)

Methods

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

Trav (TrBr a o)

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)

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 ()