Agda- A dependently typed functional programming language and proof assistant

Safe HaskellNone




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.


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]

non-empty list of user patterns which could not yet be typed

restType :: Type

type eliminated by restPats


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




focusCon :: QName
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


Split ProblemPart [Name] (Arg Focus) (Abs ProblemPart)

the [Name]s give the as-bindings for the focus

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

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

data LHSState Source

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