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' [ProblemEq] (Problem a)
problemRestPats :: Lens' [NamedArg Pattern] (Problem a)
problemCont :: Lens' (LHSState a -> TCM a) (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]
}
lhsTel :: Lens' Telescope (LHSState a)
lhsOutPat :: Lens' [NamedArg DeBruijnPattern] (LHSState a)
lhsProblem :: Lens' (Problem a) (LHSState a)
lhsTarget :: Lens' (Arg Type) (LHSState a)
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 #
Data ProblemEq Source #
Instance details Defined in Agda.Syntax.Abstract Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ProblemEq -> c ProblemEq # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ProblemEq # toConstr :: ProblemEq -> Constr # dataTypeOf :: ProblemEq -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ProblemEq) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProblemEq) # gmapT :: (forall b. Data b => b -> b) -> ProblemEq -> ProblemEq # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ProblemEq -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ProblemEq -> r # gmapQ :: (forall d. Data d => d -> u) -> ProblemEq -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> ProblemEq -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> ProblemEq -> m ProblemEq # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ProblemEq -> m ProblemEq # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ProblemEq -> m ProblemEq #
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.2.1.20220320-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' [ProblemEq] (Problem a) Source #

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

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

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

data AsBinding Source #

Constructors

AsB Name Term Type Modality

Instances

Instances details

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

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

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

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

lhsTarget :: Lens' (Arg Type) (LHSState a) 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 #