Agda-2.6.3.20230930: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Auto.SearchControl

Synopsis

Documentation

data ExpRefInfo o Source #

Constructors

ExpRefInfo 

Fields

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.

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

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.

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 #

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 #