Safe Haskell	None
Language	Haskell2010

Mikan.TypeChecking.Rules.LHS

Synopsis

checkLeftHandSide :: Call -> Range -> LetOrClause -> [NamedArg Pattern] -> Type -> Maybe Substitution -> [ProblemEq] -> (LHSResult -> TCM a) -> TCM a
data LHSResult = LHSResult {
- lhsParameters :: Nat
- lhsVarTele :: Telescope
- lhsPatterns :: [NamedArg DeBruijnPattern]
- lhsHasAbsurd :: Bool
- lhsBodyType :: Type
- lhsPatSubst :: Substitution
- lhsAsBindings :: [AsBinding]
- lhsPartialSplit :: IntSet
- lhsIndexedSplit :: Bool
}
bindAsPatterns :: [AsBinding] -> TCM a -> TCM a
class IsFlexiblePattern a where
- maybeFlexiblePattern :: forall (m :: Type -> Type). HasConstInfo m => a -> MaybeT m FlexibleVarKind
- isFlexiblePattern :: HasConstInfo m => a -> m Bool
type DataOrRecord = DataOrRecord' InductionAndEta
checkSortOfSplitVar :: (MonadTCM m, PureTCM m, MonadError TCErr m, LensSort a, PrettyTCM a, LensSort ty, PrettyTCM ty) => DataOrRecord -> a -> Telescope -> Maybe ty -> m ()
data LetOrClause
- = LetLHS
- | ClauseLHS QName
buildLHSSubstitutions :: Context -> NAPs -> LHSSubstitutionCase -> (Substitution, Substitution)
data LHSSubstitutionCase
- = NormalFunSubst
- | WithFunSubst Int Substitution

Documentation

checkLeftHandSide Source #

Arguments

:: Call	Trace, e.g. `CheckLHS` or `CheckPattern`.
-> Range	`Range` of the entire left hand side, for error reporting.
-> LetOrClause	Are we checking a let-pattern or a function clause?
-> [NamedArg Pattern]	The patterns.
-> Type	The expected type `a = Γ → b`.
-> Maybe Substitution	Module parameter substitution from with-abstraction.
-> [ProblemEq]	Patterns that have been stripped away by with-desugaring. ^ These should not contain any proper matches.
-> (LHSResult -> TCM a)	Continuation.
-> TCM a

Check a LHS. Main function.

checkLeftHandSide a ps a ret checks that user patterns ps eliminate the type a of the defined function, and calls continuation ret if successful.

data LHSResult Source #

Result of checking the LHS of a clause.

Constructors

LHSResult

Fields

lhsParameters :: Nat
The number of original module parameters. These are present in the the patterns.
lhsVarTele :: Telescope
Δ : The types of the pattern variables, in internal dependency order. Corresponds to clauseTel.
lhsPatterns :: [NamedArg DeBruijnPattern]
The patterns in internal syntax.
lhsHasAbsurd :: Bool
Whether the LHS has at least one absurd pattern.
lhsBodyType :: Type
The type of the body. Is bσ if Γ is defined.
lhsPatSubst :: Substitution
Substitution version of lhsPatterns, only up to the first projection pattern. Δ |- lhsPatSubst : Γ. Where Γ is the argument telescope of the function. This is used to update inherited dot patterns in with-function clauses.
lhsAsBindings :: [AsBinding]
As-bindings from the left-hand side. Return instead of bound since we want them in where's and right-hand sides, but not in with-clauses (Issue 2303).
lhsPartialSplit :: IntSet
have we done a partial split?
lhsIndexedSplit :: Bool
have we split on an indexed type?

Instances

Instances details

InstantiateFull LHSResult Source #
Instance details Defined in Mikan.TypeChecking.Rules.LHS Methods instantiateFull' :: LHSResult -> ReduceM LHSResult Source #

bindAsPatterns :: [AsBinding] -> TCM a -> TCM a Source #

Bind as patterns

class IsFlexiblePattern a where Source #

A pattern is flexible if it is dotted or implicit, or a record pattern with only flexible subpatterns.

Minimal complete definition

maybeFlexiblePattern

Methods

maybeFlexiblePattern :: forall (m :: Type -> Type). HasConstInfo m => a -> MaybeT m FlexibleVarKind Source #

isFlexiblePattern :: HasConstInfo m => a -> m Bool Source #

Instances

Instances details

IsFlexiblePattern Pattern Source #
Instance details Defined in Mikan.TypeChecking.Rules.LHS Methods maybeFlexiblePattern :: forall (m :: Type -> Type). HasConstInfo m => Pattern -> MaybeT m FlexibleVarKind Source # isFlexiblePattern :: HasConstInfo m => Pattern -> m Bool Source #
IsFlexiblePattern a => IsFlexiblePattern (Arg a) Source #
Instance details Defined in Mikan.TypeChecking.Rules.LHS Methods maybeFlexiblePattern :: forall (m :: Type -> Type). HasConstInfo m => Arg a -> MaybeT m FlexibleVarKind Source # isFlexiblePattern :: HasConstInfo m => Arg a -> m Bool Source #
IsFlexiblePattern (Pattern' a) Source #
Instance details Defined in Mikan.TypeChecking.Rules.LHS Methods maybeFlexiblePattern :: forall (m :: Type -> Type). HasConstInfo m => Pattern' a -> MaybeT m FlexibleVarKind Source # isFlexiblePattern :: HasConstInfo m => Pattern' a -> m Bool Source #
IsFlexiblePattern a => IsFlexiblePattern [a] Source #	Lists of flexible patterns are `RecordFlex`.
Instance details Defined in Mikan.TypeChecking.Rules.LHS Methods maybeFlexiblePattern :: forall (m :: Type -> Type). HasConstInfo m => [a] -> MaybeT m FlexibleVarKind Source # isFlexiblePattern :: HasConstInfo m => [a] -> m Bool Source #
IsFlexiblePattern a => IsFlexiblePattern (Named name a) Source #
Instance details Defined in Mikan.TypeChecking.Rules.LHS Methods maybeFlexiblePattern :: forall (m :: Type -> Type). HasConstInfo m => Named name a -> MaybeT m FlexibleVarKind Source # isFlexiblePattern :: HasConstInfo m => Named name a -> m Bool Source #

type DataOrRecord = DataOrRecord' InductionAndEta Source #

checkSortOfSplitVar :: (MonadTCM m, PureTCM m, MonadError TCErr m, LensSort a, PrettyTCM a, LensSort ty, PrettyTCM ty) => DataOrRecord -> a -> Telescope -> Maybe ty -> m () Source #

data LetOrClause Source #

Are we checking the LHS of a let-pattern binding or a function clause?

Constructors

LetLHS	Checking a pattern bound by a let.
ClauseLHS QName	Checking the LHS of a clause of the function with the given `QName`.

buildLHSSubstitutions :: Context -> NAPs -> LHSSubstitutionCase -> (Substitution, Substitution) Source #

Compute substitution from the out patterns ps

data LHSSubstitutionCase Source #

Building substitutions from out patterns needs to handle with-functions specially.

Constructors

NormalFunSubst
WithFunSubst Int Substitution