Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- type FlexibleVars = [FlexibleVar Nat]
- data FlexibleVarKind
- data FlexibleVar a = FlexibleVar {
- flexArgInfo :: ArgInfo
- flexForced :: IsForced
- flexKind :: FlexibleVarKind
- flexPos :: Maybe Int
- flexVar :: a
- allFlexVars :: [IsForced] -> Telescope -> FlexibleVars
- data FlexChoice
- 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 Type Modality
- 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
- 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 [(Name, PatVarPosition)]
- asPatterns :: [AsBinding]
- dotPatterns :: [DotPattern]
- absurdPatterns :: [AbsurdPattern]
- typeAnnotations :: [AnnotationPattern]
- otherPatterns :: [Pattern]
- getLeftoverPatterns :: PureTCM m => [ProblemEq] -> m LeftoverPatterns
- getUserVariableNames :: Telescope -> IntMap [(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...
RecordFlex [FlexibleVarKind] | From a record pattern ( |
ImplicitFlex | From a hidden formal argument or underscore ( |
DotFlex | From a dot pattern ( |
OtherFlex |
Instances
ChooseFlex FlexibleVarKind Source # | |
Defined in Agda.TypeChecking.Rules.LHS.Problem | |
Show FlexibleVarKind Source # | |
Defined in Agda.TypeChecking.Rules.LHS.Problem showsPrec :: Int -> FlexibleVarKind -> ShowS show :: FlexibleVarKind -> String showList :: [FlexibleVarKind] -> ShowS | |
Eq FlexibleVarKind Source # | |
Defined in Agda.TypeChecking.Rules.LHS.Problem (==) :: FlexibleVarKind -> FlexibleVarKind -> Bool (/=) :: FlexibleVarKind -> FlexibleVarKind -> Bool |
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.
FlexibleVar | |
|
Instances
allFlexVars :: [IsForced] -> Telescope -> FlexibleVars Source #
data FlexChoice Source #
Instances
Monoid FlexChoice Source # | |
Defined in Agda.TypeChecking.Rules.LHS.Problem mempty :: FlexChoice mappend :: FlexChoice -> FlexChoice -> FlexChoice mconcat :: [FlexChoice] -> FlexChoice | |
Semigroup FlexChoice Source # | |
Defined in Agda.TypeChecking.Rules.LHS.Problem (<>) :: FlexChoice -> FlexChoice -> FlexChoice # sconcat :: NonEmpty FlexChoice -> FlexChoice stimes :: Integral b => b -> FlexChoice -> FlexChoice | |
Show FlexChoice Source # | |
Defined in Agda.TypeChecking.Rules.LHS.Problem showsPrec :: Int -> FlexChoice -> ShowS show :: FlexChoice -> String showList :: [FlexChoice] -> ShowS | |
Eq FlexChoice Source # | |
Defined in Agda.TypeChecking.Rules.LHS.Problem (==) :: FlexChoice -> FlexChoice -> Bool (/=) :: FlexChoice -> FlexChoice -> Bool |
class ChooseFlex a where Source #
chooseFlex :: a -> a -> FlexChoice Source #
Instances
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.
ProblemEq | |
|
Instances
KillRange ProblemEq Source # | |||||
Defined in Agda.Syntax.Abstract | |||||
PrettyTCM ProblemEq Source # | |||||
Defined in Agda.TypeChecking.Rules.LHS.Problem | |||||
Subst ProblemEq Source # | |||||
Defined in Agda.TypeChecking.Substitute applySubst :: Substitution' (SubstArg ProblemEq) -> ProblemEq -> ProblemEq Source # | |||||
NFData ProblemEq Source # | |||||
Defined in Agda.Syntax.Abstract | |||||
Generic ProblemEq Source # | |||||
Defined in Agda.Syntax.Abstract
| |||||
Show ProblemEq Source # | |||||
Eq ProblemEq Source # | |||||
type SubstArg ProblemEq Source # | |||||
Defined in Agda.TypeChecking.Substitute | |||||
type Rep ProblemEq Source # | |||||
Defined in Agda.Syntax.Abstract type Rep ProblemEq = D1 ('MetaData "ProblemEq" "Agda.Syntax.Abstract" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "ProblemEq" 'PrefixI 'True) (S1 ('MetaSel ('Just "problemInPat") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Pattern) :*: (S1 ('MetaSel ('Just "problemInst") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :*: S1 ('MetaSel ('Just "problemType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Dom Type))))) |
The user patterns we still have to split on.
Problem | |
|
Instances
Subst (Problem a) Source # | |||||
Defined in Agda.TypeChecking.Rules.LHS.Problem
applySubst :: Substitution' (SubstArg (Problem a)) -> Problem a -> Problem a Source # | |||||
Show (Problem a) Source # | |||||
type SubstArg (Problem a) Source # | |||||
Defined in Agda.TypeChecking.Rules.LHS.Problem |
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 #
Instances
Pretty AsBinding Source # | |||||
PrettyTCM AsBinding Source # | |||||
Defined in Agda.TypeChecking.Rules.LHS.Problem | |||||
InstantiateFull AsBinding Source # | |||||
Defined in Agda.TypeChecking.Rules.LHS.Problem | |||||
Subst AsBinding Source # | |||||
Defined in Agda.TypeChecking.Rules.LHS.Problem
applySubst :: Substitution' (SubstArg AsBinding) -> AsBinding -> AsBinding Source # | |||||
type SubstArg AsBinding Source # | |||||
Defined in Agda.TypeChecking.Rules.LHS.Problem |
data DotPattern Source #
Instances
PrettyTCM DotPattern Source # | |||||
Defined in Agda.TypeChecking.Rules.LHS.Problem prettyTCM :: MonadPretty m => DotPattern -> m Doc Source # | |||||
Subst DotPattern Source # | |||||
Defined in Agda.TypeChecking.Rules.LHS.Problem
applySubst :: Substitution' (SubstArg DotPattern) -> DotPattern -> DotPattern Source # | |||||
type SubstArg DotPattern Source # | |||||
Defined in Agda.TypeChecking.Rules.LHS.Problem |
data AbsurdPattern Source #
Instances
PrettyTCM AbsurdPattern Source # | |||||
Defined in Agda.TypeChecking.Rules.LHS.Problem prettyTCM :: MonadPretty m => AbsurdPattern -> m Doc Source # | |||||
Subst AbsurdPattern Source # | |||||
Defined in Agda.TypeChecking.Rules.LHS.Problem
| |||||
type SubstArg AbsurdPattern Source # | |||||
Defined in Agda.TypeChecking.Rules.LHS.Problem |
data AnnotationPattern Source #
Instances
PrettyTCM AnnotationPattern Source # | |
Defined in Agda.TypeChecking.Rules.LHS.Problem prettyTCM :: MonadPretty m => AnnotationPattern -> m Doc Source # |
State worked on during the main loop of checking a lhs. [Ulf Norell's PhD, page. 35]
LHSState | |
|
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 #
LeftoverPatterns | |
|
Instances
PrettyTCM LeftoverPatterns Source # | |
Defined in Agda.TypeChecking.Rules.LHS.Problem prettyTCM :: MonadPretty m => LeftoverPatterns -> m Doc Source # | |
Null LeftoverPatterns Source # | |
Defined in Agda.TypeChecking.Rules.LHS.Problem empty :: LeftoverPatterns Source # null :: LeftoverPatterns -> Bool Source # | |
Monoid LeftoverPatterns Source # | |
Defined in Agda.TypeChecking.Rules.LHS.Problem | |
Semigroup LeftoverPatterns Source # | |
Defined in Agda.TypeChecking.Rules.LHS.Problem (<>) :: LeftoverPatterns -> LeftoverPatterns -> LeftoverPatterns # sconcat :: NonEmpty LeftoverPatterns -> LeftoverPatterns stimes :: Integral b => b -> LeftoverPatterns -> LeftoverPatterns |
getLeftoverPatterns :: PureTCM 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.
:: Telescope | The telescope of pattern variables |
-> IntMap [(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.