Safe Haskell	None
Language	Haskell2010

Mikan.TypeChecking.Rules.WithApp

Synopsis

checkWithAppHead :: Comparison -> Type -> Expr -> Term -> List1 Expr -> TCM Term
checkWithApplication :: Comparison -> Type -> WithAppHead -> QName -> Elims -> List1 Expr -> TCM Term

Documentation

checkWithAppHead Source #

Arguments

:: Comparison	How to check the target type
-> Type	Expected type
-> Expr	Abstract expression from which `tm` was elaborated, used for error reporting
-> Term	The term `tm` we want to apply
-> List1 Expr	Nonempty list of "piped" expressions
-> TCM Term

checkWithApplication Source #

Arguments

:: Comparison	How to check the target type
-> Type	Expected type
-> WithAppHead	Head expression, used for error reporting; shape does not matter
-> QName	Head symbol `f` of the left-hand side
-> Elims	Checked eliminations `es0` on the head symbol
-> List1 Expr	Nonempty list of "piped" expressions
-> TCM Term

Check that an application of a defined name to some eliminations can be the head of a with-application, and elaborate the given abstract expressions into arguments for the corresponding with-function.

The application f es0 of the head symbol should reduce in a single step of co/pattern matching (see unfoldDefinitionStep) to a with-function associated to f. This is a liberal approximation to "es0 matches a with-clause of f" that is guaranteed not to diverge from the implementation of pattern matching used for ordinary reduction, but it does technically allow re-applying a recursive with-application of f.

Finally, check that the part of the head function's telescope that was abstracted of the with-expressions remains valid with the new arguments, and that the overall expression has the given target type.