ModuleAgda-2.8.0.2Haskell2010

Agda.TypeChecking.Rules.Def

2 types
22 values

PackageAgda-2.8.0.2
Exports24
LanguageHaskell2010
LicenceMIT
SourceDef.hs

Definitions by pattern matching

14 declarations

valuecheckFunDef :: DefInfo -> QName -> [Clause] -> TCM ()

valuecheckMacroType :: Type -> TCM ()

valueisAlias :: [Clause] -> Type -> Maybe (Expr, Maybe Expr, MetaId)

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

valuecheckAlias

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

Check a trivial definition of the form f = e

valuecheckFunDef'

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

valuecheckFunDefS

:: 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, Map Name LetBinding)
substitution (from with abstraction) that needs to be applied to module parameters, and let-bindings inherited from parent clause
-> [Clause]
the clauses to check
-> TCM ()

Type check a definition by pattern matching.

valueuseTerPragma :: Definition -> TCM Definition

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

valuemapLHSCores :: (LHSCore -> LHSCore) -> RHS -> RHS

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

valueinsertNames :: List1 (Arg (Maybe BindName)) -> RHS -> RHS

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

valueinsertInspects :: List1 (Arg (Maybe BindName)) -> LHSCore -> LHSCore

valueinsertPatterns :: List1 (Arg Pattern) -> RHS -> RHS

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

valueinsertPatternsLHSCore :: List1 (Arg Pattern) -> LHSCore -> LHSCore

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

datadata WithFunctionProblem

Parameters for creating a with-function.

Constructors

NoWithFunction
WithFunction
- 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 :: List1 (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
  Substitution to generate call for the parent.
- wfLetBindings :: Map Name LetBinding
  The let-bindings in scope of the parent (in the parent context).

valuecheckSystemCoverage :: QName -> [Int] -> Type -> [Clause] -> TCM System

Info that is needed after all clauses have been processed.

10 declarations

datadata ClausesPostChecks

Constructors

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

Instances2Semigroup, Monoid

Semigroup ClausesPostChecksDefined in Agda-2.8.0.2 · Agda.TypeChecking.Rules.Def
Monoid ClausesPostChecksDefined in Agda-2.8.0.2 · Agda.TypeChecking.Rules.Def

valuecheckClauseLHS

:: Type
-> Maybe Substitution
-> SpineClause
-> LHSResult -> TCM a
-> TCM a

The LHS part of checkClause.

valuecheckClause

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

Type check a function clause.

valuegetReflPattern :: TCM Pattern

Generate the abstract pattern corresponding to Refl

valuecheckRHS

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

valuecheckWithRHS

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

valuecheckWithFunction :: [Name] -> WithFunctionProblem -> TCM (Maybe Term)

Invoked in empty context.

valuecheckWhere

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

Type check a where clause.

valuenewSection :: Erased -> ModuleName -> GeneralizeTelescope -> TCM a -> TCM a

Enter a new section during type-checking.

valueatClause

:: QName
-> Int
-> Type
-> Maybe Substitution
-> SpineClause
-> TCM a
-> TCM a

Set the current clause number.