... | ... | @@ -8,13 +8,12 @@ overview of our approach see [PatternMatchCheck](pattern-match-check). |
|
|
|
|
|
The most relevant modules are:
|
|
|
|
|
|
- `deSugar/PmExpr.hs`: The expression type (`PmExpr`) and the term equalities (`SimpleEq`s and `ComplexEq`s) used by the checker (and the term oracle).
|
|
|
- `deSugar/TmOracle.hs`: The (incremental) term oracle and other relevant utilities. The interface to the solver is function `tmOracle`.
|
|
|
- `deSugar/Check.hs`: The main algorithm. Main exports are functions `checkSingle` (check a single binding -- let),
|
|
|
`checkMatches` (check a `MatchGroup` -- case expressions and functions) and `dsPmWarn` (print the results if the respective flags are enabled).
|
|
|
- `deSugar/PmExpr.hs`: Expressions (`PmExpr`, `PmLit`), term constraints (`SimpleEq`, `ComplexEq`) and utilities for the check and the term oracle.
|
|
|
- `deSugar/TmOracle.hs`: The term oracle and utilities. Three (incremental) interfaces to the oracle are exported: `tmOracle`, `solveOneEq` and `extendSubst`.
|
|
|
- `deSugar/Check.hs`: The main algorithm. Main exports are functions `checkSingle` (check a single binding -- let) and `checkMatches` (check a `MatchGroup` -- case expressions and functions).
|
|
|
|
|
|
|
|
|
We explain each one separately below.
|
|
|
We discuss each one separately below.
|
|
|
|
|
|
## The `PmExpr` Datatype and Friends
|
|
|
|
... | ... | @@ -22,7 +21,7 @@ We explain each one separately below. |
|
|
The module exports the following data types:
|
|
|
|
|
|
```
|
|
|
dataPmExpr=PmExprVarId|PmExprConDataCon[PmExpr]|PmExprLitPmLit|PmExprEqPmExprPmExpr-- Syntactic equality|PmExprOther(HsExprId)-- NOTE [PmExprOther in PmExpr]dataPmLit=PmSLitHsLit-- simple|PmOLitBool{- is it negated? -}(HsOverLitId)-- overloadedtypeSimpleEq=(Id,PmExpr)-- We always use this orientationtypeComplexEq=(PmExpr,PmExpr)
|
|
|
dataPmExpr=PmExprVarName|PmExprConDataCon[PmExpr]|PmExprLitPmLit|PmExprEqPmExprPmExpr-- Syntactic equality|PmExprOther(HsExprId)-- Note [PmExprOther in PmExpr]dataPmLit=PmSLitHsLit-- simple|PmOLitBool{- is it negated? -}(HsOverLitId)-- overloadedtypeSimpleEq=(Id,PmExpr)-- We always use this orientationtypeComplexEq=(PmExpr,PmExpr)
|
|
|
```
|
|
|
|
|
|
|
... | ... | @@ -35,15 +34,15 @@ PmExprEq(PmExprCon<False>[])(PmExprEq(PmExprVar<x>)(PmExprLit(PmSLit<5>))) |
|
|
```
|
|
|
|
|
|
|
|
|
Literals `PmLit` are separately defined because (as we explain below) appear in the pattern language as well. Equality check for
|
|
|
Literals `PmLit` are separately defined since (for efficiency reasons) appear in the pattern language as well. Equality check for
|
|
|
`PmLit` is exported too, with signature:
|
|
|
|
|
|
```
|
|
|
eqPmLit::PmLit->PmLit->MaybeBool
|
|
|
eqPmLit::PmLit->PmLit->Bool
|
|
|
```
|
|
|
|
|
|
|
|
|
Instead of `Bool` we return `Maybe Bool` because if two overloaded literals look different it does not mean they actually are. Hence
|
|
|
Strictly speaking, the result type should be `Maybe Bool`, since if two overloaded literals look different it does not mean they actually are. Hence
|
|
|
equality in this case is inconclusive, unless we unfold the `from`-function (like `fromInteger`). E.g. syntactic equality 5 \~ 6 is
|
|
|
not necessarily inconsistent, since it actually represents `fromInteger 5 ~ fromInteger 6` which depends on the implementation of
|
|
|
function `fromInteger`. On the other hand, `fromInteger 5 ~ fromInteger 5` is always true, since `fromInteger` is a pure function.
|
... | ... | @@ -52,24 +51,38 @@ function applications, we would get poor error messages for overloaded literals. |
|
|
looks a bit hackish though).
|
|
|
|
|
|
|
|
|
Term equalities take two forms: `SimpleEq` and `ComplexEq`. `SimpleEq`s are generated by the algorithm and are the input to the term
|
|
|
oracle, as we show in the paper. Yet, the oracle returns residual constraints which may be complex so we need a type for them as well.
|
|
|
E.g. { x \~ False, x \~ (y \~ 5) } gets simplified to { False \~ (y \~ 5) } which cannot progress unless we get more information about y.
|
|
|
Nevertheless, we close our eyes to the truth above and simply return a `Bool`. This way, the warnings are
|
|
|
more comprehensible.
|
|
|
|
|
|
|
|
|
Term equalities take two forms: `SimpleEq` and `ComplexEq`. In the paper we generate only simple equalities,
|
|
|
yet this is not so performant. In many cases we would generate `{ x ~ e1, x ~ e2 }` (for a fresh variable `x`)
|
|
|
instead of the much more direct `e1 ~ e2`. Hence, the current implementation generates `ComplexEq`s. `SimpleEq`s
|
|
|
are still used for nested pattern matching (see below).
|
|
|
|
|
|
## The Term Oracle
|
|
|
|
|
|
|
|
|
The term oracle lives in `deSugar/TmOracle.hs` and has the following signature:
|
|
|
The term oracle lives in `deSugar/TmOracle.hs` and has the following signature(s):
|
|
|
|
|
|
```
|
|
|
tmOracle::TmState->[SimpleEq]->MaybeTmState
|
|
|
solveOneEq::TmState->ComplexEq->MaybeTmStatetmOracle::TmState->[ComplexEq]->MaybeTmStateextendSubst::Id->PmExpr->TmState->TmState
|
|
|
```
|
|
|
|
|
|
|
|
|
The state of the oracle `TmState` is represented as follows:
|
|
|
Function `solveOneEq` --as the name suggests-- solves a single term constraint (which is the most common case)
|
|
|
while `tmOracle` takes a list of them. They are both designed to be called incrementally, hence they both take
|
|
|
a term oracle state as argument and return the resulting one (if consistent) as well. Function `extendSubst` is
|
|
|
used when we generate a fresh variable (e.g. when checking against guards), where no actual solving takes place.
|
|
|
It is much more efficient than `solveOneEq`, but is unsafe, since it does not check the invariant, that the
|
|
|
variable does not already exist in the state.
|
|
|
|
|
|
|
|
|
The state of the oracle
|
|
|
`TmState` is represented as follows:
|
|
|
|
|
|
```
|
|
|
typePmVarEnv=Map.MapIdPmExprtypeTmOracleEnv=(Bool,PmVarEnv)typeTmState=([ComplexEq],TmOracleEnv)
|
|
|
typePmVarEnv=Map.MapNamePmExprtypeTmOracleEnv=(Bool,PmVarEnv)typeTmState=([ComplexEq],TmOracleEnv)
|
|
|
```
|
|
|
|
|
|
`TmState` contains the following components:
|
... | ... | @@ -91,24 +104,22 @@ inspect can fail for all we know, so this boolean is used for the computation of |
|
|
|
|
|
The strategy of the term oracle is quite simplistic and proceeds as follows (for a single `SimpleEq`):
|
|
|
|
|
|
- Apply existing substitution to the equality (which leaves us with a `ComplexEq`)
|
|
|
- Try to simplify the constraint using `simplifyPmExpr :: PmExpr -> (PmExpr, Bool)`. Note that we return
|
|
|
a boolean along with the (possibly) simplified expression, which indicates whether there was any progress
|
|
|
or simplification was a no-op.
|
|
|
- Apply existing substitution to the equality using `applySubstComplexEq :: PmVarEnv -> ComplexEq -> ComplexEq`.
|
|
|
- Try to simplify the constraint using `simplifyComplexEq :: ComplexEq -> ComplexEq`.
|
|
|
- Try to solve the simplified complex equality using `solveComplexEq :: TmState -> ComplexEq -> Maybe TmState`.
|
|
|
If the existing substitution is extended during solving, we apply the extended substitution to the
|
|
|
constraints that could not progress before and recurse.
|
|
|
|
|
|
|
|
|
The essence of the oracle is function `solveSimpleEq` which implements the above:
|
|
|
Function `solveOneEq` implements the above:
|
|
|
|
|
|
```
|
|
|
solveSimpleEq::TmState->SimpleEq->MaybeTmStatesolveSimpleEq solver_env@(_,(_,env)) simple
|
|
|
solveOneEq::TmState->ComplexEq->MaybeTmStatesolveOneEq solver_env@(_,(_,env)) complex
|
|
|
= solveComplexEq solver_env
|
|
|
$ simplifyComplexEq
|
|
|
$ applySubstSimpleEq env simple
|
|
|
$ applySubstComplexEq env complex
|
|
|
|
|
|
tmOracle::TmState->[SimpleEq]->MaybeTmStatetmOracle= foldlM solveSimpleEq
|
|
|
tmOracle::TmState->[ComplexEq]->MaybeTmStatetmOracle tm_state eqs = foldlM solveOneEq tm_state eqs
|
|
|
```
|
|
|
|
|
|
**Note:** We have not implemented an OccursCheck, since it is not needed at the moment. If extended though,
|
... | ... | @@ -121,10 +132,9 @@ the oracle). |
|
|
The check itself is implemented in module `deSugar/Check.hs`. Exported functions:
|
|
|
|
|
|
```
|
|
|
-- Issue warningsdsPmWarn::DynFlags->DsMatchContext->DsMPmResult->DsM()-- Compute the covered/uncovered/divergent setscheckSingle::Id->PatId->DsMPmResult-- letcheckMatches::[Id]->[LMatchId(LHsExprId)]->DsMPmResult-- case/functions-- Nested pattern matchinggenCaseTmCs1::Maybe(LHsExprId)->[Id]->BagSimpleEqgenCaseTmCs2::Maybe(LHsExprId)-- Scrutinee->[PatId]-- LHS (should have length 1)->[Id]-- MatchVars (should have length 1)->DsM(BagSimpleEq)
|
|
|
-- Issue warningsdsPmWarn::DynFlags->DsMatchContext->DsMPmResult->DsM()-- Compute the covered/uncovered/divergent sets and-- issue the warnings if the respective flags are enabledcheckSingle::DynFlags->DsMatchContext->Id->PatId->DsM()-- letcheckMatches::DynFlags->DsMatchContext->[Id]->[LMatchId(LHsExprId)]->DsM()-- case/functions-- Nested pattern matchinggenCaseTmCs1::Maybe(LHsExprId)->[Id]->BagSimpleEqgenCaseTmCs2::Maybe(LHsExprId)-- Scrutinee->[PatId]-- LHS (should have length 1)->[Id]-- MatchVars (should have length 1)->DsM(BagSimpleEq)
|
|
|
```
|
|
|
|
|
|
- `dsPmWarn` is responsible for printing the results, given that the respective flags are enabled
|
|
|
- `checkSingle` performs the check on a single pattern (let bindings)
|
|
|
- `checkMatches` performs the check on a list of matches (case expressions / function bindings)
|
|
|
- `genCaseTmCs1` generates term constraints for nested pattern matching (see below)
|
... | ... | @@ -139,63 +149,60 @@ Before explaining what each function does, we first discuss the types used. |
|
|
The `PmPat` data type is defined in `deSugar/Check.hs` as:
|
|
|
|
|
|
```
|
|
|
dataPmPat p =PmCon{ pm_con_con ::DataCon, pm_con_arg_tys ::[Type]-- The univeral arg types, 1-1 with the universal-- tyvars of the constructor, pm_con_tvs ::[TyVar]-- Existentially bound type variables (tyvars only), pm_con_dicts ::[EvVar]-- Ditto *coercion variables* and *dictionaries*, pm_con_args ::[p]}|PmVar{ pm_var_id ::Id}|PmLit{ pm_lit_lit ::PmLit}-- See NOTE [Literals in PmPat]
|
|
|
dataPatTy=PAT|VA-- Used only as a kind, to index PmPatdataPmPat::PatTy->*wherePmCon::{ pm_con_con ::DataCon, pm_con_arg_tys ::[Type], pm_con_tvs ::[TyVar], pm_con_dicts ::[EvVar], pm_con_args ::[PmPat t]}->PmPat t
|
|
|
-- For PmCon arguments' meaning see @ConPatOut@ in hsSyn/HsPat.hsPmVar::{ pm_var_id ::Id}->PmPat t
|
|
|
PmLit::{ pm_lit_lit ::PmLit}->PmPat t -- See Note [Literals in PmPat]PmNLit::{ pm_lit_id ::Id, pm_lit_not ::[PmLit]}->PmPatVAPmGrd::{ pm_grd_pv ::PatVec, pm_grd_expr ::PmExpr}->PmPatPAT
|
|
|
```
|
|
|
|
|
|
|
|
|
Literal patterns are not essential for the algorithm to work, but, as we discuss below, it is
|
|
|
much more efficient to treat them more like constructors by matching against them eagerly than
|
|
|
generating equality constraints to feed the term oracle with (as we do in the paper). `PmCon`
|
|
|
contains several fields, effectively copying constructor `ConPatOut` of type `Pat` (defined in
|
|
|
`hsSyn/HsPat.hs`). Since the algorithm runs post-typechecking, we have a lot of information
|
|
|
available for the treatment of GADTS.
|
|
|
generating equality constraints to feed the term oracle with (as we do in the paper). Additionally,
|
|
|
we use negative patterns (constructor `PmNLit`), for efficiency also. `PmCon` contains several
|
|
|
fields, effectively copying constructor `ConPatOut` of type `Pat` (defined in `hsSyn/HsPat.hs`).
|
|
|
Since the algorithm runs post-typechecking, we have a lot of information available for the
|
|
|
treatment of GADTs.
|
|
|
|
|
|
### Value Abstractions & Patterns
|
|
|
|
|
|
|
|
|
Apart from the literal patterns, both value abstractions and patterns look exactly like in the
|
|
|
paper, and are both based on the `PmPat` type:
|
|
|
Apart from the literal/negative literal patterns, both value abstractions and patterns look exactly
|
|
|
like in the paper, and are both implemented by the `PmPat` type:
|
|
|
|
|
|
```
|
|
|
newtypeValAbs=VA(PmPatValAbs)-- Value AbstractionsdataPattern=PmGuardPatVecPmExpr-- Guard Patterns|NonGuard(PmPatPattern)-- Other Patterns
|
|
|
typePattern=PmPatPAT-- ^ PatternstypeValAbs=PmPatVA-- ^ Value Abstractions
|
|
|
```
|
|
|
|
|
|
|
|
|
A value abstraction ties the recursive knot with a newtype declaration whilst patterns introduce
|
|
|
another form: guard patterns.
|
|
|
|
|
|
|
|
|
Pattern vectors and value vector abstractions are simply lists of the respective types:
|
|
|
Similarly, a pattern vector is just a list of patterns, while a value vector abstraction looks
|
|
|
like the paper, that is, it is a list of value abstractions, accompanied by a set of constraints `Delta`:
|
|
|
|
|
|
```
|
|
|
typePatVec=[Pattern]-- Pattern VectorstypeValVecAbs=[ValAbs]-- Value Vector Abstractions
|
|
|
typePatVec=[Pattern]-- ^ Pattern VectorsdataValVec=ValVec[ValAbs]Delta-- ^ Value Vector AbstractionsdataDelta=MkDelta{ delta_ty_cs ::BagEvVar, delta_tm_cs ::TmState}
|
|
|
```
|
|
|
|
|
|
### Value Set Abstractions
|
|
|
|
|
|
A big difference from the theory is that instead of storing term constraints, we store in `Delta` the whole
|
|
|
term oracle state, that is, a much more efficient representation of the term constraints. This allows us to
|
|
|
have significantly better performance, especially since we have an incremental interface for the term oracle.
|
|
|
|
|
|
After `PmPat`, the most important data type of the checker is `ValSetAbs`, used to represent value set
|
|
|
abstractions. In the formalization we treat a value set abstraction as a list of value vector abstractions
|
|
|
but since the vectors we generate usually have a common prefix, we save space and time by representing
|
|
|
them as a prefix tree. This means that we have a choice to either add the constraint set Delta only at the
|
|
|
leaves or have constraints in internal nodes as well. To make the most out of our representation we chose
|
|
|
the latter. Notionally, every path from the root to a leaf represents a value vector abstraction, where the
|
|
|
set Delta is the union of all constraints in the path. This means that we have the following invariant not
|
|
|
represented in our type:
|
|
|
### Value Set Abstractions (Covered, Uncovered and Divergent Sets)
|
|
|
|
|
|
**INVARIANT VsaArity**: The number of `Cons`s in any path to a leaf is the same. We'll refer to this as the
|
|
|
arity of the value set abstraction.
|
|
|
|
|
|
Value set abstractions are just represented as a list of value vector abstractions:
|
|
|
|
|
|
```
|
|
|
dataValSetAbs=Empty-- {}|UnionValSetAbsValSetAbs-- S1 u S2|Singleton-- { |- empty |> empty }|Constraint[PmConstraint]ValSetAbs-- Extend Delta|ConsValAbsValSetAbs-- map (ucon u) vsdataPmConstraint=TmConstraintIdPmExpr-- TermEq : x ~ e|TyConstraint[EvVar]-- TypeEq : ...|BtConstraintId-- StrictVar : x ~ _|_
|
|
|
typeValSetAbs=[ValVec]-- ^ Value Set AbstractionstypeUncovered=ValSetAbs
|
|
|
```
|
|
|
|
|
|
**NOTE**: We have attempted to use a nicer representation of value set abstractions as prefix trees but
|
|
|
we faced some performance issues. Hence, we created the task [\#11528](https://gitlab.haskell.org//ghc/ghc/issues/11528) to further investigate whether such
|
|
|
an approach is achievable.
|
|
|
|
|
|
|
|
|
Additionally, instead of using constructors `Union`, `Constraint` and `Cons` to
|
|
|
construct value set abstractions, we use the smart constructors instead
|
|
|
`mkUnion`, `mkConstraint` and `mkCons` that ensure that an empty value set
|
|
|
abstraction is represented only by `Empty`. We refer to this as the
|
|
|
**INVARIANT VsaInvariant**.
|
|
|
Note that the only set we store is the uncovered set: For both the divergent and the covered set, we are only
|
|
|
interested in whether they are empty or not. Hence, instead of creating the sets and checking whether they are
|
|
|
empty or not afterwards, we check on the fly and use just a boolean for each.
|
|
|
|
|
|
### General Strategy
|
|
|
|
... | ... | @@ -206,17 +213,12 @@ The algorithm process as follows: |
|
|
is the workhorse):
|
|
|
|
|
|
```
|
|
|
translatePat::PatId->UniqSMPatVectranslateGuards::[GuardStmtId]->UniqSMPatVectranslateMatch::LMatchId(LHsExprId)->UniqSM(PatVec,[PatVec])
|
|
|
translatePat::FamInstEnvs->PatId->PmMPatVectranslateGuards::FamInstEnvs->[GuardStmtId]->PmMPatVectranslateMatch::FamInstEnvs->LMatchId(LHsExprId)->PmM(PatVec,[PatVec])
|
|
|
```
|
|
|
- Call function `patVectProc` on the transformed clause:
|
|
|
- Call function `pmcheck` on the transformed clause:
|
|
|
|
|
|
```
|
|
|
patVectProc::(PatVec,[PatVec])->ValSetAbs->PmM(Bool,Bool,ValSetAbs)-- Covers? Forces? U(n+1)?patVectProc(vec,gvs) vsa =do
|
|
|
us <- getUniqueSupplyM
|
|
|
let(c_def, u_def, d_def)= process_guards us gvs -- default (the continuation)(usC, usU, usD)<- getUniqueSupplyM3
|
|
|
mb_c <- anySatVSA (covered usC c_def vec vsa)
|
|
|
mb_d <- anySatVSA (divergent usD d_def vec vsa)let vsa' = uncovered usU u_def vec vsa
|
|
|
return (mb_c, mb_d, vsa')
|
|
|
pmcheck::PatVec->[PatVec]->ValVec->PmMTriplepmcheckHd::Pattern->PatVec->[PatVec]->ValAbs->ValVec->PmMTriplepmcheckGuards::[PatVec]->ValVec->PmMTripletypeTriple=(Bool,Uncovered,Bool)
|
|
|
```
|
|
|
|
|
|
|
... | ... | @@ -234,42 +236,32 @@ it). That is: |
|
|
|
|
|
|
|
|
Since this is really bad for performance (significantly increases the number of clauses), we took a different
|
|
|
approach: Process the guards separately using `process_guards` and plug the results at the end of the respective
|
|
|
approach: Process the guards separately using `pmcheckGuards` and plug the results at the end of the respective
|
|
|
clause. Yet, this comes with a price: We are not able to issue warnings per-guard but only per-clause. This was
|
|
|
the case already in GHC though (see ticket [\#8494](https://gitlab.haskell.org//ghc/ghc/issues/8494)).
|
|
|
|
|
|
|
|
|
Furthermore, note that `patVectProc` does not return three sets as in the paper. Instead, we check for the
|
|
|
satisfiability of the covered and the divergent set and return a boolean (covers anything/does not cover,
|
|
|
forces any argument/does not force, respectively). Since this is the only information we care about at the
|
|
|
end, it would be a waste of space to keep the whole covered and divergent set in memory.
|
|
|
|
|
|
### Covered, Divergent, Uncovered
|
|
|
|
|
|
|
|
|
Since the three functions have the same structure and the representation of value set abstractions `ValSetAbs`
|
|
|
adds some boilerplate, the implementation of the functions is split in two parts: `pmTraverse` handles the
|
|
|
common cases and takes as argument the matcher to use when we have a value abstraction and a pattern to match
|
|
|
against. The three matchers `cMatcher`, `uMatcher` and `dMatcher` essentially implement functions `covered`,
|
|
|
`uncovered` and `divergent` as described in the paper.
|
|
|
|
|
|
```
|
|
|
pmTraverse::UniqSupply->ValSetAbs-- guard continuation->PmMatcher-- what to do->PatVec->ValSetAbs->ValSetAbstypePmMatcher=UniqSupply->ValSetAbs->PmPatPattern->PatVec-- pattern vector head and tail->PmPatValAbs->ValSetAbs-- value set abstraction head and tail->ValSetAbscovered, uncovered, divergent ::UniqSupply->ValSetAbs->PatVec->ValSetAbs->ValSetAbscovered us gvsa vec vsa = pmTraverse us gvsa cMatcher vec vsa
|
|
|
uncovered us gvsa vec vsa = pmTraverse us gvsa uMatcher vec vsa
|
|
|
divergent us gvsa vec vsa = pmTraverse us gvsa dMatcher vec vsa
|
|
|
```
|
|
|
All three `pmcheck`-functions compute (as the signatures suggest) coverage, exhaustiveness and divergence at
|
|
|
once. `pmcheck` is the main interface that takes a pattern vector, the guard vectors and the uncovered set and
|
|
|
returns all three results. It basically handles the guard case (see paper) and if both the value vector
|
|
|
abstraction and the pattern vector are in head-tail form, calls `pmcheckHd` to handle the rest of the cases.
|
|
|
When both the value vector abstraction and the pattern vector are empty, `pmcheckGuards` is called, to handle
|
|
|
the guards.
|
|
|
|
|
|
|
|
|
Note the signatures:
|
|
|
Since GHC is a production compiler and the uncovered set can grow exponentially, the recursive calls had to be
|
|
|
bounded. Hence, three variants are used in the recursive positions: `pmcheckI`, `pmcheckHdI` and `pmcheckGuardsI`
|
|
|
(`I` comes from "increment"). All three variants simply call the respective function, after increasing a counter
|
|
|
of the iterations elapsed. For example, `pmcheckI` is defined as follows:
|
|
|
|
|
|
```
|
|
|
covered, uncovered, divergent ::UniqSupply->ValSetAbs->PatVec->ValSetAbs->ValSetAbs
|
|
|
pmcheckI::PatVec->[PatVec]->ValVec->PmMTriplepmcheckI ps guards vva = incrCheckPmIterDs >> pmcheck ps guards vva
|
|
|
```
|
|
|
|
|
|
|
|
|
Instead of making the three functions monadic, we instead pass the `UniqSupply` around explicitly to make the
|
|
|
functions lazy. Since the trees that are generated by the algorithm are potentially huge (the algorithm is
|
|
|
exponential in the general case), we do not evaluate parts of the sets if they are not really needed.
|
|
|
By default, the number of iterations for bailing is 10000000 (none of the tests we have tried seems to exceed that
|
|
|
yet) but it can be set with: `-fmax-pmcheck-iterations=n`. Function `warnPmIters` in `deSugar/Check.hs` issues a
|
|
|
warning if the limit is exceeded.
|
|
|
|
|
|
### Nested Pattern Matching
|
|
|
|
... | ... | @@ -331,4 +323,19 @@ in GHC required several approximations and simplifications: |
|
|
|
|
|
```
|
|
|
f::Bool->()fTrue(x <-True)=()-- uncovered: { False |> { x ~ True } }fFalse(y <-False)=()-- uncovered: {}
|
|
|
```
|
|
|
|
|
|
1. In general, when a guard is not going to contribute, during translation we transform it to a `can fail`
|
|
|
pattern:
|
|
|
|
|
|
```
|
|
|
-- | A fake guard pattern (True <- _) used to represent cases we cannot handlefake_pat::Patternfake_pat=PmGrd{ pm_grd_pv =[truePattern], pm_grd_expr =PmExprOtherEWildPat}
|
|
|
```
|
|
|
|
|
|
Later when we check (with `pmcheck`), in case we reach a guard, we short-circuit if it is a "fake" one.
|
|
|
This trick saves a lot of effort in practice (in terms of both memory consumption and performance):
|
|
|
|
|
|
```
|
|
|
pmcheck(p@(PmGrd pv e): ps) guards vva@(ValVec vas delta)| isFakeGuard pv e = forces . mkCons vva <$> pmcheckI ps guards vva
|
|
|
| otherwise =...
|
|
|
``` |
|
|
\ No newline at end of file |