| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.TypeChecking.Rules.Application
Synopsis
- checkArguments :: Comparison -> ExpandHidden -> Expr -> [NamedArg Expr] -> Type -> Type -> (ArgsCheckState CheckedTarget -> TCM Term) -> TCM Term
- checkArguments_ :: Comparison -> ExpandHidden -> Expr -> [NamedArg Expr] -> Telescope -> TCM (Elims, Telescope)
- checkApplication :: Comparison -> Expr -> Args -> Expr -> Type -> TCM Term
- inferApplication :: ExpandHidden -> Expr -> Args -> Expr -> TCM (Term, Type)
- checkProjAppToKnownPrincipalArg :: Comparison -> Expr -> ProjOrigin -> List1 QName -> Expr -> Args -> Type -> Int -> Term -> Type -> PrincipalArgTypeMetas -> TCM Term
- disambiguateConstructor' :: ConstructorDisambiguationData -> (ConHead -> TCM Term) -> TCM Term
- univChecks :: Univ -> TCM ()
- suffixToLevel :: Suffix -> Integer
Documentation
Arguments
| :: Comparison | How the inferred type should be compared to the expected result type. |
| -> ExpandHidden | Insert trailing hidden arguments? |
| -> Expr | The function (a head). |
| -> [NamedArg Expr] | The arguments to check. |
| -> Type | Type of the function. |
| -> Type | Expected result type (type of the whole application). |
| -> (ArgsCheckState CheckedTarget -> TCM Term) | Continuation receiving the check arguments. |
| -> TCM Term |
checkArguments cmp exph hd args t0 t k tries checkArgumentsE cmp exph hd args t0 t.
If it succeeds, it continues k with the returned results. If it fails,
it registers a postponed typechecking problem and returns the resulting new
meta variable.
Checks e := ((hd : t0) args) : t.
Arguments
| :: Comparison | Comparison for target |
| -> ExpandHidden | Eagerly insert trailing hidden arguments? |
| -> Expr | Function. |
| -> [NamedArg Expr] | Arguments to check. |
| -> Telescope | Telescope to check arguments against. |
| -> TCM (Elims, Telescope) | Checked arguments and remaining telescope if successful. |
Check that a list of arguments fits a telescope. Inserts hidden arguments as necessary. Returns the type-checked arguments and the remaining telescope.
checkApplication :: Comparison -> Expr -> Args -> Expr -> Type -> TCM Term Source #
checkApplication hd args e t checks an application.
Precondition: Application hs args = appView e
checkApplication disambiguates constructors
(and continues to checkConstructorApplication)
and resolves pattern synonyms.
inferApplication :: ExpandHidden -> Expr -> Args -> Expr -> TCM (Term, Type) Source #
Precondition: Application hd args = appView e.
checkProjAppToKnownPrincipalArg :: Comparison -> Expr -> ProjOrigin -> List1 QName -> Expr -> Args -> Type -> Int -> Term -> Type -> PrincipalArgTypeMetas -> TCM Term Source #
Checking the type of an overloaded projection application.
See inferOrCheckProjAppToKnownPrincipalArg.
disambiguateConstructor' :: ConstructorDisambiguationData -> (ConHead -> TCM Term) -> TCM Term Source #
Retry a constructor disambiguation.
univChecks :: Univ -> TCM () Source #
suffixToLevel :: Suffix -> Integer Source #