Safe Haskell	Safe-Inferred
Language	Haskell2010

Agda.TypeChecking.Rules.Def

Contents

Definitions by pattern matching
Info that is needed after all clauses have been processed.

Synopsis

checkFunDef :: DefInfo -> QName -> [Clause] -> TCM ()
checkMacroType :: Type -> TCM ()
isAlias :: [Clause] -> Type -> Maybe (Expr, Maybe Expr, MetaId)
checkAlias :: Type -> ArgInfo -> DefInfo -> QName -> Expr -> Maybe Expr -> TCM ()
checkFunDef' :: Type -> ArgInfo -> Maybe ExtLamInfo -> Maybe QName -> DefInfo -> QName -> [Clause] -> TCM ()
checkFunDefS :: Type -> ArgInfo -> Maybe ExtLamInfo -> Maybe QName -> DefInfo -> QName -> Maybe Substitution -> [Clause] -> TCM ()
useTerPragma :: Definition -> TCM Definition
mapLHSCores :: (LHSCore -> LHSCore) -> RHS -> RHS
insertNames :: [Arg (Maybe BindName)] -> RHS -> RHS
insertInspects :: [Arg (Maybe BindName)] -> LHSCore -> LHSCore
insertPatterns :: [Arg Pattern] -> RHS -> RHS
insertPatternsLHSCore :: [Arg Pattern] -> LHSCore -> LHSCore
data WithFunctionProblem
- = NoWithFunction
- | WithFunction {
  - wfParentName :: QName
  - wfName :: QName
  - wfParentType :: Type
  - wfParentTel :: Telescope
  - wfBeforeTel :: Telescope
  - wfAfterTel :: Telescope
  - wfExprs :: [Arg (Term, EqualityView)]
  - wfRHSType :: Type
  - wfParentPats :: [NamedArg DeBruijnPattern]
  - wfParentParams :: Nat
  - wfPermSplit :: Permutation
  - wfPermParent :: Permutation
  - wfPermFinal :: Permutation
  - wfClauses :: List1 Clause
  - wfCallSubst :: Substitution
  }
checkSystemCoverage :: QName -> [Int] -> Type -> [Clause] -> TCM System
data ClausesPostChecks = CPC {
- cpcPartialSplits :: IntSet
}
checkClauseLHS :: Type -> Maybe Substitution -> SpineClause -> (LHSResult -> TCM a) -> TCM a
checkClause :: Type -> Maybe Substitution -> SpineClause -> TCM (Clause, ClausesPostChecks)
getReflPattern :: TCM Pattern
checkRHS :: LHSInfo -> QName -> [NamedArg Pattern] -> Type -> LHSResult -> RHS -> TCM (Maybe Term, WithFunctionProblem)
checkWithRHS :: QName -> QName -> Type -> LHSResult -> [Arg (Term, EqualityView)] -> List1 Clause -> TCM (Maybe Term, WithFunctionProblem)
checkWithFunction :: [Name] -> WithFunctionProblem -> TCM (Maybe Term)
checkWhere :: WhereDeclarations -> TCM a -> TCM a
newSection :: Erased -> ModuleName -> GeneralizeTelescope -> TCM a -> TCM a
atClause :: QName -> Int -> Type -> Maybe Substitution -> SpineClause -> TCM a -> TCM a

Definitions by pattern matching

checkFunDef :: DefInfo -> QName -> [Clause] -> TCM () Source #

checkMacroType :: Type -> TCM () Source #

isAlias :: [Clause] -> Type -> Maybe (Expr, Maybe Expr, MetaId) Source #

A single clause without arguments and without type signature is an alias.

checkAlias :: Type -> ArgInfo -> DefInfo -> QName -> Expr -> Maybe Expr -> TCM () Source #

Check a trivial definition of the form f = e

checkFunDef' Source #

Arguments

:: Type	the type we expect the function to have
-> ArgInfo	is it irrelevant (for instance)
-> Maybe ExtLamInfo	does the definition come from an extended lambda (if so, we need to know some stuff about lambda-lifted args)
-> Maybe QName	is it a with function (if so, what's the name of the parent function)
-> DefInfo	range info
-> QName	the name of the function
-> [Clause]	the clauses to check
-> TCM ()

Type check a definition by pattern matching.

checkFunDefS Source #

Arguments

:: Type	the type we expect the function to have
-> ArgInfo	is it irrelevant (for instance)
-> Maybe ExtLamInfo	does the definition come from an extended lambda (if so, we need to know some stuff about lambda-lifted args)
-> Maybe QName	is it a with function (if so, what's the name of the parent function)
-> DefInfo	range info
-> QName	the name of the function
-> Maybe Substitution	substitution (from with abstraction) that needs to be applied to module parameters
-> [Clause]	the clauses to check
-> TCM ()

Type check a definition by pattern matching.

useTerPragma :: Definition -> TCM Definition Source #

Set funTerminates according to termination info in TCEnv, which comes from a possible termination pragma.

mapLHSCores :: (LHSCore -> LHSCore) -> RHS -> RHS Source #

Modify all the LHSCore of the given RHS. (Used to insert patterns for rewrite or the inspect idiom)

insertNames :: [Arg (Maybe BindName)] -> RHS -> RHS Source #

Insert some names into the with-clauses LHS of the given RHS. (Used for the inspect idiom)

insertInspects :: [Arg (Maybe BindName)] -> LHSCore -> LHSCore Source #

insertPatterns :: [Arg Pattern] -> RHS -> RHS Source #

Insert some with-patterns into the with-clauses LHS of the given RHS. (Used for rewrite)

insertPatternsLHSCore :: [Arg Pattern] -> LHSCore -> LHSCore Source #

Insert with-patterns before the trailing with patterns. If there are none, append the with-patterns.

data WithFunctionProblem Source #

Parameters for creating a with-function.

Constructors

NoWithFunction
WithFunction
Fields wfParentName :: QName Parent function name. wfName :: QName With function name. wfParentType :: Type Type of the parent function. wfParentTel :: Telescope Context of the parent patterns. wfBeforeTel :: Telescope Types of arguments to the with function before the with expressions (needed vars). wfAfterTel :: Telescope Types of arguments to the with function after the with expressions (unneeded vars). wfExprs :: [Arg (Term, EqualityView)] With and rewrite expressions and their types. wfRHSType :: Type Type of the right hand side. wfParentPats :: [NamedArg DeBruijnPattern] Parent patterns. wfParentParams :: Nat Number of module parameters in parent patterns wfPermSplit :: Permutation Permutation resulting from splitting the telescope into needed and unneeded vars. wfPermParent :: Permutation Permutation reordering the variables in the parent pattern. wfPermFinal :: Permutation Final permutation (including permutation for the parent clause). wfClauses :: List1 Clause The given clauses for the with function wfCallSubst :: Substitution Subtsitution to generate call for the parent.

checkSystemCoverage :: QName -> [Int] -> Type -> [Clause] -> TCM System Source #

Info that is needed after all clauses have been processed.

data ClausesPostChecks Source #

Constructors

CPC
Fields cpcPartialSplits :: IntSet Which argument indexes have a partial split.

Instances

Instances details

Monoid ClausesPostChecks Source #
Instance details Defined in Agda.TypeChecking.Rules.Def Methods mempty :: ClausesPostChecks # mappend :: ClausesPostChecks -> ClausesPostChecks -> ClausesPostChecks # mconcat :: [ClausesPostChecks] -> ClausesPostChecks #
Semigroup ClausesPostChecks Source #
Instance details Defined in Agda.TypeChecking.Rules.Def Methods (<>) :: ClausesPostChecks -> ClausesPostChecks -> ClausesPostChecks # sconcat :: NonEmpty ClausesPostChecks -> ClausesPostChecks # stimes :: Integral b => b -> ClausesPostChecks -> ClausesPostChecks #

checkClauseLHS :: Type -> Maybe Substitution -> SpineClause -> (LHSResult -> TCM a) -> TCM a Source #

The LHS part of checkClause.

checkClause Source #

Arguments

:: Type	Type of function defined by this clause.
-> Maybe Substitution	Module parameter substitution arising from with-abstraction.
-> SpineClause	Clause.
-> TCM (Clause, ClausesPostChecks)	Type-checked clause

Type check a function clause.

getReflPattern :: TCM Pattern Source #

Generate the abstract pattern corresponding to Refl

checkRHS Source #

Arguments

:: LHSInfo	Range of lhs.
-> QName	Name of function.
-> [NamedArg Pattern]	Patterns in lhs.
-> Type	Top-level type of function.
-> LHSResult	Result of type-checking patterns
-> RHS	Rhs to check.
-> TCM (Maybe Term, WithFunctionProblem)

Type check the with and rewrite lhss and/or the rhs.

checkWithRHS Source #

Arguments

:: QName	Name of function.
-> QName	Name of the with-function.
-> Type	Type of function.
-> LHSResult	Result of type-checking patterns
-> [Arg (Term, EqualityView)]	Expressions and types of with-expressions.
-> List1 Clause	With-clauses to check.
-> TCM (Maybe Term, WithFunctionProblem)

checkWithFunction :: [Name] -> WithFunctionProblem -> TCM (Maybe Term) Source #

Invoked in empty context.

checkWhere Source #

Arguments

:: WhereDeclarations	Where-declarations to check.
-> TCM a	Continuation.
-> TCM a

Type check a where clause.

newSection :: Erased -> ModuleName -> GeneralizeTelescope -> TCM a -> TCM a Source #

Enter a new section during type-checking.

atClause :: QName -> Int -> Type -> Maybe Substitution -> SpineClause -> TCM a -> TCM a Source #

Set the current clause number.