Agda.Auto.Syntax

Documentation

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

Unique identifiers for variable occurrences in unification.

data HintMode

Constructors

HMNormal

HMRecCall

data EqReasoningConsts o

Constructors

EqReasoningConsts

Fields

• eqrcId, eqrcBegin, eqrcStep, eqrcEnd, eqrcSym, eqrcCong :: ConstRef o

data EqReasoningState

Constructors

EqRSNone

EqRSChain

EqRSPrf1

EqRSPrf2

EqRSPrf3

Instances

Show EqReasoningState

Defined in Agda.Auto.Syntax

Methods

showsPrec :: Int -> EqReasoningState -> ShowS

show :: EqReasoningState -> String

showList :: [EqReasoningState] -> ShowS

Eq EqReasoningState

Defined in Agda.Auto.Syntax

Methods

(==) :: EqReasoningState -> EqReasoningState -> Bool

(/=) :: EqReasoningState -> EqReasoningState -> Bool

data RefInfo o

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

Conversion TOM Clause (Maybe ([Pat O], MExp O))

Defined in Agda.Auto.Convert

Methods

convert :: Clause -> TOM (Maybe ([Pat O], MExp O))

Conversion TOM Term (MExp O)

Defined in Agda.Auto.Convert

Methods

convert :: Term -> TOM (MExp O)

Conversion TOM Type (MExp O)

Defined in Agda.Auto.Convert

Methods

convert :: Type -> TOM (MExp O)

Conversion TOM Args (MM (ArgList O) (RefInfo O))

Defined in Agda.Auto.Convert

Methods

convert :: Args -> TOM (MM (ArgList O) (RefInfo O))

Conversion TOM [Clause] [([Pat O], MExp O)]

Defined in Agda.Auto.Convert

Methods

convert :: [Clause] -> TOM [([Pat O], MExp O)]

Conversion MOT a b => Conversion MOT (MM a (RefInfo O)) b

Defined in Agda.Auto.Convert

Methods

convert :: MM a (RefInfo O) -> MOT b

LocalTerminationEnv (MArgList o)

Defined in Agda.Auto.CaseSplit

Methods

sizeAndBoundVars :: MArgList o -> (Sum Nat, [Nat])

LocalTerminationEnv (MExp o)

Defined in Agda.Auto.CaseSplit

Methods

sizeAndBoundVars :: MExp o -> (Sum Nat, [Nat])

Replace (Exp o) (MExp o)

Defined in Agda.Auto.CaseSplit

Associated Types

type ReplaceWith (Exp o) (MExp o)

Methods

replace' :: Nat -> MExp (ReplaceWith (Exp o) (MExp o)) -> Exp o -> Reader (Nat, Nat) (MExp o)

Refinable (ArgList o) (RefInfo o)

Defined in Agda.Auto.SearchControl

Methods

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

Refinable (ConstRef o) (RefInfo o)

Defined in Agda.Auto.SearchControl

Methods

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

Refinable (Exp o) (RefInfo o)

Defined in Agda.Auto.SearchControl

Methods

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

Refinable (ICExp o) (RefInfo o)

Defined in Agda.Auto.SearchControl

Methods

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

(Unify t, o ~ UnifiesTo t) => Unify (MM t (RefInfo o))

Defined in Agda.Auto.CaseSplit

Associated Types

type UnifiesTo (MM t (RefInfo o))

Methods

unify' :: MM t (RefInfo o) -> MM t (RefInfo o) -> StateT (Assignments (UnifiesTo (MM t (RefInfo o)))) Maybe ()

notequal' :: MM t (RefInfo o) -> MM t (RefInfo o) -> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo (MM t (RefInfo o)))) IO) Bool

Trav (MId, CExp o)

Defined in Agda.Auto.SearchControl

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

Replace t u => Replace (MM t (RefInfo o)) u

Defined in Agda.Auto.CaseSplit

Associated Types

type ReplaceWith (MM t (RefInfo o)) u

Methods

replace' :: Nat -> MExp (ReplaceWith (MM t (RefInfo o)) u) -> MM t (RefInfo o) -> Reader (Nat, Nat) u

type ReplaceWith (Exp o) (MExp o)

Defined in Agda.Auto.CaseSplit

type ReplaceWith (Exp o) (MExp o) = o

type UnifiesTo (MM t (RefInfo o))

Defined in Agda.Auto.CaseSplit

type UnifiesTo (MM t (RefInfo o)) = o

type Block (MId, CExp o)

Defined in Agda.Auto.SearchControl

type Block (MId, CExp o) = RefInfo o

type ReplaceWith (MM t (RefInfo o)) u

Defined in Agda.Auto.CaseSplit

type ReplaceWith (MM t (RefInfo o)) u = ReplaceWith t u

type MyPB o = PB (RefInfo o)

type MyMB a o = MB a (RefInfo o)

type Nat = Int

data MId

Constructors

Id String

NoId

Instances

Trav (MId, CExp o)

Defined in Agda.Auto.SearchControl

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

type Block (MId, CExp o)

Defined in Agda.Auto.SearchControl

type Block (MId, CExp o) = RefInfo o

data Abs a

Abstraction with maybe a name.

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

Constructors

Abs MId a

Instances

Conversion MOT a b => Conversion MOT (Abs a) (Abs b)

Defined in Agda.Auto.Convert

Methods

convert :: Abs0 a -> MOT (Abs b)

Lift t => Lift (Abs t)

Defined in Agda.Auto.CaseSplit

Methods

lift' :: Nat -> Nat -> Abs t -> Abs t

Unify t => Unify (Abs t)

Defined in Agda.Auto.CaseSplit

Associated Types

type UnifiesTo (Abs t)

Methods

unify' :: Abs t -> Abs t -> StateT (Assignments (UnifiesTo (Abs t))) Maybe ()

notequal' :: Abs t -> Abs t -> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo (Abs t))) IO) Bool

ExpandMetas t => ExpandMetas (Abs t)

Defined in Agda.Auto.Syntax

Methods

expandMetas :: Abs t -> IO (Abs t)

FreeVars t => FreeVars (Abs t)

Defined in Agda.Auto.Syntax

Methods

freeVarsOffset :: Nat -> Abs t -> Set Nat

MetaliseOKH t => MetaliseOKH (Abs t)

Defined in Agda.Auto.Syntax

Methods

metaliseOKH :: Abs t -> IO (Abs t)

Renaming t => Renaming (Abs t)

Defined in Agda.Auto.Syntax

Methods

renameOffset :: Nat -> (Nat -> Nat) -> Abs t -> Abs t

Replace t u => Replace (Abs t) (Abs u)

Defined in Agda.Auto.CaseSplit

Associated Types

type ReplaceWith (Abs t) (Abs u)

Methods

replace' :: Nat -> MExp (ReplaceWith (Abs t) (Abs u)) -> Abs t -> Reader (Nat, Nat) (Abs u)

type UnifiesTo (Abs t)

Defined in Agda.Auto.CaseSplit

type UnifiesTo (Abs t) = UnifiesTo t

type ReplaceWith (Abs t) (Abs u)

Defined in Agda.Auto.CaseSplit

type ReplaceWith (Abs t) (Abs u) = ReplaceWith t u

data ConstDef o

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

Refinable (ConstRef o) (RefInfo o)

Defined in Agda.Auto.SearchControl

Methods

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

data DeclCont o

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)

data Pat o

Constructors

PatConApp (ConstRef o) [Pat o]

PatVar String

PatExp

Dot pattern.

PatProj (ConstRef o)

Projection pattern.

Instances

Conversion TOM Clause (Maybe ([Pat O], MExp O))

Defined in Agda.Auto.Convert

Methods

convert :: Clause -> TOM (Maybe ([Pat O], MExp O))

Conversion TOM (Arg Pattern) (Pat O)

Defined in Agda.Auto.Convert

Methods

convert :: Arg Pattern -> TOM (Pat O)

Conversion TOM [Clause] [([Pat O], MExp O)]

Defined in Agda.Auto.Convert

Methods

convert :: [Clause] -> TOM [([Pat O], MExp O)]

type ConstRef o = IORef (ConstDef o)

data Elr o

Head of application (elimination).

Constructors

Var Nat

Const (ConstRef o)

Instances

FreeVars (Elr o)

Defined in Agda.Auto.Syntax

Methods

freeVarsOffset :: Nat -> Elr o -> Set Nat

Renaming (Elr o)

Defined in Agda.Auto.Syntax

Methods

renameOffset :: Nat -> (Nat -> Nat) -> Elr o -> Elr o

Weakening (Elr o)

Defined in Agda.Auto.Syntax

Methods

weak' :: Nat -> Elr o -> Elr o

Eq (Elr o)

Defined in Agda.Auto.Syntax

Methods

(==) :: Elr o -> Elr o -> Bool

(/=) :: Elr o -> Elr o -> Bool

getVar :: Elr o -> Maybe Nat

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

data Sort

Constructors

Set Nat

UnknownSort

Type

data Exp o

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

Conversion TOM Clause (Maybe ([Pat O], MExp O))

Defined in Agda.Auto.Convert

Methods

convert :: Clause -> TOM (Maybe ([Pat O], MExp O))

Conversion TOM Term (MExp O)

Defined in Agda.Auto.Convert

Methods

convert :: Term -> TOM (MExp O)

Conversion TOM Type (MExp O)

Defined in Agda.Auto.Convert

Methods

convert :: Type -> TOM (MExp O)

Conversion MOT (Exp O) Term

Defined in Agda.Auto.Convert

Methods

convert :: Exp O -> MOT Term

Conversion MOT (Exp O) Type

Defined in Agda.Auto.Convert

Methods

convert :: Exp O -> MOT Type

Conversion TOM [Clause] [([Pat O], MExp O)]

Defined in Agda.Auto.Convert

Methods

convert :: [Clause] -> TOM [([Pat O], MExp O)]

Lift (Exp o)

Defined in Agda.Auto.CaseSplit

Methods

lift' :: Nat -> Nat -> Exp o -> Exp o

LocalTerminationEnv (MExp o)

Defined in Agda.Auto.CaseSplit

Methods

sizeAndBoundVars :: MExp o -> (Sum Nat, [Nat])

Unify (Exp o)

Defined in Agda.Auto.CaseSplit

Associated Types

type UnifiesTo (Exp o)

Methods

unify' :: Exp o -> Exp o -> StateT (Assignments (UnifiesTo (Exp o))) Maybe ()

notequal' :: Exp o -> Exp o -> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo (Exp o))) IO) Bool

Trav (Exp o)

Defined in Agda.Auto.SearchControl

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

ExpandMetas (Exp o)

Defined in Agda.Auto.Syntax

Methods

expandMetas :: Exp o -> IO (Exp o)

FreeVars (Exp o)

Defined in Agda.Auto.Syntax

Methods

freeVarsOffset :: Nat -> Exp o -> Set Nat

MetaliseOKH (Exp o)

Defined in Agda.Auto.Syntax

Methods

metaliseOKH :: Exp o -> IO (Exp o)

Renaming (Exp o)

Defined in Agda.Auto.Syntax

Methods

renameOffset :: Nat -> (Nat -> Nat) -> Exp o -> Exp o

Replace (Exp o) (MExp o)

Defined in Agda.Auto.CaseSplit

Associated Types

type ReplaceWith (Exp o) (MExp o)

Methods

replace' :: Nat -> MExp (ReplaceWith (Exp o) (MExp o)) -> Exp o -> Reader (Nat, Nat) (MExp o)

Refinable (Exp o) (RefInfo o)

Defined in Agda.Auto.SearchControl

Methods

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

Refinable (ICExp o) (RefInfo o)

Defined in Agda.Auto.SearchControl

Methods

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

Trav (MId, CExp o)

Defined in Agda.Auto.SearchControl

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

type UnifiesTo (Exp o)

Defined in Agda.Auto.CaseSplit

type UnifiesTo (Exp o) = o

type Block (Exp o)

Defined in Agda.Auto.SearchControl

type Block (Exp o) = RefInfo o

type ReplaceWith (Exp o) (MExp o)

Defined in Agda.Auto.CaseSplit

type ReplaceWith (Exp o) (MExp o) = o

type Block (MId, CExp o)

Defined in Agda.Auto.SearchControl

type Block (MId, CExp o) = RefInfo o

dontCare :: Exp o

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

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

data ArgList o

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

Conversion TOM Args (MM (ArgList O) (RefInfo O))

Defined in Agda.Auto.Convert

Methods

convert :: Args -> TOM (MM (ArgList O) (RefInfo O))

Lift (ArgList o)

Defined in Agda.Auto.CaseSplit

Methods

lift' :: Nat -> Nat -> ArgList o -> ArgList o

LocalTerminationEnv (MArgList o)

Defined in Agda.Auto.CaseSplit

Methods

sizeAndBoundVars :: MArgList o -> (Sum Nat, [Nat])

Unify (ArgList o)

Defined in Agda.Auto.CaseSplit

Associated Types

type UnifiesTo (ArgList o)

Methods

unify' :: ArgList o -> ArgList o -> StateT (Assignments (UnifiesTo (ArgList o))) Maybe ()

notequal' :: ArgList o -> ArgList o -> ReaderT (Nat, Nat) (StateT (Assignments (UnifiesTo (ArgList o))) IO) Bool

Trav (ArgList o)

Defined in Agda.Auto.SearchControl

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

ExpandMetas (ArgList o)

Defined in Agda.Auto.Syntax

Methods

expandMetas :: ArgList o -> IO (ArgList o)

FreeVars (ArgList o)

Defined in Agda.Auto.Syntax

Methods

freeVarsOffset :: Nat -> ArgList o -> Set Nat

MetaliseOKH (ArgList o)

Defined in Agda.Auto.Syntax

Methods

metaliseOKH :: ArgList o -> IO (ArgList o)

Renaming (ArgList o)

Defined in Agda.Auto.Syntax

Methods

renameOffset :: Nat -> (Nat -> Nat) -> ArgList o -> ArgList o

Replace (ArgList o) (ArgList o)

Defined in Agda.Auto.CaseSplit

Associated Types

type ReplaceWith (ArgList o) (ArgList o)

Methods

replace' :: Nat -> MExp (ReplaceWith (ArgList o) (ArgList o)) -> ArgList o -> Reader (Nat, Nat) (ArgList o)

Refinable (ArgList o) (RefInfo o)

Defined in Agda.Auto.SearchControl

Methods

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

type UnifiesTo (ArgList o)

Defined in Agda.Auto.CaseSplit

type UnifiesTo (ArgList o) = o

type Block (ArgList o)

Defined in Agda.Auto.SearchControl

type Block (ArgList o) = RefInfo o

type ReplaceWith (ArgList o) (ArgList o)

Defined in Agda.Auto.CaseSplit

type ReplaceWith (ArgList o) (ArgList o) = o

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

data WithSeenUIds a o

Constructors

WithSeenUIds

Fields

• seenUIds :: [Maybe (UId o)]
• rawValue :: a

type HNExp o = WithSeenUIds (HNExp' o) o

data HNExp' o

Constructors

HNApp (Elr o) (ICArgList o)

HNLam Hiding (Abs (ICExp o))

HNPi Hiding Bool (ICExp o) (Abs (ICExp o))

HNSort Sort

data HNArgList o

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

Lazy concatenation of argument lists under explicit substitutions.

Constructors

CALNil

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

Instances

Weakening (ICArgList o)

Defined in Agda.Auto.Syntax

Methods

weak' :: Nat -> ICArgList o -> ICArgList o

type ICExp o = Clos (MExp o) o

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

data Clos a o

Constructors

Clos [CAction o] a

Instances

Refinable (ICExp o) (RefInfo o)

Defined in Agda.Auto.SearchControl

Methods

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

Trav (MId, CExp o)

Defined in Agda.Auto.SearchControl

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

Weakening (Clos a o)

Defined in Agda.Auto.Syntax

Methods

weak' :: Nat -> Clos a o -> Clos a o

type Block (MId, CExp o)

Defined in Agda.Auto.SearchControl

type Block (MId, CExp o) = RefInfo o

type CExp o = TrBr (ICExp o) o

data TrBr a o

Constructors

TrBr [MExp o] a

Instances

Trav (TrBr a o)

Defined in Agda.Auto.SearchControl

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)

Defined in Agda.Auto.SearchControl

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

Weakening a => Weakening (TrBr a o)

Defined in Agda.Auto.Syntax

Methods

weak' :: Nat -> TrBr a o -> TrBr a o

type Block (TrBr a o)

Defined in Agda.Auto.SearchControl

type Block (TrBr a o) = RefInfo o

type Block (MId, CExp o)

Defined in Agda.Auto.SearchControl

type Block (MId, CExp o) = RefInfo o

data CAction o

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

type EE = IO

detecteliminand :: [Clause o] -> Maybe Nat

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

categorizedecl :: ConstRef o -> IO ()

class MetaliseOKH t where

Methods

metaliseOKH :: t -> IO t

Instances

MetaliseOKH t => MetaliseOKH (Abs t)

Defined in Agda.Auto.Syntax

Methods

metaliseOKH :: Abs t -> IO (Abs t)

MetaliseOKH (ArgList o)

Defined in Agda.Auto.Syntax

Methods

metaliseOKH :: ArgList o -> IO (ArgList o)

MetaliseOKH (Exp o)

Defined in Agda.Auto.Syntax

Methods

metaliseOKH :: Exp o -> IO (Exp o)

MetaliseOKH t => MetaliseOKH (MM t a)

Defined in Agda.Auto.Syntax

Methods

metaliseOKH :: MM t a -> IO (MM t a)

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

class ExpandMetas t where

Methods

expandMetas :: t -> IO t

Instances

ExpandMetas t => ExpandMetas (Abs t)

Defined in Agda.Auto.Syntax

Methods

expandMetas :: Abs t -> IO (Abs t)

ExpandMetas (ArgList o)

Defined in Agda.Auto.Syntax

Methods

expandMetas :: ArgList o -> IO (ArgList o)

ExpandMetas (Exp o)

Defined in Agda.Auto.Syntax

Methods

expandMetas :: Exp o -> IO (Exp o)

ExpandMetas t => ExpandMetas (MM t a)

Defined in Agda.Auto.Syntax

Methods

expandMetas :: MM t a -> IO (MM t a)

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

Methods

weak' :: Nat -> t -> t

Instances

Weakening (Elr o)

Defined in Agda.Auto.Syntax

Methods

weak' :: Nat -> Elr o -> Elr o

Weakening (ICArgList o)

Defined in Agda.Auto.Syntax

Methods

weak' :: Nat -> ICArgList o -> ICArgList o

Weakening (Clos a o)

Defined in Agda.Auto.Syntax

Methods

weak' :: Nat -> Clos a o -> Clos a o

Weakening a => Weakening (TrBr a o)

Defined in Agda.Auto.Syntax

Methods

weak' :: Nat -> TrBr a o -> TrBr a o

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

Substituting for a variable.

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

FreeVars class and instances

class FreeVars t where

Methods

freeVarsOffset :: Nat -> t -> Set Nat

Instances

FreeVars t => FreeVars (Abs t)

Defined in Agda.Auto.Syntax

Methods

freeVarsOffset :: Nat -> Abs t -> Set Nat

FreeVars (ArgList o)

Defined in Agda.Auto.Syntax

Methods

freeVarsOffset :: Nat -> ArgList o -> Set Nat

FreeVars (Elr o)

Defined in Agda.Auto.Syntax

Methods

freeVarsOffset :: Nat -> Elr o -> Set Nat

FreeVars (Exp o)

Defined in Agda.Auto.Syntax

Methods

freeVarsOffset :: Nat -> Exp o -> Set Nat

FreeVars t => FreeVars (MM t a)

Defined in Agda.Auto.Syntax

Methods

freeVarsOffset :: Nat -> MM t a -> Set Nat

(FreeVars a, FreeVars b) => FreeVars (a, b)

Defined in Agda.Auto.Syntax

Methods

freeVarsOffset :: Nat -> (a, b) -> Set Nat

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

Renaming Typeclass and instances

class Renaming t where

Methods

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

Instances

Renaming (CSPatI o)

Defined in Agda.Auto.CaseSplit

Methods

renameOffset :: Nat -> (Nat -> Nat) -> CSPatI o -> CSPatI o

Renaming t => Renaming (HI t)

Defined in Agda.Auto.CaseSplit

Methods

renameOffset :: Nat -> (Nat -> Nat) -> HI t -> HI t

Renaming t => Renaming (Abs t)

Defined in Agda.Auto.Syntax

Methods

renameOffset :: Nat -> (Nat -> Nat) -> Abs t -> Abs t

Renaming (ArgList o)

Defined in Agda.Auto.Syntax

Methods

renameOffset :: Nat -> (Nat -> Nat) -> ArgList o -> ArgList o

Renaming (Elr o)

Defined in Agda.Auto.Syntax

Methods

renameOffset :: Nat -> (Nat -> Nat) -> Elr o -> Elr o

Renaming (Exp o)

Defined in Agda.Auto.Syntax

Methods

renameOffset :: Nat -> (Nat -> Nat) -> Exp o -> Exp o

Renaming t => Renaming (MM t a)

Defined in Agda.Auto.Syntax

Methods

renameOffset :: Nat -> (Nat -> Nat) -> MM t a -> MM t a

(Renaming a, Renaming b) => Renaming (a, b)

Defined in Agda.Auto.Syntax

Methods

renameOffset :: Nat -> (Nat -> Nat) -> (a, b) -> (a, b)