Safe Haskell | None |
---|---|
Language | Haskell2010 |
- type Substitution = [Maybe Term]
- type FlexibleVars = [FlexibleVar Nat]
- data FlexibleVarKind
- data FlexibleVar a = FlexibleVar {
- flexHiding :: Hiding
- flexKind :: FlexibleVarKind
- flexPos :: Maybe Int
- flexVar :: a
- defaultFlexibleVar :: a -> FlexibleVar a
- flexibleVarFromHiding :: Hiding -> a -> FlexibleVar a
- allFlexVars :: Telescope -> FlexibleVars
- data FlexChoice
- class ChooseFlex a where
- data Problem' p = Problem {}
- type Problem = Problem' [NamedArg DeBruijnPattern]
- type ProblemPart = Problem' ()
- data ProblemRest = ProblemRest {}
- data Focus
- = Focus {
- focusCon :: QName
- focusPatOrigin :: ConOrigin
- focusConArgs :: [NamedArg Pattern]
- focusRange :: Range
- focusOutPat :: [NamedArg DeBruijnPattern]
- focusDatatype :: QName
- focusParams :: [Arg Term]
- focusIndices :: [Arg Term]
- focusType :: Type
- | LitFocus Literal [NamedArg DeBruijnPattern] Type
- = Focus {
- data SplitProblem
- consSplitProblem :: NamedArg Pattern -> ArgName -> Dom Type -> SplitProblem -> SplitProblem
- data DotPatternInst = DPI {}
- data AsBinding = AsB Name Term Type
- data LHSState = LHSState {
- lhsProblem :: Problem
- lhsDPI :: [DotPatternInst]
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 [FlexibleVarKind] | From a record pattern ( |
ImplicitFlex | From a hidden formal argument or underscore ( |
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 # | |
Show a => Show (FlexibleVar a) Source # | |
LensHiding (FlexibleVar a) Source # | |
ChooseFlex a => ChooseFlex (FlexibleVar a) Source # | |
defaultFlexibleVar :: a -> FlexibleVar a Source #
flexibleVarFromHiding :: Hiding -> a -> FlexibleVar a Source #
allFlexVars :: Telescope -> FlexibleVars Source #
data FlexChoice Source #
class ChooseFlex a where Source #
chooseFlex :: a -> a -> FlexChoice Source #
ChooseFlex Int Source # | |
ChooseFlex Hiding Source # | |
ChooseFlex FlexibleVarKind Source # | |
ChooseFlex a => ChooseFlex [a] Source # | |
ChooseFlex a => ChooseFlex (Maybe a) Source # | |
ChooseFlex a => ChooseFlex (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' [NamedArg DeBruijnPattern] Source #
The de Bruijn indices in the pattern refer to positions in the list of abstract patterns in the problem, counted from the back.
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 [NamedArg DeBruijnPattern] 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 #
Instantiations of a dot pattern with a term.
`Maybe e` if the user wrote a dot pattern .e
Nothing
if this is an instantiation of an implicit argument or a name.
State worked on during the main loop of checking a lhs.
LHSState | |
|