Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone




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


RecordFlex [FlexibleVarKind]

From a record pattern (ConP). Saves the FlexibleVarKind of its subpatterns.


From a hidden formal argument or underscore (WildP).


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.



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.




problemInPat :: [NamedArg Pattern]

User patterns.

problemOutPat :: p

Patterns after splitting.

problemTel :: Telescope

Type of patterns.

problemRest :: ProblemRest

Patterns that cannot be typed yet.


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

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

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.




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.

data Focus Source




focusCon :: QName
focusPatOrigin :: ConPOrigin

Do we come from an implicit or 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

Result of splitProblem: Determines position for the next split.



Split on constructor pattern.


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.


Split on projection pattern.


splitProjection :: Arg QName

The projection could be belonging to an irrelevant record field.

splitRestType :: Type

consSplitProblem Source


:: 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 LHSState Source

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