Agda-2.4.2.4: A dependently typed functional programming language and proof assistant

Agda.TypeChecking.Rules.LHS.Problem

Synopsis

Documentation

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

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

Instances

 Source Source Source Eq a => Eq (FlexibleVar a) Source Source Show a => Show (FlexibleVar a) Source 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 FieldsproblemInPat :: [NamedArg Pattern]User patterns.problemOutPat :: pPatterns after splitting.problemTel :: TelescopeType of patterns.problemRest :: ProblemRestPatterns that cannot be typed yet.

Instances

 Show p => Show (Problem' p) Source Null a => Null (Problem' a) Source Source

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

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 FieldsrestPats :: [NamedArg Pattern]List of user patterns which could not yet be typed.restType :: Arg TypeType 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

 Source Source Source

data Focus Source

Constructors

 Focus FieldsfocusCon :: QName focusPatOrigin :: ConPOriginDo we come from an implicit or record pattern?focusConArgs :: [NamedArg Pattern] focusRange :: Range focusOutPat :: OneHolePatterns focusHoleIx :: IntIndex of focused variable in the out patterns.focusDatatype :: QName focusParams :: [Arg Term] focusIndices :: [Arg Term] focusType :: TypeType of variable we are splitting, kept for record patterns. LitFocus Literal OneHolePatterns Int Type

Result of `splitProblem`: Determines position for the next split.

Constructors

 Split Split on constructor pattern. FieldssplitLPats :: ProblemPartThe typed user patterns left of the split position. Invariant: `problemRest == empty`.splitAsNames :: [Name]The as-bindings for the focus.splitFocus :: Arg FocusHow to split the variable at the split position.splitRPats :: Abs ProblemPartThe typed user patterns right of the split position. SplitRest Split on projection pattern. FieldssplitProjection :: Arg QNameThe projection could be belonging to an irrelevant record field.splitRestType :: Type

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

Constructors

 DPI Expr Term (Dom Type)

Instances

 Source Source

data AsBinding Source

Constructors

 AsB Name Term Type

Instances

 Source Source

data LHSState Source

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

Constructors

 LHSState FieldslhsProblem :: Problem lhsSubst :: Substitution lhsDPI :: [DotPatternInst] lhsAsB :: [AsBinding]