Safe Haskell	None
Language	Haskell2010

Agda.Auto.Syntax

Synopsis

type UId o = Metavar (Exp o) (RefInfo o)
data HintMode
- = HMNormal
- | HMRecCall
data EqReasoningConsts o = EqReasoningConsts {
- eqrcId, eqrcBegin, eqrcStep, eqrcEnd, eqrcSym, eqrcCong :: ConstRef o
}
data EqReasoningState
- = EqRSNone
- | EqRSChain
- | EqRSPrf1
- | EqRSPrf2
- | EqRSPrf3
data RefInfo o
- = RIEnv {
  - rieHints :: [(ConstRef o, HintMode)]
  - rieDefFreeVars :: Nat
  - rieEqReasoningConsts :: Maybe (EqReasoningConsts o)
  }
- | RIMainInfo {
  - riMainCxtLength :: Nat
  - riMainType :: HNExp o
  - riMainIota :: Bool
  }
- | RIUnifInfo [CAction o] (HNExp o)
- | RICopyInfo (ICExp o)
- | RIIotaStep Bool
- | RIInferredTypeUnknown
- | RINotConstructor
- | RIUsedVars [UId o] [Elr o]
- | RIPickSubsvar
- | RIEqRState EqReasoningState
- | RICheckElim Bool
- | RICheckProjIndex [ConstRef o]
type MyPB o = PB (RefInfo o)
type MyMB a o = MB a (RefInfo o)
type Nat = Int
data MId
- = Id String
- | NoId
data Abs a = Abs MId a
data ConstDef o = ConstDef {
- cdname :: String
- cdorigin :: o
- cdtype :: MExp o
- cdcont :: DeclCont o
- cddeffreevars :: Nat
}
data DeclCont o
- = Def Nat [Clause o] (Maybe Nat) (Maybe Nat)
- | Datatype [ConstRef o] [ConstRef o]
- | Constructor Nat
- | Postulate
type Clause o = ([Pat o], MExp o)
data Pat o
- = PatConApp (ConstRef o) [Pat o]
- | PatVar String
- | PatExp
type ConstRef o = IORef (ConstDef o)
data Elr o
- = Var Nat
- | Const (ConstRef o)
getVar :: Elr o -> Maybe Nat
getConst :: Elr o -> Maybe (ConstRef o)
data Sort
- = Set Nat
- | UnknownSort
- | Type
data Exp o
- = App {
  - appUId :: Maybe (UId o)
  - appOK :: OKHandle (RefInfo o)
  - appHead :: Elr o
  - appElims :: MArgList o
  }
- | Lam Hiding (Abs (MExp o))
- | Pi (Maybe (UId o)) Hiding Bool (MExp o) (Abs (MExp o))
- | Sort Sort
- | AbsurdLambda Hiding
dontCare :: Exp o
type MExp o = MM (Exp o) (RefInfo o)
data ArgList o
- = ALNil
- | ALCons Hiding (MExp o) (MArgList o)
- | ALProj (MArgList o) (MM (ConstRef o) (RefInfo o)) Hiding (MArgList o)
- | ALConPar (MArgList o)
type MArgList o = MM (ArgList o) (RefInfo o)
data WithSeenUIds a o = WithSeenUIds {
- seenUIds :: [Maybe (UId o)]
- rawValue :: a
}
type HNExp o = WithSeenUIds (HNExp' o) o
data HNExp' o
- = HNApp (Elr o) (ICArgList o)
- | HNLam Hiding (Abs (ICExp o))
- | HNPi Hiding Bool (ICExp o) (Abs (ICExp o))
- | HNSort Sort
data HNArgList o
- = HNALNil
- | HNALCons Hiding (ICExp o) (ICArgList o)
- | HNALConPar (ICArgList o)
data ICArgList o
- = CALNil
- | CALConcat (Clos (MArgList o) o) (ICArgList o)
type ICExp o = Clos (MExp o) o
data Clos a o = Clos [CAction o] a
type CExp o = TrBr (ICExp o) o
data TrBr a o = TrBr [MExp o] a
data CAction o
- = Sub (ICExp o)
- | Skip
- | Weak Nat
type Ctx o = [(MId, CExp o)]
type EE = IO
detecteliminand :: [Clause o] -> Maybe Nat
detectsemiflex :: ConstRef o -> [Clause o] -> IO Bool
categorizedecl :: ConstRef o -> IO ()
class MetaliseOKH t where
- metaliseOKH :: t -> IO t
metaliseokh :: MExp o -> IO (MExp o)
class ExpandMetas t where
- expandMetas :: t -> IO t
addtrailingargs :: Clos (MArgList o) o -> ICArgList o -> ICArgList o
closify :: MExp o -> CExp o
sub :: MExp o -> CExp o -> CExp o
subi :: MExp o -> ICExp o -> ICExp o
weak :: Weakening t => Nat -> t -> t
class Weakening t where
- weak' :: Nat -> t -> t
doclos :: [CAction o] -> Nat -> Either Nat (ICExp o)
freeVars :: FreeVars t => t -> Set Nat
class FreeVars t where
- freeVarsOffset :: Nat -> t -> Set Nat
rename :: Renaming t => (Nat -> Nat) -> t -> t
class Renaming t where
- renameOffset :: Nat -> (Nat -> Nat) -> t -> t

Documentation

type UId o = Metavar (Exp o) (RefInfo o) Source #

Unique identifiers for variable occurrences in unification.

data HintMode Source #

Constructors

HMNormal
HMRecCall

data EqReasoningConsts o Source #

Constructors

EqReasoningConsts
Fields eqrcId, eqrcBegin, eqrcStep, eqrcEnd, eqrcSym, eqrcCong :: ConstRef o

data EqReasoningState Source #

Constructors

EqRSNone
EqRSChain
EqRSPrf1
EqRSPrf2
EqRSPrf3

Instances

Instances details

Eq EqReasoningState Source #
Instance details Defined in Agda.Auto.Syntax Methods (==) :: EqReasoningState -> EqReasoningState -> Bool # (/=) :: EqReasoningState -> EqReasoningState -> Bool #
Show EqReasoningState Source #
Instance details Defined in Agda.Auto.Syntax Methods showsPrec :: Int -> EqReasoningState -> ShowS # show :: EqReasoningState -> String # showList :: [EqReasoningState] -> ShowS #

data RefInfo o Source #

The concrete instance of the blk parameter in Metavar. I.e., the information passed to the search control.

Constructors

RIEnv
Fields rieHints :: [(ConstRef o, HintMode)] rieDefFreeVars :: Nat Nat - deffreevars (to make cost of using module parameters correspond to that of hints). rieEqReasoningConsts :: Maybe (EqReasoningConsts o)
RIMainInfo
Fields riMainCxtLength :: Nat Size of typing context in which meta was created. riMainType :: HNExp o Head normal form of type of meta. riMainIota :: Bool True if iota steps performed when normalising target type (used to put cost when traversing a definition by construction instantiation).
RIUnifInfo [CAction o] (HNExp o)
RICopyInfo (ICExp o)
RIIotaStep Bool
RIInferredTypeUnknown
RINotConstructor
RIUsedVars [UId o] [Elr o]
RIPickSubsvar
RIEqRState EqReasoningState
RICheckElim Bool
RICheckProjIndex [ConstRef o]

Instances

Instances details

Conversion TOM Clause (Maybe ([Pat O], MExp O)) Source #
Instance details Defined in Agda.Auto.Convert Methods convert :: Clause -> TOM (Maybe ([Pat O], MExp O)) Source #
Conversion TOM Type (MExp O) Source #
Instance details Defined in Agda.Auto.Convert Methods convert :: Type -> TOM (MExp O) Source #
Conversion TOM Term (MExp O) Source #
Instance details Defined in Agda.Auto.Convert Methods convert :: Term -> TOM (MExp O) Source #
Conversion TOM Args (MM (ArgList O) (RefInfo O)) Source #
Instance details Defined in Agda.Auto.Convert Methods convert :: Args -> TOM (MM (ArgList O) (RefInfo O)) Source #
Conversion TOM [Clause] [([Pat O], MExp O)] Source #
Instance details Defined in Agda.Auto.Convert Methods convert :: [Clause] -> TOM [([Pat O], MExp O)] Source #
Conversion MOT a b => Conversion MOT (MM a (RefInfo O)) b Source #
Instance details Defined in Agda.Auto.Convert Methods convert :: MM a (RefInfo O) -> MOT b Source #
LocalTerminationEnv (MArgList o) Source #
Instance details Defined in Agda.Auto.CaseSplit Methods sizeAndBoundVars :: MArgList o -> (Sum Nat, [Nat]) Source #
LocalTerminationEnv (MExp o) Source #
Instance details Defined in Agda.Auto.CaseSplit Methods sizeAndBoundVars :: MExp o -> (Sum Nat, [Nat]) Source #
Refinable (ICExp o) (RefInfo o) Source #
Instance details Defined in Agda.Auto.SearchControl Methods refinements :: RefInfo o -> [RefInfo o] -> Metavar (ICExp o) (RefInfo o) -> IO [Move' (RefInfo o) (ICExp o)] Source #
Refinable (ArgList o) (RefInfo o) Source #
Instance details Defined in Agda.Auto.SearchControl Methods refinements :: RefInfo o -> [RefInfo o] -> Metavar (ArgList o) (RefInfo o) -> IO [Move' (RefInfo o) (ArgList o)] Source #
Refinable (Exp o) (RefInfo o) Source #
Instance details Defined in Agda.Auto.SearchControl Methods refinements :: RefInfo o -> [RefInfo o] -> Metavar (Exp o) (RefInfo o) -> IO [Move' (RefInfo o) (Exp o)] Source #
Refinable (ConstRef o) (RefInfo o) Source #
Instance details Defined in Agda.Auto.SearchControl Methods refinements :: RefInfo o -> [RefInfo o] -> Metavar (ConstRef o) (RefInfo o) -> IO [Move' (RefInfo o) (ConstRef o)] Source #
Replace (Exp o) (MExp o) Source #
Instance details Defined in Agda.Auto.CaseSplit Associated Types type ReplaceWith (Exp o) (MExp o) Source # Methods replace' :: Nat -> MExp (ReplaceWith (Exp o) (MExp o)) -> Exp o -> Reader (Nat, Nat) (MExp o) Source #
Trav (MId, CExp o) Source #
Instance details Defined in Agda.Auto.SearchControl 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 #
(Unify t, o ~ UnifiesTo t) => Unify (MM t (RefInfo o)) Source #
Instance details Defined in Agda.Auto.CaseSplit Associated Types type UnifiesTo (MM t (RefInfo o)) Source # Methods unify' :: MM t (RefInfo o) -> MM t (RefInfo o) -> StateT (Assignments (UnifiesTo (MM t (RefInfo o)))) Maybe () Source # notequal' :: MM t (RefInfo o) -> MM t (RefInfo o) -> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo (MM t (RefInfo o)))) IO) Bool Source #
Replace t u => Replace (MM t (RefInfo o)) u Source #
Instance details Defined in Agda.Auto.CaseSplit Associated Types type ReplaceWith (MM t (RefInfo o)) u Source # Methods replace' :: Nat -> MExp (ReplaceWith (MM t (RefInfo o)) u) -> MM t (RefInfo o) -> Reader (Nat, Nat) u Source #
type ReplaceWith (Exp o) (MExp o) Source #
Instance details Defined in Agda.Auto.CaseSplit type ReplaceWith (Exp o) (MExp o) = o
type Block (MId, CExp o) Source #
Instance details Defined in Agda.Auto.SearchControl type Block (MId, CExp o) = RefInfo o
type UnifiesTo (MM t (RefInfo o)) Source #
Instance details Defined in Agda.Auto.CaseSplit type UnifiesTo (MM t (RefInfo o)) = o
type ReplaceWith (MM t (RefInfo o)) u Source #
Instance details Defined in Agda.Auto.CaseSplit type ReplaceWith (MM t (RefInfo o)) u = ReplaceWith t u

type MyPB o = PB (RefInfo o) Source #

type MyMB a o = MB a (RefInfo o) Source #

type Nat = Int Source #

data MId Source #

Constructors

Id String
NoId

Instances

Instances details

Trav (MId, CExp o) Source #
Instance details Defined in Agda.Auto.SearchControl 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 #
type Block (MId, CExp o) Source #
Instance details Defined in Agda.Auto.SearchControl type Block (MId, CExp o) = RefInfo o

data Abs a Source #

Abstraction with maybe a name.

Different from Agda, where there is also info whether function is constant.

Constructors

Abs MId a

Instances

Instances details

Conversion MOT a b => Conversion MOT (Abs a) (Abs b) Source #
Instance details Defined in Agda.Auto.Convert Methods convert :: Abs0 a -> MOT (Abs b) Source #
Renaming t => Renaming (Abs t) Source #
Instance details Defined in Agda.Auto.Syntax Methods renameOffset :: Nat -> (Nat -> Nat) -> Abs t -> Abs t Source #
FreeVars t => FreeVars (Abs t) Source #
Instance details Defined in Agda.Auto.Syntax Methods freeVarsOffset :: Nat -> Abs t -> Set Nat Source #
ExpandMetas t => ExpandMetas (Abs t) Source #
Instance details Defined in Agda.Auto.Syntax Methods expandMetas :: Abs t -> IO (Abs t) Source #
MetaliseOKH t => MetaliseOKH (Abs t) Source #
Instance details Defined in Agda.Auto.Syntax Methods metaliseOKH :: Abs t -> IO (Abs t) Source #
Lift t => Lift (Abs t) Source #
Instance details Defined in Agda.Auto.CaseSplit Methods lift' :: Nat -> Nat -> Abs t -> Abs t Source #
Unify t => Unify (Abs t) Source #
Instance details Defined in Agda.Auto.CaseSplit Associated Types type UnifiesTo (Abs t) Source # Methods unify' :: Abs t -> Abs t -> StateT (Assignments (UnifiesTo (Abs t))) Maybe () Source # notequal' :: Abs t -> Abs t -> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo (Abs t))) IO) Bool Source #
Replace t u => Replace (Abs t) (Abs u) Source #
Instance details Defined in Agda.Auto.CaseSplit Associated Types type ReplaceWith (Abs t) (Abs u) Source # Methods replace' :: Nat -> MExp (ReplaceWith (Abs t) (Abs u)) -> Abs t -> Reader (Nat, Nat) (Abs u) Source #
type UnifiesTo (Abs t) Source #
Instance details Defined in Agda.Auto.CaseSplit type UnifiesTo (Abs t) = UnifiesTo t
type ReplaceWith (Abs t) (Abs u) Source #
Instance details Defined in Agda.Auto.CaseSplit type ReplaceWith (Abs t) (Abs u) = ReplaceWith t u

data ConstDef o Source #

Constant signatures.

Constructors

ConstDef
Fields cdname :: String For debug printing. cdorigin :: o Reference to the Agda constant. cdtype :: MExp o Type of constant. cdcont :: DeclCont o Constant definition. cddeffreevars :: Nat Free vars of the module where the constant is defined..

Instances

Instances details

Refinable (ConstRef o) (RefInfo o) Source #
Instance details Defined in Agda.Auto.SearchControl Methods refinements :: RefInfo o -> [RefInfo o] -> Metavar (ConstRef o) (RefInfo o) -> IO [Move' (RefInfo o) (ConstRef o)] Source #

data DeclCont o Source #

Constant definitions.

Constructors

Def Nat [Clause o] (Maybe Nat) (Maybe Nat)
Datatype [ConstRef o] [ConstRef o]
Constructor Nat
Postulate

type Clause o = ([Pat o], MExp o) Source #

data Pat o Source #

Constructors

PatConApp (ConstRef o) [Pat o]
PatVar String
PatExp	Dot pattern.

Instances

Instances details

Conversion TOM Clause (Maybe ([Pat O], MExp O)) Source #
Instance details Defined in Agda.Auto.Convert Methods convert :: Clause -> TOM (Maybe ([Pat O], MExp O)) Source #
Conversion TOM [Clause] [([Pat O], MExp O)] Source #
Instance details Defined in Agda.Auto.Convert Methods convert :: [Clause] -> TOM [([Pat O], MExp O)] Source #
Conversion TOM (Arg Pattern) (Pat O) Source #
Instance details Defined in Agda.Auto.Convert Methods convert :: Arg Pattern -> TOM (Pat O) Source #

type ConstRef o = IORef (ConstDef o) Source #

data Elr o Source #

Head of application (elimination).

Constructors

Var Nat
Const (ConstRef o)

Instances

Instances details

Eq (Elr o) Source #
Instance details Defined in Agda.Auto.Syntax Methods (==) :: Elr o -> Elr o -> Bool # (/=) :: Elr o -> Elr o -> Bool #
Renaming (Elr o) Source #
Instance details Defined in Agda.Auto.Syntax Methods renameOffset :: Nat -> (Nat -> Nat) -> Elr o -> Elr o Source #
FreeVars (Elr o) Source #
Instance details Defined in Agda.Auto.Syntax Methods freeVarsOffset :: Nat -> Elr o -> Set Nat Source #
Weakening (Elr o) Source #
Instance details Defined in Agda.Auto.Syntax Methods weak' :: Nat -> Elr o -> Elr o Source #

getVar :: Elr o -> Maybe Nat Source #

getConst :: Elr o -> Maybe (ConstRef o) Source #

data Sort Source #

Constructors

Set Nat
UnknownSort
Type

data Exp o Source #

Agsy's internal syntax.

Constructors

App
Fields appUId :: Maybe (UId o) Unique identifier of the head. appOK :: OKHandle (RefInfo o) This application has been type-checked. appHead :: Elr o Head. appElims :: MArgList o Arguments.
Lam Hiding (Abs (MExp o))	Lambda with hiding information.
Pi (Maybe (UId o)) Hiding Bool (MExp o) (Abs (MExp o))	`True` if possibly dependent (var not known to not occur). `False` if non-dependent.
Sort Sort
AbsurdLambda Hiding	Absurd lambda with hiding information.

Instances

Instances details

Conversion TOM Clause (Maybe ([Pat O], MExp O)) Source #
Instance details Defined in Agda.Auto.Convert Methods convert :: Clause -> TOM (Maybe ([Pat O], MExp O)) Source #
Conversion TOM Type (MExp O) Source #
Instance details Defined in Agda.Auto.Convert Methods convert :: Type -> TOM (MExp O) Source #
Conversion TOM Term (MExp O) Source #
Instance details Defined in Agda.Auto.Convert Methods convert :: Term -> TOM (MExp O) Source #
Conversion MOT (Exp O) Type Source #
Instance details Defined in Agda.Auto.Convert Methods convert :: Exp O -> MOT Type Source #
Conversion MOT (Exp O) Term Source #
Instance details Defined in Agda.Auto.Convert Methods convert :: Exp O -> MOT Term Source #
Conversion TOM [Clause] [([Pat O], MExp O)] Source #
Instance details Defined in Agda.Auto.Convert Methods convert :: [Clause] -> TOM [([Pat O], MExp O)] Source #
Trav (Exp o) Source #
Instance details Defined in Agda.Auto.SearchControl 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 #
Renaming (Exp o) Source #
Instance details Defined in Agda.Auto.Syntax Methods renameOffset :: Nat -> (Nat -> Nat) -> Exp o -> Exp o Source #
FreeVars (Exp o) Source #
Instance details Defined in Agda.Auto.Syntax Methods freeVarsOffset :: Nat -> Exp o -> Set Nat Source #
ExpandMetas (Exp o) Source #
Instance details Defined in Agda.Auto.Syntax Methods expandMetas :: Exp o -> IO (Exp o) Source #
MetaliseOKH (Exp o) Source #
Instance details Defined in Agda.Auto.Syntax Methods metaliseOKH :: Exp o -> IO (Exp o) Source #
LocalTerminationEnv (MExp o) Source #
Instance details Defined in Agda.Auto.CaseSplit Methods sizeAndBoundVars :: MExp o -> (Sum Nat, [Nat]) Source #
Lift (Exp o) Source #
Instance details Defined in Agda.Auto.CaseSplit Methods lift' :: Nat -> Nat -> Exp o -> Exp o Source #
Unify (Exp o) Source #
Instance details Defined in Agda.Auto.CaseSplit Associated Types type UnifiesTo (Exp o) Source # Methods unify' :: Exp o -> Exp o -> StateT (Assignments (UnifiesTo (Exp o))) Maybe () Source # notequal' :: Exp o -> Exp o -> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo (Exp o))) IO) Bool Source #
Refinable (ICExp o) (RefInfo o) Source #
Instance details Defined in Agda.Auto.SearchControl Methods refinements :: RefInfo o -> [RefInfo o] -> Metavar (ICExp o) (RefInfo o) -> IO [Move' (RefInfo o) (ICExp o)] Source #
Refinable (Exp o) (RefInfo o) Source #
Instance details Defined in Agda.Auto.SearchControl Methods refinements :: RefInfo o -> [RefInfo o] -> Metavar (Exp o) (RefInfo o) -> IO [Move' (RefInfo o) (Exp o)] Source #
Replace (Exp o) (MExp o) Source #
Instance details Defined in Agda.Auto.CaseSplit Associated Types type ReplaceWith (Exp o) (MExp o) Source # Methods replace' :: Nat -> MExp (ReplaceWith (Exp o) (MExp o)) -> Exp o -> Reader (Nat, Nat) (MExp o) Source #
Trav (MId, CExp o) Source #
Instance details Defined in Agda.Auto.SearchControl 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 #
type Block (Exp o) Source #
Instance details Defined in Agda.Auto.SearchControl type Block (Exp o) = RefInfo o
type UnifiesTo (Exp o) Source #
Instance details Defined in Agda.Auto.CaseSplit type UnifiesTo (Exp o) = o
type ReplaceWith (Exp o) (MExp o) Source #
Instance details Defined in Agda.Auto.CaseSplit type ReplaceWith (Exp o) (MExp o) = o
type Block (MId, CExp o) Source #
Instance details Defined in Agda.Auto.SearchControl type Block (MId, CExp o) = RefInfo o

dontCare :: Exp o Source #

type MExp o = MM (Exp o) (RefInfo o) Source #

"Maybe expression": Expression or reference to meta variable.

data ArgList o Source #

Constructors

ALNil	No more eliminations.
ALCons Hiding (MExp o) (MArgList o)	Application and tail.
ALProj (MArgList o) (MM (ConstRef o) (RefInfo o)) Hiding (MArgList o)	proj pre args, projfcn idx, tail
ALConPar (MArgList o)	Constructor parameter (missing in Agda). Agsy has monomorphic constructors. Inserted to cover glitch of polymorphic constructor applications coming from Agda

Instances

Instances details

Conversion TOM Args (MM (ArgList O) (RefInfo O)) Source #
Instance details Defined in Agda.Auto.Convert Methods convert :: Args -> TOM (MM (ArgList O) (RefInfo O)) Source #
Trav (ArgList o) Source #
Instance details Defined in Agda.Auto.SearchControl 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 #
Renaming (ArgList o) Source #
Instance details Defined in Agda.Auto.Syntax Methods renameOffset :: Nat -> (Nat -> Nat) -> ArgList o -> ArgList o Source #
FreeVars (ArgList o) Source #
Instance details Defined in Agda.Auto.Syntax Methods freeVarsOffset :: Nat -> ArgList o -> Set Nat Source #
ExpandMetas (ArgList o) Source #
Instance details Defined in Agda.Auto.Syntax Methods expandMetas :: ArgList o -> IO (ArgList o) Source #
MetaliseOKH (ArgList o) Source #
Instance details Defined in Agda.Auto.Syntax Methods metaliseOKH :: ArgList o -> IO (ArgList o) Source #
LocalTerminationEnv (MArgList o) Source #
Instance details Defined in Agda.Auto.CaseSplit Methods sizeAndBoundVars :: MArgList o -> (Sum Nat, [Nat]) Source #
Lift (ArgList o) Source #
Instance details Defined in Agda.Auto.CaseSplit Methods lift' :: Nat -> Nat -> ArgList o -> ArgList o Source #
Unify (ArgList o) Source #
Instance details Defined in Agda.Auto.CaseSplit Associated Types type UnifiesTo (ArgList o) Source # Methods unify' :: ArgList o -> ArgList o -> StateT (Assignments (UnifiesTo (ArgList o))) Maybe () Source # notequal' :: ArgList o -> ArgList o -> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo (ArgList o))) IO) Bool Source #
Refinable (ArgList o) (RefInfo o) Source #
Instance details Defined in Agda.Auto.SearchControl Methods refinements :: RefInfo o -> [RefInfo o] -> Metavar (ArgList o) (RefInfo o) -> IO [Move' (RefInfo o) (ArgList o)] Source #
Replace (ArgList o) (ArgList o) Source #
Instance details Defined in Agda.Auto.CaseSplit Associated Types type ReplaceWith (ArgList o) (ArgList o) Source # Methods replace' :: Nat -> MExp (ReplaceWith (ArgList o) (ArgList o)) -> ArgList o -> Reader (Nat, Nat) (ArgList o) Source #
type Block (ArgList o) Source #
Instance details Defined in Agda.Auto.SearchControl type Block (ArgList o) = RefInfo o
type UnifiesTo (ArgList o) Source #
Instance details Defined in Agda.Auto.CaseSplit type UnifiesTo (ArgList o) = o
type ReplaceWith (ArgList o) (ArgList o) Source #
Instance details Defined in Agda.Auto.CaseSplit type ReplaceWith (ArgList o) (ArgList o) = o

type MArgList o = MM (ArgList o) (RefInfo o) Source #

data WithSeenUIds a o Source #

Constructors

WithSeenUIds
Fields seenUIds :: [Maybe (UId o)] rawValue :: a

type HNExp o = WithSeenUIds (HNExp' o) o Source #

data HNExp' o Source #

Constructors

HNApp (Elr o) (ICArgList o)
HNLam Hiding (Abs (ICExp o))
HNPi Hiding Bool (ICExp o) (Abs (ICExp o))
HNSort Sort

data HNArgList o Source #

Head-normal form of ICArgList. First entry is exposed.

Q: Why are there no projection eliminations?

Constructors

HNALNil
HNALCons Hiding (ICExp o) (ICArgList o)
HNALConPar (ICArgList o)

data ICArgList o Source #

Lazy concatenation of argument lists under explicit substitutions.

Constructors

CALNil
CALConcat (Clos (MArgList o) o) (ICArgList o)

Instances

Instances details

Weakening (ICArgList o) Source #
Instance details Defined in Agda.Auto.Syntax Methods weak' :: Nat -> ICArgList o -> ICArgList o Source #

type ICExp o = Clos (MExp o) o Source #

An expression a in an explicit substitution [CAction a].

data Clos a o Source #

Constructors

Clos [CAction o] a

Instances

Instances details

Refinable (ICExp o) (RefInfo o) Source #
Instance details Defined in Agda.Auto.SearchControl Methods refinements :: RefInfo o -> [RefInfo o] -> Metavar (ICExp o) (RefInfo o) -> IO [Move' (RefInfo o) (ICExp o)] Source #
Trav (MId, CExp o) Source #
Instance details Defined in Agda.Auto.SearchControl 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 #
Weakening (Clos a o) Source #
Instance details Defined in Agda.Auto.Syntax Methods weak' :: Nat -> Clos a o -> Clos a o Source #
type Block (MId, CExp o) Source #
Instance details Defined in Agda.Auto.SearchControl type Block (MId, CExp o) = RefInfo o

type CExp o = TrBr (ICExp o) o Source #

data TrBr a o Source #

Constructors

TrBr [MExp o] a

Instances

Instances details

Trav (MId, CExp o) Source #
Instance details Defined in Agda.Auto.SearchControl 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 #
Trav (TrBr a o) Source #
Instance details Defined in Agda.Auto.SearchControl 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 #
Weakening a => Weakening (TrBr a o) Source #
Instance details Defined in Agda.Auto.Syntax Methods weak' :: Nat -> TrBr a o -> TrBr a o Source #
type Block (MId, CExp o) Source #
Instance details Defined in Agda.Auto.SearchControl type Block (MId, CExp o) = RefInfo o
type Block (TrBr a o) Source #
Instance details Defined in Agda.Auto.SearchControl type Block (TrBr a o) = RefInfo o

data CAction o Source #

Entry of an explicit substitution.

An explicit substitution is a list of CActions. This is isomorphic to the usual presentation where Skip and Weak would be constructors of exp. substs.

Constructors

Sub (ICExp o)	Instantation of variable.
Skip	For going under a binder, often called Lift.
Weak Nat	Shifting substitution (going to a larger context).

type Ctx o = [(MId, CExp o)] Source #

type EE = IO Source #

detecteliminand :: [Clause o] -> Maybe Nat Source #

detectsemiflex :: ConstRef o -> [Clause o] -> IO Bool Source #

categorizedecl :: ConstRef o -> IO () Source #

class MetaliseOKH t where Source #

Methods

metaliseOKH :: t -> IO t Source #

Instances

Instances details

MetaliseOKH (ArgList o) Source #
Instance details Defined in Agda.Auto.Syntax Methods metaliseOKH :: ArgList o -> IO (ArgList o) Source #
MetaliseOKH (Exp o) Source #
Instance details Defined in Agda.Auto.Syntax Methods metaliseOKH :: Exp o -> IO (Exp o) Source #
MetaliseOKH t => MetaliseOKH (Abs t) Source #
Instance details Defined in Agda.Auto.Syntax Methods metaliseOKH :: Abs t -> IO (Abs t) Source #
MetaliseOKH t => MetaliseOKH (MM t a) Source #
Instance details Defined in Agda.Auto.Syntax Methods metaliseOKH :: MM t a -> IO (MM t a) Source #

metaliseokh :: MExp o -> IO (MExp o) Source #

class ExpandMetas t where Source #

Methods

expandMetas :: t -> IO t Source #

Instances

Instances details

ExpandMetas (ArgList o) Source #
Instance details Defined in Agda.Auto.Syntax Methods expandMetas :: ArgList o -> IO (ArgList o) Source #
ExpandMetas (Exp o) Source #
Instance details Defined in Agda.Auto.Syntax Methods expandMetas :: Exp o -> IO (Exp o) Source #
ExpandMetas t => ExpandMetas (Abs t) Source #
Instance details Defined in Agda.Auto.Syntax Methods expandMetas :: Abs t -> IO (Abs t) Source #
ExpandMetas t => ExpandMetas (MM t a) Source #
Instance details Defined in Agda.Auto.Syntax Methods expandMetas :: MM t a -> IO (MM t a) Source #

addtrailingargs :: Clos (MArgList o) o -> ICArgList o -> ICArgList o Source #

closify :: MExp o -> CExp o Source #

sub :: MExp o -> CExp o -> CExp o Source #

subi :: MExp o -> ICExp o -> ICExp o Source #

weak :: Weakening t => Nat -> t -> t Source #

class Weakening t where Source #

Methods

weak' :: Nat -> t -> t Source #

Instances

Instances details

Weakening (ICArgList o) Source #
Instance details Defined in Agda.Auto.Syntax Methods weak' :: Nat -> ICArgList o -> ICArgList o Source #
Weakening (Elr o) Source #
Instance details Defined in Agda.Auto.Syntax Methods weak' :: Nat -> Elr o -> Elr o Source #
Weakening a => Weakening (TrBr a o) Source #
Instance details Defined in Agda.Auto.Syntax Methods weak' :: Nat -> TrBr a o -> TrBr a o Source #
Weakening (Clos a o) Source #
Instance details Defined in Agda.Auto.Syntax Methods weak' :: Nat -> Clos a o -> Clos a o Source #

doclos :: [CAction o] -> Nat -> Either Nat (ICExp o) Source #

Substituting for a variable.

freeVars :: FreeVars t => t -> Set Nat Source #

FreeVars class and instances

class FreeVars t where Source #

Methods

freeVarsOffset :: Nat -> t -> Set Nat Source #

Instances

Instances details

FreeVars (ArgList o) Source #
Instance details Defined in Agda.Auto.Syntax Methods freeVarsOffset :: Nat -> ArgList o -> Set Nat Source #
FreeVars (Exp o) Source #
Instance details Defined in Agda.Auto.Syntax Methods freeVarsOffset :: Nat -> Exp o -> Set Nat Source #
FreeVars (Elr o) Source #
Instance details Defined in Agda.Auto.Syntax Methods freeVarsOffset :: Nat -> Elr o -> Set Nat Source #
FreeVars t => FreeVars (Abs t) Source #
Instance details Defined in Agda.Auto.Syntax Methods freeVarsOffset :: Nat -> Abs t -> Set Nat Source #
(FreeVars a, FreeVars b) => FreeVars (a, b) Source #
Instance details Defined in Agda.Auto.Syntax Methods freeVarsOffset :: Nat -> (a, b) -> Set Nat Source #
FreeVars t => FreeVars (MM t a) Source #
Instance details Defined in Agda.Auto.Syntax Methods freeVarsOffset :: Nat -> MM t a -> Set Nat Source #

rename :: Renaming t => (Nat -> Nat) -> t -> t Source #

Renaming Typeclass and instances

class Renaming t where Source #

Methods

renameOffset :: Nat -> (Nat -> Nat) -> t -> t Source #

Instances

Instances details

Renaming (ArgList o) Source #
Instance details Defined in Agda.Auto.Syntax Methods renameOffset :: Nat -> (Nat -> Nat) -> ArgList o -> ArgList o Source #
Renaming (Exp o) Source #
Instance details Defined in Agda.Auto.Syntax Methods renameOffset :: Nat -> (Nat -> Nat) -> Exp o -> Exp o Source #
Renaming (Elr o) Source #
Instance details Defined in Agda.Auto.Syntax Methods renameOffset :: Nat -> (Nat -> Nat) -> Elr o -> Elr o Source #
Renaming t => Renaming (Abs t) Source #
Instance details Defined in Agda.Auto.Syntax Methods renameOffset :: Nat -> (Nat -> Nat) -> Abs t -> Abs t Source #
Renaming (CSPatI o) Source #
Instance details Defined in Agda.Auto.CaseSplit Methods renameOffset :: Nat -> (Nat -> Nat) -> CSPatI o -> CSPatI o Source #
Renaming t => Renaming (HI t) Source #
Instance details Defined in Agda.Auto.CaseSplit Methods renameOffset :: Nat -> (Nat -> Nat) -> HI t -> HI t Source #
(Renaming a, Renaming b) => Renaming (a, b) Source #
Instance details Defined in Agda.Auto.Syntax Methods renameOffset :: Nat -> (Nat -> Nat) -> (a, b) -> (a, b) Source #
Renaming t => Renaming (MM t a) Source #
Instance details Defined in Agda.Auto.Syntax Methods renameOffset :: Nat -> (Nat -> Nat) -> MM t a -> MM t a Source #