Agda-2.6.2.2: A dependently typed functional programming language and proof assistant

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.Auto.SearchControl

Contents

- Orphan instances

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

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

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

List of the variables instantiated by the substitution

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.

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

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

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

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

New spine of arguments potentially using placeholders

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

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

New `App`lication node using a new spine of arguments respecting the `Hiding` annotation

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

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.

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

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

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

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.

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

costIncrease :: Cost Source #

costUnificationOccurs :: Cost Source #

costUnification :: Cost Source #

costAppVar :: Cost Source #

costAppVarUsed :: Cost Source #

costAppHint :: Cost Source #

costAppHintUsed :: Cost Source #

costAppRecCall :: Cost Source #

costAppRecCallUsed :: Cost Source #

costAppConstructor :: Cost Source #

costAppConstructorSingle :: Cost Source #

costAppExtraRef :: Cost Source #

costLam :: Cost Source #

costLamUnfold :: Cost Source #

costPi :: Cost Source #

costSort :: Cost Source #

costIotaStep :: Cost Source #

costInferredTypeUnkown :: Cost Source #

costAbsurdLam :: Cost Source #

costUnificationIf :: Bool -> Cost Source #

costEqStep :: Cost Source #

costEqEnd :: Cost Source #

costEqSym :: Cost Source #

costEqCong :: Cost Source #

prioNo :: Prio Source #

prioTypeUnknown :: Prio Source #

prioTypecheckArgList :: Prio Source #

prioInferredTypeUnknown :: Prio Source #

prioCompBeta :: Prio Source #

prioCompBetaStructured :: Prio Source #

prioCompareArgList :: Prio Source #

prioCompIota :: Prio Source #

prioCompChoice :: Prio Source #

prioCompUnif :: Prio Source #

prioCompCopy :: Prio Source #

prioNoIota :: Prio Source #

prioAbsurdLambda :: Prio Source #

prioProjIndex :: Prio Source #

prioTypecheck :: Bool -> Prio Source #

# Orphan instances

Trav (ArgList o) Source # |
Instance details Associated Types type Block (ArgList o) Source # Methods trav :: Monad m => (forall b. TravWith b (Block (ArgList o)) => MM b (Block b) -> m ()) -> ArgList o -> m () Source #
Trav (Exp o) Source # |
Instance details Associated Types type Block (Exp o) Source # Methods trav :: Monad m => (forall b. TravWith b (Block (Exp o)) => MM b (Block b) -> m ()) -> Exp o -> m () Source #
Trav a => Trav [a] Source # |
Instance details Associated Types type Block [a] Source # Methods trav :: Monad m => (forall b. TravWith b (Block [a]) => MM b (Block b) -> m ()) -> [a] -> m () Source #
Refinable (ArgList o) (RefInfo o) Source # |
Instance details Methods refinements :: RefInfo o -> [RefInfo o] -> Metavar (ArgList o) (RefInfo o) -> IO [Move' (RefInfo o) (ArgList o)] Source #
Refinable (ConstRef o) (RefInfo o) Source # |
Instance details Methods refinements :: RefInfo o -> [RefInfo o] -> Metavar (ConstRef o) (RefInfo o) -> IO [Move' (RefInfo o) (ConstRef o)] Source #
Refinable (Exp o) (RefInfo o) Source # |
Instance details Methods refinements :: RefInfo o -> [RefInfo o] -> Metavar (Exp o) (RefInfo o) -> IO [Move' (RefInfo o) (Exp o)] Source #
Refinable (ICExp o) (RefInfo o) Source # |
Instance details Methods refinements :: RefInfo o -> [RefInfo o] -> Metavar (ICExp o) (RefInfo o) -> IO [Move' (RefInfo o) (ICExp o)] Source #
Trav (TrBr a o) Source # |
Instance details Associated Types type Block (TrBr a o) Source # Methods trav :: Monad m => (forall b. TravWith b (Block (TrBr a o)) => MM b (Block b) -> m ()) -> TrBr a o -> m () Source #
Trav (MId, CExp o) Source # |
Instance details Associated Types type Block (MId, CExp o) Source # Methods trav :: Monad m => (forall b. TravWith b (Block (MId, CExp o)) => MM b (Block b) -> m ()) -> (MId, CExp o) -> m () Source #