| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Auto.SearchControl
Contents
Synopsis
- data ExpRefInfo o = ExpRefInfo {
- 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
- subsvars :: [CAction o] -> [Nat]
- type Move o = Move' (RefInfo o) (Exp o)
- newAbs :: MId -> RefCreateEnv blk (Abs (MM a blk))
- 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)
- newArgs :: [Hiding] -> RefCreateEnv (RefInfo o) (MArgList o)
- newApp' :: UId o -> ConstRef o -> [Hiding] -> [MExp o] -> RefCreateEnv (RefInfo o) (Exp o)
- newApp :: UId o -> ConstRef o -> [Hiding] -> RefCreateEnv (RefInfo o) (Exp o)
- eqStep :: UId o -> EqReasoningConsts o -> Move o
- 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)
- 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
Documentation
data ExpRefInfo o Source #
Constructors
| ExpRefInfo | |
Fields
| |
initExpRefInfo :: ExpRefInfo o Source #
getinfo :: [RefInfo o] -> ExpRefInfo o Source #
univar :: [CAction o] -> Nat -> Maybe Nat Source #
univar sub v figures out what the name of v "outside" of
the substitution sub ought to be, if anything.
type Move o = Move' (RefInfo o) (Exp o) Source #
Moves
A move is composed of a Cost together with an action
computing the refined problem.
newAbs :: MId -> RefCreateEnv blk (Abs (MM a blk)) Source #
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.
newArgs' :: [Hiding] -> [MExp o] -> RefCreateEnv (RefInfo o) (MArgList o) Source #
New spine of arguments potentially using placeholders
newApp' :: UId o -> ConstRef o -> [Hiding] -> [MExp o] -> RefCreateEnv (RefInfo o) (Exp o) Source #
New Application node using a new spine of arguments
respecting the Hiding annotation
eqStep :: UId o -> EqReasoningConsts o -> Move o Source #
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.
eqBeginStep2 :: UId o -> EqReasoningConsts o -> Move o Source #
pickUid :: forall o. [UId o] -> [Maybe (UId o)] -> (Maybe (UId o), Bool) Source #
Pick the first unused UId amongst the ones you have seen (GA: ??) Defaults to the head of the seen ones.
costIncrease :: Cost Source #
costAppVar :: Cost Source #
costAppHint :: Cost Source #
costLamUnfold :: Cost Source #
costIotaStep :: Cost Source #
costAbsurdLam :: Cost Source #
costUnificationIf :: Bool -> Cost Source #
costEqStep :: Cost Source #
costEqCong :: Cost Source #
prioCompBeta :: Prio Source #
prioCompIota :: Prio Source #
prioCompUnif :: Prio Source #
prioCompCopy :: Prio Source #
prioNoIota :: Prio Source #
prioProjIndex :: Prio Source #
prioTypecheck :: Bool -> Prio Source #