Safe Haskell	None
Language	Haskell98

Agda.TypeChecking.Rules.LHS.Problem

Synopsis

Documentation

type Substitution = [Maybe Term] Source

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

Instances

Eq FlexibleVarKind Source
Show FlexibleVarKind Source
ChooseFlex FlexibleVarKind Source

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 flexHiding :: Hiding flexKind :: FlexibleVarKind flexVar :: a

Instances

Functor FlexibleVar Source
Foldable FlexibleVar Source
Traversable FlexibleVar Source
Eq a => Eq (FlexibleVar a) Source
Show a => Show (FlexibleVar a) Source
LensHiding (FlexibleVar a) Source
ChooseFlex a => ChooseFlex (FlexibleVar a) Source

defaultFlexibleVar :: a -> FlexibleVar a Source

flexibleVarFromHiding :: Hiding -> a -> FlexibleVar a Source

data FlexChoice Source

Constructors

ChooseLeft
ChooseRight
ChooseEither
ExpandBoth

Instances

Eq FlexChoice Source
Show FlexChoice Source
Monoid FlexChoice Source

class ChooseFlex a where Source

Methods

chooseFlex :: a -> a -> FlexChoice Source

Instances

ChooseFlex Int Source
ChooseFlex Hiding Source
ChooseFlex FlexibleVarKind Source
ChooseFlex a => ChooseFlex [a] Source
ChooseFlex a => ChooseFlex (FlexibleVar a) Source

data Problem' p Source

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) Source
Show p => Show (Problem' p) Source
Null a => Null (Problem' a) Source

type Problem = Problem' [NamedArg DeBruijnPattern] Source

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' () Source

data ProblemRest Source

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 Source
Null ProblemRest Source
Subst Term ProblemRest Source

data Focus Source

Constructors

Focus
Fields focusCon :: QName focusPatOrigin :: ConPOrigin 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 Source

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`. splitAsNames :: [Name] The as-bindings for the focus. 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. splitRestType :: Type

consSplitProblem Source

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 Source

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 an underscore _

Constructors

DPI
Fields dotPatternUserExpr :: Maybe Expr dotPatternInst :: Term dotPatternType :: Dom Type

Instances

PrettyTCM DotPatternInst Source
Subst Term DotPatternInst Source

data AsBinding Source

Constructors

AsB Name Term Type

Instances

PrettyTCM AsBinding Source
Subst Term AsBinding Source

data LHSState Source

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

Constructors

LHSState
Fields lhsProblem :: Problem lhsSubst :: PatternSubstitution lhsDPI :: [DotPatternInst] lhsAsB :: [AsBinding]