Safe Haskell	Safe-Inferred
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 :: Lens' (Problem a) [ProblemEq]
problemRestPats :: Lens' (Problem a) [NamedArg Pattern]
problemCont :: Lens' (Problem a) (LHSState a -> TCM 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 :: Lens' (LHSState a) Telescope
lhsOutPat :: Lens' (LHSState a) [NamedArg DeBruijnPattern]
lhsProblem :: Lens' (LHSState a) (Problem a)
lhsTarget :: Lens' (LHSState a) (Arg Type)
data LeftoverPatterns = LeftoverPatterns {
- patternVariables :: IntMap [(Name, PatVarPosition)]
- asPatterns :: [AsBinding]
- dotPatterns :: [DotPattern]
- absurdPatterns :: [AbsurdPattern]
- typeAnnotations :: [AnnotationPattern]
- otherPatterns :: [Pattern]
}
getLeftoverPatterns :: forall m. 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...

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 #
Show FlexibleVarKind Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods showsPrec :: Int -> FlexibleVarKind -> ShowS show :: FlexibleVarKind -> String showList :: [FlexibleVarKind] -> ShowS
Eq FlexibleVarKind Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods (==) :: 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.

Constructors

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

Instances

Instances details

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)
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 #
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 #
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
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

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
Show FlexChoice Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods showsPrec :: Int -> FlexChoice -> ShowS show :: FlexChoice -> String showList :: [FlexChoice] -> ShowS
Eq FlexChoice Source #
Instance details Defined in Agda.TypeChecking.Rules.LHS.Problem Methods (==) :: FlexChoice -> FlexChoice -> Bool (/=) :: FlexChoice -> FlexChoice -> Bool

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 Source # Methods applySubst :: Substitution' (SubstArg ProblemEq) -> ProblemEq -> ProblemEq Source #
Generic ProblemEq Source #
Instance details Defined in Agda.Syntax.Abstract Associated Types type Rep ProblemEq :: Type -> 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
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
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.6.4-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)))))

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) Source # 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 :: Lens' (Problem a) [ProblemEq] Source #

problemRestPats :: Lens' (Problem a) [NamedArg Pattern] Source #

problemCont :: Lens' (Problem a) (LHSState a -> TCM a) Source #

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

data AsBinding Source #

Constructors

AsB Name Term Type Modality

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 Source # 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 Source # 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 Source # 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?

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 :: Lens' (LHSState a) Telescope Source #

lhsOutPat :: Lens' (LHSState a) [NamedArg DeBruijnPattern] Source #

lhsProblem :: Lens' (LHSState a) (Problem a) Source #

lhsTarget :: Lens' (LHSState a) (Arg Type) Source #

data LeftoverPatterns Source #

Constructors

LeftoverPatterns
Fields patternVariables :: IntMap [(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 :: forall m. 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.

getUserVariableNames Source #

Arguments

:: 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.

Orphan instances

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