Safe Haskell	None

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	From a record pattern (`ConP`).
ImplicitFlex	From a hidden formal argument (`ImplicitP`).
DotFlex	From a dot pattern (`DotP`).

Instances

Eq FlexibleVarKind
Ord FlexibleVarKind
Show FlexibleVarKind

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
Foldable FlexibleVar
Traversable FlexibleVar
Eq a => Eq (FlexibleVar a)
Ord (FlexibleVar Nat)
Show a => Show (FlexibleVar a)
LensHiding (FlexibleVar a)

defaultFlexibleVar :: a -> FlexibleVar aSource

flexibleVarFromHiding :: Hiding -> a -> FlexibleVar aSource

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 patterns. problemRest :: ProblemRest Patterns that cannot be typed yet.

Instances

Show p => Show (Problem' p)
Monoid p => Monoid (Problem' p)
Subst (Problem' p)

type Problem = Problem' (Permutation, [NamedArg Pattern])Source

The permutation should permute allHoles of the patterns to correspond to the abstract patterns in the problem.

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
Monoid ProblemRest	`ProblemRest` is a right dominant monoid. pr1 `mappend` pr2 = pr2 unless `pr2 = mempty`, then it is `pr1`. Basically, this means that the left `ProblemRest` is discarded, so use it wisely!
Subst ProblemRest

data Focus Source

Constructors

Focus
Fields focusCon :: QName focusImplicit :: Bool Do we come from an implicit record pattern? focusConArgs :: [NamedArg Pattern] focusRange :: Range focusOutPat :: OneHolePatterns focusHoleIx :: Int Index of focused variable in the out patterns. focusDatatype :: QName focusParams :: [Arg Term] focusIndices :: [Arg Term] focusType :: Type Type of variable we are splitting, kept for record patterns.
LitFocus Literal OneHolePatterns Int Type

data SplitProblem Source

Constructors

Split ProblemPart [Name] (Arg Focus) (Abs ProblemPart)	Split on constructor pattern. The `[Name]`s give the as-bindings for the focus.
SplitRest	Split on projection pattern. The projection could be belonging to an irrelevant record field.
Fields splitProjection :: Arg QName splitRestType :: Type

data SplitError Source

Constructors

NothingToSplit
SplitPanic String	__IMPOSSIBLE__, only there to make this instance of `Error`.

Instances

Error SplitError

data DotPatternInst Source

Constructors

DPI Expr Term (Dom Type)

Instances

Subst DotPatternInst
PrettyTCM DotPatternInst

data AsBinding Source

Constructors

AsB Name Term Type

Instances

Subst AsBinding
PrettyTCM AsBinding

data LHSState Source

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

Constructors

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