Agda-2.8.0: A dependently typed functional programming language and proof assistant

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

checkArguments Source #

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

checkArguments_ Source #

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 #