Agda.TypeChecking.Rules.LHS.Problem

Documentation

type Substitution = [Maybe Term]

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

Instances

Eq FlexibleVarKind

Methods

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

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

Show FlexibleVarKind

Methods

showsPrec :: Int -> FlexibleVarKind -> ShowS

show :: FlexibleVarKind -> String

showList :: [FlexibleVarKind] -> ShowS

ChooseFlex FlexibleVarKind

Methods

chooseFlex :: FlexibleVarKind -> FlexibleVarKind -> FlexChoice

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

• flexHiding :: Hiding
• flexKind :: FlexibleVarKind
• flexPos :: Maybe Int
• flexVar :: a

Instances

Functor FlexibleVar

Methods

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

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

Foldable FlexibleVar

Methods

fold :: Monoid m => FlexibleVar m -> 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

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)

Eq a => Eq (FlexibleVar a)

Methods

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

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

Show a => Show (FlexibleVar a)

Methods

showsPrec :: Int -> FlexibleVar a -> ShowS

show :: FlexibleVar a -> String

showList :: [FlexibleVar a] -> ShowS

LensHiding (FlexibleVar a)

Methods

getHiding :: FlexibleVar a -> Hiding

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

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

ChooseFlex a => ChooseFlex (FlexibleVar a)

Methods

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

defaultFlexibleVar :: a -> FlexibleVar a

flexibleVarFromHiding :: Hiding -> a -> FlexibleVar a

allFlexVars :: Telescope -> FlexibleVars

data FlexChoice

Constructors

ChooseLeft

ChooseRight

ChooseEither

ExpandBoth

Instances

Eq FlexChoice

Methods

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

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

Show FlexChoice

Methods

showsPrec :: Int -> FlexChoice -> ShowS

show :: FlexChoice -> String

showList :: [FlexChoice] -> ShowS

Semigroup FlexChoice

Methods

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

sconcat :: NonEmpty FlexChoice -> FlexChoice

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

Monoid FlexChoice

Methods

mempty :: FlexChoice

mappend :: FlexChoice -> FlexChoice -> FlexChoice

mconcat :: [FlexChoice] -> FlexChoice

class ChooseFlex a where

Minimal complete definition

chooseFlex

Methods

chooseFlex :: a -> a -> FlexChoice

Instances

ChooseFlex Int

Methods

chooseFlex :: Int -> Int -> FlexChoice

ChooseFlex Hiding

Methods

chooseFlex :: Hiding -> Hiding -> FlexChoice

ChooseFlex FlexibleVarKind

Methods

chooseFlex :: FlexibleVarKind -> FlexibleVarKind -> FlexChoice

ChooseFlex a => ChooseFlex [a]

Methods

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

ChooseFlex a => ChooseFlex (Maybe a)

Methods

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

ChooseFlex a => ChooseFlex (FlexibleVar a)

Methods

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

data Problem' p

State of typechecking a LHS; input to split. [Ulf Norell's PhD, page. 35]

In Problem ps p delta, ps are the user patterns of supposed type delta. p is the pattern resulting from the splitting.

Constructors

Problem

Fields

• problemInPat :: [NamedArg Pattern]

  User patterns.

• problemOutPat :: p

  Patterns after splitting.

• problemTel :: Telescope

  Type of in patterns.

• problemRest :: ProblemRest

  Patterns that cannot be typed yet.

Instances

Subst Term (Problem' p)

Methods

applySubst :: Substitution' Term -> Problem' p -> Problem' p

Show p => Show (Problem' p)

Methods

showsPrec :: Int -> Problem' p -> ShowS

show :: Problem' p -> String

showList :: [Problem' p] -> ShowS

Null a => Null (Problem' a)

Methods

empty :: Problem' a

null :: Problem' a -> Bool

type Problem = Problem' [NamedArg DeBruijnPattern]

The de Bruijn indices in the pattern refer to positions in the list of abstract patterns in the problem, counted from the back.

type ProblemPart = Problem' ()

data ProblemRest

User patterns that could not be given a type yet.

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 problemInPat = [false] problemTel = (b : Bool) problemRest.restPats = [zero] problemRest.restType = if b then Nat else Nat -> Nat As we instantiate b to false, the restType reduces to Nat -> Nat and we can move pattern zero over to problemInPat.

Constructors

ProblemRest

Fields

• restPats :: [NamedArg Pattern]

  List of user patterns which could not yet be typed.

• restType :: Arg Type

  Type eliminated by restPats. Can be Irrelevant to indicate that we came by an irrelevant projection and, hence, the rhs must be type-checked in irrelevant mode.

Instances

Show ProblemRest

Methods

showsPrec :: Int -> ProblemRest -> ShowS

show :: ProblemRest -> String

showList :: [ProblemRest] -> ShowS

Null ProblemRest

Methods

empty :: ProblemRest

null :: ProblemRest -> Bool

Subst Term ProblemRest

Methods

applySubst :: Substitution' Term -> ProblemRest -> ProblemRest

data Focus

Constructors

Focus

Fields

• focusCon :: QName
• focusPatOrigin :: ConOrigin

  Do we come from an implicit or record pattern?

• focusConArgs :: [NamedArg Pattern]
• focusRange :: Range
• focusOutPat :: [NamedArg DeBruijnPattern]
• focusDatatype :: QName
• focusParams :: [Arg Term]
• focusIndices :: [Arg Term]
• focusType :: Type

  Type of variable we are splitting, kept for record patterns.

LitFocus Literal [NamedArg DeBruijnPattern] Type

data SplitProblem

Result of splitProblem: Determines position for the next split.

Constructors

Split

Split on constructor pattern.

Fields

• splitLPats :: ProblemPart

  The typed user patterns left of the split position. Invariant: problemRest == empty.

• splitFocus :: Arg Focus

  How to split the variable at the split position.

• splitRPats :: Abs ProblemPart

  The typed user patterns right of the split position.

SplitRest

Split on projection pattern.

Fields

• splitProjection :: Arg QName

  The projection could be belonging to an irrelevant record field.

• splitProjOrigin :: ProjOrigin
• splitRestType :: Type

consSplitProblem

Arguments

:: NamedArg Pattern

p A pattern.

-> ArgName

x The name of the argument (from its type).

-> Dom Type

t Its type.

-> SplitProblem

The split problem, containing splitLPats ps;xs:ts.

-> SplitProblem

The result, now containing splitLPats (p,ps);(x,xs):(t,ts).

Put a typed pattern on the very left of a SplitProblem.

data DotPatternInst

Instantiations of a dot pattern with a term. `Maybe e` if the user wrote a dot pattern .e Nothing if this is an instantiation of an implicit argument or a name.

Constructors

DPI

Fields

• dotPatternName :: Maybe Name
• dotPatternUserExpr :: Maybe Expr
• dotPatternInst :: Term
• dotPatternType :: Dom Type

Instances

PrettyTCM DotPatternInst

Methods

prettyTCM :: DotPatternInst -> TCM Doc

Subst Term DotPatternInst

Methods

applySubst :: Substitution' Term -> DotPatternInst -> DotPatternInst

data AsBinding

Constructors

AsB Name Term Type

Instances

Pretty AsBinding

Methods

pretty :: AsBinding -> Doc

prettyPrec :: Int -> AsBinding -> Doc

PrettyTCM AsBinding

Methods

prettyTCM :: AsBinding -> TCM Doc

InstantiateFull AsBinding

Methods

instantiateFull' :: AsBinding -> ReduceM AsBinding

Subst Term AsBinding

Methods

applySubst :: Substitution' Term -> AsBinding -> AsBinding

data LHSState

State worked on during the main loop of checking a lhs.

Constructors

LHSState

Fields

• lhsProblem :: Problem
• lhsDPI :: [DotPatternInst]