Safe Haskell | None |
---|---|
Language | Haskell2010 |
- isType :: Expr -> Sort -> TCM Type
- isType_ :: Expr -> TCM Type
- ptsRule :: (LensSort a, LensSort b) => a -> b -> TCM Sort
- noFunctionsIntoSize :: Type -> Type -> TCM ()
- isTypeEqualTo :: Expr -> Type -> TCM Type
- leqType_ :: Type -> Type -> TCM ()
- checkTelescope :: Telescope -> (Telescope -> TCM a) -> TCM a
- checkPiTelescope :: Telescope -> (Telescope -> TCM a) -> TCM a
- data LamOrPi
- checkTelescope' :: LamOrPi -> Telescope -> (Telescope -> TCM a) -> TCM a
- checkTypedBindings :: LamOrPi -> TypedBindings -> (Telescope -> TCM a) -> TCM a
- checkTypedBinding :: LamOrPi -> ArgInfo -> TypedBinding -> (ListTel -> TCM a) -> TCM a
- checkLambda :: Arg TypedBinding -> Expr -> Type -> TCM Term
- checkPostponedLambda :: Arg ([WithHiding Name], Maybe Type) -> Expr -> Type -> TCM Term
- insertHiddenLambdas :: Hiding -> Type -> (MetaId -> Type -> TCM Term) -> (Type -> TCM Term) -> TCM Term
- checkAbsurdLambda :: ExprInfo -> Hiding -> Expr -> Type -> TCM Term
- checkExtendedLambda :: ExprInfo -> DefInfo -> QName -> [Clause] -> Expr -> Type -> TCM Term
- catchIlltypedPatternBlockedOnMeta :: TCM () -> TCM (Maybe (TCErr, MetaId))
- expandModuleAssigns :: [Either Assign ModuleName] -> [Name] -> TCM Assigns
- checkRecordExpression :: RecordAssigns -> Expr -> Type -> TCM Term
- checkRecordUpdate :: ExprInfo -> Expr -> Assigns -> Expr -> Type -> TCM Term
- checkLiteral :: Literal -> Type -> TCM Term
- checkArguments' :: ExpandHidden -> Range -> [NamedArg Expr] -> Type -> Type -> (Args -> Type -> TCM Term) -> TCM Term
- scopedExpr :: Expr -> TCM Expr
- checkExpr :: Expr -> Type -> TCM Term
- quoteGoal :: Type -> TCM (Either [MetaId] Term)
- quoteContext :: TCM (Either [MetaId] Term)
- unquoteM :: Expr -> Term -> Type -> TCM Term -> TCM Term
- unquoteTactic :: Term -> Term -> Type -> TCM Term -> TCM Term
- inferProjApp :: Expr -> ProjOrigin -> [QName] -> Args -> TCM (Term, Type)
- checkProjApp :: Expr -> ProjOrigin -> [QName] -> Args -> Type -> TCM Term
- inferOrCheckProjApp :: Expr -> ProjOrigin -> [QName] -> Args -> Maybe Type -> TCM (Term, Type)
- checkApplication :: Expr -> Args -> Expr -> Type -> TCM Term
- checkQuestionMark :: (Type -> TCM (MetaId, Term)) -> Type -> MetaInfo -> InteractionId -> TCM Term
- checkUnderscore :: Type -> MetaInfo -> TCM Term
- checkMeta :: (Type -> TCM (MetaId, Term)) -> Type -> MetaInfo -> TCM Term
- inferMeta :: (Type -> TCM (MetaId, Term)) -> MetaInfo -> TCM (Args -> Term, Type)
- checkOrInferMeta :: (Type -> TCM (MetaId, Term)) -> Maybe Type -> MetaInfo -> TCM (Term, Type)
- domainFree :: ArgInfo -> Name -> LamBinding
- inferHeadDef :: ProjOrigin -> QName -> TCM (Args -> Term, Type)
- inferHead :: Expr -> TCM (Args -> Term, Type)
- inferDef :: (Args -> Term) -> QName -> TCM (Term, Type)
- checkConstructorApplication :: Expr -> Type -> ConHead -> [NamedArg Expr] -> TCM Term
- checkHeadApplication :: Expr -> Type -> Expr -> [NamedArg Expr] -> TCM Term
- traceCallE :: Call -> ExceptT e TCM r -> ExceptT e TCM r
- checkKnownArguments :: [NamedArg Expr] -> Args -> Type -> TCM (Args, Type)
- checkKnownArgument :: NamedArg Expr -> Args -> Type -> TCM (Args, Type)
- checkNamedArg :: NamedArg Expr -> Type -> TCM Term
- checkArguments :: ExpandHidden -> Range -> [NamedArg Expr] -> Type -> Type -> ExceptT (Args, [NamedArg Expr], Type) TCM (Args, Type)
- checkArguments_ :: ExpandHidden -> Range -> [NamedArg Expr] -> Telescope -> TCM (Args, Telescope)
- inferExpr :: Expr -> TCM (Term, Type)
- inferExpr' :: ExpandHidden -> Expr -> TCM (Term, Type)
- defOrVar :: Expr -> Bool
- checkDontExpandLast :: Expr -> Type -> TCM Term
- isModuleFreeVar :: Int -> TCM Bool
- inferExprForWith :: Expr -> TCM (Term, Type)
- checkLetBindings :: [LetBinding] -> TCM a -> TCM a
- checkLetBinding :: LetBinding -> TCM a -> TCM a
Types
noFunctionsIntoSize :: Type -> Type -> TCM () Source #
Ensure that a (freshly created) function type does not inhabit SizeUniv
.
Precondition: When noFunctionsIntoSize t tBlame
is called,
we are in the context of tBlame
in order to print it correctly.
Not being in context of t
should not matter, as we are only
checking whether its sort reduces to SizeUniv
.
isTypeEqualTo :: Expr -> Type -> TCM Type Source #
Check that an expression is a type which is equal to a given type.
Telescopes
checkTelescope :: Telescope -> (Telescope -> TCM a) -> TCM a Source #
Type check a (module) telescope. Binds the variables defined by the telescope.
checkPiTelescope :: Telescope -> (Telescope -> TCM a) -> TCM a Source #
Type check the telescope of a dependent function type. Binds the resurrected variables defined by the telescope. The returned telescope is unmodified (not resurrected).
Flag to control resurrection on domains.
LamNotPi | We are checking a module telescope. We pass into the type world to check the domain type. This resurrects the whole context. |
PiNotLam | We are checking a telescope in a Pi-type. We stay in the term world, but add resurrected domains to the context to check the remaining domains and codomain of the Pi-type. |
checkTelescope' :: LamOrPi -> Telescope -> (Telescope -> TCM a) -> TCM a Source #
Type check a telescope. Binds the variables defined by the telescope.
checkTypedBindings :: LamOrPi -> TypedBindings -> (Telescope -> TCM a) -> TCM a Source #
Check a typed binding and extends the context with the bound variables. The telescope passed to the continuation is valid in the original context.
Parametrized by a flag wether we check a typed lambda or a Pi. This flag is needed for irrelevance.
checkTypedBinding :: LamOrPi -> ArgInfo -> TypedBinding -> (ListTel -> TCM a) -> TCM a Source #
Lambda abstractions
checkLambda :: Arg TypedBinding -> Expr -> Type -> TCM Term Source #
Type check a lambda expression.
checkPostponedLambda :: Arg ([WithHiding Name], Maybe Type) -> Expr -> Type -> TCM Term Source #
Checking a lambda whose domain type has already been checked.
:: Hiding | Expected hiding. |
-> Type | Expected to be a function type. |
-> (MetaId -> Type -> TCM Term) | Continuation on blocked type. |
-> (Type -> TCM Term) | Continuation when expected hiding found.
The continuation may assume that the |
-> TCM Term | Term with hidden lambda inserted. |
Insert hidden lambda until the hiding info of the domain type
matches the expected hiding info.
Throws WrongHidingInLambda
checkAbsurdLambda :: ExprInfo -> Hiding -> Expr -> Type -> TCM Term Source #
checkAbsurdLambda i h e t
checks absurd lambda against type t
.
Precondition: e = AbsurdLam i h
checkExtendedLambda :: ExprInfo -> DefInfo -> QName -> [Clause] -> Expr -> Type -> TCM Term Source #
checkExtendedLambda i di qname cs e t
check pattern matching lambda.
Precondition: e = ExtendedLam i di qname cs
catchIlltypedPatternBlockedOnMeta :: TCM () -> TCM (Maybe (TCErr, MetaId)) Source #
Run a computation.
- If successful, return Nothing.
- If
IlltypedPattern p a
is thrown and typea
is blocked on some metax
returnJust x
. Note that the returned meta might only exists in the state where the error was thrown, thus, be an invalidMetaId
in the current state. - If another error was thrown or the type
a
is not blocked, reraise the error.
Records
expandModuleAssigns :: [Either Assign ModuleName] -> [Name] -> TCM Assigns Source #
checkRecordExpression :: RecordAssigns -> Expr -> Type -> TCM Term Source #
checkRecordExpression fs e t
checks record construction against type t
.
Precondition e = Rec _ fs
.
checkRecordUpdate :: ExprInfo -> Expr -> Assigns -> Expr -> Type -> TCM Term Source #
checkRecordUpdate ei recexpr fs e t
Precondition e = RecUpdate ei recexpr fs
.
Literal
Terms
checkArguments' :: ExpandHidden -> Range -> [NamedArg Expr] -> Type -> Type -> (Args -> Type -> TCM Term) -> TCM Term Source #
checkArguments' exph r args t0 t k
tries checkArguments exph 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 := ((_ : t0) args) : t
.
scopedExpr :: Expr -> TCM Expr Source #
Remove top layers of scope info of expression and set the scope accordingly
in the TCState
.
Reflection
unquoteM :: Expr -> Term -> Type -> TCM Term -> TCM Term Source #
Unquote a TCM computation in a given hole.
Projections
inferProjApp :: Expr -> ProjOrigin -> [QName] -> Args -> TCM (Term, Type) Source #
Inferring the type of an overloaded projection application.
See inferOrCheckProjApp
.
checkProjApp :: Expr -> ProjOrigin -> [QName] -> Args -> Type -> TCM Term Source #
Checking the type of an overloaded projection application.
See inferOrCheckProjApp
.
:: Expr | The whole expression which constitutes the application. |
-> ProjOrigin | The origin of the projection involved in this projection application. |
-> [QName] | The projection name (potentially ambiguous). List must not be empty. |
-> Args | The arguments to the projection. |
-> Maybe Type | The expected type of the expression (if |
-> TCM (Term, Type) | The type-checked expression and its type (if successful). |
Inferring or Checking an overloaded projection application.
The overloaded projection is disambiguated by inferring the type of its principal argument, which is the first visible argument.
checkApplication :: 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.
Meta variables
checkQuestionMark :: (Type -> TCM (MetaId, Term)) -> Type -> MetaInfo -> InteractionId -> TCM Term Source #
Check an interaction point without arguments.
checkMeta :: (Type -> TCM (MetaId, Term)) -> Type -> MetaInfo -> TCM Term Source #
Type check a meta variable.
inferMeta :: (Type -> TCM (MetaId, Term)) -> MetaInfo -> TCM (Args -> Term, Type) Source #
Infer the type of a meta variable. If it is a new one, we create a new meta for its type.
checkOrInferMeta :: (Type -> TCM (MetaId, Term)) -> Maybe Type -> MetaInfo -> TCM (Term, Type) Source #
Type check a meta variable. If its type is not given, we return its type, or a fresh one, if it is a new meta. If its type is given, we check that the meta has this type, and we return the same type.
domainFree :: ArgInfo -> Name -> LamBinding Source #
Turn a domain-free binding (e.g. lambda) into a domain-full one, by inserting an underscore for the missing type.
Applications
inferHeadDef :: ProjOrigin -> QName -> TCM (Args -> Term, Type) Source #
inferHead :: Expr -> TCM (Args -> Term, Type) Source #
Infer the type of a head thing (variable, function symbol, or constructor). We return a function that applies the head to arguments. This is because in case of a constructor we want to drop the parameters.
checkConstructorApplication :: Expr -> Type -> ConHead -> [NamedArg Expr] -> TCM Term Source #
Check the type of a constructor application. This is easier than a general application since the implicit arguments can be inserted without looking at the arguments to the constructor.
checkHeadApplication :: Expr -> Type -> Expr -> [NamedArg Expr] -> TCM Term Source #
checkHeadApplication e t hd args
checks that e
has type t
,
assuming that e
has the form hd args
. The corresponding
type-checked term is returned.
If the head term hd
is a coinductive constructor, then a
top-level definition fresh tel = hd args
(where the clause is
delayed) is added, where tel
corresponds to the current
telescope. The returned term is fresh tel
.
Precondition: The head hd
has to be unambiguous, and there should
not be any need to insert hidden lambdas.
:: [NamedArg Expr] | User-supplied arguments (hidden ones may be missing). |
-> Args | Inferred arguments (including hidden ones). |
-> Type | Type of the head (must be Pi-type with enough domains). |
-> TCM (Args, Type) | Remaining inferred arguments, remaining type. |
Check arguments whose value we already know.
This function can be used to check user-supplied parameters we have already computed by inference.
Precondition: The type t
of the head has enough domains.
:: NamedArg Expr | User-supplied argument. |
-> Args | Inferred arguments (including hidden ones). |
-> Type | Type of the head (must be Pi-type with enough domains). |
-> TCM (Args, Type) | Remaining inferred arguments, remaining type. |
Check an argument whose value we already know.
checkArguments :: ExpandHidden -> Range -> [NamedArg Expr] -> Type -> Type -> ExceptT (Args, [NamedArg Expr], Type) TCM (Args, Type) Source #
Check a list of arguments: checkArgs args t0 t1
checks that
t0 = Delta -> t0'
and args : Delta
. Inserts hidden arguments to
make this happen. Returns the evaluated arguments vs
, the remaining
type t0'
(which should be a subtype of t1
) and any constraints cs
that have to be solved for everything to be well-formed.
:: ExpandHidden | Eagerly insert trailing hidden arguments? |
-> Range | Range of application. |
-> [NamedArg Expr] | Arguments to check. |
-> Telescope | Telescope to check arguments against. |
-> TCM (Args, 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.
inferExpr :: Expr -> TCM (Term, Type) Source #
Infer the type of an expression. Implemented by checking against a meta variable. Except for neutrals, for them a polymorphic type is inferred.
inferExpr' :: ExpandHidden -> Expr -> TCM (Term, Type) Source #
checkDontExpandLast :: Expr -> Type -> TCM Term Source #
Used to check aliases f = e
.
Switches off ExpandLast
for the checking of top-level application.
isModuleFreeVar :: Int -> TCM Bool Source #
Check whether a de Bruijn index is bound by a module telescope.
inferExprForWith :: Expr -> TCM (Term, Type) Source #
Infer the type of an expression, and if it is of the form
{tel} -> D vs
for some datatype D
then insert the hidden
arguments. Otherwise, leave the type polymorphic.
Let bindings
checkLetBindings :: [LetBinding] -> TCM a -> TCM a Source #
checkLetBinding :: LetBinding -> TCM a -> TCM a Source #