Safe Haskell | None |
---|---|
Language | Haskell98 |
- type Substitution = [Maybe Term]
- type FlexibleVars = [FlexibleVar Nat]
- data FlexibleVarKind
- data FlexibleVar a = FlexibleVar {
- flexHiding :: Hiding
- flexKind :: FlexibleVarKind
- flexVar :: a
- defaultFlexibleVar :: a -> FlexibleVar a
- flexibleVarFromHiding :: Hiding -> a -> FlexibleVar a
- data Problem' p = Problem {}
- type Problem = Problem' (Permutation, [NamedArg Pattern])
- type ProblemPart = Problem' ()
- data ProblemRest = ProblemRest {}
- data Focus
- = Focus {
- focusCon :: QName
- focusImplicit :: Bool
- 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 {
- splitLPats :: ProblemPart
- splitAsNames :: [Name]
- splitFocus :: Arg Focus
- splitRPats :: Abs ProblemPart
- | SplitRest { }
- = Split {
- consSplitProblem :: NamedArg Pattern -> ArgName -> Dom Type -> SplitProblem -> SplitProblem
- 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 = [FlexibleVar Nat] Source
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 | From a record pattern ( |
ImplicitFlex | From a hidden formal argument ( |
DotFlex | From a dot pattern ( |
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.
FlexibleVar | |
|
Functor FlexibleVar Source | |
Foldable FlexibleVar Source | |
Traversable FlexibleVar Source | |
Eq a => Eq (FlexibleVar a) Source | |
Ord (FlexibleVar Nat) Source | |
Show a => Show (FlexibleVar a) Source | |
LensHiding (FlexibleVar a) Source |
defaultFlexibleVar :: a -> FlexibleVar a Source
flexibleVarFromHiding :: Hiding -> a -> FlexibleVar a 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 | |
|
type Problem = Problem' (Permutation, [NamedArg Pattern]) Source
The permutation should permute allHoles
of the patterns to correspond to
the abstract patterns in the problem.
type ProblemPart = Problem' () Source
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
.
Focus | |
| |
LitFocus Literal OneHolePatterns Int Type |
data SplitProblem Source
Result of splitProblem
: Determines position for the next split.
Split | Split on constructor pattern. |
| |
SplitRest | Split on projection pattern. |
|
:: NamedArg Pattern |
|
-> ArgName |
|
-> Dom Type |
|
-> SplitProblem | The split problem, containing |
-> SplitProblem | The result, now containing |
Put a typed pattern on the very left of a SplitProblem
.
data DotPatternInst Source
State worked on during the main loop of checking a lhs.
LHSState | |
|