Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- data RunRecordPatternTranslation
- compileClauses' :: RunRecordPatternTranslation -> [Clause] -> Maybe SplitTree -> TCM CompiledClauses
- compileClauses :: Maybe (QName, Type) -> [Clause] -> TCM (Maybe SplitTree, Bool, CompiledClauses)
- data Cl = Cl {}
- type Cls = [Cl]
- unBruijn :: Clause -> Cl
- compileWithSplitTree :: SplitTree -> Cls -> CompiledClauses
- compile :: Cls -> CompiledClauses
- nextSplit :: Cls -> Maybe (Bool, Arg Int)
- properSplit :: Pattern' a -> Maybe Bool
- isVar :: Pattern' a -> Bool
- splitOn :: Bool -> Int -> Cls -> Case Cls
- splitC :: Int -> Cl -> Case Cl
- expandCatchAlls :: Bool -> Int -> Cls -> Cls
- ensureNPatterns :: Int -> [ArgInfo] -> Cl -> Cl
- substBody :: Subst a => Int -> Int -> SubstArg a -> a -> a
Documentation
data RunRecordPatternTranslation Source #
Instances
Eq RunRecordPatternTranslation Source # | |
Defined in Agda.TypeChecking.CompiledClause.Compile (==) :: RunRecordPatternTranslation -> RunRecordPatternTranslation -> Bool (/=) :: RunRecordPatternTranslation -> RunRecordPatternTranslation -> Bool |
compileClauses' :: RunRecordPatternTranslation -> [Clause] -> Maybe SplitTree -> TCM CompiledClauses Source #
:: Maybe (QName, Type) | Translate record patterns and coverage check with given type? |
-> [Clause] | |
-> TCM (Maybe SplitTree, Bool, CompiledClauses) | The |
Process function clauses into case tree.
This involves:
1. Coverage checking, generating a split tree.
2. Translation of lhs record patterns into rhs uses of projection.
Update the split tree.
3. Generating a case tree from the split tree.
Phases 1. and 2. are skipped if Nothing
.
Stripped-down version of Clause
used in clause compiler.
unBruijn :: Clause -> Cl Source #
Strip down a clause. Don't forget to apply the substitution to the dot patterns!
compileWithSplitTree :: SplitTree -> Cls -> CompiledClauses Source #
compile :: Cls -> CompiledClauses Source #
nextSplit :: Cls -> Maybe (Bool, Arg Int) Source #
Get the index of the next argument we need to split on. This the number of the first pattern that does a (non-lazy) match in the first clause. Or the first lazy match where all clauses agree on the constructor, if there are no non-lazy matches.
properSplit :: Pattern' a -> Maybe Bool Source #
Is is not a variable pattern? And if yes, is it a record pattern and/or a fallThrough one?
isVar :: Pattern' a -> Bool Source #
Is this a variable pattern?
Maintain invariant: isVar = isNothing . properSplit
!
splitOn :: Bool -> Int -> Cls -> Case Cls Source #
splitOn single n cs
will force expansion of catch-alls
if single
.
expandCatchAlls :: Bool -> Int -> Cls -> Cls Source #
Expand catch-alls that appear before actual matches.
Example:
true y x false false y
will expand the catch-all x
to false
.
Catch-alls need also to be expanded if they come before/after a record pattern, otherwise we get into trouble when we want to eliminate splits on records later.
Another example (see Issue 1650):
f (x, (y, z)) true = a
f _ false = b
Split tree:
0 (first argument of f)
- 1 (second component of the pair)
- 3 (last argument of f)
-- true -> a
- false -> b
We would like to get the following case tree:
case 0 of
_,_ -> case 1 of
_,_ -> case 3 of true -> a; false -> b
_ -> case 3 of true -> a; false -> b
_ -> case 3 of true -> a; false -> b
Example from issue #2168:
f x false = a
f false = _ -> b
f x true = c
case tree:
f x y = case y of
true -> case x of
true -> c
false -> b
false -> a
Example from issue #3628:
f i j k (i = i0)(k = i1) = base
f i j k (j = i1) = base
case tree:
f i j k o = case i of
i0 -> case k of
i1 -> base
_ -> case j of
i1 -> base
_ -> case j of
i1 -> base
ensureNPatterns :: Int -> [ArgInfo] -> Cl -> Cl Source #
Make sure (by eta-expansion) that clause has arity at least n
where n
is also the length of the provided list.
Orphan instances
PrecomputeFreeVars a => PrecomputeFreeVars (CompiledClauses' a) Source # | |
precomputeFreeVars :: CompiledClauses' a -> FV (CompiledClauses' a) Source # |