Agda.TypeChecking.Rules.LHS.Problem

Documentation

type FlexibleVars = [FlexibleVar Nat]

data FlexibleVarKind

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

ChooseFlex FlexibleVarKind

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

chooseFlex :: FlexibleVarKind -> FlexibleVarKind -> FlexChoice

Show FlexibleVarKind

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

showsPrec :: Int -> FlexibleVarKind -> ShowS

show :: FlexibleVarKind -> String

showList :: [FlexibleVarKind] -> ShowS

Eq FlexibleVarKind

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

(==) :: FlexibleVarKind -> FlexibleVarKind -> Bool

(/=) :: FlexibleVarKind -> FlexibleVarKind -> Bool

data FlexibleVar a

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

Foldable FlexibleVar

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

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

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

fmap :: (a -> b) -> FlexibleVar a -> FlexibleVar b

(<$) :: a -> FlexibleVar b -> FlexibleVar a

LensArgInfo (FlexibleVar a)

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

getArgInfo :: FlexibleVar a -> ArgInfo

setArgInfo :: ArgInfo -> FlexibleVar a -> FlexibleVar a

mapArgInfo :: (ArgInfo -> ArgInfo) -> FlexibleVar a -> FlexibleVar a

LensHiding (FlexibleVar a)

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

getHiding :: FlexibleVar a -> Hiding

setHiding :: Hiding -> FlexibleVar a -> FlexibleVar a

mapHiding :: (Hiding -> Hiding) -> FlexibleVar a -> FlexibleVar a

LensModality (FlexibleVar a)

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

getModality :: FlexibleVar a -> Modality

setModality :: Modality -> FlexibleVar a -> FlexibleVar a

mapModality :: (Modality -> Modality) -> FlexibleVar a -> FlexibleVar a

LensOrigin (FlexibleVar a)

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

getOrigin :: FlexibleVar a -> Origin

setOrigin :: Origin -> FlexibleVar a -> FlexibleVar a

mapOrigin :: (Origin -> Origin) -> FlexibleVar a -> FlexibleVar a

ChooseFlex a => ChooseFlex (FlexibleVar a)

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

chooseFlex :: FlexibleVar a -> FlexibleVar a -> FlexChoice

Show a => Show (FlexibleVar a)

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)

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

(==) :: FlexibleVar a -> FlexibleVar a -> Bool

(/=) :: FlexibleVar a -> FlexibleVar a -> Bool

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

data FlexChoice

Constructors

ChooseLeft

ChooseRight

ChooseEither

ExpandBoth

Instances

Monoid FlexChoice

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

mempty :: FlexChoice

mappend :: FlexChoice -> FlexChoice -> FlexChoice

mconcat :: [FlexChoice] -> FlexChoice

Semigroup FlexChoice

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

(<>) :: FlexChoice -> FlexChoice -> FlexChoice

sconcat :: NonEmpty FlexChoice -> FlexChoice

stimes :: Integral b => b -> FlexChoice -> FlexChoice

Show FlexChoice

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

showsPrec :: Int -> FlexChoice -> ShowS

show :: FlexChoice -> String

showList :: [FlexChoice] -> ShowS

Eq FlexChoice

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

(==) :: FlexChoice -> FlexChoice -> Bool

(/=) :: FlexChoice -> FlexChoice -> Bool

class ChooseFlex a where

Methods

chooseFlex :: a -> a -> FlexChoice

Instances

ChooseFlex ArgInfo

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

chooseFlex :: ArgInfo -> ArgInfo -> FlexChoice

ChooseFlex Hiding

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

chooseFlex :: Hiding -> Hiding -> FlexChoice

ChooseFlex Origin

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

chooseFlex :: Origin -> Origin -> FlexChoice

ChooseFlex IsForced

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

chooseFlex :: IsForced -> IsForced -> FlexChoice

ChooseFlex FlexibleVarKind

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

chooseFlex :: FlexibleVarKind -> FlexibleVarKind -> FlexChoice

ChooseFlex Int

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

chooseFlex :: Int -> Int -> FlexChoice

ChooseFlex a => ChooseFlex (FlexibleVar a)

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

chooseFlex :: FlexibleVar a -> FlexibleVar a -> FlexChoice

ChooseFlex a => ChooseFlex (Maybe a)

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

chooseFlex :: Maybe a -> Maybe a -> FlexChoice

ChooseFlex a => ChooseFlex [a]

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

chooseFlex :: [a] -> [a] -> FlexChoice

data ProblemEq

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

KillRange ProblemEq

Defined in Agda.Syntax.Abstract

Methods

killRange :: KillRangeT ProblemEq

PrettyTCM ProblemEq

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

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

Subst ProblemEq

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg ProblemEq

Methods

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

Generic ProblemEq

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

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> ProblemEq -> ShowS

show :: ProblemEq -> String

showList :: [ProblemEq] -> ShowS

NFData ProblemEq

Defined in Agda.Syntax.Abstract

Methods

rnf :: ProblemEq -> ()

Eq ProblemEq

Defined in Agda.Syntax.Abstract

Methods

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

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

type SubstArg ProblemEq

Defined in Agda.TypeChecking.Substitute

type SubstArg ProblemEq = Term

type Rep ProblemEq

Defined in Agda.Syntax.Abstract

type Rep ProblemEq = D1 ('MetaData "ProblemEq" "Agda.Syntax.Abstract" "Agda-2.6.2.2.20221128-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

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

Subst (Problem a)

Defined in Agda.TypeChecking.Rules.LHS.Problem

Associated Types

type SubstArg (Problem a)

Methods

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

Show (Problem a)

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)

Defined in Agda.TypeChecking.Rules.LHS.Problem

type SubstArg (Problem a) = Term

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

Constructors

AsB Name Term Type Modality

Instances

PrettyTCM AsBinding

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

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

InstantiateFull AsBinding

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

instantiateFull' :: AsBinding -> ReduceM AsBinding

Subst AsBinding

Defined in Agda.TypeChecking.Rules.LHS.Problem

Associated Types

type SubstArg AsBinding

Methods

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

Pretty AsBinding

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

pretty :: AsBinding -> Doc

prettyPrec :: Int -> AsBinding -> Doc

prettyList :: [AsBinding] -> Doc

type SubstArg AsBinding

Defined in Agda.TypeChecking.Rules.LHS.Problem

type SubstArg AsBinding = Term

data DotPattern

Constructors

Dot Expr Term (Dom Type)

Instances

PrettyTCM DotPattern

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

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

Subst DotPattern

Defined in Agda.TypeChecking.Rules.LHS.Problem

Associated Types

type SubstArg DotPattern

Methods

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

type SubstArg DotPattern

Defined in Agda.TypeChecking.Rules.LHS.Problem

type SubstArg DotPattern = Term

data AbsurdPattern

Constructors

Absurd Range Type

Instances

PrettyTCM AbsurdPattern

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

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

Subst AbsurdPattern

Defined in Agda.TypeChecking.Rules.LHS.Problem

Associated Types

type SubstArg AbsurdPattern

Methods

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

type SubstArg AbsurdPattern

Defined in Agda.TypeChecking.Rules.LHS.Problem

type SubstArg AbsurdPattern = Term

data AnnotationPattern

Constructors

Ann Expr Type

Instances

PrettyTCM AnnotationPattern

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

prettyTCM :: MonadPretty m => AnnotationPattern -> m Doc

data LHSState a

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

PrettyTCM (LHSState a)

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

prettyTCM :: MonadPretty m => LHSState a -> m Doc

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

Constructors

LeftoverPatterns

Fields

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

Instances

PrettyTCM LeftoverPatterns

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

prettyTCM :: MonadPretty m => LeftoverPatterns -> m Doc

Null LeftoverPatterns

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

empty :: LeftoverPatterns

null :: LeftoverPatterns -> Bool

Monoid LeftoverPatterns

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

mempty :: LeftoverPatterns

mappend :: LeftoverPatterns -> LeftoverPatterns -> LeftoverPatterns

mconcat :: [LeftoverPatterns] -> LeftoverPatterns

Semigroup LeftoverPatterns

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

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

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

Methods

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