Safe Haskell | None |
---|
- 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.
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
.
Monoid ProblemRest |
|
Subst ProblemRest |
Focus | |
| |
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.
type ProblemPart = Problem' ()Source
State worked on during the main loop of checking a lhs.
LHSState | |
|