Safe Haskell	None
Language	Haskell2010

Agda.TypeChecking.Rules.LHS.Problem

Contents

Orphan instances

Synopsis

type FlexibleVars = [FlexibleVar Nat]
data FlexibleVarKind
- = RecordFlex [FlexibleVarKind]
- | ImplicitFlex
- | DotFlex
- | OtherFlex
data FlexibleVar a = FlexibleVar {
- flexArgInfo :: ArgInfo
- flexForced :: IsForced
- flexKind :: FlexibleVarKind
- flexPos :: Maybe Int
- flexVar :: a
}
allFlexVars :: [IsForced] -> Telescope -> FlexibleVars
data FlexChoice
- = ChooseLeft
- | ChooseRight
- | ChooseEither
- | ExpandBoth
class ChooseFlex a where
- chooseFlex :: a -> a -> FlexChoice
data ProblemEq = ProblemEq {
- problemInPat :: Pattern
- problemInst :: Term
- problemType :: Dom Type
}
data Problem a = Problem {
- _problemEqs :: [ProblemEq]
- _problemRestPats :: [NamedArg Pattern]
- _problemCont :: LHSState a -> TCM a
}
problemEqs :: forall a f. Functor f => ([ProblemEq] -> f [ProblemEq]) -> Problem a -> f (Problem a)
problemRestPats :: forall a f. Functor f => ([NamedArg Pattern] -> f [NamedArg Pattern]) -> Problem a -> f (Problem a)
problemCont :: forall a f. Functor f => ((LHSState a -> TCM a) -> f (LHSState a -> TCM a)) -> Problem a -> f (Problem a)
problemInPats :: Problem a -> [Pattern]
data AsBinding = AsB Name Term (Dom Type)
data DotPattern = Dot Expr Term (Dom Type)
data AbsurdPattern = Absurd Range Type
data AnnotationPattern = Ann Expr Type
data LHSState a = LHSState {
- _lhsTel :: Telescope
- _lhsOutPat :: [NamedArg DeBruijnPattern]
- _lhsProblem :: Problem a
- _lhsTarget :: Arg Type
- _lhsPartialSplit :: ![Maybe Int]
- _lhsIndexedSplit :: !Bool
- _lhsMatchPrio :: !MatchPrio
}
lhsTel :: forall a f. Functor f => (Telescope -> f Telescope) -> LHSState a -> f (LHSState a)
lhsOutPat :: forall a f. Functor f => ([NamedArg DeBruijnPattern] -> f [NamedArg DeBruijnPattern]) -> LHSState a -> f (LHSState a)
lhsProblem :: forall a f. Functor f => (Problem a -> f (Problem a)) -> LHSState a -> f (LHSState a)
lhsTarget :: forall a f. Functor f => (Arg Type -> f (Arg Type)) -> LHSState a -> f (LHSState a)
data LeftoverPatterns = LeftoverPatterns {
- patternVariables :: IntMap [(Arg Name, PatVarPosition)]
- asPatterns :: [AsBinding]
- dotPatterns :: [DotPattern]
- absurdPatterns :: [AbsurdPattern]
- typeAnnotations :: [AnnotationPattern]
- otherPatterns :: [Pattern]
}
getLeftoverPatterns :: (PureTCM m, MonadFresh NameId m) => [ProblemEq] -> m LeftoverPatterns
getUserVariableNames :: Telescope -> IntMap [(Arg Name, PatVarPosition)] -> ([Maybe Name], [AsBinding])

Documentation

type FlexibleVars = [FlexibleVar Nat] Source #

data FlexibleVarKind Source #

When we encounter a flexible variable in the unifier, where did it come from? The alternatives are ordered such that we will assign the higher one first, i.e., first we try to assign a DotFlex, then...

Constructors

RecordFlex [FlexibleVarKind]	From a record pattern (`ConP`). Saves the `FlexibleVarKind` of its subpatterns.
ImplicitFlex	From a hidden formal argument or underscore (`WildP`).
DotFlex	From a dot pattern (`DotP`).
OtherFlex	From a non-record constructor or literal (`ConP` or `LitP`).

Instances

Instances details

ChooseFlex FlexibleVarKind Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods chooseFlex :: FlexibleVarKind -> FlexibleVarKind -> FlexChoice Source #
Eq FlexibleVarKind Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods (==) :: FlexibleVarKind -> FlexibleVarKind -> Bool # (/=) :: FlexibleVarKind -> FlexibleVarKind -> Bool #
Show FlexibleVarKind Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods showsPrec :: Int -> FlexibleVarKind -> ShowS # show :: FlexibleVarKind -> String # showList :: [FlexibleVarKind] -> ShowS #

data FlexibleVar a Source #

Flexible variables are equipped with information where they come from, in order to make a choice which one to assign when two flexibles are unified.

Constructors

FlexibleVar
Fields flexArgInfo :: ArgInfo flexForced :: IsForced flexKind :: FlexibleVarKind flexPos :: Maybe Int flexVar :: a

Instances

Instances details

Functor FlexibleVar Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods fmap :: (a -> b) -> FlexibleVar a -> FlexibleVar b # (<$) :: a -> FlexibleVar b -> FlexibleVar a #
Foldable FlexibleVar Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods fold :: Monoid m => FlexibleVar m -> m # foldMap :: Monoid m => (a -> m) -> FlexibleVar a -> m # foldMap' :: Monoid m => (a -> m) -> FlexibleVar a -> m # foldr :: (a -> b -> b) -> b -> FlexibleVar a -> b # foldr' :: (a -> b -> b) -> b -> FlexibleVar a -> b # foldl :: (b -> a -> b) -> b -> FlexibleVar a -> b # foldl' :: (b -> a -> b) -> b -> FlexibleVar a -> b # foldr1 :: (a -> a -> a) -> FlexibleVar a -> a # foldl1 :: (a -> a -> a) -> FlexibleVar a -> a # toList :: FlexibleVar a -> [a] # null :: FlexibleVar a -> Bool # length :: FlexibleVar a -> Int # elem :: Eq a => a -> FlexibleVar a -> Bool # maximum :: Ord a => FlexibleVar a -> a # minimum :: Ord a => FlexibleVar a -> a # sum :: Num a => FlexibleVar a -> a # product :: Num a => FlexibleVar a -> a #
Traversable FlexibleVar Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods traverse :: Applicative f => (a -> f b) -> FlexibleVar a -> f (FlexibleVar b) # sequenceA :: Applicative f => FlexibleVar (f a) -> f (FlexibleVar a) # mapM :: Monad m => (a -> m b) -> FlexibleVar a -> m (FlexibleVar b) # sequence :: Monad m => FlexibleVar (m a) -> m (FlexibleVar a) #
LensArgInfo (FlexibleVar a) Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods getArgInfo :: FlexibleVar a -> ArgInfo Source # setArgInfo :: ArgInfo -> FlexibleVar a -> FlexibleVar a Source # mapArgInfo :: (ArgInfo -> ArgInfo) -> FlexibleVar a -> FlexibleVar a Source #
LensHiding (FlexibleVar a) Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods getHiding :: FlexibleVar a -> Hiding Source # setHiding :: Hiding -> FlexibleVar a -> FlexibleVar a Source # mapHiding :: (Hiding -> Hiding) -> FlexibleVar a -> FlexibleVar a Source #
LensModality (FlexibleVar a) Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods getModality :: FlexibleVar a -> Modality Source # setModality :: Modality -> FlexibleVar a -> FlexibleVar a Source # mapModality :: (Modality -> Modality) -> FlexibleVar a -> FlexibleVar a Source #
LensOrigin (FlexibleVar a) Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods getOrigin :: FlexibleVar a -> Origin Source # setOrigin :: Origin -> FlexibleVar a -> FlexibleVar a Source # mapOrigin :: (Origin -> Origin) -> FlexibleVar a -> FlexibleVar a Source #
ChooseFlex a => ChooseFlex (FlexibleVar a) Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods chooseFlex :: FlexibleVar a -> FlexibleVar a -> FlexChoice Source #
Eq a => Eq (FlexibleVar a) Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods (==) :: FlexibleVar a -> FlexibleVar a -> Bool # (/=) :: FlexibleVar a -> FlexibleVar a -> Bool #
Show a => Show (FlexibleVar a) Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods showsPrec :: Int -> FlexibleVar a -> ShowS # show :: FlexibleVar a -> String # showList :: [FlexibleVar a] -> ShowS #

allFlexVars :: [IsForced] -> Telescope -> FlexibleVars Source #

data FlexChoice Source #

Constructors

ChooseLeft
ChooseRight
ChooseEither
ExpandBoth

Instances

Instances details

Monoid FlexChoice Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods mempty :: FlexChoice # mappend :: FlexChoice -> FlexChoice -> FlexChoice # mconcat :: [FlexChoice] -> FlexChoice #
Semigroup FlexChoice Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods (<>) :: FlexChoice -> FlexChoice -> FlexChoice # sconcat :: NonEmpty FlexChoice -> FlexChoice # stimes :: Integral b => b -> FlexChoice -> FlexChoice #
Eq FlexChoice Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods (==) :: FlexChoice -> FlexChoice -> Bool # (/=) :: FlexChoice -> FlexChoice -> Bool #
Show FlexChoice Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods showsPrec :: Int -> FlexChoice -> ShowS # show :: FlexChoice -> String # showList :: [FlexChoice] -> ShowS #

class ChooseFlex a where Source #

Methods

chooseFlex :: a -> a -> FlexChoice Source #

Instances

Instances details

ChooseFlex ArgInfo Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods chooseFlex :: ArgInfo -> ArgInfo -> FlexChoice Source #
ChooseFlex Hiding Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods chooseFlex :: Hiding -> Hiding -> FlexChoice Source #
ChooseFlex Origin Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods chooseFlex :: Origin -> Origin -> FlexChoice Source #
ChooseFlex IsForced Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods chooseFlex :: IsForced -> IsForced -> FlexChoice Source #
ChooseFlex FlexibleVarKind Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods chooseFlex :: FlexibleVarKind -> FlexibleVarKind -> FlexChoice Source #
ChooseFlex Int Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods chooseFlex :: Int -> Int -> FlexChoice Source #
ChooseFlex a => ChooseFlex (FlexibleVar a) Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods chooseFlex :: FlexibleVar a -> FlexibleVar a -> FlexChoice Source #
ChooseFlex a => ChooseFlex (Maybe a) Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods chooseFlex :: Maybe a -> Maybe a -> FlexChoice Source #
ChooseFlex a => ChooseFlex [a] Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods chooseFlex :: [a] -> [a] -> FlexChoice Source #

data ProblemEq Source #

A user pattern together with an internal term that it should be equal to after splitting is complete. Special cases: * User pattern is a variable but internal term isn't: this will be turned into an as pattern. * User pattern is a dot pattern: this pattern won't trigger any splitting but will be checked for equality after all splitting is complete and as patterns have been bound. * User pattern is an absurd pattern: emptiness of the type will be checked after splitting is complete. * User pattern is an annotated wildcard: type annotation will be checked after splitting is complete.

Constructors

ProblemEq
Fields problemInPat :: Pattern problemInst :: Term problemType :: Dom Type

Instances

Instances details

KillRange ProblemEq Source #

Instance details

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT ProblemEq Source #

PrettyTCM ProblemEq Source #

Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

prettyTCM :: MonadPretty m => ProblemEq -> m Doc Source #

Subst ProblemEq Source #

Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg ProblemEq
Instance details Defined in Agda.TypeChecking.Substitute type SubstArg ProblemEq = Term

Methods

applySubst :: Substitution' (SubstArg ProblemEq) -> ProblemEq -> ProblemEq Source #

NFData ProblemEq Source #

Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: ProblemEq -> () #

Eq ProblemEq Source #

Instance details

Defined in Agda.Syntax.Abstract

Methods

(==) :: ProblemEq -> ProblemEq -> Bool #

(/=) :: ProblemEq -> ProblemEq -> Bool #

Generic ProblemEq Source #

Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep ProblemEq

Instance details

Defined in Agda.Syntax.Abstract

type Rep ProblemEq = D1 ('MetaData "ProblemEq" "Agda.Syntax.Abstract" "Agda-2.9.0-inplace" 'False) (C1 ('MetaCons "ProblemEq" 'PrefixI 'True) (S1 ('MetaSel ('Just "problemInPat") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Pattern) :*: (S1 ('MetaSel ('Just "problemInst") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Term) :*: S1 ('MetaSel ('Just "problemType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 (Dom Type)))))

Methods

from :: ProblemEq -> Rep ProblemEq x #

to :: Rep ProblemEq x -> ProblemEq #

Show ProblemEq Source #

Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> ProblemEq -> ShowS #

show :: ProblemEq -> String #

showList :: [ProblemEq] -> ShowS #

type SubstArg ProblemEq Source #

Instance details

Defined in Agda.TypeChecking.Substitute

type SubstArg ProblemEq = Term

type Rep ProblemEq Source #

Instance details

Defined in Agda.Syntax.Abstract

type Rep ProblemEq = D1 ('MetaData "ProblemEq" "Agda.Syntax.Abstract" "Agda-2.9.0-inplace" 'False) (C1 ('MetaCons "ProblemEq" 'PrefixI 'True) (S1 ('MetaSel ('Just "problemInPat") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Pattern) :*: (S1 ('MetaSel ('Just "problemInst") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 Term) :*: S1 ('MetaSel ('Just "problemType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedStrict) (Rec0 (Dom Type)))))

data Problem a Source #

The user patterns we still have to split on.

Constructors

Problem

Fields

_problemEqs :: [ProblemEq]
User patterns which are typed (including the ones generated from implicit arguments).
_problemRestPats :: [NamedArg Pattern]
List of user patterns which could not yet be typed. Example: f : (b : Bool) -> if b then Nat else Nat -> Nat f true = zero f false zero = zero f false (suc n) = n In this sitation, for clause 2, we construct an initial problem problemEqs = [false = b] problemRestPats = [zero] As we instantiate b to false, the targetType reduces to Nat -> Nat and we can move pattern zero over to problemEqs.
_problemCont :: LHSState a -> TCM a
The code that checks the RHS.

Instances

Instances details

Subst (Problem a) Source #

Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Associated Types

type SubstArg (Problem a)
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem type SubstArg (Problem a) = Term

Methods

applySubst :: Substitution' (SubstArg (Problem a)) -> Problem a -> Problem a Source #

Show (Problem a) Source #

Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

showsPrec :: Int -> Problem a -> ShowS #

show :: Problem a -> String #

showList :: [Problem a] -> ShowS #

type SubstArg (Problem a) Source #

Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

type SubstArg (Problem a) = Term

problemEqs :: forall a f. Functor f => ([ProblemEq] -> f [ProblemEq]) -> Problem a -> f (Problem a) Source #

problemRestPats :: forall a f. Functor f => ([NamedArg Pattern] -> f [NamedArg Pattern]) -> Problem a -> f (Problem a) Source #

problemCont :: forall a f. Functor f => ((LHSState a -> TCM a) -> f (LHSState a -> TCM a)) -> Problem a -> f (Problem a) Source #

problemInPats :: Problem a -> [Pattern] Source #

data AsBinding Source #

Constructors

AsB Name Term (Dom Type)

Instances

Instances details

Pretty AsBinding Source #

Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

pretty :: AsBinding -> Doc Source #

prettyPrec :: Int -> AsBinding -> Doc Source #

prettyList :: [AsBinding] -> Doc Source #

PrettyTCM AsBinding Source #

Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

prettyTCM :: MonadPretty m => AsBinding -> m Doc Source #

InstantiateFull AsBinding Source #

Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

instantiateFull' :: AsBinding -> ReduceM AsBinding Source #

Subst AsBinding Source #

Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Associated Types

type SubstArg AsBinding
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem type SubstArg AsBinding = Term

Methods

applySubst :: Substitution' (SubstArg AsBinding) -> AsBinding -> AsBinding Source #

type SubstArg AsBinding Source #

Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

type SubstArg AsBinding = Term

data DotPattern Source #

Constructors

Dot Expr Term (Dom Type)

Instances

Instances details

PrettyTCM DotPattern Source #

Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

prettyTCM :: MonadPretty m => DotPattern -> m Doc Source #

Subst DotPattern Source #

Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Associated Types

type SubstArg DotPattern
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem type SubstArg DotPattern = Term

Methods

applySubst :: Substitution' (SubstArg DotPattern) -> DotPattern -> DotPattern Source #

type SubstArg DotPattern Source #

Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

type SubstArg DotPattern = Term

data AbsurdPattern Source #

Constructors

Absurd Range Type

Instances

Instances details

PrettyTCM AbsurdPattern Source #

Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

prettyTCM :: MonadPretty m => AbsurdPattern -> m Doc Source #

Subst AbsurdPattern Source #

Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Associated Types

type SubstArg AbsurdPattern
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem type SubstArg AbsurdPattern = Term

Methods

applySubst :: Substitution' (SubstArg AbsurdPattern) -> AbsurdPattern -> AbsurdPattern Source #

type SubstArg AbsurdPattern Source #

Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

type SubstArg AbsurdPattern = Term

data AnnotationPattern Source #

Constructors

Ann Expr Type

Instances

Instances details

PrettyTCM AnnotationPattern Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods prettyTCM :: MonadPretty m => AnnotationPattern -> m Doc Source #

data LHSState a Source #

State worked on during the main loop of checking a lhs. [Ulf Norell's PhD, page. 35]

Constructors

LHSState

Fields

_lhsTel :: Telescope
The types of the pattern variables.
_lhsOutPat :: [NamedArg DeBruijnPattern]
Patterns after splitting. The de Bruijn indices refer to positions in the list of abstract syntax patterns in the problem, counted from the back (right-to-left).
_lhsProblem :: Problem a
User patterns of supposed type delta.
_lhsTarget :: Arg Type
Type eliminated by problemRestPats in the problem. Can be Irrelevant to indicate that we came by an irrelevant projection and, hence, the rhs must be type-checked in irrelevant mode.
_lhsPartialSplit :: ![Maybe Int]
have we splitted with a PartialFocus?
_lhsIndexedSplit :: !Bool
Have we split on any indexed inductive types?
_lhsMatchPrio :: !MatchPrio
The match priority attached to the next split. The priority approximates causality, i.e. some splits (higher prio value) become available only after certain splits (lower prio value) have already been made. This information is used in the matcher for the non-compiled clauses to determine whether a DontKnow dominates a No (mismatch). The lower prio value is dominant in case of conflict. See issues #2964 and #3054, #8559.

Instances

Instances details

PrettyTCM (LHSState a) Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods prettyTCM :: MonadPretty m => LHSState a -> m Doc Source #

lhsTel :: forall a f. Functor f => (Telescope -> f Telescope) -> LHSState a -> f (LHSState a) Source #

lhsOutPat :: forall a f. Functor f => ([NamedArg DeBruijnPattern] -> f [NamedArg DeBruijnPattern]) -> LHSState a -> f (LHSState a) Source #

lhsProblem :: forall a f. Functor f => (Problem a -> f (Problem a)) -> LHSState a -> f (LHSState a) Source #

lhsTarget :: forall a f. Functor f => (Arg Type -> f (Arg Type)) -> LHSState a -> f (LHSState a) Source #

data LeftoverPatterns Source #

Constructors

LeftoverPatterns
Fields patternVariables :: IntMap [(Arg Name, PatVarPosition)] asPatterns :: [AsBinding] dotPatterns :: [DotPattern] absurdPatterns :: [AbsurdPattern] typeAnnotations :: [AnnotationPattern] otherPatterns :: [Pattern]

Instances

Instances details

PrettyTCM LeftoverPatterns Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods prettyTCM :: MonadPretty m => LeftoverPatterns -> m Doc Source #
Null LeftoverPatterns Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods empty :: LeftoverPatterns Source # null :: LeftoverPatterns -> Bool Source #
Monoid LeftoverPatterns Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods mempty :: LeftoverPatterns # mappend :: LeftoverPatterns -> LeftoverPatterns -> LeftoverPatterns # mconcat :: [LeftoverPatterns] -> LeftoverPatterns #
Semigroup LeftoverPatterns Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods (<>) :: LeftoverPatterns -> LeftoverPatterns -> LeftoverPatterns # sconcat :: NonEmpty LeftoverPatterns -> LeftoverPatterns # stimes :: Integral b => b -> LeftoverPatterns -> LeftoverPatterns #

getLeftoverPatterns :: (PureTCM m, MonadFresh NameId m) => [ProblemEq] -> m LeftoverPatterns Source #

Classify remaining patterns after splitting is complete into pattern variables, as patterns, dot patterns, and absurd patterns. Precondition: there are no more constructor patterns.

getUserVariableNames Source #

Arguments

:: Telescope	The telescope of pattern variables
-> IntMap [(Arg Name, PatVarPosition)]	The list of user names for each pattern variable
-> ([Maybe Name], [AsBinding])

Build a renaming for the internal patterns using variable names from the user patterns. If there are multiple user names for the same internal variable, the unused ones are returned as as-bindings. Names that are not also module parameters are preferred over those that are.

Orphan instances

PrettyTCM ProblemEq Source #
Instance details Methods prettyTCM :: MonadPretty m => ProblemEq -> m Doc Source #
PrettyTCM MatchPrio Source #
Instance details Methods prettyTCM :: MonadPretty m => MatchPrio -> m Doc Source #