| Safe Haskell | None |
|---|
Agda.TypeChecking.Rules.LHS.Problem
- type Substitution = [Maybe Term]
- type FlexibleVars = [Nat]
- data Problem' p = Problem {}
- data ProblemRest = ProblemRest {}
- data Focus
- = Focus {
- focusCon :: QName
- focusConArgs :: [NamedArg Pattern]
- focusRange :: Range
- focusOutPat :: OneHolePatterns
- focusHoleIx :: Int
- focusDatatype :: QName
- focusParams :: [Arg Term]
- focusIndices :: [Arg Term]
- focusType :: Type
- | LitFocus Literal OneHolePatterns Int Type
- = Focus {
- data SplitProblem = Split ProblemPart [Name] (Arg Focus) (Abs ProblemPart)
- data SplitError
- type Problem = Problem' (Permutation, [Arg Pattern])
- type ProblemPart = Problem' ()
- data DotPatternInst = DPI Expr Term (Dom Type)
- data AsBinding = AsB Name Term Type
- data LHSState = LHSState {
- lhsProblem :: Problem
- lhsSubst :: Substitution
- lhsDPI :: [DotPatternInst]
- lhsAsB :: [AsBinding]
Documentation
type Substitution = [Maybe Term]Source
type FlexibleVars = [Nat]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
| |
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 | |
Instances
| Monoid ProblemRest |
|
| Subst ProblemRest |
Constructors
| Focus | |
Fields
| |
| LitFocus Literal OneHolePatterns Int Type | |
data SplitProblem Source
Constructors
| 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.
type ProblemPart = Problem' ()Source
data DotPatternInst Source
Instances
State worked on during the main loop of checking a lhs.
Constructors
| LHSState | |
Fields
| |